Remove some obsolete files from the HOL4 backend

4 files changed, 0 insertions, 3302 deletions

diff --git a/backends/hol4/testHashmapScript.sml b/backends/hol4/testHashmapScript.sml
deleted file mode 100644
index c3f04cca..00000000
--- a/backends/hol4/testHashmapScript.sml
+++ /dev/null
@@ -1,416 +0,0 @@
-open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
-
-open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
-open primitivesLib
-
-val _ = new_theory "testHashmap"
-
-(*
- * Examples of proofs
- *)
-
-Datatype:
-  list_t =
-    ListCons 't list_t
-  | ListNil
-End
-
-val nth_mut_fwd_def = Define ‘
-  nth_mut_fwd (ls : 't list_t) (i : u32) : 't result =
-  case ls of
-  | ListCons x tl =>
-    if u32_to_int i = (0:int)
-    then Return x
-    else
-      do
-      i0 <- u32_sub i (int_to_u32 1);
-      nth_mut_fwd tl i0
-      od
-  | ListNil => 
-    Fail Failure
-’
-                                            
-(*** Examples of proofs on [nth] *)
-val list_t_v_def = Define ‘
-  list_t_v ListNil = [] /\
-  list_t_v (ListCons x tl) = x :: list_t_v tl
-’
-
-Theorem nth_mut_fwd_spec:
-  !(ls : 't list_t) (i : u32).
-    u32_to_int i < len (list_t_v ls) ==>
-    case nth_mut_fwd ls i of
-    | Return x => x = index (u32_to_int i) (list_t_v ls)
-    | Fail _ => F
-    | Diverge => F
-Proof
-  Induct_on ‘ls’ >> rw [list_t_v_def, len_def] >~ [‘ListNil’]
-  >-(massage >> int_tac) >>
-  pure_once_rewrite_tac [nth_mut_fwd_def] >> rw [] >>
-  fs [index_eq] >>
-  progress >> progress
-QED
-
-val _ = save_spec_thm "nth_mut_fwd_spec"
-
-val _ = new_constant ("insert", “: u32 -> 't -> (u32 # 't) list_t -> (u32 # 't) list_t result”)
-val insert_def = new_axiom ("insert_def", “
- insert (key : u32) (value : 't) (ls : (u32 # 't) list_t) : (u32 # 't) list_t result =
-  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)
- ”)
-
-(* Property that keys are pairwise distinct *)
-val distinct_keys_def = Define ‘
-  distinct_keys (ls : (u32 # 't) list) =
-    !i j.
-      0 ≤ i ⇒ i < j ⇒ j < len ls ⇒
-      FST (index i ls) ≠ FST (index j ls)
-’
-
-val lookup_raw_def = Define ‘
-  lookup_raw key [] = NONE /\
-  lookup_raw key ((k, v) :: ls) =
-    if k = key then SOME v else lookup_raw key ls
-’
-
-val lookup_def = Define ‘
-  lookup key ls = lookup_raw key (list_t_v ls)
-’
-
-(* Lemma about ‘insert’, without the invariant *)
-Theorem insert_lem_aux:
-  !ls key value.
-    (* The keys are pairwise distinct *)
-    case insert key value ls of
-    | Return ls1 =>
-      (* We updated the binding *)
-      lookup key ls1 = SOME value /\
-      (* The other bindings are left unchanged *)
-      (!k. k <> key ==> lookup k ls = lookup k ls1)
-    | Fail _ => F
-    | Diverge => F
-Proof
-  Induct_on ‘ls’ >> rw [list_t_v_def] >~ [‘ListNil’] >>
-  pure_once_rewrite_tac [insert_def] >> rw []
-  >- (rw [lookup_def, lookup_raw_def, list_t_v_def])
-  >- (rw [lookup_def, lookup_raw_def, list_t_v_def]) >>
-  case_tac >> rw []
-  >- (rw [lookup_def, lookup_raw_def, list_t_v_def])
-  >- (rw [lookup_def, lookup_raw_def, list_t_v_def]) >>
-  progress >>
-  fs [lookup_def, lookup_raw_def, list_t_v_def]
-QED
-
-(*
- * Invariant proof 1
- *)
-
-Theorem distinct_keys_cons:
-  ∀ k v ls.
-  (∀ i. 0 ≤ i ⇒ i < len ls ⇒ FST (index i ls) ≠ k) ⇒
-  distinct_keys ls ⇒
-  distinct_keys ((k,v) :: ls)
-Proof
-  rw [] >>
-  rw [distinct_keys_def] >>
-  Cases_on ‘i = 0’ >> fs []
-  >-(
-    (* Use the first hypothesis *)
-    fs [index_eq] >>
-    last_x_assum (qspecl_assume [‘j - 1’]) >>
-    sg ‘0 ≤ j - 1’ >- int_tac >>
-    fs [len_def] >>
-    sg ‘j - 1 < len ls’ >- int_tac >>
-    fs []
-  ) >>
-  (* Use the second hypothesis *)
-  sg ‘0 < i’ >- int_tac >>
-  sg ‘0 < j’ >- int_tac >>
-  fs [distinct_keys_def, index_eq, len_def] >>
-  first_x_assum (qspecl_assume [‘i - 1’, ‘j - 1’]) >>
-  sg ‘0 ≤ i - 1 ∧ i - 1 < j - 1 ∧ j - 1 < len ls’ >- int_tac >>
-  fs []
-QED
-
-Theorem distinct_keys_tail:
-  ∀ k v ls.
-  distinct_keys ((k,v) :: ls) ⇒
-  distinct_keys ls
-Proof
-  rw [distinct_keys_def] >>
-  last_x_assum (qspecl_assume [‘i + 1’, ‘j + 1’]) >>
-  fs [len_def] >>
-  sg ‘0 ≤ i + 1 ∧ i + 1 < j + 1 ∧ j + 1 < 1 + len ls’ >- int_tac >> fs [] >>
-  sg ‘0 < i + 1 ∧ 0 < j + 1’ >- int_tac >> fs [index_eq] >>
-  sg ‘i + 1 - 1 = i ∧ j + 1 - 1 = j’ >- int_tac >> fs []
-QED
-
-Theorem insert_index_neq:
-  ∀ q k v ls0 ls1 i.
-  (∀ j. 0 ≤ j ∧ j < len (list_t_v ls0) ⇒ q ≠ FST (index j (list_t_v ls0))) ⇒
-  q ≠ k ⇒
-  insert k v ls0 = Return ls1 ⇒
-  0 ≤ i ⇒
-  i < len (list_t_v ls1) ⇒
-  FST (index i (list_t_v ls1)) ≠ q
-Proof
-  ntac 3 strip_tac >>
-  Induct_on ‘ls0’ >> rw [] >~ [‘ListNil’]
-  >-(
-    fs [insert_def] >>
-    sg ‘ls1 = ListCons (k,v) ListNil’ >- fs [] >> fs [list_t_v_def, len_def] >>
-    sg ‘i = 0’ >- int_tac >> fs [index_eq]) >>
-  Cases_on ‘t’ >>
-  Cases_on ‘i = 0’ >> fs []
-  >-(
-    qpat_x_assum ‘insert _ _ _ = _’ mp_tac >>
-    simp [MK_BOUNDED insert_def 1, bind_def] >>
-    Cases_on ‘q' = k’ >> rw []
-    >- (fs [list_t_v_def, index_eq]) >>
-    Cases_on ‘insert k v ls0’ >> fs [] >>
-    gvs [list_t_v_def, index_eq] >>
-    first_x_assum (qspec_assume ‘0’) >>
-    fs [len_def] >>
-    strip_tac >>
-    qspec_assume ‘list_t_v ls0’ len_pos >>
-    sg ‘0 < 1 + len (list_t_v ls0)’ >- int_tac >>
-    fs []) >>
-  qpat_x_assum ‘insert _ _ _ = _’ mp_tac >>
-  simp [MK_BOUNDED insert_def 1, bind_def] >>
-  Cases_on ‘q' = k’ >> rw []
-  >-(
-    fs [list_t_v_def, index_eq, len_def] >>
-    first_x_assum (qspec_assume ‘i’) >> rfs []) >>
-  Cases_on ‘insert k v ls0’ >> fs [] >>
-  gvs [list_t_v_def, index_eq] >>
-  last_x_assum (qspec_assume ‘i - 1’) >>
-  fs [len_def] >>
-  sg ‘0 ≤ i - 1 ∧ i - 1 < len (list_t_v a)’ >- int_tac >> fs [] >>
-  first_x_assum irule >>
-  rw [] >>
-  last_x_assum (qspec_assume ‘j + 1’) >>
-  rfs [] >>
-  sg ‘j + 1 < 1 + len (list_t_v ls0) ∧ j + 1 − 1 = j ∧ j + 1 ≠ 0’ >- int_tac >> fs []
-QED
-
-Theorem distinct_keys_insert_index_neq:
-  ∀ k v q r ls0 ls1 i.
-  distinct_keys ((q,r)::list_t_v ls0) ⇒
-  q ≠ k ⇒
-  insert k v ls0 = Return ls1 ⇒
-  0 ≤ i ⇒
-  i < len (list_t_v ls1) ⇒
-  FST (index i (list_t_v ls1)) ≠ q
-Proof
-  rw [] >>
-  (* Use the first assumption to prove the following assertion *)
-  sg ‘∀ j. 0 ≤ j ∧ j < len (list_t_v ls0) ⇒ q ≠ FST (index j (list_t_v ls0))’
-  >-(
-    strip_tac >>
-    fs [distinct_keys_def] >>
-    last_x_assum (qspecl_assume [‘0’, ‘j + 1’]) >>
-    fs [index_eq] >>
-    sg ‘j + 1 - 1 = j’ >- int_tac >> fs [len_def] >>
-    rw []>>
-    first_x_assum irule >> int_tac) >>
-  qspecl_assume [‘q’, ‘k’, ‘v’, ‘ls0’, ‘ls1’, ‘i’] insert_index_neq >>
-  fs []
-QED
-
-Theorem distinct_keys_insert:
-  ∀ k v ls0 ls1.
-  distinct_keys (list_t_v ls0) ⇒
-  insert k v ls0 = Return ls1 ⇒
-  distinct_keys (list_t_v ls1)
-Proof
-  Induct_on ‘ls0’ >~ [‘ListNil’]
-  >-(
-    rw [distinct_keys_def, list_t_v_def, insert_def] >>
-    fs [list_t_v_def, len_def] >>
-    int_tac) >>  
-  Cases >>
-  pure_once_rewrite_tac [insert_def] >> fs[] >>
-  rw [] >> fs []
-  >-(
-    (* k = q *)
-    last_x_assum ignore_tac >>
-    fs [distinct_keys_def] >>
-    rw [] >>
-    last_x_assum (qspecl_assume [‘i’, ‘j’]) >>
-    rfs [list_t_v_def, len_def] >>
-    sg ‘0 < j’ >- int_tac >>
-    Cases_on ‘i = 0’ >> gvs [index_eq]) >>
-  (* k ≠ q: recursion *)
-  Cases_on ‘insert k v ls0’ >> fs [bind_def] >>
-  last_x_assum (qspecl_assume [‘k’, ‘v’, ‘a’]) >>
-  gvs [list_t_v_def] >>
-  imp_res_tac distinct_keys_tail >> fs [] >>
-  irule distinct_keys_cons >> rw [] >>
-  metis_tac [distinct_keys_insert_index_neq]
-QED  
-
-Theorem insert_lem:
-  !ls key value.
-    (* The keys are pairwise distinct *)
-    distinct_keys (list_t_v ls) ==>
-    case insert key value ls of
-    | Return ls1 =>
-      (* We updated the binding *)
-      lookup key ls1 = SOME value /\
-      (* The other bindings are left unchanged *)
-      (!k. k <> key ==> lookup k ls = lookup k ls1) ∧
-      (* The keys are still pairwise disjoint *)
-      distinct_keys (list_t_v ls1)
-    | Fail _ => F
-    | Diverge => F
-Proof
-  rw [] >>
-  qspecl_assume [‘ls’, ‘key’, ‘value’] insert_lem_aux >>
-  case_tac >> fs [] >>
-  metis_tac [distinct_keys_insert]
-QED
-
-(*
- * Invariant proof 2: functional version of the invariant
- *)
-val for_all_def = Define ‘
-  for_all p [] = T ∧
-  for_all p (x :: ls) = (p x ∧ for_all p ls)
-’
-
-val pairwise_rel_def = Define ‘
-  pairwise_rel p [] = T ∧
-  pairwise_rel p (x :: ls) = (for_all (p x) ls ∧ pairwise_rel p ls)
-’
-
-val distinct_keys_f_def = Define ‘
-  distinct_keys_f (ls : (u32 # 't) list) =
-    pairwise_rel (\x y. FST x ≠ FST y) ls
-’
-
-Theorem distinct_keys_f_insert_for_all:
-  ∀k v k1 ls0 ls1.
-  k1 ≠ k ⇒
-  for_all (λy. k1 ≠ FST y) (list_t_v ls0) ⇒
-  pairwise_rel (λx y. FST x ≠ FST y) (list_t_v ls0) ⇒
-  insert k v ls0 = Return ls1 ⇒
-  for_all (λy. k1 ≠ FST y) (list_t_v ls1)
-Proof
-  Induct_on ‘ls0’ >> rw [pairwise_rel_def] >~ [‘ListNil’] >>
-  gvs [list_t_v_def, pairwise_rel_def, for_all_def]
-  >-(gvs [MK_BOUNDED insert_def 1, bind_def, list_t_v_def, for_all_def]) >>
-  pat_undisch_tac ‘insert _ _ _ = _’ >>
-  simp [MK_BOUNDED insert_def 1, bind_def] >>
-  Cases_on ‘t’ >> rw [] >> gvs [list_t_v_def, pairwise_rel_def, for_all_def] >>
-  Cases_on ‘insert k v ls0’ >>
-  gvs [distinct_keys_f_def, list_t_v_def, pairwise_rel_def, for_all_def] >>
-  metis_tac []
-QED
-
-Theorem distinct_keys_f_insert:
-  ∀ k v ls0 ls1.
-  distinct_keys_f (list_t_v ls0) ⇒
-  insert k v ls0 = Return ls1 ⇒
-  distinct_keys_f (list_t_v ls1)
-Proof
-  Induct_on ‘ls0’ >> rw [distinct_keys_f_def] >~ [‘ListNil’]
-  >-(
-    fs [list_t_v_def, insert_def] >>
-    gvs [list_t_v_def, pairwise_rel_def, for_all_def]) >>
-  last_x_assum (qspecl_assume [‘k’, ‘v’]) >>
-  pat_undisch_tac ‘insert _ _ _ = _’ >>
-  simp [MK_BOUNDED insert_def 1, bind_def] >>
-  (* TODO: improve case_tac *)
-  Cases_on ‘t’ >> rw [] >> gvs [list_t_v_def, pairwise_rel_def, for_all_def] >>
-  Cases_on ‘insert k v ls0’ >>
-  gvs [distinct_keys_f_def, list_t_v_def, pairwise_rel_def, for_all_def] >>
-  metis_tac [distinct_keys_f_insert_for_all]
-QED
-
-(*
- * Proving equivalence between the two version - exercise.
- *)
-Theorem for_all_quant:
-  ∀p ls. for_all p ls ⇔ ∀i. 0 ≤ i ⇒ i < len ls ⇒ p (index i ls)
-Proof
-  strip_tac >> Induct_on ‘ls’
-  >-(rw [for_all_def, len_def] >> int_tac) >>
-  rw [for_all_def, len_def, index_eq] >>
-  equiv_tac
-  >-(
-    rw [] >>
-    Cases_on ‘i = 0’ >> fs [] >>
-    first_x_assum irule >>
-    int_tac) >>
-  rw []
-  >-(
-    first_x_assum (qspec_assume ‘0’) >> fs [] >>
-    first_x_assum irule >>
-    qspec_assume ‘ls’ len_pos >>
-    int_tac) >>
-  first_x_assum (qspec_assume ‘i + 1’) >>
-  fs [] >>
-  sg ‘i + 1 ≠ 0 ∧ i + 1 - 1 = i’ >- int_tac >> fs [] >>
-  first_x_assum irule >> int_tac
-QED
-
-Theorem pairwise_rel_quant:
-  ∀p ls. pairwise_rel p ls ⇔
-    (∀i j. 0 ≤ i ⇒ i < j ⇒ j < len ls ⇒ p (index i ls) (index j ls))
-Proof
-  strip_tac >> Induct_on ‘ls’
-  >-(rw [pairwise_rel_def, len_def] >> int_tac) >>
-  rw [pairwise_rel_def, len_def] >>
-  equiv_tac
-  >-(
-    (* ==> *)
-    rw [] >>
-    sg ‘0 < j’ >- int_tac >>
-    Cases_on ‘i = 0’
-    >-(
-      simp [index_eq] >>
-      qspecl_assume [‘p h’, ‘ls’] (iffLR for_all_quant) >>
-      first_x_assum irule >> fs [] >> int_tac
-    ) >>
-    rw [index_eq] >>
-    first_x_assum irule >> int_tac
-  ) >>
-  (* <== *)
-  rw []
-  >-(
-    rw [for_all_quant] >>
-    first_x_assum (qspecl_assume [‘0’, ‘i + 1’]) >>
-    sg ‘0 < i + 1 ∧ i + 1 - 1 = i’ >- int_tac >>
-    fs [index_eq] >>
-    first_x_assum irule >> int_tac
-  ) >>
-  sg ‘pairwise_rel p ls’
-  >-(
-    rw [pairwise_rel_def] >>
-    first_x_assum (qspecl_assume [‘i' + 1’, ‘j' + 1’]) >>
-    sg ‘0 < i' + 1 ∧ 0 < j' + 1’ >- int_tac >>
-    fs [index_eq, int_add_minus_same_eq] >>
-    first_x_assum irule >> int_tac
-  ) >>
-  fs []
-QED
-
-Theorem distinct_keys_f_eq_distinct_keys:
-  ∀ ls.
-  distinct_keys_f ls ⇔ distinct_keys ls
-Proof
-  rw [distinct_keys_def, distinct_keys_f_def] >>
-  qspecl_assume [‘(λx y. FST x ≠ FST y)’, ‘ls’] pairwise_rel_quant >>
-  fs []
-QED
-
-val _ = export_theory ()
diff --git a/backends/hol4/testHashmapTheory.sig b/backends/hol4/testHashmapTheory.sig
deleted file mode 100644
index 1d304723..00000000
--- a/backends/hol4/testHashmapTheory.sig
+++ /dev/null
@@ -1,305 +0,0 @@
-signature testHashmapTheory =
-sig
-  type thm = Thm.thm
-  
-  (*  Axioms  *)
-    val insert_def : thm
-  
-  (*  Definitions  *)
-    val distinct_keys_def : thm
-    val distinct_keys_f_def : thm
-    val for_all_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 pairwise_rel_def : thm
-  
-  (*  Theorems  *)
-    val datatype_list_t : thm
-    val distinct_keys_cons : thm
-    val distinct_keys_f_eq_distinct_keys : thm
-    val distinct_keys_f_insert : thm
-    val distinct_keys_f_insert_for_all : thm
-    val distinct_keys_insert : thm
-    val distinct_keys_insert_index_neq : thm
-    val distinct_keys_tail : thm
-    val for_all_quant : thm
-    val insert_index_neq : thm
-    val insert_lem : thm
-    val insert_lem_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 lookup_raw_def : thm
-    val lookup_raw_ind : thm
-    val nth_mut_fwd_def : thm
-    val nth_mut_fwd_ind : thm
-    val nth_mut_fwd_spec : thm
-    val pairwise_rel_quant : thm
-  
-  val testHashmap_grammars : type_grammar.grammar * term_grammar.grammar
-(*
-   [primitives] Parent theory of "testHashmap"
-   
-   [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)
-   
-   [distinct_keys_def]  Definition
-      
-      ⊢ ∀ls.
-          distinct_keys ls ⇔
-          ∀i j.
-            0 ≤ i ⇒
-            i < j ⇒
-            j < len ls ⇒
-            FST (index i ls) ≠ FST (index j ls)
-   
-   [distinct_keys_f_def]  Definition
-      
-      ⊢ ∀ls. distinct_keys_f ls ⇔ pairwise_rel (λx y. FST x ≠ FST y) ls
-   
-   [for_all_def]  Definition
-      
-      ⊢ (∀p. for_all p [] ⇔ T) ∧
-        ∀p x ls. for_all p (x::ls) ⇔ p x ∧ for_all p ls
-   
-   [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)
-   
-   [pairwise_rel_def]  Definition
-      
-      ⊢ (∀p. pairwise_rel p [] ⇔ T) ∧
-        ∀p x ls.
-          pairwise_rel p (x::ls) ⇔ for_all (p x) ls ∧ pairwise_rel p ls
-   
-   [datatype_list_t]  Theorem
-      
-      ⊢ DATATYPE (list_t ListCons ListNil)
-   
-   [distinct_keys_cons]  Theorem
-      
-      ⊢ ∀k v ls.
-          (∀i. 0 ≤ i ⇒ i < len ls ⇒ FST (index i ls) ≠ k) ⇒
-          distinct_keys ls ⇒
-          distinct_keys ((k,v)::ls)
-   
-   [distinct_keys_f_eq_distinct_keys]  Theorem
-      
-      ⊢ ∀ls. distinct_keys_f ls ⇔ distinct_keys ls
-   
-   [distinct_keys_f_insert]  Theorem
-      
-      [oracles: DISK_THM] [axioms: insert_def] []
-      ⊢ ∀k v ls0 ls1.
-          distinct_keys_f (list_t_v ls0) ⇒
-          insert k v ls0 = Return ls1 ⇒
-          distinct_keys_f (list_t_v ls1)
-   
-   [distinct_keys_f_insert_for_all]  Theorem
-      
-      [oracles: DISK_THM] [axioms: insert_def] []
-      ⊢ ∀k v k1 ls0 ls1.
-          k1 ≠ k ⇒
-          for_all (λy. k1 ≠ FST y) (list_t_v ls0) ⇒
-          pairwise_rel (λx y. FST x ≠ FST y) (list_t_v ls0) ⇒
-          insert k v ls0 = Return ls1 ⇒
-          for_all (λy. k1 ≠ FST y) (list_t_v ls1)
-   
-   [distinct_keys_insert]  Theorem
-      
-      [oracles: DISK_THM] [axioms: insert_def] []
-      ⊢ ∀k v ls0 ls1.
-          distinct_keys (list_t_v ls0) ⇒
-          insert k v ls0 = Return ls1 ⇒
-          distinct_keys (list_t_v ls1)
-   
-   [distinct_keys_insert_index_neq]  Theorem
-      
-      [oracles: DISK_THM] [axioms: insert_def] []
-      ⊢ ∀k v q r ls0 ls1 i.
-          distinct_keys ((q,r)::list_t_v ls0) ⇒
-          q ≠ k ⇒
-          insert k v ls0 = Return ls1 ⇒
-          0 ≤ i ⇒
-          i < len (list_t_v ls1) ⇒
-          FST (index i (list_t_v ls1)) ≠ q
-   
-   [distinct_keys_tail]  Theorem
-      
-      ⊢ ∀k v ls. distinct_keys ((k,v)::ls) ⇒ distinct_keys ls
-   
-   [for_all_quant]  Theorem
-      
-      ⊢ ∀p ls. for_all p ls ⇔ ∀i. 0 ≤ i ⇒ i < len ls ⇒ p (index i ls)
-   
-   [insert_index_neq]  Theorem
-      
-      [oracles: DISK_THM] [axioms: insert_def] []
-      ⊢ ∀q k v ls0 ls1 i.
-          (∀j. 0 ≤ j ∧ j < len (list_t_v ls0) ⇒
-               q ≠ FST (index j (list_t_v ls0))) ⇒
-          q ≠ k ⇒
-          insert k v ls0 = Return ls1 ⇒
-          0 ≤ i ⇒
-          i < len (list_t_v ls1) ⇒
-          FST (index i (list_t_v ls1)) ≠ q
-   
-   [insert_lem]  Theorem
-      
-      [oracles: DISK_THM] [axioms: 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) ∧
-              distinct_keys (list_t_v ls1)
-          | Fail v1 => F
-          | Diverge => F
-   
-   [insert_lem_aux]  Theorem
-      
-      [oracles: DISK_THM] [axioms: insert_def] []
-      ⊢ ∀ls key value.
-          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
-          | Diverge => F
-   
-   [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_mut_fwd_def]  Theorem
-      
-      ⊢ ∀ls i.
-          nth_mut_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); nth_mut_fwd tl i0 od
-          | ListNil => Fail Failure
-   
-   [nth_mut_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
-   
-   [nth_mut_fwd_spec]  Theorem
-      
-      ⊢ ∀ls i.
-          u32_to_int i < len (list_t_v ls) ⇒
-          case nth_mut_fwd ls i of
-            Return x => x = index (u32_to_int i) (list_t_v ls)
-          | Fail v1 => F
-          | Diverge => F
-   
-   [pairwise_rel_quant]  Theorem
-      
-      ⊢ ∀p ls.
-          pairwise_rel p ls ⇔
-          ∀i j. 0 ≤ i ⇒ i < j ⇒ j < len ls ⇒ p (index i ls) (index j ls)
-   
-   
-*)
-end
diff --git a/backends/hol4/testScript.sml b/backends/hol4/testScript.sml
deleted file mode 100644
index 8b4d523c..00000000
--- a/backends/hol4/testScript.sml
+++ /dev/null
@@ -1,1747 +0,0 @@
-open HolKernel boolLib bossLib Parse
-
-val primitives_theory_name = "test"
-val _ = new_theory primitives_theory_name
-
-open boolTheory integerTheory wordsTheory stringTheory
-
-Datatype:
-  error = Failure
-End
-
-Datatype:
-  result = Return 'a | Fail error | Loop
-End
-
-Type M = ``: 'a result``
-
-(* TODO: rename *)
-val st_ex_bind_def = Define `
-  (st_ex_bind : 'a M -> ('a -> 'b M) -> 'b M) x f =
-    case x of
-      Return y => f y
-    | Fail e => Fail e
-    | Loop => Loop`;
-
-val bind_name = fst (dest_const “st_ex_bind”)
-
-val st_ex_return_def = Define `
-  (st_ex_return : 'a -> 'a M) x =
-    Return x`;
-
-Overload monad_bind[local] = ``st_ex_bind``
-Overload monad_unitbind[local] = ``\x y. st_ex_bind x (\z. y)``
-Overload monad_ignore_bind[local] = ``\x y. st_ex_bind x (\z. y)``
-(*Overload ex_bind[local] = ``st_ex_bind`` *)
-(* Overload ex_return[local] = ``st_ex_return`` *)
-(*Overload failwith = ``raise_Fail``*)
-
-(* Temporarily allow the monadic syntax *)
-val _ = monadsyntax.temp_add_monadsyntax ()
-
-val test1_def = Define `
-  test1 (x : bool) = Return x`
-
-val is_true_def = Define ‘
-  is_true (x : bool) = if x then Return () else Fail Failure’
-
-val test1_def = Define ‘
-  test1 (x : bool) = Return x’
-
-val test_monad_def = Define `
-  test_monad v =
-    do
-      x <- Return v;
-      Return x
-    od`
-
-val test_monad2_def = Define `
-  test_monad2 =
-    do
-      x <- Return T;
-      Return x
-    od`
-
-val test_monad3_def = Define `
-  test_monad3 x =
-    do
-      is_true x;
-      Return x
-    od`
-
-(**
- *  Arithmetic
- *)
-
-open intLib
-
-val test_int1 = Define ‘int1 = 32’
-val test_int2 = Define ‘int2 = -32’
-
-Theorem INT_THM1:
-  !(x y : int). x > 0 ==> y > 0 ==> x + y > 0
-Proof
-  ARITH_TAC
-QED
-
-Theorem INT_THM2:
-  !(x : int). T
-Proof
-  rw[]
-QED
-
-val _ = prefer_int ()
-
-val x = “-36217863217862718”
-
-(* Deactivate notations for int *)
-val _ = deprecate_int ()
-open arithmeticTheory
-
-
-val m = Hol_pp.print_apropos
-val f = Hol_pp.print_find
-
-(* Display types on/off: M-h C-t *)
-(* Move back: M-h b *)
-
-val _ = numLib.deprecate_num ()
-val _ = numLib.prefer_num ()
-
-Theorem NAT_THM1:
-  !(n : num). n < n + 1
-Proof
-  Induct_on ‘n’ >> DECIDE_TAC
-QED
-
-Theorem NAT_THM2:
-  !(n : num). n < n + (1 : num)
-Proof
-  gen_tac >>
-  Induct_on ‘n’ >- (
-    PURE_REWRITE_TAC [ADD, NUMERAL_DEF, BIT1, ALT_ZERO] >>
-    PURE_REWRITE_TAC [prim_recTheory.LESS_0_0]) >>
-  PURE_REWRITE_TAC [ADD] >>
-  irule prim_recTheory.LESS_MONO >>
-  asm_rewrite_tac []
-QED
-
-
-val x = “1278361286371286:num”
-
-
-(********************** PRIMITIVES *)
-val _ = prefer_int ()
-
-val _ = new_type ("u32", 0)
-val _ = new_type ("i32", 0)
-
-(*val u32_min_def = Define ‘u32_min = (0:int)’*)
-val u32_max_def = Define ‘u32_max = (4294967295:int)’
-
-(* TODO: change that *)
-val usize_max_def = Define ‘usize_max = (4294967295:int)’
-
-val i32_min_def = Define ‘i32_min = (-2147483648:int)’
-val i32_max_def = Define ‘i32_max = (2147483647:int)’
-
-val _ = new_constant ("u32_to_int", “:u32 -> int”)
-val _ = new_constant ("i32_to_int", “:i32 -> int”)
-
-val _ = new_constant ("int_to_u32", “:int -> u32”)
-val _ = new_constant ("int_to_i32", “:int -> i32”)
-
-
-(* TODO: change to "...of..." *)
-val u32_to_int_bounds =
-  new_axiom (
-    "u32_to_int_bounds",
-    “!n. 0 <= u32_to_int n /\ u32_to_int n <= u32_max”)
-
-val i32_to_int_bounds =
-  new_axiom (
-    "i32_to_int_bounds",
-    “!n. i32_min <= i32_to_int n /\ i32_to_int n <= i32_max”)
-
-val int_to_u32_id = new_axiom ("int_to_u32_id",
-    “!n. 0 <= n /\ n <= u32_max ==> u32_to_int (int_to_u32 n) = n”)
-
-val int_to_i32_id =
-  new_axiom (
-    "int_to_i32_id",
-    “!n. i32_min <= n /\ n <= i32_max ==>
-     i32_to_int (int_to_i32 n) = n”)
-
-val mk_u32_def = Define
-  ‘mk_u32 n =
-    if 0 <= n /\ n <= u32_max then Return (int_to_u32 n)
-    else Fail Failure’
-
-val u32_add_def = Define ‘u32_add x y = mk_u32 ((u32_to_int x) + (u32_to_int y))’
-
-Theorem MK_U32_SUCCESS:
-  !n. 0 <= n /\ n <= u32_max ==>
-  mk_u32 n = Return (int_to_u32 n)
-Proof
-  rw[mk_u32_def]
-QED
-
-Theorem U32_ADD_EQ:
-  !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
-Proof
-  rpt gen_tac >>
-  rpt DISCH_TAC >>
-  exists_tac “int_to_u32 (u32_to_int x + u32_to_int y)” >>
-  imp_res_tac MK_U32_SUCCESS >>
-  (* There is probably a better way of doing this *)
-  sg ‘0 <= u32_to_int x’ >- (rw[u32_to_int_bounds]) >>
-  sg ‘0 <= u32_to_int y’ >- (rw[u32_to_int_bounds]) >>
-  fs [u32_add_def] >>
-  irule int_to_u32_id >>
-  fs[]
-QED
-
-val u32_sub_def = Define ‘u32_sub x y = mk_u32 ((u32_to_int x) - (u32_to_int y))’
-
-Theorem U32_SUB_EQ:
-  !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
-Proof
-  rpt gen_tac >>
-  rpt DISCH_TAC >>
-  exists_tac “int_to_u32 (u32_to_int x - u32_to_int y)” >>
-  imp_res_tac MK_U32_SUCCESS >>
-  (* There is probably a better way of doing this *)
-  sg ‘u32_to_int x − u32_to_int y ≤ u32_max’ >-(
-    sg ‘u32_to_int x <= u32_max’ >- (rw[u32_to_int_bounds]) >>
-    sg ‘0 <= u32_to_int y’ >- (rw[u32_to_int_bounds]) >>
-    COOPER_TAC
-  ) >>
-  fs [u32_sub_def] >>
-  irule int_to_u32_id >>
-  fs[]
-QED
-
-val mk_i32_def = Define
-  ‘mk_i32 n =
-    if i32_min <= n /\ n <= i32_max then Return (int_to_i32 n)
-    else Fail Failure’
-
-val i32_add_def = Define ‘i32_add x y = mk_i32 ((i32_to_int x) + (i32_to_int y))’
-
-Theorem MK_I32_SUCCESS:
-  !n. i32_min <= n /\ n <= i32_max ==>
-  mk_i32 n = Return (int_to_i32 n)
-Proof
-  rw[mk_i32_def]
-QED
-
-Theorem I32_ADD_EQ:
-  !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
-Proof
-  rpt gen_tac >>
-  rpt DISCH_TAC >>
-  exists_tac “int_to_i32 (i32_to_int x + i32_to_int y)” >>
-  imp_res_tac MK_I32_SUCCESS >>
-  fs [i32_min_def, i32_add_def] >>
-  irule int_to_i32_id >>
-  fs[i32_min_def]
-QED
-
-open listTheory
-
-val _ = new_type ("vec", 1)
-val _ = new_constant ("vec_to_list", “:'a vec -> 'a list”)
-
-val VEC_TO_LIST_NUM_BOUNDS =
-  new_axiom (
-    "VEC_TO_LIST_BOUNDS",
-    “!v. let l = LENGTH (vec_to_list v) in
-     (0:num) <= l /\ l <= (4294967295:num)”)
-
-Theorem VEC_TO_LIST_INT_BOUNDS:
-  !v. let l = int_of_num (LENGTH (vec_to_list v)) in
-     0 <= l /\ l <= u32_max
-Proof
-  gen_tac >>
-  rw [u32_max_def] >>
-  assume_tac VEC_TO_LIST_NUM_BOUNDS >>
-  fs[]
-QED
-
-val VEC_LEN_DEF = Define ‘vec_len v = int_to_u32 (int_of_num (LENGTH (vec_to_list v)))’
-
-(*
-(* Useless *)
-Theorem VEC_LEN_BOUNDS:
-  !v. u32_min <= u32_to_int (vec_len v) /\ u32_to_int (vec_len v) <= u32_max
-Proof
-  gen_tac >>
-  qspec_then ‘v’ assume_tac VEC_TO_LIST_INT_BOUNDS >>
-  fs[VEC_LEN_DEF] >>
-  IMP_RES_TAC int_to_u32_id >>
-  fs[]
-QED
-*)
-
-(* The type parameters are ordered in alphabetical order *)
-Datatype:
-  test = Variant1 'b | Variant2 'a
-End
-
-Datatype:
-  test2 = Variant1_1 'T2 | Variant2_1 'T1
-End
-
-Datatype:
-  test2 = Variant1_2 'T1 | Variant2_2 'T2
-End
-
-(*
-“Variant1_1 3”
-“Variant1_2 3”
-
-type_of “CONS 3”
-*)
-
-(* TODO: argument order, we must also omit arguments in new type *)
-Datatype:
-  list_t =
-    ListCons 't list_t
-  | ListNil
-End
-
-val list_nth_mut_loop_loop_fwd_def = Define ‘
-  list_nth_mut_loop_loop_fwd (ls : 't list_t) (i : u32) : 't result =
-  case ls of
-  | ListCons x tl =>
-    if u32_to_int i = (0:int)
-    then Return x
-    else
-      do
-      i0 <- u32_sub i (int_to_u32 1);
-      list_nth_mut_loop_loop_fwd tl i0
-      od
-  | ListNil => 
-    Fail Failure
-’
-
-(*
-CoInductive coind:
- !x y. coind x /\ coind y ==> coind (x + y)
-End
-*)
-
-(*
-(* This generates inconsistent theorems *)
-CoInductive loop:
- !x. loop x = if x then loop x else 0
-End
-
-CoInductive loop:
- !(x : int). loop x = if x > 0 then loop (x - 1) else 0
-End
-*)
-
-(* This terminates *)
-val list_nth_mut_loop_loop_fwd_def = Define ‘
-  list_nth_mut_loop_loop_fwd (ls : 't list_t) (i : u32) : 't result =
-  case ls of
-  | ListCons x tl =>
-    if u32_to_int i = (0:int)
-    then Return x
-    else
-      do
-      i0 <- u32_sub i (int_to_u32 1);
-      list_nth_mut_loop_loop_fwd tl i0
-      od
-  | ListNil => 
-    Fail Failure
-’
-
-(* This is sort of a coinductive definition.
-
-   This can be justified:
-   - we first define a version [nth_fuel] which uses fuel (and is thus terminating)
-   - we define the predicate P:
-     P ls i n = case nth_fuel n ls i of Return _ => T |  _ => F
-   - we then use [LEAST] (least upper bound for natural numbers) to define nth as:
-     “nth ls i = if (?n. P n) then nth_fuel (LEAST (P ls i)) ls i else Fail Loop ”
-   - we finally prove that nth satisfies the proper equation.
-
-     We would need the following intermediate lemma:
-     !n.
-       n < LEAST (P ls i) ==> nth_fuel n ls i = Fail _ /\
-       n >= LEAST (P ls i) ==> nth_fuel n ls i = nth_fuel (LEAST P ls i) ls i
-     
- *)
-val _ = new_constant ("nth", “:'t list_t -> u32 -> 't result”)
-val nth_def = new_axiom ("nth_def", “
- 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
- ”)
-
-
-(*** Examples of proofs on [nth] *)
-val list_t_v_def = Define ‘
-  list_t_v ListNil = [] /\
-  list_t_v (ListCons x tl) = x :: list_t_v tl
-’
-
-(* TODO: move *)
-open dep_rewrite
-open integerTheory
-
-(* Ignore a theorem.
-
-   To be used in conjunction with {!pop_assum} for instance.
- *)
-fun IGNORE_TAC (_ : thm) : tactic = ALL_TAC
-
-
-Theorem INT_OF_NUM_INJ:
-  !n m. &n = &m ==> n = m
-Proof
-  rpt strip_tac >>
-  fs [Num]
-QED
-
-Theorem NUM_SUB_EQ:
-  !(x y z : int). x = y - z ==> 0 <= x ==> 0 <= z ==> Num y = Num z + Num x
-Proof
-  rpt strip_tac >>
-  sg ‘0 <= y’ >- COOPER_TAC >>
-  rfs [] >>
-  (* Convert to integers *)
-  irule INT_OF_NUM_INJ >>
-  imp_res_tac (GSYM INT_OF_NUM) >>
-  (* Associativity of & *)
-  PURE_REWRITE_TAC [GSYM INT_ADD] >>
-  fs []
-QED
-
-Theorem NUM_SUB_1_EQ:
-  !(x y : int). x = y - 1 ==> 0 <= x ==> Num y = SUC (Num x)
-Proof
-  rpt strip_tac >>
-  (* Get rid of the SUC *)
-  sg ‘SUC (Num x) = 1 + Num x’ >-(rw [ADD]) >> rw [] >>
-  (* Massage a bit the goal *)
-  qsuff_tac ‘Num y = Num (y − 1) + Num 1’ >- COOPER_TAC >>
-  (* Apply the general theorem *)
-  irule NUM_SUB_EQ >>
-  COOPER_TAC
-QED
-
-(* TODO: remove *)
-Theorem NUM_SUB_1_EQ1:
-  !i. 0 <= i - 1 ==> Num i = SUC (Num (i-1))
-Proof
-  rpt strip_tac >>
-  (* 0 <= i *)
-  sg ‘0 <= i’ >- COOPER_TAC >>
-  (* Get rid of the SUC *)
-  sg ‘SUC (Num (i - 1)) = 1 + Num (i - 1)’ >-(rw [ADD]) >>
-  rw [] >>
-  (* Convert to integers*)
-  irule INT_OF_NUM_INJ >>
-  imp_res_tac (GSYM INT_OF_NUM) >>
-  (* Associativity of & *)
-  PURE_REWRITE_TAC [GSYM INT_ADD] >>
-  fs []
-QED
-
-(* TODO:
-   - list all the integer variables, and insert bounds in the assumptions
-   - replace u32_min by 0?
-   - i - 1
-   - auto lookup of spec lemmas
-*)
-
-(* Add a list of theorems in the assumptions - TODO: move *)
-fun ASSUME_TACL (thms : thm list) : tactic =
-  let
-    (* TODO: use MAP_EVERY *)
-    fun t thms =
-      case thms of
-        [] => ALL_TAC
-      | thm :: thms => ASSUME_TAC thm >> t thms
-  in
-  t thms
-  end
-
-(* The map from integer type to bounds lemmas *)
-val integer_bounds_lemmas =
-  Redblackmap.fromList String.compare
-  [
-    ("u32", u32_to_int_bounds),
-    ("i32", i32_to_int_bounds)
-  ]
-
-(* The map from integer type to conversion lemmas *)
-val integer_conversion_lemmas =
-  Redblackmap.fromList String.compare
-  [
-    ("u32", int_to_u32_id),
-    ("i32", int_to_i32_id)
-  ]
-
-val integer_conversion_lemmas_list =
-  map snd (Redblackmap.listItems integer_conversion_lemmas)
-
-(* Not sure how term nets work, nor how we are supposed to convert Term.term
-   to mlibTerm.term.
-
-   TODO: it seems we need to explore the term and convert everything to strings.
- *)
-fun term_to_mlib_term (t : term) : mlibTerm.term =
-  mlibTerm.string_to_term (term_to_string t)
-
-(*
-(* The lhs of the conclusion of the integer conversion lemmas - we use this for
-   pattern matching *)
-val integer_conversion_lhs_concls =
-  let
-    val thms = map snd (Redblackmap.listItems integer_conversion_lemmas);
-    val concls = map (lhs o concl o UNDISCH_ALL o SPEC_ALL) thms;
-  in concls end
-*)
-
-(*
-val integer_conversion_concls_net =
-  let
-    val maplets = map (fn x => fst (dest_eq x) |-> ()) integer_conversion_concls;
-
-    val maplets = map (fn x => fst (mlibTerm.dest_eq x) |-> ()) integer_conversion_concls;
-    val maplets = map (fn x => fst (mlibThm.dest_unit_eq x) |-> ()) integer_conversion_concls;
-    val parameters = { fifo=false };
-  in mlibTermnet.from_maplets parameters maplets end
-
-mlibTerm.string_to_term (term_to_string “u32_to_int (int_to_u32 n) = n”)
-term_to_quote
-
-SIMP_CONV
-mlibThm.dest_thm u32_to_int_bounds
-mlibThm.dest_unit u32_to_int_bounds
-*)
-
-(* The integer types *)
-val integer_types_names =
-  Redblackset.fromList String.compare
-  (map fst (Redblackmap.listItems integer_bounds_lemmas))
-
-val all_integer_bounds = [
-  u32_max_def,
-  i32_min_def,
-  i32_max_def
-]
-
-(* Small utility: compute the set of assumptions in the context.
-
-   We isolate this code in a utility in order to be able to improve it:
-   for now we simply put all the assumptions in a set, but in the future
-   we might want to split the assumptions which are conjunctions in order
-   to be more precise.
- *)
-fun compute_asms_set ((asms,g) : goal) : term Redblackset.set =
-  Redblackset.fromList Term.compare asms
-
-(* See {!assume_bounds_for_all_int_vars}.
-
-   This tactic is in charge of adding assumptions for one variable.
- *)
-
-fun assume_bounds_for_int_var
-  (asms_set: term Redblackset.set) (var : string) (ty : string) :
-  tactic =
-  let
-    (* Lookup the lemma to apply *)
-    val lemma = Redblackmap.find (integer_bounds_lemmas, ty);
-    (* Instantiate the lemma *)
-    val ty_t = mk_type (ty, []);
-    val var_t = mk_var (var, ty_t);
-    val lemma = SPEC var_t lemma;
-    (* Split the theorem into a list of conjuncts.
-
-       The bounds are typically a conjunction:
-       {[
-         ⊢ 0 ≤ u32_to_int x ∧ u32_to_int x ≤ u32_max: thm
-       ]}
-     *)
-    val lemmas = CONJUNCTS lemma;
-    (* Filter the conjuncts: some of them might already be in the context,
-       we don't want to introduce them again, as it would pollute it.
-     *)
-    val lemmas = filter (fn lem => not (Redblackset.member (asms_set, concl lem))) lemmas;
-   in
-  (* Introduce the assumptions in the context *)
-  ASSUME_TACL lemmas
-  end
-
-(* Destruct if possible a term of the shape: [x y],
-   where [x] is not a comb.
-
-   Returns [(x, y)]
- *)
-fun dest_single_comb (t : term) : (term * term) option =
-  case strip_comb t of
-    (x, [y]) => SOME (x, y)
-  | _ => NONE
-
-(** Destruct if possible a term of the shape: [x (y z)].
-    Returns [(x, y, z)]
- *)
-fun dest_single_comb_twice (t : term) : (term * term * term) option =
-  case dest_single_comb t of
-    NONE => NONE
-  | SOME (x, y) =>
-    case dest_single_comb y of
-      NONE => NONE
-    | SOME (y, z) => SOME (x, y, z)
-
-(* A utility map to lookup integer conversion lemmas *)
-val integer_conversion_pat_map =
-  let
-    val thms = map snd (Redblackmap.listItems integer_conversion_lemmas);
-    val tl = map (lhs o concl o UNDISCH_ALL o SPEC_ALL) thms;
-    val tl = map (valOf o dest_single_comb_twice) tl;
-    val tl = map (fn (x, y, _) => (x, y)) tl;
-    val m = Redblackmap.fromList Term.compare tl
-  in m end
-
-(* Introduce bound assumptions for all the machine integers in the context.
-
-   Exemple:
-   ========
-   If there is “x : u32” in the input set, then we introduce:
-   {[
-     0 <= u32_to_int x
-     u32_to_int x <= u32_max
-   ]}
- *)
-fun assume_bounds_for_all_int_vars (asms, g) =
-  let
-    (* Compute the set of integer variables in the context *)
-    val vars = free_varsl (g :: asms);
-    (* Compute the set of assumptions already present in the context *)
-    val asms_set = compute_asms_set (asms, g);
-    (* Filter the variables to keep only the ones with type machine integer,
-       decompose the types at the same time *)
-    fun decompose_var (v : term) : (string * string) =
-      let
-        val (v, ty) = dest_var v;
-        val {Args=args, Thy=thy, Tyop=ty} = dest_thy_type ty;
-        val _ = assert null args;
-        val _ = assert (fn thy => thy = primitives_theory_name) thy;
-        val _ = assert (fn ty => Redblackset.member (integer_types_names, ty)) ty;
-      in (v, ty) end;
-    val vars = mapfilter decompose_var vars; 
-    (* Add assumptions for one variable *)
-    fun add_var_asm (v, ty) : tactic =
-      assume_bounds_for_int_var asms_set v ty;    
-    (* Add assumptions for all the variables *)
-    (* TODO: use MAP_EVERY *)
-    fun add_vars_asm vl : tactic =
-      case vl of
-        [] => ALL_TAC
-      | v :: vl =>
-        add_var_asm v >> add_vars_asm vl;
-  in
-    add_vars_asm vars (asms, g)
-  end
-
-(*
-dest_thy_type “:u32”
-val massage : tactic = assume_bounds_for_all_int_vars
-val vl = vars
-val (v::vl) = vl
-*)
-
-(*
-val (asms, g) = top_goal ()
-fun bounds_for_ints_in_list (vars : (string * hol_type) list) : tactic =
-  foldl
-  FAIL_TAC ""
-val var = "x"
-val ty = "u32"
-
-val asms_set = Redblackset.fromList Term.compare asms;
-
-val x = “1: int”
-val ty = "u32"
-
-val thm = lemma
-*)
-
-(* Given a theorem of the shape:
-   {[
-     A0, ..., An ⊢ B0 ==> ... ==> Bm ==> concl
-   ]}
-
-   Rewrite it so that it has the shape:
-   {[
-     ⊢ (A0 /\ ... /\ An /\ B0 /\ ... /\ Bm) ==> concl
-   ]}
- *)
-fun thm_to_conj_implies (thm : thm) : thm =
-  let
-    (* Discharge all the assumptions *)
-    val thm = DISCH_ALL thm;
-    (* Rewrite the implications as one conjunction *)
-    val thm = PURE_REWRITE_RULE [GSYM satTheory.AND_IMP] thm;
-  in thm end
-
-
-(* Like THEN1 and >-, but doesn't fail if the first subgoal is not completely
-   solved.
-
-   TODO: how to get the notation right?
- *)
-fun op PARTIAL_THEN1 (tac1: tactic) (tac2: tactic) : tactic = tac1 THEN_LT (NTH_GOAL tac2 1)
-
-(* If the current goal is [asms ⊢ g], and given a lemma of the form
-   [⊢ H ==> C], do the following:
-   - introduce [asms ⊢ H] as a subgoal and apply the given tactic on it
-   - also calls the theorem tactic with the theorem [asms ⊢ C]
-   
-   If the lemma is not an implication, we directly call the theorem tactic.
- *)
-fun sg_premise_then (premise_tac: tactic) (then_tac: thm_tactic) (thm : thm)  : tactic =
-  let
-    val c = concl thm;
-    (* First case: there is a premise to prove *)
-    fun prove_premise_then (h : term) =
-      PARTIAL_THEN1 (SUBGOAL_THEN h (fn h_thm => then_tac (MP thm h_thm))) premise_tac;
-    (* Second case: no premise to prove *)
-    val no_prove_premise_then = then_tac thm;
-  in
-    if is_imp c then prove_premise_then (fst (dest_imp c)) else no_prove_premise_then
-  end
-
-(* Same as {!sg_premise_then} but fails if the premise_tac fails to prove the premise *)
-fun prove_premise_then (premise_tac: tactic) (then_tac: thm_tactic) (thm : thm)  : tactic =
-  sg_premise_then
-    (premise_tac >> FAIL_TAC "prove_premise_then: could not prove premise")
-    then_tac thm
-
-(*
-val thm = th
-*)
-
-(* Call a function on all the subterms of a term *)
-fun dep_apply_in_subterms
-  (f : string Redblackset.set -> term -> unit)
-  (bound_vars : string Redblackset.set)
-  (t : term) : unit =
-  let
-    val dep = dep_apply_in_subterms f;
-    val _ = f bound_vars t;
-  in
-  case dest_term t of
-    VAR (name, ty) => ()
-  | CONST {Name=name, Thy=thy, Ty=ty} => ()
-  | COMB (app, arg) =>
-    let
-      val _ = dep bound_vars app;
-      val _ = dep bound_vars arg;
-    in () end
-  | LAMB (bvar, body) =>
-    let
-      val (varname, ty) = dest_var bvar;
-      val bound_vars = Redblackset.add (bound_vars, varname);
-      val _ = dep bound_vars body;
-    in () end
-  end
-
-(* Return the set of free variables appearing in the residues of a term substitution *)
-fun free_vars_in_subst_residue (s: (term, term) Term.subst) : string Redblackset.set =
-  let
-    val free_vars = free_varsl (map (fn {redex=_, residue=x} => x) s);
-    val free_vars = map (fst o dest_var) free_vars;
-    val free_vars = Redblackset.fromList String.compare free_vars;
-  in free_vars end
-
-(* Attempt to instantiate a rewrite theorem.
-
-   Remark: this theorem should be of the form:
-   H ⊢ x = y
-   
-   (without quantified variables).
-   
-   **REMARK**: the function raises a HOL_ERR exception if it fails.
-   
-   [forbid_vars]: forbid substituting with those vars (typically because
-   we are maching in a subterm under lambdas, and some of those variables
-   are bounds in the outer lambdas).
-*)
-fun inst_match_concl (forbid_vars : string Redblackset.set) (th : thm) (t : term) : thm =
-  let
-    (* Retrieve the lhs of the conclusion of the theorem *)
-    val l = lhs (concl th);
-    (* Match this lhs with the term *)
-    val (var_s, ty_s) = match_term l t;
-    (* Check that we are allowed to perform the substitution *)
-    val free_vars = free_vars_in_subst_residue var_s;
-    val _ = assert Redblackset.isEmpty (Redblackset.intersection (free_vars, forbid_vars));
-  in
-    (* Perform the substitution *)
-    INST var_s (INST_TYPE ty_s th)
-  end
-
-(*
-val forbid_vars = Redblackset.empty String.compare
-val t = “u32_to_int (int_to_u32 x)”
-val t = “u32_to_int (int_to_u32 3)”
-val th = (UNDISCH_ALL o SPEC_ALL) int_to_u32_id
-*)
-
-(* Attempt to instantiate a theorem by matching its first premise.
-
-   Note that we make the hypothesis tha all the free variables which need
-   to be instantiated appear in the first premise, of course (the caller should
-   enforce this).
-
-   Remark: this theorem should be of the form:
-   ⊢ H0 ==> ... ==> Hn ==> H
-   
-   (without quantified variables).
-   
-   **REMARK**: the function raises a HOL_ERR exception if it fails.
-   
-   [forbid_vars]: see [inst_match_concl]
-*)
-fun inst_match_first_premise
-  (forbid_vars : string Redblackset.set) (th : thm) (t : term) : thm =
-  let
-    (* Retrieve the first premise *)
-    val l = (fst o dest_imp o concl) th;
-    (* Match this with the term *)
-    val (var_s, ty_s) = match_term l t;
-    (* Check that we are allowed to perform the substitution *)
-    val free_vars = free_vars_in_subst_residue var_s;
-    val _ = assert Redblackset.isEmpty (Redblackset.intersection (free_vars, forbid_vars));
-  in
-    (* Perform the substitution *)
-    INST var_s (INST_TYPE ty_s th)
-  end
-
-(*
-val forbid_vars = Redblackset.empty String.compare
-val t = “u32_to_int z = u32_to_int i − 1”
-val th = SPEC_ALL NUM_SUB_1_EQ
-*)
-
-(* Call a matching function on all the subterms in the provided list of term.
-   This is a generic function.
-
-   [try_match] should return an instantiated theorem, as well as a term which
-   identifies this theorem (the lhs of the equality, if this is a rewriting
-   theorem for instance - we use this to check for collisions, and discard
-   redundant instantiations).
- *)
-fun inst_match_in_terms
-  (try_match: string Redblackset.set -> term -> term * thm)
-  (tl : term list) : thm list =
-  let
-    (* We use a map when storing the theorems, to avoid storing the same theorem twice *)
-    val inst_thms: (term, thm) Redblackmap.dict ref = ref (Redblackmap.mkDict Term.compare);
-    fun try_instantiate bvars t =
-      let
-        val (inst_th_tm, inst_th) = try_match bvars t;
-      in
-        inst_thms := Redblackmap.insert (!inst_thms, inst_th_tm, inst_th)
-      end
-      handle HOL_ERR _ => ();
-    (* Explore the term *)
-    val _ = app (dep_apply_in_subterms try_instantiate (Redblackset.empty String.compare)) tl;
-  in
-    map snd (Redblackmap.listItems (!inst_thms))
-  end
-
-(* Given a rewriting theorem [th] which has premises, return all the
-   instantiations of this theorem which make its conclusion match subterms
-   in the provided list of term.
- *)
-fun inst_match_concl_in_terms (th : thm) (tl : term list) : thm list =
-  let
-    val th = (UNDISCH_ALL o SPEC_ALL) th;
-    fun try_match bvars t =
-      let
-        val inst_th = inst_match_concl bvars th t;
-      in
-        (lhs (concl inst_th), inst_th)
-      end;
-  in
-    inst_match_in_terms try_match tl
-  end
-
-(*
-val t = “!x. u32_to_int (int_to_u32 x) = u32_to_int (int_to_u32 y)”
-val th = int_to_u32_id
-
-val thms = inst_match_concl_in_terms int_to_u32_id [t]
-*)
-
-
-(* Given a theorem [th] which has premises, return all the
-   instantiations of this theorem which make its first premise match subterms
-   in the provided list of term.
- *)
-fun inst_match_first_premise_in_terms (th : thm) (tl : term list) : thm list =
-  let
-    val th = SPEC_ALL th;
-    fun try_match bvars t =
-      let
-        val inst_th = inst_match_first_premise bvars th t;
-      in
-        ((fst o dest_imp o concl) inst_th, inst_th)
-      end;
-  in
-    inst_match_in_terms try_match tl
-  end
-
-(*
-val t = “x = y - 1 ==> T”
-val th = SPEC_ALL NUM_SUB_1_EQ
-
-val thms = inst_match_first_premise_in_terms th [t]
-*)
-
-(* Attempt to apply dependent rewrites with a theorem by matching its
-   conclusion with subterms of the goal.
- *)
-fun apply_dep_rewrites_match_concl_tac
-  (prove_premise : tactic) (then_tac : thm_tactic) (th : thm) : tactic =
-  fn (asms, g) =>
-    let
-      (* Discharge the assumptions so that the goal is one single term *)
-      val thms = inst_match_concl_in_terms th (g :: asms);
-      val thms = map thm_to_conj_implies thms;
-    in
-      (* Apply each theorem *)
-      MAP_EVERY (prove_premise_then prove_premise then_tac) thms (asms, g)
-    end
-
-(*
-val (asms, g) = ([
-  “u32_to_int z = u32_to_int i − u32_to_int (int_to_u32 1)”,
-  “u32_to_int (int_to_u32 2) = 2”
-], “T”)
-
-apply_dep_rewrites_match_concl_tac
-  (FULL_SIMP_TAC simpLib.empty_ss all_integer_bounds >> COOPER_TAC)
-  (fn th => FULL_SIMP_TAC simpLib.empty_ss [th])
-  int_to_u32_id
-*)
-
-(* Attempt to apply dependent rewrites with a theorem by matching its
-   first premise with subterms of the goal.
- *)
-fun apply_dep_rewrites_match_first_premise_tac
-  (prove_premise : tactic) (then_tac : thm_tactic) (th : thm) : tactic =
-  fn (asms, g) =>
-    let
-      (* Discharge the assumptions so that the goal is one single term *)
-      val thms = inst_match_first_premise_in_terms th (g :: asms);
-      val thms = map thm_to_conj_implies thms;
-      fun apply_tac th =
-        let
-          val th = thm_to_conj_implies th;
-        in
-          prove_premise_then prove_premise then_tac th
-        end;
-    in
-      (* Apply each theorem *)
-      MAP_EVERY apply_tac thms (asms, g)
-    end
-
-(* See {!rewrite_all_int_conversion_ids}.
-
-   Small utility which takes care of one rewriting.
-
-   TODO: we actually don't use it. REMOVE?
- *)
-fun rewrite_int_conversion_id
-  (asms_set: term Redblackset.set) (x : term) (ty : string) :
-  tactic =
-  let
-    (* Lookup the theorem *)
-    val lemma = Redblackmap.find (integer_conversion_lemmas, ty);
-    (* Instantiate *)
-    val lemma = SPEC x lemma;
-    (* Rewrite the lemma. The lemma typically has the shape:
-       ⊢ u32_min <= x /\ x <= u32_max ==> u32_to_int (int_to_u32 x) = x
-       
-       Make sure the lemma has the proper shape, attempt to prove the premise,
-       then use the conclusion if it succeeds.
-     *)
-    val lemma = thm_to_conj_implies lemma;
-    (* Retrieve the conclusion of the lemma - we do this to check if it is not
-       already in the assumptions *)
-    val c = concl (UNDISCH_ALL lemma);
-    val already_in_asms = Redblackset.member (asms_set, c);
-    (* Small utility: the tactic to prove the premise *)
-    val prove_premise =
-      (* We might need to unfold the bound definitions, in particular if the
-         term is a constant (e.g.,  “3:int”) *)
-      FULL_SIMP_TAC simpLib.empty_ss all_integer_bounds >>
-      COOPER_TAC;
-    (* Rewrite with a lemma, then assume it *)
-    fun rewrite_then_assum (thm : thm) : tactic =
-      FULL_SIMP_TAC simpLib.empty_ss [thm] >> assume_tac thm;
-  in
-    (* If the conclusion is not already in the assumptions, prove it, use
-       it to rewrite the goal and add it in the assumptions, otherwise do nothing *)
-    if already_in_asms then ALL_TAC
-    else prove_premise_then prove_premise rewrite_then_assum lemma
- end
-
-(* Look for conversions from integers to machine integers and back.
-   {[
-     u32_to_int (int_to_u32 x)
-   ]}
-
-   Attempts to prove and apply equalities of the form:
-   {[
-     u32_to_int (int_to_u32 x) = x
-   ]}
-   
-   **REMARK**: this function can fail, if it doesn't manage to prove the
-   premises of the theorem to apply.
-
-   TODO: update
- *)
-val rewrite_with_dep_int_lemmas : tactic =
-  (* We're not trying to be smart: we just try to rewrite with each theorem at
-     a time *)
-  let
-    val prove_premise = FULL_SIMP_TAC simpLib.empty_ss all_integer_bounds >> COOPER_TAC;
-    val then_tac1 = (fn th => FULL_SIMP_TAC simpLib.empty_ss [th]);
-    val rewr_tac1 = apply_dep_rewrites_match_concl_tac prove_premise then_tac1;
-    val then_tac2 = (fn th => FULL_SIMP_TAC simpLib.empty_ss [th]);
-    val rewr_tac2 = apply_dep_rewrites_match_first_premise_tac prove_premise then_tac2;
-  in
-      MAP_EVERY rewr_tac1 integer_conversion_lemmas_list >>
-      MAP_EVERY rewr_tac2 [NUM_SUB_1_EQ]
-  end
-
-(*
-apply_dep_rewrites_match_first_premise_tac prove_premise then_tac NUM_SUB_1_EQ
-
-sg ‘u32_to_int z = u32_to_int i − 1 /\ 0 ≤ u32_to_int z’ >- prove_premise
-
-prove_premise_then prove_premise
-
-val thm = thm_to_conj_implies  (SPECL [“u32_to_int z”, “u32_to_int i”] NUM_SUB_1_EQ)
-
-val h = “u32_to_int z = u32_to_int i − 1 ∧ 0 ≤ u32_to_int z”
-*)
-
-(* Massage a bit the goal, for instance by introducing integer bounds in the
-   assumptions.
-*)
-val massage : tactic =
-  assume_bounds_for_all_int_vars >>
-  rewrite_with_dep_int_lemmas
-
-(* Lexicographic order over pairs *)
-fun pair_compare (comp1 : 'a * 'a -> order) (comp2 : 'b * 'b -> order)
-  ((p1, p2) : (('a * 'b) * ('a * 'b))) : order =
-  let
-    val (x1, y1) = p1;
-    val (x2, y2) = p2;
-  in
-    case comp1 (x1, x2) of
-      LESS => LESS
-    | GREATER => GREATER
-    | EQUAL => comp2 (y1, y2)
-  end
-
-(* A constant name (theory, constant name) *)
-type const_name = string * string
-
-val const_name_compare = pair_compare String.compare String.compare
-
-(* The registered spec theorems, that {!progress} will automatically apply.
-
-   The keys are the function names (it is a pair, because constant names
-   are made of the theory name and the name of the constant itself).
-
-   Also note that we can store several specs per definition (in practice, when
-   looking up specs, we will try them all one by one, in a LIFO order).
-
-   We store theorems where all the premises are in the goal, with implications
-   (i.e.: [⊢ H0 ==> ... ==> Hn ==> H], not  [H0, ..., Hn ⊢ H]).
-
-   We do this because, when doing proofs by induction, {!progress} might have to
-   handle *unregistered* theorems coming the current goal assumptions and of the shape
-   (the conclusion of the theorem is an assumption, and we want to ignore this assumption):
-   {[
-     [∀i. u32_to_int i < &LENGTH (list_t_v ls) ⇒
-         case nth ls i of
-           Return x => ...
-         | ...      => ...]
-     ⊢ ∀i. u32_to_int i < &LENGTH (list_t_v ls) ⇒
-         case nth ls i of
-           Return x => ...
-         | ...      => ...
-   ]}
- *)
-val reg_spec_thms: (const_name, thm) Redblackmap.dict ref =
-  ref (Redblackmap.mkDict const_name_compare)
-
-(* Retrieve the specified application in a spec theorem.
-
-   A spec theorem for a function [f] typically has the shape:
-   {[
-     !x0 ... xn.
-       H0 ==> ... Hm ==>
-         (exists ...
-           (exists ... . f y0 ... yp = ... /\ ...) \/
-           (exists ... . f y0 ... yp = ... /\ ...) \/
-           ...
-   ]}
-
-   Or:
-   {[
-    !x0 ... xn.
-      H0 ==> ... Hm ==>
-        case f y0 ... yp of
-          ... => ...
-        | ... =>  ...
-   ]}
-
-   We return: [f y0 ... yp]
-*)
-fun get_spec_app (t : term) : term =
-  let
-    (* Remove the universally quantified variables, the premises and
-       the existentially quantified variables *)
-    val t = (snd o strip_exists o snd o strip_imp o snd o strip_forall) t;
-    (* Remove the exists, take the first disjunct *)
-    val t = (hd o strip_disj o snd o strip_exists) t;
-    (* Split the conjunctions and take the first conjunct *)
-    val t = (hd o strip_conj) t;
-    (* Remove the case if there is, otherwise destruct the equality *)
-    val t =
-      if TypeBase.is_case t then let val (_, t, _) = TypeBase.dest_case t in t end
-      else (fst o dest_eq) t;
-  in t end
-
-(* Given a function call [f y0 ... yn] return the name of the function *)
-fun get_fun_name_from_app (t : term) : const_name =
-  let
-    val f = (fst o strip_comb) t;
-    val {Name=name, Thy=thy, Ty=_} = dest_thy_const f;
-    val cn = (thy, name);
-  in cn end
-
-(* Register a spec theorem in the spec database.
-
-   For the shape of spec theorems, see {!get_spec_thm_app}.
- *)
-fun register_spec_thm (th: thm) : unit =
-  let
-    (* Transform the theroem a bit before storing it *)
-    val th = SPEC_ALL th;
-    (* Retrieve the app ([f x0 ... xn]) *)
-    val f = get_spec_app (concl th);
-    (* Retrieve the function name *)
-    val cn = get_fun_name_from_app f;
-  in
-    (* Store *)
-    reg_spec_thms := Redblackmap.insert (!reg_spec_thms, cn, th)
-  end
-
-(* TODO: I32_SUB_EQ *)
-val _ = app register_spec_thm [U32_ADD_EQ, U32_SUB_EQ, I32_ADD_EQ]
-
-(*
-app register_spec_thm [U32_ADD_EQ, U32_SUB_EQ, I32_ADD_EQ]
-Redblackmap.listItems (!reg_spec_thms)
-*)
-
-(*
-(* TODO: remove? *)
-datatype monadic_app_kind =
- Call | Bind | Case
-*)
-
-(* Repeatedly destruct cases and return the last scrutinee we get *)
-fun strip_all_cases_get_scrutinee (t : term) : term =
-  if TypeBase.is_case t
-  then (strip_all_cases_get_scrutinee o fst o TypeBase.strip_case) t
-  else t
-
-(*
-TypeBase.dest_case “case ls of [] => T | _ => F”
-TypeBase.strip_case “case ls of [] => T | _ => F”
-TypeBase.strip_case “case (if b then [] else [0, 1]) of [] => T | _ => F”
-TypeBase.strip_case “3”
-TypeBase.dest_case “3”
-
-strip_all_cases_get_scrutinee “case ls of [] => T | _ => F”
-strip_all_cases_get_scrutinee “case (if b then [] else [0, 1]) of [] => T | _ => F”
-strip_all_cases_get_scrutinee “3”
-*)
-
-
-(* Provided the goal contains a call to a monadic function, return this function call.
-
-   The goal should be of the shape:
-   1.
-   {[
-     case (* potentially expanded function body *) of
-       ... => ...
-     | ... => ...
-   ]}
-
-   2. Or:
-   {[
-     exists ... .
-       ... (* potentially expanded function body *) = Return ... /\
-       ... (* Various properties *)
-   ]}
-
-   3. Or a disjunction of cases like the one above, below existential binders
-   (actually: note sure this last case exists in practice):
-   {[
-     exists ... .
-       (exists ... . (* body *) = Return ... /\ ...) \/
-       ...
-   ]}
-
-   The function body should be of the shape:
-   {[
-     x <- f y0 ... yn;
-     ...
-   ]}
-
-   Or (typically if we expanded the monadic binds):
-   {[
-     case f y0 ... yn of
-     ...
-   ]}
-
-   Or simply (typically if we reached the end of the function we're analyzing):
-   {[
-     f y0 ... yn
-   ]}
-
-   For all the above cases we would return [f y0 ... yn].
- *)
-fun get_monadic_app_call (t : term) : term =
-  (* We do something slightly imprecise but hopefully general and robut *)
-  let
-     (* Case 3.: strip the existential binders, and take the first disjuntion *)
-     val t = (hd o strip_disj o snd o strip_exists) t;
-     (* Case 2.: strip the existential binders, and take the first conjunction *)
-     val t = (hd o strip_conj o snd o strip_exists) t;
-     (* If it is an equality, take the lhs *)
-     val t = if is_eq t then lhs t else t;
-     (* Expand the binders to transform them to cases *)
-     val t =
-       (rhs o concl) (REWRITE_CONV [st_ex_bind_def] t)
-       handle UNCHANGED => t;
-     (* Strip all the cases *)
-     val t = strip_all_cases_get_scrutinee t;
-  in t end
-
-(* Use the given theorem to progress by one step (we use this when
-   analyzing a function body: this goes forward by one call to a monadic function).
-
-   We transform the goal by:
-   - pushing the theorem premises to a subgoal
-   - adding the theorem conclusion in the assumptions in another goal, and
-     getting rid of the monadic call
-
-  Then [then_tac] receives as paramter the monadic call on which we applied
-  the lemma. This can be useful, for instance, to make a case disjunction.
-
-  This function is the most primitive of the [progress...] functions.
- *)
-fun pure_progress_with (premise_tac : tactic)
-  (then_tac : term -> thm_tactic) (th : thm) : tactic =
-  fn (asms,g) =>
-  let
-    (* Remove all the universally quantified variables from the theorem *)
-    val th = SPEC_ALL th;
-    (* Retrieve the monadic call from the goal *)
-    val fgoal = get_monadic_app_call g;
-    (* Retrieve the app call from the theroem *)
-    val gth = get_spec_app (concl th);
-    (* Match and instantiate *)
-    val (var_s, ty_s) = match_term gth fgoal;
-    (* Instantiate the theorem *)
-    val th = INST var_s (INST_TYPE ty_s th);
-    (* Retrieve the premises of the theorem *)
-    val th = PURE_REWRITE_RULE [GSYM satTheory.AND_IMP] th;
-  in
-    (* Apply the theorem *)
-    sg_premise_then premise_tac (then_tac fgoal) th (asms, g)
-  end
-
-(*
-val (asms, g) = top_goal ()
-val t = g
-
-val th = U32_SUB_EQ
-
-val premise_tac =  massage >> TRY COOPER_TAC
-fun then_tac fgoal =
-  fn thm => ASSUME_TAC thm >> Cases_on ‘^fgoal’ >>
-  rw [] >> fs [st_ex_bind_def] >> massage >> fs []
-
-pure_progress_with premise_tac then_tac th
-*)
-
-fun progress_with (th : thm) : tactic =
-  let
-    val premise_tac = massage >> fs [] >> rw [] >> TRY COOPER_TAC;
-    fun then_tac fgoal thm =
-      ASSUME_TAC thm >> Cases_on ‘^fgoal’ >>
-      rw [] >> fs [st_ex_bind_def] >> massage >> fs [];
-  in
-    pure_progress_with premise_tac then_tac th
-  end
-
-(*
-progress_with U32_SUB_EQ
-*)
-
-(* This function lookups the theorem to use to make progress *)
-val progress : tactic =
-  fn (asms, g) =>
-  let
-    (* Retrieve the monadic call from the goal *)
-    val fgoal = get_monadic_app_call g;
-    val fname = get_fun_name_from_app fgoal;
-    (* Lookup the theorem: first look in the assumptions (we might want to
-       use the inductive hypothesis for instance) *)
-    fun asm_to_spec asm =
-      let
-        (* Fail if there are no universal quantifiers *)
-        val _ =
-          if is_forall asm then asm
-          else assert is_forall ((snd o strip_imp) asm);
-        val asm_fname = (get_fun_name_from_app o get_spec_app) asm;
-        (* Fail if the name is not the one we're looking for *)
-        val _ = assert (fn n => fname = n) asm_fname;
-      in
-        ASSUME asm
-      end
-    val asms_thl = mapfilter asm_to_spec asms;
-    (* Lookup a spec in the database *)
-    val thl =
-      case Redblackmap.peek (!reg_spec_thms, fname) of
-        NONE => asms_thl
-      | SOME spec => spec :: asms_thl;
-    val _ =
-      if null thl then
-        raise (failwith "progress: could not find a suitable theorem to apply")
-      else ();
-  in
-    (* Attempt to use the theorems one by one *)
-    MAP_FIRST progress_with thl (asms, g)
-  end
-
-(*
-val (asms, g) = top_goal ()
-*)
-
-(* TODO: no exfalso tactic?? *)
-val EX_FALSO : tactic =
-  SUBGOAL_THEN “F” (fn th => ASSUME_TAC th >> fs[])
-
-Theorem nth_lem:
-  !(ls : 't list_t) (i : u32).
-    u32_to_int i < int_of_num (LENGTH (list_t_v ls)) ==>
-    case nth ls i of
-    | Return x => x = EL (Num (u32_to_int i)) (list_t_v ls)
-    | Fail _ => F
-    | Loop => F
-Proof
-  Induct_on ‘ls’ >> rw [list_t_v_def] >~ [‘ListNil’]
-  >-(massage >> EX_FALSO >> COOPER_TAC) >>
-  PURE_ONCE_REWRITE_TAC [nth_def] >> rw [] >>
-  progress >> progress
-QED
-
-(* Example from the hashmap *)
-val _ = new_constant ("insert", “: u32 -> 't -> (u32 # 't) list_t -> (u32 # 't) list_t result”)
-val insert_def = new_axiom ("insert_def", “
- insert (key : u32) (value : 't) (ls : (u32 # 't) list_t) : (u32 # 't) list_t result =
-  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)
- ”)
-
-(* Property that keys are pairwise distinct *)
-val distinct_keys_def = Define ‘
-  distinct_keys (ls : (u32 # 't) list) =
-    !i j.
-      i < LENGTH ls ==>
-      j < LENGTH ls ==>
-      FST (EL i ls) = FST (EL j ls) ==>
-      i = j
-’
-
-val lookup_raw_def = Define ‘
-  lookup_raw key [] = NONE /\
-  lookup_raw key ((k, v) :: ls) =
-    if k = key then SOME v else lookup_raw key ls
-’
-
-val lookup_def = Define ‘
-  lookup key ls = lookup_raw key (list_t_v ls)
-’
-
-Theorem insert_lem:
-  !ls key value.
-    (* The keys are pairwise distinct *)
-    distinct_keys (list_t_v ls) ==>
-    case insert key value ls of
-    | Return ls1 =>
-      (* We updated the binding *)
-      lookup key ls1 = SOME value /\
-      (* The other bindings are left unchanged *)
-      (!k. k <> key ==> lookup k ls = lookup k ls1)
-    | Fail _ => F
-    | Loop => F
-Proof
-  Induct_on ‘ls’ >> rw [list_t_v_def] >~ [‘ListNil’] >>
-  PURE_ONCE_REWRITE_TAC [insert_def] >> rw []
-  >- (rw [lookup_def, lookup_raw_def, list_t_v_def])
-  >- (rw [lookup_def, lookup_raw_def, list_t_v_def]) >>
-  CASE_TAC >> rw []
-  >- (rw [lookup_def, lookup_raw_def, list_t_v_def])
-  >- (rw [lookup_def, lookup_raw_def, list_t_v_def]) >>
-  progress
-  >- (
-    fs [distinct_keys_def] >>
-    rpt strip_tac >>
-    first_assum (qspecl_then [‘SUC i’, ‘SUC j’] ASSUME_TAC) >>
-    fs []
-    (* Alternative: *)
-    (*
-      PURE_ONCE_REWRITE_TAC [GSYM prim_recTheory.INV_SUC_EQ] >>
-      first_assum irule >> fs []
-     *)) >>
-  fs [lookup_def, lookup_raw_def, list_t_v_def]
-QED
-
-(***
- * Example of how to get rid of the fuel in practice
- *)
-val nth_fuel_def = Define ‘
- 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 is_loop_def = Define ‘is_loop r = case r of Loop => T | _ => F’
- 
-val nth_fuel_P_def = Define ‘
-  nth_fuel_P ls i n = ~is_loop (nth_fuel n ls i)
-’
-
-(* TODO: this is not the theorem we want: we want the one below *)
-Theorem nth_fuel_mono:
-  !n m ls i.
-    n <= m ==>
-    if is_loop (nth_fuel n ls i) then T
-    else nth_fuel n ls i = nth_fuel m ls i
-Proof
-  Induct_on ‘n’ >- (
-    rpt gen_tac >>
-    DISCH_TAC >>
-    PURE_ONCE_REWRITE_TAC [nth_fuel_def] >>
-    rw[is_loop_def]
-  ) >>
-  (* Interesting case *)
-  rpt gen_tac >>
-  DISCH_TAC >>
-  CASE_TAC >>
-  Cases_on ‘m’ >- (
-    (* Contradiction: SUC n < 0 *)
-    sg ‘SUC n = 0’ >- decide_tac >>
-    fs [is_loop_def]
-  ) >>
-  fs [is_loop_def] >>
-  pop_assum mp_tac >>
-  PURE_ONCE_REWRITE_TAC [nth_fuel_def] >>
-  fs [] >>
-  DISCH_TAC >>
-  (* We just have to explore all the paths: we can have dedicated tactics for that
-     (we need to do case analysis) *)
-  Cases_on ‘ls’ >> fs [] >>
-  Cases_on ‘u32_to_int (i :u32) = (0 :int)’ >> fs [] >>
-  fs [st_ex_bind_def] >>
-  Cases_on ‘u32_sub (i :u32) (int_to_u32 (1 :int))’ >> fs [] >>
-  (* Apply the induction hypothesis *)
-  first_x_assum (qspecl_then [‘n'’, ‘l’, ‘a’] assume_tac) >>
-  first_x_assum imp_res_tac >>
-  pop_assum mp_tac >>
-  CASE_TAC
-QED
-
-Theorem nth_fuel_P_mono:
-  !n m ls i.
-    n <= m ==>
-    nth_fuel_P ls i n ==>
-    nth_fuel n ls i = nth_fuel m ls i
-Proof
-  rpt gen_tac >> rpt DISCH_TAC >>
-  fs [nth_fuel_P_def] >>
-  imp_res_tac nth_fuel_mono >>
-  pop_assum (qspecl_then [‘ls’, ‘i’] assume_tac) >>
-  pop_assum mp_tac >> CASE_TAC >> fs []
-QED
-
-(*Theorem nth_fuel_least_fail_mono:
-  !n ls i.
-    n < $LEAST (nth_fuel_P ls i) ==>
-    nth_fuel n ls i = Loop
-Proof
-  rpt gen_tac >>
-  disch_tac >>
-  imp_res_tac whileTheory.LESS_LEAST >>
-  fs [nth_fuel_P_def, is_loop_def] >>
-  pop_assum mp_tac >>
-  CASE_TAC
-QED*)
-
-Theorem nth_fuel_least_success_mono:
-  !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
-Proof
-  rpt gen_tac >>
-  disch_tac >>
-  (* Case disjunction on whether there exists a fuel such that it terminates *)
-  Cases_on ‘?m. nth_fuel_P ls i m’ >- (
-    (* Terminates *)
-    irule EQ_SYM >>
-    irule nth_fuel_P_mono >> fs [] >>
-    (* Prove that calling with the least upper bound of fuel succeeds *)    
-    qspec_then ‘nth_fuel_P (ls :α list_t) (i :u32)’ imp_res_tac whileTheory.LEAST_EXISTS_IMP
-  ) >>
-  (* Doesn't terminate *)
-  fs [] >>
-  sg ‘~(nth_fuel_P ls i n)’ >- fs [] >>
-  sg ‘~(nth_fuel_P ls i ($LEAST (nth_fuel_P ls i)))’ >- fs [] >>
-  fs [nth_fuel_P_def, is_loop_def] >>
-  pop_assum mp_tac >> CASE_TAC >>
-  pop_assum mp_tac >>
-  pop_assum mp_tac >> CASE_TAC
-QED
-
-val nth_def_raw = Define ‘
-  nth ls i =
-    if (?n. nth_fuel_P ls i n) then nth_fuel ($LEAST (nth_fuel_P ls i)) ls i
-    else Loop
-’
-
-(* This makes the proofs easier, in that it helps us control the context *)
-val nth_expand_def = Define ‘
-  nth_expand nth ls i =
-    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
-’             
-
-(* Prove the important theorems: termination case *)
-Theorem nth_def_terminates:
-  !ls i.
-  (?n. nth_fuel_P ls i n) ==>
-  nth ls i =
-    nth_expand nth ls i
-Proof
-  rpt strip_tac >>
-  fs [nth_expand_def] >>
-  PURE_ONCE_REWRITE_TAC [nth_def_raw] >>
-  (* Prove that the least upper bound is <= n *)
-  sg ‘$LEAST (nth_fuel_P ls i) <= n’ >-(
-    qspec_then ‘nth_fuel_P (ls :α list_t) (i :u32)’ imp_res_tac whileTheory.LEAST_EXISTS_IMP >>
-    spose_not_then assume_tac >> fs []
-  ) >>
-  (* Use the monotonicity theorem - TODO: ? *)
-  imp_res_tac nth_fuel_least_success_mono >>
-  (* Rewrite only on the left - TODO: easy way ?? *)
-  qspecl_then [‘$LEAST (nth_fuel_P ls i)’, ‘ls’, ‘i’] assume_tac nth_fuel_def >>
-  (* TODO: how to discard assumptions?? *)
-  fs [] >> pop_assum (fn _ => fs []) >>
-  (* Cases on the least upper bound *)
-  Cases_on ‘$LEAST (nth_fuel_P ls i)’ >> rw [] >- (
-    (* The bound is equal to 0: contradiction *)
-    sg ‘nth_fuel 0 ls i = Loop’ >- (PURE_ONCE_REWRITE_TAC [nth_fuel_def] >> rw []) >>
-    fs [nth_fuel_P_def, is_loop_def]
-  ) >>
-  (* Bound not equal to 0 *)
-  fs [nth_fuel_P_def, is_loop_def] >>
-  (* Explore all the paths *)
-  fs [st_ex_bind_def] >>
-  Cases_on ‘ls’ >> rw [] >> fs [] >>
-  Cases_on ‘u32_sub i (int_to_u32 1)’ >> rw [] >> fs [] >>
-  (* Recursive call: use monotonicity - we have an assumption which eliminates the Loop case *)
-  Cases_on ‘nth_fuel n' l a’ >> rw [] >> fs [] >>
-  (sg ‘nth_fuel_P l a n'’ >- fs [nth_fuel_P_def, is_loop_def]) >>
-  (sg ‘$LEAST (nth_fuel_P l a) <= n'’ >-(
-   qspec_then ‘nth_fuel_P l a’ imp_res_tac whileTheory.LEAST_EXISTS_IMP >>
-   spose_not_then assume_tac >> fs [])) >>
-  imp_res_tac nth_fuel_least_success_mono >> fs []
-QED
-
-(* Prove the important theorems: divergence case *)
-Theorem nth_def_loop:
-  !ls i.
-  (!n. ~nth_fuel_P ls i n) ==>
-  nth ls i =
-    nth_expand nth ls i
-Proof
-  rpt gen_tac >>
-  PURE_ONCE_REWRITE_TAC [nth_def_raw] >>
-  strip_tac >> rw[] >>
-  (* Non-terminating case *)
-  sg ‘∀n. ¬nth_fuel_P ls i (SUC n)’ >- rw [] >>
-  fs [nth_fuel_P_def, is_loop_def] >>
-  pop_assum mp_tac >>
-  PURE_ONCE_REWRITE_TAC [nth_fuel_def] >>
-  rw [] >>  
-  fs [nth_expand_def] >>
-  (* Evaluate all the paths *)
-  fs [st_ex_bind_def] >>
-  Cases_on ‘ls’ >> rw [] >> fs [] >>
-  Cases_on ‘u32_sub i (int_to_u32 1)’ >> rw [] >> fs [] >>
-  (* Use the definition of nth *)
-  rw [nth_def_raw] >>
-  first_x_assum (qspec_then ‘$LEAST (nth_fuel_P l a)’ assume_tac) >>
-  Cases_on ‘nth_fuel ($LEAST (nth_fuel_P l a)) l a’ >> fs []
-QED
-
-(* The final theorem *)
-Theorem nth_def:
-  !ls i.
-  nth ls i =
-    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 >>
-  Cases_on ‘?n. nth_fuel_P ls i n’ >-(
-    assume_tac nth_def_terminates >>
-    fs [nth_expand_def] >>
-    pop_assum irule >>
-    metis_tac []) >>
-  fs [] >> imp_res_tac nth_def_loop >> fs [nth_expand_def]
-QED
-
-(*
-
-Je viens de finir ma petite expérimentation avec le fuel : ça marche bien. Par exemple, si je pose les définitions suivantes :
-Datatype:
-  result = Return 'a | Fail error | Loop
-End
-
-(* Omitting some definitions like the bind *)
-
-val _ = Define ‘
- 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 _ = Define 'is_loop r = case r of Loop => T | _ => F'
- 
-val _ = Define 'nth_fuel_P ls i n = ~is_loop (nth_fuel n ls i)'
-
-(* $LEAST returns the least upper bound for a predicate (if it exists - otherwise it returns an arbitrary number) *)
-val _ = Define ‘
-  nth ls i =
-    if (?n. nth_fuel_P ls i n) then nth_fuel ($LEAST (nth_fuel_P ls i)) ls i
-    else Loop
-’
-J'arrive à montrer (c'est un chouïa technique) :
-Theorem nth_def:
-  !ls i.
-  nth ls i =
-    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
-
-*)
-
-val _ = export_theory ()
diff --git a/backends/hol4/testTheory.sig b/backends/hol4/testTheory.sig
deleted file mode 100644
index 21b74a39..00000000
--- a/backends/hol4/testTheory.sig
+++ /dev/null
@@ -1,834 +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_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_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