# HG changeset patch
# User bulwahn
# Date 1332855244 -7200
# Node ID 9bfc32fc7cedfadf4fb108b2f8b13a262ed94541
# Parent  212f7a975d4950053f57aca26a641bd9f25c7935# Parent  d64fa2ca54b8fda6e69ee35483018c103b0ae02a
merged

diff -r 212f7a975d49 -r 9bfc32fc7ced NEWS
--- a/NEWS	Tue Mar 27 14:14:46 2012 +0200
+++ b/NEWS	Tue Mar 27 15:34:04 2012 +0200
@@ -136,6 +136,16 @@
 
 * New type synonym 'a rel = ('a * 'a) set
 
+* Theory Divides: Discontinued redundant theorems about div and mod.
+INCOMPATIBILITY, use the corresponding generic theorems instead.
+
+  DIVISION_BY_ZERO ~> div_by_0, mod_by_0
+  zdiv_self ~> div_self
+  zmod_self ~> mod_self
+  zdiv_zero ~> div_0
+  zmod_zero ~> mod_0
+  zmod_zdiv_trivial ~> mod_div_trivial
+
 * More default pred/set conversions on a couple of relation operations
 and predicates.  Consolidation of some relation theorems:
 
diff -r 212f7a975d49 -r 9bfc32fc7ced src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Tue Mar 27 14:14:46 2012 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Tue Mar 27 15:34:04 2012 +0200
@@ -1392,7 +1392,7 @@
     have "c div c\<le> l div c"
       by (simp add: zdiv_mono1[OF clel cp])
     then have ldcp:"0 < l div c" 
-      by (simp add: zdiv_self[OF cnz])
+      by (simp add: div_self[OF cnz])
     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
@@ -1410,7 +1410,7 @@
     have "c div c\<le> l div c"
       by (simp add: zdiv_mono1[OF clel cp])
     then have ldcp:"0 < l div c" 
-      by (simp add: zdiv_self[OF cnz])
+      by (simp add: div_self[OF cnz])
     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
@@ -1428,7 +1428,7 @@
     have "c div c\<le> l div c"
       by (simp add: zdiv_mono1[OF clel cp])
     then have ldcp:"0 < l div c" 
-      by (simp add: zdiv_self[OF cnz])
+      by (simp add: div_self[OF cnz])
     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
@@ -1446,7 +1446,7 @@
     have "c div c\<le> l div c"
       by (simp add: zdiv_mono1[OF clel cp])
     then have ldcp:"0 < l div c" 
-      by (simp add: zdiv_self[OF cnz])
+      by (simp add: div_self[OF cnz])
     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
@@ -1466,7 +1466,7 @@
     have "c div c\<le> l div c"
       by (simp add: zdiv_mono1[OF clel cp])
     then have ldcp:"0 < l div c" 
-      by (simp add: zdiv_self[OF cnz])
+      by (simp add: div_self[OF cnz])
     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
@@ -1484,7 +1484,7 @@
     have "c div c\<le> l div c"
       by (simp add: zdiv_mono1[OF clel cp])
     then have ldcp:"0 < l div c" 
-      by (simp add: zdiv_self[OF cnz])
+      by (simp add: div_self[OF cnz])
     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
@@ -1502,7 +1502,7 @@
     have "c div c\<le> l div c"
       by (simp add: zdiv_mono1[OF clel cp])
     then have ldcp:"0 < l div c" 
-      by (simp add: zdiv_self[OF cnz])
+      by (simp add: div_self[OF cnz])
     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
@@ -1519,7 +1519,7 @@
     have "c div c\<le> l div c"
       by (simp add: zdiv_mono1[OF clel cp])
     then have ldcp:"0 < l div c" 
-      by (simp add: zdiv_self[OF cnz])
+      by (simp add: div_self[OF cnz])
     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
diff -r 212f7a975d49 -r 9bfc32fc7ced src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Tue Mar 27 14:14:46 2012 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Tue Mar 27 15:34:04 2012 +0200
@@ -726,7 +726,7 @@
         have gpdd: "?g' dvd n" by simp
         have gpdgp: "?g' dvd ?g'" by simp
         from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" .
-        from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]]
+        from zdiv_mono1[OF g'n g'p, simplified div_self[OF gp0]]
         have "n div ?g' >0" by simp
         hence ?thesis using assms g1 g'1
           by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0 simpnum_numbound0) }
diff -r 212f7a975d49 -r 9bfc32fc7ced src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Tue Mar 27 14:14:46 2012 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Tue Mar 27 15:34:04 2012 +0200
@@ -1000,7 +1000,7 @@
         have gpdd: "?g' dvd n" by simp
         have gpdgp: "?g' dvd ?g'" by simp
         from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" .
-        from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]]
+        from zdiv_mono1[OF g'n g'p, simplified div_self[OF gp0]]
         have "n div ?g' >0" by simp
         hence ?thesis using assms g1 g'1
           by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0)}
@@ -1138,7 +1138,7 @@
       have "Ifm bs (Dvd (fst (simpdvd d t)) (snd(simpdvd d t))) = Ifm bs (Dvd (d div ?g') ?tt)"
         by (simp add: simpdvd_def Let_def)
       also have "\<dots> = (real d rdvd (Inum bs t))"
-        using rdvd_reduce[OF gpdd gpdgp g'p, where t="?t", simplified zdiv_self[OF gp0]] 
+        using rdvd_reduce[OF gpdd gpdgp g'p, where t="?t", simplified div_self[OF gp0]] 
           th2[symmetric] by simp
       finally have ?thesis by simp  }
     ultimately have ?thesis by blast
@@ -2420,7 +2420,7 @@
     have "c div c\<le> l div c"
       by (simp add: zdiv_mono1[OF clel cp])
     then have ldcp:"0 < l div c" 
-      by (simp add: zdiv_self[OF cnz])
+      by (simp add: div_self[OF cnz])
     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
@@ -2438,7 +2438,7 @@
     have "c div c\<le> l div c"
       by (simp add: zdiv_mono1[OF clel cp])
     then have ldcp:"0 < l div c" 
-      by (simp add: zdiv_self[OF cnz])
+      by (simp add: div_self[OF cnz])
     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
@@ -2456,7 +2456,7 @@
     have "c div c\<le> l div c"
       by (simp add: zdiv_mono1[OF clel cp])
     then have ldcp:"0 < l div c" 
-      by (simp add: zdiv_self[OF cnz])
+      by (simp add: div_self[OF cnz])
     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
@@ -2474,7 +2474,7 @@
     have "c div c\<le> l div c"
       by (simp add: zdiv_mono1[OF clel cp])
     then have ldcp:"0 < l div c" 
-      by (simp add: zdiv_self[OF cnz])
+      by (simp add: div_self[OF cnz])
     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
@@ -2492,7 +2492,7 @@
     have "c div c\<le> l div c"
       by (simp add: zdiv_mono1[OF clel cp])
     then have ldcp:"0 < l div c" 
-      by (simp add: zdiv_self[OF cnz])
+      by (simp add: div_self[OF cnz])
     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
@@ -2510,7 +2510,7 @@
     have "c div c\<le> l div c"
       by (simp add: zdiv_mono1[OF clel cp])
     then have ldcp:"0 < l div c" 
-      by (simp add: zdiv_self[OF cnz])
+      by (simp add: div_self[OF cnz])
     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
@@ -2528,7 +2528,7 @@
     have "c div c\<le> l div c"
       by (simp add: zdiv_mono1[OF clel cp])
     then have ldcp:"0 < l div c" 
-      by (simp add: zdiv_self[OF cnz])
+      by (simp add: div_self[OF cnz])
     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
@@ -2545,7 +2545,7 @@
     have "c div c\<le> l div c"
       by (simp add: zdiv_mono1[OF clel cp])
     then have ldcp:"0 < l div c" 
-      by (simp add: zdiv_self[OF cnz])
+      by (simp add: div_self[OF cnz])
     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
@@ -3970,7 +3970,7 @@
         by (simp add: numgcd_def)
       from `c > 0` have th': "c\<noteq>0" by auto
       from `c > 0` have cp: "c \<ge> 0" by simp
-      from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
+      from zdiv_mono2[OF cp th1 th, simplified div_self[OF th']]
       have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
     }
     with Lt a have ?case
@@ -3994,7 +3994,7 @@
         by (simp add: numgcd_def)
       from `c > 0` have th': "c\<noteq>0" by auto
       from `c > 0` have cp: "c \<ge> 0" by simp
-      from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
+      from zdiv_mono2[OF cp th1 th, simplified div_self[OF th']]
       have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
     }
     with Le a have ?case
@@ -4018,7 +4018,7 @@
         by (simp add: numgcd_def)
       from `c > 0` have th': "c\<noteq>0" by auto
       from `c > 0` have cp: "c \<ge> 0" by simp
-      from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
+      from zdiv_mono2[OF cp th1 th, simplified div_self[OF th']]
       have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
     }
     with Gt a have ?case
@@ -4042,7 +4042,7 @@
         by (simp add: numgcd_def)
       from `c > 0` have th': "c\<noteq>0" by auto
       from `c > 0` have cp: "c \<ge> 0" by simp
-      from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
+      from zdiv_mono2[OF cp th1 th, simplified div_self[OF th']]
       have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
     }
     with Ge a have ?case
@@ -4066,7 +4066,7 @@
         by (simp add: numgcd_def)
       from `c > 0` have th': "c\<noteq>0" by auto
       from `c > 0` have cp: "c \<ge> 0" by simp
-      from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
+      from zdiv_mono2[OF cp th1 th, simplified div_self[OF th']]
       have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
     }
     with Eq a have ?case
@@ -4090,7 +4090,7 @@
         by (simp add: numgcd_def)
       from `c > 0` have th': "c\<noteq>0" by auto
       from `c > 0` have cp: "c \<ge> 0" by simp
-      from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
+      from zdiv_mono2[OF cp th1 th, simplified div_self[OF th']]
       have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
     }
     with NEq a have ?case
diff -r 212f7a975d49 -r 9bfc32fc7ced src/HOL/Decision_Procs/cooper_tac.ML
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Tue Mar 27 14:14:46 2012 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Tue Mar 27 15:34:04 2012 +0200
@@ -73,10 +73,9 @@
       addsimps [refl,mod_add_eq, mod_add_left_eq,
           mod_add_right_eq,
           nat_div_add_eq, int_div_add_eq,
-          @{thm mod_self}, @{thm "zmod_self"},
-          @{thm mod_by_0}, @{thm div_by_0},
-          @{thm "zdiv_zero"}, @{thm "zmod_zero"}, @{thm "div_0"}, @{thm "mod_0"},
-          @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
+          @{thm mod_self},
+          @{thm div_by_0}, @{thm mod_by_0}, @{thm div_0}, @{thm mod_0},
+          @{thm div_by_1}, @{thm mod_by_1}, @{thm div_1}, @{thm mod_1},
           Suc_eq_plus1]
       addsimps @{thms add_ac}
       addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
diff -r 212f7a975d49 -r 9bfc32fc7ced src/HOL/Decision_Procs/ferrack_tac.ML
--- a/src/HOL/Decision_Procs/ferrack_tac.ML	Tue Mar 27 14:14:46 2012 +0200
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Tue Mar 27 15:34:04 2012 +0200
@@ -38,8 +38,6 @@
 val mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
 val nat_div_add_eq = @{thm div_add1_eq} RS sym;
 val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
-val ZDIVISION_BY_ZERO_MOD = @{thm DIVISION_BY_ZERO} RS conjunct2;
-val ZDIVISION_BY_ZERO_DIV = @{thm DIVISION_BY_ZERO} RS conjunct1;
 
 fun prepare_for_linr sg q fm = 
   let
diff -r 212f7a975d49 -r 9bfc32fc7ced src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Tue Mar 27 14:14:46 2012 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Tue Mar 27 15:34:04 2012 +0200
@@ -54,8 +54,6 @@
 val mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym;
 val nat_div_add_eq = @{thm "div_add1_eq"} RS sym;
 val int_div_add_eq = @{thm "zdiv_zadd1_eq"} RS sym;
-val ZDIVISION_BY_ZERO_MOD = @{thm "DIVISION_BY_ZERO"} RS conjunct2;
-val ZDIVISION_BY_ZERO_DIV = @{thm "DIVISION_BY_ZERO"} RS conjunct1;
 
 fun prepare_for_mir thy q fm = 
   let
@@ -96,8 +94,8 @@
     (* Some simpsets for dealing with mod div abs and nat*)
     val mod_div_simpset = HOL_basic_ss 
                         addsimps [refl, mod_add_eq, 
-                                  @{thm "mod_self"}, @{thm "zmod_self"},
-                                  @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"},
+                                  @{thm mod_self},
+                                  @{thm div_0}, @{thm mod_0},
                                   @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
                                   @{thm "Suc_eq_plus1"}]
                         addsimps @{thms add_ac}
diff -r 212f7a975d49 -r 9bfc32fc7ced src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue Mar 27 14:14:46 2012 +0200
+++ b/src/HOL/Divides.thy	Tue Mar 27 15:34:04 2012 +0200
@@ -535,7 +535,7 @@
   by (auto simp add: divmod_nat_def intro: theI elim: divmod_nat_rel_unique)
 qed
 
-lemma divmod_nat_eq:
+lemma divmod_nat_unique:
   assumes "divmod_nat_rel m n qr" 
   shows "divmod_nat m n = qr"
   using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
@@ -561,58 +561,36 @@
   "divmod_nat m n = (m div n, m mod n)"
   by (simp add: prod_eq_iff)
 
-lemma div_eq:
+lemma div_nat_unique:
   assumes "divmod_nat_rel m n (q, r)" 
   shows "m div n = q"
-  using assms by (auto dest!: divmod_nat_eq simp add: prod_eq_iff)
-
-lemma mod_eq:
+  using assms by (auto dest!: divmod_nat_unique simp add: prod_eq_iff)
+
+lemma mod_nat_unique:
   assumes "divmod_nat_rel m n (q, r)" 
   shows "m mod n = r"
-  using assms by (auto dest!: divmod_nat_eq simp add: prod_eq_iff)
+  using assms by (auto dest!: divmod_nat_unique simp add: prod_eq_iff)
 
 lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"
   using divmod_nat_rel_divmod_nat by (simp add: divmod_nat_div_mod)
 
-lemma divmod_nat_zero:
-  "divmod_nat m 0 = (0, m)"
-proof -
-  from divmod_nat_rel [of m 0] show ?thesis
-    unfolding divmod_nat_div_mod divmod_nat_rel_def by simp
-qed
-
-lemma divmod_nat_base:
-  assumes "m < n"
-  shows "divmod_nat m n = (0, m)"
-proof -
-  from divmod_nat_rel [of m n] show ?thesis
-    unfolding divmod_nat_div_mod divmod_nat_rel_def
-    using assms by (cases "m div n = 0")
-      (auto simp add: gr0_conv_Suc [of "m div n"])
-qed
+lemma divmod_nat_zero: "divmod_nat m 0 = (0, m)"
+  by (simp add: divmod_nat_unique divmod_nat_rel_def)
+
+lemma divmod_nat_zero_left: "divmod_nat 0 n = (0, 0)"
+  by (simp add: divmod_nat_unique divmod_nat_rel_def)
+
+lemma divmod_nat_base: "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
+  by (simp add: divmod_nat_unique divmod_nat_rel_def)
 
 lemma divmod_nat_step:
   assumes "0 < n" and "n \<le> m"
   shows "divmod_nat m n = (Suc ((m - n) div n), (m - n) mod n)"
-proof -
-  from divmod_nat_rel have divmod_nat_m_n: "divmod_nat_rel m n (m div n, m mod n)" .
-  with assms have m_div_n: "m div n \<ge> 1"
-    by (cases "m div n") (auto simp add: divmod_nat_rel_def)
-  have "divmod_nat_rel (m - n) n (m div n - Suc 0, m mod n)"
-  proof -
-    from assms have
-      "n \<noteq> 0"
-      "\<And>k. m = Suc k * n + m mod n ==> m - n = (Suc k - Suc 0) * n + m mod n"
-      by simp_all
-    then show ?thesis using assms divmod_nat_m_n 
-      by (cases "m div n")
-         (simp_all only: divmod_nat_rel_def fst_conv snd_conv, simp_all)
-  qed
-  with divmod_nat_eq have "divmod_nat (m - n) n = (m div n - Suc 0, m mod n)" by simp
-  moreover from divmod_nat_div_mod have "divmod_nat (m - n) n = ((m - n) div n, (m - n) mod n)" .
-  ultimately have "m div n = Suc ((m - n) div n)"
-    and "m mod n = (m - n) mod n" using m_div_n by simp_all
-  then show ?thesis using divmod_nat_div_mod by simp
+proof (rule divmod_nat_unique)
+  have "divmod_nat_rel (m - n) n ((m - n) div n, (m - n) mod n)"
+    by (rule divmod_nat_rel)
+  thus "divmod_nat_rel m n (Suc ((m - n) div n), (m - n) mod n)"
+    unfolding divmod_nat_rel_def using assms by auto
 qed
 
 text {* The ''recursion'' equations for @{const div} and @{const mod} *}
@@ -641,40 +619,30 @@
   shows "m mod n = (m - n) mod n"
   using assms divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
 
-instance proof -
-  have [simp]: "\<And>n::nat. n div 0 = 0"
+instance proof
+  fix m n :: nat
+  show "m div n * n + m mod n = m"
+    using divmod_nat_rel [of m n] by (simp add: divmod_nat_rel_def)
+next
+  fix m n q :: nat
+  assume "n \<noteq> 0"
+  then show "(q + m * n) div n = m + q div n"
+    by (induct m) (simp_all add: le_div_geq)
+next
+  fix m n q :: nat
+  assume "m \<noteq> 0"
+  hence "\<And>a b. divmod_nat_rel n q (a, b) \<Longrightarrow> divmod_nat_rel (m * n) (m * q) (a, m * b)"
+    unfolding divmod_nat_rel_def
+    by (auto split: split_if_asm, simp_all add: algebra_simps)
+  moreover from divmod_nat_rel have "divmod_nat_rel n q (n div q, n mod q)" .
+  ultimately have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))" .
+  thus "(m * n) div (m * q) = n div q" by (rule div_nat_unique)
+next
+  fix n :: nat show "n div 0 = 0"
     by (simp add: div_nat_def divmod_nat_zero)
-  have [simp]: "\<And>n::nat. 0 div n = 0"
-  proof -
-    fix n :: nat
-    show "0 div n = 0"
-      by (cases "n = 0") simp_all
-  qed
-  show "OFCLASS(nat, semiring_div_class)" proof
-    fix m n :: nat
-    show "m div n * n + m mod n = m"
-      using divmod_nat_rel [of m n] by (simp add: divmod_nat_rel_def)
-  next
-    fix m n q :: nat
-    assume "n \<noteq> 0"
-    then show "(q + m * n) div n = m + q div n"
-      by (induct m) (simp_all add: le_div_geq)
-  next
-    fix m n q :: nat
-    assume "m \<noteq> 0"
-    then show "(m * n) div (m * q) = n div q"
-    proof (cases "n \<noteq> 0 \<and> q \<noteq> 0")
-      case False then show ?thesis by auto
-    next
-      case True with `m \<noteq> 0`
-        have "m > 0" and "n > 0" and "q > 0" by auto
-      then have "\<And>a b. divmod_nat_rel n q (a, b) \<Longrightarrow> divmod_nat_rel (m * n) (m * q) (a, m * b)"
-        by (auto simp add: divmod_nat_rel_def) (simp_all add: algebra_simps)
-      moreover from divmod_nat_rel have "divmod_nat_rel n q (n div q, n mod q)" .
-      ultimately have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))" .
-      then show ?thesis by (simp add: div_eq)
-    qed
-  qed simp_all
+next
+  fix n :: nat show "0 div n = 0"
+    by (simp add: div_nat_def divmod_nat_zero_left)
 qed
 
 end
@@ -745,19 +713,14 @@
 by (induct m) (simp_all add: mod_geq)
 
 lemma mod_mult_distrib: "(m mod n) * (k\<Colon>nat) = (m * k) mod (n * k)"
-  apply (cases "n = 0", simp)
-  apply (cases "k = 0", simp)
-  apply (induct m rule: nat_less_induct)
-  apply (subst mod_if, simp)
-  apply (simp add: mod_geq diff_mult_distrib)
-  done
+  by (fact mod_mult_mult2 [symmetric]) (* FIXME: generalize *)
 
 lemma mod_mult_distrib2: "(k::nat) * (m mod n) = (k*m) mod (k*n)"
-by (simp add: mult_commute [of k] mod_mult_distrib)
+  by (fact mod_mult_mult1 [symmetric]) (* FIXME: generalize *)
 
 (* a simple rearrangement of mod_div_equality: *)
 lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
-by (cut_tac a = m and b = n in mod_div_equality2, arith)
+  using mod_div_equality2 [of n m] by arith
 
 lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"
   apply (drule mod_less_divisor [where m = m])
@@ -773,7 +736,7 @@
 
 lemma div_mult1_eq:
   "(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)"
-by (blast intro: divmod_nat_rel [THEN divmod_nat_rel_mult1_eq, THEN div_eq])
+by (blast intro: divmod_nat_rel_mult1_eq [THEN div_nat_unique] divmod_nat_rel)
 
 lemma divmod_nat_rel_add1_eq:
   "divmod_nat_rel a c (aq, ar) \<Longrightarrow> divmod_nat_rel b c (bq, br)
@@ -783,7 +746,7 @@
 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
 lemma div_add1_eq:
   "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
-by (blast intro: divmod_nat_rel_add1_eq [THEN div_eq] divmod_nat_rel)
+by (blast intro: divmod_nat_rel_add1_eq [THEN div_nat_unique] divmod_nat_rel)
 
 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)
@@ -798,10 +761,10 @@
 by (auto simp add: mult_ac divmod_nat_rel_def add_mult_distrib2 [symmetric] mod_lemma)
 
 lemma div_mult2_eq: "a div (b*c) = (a div b) div (c::nat)"
-by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_eq])
+by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_nat_unique])
 
 lemma mod_mult2_eq: "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)"
-by (auto simp add: mult_commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_eq])
+by (auto simp add: mult_commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_nat_unique])
 
 
 subsubsection {* Further Facts about Quotient and Remainder *}
@@ -850,9 +813,9 @@
 done
 
 (* Similar for "less than" *)
-lemma div_less_dividend [rule_format]:
-     "!!n::nat. 1<n ==> 0 < m --> m div n < m"
-apply (induct_tac m rule: nat_less_induct)
+lemma div_less_dividend [simp]:
+  "\<lbrakk>(1::nat) < n; 0 < m\<rbrakk> \<Longrightarrow> m div n < m"
+apply (induct m rule: nat_less_induct)
 apply (rename_tac "m")
 apply (case_tac "m<n", simp)
 apply (subgoal_tac "0<n")
@@ -865,8 +828,6 @@
   apply (simp_all)
 done
 
-declare div_less_dividend [simp]
-
 text{*A fact for the mutilated chess board*}
 lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
 apply (case_tac "n=0", simp)
@@ -995,23 +956,11 @@
 qed
 
 theorem mod_div_equality': "(m::nat) mod n = m - (m div n) * n"
-  apply (rule_tac P="%x. m mod n = x - (m div n) * n" in
-    subst [OF mod_div_equality [of _ n]])
-  apply arith
-  done
-
-lemma div_mod_equality':
-  fixes m n :: nat
-  shows "m div n * n = m - m mod n"
-proof -
-  have "m mod n \<le> m mod n" ..
-  from div_mod_equality have 
-    "m div n * n + m mod n - m mod n = m - m mod n" by simp
-  with diff_add_assoc [OF `m mod n \<le> m mod n`, of "m div n * n"] have
-    "m div n * n + (m mod n - m mod n) = m - m mod n"
-    by simp
-  then show ?thesis by simp
-qed
+  using mod_div_equality [of m n] by arith
+
+lemma div_mod_equality': "(m::nat) div n * n = m - m mod n"
+  using mod_div_equality [of m n] by arith
+(* FIXME: very similar to mult_div_cancel *)
 
 
 subsubsection {* An ``induction'' law for modulus arithmetic. *}
@@ -1103,17 +1052,14 @@
 qed
 
 lemma div2_Suc_Suc [simp]: "Suc (Suc m) div 2 = Suc (m div 2)"
-by (auto simp add: numeral_2_eq_2 le_div_geq)
+  by (simp add: numeral_2_eq_2 le_div_geq)
+
+lemma mod2_Suc_Suc [simp]: "Suc (Suc m) mod 2 = m mod 2"
+  by (simp add: numeral_2_eq_2 le_mod_geq)
 
 lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
 by (simp add: nat_mult_2 [symmetric])
 
-lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
-apply (subgoal_tac "m mod 2 < 2")
-apply (erule less_2_cases [THEN disjE])
-apply (simp_all (no_asm_simp) add: Let_def mod_Suc)
-done
-
 lemma mod2_gr_0 [simp]: "0 < (m\<Colon>nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
 proof -
   { fix n :: nat have  "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (cases n) simp_all }
@@ -1149,8 +1095,8 @@
 
 declare Suc_times_mod_eq [of "numeral w", simp] for w
 
-lemma [simp]: "n div k \<le> (Suc n) div k"
-by (simp add: div_le_mono) 
+lemma Suc_div_le_mono [simp]: "n div k \<le> (Suc n) div k"
+by (simp add: div_le_mono)
 
 lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2"
 by (cases n) simp_all
@@ -1187,8 +1133,8 @@
 
 definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" where
     --{*definition of quotient and remainder*}
-    "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
-               (if 0 < b then 0 \<le> r \<and> r < b else b < r \<and> r \<le> 0))"
+  "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
+    (if 0 < b then 0 \<le> r \<and> r < b else if b < 0 then b < r \<and> r \<le> 0 else q = 0))"
 
 definition adjust :: "int \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int" where
     --{*for the division algorithm*}
@@ -1386,42 +1332,87 @@
 subsubsection {* Existence Shown by Proving the Division Algorithm to be Correct *}
 
 (*the case a=0*)
-lemma divmod_int_rel_0: "b \<noteq> 0 ==> divmod_int_rel 0 b (0, 0)"
+lemma divmod_int_rel_0: "divmod_int_rel 0 b (0, 0)"
 by (auto simp add: divmod_int_rel_def linorder_neq_iff)
 
 lemma posDivAlg_0 [simp]: "posDivAlg 0 b = (0, 0)"
 by (subst posDivAlg.simps, auto)
 
+lemma posDivAlg_0_right [simp]: "posDivAlg a 0 = (0, a)"
+by (subst posDivAlg.simps, auto)
+
 lemma negDivAlg_minus1 [simp]: "negDivAlg -1 b = (-1, b - 1)"
 by (subst negDivAlg.simps, auto)
 
 lemma divmod_int_rel_neg: "divmod_int_rel (-a) (-b) qr ==> divmod_int_rel a b (apsnd uminus qr)"
-by (auto simp add: split_ifs divmod_int_rel_def)
-
-lemma divmod_int_correct: "b \<noteq> 0 ==> divmod_int_rel a b (divmod_int a b)"
+by (auto simp add: divmod_int_rel_def)
+
+lemma divmod_int_correct: "divmod_int_rel a b (divmod_int a b)"
+apply (cases "b = 0", simp add: divmod_int_def divmod_int_rel_def)
 by (force simp add: linorder_neq_iff divmod_int_rel_0 divmod_int_def divmod_int_rel_neg
                     posDivAlg_correct negDivAlg_correct)
 
-text{*Arbitrary definitions for division by zero.  Useful to simplify 
-    certain equations.*}
-
-lemma DIVISION_BY_ZERO [simp]: "a div (0::int) = 0 & a mod (0::int) = a"
-by (simp add: div_int_def mod_int_def divmod_int_def posDivAlg.simps)  
-
+lemma divmod_int_unique:
+  assumes "divmod_int_rel a b qr" 
+  shows "divmod_int a b = qr"
+  using assms divmod_int_correct [of a b]
+  using unique_quotient [of a b] unique_remainder [of a b]
+  by (metis pair_collapse)
+
+lemma divmod_int_rel_div_mod: "divmod_int_rel a b (a div b, a mod b)"
+  using divmod_int_correct by (simp add: divmod_int_mod_div)
+
+lemma div_int_unique: "divmod_int_rel a b (q, r) \<Longrightarrow> a div b = q"
+  by (simp add: divmod_int_rel_div_mod [THEN unique_quotient])
+
+lemma mod_int_unique: "divmod_int_rel a b (q, r) \<Longrightarrow> a mod b = r"
+  by (simp add: divmod_int_rel_div_mod [THEN unique_remainder])
+
+instance int :: ring_div
+proof
+  fix a b :: int
+  show "a div b * b + a mod b = a"
+    using divmod_int_rel_div_mod [of a b]
+    unfolding divmod_int_rel_def by (simp add: mult_commute)
+next
+  fix a b c :: int
+  assume "b \<noteq> 0"
+  hence "divmod_int_rel (a + c * b) b (c + a div b, a mod b)"
+    using divmod_int_rel_div_mod [of a b]
+    unfolding divmod_int_rel_def by (auto simp: algebra_simps)
+  thus "(a + c * b) div b = c + a div b"
+    by (rule div_int_unique)
+next
+  fix a b c :: int
+  assume "c \<noteq> 0"
+  hence "\<And>q r. divmod_int_rel a b (q, r)
+    \<Longrightarrow> divmod_int_rel (c * a) (c * b) (q, c * r)"
+    unfolding divmod_int_rel_def
+    by - (rule linorder_cases [of 0 b], auto simp: algebra_simps
+      mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
+      mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff)
+  hence "divmod_int_rel (c * a) (c * b) (a div b, c * (a mod b))"
+    using divmod_int_rel_div_mod [of a b] .
+  thus "(c * a) div (c * b) = a div b"
+    by (rule div_int_unique)
+next
+  fix a :: int show "a div 0 = 0"
+    by (rule div_int_unique, simp add: divmod_int_rel_def)
+next
+  fix a :: int show "0 div a = 0"
+    by (rule div_int_unique, auto simp add: divmod_int_rel_def)
+qed
 
 text{*Basic laws about division and remainder*}
 
 lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
-apply (case_tac "b = 0", simp)
-apply (cut_tac a = a and b = b in divmod_int_correct)
-apply (auto simp add: divmod_int_rel_def prod_eq_iff)
-done
+  by (fact mod_div_equality2 [symmetric])
 
 lemma zdiv_zmod_equality: "(b * (a div b) + (a mod b)) + k = (a::int)+k"
-by(simp add: zmod_zdiv_equality[symmetric])
+  by (fact div_mod_equality2)
 
 lemma zdiv_zmod_equality2: "((a div b) * b + (a mod b)) + k = (a::int)+k"
-by(simp add: mult_commute zmod_zdiv_equality[symmetric])
+  by (fact div_mod_equality)
 
 text {* Tool setup *}
 
@@ -1446,18 +1437,16 @@
 
 simproc_setup cancel_div_mod_int ("(k::int) + l") = {* K Cancel_Div_Mod_Int.proc *}
 
-lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b"
-apply (cut_tac a = a and b = b in divmod_int_correct)
-apply (auto simp add: divmod_int_rel_def prod_eq_iff)
-done
+lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
+  using divmod_int_correct [of a b]
+  by (auto simp add: divmod_int_rel_def prod_eq_iff)
 
 lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
    and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2]
 
-lemma neg_mod_conj : "b < (0::int) ==> a mod b \<le> 0 & b < a mod b"
-apply (cut_tac a = a and b = b in divmod_int_correct)
-apply (auto simp add: divmod_int_rel_def prod_eq_iff)
-done
+lemma neg_mod_conj: "b < (0::int) \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b"
+  using divmod_int_correct [of a b]
+  by (auto simp add: divmod_int_rel_def prod_eq_iff)
 
 lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
    and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
@@ -1465,50 +1454,35 @@
 
 subsubsection {* General Properties of div and mod *}
 
-lemma divmod_int_rel_div_mod: "b \<noteq> 0 ==> divmod_int_rel a b (a div b, a mod b)"
-apply (cut_tac a = a and b = b in zmod_zdiv_equality)
-apply (force simp add: divmod_int_rel_def linorder_neq_iff)
-done
-
-lemma divmod_int_rel_div: "[| divmod_int_rel a b (q, r) |] ==> a div b = q"
-apply (cases "b = 0")
-apply (simp add: divmod_int_rel_def)
-by (simp add: divmod_int_rel_div_mod [THEN unique_quotient])
-
-lemma divmod_int_rel_mod: "[| divmod_int_rel a b (q, r) |] ==> a mod b = r"
-apply (cases "b = 0")
-apply (simp add: divmod_int_rel_def)
-by (simp add: divmod_int_rel_div_mod [THEN unique_remainder])
-
 lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
-apply (rule divmod_int_rel_div)
+apply (rule div_int_unique)
 apply (auto simp add: divmod_int_rel_def)
 done
 
 lemma div_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a div b = 0"
-apply (rule divmod_int_rel_div)
+apply (rule div_int_unique)
 apply (auto simp add: divmod_int_rel_def)
 done
 
 lemma div_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a div b = -1"
-apply (rule divmod_int_rel_div)
+apply (rule div_int_unique)
 apply (auto simp add: divmod_int_rel_def)
 done
 
 (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)
 
 lemma mod_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a mod b = a"
-apply (rule_tac q = 0 in divmod_int_rel_mod)
+apply (rule_tac q = 0 in mod_int_unique)
 apply (auto simp add: divmod_int_rel_def)
 done
 
 lemma mod_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a mod b = a"
-apply (rule_tac q = 0 in divmod_int_rel_mod)
+apply (rule_tac q = 0 in mod_int_unique)
 apply (auto simp add: divmod_int_rel_def)
 done
 
 lemma mod_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a mod b = a+b"
-apply (rule_tac q = "-1" in divmod_int_rel_mod)
+apply (rule_tac q = "-1" in mod_int_unique)
 apply (auto simp add: divmod_int_rel_def)
 done
 
@@ -1517,24 +1491,17 @@
 
 (*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*)
 lemma zdiv_zminus_zminus [simp]: "(-a) div (-b) = a div (b::int)"
-apply (case_tac "b = 0", simp)
-apply (simp add: divmod_int_rel_div_mod [THEN divmod_int_rel_neg, simplified, 
-                                 THEN divmod_int_rel_div, THEN sym])
-
-done
+  using div_mult_mult1 [of "-1" a b] by simp (* FIXME: generalize *)
 
 (*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*)
 lemma zmod_zminus_zminus [simp]: "(-a) mod (-b) = - (a mod (b::int))"
-apply (case_tac "b = 0", simp)
-apply (subst divmod_int_rel_div_mod [THEN divmod_int_rel_neg, simplified, THEN divmod_int_rel_mod],
-       auto)
-done
+  using mod_mult_mult1 [of "-1" a b] by simp (* FIXME: generalize *)
 
 
 subsubsection {* Laws for div and mod with Unary Minus *}
 
 lemma zminus1_lemma:
-     "divmod_int_rel a b (q, r)
+     "divmod_int_rel a b (q, r) ==> b \<noteq> 0
       ==> divmod_int_rel (-a) b (if r=0 then -q else -q - 1,  
                           if r=0 then 0 else b-r)"
 by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_diff_distrib)
@@ -1544,12 +1511,12 @@
      "b \<noteq> (0::int)  
       ==> (-a) div b =  
           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
-by (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN divmod_int_rel_div])
+by (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN div_int_unique])
 
 lemma zmod_zminus1_eq_if:
      "(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))"
 apply (case_tac "b = 0", simp)
-apply (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN divmod_int_rel_mod])
+apply (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN mod_int_unique])
 done
 
 lemma zmod_zminus1_not_zero:
@@ -1558,10 +1525,10 @@
   unfolding zmod_zminus1_eq_if by auto
 
 lemma zdiv_zminus2: "a div (-b) = (-a::int) div b"
-by (cut_tac a = "-a" in zdiv_zminus_zminus, auto)
+  using zdiv_zminus_zminus [of "-a" b] by simp (* FIXME: generalize *)
 
 lemma zmod_zminus2: "a mod (-b) = - ((-a::int) mod b)"
-by (cut_tac a = "-a" and b = b in zmod_zminus_zminus, auto)
+  using zmod_zminus_zminus [of "-a" b] by simp (* FIXME: generalize*)
 
 lemma zdiv_zminus2_eq_if:
      "b \<noteq> (0::int)  
@@ -1579,53 +1546,11 @@
   unfolding zmod_zminus2_eq_if by auto 
 
 
-subsubsection {* Division of a Number by Itself *}
-
-lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 \<le> q"
-apply (subgoal_tac "0 < a*q")
- apply (simp add: zero_less_mult_iff, arith)
-done
-
-lemma self_quotient_aux2: "[| (0::int) < a; a = r + a*q; 0 \<le> r |] ==> q \<le> 1"
-apply (subgoal_tac "0 \<le> a* (1-q) ")
- apply (simp add: zero_le_mult_iff)
-apply (simp add: right_diff_distrib)
-done
-
-lemma self_quotient: "[| divmod_int_rel a a (q, r) |] ==> q = 1"
-apply (simp add: split_ifs divmod_int_rel_def linorder_neq_iff)
-apply (rule order_antisym, safe, simp_all)
-apply (rule_tac [3] a = "-a" and r = "-r" in self_quotient_aux1)
-apply (rule_tac a = "-a" and r = "-r" in self_quotient_aux2)
-apply (force intro: self_quotient_aux1 self_quotient_aux2 simp add: add_commute)+
-done
-
-lemma self_remainder: "[| divmod_int_rel a a (q, r) |] ==> r = 0"
-apply (frule self_quotient)
-apply (simp add: divmod_int_rel_def)
-done
-
-lemma zdiv_self [simp]: "a \<noteq> 0 ==> a div a = (1::int)"
-by (simp add: divmod_int_rel_div_mod [THEN self_quotient])
-
-(*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *)
-lemma zmod_self [simp]: "a mod a = (0::int)"
-apply (case_tac "a = 0", simp)
-apply (simp add: divmod_int_rel_div_mod [THEN self_remainder])
-done
-
-
 subsubsection {* Computation of Division and Remainder *}
 
-lemma zdiv_zero [simp]: "(0::int) div b = 0"
-by (simp add: div_int_def divmod_int_def)
-
 lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"
 by (simp add: div_int_def divmod_int_def)
 
-lemma zmod_zero [simp]: "(0::int) mod b = 0"
-by (simp add: mod_int_def divmod_int_def)
-
 lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
 by (simp add: mod_int_def divmod_int_def)
 
@@ -1668,18 +1593,18 @@
 text {*Simplify expresions in which div and mod combine numerical constants*}
 
 lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
-  by (rule divmod_int_rel_div [of a b q r]) (simp add: divmod_int_rel_def)
+  by (rule div_int_unique [of a b q r]) (simp add: divmod_int_rel_def)
 
 lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"
-  by (rule divmod_int_rel_div [of a b q r],
+  by (rule div_int_unique [of a b q r],
     simp add: divmod_int_rel_def)
 
 lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r"
-  by (rule divmod_int_rel_mod [of a b q r],
+  by (rule mod_int_unique [of a b q r],
     simp add: divmod_int_rel_def)
 
 lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"
-  by (rule divmod_int_rel_mod [of a b q r],
+  by (rule mod_int_unique [of a b q r],
     simp add: divmod_int_rel_def)
 
 (* simprocs adapted from HOL/ex/Binary.thy *)
@@ -1742,10 +1667,11 @@
 apply (cut_tac a = a and b = "-1" in neg_mod_sign)
 apply (cut_tac [2] a = a and b = "-1" in neg_mod_bound)
 apply (auto simp del: neg_mod_sign neg_mod_bound)
-done
+done (* FIXME: generalize *)
 
 lemma zdiv_minus1_right [simp]: "a div (-1::int) = -a"
 by (cut_tac a = a and b = "-1" in zmod_zdiv_equality, auto)
+(* FIXME: generalize *)
 
 (** The last remaining special cases for constant arithmetic:
     1 div z and 1 mod z **)
@@ -1863,18 +1789,11 @@
 
 lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
 apply (case_tac "c = 0", simp)
-apply (blast intro: divmod_int_rel_div_mod [THEN zmult1_lemma, THEN divmod_int_rel_div])
+apply (blast intro: divmod_int_rel_div_mod [THEN zmult1_lemma, THEN div_int_unique])
 done
 
 lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)"
-apply (case_tac "c = 0", simp)
-apply (blast intro: divmod_int_rel_div_mod [THEN zmult1_lemma, THEN divmod_int_rel_mod])
-done
-
-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
+  by (fact mod_mult_right_eq) (* FIXME: delete *)
 
 text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
 
@@ -1887,36 +1806,9 @@
 lemma zdiv_zadd1_eq:
      "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
 apply (case_tac "c = 0", simp)
-apply (blast intro: zadd1_lemma [OF divmod_int_rel_div_mod divmod_int_rel_div_mod] divmod_int_rel_div)
+apply (blast intro: zadd1_lemma [OF divmod_int_rel_div_mod divmod_int_rel_div_mod] div_int_unique)
 done
 
-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 zmod_zdiv_trivial zdiv_zmult1_eq)
-next
-  fix a b c :: int
-  assume "a \<noteq> 0"
-  then show "(a * b) div (a * c) = b div c"
-  proof (cases "b \<noteq> 0 \<and> c \<noteq> 0")
-    case False then show ?thesis by auto
-  next
-    case True then have "b \<noteq> 0" and "c \<noteq> 0" by auto
-    with `a \<noteq> 0`
-    have "\<And>q r. divmod_int_rel b c (q, r) \<Longrightarrow> divmod_int_rel (a * b) (a * c) (q, a * r)"
-      apply (auto simp add: divmod_int_rel_def) 
-      apply (auto simp add: algebra_simps)
-      apply (auto simp add: zero_less_mult_iff zero_le_mult_iff mult_le_0_iff mult_commute [of a] mult_less_cancel_right)
-      done
-    moreover with `c \<noteq> 0` divmod_int_rel_div_mod have "divmod_int_rel b c (b div c, b mod c)" by auto
-    ultimately have "divmod_int_rel (a * b) (a * c) (b div c, a * (b mod c))" .
-    from this show ?thesis by (rule divmod_int_rel_div)
-  qed
-qed auto
-
 lemma posDivAlg_div_mod:
   assumes "k \<ge> 0"
   and "l \<ge> 0"
@@ -1927,7 +1819,7 @@
   case False with assms posDivAlg_correct
     have "divmod_int_rel k l (fst (posDivAlg k l), snd (posDivAlg k l))"
     by simp
-  from divmod_int_rel_div [OF this] divmod_int_rel_mod [OF this]
+  from div_int_unique [OF this] mod_int_unique [OF this]
   show ?thesis by simp
 qed
 
@@ -1940,7 +1832,7 @@
   from assms negDivAlg_correct
     have "divmod_int_rel k l (fst (negDivAlg k l), snd (negDivAlg k l))"
     by simp
-  from divmod_int_rel_div [OF this] divmod_int_rel_mod [OF this]
+  from div_int_unique [OF this] mod_int_unique [OF this]
   show ?thesis by simp
 qed
 
@@ -1952,8 +1844,7 @@
 
 lemma zmod_zdiv_equality':
   "(m\<Colon>int) mod n = m - (m div n) * n"
-  by (rule_tac P="%x. m mod n = x - (m div n) * n" in subst [OF mod_div_equality [of _ n]])
-    arith
+  using mod_div_equality [of m n] by arith
 
 
 subsubsection {* Proving  @{term "a div (b*c) = (a div b) div c"} *}
@@ -2003,17 +1894,17 @@
       ==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"
 by (auto simp add: mult_ac divmod_int_rel_def linorder_neq_iff
                    zero_less_mult_iff right_distrib [symmetric] 
-                   zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4)
+                   zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: split_if_asm)
 
 lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c"
 apply (case_tac "b = 0", simp)
-apply (force simp add: divmod_int_rel_div_mod [THEN zmult2_lemma, THEN divmod_int_rel_div])
+apply (force simp add: divmod_int_rel_div_mod [THEN zmult2_lemma, THEN div_int_unique])
 done
 
 lemma zmod_zmult2_eq:
      "(0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b"
 apply (case_tac "b = 0", simp)
-apply (force simp add: divmod_int_rel_div_mod [THEN zmult2_lemma, THEN divmod_int_rel_mod])
+apply (force simp add: divmod_int_rel_div_mod [THEN zmult2_lemma, THEN mod_int_unique])
 done
 
 lemma div_pos_geq:
@@ -2295,14 +2186,14 @@
 
 lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
   using zmod_zdiv_equality[where a="m" and b="n"]
-  by (simp add: algebra_simps)
+  by (simp add: algebra_simps) (* FIXME: generalize *)
 
 lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
 apply (induct "y", auto)
-apply (rule zmod_zmult1_eq [THEN trans])
+apply (rule mod_mult_right_eq [THEN trans])
 apply (simp (no_asm_simp))
 apply (rule mod_mult_eq [symmetric])
-done
+done (* FIXME: generalize *)
 
 lemma zdiv_int: "int (a div b) = (int a) div (int b)"
 apply (subst split_div, auto)
@@ -2350,7 +2241,7 @@
 lemmas zmod_simps =
   mod_add_left_eq  [symmetric]
   mod_add_right_eq [symmetric]
-  zmod_zmult1_eq   [symmetric]
+  mod_mult_right_eq[symmetric]
   mod_mult_left_eq [symmetric]
   zpower_zmod
   zminus_zmod zdiff_zmod_left zdiff_zmod_right
diff -r 212f7a975d49 -r 9bfc32fc7ced src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Tue Mar 27 14:14:46 2012 +0200
+++ b/src/HOL/Groebner_Basis.thy	Tue Mar 27 15:34:04 2012 +0200
@@ -50,16 +50,16 @@
 declare dvd_eq_mod_eq_0[symmetric, algebra]
 declare mod_div_trivial[algebra]
 declare mod_mod_trivial[algebra]
-declare conjunct1[OF DIVISION_BY_ZERO, algebra]
-declare conjunct2[OF DIVISION_BY_ZERO, algebra]
+declare div_by_0[algebra]
+declare mod_by_0[algebra]
 declare zmod_zdiv_equality[symmetric,algebra]
 declare zdiv_zmod_equality[symmetric, algebra]
 declare zdiv_zminus_zminus[algebra]
 declare zmod_zminus_zminus[algebra]
 declare zdiv_zminus2[algebra]
 declare zmod_zminus2[algebra]
-declare zdiv_zero[algebra]
-declare zmod_zero[algebra]
+declare div_0[algebra]
+declare mod_0[algebra]
 declare mod_by_1[algebra]
 declare div_by_1[algebra]
 declare zmod_minus1_right[algebra]
diff -r 212f7a975d49 -r 9bfc32fc7ced src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Tue Mar 27 14:14:46 2012 +0200
+++ b/src/HOL/Presburger.thy	Tue Mar 27 15:34:04 2012 +0200
@@ -396,8 +396,6 @@
 declare mod_1[presburger] 
 declare mod_0[presburger]
 declare mod_by_1[presburger]
-declare zmod_zero[presburger]
-declare zmod_self[presburger]
 declare mod_self[presburger]
 declare mod_by_0[presburger]
 declare mod_div_trivial[presburger]
diff -r 212f7a975d49 -r 9bfc32fc7ced src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Tue Mar 27 14:14:46 2012 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Tue Mar 27 15:34:04 2012 +0200
@@ -802,9 +802,7 @@
     [@{thm "dvd_eq_mod_eq_0"},
      @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, 
      @{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
-  @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"}, 
-     @{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1, 
-     @{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"}, 
+  @ [@{thm "mod_self"}, @{thm "mod_by_0"}, @{thm "div_by_0"},
      @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, 
      @{thm "mod_1"}, @{thm "Suc_eq_plus1"}]
   @ @{thms add_ac}