1215976Sjmallettopen HolKernel boolLib bossLib Parse 2232812Sjmallett 3215976Sjmallettopen termTheory sttTheory contextlistsTheory NEWLib nomsetTheory 4215976Sjmallett 5215976Sjmallettval _ = new_theory "sttVariants" 6215976Sjmallett 7215976Sjmallett(* prove a cofinite version of the induction principle *) 8215976Sjmallettval hastype_cofin_ind = store_thm( 9215976Sjmallett "hastype_cofin_ind", 10215976Sjmallett ``!P. 11215976Sjmallett (!G s A. valid_ctxt G /\ MEM (s,A) G ==> P G (VAR s) A) /\ 12215976Sjmallett (!G m n A B. 13215976Sjmallett P G m (A --> B) /\ P G n A ==> 14215976Sjmallett P G (m @@ n) B) /\ 15215976Sjmallett (!G v m A B X. 16215976Sjmallett FINITE X /\ 17215976Sjmallett (!y. ~(y IN X) ==> P ((y,A)::G) ([VAR y/v]m) B) ==> 18232812Sjmallett P G (LAM v m) (A --> B)) ==> 19215976Sjmallett !G m A. G |- m -: A ==> P G m A``, 20215976Sjmallett GEN_TAC THEN STRIP_TAC THEN 21215976Sjmallett Q_TAC SUFF_TAC `!G m A. G |- m -: A ==> !pi. P (ctxtswap pi G) (tpm pi m) A` 22215976Sjmallett THEN1 METIS_TAC [pmact_nil] THEN 23215976Sjmallett HO_MATCH_MP_TAC hastype_strongind THEN 24215976Sjmallett SRW_TAC [][] THEN1 METIS_TAC [] THEN 25215976Sjmallett Q_TAC (NEW_TAC "z") `FV (tpm pi m) UNION ctxtFV (ctxtswap pi G) UNION 26215976Sjmallett {x;lswapstr pi x} UNION FV m UNION ctxtFV G` THEN 27215976Sjmallett `LAM (lswapstr pi x) (tpm pi m) = LAM z (tpm [(z,lswapstr pi x)] (tpm pi m))` 28215976Sjmallett by SRW_TAC [][tpm_ALPHA] THEN 29232812Sjmallett SRW_TAC [][] THEN 30215976Sjmallett FIRST_X_ASSUM MATCH_MP_TAC THEN 31215976Sjmallett Q.EXISTS_TAC `ctxtFV (ctxtswap pi G) UNION FV (tpm pi m) UNION 32215976Sjmallett {x; z; lswapstr pi x} UNION FV m UNION ctxtFV G` THEN 33215976Sjmallett SRW_TAC [][] THEN 34215976Sjmallett FIRST_X_ASSUM (Q.SPEC_THEN `(y, lswapstr pi x) :: pi` MP_TAC) THEN 35215976Sjmallett ASM_SIMP_TAC (srw_ss()) [] THEN 36215976Sjmallett `~(x IN ctxtFV G)` 37215976Sjmallett by (`valid_ctxt ((x,A)::G)` by METIS_TAC [hastype_valid_ctxt] THEN 38215976Sjmallett FULL_SIMP_TAC (srw_ss()) []) THEN 39215976Sjmallett `ctxtswap ((y,lswapstr pi x)::pi) G = 40215976Sjmallett ctxtswap [(y,lswapstr pi x)] (ctxtswap pi G)` 41215976Sjmallett by SRW_TAC [][GSYM pmact_decompose] THEN 42215976Sjmallett `_ = ctxtswap pi G` by SRW_TAC [][ctxtswap_fresh] THEN 43215976Sjmallett `[VAR y/z] (tpm [(z,lswapstr pi x)] (tpm pi m)) = 44215976Sjmallett tpm [(y,z)] (tpm [(z,lswapstr pi x)] (tpm pi m))` 45215976Sjmallett by SRW_TAC [][fresh_tpm_subst] THEN 46215976Sjmallett `_ = tpm [(lswapstr [(y,z)] z, lswapstr [(y,z)] (lswapstr pi x))] 47215976Sjmallett (tpm [(y,z)] (tpm pi m))` 48215976Sjmallett by SRW_TAC [][Once (GSYM pmact_sing_to_back)] THEN 49215976Sjmallett `_ = tpm [(y,lswapstr pi x)] (tpm pi m)` 50215976Sjmallett by SRW_TAC [][tpm_fresh, nomsetTheory.supp_apart] THEN 51215976Sjmallett SRW_TAC [][GSYM pmact_decompose]); 52232812Sjmallett 53232812Sjmallett(* and a "cofinite" introduction rule for the abstraction case *) 54215976Sjmallettval cofin_hastype_abs_I = store_thm( 55215976Sjmallett "cofin_hastype_abs_I", 56215976Sjmallett ``!X v M A B G. 57215976Sjmallett FINITE X /\ 58215976Sjmallett (!u. ~(u IN X) ==> (u,A)::G |- [VAR u/v]M -: B) 59232812Sjmallett ==> 60215976Sjmallett G |- LAM v M -: (A --> B)``, 61215976Sjmallett REPEAT STRIP_TAC THEN 62215976Sjmallett Q_TAC (NEW_TAC "z") `X UNION FV M` THEN 63215976Sjmallett `LAM v M = LAM z ([VAR z/v] M)` by SRW_TAC [][SIMPLE_ALPHA] THEN 64215976Sjmallett SRW_TAC [][hastype_rules]); 65215976Sjmallett 66215976Sjmallett(* this then allows a nice, renaming free proof of weakening *) 67215976Sjmallettval weakening_cofin = prove( 68215976Sjmallett ``!G m A. G |- m -: A ==> !D. G ��� D /\ valid_ctxt D ==> D |- m -: A``, 69215976Sjmallett HO_MATCH_MP_TAC hastype_cofin_ind THEN 70215976Sjmallett SRW_TAC [][] THENL [ 71215976Sjmallett METIS_TAC [hastype_rules, subctxt_def], 72232812Sjmallett METIS_TAC [hastype_rules], 73232812Sjmallett MATCH_MP_TAC cofin_hastype_abs_I THEN 74232812Sjmallett Q.EXISTS_TAC `X UNION ctxtFV D` THEN SRW_TAC [][] THEN 75232812Sjmallett `valid_ctxt ((u,A)::D)` by FULL_SIMP_TAC (srw_ss()) [] THEN 76215976Sjmallett `((u,A)::G) ��� ((u,A)::D)` 77215976Sjmallett by FULL_SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss) [subctxt_def] THEN 78215976Sjmallett SRW_TAC [][] 79215976Sjmallett ]); 80215976Sjmallett 81215976Sjmallett 82215976Sjmallett(* ---------------------------------------------------------------------- 83215976Sjmallett A more involved way of doing a similar "universal in the hypothesis" 84215976Sjmallett thing. 85215976Sjmallett ---------------------------------------------------------------------- *) 86232812Sjmallett 87215976Sjmallett(* now a slightly different typing relation, with different syntax: "||-" 88215976Sjmallett instead of "|-". Underlying name of constant is "hastype2". *) 89215976Sjmallettval _ = add_rule {block_style = (AroundEachPhrase, (PP.INCONSISTENT, 2)), 90215976Sjmallett fixity = Infix(NONASSOC, 425), 91215976Sjmallett paren_style = OnlyIfNecessary, 92215976Sjmallett pp_elements = [HardSpace 1, TOK "||-", BreakSpace(1, 0), 93215976Sjmallett BeginFinalBlock(PP.INCONSISTENT, 2), 94215976Sjmallett TM, HardSpace 1, TOK "-:", BreakSpace(1,0)], 95215976Sjmallett term_name = "hastype2"} 96215976Sjmallett 97232812Sjmallettval (hastype2_rules, hastype2_ind, hastype2_cases) = Hol_reln` 98215976Sjmallett (!Gamma s A. valid_ctxt Gamma /\ MEM (s,A) Gamma ==> 99215976Sjmallett Gamma ||- VAR s -: A) /\ 100215976Sjmallett (!Gamma m n A B. Gamma ||- m -: A --> B /\ Gamma ||- n -: A ==> 101215976Sjmallett Gamma ||- m @@ n -: B) /\ 102215976Sjmallett (!Gamma m x A B. (!v. ~(v IN ctxtFV Gamma) ==> 103215976Sjmallett (v,A) :: Gamma ||- [VAR v/x]m -: B) ��� 104215976Sjmallett ~(x ��� ctxtFV Gamma) ==> 105215976Sjmallett Gamma ||- LAM x m -: A --> B) 106215976Sjmallett`; 107232812Sjmallett 108232812Sjmallettval hastype2_swap = store_thm( 109232812Sjmallett "hastype2_swap", 110232812Sjmallett ``!G m A. G ||- m -: A ==> !pi. ctxtswap pi G ||- tpm pi m -: A``, 111232812Sjmallett HO_MATCH_MP_TAC hastype2_ind THEN SRW_TAC [][] THENL [ 112232812Sjmallett METIS_TAC [hastype2_rules, MEM_ctxtswap, valid_ctxt_swap], 113232812Sjmallett METIS_TAC [hastype2_rules], 114232812Sjmallett MATCH_MP_TAC (last (CONJUNCTS hastype2_rules)) THEN 115232812Sjmallett SRW_TAC [][tpm_subst_out] THEN 116232812Sjmallett METIS_TAC [pmact_inverse] 117232812Sjmallett ]); 118215976Sjmallett 119232812SjmallettTheorem hastype2_bvc_ind: 120215976Sjmallett ���P fv. 121232812Sjmallett (���x. FINITE (fv x)) 122232812Sjmallett ��� 123215976Sjmallett (���G s A x. valid_ctxt G /\ MEM (s,A) G ==> P G (VAR s) A x) 124232812Sjmallett ��� 125232812Sjmallett (���G m n A B x. 126232812Sjmallett (���y. P G m (A --> B) y) ��� (���y. P G n A y) ��� P G (m @@ n) B x) 127232812Sjmallett ��� 128232812Sjmallett (���G m u A B x. 129232812Sjmallett (���v y. v ��� ctxtFV G ��� P ((v,A)::G) ([VAR v/u] m) B y) ��� 130232812Sjmallett u ��� ctxtFV G ��� u ��� fv x 131232812Sjmallett ��� 132232812Sjmallett P G (LAM u m) (A --> B) x) 133232812Sjmallett ��� 134232812Sjmallett ���G m ty. G ||- m -: ty ��� ���x. P G m ty x 135232812SjmallettProof 136232812Sjmallett REPEAT GEN_TAC THEN STRIP_TAC THEN 137232812Sjmallett ������G m ty. G ||- m -: ty ==> 138232812Sjmallett ���pi x. P (ctxtswap pi G) (tpm pi m) ty x��� 139232812Sjmallett suffices_by METIS_TAC [pmact_nil] THEN 140232812Sjmallett HO_MATCH_MP_TAC hastype2_ind THEN 141232812Sjmallett SRW_TAC [][] THEN1 METIS_TAC [] THEN 142232812Sjmallett Q.MATCH_ABBREV_TAC ���P GG (LAM vv MM) (A --> B) xx��� THEN 143232812Sjmallett Q_TAC (NEW_TAC "z") ���{vv} UNION FV MM UNION ctxtFV GG UNION fv xx��� THEN 144232812Sjmallett ���LAM vv MM = LAM z (tpm [(z,vv)] MM)��� 145232812Sjmallett by SRW_TAC [][tpm_ALPHA] THEN 146232812Sjmallett SRW_TAC [][] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN 147232812Sjmallett SRW_TAC [][] THEN 148232812Sjmallett FULL_SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss) [tpm_subst] THEN 149232812Sjmallett FIRST_X_ASSUM (Q.SPECL_THEN [���lswapstr (REVERSE ((z,vv)::pi)) v���, 150232812Sjmallett ���(z,vv)::pi���, ���y���] 151232812Sjmallett MP_TAC) THEN 152232812Sjmallett ASM_SIMP_TAC (srw_ss()) [pmact_decompose] THEN 153232812Sjmallett ���vv ��� ctxtFV GG��� by SRW_TAC [][Abbr���vv���, Abbr���GG���] THEN 154232812Sjmallett ���ctxtswap ((z,vv)::pi) G = ctxtswap [(z,vv)] GG��� 155232812Sjmallett by SRW_TAC [][Abbr���GG���, GSYM pmact_decompose] THEN 156232812Sjmallett ��� _ = GG��� by SRW_TAC [][ctxtswap_fresh] THEN 157232812Sjmallett ���tpm ((z,vv)::pi) m = tpm [(z,vv)] MM��� 158232812Sjmallett by SRW_TAC [][Abbr���MM���, GSYM pmact_decompose] THEN 159232812Sjmallett markerLib.RM_ABBREV_TAC "GG" THEN 160232812Sjmallett SRW_TAC [][] THEN 161232812Sjmallett FIRST_X_ASSUM MATCH_MP_TAC THEN 162232812Sjmallett FULL_SIMP_TAC (srw_ss()) [pmact_decompose] 163232812SjmallettQED 164232812Sjmallett 165232812Sjmallettval hastype2_bvc_ind0 = save_thm( 166232812Sjmallett "hastype2_bvc_ind0", 167232812Sjmallett (Q.GEN `P` o Q.GEN `X` o 168232812Sjmallett SIMP_RULE bool_ss [] o 169232812Sjmallett Q.SPECL [`\G m ty x. P G m ty`, `\x. X`]) hastype2_bvc_ind) 170232812Sjmallett 171232812Sjmallettval hastype2_valid_ctxt = store_thm( 172232812Sjmallett "hastype2_valid_ctxt", 173232812Sjmallett ``!G m A. G ||- m -: A ==> valid_ctxt G``, 174232812Sjmallett HO_MATCH_MP_TAC hastype2_ind THEN SRW_TAC [][] THEN METIS_TAC []); 175232812Sjmallett 176232812Sjmallettval hastype2_swap_eqn = store_thm( 177232812Sjmallett "hastype2_swap_eqn", 178232812Sjmallett ``G ||- tpm pi m -: A <=> ctxtswap (REVERSE pi) G ||- m -: A``, 179232812Sjmallett METIS_TAC [hastype2_swap, pmact_inverse]); 180232812Sjmallett 181232812Sjmallettval hastype2_hastype = prove( 182232812Sjmallett ``!G m A. G ||- m -: A ==> G |- m -: A``, 183232812Sjmallett HO_MATCH_MP_TAC hastype2_ind THEN REPEAT CONJ_TAC THENL [ 184232812Sjmallett (* var case *) SRW_TAC [][hastype_rules], 185232812Sjmallett (* app case *) METIS_TAC [hastype_rules], 186232812Sjmallett (* abs case *) METIS_TAC [hastype_rules, lemma14a] 187232812Sjmallett ]); 188232812Sjmallett 189232812Sjmallettval hastype_hastype2 = prove( 190232812Sjmallett ``!G m A. G |- m -: A ==> G ||- m -: A``, 191232812Sjmallett HO_MATCH_MP_TAC hastype_indX THEN Q.EXISTS_TAC `{}` THEN 192232812Sjmallett SRW_TAC [][hastype2_rules] THENL [ 193232812Sjmallett (* app case *) METIS_TAC [hastype2_rules], 194232812Sjmallett (* abs case; goal with IH is: *) 195232812Sjmallett MATCH_MP_TAC (last (CONJUNCTS hastype2_rules)) THEN 196232812Sjmallett SRW_TAC [][] THEN 197215976Sjmallett Cases_on `v = v'` THEN1 SRW_TAC [][lemma14a] THEN 198215976Sjmallett (* if v' = v, proof is trivial; rest of tactic is for other case *) 199215976Sjmallett `v' ��� ctxtFV ((v,A)::G)` by SRW_TAC [][] THEN 200215976Sjmallett `~(v' IN FV m)` by METIS_TAC [hastype_FV] THEN 201215976Sjmallett `[VAR v'/v] m = tpm [(v',v)] m` by SRW_TAC [][fresh_tpm_subst] THEN 202215976Sjmallett SRW_TAC [][hastype2_swap_eqn, ctxtswap_fresh] 203215976Sjmallett ]); 204215976Sjmallett 205215976Sjmallettval hastype_hastype2_eqn = store_thm( 206215976Sjmallett "hastype_hastype2_eqn", 207215976Sjmallett ``G |- m -: A <=> G ||- m -: A``, 208215976Sjmallett METIS_TAC [hastype2_hastype, hastype_hastype2]); 209215976Sjmallett 210215976Sjmallettval _ = export_theory () 211215976Sjmallett