src/HOL/Divides.thy
 changeset 47159 978c00c20a59 parent 47142 d64fa2ca54b8 child 47160 8ada79014cb2
```     1.1 --- a/src/HOL/Divides.thy	Tue Mar 27 14:49:56 2012 +0200
1.2 +++ b/src/HOL/Divides.thy	Tue Mar 27 15:27:49 2012 +0200
1.3 @@ -343,6 +343,12 @@
1.4    "(a * c) mod (b * c) = (a mod b) * c"
1.5    using mod_mult_mult1 [of c a b] by (simp add: mult_commute)
1.6
1.7 +lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)"
1.8 +  by (fact mod_mult_mult2 [symmetric])
1.9 +
1.10 +lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
1.11 +  by (fact mod_mult_mult1 [symmetric])
1.12 +
1.13  lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
1.14    unfolding dvd_def by (auto simp add: mod_mult_mult1)
1.15
1.16 @@ -444,6 +450,19 @@
1.17  apply simp
1.18  done
1.19
1.20 +lemma div_minus_minus [simp]: "(-a) div (-b) = a div b"
1.21 +  using div_mult_mult1 [of "- 1" a b]
1.22 +  unfolding neg_equal_0_iff_equal by simp
1.23 +
1.24 +lemma mod_minus_minus [simp]: "(-a) mod (-b) = - (a mod b)"
1.25 +  using mod_mult_mult1 [of "- 1" a b] by simp
1.26 +
1.27 +lemma div_minus_right: "a div (-b) = (-a) div b"
1.28 +  using div_minus_minus [of "-a" b] by simp
1.29 +
1.30 +lemma mod_minus_right: "a mod (-b) = - ((-a) mod b)"
1.31 +  using mod_minus_minus [of "-a" b] by simp
1.32 +
1.33  end
1.34
1.35
1.36 @@ -712,12 +731,6 @@
1.37  lemma mod_1 [simp]: "m mod Suc 0 = 0"
1.38  by (induct m) (simp_all add: mod_geq)
1.39
1.40 -lemma mod_mult_distrib: "(m mod n) * (k\<Colon>nat) = (m * k) mod (n * k)"
1.41 -  by (fact mod_mult_mult2 [symmetric]) (* FIXME: generalize *)
1.42 -
1.43 -lemma mod_mult_distrib2: "(k::nat) * (m mod n) = (k*m) mod (k*n)"
1.44 -  by (fact mod_mult_mult1 [symmetric]) (* FIXME: generalize *)
1.45 -
1.46  (* a simple rearrangement of mod_div_equality: *)
1.47  lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
1.48    using mod_div_equality2 [of n m] by arith
1.49 @@ -1489,15 +1502,6 @@
1.50  text{*There is no @{text mod_neg_pos_trivial}.*}
1.51
1.52
1.53 -(*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*)
1.54 -lemma zdiv_zminus_zminus [simp]: "(-a) div (-b) = a div (b::int)"
1.55 -  using div_mult_mult1 [of "-1" a b] by simp (* FIXME: generalize *)
1.56 -
1.57 -(*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*)
1.58 -lemma zmod_zminus_zminus [simp]: "(-a) mod (-b) = - (a mod (b::int))"
1.59 -  using mod_mult_mult1 [of "-1" a b] by simp (* FIXME: generalize *)
1.60 -
1.61 -
1.62  subsubsection {* Laws for div and mod with Unary Minus *}
1.63
1.64  lemma zminus1_lemma:
1.65 @@ -1524,21 +1528,15 @@
1.66    shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
1.67    unfolding zmod_zminus1_eq_if by auto
1.68
1.69 -lemma zdiv_zminus2: "a div (-b) = (-a::int) div b"
1.70 -  using zdiv_zminus_zminus [of "-a" b] by simp (* FIXME: generalize *)
1.71 -
1.72 -lemma zmod_zminus2: "a mod (-b) = - ((-a::int) mod b)"
1.73 -  using zmod_zminus_zminus [of "-a" b] by simp (* FIXME: generalize*)
1.74 -
1.75  lemma zdiv_zminus2_eq_if:
1.76       "b \<noteq> (0::int)
1.77        ==> a div (-b) =
1.78            (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
1.79 -by (simp add: zdiv_zminus1_eq_if zdiv_zminus2)
1.80 +by (simp add: zdiv_zminus1_eq_if div_minus_right)
1.81
1.82  lemma zmod_zminus2_eq_if:
1.83       "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"
1.84 -by (simp add: zmod_zminus1_eq_if zmod_zminus2)
1.85 +by (simp add: zmod_zminus1_eq_if mod_minus_right)
1.86
1.87  lemma zmod_zminus2_not_zero:
1.88    fixes k l :: int
1.89 @@ -2024,7 +2022,7 @@
1.90    have "(1 + 2 * (-b - 1)) div (2 * (-a)) = (-b - 1) div (-a)"
1.91      by (rule pos_zdiv_mult_2, simp add: A)
1.92    thus ?thesis
1.93 -    by (simp only: R zdiv_zminus_zminus diff_minus
1.94 +    by (simp only: R div_minus_minus diff_minus
1.96  qed
1.97
1.98 @@ -2072,7 +2070,7 @@
1.99    from assms have "0 \<le> - a" by auto
1.100    then have "(1 + 2 * (- b - 1)) mod (2 * (- a)) = 1 + 2 * ((- b - 1) mod (- a))"
1.101      by (rule pos_zmod_mult_2)
1.102 -  then show ?thesis by (simp add: zmod_zminus2 algebra_simps)
1.103 +  then show ?thesis by (simp add: mod_minus_right algebra_simps)