diff options
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/hol4/ilistScript.sml | 19 | ||||
| -rw-r--r-- | backends/hol4/ilistTheory.sig | 16 | ||||
| -rw-r--r-- | backends/hol4/primitivesArithScript.sml | 118 | ||||
| -rw-r--r-- | backends/hol4/primitivesArithTheory.sig | 25 | ||||
| -rw-r--r-- | backends/hol4/primitivesLib.sml | 4 |
5 files changed, 180 insertions, 2 deletions
diff --git a/backends/hol4/ilistScript.sml b/backends/hol4/ilistScript.sml index 157b5c00..2183ef77 100644 --- a/backends/hol4/ilistScript.sml +++ b/backends/hol4/ilistScript.sml @@ -64,6 +64,25 @@ Proof exfalso >> cooper_tac QED +Definition drop_def: + drop (i : int) ([] : 'a list) = [] ∧ + drop (i : int) (x :: ls) = + if i < 0 then x :: ls + else if i = 0 then x :: ls + else drop (i - 1) ls +End + +Theorem drop_eq: + (∀ i. drop i [] = []) ∧ + (∀ ls. drop 0 ls = ls) ∧ + (∀ i x ls. drop i (x :: ls) = + if (0 < i) ∨ (0 ≤ i ∧ i ≠ 0) then drop (i - 1) ls + else x :: ls) +Proof + rw [drop_def] >> fs [] >> try_tac int_tac >> + Cases_on ‘ls’ >> fs [drop_def] +QED + Theorem len_eq_LENGTH: ∀ls. len ls = &(LENGTH ls) Proof diff --git a/backends/hol4/ilistTheory.sig b/backends/hol4/ilistTheory.sig index 21545b6e..da7cdbb3 100644 --- a/backends/hol4/ilistTheory.sig +++ b/backends/hol4/ilistTheory.sig @@ -3,12 +3,14 @@ sig type thm = Thm.thm (* Definitions *) + val drop_def : thm val index_def : thm val len_def : thm val update_def : thm (* Theorems *) val append_len_eq : thm + val drop_eq : thm val index_eq : thm val index_eq_EL : thm val len_append : thm @@ -20,6 +22,13 @@ sig (* [primitivesArith] Parent theory of "ilist" + [drop_def] Definition + + ⊢ (∀i. drop i [] = []) ∧ + ∀i x ls. + drop i (x::ls) = + if i < 0 then x::ls else if i = 0 then x::ls else drop (i − 1) ls + [index_def] Definition ⊢ ∀i x ls. @@ -46,6 +55,13 @@ sig ∀l1 l2 l1' l2'. len l2 = len l2' ⇒ (l1 ⧺ l2 = l1' ⧺ l2' ⇔ l1 = l1' ∧ l2 = l2') + [drop_eq] Theorem + + ⊢ (∀i. drop i [] = []) ∧ (∀ls. drop 0 ls = ls) ∧ + ∀i x ls. + drop i (x::ls) = + if 0 < i ∨ 0 ≤ i ∧ i ≠ 0 then drop (i − 1) ls else x::ls + [index_eq] Theorem ⊢ (∀x ls. index 0 (x::ls) = x) ∧ diff --git a/backends/hol4/primitivesArithScript.sml b/backends/hol4/primitivesArithScript.sml index 727fc8c2..decb1109 100644 --- a/backends/hol4/primitivesArithScript.sml +++ b/backends/hol4/primitivesArithScript.sml @@ -162,6 +162,12 @@ Proof metis_tac [INT_LE_ADDR] QED +Theorem pos_div_pos_ge: + !(x y d : int). 0 <= x ==> 0 <= y ==> 0 < d ==> x >= y ==> x / d >= y / d +Proof + metis_tac [pos_div_pos_le, ge_eq_le] +QED + Theorem pos_div_pos_le_init: !(x y : int). 0 <= x ==> 0 < y ==> x / y <= x Proof @@ -223,4 +229,116 @@ Proof metis_tac [pos_mod_pos_is_pos, pos_mod_pos_lt] QED +Theorem mul_pos_left_le: + ∀ (a x y : int). 0 ≤ a ⇒ x ≤ y ⇒ a * x ≤ a * y +Proof + rw [] >> Cases_on ‘a = 0’ >> fs [] >> + sg ‘0 < a’ >- cooper_tac >> + metis_tac [integerTheory.INT_LE_MONO] +QED + +Theorem mul_pos_right_le: + ∀ (a x y : int). 0 ≤ a ⇒ x ≤ y ⇒ x * a ≤ y * a +Proof + rw [mul_pos_left_le, integerTheory.INT_MUL_COMM] +QED + +Theorem mul_pos_left_lt: + ∀ (a x y : int). 0 < a ⇒ x < y ⇒ a * x < a * y +Proof + metis_tac [integerTheory.INT_LT_MONO] +QED + +Theorem mul_pos_right_lt: + ∀ (a x y : int). 0 < a ⇒ x < y ⇒ x * a < y * a +Proof + metis_tac [mul_pos_left_lt, integerTheory.INT_MUL_COMM] +QED + +Theorem pos_mul_left_pos_le: + ∀ a x. 0 < a ⇒ 0 ≤ x ⇒ x ≤ a * x +Proof + rw [] >> + Cases_on ‘a = 1’ >> fs [] >> + sg ‘0 ≤ (a - 1) * x’ >- (irule pos_mul_pos_is_pos >> int_tac) >> + sg ‘x ≤ x + (a - 1) * x’ >- fs [] >> + sg ‘a * x = 1 * x + (a - 1) * x’ >- fs [GSYM integerTheory.INT_RDISTRIB] >> + fs [] +QED + +Theorem pos_mul_right_pos_le: + ∀ a x. 0 < a ⇒ 0 ≤ x ⇒ x ≤ x * a +Proof + metis_tac [pos_mul_left_pos_le, integerTheory.INT_MUL_COMM] +QED + +Theorem pos_mul_left_pos_lt: + ∀ a x. 1 < a ⇒ 0 < x ⇒ x < a * x +Proof + rw [] >> + sg ‘a * x = 1 * x + (a - 1) * x’ + >- (fs [GSYM integerTheory.INT_RDISTRIB]) >> + fs [] >> + sg ‘(a − 1) * x = 1 * x + (a - 2) * x’ + >- ( + fs [GSYM integerTheory.INT_RDISTRIB] >> + sg ‘1 + (a − 2) = a - 1’ >- int_tac >> + fs [] + ) >> + fs [] >> + sg ‘0 ≤ (a − 2) * x’ >- (irule pos_mul_pos_is_pos >> int_tac) >> + int_tac +QED + +Theorem pos_mul_right_pos_lt: + ∀ a x. 1 < a ⇒ 0 < x ⇒ x < x * a +Proof + metis_tac [pos_mul_left_pos_lt, integerTheory.INT_MUL_COMM] +QED + +Theorem pos_div_pos_mul_le: + ∀ x y. 0 ≤ x ⇒ 0 < y ⇒ (x / y) * y ≤ x +Proof + rw [] >> + qspec_assume ‘y’ integerTheory.INT_DIVISION >> + sg ‘y ≠ 0 ∧ ~(y < 0)’ >- int_tac >> fs [] >> + first_x_assum (qspec_assume ‘x’) >> + fs [] >> + (* TODO: int_tac loops here *) + cooper_tac +QED + +Theorem pos_mul_pos_div_pos_decompose: + ∀ x y z. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 < z ⇒ x / z + y / z ≤ (x + y) / z +Proof + rw [] >> + sg ‘z ≠ 0’ >- int_tac >> + sg ‘(x / z * z + x % z) + (y / z * z + y % z) = (x + y) / z * z + (x + y) % z’ >- metis_tac [integerTheory.INT_DIVISION] >> + sg ‘(x + y) % z = ((x % z) + (y % z)) % z’ >- metis_tac [integerTheory.INT_MOD_PLUS] >> + sg ‘0 ≤ (x % z) ∧ 0 ≤ (y % z)’ >- metis_tac [pos_mod_pos_is_pos] >> + sg ‘0 ≤ (x % z) + (y % z)’ >- int_tac >> + sg ‘((x % z) + (y % z)) % z ≤ (x % z) + (y % z)’ >- metis_tac [pos_mod_pos_le_init] >> + sg ‘x / z * z + y / z * z ≤ (x + y) / z * z’ >- int_tac >> + sg ‘x / z * z + y / z * z = (x / z + y / z) * z’ >- fs [integerTheory.INT_RDISTRIB] >> fs [] >> + sg ‘0 ≤ x / z’ >- (irule pos_div_pos_is_pos >> fs []) >> + sg ‘0 ≤ y / z’ >- (irule pos_div_pos_is_pos >> fs []) >> + sg ‘0 ≤ (x + y) / z’ >- (irule pos_div_pos_is_pos >> fs []) >> + sg ‘(x / z + y / z) * z / z ≤ (x + y) / z * z / z’ + >- ( + irule pos_div_pos_le >> fs [] >> + rw [] >> irule pos_mul_pos_is_pos >> fs []) >> + imp_res_tac integerTheory.INT_DIV_RMUL >> + metis_tac [] +QED + +Theorem pos_mul_2_div_pos_decompose: + ∀ x y. 0 ≤ x ⇒ 0 < y ⇒ x / y + x / y ≤ x * 2 / y +Proof + rw [] >> + qspecl_assume [‘x’, ‘x’, ‘y’] pos_mul_pos_div_pos_decompose >> gvs [] >> + sg ‘x * 2 = (x * 1) + (x * 1)’ + >- (pure_rewrite_tac [GSYM integerTheory.INT_LDISTRIB] >> fs []) >> + fs [] +QED + val _ = export_theory () diff --git a/backends/hol4/primitivesArithTheory.sig b/backends/hol4/primitivesArithTheory.sig index 531797ac..84b9b67a 100644 --- a/backends/hol4/primitivesArithTheory.sig +++ b/backends/hol4/primitivesArithTheory.sig @@ -14,6 +14,8 @@ sig val int_of_num_inj : thm val le_eq_ge : thm val lt_eq_gt : thm + val mul_pos_left_le : thm + val mul_pos_right_le : thm val not_ge_eq_lt : thm val not_gt_eq_le : thm val not_le_eq_gt : thm @@ -23,11 +25,14 @@ sig val pos_div_pos_is_pos : thm val pos_div_pos_le : thm val pos_div_pos_le_init : thm + val pos_div_pos_mul_le : thm val pos_mod_pos_ineqs : thm val pos_mod_pos_is_pos : thm val pos_mod_pos_le_init : thm val pos_mod_pos_lt : thm + val pos_mul_left_pos_le : thm val pos_mul_pos_is_pos : thm + val pos_mul_right_pos_le : thm val primitivesArith_grammars : type_grammar.grammar * term_grammar.grammar (* @@ -79,6 +84,14 @@ sig ⊢ ∀x y. x < y ⇔ y > x + [mul_pos_left_le] 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 + [not_ge_eq_lt] Theorem ⊢ ∀x y. ¬(x ≥ y) ⇔ x < y @@ -115,6 +128,10 @@ sig ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x / y ≤ x + [pos_div_pos_mul_le] Theorem + + ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x / y * y ≤ x + [pos_mod_pos_ineqs] Theorem ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x % y ∧ x % y < y @@ -131,10 +148,18 @@ sig ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x % y < y + [pos_mul_left_pos_le] Theorem + + ⊢ ∀a x. 0 < a ⇒ 0 ≤ x ⇒ x ≤ a * x + [pos_mul_pos_is_pos] Theorem ⊢ ∀x y. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 ≤ x * y + [pos_mul_right_pos_le] Theorem + + ⊢ ∀a x. 0 < a ⇒ 0 ≤ x ⇒ x ≤ x * a + *) end diff --git a/backends/hol4/primitivesLib.sml b/backends/hol4/primitivesLib.sml index 0a89be4c..a90f1e32 100644 --- a/backends/hol4/primitivesLib.sml +++ b/backends/hol4/primitivesLib.sml @@ -272,7 +272,7 @@ fun get_spec_app (t : term) : term = fun get_key_normalize_thm (th : thm) : const_name * thm = let (* Transform the theroem a bit before storing it *) - val th = SPEC_ALL th; + val th = (SPEC_ALL o BETA_RULE o PURE_REWRITE_RULE [LET_DEF]) th; (* Retrieve the app ([f x0 ... xn]) *) val f = get_spec_app (concl th); (* Retrieve the function name *) @@ -532,7 +532,7 @@ val progress : tactic = val thl = case Redblackmap.peek (get_spec_thms (), fname) of NONE => asms_thl - | SOME spec => spec :: asms_thl; + | SOME spec => asms_thl @ [spec]; val _ = if null thl then raise (failwith "progress: could not find a suitable theorem to apply") |