Initial boehm_treeTheory (up to dhnf_cases)

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";

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

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).
  *)

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).
+ *)

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 *)
 
 (* ----------------------------------------------------------------------

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";