prefer generic elimination rules for even/odd over specialized unfold rules for nat
--- 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"
--- 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")
--- 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"])
--- 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
(* ------------------------------------------------------------------------- *)
--- 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
--- 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
--- 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>)"
--- 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))"