(* Title: HOL/ex/Simproc_Tests.thy Author: Brian Huffman
*)
section \<open>Testing of arithmetic simprocs\<close>
theory Simproc_Tests imports Main begin
text\<open>
This theory tests the various simprocs defined in\<^file>\<open>~~/src/HOL/Nat.thy\<close> and \<^file>\<open>~~/src/HOL/Numeral_Simprocs.thy\<close>. Many of the tests are derived from commented-out code
originally found in\<^file>\<open>~~/src/HOL/Tools/numeral_simprocs.ML\<close>. \<close>
subsection \<open>ML bindings\<close>
ML \<open> fun test ctxt procs =
CHANGED (asm_simp_tac (put_simpset HOL_basic_ss ctxt |> fold Simplifier.add_proc procs) 1) \<close>
subsection \<open>Cancellation simprocs from \<open>Nat.thy\<close>\<close>
notepad begin fix a b c d :: nat
{ assume"b = Suc c"have"a + b = Suc (c + a)" by (tactic \<open>test \<^context> [\<^simproc>\<open>nateq_cancel_sums\<close>]\<close>) fact next assume"b < Suc c"have"a + b < Suc (c + a)" by (tactic \<open>test \<^context> [\<^simproc>\<open>natless_cancel_sums\<close>]\<close>) fact next assume"b \ Suc c" have "a + b \ Suc (c + a)" by (tactic \<open>test \<^context> [\<^simproc>\<open>natle_cancel_sums\<close>]\<close>) fact next assume"b - Suc c = d"have"a + b - Suc (c + a) = d" by (tactic \<open>test \<^context> [\<^simproc>\<open>natdiff_cancel_sums\<close>]\<close>) fact
} end
schematic_goal "\(y::?'b::size). size (?x::?'a::size) \ size y + size ?x" by (tactic \<open>test \<^context> [\<^simproc>\<open>natle_cancel_sums\<close>]\<close>) (rule le0) (* TODO: test more simprocs with schematic variables *)
subsection \<open>Abelian group cancellation simprocs\<close>
notepad begin fix a b c u :: "'a::ab_group_add"
{ assume"(a + 0) - (b + 0) = u"have"(a + c) - (b + c) = u" by (tactic \<open>test \<^context> [\<^simproc>\<open>group_cancel_diff\<close>]\<close>) fact next assume"a + 0 = b + 0"have"a + c = b + c" by (tactic \<open>test \<^context> [\<^simproc>\<open>group_cancel_eq\<close>]\<close>) fact
} end (* TODO: more tests for Groups.group_cancel_{add,diff,eq,less,le} *)
(* FIXME: int_combine_numerals often unnecessarily regroups addition and rewrites subtraction to negation. Ideally it should behave more like Groups.abel_cancel_sum, preserving the shape of terms as much as
possible. *)
notepad begin fix a b c d oo uu i j k l u v w x y z :: "'a::comm_ring_1"
{ assume"a + - b = u"have"(a + c) - (b + c) = u" by (tactic \<open>test \<^context> [\<^simproc>\<open>int_combine_numerals\<close>]\<close>) fact next assume"10 + (2 * l + oo) = uu" have"l + 2 + 2 + 2 + (l + 2) + (oo + 2) = uu" by (tactic \<open>test \<^context> [\<^simproc>\<open>int_combine_numerals\<close>]\<close>) fact next assume"-3 + (i + (j + k)) = y" have"(i + j + 12 + k) - 15 = y" by (tactic \<open>test \<^context> [\<^simproc>\<open>int_combine_numerals\<close>]\<close>) fact next assume"7 + (i + (j + k)) = y" have"(i + j + 12 + k) - 5 = y" by (tactic \<open>test \<^context> [\<^simproc>\<open>int_combine_numerals\<close>]\<close>) fact next assume"-4 * (u * v) + (2 * x + y) = w" have"(2*x - (u*v) + y) - v*3*u = w" by (tactic \<open>test \<^context> [\<^simproc>\<open>int_combine_numerals\<close>]\<close>) fact next assume"2 * x * u * v + y = w" have"(2*x*u*v + (u*v)*4 + y) - v*u*4 = w" by (tactic \<open>test \<^context> [\<^simproc>\<open>int_combine_numerals\<close>]\<close>) fact next assume"3 * (u * v) + (2 * x * u * v + y) = w" have"(2*x*u*v + (u*v)*4 + y) - v*u = w" by (tactic \<open>test \<^context> [\<^simproc>\<open>int_combine_numerals\<close>]\<close>) fact next assume"-3 * (u * v) + (- (x * u * v) + - y) = w" have"u*v - (x*u*v + (u*v)*4 + y) = w" by (tactic \<open>test \<^context> [\<^simproc>\<open>int_combine_numerals\<close>]\<close>) fact next assume"a + - c = d" have"a + -(b+c) + b = d" apply (simp only: minus_add_distrib) by (tactic \<open>test \<^context> [\<^simproc>\<open>int_combine_numerals\<close>]\<close>) fact next assume"-2 * b + (a + - c) = d" have"a + -(b+c) - b = d" apply (simp only: minus_add_distrib) by (tactic \<open>test \<^context> [\<^simproc>\<open>int_combine_numerals\<close>]\<close>) fact next assume"-7 + (i + (j + (k + (- u + - y)))) = z" have"(i + j + -2 + k) - (u + 5 + y) = z" by (tactic \<open>test \<^context> [\<^simproc>\<open>int_combine_numerals\<close>]\<close>) fact next assume"-27 + (i + (j + k)) = y" have"(i + j + -12 + k) - 15 = y" by (tactic \<open>test \<^context> [\<^simproc>\<open>int_combine_numerals\<close>]\<close>) fact next assume"27 + (i + (j + k)) = y" have"(i + j + 12 + k) - -15 = y" by (tactic \<open>test \<^context> [\<^simproc>\<open>int_combine_numerals\<close>]\<close>) fact next assume"3 + (i + (j + k)) = y" have"(i + j + -12 + k) - -15 = y" by (tactic \<open>test \<^context> [\<^simproc>\<open>int_combine_numerals\<close>]\<close>) fact
} end
notepad begin fix b c i j k u y :: "'a::linordered_idom"
{ assume"y < 2 * b"have"y - b < b" by (tactic \<open>test \<^context> [\<^simproc>\<open>intless_cancel_numerals\<close>]\<close>) fact next assume"c + y < 4 * b"have"y - (3*b + c) < b - 2*c" by (tactic \<open>test \<^context> [\<^simproc>\<open>intless_cancel_numerals\<close>]\<close>) fact next assume"i + (j + k) < 8 + (u + y)" have"(i + j + -3 + k) < u + 5 + y" by (tactic \<open>test \<^context> [\<^simproc>\<open>intless_cancel_numerals\<close>]\<close>) fact next assume"9 + (i + (j + k)) < u + y" have"(i + j + 3 + k) < u + -6 + y" by (tactic \<open>test \<^context> [\<^simproc>\<open>intless_cancel_numerals\<close>]\<close>) fact
} end
notepad begin fix x y z :: "'a::{unique_euclidean_semiring,comm_ring_1,ring_char_0}"
{ assume"(3*x) div (4*y) = z"have"(9*x) div (12*y) = z" by (tactic \<open>test \<^context> [\<^simproc>\<open>int_div_cancel_numeral_factors\<close>]\<close>) fact next assume"(-3*x) div (4*y) = z"have"(-99*x) div (132*y) = z" by (tactic \<open>test \<^context> [\<^simproc>\<open>int_div_cancel_numeral_factors\<close>]\<close>) fact next assume"(111*x) div (-44*y) = z"have"(999*x) div (-396*y) = z" by (tactic \<open>test \<^context> [\<^simproc>\<open>int_div_cancel_numeral_factors\<close>]\<close>) fact next assume"(11*x) div (9*y) = z"have"(-99*x) div (-81*y) = z" by (tactic \<open>test \<^context> [\<^simproc>\<open>int_div_cancel_numeral_factors\<close>]\<close>) fact next assume"(2*x) div y = z" have"(-2 * x) div (-1 * y) = z" by (tactic \<open>test \<^context> [\<^simproc>\<open>int_div_cancel_numeral_factors\<close>]\<close>) fact
} end
notepad begin fix x y :: "'a::linordered_idom"
{ assume"3*x \ 4*y" have "9*x \ 12 * y" by (tactic \<open>test \<^context> [\<^simproc>\<open>ring_le_cancel_numeral_factor\<close>]\<close>) fact next assume"-3*x \ 4*y" have "-99*x \ 132 * y" by (tactic \<open>test \<^context> [\<^simproc>\<open>ring_le_cancel_numeral_factor\<close>]\<close>) fact next assume"111*x \ -44*y" have "999*x \ -396 * y" by (tactic \<open>test \<^context> [\<^simproc>\<open>ring_le_cancel_numeral_factor\<close>]\<close>) fact next assume"9*y \ 11*x" have "-99*x \ -81 * y" by (tactic \<open>test \<^context> [\<^simproc>\<open>ring_le_cancel_numeral_factor\<close>]\<close>) fact next assume"y \ 2*x" have "-2 * x \ -1 * y" by (tactic \<open>test \<^context> [\<^simproc>\<open>ring_le_cancel_numeral_factor\<close>]\<close>) fact next assume"23*y \ x" have "-x \ -23 * y" by (tactic \<open>test \<^context> [\<^simproc>\<open>ring_le_cancel_numeral_factor\<close>]\<close>) fact next assume"y \ 0" have "0 \ y * -2" by (tactic \<open>test \<^context> [\<^simproc>\<open>ring_le_cancel_numeral_factor\<close>]\<close>) fact next assume"- x \ y" have "- (2 * x) \ 2*y" by (tactic \<open>test \<^context> [\<^simproc>\<open>ring_le_cancel_numeral_factor\<close>]\<close>) fact
} end
notepad begin fix a b c d k x y :: "'a::idom"
{ assume"k = 0 \ x = y" have "x*k = k*y" by (tactic \<open>test \<^context> [\<^simproc>\<open>ring_eq_cancel_factor\<close>]\<close>) fact next assume"k = 0 \ 1 = y" have "k = k*y" by (tactic \<open>test \<^context> [\<^simproc>\<open>ring_eq_cancel_factor\<close>]\<close>) fact next assume"b = 0 \ a*c = 1" have "a*(b*c) = b" by (tactic \<open>test \<^context> [\<^simproc>\<open>ring_eq_cancel_factor\<close>]\<close>) fact next assume"a = 0 \ b = 0 \ c = d*x" have "a*(b*c) = d*b*(x*a)" by (tactic \<open>test \<^context> [\<^simproc>\<open>ring_eq_cancel_factor\<close>]\<close>) fact next assume"k = 0 \ x = y" have "x*k = k*y" by (tactic \<open>test \<^context> [\<^simproc>\<open>ring_eq_cancel_factor\<close>]\<close>) fact next assume"k = 0 \ 1 = y" have "k = k*y" by (tactic \<open>test \<^context> [\<^simproc>\<open>ring_eq_cancel_factor\<close>]\<close>) fact
} end
notepad begin fix a b c d k uu x y :: "'a::unique_euclidean_semiring"
{ assume"(if k = 0 then 0 else x div y) = uu" have"(x*k) div (k*y) = uu" by (tactic \<open>test \<^context> [\<^simproc>\<open>int_div_cancel_factor\<close>]\<close>) fact next assume"(if k = 0 then 0 else 1 div y) = uu" have"(k) div (k*y) = uu" by (tactic \<open>test \<^context> [\<^simproc>\<open>int_div_cancel_factor\<close>]\<close>) fact next assume"(if b = 0 then 0 else a * c) = uu" have"(a*(b*c)) div b = uu" by (tactic \<open>test \<^context> [\<^simproc>\<open>int_div_cancel_factor\<close>]\<close>) fact next assume"(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu" have"(a*(b*c)) div (d*b*(x*a)) = uu" by (tactic \<open>test \<^context> [\<^simproc>\<open>int_div_cancel_factor\<close>]\<close>) fact
} end
lemmashows"a*(b*c)/(y*z) = d*(b::'a::linordered_field)*(x*a)/z" oops\<comment> \<open>FIXME: need simproc to cover this case\<close>
notepad begin fix a b c d k uu x y :: "'a::field"
{ assume"(if k = 0 then 0 else x / y) = uu" have"(x*k) / (k*y) = uu" by (tactic \<open>test \<^context> [\<^simproc>\<open>divide_cancel_factor\<close>]\<close>) fact next assume"(if k = 0 then 0 else 1 / y) = uu" have"(k) / (k*y) = uu" by (tactic \<open>test \<^context> [\<^simproc>\<open>divide_cancel_factor\<close>]\<close>) fact next assume"(if b = 0 then 0 else a * c) = uu" have"(a*(b*c)) / b = uu" by (tactic \<open>test \<^context> [\<^simproc>\<open>divide_cancel_factor\<close>]\<close>) fact next assume"(if a = 0 then 0 else if b = 0 then 0 else c / (d * x)) = uu" have"(a*(b*c)) / (d*b*(x*a)) = uu" by (tactic \<open>test \<^context> [\<^simproc>\<open>divide_cancel_factor\<close>]\<close>) fact
} end
lemma fixes a b c d x y z :: "'a::linordered_field" shows"a*(b*c)/(y*z) = d*(b)*(x*a)/z" oops\<comment> \<open>FIXME: need simproc to cover this case\<close>
notepad begin fix x y z :: "'a::linordered_idom"
{ assume"0 < z \ x < y" have "0 < z \ x*z < y*z" by (tactic \<open>test \<^context> [\<^simproc>\<open>linordered_ring_less_cancel_factor\<close>]\<close>) fact next assume"0 < z \ x < y" have "0 < z \ x*z < z*y" by (tactic \<open>test \<^context> [\<^simproc>\<open>linordered_ring_less_cancel_factor\<close>]\<close>) fact next assume"0 < z \ x < y" have "0 < z \ z*x < y*z" by (tactic \<open>test \<^context> [\<^simproc>\<open>linordered_ring_less_cancel_factor\<close>]\<close>) fact next assume"0 < z \ x < y" have "0 < z \ z*x < z*y" by (tactic \<open>test \<^context> [\<^simproc>\<open>linordered_ring_less_cancel_factor\<close>]\<close>) fact next txt"This simproc now uses the simplifier to prove that terms to
be canceled are positive/negative." assume z_pos: "0 < z" assume"x < y"have"z*x < z*y" by (tactic \<open>CHANGED (asm_simp_tac (put_simpset HOL_basic_ss \<^context>
|> Simplifier.add_proc \<^simproc>\<open>linordered_ring_less_cancel_factor\<close>
|> Simplifier.add_simp @{thm z_pos}) 1)\<close>) fact
} end
notepad begin fix x y z :: "'a::linordered_idom"
{ assume"0 < z \ x \ y" have "0 < z \ x*z \ y*z" by (tactic \<open>test \<^context> [\<^simproc>\<open>linordered_ring_le_cancel_factor\<close>]\<close>) fact next assume"0 < z \ x \ y" have "0 < z \ z*x \ z*y" by (tactic \<open>test \<^context> [\<^simproc>\<open>linordered_ring_le_cancel_factor\<close>]\<close>) fact
} end
notepad begin fix x y z uu :: "'a::{field,ring_char_0}"
{ assume"5 / 6 * x = uu"have"x / 2 + x / 3 = uu" by (tactic \<open>test \<^context> [\<^simproc>\<open>field_combine_numerals\<close>]\<close>) fact next assume"6 / 9 * x + y = uu"have"x / 3 + y + x / 3 = uu" by (tactic \<open>test \<^context> [\<^simproc>\<open>field_combine_numerals\<close>]\<close>) fact next assume"9 / 9 * x = uu"have"2 * x / 3 + x / 3 = uu" by (tactic \<open>test \<^context> [\<^simproc>\<open>field_combine_numerals\<close>]\<close>) fact next assume"y + z = uu" have"x / 2 + y - 3 * x / 6 + z = uu" by (tactic \<open>test \<^context> [\<^simproc>\<open>field_combine_numerals\<close>]\<close>) fact next assume"1 / 15 * x + y = uu" have"7 * x / 5 + y - 4 * x / 3 = uu" by (tactic \<open>test \<^context> [\<^simproc>\<open>field_combine_numerals\<close>]\<close>) fact
} end
lemma fixes x :: "'a::{linordered_field}" shows"2/3 * x + x / 3 = uu" apply (tactic \<open>test \<^context> [\<^simproc>\<open>field_combine_numerals\<close>]\<close>)? oops\<comment> \<open>FIXME: test fails\<close>
notepad begin fix length :: "'a \ nat" and l2 l3 :: "'a" and f :: "nat \ 'a" fix c e i j k l oo u uu vv w y z w' y' z' :: "nat"
{ assume"u + y \ 36 * Suc 0 + (i + (j + k))" have"Suc (Suc (Suc (Suc (Suc (u + y))))) \ ((i + j) + 41 + k)" by (tactic \<open>test \<^context> [\<^simproc>\<open>natle_cancel_numerals\<close>]\<close>) fact next assume"5 * Suc 0 + (case length (f c) of 0 \ 0 | Suc k \ k) = 0" have"(Suc (Suc (Suc (Suc (Suc (Suc (case length (f c) of 0 => 0 | Suc k => k)))))) \ Suc 0)" by (tactic \<open>test \<^context> [\<^simproc>\<open>natle_cancel_numerals\<close>]\<close>) fact next assume"6 + length l2 = 0"have"Suc (Suc (Suc (Suc (Suc (Suc (length l1 + length l2)))))) \ length l1" by (tactic \<open>test \<^context> [\<^simproc>\<open>natle_cancel_numerals\<close>]\<close>) fact next assume"5 + length l3 = 0" have"( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length l3)))))) \ length (compT P E A ST mxr e))" by (tactic \<open>test \<^context> [\<^simproc>\<open>natle_cancel_numerals\<close>]\<close>) fact next assume"5 + length (compT P E (A \ A' e) ST mxr c) = 0" 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))" by (tactic \<open>test \<^context> [\<^simproc>\<open>natle_cancel_numerals\<close>]\<close>) fact
} end
notepad begin fix length :: "'a \ nat" and l2 l3 :: "'a" and f :: "nat \ 'a" fix c e i j k l oo u uu vv v w x y z zz w' y' z' :: "nat"
{ assume"i + (j + k) - 3 * Suc 0 = y"have"(i + j + 12 + k) - 15 = y" by (tactic \<open>test \<^context> [\<^simproc>\<open>natdiff_cancel_numerals\<close>]\<close>) fact next assume"7 * Suc 0 + (i + (j + k)) - 0 = y"have"(i + j + 12 + k) - 5 = y" by (tactic \<open>test \<^context> [\<^simproc>\<open>natdiff_cancel_numerals\<close>]\<close>) fact next assume"u - Suc 0 * Suc 0 = y"have"Suc u - 2 = y" by (tactic \<open>test \<^context> [\<^simproc>\<open>natdiff_cancel_numerals\<close>]\<close>) fact next assume"Suc 0 * Suc 0 + u - 0 = y"have"Suc (Suc (Suc u)) - 2 = y" by (tactic \<open>test \<^context> [\<^simproc>\<open>natdiff_cancel_numerals\<close>]\<close>) fact next assume"Suc 0 * Suc 0 + (i + (j + k)) - 0 = y" have"(i + j + 2 + k) - 1 = y" by (tactic \<open>test \<^context> [\<^simproc>\<open>natdiff_cancel_numerals\<close>]\<close>) fact next assume"i + (j + k) - Suc 0 * Suc 0 = y" have"(i + j + 1 + k) - 2 = y" by (tactic \<open>test \<^context> [\<^simproc>\<open>natdiff_cancel_numerals\<close>]\<close>) fact next assume"2 * x + y - 2 * (u * v) = w" have"(2*x + (u*v) + y) - v*3*u = w" by (tactic \<open>test \<^context> [\<^simproc>\<open>natdiff_cancel_numerals\<close>]\<close>) fact next assume"2 * x * u * v + (5 + y) - 0 = w" have"(2*x*u*v + 5 + (u*v)*4 + y) - v*u*4 = w" by (tactic \<open>test \<^context> [\<^simproc>\<open>natdiff_cancel_numerals\<close>]\<close>) fact next assume"3 * (u * v) + (2 * x * u * v + y) - 0 = w" have"(2*x*u*v + (u*v)*4 + y) - v*u = w" by (tactic \<open>test \<^context> [\<^simproc>\<open>natdiff_cancel_numerals\<close>]\<close>) fact next assume"3 * u + (2 + (2 * x * u * v + y)) - 0 = w" have"Suc (Suc (2*x*u*v + u*4 + y)) - u = w" by (tactic \<open>test \<^context> [\<^simproc>\<open>natdiff_cancel_numerals\<close>]\<close>) fact next assume"Suc (Suc 0 * (u * v)) - 0 = w" have"Suc ((u*v)*4) - v*3*u = w" by (tactic \<open>test \<^context> [\<^simproc>\<open>natdiff_cancel_numerals\<close>]\<close>) fact next assume"2 - 0 = w"have"Suc (Suc ((u*v)*3)) - v*3*u = w" by (tactic \<open>test \<^context> [\<^simproc>\<open>natdiff_cancel_numerals\<close>]\<close>) fact next assume"17 * Suc 0 + (i + (j + k)) - (u + y) = zz" have"(i + j + 32 + k) - (u + 15 + y) = zz" by (tactic \<open>test \<^context> [\<^simproc>\<open>natdiff_cancel_numerals\<close>]\<close>) fact next assume"u + y - 0 = v"have"Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v" by (tactic \<open>test \<^context> [\<^simproc>\<open>natdiff_cancel_numerals\<close>]\<close>) fact
} end
subsection \<open>Factor-cancellation simprocs for type \<^typ>\<open>nat\<close>\<close>
text\<open>\<open>nat_eq_cancel_factor\<close>, \<open>nat_less_cancel_factor\<close>, \<open>nat_le_cancel_factor\<close>, \<open>nat_divide_cancel_factor\<close>, and \<open>nat_dvd_cancel_factor\<close>.\<close>
notepad begin fix a b c d k x y uu :: nat
{ assume"k = 0 \ x = y" have "x*k = k*y" by (tactic \<open>test \<^context> [\<^simproc>\<open>nat_eq_cancel_factor\<close>]\<close>) fact next assume"k = 0 \ Suc 0 = y" have "k = k*y" by (tactic \<open>test \<^context> [\<^simproc>\<open>nat_eq_cancel_factor\<close>]\<close>) fact next assume"b = 0 \ a * c = Suc 0" have "a*(b*c) = b" by (tactic \<open>test \<^context> [\<^simproc>\<open>nat_eq_cancel_factor\<close>]\<close>) fact next assume"a = 0 \ b = 0 \ c = d * x" have "a*(b*c) = d*b*(x*a)" by (tactic \<open>test \<^context> [\<^simproc>\<open>nat_eq_cancel_factor\<close>]\<close>) fact next assume"0 < k \ x < y" have "x*k < k*y" by (tactic \<open>test \<^context> [\<^simproc>\<open>nat_less_cancel_factor\<close>]\<close>) fact next assume"0 < k \ Suc 0 < y" have "k < k*y" by (tactic \<open>test \<^context> [\<^simproc>\<open>nat_less_cancel_factor\<close>]\<close>) fact next assume"0 < b \ a * c < Suc 0" have "a*(b*c) < b" by (tactic \<open>test \<^context> [\<^simproc>\<open>nat_less_cancel_factor\<close>]\<close>) fact next assume"0 < a \ 0 < b \ c < d * x" have "a*(b*c) < d*b*(x*a)" by (tactic \<open>test \<^context> [\<^simproc>\<open>nat_less_cancel_factor\<close>]\<close>) fact next assume"0 < k \ x \ y" have "x*k \ k*y" by (tactic \<open>test \<^context> [\<^simproc>\<open>nat_le_cancel_factor\<close>]\<close>) fact next assume"0 < k \ Suc 0 \ y" have "k \ k*y" by (tactic \<open>test \<^context> [\<^simproc>\<open>nat_le_cancel_factor\<close>]\<close>) fact next assume"0 < b \ a * c \ Suc 0" have "a*(b*c) \ b" by (tactic \<open>test \<^context> [\<^simproc>\<open>nat_le_cancel_factor\<close>]\<close>) fact next assume"0 < a \ 0 < b \ c \ d * x" have "a*(b*c) \ d*b*(x*a)" by (tactic \<open>test \<^context> [\<^simproc>\<open>nat_le_cancel_factor\<close>]\<close>) fact next assume"(if k = 0 then 0 else x div y) = uu"have"(x*k) div (k*y) = uu" by (tactic \<open>test \<^context> [\<^simproc>\<open>nat_div_cancel_factor\<close>]\<close>) fact next assume"(if k = 0 then 0 else Suc 0 div y) = uu"have"k div (k*y) = uu" by (tactic \<open>test \<^context> [\<^simproc>\<open>nat_div_cancel_factor\<close>]\<close>) fact next assume"(if b = 0 then 0 else a * c) = uu"have"(a*(b*c)) div (b) = uu" by (tactic \<open>test \<^context> [\<^simproc>\<open>nat_div_cancel_factor\<close>]\<close>) fact next assume"(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu" have"(a*(b*c)) div (d*b*(x*a)) = uu" by (tactic \<open>test \<^context> [\<^simproc>\<open>nat_div_cancel_factor\<close>]\<close>) fact next assume"k = 0 \ x dvd y" have "(x*k) dvd (k*y)" by (tactic \<open>test \<^context> [\<^simproc>\<open>nat_dvd_cancel_factor\<close>]\<close>) fact next assume"k = 0 \ Suc 0 dvd y" have "k dvd (k*y)" by (tactic \<open>test \<^context> [\<^simproc>\<open>nat_dvd_cancel_factor\<close>]\<close>) fact next assume"b = 0 \ a * c dvd Suc 0" have "(a*(b*c)) dvd (b)" by (tactic \<open>test \<^context> [\<^simproc>\<open>nat_dvd_cancel_factor\<close>]\<close>) fact next assume"b = 0 \ Suc 0 dvd a * c" have "b dvd (a*(b*c))" by (tactic \<open>test \<^context> [\<^simproc>\<open>nat_dvd_cancel_factor\<close>]\<close>) fact next assume"a = 0 \ b = 0 \ c dvd d * x" have "(a*(b*c)) dvd (d*b*(x*a))" by (tactic \<open>test \<^context> [\<^simproc>\<open>nat_dvd_cancel_factor\<close>]\<close>) fact
} end
subsection \<open>Numeral-cancellation simprocs for type \<^typ>\<open>nat\<close>\<close>
notepad begin fix x y z :: nat
{ assume"3 * x = 4 * y"have"9*x = 12 * y" by (tactic \<open>test \<^context> [\<^simproc>\<open>nat_eq_cancel_numeral_factor\<close>]\<close>) fact next assume"3 * x < 4 * y"have"9*x < 12 * y" by (tactic \<open>test \<^context> [\<^simproc>\<open>nat_less_cancel_numeral_factor\<close>]\<close>) fact next assume"3 * x \ 4 * y" have "9*x \ 12 * y" by (tactic \<open>test \<^context> [\<^simproc>\<open>nat_le_cancel_numeral_factor\<close>]\<close>) fact next assume"(3 * x) div (4 * y) = z"have"(9*x) div (12 * y) = z" by (tactic \<open>test \<^context> [\<^simproc>\<open>nat_div_cancel_numeral_factor\<close>]\<close>) fact next assume"(3 * x) dvd (4 * y)"have"(9*x) dvd (12 * y)" by (tactic \<open>test \<^context> [\<^simproc>\<open>nat_dvd_cancel_numeral_factor\<close>]\<close>) fact
} end
notepad begin have"(10::int) div 3 = 3" by (tactic \<open>test \<^context> [\<^simproc>\<open>numeral_divmod\<close>]\<close>) have"(10::int) mod 3 = 1" by (tactic \<open>test \<^context> [\<^simproc>\<open>numeral_divmod\<close>]\<close>) have"(10::int) div -3 = -4" by (tactic \<open>test \<^context> [\<^simproc>\<open>numeral_divmod\<close>]\<close>) have"(10::int) mod -3 = -2" by (tactic \<open>test \<^context> [\<^simproc>\<open>numeral_divmod\<close>]\<close>) have"(-10::int) div 3 = -4" by (tactic \<open>test \<^context> [\<^simproc>\<open>numeral_divmod\<close>]\<close>) have"(-10::int) mod 3 = 2" by (tactic \<open>test \<^context> [\<^simproc>\<open>numeral_divmod\<close>]\<close>) have"(-10::int) div -3 = 3" by (tactic \<open>test \<^context> [\<^simproc>\<open>numeral_divmod\<close>]\<close>) have"(-10::int) mod -3 = -1" by (tactic \<open>test \<^context> [\<^simproc>\<open>numeral_divmod\<close>]\<close>) have"(8452::int) mod 3 = 1" by (tactic \<open>test \<^context> [\<^simproc>\<open>numeral_divmod\<close>]\<close>) have"(59485::int) div 434 = 137" by (tactic \<open>test \<^context> [\<^simproc>\<open>numeral_divmod\<close>]\<close>) have"(1000006::int) mod 10 = 6" by (tactic \<open>test \<^context> [\<^simproc>\<open>numeral_divmod\<close>]\<close>) have"10000000 div 2 = (5000000::int)" by (tactic \<open>test \<^context> [\<^simproc>\<open>numeral_divmod\<close>]\<close>) have"10000001 mod 2 = (1::int)" by (tactic \<open>test \<^context> [\<^simproc>\<open>numeral_divmod\<close>]\<close>) have"10000055 div 32 = (312501::int)" by (tactic \<open>test \<^context> [\<^simproc>\<open>numeral_divmod\<close>]\<close>) have"10000055 mod 32 = (23::int)" by (tactic \<open>test \<^context> [\<^simproc>\<open>numeral_divmod\<close>]\<close>) have"100094 div 144 = (695::int)" by (tactic \<open>test \<^context> [\<^simproc>\<open>numeral_divmod\<close>]\<close>) have"100094 mod 144 = (14::int)" by (tactic \<open>test \<^context> [\<^simproc>\<open>numeral_divmod\<close>]\<close>) end
end
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.19Bemerkung:
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
