From b1932f570d0d387247222cb8e41f01884c393019 Mon Sep 17 00:00:00 2001
From: Michael Norrish <michael.norrish@anu.edu.au>
Date: Wed, 4 Oct 2023 16:54:19 +1100
Subject: [PATCH] [examples/lambda] Some minor tweaks to results about appstar

Use

  Induct_on `x` using SNOC_INDUCT

idiom more and also add some more rewrites.
---
 examples/lambda/barendregt/chap2Script.sml    | 10 ++--
 .../barendregt/standardisationScript.sml      | 48 +++++++++----------
 examples/lambda/basics/appFOLDLScript.sml     | 10 ++--
 3 files changed, 31 insertions(+), 37 deletions(-)

diff --git a/examples/lambda/barendregt/chap2Script.sml b/examples/lambda/barendregt/chap2Script.sml
index 667aaec3ee..56be0b51a7 100644
--- a/examples/lambda/barendregt/chap2Script.sml
+++ b/examples/lambda/barendregt/chap2Script.sml
@@ -87,7 +87,9 @@ Inductive lameq :
      (!M N. M == N ==> N == M) /\
 [~TRANS:]
      (!M N L. M == N /\ N == L ==> M == L) /\
+[~APPL:]
      (!M N Z. M == N ==> M @@ Z == N @@ Z) /\
+[~APPR:]
      (!M N Z. M == N ==> Z @@ M == Z @@ N) /\
      (!M N x. M == N ==> LAM x M == LAM x N)
 End
@@ -343,8 +345,8 @@ val lameq_I = store_thm(
 Theorem I_appstar' :
     !Is. (!e. MEM e Is ==> e = I) ==> I @* Is == I
 Proof
-    HO_MATCH_MP_TAC SNOC_INDUCT >> rw []
- >> ASM_SIMP_TAC (betafy (srw_ss())) [SNOC_APPEND, SYM appstar_SNOC, lameq_I]
+  Induct_on ‘Is’ using SNOC_INDUCT >> rw [appstar_SNOC]
+  >> ASM_SIMP_TAC (betafy (srw_ss())) [lameq_I]
 QED
 
 Theorem I_appstar :
@@ -723,9 +725,7 @@ QED
 Theorem lameq_appstar_cong :
     !M N Ns. M == N ==> M @* Ns == N @* Ns
 Proof
-    NTAC 2 GEN_TAC
- >> HO_MATCH_MP_TAC SNOC_INDUCT >> rw []
- >> ASM_SIMP_TAC (betafy (srw_ss())) [SNOC_APPEND, SYM appstar_SNOC]
+  Induct_on ‘Ns’ using SNOC_INDUCT >> rw [appstar_SNOC, lameq_APPL]
 QED
 
 val _ = remove_ovl_mapping "Y" {Thy = "chap2", Name = "Y"}
diff --git a/examples/lambda/barendregt/standardisationScript.sml b/examples/lambda/barendregt/standardisationScript.sml
index 3f9fcade33..b0378b355d 100644
--- a/examples/lambda/barendregt/standardisationScript.sml
+++ b/examples/lambda/barendregt/standardisationScript.sml
@@ -2499,38 +2499,34 @@ 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. Ns <> [] ==> (hnf (M @* Ns) <=> hnf M /\ ~is_abs M)
+    !M Ns. hnf (M @* Ns) <=> hnf M /\ (is_abs M ⇒ (Ns = []))
 Proof
-    rpt STRIP_TAC
- >> EQ_TAC
- >- (POP_ASSUM MP_TAC \\
-     Q.ID_SPEC_TAC ‘Ns’ >> HO_MATCH_MP_TAC SNOC_INDUCT \\
-     rw [SNOC_APPEND, SYM appstar_SNOC] \\
-     Cases_on ‘Ns = []’ >> fs [])
- >> STRIP_TAC
- >> Q.ID_SPEC_TAC ‘Ns’
- >> HO_MATCH_MP_TAC SNOC_INDUCT
- >> rw [SNOC_APPEND, SYM appstar_SNOC]
- >> Q.PAT_X_ASSUM ‘~is_abs M’ MP_TAC >> KILL_TAC >> DISCH_TAC
- >> Q.SPEC_TAC (‘Ns'’, ‘Ns’)
- >> HO_MATCH_MP_TAC SNOC_INDUCT
- >> rw [SNOC_APPEND, SYM appstar_SNOC]
+  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)
+  !M : term. hnf M <=> ?vs args y. M = LAMl vs (VAR y @* args)
 Proof
-    rpt STRIP_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[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] *)
diff --git a/examples/lambda/basics/appFOLDLScript.sml b/examples/lambda/basics/appFOLDLScript.sml
index 06cea4bb35..035cfaaf78 100644
--- a/examples/lambda/basics/appFOLDLScript.sml
+++ b/examples/lambda/basics/appFOLDLScript.sml
@@ -151,10 +151,10 @@ Proof
   qid_spec_tac ‘x’ >> Induct_on ‘Ms1’ >> simp[]
 QED
 
-Theorem appstar_SNOC:
-  x ·· Ms @@ M = x ·· (Ms ++ [M])
+Theorem appstar_SNOC[simp]:
+  x ·· (SNOC M Ms) = (x ·· Ms) @@ M
 Proof
-  simp[appstar_APPEND]
+  simp[appstar_APPEND, SNOC_APPEND]
 QED
 
 Theorem appstar_CONS :
@@ -174,9 +174,7 @@ QED
 Theorem ssub_appstar :
     fm ' (M @* Ns) = (fm ' M) @* MAP (ssub fm) Ns
 Proof
-    Q.ID_SPEC_TAC ‘Ns’
- >> HO_MATCH_MP_TAC SNOC_INDUCT
- >> rw [SNOC_APPEND, SYM appstar_SNOC]
+    Induct_on ‘Ns’ using SNOC_INDUCT >> simp[appstar_SNOC, MAP_SNOC]
 QED
 
 val _ = export_theory ()