1.1 --- a/src/HOL/IntDiv.thy	Fri Feb 20 23:46:03 2009 +0100
     1.2 +++ b/src/HOL/IntDiv.thy	Sat Feb 21 09:58:26 2009 +0100
     1.3 @@ -747,41 +747,12 @@
     1.4    show ?thesis by simp
     1.5  qed
     1.6  
     1.7 -lemma zdiv_zadd_self1: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
     1.8 -by (rule div_add_self1) (* already declared [simp] *)
     1.9 -
    1.10 -lemma zdiv_zadd_self2: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
    1.11 -by (rule div_add_self2) (* already declared [simp] *)
    1.12 -
    1.13 -lemma zdiv_zmult_self2: "b \<noteq> (0::int) ==> (b*a) div b = a"
    1.14 -by (rule div_mult_self1_is_id) (* already declared [simp] *)
    1.15 -
    1.16 -lemma zmod_zmult_self1: "(a*b) mod b = (0::int)"
    1.17 -by (rule mod_mult_self2_is_0) (* already declared [simp] *)
    1.18 -
    1.19 -lemma zmod_zmult_self2: "(b*a) mod b = (0::int)"
    1.20 -by (rule mod_mult_self1_is_0) (* already declared [simp] *)
    1.21 -
    1.22  lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
    1.23  by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
    1.24  
    1.25  (* REVISIT: should this be generalized to all semiring_div types? *)
    1.26  lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
    1.27  
    1.28 -lemma zmod_zadd_left_eq: "(a+b) mod (c::int) = ((a mod c) + b) mod c"
    1.29 -by (rule mod_add_left_eq)
    1.30 -
    1.31 -lemma zmod_zadd_right_eq: "(a+b) mod (c::int) = (a + (b mod c)) mod c"
    1.32 -by (rule mod_add_right_eq)
    1.33 -
    1.34 -lemma zmod_zadd_self1: "(a+b) mod a = b mod (a::int)"
    1.35 -by (rule mod_add_self1) (* already declared [simp] *)
    1.36 -
    1.37 -lemma zmod_zadd_self2: "(b+a) mod a = b mod (a::int)"
    1.38 -by (rule mod_add_self2) (* already declared [simp] *)
    1.39 -
    1.40 -lemma zmod_zdiff1_eq: "(a - b) mod c = (a mod c - b mod c) mod (c::int)"
    1.41 -by (rule mod_diff_eq)
    1.42  
    1.43  subsection{*Proving  @{term "a div (b*c) = (a div b) div c"} *}
    1.44  
    1.45 @@ -896,9 +867,6 @@
    1.46  apply (auto simp add: mult_commute)
    1.47  done
    1.48  
    1.49 -lemma zmod_zmod_cancel: "n dvd m \<Longrightarrow> (k::int) mod m mod n = k mod n"
    1.50 -by (rule mod_mod_cancel)
    1.51 -
    1.52  
    1.53  subsection {*Splitting Rules for div and mod*}
    1.54  
    1.55 @@ -1350,8 +1318,8 @@
    1.56  by (rule mod_diff_right_eq [symmetric])
    1.57  
    1.58  lemmas zmod_simps =
    1.59 -  IntDiv.zmod_zadd_left_eq  [symmetric]
    1.60 -  IntDiv.zmod_zadd_right_eq [symmetric]
    1.61 +  mod_add_left_eq  [symmetric]
    1.62 +  mod_add_right_eq [symmetric]
    1.63    IntDiv.zmod_zmult1_eq     [symmetric]
    1.64    mod_mult_left_eq          [symmetric]
    1.65    IntDiv.zpower_zmod
    1.66 @@ -1426,14 +1394,14 @@
    1.67    assume H: "x mod n = y mod n"
    1.68    hence "x mod n - y mod n = 0" by simp
    1.69    hence "(x mod n - y mod n) mod n = 0" by simp 
    1.70 -  hence "(x - y) mod n = 0" by (simp add: zmod_zdiff1_eq[symmetric])
    1.71 +  hence "(x - y) mod n = 0" by (simp add: mod_diff_eq[symmetric])
    1.72    thus "n dvd x - y" by (simp add: zdvd_iff_zmod_eq_0)
    1.73  next
    1.74    assume H: "n dvd x - y"
    1.75    then obtain k where k: "x-y = n*k" unfolding dvd_def by blast
    1.76    hence "x = n*k + y" by simp
    1.77    hence "x mod n = (n*k + y) mod n" by simp
    1.78 -  thus "x mod n = y mod n" by (simp add: zmod_zadd_left_eq)
    1.79 +  thus "x mod n = y mod n" by (simp add: mod_add_left_eq)
    1.80  qed
    1.81  
    1.82  lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y  mod n" and xy:"y \<le> x"