--- 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:
--- 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
--- 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) }
--- 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
--- 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}]
--- 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
--- 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}
--- 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
--- 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]
--- 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]
--- 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}