Fix minor issues

1 files changed, 61 insertions, 4 deletions

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 ()