add lemmas about arctan;
authorhuffman
Mon Sep 05 22:30:25 2011 -0700 (2011-09-05)
changeset 447469e4f7d3b5376
parent 44745 b068207a7400
child 44747 ab7522fbe1a2
add lemmas about arctan;
simplify some proofs about arctan;
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Transcendental.thy	Mon Sep 05 18:06:02 2011 -0700
     1.2 +++ b/src/HOL/Transcendental.thy	Mon Sep 05 22:30:25 2011 -0700
     1.3 @@ -2206,15 +2206,24 @@
     1.4  lemma arctan_ubound: "arctan y < pi/2"
     1.5  by (auto simp only: arctan)
     1.6  
     1.7 +lemma arctan_unique:
     1.8 +  assumes "-(pi/2) < x" and "x < pi/2" and "tan x = y"
     1.9 +  shows "arctan y = x"
    1.10 +  using assms arctan [of y] tan_total [of y] by (fast elim: ex1E)
    1.11 +
    1.12  lemma arctan_tan:
    1.13        "[|-(pi/2) < x; x < pi/2 |] ==> arctan(tan x) = x"
    1.14 -apply (unfold arctan_def)
    1.15 -apply (rule the1_equality)
    1.16 -apply (rule tan_total, auto)
    1.17 -done
    1.18 +  by (rule arctan_unique, simp_all)
    1.19  
    1.20  lemma arctan_zero_zero [simp]: "arctan 0 = 0"
    1.21 -by (insert arctan_tan [of 0], simp)
    1.22 +  by (rule arctan_unique, simp_all)
    1.23 +
    1.24 +lemma arctan_minus: "arctan (- x) = - arctan x"
    1.25 +  apply (rule arctan_unique)
    1.26 +  apply (simp only: neg_less_iff_less arctan_ubound)
    1.27 +  apply (metis minus_less_iff arctan_lbound)
    1.28 +  apply simp
    1.29 +  done
    1.30  
    1.31  lemma cos_arctan_not_zero [simp]: "cos (arctan x) \<noteq> 0"
    1.32    by (intro less_imp_neq [symmetric] cos_gt_zero_pi
    1.33 @@ -2245,6 +2254,30 @@
    1.34                    mult_assoc power_inverse [symmetric])
    1.35  done
    1.36  
    1.37 +lemma arctan_less_iff: "arctan x < arctan y \<longleftrightarrow> x < y"
    1.38 +  by (metis tan_monotone' arctan_lbound arctan_ubound tan_arctan)
    1.39 +
    1.40 +lemma arctan_le_iff: "arctan x \<le> arctan y \<longleftrightarrow> x \<le> y"
    1.41 +  by (simp only: not_less [symmetric] arctan_less_iff)
    1.42 +
    1.43 +lemma arctan_eq_iff: "arctan x = arctan y \<longleftrightarrow> x = y"
    1.44 +  by (simp only: eq_iff [where 'a=real] arctan_le_iff)
    1.45 +
    1.46 +lemma zero_less_arctan_iff [simp]: "0 < arctan x \<longleftrightarrow> 0 < x"
    1.47 +  using arctan_less_iff [of 0 x] by simp
    1.48 +
    1.49 +lemma arctan_less_zero_iff [simp]: "arctan x < 0 \<longleftrightarrow> x < 0"
    1.50 +  using arctan_less_iff [of x 0] by simp
    1.51 +
    1.52 +lemma zero_le_arctan_iff [simp]: "0 \<le> arctan x \<longleftrightarrow> 0 \<le> x"
    1.53 +  using arctan_le_iff [of 0 x] by simp
    1.54 +
    1.55 +lemma arctan_le_zero_iff [simp]: "arctan x \<le> 0 \<longleftrightarrow> x \<le> 0"
    1.56 +  using arctan_le_iff [of x 0] by simp
    1.57 +
    1.58 +lemma arctan_eq_zero_iff [simp]: "arctan x = 0 \<longleftrightarrow> x = 0"
    1.59 +  using arctan_eq_iff [of x 0] by simp
    1.60 +
    1.61  lemma isCont_inverse_function2:
    1.62    fixes f g :: "real \<Rightarrow> real" shows
    1.63    "\<lbrakk>a < x; x < b;
    1.64 @@ -2437,98 +2470,34 @@
    1.65  
    1.66  subsection {* Machins formula *}
    1.67  
    1.68 +lemma arctan_one: "arctan 1 = pi / 4"
    1.69 +  by (rule arctan_unique, simp_all add: tan_45 m2pi_less_pi)
    1.70 +
    1.71  lemma tan_total_pi4: assumes "\<bar>x\<bar> < 1"
    1.72    shows "\<exists> z. - (pi / 4) < z \<and> z < pi / 4 \<and> tan z = x"
    1.73 -proof -
    1.74 -  obtain z where "- (pi / 2) < z" and "z < pi / 2" and "tan z = x" using tan_total by blast
    1.75 -  have "tan (pi / 4) = 1" and "tan (- (pi / 4)) = - 1" using tan_45 tan_minus by auto
    1.76 -  have "z \<noteq> pi / 4"
    1.77 -  proof (rule ccontr)
    1.78 -    assume "\<not> (z \<noteq> pi / 4)" hence "z = pi / 4" by auto
    1.79 -    have "tan z = 1" unfolding `z = pi / 4` `tan (pi / 4) = 1` ..
    1.80 -    thus False unfolding `tan z = x` using `\<bar>x\<bar> < 1` by auto
    1.81 -  qed
    1.82 -  have "z \<noteq> - (pi / 4)"
    1.83 -  proof (rule ccontr)
    1.84 -    assume "\<not> (z \<noteq> - (pi / 4))" hence "z = - (pi / 4)" by auto
    1.85 -    have "tan z = - 1" unfolding `z = - (pi / 4)` `tan (- (pi / 4)) = - 1` ..
    1.86 -    thus False unfolding `tan z = x` using `\<bar>x\<bar> < 1` by auto
    1.87 -  qed
    1.88 -
    1.89 -  have "z < pi / 4"
    1.90 -  proof (rule ccontr)
    1.91 -    assume "\<not> (z < pi / 4)" hence "pi / 4 < z" using `z \<noteq> pi / 4` by auto
    1.92 -    have "- (pi / 2) < pi / 4" using m2pi_less_pi by auto
    1.93 -    from tan_monotone[OF this `pi / 4 < z` `z < pi / 2`]
    1.94 -    have "1 < x" unfolding `tan z = x` `tan (pi / 4) = 1` .
    1.95 -    thus False using `\<bar>x\<bar> < 1` by auto
    1.96 -  qed
    1.97 -  moreover
    1.98 -  have "-(pi / 4) < z"
    1.99 -  proof (rule ccontr)
   1.100 -    assume "\<not> (-(pi / 4) < z)" hence "z < - (pi / 4)" using `z \<noteq> - (pi / 4)` by auto
   1.101 -    have "-(pi / 4) < pi / 2" using m2pi_less_pi by auto
   1.102 -    from tan_monotone[OF `-(pi / 2) < z` `z < -(pi / 4)` this]
   1.103 -    have "x < - 1" unfolding `tan z = x` `tan (-(pi / 4)) = - 1` .
   1.104 -    thus False using `\<bar>x\<bar> < 1` by auto
   1.105 -  qed
   1.106 -  ultimately show ?thesis using `tan z = x` by auto
   1.107 +proof
   1.108 +  show "- (pi / 4) < arctan x \<and> arctan x < pi / 4 \<and> tan (arctan x) = x"
   1.109 +    unfolding arctan_one [symmetric] arctan_minus [symmetric]
   1.110 +    unfolding arctan_less_iff using assms by auto
   1.111  qed
   1.112  
   1.113  lemma arctan_add: assumes "\<bar>x\<bar> \<le> 1" and "\<bar>y\<bar> < 1"
   1.114    shows "arctan x + arctan y = arctan ((x + y) / (1 - x * y))"
   1.115 -proof -
   1.116 -  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
   1.117 -
   1.118 -  have "pi / 4 < pi / 2" by auto
   1.119 -
   1.120 -  have "\<exists> x'. -(pi/4) \<le> x' \<and> x' \<le> pi/4 \<and> tan x' = x"
   1.121 -  proof (cases "\<bar>x\<bar> < 1")
   1.122 -    case True from tan_total_pi4[OF this] obtain x' where "-(pi/4) < x'" and "x' < pi/4" and "tan x' = x" by blast
   1.123 -    hence "-(pi/4) \<le> x'" and "x' \<le> pi/4" and "tan x' = x" by auto
   1.124 -    thus ?thesis by auto
   1.125 -  next
   1.126 -    case False
   1.127 -    show ?thesis
   1.128 -    proof (cases "x = 1")
   1.129 -      case True hence "tan (pi/4) = x" using tan_45 by auto
   1.130 -      moreover
   1.131 -      have "- pi \<le> pi" unfolding minus_le_self_iff by auto
   1.132 -      hence "-(pi/4) \<le> pi/4" and "pi/4 \<le> pi/4" by auto
   1.133 -      ultimately show ?thesis by blast
   1.134 -    next
   1.135 -      case False hence "x = -1" using `\<not> \<bar>x\<bar> < 1` and `\<bar>x\<bar> \<le> 1` by auto
   1.136 -      hence "tan (-(pi/4)) = x" using tan_45 tan_minus by auto
   1.137 -      moreover
   1.138 -      have "- pi \<le> pi" unfolding minus_le_self_iff by auto
   1.139 -      hence "-(pi/4) \<le> pi/4" and "-(pi/4) \<le> -(pi/4)" by auto
   1.140 -      ultimately show ?thesis by blast
   1.141 -    qed
   1.142 -  qed
   1.143 -  then obtain x' where "-(pi/4) \<le> x'" and "x' \<le> pi/4" and "tan x' = x" by blast
   1.144 -  hence "-(pi/2) < x'" and "x' < pi/2" using order_le_less_trans[OF `x' \<le> pi/4` `pi / 4 < pi / 2`] by auto
   1.145 -
   1.146 -  have "cos x' \<noteq> 0" using cos_gt_zero_pi[THEN less_imp_neq] and `-(pi/2) < x'` and `x' < pi/2` by auto
   1.147 -  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
   1.148 -  ultimately have "cos x' * cos y' \<noteq> 0" by auto
   1.149 -
   1.150 -  have divide_nonzero_divide: "\<And> A B C :: real. C \<noteq> 0 \<Longrightarrow> (A / C) / (B / C) = A / B" by auto
   1.151 -  have divide_mult_commute: "\<And> A B C D :: real. A * B / (C * D) = (A / C) * (B / D)" by auto
   1.152 -
   1.153 -  have "tan (x' + y') = sin (x' + y') / (cos x' * cos y' - sin x' * sin y')" unfolding tan_def cos_add ..
   1.154 -  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`] ..
   1.155 -  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 ..
   1.156 -  finally have tan_eq: "tan (x' + y') = (x + y) / (1 - x * y)" unfolding `tan y' = y` `tan x' = x` .
   1.157 -
   1.158 -  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)
   1.159 -  moreover have "arctan (tan (x')) = x'" using `-(pi/2) < x'` and `x' < pi/2` by (auto intro!: arctan_tan)
   1.160 -  moreover have "arctan (tan (y')) = y'" using `-(pi/4) < y'` and `y' < pi/4` by (auto intro!: arctan_tan)
   1.161 -  ultimately have "arctan x + arctan y = arctan (tan (x' + y'))" unfolding `tan y' = y` [symmetric] `tan x' = x`[symmetric] by auto
   1.162 -  thus "arctan x + arctan y = arctan ((x + y) / (1 - x * y))" unfolding tan_eq .
   1.163 +proof (rule arctan_unique [symmetric])
   1.164 +  have "- (pi / 4) \<le> arctan x" and "- (pi / 4) < arctan y"
   1.165 +    unfolding arctan_one [symmetric] arctan_minus [symmetric]
   1.166 +    unfolding arctan_le_iff arctan_less_iff using assms by auto
   1.167 +  from add_le_less_mono [OF this]
   1.168 +  show 1: "- (pi / 2) < arctan x + arctan y" by simp
   1.169 +  have "arctan x \<le> pi / 4" and "arctan y < pi / 4"
   1.170 +    unfolding arctan_one [symmetric]
   1.171 +    unfolding arctan_le_iff arctan_less_iff using assms by auto
   1.172 +  from add_le_less_mono [OF this]
   1.173 +  show 2: "arctan x + arctan y < pi / 2" by simp
   1.174 +  show "tan (arctan x + arctan y) = (x + y) / (1 - x * y)"
   1.175 +    using cos_gt_zero_pi [OF 1 2] by (simp add: tan_add)
   1.176  qed
   1.177  
   1.178 -lemma arctan1_eq_pi4: "arctan 1 = pi / 4" unfolding tan_45[symmetric] by (rule arctan_tan, auto simp add: m2pi_less_pi)
   1.179 -
   1.180  theorem machin: "pi / 4 = 4 * arctan (1/5) - arctan (1 / 239)"
   1.181  proof -
   1.182    have "\<bar>1 / 5\<bar> < (1 :: real)" by auto
   1.183 @@ -2543,8 +2512,9 @@
   1.184    from arctan_add[OF this]
   1.185    have "arctan 1 + arctan (1 / 239) = arctan (120 / 119)" by auto
   1.186    ultimately have "arctan 1 + arctan (1 / 239) = 4 * arctan (1 / 5)" by auto
   1.187 -  thus ?thesis unfolding arctan1_eq_pi4 by algebra
   1.188 +  thus ?thesis unfolding arctan_one by algebra
   1.189  qed
   1.190 +
   1.191  subsection {* Introducing the arcus tangens power series *}
   1.192  
   1.193  lemma monoseq_arctan_series: fixes x :: real
   1.194 @@ -2837,65 +2807,34 @@
   1.195  
   1.196  lemma arctan_monotone: assumes "x < y"
   1.197    shows "arctan x < arctan y"
   1.198 -proof -
   1.199 -  obtain z where "-(pi / 2) < z" and "z < pi / 2" and "tan z = x" using tan_total by blast
   1.200 -  obtain w where "-(pi / 2) < w" and "w < pi / 2" and "tan w = y" using tan_total by blast
   1.201 -  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` .
   1.202 -  thus ?thesis
   1.203 -    unfolding `tan z = x`[symmetric] arctan_tan[OF `-(pi / 2) < z` `z < pi / 2`]
   1.204 -    unfolding `tan w = y`[symmetric] arctan_tan[OF `-(pi / 2) < w` `w < pi / 2`] .
   1.205 -qed
   1.206 +  using assms by (simp only: arctan_less_iff)
   1.207  
   1.208  lemma arctan_monotone': assumes "x \<le> y" shows "arctan x \<le> arctan y"
   1.209 -proof (cases "x = y")
   1.210 -  case False hence "x < y" using `x \<le> y` by auto from arctan_monotone[OF this] show ?thesis by auto
   1.211 -qed auto
   1.212 -
   1.213 -lemma arctan_minus: "arctan (- x) = - arctan x"
   1.214 -proof -
   1.215 -  obtain y where "- (pi / 2) < y" and "y < pi / 2" and "tan y = x" using tan_total by blast
   1.216 -  thus ?thesis unfolding `tan y = x`[symmetric] tan_minus[symmetric] using arctan_tan[of y] arctan_tan[of "-y"] by auto
   1.217 -qed
   1.218 -
   1.219 -lemma arctan_inverse: assumes "x \<noteq> 0" shows "arctan (1 / x) = sgn x * pi / 2 - arctan x"
   1.220 -proof -
   1.221 -  obtain y where "- (pi / 2) < y" and "y < pi / 2" and "tan y = x" using tan_total by blast
   1.222 -  hence "y = arctan x" unfolding `tan y = x`[symmetric] using arctan_tan by auto
   1.223 -
   1.224 -  { 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
   1.225 -    have "tan y > 0" using tan_monotone'[OF _ _ `- (pi / 2) < y` `y < pi / 2`, of 0] tan_zero `0 < y` by auto
   1.226 -    hence "x > 0" using `tan y = x` by auto
   1.227 -
   1.228 -    have "- (pi / 2) < pi / 2 - y" using `y > 0` `y < pi / 2` by auto
   1.229 -    moreover have "pi / 2 - y < pi / 2" using `y > 0` `y < pi / 2` by auto
   1.230 -    ultimately have "arctan (1 / x) = pi / 2 - y" unfolding `tan y = x`[symmetric] tan_inverse using arctan_tan by auto
   1.231 -    hence "arctan (1 / x) = sgn x * pi / 2 - arctan x" unfolding `y = arctan x` real_sgn_pos[OF `x > 0`] by auto
   1.232 -  } note pos_y = this
   1.233 -
   1.234 -  show ?thesis
   1.235 -  proof (cases "y > 0")
   1.236 -    case True from pos_y[OF this `y < pi / 2` `y = arctan x` `tan y = x`] show ?thesis .
   1.237 -  next
   1.238 -    case False hence "y \<le> 0" by auto
   1.239 -    moreover have "y \<noteq> 0"
   1.240 -    proof (rule ccontr)
   1.241 -      assume "\<not> y \<noteq> 0" hence "y = 0" by auto
   1.242 -      have "x = 0" unfolding `tan y = x`[symmetric] `y = 0` tan_zero ..
   1.243 -      thus False using `x \<noteq> 0` by auto
   1.244 -    qed
   1.245 -    ultimately have "y < 0" by auto
   1.246 -    hence "0 < - y" and "-y < pi / 2" using `- (pi / 2) < y` by auto
   1.247 -    moreover have "-y = arctan (-x)" unfolding arctan_minus `y = arctan x` ..
   1.248 -    moreover have "tan (-y) = -x" unfolding tan_minus `tan y = x` ..
   1.249 -    ultimately have "arctan (1 / -x) = sgn (-x) * pi / 2 - arctan (-x)" using pos_y by blast
   1.250 -    hence "arctan (- (1 / x)) = - (sgn x * pi / 2 - arctan x)" unfolding arctan_minus[of x] divide_minus_right sgn_minus by auto
   1.251 -    thus ?thesis unfolding arctan_minus neg_equal_iff_equal .
   1.252 -  qed
   1.253 +  using assms by (simp only: arctan_le_iff)
   1.254 +
   1.255 +lemma arctan_inverse:
   1.256 +  assumes "x \<noteq> 0" shows "arctan (1 / x) = sgn x * pi / 2 - arctan x"
   1.257 +proof (rule arctan_unique)
   1.258 +  show "- (pi / 2) < sgn x * pi / 2 - arctan x"
   1.259 +    using arctan_bounded [of x] assms
   1.260 +    unfolding sgn_real_def
   1.261 +    apply (auto simp add: algebra_simps)
   1.262 +    apply (drule zero_less_arctan_iff [THEN iffD2])
   1.263 +    apply arith
   1.264 +    done
   1.265 +  show "sgn x * pi / 2 - arctan x < pi / 2"
   1.266 +    using arctan_bounded [of "- x"] assms
   1.267 +    unfolding sgn_real_def arctan_minus
   1.268 +    by auto
   1.269 +  show "tan (sgn x * pi / 2 - arctan x) = 1 / x"
   1.270 +    unfolding tan_inverse [of "arctan x", unfolded tan_arctan]
   1.271 +    unfolding sgn_real_def
   1.272 +    by (simp add: tan_def cos_arctan sin_arctan sin_diff cos_diff)
   1.273  qed
   1.274  
   1.275  theorem pi_series: "pi / 4 = (\<Sum> k. (-1)^k * 1 / real (k*2+1))" (is "_ = ?SUM")
   1.276  proof -
   1.277 -  have "pi / 4 = arctan 1" using arctan1_eq_pi4 by auto
   1.278 +  have "pi / 4 = arctan 1" using arctan_one by auto
   1.279    also have "\<dots> = ?SUM" using arctan_series[of 1] by auto
   1.280    finally show ?thesis by auto
   1.281  qed