merged
authorbulwahn
Tue Sep 06 17:52:00 2011 +0200 (2011-09-06)
changeset 44752eaf394237ba7
parent 44751 f523923d8182
parent 44750 5b11f36fcacb
child 44753 3c73f4068978
merged
     1.1 --- a/NEWS	Tue Sep 06 16:40:22 2011 +0200
     1.2 +++ b/NEWS	Tue Sep 06 17:52:00 2011 +0200
     1.3 @@ -276,6 +276,7 @@
     1.4    real_squared_diff_one_factored ~> square_diff_one_factored
     1.5    realpow_two_diff ~> square_diff_square_factored
     1.6    reals_complete2 ~> complete_real
     1.7 +  real_sum_squared_expand ~> power2_sum
     1.8    exp_ln_eq ~> ln_unique
     1.9    expi_add ~> exp_add
    1.10    expi_zero ~> exp_zero
    1.11 @@ -301,6 +302,7 @@
    1.12    LIMSEQ_add_minus ~> tendsto_add [OF _ tendsto_minus]
    1.13    LIMSEQ_add_const ~> tendsto_add [OF _ tendsto_const]
    1.14    LIMSEQ_diff_const ~> tendsto_diff [OF _ tendsto_const]
    1.15 +  LIMSEQ_Complex ~> tendsto_Complex
    1.16    LIM_ident ~> tendsto_ident_at
    1.17    LIM_const ~> tendsto_const
    1.18    LIM_add ~> tendsto_add
     2.1 --- a/src/HOL/Complex.thy	Tue Sep 06 16:40:22 2011 +0200
     2.2 +++ b/src/HOL/Complex.thy	Tue Sep 06 17:52:00 2011 +0200
     2.3 @@ -321,8 +321,6 @@
     2.4  lemma complex_mod_triangle_ineq2 [simp]: "cmod(b + a) - cmod b \<le> cmod a"
     2.5    by (rule ord_le_eq_trans [OF norm_triangle_ineq2], simp)
     2.6  
     2.7 -lemmas real_sum_squared_expand = power2_sum [where 'a=real]
     2.8 -
     2.9  lemma abs_Re_le_cmod: "\<bar>Re x\<bar> \<le> cmod x"
    2.10    by (cases x) simp
    2.11  
    2.12 @@ -366,10 +364,6 @@
    2.13         (simp add: dist_norm real_sqrt_sum_squares_less)
    2.14  qed
    2.15  
    2.16 -lemma LIMSEQ_Complex:
    2.17 -  "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. Complex (X n) (Y n)) ----> Complex a b"
    2.18 -  by (rule tendsto_Complex)
    2.19 -
    2.20  instance complex :: banach
    2.21  proof
    2.22    fix X :: "nat \<Rightarrow> complex"
    2.23 @@ -379,7 +373,7 @@
    2.24    from Cauchy_Im [OF X] have 2: "(\<lambda>n. Im (X n)) ----> lim (\<lambda>n. Im (X n))"
    2.25      by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
    2.26    have "X ----> Complex (lim (\<lambda>n. Re (X n))) (lim (\<lambda>n. Im (X n)))"
    2.27 -    using LIMSEQ_Complex [OF 1 2] by simp
    2.28 +    using tendsto_Complex [OF 1 2] by simp
    2.29    thus "convergent X"
    2.30      by (rule convergentI)
    2.31  qed
     3.1 --- a/src/HOL/Library/Product_Vector.thy	Tue Sep 06 16:40:22 2011 +0200
     3.2 +++ b/src/HOL/Library/Product_Vector.thy	Tue Sep 06 17:52:00 2011 +0200
     3.3 @@ -450,7 +450,7 @@
     3.4    assumes x: "0 \<le> x" and y: "0 \<le> y"
     3.5    shows "sqrt (x + y) \<le> sqrt x + sqrt y"
     3.6  apply (rule power2_le_imp_le)
     3.7 -apply (simp add: real_sum_squared_expand x y)
     3.8 +apply (simp add: power2_sum x y)
     3.9  apply (simp add: mult_nonneg_nonneg x y)
    3.10  apply (simp add: x y)
    3.11  done
     4.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Sep 06 16:40:22 2011 +0200
     4.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Sep 06 17:52:00 2011 +0200
     4.3 @@ -415,16 +415,6 @@
     4.4    from power2_le_imp_le[OF th yz] show ?thesis .
     4.5  qed
     4.6  
     4.7 -text {* TODO: move to NthRoot *}
     4.8 -lemma sqrt_add_le_add_sqrt:
     4.9 -  assumes x: "0 \<le> x" and y: "0 \<le> y"
    4.10 -  shows "sqrt (x + y) \<le> sqrt x + sqrt y"
    4.11 -apply (rule power2_le_imp_le)
    4.12 -apply (simp add: real_sum_squared_expand x y)
    4.13 -apply (simp add: mult_nonneg_nonneg x y)
    4.14 -apply (simp add: x y)
    4.15 -done
    4.16 -
    4.17  subsection {* A generic notion of "hull" (convex, affine, conic hull and closure). *}
    4.18  
    4.19  definition hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "hull" 75) where
     5.1 --- a/src/HOL/Transcendental.thy	Tue Sep 06 16:40:22 2011 +0200
     5.2 +++ b/src/HOL/Transcendental.thy	Tue Sep 06 17:52:00 2011 +0200
     5.3 @@ -1722,19 +1722,29 @@
     5.4  lemma sin_ge_zero: "[| 0 \<le> x; x \<le> pi |] ==> 0 \<le> sin x"
     5.5  by (auto simp add: order_le_less sin_gt_zero_pi)
     5.6  
     5.7 +text {* FIXME: This proof is almost identical to lemma @{text cos_is_zero}.
     5.8 +  It should be possible to factor out some of the common parts. *}
     5.9 +
    5.10  lemma cos_total: "[| -1 \<le> y; y \<le> 1 |] ==> EX! x. 0 \<le> x & x \<le> pi & (cos x = y)"
    5.11 -apply (subgoal_tac "\<exists>x. 0 \<le> x & x \<le> pi & cos x = y")
    5.12 -apply (rule_tac [2] IVT2)
    5.13 -apply (auto intro: order_less_imp_le DERIV_isCont DERIV_cos)
    5.14 -apply (cut_tac x = xa and y = y in linorder_less_linear)
    5.15 -apply (rule ccontr, auto)
    5.16 -apply (drule_tac f = cos in Rolle)
    5.17 -apply (drule_tac [5] f = cos in Rolle)
    5.18 -apply (auto intro: order_less_imp_le DERIV_isCont DERIV_cos
    5.19 -            dest!: DERIV_cos [THEN DERIV_unique]
    5.20 -            simp add: differentiable_def)
    5.21 -apply (auto dest: sin_gt_zero_pi [OF order_le_less_trans order_less_le_trans])
    5.22 -done
    5.23 +proof (rule ex_ex1I)
    5.24 +  assume y: "-1 \<le> y" "y \<le> 1"
    5.25 +  show "\<exists>x. 0 \<le> x & x \<le> pi & cos x = y"
    5.26 +    by (rule IVT2, simp_all add: y)
    5.27 +next
    5.28 +  fix a b
    5.29 +  assume a: "0 \<le> a \<and> a \<le> pi \<and> cos a = y"
    5.30 +  assume b: "0 \<le> b \<and> b \<le> pi \<and> cos b = y"
    5.31 +  have [simp]: "\<forall>x. cos differentiable x"
    5.32 +    unfolding differentiable_def by (auto intro: DERIV_cos)
    5.33 +  from a b show "a = b"
    5.34 +    apply (cut_tac less_linear [of a b], auto)
    5.35 +    apply (drule_tac f = cos in Rolle)
    5.36 +    apply (drule_tac [5] f = cos in Rolle)
    5.37 +    apply (auto dest!: DERIV_cos [THEN DERIV_unique])
    5.38 +    apply (metis order_less_le_trans less_le sin_gt_zero_pi)
    5.39 +    apply (metis order_less_le_trans less_le sin_gt_zero_pi)
    5.40 +    done
    5.41 +qed
    5.42  
    5.43  lemma sin_total:
    5.44       "[| -1 \<le> y; y \<le> 1 |] ==> EX! x. -(pi/2) \<le> x & x \<le> pi/2 & (sin x = y)"
    5.45 @@ -2196,15 +2206,24 @@
    5.46  lemma arctan_ubound: "arctan y < pi/2"
    5.47  by (auto simp only: arctan)
    5.48  
    5.49 +lemma arctan_unique:
    5.50 +  assumes "-(pi/2) < x" and "x < pi/2" and "tan x = y"
    5.51 +  shows "arctan y = x"
    5.52 +  using assms arctan [of y] tan_total [of y] by (fast elim: ex1E)
    5.53 +
    5.54  lemma arctan_tan:
    5.55        "[|-(pi/2) < x; x < pi/2 |] ==> arctan(tan x) = x"
    5.56 -apply (unfold arctan_def)
    5.57 -apply (rule the1_equality)
    5.58 -apply (rule tan_total, auto)
    5.59 -done
    5.60 +  by (rule arctan_unique, simp_all)
    5.61  
    5.62  lemma arctan_zero_zero [simp]: "arctan 0 = 0"
    5.63 -by (insert arctan_tan [of 0], simp)
    5.64 +  by (rule arctan_unique, simp_all)
    5.65 +
    5.66 +lemma arctan_minus: "arctan (- x) = - arctan x"
    5.67 +  apply (rule arctan_unique)
    5.68 +  apply (simp only: neg_less_iff_less arctan_ubound)
    5.69 +  apply (metis minus_less_iff arctan_lbound)
    5.70 +  apply simp
    5.71 +  done
    5.72  
    5.73  lemma cos_arctan_not_zero [simp]: "cos (arctan x) \<noteq> 0"
    5.74    by (intro less_imp_neq [symmetric] cos_gt_zero_pi
    5.75 @@ -2235,6 +2254,30 @@
    5.76                    mult_assoc power_inverse [symmetric])
    5.77  done
    5.78  
    5.79 +lemma arctan_less_iff: "arctan x < arctan y \<longleftrightarrow> x < y"
    5.80 +  by (metis tan_monotone' arctan_lbound arctan_ubound tan_arctan)
    5.81 +
    5.82 +lemma arctan_le_iff: "arctan x \<le> arctan y \<longleftrightarrow> x \<le> y"
    5.83 +  by (simp only: not_less [symmetric] arctan_less_iff)
    5.84 +
    5.85 +lemma arctan_eq_iff: "arctan x = arctan y \<longleftrightarrow> x = y"
    5.86 +  by (simp only: eq_iff [where 'a=real] arctan_le_iff)
    5.87 +
    5.88 +lemma zero_less_arctan_iff [simp]: "0 < arctan x \<longleftrightarrow> 0 < x"
    5.89 +  using arctan_less_iff [of 0 x] by simp
    5.90 +
    5.91 +lemma arctan_less_zero_iff [simp]: "arctan x < 0 \<longleftrightarrow> x < 0"
    5.92 +  using arctan_less_iff [of x 0] by simp
    5.93 +
    5.94 +lemma zero_le_arctan_iff [simp]: "0 \<le> arctan x \<longleftrightarrow> 0 \<le> x"
    5.95 +  using arctan_le_iff [of 0 x] by simp
    5.96 +
    5.97 +lemma arctan_le_zero_iff [simp]: "arctan x \<le> 0 \<longleftrightarrow> x \<le> 0"
    5.98 +  using arctan_le_iff [of x 0] by simp
    5.99 +
   5.100 +lemma arctan_eq_zero_iff [simp]: "arctan x = 0 \<longleftrightarrow> x = 0"
   5.101 +  using arctan_eq_iff [of x 0] by simp
   5.102 +
   5.103  lemma isCont_inverse_function2:
   5.104    fixes f g :: "real \<Rightarrow> real" shows
   5.105    "\<lbrakk>a < x; x < b;
   5.106 @@ -2427,98 +2470,34 @@
   5.107  
   5.108  subsection {* Machins formula *}
   5.109  
   5.110 +lemma arctan_one: "arctan 1 = pi / 4"
   5.111 +  by (rule arctan_unique, simp_all add: tan_45 m2pi_less_pi)
   5.112 +
   5.113  lemma tan_total_pi4: assumes "\<bar>x\<bar> < 1"
   5.114    shows "\<exists> z. - (pi / 4) < z \<and> z < pi / 4 \<and> tan z = x"
   5.115 -proof -
   5.116 -  obtain z where "- (pi / 2) < z" and "z < pi / 2" and "tan z = x" using tan_total by blast
   5.117 -  have "tan (pi / 4) = 1" and "tan (- (pi / 4)) = - 1" using tan_45 tan_minus by auto
   5.118 -  have "z \<noteq> pi / 4"
   5.119 -  proof (rule ccontr)
   5.120 -    assume "\<not> (z \<noteq> pi / 4)" hence "z = pi / 4" by auto
   5.121 -    have "tan z = 1" unfolding `z = pi / 4` `tan (pi / 4) = 1` ..
   5.122 -    thus False unfolding `tan z = x` using `\<bar>x\<bar> < 1` by auto
   5.123 -  qed
   5.124 -  have "z \<noteq> - (pi / 4)"
   5.125 -  proof (rule ccontr)
   5.126 -    assume "\<not> (z \<noteq> - (pi / 4))" hence "z = - (pi / 4)" by auto
   5.127 -    have "tan z = - 1" unfolding `z = - (pi / 4)` `tan (- (pi / 4)) = - 1` ..
   5.128 -    thus False unfolding `tan z = x` using `\<bar>x\<bar> < 1` by auto
   5.129 -  qed
   5.130 -
   5.131 -  have "z < pi / 4"
   5.132 -  proof (rule ccontr)
   5.133 -    assume "\<not> (z < pi / 4)" hence "pi / 4 < z" using `z \<noteq> pi / 4` by auto
   5.134 -    have "- (pi / 2) < pi / 4" using m2pi_less_pi by auto
   5.135 -    from tan_monotone[OF this `pi / 4 < z` `z < pi / 2`]
   5.136 -    have "1 < x" unfolding `tan z = x` `tan (pi / 4) = 1` .
   5.137 -    thus False using `\<bar>x\<bar> < 1` by auto
   5.138 -  qed
   5.139 -  moreover
   5.140 -  have "-(pi / 4) < z"
   5.141 -  proof (rule ccontr)
   5.142 -    assume "\<not> (-(pi / 4) < z)" hence "z < - (pi / 4)" using `z \<noteq> - (pi / 4)` by auto
   5.143 -    have "-(pi / 4) < pi / 2" using m2pi_less_pi by auto
   5.144 -    from tan_monotone[OF `-(pi / 2) < z` `z < -(pi / 4)` this]
   5.145 -    have "x < - 1" unfolding `tan z = x` `tan (-(pi / 4)) = - 1` .
   5.146 -    thus False using `\<bar>x\<bar> < 1` by auto
   5.147 -  qed
   5.148 -  ultimately show ?thesis using `tan z = x` by auto
   5.149 +proof
   5.150 +  show "- (pi / 4) < arctan x \<and> arctan x < pi / 4 \<and> tan (arctan x) = x"
   5.151 +    unfolding arctan_one [symmetric] arctan_minus [symmetric]
   5.152 +    unfolding arctan_less_iff using assms by auto
   5.153  qed
   5.154  
   5.155  lemma arctan_add: assumes "\<bar>x\<bar> \<le> 1" and "\<bar>y\<bar> < 1"
   5.156    shows "arctan x + arctan y = arctan ((x + y) / (1 - x * y))"
   5.157 -proof -
   5.158 -  obtain y' where "-(pi/4) < y'" and "y' < pi/4" and "tan y' = y" using tan_total_pi4[OF `\<bar>y\<bar> < 1`] by blast
   5.159 -
   5.160 -  have "pi / 4 < pi / 2" by auto
   5.161 -
   5.162 -  have "\<exists> x'. -(pi/4) \<le> x' \<and> x' \<le> pi/4 \<and> tan x' = x"
   5.163 -  proof (cases "\<bar>x\<bar> < 1")
   5.164 -    case True from tan_total_pi4[OF this] obtain x' where "-(pi/4) < x'" and "x' < pi/4" and "tan x' = x" by blast
   5.165 -    hence "-(pi/4) \<le> x'" and "x' \<le> pi/4" and "tan x' = x" by auto
   5.166 -    thus ?thesis by auto
   5.167 -  next
   5.168 -    case False
   5.169 -    show ?thesis
   5.170 -    proof (cases "x = 1")
   5.171 -      case True hence "tan (pi/4) = x" using tan_45 by auto
   5.172 -      moreover
   5.173 -      have "- pi \<le> pi" unfolding minus_le_self_iff by auto
   5.174 -      hence "-(pi/4) \<le> pi/4" and "pi/4 \<le> pi/4" by auto
   5.175 -      ultimately show ?thesis by blast
   5.176 -    next
   5.177 -      case False hence "x = -1" using `\<not> \<bar>x\<bar> < 1` and `\<bar>x\<bar> \<le> 1` by auto
   5.178 -      hence "tan (-(pi/4)) = x" using tan_45 tan_minus by auto
   5.179 -      moreover
   5.180 -      have "- pi \<le> pi" unfolding minus_le_self_iff by auto
   5.181 -      hence "-(pi/4) \<le> pi/4" and "-(pi/4) \<le> -(pi/4)" by auto
   5.182 -      ultimately show ?thesis by blast
   5.183 -    qed
   5.184 -  qed
   5.185 -  then obtain x' where "-(pi/4) \<le> x'" and "x' \<le> pi/4" and "tan x' = x" by blast
   5.186 -  hence "-(pi/2) < x'" and "x' < pi/2" using order_le_less_trans[OF `x' \<le> pi/4` `pi / 4 < pi / 2`] by auto
   5.187 -
   5.188 -  have "cos x' \<noteq> 0" using cos_gt_zero_pi[THEN less_imp_neq] and `-(pi/2) < x'` and `x' < pi/2` by auto
   5.189 -  moreover have "cos y' \<noteq> 0" using cos_gt_zero_pi[THEN less_imp_neq] and `-(pi/4) < y'` and `y' < pi/4` by auto
   5.190 -  ultimately have "cos x' * cos y' \<noteq> 0" by auto
   5.191 -
   5.192 -  have divide_nonzero_divide: "\<And> A B C :: real. C \<noteq> 0 \<Longrightarrow> (A / C) / (B / C) = A / B" by auto
   5.193 -  have divide_mult_commute: "\<And> A B C D :: real. A * B / (C * D) = (A / C) * (B / D)" by auto
   5.194 -
   5.195 -  have "tan (x' + y') = sin (x' + y') / (cos x' * cos y' - sin x' * sin y')" unfolding tan_def cos_add ..
   5.196 -  also have "\<dots> = (tan x' + tan y') / ((cos x' * cos y' - sin x' * sin y') / (cos x' * cos y'))" unfolding add_tan_eq[OF `cos x' \<noteq> 0` `cos y' \<noteq> 0`] divide_nonzero_divide[OF `cos x' * cos y' \<noteq> 0`] ..
   5.197 -  also have "\<dots> = (tan x' + tan y') / (1 - tan x' * tan y')" unfolding tan_def diff_divide_distrib divide_self[OF `cos x' * cos y' \<noteq> 0`] unfolding divide_mult_commute ..
   5.198 -  finally have tan_eq: "tan (x' + y') = (x + y) / (1 - x * y)" unfolding `tan y' = y` `tan x' = x` .
   5.199 -
   5.200 -  have "arctan (tan (x' + y')) = x' + y'" using `-(pi/4) < y'` `-(pi/4) \<le> x'` `y' < pi/4` and `x' \<le> pi/4` by (auto intro!: arctan_tan)
   5.201 -  moreover have "arctan (tan (x')) = x'" using `-(pi/2) < x'` and `x' < pi/2` by (auto intro!: arctan_tan)
   5.202 -  moreover have "arctan (tan (y')) = y'" using `-(pi/4) < y'` and `y' < pi/4` by (auto intro!: arctan_tan)
   5.203 -  ultimately have "arctan x + arctan y = arctan (tan (x' + y'))" unfolding `tan y' = y` [symmetric] `tan x' = x`[symmetric] by auto
   5.204 -  thus "arctan x + arctan y = arctan ((x + y) / (1 - x * y))" unfolding tan_eq .
   5.205 +proof (rule arctan_unique [symmetric])
   5.206 +  have "- (pi / 4) \<le> arctan x" and "- (pi / 4) < arctan y"
   5.207 +    unfolding arctan_one [symmetric] arctan_minus [symmetric]
   5.208 +    unfolding arctan_le_iff arctan_less_iff using assms by auto
   5.209 +  from add_le_less_mono [OF this]
   5.210 +  show 1: "- (pi / 2) < arctan x + arctan y" by simp
   5.211 +  have "arctan x \<le> pi / 4" and "arctan y < pi / 4"
   5.212 +    unfolding arctan_one [symmetric]
   5.213 +    unfolding arctan_le_iff arctan_less_iff using assms by auto
   5.214 +  from add_le_less_mono [OF this]
   5.215 +  show 2: "arctan x + arctan y < pi / 2" by simp
   5.216 +  show "tan (arctan x + arctan y) = (x + y) / (1 - x * y)"
   5.217 +    using cos_gt_zero_pi [OF 1 2] by (simp add: tan_add)
   5.218  qed
   5.219  
   5.220 -lemma arctan1_eq_pi4: "arctan 1 = pi / 4" unfolding tan_45[symmetric] by (rule arctan_tan, auto simp add: m2pi_less_pi)
   5.221 -
   5.222  theorem machin: "pi / 4 = 4 * arctan (1/5) - arctan (1 / 239)"
   5.223  proof -
   5.224    have "\<bar>1 / 5\<bar> < (1 :: real)" by auto
   5.225 @@ -2533,8 +2512,9 @@
   5.226    from arctan_add[OF this]
   5.227    have "arctan 1 + arctan (1 / 239) = arctan (120 / 119)" by auto
   5.228    ultimately have "arctan 1 + arctan (1 / 239) = 4 * arctan (1 / 5)" by auto
   5.229 -  thus ?thesis unfolding arctan1_eq_pi4 by algebra
   5.230 +  thus ?thesis unfolding arctan_one by algebra
   5.231  qed
   5.232 +
   5.233  subsection {* Introducing the arcus tangens power series *}
   5.234  
   5.235  lemma monoseq_arctan_series: fixes x :: real
   5.236 @@ -2827,65 +2807,34 @@
   5.237  
   5.238  lemma arctan_monotone: assumes "x < y"
   5.239    shows "arctan x < arctan y"
   5.240 -proof -
   5.241 -  obtain z where "-(pi / 2) < z" and "z < pi / 2" and "tan z = x" using tan_total by blast
   5.242 -  obtain w where "-(pi / 2) < w" and "w < pi / 2" and "tan w = y" using tan_total by blast
   5.243 -  have "z < w" unfolding tan_monotone'[OF `-(pi / 2) < z` `z < pi / 2` `-(pi / 2) < w` `w < pi / 2`] `tan z = x` `tan w = y` using `x < y` .
   5.244 -  thus ?thesis
   5.245 -    unfolding `tan z = x`[symmetric] arctan_tan[OF `-(pi / 2) < z` `z < pi / 2`]
   5.246 -    unfolding `tan w = y`[symmetric] arctan_tan[OF `-(pi / 2) < w` `w < pi / 2`] .
   5.247 -qed
   5.248 +  using assms by (simp only: arctan_less_iff)
   5.249  
   5.250  lemma arctan_monotone': assumes "x \<le> y" shows "arctan x \<le> arctan y"
   5.251 -proof (cases "x = y")
   5.252 -  case False hence "x < y" using `x \<le> y` by auto from arctan_monotone[OF this] show ?thesis by auto
   5.253 -qed auto
   5.254 -
   5.255 -lemma arctan_minus: "arctan (- x) = - arctan x"
   5.256 -proof -
   5.257 -  obtain y where "- (pi / 2) < y" and "y < pi / 2" and "tan y = x" using tan_total by blast
   5.258 -  thus ?thesis unfolding `tan y = x`[symmetric] tan_minus[symmetric] using arctan_tan[of y] arctan_tan[of "-y"] by auto
   5.259 -qed
   5.260 -
   5.261 -lemma arctan_inverse: assumes "x \<noteq> 0" shows "arctan (1 / x) = sgn x * pi / 2 - arctan x"
   5.262 -proof -
   5.263 -  obtain y where "- (pi / 2) < y" and "y < pi / 2" and "tan y = x" using tan_total by blast
   5.264 -  hence "y = arctan x" unfolding `tan y = x`[symmetric] using arctan_tan by auto
   5.265 -
   5.266 -  { fix y x :: real assume "0 < y" and "y < pi /2" and "y = arctan x" and "tan y = x" hence "- (pi / 2) < y" by auto
   5.267 -    have "tan y > 0" using tan_monotone'[OF _ _ `- (pi / 2) < y` `y < pi / 2`, of 0] tan_zero `0 < y` by auto
   5.268 -    hence "x > 0" using `tan y = x` by auto
   5.269 -
   5.270 -    have "- (pi / 2) < pi / 2 - y" using `y > 0` `y < pi / 2` by auto
   5.271 -    moreover have "pi / 2 - y < pi / 2" using `y > 0` `y < pi / 2` by auto
   5.272 -    ultimately have "arctan (1 / x) = pi / 2 - y" unfolding `tan y = x`[symmetric] tan_inverse using arctan_tan by auto
   5.273 -    hence "arctan (1 / x) = sgn x * pi / 2 - arctan x" unfolding `y = arctan x` real_sgn_pos[OF `x > 0`] by auto
   5.274 -  } note pos_y = this
   5.275 -
   5.276 -  show ?thesis
   5.277 -  proof (cases "y > 0")
   5.278 -    case True from pos_y[OF this `y < pi / 2` `y = arctan x` `tan y = x`] show ?thesis .
   5.279 -  next
   5.280 -    case False hence "y \<le> 0" by auto
   5.281 -    moreover have "y \<noteq> 0"
   5.282 -    proof (rule ccontr)
   5.283 -      assume "\<not> y \<noteq> 0" hence "y = 0" by auto
   5.284 -      have "x = 0" unfolding `tan y = x`[symmetric] `y = 0` tan_zero ..
   5.285 -      thus False using `x \<noteq> 0` by auto
   5.286 -    qed
   5.287 -    ultimately have "y < 0" by auto
   5.288 -    hence "0 < - y" and "-y < pi / 2" using `- (pi / 2) < y` by auto
   5.289 -    moreover have "-y = arctan (-x)" unfolding arctan_minus `y = arctan x` ..
   5.290 -    moreover have "tan (-y) = -x" unfolding tan_minus `tan y = x` ..
   5.291 -    ultimately have "arctan (1 / -x) = sgn (-x) * pi / 2 - arctan (-x)" using pos_y by blast
   5.292 -    hence "arctan (- (1 / x)) = - (sgn x * pi / 2 - arctan x)" unfolding arctan_minus[of x] divide_minus_right sgn_minus by auto
   5.293 -    thus ?thesis unfolding arctan_minus neg_equal_iff_equal .
   5.294 -  qed
   5.295 +  using assms by (simp only: arctan_le_iff)
   5.296 +
   5.297 +lemma arctan_inverse:
   5.298 +  assumes "x \<noteq> 0" shows "arctan (1 / x) = sgn x * pi / 2 - arctan x"
   5.299 +proof (rule arctan_unique)
   5.300 +  show "- (pi / 2) < sgn x * pi / 2 - arctan x"
   5.301 +    using arctan_bounded [of x] assms
   5.302 +    unfolding sgn_real_def
   5.303 +    apply (auto simp add: algebra_simps)
   5.304 +    apply (drule zero_less_arctan_iff [THEN iffD2])
   5.305 +    apply arith
   5.306 +    done
   5.307 +  show "sgn x * pi / 2 - arctan x < pi / 2"
   5.308 +    using arctan_bounded [of "- x"] assms
   5.309 +    unfolding sgn_real_def arctan_minus
   5.310 +    by auto
   5.311 +  show "tan (sgn x * pi / 2 - arctan x) = 1 / x"
   5.312 +    unfolding tan_inverse [of "arctan x", unfolded tan_arctan]
   5.313 +    unfolding sgn_real_def
   5.314 +    by (simp add: tan_def cos_arctan sin_arctan sin_diff cos_diff)
   5.315  qed
   5.316  
   5.317  theorem pi_series: "pi / 4 = (\<Sum> k. (-1)^k * 1 / real (k*2+1))" (is "_ = ?SUM")
   5.318  proof -
   5.319 -  have "pi / 4 = arctan 1" using arctan1_eq_pi4 by auto
   5.320 +  have "pi / 4 = arctan 1" using arctan_one by auto
   5.321    also have "\<dots> = ?SUM" using arctan_series[of 1] by auto
   5.322    finally show ?thesis by auto
   5.323  qed