Improved hnf_appstar and abs_betastar, etc.

examples/lambda/barendregt/chap2Script.sml

@@ -80,15 +80,17 @@ val one_hole_is_normal = store_thm(
                                   MP_TAC (MATCH_MP imp (CONJ cth th))))) THEN
   SIMP_TAC std_ss []);
 
-val (lameq_rules, lameq_indn, lameq_cases) = (* p. 13 *)
-  IndDefLib.xHol_reln "lameq"
-    `(!x M N. (LAM x M) @@ N == [N/x]M) /\
+Inductive lameq :
+     (!x M N. (LAM x M) @@ N == [N/x]M) /\
      (!M. M == M) /\
+[~SYM:]
      (!M N. M == N ==> N == M) /\
+[~TRANS:]
      (!M N L. M == N /\ N == L ==> M == L) /\
      (!M N Z. M == N ==> M @@ Z == N @@ Z) /\
      (!M N Z. M == N ==> Z @@ M == Z @@ N) /\
-     (!M N x. M == N ==> LAM x M == LAM x N)`;
+     (!M N x. M == N ==> LAM x M == LAM x N)
+End
 
 val lameq_refl = Store_thm(
   "lameq_refl",
@@ -105,9 +107,6 @@ val lameq_weaken_cong = store_thm(
   ``(M1:term) == M2 ==> N1 == N2 ==> (M1 == N1 <=> M2 == N2)``,
   METIS_TAC [lameq_rules]);
 
-Theorem lameq_SYM = List.nth(CONJUNCTS lameq_rules, 2)
-Theorem lameq_TRANS = List.nth(CONJUNCTS lameq_rules, 3)
-
 val fixed_point_thm = store_thm(  (* p. 14 *)
   "fixed_point_thm",
   ``!f. ?x. f @@ x == x``,
@@ -309,7 +308,7 @@ val SUB_LAM_RWT = store_thm(
 val lameq_asmlam = store_thm(
   "lameq_asmlam",
   ``!M N. M == N ==> asmlam eqns M N``,
-  HO_MATCH_MP_TAC lameq_indn THEN METIS_TAC [asmlam_rules]);
+  HO_MATCH_MP_TAC lameq_ind THEN METIS_TAC [asmlam_rules]);
 
 fun betafy ss =
     simpLib.add_relsimp {refl = GEN_ALL lameq_refl,

examples/lambda/barendregt/chap3Script.sml

@@ -929,9 +929,12 @@ QED
 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 -b->* N'
+    !x M Z. LAM x M -b->* Z <=> ?N'. (Z = LAM x N') /\ M -b->* N'
 Proof
     rpt GEN_TAC
+ >> reverse EQ_TAC
+ >- (rw [] >> PROVE_TAC [reduction_rules])
+ (* stage work *)
  >> REWRITE_TAC [SYM theorem3_17]
  >> Q.ID_SPEC_TAC ‘Z’
  >> HO_MATCH_MP_TAC (Q.ISPEC ‘grandbeta’ TC_INDUCT_ALT_RIGHT)

examples/lambda/barendregt/head_reductionScript.sml

@@ -1,7 +1,8 @@
 open HolKernel Parse boolLib bossLib
 
-open chap3Theory pred_setTheory termTheory boolSimps
-open nomsetTheory binderLib
+open pred_setTheory boolSimps;
+
+open termTheory chap2Theory chap3Theory nomsetTheory binderLib;
 
 val _ = new_theory "head_reduction"
 
@@ -351,4 +352,14 @@ val head_reductions_have_weak_prefixes = store_thm(
      >- metis_tac [hnf_whnf, relationTheory.RTC_RULES] >>
    metis_tac [relationTheory.RTC_RULES, hreduce_weak_or_strong]);
 
+(* ----------------------------------------------------------------------
+    HNF and Combinators
+   ---------------------------------------------------------------------- *)
+
+Theorem hnf_I :
+    hnf I
+Proof
+    RW_TAC std_ss [hnf_thm, I_def]
+QED
+
 val _ = export_theory()

examples/lambda/barendregt/standardisationScript.sml

@@ -2500,12 +2500,22 @@ Proof
 QED
 
 Theorem hnf_appstar :
-    !M Ns. hnf (M @* Ns) /\ Ns <> [] ==> hnf M /\ ~is_abs M
+    !M Ns. Ns <> [] ==> (hnf (M @* Ns) <=> hnf M /\ ~is_abs M)
 Proof
-    Q.X_GEN_TAC ‘M’
+    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]
- >> Cases_on ‘Ns = []’ >> fs []
 QED
 
 Theorem hnf_cases :
@@ -2536,9 +2546,7 @@ Proof
      rw [hnf_cases])
  (* stage work *)
  >> ‘?Z. LAM x M -b->* Z /\ N -b->* Z’ by METIS_TAC [lameq_CR]
- >> Know ‘?N'. (Z = LAM x N') /\ M -b->* N'’
- >- (MATCH_MP_TAC abs_betastar >> art [])
- >> STRIP_TAC
+ >> ‘?N'. (Z = LAM x N') /\ M -b->* N'’ by rw [GSYM abs_betastar]
  >> Q.EXISTS_TAC ‘N'’
  >> ‘hnf Z’ by PROVE_TAC [hnf_preserved]
  >> gs [hnf_thm]