--- a/NEWS Wed Mar 28 00:18:11 2012 +0200
+++ b/NEWS Wed Mar 28 08:25:51 2012 +0200
@@ -146,7 +146,22 @@
zmod_self ~> mod_self
zdiv_zero ~> div_0
zmod_zero ~> mod_0
+ zdiv_zmod_equality ~> div_mod_equality2
+ zdiv_zmod_equality2 ~> div_mod_equality
zmod_zdiv_trivial ~> mod_div_trivial
+ zdiv_zminus_zminus ~> div_minus_minus
+ zmod_zminus_zminus ~> mod_minus_minus
+ zdiv_zminus2 ~> div_minus_right
+ zmod_zminus2 ~> mod_minus_right
+ zdiv_minus1_right ~> div_minus1_right
+ zmod_minus1_right ~> mod_minus1_right
+ zdvd_mult_div_cancel ~> dvd_mult_div_cancel
+ zmod_zmult1_eq ~> mod_mult_right_eq
+ zpower_zmod ~> power_mod
+ zdvd_zmod ~> dvd_mod
+ zdvd_zmod_imp_zdvd ~> dvd_mod_imp_dvd
+ mod_mult_distrib ~> mult_mod_left
+ mod_mult_distrib2 ~> mult_mod_right
* More default pred/set conversions on a couple of relation operations
and predicates. Consolidation of some relation theorems:
--- a/src/HOL/Divides.thy Wed Mar 28 00:18:11 2012 +0200
+++ b/src/HOL/Divides.thy Wed Mar 28 08:25:51 2012 +0200
@@ -283,6 +283,15 @@
by (simp only: mod_mult_eq [symmetric])
qed
+text {* Exponentiation respects modular equivalence. *}
+
+lemma power_mod: "(a mod b)^n mod b = a^n mod b"
+apply (induct n, simp_all)
+apply (rule mod_mult_right_eq [THEN trans])
+apply (simp (no_asm_simp))
+apply (rule mod_mult_eq [symmetric])
+done
+
lemma mod_mod_cancel:
assumes "c dvd b"
shows "a mod b mod c = a mod c"
@@ -343,6 +352,12 @@
"(a * c) mod (b * c) = (a mod b) * c"
using mod_mult_mult1 [of c a b] by (simp add: mult_commute)
+lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)"
+ by (fact mod_mult_mult2 [symmetric])
+
+lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
+ by (fact mod_mult_mult1 [symmetric])
+
lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
unfolding dvd_def by (auto simp add: mod_mult_mult1)
@@ -444,6 +459,25 @@
apply simp
done
+lemma div_minus_minus [simp]: "(-a) div (-b) = a div b"
+ using div_mult_mult1 [of "- 1" a b]
+ unfolding neg_equal_0_iff_equal by simp
+
+lemma mod_minus_minus [simp]: "(-a) mod (-b) = - (a mod b)"
+ using mod_mult_mult1 [of "- 1" a b] by simp
+
+lemma div_minus_right: "a div (-b) = (-a) div b"
+ using div_minus_minus [of "-a" b] by simp
+
+lemma mod_minus_right: "a mod (-b) = - ((-a) mod b)"
+ using mod_minus_minus [of "-a" b] by simp
+
+lemma div_minus1_right [simp]: "a div (-1) = -a"
+ using div_minus_right [of a 1] by simp
+
+lemma mod_minus1_right [simp]: "a mod (-1) = 0"
+ using mod_minus_right [of a 1] by simp
+
end
@@ -712,12 +746,6 @@
lemma mod_1 [simp]: "m mod Suc 0 = 0"
by (induct m) (simp_all add: mod_geq)
-lemma mod_mult_distrib: "(m mod n) * (k\<Colon>nat) = (m * k) mod (n * k)"
- by (fact mod_mult_mult2 [symmetric]) (* FIXME: generalize *)
-
-lemma mod_mult_distrib2: "(k::nat) * (m mod n) = (k*m) mod (k*n)"
- by (fact mod_mult_mult1 [symmetric]) (* FIXME: generalize *)
-
(* a simple rearrangement of mod_div_equality: *)
lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
using mod_div_equality2 [of n m] by arith
@@ -1408,12 +1436,6 @@
lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
by (fact mod_div_equality2 [symmetric])
-lemma zdiv_zmod_equality: "(b * (a div b) + (a mod b)) + k = (a::int)+k"
- by (fact div_mod_equality2)
-
-lemma zdiv_zmod_equality2: "((a div b) * b + (a mod b)) + k = (a::int)+k"
- by (fact div_mod_equality)
-
text {* Tool setup *}
(* FIXME: Theorem list add_0s doesn't exist, because Numeral0 has gone. *)
@@ -1428,7 +1450,7 @@
val mk_sum = Arith_Data.mk_sum HOLogic.intT;
val dest_sum = Arith_Data.dest_sum;
- val div_mod_eqs = map mk_meta_eq [@{thm zdiv_zmod_equality}, @{thm zdiv_zmod_equality2}];
+ val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
(@{thm diff_minus} :: @{thms add_0s} @ @{thms add_ac}))
@@ -1489,15 +1511,6 @@
text{*There is no @{text mod_neg_pos_trivial}.*}
-(*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*)
-lemma zdiv_zminus_zminus [simp]: "(-a) div (-b) = a div (b::int)"
- using div_mult_mult1 [of "-1" a b] by simp (* FIXME: generalize *)
-
-(*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*)
-lemma zmod_zminus_zminus [simp]: "(-a) mod (-b) = - (a mod (b::int))"
- using mod_mult_mult1 [of "-1" a b] by simp (* FIXME: generalize *)
-
-
subsubsection {* Laws for div and mod with Unary Minus *}
lemma zminus1_lemma:
@@ -1524,21 +1537,15 @@
shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
unfolding zmod_zminus1_eq_if by auto
-lemma zdiv_zminus2: "a div (-b) = (-a::int) div b"
- using zdiv_zminus_zminus [of "-a" b] by simp (* FIXME: generalize *)
-
-lemma zmod_zminus2: "a mod (-b) = - ((-a::int) mod b)"
- using zmod_zminus_zminus [of "-a" b] by simp (* FIXME: generalize*)
-
lemma zdiv_zminus2_eq_if:
"b \<noteq> (0::int)
==> a div (-b) =
(if a mod b = 0 then - (a div b) else - (a div b) - 1)"
-by (simp add: zdiv_zminus1_eq_if zdiv_zminus2)
+by (simp add: zdiv_zminus1_eq_if div_minus_right)
lemma zmod_zminus2_eq_if:
"a mod (-b::int) = (if a mod b = 0 then 0 else (a mod b) - b)"
-by (simp add: zmod_zminus1_eq_if zmod_zminus2)
+by (simp add: zmod_zminus1_eq_if mod_minus_right)
lemma zmod_zminus2_not_zero:
fixes k l :: int
@@ -1663,16 +1670,6 @@
text{*Special-case simplification *}
-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)
-apply (auto simp del: neg_mod_sign neg_mod_bound)
-done (* FIXME: generalize *)
-
-lemma zdiv_minus1_right [simp]: "a div (-1::int) = -a"
-by (cut_tac a = a and b = "-1" in zmod_zdiv_equality, auto)
-(* FIXME: generalize *)
-
(** The last remaining special cases for constant arithmetic:
1 div z and 1 mod z **)
@@ -1792,9 +1789,6 @@
apply (blast intro: divmod_int_rel_div_mod [THEN zmult1_lemma, THEN div_int_unique])
done
-lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)"
- by (fact mod_mult_right_eq) (* FIXME: delete *)
-
text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
lemma zadd1_lemma:
@@ -1989,44 +1983,30 @@
declare split_zmod [of _ _ "numeral k", arith_split] for k
-subsubsection {* Speeding up the Division Algorithm with Shifting *}
+subsubsection {* Computing @{text "div"} and @{text "mod"} with shifting *}
+
+lemma pos_divmod_int_rel_mult_2:
+ assumes "0 \<le> b"
+ assumes "divmod_int_rel a b (q, r)"
+ shows "divmod_int_rel (1 + 2*a) (2*b) (q, 1 + 2*r)"
+ using assms unfolding divmod_int_rel_def by auto
+
+lemma neg_divmod_int_rel_mult_2:
+ assumes "b \<le> 0"
+ assumes "divmod_int_rel (a + 1) b (q, r)"
+ shows "divmod_int_rel (1 + 2*a) (2*b) (q, 2*r - 1)"
+ using assms unfolding divmod_int_rel_def by auto
text{*computing div by shifting *}
lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"
-proof cases
- assume "a=0"
- thus ?thesis by simp
-next
- assume "a\<noteq>0" and le_a: "0\<le>a"
- hence a_pos: "1 \<le> a" by arith
- hence one_less_a2: "1 < 2 * a" by arith
- hence le_2a: "2 * (1 + b mod a) \<le> 2 * a"
- unfolding mult_le_cancel_left
- by (simp add: add1_zle_eq add_commute [of 1])
- with a_pos have "0 \<le> b mod a" by simp
- hence le_addm: "0 \<le> 1 mod (2*a) + 2*(b mod a)"
- by (simp add: mod_pos_pos_trivial one_less_a2)
- with le_2a
- have "(1 mod (2*a) + 2*(b mod a)) div (2*a) = 0"
- by (simp add: div_pos_pos_trivial le_addm mod_pos_pos_trivial one_less_a2
- right_distrib)
- thus ?thesis
- by (subst zdiv_zadd1_eq,
- simp add: mod_mult_mult1 one_less_a2
- div_pos_pos_trivial)
-qed
+ using pos_divmod_int_rel_mult_2 [OF _ divmod_int_rel_div_mod]
+ by (rule div_int_unique)
lemma neg_zdiv_mult_2:
assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"
-proof -
- have R: "1 + - (2 * (b + 1)) = - (1 + 2 * b)" by simp
- have "(1 + 2 * (-b - 1)) div (2 * (-a)) = (-b - 1) div (-a)"
- by (rule pos_zdiv_mult_2, simp add: A)
- thus ?thesis
- by (simp only: R zdiv_zminus_zminus diff_minus
- minus_add_distrib [symmetric] mult_minus_right)
-qed
+ using neg_divmod_int_rel_mult_2 [OF A divmod_int_rel_div_mod]
+ by (rule div_int_unique)
(* FIXME: add rules for negative numerals *)
lemma zdiv_numeral_Bit0 [simp]:
@@ -2042,39 +2022,19 @@
unfolding mult_2 [symmetric] add_commute [of _ 1]
by (rule pos_zdiv_mult_2, simp)
-
-subsubsection {* Computing mod by Shifting (proofs resemble those for div) *}
-
lemma pos_zmod_mult_2:
fixes a b :: int
assumes "0 \<le> a"
shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)"
-proof (cases "0 < a")
- case False with assms show ?thesis by simp
-next
- case True
- then have "b mod a < a" by (rule pos_mod_bound)
- then have "1 + b mod a \<le> a" by simp
- then have A: "2 * (1 + b mod a) \<le> 2 * a" by simp
- from `0 < a` have "0 \<le> b mod a" by (rule pos_mod_sign)
- then have B: "0 \<le> 1 + 2 * (b mod a)" by simp
- have "((1\<Colon>int) mod ((2\<Colon>int) * a) + (2\<Colon>int) * b mod ((2\<Colon>int) * a)) mod ((2\<Colon>int) * a) = (1\<Colon>int) + (2\<Colon>int) * (b mod a)"
- using `0 < a` and A
- by (auto simp add: mod_mult_mult1 mod_pos_pos_trivial ring_distribs intro!: mod_pos_pos_trivial B)
- then show ?thesis by (subst mod_add_eq)
-qed
+ using pos_divmod_int_rel_mult_2 [OF assms divmod_int_rel_div_mod]
+ by (rule mod_int_unique)
lemma neg_zmod_mult_2:
fixes a b :: int
assumes "a \<le> 0"
shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1"
-proof -
- from assms have "0 \<le> - a" by auto
- then have "(1 + 2 * (- b - 1)) mod (2 * (- a)) = 1 + 2 * ((- b - 1) mod (- a))"
- by (rule pos_zmod_mult_2)
- then show ?thesis by (simp add: zmod_zminus2 algebra_simps)
- (simp add: diff_minus add_ac)
-qed
+ using neg_divmod_int_rel_mult_2 [OF assms divmod_int_rel_div_mod]
+ by (rule mod_int_unique)
(* FIXME: add rules for negative numerals *)
lemma zmod_numeral_Bit0 [simp]:
@@ -2131,7 +2091,7 @@
lemma neg_imp_zdiv_nonneg_iff:
"b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))"
-apply (subst zdiv_zminus_zminus [symmetric])
+apply (subst div_minus_minus [symmetric])
apply (subst pos_imp_zdiv_nonneg_iff, auto)
done
@@ -2172,12 +2132,6 @@
dvd_eq_mod_eq_0 [of "neg_numeral x::int" "numeral y::int"]
dvd_eq_mod_eq_0 [of "neg_numeral x::int" "neg_numeral y::int"] for x y
-lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
- by (rule dvd_mod) (* TODO: remove *)
-
-lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
- by (rule dvd_mod_imp_dvd) (* TODO: remove *)
-
lemmas dvd_eq_mod_eq_0_numeral [simp] =
dvd_eq_mod_eq_0 [of "numeral x" "numeral y"] for x y
@@ -2188,13 +2142,6 @@
using zmod_zdiv_equality[where a="m" and b="n"]
by (simp add: algebra_simps) (* FIXME: generalize *)
-lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
-apply (induct "y", auto)
-apply (rule mod_mult_right_eq [THEN trans])
-apply (simp (no_asm_simp))
-apply (rule mod_mult_eq [symmetric])
-done (* FIXME: generalize *)
-
lemma zdiv_int: "int (a div b) = (int a) div (int b)"
apply (subst split_div, auto)
apply (subst split_zdiv, auto)
@@ -2213,12 +2160,6 @@
lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y"
by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
-lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m"
-apply (subgoal_tac "m mod n = 0")
- apply (simp add: zmult_div_cancel)
-apply (simp only: dvd_eq_mod_eq_0)
-done
-
text{*Suggested by Matthias Daum*}
lemma int_power_div_base:
"\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
@@ -2243,7 +2184,7 @@
mod_add_right_eq [symmetric]
mod_mult_right_eq[symmetric]
mod_mult_left_eq [symmetric]
- zpower_zmod
+ power_mod
zminus_zmod zdiff_zmod_left zdiff_zmod_right
text {* Distributive laws for function @{text nat}. *}
--- a/src/HOL/Groebner_Basis.thy Wed Mar 28 00:18:11 2012 +0200
+++ b/src/HOL/Groebner_Basis.thy Wed Mar 28 08:25:51 2012 +0200
@@ -53,19 +53,17 @@
declare div_by_0[algebra]
declare mod_by_0[algebra]
declare zmod_zdiv_equality[symmetric,algebra]
-declare zdiv_zmod_equality[symmetric, algebra]
-declare zdiv_zminus_zminus[algebra]
-declare zmod_zminus_zminus[algebra]
-declare zdiv_zminus2[algebra]
-declare zmod_zminus2[algebra]
+declare div_mod_equality2[symmetric, algebra]
+declare div_minus_minus[algebra]
+declare mod_minus_minus[algebra]
+declare div_minus_right[algebra]
+declare mod_minus_right[algebra]
declare div_0[algebra]
declare mod_0[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]
-declare mod_mod_trivial[algebra]
+declare mod_minus1_right[algebra]
+declare div_minus1_right[algebra]
declare mod_mult_self2_is_0[algebra]
declare mod_mult_self1_is_0[algebra]
declare zmod_eq_0_iff[algebra]
--- a/src/HOL/Import/HOL_Light/HOLLightInt.thy Wed Mar 28 00:18:11 2012 +0200
+++ b/src/HOL/Import/HOL_Light/HOLLightInt.thy Wed Mar 28 08:25:51 2012 +0200
@@ -162,7 +162,7 @@
apply (simp add: hl_mod_def hl_div_def)
apply (metis comm_semiring_1_class.normalizing_semiring_rules(24) div_mult_self2 not_less_iff_gr_or_eq order_less_le add_0 zdiv_eq_0_iff mult_commute)
apply (simp add: hl_mod_def hl_div_def)
- by (metis add.comm_neutral add_pos_nonneg div_mult_self1 less_minus_iff minus_add minus_add_cancel minus_minus mult_zero_right not_square_less_zero zdiv_eq_0_iff zdiv_zminus2)
+ by (metis add.comm_neutral add_pos_nonneg div_mult_self1 less_minus_iff minus_add minus_add_cancel minus_minus mult_zero_right not_square_less_zero zdiv_eq_0_iff div_minus_right)
lemma DEF_rem:
"hl_mod = (SOME r. \<forall>m n. if n = int 0 then
@@ -182,7 +182,7 @@
apply (simp add: hl_mod_def hl_div_def)
apply (metis add_left_cancel mod_div_equality)
apply (simp add: hl_mod_def hl_div_def)
- by (metis minus_mult_right mod_mult_self2 mod_pos_pos_trivial add_commute zminus_zmod zmod_zminus2 mult_commute)
+ by (metis minus_mult_right mod_mult_self2 mod_pos_pos_trivial add_commute zminus_zmod mod_minus_right mult_commute)
lemma DEF_int_gcd:
"int_gcd = (SOME d. \<forall>a b. (int 0) \<le> (d (a, b)) \<and> (d (a, b)) dvd a \<and>
--- a/src/HOL/Library/Abstract_Rat.thy Wed Mar 28 00:18:11 2012 +0200
+++ b/src/HOL/Library/Abstract_Rat.thy Wed Mar 28 08:25:51 2012 +0200
@@ -40,7 +40,7 @@
from anz bnz have "?g \<noteq> 0" by simp with gcd_ge_0_int[of a b]
have gpos: "?g > 0" by arith
have gdvd: "?g dvd a" "?g dvd b" by arith+
- from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)] anz bnz
+ from dvd_mult_div_cancel[OF gdvd(1)] dvd_mult_div_cancel[OF gdvd(2)] anz bnz
have nz': "?a' \<noteq> 0" "?b' \<noteq> 0" by - (rule notI, simp)+
from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith
from div_gcd_coprime_int[OF stupid] have gp1: "?g' = 1" .
@@ -56,7 +56,7 @@
assume b: "b < 0"
{ assume b': "?b' \<ge> 0"
from gpos have th: "?g \<ge> 0" by arith
- from mult_nonneg_nonneg[OF th b'] zdvd_mult_div_cancel[OF gdvd(2)]
+ from mult_nonneg_nonneg[OF th b'] dvd_mult_div_cancel[OF gdvd(2)]
have False using b by arith }
hence b': "?b' < 0" by (presburger add: linorder_not_le[symmetric])
from anz bnz nz' b b' gp1 have ?thesis
--- a/src/HOL/Library/Char_nat.thy Wed Mar 28 00:18:11 2012 +0200
+++ b/src/HOL/Library/Char_nat.thy Wed Mar 28 08:25:51 2012 +0200
@@ -158,7 +158,7 @@
unfolding 256 mult_assoc [symmetric] mod_mult_self3 ..
show ?thesis
by (simp add: nat_of_char.simps char_of_nat_def nibble_of_pair
- nat_of_nibble_of_nat mod_mult_distrib
+ nat_of_nibble_of_nat mult_mod_left
n aux3 l_256 aux4 mod_add_eq [of "256 * k"] l_div_256)
qed
--- a/src/HOL/Library/Float.thy Wed Mar 28 00:18:11 2012 +0200
+++ b/src/HOL/Library/Float.thy Wed Mar 28 08:25:51 2012 +0200
@@ -488,7 +488,7 @@
hence "x < x - x mod 2 + 2" unfolding algebra_simps by auto
thus ?thesis by auto
qed
- also have "x - x mod 2 + 2 = (x div 2 + 1) * 2" unfolding algebra_simps using `0 < x` zdiv_zmod_equality2[of x 2 0] by auto
+ also have "x - x mod 2 + 2 = (x div 2 + 1) * 2" unfolding algebra_simps using `0 < x` div_mod_equality[of x 2 0] by auto
also have "\<dots> \<le> 2^nat (bitlen (x div 2)) * 2" using hyp[OF `0 < x div 2`, THEN conjunct2] by (rule mult_right_mono, auto)
also have "\<dots> = 2^(1 + nat (bitlen (x div 2)))" unfolding power_Suc2[symmetric] by auto
finally have "x + 1 \<le> 2^(1 + nat (bitlen (x div 2)))" .
@@ -1122,7 +1122,7 @@
show ?thesis
proof (cases "m mod ?p = 0")
case True
- have m: "m = m div ?p * ?p + 0" unfolding True[symmetric] using zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right, symmetric] .
+ have m: "m = m div ?p * ?p + 0" unfolding True[symmetric] using mod_div_equality [symmetric] .
have "real (Float m e) = real (Float (m div ?p) (e + ?d))" unfolding real_of_float_simp arg_cong[OF m, of real]
by (auto simp add: pow2_add `0 < ?d` pow_d)
thus ?thesis
@@ -1130,7 +1130,7 @@
by auto
next
case False
- have "m = m div ?p * ?p + m mod ?p" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] ..
+ have "m = m div ?p * ?p + m mod ?p" unfolding mod_div_equality ..
also have "\<dots> \<le> (m div ?p + 1) * ?p" unfolding left_distrib mult_1 by (rule add_left_mono, rule pos_mod_bound[OF `0 < ?p`, THEN less_imp_le])
finally have "real (Float m e) \<le> real (Float (m div ?p + 1) (e + ?d))" unfolding real_of_float_simp add_commute[of e]
unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of m, symmetric]
@@ -1156,7 +1156,7 @@
case True
hence pow_d: "pow2 ?d = real ?p" using pow2_int[symmetric] by simp
have "m div ?p * ?p \<le> m div ?p * ?p + m mod ?p" by (auto simp add: pos_mod_bound[OF `0 < ?p`, THEN less_imp_le])
- also have "\<dots> \<le> m" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] ..
+ also have "\<dots> \<le> m" unfolding mod_div_equality ..
finally have "real (Float (m div ?p) (e + ?d)) \<le> real (Float m e)" unfolding real_of_float_simp add_commute[of e]
unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of _ m, symmetric]
by (auto intro!: mult_mono simp add: pow2_add `0 < ?d` pow_d)
--- a/src/HOL/Library/Target_Numeral.thy Wed Mar 28 00:18:11 2012 +0200
+++ b/src/HOL/Library/Target_Numeral.thy Wed Mar 28 08:25:51 2012 +0200
@@ -296,7 +296,7 @@
have aux2: "\<And>q::int. - int_of k = int_of l * q \<longleftrightarrow> int_of k = int_of l * - q" by auto
show ?thesis
by (simp add: prod_eq_iff Target_Numeral.int_eq_iff prod_case_beta aux1)
- (auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if zdiv_zminus2 zmod_zminus2 aux2)
+ (auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right aux2)
qed
lemma div_int_code [code]:
--- a/src/HOL/Number_Theory/Cong.thy Wed Mar 28 00:18:11 2012 +0200
+++ b/src/HOL/Number_Theory/Cong.thy Wed Mar 28 08:25:51 2012 +0200
@@ -214,9 +214,9 @@
lemma cong_mult_int:
"[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
apply (unfold cong_int_def)
- apply (subst (1 2) zmod_zmult1_eq)
+ apply (subst (1 2) mod_mult_right_eq)
apply (subst (1 2) mult_commute)
- apply (subst (1 2) zmod_zmult1_eq)
+ apply (subst (1 2) mod_mult_right_eq)
apply simp
done
--- a/src/HOL/Number_Theory/Residues.thy Wed Mar 28 00:18:11 2012 +0200
+++ b/src/HOL/Number_Theory/Residues.thy Wed Mar 28 08:25:51 2012 +0200
@@ -56,7 +56,7 @@
apply auto
apply (subgoal_tac "x * y mod m * z mod m = z * (x * y mod m) mod m")
apply (erule ssubst)
- apply (subst zmod_zmult1_eq [symmetric])+
+ apply (subst mod_mult_right_eq [symmetric])+
apply (simp_all only: mult_ac)
done
@@ -67,7 +67,7 @@
apply (unfold R_def residue_ring_def, auto)
apply (subst mod_add_eq [symmetric])
apply (subst mult_commute)
- apply (subst zmod_zmult1_eq [symmetric])
+ apply (subst mod_mult_right_eq [symmetric])
apply (simp add: field_simps)
done
@@ -151,9 +151,9 @@
lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m"
apply (unfold R_def residue_ring_def, auto)
- apply (subst zmod_zmult1_eq [symmetric])
+ apply (subst mod_mult_right_eq [symmetric])
apply (subst mult_commute)
- apply (subst zmod_zmult1_eq [symmetric])
+ apply (subst mod_mult_right_eq [symmetric])
apply (subst mult_commute)
apply auto
done
--- a/src/HOL/Numeral_Simprocs.thy Wed Mar 28 00:18:11 2012 +0200
+++ b/src/HOL/Numeral_Simprocs.thy Wed Mar 28 08:25:51 2012 +0200
@@ -72,7 +72,7 @@
lemma nat_mult_dvd_cancel_disj[simp]:
"(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))"
-by(auto simp: dvd_eq_mod_eq_0 mod_mult_distrib2[symmetric])
+by (auto simp: dvd_eq_mod_eq_0 mod_mult_mult1)
lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"
by(auto)
--- a/src/HOL/Old_Number_Theory/IntPrimes.thy Wed Mar 28 00:18:11 2012 +0200
+++ b/src/HOL/Old_Number_Theory/IntPrimes.thy Wed Mar 28 08:25:51 2012 +0200
@@ -105,7 +105,7 @@
by (simp add: zgcd_zmult_cancel)
lemma zdvd_iff_zgcd: "0 < m ==> m dvd n \<longleftrightarrow> zgcd n m = m"
- by (metis abs_of_pos zdvd_mult_div_cancel zgcd_0 zgcd_commute zgcd_geq_zero zgcd_zdvd2 zgcd_zmult_eq_self)
+ by (metis abs_of_pos dvd_mult_div_cancel zgcd_0 zgcd_commute zgcd_geq_zero zgcd_zdvd2 zgcd_zmult_eq_self)
@@ -197,7 +197,7 @@
apply (subgoal_tac "m dvd n * ka")
apply (subgoal_tac "m dvd ka")
apply (case_tac [2] "0 \<le> ka")
- apply (metis zdvd_mult_div_cancel dvd_refl dvd_mult_left mult_commute zrelprime_zdvd_zmult)
+ apply (metis dvd_mult_div_cancel dvd_refl dvd_mult_left mult_commute zrelprime_zdvd_zmult)
apply (metis abs_dvd_iff abs_of_nonneg add_0 zgcd_0_left zgcd_commute zgcd_zadd_zmult zgcd_zdvd_zgcd_zmult zgcd_zmult_distrib2_abs mult_1_right mult_commute)
apply (metis mult_le_0_iff zdvd_mono zdvd_mult_cancel dvd_triv_left zero_le_mult_iff order_antisym linorder_linear order_refl mult_commute zrelprime_zdvd_zmult)
apply (metis dvd_triv_left)
@@ -407,7 +407,7 @@
apply (cut_tac a = a and n = n in zcong_lineq_ex, auto)
apply (rule_tac x = "x * b mod n" in exI, safe)
apply (simp_all (no_asm_simp))
- apply (metis zcong_scalar zcong_zmod zmod_zmult1_eq mult_1 mult_assoc)
+ apply (metis zcong_scalar zcong_zmod mod_mult_right_eq mult_1 mult_assoc)
done
end
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy Wed Mar 28 00:18:11 2012 +0200
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy Wed Mar 28 08:25:51 2012 +0200
@@ -643,8 +643,8 @@
unfolding dvd_def by blast
then have "?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'" by simp_all
then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
- by (auto simp add: zdvd_mult_div_cancel [OF dvdg(1)]
- zdvd_mult_div_cancel [OF dvdg(2)] dvd_def)
+ by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
+ dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
have "?g \<noteq> 0" using nz by simp
then have gp: "?g \<noteq> 0" using zgcd_pos[where i="a" and j="b"] by arith
from zgcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
--- a/src/HOL/Old_Number_Theory/WilsonRuss.thy Wed Mar 28 00:18:11 2012 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy Wed Mar 28 08:25:51 2012 +0200
@@ -35,7 +35,7 @@
"zprime p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> [a * inv p a = 1] (mod p)"
apply (unfold inv_def)
apply (subst zcong_zmod)
- apply (subst zmod_zmult1_eq [symmetric])
+ apply (subst mod_mult_right_eq [symmetric])
apply (subst zcong_zmod [symmetric])
apply (subst power_Suc [symmetric])
apply (subst inv_is_inv_aux)
@@ -137,7 +137,7 @@
lemma inv_inv: "zprime p \<Longrightarrow>
5 \<le> p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> inv p (inv p a) = a"
apply (unfold inv_def)
- apply (subst zpower_zmod)
+ apply (subst power_mod)
apply (subst zpower_zpower)
apply (rule zcong_zless_imp_eq)
prefer 5
--- a/src/HOL/Parity.thy Wed Mar 28 00:18:11 2012 +0200
+++ b/src/HOL/Parity.thy Wed Mar 28 08:25:51 2012 +0200
@@ -74,7 +74,7 @@
lemma anything_times_even: "even (y::int) ==> even (x * y)" by algebra
lemma odd_times_odd: "odd (x::int) ==> odd y ==> odd (x * y)"
- by (simp add: even_def zmod_zmult1_eq)
+ by (simp add: even_def mod_mult_right_eq)
lemma even_product[simp,presburger]: "even((x::int) * y) = (even x | even y)"
apply (auto simp add: even_times_anything anything_times_even)
--- a/src/HOL/Presburger.thy Wed Mar 28 00:18:11 2012 +0200
+++ b/src/HOL/Presburger.thy Wed Mar 28 08:25:51 2012 +0200
@@ -405,8 +405,8 @@
declare mod_div_equality[presburger]
declare mod_mult_self1[presburger]
declare mod_mult_self2[presburger]
-declare zdiv_zmod_equality2[presburger]
-declare zdiv_zmod_equality[presburger]
+declare div_mod_equality[presburger]
+declare div_mod_equality2[presburger]
declare mod2_Suc_Suc[presburger]
lemma [presburger]: "(a::int) div 0 = 0" and [presburger]: "a mod 0 = a"
by simp_all
--- a/src/HOL/Word/Bit_Representation.thy Wed Mar 28 00:18:11 2012 +0200
+++ b/src/HOL/Word/Bit_Representation.thy Wed Mar 28 08:25:51 2012 +0200
@@ -613,8 +613,7 @@
lemma sb_dec_lem:
"(0::int) <= - (2^k) + a ==> (a + 2^k) mod (2 * 2 ^ k) <= - (2 ^ k) + a"
- by (rule int_mod_le' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k",
- simplified zless2p, OF _ TrueI, simplified])
+ by (rule int_mod_le' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k", simplified])
lemma sb_dec_lem':
"(2::int) ^ k <= a ==> (a + 2 ^ k) mod (2 * 2 ^ k) <= - (2 ^ k) + a"
@@ -624,22 +623,22 @@
"x >= (2 ^ n) ==> x - 2 ^ (Suc n) >= sbintrunc n x"
unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp
-lemmas zmod_uminus' = zmod_uminus [where b=c] for c
-lemmas zpower_zmod' = zpower_zmod [where m=c and y=k] for c k
+lemmas zmod_uminus' = zminus_zmod [where m=c] for c
+lemmas zpower_zmod' = power_mod [where b=c and n=k] for c k
-lemmas brdmod1s' [symmetric] =
- mod_add_left_eq mod_add_right_eq
- zmod_zsub_left_eq zmod_zsub_right_eq
- zmod_zmult1_eq zmod_zmult1_eq_rev
+lemmas brdmod1s' [symmetric] =
+ mod_add_left_eq mod_add_right_eq
+ mod_diff_left_eq mod_diff_right_eq
+ mod_mult_left_eq mod_mult_right_eq
lemmas brdmods' [symmetric] =
zpower_zmod' [symmetric]
trans [OF mod_add_left_eq mod_add_right_eq]
- trans [OF zmod_zsub_left_eq zmod_zsub_right_eq]
- trans [OF zmod_zmult1_eq zmod_zmult1_eq_rev]
+ trans [OF mod_diff_left_eq mod_diff_right_eq]
+ trans [OF mod_mult_right_eq mod_mult_left_eq]
zmod_uminus' [symmetric]
mod_add_left_eq [where b = "1::int"]
- zmod_zsub_left_eq [where b = "1"]
+ mod_diff_left_eq [where b = "1::int"]
lemmas bintr_arith1s =
brdmod1s' [where c="2^n::int", folded bintrunc_mod2p] for n
--- a/src/HOL/Word/Misc_Numeric.thy Wed Mar 28 00:18:11 2012 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy Wed Mar 28 08:25:51 2012 +0200
@@ -33,8 +33,8 @@
lemma zless2: "0 < (2 :: int)" by arith
-lemmas zless2p [simp] = zless2 [THEN zero_less_power]
-lemmas zle2p [simp] = zless2p [THEN order_less_imp_le]
+lemmas zless2p = zless2 [THEN zero_less_power]
+lemmas zle2p = zless2p [THEN order_less_imp_le]
lemmas pos_mod_sign2 = zless2 [THEN pos_mod_sign [where b = "2::int"]]
lemmas pos_mod_bound2 = zless2 [THEN pos_mod_bound [where b = "2::int"]]
@@ -96,38 +96,13 @@
lemmas add_diff_cancel2 = add_commute [THEN diff_eq_eq [THEN iffD2]]
-lemma zmod_uminus: "- ((a :: int) mod b) mod b = -a mod b"
- by (simp add : zmod_zminus1_eq_if)
-
-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 _ 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"
- apply (unfold diff_int_def)
- apply (rule trans [OF _ mod_add_right_eq [symmetric]])
- apply (simp add : zmod_uminus mod_add_right_eq [symmetric])
- done
-
-lemma zmod_zsub_left_eq: "((a::int) - b) mod c = (a mod c - b) mod c"
- by (rule mod_add_left_eq [where b = "- b", simplified diff_int_def [symmetric]])
-
lemma zmod_zsub_self [simp]:
"((b :: int) - a) mod a = b mod a"
- by (simp add: zmod_zsub_right_eq)
+ by (simp add: mod_diff_right_eq)
-lemma zmod_zmult1_eq_rev:
- "b * a mod c = b mod c * a mod (c::int)"
- apply (simp add: mult_commute)
- apply (subst zmod_zmult1_eq)
- apply simp
- done
-
-lemmas rdmods [symmetric] = zmod_uminus [symmetric]
- zmod_zsub_left_eq zmod_zsub_right_eq mod_add_left_eq
- mod_add_right_eq zmod_zmult1_eq zmod_zmult1_eq_rev
+lemmas rdmods [symmetric] = mod_minus_eq
+ mod_diff_left_eq mod_diff_right_eq mod_add_left_eq
+ mod_add_right_eq mod_mult_right_eq mod_mult_left_eq
lemma mod_plus_right:
"((a + x) mod m = (b + x) mod m) = (a mod m = b mod (m :: nat))"
@@ -143,8 +118,8 @@
THEN mod_plus_right [THEN iffD2], simplified]
lemmas push_mods' = mod_add_eq
- mod_mult_eq zmod_zsub_distrib
- zmod_uminus [symmetric]
+ mod_mult_eq mod_diff_eq
+ mod_minus_eq
lemmas push_mods = push_mods' [THEN eq_reflection]
lemmas pull_mods = push_mods [symmetric] rdmods [THEN eq_reflection]
@@ -197,13 +172,11 @@
lemmas int_mod_eq' = refl [THEN [3] int_mod_eq]
-lemma int_mod_le: "0 <= a ==> 0 < (n :: int) ==> a mod n <= a"
- apply (cases "a < n")
- apply (auto dest: mod_pos_pos_trivial pos_mod_bound [where a=a])
- done
+lemma int_mod_le: "(0::int) <= a ==> a mod n <= a"
+ by (fact zmod_le_nonneg_dividend) (* FIXME: delete *)
-lemma int_mod_le': "0 <= b - n ==> 0 < (n :: int) ==> b mod n <= b - n"
- by (rule int_mod_le [where a = "b - n" and n = n, simplified])
+lemma int_mod_le': "(0::int) <= b - n ==> b mod n <= b - n"
+ using zmod_le_nonneg_dividend [of "b - n" "n"] by simp
lemma int_mod_ge: "a < n ==> 0 < (n :: int) ==> a <= a mod n"
apply (cases "0 <= a")
@@ -289,11 +262,7 @@
lemmas td_gal_lt = td_gal [simplified not_less [symmetric], simplified]
lemma div_mult_le: "(a :: nat) div b * b <= a"
- apply (cases b)
- prefer 2
- apply (rule order_refl [THEN th2])
- apply auto
- done
+ by (fact dtle)
lemmas sdl = split_div_lemma [THEN iffD1, symmetric]
--- a/src/HOL/Word/Word.thy Wed Mar 28 00:18:11 2012 +0200
+++ b/src/HOL/Word/Word.thy Wed Mar 28 08:25:51 2012 +0200
@@ -4465,9 +4465,9 @@
and 4: "x' - y' = z'"
shows "(x - y) mod b = z' mod b'"
using assms
- apply (subst zmod_zsub_left_eq)
- apply (subst zmod_zsub_right_eq)
- apply (simp add: zmod_zsub_left_eq [symmetric] zmod_zsub_right_eq [symmetric])
+ apply (subst mod_diff_left_eq)
+ apply (subst mod_diff_right_eq)
+ apply (simp add: mod_diff_left_eq [symmetric] mod_diff_right_eq [symmetric])
done
lemma word_induct_less: