Make progress on primitivesScript.sml and experiment a bit

4 files changed, 890 insertions, 87 deletions

diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml
index b5d9918e..0368ee9a 100644
--- a/backends/hol4/primitivesBaseTacLib.sml
+++ b/backends/hol4/primitivesBaseTacLib.sml
@@ -13,6 +13,8 @@ fun ignore_tac (_ : thm) : tactic = ALL_TAC
 
 val pop_ignore_tac = pop_assum ignore_tac
 
+val try_tac = TRY
+
 (* TODO: no exfalso tactic?? *)
 val ex_falso : tactic =
   SUBGOAL_THEN “F” (fn th => ASSUME_TAC th >> fs[])
@@ -22,13 +24,406 @@ fun qspecl_assume xl th = qspecl_then xl assume_tac th
 fun first_qspec_assume x = first_assum (qspec_assume x)
 fun first_qspecl_assume xl = first_assum (qspecl_assume xl)
 
-
-
+val all_tac = all_tac
 val cooper_tac = COOPER_TAC
+val pure_rewrite_tac = PURE_REWRITE_TAC
 val pure_once_rewrite_tac = PURE_ONCE_REWRITE_TAC
 
 (* Dependent rewrites *)
 val dep_pure_once_rewrite_tac = dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC
 val dep_pure_rewrite_tac = dep_rewrite.DEP_PURE_REWRITE_TAC
 
+
+(* Add a list of theorems in the assumptions *)
+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
+
+(* 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
+
+(* Add the first premise of the theorem as subgoal, and add the theorem without its
+   first premise as an assumption.
+
+   For instance, if we have the goal:
+     asls
+     ====
+      c
+   and the theorem: ⊢ H ==> G
+
+   We generate:
+   asls     asls
+   ====     G
+     H      ====
+            C
+
+*)
+val sg_premise_tac = sg_premise_then all_tac assume_tac
+
+(* 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.
+
+   [ignore]: if the conclusion of a theorem matches a term in this set, ignore it.
+ *)
+fun inst_match_concl_in_terms (ignore : term Redblackset.set) (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;
+        val c = concl inst_th;
+      in
+        (* Check that we mustn't ignore the theorem *)
+        if Redblackset.member (ignore, c) then failwith "inst_match_concl_in_terms: already in the assumptions"
+        else (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 in the given list of terms.
+
+   Leaves the premises as subgoals if [prove_premise] doesn't prove them.
+ *)
+fun apply_dep_rewrites_match_concl_with_terms_tac
+  (prove_premise : tactic) (then_tac : thm_tactic) (tl : term list) (th : thm) : tactic =
+  let
+    val ignore = Redblackset.fromList Term.compare tl;
+    (* Discharge the assumptions so that the goal is one single term *)
+    val thms = inst_match_concl_in_terms ignore th tl;
+    val thms = map thm_to_conj_implies thms;
+  in
+    (* Apply each theorem *)
+    MAP_EVERY (sg_premise_then prove_premise then_tac) thms
+  end
+
+(* Attempt to apply dependent rewrites with a theorem by matching its
+   conclusion with subterms of the goal (including the assumptions).
+
+   Leaves the premises as subgoals if [prove_premise] doesn't prove them.
+ *)
+fun apply_dep_rewrites_match_concl_with_all_tac
+  (prove_premise : tactic) (then_tac : thm_tactic) (th : thm) : tactic =
+  fn (asms, g) => apply_dep_rewrites_match_concl_with_terms_tac prove_premise then_tac (g :: asms) th (asms, g)
+
+(* Same as {!apply_dep_rewrites_match_concl_with_all_tac} but we only match the
+   conclusion of the goal.
+ *)
+fun apply_dep_rewrites_match_concl_with_goal_tac
+  (prove_premise : tactic) (then_tac : thm_tactic) (th : thm) : tactic =
+  fn (asms, g) => apply_dep_rewrites_match_concl_with_terms_tac prove_premise then_tac [g] th (asms, g)
+
+(* A theorem might be of the shape: [H => A = B /\ C = D], in which
+   case we can split it into:
+   [H => A = B]
+   [H => C = D]
+
+   The theorem mustn't have assumptions.
+ *)
+fun split_rewrite_thm (th : thm) : thm list =
+  let
+    val _ = null (hyp th);
+    val t = concl th;
+    val (vars, t) = strip_forall t;
+    val (impl, t) = strip_imp t;
+    val tl = strip_conj t;
+    fun mk_goal (t : term) = list_mk_forall (vars, (list_mk_imp (impl, t)))
+    val prove_tac =
+      rpt gen_tac >> rpt disch_tac >>
+      qspecl_assume (map (fn a => ‘^a’) vars) th >>
+      fs [];
+    fun mk_th (t : term) = prove (mk_goal t, prove_tac);
+    (* Change the shape of the theorem (one of the conjuncts may have
+       universally quantified variables)
+     *)
+    fun transform_th (th : thm) : thm =
+      (GEN_ALL o thm_to_conj_implies o SPEC_ALL o UNDISCH_ALL o SPEC_ALL) th
+  in
+    map (transform_th o mk_th) tl
+  end
+
+(* A dependent rewrite tactic which introduces the premises in a new goal.
+
+   We try to apply dependent rewrites to the whole goal, including its assumptions.
+
+   TODO: this tactic sometimes introduces several times the same subgoal
+   (because we split theorems...).
+ *)
+fun sg_dep_rewrite_all_tac (th : thm) =
+  let
+    (* Split the theorem *)
+    val thml = split_rewrite_thm th
+  in
+    MAP_EVERY (apply_dep_rewrites_match_concl_with_all_tac all_tac assume_tac) thml
+  end
+
+(* Same as {!sg_dep_rewrite_tac} but this time we apply rewrites only in the conclusion
+   of the goal (not the assumptions).
+ *)
+fun sg_dep_rewrite_goal_tac (th : thm) =
+  let
+    (* Split the theorem *)
+    val thml = split_rewrite_thm th
+  in
+    MAP_EVERY (apply_dep_rewrites_match_concl_with_goal_tac all_tac assume_tac) thml
+  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.
+
+   Leaves the premises as subgoals if [prove_premise] doesn't prove them.
+ *)
+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
+          sg_premise_then prove_premise then_tac th
+        end;
+    in
+      (* Apply each theorem *)
+      MAP_EVERY apply_tac thms (asms, g)
+    end
+
 end
diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml
index 85efeb61..2df3375a 100644
--- a/backends/hol4/primitivesScript.sml
+++ b/backends/hol4/primitivesScript.sml
@@ -1389,8 +1389,23 @@ QED
 
 (* TODO: automate: take assumption, intro first premise as subgoal *)
 
+(* TODO: I think we should express as much as we could in terms of integers (not machine integers).
+
+   For instance:
+   - theorem below: ‘j <> i’ ~~> ‘usize_to_int j <> usize_to_int i’
+   - we should prove theorems like: ‘usize_eq i j <=> usize_to_int i = usize_to_int j’
+     (that we would automatically apply)
+*)
+
+(*
+  &(SUC n) = 1 + &n
+  n < m
+  &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)’
+
 Theorem VEC_INSERT_BACK_SPEC:
   ∀v i x.
     usize_to_int i < usize_to_int (vec_len v) ⇒
@@ -1433,4 +1448,166 @@ Proof
   qspec_assume ‘j’ usize_to_int_bounds >> fs []
 QED
 
+(* TODO: use lowercase everywhere for the theorem names *)
+
+(* We generate and save an induction theorem for positive integers *)
+Theorem int_induction:
+  !(P : int -> bool). P 0 /\ (!i. 0 <= i /\ P i ==> P (i+1)) ==> !i. 0 <= i ==> P i
+Proof
+  ntac 4 strip_tac >>
+  Induct_on ‘Num i’ >> rpt strip_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 _ = TypeBase.update_induction int_induction
+
+(* 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
+Proof
+  Induct_on ‘ls’ >> Cases_on ‘i’ >> rw [update_def, len_def]
+QED
+
+Theorem update_spec:
+  ∀ls i y.
+    0 <= i ==>
+    i < len ls ==>
+    len (update ls i y) = len ls ∧
+    index i (update ls i y) = y ∧
+    ∀j. j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls
+Proof
+  Induct_on ‘ls’ >> Cases_on ‘i = 0’ >> rw [update_def, len_def, index_def] >> try_tac (ex_falso >> cooper_tac) >>
+  try_tac (
+    pop_last_assum (qspecl_assume [‘i' - 1’, ‘y’]) >>
+    pop_assum sg_premise_tac >- cooper_tac >>
+    pop_assum sg_premise_tac >- cooper_tac >>
+    rw [])
+  >> (
+    pop_assum (qspec_assume ‘j - 1’) >>
+    pop_assum sg_premise_tac >- cooper_tac >>
+    pop_assum sg_premise_tac >- cooper_tac >>
+    rw [])
+QED
+
+Theorem index_update_same:
+  ∀ls i j y.
+    0 <= i ==>
+    i < len ls ==>
+    j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls
+Proof
+  rpt strip_tac >>
+  qspecl_assume [‘ls’, ‘i’, ‘y’] update_spec >>
+  rw []
+QED
+
+Theorem index_update_diff:
+  ∀ls i j y.
+    0 <= i ==>
+    i < len ls ==>
+    index i (update ls i y) = y
+Proof
+  rpt strip_tac >>
+  qspecl_assume [‘ls’, ‘i’, ‘y’] update_spec >>
+  rw []
+QED
+
+Theorem vec_to_list_int_bounds:
+  !v. 0 <= len (vec_to_list v) /\ len (vec_to_list v) <= usize_max
+Proof
+  (* TODO *)
+  cheat
+QED
+
+val vec_len_def = Define ‘vec_len v = int_to_usize (len (vec_to_list v))’
+Theorem vec_len_spec:
+  ∀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
+Proof
+  gen_tac >> rw [vec_len_def] >>
+  qspec_assume ‘v’ vec_to_list_int_bounds >>
+  fs []
+QED
+
+val vec_index_def = Define ‘
+  vec_index i v = if usize_to_int i ≤ usize_to_int (vec_len v) 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”)
+
+(* Redefining ‘vec_insert_back’ *)
+val vec_insert_back_def = Define ‘
+  vec_insert_back (v : 'a vec) (i : usize) (x : 'a) = mk_vec (update (vec_to_list v) (usize_to_int i) x)’
+
+Theorem vec_insert_back_spec:
+  ∀v i x.
+    usize_to_int i < usize_to_int (vec_len v) ⇒
+    ∃nv. vec_insert_back v i x = Return nv ∧
+    vec_len v = vec_len nv ∧
+    vec_index i nv = Return x ∧
+    (∀j. usize_to_int j < usize_to_int (vec_len nv) ⇒ usize_to_int j ≠ usize_to_int i ⇒ vec_index j nv = vec_index j v)
+Proof
+  rpt strip_tac >> fs [vec_insert_back_def] >>
+  (* TODO: improve this? *)
+  qspec_assume ‘update (vec_to_list v) (usize_to_int i) x’ mk_vec_spec >>
+  sg_dep_rewrite_all_tac update_len >> fs [] >>
+  qspec_assume ‘v’ vec_len_spec >>
+  rw [] >> gvs [] >>
+  fs [vec_len_def, vec_index_def] >>
+  qspec_assume ‘i’ usize_to_int_bounds >>
+  sg_dep_rewrite_all_tac int_to_usize_id >- cooper_tac >> fs [] >>
+  sg_dep_rewrite_goal_tac index_update_diff >- cooper_tac >> fs [] >>
+  rw [] >>
+  irule index_update_same >> cooper_tac
+QED
+
+(* TODO: add theorems to the rewriting theorems
+from listSimps.sml:
+
+val LIST_ss = BasicProvers.thy_ssfrag "list"
+val _ = BasicProvers.logged_addfrags {thyname="list"} [LIST_EQ_ss]
+
+val list_rws = computeLib.add_thms
+  [
+   ALL_DISTINCT, APPEND, APPEND_NIL, CONS_11, DROP_compute, EL_restricted,
+   EL_simp_restricted, EVERY_DEF, EXISTS_DEF, FILTER, FIND_def, FLAT, FOLDL,
+   FOLDR, FRONT_DEF, GENLIST_AUX_compute, GENLIST_NUMERALS, HD, INDEX_FIND_def,
+   INDEX_OF_def, LAST_compute, LENGTH, LEN_DEF, LIST_APPLY_def, LIST_BIND_def,
+   LIST_IGNORE_BIND_def, LIST_LIFT2_def, LIST_TO_SET_THM, LLEX_def, LRC_def,
+   LUPDATE_compute, MAP, MAP2, NOT_CONS_NIL, NOT_NIL_CONS, NULL_DEF, oEL_def,
+   oHD_def,
+   PAD_LEFT, PAD_RIGHT, REVERSE_REV, REV_DEF, SHORTLEX_def, SNOC, SUM_ACC_DEF,
+   SUM_SUM_ACC,
+   TAKE_compute, TL, UNZIP, ZIP, computeLib.lazyfy_thm list_case_compute,
+   dropWhile_def, isPREFIX, list_size_def, nub_def, splitAtPki_def
+  ]
+
+fun list_compset () =
+   let
+      val base = reduceLib.num_compset()
+   in
+      list_rws base; base
+   end
+*)
+
 val _ = export_theory ()
diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index 75098bfe..cc2f3115 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -3,26 +3,40 @@ sig
   type thm = Thm.thm
   
   (*  Axioms  *)
+    val MK_VEC_SPEC : thm
     val VEC_TO_LIST_BOUNDS : thm
     val i128_to_int_bounds : thm
     val i16_to_int_bounds : thm
     val i32_to_int_bounds : thm
     val i64_to_int_bounds : thm
     val i8_to_int_bounds : thm
+    val int_to_i128_i128_to_int : thm
     val int_to_i128_id : thm
+    val int_to_i16_i16_to_int : thm
     val int_to_i16_id : thm
+    val int_to_i32_i32_to_int : thm
     val int_to_i32_id : thm
+    val int_to_i64_i64_to_int : thm
     val int_to_i64_id : thm
+    val int_to_i8_i8_to_int : thm
     val int_to_i8_id : thm
     val int_to_isize_id : thm
+    val int_to_isize_isize_to_int : thm
     val int_to_u128_id : thm
+    val int_to_u128_u128_to_int : thm
     val int_to_u16_id : thm
+    val int_to_u16_u16_to_int : thm
     val int_to_u32_id : thm
+    val int_to_u32_u32_to_int : thm
     val int_to_u64_id : thm
+    val int_to_u64_u64_to_int : thm
     val int_to_u8_id : thm
+    val int_to_u8_u8_to_int : thm
     val int_to_usize_id : thm
+    val int_to_usize_usize_to_int : thm
     val isize_bounds : thm
     val isize_to_int_bounds : thm
+    val mk_vec_spec : thm
     val u128_to_int_bounds : thm
     val u16_to_int_bounds : thm
     val u32_to_int_bounds : thm
@@ -72,12 +86,14 @@ 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
@@ -127,12 +143,17 @@ 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
     val usize_rem_def : thm
     val usize_sub_def : thm
+    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 I128_ADD_EQ : thm
@@ -159,6 +180,8 @@ sig
     val I8_MUL_EQ : thm
     val I8_REM_EQ : thm
     val I8_SUB_EQ : thm
+    val INT_OF_NUM : thm
+    val INT_OF_NUM_NEQ_INJ : thm
     val ISIZE_ADD_EQ : thm
     val ISIZE_DIV_EQ : thm
     val ISIZE_MUL_EQ : thm
@@ -193,6 +216,9 @@ sig
     val USIZE_MUL_EQ : thm
     val USIZE_REM_EQ : thm
     val USIZE_SUB_EQ : thm
+    val USIZE_TO_INT_INJ : thm
+    val USIZE_TO_INT_NEQ_INJ : thm
+    val VEC_NEW_SPEC : thm
     val VEC_TO_LIST_INT_BOUNDS : thm
     val datatype_error : thm
     val datatype_result : thm
@@ -207,6 +233,9 @@ sig
     val error_case_eq : thm
     val error_induction : thm
     val error_nchotomy : thm
+    val index_update_diff : thm
+    val index_update_same : thm
+    val int_induction : thm
     val num2error_11 : thm
     val num2error_ONTO : thm
     val num2error_error2num : thm
@@ -218,6 +247,12 @@ sig
     val result_distinct : thm
     val result_induction : thm
     val result_nchotomy : thm
+    val update_ind : thm
+    val update_len : thm
+    val update_spec : thm
+    val vec_insert_back_spec : thm
+    val vec_len_spec : thm
+    val vec_to_list_int_bounds : thm
   
   val primitives_grammars : type_grammar.grammar * term_grammar.grammar
 (*
@@ -225,61 +260,84 @@ sig
    
    [string] Parent theory of "primitives"
    
-   [int_to_u128_id]  Axiom
+   [mk_vec_spec]  Axiom
       
-      [oracles: ] [axioms: int_to_u128_id] []
-      ⊢ ∀n. 0 ≤ n ∧ n ≤ u128_max ⇒ u128_to_int (int_to_u128 n) = n
+      [oracles: ] [axioms: mk_vec_spec] []
+      ⊢ ∀l. len l ≤ usize_max ⇒ ∃v. mk_vec l = Return v ∧ vec_to_list v = l
    
-   [int_to_u64_id]  Axiom
+   [VEC_TO_LIST_BOUNDS]  Axiom
       
-      [oracles: ] [axioms: int_to_u64_id] []
-      ⊢ ∀n. 0 ≤ n ∧ n ≤ u64_max ⇒ u64_to_int (int_to_u64 n) = n
+      [oracles: ] [axioms: VEC_TO_LIST_BOUNDS] []
+      ⊢ ∀v. (let l = LENGTH (vec_to_list v) in 0 ≤ l ∧ l ≤ Num usize_max)
    
-   [int_to_u32_id]  Axiom
+   [isize_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_u32_id] []
-      ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ u32_to_int (int_to_u32 n) = n
+      [oracles: ] [axioms: isize_bounds] []
+      ⊢ isize_min ≤ i16_min ∧ isize_max ≥ i16_max
    
-   [int_to_u16_id]  Axiom
+   [usize_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_u16_id] []
-      ⊢ ∀n. 0 ≤ n ∧ n ≤ u16_max ⇒ u16_to_int (int_to_u16 n) = n
+      [oracles: ] [axioms: usize_bounds] [] ⊢ usize_max ≥ u16_max
    
-   [int_to_u8_id]  Axiom
+   [isize_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_u8_id] []
-      ⊢ ∀n. 0 ≤ n ∧ n ≤ u8_max ⇒ u8_to_int (int_to_u8 n) = n
+      [oracles: ] [axioms: isize_to_int_bounds] []
+      ⊢ ∀n. isize_min ≤ isize_to_int n ∧ isize_to_int n ≤ isize_max
    
-   [int_to_i128_id]  Axiom
+   [i8_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_i128_id] []
-      ⊢ ∀n. i128_min ≤ n ∧ n ≤ i128_max ⇒ i128_to_int (int_to_i128 n) = n
+      [oracles: ] [axioms: i8_to_int_bounds] []
+      ⊢ ∀n. i8_min ≤ i8_to_int n ∧ i8_to_int n ≤ i8_max
    
-   [int_to_i64_id]  Axiom
+   [i16_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_i64_id] []
-      ⊢ ∀n. i64_min ≤ n ∧ n ≤ i64_max ⇒ i64_to_int (int_to_i64 n) = n
+      [oracles: ] [axioms: i16_to_int_bounds] []
+      ⊢ ∀n. i16_min ≤ i16_to_int n ∧ i16_to_int n ≤ i16_max
    
-   [int_to_i32_id]  Axiom
+   [i32_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_i32_id] []
-      ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ i32_to_int (int_to_i32 n) = n
+      [oracles: ] [axioms: i32_to_int_bounds] []
+      ⊢ ∀n. i32_min ≤ i32_to_int n ∧ i32_to_int n ≤ i32_max
    
-   [int_to_i16_id]  Axiom
+   [i64_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_i16_id] []
-      ⊢ ∀n. i16_min ≤ n ∧ n ≤ i16_max ⇒ i16_to_int (int_to_i16 n) = n
+      [oracles: ] [axioms: i64_to_int_bounds] []
+      ⊢ ∀n. i64_min ≤ i64_to_int n ∧ i64_to_int n ≤ i64_max
    
-   [int_to_i8_id]  Axiom
+   [i128_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_i8_id] []
-      ⊢ ∀n. i8_min ≤ n ∧ n ≤ i8_max ⇒ i8_to_int (int_to_i8 n) = n
+      [oracles: ] [axioms: i128_to_int_bounds] []
+      ⊢ ∀n. i128_min ≤ i128_to_int n ∧ i128_to_int n ≤ i128_max
    
-   [int_to_usize_id]  Axiom
+   [usize_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_usize_id] []
-      ⊢ ∀n. 0 ≤ n ∧ (n ≤ u16_max ∨ n ≤ usize_max) ⇒
-            usize_to_int (int_to_usize n) = n
+      [oracles: ] [axioms: usize_to_int_bounds] []
+      ⊢ ∀n. 0 ≤ usize_to_int n ∧ usize_to_int n ≤ usize_max
+   
+   [u8_to_int_bounds]  Axiom
+      
+      [oracles: ] [axioms: u8_to_int_bounds] []
+      ⊢ ∀n. 0 ≤ u8_to_int n ∧ u8_to_int n ≤ u8_max
+   
+   [u16_to_int_bounds]  Axiom
+      
+      [oracles: ] [axioms: u16_to_int_bounds] []
+      ⊢ ∀n. 0 ≤ u16_to_int n ∧ u16_to_int n ≤ u16_max
+   
+   [u32_to_int_bounds]  Axiom
+      
+      [oracles: ] [axioms: u32_to_int_bounds] []
+      ⊢ ∀n. 0 ≤ u32_to_int n ∧ u32_to_int n ≤ u32_max
+   
+   [u64_to_int_bounds]  Axiom
+      
+      [oracles: ] [axioms: u64_to_int_bounds] []
+      ⊢ ∀n. 0 ≤ u64_to_int n ∧ u64_to_int n ≤ u64_max
+   
+   [u128_to_int_bounds]  Axiom
+      
+      [oracles: ] [axioms: u128_to_int_bounds] []
+      ⊢ ∀n. 0 ≤ u128_to_int n ∧ u128_to_int n ≤ u128_max
    
    [int_to_isize_id]  Axiom
       
@@ -287,79 +345,127 @@ sig
       ⊢ ∀n. (i16_min ≤ n ∨ isize_min ≤ n) ∧ (n ≤ i16_max ∨ n ≤ isize_max) ⇒
             isize_to_int (int_to_isize n) = n
    
-   [u128_to_int_bounds]  Axiom
+   [int_to_usize_id]  Axiom
       
-      [oracles: ] [axioms: u128_to_int_bounds] []
-      ⊢ ∀n. 0 ≤ u128_to_int n ∧ u128_to_int n ≤ u128_max
+      [oracles: ] [axioms: int_to_usize_id] []
+      ⊢ ∀n. 0 ≤ n ∧ (n ≤ u16_max ∨ n ≤ usize_max) ⇒
+            usize_to_int (int_to_usize n) = n
    
-   [u64_to_int_bounds]  Axiom
+   [int_to_i8_id]  Axiom
       
-      [oracles: ] [axioms: u64_to_int_bounds] []
-      ⊢ ∀n. 0 ≤ u64_to_int n ∧ u64_to_int n ≤ u64_max
+      [oracles: ] [axioms: int_to_i8_id] []
+      ⊢ ∀n. i8_min ≤ n ∧ n ≤ i8_max ⇒ i8_to_int (int_to_i8 n) = n
    
-   [u32_to_int_bounds]  Axiom
+   [int_to_i16_id]  Axiom
       
-      [oracles: ] [axioms: u32_to_int_bounds] []
-      ⊢ ∀n. 0 ≤ u32_to_int n ∧ u32_to_int n ≤ u32_max
+      [oracles: ] [axioms: int_to_i16_id] []
+      ⊢ ∀n. i16_min ≤ n ∧ n ≤ i16_max ⇒ i16_to_int (int_to_i16 n) = n
    
-   [u16_to_int_bounds]  Axiom
+   [int_to_i32_id]  Axiom
       
-      [oracles: ] [axioms: u16_to_int_bounds] []
-      ⊢ ∀n. 0 ≤ u16_to_int n ∧ u16_to_int n ≤ u16_max
+      [oracles: ] [axioms: int_to_i32_id] []
+      ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ i32_to_int (int_to_i32 n) = n
    
-   [u8_to_int_bounds]  Axiom
+   [int_to_i64_id]  Axiom
       
-      [oracles: ] [axioms: u8_to_int_bounds] []
-      ⊢ ∀n. 0 ≤ u8_to_int n ∧ u8_to_int n ≤ u8_max
+      [oracles: ] [axioms: int_to_i64_id] []
+      ⊢ ∀n. i64_min ≤ n ∧ n ≤ i64_max ⇒ i64_to_int (int_to_i64 n) = n
    
-   [usize_to_int_bounds]  Axiom
+   [int_to_i128_id]  Axiom
       
-      [oracles: ] [axioms: usize_to_int_bounds] []
-      ⊢ ∀n. 0 ≤ usize_to_int n ∧ usize_to_int n ≤ usize_max
+      [oracles: ] [axioms: int_to_i128_id] []
+      ⊢ ∀n. i128_min ≤ n ∧ n ≤ i128_max ⇒ i128_to_int (int_to_i128 n) = n
    
-   [i128_to_int_bounds]  Axiom
+   [int_to_u8_id]  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_id] []
+      ⊢ ∀n. 0 ≤ n ∧ n ≤ u8_max ⇒ u8_to_int (int_to_u8 n) = n
    
-   [i64_to_int_bounds]  Axiom
+   [int_to_u16_id]  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_id] []
+      ⊢ ∀n. 0 ≤ n ∧ n ≤ u16_max ⇒ u16_to_int (int_to_u16 n) = n
    
-   [i32_to_int_bounds]  Axiom
+   [int_to_u32_id]  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_id] []
+      ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ u32_to_int (int_to_u32 n) = n
    
-   [i16_to_int_bounds]  Axiom
+   [int_to_u64_id]  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_id] []
+      ⊢ ∀n. 0 ≤ n ∧ n ≤ u64_max ⇒ u64_to_int (int_to_u64 n) = n
    
-   [i8_to_int_bounds]  Axiom
+   [int_to_u128_id]  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_id] []
+      ⊢ ∀n. 0 ≤ n ∧ n ≤ u128_max ⇒ u128_to_int (int_to_u128 n) = n
    
-   [isize_to_int_bounds]  Axiom
+   [int_to_i8_i8_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_i8_i8_to_int] []
+      ⊢ ∀i. int_to_i8 (i8_to_int i) = i
    
-   [usize_bounds]  Axiom
+   [int_to_i16_i16_to_int]  Axiom
       
-      [oracles: ] [axioms: usize_bounds] [] ⊢ usize_max ≥ u16_max
+      [oracles: ] [axioms: int_to_i16_i16_to_int] []
+      ⊢ ∀i. int_to_i16 (i16_to_int i) = i
    
-   [isize_bounds]  Axiom
+   [int_to_i32_i32_to_int]  Axiom
       
-      [oracles: ] [axioms: isize_bounds] []
-      ⊢ isize_min ≤ i16_min ∧ isize_max ≥ i16_max
+      [oracles: ] [axioms: int_to_i32_i32_to_int] []
+      ⊢ ∀i. int_to_i32 (i32_to_int i) = i
    
-   [VEC_TO_LIST_BOUNDS]  Axiom
+   [int_to_i64_i64_to_int]  Axiom
       
-      [oracles: ] [axioms: VEC_TO_LIST_BOUNDS] []
-      ⊢ ∀v. (let l = LENGTH (vec_to_list v) in 0 ≤ l ∧ l ≤ 4294967295)
+      [oracles: ] [axioms: int_to_i64_i64_to_int] []
+      ⊢ ∀i. int_to_i64 (i64_to_int i) = i
+   
+   [int_to_i128_i128_to_int]  Axiom
+      
+      [oracles: ] [axioms: int_to_i128_i128_to_int] []
+      ⊢ ∀i. int_to_i128 (i128_to_int i) = i
+   
+   [int_to_isize_isize_to_int]  Axiom
+      
+      [oracles: ] [axioms: int_to_isize_isize_to_int] []
+      ⊢ ∀i. int_to_isize (isize_to_int i) = i
+   
+   [int_to_u8_u8_to_int]  Axiom
+      
+      [oracles: ] [axioms: int_to_u8_u8_to_int] []
+      ⊢ ∀i. int_to_u8 (u8_to_int i) = i
+   
+   [int_to_u16_u16_to_int]  Axiom
+      
+      [oracles: ] [axioms: int_to_u16_u16_to_int] []
+      ⊢ ∀i. int_to_u16 (u16_to_int i) = i
+   
+   [int_to_u32_u32_to_int]  Axiom
+      
+      [oracles: ] [axioms: int_to_u32_u32_to_int] []
+      ⊢ ∀i. int_to_u32 (u32_to_int i) = i
+   
+   [int_to_u64_u64_to_int]  Axiom
+      
+      [oracles: ] [axioms: int_to_u64_u64_to_int] []
+      ⊢ ∀i. int_to_u64 (u64_to_int i) = i
+   
+   [int_to_u128_u128_to_int]  Axiom
+      
+      [oracles: ] [axioms: int_to_u128_u128_to_int] []
+      ⊢ ∀i. int_to_u128 (u128_to_int i) = i
+   
+   [int_to_usize_usize_to_int]  Axiom
+      
+      [oracles: ] [axioms: int_to_usize_usize_to_int] []
+      ⊢ ∀i. int_to_usize (usize_to_int i) = i
+   
+   [MK_VEC_SPEC]  Axiom
+      
+      [oracles: ] [axioms: MK_VEC_SPEC] []
+      ⊢ ∀l. &LENGTH l ≤ usize_max ⇒
+            ∃v. mk_vec l = Return v ∧ vec_to_list v = l
    
    [bind_def]  Definition
       
@@ -554,6 +660,12 @@ 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.
@@ -586,6 +698,10 @@ 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
@@ -857,6 +973,15 @@ 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)
@@ -883,9 +1008,32 @@ sig
       
       ⊢ ∀x y. usize_sub x y = mk_usize (usize_to_int x − usize_to_int y)
    
+   [vec_index_def]  Definition
+      
+      ⊢ ∀i v.
+          vec_index i v =
+          if usize_to_int i ≤ usize_to_int (vec_len v) then
+            Return (index (usize_to_int i) (vec_to_list v))
+          else Fail Failure
+   
+   [vec_insert_back_def]  Definition
+      
+      ⊢ ∀v i x.
+          vec_insert_back v i x =
+          mk_vec (update (vec_to_list v) (usize_to_int i) x)
+   
    [vec_len_def]  Definition
       
-      ⊢ ∀v. vec_len v = int_to_u32 (&LENGTH (vec_to_list v))
+      ⊢ ∀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])
    
    [I128_ADD_EQ]  Theorem
       
@@ -1140,6 +1288,14 @@ sig
           ∃z. i8_sub x y = Return z ∧
               i8_to_int z = i8_to_int x − i8_to_int y
    
+   [INT_OF_NUM]  Theorem
+      
+      ⊢ ∀i. 0 ≤ i ⇒ &Num i = i
+   
+   [INT_OF_NUM_NEQ_INJ]  Theorem
+      
+      ⊢ ∀n m. &n ≠ &m ⇒ n ≠ m
+   
    [ISIZE_ADD_EQ]  Theorem
       
       [oracles: DISK_THM]
@@ -1495,10 +1651,26 @@ sig
           ∃z. usize_sub x y = Return z ∧
               usize_to_int z = usize_to_int x − usize_to_int y
    
+   [USIZE_TO_INT_INJ]  Theorem
+      
+      [oracles: DISK_THM] [axioms: int_to_usize_usize_to_int] []
+      ⊢ ∀i j. usize_to_int i = usize_to_int j ⇔ i = j
+   
+   [USIZE_TO_INT_NEQ_INJ]  Theorem
+      
+      [oracles: DISK_THM] [axioms: int_to_usize_usize_to_int] []
+      ⊢ ∀i j. i ≠ j ⇒ usize_to_int i ≠ usize_to_int j
+   
+   [VEC_NEW_SPEC]  Theorem
+      
+      [oracles: DISK_THM] [axioms: usize_bounds, MK_VEC_SPEC] []
+      ⊢ vec_to_list vec_new = []
+   
    [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)
+      [oracles: DISK_THM] [axioms: usize_bounds, VEC_TO_LIST_BOUNDS] []
+      ⊢ ∀v. 0 ≤ &LENGTH (vec_to_list v) ∧
+            &LENGTH (vec_to_list v) ≤ usize_max
    
    [datatype_error]  Theorem
       
@@ -1554,6 +1726,23 @@ sig
       
       ⊢ ∀a. a = Failure
    
+   [index_update_diff]  Theorem
+      
+      ⊢ ∀ls i j y. 0 ≤ i ⇒ i < len ls ⇒ index i (update ls i y) = y
+   
+   [index_update_same]  Theorem
+      
+      ⊢ ∀ls i j y.
+          0 ≤ i ⇒
+          i < len ls ⇒
+          j < len ls ⇒
+          j ≠ i ⇒
+          index j (update ls i y) = index j ls
+   
+   [int_induction]  Theorem
+      
+      ⊢ ∀P. P 0 ∧ (∀i. 0 ≤ i ∧ P i ⇒ P (i + 1)) ⇒ ∀i. 0 ≤ i ⇒ P i
+   
    [num2error_11]  Theorem
       
       ⊢ ∀r r'. r < 1 ⇒ r' < 1 ⇒ (num2error r = num2error r' ⇔ r = r')
@@ -1607,6 +1796,48 @@ sig
       
       ⊢ ∀rr. (∃a. rr = Return a) ∨ (∃e. rr = Fail e) ∨ rr = Loop
    
+   [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
+   
+   [update_spec]  Theorem
+      
+      ⊢ ∀ls i y.
+          0 ≤ i ⇒
+          i < len ls ⇒
+          len (update ls i y) = len ls ∧ index i (update ls i y) = y ∧
+          ∀j. j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls
+   
+   [vec_insert_back_spec]  Theorem
+      
+      [oracles: DISK_THM, cheat]
+      [axioms: usize_to_int_bounds, int_to_usize_id, mk_vec_spec] []
+      ⊢ ∀v i x.
+          usize_to_int i < usize_to_int (vec_len v) ⇒
+          ∃nv.
+            vec_insert_back v i x = Return nv ∧ vec_len v = vec_len nv ∧
+            vec_index i nv = Return x ∧
+            ∀j. usize_to_int j < usize_to_int (vec_len nv) ⇒
+                usize_to_int j ≠ usize_to_int i ⇒
+                vec_index j nv = vec_index j v
+   
+   [vec_len_spec]  Theorem
+      
+      [oracles: DISK_THM, cheat] [axioms: ] []
+      ⊢ ∀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: ] []
+      ⊢ ∀v. 0 ≤ len (vec_to_list v) ∧ len (vec_to_list v) ≤ usize_max
+   
    
 *)
 end
diff --git a/backends/hol4/testScript.sml b/backends/hol4/testScript.sml
index fe1c1e11..a2d15117 100644
--- a/backends/hol4/testScript.sml
+++ b/backends/hol4/testScript.sml
@@ -722,7 +722,7 @@ fun op PARTIAL_THEN1 (tac1: tactic) (tac2: tactic) : tactic = tac1 THEN_LT (NTH_
    
    If the lemma is not an implication, we directly call the theorem tactic.
  *)
-fun intro_premise_then (premise_tac: tactic) (then_tac: thm_tactic) (thm : thm)  : 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 *)
@@ -734,9 +734,9 @@ fun intro_premise_then (premise_tac: tactic) (then_tac: thm_tactic) (thm : thm)
     if is_imp c then prove_premise_then (fst (dest_imp c)) else no_prove_premise_then
   end
 
-(* Same as {!intro_premise_then} but fails if the premise_tac fails to prove the premise *)
+(* 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 =
-  intro_premise_then
+  sg_premise_then
     (premise_tac >> FAIL_TAC "prove_premise_then: could not prove premise")
     then_tac thm
 
@@ -1294,7 +1294,7 @@ fun pure_progress_with (premise_tac : tactic)
     val th = PURE_REWRITE_RULE [GSYM satTheory.AND_IMP] th;
   in
     (* Apply the theorem *)
-    intro_premise_then premise_tac (then_tac fgoal) th (asms, g)
+    sg_premise_then premise_tac (then_tac fgoal) th (asms, g)
   end
 
 (*