src/HOL/Transcendental.thy
changeset 59869 3b5b53eb78ba
parent 59867 58043346ca64
child 60017 b785d6d06430
     1.1 --- a/src/HOL/Transcendental.thy	Tue Mar 31 21:54:32 2015 +0200
     1.2 +++ b/src/HOL/Transcendental.thy	Wed Apr 01 14:08:17 2015 +0100
     1.3 @@ -4013,6 +4013,27 @@
     1.4    apply (rule sin_total, auto)
     1.5    done
     1.6  
     1.7 +lemma arcsin_0 [simp]: "arcsin 0 = 0"
     1.8 +  using arcsin_sin [of 0]
     1.9 +  by simp
    1.10 +
    1.11 +lemma arcsin_1 [simp]: "arcsin 1 = pi/2"
    1.12 +  using arcsin_sin [of "pi/2"]
    1.13 +  by simp
    1.14 +
    1.15 +lemma arcsin_minus_1 [simp]: "arcsin (-1) = - (pi/2)"
    1.16 +  using arcsin_sin [of "-pi/2"]
    1.17 +  by simp
    1.18 +
    1.19 +lemma arcsin_minus: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin(-x) = -arcsin x"
    1.20 +  by (metis (no_types, hide_lams) arcsin arcsin_sin minus_minus neg_le_iff_le sin_minus)
    1.21 +
    1.22 +lemma arcsin_eq_iff: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> (arcsin x = arcsin y \<longleftrightarrow> x = y)"
    1.23 +  by (metis abs_le_interval_iff arcsin)
    1.24 +
    1.25 +lemma cos_arcsin_nonzero: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> cos(arcsin x) \<noteq> 0"
    1.26 +  using arcsin_lt_bounded cos_gt_zero_pi by force
    1.27 +
    1.28  lemma arccos:
    1.29       "\<lbrakk>-1 \<le> y; y \<le> 1\<rbrakk>
    1.30        \<Longrightarrow> 0 \<le> arccos y & arccos y \<le> pi & cos(arccos y) = y"
    1.31 @@ -4031,8 +4052,7 @@
    1.32    by (blast dest: arccos)
    1.33  
    1.34  lemma arccos_lt_bounded:
    1.35 -     "\<lbrakk>-1 < y; y < 1\<rbrakk>
    1.36 -      \<Longrightarrow> 0 < arccos y & arccos y < pi"
    1.37 +     "\<lbrakk>-1 < y; y < 1\<rbrakk> \<Longrightarrow> 0 < arccos y & arccos y < pi"
    1.38    apply (frule order_less_imp_le)
    1.39    apply (frule_tac y = y in order_less_imp_le)
    1.40    apply (frule arccos_bounded, auto)
    1.41 @@ -4081,17 +4101,27 @@
    1.42  lemma arccos_1 [simp]: "arccos 1 = 0"
    1.43    using arccos_cos by force
    1.44  
    1.45 -lemma arctan [simp]: "- (pi/2) < arctan y  & arctan y < pi/2 & tan (arctan y) = y"
    1.46 +lemma arccos_minus_1 [simp]: "arccos(-1) = pi"
    1.47 +  by (metis arccos_cos cos_pi order_refl pi_ge_zero)
    1.48 +
    1.49 +lemma arccos_minus: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos(-x) = pi - arccos x"
    1.50 +  by (metis arccos_cos arccos_cos2 cos_minus_pi cos_total diff_le_0_iff_le le_add_same_cancel1 
    1.51 +    minus_diff_eq uminus_add_conv_diff)
    1.52 +
    1.53 +lemma sin_arccos_nonzero: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> ~(sin(arccos x) = 0)"
    1.54 +  using arccos_lt_bounded sin_gt_zero by force
    1.55 +
    1.56 +lemma arctan: "- (pi/2) < arctan y  & arctan y < pi/2 & tan (arctan y) = y"
    1.57    unfolding arctan_def by (rule theI' [OF tan_total])
    1.58  
    1.59  lemma tan_arctan: "tan (arctan y) = y"
    1.60 -  by auto
    1.61 +  by (simp add: arctan)
    1.62  
    1.63  lemma arctan_bounded: "- (pi/2) < arctan y  & arctan y < pi/2"
    1.64    by (auto simp only: arctan)
    1.65  
    1.66  lemma arctan_lbound: "- (pi/2) < arctan y"
    1.67 -  by auto
    1.68 +  by (simp add: arctan)
    1.69  
    1.70  lemma arctan_ubound: "arctan y < pi/2"
    1.71    by (auto simp only: arctan)
    1.72 @@ -4112,7 +4142,7 @@
    1.73  lemma arctan_minus: "arctan (- x) = - arctan x"
    1.74    apply (rule arctan_unique)
    1.75    apply (simp only: neg_less_iff_less arctan_ubound)
    1.76 -  apply (metis minus_less_iff arctan_lbound, simp)
    1.77 +  apply (metis minus_less_iff arctan_lbound, simp add: arctan)
    1.78    done
    1.79  
    1.80  lemma cos_arctan_not_zero [simp]: "cos (arctan x) \<noteq> 0"
    1.81 @@ -4128,7 +4158,7 @@
    1.82    have "(cos (arctan x))\<^sup>2 * (1 + (tan (arctan x))\<^sup>2) = 1"
    1.83      unfolding tan_def by (simp add: distrib_left power_divide)
    1.84    thus "(cos (arctan x))\<^sup>2 = (1 / sqrt (1 + x\<^sup>2))\<^sup>2"
    1.85 -    using `0 < 1 + x\<^sup>2` by (simp add: power_divide eq_divide_eq)
    1.86 +    using `0 < 1 + x\<^sup>2` by (simp add: arctan power_divide eq_divide_eq)
    1.87  qed
    1.88  
    1.89  lemma sin_arctan: "sin (arctan x) = x / sqrt (1 + x\<^sup>2)"
    1.90 @@ -4221,7 +4251,7 @@
    1.91  lemma isCont_arctan: "isCont arctan x"
    1.92    apply (rule arctan_lbound [of x, THEN dense, THEN exE], clarify)
    1.93    apply (rule arctan_ubound [of x, THEN dense, THEN exE], clarify)
    1.94 -  apply (subgoal_tac "isCont arctan (tan (arctan x))", simp)
    1.95 +  apply (subgoal_tac "isCont arctan (tan (arctan x))", simp add: arctan)
    1.96    apply (erule (1) isCont_inverse_function2 [where f=tan])
    1.97    apply (metis arctan_tan order_le_less_trans order_less_le_trans)
    1.98    apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans less_le)
    1.99 @@ -4262,10 +4292,9 @@
   1.100    apply (rule DERIV_inverse_function [where f=tan and a="x - 1" and b="x + 1"])
   1.101    apply (rule DERIV_cong [OF DERIV_tan])
   1.102    apply (rule cos_arctan_not_zero)
   1.103 -  apply (simp add: power_inverse tan_sec [symmetric])
   1.104 +  apply (simp add: arctan power_inverse tan_sec [symmetric])
   1.105    apply (subgoal_tac "0 < 1 + x\<^sup>2", simp)
   1.106 -  apply (simp add: add_pos_nonneg)
   1.107 -  apply (simp, simp, simp, rule isCont_arctan)
   1.108 +  apply (simp_all add: add_pos_nonneg arctan isCont_arctan)
   1.109    done
   1.110  
   1.111  declare
   1.112 @@ -4275,12 +4304,12 @@
   1.113  
   1.114  lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- pi/2))"
   1.115    by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
   1.116 -     (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
   1.117 +     (auto simp: arctan le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
   1.118             intro!: tan_monotone exI[of _ "pi/2"])
   1.119  
   1.120  lemma filterlim_tan_at_left: "filterlim tan at_top (at_left (pi/2))"
   1.121    by (rule filterlim_at_top_at_left[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
   1.122 -     (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
   1.123 +     (auto simp: arctan le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
   1.124             intro!: tan_monotone exI[of _ "pi/2"])
   1.125  
   1.126  lemma tendsto_arctan_at_top: "(arctan ---> (pi/2)) at_top"
   1.127 @@ -4312,6 +4341,12 @@
   1.128  
   1.129  subsection{* Prove Totality of the Trigonometric Functions *}
   1.130  
   1.131 +lemma cos_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> cos (arccos y) = y"
   1.132 +  by (simp add: abs_le_iff)
   1.133 +
   1.134 +lemma sin_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> sin (arccos y) = sqrt (1 - y\<^sup>2)"
   1.135 +  by (simp add: sin_arccos abs_le_iff)
   1.136 +
   1.137  lemma sin_mono_less_eq: "\<lbrakk>-(pi/2) \<le> x; x \<le> pi/2; -(pi/2) \<le> y; y \<le> pi/2\<rbrakk>
   1.138           \<Longrightarrow> (sin(x) < sin(y) \<longleftrightarrow> x < y)"
   1.139  by (metis not_less_iff_gr_or_eq sin_monotone_2pi)
   1.140 @@ -4320,12 +4355,12 @@
   1.141           \<Longrightarrow> (sin(x) \<le> sin(y) \<longleftrightarrow> x \<le> y)"
   1.142  by (meson leD le_less_linear sin_monotone_2pi sin_monotone_2pi_le)
   1.143  
   1.144 -lemma sin_inj_pi: "-(pi/2) \<le> x ==> x \<le> pi/2 ==>
   1.145 -         -(pi/2) \<le> y ==> y \<le> pi/2 ==> sin(x) = sin(y) \<Longrightarrow> x = y"
   1.146 +lemma sin_inj_pi: 
   1.147 +    "\<lbrakk>-(pi/2) \<le> x; x \<le> pi/2;-(pi/2) \<le> y; y \<le> pi/2; sin(x) = sin(y)\<rbrakk> \<Longrightarrow> x = y"
   1.148  by (metis arcsin_sin)
   1.149  
   1.150 -lemma cos_mono_lt_eq: "0 \<le> x ==> x \<le> pi ==> 0 \<le> y ==> y \<le> pi
   1.151 -         \<Longrightarrow> (cos(x) < cos(y) \<longleftrightarrow> y < x)"
   1.152 +lemma cos_mono_less_eq:
   1.153 +    "0 \<le> x ==> x \<le> pi ==> 0 \<le> y ==> y \<le> pi \<Longrightarrow> (cos(x) < cos(y) \<longleftrightarrow> y < x)"
   1.154  by (meson cos_monotone_0_pi cos_monotone_0_pi_le leD le_less_linear)
   1.155  
   1.156  lemma cos_mono_le_eq: "0 \<le> x ==> x \<le> pi ==> 0 \<le> y ==> y \<le> pi
   1.157 @@ -4407,6 +4442,40 @@
   1.158      done
   1.159  qed
   1.160  
   1.161 +lemma arcsin_less_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> arcsin x < arcsin y \<longleftrightarrow> x < y"
   1.162 +  apply (rule trans [OF sin_mono_less_eq [symmetric]])
   1.163 +  using arcsin_ubound arcsin_lbound
   1.164 +  apply (auto simp: )
   1.165 +  done
   1.166 +
   1.167 +lemma arcsin_le_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> arcsin x \<le> arcsin y \<longleftrightarrow> x \<le> y"
   1.168 +  using arcsin_less_mono not_le by blast
   1.169 +
   1.170 +lemma arcsin_less_arcsin: "-1 \<le> x \<Longrightarrow> x < y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arcsin x < arcsin y"
   1.171 +  using arcsin_less_mono by auto
   1.172 +
   1.173 +lemma arcsin_le_arcsin: "-1 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arcsin x \<le> arcsin y"
   1.174 +  using arcsin_le_mono by auto
   1.175 +
   1.176 +lemma arccos_less_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> (arccos x < arccos y \<longleftrightarrow> y < x)"
   1.177 +  apply (rule trans [OF cos_mono_less_eq [symmetric]])
   1.178 +  using arccos_ubound arccos_lbound
   1.179 +  apply (auto simp: )
   1.180 +  done
   1.181 +
   1.182 +lemma arccos_le_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> arccos x \<le> arccos y \<longleftrightarrow> y \<le> x"
   1.183 +  using arccos_less_mono [of y x] 
   1.184 +  by (simp add: not_le [symmetric])
   1.185 +
   1.186 +lemma arccos_less_arccos: "-1 \<le> x \<Longrightarrow> x < y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arccos y < arccos x"
   1.187 +  using arccos_less_mono by auto
   1.188 +
   1.189 +lemma arccos_le_arccos: "-1 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arccos y \<le> arccos x"
   1.190 +  using arccos_le_mono by auto
   1.191 +
   1.192 +lemma arccos_eq_iff: "abs x \<le> 1 & abs y \<le> 1 \<Longrightarrow> (arccos x = arccos y \<longleftrightarrow> x = y)"
   1.193 +  using cos_arccos_abs by fastforce
   1.194 +
   1.195  subsection {* Machins formula *}
   1.196  
   1.197  lemma arctan_one: "arctan 1 = pi / 4"
   1.198 @@ -4418,7 +4487,8 @@
   1.199  proof
   1.200    show "- (pi / 4) < arctan x \<and> arctan x < pi / 4 \<and> tan (arctan x) = x"
   1.201      unfolding arctan_one [symmetric] arctan_minus [symmetric]
   1.202 -    unfolding arctan_less_iff using assms by auto
   1.203 +    unfolding arctan_less_iff using assms  by (auto simp add: arctan)
   1.204 +
   1.205  qed
   1.206  
   1.207  lemma arctan_add:
   1.208 @@ -4436,7 +4506,7 @@
   1.209    from add_le_less_mono [OF this]
   1.210    show 2: "arctan x + arctan y < pi / 2" by simp
   1.211    show "tan (arctan x + arctan y) = (x + y) / (1 - x * y)"
   1.212 -    using cos_gt_zero_pi [OF 1 2] by (simp add: tan_add)
   1.213 +    using cos_gt_zero_pi [OF 1 2] by (simp add: arctan tan_add)
   1.214  qed
   1.215  
   1.216  theorem machin: "pi / 4 = 4 * arctan (1/5) - arctan (1 / 239)"
   1.217 @@ -4882,7 +4952,7 @@
   1.218    show "- (pi / 2) < sgn x * pi / 2 - arctan x"
   1.219      using arctan_bounded [of x] assms
   1.220      unfolding sgn_real_def
   1.221 -    apply (auto simp add: algebra_simps)
   1.222 +    apply (auto simp add: arctan algebra_simps)
   1.223      apply (drule zero_less_arctan_iff [THEN iffD2])
   1.224      apply arith
   1.225      done
   1.226 @@ -4911,12 +4981,6 @@
   1.227    apply (simp add: power_divide divide_le_eq not_sum_power2_lt_zero)
   1.228    done
   1.229  
   1.230 -lemma cos_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> cos (arccos y) = y"
   1.231 -  by (simp add: abs_le_iff)
   1.232 -
   1.233 -lemma sin_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> sin (arccos y) = sqrt (1 - y\<^sup>2)"
   1.234 -  by (simp add: sin_arccos abs_le_iff)
   1.235 -
   1.236  lemmas cos_arccos_lemma1 = cos_arccos_abs [OF cos_x_y_le_one]
   1.237  
   1.238  lemmas sin_arccos_lemma1 = sin_arccos_abs [OF cos_x_y_le_one]