# HG changeset patch
# User haftmann
# Date 1413734726 -7200
# Node ID efdc6c533bd3c67e19fa814a283dd68e18bcfb07
# Parent  6001375db25160fef5defbeb9e1aa64b7fc62aed
prefer generic elimination rules for even/odd over specialized unfold rules for nat

diff -r 6001375db251 -r efdc6c533bd3 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Sun Oct 19 12:47:34 2014 +0200
+++ b/src/HOL/Complex.thy	Sun Oct 19 18:05:26 2014 +0200
@@ -732,8 +732,8 @@
     hence cos: "cos d = 1" unfolding d_def cos_diff by simp
     moreover from cos have "sin d = 0" by (rule cos_one_sin_zero)
     ultimately have "d = 0"
-      unfolding sin_zero_iff even_mult_two_ex
-      by (auto simp add: numeral_2_eq_2 less_Suc_eq)
+      unfolding sin_zero_iff
+      by (auto simp add: numeral_2_eq_2 less_Suc_eq elim!: evenE)
     thus "a = x" unfolding d_def by simp
   qed (simp add: assms del: Re_sgn Im_sgn)
   with `z \<noteq> 0` show "arg z = x"
diff -r 6001375db251 -r efdc6c533bd3 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Sun Oct 19 12:47:34 2014 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Oct 19 18:05:26 2014 +0200
@@ -137,8 +137,11 @@
 lemma get_odd_ex: "\<exists> k. Suc k = get_odd n \<and> odd (Suc k)"
   by (auto simp: get_odd_def odd_pos intro!: exI[of _ "n - 1"])
 
-lemma get_even_double: "\<exists>i. get_even n = 2 * i" using get_even[unfolded even_mult_two_ex] .
-lemma get_odd_double: "\<exists>i. get_odd n = 2 * i + 1" using get_odd[unfolded odd_Suc_mult_two_ex] by auto
+lemma get_even_double:
+  "\<exists>i. get_even n = 2 * i" using get_even by (blast elim: evenE)
+
+lemma get_odd_double:
+  "\<exists>i. get_odd n = 2 * i + 1" using get_odd by (blast elim: oddE)
 
 section "Power function"
 
@@ -363,7 +366,7 @@
   let ?S = "\<lambda>n. \<Sum> i=0..<n. ?c i"
 
   have "0 \<le> real (x * x)" by auto
-  from `even n` obtain m where "2 * m = n" unfolding even_mult_two_ex by auto
+  from `even n` obtain m where "2 * m = n" by (blast elim: evenE)
 
   have "arctan x \<in> { ?S n .. ?S (Suc n) }"
   proof (cases "real x = 0")
diff -r 6001375db251 -r efdc6c533bd3 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Sun Oct 19 12:47:34 2014 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Sun Oct 19 18:05:26 2014 +0200
@@ -3600,8 +3600,7 @@
   { fix n :: nat
     {
       assume en: "even n"
-      from en obtain m where m: "n = 2 * m"
-        unfolding even_mult_two_ex by blast
+      from en obtain m where m: "n = 2 * m" ..
 
       have "?l $n = ?r$n"
         by (simp add: m fps_sin_def fps_cos_def power_mult_distrib power_mult power_minus [of "c ^ 2"])
diff -r 6001375db251 -r efdc6c533bd3 src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Sun Oct 19 12:47:34 2014 +0200
+++ b/src/HOL/MacLaurin.thy	Sun Oct 19 18:05:26 2014 +0200
@@ -425,7 +425,7 @@
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule setsum.cong[OF refl])
-apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
+apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE)
 done
 
 lemma Maclaurin_sin_expansion:
@@ -450,7 +450,7 @@
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule setsum.cong[OF refl])
-apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
+apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE)
 done
 
 lemma Maclaurin_sin_expansion4:
@@ -467,7 +467,7 @@
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule setsum.cong[OF refl])
-apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
+apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE)
 done
 
 
@@ -497,7 +497,7 @@
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule setsum.cong[OF refl])
-apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
+apply (auto simp add: cos_coeff_def cos_zero_iff elim: evenE)
 done
 
 lemma Maclaurin_cos_expansion2:
@@ -513,7 +513,7 @@
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule setsum.cong[OF refl])
-apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
+apply (auto simp add: cos_coeff_def cos_zero_iff elim: evenE)
 done
 
 lemma Maclaurin_minus_cos_expansion:
@@ -529,7 +529,7 @@
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule setsum.cong[OF refl])
-apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
+apply (auto simp add: cos_coeff_def cos_zero_iff elim: evenE)
 done
 
 (* ------------------------------------------------------------------------- *)
diff -r 6001375db251 -r efdc6c533bd3 src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Sun Oct 19 12:47:34 2014 +0200
+++ b/src/HOL/NthRoot.thy	Sun Oct 19 18:05:26 2014 +0200
@@ -429,8 +429,7 @@
   assumes n: "even n"
   shows "sqrt (2 ^ n) = 2 ^ (n div 2)"
 proof -
-  from n obtain m where m: "n = 2 * m"
-    unfolding even_mult_two_ex ..
+  from n obtain m where m: "n = 2 * m" ..
   from m have "sqrt (2 ^ n) = sqrt ((2 ^ m)\<^sup>2)"
     by (simp only: power_mult[symmetric] mult.commute)
   then show ?thesis
diff -r 6001375db251 -r efdc6c533bd3 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sun Oct 19 12:47:34 2014 +0200
+++ b/src/HOL/Parity.thy	Sun Oct 19 18:05:26 2014 +0200
@@ -514,14 +514,6 @@
 
 subsubsection {* Miscellaneous *}
 
-lemma even_mult_two_ex:
-  "even(n) = (\<exists>m::nat. n = 2*m)"
-  by presburger
-
-lemma odd_Suc_mult_two_ex:
-  "odd(n) = (\<exists>m. n = Suc (2*m))"
-  by presburger
-
 lemma even_nat_plus_one_div_two:
   "even (x::nat) ==> (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)"
   by presburger
diff -r 6001375db251 -r efdc6c533bd3 src/HOL/Probability/Distributions.thy
--- a/src/HOL/Probability/Distributions.thy	Sun Oct 19 12:47:34 2014 +0200
+++ b/src/HOL/Probability/Distributions.thy	Sun Oct 19 18:05:26 2014 +0200
@@ -941,7 +941,7 @@
                    filterlim_at_top_imp_at_infinity filterlim_ident filterlim_pow_at_top filterlim_ident)
              auto
         also have "(\<lambda>x. ((x\<^sup>2)^(k div 2 + 1) / exp (x\<^sup>2)) * (1 / x) :: real) = ?M (k + 1)"
-          using `even k` by (auto simp: even_mult_two_ex fun_eq_iff exp_minus field_simps power2_eq_square power_mult)
+          using `even k` by (auto simp: fun_eq_iff exp_minus field_simps power2_eq_square power_mult elim: evenE)
         finally show ?thesis by simp
       next
         assume "odd k"
@@ -950,7 +950,7 @@
                     filterlim_ident filterlim_pow_at_top)
              auto
         also have "(\<lambda>x. ((x\<^sup>2)^((k - 1) div 2 + 1) / exp (x\<^sup>2)) :: real) = ?M (k + 1)"
-          using `odd k` by (auto simp: odd_Suc_mult_two_ex fun_eq_iff exp_minus field_simps power2_eq_square power_mult)
+          using `odd k` by (auto simp: fun_eq_iff exp_minus field_simps power2_eq_square power_mult elim: oddE)
         finally show ?thesis by simp
       qed
     qed
@@ -1126,19 +1126,19 @@
 lemma integrable_normal_moment: "integrable lborel (\<lambda>x. normal_density \<mu> \<sigma> x * (x - \<mu>)^k)"
 proof cases
   assume "even k" then show ?thesis
-    using integrable.intros[OF normal_moment_even] by (auto simp add: even_mult_two_ex)
+    using integrable.intros[OF normal_moment_even] by (auto elim: evenE)
 next
   assume "odd k" then show ?thesis
-    using integrable.intros[OF normal_moment_odd] by (auto simp add: odd_Suc_mult_two_ex)
+    using integrable.intros[OF normal_moment_odd] by (auto elim: oddE)
 qed
 
 lemma integrable_normal_moment_abs: "integrable lborel (\<lambda>x. normal_density \<mu> \<sigma> x * \<bar>x - \<mu>\<bar>^k)"
 proof cases
   assume "even k" then show ?thesis
-    using integrable.intros[OF normal_moment_even] by (auto simp add: even_mult_two_ex power_even_abs)
+    using integrable.intros[OF normal_moment_even] by (auto simp add: power_even_abs elim: evenE)
 next
   assume "odd k" then show ?thesis
-    using integrable.intros[OF normal_moment_abs_odd] by (auto simp add: odd_Suc_mult_two_ex)
+    using integrable.intros[OF normal_moment_abs_odd] by (auto elim: oddE)
 qed
 
 lemma integrable_normal_density[simp, intro]: "integrable lborel (normal_density \<mu> \<sigma>)"
diff -r 6001375db251 -r efdc6c533bd3 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun Oct 19 12:47:34 2014 +0200
+++ b/src/HOL/Transcendental.thy	Sun Oct 19 18:05:26 2014 +0200
@@ -2275,7 +2275,7 @@
 
 lemma cos_coeff_Suc: "cos_coeff (Suc n) = - sin_coeff n / real (Suc n)"
   unfolding cos_coeff_def sin_coeff_def
-  by (simp del: mult_Suc, auto simp add: odd_Suc_mult_two_ex)
+  by (simp del: mult_Suc) (auto elim: oddE)
 
 lemma summable_sin: "summable (\<lambda>n. sin_coeff n * x ^ n)"
   unfolding sin_coeff_def
@@ -2863,24 +2863,30 @@
       \<exists>n::nat. even n & x = real n * (pi/2)"
 apply (subgoal_tac "\<exists>n::nat. ~ even n & x + pi/2 = real n * (pi/2) ")
  apply (clarify, rule_tac x = "n - 1" in exI)
- apply (force simp add: odd_Suc_mult_two_ex real_of_nat_Suc distrib_right)
-apply (rule cos_zero_lemma)
-apply (simp_all add: cos_add)
+ apply (auto elim!: oddE simp add: real_of_nat_Suc field_simps)[1]
+ apply (rule cos_zero_lemma)
+ apply (auto simp add: cos_add)
 done
 
-
 lemma cos_zero_iff:
      "(cos x = 0) =
       ((\<exists>n::nat. ~even n & (x = real n * (pi/2))) |
        (\<exists>n::nat. ~even n & (x = -(real n * (pi/2)))))"
-apply (rule iffI)
-apply (cut_tac linorder_linear [of 0 x], safe)
-apply (drule cos_zero_lemma, assumption+)
-apply (cut_tac x="-x" in cos_zero_lemma, simp, simp)
-apply (force simp add: minus_equation_iff [of x])
-apply (auto simp only: odd_Suc_mult_two_ex real_of_nat_Suc distrib_right)
-apply (auto simp add: cos_diff cos_add)
-done
+proof -
+  { fix n :: nat
+    assume "odd n"
+    then obtain m where "n = 2 * m + 1" ..
+    then have "cos (real n * pi / 2) = 0"
+      by (simp add: field_simps real_of_nat_Suc) (simp add: cos_add add_divide_distrib)
+  } note * = this
+  show ?thesis
+  apply (rule iffI)
+  apply (cut_tac linorder_linear [of 0 x], safe)
+  apply (drule cos_zero_lemma, assumption+)
+  apply (cut_tac x="-x" in cos_zero_lemma, simp, simp)
+  apply (auto dest: *)
+  done
+qed
 
 (* ditto: but to a lesser extent *)
 lemma sin_zero_iff:
@@ -2892,7 +2898,7 @@
 apply (drule sin_zero_lemma, assumption+)
 apply (cut_tac x="-x" in sin_zero_lemma, simp, simp, safe)
 apply (force simp add: minus_equation_iff [of x])
-apply (auto simp add: even_mult_two_ex)
+apply (auto elim: evenE)
 done
 
 lemma cos_monotone_0_pi:
@@ -3623,7 +3629,7 @@
   by (auto intro!: derivative_eq_intros)
 
 lemma sin_zero_abs_cos_one: "sin x = 0 ==> \<bar>cos x\<bar> = 1"
-  by (auto simp add: sin_zero_iff even_mult_two_ex)
+  by (auto simp add: sin_zero_iff elim: evenE)
 
 lemma cos_one_sin_zero: "cos x = 1 ==> sin x = 0"
   using sin_cos_squared_add3 [where x = x] by auto
@@ -3973,8 +3979,8 @@
         proof (cases "even n")
           case True
           hence sgn_pos: "(-1)^n = (1::real)" by auto
-          from `even n` obtain m where "2 * m = n"
-            unfolding even_mult_two_ex by auto
+          from `even n` obtain m where "n = 2 * m" ..
+          then have "2 * m = n" ..
           from bounds[of m, unfolded this atLeastAtMost_iff]
           have "\<bar>arctan x - (\<Sum>i<n. (?c x i))\<bar> \<le> (\<Sum>i<n + 1. (?c x i)) - (\<Sum>i<n. (?c x i))"
             by auto
@@ -3984,8 +3990,8 @@
         next
           case False
           hence sgn_neg: "(-1)^n = (-1::real)" by auto
-          from `odd n` obtain m where m_def: "2 * m + 1 = n"
-            unfolding odd_Suc_mult_two_ex by auto
+          from `odd n` obtain m where "n = 2 * m + 1" ..
+          then have m_def: "2 * m + 1 = n" ..
           hence m_plus: "2 * (m + 1) = n + 1" by auto
           from bounds[of "m + 1", unfolded this atLeastAtMost_iff, THEN conjunct1] bounds[of m, unfolded m_def atLeastAtMost_iff, THEN conjunct2]
           have "\<bar>arctan x - (\<Sum>i<n. (?c x i))\<bar> \<le> (\<Sum>i<n. (?c x i)) - (\<Sum>i<n+1. (?c x i))"