Fix minor issues

3 files changed, 508 insertions, 12 deletions

diff --git a/backends/hol4/divDefLib.sml b/backends/hol4/divDefLib.sml
index 347e2d8e..80f47f65 100644
--- a/backends/hol4/divDefLib.sml
+++ b/backends/hol4/divDefLib.sml
@@ -664,7 +664,9 @@ fun prove_body_is_valid_tac_step (asms, g) =
             - we have to prove that ‘h’ is valid
             - we have to finish the proof of validity for the current body
           *)
-         conj_tac >> fs [case_result_switch_eq])
+         conj_tac >> fs [case_result_switch_eq, bind_def] >>
+         (* The first subgoal should have been eliminated *)
+         gen_tac)
       end
   in
     (* If recursive call: special treatment. Otherwise, we do a simple disjunction *)
@@ -687,24 +689,24 @@ fun prove_body_is_valid_tac (body_def : thm option) : tactic =
 (* Prove that a body satisfies the validity condition of the fixed point *)
 fun prove_body_is_valid (body : term) : thm =
   let
-    (* Explore the body and count the number of occurrences of nested recursive
-       calls so that we can properly instantiate the ‘N’ argument of ‘is_valid_fp_body’.
+    (* Explore the body and count the number of occurrences of recursive
+       calls so that we can properly instantiate the ‘N’ argument of ‘is_valid_fp_body’
+       (note: we compute an overapproximation).
 
        We first retrieve the name of the continuation parameter.
+
        Rem.: we generated fresh names so that, for instance, the continuation name
        doesn't collide with other names. Because of this, we don't need to look for
        collisions when exploring the body (and in the worst case, we would cound
-       an overapproximation of the number of recursive calls, which is perfectly
-       valid).
+       an overapproximation of the number of recursive calls).
      *)
     val fcont = (hd o fst o strip_abs) body
     val fcont_name = (fst o dest_var) fcont
-    fun max x y = if x > y then x else y
     fun count_body_rec_calls (body : term) : int =
       case dest_term body of
         VAR (name, _) => if name = fcont_name then 1 else 0
       | CONST _ => 0
-      | COMB (x, y) => max (count_body_rec_calls x) (count_body_rec_calls y)
+      | COMB (x, y) => count_body_rec_calls x + count_body_rec_calls y
       | LAMB (_, x) => count_body_rec_calls x
     val num_rec_calls = count_body_rec_calls body
 
@@ -722,7 +724,6 @@ fun prove_body_is_valid (body : term) : thm =
     (* Generate the lemma statement *)
     val is_valid_tm = list_mk_icomb (is_valid_fp_body_tm, [n_tm, body])
     val is_valid_thm = prove (is_valid_tm, prove_body_is_valid_tac NONE)
-
     (* Replace ‘nvar’ with ‘0’ *)
     val is_valid_thm = INST [nvar |-> zero_num_tm] is_valid_thm
   in
@@ -894,6 +895,10 @@ fun DefineDiv (def_qt : term quotation) =
 
     (* Prove the final equations *)
     val def_eqs = prove_def_eqs body_is_valid def_tms raw_defs
+
+    (* Save the definitions *)
+    val thm_names = map (fn x => x ^ "_def") fnames
+    val _ = map save_thm (zip thm_names def_eqs)
   in
     def_eqs
   end
diff --git a/backends/hol4/divDefLibTestScript.sml b/backends/hol4/divDefLibTestScript.sml
index b1243065..80170b24 100644
--- a/backends/hol4/divDefLibTestScript.sml
+++ b/backends/hol4/divDefLibTestScript.sml
@@ -7,10 +7,9 @@ open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
 open primitivesLib
 open divDefTheory divDefLib
 
-val [even_def, odd_def] = DefineDiv ‘
-  (even (i : int) : bool result = if i = 0 then Return T else odd (i - 1)) /\
-  (odd (i : int) : bool result = if i = 0 then Return F else even (i - 1))
-’
+val _ = new_theory "divDefLibTest"
+
+(* nth *)
 
 Datatype:
   list_t =
@@ -31,3 +30,61 @@ val [nth_def] = DefineDiv ‘
         od
     | ListNil => Fail Failure
 ’
+
+(* even, odd *)
+
+val [even_def, odd_def] = DefineDiv ‘
+  (even (i : int) : bool result = if i = 0 then Return T else odd (i - 1)) /\
+  (odd (i : int) : bool result = if i = 0 then Return F else even (i - 1))
+’
+
+(* btree *)
+
+Datatype:
+  btree =
+    BLeaf 'a
+  | BNode btree btree
+End
+
+val [btree_height_def] = DefineDiv ‘
+  btree_height (tree : 'a btree) : int result =
+    case tree of
+    | BLeaf _ => Return 1
+    | BNode l r =>
+      do
+      hl <- btree_height l;
+      hr <- btree_height r;
+      Return (hl + hr)
+      od
+’
+
+(* tree 2 *)
+
+Datatype:
+  tree =
+    TLeaf 'a
+  | TNode node ;
+  
+  node = 
+    Node (tree list)
+End
+
+val [tree_height_def, tree_nodes_height_def] = DefineDiv ‘
+  (tree_height (tree : 'a tree) : int result =
+    case tree of
+      TLeaf _ => Return 1
+    | TNode n =>
+      case n of Node ls => tree_nodes_height ls) ∧
+
+  (tree_nodes_height (ls : ('a tree) list) : int result =
+    case ls of
+      [] => Return 0
+    | t :: tl =>
+      do
+        h1 <- tree_height t;
+        h2 <- tree_nodes_height tl;
+        Return (h1 + h2)
+      od)
+’
+
+val _ = export_theory ()
diff --git a/backends/hol4/divDefLibTestTheory.sig b/backends/hol4/divDefLibTestTheory.sig
new file mode 100644
index 00000000..8da736ab
--- /dev/null
+++ b/backends/hol4/divDefLibTestTheory.sig
@@ -0,0 +1,434 @@
+signature divDefLibTestTheory =
+sig
+  type thm = Thm.thm
+  
+  (*  Definitions  *)
+    val btree_TY_DEF : thm
+    val btree_case_def : thm
+    val btree_size_def : thm
+    val list_t_TY_DEF : thm
+    val list_t_case_def : thm
+    val list_t_size_def : thm
+    val node_TY_DEF : thm
+    val node_case_def : thm
+    val tree_TY_DEF : thm
+    val tree_case_def : thm
+    val tree_size_def : thm
+  
+  (*  Theorems  *)
+    val btree_11 : thm
+    val btree_Axiom : thm
+    val btree_case_cong : thm
+    val btree_case_eq : thm
+    val btree_distinct : thm
+    val btree_height_def : thm
+    val btree_induction : thm
+    val btree_nchotomy : thm
+    val datatype_btree : thm
+    val datatype_list_t : thm
+    val datatype_tree : thm
+    val even_def : 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 node_11 : thm
+    val node_Axiom : thm
+    val node_case_cong : thm
+    val node_case_eq : thm
+    val node_induction : thm
+    val node_nchotomy : thm
+    val nth_def : thm
+    val odd_def : thm
+    val tree_11 : thm
+    val tree_Axiom : thm
+    val tree_case_cong : thm
+    val tree_case_eq : thm
+    val tree_distinct : thm
+    val tree_height_def : thm
+    val tree_induction : thm
+    val tree_nchotomy : thm
+    val tree_nodes_height_def : thm
+    val tree_size_eq : thm
+  
+  val divDefLibTest_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+   [divDef] Parent theory of "divDefLibTest"
+   
+   [btree_TY_DEF]  Definition
+      
+      ⊢ ∃rep.
+          TYPE_DEFINITION
+            (λa0'.
+                 ∀ $var$('btree').
+                   (∀a0'.
+                      (∃a. a0' =
+                           (λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM))
+                             a) ∨
+                      (∃a0 a1.
+                         a0' =
+                         (λa0 a1.
+                              ind_type$CONSTR (SUC 0) ARB
+                                (ind_type$FCONS a0
+                                   (ind_type$FCONS a1 (λn. ind_type$BOTTOM))))
+                           a0 a1 ∧ $var$('btree') a0 ∧ $var$('btree') a1) ⇒
+                      $var$('btree') a0') ⇒
+                   $var$('btree') a0') rep
+   
+   [btree_case_def]  Definition
+      
+      ⊢ (∀a f f1. btree_CASE (BLeaf a) f f1 = f a) ∧
+        ∀a0 a1 f f1. btree_CASE (BNode a0 a1) f f1 = f1 a0 a1
+   
+   [btree_size_def]  Definition
+      
+      ⊢ (∀f a. btree_size f (BLeaf a) = 1 + f a) ∧
+        ∀f a0 a1.
+          btree_size f (BNode a0 a1) =
+          1 + (btree_size f a0 + btree_size f a1)
+   
+   [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
+   
+   [node_TY_DEF]  Definition
+      
+      ⊢ ∃rep.
+          TYPE_DEFINITION
+            (λa1'.
+                 ∀ $var$('tree') $var$('node')
+                     $var$('@temp @ind_typedivDefLibTest8list').
+                   (∀a0'.
+                      (∃a. a0' =
+                           (λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM))
+                             a) ∨
+                      (∃a. a0' =
+                           (λa.
+                                ind_type$CONSTR (SUC 0) ARB
+                                  (ind_type$FCONS a (λn. ind_type$BOTTOM)))
+                             a ∧ $var$('node') a) ⇒
+                      $var$('tree') a0') ∧
+                   (∀a1'.
+                      (∃a. a1' =
+                           (λa.
+                                ind_type$CONSTR (SUC (SUC 0)) ARB
+                                  (ind_type$FCONS a (λn. ind_type$BOTTOM)))
+                             a ∧
+                           $var$('@temp @ind_typedivDefLibTest8list') a) ⇒
+                      $var$('node') a1') ∧
+                   (∀a2.
+                      a2 =
+                      ind_type$CONSTR (SUC (SUC (SUC 0))) ARB
+                        (λn. ind_type$BOTTOM) ∨
+                      (∃a0 a1.
+                         a2 =
+                         (λa0 a1.
+                              ind_type$CONSTR (SUC (SUC (SUC (SUC 0)))) ARB
+                                (ind_type$FCONS a0
+                                   (ind_type$FCONS a1 (λn. ind_type$BOTTOM))))
+                           a0 a1 ∧ $var$('tree') a0 ∧
+                         $var$('@temp @ind_typedivDefLibTest8list') a1) ⇒
+                      $var$('@temp @ind_typedivDefLibTest8list') a2) ⇒
+                   $var$('node') a1') rep
+   
+   [node_case_def]  Definition
+      
+      ⊢ ∀a f. node_CASE (Node a) f = f a
+   
+   [tree_TY_DEF]  Definition
+      
+      ⊢ ∃rep.
+          TYPE_DEFINITION
+            (λa0'.
+                 ∀ $var$('tree') $var$('node')
+                     $var$('@temp @ind_typedivDefLibTest8list').
+                   (∀a0'.
+                      (∃a. a0' =
+                           (λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM))
+                             a) ∨
+                      (∃a. a0' =
+                           (λa.
+                                ind_type$CONSTR (SUC 0) ARB
+                                  (ind_type$FCONS a (λn. ind_type$BOTTOM)))
+                             a ∧ $var$('node') a) ⇒
+                      $var$('tree') a0') ∧
+                   (∀a1'.
+                      (∃a. a1' =
+                           (λa.
+                                ind_type$CONSTR (SUC (SUC 0)) ARB
+                                  (ind_type$FCONS a (λn. ind_type$BOTTOM)))
+                             a ∧
+                           $var$('@temp @ind_typedivDefLibTest8list') a) ⇒
+                      $var$('node') a1') ∧
+                   (∀a2.
+                      a2 =
+                      ind_type$CONSTR (SUC (SUC (SUC 0))) ARB
+                        (λn. ind_type$BOTTOM) ∨
+                      (∃a0 a1.
+                         a2 =
+                         (λa0 a1.
+                              ind_type$CONSTR (SUC (SUC (SUC (SUC 0)))) ARB
+                                (ind_type$FCONS a0
+                                   (ind_type$FCONS a1 (λn. ind_type$BOTTOM))))
+                           a0 a1 ∧ $var$('tree') a0 ∧
+                         $var$('@temp @ind_typedivDefLibTest8list') a1) ⇒
+                      $var$('@temp @ind_typedivDefLibTest8list') a2) ⇒
+                   $var$('tree') a0') rep
+   
+   [tree_case_def]  Definition
+      
+      ⊢ (∀a f f1. tree_CASE (TLeaf a) f f1 = f a) ∧
+        ∀a f f1. tree_CASE (TNode a) f f1 = f1 a
+   
+   [tree_size_def]  Definition
+      
+      ⊢ (∀f a. tree_size f (TLeaf a) = 1 + f a) ∧
+        (∀f a. tree_size f (TNode a) = 1 + node_size f a) ∧
+        (∀f a. node_size f (Node a) = 1 + tree1_size f a) ∧
+        (∀f. tree1_size f [] = 0) ∧
+        ∀f a0 a1.
+          tree1_size f (a0::a1) = 1 + (tree_size f a0 + tree1_size f a1)
+   
+   [btree_11]  Theorem
+      
+      ⊢ (∀a a'. BLeaf a = BLeaf a' ⇔ a = a') ∧
+        ∀a0 a1 a0' a1'. BNode a0 a1 = BNode a0' a1' ⇔ a0 = a0' ∧ a1 = a1'
+   
+   [btree_Axiom]  Theorem
+      
+      ⊢ ∀f0 f1. ∃fn.
+          (∀a. fn (BLeaf a) = f0 a) ∧
+          ∀a0 a1. fn (BNode a0 a1) = f1 a0 a1 (fn a0) (fn a1)
+   
+   [btree_case_cong]  Theorem
+      
+      ⊢ ∀M M' f f1.
+          M = M' ∧ (∀a. M' = BLeaf a ⇒ f a = f' a) ∧
+          (∀a0 a1. M' = BNode a0 a1 ⇒ f1 a0 a1 = f1' a0 a1) ⇒
+          btree_CASE M f f1 = btree_CASE M' f' f1'
+   
+   [btree_case_eq]  Theorem
+      
+      ⊢ btree_CASE x f f1 = v ⇔
+        (∃a. x = BLeaf a ∧ f a = v) ∨ ∃b b0. x = BNode b b0 ∧ f1 b b0 = v
+   
+   [btree_distinct]  Theorem
+      
+      ⊢ ∀a1 a0 a. BLeaf a ≠ BNode a0 a1
+   
+   [btree_height_def]  Theorem
+      
+      ⊢ ∀tree.
+          btree_height tree =
+          case tree of
+            BLeaf v => Return 1
+          | BNode l r =>
+            do
+              hl <- btree_height l;
+              hr <- btree_height r;
+              Return (hl + hr)
+            od
+   
+   [btree_induction]  Theorem
+      
+      ⊢ ∀P. (∀a. P (BLeaf a)) ∧ (∀b b0. P b ∧ P b0 ⇒ P (BNode b b0)) ⇒
+            ∀b. P b
+   
+   [btree_nchotomy]  Theorem
+      
+      ⊢ ∀bb. (∃a. bb = BLeaf a) ∨ ∃b b0. bb = BNode b b0
+   
+   [datatype_btree]  Theorem
+      
+      ⊢ DATATYPE (btree BLeaf BNode)
+   
+   [datatype_list_t]  Theorem
+      
+      ⊢ DATATYPE (list_t ListCons ListNil)
+   
+   [datatype_tree]  Theorem
+      
+      ⊢ DATATYPE (tree TLeaf TNode ∧ node Node)
+   
+   [even_def]  Theorem
+      
+      ⊢ ∀i. even i = if i = 0 then Return T else odd (i − 1)
+   
+   [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
+   
+   [node_11]  Theorem
+      
+      ⊢ ∀a a'. Node a = Node a' ⇔ a = a'
+   
+   [node_Axiom]  Theorem
+      
+      ⊢ ∀f0 f1 f2 f3 f4. ∃fn0 fn1 fn2.
+          (∀a. fn0 (TLeaf a) = f0 a) ∧ (∀a. fn0 (TNode a) = f1 a (fn1 a)) ∧
+          (∀a. fn1 (Node a) = f2 a (fn2 a)) ∧ fn2 [] = f3 ∧
+          ∀a0 a1. fn2 (a0::a1) = f4 a0 a1 (fn0 a0) (fn2 a1)
+   
+   [node_case_cong]  Theorem
+      
+      ⊢ ∀M M' f.
+          M = M' ∧ (∀a. M' = Node a ⇒ f a = f' a) ⇒
+          node_CASE M f = node_CASE M' f'
+   
+   [node_case_eq]  Theorem
+      
+      ⊢ node_CASE x f = v ⇔ ∃l. x = Node l ∧ f l = v
+   
+   [node_induction]  Theorem
+      
+      ⊢ ∀P0 P1 P2.
+          (∀a. P0 (TLeaf a)) ∧ (∀n. P1 n ⇒ P0 (TNode n)) ∧
+          (∀l. P2 l ⇒ P1 (Node l)) ∧ P2 [] ∧
+          (∀t l. P0 t ∧ P2 l ⇒ P2 (t::l)) ⇒
+          (∀t. P0 t) ∧ (∀n. P1 n) ∧ ∀l. P2 l
+   
+   [node_nchotomy]  Theorem
+      
+      ⊢ ∀nn. ∃l. nn = Node l
+   
+   [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
+   
+   [odd_def]  Theorem
+      
+      ⊢ ∀i. odd i = if i = 0 then Return F else even (i − 1)
+   
+   [tree_11]  Theorem
+      
+      ⊢ (∀a a'. TLeaf a = TLeaf a' ⇔ a = a') ∧
+        ∀a a'. TNode a = TNode a' ⇔ a = a'
+   
+   [tree_Axiom]  Theorem
+      
+      ⊢ ∀f0 f1 f2 f3 f4. ∃fn0 fn1 fn2.
+          (∀a. fn0 (TLeaf a) = f0 a) ∧ (∀a. fn0 (TNode a) = f1 a (fn1 a)) ∧
+          (∀a. fn1 (Node a) = f2 a (fn2 a)) ∧ fn2 [] = f3 ∧
+          ∀a0 a1. fn2 (a0::a1) = f4 a0 a1 (fn0 a0) (fn2 a1)
+   
+   [tree_case_cong]  Theorem
+      
+      ⊢ ∀M M' f f1.
+          M = M' ∧ (∀a. M' = TLeaf a ⇒ f a = f' a) ∧
+          (∀a. M' = TNode a ⇒ f1 a = f1' a) ⇒
+          tree_CASE M f f1 = tree_CASE M' f' f1'
+   
+   [tree_case_eq]  Theorem
+      
+      ⊢ tree_CASE x f f1 = v ⇔
+        (∃a. x = TLeaf a ∧ f a = v) ∨ ∃n. x = TNode n ∧ f1 n = v
+   
+   [tree_distinct]  Theorem
+      
+      ⊢ ∀a' a. TLeaf a ≠ TNode a'
+   
+   [tree_height_def]  Theorem
+      
+      ⊢ ∀tree.
+          tree_height tree =
+          case tree of
+            TLeaf v => Return 1
+          | TNode (Node ls) => tree_nodes_height ls
+   
+   [tree_induction]  Theorem
+      
+      ⊢ ∀P0 P1 P2.
+          (∀a. P0 (TLeaf a)) ∧ (∀n. P1 n ⇒ P0 (TNode n)) ∧
+          (∀l. P2 l ⇒ P1 (Node l)) ∧ P2 [] ∧
+          (∀t l. P0 t ∧ P2 l ⇒ P2 (t::l)) ⇒
+          (∀t. P0 t) ∧ (∀n. P1 n) ∧ ∀l. P2 l
+   
+   [tree_nchotomy]  Theorem
+      
+      ⊢ ∀tt. (∃a. tt = TLeaf a) ∨ ∃n. tt = TNode n
+   
+   [tree_nodes_height_def]  Theorem
+      
+      ⊢ ∀ls.
+          tree_nodes_height ls =
+          case ls of
+            [] => Return 0
+          | t::tl =>
+            do
+              h1 <- tree_height t;
+              h2 <- tree_nodes_height tl;
+              Return (h1 + h2)
+            od
+   
+   [tree_size_eq]  Theorem
+      
+      ⊢ tree1_size f = list_size (tree_size f)
+   
+   
+*)
+end