--- a/src/HOL/Transcendental.thy Sat Jul 07 15:07:46 2018 +0100
+++ b/src/HOL/Transcendental.thy Sun Jul 08 11:00:20 2018 +0100
@@ -2581,10 +2581,8 @@
by (simp_all add: log_mult log_divide)
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, auto)
- done
+ using powr_less_cancel_iff [of a] powr_log_cancel [of a x] powr_log_cancel [of a y]
+ by (metis less_eq_real_def less_trans not_le zero_less_one)
lemma log_inj:
assumes "1 < b"
@@ -2641,11 +2639,7 @@
assumes "1 < b" "x > 0"
shows "y \<le> log b x \<longleftrightarrow> b powr y \<le> x"
using assms
- apply auto
- apply (metis (no_types, hide_lams) less_irrefl less_le_trans linear powr_le_cancel_iff
- powr_log_cancel zero_less_one)
- apply (metis not_less order.trans order_refl powr_le_cancel_iff powr_log_cancel zero_le_one)
- done
+ by (metis less_irrefl less_trans powr_le_cancel_iff powr_log_cancel zero_less_one)
lemma less_log_iff:
assumes "1 < b" "x > 0"
@@ -3149,10 +3143,7 @@
lemma tendsto_exp_limit_at_top: "((\<lambda>y. (1 + x / y) powr y) \<longlongrightarrow> exp x) at_top"
for x :: real
- apply (subst filterlim_at_top_to_right)
- apply (simp add: inverse_eq_divide)
- apply (rule tendsto_exp_limit_at_right)
- done
+ by (simp add: filterlim_at_top_to_right inverse_eq_divide tendsto_exp_limit_at_right)
lemma tendsto_exp_limit_sequentially: "(\<lambda>n. (1 + x / n) ^ n) \<longlonglongrightarrow> exp x"
for x :: real
@@ -3715,45 +3706,44 @@
show "\<exists>x::real. 0 \<le> x \<and> x \<le> 2 \<and> cos x = 0"
by (rule IVT2) simp_all
next
- 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 cosd[simp]: "\<forall>x::real. cos differentiable (at x)"
+ fix a b :: real
+ assume ab: "0 \<le> a \<and> a \<le> 2 \<and> cos a = 0" "0 \<le> b \<and> b \<le> 2 \<and> cos b = 0"
+ have cosd: "\<And>x::real. cos differentiable (at x)"
unfolding real_differentiable_def by (auto intro: DERIV_cos)
- show "x = y"
- proof (cases x y rule: linorder_cases)
+ show "a = b"
+ proof (cases a b 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 obtain z where "a < z" "z < b" "(cos has_real_derivative 0) (at z)"
+ using Rolle by (metis cosd isCont_cos ab)
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)
+ by (metis \<open>a < z\<close> \<open>z < b\<close> ab 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 obtain z where "b < z" "z < a" "(cos has_real_derivative 0) (at z)"
+ using Rolle by (metis cosd isCont_cos ab)
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)
+ by (metis \<open>b < z\<close> \<open>z < a\<close> ab 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)"
by (simp add: pi_def)
-lemma cos_pi_half [simp]: "cos (pi / 2) = 0"
+lemma cos_pi_half [simp]: "cos (pi/2) = 0"
by (simp add: pi_half cos_is_zero [THEN theI'])
-lemma cos_of_real_pi_half [simp]: "cos ((of_real pi / 2) :: 'a) = 0"
+lemma cos_of_real_pi_half [simp]: "cos ((of_real pi/2) :: 'a) = 0"
if "SORT_CONSTRAINT('a::{real_field,banach,real_normed_algebra_1})"
by (metis cos_pi_half cos_of_real eq_numeral_simps(4)
nonzero_of_real_divide of_real_0 of_real_numeral)
-lemma pi_half_gt_zero [simp]: "0 < pi / 2"
-proof -
- have "0 \<le> pi / 2"
+lemma pi_half_gt_zero [simp]: "0 < pi/2"
+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)
@@ -3762,9 +3752,9 @@
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"
-proof -
- have "pi / 2 \<le> 2"
+lemma pi_half_less_two [simp]: "pi/2 < 2"
+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)
@@ -3796,26 +3786,26 @@
using sin_gt_zero_02 [OF pi_half_gt_zero pi_half_less_two]
by (simp add: power2_eq_1_iff)
-lemma sin_of_real_pi_half [simp]: "sin ((of_real pi / 2) :: 'a) = 1"
+lemma sin_of_real_pi_half [simp]: "sin ((of_real pi/2) :: 'a) = 1"
if "SORT_CONSTRAINT('a::{real_field,banach,real_normed_algebra_1})"
using sin_pi_half
by (metis sin_pi_half eq_numeral_simps(4) nonzero_of_real_divide of_real_1 of_real_numeral sin_of_real)
-lemma sin_cos_eq: "sin x = cos (of_real pi / 2 - x)"
+lemma sin_cos_eq: "sin x = cos (of_real pi/2 - x)"
for x :: "'a::{real_normed_field,banach}"
by (simp add: cos_diff)
-lemma minus_sin_cos_eq: "- sin x = cos (x + of_real pi / 2)"
+lemma minus_sin_cos_eq: "- sin x = cos (x + of_real pi/2)"
for x :: "'a::{real_normed_field,banach}"
by (simp add: cos_add nonzero_of_real_divide)
-lemma cos_sin_eq: "cos x = sin (of_real pi / 2 - x)"
+lemma cos_sin_eq: "cos x = sin (of_real pi/2 - x)"
for x :: "'a::{real_normed_field,banach}"
- using sin_cos_eq [of "of_real pi / 2 - x"] by simp
+ using sin_cos_eq [of "of_real pi/2 - x"] by simp
lemma sin_add: "sin (x + y) = sin x * cos y + cos x * sin y"
for x :: "'a::{real_normed_field,banach}"
- using cos_add [of "of_real pi / 2 - x" "-y"]
+ using cos_add [of "of_real pi/2 - x" "-y"]
by (simp add: cos_sin_eq) (simp add: sin_cos_eq)
lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"
@@ -3895,13 +3885,13 @@
by (simp add: cos_diff cos_add)
lemma sin_plus_sin: "sin w + sin z = 2 * sin ((w + z) / 2) * cos ((w - z) / 2)"
- for w :: "'a::{real_normed_field,banach,field}" (* FIXME field should not be necessary *)
+ for w :: "'a::{real_normed_field,banach}"
apply (simp add: mult.assoc sin_times_cos)
apply (simp add: field_simps)
done
lemma sin_diff_sin: "sin w - sin z = 2 * sin ((w - z) / 2) * cos ((w + z) / 2)"
- for w :: "'a::{real_normed_field,banach,field}"
+ for w :: "'a::{real_normed_field,banach}"
apply (simp add: mult.assoc sin_times_cos)
apply (simp add: field_simps)
done
@@ -4017,28 +4007,36 @@
shows "0 < sin (pi / real n)"
by (rule sin_gt_zero) (use assms in \<open>simp_all add: divide_simps\<close>)
-(* FIXME: This proof is almost identical to lemma \<open>cos_is_zero\<close>.
- It should be possible to factor out some of the common parts. *)
+text\<open>Proof resembles that of @{text cos_is_zero} but with @{term pi} for the upper bound\<close>
lemma cos_total:
- assumes y: "- 1 \<le> y" "y \<le> 1"
+ assumes y: "-1 \<le> y" "y \<le> 1"
shows "\<exists>!x. 0 \<le> x \<and> x \<le> pi \<and> cos x = y"
proof (rule ex_ex1I)
- show "\<exists>x. 0 \<le> x \<and> x \<le> pi \<and> cos x = y"
+ show "\<exists>x::real. 0 \<le> x \<and> x \<le> pi \<and> cos x = y"
by (rule IVT2) (simp_all add: y)
next
- fix a b
- assume a: "0 \<le> a \<and> a \<le> pi \<and> cos a = y"
- assume b: "0 \<le> b \<and> b \<le> pi \<and> cos b = y"
- have [simp]: "\<forall>x::real. cos differentiable (at x)"
+ fix a b :: real
+ assume ab: "0 \<le> a \<and> a \<le> pi \<and> cos a = y" "0 \<le> b \<and> b \<le> pi \<and> cos b = y"
+ have cosd: "\<And>x::real. cos differentiable (at x)"
unfolding real_differentiable_def by (auto intro: DERIV_cos)
- from a b less_linear [of a b] show "a = b"
- 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)
- apply (metis order_less_le_trans less_le sin_gt_zero)
- done
+ show "a = b"
+ proof (cases a b rule: linorder_cases)
+ case less
+ then obtain z where "a < z" "z < b" "(cos has_real_derivative 0) (at z)"
+ using Rolle by (metis cosd isCont_cos ab)
+ then have "sin z = 0"
+ using DERIV_cos DERIV_unique neg_equal_0_iff_equal by blast
+ then show ?thesis
+ by (metis \<open>a < z\<close> \<open>z < b\<close> ab order_less_le_trans less_le sin_gt_zero)
+ next
+ case greater
+ then obtain z where "b < z" "z < a" "(cos has_real_derivative 0) (at z)"
+ using Rolle by (metis cosd isCont_cos ab)
+ then have "sin z = 0"
+ using DERIV_cos DERIV_unique neg_equal_0_iff_equal by blast
+ then show ?thesis
+ by (metis \<open>b < z\<close> \<open>z < a\<close> ab order_less_le_trans less_le sin_gt_zero)
+ qed auto
qed
lemma sin_total:
@@ -4052,10 +4050,8 @@
show ?thesis
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
+ 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
@@ -4100,7 +4096,7 @@
"cos x = 0 \<longleftrightarrow> ((\<exists>n. odd n \<and> x = real n * (pi/2)) \<or> (\<exists>n. odd n \<and> x = - (real n * (pi/2))))"
(is "?lhs = ?rhs")
proof -
- have *: "cos (real n * pi / 2) = 0" if "odd n" for n :: nat
+ have *: "cos (real n * pi/2) = 0" if "odd n" for n :: nat
proof -
from that obtain m where "n = 2 * m + 1" ..
then show ?thesis
@@ -4126,38 +4122,32 @@
qed
lemma cos_zero_iff_int: "cos x = 0 \<longleftrightarrow> (\<exists>n. odd n \<and> x = of_int n * (pi/2))"
-proof safe
- assume "cos x = 0"
- then show "\<exists>n. odd n \<and> x = of_int n * (pi / 2)"
- unfolding 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
- done
-next
- fix n :: int
- assume "odd n"
- then show "cos (of_int n * (pi / 2)) = 0"
- by (cases n rule: int_cases2, simp_all add: cos_zero_iff)
+proof -
+ have 1: "\<And>n. odd n \<Longrightarrow> \<exists>i. odd i \<and> real n = real_of_int i"
+ by (metis even_of_nat of_int_of_nat_eq)
+ have 2: "\<And>n. odd n \<Longrightarrow> \<exists>i. odd i \<and> - (real n * pi) = real_of_int i * pi"
+ by (metis even_minus even_of_nat mult.commute mult_minus_right of_int_minus of_int_of_nat_eq)
+ have 3: "\<lbrakk>odd i; \<forall>n. even n \<or> real_of_int i \<noteq> - (real n)\<rbrakk>
+ \<Longrightarrow> \<exists>n. odd n \<and> real_of_int i = real n" for i
+ by (cases i rule: int_cases2) auto
+ show ?thesis
+ by (force simp: cos_zero_iff intro!: 1 2 3)
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)"
+ then show "\<exists>n. even n \<and> x = of_int n * (pi/2)"
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
done
next
- fix n :: int
- assume "even n"
- then show "sin (of_int n * (pi / 2)) = 0"
- apply (simp add: sin_zero_iff)
- apply (cases n rule: int_cases2, simp_all)
- done
+ fix i :: int
+ assume "even i"
+ then show "sin (of_int i * (pi/2)) = 0"
+ by (cases i rule: int_cases2, simp_all add: sin_zero_iff)
qed
lemma sin_zero_iff_int2: "sin x = 0 \<longleftrightarrow> (\<exists>n::int. x = of_int n * pi)"
@@ -4227,14 +4217,11 @@
lemma sin_monotone_2pi:
assumes "- (pi/2) \<le> y" and "y < x" and "x \<le> pi/2"
shows "sin y < sin x"
- apply (simp add: sin_cos_eq)
- apply (rule cos_monotone_0_pi)
- using assms
- apply auto
- done
+ unfolding sin_cos_eq
+ using assms by (auto intro: cos_monotone_0_pi)
lemma sin_monotone_2pi_le:
- assumes "- (pi / 2) \<le> y" and "y \<le> x" and "x \<le> pi / 2"
+ assumes "- (pi/2) \<le> y" and "y \<le> x" and "x \<le> pi/2"
shows "sin y \<le> sin x"
by (metis assms le_less sin_monotone_2pi)
@@ -4274,7 +4261,7 @@
subsection \<open>More Corollaries about Sine and Cosine\<close>
-lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
+lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi/2) = (-1) ^ n"
proof -
have "sin ((real n + 1/2) * pi) = cos (real n * pi)"
by (auto simp: algebra_simps sin_add)
@@ -4287,20 +4274,26 @@
by (cases "even n") (simp_all add: cos_double mult.assoc)
lemma cos_3over2_pi [simp]: "cos (3/2*pi) = 0"
- apply (subgoal_tac "cos (pi + pi/2) = 0")
- apply simp
- apply (subst cos_add, simp)
- done
+proof -
+ have "cos (3/2*pi) = cos (pi + pi/2)"
+ by simp
+ also have "... = 0"
+ by (subst cos_add, simp)
+ finally show ?thesis .
+qed
lemma sin_2npi [simp]: "sin (2 * real n * pi) = 0"
for n :: nat
by (auto simp: mult.assoc sin_double)
lemma sin_3over2_pi [simp]: "sin (3/2*pi) = - 1"
- apply (subgoal_tac "sin (pi + pi/2) = - 1")
- apply simp
- apply (subst sin_add, simp)
- done
+proof -
+ have "sin (3/2*pi) = sin (pi + pi/2)"
+ by simp
+ also have "... = -1"
+ by (subst sin_add, simp)
+ finally show ?thesis .
+qed
lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
by (simp only: cos_add sin_add of_nat_Suc distrib_right distrib_left add_divide_distrib, auto)
@@ -4366,10 +4359,7 @@
proof
assume "cos x = 1"
then show ?rhs
- apply (auto simp: cos_one_2pi)
- apply (metis of_int_of_nat_eq)
- apply (metis mult_minus_right of_int_minus of_int_of_nat_eq)
- done
+ by (metis cos_one_2pi mult.commute mult_minus_right of_int_minus of_int_of_nat_eq)
next
assume ?rhs
then show "cos x = 1"
@@ -4444,11 +4434,12 @@
by (simp add: sin_cos_eq cos_30)
lemma cos_60: "cos (pi / 3) = 1 / 2"
- 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], simp_all)
- done
+proof -
+ have "0 \<le> cos (pi / 3)"
+ by (rule cos_ge_zero) (use pi_half_ge_zero in \<open>linarith+\<close>)
+ then show ?thesis
+ by (simp add: cos_squared_eq sin_60 power_divide power2_eq_imp_eq)
+qed
lemma sin_30: "sin (pi / 6) = 1 / 2"
by (simp add: sin_cos_eq cos_60)
@@ -4584,40 +4575,63 @@
lemma LIM_cos_div_sin: "(\<lambda>x. cos(x)/sin(x)) \<midarrow>pi/2\<rightarrow> 0"
by (rule LIM_cong_limit, (rule tendsto_intros)+, simp_all)
-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, safe)
- apply force
- 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: tan_def sin_diff cos_diff)
- apply (rule inverse_less_iff_less [THEN iffD1])
- 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, safe)
- prefer 2 apply force
- 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)
- apply (auto dest: cos_gt_zero)
- done
-
+lemma lemma_tan_total:
+ assumes "0 < y" shows "\<exists>x. 0 < x \<and> x < pi/2 \<and> y < tan x"
+proof -
+ obtain s where "0 < s"
+ and s: "\<And>x. \<lbrakk>x \<noteq> pi/2; norm (x - pi/2) < s\<rbrakk> \<Longrightarrow> norm (cos x / sin x - 0) < inverse y"
+ using LIM_D [OF LIM_cos_div_sin, of "inverse y"] that assms by force
+ obtain e where e: "0 < e" "e < s" "e < pi/2"
+ using \<open>0 < s\<close> field_lbound_gt_zero pi_half_gt_zero by blast
+ show ?thesis
+ proof (intro exI conjI)
+ have "0 < sin e" "0 < cos e"
+ using e by (auto intro: cos_gt_zero sin_gt_zero2 simp: mult.commute)
+ then
+ show "y < tan (pi/2 - e)"
+ using s [of "pi/2 - e"] e assms
+ by (simp add: tan_def sin_diff cos_diff) (simp add: field_simps split: if_split_asm)
+ qed (use e in auto)
+qed
+
+lemma tan_total_pos:
+ assumes "0 \<le> y" shows "\<exists>x. 0 \<le> x \<and> x < pi/2 \<and> tan x = y"
+proof (cases "y = 0")
+ case True
+ then show ?thesis
+ using pi_half_gt_zero tan_zero by blast
+next
+ case False
+ with assms have "y > 0"
+ by linarith
+ obtain x where x: "0 < x" "x < pi/2" "y < tan x"
+ using lemma_tan_total \<open>0 < y\<close> by blast
+ have "\<exists>u\<ge>0. u \<le> x \<and> tan u = y"
+ proof (intro IVT allI impI)
+ show "isCont tan u" if "0 \<le> u \<and> u \<le> x" for u
+ proof -
+ have "cos u \<noteq> 0"
+ using antisym_conv2 cos_gt_zero that x(2) by fastforce
+ with assms show ?thesis
+ by (auto intro!: DERIV_tan [THEN DERIV_isCont])
+ qed
+ qed (use assms x in auto)
+ then show ?thesis
+ using x(2) by auto
+qed
+
lemma lemma_tan_total1: "\<exists>x. -(pi/2) < x \<and> x < (pi/2) \<and> tan x = y"
- apply (insert linorder_linear [of 0 y], safe)
- apply (drule tan_total_pos)
- 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
+proof (cases "0::real" y rule: le_cases)
+ case le
+ then show ?thesis
+ by (meson less_le_trans minus_pi_half_less_zero tan_total_pos)
+next
+ case ge
+ with tan_total_pos [of "-y"] obtain x where "0 \<le> x" "x < pi / 2" "tan x = - y"
+ by force
+ then show ?thesis
+ by (rule_tac x="-x" in exI) auto
+qed
lemma tan_total: "\<exists>! x. -(pi/2) < x \<and> x < (pi/2) \<and> tan x = y"
apply (insert lemma_tan_total1 [where y = y], auto)
@@ -4635,7 +4649,7 @@
done
lemma tan_monotone:
- assumes "- (pi / 2) < y" and "y < x" and "x < pi / 2"
+ assumes "- (pi/2) < y" and "y < x" and "x < pi/2"
shows "tan y < tan x"
proof -
have "\<forall>x'. y \<le> x' \<and> x' \<le> x \<longrightarrow> DERIV tan x' :> inverse ((cos x')\<^sup>2)"
@@ -4652,7 +4666,7 @@
from MVT2[OF \<open>y < x\<close> this]
obtain z where "y < z" and "z < x"
and tan_diff: "tan x - tan y = (x - y) * inverse ((cos z)\<^sup>2)" by auto
- then have "- (pi / 2) < z" and "z < pi / 2"
+ then have "- (pi/2) < z" and "z < pi/2"
using assms by auto
then have "0 < cos z"
using cos_gt_zero_pi by auto
@@ -4665,15 +4679,15 @@
qed
lemma tan_monotone':
- assumes "- (pi / 2) < y"
- and "y < pi / 2"
- and "- (pi / 2) < x"
- and "x < pi / 2"
+ assumes "- (pi/2) < y"
+ and "y < pi/2"
+ and "- (pi/2) < x"
+ and "x < pi/2"
shows "y < x \<longleftrightarrow> tan y < tan x"
proof
assume "y < x"
then show "tan y < tan x"
- using tan_monotone and \<open>- (pi / 2) < y\<close> and \<open>x < pi / 2\<close> by auto
+ using tan_monotone and \<open>- (pi/2) < y\<close> and \<open>x < pi/2\<close> by auto
next
assume "tan y < tan x"
show "y < x"
@@ -4687,7 +4701,7 @@
next
case False
then have "x < y" using \<open>x \<le> y\<close> by auto
- from tan_monotone[OF \<open>- (pi/2) < x\<close> this \<open>y < pi / 2\<close>] show ?thesis
+ from tan_monotone[OF \<open>- (pi/2) < x\<close> this \<open>y < pi/2\<close>] show ?thesis
by auto
qed
then show False
@@ -4695,7 +4709,7 @@
qed
qed
-lemma tan_inverse: "1 / (tan y) = tan (pi / 2 - y)"
+lemma tan_inverse: "1 / (tan y) = tan (pi/2 - y)"
unfolding tan_def sin_cos_eq[of y] cos_sin_eq[of y] by auto
lemma tan_periodic_pi[simp]: "tan (x + pi) = tan x"
@@ -5080,13 +5094,13 @@
lemma continuous_on_arcsin': "continuous_on {-1 .. 1} arcsin"
proof -
- have "continuous_on (sin ` {- pi / 2 .. pi / 2}) arcsin"
+ have "continuous_on (sin ` {- pi/2 .. pi/2}) arcsin"
by (rule continuous_on_inv) (auto intro: continuous_intros simp: arcsin_sin)
- also have "sin ` {- pi / 2 .. pi / 2} = {-1 .. 1}"
+ also have "sin ` {- pi/2 .. pi/2} = {-1 .. 1}"
proof safe
fix x :: real
assume "x \<in> {-1..1}"
- then show "x \<in> sin ` {- pi / 2..pi / 2}"
+ then show "x \<in> sin ` {- pi/2..pi/2}"
using arcsin_lbound arcsin_ubound
by (intro image_eqI[where x="arcsin x"]) auto
qed simp
@@ -5213,7 +5227,7 @@
define y where "y = pi/2 - min (pi/2) e"
then have y: "0 \<le> y" "y < pi/2" "pi/2 \<le> e + y"
using \<open>0 < e\<close> by auto
- show "eventually (\<lambda>x. dist (arctan x) (pi / 2) < e) at_top"
+ show "eventually (\<lambda>x. dist (arctan x) (pi/2) < e) at_top"
proof (intro eventually_at_top_dense[THEN iffD2] exI allI impI)
fix x
assume "tan y < x"
@@ -5222,7 +5236,7 @@
with y have "y < arctan x"
by (subst (asm) arctan_tan) simp_all
with arctan_ubound[of x, arith] y \<open>0 < e\<close>
- show "dist (arctan x) (pi / 2) < e"
+ show "dist (arctan x) (pi/2) < e"
by (simp add: dist_real_def)
qed
qed
@@ -5433,13 +5447,13 @@
unfolding arctan_one [symmetric] arctan_minus [symmetric]
unfolding arctan_le_iff arctan_less_iff
using assms by auto
- from add_le_less_mono [OF this] show 1: "- (pi / 2) < arctan x + arctan y"
+ from add_le_less_mono [OF this] show 1: "- (pi/2) < arctan x + arctan y"
by simp
have "arctan x \<le> pi / 4" "arctan y < pi / 4"
unfolding arctan_one [symmetric]
unfolding arctan_le_iff arctan_less_iff
using assms by auto
- from add_le_less_mono [OF this] show 2: "arctan x + arctan y < pi / 2"
+ from add_le_less_mono [OF this] show 2: "arctan x + arctan y < pi/2"
by simp
show "tan (arctan x + arctan y) = (x + y) / (1 - x * y)"
using cos_gt_zero_pi [OF 1 2] by (simp add: arctan tan_add)
@@ -5847,7 +5861,7 @@
case False
then have "x = -1" using \<open>\<bar>x\<bar> = 1\<close> by auto
- have "- (pi / 2) < 0" using pi_gt_zero by auto
+ have "- (pi/2) < 0" using pi_gt_zero by auto
have "- (2 * pi) < 0" using pi_gt_zero by auto
have c_minus_minus: "?c (- 1) i = - ?c 1 i" for i by auto
@@ -5855,7 +5869,7 @@
have "arctan (- 1) = arctan (tan (-(pi / 4)))"
unfolding tan_45 tan_minus ..
also have "\<dots> = - (pi / 4)"
- by (rule arctan_tan) (auto simp: order_less_trans[OF \<open>- (pi / 2) < 0\<close> pi_gt_zero])
+ by (rule arctan_tan) (auto simp: order_less_trans[OF \<open>- (pi/2) < 0\<close> pi_gt_zero])
also have "\<dots> = - (arctan (tan (pi / 4)))"
unfolding neg_equal_iff_equal
by (rule arctan_tan[symmetric]) (auto simp: order_less_trans[OF \<open>- (2 * pi) < 0\<close> pi_gt_zero])
@@ -5874,9 +5888,9 @@
lemma arctan_half: "arctan x = 2 * arctan (x / (1 + sqrt(1 + x\<^sup>2)))"
for x :: real
proof -
- obtain y where low: "- (pi / 2) < y" and high: "y < pi / 2" and y_eq: "tan y = x"
+ obtain y where low: "- (pi/2) < y" and high: "y < pi/2" and y_eq: "tan y = x"
using tan_total by blast
- then have low2: "- (pi / 2) < y / 2" and high2: "y / 2 < pi / 2"
+ then have low2: "- (pi/2) < y / 2" and high2: "y / 2 < pi/2"
by auto
have "0 < cos y" by (rule cos_gt_zero_pi[OF low high])
@@ -5920,19 +5934,19 @@
lemma arctan_inverse:
assumes "x \<noteq> 0"
- shows "arctan (1 / x) = sgn x * pi / 2 - arctan x"
+ shows "arctan (1 / x) = sgn x * pi/2 - arctan x"
proof (rule arctan_unique)
- show "- (pi / 2) < sgn x * pi / 2 - arctan x"
+ show "- (pi/2) < sgn x * pi/2 - arctan x"
using arctan_bounded [of x] assms
unfolding sgn_real_def
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"
+ show "sgn x * pi/2 - arctan x < pi/2"
using arctan_bounded [of "- x"] assms
unfolding sgn_real_def arctan_minus
by (auto simp: algebra_simps)
- show "tan (sgn x * pi / 2 - arctan x) = 1 / x"
+ show "tan (sgn x * pi/2 - arctan x) = 1 / x"
unfolding tan_inverse [of "arctan x", unfolded tan_arctan]
unfolding sgn_real_def
by (simp add: tan_def cos_arctan sin_arctan sin_diff cos_diff)