merged.

--- a/src/HOL/Divides.thy	Fri Jan 09 08:22:44 2009 +0100
+++ b/src/HOL/Divides.thy	Fri Jan 09 09:49:01 2009 -0800
@@ -33,6 +33,10 @@
   unfolding mult_commute [of b]
   by (rule mod_div_equality)
 
+lemma mod_div_equality': "a mod b + a div b * b = a"
+  using mod_div_equality [of a b]
+  by (simp only: add_ac)
+
 lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
   by (simp add: mod_div_equality)
 
@@ -143,6 +147,173 @@
   then show "b mod a = 0" by simp
 qed
 
+lemma mod_div_trivial [simp]: "a mod b div b = 0"
+proof (cases "b = 0")
+  assume "b = 0"
+  thus ?thesis by simp
+next
+  assume "b \<noteq> 0"
+  hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
+    by (rule div_mult_self1 [symmetric])
+  also have "\<dots> = a div b"
+    by (simp only: mod_div_equality')
+  also have "\<dots> = a div b + 0"
+    by simp
+  finally show ?thesis
+    by (rule add_left_imp_eq)
+qed
+
+lemma mod_mod_trivial [simp]: "a mod b mod b = a mod b"
+proof -
+  have "a mod b mod b = (a mod b + a div b * b) mod b"
+    by (simp only: mod_mult_self1)
+  also have "\<dots> = a mod b"
+    by (simp only: mod_div_equality')
+  finally show ?thesis .
+qed
+
+text {* Addition respects modular equivalence. *}
+
+lemma mod_add_left_eq: "(a + b) mod c = (a mod c + b) mod c"
+proof -
+  have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
+    by (simp only: mod_div_equality)
+  also have "\<dots> = (a mod c + b + a div c * c) mod c"
+    by (simp only: add_ac)
+  also have "\<dots> = (a mod c + b) mod c"
+    by (rule mod_mult_self1)
+  finally show ?thesis .
+qed
+
+lemma mod_add_right_eq: "(a + b) mod c = (a + b mod c) mod c"
+proof -
+  have "(a + b) mod c = (a + (b div c * c + b mod c)) mod c"
+    by (simp only: mod_div_equality)
+  also have "\<dots> = (a + b mod c + b div c * c) mod c"
+    by (simp only: add_ac)
+  also have "\<dots> = (a + b mod c) mod c"
+    by (rule mod_mult_self1)
+  finally show ?thesis .
+qed
+
+lemma mod_add_eq: "(a + b) mod c = (a mod c + b mod c) mod c"
+by (rule trans [OF mod_add_left_eq mod_add_right_eq])
+
+lemma mod_add_cong:
+  assumes "a mod c = a' mod c"
+  assumes "b mod c = b' mod c"
+  shows "(a + b) mod c = (a' + b') mod c"
+proof -
+  have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
+    unfolding assms ..
+  thus ?thesis
+    by (simp only: mod_add_eq [symmetric])
+qed
+
+text {* Multiplication respects modular equivalence. *}
+
+lemma mod_mult_left_eq: "(a * b) mod c = ((a mod c) * b) mod c"
+proof -
+  have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
+    by (simp only: mod_div_equality)
+  also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
+    by (simp only: left_distrib right_distrib add_ac mult_ac)
+  also have "\<dots> = (a mod c * b) mod c"
+    by (rule mod_mult_self1)
+  finally show ?thesis .
+qed
+
+lemma mod_mult_right_eq: "(a * b) mod c = (a * (b mod c)) mod c"
+proof -
+  have "(a * b) mod c = (a * (b div c * c + b mod c)) mod c"
+    by (simp only: mod_div_equality)
+  also have "\<dots> = (a * (b mod c) + a * (b div c) * c) mod c"
+    by (simp only: left_distrib right_distrib add_ac mult_ac)
+  also have "\<dots> = (a * (b mod c)) mod c"
+    by (rule mod_mult_self1)
+  finally show ?thesis .
+qed
+
+lemma mod_mult_eq: "(a * b) mod c = ((a mod c) * (b mod c)) mod c"
+by (rule trans [OF mod_mult_left_eq mod_mult_right_eq])
+
+lemma mod_mult_cong:
+  assumes "a mod c = a' mod c"
+  assumes "b mod c = b' mod c"
+  shows "(a * b) mod c = (a' * b') mod c"
+proof -
+  have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
+    unfolding assms ..
+  thus ?thesis
+    by (simp only: mod_mult_eq [symmetric])
+qed
+
+lemma mod_mod_cancel:
+  assumes "c dvd b"
+  shows "a mod b mod c = a mod c"
+proof -
+  from `c dvd b` obtain k where "b = c * k"
+    by (rule dvdE)
+  have "a mod b mod c = a mod (c * k) mod c"
+    by (simp only: `b = c * k`)
+  also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
+    by (simp only: mod_mult_self1)
+  also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
+    by (simp only: add_ac mult_ac)
+  also have "\<dots> = a mod c"
+    by (simp only: mod_div_equality)
+  finally show ?thesis .
+qed
+
+end
+
+class ring_div = semiring_div + comm_ring_1
+begin
+
+text {* Negation respects modular equivalence. *}
+
+lemma mod_minus_eq: "(- a) mod b = (- (a mod b)) mod b"
+proof -
+  have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
+    by (simp only: mod_div_equality)
+  also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
+    by (simp only: minus_add_distrib minus_mult_left add_ac)
+  also have "\<dots> = (- (a mod b)) mod b"
+    by (rule mod_mult_self1)
+  finally show ?thesis .
+qed
+
+lemma mod_minus_cong:
+  assumes "a mod b = a' mod b"
+  shows "(- a) mod b = (- a') mod b"
+proof -
+  have "(- (a mod b)) mod b = (- (a' mod b)) mod b"
+    unfolding assms ..
+  thus ?thesis
+    by (simp only: mod_minus_eq [symmetric])
+qed
+
+text {* Subtraction respects modular equivalence. *}
+
+lemma mod_diff_left_eq: "(a - b) mod c = (a mod c - b) mod c"
+  unfolding diff_minus
+  by (intro mod_add_cong mod_minus_cong) simp_all
+
+lemma mod_diff_right_eq: "(a - b) mod c = (a - b mod c) mod c"
+  unfolding diff_minus
+  by (intro mod_add_cong mod_minus_cong) simp_all
+
+lemma mod_diff_eq: "(a - b) mod c = (a mod c - b mod c) mod c"
+  unfolding diff_minus
+  by (intro mod_add_cong mod_minus_cong) simp_all
+
+lemma mod_diff_cong:
+  assumes "a mod c = a' mod c"
+  assumes "b mod c = b' mod c"
+  shows "(a - b) mod c = (a' - b') mod c"
+  unfolding diff_minus using assms
+  by (intro mod_add_cong mod_minus_cong)
+
 end
 
 
@@ -467,22 +638,14 @@
 done
 
 lemma mod_mult1_eq: "(a*b) mod c = a*(b mod c) mod (c::nat)"
-apply (cases "c = 0", simp)
-apply (blast intro: divmod_rel [THEN divmod_rel_mult1_eq, THEN mod_eq])
-done
+  by (rule mod_mult_right_eq)
 
 lemma mod_mult1_eq': "(a*b) mod (c::nat) = ((a mod c) * b) mod c"
-  apply (rule trans)
-   apply (rule_tac s = "b*a mod c" in trans)
-    apply (rule_tac [2] mod_mult1_eq)
-   apply (simp_all add: mult_commute)
-  done
+  by (rule mod_mult_left_eq)
 
 lemma mod_mult_distrib_mod:
   "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c"
-apply (rule mod_mult1_eq' [THEN trans])
-apply (rule mod_mult1_eq)
-done
+  by (rule mod_mult_eq)
 
 lemma divmod_rel_add1_eq:
   "[| divmod_rel a c aq ar; divmod_rel b c bq br;  c > 0 |]
@@ -497,9 +660,7 @@
 done
 
 lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"
-apply (cases "c = 0", simp)
-apply (blast intro: divmod_rel_add1_eq [THEN mod_eq] divmod_rel)
-done
+  by (rule mod_add_eq)
 
 lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
   apply (cut_tac m = q and n = c in mod_less_divisor)
@@ -618,11 +779,11 @@
 apply (auto simp add: Suc_diff_le le_mod_geq)
 done
 
-lemma nat_mod_div_trivial [simp]: "m mod n div n = (0 :: nat)"
-  by (cases "n = 0") auto
+lemma nat_mod_div_trivial: "m mod n div n = (0 :: nat)"
+  by simp
 
-lemma nat_mod_mod_trivial [simp]: "m mod n mod n = (m mod n :: nat)"
-  by (cases "n = 0") auto
+lemma nat_mod_mod_trivial: "m mod n mod n = (m mod n :: nat)"
+  by simp
 
 
 subsubsection {* The Divides Relation *}
@@ -718,18 +879,6 @@
   apply (simp add: power_add)
   done
 
-lemma mod_add_left_eq: "((a::nat) + b) mod c = (a mod c + b) mod c"
-  apply (rule trans [symmetric])
-   apply (rule mod_add1_eq, simp)
-  apply (rule mod_add1_eq [symmetric])
-  done
-
-lemma mod_add_right_eq: "(a+b) mod (c::nat) = (a + (b mod c)) mod c"
-  apply (rule trans [symmetric])
-   apply (rule mod_add1_eq, simp)
-  apply (rule mod_add1_eq [symmetric])
-  done
-
 lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
   by (induct n) auto
 

--- a/src/HOL/IntDiv.thy	Fri Jan 09 08:22:44 2009 +0100
+++ b/src/HOL/IntDiv.thy	Fri Jan 09 09:49:01 2009 -0800
@@ -747,12 +747,12 @@
 lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a"
 by (simp add: zdiv_zmult1_eq)
 
-lemma mod_div_trivial [simp]: "(a mod b) div b = (0::int)"
+lemma zmod_zdiv_trivial: "(a mod b) div b = (0::int)"
 apply (case_tac "b = 0", simp)
 apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
 done
 
-lemma mod_mod_trivial [simp]: "(a mod b) mod b = a mod (b::int)"
+lemma zmod_zmod_trivial: "(a mod b) mod b = a mod (b::int)"
 apply (case_tac "b = 0", simp)
 apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial)
 done
@@ -776,72 +776,50 @@
 apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod)
 done
 
-lemma zdiv_zadd_self1[simp]: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
-by (simp add: zdiv_zadd1_eq)
-
-lemma zdiv_zadd_self2[simp]: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
-by (simp add: zdiv_zadd1_eq)
-
-instance int :: semiring_div
+instance int :: ring_div
 proof
   fix a b c :: int
   assume not0: "b \<noteq> 0"
   show "(a + c * b) div b = c + a div b"
     unfolding zdiv_zadd1_eq [of a "c * b"] using not0 
-      by (simp add: zmod_zmult1_eq)
+      by (simp add: zmod_zmult1_eq zmod_zdiv_trivial)
 qed auto
 
-lemma zdiv_zmult_self2 [simp]: "b \<noteq> (0::int) ==> (b*a) div b = a"
-by (subst mult_commute, erule zdiv_zmult_self1)
+lemma zdiv_zadd_self1: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
+by (rule div_add_self1) (* already declared [simp] *)
+
+lemma zdiv_zadd_self2: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
+by (rule div_add_self2) (* already declared [simp] *)
 
-lemma zmod_zmult_self1 [simp]: "(a*b) mod b = (0::int)"
-by (simp add: zmod_zmult1_eq)
+lemma zdiv_zmult_self2: "b \<noteq> (0::int) ==> (b*a) div b = a"
+by (rule div_mult_self1_is_id) (* already declared [simp] *)
 
-lemma zmod_zmult_self2 [simp]: "(b*a) mod b = (0::int)"
-by (simp add: mult_commute zmod_zmult1_eq)
+lemma zmod_zmult_self1: "(a*b) mod b = (0::int)"
+by (rule mod_mult_self2_is_0) (* already declared [simp] *)
+
+lemma zmod_zmult_self2: "(b*a) mod b = (0::int)"
+by (rule mod_mult_self1_is_0) (* already declared [simp] *)
 
 lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
-proof
-  assume "m mod d = 0"
-  with zmod_zdiv_equality[of m d] show "EX q::int. m = d*q" by auto
-next
-  assume "EX q::int. m = d*q"
-  thus "m mod d = 0" by auto
-qed
+by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
 
+(* REVISIT: should this be generalized to all semiring_div types? *)
 lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
 
 lemma zmod_zadd_left_eq: "(a+b) mod (c::int) = ((a mod c) + b) mod c"
-apply (rule trans [symmetric])
-apply (rule zmod_zadd1_eq, simp)
-apply (rule zmod_zadd1_eq [symmetric])
-done
+by (rule mod_add_left_eq)
 
 lemma zmod_zadd_right_eq: "(a+b) mod (c::int) = (a + (b mod c)) mod c"
-apply (rule trans [symmetric])
-apply (rule zmod_zadd1_eq, simp)
-apply (rule zmod_zadd1_eq [symmetric])
-done
+by (rule mod_add_right_eq)
 
-lemma zmod_zadd_self1[simp]: "(a+b) mod a = b mod (a::int)"
-apply (case_tac "a = 0", simp)
-apply (simp add: zmod_zadd1_eq)
-done
+lemma zmod_zadd_self1: "(a+b) mod a = b mod (a::int)"
+by (rule mod_add_self1) (* already declared [simp] *)
 
-lemma zmod_zadd_self2[simp]: "(b+a) mod a = b mod (a::int)"
-apply (case_tac "a = 0", simp)
-apply (simp add: zmod_zadd1_eq)
-done
-
+lemma zmod_zadd_self2: "(b+a) mod a = b mod (a::int)"
+by (rule mod_add_self2) (* already declared [simp] *)
 
-lemma zmod_zdiff1_eq: fixes a::int
-  shows "(a - b) mod c = (a mod c - b mod c) mod c" (is "?l = ?r")
-proof -
-  have "?l = (c + (a mod c - b mod c)) mod c"
-    using zmod_zadd1_eq[of a "-b" c] by(simp add:ring_simps zmod_zminus1_eq_if)
-  also have "\<dots> = ?r" by simp
-  finally show ?thesis .
-qed
+lemma zmod_zdiff1_eq: "(a - b) mod c = (a mod c - b mod c) mod (c::int)"
+by (rule mod_diff_eq)
 
 subsection{*Proving  @{term "a div (b*c) = (a div b) div c"} *}
 
@@ -954,18 +932,8 @@
 apply (auto simp add: mult_commute)
 done
 
-lemma zmod_zmod_cancel:
-assumes "n dvd m" shows "(k::int) mod m mod n = k mod n"
-proof -
-  from `n dvd m` obtain r where "m = n*r" by(auto simp:dvd_def)
-  have "k mod n = (m * (k div m) + k mod m) mod n"
-    using zmod_zdiv_equality[of k m] by simp
-  also have "\<dots> = (m * (k div m) mod n + k mod m mod n) mod n"
-    by(subst zmod_zadd1_eq, rule refl)
-  also have "m * (k div m) mod n = 0" using `m = n*r`
-    by(simp add:mult_ac)
-  finally show ?thesis by simp
-qed
+lemma zmod_zmod_cancel: "n dvd m \<Longrightarrow> (k::int) mod m mod n = k mod n"
+by (rule mod_mod_cancel)
 
 
 subsection {*Splitting Rules for div and mod*}
@@ -1169,50 +1137,31 @@
 subsection {* The Divides Relation *}
 
 lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
-  by (simp add: dvd_def zmod_eq_0_iff)
+  by (rule dvd_eq_mod_eq_0)
 
 lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
   zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard]
 
-lemma zdvd_0_right [iff]: "(m::int) dvd 0"
-  by (simp add: dvd_def)
+lemma zdvd_0_right: "(m::int) dvd 0"
+  by (rule dvd_0_right) (* already declared [iff] *)
 
-lemma zdvd_0_left [iff,noatp]: "(0 dvd (m::int)) = (m = 0)"
-  by (simp add: dvd_def)
+lemma zdvd_0_left: "(0 dvd (m::int)) = (m = 0)"
+  by (rule dvd_0_left_iff) (* already declared [noatp,simp] *)
 
-lemma zdvd_1_left [iff]: "1 dvd (m::int)"
-  by (simp add: dvd_def)
+lemma zdvd_1_left: "1 dvd (m::int)"
+  by (rule one_dvd) (* already declared [simp] *)
 
 lemma zdvd_refl [simp]: "m dvd (m::int)"
-  by (auto simp add: dvd_def intro: zmult_1_right [symmetric])
+  by (rule dvd_refl) (* TODO: declare generic dvd_refl [simp] *)
 
 lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
-  by (auto simp add: dvd_def intro: mult_assoc)
+  by (rule dvd_trans)
 
 lemma zdvd_zminus_iff: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
-proof
-  assume "m dvd - n"
-  then obtain k where "- n = m * k" ..
-  then have "n = m * - k" by simp
-  then show "m dvd n" ..
-next
-  assume "m dvd n"
-  then have "m dvd n * -1" by (rule dvd_mult2)
-  then show "m dvd - n" by simp
-qed
+  by (rule dvd_minus_iff)
 
 lemma zdvd_zminus2_iff: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
-proof
-  assume "- m dvd n"
-  then obtain k where "n = - m * k" ..
-  then have "n = m * - k" by simp
-  then show "m dvd n" ..
-next
-  assume "m dvd n"
-  then obtain k where "n = m * k" ..
-  then have "n = - m * - k" by simp
-  then show "- m dvd n" ..
-qed
+  by (rule minus_dvd_iff)
 
 lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)" 
   by (cases "i > 0") (simp_all add: zdvd_zminus2_iff)
@@ -1227,9 +1176,7 @@
   done
 
 lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)"
-  apply (simp add: dvd_def)
-  apply (blast intro: right_distrib [symmetric])
-  done
+  by (rule dvd_add)
 
 lemma zdvd_dvd_eq: assumes anz:"a \<noteq> 0" and ab: "(a::int) dvd b" and ba:"b dvd a" 
   shows "\<bar>a\<bar> = \<bar>b\<bar>"
@@ -1244,9 +1191,7 @@
 qed
 
 lemma zdvd_zdiff: "k dvd m ==> k dvd n ==> k dvd (m - n :: int)"
-  apply (simp add: dvd_def)
-  apply (blast intro: right_diff_distrib [symmetric])
-  done
+  by (rule Ring_and_Field.dvd_diff)
 
 lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
   apply (subgoal_tac "m = n + (m - n)")
@@ -1255,34 +1200,22 @@
   done
 
 lemma zdvd_zmult: "k dvd (n::int) ==> k dvd m * n"
-  apply (simp add: dvd_def)
-  apply (blast intro: mult_left_commute)
-  done
+  by (rule dvd_mult)
 
 lemma zdvd_zmult2: "k dvd (m::int) ==> k dvd m * n"
-  apply (subst mult_commute)
-  apply (erule zdvd_zmult)
-  done
+  by (rule dvd_mult2)
 
-lemma zdvd_triv_right [iff]: "(k::int) dvd m * k"
-  apply (rule zdvd_zmult)
-  apply (rule zdvd_refl)
-  done
+lemma zdvd_triv_right: "(k::int) dvd m * k"
+  by (rule dvd_triv_right) (* already declared [simp] *)
 
-lemma zdvd_triv_left [iff]: "(k::int) dvd k * m"
-  apply (rule zdvd_zmult2)
-  apply (rule zdvd_refl)
-  done
+lemma zdvd_triv_left: "(k::int) dvd k * m"
+  by (rule dvd_triv_left) (* already declared [simp] *)
 
 lemma zdvd_zmultD2: "j * k dvd n ==> j dvd (n::int)"
-  apply (simp add: dvd_def)
-  apply (simp add: mult_assoc, blast)
-  done
+  by (rule dvd_mult_left)
 
 lemma zdvd_zmultD: "j * k dvd n ==> k dvd (n::int)"
-  apply (rule zdvd_zmultD2)
-  apply (subst mult_commute, assumption)
-  done
+  by (rule dvd_mult_right)
 
 lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n"
   by (rule mult_dvd_mono)
@@ -1333,7 +1266,7 @@
   {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
     with h have False by (simp add: mult_assoc)}
   hence "n = m * h" by blast
-  thus ?thesis by blast
+  thus ?thesis by simp
 qed
 
 lemma zdvd_zmult_cancel_disj[simp]:
@@ -1371,8 +1304,8 @@
       then show ?thesis by (simp only: negative_eq_positive) auto
     qed
   qed
-  then show ?thesis by (auto elim!: dvdE simp only: zmult_int [symmetric])
-qed 
+  then show ?thesis by (auto elim!: dvdE simp only: zdvd_triv_left int_mult)
+qed
 
 lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
 proof
@@ -1404,10 +1337,10 @@
   by (auto simp add: dvd_int_iff)
 
 lemma zminus_dvd_iff [iff]: "(-z dvd w) = (z dvd (w::int))"
-  by (simp add: zdvd_zminus2_iff)
+  by (rule minus_dvd_iff)
 
 lemma dvd_zminus_iff [iff]: "(z dvd -w) = (z dvd (w::int))"
-  by (simp add: zdvd_zminus_iff)
+  by (rule dvd_minus_iff)
 
 lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
   apply (rule_tac z=n in int_cases)
@@ -1449,20 +1382,13 @@
 
 text {* by Brian Huffman *}
 lemma zminus_zmod: "- ((x::int) mod m) mod m = - x mod m"
-by (simp only: zmod_zminus1_eq_if mod_mod_trivial)
+by (rule mod_minus_eq [symmetric])
 
 lemma zdiff_zmod_left: "(x mod m - y) mod m = (x - y) mod (m::int)"
-by (simp only: diff_def zmod_zadd_left_eq [symmetric])
+by (rule mod_diff_left_eq [symmetric])
 
 lemma zdiff_zmod_right: "(x - y mod m) mod m = (x - y) mod (m::int)"
-proof -
-  have "(x + - (y mod m) mod m) mod m = (x + - y mod m) mod m"
-    by (simp only: zminus_zmod)
-  hence "(x + - (y mod m)) mod m = (x + - y) mod m"
-    by (simp only: zmod_zadd_right_eq [symmetric])
-  thus "(x - y mod m) mod m = (x - y) mod m"
-    by (simp only: diff_def)
-qed
+by (rule mod_diff_right_eq [symmetric])
 
 lemmas zmod_simps =
   IntDiv.zmod_zadd_left_eq  [symmetric]

--- a/src/HOL/NatBin.thy	Fri Jan 09 08:22:44 2009 +0100
+++ b/src/HOL/NatBin.thy	Fri Jan 09 09:49:01 2009 -0800
@@ -29,14 +29,14 @@
   unfolding nat_number_of_def ..
 
 abbreviation (xsymbols)
-  square :: "'a::power => 'a"  ("(_\<twosuperior>)" [1000] 999) where
+  power2 :: "'a::power => 'a"  ("(_\<twosuperior>)" [1000] 999) where
   "x\<twosuperior> == x^2"
 
 notation (latex output)
-  square  ("(_\<twosuperior>)" [1000] 999)
+  power2  ("(_\<twosuperior>)" [1000] 999)
 
 notation (HTML output)
-  square  ("(_\<twosuperior>)" [1000] 999)
+  power2  ("(_\<twosuperior>)" [1000] 999)
 
 
 subsection {* Predicate for negative binary numbers *}

--- a/src/HOL/NumberTheory/IntPrimes.thy	Fri Jan 09 08:22:44 2009 +0100
+++ b/src/HOL/NumberTheory/IntPrimes.thy	Fri Jan 09 09:49:01 2009 -0800
@@ -94,7 +94,7 @@
 
 lemma zgcd_zdvd_zgcd_zmult: "zgcd m n dvd zgcd (k * m) n"
   apply (simp add: zgcd_greatest_iff)
-  apply (blast intro: zdvd_trans)
+  apply (blast intro: zdvd_trans dvd_triv_right)
   done
 
 lemma zgcd_zmult_zdvd_zgcd:

--- a/src/HOL/Ring_and_Field.thy	Fri Jan 09 08:22:44 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy	Fri Jan 09 09:49:01 2009 -0800
@@ -235,19 +235,21 @@
 lemma minus_mult_right: "- (a * b) = a * - b"
   by (rule equals_zero_I) (simp add: right_distrib [symmetric]) 
 
+text{*Extract signs from products*}
+lemmas mult_minus_left [simp] = minus_mult_left [symmetric]
+lemmas mult_minus_right [simp] = minus_mult_right [symmetric]
+
 lemma minus_mult_minus [simp]: "- a * - b = a * b"
-  by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])
+  by simp
 
 lemma minus_mult_commute: "- a * b = a * - b"
-  by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])
+  by simp
 
 lemma right_diff_distrib: "a * (b - c) = a * b - a * c"
-  by (simp add: right_distrib diff_minus 
-    minus_mult_left [symmetric] minus_mult_right [symmetric]) 
+  by (simp add: right_distrib diff_minus)
 
 lemma left_diff_distrib: "(a - b) * c = a * c - b * c"
-  by (simp add: left_distrib diff_minus 
-    minus_mult_left [symmetric] minus_mult_right [symmetric]) 
+  by (simp add: left_distrib diff_minus)
 
 lemmas ring_distribs =
   right_distrib left_distrib left_diff_distrib right_diff_distrib
@@ -293,6 +295,33 @@
 subclass ring_1 ..
 subclass comm_semiring_1_cancel ..
 
+lemma dvd_minus_iff: "x dvd - y \<longleftrightarrow> x dvd y"
+proof
+  assume "x dvd - y"
+  then have "x dvd - 1 * - y" by (rule dvd_mult)
+  then show "x dvd y" by simp
+next
+  assume "x dvd y"
+  then have "x dvd - 1 * y" by (rule dvd_mult)
+  then show "x dvd - y" by simp
+qed
+
+lemma minus_dvd_iff: "- x dvd y \<longleftrightarrow> x dvd y"
+proof
+  assume "- x dvd y"
+  then obtain k where "y = - x * k" ..
+  then have "y = x * - k" by simp
+  then show "x dvd y" ..
+next
+  assume "x dvd y"
+  then obtain k where "y = x * k" ..
+  then have "y = - x * - k" by simp
+  then show "- x dvd y" ..
+qed
+
+lemma dvd_diff: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
+  by (simp add: diff_minus dvd_add dvd_minus_iff)
+
 end
 
 class ring_no_zero_divisors = ring + no_zero_divisors
@@ -397,67 +426,47 @@
 apply auto
 done
 
-lemma nonzero_inverse_minus_eq:
-  assumes "a \<noteq> 0"
-  shows "inverse (- a) = - inverse a"
-proof -
-  have "- a * inverse (- a) = - a * - inverse a"
-    using assms by simp
-  then show ?thesis unfolding mult_cancel_left using assms by simp 
-qed
-
-lemma nonzero_inverse_inverse_eq:
-  assumes "a \<noteq> 0"
-  shows "inverse (inverse a) = a"
-proof -
-  have "(inverse (inverse a) * inverse a) * a = a" 
-    using assms by (simp add: nonzero_imp_inverse_nonzero)
-  then show ?thesis using assms by (simp add: mult_assoc)
-qed
-
-lemma nonzero_inverse_eq_imp_eq:
-  assumes inveq: "inverse a = inverse b"
-    and anz:  "a \<noteq> 0"
-    and bnz:  "b \<noteq> 0"
-  shows "a = b"
-proof -
-  have "a * inverse b = a * inverse a"
-    by (simp add: inveq)
-  hence "(a * inverse b) * b = (a * inverse a) * b"
-    by simp
-  then show "a = b"
-    by (simp add: mult_assoc anz bnz)
-qed
-
-lemma inverse_1 [simp]: "inverse 1 = 1"
-proof -
-  have "inverse 1 * 1 = 1" 
-    by (rule left_inverse) (rule one_neq_zero)
-  then show ?thesis by simp
-qed
-
 lemma inverse_unique: 
   assumes ab: "a * b = 1"
   shows "inverse a = b"
 proof -
   have "a \<noteq> 0" using ab by (cases "a = 0") simp_all
-  moreover have "inverse a * (a * b) = inverse a" by (simp add: ab) 
-  ultimately show ?thesis by (simp add: mult_assoc [symmetric]) 
+  moreover have "inverse a * (a * b) = inverse a" by (simp add: ab)
+  ultimately show ?thesis by (simp add: mult_assoc [symmetric])
 qed
 
+lemma nonzero_inverse_minus_eq:
+  "a \<noteq> 0 \<Longrightarrow> inverse (- a) = - inverse a"
+  by (rule inverse_unique) simp
+
+lemma nonzero_inverse_inverse_eq:
+  "a \<noteq> 0 \<Longrightarrow> inverse (inverse a) = a"
+  by (rule inverse_unique) simp
+
+lemma nonzero_inverse_eq_imp_eq:
+  assumes "inverse a = inverse b" and "a \<noteq> 0" and "b \<noteq> 0"
+  shows "a = b"
+proof -
+  from `inverse a = inverse b`
+  have "inverse (inverse a) = inverse (inverse b)"
+    by (rule arg_cong)
+  with `a \<noteq> 0` and `b \<noteq> 0` show "a = b"
+    by (simp add: nonzero_inverse_inverse_eq)
+qed
+
+lemma inverse_1 [simp]: "inverse 1 = 1"
+  by (rule inverse_unique) simp
+
 lemma nonzero_inverse_mult_distrib: 
-  assumes anz: "a \<noteq> 0"
-    and bnz: "b \<noteq> 0"
+  assumes "a \<noteq> 0" and "b \<noteq> 0"
   shows "inverse (a * b) = inverse b * inverse a"
 proof -
-  have "inverse (a * b) * (a * b) * inverse b = inverse b" 
-    by (simp add: anz bnz)
-  hence "inverse (a * b) * a = inverse b" 
-    by (simp add: mult_assoc bnz)
-  hence "inverse (a * b) * a * inverse a = inverse b * inverse a" 
-    by simp
+  have "a * (b * inverse b) * inverse a = 1"
+    using assms by simp
+  hence "a * b * (inverse b * inverse a) = 1"
+    by (simp only: mult_assoc)
   thus ?thesis
-    by (simp add: mult_assoc anz)
+    by (rule inverse_unique)
 qed
 
 lemma division_ring_inverse_add:
@@ -1266,19 +1275,19 @@
 subsection {* Division and Unary Minus *}
 
 lemma nonzero_minus_divide_left: "b \<noteq> 0 ==> - (a/b) = (-a) / (b::'a::field)"
-by (simp add: divide_inverse minus_mult_left)
+by (simp add: divide_inverse)
 
 lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a/b) = a / -(b::'a::field)"
-by (simp add: divide_inverse nonzero_inverse_minus_eq minus_mult_right)
+by (simp add: divide_inverse nonzero_inverse_minus_eq)
 
 lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a)/(-b) = a / (b::'a::field)"
 by (simp add: divide_inverse nonzero_inverse_minus_eq)
 
 lemma minus_divide_left: "- (a/b) = (-a) / (b::'a::field)"
-by (simp add: divide_inverse minus_mult_left [symmetric])
+by (simp add: divide_inverse)
 
 lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
-by (simp add: divide_inverse minus_mult_right [symmetric])
+by (simp add: divide_inverse)
 
 
 text{*The effect is to extract signs from divisions*}
@@ -1286,11 +1295,6 @@
 lemmas divide_minus_right = minus_divide_right [symmetric]
 declare divide_minus_left [simp]   divide_minus_right [simp]
 
-text{*Also, extract signs from products*}
-lemmas mult_minus_left = minus_mult_left [symmetric]
-lemmas mult_minus_right = minus_mult_right [symmetric]
-declare mult_minus_left [simp]   mult_minus_right [simp]
-
 lemma minus_divide_divide [simp]:
   "(-a)/(-b) = a / (b::'a::{field,division_by_zero})"
 apply (cases "b=0", simp) 

--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Fri Jan 09 08:22:44 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Fri Jan 09 09:49:01 2009 -0800
@@ -10,6 +10,12 @@
 
 structure Domain_Theorems = struct
 
+val quiet_mode = ref false;
+val trace_domain = ref false;
+
+fun message s = if !quiet_mode then () else writeln s;
+fun trace s = if !trace_domain then tracing s else ();
+
 local
 
 val adm_impl_admw = @{thm adm_impl_admw};
@@ -115,7 +121,7 @@
 fun theorems (((dname, _), cons) : eq, eqs : eq list) thy =
 let
 
-val dummy = writeln ("Proving isomorphism properties of domain "^dname^" ...");
+val _ = message ("Proving isomorphism properties of domain "^dname^" ...");
 val pg = pg' thy;
 
 (* ----- getting the axioms and definitions --------------------------------- *)
@@ -158,6 +164,8 @@
 
 (* ----- generating beta reduction rules from definitions-------------------- *)
 
+val _ = trace " Proving beta reduction rules...";
+
 local
   fun arglist (Const _ $ Abs (s, _, t)) =
     let
@@ -179,7 +187,9 @@
     in pg (def::betas) appl (K [rtac reflexive_thm 1]) end;
 end;
 
+val _ = trace "Proving when_appl...";
 val when_appl = appl_of_def ax_when_def;
+val _ = trace "Proving con_appls...";
 val con_appls = map appl_of_def axs_con_def;
 
 local
@@ -229,7 +239,9 @@
     rewrite_goals_tac [mk_meta_eq iso_swap],
     rtac thm3 1];
 in
+  val _ = trace " Proving exhaust...";
   val exhaust = pg con_appls (mk_trp exh) (K tacs);
+  val _ = trace " Proving casedist...";
   val casedist =
     standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
 end;
@@ -239,6 +251,7 @@
   fun bound_fun i _ = Bound (length cons - i);
   val when_app = list_ccomb (%%:(dname^"_when"), mapn bound_fun 1 cons);
 in
+  val _ = trace " Proving when_strict...";
   val when_strict =
     let
       val axs = [when_appl, mk_meta_eq rep_strict];
@@ -246,6 +259,7 @@
       val tacs = [resolve_tac [sscase1, ssplit1, strictify1] 1];
     in pg axs goal (K tacs) end;
 
+  val _ = trace " Proving when_apps...";
   val when_apps =
     let
       fun one_when n (con,args) =
@@ -276,6 +290,7 @@
       val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
     in pg axs_dis_def goal (K tacs) end;
 
+  val _ = trace " Proving dis_apps...";
   val dis_apps = maps (fn (c,_) => map (dis_app c) cons) cons;
 
   fun dis_defin (con, args) =
@@ -288,7 +303,9 @@
           (asm_simp_tac (HOLCF_ss addsimps dis_apps) 1))];
     in pg [] goal (K tacs) end;
 
+  val _ = trace " Proving dis_stricts...";
   val dis_stricts = map dis_strict cons;
+  val _ = trace " Proving dis_defins...";
   val dis_defins = map dis_defin cons;
 in
   val dis_rews = dis_stricts @ dis_defins @ dis_apps;
@@ -301,6 +318,7 @@
       val tacs = [rtac when_strict 1];
     in pg axs_mat_def goal (K tacs) end;
 
+  val _ = trace " Proving mat_stricts...";
   val mat_stricts = map mat_strict cons;
 
   fun one_mat c (con, args) =
@@ -314,6 +332,7 @@
       val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
     in pg axs_mat_def goal (K tacs) end;
 
+  val _ = trace " Proving mat_apps...";
   val mat_apps =
     maps (fn (c,_) => map (one_mat c) cons) cons;
 in
@@ -346,7 +365,9 @@
       val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
     in pg axs goal (K tacs) end;
 
+  val _ = trace " Proving pat_stricts...";
   val pat_stricts = map pat_strict cons;
+  val _ = trace " Proving pat_apps...";
   val pat_apps = maps (fn c => map (pat_app c) cons) cons;
 in
   val pat_rews = pat_stricts @ pat_apps;
@@ -374,7 +395,9 @@
         asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
     in pg [] goal tacs end;
 in
+  val _ = trace " Proving con_stricts...";
   val con_stricts = maps con_strict cons;
+  val _ = trace " Proving pat_defins...";
   val con_defins = map con_defin cons;
   val con_rews = con_stricts @ con_defins;
 end;
@@ -391,6 +414,7 @@
         REPEAT (resolve_tac rules 1 ORELSE atac 1)];
     in pg con_appls goal (K tacs) end;
 in
+  val _ = trace " Proving con_compacts...";
   val con_compacts = map con_compact cons;
 end;
 
@@ -402,6 +426,7 @@
   fun sel_strict (_, args) =
     List.mapPartial (Option.map one_sel o sel_of) args;
 in
+  val _ = trace " Proving sel_stricts...";
   val sel_stricts = maps sel_strict cons;
 end;
 
@@ -439,6 +464,7 @@
   fun one_con (c, args) =
     flat (map_filter I (mapn (one_sel' c) 0 args));
 in
+  val _ = trace " Proving sel_apps...";
   val sel_apps = maps one_con cons;
 end;
 
@@ -453,6 +479,7 @@
           (asm_simp_tac (HOLCF_ss addsimps sel_apps) 1))];
     in pg [] goal (K tacs) end;
 in
+  val _ = trace " Proving sel_defins...";
   val sel_defins =
     if length cons = 1
     then List.mapPartial (fn arg => Option.map sel_defin (sel_of arg))
@@ -463,6 +490,7 @@
 val sel_rews = sel_stricts @ sel_defins @ sel_apps;
 val rev_contrapos = @{thm rev_contrapos};
 
+val _ = trace " Proving dist_les...";
 val distincts_le =
   let
     fun dist (con1, args1) (con2, args2) =
@@ -487,6 +515,8 @@
       | distincts (c::cs) = (map (distinct c) cs) :: distincts cs;
   in distincts cons end;
 val dist_les = flat (flat distincts_le);
+
+val _ = trace " Proving dist_eqs...";
 val dist_eqs =
   let
     fun distinct (_,args1) ((_,args2), leqs) =
@@ -517,6 +547,7 @@
     in pg con_appls prop end;
   val cons' = List.filter (fn (_,args) => args<>[]) cons;
 in
+  val _ = trace " Proving inverts...";
   val inverts =
     let
       val abs_less = ax_abs_iso RS (allI RS injection_less);
@@ -524,6 +555,7 @@
         [asm_full_simp_tac (HOLCF_ss addsimps [abs_less, spair_less]) 1];
     in map (fn (con, args) => pgterm (op <<) con args (K tacs)) cons' end;
 
+  val _ = trace " Proving injects...";
   val injects =
     let
       val abs_eq = ax_abs_iso RS (allI RS injection_eq);
@@ -551,6 +583,7 @@
       val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_apps) 1];
     in pg [ax_copy_def] goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
 in
+  val _ = trace " Proving copy_apps...";
   val copy_apps = map copy_app cons;
 end;
 
@@ -565,6 +598,7 @@
 
   fun has_nonlazy_rec (_, args) = exists is_nonlazy_rec args;
 in
+  val _ = trace " Proving copy_stricts...";
   val copy_stricts = map one_strict (List.filter has_nonlazy_rec cons);
 end;
 
@@ -603,7 +637,7 @@
 val conss  = map  snd        eqs;
 val comp_dname = Sign.full_bname thy comp_dnam;
 
-val d = writeln("Proving induction properties of domain "^comp_dname^" ...");
+val _ = message ("Proving induction properties of domain "^comp_dname^" ...");
 val pg = pg' thy;
 
 (* ----- getting the composite axiom and definitions ------------------------ *)
@@ -639,6 +673,7 @@
   val copy_con_rews  = copy_rews @ con_rews;
   val copy_take_defs =
     (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
+  val _ = trace " Proving take_stricts...";
   val take_stricts =
     let
       fun one_eq ((dn, args), _) = strict (dc_take dn $ %:"n");
@@ -656,6 +691,7 @@
     in pg axs_take_def goal (K [simp_tac iterate_Cprod_ss 1]) end;
   val take_0s = mapn take_0 1 dnames;
   fun c_UU_tac ctxt = case_UU_tac ctxt (take_stricts'::copy_con_rews) 1;
+  val _ = trace " Proving take_apps...";
   val take_apps =
     let
       fun mk_eqn dn (con, args) =
@@ -737,6 +773,7 @@
     val is_finite = forall (not o lazy_rec_to [] false) n__eqs;
   end;
 in (* local *)
+  val _ = trace " Proving finite_ind...";
   val finite_ind =
     let
       fun concf n dn = %:(P_name n) $ (dc_take dn $ %:"n" `%(x_name n));
@@ -768,6 +805,7 @@
         end;
     in pg'' thy [] goal tacf end;
 
+  val _ = trace " Proving take_lemmas...";
   val take_lemmas =
     let
       fun take_lemma n (dn, ax_reach) =
@@ -793,6 +831,7 @@
 
 (* ----- theorems concerning finiteness and induction ----------------------- *)
 
+  val _ = trace " Proving finites, ind...";
   val (finites, ind) =
     if is_finite
     then (* finite case *)
@@ -914,6 +953,7 @@
   fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1);
   val take_ss = HOL_ss addsimps take_rews;
   val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")"));
+  val _ = trace " Proving coind_lemma...";
   val coind_lemma =
     let
       fun mk_prj n _ = proj (%:"R") eqs n $ bnd_arg n 0 $ bnd_arg n 1;
@@ -940,6 +980,7 @@
         flat (mapn (x_tacs ctxt) 0 xs);
     in pg [ax_bisim_def] goal tacs end;
 in
+  val _ = trace " Proving coind...";
   val coind = 
     let
       fun mk_prj n x = mk_trp (proj (%:"R") eqs n $ %:x $ %:(x^"'"));