1(* Fun and games with the "locally nameless" approach to language meta-theory 2 as done in the POPL paper "Engineering Formal Metatheory" by Brian 3 Aydemir, Arthur Chargu��raud, Benjamin Pierce, Randy Pollack and Stephanie 4 Weirich. 5 6 Contribution below is to show that it's as easy to prove the 7 cofinite introduction rule and the cofinite induction principle of 8 the original relations directly, rather than bothering to define a 9 whole new cofinite relation and to then show that this is 10 equivalent to the original. 11*) 12 13open HolKernel boolLib bossLib Parse 14 15open binderLib 16 17open nomsetTheory pred_setTheory 18 19fun Store_thm (p as (n,t,tac)) = store_thm p before export_rewrites [n] 20 21val _ = new_theory "lnameless" 22 23val _ = Datatype`lnt = var string | bnd num | app lnt lnt | abs lnt`; 24 25val open_def = Define` 26 (open k u (bnd i) = if i = k then u else bnd i) /\ 27 (open k u (var s) = var s) /\ 28 (open k u (app t1 t2) = app (open k u t1) (open k u t2)) /\ 29 (open k u (abs t) = abs (open (k + 1) u t)) 30`; 31val _ = export_rewrites ["open_def"] 32 33val raw_lnpm_def = Define` 34 (raw_lnpm pi (var s) = var (lswapstr pi s)) /\ 35 (raw_lnpm pi (bnd i) = bnd i) /\ 36 (raw_lnpm pi (app t1 t2) = app (raw_lnpm pi t1) (raw_lnpm pi t2)) /\ 37 (raw_lnpm pi (abs t) = abs (raw_lnpm pi t)) 38`; 39val _ = export_rewrites ["raw_lnpm_def"] 40 41val _ = overload_on("ln_pmact",``mk_pmact raw_lnpm``); 42val _ = overload_on("lnpm",``pmact ln_pmact``); 43 44val lnpm_raw = store_thm( 45 "lnpm_raw", 46 ``lnpm = raw_lnpm``, 47 SRW_TAC [][GSYM pmact_bijections] THEN 48 SRW_TAC [][is_pmact_def, permeq_thm, FUN_EQ_THM] THENL [ 49 Induct_on `x` THEN SRW_TAC [][], 50 Induct_on `x` THEN SRW_TAC [][pmact_decompose], 51 Induct_on `x` THEN SRW_TAC [][] 52 ]); 53 54val lnpm_thm = save_thm( 55"lnpm_thm", 56raw_lnpm_def |> SUBS [GSYM lnpm_raw]); 57val _ = export_rewrites["lnpm_thm"]; 58 59val lnpm_open = prove( 60 ``!i. lnpm pi (open i t1 t2) = open i (lnpm pi t1) (lnpm pi t2)``, 61 Induct_on `t2` THEN SRW_TAC [][]); 62 63val fv_def = Define` 64 (fv (var s) = {s}) /\ 65 (fv (bnd i) = {}) /\ 66 (fv (app t u) = fv t UNION fv u) /\ 67 (fv (abs t) = fv t) 68`; 69val _ = export_rewrites ["fv_def"] 70 71val fv_lnpm = prove( 72 ``!t. fv (lnpm pi t) = ssetpm pi (fv t)``, 73 Induct THEN SRW_TAC [][pmact_INSERT, pmact_UNION]); 74 75val FINITE_fv = Store_thm( 76 "FINITE_fv", 77 ``!t. FINITE (fv t)``, 78 Induct THEN SRW_TAC [][]); 79 80val lnpm_fresh = store_thm( 81 "lnpm_fresh", 82 ``~(a IN fv t) /\ ~(b IN fv t) ==> (lnpm [(a,b)] t = t)``, 83 Induct_on `t` THEN SRW_TAC [][]); 84 85val (lclosed_rules, lclosed_ind, lclosed_cases) = Hol_reln` 86 (!s. lclosed (var s)) /\ 87 (!t1 t2. lclosed t1 /\ lclosed t2 ==> lclosed (app t1 t2)) /\ 88 (!s t. ~(s IN fv t) /\ lclosed (open 0 (var s) t) ==> 89 lclosed (abs t)) 90`; 91 92val lclosed_eqvt = prove( 93 ``!t. lclosed t ==> !pi. lclosed (lnpm pi t)``, 94 HO_MATCH_MP_TAC lclosed_ind THEN SRW_TAC [][lclosed_rules, lnpm_open] THEN 95 MATCH_MP_TAC (last (CONJUNCTS lclosed_rules)) THEN 96 Q.EXISTS_TAC `lswapstr pi s` THEN 97 SRW_TAC [][fv_lnpm]); 98 99val lclosed_gen_bvc_ind = store_thm( 100 "lclosed_gen_bvc_ind", 101 ``!P f. (!c. FINITE (f c)) /\ 102 (!s c. P (var s) c) /\ 103 (!t1 t2 c. (!d. P t1 d) /\ (!d. P t2 d) ==> P (app t1 t2) c) /\ 104 (!s t c. ~(s IN f c) /\ ~(s IN fv t) /\ 105 (!d. P (open 0 (var s) t) d) ==> 106 P (abs t) c) ==> 107 !t. lclosed t ==> !c. P t c``, 108 REPEAT GEN_TAC THEN STRIP_TAC THEN 109 Q_TAC SUFF_TAC `!t. lclosed t ==> !pi c. P (lnpm pi t) c` 110 THEN1 METIS_TAC [pmact_nil] THEN 111 HO_MATCH_MP_TAC lclosed_ind THEN SRW_TAC [][lnpm_open] THEN 112 FIRST_X_ASSUM MATCH_MP_TAC THEN 113 Q_TAC (NEW_TAC "z") `fv (lnpm pi t) UNION f c` THEN 114 FIRST_X_ASSUM (Q.SPEC_THEN `(stringpm pi s, z) :: pi` MP_TAC) THEN 115 ASM_SIMP_TAC (srw_ss()) [] THEN 116 `lnpm [(stringpm pi s, z)] (lnpm pi t) = lnpm pi t` 117 by SRW_TAC [][lnpm_fresh, fv_lnpm] THEN 118 FULL_SIMP_TAC (srw_ss()) [GSYM pmact_decompose] THEN 119 STRIP_TAC THEN Q.EXISTS_TAC `z` THEN SRW_TAC [][]); 120 121val all_fnone = prove( 122 ``(!(f:one -> 'a). P f) = !x:'a. P (K x)``, 123 SRW_TAC [][EQ_IMP_THM] THEN 124 Q_TAC SUFF_TAC `f = K (f())` 125 THEN1 (DISCH_THEN SUBST1_TAC THEN SRW_TAC [][]) THEN 126 SRW_TAC [][FUN_EQ_THM, oneTheory.one]); 127 128val lclosed_bvc_ind = save_thm( 129 "lclosed_bvc_ind", 130 (Q.GEN `P` o Q.GEN `X` o 131 SIMP_RULE bool_ss [] o 132 SPECL [``(\M:lnt x:one. P M:bool)``, 133 ``X:string -> bool``] o 134 SIMP_RULE (srw_ss()) [all_fnone, oneTheory.one] o 135 INST_TYPE [alpha |-> ``:one``] o 136 GEN_ALL) lclosed_gen_bvc_ind); 137 138val lclosed_cofin_ind = store_thm( 139 "lclosed_cofin_ind", 140 ``!P. (!s. P (var s)) /\ 141 (!t1 t2. P t1 /\ P t2 ==> P (app t1 t2)) /\ 142 (!t X. FINITE X /\ 143 (!s. ~(s IN X) ==> P (open 0 (var s) t)) ==> 144 P (abs t)) ==> 145 !t. lclosed t ==> P t``, 146 GEN_TAC THEN STRIP_TAC THEN 147 Q_TAC SUFF_TAC `!t. lclosed t ==> !pi. P (lnpm pi t)` 148 THEN1 METIS_TAC [pmact_nil] THEN 149 HO_MATCH_MP_TAC lclosed_bvc_ind THEN SRW_TAC [][lnpm_open] THEN 150 Q.EXISTS_TAC `{}` THEN SRW_TAC [][] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN 151 Q.EXISTS_TAC `fv (lnpm pi t)` THEN SRW_TAC [][] THEN 152 `lnpm [(s',stringpm pi s)] (lnpm pi t) = lnpm pi t` 153 by SRW_TAC [][lnpm_fresh, fv_lnpm] THEN 154 FIRST_X_ASSUM (Q.SPEC_THEN `[(s',stringpm pi s)] ++ pi` MP_TAC) THEN 155 SRW_TAC [][pmact_decompose]); 156 157val abs_lclosed_I = store_thm( 158 "abs_lclosed_I", 159 ``FINITE X /\ (!s. ~(s IN X) ==> lclosed (open 0 (var s) t)) ==> 160 lclosed (abs t)``, 161 STRIP_TAC THEN MATCH_MP_TAC (last (CONJUNCTS lclosed_rules)) THEN 162 Q_TAC (NEW_TAC "z") `fv t UNION X` THEN Q.EXISTS_TAC `z` THEN 163 SRW_TAC [][]); 164 165val strong_lclosed_cofin_ind = store_thm( 166 "strong_lclosed_cofin_ind", 167 ``!P. (!s. P (var s)) /\ 168 (!t1 t2. P t1 /\ P t2 /\ lclosed t1 /\ lclosed t2 ==> 169 P (app t1 t2)) /\ 170 (!t X. FINITE X /\ 171 (!s. ~(s IN X) ==> P (open 0 (var s) t) /\ 172 lclosed (open 0 (var s) t)) ==> 173 P (abs t)) 174 ==> 175 !t. lclosed t ==> P t``, 176 GEN_TAC THEN STRIP_TAC THEN 177 Q_TAC SUFF_TAC `!t. lclosed t ==> P t /\ lclosed t` THEN1 SRW_TAC [][] THEN 178 HO_MATCH_MP_TAC lclosed_cofin_ind THEN 179 METIS_TAC [abs_lclosed_I, lclosed_rules]); 180 181val lclosed_E = store_thm( 182 "lclosed_E", 183 ``!t. 184 lclosed t ==> 185 (?s. (t = var s)) \/ 186 (?t1 t2. (t = app t1 t2) /\ lclosed t1 /\ lclosed t2) \/ 187 (?X u. (t = abs u) /\ FINITE X /\ 188 !s. ~(s IN X) ==> lclosed (open 0 (var s) u))``, 189 HO_MATCH_MP_TAC strong_lclosed_cofin_ind THEN 190 SIMP_TAC (srw_ss()) [] THEN REPEAT STRIP_TAC THEN 191 METIS_TAC [lclosed_rules, abs_lclosed_I]); 192 193val lclosed_abs_cofin = store_thm( 194 "lclosed_abs_cofin", 195 ``lclosed (abs t) = ?X. FINITE X /\ 196 !s. ~(s IN X) ==> lclosed (open 0 (var s) t)``, 197 EQ_TAC THEN STRIP_TAC THENL [ 198 IMP_RES_TAC lclosed_E THEN 199 FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC [], 200 METIS_TAC [abs_lclosed_I] 201 ]); 202 203val _ = Datatype `ltype = tyOne | tyFun ltype ltype`; 204 205val _ = set_fixity "-->" (Infixr 700) 206val _ = overload_on ("-->", ``tyFun``); 207 208val valid_ctxt_def = Define` 209 (valid_ctxt [] = T) /\ 210 (valid_ctxt ((x,A) :: G) = (!A'. ~MEM (x, A') G) /\ valid_ctxt G) 211`; 212val _ = export_rewrites ["valid_ctxt_def"] 213 214(* permutation over contexts swaps the strings and leaves the types alone *) 215val ctxtswap_def = Define` 216 (ctxtswap pi [] = []) /\ 217 (ctxtswap pi (sA :: G) = (lswapstr pi (FST sA), SND sA) :: ctxtswap pi G) 218`; 219val _ = export_rewrites ["ctxtswap_def"] 220 221val ctxtswap_NIL = store_thm( 222 "ctxtswap_NIL", 223 ``ctxtswap [] G = G``, 224 Induct_on `G` THEN SRW_TAC [][]); 225val _ = export_rewrites ["ctxtswap_NIL"] 226 227val ctxtswap_inverse = store_thm( 228 "ctxtswap_inverse", 229 ``(ctxtswap pi (ctxtswap (REVERSE pi) G) = G) /\ 230 (ctxtswap (REVERSE pi) (ctxtswap pi G) = G)``, 231 Induct_on `G` THEN SRW_TAC [][]); 232val _ = export_rewrites ["ctxtswap_inverse"] 233 234val ctxtswap_sing_inv = store_thm( 235 "ctxtswap_sing_inv", 236 ``ctxtswap [(x,y)] (ctxtswap [(x,y)] G) = G``, 237 METIS_TAC [listTheory.APPEND, listTheory.REVERSE_DEF, ctxtswap_inverse]); 238val _ = export_rewrites ["ctxtswap_sing_inv"] 239 240val ctxtswap_APPEND = store_thm( 241 "ctxtswap_APPEND", 242 ``!p1 p2. ctxtswap (p1 ++ p2) G = ctxtswap p1 (ctxtswap p2 G)``, 243 Induct_on `G` THEN SRW_TAC [][pmact_decompose]); 244 245(* context membership "respects" permutation *) 246val MEM_ctxtswap = store_thm( 247 "MEM_ctxtswap", 248 ``!G pi x A. MEM (lswapstr pi x, A) (ctxtswap pi G) = MEM (x,A) G``, 249 Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD]); 250val _ = export_rewrites ["MEM_ctxtswap"] 251 252(* valid_ctxt also respects permutation *) 253val valid_ctxt_swap0 = prove( 254 ``!G. valid_ctxt G ==> !x y. valid_ctxt (ctxtswap pi G)``, 255 Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD]); 256val valid_ctxt_swap = store_thm( 257 "valid_ctxt_swap", 258 ``valid_ctxt (ctxtswap pi G) = valid_ctxt G``, 259 METIS_TAC [valid_ctxt_swap0, ctxtswap_inverse]); 260val _ = export_rewrites ["valid_ctxt_swap"] 261 262(* the free variables of a context, defined with primitive recursion to 263 give us nice rewrites *) 264val ctxtFV_def = Define` 265 (ctxtFV [] = {}) /\ 266 (ctxtFV (h::t) = FST h INSERT ctxtFV t) 267`; 268val _ = export_rewrites ["ctxtFV_def"] 269 270(* contexts have finitely many free variables *) 271val FINITE_ctxtFV = store_thm( 272 "FINITE_ctxtFV", 273 ``FINITE (ctxtFV G)``, 274 Induct_on `G` THEN SRW_TAC [][]); 275val _ = export_rewrites ["FINITE_ctxtFV"] 276 277val ctxtswap_fresh = store_thm( 278 "ctxtswap_fresh", 279 ``~(x IN ctxtFV G) /\ ~(y IN ctxtFV G) ==> (ctxtswap [(x,y)] G = G)``, 280 Induct_on `G` THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD]); 281 282val ctxtFV_ctxtswap = store_thm( 283 "ctxtFV_ctxtswap", 284 ``ctxtFV (ctxtswap pi G) = ssetpm pi (ctxtFV G)``, 285 Induct_on `G` THEN SRW_TAC [][pmact_INSERT, stringpm_raw]); 286val _ = export_rewrites ["ctxtFV_ctxtswap"] 287 288(* more direct characterisation of ctxtFV *) 289val ctxtFV_MEM = store_thm( 290 "ctxtFV_MEM", 291 ``x IN ctxtFV G = (?A. MEM (x,A) G)``, 292 Induct_on `G` THEN 293 ASM_SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss) [pairTheory.FORALL_PROD]); 294 295 296val valid_ctxt_CONS = prove( 297 ``!z ty. valid_ctxt ((z,ty) :: G) = ~(z IN ctxtFV G) /\ valid_ctxt G``, 298 Induct_on `G` THEN1 SRW_TAC [][] THEN 299 ASM_SIMP_TAC bool_ss [pairTheory.FORALL_PROD, Once valid_ctxt_def] THEN 300 SRW_TAC [][ctxtFV_MEM]); 301 302 303val (typing_rules, typing_ind, typing_cases) = Hol_reln` 304 (!G s ty. valid_ctxt G /\ MEM (s,ty) G ==> typing G (var s) ty) /\ 305 (!G t1 t2 ty1 ty2. 306 typing G t1 (ty1 --> ty2) /\ typing G t2 ty1 ==> 307 typing G (app t1 t2) ty2) /\ 308 (!G t s ty1 ty2. 309 typing ((s,ty1)::G) (open 0 (var s) t) ty2 /\ 310 ~(s IN fv t) 311 ==> 312 typing G (abs t) (ty1 --> ty2)) 313`; 314 315val typing_eqvt = store_thm( 316 "typing_eqvt", 317 ``!G t ty. typing G t ty ==> !pi. typing (ctxtswap pi G) (lnpm pi t) ty``, 318 HO_MATCH_MP_TAC typing_ind THEN SRW_TAC [][typing_rules, lnpm_open] THENL [ 319 METIS_TAC [typing_rules], 320 MATCH_MP_TAC (last (CONJUNCTS typing_rules)) THEN 321 Q.EXISTS_TAC `lswapstr pi s` THEN 322 SRW_TAC [][fv_lnpm] 323 ]); 324 325 326val typing_valid_ctxt = store_thm( 327 "typing_valid_ctxt", 328 ``!G t ty. typing G t ty ==> valid_ctxt G``, 329 HO_MATCH_MP_TAC typing_ind THEN SRW_TAC [][]); 330 331val typing_lclosed = store_thm( 332 "typing_lclosed", 333 ``!G t ty. typing G t ty ==> lclosed t``, 334 HO_MATCH_MP_TAC typing_ind THEN SRW_TAC [][lclosed_rules] THEN 335 METIS_TAC [lclosed_rules]); 336 337val typing_bvc_ind = store_thm( 338 "typing_bvc_ind", 339 ``!P X. FINITE X /\ 340 (!G s ty. valid_ctxt G /\ MEM (s,ty) G ==> P G (var s) ty) /\ 341 (!G t1 t2 ty1 ty2. 342 P G t1 (ty1 --> ty2) /\ P G t2 ty1 /\ 343 typing G t1 (ty1 --> ty2) /\ typing G t2 ty1 ==> 344 P G (app t1 t2) ty2) /\ 345 (!G s t ty1 ty2. 346 ~(s IN X) /\ ~(s IN fv t) /\ 347 P ((s,ty1)::G) (open 0 (var s) t) ty2 /\ 348 typing ((s,ty1)::G) (open 0 (var s) t) ty2 349 ==> 350 P G (abs t) (ty1 --> ty2)) 351 ==> 352 !G t ty. typing G t ty ==> P G t ty``, 353 REPEAT GEN_TAC THEN STRIP_TAC THEN 354 Q_TAC SUFF_TAC `!G t ty. typing G t ty ==> 355 !pi. typing (ctxtswap pi G) (lnpm pi t) ty /\ 356 P (ctxtswap pi G) (lnpm pi t) ty` 357 THEN1 METIS_TAC [pmact_nil, ctxtswap_NIL] THEN 358 HO_MATCH_MP_TAC typing_ind THEN SRW_TAC [][lnpm_open, typing_rules] THENL [ 359 METIS_TAC [typing_rules], 360 METIS_TAC [], 361 MATCH_MP_TAC (last (CONJUNCTS typing_rules)) THEN 362 Q.EXISTS_TAC `lswapstr pi s` THEN SRW_TAC [][fv_lnpm], 363 364 Q_TAC (NEW_TAC "z") `fv (lnpm pi t) UNION X UNION 365 ctxtFV (ctxtswap pi G) UNION 366 {lswapstr pi s}` THEN 367 FIRST_X_ASSUM MATCH_MP_TAC THEN Q.EXISTS_TAC `z` THEN 368 ASM_SIMP_TAC (srw_ss()) [] THEN 369 FIRST_X_ASSUM (Q.SPEC_THEN `(lswapstr pi s, z) :: pi` MP_TAC) THEN 370 ASM_SIMP_TAC (srw_ss()) [] THEN 371 STRIP_TAC THEN 372 `lnpm [(lswapstr pi s, z)] (lnpm pi t) = lnpm pi t` 373 by SRW_TAC [][lnpm_fresh, fv_lnpm] THEN 374 `~(s IN ctxtFV G)` 375 by (IMP_RES_TAC typing_valid_ctxt THEN 376 FULL_SIMP_TAC bool_ss [valid_ctxt_CONS] THEN 377 FULL_SIMP_TAC (srw_ss()) [ctxtFV_ctxtswap, pmact_decompose] THEN 378 FULL_SIMP_TAC (srw_ss()) []) THEN 379 `ctxtswap [(lswapstr pi s,z)] (ctxtswap pi G) = ctxtswap pi G` 380 by SRW_TAC [][ctxtswap_fresh] THEN 381 FULL_SIMP_TAC (srw_ss()) [GSYM pmact_decompose, 382 GSYM ctxtswap_APPEND] 383 ]); 384 385val strong_typing_ind = IndDefLib.derive_strong_induction(typing_rules, 386 typing_ind) 387 388val typing_cofin_ind = store_thm( 389 "typing_cofin_ind", 390 ``!P. (!G s ty. valid_ctxt G /\ MEM (s,ty) G ==> P G (var s) ty) /\ 391 (!G t1 t2 ty1 ty2. 392 P G t1 (ty1 --> ty2) /\ P G t2 ty1 ==> 393 P G (app t1 t2) ty2) /\ 394 (!G X t ty1 ty2. 395 FINITE X /\ 396 (!s. ~(s IN X) ==> P ((s,ty1)::G) (open 0 (var s) t) ty2) ==> 397 P G (abs t) (ty1 --> ty2)) 398 ==> 399 !G t ty. typing G t ty ==> P G t ty``, 400 GEN_TAC THEN STRIP_TAC THEN 401 Q_TAC SUFF_TAC `!G t ty. typing G t ty ==> 402 !pi. P (ctxtswap pi G) (lnpm pi t) ty` 403 THEN1 METIS_TAC [pmact_nil, ctxtswap_NIL] THEN 404 HO_MATCH_MP_TAC strong_typing_ind THEN 405 SRW_TAC [][lnpm_open] THEN1 METIS_TAC [] THEN 406 FIRST_X_ASSUM MATCH_MP_TAC THEN 407 Q.EXISTS_TAC `fv (lnpm pi t) UNION ctxtFV (ctxtswap pi G)` THEN 408 SRW_TAC [][] THEN 409 FIRST_X_ASSUM (Q.SPEC_THEN `[(s',lswapstr pi s)] ++ pi` MP_TAC) THEN 410 ASM_SIMP_TAC (srw_ss()) [] THEN 411 Q_TAC SUFF_TAC `(lnpm ((s', lswapstr pi s)::pi) t = lnpm pi t) /\ 412 (ctxtswap ((s',lswapstr pi s)::pi) G = ctxtswap pi G)` 413 THEN1 SRW_TAC [][] THEN 414 `lnpm [(s',lswapstr pi s)] (lnpm pi t) = lnpm pi t` 415 by SRW_TAC [][lnpm_fresh, fv_lnpm] THEN 416 FULL_SIMP_TAC (srw_ss()) [GSYM pmact_decompose] THEN 417 `~(s IN ctxtFV G)` 418 by (IMP_RES_TAC typing_valid_ctxt THEN 419 FULL_SIMP_TAC bool_ss [valid_ctxt_CONS]) THEN 420 `ctxtswap ((s',lswapstr pi s)::pi) G = 421 ctxtswap ([(s',lswapstr pi s)] ++ pi) G` 422 by SRW_TAC [][] THEN 423 ` _ = ctxtswap [(s',lswapstr pi s)] (ctxtswap pi G)` 424 by SRW_TAC [][ctxtswap_APPEND] THEN 425 ` _ = ctxtswap pi G` 426 by SRW_TAC [][ctxtswap_fresh] THEN 427 SRW_TAC [][]); 428 429(* The approach in "Engineering Formal Metatheory" is to define a separate 430 "cofinite" relation, to prove the desired properties of this relation, and 431 to finish up by showing that it and the original correspond. *) 432 433val (cotyping_rules, cotyping_ind, cotyping_cases) = Hol_reln` 434 (!G s ty. valid_ctxt G /\ MEM (s, ty) G ==> cotyping G (var s) ty) /\ 435 (!G t1 t2 ty1 ty2. 436 cotyping G t1 (ty1 --> ty2) /\ cotyping G t2 ty1 ==> 437 cotyping G (app t1 t2) ty2) /\ 438 (!G X t ty1 ty2. 439 FINITE X /\ 440 (!s. ~(s IN X) ==> cotyping ((s,ty1)::G) (open 0 (var s) t) ty2) ==> 441 cotyping G (abs t) (ty1 --> ty2)) 442`; 443 444val cotyping_typing = store_thm( 445 "cotyping_typing", 446 ``!G t ty. cotyping G t ty ==> typing G t ty``, 447 HO_MATCH_MP_TAC cotyping_ind THEN SRW_TAC [][typing_rules] 448 THEN1 METIS_TAC [typing_rules] THEN 449 MATCH_MP_TAC (last (CONJUNCTS typing_rules)) THEN 450 Q_TAC (NEW_TAC "z") `fv t UNION X` THEN METIS_TAC []); 451 452val typing_cotyping = store_thm( 453 "typing_cotyping", 454 ``!G t ty. typing G t ty ==> cotyping G t ty``, 455 HO_MATCH_MP_TAC typing_cofin_ind THEN SRW_TAC [][cotyping_rules] THEN 456 METIS_TAC [cotyping_rules]); 457 458val _ = export_theory(); 459