# HG changeset patch # User haftmann # Date 1526156446 -7200 # Node ID 057d5b4ce47e60a415e748106fcd1e8698d060aa # Parent 7da3af31ca4db708185e0fa2800d535c945c08dc removed some non-essential rules diff -r 7da3af31ca4d -r 057d5b4ce47e NEWS --- 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 *** diff -r 7da3af31ca4d -r 057d5b4ce47e src/HOL/Algebra/Multiplicative_Group.thy --- 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 \ ?L" by blast { fix y assume "y \ ?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 \ 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 \ 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) diff -r 7da3af31ca4d -r 057d5b4ce47e src/HOL/Divides.thy --- 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 \ (SML) Arith and (OCaml) Arith and (Haskell) Arith -lemma dvd_eq_mod_eq_0_numeral: - "numeral x dvd (numeral y :: 'a) \ 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 \Lemmas of doubtful value\ -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 " \ m < n" for m n :: nat by (rule le_div_geq) (use that in \simp_all add: not_less\) @@ -1307,24 +1299,8 @@ "m mod n = (m - n) mod n" if "\ m < n" for m n :: nat by (rule le_mod_geq) (use that in \simp add: not_less\) -lemma mod_eq_0_iff: "(m mod d = 0) = (\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 rq. 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) \ k = 1 \ k = - 1" - by auto +lemma mod_eq_0D [dest!]: + "\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 diff -r 7da3af31ca4d -r 057d5b4ce47e src/HOL/MacLaurin.thy --- 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 \ 1 \ 0 \ y \ x * y \ 1 * y" for x y :: real by (rule mult_right_mono) simp_all - let ?diff = "\(n::nat) x. + let ?diff = "\(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: "\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: "\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: "\t\ \ \x\" and t2: "sin x = (\mm. ?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) diff -r 7da3af31ca4d -r 057d5b4ce47e src/HOL/Number_Theory/Pocklington.thy --- 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) diff -r 7da3af31ca4d -r 057d5b4ce47e src/HOL/Parity.thy --- 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 \ Suc 0 \ n mod 2 = 0" + using not_mod_2_eq_1_eq_0 [of n] by simp + subsection \Parity and powers\ diff -r 7da3af31ca4d -r 057d5b4ce47e src/HOL/Presburger.thy --- 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) \ odd ((n - 1) div 2)" + "n mod 4 = (3::nat) \ odd ((n - Suc 0) div 2)" by presburger lemma even_mod_4_div_2: - "n mod 4 = (1::nat) \ even ((n - 1) div 2)" + "n mod 4 = Suc 0 \ even ((n - Suc 0) div 2)" by presburger diff -r 7da3af31ca4d -r 057d5b4ce47e src/HOL/Word/Word.thy --- 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 \ (\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 \ (\q. n = unat w + q * 2 ^ size w)" unfolding word_size by (rule of_nat_eq) diff -r 7da3af31ca4d -r 057d5b4ce47e src/HOL/Word/Word_Miscellaneous.thy --- 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 \ a ^ n mod a ^ m = (if m \ 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 \ a \ c \ b \ d \ a \ c \ b \ d" for a b c d :: nat