1.1 --- a/NEWS	Tue Mar 27 14:49:56 2012 +0200
     1.2 +++ b/NEWS	Tue Mar 27 15:27:49 2012 +0200
     1.3 @@ -145,6 +145,12 @@
     1.4    zdiv_zero ~> div_0
     1.5    zmod_zero ~> mod_0
     1.6    zmod_zdiv_trivial ~> mod_div_trivial
     1.7 +  zdiv_zminus_zminus ~> div_minus_minus
     1.8 +  zmod_zminus_zminus ~> mod_minus_minus
     1.9 +  zdiv_zminus2 ~> div_minus_right
    1.10 +  zmod_zminus2 ~> mod_minus_right
    1.11 +  mod_mult_distrib ~> mult_mod_left
    1.12 +  mod_mult_distrib2 ~> mult_mod_right
    1.13  
    1.14  * More default pred/set conversions on a couple of relation operations
    1.15  and predicates.  Consolidation of some relation theorems:

     2.1 --- a/src/HOL/Divides.thy	Tue Mar 27 14:49:56 2012 +0200
     2.2 +++ b/src/HOL/Divides.thy	Tue Mar 27 15:27:49 2012 +0200
     2.3 @@ -343,6 +343,12 @@
     2.4    "(a * c) mod (b * c) = (a mod b) * c"
     2.5    using mod_mult_mult1 [of c a b] by (simp add: mult_commute)
     2.6  
     2.7 +lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)"
     2.8 +  by (fact mod_mult_mult2 [symmetric])
     2.9 +
    2.10 +lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
    2.11 +  by (fact mod_mult_mult1 [symmetric])
    2.12 +
    2.13  lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
    2.14    unfolding dvd_def by (auto simp add: mod_mult_mult1)
    2.15  
    2.16 @@ -444,6 +450,19 @@
    2.17  apply simp
    2.18  done
    2.19  
    2.20 +lemma div_minus_minus [simp]: "(-a) div (-b) = a div b"
    2.21 +  using div_mult_mult1 [of "- 1" a b]
    2.22 +  unfolding neg_equal_0_iff_equal by simp
    2.23 +
    2.24 +lemma mod_minus_minus [simp]: "(-a) mod (-b) = - (a mod b)"
    2.25 +  using mod_mult_mult1 [of "- 1" a b] by simp
    2.26 +
    2.27 +lemma div_minus_right: "a div (-b) = (-a) div b"
    2.28 +  using div_minus_minus [of "-a" b] by simp
    2.29 +
    2.30 +lemma mod_minus_right: "a mod (-b) = - ((-a) mod b)"
    2.31 +  using mod_minus_minus [of "-a" b] by simp
    2.32 +
    2.33  end
    2.34  
    2.35  
    2.36 @@ -712,12 +731,6 @@
    2.37  lemma mod_1 [simp]: "m mod Suc 0 = 0"
    2.38  by (induct m) (simp_all add: mod_geq)
    2.39  
    2.40 -lemma mod_mult_distrib: "(m mod n) * (k\<Colon>nat) = (m * k) mod (n * k)"
    2.41 -  by (fact mod_mult_mult2 [symmetric]) (* FIXME: generalize *)
    2.42 -
    2.43 -lemma mod_mult_distrib2: "(k::nat) * (m mod n) = (k*m) mod (k*n)"
    2.44 -  by (fact mod_mult_mult1 [symmetric]) (* FIXME: generalize *)
    2.45 -
    2.46  (* a simple rearrangement of mod_div_equality: *)
    2.47  lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
    2.48    using mod_div_equality2 [of n m] by arith
    2.49 @@ -1489,15 +1502,6 @@
    2.50  text{*There is no @{text mod_neg_pos_trivial}.*}
    2.51  
    2.52  
    2.53 -(*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*)
    2.54 -lemma zdiv_zminus_zminus [simp]: "(-a) div (-b) = a div (b::int)"
    2.55 -  using div_mult_mult1 [of "-1" a b] by simp (* FIXME: generalize *)
    2.56 -
    2.57 -(*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*)
    2.58 -lemma zmod_zminus_zminus [simp]: "(-a) mod (-b) = - (a mod (b::int))"
    2.59 -  using mod_mult_mult1 [of "-1" a b] by simp (* FIXME: generalize *)
    2.60 -
    2.61 -
    2.62  subsubsection {* Laws for div and mod with Unary Minus *}
    2.63  
    2.64  lemma zminus1_lemma:
    2.65 @@ -1524,21 +1528,15 @@
    2.66    shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
    2.67    unfolding zmod_zminus1_eq_if by auto
    2.68  
    2.69 -lemma zdiv_zminus2: "a div (-b) = (-a::int) div b"
    2.70 -  using zdiv_zminus_zminus [of "-a" b] by simp (* FIXME: generalize *)
    2.71 -
    2.72 -lemma zmod_zminus2: "a mod (-b) = - ((-a::int) mod b)"
    2.73 -  using zmod_zminus_zminus [of "-a" b] by simp (* FIXME: generalize*)
    2.74 -
    2.75  lemma zdiv_zminus2_eq_if:
    2.76       "b \<noteq> (0::int)  
    2.77        ==> a div (-b) =  
    2.78            (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
    2.79 -by (simp add: zdiv_zminus1_eq_if zdiv_zminus2)
    2.80 +by (simp add: zdiv_zminus1_eq_if div_minus_right)
    2.81  
    2.82  lemma zmod_zminus2_eq_if:
    2.83       "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"
    2.84 -by (simp add: zmod_zminus1_eq_if zmod_zminus2)
    2.85 +by (simp add: zmod_zminus1_eq_if mod_minus_right)
    2.86  
    2.87  lemma zmod_zminus2_not_zero:
    2.88    fixes k l :: int
    2.89 @@ -2024,7 +2022,7 @@
    2.90    have "(1 + 2 * (-b - 1)) div (2 * (-a)) = (-b - 1) div (-a)"
    2.91      by (rule pos_zdiv_mult_2, simp add: A)
    2.92    thus ?thesis
    2.93 -    by (simp only: R zdiv_zminus_zminus diff_minus
    2.94 +    by (simp only: R div_minus_minus diff_minus
    2.95        minus_add_distrib [symmetric] mult_minus_right)
    2.96  qed
    2.97  
    2.98 @@ -2072,7 +2070,7 @@
    2.99    from assms have "0 \<le> - a" by auto
   2.100    then have "(1 + 2 * (- b - 1)) mod (2 * (- a)) = 1 + 2 * ((- b - 1) mod (- a))"
   2.101      by (rule pos_zmod_mult_2)
   2.102 -  then show ?thesis by (simp add: zmod_zminus2 algebra_simps)
   2.103 +  then show ?thesis by (simp add: mod_minus_right algebra_simps)
   2.104       (simp add: diff_minus add_ac)
   2.105  qed
   2.106  
   2.107 @@ -2131,7 +2129,7 @@
   2.108  
   2.109  lemma neg_imp_zdiv_nonneg_iff:
   2.110    "b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))"
   2.111 -apply (subst zdiv_zminus_zminus [symmetric])
   2.112 +apply (subst div_minus_minus [symmetric])
   2.113  apply (subst pos_imp_zdiv_nonneg_iff, auto)
   2.114  done
   2.115  

     3.1 --- a/src/HOL/Groebner_Basis.thy	Tue Mar 27 14:49:56 2012 +0200
     3.2 +++ b/src/HOL/Groebner_Basis.thy	Tue Mar 27 15:27:49 2012 +0200
     3.3 @@ -54,10 +54,10 @@
     3.4  declare mod_by_0[algebra]
     3.5  declare zmod_zdiv_equality[symmetric,algebra]
     3.6  declare zdiv_zmod_equality[symmetric, algebra]
     3.7 -declare zdiv_zminus_zminus[algebra]
     3.8 -declare zmod_zminus_zminus[algebra]
     3.9 -declare zdiv_zminus2[algebra]
    3.10 -declare zmod_zminus2[algebra]
    3.11 +declare div_minus_minus[algebra]
    3.12 +declare mod_minus_minus[algebra]
    3.13 +declare div_minus_right[algebra]
    3.14 +declare mod_minus_right[algebra]
    3.15  declare div_0[algebra]
    3.16  declare mod_0[algebra]
    3.17  declare mod_by_1[algebra]

     4.1 --- a/src/HOL/Import/HOL_Light/HOLLightInt.thy	Tue Mar 27 14:49:56 2012 +0200
     4.2 +++ b/src/HOL/Import/HOL_Light/HOLLightInt.thy	Tue Mar 27 15:27:49 2012 +0200
     4.3 @@ -162,7 +162,7 @@
     4.4    apply (simp add: hl_mod_def hl_div_def)
     4.5    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)
     4.6    apply (simp add: hl_mod_def hl_div_def)
     4.7 -  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)
     4.8 +  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)
     4.9  
    4.10  lemma DEF_rem:
    4.11    "hl_mod = (SOME r. \<forall>m n. if n = int 0 then
    4.12 @@ -182,7 +182,7 @@
    4.13    apply (simp add: hl_mod_def hl_div_def)
    4.14    apply (metis add_left_cancel mod_div_equality)
    4.15    apply (simp add: hl_mod_def hl_div_def)
    4.16 -  by (metis minus_mult_right mod_mult_self2 mod_pos_pos_trivial add_commute zminus_zmod zmod_zminus2 mult_commute)
    4.17 +  by (metis minus_mult_right mod_mult_self2 mod_pos_pos_trivial add_commute zminus_zmod mod_minus_right mult_commute)
    4.18  
    4.19  lemma DEF_int_gcd:
    4.20    "int_gcd = (SOME d. \<forall>a b. (int 0) \<le> (d (a, b)) \<and> (d (a, b)) dvd a \<and>

     5.1 --- a/src/HOL/Library/Char_nat.thy	Tue Mar 27 14:49:56 2012 +0200
     5.2 +++ b/src/HOL/Library/Char_nat.thy	Tue Mar 27 15:27:49 2012 +0200
     5.3 @@ -158,7 +158,7 @@
     5.4      unfolding 256 mult_assoc [symmetric] mod_mult_self3 ..
     5.5    show ?thesis
     5.6      by (simp add: nat_of_char.simps char_of_nat_def nibble_of_pair
     5.7 -      nat_of_nibble_of_nat mod_mult_distrib
     5.8 +      nat_of_nibble_of_nat mult_mod_left
     5.9        n aux3 l_256 aux4 mod_add_eq [of "256 * k"] l_div_256)
    5.10  qed
    5.11  

     6.1 --- a/src/HOL/Library/Target_Numeral.thy	Tue Mar 27 14:49:56 2012 +0200
     6.2 +++ b/src/HOL/Library/Target_Numeral.thy	Tue Mar 27 15:27:49 2012 +0200
     6.3 @@ -296,7 +296,7 @@
     6.4    have aux2: "\<And>q::int. - int_of k = int_of l * q \<longleftrightarrow> int_of k = int_of l * - q" by auto
     6.5    show ?thesis
     6.6      by (simp add: prod_eq_iff Target_Numeral.int_eq_iff prod_case_beta aux1)
     6.7 -      (auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if zdiv_zminus2 zmod_zminus2 aux2)
     6.8 +      (auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right aux2)
     6.9  qed
    6.10  
    6.11  lemma div_int_code [code]:

     7.1 --- a/src/HOL/Numeral_Simprocs.thy	Tue Mar 27 14:49:56 2012 +0200
     7.2 +++ b/src/HOL/Numeral_Simprocs.thy	Tue Mar 27 15:27:49 2012 +0200
     7.3 @@ -72,7 +72,7 @@
     7.4  
     7.5  lemma nat_mult_dvd_cancel_disj[simp]:
     7.6    "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))"
     7.7 -by(auto simp: dvd_eq_mod_eq_0 mod_mult_distrib2[symmetric])
     7.8 +by (auto simp: dvd_eq_mod_eq_0 mod_mult_mult1)
     7.9  
    7.10  lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"
    7.11  by(auto)