diff options
Diffstat (limited to 'backends/hol4')
| -rw-r--r-- | backends/hol4/ilistScript.sml | 82 | ||||
| -rw-r--r-- | backends/hol4/ilistTheory.sig | 63 | ||||
| -rw-r--r-- | backends/hol4/primitivesArithScript.sml | 55 | ||||
| -rw-r--r-- | backends/hol4/primitivesArithTheory.sig | 9 | ||||
| -rw-r--r-- | backends/hol4/primitivesScript.sml | 44 | ||||
| -rw-r--r-- | backends/hol4/primitivesTheory.sig | 291 |
6 files changed, 333 insertions, 211 deletions
diff --git a/backends/hol4/ilistScript.sml b/backends/hol4/ilistScript.sml new file mode 100644 index 00000000..3e17dcc8 --- /dev/null +++ b/backends/hol4/ilistScript.sml @@ -0,0 +1,82 @@ +open HolKernel boolLib bossLib Parse +open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory + +open primitivesArithTheory primitivesBaseTacLib + +(* The following theory contains alternative definitions of functions operating + on lists like “EL” or “LENGTH”, but this time using integers rather than + natural numbers. + + By using integers, we make sure we don't have to convert back and forth + between integers and natural numbers, which is extremely cumbersome in + the proofs. + *) + +val _ = new_theory "ilist" + +val len_def = Define ‘ + len [] : int = 0 /\ + len (x :: ls) : int = 1 + len ls +’ + +(* Return the ith element of a list. + + Remark: we initially added the following case, so that we wouldn't need the + premise [i < len ls] is [index_eq_EL]: + “index (i : int) [] = EL (Num i) []” + *) +val index_def = Define ‘ + index (i : int) [] = EL (Num i) [] ∧ + index (i : int) (x :: ls) = if i = 0 then x else (if 0 < i then index (i - 1) ls else ARB) +’ + +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) +’ + +Theorem len_eq_LENGTH: + ∀ls. len ls = &(LENGTH ls) +Proof + Induct_on ‘ls’ >> fs [len_def] >> cooper_tac +QED + +Theorem index_eq_EL: + ∀(i: int) ls. + 0 ≤ i ⇒ + i < len ls ⇒ + index i ls = EL (Num i) ls +Proof + Induct_on ‘ls’ >> rpt strip_tac >> fs [len_def, index_def] >> + Cases_on ‘i = 0’ >> fs [] >> + (* TODO: automate *) + sg ‘0 < i’ >- cooper_tac >> fs [] >> + Cases_on ‘Num i’ >- (exfalso >> cooper_tac) >> fs [] >> + last_assum (qspec_assume ‘i - 1’) >> + pop_assum sg_premise_tac >- cooper_tac >> + sg ‘n = Num (i - 1)’ >- cooper_tac >> fs [] >> + last_assum irule >> cooper_tac +QED + +Theorem len_append: + ∀l1 l2. len (l1 ++ l2) = len l1 + len l2 +Proof + rw [len_eq_LENGTH] >> cooper_tac +QED + +Theorem append_len_eq: + (∀l1 l2 l1' l2'. + len l1 = len l1' ⇒ + (l1 ⧺ l2 = l1' ⧺ l2' ⇔ l1 = l1' ∧ l2 = l2')) ∧ + (∀l1 l2 l1' l2'. + len l2 = len l2' ⇒ + (l1 ⧺ l2 = l1' ⧺ l2' ⇔ l1 = l1' ∧ l2 = l2')) +Proof + rw [len_eq_LENGTH] >> fs [APPEND_11_LENGTH] +QED + +(* TODO: prove more theorems, and add rewriting theorems *) + +val _ = export_theory () diff --git a/backends/hol4/ilistTheory.sig b/backends/hol4/ilistTheory.sig new file mode 100644 index 00000000..9612f063 --- /dev/null +++ b/backends/hol4/ilistTheory.sig @@ -0,0 +1,63 @@ +signature ilistTheory = +sig + type thm = Thm.thm + + (* Definitions *) + val index_def : thm + val len_def : thm + val update_def : thm + + (* Theorems *) + val append_len_eq : thm + val index_eq_EL : thm + val len_append : thm + val len_eq_LENGTH : thm + + val ilist_grammars : type_grammar.grammar * term_grammar.grammar +(* + [primitivesArith] Parent theory of "ilist" + + [string] Parent theory of "ilist" + + [index_def] Definition + + ⊢ (∀i. index i [] = EL (Num i) []) ∧ + ∀i x ls. + index i (x::ls) = + if i = 0 then x else if 0 < i then index (i − 1) ls else ARB + + [len_def] Definition + + ⊢ len [] = 0 ∧ ∀x ls. len (x::ls) = 1 + len ls + + [update_def] Definition + + ⊢ (∀i y. update [] i y = []) ∧ + ∀x ls i y. + update (x::ls) i y = + if i = 0 then y::ls + else if 0 < i then x::update ls (i − 1) y + else x::ls + + [append_len_eq] Theorem + + ⊢ (∀l1 l2 l1' l2'. + len l1 = len l1' ⇒ (l1 ⧺ l2 = l1' ⧺ l2' ⇔ l1 = l1' ∧ l2 = l2')) ∧ + ∀l1 l2 l1' l2'. + len l2 = len l2' ⇒ (l1 ⧺ l2 = l1' ⧺ l2' ⇔ l1 = l1' ∧ l2 = l2') + + [index_eq_EL] Theorem + + ⊢ ∀i ls. 0 ≤ i ⇒ i < len ls ⇒ index i ls = EL (Num i) ls + + [len_append] Theorem + + ⊢ ∀l1 l2. len (l1 ⧺ l2) = len l1 + len l2 + + [len_eq_LENGTH] Theorem + + ⊢ ∀ls. len ls = &LENGTH ls + + +*) +end diff --git a/backends/hol4/primitivesArithScript.sml b/backends/hol4/primitivesArithScript.sml index 79d94698..eb2548fd 100644 --- a/backends/hol4/primitivesArithScript.sml +++ b/backends/hol4/primitivesArithScript.sml @@ -6,8 +6,27 @@ 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: +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) +(* TODO: add gsymed versions of those as rewriting theorems by default (we only want to + manipulate ‘<’ and ‘≤’) *) +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) + +(* + * We generate and save an induction theorem for positive integers + *) + +(* This is the induction theorem we want. + + Unfortunately, it often can't be applied by [Induct_on]. + *) +Theorem int_induction_ideal: !(P : int -> bool). P 0 /\ (!i. 0 <= i /\ P i ==> P (i+1)) ==> !i. 0 <= i ==> P i Proof ntac 4 strip_tac >> @@ -21,20 +40,26 @@ Proof 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) +(* This induction theorem works well with [Induct_on] *) +Theorem int_induction: + !(P : int -> bool). (∀i. i < 0 ⇒ P i) ∧ P 0 /\ (!i. P i ==> P (i+1)) ==> !i. P i +Proof + ntac 3 strip_tac >> + Cases_on ‘i < 0’ >- (last_assum irule >> fs []) >> + fs [not_lt_eq_ge] >> + Induct_on ‘Num i’ >> rpt strip_tac >> pop_last_assum ignore_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 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 _ = TypeBase.update_induction int_induction -Theorem int_of_num: +Theorem int_of_num_id: ∀i. 0 ≤ i ⇒ &Num i = i Proof fs [INT_OF_NUM] @@ -64,7 +89,7 @@ Proof imp_res_tac int_of_num >> (* Associativity of & *) pure_rewrite_tac [int_add] >> - fs [] + cooper_tac QED Theorem num_sub_1_eq: diff --git a/backends/hol4/primitivesArithTheory.sig b/backends/hol4/primitivesArithTheory.sig index 73a6cf20..b2172b7c 100644 --- a/backends/hol4/primitivesArithTheory.sig +++ b/backends/hol4/primitivesArithTheory.sig @@ -7,7 +7,8 @@ sig val gt_eq_lt : thm val int_add : thm val int_induction : thm - val int_of_num : thm + val int_induction_ideal : thm + val int_of_num_id : thm val int_of_num_inj : thm val le_eq_ge : thm val lt_eq_gt : thm @@ -44,9 +45,13 @@ sig [int_induction] Theorem + ⊢ ∀P. (∀i. i < 0 ⇒ P i) ∧ P 0 ∧ (∀i. P i ⇒ P (i + 1)) ⇒ ∀i. P i + + [int_induction_ideal] Theorem + ⊢ ∀P. P 0 ∧ (∀i. 0 ≤ i ∧ P i ⇒ P (i + 1)) ⇒ ∀i. 0 ≤ i ⇒ P i - [int_of_num] Theorem + [int_of_num_id] Theorem ⊢ ∀i. 0 ≤ i ⇒ &Num i = i diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml index b1dd770b..b7bc978f 100644 --- a/backends/hol4/primitivesScript.sml +++ b/backends/hol4/primitivesScript.sml @@ -1,7 +1,7 @@ open HolKernel boolLib bossLib Parse open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory -open primitivesArithTheory primitivesBaseTacLib +open primitivesArithTheory primitivesBaseTacLib ilistTheory val primitives_theory_name = "primitives" val _ = new_theory primitives_theory_name @@ -1169,12 +1169,11 @@ val _ = new_constant ("vec_to_list", “:'a vec -> 'a list”) (* TODO: we could also make ‘mk_vec’ return ‘'a vec’ (no result) *) val _ = new_constant ("mk_vec", “:'a list -> 'a vec result”) - 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”) + “!v. (0:num) <= LENGTH (vec_to_list v) /\ LENGTH (vec_to_list v) <= Num usize_max”) +(* 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 @@ -1252,13 +1251,16 @@ Proof 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’ +*) (* TODO: shortcut for qspec_then ... ASSUME_TAC *) (* TODO: use cooper_tac everywhere *) @@ -1300,6 +1302,7 @@ QED &n < &m *) +(* 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)’ @@ -1326,7 +1329,7 @@ Proof 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 [primitivesArithTheory.int_of_num] >> + dep_pure_once_rewrite_tac [int_of_num_id] >> qspec_assume ‘i’ usize_to_int_bounds >> fs [] ) >> fs [] >> @@ -1336,33 +1339,16 @@ Proof rw [] >-( (* TODO: automate *) irule int_of_num_neq_inj >> - dep_pure_rewrite_tac [primitivesArithTheory.int_of_num] >> + dep_pure_rewrite_tac [int_of_num_id] >> rw [usize_to_int_bounds] >> metis_tac [int_to_usize_usize_to_int] ) >> (* TODO: automate *) pure_once_rewrite_tac [gsym INT_LT] >> - dep_pure_once_rewrite_tac [primitivesArithTheory.int_of_num] >> + dep_pure_once_rewrite_tac [int_of_num_id] >> qspec_assume ‘j’ usize_to_int_bounds >> fs [] QED - - -(* Small experiment: trying to redefine common functions with integers instead of nums *) -val index_def = Define ‘ - index (i : int) (x :: ls) = if i = 0 then x else (if 0 < i then index (i - 1) ls else ARB) -’ - -val len_def = Define ‘ - len [] : int = 0 /\ - len (x :: ls) : int = 1 + len ls -’ - -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) -’ +*) Theorem update_len: ∀ls i y. len (update ls i y) = len ls @@ -1417,8 +1403,11 @@ QED Theorem vec_to_list_int_bounds: !v. 0 <= len (vec_to_list v) /\ len (vec_to_list v) <= usize_max Proof - (* TODO *) - cheat + gen_tac >> + qspec_assume ‘v’ vec_to_list_num_bounds >> + fs [len_eq_LENGTH] >> + assume_tac usize_bounds >> fs [u16_max_def] >> + cooper_tac QED val vec_len_def = Define ‘vec_len v = int_to_usize (len (vec_to_list v))’ @@ -1438,7 +1427,6 @@ val vec_index_def = Define ‘ 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”) diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig index 92f02af8..23846737 100644 --- a/backends/hol4/primitivesTheory.sig +++ b/backends/hol4/primitivesTheory.sig @@ -85,14 +85,12 @@ sig val i8_mul_def : thm val i8_rem_def : thm val i8_sub_def : thm - val index_def : thm val int_rem_def : thm val isize_add_def : thm val isize_div_def : thm val isize_mul_def : thm val isize_rem_def : thm val isize_sub_def : thm - val len_def : thm val massert_def : thm val mem_replace_back_def : thm val mem_replace_fwd_def : thm @@ -142,7 +140,6 @@ sig val u8_mul_def : thm val u8_rem_def : thm val u8_sub_def : thm - val update_def : thm val usize_add_def : thm val usize_div_def : thm val usize_mul_def : thm @@ -151,8 +148,6 @@ sig val vec_index_def : thm val vec_insert_back_def : thm val vec_len_def : thm - val vec_new_def : thm - val vec_push_back_def : thm (* Theorems *) val datatype_error : thm @@ -237,7 +232,6 @@ sig 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 @@ -251,209 +245,208 @@ sig val primitives_grammars : type_grammar.grammar * term_grammar.grammar (* - [primitivesArith] Parent theory of "primitives" + [ilist] Parent theory of "primitives" - [string] Parent theory of "primitives" + [isize_bounds] Axiom + + [oracles: ] [axioms: isize_bounds] [] + ⊢ isize_min ≤ i16_min ∧ isize_max ≥ i16_max - [mk_vec_spec] Axiom + [usize_bounds] Axiom - [oracles: ] [axioms: mk_vec_spec] [] - ⊢ ∀l. len l ≤ usize_max ⇒ ∃v. mk_vec l = Return v ∧ vec_to_list v = l + [oracles: ] [axioms: usize_bounds] [] ⊢ usize_max ≥ u16_max - [vec_to_list_num_bounds] Axiom + [isize_to_int_bounds] Axiom - [oracles: ] [axioms: vec_to_list_num_bounds] [] - ⊢ ∀v. (let l = LENGTH (vec_to_list v) in 0 ≤ l ∧ l ≤ Num usize_max) + [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 + [i8_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_usize_usize_to_int] [] - ⊢ ∀i. int_to_usize (usize_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 + [i16_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_u128_u128_to_int] [] - ⊢ ∀i. int_to_u128 (u128_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 + [i32_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_u64_u64_to_int] [] - ⊢ ∀i. int_to_u64 (u64_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 + [i64_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_u32_u32_to_int] [] - ⊢ ∀i. int_to_u32 (u32_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 + [i128_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_u16_u16_to_int] [] - ⊢ ∀i. int_to_u16 (u16_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 + [usize_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_u8_u8_to_int] [] - ⊢ ∀i. int_to_u8 (u8_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 + [u8_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_isize_isize_to_int] [] - ⊢ ∀i. int_to_isize (isize_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 + [u16_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_i128_i128_to_int] [] - ⊢ ∀i. int_to_i128 (i128_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 + [u32_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_i64_i64_to_int] [] - ⊢ ∀i. int_to_i64 (i64_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 + [u64_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_i32_i32_to_int] [] - ⊢ ∀i. int_to_i32 (i32_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 + [u128_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_i16_i16_to_int] [] - ⊢ ∀i. int_to_i16 (i16_to_int i) = i + [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 + [isize_to_int_int_to_isize] Axiom - [oracles: ] [axioms: int_to_i8_i8_to_int] [] - ⊢ ∀i. int_to_i8 (i8_to_int i) = i + [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_int_to_u128] Axiom + [i8_to_int_int_to_i8] Axiom - [oracles: ] [axioms: u128_to_int_int_to_u128] [] - ⊢ ∀n. 0 ≤ n ∧ n ≤ u128_max ⇒ u128_to_int (int_to_u128 n) = n + [oracles: ] [axioms: i8_to_int_int_to_i8] [] + ⊢ ∀n. i8_min ≤ n ∧ n ≤ i8_max ⇒ i8_to_int (int_to_i8 n) = n - [u64_to_int_int_to_u64] Axiom + [i16_to_int_int_to_i16] Axiom - [oracles: ] [axioms: u64_to_int_int_to_u64] [] - ⊢ ∀n. 0 ≤ n ∧ n ≤ u64_max ⇒ u64_to_int (int_to_u64 n) = n + [oracles: ] [axioms: i16_to_int_int_to_i16] [] + ⊢ ∀n. i16_min ≤ n ∧ n ≤ i16_max ⇒ i16_to_int (int_to_i16 n) = n - [u32_to_int_int_to_u32] Axiom + [i32_to_int_int_to_i32] Axiom - [oracles: ] [axioms: u32_to_int_int_to_u32] [] - ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ u32_to_int (int_to_u32 n) = n + [oracles: ] [axioms: i32_to_int_int_to_i32] [] + ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ i32_to_int (int_to_i32 n) = n - [u16_to_int_int_to_u16] Axiom + [i64_to_int_int_to_i64] Axiom - [oracles: ] [axioms: u16_to_int_int_to_u16] [] - ⊢ ∀n. 0 ≤ n ∧ n ≤ u16_max ⇒ u16_to_int (int_to_u16 n) = n + [oracles: ] [axioms: i64_to_int_int_to_i64] [] + ⊢ ∀n. i64_min ≤ n ∧ n ≤ i64_max ⇒ i64_to_int (int_to_i64 n) = n - [u8_to_int_int_to_u8] Axiom + [i128_to_int_int_to_i128] Axiom - [oracles: ] [axioms: u8_to_int_int_to_u8] [] - ⊢ ∀n. 0 ≤ n ∧ n ≤ u8_max ⇒ u8_to_int (int_to_u8 n) = n + [oracles: ] [axioms: i128_to_int_int_to_i128] [] + ⊢ ∀n. i128_min ≤ n ∧ n ≤ i128_max ⇒ i128_to_int (int_to_i128 n) = n [usize_to_int_int_to_usize] Axiom [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 - - [i64_to_int_int_to_i64] Axiom + [u8_to_int_int_to_u8] Axiom - [oracles: ] [axioms: i64_to_int_int_to_i64] [] - ⊢ ∀n. i64_min ≤ n ∧ n ≤ i64_max ⇒ i64_to_int (int_to_i64 n) = n + [oracles: ] [axioms: u8_to_int_int_to_u8] [] + ⊢ ∀n. 0 ≤ n ∧ n ≤ u8_max ⇒ u8_to_int (int_to_u8 n) = n - [i32_to_int_int_to_i32] Axiom + [u16_to_int_int_to_u16] Axiom - [oracles: ] [axioms: i32_to_int_int_to_i32] [] - ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ i32_to_int (int_to_i32 n) = n + [oracles: ] [axioms: u16_to_int_int_to_u16] [] + ⊢ ∀n. 0 ≤ n ∧ n ≤ u16_max ⇒ u16_to_int (int_to_u16 n) = n - [i16_to_int_int_to_i16] Axiom + [u32_to_int_int_to_u32] Axiom - [oracles: ] [axioms: i16_to_int_int_to_i16] [] - ⊢ ∀n. i16_min ≤ n ∧ n ≤ i16_max ⇒ i16_to_int (int_to_i16 n) = n + [oracles: ] [axioms: u32_to_int_int_to_u32] [] + ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ u32_to_int (int_to_u32 n) = n - [i8_to_int_int_to_i8] Axiom + [u64_to_int_int_to_u64] Axiom - [oracles: ] [axioms: i8_to_int_int_to_i8] [] - ⊢ ∀n. i8_min ≤ n ∧ n ≤ i8_max ⇒ i8_to_int (int_to_i8 n) = n + [oracles: ] [axioms: u64_to_int_int_to_u64] [] + ⊢ ∀n. 0 ≤ n ∧ n ≤ u64_max ⇒ u64_to_int (int_to_u64 n) = n - [isize_to_int_int_to_isize] Axiom + [u128_to_int_int_to_u128] Axiom - [oracles: ] [axioms: isize_to_int_int_to_isize] [] - ⊢ ∀n. isize_min ≤ n ∧ n ≤ isize_max ⇒ - isize_to_int (int_to_isize n) = n + [oracles: ] [axioms: u128_to_int_int_to_u128] [] + ⊢ ∀n. 0 ≤ n ∧ n ≤ u128_max ⇒ u128_to_int (int_to_u128 n) = n - [u128_to_int_bounds] Axiom + [int_to_i8_i8_to_int] Axiom - [oracles: ] [axioms: u128_to_int_bounds] [] - ⊢ ∀n. 0 ≤ u128_to_int n ∧ u128_to_int n ≤ u128_max + [oracles: ] [axioms: int_to_i8_i8_to_int] [] + ⊢ ∀i. int_to_i8 (i8_to_int i) = i - [u64_to_int_bounds] Axiom + [int_to_i16_i16_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_i16_i16_to_int] [] + ⊢ ∀i. int_to_i16 (i16_to_int i) = i - [u32_to_int_bounds] Axiom + [int_to_i32_i32_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_i32_i32_to_int] [] + ⊢ ∀i. int_to_i32 (i32_to_int i) = i - [u16_to_int_bounds] Axiom + [int_to_i64_i64_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_i64_i64_to_int] [] + ⊢ ∀i. int_to_i64 (i64_to_int i) = i - [u8_to_int_bounds] Axiom + [int_to_i128_i128_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_i128_i128_to_int] [] + ⊢ ∀i. int_to_i128 (i128_to_int i) = i - [usize_to_int_bounds] Axiom + [int_to_isize_isize_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_isize_isize_to_int] [] + ⊢ ∀i. int_to_isize (isize_to_int i) = i - [i128_to_int_bounds] Axiom + [int_to_u8_u8_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_u8_u8_to_int] [] + ⊢ ∀i. int_to_u8 (u8_to_int i) = i - [i64_to_int_bounds] Axiom + [int_to_u16_u16_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_u16_u16_to_int] [] + ⊢ ∀i. int_to_u16 (u16_to_int i) = i - [i32_to_int_bounds] Axiom + [int_to_u32_u32_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_u32_u32_to_int] [] + ⊢ ∀i. int_to_u32 (u32_to_int i) = i - [i16_to_int_bounds] Axiom + [int_to_u64_u64_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_u64_u64_to_int] [] + ⊢ ∀i. int_to_u64 (u64_to_int i) = i - [i8_to_int_bounds] Axiom + [int_to_u128_u128_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_u128_u128_to_int] [] + ⊢ ∀i. int_to_u128 (u128_to_int i) = i - [isize_to_int_bounds] Axiom + [int_to_usize_usize_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_usize_usize_to_int] [] + ⊢ ∀i. int_to_usize (usize_to_int i) = i - [usize_bounds] Axiom + [vec_to_list_num_bounds] Axiom - [oracles: ] [axioms: usize_bounds] [] ⊢ usize_max ≥ u16_max + [oracles: ] [axioms: vec_to_list_num_bounds] [] + ⊢ ∀v. 0 ≤ LENGTH (vec_to_list v) ∧ + LENGTH (vec_to_list v) ≤ Num usize_max - [isize_bounds] Axiom + [mk_vec_spec] Axiom - [oracles: ] [axioms: isize_bounds] [] - ⊢ isize_min ≤ i16_min ∧ isize_max ≥ i16_max + [oracles: ] [axioms: mk_vec_spec] [] + ⊢ ∀l. len l ≤ usize_max ⇒ ∃v. mk_vec l = Return v ∧ vec_to_list v = l [bind_def] Definition @@ -648,12 +641,6 @@ sig ⊢ ∀x y. i8_sub x y = mk_i8 (i8_to_int x − i8_to_int y) - [index_def] Definition - - ⊢ ∀i x ls. - index i (x::ls) = - if i = 0 then x else if 0 < i then index (i − 1) ls else ARB - [int_rem_def] Definition ⊢ ∀x y. @@ -686,10 +673,6 @@ sig ⊢ ∀x y. isize_sub x y = mk_isize (isize_to_int x − isize_to_int y) - [len_def] Definition - - ⊢ len [] = 0 ∧ ∀x ls. len (x::ls) = 1 + len ls - [massert_def] Definition ⊢ ∀b. massert b = if b then Return () else Fail Failure @@ -961,15 +944,6 @@ sig ⊢ ∀x y. u8_sub x y = mk_u8 (u8_to_int x − u8_to_int y) - [update_def] Definition - - ⊢ (∀i y. update [] i y = []) ∧ - ∀x ls i y. - update (x::ls) i y = - if i = 0 then y::ls - else if 0 < i then x::update ls (i − 1) y - else x::ls - [usize_add_def] Definition ⊢ ∀x y. usize_add x y = mk_usize (usize_to_int x + usize_to_int y) @@ -1014,15 +988,6 @@ sig ⊢ ∀v. vec_len v = int_to_usize (len (vec_to_list v)) - [vec_new_def] Definition - - ⊢ vec_new = - case mk_vec [] of Return v => v | Fail v2 => ARB | Loop => ARB - - [vec_push_back_def] Definition - - ⊢ ∀v x. vec_push_back v x = mk_vec (vec_to_list v ⧺ [x]) - [datatype_error] Theorem ⊢ DATATYPE (error Failure) @@ -1729,12 +1694,6 @@ sig ∃z. u8_sub x y = Return z ∧ u8_to_int z = u8_to_int x − u8_to_int y - [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 @@ -1801,9 +1760,9 @@ sig [vec_insert_back_spec] Theorem - [oracles: DISK_THM, cheat] - [axioms: usize_to_int_bounds, usize_to_int_int_to_usize, mk_vec_spec] - [] + [oracles: DISK_THM] + [axioms: vec_to_list_num_bounds, usize_bounds, + usize_to_int_int_to_usize, usize_to_int_bounds, mk_vec_spec] [] ⊢ ∀v i x. usize_to_int i < usize_to_int (vec_len v) ⇒ ∃nv. @@ -1815,13 +1774,13 @@ sig [vec_len_spec] Theorem - [oracles: DISK_THM, cheat] [axioms: ] [] + [oracles: DISK_THM] [axioms: usize_bounds, vec_to_list_num_bounds] [] ⊢ ∀v. vec_len v = int_to_usize (len (vec_to_list v)) ∧ 0 ≤ len (vec_to_list v) ∧ len (vec_to_list v) ≤ usize_max [vec_to_list_int_bounds] Theorem - [oracles: cheat] [axioms: ] [] + [oracles: DISK_THM] [axioms: usize_bounds, vec_to_list_num_bounds] [] ⊢ ∀v. 0 ≤ len (vec_to_list v) ∧ len (vec_to_list v) ≤ usize_max |