huffman@45224: (* Title: HOL/ex/Simproc_Tests.thy
huffman@45224: Author: Brian Huffman
huffman@45224: *)
huffman@45224:
huffman@45224: header {* Testing of arithmetic simprocs *}
huffman@45224:
huffman@45224: theory Simproc_Tests
huffman@45462: imports Main
huffman@45224: begin
huffman@45224:
huffman@45224: text {*
huffman@45224: This theory tests the various simprocs defined in
huffman@45224: @{file "~~/src/HOL/Numeral_Simprocs.thy"}. Many of the tests
huffman@45224: are derived from commented-out code originally found in
huffman@45224: @{file "~~/src/HOL/Tools/numeral_simprocs.ML"}.
huffman@45224: *}
huffman@45224:
huffman@45224: subsection {* ML bindings *}
huffman@45224:
huffman@45224: ML {*
huffman@45224: fun test ps = CHANGED (asm_simp_tac (HOL_basic_ss addsimprocs ps) 1)
huffman@45224: *}
huffman@45224:
huffman@45464: subsection {* Abelian group cancellation simprocs *}
huffman@45464:
huffman@45464: notepad begin
huffman@45464: fix a b c u :: "'a::ab_group_add"
huffman@45464: {
huffman@45464: assume "(a + 0) - (b + 0) = u" have "(a + c) - (b + c) = u"
huffman@45464: by (tactic {* test [@{simproc abel_cancel_sum}] *}) fact
huffman@45464: next
huffman@45464: assume "a + 0 = b + 0" have "a + c = b + c"
huffman@45464: by (tactic {* test [@{simproc abel_cancel_relation}] *}) fact
huffman@45464: }
huffman@45464: end
huffman@45464: (* TODO: more tests for Groups.abel_cancel_{sum,relation} *)
huffman@45224:
huffman@45224: subsection {* @{text int_combine_numerals} *}
huffman@45224:
huffman@45464: (* FIXME: int_combine_numerals often unnecessarily regroups addition
huffman@45464: and rewrites subtraction to negation. Ideally it should behave more
huffman@45464: like Groups.abel_cancel_sum, preserving the shape of terms as much as
huffman@45464: possible. *)
huffman@45464:
huffman@45435: notepad begin
huffman@45435: fix a b c d oo uu i j k l u v w x y z :: "'a::number_ring"
huffman@45435: {
huffman@45464: assume "a + - b = u" have "(a + c) - (b + c) = u"
huffman@45464: by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45464: next
huffman@45435: assume "10 + (2 * l + oo) = uu"
huffman@45435: have "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = uu"
huffman@45435: by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435: next
huffman@45435: assume "-3 + (i + (j + k)) = y"
huffman@45435: have "(i + j + 12 + k) - 15 = y"
huffman@45435: by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435: next
huffman@45435: assume "7 + (i + (j + k)) = y"
huffman@45435: have "(i + j + 12 + k) - 5 = y"
huffman@45435: by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435: next
huffman@45435: assume "-4 * (u * v) + (2 * x + y) = w"
huffman@45435: have "(2*x - (u*v) + y) - v*3*u = w"
huffman@45435: by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435: next
huffman@45437: assume "2 * x * u * v + y = w"
huffman@45435: have "(2*x*u*v + (u*v)*4 + y) - v*u*4 = w"
huffman@45435: by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435: next
huffman@45435: assume "3 * (u * v) + (2 * x * u * v + y) = w"
huffman@45435: have "(2*x*u*v + (u*v)*4 + y) - v*u = w"
huffman@45435: by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435: next
huffman@45435: assume "-3 * (u * v) + (- (x * u * v) + - y) = w"
huffman@45435: have "u*v - (x*u*v + (u*v)*4 + y) = w"
huffman@45435: by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435: next
huffman@45437: assume "a + - c = d"
huffman@45435: have "a + -(b+c) + b = d"
huffman@45435: apply (simp only: minus_add_distrib)
huffman@45435: by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435: next
huffman@45435: assume "-2 * b + (a + - c) = d"
huffman@45435: have "a + -(b+c) - b = d"
huffman@45435: apply (simp only: minus_add_distrib)
huffman@45435: by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435: next
huffman@45435: assume "-7 + (i + (j + (k + (- u + - y)))) = z"
huffman@45435: have "(i + j + -2 + k) - (u + 5 + y) = z"
huffman@45435: by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435: next
huffman@45435: assume "-27 + (i + (j + k)) = y"
huffman@45435: have "(i + j + -12 + k) - 15 = y"
huffman@45435: by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435: next
huffman@45435: assume "27 + (i + (j + k)) = y"
huffman@45435: have "(i + j + 12 + k) - -15 = y"
huffman@45435: by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435: next
huffman@45435: assume "3 + (i + (j + k)) = y"
huffman@45435: have "(i + j + -12 + k) - -15 = y"
huffman@45435: by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435: }
huffman@45435: end
huffman@45224:
huffman@45224: subsection {* @{text inteq_cancel_numerals} *}
huffman@45224:
huffman@45435: notepad begin
huffman@45435: fix i j k u vv w y z w' y' z' :: "'a::number_ring"
huffman@45435: {
huffman@45437: assume "u = 0" have "2*u = u"
huffman@45435: by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
huffman@45224: (* conclusion matches Rings.ring_1_no_zero_divisors_class.mult_cancel_right2 *)
huffman@45435: next
huffman@45435: assume "i + (j + k) = 3 + (u + y)"
huffman@45435: have "(i + j + 12 + k) = u + 15 + y"
huffman@45435: by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
huffman@45435: next
huffman@45435: assume "7 + (j + (i + k)) = y"
huffman@45435: have "(i + j*2 + 12 + k) = j + 5 + y"
huffman@45435: by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
huffman@45435: next
huffman@45435: assume "u + (6*z + (4*y + 6*w)) = 6*z' + (4*y' + (6*w' + vv))"
huffman@45435: have "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + vv"
huffman@45435: by (tactic {* test [@{simproc int_combine_numerals}, @{simproc inteq_cancel_numerals}] *}) fact
huffman@45435: }
huffman@45435: end
huffman@45224:
huffman@45224: subsection {* @{text intless_cancel_numerals} *}
huffman@45224:
huffman@45435: notepad begin
huffman@45435: fix b c i j k u y :: "'a::{linordered_idom,number_ring}"
huffman@45435: {
huffman@45435: assume "y < 2 * b" have "y - b < b"
huffman@45435: by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
huffman@45435: next
huffman@45435: assume "c + y < 4 * b" have "y - (3*b + c) < b - 2*c"
huffman@45435: by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
huffman@45435: next
huffman@45435: assume "i + (j + k) < 8 + (u + y)"
huffman@45435: have "(i + j + -3 + k) < u + 5 + y"
huffman@45435: by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
huffman@45435: next
huffman@45435: assume "9 + (i + (j + k)) < u + y"
huffman@45435: have "(i + j + 3 + k) < u + -6 + y"
huffman@45435: by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
huffman@45435: }
huffman@45435: end
huffman@45224:
huffman@45224: subsection {* @{text ring_eq_cancel_numeral_factor} *}
huffman@45224:
huffman@45435: notepad begin
huffman@45435: fix x y :: "'a::{idom,ring_char_0,number_ring}"
huffman@45435: {
huffman@45435: assume "3*x = 4*y" have "9*x = 12 * y"
huffman@45435: by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "-3*x = 4*y" have "-99*x = 132 * y"
huffman@45435: by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "111*x = -44*y" have "999*x = -396 * y"
huffman@45435: by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "11*x = 9*y" have "-99*x = -81 * y"
huffman@45435: by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
huffman@45435: next
huffman@45437: assume "2*x = y" have "-2 * x = -1 * y"
huffman@45435: by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
huffman@45435: next
huffman@45437: assume "2*x = y" have "-2 * x = -y"
huffman@45435: by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
huffman@45435: }
huffman@45435: end
huffman@45224:
huffman@45224: subsection {* @{text int_div_cancel_numeral_factors} *}
huffman@45224:
huffman@45435: notepad begin
huffman@45435: fix x y z :: "'a::{semiring_div,ring_char_0,number_ring}"
huffman@45435: {
huffman@45435: assume "(3*x) div (4*y) = z" have "(9*x) div (12*y) = z"
huffman@45435: by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
huffman@45435: next
huffman@45435: assume "(-3*x) div (4*y) = z" have "(-99*x) div (132*y) = z"
huffman@45435: by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
huffman@45435: next
huffman@45435: assume "(111*x) div (-44*y) = z" have "(999*x) div (-396*y) = z"
huffman@45435: by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
huffman@45435: next
huffman@45435: assume "(11*x) div (9*y) = z" have "(-99*x) div (-81*y) = z"
huffman@45435: by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
huffman@45435: next
huffman@45437: assume "(2*x) div y = z"
huffman@45435: have "(-2 * x) div (-1 * y) = z"
huffman@45435: by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
huffman@45435: }
huffman@45435: end
huffman@45224:
huffman@45224: subsection {* @{text ring_less_cancel_numeral_factor} *}
huffman@45224:
huffman@45435: notepad begin
huffman@45435: fix x y :: "'a::{linordered_idom,number_ring}"
huffman@45435: {
huffman@45435: assume "3*x < 4*y" have "9*x < 12 * y"
huffman@45435: by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "-3*x < 4*y" have "-99*x < 132 * y"
huffman@45435: by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "111*x < -44*y" have "999*x < -396 * y"
huffman@45435: by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "9*y < 11*x" have "-99*x < -81 * y"
huffman@45435: by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
huffman@45435: next
huffman@45437: assume "y < 2*x" have "-2 * x < -y"
huffman@45435: by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
huffman@45435: next
huffman@45437: assume "23*y < x" have "-x < -23 * y"
huffman@45435: by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
huffman@45435: }
huffman@45435: end
huffman@45224:
huffman@45224: subsection {* @{text ring_le_cancel_numeral_factor} *}
huffman@45224:
huffman@45435: notepad begin
huffman@45435: fix x y :: "'a::{linordered_idom,number_ring}"
huffman@45435: {
huffman@45435: assume "3*x \ 4*y" have "9*x \ 12 * y"
huffman@45435: by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "-3*x \ 4*y" have "-99*x \ 132 * y"
huffman@45435: by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "111*x \ -44*y" have "999*x \ -396 * y"
huffman@45435: by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "9*y \ 11*x" have "-99*x \ -81 * y"
huffman@45435: by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
huffman@45435: next
huffman@45437: assume "y \ 2*x" have "-2 * x \ -1 * y"
huffman@45435: by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
huffman@45435: next
huffman@45437: assume "23*y \ x" have "-x \ -23 * y"
huffman@45435: by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
huffman@45435: next
huffman@45437: assume "y \ 0" have "0 \ y * -2"
huffman@45435: by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
huffman@45435: next
huffman@45437: assume "- x \ y" have "- (2 * x) \ 2*y"
huffman@45435: by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
huffman@45435: }
huffman@45435: end
huffman@45224:
huffman@45285: subsection {* @{text divide_cancel_numeral_factor} *}
huffman@45224:
huffman@45435: notepad begin
huffman@45435: fix x y z :: "'a::{field_inverse_zero,ring_char_0,number_ring}"
huffman@45435: {
huffman@45435: assume "(3*x) / (4*y) = z" have "(9*x) / (12 * y) = z"
huffman@45435: by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "(-3*x) / (4*y) = z" have "(-99*x) / (132 * y) = z"
huffman@45435: by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "(111*x) / (-44*y) = z" have "(999*x) / (-396 * y) = z"
huffman@45435: by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "(11*x) / (9*y) = z" have "(-99*x) / (-81 * y) = z"
huffman@45435: by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
huffman@45435: next
huffman@45437: assume "(2*x) / y = z" have "(-2 * x) / (-1 * y) = z"
huffman@45435: by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
huffman@45435: }
huffman@45435: end
huffman@45224:
huffman@45224: subsection {* @{text ring_eq_cancel_factor} *}
huffman@45224:
huffman@45435: notepad begin
huffman@45435: fix a b c d k x y :: "'a::idom"
huffman@45435: {
huffman@45435: assume "k = 0 \ x = y" have "x*k = k*y"
huffman@45435: by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "k = 0 \ 1 = y" have "k = k*y"
huffman@45435: by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "b = 0 \ a*c = 1" have "a*(b*c) = b"
huffman@45435: by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "a = 0 \ b = 0 \ c = d*x" have "a*(b*c) = d*b*(x*a)"
huffman@45435: by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "k = 0 \ x = y" have "x*k = k*y"
huffman@45435: by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "k = 0 \ 1 = y" have "k = k*y"
huffman@45435: by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
huffman@45435: }
huffman@45435: end
huffman@45224:
huffman@45224: subsection {* @{text int_div_cancel_factor} *}
huffman@45224:
huffman@45435: notepad begin
huffman@45435: fix a b c d k uu x y :: "'a::semiring_div"
huffman@45435: {
huffman@45435: assume "(if k = 0 then 0 else x div y) = uu"
huffman@45435: have "(x*k) div (k*y) = uu"
huffman@45435: by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "(if k = 0 then 0 else 1 div y) = uu"
huffman@45435: have "(k) div (k*y) = uu"
huffman@45435: by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "(if b = 0 then 0 else a * c) = uu"
huffman@45435: have "(a*(b*c)) div b = uu"
huffman@45435: by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu"
huffman@45435: have "(a*(b*c)) div (d*b*(x*a)) = uu"
huffman@45435: by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
huffman@45435: }
huffman@45435: end
huffman@45224:
huffman@45224: subsection {* @{text divide_cancel_factor} *}
huffman@45224:
huffman@45435: notepad begin
huffman@45435: fix a b c d k uu x y :: "'a::field_inverse_zero"
huffman@45435: {
huffman@45435: assume "(if k = 0 then 0 else x / y) = uu"
huffman@45435: have "(x*k) / (k*y) = uu"
huffman@45435: by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "(if k = 0 then 0 else 1 / y) = uu"
huffman@45435: have "(k) / (k*y) = uu"
huffman@45435: by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "(if b = 0 then 0 else a * c / 1) = uu"
huffman@45435: have "(a*(b*c)) / b = uu"
huffman@45435: by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "(if a = 0 then 0 else if b = 0 then 0 else c / (d * x)) = uu"
huffman@45435: have "(a*(b*c)) / (d*b*(x*a)) = uu"
huffman@45435: by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
huffman@45435: }
huffman@45435: end
huffman@45224:
huffman@45462: lemma
huffman@45462: fixes a b c d x y z :: "'a::linordered_field_inverse_zero"
huffman@45462: shows "a*(b*c)/(y*z) = d*(b)*(x*a)/z"
huffman@45224: oops -- "FIXME: need simproc to cover this case"
huffman@45224:
huffman@45224: subsection {* @{text linordered_ring_less_cancel_factor} *}
huffman@45224:
huffman@45435: notepad begin
huffman@45435: fix x y z :: "'a::linordered_idom"
huffman@45435: {
huffman@45435: assume "0 < z \ x < y" have "0 < z \ x*z < y*z"
huffman@45435: by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "0 < z \ x < y" have "0 < z \ x*z < z*y"
huffman@45435: by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "0 < z \ x < y" have "0 < z \ z*x < y*z"
huffman@45435: by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "0 < z \ x < y" have "0 < z \ z*x < z*y"
huffman@45435: by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
huffman@46240: next
huffman@46240: txt "This simproc now uses the simplifier to prove that terms to
huffman@46240: be canceled are positive/negative."
huffman@46240: assume z_pos: "0 < z"
huffman@46240: assume "x < y" have "z*x < z*y"
huffman@46240: by (tactic {* CHANGED (asm_simp_tac (HOL_basic_ss
huffman@46240: addsimprocs [@{simproc linordered_ring_less_cancel_factor}]
huffman@46240: addsimps [@{thm z_pos}]) 1) *}) fact
huffman@45435: }
huffman@45435: end
huffman@45224:
huffman@45224: subsection {* @{text linordered_ring_le_cancel_factor} *}
huffman@45224:
huffman@45435: notepad begin
huffman@45435: fix x y z :: "'a::linordered_idom"
huffman@45435: {
huffman@45435: assume "0 < z \ x \ y" have "0 < z \ x*z \ y*z"
huffman@45435: by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact
huffman@45435: next
huffman@45435: assume "0 < z \ x \ y" have "0 < z \ z*x \ z*y"
huffman@45435: by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact
huffman@45435: }
huffman@45435: end
huffman@45224:
huffman@45224: subsection {* @{text field_combine_numerals} *}
huffman@45224:
huffman@45435: notepad begin
huffman@45437: fix x y z uu :: "'a::{field_inverse_zero,ring_char_0,number_ring}"
huffman@45435: {
huffman@45435: assume "5 / 6 * x = uu" have "x / 2 + x / 3 = uu"
huffman@45435: by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
huffman@45435: next
huffman@45435: assume "6 / 9 * x + y = uu" have "x / 3 + y + x / 3 = uu"
huffman@45435: by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
huffman@45435: next
huffman@45435: assume "9 / 9 * x = uu" have "2 * x / 3 + x / 3 = uu"
huffman@45435: by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
huffman@45437: next
huffman@45437: assume "y + z = uu"
huffman@45437: have "x / 2 + y - 3 * x / 6 + z = uu"
huffman@45437: by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
huffman@45437: next
huffman@45437: assume "1 / 15 * x + y = uu"
huffman@45437: have "7 * x / 5 + y - 4 * x / 3 = uu"
huffman@45437: by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
huffman@45435: }
huffman@45435: end
huffman@45224:
huffman@45462: lemma
huffman@45462: fixes x :: "'a::{linordered_field_inverse_zero,number_ring}"
huffman@45462: shows "2/3 * x + x / 3 = uu"
huffman@45284: apply (tactic {* test [@{simproc field_combine_numerals}] *})?
huffman@45224: oops -- "FIXME: test fails"
huffman@45224:
huffman@45462: subsection {* @{text nat_combine_numerals} *}
huffman@45462:
huffman@45462: notepad begin
huffman@45462: fix i j k m n u :: nat
huffman@45462: {
huffman@45462: assume "4*k = u" have "k + 3*k = u"
huffman@45462: by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
huffman@45462: next
huffman@45530: (* FIXME "Suc (i + 3) \ i + 4" *)
huffman@45462: assume "4 * Suc 0 + i = u" have "Suc (i + 3) = u"
huffman@45462: by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
huffman@45462: next
huffman@45530: (* FIXME "Suc (i + j + 3 + k) \ i + j + 4 + k" *)
huffman@45462: assume "4 * Suc 0 + (i + (j + k)) = u" have "Suc (i + j + 3 + k) = u"
huffman@45462: by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
huffman@45462: next
huffman@45462: assume "2 * j + 4 * k = u" have "k + j + 3*k + j = u"
huffman@45462: by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
huffman@45462: next
huffman@45462: assume "6 * Suc 0 + (5 * (i * j) + (4 * k + i)) = u"
huffman@45462: have "Suc (j*i + i + k + 5 + 3*k + i*j*4) = u"
huffman@45462: by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
huffman@45462: next
huffman@45462: assume "5 * (m * n) = u" have "(2*n*m) + (3*(m*n)) = u"
huffman@45462: by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
huffman@45462: }
huffman@45462: end
huffman@45462:
huffman@45462: (*negative numerals: FAIL*)
huffman@45462: lemma "Suc (i + j + -3 + k) = u"
huffman@45462: apply (tactic {* test [@{simproc nat_combine_numerals}] *})?
huffman@45462: oops
huffman@45462:
huffman@45436: subsection {* @{text nateq_cancel_numerals} *}
huffman@45436:
huffman@45436: notepad begin
huffman@45436: fix i j k l oo u uu vv w y z w' y' z' :: "nat"
huffman@45436: {
huffman@45462: assume "Suc 0 * u = 0" have "2*u = u"
huffman@45436: by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "Suc 0 * u = Suc 0" have "2*u = Suc (u)"
huffman@45436: by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "i + (j + k) = 3 * Suc 0 + (u + y)"
huffman@45436: have "(i + j + 12 + k) = u + 15 + y"
huffman@45436: by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "7 * Suc 0 + (i + (j + k)) = u + y"
huffman@45436: have "(i + j + 12 + k) = u + 5 + y"
huffman@45436: by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "11 * Suc 0 + (i + (j + k)) = u + y"
huffman@45436: have "(i + j + 12 + k) = Suc (u + y)"
huffman@45436: by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "i + (j + k) = 2 * Suc 0 + (u + y)"
huffman@45436: have "(i + j + 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))"
huffman@45436: by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "Suc 0 * u + (2 * y + 3 * z) = Suc 0"
huffman@45436: have "2*y + 3*z + 2*u = Suc (u)"
huffman@45436: by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "Suc 0 * u + (2 * y + (3 * z + (6 * w + (2 * y + 3 * z)))) = Suc 0"
huffman@45436: have "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = Suc (u)"
huffman@45436: by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "Suc 0 * u + (2 * y + (3 * z + (6 * w + (2 * y + 3 * z)))) =
huffman@45436: 2 * y' + (3 * z' + (6 * w' + (2 * y' + (3 * z' + vv))))"
huffman@45436: have "2*y + 3*z + 6*w + 2*y + 3*z + 2*u =
huffman@45436: 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + vv"
huffman@45436: by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "2 * u + (2 * z + (5 * Suc 0 + 2 * y)) = vv"
huffman@45436: have "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)"
huffman@45436: by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436: }
huffman@45224: end
huffman@45436:
huffman@45436: subsection {* @{text natless_cancel_numerals} *}
huffman@45436:
huffman@45436: notepad begin
huffman@45436: fix length :: "'a \ nat" and l1 l2 xs :: "'a" and f :: "nat \ 'a"
huffman@45436: fix c i j k l oo u uu vv w y z w' y' z' :: "nat"
huffman@45436: {
huffman@45436: assume "0 < j" have "(2*length xs < 2*length xs + j)"
huffman@45436: by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "0 < j" have "(2*length xs < length xs * 2 + j)"
huffman@45436: by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "i + (j + k) < u + y"
huffman@45436: have "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))"
huffman@45436: by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "0 < Suc 0 * (m * n) + u" have "(2*n*m) < (3*(m*n)) + u"
huffman@45436: by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: (* FIXME: negative numerals fail
huffman@45436: have "(i + j + -23 + (k::nat)) < u + 15 + y"
huffman@45436: apply (tactic {* test [@{simproc natless_cancel_numerals}] *})?
huffman@45436: sorry
huffman@45436: have "(i + j + 3 + (k::nat)) < u + -15 + y"
huffman@45436: apply (tactic {* test [@{simproc natless_cancel_numerals}] *})?
huffman@45436: sorry*)
huffman@45436: }
huffman@45436: end
huffman@45436:
huffman@45436: subsection {* @{text natle_cancel_numerals} *}
huffman@45436:
huffman@45436: notepad begin
huffman@45436: fix length :: "'a \ nat" and l2 l3 :: "'a" and f :: "nat \ 'a"
huffman@45436: fix c e i j k l oo u uu vv w y z w' y' z' :: "nat"
huffman@45436: {
huffman@45436: assume "u + y \ 36 * Suc 0 + (i + (j + k))"
huffman@45436: have "Suc (Suc (Suc (Suc (Suc (u + y))))) \ ((i + j) + 41 + k)"
huffman@45436: by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "5 * Suc 0 + (case length (f c) of 0 \ 0 | Suc k \ k) = 0"
huffman@45436: have "(Suc (Suc (Suc (Suc (Suc (Suc (case length (f c) of 0 => 0 | Suc k => k)))))) \ Suc 0)"
huffman@45436: by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "6 + length l2 = 0" have "Suc (Suc (Suc (Suc (Suc (Suc (length l1 + length l2)))))) \ length l1"
huffman@45436: by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "5 + length l3 = 0"
huffman@45436: have "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length l3)))))) \ length (compT P E A ST mxr e))"
huffman@45436: by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "5 + length (compT P E (A \ A' e) ST mxr c) = 0"
huffman@45436: have "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length (compT P E (A Un A' e) ST mxr c))))))) \ length (compT P E A ST mxr e))"
huffman@45436: by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
huffman@45436: }
huffman@45436: end
huffman@45436:
huffman@45436: subsection {* @{text natdiff_cancel_numerals} *}
huffman@45436:
huffman@45436: notepad begin
huffman@45436: fix length :: "'a \ nat" and l2 l3 :: "'a" and f :: "nat \ 'a"
huffman@45436: fix c e i j k l oo u uu vv v w x y z zz w' y' z' :: "nat"
huffman@45436: {
huffman@45436: assume "i + (j + k) - 3 * Suc 0 = y" have "(i + j + 12 + k) - 15 = y"
huffman@45436: by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "7 * Suc 0 + (i + (j + k)) - 0 = y" have "(i + j + 12 + k) - 5 = y"
huffman@45436: by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "u - Suc 0 * Suc 0 = y" have "Suc u - 2 = y"
huffman@45436: by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "Suc 0 * Suc 0 + u - 0 = y" have "Suc (Suc (Suc u)) - 2 = y"
huffman@45436: by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "Suc 0 * Suc 0 + (i + (j + k)) - 0 = y"
huffman@45436: have "(i + j + 2 + k) - 1 = y"
huffman@45436: by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "i + (j + k) - Suc 0 * Suc 0 = y"
huffman@45436: have "(i + j + 1 + k) - 2 = y"
huffman@45436: by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "2 * x + y - 2 * (u * v) = w"
huffman@45436: have "(2*x + (u*v) + y) - v*3*u = w"
huffman@45436: by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "2 * x * u * v + (5 + y) - 0 = w"
huffman@45436: have "(2*x*u*v + 5 + (u*v)*4 + y) - v*u*4 = w"
huffman@45436: by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "3 * (u * v) + (2 * x * u * v + y) - 0 = w"
huffman@45436: have "(2*x*u*v + (u*v)*4 + y) - v*u = w"
huffman@45436: by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "3 * u + (2 + (2 * x * u * v + y)) - 0 = w"
huffman@45436: have "Suc (Suc (2*x*u*v + u*4 + y)) - u = w"
huffman@45436: by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "Suc (Suc 0 * (u * v)) - 0 = w"
huffman@45436: have "Suc ((u*v)*4) - v*3*u = w"
huffman@45436: by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "2 - 0 = w" have "Suc (Suc ((u*v)*3)) - v*3*u = w"
huffman@45436: by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "17 * Suc 0 + (i + (j + k)) - (u + y) = zz"
huffman@45436: have "(i + j + 32 + k) - (u + 15 + y) = zz"
huffman@45436: by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: assume "u + y - 0 = v" have "Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v"
huffman@45436: by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436: next
huffman@45436: (* FIXME: negative numerals fail
huffman@45436: have "(i + j + -12 + k) - 15 = y"
huffman@45436: apply (tactic {* test [@{simproc natdiff_cancel_numerals}] *})?
huffman@45436: sorry
huffman@45436: have "(i + j + 12 + k) - -15 = y"
huffman@45436: apply (tactic {* test [@{simproc natdiff_cancel_numerals}] *})?
huffman@45436: sorry
huffman@45436: have "(i + j + -12 + k) - -15 = y"
huffman@45436: apply (tactic {* test [@{simproc natdiff_cancel_numerals}] *})?
huffman@45436: sorry*)
huffman@45436: }
huffman@45436: end
huffman@45436:
huffman@45462: subsection {* Factor-cancellation simprocs for type @{typ nat} *}
huffman@45462:
huffman@45462: text {* @{text nat_eq_cancel_factor}, @{text nat_less_cancel_factor},
huffman@45462: @{text nat_le_cancel_factor}, @{text nat_divide_cancel_factor}, and
huffman@45462: @{text nat_dvd_cancel_factor}. *}
huffman@45462:
huffman@45462: notepad begin
huffman@45462: fix a b c d k x y uu :: nat
huffman@45462: {
huffman@45462: assume "k = 0 \ x = y" have "x*k = k*y"
huffman@45462: by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
huffman@45462: next
huffman@45462: assume "k = 0 \ Suc 0 = y" have "k = k*y"
huffman@45462: by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
huffman@45462: next
huffman@45462: assume "b = 0 \ a * c = Suc 0" have "a*(b*c) = b"
huffman@45462: by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
huffman@45462: next
huffman@45462: assume "a = 0 \ b = 0 \ c = d * x" have "a*(b*c) = d*b*(x*a)"
huffman@45462: by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
huffman@45462: next
huffman@45462: assume "0 < k \ x < y" have "x*k < k*y"
huffman@45462: by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
huffman@45462: next
huffman@45462: assume "0 < k \ Suc 0 < y" have "k < k*y"
huffman@45462: by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
huffman@45462: next
huffman@45462: assume "0 < b \ a * c < Suc 0" have "a*(b*c) < b"
huffman@45462: by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
huffman@45462: next
huffman@45462: assume "0 < a \ 0 < b \ c < d * x" have "a*(b*c) < d*b*(x*a)"
huffman@45462: by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
huffman@45462: next
huffman@45462: assume "0 < k \ x \ y" have "x*k \ k*y"
huffman@45462: by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
huffman@45462: next
huffman@45462: assume "0 < k \ Suc 0 \ y" have "k \ k*y"
huffman@45462: by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
huffman@45462: next
huffman@45462: assume "0 < b \ a * c \ Suc 0" have "a*(b*c) \ b"
huffman@45462: by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
huffman@45462: next
huffman@45462: assume "0 < a \ 0 < b \ c \ d * x" have "a*(b*c) \ d*b*(x*a)"
huffman@45462: by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
huffman@45462: next
huffman@45462: assume "(if k = 0 then 0 else x div y) = uu" have "(x*k) div (k*y) = uu"
huffman@45463: by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
huffman@45462: next
huffman@45462: assume "(if k = 0 then 0 else Suc 0 div y) = uu" have "k div (k*y) = uu"
huffman@45463: by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
huffman@45462: next
huffman@45462: assume "(if b = 0 then 0 else a * c) = uu" have "(a*(b*c)) div (b) = uu"
huffman@45463: by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
huffman@45462: next
huffman@45462: assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu"
huffman@45462: have "(a*(b*c)) div (d*b*(x*a)) = uu"
huffman@45463: by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
huffman@45462: next
huffman@45462: assume "k = 0 \ x dvd y" have "(x*k) dvd (k*y)"
huffman@45462: by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
huffman@45462: next
huffman@45462: assume "k = 0 \ Suc 0 dvd y" have "k dvd (k*y)"
huffman@45462: by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
huffman@45462: next
huffman@45462: assume "b = 0 \ a * c dvd Suc 0" have "(a*(b*c)) dvd (b)"
huffman@45462: by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
huffman@45462: next
huffman@45462: assume "b = 0 \ Suc 0 dvd a * c" have "b dvd (a*(b*c))"
huffman@45462: by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
huffman@45462: next
huffman@45462: assume "a = 0 \ b = 0 \ c dvd d * x" have "(a*(b*c)) dvd (d*b*(x*a))"
huffman@45462: by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
huffman@45462: }
huffman@45436: end
huffman@45462:
huffman@45463: subsection {* Numeral-cancellation simprocs for type @{typ nat} *}
huffman@45463:
huffman@45463: notepad begin
huffman@45463: fix x y z :: nat
huffman@45463: {
huffman@45463: assume "3 * x = 4 * y" have "9*x = 12 * y"
huffman@45463: by (tactic {* test [@{simproc nat_eq_cancel_numeral_factor}] *}) fact
huffman@45463: next
huffman@45463: assume "3 * x < 4 * y" have "9*x < 12 * y"
huffman@45463: by (tactic {* test [@{simproc nat_less_cancel_numeral_factor}] *}) fact
huffman@45463: next
huffman@45463: assume "3 * x \ 4 * y" have "9*x \ 12 * y"
huffman@45463: by (tactic {* test [@{simproc nat_le_cancel_numeral_factor}] *}) fact
huffman@45463: next
huffman@45463: assume "(3 * x) div (4 * y) = z" have "(9*x) div (12 * y) = z"
huffman@45463: by (tactic {* test [@{simproc nat_div_cancel_numeral_factor}] *}) fact
huffman@45463: next
huffman@45463: assume "(3 * x) dvd (4 * y)" have "(9*x) dvd (12 * y)"
huffman@45463: by (tactic {* test [@{simproc nat_dvd_cancel_numeral_factor}] *}) fact
huffman@45463: }
huffman@45462: end
huffman@45463:
huffman@45530: subsection {* Integer numeral div/mod simprocs *}
huffman@45530:
huffman@45530: notepad begin
huffman@45530: have "(10::int) div 3 = 3"
huffman@45530: by (tactic {* test [@{simproc binary_int_div}] *})
huffman@45530: have "(10::int) mod 3 = 1"
huffman@45530: by (tactic {* test [@{simproc binary_int_mod}] *})
huffman@45530: have "(10::int) div -3 = -4"
huffman@45530: by (tactic {* test [@{simproc binary_int_div}] *})
huffman@45530: have "(10::int) mod -3 = -2"
huffman@45530: by (tactic {* test [@{simproc binary_int_mod}] *})
huffman@45530: have "(-10::int) div 3 = -4"
huffman@45530: by (tactic {* test [@{simproc binary_int_div}] *})
huffman@45530: have "(-10::int) mod 3 = 2"
huffman@45530: by (tactic {* test [@{simproc binary_int_mod}] *})
huffman@45530: have "(-10::int) div -3 = 3"
huffman@45530: by (tactic {* test [@{simproc binary_int_div}] *})
huffman@45530: have "(-10::int) mod -3 = -1"
huffman@45530: by (tactic {* test [@{simproc binary_int_mod}] *})
huffman@45530: have "(8452::int) mod 3 = 1"
huffman@45530: by (tactic {* test [@{simproc binary_int_mod}] *})
huffman@45530: have "(59485::int) div 434 = 137"
huffman@45530: by (tactic {* test [@{simproc binary_int_div}] *})
huffman@45530: have "(1000006::int) mod 10 = 6"
huffman@45530: by (tactic {* test [@{simproc binary_int_mod}] *})
huffman@45530: have "10000000 div 2 = (5000000::int)"
huffman@45530: by (tactic {* test [@{simproc binary_int_div}] *})
huffman@45530: have "10000001 mod 2 = (1::int)"
huffman@45530: by (tactic {* test [@{simproc binary_int_mod}] *})
huffman@45530: have "10000055 div 32 = (312501::int)"
huffman@45530: by (tactic {* test [@{simproc binary_int_div}] *})
huffman@45530: have "10000055 mod 32 = (23::int)"
huffman@45530: by (tactic {* test [@{simproc binary_int_mod}] *})
huffman@45530: have "100094 div 144 = (695::int)"
huffman@45530: by (tactic {* test [@{simproc binary_int_div}] *})
huffman@45530: have "100094 mod 144 = (14::int)"
huffman@45530: by (tactic {* test [@{simproc binary_int_mod}] *})
huffman@45463: end
huffman@45530:
huffman@45530: end