summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-01-26 09:19:52 +0100
committerSon HO2023-06-04 21:54:38 +0200
commitceb8447d10a395e9657a90ea656dd1218fa19a69 (patch)
tree2f3c297c1b92dc31564964387679356c94106b6d
parentaf587522a71574f6022cd5c99942ced6063e9e3b (diff)
Make more progress on primitivesScript.sml
Diffstat (limited to '')
-rw-r--r--backends/hol4/primitivesScript.sml116
-rw-r--r--backends/hol4/primitivesTheory.sig284
2 files changed, 191 insertions, 209 deletions
diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml
index 9da8505d..b1dd770b 100644
--- a/backends/hol4/primitivesScript.sml
+++ b/backends/hol4/primitivesScript.sml
@@ -185,85 +185,83 @@ 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: rename those *)
-val int_to_isize_id =
- new_axiom ("int_to_isize_id",
- “!n. (i16_min <= n \/ isize_min <= n) /\ (n <= i16_max \/ n <= isize_max) ==>
- isize_to_int (int_to_isize n) = n”)
-
(* TODO: remove the condition on u16_max, and make the massage tactic automatically use usize_bounds *)
-val int_to_usize_id =
- new_axiom ("int_to_usize_id",
- “!n. 0 <= n /\ (n <= u16_max \/ n <= usize_max) ==> usize_to_int (int_to_usize n) = n”)
+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”)
-val int_to_i8_id =
- new_axiom ("int_to_i8_id",
+val i8_to_int_int_to_i8 =
+ new_axiom ("i8_to_int_int_to_i8",
“!n. i8_min <= n /\ n <= i8_max ==> i8_to_int (int_to_i8 n) = n”)
-val int_to_i16_id =
- new_axiom ("int_to_i16_id",
+val i16_to_int_int_to_i16 =
+ new_axiom ("i16_to_int_int_to_i16",
“!n. i16_min <= n /\ n <= i16_max ==> i16_to_int (int_to_i16 n) = n”)
-val int_to_i32_id =
- new_axiom ("int_to_i32_id",
+val i32_to_int_int_to_i32 =
+ new_axiom ("i32_to_int_int_to_i32",
“!n. i32_min <= n /\ n <= i32_max ==> i32_to_int (int_to_i32 n) = n”)
-val int_to_i64_id =
- new_axiom ("int_to_i64_id",
+val i64_to_int_int_to_i64 =
+ new_axiom ("i64_to_int_int_to_i64",
“!n. i64_min <= n /\ n <= i64_max ==> i64_to_int (int_to_i64 n) = n”)
-val int_to_i128_id =
- new_axiom ("int_to_i128_id",
+val i128_to_int_int_to_i128 =
+ new_axiom ("i128_to_int_int_to_i128",
“!n. i128_min <= n /\ n <= i128_max ==> i128_to_int (int_to_i128 n) = n”)
-val int_to_u8_id =
- new_axiom ("int_to_u8_id",
+val usize_to_int_int_to_usize =
+ new_axiom ("usize_to_int_int_to_usize",
+ “!n. 0 <= n /\ n <= usize_max ==> usize_to_int (int_to_usize n) = n”)
+
+val u8_to_int_int_to_u8 =
+ new_axiom ("u8_to_int_int_to_u8",
“!n. 0 <= n /\ n <= u8_max ==> u8_to_int (int_to_u8 n) = n”)
-val int_to_u16_id =
- new_axiom ("int_to_u16_id",
+val u16_to_int_int_to_u16 =
+ new_axiom ("u16_to_int_int_to_u16",
“!n. 0 <= n /\ n <= u16_max ==> u16_to_int (int_to_u16 n) = n”)
-val int_to_u32_id =
- new_axiom ("int_to_u32_id",
+val u32_to_int_int_to_u32 =
+ new_axiom ("u32_to_int_int_to_u32",
“!n. 0 <= n /\ n <= u32_max ==> u32_to_int (int_to_u32 n) = n”)
-val int_to_u64_id =
- new_axiom ("int_to_u64_id",
+val u64_to_int_int_to_u64 =
+ new_axiom ("u64_to_int_int_to_u64",
“!n. 0 <= n /\ n <= u64_max ==> u64_to_int (int_to_u64 n) = n”)
-val int_to_u128_id =
- new_axiom ("int_to_u128_id",
+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 = [
- int_to_isize_id,
- int_to_i8_id,
- int_to_i16_id,
- int_to_i32_id,
- int_to_i64_id,
- int_to_i128_id,
- int_to_usize_id,
- int_to_u8_id,
- int_to_u16_id,
- int_to_u32_id,
- int_to_u64_id,
- int_to_u128_id
+ isize_to_int_int_to_isize,
+ i8_to_int_int_to_i8,
+ i16_to_int_int_to_i16,
+ i32_to_int_int_to_i32,
+ i64_to_int_int_to_i64,
+ i128_to_int_int_to_i128,
+ usize_to_int_int_to_usize,
+ u8_to_int_int_to_u8,
+ u16_to_int_int_to_u16,
+ u32_to_int_int_to_u32,
+ u64_to_int_int_to_u64,
+ u128_to_int_int_to_u128
]
-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”)
-val int_to_i64_i64_to_int = new_axiom ("int_to_i64_i64_to_int", “∀i. int_to_i64 (i64_to_int i) = i”)
-val int_to_i128_i128_to_int = new_axiom ("int_to_i128_i128_to_int", “∀i. int_to_i128 (i128_to_int i) = i”)
+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”)
+val int_to_i64_i64_to_int = new_axiom ("int_to_i64_i64_to_int", “∀i. int_to_i64 (i64_to_int i) = i”)
+val int_to_i128_i128_to_int = new_axiom ("int_to_i128_i128_to_int", “∀i. int_to_i128 (i128_to_int i) = i”)
val int_to_isize_isize_to_int = new_axiom ("int_to_isize_isize_to_int", “∀i. int_to_isize (isize_to_int i) = i”)
-val int_to_u8_u8_to_int = new_axiom ("int_to_u8_u8_to_int", “∀i. int_to_u8 (u8_to_int i) = i”)
-val int_to_u16_u16_to_int = new_axiom ("int_to_u16_u16_to_int", “∀i. int_to_u16 (u16_to_int i) = i”)
-val int_to_u32_u32_to_int = new_axiom ("int_to_u32_u32_to_int", “∀i. int_to_u32 (u32_to_int i) = i”)
-val int_to_u64_u64_to_int = new_axiom ("int_to_u64_u64_to_int", “∀i. int_to_u64 (u64_to_int i) = 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_u8_u8_to_int = new_axiom ("int_to_u8_u8_to_int", “∀i. int_to_u8 (u8_to_int i) = i”)
+val int_to_u16_u16_to_int = new_axiom ("int_to_u16_u16_to_int", “∀i. int_to_u16 (u16_to_int i) = i”)
+val int_to_u32_u32_to_int = new_axiom ("int_to_u32_u32_to_int", “∀i. int_to_u32 (u32_to_int i) = i”)
+val int_to_u64_u64_to_int = new_axiom ("int_to_u64_u64_to_int", “∀i. int_to_u64 (u64_to_int i) = 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”)
(** Utilities to define the arithmetic operations *)
@@ -1266,14 +1264,11 @@ val vec_index_def = Define ‘
(* TODO: use cooper_tac everywhere *)
(* TODO: use pure_once_rewrite_tac everywhere *)
-(* TODO: injectivity lemmas for ..._to_int *)
+(*
Theorem usize_to_int_inj:
∀i j. usize_to_int i = usize_to_int j ⇔ i = j
Proof
- rpt strip_tac >>
- qspec_assume ‘i’ int_to_usize_usize_to_int >>
- qspec_assume ‘j’ int_to_usize_usize_to_int >>
- metis_tac []
+ metis_tac [int_to_usize_usize_to_int]
QED
Theorem usize_to_int_neq_inj:
@@ -1281,6 +1276,7 @@ Theorem usize_to_int_neq_inj:
Proof
metis_tac [usize_to_int_inj]
QED
+*)
Theorem int_of_num_neq_inj:
∀n m. &n ≠ &m ⇒ n ≠ m
@@ -1324,7 +1320,7 @@ Proof
rw [] >> gvs [] >>
fs [vec_len_def, vec_index_def] >>
sg ‘usize_to_int (int_to_usize (&LENGTH (vec_to_list v))) = &LENGTH (vec_to_list v)’
- >-(irule int_to_usize_id >> cooper_tac) >>
+ >-(irule usize_to_int_int_to_usize >> cooper_tac) >>
fs [] >>
qspecl_assume [‘vec_to_list v’, ‘Num (usize_to_int i)’, ‘x’] update_spec >> rfs [] >>
sg ‘Num (usize_to_int i) < LENGTH (vec_to_list v)’ >-(
@@ -1342,7 +1338,7 @@ Proof
irule int_of_num_neq_inj >>
dep_pure_rewrite_tac [primitivesArithTheory.int_of_num] >>
rw [usize_to_int_bounds] >>
- metis_tac [usize_to_int_neq_inj]
+ metis_tac [int_to_usize_usize_to_int]
) >>
(* TODO: automate *)
pure_once_rewrite_tac [gsym INT_LT] >>
@@ -1350,8 +1346,6 @@ Proof
qspec_assume ‘j’ usize_to_int_bounds >> fs []
QED
-(* TODO: use lowercase everywhere for the theorem names *)
-
(* Small experiment: trying to redefine common functions with integers instead of nums *)
val index_def = Define ‘
@@ -1468,7 +1462,7 @@ Proof
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_all_tac usize_to_int_int_to_usize >- cooper_tac >> fs [] >>
sg_dep_rewrite_goal_tac index_update_diff >- cooper_tac >> fs [] >>
rw [] >>
irule index_update_same >> cooper_tac
diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index 66adac64..92f02af8 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -4,44 +4,44 @@ sig
(* Axioms *)
val i128_to_int_bounds : thm
+ val i128_to_int_int_to_i128 : thm
val i16_to_int_bounds : thm
+ val i16_to_int_int_to_i16 : thm
val i32_to_int_bounds : thm
+ val i32_to_int_int_to_i32 : thm
val i64_to_int_bounds : thm
+ val i64_to_int_int_to_i64 : thm
val i8_to_int_bounds : thm
+ val i8_to_int_int_to_i8 : 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 isize_to_int_int_to_isize : thm
val mk_vec_spec : thm
val u128_to_int_bounds : thm
+ val u128_to_int_int_to_u128 : thm
val u16_to_int_bounds : thm
+ val u16_to_int_int_to_u16 : thm
val u32_to_int_bounds : thm
+ val u32_to_int_int_to_u32 : thm
val u64_to_int_bounds : thm
+ val u64_to_int_int_to_u64 : thm
val u8_to_int_bounds : thm
+ val u8_to_int_int_to_u8 : thm
val usize_bounds : thm
val usize_to_int_bounds : thm
+ val usize_to_int_int_to_usize : thm
val vec_to_list_num_bounds : thm
(* Definitions *)
@@ -245,8 +245,6 @@ 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_insert_back_spec : thm
val vec_len_spec : thm
val vec_to_list_int_bounds : thm
@@ -327,66 +325,65 @@ sig
[oracles: ] [axioms: int_to_i8_i8_to_int] []
⊢ ∀i. int_to_i8 (i8_to_int i) = i
- [int_to_u128_id] Axiom
+ [u128_to_int_int_to_u128] Axiom
- [oracles: ] [axioms: int_to_u128_id] []
+ [oracles: ] [axioms: u128_to_int_int_to_u128] []
⊢ ∀n. 0 ≤ n ∧ n ≤ u128_max ⇒ u128_to_int (int_to_u128 n) = n
- [int_to_u64_id] Axiom
+ [u64_to_int_int_to_u64] Axiom
- [oracles: ] [axioms: int_to_u64_id] []
+ [oracles: ] [axioms: u64_to_int_int_to_u64] []
⊢ ∀n. 0 ≤ n ∧ n ≤ u64_max ⇒ u64_to_int (int_to_u64 n) = n
- [int_to_u32_id] Axiom
+ [u32_to_int_int_to_u32] Axiom
- [oracles: ] [axioms: int_to_u32_id] []
+ [oracles: ] [axioms: u32_to_int_int_to_u32] []
⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ u32_to_int (int_to_u32 n) = n
- [int_to_u16_id] Axiom
+ [u16_to_int_int_to_u16] Axiom
- [oracles: ] [axioms: int_to_u16_id] []
+ [oracles: ] [axioms: u16_to_int_int_to_u16] []
⊢ ∀n. 0 ≤ n ∧ n ≤ u16_max ⇒ u16_to_int (int_to_u16 n) = n
- [int_to_u8_id] Axiom
+ [u8_to_int_int_to_u8] Axiom
- [oracles: ] [axioms: int_to_u8_id] []
+ [oracles: ] [axioms: u8_to_int_int_to_u8] []
⊢ ∀n. 0 ≤ n ∧ n ≤ u8_max ⇒ u8_to_int (int_to_u8 n) = n
- [int_to_i128_id] Axiom
+ [usize_to_int_int_to_usize] Axiom
- [oracles: ] [axioms: int_to_i128_id] []
+ [oracles: ] [axioms: usize_to_int_int_to_usize] []
+ ⊢ ∀n. 0 ≤ n ∧ n ≤ usize_max ⇒ usize_to_int (int_to_usize n) = n
+
+ [i128_to_int_int_to_i128] Axiom
+
+ [oracles: ] [axioms: i128_to_int_int_to_i128] []
⊢ ∀n. i128_min ≤ n ∧ n ≤ i128_max ⇒ i128_to_int (int_to_i128 n) = n
- [int_to_i64_id] Axiom
+ [i64_to_int_int_to_i64] Axiom
- [oracles: ] [axioms: int_to_i64_id] []
+ [oracles: ] [axioms: i64_to_int_int_to_i64] []
⊢ ∀n. i64_min ≤ n ∧ n ≤ i64_max ⇒ i64_to_int (int_to_i64 n) = n
- [int_to_i32_id] Axiom
+ [i32_to_int_int_to_i32] Axiom
- [oracles: ] [axioms: int_to_i32_id] []
+ [oracles: ] [axioms: i32_to_int_int_to_i32] []
⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ i32_to_int (int_to_i32 n) = n
- [int_to_i16_id] Axiom
+ [i16_to_int_int_to_i16] Axiom
- [oracles: ] [axioms: int_to_i16_id] []
+ [oracles: ] [axioms: i16_to_int_int_to_i16] []
⊢ ∀n. i16_min ≤ n ∧ n ≤ i16_max ⇒ i16_to_int (int_to_i16 n) = n
- [int_to_i8_id] Axiom
+ [i8_to_int_int_to_i8] Axiom
- [oracles: ] [axioms: int_to_i8_id] []
+ [oracles: ] [axioms: i8_to_int_int_to_i8] []
⊢ ∀n. i8_min ≤ n ∧ n ≤ i8_max ⇒ i8_to_int (int_to_i8 n) = n
- [int_to_usize_id] Axiom
+ [isize_to_int_int_to_isize] Axiom
- [oracles: ] [axioms: int_to_usize_id] []
- ⊢ ∀n. 0 ≤ n ∧ (n ≤ u16_max ∨ n ≤ usize_max) ⇒
- usize_to_int (int_to_usize n) = n
-
- [int_to_isize_id] Axiom
-
- [oracles: ] [axioms: int_to_isize_id] []
- ⊢ ∀n. (i16_min ≤ n ∨ isize_min ≤ n) ∧ (n ≤ i16_max ∨ n ≤ isize_max) ⇒
+ [oracles: ] [axioms: isize_to_int_int_to_isize] []
+ ⊢ ∀n. isize_min ≤ n ∧ n ≤ isize_max ⇒
isize_to_int (int_to_isize n) = n
[u128_to_int_bounds] Axiom
@@ -1083,7 +1080,7 @@ sig
[i128_add_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_i128_id, usize_bounds] []
+ [axioms: isize_bounds, i128_to_int_int_to_i128, usize_bounds] []
⊢ ∀x y.
i128_min ≤ i128_to_int x + i128_to_int y ⇒
i128_to_int x + i128_to_int y ≤ i128_max ⇒
@@ -1093,7 +1090,7 @@ sig
[i128_div_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_i128_id, usize_bounds] []
+ [axioms: isize_bounds, i128_to_int_int_to_i128, usize_bounds] []
⊢ ∀x y.
i128_to_int y ≠ 0 ⇒
i128_min ≤ i128_to_int x / i128_to_int y ⇒
@@ -1104,7 +1101,7 @@ sig
[i128_mul_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_i128_id, usize_bounds] []
+ [axioms: isize_bounds, i128_to_int_int_to_i128, usize_bounds] []
⊢ ∀x y.
i128_min ≤ i128_to_int x * i128_to_int y ⇒
i128_to_int x * i128_to_int y ≤ i128_max ⇒
@@ -1114,7 +1111,7 @@ sig
[i128_rem_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_i128_id, i128_to_int_bounds,
+ [axioms: isize_bounds, i128_to_int_int_to_i128, i128_to_int_bounds,
usize_bounds] []
⊢ ∀x y.
i128_to_int y ≠ 0 ⇒
@@ -1126,7 +1123,7 @@ sig
[i128_sub_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_i128_id, usize_bounds] []
+ [axioms: isize_bounds, i128_to_int_int_to_i128, usize_bounds] []
⊢ ∀x y.
i128_min ≤ i128_to_int x − i128_to_int y ⇒
i128_to_int x − i128_to_int y ≤ i128_max ⇒
@@ -1136,7 +1133,7 @@ sig
[i16_add_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_i16_id, usize_bounds] []
+ [axioms: isize_bounds, i16_to_int_int_to_i16, usize_bounds] []
⊢ ∀x y.
i16_min ≤ i16_to_int x + i16_to_int y ⇒
i16_to_int x + i16_to_int y ≤ i16_max ⇒
@@ -1146,7 +1143,7 @@ sig
[i16_div_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_i16_id, usize_bounds] []
+ [axioms: isize_bounds, i16_to_int_int_to_i16, usize_bounds] []
⊢ ∀x y.
i16_to_int y ≠ 0 ⇒
i16_min ≤ i16_to_int x / i16_to_int y ⇒
@@ -1157,7 +1154,7 @@ sig
[i16_mul_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_i16_id, usize_bounds] []
+ [axioms: isize_bounds, i16_to_int_int_to_i16, usize_bounds] []
⊢ ∀x y.
i16_min ≤ i16_to_int x * i16_to_int y ⇒
i16_to_int x * i16_to_int y ≤ i16_max ⇒
@@ -1167,8 +1164,8 @@ sig
[i16_rem_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_i16_id, i16_to_int_bounds, usize_bounds]
- []
+ [axioms: isize_bounds, i16_to_int_int_to_i16, i16_to_int_bounds,
+ usize_bounds] []
⊢ ∀x y.
i16_to_int y ≠ 0 ⇒
i16_min ≤ int_rem (i16_to_int x) (i16_to_int y) ⇒
@@ -1179,7 +1176,7 @@ sig
[i16_sub_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_i16_id, usize_bounds] []
+ [axioms: isize_bounds, i16_to_int_int_to_i16, usize_bounds] []
⊢ ∀x y.
i16_min ≤ i16_to_int x − i16_to_int y ⇒
i16_to_int x − i16_to_int y ≤ i16_max ⇒
@@ -1189,7 +1186,7 @@ sig
[i32_add_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_i32_id, usize_bounds] []
+ [axioms: isize_bounds, i32_to_int_int_to_i32, usize_bounds] []
⊢ ∀x y.
i32_min ≤ i32_to_int x + i32_to_int y ⇒
i32_to_int x + i32_to_int y ≤ i32_max ⇒
@@ -1199,7 +1196,7 @@ sig
[i32_div_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_i32_id, usize_bounds] []
+ [axioms: isize_bounds, i32_to_int_int_to_i32, usize_bounds] []
⊢ ∀x y.
i32_to_int y ≠ 0 ⇒
i32_min ≤ i32_to_int x / i32_to_int y ⇒
@@ -1210,7 +1207,7 @@ sig
[i32_mul_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_i32_id, usize_bounds] []
+ [axioms: isize_bounds, i32_to_int_int_to_i32, usize_bounds] []
⊢ ∀x y.
i32_min ≤ i32_to_int x * i32_to_int y ⇒
i32_to_int x * i32_to_int y ≤ i32_max ⇒
@@ -1220,8 +1217,8 @@ sig
[i32_rem_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_i32_id, i32_to_int_bounds, usize_bounds]
- []
+ [axioms: isize_bounds, i32_to_int_int_to_i32, i32_to_int_bounds,
+ usize_bounds] []
⊢ ∀x y.
i32_to_int y ≠ 0 ⇒
i32_min ≤ int_rem (i32_to_int x) (i32_to_int y) ⇒
@@ -1232,7 +1229,7 @@ sig
[i32_sub_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_i32_id, usize_bounds] []
+ [axioms: isize_bounds, i32_to_int_int_to_i32, usize_bounds] []
⊢ ∀x y.
i32_min ≤ i32_to_int x − i32_to_int y ⇒
i32_to_int x − i32_to_int y ≤ i32_max ⇒
@@ -1242,7 +1239,7 @@ sig
[i64_add_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_i64_id, usize_bounds] []
+ [axioms: isize_bounds, i64_to_int_int_to_i64, usize_bounds] []
⊢ ∀x y.
i64_min ≤ i64_to_int x + i64_to_int y ⇒
i64_to_int x + i64_to_int y ≤ i64_max ⇒
@@ -1252,7 +1249,7 @@ sig
[i64_div_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_i64_id, usize_bounds] []
+ [axioms: isize_bounds, i64_to_int_int_to_i64, usize_bounds] []
⊢ ∀x y.
i64_to_int y ≠ 0 ⇒
i64_min ≤ i64_to_int x / i64_to_int y ⇒
@@ -1263,7 +1260,7 @@ sig
[i64_mul_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_i64_id, usize_bounds] []
+ [axioms: isize_bounds, i64_to_int_int_to_i64, usize_bounds] []
⊢ ∀x y.
i64_min ≤ i64_to_int x * i64_to_int y ⇒
i64_to_int x * i64_to_int y ≤ i64_max ⇒
@@ -1273,8 +1270,8 @@ sig
[i64_rem_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_i64_id, i64_to_int_bounds, usize_bounds]
- []
+ [axioms: isize_bounds, i64_to_int_int_to_i64, i64_to_int_bounds,
+ usize_bounds] []
⊢ ∀x y.
i64_to_int y ≠ 0 ⇒
i64_min ≤ int_rem (i64_to_int x) (i64_to_int y) ⇒
@@ -1285,7 +1282,7 @@ sig
[i64_sub_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_i64_id, usize_bounds] []
+ [axioms: isize_bounds, i64_to_int_int_to_i64, usize_bounds] []
⊢ ∀x y.
i64_min ≤ i64_to_int x − i64_to_int y ⇒
i64_to_int x − i64_to_int y ≤ i64_max ⇒
@@ -1295,7 +1292,7 @@ sig
[i8_add_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_i8_id, usize_bounds] []
+ [axioms: isize_bounds, i8_to_int_int_to_i8, usize_bounds] []
⊢ ∀x y.
i8_min ≤ i8_to_int x + i8_to_int y ⇒
i8_to_int x + i8_to_int y ≤ i8_max ⇒
@@ -1305,7 +1302,7 @@ sig
[i8_div_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_i8_id, usize_bounds] []
+ [axioms: isize_bounds, i8_to_int_int_to_i8, usize_bounds] []
⊢ ∀x y.
i8_to_int y ≠ 0 ⇒
i8_min ≤ i8_to_int x / i8_to_int y ⇒
@@ -1316,7 +1313,7 @@ sig
[i8_mul_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_i8_id, usize_bounds] []
+ [axioms: isize_bounds, i8_to_int_int_to_i8, usize_bounds] []
⊢ ∀x y.
i8_min ≤ i8_to_int x * i8_to_int y ⇒
i8_to_int x * i8_to_int y ≤ i8_max ⇒
@@ -1326,8 +1323,8 @@ sig
[i8_rem_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_i8_id, i8_to_int_bounds, usize_bounds]
- []
+ [axioms: isize_bounds, i8_to_int_int_to_i8, i8_to_int_bounds,
+ usize_bounds] []
⊢ ∀x y.
i8_to_int y ≠ 0 ⇒
i8_min ≤ int_rem (i8_to_int x) (i8_to_int y) ⇒
@@ -1338,7 +1335,7 @@ sig
[i8_sub_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_i8_id, usize_bounds] []
+ [axioms: isize_bounds, i8_to_int_int_to_i8, usize_bounds] []
⊢ ∀x y.
i8_min ≤ i8_to_int x − i8_to_int y ⇒
i8_to_int x − i8_to_int y ≤ i8_max ⇒
@@ -1365,8 +1362,8 @@ sig
[isize_add_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_isize_id, isize_to_int_bounds,
- usize_bounds] []
+ [axioms: isize_bounds, isize_to_int_int_to_isize,
+ isize_to_int_bounds, usize_bounds] []
⊢ ∀x y.
i16_min ≤ isize_to_int x + isize_to_int y ∨
isize_min ≤ isize_to_int x + isize_to_int y ⇒
@@ -1378,8 +1375,8 @@ sig
[isize_div_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_isize_id, isize_to_int_bounds,
- usize_bounds] []
+ [axioms: isize_bounds, isize_to_int_int_to_isize,
+ isize_to_int_bounds, usize_bounds] []
⊢ ∀x y.
isize_to_int y ≠ 0 ⇒
i16_min ≤ isize_to_int x / isize_to_int y ∨
@@ -1392,8 +1389,8 @@ sig
[isize_mul_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_isize_id, isize_to_int_bounds,
- usize_bounds] []
+ [axioms: isize_bounds, isize_to_int_int_to_isize,
+ isize_to_int_bounds, usize_bounds] []
⊢ ∀x y.
i16_min ≤ isize_to_int x * isize_to_int y ∨
isize_min ≤ isize_to_int x * isize_to_int y ⇒
@@ -1405,8 +1402,8 @@ sig
[isize_rem_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_isize_id, isize_to_int_bounds,
- usize_bounds] []
+ [axioms: isize_bounds, isize_to_int_int_to_isize,
+ isize_to_int_bounds, usize_bounds] []
⊢ ∀x y.
isize_to_int y ≠ 0 ⇒
i16_min ≤ int_rem (isize_to_int x) (isize_to_int y) ∨
@@ -1419,8 +1416,8 @@ sig
[isize_sub_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_isize_id, isize_to_int_bounds,
- usize_bounds] []
+ [axioms: isize_bounds, isize_to_int_int_to_isize,
+ isize_to_int_bounds, usize_bounds] []
⊢ ∀x y.
i16_min ≤ isize_to_int x − isize_to_int y ∨
isize_min ≤ isize_to_int x − isize_to_int y ⇒
@@ -1485,7 +1482,7 @@ sig
[u128_add_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_u128_id, u128_to_int_bounds,
+ [axioms: isize_bounds, u128_to_int_int_to_u128, u128_to_int_bounds,
usize_bounds] []
⊢ ∀x y.
u128_to_int x + u128_to_int y ≤ u128_max ⇒
@@ -1495,7 +1492,7 @@ sig
[u128_div_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_u128_id, u128_to_int_bounds,
+ [axioms: isize_bounds, u128_to_int_int_to_u128, u128_to_int_bounds,
usize_bounds] []
⊢ ∀x y.
u128_to_int y ≠ 0 ⇒
@@ -1505,7 +1502,7 @@ sig
[u128_mul_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_u128_id, u128_to_int_bounds,
+ [axioms: isize_bounds, u128_to_int_int_to_u128, u128_to_int_bounds,
usize_bounds] []
⊢ ∀x y.
u128_to_int x * u128_to_int y ≤ u128_max ⇒
@@ -1515,7 +1512,7 @@ sig
[u128_rem_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_u128_id, u128_to_int_bounds,
+ [axioms: isize_bounds, u128_to_int_int_to_u128, u128_to_int_bounds,
usize_bounds] []
⊢ ∀x y.
u128_to_int y ≠ 0 ⇒
@@ -1525,7 +1522,7 @@ sig
[u128_sub_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_u128_id, u128_to_int_bounds,
+ [axioms: isize_bounds, u128_to_int_int_to_u128, u128_to_int_bounds,
usize_bounds] []
⊢ ∀x y.
0 ≤ u128_to_int x − u128_to_int y ⇒
@@ -1535,8 +1532,8 @@ sig
[u16_add_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_u16_id, u16_to_int_bounds, usize_bounds]
- []
+ [axioms: isize_bounds, u16_to_int_int_to_u16, u16_to_int_bounds,
+ usize_bounds] []
⊢ ∀x y.
u16_to_int x + u16_to_int y ≤ u16_max ⇒
∃z. u16_add x y = Return z ∧
@@ -1545,8 +1542,8 @@ sig
[u16_div_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_u16_id, u16_to_int_bounds, usize_bounds]
- []
+ [axioms: isize_bounds, u16_to_int_int_to_u16, u16_to_int_bounds,
+ usize_bounds] []
⊢ ∀x y.
u16_to_int y ≠ 0 ⇒
∃z. u16_div x y = Return z ∧
@@ -1555,8 +1552,8 @@ sig
[u16_mul_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_u16_id, u16_to_int_bounds, usize_bounds]
- []
+ [axioms: isize_bounds, u16_to_int_int_to_u16, u16_to_int_bounds,
+ usize_bounds] []
⊢ ∀x y.
u16_to_int x * u16_to_int y ≤ u16_max ⇒
∃z. u16_mul x y = Return z ∧
@@ -1565,8 +1562,8 @@ sig
[u16_rem_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_u16_id, u16_to_int_bounds, usize_bounds]
- []
+ [axioms: isize_bounds, u16_to_int_int_to_u16, u16_to_int_bounds,
+ usize_bounds] []
⊢ ∀x y.
u16_to_int y ≠ 0 ⇒
∃z. u16_rem x y = Return z ∧
@@ -1575,8 +1572,8 @@ sig
[u16_sub_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_u16_id, u16_to_int_bounds, usize_bounds]
- []
+ [axioms: isize_bounds, u16_to_int_int_to_u16, u16_to_int_bounds,
+ usize_bounds] []
⊢ ∀x y.
0 ≤ u16_to_int x − u16_to_int y ⇒
∃z. u16_sub x y = Return z ∧
@@ -1585,8 +1582,8 @@ sig
[u32_add_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_u32_id, u32_to_int_bounds, usize_bounds]
- []
+ [axioms: isize_bounds, u32_to_int_int_to_u32, u32_to_int_bounds,
+ usize_bounds] []
⊢ ∀x y.
u32_to_int x + u32_to_int y ≤ u32_max ⇒
∃z. u32_add x y = Return z ∧
@@ -1595,8 +1592,8 @@ sig
[u32_div_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_u32_id, u32_to_int_bounds, usize_bounds]
- []
+ [axioms: isize_bounds, u32_to_int_int_to_u32, u32_to_int_bounds,
+ usize_bounds] []
⊢ ∀x y.
u32_to_int y ≠ 0 ⇒
∃z. u32_div x y = Return z ∧
@@ -1605,8 +1602,8 @@ sig
[u32_mul_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_u32_id, u32_to_int_bounds, usize_bounds]
- []
+ [axioms: isize_bounds, u32_to_int_int_to_u32, u32_to_int_bounds,
+ usize_bounds] []
⊢ ∀x y.
u32_to_int x * u32_to_int y ≤ u32_max ⇒
∃z. u32_mul x y = Return z ∧
@@ -1615,8 +1612,8 @@ sig
[u32_rem_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_u32_id, u32_to_int_bounds, usize_bounds]
- []
+ [axioms: isize_bounds, u32_to_int_int_to_u32, u32_to_int_bounds,
+ usize_bounds] []
⊢ ∀x y.
u32_to_int y ≠ 0 ⇒
∃z. u32_rem x y = Return z ∧
@@ -1625,8 +1622,8 @@ sig
[u32_sub_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_u32_id, u32_to_int_bounds, usize_bounds]
- []
+ [axioms: isize_bounds, u32_to_int_int_to_u32, u32_to_int_bounds,
+ usize_bounds] []
⊢ ∀x y.
0 ≤ u32_to_int x − u32_to_int y ⇒
∃z. u32_sub x y = Return z ∧
@@ -1635,8 +1632,8 @@ sig
[u64_add_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_u64_id, u64_to_int_bounds, usize_bounds]
- []
+ [axioms: isize_bounds, u64_to_int_int_to_u64, u64_to_int_bounds,
+ usize_bounds] []
⊢ ∀x y.
u64_to_int x + u64_to_int y ≤ u64_max ⇒
∃z. u64_add x y = Return z ∧
@@ -1645,8 +1642,8 @@ sig
[u64_div_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_u64_id, u64_to_int_bounds, usize_bounds]
- []
+ [axioms: isize_bounds, u64_to_int_int_to_u64, u64_to_int_bounds,
+ usize_bounds] []
⊢ ∀x y.
u64_to_int y ≠ 0 ⇒
∃z. u64_div x y = Return z ∧
@@ -1655,8 +1652,8 @@ sig
[u64_mul_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_u64_id, u64_to_int_bounds, usize_bounds]
- []
+ [axioms: isize_bounds, u64_to_int_int_to_u64, u64_to_int_bounds,
+ usize_bounds] []
⊢ ∀x y.
u64_to_int x * u64_to_int y ≤ u64_max ⇒
∃z. u64_mul x y = Return z ∧
@@ -1665,8 +1662,8 @@ sig
[u64_rem_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_u64_id, u64_to_int_bounds, usize_bounds]
- []
+ [axioms: isize_bounds, u64_to_int_int_to_u64, u64_to_int_bounds,
+ usize_bounds] []
⊢ ∀x y.
u64_to_int y ≠ 0 ⇒
∃z. u64_rem x y = Return z ∧
@@ -1675,8 +1672,8 @@ sig
[u64_sub_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_u64_id, u64_to_int_bounds, usize_bounds]
- []
+ [axioms: isize_bounds, u64_to_int_int_to_u64, u64_to_int_bounds,
+ usize_bounds] []
⊢ ∀x y.
0 ≤ u64_to_int x − u64_to_int y ⇒
∃z. u64_sub x y = Return z ∧
@@ -1685,8 +1682,8 @@ sig
[u8_add_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_u8_id, u8_to_int_bounds, usize_bounds]
- []
+ [axioms: isize_bounds, u8_to_int_int_to_u8, u8_to_int_bounds,
+ usize_bounds] []
⊢ ∀x y.
u8_to_int x + u8_to_int y ≤ u8_max ⇒
∃z. u8_add x y = Return z ∧
@@ -1695,8 +1692,8 @@ sig
[u8_div_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_u8_id, u8_to_int_bounds, usize_bounds]
- []
+ [axioms: isize_bounds, u8_to_int_int_to_u8, u8_to_int_bounds,
+ usize_bounds] []
⊢ ∀x y.
u8_to_int y ≠ 0 ⇒
∃z. u8_div x y = Return z ∧
@@ -1705,8 +1702,8 @@ sig
[u8_mul_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_u8_id, u8_to_int_bounds, usize_bounds]
- []
+ [axioms: isize_bounds, u8_to_int_int_to_u8, u8_to_int_bounds,
+ usize_bounds] []
⊢ ∀x y.
u8_to_int x * u8_to_int y ≤ u8_max ⇒
∃z. u8_mul x y = Return z ∧
@@ -1715,8 +1712,8 @@ sig
[u8_rem_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_u8_id, u8_to_int_bounds, usize_bounds]
- []
+ [axioms: isize_bounds, u8_to_int_int_to_u8, u8_to_int_bounds,
+ usize_bounds] []
⊢ ∀x y.
u8_to_int y ≠ 0 ⇒
∃z. u8_rem x y = Return z ∧
@@ -1725,8 +1722,8 @@ sig
[u8_sub_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_u8_id, u8_to_int_bounds, usize_bounds]
- []
+ [axioms: isize_bounds, u8_to_int_int_to_u8, u8_to_int_bounds,
+ usize_bounds] []
⊢ ∀x y.
0 ≤ u8_to_int x − u8_to_int y ⇒
∃z. u8_sub x y = Return z ∧
@@ -1753,8 +1750,8 @@ sig
[usize_add_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_usize_id, usize_to_int_bounds,
- usize_bounds] []
+ [axioms: isize_bounds, usize_to_int_int_to_usize,
+ usize_to_int_bounds, usize_bounds] []
⊢ ∀x y.
usize_to_int x + usize_to_int y ≤ u16_max ∨
usize_to_int x + usize_to_int y ≤ usize_max ⇒
@@ -1764,8 +1761,8 @@ sig
[usize_div_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_usize_id, usize_to_int_bounds,
- usize_bounds] []
+ [axioms: isize_bounds, usize_to_int_int_to_usize,
+ usize_to_int_bounds, usize_bounds] []
⊢ ∀x y.
usize_to_int y ≠ 0 ⇒
∃z. usize_div x y = Return z ∧
@@ -1774,8 +1771,8 @@ sig
[usize_mul_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_usize_id, usize_to_int_bounds,
- usize_bounds] []
+ [axioms: isize_bounds, usize_to_int_int_to_usize,
+ usize_to_int_bounds, usize_bounds] []
⊢ ∀x y.
usize_to_int x * usize_to_int y ≤ u16_max ∨
usize_to_int x * usize_to_int y ≤ usize_max ⇒
@@ -1785,8 +1782,8 @@ sig
[usize_rem_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_usize_id, usize_to_int_bounds,
- usize_bounds] []
+ [axioms: isize_bounds, usize_to_int_int_to_usize,
+ usize_to_int_bounds, usize_bounds] []
⊢ ∀x y.
usize_to_int y ≠ 0 ⇒
∃z. usize_rem x y = Return z ∧
@@ -1795,27 +1792,18 @@ sig
[usize_sub_eq] Theorem
[oracles: DISK_THM]
- [axioms: isize_bounds, int_to_usize_id, usize_to_int_bounds,
- usize_bounds] []
+ [axioms: isize_bounds, usize_to_int_int_to_usize,
+ usize_to_int_bounds, usize_bounds] []
⊢ ∀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
- [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_insert_back_spec] Theorem
[oracles: DISK_THM, cheat]
- [axioms: usize_to_int_bounds, int_to_usize_id, mk_vec_spec] []
+ [axioms: usize_to_int_bounds, usize_to_int_int_to_usize, mk_vec_spec]
+ []
⊢ ∀v i x.
usize_to_int i < usize_to_int (vec_len v) ⇒
∃nv.