Cleanup a bit the HOL4 backend and implement eval_conv

14 files changed, 238 insertions, 56 deletions

diff --git a/backends/hol4/divDefExampleScript.sml b/backends/hol4/divDefExampleScript.sml
index 338385ab..4a17977c 100644
--- a/backends/hol4/divDefExampleScript.sml
+++ b/backends/hol4/divDefExampleScript.sml
@@ -1,11 +1,6 @@
 (* Manually written examples of how to use the fixed-point operator from divDefScript *)
 
-open HolKernel boolLib bossLib Parse
-open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
-
-open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
-open primitivesLib
-open divDefTheory
+open primitivesLib divDefTheory
 
 val _ = new_theory "divDefExample"
 
diff --git a/backends/hol4/divDefLib.sml b/backends/hol4/divDefLib.sml
index 78e664e6..1e95b6c5 100644
--- a/backends/hol4/divDefLib.sml
+++ b/backends/hol4/divDefLib.sml
@@ -1,12 +1,7 @@
 structure divDefLib :> divDefLib =
 struct
 
-open HolKernel boolLib bossLib Parse
-open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
-
-open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
-open primitivesLib
-open divDefTheory
+open primitivesBaseTacLib primitivesLib divDefTheory
 
 val dbg = ref false
 fun print_dbg s = if (!dbg) then print s else ()
@@ -907,7 +902,7 @@ fun DefineDiv (def_qt : term quotation) =
     (* Because [store_definition] overrides existing names, it seems that in
        practice we don't really need to  delete the previous definitions
        (we still do it: it doesn't cost much). *)
-    val _ = map delete_binding thm_names
+    val _ = app delete_binding thm_names
     val _ = map store_definition (zip thm_names def_eqs)
   in
     def_eqs
diff --git a/backends/hol4/divDefLibTestScript.sml b/backends/hol4/divDefLibTestScript.sml
index f5df6139..2e6d56b6 100644
--- a/backends/hol4/divDefLibTestScript.sml
+++ b/backends/hol4/divDefLibTestScript.sml
@@ -1,6 +1,7 @@
 (* Examples which use divDefLib.DefineDiv *)
 
-open primitivesLib divDefLib
+open HolKernel
+open divDefLib
 
 val _ = new_theory "divDefLibTest"
 
diff --git a/backends/hol4/divDefNoFixLib.sml b/backends/hol4/divDefNoFixLib.sml
index 59319e6a..f7b9763d 100644
--- a/backends/hol4/divDefNoFixLib.sml
+++ b/backends/hol4/divDefNoFixLib.sml
@@ -3,11 +3,7 @@
 structure divDefNoFixLib :> divDefNoFixLib =
 struct
 
-open HolKernel boolLib bossLib Parse
-open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
-
-open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
-open primitivesLib
+open primitivesArithTheory primitivesBaseTacLib primitivesLib
 
 val case_result_same_eq = prove (
   “!(r : 'a result).
@@ -849,7 +845,7 @@ fun prove_termination_thms
       in
         (* Apply the theorem, prove the premise, and rewrite *)
         (prove_premise_then premise_tac assume_tac eq_th >> fs []) (asms, g)
-      end handle NotFound => all_tac (asms, g)
+      end handle Redblackmap.NotFound => all_tac (asms, g)
           | HOL_ERR _ => all_tac (asms, g) (* Getting the function name can also fail *)
   
     fun prove_one ((pred_tm, fun_eq_tm), pred_n_imp_pred_least_thm) :
diff --git a/backends/hol4/divDefNoFixLibTestScript.sml b/backends/hol4/divDefNoFixLibTestScript.sml
index b2a4d607..f613c327 100644
--- a/backends/hol4/divDefNoFixLibTestScript.sml
+++ b/backends/hol4/divDefNoFixLibTestScript.sml
@@ -1,8 +1,5 @@
-open HolKernel boolLib bossLib Parse
-open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
-
-open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
-open primitivesLib divDefNoFixLib
+open HolKernel
+open divDefNoFixLib
 
 val _ = new_theory "divDefNoFixLibTest"
 
diff --git a/backends/hol4/divDefScript.sml b/backends/hol4/divDefScript.sml
index cc745e5d..8ef99530 100644
--- a/backends/hol4/divDefScript.sml
+++ b/backends/hol4/divDefScript.sml
@@ -7,11 +7,7 @@
    how to use it.
  *)
 
-open HolKernel boolLib bossLib Parse
-open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
-
-open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
-open primitivesLib
+open primitivesArithTheory primitivesBaseTacLib primitivesTheory primitivesLib
 
 val _ = new_theory "divDef"
 
diff --git a/backends/hol4/ilistScript.sml b/backends/hol4/ilistScript.sml
index f382d95d..157b5c00 100644
--- a/backends/hol4/ilistScript.sml
+++ b/backends/hol4/ilistScript.sml
@@ -1,6 +1,4 @@
-open HolKernel boolLib bossLib Parse
-open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
-
+open listTheory
 open primitivesArithTheory primitivesBaseTacLib
 
 (* The following theory contains alternative definitions of functions operating
diff --git a/backends/hol4/ilistTheory.sig b/backends/hol4/ilistTheory.sig
index f155a328..21545b6e 100644
--- a/backends/hol4/ilistTheory.sig
+++ b/backends/hol4/ilistTheory.sig
@@ -20,8 +20,6 @@ sig
 (*
    [primitivesArith] Parent theory of "ilist"
    
-   [string] Parent theory of "ilist"
-   
    [index_def]  Definition
       
       ⊢ ∀i x ls.
diff --git a/backends/hol4/primitivesArithScript.sml b/backends/hol4/primitivesArithScript.sml
index b7b44b25..679ed2cd 100644
--- a/backends/hol4/primitivesArithScript.sml
+++ b/backends/hol4/primitivesArithScript.sml
@@ -1,5 +1,4 @@
-open HolKernel boolLib bossLib Parse
-open boolTheory arithmeticTheory integerTheory intLib listTheory
+open arithmeticTheory integerTheory
 open primitivesBaseTacLib
 
 val _ = new_theory "primitivesArith"
diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml
index 133f6a99..3d6d9e3e 100644
--- a/backends/hol4/primitivesBaseTacLib.sml
+++ b/backends/hol4/primitivesBaseTacLib.sml
@@ -2,8 +2,7 @@
 structure primitivesBaseTacLib =
 struct
 
-open HolKernel boolLib bossLib Parse
-open boolTheory arithmeticTheory integerTheory intLib listTheory
+open HolKernel boolLib bossLib intLib
 
 val debug = ref false
 
diff --git a/backends/hol4/primitivesLib.sml b/backends/hol4/primitivesLib.sml
index cf7368a6..eed50e25 100644
--- a/backends/hol4/primitivesLib.sml
+++ b/backends/hol4/primitivesLib.sml
@@ -2,10 +2,7 @@
 structure primitivesLib =
 struct
 
-open HolKernel boolLib bossLib Parse
-open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
-
-open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
+open primitivesBaseTacLib primitivesTheory
 
 val primitives_theory_name = "primitives"
 
diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml
index 5ef51f2e..2a13e76d 100644
--- a/backends/hol4/primitivesScript.sml
+++ b/backends/hol4/primitivesScript.sml
@@ -1,10 +1,7 @@
-open HolKernel boolLib bossLib Parse
-open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
-
+open stringTheory
 open primitivesArithTheory primitivesBaseTacLib ilistTheory
 
-val primitives_theory_name = "primitives"
-val _ = new_theory primitives_theory_name
+val _ = new_theory "primitives"
 
 (*** Result *)
 Datatype:
@@ -203,7 +200,6 @@ val all_to_int_bounds_lemmas = [
    Note that for isize and usize, we write the lemmas in such a way that the
    proofs are easily automatable for constants.
  *)
-(* TODO: remove the condition on u16_max, and make the massage tactic automatically use usize_bounds *)
 val isize_to_int_int_to_isize =
   new_axiom ("isize_to_int_int_to_isize",
     “!n. isize_min <= n /\ n <= isize_max ==> isize_to_int (int_to_isize n) = n”)
@@ -252,8 +248,7 @@ val u128_to_int_int_to_u128 =
   new_axiom ("u128_to_int_int_to_u128",
     “!n. 0 <= n /\ n <= u128_max ==> u128_to_int (int_to_u128 n) = n”)
 
-(* TODO: rename *)
-val all_conversion_id_lemmas = [
+val all_int_to_scalar_to_int_lemmas = [
   isize_to_int_int_to_isize,
   i8_to_int_int_to_i8,
   i16_to_int_int_to_i16,
@@ -268,6 +263,103 @@ val all_conversion_id_lemmas = [
   u128_to_int_int_to_u128
 ]
 
+val prove_int_to_scalar_to_int_unfold_tac =
+  assume_tac isize_bounds >> (* Only useful for isize of course *)
+  assume_tac usize_bounds >> (* Only useful for usize of course *)
+  rw [] >> MAP_FIRST irule all_int_to_scalar_to_int_lemmas >> int_tac
+
+(* Custom unfolding lemmas for the purpose of evaluation *)
+
+(* For isize, we don't use isize_{min,max} (which are opaque) but i16_{min,max} *)
+Theorem isize_to_int_int_to_isize_unfold:
+  ∀n. isize_to_int (int_to_isize n) = if i16_min <= n /\ n <= i16_max then n else isize_to_int (int_to_isize n)
+Proof
+  prove_int_to_scalar_to_int_unfold_tac
+QED
+
+Theorem i8_to_int_int_to_i8_unfold:
+  ∀n. i8_to_int (int_to_i8 n) = if i8_min <= n /\ n <= i8_max then n else i8_to_int (int_to_i8 n)
+Proof
+  prove_int_to_scalar_to_int_unfold_tac
+QED
+
+Theorem i16_to_int_int_to_i16_unfold:
+  ∀n. i16_to_int (int_to_i16 n) = if i16_min <= n /\ n <= i16_max then n else i16_to_int (int_to_i16 n)
+Proof
+  prove_int_to_scalar_to_int_unfold_tac
+QED
+
+Theorem i32_to_int_int_to_i32_unfold:
+  ∀n. i32_to_int (int_to_i32 n) = if i32_min <= n /\ n <= i32_max then n else i32_to_int (int_to_i32 n)
+Proof
+  prove_int_to_scalar_to_int_unfold_tac
+QED
+
+Theorem i64_to_int_int_to_i64_unfold:
+  ∀n. i64_to_int (int_to_i64 n) = if i64_min <= n /\ n <= i64_max then n else i64_to_int (int_to_i64 n)
+Proof
+  prove_int_to_scalar_to_int_unfold_tac
+QED
+
+Theorem i128_to_int_int_to_i128_unfold:
+  ∀n. i128_to_int (int_to_i128 n) = if i128_min <= n /\ n <= i128_max then n else i128_to_int (int_to_i128 n)
+Proof
+  prove_int_to_scalar_to_int_unfold_tac
+QED
+
+(* For usize, we don't use isize_{min,max} (which are opaque) but u16_{min,max} *)
+Theorem usize_to_int_int_to_usize_unfold:
+  ∀n. usize_to_int (int_to_usize n) = if 0 ≤ n ∧ n <= u16_max then n else usize_to_int (int_to_usize n)
+Proof
+  prove_int_to_scalar_to_int_unfold_tac
+QED
+
+Theorem u8_to_int_int_to_u8_unfold:
+  ∀n. u8_to_int (int_to_u8 n) = if 0 <= n /\ n <= u8_max then n else u8_to_int (int_to_u8 n)
+Proof
+  prove_int_to_scalar_to_int_unfold_tac
+QED
+
+Theorem u16_to_int_int_to_u16_unfold:
+  ∀n. u16_to_int (int_to_u16 n) = if 0 <= n /\ n <= u16_max then n else u16_to_int (int_to_u16 n)
+Proof
+  prove_int_to_scalar_to_int_unfold_tac
+QED
+
+Theorem u32_to_int_int_to_u32_unfold:
+  ∀n. u32_to_int (int_to_u32 n) = if 0 <= n /\ n <= u32_max then n else u32_to_int (int_to_u32 n)
+Proof
+  prove_int_to_scalar_to_int_unfold_tac
+QED
+
+Theorem u64_to_int_int_to_u64_unfold:
+  ∀n. u64_to_int (int_to_u64 n) = if 0 <= n /\ n <= u64_max then n else u64_to_int (int_to_u64 n)
+Proof
+  prove_int_to_scalar_to_int_unfold_tac
+QED
+
+Theorem u128_to_int_int_to_u128_unfold:
+  ∀n. u128_to_int (int_to_u128 n) = if 0 <= n /\ n <= u128_max then n else u128_to_int (int_to_u128 n)
+Proof
+  prove_int_to_scalar_to_int_unfold_tac
+QED
+
+val all_int_to_scalar_to_int_unfold_lemmas = [
+  isize_to_int_int_to_isize_unfold,
+  i8_to_int_int_to_i8_unfold,
+  i16_to_int_int_to_i16_unfold,
+  i32_to_int_int_to_i32_unfold,
+  i64_to_int_int_to_i64_unfold,
+  i128_to_int_int_to_i128_unfold,
+  usize_to_int_int_to_usize_unfold,
+  u8_to_int_int_to_u8_unfold,
+  u16_to_int_int_to_u16_unfold,
+  u32_to_int_int_to_u32_unfold,
+  u64_to_int_int_to_u64_unfold,
+  u128_to_int_int_to_u128_unfold
+]
+val _ = evalLib.add_unfold_thms (all_int_to_scalar_to_int_unfold_lemmas)
+
 val int_to_i8_i8_to_int       = new_axiom ("int_to_i8_i8_to_int",       “∀i. int_to_i8 (i8_to_int i) = i”)
 val int_to_i16_i16_to_int     = new_axiom ("int_to_i16_i16_to_int",     “∀i. int_to_i16 (i16_to_int i) = i”)
 val int_to_i32_i32_to_int     = new_axiom ("int_to_i32_i32_to_int",     “∀i. int_to_i32 (i32_to_int i) = i”)
@@ -282,6 +374,22 @@ val int_to_u64_u64_to_int     = new_axiom ("int_to_u64_u64_to_int",     “∀i.
 val int_to_u128_u128_to_int   = new_axiom ("int_to_u128_u128_to_int",   “∀i. int_to_u128 (u128_to_int i) = i”)
 val int_to_usize_usize_to_int = new_axiom ("int_to_usize_usize_to_int", “∀i. int_to_usize (usize_to_int i) = i”)
 
+val all_scalar_to_int_to_scalar_lemmas = [
+  int_to_i8_i8_to_int,
+  int_to_i16_i16_to_int,
+  int_to_i32_i32_to_int,
+  int_to_i64_i64_to_int,
+  int_to_i128_i128_to_int,
+  int_to_isize_isize_to_int,
+  int_to_u8_u8_to_int,
+  int_to_u16_u16_to_int,
+  int_to_u32_u32_to_int,
+  int_to_u64_u64_to_int,
+  int_to_u128_u128_to_int,
+  int_to_usize_usize_to_int
+]
+val _ = evalLib.add_rewrites all_scalar_to_int_to_scalar_lemmas
+
 (** Utilities to define the arithmetic operations *)
 val mk_isize_def = Define
   ‘mk_isize n =
@@ -558,7 +666,7 @@ val (asms,g) = top_goal ()
 
 fun prove_arith_unop_eq (asms, g) =
   let
-    val rw_thms = List.concat [all_neg_defs, all_mk_int_defs, all_conversion_id_lemmas]
+    val rw_thms = List.concat [all_neg_defs, all_mk_int_defs, all_int_to_scalar_to_int_lemmas]
   in
     (rpt gen_tac >>
      rpt disch_tac >>
@@ -630,7 +738,7 @@ fun prove_arith_op_eq (asms, g) =
       | _ => failwith "Unexpected"
     val x = (snd o dest_comb) x_to_int;
     val y = (snd o dest_comb) y_to_int;
-    val rw_thms = int_rem_def :: List.concat [all_rem_defs, all_add_defs, all_sub_defs, all_mul_defs, all_div_defs, all_mk_int_defs, all_to_int_bounds_lemmas, all_conversion_id_lemmas];
+    val rw_thms = int_rem_def :: List.concat [all_rem_defs, all_add_defs, all_sub_defs, all_mul_defs, all_div_defs, all_mk_int_defs, all_to_int_bounds_lemmas, all_int_to_scalar_to_int_lemmas];
     fun inst_first_lem arg lems =
       map_first_tac (fn th => (assume_tac (SPEC arg th) handle HOL_ERR _ => fail_tac "")) lems;
   in
@@ -650,11 +758,11 @@ fun prove_arith_op_eq (asms, g) =
        qspecl_assume [‘^x_to_int’, ‘^y_to_int’] pos_div_pos_le_init >>
        cooper_tac,
        (* For remainder *)
-       dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC all_conversion_id_lemmas >> fs [] >>
+       dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC all_int_to_scalar_to_int_lemmas >> fs [] >>
        qspecl_assume [‘^x_to_int’, ‘^y_to_int’] pos_mod_pos_is_pos >>
        qspecl_assume [‘^x_to_int’, ‘^y_to_int’] pos_mod_pos_le_init >>
        cooper_tac,
-       dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC all_conversion_id_lemmas >> fs []
+       dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC all_int_to_scalar_to_int_lemmas >> fs []
      ]) (asms, g)
   end
 
diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index 3b029c05..3e82565c 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -225,30 +225,35 @@ sig
     val i128_neg_eq : thm
     val i128_rem_eq : thm
     val i128_sub_eq : thm
+    val i128_to_int_int_to_i128_unfold : thm
     val i16_add_eq : thm
     val i16_div_eq : thm
     val i16_mul_eq : thm
     val i16_neg_eq : thm
     val i16_rem_eq : thm
     val i16_sub_eq : thm
+    val i16_to_int_int_to_i16_unfold : thm
     val i32_add_eq : thm
     val i32_div_eq : thm
     val i32_mul_eq : thm
     val i32_neg_eq : thm
     val i32_rem_eq : thm
     val i32_sub_eq : thm
+    val i32_to_int_int_to_i32_unfold : thm
     val i64_add_eq : thm
     val i64_div_eq : thm
     val i64_mul_eq : thm
     val i64_neg_eq : thm
     val i64_rem_eq : thm
     val i64_sub_eq : thm
+    val i64_to_int_int_to_i64_unfold : thm
     val i8_add_eq : thm
     val i8_div_eq : thm
     val i8_mul_eq : thm
     val i8_neg_eq : thm
     val i8_rem_eq : thm
     val i8_sub_eq : thm
+    val i8_to_int_int_to_i8_unfold : thm
     val index_update_diff : thm
     val index_update_same : thm
     val isize_add_eq : thm
@@ -257,6 +262,7 @@ sig
     val isize_neg_eq : thm
     val isize_rem_eq : thm
     val isize_sub_eq : thm
+    val isize_to_int_int_to_isize_unfold : thm
     val num2error_11 : thm
     val num2error_ONTO : thm
     val num2error_error2num : thm
@@ -273,26 +279,31 @@ sig
     val u128_mul_eq : thm
     val u128_rem_eq : thm
     val u128_sub_eq : thm
+    val u128_to_int_int_to_u128_unfold : thm
     val u16_add_eq : thm
     val u16_div_eq : thm
     val u16_mul_eq : thm
     val u16_rem_eq : thm
     val u16_sub_eq : thm
+    val u16_to_int_int_to_u16_unfold : thm
     val u32_add_eq : thm
     val u32_div_eq : thm
     val u32_mul_eq : thm
     val u32_rem_eq : thm
     val u32_sub_eq : thm
+    val u32_to_int_int_to_u32_unfold : thm
     val u64_add_eq : thm
     val u64_div_eq : thm
     val u64_mul_eq : thm
     val u64_rem_eq : thm
     val u64_sub_eq : thm
+    val u64_to_int_int_to_u64_unfold : thm
     val u8_add_eq : thm
     val u8_div_eq : thm
     val u8_mul_eq : thm
     val u8_rem_eq : thm
     val u8_sub_eq : thm
+    val u8_to_int_int_to_u8_unfold : thm
     val update_len : thm
     val update_spec : thm
     val usize_add_eq : thm
@@ -300,6 +311,7 @@ sig
     val usize_mul_eq : thm
     val usize_rem_eq : thm
     val usize_sub_eq : thm
+    val usize_to_int_int_to_usize_unfold : thm
     val vec_insert_back_spec : thm
     val vec_len_spec : thm
     val vec_to_list_int_bounds : thm
@@ -308,6 +320,8 @@ sig
 (*
    [ilist] Parent theory of "primitives"
    
+   [string] Parent theory of "primitives"
+   
    [isize_bounds]  Axiom
       
       [oracles: ] [axioms: isize_bounds] []
@@ -1390,6 +1404,14 @@ sig
           ∃z. i128_sub x y = Return z ∧
               i128_to_int z = i128_to_int x − i128_to_int y
    
+   [i128_to_int_int_to_i128_unfold]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: usize_bounds, i128_to_int_int_to_i128, isize_bounds] []
+      ⊢ ∀n. i128_to_int (int_to_i128 n) =
+            if i128_min ≤ n ∧ n ≤ i128_max then n
+            else i128_to_int (int_to_i128 n)
+   
    [i16_add_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -1451,6 +1473,14 @@ sig
           ∃z. i16_sub x y = Return z ∧
               i16_to_int z = i16_to_int x − i16_to_int y
    
+   [i16_to_int_int_to_i16_unfold]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: usize_bounds, i16_to_int_int_to_i16, isize_bounds] []
+      ⊢ ∀n. i16_to_int (int_to_i16 n) =
+            if i16_min ≤ n ∧ n ≤ i16_max then n
+            else i16_to_int (int_to_i16 n)
+   
    [i32_add_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -1512,6 +1542,14 @@ sig
           ∃z. i32_sub x y = Return z ∧
               i32_to_int z = i32_to_int x − i32_to_int y
    
+   [i32_to_int_int_to_i32_unfold]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: usize_bounds, i32_to_int_int_to_i32, isize_bounds] []
+      ⊢ ∀n. i32_to_int (int_to_i32 n) =
+            if i32_min ≤ n ∧ n ≤ i32_max then n
+            else i32_to_int (int_to_i32 n)
+   
    [i64_add_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -1573,6 +1611,14 @@ sig
           ∃z. i64_sub x y = Return z ∧
               i64_to_int z = i64_to_int x − i64_to_int y
    
+   [i64_to_int_int_to_i64_unfold]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: usize_bounds, i64_to_int_int_to_i64, isize_bounds] []
+      ⊢ ∀n. i64_to_int (int_to_i64 n) =
+            if i64_min ≤ n ∧ n ≤ i64_max then n
+            else i64_to_int (int_to_i64 n)
+   
    [i8_add_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -1634,6 +1680,13 @@ sig
           ∃z. i8_sub x y = Return z ∧
               i8_to_int z = i8_to_int x − i8_to_int y
    
+   [i8_to_int_int_to_i8_unfold]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: usize_bounds, i8_to_int_int_to_i8, isize_bounds] []
+      ⊢ ∀n. i8_to_int (int_to_i8 n) =
+            if i8_min ≤ n ∧ n ≤ i8_max then n else i8_to_int (int_to_i8 n)
+   
    [index_update_diff]  Theorem
       
       ⊢ ∀ls i j y. 0 ≤ i ⇒ i < len ls ⇒ index i (update ls i y) = y
@@ -1723,6 +1776,14 @@ sig
           ∃z. isize_sub x y = Return z ∧
               isize_to_int z = isize_to_int x − isize_to_int y
    
+   [isize_to_int_int_to_isize_unfold]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: usize_bounds, isize_to_int_int_to_isize, isize_bounds] []
+      ⊢ ∀n. isize_to_int (int_to_isize n) =
+            if i16_min ≤ n ∧ n ≤ i16_max then n
+            else isize_to_int (int_to_isize n)
+   
    [num2error_11]  Theorem
       
       ⊢ ∀r r'. r < 1 ⇒ r' < 1 ⇒ (num2error r = num2error r' ⇔ r = r')
@@ -1826,6 +1887,13 @@ sig
           ∃z. u128_sub x y = Return z ∧
               u128_to_int z = u128_to_int x − u128_to_int y
    
+   [u128_to_int_int_to_u128_unfold]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: usize_bounds, u128_to_int_int_to_u128, isize_bounds] []
+      ⊢ ∀n. u128_to_int (int_to_u128 n) =
+            if 0 ≤ n ∧ n ≤ u128_max then n else u128_to_int (int_to_u128 n)
+   
    [u16_add_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -1876,6 +1944,13 @@ sig
           ∃z. u16_sub x y = Return z ∧
               u16_to_int z = u16_to_int x − u16_to_int y
    
+   [u16_to_int_int_to_u16_unfold]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: usize_bounds, u16_to_int_int_to_u16, isize_bounds] []
+      ⊢ ∀n. u16_to_int (int_to_u16 n) =
+            if 0 ≤ n ∧ n ≤ u16_max then n else u16_to_int (int_to_u16 n)
+   
    [u32_add_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -1926,6 +2001,13 @@ sig
           ∃z. u32_sub x y = Return z ∧
               u32_to_int z = u32_to_int x − u32_to_int y
    
+   [u32_to_int_int_to_u32_unfold]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: usize_bounds, u32_to_int_int_to_u32, isize_bounds] []
+      ⊢ ∀n. u32_to_int (int_to_u32 n) =
+            if 0 ≤ n ∧ n ≤ u32_max then n else u32_to_int (int_to_u32 n)
+   
    [u64_add_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -1976,6 +2058,13 @@ sig
           ∃z. u64_sub x y = Return z ∧
               u64_to_int z = u64_to_int x − u64_to_int y
    
+   [u64_to_int_int_to_u64_unfold]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: usize_bounds, u64_to_int_int_to_u64, isize_bounds] []
+      ⊢ ∀n. u64_to_int (int_to_u64 n) =
+            if 0 ≤ n ∧ n ≤ u64_max then n else u64_to_int (int_to_u64 n)
+   
    [u8_add_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -2026,6 +2115,13 @@ sig
           ∃z. u8_sub x y = Return z ∧
               u8_to_int z = u8_to_int x − u8_to_int y
    
+   [u8_to_int_int_to_u8_unfold]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: usize_bounds, u8_to_int_int_to_u8, isize_bounds] []
+      ⊢ ∀n. u8_to_int (int_to_u8 n) =
+            if 0 ≤ n ∧ n ≤ u8_max then n else u8_to_int (int_to_u8 n)
+   
    [update_len]  Theorem
       
       ⊢ ∀ls i y. len (update ls i y) = len ls
@@ -2090,6 +2186,14 @@ sig
           ∃z. usize_sub x y = Return z ∧
               usize_to_int z = usize_to_int x − usize_to_int y
    
+   [usize_to_int_int_to_usize_unfold]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: usize_bounds, usize_to_int_int_to_usize, isize_bounds] []
+      ⊢ ∀n. usize_to_int (int_to_usize n) =
+            if 0 ≤ n ∧ n ≤ u16_max then n
+            else usize_to_int (int_to_usize n)
+   
    [vec_insert_back_spec]  Theorem
       
       [oracles: DISK_THM]
diff --git a/backends/hol4/testHashmapScript.sml b/backends/hol4/testHashmapScript.sml
index 0e16ead3..79026376 100644
--- a/backends/hol4/testHashmapScript.sml
+++ b/backends/hol4/testHashmapScript.sml
@@ -1,4 +1,3 @@
-open HolKernel boolLib bossLib Parse
 open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
 
 open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory