From 418915e7bf952a6f354bbb952d8464de81e801ab Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Thu, 26 Oct 2023 10:33:39 +1100 Subject: [PATCH] [examples/lambda] Move more theorems earlier in development --- examples/lambda/barendregt/chap2Script.sml | 129 +++++++++++++----- .../lambda/barendregt/normal_orderScript.sml | 46 +++---- examples/lambda/typing/sttScript.sml | 96 +------------ 3 files changed, 115 insertions(+), 156 deletions(-) diff --git a/examples/lambda/barendregt/chap2Script.sml b/examples/lambda/barendregt/chap2Script.sml index 9cf3ffc599..dee506ea14 100644 --- a/examples/lambda/barendregt/chap2Script.sml +++ b/examples/lambda/barendregt/chap2Script.sml @@ -606,6 +606,22 @@ Proof SRW_TAC [][SUB_THM, SUB_VAR] QED +Theorem EQ_LAML_bodies_permute: + ∀us vs M N. (LAMl us M = LAMl vs N) ∧ ¬is_abs M ∧ ¬is_abs N ⇒ + ∃pi. N = tpm pi M +Proof + Induct >> simp[] + >- metis_tac[pmact_nil] >> + simp[] >> rpt gen_tac >> rename [‘LAM x (LAMl xs _) = LAMl ys _’] >> + Cases_on ‘ys’ >> simp[] >- (rw[] >> gvs[]) >> + rename [‘LAM x (LAMl xs M) = LAM y (LAMl ys N)’] >> + simp[LAM_eq_thm] >> rw[] >> gvs[tpm_LAMl] + >- metis_tac[] >> + first_x_assum drule >> simp[] >> rename [‘tpm [(a,b)] N = _’] >> + rw[] >> pop_assum (mp_tac o Q.AP_TERM ‘tpm [(a,b)]’) >> + REWRITE_TAC [pmact_sing_inv] >> metis_tac[pmact_decompose] +QED + val (is_var_thm, _) = define_recursive_term_function `(is_var (VAR s) = T) /\ (is_var (t1 @@ t2) = F) /\ @@ -635,6 +651,41 @@ Proof >> SRW_TAC [][] QED +Theorem term_laml_cases: + ∀X. FINITE X ⇒ + ∀t. (∃s. t = VAR s) ∨ (∃M1 M2. t = M1 @@ M2) ∨ + ∃v vs Body. t = LAM v (LAMl vs Body) ∧ ¬is_abs Body ∧ v ∉ X ∧ + ¬MEM v vs ∧ ALL_DISTINCT vs ∧ DISJOINT (set vs) X +Proof + gen_tac >> strip_tac >> ho_match_mp_tac nc_INDUCTION2 >> simp[] >> + qexists ‘X’ >> simp[] >> rw[] >~ + [‘LAM v (VAR u)’, ‘v ∉ X’] + >- (qexistsl [‘v’, ‘[]’, ‘VAR u’] >> simp[]) >~ + [‘LAM v (M1 @@ M2)’, ‘v ∉ X’] + >- (qexistsl [‘v’, ‘[]’, ‘M1 @@ M2’] >> simp[]) >~ + [‘LAM u (LAM v (LAMl vs Body))’, ‘u ∉ X’, ‘v ∉ X’] >> + Cases_on ‘u = v’ >> gvs[] + >- (Q_TAC (NEW_TAC "z") ‘u INSERT set vs ∪ FV Body ∪ X’ >> + ‘z # LAM u (LAMl vs Body)’ by simp[FV_LAMl] >> + drule_then (qspec_then ‘u’ assume_tac) SIMPLE_ALPHA >> simp[lemma14b] >> + qexistsl [‘z’, ‘u::vs’, ‘Body’] >> simp[]) >> + Cases_on ‘MEM u vs’ + >- (Q_TAC (NEW_TAC "z") ‘{u;v} ∪ set vs ∪ FV Body ∪ X’ >> + ‘z # LAM v (LAMl vs Body)’ by simp[FV_LAMl] >> + drule_then (qspec_then ‘u’ assume_tac) SIMPLE_ALPHA >> + simp[lemma14b, FV_LAMl] >> + qexistsl [‘z’, ‘v::vs’, ‘Body’] >> simp[]) >> + Q_TAC (NEW_TAC "z") ‘{u;v} ∪ set vs ∪ X ∪ FV Body’ >> + ‘z # LAM v (LAMl vs Body)’ by simp[FV_LAMl] >> + drule_then (qspec_then ‘u’ assume_tac) tpm_ALPHA >> simp[] >> + qexists ‘z’ >> Q.REFINE_EXISTS_TAC ‘x::xs’ >> simp[tpm_LAMl] >> + irule_at Any EQ_REFL >> simp[DISJOINT_DEF, EXTENSION, MEM_listpm] >> + qx_gen_tac ‘a’ >> Cases_on ‘a ∈ X’ >> simp[] >> + Cases_on ‘a = u’ >> gvs[] >> + Cases_on ‘a = z’ >> gvs[] >> + gvs[DISJOINT_DEF, EXTENSION] >> metis_tac[] +QED + val (bnf_thm, _) = define_recursive_term_function `(bnf (VAR s) <=> T) /\ (bnf (t1 @@ t2) <=> bnf t1 /\ bnf t2 /\ ~is_abs t1) /\ @@ -671,39 +722,55 @@ 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[] +Theorem bnf_LAMl[simp]: + bnf (LAMl vs M) = bnf M +Proof + Induct_on ‘vs’ >> simp[] QED +Theorem bnf_appstar[simp]: + ∀M Ns. bnf (M @* Ns) ⇔ bnf M ∧ (∀N. MEM N Ns ⇒ bnf N) ∧ (is_abs M ⇒ Ns = []) +Proof + Induct_on ‘Ns’ using listTheory.SNOC_INDUCT >> + simp[DISJ_IMP_THM, FORALL_AND_THM] >> metis_tac[] +QED + +Theorem bnf_characterisation_X: + ∀M X. FINITE X ⇒ + (bnf M ⇔ + ∃vs v Ms. DISJOINT (set vs) X ∧ M = LAMl vs (VAR v @* Ms) ∧ + ALL_DISTINCT vs ∧ ∀M. MEM M Ms ⇒ bnf M) +Proof + completeInduct_on ‘size M’ >> rw[] >> gvs[GSYM RIGHT_FORALL_IMP_THM] >> + drule_then (qspec_then ‘M’ strip_assume_tac) term_laml_cases >> simp[] >~ + [‘M1 @@ M2’] + >- (first_assum $ qspec_then ‘M1’ assume_tac >> + first_x_assum $ qspec_then ‘M2’ assume_tac >> gs[]>> + rpt (first_x_assum $ drule_then assume_tac) >> + simp[] >> iff_tac >> rw[] >> + gvs[app_eq_appstar_SNOC, LAMl_eq_appstar, DISJ_IMP_THM, FORALL_AND_THM] >> + dsimp[PULL_EXISTS] >> metis_tac[]) >~ + [‘LAM u $ LAMl us Body’] + >- (gvs[] >> + first_x_assum $ qspec_then ‘Body’ mp_tac >> simp[]>> + disch_then $ qspec_then ‘∅’ mp_tac >> simp[] >> + disch_then kall_tac >> + ‘∀xs M. Body = LAMl xs M ⇔ xs = [] ∧ M = Body’ + by (rpt gen_tac >> Cases_on ‘xs’ >> simp[] >- metis_tac[] >> + strip_tac >> gvs[]) >> + simp[] >> iff_tac >> rw[] + >- (qexistsl [‘u::us’, ‘v’, ‘Ms’] >> simp[]) >> + rename [‘LAM u (LAMl us Body) = LAMl vs (VAR v @* Ms)’] >> + ‘LAMl vs (VAR v @* Ms) = LAMl (u::us) Body’ by simp[] >> + drule EQ_LAML_bodies_permute >> + simp[PULL_EXISTS, tpm_appstar, MEM_listpm_EXISTS]) +QED + +Theorem bnf_characterisation = + MATCH_MP bnf_characterisation_X + (INST_TYPE [“:α” |-> “:string”] FINITE_EMPTY) + |> REWRITE_RULE [DISJOINT_EMPTY] + val _ = augment_srw_ss [rewrites [LAM_eq_thm]] val (rand_thm, _) = define_recursive_term_function `rand (t1 @@ t2) = t2`; val _ = export_rewrites ["rand_thm"] diff --git a/examples/lambda/barendregt/normal_orderScript.sml b/examples/lambda/barendregt/normal_orderScript.sml index 6f08fa949b..18c213e4ba 100644 --- a/examples/lambda/barendregt/normal_orderScript.sml +++ b/examples/lambda/barendregt/normal_orderScript.sml @@ -878,38 +878,24 @@ QED val normorder_strong_ind = IndDefLib.derive_strong_induction (normorder_rules,normorder_ind) -Theorem bnf_appstar[simp]: - ∀args f. - bnf (f ·· args) ⇔ bnf f ∧ EVERY bnf args ∧ (is_abs f ⇒ (args = [])) -Proof Induct THEN SRW_TAC [][] THEN METIS_TAC [] +Theorem norm_varhead0[local]: + ∀M N. M -n-> N ⇒ + ∀v Ms. (M = VAR v ·· Ms) ⇒ + ∃p s M0 N0. + (Ms = p ++ [M0] ++ s) ∧ + (N = VAR v ·· (p ++ [N0] ++ s)) ∧ + EVERY bnf p ∧ + M0 -n-> N0 +Proof + HO_MATCH_MP_TAC normorder_strong_ind >> + rw[lam_eq_appstar, app_eq_appstar_SNOC] >> + gvs[] + >- (REWRITE_TAC [GSYM listTheory.APPEND_ASSOC] >> + rpt $ irule_at Any EQ_REFL >> simp[]) >> + first_assum $ irule_at (Pat ‘_ -n-> _’) >> + simp[listTheory.EVERY_MEM] >> qexists ‘[]’ >> simp[] QED -val norm_varhead0 = prove( - ``∀M N. M -n-> N ⇒ - ∀v Ms. (M = VAR v ·· Ms) ⇒ - ∃p s M0 N0. - (Ms = p ++ [M0] ++ s) ∧ - (N = VAR v ·· (p ++ [N0] ++ s)) ∧ - EVERY bnf p ∧ - M0 -n-> N0``, - HO_MATCH_MP_TAC normorder_strong_ind THEN - SRW_TAC [][lam_eq_appstar, app_eq_varappstar] THENL [ - FIRST_X_ASSUM (Q.SPECL_THEN [`v`, `FRONT Ms`] MP_TAC) THEN - SRW_TAC [][] THEN - MAP_EVERY Q.EXISTS_TAC [`p`, `s ++ [LAST Ms]`, `M0`, `N0`] THEN - SRW_TAC [][rich_listTheory.FRONT_APPEND, listTheory.FRONT_DEF, - rich_listTheory.LAST_APPEND, listTheory.LAST_DEF] THEN - IMP_RES_TAC listTheory.APPEND_FRONT_LAST THEN - POP_ASSUM (fn th => REWRITE_TAC [Once (GSYM th)]) THEN - SRW_TAC [][] THEN - REWRITE_TAC [GSYM listTheory.APPEND_ASSOC, listTheory.APPEND], - - MAP_EVERY Q.EXISTS_TAC [`FRONT Ms`, `[]`, `LAST Ms`, `N`] THEN - SRW_TAC [][listTheory.APPEND_FRONT_LAST, rich_listTheory.FRONT_APPEND, - rich_listTheory.LAST_APPEND] THEN - FULL_SIMP_TAC (srw_ss()) [] - ]); - val norm_varhead = save_thm( "norm_varhead", SIMP_RULE (srw_ss() ++ DNF_ss) [] norm_varhead0); diff --git a/examples/lambda/typing/sttScript.sml b/examples/lambda/typing/sttScript.sml index 1a3ee8cf4c..c253081428 100644 --- a/examples/lambda/typing/sttScript.sml +++ b/examples/lambda/typing/sttScript.sml @@ -2,7 +2,7 @@ open HolKernel boolLib Parse bossLib open binderLib nomsetTheory metisLib termTheory contextlistsTheory open chap3Theory open sortingTheory -open appFOLDLTheory standardisationTheory +open appFOLDLTheory open pred_setTheory val _ = new_theory "stt"; @@ -443,100 +443,6 @@ Proof Induct_on ‘subterm’ >> simp[] QED -Theorem term_laml_cases: - ∀X. FINITE X ⇒ - ∀t. (∃s. t = VAR s) ∨ (∃M1 M2. t = M1 @@ M2) ∨ - ∃v vs Body. t = LAM v (LAMl vs Body) ∧ ¬is_abs Body ∧ v ∉ X ∧ - ¬MEM v vs ∧ ALL_DISTINCT vs ∧ DISJOINT (set vs) X -Proof - gen_tac >> strip_tac >> ho_match_mp_tac nc_INDUCTION2 >> simp[] >> - qexists ‘X’ >> simp[] >> rw[] >~ - [‘LAM v (VAR u)’, ‘v ∉ X’] - >- (qexistsl [‘v’, ‘[]’, ‘VAR u’] >> simp[]) >~ - [‘LAM v (M1 @@ M2)’, ‘v ∉ X’] - >- (qexistsl [‘v’, ‘[]’, ‘M1 @@ M2’] >> simp[]) >~ - [‘LAM u (LAM v (LAMl vs Body))’, ‘u ∉ X’, ‘v ∉ X’] >> - Cases_on ‘u = v’ >> gvs[] - >- (Q_TAC (NEW_TAC "z") ‘u INSERT set vs ∪ FV Body ∪ X’ >> - ‘z # LAM u (LAMl vs Body)’ by simp[FV_LAMl] >> - drule_then (qspec_then ‘u’ assume_tac) SIMPLE_ALPHA >> simp[lemma14b] >> - qexistsl [‘z’, ‘u::vs’, ‘Body’] >> simp[]) >> - Cases_on ‘MEM u vs’ - >- (Q_TAC (NEW_TAC "z") ‘{u;v} ∪ set vs ∪ FV Body ∪ X’ >> - ‘z # LAM v (LAMl vs Body)’ by simp[FV_LAMl] >> - drule_then (qspec_then ‘u’ assume_tac) SIMPLE_ALPHA >> - simp[lemma14b, FV_LAMl] >> - qexistsl [‘z’, ‘v::vs’, ‘Body’] >> simp[]) >> - Q_TAC (NEW_TAC "z") ‘{u;v} ∪ set vs ∪ X ∪ FV Body’ >> - ‘z # LAM v (LAMl vs Body)’ by simp[FV_LAMl] >> - drule_then (qspec_then ‘u’ assume_tac) tpm_ALPHA >> simp[] >> - qexists ‘z’ >> Q.REFINE_EXISTS_TAC ‘x::xs’ >> simp[tpm_LAMl] >> - irule_at Any EQ_REFL >> simp[DISJOINT_DEF, EXTENSION, MEM_listpm] >> - qx_gen_tac ‘a’ >> Cases_on ‘a ∈ X’ >> simp[] >> - Cases_on ‘a = u’ >> gvs[] >> - Cases_on ‘a = z’ >> gvs[] >> - gvs[DISJOINT_DEF, EXTENSION] >> metis_tac[] -QED - -Theorem bnf_LAMl[simp]: - bnf (LAMl vs M) = bnf M -Proof - Induct_on ‘vs’ >> simp[] -QED - -Theorem EQ_LAML_E: - ∀us vs M N. (LAMl us M = LAMl vs N) ∧ ¬is_abs M ∧ ¬is_abs N ⇒ - ∃pi. N = tpm pi M -Proof - Induct >> simp[] - >- metis_tac[pmact_nil] >> - simp[] >> rpt gen_tac >> rename [‘LAM x (LAMl xs _) = LAMl ys _’] >> - Cases_on ‘ys’ >> simp[] >- (rw[] >> gvs[]) >> - rename [‘LAM x (LAMl xs M) = LAM y (LAMl ys N)’] >> - simp[LAM_eq_thm] >> rw[] >> gvs[tpm_LAMl] - >- metis_tac[] >> - first_x_assum drule >> simp[] >> rename [‘tpm [(a,b)] N = _’] >> - rw[] >> pop_assum (mp_tac o Q.AP_TERM ‘tpm [(a,b)]’) >> - REWRITE_TAC [pmact_sing_inv] >> metis_tac[pmact_decompose] -QED - -Theorem bnf_characterisation': - ∀M X. FINITE X ⇒ - (bnf M ⇔ - ∃vs v Ms. DISJOINT (set vs) X ∧ M = LAMl vs (VAR v @* Ms) ∧ - ALL_DISTINCT vs ∧ ∀M. MEM M Ms ⇒ bnf M) -Proof - completeInduct_on ‘size M’ >> rw[] >> gvs[GSYM RIGHT_FORALL_IMP_THM] >> - drule_then (qspec_then ‘M’ strip_assume_tac) term_laml_cases >> simp[] >~ - [‘M1 @@ M2’] - >- (first_assum $ qspec_then ‘M1’ assume_tac >> - first_x_assum $ qspec_then ‘M2’ assume_tac >> gs[]>> - rpt (first_x_assum $ drule_then assume_tac) >> - simp[] >> iff_tac >> rw[] >> - gvs[app_eq_appstar_SNOC, LAMl_eq_appstar, DISJ_IMP_THM, FORALL_AND_THM] >> - dsimp[PULL_EXISTS] >> metis_tac[]) >~ - [‘LAM u $ LAMl us Body’] - >- (gvs[] >> - first_x_assum $ qspec_then ‘Body’ mp_tac >> simp[]>> - disch_then $ qspec_then ‘∅’ mp_tac >> simp[] >> - disch_then kall_tac >> - ‘∀xs M. Body = LAMl xs M ⇔ xs = [] ∧ M = Body’ - by (rpt gen_tac >> Cases_on ‘xs’ >> simp[] >- metis_tac[] >> - strip_tac >> gvs[]) >> - simp[] >> iff_tac >> rw[] - >- (qexistsl [‘u::us’, ‘v’, ‘Ms’] >> simp[]) >> - rename [‘LAM u (LAMl us Body) = LAMl vs (VAR v @* Ms)’] >> - ‘LAMl vs (VAR v @* Ms) = LAMl (u::us) Body’ by simp[] >> - drule EQ_LAML_E >> simp[PULL_EXISTS, tpm_appstar, MEM_listpm_EXISTS]) -QED - -Theorem bnf_appstar[simp]: - ∀M Ns. bnf (M @* Ns) ⇔ bnf M ∧ (∀N. MEM N Ns ⇒ bnf N) ∧ (is_abs M ⇒ Ns = []) -Proof - Induct_on ‘Ns’ using listTheory.SNOC_INDUCT >> - simp[DISJ_IMP_THM, FORALL_AND_THM] >> metis_tac[] -QED - Theorem subterm_perm: ∀G0 M0 G M. subterm (G0,M0) (G,M) ⇒