--- a/NEWS Tue Mar 03 12:14:52 2009 +1100
+++ b/NEWS Tue Mar 03 17:05:18 2009 +0100
@@ -376,12 +376,16 @@
mult_div ~> div_mult_self2_is_id
mult_mod ~> mod_mult_self2_is_0
-* HOL/IntDiv: removed most (all?) lemmas that are instances of class-based
+* HOL/IntDiv: removed many lemmas that are instances of class-based
generalizations (from Divides and Ring_and_Field).
INCOMPATIBILITY. Rename old lemmas as follows:
dvd_diff -> nat_dvd_diff
dvd_zminus_iff -> dvd_minus_iff
+mod_add1_eq -> mod_add_eq
+mod_mult1_eq -> mod_mult_right_eq
+mod_mult1_eq' -> mod_mult_left_eq
+mod_mult_distrib_mod -> mod_mult_eq
nat_mod_add_left_eq -> mod_add_left_eq
nat_mod_add_right_eq -> mod_add_right_eq
nat_mod_div_trivial -> mod_div_trivial
@@ -398,7 +402,7 @@
zmod_zadd_right_eq -> mod_add_right_eq
zmod_zadd_self1 -> mod_add_self1
zmod_zadd_self2 -> mod_add_self2
-zmod_zadd1_eq -> mod_add1_eq
+zmod_zadd1_eq -> mod_add_eq
zmod_zdiff1_eq -> mod_diff_eq
zmod_zdvd_zmod -> mod_mod_cancel
zmod_zmod_cancel -> mod_mod_cancel
--- a/doc-src/TutorialI/Types/Numbers.thy Tue Mar 03 12:14:52 2009 +1100
+++ b/doc-src/TutorialI/Types/Numbers.thy Tue Mar 03 17:05:18 2009 +0100
@@ -100,8 +100,8 @@
@{thm[display] div_mult1_eq[no_vars]}
\rulename{div_mult1_eq}
-@{thm[display] mod_mult1_eq[no_vars]}
-\rulename{mod_mult1_eq}
+@{thm[display] mod_mult_right_eq[no_vars]}
+\rulename{mod_mult_right_eq}
@{thm[display] div_mult2_eq[no_vars]}
\rulename{div_mult2_eq}
@@ -147,8 +147,8 @@
@{thm[display] zdiv_zadd1_eq[no_vars]}
\rulename{zdiv_zadd1_eq}
-@{thm[display] mod_add1_eq[no_vars]}
-\rulename{mod_add1_eq}
+@{thm[display] mod_add_eq[no_vars]}
+\rulename{mod_add_eq}
@{thm[display] zdiv_zmult1_eq[no_vars]}
\rulename{zdiv_zmult1_eq}
--- a/doc-src/TutorialI/Types/document/Numbers.tex Tue Mar 03 12:14:52 2009 +1100
+++ b/doc-src/TutorialI/Types/document/Numbers.tex Tue Mar 03 17:05:18 2009 +0100
@@ -244,7 +244,7 @@
\begin{isabelle}%
a\ {\isacharasterisk}\ b\ mod\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ mod\ c%
\end{isabelle}
-\rulename{mod_mult1_eq}
+\rulename{mod_mult_right_eq}
\begin{isabelle}%
a\ div\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ a\ div\ b\ div\ c%
@@ -318,7 +318,7 @@
\begin{isabelle}%
{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ mod\ c\ {\isacharequal}\ {\isacharparenleft}a\ mod\ c\ {\isacharplus}\ b\ mod\ c{\isacharparenright}\ mod\ c%
\end{isabelle}
-\rulename{mod_add1_eq}
+\rulename{mod_add_eq}
\begin{isabelle}%
a\ {\isacharasterisk}\ b\ div\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ div\ c{\isacharparenright}\ {\isacharplus}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ div\ c%
--- a/doc-src/TutorialI/Types/numerics.tex Tue Mar 03 12:14:52 2009 +1100
+++ b/doc-src/TutorialI/Types/numerics.tex Tue Mar 03 17:05:18 2009 +0100
@@ -154,7 +154,7 @@
a\ *\ b\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%
\rulename{div_mult1_eq}\isanewline
a\ *\ b\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%
-\rulename{mod_mult1_eq}\isanewline
+\rulename{mod_mult_right_eq}\isanewline
a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
\rulename{div_mult2_eq}\isanewline
a\ mod\ (b*c)\ =\ b * (a\ div\ b\ mod\ c)\ +\ a\ mod\ b%
@@ -276,7 +276,7 @@
\rulename{zdiv_zadd1_eq}
\par\smallskip
(a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c%
-\rulename{mod_add1_eq}
+\rulename{mod_add_eq}
\end{isabelle}
\begin{isabelle}
--- a/src/HOL/Decision_Procs/cooper_tac.ML Tue Mar 03 12:14:52 2009 +1100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Tue Mar 03 17:05:18 2009 +0100
@@ -27,10 +27,9 @@
val Suc_plus1 = @{thm Suc_plus1};
val imp_le_cong = @{thm imp_le_cong};
val conj_le_cong = @{thm conj_le_cong};
-val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
val mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
-val int_mod_add_eq = @{thm mod_add_eq} RS sym;
+val mod_add_eq = @{thm mod_add_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;
@@ -68,8 +67,8 @@
val (t,np,nh) = prepare_for_linz q g
(* Some simpsets for dealing with mod div abs and nat*)
val mod_div_simpset = HOL_basic_ss
- addsimps [refl,nat_mod_add_eq, mod_add_left_eq,
- mod_add_right_eq, int_mod_add_eq,
+ 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},
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Tue Mar 03 12:14:52 2009 +1100
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Tue Mar 03 17:05:18 2009 +0100
@@ -31,10 +31,8 @@
val Suc_plus1 = @{thm Suc_plus1};
val imp_le_cong = @{thm imp_le_cong};
val conj_le_cong = @{thm conj_le_cong};
-val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
val mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
-val int_mod_add_eq = @{thm mod_add_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;
--- a/src/HOL/Decision_Procs/mir_tac.ML Tue Mar 03 12:14:52 2009 +1100
+++ b/src/HOL/Decision_Procs/mir_tac.ML Tue Mar 03 17:05:18 2009 +0100
@@ -46,10 +46,9 @@
val Suc_plus1 = @{thm "Suc_plus1"};
val imp_le_cong = @{thm "imp_le_cong"};
val conj_le_cong = @{thm "conj_le_cong"};
-val nat_mod_add_eq = @{thm "mod_add1_eq"} RS sym;
+val mod_add_eq = @{thm "mod_add_eq"} RS sym;
val mod_add_left_eq = @{thm "mod_add_left_eq"} RS sym;
val mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym;
-val int_mod_add_eq = @{thm "mod_add_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;
@@ -94,7 +93,7 @@
val (t,np,nh) = prepare_for_mir thy q g
(* Some simpsets for dealing with mod div abs and nat*)
val mod_div_simpset = HOL_basic_ss
- addsimps [refl,nat_mod_add_eq,
+ addsimps [refl, mod_add_eq,
@{thm "mod_self"}, @{thm "zmod_self"},
@{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"},
--- a/src/HOL/Divides.thy Tue Mar 03 12:14:52 2009 +1100
+++ b/src/HOL/Divides.thy Tue Mar 03 17:05:18 2009 +0100
@@ -684,16 +684,6 @@
apply (blast intro: divmod_rel [THEN divmod_rel_mult1_eq, THEN div_eq])
done
-lemma mod_mult1_eq: "(a*b) mod c = a*(b mod c) mod (c::nat)"
-by (rule mod_mult_right_eq)
-
-lemma mod_mult1_eq': "(a*b) mod (c::nat) = ((a mod c) * b) mod c"
-by (rule mod_mult_left_eq)
-
-lemma mod_mult_distrib_mod:
- "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c"
-by (rule mod_mult_eq)
-
lemma divmod_rel_add1_eq:
"[| divmod_rel a c aq ar; divmod_rel b c bq br; c > 0 |]
==> divmod_rel (a + b) c (aq + bq + (ar+br) div c) ((ar + br) mod c)"
@@ -706,9 +696,6 @@
apply (blast intro: divmod_rel_add1_eq [THEN div_eq] divmod_rel)
done
-lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"
-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)
apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
--- a/src/HOL/Library/Char_nat.thy Tue Mar 03 12:14:52 2009 +1100
+++ b/src/HOL/Library/Char_nat.thy Tue Mar 03 17:05:18 2009 +0100
@@ -132,7 +132,7 @@
lemma Char_char_of_nat:
"Char n m = char_of_nat (nat_of_nibble n * 16 + nat_of_nibble m)"
unfolding char_of_nat_def Let_def nibble_pair_of_nat_def
- by (auto simp add: div_add1_eq mod_add1_eq nat_of_nibble_div_16 nibble_of_nat_norm nibble_of_nat_of_nibble)
+ by (auto simp add: div_add1_eq mod_add_eq nat_of_nibble_div_16 nibble_of_nat_norm nibble_of_nat_of_nibble)
lemma char_of_nat_of_char:
"char_of_nat (nat_of_char c) = c"
@@ -165,7 +165,7 @@
show ?thesis
by (simp add: nat_of_char.simps char_of_nat_def nibble_of_pair
nat_of_nibble_of_nat mod_mult_distrib
- n aux3 mod_mult_self3 l_256 aux4 mod_add1_eq [of "256 * k"] l_div_256)
+ n aux3 mod_mult_self3 l_256 aux4 mod_add_eq [of "256 * k"] l_div_256)
qed
lemma nibble_pair_of_nat_char:
--- a/src/HOL/Library/Pocklington.thy Tue Mar 03 12:14:52 2009 +1100
+++ b/src/HOL/Library/Pocklington.thy Tue Mar 03 17:05:18 2009 +0100
@@ -142,10 +142,10 @@
shows "[x * y = x' * y'] (mod n)"
proof-
have "(x * y) mod n = (x mod n) * (y mod n) mod n"
- by (simp add: mod_mult1_eq'[of x y n] mod_mult1_eq[of "x mod n" y n])
+ by (simp add: mod_mult_left_eq[of x y n] mod_mult_right_eq[of "x mod n" y n])
also have "\<dots> = (x' mod n) * (y' mod n) mod n" using xx'[unfolded modeq_def] yy'[unfolded modeq_def] by simp
also have "\<dots> = (x' * y') mod n"
- by (simp add: mod_mult1_eq'[of x' y' n] mod_mult1_eq[of "x' mod n" y' n])
+ by (simp add: mod_mult_left_eq[of x' y' n] mod_mult_right_eq[of "x' mod n" y' n])
finally show ?thesis unfolding modeq_def .
qed
@@ -296,7 +296,7 @@
from cong_solve[OF an] obtain x where x: "[a*x = b] (mod n)" by blast
let ?x = "x mod n"
from x have th: "[a * ?x = b] (mod n)"
- by (simp add: modeq_def mod_mult1_eq[of a x n])
+ by (simp add: modeq_def mod_mult_right_eq[of a x n])
from mod_less_divisor[ of n x] nz th have Px: "?P ?x" by simp
{fix y assume Py: "y < n" "[a * y = b] (mod n)"
from Py(2) th have "[a * y = a*?x] (mod n)" by (simp add: modeq_def)
@@ -753,10 +753,10 @@
next
case (Suc n)
have "(x mod m)^(Suc n) mod m = ((x mod m) * (((x mod m) ^ n) mod m)) mod m"
- by (simp add: mod_mult1_eq[symmetric])
+ by (simp add: mod_mult_right_eq[symmetric])
also have "\<dots> = ((x mod m) * (x^n mod m)) mod m" using Suc.hyps by simp
also have "\<dots> = x^(Suc n) mod m"
- by (simp add: mod_mult1_eq'[symmetric] mod_mult1_eq[symmetric])
+ by (simp add: mod_mult_left_eq[symmetric] mod_mult_right_eq[symmetric])
finally show ?case .
qed
@@ -891,9 +891,9 @@
hence "[(a^?o)^?q * (a^?r) = 1] (mod n)"
by (simp add: modeq_def power_mult[symmetric] power_add[symmetric])
hence th: "[a^?r = 1] (mod n)"
- using eqo mod_mult1_eq'[of "(a^?o)^?q" "a^?r" n]
+ using eqo mod_mult_left_eq[of "(a^?o)^?q" "a^?r" n]
apply (simp add: modeq_def del: One_nat_def)
- by (simp add: mod_mult1_eq'[symmetric])
+ by (simp add: mod_mult_left_eq[symmetric])
{assume r: "?r = 0" hence ?rhs by (simp add: dvd_eq_mod_eq_0)}
moreover
{assume r: "?r \<noteq> 0"
--- a/src/HOL/Library/Word.thy Tue Mar 03 12:14:52 2009 +1100
+++ b/src/HOL/Library/Word.thy Tue Mar 03 17:05:18 2009 +0100
@@ -575,7 +575,7 @@
have "?lhs = (1 + 2 * bv_to_nat w) mod 2"
by (simp add: add_commute)
also have "... = 1"
- by (subst mod_add1_eq) simp
+ by (subst mod_add_eq) simp
finally have eq1: "?lhs = 1" .
have "?rhs = 0" by simp
with orig and eq1
--- a/src/HOL/Tools/Qelim/presburger.ML Tue Mar 03 12:14:52 2009 +1100
+++ b/src/HOL/Tools/Qelim/presburger.ML Tue Mar 03 17:05:18 2009 +0100
@@ -122,7 +122,7 @@
addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
val div_mod_ss = HOL_basic_ss addsimps simp_thms
@ map (symmetric o mk_meta_eq)
- [@{thm "dvd_eq_mod_eq_0"}, @{thm "mod_add1_eq"},
+ [@{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"},