--- a/src/HOL/Transcendental.thy Fri Jul 06 22:52:49 2018 +0200
+++ b/src/HOL/Transcendental.thy Sat Jul 07 15:07:46 2018 +0100
@@ -251,7 +251,7 @@
then have "Bseq (\<lambda>n. f n * x^n)"
by (rule Cauchy_Bseq)
then obtain K where 3: "0 < K" and 4: "\<forall>n. norm (f n * x^n) \<le> K"
- by (auto simp add: Bseq_def)
+ by (auto simp: Bseq_def)
have "\<exists>N. \<forall>n\<ge>N. norm (norm (f n * z ^ n)) \<le> K * norm (z ^ n) * inverse (norm (x^n))"
proof (intro exI allI impI)
fix n :: nat
@@ -369,7 +369,7 @@
proof (cases "even m")
case True
then show ?thesis
- by (auto simp add: even_two_times_div_two)
+ by (auto simp: even_two_times_div_two)
next
case False
then have eq: "Suc (2 * (m div 2)) = m" by simp
@@ -612,7 +612,7 @@
fixes z :: "'a :: {monoid_mult,comm_ring}"
shows "(\<Sum>p<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =
(\<Sum>p<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p))))"
- by (auto simp add: algebra_simps power_add [symmetric])
+ by (auto simp: algebra_simps power_add [symmetric])
lemma sumr_diff_mult_const2: "sum f {..<n} - of_nat n * r = (\<Sum>i<n. f i - r)"
for r :: "'a::ring_1"
@@ -660,7 +660,7 @@
and K: "0 \<le> K"
shows "sum f {..<n-k} \<le> of_nat n * K"
apply (rule order_trans [OF sum_mono [OF f]])
- apply (auto simp add: mult_right_mono K)
+ apply (auto simp: mult_right_mono K)
done
lemma lemma_termdiff3:
@@ -691,8 +691,7 @@
mult_nonneg_nonneg
of_nat_0_le_iff
zero_le_power K)
- apply (rule le_Kn)
- apply simp
+ apply (rule le_Kn, simp)
done
qed
also have "\<dots> = of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h"
@@ -712,7 +711,7 @@
show "eventually (\<lambda>h. 0 \<le> norm (f h)) (at 0)"
by simp
show "eventually (\<lambda>h. norm (f h) \<le> K * norm h) (at 0)"
- using k by (auto simp add: eventually_at dist_norm le)
+ using k by (auto simp: eventually_at dist_norm le)
show "(\<lambda>h. 0) \<midarrow>(0::'a)\<rightarrow> (0::real)"
by (rule tendsto_const)
have "(\<lambda>h. K * norm h) \<midarrow>(0::'a)\<rightarrow> K * norm (0::'a)"
@@ -788,11 +787,9 @@
"(\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0)) =
(\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))"
apply (rule ext)
- apply (case_tac n)
- apply simp
+ apply (case_tac n, simp)
apply (rename_tac nat)
- apply (case_tac nat)
- apply simp
+ apply (case_tac nat, simp)
apply (simp add: r_neq_0)
done
finally show "summable (\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))" .
@@ -868,13 +865,11 @@
then obtain r :: real where r: "norm x < norm r" "norm r < K" "r > 0"
using K False
by (auto simp: field_simps abs_less_iff add_pos_pos intro: that [of "(norm x + K) / 2"])
- have "(\<lambda>n. of_nat n * (x / of_real r) ^ n) \<longlonglongrightarrow> 0"
+ have to0: "(\<lambda>n. of_nat n * (x / of_real r) ^ n) \<longlonglongrightarrow> 0"
using r by (simp add: norm_divide powser_times_n_limit_0 [of "x / of_real r"])
- then obtain N where N: "\<And>n. n\<ge>N \<Longrightarrow> real_of_nat n * norm x ^ n < r ^ n"
- using r unfolding LIMSEQ_iff
- apply (drule_tac x=1 in spec)
- apply (auto simp: norm_divide norm_mult norm_power field_simps)
- done
+ obtain N where N: "\<And>n. n\<ge>N \<Longrightarrow> real_of_nat n * norm x ^ n < r ^ n"
+ using r LIMSEQ_D [OF to0, of 1]
+ by (auto simp: norm_divide norm_mult norm_power field_simps)
have "summable (\<lambda>n. (of_nat n * c n) * x ^ n)"
proof (rule summable_comparison_test')
show "summable (\<lambda>n. norm (c n * of_real r ^ n))"
@@ -1007,7 +1002,7 @@
then show ?thesis
apply (rule Lim_transform)
apply (clarsimp simp: LIM_eq)
- apply (rule_tac x="s" in exI)
+ apply (rule_tac x=s in exI)
using s sm sums_unique by fastforce
qed
@@ -1018,10 +1013,7 @@
shows "(f \<longlongrightarrow> a 0) (at 0)"
proof -
have *: "((\<lambda>x. if x = 0 then a 0 else f x) \<longlongrightarrow> a 0) (at 0)"
- apply (rule powser_limit_0 [OF s])
- apply (case_tac "x = 0")
- apply (auto simp add: powser_sums_zero sm)
- done
+ by (rule powser_limit_0 [OF s]) (auto simp: powser_sums_zero sm)
show ?thesis
apply (subst LIM_equal [where g = "(\<lambda>x. if x = 0 then a 0 else f x)"])
apply (simp_all add: *)
@@ -1077,7 +1069,7 @@
obtain s where s_bound: "0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < s \<longrightarrow> \<bar>?diff n x - f' x0 n\<bar> < ?r)"
by auto
have "0 < ?s n"
- by (rule someI2[where a=s]) (auto simp add: s_bound simp del: of_nat_Suc)
+ by (rule someI2[where a=s]) (auto simp: s_bound simp del: of_nat_Suc)
then show "0 < x" by (simp only: \<open>x = ?s n\<close>)
qed
qed auto
@@ -1154,9 +1146,8 @@
also have "\<dots> \<le> ?diff_part + \<bar>(\<Sum>n. ?diff (n + ?N) x) - (\<Sum> n. f' x0 (n + ?N))\<bar>"
unfolding suminf_split_initial_segment[OF all_smbl, where k="?N"]
unfolding suminf_diff[OF div_shft_smbl ign[OF \<open>summable (f' x0)\<close>]]
- apply (subst (5) add.commute)
- apply (rule abs_triangle_ineq)
- done
+ apply (simp only: add.commute)
+ using abs_triangle_ineq by blast
also have "\<dots> \<le> ?diff_part + ?L_part + ?f'_part"
using abs_triangle_ineq4 by auto
also have "\<dots> < r /3 + r/3 + r/3"
@@ -1373,12 +1364,16 @@
lemma DERIV_exp [simp]: "DERIV exp x :> exp x"
unfolding exp_def scaleR_conv_of_real
- apply (rule DERIV_cong)
- apply (rule termdiffs [where K="of_real (1 + norm x)"])
- apply (simp_all only: diffs_of_real scaleR_conv_of_real exp_fdiffs)
- apply (rule exp_converges [THEN sums_summable, unfolded scaleR_conv_of_real])+
- apply (simp del: of_real_add)
- done
+proof (rule DERIV_cong)
+ have sinv: "summable (\<lambda>n. of_real (inverse (fact n)) * x ^ n)" for x::'a
+ by (rule exp_converges [THEN sums_summable, unfolded scaleR_conv_of_real])
+ note xx = exp_converges [THEN sums_summable, unfolded scaleR_conv_of_real]
+ show "((\<lambda>x. \<Sum>n. of_real (inverse (fact n)) * x ^ n) has_field_derivative
+ (\<Sum>n. diffs (\<lambda>n. of_real (inverse (fact n))) n * x ^ n)) (at x)"
+ by (rule termdiffs [where K="of_real (1 + norm x)"]) (simp_all only: diffs_of_real exp_fdiffs sinv norm_of_real)
+ show "(\<Sum>n. diffs (\<lambda>n. of_real (inverse (fact n))) n * x ^ n) = (\<Sum>n. of_real (inverse (fact n)) * x ^ n)"
+ by (simp add: diffs_of_real exp_fdiffs)
+qed
declare DERIV_exp[THEN DERIV_chain2, derivative_intros]
and DERIV_exp[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
@@ -1487,8 +1482,7 @@
lemma exp_of_real: "exp (of_real x) = of_real (exp x)"
unfolding exp_def
- apply (subst suminf_of_real)
- apply (rule summable_exp_generic)
+ apply (subst suminf_of_real [OF summable_exp_generic])
apply (simp add: scaleR_conv_of_real)
done
@@ -1518,7 +1512,7 @@
lemma exp_of_nat_mult: "exp (of_nat n * x) = exp x ^ n"
for x :: "'a::{real_normed_field,banach}"
- by (induct n) (auto simp add: distrib_left exp_add mult.commute)
+ by (induct n) (auto simp: distrib_left exp_add mult.commute)
corollary exp_of_nat2_mult: "exp (x * of_nat n) = exp x ^ n"
for x :: "'a::{real_normed_field,banach}"
@@ -1533,9 +1527,6 @@
shows "exp (x / of_nat n) ^ n = exp x"
using assms
proof (induction n arbitrary: x)
- case 0
- then show ?case by simp
-next
case (Suc n)
show ?case
proof (cases "n = 0")
@@ -1553,7 +1544,7 @@
using Suc.IH [of "x * of_nat n / (1 + of_nat n)"] False
by (simp add: exp_add [symmetric])
qed
-qed
+qed simp
subsubsection \<open>Properties of the Exponential Function on Reals\<close>
@@ -1596,19 +1587,15 @@
proof
assume "0 < x"
have "1 + x \<le> (\<Sum>n<2. inverse (fact n) * x^n)"
- by (auto simp add: numeral_2_eq_2)
+ by (auto simp: numeral_2_eq_2)
also have "\<dots> \<le> (\<Sum>n. inverse (fact n) * x^n)"
apply (rule sum_le_suminf [OF summable_exp])
using \<open>0 < x\<close>
- apply (auto simp add: zero_le_mult_iff)
+ apply (auto simp add: zero_le_mult_iff)
done
finally show "1 + x \<le> exp x"
by (simp add: exp_def)
-next
- assume "0 = x"
- then show "1 + x \<le> exp x"
- by auto
-qed
+qed auto
lemma exp_gt_one: "0 < x \<Longrightarrow> 1 < exp x"
for x :: real
@@ -1634,7 +1621,7 @@
lemma exp_less_cancel: "exp x < exp y \<Longrightarrow> x < y"
for x y :: real
unfolding linorder_not_le [symmetric]
- by (auto simp add: order_le_less exp_less_mono)
+ by (auto simp: order_le_less exp_less_mono)
lemma exp_less_cancel_iff [iff]: "exp x < exp y \<longleftrightarrow> x < y"
for x y :: real
@@ -1642,7 +1629,7 @@
lemma exp_le_cancel_iff [iff]: "exp x \<le> exp y \<longleftrightarrow> x \<le> y"
for x y :: real
- by (auto simp add: linorder_not_less [symmetric])
+ by (auto simp: linorder_not_less [symmetric])
lemma exp_inj_iff [iff]: "exp x = exp y \<longleftrightarrow> x = y"
for x y :: real
@@ -1916,7 +1903,7 @@
then have "norm (-x) < 1" by auto
show "summable (\<lambda>n. (- 1) ^ n * (1 / real (n + 1)) * real (Suc n) * x^n)"
unfolding One_nat_def
- by (auto simp add: power_mult_distrib[symmetric] summable_geometric[OF \<open>norm (-x) < 1\<close>])
+ by (auto simp: power_mult_distrib[symmetric] summable_geometric[OF \<open>norm (-x) < 1\<close>])
qed
then have "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)"
unfolding One_nat_def by auto
@@ -1925,7 +1912,7 @@
ultimately have "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> suminf (?f' x) - suminf (?f' x)"
by (rule DERIV_diff)
then show "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> 0" by auto
- qed (auto simp add: assms)
+ qed (auto simp: assms)
then show ?thesis by auto
qed
@@ -1955,39 +1942,38 @@
and b: "x \<le> 1"
shows "exp x \<le> 1 + x + x\<^sup>2"
proof -
- have aux1: "inverse (fact (n + 2)) * x ^ (n + 2) \<le> (x\<^sup>2/2) * ((1/2)^n)" for n :: nat
- proof -
- have "(2::nat) * 2 ^ n \<le> fact (n + 2)"
- by (induct n) simp_all
- then have "real ((2::nat) * 2 ^ n) \<le> real_of_nat (fact (n + 2))"
- by (simp only: of_nat_le_iff)
- then have "((2::real) * 2 ^ n) \<le> fact (n + 2)"
- unfolding of_nat_fact by simp
- then have "inverse (fact (n + 2)) \<le> inverse ((2::real) * 2 ^ n)"
- by (rule le_imp_inverse_le) simp
- then have "inverse (fact (n + 2)) \<le> 1/(2::real) * (1/2)^n"
- by (simp add: power_inverse [symmetric])
- then have "inverse (fact (n + 2)) * (x^n * x\<^sup>2) \<le> 1/2 * (1/2)^n * (1 * x\<^sup>2)"
- by (rule mult_mono) (rule mult_mono, simp_all add: power_le_one a b)
- then show ?thesis
- unfolding power_add by (simp add: ac_simps del: fact_Suc)
- qed
- have "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))"
- by (intro sums_mult geometric_sums) simp
- then have aux2: "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums x\<^sup>2"
- by simp
have "suminf (\<lambda>n. inverse(fact (n+2)) * (x ^ (n + 2))) \<le> x\<^sup>2"
proof -
+ have "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))"
+ by (intro sums_mult geometric_sums) simp
+ then have sumsx: "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums x\<^sup>2"
+ by simp
have "suminf (\<lambda>n. inverse(fact (n+2)) * (x ^ (n + 2))) \<le> suminf (\<lambda>n. (x\<^sup>2/2) * ((1/2)^n))"
- apply (rule suminf_le)
- apply (rule allI)
- apply (rule aux1)
- apply (rule summable_exp [THEN summable_ignore_initial_segment])
- apply (rule sums_summable)
- apply (rule aux2)
- done
+ proof (intro suminf_le allI)
+ show "inverse (fact (n + 2)) * x ^ (n + 2) \<le> (x\<^sup>2/2) * ((1/2)^n)" for n :: nat
+ proof -
+ have "(2::nat) * 2 ^ n \<le> fact (n + 2)"
+ by (induct n) simp_all
+ then have "real ((2::nat) * 2 ^ n) \<le> real_of_nat (fact (n + 2))"
+ by (simp only: of_nat_le_iff)
+ then have "((2::real) * 2 ^ n) \<le> fact (n + 2)"
+ unfolding of_nat_fact by simp
+ then have "inverse (fact (n + 2)) \<le> inverse ((2::real) * 2 ^ n)"
+ by (rule le_imp_inverse_le) simp
+ then have "inverse (fact (n + 2)) \<le> 1/(2::real) * (1/2)^n"
+ by (simp add: power_inverse [symmetric])
+ then have "inverse (fact (n + 2)) * (x^n * x\<^sup>2) \<le> 1/2 * (1/2)^n * (1 * x\<^sup>2)"
+ by (rule mult_mono) (rule mult_mono, simp_all add: power_le_one a b)
+ then show ?thesis
+ unfolding power_add by (simp add: ac_simps del: fact_Suc)
+ qed
+ show "summable (\<lambda>n. inverse (fact (n + 2)) * x ^ (n + 2))"
+ by (rule summable_exp [THEN summable_ignore_initial_segment])
+ show "summable (\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n)"
+ by (rule sums_summable [OF sumsx])
+ qed
also have "\<dots> = x\<^sup>2"
- by (rule sums_unique [THEN sym]) (rule aux2)
+ by (rule sums_unique [THEN sym]) (rule sumsx)
finally show ?thesis .
qed
then show ?thesis
@@ -2011,16 +1997,14 @@
proof -
have *: "(norm z)\<^sup>2 \<le> norm z * 1"
unfolding power2_eq_square
- apply (rule mult_left_mono)
- using assms
- apply auto
- done
- show ?thesis
- apply (rule order_trans [OF norm_exp])
- apply (rule order_trans [OF exp_bound])
- using assms *
- apply auto
- done
+ by (rule mult_left_mono) (use assms in auto)
+ have "norm (exp z) \<le> exp (norm z)"
+ by (rule norm_exp)
+ also have "\<dots> \<le> 1 + (norm z) + (norm z)\<^sup>2"
+ using assms exp_bound by auto
+ also have "\<dots> \<le> 1 + 2 * norm z"
+ using * by auto
+ finally show ?thesis .
qed
lemma real_exp_bound_lemma: "0 \<le> x \<Longrightarrow> x \<le> 1/2 \<Longrightarrow> exp x \<le> 1 + 2 * x"
@@ -2035,7 +2019,7 @@
have "(1 - x) * (1 + x + x\<^sup>2) = 1 - x^3"
by (simp add: algebra_simps power2_eq_square power3_eq_cube)
also have "\<dots> \<le> 1"
- by (auto simp add: a)
+ by (auto simp: a)
finally have "(1 - x) * (1 + x + x\<^sup>2) \<le> 1" .
moreover have c: "0 < 1 + x + x\<^sup>2"
by (simp add: add_pos_nonneg a)
@@ -2045,7 +2029,7 @@
by (metis a abs_one b exp_bound exp_gt_zero frac_le less_eq_real_def real_sqrt_abs
real_sqrt_pow2_iff real_sqrt_power)
also have "\<dots> = exp (- x)"
- by (auto simp add: exp_minus divide_inverse)
+ by (auto simp: exp_minus divide_inverse)
finally have "1 - x \<le> exp (- x)" .
also have "1 - x = exp (ln (1 - x))"
by (metis b diff_0 exp_ln_iff less_iff_diff_less_0 minus_diff_eq)
@@ -2056,21 +2040,22 @@
lemma exp_ge_add_one_self [simp]: "1 + x \<le> exp x"
for x :: real
- apply (cases "0 \<le> x")
- apply (erule exp_ge_add_one_self_aux)
- apply (cases "x \<le> -1")
- apply (subgoal_tac "1 + x \<le> 0")
- apply (erule order_trans)
- apply simp
- apply simp
- apply (subgoal_tac "1 + x = exp (ln (1 + x))")
- apply (erule ssubst)
- apply (subst exp_le_cancel_iff)
- apply (subgoal_tac "ln (1 - (- x)) \<le> - (- x)")
- apply simp
- apply (rule ln_one_minus_pos_upper_bound)
- apply auto
- done
+proof (cases "0 \<le> x \<or> x \<le> -1")
+ case True
+ then show ?thesis
+ apply (rule disjE)
+ apply (simp add: exp_ge_add_one_self_aux)
+ using exp_ge_zero order_trans real_add_le_0_iff by blast
+next
+ case False
+ then have ln1: "ln (1 + x) \<le> x"
+ using ln_one_minus_pos_upper_bound [of "-x"] by simp
+ have "1 + x = exp (ln (1 + x))"
+ using False by auto
+ also have "\<dots> \<le> exp x"
+ by (simp add: ln1)
+ finally show ?thesis .
+qed
lemma ln_one_plus_pos_lower_bound:
fixes x :: real
@@ -2104,11 +2089,7 @@
proof -
from b have c: "x < 1" by auto
then have "ln (1 - x) = - ln (1 + x / (1 - x))"
- apply (subst ln_inverse [symmetric])
- apply (simp add: field_simps)
- apply (rule arg_cong [where f=ln])
- apply (simp add: field_simps)
- done
+ by (auto simp: ln_inverse [symmetric] field_simps intro: arg_cong [where f=ln])
also have "- (x / (1 - x)) \<le> \<dots>"
proof -
have "ln (1 + x / (1 - x)) \<le> x / (1 - x)"
@@ -2130,11 +2111,7 @@
lemma ln_add_one_self_le_self2:
fixes x :: real
shows "-1 < x \<Longrightarrow> ln (1 + x) \<le> x"
- apply (subgoal_tac "ln (1 + x) \<le> ln (exp x)")
- apply simp
- apply (subst ln_le_cancel_iff)
- apply auto
- done
+ by (metis diff_gt_0_iff_gt diff_minus_eq_add exp_ge_add_one_self exp_le_cancel_iff exp_ln minus_less_iff)
lemma abs_ln_one_plus_x_minus_x_bound_nonneg:
fixes x :: real
@@ -2164,31 +2141,28 @@
assumes a: "-(1 / 2) \<le> x" and b: "x \<le> 0"
shows "\<bar>ln (1 + x) - x\<bar> \<le> 2 * x\<^sup>2"
proof -
+ have *: "- (-x) - 2 * (-x)\<^sup>2 \<le> ln (1 - (- x))"
+ by (metis a b diff_zero ln_one_minus_pos_lower_bound minus_diff_eq neg_le_iff_le)
have "\<bar>ln (1 + x) - x\<bar> = x - ln (1 - (- x))"
- apply (subst abs_of_nonpos)
- apply simp
- apply (rule ln_add_one_self_le_self2)
- using a apply auto
- done
+ using a ln_add_one_self_le_self2 [of x] by (simp add: abs_if)
also have "\<dots> \<le> 2 * x\<^sup>2"
- apply (subgoal_tac "- (-x) - 2 * (-x)\<^sup>2 \<le> ln (1 - (- x))")
- apply (simp add: algebra_simps)
- apply (rule ln_one_minus_pos_lower_bound)
- using a b apply auto
- done
+ using * by (simp add: algebra_simps)
finally show ?thesis .
qed
lemma abs_ln_one_plus_x_minus_x_bound:
fixes x :: real
- shows "\<bar>x\<bar> \<le> 1 / 2 \<Longrightarrow> \<bar>ln (1 + x) - x\<bar> \<le> 2 * x\<^sup>2"
- apply (cases "0 \<le> x")
- apply (rule order_trans)
- apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg)
- apply auto
- apply (rule abs_ln_one_plus_x_minus_x_bound_nonpos)
- apply auto
- done
+ assumes "\<bar>x\<bar> \<le> 1 / 2"
+ shows "\<bar>ln (1 + x) - x\<bar> \<le> 2 * x\<^sup>2"
+proof (cases "0 \<le> x")
+ case True
+ then show ?thesis
+ using abs_ln_one_plus_x_minus_x_bound_nonneg assms by fastforce
+next
+ case False
+ then show ?thesis
+ using abs_ln_one_plus_x_minus_x_bound_nonpos assms by auto
+qed
lemma ln_x_over_x_mono:
fixes x :: real
@@ -2214,13 +2188,7 @@
using a by simp
also have "\<dots> = (y - x) * ln (exp 1)" by simp
also have "\<dots> \<le> (y - x) * ln x"
- apply (rule mult_left_mono)
- apply (subst ln_le_cancel_iff)
- apply fact
- apply (rule a)
- apply (rule x)
- using x apply simp
- done
+ using a x exp_total of_nat_1 x(1) by (fastforce intro: mult_left_mono)
also have "\<dots> = y * ln x - x * ln x"
by (rule left_diff_distrib)
finally have "x * ln y \<le> y * ln x"
@@ -2303,7 +2271,7 @@
also from assms False have "ln (1 + x / real n) \<le> x / real n"
by (intro ln_add_one_self_le_self2) (simp_all add: field_simps)
with assms have "exp (of_nat n * ln (1 + x / of_nat n)) \<le> exp x"
- by (simp add: field_simps del: exp_of_nat_mult)
+ by (simp add: field_simps)
finally show ?thesis .
next
case True
@@ -2321,17 +2289,12 @@
fix r :: real
assume "0 < r"
have "exp x < r" if "x < ln r" for x
- proof -
- from that have "exp x < exp (ln r)"
- by simp
- with \<open>0 < r\<close> show ?thesis
- by simp
- qed
+ by (metis \<open>0 < r\<close> exp_less_mono exp_ln that)
then show "\<exists>k. \<forall>n<k. exp n < r" by auto
qed
lemma exp_at_top: "LIM x at_top. exp x :: real :> at_top"
- by (rule filterlim_at_top_at_top[where Q="\<lambda>x. True" and P="\<lambda>x. 0 < x" and g="ln"])
+ by (rule filterlim_at_top_at_top[where Q="\<lambda>x. True" and P="\<lambda>x. 0 < x" and g=ln])
(auto intro: eventually_gt_at_top)
lemma lim_exp_minus_1: "((\<lambda>z::'a. (exp(z) - 1) / z) \<longlongrightarrow> 1) (at 0)"
@@ -2344,11 +2307,11 @@
qed
lemma ln_at_0: "LIM x at_right 0. ln (x::real) :> at_bot"
- by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
+ by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g=exp])
(auto simp: eventually_at_filter)
lemma ln_at_top: "LIM x at_top. ln (x::real) :> at_top"
- by (rule filterlim_at_top_at_top[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
+ by (rule filterlim_at_top_at_top[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g=exp])
(auto intro: eventually_gt_at_top)
lemma filtermap_ln_at_top: "filtermap (ln::real \<Rightarrow> real) at_top = at_top"
@@ -2423,7 +2386,7 @@
case False
have "-x \<le> (exp(-x) - inverse(exp(-x))) / 2"
by (meson False linear neg_le_0_iff_le real_le_x_sinh)
- also have "... \<le> \<bar>(exp x - inverse (exp x)) / 2\<bar>"
+ also have "\<dots> \<le> \<bar>(exp x - inverse (exp x)) / 2\<bar>"
by (metis (no_types, hide_lams) abs_divide abs_le_iff abs_minus_cancel
add.inverse_inverse exp_minus minus_diff_eq order_refl)
finally show ?thesis
@@ -2620,8 +2583,7 @@
lemma log_less_cancel_iff [simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> log a x < log a y \<longleftrightarrow> x < y"
apply safe
apply (rule_tac [2] powr_less_cancel)
- apply (drule_tac a = "log a x" in powr_less_mono)
- apply auto
+ apply (drule_tac a = "log a x" in powr_less_mono, auto)
done
lemma log_inj:
@@ -2742,7 +2704,7 @@
by(simp add: less_powr_iff)
lemma floor_log_eq_powr_iff: "x > 0 \<Longrightarrow> b > 1 \<Longrightarrow> \<lfloor>log b x\<rfloor> = k \<longleftrightarrow> b powr k \<le> x \<and> x < b powr (k + 1)"
- by (auto simp add: floor_eq_iff powr_le_iff less_powr_iff)
+ by (auto simp: floor_eq_iff powr_le_iff less_powr_iff)
lemma floor_log_nat_eq_powr_iff: fixes b n k :: nat
shows "\<lbrakk> b \<ge> 2; k > 0 \<rbrakk> \<Longrightarrow>
@@ -2761,7 +2723,7 @@
lemma ceiling_log_eq_powr_iff: "\<lbrakk> x > 0; b > 1 \<rbrakk>
\<Longrightarrow> \<lceil>log b x\<rceil> = int k + 1 \<longleftrightarrow> b powr k < x \<and> x \<le> b powr (k + 1)"
-by (auto simp add: ceiling_eq_iff powr_less_iff le_powr_iff)
+by (auto simp: ceiling_eq_iff powr_less_iff le_powr_iff)
lemma ceiling_log_nat_eq_powr_iff: fixes b n k :: nat
shows "\<lbrakk> b \<ge> 2; k > 0 \<rbrakk> \<Longrightarrow>
@@ -2809,7 +2771,7 @@
have "n \<le> 2*?m" by arith
also have "2*?m \<le> 2 ^ ((i+1)+1)" using i(2) by simp
finally have *: "n \<le> \<dots>" .
- have "2^(i+1) < n" using i(1) by (auto simp add: less_Suc_eq_0_disj)
+ have "2^(i+1) < n" using i(1) by (auto simp: less_Suc_eq_0_disj)
from ceiling_log_nat_eq_if[OF this *] ceiling_log_nat_eq_if[OF i]
show ?thesis by simp
qed
@@ -2885,7 +2847,7 @@
shows "n = log b (real m)"
proof -
have "n = log b (b ^ n)" using assms(2) by (simp add: log_nat_power)
- also have "\<dots> = log b m" using assms by (simp)
+ also have "\<dots> = log b m" using assms by simp
finally show ?thesis .
qed
@@ -2907,16 +2869,10 @@
lemma ln_bound: "0 < x \<Longrightarrow> ln x \<le> x" for x :: real
using ln_le_minus_one by force
-lemma powr_mono: "a \<le> b \<Longrightarrow> 1 \<le> x \<Longrightarrow> x powr a \<le> x powr b"
- for x :: real
- apply (cases "x = 1")
- apply simp
- apply (cases "a = b")
- apply simp
- apply (rule order_less_imp_le)
- apply (rule powr_less_mono)
- apply auto
- done
+lemma powr_mono:
+ fixes x :: real
+ assumes "a \<le> b" and "1 \<le> x" shows "x powr a \<le> x powr b"
+ using assms less_eq_real_def by auto
lemma ge_one_powr_ge_zero: "1 \<le> x \<Longrightarrow> 0 \<le> a \<Longrightarrow> 1 \<le> x powr a"
for x :: real
@@ -2932,20 +2888,7 @@
lemma powr_mono2: "x powr a \<le> y powr a" if "0 \<le> a" "0 \<le> x" "x \<le> y"
for x :: real
-proof (cases "a = 0")
- case True
- with that show ?thesis by simp
-next
- case False show ?thesis
- proof (cases "x = y")
- case True
- then show ?thesis by simp
- next
- case False
- then show ?thesis
- by (metis dual_order.strict_iff_order powr_less_mono2 that \<open>a \<noteq> 0\<close>)
- qed
-qed
+ using less_eq_real_def powr_less_mono2 that by auto
lemma powr_le1: "0 \<le> a \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> x powr a \<le> 1"
for x :: real
@@ -2959,7 +2902,7 @@
from assms have "x powr - a \<le> y powr - a"
by (intro powr_mono2) simp_all
with assms show ?thesis
- by (auto simp add: powr_minus field_simps)
+ by (auto simp: powr_minus field_simps)
qed
lemma powr_mono_both:
@@ -3034,7 +2977,7 @@
proof (intro filterlim_If)
have "filterlim f (principal {0<..}) (inf F (principal {z. f z \<noteq> 0}))"
using \<open>eventually (\<lambda>x. f x \<ge> 0) F\<close>
- by (auto simp add: filterlim_iff eventually_inf_principal
+ by (auto simp: filterlim_iff eventually_inf_principal
eventually_principal elim: eventually_mono)
moreover have "filterlim f (nhds a) (inf F (principal {z. f z \<noteq> 0}))"
by (rule tendsto_mono[OF _ f]) simp_all
@@ -3189,7 +3132,7 @@
have "((\<lambda>y. ln (1 + x * y)::real) has_real_derivative 1 * x) (at 0)"
by (auto intro!: derivative_eq_intros)
then have "((\<lambda>y. ln (1 + x * y) / y) \<longlongrightarrow> x) (at 0)"
- by (auto simp add: has_field_derivative_def field_has_derivative_at)
+ by (auto simp: has_field_derivative_def field_has_derivative_at)
then have *: "((\<lambda>y. exp (ln (1 + x * y) / y)) \<longlongrightarrow> exp x) (at 0)"
by (rule tendsto_intros)
then show ?thesis
@@ -3216,13 +3159,7 @@
proof (rule filterlim_mono_eventually)
from reals_Archimedean2 [of "\<bar>x\<bar>"] obtain n :: nat where *: "real n > \<bar>x\<bar>" ..
then have "eventually (\<lambda>n :: nat. 0 < 1 + x / real n) at_top"
- apply (intro eventually_sequentiallyI [of n])
- apply (cases "x \<ge> 0")
- apply (rule add_pos_nonneg)
- apply (auto intro: divide_nonneg_nonneg)
- apply (subgoal_tac "x / real xa > - 1")
- apply (auto simp add: field_simps)
- done
+ by (intro eventually_sequentiallyI [of n]) (auto simp: divide_simps)
then show "eventually (\<lambda>n. (1 + x / n) powr n = (1 + x / n) ^ n) at_top"
by (rule eventually_mono) (erule powr_realpow)
show "(\<lambda>n. (1 + x / real n) powr real n) \<longlonglongrightarrow> exp x"
@@ -3717,23 +3654,24 @@
by (simp add: cos_coeff_def ac_simps)
qed
-lemmas realpow_num_eq_if = power_eq_if
-
-lemma sumr_pos_lt_pair:
+lemma sum_pos_lt_pair:
fixes f :: "nat \<Rightarrow> real"
- shows "summable f \<Longrightarrow>
- (\<And>d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc (Suc 0) * d) + 1))) \<Longrightarrow>
- sum f {..<k} < suminf f"
- apply (simp only: One_nat_def)
- apply (subst suminf_split_initial_segment [where k=k])
- apply assumption
- apply simp
- apply (drule_tac k=k in summable_ignore_initial_segment)
- apply (drule_tac k="Suc (Suc 0)" in sums_group [OF summable_sums])
- apply simp
- apply simp
- apply (metis (no_types, lifting) add.commute suminf_pos summable_def sums_unique)
- done
+ assumes f: "summable f" and fplus: "\<And>d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc (Suc 0) * d) + 1))"
+ shows "sum f {..<k} < suminf f"
+proof -
+ have "(\<lambda>n. \<Sum>n = n * Suc (Suc 0)..<n * Suc (Suc 0) + Suc (Suc 0). f (n + k))
+ sums (\<Sum>n. f (n + k))"
+ proof (rule sums_group)
+ show "(\<lambda>n. f (n + k)) sums (\<Sum>n. f (n + k))"
+ by (simp add: f summable_iff_shift summable_sums)
+ qed auto
+ with fplus have "0 < (\<Sum>n. f (n + k))"
+ apply (simp add: add.commute)
+ apply (metis (no_types, lifting) suminf_pos summable_def sums_unique)
+ done
+ then show ?thesis
+ by (simp add: f suminf_minus_initial_segment)
+qed
lemma cos_two_less_zero [simp]: "cos 2 < (0::real)"
proof -
@@ -3744,7 +3682,7 @@
then have sm: "summable (\<lambda>n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
by (rule sums_summable)
have "0 < (\<Sum>n<Suc (Suc (Suc 0)). - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
- by (simp add: fact_num_eq_if realpow_num_eq_if)
+ by (simp add: fact_num_eq_if power_eq_if)
moreover have "(\<Sum>n<Suc (Suc (Suc 0)). - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n)))) <
(\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
proof -
@@ -3759,7 +3697,7 @@
by (simp add: inverse_eq_divide less_divide_eq)
}
then show ?thesis
- by (force intro!: sumr_pos_lt_pair [OF sm] simp add: divide_inverse algebra_simps)
+ by (force intro!: sum_pos_lt_pair [OF sm] simp add: divide_inverse algebra_simps)
qed
ultimately have "0 < (\<Sum>n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
by (rule order_less_trans)
@@ -3780,16 +3718,26 @@
fix x y :: real
assume x: "0 \<le> x \<and> x \<le> 2 \<and> cos x = 0"
assume y: "0 \<le> y \<and> y \<le> 2 \<and> cos y = 0"
- have [simp]: "\<forall>x::real. cos differentiable (at x)"
+ have cosd[simp]: "\<forall>x::real. cos differentiable (at x)"
unfolding real_differentiable_def by (auto intro: DERIV_cos)
- from x y less_linear [of x y] show "x = y"
- apply auto
- apply (drule_tac f = cos in Rolle)
- apply (drule_tac [5] f = cos in Rolle)
- apply (auto dest!: DERIV_cos [THEN DERIV_unique])
- apply (metis order_less_le_trans less_le sin_gt_zero_02)
- apply (metis order_less_le_trans less_le sin_gt_zero_02)
- done
+ show "x = y"
+ proof (cases x y rule: linorder_cases)
+ case less
+ then obtain z where "x < z" "z < y" "(cos has_real_derivative 0) (at z)"
+ using Rolle by (metis cosd isCont_cos x y)
+ then have "sin z = 0"
+ using DERIV_cos DERIV_unique neg_equal_0_iff_equal by blast
+ then show ?thesis
+ by (metis \<open>x < z\<close> \<open>z < y\<close> x y order_less_le_trans less_le sin_gt_zero_02)
+ next
+ case greater
+ then obtain z where "y < z" "z < x" "(cos has_real_derivative 0) (at z)"
+ using Rolle by (metis cosd isCont_cos x y)
+ then have "sin z = 0"
+ using DERIV_cos DERIV_unique neg_equal_0_iff_equal by blast
+ then show ?thesis
+ by (metis \<open>y < z\<close> \<open>z < x\<close> x y order_less_le_trans less_le sin_gt_zero_02)
+ qed auto
qed
lemma pi_half: "pi/2 = (THE x. 0 \<le> x \<and> x \<le> 2 \<and> cos x = 0)"
@@ -3804,19 +3752,23 @@
nonzero_of_real_divide of_real_0 of_real_numeral)
lemma pi_half_gt_zero [simp]: "0 < pi / 2"
- apply (rule order_le_neq_trans)
- apply (simp add: pi_half cos_is_zero [THEN theI'])
- apply (metis cos_pi_half cos_zero zero_neq_one)
- done
+proof -
+ have "0 \<le> pi / 2"
+ by (simp add: pi_half cos_is_zero [THEN theI'])
+ then show ?thesis
+ by (metis cos_pi_half cos_zero less_eq_real_def one_neq_zero)
+qed
lemmas pi_half_neq_zero [simp] = pi_half_gt_zero [THEN less_imp_neq, symmetric]
lemmas pi_half_ge_zero [simp] = pi_half_gt_zero [THEN order_less_imp_le]
lemma pi_half_less_two [simp]: "pi / 2 < 2"
- apply (rule order_le_neq_trans)
- apply (simp add: pi_half cos_is_zero [THEN theI'])
- apply (metis cos_pi_half cos_two_neq_zero)
- done
+proof -
+ have "pi / 2 \<le> 2"
+ by (simp add: pi_half cos_is_zero [THEN theI'])
+ then show ?thesis
+ by (metis cos_pi_half cos_two_neq_zero le_less)
+qed
lemmas pi_half_neq_two [simp] = pi_half_less_two [THEN less_imp_neq]
lemmas pi_half_le_two [simp] = pi_half_less_two [THEN order_less_imp_le]
@@ -4098,12 +4050,14 @@
and uniq: "\<And>x'. 0 \<le> x' \<Longrightarrow> x' \<le> pi \<Longrightarrow> cos x' = y \<Longrightarrow> x' = x "
by blast
show ?thesis
- apply (simp add: sin_cos_eq)
- apply (rule ex1I [where a="pi/2 - x"])
- apply (cut_tac [2] x'="pi/2 - xa" in uniq)
- using x
- apply auto
- done
+ unfolding sin_cos_eq
+ proof (rule ex1I [where a="pi/2 - x"])
+ show "- (pi / 2) \<le> z \<and>
+ z \<le> pi / 2 \<and>
+ cos (of_real pi / 2 - z) = y \<Longrightarrow>
+ z = pi / 2 - x" for z
+ using uniq [of "pi/2 -z"] by auto
+ qed (use x in auto)
qed
lemma cos_zero_lemma:
@@ -4114,11 +4068,12 @@
using floor_correct [of "x/pi"]
by (simp add: add.commute divide_less_eq)
obtain n where "real n * pi \<le> x" "x < real (Suc n) * pi"
- apply (rule that [of "nat \<lfloor>x/pi\<rfloor>"])
- using assms
- apply (simp_all add: xle)
- apply (metis floor_less_iff less_irrefl mult_imp_div_pos_less not_le pi_gt_zero)
- done
+ proof
+ show "real (nat \<lfloor>x / pi\<rfloor>) * pi \<le> x"
+ using assms floor_divide_lower [of pi x] by auto
+ show "x < real (Suc (nat \<lfloor>x / pi\<rfloor>)) * pi"
+ using assms floor_divide_upper [of pi x] by (simp add: xle)
+ qed
then have x: "0 \<le> x - n * pi" "(x - n * pi) \<le> pi" "cos (x - n * pi) = 0"
by (auto simp: algebra_simps cos_diff assms)
then have "\<exists>!x. 0 \<le> x \<and> x \<le> pi \<and> cos x = 0"
@@ -4175,7 +4130,7 @@
assume "cos x = 0"
then show "\<exists>n. odd n \<and> x = of_int n * (pi / 2)"
unfolding cos_zero_iff
- apply (auto simp add: cos_zero_iff)
+ apply (auto simp: cos_zero_iff)
apply (metis even_of_nat of_int_of_nat_eq)
apply (rule_tac x="- (int n)" in exI)
apply simp
@@ -4184,18 +4139,14 @@
fix n :: int
assume "odd n"
then show "cos (of_int n * (pi / 2)) = 0"
- apply (simp add: cos_zero_iff)
- apply (cases n rule: int_cases2)
- apply simp_all
- done
+ by (cases n rule: int_cases2, simp_all add: cos_zero_iff)
qed
lemma sin_zero_iff_int: "sin x = 0 \<longleftrightarrow> (\<exists>n. even n \<and> x = of_int n * (pi/2))"
proof safe
assume "sin x = 0"
then show "\<exists>n. even n \<and> x = of_int n * (pi / 2)"
- apply (simp add: sin_zero_iff)
- apply safe
+ apply (simp add: sin_zero_iff, safe)
apply (metis even_of_nat of_int_of_nat_eq)
apply (rule_tac x="- (int n)" in exI)
apply simp
@@ -4205,8 +4156,7 @@
assume "even n"
then show "sin (of_int n * (pi / 2)) = 0"
apply (simp add: sin_zero_iff)
- apply (cases n rule: int_cases2)
- apply simp_all
+ apply (cases n rule: int_cases2, simp_all)
done
qed
@@ -4339,8 +4289,7 @@
lemma cos_3over2_pi [simp]: "cos (3/2*pi) = 0"
apply (subgoal_tac "cos (pi + pi/2) = 0")
apply simp
- apply (subst cos_add)
- apply simp
+ apply (subst cos_add, simp)
done
lemma sin_2npi [simp]: "sin (2 * real n * pi) = 0"
@@ -4350,8 +4299,7 @@
lemma sin_3over2_pi [simp]: "sin (3/2*pi) = - 1"
apply (subgoal_tac "sin (pi + pi/2) = - 1")
apply simp
- apply (subst sin_add)
- apply simp
+ apply (subst sin_add, simp)
done
lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
@@ -4499,8 +4447,7 @@
apply (rule power2_eq_imp_eq)
apply (simp add: cos_squared_eq sin_60 power_divide)
apply (rule cos_ge_zero)
- apply (rule order_trans [where y=0])
- apply simp_all
+ apply (rule order_trans [where y=0], simp_all)
done
lemma sin_30: "sin (pi / 6) = 1 / 2"
@@ -4640,28 +4587,24 @@
lemma lemma_tan_total: "0 < y \<Longrightarrow> \<exists>x. 0 < x \<and> x < pi/2 \<and> y < tan x"
apply (insert LIM_cos_div_sin)
apply (simp only: LIM_eq)
- apply (drule_tac x = "inverse y" in spec)
- apply safe
+ apply (drule_tac x = "inverse y" in spec, safe)
apply force
- apply (drule_tac ?d1.0 = s in pi_half_gt_zero [THEN [2] field_lbound_gt_zero])
- apply safe
+ apply (drule_tac ?d1.0 = s in pi_half_gt_zero [THEN [2] field_lbound_gt_zero], safe)
apply (rule_tac x = "(pi/2) - e" in exI)
apply (simp (no_asm_simp))
apply (drule_tac x = "(pi/2) - e" in spec)
- apply (auto simp add: tan_def sin_diff cos_diff)
+ apply (auto simp: tan_def sin_diff cos_diff)
apply (rule inverse_less_iff_less [THEN iffD1])
- apply (auto simp add: divide_inverse)
+ apply (auto simp: divide_inverse)
apply (rule mult_pos_pos)
apply (subgoal_tac [3] "0 < sin e \<and> 0 < cos e")
apply (auto intro: cos_gt_zero sin_gt_zero2 simp: mult.commute)
done
lemma tan_total_pos: "0 \<le> y \<Longrightarrow> \<exists>x. 0 \<le> x \<and> x < pi/2 \<and> tan x = y"
- apply (frule order_le_imp_less_or_eq)
- apply safe
+ apply (frule order_le_imp_less_or_eq, safe)
prefer 2 apply force
- apply (drule lemma_tan_total)
- apply safe
+ apply (drule lemma_tan_total, safe)
apply (cut_tac f = tan and a = 0 and b = x and y = y in IVT_objl)
apply (auto intro!: DERIV_tan [THEN DERIV_isCont])
apply (drule_tac y = xa in order_le_imp_less_or_eq)
@@ -4669,21 +4612,17 @@
done
lemma lemma_tan_total1: "\<exists>x. -(pi/2) < x \<and> x < (pi/2) \<and> tan x = y"
- apply (insert linorder_linear [of 0 y])
- apply safe
+ apply (insert linorder_linear [of 0 y], safe)
apply (drule tan_total_pos)
- apply (cut_tac [2] y="-y" in tan_total_pos)
- apply safe
+ apply (cut_tac [2] y="-y" in tan_total_pos, safe)
apply (rule_tac [3] x = "-x" in exI)
apply (auto del: exI intro!: exI)
done
lemma tan_total: "\<exists>! x. -(pi/2) < x \<and> x < (pi/2) \<and> tan x = y"
- apply (insert lemma_tan_total1 [where y = y])
- apply auto
+ apply (insert lemma_tan_total1 [where y = y], auto)
apply hypsubst_thin
- apply (cut_tac x = xa and y = y in linorder_less_linear)
- apply auto
+ apply (cut_tac x = xa and y = y in linorder_less_linear, auto)
apply (subgoal_tac [2] "\<exists>z. y < z \<and> z < xa \<and> DERIV tan z :> 0")
apply (subgoal_tac "\<exists>z. xa < z \<and> z < y \<and> DERIV tan z :> 0")
apply (rule_tac [4] Rolle)
@@ -4812,7 +4751,7 @@
lemma sin_tan: "\<bar>x\<bar> < pi/2 \<Longrightarrow> sin x = tan x / sqrt (1 + tan x ^ 2)"
using cos_gt_zero [of "x"] cos_gt_zero [of "-x"]
- by (force simp add: divide_simps tan_def real_sqrt_divide abs_if split: if_split_asm)
+ by (force simp: divide_simps tan_def real_sqrt_divide abs_if split: if_split_asm)
lemma tan_mono_le: "-(pi/2) < x \<Longrightarrow> x \<le> y \<Longrightarrow> y < pi/2 \<Longrightarrow> tan x \<le> tan y"
using less_eq_real_def tan_monotone by auto
@@ -4948,21 +4887,17 @@
lemma arcsin_lt_bounded: "- 1 < y \<Longrightarrow> y < 1 \<Longrightarrow> - (pi/2) < arcsin y \<and> arcsin y < pi/2"
apply (frule order_less_imp_le)
apply (frule_tac y = y in order_less_imp_le)
- apply (frule arcsin_bounded)
- apply safe
+ apply (frule arcsin_bounded, safe)
apply simp
apply (drule_tac y = "arcsin y" in order_le_imp_less_or_eq)
- apply (drule_tac [2] y = "pi/2" in order_le_imp_less_or_eq)
- apply safe
- apply (drule_tac [!] f = sin in arg_cong)
- apply auto
+ apply (drule_tac [2] y = "pi/2" in order_le_imp_less_or_eq, safe)
+ apply (drule_tac [!] f = sin in arg_cong, auto)
done
lemma arcsin_sin: "- (pi/2) \<le> x \<Longrightarrow> x \<le> pi/2 \<Longrightarrow> arcsin (sin x) = x"
apply (unfold arcsin_def)
apply (rule the1_equality)
- apply (rule sin_total)
- apply auto
+ apply (rule sin_total, auto)
done
lemma arcsin_0 [simp]: "arcsin 0 = 0"
@@ -5001,13 +4936,10 @@
lemma arccos_lt_bounded: "- 1 < y \<Longrightarrow> y < 1 \<Longrightarrow> 0 < arccos y \<and> arccos y < pi"
apply (frule order_less_imp_le)
apply (frule_tac y = y in order_less_imp_le)
- apply (frule arccos_bounded)
- apply auto
+ apply (frule arccos_bounded, auto)
apply (drule_tac y = "arccos y" in order_le_imp_less_or_eq)
- apply (drule_tac [2] y = pi in order_le_imp_less_or_eq)
- apply auto
- apply (drule_tac [!] f = cos in arg_cong)
- apply auto
+ apply (drule_tac [2] y = pi in order_le_imp_less_or_eq, auto)
+ apply (drule_tac [!] f = cos in arg_cong, auto)
done
lemma arccos_cos: "0 \<le> x \<Longrightarrow> x \<le> pi \<Longrightarrow> arccos (cos x) = x"
@@ -5024,10 +4956,8 @@
apply (erule (1) arcsin_lbound)
apply (erule (1) arcsin_ubound)
apply simp
- apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 \<le> 1\<^sup>2")
- apply simp
- apply (rule power_mono)
- apply simp
+ apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 \<le> 1\<^sup>2", simp)
+ apply (rule power_mono, simp)
apply simp
done
@@ -5039,10 +4969,8 @@
apply (erule (1) arccos_lbound)
apply (erule (1) arccos_ubound)
apply simp
- apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 \<le> 1\<^sup>2")
- apply simp
- apply (rule power_mono)
- apply simp
+ apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 \<le> 1\<^sup>2", simp)
+ apply (rule power_mono, simp)
apply simp
done
@@ -5123,7 +5051,7 @@
for x :: "'a::{real_normed_field,banach,field}"
apply (rule power_inverse [THEN subst])
apply (rule_tac c1 = "(cos x)\<^sup>2" in mult_right_cancel [THEN iffD1])
- apply (auto simp add: tan_def field_simps)
+ apply (auto simp: tan_def field_simps)
done
lemma arctan_less_iff: "arctan x < arctan y \<longleftrightarrow> x < y"
@@ -5199,10 +5127,8 @@
by (auto simp: continuous_on_eq_continuous_at subset_eq)
lemma isCont_arctan: "isCont arctan x"
- apply (rule arctan_lbound [of x, THEN dense, THEN exE])
- apply clarify
- apply (rule arctan_ubound [of x, THEN dense, THEN exE])
- apply clarify
+ apply (rule arctan_lbound [of x, THEN dense, THEN exE], clarify)
+ apply (rule arctan_ubound [of x, THEN dense, THEN exE], clarify)
apply (subgoal_tac "isCont arctan (tan (arctan x))")
apply (simp add: arctan)
apply (erule (1) isCont_inverse_function2 [where f=tan])
@@ -5224,10 +5150,8 @@
apply (rule DERIV_inverse_function [where f=sin and a="-1" and b=1])
apply (rule DERIV_cong [OF DERIV_sin])
apply (simp add: cos_arcsin)
- apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 < 1\<^sup>2")
- apply simp
- apply (rule power_strict_mono)
- apply simp
+ apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 < 1\<^sup>2", simp)
+ apply (rule power_strict_mono, simp)
apply simp
apply simp
apply assumption
@@ -5240,10 +5164,8 @@
apply (rule DERIV_inverse_function [where f=cos and a="-1" and b=1])
apply (rule DERIV_cong [OF DERIV_cos])
apply (simp add: sin_arccos)
- apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 < 1\<^sup>2")
- apply simp
- apply (rule power_strict_mono)
- apply simp
+ apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 < 1\<^sup>2", simp)
+ apply (rule power_strict_mono, simp)
apply simp
apply simp
apply assumption
@@ -5258,8 +5180,7 @@
apply (rule cos_arctan_not_zero)
apply (simp_all add: add_pos_nonneg arctan isCont_arctan)
apply (simp add: arctan power_inverse [symmetric] tan_sec [symmetric])
- apply (subgoal_tac "0 < 1 + x\<^sup>2")
- apply simp
+ apply (subgoal_tac "0 < 1 + x\<^sup>2", simp)
apply (simp_all add: add_pos_nonneg arctan isCont_arctan)
done
@@ -5436,7 +5357,7 @@
lemma arccos_cos_eq_abs:
assumes "\<bar>\<theta>\<bar> \<le> pi"
shows "arccos (cos \<theta>) = \<bar>\<theta>\<bar>"
- unfolding arccos_def
+ unfolding arccos_def
proof (intro the_equality conjI; clarify?)
show "cos \<bar>\<theta>\<bar> = cos \<theta>"
by (simp add: abs_real_def)
@@ -5453,9 +5374,9 @@
by (auto simp: k_def abs_if algebra_simps)
have "arccos (cos \<theta>) = arccos (cos (\<theta> - of_int k * (2 * pi)))"
using cos_int_2pin sin_int_2pin by (simp add: cos_diff mult.commute)
- also have "... = \<bar>\<theta> - of_int k * (2 * pi)\<bar>"
+ also have "\<dots> = \<bar>\<theta> - of_int k * (2 * pi)\<bar>"
using arccos_cos_eq_abs lepi by blast
- finally show ?thesis
+ finally show ?thesis
using that by metis
qed
@@ -5486,7 +5407,7 @@
then have "(\<lambda>j. \<Theta> + ((\<theta> j - \<Theta>) - of_int (k j) * (2 * pi))) \<longlonglongrightarrow> \<Theta> + 0"
by (rule tendsto_add [OF tendsto_const])
with that show ?thesis
- by (auto simp: )
+ by auto
qed
subsection \<open>Machin's formula\<close>
@@ -5501,7 +5422,7 @@
show "- (pi / 4) < arctan x \<and> arctan x < pi / 4 \<and> tan (arctan x) = x"
unfolding arctan_one [symmetric] arctan_minus [symmetric]
unfolding arctan_less_iff
- using assms by (auto simp add: arctan)
+ using assms by (auto simp: arctan)
qed
lemma arctan_add:
@@ -5830,11 +5751,11 @@
then have "0 < \<bar>x\<bar>" and "- \<bar>x\<bar> < \<bar>x\<bar>"
by auto
have "suminf (?c (- \<bar>x\<bar>)) - arctan (- \<bar>x\<bar>) = suminf (?c 0) - arctan 0"
- by (rule suminf_eq_arctan_bounded[where x1="0" and a1="-\<bar>x\<bar>" and b1="\<bar>x\<bar>", symmetric])
+ by (rule suminf_eq_arctan_bounded[where x1=0 and a1="-\<bar>x\<bar>" and b1="\<bar>x\<bar>", symmetric])
(simp_all only: \<open>\<bar>x\<bar> < r\<close> \<open>-\<bar>x\<bar> < \<bar>x\<bar>\<close> neg_less_iff_less)
moreover
have "suminf (?c x) - arctan x = suminf (?c (- \<bar>x\<bar>)) - arctan (- \<bar>x\<bar>)"
- by (rule suminf_eq_arctan_bounded[where x1="x" and a1="- \<bar>x\<bar>" and b1="\<bar>x\<bar>"])
+ by (rule suminf_eq_arctan_bounded[where x1=x and a1="- \<bar>x\<bar>" and b1="\<bar>x\<bar>"])
(simp_all only: \<open>\<bar>x\<bar> < r\<close> \<open>- \<bar>x\<bar> < \<bar>x\<bar>\<close> neg_less_iff_less)
ultimately show ?thesis
using suminf_arctan_zero by auto
@@ -6004,14 +5925,13 @@
show "- (pi / 2) < sgn x * pi / 2 - arctan x"
using arctan_bounded [of x] assms
unfolding sgn_real_def
- apply (auto simp add: arctan algebra_simps)
- apply (drule zero_less_arctan_iff [THEN iffD2])
- apply arith
+ apply (auto simp: arctan algebra_simps)
+ apply (drule zero_less_arctan_iff [THEN iffD2], arith)
done
show "sgn x * pi / 2 - arctan x < pi / 2"
using arctan_bounded [of "- x"] assms
unfolding sgn_real_def arctan_minus
- by (auto simp add: algebra_simps)
+ by (auto simp: algebra_simps)
show "tan (sgn x * pi / 2 - arctan x) = 1 / x"
unfolding tan_inverse [of "arctan x", unfolded tan_arctan]
unfolding sgn_real_def
@@ -6055,7 +5975,7 @@
next
case equal
then show ?thesis
- by (force simp add: intro!: cos_zero sin_zero)
+ by (force simp: intro!: cos_zero sin_zero)
next
case greater
with polar_ex1 [where y="-y"] show ?thesis
@@ -6134,7 +6054,7 @@
also have "\<dots> = (\<Sum>(i,j) \<in> (SIGMA i : atMost n. lessThan i). a i * (x - y) * (y^(i - Suc j) * x^j))"
by (simp add: sum.Sigma)
also have "\<dots> = (\<Sum>(j,i) \<in> (SIGMA j : lessThan n. {Suc j..n}). a i * (x - y) * (y^(i - Suc j) * x^j))"
- by (auto simp add: sum.reindex_bij_betw [OF h, symmetric] intro: sum.strong_cong)
+ by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.strong_cong)
also have "\<dots> = (\<Sum>j<n. \<Sum>i=Suc j..n. a i * (x - y) * (y^(i - Suc j) * x^j))"
by (simp add: sum.Sigma)
also have "\<dots> = (x - y) * (\<Sum>j<n. (\<Sum>i=Suc j..n. a i * y^(i - j - 1)) * x^j)"
@@ -6153,11 +6073,10 @@
proof -
have h: "bij_betw (\<lambda>i. i - (j + 1)) {Suc j..n} (lessThan (n-j))"
apply (auto simp: bij_betw_def inj_on_def)
- apply (rule_tac x="x + Suc j" in image_eqI)
- apply (auto simp: )
+ apply (rule_tac x="x + Suc j" in image_eqI, auto)
done
then show ?thesis
- by (auto simp add: sum.reindex_bij_betw [OF h, symmetric] intro: sum.strong_cong)
+ by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.strong_cong)
qed
then show ?thesis
by (simp add: polyfun_diff [OF assms] sum_distrib_right)
@@ -6224,7 +6143,7 @@
by (simp cong: LIM_cong) \<comment> \<open>the case \<open>w = 0\<close> by continuity\<close>
then have "(\<Sum>i\<le>n. c (Suc i) * 0^i) = 0"
using isCont_polynom [of 0 "\<lambda>i. c (Suc i)" n] LIM_unique
- by (force simp add: Limits.isCont_iff)
+ by (force simp: Limits.isCont_iff)
then have "\<And>w. (\<Sum>i\<le>n. c (Suc i) * w^i) = 0"
using w by metis
then have "\<And>i. i \<le> n \<Longrightarrow> c (Suc i) = 0"
@@ -6352,17 +6271,17 @@
shows finite_roots_unity: "finite {z::'a. z^n = 1}"
and card_roots_unity: "card {z::'a. z^n = 1} \<le> n"
using polyfun_rootbound [of "\<lambda>i. if i = 0 then -1 else if i=n then 1 else 0" n n] assms(2)
- by (auto simp add: root_polyfun [OF assms(2)])
+ by (auto simp: root_polyfun [OF assms(2)])
subsection \<open>Hyperbolic functions\<close>
definition sinh :: "'a :: {banach, real_normed_algebra_1} \<Rightarrow> 'a" where
"sinh x = (exp x - exp (-x)) /\<^sub>R 2"
-
+
definition cosh :: "'a :: {banach, real_normed_algebra_1} \<Rightarrow> 'a" where
"cosh x = (exp x + exp (-x)) /\<^sub>R 2"
-
+
definition tanh :: "'a :: {banach, real_normed_field} \<Rightarrow> 'a" where
"tanh x = sinh x / cosh x"
@@ -6409,7 +6328,7 @@
finally show ?thesis .
qed
-
+
lemma sinh_converges: "(\<lambda>n. if even n then 0 else x ^ n /\<^sub>R fact n) sums sinh x"
proof -
have "(\<lambda>n. (x ^ n /\<^sub>R fact n - (-x) ^ n /\<^sub>R fact n) /\<^sub>R 2) sums sinh x"
@@ -6418,7 +6337,7 @@
(\<lambda>n. if even n then 0 else x ^ n /\<^sub>R fact n)" by auto
finally show ?thesis .
qed
-
+
lemma cosh_converges: "(\<lambda>n. if even n then x ^ n /\<^sub>R fact n else 0) sums cosh x"
proof -
have "(\<lambda>n. (x ^ n /\<^sub>R fact n + (-x) ^ n /\<^sub>R fact n) /\<^sub>R 2) sums cosh x"
@@ -6430,7 +6349,7 @@
lemma sinh_0 [simp]: "sinh 0 = 0"
by (simp add: sinh_def)
-
+
lemma cosh_0 [simp]: "cosh 0 = 1"
proof -
have "cosh 0 = (1/2) *\<^sub>R (1 + 1)" by (simp add: cosh_def)
@@ -6455,7 +6374,7 @@
lemma cosh_ln_real: "x > 0 \<Longrightarrow> cosh (ln x :: real) = (x + inverse x) / 2"
by (simp add: cosh_def exp_minus)
-
+
lemma tanh_ln_real: "x > 0 \<Longrightarrow> tanh (ln x :: real) = (x ^ 2 - 1) / (x ^ 2 + 1)"
by (simp add: tanh_def sinh_ln_real cosh_ln_real divide_simps power2_eq_square)
@@ -6464,17 +6383,17 @@
unfolding has_field_derivative_def
using has_derivative_scaleR_right[of f "\<lambda>x. D * x" F c]
by (simp add: mult_scaleR_left [symmetric] del: mult_scaleR_left)
-
-lemma has_field_derivative_sinh [THEN DERIV_chain2, derivative_intros]:
+
+lemma has_field_derivative_sinh [THEN DERIV_chain2, derivative_intros]:
"(sinh has_field_derivative cosh x) (at (x :: 'a :: {banach, real_normed_field}))"
unfolding sinh_def cosh_def by (auto intro!: derivative_eq_intros)
-lemma has_field_derivative_cosh [THEN DERIV_chain2, derivative_intros]:
+lemma has_field_derivative_cosh [THEN DERIV_chain2, derivative_intros]:
"(cosh has_field_derivative sinh x) (at (x :: 'a :: {banach, real_normed_field}))"
unfolding sinh_def cosh_def by (auto intro!: derivative_eq_intros)
-lemma has_field_derivative_tanh [THEN DERIV_chain2, derivative_intros]:
- "cosh x \<noteq> 0 \<Longrightarrow> (tanh has_field_derivative 1 - tanh x ^ 2)
+lemma has_field_derivative_tanh [THEN DERIV_chain2, derivative_intros]:
+ "cosh x \<noteq> 0 \<Longrightarrow> (tanh has_field_derivative 1 - tanh x ^ 2)
(at (x :: 'a :: {banach, real_normed_field}))"
unfolding tanh_def by (auto intro!: derivative_eq_intros simp: power2_eq_square divide_simps)
@@ -6486,7 +6405,7 @@
have "((\<lambda>x. - g x) has_derivative (\<lambda>y. -(Db * y))) (at x within s)"
using assms by (intro derivative_intros)
also have "(\<lambda>y. -(Db * y)) = (\<lambda>x. (-Db) * x)" by (simp add: fun_eq_iff)
- finally have "((\<lambda>x. sinh (g x)) has_derivative
+ finally have "((\<lambda>x. sinh (g x)) has_derivative
(\<lambda>y. (exp (g x) * Db * y - exp (-g x) * (-Db) * y) /\<^sub>R 2)) (at x within s)"
unfolding sinh_def by (intro derivative_intros assms)
also have "(\<lambda>y. (exp (g x) * Db * y - exp (-g x) * (-Db) * y) /\<^sub>R 2) = (\<lambda>y. (cosh (g x) * Db) * y)"
@@ -6502,7 +6421,7 @@
have "((\<lambda>x. - g x) has_derivative (\<lambda>y. -(Db * y))) (at x within s)"
using assms by (intro derivative_intros)
also have "(\<lambda>y. -(Db * y)) = (\<lambda>y. (-Db) * y)" by (simp add: fun_eq_iff)
- finally have "((\<lambda>x. cosh (g x)) has_derivative
+ finally have "((\<lambda>x. cosh (g x)) has_derivative
(\<lambda>y. (exp (g x) * Db * y + exp (-g x) * (-Db) * y) /\<^sub>R 2)) (at x within s)"
unfolding cosh_def by (intro derivative_intros assms)
also have "(\<lambda>y. (exp (g x) * Db * y + exp (-g x) * (-Db) * y) /\<^sub>R 2) = (\<lambda>y. (sinh (g x) * Db) * y)"
@@ -6539,12 +6458,12 @@
lemma sinh_zero_iff: "sinh x = 0 \<longleftrightarrow> exp x \<in> {1, -1}"
by (auto simp: sinh_def field_simps exp_minus power2_eq_square square_eq_1_iff)
-
+
lemma cosh_zero_iff: "cosh x = 0 \<longleftrightarrow> exp x ^ 2 = -1"
by (auto simp: cosh_def exp_minus field_simps power2_eq_square eq_neg_iff_add_eq_0)
lemma cosh_square_eq: "cosh x ^ 2 = sinh x ^ 2 + 1"
- by (simp add: cosh_def sinh_def algebra_simps power2_eq_square exp_add [symmetric]
+ by (simp add: cosh_def sinh_def algebra_simps power2_eq_square exp_add [symmetric]
scaleR_conv_of_real)
lemma sinh_square_eq: "sinh x ^ 2 = cosh x ^ 2 - 1"
@@ -6557,15 +6476,15 @@
by (simp add: sinh_def cosh_def algebra_simps scaleR_conv_of_real exp_add [symmetric])
lemma sinh_diff: "sinh (x - y) = sinh x * cosh y - cosh x * sinh y"
- by (simp add: sinh_def cosh_def algebra_simps scaleR_conv_of_real exp_add [symmetric])
+ by (simp add: sinh_def cosh_def algebra_simps scaleR_conv_of_real exp_add [symmetric])
lemma cosh_add: "cosh (x + y) = cosh x * cosh y + sinh x * sinh y"
by (simp add: sinh_def cosh_def algebra_simps scaleR_conv_of_real exp_add [symmetric])
-
+
lemma cosh_diff: "cosh (x - y) = cosh x * cosh y - sinh x * sinh y"
by (simp add: sinh_def cosh_def algebra_simps scaleR_conv_of_real exp_add [symmetric])
-lemma tanh_add:
+lemma tanh_add:
"cosh x \<noteq> 0 \<Longrightarrow> cosh y \<noteq> 0 \<Longrightarrow> tanh (x + y) = (tanh x + tanh y) / (1 + tanh x * tanh y)"
by (simp add: tanh_def sinh_add cosh_add divide_simps)
@@ -6621,7 +6540,7 @@
lemma cosh_real_pos [simp]: "cosh (x :: real) > 0"
using cosh_real_ge_1[of x] by simp
-
+
lemma cosh_real_nonneg[simp]: "cosh (x :: real) \<ge> 0"
using cosh_real_ge_1[of x] by simp
@@ -6696,7 +6615,7 @@
context
fixes x :: real
begin
-
+
lemma arsinh_sinh_real: "arsinh (sinh x) = x"
by (simp add: arsinh_real_def powr_def sinh_square_eq sinh_plus_cosh)
@@ -6707,9 +6626,9 @@
proof -
have "artanh (tanh x) = ln (cosh x * (cosh x + sinh x) / (cosh x * (cosh x - sinh x))) / 2"
by (simp add: artanh_def tanh_def divide_simps)
- also have "cosh x * (cosh x + sinh x) / (cosh x * (cosh x - sinh x)) =
+ also have "cosh x * (cosh x + sinh x) / (cosh x * (cosh x - sinh x)) =
(cosh x + sinh x) / (cosh x - sinh x)" by simp
- also have "\<dots> = (exp x)^2"
+ also have "\<dots> = (exp x)^2"
by (simp add: cosh_plus_sinh cosh_minus_sinh exp_minus field_simps power2_eq_square)
also have "ln ((exp x)^2) / 2 = x" by (simp add: ln_realpow)
finally show ?thesis .
@@ -6717,21 +6636,6 @@
end
-(* TODO Move *)
-lemma pos_deriv_imp_strict_mono:
- assumes "\<And>x. (f has_real_derivative f' x) (at x)"
- assumes "\<And>x. f' x > 0"
- shows "strict_mono f"
-proof (rule strict_monoI)
- fix x y :: real assume xy: "x < y"
- from assms and xy have "\<exists>z>x. z < y \<and> f y - f x = (y - x) * f' z"
- by (intro MVT2) (auto dest: connectedD_interval)
- then obtain z where z: "z > x" "z < y" "f y - f x = (y - x) * f' z" by blast
- note \<open>f y - f x = (y - x) * f' z\<close>
- also have "(y - x) * f' z > 0" using xy assms by (intro mult_pos_pos) auto
- finally show "f x < f y" by simp
-qed
-
lemma sinh_real_strict_mono: "strict_mono (sinh :: real \<Rightarrow> real)"
by (rule pos_deriv_imp_strict_mono derivative_intros)+ auto
@@ -6762,7 +6666,7 @@
by (simp add: abs_if)
lemma tanh_real_abs [simp]: "tanh (abs x :: real) = abs (tanh x)"
- by (auto simp add: abs_if)
+ by (auto simp: abs_if)
lemma sinh_real_eq_iff [simp]: "sinh x = sinh y \<longleftrightarrow> x = (y :: real)"
using sinh_real_strict_mono by (simp add: strict_mono_eq)
@@ -6813,7 +6717,7 @@
have *: "((\<lambda>x. - exp (- x)) \<longlongrightarrow> (-0::real)) at_top"
by (intro tendsto_minus filterlim_compose[OF exp_at_bot] filterlim_uminus_at_bot_at_top)
have "filterlim (\<lambda>x. (1 / 2) * (-exp (-x) + exp x) :: real) at_top at_top"
- by (rule filterlim_tendsto_pos_mult_at_top[OF _ _
+ by (rule filterlim_tendsto_pos_mult_at_top[OF _ _
filterlim_tendsto_add_at_top[OF *]] tendsto_const)+ (auto simp: exp_at_top)
also have "(\<lambda>x. (1 / 2) * (-exp (-x) + exp x) :: real) = sinh"
by (simp add: fun_eq_iff sinh_def)
@@ -6833,7 +6737,7 @@
have *: "((\<lambda>x. exp (- x)) \<longlongrightarrow> (0::real)) at_top"
by (intro filterlim_compose[OF exp_at_bot] filterlim_uminus_at_bot_at_top)
have "filterlim (\<lambda>x. (1 / 2) * (exp (-x) + exp x) :: real) at_top at_top"
- by (rule filterlim_tendsto_pos_mult_at_top[OF _ _
+ by (rule filterlim_tendsto_pos_mult_at_top[OF _ _
filterlim_tendsto_add_at_top[OF *]] tendsto_const)+ (auto simp: exp_at_top)
also have "(\<lambda>x. (1 / 2) * (exp (-x) + exp x) :: real) = cosh"
by (simp add: fun_eq_iff cosh_def)
@@ -6882,7 +6786,7 @@
fixes f :: "_ \<Rightarrow>'a::{real_normed_field,banach}"
assumes "continuous_on A f"
shows "continuous_on A (\<lambda>x. sinh (f x))"
- unfolding sinh_def using assms by (intro continuous_intros)
+ unfolding sinh_def using assms by (intro continuous_intros)
lemma continuous_on_cosh [continuous_intros]:
fixes f :: "_ \<Rightarrow>'a::{real_normed_field,banach}"
@@ -6912,13 +6816,13 @@
fixes f :: "_ \<Rightarrow>'a::{real_normed_field,banach}"
assumes "continuous (at x within A) f" "cosh (f x) \<noteq> 0"
shows "continuous (at x within A) (\<lambda>x. tanh (f x))"
- unfolding tanh_def using assms by (intro continuous_intros continuous_divide) auto
+ unfolding tanh_def using assms by (intro continuous_intros continuous_divide) auto
lemma continuous_tanh [continuous_intros]:
fixes f :: "_ \<Rightarrow>'a::{real_normed_field,banach}"
assumes "continuous F f" "cosh (f (Lim F (\<lambda>x. x))) \<noteq> 0"
shows "continuous F (\<lambda>x. tanh (f x))"
- unfolding tanh_def using assms by (intro continuous_intros continuous_divide) auto
+ unfolding tanh_def using assms by (intro continuous_intros continuous_divide) auto
lemma tendsto_sinh [tendsto_intros]:
fixes f :: "_ \<Rightarrow>'a::{real_normed_field,banach}"
@@ -6952,7 +6856,7 @@
proof -
from assms have "x + sqrt (x\<^sup>2 - 1) > 0" by (simp add: add_pos_pos)
thus ?thesis using assms unfolding arcosh_def [abs_def]
- by (auto intro!: derivative_eq_intros
+ by (auto intro!: derivative_eq_intros
simp: powr_minus powr_half_sqrt divide_simps power2_eq_1_iff)
qed
@@ -6962,7 +6866,7 @@
shows "(artanh has_field_derivative (1 / (1 - x ^ 2))) (at x within A)"
proof -
from assms have "x > -1" "x < 1" by linarith+
- hence "(artanh has_field_derivative (4 - 4 * x) / ((1 + x) * (1 - x) * (1 - x) * 4))
+ hence "(artanh has_field_derivative (4 - 4 * x) / ((1 + x) * (1 - x) * (1 - x) * 4))
(at x within A)" unfolding artanh_def [abs_def]
by (auto intro!: derivative_eq_intros simp: powr_minus powr_half_sqrt)
also have "(4 - 4 * x) / ((1 + x) * (1 - x) * (1 - x) * 4) = 1 / ((1 + x) * (1 - x))"
@@ -7058,7 +6962,7 @@
thus ?thesis by simp
qed
-lemma tendsto_artanh [tendsto_intros]:
+lemma tendsto_artanh [tendsto_intros]:
fixes f :: "'a \<Rightarrow> real"
assumes "(f \<longlongrightarrow> a) F" "a > -1" "a < 1"
shows "((\<lambda>x. artanh (f x)) \<longlongrightarrow> artanh a) F"
@@ -7154,8 +7058,8 @@
context
begin
-
-private lemma sqrt_numeral_simproc_aux:
+
+private lemma sqrt_numeral_simproc_aux:
assumes "m * m \<equiv> n"
shows "sqrt (numeral n :: real) \<equiv> numeral m"
proof -
@@ -7164,7 +7068,7 @@
ultimately show "sqrt (numeral n :: real) \<equiv> numeral m" by simp
qed
-private lemma root_numeral_simproc_aux:
+private lemma root_numeral_simproc_aux:
assumes "Num.pow m n \<equiv> x"
shows "root (numeral n) (numeral x :: real) \<equiv> numeral m"
by (subst assms [symmetric], subst numeral_pow, subst real_root_pos2) simp_all
@@ -7175,7 +7079,7 @@
by (subst assms [symmetric], subst numeral_pow, subst powr_numeral [symmetric])
(simp, subst powr_powr, simp_all)
-private lemma numeral_powr_inverse_eq:
+private lemma numeral_powr_inverse_eq:
"numeral x powr (inverse (numeral n)) = numeral x powr (1 / numeral n :: real)"
by simp