Start working on more general fixed-point combinators

1 files changed, 225 insertions, 0 deletions

diff --git a/backends/hol4/divDefProto2Theory.sig b/backends/hol4/divDefProto2Theory.sig
new file mode 100644
index 00000000..349aabf7
--- /dev/null
+++ b/backends/hol4/divDefProto2Theory.sig
@@ -0,0 +1,225 @@
+signature divDefProto2Theory =
+sig
+  type thm = Thm.thm
+  
+  (*  Definitions  *)
+    val fix_def : thm
+    val fix_fuel_P_def : thm
+    val fix_fuel_def : thm
+    val ftree_TY_DEF : thm
+    val ftree_case_def : thm
+    val ftree_size_def : thm
+    val is_valid_fp_body_def : thm
+  
+  (*  Theorems  *)
+    val datatype_ftree : thm
+    val eval_ftree_compute : thm
+    val eval_ftree_def : thm
+    val eval_ftree_ind : thm
+    val fix_fuel_compute : thm
+    val ftree_11 : thm
+    val ftree_Axiom : thm
+    val ftree_case_cong : thm
+    val ftree_case_eq : thm
+    val ftree_distinct : thm
+    val ftree_induction : thm
+    val ftree_nchotomy : thm
+    val ftree_size_eq : thm
+  
+  val divDefProto2_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+   [primitives] Parent theory of "divDefProto2"
+   
+   [fix_def]  Definition
+      
+      ⊢ ∀f x.
+          fix f x =
+          if ∃n. fix_fuel_P f x n then
+            fix_fuel ($LEAST (fix_fuel_P f x)) f x
+          else Diverge
+   
+   [fix_fuel_P_def]  Definition
+      
+      ⊢ ∀f x n. fix_fuel_P f x n ⇔ ¬is_diverge (fix_fuel n f x)
+   
+   [fix_fuel_def]  Definition
+      
+      ⊢ (∀f x. fix_fuel 0 f x = Diverge) ∧
+        ∀n f x. fix_fuel (SUC n) f x = f (fix_fuel n f) x
+   
+   [ftree_TY_DEF]  Definition
+      
+      ⊢ ∃rep.
+          TYPE_DEFINITION
+            (λa0'.
+                 ∀ $var$('ftree') $var$('@temp @ind_typedivDefProto20prod')
+                     $var$('@temp @ind_typedivDefProto21list').
+                   (∀a0'.
+                      (∃a. a0' =
+                           (λa.
+                                ind_type$CONSTR 0 (ARB,ARB)
+                                  (ind_type$FCONS a (λn. ind_type$BOTTOM)))
+                             a ∧
+                           $var$('@temp @ind_typedivDefProto20prod') a) ∨
+                      (∃a. a0' =
+                           (λa.
+                                ind_type$CONSTR (SUC 0) (a,ARB)
+                                  (λn. ind_type$BOTTOM)) a) ⇒
+                      $var$('ftree') a0') ∧
+                   (∀a1'.
+                      (∃a0 a1.
+                         a1' =
+                         (λa0 a1.
+                              ind_type$CONSTR (SUC (SUC 0)) (ARB,a0)
+                                (ind_type$FCONS a1 (λn. ind_type$BOTTOM)))
+                           a0 a1 ∧
+                         $var$('@temp @ind_typedivDefProto21list') a1) ⇒
+                      $var$('@temp @ind_typedivDefProto20prod') a1') ∧
+                   (∀a2.
+                      a2 =
+                      ind_type$CONSTR (SUC (SUC (SUC 0))) (ARB,ARB)
+                        (λn. ind_type$BOTTOM) ∨
+                      (∃a0 a1.
+                         a2 =
+                         (λa0 a1.
+                              ind_type$CONSTR (SUC (SUC (SUC (SUC 0))))
+                                (ARB,ARB)
+                                (ind_type$FCONS a0
+                                   (ind_type$FCONS a1 (λn. ind_type$BOTTOM))))
+                           a0 a1 ∧ $var$('ftree') a0 ∧
+                         $var$('@temp @ind_typedivDefProto21list') a1) ⇒
+                      $var$('@temp @ind_typedivDefProto21list') a2) ⇒
+                   $var$('ftree') a0') rep
+   
+   [ftree_case_def]  Definition
+      
+      ⊢ (∀a f f1. ftree_CASE (Rec a) f f1 = f a) ∧
+        ∀a f f1. ftree_CASE (NRec a) f f1 = f1 a
+   
+   [ftree_size_def]  Definition
+      
+      ⊢ (∀f a. ftree_size f (Rec a) = 1 + ftree1_size f a) ∧
+        (∀f a. ftree_size f (NRec a) = 1) ∧
+        (∀f a0 a1. ftree1_size f (a0,a1) = 1 + ftree2_size f a1) ∧
+        (∀f. ftree2_size f [] = 0) ∧
+        ∀f a0 a1.
+          ftree2_size f (a0::a1) = 1 + (ftree_size f a0 + ftree2_size f a1)
+   
+   [is_valid_fp_body_def]  Definition
+      
+      ⊢ ∀f. is_valid_fp_body f ⇔ ∀x. ∃n ft. ∀g. f g x = eval_ftree n g ft
+   
+   [datatype_ftree]  Theorem
+      
+      ⊢ DATATYPE (ftree Rec NRec)
+   
+   [eval_ftree_compute]  Theorem
+      
+      ⊢ (∀x g fs. eval_ftree 0 g (fs,x) = Diverge) ∧
+        (∀x n g fs.
+           eval_ftree (NUMERAL (BIT1 n)) g (fs,x) =
+           case x of
+             INL r => r
+           | INR (y,i) =>
+             case g y of
+               Return z =>
+                 (let
+                    f = EL i fs
+                  in
+                    eval_ftree (NUMERAL (BIT1 n) − 1) g (fs,f z))
+             | Fail e => Fail e
+             | Diverge => Diverge) ∧
+        ∀x n g fs.
+          eval_ftree (NUMERAL (BIT2 n)) g (fs,x) =
+          case x of
+            INL r => r
+          | INR (y,i) =>
+            case g y of
+              Return z =>
+                (let
+                   f = EL i fs
+                 in
+                   eval_ftree (NUMERAL (BIT1 n)) g (fs,f z))
+            | Fail e => Fail e
+            | Diverge => Diverge
+   
+   [eval_ftree_def]  Theorem
+      
+      ⊢ (∀x g fs. eval_ftree 0 g (fs,x) = Diverge) ∧
+        ∀x n g fs.
+          eval_ftree (SUC n) g (fs,x) =
+          case x of
+            INL r => r
+          | INR (y,i) =>
+            case g y of
+              Return z => (let f = EL i fs in eval_ftree n g (fs,f z))
+            | Fail e => Fail e
+            | Diverge => Diverge
+   
+   [eval_ftree_ind]  Theorem
+      
+      ⊢ ∀P. (∀g fs x. P 0 g (fs,x)) ∧
+            (∀n g fs x.
+               (∀v1 y i z f.
+                  x = INR v1 ∧ v1 = (y,i) ∧ g y = Return z ∧ f = EL i fs ⇒
+                  P n g (fs,f z)) ⇒
+               P (SUC n) g (fs,x)) ⇒
+            ∀v v1 v2 v3. P v v1 (v2,v3)
+   
+   [fix_fuel_compute]  Theorem
+      
+      ⊢ (∀f x. fix_fuel 0 f x = Diverge) ∧
+        (∀n f x.
+           fix_fuel (NUMERAL (BIT1 n)) f x =
+           f (fix_fuel (NUMERAL (BIT1 n) − 1) f) x) ∧
+        ∀n f x.
+          fix_fuel (NUMERAL (BIT2 n)) f x =
+          f (fix_fuel (NUMERAL (BIT1 n)) f) x
+   
+   [ftree_11]  Theorem
+      
+      ⊢ (∀a a'. Rec a = Rec a' ⇔ a = a') ∧ ∀a a'. NRec a = NRec a' ⇔ a = a'
+   
+   [ftree_Axiom]  Theorem
+      
+      ⊢ ∀f0 f1 f2 f3 f4. ∃fn0 fn1 fn2.
+          (∀a. fn0 (Rec a) = f0 a (fn1 a)) ∧ (∀a. fn0 (NRec a) = f1 a) ∧
+          (∀a0 a1. fn1 (a0,a1) = f2 a0 a1 (fn2 a1)) ∧ fn2 [] = f3 ∧
+          ∀a0 a1. fn2 (a0::a1) = f4 a0 a1 (fn0 a0) (fn2 a1)
+   
+   [ftree_case_cong]  Theorem
+      
+      ⊢ ∀M M' f f1.
+          M = M' ∧ (∀a. M' = Rec a ⇒ f a = f' a) ∧
+          (∀a. M' = NRec a ⇒ f1 a = f1' a) ⇒
+          ftree_CASE M f f1 = ftree_CASE M' f' f1'
+   
+   [ftree_case_eq]  Theorem
+      
+      ⊢ ftree_CASE x f f1 = v ⇔
+        (∃p. x = Rec p ∧ f p = v) ∨ ∃f'. x = NRec f' ∧ f1 f' = v
+   
+   [ftree_distinct]  Theorem
+      
+      ⊢ ∀a' a. Rec a ≠ NRec a'
+   
+   [ftree_induction]  Theorem
+      
+      ⊢ ∀P0 P1 P2.
+          (∀p. P1 p ⇒ P0 (Rec p)) ∧ (∀f. P0 (NRec f)) ∧
+          (∀l. P2 l ⇒ ∀f. P1 (f,l)) ∧ P2 [] ∧
+          (∀f l. P0 f ∧ P2 l ⇒ P2 (f::l)) ⇒
+          (∀f. P0 f) ∧ (∀p. P1 p) ∧ ∀l. P2 l
+   
+   [ftree_nchotomy]  Theorem
+      
+      ⊢ ∀ff. (∃p. ff = Rec p) ∨ ∃f. ff = NRec f
+   
+   [ftree_size_eq]  Theorem
+      
+      ⊢ ftree1_size f = pair_size (λv. 0) (list_size (ftree_size f)) ∧
+        ftree2_size f = list_size (ftree_size f)
+   
+   
+*)
+end