--- a/src/HOL/Algebra/IntRing.thy Tue Feb 17 18:45:41 2009 +0100
+++ b/src/HOL/Algebra/IntRing.thy Tue Feb 17 21:51:52 2009 +0100
@@ -407,7 +407,7 @@
hence "b mod m = (x * m + a) mod m" by simp
also
- have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: zmod_zadd1_eq)
+ have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: mod_add_eq)
also
have "\<dots> = a mod m" by simp
finally
--- a/src/HOL/Decision_Procs/cooper_tac.ML Tue Feb 17 18:45:41 2009 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Tue Feb 17 21:51:52 2009 +0100
@@ -30,7 +30,7 @@
val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
-val int_mod_add_eq = @{thm zmod_zadd1_eq} RS sym;
+val int_mod_add_eq = @{thm mod_add_eq} RS sym;
val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
val nat_div_add_eq = @{thm div_add1_eq} RS sym;
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Tue Feb 17 18:45:41 2009 +0100
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Tue Feb 17 21:51:52 2009 +0100
@@ -34,7 +34,7 @@
val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
-val int_mod_add_eq = @{thm zmod_zadd1_eq} RS sym;
+val int_mod_add_eq = @{thm mod_add_eq} RS sym;
val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
val nat_div_add_eq = @{thm div_add1_eq} RS sym;
--- a/src/HOL/Decision_Procs/mir_tac.ML Tue Feb 17 18:45:41 2009 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML Tue Feb 17 21:51:52 2009 +0100
@@ -49,7 +49,7 @@
val nat_mod_add_eq = @{thm "mod_add1_eq"} RS sym;
val nat_mod_add_left_eq = @{thm "mod_add_left_eq"} RS sym;
val nat_mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym;
-val int_mod_add_eq = @{thm "zmod_zadd1_eq"} RS sym;
+val int_mod_add_eq = @{thm "mod_add_eq"} RS sym;
val int_mod_add_left_eq = @{thm "zmod_zadd_left_eq"} RS sym;
val int_mod_add_right_eq = @{thm "zmod_zadd_right_eq"} RS sym;
val nat_div_add_eq = @{thm "div_add1_eq"} RS sym;
--- a/src/HOL/Divides.thy Tue Feb 17 18:45:41 2009 +0100
+++ b/src/HOL/Divides.thy Tue Feb 17 21:51:52 2009 +0100
@@ -173,7 +173,7 @@
qed
lemma dvd_imp_mod_0: "a dvd b \<Longrightarrow> b mod a = 0"
-by (unfold dvd_def, auto)
+by (rule dvd_eq_mod_eq_0[THEN iffD1])
lemma dvd_div_mult_self: "a dvd b \<Longrightarrow> (b div a) * a = b"
by (subst (2) mod_div_equality [of b a, symmetric]) (simp add:dvd_imp_mod_0)
--- a/src/HOL/IntDiv.thy Tue Feb 17 18:45:41 2009 +0100
+++ b/src/HOL/IntDiv.thy Tue Feb 17 21:51:52 2009 +0100
@@ -451,9 +451,6 @@
lemma zmod_zero [simp]: "(0::int) mod b = 0"
by (simp add: mod_def divmod_def)
-lemma zdiv_minus1: "(0::int) < b ==> -1 div b = -1"
-by (simp add: div_def divmod_def)
-
lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
by (simp add: mod_def divmod_def)
@@ -729,18 +726,6 @@
apply (blast intro: divmod_rel_div_mod [THEN zmult1_lemma, THEN divmod_rel_mod])
done
-lemma zmod_zmult1_eq': "(a*b) mod (c::int) = ((a mod c) * b) mod c"
-apply (rule trans)
-apply (rule_tac s = "b*a mod c" in trans)
-apply (rule_tac [2] zmod_zmult1_eq)
-apply (simp_all add: mult_commute)
-done
-
-lemma zmod_zmult_distrib: "(a*b) mod (c::int) = ((a mod c) * (b mod c)) mod c"
-apply (rule zmod_zmult1_eq' [THEN trans])
-apply (rule zmod_zmult1_eq)
-done
-
lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a"
by (simp add: zdiv_zmult1_eq)
@@ -749,11 +734,6 @@
apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
done
-lemma zmod_zmod_trivial: "(a mod b) mod b = a mod (b::int)"
-apply (case_tac "b = 0", simp)
-apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial)
-done
-
text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
lemma zadd1_lemma:
@@ -768,11 +748,6 @@
apply (blast intro: zadd1_lemma [OF divmod_rel_div_mod divmod_rel_div_mod] divmod_rel_div)
done
-lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c"
-apply (case_tac "c = 0", simp)
-apply (blast intro: zadd1_lemma [OF divmod_rel_div_mod divmod_rel_div_mod] divmod_rel_mod)
-done
-
instance int :: ring_div
proof
fix a b c :: int
@@ -971,7 +946,7 @@
P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
apply (rule iffI, clarify)
apply (erule_tac P="P ?x ?y" in rev_mp)
- apply (subst zmod_zadd1_eq)
+ apply (subst mod_add_eq)
apply (subst zdiv_zadd1_eq)
apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)
txt{*converse direction*}
@@ -984,7 +959,7 @@
P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
apply (rule iffI, clarify)
apply (erule_tac P="P ?x ?y" in rev_mp)
- apply (subst zmod_zadd1_eq)
+ apply (subst mod_add_eq)
apply (subst zdiv_zadd1_eq)
apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)
txt{*converse direction*}
@@ -1057,11 +1032,6 @@
simp)
done
-(*Not clear why this must be proved separately; probably number_of causes
- simplification problems*)
-lemma not_0_le_lemma: "~ 0 \<le> x ==> x \<le> (0::int)"
-by auto
-
lemma zdiv_number_of_Bit0 [simp]:
"number_of (Int.Bit0 v) div number_of (Int.Bit0 w) =
number_of v div (number_of w :: int)"
@@ -1088,7 +1058,7 @@
apply (rule_tac [2] mult_left_mono)
apply (auto simp add: add_commute [of 1] mult_commute add1_zle_eq
pos_mod_bound)
-apply (subst zmod_zadd1_eq)
+apply (subst mod_add_eq)
apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial)
apply (rule mod_pos_pos_trivial)
apply (auto simp add: mod_pos_pos_trivial ring_distribs)
@@ -1111,7 +1081,7 @@
(2::int) * (number_of v mod number_of w)"
apply (simp only: number_of_eq numeral_simps)
apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2
- not_0_le_lemma neg_zmod_mult_2 add_ac)
+ neg_zmod_mult_2 add_ac)
done
lemma zmod_number_of_Bit1 [simp]:
@@ -1121,7 +1091,7 @@
else 2 * ((number_of v + (1::int)) mod number_of w) - 1)"
apply (simp only: number_of_eq numeral_simps)
apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2
- not_0_le_lemma neg_zmod_mult_2 add_ac)
+ neg_zmod_mult_2 add_ac)
done
@@ -1131,7 +1101,7 @@
apply (subgoal_tac "a div b \<le> -1", force)
apply (rule order_trans)
apply (rule_tac a' = "-1" in zdiv_mono1)
-apply (auto simp add: zdiv_minus1)
+apply (auto simp add: div_eq_minus1)
done
lemma div_nonneg_neg_le0: "[| (0::int) \<le> a; b < 0 |] ==> a div b \<le> 0"
@@ -1177,23 +1147,23 @@
lemma zdvd_1_left: "1 dvd (m::int)"
by (rule one_dvd) (* already declared [simp] *)
-lemma zdvd_refl [simp]: "m dvd (m::int)"
- by (rule dvd_refl) (* TODO: declare generic dvd_refl [simp] *)
+lemma zdvd_refl: "m dvd (m::int)"
+ by (rule dvd_refl) (* already declared [simp] *)
lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
by (rule dvd_trans)
-lemma zdvd_zminus_iff[simp]: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
- by (rule dvd_minus_iff)
+lemma zdvd_zminus_iff: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
+ by (rule dvd_minus_iff) (* already declared [simp] *)
-lemma zdvd_zminus2_iff[simp]: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
- by (rule minus_dvd_iff)
+lemma zdvd_zminus2_iff: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
+ by (rule minus_dvd_iff) (* already declared [simp] *)
-lemma zdvd_abs1[simp]: "( \<bar>i::int\<bar> dvd j) = (i dvd j)"
- by (cases "i > 0") (simp_all add: zdvd_zminus2_iff)
+lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)"
+ by (rule abs_dvd_iff) (* already declared [simp] *)
-lemma zdvd_abs2[simp]: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)"
- by (cases "j > 0") (simp_all add: zdvd_zminus_iff)
+lemma zdvd_abs2: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)"
+ by (rule dvd_abs_iff) (* already declared [simp] *)
lemma zdvd_anti_sym:
"0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
@@ -1379,7 +1349,7 @@
apply (induct "y", auto)
apply (rule zmod_zmult1_eq [THEN trans])
apply (simp (no_asm_simp))
-apply (rule zmod_zmult_distrib [symmetric])
+apply (rule mod_mult_eq [symmetric])
done
lemma zdiv_int: "int (a div b) = (int a) div (int b)"
@@ -1420,7 +1390,7 @@
IntDiv.zmod_zadd_left_eq [symmetric]
IntDiv.zmod_zadd_right_eq [symmetric]
IntDiv.zmod_zmult1_eq [symmetric]
- IntDiv.zmod_zmult1_eq' [symmetric]
+ mod_mult_left_eq [symmetric]
IntDiv.zpower_zmod
zminus_zmod zdiff_zmod_left zdiff_zmod_right
--- a/src/HOL/NumberTheory/Chinese.thy Tue Feb 17 18:45:41 2009 +0100
+++ b/src/HOL/NumberTheory/Chinese.thy Tue Feb 17 21:51:52 2009 +0100
@@ -101,7 +101,7 @@
apply (induct l)
apply auto
apply (rule trans)
- apply (rule zmod_zadd1_eq)
+ apply (rule mod_add_eq)
apply simp
apply (rule zmod_zadd_right_eq [symmetric])
done
@@ -237,10 +237,10 @@
apply (unfold lincong_sol_def)
apply safe
apply (tactic {* stac (thm "zcong_zmod") 3 *})
- apply (tactic {* stac (thm "zmod_zmult_distrib") 3 *})
+ apply (tactic {* stac (thm "mod_mult_eq") 3 *})
apply (tactic {* stac (thm "zmod_zdvd_zmod") 3 *})
apply (tactic {* stac (thm "x_sol_lin") 5 *})
- apply (tactic {* stac (thm "zmod_zmult_distrib" RS sym) 7 *})
+ apply (tactic {* stac (thm "mod_mult_eq" RS sym) 7 *})
apply (tactic {* stac (thm "zcong_zmod" RS sym) 7 *})
apply (subgoal_tac [7]
"0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
--- a/src/HOL/NumberTheory/IntPrimes.thy Tue Feb 17 18:45:41 2009 +0100
+++ b/src/HOL/NumberTheory/IntPrimes.thy Tue Feb 17 21:51:52 2009 +0100
@@ -88,7 +88,7 @@
lemma zgcd_zadd_zmult [simp]: "zgcd (m + n * k) n = zgcd m n"
apply (rule zgcd_eq [THEN trans])
- apply (simp add: zmod_zadd1_eq)
+ apply (simp add: mod_add_eq)
apply (rule zgcd_eq [symmetric])
done
--- a/src/HOL/NumberTheory/Residues.thy Tue Feb 17 18:45:41 2009 +0100
+++ b/src/HOL/NumberTheory/Residues.thy Tue Feb 17 21:51:52 2009 +0100
@@ -53,7 +53,7 @@
lemma StandardRes_prop4: "2 < m
==> [StandardRes m x * StandardRes m y = (x * y)] (mod m)"
by (auto simp add: StandardRes_def zcong_zmod_eq
- zmod_zmult_distrib [of x y m])
+ mod_mult_eq [of x y m])
lemma StandardRes_lbound: "0 < p ==> 0 \<le> StandardRes p x"
by (auto simp add: StandardRes_def pos_mod_sign)
--- a/src/HOL/Ring_and_Field.thy Tue Feb 17 18:45:41 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy Tue Feb 17 21:51:52 2009 +0100
@@ -1100,32 +1100,11 @@
"sgn a < 0 \<longleftrightarrow> a < 0"
unfolding sgn_if by auto
-(* The int instances are proved, these generic ones are tedious to prove here.
-And not very useful, as int seems to be the only instance.
-If needed, they should be proved later, when metis is available.
-lemma dvd_abs[simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k"
-proof-
- have "\<forall>k.\<exists>ka. - (m * k) = m * ka"
- by(simp add: mult_minus_right[symmetric] del: mult_minus_right)
- moreover
- have "\<forall>k.\<exists>ka. m * k = - (m * ka)"
- by(auto intro!: minus_minus[symmetric]
- simp add: mult_minus_right[symmetric] simp del: mult_minus_right)
- ultimately show ?thesis by (auto simp: abs_if dvd_def)
-qed
-
-lemma dvd_abs2[simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
-proof-
- have "\<forall>k.\<exists>ka. - (m * k) = m * ka"
- by(simp add: mult_minus_right[symmetric] del: mult_minus_right)
- moreover
- have "\<forall>k.\<exists>ka. - (m * ka) = m * k"
- by(auto intro!: minus_minus
- simp add: mult_minus_right[symmetric] simp del: mult_minus_right)
- ultimately show ?thesis
- by (auto simp add:abs_if dvd_def minus_equation_iff[of k])
-qed
-*)
+lemma abs_dvd_iff [simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k"
+ by (simp add: abs_if)
+
+lemma dvd_abs_iff [simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
+ by (simp add: abs_if)
end
--- a/src/HOL/Tools/Qelim/presburger.ML Tue Feb 17 18:45:41 2009 +0100
+++ b/src/HOL/Tools/Qelim/presburger.ML Tue Feb 17 21:51:52 2009 +0100
@@ -124,7 +124,7 @@
@ map (symmetric o mk_meta_eq)
[@{thm "dvd_eq_mod_eq_0"}, @{thm "zdvd_iff_zmod_eq_0"}, @{thm "mod_add1_eq"},
@{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"},
- @{thm "zmod_zadd1_eq"}, @{thm "zmod_zadd_left_eq"},
+ @{thm "mod_add_eq"}, @{thm "zmod_zadd_left_eq"},
@{thm "zmod_zadd_right_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
@ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"},
@{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1,
--- a/src/HOL/Word/Num_Lemmas.thy Tue Feb 17 18:45:41 2009 +0100
+++ b/src/HOL/Word/Num_Lemmas.thy Tue Feb 17 21:51:52 2009 +0100
@@ -121,8 +121,8 @@
lemma zmod_zsub_distrib: "((a::int) - b) mod c = (a mod c - b mod c) mod c"
apply (unfold diff_int_def)
- apply (rule trans [OF _ zmod_zadd1_eq [symmetric]])
- apply (simp add: zmod_uminus zmod_zadd1_eq [symmetric])
+ apply (rule trans [OF _ mod_add_eq [symmetric]])
+ apply (simp add: zmod_uminus mod_add_eq [symmetric])
done
lemma zmod_zsub_right_eq: "((a::int) - b) mod c = (a - b mod c) mod c"
@@ -162,8 +162,8 @@
lemmas nat_minus_mod_plus_right = trans [OF nat_minus_mod mod_0 [symmetric],
THEN mod_plus_right [THEN iffD2], standard, simplified]
-lemmas push_mods' = zmod_zadd1_eq [standard]
- zmod_zmult_distrib [standard] zmod_zsub_distrib [standard]
+lemmas push_mods' = mod_add_eq [standard]
+ mod_mult_eq [standard] zmod_zsub_distrib [standard]
zmod_uminus [symmetric, standard]
lemmas push_mods = push_mods' [THEN eq_reflection, standard]
--- a/src/HOL/Word/WordGenLib.thy Tue Feb 17 18:45:41 2009 +0100
+++ b/src/HOL/Word/WordGenLib.thy Tue Feb 17 21:51:52 2009 +0100
@@ -293,9 +293,9 @@
shows "(x + y) mod b = z' mod b'"
proof -
from 1 2[symmetric] 3[symmetric] have "(x + y) mod b = (x' mod b' + y' mod b') mod b'"
- by (simp add: zmod_zadd1_eq[symmetric])
+ by (simp add: mod_add_eq[symmetric])
also have "\<dots> = (x' + y') mod b'"
- by (simp add: zmod_zadd1_eq[symmetric])
+ by (simp add: mod_add_eq[symmetric])
finally show ?thesis by (simp add: 4)
qed