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.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.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.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.79
1.80 @@ -2732,7 +2732,7 @@
1.81    unfolding tan_def sin_double cos_double sin_squared_eq
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.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.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.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.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.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.212  apply (simp, simp, simp, rule isCont_arctan)
1.213  done
1.214 @@ -3233,11 +3233,11 @@
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.224 -  finally have "?c\<twosuperior> = (sqrt 2 / 2)\<twosuperior>"
1.225 +  finally have "?c\<^sup>2 = (sqrt 2 / 2)\<^sup>2"
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.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.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)