1open HolKernel boolLib bossLib Parse 2 3open termTheory sttTheory contextlistsTheory NEWLib nomsetTheory 4 5val _ = new_theory "sttVariants" 6 7(* prove a cofinite version of the induction principle *) 8val hastype_cofin_ind = store_thm( 9 "hastype_cofin_ind", 10 ``!P. 11 (!G s A. valid_ctxt G /\ MEM (s,A) G ==> P G (VAR s) A) /\ 12 (!G m n A B. 13 P G m (A --> B) /\ P G n A ==> 14 P G (m @@ n) B) /\ 15 (!G v m A B X. 16 FINITE X /\ 17 (!y. ~(y IN X) ==> P ((y,A)::G) ([VAR y/v]m) B) ==> 18 P G (LAM v m) (A --> B)) ==> 19 !G m A. G |- m -: A ==> P G m A``, 20 GEN_TAC THEN STRIP_TAC THEN 21 Q_TAC SUFF_TAC `!G m A. G |- m -: A ==> !pi. P (ctxtswap pi G) (tpm pi m) A` 22 THEN1 METIS_TAC [pmact_nil] THEN 23 HO_MATCH_MP_TAC hastype_strongind THEN 24 SRW_TAC [][] THEN1 METIS_TAC [] THEN 25 Q_TAC (NEW_TAC "z") `FV (tpm pi m) UNION ctxtFV (ctxtswap pi G) UNION 26 {x;lswapstr pi x} UNION FV m UNION ctxtFV G` THEN 27 `LAM (lswapstr pi x) (tpm pi m) = LAM z (tpm [(z,lswapstr pi x)] (tpm pi m))` 28 by SRW_TAC [][tpm_ALPHA] THEN 29 SRW_TAC [][] THEN 30 FIRST_X_ASSUM MATCH_MP_TAC THEN 31 Q.EXISTS_TAC `ctxtFV (ctxtswap pi G) UNION FV (tpm pi m) UNION 32 {x; z; lswapstr pi x} UNION FV m UNION ctxtFV G` THEN 33 SRW_TAC [][] THEN 34 FIRST_X_ASSUM (Q.SPEC_THEN `(y, lswapstr pi x) :: pi` MP_TAC) THEN 35 ASM_SIMP_TAC (srw_ss()) [] THEN 36 `~(x IN ctxtFV G)` 37 by (`valid_ctxt ((x,A)::G)` by METIS_TAC [hastype_valid_ctxt] THEN 38 FULL_SIMP_TAC (srw_ss()) []) THEN 39 `ctxtswap ((y,lswapstr pi x)::pi) G = 40 ctxtswap [(y,lswapstr pi x)] (ctxtswap pi G)` 41 by SRW_TAC [][GSYM pmact_decompose] THEN 42 `_ = ctxtswap pi G` by SRW_TAC [][ctxtswap_fresh] THEN 43 `[VAR y/z] (tpm [(z,lswapstr pi x)] (tpm pi m)) = 44 tpm [(y,z)] (tpm [(z,lswapstr pi x)] (tpm pi m))` 45 by SRW_TAC [][fresh_tpm_subst] THEN 46 `_ = tpm [(lswapstr [(y,z)] z, lswapstr [(y,z)] (lswapstr pi x))] 47 (tpm [(y,z)] (tpm pi m))` 48 by SRW_TAC [][Once (GSYM pmact_sing_to_back)] THEN 49 `_ = tpm [(y,lswapstr pi x)] (tpm pi m)` 50 by SRW_TAC [][tpm_fresh, nomsetTheory.supp_apart] THEN 51 SRW_TAC [][GSYM pmact_decompose]); 52 53(* and a "cofinite" introduction rule for the abstraction case *) 54val cofin_hastype_abs_I = store_thm( 55 "cofin_hastype_abs_I", 56 ``!X v M A B G. 57 FINITE X /\ 58 (!u. ~(u IN X) ==> (u,A)::G |- [VAR u/v]M -: B) 59 ==> 60 G |- LAM v M -: (A --> B)``, 61 REPEAT STRIP_TAC THEN 62 Q_TAC (NEW_TAC "z") `X UNION FV M` THEN 63 `LAM v M = LAM z ([VAR z/v] M)` by SRW_TAC [][SIMPLE_ALPHA] THEN 64 SRW_TAC [][hastype_rules]); 65 66(* this then allows a nice, renaming free proof of weakening *) 67val weakening_cofin = prove( 68 ``!G m A. G |- m -: A ==> !D. G ��� D /\ valid_ctxt D ==> D |- m -: A``, 69 HO_MATCH_MP_TAC hastype_cofin_ind THEN 70 SRW_TAC [][] THENL [ 71 METIS_TAC [hastype_rules, subctxt_def], 72 METIS_TAC [hastype_rules], 73 MATCH_MP_TAC cofin_hastype_abs_I THEN 74 Q.EXISTS_TAC `X UNION ctxtFV D` THEN SRW_TAC [][] THEN 75 `valid_ctxt ((u,A)::D)` by FULL_SIMP_TAC (srw_ss()) [] THEN 76 `((u,A)::G) ��� ((u,A)::D)` 77 by FULL_SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss) [subctxt_def] THEN 78 SRW_TAC [][] 79 ]); 80 81 82(* ---------------------------------------------------------------------- 83 A more involved way of doing a similar "universal in the hypothesis" 84 thing. 85 ---------------------------------------------------------------------- *) 86 87(* now a slightly different typing relation, with different syntax: "||-" 88 instead of "|-". Underlying name of constant is "hastype2". *) 89val _ = add_rule {block_style = (AroundEachPhrase, (PP.INCONSISTENT, 2)), 90 fixity = Infix(NONASSOC, 425), 91 paren_style = OnlyIfNecessary, 92 pp_elements = [HardSpace 1, TOK "||-", BreakSpace(1, 0), 93 BeginFinalBlock(PP.INCONSISTENT, 2), 94 TM, HardSpace 1, TOK "-:", BreakSpace(1,0)], 95 term_name = "hastype2"} 96 97val (hastype2_rules, hastype2_ind, hastype2_cases) = Hol_reln` 98 (!Gamma s A. valid_ctxt Gamma /\ MEM (s,A) Gamma ==> 99 Gamma ||- VAR s -: A) /\ 100 (!Gamma m n A B. Gamma ||- m -: A --> B /\ Gamma ||- n -: A ==> 101 Gamma ||- m @@ n -: B) /\ 102 (!Gamma m x A B. (!v. ~(v IN ctxtFV Gamma) ==> 103 (v,A) :: Gamma ||- [VAR v/x]m -: B) ��� 104 ~(x ��� ctxtFV Gamma) ==> 105 Gamma ||- LAM x m -: A --> B) 106`; 107 108val hastype2_swap = store_thm( 109 "hastype2_swap", 110 ``!G m A. G ||- m -: A ==> !pi. ctxtswap pi G ||- tpm pi m -: A``, 111 HO_MATCH_MP_TAC hastype2_ind THEN SRW_TAC [][] THENL [ 112 METIS_TAC [hastype2_rules, MEM_ctxtswap, valid_ctxt_swap], 113 METIS_TAC [hastype2_rules], 114 MATCH_MP_TAC (last (CONJUNCTS hastype2_rules)) THEN 115 SRW_TAC [][tpm_subst_out] THEN 116 METIS_TAC [pmact_inverse] 117 ]); 118 119val hastype2_bvc_ind = store_thm( 120 "hastype2_bvc_ind", 121 ``!P fv. 122 (!x. FINITE (fv x)) /\ 123 (!G s A x. 124 valid_ctxt G /\ MEM (s,A) G ==> P G (VAR s) A x) 125 /\ 126 (!G m n A B x. 127 (!y. P G m (A --> B) y) /\ 128 (!y. P G n A y) ==> 129 P G (m @@ n) B x) /\ 130 131 (!G m u A B x. 132 (!v y. ~(v IN ctxtFV G) ==> P ((v,A)::G) ([VAR v/u] m) B y) /\ 133 ~(u IN ctxtFV G) /\ ~(u IN fv x) 134 ==> 135 P G (LAM u m) (A --> B) x) 136 ==> 137 !G m ty. G ||- m -: ty ==> !x. P G m ty x``, 138 REPEAT GEN_TAC THEN STRIP_TAC THEN 139 Q_TAC SUFF_TAC `!G m ty. G ||- m -: ty ==> 140 !pi x. P (ctxtswap pi G) (tpm pi m) ty x` 141 THEN1 METIS_TAC [pmact_nil] THEN 142 HO_MATCH_MP_TAC hastype2_ind THEN 143 SRW_TAC [][] THEN1 METIS_TAC [] THEN 144 Q.MATCH_ABBREV_TAC `P GG (LAM vv MM) (A --> B) xx` THEN 145 Q_TAC (NEW_TAC "z") `{vv} UNION FV MM UNION ctxtFV GG UNION fv xx` THEN 146 `LAM vv MM = LAM z (tpm [(z,vv)] MM)` 147 by SRW_TAC [][tpm_ALPHA] THEN 148 SRW_TAC [][] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN 149 SRW_TAC [][] THEN 150 FULL_SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss) [tpm_subst] THEN 151 FIRST_X_ASSUM (Q.SPECL_THEN [`lswapstr (REVERSE ((z,vv)::pi)) v`, 152 `(z,vv)::pi`, `y`] 153 MP_TAC) THEN 154 ASM_SIMP_TAC (srw_ss()) [pmact_decompose] THEN 155 `~(vv IN ctxtFV GG)` by SRW_TAC [][Abbr`vv`, Abbr`GG`] THEN 156 `ctxtswap ((z,vv)::pi) G = ctxtswap [(z,vv)] GG` 157 by SRW_TAC [][Abbr`GG`, GSYM pmact_decompose] THEN 158 ` _ = GG` by SRW_TAC [][ctxtswap_fresh] THEN 159 `tpm ((z,vv)::pi) m = tpm [(z,vv)] MM` 160 by SRW_TAC [][Abbr`MM`, GSYM pmact_decompose] THEN 161 SRW_TAC [][] THEN 162 FIRST_X_ASSUM MATCH_MP_TAC THEN 163 FULL_SIMP_TAC (srw_ss()) [pmact_decompose]); 164 165val hastype2_bvc_ind0 = save_thm( 166 "hastype2_bvc_ind0", 167 (Q.GEN `P` o Q.GEN `X` o 168 SIMP_RULE bool_ss [] o 169 Q.SPECL [`\G m ty x. P G m ty`, `\x. X`]) hastype2_bvc_ind) 170 171val hastype2_valid_ctxt = store_thm( 172 "hastype2_valid_ctxt", 173 ``!G m A. G ||- m -: A ==> valid_ctxt G``, 174 HO_MATCH_MP_TAC hastype2_ind THEN SRW_TAC [][] THEN METIS_TAC []); 175 176val hastype2_swap_eqn = store_thm( 177 "hastype2_swap_eqn", 178 ``G ||- tpm pi m -: A <=> ctxtswap (REVERSE pi) G ||- m -: A``, 179 METIS_TAC [hastype2_swap, pmact_inverse]); 180 181val hastype2_hastype = prove( 182 ``!G m A. G ||- m -: A ==> G |- m -: A``, 183 HO_MATCH_MP_TAC hastype2_ind THEN REPEAT CONJ_TAC THENL [ 184 (* var case *) SRW_TAC [][hastype_rules], 185 (* app case *) METIS_TAC [hastype_rules], 186 (* abs case *) METIS_TAC [hastype_rules, lemma14a] 187 ]); 188 189val hastype_hastype2 = prove( 190 ``!G m A. G |- m -: A ==> G ||- m -: A``, 191 HO_MATCH_MP_TAC hastype_indX THEN Q.EXISTS_TAC `{}` THEN 192 SRW_TAC [][hastype2_rules] THENL [ 193 (* app case *) METIS_TAC [hastype2_rules], 194 (* abs case; goal with IH is: *) 195 MATCH_MP_TAC (last (CONJUNCTS hastype2_rules)) THEN 196 SRW_TAC [][] THEN 197 Cases_on `v = v'` THEN1 SRW_TAC [][lemma14a] THEN 198 (* if v' = v, proof is trivial; rest of tactic is for other case *) 199 `v' ��� ctxtFV ((v,A)::G)` by SRW_TAC [][] THEN 200 `~(v' IN FV m)` by METIS_TAC [hastype_FV] THEN 201 `[VAR v'/v] m = tpm [(v',v)] m` by SRW_TAC [][fresh_tpm_subst] THEN 202 SRW_TAC [][hastype2_swap_eqn, ctxtswap_fresh] 203 ]); 204 205val hastype_hastype2_eqn = store_thm( 206 "hastype_hastype2_eqn", 207 ``G |- m -: A <=> G ||- m -: A``, 208 METIS_TAC [hastype2_hastype, hastype_hastype2]); 209 210val _ = export_theory () 211