1 files changed, 8 insertions, 90 deletions
diff --git a/backends/hol4/divDefLib.sml b/backends/hol4/divDefLib.sml
index 3ecb32df..59c1edaf 100644
--- a/backends/hol4/divDefLib.sml
+++ b/backends/hol4/divDefLib.sml
@@ -1,21 +1,21 @@
 (* This file implements utilities to define potentially diverging functions *)
 
+structure divDefLib :> divDefLib =
+struct
+
 open HolKernel boolLib bossLib Parse
 open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
 
 open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
 open primitivesLib
 
-(* TODO: move *)
-Theorem case_result_same_eq:
-  !(r : 'a result).
+val case_result_same_eq = prove (
+  “!(r : 'a result).
     (case r of
        Return x => Return x
      | Fail e => Fail e
-     | Diverge => Diverge) = r
-Proof
-  rw [] >> CASE_TAC
-QED
+     | Diverge => Diverge) = r”,
+  rw [] >> CASE_TAC)
 
 (*
 val ty = id_ty
@@ -90,8 +90,6 @@ val bool_ty = “:bool”
 val alpha_tyvar : hol_type = “:'a”
 val beta_tyvar : hol_type = “:'b”
 
-val is_diverge_def = Define ‘
-  is_diverge (r: 'a result) : bool = case r of Diverge => T | _ => F’
 val is_diverge_tm = “is_diverge: 'a result -> bool”
 val diverge_tm = “Diverge : 'a result”
 
@@ -1202,84 +1200,4 @@ fun DefineDiv (def_qt : term quotation) =
     final_eqs
   end
 
-(*
-
-val def_qt = ‘
-  (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 even_def = DefineDiv def_qt
-
-(* Complexigying the above definition *)
-val def_qt = ‘
-  (even (i : int) : bool result =
-    if i = 0 then
-      do
-        b <- Return T;
-        Return b
-      od
-    else do
-      b <- odd (i - 1);
-      Return b
-      od
-    ) /\
-  (odd (i : int) : bool result =
-    if i = 0 then
-      do
-        b <- Return F;
-        Return b
-      od
-    else do
-      b <- even (i - 1);
-      Return b
-      od)
-’
-
-val even_def = DefineDiv def_qt
-
-Datatype:
-  list_t =
-    ListCons 't list_t
-  | ListNil
-End
-
-val def_qt = ‘
-  nth_mut_fwd (ls : 't list_t) (i : u32) : 't result =
-  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);
-      nth_mut_fwd tl i0
-      od
-  | ListNil =>
-    Fail Failure
-’
-
-val nth_mut_fwd_def = DefineDiv def_qt
-
-(* Checking what happens with non terminal calls *)
-val def_qt = ‘
-  nth_mut_fwd (ls : 't list_t) (i : u32) : 't result =
-  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);
-      x <- nth_mut_fwd tl i0;
-      Return x
-      od
-  | ListNil => 
-    Fail Failure
-’
-
-val nth_mut_fwd_def = DefineDiv def_qt
-
-*)
+end