Make minor modifications to divDefLib

2 files changed, 65 insertions, 60 deletions

diff --git a/backends/hol4/divDefLib.sml b/backends/hol4/divDefLib.sml
index 80f47f65..f53ef6f8 100644
--- a/backends/hol4/divDefLib.sml
+++ b/backends/hol4/divDefLib.sml
@@ -896,9 +896,14 @@ 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 *)
+    (* Save the final equations as definitions.
+
+       Note that because we use the same names, doing this overrides the "raw"
+       definitions, which are then forgotten, which means we don't need to
+       manually delete them.
+     *)
     val thm_names = map (fn x => x ^ "_def") fnames
-    val _ = map save_thm (zip thm_names def_eqs)
+    val _ = map store_definition (zip thm_names def_eqs)
   in
     def_eqs
   end
diff --git a/backends/hol4/divDefLibTestTheory.sig b/backends/hol4/divDefLibTestTheory.sig
index 8da736ab..526f74a6 100644
--- a/backends/hol4/divDefLibTestTheory.sig
+++ b/backends/hol4/divDefLibTestTheory.sig
@@ -5,14 +5,20 @@ sig
   (*  Definitions  *)
     val btree_TY_DEF : thm
     val btree_case_def : thm
+    val btree_height_def : thm
     val btree_size_def : thm
+    val even_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 nth_def : thm
+    val odd_def : thm
     val tree_TY_DEF : thm
     val tree_case_def : thm
+    val tree_height_def : thm
+    val tree_nodes_height_def : thm
     val tree_size_def : thm
   
   (*  Theorems  *)
@@ -21,13 +27,11 @@ sig
     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
@@ -41,17 +45,13 @@ sig
     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
@@ -83,6 +83,19 @@ sig
       ⊢ (∀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_height_def]  Definition
+      
+      ⊢ ∀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_size_def]  Definition
       
       ⊢ (∀f a. btree_size f (BLeaf a) = 1 + f a) ∧
@@ -90,6 +103,10 @@ sig
           btree_size f (BNode a0 a1) =
           1 + (btree_size f a0 + btree_size f a1)
    
+   [even_def]  Definition
+      
+      ⊢ ∀i. even i = if i = 0 then Return T else odd (i − 1)
+   
    [list_t_TY_DEF]  Definition
       
       ⊢ ∃rep.
@@ -163,6 +180,20 @@ sig
       
       ⊢ ∀a f. node_CASE (Node a) f = f a
    
+   [nth_def]  Definition
+      
+      ⊢ ∀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]  Definition
+      
+      ⊢ ∀i. odd i = if i = 0 then Return F else even (i − 1)
+   
    [tree_TY_DEF]  Definition
       
       ⊢ ∃rep.
@@ -208,6 +239,27 @@ sig
       ⊢ (∀a f f1. tree_CASE (TLeaf a) f f1 = f a) ∧
         ∀a f f1. tree_CASE (TNode a) f f1 = f1 a
    
+   [tree_height_def]  Definition
+      
+      ⊢ ∀tree.
+          tree_height tree =
+          case tree of
+            TLeaf v => Return 1
+          | TNode (Node ls) => tree_nodes_height ls
+   
+   [tree_nodes_height_def]  Definition
+      
+      ⊢ ∀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_def]  Definition
       
       ⊢ (∀f a. tree_size f (TLeaf a) = 1 + f a) ∧
@@ -244,19 +296,6 @@ sig
       
       ⊢ ∀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)) ⇒
@@ -278,10 +317,6 @@ sig
       
       ⊢ 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'.
@@ -350,20 +385,6 @@ sig
       
       ⊢ ∀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') ∧
@@ -392,14 +413,6 @@ sig
       
       ⊢ ∀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.
@@ -412,19 +425,6 @@ sig
       
       ⊢ ∀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)