diff options
Diffstat (limited to 'backends/hol4')
| -rw-r--r-- | backends/hol4/ilistScript.sml | 14 | ||||
| -rw-r--r-- | backends/hol4/ilistTheory.sig | 5 | ||||
| -rw-r--r-- | backends/hol4/primitivesArithTheory.sig | 35 | ||||
| -rw-r--r-- | backends/hol4/primitivesScript.sml | 29 | ||||
| -rw-r--r-- | backends/hol4/primitivesTheory.sig | 24 |
5 files changed, 98 insertions, 9 deletions
diff --git a/backends/hol4/ilistScript.sml b/backends/hol4/ilistScript.sml index 2183ef77..fb0c7688 100644 --- a/backends/hol4/ilistScript.sml +++ b/backends/hol4/ilistScript.sml @@ -16,6 +16,7 @@ val len_def = Define ‘ len [] : int = 0 /\ len (x :: ls) : int = 1 + len ls ’ +val _ = BasicProvers.export_rewrites ["len_def"] (* Return the ith element of a list. @@ -117,6 +118,7 @@ Theorem len_append: Proof rw [len_eq_LENGTH] >> cooper_tac QED +val _ = BasicProvers.export_rewrites ["len_append"] Theorem append_len_eq: (∀l1 l2 l1' l2'. @@ -129,6 +131,18 @@ Proof rw [len_eq_LENGTH] >> fs [APPEND_11_LENGTH] QED +Theorem drop_more_than_length: + ∀ ls i. + len ls ≤ i ⇒ + drop i ls = [] +Proof + Induct_on ‘ls’ >> + rw [drop_def] >> + qspec_assume ‘ls’ len_pos >> try_tac int_tac >> + last_x_assum irule >> + int_tac +QED + (* TODO: prove more theorems, and add rewriting theorems *) val _ = export_theory () diff --git a/backends/hol4/ilistTheory.sig b/backends/hol4/ilistTheory.sig index da7cdbb3..26f455d6 100644 --- a/backends/hol4/ilistTheory.sig +++ b/backends/hol4/ilistTheory.sig @@ -11,6 +11,7 @@ sig (* Theorems *) val append_len_eq : thm val drop_eq : thm + val drop_more_than_length : thm val index_eq : thm val index_eq_EL : thm val len_append : thm @@ -62,6 +63,10 @@ sig drop i (x::ls) = if 0 < i ∨ 0 ≤ i ∧ i ≠ 0 then drop (i − 1) ls else x::ls + [drop_more_than_length] Theorem + + ⊢ ∀ls i. len ls ≤ i ⇒ drop i ls = [] + [index_eq] Theorem ⊢ (∀x ls. index 0 (x::ls) = x) ∧ diff --git a/backends/hol4/primitivesArithTheory.sig b/backends/hol4/primitivesArithTheory.sig index 84b9b67a..85a627d2 100644 --- a/backends/hol4/primitivesArithTheory.sig +++ b/backends/hol4/primitivesArithTheory.sig @@ -15,13 +15,16 @@ sig val le_eq_ge : thm val lt_eq_gt : thm val mul_pos_left_le : thm + val mul_pos_left_lt : thm val mul_pos_right_le : thm + val mul_pos_right_lt : 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_ge : thm val pos_div_pos_is_pos : thm val pos_div_pos_le : thm val pos_div_pos_le_init : thm @@ -30,9 +33,13 @@ sig val pos_mod_pos_is_pos : thm val pos_mod_pos_le_init : thm val pos_mod_pos_lt : thm + val pos_mul_2_div_pos_decompose : thm val pos_mul_left_pos_le : thm + val pos_mul_left_pos_lt : thm + val pos_mul_pos_div_pos_decompose : thm val pos_mul_pos_is_pos : thm val pos_mul_right_pos_le : thm + val pos_mul_right_pos_lt : thm val primitivesArith_grammars : type_grammar.grammar * term_grammar.grammar (* @@ -88,10 +95,18 @@ sig ⊢ ∀a x y. 0 ≤ a ⇒ x ≤ y ⇒ a * x ≤ a * y + [mul_pos_left_lt] Theorem + + ⊢ ∀a x y. 0 < a ⇒ x < y ⇒ a * x < a * y + [mul_pos_right_le] Theorem ⊢ ∀a x y. 0 ≤ a ⇒ x ≤ y ⇒ x * a ≤ y * a + [mul_pos_right_lt] Theorem + + ⊢ ∀a x y. 0 < a ⇒ x < y ⇒ x * a < y * a + [not_ge_eq_lt] Theorem ⊢ ∀x y. ¬(x ≥ y) ⇔ x < y @@ -116,6 +131,10 @@ sig ⊢ ∀x y z. x = y − z ⇒ 0 ≤ x ⇒ 0 ≤ z ⇒ Num y = Num z + Num x + [pos_div_pos_ge] Theorem + + ⊢ ∀x y d. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 < d ⇒ x ≥ y ⇒ x / d ≥ y / d + [pos_div_pos_is_pos] Theorem ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x / y @@ -148,10 +167,22 @@ sig ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x % y < y + [pos_mul_2_div_pos_decompose] Theorem + + ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x / y + x / y ≤ x * 2 / y + [pos_mul_left_pos_le] Theorem ⊢ ∀a x. 0 < a ⇒ 0 ≤ x ⇒ x ≤ a * x + [pos_mul_left_pos_lt] Theorem + + ⊢ ∀a x. 1 < a ⇒ 0 < x ⇒ x < a * x + + [pos_mul_pos_div_pos_decompose] Theorem + + ⊢ ∀x y z. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 < z ⇒ x / z + y / z ≤ (x + y) / z + [pos_mul_pos_is_pos] Theorem ⊢ ∀x y. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 ≤ x * y @@ -160,6 +191,10 @@ sig ⊢ ∀a x. 0 < a ⇒ 0 ≤ x ⇒ x ≤ x * a + [pos_mul_right_pos_lt] Theorem + + ⊢ ∀a x. 1 < a ⇒ 0 < x ⇒ x < x * a + *) end diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml index 4378f9c3..82da4de9 100644 --- a/backends/hol4/primitivesScript.sml +++ b/backends/hol4/primitivesScript.sml @@ -1702,16 +1702,16 @@ QED Theorem update_spec: ∀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 + (0 <= i ⇒ + i < len ls ⇒ + 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 (exfalso >> cooper_tac) >> try_tac ( - pop_last_assum (qspecl_assume [‘i' - 1’, ‘y’]) >> + pop_last_assum (qspecl_assume [‘i' - 1’, ‘y’]) >> fs [] >> pop_assum sg_premise_tac >- cooper_tac >> pop_assum sg_premise_tac >- cooper_tac >> rw []) @@ -1722,6 +1722,13 @@ Proof rw []) QED +Theorem len_update: + ∀ ls i y. len (update ls i y) = len ls +Proof + fs [update_spec] +QED +val _ = BasicProvers.export_rewrites ["len_update"] + Theorem index_update_same: ∀ls i j y. 0 <= i ⇒ @@ -1832,6 +1839,18 @@ Proof sg_dep_rewrite_all_tac index_update_same >- cooper_tac >> fs [] QED +Theorem vec_to_list_vec_update: + ∀ v i x. vec_to_list (vec_update v i x) = update (vec_to_list v) (usize_to_int i) x +Proof + rw [vec_update_def] >> + qspec_assume ‘v’ vec_len_spec >> + qspecl_assume [‘v’, ‘i’, ‘x’] vec_update_eq >> fs [] >> + qspecl_assume [‘vec_to_list v’, ‘usize_to_int i’, ‘x’] update_len >> + sg_dep_rewrite_all_tac mk_vec_axiom >- fs [] >> + fs [] +QED +val _ = export_rewrites ["vec_to_list_vec_update"] + Definition vec_index_fwd_def: vec_index_fwd v i = if usize_to_int i ≤ usize_to_int (vec_len v) diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig index 7e03987b..ae7f083d 100644 --- a/backends/hol4/primitivesTheory.sig +++ b/backends/hol4/primitivesTheory.sig @@ -278,6 +278,7 @@ sig val isize_sub_eq : thm val isize_to_int_int_to_isize_i16_bounds : thm val isize_to_int_int_to_isize_unfold : thm + val len_update : thm val mk_isize_unfold : thm val mk_usize_unfold : thm val mk_vec_unfold : thm @@ -349,6 +350,7 @@ sig val vec_push_back_unfold : thm val vec_to_list_int_bounds : thm val vec_to_list_vec_new : thm + val vec_to_list_vec_update : thm val vec_update_eq : thm val primitives_grammars : type_grammar.grammar * term_grammar.grammar @@ -1907,6 +1909,10 @@ sig if i16_min ≤ n ∧ n ≤ i16_max then n else isize_to_int (int_to_isize n) + [len_update] Theorem + + ⊢ ∀ls i y. len (update ls i y) = len ls + [mk_isize_unfold] Theorem [oracles: DISK_THM] [axioms: isize_bounds] [] @@ -2305,10 +2311,11 @@ sig [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 + len (update ls i y) = len ls ∧ + (0 ≤ i ⇒ + i < 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 @@ -2454,6 +2461,15 @@ sig [oracles: DISK_THM] [axioms: mk_vec_axiom, usize_bounds] [] ⊢ vec_to_list vec_new = [] + [vec_to_list_vec_update] Theorem + + [oracles: DISK_THM] + [axioms: mk_vec_axiom, usize_to_int_bounds, + usize_to_int_int_to_usize, usize_bounds, vec_to_list_num_bounds] [] + ⊢ ∀v i x. + vec_to_list (vec_update v i x) = + update (vec_to_list v) (usize_to_int i) x + [vec_update_eq] Theorem [oracles: DISK_THM] |