Organize a bit the HOL files

8 files changed, 1160 insertions, 190 deletions

diff --git a/backends/hol4/primitivesArithScript.sml b/backends/hol4/primitivesArithScript.sml
new file mode 100644
index 00000000..d251a7cc
--- /dev/null
+++ b/backends/hol4/primitivesArithScript.sml
@@ -0,0 +1,147 @@
+open HolKernel boolLib bossLib Parse
+open boolTheory arithmeticTheory integerTheory intLib listTheory
+open primitivesBaseTacLib
+
+val _ = new_theory "primitivesArith"
+
+(* TODO: we need a better library of lemmas about arithmetic *)
+
+(* TODO: add those as rewriting theorems by default *)
+val NOT_LE_EQ_GT = store_thm("NOT_LE_EQ_GT", “!(x y: int). ~(x <= y) <=> x > y”, COOPER_TAC)
+val NOT_LT_EQ_GE = store_thm("NOT_LT_EQ_GE", “!(x y: int). ~(x < y) <=> x >= y”, COOPER_TAC)
+val NOT_GE_EQ_LT = store_thm("NOT_GE_EQ_LT", “!(x y: int). ~(x >= y) <=> x < y”, COOPER_TAC)
+val NOT_GT_EQ_LE = store_thm("NOT_GT_EQ_LE", “!(x y: int). ~(x > y) <=> x <= y”, COOPER_TAC)
+
+val GE_EQ_LE = store_thm("GE_EQ_LE", “!(x y : int). x >= y <=> y <= x”, COOPER_TAC)
+val LE_EQ_GE = store_thm("LE_EQ_GE", “!(x y : int). x <= y <=> y >= x”, COOPER_TAC)
+val GT_EQ_LT = store_thm("GT_EQ_LT", “!(x y : int). x > y <=> y < x”, COOPER_TAC)
+val LT_EQ_GT = store_thm("LT_EQ_GT", “!(x y : int). x < y <=> y > x”, COOPER_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
+
+Theorem POS_MUL_POS_IS_POS:
+  !(x y : int). 0 <= x ==> 0 <= y ==> 0 <= x * y
+Proof
+  rpt strip_tac >>
+  sg ‘0 <= &(Num x) * &(Num y)’ >- (rw [INT_MUL_CALCULATE] >> COOPER_TAC) >>
+  sg ‘&(Num x) = x’ >- (irule EQ_SYM >> rw [INT_OF_NUM] >> COOPER_TAC) >>
+  sg ‘&(Num y) = y’ >- (irule EQ_SYM >> rw [INT_OF_NUM] >> COOPER_TAC) >>
+  metis_tac[]
+QED
+
+Theorem POS_DIV_POS_IS_POS:
+  !(x y : int). 0 <= x ==> 0 < y ==> 0 <= x / y
+Proof
+  rpt strip_tac >>
+  rw [LE_EQ_GE] >>  
+  sg ‘y <> 0’ >- COOPER_TAC >>
+  qspecl_then [‘\x. x >= 0’, ‘x’, ‘y’] ASSUME_TAC INT_DIV_FORALL_P >>
+  fs [] >> POP_IGNORE_TAC >> rw [] >- COOPER_TAC >>
+  fs [NOT_LT_EQ_GE] >>
+  (* Proof by contradiction: assume k < 0 *)
+  spose_not_then ASSUME_TAC >>
+  fs [NOT_GE_EQ_LT] >>
+  sg ‘k * y = (k + 1) * y + - y’ >- (fs [INT_RDISTRIB] >> COOPER_TAC) >>
+  sg ‘0 <= (-(k + 1)) * y’ >- (irule POS_MUL_POS_IS_POS >> COOPER_TAC) >>
+  COOPER_TAC
+QED
+
+Theorem POS_DIV_POS_LE:
+  !(x y d : int). 0 <= x ==> 0 <= y ==> 0 < d ==> x <= y ==> x / d <= y / d
+Proof
+  rpt strip_tac >>
+  sg ‘d <> 0’ >- COOPER_TAC >>
+  qspecl_then [‘\k. k = x / d’, ‘x’, ‘d’] ASSUME_TAC INT_DIV_P >>
+  qspecl_then [‘\k. k = y / d’, ‘y’, ‘d’] ASSUME_TAC INT_DIV_P >>
+  rfs [NOT_LT_EQ_GE] >> TRY COOPER_TAC >>
+  sg ‘y = (x / d) * d + (r' + y - x)’ >- COOPER_TAC >>
+  qspecl_then [‘(x / d) * d’, ‘r' + y - x’, ‘d’] ASSUME_TAC INT_ADD_DIV >>
+  rfs [] >>
+  Cases_on ‘x = y’ >- fs [] >>
+  sg ‘r' + y ≠ x’ >- COOPER_TAC >> fs [] >>
+  sg ‘((x / d) * d) / d = x / d’ >- (irule INT_DIV_RMUL >> COOPER_TAC) >>
+  fs [] >>
+  sg ‘0 <= (r' + y − x) / d’ >- (irule POS_DIV_POS_IS_POS >> COOPER_TAC) >>
+  metis_tac [INT_LE_ADDR]
+QED
+
+Theorem POS_DIV_POS_LE_INIT:
+  !(x y : int). 0 <= x ==> 0 < y ==> x / y <= x
+Proof
+  rpt strip_tac >>
+  sg ‘y <> 0’ >- COOPER_TAC >>
+  qspecl_then [‘\k. k = x / y’, ‘x’, ‘y’] ASSUME_TAC INT_DIV_P >>
+  rfs [NOT_LT_EQ_GE] >- COOPER_TAC >>
+  sg ‘y = (y - 1) + 1’ >- rw [] >>
+  sg ‘x = x / y + ((x / y) * (y - 1) + r)’ >-(
+    qspecl_then [‘1’, ‘y-1’, ‘x / y’] ASSUME_TAC INT_LDISTRIB >>
+    rfs [] >>
+    COOPER_TAC
+  ) >>
+  sg ‘!a b c. 0 <= c ==> a = b + c ==> b <= a’ >- (COOPER_TAC) >>
+  pop_assum irule >>
+  exists_tac “x / y * (y − 1) + r” >>
+  sg ‘0 <= x / y’ >- (irule POS_DIV_POS_IS_POS >> COOPER_TAC) >>
+  sg ‘0 <= (x / y) * (y - 1)’ >- (irule POS_MUL_POS_IS_POS >> COOPER_TAC) >>
+  COOPER_TAC
+QED
+
+Theorem POS_MOD_POS_IS_POS:
+  !(x y : int). 0 <= x ==> 0 < y ==> 0 <= x % y
+Proof
+  rpt strip_tac >>
+  sg ‘y <> 0’ >- COOPER_TAC >>
+  imp_res_tac INT_DIVISION >>
+  first_x_assum (qspec_then ‘x’ assume_tac) >>
+  first_x_assum (qspec_then ‘x’ assume_tac) >>
+  sg ‘~(y < 0)’ >- COOPER_TAC >> fs []
+QED
+
+Theorem POS_MOD_POS_LE_INIT:
+  !(x y : int). 0 <= x ==> 0 < y ==> x % y <= x
+Proof
+  rpt strip_tac >>
+  sg ‘y <> 0’ >- COOPER_TAC >>
+  imp_res_tac INT_DIVISION >>
+  first_x_assum (qspec_then ‘x’ assume_tac) >>
+  first_x_assum (qspec_then ‘x’ assume_tac) >>
+  sg ‘~(y < 0)’ >- COOPER_TAC >> fs [] >>
+  sg ‘0 <= x % y’ >- (irule POS_MOD_POS_IS_POS >> COOPER_TAC) >>
+  sg ‘0 <= x / y’ >- (irule POS_DIV_POS_IS_POS >> COOPER_TAC) >>
+  sg ‘0 <= (x / y) * y’ >- (irule POS_MUL_POS_IS_POS >> COOPER_TAC) >>
+  COOPER_TAC
+QED
+
+val _ = export_theory ()
diff --git a/backends/hol4/primitivesArithTheory.sig b/backends/hol4/primitivesArithTheory.sig
new file mode 100644
index 00000000..3b157b87
--- /dev/null
+++ b/backends/hol4/primitivesArithTheory.sig
@@ -0,0 +1,100 @@
+signature primitivesArithTheory =
+sig
+  type thm = Thm.thm
+  
+  (*  Theorems  *)
+    val GE_EQ_LE : thm
+    val GT_EQ_LT : thm
+    val INT_OF_NUM_INJ : thm
+    val LE_EQ_GE : thm
+    val LT_EQ_GT : thm
+    val NOT_GE_EQ_LT : thm
+    val NOT_GT_EQ_LE : thm
+    val NOT_LE_EQ_GT : thm
+    val NOT_LT_EQ_GE : thm
+    val NUM_SUB_1_EQ : thm
+    val NUM_SUB_EQ : thm
+    val POS_DIV_POS_IS_POS : thm
+    val POS_DIV_POS_LE : thm
+    val POS_DIV_POS_LE_INIT : thm
+    val POS_MOD_POS_IS_POS : thm
+    val POS_MOD_POS_LE_INIT : thm
+    val POS_MUL_POS_IS_POS : thm
+  
+  val primitivesArith_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+   [Omega] Parent theory of "primitivesArith"
+   
+   [int_arith] Parent theory of "primitivesArith"
+   
+   [GE_EQ_LE]  Theorem
+      
+      ⊢ ∀x y. x ≥ y ⇔ y ≤ x
+   
+   [GT_EQ_LT]  Theorem
+      
+      ⊢ ∀x y. x > y ⇔ y < x
+   
+   [INT_OF_NUM_INJ]  Theorem
+      
+      ⊢ ∀n m. &n = &m ⇒ n = m
+   
+   [LE_EQ_GE]  Theorem
+      
+      ⊢ ∀x y. x ≤ y ⇔ y ≥ x
+   
+   [LT_EQ_GT]  Theorem
+      
+      ⊢ ∀x y. x < y ⇔ y > x
+   
+   [NOT_GE_EQ_LT]  Theorem
+      
+      ⊢ ∀x y. ¬(x ≥ y) ⇔ x < y
+   
+   [NOT_GT_EQ_LE]  Theorem
+      
+      ⊢ ∀x y. ¬(x > y) ⇔ x ≤ y
+   
+   [NOT_LE_EQ_GT]  Theorem
+      
+      ⊢ ∀x y. ¬(x ≤ y) ⇔ x > y
+   
+   [NOT_LT_EQ_GE]  Theorem
+      
+      ⊢ ∀x y. ¬(x < y) ⇔ x ≥ y
+   
+   [NUM_SUB_1_EQ]  Theorem
+      
+      ⊢ ∀x y. x = y − 1 ⇒ 0 ≤ x ⇒ Num y = SUC (Num x)
+   
+   [NUM_SUB_EQ]  Theorem
+      
+      ⊢ ∀x y z. x = y − z ⇒ 0 ≤ x ⇒ 0 ≤ z ⇒ Num y = Num z + Num x
+   
+   [POS_DIV_POS_IS_POS]  Theorem
+      
+      ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x / y
+   
+   [POS_DIV_POS_LE]  Theorem
+      
+      ⊢ ∀x y d. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 < d ⇒ x ≤ y ⇒ x / d ≤ y / d
+   
+   [POS_DIV_POS_LE_INIT]  Theorem
+      
+      ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x / y ≤ x
+   
+   [POS_MOD_POS_IS_POS]  Theorem
+      
+      ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x % y
+   
+   [POS_MOD_POS_LE_INIT]  Theorem
+      
+      ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x % y ≤ x
+   
+   [POS_MUL_POS_IS_POS]  Theorem
+      
+      ⊢ ∀x y. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 ≤ x * y
+   
+   
+*)
+end
diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml
new file mode 100644
index 00000000..3da1423b
--- /dev/null
+++ b/backends/hol4/primitivesBaseTacLib.sml
@@ -0,0 +1,16 @@
+(* Base tactics for the primitives library *)
+structure primitivesBaseTacLib =
+struct
+
+open HolKernel boolLib bossLib Parse
+open boolTheory arithmeticTheory integerTheory intLib listTheory
+
+(* Ignore a theorem.
+
+   To be used in conjunction with {!pop_assum} for instance.
+ *)
+fun IGNORE_TAC (_ : thm) : tactic = ALL_TAC
+
+val POP_IGNORE_TAC = POP_ASSUM IGNORE_TAC
+
+end
diff --git a/backends/hol4/primitivesLib.sml b/backends/hol4/primitivesLib.sml
new file mode 100644
index 00000000..5803c531
--- /dev/null
+++ b/backends/hol4/primitivesLib.sml
@@ -0,0 +1,9 @@
+(* Advanced tactics for the primitives library *)
+structure primitivesBaseTacLib =
+struct
+
+open HolKernel boolLib bossLib Parse
+open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
+open primitivesBaseTacLib primitivesTheory
+
+end
diff --git a/backends/hol4/PrimitivesScript.sml b/backends/hol4/primitivesScript.sml
index 1f8bb1a5..56a876d4 100644
--- a/backends/hol4/PrimitivesScript.sml
+++ b/backends/hol4/primitivesScript.sml
@@ -1,7 +1,9 @@
 open HolKernel boolLib bossLib Parse
 open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
 
-val primitives_theory_name = "Primitives"
+open primitivesArithTheory
+
+val primitives_theory_name = "primitives"
 val _ = new_theory primitives_theory_name
 
 (*** Result *)
@@ -502,120 +504,6 @@ val all_rem_defs = [
   u128_rem_def
 ]
 
-(* Ignore a theorem.
-
-   To be used in conjunction with {!pop_assum} for instance.
- *)
-fun IGNORE_TAC (_ : thm) : tactic = ALL_TAC
-
-val POP_IGNORE_TAC = POP_ASSUM IGNORE_TAC
-
-(* TODO: we need a better library of lemmas about arithmetic *)
-
-(* TODO: add those as rewriting tactics by default *)
-val NOT_LE_EQ_GT = store_thm("NOT_LE_EQ_GT", “!(x y: int). ~(x <= y) <=> x > y”, COOPER_TAC)
-val NOT_LT_EQ_GE = store_thm("NOT_LT_EQ_GE", “!(x y: int). ~(x < y) <=> x >= y”, COOPER_TAC)
-val NOT_GE_EQ_LT = store_thm("NOT_GE_EQ_LT", “!(x y: int). ~(x >= y) <=> x < y”, COOPER_TAC)
-val NOT_GT_EQ_LE = store_thm("NOT_GT_EQ_LE", “!(x y: int). ~(x > y) <=> x <= y”, COOPER_TAC)
-
-Theorem POS_MUL_POS_IS_POS:
-  !(x y : int). 0 <= x ==> 0 <= y ==> 0 <= x * y
-Proof
-  rpt strip_tac >>
-  sg ‘0 <= &(Num x) * &(Num y)’ >- (rw [INT_MUL_CALCULATE] >> COOPER_TAC) >>
-  sg ‘&(Num x) = x’ >- (irule EQ_SYM >> rw [INT_OF_NUM] >> COOPER_TAC) >>
-  sg ‘&(Num y) = y’ >- (irule EQ_SYM >> rw [INT_OF_NUM] >> COOPER_TAC) >>
-  metis_tac[]
-QED
-
-val GE_EQ_LE = store_thm("GE_EQ_LE", “!(x y : int). x >= y <=> y <= x”, COOPER_TAC)
-val LE_EQ_GE = store_thm("LE_EQ_GE", “!(x y : int). x <= y <=> y >= x”, COOPER_TAC)
-val GT_EQ_LT = store_thm("GT_EQ_LT", “!(x y : int). x > y <=> y < x”, COOPER_TAC)
-val LT_EQ_GT = store_thm("LT_EQ_GT", “!(x y : int). x < y <=> y > x”, COOPER_TAC)
-
-Theorem POS_DIV_POS_IS_POS:
-  !(x y : int). 0 <= x ==> 0 < y ==> 0 <= x / y
-Proof
-  rpt strip_tac >>
-  rw [LE_EQ_GE] >>  
-  sg ‘y <> 0’ >- COOPER_TAC >>
-  qspecl_then [‘\x. x >= 0’, ‘x’, ‘y’] ASSUME_TAC INT_DIV_FORALL_P >>
-  fs [] >> POP_IGNORE_TAC >> rw [] >- COOPER_TAC >>
-  fs [NOT_LT_EQ_GE] >>
-  (* Proof by contradiction: assume k < 0 *)
-  spose_not_then ASSUME_TAC >>
-  fs [NOT_GE_EQ_LT] >>
-  sg ‘k * y = (k + 1) * y + - y’ >- (fs [INT_RDISTRIB] >> COOPER_TAC) >>
-  sg ‘0 <= (-(k + 1)) * y’ >- (irule POS_MUL_POS_IS_POS >> COOPER_TAC) >>
-  COOPER_TAC
-QED
-
-Theorem POS_DIV_POS_LE:
-  !(x y d : int). 0 <= x ==> 0 <= y ==> 0 < d ==> x <= y ==> x / d <= y / d
-Proof
-  rpt strip_tac >>
-  sg ‘d <> 0’ >- COOPER_TAC >>
-  qspecl_then [‘\k. k = x / d’, ‘x’, ‘d’] ASSUME_TAC INT_DIV_P >>
-  qspecl_then [‘\k. k = y / d’, ‘y’, ‘d’] ASSUME_TAC INT_DIV_P >>
-  rfs [NOT_LT_EQ_GE] >> TRY COOPER_TAC >>
-  sg ‘y = (x / d) * d + (r' + y - x)’ >- COOPER_TAC >>
-  qspecl_then [‘(x / d) * d’, ‘r' + y - x’, ‘d’] ASSUME_TAC INT_ADD_DIV >>
-  rfs [] >>
-  Cases_on ‘x = y’ >- fs [] >>
-  sg ‘r' + y ≠ x’ >- COOPER_TAC >> fs [] >>
-  sg ‘((x / d) * d) / d = x / d’ >- (irule INT_DIV_RMUL >> COOPER_TAC) >>
-  fs [] >>
-  sg ‘0 <= (r' + y − x) / d’ >- (irule POS_DIV_POS_IS_POS >> COOPER_TAC) >>
-  metis_tac [INT_LE_ADDR]
-QED
-
-Theorem POS_DIV_POS_LE_INIT:
-  !(x y : int). 0 <= x ==> 0 < y ==> x / y <= x
-Proof
-  rpt strip_tac >>
-  sg ‘y <> 0’ >- COOPER_TAC >>
-  qspecl_then [‘\k. k = x / y’, ‘x’, ‘y’] ASSUME_TAC INT_DIV_P >>
-  rfs [NOT_LT_EQ_GE] >- COOPER_TAC >>
-  sg ‘y = (y - 1) + 1’ >- rw [] >>
-  sg ‘x = x / y + ((x / y) * (y - 1) + r)’ >-(
-    qspecl_then [‘1’, ‘y-1’, ‘x / y’] ASSUME_TAC INT_LDISTRIB >>
-    rfs [] >>
-    COOPER_TAC
-  ) >>
-  sg ‘!a b c. 0 <= c ==> a = b + c ==> b <= a’ >- (COOPER_TAC) >>
-  pop_assum irule >>
-  exists_tac “x / y * (y − 1) + r” >>
-  sg ‘0 <= x / y’ >- (irule POS_DIV_POS_IS_POS >> COOPER_TAC) >>
-  sg ‘0 <= (x / y) * (y - 1)’ >- (irule POS_MUL_POS_IS_POS >> COOPER_TAC) >>
-  COOPER_TAC
-QED
-
-Theorem POS_MOD_POS_IS_POS:
-  !(x y : int). 0 <= x ==> 0 < y ==> 0 <= x % y
-Proof
-  rpt strip_tac >>
-  sg ‘y <> 0’ >- COOPER_TAC >>
-  imp_res_tac INT_DIVISION >>
-  first_x_assum (qspec_then ‘x’ assume_tac) >>
-  first_x_assum (qspec_then ‘x’ assume_tac) >>
-  sg ‘~(y < 0)’ >- COOPER_TAC >> fs []
-QED
-
-Theorem POS_MOD_POS_LE_INIT:
-  !(x y : int). 0 <= x ==> 0 < y ==> x % y <= x
-Proof
-  rpt strip_tac >>
-  sg ‘y <> 0’ >- COOPER_TAC >>
-  imp_res_tac INT_DIVISION >>
-  first_x_assum (qspec_then ‘x’ assume_tac) >>
-  first_x_assum (qspec_then ‘x’ assume_tac) >>
-  sg ‘~(y < 0)’ >- COOPER_TAC >> fs [] >>
-  sg ‘0 <= x % y’ >- (irule POS_MOD_POS_IS_POS >> COOPER_TAC) >>
-  sg ‘0 <= x / y’ >- (irule POS_DIV_POS_IS_POS >> COOPER_TAC) >>
-  sg ‘0 <= (x / y) * y’ >- (irule POS_MUL_POS_IS_POS >> COOPER_TAC) >>
-  COOPER_TAC
-QED
-
 (*
 val (asms,g) = top_goal ()
 *)
@@ -1353,4 +1241,30 @@ val all_div_eqs = [
   U128_DIV_EQ
 ]
 
+(***
+ * Vectors
+ *)
+
+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)))’
+
+
 val _ = export_theory ()
diff --git a/backends/hol4/PrimitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index 8ec350e7..75098bfe 100644
--- a/backends/hol4/PrimitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -1,8 +1,9 @@
-signature PrimitivesTheory =
+signature primitivesTheory =
 sig
   type thm = Thm.thm
   
   (*  Axioms  *)
+    val VEC_TO_LIST_BOUNDS : thm
     val i128_to_int_bounds : thm
     val i16_to_int_bounds : thm
     val i32_to_int_bounds : thm
@@ -131,10 +132,9 @@ sig
     val usize_mul_def : thm
     val usize_rem_def : thm
     val usize_sub_def : thm
+    val vec_len_def : thm
   
   (*  Theorems  *)
-    val GE_EQ_LE : thm
-    val GT_EQ_LT : thm
     val I128_ADD_EQ : thm
     val I128_DIV_EQ : thm
     val I128_MUL_EQ : thm
@@ -163,18 +163,6 @@ sig
     val ISIZE_DIV_EQ : thm
     val ISIZE_MUL_EQ : thm
     val ISIZE_SUB_EQ : thm
-    val LE_EQ_GE : thm
-    val LT_EQ_GT : thm
-    val NOT_GE_EQ_LT : thm
-    val NOT_GT_EQ_LE : thm
-    val NOT_LE_EQ_GT : thm
-    val NOT_LT_EQ_GE : thm
-    val POS_DIV_POS_IS_POS : thm
-    val POS_DIV_POS_LE : thm
-    val POS_DIV_POS_LE_INIT : thm
-    val POS_MOD_POS_IS_POS : thm
-    val POS_MOD_POS_LE_INIT : thm
-    val POS_MUL_POS_IS_POS : thm
     val U128_ADD_EQ : thm
     val U128_DIV_EQ : thm
     val U128_MUL_EQ : thm
@@ -205,6 +193,7 @@ sig
     val USIZE_MUL_EQ : thm
     val USIZE_REM_EQ : thm
     val USIZE_SUB_EQ : thm
+    val VEC_TO_LIST_INT_BOUNDS : thm
     val datatype_error : thm
     val datatype_result : thm
     val error2num_11 : thm
@@ -230,13 +219,11 @@ sig
     val result_induction : thm
     val result_nchotomy : thm
   
-  val Primitives_grammars : type_grammar.grammar * term_grammar.grammar
+  val primitives_grammars : type_grammar.grammar * term_grammar.grammar
 (*
-   [Omega] Parent theory of "Primitives"
+   [primitivesArith] Parent theory of "primitives"
    
-   [int_arith] Parent theory of "Primitives"
-   
-   [string] Parent theory of "Primitives"
+   [string] Parent theory of "primitives"
    
    [int_to_u128_id]  Axiom
       
@@ -369,6 +356,11 @@ sig
       [oracles: ] [axioms: isize_bounds] []
       ⊢ isize_min ≤ i16_min ∧ isize_max ≥ i16_max
    
+   [VEC_TO_LIST_BOUNDS]  Axiom
+      
+      [oracles: ] [axioms: VEC_TO_LIST_BOUNDS] []
+      ⊢ ∀v. (let l = LENGTH (vec_to_list v) in 0 ≤ l ∧ l ≤ 4294967295)
+   
    [bind_def]  Definition
       
       ⊢ ∀x f.
@@ -891,13 +883,9 @@ sig
       
       ⊢ ∀x y. usize_sub x y = mk_usize (usize_to_int x − usize_to_int y)
    
-   [GE_EQ_LE]  Theorem
-      
-      ⊢ ∀x y. x ≥ y ⇔ y ≤ x
-   
-   [GT_EQ_LT]  Theorem
+   [vec_len_def]  Definition
       
-      ⊢ ∀x y. x > y ⇔ y < x
+      ⊢ ∀v. vec_len v = int_to_u32 (&LENGTH (vec_to_list v))
    
    [I128_ADD_EQ]  Theorem
       
@@ -1205,54 +1193,6 @@ sig
           ∃z. isize_sub x y = Return z ∧
               isize_to_int z = isize_to_int x − isize_to_int y
    
-   [LE_EQ_GE]  Theorem
-      
-      ⊢ ∀x y. x ≤ y ⇔ y ≥ x
-   
-   [LT_EQ_GT]  Theorem
-      
-      ⊢ ∀x y. x < y ⇔ y > x
-   
-   [NOT_GE_EQ_LT]  Theorem
-      
-      ⊢ ∀x y. ¬(x ≥ y) ⇔ x < y
-   
-   [NOT_GT_EQ_LE]  Theorem
-      
-      ⊢ ∀x y. ¬(x > y) ⇔ x ≤ y
-   
-   [NOT_LE_EQ_GT]  Theorem
-      
-      ⊢ ∀x y. ¬(x ≤ y) ⇔ x > y
-   
-   [NOT_LT_EQ_GE]  Theorem
-      
-      ⊢ ∀x y. ¬(x < y) ⇔ x ≥ y
-   
-   [POS_DIV_POS_IS_POS]  Theorem
-      
-      ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x / y
-   
-   [POS_DIV_POS_LE]  Theorem
-      
-      ⊢ ∀x y d. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 < d ⇒ x ≤ y ⇒ x / d ≤ y / d
-   
-   [POS_DIV_POS_LE_INIT]  Theorem
-      
-      ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x / y ≤ x
-   
-   [POS_MOD_POS_IS_POS]  Theorem
-      
-      ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x % y
-   
-   [POS_MOD_POS_LE_INIT]  Theorem
-      
-      ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x % y ≤ x
-   
-   [POS_MUL_POS_IS_POS]  Theorem
-      
-      ⊢ ∀x y. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 ≤ x * y
-   
    [U128_ADD_EQ]  Theorem
       
       [oracles: DISK_THM]
@@ -1555,6 +1495,11 @@ sig
           ∃z. usize_sub x y = Return z ∧
               usize_to_int z = usize_to_int x − usize_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)
diff --git a/backends/hol4/TestScript.sml b/backends/hol4/testScript.sml
index 2eb3f23b..fe1c1e11 100644
--- a/backends/hol4/TestScript.sml
+++ b/backends/hol4/testScript.sml
@@ -1,6 +1,6 @@
 open HolKernel boolLib bossLib Parse
 
-val primitives_theory_name = "Test"
+val primitives_theory_name = "test"
 val _ = new_theory primitives_theory_name
 
 open boolTheory integerTheory wordsTheory stringTheory
diff --git a/backends/hol4/testTheory.sig b/backends/hol4/testTheory.sig
new file mode 100644
index 00000000..c1034394
--- /dev/null
+++ b/backends/hol4/testTheory.sig
@@ -0,0 +1,839 @@
+signature testTheory =
+sig
+  type thm = Thm.thm
+  
+  (*  Axioms  *)
+    val VEC_TO_LIST_BOUNDS : thm
+    val i32_to_int_bounds : thm
+    val insert_def : thm
+    val int_to_i32_id : thm
+    val int_to_u32_id : thm
+    val u32_to_int_bounds : thm
+  
+  (*  Definitions  *)
+    val distinct_keys_def : thm
+    val error_BIJ : thm
+    val error_CASE : thm
+    val error_TY_DEF : thm
+    val error_size_def : thm
+    val i32_add_def : thm
+    val i32_max_def : thm
+    val i32_min_def : thm
+    val int1_def : thm
+    val int2_def : thm
+    val is_loop_def : thm
+    val is_true_def : thm
+    val list_t_TY_DEF : thm
+    val list_t_case_def : thm
+    val list_t_size_def : thm
+    val list_t_v_def : thm
+    val lookup_def : thm
+    val mk_i32_def : thm
+    val mk_u32_def : thm
+    val nth_expand_def : thm
+    val nth_fuel_P_def : thm
+    val result_TY_DEF : thm
+    val result_case_def : thm
+    val result_size_def : thm
+    val st_ex_bind_def : thm
+    val st_ex_return_def : thm
+    val test1_def : thm
+    val test2_TY_DEF : thm
+    val test2_case_def : thm
+    val test2_size_def : thm
+    val test_TY_DEF : thm
+    val test_case_def : thm
+    val test_monad2_def : thm
+    val test_monad3_def : thm
+    val test_monad_def : thm
+    val test_size_def : thm
+    val u32_add_def : thm
+    val u32_max_def : thm
+    val u32_sub_def : thm
+    val usize_max_def : thm
+    val vec_len_def : thm
+  
+  (*  Theorems  *)
+    val I32_ADD_EQ : thm
+    val INT_OF_NUM_INJ : thm
+    val INT_THM1 : thm
+    val INT_THM2 : thm
+    val MK_I32_SUCCESS : thm
+    val MK_U32_SUCCESS : thm
+    val NAT_THM1 : thm
+    val NAT_THM2 : thm
+    val NUM_SUB_1_EQ : thm
+    val NUM_SUB_1_EQ1 : thm
+    val NUM_SUB_EQ : thm
+    val U32_ADD_EQ : thm
+    val U32_SUB_EQ : thm
+    val VEC_TO_LIST_INT_BOUNDS : thm
+    val datatype_error : thm
+    val datatype_list_t : thm
+    val datatype_result : thm
+    val datatype_test : thm
+    val datatype_test2 : thm
+    val error2num_11 : thm
+    val error2num_ONTO : thm
+    val error2num_num2error : thm
+    val error2num_thm : thm
+    val error_Axiom : thm
+    val error_EQ_error : thm
+    val error_case_cong : thm
+    val error_case_def : thm
+    val error_case_eq : thm
+    val error_induction : thm
+    val error_nchotomy : thm
+    val insert_lem : thm
+    val list_nth_mut_loop_loop_fwd_def : thm
+    val list_nth_mut_loop_loop_fwd_ind : thm
+    val list_t_11 : thm
+    val list_t_Axiom : thm
+    val list_t_case_cong : thm
+    val list_t_case_eq : thm
+    val list_t_distinct : thm
+    val list_t_induction : thm
+    val list_t_nchotomy : thm
+    val lookup_raw_def : thm
+    val lookup_raw_ind : thm
+    val nth_def : thm
+    val nth_def_loop : thm
+    val nth_def_terminates : thm
+    val nth_fuel_P_mono : thm
+    val nth_fuel_def : thm
+    val nth_fuel_ind : thm
+    val nth_fuel_least_fail_mono : thm
+    val nth_fuel_least_success_mono : thm
+    val nth_fuel_mono : thm
+    val num2error_11 : thm
+    val num2error_ONTO : thm
+    val num2error_error2num : thm
+    val num2error_thm : thm
+    val result_11 : thm
+    val result_Axiom : thm
+    val result_case_cong : thm
+    val result_case_eq : thm
+    val result_distinct : thm
+    val result_induction : thm
+    val result_nchotomy : thm
+    val test2_11 : thm
+    val test2_Axiom : thm
+    val test2_case_cong : thm
+    val test2_case_eq : thm
+    val test2_distinct : thm
+    val test2_induction : thm
+    val test2_nchotomy : thm
+    val test_11 : thm
+    val test_Axiom : thm
+    val test_case_cong : thm
+    val test_case_eq : thm
+    val test_distinct : thm
+    val test_induction : thm
+    val test_nchotomy : thm
+  
+  val test_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+   [Omega] Parent theory of "test"
+   
+   [int_arith] Parent theory of "test"
+   
+   [words] Parent theory of "test"
+   
+   [insert_def]  Axiom
+      
+      [oracles: ] [axioms: insert_def] []
+      ⊢ insert key value ls =
+        case ls of
+          ListCons (ckey,cvalue) tl =>
+            if ckey = key then Return (ListCons (ckey,value) tl)
+            else
+              do
+                tl0 <- insert key value tl;
+                Return (ListCons (ckey,cvalue) tl0)
+              od
+        | ListNil => Return (ListCons (key,value) ListNil)
+   
+   [u32_to_int_bounds]  Axiom
+      
+      [oracles: ] [axioms: u32_to_int_bounds] []
+      ⊢ ∀n. 0 ≤ u32_to_int n ∧ u32_to_int n ≤ u32_max
+   
+   [i32_to_int_bounds]  Axiom
+      
+      [oracles: ] [axioms: i32_to_int_bounds] []
+      ⊢ ∀n. i32_min ≤ i32_to_int n ∧ i32_to_int n ≤ i32_max
+   
+   [int_to_u32_id]  Axiom
+      
+      [oracles: ] [axioms: int_to_u32_id] []
+      ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ u32_to_int (int_to_u32 n) = n
+   
+   [int_to_i32_id]  Axiom
+      
+      [oracles: ] [axioms: int_to_i32_id] []
+      ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ i32_to_int (int_to_i32 n) = n
+   
+   [VEC_TO_LIST_BOUNDS]  Axiom
+      
+      [oracles: ] [axioms: VEC_TO_LIST_BOUNDS] []
+      ⊢ ∀v. (let l = LENGTH (vec_to_list v) in 0 ≤ l ∧ l ≤ 4294967295)
+   
+   [distinct_keys_def]  Definition
+      
+      ⊢ ∀ls.
+          distinct_keys ls ⇔
+          ∀i j.
+            i < LENGTH ls ⇒
+            j < LENGTH ls ⇒
+            FST (EL i ls) = FST (EL j ls) ⇒
+            i = j
+   
+   [error_BIJ]  Definition
+      
+      ⊢ (∀a. num2error (error2num a) = a) ∧
+        ∀r. (λn. n < 1) r ⇔ error2num (num2error r) = r
+   
+   [error_CASE]  Definition
+      
+      ⊢ ∀x v0. (case x of Failure => v0) = (λm. v0) (error2num x)
+   
+   [error_TY_DEF]  Definition
+      
+      ⊢ ∃rep. TYPE_DEFINITION (λn. n < 1) rep
+   
+   [error_size_def]  Definition
+      
+      ⊢ ∀x. error_size x = 0
+   
+   [i32_add_def]  Definition
+      
+      ⊢ ∀x y. i32_add x y = mk_i32 (i32_to_int x + i32_to_int y)
+   
+   [i32_max_def]  Definition
+      
+      ⊢ i32_max = 2147483647
+   
+   [i32_min_def]  Definition
+      
+      ⊢ i32_min = -2147483648
+   
+   [int1_def]  Definition
+      
+      ⊢ int1 = 32
+   
+   [int2_def]  Definition
+      
+      ⊢ int2 = -32
+   
+   [is_loop_def]  Definition
+      
+      ⊢ ∀r. is_loop r ⇔ case r of Return v2 => F | Fail v3 => F | Loop => T
+   
+   [is_true_def]  Definition
+      
+      ⊢ ∀x. is_true x = if x then Return () else Fail Failure
+   
+   [list_t_TY_DEF]  Definition
+      
+      ⊢ ∃rep.
+          TYPE_DEFINITION
+            (λa0'.
+                 ∀ $var$('list_t').
+                   (∀a0'.
+                      (∃a0 a1.
+                         a0' =
+                         (λa0 a1.
+                              ind_type$CONSTR 0 a0
+                                (ind_type$FCONS a1 (λn. ind_type$BOTTOM)))
+                           a0 a1 ∧ $var$('list_t') a1) ∨
+                      a0' =
+                      ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒
+                      $var$('list_t') a0') ⇒
+                   $var$('list_t') a0') rep
+   
+   [list_t_case_def]  Definition
+      
+      ⊢ (∀a0 a1 f v. list_t_CASE (ListCons a0 a1) f v = f a0 a1) ∧
+        ∀f v. list_t_CASE ListNil f v = v
+   
+   [list_t_size_def]  Definition
+      
+      ⊢ (∀f a0 a1.
+           list_t_size f (ListCons a0 a1) = 1 + (f a0 + list_t_size f a1)) ∧
+        ∀f. list_t_size f ListNil = 0
+   
+   [list_t_v_def]  Definition
+      
+      ⊢ list_t_v ListNil = [] ∧
+        ∀x tl. list_t_v (ListCons x tl) = x::list_t_v tl
+   
+   [lookup_def]  Definition
+      
+      ⊢ ∀key ls. lookup key ls = lookup_raw key (list_t_v ls)
+   
+   [mk_i32_def]  Definition
+      
+      ⊢ ∀n. mk_i32 n =
+            if i32_min ≤ n ∧ n ≤ i32_max then Return (int_to_i32 n)
+            else Fail Failure
+   
+   [mk_u32_def]  Definition
+      
+      ⊢ ∀n. mk_u32 n =
+            if 0 ≤ n ∧ n ≤ u32_max then Return (int_to_u32 n)
+            else Fail Failure
+   
+   [nth_expand_def]  Definition
+      
+      ⊢ ∀nth ls i.
+          nth_expand nth ls i =
+          case ls of
+            ListCons x tl =>
+              if u32_to_int i = 0 then Return x
+              else do i0 <- u32_sub i (int_to_u32 1); nth tl i0 od
+          | ListNil => Fail Failure
+   
+   [nth_fuel_P_def]  Definition
+      
+      ⊢ ∀ls i n. nth_fuel_P ls i n ⇔ ¬is_loop (nth_fuel n ls i)
+   
+   [result_TY_DEF]  Definition
+      
+      ⊢ ∃rep.
+          TYPE_DEFINITION
+            (λa0.
+                 ∀ $var$('result').
+                   (∀a0.
+                      (∃a. a0 =
+                           (λa.
+                                ind_type$CONSTR 0 (a,ARB)
+                                  (λn. ind_type$BOTTOM)) a) ∨
+                      (∃a. a0 =
+                           (λa.
+                                ind_type$CONSTR (SUC 0) (ARB,a)
+                                  (λn. ind_type$BOTTOM)) a) ∨
+                      a0 =
+                      ind_type$CONSTR (SUC (SUC 0)) (ARB,ARB)
+                        (λn. ind_type$BOTTOM) ⇒
+                      $var$('result') a0) ⇒
+                   $var$('result') a0) rep
+   
+   [result_case_def]  Definition
+      
+      ⊢ (∀a f f1 v. result_CASE (Return a) f f1 v = f a) ∧
+        (∀a f f1 v. result_CASE (Fail a) f f1 v = f1 a) ∧
+        ∀f f1 v. result_CASE Loop f f1 v = v
+   
+   [result_size_def]  Definition
+      
+      ⊢ (∀f a. result_size f (Return a) = 1 + f a) ∧
+        (∀f a. result_size f (Fail a) = 1 + error_size a) ∧
+        ∀f. result_size f Loop = 0
+   
+   [st_ex_bind_def]  Definition
+      
+      ⊢ ∀x f.
+          monad_bind x f =
+          case x of Return y => f y | Fail e => Fail e | Loop => Loop
+   
+   [st_ex_return_def]  Definition
+      
+      ⊢ ∀x. st_ex_return x = Return x
+   
+   [test1_def]  Definition
+      
+      ⊢ ∀x. test1 x = Return x
+   
+   [test2_TY_DEF]  Definition
+      
+      ⊢ ∃rep.
+          TYPE_DEFINITION
+            (λa0.
+                 ∀ $var$('test2').
+                   (∀a0.
+                      (∃a. a0 =
+                           (λa.
+                                ind_type$CONSTR 0 (a,ARB)
+                                  (λn. ind_type$BOTTOM)) a) ∨
+                      (∃a. a0 =
+                           (λa.
+                                ind_type$CONSTR (SUC 0) (ARB,a)
+                                  (λn. ind_type$BOTTOM)) a) ⇒
+                      $var$('test2') a0) ⇒
+                   $var$('test2') a0) rep
+   
+   [test2_case_def]  Definition
+      
+      ⊢ (∀a f f1. test2_CASE (Variant1_2 a) f f1 = f a) ∧
+        ∀a f f1. test2_CASE (Variant2_2 a) f f1 = f1 a
+   
+   [test2_size_def]  Definition
+      
+      ⊢ (∀f f1 a. test2_size f f1 (Variant1_2 a) = 1 + f a) ∧
+        ∀f f1 a. test2_size f f1 (Variant2_2 a) = 1 + f1 a
+   
+   [test_TY_DEF]  Definition
+      
+      ⊢ ∃rep.
+          TYPE_DEFINITION
+            (λa0.
+                 ∀ $var$('test').
+                   (∀a0.
+                      (∃a. a0 =
+                           (λa.
+                                ind_type$CONSTR 0 (a,ARB)
+                                  (λn. ind_type$BOTTOM)) a) ∨
+                      (∃a. a0 =
+                           (λa.
+                                ind_type$CONSTR (SUC 0) (ARB,a)
+                                  (λn. ind_type$BOTTOM)) a) ⇒
+                      $var$('test') a0) ⇒
+                   $var$('test') a0) rep
+   
+   [test_case_def]  Definition
+      
+      ⊢ (∀a f f1. test_CASE (Variant1 a) f f1 = f a) ∧
+        ∀a f f1. test_CASE (Variant2 a) f f1 = f1 a
+   
+   [test_monad2_def]  Definition
+      
+      ⊢ test_monad2 = do x <- Return T; Return x od
+   
+   [test_monad3_def]  Definition
+      
+      ⊢ ∀x. test_monad3 x = monad_ignore_bind (is_true x) (Return x)
+   
+   [test_monad_def]  Definition
+      
+      ⊢ ∀v. test_monad v = do x <- Return v; Return x od
+   
+   [test_size_def]  Definition
+      
+      ⊢ (∀f f1 a. test_size f f1 (Variant1 a) = 1 + f1 a) ∧
+        ∀f f1 a. test_size f f1 (Variant2 a) = 1 + f a
+   
+   [u32_add_def]  Definition
+      
+      ⊢ ∀x y. u32_add x y = mk_u32 (u32_to_int x + u32_to_int y)
+   
+   [u32_max_def]  Definition
+      
+      ⊢ u32_max = 4294967295
+   
+   [u32_sub_def]  Definition
+      
+      ⊢ ∀x y. u32_sub x y = mk_u32 (u32_to_int x − u32_to_int y)
+   
+   [usize_max_def]  Definition
+      
+      ⊢ usize_max = 4294967295
+   
+   [vec_len_def]  Definition
+      
+      ⊢ ∀v. vec_len v = int_to_u32 (&LENGTH (vec_to_list v))
+   
+   [I32_ADD_EQ]  Theorem
+      
+      [oracles: DISK_THM] [axioms: int_to_i32_id] []
+      ⊢ ∀x y.
+          i32_min ≤ i32_to_int x + i32_to_int y ⇒
+          i32_to_int x + i32_to_int y ≤ i32_max ⇒
+          ∃z. i32_add x y = Return z ∧
+              i32_to_int z = i32_to_int x + i32_to_int y
+   
+   [INT_OF_NUM_INJ]  Theorem
+      
+      ⊢ ∀n m. &n = &m ⇒ n = m
+   
+   [INT_THM1]  Theorem
+      
+      ⊢ ∀x y. x > 0 ⇒ y > 0 ⇒ x + y > 0
+   
+   [INT_THM2]  Theorem
+      
+      ⊢ ∀x. T
+   
+   [MK_I32_SUCCESS]  Theorem
+      
+      ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ mk_i32 n = Return (int_to_i32 n)
+   
+   [MK_U32_SUCCESS]  Theorem
+      
+      ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ mk_u32 n = Return (int_to_u32 n)
+   
+   [NAT_THM1]  Theorem
+      
+      ⊢ ∀n. n < n + 1
+   
+   [NAT_THM2]  Theorem
+      
+      ⊢ ∀n. n < n + 1
+   
+   [NUM_SUB_1_EQ]  Theorem
+      
+      ⊢ ∀x y. x = y − 1 ⇒ 0 ≤ x ⇒ Num y = SUC (Num x)
+   
+   [NUM_SUB_1_EQ1]  Theorem
+      
+      ⊢ ∀i. 0 ≤ i − 1 ⇒ Num i = SUC (Num (i − 1))
+   
+   [NUM_SUB_EQ]  Theorem
+      
+      ⊢ ∀x y z. x = y − z ⇒ 0 ≤ x ⇒ 0 ≤ z ⇒ Num y = Num z + Num x
+   
+   [U32_ADD_EQ]  Theorem
+      
+      [oracles: DISK_THM] [axioms: int_to_u32_id, u32_to_int_bounds] []
+      ⊢ ∀x y.
+          u32_to_int x + u32_to_int y ≤ u32_max ⇒
+          ∃z. u32_add x y = Return z ∧
+              u32_to_int z = u32_to_int x + u32_to_int y
+   
+   [U32_SUB_EQ]  Theorem
+      
+      [oracles: DISK_THM] [axioms: int_to_u32_id, u32_to_int_bounds] []
+      ⊢ ∀x y.
+          0 ≤ u32_to_int x − u32_to_int y ⇒
+          ∃z. u32_sub x y = Return z ∧
+              u32_to_int z = u32_to_int x − u32_to_int y
+   
+   [VEC_TO_LIST_INT_BOUNDS]  Theorem
+      
+      [oracles: DISK_THM] [axioms: VEC_TO_LIST_BOUNDS] []
+      ⊢ ∀v. (let l = &LENGTH (vec_to_list v) in 0 ≤ l ∧ l ≤ u32_max)
+   
+   [datatype_error]  Theorem
+      
+      ⊢ DATATYPE (error Failure)
+   
+   [datatype_list_t]  Theorem
+      
+      ⊢ DATATYPE (list_t ListCons ListNil)
+   
+   [datatype_result]  Theorem
+      
+      ⊢ DATATYPE (result Return Fail Loop)
+   
+   [datatype_test]  Theorem
+      
+      ⊢ DATATYPE (test Variant1 Variant2)
+   
+   [datatype_test2]  Theorem
+      
+      ⊢ DATATYPE (test2 Variant1_2 Variant2_2)
+   
+   [error2num_11]  Theorem
+      
+      ⊢ ∀a a'. error2num a = error2num a' ⇔ a = a'
+   
+   [error2num_ONTO]  Theorem
+      
+      ⊢ ∀r. r < 1 ⇔ ∃a. r = error2num a
+   
+   [error2num_num2error]  Theorem
+      
+      ⊢ ∀r. r < 1 ⇔ error2num (num2error r) = r
+   
+   [error2num_thm]  Theorem
+      
+      ⊢ error2num Failure = 0
+   
+   [error_Axiom]  Theorem
+      
+      ⊢ ∀x0. ∃f. f Failure = x0
+   
+   [error_EQ_error]  Theorem
+      
+      ⊢ ∀a a'. a = a' ⇔ error2num a = error2num a'
+   
+   [error_case_cong]  Theorem
+      
+      ⊢ ∀M M' v0.
+          M = M' ∧ (M' = Failure ⇒ v0 = v0') ⇒
+          (case M of Failure => v0) = case M' of Failure => v0'
+   
+   [error_case_def]  Theorem
+      
+      ⊢ ∀v0. (case Failure of Failure => v0) = v0
+   
+   [error_case_eq]  Theorem
+      
+      ⊢ (case x of Failure => v0) = v ⇔ x = Failure ∧ v0 = v
+   
+   [error_induction]  Theorem
+      
+      ⊢ ∀P. P Failure ⇒ ∀a. P a
+   
+   [error_nchotomy]  Theorem
+      
+      ⊢ ∀a. a = Failure
+   
+   [insert_lem]  Theorem
+      
+      [oracles: DISK_THM] [axioms: u32_to_int_bounds, insert_def] []
+      ⊢ ∀ls key value.
+          distinct_keys (list_t_v ls) ⇒
+          case insert key value ls of
+            Return ls1 =>
+              lookup key ls1 = SOME value ∧
+              ∀k. k ≠ key ⇒ lookup k ls = lookup k ls1
+          | Fail v1 => F
+          | Loop => F
+   
+   [list_nth_mut_loop_loop_fwd_def]  Theorem
+      
+      ⊢ ∀ls i.
+          list_nth_mut_loop_loop_fwd ls i =
+          case ls of
+            ListCons x tl =>
+              if u32_to_int i = 0 then Return x
+              else
+                do
+                  i0 <- u32_sub i (int_to_u32 1);
+                  list_nth_mut_loop_loop_fwd tl i0
+                od
+          | ListNil => Fail Failure
+   
+   [list_nth_mut_loop_loop_fwd_ind]  Theorem
+      
+      ⊢ ∀P. (∀ls i.
+               (∀x tl i0. ls = ListCons x tl ∧ u32_to_int i ≠ 0 ⇒ P tl i0) ⇒
+               P ls i) ⇒
+            ∀v v1. P v v1
+   
+   [list_t_11]  Theorem
+      
+      ⊢ ∀a0 a1 a0' a1'.
+          ListCons a0 a1 = ListCons a0' a1' ⇔ a0 = a0' ∧ a1 = a1'
+   
+   [list_t_Axiom]  Theorem
+      
+      ⊢ ∀f0 f1. ∃fn.
+          (∀a0 a1. fn (ListCons a0 a1) = f0 a0 a1 (fn a1)) ∧
+          fn ListNil = f1
+   
+   [list_t_case_cong]  Theorem
+      
+      ⊢ ∀M M' f v.
+          M = M' ∧ (∀a0 a1. M' = ListCons a0 a1 ⇒ f a0 a1 = f' a0 a1) ∧
+          (M' = ListNil ⇒ v = v') ⇒
+          list_t_CASE M f v = list_t_CASE M' f' v'
+   
+   [list_t_case_eq]  Theorem
+      
+      ⊢ list_t_CASE x f v = v' ⇔
+        (∃t l. x = ListCons t l ∧ f t l = v') ∨ x = ListNil ∧ v = v'
+   
+   [list_t_distinct]  Theorem
+      
+      ⊢ ∀a1 a0. ListCons a0 a1 ≠ ListNil
+   
+   [list_t_induction]  Theorem
+      
+      ⊢ ∀P. (∀l. P l ⇒ ∀t. P (ListCons t l)) ∧ P ListNil ⇒ ∀l. P l
+   
+   [list_t_nchotomy]  Theorem
+      
+      ⊢ ∀ll. (∃t l. ll = ListCons t l) ∨ ll = ListNil
+   
+   [lookup_raw_def]  Theorem
+      
+      ⊢ (∀key. lookup_raw key [] = NONE) ∧
+        ∀v ls key k.
+          lookup_raw key ((k,v)::ls) =
+          if k = key then SOME v else lookup_raw key ls
+   
+   [lookup_raw_ind]  Theorem
+      
+      ⊢ ∀P. (∀key. P key []) ∧
+            (∀key k v ls. (k ≠ key ⇒ P key ls) ⇒ P key ((k,v)::ls)) ⇒
+            ∀v v1. P v v1
+   
+   [nth_def]  Theorem
+      
+      ⊢ ∀ls i.
+          nth ls i =
+          case ls of
+            ListCons x tl =>
+              if u32_to_int i = 0 then Return x
+              else do i0 <- u32_sub i (int_to_u32 1); nth tl i0 od
+          | ListNil => Fail Failure
+   
+   [nth_def_loop]  Theorem
+      
+      ⊢ ∀ls i. (∀n. ¬nth_fuel_P ls i n) ⇒ nth ls i = nth_expand nth ls i
+   
+   [nth_def_terminates]  Theorem
+      
+      ⊢ ∀ls i. (∃n. nth_fuel_P ls i n) ⇒ nth ls i = nth_expand nth ls i
+   
+   [nth_fuel_P_mono]  Theorem
+      
+      ⊢ ∀n m ls i.
+          n ≤ m ⇒ nth_fuel_P ls i n ⇒ nth_fuel n ls i = nth_fuel m ls i
+   
+   [nth_fuel_def]  Theorem
+      
+      ⊢ ∀n ls i.
+          nth_fuel n ls i =
+          case n of
+            0 => Loop
+          | SUC n' =>
+            case ls of
+              ListCons x tl =>
+                if u32_to_int i = 0 then Return x
+                else
+                  do i0 <- u32_sub i (int_to_u32 1); nth_fuel n' tl i0 od
+            | ListNil => Fail Failure
+   
+   [nth_fuel_ind]  Theorem
+      
+      ⊢ ∀P. (∀n ls i.
+               (∀n' x tl i0.
+                  n = SUC n' ∧ ls = ListCons x tl ∧ u32_to_int i ≠ 0 ⇒
+                  P n' tl i0) ⇒
+               P n ls i) ⇒
+            ∀v v1 v2. P v v1 v2
+   
+   [nth_fuel_least_fail_mono]  Theorem
+      
+      ⊢ ∀n ls i. n < $LEAST (nth_fuel_P ls i) ⇒ nth_fuel n ls i = Loop
+   
+   [nth_fuel_least_success_mono]  Theorem
+      
+      ⊢ ∀n ls i.
+          $LEAST (nth_fuel_P ls i) ≤ n ⇒
+          nth_fuel n ls i = nth_fuel ($LEAST (nth_fuel_P ls i)) ls i
+   
+   [nth_fuel_mono]  Theorem
+      
+      ⊢ ∀n m ls i.
+          n ≤ m ⇒
+          if is_loop (nth_fuel n ls i) then T
+          else nth_fuel n ls i = nth_fuel m ls i
+   
+   [num2error_11]  Theorem
+      
+      ⊢ ∀r r'. r < 1 ⇒ r' < 1 ⇒ (num2error r = num2error r' ⇔ r = r')
+   
+   [num2error_ONTO]  Theorem
+      
+      ⊢ ∀a. ∃r. a = num2error r ∧ r < 1
+   
+   [num2error_error2num]  Theorem
+      
+      ⊢ ∀a. num2error (error2num a) = a
+   
+   [num2error_thm]  Theorem
+      
+      ⊢ num2error 0 = Failure
+   
+   [result_11]  Theorem
+      
+      ⊢ (∀a a'. Return a = Return a' ⇔ a = a') ∧
+        ∀a a'. Fail a = Fail a' ⇔ a = a'
+   
+   [result_Axiom]  Theorem
+      
+      ⊢ ∀f0 f1 f2. ∃fn.
+          (∀a. fn (Return a) = f0 a) ∧ (∀a. fn (Fail a) = f1 a) ∧
+          fn Loop = f2
+   
+   [result_case_cong]  Theorem
+      
+      ⊢ ∀M M' f f1 v.
+          M = M' ∧ (∀a. M' = Return a ⇒ f a = f' a) ∧
+          (∀a. M' = Fail a ⇒ f1 a = f1' a) ∧ (M' = Loop ⇒ v = v') ⇒
+          result_CASE M f f1 v = result_CASE M' f' f1' v'
+   
+   [result_case_eq]  Theorem
+      
+      ⊢ result_CASE x f f1 v = v' ⇔
+        (∃a. x = Return a ∧ f a = v') ∨ (∃e. x = Fail e ∧ f1 e = v') ∨
+        x = Loop ∧ v = v'
+   
+   [result_distinct]  Theorem
+      
+      ⊢ (∀a' a. Return a ≠ Fail a') ∧ (∀a. Return a ≠ Loop) ∧
+        ∀a. Fail a ≠ Loop
+   
+   [result_induction]  Theorem
+      
+      ⊢ ∀P. (∀a. P (Return a)) ∧ (∀e. P (Fail e)) ∧ P Loop ⇒ ∀r. P r
+   
+   [result_nchotomy]  Theorem
+      
+      ⊢ ∀rr. (∃a. rr = Return a) ∨ (∃e. rr = Fail e) ∨ rr = Loop
+   
+   [test2_11]  Theorem
+      
+      ⊢ (∀a a'. Variant1_2 a = Variant1_2 a' ⇔ a = a') ∧
+        ∀a a'. Variant2_2 a = Variant2_2 a' ⇔ a = a'
+   
+   [test2_Axiom]  Theorem
+      
+      ⊢ ∀f0 f1. ∃fn.
+          (∀a. fn (Variant1_2 a) = f0 a) ∧ ∀a. fn (Variant2_2 a) = f1 a
+   
+   [test2_case_cong]  Theorem
+      
+      ⊢ ∀M M' f f1.
+          M = M' ∧ (∀a. M' = Variant1_2 a ⇒ f a = f' a) ∧
+          (∀a. M' = Variant2_2 a ⇒ f1 a = f1' a) ⇒
+          test2_CASE M f f1 = test2_CASE M' f' f1'
+   
+   [test2_case_eq]  Theorem
+      
+      ⊢ test2_CASE x f f1 = v ⇔
+        (∃T'. x = Variant1_2 T' ∧ f T' = v) ∨
+        ∃T'. x = Variant2_2 T' ∧ f1 T' = v
+   
+   [test2_distinct]  Theorem
+      
+      ⊢ ∀a' a. Variant1_2 a ≠ Variant2_2 a'
+   
+   [test2_induction]  Theorem
+      
+      ⊢ ∀P. (∀T. P (Variant1_2 T)) ∧ (∀T. P (Variant2_2 T)) ⇒ ∀t. P t
+   
+   [test2_nchotomy]  Theorem
+      
+      ⊢ ∀tt. (∃T. tt = Variant1_2 T) ∨ ∃T. tt = Variant2_2 T
+   
+   [test_11]  Theorem
+      
+      ⊢ (∀a a'. Variant1 a = Variant1 a' ⇔ a = a') ∧
+        ∀a a'. Variant2 a = Variant2 a' ⇔ a = a'
+   
+   [test_Axiom]  Theorem
+      
+      ⊢ ∀f0 f1. ∃fn.
+          (∀a. fn (Variant1 a) = f0 a) ∧ ∀a. fn (Variant2 a) = f1 a
+   
+   [test_case_cong]  Theorem
+      
+      ⊢ ∀M M' f f1.
+          M = M' ∧ (∀a. M' = Variant1 a ⇒ f a = f' a) ∧
+          (∀a. M' = Variant2 a ⇒ f1 a = f1' a) ⇒
+          test_CASE M f f1 = test_CASE M' f' f1'
+   
+   [test_case_eq]  Theorem
+      
+      ⊢ test_CASE x f f1 = v ⇔
+        (∃b. x = Variant1 b ∧ f b = v) ∨ ∃a. x = Variant2 a ∧ f1 a = v
+   
+   [test_distinct]  Theorem
+      
+      ⊢ ∀a' a. Variant1 a ≠ Variant2 a'
+   
+   [test_induction]  Theorem
+      
+      ⊢ ∀P. (∀b. P (Variant1 b)) ∧ (∀a. P (Variant2 a)) ⇒ ∀t. P t
+   
+   [test_nchotomy]  Theorem
+      
+      ⊢ ∀tt. (∃b. tt = Variant1 b) ∨ ∃a. tt = Variant2 a
+   
+   
+*)
+end