Renamed to completeTheory

binghe · Dec 9, 2024 · 1fa9941 · 1fa9941
1 parent d9a6440
commit 1fa9941
Show file tree

Hide file tree

Showing 2 changed files with 30 additions and 12 deletions.
diff --git a/examples/lambda/barendregt/boehmScript.sml b/examples/lambda/barendregt/boehmScript.sml
@@ -26,10 +26,13 @@ val _ = enable_monad "option";
 (* create the theory *)
 val _ = new_theory "boehm";
 
-val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"];
-
 (* These theorems usually give unexpected results, should be applied manually *)
-val _ = temp_delsimps ["IN_UNION", "APPEND_ASSOC"];
+val _ = temp_delsimps [
+   "lift_disj_eq", "lift_imp_disj",
+   "IN_UNION",     (* |- !s t x. x IN s UNION t <=> x IN s \/ x IN t *)
+   "APPEND_ASSOC", (* |- !l1 l2 l3. l1 ++ (l2 ++ l3) = l1 ++ l2 ++ l3 *)
+   "SNOC_APPEND"   (* |- !x l. SNOC x l = l ++ [x] *)
+];
 
 val _ = hide "B";
 val _ = hide "C";

diff --git a/.../lambda/barendregt/completenessScript.sml → ...ples/lambda/barendregt/completeScript.sml b/.../lambda/barendregt/completenessScript.sml → ...ples/lambda/barendregt/completeScript.sml
@@ -1,5 +1,5 @@
 (* ========================================================================== *)
-(* FILE    : completenessScript.sml                                           *)
+(* FILE    : completeScript.sml                                               *)
 (* TITLE   : Completeness of (Untyped) Lambda-Calculus [1, Chapter 10.4]      *)
 (*                                                                            *)
 (* AUTHORS : 2024-2025 The Australian National University (Chun TIAN)         *)
@@ -9,16 +9,26 @@ open HolKernel Parse boolLib bossLib;
 
 open hurdUtils arithmeticTheory pred_setTheory listTheory rich_listTheory;
 
-open termTheory basic_swapTheory appFOLDLTheory chap2Theory solvableTheory
-     head_reductionTheory head_reductionLib boehmTheory;
+open termTheory basic_swapTheory appFOLDLTheory chap2Theory chap3Theory
+     horeductionTheory solvableTheory head_reductionTheory head_reductionLib
+     boehmTheory;
 
-val _ = temp_delsimps
-         ["lift_disj_eq", "lift_imp_disj", "IN_UNION", "APPEND_ASSOC"];
+val _ = new_theory "complete";
+
+val _ = temp_delsimps [
+   "lift_disj_eq", "lift_imp_disj",
+   "IN_UNION",     (* |- !s t x. x IN s UNION t <=> x IN s \/ x IN t *)
+   "APPEND_ASSOC", (* |- !l1 l2 l3. l1 ++ (l2 ++ l3) = l1 ++ l2 ++ l3 *)
+   "SNOC_APPEND"   (* |- !x l. SNOC x l = l ++ [x] *)
+];
 
 Overload FV  = “supp term_pmact”
 Overload VAR = “term$VAR”
 
-val _ = new_theory "completeness";
+val _ = hide "B";
+val _ = hide "C";
+val _ = hide "W";
+val _ = hide "Y";
 
 (* Definition 10.3.10 (iii) and (iv) [1, p.251]
 
@@ -756,10 +766,15 @@ QED
 *)
 
 val _ = export_theory ();
-val _ = html_theory "completeness";
+val _ = html_theory "complete";
 
 (* References:
 
-   [1] Barendregt, H.P.: The lambda calculus, its syntax and semantics.
-       College Publications, London (1984).
+ [1] Barendregt, H.P.: The lambda calculus, its syntax and semantics.
+     College Publications, London (1984).
+ [2] https://en.wikipedia.org/wiki/Corrado_Böhm (UOK)
+ [3] Böhm, C.: Alcune proprietà delle forme β-η-normali nel λ-K-calcolo. (UOK)
+     Pubblicazioni dell'IAC 696, 1-19 (1968)
+     English translation: "Some properties of beta-eta-normal forms in the
+     lambda-K-calculus".
  *)