Start working on divDefLib for diverging definitions

9 files changed, 995 insertions, 111 deletions

diff --git a/backends/hol4/divDefLib.sml b/backends/hol4/divDefLib.sml
new file mode 100644
index 00000000..bfd36af1
--- /dev/null
+++ b/backends/hol4/divDefLib.sml
@@ -0,0 +1,890 @@
+(* This file implements utilities to define potentially diverging functions *)
+
+open HolKernel boolLib bossLib Parse
+open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
+
+open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
+open primitivesLib
+
+(* TODO:
+pred_def_thms -> pred_defs
+pred_def_thm -> pred_def
+raw_def_thms -> raw_defs
+raw_def_thm -> raw_def
+
+fuel_defs_thm -> fuel_defs (and split the theorem)
+*)
+
+(* TotalDefn.Define *)
+
+(*
+Datatype:
+  list_t =
+    ListCons 't list_t
+  | ListNil
+End
+*)
+
+(* TODO: move *)
+fun list_mk_arrow (tys : hol_type list) (ret_ty : hol_type) : hol_type =
+  foldr (fn (ty, aty) => ty --> aty) ret_ty tys
+
+(*“test (x : bool) = (x <> F)” *)
+
+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 def_tms = (strip_conj o list_mk_conj o rev) (Defn.parse_quote def_qt)
+val def_tm = hd def_tms
+
+(* Small utilities *)
+val current_goal : term option ref = ref NONE
+
+(* Save a goal in {!current_goal} then prove it.
+
+   This way if the proof fails we can easily retrieve the goal for debugging
+   purposes.
+ *)
+fun save_goal_and_prove (g, tac) : thm =
+  let
+    val _ = current_goal := SOME g
+  in
+    prove (g, tac)
+  end
+  
+
+(*val def_qt = ‘
+(nth_fuel (n : num) (ls : 't list_t) (i : u32) : 't result =
+  case n of
+  | 0 => Loop
+  | SUC n => 
+    do 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_fuel n tl i0
+        od
+    | ListNil => 
+      Fail Failure
+    od)
+’*)
+
+val num_zero_tm = “0:num”
+val num_suc_tm = “SUC: num -> num”
+val num_ty = “:num”
+
+val fuel_def_suffix = "___fuel" (* TODO: name collisions *)
+val fuel_var_name = "$n" (* TODO: name collisions *)
+val fuel_var = mk_var (fuel_var_name, num_ty)
+val fuel_var0 = fuel_var
+val fuel_var1 = mk_var ("$m", “:num”) (* TODO: name collisions *)
+val fuel_vars_le = “^fuel_var0 <= ^fuel_var1”
+
+val fuel_predicate_suffix = "___P" (* TODO: name collisions *)
+
+val bool_ty = “:bool”
+
+val alpha_tyvar : hol_type = “:'a”
+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”
+
+val least_tm = “$LEAST”
+val le_tm = (fst o strip_comb) “x:num <= y:num”
+val true_tm = “T”
+val false_tm = “F”
+
+fun mk_diverge_tm (ty : hol_type) : term =
+  let
+    val diverge_ty = mk_thy_type {Thy="primitives", Tyop="result", Args = [ty] }
+    val diverge_tm = mk_thy_const { Thy="primitives", Name="Diverge", Ty=diverge_ty }
+  in
+    diverge_tm
+  end
+
+fun mk_fuel_defs (def_tms : term list) : thm =
+  let
+    (* Retrieve the identifiers.
+
+       Ex.: def_tm = “even (n : int) : bool result = if i = 0 then Return T else odd (i - 1))”
+       We want to retrive: id = “even”
+     *)
+    val app = lhs def_tm
+    val ids = map (fst o strip_comb o lhs) def_tms
+    (* In the definitions, replace the identifiers by new identifiers which use
+       fuel.
+
+       Ex.:
+       def_fuel_tm = “
+         even_fuel (fuel : nat) (n : int) : result bool =
+           case fuel of 0 => Diverge
+           | SUC fuel => 
+             if i = 0 then Return T else odd_fuel (i - 1))”
+     *)
+     fun mk_fuel_id (id : term) : term =
+       let
+         val (id_str, ty) = dest_var id
+         (* Note: we use symbols forbidden in the generation of code to
+            prevent name collisions *)
+         val fuel_id_str = id_str ^ fuel_def_suffix
+         val fuel_id = mk_var (fuel_id_str, num_ty --> ty)
+       in fuel_id end
+     val fuel_ids = map mk_fuel_id ids
+
+     val fuel_ids_with_fuel = map (fn id => mk_comb (id, fuel_var)) fuel_ids
+
+     (* Recurse through the terms and replace the calls *)
+     val rwr_thms = map (ASSUME o mk_eq) (zip ids fuel_ids_with_fuel)
+     val fuel_tms = map (rhs o concl o (PURE_REWRITE_CONV rwr_thms)) def_tms
+
+     (* Add the case over the fuel *)
+     fun add_fuel_case (tm : term) : term =
+       let
+         val (app, body) = dest_eq tm
+         (* Create the “Diverge” term with the proper type *)
+         val body_ty = type_of body
+         val return_ty =
+           case (snd o dest_type) body_ty of [ty] => ty
+           | _ => failwith "unexpected"
+         val diverge_tm = mk_diverge_tm return_ty
+         (* Create the “SUC fuel” term *)
+         val suc_tm = mk_comb (num_suc_tm, fuel_var)
+         val fuel_tm = TypeBase.mk_case (fuel_var, [(num_zero_tm, diverge_tm), (suc_tm, body)])
+       in mk_eq (app, fuel_tm) end
+     val fuel_tms = map add_fuel_case fuel_tms
+
+     (* Define the auxiliary definitions which use fuel *)
+     val fuel_defs_conj = list_mk_conj fuel_tms
+     (* Define the fuel definitions *)
+     val fuel_defs_thm = Define ‘^fuel_defs_conj’
+   in
+     fuel_defs_thm
+   end
+
+(*
+val (fuel_tms, fuel_defs_thm) = mk_fuel_defs def_tms
+val fuel_def_tms = map (snd o strip_forall) ((strip_conj o concl) fuel_defs_thm)
+val (def_tm, fuel_def_tm) = hd (zip def_tms fuel_def_tms)
+*)
+
+fun mk_is_diverge_tm (fuel_tm : term) : term =
+  case snd (dest_type (type_of fuel_tm)) of
+    [ret_ty] => mk_comb (inst [alpha_tyvar |-> ret_ty] is_diverge_tm, fuel_tm)
+   | _ => failwith "mk_is_diverge_tm: unexpected"
+
+fun mk_fuel_predicate_defs (def_tm, fuel_def_tm) : thm =
+  let
+    (* From [even i] create the term [even_P i n], where [n] is the fuel *)
+    val (id, args) = (strip_comb o lhs) def_tm
+    val (id_str, id_ty) = dest_var id
+    val {Args=tys, Thy=thy, Tyop=tyop} = dest_thy_type id_ty
+    val _ = assert (fn x => x = "fun") tyop;
+    val tys = rev tys;
+    val ret_ty = hd tys;
+    val tys = rev (num_ty :: tl tys);
+    val pred_ty = list_mk_arrow tys bool_ty
+    val pred_id = mk_var (id_str ^ fuel_predicate_suffix, pred_ty)
+    val pred_tm = list_mk_comb (pred_id, append args [fuel_var])
+
+    (* Create the term ~is_diverge (even_fuel n i) *)
+    val fuel_tm = lhs fuel_def_tm
+    val not_is_diverge_tm = mk_neg (mk_is_diverge_tm fuel_tm)
+
+    (* Create the term: even_P i n = ~(is_diverge (even_fuel n i) *)
+    val pred_def_tm = mk_eq (pred_tm, not_is_diverge_tm)
+  in
+    (* Create the definition *)
+    Define ‘^pred_def_tm’
+  end
+
+(*
+val pred_def_thms = map mk_fuel_predicate_defs (zip def_tms fuel_def_tms)
+*)
+
+(* Tactic which makes progress in a proof by making a case disjunction (we use
+   this to explore all the paths in a function body). *)
+fun case_progress (asms, g) =
+  let
+    val scrut = (strip_all_cases_get_scrutinee o lhs) g
+  in Cases_on ‘^scrut’ (asms, g) end
+
+(* Tactic to prove the fuel monotonicity theorem *)
+fun prove_fuel_mono_tac (pred_def_thms : thm list) (fuel_defs_thm : thm) =
+  Induct_on ‘^fuel_var0’ >-(
+    (* The ___P predicates are false: n is 0 *)
+    fs pred_def_thms >>
+    fs [is_diverge_def] >>
+    pure_once_rewrite_tac [fuel_defs_thm] >> fs []) >>
+  gen_tac >>
+  Cases_on ‘^fuel_var1’ >-(
+    (* Contradiction: SUC n < 0 *)
+    rw [] >> exfalso >> int_tac) >>
+  fs pred_def_thms >>
+  fs [is_diverge_def] >>
+  pure_once_rewrite_tac [fuel_defs_thm] >> fs [bind_def] >>
+  (* Split the goals *)
+  rw [] >>
+  (* Explore all the paths *)
+  rpt (case_progress >> fs [])
+
+(* Prove the fuel monotonicity properties.
+
+   We want to prove a theorem of the shape:
+   {[
+     !n m.
+       (!i. n <= m ==> even___P i n ==> even___fuel n i = even___fuel m i) /\
+       (!i. n <= m ==> odd___P i n ==> odd___fuel n i = odd___fuel m i)
+   ]}
+*)
+fun prove_fuel_mono (pred_def_thms : thm list) (fuel_defs_thm : thm) : thm =
+  let
+    val pred_tms = map (lhs o snd o strip_forall o concl) pred_def_thms
+    val fuel_tms = map (lhs o snd o strip_forall o concl) (CONJUNCTS fuel_defs_thm)
+    val pred_fuel_tms = zip pred_tms fuel_tms
+    (* Generate terms of the shape:
+       !i. n <= m ==> even___P i n ==> even___fuel n i = even___fuel m i
+     *)
+    fun mk_fuel_eq_tm (pred_tm, fuel_tm) : term =
+      let
+        (* Retrieve the variables which are not the fuel - for the quantifiers *)
+        val vars = (tl o snd o strip_comb) fuel_tm
+        (* Introduce the fuel term which uses “m” *)
+        val m_fuel_tm = subst [fuel_var0 |-> fuel_var1] fuel_tm
+        (* Introduce the equality *)
+        val fuel_eq_tm = mk_eq (fuel_tm, m_fuel_tm)
+        (* Introduce the implication with the _P pred *)
+        val fuel_eq_tm = mk_imp (pred_tm, fuel_eq_tm)
+        (* Introduce the “n <= m ==> ...” implication *)
+        val fuel_eq_tm = mk_imp (fuel_vars_le, fuel_eq_tm)
+        (* Quantify *)
+        val fuel_eq_tm = list_mk_forall (vars, fuel_eq_tm)
+      in fuel_eq_tm end
+     val fuel_eq_tms = map mk_fuel_eq_tm pred_fuel_tms
+     (* Create the conjunction *)
+     val fuel_eq_tms = list_mk_conj fuel_eq_tms
+(*     (* Add the “n <= m ==> ...” implication *)
+     val fuel_eq_tms = mk_imp (fuel_vars_le, fuel_eq_tms) *)
+     (* Qantify over the fuels *)
+     val fuel_eq_tms = list_mk_forall ([fuel_var0, fuel_var1], fuel_eq_tms)
+   in
+     (* Prove *)
+     save_goal_and_prove (fuel_eq_tms, prove_fuel_mono_tac pred_def_thms fuel_defs_thm)
+   end
+
+(*
+val fuel_mono_thm = prove_fuel_mono pred_def_thms fuel_defs_thm
+*)
+
+(* Prove the property about the least upper bound.
+
+   We want to prove theorems of the shape:
+   {[
+     (!n i. $LEAST (even___P i) <= n ==> even___fuel n i = even___fuel ($LEAST (even___P i)) i)
+   ]}
+   {[
+     (!n i. $LEAST (odd___P i) <= n ==> odd___fuel n i = odd___fuel ($LEAST (odd___P i)) i)
+   ]}
+
+   TODO: merge with other functions? (prove_pred_imp_fuel_eq_raw_thms)
+*)
+fun prove_least_fuel_mono (pred_def_thms : thm list) (fuel_mono_thm : thm) : thm list =
+  let
+    val thl = (CONJUNCTS o SPECL [fuel_var0, fuel_var1]) fuel_mono_thm
+    fun mk_least_fuel_thm (pred_def_thm, mono_thm) : thm =
+      let
+        (* Retrieve the predicate, without the fuel *)
+        val pred_tm = (lhs o snd o strip_forall o concl) pred_def_thm
+        val (pred_tm, args) = strip_comb pred_tm
+        val args = rev (tl (rev args))
+        val pred_tm = list_mk_comb (pred_tm, args)
+        (* Add $LEAST *)
+        val least_pred_tm = mk_comb (least_tm, pred_tm)
+        (* Specialize all *)
+        val vars = (fst o strip_forall o concl) mono_thm
+        val th = SPECL vars mono_thm
+        (* Substitute in the mono theorem *)
+        val th = INST [fuel_var0 |-> least_pred_tm] th
+        (* Symmetrize the equality *)
+        val th = PURE_ONCE_REWRITE_RULE [EQ_SYM_EQ] th
+        (* Quantify *)
+        val th = GENL (fuel_var1 :: vars) th
+      in
+        th
+      end
+  in
+    map mk_least_fuel_thm (zip pred_def_thms thl)
+  end
+
+(* Prove theorems of the shape:
+
+   {[
+     !n i. even___P i n ==> $LEAST (even___P i) <= n
+   ]}
+
+   TODO: merge with other functions? (prove_pred_imp_fuel_eq_raw_thms)
+ *)
+fun prove_least_pred_thms (pred_def_thms : thm list) : thm list =
+  let
+    fun prove_least_pred_thm (pred_def_thm : thm) : thm =
+      let
+        val pred_tm = (lhs o snd o strip_forall o concl) pred_def_thm
+        val (pred_no_fuel_tm, args) = strip_comb pred_tm
+        val args = rev (tl (rev args))
+        val pred_no_fuel_tm = list_mk_comb (pred_no_fuel_tm, args)
+        (* Make the “$LEAST (even___P i)” term *)
+        val least_pred_tm = mk_comb (least_tm, pred_no_fuel_tm)
+        (* Make the inequality *)
+        val tm = list_mk_comb (le_tm, [least_pred_tm, fuel_var0])
+        (* Add the implication *)
+        val tm = mk_imp (pred_tm, tm)
+        (* Quantify *)
+        val tm = list_mk_forall (args, tm)
+        val tm = mk_forall (fuel_var0, tm)
+        (* Prove *)
+        val prove_tac =
+          rpt gen_tac >>
+          disch_tac >>
+          (* Use the "fundamental" property about $LEAST *)
+          qspec_assume ‘^pred_no_fuel_tm’ whileTheory.LEAST_EXISTS_IMP >>
+          (* Prove the premise *)
+          pop_assum sg_premise_tac >- (exists_tac fuel_var0 >> fs []) >>
+          rw [] >>
+          (* Finish the proof by contraposition *)
+          spose_not_then assume_tac >>
+          fs [not_le_eq_gt]
+      in
+        save_goal_and_prove (tm, prove_tac)
+      end
+  in
+    map prove_least_pred_thm pred_def_thms
+  end
+
+
+(*
+val least_pred_thms = prove_least_pred_thms pred_def_thms
+
+val least_pred_thm = hd least_pred_thms
+*)
+
+(* Prove theorems of the shape:
+
+   {[
+     !n i. even___P i n ==> even___P i ($LEAST (even___P i))
+   ]}
+*)
+fun prove_pred_n_imp_pred_least_thms (pred_def_thms : thm list) : thm list =
+  let
+    fun prove_pred_n_imp_pred_least (pred_def_thm : thm) : thm =
+      let
+        val pred_tm = (lhs o snd o strip_forall o concl) pred_def_thm
+        val (pred_no_fuel_tm, args) = strip_comb pred_tm
+        val args = rev (tl (rev args))
+        val pred_no_fuel_tm = list_mk_comb (pred_no_fuel_tm, args)
+        (* Make the “$LEAST (even___P i)” term *)
+        val least_pred_tm = mk_comb (least_tm, pred_no_fuel_tm)
+        (* Make the “even___P i ($LEAST (even___P i))” *)
+        val tm = subst [fuel_var0 |-> least_pred_tm] pred_tm
+        (* Add the implication *)
+        val tm = mk_imp (pred_tm, tm)
+        (* Quantify *)
+        val tm = list_mk_forall (args, tm)
+        val tm = mk_forall (fuel_var0, tm)
+        (* The proof tactic *)
+        val prove_tac =
+          rpt gen_tac >>
+          disch_tac >>
+          (* Use the "fundamental" property about $LEAST *)
+          qspec_assume ‘^pred_no_fuel_tm’ whileTheory.LEAST_EXISTS_IMP >>
+          (* Prove the premise *)
+          pop_assum sg_premise_tac >- (exists_tac fuel_var0 >> fs []) >>
+          rw []
+      in
+        save_goal_and_prove (tm, prove_tac)
+      end
+  in
+    map prove_pred_n_imp_pred_least pred_def_thms
+  end
+
+(*
+val (pred_def_thm, mono_thm) = hd (zip pred_def_thms thl)
+val least_fuel_mono_thms = prove_least_fuel_mono pred_def_thms fuel_defs_thm fuel_mono_thm
+
+val least_fuel_mono_thm = hd least_fuel_mono_thms
+*)
+
+(* Define the "raw" definitions:
+
+   {[
+     even i = if (?n. even___P i n) then even___P ($LEAST (even___P i)) i else Diverge
+   ]}
+ *)
+fun define_raw_defs (def_tms : term list) (pred_def_thms : thm list) (fuel_defs_thm : thm) : thm list =
+  let
+    fun define_raw_def (def_tm, (pred_def_thm, fuel_def_thm)) : thm =
+      let
+        val app = lhs def_tm
+        val pred_tm = (lhs o snd o strip_forall o concl) pred_def_thm
+        (* Make the “?n. even___P i n” term *)
+        val exists_fuel_tm = mk_exists (fuel_var0, pred_tm)
+        (* Make the “even___fuel ($LEAST (even___P i)) i” term *)
+        val fuel_tm = (lhs o snd o strip_forall o concl) fuel_def_thm
+        val (pred_tm, args) = strip_comb pred_tm
+        val args = rev (tl (rev args))
+        val pred_tm = list_mk_comb (pred_tm, args)
+        val least_pred_tm = mk_comb (least_tm, pred_tm)
+        val fuel_tm = subst [fuel_var0 |-> least_pred_tm] fuel_tm
+        (* Create the Diverge term *)
+        val ret_ty = (hd o snd o dest_type) (type_of app)
+        (* Create the “if then else” *)
+        val body = TypeBase.mk_case (exists_fuel_tm, [(true_tm, fuel_tm), (false_tm, mk_diverge_tm ret_ty)])
+        (* *)
+        val raw_def_tm = mk_eq (app, body)
+      in
+        Define ‘^raw_def_tm’
+      end
+  in
+    map define_raw_def (zip def_tms (zip pred_def_thms (CONJUNCTS fuel_defs_thm)))
+  end
+
+(*
+val raw_def_thms = define_raw_defs def_tms pred_def_thms fuel_defs_thm
+ *)
+
+(*
+val pred_def_thm = hd pred_def_thms
+
+val pred_n_imp_pred_least_thms = prove_pred_n_imp_pred_least_thms pred_def_thms
+
+val pred_n_imp_pred_least_thm = hd pred_n_imp_pred_least_thms
+*)
+
+(* Prove theorems of the shape:
+
+   !n i. even___P i n ==> even___fuel n i = even i
+ *)
+fun prove_pred_imp_fuel_eq_raw_def_thms
+  (pred_def_thms : thm list)
+  (fuel_def_tms : term list)
+  (least_fuel_mono_thms : thm list)
+  (least_pred_thms : thm list)
+  (pred_n_imp_pred_least_thms : thm list)
+  (raw_def_thms : thm list) :
+  thm list =
+  let
+    fun prove_thm (pred_def_thm,
+                   (fuel_def_tm,
+                    (least_fuel_mono_thm,
+                     (least_pred_thm,
+                      (pred_n_imp_pred_least_thm, raw_def_thm))))) : thm =
+      let
+        (* Generate: “even___P i n” *)
+        val pred_tm = (lhs o snd o strip_forall o concl) pred_def_thm
+        val (pred_no_fuel_tm, args) = strip_comb pred_tm
+        val args = rev (tl (rev args))
+        (* Generate: “even___fuel n i” *)
+        val fuel_tm = lhs fuel_def_tm
+        (* Generate: “even i” *)
+        val raw_def_tm = (lhs o snd o strip_forall o concl) raw_def_thm
+        (* Generate: “even___fuel n i = even i” *)
+        val tm = mk_eq (fuel_tm, raw_def_tm)
+        (* Add the implication *)
+        val tm = mk_imp (pred_tm, tm)
+        (* Quantify *)
+        val tm = list_mk_forall (args, tm)
+        val tm = mk_forall (fuel_var0, tm)
+        (* Prove *)
+        val prove_tac =
+          rpt gen_tac >>
+          strip_tac >>
+          fs raw_def_thms >>
+          (* Case on ‘?n. even___P i n’ *)
+          CASE_TAC >> fs [] >>
+          (* Use the monotonicity property *)
+          irule least_fuel_mono_thm >>
+          imp_res_tac pred_n_imp_pred_least_thm >> fs [] >>
+          irule least_pred_thm >> fs []
+      in
+        save_goal_and_prove (tm, prove_tac)
+      end
+  in
+    map prove_thm (zip pred_def_thms (zip fuel_def_tms (zip least_fuel_mono_thms
+                   (zip least_pred_thms (zip pred_n_imp_pred_least_thms raw_def_thms)))))
+  end
+
+(*
+val pred_imp_fuel_eq_raw_def_thms =
+  prove_pred_imp_fuel_eq_raw_def_thms
+    pred_def_thms fuel_def_tms least_fuel_mono_thms least_pred_thms
+    pred_n_imp_pred_least_thms raw_def_thms
+
+val (pred_def_thm,
+                   (fuel_def_tm,
+                    (least_fuel_mono_thm,
+                     (least_pred_thm,
+                      (pred_n_imp_pred_least_thm, raw_def_thm))))) =
+  hd (zip pred_def_thms (zip fuel_def_tms (zip least_fuel_mono_thms
+                   (zip least_pred_thms (zip pred_n_imp_pred_least_thms raw_def_thms)))))
+ *)
+
+
+(* Generate "expand" definitions of the following shape (we use them to
+   hide the raw function bodies, to control the rewritings):
+
+   {[
+     even___expand even odd i : bool result =
+       if i = 0 then Return T else odd (i - 1)
+   ]}
+
+   {[
+     odd___expand even odd i : bool result =
+       if i = 0 then Return F else even (i - 1)
+   ]}
+
+ *)
+fun gen_expand_defs (def_tms : term list) =
+  let
+    (* Generate the variables for “even”, “odd”, etc. *)
+    val fun_vars = map (fst o strip_comb o lhs) def_tms
+    val fun_tys = map type_of fun_vars
+    (* Generate the expansion *)
+    fun mk_def (def_tm : term) : thm =
+      let
+        val (exp_fun, args) = (strip_comb o lhs) def_tm
+        val (exp_fun_str, exp_fun_ty) = dest_var exp_fun
+        val exp_fun_str = exp_fun_str ^ expand_suffix
+        val exp_fun_ty = list_mk_arrow fun_tys exp_fun_ty
+        val exp_fun = mk_var (exp_fun_str, exp_fun_ty)
+        val exp_fun = list_mk_comb (exp_fun, fun_vars)
+        val exp_fun = list_mk_comb (exp_fun, args)
+        val tm = mk_eq (exp_fun, rhs def_tm)
+      in
+        Define ‘^tm’
+      end
+  in
+    map mk_def def_tms
+  end
+
+(*
+val def_tm = hd def_tms
+
+val expand_defs = gen_expand_defs def_tms
+*)
+
+(* Small utility:
+
+   Return the list:
+   {[
+     (“even___P i n”, “even i = even___expand even odd i”),
+     ...
+   ]}
+   
+ *)
+fun mk_termination_diverge_tms
+  (pred_def_thms : thm list)
+  (raw_def_thms : thm list)
+  (expand_defs : thm list) :
+  (term * term) list =
+  let
+    (* Create the substitution for the "expand" functions:
+       {[
+         even -> even
+         odd -> odd
+         ...
+       ]}
+
+       where on the left we have *variables* and on the right we have
+       the "raw" definitions.
+     *)
+    fun mk_fun_subst (def_tm, raw_def_thm) =
+      let
+        val var = (fst o strip_comb o lhs) def_tm
+        val f = (fst o strip_comb o lhs o snd o strip_forall o concl) raw_def_thm
+      in
+        (var |-> f)
+      end
+    val fun_subst = map mk_fun_subst (zip def_tms raw_def_thms)
+  
+    fun mk_tm (pred_def_thm, (raw_def_thm, expand_def)) :
+      term * term =
+      let
+        (* “even___P i n” *)
+        val pred_tm = (lhs o snd o strip_forall o concl) pred_def_thm
+        (* “even i = even___expand even odd i” *)
+        val expand_tm = (lhs o snd o strip_forall o concl) expand_def
+        val expand_tm = subst fun_subst expand_tm
+        val fun_tm = (lhs o snd o strip_forall o concl) raw_def_thm
+        val fun_eq_tm = mk_eq (fun_tm, expand_tm)
+      in (pred_tm, fun_eq_tm) end
+  in
+    map mk_tm (zip pred_def_thms (zip raw_def_thms expand_defs))
+  end
+
+(*
+val term_div_tms =
+  mk_termination_diverge_tms pred_def_thms raw_def_thms expand_defs
+*)
+
+(* Prove the termination lemmas:
+   
+   {[
+     !i.
+       (?n. even___P i n) ==>
+         even i = even___expand even odd i
+   ]}
+ *)
+fun prove_termination_thms
+  (term_div_tms : (term * term) list)
+  (fuel_defs_thm : thm)
+  (pred_def_thms : thm list)
+  (raw_def_thms : thm list)
+  (expand_defs : thm list)
+  (pred_n_imp_pred_least_thms : thm list)
+  (pred_imp_fuel_eq_raw_def_thms : thm list)
+  : thm list =
+  let
+    (* Create a map from functions in the recursive group to lemmas
+       to apply *)
+    fun mk_rec_fun_eq_pair (fuel_def_thm, eq_th) =
+      let
+        val rfun = (get_fun_name_from_app o lhs o snd o strip_forall o concl) fuel_def_thm
+      in
+        (rfun, eq_th)
+      end
+    val rec_fun_eq_map =
+      Redblackmap.fromList const_name_compare (
+        map mk_rec_fun_eq_pair
+          (zip (CONJUNCTS fuel_defs_thm) pred_imp_fuel_eq_raw_def_thms))
+
+    (* Small tactic which rewrites the recursive calls *)
+    fun rewrite_rec_call (asms, g) =
+      let
+        val scrut = (strip_all_cases_get_scrutinee o lhs) g
+        val fun_id = get_fun_name_from_app scrut (* This can fail *)
+        (* This can raise an exception - hence the handle at the end
+           of the function *)
+        val eq_th = Redblackmap.find (rec_fun_eq_map, fun_id)
+        val eq_th = (UNDISCH_ALL o SPEC_ALL) eq_th
+        (* Match the theorem *)
+        val eq_th_tm = (lhs o concl) eq_th
+        val (var_s, ty_s) = match_term eq_th_tm scrut
+        val eq_th = INST var_s (INST_TYPE ty_s eq_th)
+        val eq_th = thm_to_conj_implies eq_th
+        (* Some tactics *)
+        val premise_tac = fs pred_def_thms >> fs [is_diverge_def]
+      in
+        (* Apply the theorem, prove the premise, and rewrite *)
+        (prove_premise_then premise_tac assume_tac eq_th >> fs []) (asms, g)
+      end handle NotFound => all_tac (asms, g)
+          | HOL_ERR _ => all_tac (asms, g) (* Getting the function name can also fail *)
+  
+    fun prove_one ((pred_tm, fun_eq_tm), pred_n_imp_pred_least_thm) :
+      thm =
+      let
+        (* “?n. even___P i n” *)
+        val pred_tm = mk_exists (fuel_var0, pred_tm)
+        (* “even i = even___expand even odd i” *)
+        val tm = fun_eq_tm
+        (* Add the implication *)
+        val tm = mk_imp (pred_tm, tm)
+        (* Quantify *)
+        val (_, args) = strip_comb fun_tm
+        val tm = list_mk_forall (args, tm)
+
+        (* Prove *)
+        val prove_tac =
+          rpt gen_tac >>
+          disch_tac >>
+
+          (* Expand the raw definition and get rid of the ‘?n ...’ *)
+          pure_once_rewrite_tac raw_def_thms >>
+          pure_asm_rewrite_tac [] >>
+
+          (* Simplify *)
+          fs [] >>
+
+          (* Prove that: “even___P i $(LEAST ...)” *)
+          imp_res_tac pred_n_imp_pred_least_thm >>
+
+          (* We don't need the ‘even___P i n’ assumption anymore: we have a more
+             precise one with the least upper bound *)
+          last_x_assum ignore_tac >>
+
+          (* Expand *)
+          fs pred_def_thms >>
+          fs [is_diverge_def] >>
+          fs expand_defs >>
+
+          (* We need to be a bit careful when expanding the definitions which use fuel:
+             it can make the simplifier loop. *)
+          rpt (pop_assum mp_tac) >>
+          pure_once_rewrite_tac [fuel_defs_thm]  >>
+          rpt disch_tac >>
+
+          (* Expand the binds *)
+          fs [bind_def] >>
+
+          (* Explore all the paths by doing case disjunctions *)
+          rpt (rewrite_rec_call >> case_progress >> fs [])
+      in
+        save_goal_and_prove (tm, prove_tac)
+      end
+  in
+    map prove_one
+      (zip term_div_tms pred_n_imp_pred_least_thms)
+  end
+
+(*
+val termination_thms =
+  prove_termination_thms term_div_tms fuel_defs_thm pred_def_thms
+    raw_def_thms expand_defs pred_n_imp_pred_least_thms
+    pred_imp_fuel_eq_raw_def_thms
+
+val expand_def = hd expand_defs
+
+val all_args = (zip pred_def_thms (zip raw_def_thms (zip expand_defs pred_n_imp_pred_least_thms)))
+val (pred_def_thm, (raw_def_thm, (expand_def,  pred_n_imp_pred_least_thm))) = hd all_args
+val (pred_def_thm, (raw_def_thm, (expand_def,  pred_n_imp_pred_least_thm))) = hd (tl all_args)
+
+set_goal ([], tm)
+*)
+
+(* Prove the divergence lemmas:
+
+   {[
+     !i.
+       (!n. ~even___P i n) ==>
+        (!n. ~even___P i (SUC n)) ==>
+         even i = even___expand even odd i
+   ]}
+
+   Note that the shape of the theorem is very precise: this helps for the proof.
+   Also, by correctly ordering the assumptions, we make sure that by rewriting
+   we don't convert one of the two to “T”.
+ *)
+fun prove_divergence_thms
+  (term_div_tms : (term * term) list)
+  (fuel_defs_thm : thm)
+  (pred_def_thms : thm list)
+  (raw_def_thms : thm list)
+  (expand_defs : thm list)
+  : thm list =
+  let
+    (* Create a set containing the names of all the functions in the recursive group *)
+    fun get_rec_fun_id (fuel_def_thm : thm) =
+     (get_fun_name_from_app o lhs o snd o strip_forall o concl) fuel_def_thm
+    val rec_fun_set =
+      Redblackset.fromList const_name_compare (
+        map get_rec_fun_id raw_def_thms)
+
+    (* Small tactic which rewrites the recursive calls *)
+    fun rewrite_rec_call (asms, g) =
+      let
+        val scrut = (strip_all_cases_get_scrutinee o lhs) g
+        val fun_id = get_fun_name_from_app scrut (* This can fail *)
+      in
+        (* Check if the function is part of the group we are considering *)
+        if Redblackset.member (rec_fun_set, fun_id) then
+          let
+            (* Create a subgoal “odd i = Diverge” *)
+            val ret_ty = (hd o snd o dest_type o type_of) scrut
+            val g = mk_eq (scrut, mk_diverge_tm ret_ty)
+
+            (* Create a subgoal: “?n. odd___P i n”.
+
+               It is a bit cumbersome because we have to lookup the proper
+               predicate (from “odd” we need to lookup “odd___P”) and we
+               may have to perform substitutions... We hack a bit by using
+               a conversion to rewrite “odd i” to a term which contains
+               the “?n. odd___P i n” we are looking for.
+             *)
+            val exists_g = (rhs o concl) (PURE_REWRITE_CONV raw_def_thms scrut)
+            val (_, exists_g, _) = TypeBase.dest_case exists_g
+            (* The tactic to prove the subgoal *)
+            val prove_sg_tac =
+              pure_rewrite_tac raw_def_thms >>
+              Cases_on ‘^exists_g’ >> pure_asm_rewrite_tac [] >> fs [] >>
+              (* There must only remain the positive case (i.e., “?n. ...”):
+                 we have a contradiction *)
+              exfalso >>
+              (* The end of the proof is done by opening the definitions *)
+              pop_assum mp_tac >>
+              fs pred_def_thms >> fs [is_diverge_def]
+          in
+            (SUBGOAL_THEN g assume_tac >- prove_sg_tac >> fs []) (asms, g)
+          end
+        else all_tac (asms, g) (* Nothing to do *)
+      end handle HOL_ERR _ => all_tac (asms, g)
+  
+    fun prove_one (pred_tm, fun_eq_tm) :
+      thm =
+      let
+        (* “!n. ~even___P i n” *)
+        val neg_pred_tm = mk_neg pred_tm
+        val pred_tm = mk_forall (fuel_var0, neg_pred_tm)
+        val pred_suc_tm = subst [fuel_var0 |-> numSyntax.mk_suc fuel_var0] neg_pred_tm
+        val pred_suc_tm = mk_forall (fuel_var0, pred_suc_tm)
+
+        (* “even i = even___expand even odd i” *)
+        val tm = fun_eq_tm
+
+        (* Add the implications *)
+        val tm = list_mk_imp ([pred_tm, pred_suc_tm], tm)
+
+        (* Quantify *)
+        val (_, args) = strip_comb fun_tm
+        val tm = list_mk_forall (args, tm)
+
+        (* Prove *)
+        val prove_tac =
+          rpt gen_tac >>
+
+          pure_rewrite_tac raw_def_thms >>
+          rpt disch_tac >>
+
+          (* This allows to simplify the “?n. even___P i n” *)
+          fs [] >>
+          (* We don't need the last assumption anymore *)
+          last_x_assum ignore_tac >>
+
+          (* Expand *)
+          fs pred_def_thms >> fs [is_diverge_def] >>
+          fs expand_defs >>
+
+          (* We need to be a bit careful when expanding the definitions which use fuel:
+             it can make the simplifier loop.
+           *)
+          pop_assum mp_tac >>
+          pure_once_rewrite_tac [fuel_defs_thm]  >>
+          rpt disch_tac >> fs [] >>
+
+          (* Evaluate all the paths *)
+          rpt (rewrite_rec_call >> case_progress >> fs [])
+      in
+        save_goal_and_prove (tm, prove_tac)
+      end
+  in
+    map prove_one term_div_tms
+  end
+
+(*
+val divergence_thms =
+  prove_divergence_thms
+    term_div_tms
+    fuel_defs_thm
+    pred_def_thms
+    raw_def_thms
+    expand_defs
+
+val (pred_tm, fun_eq_tm) = hd term_div_tms
+
+set_goal ([], tm)
+
+val (asms, g) = top_goal ()
+*)
diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml
index 28f8ab97..a718392b 100644
--- a/backends/hol4/primitivesBaseTacLib.sml
+++ b/backends/hol4/primitivesBaseTacLib.sml
@@ -5,6 +5,10 @@ struct
 open HolKernel boolLib bossLib Parse
 open boolTheory arithmeticTheory integerTheory intLib listTheory
 
+val debug = ref false
+
+fun print_dbg msg = if !debug then print msg else ()
+
 (* Remark: below, we also have conversions *)
 val gsym = GSYM
 
@@ -241,7 +245,7 @@ val th = SPEC_ALL NUM_SUB_1_EQ
  *)
 fun inst_match_in_terms
   (try_match: string Redblackset.set -> term -> term * thm)
-  (tl : term list) : thm list =
+  (tml : term list) : thm list =
   let
     (* We use a map when storing the theorems, to avoid storing the same theorem twice *)
     val inst_thms: (term, thm) Redblackmap.dict ref = ref (Redblackmap.mkDict Term.compare);
@@ -253,7 +257,7 @@ fun inst_match_in_terms
       end
       handle HOL_ERR _ => ();
     (* Explore the term *)
-    val _ = app (dep_apply_in_subterms try_instantiate (Redblackset.empty String.compare)) tl;
+    val _ = List.app (dep_apply_in_subterms try_instantiate (Redblackset.empty String.compare)) tml;
   in
     map snd (Redblackmap.listItems (!inst_thms))
   end
@@ -265,20 +269,24 @@ fun inst_match_in_terms
    [keep]: if this function returns false on an instantiated theorem, ignore
    the theorem.
  *)
-fun inst_match_concl_in_terms (keep : thm -> bool) (th : thm) (tl : term list) : thm list =
+fun inst_match_concl_in_terms (keep : thm -> bool) (th : thm) (tml : term list) : thm list =
   let
     val th = (UNDISCH_ALL o SPEC_ALL) th;
     fun try_match bvars t =
       let
-        val inst_th = inst_match_concl bvars th t;
-        val c = concl inst_th;
+        val _ = print_dbg ("inst_match_concl_in_terms: " ^ term_to_string t ^ "\n")
+        val inst_th = inst_match_concl bvars th t
+        val c = concl inst_th
+        val _ = print_dbg ("inst_match_concl_in_terms: matched with success\n")
       in
         (* Check that we mustn't ignore the theorem *)
         if keep inst_th then (lhs (concl inst_th), inst_th)
-        else failwith "inst_match_concl_in_terms: ignore theorem"
+        else
+          let val _ = print_dbg ("inst_match_concl_in_terms: matched failed\n") in
+          failwith "inst_match_concl_in_terms: ignore theorem" end
       end;
   in
-    inst_match_in_terms try_match tl
+    inst_match_in_terms try_match tml
   end
 
 (*
@@ -293,7 +301,7 @@ val thms = inst_match_concl_in_terms int_to_u32_id [t]
    instantiations of this theorem which make its first premise match subterms
    in the provided list of term.
  *)
-fun inst_match_first_premise_in_terms (keep : thm -> bool) (th : thm) (tl : term list) : thm list =
+fun inst_match_first_premise_in_terms (keep : thm -> bool) (th : thm) (tml : term list) : thm list =
   let
     val th = SPEC_ALL th;
     fun try_match bvars t =
@@ -304,7 +312,7 @@ fun inst_match_first_premise_in_terms (keep : thm -> bool) (th : thm) (tl : term
         else failwith "inst_match_first_premise_in_terms: ignore theorem"
       end;
   in
-    inst_match_in_terms try_match tl
+    inst_match_in_terms try_match tml
   end
 
 (*
@@ -321,13 +329,15 @@ val thms = inst_match_first_premise_in_terms th [t]
    Leaves the premises as subgoals if [prove_premise] doesn't prove them.
  *)
 fun apply_dep_rewrites_match_concl_with_terms_tac
-  (prove_premise : tactic) (then_tac : thm_tactic) (tl : term list) (th : thm) : tactic =
+  (prove_premise : tactic) (then_tac : thm_tactic)
+  (ignore_tml : term list)
+  (tml : term list) (th : thm) : tactic =
   let
-    val ignore = Redblackset.fromList Term.compare tl;
-    fun keep th = not (Redblackset.member (ignore, concl th));
+    val ignore = Redblackset.fromList Term.compare ignore_tml
+    fun keep th = not (Redblackset.member (ignore, concl th))
     (* Discharge the assumptions so that the goal is one single term *)
-    val thms = inst_match_concl_in_terms keep th tl;
-    val thms = map thm_to_conj_implies thms;
+    val thms = inst_match_concl_in_terms keep th tml
+    val thms = map thm_to_conj_implies thms
   in
     (* Apply each theorem *)
     map_every_tac (try_tac o sg_premise_then prove_premise then_tac) thms
@@ -340,14 +350,16 @@ fun apply_dep_rewrites_match_concl_with_terms_tac
  *)
 fun apply_dep_rewrites_match_concl_with_all_tac
   (prove_premise : tactic) (then_tac : thm_tactic) (th : thm) : tactic =
-  fn (asms, g) => apply_dep_rewrites_match_concl_with_terms_tac prove_premise then_tac (g :: asms) th (asms, g)
+  fn (asms, g) =>
+  apply_dep_rewrites_match_concl_with_terms_tac prove_premise then_tac asms (g :: asms) th (asms, g)
 
 (* Same as {!apply_dep_rewrites_match_concl_with_all_tac} but we only match the
    conclusion of the goal.
  *)
 fun apply_dep_rewrites_match_concl_with_goal_tac
   (prove_premise : tactic) (then_tac : thm_tactic) (th : thm) : tactic =
-  fn (asms, g) => apply_dep_rewrites_match_concl_with_terms_tac prove_premise then_tac [g] th (asms, g)
+  fn (asms, g) =>
+  apply_dep_rewrites_match_concl_with_terms_tac prove_premise then_tac asms [g] th (asms, g)
 
 (* A theorem might be of the shape: [H => A = B /\ C = D], in which
    case we can split it into:
@@ -362,7 +374,7 @@ fun split_rewrite_thm (th : thm) : thm list =
     val t = concl th;
     val (vars, t) = strip_forall t;
     val (impl, t) = strip_imp t;
-    val tl = strip_conj t;
+    val tml = strip_conj t;
     fun mk_goal (t : term) = list_mk_forall (vars, (list_mk_imp (impl, t)))
     val prove_tac =
       rpt gen_tac >> rpt disch_tac >>
@@ -375,7 +387,7 @@ fun split_rewrite_thm (th : thm) : thm list =
     fun transform_th (th : thm) : thm =
       (GEN_ALL o thm_to_conj_implies o SPEC_ALL o UNDISCH_ALL o SPEC_ALL) th
   in
-    map (transform_th o mk_th) tl
+    map (transform_th o mk_th) tml
   end
 
 (* A dependent rewrite tactic which introduces the premises in a new goal.
@@ -528,4 +540,55 @@ fun int_tac (asms, g) =
     first_tac [cooper_tac, exfalso >> cooper_tac]) (asms, g)
  end
 
+(* Repeatedly destruct cases and return the last scrutinee we get *)
+fun strip_all_cases_get_scrutinee (t : term) : term =
+  if TypeBase.is_case t
+  then
+    (* Remark.: [strip_case] is too smart for what we want.
+       For instance: (fst o strip_case) “if i = 0 then ... else ...”
+       returns “i” while we want to get “i = 0”.
+
+       We use [dest_case] for this reason.
+     *)
+    (strip_all_cases_get_scrutinee o (fn (_, x, _) => x) o TypeBase.dest_case) t
+  else t
+
+(*
+TypeBase.dest_case “case ls of [] => T | _ => F”
+TypeBase.strip_case “case ls of [] => T | _ => F”
+TypeBase.strip_case “case (if b then [] else [0, 1]) of [] => T | _ => F”
+TypeBase.strip_case “3”
+TypeBase.dest_case “3”
+
+strip_all_cases_get_scrutinee “case ls of [] => T | _ => F”
+strip_all_cases_get_scrutinee “case (if b then [] else [0, 1]) of [] => T | _ => F”
+strip_all_cases_get_scrutinee “3”
+*)
+
+(* Lexicographic order over pairs *)
+fun pair_compare (comp1 : 'a * 'a -> order) (comp2 : 'b * 'b -> order)
+  ((p1, p2) : (('a * 'b) * ('a * 'b))) : order =
+  let
+    val (x1, y1) = p1;
+    val (x2, y2) = p2;
+  in
+    case comp1 (x1, x2) of
+      LESS => LESS
+    | GREATER => GREATER
+    | EQUAL => comp2 (y1, y2)
+  end
+
+(* A constant name (theory, constant name) *)
+type const_name = string * string
+
+val const_name_compare = pair_compare String.compare String.compare
+
+(* Given a function call [f y0 ... yn] return the name of the function *)
+fun get_fun_name_from_app (t : term) : const_name =
+  let
+    val f = (fst o strip_comb) t;
+    val {Name=name, Thy=thy, Ty=_} = dest_thy_const f;
+    val cn = (thy, name);
+  in cn end
+
 end
diff --git a/backends/hol4/primitivesLib.sml b/backends/hol4/primitivesLib.sml
index 543ded23..057c57bd 100644
--- a/backends/hol4/primitivesLib.sml
+++ b/backends/hol4/primitivesLib.sml
@@ -181,24 +181,6 @@ val massage : tactic =
   assume_bounds_for_all_int_vars >>
   rewrite_with_dep_int_lemmas
 
-(* Lexicographic order over pairs *)
-fun pair_compare (comp1 : 'a * 'a -> order) (comp2 : 'b * 'b -> order)
-  ((p1, p2) : (('a * 'b) * ('a * 'b))) : order =
-  let
-    val (x1, y1) = p1;
-    val (x2, y2) = p2;
-  in
-    case comp1 (x1, x2) of
-      LESS => LESS
-    | GREATER => GREATER
-    | EQUAL => comp2 (y1, y2)
-  end
-
-(* A constant name (theory, constant name) *)
-type const_name = string * string
-
-val const_name_compare = pair_compare String.compare String.compare
-
 (* The registered spec theorems, that {!progress} will automatically apply.
 
    The keys are the function names (it is a pair, because constant names
@@ -265,14 +247,6 @@ fun get_spec_app (t : term) : term =
       else (fst o dest_eq) t;
   in t end
 
-(* Given a function call [f y0 ... yn] return the name of the function *)
-fun get_fun_name_from_app (t : term) : const_name =
-  let
-    val f = (fst o strip_comb) t;
-    val {Name=name, Thy=thy, Ty=_} = dest_thy_const f;
-    val cn = (thy, name);
-  in cn end
-
 (* Register a spec theorem in the spec database.
 
    For the shape of spec theorems, see {!get_spec_thm_app}.
@@ -376,25 +350,6 @@ val all_vec_lems = [
 ]
 val _ = app register_spec_thm all_vec_lems
 
-(* Repeatedly destruct cases and return the last scrutinee we get *)
-fun strip_all_cases_get_scrutinee (t : term) : term =
-  if TypeBase.is_case t
-  then (strip_all_cases_get_scrutinee o fst o TypeBase.strip_case) t
-  else t
-
-(*
-TypeBase.dest_case “case ls of [] => T | _ => F”
-TypeBase.strip_case “case ls of [] => T | _ => F”
-TypeBase.strip_case “case (if b then [] else [0, 1]) of [] => T | _ => F”
-TypeBase.strip_case “3”
-TypeBase.dest_case “3”
-
-strip_all_cases_get_scrutinee “case ls of [] => T | _ => F”
-strip_all_cases_get_scrutinee “case (if b then [] else [0, 1]) of [] => T | _ => F”
-strip_all_cases_get_scrutinee “3”
-*)
-
-
 (* Provided the goal contains a call to a monadic function, return this function call.
 
    The goal should be of the shape:
diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml
index 6dd9f6ec..969e9f6e 100644
--- a/backends/hol4/primitivesScript.sml
+++ b/backends/hol4/primitivesScript.sml
@@ -12,7 +12,7 @@ Datatype:
 End
 
 Datatype:
-  result = Return 'a | Fail error | Loop
+  result = Return 'a | Fail error | Diverge
 End
 
 Type M = ``: 'a result``
@@ -22,7 +22,7 @@ val bind_def = Define `
     case x of
       Return y => f y
     | Fail e => Fail e
-    | Loop => Loop`;
+    | Diverge => Diverge`;
 
 val bind_name = fst (dest_const “bind”)
 
diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index bac7fd4f..cf550f00 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -451,7 +451,7 @@ sig
       
       ⊢ ∀x f.
           monad_bind x f =
-          case x of Return y => f y | Fail e => Fail e | Loop => Loop
+          case x of Return y => f y | Fail e => Fail e | Diverge => Diverge
    
    [error_BIJ]  Definition
       
@@ -781,13 +781,13 @@ sig
       
       ⊢ (∀a f f1 v. result_CASE (Return a) f f1 v = f a) ∧
         (∀a f f1 v. result_CASE (Fail a) f f1 v = f1 a) ∧
-        ∀f f1 v. result_CASE Loop f f1 v = v
+        ∀f f1 v. result_CASE Diverge f f1 v = v
    
    [result_size_def]  Definition
       
       ⊢ (∀f a. result_size f (Return a) = 1 + f a) ∧
         (∀f a. result_size f (Fail a) = 1 + error_size a) ∧
-        ∀f. result_size f Loop = 0
+        ∀f. result_size f Diverge = 0
    
    [return_def]  Definition
       
@@ -993,7 +993,7 @@ sig
    
    [datatype_result]  Theorem
       
-      ⊢ DATATYPE (result Return Fail Loop)
+      ⊢ DATATYPE (result Return Fail Diverge)
    
    [error2num_11]  Theorem
       
@@ -1411,33 +1411,33 @@ sig
       
       ⊢ ∀f0 f1 f2. ∃fn.
           (∀a. fn (Return a) = f0 a) ∧ (∀a. fn (Fail a) = f1 a) ∧
-          fn Loop = f2
+          fn Diverge = f2
    
    [result_case_cong]  Theorem
       
       ⊢ ∀M M' f f1 v.
           M = M' ∧ (∀a. M' = Return a ⇒ f a = f' a) ∧
-          (∀a. M' = Fail a ⇒ f1 a = f1' a) ∧ (M' = Loop ⇒ v = v') ⇒
+          (∀a. M' = Fail a ⇒ f1 a = f1' a) ∧ (M' = Diverge ⇒ v = v') ⇒
           result_CASE M f f1 v = result_CASE M' f' f1' v'
    
    [result_case_eq]  Theorem
       
       ⊢ result_CASE x f f1 v = v' ⇔
         (∃a. x = Return a ∧ f a = v') ∨ (∃e. x = Fail e ∧ f1 e = v') ∨
-        x = Loop ∧ v = v'
+        x = Diverge ∧ v = v'
    
    [result_distinct]  Theorem
       
-      ⊢ (∀a' a. Return a ≠ Fail a') ∧ (∀a. Return a ≠ Loop) ∧
-        ∀a. Fail a ≠ Loop
+      ⊢ (∀a' a. Return a ≠ Fail a') ∧ (∀a. Return a ≠ Diverge) ∧
+        ∀a. Fail a ≠ Diverge
    
    [result_induction]  Theorem
       
-      ⊢ ∀P. (∀a. P (Return a)) ∧ (∀e. P (Fail e)) ∧ P Loop ⇒ ∀r. P r
+      ⊢ ∀P. (∀a. P (Return a)) ∧ (∀e. P (Fail e)) ∧ P Diverge ⇒ ∀r. P r
    
    [result_nchotomy]  Theorem
       
-      ⊢ ∀rr. (∃a. rr = Return a) ∨ (∃e. rr = Fail e) ∨ rr = Loop
+      ⊢ ∀rr. (∃a. rr = Return a) ∨ (∃e. rr = Fail e) ∨ rr = Diverge
    
    [u128_add_eq]  Theorem
       
diff --git a/backends/hol4/testHashmapScript.sml b/backends/hol4/testHashmapScript.sml
index 249bc0bf..77c97651 100644
--- a/backends/hol4/testHashmapScript.sml
+++ b/backends/hol4/testHashmapScript.sml
@@ -37,17 +37,6 @@ val list_t_v_def = Define ‘
   list_t_v (ListCons x tl) = x :: list_t_v tl
 ’
 
-(* TODO: move *)
-Theorem index_eq:
-  (∀x ls. index 0 (x :: ls) = x) ∧
-  (∀i x ls. index i (x :: ls) =
-    if (0 < i) ∨ (0 ≤ i ∧ i ≠ 0) then index (i - 1) ls
-    else (if i = 0 then x else ARB))
-Proof
-  rw [index_def] >> fs [] >>
-  exfalso >> cooper_tac
-QED
-
 Theorem nth_mut_fwd_spec:
   !(ls : 't list_t) (i : u32).
     u32_to_int i < len (list_t_v ls) ==>
@@ -57,7 +46,7 @@ Theorem nth_mut_fwd_spec:
     | Loop => F
 Proof
   Induct_on ‘ls’ >> rw [list_t_v_def, len_def] >~ [‘ListNil’]
-  >-(massage >> exfalso >> cooper_tac) >>
+  >-(massage >> int_tac) >>
   pure_once_rewrite_tac [nth_mut_fwd_def] >> rw [] >>
   fs [index_eq] >>
   progress >> progress
@@ -108,6 +97,7 @@ Theorem insert_lem:
       lookup key ls1 = SOME value /\
       (* The other bindings are left unchanged *)
       (!k. k <> key ==> lookup k ls = lookup k ls1)
+      (* TODO: invariant *)
     | Fail _ => F
     | Loop => F
 Proof
diff --git a/backends/hol4/testHashmapTheory.sig b/backends/hol4/testHashmapTheory.sig
index 64312406..fd22e05b 100644
--- a/backends/hol4/testHashmapTheory.sig
+++ b/backends/hol4/testHashmapTheory.sig
@@ -15,7 +15,6 @@ sig
   
   (*  Theorems  *)
     val datatype_list_t : thm
-    val index_eq : thm
     val insert_lem : thm
     val list_t_11 : thm
     val list_t_Axiom : thm
@@ -102,15 +101,6 @@ sig
       
       ⊢ DATATYPE (list_t ListCons ListNil)
    
-   [index_eq]  Theorem
-      
-      ⊢ (∀x ls. index 0 (x::ls) = x) ∧
-        ∀i x ls.
-          index i (x::ls) =
-          if 0 < i ∨ 0 ≤ i ∧ i ≠ 0 then index (i − 1) ls
-          else if i = 0 then x
-          else ARB
-   
    [insert_lem]  Theorem
       
       [oracles: DISK_THM] [axioms: insert_def] []
@@ -120,8 +110,8 @@ sig
             Return ls1 =>
               lookup key ls1 = SOME value ∧
               ∀k. k ≠ key ⇒ lookup k ls = lookup k ls1
-          | Fail v1 => F
-          | Loop => F
+          | Fail v3 => F
+          | Diverge => F
    
    [list_t_11]  Theorem
       
@@ -194,8 +184,8 @@ sig
           u32_to_int i < len (list_t_v ls) ⇒
           case nth_mut_fwd ls i of
             Return x => x = index (u32_to_int i) (list_t_v ls)
-          | Fail v1 => F
-          | Loop => F
+          | Fail v3 => F
+          | Diverge => F
    
    
 *)
diff --git a/backends/hol4/testScript.sml b/backends/hol4/testScript.sml
index a2d15117..8b4d523c 100644
--- a/backends/hol4/testScript.sml
+++ b/backends/hol4/testScript.sml
@@ -1481,6 +1481,7 @@ val nth_fuel_P_def = Define ‘
   nth_fuel_P ls i n = ~is_loop (nth_fuel n ls i)
 ’
 
+(* TODO: this is not the theorem we want: we want the one below *)
 Theorem nth_fuel_mono:
   !n m ls i.
     n <= m ==>
@@ -1533,7 +1534,7 @@ Proof
   pop_assum mp_tac >> CASE_TAC >> fs []
 QED
 
-Theorem nth_fuel_least_fail_mono:
+(*Theorem nth_fuel_least_fail_mono:
   !n ls i.
     n < $LEAST (nth_fuel_P ls i) ==>
     nth_fuel n ls i = Loop
@@ -1544,7 +1545,7 @@ Proof
   fs [nth_fuel_P_def, is_loop_def] >>
   pop_assum mp_tac >>
   CASE_TAC
-QED
+QED*)
 
 Theorem nth_fuel_least_success_mono:
   !n ls i.
@@ -1593,7 +1594,7 @@ val nth_expand_def = Define ‘
       Fail Failure
 ’             
 
-(* Prove the important theorems *)
+(* Prove the important theorems: termination case *)
 Theorem nth_def_terminates:
   !ls i.
   (?n. nth_fuel_P ls i n) ==>
@@ -1635,7 +1636,7 @@ Proof
   imp_res_tac nth_fuel_least_success_mono >> fs []
 QED
 
-(* Prove the important theorems *)
+(* Prove the important theorems: divergence case *)
 Theorem nth_def_loop:
   !ls i.
   (!n. ~nth_fuel_P ls i n) ==>
diff --git a/backends/hol4/testTheory.sig b/backends/hol4/testTheory.sig
index c1034394..21b74a39 100644
--- a/backends/hol4/testTheory.sig
+++ b/backends/hol4/testTheory.sig
@@ -102,7 +102,6 @@ sig
     val nth_fuel_P_mono : thm
     val nth_fuel_def : thm
     val nth_fuel_ind : thm
-    val nth_fuel_least_fail_mono : thm
     val nth_fuel_least_success_mono : thm
     val nth_fuel_mono : thm
     val num2error_11 : thm
@@ -695,10 +694,6 @@ sig
                P n ls i) ⇒
             ∀v v1 v2. P v v1 v2
    
-   [nth_fuel_least_fail_mono]  Theorem
-      
-      ⊢ ∀n ls i. n < $LEAST (nth_fuel_P ls i) ⇒ nth_fuel n ls i = Loop
-   
    [nth_fuel_least_success_mono]  Theorem
       
       ⊢ ∀n ls i.