summaryrefslogtreecommitdiff
path: root/backends/hol4
diff options
context:
space:
mode:
authorSon Ho2023-01-23 23:41:20 +0100
committerSon HO2023-06-04 21:54:38 +0200
commit6a68fb13036c0efa4028df3be499fc2159681c94 (patch)
tree74ef4b3082e4a71e146b24b394f5d4882c4ce8a0 /backends/hol4
parent41cfff628a12bcdc07861db029f54dac74b39853 (diff)
Make good progress on Primitives.sml
Diffstat (limited to 'backends/hol4')
-rw-r--r--backends/hol4/Primitives.sml1021
1 files changed, 997 insertions, 24 deletions
diff --git a/backends/hol4/Primitives.sml b/backends/hol4/Primitives.sml
index 4d77b84a..be384012 100644
--- a/backends/hol4/Primitives.sml
+++ b/backends/hol4/Primitives.sml
@@ -165,6 +165,21 @@ val u64_to_int_bounds = new_axiom ("u64_to_int_bounds",
val u128_to_int_bounds = new_axiom ("u128_to_int_bounds",
“!n. 0 <= u128_to_int n /\ u128_to_int n <= u128_max”)
+val all_to_int_bounds_lemmas = [
+ isize_to_int_bounds,
+ i8_to_int_bounds,
+ i16_to_int_bounds,
+ i32_to_int_bounds,
+ i64_to_int_bounds,
+ i128_to_int_bounds,
+ usize_to_int_bounds,
+ u8_to_int_bounds,
+ u16_to_int_bounds,
+ u32_to_int_bounds,
+ u64_to_int_bounds,
+ u128_to_int_bounds
+]
+
(* Conversion to and from int.
Note that for isize and usize, we write the lemmas in such a way that the
@@ -295,6 +310,22 @@ val mk_u128_def = Define
if 0 <= n /\ n <= u128_max then Return (int_to_u128 n)
else Fail Failure’
+val all_mk_int_defs = [
+ mk_isize_def,
+ mk_i8_def,
+ mk_i16_def,
+ mk_i32_def,
+ mk_i64_def,
+ mk_i128_def,
+ mk_usize_def,
+ mk_u8_def,
+ mk_u16_def,
+ mk_u32_def,
+ mk_u64_def,
+ mk_u128_def
+]
+
+
val isize_add_def = Define ‘isize_add x y = mk_isize ((isize_to_int x) + (isize_to_int y))’
val i8_add_def = Define ‘i8_add x y = mk_i8 ((i8_to_int x) + (i8_to_int y))’
val i16_add_def = Define ‘i16_add x y = mk_i16 ((i16_to_int x) + (i16_to_int y))’
@@ -308,6 +339,21 @@ val u32_add_def = Define ‘u32_add x y = mk_u32 ((u32_to_int x) + (u32_to_i
val u64_add_def = Define ‘u64_add x y = mk_u64 ((u64_to_int x) + (u64_to_int y))’
val u128_add_def = Define ‘u128_add x y = mk_u128 ((u128_to_int x) + (u128_to_int y))’
+val all_add_defs = [
+ isize_add_def,
+ i8_add_def,
+ i16_add_def,
+ i32_add_def,
+ i64_add_def,
+ i128_add_def,
+ usize_add_def,
+ u8_add_def,
+ u16_add_def,
+ u32_add_def,
+ u64_add_def,
+ u128_add_def
+]
+
val isize_sub_def = Define ‘isize_sub x y = mk_isize ((isize_to_int x) - (isize_to_int y))’
val i8_sub_def = Define ‘i8_sub x y = mk_i8 ((i8_to_int x) - (i8_to_int y))’
val i16_sub_def = Define ‘i16_sub x y = mk_i16 ((i16_to_int x) - (i16_to_int y))’
@@ -321,6 +367,21 @@ val u32_sub_def = Define ‘u32_sub x y = mk_u32 ((u32_to_int x) - (u32_to_i
val u64_sub_def = Define ‘u64_sub x y = mk_u64 ((u64_to_int x) - (u64_to_int y))’
val u128_sub_def = Define ‘u128_sub x y = mk_u128 ((u128_to_int x) - (u128_to_int y))’
+val all_sub_defs = [
+ isize_sub_def,
+ i8_sub_def,
+ i16_sub_def,
+ i32_sub_def,
+ i64_sub_def,
+ i128_sub_def,
+ usize_sub_def,
+ u8_sub_def,
+ u16_sub_def,
+ u32_sub_def,
+ u64_sub_def,
+ u128_sub_def
+]
+
val isize_mul_def = Define ‘isize_mul x y = mk_isize ((isize_to_int x) * (isize_to_int y))’
val i8_mul_def = Define ‘i8_mul x y = mk_i8 ((i8_to_int x) * (i8_to_int y))’
val i16_mul_def = Define ‘i16_mul x y = mk_i16 ((i16_to_int x) * (i16_to_int y))’
@@ -334,6 +395,21 @@ val u32_mul_def = Define ‘u32_mul x y = mk_u32 ((u32_to_int x) * (u32_to_i
val u64_mul_def = Define ‘u64_mul x y = mk_u64 ((u64_to_int x) * (u64_to_int y))’
val u128_mul_def = Define ‘u128_mul x y = mk_u128 ((u128_to_int x) * (u128_to_int y))’
+val all_mul_defs = [
+ isize_mul_def,
+ i8_mul_def,
+ i16_mul_def,
+ i32_mul_def,
+ i64_mul_def,
+ i128_mul_def,
+ usize_mul_def,
+ u8_mul_def,
+ u16_mul_def,
+ u32_mul_def,
+ u64_mul_def,
+ u128_mul_def
+]
+
val isize_div_def = Define ‘isize_div x y =
if isize_to_int y = 0 then Fail Failure else mk_isize ((isize_to_int x) / (isize_to_int y))’
val i8_div_def = Define ‘i8_div x y =
@@ -359,27 +435,924 @@ val u64_div_def = Define ‘u64_div x y =
val u128_div_def = Define ‘u128_div x y =
if u128_to_int y = 0 then Fail Failure else mk_u128 ((u128_to_int x) / (u128_to_int y))’
-val isize_mod_def = Define ‘isize_mod x y =
- if isize_to_int y = 0 then Fail Failure else mk_isize ((isize_to_int x) % (isize_to_int y))’
-val i8_mod_def = Define ‘i8_mod x y =
- if i8_to_int y = 0 then Fail Failure else mk_i8 ((i8_to_int x) % (i8_to_int y))’
-val i16_mod_def = Define ‘i16_mod x y =
- if i16_to_int y = 0 then Fail Failure else mk_i16 ((i16_to_int x) % (i16_to_int y))’
-val i32_mod_def = Define ‘i32_mod x y =
- if i32_to_int y = 0 then Fail Failure else mk_i32 ((i32_to_int x) % (i32_to_int y))’
-val i64_mod_def = Define ‘i64_mod x y =
- if i64_to_int y = 0 then Fail Failure else mk_i64 ((i64_to_int x) % (i64_to_int y))’
-val i128_mod_def = Define ‘i128_mod x y =
- if i128_to_int y = 0 then Fail Failure else mk_i128 ((i128_to_int x) % (i128_to_int y))’
-val usize_mod_def = Define ‘usize_mod x y =
- if usize_to_int y = 0 then Fail Failure else mk_usize ((usize_to_int x) % (usize_to_int y))’
-val u8_mod_def = Define ‘u8_mod x y =
- if u8_to_int y = 0 then Fail Failure else mk_u8 ((u8_to_int x) % (u8_to_int y))’
-val u16_mod_def = Define ‘u16_mod x y =
- if u16_to_int y = 0 then Fail Failure else mk_u16 ((u16_to_int x) % (u16_to_int y))’
-val u32_mod_def = Define ‘u32_mod x y =
- if u32_to_int y = 0 then Fail Failure else mk_u32 ((u32_to_int x) % (u32_to_int y))’
-val u64_mod_def = Define ‘u64_mod x y =
- if u64_to_int y = 0 then Fail Failure else mk_u64 ((u64_to_int x) % (u64_to_int y))’
-val u128_mod_def = Define ‘u128_mod x y =
- if u128_to_int y = 0 then Fail Failure else mk_u128 ((u128_to_int x) % (u128_to_int y))’
+val all_div_defs = [
+ isize_div_def,
+ i8_div_def,
+ i16_div_def,
+ i32_div_def,
+ i64_div_def,
+ i128_div_def,
+ usize_div_def,
+ u8_div_def,
+ u16_div_def,
+ u32_div_def,
+ u64_div_def,
+ u128_div_def
+]
+
+(* The remainder operation is not a modulo.
+
+ In Rust, the remainder has the sign of the dividend.
+ In HOL4, it has the sign of the divisor.
+ *)
+val int_rem_def = Define ‘int_rem (x : int) (y : int) : int =
+ if (x >= 0 /\ y >= 0) \/ (x < 0 /\ y < 0) then x % y else -(x % y)’
+
+(* Checking consistency with Rust *)
+val _ = prove(“int_rem 1 2 = 1”, EVAL_TAC)
+val _ = prove(“int_rem (-1) 2 = -1”, EVAL_TAC)
+val _ = prove(“int_rem 1 (-2) = 1”, EVAL_TAC)
+val _ = prove(“int_rem (-1) (-2) = -1”, EVAL_TAC)
+
+val isize_rem_def = Define ‘isize_rem x y =
+ if isize_to_int y = 0 then Fail Failure else mk_isize (int_rem (isize_to_int x) (isize_to_int y))’
+val i8_rem_def = Define ‘i8_rem x y =
+ if i8_to_int y = 0 then Fail Failure else mk_i8 (int_rem (i8_to_int x) (i8_to_int y))’
+val i16_rem_def = Define ‘i16_rem x y =
+ if i16_to_int y = 0 then Fail Failure else mk_i16 (int_rem (i16_to_int x) (i16_to_int y))’
+val i32_rem_def = Define ‘i32_rem x y =
+ if i32_to_int y = 0 then Fail Failure else mk_i32 (int_rem (i32_to_int x) (i32_to_int y))’
+val i64_rem_def = Define ‘i64_rem x y =
+ if i64_to_int y = 0 then Fail Failure else mk_i64 (int_rem (i64_to_int x) (i64_to_int y))’
+val i128_rem_def = Define ‘i128_rem x y =
+ if i128_to_int y = 0 then Fail Failure else mk_i128 (int_rem (i128_to_int x) (i128_to_int y))’
+val usize_rem_def = Define ‘usize_rem x y =
+ if usize_to_int y = 0 then Fail Failure else mk_usize (int_rem (usize_to_int x) (usize_to_int y))’
+val u8_rem_def = Define ‘u8_rem x y =
+ if u8_to_int y = 0 then Fail Failure else mk_u8 (int_rem (u8_to_int x) (u8_to_int y))’
+val u16_rem_def = Define ‘u16_rem x y =
+ if u16_to_int y = 0 then Fail Failure else mk_u16 (int_rem (u16_to_int x) (u16_to_int y))’
+val u32_rem_def = Define ‘u32_rem x y =
+ if u32_to_int y = 0 then Fail Failure else mk_u32 (int_rem (u32_to_int x) (u32_to_int y))’
+val u64_rem_def = Define ‘u64_rem x y =
+ if u64_to_int y = 0 then Fail Failure else mk_u64 (int_rem (u64_to_int x) (u64_to_int y))’
+val u128_rem_def = Define ‘u128_rem x y =
+ if u128_to_int y = 0 then Fail Failure else mk_u128 (int_rem (u128_to_int x) (u128_to_int y))’
+
+val all_rem_defs = [
+ isize_rem_def,
+ i8_rem_def,
+ i16_rem_def,
+ i32_rem_def,
+ i64_rem_def,
+ i128_rem_def,
+ usize_rem_def,
+ u8_rem_def,
+ u16_rem_def,
+ u32_rem_def,
+ u64_rem_def,
+ u128_rem_def
+]
+
+(* Ignore a theorem.
+
+ To be used in conjunction with {!pop_assum} for instance.
+ *)
+fun IGNORE_TAC (_ : thm) : tactic = ALL_TAC
+
+val POP_IGNORE_TAC = POP_ASSUM IGNORE_TAC
+
+(* TODO: we need a better library of lemmas about arithmetic *)
+
+(* TODO: add those as rewriting tactics by default *)
+val NOT_LE_EQ_GT = store_thm("NOT_LE_EQ_GT", “!(x y: int). ~(x <= y) <=> x > y”, COOPER_TAC)
+val NOT_LT_EQ_GE = store_thm("NOT_LT_EQ_GE", “!(x y: int). ~(x < y) <=> x >= y”, COOPER_TAC)
+val NOT_GE_EQ_LT = store_thm("NOT_GE_EQ_LT", “!(x y: int). ~(x >= y) <=> x < y”, COOPER_TAC)
+val NOT_GT_EQ_LE = store_thm("NOT_GT_EQ_LE", “!(x y: int). ~(x > y) <=> x <= y”, COOPER_TAC)
+
+Theorem POS_MUL_POS_IS_POS:
+ !(x y : int). 0 <= x ==> 0 <= y ==> 0 <= x * y
+Proof
+ rpt strip_tac >>
+ sg ‘0 <= &(Num x) * &(Num y)’ >- (rw [INT_MUL_CALCULATE] >> COOPER_TAC) >>
+ sg ‘&(Num x) = x’ >- (irule EQ_SYM >> rw [INT_OF_NUM] >> COOPER_TAC) >>
+ sg ‘&(Num y) = y’ >- (irule EQ_SYM >> rw [INT_OF_NUM] >> COOPER_TAC) >>
+ metis_tac[]
+QED
+
+val GE_EQ_LE = store_thm("GE_EQ_LE", “!(x y : int). x >= y <=> y <= x”, COOPER_TAC)
+val LE_EQ_GE = store_thm("LE_EQ_GE", “!(x y : int). x <= y <=> y >= x”, COOPER_TAC)
+val GT_EQ_LT = store_thm("GT_EQ_LT", “!(x y : int). x > y <=> y < x”, COOPER_TAC)
+val LT_EQ_GT = store_thm("LT_EQ_GT", “!(x y : int). x < y <=> y > x”, COOPER_TAC)
+
+Theorem POS_DIV_POS_IS_POS:
+ !(x y : int). 0 <= x ==> 0 < y ==> 0 <= x / y
+Proof
+ rpt strip_tac >>
+ rw [LE_EQ_GE] >>
+ sg ‘y <> 0’ >- COOPER_TAC >>
+ qspecl_then [‘\x. x >= 0’, ‘x’, ‘y’] ASSUME_TAC INT_DIV_FORALL_P >>
+ fs [] >> POP_IGNORE_TAC >> rw [] >- COOPER_TAC >>
+ fs [NOT_LT_EQ_GE] >>
+ (* Proof by contradiction: assume k < 0 *)
+ spose_not_then ASSUME_TAC >>
+ fs [NOT_GE_EQ_LT] >>
+ sg ‘k * y = (k + 1) * y + - y’ >- (fs [INT_RDISTRIB] >> COOPER_TAC) >>
+ sg ‘0 <= (-(k + 1)) * y’ >- (irule POS_MUL_POS_IS_POS >> COOPER_TAC) >>
+ COOPER_TAC
+QED
+
+Theorem POS_DIV_POS_LE:
+ !(x y d : int). 0 <= x ==> 0 <= y ==> 0 < d ==> x <= y ==> x / d <= y / d
+Proof
+ rpt strip_tac >>
+ sg ‘d <> 0’ >- COOPER_TAC >>
+ qspecl_then [‘\k. k = x / d’, ‘x’, ‘d’] ASSUME_TAC INT_DIV_P >>
+ qspecl_then [‘\k. k = y / d’, ‘y’, ‘d’] ASSUME_TAC INT_DIV_P >>
+ rfs [NOT_LT_EQ_GE] >> TRY COOPER_TAC >>
+ sg ‘y = (x / d) * d + (r' + y - x)’ >- COOPER_TAC >>
+ qspecl_then [‘(x / d) * d’, ‘r' + y - x’, ‘d’] ASSUME_TAC INT_ADD_DIV >>
+ rfs [] >>
+ Cases_on ‘x = y’ >- fs [] >>
+ sg ‘r' + y ≠ x’ >- COOPER_TAC >> fs [] >>
+ sg ‘((x / d) * d) / d = x / d’ >- (irule INT_DIV_RMUL >> COOPER_TAC) >>
+ fs [] >>
+ sg ‘0 <= (r' + y − x) / d’ >- (irule POS_DIV_POS_IS_POS >> COOPER_TAC) >>
+ metis_tac [INT_LE_ADDR]
+QED
+
+Theorem POS_DIV_POS_LE_INIT:
+ !(x y : int). 0 <= x ==> 0 < y ==> x / y <= x
+Proof
+ rpt strip_tac >>
+ sg ‘y <> 0’ >- COOPER_TAC >>
+ qspecl_then [‘\k. k = x / y’, ‘x’, ‘y’] ASSUME_TAC INT_DIV_P >>
+ rfs [NOT_LT_EQ_GE] >- COOPER_TAC >>
+ sg ‘y = (y - 1) + 1’ >- rw [] >>
+ sg ‘x = x / y + ((x / y) * (y - 1) + r)’ >-(
+ qspecl_then [‘1’, ‘y-1’, ‘x / y’] ASSUME_TAC INT_LDISTRIB >>
+ rfs [] >>
+ COOPER_TAC
+ ) >>
+ sg ‘!a b c. 0 <= c ==> a = b + c ==> b <= a’ >- (COOPER_TAC) >>
+ pop_assum irule >>
+ exists_tac “x / y * (y − 1) + r” >>
+ sg ‘0 <= x / y’ >- (irule POS_DIV_POS_IS_POS >> COOPER_TAC) >>
+ sg ‘0 <= (x / y) * (y - 1)’ >- (irule POS_MUL_POS_IS_POS >> COOPER_TAC) >>
+ COOPER_TAC
+QED
+
+Theorem POS_MOD_POS_IS_POS:
+ !(x y : int). 0 <= x ==> 0 < y ==> 0 <= x % y
+Proof
+ rpt strip_tac >>
+ sg ‘y <> 0’ >- COOPER_TAC >>
+ imp_res_tac INT_DIVISION >>
+ first_x_assum (qspec_then ‘x’ assume_tac) >>
+ first_x_assum (qspec_then ‘x’ assume_tac) >>
+ sg ‘~(y < 0)’ >- COOPER_TAC >> fs []
+QED
+
+Theorem POS_MOD_POS_LE_INIT:
+ !(x y : int). 0 <= x ==> 0 < y ==> x % y <= x
+Proof
+ rpt strip_tac >>
+ sg ‘y <> 0’ >- COOPER_TAC >>
+ imp_res_tac INT_DIVISION >>
+ first_x_assum (qspec_then ‘x’ assume_tac) >>
+ first_x_assum (qspec_then ‘x’ assume_tac) >>
+ sg ‘~(y < 0)’ >- COOPER_TAC >> fs [] >>
+ sg ‘0 <= x % y’ >- (irule POS_MOD_POS_IS_POS >> COOPER_TAC) >>
+ sg ‘0 <= x / y’ >- (irule POS_DIV_POS_IS_POS >> COOPER_TAC) >>
+ sg ‘0 <= (x / y) * y’ >- (irule POS_MUL_POS_IS_POS >> COOPER_TAC) >>
+ COOPER_TAC
+QED
+
+(*
+val (asms,g) = top_goal ()
+*)
+
+fun prove_arith_op_eq (asms, g) =
+ let
+ val (_, t) = (dest_exists o snd o strip_imp o snd o strip_forall) g;
+ val (x_to_int, y_to_int) =
+ case (snd o strip_comb o rhs o snd o dest_conj) t of
+ [x, y] => (x,y)
+ | _ => failwith "Unexpected"
+ val x = (snd o dest_comb) x_to_int;
+ val y = (snd o dest_comb) y_to_int;
+ fun inst_first_lem arg lems =
+ MAP_FIRST (fn th => (ASSUME_TAC (SPEC arg th) handle HOL_ERR _ => FAIL_TAC "")) lems;
+ in
+ (rpt gen_tac >>
+ rpt DISCH_TAC >>
+ ASSUME_TAC usize_bounds >> (* Only useful for usize of course *)
+ ASSUME_TAC isize_bounds >> (* Only useful for isize of course *)
+ rw (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]) >>
+ fs (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]) >>
+ inst_first_lem x all_to_int_bounds_lemmas >>
+ inst_first_lem y all_to_int_bounds_lemmas >>
+ gs [NOT_LE_EQ_GT, NOT_LT_EQ_GE, NOT_GE_EQ_LT, NOT_GT_EQ_LE, GE_EQ_LE, GT_EQ_LT] >>
+ TRY COOPER_TAC >>
+ FIRST [
+ (* For division *)
+ qspecl_then [‘^x_to_int’, ‘^y_to_int’] ASSUME_TAC POS_DIV_POS_IS_POS >>
+ qspecl_then [‘^x_to_int’, ‘^y_to_int’] ASSUME_TAC POS_DIV_POS_LE_INIT >>
+ COOPER_TAC,
+ (* For remainder *)
+ dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC all_conversion_id_lemmas >> fs [] >>
+ qspecl_then [‘^x_to_int’, ‘^y_to_int’] ASSUME_TAC POS_MOD_POS_IS_POS >>
+ qspecl_then [‘^x_to_int’, ‘^y_to_int’] ASSUME_TAC POS_MOD_POS_LE_INIT >>
+ COOPER_TAC,
+ dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC all_conversion_id_lemmas >> fs []
+ ]) (asms, g)
+ end
+
+Theorem U8_ADD_EQ:
+ !x y.
+ u8_to_int x + u8_to_int y <= u8_max ==>
+ ?z. u8_add x y = Return z /\ u8_to_int z = u8_to_int x + u8_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem U16_ADD_EQ:
+ !x y.
+ u16_to_int x + u16_to_int y <= u16_max ==>
+ ?z. u16_add x y = Return z /\ u16_to_int z = u16_to_int x + u16_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem U32_ADD_EQ:
+ !x y.
+ u32_to_int x + u32_to_int y <= u32_max ==>
+ ?z. u32_add x y = Return z /\ u32_to_int z = u32_to_int x + u32_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem U64_ADD_EQ:
+ !x y.
+ u64_to_int x + u64_to_int y <= u64_max ==>
+ ?z. u64_add x y = Return z /\ u64_to_int z = u64_to_int x + u64_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem U128_ADD_EQ:
+ !x y.
+ u128_to_int x + u128_to_int y <= u128_max ==>
+ ?z. u128_add x y = Return z /\ u128_to_int z = u128_to_int x + u128_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem USIZE_ADD_EQ:
+ !x y.
+ (usize_to_int x + usize_to_int y <= u16_max) \/ (usize_to_int x + usize_to_int y <= usize_max) ==>
+ ?z. usize_add x y = Return z /\ usize_to_int z = usize_to_int x + usize_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I8_ADD_EQ:
+ !x y.
+ i8_min <= i8_to_int x + i8_to_int y ==>
+ i8_to_int x + i8_to_int y <= i8_max ==>
+ ?z. i8_add x y = Return z /\ i8_to_int z = i8_to_int x + i8_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I16_ADD_EQ:
+ !x y.
+ i16_min <= i16_to_int x + i16_to_int y ==>
+ i16_to_int x + i16_to_int y <= i16_max ==>
+ ?z. i16_add x y = Return z /\ i16_to_int z = i16_to_int x + i16_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I32_ADD_EQ:
+ !x y.
+ i32_min <= i32_to_int x + i32_to_int y ==>
+ i32_to_int x + i32_to_int y <= i32_max ==>
+ ?z. i32_add x y = Return z /\ i32_to_int z = i32_to_int x + i32_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I64_ADD_EQ:
+ !x y.
+ i64_min <= i64_to_int x + i64_to_int y ==>
+ i64_to_int x + i64_to_int y <= i64_max ==>
+ ?z. i64_add x y = Return z /\ i64_to_int z = i64_to_int x + i64_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I128_ADD_EQ:
+ !x y.
+ i128_min <= i128_to_int x + i128_to_int y ==>
+ i128_to_int x + i128_to_int y <= i128_max ==>
+ ?z. i128_add x y = Return z /\ i128_to_int z = i128_to_int x + i128_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem ISIZE_ADD_EQ:
+ !x y.
+ (i16_min <= isize_to_int x + isize_to_int y \/ isize_min <= isize_to_int x + isize_to_int y) ==>
+ (isize_to_int x + isize_to_int y <= i16_max \/ isize_to_int x + isize_to_int y <= isize_max) ==>
+ ?z. isize_add x y = Return z /\ isize_to_int z = isize_to_int x + isize_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+val all_add_eqs = [
+ ISIZE_ADD_EQ,
+ I8_ADD_EQ,
+ I16_ADD_EQ,
+ I32_ADD_EQ,
+ I64_ADD_EQ,
+ I128_ADD_EQ,
+ USIZE_ADD_EQ,
+ U8_ADD_EQ,
+ U16_ADD_EQ,
+ U32_ADD_EQ,
+ U64_ADD_EQ,
+ U128_ADD_EQ
+]
+
+Theorem U8_SUB_EQ:
+ !x y.
+ 0 <= u8_to_int x - u8_to_int y ==>
+ ?z. u8_sub x y = Return z /\ u8_to_int z = u8_to_int x - u8_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem U16_SUB_EQ:
+ !x y.
+ 0 <= u16_to_int x - u16_to_int y ==>
+ ?z. u16_sub x y = Return z /\ u16_to_int z = u16_to_int x - u16_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem U32_SUB_EQ:
+ !x y.
+ 0 <= u32_to_int x - u32_to_int y ==>
+ ?z. u32_sub x y = Return z /\ u32_to_int z = u32_to_int x - u32_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem U64_SUB_EQ:
+ !x y.
+ 0 <= u64_to_int x - u64_to_int y ==>
+ ?z. u64_sub x y = Return z /\ u64_to_int z = u64_to_int x - u64_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem U128_SUB_EQ:
+ !x y.
+ 0 <= u128_to_int x - u128_to_int y ==>
+ ?z. u128_sub x y = Return z /\ u128_to_int z = u128_to_int x - u128_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem USIZE_SUB_EQ:
+ !x y.
+ 0 <= usize_to_int x - usize_to_int y ==>
+ ?z. usize_sub x y = Return z /\ usize_to_int z = usize_to_int x - usize_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I8_SUB_EQ:
+ !x y.
+ i8_min <= i8_to_int x - i8_to_int y ==>
+ i8_to_int x - i8_to_int y <= i8_max ==>
+ ?z. i8_sub x y = Return z /\ i8_to_int z = i8_to_int x - i8_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I16_SUB_EQ:
+ !x y.
+ i16_min <= i16_to_int x - i16_to_int y ==>
+ i16_to_int x - i16_to_int y <= i16_max ==>
+ ?z. i16_sub x y = Return z /\ i16_to_int z = i16_to_int x - i16_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I32_SUB_EQ:
+ !x y.
+ i32_min <= i32_to_int x - i32_to_int y ==>
+ i32_to_int x - i32_to_int y <= i32_max ==>
+ ?z. i32_sub x y = Return z /\ i32_to_int z = i32_to_int x - i32_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I64_SUB_EQ:
+ !x y.
+ i64_min <= i64_to_int x - i64_to_int y ==>
+ i64_to_int x - i64_to_int y <= i64_max ==>
+ ?z. i64_sub x y = Return z /\ i64_to_int z = i64_to_int x - i64_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I128_SUB_EQ:
+ !x y.
+ i128_min <= i128_to_int x - i128_to_int y ==>
+ i128_to_int x - i128_to_int y <= i128_max ==>
+ ?z. i128_sub x y = Return z /\ i128_to_int z = i128_to_int x - i128_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem ISIZE_SUB_EQ:
+ !x y.
+ (i16_min <= isize_to_int x - isize_to_int y \/ isize_min <= isize_to_int x - isize_to_int y) ==>
+ (isize_to_int x - isize_to_int y <= i16_max \/ isize_to_int x - isize_to_int y <= isize_max) ==>
+ ?z. isize_sub x y = Return z /\ isize_to_int z = isize_to_int x - isize_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+val all_sub_eqs = [
+ ISIZE_SUB_EQ,
+ I8_SUB_EQ,
+ I16_SUB_EQ,
+ I32_SUB_EQ,
+ I64_SUB_EQ,
+ I128_SUB_EQ,
+ USIZE_SUB_EQ,
+ U8_SUB_EQ,
+ U16_SUB_EQ,
+ U32_SUB_EQ,
+ U64_SUB_EQ,
+ U128_SUB_EQ
+]
+
+Theorem U8_MUL_EQ:
+ !x y.
+ u8_to_int x * u8_to_int y <= u8_max ==>
+ ?z. u8_mul x y = Return z /\ u8_to_int z = u8_to_int x * u8_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem U16_MUL_EQ:
+ !x y.
+ u16_to_int x * u16_to_int y <= u16_max ==>
+ ?z. u16_mul x y = Return z /\ u16_to_int z = u16_to_int x * u16_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem U32_MUL_EQ:
+ !x y.
+ u32_to_int x * u32_to_int y <= u32_max ==>
+ ?z. u32_mul x y = Return z /\ u32_to_int z = u32_to_int x * u32_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem U64_MUL_EQ:
+ !x y.
+ u64_to_int x * u64_to_int y <= u64_max ==>
+ ?z. u64_mul x y = Return z /\ u64_to_int z = u64_to_int x * u64_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem U128_MUL_EQ:
+ !x y.
+ u128_to_int x * u128_to_int y <= u128_max ==>
+ ?z. u128_mul x y = Return z /\ u128_to_int z = u128_to_int x * u128_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem USIZE_MUL_EQ:
+ !x y.
+ (usize_to_int x * usize_to_int y <= u16_max) \/ (usize_to_int x * usize_to_int y <= usize_max) ==>
+ ?z. usize_mul x y = Return z /\ usize_to_int z = usize_to_int x * usize_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I8_MUL_EQ:
+ !x y.
+ i8_min <= i8_to_int x * i8_to_int y ==>
+ i8_to_int x * i8_to_int y <= i8_max ==>
+ ?z. i8_mul x y = Return z /\ i8_to_int z = i8_to_int x * i8_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I16_MUL_EQ:
+ !x y.
+ i16_min <= i16_to_int x * i16_to_int y ==>
+ i16_to_int x * i16_to_int y <= i16_max ==>
+ ?z. i16_mul x y = Return z /\ i16_to_int z = i16_to_int x * i16_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I32_MUL_EQ:
+ !x y.
+ i32_min <= i32_to_int x * i32_to_int y ==>
+ i32_to_int x * i32_to_int y <= i32_max ==>
+ ?z. i32_mul x y = Return z /\ i32_to_int z = i32_to_int x * i32_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I64_MUL_EQ:
+ !x y.
+ i64_min <= i64_to_int x * i64_to_int y ==>
+ i64_to_int x * i64_to_int y <= i64_max ==>
+ ?z. i64_mul x y = Return z /\ i64_to_int z = i64_to_int x * i64_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I128_MUL_EQ:
+ !x y.
+ i128_min <= i128_to_int x * i128_to_int y ==>
+ i128_to_int x * i128_to_int y <= i128_max ==>
+ ?z. i128_mul x y = Return z /\ i128_to_int z = i128_to_int x * i128_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem ISIZE_MUL_EQ:
+ !x y.
+ (i16_min <= isize_to_int x * isize_to_int y \/ isize_min <= isize_to_int x * isize_to_int y) ==>
+ (isize_to_int x * isize_to_int y <= i16_max \/ isize_to_int x * isize_to_int y <= isize_max) ==>
+ ?z. isize_mul x y = Return z /\ isize_to_int z = isize_to_int x * isize_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+val all_mul_eqs = [
+ ISIZE_MUL_EQ,
+ I8_MUL_EQ,
+ I16_MUL_EQ,
+ I32_MUL_EQ,
+ I64_MUL_EQ,
+ I128_MUL_EQ,
+ USIZE_MUL_EQ,
+ U8_MUL_EQ,
+ U16_MUL_EQ,
+ U32_MUL_EQ,
+ U64_MUL_EQ,
+ U128_MUL_EQ
+]
+
+Theorem U8_DIV_EQ:
+ !x y.
+ u8_to_int y <> 0 ==>
+ ?z. u8_div x y = Return z /\ u8_to_int z = u8_to_int x / u8_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem U16_DIV_EQ:
+ !x y.
+ u16_to_int y <> 0 ==>
+ ?z. u16_div x y = Return z /\ u16_to_int z = u16_to_int x / u16_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem U32_DIV_EQ:
+ !x y.
+ u32_to_int y <> 0 ==>
+ ?z. u32_div x y = Return z /\ u32_to_int z = u32_to_int x / u32_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem U64_DIV_EQ:
+ !x y.
+ u64_to_int y <> 0 ==>
+ ?z. u64_div x y = Return z /\ u64_to_int z = u64_to_int x / u64_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem U128_DIV_EQ:
+ !x y.
+ u128_to_int y <> 0 ==>
+ ?z. u128_div x y = Return z /\ u128_to_int z = u128_to_int x / u128_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem USIZE_DIV_EQ:
+ !x y.
+ usize_to_int y <> 0 ==>
+ ?z. usize_div x y = Return z /\ usize_to_int z = usize_to_int x / usize_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I8_DIV_EQ:
+ !x y.
+ i8_to_int y <> 0 ==>
+ i8_min <= i8_to_int x / i8_to_int y ==>
+ i8_to_int x / i8_to_int y <= i8_max ==>
+ ?z. i8_div x y = Return z /\ i8_to_int z = i8_to_int x / i8_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I16_DIV_EQ:
+ !x y.
+ i16_to_int y <> 0 ==>
+ i16_min <= i16_to_int x / i16_to_int y ==>
+ i16_to_int x / i16_to_int y <= i16_max ==>
+ ?z. i16_div x y = Return z /\ i16_to_int z = i16_to_int x / i16_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I32_DIV_EQ:
+ !x y.
+ i32_to_int y <> 0 ==>
+ i32_min <= i32_to_int x / i32_to_int y ==>
+ i32_to_int x / i32_to_int y <= i32_max ==>
+ ?z. i32_div x y = Return z /\ i32_to_int z = i32_to_int x / i32_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I64_DIV_EQ:
+ !x y.
+ i64_to_int y <> 0 ==>
+ i64_min <= i64_to_int x / i64_to_int y ==>
+ i64_to_int x / i64_to_int y <= i64_max ==>
+ ?z. i64_div x y = Return z /\ i64_to_int z = i64_to_int x / i64_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I128_DIV_EQ:
+ !x y.
+ i128_to_int y <> 0 ==>
+ i128_min <= i128_to_int x / i128_to_int y ==>
+ i128_to_int x / i128_to_int y <= i128_max ==>
+ ?z. i128_div x y = Return z /\ i128_to_int z = i128_to_int x / i128_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem ISIZE_DIV_EQ:
+ !x y.
+ isize_to_int y <> 0 ==>
+ (i16_min <= isize_to_int x / isize_to_int y \/ isize_min <= isize_to_int x / isize_to_int y) ==>
+ (isize_to_int x / isize_to_int y <= i16_max \/ isize_to_int x / isize_to_int y <= isize_max) ==>
+ ?z. isize_div x y = Return z /\ isize_to_int z = isize_to_int x / isize_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+val all_div_eqs = [
+ ISIZE_DIV_EQ,
+ I8_DIV_EQ,
+ I16_DIV_EQ,
+ I32_DIV_EQ,
+ I64_DIV_EQ,
+ I128_DIV_EQ,
+ USIZE_DIV_EQ,
+ U8_DIV_EQ,
+ U16_DIV_EQ,
+ U32_DIV_EQ,
+ U64_DIV_EQ,
+ U128_DIV_EQ
+]
+
+Theorem U8_REM_EQ:
+ !x y.
+ u8_to_int y <> 0 ==>
+ ?z. u8_rem x y = Return z /\ u8_to_int z = int_rem (u8_to_int x) (u8_to_int y)
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem U16_REM_EQ:
+ !x y.
+ u16_to_int y <> 0 ==>
+ ?z. u16_rem x y = Return z /\ u16_to_int z = int_rem (u16_to_int x) (u16_to_int y)
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem U32_REM_EQ:
+ !x y.
+ u32_to_int y <> 0 ==>
+ ?z. u32_rem x y = Return z /\ u32_to_int z = int_rem (u32_to_int x) (u32_to_int y)
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem U64_REM_EQ:
+ !x y.
+ u64_to_int y <> 0 ==>
+ ?z. u64_rem x y = Return z /\ u64_to_int z = int_rem (u64_to_int x) (u64_to_int y)
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem U128_REM_EQ:
+ !x y.
+ u128_to_int y <> 0 ==>
+ ?z. u128_rem x y = Return z /\ u128_to_int z = int_rem (u128_to_int x) (u128_to_int y)
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem USIZE_REM_EQ:
+ !x y.
+ usize_to_int y <> 0 ==>
+ ?z. usize_rem x y = Return z /\ usize_to_int z = int_rem (usize_to_int x) (usize_to_int y)
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I8_REM_EQ:
+ !x y.
+ i8_to_int y <> 0 ==>
+ i8_min <= int_rem (i8_to_int x) (i8_to_int y) ==>
+ int_rem (i8_to_int x) (i8_to_int y) <= i8_max ==>
+ ?z. i8_rem x y = Return z /\ i8_to_int z = int_rem (i8_to_int x) (i8_to_int y)
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I16_REM_EQ:
+ !x y.
+ i16_to_int y <> 0 ==>
+ i16_min <= int_rem (i16_to_int x) (i16_to_int y) ==>
+ int_rem (i16_to_int x) (i16_to_int y) <= i16_max ==>
+ ?z. i16_rem x y = Return z /\ i16_to_int z = int_rem (i16_to_int x) (i16_to_int y)
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I32_REM_EQ:
+ !x y.
+ i32_to_int y <> 0 ==>
+ i32_min <= int_rem (i32_to_int x) (i32_to_int y) ==>
+ int_rem (i32_to_int x) (i32_to_int y) <= i32_max ==>
+ ?z. i32_rem x y = Return z /\ i32_to_int z = int_rem (i32_to_int x) (i32_to_int y)
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I64_REM_EQ:
+ !x y.
+ i64_to_int y <> 0 ==>
+ i64_min <= int_rem (i64_to_int x) (i64_to_int y) ==>
+ int_rem (i64_to_int x) (i64_to_int y) <= i64_max ==>
+ ?z. i64_rem x y = Return z /\ i64_to_int z = int_rem (i64_to_int x) (i64_to_int y)
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I8_REM_EQ:
+ !x y.
+ i8_to_int y <> 0 ==>
+ i8_min <= int_rem (i8_to_int x) (i8_to_int y) ==>
+ int_rem (i8_to_int x) (i8_to_int y) <= i8_max ==>
+ ?z. i8_rem x y = Return z /\ i8_to_int z = int_rem (i8_to_int x) (i8_to_int y)
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I8_REM_EQ:
+ !x y.
+ i8_to_int y <> 0 ==>
+ i8_min <= int_rem (i8_to_int x) (i8_to_int y) ==>
+ int_rem (i8_to_int x) (i8_to_int y) <= i8_max ==>
+ ?z. i8_rem x y = Return z /\ i8_to_int z = int_rem (i8_to_int x) (i8_to_int y)
+Proof
+ prove_arith_op_eq
+QED
+
+
+(*
+Theorem U16_DIV_EQ:
+ !x y.
+ u16_to_int y <> 0 ==>
+ ?z. u16_div x y = Return z /\ u16_to_int z = u16_to_int x / u16_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem U32_DIV_EQ:
+ !x y.
+ u32_to_int y <> 0 ==>
+ ?z. u32_div x y = Return z /\ u32_to_int z = u32_to_int x / u32_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem U64_DIV_EQ:
+ !x y.
+ u64_to_int y <> 0 ==>
+ ?z. u64_div x y = Return z /\ u64_to_int z = u64_to_int x / u64_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem U128_DIV_EQ:
+ !x y.
+ u128_to_int y <> 0 ==>
+ ?z. u128_div x y = Return z /\ u128_to_int z = u128_to_int x / u128_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem USIZE_DIV_EQ:
+ !x y.
+ usize_to_int y <> 0 ==>
+ ?z. usize_div x y = Return z /\ usize_to_int z = usize_to_int x / usize_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I8_DIV_EQ:
+ !x y.
+ i8_to_int y <> 0 ==>
+ i8_min <= i8_to_int x / i8_to_int y ==>
+ i8_to_int x / i8_to_int y <= i8_max ==>
+ ?z. i8_div x y = Return z /\ i8_to_int z = i8_to_int x / i8_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I16_DIV_EQ:
+ !x y.
+ i16_to_int y <> 0 ==>
+ i16_min <= i16_to_int x / i16_to_int y ==>
+ i16_to_int x / i16_to_int y <= i16_max ==>
+ ?z. i16_div x y = Return z /\ i16_to_int z = i16_to_int x / i16_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I32_DIV_EQ:
+ !x y.
+ i32_to_int y <> 0 ==>
+ i32_min <= i32_to_int x / i32_to_int y ==>
+ i32_to_int x / i32_to_int y <= i32_max ==>
+ ?z. i32_div x y = Return z /\ i32_to_int z = i32_to_int x / i32_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I64_DIV_EQ:
+ !x y.
+ i64_to_int y <> 0 ==>
+ i64_min <= i64_to_int x / i64_to_int y ==>
+ i64_to_int x / i64_to_int y <= i64_max ==>
+ ?z. i64_div x y = Return z /\ i64_to_int z = i64_to_int x / i64_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem I128_DIV_EQ:
+ !x y.
+ i128_to_int y <> 0 ==>
+ i128_min <= i128_to_int x / i128_to_int y ==>
+ i128_to_int x / i128_to_int y <= i128_max ==>
+ ?z. i128_div x y = Return z /\ i128_to_int z = i128_to_int x / i128_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+Theorem ISIZE_DIV_EQ:
+ !x y.
+ isize_to_int y <> 0 ==>
+ (i16_min <= isize_to_int x / isize_to_int y \/ isize_min <= isize_to_int x / isize_to_int y) ==>
+ (isize_to_int x / isize_to_int y <= i16_max \/ isize_to_int x / isize_to_int y <= isize_max) ==>
+ ?z. isize_div x y = Return z /\ isize_to_int z = isize_to_int x / isize_to_int y
+Proof
+ prove_arith_op_eq
+QED
+
+val all_div_eqs = [
+ ISIZE_DIV_EQ,
+ I8_DIV_EQ,
+ I16_DIV_EQ,
+ I32_DIV_EQ,
+ I64_DIV_EQ,
+ I128_DIV_EQ,
+ USIZE_DIV_EQ,
+ U8_DIV_EQ,
+ U16_DIV_EQ,
+ U32_DIV_EQ,
+ U64_DIV_EQ,
+ U128_DIV_EQ
+]