diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/hol4/primitivesScript.sml | 116 | ||||
| -rw-r--r-- | backends/hol4/primitivesTheory.sig | 284 |
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. |