removed some non-essential rules
authorhaftmann
Sat May 12 22:20:46 2018 +0200 (12 months ago)
changeset 68157057d5b4ce47e
parent 68156 7da3af31ca4d
child 68158 b00f0f990bc5
removed some non-essential rules
NEWS
src/HOL/Algebra/Multiplicative_Group.thy
src/HOL/Divides.thy
src/HOL/MacLaurin.thy
src/HOL/Number_Theory/Pocklington.thy
src/HOL/Parity.thy
src/HOL/Presburger.thy
src/HOL/Word/Word.thy
src/HOL/Word/Word_Miscellaneous.thy
     1.1 --- a/NEWS	Sat May 12 17:53:12 2018 +0200
     1.2 +++ b/NEWS	Sat May 12 22:20:46 2018 +0200
     1.3 @@ -328,6 +328,15 @@
     1.4  
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Eliminated some theorem duplicate variations:
     1.8 +  * dvd_eq_mod_eq_0_numeral can be replaced by dvd_eq_mod_eq_0.
     1.9 +  * mod_Suc_eq_Suc_mod can be replaced by mod_Suc.
    1.10 +  * mod_Suc_eq_Suc_mod [symmetrict] can be replaced by mod_simps.
    1.11 +  * mod_eq_0_iff can be replaced by mod_eq_0_iff_dvd and dvd_def.
    1.12 +  * The witness of mod_eqD can be given directly as "_ div _".
    1.13 +
    1.14 +INCOMPATIBILITY.
    1.15 +
    1.16  
    1.17  *** ML ***
    1.18  
     2.1 --- a/src/HOL/Algebra/Multiplicative_Group.thy	Sat May 12 17:53:12 2018 +0200
     2.2 +++ b/src/HOL/Algebra/Multiplicative_Group.thy	Sat May 12 22:20:46 2018 +0200
     2.3 @@ -411,8 +411,9 @@
     2.4    show "?R \<subseteq> ?L" by blast
     2.5    { fix y assume "y \<in> ?L"
     2.6      then obtain x::nat where x:"y = a[^]x" by auto
     2.7 -    define r where "r = x mod ord a"
     2.8 -    then obtain q where q:"x = q * ord a + r" using mod_eqD by atomize_elim presburger
     2.9 +    define r q where "r = x mod ord a" and "q = x div ord a"
    2.10 +    then have "x = q * ord a + r"
    2.11 +      by (simp add: div_mult_mod_eq)
    2.12      hence "y = (a[^]ord a)[^]q \<otimes> a[^]r"
    2.13        using x assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
    2.14      hence "y = a[^]r" using assms by (simp add: pow_ord_eq_1)
    2.15 @@ -428,7 +429,10 @@
    2.16    shows "ord a dvd k"
    2.17  proof -
    2.18    define r where "r = k mod ord a"
    2.19 -  then obtain q where q:"k = q*ord a + r" using mod_eqD by atomize_elim presburger
    2.20 +
    2.21 +  define r q where "r = k mod ord a" and "q = k div ord a"
    2.22 +  then have q: "k = q * ord a + r"
    2.23 +    by (simp add: div_mult_mod_eq)
    2.24    hence "a[^]k = (a[^]ord a)[^]q \<otimes> a[^]r"
    2.25        using assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
    2.26    hence "a[^]k = a[^]r" using assms by (simp add: pow_ord_eq_1)
     3.1 --- a/src/HOL/Divides.thy	Sat May 12 17:53:12 2018 +0200
     3.2 +++ b/src/HOL/Divides.thy	Sat May 12 22:20:46 2018 +0200
     3.3 @@ -1286,19 +1286,11 @@
     3.4  code_identifier
     3.5    code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
     3.6  
     3.7 -lemma dvd_eq_mod_eq_0_numeral:
     3.8 -  "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semidom_modulo)"
     3.9 -  by (fact dvd_eq_mod_eq_0)
    3.10 -
    3.11  declare minus_div_mult_eq_mod [symmetric, nitpick_unfold]
    3.12  
    3.13  
    3.14  subsubsection \<open>Lemmas of doubtful value\<close>
    3.15  
    3.16 -lemma mod_Suc_eq_Suc_mod:
    3.17 -  "Suc m mod n = Suc (m mod n) mod n"
    3.18 -  by (simp add: mod_simps)
    3.19 -
    3.20  lemma div_geq:
    3.21    "m div n = Suc ((m - n) div n)" if "0 < n" and " \<not> m < n" for m n :: nat
    3.22    by (rule le_div_geq) (use that in \<open>simp_all add: not_less\<close>)
    3.23 @@ -1307,24 +1299,8 @@
    3.24    "m mod n = (m - n) mod n" if "\<not> m < n" for m n :: nat
    3.25    by (rule le_mod_geq) (use that in \<open>simp add: not_less\<close>)
    3.26  
    3.27 -lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
    3.28 -  by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
    3.29 -
    3.30 -lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
    3.31 -
    3.32 -(*Loses information, namely we also have r<d provided d is nonzero*)
    3.33 -lemma mod_eqD:
    3.34 -  fixes m d r q :: nat
    3.35 -  assumes "m mod d = r"
    3.36 -  shows "\<exists>q. m = r + q * d"
    3.37 -proof -
    3.38 -  from div_mult_mod_eq obtain q where "q * d + m mod d = m" by blast
    3.39 -  with assms have "m = r + q * d" by simp
    3.40 -  then show ?thesis ..
    3.41 -qed
    3.42 -
    3.43 -lemma is_unit_int:
    3.44 -  "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
    3.45 -  by auto
    3.46 +lemma mod_eq_0D [dest!]:
    3.47 +  "\<exists>q. m = d * q" if "m mod d = 0" for m d :: nat
    3.48 +  using that by (auto simp add: mod_eq_0_iff_dvd elim: dvdE)
    3.49  
    3.50  end
     4.1 --- a/src/HOL/MacLaurin.thy	Sat May 12 17:53:12 2018 +0200
     4.2 +++ b/src/HOL/MacLaurin.thy	Sat May 12 22:20:46 2018 +0200
     4.3 @@ -526,31 +526,24 @@
     4.4  proof -
     4.5    have est: "x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y" for x y :: real
     4.6      by (rule mult_right_mono) simp_all
     4.7 -  let ?diff = "\<lambda>(n::nat) x.
     4.8 +  let ?diff = "\<lambda>(n::nat) (x::real).
     4.9      if n mod 4 = 0 then sin x
    4.10      else if n mod 4 = 1 then cos x
    4.11      else if n mod 4 = 2 then - sin x
    4.12      else - cos x"
    4.13    have diff_0: "?diff 0 = sin" by simp
    4.14 -  have DERIV_diff: "\<forall>m x. DERIV (?diff m) x :> ?diff (Suc m) x"
    4.15 -    apply clarify
    4.16 -    apply (subst (1 2 3) mod_Suc_eq_Suc_mod)
    4.17 -    apply (cut_tac m=m in mod_exhaust_less_4)
    4.18 -    apply safe
    4.19 -       apply (auto intro!: derivative_eq_intros)
    4.20 -    done
    4.21 +  have "DERIV (?diff m) x :> ?diff (Suc m) x" for m and x
    4.22 +    using mod_exhaust_less_4 [of m]
    4.23 +    by (auto simp add: mod_Suc intro!: derivative_eq_intros)
    4.24 +  then have DERIV_diff: "\<forall>m x. DERIV (?diff m) x :> ?diff (Suc m) x"
    4.25 +    by blast
    4.26    from Maclaurin_all_le [OF diff_0 DERIV_diff]
    4.27    obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>"
    4.28      and t2: "sin x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) + ?diff n t / (fact n) * x ^ n"
    4.29      by fast
    4.30 -  have diff_m_0: "\<And>m. ?diff m 0 = (if even m then 0 else (- 1) ^ ((m - Suc 0) div 2))"
    4.31 -    apply (subst even_even_mod_4_iff)
    4.32 -    apply (cut_tac m=m in mod_exhaust_less_4)
    4.33 -    apply (elim disjE)
    4.34 -       apply simp_all
    4.35 -     apply (safe dest!: mod_eqD)
    4.36 -     apply simp_all
    4.37 -    done
    4.38 +  have diff_m_0: "?diff m 0 = (if even m then 0 else (- 1) ^ ((m - Suc 0) div 2))" for m
    4.39 +    using mod_exhaust_less_4 [of m]
    4.40 +    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)
    4.41    show ?thesis
    4.42      unfolding sin_coeff_def
    4.43      apply (subst t2)
     5.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Sat May 12 17:53:12 2018 +0200
     5.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Sat May 12 22:20:46 2018 +0200
     5.3 @@ -838,7 +838,7 @@
     5.4      {
     5.5        assume "a ^ ((n - 1) div p) mod n = 0"
     5.6        then obtain s where s: "a ^ ((n - 1) div p) = n * s"
     5.7 -        unfolding mod_eq_0_iff by blast
     5.8 +        by blast
     5.9        then have eq0: "(a^((n - 1) div p))^p = (n*s)^p" by simp
    5.10        from qrn[symmetric] have qn1: "q dvd n - 1"
    5.11          by (auto simp: dvd_def)
     6.1 --- a/src/HOL/Parity.thy	Sat May 12 17:53:12 2018 +0200
     6.2 +++ b/src/HOL/Parity.thy	Sat May 12 22:20:46 2018 +0200
     6.3 @@ -542,6 +542,10 @@
     6.4    qed
     6.5  qed
     6.6  
     6.7 +lemma not_mod2_eq_Suc_0_eq_0 [simp]:
     6.8 +  "n mod 2 \<noteq> Suc 0 \<longleftrightarrow> n mod 2 = 0"
     6.9 +  using not_mod_2_eq_1_eq_0 [of n] by simp
    6.10 +
    6.11  
    6.12  subsection \<open>Parity and powers\<close>
    6.13  
     7.1 --- a/src/HOL/Presburger.thy	Sat May 12 17:53:12 2018 +0200
     7.2 +++ b/src/HOL/Presburger.thy	Sat May 12 22:20:46 2018 +0200
     7.3 @@ -495,11 +495,11 @@
     7.4    by presburger
     7.5  
     7.6  lemma odd_mod_4_div_2:
     7.7 -  "n mod 4 = (3::nat) \<Longrightarrow> odd ((n - 1) div 2)"
     7.8 +  "n mod 4 = (3::nat) \<Longrightarrow> odd ((n - Suc 0) div 2)"
     7.9    by presburger
    7.10  
    7.11  lemma even_mod_4_div_2:
    7.12 -  "n mod 4 = (1::nat) \<Longrightarrow> even ((n - 1) div 2)"
    7.13 +  "n mod 4 = Suc 0 \<Longrightarrow> even ((n - Suc 0) div 2)"
    7.14    by presburger
    7.15  
    7.16  
     8.1 --- a/src/HOL/Word/Word.thy	Sat May 12 17:53:12 2018 +0200
     8.2 +++ b/src/HOL/Word/Word.thy	Sat May 12 22:20:46 2018 +0200
     8.3 @@ -1750,13 +1750,8 @@
     8.4  
     8.5  lemma of_nat_eq: "of_nat n = w \<longleftrightarrow> (\<exists>q. n = unat w + q * 2 ^ len_of TYPE('a))"
     8.6    for w :: "'a::len word"
     8.7 -  apply (rule trans)
     8.8 -   apply (rule word_unat.inverse_norm)
     8.9 -  apply (rule iffI)
    8.10 -   apply (rule mod_eqD)
    8.11 -   apply simp
    8.12 -  apply clarsimp
    8.13 -  done
    8.14 +  using mod_div_mult_eq [of n "2 ^ LENGTH('a)", symmetric]
    8.15 +  by (auto simp add: word_unat.inverse_norm)
    8.16  
    8.17  lemma of_nat_eq_size: "of_nat n = w \<longleftrightarrow> (\<exists>q. n = unat w + q * 2 ^ size w)"
    8.18    unfolding word_size by (rule of_nat_eq)
     9.1 --- a/src/HOL/Word/Word_Miscellaneous.thy	Sat May 12 17:53:12 2018 +0200
     9.2 +++ b/src/HOL/Word/Word_Miscellaneous.thy	Sat May 12 22:20:46 2018 +0200
     9.3 @@ -275,7 +275,7 @@
     9.4  
     9.5  lemma mod_power_lem: "a > 1 \<Longrightarrow> a ^ n mod a ^ m = (if m \<le> n then 0 else a ^ n)"
     9.6    for a :: int
     9.7 -  by (simp add: mod_eq_0_iff le_imp_power_dvd)
     9.8 +  by (simp add: mod_eq_0_iff_dvd le_imp_power_dvd)
     9.9  
    9.10  lemma pl_pl_rels: "a + b = c + d \<Longrightarrow> a \<ge> c \<and> b \<le> d \<or> a \<le> c \<and> b \<ge> d"
    9.11    for a b c d :: nat