# HG changeset patch
# User huffman
# Date 1332852596 -7200
# Node ID d64fa2ca54b8fda6e69ee35483018c103b0ae02a
# Parent  02d6b816e4b30d94d70aa6ed0594e6cc7f894449
remove redundant lemmas

diff -r 02d6b816e4b3 -r d64fa2ca54b8 NEWS
--- a/NEWS	Tue Mar 27 12:42:54 2012 +0200
+++ b/NEWS	Tue Mar 27 14:49:56 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 02d6b816e4b3 -r d64fa2ca54b8 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Tue Mar 27 12:42:54 2012 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Tue Mar 27 14:49:56 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 02d6b816e4b3 -r d64fa2ca54b8 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Tue Mar 27 12:42:54 2012 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Tue Mar 27 14:49:56 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 02d6b816e4b3 -r d64fa2ca54b8 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Tue Mar 27 12:42:54 2012 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Tue Mar 27 14:49:56 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 02d6b816e4b3 -r d64fa2ca54b8 src/HOL/Decision_Procs/cooper_tac.ML
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Tue Mar 27 12:42:54 2012 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Tue Mar 27 14:49:56 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 02d6b816e4b3 -r d64fa2ca54b8 src/HOL/Decision_Procs/ferrack_tac.ML
--- a/src/HOL/Decision_Procs/ferrack_tac.ML	Tue Mar 27 12:42:54 2012 +0200
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Tue Mar 27 14:49:56 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 02d6b816e4b3 -r d64fa2ca54b8 src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Tue Mar 27 12:42:54 2012 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Tue Mar 27 14:49:56 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 02d6b816e4b3 -r d64fa2ca54b8 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue Mar 27 12:42:54 2012 +0200
+++ b/src/HOL/Divides.thy	Tue Mar 27 14:49:56 2012 +0200
@@ -1403,12 +1403,6 @@
     by (rule div_int_unique, auto simp add: divmod_int_rel_def)
 qed
 
-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 (* FIXME: delete *)
-
 text{*Basic laws about division and remainder*}
 
 lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
@@ -1552,51 +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); a \<noteq> 0 |] ==> 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); a \<noteq> 0 |] ==> r = 0"
-apply (frule (1) self_quotient)
-apply (simp add: divmod_int_rel_def)
-done
-
-lemma zdiv_self [simp]: "a \<noteq> 0 ==> a div a = (1::int)"
-  by (fact div_self) (* FIXME: delete *)
-
-(*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)"
-  by (fact mod_self) (* FIXME: delete *)
-
-
 subsubsection {* Computation of Division and Remainder *}
 
-lemma zdiv_zero [simp]: "(0::int) div b = 0"
-  by (fact div_0) (* FIXME: delete *)
-
 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 (fact mod_0) (* FIXME: delete *)
-
 lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
 by (simp add: mod_int_def divmod_int_def)
 
@@ -1841,9 +1795,6 @@
 lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)"
   by (fact mod_mult_right_eq) (* FIXME: delete *)
 
-lemma zmod_zdiv_trivial: "(a mod b) div b = (0::int)"
-  by (fact mod_div_trivial) (* FIXME: delete *)
-
 text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
 
 lemma zadd1_lemma:
@@ -2235,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)
@@ -2290,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 02d6b816e4b3 -r d64fa2ca54b8 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Tue Mar 27 12:42:54 2012 +0200
+++ b/src/HOL/Groebner_Basis.thy	Tue Mar 27 14:49:56 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 02d6b816e4b3 -r d64fa2ca54b8 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Tue Mar 27 12:42:54 2012 +0200
+++ b/src/HOL/Presburger.thy	Tue Mar 27 14:49:56 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 02d6b816e4b3 -r d64fa2ca54b8 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Tue Mar 27 12:42:54 2012 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Tue Mar 27 14:49:56 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}