prefer generic elimination rules for even/odd over specialized unfold rules for nat
authorhaftmann
Sun Oct 19 18:05:26 2014 +0200 (2014-10-19)
changeset 58709efdc6c533bd3
parent 58708 6001375db251
child 58710 7216a10d69ba
prefer generic elimination rules for even/odd over specialized unfold rules for nat
src/HOL/Complex.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/MacLaurin.thy
src/HOL/NthRoot.thy
src/HOL/Parity.thy
src/HOL/Probability/Distributions.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Complex.thy	Sun Oct 19 12:47:34 2014 +0200
     1.2 +++ b/src/HOL/Complex.thy	Sun Oct 19 18:05:26 2014 +0200
     1.3 @@ -732,8 +732,8 @@
     1.4      hence cos: "cos d = 1" unfolding d_def cos_diff by simp
     1.5      moreover from cos have "sin d = 0" by (rule cos_one_sin_zero)
     1.6      ultimately have "d = 0"
     1.7 -      unfolding sin_zero_iff even_mult_two_ex
     1.8 -      by (auto simp add: numeral_2_eq_2 less_Suc_eq)
     1.9 +      unfolding sin_zero_iff
    1.10 +      by (auto simp add: numeral_2_eq_2 less_Suc_eq elim!: evenE)
    1.11      thus "a = x" unfolding d_def by simp
    1.12    qed (simp add: assms del: Re_sgn Im_sgn)
    1.13    with `z \<noteq> 0` show "arg z = x"
     2.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Sun Oct 19 12:47:34 2014 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Oct 19 18:05:26 2014 +0200
     2.3 @@ -137,8 +137,11 @@
     2.4  lemma get_odd_ex: "\<exists> k. Suc k = get_odd n \<and> odd (Suc k)"
     2.5    by (auto simp: get_odd_def odd_pos intro!: exI[of _ "n - 1"])
     2.6  
     2.7 -lemma get_even_double: "\<exists>i. get_even n = 2 * i" using get_even[unfolded even_mult_two_ex] .
     2.8 -lemma get_odd_double: "\<exists>i. get_odd n = 2 * i + 1" using get_odd[unfolded odd_Suc_mult_two_ex] by auto
     2.9 +lemma get_even_double:
    2.10 +  "\<exists>i. get_even n = 2 * i" using get_even by (blast elim: evenE)
    2.11 +
    2.12 +lemma get_odd_double:
    2.13 +  "\<exists>i. get_odd n = 2 * i + 1" using get_odd by (blast elim: oddE)
    2.14  
    2.15  section "Power function"
    2.16  
    2.17 @@ -363,7 +366,7 @@
    2.18    let ?S = "\<lambda>n. \<Sum> i=0..<n. ?c i"
    2.19  
    2.20    have "0 \<le> real (x * x)" by auto
    2.21 -  from `even n` obtain m where "2 * m = n" unfolding even_mult_two_ex by auto
    2.22 +  from `even n` obtain m where "2 * m = n" by (blast elim: evenE)
    2.23  
    2.24    have "arctan x \<in> { ?S n .. ?S (Suc n) }"
    2.25    proof (cases "real x = 0")
     3.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Sun Oct 19 12:47:34 2014 +0200
     3.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Sun Oct 19 18:05:26 2014 +0200
     3.3 @@ -3600,8 +3600,7 @@
     3.4    { fix n :: nat
     3.5      {
     3.6        assume en: "even n"
     3.7 -      from en obtain m where m: "n = 2 * m"
     3.8 -        unfolding even_mult_two_ex by blast
     3.9 +      from en obtain m where m: "n = 2 * m" ..
    3.10  
    3.11        have "?l $n = ?r$n"
    3.12          by (simp add: m fps_sin_def fps_cos_def power_mult_distrib power_mult power_minus [of "c ^ 2"])
     4.1 --- a/src/HOL/MacLaurin.thy	Sun Oct 19 12:47:34 2014 +0200
     4.2 +++ b/src/HOL/MacLaurin.thy	Sun Oct 19 18:05:26 2014 +0200
     4.3 @@ -425,7 +425,7 @@
     4.4  apply (erule ssubst)
     4.5  apply (rule_tac x = t in exI, simp)
     4.6  apply (rule setsum.cong[OF refl])
     4.7 -apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
     4.8 +apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE)
     4.9  done
    4.10  
    4.11  lemma Maclaurin_sin_expansion:
    4.12 @@ -450,7 +450,7 @@
    4.13  apply (erule ssubst)
    4.14  apply (rule_tac x = t in exI, simp)
    4.15  apply (rule setsum.cong[OF refl])
    4.16 -apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
    4.17 +apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE)
    4.18  done
    4.19  
    4.20  lemma Maclaurin_sin_expansion4:
    4.21 @@ -467,7 +467,7 @@
    4.22  apply (erule ssubst)
    4.23  apply (rule_tac x = t in exI, simp)
    4.24  apply (rule setsum.cong[OF refl])
    4.25 -apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
    4.26 +apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE)
    4.27  done
    4.28  
    4.29  
    4.30 @@ -497,7 +497,7 @@
    4.31  apply (erule ssubst)
    4.32  apply (rule_tac x = t in exI, simp)
    4.33  apply (rule setsum.cong[OF refl])
    4.34 -apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
    4.35 +apply (auto simp add: cos_coeff_def cos_zero_iff elim: evenE)
    4.36  done
    4.37  
    4.38  lemma Maclaurin_cos_expansion2:
    4.39 @@ -513,7 +513,7 @@
    4.40  apply (erule ssubst)
    4.41  apply (rule_tac x = t in exI, simp)
    4.42  apply (rule setsum.cong[OF refl])
    4.43 -apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
    4.44 +apply (auto simp add: cos_coeff_def cos_zero_iff elim: evenE)
    4.45  done
    4.46  
    4.47  lemma Maclaurin_minus_cos_expansion:
    4.48 @@ -529,7 +529,7 @@
    4.49  apply (erule ssubst)
    4.50  apply (rule_tac x = t in exI, simp)
    4.51  apply (rule setsum.cong[OF refl])
    4.52 -apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
    4.53 +apply (auto simp add: cos_coeff_def cos_zero_iff elim: evenE)
    4.54  done
    4.55  
    4.56  (* ------------------------------------------------------------------------- *)
     5.1 --- a/src/HOL/NthRoot.thy	Sun Oct 19 12:47:34 2014 +0200
     5.2 +++ b/src/HOL/NthRoot.thy	Sun Oct 19 18:05:26 2014 +0200
     5.3 @@ -429,8 +429,7 @@
     5.4    assumes n: "even n"
     5.5    shows "sqrt (2 ^ n) = 2 ^ (n div 2)"
     5.6  proof -
     5.7 -  from n obtain m where m: "n = 2 * m"
     5.8 -    unfolding even_mult_two_ex ..
     5.9 +  from n obtain m where m: "n = 2 * m" ..
    5.10    from m have "sqrt (2 ^ n) = sqrt ((2 ^ m)\<^sup>2)"
    5.11      by (simp only: power_mult[symmetric] mult.commute)
    5.12    then show ?thesis
     6.1 --- a/src/HOL/Parity.thy	Sun Oct 19 12:47:34 2014 +0200
     6.2 +++ b/src/HOL/Parity.thy	Sun Oct 19 18:05:26 2014 +0200
     6.3 @@ -514,14 +514,6 @@
     6.4  
     6.5  subsubsection {* Miscellaneous *}
     6.6  
     6.7 -lemma even_mult_two_ex:
     6.8 -  "even(n) = (\<exists>m::nat. n = 2*m)"
     6.9 -  by presburger
    6.10 -
    6.11 -lemma odd_Suc_mult_two_ex:
    6.12 -  "odd(n) = (\<exists>m. n = Suc (2*m))"
    6.13 -  by presburger
    6.14 -
    6.15  lemma even_nat_plus_one_div_two:
    6.16    "even (x::nat) ==> (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)"
    6.17    by presburger
     7.1 --- a/src/HOL/Probability/Distributions.thy	Sun Oct 19 12:47:34 2014 +0200
     7.2 +++ b/src/HOL/Probability/Distributions.thy	Sun Oct 19 18:05:26 2014 +0200
     7.3 @@ -941,7 +941,7 @@
     7.4                     filterlim_at_top_imp_at_infinity filterlim_ident filterlim_pow_at_top filterlim_ident)
     7.5               auto
     7.6          also have "(\<lambda>x. ((x\<^sup>2)^(k div 2 + 1) / exp (x\<^sup>2)) * (1 / x) :: real) = ?M (k + 1)"
     7.7 -          using `even k` by (auto simp: even_mult_two_ex fun_eq_iff exp_minus field_simps power2_eq_square power_mult)
     7.8 +          using `even k` by (auto simp: fun_eq_iff exp_minus field_simps power2_eq_square power_mult elim: evenE)
     7.9          finally show ?thesis by simp
    7.10        next
    7.11          assume "odd k"
    7.12 @@ -950,7 +950,7 @@
    7.13                      filterlim_ident filterlim_pow_at_top)
    7.14               auto
    7.15          also have "(\<lambda>x. ((x\<^sup>2)^((k - 1) div 2 + 1) / exp (x\<^sup>2)) :: real) = ?M (k + 1)"
    7.16 -          using `odd k` by (auto simp: odd_Suc_mult_two_ex fun_eq_iff exp_minus field_simps power2_eq_square power_mult)
    7.17 +          using `odd k` by (auto simp: fun_eq_iff exp_minus field_simps power2_eq_square power_mult elim: oddE)
    7.18          finally show ?thesis by simp
    7.19        qed
    7.20      qed
    7.21 @@ -1126,19 +1126,19 @@
    7.22  lemma integrable_normal_moment: "integrable lborel (\<lambda>x. normal_density \<mu> \<sigma> x * (x - \<mu>)^k)"
    7.23  proof cases
    7.24    assume "even k" then show ?thesis
    7.25 -    using integrable.intros[OF normal_moment_even] by (auto simp add: even_mult_two_ex)
    7.26 +    using integrable.intros[OF normal_moment_even] by (auto elim: evenE)
    7.27  next
    7.28    assume "odd k" then show ?thesis
    7.29 -    using integrable.intros[OF normal_moment_odd] by (auto simp add: odd_Suc_mult_two_ex)
    7.30 +    using integrable.intros[OF normal_moment_odd] by (auto elim: oddE)
    7.31  qed
    7.32  
    7.33  lemma integrable_normal_moment_abs: "integrable lborel (\<lambda>x. normal_density \<mu> \<sigma> x * \<bar>x - \<mu>\<bar>^k)"
    7.34  proof cases
    7.35    assume "even k" then show ?thesis
    7.36 -    using integrable.intros[OF normal_moment_even] by (auto simp add: even_mult_two_ex power_even_abs)
    7.37 +    using integrable.intros[OF normal_moment_even] by (auto simp add: power_even_abs elim: evenE)
    7.38  next
    7.39    assume "odd k" then show ?thesis
    7.40 -    using integrable.intros[OF normal_moment_abs_odd] by (auto simp add: odd_Suc_mult_two_ex)
    7.41 +    using integrable.intros[OF normal_moment_abs_odd] by (auto elim: oddE)
    7.42  qed
    7.43  
    7.44  lemma integrable_normal_density[simp, intro]: "integrable lborel (normal_density \<mu> \<sigma>)"
     8.1 --- a/src/HOL/Transcendental.thy	Sun Oct 19 12:47:34 2014 +0200
     8.2 +++ b/src/HOL/Transcendental.thy	Sun Oct 19 18:05:26 2014 +0200
     8.3 @@ -2275,7 +2275,7 @@
     8.4  
     8.5  lemma cos_coeff_Suc: "cos_coeff (Suc n) = - sin_coeff n / real (Suc n)"
     8.6    unfolding cos_coeff_def sin_coeff_def
     8.7 -  by (simp del: mult_Suc, auto simp add: odd_Suc_mult_two_ex)
     8.8 +  by (simp del: mult_Suc) (auto elim: oddE)
     8.9  
    8.10  lemma summable_sin: "summable (\<lambda>n. sin_coeff n * x ^ n)"
    8.11    unfolding sin_coeff_def
    8.12 @@ -2863,24 +2863,30 @@
    8.13        \<exists>n::nat. even n & x = real n * (pi/2)"
    8.14  apply (subgoal_tac "\<exists>n::nat. ~ even n & x + pi/2 = real n * (pi/2) ")
    8.15   apply (clarify, rule_tac x = "n - 1" in exI)
    8.16 - apply (force simp add: odd_Suc_mult_two_ex real_of_nat_Suc distrib_right)
    8.17 -apply (rule cos_zero_lemma)
    8.18 -apply (simp_all add: cos_add)
    8.19 + apply (auto elim!: oddE simp add: real_of_nat_Suc field_simps)[1]
    8.20 + apply (rule cos_zero_lemma)
    8.21 + apply (auto simp add: cos_add)
    8.22  done
    8.23  
    8.24 -
    8.25  lemma cos_zero_iff:
    8.26       "(cos x = 0) =
    8.27        ((\<exists>n::nat. ~even n & (x = real n * (pi/2))) |
    8.28         (\<exists>n::nat. ~even n & (x = -(real n * (pi/2)))))"
    8.29 -apply (rule iffI)
    8.30 -apply (cut_tac linorder_linear [of 0 x], safe)
    8.31 -apply (drule cos_zero_lemma, assumption+)
    8.32 -apply (cut_tac x="-x" in cos_zero_lemma, simp, simp)
    8.33 -apply (force simp add: minus_equation_iff [of x])
    8.34 -apply (auto simp only: odd_Suc_mult_two_ex real_of_nat_Suc distrib_right)
    8.35 -apply (auto simp add: cos_diff cos_add)
    8.36 -done
    8.37 +proof -
    8.38 +  { fix n :: nat
    8.39 +    assume "odd n"
    8.40 +    then obtain m where "n = 2 * m + 1" ..
    8.41 +    then have "cos (real n * pi / 2) = 0"
    8.42 +      by (simp add: field_simps real_of_nat_Suc) (simp add: cos_add add_divide_distrib)
    8.43 +  } note * = this
    8.44 +  show ?thesis
    8.45 +  apply (rule iffI)
    8.46 +  apply (cut_tac linorder_linear [of 0 x], safe)
    8.47 +  apply (drule cos_zero_lemma, assumption+)
    8.48 +  apply (cut_tac x="-x" in cos_zero_lemma, simp, simp)
    8.49 +  apply (auto dest: *)
    8.50 +  done
    8.51 +qed
    8.52  
    8.53  (* ditto: but to a lesser extent *)
    8.54  lemma sin_zero_iff:
    8.55 @@ -2892,7 +2898,7 @@
    8.56  apply (drule sin_zero_lemma, assumption+)
    8.57  apply (cut_tac x="-x" in sin_zero_lemma, simp, simp, safe)
    8.58  apply (force simp add: minus_equation_iff [of x])
    8.59 -apply (auto simp add: even_mult_two_ex)
    8.60 +apply (auto elim: evenE)
    8.61  done
    8.62  
    8.63  lemma cos_monotone_0_pi:
    8.64 @@ -3623,7 +3629,7 @@
    8.65    by (auto intro!: derivative_eq_intros)
    8.66  
    8.67  lemma sin_zero_abs_cos_one: "sin x = 0 ==> \<bar>cos x\<bar> = 1"
    8.68 -  by (auto simp add: sin_zero_iff even_mult_two_ex)
    8.69 +  by (auto simp add: sin_zero_iff elim: evenE)
    8.70  
    8.71  lemma cos_one_sin_zero: "cos x = 1 ==> sin x = 0"
    8.72    using sin_cos_squared_add3 [where x = x] by auto
    8.73 @@ -3973,8 +3979,8 @@
    8.74          proof (cases "even n")
    8.75            case True
    8.76            hence sgn_pos: "(-1)^n = (1::real)" by auto
    8.77 -          from `even n` obtain m where "2 * m = n"
    8.78 -            unfolding even_mult_two_ex by auto
    8.79 +          from `even n` obtain m where "n = 2 * m" ..
    8.80 +          then have "2 * m = n" ..
    8.81            from bounds[of m, unfolded this atLeastAtMost_iff]
    8.82            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))"
    8.83              by auto
    8.84 @@ -3984,8 +3990,8 @@
    8.85          next
    8.86            case False
    8.87            hence sgn_neg: "(-1)^n = (-1::real)" by auto
    8.88 -          from `odd n` obtain m where m_def: "2 * m + 1 = n"
    8.89 -            unfolding odd_Suc_mult_two_ex by auto
    8.90 +          from `odd n` obtain m where "n = 2 * m + 1" ..
    8.91 +          then have m_def: "2 * m + 1 = n" ..
    8.92            hence m_plus: "2 * (m + 1) = n + 1" by auto
    8.93            from bounds[of "m + 1", unfolded this atLeastAtMost_iff, THEN conjunct1] bounds[of m, unfolded m_def atLeastAtMost_iff, THEN conjunct2]
    8.94            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))"