1.1 --- a/src/HOL/IntDiv.thy	Wed Jan 07 08:13:56 2009 -0800
     1.2 +++ b/src/HOL/IntDiv.thy	Thu Jan 08 08:24:08 2009 -0800
     1.3 @@ -747,12 +747,12 @@
     1.4  lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a"
     1.5  by (simp add: zdiv_zmult1_eq)
     1.6  
     1.7 -lemma mod_div_trivial [simp]: "(a mod b) div b = (0::int)"
     1.8 +lemma zmod_zdiv_trivial: "(a mod b) div b = (0::int)"
     1.9  apply (case_tac "b = 0", simp)
    1.10  apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
    1.11  done
    1.12  
    1.13 -lemma mod_mod_trivial [simp]: "(a mod b) mod b = a mod (b::int)"
    1.14 +lemma zmod_zmod_trivial: "(a mod b) mod b = a mod (b::int)"
    1.15  apply (case_tac "b = 0", simp)
    1.16  apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial)
    1.17  done
    1.18 @@ -776,63 +776,47 @@
    1.19  apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod)
    1.20  done
    1.21  
    1.22 -lemma zdiv_zadd_self1[simp]: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
    1.23 -by (simp add: zdiv_zadd1_eq)
    1.24 -
    1.25 -lemma zdiv_zadd_self2[simp]: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
    1.26 -by (simp add: zdiv_zadd1_eq)
    1.27 -
    1.28  instance int :: semiring_div
    1.29  proof
    1.30    fix a b c :: int
    1.31    assume not0: "b \<noteq> 0"
    1.32    show "(a + c * b) div b = c + a div b"
    1.33      unfolding zdiv_zadd1_eq [of a "c * b"] using not0 
    1.34 -      by (simp add: zmod_zmult1_eq)
    1.35 +      by (simp add: zmod_zmult1_eq zmod_zdiv_trivial)
    1.36  qed auto
    1.37  
    1.38 -lemma zdiv_zmult_self2 [simp]: "b \<noteq> (0::int) ==> (b*a) div b = a"
    1.39 -by (subst mult_commute, erule zdiv_zmult_self1)
    1.40 +lemma zdiv_zadd_self1: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
    1.41 +by (rule div_add_self1) (* already declared [simp] *)
    1.42 +
    1.43 +lemma zdiv_zadd_self2: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
    1.44 +by (rule div_add_self2) (* already declared [simp] *)
    1.45  
    1.46 -lemma zmod_zmult_self1 [simp]: "(a*b) mod b = (0::int)"
    1.47 -by (simp add: zmod_zmult1_eq)
    1.48 +lemma zdiv_zmult_self2: "b \<noteq> (0::int) ==> (b*a) div b = a"
    1.49 +by (rule div_mult_self1_is_id) (* already declared [simp] *)
    1.50  
    1.51 -lemma zmod_zmult_self2 [simp]: "(b*a) mod b = (0::int)"
    1.52 -by (simp add: mult_commute zmod_zmult1_eq)
    1.53 +lemma zmod_zmult_self1: "(a*b) mod b = (0::int)"
    1.54 +by (rule mod_mult_self2_is_0) (* already declared [simp] *)
    1.55 +
    1.56 +lemma zmod_zmult_self2: "(b*a) mod b = (0::int)"
    1.57 +by (rule mod_mult_self1_is_0) (* already declared [simp] *)
    1.58  
    1.59  lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
    1.60 -proof
    1.61 -  assume "m mod d = 0"
    1.62 -  with zmod_zdiv_equality[of m d] show "EX q::int. m = d*q" by auto
    1.63 -next
    1.64 -  assume "EX q::int. m = d*q"
    1.65 -  thus "m mod d = 0" by auto
    1.66 -qed
    1.67 +by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
    1.68  
    1.69 +(* REVISIT: should this be generalized to all semiring_div types? *)
    1.70  lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
    1.71  
    1.72  lemma zmod_zadd_left_eq: "(a+b) mod (c::int) = ((a mod c) + b) mod c"
    1.73 -apply (rule trans [symmetric])
    1.74 -apply (rule zmod_zadd1_eq, simp)
    1.75 -apply (rule zmod_zadd1_eq [symmetric])
    1.76 -done
    1.77 +by (rule mod_add_left_eq)
    1.78  
    1.79  lemma zmod_zadd_right_eq: "(a+b) mod (c::int) = (a + (b mod c)) mod c"
    1.80 -apply (rule trans [symmetric])
    1.81 -apply (rule zmod_zadd1_eq, simp)
    1.82 -apply (rule zmod_zadd1_eq [symmetric])
    1.83 -done
    1.84 +by (rule mod_add_right_eq)
    1.85  
    1.86 -lemma zmod_zadd_self1[simp]: "(a+b) mod a = b mod (a::int)"
    1.87 -apply (case_tac "a = 0", simp)
    1.88 -apply (simp add: zmod_zadd1_eq)
    1.89 -done
    1.90 +lemma zmod_zadd_self1: "(a+b) mod a = b mod (a::int)"
    1.91 +by (rule mod_add_self1) (* already declared [simp] *)
    1.92  
    1.93 -lemma zmod_zadd_self2[simp]: "(b+a) mod a = b mod (a::int)"
    1.94 -apply (case_tac "a = 0", simp)
    1.95 -apply (simp add: zmod_zadd1_eq)
    1.96 -done
    1.97 -
    1.98 +lemma zmod_zadd_self2: "(b+a) mod a = b mod (a::int)"
    1.99 +by (rule mod_add_self2) (* already declared [simp] *)
   1.100  
   1.101  lemma zmod_zdiff1_eq: fixes a::int
   1.102    shows "(a - b) mod c = (a mod c - b mod c) mod c" (is "?l = ?r")