[examples/lambda] Move more theorems earlier in development

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"]

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);

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) ⇒