From 266bb06fea0a3ed22aad8b5862b502cb621714ac Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 3 Feb 2023 19:49:49 +0100
Subject: Start working on a version of divDefLib which uses fixed point
 combinators

---
 backends/hol4/divDefProtoTheory.sig | 210 ++++++++++++++++++++++++++++++++++++
 1 file changed, 210 insertions(+)
 create mode 100644 backends/hol4/divDefProtoTheory.sig

(limited to 'backends/hol4/divDefProtoTheory.sig')

diff --git a/backends/hol4/divDefProtoTheory.sig b/backends/hol4/divDefProtoTheory.sig
new file mode 100644
index 00000000..6e4e5950
--- /dev/null
+++ b/backends/hol4/divDefProtoTheory.sig
@@ -0,0 +1,210 @@
+signature divDefProtoTheory =
+sig
+  type thm = Thm.thm
+  
+  (*  Definitions  *)
+    val fix_def : thm
+    val fix_fuel_P_def : thm
+    val fix_fuel_def : thm
+    val is_valid_fp_body_def : thm
+    val list_t_TY_DEF : thm
+    val list_t_case_def : thm
+    val list_t_size_def : thm
+    val nth_body_def : thm
+  
+  (*  Theorems  *)
+    val datatype_list_t : thm
+    val fix_fixed_diverges : thm
+    val fix_fixed_eq : thm
+    val fix_fixed_terminates : thm
+    val fix_fixed_termination_rec_case : thm
+    val fix_fuel_compute : thm
+    val fix_fuel_mono : thm
+    val fix_fuel_mono_least : thm
+    val is_valid_suffice : thm
+    val list_t_11 : thm
+    val list_t_Axiom : thm
+    val list_t_case_cong : thm
+    val list_t_case_eq : thm
+    val list_t_distinct : thm
+    val list_t_induction : thm
+    val list_t_nchotomy : thm
+    val nth_body_is_valid : thm
+    val nth_def : thm
+  
+  val divDefProto_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+   [primitives] Parent theory of "divDefProto"
+   
+   [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
+   
+   [is_valid_fp_body_def]  Definition
+      
+      ⊢ ∀f. is_valid_fp_body f ⇔
+            ∀x. (∀g h. f g x = f h x) ∨ ∃y. ∀g. f g x = g y
+   
+   [list_t_TY_DEF]  Definition
+      
+      ⊢ ∃rep.
+          TYPE_DEFINITION
+            (λa0'.
+                 ∀ $var$('list_t').
+                   (∀a0'.
+                      (∃a0 a1.
+                         a0' =
+                         (λa0 a1.
+                              ind_type$CONSTR 0 a0
+                                (ind_type$FCONS a1 (λn. ind_type$BOTTOM)))
+                           a0 a1 ∧ $var$('list_t') a1) ∨
+                      a0' =
+                      ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒
+                      $var$('list_t') a0') ⇒
+                   $var$('list_t') a0') rep
+   
+   [list_t_case_def]  Definition
+      
+      ⊢ (∀a0 a1 f v. list_t_CASE (ListCons a0 a1) f v = f a0 a1) ∧
+        ∀f v. list_t_CASE ListNil f v = v
+   
+   [list_t_size_def]  Definition
+      
+      ⊢ (∀f a0 a1.
+           list_t_size f (ListCons a0 a1) = 1 + (f a0 + list_t_size f a1)) ∧
+        ∀f. list_t_size f ListNil = 0
+   
+   [nth_body_def]  Definition
+      
+      ⊢ ∀f x.
+          nth_body f x =
+          (let
+             (ls,i) = x
+           in
+             case ls of
+               ListCons x tl =>
+                 if u32_to_int i = 0 then Return x
+                 else do i0 <- u32_sub i (int_to_u32 1); f (tl,i0) od
+             | ListNil => Fail Failure)
+   
+   [datatype_list_t]  Theorem
+      
+      ⊢ DATATYPE (list_t ListCons ListNil)
+   
+   [fix_fixed_diverges]  Theorem
+      
+      ⊢ ∀f. is_valid_fp_body f ⇒
+            ∀x. ¬(∃n. fix_fuel_P f x n) ⇒ fix f x = f (fix f) x
+   
+   [fix_fixed_eq]  Theorem
+      
+      ⊢ ∀f. is_valid_fp_body f ⇒ ∀x. fix f x = f (fix f) x
+   
+   [fix_fixed_terminates]  Theorem
+      
+      ⊢ ∀f. is_valid_fp_body f ⇒
+            ∀x n. fix_fuel_P f x n ⇒ fix f x = f (fix f) x
+   
+   [fix_fixed_termination_rec_case]  Theorem
+      
+      ⊢ ∀x y n m.
+          is_valid_fp_body f ⇒
+          (∀g. f g x = g y) ⇒
+          fix_fuel_P f x n ⇒
+          fix_fuel_P f y m ⇒
+          fix_fuel ($LEAST (fix_fuel_P f x)) f x =
+          fix_fuel ($LEAST (fix_fuel_P f y)) f y
+   
+   [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
+   
+   [fix_fuel_mono]  Theorem
+      
+      ⊢ ∀f. is_valid_fp_body f ⇒
+            ∀n x.
+              fix_fuel_P f x n ⇒
+              ∀m. n ≤ m ⇒ fix_fuel n f x = fix_fuel m f x
+   
+   [fix_fuel_mono_least]  Theorem
+      
+      ⊢ ∀f. is_valid_fp_body f ⇒
+            ∀n x.
+              fix_fuel_P f x n ⇒
+              fix_fuel n f x = fix_fuel ($LEAST (fix_fuel_P f x)) f x
+   
+   [is_valid_suffice]  Theorem
+      
+      ⊢ ∃y. ∀g. g x = g y
+   
+   [list_t_11]  Theorem
+      
+      ⊢ ∀a0 a1 a0' a1'.
+          ListCons a0 a1 = ListCons a0' a1' ⇔ a0 = a0' ∧ a1 = a1'
+   
+   [list_t_Axiom]  Theorem
+      
+      ⊢ ∀f0 f1. ∃fn.
+          (∀a0 a1. fn (ListCons a0 a1) = f0 a0 a1 (fn a1)) ∧
+          fn ListNil = f1
+   
+   [list_t_case_cong]  Theorem
+      
+      ⊢ ∀M M' f v.
+          M = M' ∧ (∀a0 a1. M' = ListCons a0 a1 ⇒ f a0 a1 = f' a0 a1) ∧
+          (M' = ListNil ⇒ v = v') ⇒
+          list_t_CASE M f v = list_t_CASE M' f' v'
+   
+   [list_t_case_eq]  Theorem
+      
+      ⊢ list_t_CASE x f v = v' ⇔
+        (∃t l. x = ListCons t l ∧ f t l = v') ∨ x = ListNil ∧ v = v'
+   
+   [list_t_distinct]  Theorem
+      
+      ⊢ ∀a1 a0. ListCons a0 a1 ≠ ListNil
+   
+   [list_t_induction]  Theorem
+      
+      ⊢ ∀P. (∀l. P l ⇒ ∀t. P (ListCons t l)) ∧ P ListNil ⇒ ∀l. P l
+   
+   [list_t_nchotomy]  Theorem
+      
+      ⊢ ∀ll. (∃t l. ll = ListCons t l) ∨ ll = ListNil
+   
+   [nth_body_is_valid]  Theorem
+      
+      ⊢ is_valid_fp_body nth_body
+   
+   [nth_def]  Theorem
+      
+      ⊢ ∀ls i.
+          nth ls i =
+          case ls of
+            ListCons x tl =>
+              if u32_to_int i = 0 then Return x
+              else do i0 <- u32_sub i (int_to_u32 1); nth tl i0 od
+          | ListNil => Fail Failure
+   
+   
+*)
+end
-- 
cgit v1.2.3