--- 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},
--- 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)";
*)
--- 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 \<or> x = y" have "x*k = k*y"
+ by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
+ next
+ assume "k = 0 \<or> Suc 0 = y" have "k = k*y"
+ by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
+ next
+ assume "b = 0 \<or> a * c = Suc 0" have "a*(b*c) = b"
+ by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
+ next
+ assume "a = 0 \<or> b = 0 \<or> c = d * x" have "a*(b*c) = d*b*(x*a)"
+ by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
+ next
+ assume "0 < k \<and> x < y" have "x*k < k*y"
+ by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
+ next
+ assume "0 < k \<and> Suc 0 < y" have "k < k*y"
+ by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
+ next
+ assume "0 < b \<and> a * c < Suc 0" have "a*(b*c) < b"
+ by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
+ next
+ assume "0 < a \<and> 0 < b \<and> c < d * x" have "a*(b*c) < d*b*(x*a)"
+ by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
+ next
+ assume "0 < k \<longrightarrow> x \<le> y" have "x*k \<le> k*y"
+ by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
+ next
+ assume "0 < k \<longrightarrow> Suc 0 \<le> y" have "k \<le> k*y"
+ by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
+ next
+ assume "0 < b \<longrightarrow> a * c \<le> Suc 0" have "a*(b*c) \<le> b"
+ by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
+ next
+ assume "0 < a \<longrightarrow> 0 < b \<longrightarrow> c \<le> d * x" have "a*(b*c) \<le> 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 \<or> x dvd y" have "(x*k) dvd (k*y)"
+ by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
+ next
+ assume "k = 0 \<or> Suc 0 dvd y" have "k dvd (k*y)"
+ by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
+ next
+ assume "b = 0 \<or> a * c dvd Suc 0" have "(a*(b*c)) dvd (b)"
+ by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
+ next
+ assume "b = 0 \<or> Suc 0 dvd a * c" have "b dvd (a*(b*c))"
+ by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
+ next
+ assume "a = 0 \<or> b = 0 \<or> c dvd d * x" have "(a*(b*c)) dvd (d*b*(x*a))"
+ by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
+ }
end
+
+end