Make progress on primitivesScript

6 files changed, 333 insertions, 211 deletions

diff --git a/backends/hol4/ilistScript.sml b/backends/hol4/ilistScript.sml
new file mode 100644
index 00000000..3e17dcc8
--- /dev/null
+++ b/backends/hol4/ilistScript.sml
@@ -0,0 +1,82 @@
+open HolKernel boolLib bossLib Parse
+open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
+
+open primitivesArithTheory primitivesBaseTacLib
+
+(* The following theory contains alternative definitions of functions operating
+   on lists like “EL” or “LENGTH”, but this time using integers rather than
+   natural numbers.
+
+   By using integers, we make sure we don't have to convert back and forth
+   between integers and natural numbers, which is extremely cumbersome in
+   the proofs.
+ *)
+
+val _ = new_theory "ilist"
+
+val len_def = Define ‘
+  len [] : int = 0 /\
+  len (x :: ls) : int = 1 + len ls
+’
+
+(* Return the ith element of a list.
+
+   Remark: we initially added the following case, so that we wouldn't need the
+   premise [i < len ls] is [index_eq_EL]:
+   “index (i : int) [] = EL (Num i) []”
+ *)
+val index_def = Define ‘
+  index (i : int) [] = EL (Num i) [] ∧
+  index (i : int) (x :: ls) = if i = 0 then x else (if 0 < i then index (i - 1) ls else ARB)
+’
+
+val update_def = Define ‘
+  update ([] : 'a list) (i : int) (y : 'a) : 'a list = [] ∧
+
+  update (x :: ls) (i : int) y =
+    if i = 0 then y :: ls else (if 0 < i then x :: update ls (i - 1) y else x :: ls)
+’
+
+Theorem len_eq_LENGTH:
+  ∀ls. len ls = &(LENGTH ls)
+Proof
+  Induct_on ‘ls’ >> fs [len_def] >> cooper_tac
+QED
+
+Theorem index_eq_EL:
+  ∀(i: int) ls.
+    0 ≤ i ⇒
+    i < len ls ⇒
+    index i ls = EL (Num i) ls
+Proof  
+  Induct_on ‘ls’ >> rpt strip_tac >> fs [len_def, index_def] >>
+  Cases_on ‘i = 0’ >> fs [] >>
+  (* TODO: automate *)
+  sg ‘0 < i’ >- cooper_tac >> fs [] >>
+  Cases_on ‘Num i’ >- (exfalso >> cooper_tac) >> fs [] >>
+  last_assum (qspec_assume ‘i - 1’) >>
+  pop_assum sg_premise_tac >- cooper_tac >>
+  sg ‘n = Num (i - 1)’ >- cooper_tac >> fs [] >>
+  last_assum irule >> cooper_tac
+QED
+
+Theorem len_append:
+  ∀l1 l2. len (l1 ++ l2) = len l1 + len l2
+Proof
+  rw [len_eq_LENGTH] >> cooper_tac
+QED
+
+Theorem append_len_eq:
+  (∀l1 l2 l1' l2'.
+       len l1 = len l1' ⇒
+       (l1 ⧺ l2 = l1' ⧺ l2' ⇔ l1 = l1' ∧ l2 = l2')) ∧
+  (∀l1 l2 l1' l2'.
+        len l2 = len l2' ⇒
+        (l1 ⧺ l2 = l1' ⧺ l2' ⇔ l1 = l1' ∧ l2 = l2'))
+Proof
+  rw [len_eq_LENGTH] >> fs [APPEND_11_LENGTH]
+QED
+
+(* TODO: prove more theorems, and add rewriting theorems *)
+
+val _ = export_theory ()
diff --git a/backends/hol4/ilistTheory.sig b/backends/hol4/ilistTheory.sig
new file mode 100644
index 00000000..9612f063
--- /dev/null
+++ b/backends/hol4/ilistTheory.sig
@@ -0,0 +1,63 @@
+signature ilistTheory =
+sig
+  type thm = Thm.thm
+  
+  (*  Definitions  *)
+    val index_def : thm
+    val len_def : thm
+    val update_def : thm
+  
+  (*  Theorems  *)
+    val append_len_eq : thm
+    val index_eq_EL : thm
+    val len_append : thm
+    val len_eq_LENGTH : thm
+  
+  val ilist_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+   [primitivesArith] Parent theory of "ilist"
+   
+   [string] Parent theory of "ilist"
+   
+   [index_def]  Definition
+      
+      ⊢ (∀i. index i [] = EL (Num i) []) ∧
+        ∀i x ls.
+          index i (x::ls) =
+          if i = 0 then x else if 0 < i then index (i − 1) ls else ARB
+   
+   [len_def]  Definition
+      
+      ⊢ len [] = 0 ∧ ∀x ls. len (x::ls) = 1 + len ls
+   
+   [update_def]  Definition
+      
+      ⊢ (∀i y. update [] i y = []) ∧
+        ∀x ls i y.
+          update (x::ls) i y =
+          if i = 0 then y::ls
+          else if 0 < i then x::update ls (i − 1) y
+          else x::ls
+   
+   [append_len_eq]  Theorem
+      
+      ⊢ (∀l1 l2 l1' l2'.
+           len l1 = len l1' ⇒ (l1 ⧺ l2 = l1' ⧺ l2' ⇔ l1 = l1' ∧ l2 = l2')) ∧
+        ∀l1 l2 l1' l2'.
+          len l2 = len l2' ⇒ (l1 ⧺ l2 = l1' ⧺ l2' ⇔ l1 = l1' ∧ l2 = l2')
+   
+   [index_eq_EL]  Theorem
+      
+      ⊢ ∀i ls. 0 ≤ i ⇒ i < len ls ⇒ index i ls = EL (Num i) ls
+   
+   [len_append]  Theorem
+      
+      ⊢ ∀l1 l2. len (l1 ⧺ l2) = len l1 + len l2
+   
+   [len_eq_LENGTH]  Theorem
+      
+      ⊢ ∀ls. len ls = &LENGTH ls
+   
+   
+*)
+end
diff --git a/backends/hol4/primitivesArithScript.sml b/backends/hol4/primitivesArithScript.sml
index 79d94698..eb2548fd 100644
--- a/backends/hol4/primitivesArithScript.sml
+++ b/backends/hol4/primitivesArithScript.sml
@@ -6,8 +6,27 @@ val _ = new_theory "primitivesArith"
 
 (* TODO: we need a better library of lemmas about arithmetic *)
 
-(* We generate and save an induction theorem for positive integers *)
-Theorem int_induction:
+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)
+(* TODO: add gsymed versions of those as rewriting theorems by default (we only want to
+   manipulate ‘<’ and ‘≤’) *)
+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)
+
+(*
+ * We generate and save an induction theorem for positive integers
+ *)
+
+(* This is the induction theorem we want.
+
+   Unfortunately, it often can't be applied by [Induct_on].
+ *)
+Theorem int_induction_ideal:
   !(P : int -> bool). P 0 /\ (!i. 0 <= i /\ P i ==> P (i+1)) ==> !i. 0 <= i ==> P i
 Proof
   ntac 4 strip_tac >>
@@ -21,20 +40,26 @@ Proof
   rw [] >> try_tac cooper_tac
 QED
 
-val _ = TypeBase.update_induction int_induction
-
-(* 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)
+(* This induction theorem works well with [Induct_on] *)
+Theorem int_induction:
+  !(P : int -> bool). (∀i. i < 0 ⇒ P i) ∧ P 0 /\ (!i. P i ==> P (i+1)) ==> !i. P i
+Proof
+  ntac 3 strip_tac >>
+  Cases_on ‘i < 0’ >- (last_assum irule >> fs []) >>
+  fs [not_lt_eq_ge] >>
+  Induct_on ‘Num i’ >> rpt strip_tac >> pop_last_assum ignore_tac
+  >-(sg ‘i = 0’ >- cooper_tac >> fs []) >>
+  last_assum (qspec_assume ‘i-1’) >>
+  fs [] >> pop_assum irule >>
+  rw [] >> try_tac cooper_tac >>
+  first_assum (qspec_assume ‘i - 1’) >>
+  pop_assum irule >>
+  rw [] >> try_tac cooper_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)
+val _ = TypeBase.update_induction int_induction
 
-Theorem int_of_num:
+Theorem int_of_num_id:
   ∀i. 0 ≤ i ⇒ &Num i = i
 Proof
   fs [INT_OF_NUM]
@@ -64,7 +89,7 @@ Proof
   imp_res_tac int_of_num >>
   (* Associativity of & *)
   pure_rewrite_tac [int_add] >>
-  fs []
+  cooper_tac
 QED
 
 Theorem num_sub_1_eq:
diff --git a/backends/hol4/primitivesArithTheory.sig b/backends/hol4/primitivesArithTheory.sig
index 73a6cf20..b2172b7c 100644
--- a/backends/hol4/primitivesArithTheory.sig
+++ b/backends/hol4/primitivesArithTheory.sig
@@ -7,7 +7,8 @@ sig
     val gt_eq_lt : thm
     val int_add : thm
     val int_induction : thm
-    val int_of_num : thm
+    val int_induction_ideal : thm
+    val int_of_num_id : thm
     val int_of_num_inj : thm
     val le_eq_ge : thm
     val lt_eq_gt : thm
@@ -44,9 +45,13 @@ sig
    
    [int_induction]  Theorem
       
+      ⊢ ∀P. (∀i. i < 0 ⇒ P i) ∧ P 0 ∧ (∀i. P i ⇒ P (i + 1)) ⇒ ∀i. P i
+   
+   [int_induction_ideal]  Theorem
+      
       ⊢ ∀P. P 0 ∧ (∀i. 0 ≤ i ∧ P i ⇒ P (i + 1)) ⇒ ∀i. 0 ≤ i ⇒ P i
    
-   [int_of_num]  Theorem
+   [int_of_num_id]  Theorem
       
       ⊢ ∀i. 0 ≤ i ⇒ &Num i = i
    
diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml
index b1dd770b..b7bc978f 100644
--- a/backends/hol4/primitivesScript.sml
+++ b/backends/hol4/primitivesScript.sml
@@ -1,7 +1,7 @@
 open HolKernel boolLib bossLib Parse
 open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
 
-open primitivesArithTheory primitivesBaseTacLib
+open primitivesArithTheory primitivesBaseTacLib ilistTheory
 
 val primitives_theory_name = "primitives"
 val _ = new_theory primitives_theory_name
@@ -1169,12 +1169,11 @@ val _ = new_constant ("vec_to_list", “:'a vec -> 'a list”)
 (* TODO: we could also make ‘mk_vec’ return ‘'a vec’ (no result) *)
 val _ = new_constant ("mk_vec", “:'a list -> 'a vec result”)
 
-
 val vec_to_list_num_bounds =
   new_axiom ("vec_to_list_num_bounds",
-    “!v. let l = LENGTH (vec_to_list v) in
-     (0:num) <= l /\ l <= Num usize_max”)
+    “!v. (0:num) <= LENGTH (vec_to_list v) /\ LENGTH (vec_to_list v) <= Num usize_max”)
 
+(*
 Theorem vec_to_list_int_bounds:
   !v. 0 <= int_of_num (LENGTH (vec_to_list v)) /\ int_of_num (LENGTH (vec_to_list v)) <= usize_max
 Proof
@@ -1252,13 +1251,16 @@ Proof
   Induct_on ‘ls’ >> Cases_on ‘i’ >> rw [update_def] >>
   Cases_on ‘j’ >> fs []
 QED
+*)
 
+(*
 (* TODO: this is the base definition for index. Shall we remove the ‘return’ type? *)
 val vec_index_def = Define ‘
   vec_index i v =
     if usize_to_int i ≤ usize_to_int (vec_len v)
     then Return (EL (Num (usize_to_int i)) (vec_to_list v))
     else Fail Failure’
+*)
 
 (* TODO: shortcut for qspec_then ... ASSUME_TAC *)
 (* TODO: use cooper_tac everywhere *)
@@ -1300,6 +1302,7 @@ QED
   &n < &m
 *)
 
+(*
 val vec_insert_back_def = Define ‘
   vec_insert_back (v : 'a vec) (i : usize) (x : 'a) = mk_vec (update (vec_to_list v) (Num (usize_to_int i)) x)’
 
@@ -1326,7 +1329,7 @@ Proof
   sg ‘Num (usize_to_int i) < LENGTH (vec_to_list v)’ >-(
     (* TODO: automate *)
     pure_once_rewrite_tac [gsym INT_LT] >>
-    dep_pure_once_rewrite_tac [primitivesArithTheory.int_of_num] >>
+    dep_pure_once_rewrite_tac [int_of_num_id] >>
     qspec_assume ‘i’ usize_to_int_bounds >> fs []
   ) >>
   fs [] >>
@@ -1336,33 +1339,16 @@ Proof
   rw [] >-(
     (* TODO: automate *)
     irule int_of_num_neq_inj >>
-    dep_pure_rewrite_tac [primitivesArithTheory.int_of_num] >>
+    dep_pure_rewrite_tac [int_of_num_id] >>
     rw [usize_to_int_bounds] >>
     metis_tac [int_to_usize_usize_to_int]
   ) >>
   (* TODO: automate *)
   pure_once_rewrite_tac [gsym INT_LT] >>
-  dep_pure_once_rewrite_tac [primitivesArithTheory.int_of_num] >>
+  dep_pure_once_rewrite_tac [int_of_num_id] >>
   qspec_assume ‘j’ usize_to_int_bounds >> fs []
 QED
-
-
-(* Small experiment: trying to redefine common functions with integers instead of nums *)
-val index_def = Define ‘
-  index (i : int) (x :: ls) = if i = 0 then x else (if 0 < i then index (i - 1) ls else ARB)
-’
-
-val len_def = Define ‘
-  len [] : int = 0 /\
-  len (x :: ls) : int = 1 + len ls
-’
-
-val update_def = Define ‘
-  update ([] : 'a list) (i : int) (y : 'a) : 'a list = [] ∧
-
-  update (x :: ls) (i : int) y =
-    if i = 0 then y :: ls else (if 0 < i then x :: update ls (i - 1) y else x :: ls)
-’
+*)
 
 Theorem update_len:
   ∀ls i y. len (update ls i y) = len ls
@@ -1417,8 +1403,11 @@ QED
 Theorem vec_to_list_int_bounds:
   !v. 0 <= len (vec_to_list v) /\ len (vec_to_list v) <= usize_max
 Proof
-  (* TODO *)
-  cheat
+  gen_tac >>
+  qspec_assume ‘v’ vec_to_list_num_bounds >>
+  fs [len_eq_LENGTH] >>
+  assume_tac usize_bounds >> fs [u16_max_def] >>
+  cooper_tac
 QED
 
 val vec_len_def = Define ‘vec_len v = int_to_usize (len (vec_to_list v))’
@@ -1438,7 +1427,6 @@ val vec_index_def = Define ‘
     then Return (index (usize_to_int i) (vec_to_list v))
     else Fail Failure’
 
-(* TODO: *)
 val mk_vec_spec = new_axiom ("mk_vec_spec",
   “∀l. len l ≤ usize_max ⇒ ∃v. mk_vec l = Return v ∧ vec_to_list v = l”)
 
diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index 92f02af8..23846737 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -85,14 +85,12 @@ sig
     val i8_mul_def : thm
     val i8_rem_def : thm
     val i8_sub_def : thm
-    val index_def : thm
     val int_rem_def : thm
     val isize_add_def : thm
     val isize_div_def : thm
     val isize_mul_def : thm
     val isize_rem_def : thm
     val isize_sub_def : thm
-    val len_def : thm
     val massert_def : thm
     val mem_replace_back_def : thm
     val mem_replace_fwd_def : thm
@@ -142,7 +140,6 @@ sig
     val u8_mul_def : thm
     val u8_rem_def : thm
     val u8_sub_def : thm
-    val update_def : thm
     val usize_add_def : thm
     val usize_div_def : thm
     val usize_mul_def : thm
@@ -151,8 +148,6 @@ sig
     val vec_index_def : thm
     val vec_insert_back_def : thm
     val vec_len_def : thm
-    val vec_new_def : thm
-    val vec_push_back_def : thm
   
   (*  Theorems  *)
     val datatype_error : thm
@@ -237,7 +232,6 @@ sig
     val u8_mul_eq : thm
     val u8_rem_eq : thm
     val u8_sub_eq : thm
-    val update_ind : thm
     val update_len : thm
     val update_spec : thm
     val usize_add_eq : thm
@@ -251,209 +245,208 @@ sig
   
   val primitives_grammars : type_grammar.grammar * term_grammar.grammar
 (*
-   [primitivesArith] Parent theory of "primitives"
+   [ilist] Parent theory of "primitives"
    
-   [string] Parent theory of "primitives"
+   [isize_bounds]  Axiom
+      
+      [oracles: ] [axioms: isize_bounds] []
+      ⊢ isize_min ≤ i16_min ∧ isize_max ≥ i16_max
    
-   [mk_vec_spec]  Axiom
+   [usize_bounds]  Axiom
       
-      [oracles: ] [axioms: mk_vec_spec] []
-      ⊢ ∀l. len l ≤ usize_max ⇒ ∃v. mk_vec l = Return v ∧ vec_to_list v = l
+      [oracles: ] [axioms: usize_bounds] [] ⊢ usize_max ≥ u16_max
    
-   [vec_to_list_num_bounds]  Axiom
+   [isize_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: vec_to_list_num_bounds] []
-      ⊢ ∀v. (let l = LENGTH (vec_to_list v) in 0 ≤ l ∧ l ≤ Num usize_max)
+      [oracles: ] [axioms: isize_to_int_bounds] []
+      ⊢ ∀n. isize_min ≤ isize_to_int n ∧ isize_to_int n ≤ isize_max
    
-   [int_to_usize_usize_to_int]  Axiom
+   [i8_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_usize_usize_to_int] []
-      ⊢ ∀i. int_to_usize (usize_to_int i) = i
+      [oracles: ] [axioms: i8_to_int_bounds] []
+      ⊢ ∀n. i8_min ≤ i8_to_int n ∧ i8_to_int n ≤ i8_max
    
-   [int_to_u128_u128_to_int]  Axiom
+   [i16_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_u128_u128_to_int] []
-      ⊢ ∀i. int_to_u128 (u128_to_int i) = i
+      [oracles: ] [axioms: i16_to_int_bounds] []
+      ⊢ ∀n. i16_min ≤ i16_to_int n ∧ i16_to_int n ≤ i16_max
    
-   [int_to_u64_u64_to_int]  Axiom
+   [i32_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_u64_u64_to_int] []
-      ⊢ ∀i. int_to_u64 (u64_to_int i) = i
+      [oracles: ] [axioms: i32_to_int_bounds] []
+      ⊢ ∀n. i32_min ≤ i32_to_int n ∧ i32_to_int n ≤ i32_max
    
-   [int_to_u32_u32_to_int]  Axiom
+   [i64_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_u32_u32_to_int] []
-      ⊢ ∀i. int_to_u32 (u32_to_int i) = i
+      [oracles: ] [axioms: i64_to_int_bounds] []
+      ⊢ ∀n. i64_min ≤ i64_to_int n ∧ i64_to_int n ≤ i64_max
    
-   [int_to_u16_u16_to_int]  Axiom
+   [i128_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_u16_u16_to_int] []
-      ⊢ ∀i. int_to_u16 (u16_to_int i) = i
+      [oracles: ] [axioms: i128_to_int_bounds] []
+      ⊢ ∀n. i128_min ≤ i128_to_int n ∧ i128_to_int n ≤ i128_max
    
-   [int_to_u8_u8_to_int]  Axiom
+   [usize_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_u8_u8_to_int] []
-      ⊢ ∀i. int_to_u8 (u8_to_int i) = i
+      [oracles: ] [axioms: usize_to_int_bounds] []
+      ⊢ ∀n. 0 ≤ usize_to_int n ∧ usize_to_int n ≤ usize_max
    
-   [int_to_isize_isize_to_int]  Axiom
+   [u8_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_isize_isize_to_int] []
-      ⊢ ∀i. int_to_isize (isize_to_int i) = i
+      [oracles: ] [axioms: u8_to_int_bounds] []
+      ⊢ ∀n. 0 ≤ u8_to_int n ∧ u8_to_int n ≤ u8_max
    
-   [int_to_i128_i128_to_int]  Axiom
+   [u16_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_i128_i128_to_int] []
-      ⊢ ∀i. int_to_i128 (i128_to_int i) = i
+      [oracles: ] [axioms: u16_to_int_bounds] []
+      ⊢ ∀n. 0 ≤ u16_to_int n ∧ u16_to_int n ≤ u16_max
    
-   [int_to_i64_i64_to_int]  Axiom
+   [u32_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_i64_i64_to_int] []
-      ⊢ ∀i. int_to_i64 (i64_to_int i) = i
+      [oracles: ] [axioms: u32_to_int_bounds] []
+      ⊢ ∀n. 0 ≤ u32_to_int n ∧ u32_to_int n ≤ u32_max
    
-   [int_to_i32_i32_to_int]  Axiom
+   [u64_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_i32_i32_to_int] []
-      ⊢ ∀i. int_to_i32 (i32_to_int i) = i
+      [oracles: ] [axioms: u64_to_int_bounds] []
+      ⊢ ∀n. 0 ≤ u64_to_int n ∧ u64_to_int n ≤ u64_max
    
-   [int_to_i16_i16_to_int]  Axiom
+   [u128_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_i16_i16_to_int] []
-      ⊢ ∀i. int_to_i16 (i16_to_int i) = i
+      [oracles: ] [axioms: u128_to_int_bounds] []
+      ⊢ ∀n. 0 ≤ u128_to_int n ∧ u128_to_int n ≤ u128_max
    
-   [int_to_i8_i8_to_int]  Axiom
+   [isize_to_int_int_to_isize]  Axiom
       
-      [oracles: ] [axioms: int_to_i8_i8_to_int] []
-      ⊢ ∀i. int_to_i8 (i8_to_int i) = i
+      [oracles: ] [axioms: isize_to_int_int_to_isize] []
+      ⊢ ∀n. isize_min ≤ n ∧ n ≤ isize_max ⇒
+            isize_to_int (int_to_isize n) = n
    
-   [u128_to_int_int_to_u128]  Axiom
+   [i8_to_int_int_to_i8]  Axiom
       
-      [oracles: ] [axioms: u128_to_int_int_to_u128] []
-      ⊢ ∀n. 0 ≤ n ∧ n ≤ u128_max ⇒ u128_to_int (int_to_u128 n) = n
+      [oracles: ] [axioms: i8_to_int_int_to_i8] []
+      ⊢ ∀n. i8_min ≤ n ∧ n ≤ i8_max ⇒ i8_to_int (int_to_i8 n) = n
    
-   [u64_to_int_int_to_u64]  Axiom
+   [i16_to_int_int_to_i16]  Axiom
       
-      [oracles: ] [axioms: u64_to_int_int_to_u64] []
-      ⊢ ∀n. 0 ≤ n ∧ n ≤ u64_max ⇒ u64_to_int (int_to_u64 n) = n
+      [oracles: ] [axioms: i16_to_int_int_to_i16] []
+      ⊢ ∀n. i16_min ≤ n ∧ n ≤ i16_max ⇒ i16_to_int (int_to_i16 n) = n
    
-   [u32_to_int_int_to_u32]  Axiom
+   [i32_to_int_int_to_i32]  Axiom
       
-      [oracles: ] [axioms: u32_to_int_int_to_u32] []
-      ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ u32_to_int (int_to_u32 n) = n
+      [oracles: ] [axioms: i32_to_int_int_to_i32] []
+      ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ i32_to_int (int_to_i32 n) = n
    
-   [u16_to_int_int_to_u16]  Axiom
+   [i64_to_int_int_to_i64]  Axiom
       
-      [oracles: ] [axioms: u16_to_int_int_to_u16] []
-      ⊢ ∀n. 0 ≤ n ∧ n ≤ u16_max ⇒ u16_to_int (int_to_u16 n) = n
+      [oracles: ] [axioms: i64_to_int_int_to_i64] []
+      ⊢ ∀n. i64_min ≤ n ∧ n ≤ i64_max ⇒ i64_to_int (int_to_i64 n) = n
    
-   [u8_to_int_int_to_u8]  Axiom
+   [i128_to_int_int_to_i128]  Axiom
       
-      [oracles: ] [axioms: u8_to_int_int_to_u8] []
-      ⊢ ∀n. 0 ≤ n ∧ n ≤ u8_max ⇒ u8_to_int (int_to_u8 n) = n
+      [oracles: ] [axioms: i128_to_int_int_to_i128] []
+      ⊢ ∀n. i128_min ≤ n ∧ n ≤ i128_max ⇒ i128_to_int (int_to_i128 n) = n
    
    [usize_to_int_int_to_usize]  Axiom
       
       [oracles: ] [axioms: usize_to_int_int_to_usize] []
       ⊢ ∀n. 0 ≤ n ∧ n ≤ usize_max ⇒ usize_to_int (int_to_usize n) = n
    
-   [i128_to_int_int_to_i128]  Axiom
-      
-      [oracles: ] [axioms: i128_to_int_int_to_i128] []
-      ⊢ ∀n. i128_min ≤ n ∧ n ≤ i128_max ⇒ i128_to_int (int_to_i128 n) = n
-   
-   [i64_to_int_int_to_i64]  Axiom
+   [u8_to_int_int_to_u8]  Axiom
       
-      [oracles: ] [axioms: i64_to_int_int_to_i64] []
-      ⊢ ∀n. i64_min ≤ n ∧ n ≤ i64_max ⇒ i64_to_int (int_to_i64 n) = n
+      [oracles: ] [axioms: u8_to_int_int_to_u8] []
+      ⊢ ∀n. 0 ≤ n ∧ n ≤ u8_max ⇒ u8_to_int (int_to_u8 n) = n
    
-   [i32_to_int_int_to_i32]  Axiom
+   [u16_to_int_int_to_u16]  Axiom
       
-      [oracles: ] [axioms: i32_to_int_int_to_i32] []
-      ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ i32_to_int (int_to_i32 n) = n
+      [oracles: ] [axioms: u16_to_int_int_to_u16] []
+      ⊢ ∀n. 0 ≤ n ∧ n ≤ u16_max ⇒ u16_to_int (int_to_u16 n) = n
    
-   [i16_to_int_int_to_i16]  Axiom
+   [u32_to_int_int_to_u32]  Axiom
       
-      [oracles: ] [axioms: i16_to_int_int_to_i16] []
-      ⊢ ∀n. i16_min ≤ n ∧ n ≤ i16_max ⇒ i16_to_int (int_to_i16 n) = n
+      [oracles: ] [axioms: u32_to_int_int_to_u32] []
+      ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ u32_to_int (int_to_u32 n) = n
    
-   [i8_to_int_int_to_i8]  Axiom
+   [u64_to_int_int_to_u64]  Axiom
       
-      [oracles: ] [axioms: i8_to_int_int_to_i8] []
-      ⊢ ∀n. i8_min ≤ n ∧ n ≤ i8_max ⇒ i8_to_int (int_to_i8 n) = n
+      [oracles: ] [axioms: u64_to_int_int_to_u64] []
+      ⊢ ∀n. 0 ≤ n ∧ n ≤ u64_max ⇒ u64_to_int (int_to_u64 n) = n
    
-   [isize_to_int_int_to_isize]  Axiom
+   [u128_to_int_int_to_u128]  Axiom
       
-      [oracles: ] [axioms: isize_to_int_int_to_isize] []
-      ⊢ ∀n. isize_min ≤ n ∧ n ≤ isize_max ⇒
-            isize_to_int (int_to_isize n) = n
+      [oracles: ] [axioms: u128_to_int_int_to_u128] []
+      ⊢ ∀n. 0 ≤ n ∧ n ≤ u128_max ⇒ u128_to_int (int_to_u128 n) = n
    
-   [u128_to_int_bounds]  Axiom
+   [int_to_i8_i8_to_int]  Axiom
       
-      [oracles: ] [axioms: u128_to_int_bounds] []
-      ⊢ ∀n. 0 ≤ u128_to_int n ∧ u128_to_int n ≤ u128_max
+      [oracles: ] [axioms: int_to_i8_i8_to_int] []
+      ⊢ ∀i. int_to_i8 (i8_to_int i) = i
    
-   [u64_to_int_bounds]  Axiom
+   [int_to_i16_i16_to_int]  Axiom
       
-      [oracles: ] [axioms: u64_to_int_bounds] []
-      ⊢ ∀n. 0 ≤ u64_to_int n ∧ u64_to_int n ≤ u64_max
+      [oracles: ] [axioms: int_to_i16_i16_to_int] []
+      ⊢ ∀i. int_to_i16 (i16_to_int i) = i
    
-   [u32_to_int_bounds]  Axiom
+   [int_to_i32_i32_to_int]  Axiom
       
-      [oracles: ] [axioms: u32_to_int_bounds] []
-      ⊢ ∀n. 0 ≤ u32_to_int n ∧ u32_to_int n ≤ u32_max
+      [oracles: ] [axioms: int_to_i32_i32_to_int] []
+      ⊢ ∀i. int_to_i32 (i32_to_int i) = i
    
-   [u16_to_int_bounds]  Axiom
+   [int_to_i64_i64_to_int]  Axiom
       
-      [oracles: ] [axioms: u16_to_int_bounds] []
-      ⊢ ∀n. 0 ≤ u16_to_int n ∧ u16_to_int n ≤ u16_max
+      [oracles: ] [axioms: int_to_i64_i64_to_int] []
+      ⊢ ∀i. int_to_i64 (i64_to_int i) = i
    
-   [u8_to_int_bounds]  Axiom
+   [int_to_i128_i128_to_int]  Axiom
       
-      [oracles: ] [axioms: u8_to_int_bounds] []
-      ⊢ ∀n. 0 ≤ u8_to_int n ∧ u8_to_int n ≤ u8_max
+      [oracles: ] [axioms: int_to_i128_i128_to_int] []
+      ⊢ ∀i. int_to_i128 (i128_to_int i) = i
    
-   [usize_to_int_bounds]  Axiom
+   [int_to_isize_isize_to_int]  Axiom
       
-      [oracles: ] [axioms: usize_to_int_bounds] []
-      ⊢ ∀n. 0 ≤ usize_to_int n ∧ usize_to_int n ≤ usize_max
+      [oracles: ] [axioms: int_to_isize_isize_to_int] []
+      ⊢ ∀i. int_to_isize (isize_to_int i) = i
    
-   [i128_to_int_bounds]  Axiom
+   [int_to_u8_u8_to_int]  Axiom
       
-      [oracles: ] [axioms: i128_to_int_bounds] []
-      ⊢ ∀n. i128_min ≤ i128_to_int n ∧ i128_to_int n ≤ i128_max
+      [oracles: ] [axioms: int_to_u8_u8_to_int] []
+      ⊢ ∀i. int_to_u8 (u8_to_int i) = i
    
-   [i64_to_int_bounds]  Axiom
+   [int_to_u16_u16_to_int]  Axiom
       
-      [oracles: ] [axioms: i64_to_int_bounds] []
-      ⊢ ∀n. i64_min ≤ i64_to_int n ∧ i64_to_int n ≤ i64_max
+      [oracles: ] [axioms: int_to_u16_u16_to_int] []
+      ⊢ ∀i. int_to_u16 (u16_to_int i) = i
    
-   [i32_to_int_bounds]  Axiom
+   [int_to_u32_u32_to_int]  Axiom
       
-      [oracles: ] [axioms: i32_to_int_bounds] []
-      ⊢ ∀n. i32_min ≤ i32_to_int n ∧ i32_to_int n ≤ i32_max
+      [oracles: ] [axioms: int_to_u32_u32_to_int] []
+      ⊢ ∀i. int_to_u32 (u32_to_int i) = i
    
-   [i16_to_int_bounds]  Axiom
+   [int_to_u64_u64_to_int]  Axiom
       
-      [oracles: ] [axioms: i16_to_int_bounds] []
-      ⊢ ∀n. i16_min ≤ i16_to_int n ∧ i16_to_int n ≤ i16_max
+      [oracles: ] [axioms: int_to_u64_u64_to_int] []
+      ⊢ ∀i. int_to_u64 (u64_to_int i) = i
    
-   [i8_to_int_bounds]  Axiom
+   [int_to_u128_u128_to_int]  Axiom
       
-      [oracles: ] [axioms: i8_to_int_bounds] []
-      ⊢ ∀n. i8_min ≤ i8_to_int n ∧ i8_to_int n ≤ i8_max
+      [oracles: ] [axioms: int_to_u128_u128_to_int] []
+      ⊢ ∀i. int_to_u128 (u128_to_int i) = i
    
-   [isize_to_int_bounds]  Axiom
+   [int_to_usize_usize_to_int]  Axiom
       
-      [oracles: ] [axioms: isize_to_int_bounds] []
-      ⊢ ∀n. isize_min ≤ isize_to_int n ∧ isize_to_int n ≤ isize_max
+      [oracles: ] [axioms: int_to_usize_usize_to_int] []
+      ⊢ ∀i. int_to_usize (usize_to_int i) = i
    
-   [usize_bounds]  Axiom
+   [vec_to_list_num_bounds]  Axiom
       
-      [oracles: ] [axioms: usize_bounds] [] ⊢ usize_max ≥ u16_max
+      [oracles: ] [axioms: vec_to_list_num_bounds] []
+      ⊢ ∀v. 0 ≤ LENGTH (vec_to_list v) ∧
+            LENGTH (vec_to_list v) ≤ Num usize_max
    
-   [isize_bounds]  Axiom
+   [mk_vec_spec]  Axiom
       
-      [oracles: ] [axioms: isize_bounds] []
-      ⊢ isize_min ≤ i16_min ∧ isize_max ≥ i16_max
+      [oracles: ] [axioms: mk_vec_spec] []
+      ⊢ ∀l. len l ≤ usize_max ⇒ ∃v. mk_vec l = Return v ∧ vec_to_list v = l
    
    [bind_def]  Definition
       
@@ -648,12 +641,6 @@ sig
       
       ⊢ ∀x y. i8_sub x y = mk_i8 (i8_to_int x − i8_to_int y)
    
-   [index_def]  Definition
-      
-      ⊢ ∀i x ls.
-          index i (x::ls) =
-          if i = 0 then x else if 0 < i then index (i − 1) ls else ARB
-   
    [int_rem_def]  Definition
       
       ⊢ ∀x y.
@@ -686,10 +673,6 @@ sig
       
       ⊢ ∀x y. isize_sub x y = mk_isize (isize_to_int x − isize_to_int y)
    
-   [len_def]  Definition
-      
-      ⊢ len [] = 0 ∧ ∀x ls. len (x::ls) = 1 + len ls
-   
    [massert_def]  Definition
       
       ⊢ ∀b. massert b = if b then Return () else Fail Failure
@@ -961,15 +944,6 @@ sig
       
       ⊢ ∀x y. u8_sub x y = mk_u8 (u8_to_int x − u8_to_int y)
    
-   [update_def]  Definition
-      
-      ⊢ (∀i y. update [] i y = []) ∧
-        ∀x ls i y.
-          update (x::ls) i y =
-          if i = 0 then y::ls
-          else if 0 < i then x::update ls (i − 1) y
-          else x::ls
-   
    [usize_add_def]  Definition
       
       ⊢ ∀x y. usize_add x y = mk_usize (usize_to_int x + usize_to_int y)
@@ -1014,15 +988,6 @@ sig
       
       ⊢ ∀v. vec_len v = int_to_usize (len (vec_to_list v))
    
-   [vec_new_def]  Definition
-      
-      ⊢ vec_new =
-        case mk_vec [] of Return v => v | Fail v2 => ARB | Loop => ARB
-   
-   [vec_push_back_def]  Definition
-      
-      ⊢ ∀v x. vec_push_back v x = mk_vec (vec_to_list v ⧺ [x])
-   
    [datatype_error]  Theorem
       
       ⊢ DATATYPE (error Failure)
@@ -1729,12 +1694,6 @@ sig
           ∃z. u8_sub x y = Return z ∧
               u8_to_int z = u8_to_int x − u8_to_int y
    
-   [update_ind]  Theorem
-      
-      ⊢ ∀P. (∀i y. P [] i y) ∧ (∀v0 ls y. P (v0::ls) 0 y) ∧
-            (∀x ls i y. P ls i y ⇒ P (x::ls) (SUC i) y) ⇒
-            ∀v v1 v2. P v v1 v2
-   
    [update_len]  Theorem
       
       ⊢ ∀ls i y. len (update ls i y) = len ls
@@ -1801,9 +1760,9 @@ sig
    
    [vec_insert_back_spec]  Theorem
       
-      [oracles: DISK_THM, cheat]
-      [axioms: usize_to_int_bounds, usize_to_int_int_to_usize, mk_vec_spec]
-      []
+      [oracles: DISK_THM]
+      [axioms: vec_to_list_num_bounds, usize_bounds,
+       usize_to_int_int_to_usize, usize_to_int_bounds, mk_vec_spec] []
       ⊢ ∀v i x.
           usize_to_int i < usize_to_int (vec_len v) ⇒
           ∃nv.
@@ -1815,13 +1774,13 @@ sig
    
    [vec_len_spec]  Theorem
       
-      [oracles: DISK_THM, cheat] [axioms: ] []
+      [oracles: DISK_THM] [axioms: usize_bounds, vec_to_list_num_bounds] []
       ⊢ ∀v. vec_len v = int_to_usize (len (vec_to_list v)) ∧
             0 ≤ len (vec_to_list v) ∧ len (vec_to_list v) ≤ usize_max
    
    [vec_to_list_int_bounds]  Theorem
       
-      [oracles: cheat] [axioms: ] []
+      [oracles: DISK_THM] [axioms: usize_bounds, vec_to_list_num_bounds] []
       ⊢ ∀v. 0 ≤ len (vec_to_list v) ∧ len (vec_to_list v) ≤ usize_max