From 4a0b51d9300cc6c00b5781423da3165f1a7de7e6 Mon Sep 17 00:00:00 2001
From: Chun Tian <binghe.lisp@gmail.com>
Date: Wed, 25 Oct 2023 01:36:17 +1100
Subject: [PATCH 1/4] Initial boehm_treeTheory (up to dhnf_cases)

---
 examples/lambda/Holmakefile                   |   4 +-
 examples/lambda/barendregt/chap2Script.sml    |  84 +--
 examples/lambda/barendregt/chap3Script.sml    |  51 +-
 .../barendregt/finite_developmentsScript.sml  |   9 +-
 examples/lambda/basics/appFOLDLScript.sml     |  19 +-
 examples/lambda/basics/termScript.sml         |  59 ++-
 examples/lambda/completeness/Holmakefile      |   3 +
 .../lambda/completeness/boehm_treeScript.sml  | 186 +++++++
 examples/lambda/other-models/diagsScript.sml  |  14 +-
 .../lambda/other-models/pure_dBScript.sml     | 478 +++++++++++++++---
 src/list/src/listScript.sml                   |  24 +
 src/relation/relationScript.sml               |  32 ++
 12 files changed, 774 insertions(+), 189 deletions(-)
 create mode 100644 examples/lambda/completeness/Holmakefile
 create mode 100644 examples/lambda/completeness/boehm_treeScript.sml

diff --git a/examples/lambda/Holmakefile b/examples/lambda/Holmakefile
index 89d3c3e996..c818c7c09e 100644
--- a/examples/lambda/Holmakefile
+++ b/examples/lambda/Holmakefile
@@ -1,2 +1,4 @@
 CLINE_OPTIONS = -r
-INCLUDES = barendregt basics other-models typing wcbv-reasonable examples
+
+INCLUDES = barendregt basics other-models typing wcbv-reasonable examples \
+	   completeness
diff --git a/examples/lambda/barendregt/chap2Script.sml b/examples/lambda/barendregt/chap2Script.sml
index bf6c310e59..9cf3ffc599 100644
--- a/examples/lambda/barendregt/chap2Script.sml
+++ b/examples/lambda/barendregt/chap2Script.sml
@@ -118,14 +118,6 @@ val fixed_point_thm = store_thm(  (* p. 14 *)
 
 (* properties of substitution - p19 *)
 
-val SUB_TWICE_ONE_VAR = store_thm(
-  "SUB_TWICE_ONE_VAR",
-  ``!body. [x/v] ([y/v] body) = [[x/v]y / v] body``,
-  HO_MATCH_MP_TAC nc_INDUCTION2 THEN SRW_TAC [][SUB_THM, SUB_VAR] THEN
-  Q.EXISTS_TAC `v INSERT FV x UNION FV y` THEN
-  SRW_TAC [][SUB_THM] THEN
-  Cases_on `v IN FV y` THEN SRW_TAC [][SUB_THM, lemma14c, lemma14b]);
-
 val lemma2_11 = store_thm(
   "lemma2_11",
   ``!t. ~(v = u)  /\ ~(v IN FV M) ==>
@@ -166,6 +158,7 @@ val lemma2_12 = store_thm( (* p. 19 *)
     PROVE_TAC [lameq_rules]
   ]);
 
+(* |- M == M' ==> N == N' ==> [N/x] M == [N'/x] M' *)
 val lameq_sub_cong = save_thm(
   "lameq_sub_cong",
   REWRITE_RULE [GSYM AND_IMP_INTRO] (last (CONJUNCTS lemma2_12)));
@@ -221,24 +214,54 @@ val lemma2_14 = store_thm(
     PROVE_TAC [lameta_rules]
   ]);
 
-val consistent_def =
-    Define`consistent (thy:term -> term -> bool) = ?M N. ~thy M N`;
+(* Definition 2.1.30 [1, p.33]: "Let tt be a formal theory with equations as
+   formulas. Then tt is consistent (notation Con(tt)) if tt does not prove every
+   closed equation. In the opposite case tt is consistent.
+ *)
+Definition consistent_def :
+    consistent (thy:term -> term -> bool) = ?M N. ~thy M N
+End
+
+(* This is lambda theories (only having beta equivalence, no eta equivalence)
+   extended with extra equations as formulas.
 
-val (asmlam_rules, asmlam_ind, asmlam_cases) = Hol_reln`
+   cf. Definition 4.1.1 [1, p.76]. If ‘eqns’ is a set of closed equations,
+   then ‘{(M,N) | asmlam eqns M N}’ is the set of closed equations provable
+   in lambda + eqns, denoted by ‘eqns^+’ in [1], or ‘asmlam eqns’ here.
+ *)
+Inductive asmlam :
+[~eqn:]
   (!M N. (M,N) IN eqns ==> asmlam eqns M N) /\
+[~beta:]
   (!x M N. asmlam eqns (LAM x M @@ N) ([N/x]M)) /\
+[~refl:]
   (!M. asmlam eqns M M) /\
+[~sym:]
   (!M N. asmlam eqns M N ==> asmlam eqns N M) /\
+[~trans:]
   (!M N P. asmlam eqns M N /\ asmlam eqns N P ==> asmlam eqns M P) /\
+[~lcong:]
   (!M M' N. asmlam eqns M M' ==> asmlam eqns (M @@ N) (M' @@ N)) /\
+[~rcong:]
   (!M N N'. asmlam eqns N N' ==> asmlam eqns (M @@ N) (M @@ N')) /\
+[~abscong:]
   (!x M M'. asmlam eqns M M' ==> asmlam eqns (LAM x M) (LAM x M'))
-`;
+End
+
+(* Definition 2.1.32 [1, p.33]
 
-(* This is also Definition 2.1.32 [1, p.33] *)
-val incompatible_def =
-    Define`incompatible x y = ~consistent (asmlam {(x,y)})`
+   cf. also Definition 2.1.30 (iii): If t is a set of equations, then lambda + t
+   is the theory obtained from lambda by adding the equations of t as axioms.
+   t is called consistent (notation Con(t)) if Con(lambda + t), or in our words,
+  ‘consistent (asmlam T)’.
 
+   This explains why ‘asmlam’ is involved in the definition of ‘incompatible’.
+*)
+Definition incompatible_def :
+    incompatible x y = ~consistent (asmlam {(x,y)})
+End
+
+(* NOTE: in termTheory, ‘v # M’ also denotes ‘v NOTIN FV M’ *)
 Overload "#" = “incompatible”
 
 val S_def =
@@ -465,9 +488,10 @@ val Yf_cong = store_thm(
   STRIP_TAC THEN ASM_SIMP_TAC (srw_ss()) [] THEN
   METIS_TAC [lameq_rules]);
 
-val SK_incompatible = store_thm( (* example 2.18, p23 *)
-  "SK_incompatible",
-  ``incompatible S K``,
+(* This is Example 2.1.33 [1, p.33] and Example 2.18 [2, p23] *)
+Theorem SK_incompatible :
+    incompatible S K
+Proof
   Q_TAC SUFF_TAC `!M N. asmlam {(S,K)} M N`
         THEN1 SRW_TAC [][incompatible_def, consistent_def] THEN
   REPEAT GEN_TAC THEN
@@ -480,11 +504,8 @@ val SK_incompatible = store_thm( (* example 2.18, p23 *)
       by PROVE_TAC [lameq_S, asmlam_rules, lameq_asmlam] THEN
   `!D. asmlam {(S,K)} D I`
       by PROVE_TAC [lameq_I, lameq_K, asmlam_rules, lameq_asmlam] THEN
-  PROVE_TAC [asmlam_rules]);
-
-val [asmlam_eqn, asmlam_beta, asmlam_refl, asmlam_sym, asmlam_trans,
-     asmlam_lcong, asmlam_rcong, asmlam_abscong] =
-    CONJUNCTS (SPEC_ALL asmlam_rules)
+  PROVE_TAC [asmlam_rules]
+QED
 
 val xx_xy_incompatible = store_thm( (* example 2.20, p24 *)
   "xx_xy_incompatible",
@@ -856,15 +877,6 @@ Proof
  >> MATCH_MP_TAC lameq_appstar_cong >> art []
 QED
 
-val foldl_snoc = prove(
-  ``!l f x y. FOLDL f x (APPEND l [y]) = f (FOLDL f x l) y``,
-  Induct THEN SRW_TAC [][]);
-
-val combs_not_size_1 = prove(
-  ``(size M = 1) ==> ~is_comb M``,
-  Q.SPEC_THEN `M` STRUCT_CASES_TAC term_CASES THEN
-  SRW_TAC [][size_thm, size_nz]);
-
 Theorem strange_cases :
     !M : term. (?vs M'. (M = LAMl vs M') /\ (size M' = 1)) \/
                (?vs args t.
@@ -885,11 +897,11 @@ Proof
               THENL [
                 MAP_EVERY Q.EXISTS_TAC [`[N]`, `M`] THEN
                 ASM_SIMP_TAC (srw_ss()) [] THEN
-                PROVE_TAC [combs_not_size_1],
+                fs [size_1_cases],
                 ASM_SIMP_TAC (srw_ss()) [] THEN
                 Cases_on `vs` THENL [
-                  MAP_EVERY Q.EXISTS_TAC [`APPEND args [N]`, `t`] THEN
-                  ASM_SIMP_TAC (srw_ss()) [foldl_snoc],
+                  MAP_EVERY Q.EXISTS_TAC [`SNOC N args`, `t`] THEN
+                  ASM_SIMP_TAC (srw_ss()) [FOLDL_SNOC],
                   MAP_EVERY Q.EXISTS_TAC [`[N]`, `M`] THEN
                   ASM_SIMP_TAC (srw_ss()) []
                 ]
@@ -912,6 +924,8 @@ val _ = html_theory "chap2";
 
 (* References:
 
+   [1] Barendregt, H.P.: The Lambda Calculus, Its Syntax and Semantics.
+       College Publications, London (1984).
    [2] Hankin, C.: Lambda Calculi: A Guide for Computer Scientists.
        Clarendon Press, Oxford (1994).
  *)
diff --git a/examples/lambda/barendregt/chap3Script.sml b/examples/lambda/barendregt/chap3Script.sml
index d710f791c2..fea68a1b8a 100644
--- a/examples/lambda/barendregt/chap3Script.sml
+++ b/examples/lambda/barendregt/chap3Script.sml
@@ -1,6 +1,6 @@
 open HolKernel Parse boolLib bossLib;
 
-open metisLib basic_swapTheory relationTheory hurdUtils;
+open boolSimps metisLib basic_swapTheory relationTheory hurdUtils;
 
 local open pred_setLib in end;
 
@@ -910,6 +910,13 @@ val betastar_lameq_bnf = store_thm(
   METIS_TAC [theorem3_13, beta_CR, betastar_lameq, bnf_reduction_to_self,
              lameq_betaconversion]);
 
+(* moved here from churchnumScript.sml *)
+Theorem lameq_triangle :
+    M == N ∧ M == P ∧ bnf N ∧ bnf P ⇒ (N = P)
+Proof
+  METIS_TAC [betastar_lameq_bnf, lameq_rules, bnf_reduction_to_self]
+QED
+
 (* |- !M N. M =b=> N ==> M -b->* N *)
 Theorem grandbeta_imp_betastar =
     (REWRITE_RULE [theorem3_17] (Q.ISPEC ‘grandbeta’ TC_SUBSET))
@@ -1028,37 +1035,6 @@ val hr_lemma0 = prove(
                             RUNION] THEN
   PROVE_TAC []);
 
-val RUNION_RTC_MONOTONE = store_thm(
-  "RUNION_RTC_MONOTONE",
-  ``!R1 x y. RTC R1 x y ==> !R2. RTC (R1 RUNION R2) x y``,
-  GEN_TAC THEN HO_MATCH_MP_TAC RTC_INDUCT THEN
-  PROVE_TAC [RTC_RULES, RUNION]);
-
-val RTC_OUT = store_thm(
-  "RTC_OUT",
-  ``!R1 R2. RTC (RTC R1 RUNION RTC R2) = RTC (R1 RUNION R2)``,
-  REPEAT GEN_TAC THEN
-  Q_TAC SUFF_TAC
-    `(!x y. RTC (RTC R1 RUNION RTC R2) x y ==> RTC (R1 RUNION R2) x y) /\
-     (!x y. RTC (R1 RUNION R2) x y ==> RTC (RTC R1 RUNION RTC R2) x y)` THEN1
-    (SIMP_TAC (srw_ss()) [FUN_EQ_THM, EQ_IMP_THM, FORALL_AND_THM] THEN
-     PROVE_TAC []) THEN CONJ_TAC
-  THEN HO_MATCH_MP_TAC RTC_INDUCT THENL [
-    CONJ_TAC THENL [
-      PROVE_TAC [RTC_RULES],
-      MAP_EVERY Q.X_GEN_TAC [`x`,`y`,`z`] THEN REPEAT STRIP_TAC THEN
-      `RTC R1 x y \/ RTC R2 x y` by PROVE_TAC [RUNION] THEN
-      PROVE_TAC [RUNION_RTC_MONOTONE, RTC_RTC, RUNION_COMM]
-    ],
-    CONJ_TAC THENL [
-      PROVE_TAC [RTC_RULES],
-      MAP_EVERY Q.X_GEN_TAC [`x`,`y`,`z`] THEN REPEAT STRIP_TAC THEN
-      `R1 x y \/ R2 x y` by PROVE_TAC [RUNION] THEN
-      PROVE_TAC [RTC_RULES, RUNION]
-    ]
-  ]);
-
-
 val CC_RUNION_MONOTONE = store_thm(
   "CC_RUNION_MONOTONE",
   ``!R1 x y. compat_closure R1 x y ==> compat_closure (R1 RUNION R2) x y``,
@@ -1095,7 +1071,7 @@ val hindley_rosen_lemma = store_thm( (* p43 *)
     `diamond_property (RTC (RTC (compat_closure R1) RUNION
                             RTC (compat_closure R2)))`
         by PROVE_TAC [hr_lemma0] THEN
-    FULL_SIMP_TAC (srw_ss()) [RTC_OUT, CC_RUNION_DISTRIB]
+    FULL_SIMP_TAC (srw_ss()) [RTC_RUNION, CC_RUNION_DISTRIB]
   ]);
 
 val eta_def =
@@ -1461,7 +1437,6 @@ val rator_isub_commutes = store_thm(
     Congruence and rewrite rules for -b-> and -b->*
    ---------------------------------------------------------------------- *)
 
-open boolSimps
 val RTC1_step = CONJUNCT2 (SPEC_ALL RTC_RULES)
 
 val betastar_LAM = store_thm(
@@ -1515,3 +1490,11 @@ val betastar_eq_cong = store_thm(
 
 val _ = export_theory();
 val _ = html_theory "chap3";
+
+(* References:
+
+   [1] Barendregt, H.P.: The Lambda Calculus, Its Syntax and Semantics.
+       College Publications, London (1984).
+   [2] Hankin, C.: Lambda Calculi: A Guide for Computer Scientists.
+       Clarendon Press, Oxford (1994).
+ *)
diff --git a/examples/lambda/barendregt/finite_developmentsScript.sml b/examples/lambda/barendregt/finite_developmentsScript.sml
index 79e2dc1848..1fd39a096e 100644
--- a/examples/lambda/barendregt/finite_developmentsScript.sml
+++ b/examples/lambda/barendregt/finite_developmentsScript.sml
@@ -1,10 +1,9 @@
-open HolKernel Parse boolLib
+open HolKernel Parse bossLib boolLib;
 
-open bossLib metisLib boolSimps
+open BasicProvers metisLib boolSimps pred_setTheory pathTheory relationTheory;
 
 open chap3Theory chap2Theory labelledTermsTheory termTheory binderLib
-open term_posnsTheory chap11_1Theory
-open pathTheory BasicProvers nomsetTheory pred_setTheory
+     term_posnsTheory chap11_1Theory nomsetTheory;
 
 local open pred_setLib in end
 val _ = augment_srw_ss [boolSimps.LET_ss]
@@ -19,6 +18,8 @@ val _ = hide "set"
 val RUNION_COMM = relationTheory.RUNION_COMM
 val RUNION = relationTheory.RUNION
 
+val SN_def = pathTheory.SN_def; (* cf. chap3Theory.SN_def, relationTheory.SN_def *)
+
 (* finiteness of developments : section 11.2 of Barendregt *)
 
 (* ----------------------------------------------------------------------
diff --git a/examples/lambda/basics/appFOLDLScript.sml b/examples/lambda/basics/appFOLDLScript.sml
index 3b9a2733cf..4e6dbae49f 100644
--- a/examples/lambda/basics/appFOLDLScript.sml
+++ b/examples/lambda/basics/appFOLDLScript.sml
@@ -8,7 +8,8 @@ val _ = new_theory "appFOLDL"
 
 val _ = set_fixity "@*" (Infixl 901)
 val _ = Unicode.unicode_version { u = "··", tmnm = "@*"}
-val _ = overload_on ("@*", ``λf (args:term list). FOLDL APP f args``)
+
+Overload "@*" = “\f (args:term list). FOLDL APP f args”
 
 Theorem var_eq_appstar[simp]:
   VAR s = f ·· args ⇔ args = [] ∧ f = VAR s
@@ -173,9 +174,13 @@ QED
  *  LAMl (was in standardisationTheory)
  *---------------------------------------------------------------------------*)
 
-Definition LAMl_def:
+Overload "LAMl" = “\vs (t :term). FOLDR LAM t vs”
+
+Theorem LAMl_def :
   LAMl vs (t : term) = FOLDR LAM t vs
-End
+Proof
+    rw []
+QED
 
 Theorem LAMl_thm[simp]:
   (LAMl [] M = M) /\
@@ -316,5 +321,13 @@ Proof
  >> SET_TAC []
 QED
 
+(* moved here from churchnumScript.sml *)
+Theorem size_funpow :
+    size (FUNPOW (APP f) n x) = (size f + 1) * n + size x
+Proof
+  Induct_on `n` THEN
+  SRW_TAC [ARITH_ss][FUNPOW_SUC, LEFT_ADD_DISTRIB, MULT_CLAUSES]
+QED
+
 val _ = export_theory ()
 val _ = html_theory "appFOLDL";
diff --git a/examples/lambda/basics/termScript.sml b/examples/lambda/basics/termScript.sml
index 2110260022..51b9b8e74e 100644
--- a/examples/lambda/basics/termScript.sml
+++ b/examples/lambda/basics/termScript.sml
@@ -1,18 +1,13 @@
-open HolKernel boolLib Parse bossLib generic_termsTheory
+open HolKernel Parse boolLib bossLib;
 
-open boolSimps arithmeticTheory;
+open boolSimps arithmeticTheory pred_setTheory finite_mapTheory hurdUtils;
+
+open generic_termsTheory binderLib nomsetTheory nomdatatype;
 
-open nomsetTheory
-open pred_setTheory finite_mapTheory hurdUtils
-open binderLib
-open nomdatatype
 val _ = new_theory "term";
 
 val _ = set_fixity "=" (Infix(NONASSOC, 450))
 
-fun Save_thm (nm, th) = save_thm(nm,th) before export_rewrites [nm]
-fun Store_thm(nm,t,tac) = store_thm(nm,t,tac) before export_rewrites [nm]
-
 val tyname = "term"
 
 val vp = ``(λn u:unit. n = 0)``
@@ -120,11 +115,10 @@ in
     |> GEN_ALL
 end
 
-val FV_thm = Save_thm(
-  "FV_thm",
-  LIST_CONJ (map supp_clause cons_info))
-
-
+(* |- (!s. FV (VAR s) = {s}) /\ (!t2 t1. FV (t1 @@ t2) = FV t1 UNION FV t2) /\
+      !v t. FV (LAM v t) = FV t DELETE v
+ *)
+Theorem FV_thm[simp] = LIST_CONJ (map supp_clause cons_info)
 
 fun genit th = let
   val (_, args) = strip_comb (concl th)
@@ -297,10 +291,10 @@ val tm_recursion = save_thm(
       |> SIMP_RULE (srw_ss() ++ CONJ_ss) [supp_unitfn]
       |> Q.INST [`apu` |-> `ap`, `lmu` |-> `lm`, `vru` |-> `vr`])
 
-val FV_tpm = Save_thm("FV_tpm",
-                      ``x ∈ FV (tpm p t)``
+(* |- !x t p. x IN FV (tpm p t) <=> lswapstr (REVERSE p) x IN FV t *)
+Theorem FV_tpm[simp] = ``x ∈ FV (tpm p t)``
                       |> REWRITE_CONV [perm_supp,pmact_IN]
-                      |> GEN_ALL);
+                      |> GEN_ALL
 
 val _ = set_mapped_fixity { term_name = "APP", tok = "@@",
                             fixity = Infixl 901}
@@ -537,6 +531,15 @@ Theorem lemma15b:
 Proof SRW_TAC [][lemma15a]
 QED
 
+Theorem SUB_TWICE_ONE_VAR :
+    !body. [x/v] ([y/v] body) = [[x/v]y / v] body
+Proof
+  HO_MATCH_MP_TAC nc_INDUCTION2 THEN SRW_TAC [][SUB_THM, SUB_VAR] THEN
+  Q.EXISTS_TAC `v INSERT FV x UNION FV y` THEN
+  SRW_TAC [][SUB_THM] THEN
+  Cases_on `v IN FV y` THEN SRW_TAC [][SUB_THM, lemma14c, lemma14b]
+QED
+
 (* ----------------------------------------------------------------------
     alpha-convertibility results
    ---------------------------------------------------------------------- *)
@@ -640,6 +643,15 @@ Definition DOM_DEF :
    (DOM ((x,y)::rst) = {y} UNION DOM rst)
 End
 
+Theorem DOM_ALT_MAP_SND :
+    !phi. DOM phi = set (MAP SND phi)
+Proof
+    Induct_on ‘phi’ >- rw [DOM_DEF]
+ >> Q.X_GEN_TAC ‘h’
+ >> Cases_on ‘h’
+ >> rw [DOM_DEF] >> SET_TAC []
+QED
+
 Definition FVS_DEF :
    (FVS [] = {}) /\
    (FVS ((t,x)::rst) = FV t UNION FVS rst)
@@ -659,8 +671,8 @@ Proof
  >> RW_TAC std_ss [FVS_DEF, FINITE_EMPTY, FINITE_UNION, FINITE_FV]
 QED
 
-Theorem ISUB_LAM :
-    !R x. ~(x IN (DOM R UNION FVS R)) ==>
+Theorem ISUB_LAM[simp] :
+    !R x. x NOTIN DOM R /\ x NOTIN FVS R ==>
           !t. (LAM x t) ISUB R = LAM x (t ISUB R)
 Proof
     Induct
@@ -836,7 +848,14 @@ val ssub_exists =
                                alphas = [tpm_ALPHA]}
 
 val ssub_def = new_specification ("ssub_def", ["ssub"], ssub_exists)
-val ssub_thm = Save_thm("ssub_thm", CONJUNCT1 ssub_def)
+
+(* |- (!s fm. fm ' (VAR s) = if s IN FDOM fm then fm ' s else VAR s) /\
+      (!fm t t'. fm ' (t' @@ t) = fm ' t' @@ fm ' t) /\
+      !v fm t.
+        v NOTIN FDOM fm /\ (!y. y IN FDOM fm ==> v # fm ' y) ==>
+        (fm ' (LAM v t) = LAM v (fm ' t))
+ *)
+Theorem ssub_thm[simp] = CONJUNCT1 ssub_def
 
 val _ = overload_on ("'", ``ssub``)
 
diff --git a/examples/lambda/completeness/Holmakefile b/examples/lambda/completeness/Holmakefile
new file mode 100644
index 0000000000..f3c62c8146
--- /dev/null
+++ b/examples/lambda/completeness/Holmakefile
@@ -0,0 +1,3 @@
+INCLUDES = $(dprot $(HOLDIR)/src/coalgebras) ../basics ../barendregt ../other-models
+
+EXTRA_CLEANS = $(patsubst %Theory.uo,%Theory.html,$(DEFAULT_TARGETS))
diff --git a/examples/lambda/completeness/boehm_treeScript.sml b/examples/lambda/completeness/boehm_treeScript.sml
new file mode 100644
index 0000000000..1ff2dd0677
--- /dev/null
+++ b/examples/lambda/completeness/boehm_treeScript.sml
@@ -0,0 +1,186 @@
+(*---------------------------------------------------------------------------*
+ * boehm_treeScript.sml: (Effective) Boehm Trees (Chapter 10 of [1])         *
+ *---------------------------------------------------------------------------*)
+
+open HolKernel boolLib Parse bossLib;
+
+(* core theories *)
+open optionTheory arithmeticTheory pred_setTheory listTheory llistTheory
+     ltreeTheory pathTheory posetTheory hurdUtils;
+
+open binderLib termTheory appFOLDLTheory chap2Theory chap3Theory
+     head_reductionTheory standardisationTheory solvableTheory pure_dBTheory;
+
+val _ = new_theory "boehm_tree";
+
+val o_DEF = combinTheory.o_DEF; (* cannot directly open combinTheory *)
+
+(* A dB-term M is hnf if its corresponding Lambda term is hnf *)
+Overload dhnf = “hnf o toTerm”
+
+Theorem dhnf_fromTerm[simp] :
+    !M. dhnf (fromTerm M) <=> hnf M
+Proof
+    rw [o_DEF]
+QED
+
+(* Translations from LAMl to dABSi.
+
+   Some samples for guessing out the statements of this theorem:
+
+> SIMP_CONV arith_ss [dLAM_def, lift_def, sub_def, lift_sub]
+                     “dLAM v1 (dLAM v0 t)”;
+# val it =
+   |- dLAM v1 (dLAM v0 t) =
+      dABS (dABS ([dV 1/v1 + 2] ([dV 0/v0 + 2] (lift (lift t 0) 1)))): thm
+
+> SIMP_CONV arith_ss [dLAM_def, lift_def, sub_def, lift_sub]
+                     “dLAM v2 (dLAM v1 (dLAM v0 t))”;
+# val it =
+   |- dLAM v2 (dLAM v1 (dLAM v0 t)) =
+      dABS
+        (dABS
+           (dABS ([dV 2/v2 + 3]
+                    ([dV 1/v1 + 3]
+                       ([dV 0/v0 + 3]
+                          (lift (lift (lift t 0) 1) 2)))))): thm
+ *)
+Theorem LAMl_to_dABSi :
+    !vs. ALL_DISTINCT (vs :num list) ==>
+         let n = LENGTH vs;
+             body = FOLDL lift t (GENLIST I n);
+             phi = ZIP (GENLIST dV n, MAP (\i. i + n) (REVERSE vs))
+         in LAMl vs t = dABSi n (body ISUB phi)
+Proof
+    Induct_on ‘vs’ >- rw [isub_def]
+ >> rw [isub_def, GSYM SNOC_APPEND, MAP_SNOC, FUNPOW_SUC, GENLIST, FOLDL_SNOC,
+        dLAM_def]
+ >> fs []
+ >> qabbrev_tac ‘n = LENGTH vs’
+ >> rw [lift_dABSi]
+ >> Q.PAT_X_ASSUM ‘LAMl vs t = _’ K_TAC
+ >> qabbrev_tac ‘N = FOLDL lift t (GENLIST I n)’
+ >> qabbrev_tac ‘Ms = GENLIST dV n’
+ >> qabbrev_tac ‘Vs = MAP (\i. i + n) (REVERSE vs)’
+ >> Know ‘lift (N ISUB ZIP (Ms,Vs)) n =
+          (lift N n) ISUB (ZIP (MAP (\e. lift e n) Ms,MAP SUC Vs))’
+ >- (MATCH_MP_TAC lift_isub \\
+     rw [Abbr ‘Ms’, Abbr ‘Vs’, EVERY_MEM, MEM_MAP] >> rw [])
+ >> Rewr'
+ >> ‘MAP SUC Vs = MAP (\i. i + SUC n) (REVERSE vs)’
+       by (rw [LIST_EQ_REWRITE, EL_MAP, Abbr ‘Vs’]) >> POP_ORW
+ >> qunabbrev_tac ‘Vs’ (* now useless *)
+ >> rw [sub_def, GSYM ADD1]
+ >> ‘MAP (\e. lift e n) Ms = Ms’
+       by (rw [LIST_EQ_REWRITE, EL_MAP, Abbr ‘Ms’]) >> POP_ORW
+ >> qabbrev_tac ‘Ns = MAP (\i. i + SUC n) (REVERSE vs)’
+ >> qabbrev_tac ‘N' = lift N n’
+ >> Suff ‘N' ISUB ZIP (SNOC (dV n) Ms,SNOC (h + SUC n) Ns) =
+          [dV n/h + SUC n] (N' ISUB ZIP (Ms,Ns))’ >- rw []
+ >> MATCH_MP_TAC isub_SNOC
+ >> rw [Abbr ‘Ms’, Abbr ‘Ns’, MEM_EL, EL_MAP]
+ >> rename1 ‘~(i < n)’
+ >> ‘LENGTH (REVERSE vs) = n’ by rw [Abbr ‘n’]
+ >> CCONTR_TAC >> gs [EL_MAP]
+ >> ‘h = EL i (REVERSE vs)’ by rw []
+ >> Suff ‘MEM h (REVERSE vs)’ >- rw [MEM_REVERSE]
+ >> Q.PAT_X_ASSUM ‘~MEM h vs’ K_TAC
+ >> ‘LENGTH (REVERSE vs) = n’ by rw [Abbr ‘n’]
+ >> REWRITE_TAC [MEM_EL]
+ >> Q.EXISTS_TAC ‘i’ >> art []
+QED
+
+(* |- !t vs.
+        ALL_DISTINCT vs ==>
+        LAMl vs t =
+        dABSi (LENGTH vs)
+          (FOLDL lift t (GENLIST I (LENGTH vs)) ISUB
+           ZIP (GENLIST dV (LENGTH vs),MAP (\i. i + LENGTH vs) (REVERSE vs)))
+ *)
+Theorem LAMl_to_dABSi_applied[local] =
+    GEN_ALL (SIMP_RULE std_ss [LET_DEF] LAMl_to_dABSi)
+
+(* dB version of hnf_cases (only the ==> direction) *)
+Theorem dhnf_cases :
+    !M. dhnf M ==> ?n y Ms. M = dABSi n (dV y @* Ms)
+Proof
+    RW_TAC std_ss [hnf_cases]
+ >> qabbrev_tac ‘n = LENGTH vs’
+ >> Q.EXISTS_TAC ‘n’
+ >> Know ‘fromTerm (toTerm M) = fromTerm (LAMl vs (VAR y @* args))’
+ >- (art [fromTerm_11])
+ >> Q.PAT_X_ASSUM ‘toTerm M = LAMl vs (VAR y @* args)’ K_TAC
+ >> rw [fromTerm_LAMl, fromTerm_appstar]
+ >> qabbrev_tac ‘vs' = MAP s2n vs’
+ >> qabbrev_tac ‘Ms = MAP fromTerm args’
+ >> qabbrev_tac ‘y' = s2n y’
+ >> Know ‘LAMl vs' (dV y' @* Ms) =
+          dABSi (LENGTH vs')
+            (FOLDL lift (dV y' @* Ms) (GENLIST I (LENGTH vs')) ISUB
+             ZIP (GENLIST dV (LENGTH vs'),
+                  MAP (\i. i + LENGTH vs') (REVERSE vs')))’
+ >- (MATCH_MP_TAC LAMl_to_dABSi_applied \\
+     qunabbrev_tac ‘vs'’ \\
+     MATCH_MP_TAC ALL_DISTINCT_MAP_INJ >> rw [])
+ >> ‘LENGTH vs' = n’ by rw [Abbr ‘vs'’] >> POP_ORW
+ >> Rewr'
+ >> simp [FOLDL_lift_appstar, isub_appstar]
+ >> Know ‘FOLDL lift (dV y') (GENLIST I n) = dV (y' + n)’
+ >- (KILL_TAC \\
+     Induct_on ‘n’ >> rw [GENLIST, FOLDL_SNOC])
+ >> Rewr'
+ >> qabbrev_tac ‘Ms' = MAP (\e. FOLDL lift e (GENLIST I n)) Ms’
+ >> reverse (Cases_on ‘MEM y vs’)
+ >- (‘~MEM y' vs'’ by (rw [Abbr ‘y'’, Abbr ‘vs'’, MEM_MAP]) \\
+     ‘~MEM y' (REVERSE vs')’ by PROVE_TAC [MEM_REVERSE] \\
+     Suff ‘dV (y' + n) ISUB ZIP (GENLIST dV n,MAP (\i. i + n) (REVERSE vs')) =
+           dV (y' + n)’ >- (Rewr' >> METIS_TAC []) \\
+     MATCH_MP_TAC isub_dV_fresh \\
+     qabbrev_tac ‘l1 = GENLIST dV n’ \\
+     qabbrev_tac ‘l2 = MAP (\i. i + n) (REVERSE vs')’ \\
+    ‘LENGTH l1 = n’ by rw [Abbr ‘l1’] \\
+    ‘LENGTH l2 = n’ by rw [Abbr ‘l2’, Abbr ‘n’, Abbr ‘vs'’] \\
+     simp [DOM_ALT_MAP_SND, MAP_ZIP] \\
+     rw [Abbr ‘l2’, MEM_MAP])
+ (* stage work *)
+ >> ‘MEM y' vs'’ by (rw [Abbr ‘y'’, Abbr ‘vs'’, MEM_MAP])
+ >> ‘MEM y' (REVERSE vs')’ by PROVE_TAC [MEM_REVERSE]
+ >> ‘?j. j < LENGTH (REVERSE vs') /\ y' = EL j (REVERSE vs')’
+        by METIS_TAC [MEM_EL]
+ >> ‘LENGTH (REVERSE vs') = n’ by rw [Abbr ‘vs'’, Abbr ‘n’]
+ >> qabbrev_tac ‘Ns = MAP (\i. i + n) (REVERSE vs')’
+ >> ‘LENGTH Ns = n’ by rw [Abbr ‘Ns’]
+ >> Know ‘ALL_DISTINCT Ns’
+ >- (qunabbrev_tac ‘Ns’ \\
+     MATCH_MP_TAC ALL_DISTINCT_MAP_INJ >> rw [] \\
+     qunabbrev_tac ‘vs'’ \\
+     MATCH_MP_TAC ALL_DISTINCT_MAP_INJ >> rw [])
+ >> DISCH_TAC
+ >> Suff ‘dV (y' + n) ISUB ZIP (GENLIST dV n,Ns) = EL j (GENLIST dV n)’
+ >- (Rewr' \\
+     simp [EL_GENLIST] >> METIS_TAC [])
+ >> MATCH_MP_TAC isub_dV_once >> simp []
+ >> CONJ_TAC >- (rw [Abbr ‘Ns’, EL_MAP])
+ >> Q.X_GEN_TAC ‘i’ >> DISCH_TAC
+ >> ‘n <= EL i Ns’ by rw [Abbr ‘Ns’, EL_MAP]
+ >> Suff ‘FVS (ZIP (GENLIST dV n,Ns)) = count n’ >- rw []
+ >> Q.PAT_X_ASSUM ‘LENGTH Ns = n’ MP_TAC
+ >> KILL_TAC >> Q.ID_SPEC_TAC ‘Ns’
+ >> Induct_on ‘n’ >> rw [dFVS_def]
+ >> ‘Ns <> []’ by rw [NOT_NIL_EQ_LENGTH_NOT_0]
+ >> ‘LENGTH (FRONT Ns) = n’ by rw [LENGTH_FRONT]
+ >> ‘Ns = SNOC (LAST Ns) (FRONT Ns)’
+      by (rw [APPEND_FRONT_LAST, SNOC_APPEND]) >> POP_ORW
+ >> Q.PAT_X_ASSUM ‘!Ns. LENGTH Ns = n ==> P’ (MP_TAC o (Q.SPEC ‘FRONT Ns’))
+ >> rw [GENLIST, COUNT_SUC, dFVS_SNOC, ZIP_SNOC, dFV_def]
+ >> SET_TAC []
+QED
+
+val _ = export_theory ();
+val _ = html_theory "boehm_tree";
+
+(* References:
+
+   [1] Barendregt, H.P.: The lambda calculus, its syntax and semantics.
+       College Publications, London (1984).
+ *)
diff --git a/examples/lambda/other-models/diagsScript.sml b/examples/lambda/other-models/diagsScript.sml
index e01d616ef5..9ceed44c7c 100644
--- a/examples/lambda/other-models/diagsScript.sml
+++ b/examples/lambda/other-models/diagsScript.sml
@@ -1,8 +1,6 @@
-open HolKernel Parse boolLib
+open HolKernel Parse boolLib bossLib;
 
-open relationTheory bossLib boolSimps
-
-open pred_setTheory
+open boolSimps relationTheory pred_setTheory chap3Theory;
 
 val _ = new_theory "diags"
 
@@ -386,7 +384,7 @@ val note_lemma9 = store_thm(
        by METIS_TAC [] THEN
     `RTC s a1 a1' /\ RTC s a2' a2` by METIS_TAC [] THEN
     `RTC (x RUNION s) a1 a1' /\ RTC (x RUNION s) a2' a2`
-       by METIS_TAC [chap3Theory.RUNION_RTC_MONOTONE, RUNION_COMM] THEN
+       by METIS_TAC [RUNION_RTC_MONOTONE, RUNION_COMM] THEN
     METIS_TAC [RTC_RTC],
     METIS_TAC []
   ]);
@@ -401,13 +399,13 @@ val note_prop10_1 = store_thm(
   SIMP_TAC (srw_ss()) [sRefl_def, onto_def, ofree_def, kCompl_def] THEN
   STRIP_TAC THEN
   HO_MATCH_MP_TAC RTC_INDUCT THEN CONJ_TAC THENL [
-    METIS_TAC [chap3Theory.RUNION_RTC_MONOTONE, RUNION_COMM],
+    METIS_TAC [RUNION_RTC_MONOTONE, RUNION_COMM],
     REPEAT STRIP_TAC THEN
     `?a0 a1'. x a0 a1' /\ (b1 = f a0) /\ (b1' = f a1')` by METIS_TAC [] THEN
     `RTC s a1' a1` by METIS_TAC [] THEN
     `RTC (x RUNION s) a1' a1`
-      by METIS_TAC [chap3Theory.RUNION_RTC_MONOTONE, RUNION_COMM] THEN
-    `RTC (x RUNION s) a0 a1'` by METIS_TAC [chap3Theory.RUNION_RTC_MONOTONE,
+      by METIS_TAC [RUNION_RTC_MONOTONE, RUNION_COMM] THEN
+    `RTC (x RUNION s) a0 a1'` by METIS_TAC [RUNION_RTC_MONOTONE,
                                             RTC_RULES] THEN
     METIS_TAC [RTC_RTC]
   ]);
diff --git a/examples/lambda/other-models/pure_dBScript.sml b/examples/lambda/other-models/pure_dBScript.sml
index be3b294903..cc9fd06e58 100644
--- a/examples/lambda/other-models/pure_dBScript.sml
+++ b/examples/lambda/other-models/pure_dBScript.sml
@@ -1,10 +1,16 @@
-open HolKernel boolLib Parse bossLib pred_setTheory termTheory BasicProvers
+(*---------------------------------------------------------------------------*
+   Mechanisation of the type of "pure" de Bruijn terms, following
+   Tobias Nipkow's paper "More Church-Rosser Proofs" [1].  (They are
+   "pure" in contrast with Andy Gordon's de Bruijn terms, which have
+   indices for bound variables and strings for free variables.)
+ *---------------------------------------------------------------------------*)
 
-open arithmeticTheory boolSimps
+open HolKernel boolLib Parse bossLib BasicProvers;
 
-local open string_numTheory chap2Theory chap3Theory in end
+open boolSimps arithmeticTheory pred_setTheory string_numTheory listTheory
+     hurdUtils;
 
-fun Store_thm(trip as (n,t,tac)) = store_thm trip before export_rewrites [n]
+open termTheory appFOLDLTheory chap2Theory chap3Theory;
 
 val _ = new_theory "pure_dB"
 
@@ -14,36 +20,52 @@ val _ = temp_set_fixity "=" (Infix(NONASSOC, 100))
 val _ = Datatype`pdb = dV num | dAPP pdb pdb | dABS pdb`
 
 (* Definitions of lift and substitution from Nipkow's "More Church-Rosser
-   proofs" *)
-val lift_def = Define`
+   proofs". NOTE: ‘lift s 0’ will forcely lift everything.
+ *)
+Definition lift_def :
   (lift (dV i) k = if i < k then dV i else dV (i + 1)) /\
   (lift (dAPP s t) k = dAPP (lift s k) (lift t k)) /\
   (lift (dABS s) k = dABS (lift s (k + 1)))
-`;
+End
 val _ = export_rewrites ["lift_def"]
 
+(* ‘k = 0’ is a common usage of ‘lift’ *)
+Theorem lift_dV_0[simp] :
+    lift (dV i) 0 = dV (i + 1)
+Proof
+    rw [lift_def]
+QED
+
+Theorem FUNPOW_lift_dV_0[simp] :
+    FUNPOW (\e. lift e 0) n (dV i) = dV (i + n)
+Proof
+    Induct_on ‘n’ >> rw [FUNPOW_SUC]
+QED
+
 (* "Nipkow" substitution *)
-val nsub_def = Define`
+Definition nsub_def :
   (nsub s k (dV i) = if k < i then dV (i - 1)
                        else if i = k then s else dV i) /\
   (nsub s k (dAPP t u) = dAPP (nsub s k t) (nsub s k u)) /\
   (nsub s k (dABS t) = dABS (nsub (lift s 0) (k + 1) t))
-`;
+End
 val _ = export_rewrites ["nsub_def"]
 
 (* substitution that corresponds to substitution in the lambda-calculus;
    no variable decrementing in the dV clause *)
-val sub_def = Define`
+Definition sub_def :
   (sub s k (dV i) = if i = k then s else dV i) /\
   (sub s k (dAPP t u) = dAPP (sub s k t) (sub s k u)) /\
   (sub s k (dABS t) = dABS (sub (lift s 0) (k + 1) t))
-`;
+End
 val _ = export_rewrites ["sub_def"]
 
+Overload SUB = “sub” (* same [./.] syntax as SUB *)
+
 (* a variable-binding lambda-equivalent for dB terms *)
-val dLAM_def = Define`
+Definition dLAM_def :
   dLAM v body = dABS (sub (dV 0) (v + 1) (lift body 0))
-`
+End
 
 (* the set of free indices in a term *)
 val dFV_def = Define`
@@ -170,6 +192,7 @@ val _ = export_rewrites ["dpm_thm"]
 
 (* dFVs gives the free indices of a dB term as strings *)
 val dFVs_def = Define`dFVs t = IMAGE n2s (dFV t)`
+
 val IN_dFVs_thm = store_thm(
   "IN_dFVs_thm",
   ``(s IN dFVs (dV i) = (i = s2n s)) /\
@@ -297,8 +320,6 @@ val sub_15a = store_thm(
   FIRST_X_ASSUM MATCH_MP_TAC THEN
   FIRST_X_ASSUM (Q.SPEC_THEN `i + 1` MP_TAC) THEN SRW_TAC [ARITH_ss][]);
 
-open chap2Theory
-
 (* from Nipkow *)
 val nipkow_lift_lemma1 = store_thm(
   "nipkow_lift_lemma1",
@@ -329,6 +350,12 @@ val IN_dFV_lift = store_thm(
   ])
 val _ = export_rewrites ["IN_dFV_lift"]
 
+Theorem dLAM_alt_dpm :
+    !v body. dLAM v body = dABS (dpm [(n2s 0, n2s (v + 1))] (lift body 0))
+Proof
+    RW_TAC arith_ss [dLAM_def, fresh_dpm_sub, IN_dFV_lift]
+QED
+
 (* The substitution lemma, in dB guise *)
 val sub_lemma = store_thm(
   "sub_lemma",
@@ -342,13 +369,14 @@ val sub_lemma = store_thm(
 
 (* which allows us to prove that substitution interacts with dLAM in the way
    we'd expect *)
-val sub_dLAM = store_thm(
-  "sub_dLAM",
-  ``~(i IN dFV N) /\ ~(i = j) ==>
-    (sub N j (dLAM i M) = dLAM i (sub N j M))``,
+Theorem sub_dLAM[simp] :
+    ~(i IN dFV N) /\ ~(i = j) ==>
+    (sub N j (dLAM i M) = dLAM i (sub N j M))
+Proof
   SRW_TAC [][dLAM_def] THEN
   SRW_TAC [][Once sub_lemma] THEN
-  SRW_TAC [][lift_sub]);
+  SRW_TAC [][lift_sub]
+QED
 
 val dFVs_lift = store_thm(
   "dFVs_lift",
@@ -485,6 +513,12 @@ val fromTerm_eqlam = prove(
     SRW_TAC [][] THEN SRW_TAC [][fromTerm_def]
   ])
 
+(* |- ((fromTerm t = dV j <=> t = VAR (n2s j)) /\
+       (dV j = fromTerm t <=> t = VAR (n2s j)) /\
+       (fromTerm t = dAPP d1 d2 <=>
+        ?t1 t2. t = t1 @@ t2 /\ d1 = fromTerm t1 /\ d2 = fromTerm t2)) /\
+      (fromTerm t = dLAM i d <=> ?t0. t = LAM (n2s i) t0 /\ d = fromTerm t0)
+ *)
 val fromTerm_eqn = save_thm(
   "fromTerm_eqn",
   CONJ fromTerm_eq0 fromTerm_eqlam)
@@ -506,7 +540,6 @@ val (dbeta'_rules, dbeta'_ind, dbeta'_cases) = Hol_reln`
   (!M N i. dbeta' M N ==> dbeta' (dLAM i M) (dLAM i N))
 `;
 
-open chap3Theory
 val dbeta'_ccbeta = store_thm(
   "dbeta'_ccbeta",
   ``!t u. dbeta' t u ==> !M N. (t = fromTerm M) /\ (u = fromTerm N) ==>
@@ -865,7 +898,6 @@ val dbeta_dbeta'_eqn = store_thm(
 
 (* both of the next two proofs begin by rewriting dbeta to dbeta', using
    dbeta_dbeta'_eqn *)
-open chap3Theory
 val ccbeta_dbeta1 = prove(
   ``!M N. compat_closure beta M N ==> dbeta (fromTerm M) (fromTerm N)``,
   REWRITE_TAC [dbeta_dbeta'_eqn] THEN HO_MATCH_MP_TAC compat_closure_ind THEN
@@ -948,34 +980,37 @@ val toTerm_def = new_specification(
 val fromtoTerm = save_thm("fromtoTerm", GSYM toTerm_def)
 val _ = export_rewrites ["fromtoTerm"]
 
-val toTerm_11 = Store_thm(
-  "toTerm_11",
-  ``(toTerm d1 = toTerm d2) <=> (d1 = d2)``,
+Theorem toTerm_11[simp] :
+    (toTerm d1 = toTerm d2) <=> (d1 = d2)
+Proof
   SRW_TAC [][EQ_IMP_THM] THEN
   POP_ASSUM (MP_TAC o Q.AP_TERM `fromTerm`) THEN
-  SRW_TAC [][]);
+  SRW_TAC [][]
+QED
 
 val toTerm_onto = store_thm(
   "toTerm_onto",
   ``!t. ?d. toTerm d = t``,
   METIS_TAC [fromTerm_11, fromtoTerm]);
 
-val tofromTerm = Store_thm(
-  "tofromTerm",
-  ``toTerm (fromTerm t) = t``,
-  METIS_TAC [toTerm_onto, toTerm_11, fromtoTerm])
+Theorem tofromTerm[simp] :
+    toTerm (fromTerm t) = t
+Proof
+  METIS_TAC [toTerm_onto, toTerm_11, fromtoTerm]
+QED
 
 val toTerm_eqn = store_thm(
   "toTerm_eqn",
   ``(toTerm x = y) <=> (fromTerm y = x)``,
   SRW_TAC [][EQ_IMP_THM] THEN SRW_TAC [][])
 
-val toTerm_thm = Store_thm(
-  "toTerm_thm",
-  ``(toTerm (dV i) = VAR (n2s i)) /\
+Theorem toTerm_thm[simp] :
+    (toTerm (dV i) = VAR (n2s i)) /\
     (toTerm (dAPP M N) = toTerm M @@ toTerm N) /\
-    (toTerm (dLAM i M) = LAM (n2s i) (toTerm M))``,
-  SRW_TAC [][toTerm_eqn]);
+    (toTerm (dLAM i M) = LAM (n2s i) (toTerm M))
+Proof
+  SRW_TAC [][toTerm_eqn]
+QED
 
 val lemma = prove(
   ``!i j. i + j + 1 NOTIN dFV M ==>
@@ -1015,30 +1050,34 @@ val toTerm_dABS = store_thm(
 
 val _ = overload_on ("is_dABS", ``\d. is_abs (toTerm d)``)
 
-val is_dABS_thm = Store_thm(
-  "is_dABS_thm",
-  ``(is_dABS (dV v) = F) /\
+Theorem is_dABS_thm[simp] :
+    (is_dABS (dV v) = F) /\
     (is_dABS (dAPP d1 d2) = F) /\
     (is_dABS (dABS d) = T) /\
-    (is_dABS (dLAM v d) = T)``,
+    (is_dABS (dLAM v d) = T)
+Proof
   SRW_TAC [][] THEN
   `?i N. dABS d = dLAM i N` by METIS_TAC [dABS_dLAM_exists] THEN
-  SRW_TAC [][]);
-
-val is_dABS_vnsub_invariant = Store_thm(
-  "is_dABS_vnsub_invariant",
-  ``!d i j. is_dABS (nsub (dV i) j d) <=> is_dABS d``,
-  Induct THEN SRW_TAC [][]);
-
-val is_dABS_vsub_invariant = Store_thm(
-  "is_dABS_vsub_invariant",
-  ``!d i j. is_dABS (sub (dV i) j d) <=> is_dABS d``,
-  Induct THEN SRW_TAC [][]);
-
-val is_dABS_lift_invariant = Store_thm(
-  "is_dABS_lift_invariant",
-  ``!d j. is_dABS (lift d j) = is_dABS d``,
-  Induct THEN SRW_TAC [][]);
+  SRW_TAC [][]
+QED
+
+Theorem is_dABS_vnsub_invariant[simp] :
+    !d i j. is_dABS (nsub (dV i) j d) <=> is_dABS d
+Proof
+  Induct THEN SRW_TAC [][]
+QED
+
+Theorem is_dABS_vsub_invariant[simp] :
+    !d i j. is_dABS (sub (dV i) j d) <=> is_dABS d
+Proof
+  Induct THEN SRW_TAC [][]
+QED
+
+Theorem is_dABS_lift_invariant[simp] :
+    !d j. is_dABS (lift d j) = is_dABS d
+Proof
+  Induct THEN SRW_TAC [][]
+QED
 
 val dbnf_def = Define`
   (dbnf (dV i) = T) /\
@@ -1047,35 +1086,41 @@ val dbnf_def = Define`
 `;
 val _ = export_rewrites ["dbnf_def"]
 
-val dbnf_vnsub_invariant = Store_thm(
-  "dbnf_vnsub_invariant",
-  ``!d i j. dbnf (nsub (dV i) j d) <=> dbnf d``,
-  Induct THEN SRW_TAC [][]);
-
-val dbnf_vsub_invariant = Store_thm(
-  "dbnf_vsub_invariant",
-  ``!d i j. dbnf (sub (dV i) j d) <=> dbnf d``,
-  Induct THEN SRW_TAC [][]);
-
-val dbnf_lift_invariant = Store_thm(
-  "dbnf_lift_invariant",
-  ``!d j. dbnf (lift d j) = dbnf d``,
-  Induct THEN SRW_TAC [][]);
-
-val dbnf_dLAM = Store_thm(
-  "dbnf_dLAM",
-  ``dbnf (dLAM i d) = dbnf d``,
-  SRW_TAC [][dLAM_def]);
-
-val dbnf_fromTerm = Store_thm(
-  "dbnf_fromTerm",
-  ``!t. dbnf (fromTerm t) = bnf t``,
-  HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]);
-
-val bnf_toTerm = Store_thm(
-  "bnf_toTerm",
-  ``!d. bnf (toTerm d) = dbnf d``,
-  METIS_TAC [fromTerm_onto, fromtoTerm, dbnf_fromTerm]);
+Theorem dbnf_vnsub_invariant[simp] :
+    !d i j. dbnf (nsub (dV i) j d) <=> dbnf d
+Proof
+  Induct THEN SRW_TAC [][]
+QED
+
+Theorem dbnf_vsub_invariant[simp] :
+    !d i j. dbnf (sub (dV i) j d) <=> dbnf d
+Proof
+  Induct THEN SRW_TAC [][]
+QED
+
+Theorem dbnf_lift_invariant[simp] :
+    !d j. dbnf (lift d j) = dbnf d
+Proof
+  Induct THEN SRW_TAC [][]
+QED
+
+Theorem dbnf_dLAM[simp] :
+    dbnf (dLAM i d) = dbnf d
+Proof
+  SRW_TAC [][dLAM_def]
+QED
+
+Theorem dbnf_fromTerm[simp] :
+    !t. dbnf (fromTerm t) = bnf t
+Proof
+  HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]
+QED
+
+Theorem bnf_toTerm[simp] :
+    !d. bnf (toTerm d) = dbnf d
+Proof
+  METIS_TAC [fromTerm_onto, fromtoTerm, dbnf_fromTerm]
+QED
 
 (* ----------------------------------------------------------------------
     Eta reduction
@@ -1227,4 +1272,269 @@ val eta_eq_lam_eta = store_thm(
   ``eta (fromTerm M) (fromTerm N) = compat_closure eta M N``,
   METIS_TAC [eta_lam_eta, lam_eta_eta]);
 
+(*---------------------------------------------------------------------------*
+ *  Accumulated operators for dB terms (LAMl, appstar, etc.)
+ *---------------------------------------------------------------------------*)
+
+Overload "@*" = “\f args. FOLDL dAPP f args”
+Overload "LAMl" = “\vs t. FOLDR dLAM t vs”
+
+Theorem dappstar_APPEND :
+    (x :pdb) @* (Ms1 ++ Ms2) = (x @* Ms1) @* Ms2
+Proof
+    qid_spec_tac ‘x’ >> Induct_on ‘Ms1’ >> simp[]
+QED
+
+Theorem dappstar_SNOC[simp]:
+    (x :pdb) @* (SNOC M Ms) = dAPP (x @* Ms) M
+Proof
+    simp[dappstar_APPEND, SNOC_APPEND]
+QED
+
+Theorem fromTerm_appstar :
+    !args. fromTerm (f @* args) = fromTerm f @* MAP fromTerm args
+Proof
+    Induct_on ‘args’ using SNOC_INDUCT
+ >> simp [dappstar_SNOC, MAP_SNOC]
+QED
+
+Theorem fromTerm_LAMl :
+    !vs. fromTerm (LAMl vs t) = LAMl (MAP s2n vs) (fromTerm t)
+Proof
+    Induct_on ‘vs’ >> rw []
+QED
+
+(* NOTE: unlike LAMl, there's no need to keep a list of variable names, just the
+         number of nested dABS suffices.
+ *)
+Overload dABSi = “FUNPOW dABS”
+
+Definition isub_def:
+   (isub t [] = (t :pdb)) /\
+   (isub t ((s,x)::rst) = isub ([s/x]t) rst)
+End
+
+Overload ISUB = “isub”
+
+(* NOTE: there's already dFVs_def *)
+Definition dFVS_def :
+   (dFVS [] = {}) /\
+   (dFVS ((t,x)::rst) = dFV t UNION dFVS rst)
+End
+
+Overload FVS = “dFVS”
+
+Theorem FINITE_dFVS[simp] :
+    !phi. FINITE (dFVS phi)
+Proof
+    Induct_on ‘phi’ >| [ALL_TAC, Cases]
+ >> RW_TAC std_ss [dFVS_def, FINITE_EMPTY, FINITE_UNION, FINITE_dFV]
+QED
+
+Theorem dFVS_SNOC :
+    !rst. dFVS (SNOC (t,x) rst) = dFV t UNION dFVS rst
+Proof
+    Induct_on ‘rst’ >- rw [dFVS_def]
+ >> Q.X_GEN_TAC ‘h’ >> Cases_on ‘h’
+ >> rw [dFVS_def]
+ >> SET_TAC []
+QED
+
+Theorem isub_dLAM[simp] :
+    !R x. x NOTIN DOM R /\ x NOTIN dFVS R ==>
+          !t. (dLAM x t) ISUB R = dLAM x (t ISUB R)
+Proof
+    Induct >- rw [isub_def]
+ >> rpt GEN_TAC
+ >> Cases_on ‘h’
+ >> rw [isub_def, pairTheory.FORALL_PROD, DOM_DEF, dFVS_def, sub_def]
+QED
+
+Theorem isub_singleton :
+    !t x u. u ISUB [(t,x)] = [t/x]u:pdb
+Proof
+    SRW_TAC [][isub_def]
+QED
+
+Theorem isub_APPEND :
+    !R1 R2 t:pdb. (t ISUB R1) ISUB R2 = t ISUB (APPEND R1 R2)
+Proof
+    Induct
+ >> ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, isub_def]
+QED
+
+Theorem isub_dAPP :
+    !sub M N. (dAPP M N) ISUB sub = dAPP (M ISUB sub) (N ISUB sub)
+Proof
+    Induct
+ >> ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, isub_def, sub_def]
+QED
+
+Theorem isub_appstar :
+    !args (t:pdb) sub.
+         t @* args ISUB sub = (t ISUB sub) @* MAP (\t. t ISUB sub) args
+Proof
+    Induct >> SRW_TAC [][isub_dAPP]
+QED
+
+Theorem isub_dV_fresh :
+    !y phi. y NOTIN DOM phi ==> (dV y ISUB phi = dV y)
+Proof
+    Q.X_GEN_TAC ‘x’
+ >> Induct_on ‘phi’ >> rw [isub_def]
+ >> Cases_on ‘h’ >> fs [isub_def, DOM_DEF]
+QED
+
+(* cf. lemma14b, ssub_14b, etc. *)
+Theorem isub_14b :
+    !t phi. DISJOINT (DOM phi) (dFV t) ==> (isub t phi = t)
+Proof
+    Induct_on ‘t’
+ >- (rw [DISJOINT_ALT, isub_def] \\
+     MATCH_MP_TAC isub_dV_fresh >> art [])
+ >- (rw [DISJOINT_ALT, isub_dAPP])
+ >> rw [DISJOINT_ALT]
+ >> POP_ASSUM MP_TAC
+ >> Induct_on ‘phi’
+ >- rw [DOM_DEF, isub_def]
+ >> Q.X_GEN_TAC ‘h’
+ >> Cases_on ‘h’
+ >> rw [DOM_DEF, isub_def]
+ >> Know ‘[lift q 0/r + 1] t = t’
+ >- (MATCH_MP_TAC sub_14b \\
+     FIRST_X_ASSUM MATCH_MP_TAC >> rw [])
+ >> Rewr'
+ >> FIRST_X_ASSUM MATCH_MP_TAC
+ >> rw []
+QED
+
+Theorem isub_dV_once_lemma[local] :
+    !l i. ALL_DISTINCT (MAP SND l) /\ i < LENGTH l /\
+         (!j. j < LENGTH l ==> EL j (MAP SND l) NOTIN dFVS l) ==>
+         (dV (EL i (MAP SND l)) ISUB l = EL i (MAP FST l))
+Proof
+    Induct_on ‘l’ >- rw [isub_def]
+ >> Q.X_GEN_TAC ‘h’
+ >> Cases_on ‘h’
+ >> Q.X_GEN_TAC ‘i’
+ >> Cases_on ‘i’ >> rw [isub_def, dFVS_def]
+ >- (MATCH_MP_TAC isub_14b \\
+     rw [DOM_ALT_MAP_SND, DISJOINT_ALT, MEM_MAP, MEM_EL] \\
+     Q.PAT_X_ASSUM ‘!j. j < SUC (LENGTH l) ==> P’ (MP_TAC o (Q.SPEC ‘SUC n’)) \\
+     rw [EL_MAP])
+ (* then a contradictory *)
+ >- (fs [MEM_EL] >> METIS_TAC [])
+ >> FIRST_X_ASSUM MATCH_MP_TAC >> rw []
+ >> Q.PAT_X_ASSUM ‘!j. j < SUC (LENGTH l) ==> P’ (MP_TAC o (Q.SPEC ‘SUC j’))
+ >> rw [EL_MAP]
+QED
+
+(* The antecedents of this theorem is dirty, as it basically tries to void
+   from more than once substitutions by isub.
+ *)
+Theorem isub_dV_once :
+    !Ms Ns y i. ALL_DISTINCT Ns /\ (LENGTH Ms = LENGTH Ns) /\
+                i < LENGTH Ns /\ (y = EL i Ns) /\
+              (!j. j < LENGTH Ns ==> EL j Ns NOTIN (dFVS (ZIP (Ms,Ns)))) ==>
+               (dV y ISUB (ZIP (Ms,Ns)) = EL i Ms)
+Proof
+    rpt STRIP_TAC
+ >> qabbrev_tac ‘l = ZIP (Ms,Ns)’
+ >> ‘Ms = MAP FST l’ by rw [Abbr ‘l’, MAP_ZIP]
+ >> ‘Ns = MAP SND l’ by rw [Abbr ‘l’, MAP_ZIP]
+ >> rw []
+ >> MATCH_MP_TAC isub_dV_once_lemma >> fs []
+QED
+
+Theorem lift_appstar :
+    !Ns. lift (M @* Ns) k = lift M k @* MAP (\e. lift e k) Ns
+Proof
+    Induct_on ‘Ns’ using SNOC_INDUCT
+ >> rw [appstar_SNOC, MAP_SNOC]
+QED
+
+Theorem FOLDL_lift_appstar :
+    !ks M Ns. FOLDL lift (M @* Ns) ks = FOLDL lift M ks @* MAP (\e. FOLDL lift e ks) Ns
+Proof
+    Induct_on ‘ks’
+ >> rw [lift_appstar, MAP_MAP_o, combinTheory.o_DEF]
+QED
+
+Theorem lift_dABSi :
+    !n k. lift (dABSi n t) k = dABSi n (lift t (k + n))
+Proof
+    Induct_on ‘n’ >> rw [lift_def, FUNPOW_SUC, ADD1]
+QED
+
+(* cf. sub_def: |- [s/k] (dABS t) = dABS ([lift s 0/k + 1] t) *)
+Theorem sub_dABSi[simp] :
+    !s k. [s/k] (dABSi n t) = dABSi n ([FUNPOW (\e. lift e 0) n s/k + n] t)
+Proof
+    Induct_on ‘n’ >> rw [lift_def]
+ >> rw [FUNPOW_SUC, ADD1]
+ >> KILL_TAC
+ >> Suff ‘FUNPOW (\e. lift e 0) n (lift s 0) =
+          lift (FUNPOW (\e. lift e 0) n s) 0’ >- rw []
+ >> Induct_on ‘n’
+ >- rw [FUNPOW]
+ >> rw [FUNPOW_SUC]
+QED
+
+(* cf. lift_sub:
+
+   |- n <= i ==> lift ([M/i] N) n = [lift M n/i + 1] (lift N n)
+ *)
+Theorem lift_isub_lemma[local] :
+    !l M. EVERY (\i. n <= i) (MAP SND l) ==>
+      (lift (M ISUB l) n =
+       lift M n ISUB ZIP (MAP (\e. lift e n) (MAP FST l),MAP SUC (MAP SND l)))
+Proof
+    Induct_on ‘l’ >- rw [isub_def]
+ >> Q.X_GEN_TAC ‘h’
+ >> Cases_on ‘h’
+ >> rw [isub_def] >> fs []
+ >> rw [lift_sub, ADD1]
+QED
+
+Theorem lift_isub :
+    !M Ms Ns n. EVERY (\i. n <= i) Ns /\ (LENGTH Ms = LENGTH Ns) ==>
+               (lift (M ISUB (ZIP (Ms,Ns))) n =
+                (lift M n) ISUB (ZIP (MAP (\e. lift e n) Ms,MAP SUC Ns)))
+Proof
+    rpt STRIP_TAC
+ >> qabbrev_tac ‘l = ZIP (Ms,Ns)’
+ >> ‘Ms = MAP FST l’ by rw [Abbr ‘l’, MAP_ZIP]
+ >> ‘Ns = MAP SND l’ by rw [Abbr ‘l’, MAP_ZIP]
+ >> rw []
+ >> MATCH_MP_TAC lift_isub_lemma >> art []
+QED
+
+Theorem isub_SNOC_lemma[local] :
+    !l M. ~MEM k (MAP SND l) ==>
+           (M ISUB ZIP (SNOC s (MAP FST l),SNOC k (MAP SND l)) = [s/k] (M ISUB l))
+Proof
+    Induct_on ‘l’ >- rw [isub_def]
+ >> Q.X_GEN_TAC ‘h’
+ >> Cases_on ‘h’
+ >> rw [isub_def] >> fs []
+QED
+
+Theorem isub_SNOC :
+    !M Ms Ns s k. ~MEM k Ns /\ (LENGTH Ms = LENGTH Ns) ==>
+                 (M ISUB ZIP (SNOC s Ms,SNOC k Ns) = [s/k] (M ISUB ZIP (Ms,Ns)))
+Proof
+    rpt STRIP_TAC
+ >> qabbrev_tac ‘l = ZIP (Ms,Ns)’
+ >> ‘Ms = MAP FST l’ by rw [Abbr ‘l’, MAP_ZIP]
+ >> ‘Ns = MAP SND l’ by rw [Abbr ‘l’, MAP_ZIP]
+ >> rw []
+ >> MATCH_MP_TAC isub_SNOC_lemma >> art []
+QED
+
 val _ = export_theory();
+val _ = html_theory "pure_dB";
+
+(* References:
+
+   [1] Nipkow, T.: More Church-Rosser Proofs. J. Autom. Reason. (2001).
+ *)
diff --git a/src/list/src/listScript.sml b/src/list/src/listScript.sml
index 64a6a24086..6f00e9b023 100644
--- a/src/list/src/listScript.sml
+++ b/src/list/src/listScript.sml
@@ -1821,6 +1821,13 @@ val LENGTH_FRONT_CONS = store_thm ("LENGTH_FRONT_CONS",
 Induct_on ‘xs’ THEN ASM_SIMP_TAC bool_ss [FRONT_CONS, LENGTH])
 val _ = export_rewrites ["LENGTH_FRONT_CONS"]
 
+Theorem LENGTH_FRONT :
+    !l. l <> [] ==> LENGTH (FRONT l) = PRE (LENGTH l)
+Proof
+    rpt STRIP_TAC
+ >> Cases_on ‘l’ >> fs [LENGTH_FRONT_CONS]
+QED
+
 val FRONT_CONS_EQ_NIL = store_thm ("FRONT_CONS_EQ_NIL",
 “(!x:'a xs. (FRONT (x::xs) = []) = (xs = [])) /\
   (!x:'a xs. ([] = FRONT (x::xs)) = (xs = [])) /\
@@ -2759,6 +2766,23 @@ val SNOC_Axiom = store_thm(
 val SNOC_INDUCT = save_thm("SNOC_INDUCT", prove_induction_thm SNOC_Axiom_old);
 val SNOC_CASES =  save_thm("SNOC_CASES", hd (prove_cases_thm SNOC_INDUCT));
 
+Theorem ZIP_SNOC_lemma[local] :
+    ZIP (SNOC x1 (MAP FST l),SNOC x2 (MAP SND l)) = SNOC (x1,x2) l
+Proof
+    Induct_on ‘l’ >> rw [ZIP_def]
+QED
+
+Theorem ZIP_SNOC :
+    !x1 l1 x2 l2. (LENGTH l1 = LENGTH l2) ==>
+                  (ZIP (SNOC x1 l1,SNOC x2 l2) = SNOC (x1,x2) (ZIP (l1,l2)))
+Proof
+    rpt STRIP_TAC
+ >> Q.ABBREV_TAC ‘l = ZIP (l1,l2)’
+ >> ‘l1 = MAP FST l’ by rw [Abbr ‘l’, MAP_ZIP]
+ >> ‘l2 = MAP SND l’ by rw [Abbr ‘l’, MAP_ZIP]
+ >> rw [ZIP_SNOC_lemma]
+QED
+
 (*--------------------------------------------------------------*)
 (* List generator                                               *)
 (*  GENLIST f n = [f 0;...; f(n-1)]                             *)
diff --git a/src/relation/relationScript.sml b/src/relation/relationScript.sml
index 72e97b6275..138dfff24e 100644
--- a/src/relation/relationScript.sml
+++ b/src/relation/relationScript.sml
@@ -2350,4 +2350,36 @@ val Newmans_lemma = store_thm(
   `TC R x x0` by PROVE_TAC [EXTEND_RTC_TC] THEN
   PROVE_TAC [RTC_RTC]);
 
+Theorem RUNION_RTC_MONOTONE :
+    !R1 x y. RTC R1 x y ==> !R2. RTC (R1 RUNION R2) x y
+Proof
+  GEN_TAC THEN HO_MATCH_MP_TAC RTC_INDUCT THEN
+  PROVE_TAC [RTC_RULES, RUNION]
+QED
+
+Theorem RTC_RUNION :
+    !R1 R2. RTC (RTC R1 RUNION RTC R2) = RTC (R1 RUNION R2)
+Proof
+  REPEAT GEN_TAC THEN
+  Q_TAC SUFF_TAC
+    `(!x y. RTC (RTC R1 RUNION RTC R2) x y ==> RTC (R1 RUNION R2) x y) /\
+     (!x y. RTC (R1 RUNION R2) x y ==> RTC (RTC R1 RUNION RTC R2) x y)` THEN1
+    (SIMP_TAC (srw_ss()) [FUN_EQ_THM, EQ_IMP_THM, FORALL_AND_THM] THEN
+     PROVE_TAC []) THEN CONJ_TAC
+  THEN HO_MATCH_MP_TAC RTC_INDUCT THENL [
+    CONJ_TAC THENL [
+      PROVE_TAC [RTC_RULES],
+      MAP_EVERY Q.X_GEN_TAC [`x`,`y`,`z`] THEN REPEAT STRIP_TAC THEN
+      `RTC R1 x y \/ RTC R2 x y` by PROVE_TAC [RUNION] THEN
+      PROVE_TAC [RUNION_RTC_MONOTONE, RTC_RTC, RUNION_COMM]
+    ],
+    CONJ_TAC THENL [
+      PROVE_TAC [RTC_RULES],
+      MAP_EVERY Q.X_GEN_TAC [`x`,`y`,`z`] THEN REPEAT STRIP_TAC THEN
+      `R1 x y \/ R2 x y` by PROVE_TAC [RUNION] THEN
+      PROVE_TAC [RTC_RULES, RUNION]
+    ]
+  ]
+QED
+
 val _ = export_theory();

From 4815c6213702dbbea0ccf951b330076c88317ecb Mon Sep 17 00:00:00 2001
From: Chun Tian <binghe.lisp@gmail.com>
Date: Wed, 25 Oct 2023 01:39:58 +1100
Subject: [PATCH 2/4] Some theorems in churchnumScript.sml were moved upwards

---
 .../computability/lambda/churchnumScript.sml  | 22 +++----------------
 1 file changed, 3 insertions(+), 19 deletions(-)

diff --git a/examples/computability/lambda/churchnumScript.sml b/examples/computability/lambda/churchnumScript.sml
index 338ac0fdf9..8cd1f27f19 100644
--- a/examples/computability/lambda/churchnumScript.sml
+++ b/examples/computability/lambda/churchnumScript.sml
@@ -1,8 +1,8 @@
 open HolKernel boolLib bossLib Parse binderLib
 
 open chap3Theory
-open pred_setTheory
-open termTheory
+open arithmeticTheory pred_setTheory
+open termTheory appFOLDLTheory;
 open boolSimps
 open normal_orderTheory
 open churchboolTheory
@@ -14,21 +14,10 @@ fun Store_thm(n,t,tac) = store_thm(n,t,tac) before export_rewrites [n]
 
 val _ = new_theory "churchnum"
 
-val _ = set_trace "Unicode" 1
-
 val church_def = Define`
   church n = LAM "z" (LAM "s" (FUNPOW (APP (VAR "s")) n (VAR "z")))
 `
 
-val FUNPOW_SUC = arithmeticTheory.FUNPOW_SUC
-
-val size_funpow = store_thm(
-  "size_funpow",
-  ``size (FUNPOW (APP f) n x) = (size f + 1) * n + size x``,
-  Induct_on `n` THEN
-  SRW_TAC [ARITH_ss][FUNPOW_SUC, arithmeticTheory.LEFT_ADD_DISTRIB,
-                     arithmeticTheory.MULT_CLAUSES]);
-
 val church_11 = store_thm(
   "church_11",
   ``(church m = church n) ⇔ (m = n)``,
@@ -872,12 +861,6 @@ val cfindbody_11 = Store_thm(
       by SRW_TAC [][fresh_cfindbody] THEN
   SRW_TAC [][AC CONJ_ASSOC CONJ_COMM]);
 
-val lameq_triangle = store_thm(
-  "lameq_triangle",
-  ``M == N ∧ M == P ∧ bnf N ∧ bnf P ⇒ (N = P)``,
-  METIS_TAC [chap3Theory.betastar_lameq_bnf, chap2Theory.lameq_rules,
-             chap3Theory.bnf_reduction_to_self]);
-
 val cfindleast_bnfE = store_thm(
   "cfindleast_bnfE",
   ``(∀n. ∃b. P @@ church n == cB b) ∧
@@ -952,3 +935,4 @@ Proof
 QED
 
 val _ = export_theory()
+val _ = html_theory "churchnum";

From 5ccecf896fd0d68f5f37d584590be110f52530ce Mon Sep 17 00:00:00 2001
From: Chun Tian <binghe.lisp@gmail.com>
Date: Wed, 25 Oct 2023 11:14:48 +1100
Subject: [PATCH 3/4] Autoclean generated HTML files under
 examples/computability/lambda

---
 examples/computability/lambda/Holmakefile | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/examples/computability/lambda/Holmakefile b/examples/computability/lambda/Holmakefile
index fd982b87cc..ca43cead66 100644
--- a/examples/computability/lambda/Holmakefile
+++ b/examples/computability/lambda/Holmakefile
@@ -4,7 +4,8 @@ OPTIONS = QUIT_ON_FAILURE
 
 ifdef POLY
 HOLHEAP = computability-heap
-EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o
+EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o \
+	$(patsubst %Theory.uo,%Theory.html,$(DEFAULT_TARGETS))
 
 BARE_THYS = ../../lambda/barendregt/normal_orderTheory \
             ../../lambda/other-models/pure_dBTheory

From 93abf6c419742d5e9b780827e7f2cdabffb404c8 Mon Sep 17 00:00:00 2001
From: Chun Tian <binghe.lisp@gmail.com>
Date: Wed, 25 Oct 2023 11:30:54 +1100
Subject: [PATCH 4/4] Renamed LAMl (overloaded for dB terms) to dLAMl (to avoid
 confusing)

---
 .../lambda/completeness/boehm_treeScript.sml   | 18 +++++++++---------
 examples/lambda/other-models/pure_dBScript.sml |  4 ++--
 2 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/examples/lambda/completeness/boehm_treeScript.sml b/examples/lambda/completeness/boehm_treeScript.sml
index 1ff2dd0677..60fc697118 100644
--- a/examples/lambda/completeness/boehm_treeScript.sml
+++ b/examples/lambda/completeness/boehm_treeScript.sml
@@ -24,7 +24,7 @@ Proof
     rw [o_DEF]
 QED
 
-(* Translations from LAMl to dABSi.
+(* Translations from dLAMl to dABSi.
 
    Some samples for guessing out the statements of this theorem:
 
@@ -45,12 +45,12 @@ QED
                        ([dV 0/v0 + 3]
                           (lift (lift (lift t 0) 1) 2)))))): thm
  *)
-Theorem LAMl_to_dABSi :
+Theorem dLAMl_to_dABSi :
     !vs. ALL_DISTINCT (vs :num list) ==>
          let n = LENGTH vs;
              body = FOLDL lift t (GENLIST I n);
              phi = ZIP (GENLIST dV n, MAP (\i. i + n) (REVERSE vs))
-         in LAMl vs t = dABSi n (body ISUB phi)
+         in dLAMl vs t = dABSi n (body ISUB phi)
 Proof
     Induct_on ‘vs’ >- rw [isub_def]
  >> rw [isub_def, GSYM SNOC_APPEND, MAP_SNOC, FUNPOW_SUC, GENLIST, FOLDL_SNOC,
@@ -58,7 +58,7 @@ Proof
  >> fs []
  >> qabbrev_tac ‘n = LENGTH vs’
  >> rw [lift_dABSi]
- >> Q.PAT_X_ASSUM ‘LAMl vs t = _’ K_TAC
+ >> Q.PAT_X_ASSUM ‘dLAMl vs t = _’ K_TAC
  >> qabbrev_tac ‘N = FOLDL lift t (GENLIST I n)’
  >> qabbrev_tac ‘Ms = GENLIST dV n’
  >> qabbrev_tac ‘Vs = MAP (\i. i + n) (REVERSE vs)’
@@ -92,13 +92,13 @@ QED
 
 (* |- !t vs.
         ALL_DISTINCT vs ==>
-        LAMl vs t =
+        dLAMl vs t =
         dABSi (LENGTH vs)
           (FOLDL lift t (GENLIST I (LENGTH vs)) ISUB
            ZIP (GENLIST dV (LENGTH vs),MAP (\i. i + LENGTH vs) (REVERSE vs)))
  *)
-Theorem LAMl_to_dABSi_applied[local] =
-    GEN_ALL (SIMP_RULE std_ss [LET_DEF] LAMl_to_dABSi)
+Theorem dLAMl_to_dABSi_applied[local] =
+    GEN_ALL (SIMP_RULE std_ss [LET_DEF] dLAMl_to_dABSi)
 
 (* dB version of hnf_cases (only the ==> direction) *)
 Theorem dhnf_cases :
@@ -114,12 +114,12 @@ Proof
  >> qabbrev_tac ‘vs' = MAP s2n vs’
  >> qabbrev_tac ‘Ms = MAP fromTerm args’
  >> qabbrev_tac ‘y' = s2n y’
- >> Know ‘LAMl vs' (dV y' @* Ms) =
+ >> Know ‘dLAMl vs' (dV y' @* Ms) =
           dABSi (LENGTH vs')
             (FOLDL lift (dV y' @* Ms) (GENLIST I (LENGTH vs')) ISUB
              ZIP (GENLIST dV (LENGTH vs'),
                   MAP (\i. i + LENGTH vs') (REVERSE vs')))’
- >- (MATCH_MP_TAC LAMl_to_dABSi_applied \\
+ >- (MATCH_MP_TAC dLAMl_to_dABSi_applied \\
      qunabbrev_tac ‘vs'’ \\
      MATCH_MP_TAC ALL_DISTINCT_MAP_INJ >> rw [])
  >> ‘LENGTH vs' = n’ by rw [Abbr ‘vs'’] >> POP_ORW
diff --git a/examples/lambda/other-models/pure_dBScript.sml b/examples/lambda/other-models/pure_dBScript.sml
index cc9fd06e58..fa4e703b0d 100644
--- a/examples/lambda/other-models/pure_dBScript.sml
+++ b/examples/lambda/other-models/pure_dBScript.sml
@@ -1277,7 +1277,7 @@ val eta_eq_lam_eta = store_thm(
  *---------------------------------------------------------------------------*)
 
 Overload "@*" = “\f args. FOLDL dAPP f args”
-Overload "LAMl" = “\vs t. FOLDR dLAM t vs”
+Overload "dLAMl" = “\vs t. FOLDR dLAM t vs”
 
 Theorem dappstar_APPEND :
     (x :pdb) @* (Ms1 ++ Ms2) = (x @* Ms1) @* Ms2
@@ -1299,7 +1299,7 @@ Proof
 QED
 
 Theorem fromTerm_LAMl :
-    !vs. fromTerm (LAMl vs t) = LAMl (MAP s2n vs) (fromTerm t)
+    !vs. fromTerm (LAMl vs t) = dLAMl (MAP s2n vs) (fromTerm t)
 Proof
     Induct_on ‘vs’ >> rw []
 QED