more results of terms having head normal forms (has_hnf)

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,8 +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)
-
 val fixed_point_thm = store_thm(  (* p. 14 *)
   "fixed_point_thm",
   ``!f. ?x. f @@ x == x``,
@@ -308,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,
@@ -537,6 +537,15 @@ val is_abs_vsubst_invariant = Store_thm(
   HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;v}` THEN
   SRW_TAC [][SUB_THM, SUB_VAR]);
 
+Theorem is_abs_cases :
+    !t. is_abs t <=> ?v t0. t = LAM v t0
+Proof
+    Q.X_GEN_TAC ‘t’
+ >> Q.SPEC_THEN ‘t’ STRUCT_CASES_TAC term_CASES
+ >> SRW_TAC [][]
+ >> qexistsl_tac [‘v’, ‘t0’] >> REWRITE_TAC []
+QED
+
 val (is_comb_thm, _) = define_recursive_term_function
   `(is_comb (VAR s) = F) /\
    (is_comb (t1 @@ t2) = T) /\
@@ -561,6 +570,22 @@ val is_var_vsubst_invariant = Store_thm(
   HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;v}` THEN
   SRW_TAC [][SUB_THM, SUB_VAR]);
 
+Theorem is_var_cases :
+    !t. is_var t <=> ?y. t = VAR y
+Proof
+    Q.X_GEN_TAC ‘t’
+ >> Q.SPEC_THEN ‘t’ STRUCT_CASES_TAC term_CASES
+ >> SRW_TAC [][]
+QED
+
+Theorem term_cases :
+    !t. is_var t \/ is_comb t \/ is_abs t
+Proof
+    Q.X_GEN_TAC ‘t’
+ >> Q.SPEC_THEN ‘t’ STRUCT_CASES_TAC term_CASES
+ >> SRW_TAC [][]
+QED
+
 val (bnf_thm, _) = define_recursive_term_function
   `(bnf (VAR s) <=> T) /\
    (bnf (t1 @@ t2) <=> bnf t1 /\ bnf t2 /\ ~is_abs t1) /\
@@ -706,6 +731,7 @@ QED
 val _ = remove_ovl_mapping "Y" {Thy = "chap2", Name = "Y"}
 
 val _ = export_theory()
+val _ = html_theory "chap2";
 
 (* References:
 

examples/lambda/barendregt/chap3Script.sml

@@ -1,12 +1,12 @@
-open HolKernel Parse boolLib bossLib metisLib basic_swapTheory
-     relationTheory
+open HolKernel Parse boolLib bossLib;
 
-val _ = new_theory "chap3";
+open metisLib basic_swapTheory relationTheory hurdUtils;
 
 local open pred_setLib in end;
 
-open binderLib BasicProvers
-open nomsetTheory termTheory chap2Theory
+open binderLib BasicProvers nomsetTheory termTheory chap2Theory;
+
+val _ = new_theory "chap3";
 
 fun Store_thm (trip as (n,t,tac)) = store_thm trip before export_rewrites [n]
 
@@ -525,7 +525,7 @@ val diamond_property_def = save_thm("diamond_property_def", diamond_def)
 end
 val _ = overload_on("diamond_property", ``relation$diamond``)
 
-(* This is not the same CR as appears in   There
+(* This is not the same CR as appears in relationTheory. There
      CR R = diamond (RTC R)
    Here,
      CR R = diamond (RTC (compat_closure R))
@@ -893,6 +893,10 @@ val lameq_betaconversion = store_thm(
 
 val prop3_18 = save_thm("prop3_18", lameq_betaconversion);
 
+(* |- !M N. M == N ==> ?Z. M -b->* Z /\ N -b->* Z *)
+Theorem lameq_CR = REWRITE_RULE [GSYM lameq_betaconversion, beta_CR]
+                                (Q.SPEC ‘beta’ theorem3_13)
+
 val ccbeta_lameq = store_thm(
   "ccbeta_lameq",
   ``!M N. M -b-> N ==> M == N``,
@@ -908,6 +912,44 @@ val betastar_lameq_bnf = store_thm(
   METIS_TAC [theorem3_13, beta_CR, betastar_lameq, bnf_reduction_to_self,
              lameq_betaconversion]);
 
+(* |- !M N. M =b=> N ==> M -b->* N *)
+Theorem grandbeta_imp_betastar =
+    (REWRITE_RULE [theorem3_17] (Q.ISPEC ‘grandbeta’ TC_SUBSET))
+ |> (Q.SPECL [‘M’, ‘N’]) |> (Q.GENL [‘M’, ‘N’])
+
+Theorem grandbeta_imp_lameq :
+    !M N. M =b=> N ==> M == N
+Proof
+    rpt STRIP_TAC
+ >> MATCH_MP_TAC betastar_lameq
+ >> MATCH_MP_TAC grandbeta_imp_betastar >> art []
+QED
+
+(* |- !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 -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)
+ >> rpt STRIP_TAC
+ >- (FULL_SIMP_TAC std_ss [abs_grandbeta] \\
+     Q.EXISTS_TAC ‘N0’ >> 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 TC_TRANS
+ >> Q.EXISTS_TAC ‘N'’ >> art []
+ >> MATCH_MP_TAC TC_SUBSET >> art []
+QED
+
 val lameq_consistent = store_thm(
   "lameq_consistent",
   ``consistent $==``,
@@ -1474,4 +1516,4 @@ val betastar_eq_cong = store_thm(
   METIS_TAC [bnf_triangle, RTC_CASES_RTC_TWICE]);
 
 val _ = export_theory();
-
+val _ = html_theory "chap3";

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/normal_orderScript.sml

@@ -1057,3 +1057,4 @@ val normstar_to_vheadbinary_wstar = save_thm(
                  [leneq2, DECIDE ``x < 2 ⇔ (x = 0) ∨ (x = 1)``]);
 
 val _ = export_theory()
+val _ = html_theory "normal_order";

examples/lambda/barendregt/solvableScript.sml

@@ -9,7 +9,8 @@ open arithmeticTheory pred_setTheory listTheory sortingTheory finite_mapTheory
      hurdUtils;
 
 (* lambda theories *)
-open termTheory appFOLDLTheory chap2Theory standardisationTheory reductionEval;
+open termTheory appFOLDLTheory chap2Theory chap3Theory standardisationTheory
+     reductionEval;
 
 val _ = new_theory "solvable";
 
@@ -104,9 +105,6 @@ Proof
  >> rw [lameq_K]
 QED
 
-Theorem lameq_symm[local]  = List.nth(CONJUNCTS lameq_rules, 2)
-Theorem lameq_trans[local] = List.nth(CONJUNCTS lameq_rules, 3)
-
 Theorem solvable_xIO :
     solvable (VAR x @@ I @@ Omega)
 Proof
@@ -186,7 +184,7 @@ Proof
      MATCH_MP_TAC FV_ssub \\
      rw [Abbr ‘fm’, FUN_FMAP_DEF, FAPPLY_FUPDATE_THM])
  (* stage work *)
- >> MATCH_MP_TAC lameq_trans
+ >> MATCH_MP_TAC lameq_TRANS
  >> Q.EXISTS_TAC ‘fm ' (M @* Ns)’
  >> reverse CONJ_TAC
  >- (ONCE_REWRITE_TAC [SYM ssub_I] \\
@@ -243,7 +241,7 @@ Proof
      MATCH_MP_TAC LAMl_appstar >> rw [])
  >> DISCH_TAC
  >> ‘LAMl vs M @* Ns0 @* Ns1 == fm ' M @* Ns1’ by PROVE_TAC [lameq_appstar_cong]
- >> ‘fm ' M @* Ns1 == I’ by PROVE_TAC [lameq_trans, lameq_symm]
+ >> ‘fm ' M @* Ns1 == I’ by PROVE_TAC [lameq_TRANS, lameq_SYM]
  >> qexistsl_tac [‘fm ' M’, ‘Ns1’]
  >> rw [closed_substitution_instances_def]
  >> Q.EXISTS_TAC ‘fm’ >> rw [Abbr ‘fm’]
@@ -281,7 +279,7 @@ Proof
      FULL_SIMP_TAC std_ss [GSYM appstar_APPEND] \\
      Q.ABBREV_TAC ‘Ns' = Ns ++ Is’ \\
     ‘LENGTH Ns' = n’ by (rw [Abbr ‘Ns'’, Abbr ‘Is’]) \\
-    ‘LAMl vs M @* Ns' == I’ by PROVE_TAC [lameq_trans] \\
+    ‘LAMl vs M @* Ns' == I’ by PROVE_TAC [lameq_TRANS] \\
      Know ‘EVERY closed Ns'’
      >- (rw [EVERY_APPEND, Abbr ‘Ns'’] \\
          rw [EVERY_MEM, Abbr ‘Is’, closed_def, MEM_GENLIST] \\
@@ -327,7 +325,7 @@ Proof
  >> Know ‘LAMl vs M @* Ps @* Ns == (FEMPTY |++ ZIP (vs,Ps)) ' M @* Ns’
  >- (MATCH_MP_TAC lameq_appstar_cong >> art [])
  >> DISCH_TAC
- >> ‘LAMl vs M @* Ps @* Ns == I’ by PROVE_TAC [lameq_trans]
+ >> ‘LAMl vs M @* Ps @* Ns == I’ by PROVE_TAC [lameq_TRANS]
  >> qexistsl_tac [‘LAMl vs M’, ‘Ps ++ Ns’]
  >> rw [appstar_APPEND, closures_def]
  >> Q.EXISTS_TAC ‘vs’ >> art []
@@ -369,7 +367,7 @@ Proof
      MATCH_MP_TAC LAMl_appstar >> rw [])
  >> DISCH_TAC
  >> ‘LAMl vs M @* Ns0 @* Ns1 == fm ' M @* Ns1’ by PROVE_TAC [lameq_appstar_cong]
- >> ‘fm ' M @* Ns1 == I’ by PROVE_TAC [lameq_trans, lameq_symm]
+ >> ‘fm ' M @* Ns1 == I’ by PROVE_TAC [lameq_TRANS, lameq_SYM]
  (* Ns0' is the permuted version of Ns0 *)
  >> Q.ABBREV_TAC ‘Ns0' = GENLIST (\i. EL (f i) Ns0) n’
  >> ‘LENGTH Ns0' = n’ by rw [Abbr ‘Ns0'’, LENGTH_GENLIST]
@@ -392,9 +390,9 @@ Proof
      MATCH_MP_TAC LAMl_appstar >> rw [])
  >> DISCH_TAC
  >> ‘LAMl vs' M @* Ns0' @* Ns1 == fm' ' M @* Ns1’ by PROVE_TAC [lameq_appstar_cong]
- >> MATCH_MP_TAC lameq_trans
+ >> MATCH_MP_TAC lameq_TRANS
  >> Q.EXISTS_TAC ‘fm' ' M @* Ns1’ >> art []
- >> MATCH_MP_TAC lameq_trans
+ >> MATCH_MP_TAC lameq_TRANS
  >> Q.EXISTS_TAC ‘fm ' M @* Ns1’ >> art []
  >> Suff ‘fm = fm'’ >- rw []
  (* cleanup uncessary assumptions *)
@@ -476,7 +474,7 @@ Proof
  >> ‘LAMl vs M @* (Ns ++ Is) == I @* Is’ by rw [appstar_APPEND]
  >> Q.ABBREV_TAC ‘Ns' = Ns ++ Is’
  >> ‘LENGTH Ns' = n’ by (rw [Abbr ‘Ns'’, Abbr ‘Is’])
- >> ‘LAMl vs M @* Ns' == I’ by PROVE_TAC [lameq_trans]
+ >> ‘LAMl vs M @* Ns' == I’ by PROVE_TAC [lameq_TRANS]
  >> Know ‘EVERY closed Ns'’
  >- (rw [EVERY_APPEND, Abbr ‘Ns'’] \\
      rw [EVERY_MEM, Abbr ‘Is’, closed_def, MEM_GENLIST] \\
@@ -489,8 +487,8 @@ QED
 Theorem ssub_LAM[local] = List.nth(CONJUNCTS ssub_thm, 2)
 
 (* Lemma 8.3.3 (ii) *)
-Theorem solvable_iff_solvable_LAM[simp] :
-    !M x. solvable (LAM x M) <=> solvable M
+Theorem solvable_iff_LAM[simp] :
+    !x M. solvable (LAM x M) <=> solvable M
 Proof
     rpt STRIP_TAC
  >> reverse EQ_TAC
@@ -509,7 +507,7 @@ Proof
             rw [Abbr ‘fm0’, Abbr ‘N’, DOMSUB_FAPPLY_THM, closed_def]) >> Rewr' \\
         DISCH_TAC \\
         Know ‘fm0 ' (LAM x M @@ N) @* Ns == I’
-        >- (MATCH_MP_TAC lameq_trans \\
+        >- (MATCH_MP_TAC lameq_TRANS \\
             Q.EXISTS_TAC ‘fm0 ' ([N/x] M) @* Ns’ \\
             POP_ASSUM (REWRITE_TAC o wrap) \\
             MATCH_MP_TAC lameq_appstar_cong \\
@@ -525,7 +523,7 @@ Proof
         Q.EXISTS_TAC ‘fm0’ >> rw [Abbr ‘fm0’, DOMSUB_FAPPLY_THM],
         (* goal 1.2 (of 2) *)
         Know ‘fm ' (LAM x M @@ I) @* Ns == I’
-        >- (MATCH_MP_TAC lameq_trans \\
+        >- (MATCH_MP_TAC lameq_TRANS \\
             Q.EXISTS_TAC ‘fm ' M @* Ns’ >> art [] \\
             MATCH_MP_TAC lameq_appstar_cong \\
             MATCH_MP_TAC lameq_ssub_cong >> art [] \\
@@ -561,7 +559,7 @@ Proof
         simp [appstar_APPEND] \\
         DISCH_TAC \\
         Know ‘[h/x] (fm ' M) @* t == I’
-        >- (MATCH_MP_TAC lameq_trans \\
+        >- (MATCH_MP_TAC lameq_TRANS \\
             Q.EXISTS_TAC ‘LAM x (fm ' M) @@ h @* t’ >> art [] \\
             MATCH_MP_TAC lameq_appstar_cong \\
             rw [lameq_rules]) \\
@@ -596,7 +594,7 @@ Proof
         simp [appstar_APPEND] \\
         DISCH_TAC \\
         Know ‘[h/x] (fm ' M) @* t == I’
-        >- (MATCH_MP_TAC lameq_trans \\
+        >- (MATCH_MP_TAC lameq_TRANS \\
             Q.EXISTS_TAC ‘LAM x (fm ' M) @@ h @* t’ >> art [] \\
             MATCH_MP_TAC lameq_appstar_cong \\
             rw [lameq_rules]) \\