more symbols;
authorwenzelm
Sun Aug 18 18:49:45 2013 +0200 (2013-08-18)
changeset 5307647c9aff07725
parent 53075 98fc47533342
child 53077 a1b3784f8129
more symbols;
src/HOL/NthRoot.thy
src/HOL/Power.thy
src/HOL/Real.thy
src/HOL/Semiring_Normalization.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/NthRoot.thy	Sun Aug 18 17:00:10 2013 +0200
     1.2 +++ b/src/HOL/NthRoot.thy	Sun Aug 18 18:49:45 2013 +0200
     1.3 @@ -464,7 +464,7 @@
     1.4  apply (rule real_sqrt_abs)
     1.5  done
     1.6  
     1.7 -lemma real_inv_sqrt_pow2: "0 < x ==> inverse (sqrt(x)) ^ 2 = inverse x"
     1.8 +lemma real_inv_sqrt_pow2: "0 < x ==> (inverse (sqrt x))\<^sup>2 = inverse x"
     1.9  by (simp add: power_inverse [symmetric])
    1.10  
    1.11  lemma real_sqrt_eq_zero_cancel: "[| 0 \<le> x; sqrt(x) = 0|] ==> x = 0"
    1.12 @@ -516,7 +516,7 @@
    1.13    by (simp add: zero_le_mult_iff)
    1.14  
    1.15  lemma real_sqrt_sum_squares_mult_squared_eq [simp]:
    1.16 -     "sqrt ((x\<^sup>2 + y\<^sup>2) * (xa\<^sup>2 + ya\<^sup>2)) ^ 2 = (x\<^sup>2 + y\<^sup>2) * (xa\<^sup>2 + ya\<^sup>2)"
    1.17 +     "(sqrt ((x\<^sup>2 + y\<^sup>2) * (xa\<^sup>2 + ya\<^sup>2)))\<^sup>2 = (x\<^sup>2 + y\<^sup>2) * (xa\<^sup>2 + ya\<^sup>2)"
    1.18    by (simp add: zero_le_mult_iff)
    1.19  
    1.20  lemma real_sqrt_sum_squares_eq_cancel: "sqrt (x\<^sup>2 + y\<^sup>2) = x \<Longrightarrow> y = 0"
     2.1 --- a/src/HOL/Power.thy	Sun Aug 18 17:00:10 2013 +0200
     2.2 +++ b/src/HOL/Power.thy	Sun Aug 18 18:49:45 2013 +0200
     2.3 @@ -74,11 +74,11 @@
     2.4    by (simp add: numeral_3_eq_3 mult_assoc)
     2.5  
     2.6  lemma power_even_eq:
     2.7 -  "a ^ (2*n) = (a ^ n) ^ 2"
     2.8 +  "a ^ (2 * n) = (a ^ n)\<^sup>2"
     2.9    by (subst mult_commute) (simp add: power_mult)
    2.10  
    2.11  lemma power_odd_eq:
    2.12 -  "a ^ Suc (2*n) = a * (a ^ n) ^ 2"
    2.13 +  "a ^ Suc (2*n) = a * (a ^ n)\<^sup>2"
    2.14    by (simp add: power_even_eq)
    2.15  
    2.16  lemma power_numeral_even:
     3.1 --- a/src/HOL/Real.thy	Sun Aug 18 17:00:10 2013 +0200
     3.2 +++ b/src/HOL/Real.thy	Sun Aug 18 18:49:45 2013 +0200
     3.3 @@ -1559,13 +1559,13 @@
     3.4  
     3.5  text {* FIXME: declare this [simp] for all types, or not at all *}
     3.6  lemma realpow_two_sum_zero_iff [simp]:
     3.7 -     "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
     3.8 +     "(x\<^sup>2 + y\<^sup>2 = (0::real)) = (x = 0 & y = 0)"
     3.9  by (rule sum_power2_eq_zero_iff)
    3.10  
    3.11  lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))"
    3.12  by (rule_tac y = 0 in order_trans, auto)
    3.13  
    3.14 -lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2"
    3.15 +lemma realpow_square_minus_le [simp]: "- u\<^sup>2 \<le> (x::real)\<^sup>2"
    3.16  by (auto simp add: power2_eq_square)
    3.17  
    3.18  
     4.1 --- a/src/HOL/Semiring_Normalization.thy	Sun Aug 18 17:00:10 2013 +0200
     4.2 +++ b/src/HOL/Semiring_Normalization.thy	Sun Aug 18 18:49:45 2013 +0200
     4.3 @@ -107,7 +107,7 @@
     4.4    "(x ^ p) * (x ^ q) = x ^ (p + q)"
     4.5    "x * (x ^ q) = x ^ (Suc q)"
     4.6    "(x ^ q) * x = x ^ (Suc q)"
     4.7 -  "x * x = x ^ 2"
     4.8 +  "x * x = x\<^sup>2"
     4.9    "(x * y) ^ q = (x ^ q) * (y ^ q)"
    4.10    "(x ^ p) ^ q = x ^ (p * q)"
    4.11    "x ^ 0 = 1"
     5.1 --- a/src/HOL/Transcendental.thy	Sun Aug 18 17:00:10 2013 +0200
     5.2 +++ b/src/HOL/Transcendental.thy	Sun Aug 18 18:49:45 2013 +0200
     5.3 @@ -1251,7 +1251,7 @@
     5.4    finally show ?thesis .
     5.5  qed
     5.6  
     5.7 -lemma exp_bound: "0 <= (x::real) ==> x <= 1 ==> exp x <= 1 + x + x^2"
     5.8 +lemma exp_bound: "0 <= (x::real) ==> x <= 1 ==> exp x <= 1 + x + x\<^sup>2"
     5.9  proof -
    5.10    assume a: "0 <= x"
    5.11    assume b: "x <= 1"
    5.12 @@ -1274,17 +1274,17 @@
    5.13    note aux1 = this
    5.14    have "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))"
    5.15      by (intro sums_mult geometric_sums, simp)
    5.16 -  hence aux2: "(\<lambda>n. (x::real) ^ 2 / 2 * (1 / 2) ^ n) sums x^2"
    5.17 +  hence aux2: "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums x\<^sup>2"
    5.18      by simp
    5.19 -  have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <= x^2"
    5.20 +  have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <= x\<^sup>2"
    5.21    proof -
    5.22      have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <=
    5.23 -        suminf (%n. (x^2/2) * ((1/2)^n))"
    5.24 +        suminf (%n. (x\<^sup>2/2) * ((1/2)^n))"
    5.25        apply (rule summable_le)
    5.26        apply (rule allI, rule aux1)
    5.27        apply (rule summable_exp [THEN summable_ignore_initial_segment])
    5.28        by (rule sums_summable, rule aux2)
    5.29 -    also have "... = x^2"
    5.30 +    also have "... = x\<^sup>2"
    5.31        by (rule sums_unique [THEN sym], rule aux2)
    5.32      finally show ?thesis .
    5.33    qed
    5.34 @@ -1294,14 +1294,14 @@
    5.35  lemma ln_one_minus_pos_upper_bound: "0 <= x ==> x < 1 ==> ln (1 - x) <= - x"
    5.36  proof -
    5.37    assume a: "0 <= (x::real)" and b: "x < 1"
    5.38 -  have "(1 - x) * (1 + x + x^2) = (1 - x^3)"
    5.39 +  have "(1 - x) * (1 + x + x\<^sup>2) = (1 - x^3)"
    5.40      by (simp add: algebra_simps power2_eq_square power3_eq_cube)
    5.41    also have "... <= 1"
    5.42      by (auto simp add: a)
    5.43 -  finally have "(1 - x) * (1 + x + x ^ 2) <= 1" .
    5.44 +  finally have "(1 - x) * (1 + x + x\<^sup>2) <= 1" .
    5.45    moreover have c: "0 < 1 + x + x\<^sup>2"
    5.46      by (simp add: add_pos_nonneg a)
    5.47 -  ultimately have "1 - x <= 1 / (1 + x + x^2)"
    5.48 +  ultimately have "1 - x <= 1 / (1 + x + x\<^sup>2)"
    5.49      by (elim mult_imp_le_div_pos)
    5.50    also have "... <= 1 / exp x"
    5.51      apply (rule divide_left_mono)
    5.52 @@ -1343,18 +1343,18 @@
    5.53    apply auto
    5.54  done
    5.55  
    5.56 -lemma ln_one_plus_pos_lower_bound: "0 <= x ==> x <= 1 ==> x - x^2 <= ln (1 + x)"
    5.57 +lemma ln_one_plus_pos_lower_bound: "0 <= x ==> x <= 1 ==> x - x\<^sup>2 <= ln (1 + x)"
    5.58  proof -
    5.59    assume a: "0 <= x" and b: "x <= 1"
    5.60 -  have "exp (x - x^2) = exp x / exp (x^2)"
    5.61 +  have "exp (x - x\<^sup>2) = exp x / exp (x\<^sup>2)"
    5.62      by (rule exp_diff)
    5.63 -  also have "... <= (1 + x + x^2) / exp (x ^2)"
    5.64 +  also have "... <= (1 + x + x\<^sup>2) / exp (x \<^sup>2)"
    5.65      apply (rule divide_right_mono) 
    5.66      apply (rule exp_bound)
    5.67      apply (rule a, rule b)
    5.68      apply simp
    5.69      done
    5.70 -  also have "... <= (1 + x + x^2) / (1 + x^2)"
    5.71 +  also have "... <= (1 + x + x\<^sup>2) / (1 + x\<^sup>2)"
    5.72      apply (rule divide_left_mono)
    5.73      apply (simp add: exp_ge_add_one_self_aux)
    5.74      apply (simp add: a)
    5.75 @@ -1362,14 +1362,14 @@
    5.76      done
    5.77    also from a have "... <= 1 + x"
    5.78      by (simp add: field_simps add_strict_increasing zero_le_mult_iff)
    5.79 -  finally have "exp (x - x^2) <= 1 + x" .
    5.80 +  finally have "exp (x - x\<^sup>2) <= 1 + x" .
    5.81    also have "... = exp (ln (1 + x))"
    5.82    proof -
    5.83      from a have "0 < 1 + x" by auto
    5.84      thus ?thesis
    5.85        by (auto simp only: exp_ln_iff [THEN sym])
    5.86    qed
    5.87 -  finally have "exp (x - x ^ 2) <= exp (ln (1 + x))" .
    5.88 +  finally have "exp (x - x\<^sup>2) <= exp (ln (1 + x))" .
    5.89    thus ?thesis by (auto simp only: exp_le_cancel_iff)
    5.90  qed
    5.91  
    5.92 @@ -1392,7 +1392,7 @@
    5.93  qed
    5.94  
    5.95  lemma ln_one_minus_pos_lower_bound: "0 <= x ==> x <= (1 / 2) ==> 
    5.96 -    - x - 2 * x^2 <= ln (1 - x)"
    5.97 +    - x - 2 * x\<^sup>2 <= ln (1 - x)"
    5.98  proof -
    5.99    assume a: "0 <= x" and b: "x <= (1 / 2)"
   5.100    from b have c: "x < 1"
   5.101 @@ -1412,10 +1412,10 @@
   5.102      by auto
   5.103    finally have d: "- x / (1 - x) <= ln (1 - x)" .
   5.104    have "0 < 1 - x" using a b by simp
   5.105 -  hence e: "-x - 2 * x^2 <= - x / (1 - x)"
   5.106 +  hence e: "-x - 2 * x\<^sup>2 <= - x / (1 - x)"
   5.107      using mult_right_le_one_le[of "x*x" "2*x"] a b
   5.108      by (simp add:field_simps power2_eq_square)
   5.109 -  from e d show "- x - 2 * x^2 <= ln (1 - x)"
   5.110 +  from e d show "- x - 2 * x\<^sup>2 <= ln (1 - x)"
   5.111      by (rule order_trans)
   5.112  qed
   5.113  
   5.114 @@ -1426,7 +1426,7 @@
   5.115  done
   5.116  
   5.117  lemma abs_ln_one_plus_x_minus_x_bound_nonneg:
   5.118 -    "0 <= x ==> x <= 1 ==> abs(ln (1 + x) - x) <= x^2"
   5.119 +    "0 <= x ==> x <= 1 ==> abs(ln (1 + x) - x) <= x\<^sup>2"
   5.120  proof -
   5.121    assume x: "0 <= x"
   5.122    assume x1: "x <= 1"
   5.123 @@ -1438,9 +1438,9 @@
   5.124      by (rule abs_of_nonpos)
   5.125    also have "... = x - ln (1 + x)" 
   5.126      by simp
   5.127 -  also have "... <= x^2"
   5.128 +  also have "... <= x\<^sup>2"
   5.129    proof -
   5.130 -    from x x1 have "x - x^2 <= ln (1 + x)"
   5.131 +    from x x1 have "x - x\<^sup>2 <= ln (1 + x)"
   5.132        by (intro ln_one_plus_pos_lower_bound)
   5.133      thus ?thesis
   5.134        by simp
   5.135 @@ -1449,7 +1449,7 @@
   5.136  qed
   5.137  
   5.138  lemma abs_ln_one_plus_x_minus_x_bound_nonpos:
   5.139 -    "-(1 / 2) <= x ==> x <= 0 ==> abs(ln (1 + x) - x) <= 2 * x^2"
   5.140 +    "-(1 / 2) <= x ==> x <= 0 ==> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
   5.141  proof -
   5.142    assume a: "-(1 / 2) <= x"
   5.143    assume b: "x <= 0"
   5.144 @@ -1459,8 +1459,8 @@
   5.145      apply (rule ln_add_one_self_le_self2)
   5.146      using a apply auto
   5.147      done
   5.148 -  also have "... <= 2 * x^2"
   5.149 -    apply (subgoal_tac "- (-x) - 2 * (-x)^2 <= ln (1 - (-x))")
   5.150 +  also have "... <= 2 * x\<^sup>2"
   5.151 +    apply (subgoal_tac "- (-x) - 2 * (-x)\<^sup>2 <= ln (1 - (-x))")
   5.152      apply (simp add: algebra_simps)
   5.153      apply (rule ln_one_minus_pos_lower_bound)
   5.154      using a b apply auto
   5.155 @@ -1469,7 +1469,7 @@
   5.156  qed
   5.157  
   5.158  lemma abs_ln_one_plus_x_minus_x_bound:
   5.159 -    "abs x <= 1 / 2 ==> abs(ln (1 + x) - x) <= 2 * x^2"
   5.160 +    "abs x <= 1 / 2 ==> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
   5.161    apply (case_tac "0 <= x")
   5.162    apply (rule order_trans)
   5.163    apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg)
   5.164 @@ -2190,8 +2190,8 @@
   5.165    by (auto intro!: DERIV_intros)
   5.166  
   5.167  lemma sin_cos_add_lemma:
   5.168 -     "(sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +
   5.169 -      (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2 = 0"
   5.170 +     "(sin (x + y) - (sin x * cos y + cos x * sin y))\<^sup>2 +
   5.171 +      (cos (x + y) - (cos x * cos y - sin x * sin y))\<^sup>2 = 0"
   5.172    (is "?f x = 0")
   5.173  proof -
   5.174    have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
   5.175 @@ -2715,7 +2715,7 @@
   5.176  
   5.177  lemma tan_double:
   5.178       "[| cos x \<noteq> 0; cos (2 * x) \<noteq> 0 |]
   5.179 -      ==> tan (2 * x) = (2 * tan x)/(1 - (tan(x) ^ 2))"
   5.180 +      ==> tan (2 * x) = (2 * tan x) / (1 - (tan x)\<^sup>2)"
   5.181    using tan_add [of x x] by (simp add: power2_eq_square)
   5.182  
   5.183  lemma tan_gt_zero: "[| 0 < x; x < pi/2 |] ==> 0 < tan x"
   5.184 @@ -2818,13 +2818,13 @@
   5.185  lemma tan_monotone: assumes "- (pi / 2) < y" and "y < x" and "x < pi / 2"
   5.186    shows "tan y < tan x"
   5.187  proof -
   5.188 -  have "\<forall> x'. y \<le> x' \<and> x' \<le> x \<longrightarrow> DERIV tan x' :> inverse (cos x'^2)"
   5.189 +  have "\<forall> x'. y \<le> x' \<and> x' \<le> x \<longrightarrow> DERIV tan x' :> inverse ((cos x')\<^sup>2)"
   5.190    proof (rule allI, rule impI)
   5.191      fix x' :: real assume "y \<le> x' \<and> x' \<le> x"
   5.192      hence "-(pi/2) < x'" and "x' < pi/2" using assms by auto
   5.193      from cos_gt_zero_pi[OF this]
   5.194      have "cos x' \<noteq> 0" by auto
   5.195 -    thus "DERIV tan x' :> inverse (cos x'^2)" by (rule DERIV_tan)
   5.196 +    thus "DERIV tan x' :> inverse ((cos x')\<^sup>2)" by (rule DERIV_tan)
   5.197    qed
   5.198    from MVT2[OF `y < x` this]
   5.199    obtain z where "y < z" and "z < x" and tan_diff: "tan x - tan y = (x - y) * inverse ((cos z)\<^sup>2)" by auto
   5.200 @@ -3058,7 +3058,7 @@
   5.201    using tan_arctan [of x] unfolding tan_def cos_arctan
   5.202    by (simp add: eq_divide_eq)
   5.203  
   5.204 -lemma tan_sec: "cos x \<noteq> 0 ==> 1 + tan(x) ^ 2 = inverse(cos x) ^ 2"
   5.205 +lemma tan_sec: "cos x \<noteq> 0 ==> 1 + (tan x)\<^sup>2 = (inverse (cos x))\<^sup>2"
   5.206  apply (rule power_inverse [THEN subst])
   5.207  apply (rule_tac c1 = "(cos x)\<^sup>2" in real_mult_right_cancel [THEN iffD1])
   5.208  apply (auto dest: field_power_not_zero
   5.209 @@ -3427,10 +3427,10 @@
   5.210    assumes "\<bar>x\<bar> \<le> 1" shows "summable (\<lambda> k. (-1)^k * (1 / real (k*2+1) * x ^ (k*2+1)))" (is "summable (?c x)")
   5.211    by (rule summable_Leibniz(1), rule zeroseq_arctan_series[OF assms], rule monoseq_arctan_series[OF assms])
   5.212  
   5.213 -lemma less_one_imp_sqr_less_one: fixes x :: real assumes "\<bar>x\<bar> < 1" shows "x^2 < 1"
   5.214 +lemma less_one_imp_sqr_less_one: fixes x :: real assumes "\<bar>x\<bar> < 1" shows "x\<^sup>2 < 1"
   5.215  proof -
   5.216    from mult_left_mono[OF less_imp_le[OF `\<bar>x\<bar> < 1`] abs_ge_zero[of x]]
   5.217 -  have "\<bar> x^2 \<bar> < 1" using `\<bar> x \<bar> < 1` unfolding numeral_2_eq_2 power_Suc2 by auto
   5.218 +  have "\<bar>x\<^sup>2\<bar> < 1" using `\<bar>x\<bar> < 1` unfolding numeral_2_eq_2 power_Suc2 by auto
   5.219    thus ?thesis using zero_le_power2 by auto
   5.220  qed
   5.221  
   5.222 @@ -3442,9 +3442,9 @@
   5.223    { fix n :: nat assume "even n" hence "2 * (n div 2) = n" by presburger } note n_even=this
   5.224    have if_eq: "\<And> n x'. ?f n * real (Suc n) * x'^n = (if even n then (-1)^(n div 2) * x'^(2 * (n div 2)) else 0)" using n_even by auto
   5.225  
   5.226 -  { fix x :: real assume "\<bar>x\<bar> < 1" hence "x^2 < 1" by (rule less_one_imp_sqr_less_one)
   5.227 -    have "summable (\<lambda> n. -1 ^ n * (x^2) ^n)"
   5.228 -      by (rule summable_Leibniz(1), auto intro!: LIMSEQ_realpow_zero monoseq_realpow `x^2 < 1` order_less_imp_le[OF `x^2 < 1`])
   5.229 +  { fix x :: real assume "\<bar>x\<bar> < 1" hence "x\<^sup>2 < 1" by (rule less_one_imp_sqr_less_one)
   5.230 +    have "summable (\<lambda> n. -1 ^ n * (x\<^sup>2) ^n)"
   5.231 +      by (rule summable_Leibniz(1), auto intro!: LIMSEQ_realpow_zero monoseq_realpow `x\<^sup>2 < 1` order_less_imp_le[OF `x\<^sup>2 < 1`])
   5.232      hence "summable (\<lambda> n. -1 ^ n * x^(2*n))" unfolding power_mult .
   5.233    } note summable_Integral = this
   5.234  
   5.235 @@ -3518,11 +3518,11 @@
   5.236          proof (rule allI, rule impI)
   5.237            fix x assume "-r < x \<and> x < r" hence "\<bar>x\<bar> < r" by auto
   5.238            hence "\<bar>x\<bar> < 1" using `r < 1` by auto
   5.239 -          have "\<bar> - (x^2) \<bar> < 1" using less_one_imp_sqr_less_one[OF `\<bar>x\<bar> < 1`] by auto
   5.240 -          hence "(\<lambda> n. (- (x^2)) ^ n) sums (1 / (1 - (- (x^2))))" unfolding real_norm_def[symmetric] by (rule geometric_sums)
   5.241 -          hence "(?c' x) sums (1 / (1 - (- (x^2))))" unfolding power_mult_distrib[symmetric] power_mult nat_mult_commute[of _ 2] by auto
   5.242 -          hence suminf_c'_eq_geom: "inverse (1 + x^2) = suminf (?c' x)" using sums_unique unfolding inverse_eq_divide by auto
   5.243 -          have "DERIV (\<lambda> x. suminf (?c x)) x :> (inverse (1 + x^2))" unfolding suminf_c'_eq_geom
   5.244 +          have "\<bar> - (x\<^sup>2) \<bar> < 1" using less_one_imp_sqr_less_one[OF `\<bar>x\<bar> < 1`] by auto
   5.245 +          hence "(\<lambda> n. (- (x\<^sup>2)) ^ n) sums (1 / (1 - (- (x\<^sup>2))))" unfolding real_norm_def[symmetric] by (rule geometric_sums)
   5.246 +          hence "(?c' x) sums (1 / (1 - (- (x\<^sup>2))))" unfolding power_mult_distrib[symmetric] power_mult nat_mult_commute[of _ 2] by auto
   5.247 +          hence suminf_c'_eq_geom: "inverse (1 + x\<^sup>2) = suminf (?c' x)" using sums_unique unfolding inverse_eq_divide by auto
   5.248 +          have "DERIV (\<lambda> x. suminf (?c x)) x :> (inverse (1 + x\<^sup>2))" unfolding suminf_c'_eq_geom
   5.249              by (rule DERIV_arctan_suminf[OF `0 < r` `r < 1` `\<bar>x\<bar> < r`])
   5.250            from DERIV_add_minus[OF this DERIV_arctan]
   5.251            show "DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0" unfolding diff_minus by auto
   5.252 @@ -3632,7 +3632,7 @@
   5.253  qed
   5.254  
   5.255  lemma arctan_half: fixes x :: real
   5.256 -  shows "arctan x = 2 * arctan (x / (1 + sqrt(1 + x^2)))"
   5.257 +  shows "arctan x = 2 * arctan (x / (1 + sqrt(1 + x\<^sup>2)))"
   5.258  proof -
   5.259    obtain y where low: "- (pi / 2) < y" and high: "y < pi / 2" and y_eq: "tan y = x" using tan_total by blast
   5.260    hence low2: "- (pi / 2) < y / 2" and high2: "y / 2 < pi / 2" by auto
   5.261 @@ -3640,18 +3640,18 @@
   5.262    have divide_nonzero_divide: "\<And> A B C :: real. C \<noteq> 0 \<Longrightarrow> A / B = (A / C) / (B / C)" by auto
   5.263  
   5.264    have "0 < cos y" using cos_gt_zero_pi[OF low high] .
   5.265 -  hence "cos y \<noteq> 0" and cos_sqrt: "sqrt ((cos y) ^ 2) = cos y" by auto
   5.266 -
   5.267 -  have "1 + (tan y)^2 = 1 + sin y^2 / cos y^2" unfolding tan_def power_divide ..
   5.268 -  also have "\<dots> = cos y^2 / cos y^2 + sin y^2 / cos y^2" using `cos y \<noteq> 0` by auto
   5.269 -  also have "\<dots> = 1 / cos y^2" unfolding add_divide_distrib[symmetric] sin_cos_squared_add2 ..
   5.270 -  finally have "1 + (tan y)^2 = 1 / cos y^2" .
   5.271 +  hence "cos y \<noteq> 0" and cos_sqrt: "sqrt ((cos y)\<^sup>2) = cos y" by auto
   5.272 +
   5.273 +  have "1 + (tan y)\<^sup>2 = 1 + (sin y)\<^sup>2 / (cos y)\<^sup>2" unfolding tan_def power_divide ..
   5.274 +  also have "\<dots> = (cos y)\<^sup>2 / (cos y)\<^sup>2 + (sin y)\<^sup>2 / (cos y)\<^sup>2" using `cos y \<noteq> 0` by auto
   5.275 +  also have "\<dots> = 1 / (cos y)\<^sup>2" unfolding add_divide_distrib[symmetric] sin_cos_squared_add2 ..
   5.276 +  finally have "1 + (tan y)\<^sup>2 = 1 / (cos y)\<^sup>2" .
   5.277  
   5.278    have "sin y / (cos y + 1) = tan y / ((cos y + 1) / cos y)" unfolding tan_def divide_nonzero_divide[OF `cos y \<noteq> 0`, symmetric] ..
   5.279    also have "\<dots> = tan y / (1 + 1 / cos y)" using `cos y \<noteq> 0` unfolding add_divide_distrib by auto
   5.280 -  also have "\<dots> = tan y / (1 + 1 / sqrt(cos y^2))" unfolding cos_sqrt ..
   5.281 -  also have "\<dots> = tan y / (1 + sqrt(1 / cos y^2))" unfolding real_sqrt_divide by auto
   5.282 -  finally have eq: "sin y / (cos y + 1) = tan y / (1 + sqrt(1 + (tan y)^2))" unfolding `1 + (tan y)^2 = 1 / cos y^2` .
   5.283 +  also have "\<dots> = tan y / (1 + 1 / sqrt ((cos y)\<^sup>2))" unfolding cos_sqrt ..
   5.284 +  also have "\<dots> = tan y / (1 + sqrt (1 / (cos y)\<^sup>2))" unfolding real_sqrt_divide by auto
   5.285 +  finally have eq: "sin y / (cos y + 1) = tan y / (1 + sqrt(1 + (tan y)\<^sup>2))" unfolding `1 + (tan y)\<^sup>2 = 1 / (cos y)\<^sup>2` .
   5.286  
   5.287    have "arctan x = y" using arctan_tan low high y_eq by auto
   5.288    also have "\<dots> = 2 * (arctan (tan (y/2)))" using arctan_tan[OF low2 high2] by auto