From af587522a71574f6022cd5c99942ced6063e9e3b Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 26 Jan 2023 08:52:16 +0100 Subject: Use lower case in the names for the HOL4 backend --- backends/hol4/primitivesArithScript.sml | 153 +++--- backends/hol4/primitivesArithTheory.sig | 83 ++-- backends/hol4/primitivesBaseTacLib.sml | 12 +- backends/hol4/primitivesScript.sml | 551 +++++++++------------ backends/hol4/primitivesTheory.sig | 850 ++++++++++++++++---------------- 5 files changed, 794 insertions(+), 855 deletions(-) (limited to 'backends') diff --git a/backends/hol4/primitivesArithScript.sml b/backends/hol4/primitivesArithScript.sml index fa2f144d..79d94698 100644 --- a/backends/hol4/primitivesArithScript.sml +++ b/backends/hol4/primitivesArithScript.sml @@ -6,142 +6,169 @@ val _ = new_theory "primitivesArith" (* TODO: we need a better library of lemmas about arithmetic *) +(* We generate and save an induction theorem for positive integers *) +Theorem int_induction: + !(P : int -> bool). P 0 /\ (!i. 0 <= i /\ P i ==> P (i+1)) ==> !i. 0 <= i ==> P i +Proof + ntac 4 strip_tac >> + Induct_on ‘Num i’ >> rpt strip_tac + >-(sg ‘i = 0’ >- cooper_tac >> fs []) >> + last_assum (qspec_assume ‘i-1’) >> + fs [] >> pop_assum irule >> + rw [] >> try_tac cooper_tac >> + first_assum (qspec_assume ‘i - 1’) >> + pop_assum irule >> + rw [] >> try_tac cooper_tac +QED + +val _ = TypeBase.update_induction int_induction + (* TODO: add those as rewriting theorems 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) +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) + +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) -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 int_of_num: + ∀i. 0 ≤ i ⇒ &Num i = i +Proof + fs [INT_OF_NUM] +QED + +Theorem int_add: + ∀m n. &(m + n) = &m + &n +Proof + fs [INT_ADD] +QED -Theorem INT_OF_NUM_INJ: +Theorem int_of_num_inj: !n m. &n = &m ==> n = m Proof rpt strip_tac >> fs [Num] QED -Theorem NUM_SUB_EQ: +Theorem num_sub_eq: !(x y z : int). x = y - z ==> 0 <= x ==> 0 <= z ==> Num y = Num z + Num x Proof rpt strip_tac >> - sg ‘0 <= y’ >- COOPER_TAC >> + sg ‘0 <= y’ >- cooper_tac >> rfs [] >> (* Convert to integers *) - irule INT_OF_NUM_INJ >> - imp_res_tac (GSYM INT_OF_NUM) >> + irule int_of_num_inj >> + imp_res_tac int_of_num >> (* Associativity of & *) - PURE_REWRITE_TAC [GSYM INT_ADD] >> + pure_rewrite_tac [int_add] >> fs [] QED -Theorem NUM_SUB_1_EQ: +Theorem num_sub_1_eq: !(x y : int). x = y - 1 ==> 0 <= x ==> Num y = SUC (Num x) Proof rpt strip_tac >> (* Get rid of the SUC *) sg ‘SUC (Num x) = 1 + Num x’ >-(rw [ADD]) >> rw [] >> (* Massage a bit the goal *) - qsuff_tac ‘Num y = Num (y − 1) + Num 1’ >- COOPER_TAC >> + qsuff_tac ‘Num y = Num (y − 1) + Num 1’ >- cooper_tac >> (* Apply the general theorem *) - irule NUM_SUB_EQ >> - COOPER_TAC + irule num_sub_eq >> + cooper_tac QED -Theorem POS_MUL_POS_IS_POS: +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[] + sg ‘0 <= &(Num x) * &(Num y)’ >- (rw [INT_MUL_CALCULATE] >> cooper_tac) >> + sg_dep_rewrite_all_tac int_of_num >> try_tac cooper_tac >> fs [] QED -Theorem POS_DIV_POS_IS_POS: +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 >> + 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] >> + 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 + 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: +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 >> + sg ‘d <> 0’ >- cooper_tac >> + qspecl_assume [‘\k. k = x / d’, ‘x’, ‘d’] INT_DIV_P >> + qspecl_assume [‘\k. k = y / d’, ‘y’, ‘d’] INT_DIV_P >> + rfs [not_lt_eq_ge] >> try_tac cooper_tac >> + sg ‘y = (x / d) * d + (r' + y - x)’ >- cooper_tac >> + qspecl_assume [‘(x / d) * d’, ‘r' + y - x’, ‘d’] 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) >> + 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) >> + 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: +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 <> 0’ >- cooper_tac >> + qspecl_assume [‘\k. k = x / y’, ‘x’, ‘y’] 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 >> + qspecl_assume [‘1’, ‘y-1’, ‘x / y’] INT_LDISTRIB >> rfs [] >> - COOPER_TAC + cooper_tac ) >> - sg ‘!a b c. 0 <= c ==> a = b + c ==> b <= a’ >- (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 + 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: +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 >> + 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 ‘~(y < 0)’ >- cooper_tac >> fs [] QED -Theorem POS_MOD_POS_LE_INIT: +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 >> + 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 + 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 _ = export_theory () diff --git a/backends/hol4/primitivesArithTheory.sig b/backends/hol4/primitivesArithTheory.sig index 3b157b87..73a6cf20 100644 --- a/backends/hol4/primitivesArithTheory.sig +++ b/backends/hol4/primitivesArithTheory.sig @@ -3,23 +3,26 @@ sig type thm = Thm.thm (* Theorems *) - val GE_EQ_LE : thm - val GT_EQ_LT : thm - val INT_OF_NUM_INJ : thm - val LE_EQ_GE : thm - val LT_EQ_GT : thm - val NOT_GE_EQ_LT : thm - val NOT_GT_EQ_LE : thm - val NOT_LE_EQ_GT : thm - val NOT_LT_EQ_GE : thm - val NUM_SUB_1_EQ : thm - val NUM_SUB_EQ : thm - val POS_DIV_POS_IS_POS : thm - val POS_DIV_POS_LE : thm - val POS_DIV_POS_LE_INIT : thm - val POS_MOD_POS_IS_POS : thm - val POS_MOD_POS_LE_INIT : thm - val POS_MUL_POS_IS_POS : thm + val ge_eq_le : thm + val gt_eq_lt : thm + val int_add : thm + val int_induction : thm + val int_of_num : thm + val int_of_num_inj : thm + val le_eq_ge : thm + val lt_eq_gt : thm + val not_ge_eq_lt : thm + val not_gt_eq_le : thm + val not_le_eq_gt : thm + val not_lt_eq_ge : thm + val num_sub_1_eq : thm + val num_sub_eq : thm + val pos_div_pos_is_pos : thm + val pos_div_pos_le : thm + val pos_div_pos_le_init : thm + val pos_mod_pos_is_pos : thm + val pos_mod_pos_le_init : thm + val pos_mul_pos_is_pos : thm val primitivesArith_grammars : type_grammar.grammar * term_grammar.grammar (* @@ -27,71 +30,83 @@ sig [int_arith] Parent theory of "primitivesArith" - [GE_EQ_LE] Theorem + [ge_eq_le] Theorem ⊢ ∀x y. x ≥ y ⇔ y ≤ x - [GT_EQ_LT] Theorem + [gt_eq_lt] Theorem ⊢ ∀x y. x > y ⇔ y < x - [INT_OF_NUM_INJ] Theorem + [int_add] Theorem + + ⊢ ∀m n. &(m + n) = &m + &n + + [int_induction] Theorem + + ⊢ ∀P. P 0 ∧ (∀i. 0 ≤ i ∧ P i ⇒ P (i + 1)) ⇒ ∀i. 0 ≤ i ⇒ P i + + [int_of_num] Theorem + + ⊢ ∀i. 0 ≤ i ⇒ &Num i = i + + [int_of_num_inj] Theorem ⊢ ∀n m. &n = &m ⇒ n = m - [LE_EQ_GE] Theorem + [le_eq_ge] Theorem ⊢ ∀x y. x ≤ y ⇔ y ≥ x - [LT_EQ_GT] Theorem + [lt_eq_gt] Theorem ⊢ ∀x y. x < y ⇔ y > x - [NOT_GE_EQ_LT] Theorem + [not_ge_eq_lt] Theorem ⊢ ∀x y. ¬(x ≥ y) ⇔ x < y - [NOT_GT_EQ_LE] Theorem + [not_gt_eq_le] Theorem ⊢ ∀x y. ¬(x > y) ⇔ x ≤ y - [NOT_LE_EQ_GT] Theorem + [not_le_eq_gt] Theorem ⊢ ∀x y. ¬(x ≤ y) ⇔ x > y - [NOT_LT_EQ_GE] Theorem + [not_lt_eq_ge] Theorem ⊢ ∀x y. ¬(x < y) ⇔ x ≥ y - [NUM_SUB_1_EQ] Theorem + [num_sub_1_eq] Theorem ⊢ ∀x y. x = y − 1 ⇒ 0 ≤ x ⇒ Num y = SUC (Num x) - [NUM_SUB_EQ] Theorem + [num_sub_eq] Theorem ⊢ ∀x y z. x = y − z ⇒ 0 ≤ x ⇒ 0 ≤ z ⇒ Num y = Num z + Num x - [POS_DIV_POS_IS_POS] Theorem + [pos_div_pos_is_pos] Theorem ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x / y - [POS_DIV_POS_LE] Theorem + [pos_div_pos_le] Theorem ⊢ ∀x y d. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 < d ⇒ x ≤ y ⇒ x / d ≤ y / d - [POS_DIV_POS_LE_INIT] Theorem + [pos_div_pos_le_init] Theorem ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x / y ≤ x - [POS_MOD_POS_IS_POS] Theorem + [pos_mod_pos_is_pos] Theorem ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x % y - [POS_MOD_POS_LE_INIT] Theorem + [pos_mod_pos_le_init] Theorem ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x % y ≤ x - [POS_MUL_POS_IS_POS] Theorem + [pos_mul_pos_is_pos] Theorem ⊢ ∀x y. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 ≤ x * y diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml index 0368ee9a..75df3015 100644 --- a/backends/hol4/primitivesBaseTacLib.sml +++ b/backends/hol4/primitivesBaseTacLib.sml @@ -5,6 +5,9 @@ struct open HolKernel boolLib bossLib Parse open boolTheory arithmeticTheory integerTheory intLib listTheory +(* Remark: below, we also have conversions *) +val gsym = GSYM + (* Ignore a theorem. To be used in conjunction with {!pop_assum} for instance. @@ -13,12 +16,15 @@ fun ignore_tac (_ : thm) : tactic = ALL_TAC val pop_ignore_tac = pop_assum ignore_tac -val try_tac = TRY - (* TODO: no exfalso tactic?? *) -val ex_falso : tactic = +val exfalso : tactic = SUBGOAL_THEN “F” (fn th => ASSUME_TAC th >> fs[]) +val try_tac = TRY +val first_tac = FIRST +val map_first = MAP_FIRST +val fail_tac = FAIL_TAC + fun qspec_assume x th = qspec_then x assume_tac th fun qspecl_assume xl th = qspecl_then xl assume_tac th fun first_qspec_assume x = first_assum (qspec_assume x) diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml index 2df3375a..9da8505d 100644 --- a/backends/hol4/primitivesScript.sml +++ b/backends/hol4/primitivesScript.sml @@ -534,34 +534,35 @@ fun prove_arith_op_eq (asms, g) = | _ => failwith "Unexpected" val x = (snd o dest_comb) x_to_int; val y = (snd o dest_comb) y_to_int; + val rw_thms = int_rem_def :: List.concat [all_rem_defs, all_add_defs, all_sub_defs, all_mul_defs, all_div_defs, all_mk_int_defs, all_to_int_bounds_lemmas, all_conversion_id_lemmas]; fun inst_first_lem arg lems = - MAP_FIRST (fn th => (ASSUME_TAC (SPEC arg th) handle HOL_ERR _ => FAIL_TAC "")) 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]) >> + rpt disch_tac >> + assume_tac usize_bounds >> (* Only useful for usize of course *) + assume_tac isize_bounds >> (* Only useful for isize of course *) + rw rw_thms >> + fs rw_thms >> 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 [ + gs [not_le_eq_gt, not_lt_eq_ge, not_ge_eq_lt, not_gt_eq_le, ge_eq_le, gt_eq_lt] >> + try_tac cooper_tac >> + first_tac [ (* 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, + qspecl_assume [‘^x_to_int’, ‘^y_to_int’] pos_div_pos_is_pos >> + qspecl_assume [‘^x_to_int’, ‘^y_to_int’] pos_div_pos_le_init >> + cooper_tac, (* For remainder *) dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC all_conversion_id_lemmas >> fs [] >> - 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, + qspecl_assume [‘^x_to_int’, ‘^y_to_int’] pos_mod_pos_is_pos >> + qspecl_assume [‘^x_to_int’, ‘^y_to_int’] pos_mod_pos_le_init >> + cooper_tac, dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC all_conversion_id_lemmas >> fs [] ]) (asms, g) end -Theorem U8_ADD_EQ: +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 @@ -569,7 +570,7 @@ Proof prove_arith_op_eq QED -Theorem U16_ADD_EQ: +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 @@ -577,7 +578,7 @@ Proof prove_arith_op_eq QED -Theorem U32_ADD_EQ: +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 @@ -585,7 +586,7 @@ Proof prove_arith_op_eq QED -Theorem U64_ADD_EQ: +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 @@ -593,7 +594,7 @@ Proof prove_arith_op_eq QED -Theorem U128_ADD_EQ: +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 @@ -601,7 +602,7 @@ Proof prove_arith_op_eq QED -Theorem USIZE_ADD_EQ: +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 @@ -609,7 +610,7 @@ Proof prove_arith_op_eq QED -Theorem I8_ADD_EQ: +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 ==> @@ -618,7 +619,7 @@ Proof prove_arith_op_eq QED -Theorem I16_ADD_EQ: +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 ==> @@ -627,7 +628,7 @@ Proof prove_arith_op_eq QED -Theorem I32_ADD_EQ: +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 ==> @@ -636,7 +637,7 @@ Proof prove_arith_op_eq QED -Theorem I64_ADD_EQ: +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 ==> @@ -645,7 +646,7 @@ Proof prove_arith_op_eq QED -Theorem I128_ADD_EQ: +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 ==> @@ -654,7 +655,7 @@ Proof prove_arith_op_eq QED -Theorem ISIZE_ADD_EQ: +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) ==> @@ -664,21 +665,21 @@ Proof 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 + 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: +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 @@ -686,7 +687,7 @@ Proof prove_arith_op_eq QED -Theorem U16_SUB_EQ: +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 @@ -694,7 +695,7 @@ Proof prove_arith_op_eq QED -Theorem U32_SUB_EQ: +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 @@ -702,7 +703,7 @@ Proof prove_arith_op_eq QED -Theorem U64_SUB_EQ: +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 @@ -710,7 +711,7 @@ Proof prove_arith_op_eq QED -Theorem U128_SUB_EQ: +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 @@ -718,7 +719,7 @@ Proof prove_arith_op_eq QED -Theorem USIZE_SUB_EQ: +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 @@ -726,7 +727,7 @@ Proof prove_arith_op_eq QED -Theorem I8_SUB_EQ: +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 ==> @@ -735,7 +736,7 @@ Proof prove_arith_op_eq QED -Theorem I16_SUB_EQ: +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 ==> @@ -744,7 +745,7 @@ Proof prove_arith_op_eq QED -Theorem I32_SUB_EQ: +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 ==> @@ -753,7 +754,7 @@ Proof prove_arith_op_eq QED -Theorem I64_SUB_EQ: +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 ==> @@ -762,7 +763,7 @@ Proof prove_arith_op_eq QED -Theorem I128_SUB_EQ: +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 ==> @@ -771,7 +772,7 @@ Proof prove_arith_op_eq QED -Theorem ISIZE_SUB_EQ: +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) ==> @@ -781,21 +782,21 @@ Proof 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 + 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: +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 @@ -803,7 +804,7 @@ Proof prove_arith_op_eq QED -Theorem U16_MUL_EQ: +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 @@ -811,7 +812,7 @@ Proof prove_arith_op_eq QED -Theorem U32_MUL_EQ: +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 @@ -819,7 +820,7 @@ Proof prove_arith_op_eq QED -Theorem U64_MUL_EQ: +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 @@ -827,7 +828,7 @@ Proof prove_arith_op_eq QED -Theorem U128_MUL_EQ: +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 @@ -835,7 +836,7 @@ Proof prove_arith_op_eq QED -Theorem USIZE_MUL_EQ: +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 @@ -843,7 +844,7 @@ Proof prove_arith_op_eq QED -Theorem I8_MUL_EQ: +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 ==> @@ -852,7 +853,7 @@ Proof prove_arith_op_eq QED -Theorem I16_MUL_EQ: +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 ==> @@ -861,7 +862,7 @@ Proof prove_arith_op_eq QED -Theorem I32_MUL_EQ: +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 ==> @@ -870,7 +871,7 @@ Proof prove_arith_op_eq QED -Theorem I64_MUL_EQ: +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 ==> @@ -879,7 +880,7 @@ Proof prove_arith_op_eq QED -Theorem I128_MUL_EQ: +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 ==> @@ -888,7 +889,7 @@ Proof prove_arith_op_eq QED -Theorem ISIZE_MUL_EQ: +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) ==> @@ -898,21 +899,21 @@ Proof 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 + 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: +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 @@ -920,7 +921,7 @@ Proof prove_arith_op_eq QED -Theorem U16_DIV_EQ: +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 @@ -928,7 +929,7 @@ Proof prove_arith_op_eq QED -Theorem U32_DIV_EQ: +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 @@ -936,7 +937,7 @@ Proof prove_arith_op_eq QED -Theorem U64_DIV_EQ: +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 @@ -944,7 +945,7 @@ Proof prove_arith_op_eq QED -Theorem U128_DIV_EQ: +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 @@ -952,7 +953,7 @@ Proof prove_arith_op_eq QED -Theorem USIZE_DIV_EQ: +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 @@ -960,7 +961,7 @@ Proof prove_arith_op_eq QED -Theorem I8_DIV_EQ: +Theorem i8_div_eq: !x y. i8_to_int y <> 0 ==> i8_min <= i8_to_int x / i8_to_int y ==> @@ -970,7 +971,7 @@ Proof prove_arith_op_eq QED -Theorem I16_DIV_EQ: +Theorem i16_div_eq: !x y. i16_to_int y <> 0 ==> i16_min <= i16_to_int x / i16_to_int y ==> @@ -980,7 +981,7 @@ Proof prove_arith_op_eq QED -Theorem I32_DIV_EQ: +Theorem i32_div_eq: !x y. i32_to_int y <> 0 ==> i32_min <= i32_to_int x / i32_to_int y ==> @@ -990,7 +991,7 @@ Proof prove_arith_op_eq QED -Theorem I64_DIV_EQ: +Theorem i64_div_eq: !x y. i64_to_int y <> 0 ==> i64_min <= i64_to_int x / i64_to_int y ==> @@ -1000,7 +1001,7 @@ Proof prove_arith_op_eq QED -Theorem I128_DIV_EQ: +Theorem i128_div_eq: !x y. i128_to_int y <> 0 ==> i128_min <= i128_to_int x / i128_to_int y ==> @@ -1010,7 +1011,7 @@ Proof prove_arith_op_eq QED -Theorem ISIZE_DIV_EQ: +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) ==> @@ -1021,21 +1022,21 @@ Proof 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 + 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: +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) @@ -1043,7 +1044,7 @@ Proof prove_arith_op_eq QED -Theorem U16_REM_EQ: +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) @@ -1051,7 +1052,7 @@ Proof prove_arith_op_eq QED -Theorem U32_REM_EQ: +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) @@ -1059,7 +1060,7 @@ Proof prove_arith_op_eq QED -Theorem U64_REM_EQ: +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) @@ -1067,7 +1068,7 @@ Proof prove_arith_op_eq QED -Theorem U128_REM_EQ: +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) @@ -1075,7 +1076,7 @@ Proof prove_arith_op_eq QED -Theorem USIZE_REM_EQ: +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) @@ -1083,7 +1084,7 @@ Proof prove_arith_op_eq QED -Theorem I8_REM_EQ: +Theorem i8_rem_eq: !x y. i8_to_int y <> 0 ==> i8_min <= int_rem (i8_to_int x) (i8_to_int y) ==> @@ -1093,7 +1094,7 @@ Proof prove_arith_op_eq QED -Theorem I16_REM_EQ: +Theorem i16_rem_eq: !x y. i16_to_int y <> 0 ==> i16_min <= int_rem (i16_to_int x) (i16_to_int y) ==> @@ -1103,7 +1104,7 @@ Proof prove_arith_op_eq QED -Theorem I32_REM_EQ: +Theorem i32_rem_eq: !x y. i32_to_int y <> 0 ==> i32_min <= int_rem (i32_to_int x) (i32_to_int y) ==> @@ -1113,7 +1114,7 @@ Proof prove_arith_op_eq QED -Theorem I64_REM_EQ: +Theorem i64_rem_eq: !x y. i64_to_int y <> 0 ==> i64_min <= int_rem (i64_to_int x) (i64_to_int y) ==> @@ -1123,141 +1124,44 @@ 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: +Theorem i128_rem_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 + i128_min <= int_rem (i128_to_int x) (i128_to_int y) ==> + int_rem (i128_to_int x) (i128_to_int y) <= i128_max ==> + ?z. i128_rem x y = Return z /\ i128_to_int z = int_rem (i128_to_int x) (i128_to_int y) Proof prove_arith_op_eq QED -Theorem ISIZE_DIV_EQ: +Theorem isize_rem_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 + (i16_min <= int_rem (isize_to_int x) (isize_to_int y) \/ + isize_min <= int_rem (isize_to_int x) (isize_to_int y)) ==> + (int_rem (isize_to_int x) (isize_to_int y) <= i16_max \/ + int_rem (isize_to_int x) (isize_to_int y) <= isize_max) ==> + ?z. isize_rem x y = Return z /\ isize_to_int z = int_rem (isize_to_int x) (isize_to_int y) +Proof + prove_arith_op_eq +QED + +val all_rem_eqs = [ + isize_rem_eq, + i8_rem_eq, + i16_rem_eq, + i32_rem_eq, + i64_rem_eq, + i128_rem_eq, + usize_rem_eq, + u8_rem_eq, + u16_rem_eq, + u32_rem_eq, + u64_rem_eq, + u128_rem_eq ] + (*** * Vectors *) @@ -1268,98 +1172,102 @@ val _ = new_constant ("vec_to_list", “:'a vec -> 'a list”) val _ = new_constant ("mk_vec", “:'a list -> 'a vec result”) -val VEC_TO_LIST_NUM_BOUNDS = - new_axiom ("VEC_TO_LIST_BOUNDS", +val vec_to_list_num_bounds = + new_axiom ("vec_to_list_num_bounds", “!v. let l = LENGTH (vec_to_list v) in (0:num) <= l /\ l <= Num usize_max”) -Theorem VEC_TO_LIST_INT_BOUNDS: +Theorem vec_to_list_int_bounds: !v. 0 <= int_of_num (LENGTH (vec_to_list v)) /\ int_of_num (LENGTH (vec_to_list v)) <= usize_max Proof gen_tac >> - assume_tac VEC_TO_LIST_NUM_BOUNDS >> - pop_assum (qspec_then ‘v’ ASSUME_TAC) >> - pop_assum MP_TAC >> - PURE_ONCE_REWRITE_TAC [GSYM INT_LE] >> - sg ‘0 ≤ usize_max’ >- (ASSUME_TAC usize_bounds >> fs [u16_max_def] >> COOPER_TAC) >> + assume_tac vec_to_list_num_bounds >> + pop_assum (qspec_assume ‘v’) >> + pop_assum mp_tac >> + pure_once_rewrite_tac [GSYM INT_LE] >> + sg ‘0 ≤ usize_max’ >- (assume_tac usize_bounds >> fs [u16_max_def] >> cooper_tac) >> metis_tac [INT_OF_NUM] QED -val VEC_LEN_DEF = Define ‘vec_len v = int_to_usize (int_of_num (LENGTH (vec_to_list v)))’ -Theorem VEC_LEN_SPEC: +val vec_len_def = Define ‘vec_len v = int_to_usize (int_of_num (LENGTH (vec_to_list v)))’ +Theorem vec_len_spec: ∀v. vec_len v = int_to_usize (&(LENGTH (vec_to_list v))) ∧ 0 ≤ &(LENGTH (vec_to_list v)) ∧ &(LENGTH (vec_to_list v)) ≤ usize_max Proof - gen_tac >> rw [VEC_LEN_DEF] >> - qspec_then ‘v’ ASSUME_TAC VEC_TO_LIST_INT_BOUNDS >> + gen_tac >> rw [vec_len_def] >> + qspec_assume ‘v’ vec_to_list_int_bounds >> fs [] QED -val MK_VEC_SPEC = new_axiom ("MK_VEC_SPEC", “∀l. &(LENGTH l) ≤ usize_max ⇒ ∃v. mk_vec l = Return v ∧ vec_to_list v = l”) +val mk_vec_spec = new_axiom ("mk_vec_spec", + “∀l. &(LENGTH l) ≤ usize_max ⇒ ∃v. mk_vec l = Return v ∧ vec_to_list v = l”) -val VEC_NEW_DEF = Define ‘vec_new = case mk_vec [] of Return v => v’ -Theorem VEC_NEW_SPEC: +val vec_new_def = Define ‘vec_new = case mk_vec [] of Return v => v’ +Theorem vec_new_spec: vec_to_list vec_new = [] Proof - rw [VEC_NEW_DEF] >> + rw [vec_new_def] >> qabbrev_tac ‘l = []’ >> - qspec_then ‘l’ ASSUME_TAC MK_VEC_SPEC >> + qspec_assume ‘l’ mk_vec_spec >> Cases_on ‘mk_vec l’ >> - rfs [markerTheory.Abbrev_def, NOT_LE_EQ_GT] >> fs [] >> - ASSUME_TAC usize_bounds >> fs[u16_max_def] >> TRY (ex_falso >> COOPER_TAC) >> - sg ‘0 ≤ usize_max’ >- COOPER_TAC >> + rfs [markerTheory.Abbrev_def, not_le_eq_gt] >> fs [] >> + assume_tac usize_bounds >> fs[u16_max_def] >> try_tac (exfalso >> cooper_tac) >> + sg ‘0 ≤ usize_max’ >- cooper_tac >> fs [] QED -val VEC_PUSH_DEF = Define ‘vec_push_back v x = mk_vec (vec_to_list v ++ [x])’ -Theorem VEC_PUSH_SPEC: +val vec_push_def = Define ‘vec_push_back v x = mk_vec (vec_to_list v ++ [x])’ +Theorem vec_push_spec: ∀v x. usize_to_int (vec_len v) < usize_max ⇒ ∃vx. vec_push_back v x = Return vx ∧ vec_to_list vx = vec_to_list v ++ [x] Proof - rpt strip_tac >> fs [VEC_PUSH_DEF] >> - qspec_then ‘v’ ASSUME_TAC VEC_LEN_SPEC >> rw [] >> - qspec_then ‘vec_to_list v ++ [x]’ ASSUME_TAC MK_VEC_SPEC >> - fs [VEC_LEN_DEF] >> rw [] >> + rpt strip_tac >> fs [vec_push_def] >> + qspec_assume ‘v’ vec_len_spec >> rw [] >> + qspec_assume ‘vec_to_list v ++ [x]’ mk_vec_spec >> + fs [vec_len_def] >> rw [] >> pop_assum irule >> - pop_last_assum MP_TAC >> + pop_last_assum mp_tac >> dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC all_conversion_id_lemmas >> fs [] >> - COOPER_TAC + cooper_tac QED -val UPDATE_DEF = Define ‘ +val update_def = Define ‘ update ([] : 'a list) (i : num) (y : 'a) : 'a list = [] ∧ update (_ :: ls) (0: num) y = y :: ls ∧ update (x :: ls) (SUC i) y = x :: update ls i y ’ -Theorem UPDATE_LENGTH: +Theorem update_length: ∀ls i y. LENGTH (update ls i y) = LENGTH ls Proof - Induct_on ‘ls’ >> Cases_on ‘i’ >> rw [UPDATE_DEF] + Induct_on ‘ls’ >> Cases_on ‘i’ >> rw [update_def] QED -Theorem UPDATE_SPEC: +Theorem update_spec: ∀ls i y. i < LENGTH ls ==> LENGTH (update ls i y) = LENGTH ls ∧ EL i (update ls i y) = y ∧ ∀j. j < LENGTH ls ⇒ j ≠ i ⇒ EL j (update ls i y) = EL j ls Proof - Induct_on ‘ls’ >> Cases_on ‘i’ >> rw [UPDATE_DEF] >> + Induct_on ‘ls’ >> Cases_on ‘i’ >> rw [update_def] >> Cases_on ‘j’ >> fs [] QED (* TODO: this is the base definition for index. Shall we remove the ‘return’ type? *) -val VEC_INDEX_DEF = Define ‘ - vec_index i v = if usize_to_int i ≤ usize_to_int (vec_len v) then Return (EL (Num (usize_to_int i)) (vec_to_list v)) else Fail Failure’ +val vec_index_def = Define ‘ + vec_index i v = + if usize_to_int i ≤ usize_to_int (vec_len v) + then Return (EL (Num (usize_to_int i)) (vec_to_list v)) + else Fail Failure’ (* TODO: shortcut for qspec_then ... ASSUME_TAC *) (* TODO: use cooper_tac everywhere *) (* TODO: use pure_once_rewrite_tac everywhere *) (* TODO: injectivity lemmas for ..._to_int *) -Theorem USIZE_TO_INT_INJ: +Theorem usize_to_int_inj: ∀i j. usize_to_int i = usize_to_int j ⇔ i = j Proof rpt strip_tac >> @@ -1368,23 +1276,16 @@ Proof metis_tac [] QED -Theorem USIZE_TO_INT_NEQ_INJ: +Theorem usize_to_int_neq_inj: ∀i j. i <> j ==> usize_to_int i <> usize_to_int j Proof - metis_tac [USIZE_TO_INT_INJ] -QED - -(* TODO: move *) -Theorem INT_OF_NUM: - ∀i. 0 ≤ i ⇒ &Num i = i -Proof - metis_tac[integerTheory.INT_OF_NUM] + metis_tac [usize_to_int_inj] QED -Theorem INT_OF_NUM_NEQ_INJ: +Theorem int_of_num_neq_inj: ∀n m. &n ≠ &m ⇒ n ≠ m Proof - metis_tac [INT_OF_NUM_INJ] + metis_tac [int_of_num_inj] QED (* TODO: automate: take assumption, intro first premise as subgoal *) @@ -1403,10 +1304,10 @@ QED &n < &m *) -val VEC_INSERT_BACK_DEF = Define ‘ +val vec_insert_back_def = Define ‘ vec_insert_back (v : 'a vec) (i : usize) (x : 'a) = mk_vec (update (vec_to_list v) (Num (usize_to_int i)) x)’ -Theorem VEC_INSERT_BACK_SPEC: +Theorem vec_insert_back_spec: ∀v i x. usize_to_int i < usize_to_int (vec_len v) ⇒ ∃nv. vec_insert_back v i x = Return nv ∧ @@ -1415,20 +1316,21 @@ Theorem VEC_INSERT_BACK_SPEC: (* TODO: usize_to_int j ≠ usize_to_int i ? *) (∀j. usize_to_int j < usize_to_int (vec_len nv) ⇒ j ≠ i ⇒ vec_index j nv = vec_index j v) Proof - rpt strip_tac >> fs [VEC_INSERT_BACK_DEF] >> - qspec_assume ‘update (vec_to_list v) (Num (usize_to_int i)) x’ MK_VEC_SPEC >> - qspecl_assume [‘vec_to_list v’, ‘Num (usize_to_int i)’, ‘x’] UPDATE_LENGTH >> + rpt strip_tac >> fs [vec_insert_back_def] >> + qspec_assume ‘update (vec_to_list v) (Num (usize_to_int i)) x’ mk_vec_spec >> + qspecl_assume [‘vec_to_list v’, ‘Num (usize_to_int i)’, ‘x’] update_length >> fs [] >> - qspec_assume ‘v’ VEC_LEN_SPEC >> + qspec_assume ‘v’ vec_len_spec >> 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) >> + 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) >> fs [] >> - qspecl_assume [‘vec_to_list v’, ‘Num (usize_to_int i)’, ‘x’] UPDATE_SPEC >> rfs [] >> + 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)’ >-( (* TODO: automate *) - pure_once_rewrite_tac [GSYM INT_LT] >> - dep_pure_once_rewrite_tac [INT_OF_NUM] >> + pure_once_rewrite_tac [gsym INT_LT] >> + dep_pure_once_rewrite_tac [primitivesArithTheory.int_of_num] >> qspec_assume ‘i’ usize_to_int_bounds >> fs [] ) >> fs [] >> @@ -1437,35 +1339,19 @@ Proof first_x_assum irule >> rw [] >-( (* TODO: automate *) - irule INT_OF_NUM_NEQ_INJ >> - dep_pure_rewrite_tac [INT_OF_NUM] >> + 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 [usize_to_int_neq_inj] ) >> (* TODO: automate *) - pure_once_rewrite_tac [GSYM INT_LT] >> - dep_pure_once_rewrite_tac [INT_OF_NUM] >> + pure_once_rewrite_tac [gsym INT_LT] >> + dep_pure_once_rewrite_tac [primitivesArithTheory.int_of_num] >> qspec_assume ‘j’ usize_to_int_bounds >> fs [] QED (* TODO: use lowercase everywhere for the theorem names *) -(* We generate and save an induction theorem for positive integers *) -Theorem int_induction: - !(P : int -> bool). P 0 /\ (!i. 0 <= i /\ P i ==> P (i+1)) ==> !i. 0 <= i ==> P i -Proof - ntac 4 strip_tac >> - Induct_on ‘Num i’ >> rpt strip_tac - >-(sg ‘i = 0’ >- cooper_tac >> fs []) >> - last_assum (qspec_assume ‘i-1’) >> - fs [] >> pop_assum irule >> - rw [] >> try_tac cooper_tac >> - first_assum (qspec_assume ‘i - 1’) >> - pop_assum irule >> - rw [] >> try_tac cooper_tac -QED - -val _ = TypeBase.update_induction int_induction (* Small experiment: trying to redefine common functions with integers instead of nums *) val index_def = Define ‘ @@ -1479,7 +1365,9 @@ val len_def = Define ‘ val update_def = Define ‘ update ([] : 'a list) (i : int) (y : 'a) : 'a list = [] ∧ - update (x :: ls) (i : int) y = if i = 0 then y :: ls else (if 0 < i then x :: update ls (i - 1) y else x :: ls) + + update (x :: ls) (i : int) y = + if i = 0 then y :: ls else (if 0 < i then x :: update ls (i - 1) y else x :: ls) ’ Theorem update_len: @@ -1496,7 +1384,8 @@ Theorem update_spec: index i (update ls i y) = y ∧ ∀j. j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls Proof - Induct_on ‘ls’ >> Cases_on ‘i = 0’ >> rw [update_def, len_def, index_def] >> try_tac (ex_falso >> cooper_tac) >> + Induct_on ‘ls’ >> Cases_on ‘i = 0’ >> rw [update_def, len_def, index_def] >> + try_tac (exfalso >> cooper_tac) >> try_tac ( pop_last_assum (qspecl_assume [‘i' - 1’, ‘y’]) >> pop_assum sg_premise_tac >- cooper_tac >> @@ -1550,10 +1439,14 @@ Proof QED val vec_index_def = Define ‘ - vec_index i v = if usize_to_int i ≤ usize_to_int (vec_len v) then Return (index (usize_to_int i) (vec_to_list v)) else Fail Failure’ + vec_index i v = + if usize_to_int i ≤ usize_to_int (vec_len v) + then Return (index (usize_to_int i) (vec_to_list v)) + else Fail Failure’ (* TODO: *) -val mk_vec_spec = new_axiom ("mk_vec_spec", “∀l. len l ≤ usize_max ⇒ ∃v. mk_vec l = Return v ∧ vec_to_list v = l”) +val mk_vec_spec = new_axiom ("mk_vec_spec", + “∀l. len l ≤ usize_max ⇒ ∃v. mk_vec l = Return v ∧ vec_to_list v = l”) (* Redefining ‘vec_insert_back’ *) val vec_insert_back_def = Define ‘ diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig index cc2f3115..66adac64 100644 --- a/backends/hol4/primitivesTheory.sig +++ b/backends/hol4/primitivesTheory.sig @@ -3,8 +3,6 @@ sig type thm = Thm.thm (* Axioms *) - val MK_VEC_SPEC : thm - val VEC_TO_LIST_BOUNDS : thm val i128_to_int_bounds : thm val i16_to_int_bounds : thm val i32_to_int_bounds : thm @@ -44,6 +42,7 @@ sig val u8_to_int_bounds : thm val usize_bounds : thm val usize_to_int_bounds : thm + val vec_to_list_num_bounds : thm (* Definitions *) val bind_def : thm @@ -156,70 +155,6 @@ sig val vec_push_back_def : thm (* Theorems *) - val I128_ADD_EQ : thm - val I128_DIV_EQ : thm - val I128_MUL_EQ : thm - val I128_SUB_EQ : thm - val I16_ADD_EQ : thm - val I16_DIV_EQ : thm - val I16_MUL_EQ : thm - val I16_REM_EQ : thm - val I16_SUB_EQ : thm - val I32_ADD_EQ : thm - val I32_DIV_EQ : thm - val I32_MUL_EQ : thm - val I32_REM_EQ : thm - val I32_SUB_EQ : thm - val I64_ADD_EQ : thm - val I64_DIV_EQ : thm - val I64_MUL_EQ : thm - val I64_REM_EQ : thm - val I64_SUB_EQ : thm - val I8_ADD_EQ : thm - val I8_DIV_EQ : thm - val I8_MUL_EQ : thm - val I8_REM_EQ : thm - val I8_SUB_EQ : thm - val INT_OF_NUM : thm - val INT_OF_NUM_NEQ_INJ : thm - val ISIZE_ADD_EQ : thm - val ISIZE_DIV_EQ : thm - val ISIZE_MUL_EQ : thm - val ISIZE_SUB_EQ : thm - val U128_ADD_EQ : thm - val U128_DIV_EQ : thm - val U128_MUL_EQ : thm - val U128_REM_EQ : thm - val U128_SUB_EQ : thm - val U16_ADD_EQ : thm - val U16_DIV_EQ : thm - val U16_MUL_EQ : thm - val U16_REM_EQ : thm - val U16_SUB_EQ : thm - val U32_ADD_EQ : thm - val U32_DIV_EQ : thm - val U32_MUL_EQ : thm - val U32_REM_EQ : thm - val U32_SUB_EQ : thm - val U64_ADD_EQ : thm - val U64_DIV_EQ : thm - val U64_MUL_EQ : thm - val U64_REM_EQ : thm - val U64_SUB_EQ : thm - val U8_ADD_EQ : thm - val U8_DIV_EQ : thm - val U8_MUL_EQ : thm - val U8_REM_EQ : thm - val U8_SUB_EQ : thm - val USIZE_ADD_EQ : thm - val USIZE_DIV_EQ : thm - val USIZE_MUL_EQ : thm - val USIZE_REM_EQ : thm - val USIZE_SUB_EQ : thm - val USIZE_TO_INT_INJ : thm - val USIZE_TO_INT_NEQ_INJ : thm - val VEC_NEW_SPEC : thm - val VEC_TO_LIST_INT_BOUNDS : thm val datatype_error : thm val datatype_result : thm val error2num_11 : thm @@ -233,9 +168,39 @@ sig val error_case_eq : thm val error_induction : thm val error_nchotomy : thm + val i128_add_eq : thm + val i128_div_eq : thm + val i128_mul_eq : thm + val i128_rem_eq : thm + val i128_sub_eq : thm + val i16_add_eq : thm + val i16_div_eq : thm + val i16_mul_eq : thm + val i16_rem_eq : thm + val i16_sub_eq : thm + val i32_add_eq : thm + val i32_div_eq : thm + val i32_mul_eq : thm + val i32_rem_eq : thm + val i32_sub_eq : thm + val i64_add_eq : thm + val i64_div_eq : thm + val i64_mul_eq : thm + val i64_rem_eq : thm + val i64_sub_eq : thm + val i8_add_eq : thm + val i8_div_eq : thm + val i8_mul_eq : thm + val i8_rem_eq : thm + val i8_sub_eq : thm val index_update_diff : thm val index_update_same : thm - val int_induction : thm + val int_of_num_neq_inj : thm + val isize_add_eq : thm + val isize_div_eq : thm + val isize_mul_eq : thm + val isize_rem_eq : thm + val isize_sub_eq : thm val num2error_11 : thm val num2error_ONTO : thm val num2error_error2num : thm @@ -247,9 +212,41 @@ sig val result_distinct : thm val result_induction : thm val result_nchotomy : thm + val u128_add_eq : thm + val u128_div_eq : thm + val u128_mul_eq : thm + val u128_rem_eq : thm + val u128_sub_eq : thm + val u16_add_eq : thm + val u16_div_eq : thm + val u16_mul_eq : thm + val u16_rem_eq : thm + val u16_sub_eq : thm + val u32_add_eq : thm + val u32_div_eq : thm + val u32_mul_eq : thm + val u32_rem_eq : thm + val u32_sub_eq : thm + val u64_add_eq : thm + val u64_div_eq : thm + val u64_mul_eq : thm + val u64_rem_eq : thm + val u64_sub_eq : thm + val u8_add_eq : thm + val u8_div_eq : thm + val u8_mul_eq : thm + val u8_rem_eq : thm + val u8_sub_eq : thm val update_ind : thm val update_len : thm val update_spec : thm + val usize_add_eq : thm + val usize_div_eq : thm + 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 @@ -265,207 +262,201 @@ sig [oracles: ] [axioms: mk_vec_spec] [] ⊢ ∀l. len l ≤ usize_max ⇒ ∃v. mk_vec l = Return v ∧ vec_to_list v = l - [VEC_TO_LIST_BOUNDS] Axiom + [vec_to_list_num_bounds] Axiom - [oracles: ] [axioms: VEC_TO_LIST_BOUNDS] [] + [oracles: ] [axioms: vec_to_list_num_bounds] [] ⊢ ∀v. (let l = LENGTH (vec_to_list v) in 0 ≤ l ∧ l ≤ Num usize_max) - [isize_bounds] Axiom - - [oracles: ] [axioms: isize_bounds] [] - ⊢ isize_min ≤ i16_min ∧ isize_max ≥ i16_max - - [usize_bounds] Axiom + [int_to_usize_usize_to_int] Axiom - [oracles: ] [axioms: usize_bounds] [] ⊢ usize_max ≥ u16_max + [oracles: ] [axioms: int_to_usize_usize_to_int] [] + ⊢ ∀i. int_to_usize (usize_to_int i) = i - [isize_to_int_bounds] Axiom + [int_to_u128_u128_to_int] Axiom - [oracles: ] [axioms: isize_to_int_bounds] [] - ⊢ ∀n. isize_min ≤ isize_to_int n ∧ isize_to_int n ≤ isize_max + [oracles: ] [axioms: int_to_u128_u128_to_int] [] + ⊢ ∀i. int_to_u128 (u128_to_int i) = i - [i8_to_int_bounds] Axiom + [int_to_u64_u64_to_int] Axiom - [oracles: ] [axioms: i8_to_int_bounds] [] - ⊢ ∀n. i8_min ≤ i8_to_int n ∧ i8_to_int n ≤ i8_max + [oracles: ] [axioms: int_to_u64_u64_to_int] [] + ⊢ ∀i. int_to_u64 (u64_to_int i) = i - [i16_to_int_bounds] Axiom + [int_to_u32_u32_to_int] Axiom - [oracles: ] [axioms: i16_to_int_bounds] [] - ⊢ ∀n. i16_min ≤ i16_to_int n ∧ i16_to_int n ≤ i16_max + [oracles: ] [axioms: int_to_u32_u32_to_int] [] + ⊢ ∀i. int_to_u32 (u32_to_int i) = i - [i32_to_int_bounds] Axiom + [int_to_u16_u16_to_int] Axiom - [oracles: ] [axioms: i32_to_int_bounds] [] - ⊢ ∀n. i32_min ≤ i32_to_int n ∧ i32_to_int n ≤ i32_max + [oracles: ] [axioms: int_to_u16_u16_to_int] [] + ⊢ ∀i. int_to_u16 (u16_to_int i) = i - [i64_to_int_bounds] Axiom + [int_to_u8_u8_to_int] Axiom - [oracles: ] [axioms: i64_to_int_bounds] [] - ⊢ ∀n. i64_min ≤ i64_to_int n ∧ i64_to_int n ≤ i64_max + [oracles: ] [axioms: int_to_u8_u8_to_int] [] + ⊢ ∀i. int_to_u8 (u8_to_int i) = i - [i128_to_int_bounds] Axiom + [int_to_isize_isize_to_int] Axiom - [oracles: ] [axioms: i128_to_int_bounds] [] - ⊢ ∀n. i128_min ≤ i128_to_int n ∧ i128_to_int n ≤ i128_max + [oracles: ] [axioms: int_to_isize_isize_to_int] [] + ⊢ ∀i. int_to_isize (isize_to_int i) = i - [usize_to_int_bounds] Axiom + [int_to_i128_i128_to_int] Axiom - [oracles: ] [axioms: usize_to_int_bounds] [] - ⊢ ∀n. 0 ≤ usize_to_int n ∧ usize_to_int n ≤ usize_max + [oracles: ] [axioms: int_to_i128_i128_to_int] [] + ⊢ ∀i. int_to_i128 (i128_to_int i) = i - [u8_to_int_bounds] Axiom + [int_to_i64_i64_to_int] Axiom - [oracles: ] [axioms: u8_to_int_bounds] [] - ⊢ ∀n. 0 ≤ u8_to_int n ∧ u8_to_int n ≤ u8_max + [oracles: ] [axioms: int_to_i64_i64_to_int] [] + ⊢ ∀i. int_to_i64 (i64_to_int i) = i - [u16_to_int_bounds] Axiom + [int_to_i32_i32_to_int] Axiom - [oracles: ] [axioms: u16_to_int_bounds] [] - ⊢ ∀n. 0 ≤ u16_to_int n ∧ u16_to_int n ≤ u16_max + [oracles: ] [axioms: int_to_i32_i32_to_int] [] + ⊢ ∀i. int_to_i32 (i32_to_int i) = i - [u32_to_int_bounds] Axiom + [int_to_i16_i16_to_int] Axiom - [oracles: ] [axioms: u32_to_int_bounds] [] - ⊢ ∀n. 0 ≤ u32_to_int n ∧ u32_to_int n ≤ u32_max + [oracles: ] [axioms: int_to_i16_i16_to_int] [] + ⊢ ∀i. int_to_i16 (i16_to_int i) = i - [u64_to_int_bounds] Axiom + [int_to_i8_i8_to_int] Axiom - [oracles: ] [axioms: u64_to_int_bounds] [] - ⊢ ∀n. 0 ≤ u64_to_int n ∧ u64_to_int n ≤ u64_max + [oracles: ] [axioms: int_to_i8_i8_to_int] [] + ⊢ ∀i. int_to_i8 (i8_to_int i) = i - [u128_to_int_bounds] Axiom + [int_to_u128_id] Axiom - [oracles: ] [axioms: u128_to_int_bounds] [] - ⊢ ∀n. 0 ≤ u128_to_int n ∧ u128_to_int n ≤ u128_max + [oracles: ] [axioms: int_to_u128_id] [] + ⊢ ∀n. 0 ≤ n ∧ n ≤ u128_max ⇒ u128_to_int (int_to_u128 n) = n - [int_to_isize_id] Axiom + [int_to_u64_id] Axiom - [oracles: ] [axioms: 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 + [oracles: ] [axioms: int_to_u64_id] [] + ⊢ ∀n. 0 ≤ n ∧ n ≤ u64_max ⇒ u64_to_int (int_to_u64 n) = n - [int_to_usize_id] Axiom + [int_to_u32_id] Axiom - [oracles: ] [axioms: int_to_usize_id] [] - ⊢ ∀n. 0 ≤ n ∧ (n ≤ u16_max ∨ n ≤ usize_max) ⇒ - usize_to_int (int_to_usize n) = n + [oracles: ] [axioms: int_to_u32_id] [] + ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ u32_to_int (int_to_u32 n) = n - [int_to_i8_id] Axiom + [int_to_u16_id] Axiom - [oracles: ] [axioms: int_to_i8_id] [] - ⊢ ∀n. i8_min ≤ n ∧ n ≤ i8_max ⇒ i8_to_int (int_to_i8 n) = n + [oracles: ] [axioms: int_to_u16_id] [] + ⊢ ∀n. 0 ≤ n ∧ n ≤ u16_max ⇒ u16_to_int (int_to_u16 n) = n - [int_to_i16_id] Axiom + [int_to_u8_id] Axiom - [oracles: ] [axioms: int_to_i16_id] [] - ⊢ ∀n. i16_min ≤ n ∧ n ≤ i16_max ⇒ i16_to_int (int_to_i16 n) = n + [oracles: ] [axioms: int_to_u8_id] [] + ⊢ ∀n. 0 ≤ n ∧ n ≤ u8_max ⇒ u8_to_int (int_to_u8 n) = n - [int_to_i32_id] Axiom + [int_to_i128_id] Axiom - [oracles: ] [axioms: int_to_i32_id] [] - ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ i32_to_int (int_to_i32 n) = n + [oracles: ] [axioms: int_to_i128_id] [] + ⊢ ∀n. i128_min ≤ n ∧ n ≤ i128_max ⇒ i128_to_int (int_to_i128 n) = n [int_to_i64_id] Axiom [oracles: ] [axioms: int_to_i64_id] [] ⊢ ∀n. i64_min ≤ n ∧ n ≤ i64_max ⇒ i64_to_int (int_to_i64 n) = n - [int_to_i128_id] Axiom + [int_to_i32_id] Axiom - [oracles: ] [axioms: int_to_i128_id] [] - ⊢ ∀n. i128_min ≤ n ∧ n ≤ i128_max ⇒ i128_to_int (int_to_i128 n) = n + [oracles: ] [axioms: int_to_i32_id] [] + ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ i32_to_int (int_to_i32 n) = n - [int_to_u8_id] Axiom + [int_to_i16_id] Axiom - [oracles: ] [axioms: int_to_u8_id] [] - ⊢ ∀n. 0 ≤ n ∧ n ≤ u8_max ⇒ u8_to_int (int_to_u8 n) = n + [oracles: ] [axioms: int_to_i16_id] [] + ⊢ ∀n. i16_min ≤ n ∧ n ≤ i16_max ⇒ i16_to_int (int_to_i16 n) = n - [int_to_u16_id] Axiom + [int_to_i8_id] Axiom - [oracles: ] [axioms: int_to_u16_id] [] - ⊢ ∀n. 0 ≤ n ∧ n ≤ u16_max ⇒ u16_to_int (int_to_u16 n) = n + [oracles: ] [axioms: int_to_i8_id] [] + ⊢ ∀n. i8_min ≤ n ∧ n ≤ i8_max ⇒ i8_to_int (int_to_i8 n) = n - [int_to_u32_id] Axiom + [int_to_usize_id] Axiom - [oracles: ] [axioms: int_to_u32_id] [] - ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ u32_to_int (int_to_u32 n) = n + [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_u64_id] Axiom + [int_to_isize_id] Axiom - [oracles: ] [axioms: int_to_u64_id] [] - ⊢ ∀n. 0 ≤ n ∧ n ≤ u64_max ⇒ u64_to_int (int_to_u64 n) = n + [oracles: ] [axioms: 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 - [int_to_u128_id] Axiom + [u128_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_u128_id] [] - ⊢ ∀n. 0 ≤ n ∧ n ≤ u128_max ⇒ u128_to_int (int_to_u128 n) = n + [oracles: ] [axioms: u128_to_int_bounds] [] + ⊢ ∀n. 0 ≤ u128_to_int n ∧ u128_to_int n ≤ u128_max - [int_to_i8_i8_to_int] Axiom + [u64_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_i8_i8_to_int] [] - ⊢ ∀i. int_to_i8 (i8_to_int i) = i + [oracles: ] [axioms: u64_to_int_bounds] [] + ⊢ ∀n. 0 ≤ u64_to_int n ∧ u64_to_int n ≤ u64_max - [int_to_i16_i16_to_int] Axiom + [u32_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_i16_i16_to_int] [] - ⊢ ∀i. int_to_i16 (i16_to_int i) = i + [oracles: ] [axioms: u32_to_int_bounds] [] + ⊢ ∀n. 0 ≤ u32_to_int n ∧ u32_to_int n ≤ u32_max - [int_to_i32_i32_to_int] Axiom + [u16_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_i32_i32_to_int] [] - ⊢ ∀i. int_to_i32 (i32_to_int i) = i + [oracles: ] [axioms: u16_to_int_bounds] [] + ⊢ ∀n. 0 ≤ u16_to_int n ∧ u16_to_int n ≤ u16_max - [int_to_i64_i64_to_int] Axiom + [u8_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_i64_i64_to_int] [] - ⊢ ∀i. int_to_i64 (i64_to_int i) = i + [oracles: ] [axioms: u8_to_int_bounds] [] + ⊢ ∀n. 0 ≤ u8_to_int n ∧ u8_to_int n ≤ u8_max - [int_to_i128_i128_to_int] Axiom + [usize_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_i128_i128_to_int] [] - ⊢ ∀i. int_to_i128 (i128_to_int i) = i + [oracles: ] [axioms: usize_to_int_bounds] [] + ⊢ ∀n. 0 ≤ usize_to_int n ∧ usize_to_int n ≤ usize_max - [int_to_isize_isize_to_int] Axiom + [i128_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_isize_isize_to_int] [] - ⊢ ∀i. int_to_isize (isize_to_int i) = i + [oracles: ] [axioms: i128_to_int_bounds] [] + ⊢ ∀n. i128_min ≤ i128_to_int n ∧ i128_to_int n ≤ i128_max - [int_to_u8_u8_to_int] Axiom + [i64_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_u8_u8_to_int] [] - ⊢ ∀i. int_to_u8 (u8_to_int i) = i + [oracles: ] [axioms: i64_to_int_bounds] [] + ⊢ ∀n. i64_min ≤ i64_to_int n ∧ i64_to_int n ≤ i64_max - [int_to_u16_u16_to_int] Axiom + [i32_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_u16_u16_to_int] [] - ⊢ ∀i. int_to_u16 (u16_to_int i) = i + [oracles: ] [axioms: i32_to_int_bounds] [] + ⊢ ∀n. i32_min ≤ i32_to_int n ∧ i32_to_int n ≤ i32_max - [int_to_u32_u32_to_int] Axiom + [i16_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_u32_u32_to_int] [] - ⊢ ∀i. int_to_u32 (u32_to_int i) = i + [oracles: ] [axioms: i16_to_int_bounds] [] + ⊢ ∀n. i16_min ≤ i16_to_int n ∧ i16_to_int n ≤ i16_max - [int_to_u64_u64_to_int] Axiom + [i8_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_u64_u64_to_int] [] - ⊢ ∀i. int_to_u64 (u64_to_int i) = i + [oracles: ] [axioms: i8_to_int_bounds] [] + ⊢ ∀n. i8_min ≤ i8_to_int n ∧ i8_to_int n ≤ i8_max - [int_to_u128_u128_to_int] Axiom + [isize_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_u128_u128_to_int] [] - ⊢ ∀i. int_to_u128 (u128_to_int i) = i + [oracles: ] [axioms: isize_to_int_bounds] [] + ⊢ ∀n. isize_min ≤ isize_to_int n ∧ isize_to_int n ≤ isize_max - [int_to_usize_usize_to_int] Axiom + [usize_bounds] Axiom - [oracles: ] [axioms: int_to_usize_usize_to_int] [] - ⊢ ∀i. int_to_usize (usize_to_int i) = i + [oracles: ] [axioms: usize_bounds] [] ⊢ usize_max ≥ u16_max - [MK_VEC_SPEC] Axiom + [isize_bounds] Axiom - [oracles: ] [axioms: MK_VEC_SPEC] [] - ⊢ ∀l. &LENGTH l ≤ usize_max ⇒ - ∃v. mk_vec l = Return v ∧ vec_to_list v = l + [oracles: ] [axioms: isize_bounds] [] + ⊢ isize_min ≤ i16_min ∧ isize_max ≥ i16_max [bind_def] Definition @@ -1035,40 +1026,106 @@ sig ⊢ ∀v x. vec_push_back v x = mk_vec (vec_to_list v ⧺ [x]) - [I128_ADD_EQ] Theorem + [datatype_error] Theorem - [oracles: DISK_THM] - [axioms: isize_bounds, int_to_i128_id, usize_bounds] [] - ⊢ ∀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 + ⊢ DATATYPE (error Failure) - [I128_DIV_EQ] Theorem + [datatype_result] Theorem - [oracles: DISK_THM] - [axioms: isize_bounds, int_to_i128_id, usize_bounds] [] - ⊢ ∀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 + ⊢ DATATYPE (result Return Fail Loop) - [I128_MUL_EQ] Theorem + [error2num_11] Theorem - [oracles: DISK_THM] - [axioms: isize_bounds, int_to_i128_id, usize_bounds] [] - ⊢ ∀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 + ⊢ ∀a a'. error2num a = error2num a' ⇔ a = a' - [I128_SUB_EQ] Theorem + [error2num_ONTO] Theorem - [oracles: DISK_THM] + ⊢ ∀r. r < 1 ⇔ ∃a. r = error2num a + + [error2num_num2error] Theorem + + ⊢ ∀r. r < 1 ⇔ error2num (num2error r) = r + + [error2num_thm] Theorem + + ⊢ error2num Failure = 0 + + [error_Axiom] Theorem + + ⊢ ∀x0. ∃f. f Failure = x0 + + [error_EQ_error] Theorem + + ⊢ ∀a a'. a = a' ⇔ error2num a = error2num a' + + [error_case_cong] Theorem + + ⊢ ∀M M' v0. + M = M' ∧ (M' = Failure ⇒ v0 = v0') ⇒ + (case M of Failure => v0) = case M' of Failure => v0' + + [error_case_def] Theorem + + ⊢ ∀v0. (case Failure of Failure => v0) = v0 + + [error_case_eq] Theorem + + ⊢ (case x of Failure => v0) = v ⇔ x = Failure ∧ v0 = v + + [error_induction] Theorem + + ⊢ ∀P. P Failure ⇒ ∀a. P a + + [error_nchotomy] Theorem + + ⊢ ∀a. a = Failure + + [i128_add_eq] Theorem + + [oracles: DISK_THM] + [axioms: isize_bounds, int_to_i128_id, usize_bounds] [] + ⊢ ∀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 + + [i128_div_eq] Theorem + + [oracles: DISK_THM] + [axioms: isize_bounds, int_to_i128_id, usize_bounds] [] + ⊢ ∀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 + + [i128_mul_eq] Theorem + + [oracles: DISK_THM] + [axioms: isize_bounds, int_to_i128_id, usize_bounds] [] + ⊢ ∀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 + + [i128_rem_eq] Theorem + + [oracles: DISK_THM] + [axioms: isize_bounds, int_to_i128_id, i128_to_int_bounds, + usize_bounds] [] + ⊢ ∀x y. + i128_to_int y ≠ 0 ⇒ + i128_min ≤ int_rem (i128_to_int x) (i128_to_int y) ⇒ + int_rem (i128_to_int x) (i128_to_int y) ≤ i128_max ⇒ + ∃z. i128_rem x y = Return z ∧ + i128_to_int z = int_rem (i128_to_int x) (i128_to_int y) + + [i128_sub_eq] Theorem + + [oracles: DISK_THM] [axioms: isize_bounds, int_to_i128_id, usize_bounds] [] ⊢ ∀x y. i128_min ≤ i128_to_int x − i128_to_int y ⇒ @@ -1076,7 +1133,7 @@ sig ∃z. i128_sub x y = Return z ∧ i128_to_int z = i128_to_int x − i128_to_int y - [I16_ADD_EQ] Theorem + [i16_add_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_i16_id, usize_bounds] [] @@ -1086,7 +1143,7 @@ sig ∃z. i16_add x y = Return z ∧ i16_to_int z = i16_to_int x + i16_to_int y - [I16_DIV_EQ] Theorem + [i16_div_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_i16_id, usize_bounds] [] @@ -1097,7 +1154,7 @@ sig ∃z. i16_div x y = Return z ∧ i16_to_int z = i16_to_int x / i16_to_int y - [I16_MUL_EQ] Theorem + [i16_mul_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_i16_id, usize_bounds] [] @@ -1107,7 +1164,7 @@ sig ∃z. i16_mul x y = Return z ∧ i16_to_int z = i16_to_int x * i16_to_int y - [I16_REM_EQ] Theorem + [i16_rem_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_i16_id, i16_to_int_bounds, usize_bounds] @@ -1119,7 +1176,7 @@ sig ∃z. i16_rem x y = Return z ∧ i16_to_int z = int_rem (i16_to_int x) (i16_to_int y) - [I16_SUB_EQ] Theorem + [i16_sub_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_i16_id, usize_bounds] [] @@ -1129,7 +1186,7 @@ sig ∃z. i16_sub x y = Return z ∧ i16_to_int z = i16_to_int x − i16_to_int y - [I32_ADD_EQ] Theorem + [i32_add_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_i32_id, usize_bounds] [] @@ -1139,7 +1196,7 @@ sig ∃z. i32_add x y = Return z ∧ i32_to_int z = i32_to_int x + i32_to_int y - [I32_DIV_EQ] Theorem + [i32_div_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_i32_id, usize_bounds] [] @@ -1150,7 +1207,7 @@ sig ∃z. i32_div x y = Return z ∧ i32_to_int z = i32_to_int x / i32_to_int y - [I32_MUL_EQ] Theorem + [i32_mul_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_i32_id, usize_bounds] [] @@ -1160,7 +1217,7 @@ sig ∃z. i32_mul x y = Return z ∧ i32_to_int z = i32_to_int x * i32_to_int y - [I32_REM_EQ] Theorem + [i32_rem_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_i32_id, i32_to_int_bounds, usize_bounds] @@ -1172,7 +1229,7 @@ sig ∃z. i32_rem x y = Return z ∧ i32_to_int z = int_rem (i32_to_int x) (i32_to_int y) - [I32_SUB_EQ] Theorem + [i32_sub_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_i32_id, usize_bounds] [] @@ -1182,7 +1239,7 @@ sig ∃z. i32_sub x y = Return z ∧ i32_to_int z = i32_to_int x − i32_to_int y - [I64_ADD_EQ] Theorem + [i64_add_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_i64_id, usize_bounds] [] @@ -1192,7 +1249,7 @@ sig ∃z. i64_add x y = Return z ∧ i64_to_int z = i64_to_int x + i64_to_int y - [I64_DIV_EQ] Theorem + [i64_div_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_i64_id, usize_bounds] [] @@ -1203,7 +1260,7 @@ sig ∃z. i64_div x y = Return z ∧ i64_to_int z = i64_to_int x / i64_to_int y - [I64_MUL_EQ] Theorem + [i64_mul_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_i64_id, usize_bounds] [] @@ -1213,7 +1270,7 @@ sig ∃z. i64_mul x y = Return z ∧ i64_to_int z = i64_to_int x * i64_to_int y - [I64_REM_EQ] Theorem + [i64_rem_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_i64_id, i64_to_int_bounds, usize_bounds] @@ -1225,7 +1282,7 @@ sig ∃z. i64_rem x y = Return z ∧ i64_to_int z = int_rem (i64_to_int x) (i64_to_int y) - [I64_SUB_EQ] Theorem + [i64_sub_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_i64_id, usize_bounds] [] @@ -1235,7 +1292,7 @@ sig ∃z. i64_sub x y = Return z ∧ i64_to_int z = i64_to_int x − i64_to_int y - [I8_ADD_EQ] Theorem + [i8_add_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_i8_id, usize_bounds] [] @@ -1245,7 +1302,7 @@ sig ∃z. i8_add x y = Return z ∧ i8_to_int z = i8_to_int x + i8_to_int y - [I8_DIV_EQ] Theorem + [i8_div_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_i8_id, usize_bounds] [] @@ -1256,7 +1313,7 @@ sig ∃z. i8_div x y = Return z ∧ i8_to_int z = i8_to_int x / i8_to_int y - [I8_MUL_EQ] Theorem + [i8_mul_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_i8_id, usize_bounds] [] @@ -1266,7 +1323,7 @@ sig ∃z. i8_mul x y = Return z ∧ i8_to_int z = i8_to_int x * i8_to_int y - [I8_REM_EQ] Theorem + [i8_rem_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_i8_id, i8_to_int_bounds, usize_bounds] @@ -1278,7 +1335,7 @@ sig ∃z. i8_rem x y = Return z ∧ i8_to_int z = int_rem (i8_to_int x) (i8_to_int y) - [I8_SUB_EQ] Theorem + [i8_sub_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_i8_id, usize_bounds] [] @@ -1288,15 +1345,24 @@ sig ∃z. i8_sub x y = Return z ∧ i8_to_int z = i8_to_int x − i8_to_int y - [INT_OF_NUM] Theorem + [index_update_diff] Theorem - ⊢ ∀i. 0 ≤ i ⇒ &Num i = i + ⊢ ∀ls i j y. 0 ≤ i ⇒ i < len ls ⇒ index i (update ls i y) = y - [INT_OF_NUM_NEQ_INJ] Theorem + [index_update_same] Theorem + + ⊢ ∀ls i j y. + 0 ≤ i ⇒ + i < len ls ⇒ + j < len ls ⇒ + j ≠ i ⇒ + index j (update ls i y) = index j ls + + [int_of_num_neq_inj] Theorem ⊢ ∀n m. &n ≠ &m ⇒ n ≠ m - [ISIZE_ADD_EQ] Theorem + [isize_add_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_isize_id, isize_to_int_bounds, @@ -1309,7 +1375,7 @@ sig ∃z. isize_add x y = Return z ∧ isize_to_int z = isize_to_int x + isize_to_int y - [ISIZE_DIV_EQ] Theorem + [isize_div_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_isize_id, isize_to_int_bounds, @@ -1323,7 +1389,7 @@ sig ∃z. isize_div x y = Return z ∧ isize_to_int z = isize_to_int x / isize_to_int y - [ISIZE_MUL_EQ] Theorem + [isize_mul_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_isize_id, isize_to_int_bounds, @@ -1336,7 +1402,21 @@ sig ∃z. isize_mul x y = Return z ∧ isize_to_int z = isize_to_int x * isize_to_int y - [ISIZE_SUB_EQ] Theorem + [isize_rem_eq] Theorem + + [oracles: DISK_THM] + [axioms: isize_bounds, int_to_isize_id, 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) ∨ + isize_min ≤ int_rem (isize_to_int x) (isize_to_int y) ⇒ + int_rem (isize_to_int x) (isize_to_int y) ≤ i16_max ∨ + int_rem (isize_to_int x) (isize_to_int y) ≤ isize_max ⇒ + ∃z. isize_rem x y = Return z ∧ + isize_to_int z = int_rem (isize_to_int x) (isize_to_int y) + + [isize_sub_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_isize_id, isize_to_int_bounds, @@ -1349,7 +1429,60 @@ sig ∃z. isize_sub x y = Return z ∧ isize_to_int z = isize_to_int x − isize_to_int y - [U128_ADD_EQ] Theorem + [num2error_11] Theorem + + ⊢ ∀r r'. r < 1 ⇒ r' < 1 ⇒ (num2error r = num2error r' ⇔ r = r') + + [num2error_ONTO] Theorem + + ⊢ ∀a. ∃r. a = num2error r ∧ r < 1 + + [num2error_error2num] Theorem + + ⊢ ∀a. num2error (error2num a) = a + + [num2error_thm] Theorem + + ⊢ num2error 0 = Failure + + [result_11] Theorem + + ⊢ (∀a a'. Return a = Return a' ⇔ a = a') ∧ + ∀a a'. Fail a = Fail a' ⇔ a = a' + + [result_Axiom] Theorem + + ⊢ ∀f0 f1 f2. ∃fn. + (∀a. fn (Return a) = f0 a) ∧ (∀a. fn (Fail a) = f1 a) ∧ + fn Loop = f2 + + [result_case_cong] Theorem + + ⊢ ∀M M' f f1 v. + M = M' ∧ (∀a. M' = Return a ⇒ f a = f' a) ∧ + (∀a. M' = Fail a ⇒ f1 a = f1' a) ∧ (M' = Loop ⇒ v = v') ⇒ + result_CASE M f f1 v = result_CASE M' f' f1' v' + + [result_case_eq] Theorem + + ⊢ result_CASE x f f1 v = v' ⇔ + (∃a. x = Return a ∧ f a = v') ∨ (∃e. x = Fail e ∧ f1 e = v') ∨ + x = Loop ∧ v = v' + + [result_distinct] Theorem + + ⊢ (∀a' a. Return a ≠ Fail a') ∧ (∀a. Return a ≠ Loop) ∧ + ∀a. Fail a ≠ Loop + + [result_induction] Theorem + + ⊢ ∀P. (∀a. P (Return a)) ∧ (∀e. P (Fail e)) ∧ P Loop ⇒ ∀r. P r + + [result_nchotomy] Theorem + + ⊢ ∀rr. (∃a. rr = Return a) ∨ (∃e. rr = Fail e) ∨ rr = Loop + + [u128_add_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_u128_id, u128_to_int_bounds, @@ -1359,7 +1492,7 @@ sig ∃z. u128_add x y = Return z ∧ u128_to_int z = u128_to_int x + u128_to_int y - [U128_DIV_EQ] Theorem + [u128_div_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_u128_id, u128_to_int_bounds, @@ -1369,7 +1502,7 @@ sig ∃z. u128_div x y = Return z ∧ u128_to_int z = u128_to_int x / u128_to_int y - [U128_MUL_EQ] Theorem + [u128_mul_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_u128_id, u128_to_int_bounds, @@ -1379,7 +1512,7 @@ sig ∃z. u128_mul x y = Return z ∧ u128_to_int z = u128_to_int x * u128_to_int y - [U128_REM_EQ] Theorem + [u128_rem_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_u128_id, u128_to_int_bounds, @@ -1389,7 +1522,7 @@ sig ∃z. u128_rem x y = Return z ∧ u128_to_int z = int_rem (u128_to_int x) (u128_to_int y) - [U128_SUB_EQ] Theorem + [u128_sub_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_u128_id, u128_to_int_bounds, @@ -1399,7 +1532,7 @@ sig ∃z. u128_sub x y = Return z ∧ u128_to_int z = u128_to_int x − u128_to_int y - [U16_ADD_EQ] Theorem + [u16_add_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_u16_id, u16_to_int_bounds, usize_bounds] @@ -1409,7 +1542,7 @@ sig ∃z. u16_add x y = Return z ∧ u16_to_int z = u16_to_int x + u16_to_int y - [U16_DIV_EQ] Theorem + [u16_div_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_u16_id, u16_to_int_bounds, usize_bounds] @@ -1419,7 +1552,7 @@ sig ∃z. u16_div x y = Return z ∧ u16_to_int z = u16_to_int x / u16_to_int y - [U16_MUL_EQ] Theorem + [u16_mul_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_u16_id, u16_to_int_bounds, usize_bounds] @@ -1429,7 +1562,7 @@ sig ∃z. u16_mul x y = Return z ∧ u16_to_int z = u16_to_int x * u16_to_int y - [U16_REM_EQ] Theorem + [u16_rem_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_u16_id, u16_to_int_bounds, usize_bounds] @@ -1439,7 +1572,7 @@ sig ∃z. u16_rem x y = Return z ∧ u16_to_int z = int_rem (u16_to_int x) (u16_to_int y) - [U16_SUB_EQ] Theorem + [u16_sub_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_u16_id, u16_to_int_bounds, usize_bounds] @@ -1449,7 +1582,7 @@ sig ∃z. u16_sub x y = Return z ∧ u16_to_int z = u16_to_int x − u16_to_int y - [U32_ADD_EQ] Theorem + [u32_add_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_u32_id, u32_to_int_bounds, usize_bounds] @@ -1459,7 +1592,7 @@ sig ∃z. u32_add x y = Return z ∧ u32_to_int z = u32_to_int x + u32_to_int y - [U32_DIV_EQ] Theorem + [u32_div_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_u32_id, u32_to_int_bounds, usize_bounds] @@ -1469,7 +1602,7 @@ sig ∃z. u32_div x y = Return z ∧ u32_to_int z = u32_to_int x / u32_to_int y - [U32_MUL_EQ] Theorem + [u32_mul_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_u32_id, u32_to_int_bounds, usize_bounds] @@ -1479,7 +1612,7 @@ sig ∃z. u32_mul x y = Return z ∧ u32_to_int z = u32_to_int x * u32_to_int y - [U32_REM_EQ] Theorem + [u32_rem_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_u32_id, u32_to_int_bounds, usize_bounds] @@ -1489,7 +1622,7 @@ sig ∃z. u32_rem x y = Return z ∧ u32_to_int z = int_rem (u32_to_int x) (u32_to_int y) - [U32_SUB_EQ] Theorem + [u32_sub_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_u32_id, u32_to_int_bounds, usize_bounds] @@ -1499,7 +1632,7 @@ sig ∃z. u32_sub x y = Return z ∧ u32_to_int z = u32_to_int x − u32_to_int y - [U64_ADD_EQ] Theorem + [u64_add_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_u64_id, u64_to_int_bounds, usize_bounds] @@ -1509,7 +1642,7 @@ sig ∃z. u64_add x y = Return z ∧ u64_to_int z = u64_to_int x + u64_to_int y - [U64_DIV_EQ] Theorem + [u64_div_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_u64_id, u64_to_int_bounds, usize_bounds] @@ -1519,7 +1652,7 @@ sig ∃z. u64_div x y = Return z ∧ u64_to_int z = u64_to_int x / u64_to_int y - [U64_MUL_EQ] Theorem + [u64_mul_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_u64_id, u64_to_int_bounds, usize_bounds] @@ -1529,7 +1662,7 @@ sig ∃z. u64_mul x y = Return z ∧ u64_to_int z = u64_to_int x * u64_to_int y - [U64_REM_EQ] Theorem + [u64_rem_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_u64_id, u64_to_int_bounds, usize_bounds] @@ -1539,7 +1672,7 @@ sig ∃z. u64_rem x y = Return z ∧ u64_to_int z = int_rem (u64_to_int x) (u64_to_int y) - [U64_SUB_EQ] Theorem + [u64_sub_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_u64_id, u64_to_int_bounds, usize_bounds] @@ -1549,7 +1682,7 @@ sig ∃z. u64_sub x y = Return z ∧ u64_to_int z = u64_to_int x − u64_to_int y - [U8_ADD_EQ] Theorem + [u8_add_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_u8_id, u8_to_int_bounds, usize_bounds] @@ -1559,7 +1692,7 @@ sig ∃z. u8_add x y = Return z ∧ u8_to_int z = u8_to_int x + u8_to_int y - [U8_DIV_EQ] Theorem + [u8_div_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_u8_id, u8_to_int_bounds, usize_bounds] @@ -1569,7 +1702,7 @@ sig ∃z. u8_div x y = Return z ∧ u8_to_int z = u8_to_int x / u8_to_int y - [U8_MUL_EQ] Theorem + [u8_mul_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_u8_id, u8_to_int_bounds, usize_bounds] @@ -1579,7 +1712,7 @@ sig ∃z. u8_mul x y = Return z ∧ u8_to_int z = u8_to_int x * u8_to_int y - [U8_REM_EQ] Theorem + [u8_rem_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_u8_id, u8_to_int_bounds, usize_bounds] @@ -1589,7 +1722,7 @@ sig ∃z. u8_rem x y = Return z ∧ u8_to_int z = int_rem (u8_to_int x) (u8_to_int y) - [U8_SUB_EQ] Theorem + [u8_sub_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_u8_id, u8_to_int_bounds, usize_bounds] @@ -1599,7 +1732,25 @@ sig ∃z. u8_sub x y = Return z ∧ u8_to_int z = u8_to_int x − u8_to_int y - [USIZE_ADD_EQ] Theorem + [update_ind] Theorem + + ⊢ ∀P. (∀i y. P [] i y) ∧ (∀v0 ls y. P (v0::ls) 0 y) ∧ + (∀x ls i y. P ls i y ⇒ P (x::ls) (SUC i) y) ⇒ + ∀v v1 v2. P v v1 v2 + + [update_len] Theorem + + ⊢ ∀ls i y. len (update ls i y) = len ls + + [update_spec] Theorem + + ⊢ ∀ls i y. + 0 ≤ i ⇒ + i < len ls ⇒ + len (update ls i y) = len ls ∧ index i (update ls i y) = y ∧ + ∀j. j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls + + [usize_add_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_usize_id, usize_to_int_bounds, @@ -1610,7 +1761,7 @@ sig ∃z. usize_add x y = Return z ∧ usize_to_int z = usize_to_int x + usize_to_int y - [USIZE_DIV_EQ] Theorem + [usize_div_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_usize_id, usize_to_int_bounds, @@ -1620,7 +1771,7 @@ sig ∃z. usize_div x y = Return z ∧ usize_to_int z = usize_to_int x / usize_to_int y - [USIZE_MUL_EQ] Theorem + [usize_mul_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_usize_id, usize_to_int_bounds, @@ -1631,7 +1782,7 @@ sig ∃z. usize_mul x y = Return z ∧ usize_to_int z = usize_to_int x * usize_to_int y - [USIZE_REM_EQ] Theorem + [usize_rem_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_usize_id, usize_to_int_bounds, @@ -1641,7 +1792,7 @@ sig ∃z. usize_rem x y = Return z ∧ usize_to_int z = int_rem (usize_to_int x) (usize_to_int y) - [USIZE_SUB_EQ] Theorem + [usize_sub_eq] Theorem [oracles: DISK_THM] [axioms: isize_bounds, int_to_usize_id, usize_to_int_bounds, @@ -1651,169 +1802,16 @@ sig ∃z. usize_sub x y = Return z ∧ usize_to_int z = usize_to_int x − usize_to_int y - [USIZE_TO_INT_INJ] Theorem + [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 + [usize_to_int_neq_inj] Theorem [oracles: DISK_THM] [axioms: int_to_usize_usize_to_int] [] ⊢ ∀i j. i ≠ j ⇒ usize_to_int i ≠ usize_to_int j - [VEC_NEW_SPEC] Theorem - - [oracles: DISK_THM] [axioms: usize_bounds, MK_VEC_SPEC] [] - ⊢ vec_to_list vec_new = [] - - [VEC_TO_LIST_INT_BOUNDS] Theorem - - [oracles: DISK_THM] [axioms: usize_bounds, VEC_TO_LIST_BOUNDS] [] - ⊢ ∀v. 0 ≤ &LENGTH (vec_to_list v) ∧ - &LENGTH (vec_to_list v) ≤ usize_max - - [datatype_error] Theorem - - ⊢ DATATYPE (error Failure) - - [datatype_result] Theorem - - ⊢ DATATYPE (result Return Fail Loop) - - [error2num_11] Theorem - - ⊢ ∀a a'. error2num a = error2num a' ⇔ a = a' - - [error2num_ONTO] Theorem - - ⊢ ∀r. r < 1 ⇔ ∃a. r = error2num a - - [error2num_num2error] Theorem - - ⊢ ∀r. r < 1 ⇔ error2num (num2error r) = r - - [error2num_thm] Theorem - - ⊢ error2num Failure = 0 - - [error_Axiom] Theorem - - ⊢ ∀x0. ∃f. f Failure = x0 - - [error_EQ_error] Theorem - - ⊢ ∀a a'. a = a' ⇔ error2num a = error2num a' - - [error_case_cong] Theorem - - ⊢ ∀M M' v0. - M = M' ∧ (M' = Failure ⇒ v0 = v0') ⇒ - (case M of Failure => v0) = case M' of Failure => v0' - - [error_case_def] Theorem - - ⊢ ∀v0. (case Failure of Failure => v0) = v0 - - [error_case_eq] Theorem - - ⊢ (case x of Failure => v0) = v ⇔ x = Failure ∧ v0 = v - - [error_induction] Theorem - - ⊢ ∀P. P Failure ⇒ ∀a. P a - - [error_nchotomy] Theorem - - ⊢ ∀a. a = Failure - - [index_update_diff] Theorem - - ⊢ ∀ls i j y. 0 ≤ i ⇒ i < len ls ⇒ index i (update ls i y) = y - - [index_update_same] Theorem - - ⊢ ∀ls i j y. - 0 ≤ i ⇒ - i < len ls ⇒ - j < len ls ⇒ - j ≠ i ⇒ - index j (update ls i y) = index j ls - - [int_induction] Theorem - - ⊢ ∀P. P 0 ∧ (∀i. 0 ≤ i ∧ P i ⇒ P (i + 1)) ⇒ ∀i. 0 ≤ i ⇒ P i - - [num2error_11] Theorem - - ⊢ ∀r r'. r < 1 ⇒ r' < 1 ⇒ (num2error r = num2error r' ⇔ r = r') - - [num2error_ONTO] Theorem - - ⊢ ∀a. ∃r. a = num2error r ∧ r < 1 - - [num2error_error2num] Theorem - - ⊢ ∀a. num2error (error2num a) = a - - [num2error_thm] Theorem - - ⊢ num2error 0 = Failure - - [result_11] Theorem - - ⊢ (∀a a'. Return a = Return a' ⇔ a = a') ∧ - ∀a a'. Fail a = Fail a' ⇔ a = a' - - [result_Axiom] Theorem - - ⊢ ∀f0 f1 f2. ∃fn. - (∀a. fn (Return a) = f0 a) ∧ (∀a. fn (Fail a) = f1 a) ∧ - fn Loop = f2 - - [result_case_cong] Theorem - - ⊢ ∀M M' f f1 v. - M = M' ∧ (∀a. M' = Return a ⇒ f a = f' a) ∧ - (∀a. M' = Fail a ⇒ f1 a = f1' a) ∧ (M' = Loop ⇒ v = v') ⇒ - result_CASE M f f1 v = result_CASE M' f' f1' v' - - [result_case_eq] Theorem - - ⊢ result_CASE x f f1 v = v' ⇔ - (∃a. x = Return a ∧ f a = v') ∨ (∃e. x = Fail e ∧ f1 e = v') ∨ - x = Loop ∧ v = v' - - [result_distinct] Theorem - - ⊢ (∀a' a. Return a ≠ Fail a') ∧ (∀a. Return a ≠ Loop) ∧ - ∀a. Fail a ≠ Loop - - [result_induction] Theorem - - ⊢ ∀P. (∀a. P (Return a)) ∧ (∀e. P (Fail e)) ∧ P Loop ⇒ ∀r. P r - - [result_nchotomy] Theorem - - ⊢ ∀rr. (∃a. rr = Return a) ∨ (∃e. rr = Fail e) ∨ rr = Loop - - [update_ind] Theorem - - ⊢ ∀P. (∀i y. P [] i y) ∧ (∀v0 ls y. P (v0::ls) 0 y) ∧ - (∀x ls i y. P ls i y ⇒ P (x::ls) (SUC i) y) ⇒ - ∀v v1 v2. P v v1 v2 - - [update_len] Theorem - - ⊢ ∀ls i y. len (update ls i y) = len ls - - [update_spec] Theorem - - ⊢ ∀ls i y. - 0 ≤ i ⇒ - i < len ls ⇒ - len (update ls i y) = len ls ∧ index i (update ls i y) = y ∧ - ∀j. j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls - [vec_insert_back_spec] Theorem [oracles: DISK_THM, cheat] -- cgit v1.2.3