# HG changeset patch # User huffman # Date 1321006263 -3600 # Node ID aba629d6cee50b0c91386ae67f82dbe51ac4ea0a # Parent 74515e8e6046bed1fd7abd6adce7714812c7dbb3 use simproc_setup for more nat_numeral simprocs; add simproc tests diff -r 74515e8e6046 -r aba629d6cee5 src/HOL/Numeral_Simprocs.thy --- a/src/HOL/Numeral_Simprocs.thy Fri Nov 11 08:32:48 2011 +0100 +++ b/src/HOL/Numeral_Simprocs.thy Fri Nov 11 11:11:03 2011 +0100 @@ -202,6 +202,10 @@ use "Tools/nat_numeral_simprocs.ML" +simproc_setup nat_combine_numerals + ("(i::nat) + j" | "Suc (i + j)") = + {* fn phi => Nat_Numeral_Simprocs.combine_numerals *} + simproc_setup nateq_cancel_numerals ("(l::nat) + m = n" | "(l::nat) = m + n" | "(l::nat) * m = n" | "(l::nat) = m * n" | @@ -226,6 +230,26 @@ "Suc m - n" | "m - Suc n") = {* fn phi => Nat_Numeral_Simprocs.diff_cancel_numerals *} +simproc_setup nat_eq_cancel_factor + ("(l::nat) * m = n" | "(l::nat) = m * n") = + {* fn phi => Nat_Numeral_Simprocs.eq_cancel_factor *} + +simproc_setup nat_less_cancel_factor + ("(l::nat) * m < n" | "(l::nat) < m * n") = + {* fn phi => Nat_Numeral_Simprocs.less_cancel_factor *} + +simproc_setup nat_le_cancel_factor + ("(l::nat) * m <= n" | "(l::nat) <= m * n") = + {* fn phi => Nat_Numeral_Simprocs.le_cancel_factor *} + +simproc_setup nat_divide_cancel_factor + ("((l::nat) * m) div n" | "(l::nat) div (m * n)") = + {* fn phi => Nat_Numeral_Simprocs.divide_cancel_factor *} + +simproc_setup nat_dvd_cancel_factor + ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") = + {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_factor *} + declaration {* K (Lin_Arith.add_simps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}]) #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1}, @@ -247,7 +271,7 @@ @{simproc intless_cancel_numerals}, @{simproc intle_cancel_numerals}] #> Lin_Arith.add_simprocs - [Nat_Numeral_Simprocs.combine_numerals, + [@{simproc nat_combine_numerals}, @{simproc nateq_cancel_numerals}, @{simproc natless_cancel_numerals}, @{simproc natle_cancel_numerals}, diff -r 74515e8e6046 -r aba629d6cee5 src/HOL/Tools/nat_numeral_simprocs.ML --- a/src/HOL/Tools/nat_numeral_simprocs.ML Fri Nov 11 08:32:48 2011 +0100 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML Fri Nov 11 11:11:03 2011 +0100 @@ -5,16 +5,20 @@ signature NAT_NUMERAL_SIMPROCS = sig - val combine_numerals: simproc + val combine_numerals: simpset -> cterm -> thm option val eq_cancel_numerals: simpset -> cterm -> thm option val less_cancel_numerals: simpset -> cterm -> thm option val le_cancel_numerals: simpset -> cterm -> thm option val diff_cancel_numerals: simpset -> cterm -> thm option - val cancel_factors: simproc list + val eq_cancel_factor: simpset -> cterm -> thm option + val less_cancel_factor: simpset -> cterm -> thm option + val le_cancel_factor: simpset -> cterm -> thm option + val divide_cancel_factor: simpset -> cterm -> thm option + val dvd_cancel_factor: simpset -> cterm -> thm option val cancel_numeral_factors: simproc list end; -structure Nat_Numeral_Simprocs = +structure Nat_Numeral_Simprocs : NAT_NUMERAL_SIMPROCS = struct (*Maps n to #n for n = 0, 1, 2*) @@ -232,9 +236,7 @@ structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); -val combine_numerals = - Numeral_Simprocs.prep_simproc @{theory} - ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc); +fun combine_numerals ss ct = CombineNumerals.proc ss (term_of ct) (*** Applying CancelNumeralFactorFun ***) @@ -387,30 +389,16 @@ fun simp_conv _ _ = SOME @{thm nat_mult_dvd_cancel_disj} ); -val cancel_factor = - map (Numeral_Simprocs.prep_simproc @{theory}) - [("nat_eq_cancel_factor", - ["(l::nat) * m = n", "(l::nat) = m * n"], - K EqCancelFactor.proc), - ("nat_less_cancel_factor", - ["(l::nat) * m < n", "(l::nat) < m * n"], - K LessCancelFactor.proc), - ("nat_le_cancel_factor", - ["(l::nat) * m <= n", "(l::nat) <= m * n"], - K LeCancelFactor.proc), - ("nat_divide_cancel_factor", - ["((l::nat) * m) div n", "(l::nat) div (m * n)"], - K DivideCancelFactor.proc), - ("nat_dvd_cancel_factor", - ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"], - K DvdCancelFactor.proc)]; +fun eq_cancel_factor ss ct = EqCancelFactor.proc ss (term_of ct) +fun less_cancel_factor ss ct = LessCancelFactor.proc ss (term_of ct) +fun le_cancel_factor ss ct = LeCancelFactor.proc ss (term_of ct) +fun divide_cancel_factor ss ct = DivideCancelFactor.proc ss (term_of ct) +fun dvd_cancel_factor ss ct = DvdCancelFactor.proc ss (term_of ct) end; -Addsimprocs [Nat_Numeral_Simprocs.combine_numerals]; Addsimprocs Nat_Numeral_Simprocs.cancel_numeral_factors; -Addsimprocs Nat_Numeral_Simprocs.cancel_factor; (*examples: @@ -419,40 +407,10 @@ set simp_trace; fun test s = (Goal s; by (Simp_tac 1)); -(*combine_numerals*) -test "k + 3*k = (u::nat)"; -test "Suc (i + 3) = u"; -test "Suc (i + j + 3 + k) = u"; -test "k + j + 3*k + j = (u::nat)"; -test "Suc (j*i + i + k + 5 + 3*k + i*j*4) = (u::nat)"; -test "(2*n*m) + (3*(m*n)) = (u::nat)"; -(*negative numerals: FAIL*) -test "Suc (i + j + -3 + k) = u"; - (*cancel_numeral_factors*) test "9*x = 12 * (y::nat)"; test "(9*x) div (12 * (y::nat)) = z"; test "9*x < 12 * (y::nat)"; test "9*x <= 12 * (y::nat)"; -(*cancel_factor*) -test "x*k = k*(y::nat)"; -test "k = k*(y::nat)"; -test "a*(b*c) = (b::nat)"; -test "a*(b*c) = d*(b::nat)*(x*a)"; - -test "x*k < k*(y::nat)"; -test "k < k*(y::nat)"; -test "a*(b*c) < (b::nat)"; -test "a*(b*c) < d*(b::nat)*(x*a)"; - -test "x*k <= k*(y::nat)"; -test "k <= k*(y::nat)"; -test "a*(b*c) <= (b::nat)"; -test "a*(b*c) <= d*(b::nat)*(x*a)"; - -test "(x*k) div (k*(y::nat)) = (uu::nat)"; -test "(k) div (k*(y::nat)) = (uu::nat)"; -test "(a*(b*c)) div ((b::nat)) = (uu::nat)"; -test "(a*(b*c)) div (d*(b::nat)*(x*a)) = (uu::nat)"; *) diff -r 74515e8e6046 -r aba629d6cee5 src/HOL/ex/Simproc_Tests.thy --- a/src/HOL/ex/Simproc_Tests.thy Fri Nov 11 08:32:48 2011 +0100 +++ b/src/HOL/ex/Simproc_Tests.thy Fri Nov 11 11:11:03 2011 +0100 @@ -5,7 +5,7 @@ header {* Testing of arithmetic simprocs *} theory Simproc_Tests -imports Rat +imports Main begin text {* @@ -324,10 +324,11 @@ } end -lemma shows "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z" +lemma + fixes a b c d x y z :: "'a::linordered_field_inverse_zero" + shows "a*(b*c)/(y*z) = d*(b)*(x*a)/z" oops -- "FIXME: need simproc to cover this case" - subsection {* @{text linordered_ring_less_cancel_factor} *} notepad begin @@ -384,16 +385,49 @@ } end -lemma "2/3 * (x::rat) + x / 3 = uu" +lemma + fixes x :: "'a::{linordered_field_inverse_zero,number_ring}" + shows "2/3 * x + x / 3 = uu" apply (tactic {* test [@{simproc field_combine_numerals}] *})? oops -- "FIXME: test fails" +subsection {* @{text nat_combine_numerals} *} + +notepad begin + fix i j k m n u :: nat + { + assume "4*k = u" have "k + 3*k = u" + by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact + next + assume "4 * Suc 0 + i = u" have "Suc (i + 3) = u" + by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact + next + assume "4 * Suc 0 + (i + (j + k)) = u" have "Suc (i + j + 3 + k) = u" + by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact + next + assume "2 * j + 4 * k = u" have "k + j + 3*k + j = u" + by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact + next + assume "6 * Suc 0 + (5 * (i * j) + (4 * k + i)) = u" + have "Suc (j*i + i + k + 5 + 3*k + i*j*4) = u" + by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact + next + assume "5 * (m * n) = u" have "(2*n*m) + (3*(m*n)) = u" + by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact + } +end + +(*negative numerals: FAIL*) +lemma "Suc (i + j + -3 + k) = u" +apply (tactic {* test [@{simproc nat_combine_numerals}] *})? +oops + subsection {* @{text nateq_cancel_numerals} *} notepad begin fix i j k l oo u uu vv w y z w' y' z' :: "nat" { - assume "Suc 0 * u = 0" have "2*u = (u::nat)" + assume "Suc 0 * u = 0" have "2*u = u" by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact next assume "Suc 0 * u = Suc 0" have "2*u = Suc (u)" @@ -560,4 +594,79 @@ } end +subsection {* Factor-cancellation simprocs for type @{typ nat} *} + +text {* @{text nat_eq_cancel_factor}, @{text nat_less_cancel_factor}, +@{text nat_le_cancel_factor}, @{text nat_divide_cancel_factor}, and +@{text nat_dvd_cancel_factor}. *} + +notepad begin + fix a b c d k x y uu :: nat + { + assume "k = 0 \ x = y" have "x*k = k*y" + by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact + next + assume "k = 0 \ Suc 0 = y" have "k = k*y" + by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact + next + assume "b = 0 \ a * c = Suc 0" have "a*(b*c) = b" + by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact + next + assume "a = 0 \ b = 0 \ c = d * x" have "a*(b*c) = d*b*(x*a)" + by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact + next + assume "0 < k \ x < y" have "x*k < k*y" + by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact + next + assume "0 < k \ Suc 0 < y" have "k < k*y" + by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact + next + assume "0 < b \ a * c < Suc 0" have "a*(b*c) < b" + by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact + next + assume "0 < a \ 0 < b \ c < d * x" have "a*(b*c) < d*b*(x*a)" + by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact + next + assume "0 < k \ x \ y" have "x*k \ k*y" + by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact + next + assume "0 < k \ Suc 0 \ y" have "k \ k*y" + by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact + next + assume "0 < b \ a * c \ Suc 0" have "a*(b*c) \ b" + by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact + next + assume "0 < a \ 0 < b \ c \ d * x" have "a*(b*c) \ d*b*(x*a)" + by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact + next + assume "(if k = 0 then 0 else x div y) = uu" have "(x*k) div (k*y) = uu" + by (tactic {* test [@{simproc nat_divide_cancel_factor}] *}) fact + next + assume "(if k = 0 then 0 else Suc 0 div y) = uu" have "k div (k*y) = uu" + by (tactic {* test [@{simproc nat_divide_cancel_factor}] *}) fact + next + assume "(if b = 0 then 0 else a * c) = uu" have "(a*(b*c)) div (b) = uu" + by (tactic {* test [@{simproc nat_divide_cancel_factor}] *}) 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 {* test [@{simproc nat_divide_cancel_factor}] *}) fact + next + assume "k = 0 \ x dvd y" have "(x*k) dvd (k*y)" + by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact + next + assume "k = 0 \ Suc 0 dvd y" have "k dvd (k*y)" + by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact + next + assume "b = 0 \ a * c dvd Suc 0" have "(a*(b*c)) dvd (b)" + by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact + next + assume "b = 0 \ Suc 0 dvd a * c" have "b dvd (a*(b*c))" + by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact + next + assume "a = 0 \ b = 0 \ c dvd d * x" have "(a*(b*c)) dvd (d*b*(x*a))" + by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact + } end + +end