--- a/src/HOL/Numeral_Simprocs.thy Fri Nov 11 12:10:49 2011 +0100
+++ b/src/HOL/Numeral_Simprocs.thy Fri Nov 11 12:31:00 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,46 @@
"Suc m - n" | "m - Suc n") =
{* fn phi => Nat_Numeral_Simprocs.diff_cancel_numerals *}
+simproc_setup nat_eq_cancel_numeral_factor
+ ("(l::nat) * m = n" | "(l::nat) = m * n") =
+ {* fn phi => Nat_Numeral_Simprocs.eq_cancel_numeral_factor *}
+
+simproc_setup nat_less_cancel_numeral_factor
+ ("(l::nat) * m < n" | "(l::nat) < m * n") =
+ {* fn phi => Nat_Numeral_Simprocs.less_cancel_numeral_factor *}
+
+simproc_setup nat_le_cancel_numeral_factor
+ ("(l::nat) * m <= n" | "(l::nat) <= m * n") =
+ {* fn phi => Nat_Numeral_Simprocs.le_cancel_numeral_factor *}
+
+simproc_setup nat_div_cancel_numeral_factor
+ ("((l::nat) * m) div n" | "(l::nat) div (m * n)") =
+ {* fn phi => Nat_Numeral_Simprocs.div_cancel_numeral_factor *}
+
+simproc_setup nat_dvd_cancel_numeral_factor
+ ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
+ {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_numeral_factor *}
+
+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_div_cancel_factor
+ ("((l::nat) * m) div n" | "(l::nat) div (m * n)") =
+ {* fn phi => Nat_Numeral_Simprocs.div_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 +291,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/abel_cancel.ML Fri Nov 11 12:10:49 2011 +0100
+++ b/src/HOL/Tools/abel_cancel.ML Fri Nov 11 12:31:00 2011 +0100
@@ -24,6 +24,7 @@
add_atoms pos x #> add_atoms (not pos) y
| add_atoms pos (Const (@{const_name Groups.uminus}, _) $ x) =
add_atoms (not pos) x
+ | add_atoms pos (Const (@{const_name Groups.zero}, _)) = I
| add_atoms pos x = cons (pos, x);
fun atoms t = add_atoms true t [];
--- a/src/HOL/Tools/nat_numeral_simprocs.ML Fri Nov 11 12:10:49 2011 +0100
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Fri Nov 11 12:31:00 2011 +0100
@@ -5,16 +5,24 @@
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 cancel_numeral_factors: simproc list
+ val eq_cancel_numeral_factor: simpset -> cterm -> thm option
+ val less_cancel_numeral_factor: simpset -> cterm -> thm option
+ val le_cancel_numeral_factor: simpset -> cterm -> thm option
+ val div_cancel_numeral_factor: simpset -> cterm -> thm option
+ val dvd_cancel_numeral_factor: simpset -> cterm -> thm option
+ 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 div_cancel_factor: simpset -> cterm -> thm option
+ val dvd_cancel_factor: simpset -> cterm -> thm option
end;
-structure Nat_Numeral_Simprocs =
+structure Nat_Numeral_Simprocs : NAT_NUMERAL_SIMPROCS =
struct
(*Maps n to #n for n = 0, 1, 2*)
@@ -232,9 +240,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 ***)
@@ -298,24 +304,11 @@
val neg_exchanges = true
)
-val cancel_numeral_factors =
- map (Numeral_Simprocs.prep_simproc @{theory})
- [("nateq_cancel_numeral_factors",
- ["(l::nat) * m = n", "(l::nat) = m * n"],
- K EqCancelNumeralFactor.proc),
- ("natless_cancel_numeral_factors",
- ["(l::nat) * m < n", "(l::nat) < m * n"],
- K LessCancelNumeralFactor.proc),
- ("natle_cancel_numeral_factors",
- ["(l::nat) * m <= n", "(l::nat) <= m * n"],
- K LeCancelNumeralFactor.proc),
- ("natdiv_cancel_numeral_factors",
- ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
- K DivCancelNumeralFactor.proc),
- ("natdvd_cancel_numeral_factors",
- ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"],
- K DvdCancelNumeralFactor.proc)];
-
+fun eq_cancel_numeral_factor ss ct = EqCancelNumeralFactor.proc ss (term_of ct)
+fun less_cancel_numeral_factor ss ct = LessCancelNumeralFactor.proc ss (term_of ct)
+fun le_cancel_numeral_factor ss ct = LeCancelNumeralFactor.proc ss (term_of ct)
+fun div_cancel_numeral_factor ss ct = DivCancelNumeralFactor.proc ss (term_of ct)
+fun dvd_cancel_numeral_factor ss ct = DvdCancelNumeralFactor.proc ss (term_of ct)
(*** Applying ExtractCommonTermFun ***)
@@ -387,72 +380,10 @@
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 div_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:
-print_depth 22;
-set timing;
-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 12:10:49 2011 +0100
+++ b/src/HOL/ex/Simproc_Tests.thy Fri Nov 11 12:31:00 2011 +0100
@@ -5,7 +5,7 @@
header {* Testing of arithmetic simprocs *}
theory Simproc_Tests
-imports Rat
+imports Main
begin
text {*
@@ -21,12 +21,33 @@
fun test ps = CHANGED (asm_simp_tac (HOL_basic_ss addsimprocs ps) 1)
*}
+subsection {* Abelian group cancellation simprocs *}
+
+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 {* test [@{simproc abel_cancel_sum}] *}) fact
+ next
+ assume "a + 0 = b + 0" have "a + c = b + c"
+ by (tactic {* test [@{simproc abel_cancel_relation}] *}) fact
+ }
+end
+(* TODO: more tests for Groups.abel_cancel_{sum,relation} *)
subsection {* @{text int_combine_numerals} *}
+(* 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::number_ring"
{
+ assume "a + - b = u" have "(a + c) - (b + c) = u"
+ by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
+ next
assume "10 + (2 * l + oo) = uu"
have "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = uu"
by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
@@ -324,10 +345,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 +406,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 +615,101 @@
}
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_div_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_div_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_div_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_div_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
+
+subsection {* Numeral-cancellation simprocs for type @{typ nat} *}
+
+notepad begin
+ fix x y z :: nat
+ {
+ assume "3 * x = 4 * y" have "9*x = 12 * y"
+ by (tactic {* test [@{simproc nat_eq_cancel_numeral_factor}] *}) fact
+ next
+ assume "3 * x < 4 * y" have "9*x < 12 * y"
+ by (tactic {* test [@{simproc nat_less_cancel_numeral_factor}] *}) fact
+ next
+ assume "3 * x \<le> 4 * y" have "9*x \<le> 12 * y"
+ by (tactic {* test [@{simproc nat_le_cancel_numeral_factor}] *}) fact
+ next
+ assume "(3 * x) div (4 * y) = z" have "(9*x) div (12 * y) = z"
+ by (tactic {* test [@{simproc nat_div_cancel_numeral_factor}] *}) fact
+ next
+ assume "(3 * x) dvd (4 * y)" have "(9*x) dvd (12 * y)"
+ by (tactic {* test [@{simproc nat_dvd_cancel_numeral_factor}] *}) fact
+ }
+end
+
+end