[examples/lambda] Move some theorems out of stt into appFOLDL

HOL-Theorem-Prover · Oct 25, 2023 · 34f1696 · 34f1696
1 parent 4f44597
commit 34f1696
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 27 deletions.
diff --git a/examples/lambda/basics/appFOLDLScript.sml b/examples/lambda/basics/appFOLDLScript.sml
@@ -26,10 +26,11 @@ val app_eq_appstar = store_thm(
   Induct THEN SRW_TAC [][] THEN1 METIS_TAC [] THEN
   Cases_on `args` THEN SRW_TAC [][] THEN1 METIS_TAC []);
 
-val lam_eq_appstar = store_thm(
-  "lam_eq_appstar",
-  ``∀args f. (LAM v t = f ·· args) ⇔ (args = []) ∧ (f = LAM v t)``,
-  Induct THEN SRW_TAC [][] THEN METIS_TAC []);
+Theorem lam_eq_appstar[simp]:
+  ∀args f. (LAM v t = f ·· args) ⇔ (args = []) ∧ (f = LAM v t)
+Proof
+  Induct THEN SRW_TAC [][] THEN METIS_TAC []
+QED
 
 val app_eq_varappstar = store_thm(
   "app_eq_varappstar",
@@ -141,6 +142,13 @@ Proof
   simp[appstar_APPEND, SNOC_APPEND]
 QED
 
+Theorem app_eq_appstar_SNOC:
+    t @* Ms = M1 @@ M2 ⇔
+    (∃Ms0. Ms = SNOC M2 Ms0 ∧ t @* Ms0 = M1) ∨ Ms = [] ∧ t = M1 @@ M2
+Proof
+  Cases_on ‘Ms’ using listTheory.SNOC_CASES >> simp[] >> metis_tac[]
+QED
+
 Theorem appstar_CONS :
     M @@ N @* Ns = M @* (N::Ns)
 Proof
@@ -149,12 +157,6 @@ Proof
  >> rw [appstar_APPEND]
 QED
 
-Theorem appstar_EQ_LAM[simp]:
-  x ·· Ms = LAM v M ⇔ Ms = [] ∧ x = LAM v M
-Proof
-  qid_spec_tac ‘x’ >> Induct_on ‘Ms’ >> simp[]
-QED
-
 Theorem ssub_appstar :
     fm ' (M @* Ns) = (fm ' M) @* MAP (ssub fm) Ns
 Proof

diff --git a/examples/lambda/typing/sttScript.sml b/examples/lambda/typing/sttScript.sml
@@ -443,22 +443,6 @@ Proof
   Induct_on ‘subterm’ >> simp[]
 QED
 
-Theorem appstar_EQ_LAMl:
-  t @* Ms = LAMl vs M ⇔
-    Ms = [] ∧ t = LAMl vs M ∨
-    vs = [] ∧ M = t @* Ms
-Proof
-  Cases_on ‘Ms’ using listTheory.SNOC_CASES >> simp[] >>
-  Cases_on ‘vs’ >> simp[] >> metis_tac[]
-QED
-
-Theorem appstar_EQ_APP:
-  t @* Ms = M1 @@ M2 ⇔
-    (∃Ms0. Ms = SNOC M2 Ms0 ∧ t @* Ms0 = M1) ∨ Ms = [] ∧ t = M1 @@ M2
-Proof
-  Cases_on ‘Ms’ using listTheory.SNOC_CASES >> simp[] >> metis_tac[]
-QED
-
 Theorem term_laml_cases:
   ∀X. FINITE X ⇒
       ∀t. (∃s. t = VAR s) ∨ (∃M1 M2. t = M1 @@ M2) ∨
@@ -529,7 +513,7 @@ Proof
       first_x_assum $ qspec_then ‘M2’ assume_tac >> gs[]>>
       rpt (first_x_assum $ drule_then assume_tac) >>
       simp[] >> iff_tac >> rw[] >>
-      gvs[appstar_EQ_APP, appstar_EQ_LAMl, DISJ_IMP_THM, FORALL_AND_THM] >>
+      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[] >>