Cleanup the files of the HOL4 backend

16 files changed, 2938 insertions, 3080 deletions

diff --git a/backends/hol4/TestTheory.sig b/backends/hol4/TestTheory.sig
deleted file mode 100644
index 552662b8..00000000
--- a/backends/hol4/TestTheory.sig
+++ /dev/null
@@ -1,839 +0,0 @@
-signature TestTheory =
-sig
-  type thm = Thm.thm
-  
-  (*  Axioms  *)
-    val VEC_TO_LIST_BOUNDS : thm
-    val i32_to_int_bounds : thm
-    val insert_def : thm
-    val int_to_i32_id : thm
-    val int_to_u32_id : thm
-    val u32_to_int_bounds : thm
-  
-  (*  Definitions  *)
-    val distinct_keys_def : thm
-    val error_BIJ : thm
-    val error_CASE : thm
-    val error_TY_DEF : thm
-    val error_size_def : thm
-    val i32_add_def : thm
-    val i32_max_def : thm
-    val i32_min_def : thm
-    val int1_def : thm
-    val int2_def : thm
-    val is_loop_def : thm
-    val is_true_def : thm
-    val list_t_TY_DEF : thm
-    val list_t_case_def : thm
-    val list_t_size_def : thm
-    val list_t_v_def : thm
-    val lookup_def : thm
-    val mk_i32_def : thm
-    val mk_u32_def : thm
-    val nth_expand_def : thm
-    val nth_fuel_P_def : thm
-    val result_TY_DEF : thm
-    val result_case_def : thm
-    val result_size_def : thm
-    val st_ex_bind_def : thm
-    val st_ex_return_def : thm
-    val test1_def : thm
-    val test2_TY_DEF : thm
-    val test2_case_def : thm
-    val test2_size_def : thm
-    val test_TY_DEF : thm
-    val test_case_def : thm
-    val test_monad2_def : thm
-    val test_monad3_def : thm
-    val test_monad_def : thm
-    val test_size_def : thm
-    val u32_add_def : thm
-    val u32_max_def : thm
-    val u32_sub_def : thm
-    val usize_max_def : thm
-    val vec_len_def : thm
-  
-  (*  Theorems  *)
-    val I32_ADD_EQ : thm
-    val INT_OF_NUM_INJ : thm
-    val INT_THM1 : thm
-    val INT_THM2 : thm
-    val MK_I32_SUCCESS : thm
-    val MK_U32_SUCCESS : thm
-    val NAT_THM1 : thm
-    val NAT_THM2 : thm
-    val NUM_SUB_1_EQ : thm
-    val NUM_SUB_1_EQ1 : thm
-    val NUM_SUB_EQ : thm
-    val U32_ADD_EQ : thm
-    val U32_SUB_EQ : thm
-    val VEC_TO_LIST_INT_BOUNDS : thm
-    val datatype_error : thm
-    val datatype_list_t : thm
-    val datatype_result : thm
-    val datatype_test : thm
-    val datatype_test2 : thm
-    val error2num_11 : thm
-    val error2num_ONTO : thm
-    val error2num_num2error : thm
-    val error2num_thm : thm
-    val error_Axiom : thm
-    val error_EQ_error : thm
-    val error_case_cong : thm
-    val error_case_def : thm
-    val error_case_eq : thm
-    val error_induction : thm
-    val error_nchotomy : thm
-    val insert_lem : thm
-    val list_nth_mut_loop_loop_fwd_def : thm
-    val list_nth_mut_loop_loop_fwd_ind : 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 lookup_raw_def : thm
-    val lookup_raw_ind : thm
-    val nth_def : thm
-    val nth_def_loop : thm
-    val nth_def_terminates : thm
-    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
-    val num2error_ONTO : thm
-    val num2error_error2num : thm
-    val num2error_thm : thm
-    val result_11 : thm
-    val result_Axiom : thm
-    val result_case_cong : thm
-    val result_case_eq : thm
-    val result_distinct : thm
-    val result_induction : thm
-    val result_nchotomy : thm
-    val test2_11 : thm
-    val test2_Axiom : thm
-    val test2_case_cong : thm
-    val test2_case_eq : thm
-    val test2_distinct : thm
-    val test2_induction : thm
-    val test2_nchotomy : thm
-    val test_11 : thm
-    val test_Axiom : thm
-    val test_case_cong : thm
-    val test_case_eq : thm
-    val test_distinct : thm
-    val test_induction : thm
-    val test_nchotomy : thm
-  
-  val Test_grammars : type_grammar.grammar * term_grammar.grammar
-(*
-   [Omega] Parent theory of "Test"
-   
-   [int_arith] Parent theory of "Test"
-   
-   [words] Parent theory of "Test"
-   
-   [insert_def]  Axiom
-      
-      [oracles: ] [axioms: insert_def] []
-      ⊢ insert key value ls =
-        case ls of
-          ListCons (ckey,cvalue) tl =>
-            if ckey = key then Return (ListCons (ckey,value) tl)
-            else
-              do
-                tl0 <- insert key value tl;
-                Return (ListCons (ckey,cvalue) tl0)
-              od
-        | ListNil => Return (ListCons (key,value) ListNil)
-   
-   [u32_to_int_bounds]  Axiom
-      
-      [oracles: ] [axioms: u32_to_int_bounds] []
-      ⊢ ∀n. 0 ≤ u32_to_int n ∧ u32_to_int n ≤ u32_max
-   
-   [i32_to_int_bounds]  Axiom
-      
-      [oracles: ] [axioms: i32_to_int_bounds] []
-      ⊢ ∀n. i32_min ≤ i32_to_int n ∧ i32_to_int n ≤ i32_max
-   
-   [int_to_u32_id]  Axiom
-      
-      [oracles: ] [axioms: int_to_u32_id] []
-      ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ u32_to_int (int_to_u32 n) = n
-   
-   [int_to_i32_id]  Axiom
-      
-      [oracles: ] [axioms: int_to_i32_id] []
-      ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ i32_to_int (int_to_i32 n) = n
-   
-   [VEC_TO_LIST_BOUNDS]  Axiom
-      
-      [oracles: ] [axioms: VEC_TO_LIST_BOUNDS] []
-      ⊢ ∀v. (let l = LENGTH (vec_to_list v) in 0 ≤ l ∧ l ≤ 4294967295)
-   
-   [distinct_keys_def]  Definition
-      
-      ⊢ ∀ls.
-          distinct_keys ls ⇔
-          ∀i j.
-            i < LENGTH ls ⇒
-            j < LENGTH ls ⇒
-            FST (EL i ls) = FST (EL j ls) ⇒
-            i = j
-   
-   [error_BIJ]  Definition
-      
-      ⊢ (∀a. num2error (error2num a) = a) ∧
-        ∀r. (λn. n < 1) r ⇔ error2num (num2error r) = r
-   
-   [error_CASE]  Definition
-      
-      ⊢ ∀x v0. (case x of Failure => v0) = (λm. v0) (error2num x)
-   
-   [error_TY_DEF]  Definition
-      
-      ⊢ ∃rep. TYPE_DEFINITION (λn. n < 1) rep
-   
-   [error_size_def]  Definition
-      
-      ⊢ ∀x. error_size x = 0
-   
-   [i32_add_def]  Definition
-      
-      ⊢ ∀x y. i32_add x y = mk_i32 (i32_to_int x + i32_to_int y)
-   
-   [i32_max_def]  Definition
-      
-      ⊢ i32_max = 2147483647
-   
-   [i32_min_def]  Definition
-      
-      ⊢ i32_min = -2147483648
-   
-   [int1_def]  Definition
-      
-      ⊢ int1 = 32
-   
-   [int2_def]  Definition
-      
-      ⊢ int2 = -32
-   
-   [is_loop_def]  Definition
-      
-      ⊢ ∀r. is_loop r ⇔ case r of Return v2 => F | Fail v3 => F | Loop => T
-   
-   [is_true_def]  Definition
-      
-      ⊢ ∀x. is_true x = if x then Return () else Fail Failure
-   
-   [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
-   
-   [list_t_v_def]  Definition
-      
-      ⊢ list_t_v ListNil = [] ∧
-        ∀x tl. list_t_v (ListCons x tl) = x::list_t_v tl
-   
-   [lookup_def]  Definition
-      
-      ⊢ ∀key ls. lookup key ls = lookup_raw key (list_t_v ls)
-   
-   [mk_i32_def]  Definition
-      
-      ⊢ ∀n. mk_i32 n =
-            if i32_min ≤ n ∧ n ≤ i32_max then Return (int_to_i32 n)
-            else Fail Failure
-   
-   [mk_u32_def]  Definition
-      
-      ⊢ ∀n. mk_u32 n =
-            if 0 ≤ n ∧ n ≤ u32_max then Return (int_to_u32 n)
-            else Fail Failure
-   
-   [nth_expand_def]  Definition
-      
-      ⊢ ∀nth ls i.
-          nth_expand 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
-   
-   [nth_fuel_P_def]  Definition
-      
-      ⊢ ∀ls i n. nth_fuel_P ls i n ⇔ ¬is_loop (nth_fuel n ls i)
-   
-   [result_TY_DEF]  Definition
-      
-      ⊢ ∃rep.
-          TYPE_DEFINITION
-            (λa0.
-                 ∀ $var$('result').
-                   (∀a0.
-                      (∃a. a0 =
-                           (λa.
-                                ind_type$CONSTR 0 (a,ARB)
-                                  (λn. ind_type$BOTTOM)) a) ∨
-                      (∃a. a0 =
-                           (λa.
-                                ind_type$CONSTR (SUC 0) (ARB,a)
-                                  (λn. ind_type$BOTTOM)) a) ∨
-                      a0 =
-                      ind_type$CONSTR (SUC (SUC 0)) (ARB,ARB)
-                        (λn. ind_type$BOTTOM) ⇒
-                      $var$('result') a0) ⇒
-                   $var$('result') a0) rep
-   
-   [result_case_def]  Definition
-      
-      ⊢ (∀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
-   
-   [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
-   
-   [st_ex_bind_def]  Definition
-      
-      ⊢ ∀x f.
-          monad_bind x f =
-          case x of Return y => f y | Fail e => Fail e | Loop => Loop
-   
-   [st_ex_return_def]  Definition
-      
-      ⊢ ∀x. st_ex_return x = Return x
-   
-   [test1_def]  Definition
-      
-      ⊢ ∀x. test1 x = Return x
-   
-   [test2_TY_DEF]  Definition
-      
-      ⊢ ∃rep.
-          TYPE_DEFINITION
-            (λa0.
-                 ∀ $var$('test2').
-                   (∀a0.
-                      (∃a. a0 =
-                           (λa.
-                                ind_type$CONSTR 0 (a,ARB)
-                                  (λn. ind_type$BOTTOM)) a) ∨
-                      (∃a. a0 =
-                           (λa.
-                                ind_type$CONSTR (SUC 0) (ARB,a)
-                                  (λn. ind_type$BOTTOM)) a) ⇒
-                      $var$('test2') a0) ⇒
-                   $var$('test2') a0) rep
-   
-   [test2_case_def]  Definition
-      
-      ⊢ (∀a f f1. test2_CASE (Variant1_2 a) f f1 = f a) ∧
-        ∀a f f1. test2_CASE (Variant2_2 a) f f1 = f1 a
-   
-   [test2_size_def]  Definition
-      
-      ⊢ (∀f f1 a. test2_size f f1 (Variant1_2 a) = 1 + f a) ∧
-        ∀f f1 a. test2_size f f1 (Variant2_2 a) = 1 + f1 a
-   
-   [test_TY_DEF]  Definition
-      
-      ⊢ ∃rep.
-          TYPE_DEFINITION
-            (λa0.
-                 ∀ $var$('test').
-                   (∀a0.
-                      (∃a. a0 =
-                           (λa.
-                                ind_type$CONSTR 0 (a,ARB)
-                                  (λn. ind_type$BOTTOM)) a) ∨
-                      (∃a. a0 =
-                           (λa.
-                                ind_type$CONSTR (SUC 0) (ARB,a)
-                                  (λn. ind_type$BOTTOM)) a) ⇒
-                      $var$('test') a0) ⇒
-                   $var$('test') a0) rep
-   
-   [test_case_def]  Definition
-      
-      ⊢ (∀a f f1. test_CASE (Variant1 a) f f1 = f a) ∧
-        ∀a f f1. test_CASE (Variant2 a) f f1 = f1 a
-   
-   [test_monad2_def]  Definition
-      
-      ⊢ test_monad2 = do x <- Return T; Return x od
-   
-   [test_monad3_def]  Definition
-      
-      ⊢ ∀x. test_monad3 x = monad_ignore_bind (is_true x) (Return x)
-   
-   [test_monad_def]  Definition
-      
-      ⊢ ∀v. test_monad v = do x <- Return v; Return x od
-   
-   [test_size_def]  Definition
-      
-      ⊢ (∀f f1 a. test_size f f1 (Variant1 a) = 1 + f1 a) ∧
-        ∀f f1 a. test_size f f1 (Variant2 a) = 1 + f a
-   
-   [u32_add_def]  Definition
-      
-      ⊢ ∀x y. u32_add x y = mk_u32 (u32_to_int x + u32_to_int y)
-   
-   [u32_max_def]  Definition
-      
-      ⊢ u32_max = 4294967295
-   
-   [u32_sub_def]  Definition
-      
-      ⊢ ∀x y. u32_sub x y = mk_u32 (u32_to_int x − u32_to_int y)
-   
-   [usize_max_def]  Definition
-      
-      ⊢ usize_max = 4294967295
-   
-   [vec_len_def]  Definition
-      
-      ⊢ ∀v. vec_len v = int_to_u32 (&LENGTH (vec_to_list v))
-   
-   [I32_ADD_EQ]  Theorem
-      
-      [oracles: DISK_THM] [axioms: int_to_i32_id] []
-      ⊢ ∀x y.
-          i32_min ≤ i32_to_int x + i32_to_int y ⇒
-          i32_to_int x + i32_to_int y ≤ i32_max ⇒
-          ∃z. i32_add x y = Return z ∧
-              i32_to_int z = i32_to_int x + i32_to_int y
-   
-   [INT_OF_NUM_INJ]  Theorem
-      
-      ⊢ ∀n m. &n = &m ⇒ n = m
-   
-   [INT_THM1]  Theorem
-      
-      ⊢ ∀x y. x > 0 ⇒ y > 0 ⇒ x + y > 0
-   
-   [INT_THM2]  Theorem
-      
-      ⊢ ∀x. T
-   
-   [MK_I32_SUCCESS]  Theorem
-      
-      ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ mk_i32 n = Return (int_to_i32 n)
-   
-   [MK_U32_SUCCESS]  Theorem
-      
-      ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ mk_u32 n = Return (int_to_u32 n)
-   
-   [NAT_THM1]  Theorem
-      
-      ⊢ ∀n. n < n + 1
-   
-   [NAT_THM2]  Theorem
-      
-      ⊢ ∀n. n < n + 1
-   
-   [NUM_SUB_1_EQ]  Theorem
-      
-      ⊢ ∀x y. x = y − 1 ⇒ 0 ≤ x ⇒ Num y = SUC (Num x)
-   
-   [NUM_SUB_1_EQ1]  Theorem
-      
-      ⊢ ∀i. 0 ≤ i − 1 ⇒ Num i = SUC (Num (i − 1))
-   
-   [NUM_SUB_EQ]  Theorem
-      
-      ⊢ ∀x y z. x = y − z ⇒ 0 ≤ x ⇒ 0 ≤ z ⇒ Num y = Num z + Num x
-   
-   [U32_ADD_EQ]  Theorem
-      
-      [oracles: DISK_THM] [axioms: int_to_u32_id, u32_to_int_bounds] []
-      ⊢ ∀x y.
-          u32_to_int x + u32_to_int y ≤ u32_max ⇒
-          ∃z. u32_add x y = Return z ∧
-              u32_to_int z = u32_to_int x + u32_to_int y
-   
-   [U32_SUB_EQ]  Theorem
-      
-      [oracles: DISK_THM] [axioms: int_to_u32_id, u32_to_int_bounds] []
-      ⊢ ∀x y.
-          0 ≤ u32_to_int x − u32_to_int y ⇒
-          ∃z. u32_sub x y = Return z ∧
-              u32_to_int z = u32_to_int x − u32_to_int y
-   
-   [VEC_TO_LIST_INT_BOUNDS]  Theorem
-      
-      [oracles: DISK_THM] [axioms: VEC_TO_LIST_BOUNDS] []
-      ⊢ ∀v. (let l = &LENGTH (vec_to_list v) in 0 ≤ l ∧ l ≤ u32_max)
-   
-   [datatype_error]  Theorem
-      
-      ⊢ DATATYPE (error Failure)
-   
-   [datatype_list_t]  Theorem
-      
-      ⊢ DATATYPE (list_t ListCons ListNil)
-   
-   [datatype_result]  Theorem
-      
-      ⊢ DATATYPE (result Return Fail Loop)
-   
-   [datatype_test]  Theorem
-      
-      ⊢ DATATYPE (test Variant1 Variant2)
-   
-   [datatype_test2]  Theorem
-      
-      ⊢ DATATYPE (test2 Variant1_2 Variant2_2)
-   
-   [error2num_11]  Theorem
-      
-      ⊢ ∀a a'. error2num a = error2num a' ⇔ a = a'
-   
-   [error2num_ONTO]  Theorem
-      
-      ⊢ ∀r. r < 1 ⇔ ∃a. r = error2num a
-   
-   [error2num_num2error]  Theorem
-      
-      ⊢ ∀r. r < 1 ⇔ error2num (num2error r) = r
-   
-   [error2num_thm]  Theorem
-      
-      ⊢ error2num Failure = 0
-   
-   [error_Axiom]  Theorem
-      
-      ⊢ ∀x0. ∃f. f Failure = x0
-   
-   [error_EQ_error]  Theorem
-      
-      ⊢ ∀a a'. a = a' ⇔ error2num a = error2num a'
-   
-   [error_case_cong]  Theorem
-      
-      ⊢ ∀M M' v0.
-          M = M' ∧ (M' = Failure ⇒ v0 = v0') ⇒
-          (case M of Failure => v0) = case M' of Failure => v0'
-   
-   [error_case_def]  Theorem
-      
-      ⊢ ∀v0. (case Failure of Failure => v0) = v0
-   
-   [error_case_eq]  Theorem
-      
-      ⊢ (case x of Failure => v0) = v ⇔ x = Failure ∧ v0 = v
-   
-   [error_induction]  Theorem
-      
-      ⊢ ∀P. P Failure ⇒ ∀a. P a
-   
-   [error_nchotomy]  Theorem
-      
-      ⊢ ∀a. a = Failure
-   
-   [insert_lem]  Theorem
-      
-      [oracles: DISK_THM] [axioms: u32_to_int_bounds, insert_def] []
-      ⊢ ∀ls key value.
-          distinct_keys (list_t_v ls) ⇒
-          case insert key value ls of
-            Return ls1 =>
-              lookup key ls1 = SOME value ∧
-              ∀k. k ≠ key ⇒ lookup k ls = lookup k ls1
-          | Fail v1 => F
-          | Loop => F
-   
-   [list_nth_mut_loop_loop_fwd_def]  Theorem
-      
-      ⊢ ∀ls i.
-          list_nth_mut_loop_loop_fwd 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);
-                  list_nth_mut_loop_loop_fwd tl i0
-                od
-          | ListNil => Fail Failure
-   
-   [list_nth_mut_loop_loop_fwd_ind]  Theorem
-      
-      ⊢ ∀P. (∀ls i.
-               (∀x tl i0. ls = ListCons x tl ∧ u32_to_int i ≠ 0 ⇒ P tl i0) ⇒
-               P ls i) ⇒
-            ∀v v1. P v v1
-   
-   [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
-   
-   [lookup_raw_def]  Theorem
-      
-      ⊢ (∀key. lookup_raw key [] = NONE) ∧
-        ∀v ls key k.
-          lookup_raw key ((k,v)::ls) =
-          if k = key then SOME v else lookup_raw key ls
-   
-   [lookup_raw_ind]  Theorem
-      
-      ⊢ ∀P. (∀key. P key []) ∧
-            (∀key k v ls. (k ≠ key ⇒ P key ls) ⇒ P key ((k,v)::ls)) ⇒
-            ∀v v1. P v v1
-   
-   [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
-   
-   [nth_def_loop]  Theorem
-      
-      ⊢ ∀ls i. (∀n. ¬nth_fuel_P ls i n) ⇒ nth ls i = nth_expand nth ls i
-   
-   [nth_def_terminates]  Theorem
-      
-      ⊢ ∀ls i. (∃n. nth_fuel_P ls i n) ⇒ nth ls i = nth_expand nth ls i
-   
-   [nth_fuel_P_mono]  Theorem
-      
-      ⊢ ∀n m ls i.
-          n ≤ m ⇒ nth_fuel_P ls i n ⇒ nth_fuel n ls i = nth_fuel m ls i
-   
-   [nth_fuel_def]  Theorem
-      
-      ⊢ ∀n ls i.
-          nth_fuel n ls i =
-          case n of
-            0 => Loop
-          | SUC n' =>
-            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_fuel n' tl i0 od
-            | ListNil => Fail Failure
-   
-   [nth_fuel_ind]  Theorem
-      
-      ⊢ ∀P. (∀n ls i.
-               (∀n' x tl i0.
-                  n = SUC n' ∧ ls = ListCons x tl ∧ u32_to_int i ≠ 0 ⇒
-                  P n' tl i0) ⇒
-               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.
-          $LEAST (nth_fuel_P ls i) ≤ n ⇒
-          nth_fuel n ls i = nth_fuel ($LEAST (nth_fuel_P ls i)) ls i
-   
-   [nth_fuel_mono]  Theorem
-      
-      ⊢ ∀n m ls i.
-          n ≤ m ⇒
-          if is_loop (nth_fuel n ls i) then T
-          else nth_fuel n ls i = nth_fuel m ls i
-   
-   [num2error_11]  Theorem
-      
-      ⊢ ∀r r'. r < 1 ⇒ r' < 1 ⇒ (num2error r = num2error r' ⇔ r = r')
-   
-   [num2error_ONTO]  Theorem
-      
-      ⊢ ∀a. ∃r. a = num2error r ∧ r < 1
-   
-   [num2error_error2num]  Theorem
-      
-      ⊢ ∀a. num2error (error2num a) = a
-   
-   [num2error_thm]  Theorem
-      
-      ⊢ num2error 0 = Failure
-   
-   [result_11]  Theorem
-      
-      ⊢ (∀a a'. Return a = Return a' ⇔ a = a') ∧
-        ∀a a'. Fail a = Fail a' ⇔ a = a'
-   
-   [result_Axiom]  Theorem
-      
-      ⊢ ∀f0 f1 f2. ∃fn.
-          (∀a. fn (Return a) = f0 a) ∧ (∀a. fn (Fail a) = f1 a) ∧
-          fn Loop = 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') ⇒
-          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'
-   
-   [result_distinct]  Theorem
-      
-      ⊢ (∀a' a. Return a ≠ Fail a') ∧ (∀a. Return a ≠ Loop) ∧
-        ∀a. Fail a ≠ Loop
-   
-   [result_induction]  Theorem
-      
-      ⊢ ∀P. (∀a. P (Return a)) ∧ (∀e. P (Fail e)) ∧ P Loop ⇒ ∀r. P r
-   
-   [result_nchotomy]  Theorem
-      
-      ⊢ ∀rr. (∃a. rr = Return a) ∨ (∃e. rr = Fail e) ∨ rr = Loop
-   
-   [test2_11]  Theorem
-      
-      ⊢ (∀a a'. Variant1_2 a = Variant1_2 a' ⇔ a = a') ∧
-        ∀a a'. Variant2_2 a = Variant2_2 a' ⇔ a = a'
-   
-   [test2_Axiom]  Theorem
-      
-      ⊢ ∀f0 f1. ∃fn.
-          (∀a. fn (Variant1_2 a) = f0 a) ∧ ∀a. fn (Variant2_2 a) = f1 a
-   
-   [test2_case_cong]  Theorem
-      
-      ⊢ ∀M M' f f1.
-          M = M' ∧ (∀a. M' = Variant1_2 a ⇒ f a = f' a) ∧
-          (∀a. M' = Variant2_2 a ⇒ f1 a = f1' a) ⇒
-          test2_CASE M f f1 = test2_CASE M' f' f1'
-   
-   [test2_case_eq]  Theorem
-      
-      ⊢ test2_CASE x f f1 = v ⇔
-        (∃T'. x = Variant1_2 T' ∧ f T' = v) ∨
-        ∃T'. x = Variant2_2 T' ∧ f1 T' = v
-   
-   [test2_distinct]  Theorem
-      
-      ⊢ ∀a' a. Variant1_2 a ≠ Variant2_2 a'
-   
-   [test2_induction]  Theorem
-      
-      ⊢ ∀P. (∀T. P (Variant1_2 T)) ∧ (∀T. P (Variant2_2 T)) ⇒ ∀t. P t
-   
-   [test2_nchotomy]  Theorem
-      
-      ⊢ ∀tt. (∃T. tt = Variant1_2 T) ∨ ∃T. tt = Variant2_2 T
-   
-   [test_11]  Theorem
-      
-      ⊢ (∀a a'. Variant1 a = Variant1 a' ⇔ a = a') ∧
-        ∀a a'. Variant2 a = Variant2 a' ⇔ a = a'
-   
-   [test_Axiom]  Theorem
-      
-      ⊢ ∀f0 f1. ∃fn.
-          (∀a. fn (Variant1 a) = f0 a) ∧ ∀a. fn (Variant2 a) = f1 a
-   
-   [test_case_cong]  Theorem
-      
-      ⊢ ∀M M' f f1.
-          M = M' ∧ (∀a. M' = Variant1 a ⇒ f a = f' a) ∧
-          (∀a. M' = Variant2 a ⇒ f1 a = f1' a) ⇒
-          test_CASE M f f1 = test_CASE M' f' f1'
-   
-   [test_case_eq]  Theorem
-      
-      ⊢ test_CASE x f f1 = v ⇔
-        (∃b. x = Variant1 b ∧ f b = v) ∨ ∃a. x = Variant2 a ∧ f1 a = v
-   
-   [test_distinct]  Theorem
-      
-      ⊢ ∀a' a. Variant1 a ≠ Variant2 a'
-   
-   [test_induction]  Theorem
-      
-      ⊢ ∀P. (∀b. P (Variant1 b)) ∧ (∀a. P (Variant2 a)) ⇒ ∀t. P t
-   
-   [test_nchotomy]  Theorem
-      
-      ⊢ ∀tt. (∃b. tt = Variant1 b) ∨ ∃a. tt = Variant2 a
-   
-   
-*)
-end
diff --git a/backends/hol4/divDefExampleScript.sml b/backends/hol4/divDefExampleScript.sml
new file mode 100644
index 00000000..338385ab
--- /dev/null
+++ b/backends/hol4/divDefExampleScript.sml
@@ -0,0 +1,418 @@
+(* Manually written examples of how to use the fixed-point operator from divDefScript *)
+
+open HolKernel boolLib bossLib Parse
+open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
+
+open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
+open primitivesLib
+open divDefTheory
+
+val _ = new_theory "divDefExample"
+
+(* Rewrite the goal once, and on the left part of the goal seen as an application *)
+fun pure_once_rewrite_left_tac ths =
+  CONV_TAC (PATH_CONV "l" (PURE_ONCE_REWRITE_CONV ths))
+
+(*=============================================
+ * Example 1: nth (simply recursive function)
+ *=============================================*)
+
+Datatype:
+  list_t =
+    ListCons 't list_t
+  | ListNil
+End
+
+(* We want to use the fixed-point operator ‘fix’ to define a function ‘nth’
+   which satisfies the following equation: *)
+
+val nth_qt = ‘
+  nth (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 tl i0
+        od
+    | ListNil => Fail Failure
+’
+
+(* When generating a recursive definition, we apply a fixed-point operator to a
+   non-recursive function *body*, in which the recursive calls are handled to
+   a continuation. In case we define a group of mutually recursive
+   definitions, we generate *one* single body for the whole group of definitions.
+   It works as follows.
+
+   The input of the body is an enumeration: we start by branching over this input such
+   that every branch corresponds to one function in the mutually recursive group.
+   Whenever we make a recursive call, we wrap the input parameters into the proper
+   variant before calling the continuation: in effect this allows us to choose
+   the function from the group which gets evaluated.
+
+   Moreover, because of constraints on the way the fixed-point operator is defined,
+   the input of the body must have the same type as its output: we also
+   store the outputs of the functions in this big enumeration.
+
+   In order to make this work, we need to shape the body so that:
+   - input values (at call sites) and output values (when returning) are properly
+     injected into the enumeration
+   - whenever we get an output value (which is an enumeration) from a recursive
+     call, we extract the value from the proper variant of the enumeration
+
+   We encode the enumeration with a nested sum type, whose constructors
+   are ‘INL’ and ‘INR’.
+
+   In the case of ‘nth’, we generate the encoding below, with the following
+   peculiarities:
+   - the input type is ‘: ('t list_t # u32) + 't’ the same as the output type
+     (modulo the ‘:result’). ‘:'t list_t # u32’ is for the input value, while
+     ‘t’ is for the output.
+ *)
+
+val nth_body_def = Define ‘
+  nth_body
+    (* The continuation is used for the recursive calls - this is required
+       by the fixed-point operator *)
+    (f : (('t list_t # u32) + 't) -> (('t list_t # u32) + 't) result)
+    
+    (* The input. Its type is: nth input type + nth output type *)
+    (x : (('t list_t # u32) + 't)) :
+
+    (* The output type is the same as the input type - this constraint
+       comes from limitations in the way we can define the fixed-point
+       operator inside the HOL logic *)
+    (('t list_t # u32) + 't) result =
+
+    (* Destruct the input. We need this to call the proper function in case
+       of mutually recursive definitions, but also to eliminate arguments
+       which correspond to the output value (the input type is the same
+       as the output type). *)
+    case x of
+    | INL x => ( (* Input case: normal function call *)
+      (* Body of nth *)
+      let (ls, i) = x in
+      case ls of
+      | ListCons x tl =>
+        if u32_to_int i = (0:int)
+        then Return (INR x)
+        else
+          do
+          i0 <- u32_sub i (int_to_u32 1);
+          (* Recursive call: we call the continuation.
+
+             We must wrap the input (here, in INL) then extract the
+             proper output (this last part is really important in
+             case of mutually recursive definitions).
+           *)
+          x <- (case f (INL (tl, i0)) of
+                | Fail e => Fail e
+                | Diverge => Diverge
+                | Return r =>
+                  case r of
+                  | INL _ => Fail Failure
+                  | INR x => Return x);
+
+          (* Wrap the return value *)
+          Return (INR x)
+          od
+      | ListNil => Fail Failure)
+    | INR _ => (* Output case: invalid, we fail *)
+      Fail Failure
+’
+
+(* Then, we prove that the body we just defined satisfies the validity property
+   required by the fixed-point theorem.
+
+   Remark:
+   We first prove the theorem with ‘SUC (SUC n)’ where ‘n’ is a variable
+   to prevent this quantity from being rewritten to 2 during the proofs. *)
+Theorem nth_body_is_valid_aux:
+  is_valid_fp_body (SUC (SUC n)) nth_body
+Proof
+  pure_once_rewrite_tac [is_valid_fp_body_def] >>
+  gen_tac >>
+  (* Expand *)
+  fs [nth_body_def, bind_def] >>
+  (* Simply explore all paths *)
+  Cases_on ‘x’ >> fs [] >>
+  Cases_on ‘x'’ >> fs [] >>
+  Cases_on ‘q’ >> fs [] >>
+  Cases_on ‘u32_to_int r = 0’ >> fs [] >>
+  Cases_on ‘u32_sub r (int_to_u32 1)’ >> fs [] >>
+  fs [case_result_switch_eq] >>
+  (* Recursive call *)
+  disj2_tac >>
+  qexists ‘\g x. case case x of INL v => Fail Failure | INR x => Return x of
+             Return x => Return (INR x)
+           | Fail e => Fail e
+           | Diverge => Diverge’ >>
+  qexists ‘INL (l, a)’ >>
+  conj_tac
+  >-(pure_once_rewrite_tac [is_valid_fp_body_def] >> fs []) >>
+  gen_tac >>
+  (* Explore all paths *)
+  Cases_on ‘g (INL (l,a))’ >> fs [] >>
+  Cases_on ‘a'’ >> fs []
+QED
+
+Theorem nth_body_is_valid:
+  is_valid_fp_body (SUC (SUC 0)) nth_body
+Proof
+  irule nth_body_is_valid_aux
+QED
+
+(* We can now define ‘nth’ in terms of the fixed-point operator applied to ‘nth_body’.
+
+   Important points:
+   - we apply ‘fix’ to ‘fix_body’
+   - we wrap the input to take the proper branch (‘INL (ls, i)’)
+   - we extract the output to have a function with the proper output type
+
+   This definition satisfies the equation we want (see next theorem). *)
+val nth_raw_def = Define ‘
+  nth (ls : 't list_t) (i : u32) =
+    case fix nth_body (INL (ls, i)) of
+    | Fail e => Fail e
+    | Diverge => Diverge
+    | Return r =>
+      case r of
+      | INL _ => Fail Failure
+      | INR x => Return x
+’
+
+(* We finally prove the target unfolding equation for ‘nth’ *)
+Theorem nth_def:
+  ∀ls i. nth (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 tl i0
+        od
+    | ListNil => Fail Failure
+Proof
+  rpt strip_tac >>
+  (* Expand the raw definition *)
+  pure_rewrite_tac [nth_raw_def] >>
+  (* Use the fixed-point equality - the rewrite must only be applied *on the left* of the equality, in the goal *)
+  pure_once_rewrite_left_tac [HO_MATCH_MP fix_fixed_eq nth_body_is_valid] >>
+  (* Expand the body definition *)
+  pure_rewrite_tac [nth_body_def] >>
+  (* Explore all the paths - maybe we can be smarter, but this is fast and really easy *)
+  fs [bind_def] >>
+  Cases_on ‘ls’ >> fs [] >>
+  Cases_on ‘u32_to_int i = 0’ >> fs [] >>
+  Cases_on ‘u32_sub i (int_to_u32 1)’ >> fs [] >>
+  Cases_on ‘fix nth_body (INL (l,a))’ >> fs [] >>
+  Cases_on ‘a'’ >> fs []
+QED
+
+(*=======================================================*
+ * Example 2: even, odd (mutually recursive definitions)
+ *=======================================================*)
+
+(* We consider the following group of mutually recursive definitions: *)
+
+val even_odd_qt = Defn.parse_quote ‘
+ (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))
+’
+
+(* Similarly to ‘nth’, we need to introduce a body on which to apply the
+   fixed-point operator. Here, the body is slightly more complex because
+   we have mutually recursive functions.
+
+   In particular, the input/output types is a sum of 4 types:
+   input of even + output of even + input of odd + output of odd
+   
+   That is: ‘: int + bool + int + bool’
+
+   As a consequence, the body is a case with 4 branches.
+ *)
+
+val even_odd_body_def = Define ‘
+  even_odd_body
+    (* The body takes a continuation - required by the fixed-point operator *)
+    (f : (int + bool + int + bool) -> (int + bool + int + bool) result)
+
+    (* The type of the input is:
+       input of even + output of even + input of odd + output of odd *)
+    (x : int + bool + int + bool) :
+
+    (* The output type is the same as the input type - this constraint
+       comes from limitations in the way we can define the fixed-point
+       operator inside the HOL logic *)
+    (int + bool + int + bool) result =
+
+  (* Case disjunction over the input, in order to figure out which
+     function from the group is actually called (even, or odd). *)
+  case x of
+  | INL i => (* Input of even *)
+    (* Body of even *)
+    if i = 0 then Return (INR (INL T))
+    else
+      (* Recursive calls are calls to the continuation f, wrapped
+         in the proper variant: here we call odd *)
+      (case f (INR (INR (INL (i - 1)))) of
+       | Fail e => Fail e
+       | Diverge => Diverge
+       | Return r =>
+         (* Extract the proper value from the enumeration: here, the
+            call is tail-call so this is not really necessary, but we
+            might need to retrieve the output of the call to odd, which
+            is a boolean, and do something more complex with it. *)
+         case r of
+         | INL _ => Fail Failure
+         | INR (INL _) => Fail Failure
+         | INR (INR (INL _)) => Fail Failure
+         | INR (INR (INR b)) => (* Extract the output of odd *)
+           (* Return: inject into the variant for the output of even *)
+           Return (INR (INL b))
+         )
+  | INR (INL _) => (* Output of even *)
+    (* We must ignore this one *)
+    Fail Failure
+  | INR (INR (INL i)) =>
+    (* Body of odd *)
+    if i = 0 then Return (INR (INR (INR F)))
+    else
+      (* Call to even *)
+      (case f (INL (i - 1)) of
+       | Fail e => Fail e
+       | Diverge => Diverge
+       | Return r =>
+         (* Extract the proper value from the enumeration *)
+         case r of
+         | INL _ => Fail Failure
+         | INR (INL b) => (* Extract the output of even *)
+           (* Return: inject into the variant for the output of odd *)
+           Return (INR (INR (INR b)))
+         | INR (INR (INL _)) => Fail Failure
+         | INR (INR (INR _)) => Fail Failure
+         )
+  | INR (INR (INR _)) => (* Output of odd *)
+    (* We must ignore this one *)
+    Fail Failure
+’
+
+(* We then prove that this body satisfies the validity condition *)
+Theorem even_odd_body_is_valid_aux:
+  is_valid_fp_body (SUC (SUC n)) even_odd_body
+Proof
+  pure_once_rewrite_tac [is_valid_fp_body_def] >>
+  gen_tac >>
+  (* Expand *)
+  fs [even_odd_body_def, bind_def] >>
+  (* Explore the body *)
+  Cases_on ‘x’ >> fs []
+  >-(
+    Cases_on ‘x' = 0’ >> fs [] >>
+    (* Recursive call *)
+    disj2_tac >>
+    qexists ‘\g x. case x of
+              | INL v => Fail Failure
+              | INR (INL v2) => Fail Failure
+              | INR (INR (INL v4)) => Fail Failure
+              | INR (INR (INR b)) => Return (INR (INL b))’ >>
+    qexists ‘INR (INR (INL (x' − 1)))’ >>
+    conj_tac
+    >-(pure_once_rewrite_tac [is_valid_fp_body_def] >> fs []) >>
+    fs []) >>
+  Cases_on ‘y’ >> fs [] >>
+  Cases_on ‘y'’ >> fs [] >>
+  Cases_on ‘x = 0’ >> fs []  >>
+  (* Recursive call *)
+  disj2_tac >>
+  qexists ‘\g x. case x of
+                   INL v => Fail Failure
+                 | INR (INL b) => Return (INR (INR (INR b)))
+                 | INR (INR v3) => Fail Failure’ >>
+  qexists ‘INL (x − 1)’ >>
+  conj_tac
+  >-(pure_once_rewrite_tac [is_valid_fp_body_def] >> fs []) >>
+  fs []
+QED
+
+Theorem even_odd_body_is_valid:
+  is_valid_fp_body (SUC (SUC 0)) even_odd_body
+Proof
+  irule even_odd_body_is_valid_aux
+QED
+
+(* We finally introduce the definitions for even and odd *)
+val even_raw_def = Define ‘
+  even (i : int) =
+    case fix even_odd_body (INL i) of
+    | Fail e => Fail e
+    | Diverge => Diverge
+    | Return r =>
+      case r of
+      | INL _ => Fail Failure
+      | INR (INL b) => Return b
+      | INR (INR (INL b)) => Fail Failure
+      | INR (INR (INR _)) => Fail Failure
+’
+
+val odd_raw_def = Define ‘
+  odd (i : int) =
+    case fix even_odd_body (INR (INR (INL i))) of
+    | Fail e => Fail e
+    | Diverge => Diverge
+    | Return r =>
+      case r of
+      | INL _ => Fail Failure
+      | INR (INL _) => Fail Failure
+      | INR (INR (INL _)) => Fail Failure
+      | INR (INR (INR b)) => Return b
+’
+
+Theorem even_def:
+  ∀i. even (i : int) : bool result =
+    if i = 0 then Return T else odd (i - 1)
+Proof
+  gen_tac >>
+  (* Expand the definition *)
+  pure_once_rewrite_tac [even_raw_def] >>
+  (* Use the fixed-point equality *)
+  pure_once_rewrite_left_tac [HO_MATCH_MP fix_fixed_eq even_odd_body_is_valid] >>
+  (* Expand the body definition *)
+  pure_rewrite_tac [even_odd_body_def] >>
+  (* Expand all the definitions from the group *)
+  pure_rewrite_tac [even_raw_def, odd_raw_def] >>
+  (* Explore all the paths - maybe we can be smarter, but this is fast and really easy *)
+  fs [bind_def] >>
+  Cases_on ‘i = 0’ >> fs [] >>
+  Cases_on ‘fix even_odd_body (INR (INR (INL (i − 1))))’ >> fs [] >>
+  Cases_on ‘a’ >> fs [] >>
+  Cases_on ‘y’ >> fs [] >>
+  Cases_on ‘y'’ >> fs []
+QED
+
+Theorem odd_def:
+  ∀i. odd (i : int) : bool result =
+    if i = 0 then Return F else even (i - 1)
+Proof
+  gen_tac >>
+  (* Expand the definition *)
+  pure_once_rewrite_tac [odd_raw_def] >>
+  (* Use the fixed-point equality *)
+  pure_once_rewrite_left_tac [HO_MATCH_MP fix_fixed_eq even_odd_body_is_valid] >>
+  (* Expand the body definition *)
+  pure_rewrite_tac [even_odd_body_def] >>
+  (* Expand all the definitions from the group *)
+  pure_rewrite_tac [even_raw_def, odd_raw_def] >>
+  (* Explore all the paths - maybe we can be smarter, but this is fast and really easy *)
+  fs [bind_def] >>
+  Cases_on ‘i = 0’ >> fs [] >>
+  Cases_on ‘fix even_odd_body (INL (i − 1))’ >> fs [] >>
+  Cases_on ‘a’ >> fs [] >>
+  Cases_on ‘y’ >> fs []
+QED
+
+val _ = export_theory ()
diff --git a/backends/hol4/divDefExampleTheory.sig b/backends/hol4/divDefExampleTheory.sig
new file mode 100644
index 00000000..29e98856
--- /dev/null
+++ b/backends/hol4/divDefExampleTheory.sig
@@ -0,0 +1,188 @@
+signature divDefExampleTheory =
+sig
+  type thm = Thm.thm
+  
+  (*  Definitions  *)
+    val even_odd_body_def : thm
+    val list_t_TY_DEF : thm
+    val list_t_case_def : thm
+    val list_t_size_def : thm
+    val nth_body_def : thm
+  
+  (*  Theorems  *)
+    val datatype_list_t : thm
+    val even_def : thm
+    val even_odd_body_is_valid : thm
+    val even_odd_body_is_valid_aux : 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 nth_body_is_valid : thm
+    val nth_body_is_valid_aux : thm
+    val nth_def : thm
+    val odd_def : thm
+  
+  val divDefExample_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+   [divDef] Parent theory of "divDefExample"
+   
+   [even_odd_body_def]  Definition
+      
+      ⊢ ∀f x.
+          even_odd_body f x =
+          case x of
+            INL 0 => Return (INR (INL T))
+          | INL i =>
+            (case f (INR (INR (INL (i − 1)))) of
+               Return (INL v) => Fail Failure
+             | Return (INR (INL v2)) => Fail Failure
+             | Return (INR (INR (INL v4))) => Fail Failure
+             | Return (INR (INR (INR b))) => Return (INR (INL b))
+             | Fail e => Fail e
+             | Diverge => Diverge)
+          | INR (INL v8) => Fail Failure
+          | INR (INR (INL 0)) => Return (INR (INR (INR F)))
+          | INR (INR (INL i')) =>
+            (case f (INL (i' − 1)) of
+               Return (INL v) => Fail Failure
+             | Return (INR (INL b)) => Return (INR (INR (INR b)))
+             | Return (INR (INR v3)) => Fail Failure
+             | Fail e => Fail e
+             | Diverge => Diverge)
+          | INR (INR (INR v11)) => Fail Failure
+   
+   [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
+   
+   [nth_body_def]  Definition
+      
+      ⊢ ∀f x.
+          nth_body f x =
+          case x of
+            INL x =>
+              (let
+                 (ls,i) = x
+               in
+                 case ls of
+                   ListCons x tl =>
+                     if u32_to_int i = 0 then Return (INR x)
+                     else
+                       do
+                         i0 <- u32_sub i (int_to_u32 1);
+                         x <-
+                           case f (INL (tl,i0)) of
+                             Return (INL v) => Fail Failure
+                           | Return (INR x) => Return x
+                           | Fail e => Fail e
+                           | Diverge => Diverge;
+                         Return (INR x)
+                       od
+                 | ListNil => Fail Failure)
+          | INR v3 => Fail Failure
+   
+   [datatype_list_t]  Theorem
+      
+      ⊢ DATATYPE (list_t ListCons ListNil)
+   
+   [even_def]  Theorem
+      
+      ⊢ ∀i. even i = if i = 0 then Return T else odd (i − 1)
+   
+   [even_odd_body_is_valid]  Theorem
+      
+      ⊢ is_valid_fp_body (SUC (SUC 0)) even_odd_body
+   
+   [even_odd_body_is_valid_aux]  Theorem
+      
+      ⊢ is_valid_fp_body (SUC (SUC n)) even_odd_body
+   
+   [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
+   
+   [nth_body_is_valid]  Theorem
+      
+      ⊢ is_valid_fp_body (SUC (SUC 0)) nth_body
+   
+   [nth_body_is_valid_aux]  Theorem
+      
+      ⊢ is_valid_fp_body (SUC (SUC n)) nth_body
+   
+   [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)
+   
+   
+*)
+end
diff --git a/backends/hol4/divDefLib.sig b/backends/hol4/divDefLib.sig
index d63d7771..51a09b9c 100644
--- a/backends/hol4/divDefLib.sig
+++ b/backends/hol4/divDefLib.sig
@@ -1,93 +1,19 @@
-signature divDefLib =
-sig
-  include Abbrev
-
-  (* Define a (group of mutually recursive) function(s) which uses an error
-     monad and is potentially divergent.
-
-     We encode divergence in such a way that we don't have to prove that the
-     functions we define terminate *upon defining them*, and can do those proofs
-     in an extrinsic way later. It works as follows.
-
-     Let's say you want to define the following “even” and “odd” functions
-     which operate on *integers*:
-
-     {[
-       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)
-     ]}
-
-     It is easy to prove that the functions terminate provided the input is >= 0,
-     but it would require to be able to define those functions in the first place!
-
-     {!DefineDev} consequently does the following.
+(* This library implements an automated method, DefineDiv, which generates
+   definitions by means of the fixed-point operator ‘fix’ introduced in
+   ‘divDefScript’.
 
-     It first defines versions of “even” and “odd” which use fuel:
-     {[
-       even___fuel (n : num) (i : int) : bool result =
-         case n of 0 => Diverge
-         | SUC m => if i = 0 then Return T else odd___fuel m (i - 1) /\
+   For examples of how to use the fixed-point operator step by step on
+   hand-written examples, see divDefExampleTheory.
 
-       odd___fuel (n : num) (i : int) : bool result =
-         case n of 0 => Diverge
-         | SUC m => if i = 0 then Return F else even___fuel m (i - 1)
-     ]}
+   The current file is organized so as to follow the steps detailed in
+   divDefExampleTheory.
 
-     Those functions trivially terminate.
+   For examples of how to use DefiveDiv, see divDefLibExampleScript.
+ *)
 
-     Then, provided we have the following auxiliary definition:
-     {[
-       is_diverge (r: 'a result) : bool = case r of Diverge => T | _ => F
-     ]}
-
-     we can define the following predicates, which tell us whether “even___fuel”
-     and “odd___fuel” terminate on some given inputs:
-     {[
-       even___P i n = ~(is_diverge (even___fuel n i)) /\
-
-       odd___P i n = ~(is_diverge (odd___fuel n i))
-     ]}
-
-     We can finally define “even” and “odd” as follows. We use the excluded
-     middle to test whether there exists some fuel on which the function
-     terminates: if there exists such fuel, we call the "___fuel" versions
-     of “even” and “odd” with it (we use the least upper bound, to be more
-     precise). Otherwise, we simply return “Diverge”.
-     {[
-       even i =
-         if (?n. even___P i n) then even___fuel ($LEAST (even___P i)) i
-         else Diverge /\
-
-       odd i =
-         if (?n. odd___P i n) then odd___fuel ($LEAST (odd___P i)) i
-         else Diverge
-     ]}
-
-     The definitions above happen to satisfy the rewriting theorem we want:
-     {[
-       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)
-     ]}
-
-     Moreover, if we prove a lemma which states that they don't evaluate to
-     “Diverge” on some given inputs (trivial recursion if we take “i >= 0”
-     and reuse the rewriting theorem just above), then we effectively proved
-     that the functions terminate on those inputs.
+signature divDefLib =
+sig
+  include Abbrev
 
-     Remark:
-     =======
-     {!DefineDiv} introduces all the auxiliary definitions we need and
-     automatically performs the proofs. A crucial intermediate lemma
-     we need in order to establish the last theorem is that the "___fuel"
-     versions of the functions are monotonic in the fuel.
-     More precisely:
-     {[
-       !n m. n <= m ==>
-         (!ls i. even___P ls i n ==> even___fuel n ls i n = even___fuel m ls i n) /\
-         (!ls i. odd___P ls i n ==> odd___fuel n ls i n = odd___fuel m ls i n)
-     ]}
-   *)
   val DefineDiv : term quotation -> thm list
 end
diff --git a/backends/hol4/divDefLib.sml b/backends/hol4/divDefLib.sml
index 59c1edaf..3e2d7c04 100644
--- a/backends/hol4/divDefLib.sml
+++ b/backends/hol4/divDefLib.sml
@@ -1,5 +1,3 @@
-(* This file implements utilities to define potentially diverging functions *)
-
 structure divDefLib :> divDefLib =
 struct
 
@@ -8,1196 +6,889 @@ open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
 
 open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
 open primitivesLib
+open divDefTheory
 
-val case_result_same_eq = prove (
-  “!(r : 'a result).
-    (case r of
-       Return x => Return x
-     | Fail e => Fail e
-     | Diverge => Diverge) = r”,
-  rw [] >> CASE_TAC)
-
-(*
-val ty = id_ty
-strip_arrows ty
-*)
+val dbg = ref false
+fun print_dbg s = if (!dbg) then print s else ()
 
-(* 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
+val result_ty = “:'a result”
+val error_ty = “:error”
+val alpha_ty = “:'a”
+val num_ty = “:num”
 
-(* TODO: move *)
-fun strip_arrows (ty : hol_type) : hol_type list * hol_type =
-  let
-    val (ty0, ty1) = dom_rng ty
-    val (tys, ret) = strip_arrows ty1
-  in
-    (ty0::tys, ret)
-  end
-  handle HOL_ERR _ => ([], ty)
+val zero_num_tm = “0:num”
+val suc_tm = “SUC”
 
-(* Small utilities *)
-val current_goal : term option ref = ref NONE
+val return_tm = “Return : 'a -> 'a result”
+val fail_tm = “Fail : error -> 'a result”
+val fail_failure_tm = “Fail Failure : 'a result”
+val diverge_tm = “Diverge : 'a result”
 
-(* Save a goal in {!current_goal} then prove it.
+val fix_tm = “fix”
+val is_valid_fp_body_tm = “is_valid_fp_body”
 
-   This way if the proof fails we can easily retrieve the goal for debugging
-   purposes.
- *)
-fun save_goal_and_prove (g, tac) : thm =
+fun mk_result (ty : hol_type) : hol_type = Type.type_subst [ alpha_ty |-> ty ] result_ty
+fun dest_result (ty : hol_type) : hol_type =
   let
-    val _ = current_goal := SOME g
+    val {Args=out_ty, Thy=thy, Tyop=tyop} = dest_thy_type ty
   in
-    prove (g, tac)
+    if thy = "primitives" andalso tyop = "result" then hd out_ty
+    else failwith "dest_result: not a result"
   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 expand_suffix = "___E" (* TODO: name collisions *)
+fun mk_return (x : term) : term = mk_icomb (return_tm, x)
+fun mk_fail (ty : hol_type) (e : term) : term = mk_comb (inst [ alpha_ty |-> ty ] fail_tm, e)
+fun mk_fail_failure (ty : hol_type) : term = inst [ alpha_ty |-> ty ] fail_failure_tm
+fun mk_diverge (ty : hol_type) : term = inst [ alpha_ty |-> ty ] diverge_tm
 
-val bool_ty = “:bool”
+fun mk_suc (n : term) = mk_comb (suc_tm, n)
 
-val alpha_tyvar : hol_type = “:'a”
-val beta_tyvar : hol_type = “:'b”
-
-val is_diverge_tm = “is_diverge: 'a result -> bool”
-val diverge_tm = “Diverge : 'a result”
+fun enumerate (ls : 'a list) : (int * 'a) list =
+  zip (List.tabulate (List.length ls, fn i => i)) ls
 
-val least_tm = “$LEAST”
-val le_tm = (fst o strip_comb) “x:num <= y:num”
-val true_tm = “T”
-val false_tm = “F”
+(*=============================================================================*
+ *
+ * Generate the (non-recursive) body to give to the fixed-point operator
+ *
+ * ============================================================================*)
 
-val measure_tm = “measure: ('a -> num) -> 'a -> 'a -> bool”
-
-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
+(* Small helper to generate wrappers of the shape: ‘INL x’, ‘INR (INL x)’, etc.
+   Note that we should have: ‘length before_tys + 1 + length after tys >= 2’
 
-(* Small utility: we sometimes need to generate a termination measure for
-   the fuel definitions.
+   Ex.:
+   ====
+   The enumeration has type: “: 'a + 'b + 'c + 'd”.
+   We want to generate the variant which injects “x:'c” into this enumeration.
 
-   We derive a measure for a type which is simply the sum of the tuples
-   of the input types of the functions.
-
-   For instance, for even and odd we have:
+   We need to split the list of types into:
    {[
-     even___fuel : num -> int -> bool result
-     odd___fuel  : num -> int -> bool result
+     before_tys = [“:'a”, “'b”]
+     tm = “x: 'c”
+     after_tys = [“:'d”]
    ]}
 
-   So the type would be:
+   The function will generate:
    {[
-     (num # int) + (num # int)
+     INR (INR (INL x) : 'a + 'b + 'c + 'd
    ]}
 
-   Note that generally speaking we expect a type of the shape (the “:num”
-   on the left is for the fuel):
-   {[
-     (num # ...) + (num # ...) + ... + (num # ...)
-   ]}
+   (* Debug *)
+   val before_tys = [“:'a”, “:'b”, “:'c”]
+   val tm = “x:'d”
+   val after_tys = [“:'e”, “:'f”]
 
-   The decreasing measure is simply given by a function which matches over
-   its argument to return the fuel, whatever the case.
+   val before_tys = [“:'a”, “:'b”, “:'c”]
+   val tm = “x:'d”
+   val after_tys = []
+
+   mk_inl_inr_wrapper before_tys tm after_tys
  *)
-fun mk_termination_measure_from_ty (ty : hol_type) : term =
+fun list_mk_inl_inr (before_tys : hol_type list) (tm : term) (after_tys : hol_type list) :
+  term =
   let
-    val dtys = map pairSyntax.strip_prod (sumSyntax.strip_sum ty)
-    (* For every tuple, create a match to extract the num *)
-    fun mk_case_of_tuple (tys : hol_type list) : (term * term) =
-      case tys of
-        [] => failwith "mk_termination_measure_from_ty: empty list of types"
-      | [num_ty] =>
-        (* No need for a case *)
-        let val var = genvar num_ty in (var, var) end
-      | num_ty :: rem_tys =>
+    val (before_tys, pat) =
+      if after_tys = []
+      then
         let
-          val scrut_var = genvar (pairSyntax.list_mk_prod tys)
-          val var = genvar num_ty
-          val rem_var = genvar (pairSyntax.list_mk_prod rem_tys)
-          val pats = [(pairSyntax.mk_pair (var, rem_var), var)]
-          val case_tm = TypeBase.mk_case (scrut_var, pats)
+          val just_before_ty = List.last before_tys
+          val before_tys = List.take (before_tys, List.length before_tys - 1)
+          val pat = sumSyntax.mk_inr (tm, just_before_ty)
         in
-          (scrut_var, case_tm)
+          (before_tys, pat)
         end
-     val tuple_cases = map mk_case_of_tuple dtys
-
-    (* For every sum, create a match to extract one of the tuples *)
-    fun mk_sum_case ((tuple_var, tuple_case), (nvar, case_end)) =
-      let
-        val left_pat = sumSyntax.mk_inl (tuple_var, type_of nvar)
-        val right_pat = sumSyntax.mk_inr (nvar, type_of tuple_var)
-        val scrut = genvar (sumSyntax.mk_sum (type_of tuple_var, type_of nvar))
-        val pats = [(left_pat, tuple_case), (right_pat, case_end)]
-        val case_tm = TypeBase.mk_case (scrut, pats)
-      in
-        (scrut, case_tm)
-      end
-    val tuple_cases = rev tuple_cases
-    val (nvar, case_end) = hd tuple_cases
-    val tuple_cases = tl tuple_cases
-    val (scrut, case_tm) = foldl mk_sum_case (nvar, case_end) tuple_cases
-
-    (* Create the function *)
-    val abs_tm = mk_abs (scrut, case_tm)
-    
-    (* Add the “measure term” *)
-    val tm = inst [alpha_tyvar |-> type_of scrut] measure_tm
-    val tm = mk_comb (tm, abs_tm)
+      else (before_tys, sumSyntax.mk_inl (tm, sumSyntax.list_mk_sum after_tys))
+    val pat = foldr (fn (ty, pat) => sumSyntax.mk_inr (pat, ty)) pat before_tys
   in
-    tm
+    pat
   end
 
-(*
-val ty = “: (num # 'a) + (num # 'b) + (num # 'c)”
-
-val tys = hd dtys
-val num_ty::rem_tys = tys
-
-val (tuple_var, tuple_case) = hd tuple_cases
-*)
-
-(* Get the smallest id which make the names unique (or to be more precise:
-   such that the names don't correspond to already defined constants).
-
-   We do this for {!mk_fuel_defs}: for some reason, the termination proof
-   fails if we try to reuse the same names as before.
+(* This function wraps a term into the proper variant of the input/output
+   sum.
+
+   Ex.:
+   ====
+   For the input of the first function, we generate: ‘INL x’
+   For the output of the first function, we generate: ‘INR (INL x)’
+   For the input of the 2nd function, we generate: ‘INR (INR (INL x))’
+   etc.
+
+   If ‘is_input’ is true: we are wrapping an input. Otherwise we are wrapping
+   an output.
+
+   (* Debug *)
+   val tys = [(“:'a”, “:'b”), (“:'c”, “:'d”), (“:'e”, “:'f”)]
+   val j = 1
+   val tm = “x:'c”
+   val tm = “y:'d”
+   val is_input = true
  *)
-fun get_smallest_unique_id_for_names (names : string list) : string =
+fun inject_in_param_sum (tys : (hol_type * hol_type) list) (j : int) (is_input : bool)
+  (tm : term) : term =
   let
-    (* Not trying to be smart here *)
-    val i : int option ref = ref NONE
-    fun get_i () = case !i of NONE => "" | SOME i => int_to_string i
-    fun incr_i () =
-      i := (case !i of NONE => SOME 0 | SOME i => SOME (i+1))
-    val continue = ref true
-    fun name_is_ok (name : string) : bool =
-      not (is_const (Parse.parse_in_context [] [QUOTE (name ^ get_i ())]))
-      handle HOL_ERR _ => false
-    val _ =
-      while !continue do (
-        let val _ = (continue := not (forall name_is_ok names)) in
-        if !continue then incr_i () else () end
-      )
+    fun flatten ls = List.concat (map (fn (x, y) => [x, y]) ls)
+    val before_tys = flatten (List.take (tys, j))
+    val (input_ty, output_ty) = List.nth (tys, j)
+    val after_tys = flatten (List.drop (tys, j + 1))
+    val (before_tys, after_tys) =
+      if is_input then (before_tys, output_ty :: after_tys)
+      else (before_tys @ [input_ty], after_tys)
   in
-    get_i ()
+    list_mk_inl_inr before_tys tm after_tys
   end
 
-fun mk_fuel_defs (def_tms : term list) : thm list =
-  let
-    (* Retrieve the identifiers.
+(* Remark: the order of the branches when creating matches is important.
+   For instance, in the case of ‘result’ it must be: ‘Return’, ‘Fail’, ‘Diverge’.
 
-       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 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 fuel' (i - 1))”
-     *)
-     val names = map ((fn s => s ^ fuel_def_suffix) o fst o dest_var) ids
-     val index = get_smallest_unique_id_for_names names
-     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 ^ index
-         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_fuel0 = map (fn id => mk_comb (id, fuel_var0)) fuel_ids
-     val fuel_ids_with_fuel1 = map (fn id => mk_comb (id, fuel_var1)) fuel_ids
-
-     (* Recurse through the terms and replace the calls *)
-     val rwr_thms0 = map (ASSUME o mk_eq) (zip ids fuel_ids_with_fuel0)
-     val rwr_thms1 = map (ASSUME o mk_eq) (zip ids fuel_ids_with_fuel1)
-
-     fun mk_fuel_tm (def_tm : term) : term =
-       let
-         val (tm0, tm1) = dest_eq def_tm
-         val tm0 = (rhs o concl o (PURE_REWRITE_CONV rwr_thms0)) tm0
-         val tm1 = (rhs o concl o (PURE_REWRITE_CONV rwr_thms1)) tm1
-       in mk_eq (tm0, tm1) end
-     val fuel_tms = map mk_fuel_tm def_tms
-
-     (* Add the case over the fuel *)
-     fun add_fuel_case (tm : term) : term =
-       let
-         val (f, 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_var1)
-         val fuel_tm =
-           TypeBase.mk_case (fuel_var0, [(num_zero_tm, diverge_tm), (suc_tm, body)])
-       in mk_eq (f, 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
-     (* The definition name *)
-     val def_name = (fst o dest_var o hd) fuel_ids
-     (* The tactic to prove the termination *)
-     val rty = ref “:bool” (* This is useful for debugging *)
-     fun prove_termination_tac (asms, g) =
-       let
-         val r_tm = (fst o dest_exists) g
-         val _ = rty := type_of r_tm
-         val ty = (hd o snd o dest_type) (!rty)
-         val m_tm = mk_termination_measure_from_ty ty
-       in
-         WF_REL_TAC ‘^m_tm’ (asms, g)
-       end
-
-     (* Define the fuel definitions *)
-     (*
-       val temp_def = Hol_defn def_name ‘^fuel_defs_conj’
-       Defn.tgoal temp_def
-     *)
-     val fuel_defs = tDefine def_name ‘^fuel_defs_conj’ prove_termination_tac
-   in
-     CONJUNCTS fuel_defs
-   end
-
-(*
-val (fuel_tms, fuel_defs) = mk_fuel_defs def_tms
-val fuel_def_tms = map (snd o strip_forall) ((strip_conj o concl) fuel_defs)
-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 =
+   For the purpose of stability and maintainability, we introduce this small helper
+   which reorders the cases in a pattern before actually creating the case
+   expression.
+ *)
+fun unordered_mk_case (scrut: term, pats: (term * term) list) : term =
   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 (tys, ret_ty) = strip_arrows id_ty
-    val tys = append tys [num_ty]
-    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)
+    (* Retrieve the constructors *)
+    val cl = TypeBase.constructors_of (type_of scrut)
+    (* Retrieve the names of the constructors *)
+    val names = map (fst o dest_const) cl
+    (* Use those to reorder the patterns *)
+    fun is_pat (name : string) (pat, _) =
+      let
+        val app = (fst o strip_comb) pat
+        val app_name = (fst o dest_const) app
+      in
+        app_name = name
+      end
+    val pats = map (fn name => valOf (List.find (is_pat name) pats)) names
   in
-    (* Create the definition *)
-    Define ‘^pred_def_tm’
+    (* Create the case *)
+    TypeBase.mk_case (scrut, pats)
   end
 
-(*
-val (def_tm, fuel_def_tm) = hd (zip def_tms fuel_def_tms)
-
-val pred_defs = map mk_fuel_predicate_defs (zip def_tms fuel_def_tms)
-*)
+(* Wrap a term of type “:'a result” into a ‘case of’ which matches over
+   the result.
 
-(* 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  
+   Ex.:
+   ====
+   {[
+     f x
 
-(* 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)
+     case f x of
+     | Fail e => Fail e
+     | Diverge => Diverge
+     | Return y => ... (* The branch content is generated by the continuation *)
    ]}
-*)
-fun prove_fuel_mono (pred_defs : thm list) (fuel_defs : thm list) : thm =
-  let
-    val pred_tms = map (lhs o snd o strip_forall o concl) pred_defs
-    val fuel_tms = map (lhs o snd o strip_forall o concl) fuel_defs
-    val pred_fuel_tms = zip pred_tms fuel_tms
-    (* Create a set containing the names of all the functions in the recursive group *)
-    val rec_fun_set =
-      Redblackset.fromList const_name_compare (map get_fun_name_from_app fuel_tms)
-    (* Small tactic which rewrites the occurrences of 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
-             (* Yes: use the induction hypothesis *)
-             fun apply_ind_hyp (ind_th : thm) : tactic =
-               let
-                  val th = SPEC_ALL ind_th
-                  val th_pat = (lhs o snd o strip_imp o concl) th
-                  val (var_s, ty_s) = match_term th_pat scrut
-                  (* Note that in practice the type instantiation should be empty *)
-                  val th = INST var_s (INST_TYPE ty_s th)
-               in
-                 assume_tac th
-               end
-          in
-            (last_assum apply_ind_hyp >> fs []) (asms, g)
-          end
-        else all_tac (asms, g)
-      end
-      handle HOL_ERR _ => all_tac (asms, g)
-    (* 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
-     (* Qantify over the fuels *)
-     val fuel_eq_tms = list_mk_forall ([fuel_var0, fuel_var1], fuel_eq_tms)
-     (* The tactics for the proof *)
-     val prove_tac =
-       Induct_on ‘^fuel_var0’ >-(
-         (* The ___P predicates are false: n is 0 *)
-         fs pred_defs >>
-         fs [is_diverge_def] >>
-         pure_once_rewrite_tac fuel_defs >> fs []) >>
-       (* Introduce n *)
-       gen_tac >>
-       (* Introduce m *)
-       Cases_on ‘^fuel_var1’ >-(
-         (* Contradiction: SUC n < 0 *)
-         rw [] >> exfalso >> int_tac) >>
-       fs pred_defs >>
-       fs [is_diverge_def] >>
-       pure_once_rewrite_tac fuel_defs >> fs [bind_def] >>
-       (* Introduce in the context *)
-       rpt gen_tac >>
-       (* Split the goals - note that we prove one big goal for all the functions at once *)
-       rpt strip_tac >>
-       (* Instantiate the assumption: !m. n <= m ==> ~(...)
-          with the proper m.
-        *)
-       last_x_assum imp_res_tac >>
-       (* Make sure the induction hypothesis is always the last assumption *)
-       last_x_assum assume_tac >>
-       (* Split the goals *)
-       rpt strip_tac >> fs [case_result_same_eq] >>
-       (* Explore all the paths *)
-       rpt (rewrite_rec_call >> case_progress >> fs [case_result_same_eq])
-   in
-     (* Prove *)
-     save_goal_and_prove (fuel_eq_tms, prove_tac)
-   end
 
-(*
-val fuel_mono_thm = prove_fuel_mono pred_defs fuel_defs
+   ‘gen_ret_branch’ is a *continuation* which generates the content of the
+   ‘Return’ branch (i.e., the content of the ‘...’ in the example above).
+   It receives as input the value contained by the ‘Return’ (i.e., the variable
+   ‘y’ in the example above).
 
-set_goal ([], fuel_eq_tms)
-*)
+   Remark.: the type of the term generated by ‘gen_ret_branch’ must have
+   the type ‘result’, but it can change the content of the result (i.e.,
+   if ‘scrut’ has type ‘:'a result’, we can change the type of the wrapped
+   expression to ‘:'b result’).
 
-(* Prove the property about the least upper bound.
+   (* Debug *)
+   val scrut = “x: int result”
+   fun gen_ret_branch x = mk_return x
 
-   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)
-   ]}
+   val scrut = “x: int result”
+   fun gen_ret_branch _ = “Return T”
 
-   TODO: merge with other functions? (prove_pred_imp_fuel_eq_raw_thms)
-*)
-fun prove_least_fuel_mono (pred_defs : thm list) (fuel_mono_thm : thm) : thm list =
+   mk_result_case scrut gen_ret_branch
+ *)
+fun mk_result_case (scrut : term) (gen_ret_branch : term -> term) : term =
   let
-    val thl = (CONJUNCTS o SPECL [fuel_var0, fuel_var1]) fuel_mono_thm
-    fun mk_least_fuel_thm (pred_def, mono_thm) : thm =
-      let
-        (* Retrieve the predicate, without the fuel *)
-        val pred_tm = (lhs o snd o strip_forall o concl) pred_def
-        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
+    val scrut_ty = dest_result (type_of scrut)
+    (* Return branch *)
+    val ret_var = genvar scrut_ty
+    val ret_pat = mk_return ret_var
+    val ret_br = gen_ret_branch ret_var
+    val ret_ty = dest_result (type_of ret_br)
+    (* Failure branch *)
+    val fail_var = genvar error_ty
+    val fail_pat = mk_fail scrut_ty fail_var
+    val fail_br = mk_fail ret_ty fail_var
+    (* Diverge branch *)
+    val div_pat = mk_diverge scrut_ty
+    val div_br = mk_diverge ret_ty
   in
-    map mk_least_fuel_thm (zip pred_defs thl)
+    unordered_mk_case (scrut, [(ret_pat, ret_br), (fail_pat, fail_br), (div_pat, div_br)])
   end
 
-(*
-val (pred_def, mono_thm) = hd (zip pred_defs thl)
-*)
+(* Generate a ‘case ... of’ over a sum type.
 
-(* Prove theorems of the shape:
+   Ex.:
+   ====
+   If the scrutinee is: “x : 'a + 'b + 'c” (i.e., the tys list is: [“:'a”, “:b”, “:c”]),
+   we generate:
 
    {[
-     !n i. even___P i n ==> $LEAST (even___P i) <= n
+     case x of
+     | INL y0 => ... (* Branch of index 0 *)
+     | INR (INL y1) => ... (* Branch of index 1 *)
+     | INR (INR (INL y2)) => ... (* Branch of index 2 *)
+     | INR (INR (INR y3)) => ... (* Branch of index 3 *)
    ]}
 
-   TODO: merge with other functions? (prove_pred_imp_fuel_eq_raw_thms)
+   The content of the branches is generated by the ‘gen_branch’ continuation,
+   which receives as input the index of the branch as well as the variable
+   introduced by the pattern (in the example above: ‘y0’ for the branch 0,
+   ‘y1’ for the branch 1, etc.)
+
+   (* Debug *)
+   val tys = [“:'a”, “:'b”]
+   val scrut = mk_var ("x", sumSyntax.list_mk_sum tys)
+   fun gen_branch i (x : term) = “F”
+
+   val tys = [“:'a”, “:'b”, “:'c”, “:'d”]
+   val scrut = mk_var ("x", sumSyntax.list_mk_sum tys)
+   fun gen_branch i (x : term) = if type_of x = “:'c” then mk_return x else mk_fail_failure “:'c”
+
+   list_mk_sum_case scrut tys gen_branch
  *)
-fun prove_least_pred_thms (pred_defs : thm list) : thm list =
+(* For debugging *)
+val list_mk_sum_case_case = ref (“T”, [] : (term * term) list)
+(*
+val (scrut, [(pat1, br1), (pat2, br2)]) = !list_mk_sum_case_case
+*)
+fun list_mk_sum_case (scrut : term) (tys : hol_type list)
+  (gen_branch : int -> term -> term) : term =
   let
-    fun prove_least_pred_thm (pred_def : thm) : thm =
+    (* Create the cases. Note that without sugar, the match actually looks like this:
+       {[
+         case x of
+         | INL y0 => ... (* Branch of index 0 *)
+         | INR x1
+           case x1 of
+           | INL y1 => ... (* Branch of index 1 *)
+           | INR x2 =>
+             case x2 of
+             | INL y2 => ... (* Branch of index 2 *)
+             | INR y3 => ... (* Branch of index 3 *)
+       ]}
+     *)
+    fun create_case (j : int) (scrut : term) (tys : hol_type list) : term =
       let
-        val pred_tm = (lhs o snd o strip_forall o concl) pred_def
-        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]
+        val _ = print_dbg ("list_mk_sum_case: " ^
+                           String.concatWith ", " (map type_to_string tys) ^ "\n")
       in
-        save_goal_and_prove (tm, prove_tac)
+        case tys of
+          [] => failwith "tys is too short"
+        | [ ty ] =>
+          (* Last element: no match to perform *)
+          gen_branch j scrut
+        | ty1 :: tys =>
+          (* Not last: we create a pattern:
+             {[
+               case scrut of
+               | INL pat_var1 => ... (* Branch of index i *)
+               | INR pat_var2 =>
+                 ... (* Generate this term recursively *)
+             ]}
+           *)
+          let
+            (* INL branch *)
+            val after_ty = sumSyntax.list_mk_sum tys
+            val pat_var1 = genvar ty1
+            val pat1 = sumSyntax.mk_inl (pat_var1, after_ty)
+            val br1 = gen_branch j pat_var1
+            (* INR branch *)
+            val pat_var2 = genvar after_ty
+            val pat2 = sumSyntax.mk_inr (pat_var2, ty1)
+            val br2 = create_case (j+1) pat_var2 tys
+            val _ = print_dbg ("list_mk_sum_case: assembling:\n" ^
+                               term_to_string scrut ^ ",\n" ^
+                               "[(" ^ term_to_string pat1 ^ ",\n  " ^ term_to_string br1 ^ "),\n\n" ^
+                               " (" ^ term_to_string pat2 ^ ",\n  " ^ term_to_string br2 ^ ")]\n\n")
+            val case_elems = (scrut, [(pat1, br1), (pat2, br2)])
+            val _ = list_mk_sum_case_case := case_elems
+          in
+            (* Put everything together *)
+            TypeBase.mk_case case_elems
+          end
       end
   in
-    map prove_least_pred_thm pred_defs
+    create_case 0 scrut tys
   end
 
+(* Generate a ‘case ... of’ to select the input/output of the ith variant of
+   the param enumeration.
 
-(*
-val least_pred_thms = prove_least_pred_thms pred_defs
-
-val least_pred_thm = hd least_pred_thms
-*)
-
-(* Prove theorems of the shape:
-
+   Ex.:
+   ====
+   There are two functions in the group, and we select the input of the function of index 1:
    {[
-     !n i. even___P i n ==> even___P i ($LEAST (even___P i))
+     case x of
+     | INL _ => Fail Failure              (* Input of function of index 0 *)
+     | INR (INL _) => Fail Failure        (* Output of function of index 0 *)
+     | INR (INR (INL y)) => Return y      (* Input of the function of index 1: select this one *)
+     | INR (INR (INR _)) => Fail Failure  (* Output of the function of index 1 *)
    ]}
-*)
-fun prove_pred_n_imp_pred_least_thms (pred_defs : thm list) : thm list =
-  let
-    fun prove_pred_n_imp_pred_least (pred_def : thm) : thm =
-      let
-        val pred_tm = (lhs o snd o strip_forall o concl) pred_def
-        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_defs
-  end
 
-(*
-val (pred_def, mono_thm) = hd (zip pred_defs thl)
-val least_fuel_mono_thms = prove_least_fuel_mono pred_defs fuel_defs fuel_mono_thm
+   (* Debug *)
+   val tys = [(“:'a”, “:'b”)]
+   val scrut = “x : 'a + 'b”
+   val fi = 0
+   val is_input = true
 
-val least_fuel_mono_thm = hd least_fuel_mono_thms
-*)
+   val tys = [(“:'a”, “:'b”), (“:'c”, “:'d”)]
+   val scrut = “x : 'a + 'b + 'c + 'd”
+   val fi = 1
+   val is_input = false
 
-(* Define the "raw" definitions:
+   val scrut = mk_var ("x", sumSyntax.list_mk_sum (flatten tys))
 
-   {[
-     even i = if (?n. even___P i n) then even___P ($LEAST (even___P i)) i else Diverge
-   ]}
+   list_mk_case_select scrut tys fi is_input
  *)
-fun define_raw_defs (def_tms : term list) (pred_defs : thm list) (fuel_defs : thm list) : thm list =
+fun list_mk_case_sum_select (scrut : term) (tys : (hol_type * hol_type) list)
+  (fi : int) (is_input : bool) : term =
   let
-    fun define_raw_def (def_tm, (pred_def, fuel_def)) : thm =
-      let
-        val app = lhs def_tm
-        val pred_tm = (lhs o snd o strip_forall o concl) pred_def
-        (* 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
-        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
+    (* The index of the element in the enumeration that we will select *)
+    val i = 2 * fi + (if is_input then 0 else 1)
+    (* Flatten the types and numerotate them *)
+    fun flatten ls = List.concat (map (fn (x, y) => [x, y]) ls)
+    val tys = flatten tys
+    (* Get the return type *)
+    val ret_ty = List.nth (tys, i)
+    (* The continuation which will generate the content of the branches *)
+    fun gen_branch j var = if j = i then mk_return var else mk_fail_failure ret_ty
   in
-    map define_raw_def (zip def_tms (zip pred_defs fuel_defs))
+    (* Generate the ‘case ... of’ *)
+    list_mk_sum_case scrut tys gen_branch
   end
 
-(*
-val raw_defs = define_raw_defs def_tms pred_defs fuel_defs
+(* Generate a ‘case ... of’ to select the input/output of the ith variant of
+   the param enumeration.
+
+   Ex.:
+   ====
+   There are two functions in the group, and we select the input of the function of index 1:
+   {[
+     case x of
+     | Fail e => Fail e
+     | Diverge => Diverge
+     | Return r =>
+       case r of
+       | INL _ => Fail Failure              (* Input of function of index 0 *)
+       | INR (INL _) => Fail Failure        (* Output of function of index 0 *)
+       | INR (INR (INL y)) => Return y      (* Input of the function of index 1: select this one *)
+       | INR (INR (INR _)) => Fail Failure  (* Output of the function of index 1 *)
+   ]}
  *)
+fun mk_case_select_result_sum (scrut : term) (tys : (hol_type * hol_type) list)
+  (fi : int) (is_input : bool) : term =
+  (* We match over the result, then over the enumeration *)
+  mk_result_case scrut (fn x => list_mk_case_sum_select x tys fi is_input)
 
-(* Prove theorems of the shape:
+(* Generate a body for the fixed-point operator from a quoted group of mutually
+   recursive definitions.
 
-   !n i. even___P i n ==> even___fuel n i = even i
+   See TODO for detailed explanations: from the quoted equations for ‘nth’
+   (or for [‘even’, ‘odd’]) we generate the body ‘nth_body’ (or ‘even_odd_body’,
+   respectively).
  *)
-fun prove_pred_imp_fuel_eq_raw_defs
-  (pred_defs : 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_defs : thm list) :
-  thm list =
+fun mk_body (fnames : string list) (in_out_tys : (hol_type * hol_type) list)
+  (def_tms : term list) : term =
   let
-    fun prove_thm (pred_def,
-                   (fuel_def_tm,
-                    (least_fuel_mono_thm,
-                     (least_pred_thm,
-                      (pred_n_imp_pred_least_thm, raw_def))))) : thm =
-      let
-        (* Generate: “even___P i n” *)
-        val pred_tm = (lhs o snd o strip_forall o concl) pred_def
-        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
-        (* 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_defs >>
-          (* 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_defs (zip fuel_def_tms (zip least_fuel_mono_thms
-                   (zip least_pred_thms (zip pred_n_imp_pred_least_thms raw_defs)))))
-  end
+    val fnames_set = Redblackset.fromList String.compare fnames
+
+    (* Compute a map from function name to function index *)
+    val fnames_map = Redblackmap.fromList String.compare
+      (map (fn (x, y) => (y, x)) (enumerate fnames))
+
+    (* Compute the input/output type, that we dub the "parameter type" *)
+    fun flatten ls = List.concat (map (fn (x, y) => [x, y]) ls)
+    val param_type = sumSyntax.list_mk_sum (flatten in_out_tys)
+
+    (* Introduce a variable for the confinuation *)
+    val fcont = genvar (param_type --> mk_result param_type)
+
+    (* In the function equations, replace all the recursive calls with calls to the continuation.
+
+       When replacing a recursive call, we have to do two things:
+       - we need to inject the input parameters into the parameter type
+         Ex.:
+         - ‘nth tl i’ becomes ‘f (INL (tl, i))’ where ‘f’ is the continuation
+         - ‘even i’ becomes ‘f (INL i)’ where ‘f’ is the continuation
+       - we need to wrap the the call to the continuation into a ‘case ... of’
+         to extract its output (we need to make sure that the transformation
+         preserves the type of the expression!)
+         Ex.: ‘nth tl i’ becomes:
+         {[
+           case f (INL (tl, i)) of
+           | Fail e => Fail e
+           | Diverge => Diverge
+           | Return r =>
+             case r of
+             | INL _ => Fail Failure
+             | INR x => Return (INR x)
+         ]}
+     *)
+     (* For debugging *)
+     val replace_rec_calls_rec_call_tm = ref “T”
+     fun replace_rec_calls (fnames_set : string Redblackset.set) (tm : term) : term =
+       let
+         val _ = print_dbg ("replace_rec_calls: original expression:\n" ^
+                            term_to_string tm ^ "\n\n")
+         val ntm =
+           case dest_term tm of
+             VAR (name, ty) =>
+             (* Check that this is not one of the functions in the group - remark:
+                we could handle that by introducing lambdas.
+              *)
+             if Redblackset.member (fnames_set, name)
+             then failwith ("mk_body: not well-formed definition: found " ^ name ^
+                            " in an improper position")
+             else tm
+           | CONST _ => tm
+           | LAMB (x, tm) =>
+             let
+               (* The variable might shadow one of the functions *)
+               val fnames_set = Redblackset.delete (fnames_set, (fst o dest_var) x)
+               (* Update the term in the lambda *)
+               val tm = replace_rec_calls fnames_set tm
+             in
+               (* Reconstruct *)
+               mk_abs (x, tm)
+             end
+           | COMB (_, _) =>
+             let
+               (* Completely destruct the application, check if this is a recursive call *)
+               val (app, args) = strip_comb tm
+               val is_rec_call = Redblackset.member (fnames_set, (fst o dest_var) app)
+                 handle HOL_ERR _ => false
+               (* Whatever the case, apply the transformation to all the inputs *)
+               val args = map (replace_rec_calls fnames_set) args
+             in
+               (* If this is not a recursive call: apply the transformation to all the
+                  terms. Otherwise, replace. *)
+               if not is_rec_call then list_mk_comb (replace_rec_calls fnames_set app, args)
+               else
+                 (* Rec call: replace *)
+                 let
+                   val _ = replace_rec_calls_rec_call_tm := tm
+                   (* First, find the index of the function *)
+                   val fname = (fst o dest_var) app
+                   val fi = Redblackmap.find (fnames_map, fname)
+                   (* Inject the input values into the param type *)
+                   val input = pairSyntax.list_mk_pair args
+                   val input = inject_in_param_sum in_out_tys fi true input
+                   (* Create the recursive call *)
+                   val call = mk_comb (fcont, input)
+                   (* Wrap the call into a ‘case ... of’ to extract the output *)
+                   val call = mk_case_select_result_sum call in_out_tys fi false
+                 in
+                   (* Return *)
+                   call
+                 end
+             end
+         val _ = print_dbg ("replace_rec_calls: new expression:\n" ^ term_to_string ntm ^ "\n\n")
+       in
+         ntm
+       end
+       handle HOL_ERR e =>
+         let
+           val _ = print_dbg ("replace_rec_calls: failed on:\n" ^ term_to_string tm ^ "\n\n")
+         in
+           raise (HOL_ERR e)
+         end
+     fun replace_rec_calls_in_eq (eq : term) : term =
+       let
+         val (l, r) = dest_eq eq
+       in
+         mk_eq (l, replace_rec_calls fnames_set r)
+       end
+     val def_tms_with_fcont = map replace_rec_calls_in_eq def_tms
 
-(*
-val pred_imp_fuel_eq_raw_defs =
-  prove_pred_imp_fuel_eq_raw_defs
-    pred_defs fuel_def_tms least_fuel_mono_thms least_pred_thms
-    pred_n_imp_pred_least_thms raw_defs
- *)
+     (* Wrap all the function bodies to inject their result into the param type.
 
+        We collect the function inputs at the same time, because they will be
+        grouped into a tuple that we will have to deconstruct.
+      *)
+     fun inject_body_to_enums (i : int, def_eq : term) : term list * term =
+       let
+         val (l, body) = dest_eq def_eq
+         val (_, args) = strip_comb l
+         (* We have the deconstruct the result, then, in the ‘Return’ branch,
+            properly wrap the returned value *)
+         val body = mk_result_case body (fn x => mk_return (inject_in_param_sum in_out_tys i false x))
+       in
+         (args, body)
+       end
+     val def_tms_inject = map inject_body_to_enums (enumerate def_tms_with_fcont)
 
-(* Generate "expand" definitions of the following shape (we use them to
-   hide the raw function bodies, to control the rewritings):
+     (* Currify the body inputs.
 
-   {[
-     even___expand even odd i : bool result =
-       if i = 0 then Return T else odd (i - 1)
-   ]}
+        For instance, if the body has inputs: ‘x’, ‘y’; we return the following:
+        {[
+          (‘z’, ‘case z of (x, y) => ... (* body *) ’)
+        ]}
+        where ‘z’ is fresh.
 
-   {[
-     odd___expand even odd i : bool result =
-       if i = 0 then Return F else even (i - 1)
-   ]}
+        We return: (curried input, body).
 
- *)
-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
+        (* Debug *)
+        val body = “(x:'a, y:'b, z:'c)”
+        val args = [“x:'a”, “y:'b”, “z:'c”]
+        currify_body_inputs (args, body)
+      *)
+     fun currify_body_inputs (args : term list, body : term) : term * term =
+       let
+         fun mk_curry (args : term list) (body : term) : term * term =
+           case args of
+             [] => failwith "no inputs"
+           | [x] => (x, body)
+           | x1 :: args =>
+             let
+               val (x2, body) = mk_curry args body
+               val scrut = genvar (pairSyntax.list_mk_prod (map type_of (x1 :: args)))
+               val pat = pairSyntax.mk_pair (x1, x2)
+               val br = body
+             in
+               (scrut, TypeBase.mk_case (scrut, [(pat, br)]))
+             end
+       in
+         mk_curry args body
+       end
+     val def_tms_currified = map currify_body_inputs def_tms_inject
+
+     (* Group all the functions into a single body, with an outer ‘case .. of’
+        which selects the appropriate body depending on the input *)
+     val param_ty = sumSyntax.list_mk_sum (flatten in_out_tys)
+     val input = genvar param_ty
+     fun mk_mut_rec_body_branch (i : int) (patvar : term) : term =
+       (* Case disjunction on whether the branch is for an input value (in
+          which case we call the proper body) or an output value (in which
+          case we return ‘Fail ...’ *)
+       if i mod 2 = 0 then
+         let
+           val fi = i div 2
+           val (x, def_tm) = List.nth (def_tms_currified, fi)
+           (* The variable in the pattern and the variable expected by the
+              body may not be the same: we introduce a let binding *)
+           val def_tm = mk_let (mk_abs (x, def_tm), patvar)
+         in
+           def_tm
+         end
+       else
+         (* Output value: fail *)
+         mk_fail_failure param_ty
+     val mut_rec_body = list_mk_sum_case input (flatten in_out_tys) mk_mut_rec_body_branch
+
+
+     (* Abstract away the parameters to produce the final body of the fixed point *)
+     val mut_rec_body = list_mk_abs ([fcont, input], mut_rec_body)
   in
-    map mk_def def_tms
+    mut_rec_body
   end
 
-(*
-val def_tm = hd def_tms
+(*=============================================================================*
+ *
+ * Prove that the body satisfies the validity condition
+ *
+ * ============================================================================*)
 
-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
-  (def_tms : term list)
-  (pred_defs : thm list)
-  (raw_defs : thm list)
-  (expand_defs : thm list) :
-  (term * term) list =
+(* Tactic to prove that a body is valid: perform one step. *)
+fun prove_body_is_valid_tac_step (asms, g) =
   let
-    (* Create the substitution for the "expand" functions:
+    (* The goal has the shape:
        {[
-         even -> even
-         odd -> odd
-         ...
-       ]}
-
-       where on the left we have *variables* and on the right we have
-       the "raw" definitions.
+         (∀g h. ... g x = ... h x) ∨
+         ∃h y. is_valid_fp_body n h ∧ ∀g. ... g x = ... od
+       ]}   
+     *)
+    (* Retrieve the scrutinee in the goal (‘x’).
+       There are two cases:
+       - either the function has the shape:
+         {[
+           (λ(y,z). ...) x
+         ]}
+         in which case we need to destruct ‘x’
+       - or we have a normal ‘case ... of’
      *)
-    fun mk_fun_subst (def_tm, raw_def) =
+    val body = (lhs o snd o strip_forall o fst o dest_disj) g
+    val scrut =
       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
+        val (app, x) = dest_comb body
+        val (app, _) = dest_comb app
+        val {Name=name, Thy=thy, Ty = _ } = dest_thy_const app
       in
-        (var |-> f)
+        if thy = "pair" andalso name = "UNCURRY" then x else failwith "not a curried argument"
       end
-    val fun_subst = map mk_fun_subst (zip def_tms raw_defs)
-  
-    fun mk_tm (pred_def, (raw_def, expand_def)) :
-      term * term =
+      handle HOL_ERR _ => strip_all_cases_get_scrutinee body
+    (* Retrieve the first quantified continuations from the goal (‘g’) *)
+    val qc = (hd o fst o strip_forall o fst o dest_disj) g
+    (* Check if the scrutinee is a recursive call *)
+    val (scrut_app, _) = strip_comb scrut
+    val _ = print_dbg ("prove_body_is_valid_step: Scrutinee: " ^ term_to_string scrut ^ "\n")
+    (* For the recursive calls: *)
+    fun step_rec () =
       let
-        (* “even___P i n” *)
-        val pred_tm = (lhs o snd o strip_forall o concl) pred_def
-        (* “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
-        val fun_eq_tm = mk_eq (fun_tm, expand_tm)
-      in (pred_tm, fun_eq_tm) end
+        val _ = print_dbg ("prove_body_is_valid_step: rec call\n")
+        (* We need to instantiate the ‘h’ existantially quantified function *)
+        (* First, retrieve the body of the function: it is given by the ‘Return’ branch *)
+        val (_, _, branches) = TypeBase.dest_case body
+        (* Find the branch corresponding to the return *)
+        val ret_branch = List.find (fn (pat, _) =>
+          let
+            val {Name=name, Thy=thy, Ty = _ } = (dest_thy_const o fst o strip_comb) pat
+          in
+            thy = "primitives" andalso name = "Return"
+          end) branches
+        val var = (hd o snd o strip_comb o fst o valOf) ret_branch
+        val br = (snd o valOf) ret_branch
+        (* Abstract away the input variable introduced by the pattern and the continuation ‘g’ *)
+        val h = list_mk_abs ([qc, var], br)
+        val _ = print_dbg ("prove_body_is_valid_step: h: " ^ term_to_string h ^ "\n")
+        (* Retrieve the input parameter ‘x’ *)
+        val input = (snd o dest_comb) scrut
+        val _ = print_dbg ("prove_body_is_valid_step: y: " ^ term_to_string input ^ "\n")
+      in
+        ((* Choose the right possibility (this is a recursive call) *)
+         disj2_tac >>
+         (* Instantiate the quantifiers *)
+         qexists ‘^h’ >>
+         qexists ‘^input’ >>
+         (* Unfold the predicate once *)
+         pure_once_rewrite_tac [is_valid_fp_body_def] >>
+         (* We have two subgoals:
+            - 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])
+      end
   in
-    map mk_tm (zip pred_defs (zip raw_defs expand_defs))
+    (* If recursive call: special treatment. Otherwise, we do a simple disjunction *)
+    (if term_eq scrut_app qc then step_rec ()
+     else (Cases_on ‘^scrut’ >> fs [case_result_switch_eq])) (asms, g)
   end
 
-(*
-val term_div_tms =
-  mk_termination_diverge_tms pred_defs raw_defs expand_defs
-*)
+(* Tactic to prove that a body is valid *)
+fun prove_body_is_valid_tac (body_def : thm option) : tactic =
+  let val body_def_thm = case body_def of SOME th => [th] | NONE => []
+  in
+    pure_once_rewrite_tac [is_valid_fp_body_def] >> gen_tac >>
+    (* Expand *)
+    fs body_def_thm >>
+    fs [bind_def, case_result_switch_eq] >>
+    (* Explore the body *)
+    rpt prove_body_is_valid_tac_step
+  end
 
-(* 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 list)
-  (pred_defs : thm list)
-  (raw_defs : thm list)
-  (expand_defs : thm list)
-  (pred_n_imp_pred_least_thms : thm list)
-  (pred_imp_fuel_eq_raw_defs : thm list)
-  : thm list =
+(* Prove that a body satisfies the validity condition of the fixed point *)
+fun prove_body_is_valid (body : term) : thm =
   let
-    (* Create a map from functions in the recursive group to lemmas
-       to apply *)
-    fun mk_rec_fun_eq_pair (fuel_def, eq_th) =
-      let
-        val rfun = (get_fun_name_from_app o lhs o snd o strip_forall o concl) fuel_def
-      in
-        (rfun, eq_th)
-      end
-    val rec_fun_eq_map =
-      Redblackmap.fromList const_name_compare (
-        map mk_rec_fun_eq_pair
-          (zip fuel_defs pred_imp_fuel_eq_raw_defs))
-
-    (* 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_defs >> 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 (lhs fun_eq_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_defs >>
-          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_defs >>
-          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 >>
-          rpt disch_tac >>
+    (* 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’.
+
+       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).
+     *)
+    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)
+      | LAMB (_, x) => count_body_rec_calls x
+    val num_rec_calls = count_body_rec_calls body
+
+    (* Generate the term ‘SUC (SUC ... (SUC n))’ where ‘n’ is a fresh variable.
+
+       Remark: we first prove ‘is_valid_fp_body (SUC ... n) body’ then substitue
+       ‘n’ with ‘0’ to prevent the quantity from being rewritten to a bit
+       representation, which would prevent unfolding of the ‘is_valid_fp_body’.
+     *)
+    val nvar = genvar num_ty
+    (* Rem.: we stack num_rec_calls + 1 occurrences of ‘SUC’ (and the + 1 is important) *)
+    fun mk_n i = if i = 0 then mk_suc nvar else mk_suc (mk_n (i-1))
+    val n_tm = mk_n num_rec_calls
 
-          (* Expand the binds *)
-          fs [bind_def, case_result_same_eq] >>
+    (* 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)
 
-          (* Explore all the paths by doing case disjunctions *)
-          rpt (rewrite_rec_call >> case_progress >> fs [case_result_same_eq])
-      in
-        save_goal_and_prove (tm, prove_tac)
-      end
+    (* Replace ‘nvar’ with ‘0’ *)
+    val is_valid_thm = INST [nvar |-> zero_num_tm] is_valid_thm
   in
-    map prove_one
-      (zip term_div_tms pred_n_imp_pred_least_thms)
+    is_valid_thm
   end
 
-(*
-val termination_thms =
-  prove_termination_thms term_div_tms fuel_defs pred_defs
-    raw_defs expand_defs pred_n_imp_pred_least_thms
-    pred_imp_fuel_eq_raw_defs
-
-val ((pred_tm, fun_eq_tm), pred_n_imp_pred_least_thm) = hd (zip term_div_tms pred_n_imp_pred_least_thms)
-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
-   ]}
+(*=============================================================================*
+ *
+ * Generate the definitions with the fixed-point operator
+ *
+ * ============================================================================*)
 
-   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 list)
-  (pred_defs : thm list)
-  (raw_defs : thm list)
-  (expand_defs : thm list)
-  : thm list =
+(* Generate the raw definitions by using the grouped definition body and the
+   fixed point operator *)
+fun mk_raw_defs (in_out_tys : (hol_type * hol_type) list)
+  (def_tms : term list) (body_is_valid : thm) : 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) =
-     (get_fun_name_from_app o lhs o snd o strip_forall o concl) fuel_def
-    val rec_fun_set =
-      Redblackset.fromList const_name_compare (
-        map get_rec_fun_id raw_defs)
-
-    (* 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_defs scrut)
-            val (_, exists_g, _) = TypeBase.dest_case exists_g
-            (* The tactic to prove the subgoal *)
-            val prove_sg_tac =
-              pure_rewrite_tac raw_defs >>
-              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_defs >> 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
+    (* Retrieve the body *)
+    val body = (List.last o snd o strip_comb o concl) body_is_valid
 
-        (* Add the implications *)
-        val tm = list_mk_imp ([pred_tm, pred_suc_tm], tm)
+    (* Create the term ‘fix body’ *)
+    val fixed_body = mk_icomb (fix_tm, body)
 
-        (* Quantify *)
-        val (_, args) = strip_comb (lhs fun_eq_tm)
-        val tm = list_mk_forall (args, tm)
+    (* For every function in the group, generate the equation that we will
+       use as definition. In particular:
+       - add the properly injected input ‘x’ to ‘fix body’ (ex.: for ‘nth ls i’
+         we add the input ‘INL (ls, i)’)
+       - wrap ‘fix body x’ into a case disjunction to extract the relevant output
 
-        (* Prove *)
-        val prove_tac =
-          rpt gen_tac >>
-
-          pure_rewrite_tac raw_defs >>
-          rpt disch_tac >>
+       For instance, in the case of ‘nth ls i’:
+       {[
+         nth (ls : 't list_t) (i : u32) =
+           case fix nth_body (INL (ls, i)) of
+           | Fail e => Fail e
+           | Diverge => Diverge
+           | Return r =>
+             case r of
+             | INL _ => Fail Failure
+             | INR x => Return x
+       ]}
+     *)
+    fun mk_def_eq (i : int, def_tm : term) : term =
+      let
+        (* Retrieve the lhs of the original definition equation, and in
+           particular the inputs *)
+        val def_lhs = lhs def_tm
+        val args = (snd o strip_comb) def_lhs
 
-          (* This allows to simplify the “?n. even___P i n” *)
-          fs [] >>
-          (* We don't need the last assumption anymore *)
-          last_x_assum ignore_tac >>
+        (* Inject the inputs into the param type *)
+        val input = pairSyntax.list_mk_pair args
+        val input = inject_in_param_sum in_out_tys i true input
 
-          (* Expand *)
-          fs pred_defs >> fs [is_diverge_def] >>
-          fs expand_defs >>
+        (* Compose*)
+        val def_rhs = mk_comb (fixed_body, input)
 
-          (* 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  >>
-          rpt disch_tac >> fs [bind_def, case_result_same_eq] >>
+        (* Wrap in the case disjunction *)
+        val def_rhs = mk_case_select_result_sum def_rhs in_out_tys i false
 
-          (* Evaluate all the paths *)
-          rpt (rewrite_rec_call >> case_progress >> fs [case_result_same_eq])
+        (* Create the equation *)
+        val def_eq_tm = mk_eq (def_lhs, def_rhs)
       in
-        save_goal_and_prove (tm, prove_tac)
+        def_eq_tm
       end
+    val raw_def_tms = map mk_def_eq (enumerate def_tms)
+
+    (* Generate the definitions *)
+    val raw_defs = map (fn tm => Define ‘^tm’) raw_def_tms
   in
-    map prove_one term_div_tms
+    raw_defs
   end
 
-(*
-val (pred_tm, fun_eq_tm) = hd term_div_tms
-set_goal ([], tm)
-
-val divergence_thms =
-  prove_divergence_thms
-    term_div_tms
-    fuel_defs
-    pred_defs
-    raw_defs
-    expand_defs
-*)
+(*=============================================================================*
+ *
+ * Prove that the definitions satisfy the target equations
+ *
+ * ============================================================================*)
 
-(* Prove the final lemmas:
+(* 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
 
-   {[
-     !i. even i = even___expand even odd i
-   ]}
+(* Prove the final equation, that we will use as definition. *)
+fun prove_def_eq_tac
+  (current_raw_def : thm) (all_raw_defs : thm list) (is_valid : thm)
+  (body_def : thm option) : tactic =
+  let
+    val body_def_thm = case body_def of SOME th => [th] | NONE => []
+  in
+    rpt gen_tac >>
+    (* Expand the definition *)
+    pure_once_rewrite_tac [current_raw_def] >>
+    (* Use the fixed-point equality *)
+    pure_once_rewrite_left_tac [HO_MATCH_MP fix_fixed_eq is_valid] >>
+    (* Expand the body definition *)
+    pure_rewrite_tac body_def_thm >>
+    (* Expand all the definitions from the group *)
+    pure_rewrite_tac all_raw_defs >>
+    (* Explore all the paths - maybe we can be smarter, but this is fast and really easy *)
+    fs [bind_def] >>
+    rpt (case_progress >> fs [])
+  end
 
-   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_final_eqs
-  (term_div_tms : (term * term) list)
-  (termination_thms : thm list)
-  (divergence_thms : thm list)
-  (raw_defs : thm list)
-  : thm list =
+(* Prove the final equations that we will give to the user as definitions *)
+fun prove_def_eqs (body_is_valid : thm) (def_tms : term list) (raw_defs : thm list) : thm list=
   let
-    fun prove_one ((pred_tm, fun_eq_tm), (termination_thm, divergence_thm)) : thm =
+    val defs_tgt_raw = zip def_tms raw_defs
+    (* Substitute the function variables with the constants introduced in the raw
+       definitions *)
+    fun compute_fsubst (def_tm, raw_def) : {redex: term, residue: term} =
+      let
+        val (fvar, _) = (strip_comb o lhs) def_tm
+        val fconst = (fst o strip_comb o lhs o snd o strip_forall o concl) raw_def
+      in
+        (fvar |-> fconst)
+      end
+    val fsubst = map compute_fsubst defs_tgt_raw
+    val defs_tgt_raw = map (fn (x, y) => (subst fsubst x, y)) defs_tgt_raw
+
+    fun prove_def_eq (def_tm, raw_def) : thm =
       let
-        val (_, args) = strip_comb (lhs fun_eq_tm)
-        val g = list_mk_forall (args, fun_eq_tm)
-        (* We make a case disjunction of the subgoal: “exists n. even___P i n” *)
-        val exists_g = (rhs o concl) (PURE_REWRITE_CONV raw_defs (lhs fun_eq_tm))
-        val (_, exists_g, _) = TypeBase.dest_case exists_g
-        val prove_tac =
-          rpt gen_tac >>
-          Cases_on ‘^exists_g’
-          >-( (* Termination *)
-             irule termination_thm >> pure_asm_rewrite_tac [])
-          (* Divergence *)
-          >> irule divergence_thm >> fs []
-          
+        (* Quantify the parameters *)
+        val (_, params) = (strip_comb o lhs) def_tm
+        val def_eq_tm = list_mk_forall (params, def_tm)
+        (* Prove *)
+        val def_eq = prove (def_eq_tm, prove_def_eq_tac raw_def raw_defs body_is_valid NONE)
       in
-        save_goal_and_prove (g, prove_tac)
-      end    
+        def_eq
+      end
+    val def_eqs = map prove_def_eq defs_tgt_raw
   in
-    map prove_one (zip term_div_tms (zip termination_thms divergence_thms))
+    def_eqs
   end
 
-(*
-val termination_thm = hd termination_thms
-val divergence_thm = hd divergence_thms
-set_goal ([], g)
-*)
+(*=============================================================================*
+ *
+ * The final DefineDiv function
+ *
+ * ============================================================================*)
 
-(* The final function: define potentially diverging functions in an error monad *)
 fun DefineDiv (def_qt : term quotation) =
   let
-    (* Parse the definitions.
-    
-       Example:
-       {[
-         (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))
-       ]}
-     *)
+    (* Parse the definitions *)
     val def_tms = (strip_conj o list_mk_conj o rev) (Defn.parse_quote def_qt)
 
-    (* Generate definitions which use some fuel
-    
-       Example:
-       {[
-         even___fuel n i =
-           case fuel of
-             0 => Diverge
-           | SUC fuel => 
-             if i = 0 then Return T else odd_fuel (i - 1))
-       ]}
-     *)
-     val fuel_defs = mk_fuel_defs def_tms
-
-     (* Generate the predicate definitions.
-     
-        {[ even___P n i = = ~is_diverge (even___fuel n i) ]}
-      *)
-     val fuel_def_tms = map (snd o strip_forall o concl) fuel_defs
-     val pred_defs = map mk_fuel_predicate_defs (zip def_tms fuel_def_tms)
-     
-     (* Prove the monotonicity property for the fuel, all at once
-
-      *)
-     val fuel_mono_thm = prove_fuel_mono pred_defs fuel_defs
-     
-     (* Prove the individual fuel functions - TODO: update
-
-        {[
-          !n i. $LEAST (even___P i) <= n ==> even___fuel n i = even___fuel ($LEAST (even___P i)) i
-        ]}
-      *)
-     val least_fuel_mono_thms = prove_least_fuel_mono pred_defs fuel_mono_thm
-
-     (*
-       {[
-         !n i. even___P i n ==> $LEAST (even___P i) <= n
-       ]}
-      *)
-     val least_pred_thms = prove_least_pred_thms pred_defs
-
-     (*
-       {[
-         !n i. even___P i n ==> even___P i ($LEAST (even___P i))
-       ]}
-      *)
-     val pred_n_imp_pred_least_thms = prove_pred_n_imp_pred_least_thms pred_defs
-
-     (*
-       "Raw" definitions:
-
-       {[
-         even i = if (?n. even___P i n) then even___P ($LEAST (even___P i)) i else Diverge
-       ]}
-      *)
-     val raw_defs = define_raw_defs def_tms pred_defs fuel_defs
-
-     (*
-       !n i. even___P i n ==> even___fuel n i = even i
-      *)
-     val pred_imp_fuel_eq_raw_defs =
-       prove_pred_imp_fuel_eq_raw_defs
-         pred_defs fuel_def_tms least_fuel_mono_thms
-         least_pred_thms pred_n_imp_pred_least_thms raw_defs
-
-     (* "Expand" definitions *)
-     val expand_defs = gen_expand_defs def_tms
-
-     (* Small utility *)
-     val term_div_tms = mk_termination_diverge_tms def_tms pred_defs raw_defs expand_defs
-
-     (* Termination theorems *)
-     val termination_thms =
-       prove_termination_thms term_div_tms fuel_defs pred_defs
-         raw_defs expand_defs pred_n_imp_pred_least_thms pred_imp_fuel_eq_raw_defs
+    (* Compute the names and the input/output types of the functions *)
+    fun compute_names_in_out_tys (tm : term) : string * (hol_type * hol_type) =
+      let
+        val app = lhs tm
+        val name = (fst o dest_var o fst o strip_comb) app
+        val out_ty = dest_result (type_of app)
+        val input_tys = pairSyntax.list_mk_prod (map type_of ((snd o strip_comb) app))
+      in
+        (name, (input_tys, out_ty))
+      end
+    val (fnames, in_out_tys) = unzip (map compute_names_in_out_tys def_tms)
 
-     (* Divergence theorems *)
-     val divergence_thms =
-       prove_divergence_thms term_div_tms fuel_defs pred_defs raw_defs expand_defs
+    (* Generate the body to give to the fixed-point operator *)
+    val body = mk_body fnames in_out_tys def_tms
 
-     (* Final theorems:
+    (* Prove that the body satisfies the validity property required by the fixed point *)
+    val body_is_valid = prove_body_is_valid body
+    
+    (* Generate the definitions for the various functions by using the fixed point
+       and the body *)
+    val raw_defs = mk_raw_defs in_out_tys def_tms body_is_valid
 
-        {[
-          ∀i. even i = even___E even odd i,
-          ⊢ ∀i. odd i = odd___E even odd i
-        ]}
-      *)
-     val final_eqs = prove_final_eqs term_div_tms termination_thms divergence_thms raw_defs
-     val final_eqs = map (PURE_REWRITE_RULE expand_defs) final_eqs
+    (* Prove the final equations *)
+    val def_eqs = prove_def_eqs body_is_valid def_tms raw_defs
   in
-    (* We return the final equations, which act as rewriting theorems *)
-    final_eqs
+    def_eqs
   end
 
 end
diff --git a/backends/hol4/divDefLibExampleScript.sml b/backends/hol4/divDefLibExampleScript.sml
new file mode 100644
index 00000000..c4a57783
--- /dev/null
+++ b/backends/hol4/divDefLibExampleScript.sml
@@ -0,0 +1,29 @@
+(* Examples which use divDefLib.DefineDiv *)
+
+open HolKernel boolLib bossLib Parse
+open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
+
+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 [nth_def] = DefineDiv ‘
+  nth (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 tl i0
+        od
+    | ListNil => Fail Failure
+’
diff --git a/backends/hol4/divDefNoFixLib.sig b/backends/hol4/divDefNoFixLib.sig
new file mode 100644
index 00000000..eefc6ff7
--- /dev/null
+++ b/backends/hol4/divDefNoFixLib.sig
@@ -0,0 +1,99 @@
+(* **DEPRECATED**: see divDefLib
+
+   This library defines an older version of DefineDiv, which doesn't use
+   fixed-point operator and thus relies on more complex meta functions.
+
+   Define a (group of mutually recursive) function(s) which uses an error
+   monad and is potentially divergent.
+
+   We encode divergence in such a way that we don't have to prove that the
+   functions we define terminate *upon defining them*, and can do those proofs
+   in an extrinsic way later. It works as follows.
+
+   Let's say you want to define the following “even” and “odd” functions
+   which operate on *integers*:
+
+   {[
+     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)
+   ]}
+
+   It is easy to prove that the functions terminate provided the input is >= 0,
+   but it would require to be able to define those functions in the first place!
+
+   {!DefineDev} consequently does the following.
+
+   It first defines versions of “even” and “odd” which use fuel:
+   {[
+     even___fuel (n : num) (i : int) : bool result =
+       case n of 0 => Diverge
+       | SUC m => if i = 0 then Return T else odd___fuel m (i - 1) /\
+
+     odd___fuel (n : num) (i : int) : bool result =
+       case n of 0 => Diverge
+       | SUC m => if i = 0 then Return F else even___fuel m (i - 1)
+   ]}
+
+   Those functions trivially terminate.
+
+   Then, provided we have the following auxiliary definition:
+   {[
+     is_diverge (r: 'a result) : bool = case r of Diverge => T | _ => F
+   ]}
+
+   we can define the following predicates, which tell us whether “even___fuel”
+   and “odd___fuel” terminate on some given inputs:
+   {[
+     even___P i n = ~(is_diverge (even___fuel n i)) /\
+
+     odd___P i n = ~(is_diverge (odd___fuel n i))
+   ]}
+
+   We can finally define “even” and “odd” as follows. We use the excluded
+   middle to test whether there exists some fuel on which the function
+   terminates: if there exists such fuel, we call the "___fuel" versions
+   of “even” and “odd” with it (we use the least upper bound, to be more
+   precise). Otherwise, we simply return “Diverge”.
+   {[
+     even i =
+       if (?n. even___P i n) then even___fuel ($LEAST (even___P i)) i
+       else Diverge /\
+
+     odd i =
+       if (?n. odd___P i n) then odd___fuel ($LEAST (odd___P i)) i
+       else Diverge
+   ]}
+
+   The definitions above happen to satisfy the rewriting theorem we want:
+   {[
+     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)
+   ]}
+
+   Moreover, if we prove a lemma which states that they don't evaluate to
+   “Diverge” on some given inputs (trivial recursion if we take “i >= 0”
+   and reuse the rewriting theorem just above), then we effectively proved
+   that the functions terminate on those inputs.
+
+   Remark:
+   =======
+   {!DefineDiv} introduces all the auxiliary definitions we need and
+   automatically performs the proofs. A crucial intermediate lemma
+   we need in order to establish the last theorem is that the "___fuel"
+   versions of the functions are monotonic in the fuel.
+   More precisely:
+   {[
+     !n m. n <= m ==>
+       (!ls i. even___P ls i n ==> even___fuel n ls i n = even___fuel m ls i n) /\
+       (!ls i. odd___P ls i n ==> odd___fuel n ls i n = odd___fuel m ls i n)
+   ]}
+ *)
+
+signature divDefNoFixLib =
+sig
+  include Abbrev
+
+  val DefineDiv : term quotation -> thm list
+end
diff --git a/backends/hol4/divDefNoFixLib.sml b/backends/hol4/divDefNoFixLib.sml
new file mode 100644
index 00000000..59319e6a
--- /dev/null
+++ b/backends/hol4/divDefNoFixLib.sml
@@ -0,0 +1,1203 @@
+(* **DEPRECATED**: see divDefLib *)
+
+structure divDefNoFixLib :> divDefNoFixLib =
+struct
+
+open HolKernel boolLib bossLib Parse
+open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
+
+open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
+open primitivesLib
+
+val case_result_same_eq = prove (
+  “!(r : 'a result).
+    (case r of
+       Return x => Return x
+     | Fail e => Fail e
+     | Diverge => Diverge) = r”,
+  rw [] >> CASE_TAC)
+
+(*
+val ty = id_ty
+strip_arrows ty
+*)
+
+(* 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
+
+(* TODO: move *)
+fun strip_arrows (ty : hol_type) : hol_type list * hol_type =
+  let
+    val (ty0, ty1) = dom_rng ty
+    val (tys, ret) = strip_arrows ty1
+  in
+    (ty0::tys, ret)
+  end
+  handle HOL_ERR _ => ([], ty)
+
+(* 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 expand_suffix = "___E" (* TODO: name collisions *)
+
+val bool_ty = “:bool”
+
+val alpha_tyvar : hol_type = “:'a”
+val beta_tyvar : hol_type = “:'b”
+
+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”
+
+val measure_tm = “measure: ('a -> num) -> 'a -> 'a -> bool”
+
+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
+
+(* Small utility: we sometimes need to generate a termination measure for
+   the fuel definitions.
+
+   We derive a measure for a type which is simply the sum of the tuples
+   of the input types of the functions.
+
+   For instance, for even and odd we have:
+   {[
+     even___fuel : num -> int -> bool result
+     odd___fuel  : num -> int -> bool result
+   ]}
+
+   So the type would be:
+   {[
+     (num # int) + (num # int)
+   ]}
+
+   Note that generally speaking we expect a type of the shape (the “:num”
+   on the left is for the fuel):
+   {[
+     (num # ...) + (num # ...) + ... + (num # ...)
+   ]}
+
+   The decreasing measure is simply given by a function which matches over
+   its argument to return the fuel, whatever the case.
+ *)
+fun mk_termination_measure_from_ty (ty : hol_type) : term =
+  let
+    val dtys = map pairSyntax.strip_prod (sumSyntax.strip_sum ty)
+    (* For every tuple, create a match to extract the num *)
+    fun mk_case_of_tuple (tys : hol_type list) : (term * term) =
+      case tys of
+        [] => failwith "mk_termination_measure_from_ty: empty list of types"
+      | [num_ty] =>
+        (* No need for a case *)
+        let val var = genvar num_ty in (var, var) end
+      | num_ty :: rem_tys =>
+        let
+          val scrut_var = genvar (pairSyntax.list_mk_prod tys)
+          val var = genvar num_ty
+          val rem_var = genvar (pairSyntax.list_mk_prod rem_tys)
+          val pats = [(pairSyntax.mk_pair (var, rem_var), var)]
+          val case_tm = TypeBase.mk_case (scrut_var, pats)
+        in
+          (scrut_var, case_tm)
+        end
+     val tuple_cases = map mk_case_of_tuple dtys
+
+    (* For every sum, create a match to extract one of the tuples *)
+    fun mk_sum_case ((tuple_var, tuple_case), (nvar, case_end)) =
+      let
+        val left_pat = sumSyntax.mk_inl (tuple_var, type_of nvar)
+        val right_pat = sumSyntax.mk_inr (nvar, type_of tuple_var)
+        val scrut = genvar (sumSyntax.mk_sum (type_of tuple_var, type_of nvar))
+        val pats = [(left_pat, tuple_case), (right_pat, case_end)]
+        val case_tm = TypeBase.mk_case (scrut, pats)
+      in
+        (scrut, case_tm)
+      end
+    val tuple_cases = rev tuple_cases
+    val (nvar, case_end) = hd tuple_cases
+    val tuple_cases = tl tuple_cases
+    val (scrut, case_tm) = foldl mk_sum_case (nvar, case_end) tuple_cases
+
+    (* Create the function *)
+    val abs_tm = mk_abs (scrut, case_tm)
+    
+    (* Add the “measure term” *)
+    val tm = inst [alpha_tyvar |-> type_of scrut] measure_tm
+    val tm = mk_comb (tm, abs_tm)
+  in
+    tm
+  end
+
+(*
+val ty = “: (num # 'a) + (num # 'b) + (num # 'c)”
+
+val tys = hd dtys
+val num_ty::rem_tys = tys
+
+val (tuple_var, tuple_case) = hd tuple_cases
+*)
+
+(* Get the smallest id which make the names unique (or to be more precise:
+   such that the names don't correspond to already defined constants).
+
+   We do this for {!mk_fuel_defs}: for some reason, the termination proof
+   fails if we try to reuse the same names as before.
+ *)
+fun get_smallest_unique_id_for_names (names : string list) : string =
+  let
+    (* Not trying to be smart here *)
+    val i : int option ref = ref NONE
+    fun get_i () = case !i of NONE => "" | SOME i => int_to_string i
+    fun incr_i () =
+      i := (case !i of NONE => SOME 0 | SOME i => SOME (i+1))
+    val continue = ref true
+    fun name_is_ok (name : string) : bool =
+      not (is_const (Parse.parse_in_context [] [QUOTE (name ^ get_i ())]))
+      handle HOL_ERR _ => false
+    val _ =
+      while !continue do (
+        let val _ = (continue := not (forall name_is_ok names)) in
+        if !continue then incr_i () else () end
+      )
+  in
+    get_i ()
+  end
+
+fun mk_fuel_defs (def_tms : term list) : thm list =
+  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 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 fuel' (i - 1))”
+     *)
+     val names = map ((fn s => s ^ fuel_def_suffix) o fst o dest_var) ids
+     val index = get_smallest_unique_id_for_names names
+     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 ^ index
+         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_fuel0 = map (fn id => mk_comb (id, fuel_var0)) fuel_ids
+     val fuel_ids_with_fuel1 = map (fn id => mk_comb (id, fuel_var1)) fuel_ids
+
+     (* Recurse through the terms and replace the calls *)
+     val rwr_thms0 = map (ASSUME o mk_eq) (zip ids fuel_ids_with_fuel0)
+     val rwr_thms1 = map (ASSUME o mk_eq) (zip ids fuel_ids_with_fuel1)
+
+     fun mk_fuel_tm (def_tm : term) : term =
+       let
+         val (tm0, tm1) = dest_eq def_tm
+         val tm0 = (rhs o concl o (PURE_REWRITE_CONV rwr_thms0)) tm0
+         val tm1 = (rhs o concl o (PURE_REWRITE_CONV rwr_thms1)) tm1
+       in mk_eq (tm0, tm1) end
+     val fuel_tms = map mk_fuel_tm def_tms
+
+     (* Add the case over the fuel *)
+     fun add_fuel_case (tm : term) : term =
+       let
+         val (f, 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_var1)
+         val fuel_tm =
+           TypeBase.mk_case (fuel_var0, [(num_zero_tm, diverge_tm), (suc_tm, body)])
+       in mk_eq (f, 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
+     (* The definition name *)
+     val def_name = (fst o dest_var o hd) fuel_ids
+     (* The tactic to prove the termination *)
+     val rty = ref “:bool” (* This is useful for debugging *)
+     fun prove_termination_tac (asms, g) =
+       let
+         val r_tm = (fst o dest_exists) g
+         val _ = rty := type_of r_tm
+         val ty = (hd o snd o dest_type) (!rty)
+         val m_tm = mk_termination_measure_from_ty ty
+       in
+         WF_REL_TAC ‘^m_tm’ (asms, g)
+       end
+
+     (* Define the fuel definitions *)
+     (*
+       val temp_def = Hol_defn def_name ‘^fuel_defs_conj’
+       Defn.tgoal temp_def
+     *)
+     val fuel_defs = tDefine def_name ‘^fuel_defs_conj’ prove_termination_tac
+   in
+     CONJUNCTS fuel_defs
+   end
+
+(*
+val (fuel_tms, fuel_defs) = mk_fuel_defs def_tms
+val fuel_def_tms = map (snd o strip_forall) ((strip_conj o concl) fuel_defs)
+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 (tys, ret_ty) = strip_arrows id_ty
+    val tys = append tys [num_ty]
+    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 (def_tm, fuel_def_tm) = hd (zip def_tms fuel_def_tms)
+
+val pred_defs = 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  
+
+(* 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_defs : thm list) (fuel_defs : thm list) : thm =
+  let
+    val pred_tms = map (lhs o snd o strip_forall o concl) pred_defs
+    val fuel_tms = map (lhs o snd o strip_forall o concl) fuel_defs
+    val pred_fuel_tms = zip pred_tms fuel_tms
+    (* Create a set containing the names of all the functions in the recursive group *)
+    val rec_fun_set =
+      Redblackset.fromList const_name_compare (map get_fun_name_from_app fuel_tms)
+    (* Small tactic which rewrites the occurrences of 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
+             (* Yes: use the induction hypothesis *)
+             fun apply_ind_hyp (ind_th : thm) : tactic =
+               let
+                  val th = SPEC_ALL ind_th
+                  val th_pat = (lhs o snd o strip_imp o concl) th
+                  val (var_s, ty_s) = match_term th_pat scrut
+                  (* Note that in practice the type instantiation should be empty *)
+                  val th = INST var_s (INST_TYPE ty_s th)
+               in
+                 assume_tac th
+               end
+          in
+            (last_assum apply_ind_hyp >> fs []) (asms, g)
+          end
+        else all_tac (asms, g)
+      end
+      handle HOL_ERR _ => all_tac (asms, g)
+    (* 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
+     (* Qantify over the fuels *)
+     val fuel_eq_tms = list_mk_forall ([fuel_var0, fuel_var1], fuel_eq_tms)
+     (* The tactics for the proof *)
+     val prove_tac =
+       Induct_on ‘^fuel_var0’ >-(
+         (* The ___P predicates are false: n is 0 *)
+         fs pred_defs >>
+         fs [is_diverge_def] >>
+         pure_once_rewrite_tac fuel_defs >> fs []) >>
+       (* Introduce n *)
+       gen_tac >>
+       (* Introduce m *)
+       Cases_on ‘^fuel_var1’ >-(
+         (* Contradiction: SUC n < 0 *)
+         rw [] >> exfalso >> int_tac) >>
+       fs pred_defs >>
+       fs [is_diverge_def] >>
+       pure_once_rewrite_tac fuel_defs >> fs [bind_def] >>
+       (* Introduce in the context *)
+       rpt gen_tac >>
+       (* Split the goals - note that we prove one big goal for all the functions at once *)
+       rpt strip_tac >>
+       (* Instantiate the assumption: !m. n <= m ==> ~(...)
+          with the proper m.
+        *)
+       last_x_assum imp_res_tac >>
+       (* Make sure the induction hypothesis is always the last assumption *)
+       last_x_assum assume_tac >>
+       (* Split the goals *)
+       rpt strip_tac >> fs [case_result_same_eq] >>
+       (* Explore all the paths *)
+       rpt (rewrite_rec_call >> case_progress >> fs [case_result_same_eq])
+   in
+     (* Prove *)
+     save_goal_and_prove (fuel_eq_tms, prove_tac)
+   end
+
+(*
+val fuel_mono_thm = prove_fuel_mono pred_defs fuel_defs
+
+set_goal ([], fuel_eq_tms)
+*)
+
+(* 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_defs : 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, mono_thm) : thm =
+      let
+        (* Retrieve the predicate, without the fuel *)
+        val pred_tm = (lhs o snd o strip_forall o concl) pred_def
+        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_defs thl)
+  end
+
+(*
+val (pred_def, mono_thm) = hd (zip pred_defs thl)
+*)
+
+(* 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_defs : thm list) : thm list =
+  let
+    fun prove_least_pred_thm (pred_def : thm) : thm =
+      let
+        val pred_tm = (lhs o snd o strip_forall o concl) pred_def
+        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_defs
+  end
+
+
+(*
+val least_pred_thms = prove_least_pred_thms pred_defs
+
+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_defs : thm list) : thm list =
+  let
+    fun prove_pred_n_imp_pred_least (pred_def : thm) : thm =
+      let
+        val pred_tm = (lhs o snd o strip_forall o concl) pred_def
+        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_defs
+  end
+
+(*
+val (pred_def, mono_thm) = hd (zip pred_defs thl)
+val least_fuel_mono_thms = prove_least_fuel_mono pred_defs fuel_defs 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_defs : thm list) (fuel_defs : thm list) : thm list =
+  let
+    fun define_raw_def (def_tm, (pred_def, fuel_def)) : thm =
+      let
+        val app = lhs def_tm
+        val pred_tm = (lhs o snd o strip_forall o concl) pred_def
+        (* 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
+        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_defs fuel_defs))
+  end
+
+(*
+val raw_defs = define_raw_defs def_tms pred_defs fuel_defs
+ *)
+
+(* Prove theorems of the shape:
+
+   !n i. even___P i n ==> even___fuel n i = even i
+ *)
+fun prove_pred_imp_fuel_eq_raw_defs
+  (pred_defs : 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_defs : thm list) :
+  thm list =
+  let
+    fun prove_thm (pred_def,
+                   (fuel_def_tm,
+                    (least_fuel_mono_thm,
+                     (least_pred_thm,
+                      (pred_n_imp_pred_least_thm, raw_def))))) : thm =
+      let
+        (* Generate: “even___P i n” *)
+        val pred_tm = (lhs o snd o strip_forall o concl) pred_def
+        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
+        (* 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_defs >>
+          (* 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_defs (zip fuel_def_tms (zip least_fuel_mono_thms
+                   (zip least_pred_thms (zip pred_n_imp_pred_least_thms raw_defs)))))
+  end
+
+(*
+val pred_imp_fuel_eq_raw_defs =
+  prove_pred_imp_fuel_eq_raw_defs
+    pred_defs fuel_def_tms least_fuel_mono_thms least_pred_thms
+    pred_n_imp_pred_least_thms raw_defs
+ *)
+
+
+(* 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
+  (def_tms : term list)
+  (pred_defs : thm list)
+  (raw_defs : 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) =
+      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
+      in
+        (var |-> f)
+      end
+    val fun_subst = map mk_fun_subst (zip def_tms raw_defs)
+  
+    fun mk_tm (pred_def, (raw_def, expand_def)) :
+      term * term =
+      let
+        (* “even___P i n” *)
+        val pred_tm = (lhs o snd o strip_forall o concl) pred_def
+        (* “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
+        val fun_eq_tm = mk_eq (fun_tm, expand_tm)
+      in (pred_tm, fun_eq_tm) end
+  in
+    map mk_tm (zip pred_defs (zip raw_defs expand_defs))
+  end
+
+(*
+val term_div_tms =
+  mk_termination_diverge_tms pred_defs raw_defs 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 list)
+  (pred_defs : thm list)
+  (raw_defs : thm list)
+  (expand_defs : thm list)
+  (pred_n_imp_pred_least_thms : thm list)
+  (pred_imp_fuel_eq_raw_defs : 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, eq_th) =
+      let
+        val rfun = (get_fun_name_from_app o lhs o snd o strip_forall o concl) fuel_def
+      in
+        (rfun, eq_th)
+      end
+    val rec_fun_eq_map =
+      Redblackmap.fromList const_name_compare (
+        map mk_rec_fun_eq_pair
+          (zip fuel_defs pred_imp_fuel_eq_raw_defs))
+
+    (* 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_defs >> 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 (lhs fun_eq_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_defs >>
+          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_defs >>
+          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 >>
+          rpt disch_tac >>
+
+          (* Expand the binds *)
+          fs [bind_def, case_result_same_eq] >>
+
+          (* Explore all the paths by doing case disjunctions *)
+          rpt (rewrite_rec_call >> case_progress >> fs [case_result_same_eq])
+      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 pred_defs
+    raw_defs expand_defs pred_n_imp_pred_least_thms
+    pred_imp_fuel_eq_raw_defs
+
+val ((pred_tm, fun_eq_tm), pred_n_imp_pred_least_thm) = hd (zip term_div_tms pred_n_imp_pred_least_thms)
+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 list)
+  (pred_defs : thm list)
+  (raw_defs : 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) =
+     (get_fun_name_from_app o lhs o snd o strip_forall o concl) fuel_def
+    val rec_fun_set =
+      Redblackset.fromList const_name_compare (
+        map get_rec_fun_id raw_defs)
+
+    (* 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_defs scrut)
+            val (_, exists_g, _) = TypeBase.dest_case exists_g
+            (* The tactic to prove the subgoal *)
+            val prove_sg_tac =
+              pure_rewrite_tac raw_defs >>
+              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_defs >> 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 (lhs fun_eq_tm)
+        val tm = list_mk_forall (args, tm)
+
+        (* Prove *)
+        val prove_tac =
+          rpt gen_tac >>
+
+          pure_rewrite_tac raw_defs >>
+          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_defs >> 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  >>
+          rpt disch_tac >> fs [bind_def, case_result_same_eq] >>
+
+          (* Evaluate all the paths *)
+          rpt (rewrite_rec_call >> case_progress >> fs [case_result_same_eq])
+      in
+        save_goal_and_prove (tm, prove_tac)
+      end
+  in
+    map prove_one term_div_tms
+  end
+
+(*
+val (pred_tm, fun_eq_tm) = hd term_div_tms
+set_goal ([], tm)
+
+val divergence_thms =
+  prove_divergence_thms
+    term_div_tms
+    fuel_defs
+    pred_defs
+    raw_defs
+    expand_defs
+*)
+
+(* Prove the final lemmas:
+
+   {[
+     !i. 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_final_eqs
+  (term_div_tms : (term * term) list)
+  (termination_thms : thm list)
+  (divergence_thms : thm list)
+  (raw_defs : thm list)
+  : thm list =
+  let
+    fun prove_one ((pred_tm, fun_eq_tm), (termination_thm, divergence_thm)) : thm =
+      let
+        val (_, args) = strip_comb (lhs fun_eq_tm)
+        val g = list_mk_forall (args, fun_eq_tm)
+        (* We make a case disjunction of the subgoal: “exists n. even___P i n” *)
+        val exists_g = (rhs o concl) (PURE_REWRITE_CONV raw_defs (lhs fun_eq_tm))
+        val (_, exists_g, _) = TypeBase.dest_case exists_g
+        val prove_tac =
+          rpt gen_tac >>
+          Cases_on ‘^exists_g’
+          >-( (* Termination *)
+             irule termination_thm >> pure_asm_rewrite_tac [])
+          (* Divergence *)
+          >> irule divergence_thm >> fs []
+          
+      in
+        save_goal_and_prove (g, prove_tac)
+      end    
+  in
+    map prove_one (zip term_div_tms (zip termination_thms divergence_thms))
+  end
+
+(*
+val termination_thm = hd termination_thms
+val divergence_thm = hd divergence_thms
+set_goal ([], g)
+*)
+
+(* The final function: define potentially diverging functions in an error monad *)
+fun DefineDiv (def_qt : term quotation) =
+  let
+    (* Parse the definitions.
+    
+       Example:
+       {[
+         (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)
+
+    (* Generate definitions which use some fuel
+    
+       Example:
+       {[
+         even___fuel n i =
+           case fuel of
+             0 => Diverge
+           | SUC fuel => 
+             if i = 0 then Return T else odd_fuel (i - 1))
+       ]}
+     *)
+     val fuel_defs = mk_fuel_defs def_tms
+
+     (* Generate the predicate definitions.
+     
+        {[ even___P n i = = ~is_diverge (even___fuel n i) ]}
+      *)
+     val fuel_def_tms = map (snd o strip_forall o concl) fuel_defs
+     val pred_defs = map mk_fuel_predicate_defs (zip def_tms fuel_def_tms)
+     
+     (* Prove the monotonicity property for the fuel, all at once
+
+      *)
+     val fuel_mono_thm = prove_fuel_mono pred_defs fuel_defs
+     
+     (* Prove the individual fuel functions - TODO: update
+
+        {[
+          !n i. $LEAST (even___P i) <= n ==> even___fuel n i = even___fuel ($LEAST (even___P i)) i
+        ]}
+      *)
+     val least_fuel_mono_thms = prove_least_fuel_mono pred_defs fuel_mono_thm
+
+     (*
+       {[
+         !n i. even___P i n ==> $LEAST (even___P i) <= n
+       ]}
+      *)
+     val least_pred_thms = prove_least_pred_thms pred_defs
+
+     (*
+       {[
+         !n i. even___P i n ==> even___P i ($LEAST (even___P i))
+       ]}
+      *)
+     val pred_n_imp_pred_least_thms = prove_pred_n_imp_pred_least_thms pred_defs
+
+     (*
+       "Raw" definitions:
+
+       {[
+         even i = if (?n. even___P i n) then even___P ($LEAST (even___P i)) i else Diverge
+       ]}
+      *)
+     val raw_defs = define_raw_defs def_tms pred_defs fuel_defs
+
+     (*
+       !n i. even___P i n ==> even___fuel n i = even i
+      *)
+     val pred_imp_fuel_eq_raw_defs =
+       prove_pred_imp_fuel_eq_raw_defs
+         pred_defs fuel_def_tms least_fuel_mono_thms
+         least_pred_thms pred_n_imp_pred_least_thms raw_defs
+
+     (* "Expand" definitions *)
+     val expand_defs = gen_expand_defs def_tms
+
+     (* Small utility *)
+     val term_div_tms = mk_termination_diverge_tms def_tms pred_defs raw_defs expand_defs
+
+     (* Termination theorems *)
+     val termination_thms =
+       prove_termination_thms term_div_tms fuel_defs pred_defs
+         raw_defs expand_defs pred_n_imp_pred_least_thms pred_imp_fuel_eq_raw_defs
+
+     (* Divergence theorems *)
+     val divergence_thms =
+       prove_divergence_thms term_div_tms fuel_defs pred_defs raw_defs expand_defs
+
+     (* Final theorems:
+
+        {[
+          ∀i. even i = even___E even odd i,
+          ⊢ ∀i. odd i = odd___E even odd i
+        ]}
+      *)
+     val final_eqs = prove_final_eqs term_div_tms termination_thms divergence_thms raw_defs
+     val final_eqs = map (PURE_REWRITE_RULE expand_defs) final_eqs
+  in
+    (* We return the final equations, which act as rewriting theorems *)
+    final_eqs
+  end
+
+end
diff --git a/backends/hol4/testDivDefScript.sml b/backends/hol4/divDefNoFixLibTestScript.sml
index 4a87895f..b2a4d607 100644
--- a/backends/hol4/testDivDefScript.sml
+++ b/backends/hol4/divDefNoFixLibTestScript.sml
@@ -2,9 +2,9 @@ open HolKernel boolLib bossLib Parse
 open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
 
 open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
-open primitivesLib divDefLib
+open primitivesLib divDefNoFixLib
 
-val _ = new_theory "testDivDef"
+val _ = new_theory "divDefNoFixLibTest"
 
 val def_qt = ‘
   (even (i : int) : bool result =
diff --git a/backends/hol4/testDivDefTheory.sig b/backends/hol4/divDefNoFixLibTestTheory.sig
index a3ce2255..999cf543 100644
--- a/backends/hol4/testDivDefTheory.sig
+++ b/backends/hol4/divDefNoFixLibTestTheory.sig
@@ -1,4 +1,4 @@
-signature testDivDefTheory =
+signature divDefNoFixLibTestTheory =
 sig
   type thm = Thm.thm
   
@@ -40,9 +40,9 @@ sig
     val nth_mut_fwd___fuel_def : thm
     val nth_mut_fwd___fuel_ind : thm
   
-  val testDivDef_grammars : type_grammar.grammar * term_grammar.grammar
+  val divDefNoFixLibTest_grammars : type_grammar.grammar * term_grammar.grammar
 (*
-   [primitives] Parent theory of "testDivDef"
+   [primitives] Parent theory of "divDefNoFixLibTest"
    
    [even___E_def]  Definition
       
diff --git a/backends/hol4/divDefProto2TestScript.sml b/backends/hol4/divDefProto2TestScript.sml
index 39719b65..bc9ea9a7 100644
--- a/backends/hol4/divDefProto2TestScript.sml
+++ b/backends/hol4/divDefProto2TestScript.sml
@@ -57,29 +57,6 @@ fun prove_valid_case_progress
 val (asms, g) = top_goal ()
 *)
 
-(* TODO: move *)
-(* This theorem is important to shape the goal when proving that a body
-   satifies the fixed point validity property.
-
-   Importantly: this theorem relies on the fact that errors are just transmitted
-   to the caller (in particular, without modification).
- *)
-Theorem case_result_switch_eq:
-  (case (case x of Return y => f y | Fail e => Fail e | Diverge => Diverge) of
-  | Return y => g y
-  | Fail e => Fail e
-  | Diverge => Diverge) =
-  (case x of
-   | Return y =>
-     (case f y of
-     | Return y => g y
-     | Fail e => Fail e
-     | Diverge => Diverge)
-  | Fail e => Fail e
-  | Diverge => Diverge)
-Proof
-  Cases_on ‘x’ >> fs []
-QED
 
 (* Tactic to prove that a body is valid: perform one step. *)
 fun prove_body_is_valid_tac_step (asms, g) =
diff --git a/backends/hol4/divDefProto2Theory.sig b/backends/hol4/divDefProto2Theory.sig
deleted file mode 100644
index 77d5631e..00000000
--- a/backends/hol4/divDefProto2Theory.sig
+++ /dev/null
@@ -1,334 +0,0 @@
-signature divDefProto2Theory =
-sig
-  type thm = Thm.thm
-  
-  (*  Definitions  *)
-    val even_odd_body_def : thm
-    val fix_def : thm
-    val fix_fuel_P_def : thm
-    val fix_fuel_def : thm
-    val is_valid_fp_body_def : thm
-    val list_t_TY_DEF : thm
-    val list_t_case_def : thm
-    val list_t_size_def : thm
-    val nth_body_def : thm
-  
-  (*  Theorems  *)
-    val datatype_list_t : thm
-    val even_def : thm
-    val even_odd_body_is_valid : thm
-    val even_odd_body_is_valid_aux : thm
-    val fix_fixed_diverges : thm
-    val fix_fixed_eq : thm
-    val fix_fixed_terminates : thm
-    val fix_fuel_P_least : thm
-    val fix_fuel_compute : thm
-    val fix_fuel_eq_fix : thm
-    val fix_fuel_mono : thm
-    val fix_fuel_mono_aux : thm
-    val fix_fuel_mono_least : thm
-    val fix_fuel_not_diverge_eq_fix : thm
-    val fix_fuel_not_diverge_eq_fix_aux : thm
-    val fix_not_diverge_implies_fix_fuel : thm
-    val fix_not_diverge_implies_fix_fuel_aux : thm
-    val is_valid_fp_body_compute : 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 nth_body_is_valid : thm
-    val nth_body_is_valid_aux : thm
-    val nth_def : thm
-    val odd_def : thm
-  
-  val divDefProto2_grammars : type_grammar.grammar * term_grammar.grammar
-(*
-   [primitives] Parent theory of "divDefProto2"
-   
-   [even_odd_body_def]  Definition
-      
-      ⊢ ∀f x.
-          even_odd_body f x =
-          case x of
-            INL 0 => Return (INR (INR T))
-          | INL i =>
-            (case f (INR (INL (i − 1))) of
-               Return (INL v) => Fail Failure
-             | Return (INR (INL v2)) => Fail Failure
-             | Return (INR (INR b)) => Return (INR (INR b))
-             | Fail e => Fail e
-             | Diverge => Diverge)
-          | INR (INL 0) => Return (INR (INR F))
-          | INR (INL i) =>
-            (case f (INL (i − 1)) of
-               Return (INL v) => Fail Failure
-             | Return (INR (INL v2)) => Fail Failure
-             | Return (INR (INR b)) => Return (INR (INR b))
-             | Fail e => Fail e
-             | Diverge => Diverge)
-          | INR (INR v5) => Fail Failure
-   
-   [fix_def]  Definition
-      
-      ⊢ ∀f x.
-          fix f x =
-          if ∃n. fix_fuel_P f x n then
-            fix_fuel ($LEAST (fix_fuel_P f x)) f x
-          else Diverge
-   
-   [fix_fuel_P_def]  Definition
-      
-      ⊢ ∀f x n. fix_fuel_P f x n ⇔ ¬is_diverge (fix_fuel n f x)
-   
-   [fix_fuel_def]  Definition
-      
-      ⊢ (∀f x. fix_fuel 0 f x = Diverge) ∧
-        ∀n f x. fix_fuel (SUC n) f x = f (fix_fuel n f) x
-   
-   [is_valid_fp_body_def]  Definition
-      
-      ⊢ (∀f. is_valid_fp_body 0 f ⇔ F) ∧
-        ∀n f.
-          is_valid_fp_body (SUC n) f ⇔
-          ∀x. (∀g h. f g x = f h x) ∨
-              ∃h y.
-                is_valid_fp_body n h ∧ ∀g. f g x = do z <- g y; h g z od
-   
-   [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
-   
-   [nth_body_def]  Definition
-      
-      ⊢ ∀f x.
-          nth_body f x =
-          case x of
-            INL x =>
-              (let
-                 (ls,i) = x
-               in
-                 case ls of
-                   ListCons x tl =>
-                     if u32_to_int i = 0 then Return (INR x)
-                     else
-                       do
-                         i0 <- u32_sub i (int_to_u32 1);
-                         r <- f (INL (tl,i0));
-                         case r of
-                           INL v => Fail Failure
-                         | INR i1 => Return (INR i1)
-                       od
-                 | ListNil => Fail Failure)
-          | INR v2 => Fail Failure
-   
-   [datatype_list_t]  Theorem
-      
-      ⊢ DATATYPE (list_t ListCons ListNil)
-   
-   [even_def]  Theorem
-      
-      ⊢ ∀i. even i = if i = 0 then Return T else odd (i − 1)
-   
-   [even_odd_body_is_valid]  Theorem
-      
-      ⊢ is_valid_fp_body (SUC (SUC 0)) even_odd_body
-   
-   [even_odd_body_is_valid_aux]  Theorem
-      
-      ⊢ is_valid_fp_body (SUC (SUC n)) even_odd_body
-   
-   [fix_fixed_diverges]  Theorem
-      
-      ⊢ ∀N f.
-          is_valid_fp_body N f ⇒
-          ∀x. ¬(∃n. fix_fuel_P f x n) ⇒ fix f x = f (fix f) x
-   
-   [fix_fixed_eq]  Theorem
-      
-      ⊢ ∀N f. is_valid_fp_body N f ⇒ ∀x. fix f x = f (fix f) x
-   
-   [fix_fixed_terminates]  Theorem
-      
-      ⊢ ∀N f.
-          is_valid_fp_body N f ⇒
-          ∀x n. fix_fuel_P f x n ⇒ fix f x = f (fix f) x
-   
-   [fix_fuel_P_least]  Theorem
-      
-      ⊢ ∀f n x.
-          fix_fuel n f x ≠ Diverge ⇒
-          fix_fuel_P f x ($LEAST (fix_fuel_P f x))
-   
-   [fix_fuel_compute]  Theorem
-      
-      ⊢ (∀f x. fix_fuel 0 f x = Diverge) ∧
-        (∀n f x.
-           fix_fuel (NUMERAL (BIT1 n)) f x =
-           f (fix_fuel (NUMERAL (BIT1 n) − 1) f) x) ∧
-        ∀n f x.
-          fix_fuel (NUMERAL (BIT2 n)) f x =
-          f (fix_fuel (NUMERAL (BIT1 n)) f) x
-   
-   [fix_fuel_eq_fix]  Theorem
-      
-      ⊢ ∀N f.
-          is_valid_fp_body N f ⇒
-          ∀n x. fix_fuel_P f x n ⇒ fix_fuel n f x = fix f x
-   
-   [fix_fuel_mono]  Theorem
-      
-      ⊢ ∀N f.
-          is_valid_fp_body N f ⇒
-          ∀n x.
-            fix_fuel_P f x n ⇒ ∀m. n ≤ m ⇒ fix_fuel n f x = fix_fuel m f x
-   
-   [fix_fuel_mono_aux]  Theorem
-      
-      ⊢ ∀n N M g f.
-          is_valid_fp_body M f ⇒
-          is_valid_fp_body N g ⇒
-          ∀x. ¬is_diverge (g (fix_fuel n f) x) ⇒
-              ∀m. n ≤ m ⇒ g (fix_fuel n f) x = g (fix_fuel m f) x
-   
-   [fix_fuel_mono_least]  Theorem
-      
-      ⊢ ∀N f.
-          is_valid_fp_body N f ⇒
-          ∀n x.
-            fix_fuel_P f x n ⇒
-            fix_fuel n f x = fix_fuel ($LEAST (fix_fuel_P f x)) f x
-   
-   [fix_fuel_not_diverge_eq_fix]  Theorem
-      
-      ⊢ ∀N f.
-          is_valid_fp_body N f ⇒
-          ∀n x.
-            f (fix_fuel n f) x ≠ Diverge ⇒ f (fix f) x = f (fix_fuel n f) x
-   
-   [fix_fuel_not_diverge_eq_fix_aux]  Theorem
-      
-      ⊢ ∀N M g f.
-          is_valid_fp_body M f ⇒
-          is_valid_fp_body N g ⇒
-          ∀n x.
-            g (fix_fuel n f) x ≠ Diverge ⇒ g (fix f) x = g (fix_fuel n f) x
-   
-   [fix_not_diverge_implies_fix_fuel]  Theorem
-      
-      ⊢ ∀N f.
-          is_valid_fp_body N f ⇒
-          ∀x. f (fix f) x ≠ Diverge ⇒ ∃n. f (fix f) x = f (fix_fuel n f) x
-   
-   [fix_not_diverge_implies_fix_fuel_aux]  Theorem
-      
-      ⊢ ∀N M g f.
-          is_valid_fp_body M f ⇒
-          is_valid_fp_body N g ⇒
-          ∀x. g (fix f) x ≠ Diverge ⇒
-              ∃n. g (fix f) x = g (fix_fuel n f) x ∧
-                  ∀m. n ≤ m ⇒ g (fix_fuel m f) x = g (fix_fuel n f) x
-   
-   [is_valid_fp_body_compute]  Theorem
-      
-      ⊢ (∀f. is_valid_fp_body 0 f ⇔ F) ∧
-        (∀n f.
-           is_valid_fp_body (NUMERAL (BIT1 n)) f ⇔
-           ∀x. (∀g h. f g x = f h x) ∨
-               ∃h y.
-                 is_valid_fp_body (NUMERAL (BIT1 n) − 1) h ∧
-                 ∀g. f g x = do z <- g y; h g z od) ∧
-        ∀n f.
-          is_valid_fp_body (NUMERAL (BIT2 n)) f ⇔
-          ∀x. (∀g h. f g x = f h x) ∨
-              ∃h y.
-                is_valid_fp_body (NUMERAL (BIT1 n)) h ∧
-                ∀g. f g x = do z <- g y; h g z od
-   
-   [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
-   
-   [nth_body_is_valid]  Theorem
-      
-      ⊢ is_valid_fp_body (SUC (SUC 0)) nth_body
-   
-   [nth_body_is_valid_aux]  Theorem
-      
-      ⊢ is_valid_fp_body (SUC (SUC n)) nth_body
-   
-   [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)
-   
-   
-*)
-end
diff --git a/backends/hol4/divDefProtoScript.sml b/backends/hol4/divDefProtoScript.sml
deleted file mode 100644
index 6280fa7e..00000000
--- a/backends/hol4/divDefProtoScript.sml
+++ /dev/null
@@ -1,252 +0,0 @@
-(* Prototype: divDefLib but with general combinators *)
-
-open HolKernel boolLib bossLib Parse
-open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
-
-open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
-open primitivesLib
-
-val _ = new_theory "divDefProto"
-
-(*
- * Test with a general validity predicate.
- *
- * TODO: this works! Cleanup.
- *)
-val fix_fuel_def = Define ‘
-  (fix_fuel (0 : num) (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = Diverge) ∧
-  (fix_fuel (SUC n) (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = f (fix_fuel n f) x)
-’
-
-val fix_fuel_P_def = Define ‘
-  fix_fuel_P f x n = ~(is_diverge (fix_fuel n f x))
-’
-
-val fix_def = Define ‘
-  fix (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result =
-    if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge
-’
-
-val is_valid_fp_body_def = Define ‘
-  is_valid_fp_body (f : ('a -> 'b result) -> 'a -> 'b result) =
-    ∀x. (∀g h. f g x = f h x) ∨ (∃ y. ∀g. f g x = g y)
-’
-
-Theorem fix_fuel_mono:
-  ∀f. is_valid_fp_body f ⇒
-    ∀n x. fix_fuel_P f x n ⇒
-     ∀ m. n ≤ m ⇒
-       fix_fuel n f x = fix_fuel m f x
-Proof
-  ntac 2 strip_tac >>
-  Induct_on ‘n’ >> rpt strip_tac
-  >- (fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]) >>
-  Cases_on ‘m’ >- int_tac >> fs [] >>
-    fs [is_valid_fp_body_def] >>
-  fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
-
-  (* Use the validity property *)
-  last_x_assum (qspec_assume ‘x’) >>
-  (* This makes a case disjunction on the validity property *)
-  rw []
-  >-((* Case 1: the continuation doesn't matter *) fs []) >>
-  (* Case 2: the continuation *does* matter (i.e., there is a recursive call *)
-  (* Instantiate the validity property with the different continuations *)
-  first_assum (qspec_assume ‘fix_fuel n f’) >>
-  first_assum (qspec_assume ‘fix_fuel n' f’) >>
-  last_assum (qspec_assume ‘y’) >>
-  fs []
-QED
-
-(* TODO: remove? *)
-Theorem fix_fuel_mono_least:
-  ∀f. is_valid_fp_body f ⇒
-    ∀n x. fix_fuel_P f x n ⇒
-      fix_fuel n f x = fix_fuel ($LEAST (fix_fuel_P f x)) f x
-Proof
-  rw [] >>
-  pure_once_rewrite_tac [EQ_SYM_EQ] >>
-  irule fix_fuel_mono >> fs [] >>
-  (* Use the "fundamental" property about $LEAST *)
-  qspec_assume ‘fix_fuel_P f x’ whileTheory.LEAST_EXISTS_IMP >>
-  (* Prove the premise *)
-  pop_assum sg_premise_tac >- metis_tac [] >> fs [] >>
-  spose_not_then assume_tac >>
-  fs [not_le_eq_gt]
-QED
-
-Theorem fix_fixed_diverges:
-  ∀f. is_valid_fp_body f ⇒ ∀x. ~(∃ n. fix_fuel_P f x n) ⇒ fix f x = f (fix f) x
-Proof
-  rw [fix_def] >>
-  (* Case disjunction on the validity hypothesis *)
-  fs [is_valid_fp_body_def] >>
-  last_x_assum (qspec_assume ‘x’) >>
-  rw []
-  >- (
-    last_assum (qspec_assume ‘SUC n’) >>
-    fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
-    first_assum (qspecl_assume [‘fix f’, ‘fix_fuel n f’]) >>
-    Cases_on ‘f (fix_fuel n f) x’ >> fs []
-  ) >>
-  first_assum (qspec_assume ‘fix f’) >> fs [] >>
-  fs [fix_def] >>
-  (* Case disjunction on the ‘∃n. ...’ *)
-  rw [] >>
-  (* Use the hypothesis that there is no fuel s.t. ... *)
-  last_assum (qspec_assume ‘SUC n’) >>
-  fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
-  first_assum (qspec_assume ‘fix_fuel n f’) >>
-  Cases_on ‘fix_fuel n f y’ >> fs []
-QED
-
-(* TODO: I think we can merge this with the theorem below *)
-Theorem fix_fixed_termination_rec_case_aux:
-  ∀x y n m.
-  is_valid_fp_body f ⇒
-  (∀g. f g x = g y) ⇒
-  fix_fuel_P f x n ⇒
-  fix_fuel_P f y m ⇒
-  fix_fuel n f x = fix_fuel m f y
-Proof
-  rw [] >>
-  Cases_on ‘n’ >- fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
-  pure_asm_rewrite_tac [fix_fuel_def] >>
-  sg ‘fix_fuel_P f y n'’ >- rfs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
-  imp_res_tac fix_fuel_mono_least >>
-  fs []
-QED
-
-Theorem fix_fixed_termination_rec_case:
-  ∀ x y n m.
-  is_valid_fp_body f ⇒
-  (∀g. f g x = g y) ⇒
-  fix_fuel_P f x n ⇒
-  fix_fuel_P f y m ⇒
-  fix_fuel ($LEAST (fix_fuel_P f x)) f x =
-  fix_fuel ($LEAST (fix_fuel_P f y)) f y
-Proof
-  rw [] >>
-  imp_res_tac fix_fuel_mono_least >>
-  irule fix_fixed_termination_rec_case_aux >>
-  fs [] >>
-  (* TODO: factorize *)
-  qspec_assume ‘fix_fuel_P f x’ whileTheory.LEAST_EXISTS_IMP >>
-  pop_assum sg_premise_tac >- metis_tac [] >>
-  qspec_assume ‘fix_fuel_P f y’ whileTheory.LEAST_EXISTS_IMP >>
-  pop_assum sg_premise_tac >- metis_tac [] >>
-  rw []
-QED
-
-Theorem fix_fixed_terminates:
-  ∀f. is_valid_fp_body f ⇒ ∀x n. fix_fuel_P f x n ⇒ fix f x = f (fix f) x
-Proof
-  rpt strip_tac >>
-  (* Case disjunction on the validity hypothesis - we don't want to consume it *)
-  last_assum mp_tac >>
-  pure_rewrite_tac [is_valid_fp_body_def] >> rpt strip_tac >>
-  pop_assum (qspec_assume ‘x’) >>
-  rw []
-  >-( (* No recursive call *)
-    fs [fix_def] >> rw [] >> fs [] >>
-    imp_res_tac fix_fuel_mono_least >>
-    Cases_on ‘$LEAST (fix_fuel_P f x)’ >> fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]
-  ) >>
-  (* There exists a recursive call *)
-  SUBGOAL_THEN “∃m. fix_fuel_P f y m” assume_tac >-(
-    Cases_on ‘n’ >>
-    fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
-    metis_tac []
-  ) >>
-  fs [fix_def] >> rw [] >> fs [] >>
-  irule fix_fixed_termination_rec_case >>
-  fs [] >>
-  metis_tac []
-QED
-
-Theorem fix_fixed_eq:
-  ∀f. is_valid_fp_body f ⇒ ∀x. fix f x = f (fix f) x
-Proof
-  rw [] >>
-  Cases_on ‘∃n. fix_fuel_P f x n’
-  >- (irule fix_fixed_terminates >> metis_tac []) >>
-  irule fix_fixed_diverges >>
-  fs []
-QED  
-
-(* Testing on an example *)
-Datatype:
-  list_t =
-    ListCons 't list_t
-  | ListNil
-End
-
-val nth_body_def = Define ‘
-  nth_body (f : ('t list_t # u32) -> 't result) (x : ('t list_t # u32)) : 't result =
-    let (ls, i) = x in
-    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);
-        f (tl, i0)
-        od
-    | ListNil => Fail Failure
-’
-
-(* TODO: move *)
-Theorem is_valid_suffice:
-  ∃y. ∀g. g x = g y
-Proof
-  metis_tac []
-QED
-
-(* The general proof of is_valid_fp_body *)
-Theorem nth_body_is_valid:
-  is_valid_fp_body nth_body
-Proof
-  pure_rewrite_tac [is_valid_fp_body_def] >>
-  gen_tac >>
-  (* TODO: automate this *)
-  Cases_on ‘x’ >> fs [] >>
-  (* Expand *)
-  fs [nth_body_def, bind_def] >>
-  (* Explore all paths *)
-  Cases_on ‘q’ >> fs [is_valid_suffice] >>
-  Cases_on ‘u32_to_int r = 0’ >> fs [is_valid_suffice] >>
-  Cases_on ‘u32_sub r (int_to_u32 1)’ >> fs [is_valid_suffice]
-QED
-
-val nth_raw_def = Define ‘
-  nth (ls : 't list_t) (i : u32) = fix nth_body (ls, i)
-’
-
-Theorem nth_def:
-  ∀ls i. nth (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 tl i0
-        od
-    | ListNil => Fail Failure
-Proof
-  rpt strip_tac >>
-  (* Expand the raw definition *)
-  pure_rewrite_tac [nth_raw_def] >>
-  (* Use the fixed-point equality *)
-  sg ‘fix nth_body (ls,i) = nth_body (fix nth_body) (ls,i)’
-  >- simp_tac bool_ss [HO_MATCH_MP fix_fixed_eq nth_body_is_valid] >>
-  pure_asm_rewrite_tac [] >>
-  (* Expand the body definition *)
-  qspecl_assume [‘fix nth_body’, ‘(ls, i)’] nth_body_def >>
-  pure_asm_rewrite_tac [LET_THM] >>
-  simp_tac arith_ss []
-QED
-
-val _ = export_theory ()
diff --git a/backends/hol4/divDefProtoTheory.sig b/backends/hol4/divDefProtoTheory.sig
deleted file mode 100644
index e74c2fd4..00000000
--- a/backends/hol4/divDefProtoTheory.sig
+++ /dev/null
@@ -1,220 +0,0 @@
-signature divDefProtoTheory =
-sig
-  type thm = Thm.thm
-  
-  (*  Definitions  *)
-    val fix_def : thm
-    val fix_fuel_P_def : thm
-    val fix_fuel_def : thm
-    val is_valid_fp_body_def : thm
-    val list_t_TY_DEF : thm
-    val list_t_case_def : thm
-    val list_t_size_def : thm
-    val nth_body_def : thm
-  
-  (*  Theorems  *)
-    val datatype_list_t : thm
-    val fix_fixed_diverges : thm
-    val fix_fixed_eq : thm
-    val fix_fixed_terminates : thm
-    val fix_fixed_termination_rec_case : thm
-    val fix_fixed_termination_rec_case_aux : thm
-    val fix_fuel_compute : thm
-    val fix_fuel_mono : thm
-    val fix_fuel_mono_least : thm
-    val is_valid_suffice : 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 nth_body_is_valid : thm
-    val nth_def : thm
-  
-  val divDefProto_grammars : type_grammar.grammar * term_grammar.grammar
-(*
-   [primitives] Parent theory of "divDefProto"
-   
-   [fix_def]  Definition
-      
-      ⊢ ∀f x.
-          fix f x =
-          if ∃n. fix_fuel_P f x n then
-            fix_fuel ($LEAST (fix_fuel_P f x)) f x
-          else Diverge
-   
-   [fix_fuel_P_def]  Definition
-      
-      ⊢ ∀f x n. fix_fuel_P f x n ⇔ ¬is_diverge (fix_fuel n f x)
-   
-   [fix_fuel_def]  Definition
-      
-      ⊢ (∀f x. fix_fuel 0 f x = Diverge) ∧
-        ∀n f x. fix_fuel (SUC n) f x = f (fix_fuel n f) x
-   
-   [is_valid_fp_body_def]  Definition
-      
-      ⊢ ∀f. is_valid_fp_body f ⇔
-            ∀x. (∀g h. f g x = f h x) ∨ ∃y. ∀g. f g x = g y
-   
-   [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
-   
-   [nth_body_def]  Definition
-      
-      ⊢ ∀f x.
-          nth_body f x =
-          (let
-             (ls,i) = x
-           in
-             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); f (tl,i0) od
-             | ListNil => Fail Failure)
-   
-   [datatype_list_t]  Theorem
-      
-      ⊢ DATATYPE (list_t ListCons ListNil)
-   
-   [fix_fixed_diverges]  Theorem
-      
-      ⊢ ∀f. is_valid_fp_body f ⇒
-            ∀x. ¬(∃n. fix_fuel_P f x n) ⇒ fix f x = f (fix f) x
-   
-   [fix_fixed_eq]  Theorem
-      
-      ⊢ ∀f. is_valid_fp_body f ⇒ ∀x. fix f x = f (fix f) x
-   
-   [fix_fixed_terminates]  Theorem
-      
-      ⊢ ∀f. is_valid_fp_body f ⇒
-            ∀x n. fix_fuel_P f x n ⇒ fix f x = f (fix f) x
-   
-   [fix_fixed_termination_rec_case]  Theorem
-      
-      ⊢ ∀x y n m.
-          is_valid_fp_body f ⇒
-          (∀g. f g x = g y) ⇒
-          fix_fuel_P f x n ⇒
-          fix_fuel_P f y m ⇒
-          fix_fuel ($LEAST (fix_fuel_P f x)) f x =
-          fix_fuel ($LEAST (fix_fuel_P f y)) f y
-   
-   [fix_fixed_termination_rec_case_aux]  Theorem
-      
-      ⊢ ∀x y n m.
-          is_valid_fp_body f ⇒
-          (∀g. f g x = g y) ⇒
-          fix_fuel_P f x n ⇒
-          fix_fuel_P f y m ⇒
-          fix_fuel n f x = fix_fuel m f y
-   
-   [fix_fuel_compute]  Theorem
-      
-      ⊢ (∀f x. fix_fuel 0 f x = Diverge) ∧
-        (∀n f x.
-           fix_fuel (NUMERAL (BIT1 n)) f x =
-           f (fix_fuel (NUMERAL (BIT1 n) − 1) f) x) ∧
-        ∀n f x.
-          fix_fuel (NUMERAL (BIT2 n)) f x =
-          f (fix_fuel (NUMERAL (BIT1 n)) f) x
-   
-   [fix_fuel_mono]  Theorem
-      
-      ⊢ ∀f. is_valid_fp_body f ⇒
-            ∀n x.
-              fix_fuel_P f x n ⇒
-              ∀m. n ≤ m ⇒ fix_fuel n f x = fix_fuel m f x
-   
-   [fix_fuel_mono_least]  Theorem
-      
-      ⊢ ∀f. is_valid_fp_body f ⇒
-            ∀n x.
-              fix_fuel_P f x n ⇒
-              fix_fuel n f x = fix_fuel ($LEAST (fix_fuel_P f x)) f x
-   
-   [is_valid_suffice]  Theorem
-      
-      ⊢ ∃y. ∀g. g x = g y
-   
-   [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
-   
-   [nth_body_is_valid]  Theorem
-      
-      ⊢ is_valid_fp_body nth_body
-   
-   [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
-   
-   
-*)
-end
diff --git a/backends/hol4/divDefProto2Script.sml b/backends/hol4/divDefScript.sml
index 9efe835b..c742fb1f 100644
--- a/backends/hol4/divDefProto2Script.sml
+++ b/backends/hol4/divDefScript.sml
@@ -1,4 +1,11 @@
-(* Prototype: divDefLib but with general combinators *)
+(* This file introduces a fixed-point operator to define potentially diverging
+   functions so that the user doesn't have to prove termination at *definition time*
+   but can prove it in an extrinsic manner.
+
+   See divDefLib for a library which uses this fixed-point operator in an automated
+   manner, and divDefExampleScript for hand-written and well commented examples of
+   how to use it.
+ *)
 
 open HolKernel boolLib bossLib Parse
 open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
@@ -6,27 +13,34 @@ open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
 open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
 open primitivesLib
 
-val _ = new_theory "divDefProto2"
+val _ = new_theory "divDef"
 
-(*
- * Test with a general validity predicate.
- *
- * TODO: this works! Cleanup.
- *)
+(*======================
+ * Fixed-point operator
+ *======================*)
+
+(* An auxiliary operator which uses some fuel *)
 val fix_fuel_def = Define ‘
   (fix_fuel (0 : num) (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = Diverge) ∧
   (fix_fuel (SUC n) (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = f (fix_fuel n f) x)
 ’
 
+(* An auxiliary predicate *)
 val fix_fuel_P_def = Define ‘
   fix_fuel_P f x n = ~(is_diverge (fix_fuel n f x))
 ’
 
+(* The fixed point operator *)
 val fix_def = Define ‘
   fix (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result =
     if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge
 ’
 
+(* A validity condition.
+
+   If a function body ‘f’ satisfies this condition, then we have the fixed point
+   equation ‘fix f = f (fix f)’ (see [fix_fixed_eq]).
+ *)
 val is_valid_fp_body_def = Define ‘
   (is_valid_fp_body (0 : num) (f : ('a -> 'a result) -> 'a -> 'a result) = F) ∧
   
@@ -35,9 +49,11 @@ val is_valid_fp_body_def = Define ‘
          (∃ h y. is_valid_fp_body n h ∧
                   ∀g. f g x = do z <- g y; h g z od))
 ’
-
+(*======================
+ * Lemmas
+ *======================*)
 (* Auxiliary lemma.
-   We generalize the goal of fix_fuel_mono in the case the fuel is non-empty
+   We generalize the goal of [fix_fuel_mono] in the case the fuel is non-empty
    (this allows us to unfold definitions like ‘fix_fuel’ once, and reveal
    a first intermediate function).
 
@@ -93,6 +109,7 @@ Proof
   gvs []
 QED
 
+(* ‘fix_fuel’ is monotonous over the fuel *)
 Theorem fix_fuel_mono:
   ∀N f. is_valid_fp_body N f ⇒
     ∀n x. fix_fuel_P f x n ⇒
@@ -108,7 +125,6 @@ Proof
   gvs [fix_fuel_def]
 QED
 
-(* TODO: remove? *)
 Theorem fix_fuel_mono_least:
   ∀N f. is_valid_fp_body N f ⇒
     ∀n x. fix_fuel_P f x n ⇒
@@ -149,7 +165,11 @@ Proof
   rw []
 QED
 
-(* If ‘g (fix f) x’ doesn't diverge, we can exhibit some fuel *)
+(* If ‘g (fix f) x’ doesn't diverge, we can write it in terms of ‘g (fix_fuel n f)’
+   for some fuel ‘n’.
+
+   This is an auxiliary lemma used to prove [fix_not_diverge_implies_fix_fuel]
+ *)
 Theorem fix_not_diverge_implies_fix_fuel_aux:
   ∀N M g f. is_valid_fp_body M f ⇒
     is_valid_fp_body N g ⇒
@@ -215,7 +235,8 @@ Proof
   first_x_assum (fn th => assume_tac (GSYM th)) >> fs []
 QED
 
-(* If ‘g (fix f) x’ doesn't diverge, we can exhibit some fuel *)
+(* If ‘g (fix f) x’ doesn't diverge, we can write it in terms of ‘g (fix_fuel n f)’
+   for some fuel ‘n’. *)
 Theorem fix_not_diverge_implies_fix_fuel:
   ∀N f. is_valid_fp_body N f ⇒
      ∀x. f (fix f) x ≠ Diverge ⇒
@@ -224,6 +245,7 @@ Proof
   metis_tac [fix_not_diverge_implies_fix_fuel_aux]
 QED    
 
+(* ‘fix’ satisfies the fixed point equation in case the evaluation diverges *)
 Theorem fix_fixed_diverges:
   ∀N f. is_valid_fp_body N f ⇒ ∀x. ~(∃ n. fix_fuel_P f x n) ⇒ fix f x = f (fix f) x
 Proof
@@ -272,6 +294,7 @@ Proof
   metis_tac [fix_fuel_not_diverge_eq_fix_aux]
 QED
 
+(* ‘fix’ satisfies the fixed point equation in case the evaluation terminates *)
 Theorem fix_fixed_terminates:
   ∀N f. is_valid_fp_body N f ⇒ ∀x n. fix_fuel_P f x n ⇒ fix f x = f (fix f) x
 Proof
@@ -287,6 +310,7 @@ Proof
   Cases_on ‘f (fix_fuel n'' f) x’ >> fs [] >> metis_tac []
 QED
 
+(* The final fixed point equation *)
 Theorem fix_fixed_eq:
   ∀N f. is_valid_fp_body N f ⇒ ∀x. fix f x = f (fix f) x
 Proof
@@ -295,272 +319,33 @@ Proof
   >- (irule fix_fixed_terminates >> metis_tac []) >>
   irule fix_fixed_diverges >>
   metis_tac []
-QED  
-
-(*======================
- * Example 1: nth
- *======================*)
-Datatype:
-  list_t =
-    ListCons 't list_t
-  | ListNil
-End
-
-(* We use this version of the body to prove that the body is valid *)
-val nth_body_def = Define ‘
-  nth_body (f : (('t list_t # u32) + 't) -> (('t list_t # u32) + 't) result)
-    (x : (('t list_t # u32) + 't)) :
-    (('t list_t # u32) + 't) result =
-    (* Destruct the input. We need this to call the proper function in case
-       of mutually recursive definitions, but also to eliminate arguments
-       which correspond to the output value (the input type is the same
-       as the output type). *)
-    case x of
-    | INL x => (
-      let (ls, i) = x in
-      case ls of
-      | ListCons x tl =>
-        if u32_to_int i = (0:int)
-        then Return (INR x)
-        else
-          do
-          i0 <- u32_sub i (int_to_u32 1);
-          r <- f (INL (tl, i0));
-          (* Eliminate the invalid outputs. This is not necessary here,
-             but it is in the case of non tail call recursive calls. *)
-          case r of
-          | INL _ => Fail Failure
-          | INR i1 => Return (INR i1)
-          od
-      | ListNil => Fail Failure)
-    | INR _ => Fail Failure
-’
-
-(* We first prove the theorem with ‘SUC (SUC n)’ where ‘n’ is a variable
-   to prevent this quantity from being rewritten to 2 *)
-Theorem nth_body_is_valid_aux:
-  is_valid_fp_body (SUC (SUC n)) nth_body
-Proof
-  pure_once_rewrite_tac [is_valid_fp_body_def] >>
-  gen_tac >>
-  (* TODO: automate this *)
-  Cases_on ‘x’ >> fs [] >>
-  (* Expand *)
-  fs [nth_body_def, bind_def] >>
-  (* Explore all paths *)
-  Cases_on ‘x'’ >> fs [] >>
-  Cases_on ‘q’ >> fs [] >>
-  Cases_on ‘u32_to_int r = 0’ >> fs [] >>
-  Cases_on ‘u32_sub r (int_to_u32 1)’ >> fs [] >>
-  disj2_tac >>
-  (* This is hard *)
-  qexists ‘\g x. case x of | INL _ => Fail Failure | INR i1 => Return (INR i1)’ >>
-  qexists ‘INL (l, a)’ >>
-  conj_tac
-  >-(
-    (* Prove that the body of h is valid *)
-    pure_once_rewrite_tac [is_valid_fp_body_def] >>
-    (* *)
-    fs []) >>
-  gen_tac >>
-  (* Explore all paths *)
-  Cases_on ‘g (INL (l,a))’ >> fs [] >>
-  Cases_on ‘a'’ >> fs []
-QED
-
-Theorem nth_body_is_valid:
-  is_valid_fp_body (SUC (SUC 0)) nth_body
-Proof
-  irule nth_body_is_valid_aux
 QED
 
-val nth_raw_def = Define ‘
-  nth (ls : 't list_t) (i : u32) =
-    case fix nth_body (INL (ls, i)) of
-    | Fail e => Fail e
-    | Diverge => Diverge
-    | Return r =>
-      case r of
-      | INL _ => Fail Failure
-      | INR x => Return x
-’
-
-(* Rewrite the goal once, and on the left part of the goal seen as an application *)
-fun pure_once_rewrite_left_tac ths =
-  CONV_TAC (PATH_CONV "l" (PURE_ONCE_REWRITE_CONV ths))
+(*===============================
+ * Utilities for the automation
+ *===============================*)
 
-Theorem nth_def:
-  ∀ls i. nth (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 tl i0
-        od
-    | ListNil => Fail Failure
-Proof
-  rpt strip_tac >>
-  (* Expand the raw definition *)
-  pure_rewrite_tac [nth_raw_def] >>
-  (* Use the fixed-point equality - the rewrite must only be applied *on the left* of the equality, in the goal *)
-  pure_once_rewrite_left_tac [HO_MATCH_MP fix_fixed_eq nth_body_is_valid] >>
-  (* Expand the body definition *)
-  pure_rewrite_tac [nth_body_def] >>
-  (* Explore all the paths - maybe we can be smarter, but this is fast and really easy *)
-  fs [bind_def] >>
-  Cases_on ‘ls’ >> fs [] >>
-  Cases_on ‘u32_to_int i = 0’ >> fs [] >>
-  Cases_on ‘u32_sub i (int_to_u32 1)’ >> fs [] >>
-  Cases_on ‘fix nth_body (INL (l,a))’ >> fs [] >>
-  Cases_on ‘a'’ >> fs []
-QED
-
-(*======================
- * Example 2: even, odd
- *======================*)
+(* This theorem is important to shape the goal when proving that a body
+   satifies the fixed point validity property.
 
-val even_odd_body_def = Define ‘
-  even_odd_body
-    (f : (int + int + bool) -> (int + int + bool) result)
-    (x : int + int + bool) : (int + int + bool) result =
-    case x of
-    | INL i =>
-      (* Even *)
-      if i = 0 then Return (INR (INR T))
-      else
-        (case f (INR (INL (i - 1))) of
-         | Fail e => Fail e
-         | Diverge => Diverge
-         | Return r =>
-           (* Eliminate the unwanted results *)
-           case r of
-           | INL _ => Fail Failure
-           | INR (INL _) => Fail Failure
-           | INR (INR b) => Return (INR (INR b))
-           )
-    | INR x =>
-      case x of
-      | INL i =>
-        (* Odd *)
-        if i = 0 then Return (INR (INR F))
-        else
-          (case f (INL (i - 1)) of
-           | Fail e => Fail e
-           | Diverge => Diverge
-           | Return r =>
-             (* Eliminate the unwanted results *)
-             case r of
-             | INL _ => Fail Failure
-             | INR (INL _) => Fail Failure
-             | INR (INR b) => Return (INR (INR b))
-             )
-      | INR _ =>
-        (* This case is for the return value *)
-        Fail Failure
-’
-
-Theorem even_odd_body_is_valid_aux:
-  is_valid_fp_body (SUC (SUC n)) even_odd_body
+   Important: this theorem (and its usafe) relies on the fact that errors are just
+   transmitted to the caller (in particular, without modification).
+ *)
+Theorem case_result_switch_eq:
+  (case (case x of Return y => f y | Fail e => Fail e | Diverge => Diverge) of
+  | Return y => g y
+  | Fail e => Fail e
+  | Diverge => Diverge) =
+  (case x of
+   | Return y =>
+     (case f y of
+     | Return y => g y
+     | Fail e => Fail e
+     | Diverge => Diverge)
+  | Fail e => Fail e
+  | Diverge => Diverge)
 Proof
-  pure_once_rewrite_tac [is_valid_fp_body_def] >>
-  gen_tac >>
-  (* Expand *)
-  fs [even_odd_body_def, bind_def] >>
-  (* TODO: automate this *)
   Cases_on ‘x’ >> fs []
-  >-(
-    Cases_on ‘x' = 0’ >> fs [] >>
-    (* Recursive call *)
-    disj2_tac >>
-    qexists ‘\g x. case x of | INL _ => Fail Failure | INR (INL _) => Fail Failure | INR (INR i1) => Return (INR (INR i1))’ >>
-    qexists ‘INR (INL (x' − 1))’ >>
-    conj_tac
-    >-(pure_once_rewrite_tac [is_valid_fp_body_def] >> fs []) >>
-    fs []) >>
-  Cases_on ‘y’ >> fs []  >>
-  Cases_on ‘x = 0’ >> fs []  >>
-  (* Recursive call *)
-  disj2_tac >>
-  qexists ‘\g x. case x of | INL _ => Fail Failure | INR (INL _) => Fail Failure | INR (INR i1) => Return (INR (INR i1))’ >>
-  qexists ‘INL (x − 1)’ >>
-  conj_tac
-  >-(pure_once_rewrite_tac [is_valid_fp_body_def] >> fs []) >>
-  fs []
-QED
-
-Theorem even_odd_body_is_valid:
-  is_valid_fp_body (SUC (SUC 0)) even_odd_body
-Proof
-  irule even_odd_body_is_valid_aux
-QED
-
-val even_raw_def = Define ‘
-  even (i : int) =
-    case fix even_odd_body (INL i) of
-    | Fail e => Fail e
-    | Diverge => Diverge
-    | Return r =>
-      case r of
-      | INL _ => Fail Failure
-      | INR (INL _) => Fail Failure
-      | INR (INR b) => Return b
-’
-
-val odd_raw_def = Define ‘
-  odd (i : int) =
-    case fix even_odd_body (INR (INL i)) of
-    | Fail e => Fail e
-    | Diverge => Diverge
-    | Return r =>
-      case r of
-      | INL _ => Fail Failure
-      | INR (INL _) => Fail Failure
-      | INR (INR b) => Return b
-’
-
-Theorem even_def:
-  ∀i. even (i : int) : bool result =
-    if i = 0 then Return T else odd (i - 1)
-Proof
-  gen_tac >>
-  (* Expand the definition *)
-  pure_once_rewrite_tac [even_raw_def] >>
-  (* Use the fixed-point equality *)
-  pure_once_rewrite_left_tac [HO_MATCH_MP fix_fixed_eq even_odd_body_is_valid] >>
-  (* Expand the body definition *)
-  pure_rewrite_tac [even_odd_body_def] >>
-  (* Expand all the definitions from the group *)
-  pure_rewrite_tac [even_raw_def, odd_raw_def] >>
-  (* Explore all the paths - maybe we can be smarter, but this is fast and really easy *)
-  fs [bind_def] >>
-  Cases_on ‘i = 0’ >> fs [] >>
-  Cases_on ‘fix even_odd_body (INR (INL (i − 1)))’ >> fs [] >>
-  Cases_on ‘a’ >> fs [] >>
-  Cases_on ‘y’ >> fs []
-QED
-
-Theorem odd_def:
-  ∀i. odd (i : int) : bool result =
-    if i = 0 then Return F else even (i - 1)
-Proof
-  gen_tac >>
-  (* Expand the definition *)
-  pure_once_rewrite_tac [odd_raw_def] >>
-  (* Use the fixed-point equality *)
-  pure_once_rewrite_left_tac [HO_MATCH_MP fix_fixed_eq even_odd_body_is_valid] >>
-  (* Expand the body definition *)
-  pure_rewrite_tac [even_odd_body_def] >>
-  (* Expand all the definitions from the group *)
-  pure_rewrite_tac [even_raw_def, odd_raw_def] >>
-  (* Explore all the paths - maybe we can be smarter, but this is fast and really easy *)
-  fs [bind_def] >>
-  Cases_on ‘i = 0’ >> fs [] >>
-  Cases_on ‘fix even_odd_body (INL (i − 1))’ >> fs [] >>
-  Cases_on ‘a’ >> fs [] >>
-  Cases_on ‘y’ >> fs []
 QED
 
 val _ = export_theory ()
diff --git a/backends/hol4/divDefTheory.sig b/backends/hol4/divDefTheory.sig
new file mode 100644
index 00000000..15592052
--- /dev/null
+++ b/backends/hol4/divDefTheory.sig
@@ -0,0 +1,187 @@
+signature divDefTheory =
+sig
+  type thm = Thm.thm
+  
+  (*  Definitions  *)
+    val fix_def : thm
+    val fix_fuel_P_def : thm
+    val fix_fuel_def : thm
+    val is_valid_fp_body_def : thm
+  
+  (*  Theorems  *)
+    val case_result_switch_eq : thm
+    val fix_fixed_diverges : thm
+    val fix_fixed_eq : thm
+    val fix_fixed_terminates : thm
+    val fix_fuel_P_least : thm
+    val fix_fuel_compute : thm
+    val fix_fuel_eq_fix : thm
+    val fix_fuel_mono : thm
+    val fix_fuel_mono_aux : thm
+    val fix_fuel_mono_least : thm
+    val fix_fuel_not_diverge_eq_fix : thm
+    val fix_fuel_not_diverge_eq_fix_aux : thm
+    val fix_not_diverge_implies_fix_fuel : thm
+    val fix_not_diverge_implies_fix_fuel_aux : thm
+    val is_valid_fp_body_compute : thm
+  
+  val divDef_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+   [primitives] Parent theory of "divDef"
+   
+   [fix_def]  Definition
+      
+      ⊢ ∀f x.
+          fix f x =
+          if ∃n. fix_fuel_P f x n then
+            fix_fuel ($LEAST (fix_fuel_P f x)) f x
+          else Diverge
+   
+   [fix_fuel_P_def]  Definition
+      
+      ⊢ ∀f x n. fix_fuel_P f x n ⇔ ¬is_diverge (fix_fuel n f x)
+   
+   [fix_fuel_def]  Definition
+      
+      ⊢ (∀f x. fix_fuel 0 f x = Diverge) ∧
+        ∀n f x. fix_fuel (SUC n) f x = f (fix_fuel n f) x
+   
+   [is_valid_fp_body_def]  Definition
+      
+      ⊢ (∀f. is_valid_fp_body 0 f ⇔ F) ∧
+        ∀n f.
+          is_valid_fp_body (SUC n) f ⇔
+          ∀x. (∀g h. f g x = f h x) ∨
+              ∃h y.
+                is_valid_fp_body n h ∧ ∀g. f g x = do z <- g y; h g z od
+   
+   [case_result_switch_eq]  Theorem
+      
+      ⊢ (case
+           case x of
+             Return y => f y
+           | Fail e => Fail e
+           | Diverge => Diverge
+         of
+           Return y => g y
+         | Fail e => Fail e
+         | Diverge => Diverge) =
+        case x of
+          Return y =>
+            (case f y of
+               Return y => g y
+             | Fail e => Fail e
+             | Diverge => Diverge)
+        | Fail e => Fail e
+        | Diverge => Diverge
+   
+   [fix_fixed_diverges]  Theorem
+      
+      ⊢ ∀N f.
+          is_valid_fp_body N f ⇒
+          ∀x. ¬(∃n. fix_fuel_P f x n) ⇒ fix f x = f (fix f) x
+   
+   [fix_fixed_eq]  Theorem
+      
+      ⊢ ∀N f. is_valid_fp_body N f ⇒ ∀x. fix f x = f (fix f) x
+   
+   [fix_fixed_terminates]  Theorem
+      
+      ⊢ ∀N f.
+          is_valid_fp_body N f ⇒
+          ∀x n. fix_fuel_P f x n ⇒ fix f x = f (fix f) x
+   
+   [fix_fuel_P_least]  Theorem
+      
+      ⊢ ∀f n x.
+          fix_fuel n f x ≠ Diverge ⇒
+          fix_fuel_P f x ($LEAST (fix_fuel_P f x))
+   
+   [fix_fuel_compute]  Theorem
+      
+      ⊢ (∀f x. fix_fuel 0 f x = Diverge) ∧
+        (∀n f x.
+           fix_fuel (NUMERAL (BIT1 n)) f x =
+           f (fix_fuel (NUMERAL (BIT1 n) − 1) f) x) ∧
+        ∀n f x.
+          fix_fuel (NUMERAL (BIT2 n)) f x =
+          f (fix_fuel (NUMERAL (BIT1 n)) f) x
+   
+   [fix_fuel_eq_fix]  Theorem
+      
+      ⊢ ∀N f.
+          is_valid_fp_body N f ⇒
+          ∀n x. fix_fuel_P f x n ⇒ fix_fuel n f x = fix f x
+   
+   [fix_fuel_mono]  Theorem
+      
+      ⊢ ∀N f.
+          is_valid_fp_body N f ⇒
+          ∀n x.
+            fix_fuel_P f x n ⇒ ∀m. n ≤ m ⇒ fix_fuel n f x = fix_fuel m f x
+   
+   [fix_fuel_mono_aux]  Theorem
+      
+      ⊢ ∀n N M g f.
+          is_valid_fp_body M f ⇒
+          is_valid_fp_body N g ⇒
+          ∀x. ¬is_diverge (g (fix_fuel n f) x) ⇒
+              ∀m. n ≤ m ⇒ g (fix_fuel n f) x = g (fix_fuel m f) x
+   
+   [fix_fuel_mono_least]  Theorem
+      
+      ⊢ ∀N f.
+          is_valid_fp_body N f ⇒
+          ∀n x.
+            fix_fuel_P f x n ⇒
+            fix_fuel n f x = fix_fuel ($LEAST (fix_fuel_P f x)) f x
+   
+   [fix_fuel_not_diverge_eq_fix]  Theorem
+      
+      ⊢ ∀N f.
+          is_valid_fp_body N f ⇒
+          ∀n x.
+            f (fix_fuel n f) x ≠ Diverge ⇒ f (fix f) x = f (fix_fuel n f) x
+   
+   [fix_fuel_not_diverge_eq_fix_aux]  Theorem
+      
+      ⊢ ∀N M g f.
+          is_valid_fp_body M f ⇒
+          is_valid_fp_body N g ⇒
+          ∀n x.
+            g (fix_fuel n f) x ≠ Diverge ⇒ g (fix f) x = g (fix_fuel n f) x
+   
+   [fix_not_diverge_implies_fix_fuel]  Theorem
+      
+      ⊢ ∀N f.
+          is_valid_fp_body N f ⇒
+          ∀x. f (fix f) x ≠ Diverge ⇒ ∃n. f (fix f) x = f (fix_fuel n f) x
+   
+   [fix_not_diverge_implies_fix_fuel_aux]  Theorem
+      
+      ⊢ ∀N M g f.
+          is_valid_fp_body M f ⇒
+          is_valid_fp_body N g ⇒
+          ∀x. g (fix f) x ≠ Diverge ⇒
+              ∃n. g (fix f) x = g (fix_fuel n f) x ∧
+                  ∀m. n ≤ m ⇒ g (fix_fuel m f) x = g (fix_fuel n f) x
+   
+   [is_valid_fp_body_compute]  Theorem
+      
+      ⊢ (∀f. is_valid_fp_body 0 f ⇔ F) ∧
+        (∀n f.
+           is_valid_fp_body (NUMERAL (BIT1 n)) f ⇔
+           ∀x. (∀g h. f g x = f h x) ∨
+               ∃h y.
+                 is_valid_fp_body (NUMERAL (BIT1 n) − 1) h ∧
+                 ∀g. f g x = do z <- g y; h g z od) ∧
+        ∀n f.
+          is_valid_fp_body (NUMERAL (BIT2 n)) f ⇔
+          ∀x. (∀g h. f g x = f h x) ∨
+              ∃h y.
+                is_valid_fp_body (NUMERAL (BIT1 n)) h ∧
+                ∀g. f g x = do z <- g y; h g z od
+   
+   
+*)
+end