--- a/NEWS Sat May 12 17:53:12 2018 +0200
+++ b/NEWS Sat May 12 22:20:46 2018 +0200
@@ -328,6 +328,15 @@
INCOMPATIBILITY.
+* Eliminated some theorem duplicate variations:
+ * dvd_eq_mod_eq_0_numeral can be replaced by dvd_eq_mod_eq_0.
+ * mod_Suc_eq_Suc_mod can be replaced by mod_Suc.
+ * mod_Suc_eq_Suc_mod [symmetrict] can be replaced by mod_simps.
+ * mod_eq_0_iff can be replaced by mod_eq_0_iff_dvd and dvd_def.
+ * The witness of mod_eqD can be given directly as "_ div _".
+
+INCOMPATIBILITY.
+
*** ML ***
--- a/src/HOL/Algebra/Multiplicative_Group.thy Sat May 12 17:53:12 2018 +0200
+++ b/src/HOL/Algebra/Multiplicative_Group.thy Sat May 12 22:20:46 2018 +0200
@@ -411,8 +411,9 @@
show "?R \<subseteq> ?L" by blast
{ fix y assume "y \<in> ?L"
then obtain x::nat where x:"y = a[^]x" by auto
- define r where "r = x mod ord a"
- then obtain q where q:"x = q * ord a + r" using mod_eqD by atomize_elim presburger
+ define r q where "r = x mod ord a" and "q = x div ord a"
+ then have "x = q * ord a + r"
+ by (simp add: div_mult_mod_eq)
hence "y = (a[^]ord a)[^]q \<otimes> a[^]r"
using x assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
hence "y = a[^]r" using assms by (simp add: pow_ord_eq_1)
@@ -428,7 +429,10 @@
shows "ord a dvd k"
proof -
define r where "r = k mod ord a"
- then obtain q where q:"k = q*ord a + r" using mod_eqD by atomize_elim presburger
+
+ define r q where "r = k mod ord a" and "q = k div ord a"
+ then have q: "k = q * ord a + r"
+ by (simp add: div_mult_mod_eq)
hence "a[^]k = (a[^]ord a)[^]q \<otimes> a[^]r"
using assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
hence "a[^]k = a[^]r" using assms by (simp add: pow_ord_eq_1)
--- a/src/HOL/Divides.thy Sat May 12 17:53:12 2018 +0200
+++ b/src/HOL/Divides.thy Sat May 12 22:20:46 2018 +0200
@@ -1286,19 +1286,11 @@
code_identifier
code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
-lemma dvd_eq_mod_eq_0_numeral:
- "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semidom_modulo)"
- by (fact dvd_eq_mod_eq_0)
-
declare minus_div_mult_eq_mod [symmetric, nitpick_unfold]
subsubsection \<open>Lemmas of doubtful value\<close>
-lemma mod_Suc_eq_Suc_mod:
- "Suc m mod n = Suc (m mod n) mod n"
- by (simp add: mod_simps)
-
lemma div_geq:
"m div n = Suc ((m - n) div n)" if "0 < n" and " \<not> m < n" for m n :: nat
by (rule le_div_geq) (use that in \<open>simp_all add: not_less\<close>)
@@ -1307,24 +1299,8 @@
"m mod n = (m - n) mod n" if "\<not> m < n" for m n :: nat
by (rule le_mod_geq) (use that in \<open>simp add: not_less\<close>)
-lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
- by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
-
-lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
-
-(*Loses information, namely we also have r<d provided d is nonzero*)
-lemma mod_eqD:
- fixes m d r q :: nat
- assumes "m mod d = r"
- shows "\<exists>q. m = r + q * d"
-proof -
- from div_mult_mod_eq obtain q where "q * d + m mod d = m" by blast
- with assms have "m = r + q * d" by simp
- then show ?thesis ..
-qed
-
-lemma is_unit_int:
- "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
- by auto
+lemma mod_eq_0D [dest!]:
+ "\<exists>q. m = d * q" if "m mod d = 0" for m d :: nat
+ using that by (auto simp add: mod_eq_0_iff_dvd elim: dvdE)
end
--- a/src/HOL/MacLaurin.thy Sat May 12 17:53:12 2018 +0200
+++ b/src/HOL/MacLaurin.thy Sat May 12 22:20:46 2018 +0200
@@ -526,31 +526,24 @@
proof -
have est: "x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y" for x y :: real
by (rule mult_right_mono) simp_all
- let ?diff = "\<lambda>(n::nat) x.
+ let ?diff = "\<lambda>(n::nat) (x::real).
if n mod 4 = 0 then sin x
else if n mod 4 = 1 then cos x
else if n mod 4 = 2 then - sin x
else - cos x"
have diff_0: "?diff 0 = sin" by simp
- have DERIV_diff: "\<forall>m x. DERIV (?diff m) x :> ?diff (Suc m) x"
- apply clarify
- apply (subst (1 2 3) mod_Suc_eq_Suc_mod)
- apply (cut_tac m=m in mod_exhaust_less_4)
- apply safe
- apply (auto intro!: derivative_eq_intros)
- done
+ have "DERIV (?diff m) x :> ?diff (Suc m) x" for m and x
+ using mod_exhaust_less_4 [of m]
+ by (auto simp add: mod_Suc intro!: derivative_eq_intros)
+ then have DERIV_diff: "\<forall>m x. DERIV (?diff m) x :> ?diff (Suc m) x"
+ by blast
from Maclaurin_all_le [OF diff_0 DERIV_diff]
obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>"
and t2: "sin x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) + ?diff n t / (fact n) * x ^ n"
by fast
- have diff_m_0: "\<And>m. ?diff m 0 = (if even m then 0 else (- 1) ^ ((m - Suc 0) div 2))"
- apply (subst even_even_mod_4_iff)
- apply (cut_tac m=m in mod_exhaust_less_4)
- apply (elim disjE)
- apply simp_all
- apply (safe dest!: mod_eqD)
- apply simp_all
- done
+ have diff_m_0: "?diff m 0 = (if even m then 0 else (- 1) ^ ((m - Suc 0) div 2))" for m
+ using mod_exhaust_less_4 [of m]
+ by (auto simp add: minus_one_power_iff even_even_mod_4_iff [of m] dest: even_mod_4_div_2 odd_mod_4_div_2)
show ?thesis
unfolding sin_coeff_def
apply (subst t2)
--- a/src/HOL/Number_Theory/Pocklington.thy Sat May 12 17:53:12 2018 +0200
+++ b/src/HOL/Number_Theory/Pocklington.thy Sat May 12 22:20:46 2018 +0200
@@ -838,7 +838,7 @@
{
assume "a ^ ((n - 1) div p) mod n = 0"
then obtain s where s: "a ^ ((n - 1) div p) = n * s"
- unfolding mod_eq_0_iff by blast
+ by blast
then have eq0: "(a^((n - 1) div p))^p = (n*s)^p" by simp
from qrn[symmetric] have qn1: "q dvd n - 1"
by (auto simp: dvd_def)
--- a/src/HOL/Parity.thy Sat May 12 17:53:12 2018 +0200
+++ b/src/HOL/Parity.thy Sat May 12 22:20:46 2018 +0200
@@ -542,6 +542,10 @@
qed
qed
+lemma not_mod2_eq_Suc_0_eq_0 [simp]:
+ "n mod 2 \<noteq> Suc 0 \<longleftrightarrow> n mod 2 = 0"
+ using not_mod_2_eq_1_eq_0 [of n] by simp
+
subsection \<open>Parity and powers\<close>
--- a/src/HOL/Presburger.thy Sat May 12 17:53:12 2018 +0200
+++ b/src/HOL/Presburger.thy Sat May 12 22:20:46 2018 +0200
@@ -495,11 +495,11 @@
by presburger
lemma odd_mod_4_div_2:
- "n mod 4 = (3::nat) \<Longrightarrow> odd ((n - 1) div 2)"
+ "n mod 4 = (3::nat) \<Longrightarrow> odd ((n - Suc 0) div 2)"
by presburger
lemma even_mod_4_div_2:
- "n mod 4 = (1::nat) \<Longrightarrow> even ((n - 1) div 2)"
+ "n mod 4 = Suc 0 \<Longrightarrow> even ((n - Suc 0) div 2)"
by presburger
--- a/src/HOL/Word/Word.thy Sat May 12 17:53:12 2018 +0200
+++ b/src/HOL/Word/Word.thy Sat May 12 22:20:46 2018 +0200
@@ -1750,13 +1750,8 @@
lemma of_nat_eq: "of_nat n = w \<longleftrightarrow> (\<exists>q. n = unat w + q * 2 ^ len_of TYPE('a))"
for w :: "'a::len word"
- apply (rule trans)
- apply (rule word_unat.inverse_norm)
- apply (rule iffI)
- apply (rule mod_eqD)
- apply simp
- apply clarsimp
- done
+ using mod_div_mult_eq [of n "2 ^ LENGTH('a)", symmetric]
+ by (auto simp add: word_unat.inverse_norm)
lemma of_nat_eq_size: "of_nat n = w \<longleftrightarrow> (\<exists>q. n = unat w + q * 2 ^ size w)"
unfolding word_size by (rule of_nat_eq)
--- a/src/HOL/Word/Word_Miscellaneous.thy Sat May 12 17:53:12 2018 +0200
+++ b/src/HOL/Word/Word_Miscellaneous.thy Sat May 12 22:20:46 2018 +0200
@@ -275,7 +275,7 @@
lemma mod_power_lem: "a > 1 \<Longrightarrow> a ^ n mod a ^ m = (if m \<le> n then 0 else a ^ n)"
for a :: int
- by (simp add: mod_eq_0_iff le_imp_power_dvd)
+ by (simp add: mod_eq_0_iff_dvd le_imp_power_dvd)
lemma pl_pl_rels: "a + b = c + d \<Longrightarrow> a \<ge> c \<and> b \<le> d \<or> a \<le> c \<and> b \<ge> d"
for a b c d :: nat