src/HOL/Transcendental.thy
changeset 53015 a1119cf551e8
parent 52139 40fe6b80b481
child 53076 47c9aff07725
     1.1 --- a/src/HOL/Transcendental.thy	Tue Aug 13 14:20:22 2013 +0200
     1.2 +++ b/src/HOL/Transcendental.thy	Tue Aug 13 16:25:47 2013 +0200
     1.3 @@ -1266,13 +1266,13 @@
     1.4        by (rule le_imp_inverse_le) simp
     1.5      hence "inverse (fact (n + 2)) \<le> 1/2 * (1/2)^n"
     1.6        by (simp add: inverse_mult_distrib power_inverse)
     1.7 -    hence "inverse (fact (n + 2)) * (x^n * x\<twosuperior>) \<le> 1/2 * (1/2)^n * (1 * x\<twosuperior>)"
     1.8 +    hence "inverse (fact (n + 2)) * (x^n * x\<^sup>2) \<le> 1/2 * (1/2)^n * (1 * x\<^sup>2)"
     1.9        by (rule mult_mono)
    1.10          (rule mult_mono, simp_all add: power_le_one a b mult_nonneg_nonneg)
    1.11 -    hence "inverse (fact (n + 2)) * x ^ (n + 2) \<le> (x\<twosuperior>/2) * ((1/2)^n)"
    1.12 +    hence "inverse (fact (n + 2)) * x ^ (n + 2) \<le> (x\<^sup>2/2) * ((1/2)^n)"
    1.13        unfolding power_add by (simp add: mult_ac del: fact_Suc) }
    1.14    note aux1 = this
    1.15 -  have "(\<lambda>n. x\<twosuperior> / 2 * (1 / 2) ^ n) sums (x\<twosuperior> / 2 * (1 / (1 - 1 / 2)))"
    1.16 +  have "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))"
    1.17      by (intro sums_mult geometric_sums, simp)
    1.18    hence aux2: "(\<lambda>n. (x::real) ^ 2 / 2 * (1 / 2) ^ n) sums x^2"
    1.19      by simp
    1.20 @@ -1299,7 +1299,7 @@
    1.21    also have "... <= 1"
    1.22      by (auto simp add: a)
    1.23    finally have "(1 - x) * (1 + x + x ^ 2) <= 1" .
    1.24 -  moreover have c: "0 < 1 + x + x\<twosuperior>"
    1.25 +  moreover have c: "0 < 1 + x + x\<^sup>2"
    1.26      by (simp add: add_pos_nonneg a)
    1.27    ultimately have "1 - x <= 1 / (1 + x + x^2)"
    1.28      by (elim mult_imp_le_div_pos)
    1.29 @@ -2134,25 +2134,25 @@
    1.30  lemma cos_zero [simp]: "cos 0 = 1"
    1.31    unfolding cos_def cos_coeff_def by (simp add: powser_zero)
    1.32  
    1.33 -lemma sin_cos_squared_add [simp]: "(sin x)\<twosuperior> + (cos x)\<twosuperior> = 1"
    1.34 +lemma sin_cos_squared_add [simp]: "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
    1.35  proof -
    1.36 -  have "\<forall>x. DERIV (\<lambda>x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
    1.37 +  have "\<forall>x. DERIV (\<lambda>x. (sin x)\<^sup>2 + (cos x)\<^sup>2) x :> 0"
    1.38      by (auto intro!: DERIV_intros)
    1.39 -  hence "(sin x)\<twosuperior> + (cos x)\<twosuperior> = (sin 0)\<twosuperior> + (cos 0)\<twosuperior>"
    1.40 +  hence "(sin x)\<^sup>2 + (cos x)\<^sup>2 = (sin 0)\<^sup>2 + (cos 0)\<^sup>2"
    1.41      by (rule DERIV_isconst_all)
    1.42 -  thus "(sin x)\<twosuperior> + (cos x)\<twosuperior> = 1" by simp
    1.43 +  thus "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1" by simp
    1.44  qed
    1.45  
    1.46 -lemma sin_cos_squared_add2 [simp]: "(cos x)\<twosuperior> + (sin x)\<twosuperior> = 1"
    1.47 +lemma sin_cos_squared_add2 [simp]: "(cos x)\<^sup>2 + (sin x)\<^sup>2 = 1"
    1.48    by (subst add_commute, rule sin_cos_squared_add)
    1.49  
    1.50  lemma sin_cos_squared_add3 [simp]: "cos x * cos x + sin x * sin x = 1"
    1.51    using sin_cos_squared_add2 [unfolded power2_eq_square] .
    1.52  
    1.53 -lemma sin_squared_eq: "(sin x)\<twosuperior> = 1 - (cos x)\<twosuperior>"
    1.54 +lemma sin_squared_eq: "(sin x)\<^sup>2 = 1 - (cos x)\<^sup>2"
    1.55    unfolding eq_diff_eq by (rule sin_cos_squared_add)
    1.56  
    1.57 -lemma cos_squared_eq: "(cos x)\<twosuperior> = 1 - (sin x)\<twosuperior>"
    1.58 +lemma cos_squared_eq: "(cos x)\<^sup>2 = 1 - (sin x)\<^sup>2"
    1.59    unfolding eq_diff_eq by (rule sin_cos_squared_add2)
    1.60  
    1.61  lemma abs_sin_le_one [simp]: "\<bar>sin x\<bar> \<le> 1"
    1.62 @@ -2208,7 +2208,7 @@
    1.63    using sin_cos_add_lemma unfolding realpow_two_sum_zero_iff by simp
    1.64  
    1.65  lemma sin_cos_minus_lemma:
    1.66 -  "(sin(-x) + sin(x))\<twosuperior> + (cos(-x) - cos(x))\<twosuperior> = 0" (is "?f x = 0")
    1.67 +  "(sin(-x) + sin(x))\<^sup>2 + (cos(-x) - cos(x))\<^sup>2 = 0" (is "?f x = 0")
    1.68  proof -
    1.69    have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
    1.70      by (auto intro!: DERIV_intros simp add: algebra_simps)
    1.71 @@ -2238,7 +2238,7 @@
    1.72  lemma sin_double [simp]: "sin(2 * x) = 2* sin x * cos x"
    1.73    using sin_add [where x=x and y=x] by simp
    1.74  
    1.75 -lemma cos_double: "cos(2* x) = ((cos x)\<twosuperior>) - ((sin x)\<twosuperior>)"
    1.76 +lemma cos_double: "cos(2* x) = ((cos x)\<^sup>2) - ((sin x)\<^sup>2)"
    1.77    using cos_add [where x=x and y=x]
    1.78    by (simp add: power2_eq_square)
    1.79  
    1.80 @@ -2732,7 +2732,7 @@
    1.81    unfolding tan_def sin_double cos_double sin_squared_eq
    1.82    by (simp add: power2_eq_square)
    1.83  
    1.84 -lemma DERIV_tan [simp]: "cos x \<noteq> 0 \<Longrightarrow> DERIV tan x :> inverse ((cos x)\<twosuperior>)"
    1.85 +lemma DERIV_tan [simp]: "cos x \<noteq> 0 \<Longrightarrow> DERIV tan x :> inverse ((cos x)\<^sup>2)"
    1.86    unfolding tan_def
    1.87    by (auto intro!: DERIV_intros, simp add: divide_inverse power2_eq_square)
    1.88  
    1.89 @@ -2827,10 +2827,10 @@
    1.90      thus "DERIV tan x' :> inverse (cos x'^2)" by (rule DERIV_tan)
    1.91    qed
    1.92    from MVT2[OF `y < x` this]
    1.93 -  obtain z where "y < z" and "z < x" and tan_diff: "tan x - tan y = (x - y) * inverse ((cos z)\<twosuperior>)" by auto
    1.94 +  obtain z where "y < z" and "z < x" and tan_diff: "tan x - tan y = (x - y) * inverse ((cos z)\<^sup>2)" by auto
    1.95    hence "- (pi / 2) < z" and "z < pi / 2" using assms by auto
    1.96    hence "0 < cos z" using cos_gt_zero_pi by auto
    1.97 -  hence inv_pos: "0 < inverse ((cos z)\<twosuperior>)" by auto
    1.98 +  hence inv_pos: "0 < inverse ((cos z)\<^sup>2)" by auto
    1.99    have "0 < x - y" using `y < x` by auto
   1.100    from mult_pos_pos [OF this inv_pos]
   1.101    have "0 < tan x - tan y" unfolding tan_diff by auto
   1.102 @@ -2978,27 +2978,27 @@
   1.103  apply (auto intro!: the1_equality cos_total)
   1.104  done
   1.105  
   1.106 -lemma cos_arcsin: "\<lbrakk>-1 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> cos (arcsin x) = sqrt (1 - x\<twosuperior>)"
   1.107 -apply (subgoal_tac "x\<twosuperior> \<le> 1")
   1.108 +lemma cos_arcsin: "\<lbrakk>-1 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> cos (arcsin x) = sqrt (1 - x\<^sup>2)"
   1.109 +apply (subgoal_tac "x\<^sup>2 \<le> 1")
   1.110  apply (rule power2_eq_imp_eq)
   1.111  apply (simp add: cos_squared_eq)
   1.112  apply (rule cos_ge_zero)
   1.113  apply (erule (1) arcsin_lbound)
   1.114  apply (erule (1) arcsin_ubound)
   1.115  apply simp
   1.116 -apply (subgoal_tac "\<bar>x\<bar>\<twosuperior> \<le> 1\<twosuperior>", simp)
   1.117 +apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 \<le> 1\<^sup>2", simp)
   1.118  apply (rule power_mono, simp, simp)
   1.119  done
   1.120  
   1.121 -lemma sin_arccos: "\<lbrakk>-1 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> sin (arccos x) = sqrt (1 - x\<twosuperior>)"
   1.122 -apply (subgoal_tac "x\<twosuperior> \<le> 1")
   1.123 +lemma sin_arccos: "\<lbrakk>-1 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> sin (arccos x) = sqrt (1 - x\<^sup>2)"
   1.124 +apply (subgoal_tac "x\<^sup>2 \<le> 1")
   1.125  apply (rule power2_eq_imp_eq)
   1.126  apply (simp add: sin_squared_eq)
   1.127  apply (rule sin_ge_zero)
   1.128  apply (erule (1) arccos_lbound)
   1.129  apply (erule (1) arccos_ubound)
   1.130  apply simp
   1.131 -apply (subgoal_tac "\<bar>x\<bar>\<twosuperior> \<le> 1\<twosuperior>", simp)
   1.132 +apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 \<le> 1\<^sup>2", simp)
   1.133  apply (rule power_mono, simp, simp)
   1.134  done
   1.135  
   1.136 @@ -3041,26 +3041,26 @@
   1.137    by (intro less_imp_neq [symmetric] cos_gt_zero_pi
   1.138      arctan_lbound arctan_ubound)
   1.139  
   1.140 -lemma cos_arctan: "cos (arctan x) = 1 / sqrt (1 + x\<twosuperior>)"
   1.141 +lemma cos_arctan: "cos (arctan x) = 1 / sqrt (1 + x\<^sup>2)"
   1.142  proof (rule power2_eq_imp_eq)
   1.143 -  have "0 < 1 + x\<twosuperior>" by (simp add: add_pos_nonneg)
   1.144 -  show "0 \<le> 1 / sqrt (1 + x\<twosuperior>)" by simp
   1.145 +  have "0 < 1 + x\<^sup>2" by (simp add: add_pos_nonneg)
   1.146 +  show "0 \<le> 1 / sqrt (1 + x\<^sup>2)" by simp
   1.147    show "0 \<le> cos (arctan x)"
   1.148      by (intro less_imp_le cos_gt_zero_pi arctan_lbound arctan_ubound)
   1.149 -  have "(cos (arctan x))\<twosuperior> * (1 + (tan (arctan x))\<twosuperior>) = 1"
   1.150 +  have "(cos (arctan x))\<^sup>2 * (1 + (tan (arctan x))\<^sup>2) = 1"
   1.151      unfolding tan_def by (simp add: distrib_left power_divide)
   1.152 -  thus "(cos (arctan x))\<twosuperior> = (1 / sqrt (1 + x\<twosuperior>))\<twosuperior>"
   1.153 -    using `0 < 1 + x\<twosuperior>` by (simp add: power_divide eq_divide_eq)
   1.154 +  thus "(cos (arctan x))\<^sup>2 = (1 / sqrt (1 + x\<^sup>2))\<^sup>2"
   1.155 +    using `0 < 1 + x\<^sup>2` by (simp add: power_divide eq_divide_eq)
   1.156  qed
   1.157  
   1.158 -lemma sin_arctan: "sin (arctan x) = x / sqrt (1 + x\<twosuperior>)"
   1.159 +lemma sin_arctan: "sin (arctan x) = x / sqrt (1 + x\<^sup>2)"
   1.160    using add_pos_nonneg [OF zero_less_one zero_le_power2 [of x]]
   1.161    using tan_arctan [of x] unfolding tan_def cos_arctan
   1.162    by (simp add: eq_divide_eq)
   1.163  
   1.164  lemma tan_sec: "cos x \<noteq> 0 ==> 1 + tan(x) ^ 2 = inverse(cos x) ^ 2"
   1.165  apply (rule power_inverse [THEN subst])
   1.166 -apply (rule_tac c1 = "(cos x)\<twosuperior>" in real_mult_right_cancel [THEN iffD1])
   1.167 +apply (rule_tac c1 = "(cos x)\<^sup>2" in real_mult_right_cancel [THEN iffD1])
   1.168  apply (auto dest: field_power_not_zero
   1.169          simp add: power_mult_distrib distrib_right power_divide tan_def
   1.170                    mult_assoc power_inverse [symmetric])
   1.171 @@ -3151,11 +3151,11 @@
   1.172    unfolding continuous_on_def by (auto intro: tendsto_arctan)
   1.173    
   1.174  lemma DERIV_arcsin:
   1.175 -  "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arcsin x :> inverse (sqrt (1 - x\<twosuperior>))"
   1.176 +  "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arcsin x :> inverse (sqrt (1 - x\<^sup>2))"
   1.177  apply (rule DERIV_inverse_function [where f=sin and a="-1" and b="1"])
   1.178  apply (rule DERIV_cong [OF DERIV_sin])
   1.179  apply (simp add: cos_arcsin)
   1.180 -apply (subgoal_tac "\<bar>x\<bar>\<twosuperior> < 1\<twosuperior>", simp)
   1.181 +apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 < 1\<^sup>2", simp)
   1.182  apply (rule power_strict_mono, simp, simp, simp)
   1.183  apply assumption
   1.184  apply assumption
   1.185 @@ -3164,11 +3164,11 @@
   1.186  done
   1.187  
   1.188  lemma DERIV_arccos:
   1.189 -  "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arccos x :> inverse (- sqrt (1 - x\<twosuperior>))"
   1.190 +  "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arccos x :> inverse (- sqrt (1 - x\<^sup>2))"
   1.191  apply (rule DERIV_inverse_function [where f=cos and a="-1" and b="1"])
   1.192  apply (rule DERIV_cong [OF DERIV_cos])
   1.193  apply (simp add: sin_arccos)
   1.194 -apply (subgoal_tac "\<bar>x\<bar>\<twosuperior> < 1\<twosuperior>", simp)
   1.195 +apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 < 1\<^sup>2", simp)
   1.196  apply (rule power_strict_mono, simp, simp, simp)
   1.197  apply assumption
   1.198  apply assumption
   1.199 @@ -3176,12 +3176,12 @@
   1.200  apply (erule (1) isCont_arccos)
   1.201  done
   1.202  
   1.203 -lemma DERIV_arctan: "DERIV arctan x :> inverse (1 + x\<twosuperior>)"
   1.204 +lemma DERIV_arctan: "DERIV arctan x :> inverse (1 + x\<^sup>2)"
   1.205  apply (rule DERIV_inverse_function [where f=tan and a="x - 1" and b="x + 1"])
   1.206  apply (rule DERIV_cong [OF DERIV_tan])
   1.207  apply (rule cos_arctan_not_zero)
   1.208  apply (simp add: power_inverse tan_sec [symmetric])
   1.209 -apply (subgoal_tac "0 < 1 + x\<twosuperior>", simp)
   1.210 +apply (subgoal_tac "0 < 1 + x\<^sup>2", simp)
   1.211  apply (simp add: add_pos_nonneg)
   1.212  apply (simp, simp, simp, rule isCont_arctan)
   1.213  done
   1.214 @@ -3233,11 +3233,11 @@
   1.215      by (simp add: cos_ge_zero)
   1.216    have "0 = cos (pi / 4 + pi / 4)"
   1.217      by simp
   1.218 -  also have "cos (pi / 4 + pi / 4) = ?c\<twosuperior> - ?s\<twosuperior>"
   1.219 +  also have "cos (pi / 4 + pi / 4) = ?c\<^sup>2 - ?s\<^sup>2"
   1.220      by (simp only: cos_add power2_eq_square)
   1.221 -  also have "\<dots> = 2 * ?c\<twosuperior> - 1"
   1.222 +  also have "\<dots> = 2 * ?c\<^sup>2 - 1"
   1.223      by (simp add: sin_squared_eq)
   1.224 -  finally have "?c\<twosuperior> = (sqrt 2 / 2)\<twosuperior>"
   1.225 +  finally have "?c\<^sup>2 = (sqrt 2 / 2)\<^sup>2"
   1.226      by (simp add: power_divide)
   1.227    thus ?thesis
   1.228      using nonneg by (rule power2_eq_imp_eq) simp
   1.229 @@ -3252,9 +3252,9 @@
   1.230      by simp
   1.231    also have "\<dots> = (?c * ?c - ?s * ?s) * ?c - (?s * ?c + ?c * ?s) * ?s"
   1.232      by (simp only: cos_add sin_add)
   1.233 -  also have "\<dots> = ?c * (?c\<twosuperior> - 3 * ?s\<twosuperior>)"
   1.234 +  also have "\<dots> = ?c * (?c\<^sup>2 - 3 * ?s\<^sup>2)"
   1.235      by (simp add: algebra_simps power2_eq_square)
   1.236 -  finally have "?c\<twosuperior> = (sqrt 3 / 2)\<twosuperior>"
   1.237 +  finally have "?c\<^sup>2 = (sqrt 3 / 2)\<^sup>2"
   1.238      using pos_c by (simp add: sin_squared_eq power_divide)
   1.239    thus ?thesis
   1.240      using pos_c [THEN order_less_imp_le]
   1.241 @@ -3695,7 +3695,7 @@
   1.242  
   1.243  subsection {* Existence of Polar Coordinates *}
   1.244  
   1.245 -lemma cos_x_y_le_one: "\<bar>x / sqrt (x\<twosuperior> + y\<twosuperior>)\<bar> \<le> 1"
   1.246 +lemma cos_x_y_le_one: "\<bar>x / sqrt (x\<^sup>2 + y\<^sup>2)\<bar> \<le> 1"
   1.247  apply (rule power2_le_imp_le [OF _ zero_le_one])
   1.248  apply (simp add: power_divide divide_le_eq not_sum_power2_lt_zero)
   1.249  done
   1.250 @@ -3703,7 +3703,7 @@
   1.251  lemma cos_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> cos (arccos y) = y"
   1.252  by (simp add: abs_le_iff)
   1.253  
   1.254 -lemma sin_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> sin (arccos y) = sqrt (1 - y\<twosuperior>)"
   1.255 +lemma sin_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> sin (arccos y) = sqrt (1 - y\<^sup>2)"
   1.256  by (simp add: sin_arccos abs_le_iff)
   1.257  
   1.258  lemmas cos_arccos_lemma1 = cos_arccos_abs [OF cos_x_y_le_one]
   1.259 @@ -3712,8 +3712,8 @@
   1.260  
   1.261  lemma polar_ex1:
   1.262       "0 < y ==> \<exists>r a. x = r * cos a & y = r * sin a"
   1.263 -apply (rule_tac x = "sqrt (x\<twosuperior> + y\<twosuperior>)" in exI)
   1.264 -apply (rule_tac x = "arccos (x / sqrt (x\<twosuperior> + y\<twosuperior>))" in exI)
   1.265 +apply (rule_tac x = "sqrt (x\<^sup>2 + y\<^sup>2)" in exI)
   1.266 +apply (rule_tac x = "arccos (x / sqrt (x\<^sup>2 + y\<^sup>2))" in exI)
   1.267  apply (simp add: cos_arccos_lemma1)
   1.268  apply (simp add: sin_arccos_lemma1)
   1.269  apply (simp add: power_divide)