From 30a4efc93bd341cdf5530d3379fb5511d4329b3d Mon Sep 17 00:00:00 2001
From: Michael Norrish <michael.norrish@anu.edu.au>
Date: Thu, 5 Oct 2023 10:27:31 +1100
Subject: [PATCH] [examples/lambda] fix sttScript and tidy some more appstar
 results

Thanks to Chun Tian for the bug report.
---
 .../lambda/barendregt/normal_orderScript.sml  | 26 +++------
 .../barendregt/standardisationScript.sml      | 58 ++++++++++++++-----
 examples/lambda/basics/appFOLDLScript.sml     | 13 ++---
 examples/lambda/typing/sttScript.sml          |  7 +--
 4 files changed, 60 insertions(+), 44 deletions(-)

diff --git a/examples/lambda/barendregt/normal_orderScript.sml b/examples/lambda/barendregt/normal_orderScript.sml
index 3162377f67..a1083f4aca 100644
--- a/examples/lambda/barendregt/normal_orderScript.sml
+++ b/examples/lambda/barendregt/normal_orderScript.sml
@@ -864,23 +864,15 @@ val normwhnf_is_abs_rpreserved = store_thm(
   HO_MATCH_MP_TAC normorder_ind THEN SRW_TAC [][]);
 
 
-val whnf_is_abs_appstr = store_thm(
-  "whnf_is_abs_appstr",
-  ``∀t. whnf t ⇔ is_abs t ∨ ∃v args. t = VAR v ·· args``,
-  HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][] THENL [
-    MAP_EVERY Q.EXISTS_TAC [`s`, `[]`] THEN SRW_TAC [][],
-    SRW_TAC [][EQ_IMP_THM] THENL [
-      MAP_EVERY Q.EXISTS_TAC [`v`, `args ++ [t']`] THEN
-      SRW_TAC [][rich_listTheory.FOLDL_APPEND],
-
-      FULL_SIMP_TAC (srw_ss()) [app_eq_varappstar] THEN
-      Q.SPEC_THEN `VAR v ·· FRONT args` MP_TAC term_CASES THEN
-      STRIP_TAC THEN SRW_TAC [][] THEN
-      FULL_SIMP_TAC (srw_ss()) [lam_eq_appstar],
-
-      FULL_SIMP_TAC (srw_ss()) [app_eq_varappstar] THEN METIS_TAC []
-    ]
-  ]);
+Theorem whnf_is_abs_appstr:
+  ∀t. whnf t ⇔ is_abs t ∨ ∃v args. t = VAR v ·· args
+Proof
+  HO_MATCH_MP_TAC simple_induction >> rw[SF CONJ_ss] >>
+  simp[app_eq_varappstar, PULL_EXISTS] >> iff_tac >> rw[] >>
+  gvs[] >>
+  rename [‘Ns = FRONT _’, ‘M = LAST _’] >>
+  qexists ‘SNOC M Ns’ >> simp[rich_listTheory.FRONT_APPEND]
+QED
 
 val normorder_strong_ind =
     IndDefLib.derive_strong_induction (normorder_rules,normorder_ind)
diff --git a/examples/lambda/barendregt/standardisationScript.sml b/examples/lambda/barendregt/standardisationScript.sml
index b0378b355d..a3caae2a59 100644
--- a/examples/lambda/barendregt/standardisationScript.sml
+++ b/examples/lambda/barendregt/standardisationScript.sml
@@ -1212,25 +1212,53 @@ val i_reduce_to_LAM_underneath = prove(
     PROVE_TAC [labelled_redn_rules]
   ]);
 
-val LAMl_def = Define`
+Definition LAMl_def:
   LAMl vs (t : term) = FOLDR LAM t vs
-`;
+End
 
-val LAMl_thm = Store_Thm(
-  "LAMl_thm",
-  ``(LAMl [] M = M) /\
-    (LAMl (h::t) M = LAM h (LAMl t M))``,
-  SRW_TAC [][LAMl_def]);
+Theorem LAMl_thm[simp]:
+  (LAMl [] M = M) /\
+  (LAMl (h::t) M = LAM h (LAMl t M))
+Proof SRW_TAC [][LAMl_def]
+QED
 
-val LAMl_11 = Store_Thm(
-  "LAMl_11",
-  ``!vs. (LAMl vs x = LAMl vs y) = (x = y)``,
-  Induct THEN SRW_TAC [][]);
+Theorem LAMl_11[simp]:
+  !vs. (LAMl vs x = LAMl vs y) = (x = y)
+Proof
+  Induct THEN SRW_TAC [][]
+QED
 
-val size_LAMl = Store_Thm(
-  "size_LAMl",
-  ``!vs. size (LAMl vs M) = LENGTH vs + size M``,
-  Induct THEN SRW_TAC [numSimps.ARITH_ss][size_thm]);
+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",
diff --git a/examples/lambda/basics/appFOLDLScript.sml b/examples/lambda/basics/appFOLDLScript.sml
index 035cfaaf78..b5f8605a1a 100644
--- a/examples/lambda/basics/appFOLDLScript.sml
+++ b/examples/lambda/basics/appFOLDLScript.sml
@@ -13,14 +13,11 @@ val _ = set_fixity "@*" (Infixl 901)
 val _ = Unicode.unicode_version { u = "··", tmnm = "@*"}
 val _ = overload_on ("@*", ``λf (args:term list). FOLDL APP f args``)
 
-val var_eq_appstar = store_thm(
-  "var_eq_appstar",
-  ``(VAR s = f ·· args) ⇔ (args = []) ∧ (f = VAR s)``,
-  Induct_on `args` THEN SRW_TAC [][] THENL [
-    METIS_TAC [],
-    MAP_EVERY Q.ID_SPEC_TAC [`f`,`h`] THEN POP_ASSUM (K ALL_TAC) THEN
-    Induct_on `args` THEN SRW_TAC [][]
-  ]);
+Theorem var_eq_appstar[simp]:
+  VAR s = f ·· args ⇔ args = [] ∧ f = VAR s
+Proof
+  Cases_on `args` using SNOC_CASES >> simp[FOLDL_SNOC] >> metis_tac[]
+QED
 
 val app_eq_appstar = store_thm(
   "app_eq_appstar",
diff --git a/examples/lambda/typing/sttScript.sml b/examples/lambda/typing/sttScript.sml
index 8d968598b9..b880aa4470 100644
--- a/examples/lambda/typing/sttScript.sml
+++ b/examples/lambda/typing/sttScript.sml
@@ -378,12 +378,12 @@ Theorem bnf_characterisation:
                 (∀M. MEM M Ms ⇒ bnf M)
 Proof
   ho_match_mp_tac nc_INDUCTION2 >> qexists ‘∅’ >> rw[] >~
-  [‘VAR s = LAMl _ (VAR _ ·· _)’]
-  >- (qexistsl  [‘[]’, ‘s’, ‘[]’] >> simp[]) >~
   [‘VAR _ ·· _ = M1 @@ M2’]
   >- (simp[] >> eq_tac >> rpt strip_tac >~
       [‘M1 = LAMl vs1 _’, ‘M1 @@ M2’]
-      >- (‘vs1 = []’ by (Cases_on ‘vs1’ >> gvs[]) >> gvs[appstar_SNOC] >>
+      >- (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] >>
@@ -404,7 +404,6 @@ Proof
   simp[MEM_listpm] >> rpt strip_tac >> first_assum drule >> simp[]
 QED
 
-
 (*