src/HOL/Transcendental.thy
changeset 61944 5d06ecfdb472
parent 61942 f02b26f7d39d
child 61969 e01015e49041
     1.1 --- a/src/HOL/Transcendental.thy	Sun Dec 27 22:07:17 2015 +0100
     1.2 +++ b/src/HOL/Transcendental.thy	Mon Dec 28 01:26:34 2015 +0100
     1.3 @@ -1872,7 +1872,7 @@
     1.4    done
     1.5  
     1.6  lemma abs_ln_one_plus_x_minus_x_bound_nonneg:
     1.7 -  fixes x::real shows "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> abs(ln (1 + x) - x) <= x\<^sup>2"
     1.8 +  fixes x::real shows "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> \<bar>ln (1 + x) - x\<bar> <= x\<^sup>2"
     1.9  proof -
    1.10    assume x: "0 <= x"
    1.11    assume x1: "x <= 1"
    1.12 @@ -1880,7 +1880,7 @@
    1.13      by (rule ln_add_one_self_le_self)
    1.14    then have "ln (1 + x) - x <= 0"
    1.15      by simp
    1.16 -  then have "abs(ln(1 + x) - x) = - (ln(1 + x) - x)"
    1.17 +  then have "\<bar>ln(1 + x) - x\<bar> = - (ln(1 + x) - x)"
    1.18      by (rule abs_of_nonpos)
    1.19    also have "... = x - ln (1 + x)"
    1.20      by simp
    1.21 @@ -1895,11 +1895,11 @@
    1.22  qed
    1.23  
    1.24  lemma abs_ln_one_plus_x_minus_x_bound_nonpos:
    1.25 -  fixes x::real shows "-(1 / 2) <= x \<Longrightarrow> x <= 0 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
    1.26 +  fixes x::real shows "-(1 / 2) <= x \<Longrightarrow> x <= 0 \<Longrightarrow> \<bar>ln (1 + x) - x\<bar> <= 2 * x\<^sup>2"
    1.27  proof -
    1.28    assume a: "-(1 / 2) <= x"
    1.29    assume b: "x <= 0"
    1.30 -  have "abs(ln (1 + x) - x) = x - ln(1 - (-x))"
    1.31 +  have "\<bar>ln (1 + x) - x\<bar> = x - ln(1 - (-x))"
    1.32      apply (subst abs_of_nonpos)
    1.33      apply simp
    1.34      apply (rule ln_add_one_self_le_self2)
    1.35 @@ -1915,7 +1915,7 @@
    1.36  qed
    1.37  
    1.38  lemma abs_ln_one_plus_x_minus_x_bound:
    1.39 -  fixes x::real shows "abs x <= 1 / 2 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
    1.40 +  fixes x::real shows "\<bar>x\<bar> <= 1 / 2 \<Longrightarrow> \<bar>ln (1 + x) - x\<bar> <= 2 * x\<^sup>2"
    1.41    apply (case_tac "0 <= x")
    1.42    apply (rule order_trans)
    1.43    apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg)
    1.44 @@ -2648,7 +2648,7 @@
    1.45    fixes x :: real
    1.46    shows "(\<lambda>n. (1 + x / n) ^ n) ----> exp x"
    1.47  proof (rule filterlim_mono_eventually)
    1.48 -  from reals_Archimedean2 [of "abs x"] obtain n :: nat where *: "real n > abs x" ..
    1.49 +  from reals_Archimedean2 [of "\<bar>x\<bar>"] obtain n :: nat where *: "real n > \<bar>x\<bar>" ..
    1.50    hence "eventually (\<lambda>n :: nat. 0 < 1 + x / real n) at_top"
    1.51      apply (intro eventually_sequentiallyI [of n])
    1.52      apply (case_tac "x \<ge> 0")
    1.53 @@ -3100,7 +3100,7 @@
    1.54    by (simp add: power2_eq_square)
    1.55  
    1.56  lemma sin_cos_le1:
    1.57 -  fixes x::real shows "abs (sin x * sin y + cos x * cos y) \<le> 1"
    1.58 +  fixes x::real shows "\<bar>sin x * sin y + cos x * cos y\<bar> \<le> 1"
    1.59    using cos_diff [of x y]
    1.60    by (metis abs_cos_le_one add.commute)
    1.61  
    1.62 @@ -4225,11 +4225,11 @@
    1.63  lemma tan_pos_pi2_le: "0 \<le> x ==> x < pi/2 \<Longrightarrow> 0 \<le> tan x"
    1.64    using less_eq_real_def tan_gt_zero by auto
    1.65  
    1.66 -lemma cos_tan: "abs(x) < pi/2 \<Longrightarrow> cos(x) = 1 / sqrt(1 + tan(x) ^ 2)"
    1.67 +lemma cos_tan: "\<bar>x\<bar> < pi/2 \<Longrightarrow> cos(x) = 1 / sqrt(1 + tan(x) ^ 2)"
    1.68    using cos_gt_zero_pi [of x]
    1.69    by (simp add: divide_simps tan_def real_sqrt_divide abs_if split: split_if_asm)
    1.70  
    1.71 -lemma sin_tan: "abs(x) < pi/2 \<Longrightarrow> sin(x) = tan(x) / sqrt(1 + tan(x) ^ 2)"
    1.72 +lemma sin_tan: "\<bar>x\<bar> < pi/2 \<Longrightarrow> sin(x) = tan(x) / sqrt(1 + tan(x) ^ 2)"
    1.73    using cos_gt_zero [of "x"] cos_gt_zero [of "-x"]
    1.74    by (force simp add: divide_simps tan_def real_sqrt_divide abs_if split: split_if_asm)
    1.75  
    1.76 @@ -4244,7 +4244,7 @@
    1.77           \<Longrightarrow> (tan(x) \<le> tan(y) \<longleftrightarrow> x \<le> y)"
    1.78    by (meson tan_mono_le not_le tan_monotone)
    1.79  
    1.80 -lemma tan_bound_pi2: "abs(x) < pi/4 \<Longrightarrow> abs(tan x) < 1"
    1.81 +lemma tan_bound_pi2: "\<bar>x\<bar> < pi/4 \<Longrightarrow> \<bar>tan x\<bar> < 1"
    1.82    using tan_45 tan_monotone [of x "pi/4"] tan_monotone [of "-x" "pi/4"]
    1.83    by (auto simp: abs_if split: split_if_asm)
    1.84  
    1.85 @@ -4404,7 +4404,7 @@
    1.86  lemma arcsin_minus: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin(-x) = -arcsin x"
    1.87    by (metis (no_types, hide_lams) arcsin arcsin_sin minus_minus neg_le_iff_le sin_minus)
    1.88  
    1.89 -lemma arcsin_eq_iff: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> (arcsin x = arcsin y \<longleftrightarrow> x = y)"
    1.90 +lemma arcsin_eq_iff: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> \<bar>y\<bar> \<le> 1 \<Longrightarrow> (arcsin x = arcsin y \<longleftrightarrow> x = y)"
    1.91    by (metis abs_le_iff arcsin minus_le_iff)
    1.92  
    1.93  lemma cos_arcsin_nonzero: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> cos(arcsin x) \<noteq> 0"
    1.94 @@ -4820,13 +4820,13 @@
    1.95      done
    1.96  qed
    1.97  
    1.98 -lemma arcsin_less_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> arcsin x < arcsin y \<longleftrightarrow> x < y"
    1.99 +lemma arcsin_less_mono: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> \<bar>y\<bar> \<le> 1 \<Longrightarrow> arcsin x < arcsin y \<longleftrightarrow> x < y"
   1.100    apply (rule trans [OF sin_mono_less_eq [symmetric]])
   1.101    using arcsin_ubound arcsin_lbound
   1.102    apply auto
   1.103    done
   1.104  
   1.105 -lemma arcsin_le_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> arcsin x \<le> arcsin y \<longleftrightarrow> x \<le> y"
   1.106 +lemma arcsin_le_mono: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> \<bar>y\<bar> \<le> 1 \<Longrightarrow> arcsin x \<le> arcsin y \<longleftrightarrow> x \<le> y"
   1.107    using arcsin_less_mono not_le by blast
   1.108  
   1.109  lemma arcsin_less_arcsin: "-1 \<le> x \<Longrightarrow> x < y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arcsin x < arcsin y"
   1.110 @@ -4835,13 +4835,13 @@
   1.111  lemma arcsin_le_arcsin: "-1 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arcsin x \<le> arcsin y"
   1.112    using arcsin_le_mono by auto
   1.113  
   1.114 -lemma arccos_less_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> (arccos x < arccos y \<longleftrightarrow> y < x)"
   1.115 +lemma arccos_less_mono: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> \<bar>y\<bar> \<le> 1 \<Longrightarrow> (arccos x < arccos y \<longleftrightarrow> y < x)"
   1.116    apply (rule trans [OF cos_mono_less_eq [symmetric]])
   1.117    using arccos_ubound arccos_lbound
   1.118    apply auto
   1.119    done
   1.120  
   1.121 -lemma arccos_le_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> arccos x \<le> arccos y \<longleftrightarrow> y \<le> x"
   1.122 +lemma arccos_le_mono: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> \<bar>y\<bar> \<le> 1 \<Longrightarrow> arccos x \<le> arccos y \<longleftrightarrow> y \<le> x"
   1.123    using arccos_less_mono [of y x]
   1.124    by (simp add: not_le [symmetric])
   1.125  
   1.126 @@ -4851,7 +4851,7 @@
   1.127  lemma arccos_le_arccos: "-1 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arccos y \<le> arccos x"
   1.128    using arccos_le_mono by auto
   1.129  
   1.130 -lemma arccos_eq_iff: "abs x \<le> 1 & abs y \<le> 1 \<Longrightarrow> (arccos x = arccos y \<longleftrightarrow> x = y)"
   1.131 +lemma arccos_eq_iff: "\<bar>x\<bar> \<le> 1 & \<bar>y\<bar> \<le> 1 \<Longrightarrow> (arccos x = arccos y \<longleftrightarrow> x = y)"
   1.132    using cos_arccos_abs by fastforce
   1.133  
   1.134  subsection \<open>Machins formula\<close>