From 27421e280916ac5c53a84940ca5e0f8a493d5d53 Mon Sep 17 00:00:00 2001
From: Chun Tian <binghe.lisp@gmail.com>
Date: Tue, 3 Oct 2023 23:44:09 +1100
Subject: [PATCH] [examples/lambda] generalized "abs_betastar" using `-b->*`
 instead of `==`

---
 examples/lambda/barendregt/chap3Script.sml         | 12 +++++++-----
 .../lambda/barendregt/standardisationScript.sml    | 14 ++++++++------
 2 files changed, 15 insertions(+), 11 deletions(-)

diff --git a/examples/lambda/barendregt/chap3Script.sml b/examples/lambda/barendregt/chap3Script.sml
index 9618d09aef..f9931d275f 100644
--- a/examples/lambda/barendregt/chap3Script.sml
+++ b/examples/lambda/barendregt/chap3Script.sml
@@ -925,9 +925,11 @@ Proof
  >> MATCH_MP_TAC grandbeta_imp_betastar >> art []
 QED
 
-(* cf. abs_grandbeta, added by Chun Tian *)
+(* |- !R x y z. R^+ x y /\ R^+ y z ==> R^+ x z *)
+Theorem TC_TRANS[local] = REWRITE_RULE [transitive_def] TC_TRANSITIVE
+
 Theorem abs_betastar :
-    !x M Z. LAM x M -b->* Z ==> ?N'. (Z = LAM x N') /\ M == N'
+    !x M Z. LAM x M -b->* Z ==> ?N'. (Z = LAM x N') /\ M -b->* N'
 Proof
     rpt GEN_TAC
  >> REWRITE_TAC [SYM theorem3_17]
@@ -936,13 +938,13 @@ Proof
  >> rpt STRIP_TAC
  >- (FULL_SIMP_TAC std_ss [abs_grandbeta] \\
      Q.EXISTS_TAC ‘N0’ >> art [] \\
-     MATCH_MP_TAC grandbeta_imp_lameq >> art [])
+     MATCH_MP_TAC TC_SUBSET >> art [])
  >> Q.PAT_X_ASSUM ‘Z = LAM x N'’ (FULL_SIMP_TAC std_ss o wrap)
  >> FULL_SIMP_TAC std_ss [abs_grandbeta]
  >> Q.EXISTS_TAC ‘N0’ >> art []
- >> MATCH_MP_TAC lameq_TRANS
+ >> MATCH_MP_TAC TC_TRANS
  >> Q.EXISTS_TAC ‘N'’ >> art []
- >> MATCH_MP_TAC grandbeta_imp_lameq >> art []
+ >> MATCH_MP_TAC TC_SUBSET >> art []
 QED
 
 val lameq_consistent = store_thm(
diff --git a/examples/lambda/barendregt/standardisationScript.sml b/examples/lambda/barendregt/standardisationScript.sml
index a6bcd346e2..35aec9fd29 100644
--- a/examples/lambda/barendregt/standardisationScript.sml
+++ b/examples/lambda/barendregt/standardisationScript.sml
@@ -2523,7 +2523,7 @@ Proof
  >> qexistsl_tac [‘vs’, ‘args’, ‘y’] >> art []
 QED
 
-(* Proposition 8.3.13 (i) *)
+(* Proposition 8.3.13 (i) [1, p.174] *)
 Theorem has_hnf_iff_LAM[simp] :
     !x M. has_hnf (LAM x M) <=> has_hnf M
 Proof
@@ -2536,11 +2536,13 @@ Proof
      rw [hnf_cases])
  (* stage work *)
  >> ‘?Z. LAM x M -b->* Z /\ N -b->* Z’ by METIS_TAC [lameq_CR]
- >> Suff ‘?N'. (Z = LAM x N') /\ M == N'’
- >- (STRIP_TAC \\
-    ‘hnf Z’ by PROVE_TAC [hnf_preserved] \\
-     Q.EXISTS_TAC ‘N'’ >> gs [hnf_thm])
- >> MATCH_MP_TAC abs_betastar >> art []
+ >> Know ‘?N'. (Z = LAM x N') /\ M -b->* N'’
+ >- (MATCH_MP_TAC abs_betastar >> art [])
+ >> STRIP_TAC
+ >> Q.EXISTS_TAC ‘N'’
+ >> ‘hnf Z’ by PROVE_TAC [hnf_preserved]
+ >> gs [hnf_thm]
+ >> MATCH_MP_TAC betastar_lameq >> art []
 QED
 
 val _ = export_theory()