--- a/src/HOL/Decision_Procs/cooper_tac.ML Fri Feb 20 21:29:34 2009 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Fri Feb 20 23:46:03 2009 +0100
@@ -77,7 +77,7 @@
@{thm mod_self}, @{thm "zmod_self"},
@{thm mod_by_0}, @{thm div_by_0},
@{thm "zdiv_zero"}, @{thm "zmod_zero"}, @{thm "div_0"}, @{thm "mod_0"},
- @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},
+ @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
Suc_plus1]
addsimps @{thms add_ac}
addsimprocs [cancel_div_mod_proc]
--- a/src/HOL/Decision_Procs/mir_tac.ML Fri Feb 20 21:29:34 2009 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML Fri Feb 20 23:46:03 2009 +0100
@@ -99,7 +99,7 @@
addsimps [refl,nat_mod_add_eq,
@{thm "mod_self"}, @{thm "zmod_self"},
@{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"},
- @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},
+ @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
@{thm "Suc_plus1"}]
addsimps @{thms add_ac}
addsimprocs [cancel_div_mod_proc]
--- a/src/HOL/Groebner_Basis.thy Fri Feb 20 21:29:34 2009 +0100
+++ b/src/HOL/Groebner_Basis.thy Fri Feb 20 23:46:03 2009 +0100
@@ -448,8 +448,8 @@
declare zmod_zminus2[algebra]
declare zdiv_zero[algebra]
declare zmod_zero[algebra]
-declare zmod_1[algebra]
-declare zdiv_1[algebra]
+declare mod_by_1[algebra]
+declare div_by_1[algebra]
declare zmod_minus1_right[algebra]
declare zdiv_minus1_right[algebra]
declare mod_div_trivial[algebra]
--- a/src/HOL/IntDiv.thy Fri Feb 20 21:29:34 2009 +0100
+++ b/src/HOL/IntDiv.thy Fri Feb 20 23:46:03 2009 +0100
@@ -547,34 +547,6 @@
simproc_setup binary_int_mod ("number_of m mod number_of n :: int") =
{* K (divmod_proc (@{thm divmod_rel_mod_eq})) *}
-(* The following 8 lemmas are made unnecessary by the above simprocs: *)
-
-lemmas div_pos_pos_number_of =
- div_pos_pos [of "number_of v" "number_of w", standard]
-
-lemmas div_neg_pos_number_of =
- div_neg_pos [of "number_of v" "number_of w", standard]
-
-lemmas div_pos_neg_number_of =
- div_pos_neg [of "number_of v" "number_of w", standard]
-
-lemmas div_neg_neg_number_of =
- div_neg_neg [of "number_of v" "number_of w", standard]
-
-
-lemmas mod_pos_pos_number_of =
- mod_pos_pos [of "number_of v" "number_of w", standard]
-
-lemmas mod_neg_pos_number_of =
- mod_neg_pos [of "number_of v" "number_of w", standard]
-
-lemmas mod_pos_neg_number_of =
- mod_pos_neg [of "number_of v" "number_of w", standard]
-
-lemmas mod_neg_neg_number_of =
- mod_neg_neg [of "number_of v" "number_of w", standard]
-
-
lemmas posDivAlg_eqn_number_of [simp] =
posDivAlg_eqn [of "number_of v" "number_of w", standard]
@@ -584,15 +556,6 @@
text{*Special-case simplification *}
-lemma zmod_1 [simp]: "a mod (1::int) = 0"
-apply (cut_tac a = a and b = 1 in pos_mod_sign)
-apply (cut_tac [2] a = a and b = 1 in pos_mod_bound)
-apply (auto simp del:pos_mod_bound pos_mod_sign)
-done
-
-lemma zdiv_1 [simp]: "a div (1::int) = a"
-by (cut_tac a = a and b = 1 in zmod_zdiv_equality, auto)
-
lemma zmod_minus1_right [simp]: "a mod (-1::int) = 0"
apply (cut_tac a = a and b = "-1" in neg_mod_sign)
apply (cut_tac [2] a = a and b = "-1" in neg_mod_bound)
--- a/src/HOL/Presburger.thy Fri Feb 20 21:29:34 2009 +0100
+++ b/src/HOL/Presburger.thy Fri Feb 20 23:46:03 2009 +0100
@@ -412,14 +412,10 @@
"(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
by (rule eq_number_of_eq)
-lemma mod_eq0_dvd_iff[presburger]: "(m::nat) mod n = 0 \<longleftrightarrow> n dvd m"
-unfolding dvd_eq_mod_eq_0[symmetric] ..
-
-lemma zmod_eq0_zdvd_iff[presburger]: "(m::int) mod n = 0 \<longleftrightarrow> n dvd m"
-unfolding zdvd_iff_zmod_eq_0[symmetric] ..
+declare dvd_eq_mod_eq_0[symmetric, presburger]
declare mod_1[presburger]
declare mod_0[presburger]
-declare zmod_1[presburger]
+declare mod_by_1[presburger]
declare zmod_zero[presburger]
declare zmod_self[presburger]
declare mod_self[presburger]
--- a/src/HOL/Tools/Qelim/presburger.ML Fri Feb 20 21:29:34 2009 +0100
+++ b/src/HOL/Tools/Qelim/presburger.ML Fri Feb 20 23:46:03 2009 +0100
@@ -129,7 +129,7 @@
@ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"},
@{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1,
@{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"},
- @{thm "div_0"}, @{thm "mod_0"}, @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"},
+ @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"},
@{thm "mod_1"}, @{thm "Suc_plus1"}]
@ @{thms add_ac}
addsimprocs [cancel_div_mod_proc]
--- a/src/HOL/Tools/int_factor_simprocs.ML Fri Feb 20 21:29:34 2009 +0100
+++ b/src/HOL/Tools/int_factor_simprocs.ML Fri Feb 20 23:46:03 2009 +0100
@@ -216,7 +216,7 @@
(** Final simplification for the CancelFactor simprocs **)
val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq
- [@{thm mult_1_left}, @{thm mult_1_right}, @{thm zdiv_1}, @{thm numeral_1_eq_1}];
+ [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}];
fun cancel_simplify_meta_eq cancel_th ss th =
simplify_one ss (([th, cancel_th]) MRS trans);
--- a/src/HOL/Word/Num_Lemmas.thy Fri Feb 20 21:29:34 2009 +0100
+++ b/src/HOL/Word/Num_Lemmas.thy Fri Feb 20 23:46:03 2009 +0100
@@ -95,7 +95,7 @@
lemma z1pdiv2:
"(2 * b + 1) div 2 = (b::int)" by arith
-lemmas zdiv_le_dividend = xtr3 [OF zdiv_1 [symmetric] zdiv_mono2,
+lemmas zdiv_le_dividend = xtr3 [OF div_by_1 [symmetric] zdiv_mono2,
simplified int_one_le_iff_zero_less, simplified, standard]
lemma axxbyy: