From 31d69d84f0bef2a691ca764139b9ca34c8bf5ee5 Mon Sep 17 00:00:00 2001 From: Chun Tian Date: Fri, 6 Oct 2023 12:29:24 +1100 Subject: [PATCH] Done hreduce1_substitutive (Lemma 8.3.12); moved/balanced existing contents --- examples/lambda/barendregt/chap2Script.sml | 166 ++++++++ .../barendregt/head_reductionScript.sml | 273 ++++++++++-- .../lambda/barendregt/normal_orderScript.sml | 7 +- examples/lambda/barendregt/solvableScript.sml | 14 +- .../barendregt/standardisationScript.sml | 398 +----------------- examples/lambda/basics/appFOLDLScript.sml | 137 +++++- examples/lambda/basics/nomsetScript.sml | 7 + examples/lambda/basics/termScript.sml | 21 +- examples/lambda/typing/sttScript.sml | 69 --- 9 files changed, 584 insertions(+), 508 deletions(-) diff --git a/examples/lambda/barendregt/chap2Script.sml b/examples/lambda/barendregt/chap2Script.sml index 8c6746961c..e73bb1be60 100644 --- a/examples/lambda/barendregt/chap2Script.sml +++ b/examples/lambda/barendregt/chap2Script.sml @@ -235,9 +235,12 @@ val (asmlam_rules, asmlam_ind, asmlam_cases) = Hol_reln` (!x M M'. asmlam eqns M M' ==> asmlam eqns (LAM x M) (LAM x M')) `; +(* This is also Definition 2.1.32 [1, p.33] *) val incompatible_def = Define`incompatible x y = ~consistent (asmlam {(x,y)})` +Overload "#" = “incompatible” + val S_def = Define`S = LAM "x" (LAM "y" (LAM "z" ((VAR "x" @@ VAR "z") @@ @@ -550,12 +553,31 @@ Proof >> qexistsl_tac [‘v’, ‘t0’] >> REWRITE_TAC [] QED +Theorem is_abs_appstar[simp]: + is_abs (M @* Ns) ⇔ is_abs M ∧ (Ns = []) +Proof + Induct_on ‘Ns’ using SNOC_INDUCT >> + simp[appstar_SNOC] +QED + +Theorem is_abs_LAMl[simp]: + is_abs (LAMl vs M) ⇔ vs ≠ [] ∨ is_abs M +Proof + Cases_on ‘vs’ >> simp[] +QED + val (is_comb_thm, _) = define_recursive_term_function `(is_comb (VAR s) = F) /\ (is_comb (t1 @@ t2) = T) /\ (is_comb (LAM v t) = F)`; val _ = export_rewrites ["is_comb_thm"] +Theorem is_comb_LAMl[simp] : + is_comb (LAMl vs M) <=> (vs = []) /\ is_comb M +Proof + Cases_on `vs` THEN SRW_TAC [][] +QED + Theorem is_comb_vsubst_invariant[simp]: !t. is_comb ([VAR v/u] t) = is_comb t Proof @@ -628,6 +650,39 @@ Proof SRW_TAC [][SUB_THM, SUB_VAR] QED +Theorem bnf_characterisation: + ∀M. + bnf M ⇔ + ∃vs v Ms. ALL_DISTINCT vs ∧ M = LAMl vs (VAR v ·· Ms) ∧ + (∀M. MEM M Ms ⇒ bnf M) +Proof + ho_match_mp_tac nc_INDUCTION2 >> qexists ‘∅’ >> rw[] >~ + [‘VAR _ ·· _ = M1 @@ M2’] + >- (simp[] >> eq_tac >> rpt strip_tac >~ + [‘M1 = LAMl vs1 _’, ‘M1 @@ M2’] + >- (gvs[app_eq_appstar] >> + Q.REFINE_EXISTS_TAC ‘SNOC M Mt’ >> + simp[DISJ_IMP_THM, rich_listTheory.FRONT_APPEND] >> + metis_tac[]) >> + Cases_on ‘Ms’ using rich_listTheory.SNOC_CASES >> + gvs[rich_listTheory.SNOC_APPEND, appstar_APPEND] >> + dsimp[LAMl_eq_appstar] >> irule_at Any EQ_REFL >> simp[]) >> + pop_assum SUBST_ALL_TAC >> eq_tac >> rpt strip_tac >> gvs[] >~ + [‘LAM y (LAMl vs _)’] + >- (reverse (Cases_on ‘MEM y vs’) + >- (qexists ‘y::vs’ >> simp[]) >> + ‘y # LAMl vs (VAR v ·· Ms)’ by simp[FV_LAMl] >> + Q_TAC (NEW_TAC "z") ‘y INSERT set vs ∪ FV (VAR v ·· Ms)’ >> + ‘z # LAMl vs (VAR v ·· Ms)’ by simp[FV_LAMl] >> + dxrule_then (qspec_then ‘y’ mp_tac) tpm_ALPHA >> + simp[tpm_fresh, FV_LAMl] >> strip_tac >> qexists ‘z::vs’ >> simp[]) >> + rename [‘LAM y M = LAMl vs (VAR v ·· Ms)’] >> + Cases_on ‘vs’ >> gvs[] >> gvs[LAM_eq_thm] + >- metis_tac[] >> + simp[tpm_LAMl, tpm_appstar] >> irule_at Any EQ_REFL >> + simp[MEM_listpm] >> rpt strip_tac >> first_assum drule >> simp[] +QED + val _ = augment_srw_ss [rewrites [LAM_eq_thm]] val (rand_thm, _) = define_recursive_term_function `rand (t1 @@ t2) = t2`; val _ = export_rewrites ["rand_thm"] @@ -739,6 +794,117 @@ Proof Induct_on ‘Ns’ using SNOC_INDUCT >> rw [appstar_SNOC, lameq_APPL] QED +Theorem lameq_LAMl_appstar : + !vs M Ns. ALL_DISTINCT vs /\ (LENGTH vs = LENGTH Ns) /\ EVERY closed Ns ==> + LAMl vs M @* Ns == (FEMPTY |++ ZIP (vs,Ns)) ' M +Proof + rpt STRIP_TAC + >> NewQ.ABBREV_TAC ‘L = ZIP (vs,Ns)’ + >> ‘(Ns = MAP SND L) /\ (vs = MAP FST L)’ by rw [Abbr ‘L’, MAP_ZIP] + >> FULL_SIMP_TAC std_ss [] + >> Q.PAT_X_ASSUM ‘EVERY closed (MAP SND L)’ MP_TAC + >> Q.PAT_X_ASSUM ‘ALL_DISTINCT (MAP FST L)’ MP_TAC + >> KILL_TAC + >> Q.ID_SPEC_TAC ‘M’ + >> Induct_on ‘L’ >> rw [] + >- (Suff ‘FEMPTY |++ [] = FEMPTY :string |-> term’ >- rw [] \\ + rw [FUPDATE_LIST_EQ_FEMPTY]) + >> NewQ.ABBREV_TAC ‘v = FST h’ + >> NewQ.ABBREV_TAC ‘vs = MAP FST L’ + >> NewQ.ABBREV_TAC ‘N = SND h’ + >> NewQ.ABBREV_TAC ‘Ns = MAP SND L’ + (* RHS rewriting *) + >> ‘h :: L = [h] ++ L’ by rw [] >> POP_ORW + >> rw [FUPDATE_LIST_APPEND] + >> Know ‘FEMPTY |++ [h] |++ L = FEMPTY |++ L |++ [h]’ + >- (MATCH_MP_TAC FUPDATE_LIST_APPEND_COMMUTES \\ + rw [DISJOINT_ALT]) + >> Rewr' + >> rw [GSYM FUPDATE_EQ_FUPDATE_LIST] + >> NewQ.ABBREV_TAC ‘fm = FEMPTY |++ L’ + >> FULL_SIMP_TAC std_ss [] + >> ‘h = (v,N)’ by rw [Abbr ‘v’, Abbr ‘N’] >> POP_ORW + >> Know ‘(fm |+ (v,N)) ' M = fm ' ([N/v] M)’ + >- (MATCH_MP_TAC ssub_update_apply' \\ + Q.PAT_X_ASSUM ‘closed N’ MP_TAC \\ + rw [Abbr ‘fm’, FDOM_FUPDATE_LIST, closed_def] \\ + Cases_on ‘INDEX_OF y vs’ >- fs [INDEX_OF_eq_NONE] \\ + rename1 ‘INDEX_OF y vs = SOME n’ \\ + fs [INDEX_OF_eq_SOME] \\ + Q.PAT_X_ASSUM ‘EL n vs = y’ (ONCE_REWRITE_TAC o wrap o SYM) \\ + ‘LENGTH L = LENGTH vs’ by rw [Abbr ‘vs’, LENGTH_MAP] \\ + Know ‘(FEMPTY |++ L) ' (EL n vs) = EL n Ns’ + >- (MATCH_MP_TAC FUPDATE_LIST_APPLY_MEM \\ + Q.EXISTS_TAC ‘n’ >> rw [] \\ + ‘m <> n’ by rw [] \\ + METIS_TAC [EL_ALL_DISTINCT_EL_EQ]) >> Rewr' \\ + Q.PAT_X_ASSUM ‘EVERY closed Ns’ MP_TAC \\ + rw [EVERY_MEM, closed_def] \\ + POP_ASSUM MATCH_MP_TAC >> rw [MEM_EL] \\ + ‘LENGTH L = LENGTH Ns’ by rw [Abbr ‘Ns’, LENGTH_MAP] \\ + Q.EXISTS_TAC ‘n’ >> rw []) + >> Rewr' + (* LHS rewriting *) + >> Know ‘LAM v (LAMl vs M) @@ N == LAMl vs ([N/v] M)’ + >- (SIMP_TAC (betafy (srw_ss())) [] \\ + Suff ‘[N/v] (LAMl vs M) = LAMl vs ([N/v] M)’ >- rw [lameq_rules] \\ + MATCH_MP_TAC LAMl_SUB \\ + Q.PAT_X_ASSUM ‘closed N’ MP_TAC >> rw [closed_def]) + >> DISCH_TAC + >> MATCH_MP_TAC lameq_TRANS + >> Q.EXISTS_TAC ‘LAMl vs ([N/v] M) @* Ns’ >> art [] + >> MATCH_MP_TAC lameq_appstar_cong >> art [] +QED + +val foldl_snoc = prove( + ``!l f x y. FOLDL f x (APPEND l [y]) = f (FOLDL f x l) y``, + Induct THEN SRW_TAC [][]); + +val combs_not_size_1 = prove( + ``(size M = 1) ==> ~is_comb M``, + Q.SPEC_THEN `M` STRUCT_CASES_TAC term_CASES THEN + SRW_TAC [][size_thm, size_nz]); + +Theorem strange_cases : + !M : term. (?vs M'. (M = LAMl vs M') /\ (size M' = 1)) \/ + (?vs args t. + (M = LAMl vs (FOLDL APP t args)) /\ + ~(args = []) /\ ~is_comb t) +Proof + HO_MATCH_MP_TAC simple_induction THEN REPEAT CONJ_TAC THENL [ + (* VAR *) GEN_TAC THEN DISJ1_TAC THEN + MAP_EVERY Q.EXISTS_TAC [`[]`, `VAR s`] THEN SRW_TAC [][size_thm], + (* app *) MAP_EVERY Q.X_GEN_TAC [`M`,`N`] THEN + DISCH_THEN (CONJUNCTS_THEN ASSUME_TAC) THEN + DISJ2_TAC THEN Q.EXISTS_TAC `[]` THEN + SIMP_TAC (srw_ss()) [] THEN + `(?vs M'. (M = LAMl vs M') /\ (size M' = 1)) \/ + (?vs args t. + (M = LAMl vs (FOLDL APP t args)) /\ ~(args = []) /\ + ~is_comb t)` by PROVE_TAC [] + THENL [ + MAP_EVERY Q.EXISTS_TAC [`[N]`, `M`] THEN + ASM_SIMP_TAC (srw_ss()) [] THEN + PROVE_TAC [combs_not_size_1], + ASM_SIMP_TAC (srw_ss()) [] THEN + Cases_on `vs` THENL [ + MAP_EVERY Q.EXISTS_TAC [`APPEND args [N]`, `t`] THEN + ASM_SIMP_TAC (srw_ss()) [foldl_snoc], + MAP_EVERY Q.EXISTS_TAC [`[N]`, `M`] THEN + ASM_SIMP_TAC (srw_ss()) [] + ] + ], + (* LAM *) MAP_EVERY Q.X_GEN_TAC [`x`,`M`] THEN STRIP_TAC THENL [ + DISJ1_TAC THEN + MAP_EVERY Q.EXISTS_TAC [`x::vs`, `M'`] THEN + ASM_SIMP_TAC (srw_ss()) [], + DISJ2_TAC THEN + MAP_EVERY Q.EXISTS_TAC [`x::vs`, `args`, `t`] THEN + ASM_SIMP_TAC (srw_ss()) [] + ] + ] +QED + val _ = remove_ovl_mapping "Y" {Thy = "chap2", Name = "Y"} val _ = export_theory() diff --git a/examples/lambda/barendregt/head_reductionScript.sml b/examples/lambda/barendregt/head_reductionScript.sml index 8ecda24d66..d9040b199d 100644 --- a/examples/lambda/barendregt/head_reductionScript.sml +++ b/examples/lambda/barendregt/head_reductionScript.sml @@ -1,8 +1,10 @@ open HolKernel Parse boolLib bossLib -open pred_setTheory boolSimps; +open boolSimps relationTheory pred_setTheory listTheory finite_mapTheory + hurdUtils; -open termTheory chap2Theory chap3Theory nomsetTheory binderLib; +open termTheory appFOLDLTheory chap2Theory chap3Theory nomsetTheory binderLib + term_posnsTheory; val _ = new_theory "head_reduction" @@ -12,11 +14,13 @@ fun Store_thm(trip as (n,t,tac)) = store_thm trip before export_rewrites [n] val _ = set_trace "Unicode" 1 -val (hreduce1_rules, hreduce1_ind, hreduce1_cases) = Hol_reln` +Inductive hreduce1 : (∀v M N. hreduce1 (LAM v M @@ N) ([N/v]M)) ∧ +[~LAM:] (∀v M1 M2. hreduce1 M1 M2 ⇒ hreduce1 (LAM v M1) (LAM v M2)) ∧ +[~APP:] (∀M1 M2 N. hreduce1 M1 M2 ∧ ¬is_abs M1 ⇒ hreduce1 (M1 @@ N) (M2 @@ N)) -`; +End val _ = set_fixity "-h->" (Infix(NONASSOC, 450)) val _ = overload_on ("-h->", ``hreduce1``) @@ -43,18 +47,17 @@ val _ = temp_add_rule {block_style = (AroundEachPhrase, (PP.INCONSISTENT,2)), term_name = "apply_perm"} val _ = temp_overload_on ("apply_perm", ``λp M. tpm [p] M``) val _ = temp_overload_on ("apply_perm", ``tpm``) -val _ = temp_overload_on ("#", ``λv t. v ∉ FV t``) -val _ = temp_set_fixity "#" (Infix(NONASSOC, 450)) val tpm_hreduce_I = store_thm( "tpm_hreduce_I", ``∀M N. M -h-> N ⇒ ∀π. π·M -h-> π·N``, HO_MATCH_MP_TAC hreduce1_ind THEN SRW_TAC [][tpm_subst, hreduce1_rules]); -val tpm_hreduce = store_thm( - "tpm_hreduce", - ``∀M N π. π·M -h-> π·N ⇔ M -h-> N``, - METIS_TAC [pmact_inverse, tpm_hreduce_I]); +Theorem tpm_hreduce[simp] : + ∀M N π. π·M -h-> π·N ⇔ M -h-> N +Proof + METIS_TAC [pmact_inverse, tpm_hreduce_I] +QED val hreduce1_rwts = store_thm( "hreduce1_rwts", @@ -86,6 +89,94 @@ val hreduce1_rwts = store_thm( METIS_TAC [lemma15a, pmact_flip_args, fresh_tpm_subst] ]); +val hreduce1_unique = store_thm( + "hreduce1_unique", + ``∀M N1 N2. M -h-> N1 ∧ M -h-> N2 ⇒ (N1 = N2)``, + Q_TAC SUFF_TAC `∀M N. M -h-> N ⇒ ∀P. M -h-> P ⇒ (N = P)` + THEN1 METIS_TAC [] THEN + HO_MATCH_MP_TAC hreduce1_ind THEN + SIMP_TAC (srw_ss() ++ DNF_ss) [hreduce1_rwts]); + +Theorem hreduce1_gen_bvc_ind : + !P f. (!x. FINITE (f x)) /\ + (!v M N x. v NOTIN f x ==> P (LAM v M @@ N) ([N/v] M) x) /\ + (!v M1 M2 x. M1 -h-> M2 /\ v NOTIN f x /\ (!z. P M1 M2 z) ==> + P (LAM v M1) (LAM v M2) x) /\ + (!M1 M2 N x. M1 -h-> M2 /\ (!z. P M1 M2 z) /\ ~is_abs M1 ==> + P (M1 @@ N) (M2 @@ N) x) + ==> !M N. M -h-> N ==> !x. P M N x +Proof + rpt GEN_TAC >> STRIP_TAC + >> Suff ‘!M N. M -h-> N ==> !p x. P (tpm p M) (tpm p N) x’ + >- METIS_TAC [pmact_nil] + >> HO_MATCH_MP_TAC hreduce1_strongind + >> reverse (rw []) (* easy goal first *) + >- (Q.ABBREV_TAC ‘u = lswapstr p v’ \\ + Q_TAC (NEW_TAC "z") ‘(f x) UNION {v} UNION FV (tpm p M) UNION FV (tpm p N)’ \\ + ‘(LAM u (tpm p M) = LAM z (tpm ([(z,u)] ++ p) M)) /\ + (LAM u (tpm p N) = LAM z (tpm ([(z,u)] ++ p) N))’ + by rw [tpm_ALPHA, pmact_decompose] >> rw []) + (* stage work *) + >> Q.ABBREV_TAC ‘u = lswapstr p v’ + >> Q_TAC (NEW_TAC "z") ‘(f x) UNION {v} UNION FV (tpm p M) UNION FV (tpm p N)’ + >> ‘LAM u (tpm p M) = LAM z (tpm ([(z,u)] ++ p) M)’ by rw [tpm_ALPHA, pmact_decompose] + >> POP_ORW + >> Q.ABBREV_TAC ‘M1 = apply_perm ([(z,u)] ++ p) M’ + >> Suff ‘tpm p ([N/v] M) = [tpm p N/z] M1’ >- rw [] + >> rw [tpm_subst, Abbr ‘M1’] + >> simp [Once tpm_CONS, fresh_tpm_subst] + >> simp [lemma15a] +QED + +(* |- !P X. + FINITE X /\ (!v M N. v NOTIN X ==> P (LAM v M @@ N) ([N/v] M)) /\ + (!v M1 M2. M1 -h-> M2 /\ v NOTIN X /\ P M1 M2 ==> P (LAM v M1) (LAM v M2)) /\ + (!M1 M2 N. M1 -h-> M2 /\ P M1 M2 /\ ~is_abs M1 ==> P (M1 @@ N) (M2 @@ N)) ==> + !M N. M -h-> N ==> P M N + *) +Theorem hreduce1_bvcX_ind = + hreduce1_gen_bvc_ind |> Q.SPECL [`λM N x. P' M N`, `λx. X`] + |> SIMP_RULE (srw_ss()) [] + |> Q.INST [`P'` |-> `P`] + |> Q.GEN `X` |> Q.GEN `P` + +(* Lemma 8.3.12 [1, p.174] *) +Theorem hreduce1_substitutive : + !M N. M -h-> N ==> [P/v] M -h-> [P/v] N +Proof + HO_MATCH_MP_TAC hreduce1_bvcX_ind + >> Q.EXISTS_TAC ‘FV P UNION {v}’ >> rw [hreduce1_rules] + >- METIS_TAC [substitution_lemma, hreduce1_rules] + >> ‘is_comb M \/ is_var M’ by METIS_TAC [term_cases] + >- (MATCH_MP_TAC hreduce1_APP >> art [] \\ + gs [is_comb_APP_EXISTS, is_abs_thm]) + >> gs [is_var_cases, hreduce1_rwts] +QED + +(* This form is useful for ‘|- substitutive R ==> ...’ theorems (chap3Theory) *) +Theorem substitutive_hreduce1 : + substitutive (-h->) +Proof + rw [substitutive_def, hreduce1_substitutive] +QED + +Theorem hreduce_substitutive : + !M N. M -h->* N ==> [P/v] M -h->* [P/v] N +Proof + HO_MATCH_MP_TAC RTC_INDUCT >> rw [] + >> METIS_TAC [RTC_RULES, hreduce1_substitutive] +QED + +Theorem substitutive_hreduce : + substitutive (-h->*) +Proof + rw [substitutive_def, hreduce_substitutive] +QED + +(* ---------------------------------------------------------------------- + Head normal form (hnf) + ---------------------------------------------------------------------- *) + val hnf_def = Define`hnf M = ∀N. ¬(M -h-> N)`; val hnf_thm = Store_thm( "hnf_thm", @@ -102,14 +193,6 @@ val hnf_tpm = Store_thm( ``∀M π. hnf (π·M) = hnf M``, HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]); -val hreduce1_unique = store_thm( - "hreduce1_unique", - ``∀M N1 N2. M -h-> N1 ∧ M -h-> N2 ⇒ (N1 = N2)``, - Q_TAC SUFF_TAC `∀M N. M -h-> N ⇒ ∀P. M -h-> P ⇒ (N = P)` - THEN1 METIS_TAC [] THEN - HO_MATCH_MP_TAC hreduce1_ind THEN - SIMP_TAC (srw_ss() ++ DNF_ss) [hreduce1_rwts]); - val strong_cc_ind = IndDefLib.derive_strong_induction (compat_closure_rules, compat_closure_ind) @@ -128,16 +211,18 @@ val hnf_ccbeta_preserved = store_thm( SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] ]); -val (weak_head_rules, weak_head_ind, weak_head_cases) = Hol_reln` +(* ---------------------------------------------------------------------- + Weak head reductions (weak_head or -w->) + ---------------------------------------------------------------------- *) + +Inductive weak_head : (∀v M N. weak_head (LAM v M @@ N) ([N/v]M)) ∧ (∀M₁ M₂ N. weak_head M₁ M₂ ⇒ weak_head (M₁ @@ N) (M₂ @@ N)) -`; +End + val _ = set_fixity "-w->" (Infix(NONASSOC, 450)) val _ = overload_on ("-w->", ``weak_head``) -val strong_weak_ind = IndDefLib.derive_strong_induction(weak_head_rules, - weak_head_ind) - val wh_is_abs = store_thm( "wh_is_abs", ``∀M N. M -w-> N ⇒ ¬is_abs M``, @@ -151,9 +236,8 @@ val wh_lam = Store_thm( val wh_head = store_thm( "wh_head", ``∀M N. M -w-> N ⇒ M -h-> N``, - HO_MATCH_MP_TAC strong_weak_ind THEN METIS_TAC [wh_is_abs, hreduce1_rules]); - - + HO_MATCH_MP_TAC weak_head_strongind + >> METIS_TAC [wh_is_abs, hreduce1_rules]); val _ = set_fixity "-w->*" (Infix(NONASSOC, 450)) val _ = overload_on ("-w->*", ``RTC (-w->)``) @@ -353,7 +437,111 @@ val head_reductions_have_weak_prefixes = store_thm( metis_tac [relationTheory.RTC_RULES, hreduce_weak_or_strong]); (* ---------------------------------------------------------------------- - HNF and Combinators + Head redex + ---------------------------------------------------------------------- *) + +val _ = add_infix ("is_head_redex", 760, NONASSOC) + +Inductive is_head_redex : + (!v (t:term) u. [] is_head_redex (LAM v t @@ u)) /\ + (!v t p. p is_head_redex t ==> (In::p) is_head_redex (LAM v t)) /\ + (!t u v p. p is_head_redex (t @@ u) ==> + (Lt::p) is_head_redex (t @@ u) @@ v) +End + +val ihr_bvc_ind = store_thm( + "ihr_bvc_ind", + ``!P X. FINITE X /\ + (!v M N. ~(v IN X) /\ ~(v IN FV N) ==> P [] (LAM v M @@ N)) /\ + (!v M p. ~(v IN X) /\ P p M ==> P (In::p) (LAM v M)) /\ + (!M N L p. P p (M @@ N) ==> P (Lt::p) ((M @@ N) @@ L)) ==> + !p M. p is_head_redex M ==> P p M``, + REPEAT GEN_TAC THEN STRIP_TAC THEN + Q_TAC SUFF_TAC `!p M. p is_head_redex M ==> !pi. P p (tpm pi M)` + THEN1 METIS_TAC [pmact_nil] THEN + HO_MATCH_MP_TAC is_head_redex_ind THEN + SRW_TAC [][is_head_redex_rules] THENL [ + Q.MATCH_ABBREV_TAC `P [] (LAM vv MM @@ NN)` THEN + markerLib.RM_ALL_ABBREVS_TAC THEN + Q_TAC (NEW_TAC "z") `FV MM UNION FV NN UNION X` THEN + `LAM vv MM = LAM z (tpm [(z,vv)] MM)` by SRW_TAC [][tpm_ALPHA] THEN + SRW_TAC [][], + Q.MATCH_ABBREV_TAC `P (In::p) (LAM vv MM)` THEN + Q_TAC (NEW_TAC "z") `FV MM UNION X` THEN + `LAM vv MM = LAM z (tpm [(z,vv)] MM)` by SRW_TAC [][tpm_ALPHA] THEN + SRW_TAC [][GSYM pmact_decompose, Abbr`MM`] + ]); + +val is_head_redex_subst_invariant = store_thm( + "is_head_redex_subst_invariant", + ``!p t u v. p is_head_redex t ==> p is_head_redex [u/v] t``, + REPEAT GEN_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`t`, `p`] THEN + HO_MATCH_MP_TAC ihr_bvc_ind THEN Q.EXISTS_TAC `v INSERT FV u` THEN + SRW_TAC [][SUB_THM, SUB_VAR, is_head_redex_rules]); + +Theorem is_head_redex_tpm_invariant[simp] : + p is_head_redex (tpm pi t) = p is_head_redex t +Proof + Q_TAC SUFF_TAC `!p t. p is_head_redex t ==> !pi. p is_head_redex (tpm pi t)` + THEN1 METIS_TAC [pmact_inverse] THEN + HO_MATCH_MP_TAC is_head_redex_ind THEN SRW_TAC [][is_head_redex_rules] +QED + +val is_head_redex_unique = store_thm( + "is_head_redex_unique", + ``!t p1 p2. p1 is_head_redex t /\ p2 is_head_redex t ==> (p1 = p2)``, + Q_TAC SUFF_TAC + `!p1 t. p1 is_head_redex t ==> !p2. p2 is_head_redex t ==> (p1 = p2)` + THEN1 PROVE_TAC [] THEN + HO_MATCH_MP_TAC is_head_redex_ind THEN REPEAT STRIP_TAC THEN + POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC [is_head_redex_cases] THEN + SRW_TAC [][LAM_eq_thm]); + +val is_head_redex_thm = store_thm( + "is_head_redex_thm", + ``(p is_head_redex (LAM v t) = ?p0. (p = In::p0) /\ p0 is_head_redex t) /\ + (p is_head_redex (t @@ u) = (p = []) /\ is_abs t \/ + ?p0. (p = Lt::p0) /\ is_comb t /\ + p0 is_head_redex t) /\ + (p is_head_redex (VAR v) = F)``, + REPEAT CONJ_TAC THEN + SRW_TAC [][Once is_head_redex_cases, SimpLHS, LAM_eq_thm] THEN + SRW_TAC [][EQ_IMP_THM] THENL [ + PROVE_TAC [], + PROVE_TAC [is_abs_thm, term_CASES], + METIS_TAC [is_comb_thm, term_CASES] + ]); + +val head_redex_leftmost = store_thm( + "head_redex_leftmost", + ``!p t. p is_head_redex t ==> + !p'. p' IN redex_posns t ==> (p = p') \/ p < p'``, + HO_MATCH_MP_TAC is_head_redex_ind THEN + SRW_TAC [][redex_posns_thm, DISJ_IMP_THM]); + +val hnf_no_head_redex = store_thm( + "hnf_no_head_redex", + ``!t. hnf t = !p. ~(p is_head_redex t)``, + HO_MATCH_MP_TAC simple_induction THEN + SRW_TAC [][hnf_thm, is_head_redex_thm] THEN + Q.SPEC_THEN `t` STRUCT_CASES_TAC term_CASES THEN + SRW_TAC [][is_head_redex_thm]); + +val head_redex_is_redex = store_thm( + "head_redex_is_redex", + ``!p t. p is_head_redex t ==> p IN redex_posns t``, + HO_MATCH_MP_TAC is_head_redex_ind THEN + SRW_TAC [][redex_posns_thm]); + +val is_head_redex_vsubst_invariant = store_thm( + "is_head_redex_vsubst_invariant", + ``!t v x p. p is_head_redex ([VAR v/x] t) = p is_head_redex t``, + REPEAT GEN_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`p`, `t`] THEN + HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{x;v}` THEN + SRW_TAC [][is_head_redex_thm, SUB_THM, SUB_VAR]); + +(* ---------------------------------------------------------------------- + More results about head normal forms (hnf) ---------------------------------------------------------------------- *) Theorem hnf_I : @@ -362,4 +550,35 @@ Proof RW_TAC std_ss [hnf_thm, I_def] QED +Theorem hnf_LAMl[simp] : + hnf (LAMl vs M) <=> hnf M +Proof + Induct_on ‘vs’ >> rw [] +QED + +Theorem hnf_appstar : + !M Ns. hnf (M @* Ns) <=> hnf M /\ (is_abs M ⇒ (Ns = [])) +Proof + Induct_on ‘Ns’ using SNOC_INDUCT >> simp[appstar_SNOC] >> + dsimp[SF CONJ_ss] >> metis_tac[] +QED + +(* FIXME: can we put ‘ALL_DISTINCT vs’ into RHS? cf. bnf_characterisation *) +Theorem hnf_cases : + !M : term. hnf M <=> ?vs args y. M = LAMl vs (VAR y @* args) +Proof + simp[FORALL_AND_THM, EQ_IMP_THM] >> conj_tac + >- (gen_tac >> MP_TAC (Q.SPEC ‘M’ strange_cases) + >> RW_TAC std_ss [] + >- (FULL_SIMP_TAC std_ss [size_1_cases] \\ + qexistsl_tac [‘vs’, ‘[]’, ‘y’] >> rw []) + >> FULL_SIMP_TAC std_ss [hnf_LAMl] + >> ‘hnf t /\ ~is_abs t’ by PROVE_TAC [hnf_appstar] + >> ‘is_var t’ by METIS_TAC [term_cases] + >> FULL_SIMP_TAC std_ss [is_var_cases] + >> qexistsl_tac [‘vs’, ‘args’, ‘y’] >> art []) >> + simp[PULL_EXISTS, hnf_appstar] +QED + val _ = export_theory() +val _ = html_theory "head_reduction"; diff --git a/examples/lambda/barendregt/normal_orderScript.sml b/examples/lambda/barendregt/normal_orderScript.sml index a1083f4aca..6f08fa949b 100644 --- a/examples/lambda/barendregt/normal_orderScript.sml +++ b/examples/lambda/barendregt/normal_orderScript.sml @@ -1,8 +1,9 @@ open HolKernel Parse boolLib bossLib -open boolSimps pred_setTheory pathTheory binderLib -open chap3Theory standardisationTheory term_posnsTheory termTheory - finite_developmentsTheory appFOLDLTheory nomsetTheory +open boolSimps pred_setTheory pathTheory; + +open chap3Theory standardisationTheory term_posnsTheory termTheory binderLib + finite_developmentsTheory appFOLDLTheory nomsetTheory head_reductionTheory; val _ = new_theory "normal_order" diff --git a/examples/lambda/barendregt/solvableScript.sml b/examples/lambda/barendregt/solvableScript.sml index 4293d79c98..c00e86a45d 100644 --- a/examples/lambda/barendregt/solvableScript.sml +++ b/examples/lambda/barendregt/solvableScript.sml @@ -10,7 +10,7 @@ open arithmeticTheory pred_setTheory listTheory sortingTheory finite_mapTheory (* lambda theories *) open termTheory appFOLDLTheory chap2Theory chap3Theory standardisationTheory - reductionEval; + head_reductionTheory reductionEval; val _ = new_theory "solvable"; @@ -238,7 +238,7 @@ Proof >> Q.ABBREV_TAC ‘fm = FEMPTY |++ ZIP (vs,Ns0)’ >> Know ‘LAMl vs M @* Ns0 == fm ' M’ >- (Q.UNABBREV_TAC ‘fm’ \\ - MATCH_MP_TAC LAMl_appstar >> rw []) + MATCH_MP_TAC lameq_LAMl_appstar >> rw []) >> DISCH_TAC >> ‘LAMl vs M @* Ns0 @* Ns1 == fm ' M @* Ns1’ by PROVE_TAC [lameq_appstar_cong] >> ‘fm ' M @* Ns1 == I’ by PROVE_TAC [lameq_TRANS, lameq_SYM] @@ -290,7 +290,7 @@ Proof >> rw [solvable_def, closed_substitution_instances_def] >> Q.ABBREV_TAC ‘vss = FDOM fm’ >> ‘FINITE vss’ by rw [FDOM_FINITE, Abbr ‘vss’] - (* preparing for LAMl_appstar *) + (* preparing for lameq_LAMl_appstar *) >> Q.ABBREV_TAC ‘vs = SET_TO_LIST vss’ >> ‘ALL_DISTINCT vs’ by PROVE_TAC [Abbr ‘vs’, ALL_DISTINCT_SET_TO_LIST] >> Q.ABBREV_TAC ‘Ps = MAP (\v. fm ' v) vs’ @@ -316,7 +316,7 @@ Proof >> Rewr' >> DISCH_TAC >> Know ‘LAMl vs M @* Ps == (FEMPTY |++ ZIP (vs,Ps)) ' M’ - >- (MATCH_MP_TAC LAMl_appstar >> art [] \\ + >- (MATCH_MP_TAC lameq_LAMl_appstar >> art [] \\ rw [Abbr ‘Ps’, EVERY_MEM, MEM_MAP] \\ FIRST_X_ASSUM MATCH_MP_TAC \\ POP_ASSUM MP_TAC \\ @@ -364,7 +364,7 @@ Proof >> Q.ABBREV_TAC ‘fm = FEMPTY |++ ZIP (vs,Ns0)’ >> Know ‘LAMl vs M @* Ns0 == fm ' M’ >- (Q.UNABBREV_TAC ‘fm’ \\ - MATCH_MP_TAC LAMl_appstar >> rw []) + MATCH_MP_TAC lameq_LAMl_appstar >> rw []) >> DISCH_TAC >> ‘LAMl vs M @* Ns0 @* Ns1 == fm ' M @* Ns1’ by PROVE_TAC [lameq_appstar_cong] >> ‘fm ' M @* Ns1 == I’ by PROVE_TAC [lameq_TRANS, lameq_SYM] @@ -387,7 +387,7 @@ Proof >> Q.ABBREV_TAC ‘fm' = FEMPTY |++ ZIP (vs',Ns0')’ >> Know ‘LAMl vs' M @* Ns0' == fm' ' M’ >- (Q.UNABBREV_TAC ‘fm'’ \\ - MATCH_MP_TAC LAMl_appstar >> rw []) + MATCH_MP_TAC lameq_LAMl_appstar >> rw []) >> DISCH_TAC >> ‘LAMl vs' M @* Ns0' @* Ns1 == fm' ' M @* Ns1’ by PROVE_TAC [lameq_appstar_cong] >> MATCH_MP_TAC lameq_TRANS @@ -486,7 +486,7 @@ QED Theorem ssub_LAM[local] = List.nth(CONJUNCTS ssub_thm, 2) -(* Lemma 8.3.3 (ii) *) +(* Lemma 8.3.3 (ii) [1, p.172] *) Theorem solvable_iff_LAM[simp] : !x M. solvable (LAM x M) <=> solvable M Proof diff --git a/examples/lambda/barendregt/standardisationScript.sml b/examples/lambda/barendregt/standardisationScript.sml index a3caae2a59..160de045bb 100644 --- a/examples/lambda/barendregt/standardisationScript.sml +++ b/examples/lambda/barendregt/standardisationScript.sml @@ -61,106 +61,6 @@ val better_standard_reduction = store_thm( SRW_TAC [][] ]); -val _ = add_infix ("is_head_redex", 760, NONASSOC) - -val (is_head_redex_rules, is_head_redex_ind, is_head_redex_cases) = - IndDefLib.Hol_reln` - (!v (t:term) u. [] is_head_redex (LAM v t @@ u)) /\ - (!v t p. p is_head_redex t ==> (In::p) is_head_redex (LAM v t)) /\ - (!t u v p. p is_head_redex (t @@ u) ==> - (Lt::p) is_head_redex (t @@ u) @@ v) - `; - -val ihr_bvc_ind = store_thm( - "ihr_bvc_ind", - ``!P X. FINITE X /\ - (!v M N. ~(v IN X) /\ ~(v IN FV N) ==> P [] (LAM v M @@ N)) /\ - (!v M p. ~(v IN X) /\ P p M ==> P (In::p) (LAM v M)) /\ - (!M N L p. P p (M @@ N) ==> P (Lt::p) ((M @@ N) @@ L)) ==> - !p M. p is_head_redex M ==> P p M``, - REPEAT GEN_TAC THEN STRIP_TAC THEN - Q_TAC SUFF_TAC `!p M. p is_head_redex M ==> !pi. P p (tpm pi M)` - THEN1 METIS_TAC [pmact_nil] THEN - HO_MATCH_MP_TAC is_head_redex_ind THEN - SRW_TAC [][is_head_redex_rules] THENL [ - Q.MATCH_ABBREV_TAC `P [] (LAM vv MM @@ NN)` THEN - markerLib.RM_ALL_ABBREVS_TAC THEN - Q_TAC (NEW_TAC "z") `FV MM UNION FV NN UNION X` THEN - `LAM vv MM = LAM z (tpm [(z,vv)] MM)` by SRW_TAC [][tpm_ALPHA] THEN - SRW_TAC [][], - Q.MATCH_ABBREV_TAC `P (In::p) (LAM vv MM)` THEN - Q_TAC (NEW_TAC "z") `FV MM UNION X` THEN - `LAM vv MM = LAM z (tpm [(z,vv)] MM)` by SRW_TAC [][tpm_ALPHA] THEN - SRW_TAC [][GSYM pmact_decompose, Abbr`MM`] - ]); - -val is_head_redex_subst_invariant = store_thm( - "is_head_redex_subst_invariant", - ``!p t u v. p is_head_redex t ==> p is_head_redex [u/v] t``, - REPEAT GEN_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`t`, `p`] THEN - HO_MATCH_MP_TAC ihr_bvc_ind THEN Q.EXISTS_TAC `v INSERT FV u` THEN - SRW_TAC [][SUB_THM, SUB_VAR, is_head_redex_rules]); - -val is_head_redex_tpm_invariant = Store_Thm( - "is_head_redex_tpm_invariant", - ``p is_head_redex (tpm pi t) = p is_head_redex t``, - Q_TAC SUFF_TAC `!p t. p is_head_redex t ==> !pi. p is_head_redex (tpm pi t)` - THEN1 METIS_TAC [pmact_inverse] THEN - HO_MATCH_MP_TAC is_head_redex_ind THEN SRW_TAC [][is_head_redex_rules]); - -val is_head_redex_unique = store_thm( - "is_head_redex_unique", - ``!t p1 p2. p1 is_head_redex t /\ p2 is_head_redex t ==> (p1 = p2)``, - Q_TAC SUFF_TAC - `!p1 t. p1 is_head_redex t ==> !p2. p2 is_head_redex t ==> (p1 = p2)` - THEN1 PROVE_TAC [] THEN - HO_MATCH_MP_TAC is_head_redex_ind THEN REPEAT STRIP_TAC THEN - POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC [is_head_redex_cases] THEN - SRW_TAC [][LAM_eq_thm]); - -val is_head_redex_thm = store_thm( - "is_head_redex_thm", - ``(p is_head_redex (LAM v t) = ?p0. (p = In::p0) /\ p0 is_head_redex t) /\ - (p is_head_redex (t @@ u) = (p = []) /\ is_abs t \/ - ?p0. (p = Lt::p0) /\ is_comb t /\ - p0 is_head_redex t) /\ - (p is_head_redex (VAR v) = F)``, - REPEAT CONJ_TAC THEN - SRW_TAC [][Once is_head_redex_cases, SimpLHS, LAM_eq_thm] THEN - SRW_TAC [][EQ_IMP_THM] THENL [ - PROVE_TAC [], - PROVE_TAC [is_abs_thm, term_CASES], - METIS_TAC [is_comb_thm, term_CASES] - ]); - -val head_redex_leftmost = store_thm( - "head_redex_leftmost", - ``!p t. p is_head_redex t ==> - !p'. p' IN redex_posns t ==> (p = p') \/ p < p'``, - HO_MATCH_MP_TAC is_head_redex_ind THEN - SRW_TAC [][redex_posns_thm, DISJ_IMP_THM]); - -val hnf_no_head_redex = store_thm( - "hnf_no_head_redex", - ``!t. hnf t = !p. ~(p is_head_redex t)``, - HO_MATCH_MP_TAC simple_induction THEN - SRW_TAC [][hnf_thm, is_head_redex_thm] THEN - Q.SPEC_THEN `t` STRUCT_CASES_TAC term_CASES THEN - SRW_TAC [][is_head_redex_thm]); - -val head_redex_is_redex = store_thm( - "head_redex_is_redex", - ``!p t. p is_head_redex t ==> p IN redex_posns t``, - HO_MATCH_MP_TAC is_head_redex_ind THEN - SRW_TAC [][redex_posns_thm]); - -val is_head_redex_vsubst_invariant = store_thm( - "is_head_redex_vsubst_invariant", - ``!t v x p. p is_head_redex ([VAR v/x] t) = p is_head_redex t``, - REPEAT GEN_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`p`, `t`] THEN - HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{x;v}` THEN - SRW_TAC [][is_head_redex_thm, SUB_THM, SUB_VAR]); - val _ = add_infix("is_internal_redex", 760, NONASSOC) (* definition 11.4.2 (i) *) val is_internal_redex_def = Define` @@ -1170,15 +1070,6 @@ val lemma11_4_6 = store_thm( ] ]); -val foldl_snoc = prove( - ``!l f x y. FOLDL f x (APPEND l [y]) = f (FOLDL f x l) y``, - Induct THEN SRW_TAC [][]); - -val combs_not_size_1 = prove( - ``(size M = 1) ==> ~is_comb M``, - Q.SPEC_THEN `M` STRUCT_CASES_TAC term_CASES THEN - SRW_TAC [][size_thm, size_nz]); - val cant_ireduce_to_atom = prove( ``!M N. (size N = 1) ==> ~(M i_reduce1 N)``, Q_TAC SUFF_TAC `!M r N. labelled_redn beta M r N ==> @@ -1212,124 +1103,6 @@ val i_reduce_to_LAM_underneath = prove( PROVE_TAC [labelled_redn_rules] ]); -Definition LAMl_def: - LAMl vs (t : term) = FOLDR LAM t vs -End - -Theorem LAMl_thm[simp]: - (LAMl [] M = M) /\ - (LAMl (h::t) M = LAM h (LAMl t M)) -Proof SRW_TAC [][LAMl_def] -QED - -Theorem LAMl_11[simp]: - !vs. (LAMl vs x = LAMl vs y) = (x = y) -Proof - Induct THEN SRW_TAC [][] -QED - -Theorem size_LAMl[simp]: - !vs. size (LAMl vs M) = LENGTH vs + size M -Proof - Induct THEN SRW_TAC [numSimps.ARITH_ss][size_thm] -QED - -Theorem LAMl_eq_VAR[simp]: - (LAMl vs M = VAR v) ⇔ (vs = []) ∧ (M = VAR v) -Proof - Cases_on ‘vs’ >> simp[] -QED - -Theorem LAMl_eq_APP[simp]: - (LAMl vs M = N @@ P) ⇔ (vs = []) ∧ (M = N @@ P) -Proof - Cases_on ‘vs’ >> simp[] -QED - -Theorem LAMl_eq_appstar: - (LAMl vs M = N ·· Ns) ⇔ - (vs = []) ∧ (M = N ·· Ns) ∨ (Ns = []) ∧ (N = LAMl vs M) -Proof - Cases_on ‘vs’ >> simp[] >> Cases_on ‘Ns’ >> simp[] >> - metis_tac[] -QED - -Theorem is_abs_LAMl[simp]: - is_abs (LAMl vs M) ⇔ vs ≠ [] ∨ is_abs M -Proof - Cases_on ‘vs’ >> simp[] -QED - -val LAMl_vsub = store_thm( - "LAMl_vsub", - ``!vs u v M. - ~MEM u vs /\ ~MEM v vs ==> - ([VAR v/u] (LAMl vs M) = LAMl vs ([VAR v/u] M))``, - Induct THEN SRW_TAC [][] THEN - Q_TAC (NEW_TAC "z") `LIST_TO_SET vs UNION {h;v;u} UNION FV (LAMl vs M) UNION - FV (LAMl vs ([VAR v/u] M))` THEN - `LAM h (LAMl vs M) = LAM z ([VAR z/h] (LAMl vs M))` - by SRW_TAC [][SIMPLE_ALPHA] THEN - `LAM h (LAMl vs ([VAR v/u] M)) = LAM z ([VAR z/h] (LAMl vs ([VAR v/u] M)))` - by SRW_TAC [][SIMPLE_ALPHA] THEN - SRW_TAC [][SUB_THM]); - -val FV_LAMl = store_thm( - "FV_LAMl", - ``!vs M. FV (LAMl vs M) = FV M DIFF LIST_TO_SET vs``, - Induct THEN SRW_TAC [][] THEN - SIMP_TAC (srw_ss()) [EXTENSION] THEN PROVE_TAC []); - -val LAMl_vsub_disappears = store_thm( - "LAMl_vsub_disappears", - ``!vs u v M. MEM u vs ==> ([VAR v/u] (LAMl vs M) = LAMl vs M)``, - Induct THEN SRW_TAC [][] THENL [ - SRW_TAC [][SUB_THM, lemma14b], - `~(u IN FV (LAMl vs M))` by SRW_TAC [][FV_LAMl] THEN - `LAM h (LAMl vs M) = LAM u ([VAR u/h] (LAMl vs M))` - by SRW_TAC [][SIMPLE_ALPHA] THEN - SRW_TAC [][SUB_THM, lemma14b] - ]); - -val SUB_ISUB_SINGLETON = store_thm( - "SUB_ISUB_SINGLETON", - ``!t x u. [t/x]u:term = u ISUB [(t,x)]``, - SRW_TAC [][ISUB_def]); - -val ISUB_APPEND = store_thm( - "ISUB_APPEND", - ``!R1 R2 t:term. (t ISUB R1) ISUB R2 = t ISUB (APPEND R1 R2)``, - Induct THEN - ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, ISUB_def]); - -val LAMl_ALPHA = store_thm( - "LAMl_ALPHA", - ``!vs vs' M. - (LENGTH vs = LENGTH vs') /\ ALL_DISTINCT vs' /\ - DISJOINT (LIST_TO_SET vs') (LIST_TO_SET vs UNION FV M) ==> - (LAMl vs M = LAMl vs' (M ISUB REVERSE (ZIP(MAP VAR vs', vs))))``, - Induct THENL [ - SRW_TAC [][] THEN - FULL_SIMP_TAC (srw_ss()) [ISUB_def], - SRW_TAC [][] THEN - Cases_on `vs'` THEN - FULL_SIMP_TAC (srw_ss()) [DISJ_IMP_THM, FORALL_AND_THM] THEN - `~(h' IN LIST_TO_SET vs) /\ ~(h' IN FV M) /\ - DISJOINT (LIST_TO_SET vs) (LIST_TO_SET t) /\ - DISJOINT (FV M) (LIST_TO_SET t)` - by PROVE_TAC [DISJOINT_INSERT, DISJOINT_SYM] THEN - Q_TAC SUFF_TAC `~(h' IN FV (LAMl vs M)) /\ - (LAMl t (M ISUB APPEND (REVERSE (ZIP (MAP VAR t, vs))) - [(VAR h',h)]) = - [VAR h'/h] (LAMl vs M))` THEN1 - SRW_TAC [][SIMPLE_ALPHA] THEN - ASM_SIMP_TAC (srw_ss()) [FV_LAMl] THEN - FIRST_X_ASSUM (Q.SPECL_THEN [`t`, `M`] MP_TAC) THEN - ASM_SIMP_TAC (srw_ss()) [] THEN - DISCH_THEN (K ALL_TAC) THEN - SRW_TAC [][LAMl_vsub, SUB_ISUB_SINGLETON, ISUB_APPEND] - ]); - val FRESH_lists = store_thm( "FRESH_lists", ``!n s : string set. @@ -1376,50 +1149,6 @@ val RENAMING_ZIP_MAP_VAR = store_thm( val _ = augment_srw_ss [rewrites [RENAMING_REVERSE, RENAMING_ZIP_MAP_VAR]] -val is_comb_LAMl = store_thm( - "is_comb_LAMl", - ``is_comb (LAMl vs M) = (vs = []) /\ is_comb M``, - Cases_on `vs` THEN SRW_TAC [][]); -val _ = export_rewrites ["is_comb_LAMl"] - -val strange_cases = prove( - ``!M : term. (?vs M'. (M = LAMl vs M') /\ (size M' = 1)) \/ - (?vs args t. - (M = LAMl vs (FOLDL APP t args)) /\ - ~(args = []) /\ ~is_comb t)``, - HO_MATCH_MP_TAC simple_induction THEN REPEAT CONJ_TAC THENL [ - (* VAR *) GEN_TAC THEN DISJ1_TAC THEN - MAP_EVERY Q.EXISTS_TAC [`[]`, `VAR s`] THEN SRW_TAC [][size_thm], - (* app *) MAP_EVERY Q.X_GEN_TAC [`M`,`N`] THEN - DISCH_THEN (CONJUNCTS_THEN ASSUME_TAC) THEN - DISJ2_TAC THEN Q.EXISTS_TAC `[]` THEN - SIMP_TAC (srw_ss()) [] THEN - `(?vs M'. (M = LAMl vs M') /\ (size M' = 1)) \/ - (?vs args t. - (M = LAMl vs (FOLDL APP t args)) /\ ~(args = []) /\ - ~is_comb t)` by PROVE_TAC [] - THENL [ - MAP_EVERY Q.EXISTS_TAC [`[N]`, `M`] THEN - ASM_SIMP_TAC (srw_ss()) [] THEN - PROVE_TAC [combs_not_size_1], - ASM_SIMP_TAC (srw_ss()) [] THEN - Cases_on `vs` THENL [ - MAP_EVERY Q.EXISTS_TAC [`APPEND args [N]`, `t`] THEN - ASM_SIMP_TAC (srw_ss()) [foldl_snoc], - MAP_EVERY Q.EXISTS_TAC [`[N]`, `M`] THEN - ASM_SIMP_TAC (srw_ss()) [] - ] - ], - (* LAM *) MAP_EVERY Q.X_GEN_TAC [`x`,`M`] THEN STRIP_TAC THENL [ - DISJ1_TAC THEN - MAP_EVERY Q.EXISTS_TAC [`x::vs`, `M'`] THEN - ASM_SIMP_TAC (srw_ss()) [], - DISJ2_TAC THEN - MAP_EVERY Q.EXISTS_TAC [`x::vs`, `args`, `t`] THEN - ASM_SIMP_TAC (srw_ss()) [] - ] - ]); - val head_reduction_standard = store_thm( "head_reduction_standard", ``!s. is_head_reduction s ==> standard_reduction s``, @@ -2383,7 +2112,7 @@ val hnf_reflected_over_ireduction = store_thm( SRW_TAC [][hnf_no_head_redex, i_reduce1_def] THEN METIS_TAC [lemma11_4_3ii]); -(* NOTE: this is also Theorem 8.3.11 [1, p. 174] *) +(* NOTE: This is also Theorem 8.3.11 [1, p.174] *) val corollary11_4_8 = store_thm( "corollary11_4_8", ``!M. has_hnf M = finite (head_reduction_path M)``, @@ -2433,130 +2162,6 @@ val has_bnf_whnf = store_thm( ``has_bnf M ⇒ has_whnf M``, METIS_TAC [has_bnf_hnf, has_hnf_whnf]); -(*---------------------------------------------------------------------------* - * More results about LAMl (added by Chun Tian) - *---------------------------------------------------------------------------*) - -(* copied from chap2Script.sml *) -fun betafy ss = - simpLib.add_relsimp {refl = GEN_ALL lameq_refl, - trans = List.nth(CONJUNCTS lameq_rules, 3), - weakenings = [lameq_weaken_cong], - subsets = [], - rewrs = [hd (CONJUNCTS lameq_rules)]} ss ++ - simpLib.SSFRAG {rewrs = [], - ac = [], convs = [], - congs = [lameq_app_cong, - SPEC_ALL (last (CONJUNCTS lameq_rules)), - lameq_sub_cong], - dprocs = [], filter = NONE, name = NONE}; - -Theorem LAMl_SUB : - !M N v vs. ALL_DISTINCT vs /\ ~MEM v vs /\ (FV N = {}) ==> - [N/v] (LAMl vs M) == LAMl vs ([N/v] M) -Proof - rpt STRIP_TAC - >> Induct_on ‘vs’ >> rw [] - >> ASM_SIMP_TAC (betafy (srw_ss())) [] -QED - -Theorem LAMl_appstar : - !vs M Ns. ALL_DISTINCT vs /\ (LENGTH vs = LENGTH Ns) /\ EVERY closed Ns ==> - LAMl vs M @* Ns == (FEMPTY |++ ZIP (vs,Ns)) ' M -Proof - rpt STRIP_TAC - >> NewQ.ABBREV_TAC ‘L = ZIP (vs,Ns)’ - >> ‘(Ns = MAP SND L) /\ (vs = MAP FST L)’ by rw [Abbr ‘L’, MAP_ZIP] - >> FULL_SIMP_TAC std_ss [] - >> Q.PAT_X_ASSUM ‘EVERY closed (MAP SND L)’ MP_TAC - >> Q.PAT_X_ASSUM ‘ALL_DISTINCT (MAP FST L)’ MP_TAC - >> KILL_TAC - >> Q.ID_SPEC_TAC ‘M’ - >> Induct_on ‘L’ >> rw [] - >- (Suff ‘FEMPTY |++ [] = FEMPTY :string |-> term’ >- rw [] \\ - rw [FUPDATE_LIST_EQ_FEMPTY]) - >> NewQ.ABBREV_TAC ‘v = FST h’ - >> NewQ.ABBREV_TAC ‘vs = MAP FST L’ - >> NewQ.ABBREV_TAC ‘N = SND h’ - >> NewQ.ABBREV_TAC ‘Ns = MAP SND L’ - (* RHS rewriting *) - >> ‘h :: L = [h] ++ L’ by rw [] >> POP_ORW - >> rw [FUPDATE_LIST_APPEND] - >> Know ‘FEMPTY |++ [h] |++ L = FEMPTY |++ L |++ [h]’ - >- (MATCH_MP_TAC FUPDATE_LIST_APPEND_COMMUTES \\ - rw [DISJOINT_ALT]) - >> Rewr' - >> rw [GSYM FUPDATE_EQ_FUPDATE_LIST] - >> NewQ.ABBREV_TAC ‘fm = FEMPTY |++ L’ - >> FULL_SIMP_TAC std_ss [] - >> ‘h = (v,N)’ by rw [Abbr ‘v’, Abbr ‘N’] >> POP_ORW - >> Know ‘(fm |+ (v,N)) ' M = fm ' ([N/v] M)’ - >- (MATCH_MP_TAC ssub_update_apply' \\ - Q.PAT_X_ASSUM ‘closed N’ MP_TAC \\ - rw [Abbr ‘fm’, FDOM_FUPDATE_LIST, closed_def] \\ - Cases_on ‘INDEX_OF y vs’ >- fs [INDEX_OF_eq_NONE] \\ - rename1 ‘INDEX_OF y vs = SOME n’ \\ - fs [INDEX_OF_eq_SOME] \\ - Q.PAT_X_ASSUM ‘EL n vs = y’ (ONCE_REWRITE_TAC o wrap o SYM) \\ - ‘LENGTH L = LENGTH vs’ by rw [Abbr ‘vs’, LENGTH_MAP] \\ - Know ‘(FEMPTY |++ L) ' (EL n vs) = EL n Ns’ - >- (MATCH_MP_TAC FUPDATE_LIST_APPLY_MEM \\ - Q.EXISTS_TAC ‘n’ >> rw [] \\ - ‘m <> n’ by rw [] \\ - METIS_TAC [EL_ALL_DISTINCT_EL_EQ]) >> Rewr' \\ - Q.PAT_X_ASSUM ‘EVERY closed Ns’ MP_TAC \\ - rw [EVERY_MEM, closed_def] \\ - POP_ASSUM MATCH_MP_TAC >> rw [MEM_EL] \\ - ‘LENGTH L = LENGTH Ns’ by rw [Abbr ‘Ns’, LENGTH_MAP] \\ - Q.EXISTS_TAC ‘n’ >> rw []) - >> Rewr' - (* LHS rewriting *) - >> Know ‘LAM v (LAMl vs M) @@ N == LAMl vs ([N/v] M)’ - >- (SIMP_TAC (betafy (srw_ss())) [] \\ - MATCH_MP_TAC LAMl_SUB \\ - Q.PAT_X_ASSUM ‘closed N’ MP_TAC >> rw [closed_def]) - >> DISCH_TAC - >> MATCH_MP_TAC lameq_TRANS - >> Q.EXISTS_TAC ‘LAMl vs ([N/v] M) @* Ns’ >> art [] - >> MATCH_MP_TAC lameq_appstar_cong >> art [] -QED - -Theorem hnf_LAMl[simp] : - hnf (LAMl vs M) <=> hnf M -Proof - Induct_on ‘vs’ >> rw [] -QED - -Theorem is_abs_appstar[simp]: - is_abs (M @* Ns) ⇔ is_abs M ∧ (Ns = []) -Proof - Induct_on ‘Ns’ using SNOC_INDUCT >> - simp[appstar_SNOC] -QED - -Theorem hnf_appstar : - !M Ns. hnf (M @* Ns) <=> hnf M /\ (is_abs M ⇒ (Ns = [])) -Proof - Induct_on ‘Ns’ using SNOC_INDUCT >> simp[appstar_SNOC] >> - dsimp[SF CONJ_ss] >> metis_tac[] -QED - -Theorem hnf_cases : - !M : term. hnf M <=> ?vs args y. M = LAMl vs (VAR y @* args) -Proof - simp[FORALL_AND_THM, EQ_IMP_THM] >> conj_tac - >- (gen_tac >> MP_TAC (Q.SPEC ‘M’ strange_cases) - >> RW_TAC std_ss [] - >- (FULL_SIMP_TAC std_ss [size_1] \\ - qexistsl_tac [‘vs’, ‘[]’, ‘y’] >> rw []) - >> FULL_SIMP_TAC std_ss [hnf_LAMl] - >> ‘hnf t /\ ~is_abs t’ by PROVE_TAC [hnf_appstar] - >> ‘is_var t’ by METIS_TAC [term_cases] - >> FULL_SIMP_TAC std_ss [is_var_cases] - >> qexistsl_tac [‘vs’, ‘args’, ‘y’] >> art []) >> - simp[PULL_EXISTS, hnf_appstar] -QED - (* Proposition 8.3.13 (i) [1, p.174] *) Theorem has_hnf_iff_LAM[simp] : !x M. has_hnf (LAM x M) <=> has_hnf M @@ -2566,7 +2171,6 @@ Proof >> rpt STRIP_TAC >- (Q.EXISTS_TAC ‘LAM x N’ \\ CONJ_TAC >- PROVE_TAC [lameq_rules] \\ - ‘?vs args y. N = LAMl vs (VAR y @* args)’ by METIS_TAC [hnf_cases] \\ rw [hnf_cases]) (* stage work *) >> ‘?Z. LAM x M -b->* Z /\ N -b->* Z’ by METIS_TAC [lameq_CR] diff --git a/examples/lambda/basics/appFOLDLScript.sml b/examples/lambda/basics/appFOLDLScript.sml index b5f8605a1a..1ed781fd8c 100644 --- a/examples/lambda/basics/appFOLDLScript.sml +++ b/examples/lambda/basics/appFOLDLScript.sml @@ -1,9 +1,8 @@ -open HolKernel Parse boolLib bossLib +open HolKernel Parse boolLib bossLib; -open arithmeticTheory listTheory -open termTheory +open arithmeticTheory listTheory pred_setTheory hurdUtils; -fun Store_thm(trip as (n,t,tac)) = store_thm trip before export_rewrites [n] +open termTheory binderLib; val _ = new_theory "appFOLDL" @@ -174,4 +173,134 @@ Proof Induct_on ‘Ns’ using SNOC_INDUCT >> simp[appstar_SNOC, MAP_SNOC] QED +(*---------------------------------------------------------------------------* + * LAMl (was in standardisationTheory) + *---------------------------------------------------------------------------*) + +Definition LAMl_def: + LAMl vs (t : term) = FOLDR LAM t vs +End + +Theorem LAMl_thm[simp]: + (LAMl [] M = M) /\ + (LAMl (h::t) M = LAM h (LAMl t M)) +Proof SRW_TAC [][LAMl_def] +QED + +Theorem LAMl_11[simp]: + !vs. (LAMl vs x = LAMl vs y) = (x = y) +Proof + Induct THEN SRW_TAC [][] +QED + +Theorem size_LAMl[simp]: + !vs. size (LAMl vs M) = LENGTH vs + size M +Proof + Induct THEN SRW_TAC [numSimps.ARITH_ss][size_thm] +QED + +Theorem FV_LAMl : + !vs M. FV (LAMl vs M) = FV M DIFF LIST_TO_SET vs +Proof + Induct THEN SRW_TAC [][] THEN + SIMP_TAC (srw_ss()) [EXTENSION] THEN PROVE_TAC [] +QED + +Theorem LAMl_eq_VAR[simp]: + (LAMl vs M = VAR v) ⇔ (vs = []) ∧ (M = VAR v) +Proof + Cases_on ‘vs’ >> simp[] +QED + +Theorem LAMl_eq_APP[simp]: + (LAMl vs M = N @@ P) ⇔ (vs = []) ∧ (M = N @@ P) +Proof + Cases_on ‘vs’ >> simp[] +QED + +Theorem LAMl_eq_appstar: + (LAMl vs M = N ·· Ns) ⇔ + (vs = []) ∧ (M = N ·· Ns) ∨ (Ns = []) ∧ (N = LAMl vs M) +Proof + Cases_on ‘vs’ >> simp[] >> Cases_on ‘Ns’ >> simp[] >> + metis_tac[] +QED + +Theorem LAMl_SUB : + !M N v vs. ALL_DISTINCT vs /\ ~MEM v vs /\ (FV N = {}) ==> + ([N/v] (LAMl vs M) = LAMl vs ([N/v] M)) +Proof + rpt STRIP_TAC + >> Induct_on ‘vs’ >> rw [] +QED + +Theorem tpm_LAMl: + tpm π (LAMl vs M) = LAMl (listpm string_pmact π vs) (tpm π M) +Proof + Induct_on ‘vs’ >> simp[] +QED + +Theorem tpm_appstar: + tpm π (M ·· Ms) = tpm π M ·· listpm term_pmact π Ms +Proof + qid_spec_tac ‘M’ >> Induct_on ‘Ms’ >> simp[] +QED + +Theorem LAMl_vsub : + !vs u v M. + ~MEM u vs /\ ~MEM v vs ==> + ([VAR v/u] (LAMl vs M) = LAMl vs ([VAR v/u] M)) +Proof + Induct THEN SRW_TAC [][] THEN + Q_TAC (NEW_TAC "z") `LIST_TO_SET vs UNION {h;v;u} UNION FV (LAMl vs M) UNION + FV (LAMl vs ([VAR v/u] M))` THEN + `LAM h (LAMl vs M) = LAM z ([VAR z/h] (LAMl vs M))` + by SRW_TAC [][SIMPLE_ALPHA] THEN + `LAM h (LAMl vs ([VAR v/u] M)) = LAM z ([VAR z/h] (LAMl vs ([VAR v/u] M)))` + by SRW_TAC [][SIMPLE_ALPHA] THEN + SRW_TAC [][SUB_THM] +QED + +Theorem LAMl_vsub_disappears : + !vs u v M. MEM u vs ==> ([VAR v/u] (LAMl vs M) = LAMl vs M) +Proof + Induct THEN SRW_TAC [][] THENL [ + SRW_TAC [][SUB_THM, lemma14b], + `~(u IN FV (LAMl vs M))` by SRW_TAC [][FV_LAMl] THEN + `LAM h (LAMl vs M) = LAM u ([VAR u/h] (LAMl vs M))` + by SRW_TAC [][SIMPLE_ALPHA] THEN + SRW_TAC [][SUB_THM, lemma14b] + ] +QED + +Theorem LAMl_ALPHA : + !vs vs' M. + (LENGTH vs = LENGTH vs') /\ ALL_DISTINCT vs' /\ + DISJOINT (LIST_TO_SET vs') (LIST_TO_SET vs UNION FV M) ==> + (LAMl vs M = LAMl vs' (M ISUB REVERSE (ZIP(MAP VAR vs', vs)))) +Proof + Induct THENL [ + SRW_TAC [][] THEN + FULL_SIMP_TAC (srw_ss()) [ISUB_def], + SRW_TAC [][] THEN + Cases_on `vs'` THEN + FULL_SIMP_TAC (srw_ss()) [DISJ_IMP_THM, FORALL_AND_THM] THEN + `~(h' IN LIST_TO_SET vs) /\ ~(h' IN FV M) /\ + DISJOINT (LIST_TO_SET vs) (LIST_TO_SET t) /\ + DISJOINT (FV M) (LIST_TO_SET t)` + by PROVE_TAC [DISJOINT_INSERT, DISJOINT_SYM] THEN + Q_TAC SUFF_TAC `~(h' IN FV (LAMl vs M)) /\ + (LAMl t (M ISUB APPEND (REVERSE (ZIP (MAP VAR t, vs))) + [(VAR h',h)]) = + [VAR h'/h] (LAMl vs M))` THEN1 + SRW_TAC [][SIMPLE_ALPHA] THEN + ASM_SIMP_TAC (srw_ss()) [FV_LAMl] THEN + FIRST_X_ASSUM (Q.SPECL_THEN [`t`, `M`] MP_TAC) THEN + ASM_SIMP_TAC (srw_ss()) [] THEN + DISCH_THEN (K ALL_TAC) THEN + SRW_TAC [][LAMl_vsub, SUB_ISUB_SINGLETON, ISUB_APPEND] + ] +QED + val _ = export_theory () +val _ = html_theory "appFOLDL"; diff --git a/examples/lambda/basics/nomsetScript.sml b/examples/lambda/basics/nomsetScript.sml index 1b21b35f1b..303ce92367 100644 --- a/examples/lambda/basics/nomsetScript.sml +++ b/examples/lambda/basics/nomsetScript.sml @@ -557,6 +557,13 @@ val MEM_listpm_EXISTS = store_thm( val _ = overload_on("cpm_pmact", ``list_pmact (pair_pmact string_pmact string_pmact)``); val _ = overload_on ("cpmpm", ``pmact cpm_pmact``); +(* moved here from sttScript.sml *) +Theorem ALL_DISTINCT_listpm[simp]: + ALL_DISTINCT (listpm act π xs) = ALL_DISTINCT xs +Proof + Induct_on ‘xs’ >> simp[MEM_listpm] +QED + (* ---------------------------------------------------------------------- Notion of support, and calculating the smallest set of support ---------------------------------------------------------------------- *) diff --git a/examples/lambda/basics/termScript.sml b/examples/lambda/basics/termScript.sml index 468cf0d060..91a012b892 100644 --- a/examples/lambda/basics/termScript.sml +++ b/examples/lambda/basics/termScript.sml @@ -305,6 +305,14 @@ val FV_tpm = Save_thm("FV_tpm", val _ = set_mapped_fixity { term_name = "APP", tok = "@@", fixity = Infixl 901} +(* NOTE: The following overload "incompatible" was in sttScript.sml. + + The current "incompatibility" is between a (string) variable and a term. + See chap2Theory for the incompatibility bwtween two terms. + *) +val _ = set_fixity "#" (Infix(NONASSOC, 450)) +Overload "#" = “λv M:term. v ∉ FV M” + Theorem FRESH_APP[simp]: v NOTIN FV (M @@ N) <=> v NOTIN FV M /\ v NOTIN FV N Proof SRW_TAC [][] QED @@ -570,7 +578,7 @@ QED Theorem size_nz = REWRITE_RULE [GSYM arithmeticTheory.NOT_ZERO_LT_ZERO] size_nonzero -Theorem size_1 : +Theorem size_1_cases : (size M = 1) <=> ?y. (M = VAR y) Proof Q.SPEC_THEN `M` STRUCT_CASES_TAC term_CASES @@ -620,6 +628,17 @@ val ISUB_LAM = store_thm( ASM_SIMP_TAC (srw_ss()) [ISUB_def, pairTheory.FORALL_PROD, DOM_DEF, FVS_DEF, SUB_THM]); +val SUB_ISUB_SINGLETON = store_thm( + "SUB_ISUB_SINGLETON", + ``!t x u. [t/x]u:term = u ISUB [(t,x)]``, + SRW_TAC [][ISUB_def]); + +val ISUB_APPEND = store_thm( + "ISUB_APPEND", + ``!R1 R2 t:term. (t ISUB R1) ISUB R2 = t ISUB (APPEND R1 R2)``, + Induct THEN + ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, ISUB_def]); + (* ---------------------------------------------------------------------- Simultaneous substitution (using a finite map) - much more interesting ---------------------------------------------------------------------- *) diff --git a/examples/lambda/typing/sttScript.sml b/examples/lambda/typing/sttScript.sml index b880aa4470..3904619a1f 100644 --- a/examples/lambda/typing/sttScript.sml +++ b/examples/lambda/typing/sttScript.sml @@ -335,75 +335,6 @@ val (ground_subterms_def, _) = define_recursive_term_function ‘ ’ val _ = export_rewrites ["ground_subterms_def"] -Theorem APP_EQ_LAMl[simp]: - M @@ N = LAMl vs P ⇔ vs = [] ∧ P = M @@ N -Proof - Cases_on ‘vs’ >> simp[] >> metis_tac[] -QED - -Theorem is_abs_appstar[simp]: - is_abs (M ·· Ms) ⇔ is_abs M ∧ Ms = [] -Proof - qid_spec_tac ‘M’ >> Induct_on ‘Ms’ >> simp[] -QED - -Theorem appstar_EQ_LAMl: - x ·· Ms = LAMl vs M ⇔ vs = [] ∧ M = x ·· Ms ∨ Ms = [] ∧ x = LAMl vs M -Proof - Cases_on ‘vs’ >> simp[] >> Cases_on ‘Ms’ >> simp[] >> metis_tac[] -QED - -Theorem tpm_LAMl: - tpm π (LAMl vs M) = LAMl (listpm string_pmact π vs) (tpm π M) -Proof - Induct_on ‘vs’ >> simp[] -QED - -Theorem tpm_appstar: - tpm π (M ·· Ms) = tpm π M ·· listpm term_pmact π Ms -Proof - qid_spec_tac ‘M’ >> Induct_on ‘Ms’ >> simp[] -QED - -Theorem ALL_DISTINCT_listpm[simp]: - ALL_DISTINCT (listpm act π xs) = ALL_DISTINCT xs -Proof - Induct_on ‘xs’ >> simp[MEM_listpm] -QED - -Theorem bnf_characterisation: - ∀M. - bnf M ⇔ - ∃vs v Ms. ALL_DISTINCT vs ∧ M = LAMl vs (VAR v ·· Ms) ∧ - (∀M. MEM M Ms ⇒ bnf M) -Proof - ho_match_mp_tac nc_INDUCTION2 >> qexists ‘∅’ >> rw[] >~ - [‘VAR _ ·· _ = M1 @@ M2’] - >- (simp[] >> eq_tac >> rpt strip_tac >~ - [‘M1 = LAMl vs1 _’, ‘M1 @@ M2’] - >- (gvs[app_eq_appstar] >> - Q.REFINE_EXISTS_TAC ‘SNOC M Mt’ >> - simp[DISJ_IMP_THM, rich_listTheory.FRONT_APPEND] >> - metis_tac[]) >> - Cases_on ‘Ms’ using rich_listTheory.SNOC_CASES >> - gvs[rich_listTheory.SNOC_APPEND, appstar_APPEND] >> - dsimp[appstar_EQ_LAMl] >> irule_at Any EQ_REFL >> simp[]) >> - pop_assum SUBST_ALL_TAC >> eq_tac >> rpt strip_tac >> gvs[] >~ - [‘LAM y (LAMl vs _)’] - >- (reverse (Cases_on ‘MEM y vs’) - >- (qexists ‘y::vs’ >> simp[]) >> - ‘y # LAMl vs (VAR v ·· Ms)’ by simp[FV_LAMl] >> - Q_TAC (NEW_TAC "z") ‘y INSERT set vs ∪ FV (VAR v ·· Ms)’ >> - ‘z # LAMl vs (VAR v ·· Ms)’ by simp[FV_LAMl] >> - dxrule_then (qspec_then ‘y’ mp_tac) tpm_ALPHA >> - simp[tpm_fresh, FV_LAMl] >> strip_tac >> qexists ‘z::vs’ >> simp[]) >> - rename [‘LAM y M = LAMl vs (VAR v ·· Ms)’] >> - Cases_on ‘vs’ >> gvs[] >> gvs[LAM_eq_thm] - >- metis_tac[] >> - simp[tpm_LAMl, tpm_appstar] >> irule_at Any EQ_REFL >> - simp[MEM_listpm] >> rpt strip_tac >> first_assum drule >> simp[] -QED - (*