1(* standard prelude *) 2open HolKernel boolLib Parse 3 4 5(* extra theorem-proving oomph from libraries *) 6open bossLib metisLib ncLib BasicProvers boolSimps 7 8 9 10(* ancestor theories *) 11open fsubtypesTheory pred_setTheory 12 sortingTheory (* for theorems about permutations *) 13 14val _ = new_theory "full_subtyping" 15 16val _ = add_rule {block_style = (AroundEachPhrase, (PP.INCONSISTENT, 2)), 17 fixity = Infix(NONASSOC, 425), 18 paren_style = OnlyIfNecessary, 19 pp_elements = [HardSpace 1, TOK "|-", BreakSpace(1, 0), 20 BeginFinalBlock(PP.INCONSISTENT, 2), 21 TM, HardSpace 1, TOK "<:", BreakSpace(1,0)], 22 term_name = "fsubtyping"} 23 24(* define subtyping rules : figure 26-2 *) 25val (fsubtyping_rules, fsubtyping_ind, fsubtyping_cases) = Hol_reln` 26 (!Gamma ty. wfctxt Gamma /\ ftyFV ty SUBSET cdom Gamma ==> 27 Gamma |- ty <: ty) /\ 28 (!Gamma ty1 ty2 ty3. Gamma |- ty1 <: ty2 /\ 29 Gamma |- ty2 <: ty3 ==> 30 Gamma |- ty1 <: ty3) /\ 31 (!Gamma ty. wfctxt Gamma /\ ftyFV ty SUBSET cdom Gamma ==> 32 Gamma |- ty <: Top) /\ 33 (!Gamma x ty. wfctxt Gamma /\ MEM (x, ty) Gamma ==> 34 Gamma |- TyVar x <: ty) /\ 35 (!Gamma s1 t1 s2 t2. 36 Gamma |- t1 <: s1 /\ Gamma |- s2 <: t2 ==> 37 Gamma |- Fun s1 s2 <: Fun t1 t2) /\ 38 (!Gamma x s1 t1 s2 t2. 39 Gamma |- t1 <: s1 /\ 40 ((x,t1) :: Gamma) |- s2 <: t2 ==> 41 Gamma |- ForallTy x s1 s2 <: ForallTy x t1 t2) 42`; 43 44val fsubtyping_swap = store_thm( 45 "fsubtyping_swap", 46 ``!G t1 t2. G |- t1 <: t2 ==> 47 !x y. ctxtswap x y G |- fswap x y t1 <: fswap x y t2``, 48 HO_MATCH_MP_TAC fsubtyping_ind THEN REPEAT CONJ_TAC THENL [ 49 SRW_TAC [][SUBSET_DEF, fsubtyping_rules], 50 METIS_TAC [fsubtyping_rules], 51 SRW_TAC [][SUBSET_DEF, fsubtyping_rules], 52 SRW_TAC [][fsubtyping_rules], 53 SRW_TAC [][fsubtyping_rules], 54 SRW_TAC [][SUBSET_DEF, fsubtyping_rules] 55 ]); 56 57val fsubtyping_wfctxt = store_thm( 58 "fsubtyping_wfctxt", 59 ``!G t1 t2. G |- t1 <: t2 ==> wfctxt G``, 60 HO_MATCH_MP_TAC fsubtyping_ind THEN SRW_TAC [][]); 61 62(* define algorithmic sub-typing, with a depth of derivation parameter *) 63val (algn_subtyping_rules, algn_subtyping_ind, algn_subtyping_cases) = 64 Hol_reln` 65 (!Gamma s. wfctxt Gamma /\ ftyFV s SUBSET cdom Gamma ==> 66 algn_subtyping 0 Gamma s Top) /\ 67 (!Gamma x. wfctxt Gamma /\ x IN cdom Gamma ==> 68 algn_subtyping 0 Gamma (TyVar x) (TyVar x)) /\ 69 (!Gamma x u t n. MEM (x, u) Gamma /\ algn_subtyping n Gamma u t ==> 70 algn_subtyping (n + 1) Gamma (TyVar x) t) /\ 71 (!Gamma t1 s1 t2 s2 n m. 72 algn_subtyping n Gamma t1 s1 /\ 73 algn_subtyping m Gamma s2 t2 ==> 74 algn_subtyping (MAX n m + 1) Gamma (Fun s1 s2) (Fun t1 t2)) /\ 75 (!Gamma x s1 s2 t1 t2 m n. 76 algn_subtyping m Gamma t1 s1 /\ 77 algn_subtyping n ((x,t1)::Gamma) s2 t2 ==> 78 algn_subtyping (MAX m n + 1) Gamma (ForallTy x s1 s2) 79 (ForallTy x t1 t2)) 80`; 81 82val algn_subtyping_swap = store_thm( 83 "algn_subtyping_swap", 84 ``!n G t1 t2. algn_subtyping n G t1 t2 ==> 85 !x y. algn_subtyping n (ctxtswap x y G) 86 (fswap x y t1) (fswap x y t2)``, 87 HO_MATCH_MP_TAC algn_subtyping_ind THEN 88 SRW_TAC [][algn_subtyping_rules, SUBSET_DEF] THEN 89 (* only sa-trans-tvar case remains *) 90 MATCH_MP_TAC (List.nth(CONJUNCTS algn_subtyping_rules, 2)) THEN 91 Q.EXISTS_TAC `fswap x' y t1` THEN SRW_TAC [][]); 92 93val algn_subtyping_swap1_eqn = store_thm( 94 "algn_subtyping_swap1_eqn", 95 ``!n G t1 t2 x y. algn_subtyping n G (fswap x y t1) t2 = 96 algn_subtyping n (ctxtswap x y G) t1 (fswap x y t2)``, 97 METIS_TAC [algn_subtyping_swap, ctxtswap_inv, fswap_inv]); 98 99val algn_subtyping_wfctxt = store_thm( 100 "algn_subtyping_wfctxt", 101 ``!n G t1 t2. algn_subtyping n G t1 t2 ==> wfctxt G``, 102 HO_MATCH_MP_TAC algn_subtyping_ind THEN SRW_TAC [][]); 103 104val cdom_APPEND = store_thm( 105 "cdom_APPEND", 106 ``cdom (X ++ Y) = cdom X UNION cdom Y``, 107 SRW_TAC [DNF_ss][cdom_MEM, EXTENSION]); 108val _ = export_rewrites ["cdom_APPEND"] 109 110val wfctxt_APPEND = store_thm( 111 "wfctxt_APPEND", 112 ``!X Y. DISJOINT (cdom X) (cdom Y) /\ wfctxt X /\ wfctxt Y ==> 113 wfctxt (X ++ Y)``, 114 Induct THEN 115 ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, SUBSET_DEF]); 116 117val wfctxt_APPEND_down = store_thm( 118 "wfctxt_APPEND_down", 119 ``!X Y x y z. wfctxt (X ++ (x,y)::Y) /\ ftyFV z SUBSET cdom Y ==> 120 wfctxt (X ++ (x,z)::Y)``, 121 Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD] THEN 122 METIS_TAC []); 123 124val wfctxt_INSERT = store_thm( 125 "wfctxt_INSERT", 126 ``!D G v ty. 127 wfctxt (D ++ G) /\ ~(v IN cdom D) /\ ~(v IN cdom G) /\ 128 ftyFV ty SUBSET cdom G ==> 129 wfctxt (D ++ (v,ty)::G)``, 130 Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD] THEN 131 SRW_TAC [][SUBSET_DEF] THEN METIS_TAC []); 132 133val wfctxt_APPEND_DISJOINT = store_thm( 134 "wfctxt_APPEND_DISJOINT", 135 ``!X Y. wfctxt (X ++ Y) ==> DISJOINT (cdom X) (cdom Y)``, 136 Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD]); 137 138val ctxtswap_APPEND = store_thm( 139 "ctxtswap_APPEND", 140 ``!X Y. ctxtswap x y (X ++ Y) = ctxtswap x y X ++ ctxtswap x y Y``, 141 Induct THEN SRW_TAC [][]); 142val _ = export_rewrites ["ctxtswap_APPEND"] 143 144val cdom_PERM = store_thm( 145 "cdom_PERM", 146 ``!G1 G2. PERM G1 G2 ==> (cdom G1 = cdom G2)``, 147 HO_MATCH_MP_TAC PERM_IND THEN 148 ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, INSERT_COMM]); 149 150val algn_subtyping_FVs = store_thm( 151 "algn_subtyping_FVs", 152 ``!n G ty1 ty2. algn_subtyping n G ty1 ty2 ==> 153 ftyFV ty1 SUBSET cdom G /\ 154 ftyFV ty2 SUBSET cdom G``, 155 HO_MATCH_MP_TAC algn_subtyping_ind THEN SRW_TAC [][] THENL [ 156 METIS_TAC [cdom_MEM], 157 FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN METIS_TAC [], 158 FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN METIS_TAC [] 159 ]); 160 161val strong_algn_subtyping_ind = 162 IndDefRules.derive_strong_induction (CONJUNCTS algn_subtyping_rules, 163 algn_subtyping_ind) 164 165(* lemma 28.4.1.1 *) 166val algn_subtyping_permutation = store_thm( 167 "algn_subtyping_permutation", 168 ``!n G t1 t2. algn_subtyping n G t1 t2 ==> 169 !D. PERM D G /\ wfctxt D ==> 170 algn_subtyping n D t1 t2``, 171 HO_MATCH_MP_TAC strong_algn_subtyping_ind THEN REPEAT CONJ_TAC THENL [ 172 METIS_TAC [algn_subtyping_rules, cdom_PERM], 173 METIS_TAC [algn_subtyping_rules, cdom_PERM], 174 METIS_TAC [algn_subtyping_rules, PERM_MEM_EQ], 175 METIS_TAC [algn_subtyping_rules], 176 REPEAT STRIP_TAC THEN 177 MATCH_MP_TAC (last (CONJUNCTS algn_subtyping_rules)) THEN 178 `wfctxt ((x,t1')::G)` by METIS_TAC [algn_subtyping_wfctxt] THEN 179 `~(x IN cdom G) /\ ftyFV t1' SUBSET cdom G` 180 by FULL_SIMP_TAC (srw_ss()) [] THEN 181 `~(x IN cdom D) /\ ftyFV t1' SUBSET cdom D` 182 by METIS_TAC [cdom_PERM] THEN 183 CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN SRW_TAC [][] 184 ]); 185 186(* lemma 28.4.1.2 *) 187val algn_subtyping_weakening = store_thm( 188 "algn_subtyping_weakening", 189 ``!n G t1 t2. algn_subtyping n G t1 t2 ==> 190 !D. wfctxt (D ++ G) ==> algn_subtyping n (D ++ G) t1 t2``, 191 HO_MATCH_MP_TAC strong_algn_subtyping_ind THEN REPEAT CONJ_TAC THENL[ 192 SRW_TAC [][SUBSET_DEF, wfctxt_APPEND, algn_subtyping_rules], 193 SRW_TAC [][SUBSET_DEF, wfctxt_APPEND, algn_subtyping_rules], 194 METIS_TAC [listTheory.MEM_APPEND, algn_subtyping_rules], 195 SRW_TAC [][algn_subtyping_rules], 196 197 (* SA-ALL case *) 198 Q_TAC SUFF_TAC 199 `!G x s1 s2 t1 t2 m n. 200 algn_subtyping m G t1 s1 /\ 201 (!D. wfctxt (D ++ G) ==> algn_subtyping m (D ++ G) t1 s1) /\ 202 algn_subtyping n ((x,t1)::G) s2 t2 /\ 203 (!D. wfctxt (D ++ (x,t1)::G) ==> 204 algn_subtyping n (D ++ (x,t1)::G) s2 t2) ==> 205 !D. wfctxt (D ++ G) ==> 206 algn_subtyping (MAX m n + 1) (D ++ G) 207 (ForallTy x s1 s2) 208 (ForallTy x t1 t2)` THEN1 209 SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN 210 REPEAT STRIP_TAC THEN 211 (* generate fresh z *) 212 Q_TAC (NEW_TAC "z") `ftyFV t1 UNION cdom G UNION cdom D UNION ftyFV s2 213 UNION ftyFV t2 UNION {x}` THEN 214 215 (* state that types have alpha equivalent forms involving z *) 216 `(ForallTy x s1 s2 = ForallTy z s1 (fswap z x s2)) /\ 217 (ForallTy x t1 t2 = ForallTy z t1 (fswap z x t2))` 218 by SRW_TAC [][ForallTy_11] THEN 219 220 (* by SA-ALL rule if suffices to show (various side conditions drop 221 out because z is fresh) ... *) 222 Q_TAC SUFF_TAC 223 `algn_subtyping m (D ++ G) t1 s1 /\ 224 algn_subtyping n ((z,t1)::(D ++ G)) (fswap z x s2) (fswap z x t2)` 225 THEN1 SRW_TAC [][algn_subtyping_rules, SUBSET_DEF] THEN 226 227 `wfctxt ((x,t1)::G) /\ wfctxt G` by METIS_TAC [algn_subtyping_wfctxt] THEN 228 `~(x IN cdom G) /\ (!v. v IN ftyFV t1 ==> v IN cdom G)` 229 by FULL_SIMP_TAC (srw_ss()) [wfctxt_def, SUBSET_DEF] THEN 230 `~(x IN ftyFV t1)` by METIS_TAC [] THEN 231 232 (* move swaps out, over (z,t1), the z turns into x; the t1 is unchanged 233 because z and x are both fresh wrt it, similarly G *) 234 Q_TAC SUFF_TAC 235 `algn_subtyping n ((x,t1)::ctxtswap z x D ++ G) s2 t2` 236 THEN1 SRW_TAC [][algn_subtyping_swap1_eqn, fswap_fresh, 237 ctxtswap_fresh, wfctxt_ctxtFV_cdom] THEN 238 239 (* set up appeal to permutation result *) 240 `PERM ((x,t1)::ctxtswap z x D ++ G) (ctxtswap z x D ++ (x,t1)::G)` 241 by (SRW_TAC [][PERM_CONS_EQ_APPEND] THEN 242 METIS_TAC [PERM_REFL]) THEN 243 244 (* the permuted context is well-formed too: *) 245 `wfctxt (ctxtswap z x D ++ G)` 246 by (`ctxtswap z x D ++ G = ctxtswap z x (D ++ G)` 247 by SRW_TAC [][ctxtswap_fresh, wfctxt_ctxtFV_cdom] THEN 248 METIS_TAC [wfctxt_swap]) THEN 249 `wfctxt ((x,t1) :: ctxtswap z x D ++ G)` 250 by SRW_TAC [][SUBSET_DEF, wfctxt_APPEND] THEN 251 252 (* apply permutation result *) 253 Q_TAC SUFF_TAC 254 `algn_subtyping n (ctxtswap z x D ++ (x,t1)::G) s2 t2` 255 THEN1 METIS_TAC [algn_subtyping_permutation] THEN 256 257 (* apply IH *) 258 Q_TAC SUFF_TAC `wfctxt (ctxtswap z x D ++ (x,t1)::G)` 259 THEN1 SRW_TAC [][] THEN 260 261 `ctxtswap z x D ++ (x,t1)::G = ctxtswap z x (D ++ (z,t1)::G)` 262 by SRW_TAC [][fswap_fresh, ctxtswap_fresh, wfctxt_ctxtFV_cdom] THEN 263 SRW_TAC [][wfctxt_INSERT, SUBSET_DEF] 264 ]); 265 266val algn_subtyping_Top_left = store_thm( 267 "algn_subtyping_Top_left", 268 ``algn_subtyping n G Top t = (t = Top) /\ (n = 0) /\ wfctxt G``, 269 ONCE_REWRITE_TAC [algn_subtyping_cases] THEN 270 SRW_TAC [][] THEN METIS_TAC []); 271val _ = export_rewrites ["algn_subtyping_Top_left"] 272 273val wfctxt_assoc_unique = store_thm( 274 "wfctxt_assoc_unique", 275 ``!G x y z. wfctxt G /\ MEM (x,y) G /\ MEM (x,z) G ==> (z = y)``, 276 Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, cdom_MEM] THEN 277 METIS_TAC []); 278 279val algn_subtyping_foralltyleft_inversion = store_thm( 280 "algn_subtyping_foralltyleft_inversion", 281 ``~(x IN cdom G) /\ ~(x IN ftyFV t1) ==> 282 (algn_subtyping n G (ForallTy x t1 t2) t = 283 wfctxt G /\ 284 ((t = Top) /\ (n = 0) /\ ftyFV (ForallTy x t1 t2) SUBSET cdom G \/ 285 (?t1' t2' m1 m2. (t = ForallTy x t1' t2') /\ 286 (n = MAX m1 m2 + 1) /\ 287 algn_subtyping m1 G t1' t1 /\ 288 algn_subtyping m2 ((x,t1')::G) t2 t2')))``, 289 SIMP_TAC (srw_ss() ++ DNF_ss ++ SatisfySimps.SATISFY_ss) 290 [EQ_IMP_THM, algn_subtyping_rules, algn_subtyping_wfctxt] THEN 291 STRIP_TAC THEN 292 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [algn_subtyping_cases])) THEN 293 SRW_TAC[][] THEN DISJ2_TAC THEN 294 Cases_on `x = x'` THEN FULL_SIMP_TAC (srw_ss()) [ForallTy_11] THENL [ 295 METIS_TAC [], 296 Q.EXISTS_TAC `fswap x x' t2'` THEN 297 SRW_TAC [][algn_subtyping_swap1_eqn] THEN 298 `wfctxt G /\ wfctxt ((x',t1')::G)` 299 by METIS_TAC [algn_subtyping_wfctxt] THEN 300 `~(x' IN cdom G) /\ (!v. v IN ftyFV t1' ==> v IN cdom G)` 301 by METIS_TAC [SUBSET_DEF, wfctxt_def] THEN 302 `~(x' IN ftyFV t1') /\ ~(x IN ftyFV t1')` by METIS_TAC [] THEN 303 `ctxtswap x x' G = G` 304 by SRW_TAC [][ctxtswap_fresh, wfctxt_ctxtFV_cdom] THEN 305 SRW_TAC [][fswap_fresh] THEN 306 `ftyFV t2' SUBSET cdom ((x',t1')::G)` 307 by METIS_TAC [algn_subtyping_FVs] THEN 308 `~(x IN ftyFV t2')` 309 by METIS_TAC [SUBSET_DEF, cdom_def, IN_INSERT, pairTheory.FST] THEN 310 METIS_TAC [] 311 ]); 312 313val lemma28_4_2_0 = prove( 314 ``!sz q. (fsize q = sz) ==> 315 (!i j G s t. algn_subtyping i G s q /\ algn_subtyping j G q t ==> 316 ?k. algn_subtyping k G s t) /\ 317 (!i j G D p m n x. 318 algn_subtyping i (D ++ ((x,q) :: G)) m n /\ 319 algn_subtyping j G p q ==> 320 ?k. algn_subtyping k (D ++ (x,p) :: G) m n)``, 321 HO_MATCH_MP_TAC arithmeticTheory.COMPLETE_INDUCTION THEN 322 GEN_TAC THEN 323 DISCH_THEN (STRIP_ASSUME_TAC o SIMP_RULE (srw_ss() ++ DNF_ss) []) THEN 324 GEN_TAC THEN STRIP_TAC THEN 325 (* part 1 *) 326 `!i j G s t. 327 algn_subtyping i G s q /\ algn_subtyping j G q t ==> 328 ?k. algn_subtyping k G s t` 329 by (HO_MATCH_MP_TAC arithmeticTheory.COMPLETE_INDUCTION THEN 330 GEN_TAC THEN STRIP_TAC THEN REPEAT GEN_TAC THEN 331 CONV_TAC (LAND_CONV 332 (LAND_CONV 333 (ONCE_REWRITE_CONV [algn_subtyping_cases]))) THEN 334 SRW_TAC [][] THENL [ 335 (* Top case *) 336 FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][] THEN 337 METIS_TAC [algn_subtyping_rules], 338 (* Tyvar case - 1*) 339 METIS_TAC [], 340 (* Tyvar case - 2*) 341 `?k. algn_subtyping k G u t` 342 by METIS_TAC [DECIDE ``n < n + 1``] THEN 343 METIS_TAC [algn_subtyping_rules], 344 (* Fun case *) 345 Q.PAT_ASSUM `algn_subtyping X Y (Fun t1 t2) Z` 346 (MP_TAC o 347 ONCE_REWRITE_RULE [algn_subtyping_cases]) THEN 348 SRW_TAC [][] THENL [ 349 METIS_TAC [algn_subtyping_rules, ftyFV_thm, UNION_SUBSET, 350 algn_subtyping_FVs], 351 `fsize t1 < fsize (Fun t1 t2) /\ fsize t2 < fsize (Fun t1 t2)` 352 by SRW_TAC [numSimps.ARITH_ss][fsize_thm] THEN 353 `(?k1. algn_subtyping k1 G t1' s1) /\ 354 (?k2. algn_subtyping k2 G s2 t2')` 355 by METIS_TAC [] THEN 356 METIS_TAC [algn_subtyping_rules] 357 ], 358 359 (* ForallTy case *) 360 `wfctxt G /\ wfctxt ((x,t1)::G)` 361 by METIS_TAC [algn_subtyping_wfctxt] THEN 362 `~(x IN cdom G) /\ (!v. v IN ftyFV t1 ==> v IN cdom G)` 363 by FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN 364 `~(x IN ftyFV t1)` by METIS_TAC [] THEN 365 `ftyFV s1 SUBSET cdom G /\ ftyFV s2 SUBSET cdom ((x,t1)::G)` 366 by METIS_TAC [algn_subtyping_FVs] THEN 367 `~(x IN ftyFV s1)` by METIS_TAC [SUBSET_DEF] THEN 368 Q.PAT_ASSUM `algn_subtyping X Y (ForallTy x t1 t2) Z` MP_TAC THEN 369 SRW_TAC [][algn_subtyping_foralltyleft_inversion] THENL [ 370 FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN 371 METIS_TAC [], 372 SRW_TAC [][ForallTy_11] THEN 373 `fsize t1 < fsize (ForallTy x t1 t2) /\ 374 fsize t2 < fsize (ForallTy x t1 t2)` 375 by SRW_TAC[numSimps.ARITH_ss][fsize_thm] THEN 376 `?k1. algn_subtyping k1 G t1' s1` by METIS_TAC [] THEN 377 Q_TAC SUFF_TAC 378 `?k2. algn_subtyping k2 ((x,t1')::G) s2 t2'` 379 THEN1 METIS_TAC [] THEN 380 Q_TAC SUFF_TAC 381 `?k3. algn_subtyping k3 ((x,t1')::G) s2 t2` 382 THEN1 METIS_TAC [] THEN 383 METIS_TAC [listTheory.APPEND] 384 ] 385 ]) THEN 386 (* part 2 *) 387 CONJ_TAC THEN1 FIRST_ASSUM ACCEPT_TAC THEN 388 HO_MATCH_MP_TAC arithmeticTheory.COMPLETE_INDUCTION THEN 389 REPEAT STRIP_TAC THEN 390 `ftyFV p SUBSET cdom G` by METIS_TAC [algn_subtyping_FVs] THEN 391 `wfctxt (D ++ (x,q)::G)` by METIS_TAC [algn_subtyping_wfctxt] THEN 392 `wfctxt (D ++ (x,p)::G)` by METIS_TAC [wfctxt_APPEND_down] THEN 393 Q.PAT_ASSUM `algn_subtyping X (D ++ Y :: G) M N` MP_TAC THEN 394 Q.ABBREV_TAC `xqctxt = D ++ (x,q) :: G` THEN 395 Q.ABBREV_TAC `xpctxt = D ++ (x,p) :: G` THEN 396 `cdom xpctxt = cdom xqctxt` by SRW_TAC [][Abbr`xpctxt`, Abbr`xqctxt`] THEN 397 CONV_TAC (LAND_CONV 398 (ONCE_REWRITE_CONV [algn_subtyping_cases])) THEN 399 SRW_TAC [][]THENL [ 400 (* Top case *) 401 Q.EXISTS_TAC `0` THEN SRW_TAC [][algn_subtyping_rules], 402 403 (* tyvar refl case *) 404 Q.EXISTS_TAC `0` THEN SRW_TAC [][algn_subtyping_rules], 405 406 (* tyvar trans case *) 407 Cases_on `x = x'` THENL [ 408 `u = q` 409 by (`MEM (x,q) xqctxt` by SRW_TAC [][Abbr`xqctxt`] THEN 410 METIS_TAC [wfctxt_assoc_unique]) THEN 411 REPEAT VAR_EQ_TAC THEN 412 `n' < n' + 1` by DECIDE_TAC THEN 413 `?k. algn_subtyping k xpctxt q n` by METIS_TAC [] THEN 414 `MEM (x,p) xpctxt` by SRW_TAC [][Abbr`xpctxt`] THEN 415 Q_TAC SUFF_TAC 416 `?k1. algn_subtyping k1 xpctxt p n` 417 THEN1 METIS_TAC [algn_subtyping_rules] THEN 418 Q_TAC SUFF_TAC 419 `?k2. algn_subtyping k2 xpctxt p q` 420 THEN1 METIS_TAC [] THEN 421 `xpctxt = (D ++ [(x,p)]) ++ G` 422 by ASM_SIMP_TAC bool_ss [GSYM listTheory.APPEND_ASSOC, Abbr`xpctxt`, 423 listTheory.APPEND] THEN 424 METIS_TAC [algn_subtyping_weakening], 425 426 `MEM (x',u) xpctxt` 427 by FULL_SIMP_TAC (srw_ss()) [Abbr`xpctxt`, Abbr`xqctxt`] THEN 428 METIS_TAC [algn_subtyping_rules, DECIDE ``n' < n' + 1``] 429 ], 430 431 (* Fun case *) 432 `n' < MAX n' m' + 1 /\ m' < MAX n' m' + 1` 433 by SRW_TAC [numSimps.ARITH_ss][arithmeticTheory.MAX_DEF] THEN 434 METIS_TAC [algn_subtyping_rules], 435 436 (* Forall case *) 437 `n' < MAX m' n' + 1 /\ m' < MAX m' n' + 1` 438 by SRW_TAC [numSimps.ARITH_ss][arithmeticTheory.MAX_DEF] THEN 439 `?k1. algn_subtyping k1 xpctxt t1 s1` by METIS_TAC [] THEN 440 `((x',t1) :: xqctxt = ((x',t1)::D) ++ ((x,q)::G)) /\ 441 ((x',t1) :: xpctxt = ((x',t1)::D) ++ ((x,p)::G))` 442 by SRW_TAC [][Abbr`xqctxt`, Abbr`xpctxt`] THEN 443 `?k2. algn_subtyping k2 ((x',t1)::xpctxt) s2 t2` 444 by METIS_TAC [] THEN 445 METIS_TAC [algn_subtyping_rules] 446 ]); 447 448val _ = remove_rules_for_term "dSUB" 449 450val _ = add_rule {block_style = (AroundEachPhrase, (PP.INCONSISTENT, 2)), 451 fixity = Infix(NONASSOC, 425), 452 paren_style = OnlyIfNecessary, 453 pp_elements = [HardSpace 1, TOK "|->", BreakSpace(1, 0), 454 BeginFinalBlock(PP.INCONSISTENT, 2), 455 TM, HardSpace 1, TOK "<:", BreakSpace(1,0)], 456 term_name = "alg_subtyping"} 457 458val alg_subtyping_def = Define` 459 G |-> ty1 <: ty2 = ?n. algn_subtyping n G ty1 ty2 460`; 461 462fun derive_rule th0 = let 463 val (vs, base) = strip_forall (concl th0) 464 val th = UNDISCH_ALL (SPEC_ALL th0) 465 val (f, args) = strip_comb (concl th) 466 val n = mk_var("n", numSyntax.num) 467 val pattern = mk_exists(n, list_mk_comb(f, n::tl args)) 468 val witness = hd args 469 val ex_thm = EXISTS (pattern, witness) th 470 val discharged = 471 GENL vs (DISCH_ALL (REWRITE_RULE [GSYM alg_subtyping_def] ex_thm)) 472 val exs_in = SIMP_RULE bool_ss [LEFT_FORALL_IMP_THM, 473 LEFT_EXISTS_AND_THM, 474 RIGHT_EXISTS_AND_THM] discharged 475in 476 REWRITE_RULE [GSYM alg_subtyping_def] exs_in 477end 478 479val alg_subtyping_rules = save_thm( 480 "alg_subtyping_rules", 481 LIST_CONJ (map derive_rule (CONJUNCTS algn_subtyping_rules))); 482 483val alg_subtyping_ind = save_thm( 484 "alg_subtyping_ind", 485 (Q.GEN `P` o 486 SIMP_RULE (srw_ss()) [GSYM alg_subtyping_def] o 487 CONV_RULE (RAND_CONV 488 (SWAP_VARS_CONV THENC 489 BINDER_CONV (SWAP_VARS_CONV THENC 490 BINDER_CONV (SWAP_VARS_CONV THENC 491 BINDER_CONV FORALL_IMP_CONV)))) o 492 SIMP_RULE (srw_ss()) [] o 493 Q.SPEC `\n G ty1 ty2. P G ty1 ty2`) algn_subtyping_ind); 494 495val alg_subtyping_cases = save_thm( 496 "alg_subtyping_cases", 497 (REWRITE_CONV [alg_subtyping_def] THENC 498 ONCE_REWRITE_CONV [algn_subtyping_cases] THENC 499 SIMP_CONV (srw_ss()) [EXISTS_OR_THM] THENC 500 SIMP_CONV (srw_ss()) 501 (map (INST_TYPE [alpha |-> numSyntax.num]) 502 [LEFT_EXISTS_AND_THM, RIGHT_EXISTS_AND_THM]) THENC 503 REWRITE_CONV [GSYM alg_subtyping_def]) 504 ``Gamma |-> ty1 <: ty2``); 505 506val alg_subtyping_swap1_eqn = store_thm( 507 "alg_subtyping_swap1_eqn", 508 ``G |-> fswap x y ty1 <: ty2 = ctxtswap x y G |-> ty1 <: fswap x y ty2``, 509 METIS_TAC [alg_subtyping_def, algn_subtyping_swap1_eqn]); 510 511val alg_subtyping_refl = store_thm( 512 "alg_subtyping_refl", 513 ``!ty G. wfctxt G /\ ftyFV ty SUBSET cdom G ==> G |-> ty <: ty``, 514 HO_MATCH_MP_TAC fsubty_ind THEN 515 SRW_TAC [][alg_subtyping_rules] THEN 516 Q_TAC (NEW_TAC "z") `cdom G UNION ftyFV ty UNION ftyFV ty'` THEN 517 `ForallTy v ty ty' = ForallTy z ty (fswap z v ty')` 518 by SRW_TAC [][ForallTy_11] THEN 519 SRW_TAC [][] THEN 520 MATCH_MP_TAC (last (CONJUNCTS alg_subtyping_rules)) THEN 521 SRW_TAC [][alg_subtyping_swap1_eqn] THEN 522 FIRST_X_ASSUM MATCH_MP_TAC THEN SRW_TAC [][] THEN 523 FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN 524 METIS_TAC [swapTheory.swapstr_def]); 525 526val alg_subtyping_trans = store_thm( 527 "alg_subtyping_trans", 528 ``G |-> ty1 <: ty2 /\ G |-> ty2 <: ty3 ==> G |-> ty1 <: ty3``, 529 METIS_TAC [alg_subtyping_def, lemma28_4_2_0]); 530 531val alg_soundcomplete = store_thm( 532 "alg_soundcomplete", 533 ``G |- ty1 <: ty2 = G |-> ty1 <: ty2``, 534 EQ_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`ty2`, `ty1`, `G`] THENL [ 535 HO_MATCH_MP_TAC fsubtyping_ind THEN 536 SRW_TAC [][alg_subtyping_rules] THENL [ 537 METIS_TAC [alg_subtyping_refl], 538 METIS_TAC [alg_subtyping_trans], 539 METIS_TAC [wfctxt_MEM, SUBSET_DEF, alg_subtyping_refl, 540 alg_subtyping_rules] 541 ], 542 HO_MATCH_MP_TAC alg_subtyping_ind THEN 543 SRW_TAC [][fsubtyping_rules] THEN 544 METIS_TAC [fsubtyping_rules, fsubtyping_wfctxt] 545 ]); 546 547val _ = export_theory() 548 549