From 584f9cbae56687c117ea02f380634839ccf88ac1 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 11 May 2023 15:42:50 +0200
Subject: Write a prototype definition using the general fixed-point combinator

---
 backends/hol4/divDefProto2Script.sml | 527 +++++++++++------------------------
 backends/hol4/divDefProto2Theory.sig | 400 ++++++++++++++++----------
 2 files changed, 417 insertions(+), 510 deletions(-)

(limited to 'backends/hol4')

diff --git a/backends/hol4/divDefProto2Script.sml b/backends/hol4/divDefProto2Script.sml
index 985b930f..074006c9 100644
--- a/backends/hol4/divDefProto2Script.sml
+++ b/backends/hol4/divDefProto2Script.sml
@@ -15,8 +15,8 @@ val _ = new_theory "divDefProto2"
  * TODO: this works! Cleanup.
  *)
 val fix_fuel_def = Define ‘
-  (fix_fuel (0 : num) (f : ('a -> 'a result) -> 'a -> 'a result) (x : 'a) : 'a result = Diverge) ∧
-  (fix_fuel (SUC n) (f : ('a -> 'a result) -> 'a -> 'a result) (x : 'a) : 'a result = f (fix_fuel n f) x)
+  (fix_fuel (0 : num) (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = Diverge) ∧
+  (fix_fuel (SUC n) (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = f (fix_fuel n f) x)
 ’
 
 val fix_fuel_P_def = Define ‘
@@ -24,7 +24,7 @@ val fix_fuel_P_def = Define ‘
 ’
 
 val fix_def = Define ‘
-  fix (f : ('a -> 'a result) -> 'a -> 'a result) (x : 'a) : 'a result =
+  fix (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result =
     if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge
 ’
 
@@ -288,391 +288,188 @@ Proof
   Cases_on ‘f (fix_fuel n'' f) x’ >> fs [] >> metis_tac []
 QED
 
-(*
-Type ft = ``: 'a -> ('a result + (num # num # 'a))``
-
-val fix_fuel_def = Define ‘
-  (fix_fuel (0 : num) (fs : ('a ft) list)
-            (i : num) (x : 'a) : 'a result = Diverge) ∧
-  
-  (fix_fuel (SUC n) fs i x =
-    case EL i fs x of
-    | INL r => r
-    | INR (j, k, y) =>
-      case fix_fuel n fs j y of
-      | Fail e => Fail e
-      | Diverge => Diverge
-      | Return z =>
-        fix_fuel n fs k z)
-’
-
-val fix_fuel_P_def = Define ‘
-  fix_fuel_P fs i x n = ~(is_diverge (fix_fuel n fs i x))
-’
-
-val fix_def = Define ‘
-  fix (fs : ('a ft) list) (i : num) (x : 'a) : 'a result =
-    if (∃ n. fix_fuel_P fs i x n)
-    then fix_fuel ($LEAST (fix_fuel_P fs i x)) fs i x
-    else Diverge
-’
-
-Theorem fix_fuel_mono:
-  ∀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
+Theorem fix_fixed_eq:
+  ∀N f. is_valid_fp_body N f ⇒ ∀x. fix f x = f (fix f) x
 Proof
-  ntac 2 strip_tac >>
-  Induct_on ‘n’ >> rpt strip_tac
-  >- (fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]) >>
-  Cases_on ‘m’ >- int_tac >> fs [] >>
-  fs [is_valid_fp_body_def] >>
-  fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
-
-  (*(* Use the validity property *)
-  last_assum (qspec_assume ‘x’) >> (* TODO: consume? *) *)
-
-  (*pop_assum ignore_tac >> (* TODO: not sure *) *)
-  Induct_on ‘N’ >- fs [eval_ftree_def] >>
-  rw [] >>
-  rw [eval_ftree_def] >>
-  Cases_on ‘h x’ >> fs [] >>
-  Cases_on ‘y’ >> fs [] >>
-  Cases_on ‘y'’ >> fs [] >>
-  
-  last_assum (qspec_assume ‘q’) >>
-  Cases_on ‘fix_fuel n f q’ >> fs [] >>
-  
-  Cases_on ‘N’ >> fs [eval_ftree_def] >>
-  
-  Cases_on ‘y’ >> fs [] >>
-  Cases_on ‘y'’ >> fs [] >>
   rw [] >>
-  (* This makes a case disjunction on the validity property *)
-  rw []
-  >-((* Case 1: the continuation doesn't matter *) fs []) >>
-  (* Case 2: the continuation *does* matter (i.e., there is a recursive call *)
-  (* Instantiate the validity property with the different continuations *)
-  first_assum (qspec_assume ‘fix_fuel n f’) >>
-  first_assum (qspec_assume ‘fix_fuel n' f’) >>
-  last_assum (qspec_assume ‘y’) >>
-  fs []
-QED
-
-
-
-Type ft = ``: ('a -> 'a result) -> 'a -> ('a result + (num # 'a))``
-
-val fix_fuel_def = Define ‘
-  (fix_fuel (0 : num) (fs : ('a ft) list) (g : 'a -> 'a result)
-            (i : num) (x : 'a) : 'a result = Diverge) ∧
-  
-  (fix_fuel (SUC n) fs g i x =
-    case EL i fs g x of
-    | INL r => r
-    | INR (j, y) =>
-      case g y of
-      | Fail e => Fail e
-      | Diverge => Diverge
-      | Return z => fix_fuel n fs g j z)
-’
-
-val fix_fuel_def = Define ‘
-  (fix_fuel (0 : num) (fs : ('a ft) list) g (i : num) (x : 'a) : 'a result = Diverge) ∧
-  
-  (fix_fuel (SUC n) fs g i x =
-    case EL i fs x of
-    | INL r => r
-    | INR (j, y) =>
-      case g y of
-      | Fail e => Fail e
-      | Diverge => Diverge
-      | Return z => fix_fuel n fs g j z)
-’
-
-val fix_fuel_def = Define ‘
-  (fix_fuel (0 : num) (f : ('a -> 'a result) -> 'a -> 'a result) (x : 'a) : 'a result = Diverge) ∧
-  (fix_fuel (SUC n) (f : ('a -> 'a result) -> 'a -> 'a result) (x : 'a) : 'a result = f (fix_fuel n f) x)
-’
-
-val fix_fuel_P_def = Define ‘
-  fix_fuel_P f x n = ~(is_diverge (fix_fuel n f x))
-’
+  Cases_on ‘∃n. fix_fuel_P f x n’
+  >- (irule fix_fixed_terminates >> metis_tac []) >>
+  irule fix_fixed_diverges >>
+  metis_tac []
+QED  
 
-val fix_def = Define ‘
-  fix (f : ('a -> 'a result) -> 'a -> 'a result) (x : 'a) : 'a result =
-    if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge
+(*
+ * Attempt to make the lemmas work with more general types
+ * (we want ‘: 'a -> 'b result’, not ‘:'a -> 'a result’).
+ *)
+val simp_types_def = Define ‘
+  simp_types (f : 'a -> 'b result) : ('a + 'b) -> ('a + 'b) result =
+    \x. case x of
+    | INL x =>
+      (case f x of
+       | Fail e => Fail e
+       | Diverge => Diverge
+       | Return y =>
+         Return (INR y))
+    | INR _ => Fail Failure
 ’
 
-(*Datatype:
-  ftree = Rec (('a -> ('a result + ('a # num))) # ftree list) | NRec ('a -> 'a result)
+(* Testing on an example *)
+Datatype:
+  list_t =
+    ListCons 't list_t
+  | ListNil
 End
 
-Type frtree = ``: ('b -> ('b result + ('a # num))) list``
-Type ftree = “: ('a, 'b) frtree # ('b result + ('a # num))”
-*)
-
-val eval_ftree_def = Define ‘
-  (eval_ftree 0 (g : 'a -> 'a result)
-    (fs : ('a -> ('a result + ('a # num))) list) x = Diverge) ∧
-
-  (eval_ftree (SUC n) g fs x =
+(* We use this version of the body to prove that the body is valid *)
+val nth_body_valid_def = Define ‘
+  nth_body_valid (f : (('t list_t # u32) + 't) -> (('t list_t # u32) + 't) result)
+    (x : (('t list_t # u32) + 't)) :
+    (('t list_t # u32) + 't) result =
     case x of
-    | INL r => r
-    | INR (y, i) =>
-      case g y of
-      | Fail e => Fail e
-      | Diverge => Diverge
-      | Return z =>
-        let f = EL i fs in
-        eval_ftree n g fs (f z))
+    | INL x => (
+      let (ls, i) = x in
+      case ls of
+      | ListCons x tl =>
+        if u32_to_int i = (0:int)
+        then Return (INR x)
+        else
+          do
+          i0 <- u32_sub i (int_to_u32 1);
+          r <- f (INL (tl, i0));
+          case r of
+          | INL _ => Fail Failure
+          | INR i1 => Return (INR i1)
+          od
+      | ListNil => Fail Failure)
+    | INR _ => Fail Failure
 ’
 
-Theorem fix_fuel_mono:
-  ∀N fs i.
-  let f = (\g x. eval_ftree N g fs (INR (x, i))) in
-  ∀n x. fix_fuel_P f x n ⇒
-  ∀ m. n ≤ m ⇒ fix_fuel n f x = fix_fuel m f x
+(* TODO: move *)
+Theorem is_valid_suffice:
+  ∃y. ∀g. g x = g y
 Proof
-  Induct_on ‘N’
-  >-(
-    fs [eval_ftree_def] >>
-
-  ntac 2 strip_tac >>
-  Induct_on ‘n’ >> rpt strip_tac
-  >- (fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]) >>
-  Cases_on ‘m’ >- int_tac >> fs [] >>
-  fs [is_valid_fp_body_def] >>
-  fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
-
-
-val is_valid_fp_body_def = Define ‘
-  is_valid_fp_body (f : ('a -> 'b result) -> 'a -> 'b result) =
-    (∃N ft. ∀x g. f g x = eval_ftree N g ft (x, i))
-’
-
-val eval_ftree_def = Define ‘
-  (eval_ftree 0 (g : 'a -> 'b result)
-    (fs : ('b -> ('b result + ('a # num))) list, x : 'b result + ('a # num)) = Diverge) ∧
-  
-  (eval_ftree (SUC n) g (fs, x) =
-    case x of
-    | INL r => r
-    | INR (y, i) =>
-      case g y of
-      | Fail e => Fail e
-      | Diverge => Diverge
-      | Return z =>
-        let f = EL i fs in
-        eval_ftree n g (fs, f z))
-’
-
-val is_valid_fp_body_def = Define ‘
-  is_valid_fp_body (f : ('a -> 'b result) -> 'a -> 'b result) =
-    (∃N ft h. ∀x g. f g x = eval_ftree N g (ft, h x))
-’
-
-Theorem fix_fuel_mono:
-  let f = (\x. eval_ftree N g (ft, h x)) in
-  ∀n x. fix_fuel_P f x n ⇒
-   ∀ m. n ≤ m ⇒ fix_fuel n f x = fix_fuel m f x
-Proof
-
-
-Theorem fix_fuel_mono:
-  ∀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
-Proof
-  ntac 2 strip_tac >>
-  Induct_on ‘n’ >> rpt strip_tac
-  >- (fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]) >>
-  Cases_on ‘m’ >- int_tac >> fs [] >>
-  fs [is_valid_fp_body_def] >>
-  fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
-
-  (*(* Use the validity property *)
-  last_assum (qspec_assume ‘x’) >> (* TODO: consume? *) *)
-
-  (*pop_assum ignore_tac >> (* TODO: not sure *) *)
-  Induct_on ‘N’ >- fs [eval_ftree_def] >>
-  rw [] >>
-  rw [eval_ftree_def] >>
-  Cases_on ‘h x’ >> fs [] >>
-  Cases_on ‘y’ >> fs [] >>
-  Cases_on ‘y'’ >> fs [] >>
-  
-  last_assum (qspec_assume ‘q’) >>
-  Cases_on ‘fix_fuel n f q’ >> fs [] >>
-  
-  Cases_on ‘N’ >> fs [eval_ftree_def] >>
-  
-  Cases_on ‘y’ >> fs [] >>
-  Cases_on ‘y'’ >> fs [] >>
-  rw [] >>
-  (* This makes a case disjunction on the validity property *)
-  rw []
-  >-((* Case 1: the continuation doesn't matter *) fs []) >>
-  (* Case 2: the continuation *does* matter (i.e., there is a recursive call *)
-  (* Instantiate the validity property with the different continuations *)
-  first_assum (qspec_assume ‘fix_fuel n f’) >>
-  first_assum (qspec_assume ‘fix_fuel n' f’) >>
-  last_assum (qspec_assume ‘y’) >>
-  fs []
+  metis_tac []
 QED
 
-
-val length_ftree = “
-(
-  [
-    (\n. INL (return (1 + n)))
-  ],
-  (case ls of
-   | ListCons x tl =>
-     INR (tl, 0)
-   | ListNil => INL (return 0))
-) : ('a list_t, int) ftree
-”
-
-val eval_length_ftree = mk_icomb (“eval_ftree 1 g”, length_ftree)
-
-Theorem length_body_eq:
-  eval_ftree (SUC (SUC 0)) g
-  (
-    [
-      (\n. INL (Return (1 + n)))
-    ],
-    (case ls of
-     | ListCons x tl =>
-       INR (tl, 0)
-     | ListNil => INL (Return 0))
-  ) =
-  case ls of
-  | ListCons x tl =>
-    do
-      n <- g tl;
-      Return (1 + n)
-    od
-  | ListNil => Return 0
+Theorem nth_body_valid_is_valid:
+  is_valid_fp_body (SUC (SUC 0)) nth_body_valid
 Proof
-  fs [eval_ftree_def, bind_def] >>
-  Cases_on ‘ls’ >> fs []
+  pure_once_rewrite_tac [is_valid_fp_body_def] >>
+  gen_tac >>
+  (* TODO: automate this *)
+  Cases_on ‘x’ >> fs [] >>
+  (* Expand *)
+  fs [nth_body_valid_def, bind_def] >>
+  (* Explore all paths *)
+  Cases_on ‘x'’ >> fs [] >>
+  Cases_on ‘q’ >> fs [] >>
+  Cases_on ‘u32_to_int r = 0’ >> fs [] >>
+  Cases_on ‘u32_sub r (int_to_u32 1)’ >> fs [] >>
+  disj2_tac >>
+  (* This is hard *)
+  qexists ‘\g x. case x of | INL _ => Fail Failure | INR i1 => Return (INR i1)’ >>
+  qexists ‘INL (l, a)’ >>
+  conj_tac
+  >-(
+    (* Prove that the body of h is valid *)
+    sg ‘1 = SUC 0’ >- fs [] >>
+    pop_assum (fn th => pure_rewrite_tac [th]) >>
+    pure_once_rewrite_tac [is_valid_fp_body_def] >>
+    (* *)
+    fs []) >>
+  gen_tac >>
+  (* Explore all paths *)
+  Cases_on ‘g (INL (l,a))’ >> fs [] >>
+  Cases_on ‘a'’ >> fs []
 QED
 
-val eval_ftree_def = Define ‘
-  eval_ftree 0 (fs : ('a, 'b) ftree) (g : 'a -> 'b result) (x : 'b result + ('a # num)) = Diverge ∧
-  
-  eval_ftree (SUC n) fs g x =
+(* We prove that ‘nth_body_valid’ is equivalent to ‘nth_body’ *)
+val nth_body1_def = Define ‘
+  nth_body1 (f : (('t list_t # u32) + 't) -> (('t list_t # u32) + 't) result)
+    (x : (('t list_t # u32) + 't)) :
+    (('t list_t # u32) + 't) result =
     case x of
-    | INL r => r
-    | INR (y, i) =>
-      case g y of
-      | Fail e => Fail e
-      | Diverge => Diverge
-      | Return z =>
-        let f = EL i fs in
-        eval_ftree n fs g (f z)
+    | INL x => (
+      let (ls, i) = x in
+      case ls of
+      | ListCons x tl =>
+        if u32_to_int i = (0:int)
+        then Return (INR x)
+        else
+          do
+          i0 <- u32_sub i (int_to_u32 1);
+          r <- case f (INL (tl, i0)) of
+               | Fail e => Fail e
+               | Diverge => Diverge
+               | Return r =>
+                 case r of
+                 | INL _ => Fail Failure
+                 | INR i1 => Return i1;
+          Return (INR r)
+          od
+      | ListNil => Fail Failure)
+    | INR _ => Fail Failure
 ’
 
-val length_body_funs_def = Define 
-
-“
-[
-  (\ls. case ls of
-   | ListCons x tl =>
-     INR (tl, 1)
-   | ListNil => INL (return 0)),
-  (\n. INL (return (1 + n)))
-]
-”
-
-
-
-“:('a, 'b) FT”
-
-Define 
-
-val nth_body = Define ‘
-  
+Theorem nth_body_valid_eq:
+  nth_body_valid = nth_body1
+Proof
+  ntac 2 (irule EQ_EXT >> gen_tac) >>
+  pure_rewrite_tac [nth_body_valid_def, nth_body1_def, bind_def, LET_DEF] >>
+  (* TODO: automate *)
+  Cases_on ‘x'’ >> fs [] >>
+  Cases_on ‘x''’ >> fs [] >>
+  Cases_on ‘q’ >> fs [] >>
+  Cases_on ‘u32_to_int r = 0’ >> fs [] >>
+  Cases_on ‘u32_sub r (int_to_u32 1)’ >> fs [] >>
+  Cases_on ‘x (INL (l,a))’ >> fs [] >>
+  Cases_on ‘a'’ >> fs []
+QED
 
+val nth_raw_def = Define ‘
+  nth (ls : 't list_t) (i : u32) =
+    case fix nth_body1 (INL (ls, i)) of
+    | Fail e => Fail e
+    | Diverge => Diverge
+    | Return r =>
+      case r of
+      | INL _ => Fail Failure
+      | INR x => Return x
 ’
 
-“INL”
-“INR”
-
-“
-  Rec (
+Theorem nth_def:
+  ∀ls i. nth (ls : 't list_t) (i : u32) : 't result =
     case ls of
     | ListCons x tl =>
-      do
-        INR (tl, 0)
-      od
-    | ListNil => INL (return 0),
-    [NRec (\n. return (1 + n))])
-”
-
-“
-  case ls of
-  | ListCons x tl =>
-    if u32_to_int i = (0:int)
-    then (Return x)
-    else
-      do
-      i0 <- u32_sub i (int_to_u32 1);
-      y <- nth tl i0;
-      return y
-      od
-  | ListNil => Fail Failure
-”
-
-
-“:'a + 'b”
-“:'a # 'b”
-
-(*** Encoding of a function *)
-Datatype:
-  ('a, 'b) test = Return ('a -> 'b)
-End
-
-val tyax =
-      new_type_definition ("three",
-        Q.prove(`?p. (\(x,y). ~(x /\ y)) p`, cheat))
-
-val three_bij = define_new_type_bijections
-                      {name="three_tybij", ABS="abs3", REP="rep3", tyax=tyax}
-type_of “rep3”
-type_of “abs3”
-
-m “”
-
-                Q.EXISTS_TAC `(F,F)` THEN GEN_BETA_TAC THEN REWRITE_TAC []));
-
-“Return (\x. x)”
-
-Datatype:
-  ftree = Rec ('a -> ('a result + ('a # ftree))) | NRec ('a -> 'a result)
-End
-
-Datatype:
-  'a ftree = Rec ('a -> ('a result + ('a # ftree))) | NRec ('a -> 'a result)
-End
-
-Datatype:
-  ftree = Rec ('a -> ('a result + ('a # ftree))) | NRec ('a -> 'a result)
-End
-
-Datatype:
-  result = Return 'a | Fail error | Diverge
-End
-
-Type M = ``: 'a result``
-
-
-val fix_def = Define ‘
-  fix (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result =
-    if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge
-’
+      if u32_to_int i = (0:int)
+      then (Return x)
+      else
+        do
+        i0 <- u32_sub i (int_to_u32 1);
+        nth tl i0
+        od
+    | ListNil => Fail Failure
+Proof
+  rpt strip_tac >>
+  (* Expand the raw definition *)
+  pure_rewrite_tac [nth_raw_def] >>
+  (* Use the fixed-point equality *)
+  sg ‘fix nth_body1 (INL (ls,i)) = nth_body1 (fix nth_body1) (INL (ls,i))’
+  >- (
+    pure_rewrite_tac [GSYM nth_body_valid_eq] >>
+    simp_tac bool_ss [HO_MATCH_MP fix_fixed_eq nth_body_valid_is_valid]) >>
+  pop_assum (fn th => pure_asm_rewrite_tac [th]) >>
+  (* Expand the body definition *)
+  qspecl_assume [‘fix nth_body1’, ‘(INL (ls, i))’] nth_body1_def >>
+  pop_assum (fn th => pure_rewrite_tac [th, LET_THM]) >>
+  (* Do we really have to explore all the paths again? If yes, nth_body1 is useless *)
+  fs [bind_def] >>
+  Cases_on ‘ls’ >> fs [] >>
+  Cases_on ‘u32_to_int i = 0’ >> fs [] >>
+  Cases_on ‘u32_sub i (int_to_u32 1)’ >> fs [] >>
+  Cases_on ‘fix nth_body1 (INL (l,a))’ >> fs [] >>
+  Cases_on ‘a'’ >> fs []
+QED
 
 val _ = export_theory ()
diff --git a/backends/hol4/divDefProto2Theory.sig b/backends/hol4/divDefProto2Theory.sig
index 349aabf7..7ce4b194 100644
--- a/backends/hol4/divDefProto2Theory.sig
+++ b/backends/hol4/divDefProto2Theory.sig
@@ -6,25 +6,41 @@ sig
     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
+    val list_t_TY_DEF : thm
+    val list_t_case_def : thm
+    val list_t_size_def : thm
+    val nth_body1_def : thm
+    val nth_body_valid_def : thm
+    val simp_types_def : thm
   
   (*  Theorems  *)
-    val datatype_ftree : thm
-    val eval_ftree_compute : thm
-    val eval_ftree_def : thm
-    val eval_ftree_ind : thm
+    val datatype_list_t : thm
+    val fix_fixed_diverges : thm
+    val fix_fixed_eq : thm
+    val fix_fixed_terminates : thm
+    val fix_fuel_P_least : 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 fix_fuel_eq_fix : thm
+    val fix_fuel_mono : thm
+    val fix_fuel_mono_aux : thm
+    val fix_fuel_mono_least : thm
+    val fix_fuel_not_diverge_eq_fix : thm
+    val fix_fuel_not_diverge_eq_fix_aux : thm
+    val fix_not_diverge_implies_fix_fuel : thm
+    val fix_not_diverge_implies_fix_fuel_aux : thm
+    val is_valid_fp_body_compute : 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_valid_eq : thm
+    val nth_body_valid_is_valid : thm
+    val nth_def : thm
   
   val divDefProto2_grammars : type_grammar.grammar * term_grammar.grammar
 (*
@@ -47,124 +63,130 @@ sig
       ⊢ (∀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
+   [is_valid_fp_body_def]  Definition
+      
+      ⊢ (∀f. is_valid_fp_body 0 f ⇔ F) ∧
+        ∀n f.
+          is_valid_fp_body (SUC n) f ⇔
+          ∀x. (∀g h. f g x = f h x) ∨
+              ∃h y.
+                is_valid_fp_body n h ∧ ∀g. f g x = do z <- g y; h g z od
+   
+   [list_t_TY_DEF]  Definition
       
       ⊢ ∃rep.
           TYPE_DEFINITION
             (λa0'.
-                 ∀ $var$('ftree') $var$('@temp @ind_typedivDefProto20prod')
-                     $var$('@temp @ind_typedivDefProto21list').
+                 ∀ $var$('list_t').
                    (∀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' =
                          (λa0 a1.
-                              ind_type$CONSTR (SUC (SUC 0)) (ARB,a0)
+                              ind_type$CONSTR 0 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
+                           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
    
-   [ftree_case_def]  Definition
+   [list_t_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
+      ⊢ (∀a0 a1 f v. list_t_CASE (ListCons a0 a1) f v = f a0 a1) ∧
+        ∀f v. list_t_CASE ListNil f v = v
    
-   [ftree_size_def]  Definition
+   [list_t_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)
+      ⊢ (∀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
    
-   [is_valid_fp_body_def]  Definition
+   [nth_body1_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) =
+      ⊢ ∀f x.
+          nth_body1 f 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) =
+            INL x =>
+              (let
+                 (ls,i) = x
+               in
+                 case ls of
+                   ListCons x tl =>
+                     if u32_to_int i = 0 then Return (INR x)
+                     else
+                       do
+                         i0 <- u32_sub i (int_to_u32 1);
+                         r <-
+                           case f (INL (tl,i0)) of
+                             Return (INL v) => Fail Failure
+                           | Return (INR i1) => Return i1
+                           | Fail e => Fail e
+                           | Diverge => Diverge;
+                         Return (INR r)
+                       od
+                 | ListNil => Fail Failure)
+          | INR v3 => Fail Failure
+   
+   [nth_body_valid_def]  Definition
+      
+      ⊢ ∀f x.
+          nth_body_valid f 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)
+            INL x =>
+              (let
+                 (ls,i) = x
+               in
+                 case ls of
+                   ListCons x tl =>
+                     if u32_to_int i = 0 then Return (INR x)
+                     else
+                       do
+                         i0 <- u32_sub i (int_to_u32 1);
+                         r <- f (INL (tl,i0));
+                         case r of
+                           INL v => Fail Failure
+                         | INR i1 => Return (INR i1)
+                       od
+                 | ListNil => Fail Failure)
+          | INR v2 => Fail Failure
+   
+   [simp_types_def]  Definition
+      
+      ⊢ ∀f. simp_types f =
+            (λx'.
+                 case x' of
+                   INL x =>
+                     (case f x of
+                        Return y => Return (INR y)
+                      | Fail e => Fail e
+                      | Diverge => Diverge)
+                 | INR v1 => Fail Failure)
+   
+   [datatype_list_t]  Theorem
+      
+      ⊢ DATATYPE (list_t ListCons ListNil)
+   
+   [fix_fixed_diverges]  Theorem
+      
+      ⊢ ∀N f.
+          is_valid_fp_body N f ⇒
+          ∀x. ¬(∃n. fix_fuel_P f x n) ⇒ fix f x = f (fix f) x
+   
+   [fix_fixed_eq]  Theorem
+      
+      ⊢ ∀N f. is_valid_fp_body N f ⇒ ∀x. fix f x = f (fix f) x
+   
+   [fix_fixed_terminates]  Theorem
+      
+      ⊢ ∀N f.
+          is_valid_fp_body N f ⇒
+          ∀x n. fix_fuel_P f x n ⇒ fix f x = f (fix f) x
+   
+   [fix_fuel_P_least]  Theorem
+      
+      ⊢ ∀f n x.
+          fix_fuel n f x ≠ Diverge ⇒
+          fix_fuel_P f x ($LEAST (fix_fuel_P f x))
    
    [fix_fuel_compute]  Theorem
       
@@ -176,49 +198,137 @@ sig
           fix_fuel (NUMERAL (BIT2 n)) f x =
           f (fix_fuel (NUMERAL (BIT1 n)) f) x
    
-   [ftree_11]  Theorem
+   [fix_fuel_eq_fix]  Theorem
+      
+      ⊢ ∀N f.
+          is_valid_fp_body N f ⇒
+          ∀n x. fix_fuel_P f x n ⇒ fix_fuel n f x = fix f x
+   
+   [fix_fuel_mono]  Theorem
+      
+      ⊢ ∀N f.
+          is_valid_fp_body N 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_aux]  Theorem
+      
+      ⊢ ∀n N M g f.
+          is_valid_fp_body M f ⇒
+          is_valid_fp_body N g ⇒
+          ∀x. ¬is_diverge (g (fix_fuel n f) x) ⇒
+              ∀m. n ≤ m ⇒ g (fix_fuel n f) x = g (fix_fuel m f) x
+   
+   [fix_fuel_mono_least]  Theorem
+      
+      ⊢ ∀N f.
+          is_valid_fp_body N f ⇒
+          ∀n x.
+            fix_fuel_P f x n ⇒
+            fix_fuel n f x = fix_fuel ($LEAST (fix_fuel_P f x)) f x
+   
+   [fix_fuel_not_diverge_eq_fix]  Theorem
+      
+      ⊢ ∀N f.
+          is_valid_fp_body N f ⇒
+          ∀n x.
+            f (fix_fuel n f) x ≠ Diverge ⇒ f (fix f) x = f (fix_fuel n f) x
+   
+   [fix_fuel_not_diverge_eq_fix_aux]  Theorem
+      
+      ⊢ ∀N M g f.
+          is_valid_fp_body M f ⇒
+          is_valid_fp_body N g ⇒
+          ∀n x.
+            g (fix_fuel n f) x ≠ Diverge ⇒ g (fix f) x = g (fix_fuel n f) x
+   
+   [fix_not_diverge_implies_fix_fuel]  Theorem
+      
+      ⊢ ∀N f.
+          is_valid_fp_body N f ⇒
+          ∀x. f (fix f) x ≠ Diverge ⇒ ∃n. f (fix f) x = f (fix_fuel n f) x
+   
+   [fix_not_diverge_implies_fix_fuel_aux]  Theorem
+      
+      ⊢ ∀N M g f.
+          is_valid_fp_body M f ⇒
+          is_valid_fp_body N g ⇒
+          ∀x. g (fix f) x ≠ Diverge ⇒
+              ∃n. g (fix f) x = g (fix_fuel n f) x ∧
+                  ∀m. n ≤ m ⇒ g (fix_fuel m f) x = g (fix_fuel n f) x
+   
+   [is_valid_fp_body_compute]  Theorem
+      
+      ⊢ (∀f. is_valid_fp_body 0 f ⇔ F) ∧
+        (∀n f.
+           is_valid_fp_body (NUMERAL (BIT1 n)) f ⇔
+           ∀x. (∀g h. f g x = f h x) ∨
+               ∃h y.
+                 is_valid_fp_body (NUMERAL (BIT1 n) − 1) h ∧
+                 ∀g. f g x = do z <- g y; h g z od) ∧
+        ∀n f.
+          is_valid_fp_body (NUMERAL (BIT2 n)) f ⇔
+          ∀x. (∀g h. f g x = f h x) ∨
+              ∃h y.
+                is_valid_fp_body (NUMERAL (BIT1 n)) h ∧
+                ∀g. f g x = do z <- g y; h g z od
+   
+   [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
       
-      ⊢ (∀a a'. Rec a = Rec a' ⇔ a = a') ∧ ∀a a'. NRec a = NRec a' ⇔ a = a'
+      ⊢ ∀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'
    
-   [ftree_Axiom]  Theorem
+   [list_t_case_eq]  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)
+      ⊢ list_t_CASE x f v = v' ⇔
+        (∃t l. x = ListCons t l ∧ f t l = v') ∨ x = ListNil ∧ v = v'
    
-   [ftree_case_cong]  Theorem
+   [list_t_distinct]  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'
+      ⊢ ∀a1 a0. ListCons a0 a1 ≠ ListNil
    
-   [ftree_case_eq]  Theorem
+   [list_t_induction]  Theorem
       
-      ⊢ ftree_CASE x f f1 = v ⇔
-        (∃p. x = Rec p ∧ f p = v) ∨ ∃f'. x = NRec f' ∧ f1 f' = v
+      ⊢ ∀P. (∀l. P l ⇒ ∀t. P (ListCons t l)) ∧ P ListNil ⇒ ∀l. P l
    
-   [ftree_distinct]  Theorem
+   [list_t_nchotomy]  Theorem
       
-      ⊢ ∀a' a. Rec a ≠ NRec a'
+      ⊢ ∀ll. (∃t l. ll = ListCons t l) ∨ ll = ListNil
    
-   [ftree_induction]  Theorem
+   [nth_body_valid_eq]  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
+      ⊢ nth_body_valid = nth_body1
    
-   [ftree_nchotomy]  Theorem
+   [nth_body_valid_is_valid]  Theorem
       
-      ⊢ ∀ff. (∃p. ff = Rec p) ∨ ∃f. ff = NRec f
+      ⊢ is_valid_fp_body (SUC (SUC 0)) nth_body_valid
    
-   [ftree_size_eq]  Theorem
+   [nth_def]  Theorem
       
-      ⊢ ftree1_size f = pair_size (λv. 0) (list_size (ftree_size f)) ∧
-        ftree2_size f = list_size (ftree_size f)
+      ⊢ ∀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
    
    
 *)
-- 
cgit v1.2.3