src/HOL/Nonstandard_Analysis/HTranscendental.thy
author paulson <lp15@cam.ac.uk>
Sun Apr 28 18:06:47 2019 +0100 (8 months ago)
changeset 70209 ab29bd01b8b2
parent 70208 65b3bfc565b5
child 70210 1ececb77b27a
permissions -rw-r--r--
further de-applying
wenzelm@62479
     1
(*  Title:      HOL/Nonstandard_Analysis/HTranscendental.thy
wenzelm@62479
     2
    Author:     Jacques D. Fleuriot
wenzelm@62479
     3
    Copyright:  2001 University of Edinburgh
huffman@27468
     4
huffman@27468
     5
Converted to Isar and polished by lcp
huffman@27468
     6
*)
huffman@27468
     7
wenzelm@61975
     8
section\<open>Nonstandard Extensions of Transcendental Functions\<close>
huffman@27468
     9
huffman@27468
    10
theory HTranscendental
lp15@70208
    11
imports Complex_Main HSeries HDeriv Sketch_and_Explore
huffman@27468
    12
begin
huffman@27468
    13
lp15@70208
    14
lp15@70208
    15
sledgehammer_params [timeout = 90]
lp15@70208
    16
huffman@27468
    17
definition
lp15@70208
    18
  exphr :: "real \<Rightarrow> hypreal" where
wenzelm@67443
    19
    \<comment> \<open>define exponential function using standard part\<close>
lp15@70208
    20
  "exphr x \<equiv>  st(sumhr (0, whn, \<lambda>n. inverse (fact n) * (x ^ n)))"
huffman@27468
    21
huffman@27468
    22
definition
lp15@70208
    23
  sinhr :: "real \<Rightarrow> hypreal" where
lp15@70208
    24
  "sinhr x \<equiv> st(sumhr (0, whn, \<lambda>n. sin_coeff n * x ^ n))"
huffman@27468
    25
  
huffman@27468
    26
definition
lp15@70208
    27
  coshr :: "real \<Rightarrow> hypreal" where
lp15@70208
    28
  "coshr x \<equiv> st(sumhr (0, whn, \<lambda>n. cos_coeff n * x ^ n))"
huffman@27468
    29
huffman@27468
    30
wenzelm@61975
    31
subsection\<open>Nonstandard Extension of Square Root Function\<close>
huffman@27468
    32
huffman@27468
    33
lemma STAR_sqrt_zero [simp]: "( *f* sqrt) 0 = 0"
lp15@70208
    34
  by (simp add: starfun star_n_zero_num)
huffman@27468
    35
huffman@27468
    36
lemma STAR_sqrt_one [simp]: "( *f* sqrt) 1 = 1"
lp15@70208
    37
  by (simp add: starfun star_n_one_num)
huffman@27468
    38
huffman@27468
    39
lemma hypreal_sqrt_pow2_iff: "(( *f* sqrt)(x) ^ 2 = x) = (0 \<le> x)"
lp15@70208
    40
proof (cases x)
lp15@70208
    41
  case (star_n X)
lp15@70208
    42
  then show ?thesis
lp15@70208
    43
    by (simp add: star_n_le star_n_zero_num starfun hrealpow star_n_eq_iff del: hpowr_Suc power_Suc)
lp15@70208
    44
qed
huffman@27468
    45
lp15@70208
    46
lemma hypreal_sqrt_gt_zero_pow2: "\<And>x. 0 < x \<Longrightarrow> ( *f* sqrt) (x) ^ 2 = x"
lp15@70208
    47
  by transfer simp
huffman@27468
    48
lp15@70208
    49
lemma hypreal_sqrt_pow2_gt_zero: "0 < x \<Longrightarrow> 0 < ( *f* sqrt) (x) ^ 2"
lp15@70208
    50
  by (frule hypreal_sqrt_gt_zero_pow2, auto)
lp15@70208
    51
lp15@70208
    52
lemma hypreal_sqrt_not_zero: "0 < x \<Longrightarrow> ( *f* sqrt) (x) \<noteq> 0"
lp15@70208
    53
  using hypreal_sqrt_gt_zero_pow2 by fastforce
huffman@27468
    54
huffman@27468
    55
lemma hypreal_inverse_sqrt_pow2:
lp15@70208
    56
     "0 < x \<Longrightarrow> inverse (( *f* sqrt)(x)) ^ 2 = inverse x"
lp15@70208
    57
  by (simp add: hypreal_sqrt_gt_zero_pow2 power_inverse)
huffman@27468
    58
huffman@27468
    59
lemma hypreal_sqrt_mult_distrib: 
lp15@70208
    60
    "\<And>x y. \<lbrakk>0 < x; 0 <y\<rbrakk> \<Longrightarrow>
huffman@27468
    61
      ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)"
lp15@70208
    62
  by transfer (auto intro: real_sqrt_mult) 
huffman@27468
    63
huffman@27468
    64
lemma hypreal_sqrt_mult_distrib2:
lp15@70208
    65
     "\<lbrakk>0\<le>x; 0\<le>y\<rbrakk> \<Longrightarrow>  ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)"
huffman@27468
    66
by (auto intro: hypreal_sqrt_mult_distrib simp add: order_le_less)
huffman@27468
    67
huffman@27468
    68
lemma hypreal_sqrt_approx_zero [simp]:
lp15@70208
    69
  assumes "0 < x"
lp15@70208
    70
  shows "(( *f* sqrt) x \<approx> 0) \<longleftrightarrow> (x \<approx> 0)"
lp15@70208
    71
proof -
lp15@70208
    72
  have "( *f* sqrt) x \<in> Infinitesimal \<longleftrightarrow> ((*f* sqrt) x)\<^sup>2 \<in> Infinitesimal"
lp15@70208
    73
    by (metis Infinitesimal_hrealpow pos2 power2_eq_square Infinitesimal_square_iff)
lp15@70208
    74
  also have "... \<longleftrightarrow> x \<in> Infinitesimal"
lp15@70208
    75
    by (simp add: assms hypreal_sqrt_gt_zero_pow2)
lp15@70208
    76
  finally show ?thesis
lp15@70208
    77
    using mem_infmal_iff by blast
lp15@70208
    78
qed
huffman@27468
    79
huffman@27468
    80
lemma hypreal_sqrt_approx_zero2 [simp]:
lp15@70208
    81
  "0 \<le> x \<Longrightarrow> (( *f* sqrt)(x) \<approx> 0) = (x \<approx> 0)"
lp15@70208
    82
  by (auto simp add: order_le_less)
huffman@27468
    83
lp15@70208
    84
lemma hypreal_sqrt_gt_zero: "\<And>x. 0 < x \<Longrightarrow> 0 < ( *f* sqrt)(x)"
lp15@70208
    85
  by transfer (simp add: real_sqrt_gt_zero)
huffman@27468
    86
lp15@70208
    87
lemma hypreal_sqrt_ge_zero: "0 \<le> x \<Longrightarrow> 0 \<le> ( *f* sqrt)(x)"
lp15@70208
    88
  by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less)
huffman@27468
    89
lp15@70208
    90
lemma hypreal_sqrt_hrabs [simp]: "\<And>x. ( *f* sqrt)(x\<^sup>2) = \<bar>x\<bar>"
lp15@70208
    91
  by transfer simp
huffman@27468
    92
lp15@70208
    93
lemma hypreal_sqrt_hrabs2 [simp]: "\<And>x. ( *f* sqrt)(x*x) = \<bar>x\<bar>"
lp15@70208
    94
  by transfer simp
huffman@27468
    95
huffman@27468
    96
lemma hypreal_sqrt_hyperpow_hrabs [simp]:
lp15@70208
    97
  "\<And>x. ( *f* sqrt)(x pow (hypnat_of_nat 2)) = \<bar>x\<bar>"
lp15@70208
    98
  by transfer simp
huffman@27468
    99
huffman@27468
   100
lemma star_sqrt_HFinite: "\<lbrakk>x \<in> HFinite; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> HFinite"
lp15@70208
   101
  by (metis HFinite_square_iff hypreal_sqrt_pow2_iff power2_eq_square)
huffman@27468
   102
huffman@27468
   103
lemma st_hypreal_sqrt:
lp15@70208
   104
  assumes "x \<in> HFinite" "0 \<le> x"
lp15@70208
   105
  shows "st(( *f* sqrt) x) = ( *f* sqrt)(st x)"
lp15@70208
   106
proof (rule power_inject_base)
lp15@70208
   107
  show "st ((*f* sqrt) x) ^ Suc 1 = (*f* sqrt) (st x) ^ Suc 1"
lp15@70208
   108
    using assms hypreal_sqrt_pow2_iff [of x]
lp15@70208
   109
    by (metis HFinite_square_iff hypreal_sqrt_hrabs2 power2_eq_square st_hrabs st_mult)
lp15@70208
   110
  show "0 \<le> st ((*f* sqrt) x)"
lp15@70208
   111
    by (simp add: assms hypreal_sqrt_ge_zero st_zero_le star_sqrt_HFinite)
lp15@70208
   112
  show "0 \<le> (*f* sqrt) (st x)"
lp15@70208
   113
    by (simp add: assms hypreal_sqrt_ge_zero st_zero_le)
lp15@70208
   114
qed
huffman@27468
   115
lp15@70208
   116
lemma hypreal_sqrt_sum_squares_ge1 [simp]: "\<And>x y. x \<le> ( *f* sqrt)(x\<^sup>2 + y\<^sup>2)"
lp15@70208
   117
  by transfer (rule real_sqrt_sum_squares_ge1)
huffman@27468
   118
huffman@27468
   119
lemma HFinite_hypreal_sqrt_imp_HFinite:
lp15@70208
   120
  "\<lbrakk>0 \<le> x; ( *f* sqrt) x \<in> HFinite\<rbrakk> \<Longrightarrow> x \<in> HFinite"
lp15@70208
   121
  by (metis HFinite_mult hrealpow_two hypreal_sqrt_pow2_iff numeral_2_eq_2)
huffman@27468
   122
huffman@27468
   123
lemma HFinite_hypreal_sqrt_iff [simp]:
lp15@70208
   124
  "0 \<le> x \<Longrightarrow> (( *f* sqrt) x \<in> HFinite) = (x \<in> HFinite)"
lp15@70208
   125
  by (blast intro: star_sqrt_HFinite HFinite_hypreal_sqrt_imp_HFinite)
huffman@27468
   126
huffman@27468
   127
lemma Infinitesimal_hypreal_sqrt:
lp15@70208
   128
     "\<lbrakk>0 \<le> x; x \<in> Infinitesimal\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> Infinitesimal"
lp15@70208
   129
  by (simp add: mem_infmal_iff)
huffman@27468
   130
huffman@27468
   131
lemma Infinitesimal_hypreal_sqrt_imp_Infinitesimal:
lp15@70208
   132
     "\<lbrakk>0 \<le> x; ( *f* sqrt) x \<in> Infinitesimal\<rbrakk> \<Longrightarrow> x \<in> Infinitesimal"
lp15@70208
   133
  using hypreal_sqrt_approx_zero2 mem_infmal_iff by blast
huffman@27468
   134
huffman@27468
   135
lemma Infinitesimal_hypreal_sqrt_iff [simp]:
lp15@70208
   136
     "0 \<le> x \<Longrightarrow> (( *f* sqrt) x \<in> Infinitesimal) = (x \<in> Infinitesimal)"
huffman@27468
   137
by (blast intro: Infinitesimal_hypreal_sqrt_imp_Infinitesimal Infinitesimal_hypreal_sqrt)
huffman@27468
   138
huffman@27468
   139
lemma HInfinite_hypreal_sqrt:
lp15@70208
   140
     "\<lbrakk>0 \<le> x; x \<in> HInfinite\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> HInfinite"
lp15@70208
   141
  by (simp add: HInfinite_HFinite_iff)
huffman@27468
   142
huffman@27468
   143
lemma HInfinite_hypreal_sqrt_imp_HInfinite:
lp15@70208
   144
     "\<lbrakk>0 \<le> x; ( *f* sqrt) x \<in> HInfinite\<rbrakk> \<Longrightarrow> x \<in> HInfinite"
lp15@70208
   145
  using HFinite_hypreal_sqrt_iff HInfinite_HFinite_iff by blast
huffman@27468
   146
huffman@27468
   147
lemma HInfinite_hypreal_sqrt_iff [simp]:
lp15@70208
   148
     "0 \<le> x \<Longrightarrow> (( *f* sqrt) x \<in> HInfinite) = (x \<in> HInfinite)"
huffman@27468
   149
by (blast intro: HInfinite_hypreal_sqrt HInfinite_hypreal_sqrt_imp_HInfinite)
huffman@27468
   150
huffman@27468
   151
lemma HFinite_exp [simp]:
lp15@70208
   152
  "sumhr (0, whn, \<lambda>n. inverse (fact n) * x ^ n) \<in> HFinite"
lp15@70208
   153
  unfolding sumhr_app star_zero_def starfun2_star_of atLeast0LessThan
lp15@70208
   154
  by (metis NSBseqD2 NSconvergent_NSBseq convergent_NSconvergent_iff summable_iff_convergent summable_exp)
huffman@27468
   155
huffman@27468
   156
lemma exphr_zero [simp]: "exphr 0 = 1"
lp15@70208
   157
proof -
lp15@70208
   158
  have "\<forall>x>1. 1 = sumhr (0, 1, \<lambda>n. inverse (fact n) * 0 ^ n) + sumhr (1, x, \<lambda>n. inverse (fact n) * 0 ^ n)"
lp15@70208
   159
    unfolding sumhr_app by transfer (simp add: power_0_left)
lp15@70208
   160
  then have "sumhr (0, 1, \<lambda>n. inverse (fact n) * 0 ^ n) + sumhr (1, whn, \<lambda>n. inverse (fact n) * 0 ^ n) \<approx> 1"
lp15@70208
   161
    by auto
lp15@70208
   162
  then show ?thesis
lp15@70208
   163
    unfolding exphr_def
lp15@70208
   164
    using sumhr_split_add [OF hypnat_one_less_hypnat_omega] st_unique by auto
lp15@70208
   165
qed
huffman@27468
   166
huffman@27468
   167
lemma coshr_zero [simp]: "coshr 0 = 1"
lp15@70209
   168
  proof -
lp15@70209
   169
  have "\<forall>x>1. 1 = sumhr (0, 1, \<lambda>n. cos_coeff n * 0 ^ n) + sumhr (1, x, \<lambda>n. cos_coeff n * 0 ^ n)"
lp15@70209
   170
    unfolding sumhr_app by transfer (simp add: power_0_left)
lp15@70209
   171
  then have "sumhr (0, 1, \<lambda>n. cos_coeff n * 0 ^ n) + sumhr (1, whn, \<lambda>n. cos_coeff n * 0 ^ n) \<approx> 1"
lp15@70209
   172
    by auto
lp15@70209
   173
  then show ?thesis
lp15@70209
   174
    unfolding coshr_def
lp15@70209
   175
    using sumhr_split_add [OF hypnat_one_less_hypnat_omega] st_unique by auto
lp15@70209
   176
qed
huffman@27468
   177
wenzelm@61982
   178
lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) (0::hypreal) \<approx> 1"
lp15@70209
   179
  proof -
lp15@70209
   180
  have "(*f* exp) (0::real star) = 1"
lp15@70209
   181
    by transfer simp
lp15@70209
   182
  then show ?thesis
lp15@70209
   183
    by auto
lp15@70209
   184
qed
huffman@27468
   185
lp15@70209
   186
lemma STAR_exp_Infinitesimal: 
lp15@70209
   187
  assumes "x \<in> Infinitesimal" shows "( *f* exp) (x::hypreal) \<approx> 1"
lp15@70209
   188
proof (cases "x = 0")
lp15@70209
   189
  case False
lp15@70209
   190
  have "NSDERIV exp 0 :> 1"
lp15@70209
   191
    by (metis DERIV_exp NSDERIV_DERIV_iff exp_zero)
lp15@70209
   192
  then have "((*f* exp) x - 1) / x \<approx> 1"
lp15@70209
   193
    using nsderiv_def False NSDERIVD2 assms by fastforce
lp15@70209
   194
  then have "(*f* exp) x - 1 \<approx> x"
lp15@70209
   195
    using NSDERIVD4 \<open>NSDERIV exp 0 :> 1\<close> assms by fastforce
lp15@70209
   196
  then show ?thesis
lp15@70209
   197
    by (meson Infinitesimal_approx approx_minus_iff approx_trans2 assms not_Infinitesimal_not_zero)
lp15@70209
   198
qed auto
huffman@27468
   199
wenzelm@61982
   200
lemma STAR_exp_epsilon [simp]: "( *f* exp) \<epsilon> \<approx> 1"
lp15@70209
   201
  by (auto intro: STAR_exp_Infinitesimal)
huffman@27468
   202
immler@58656
   203
lemma STAR_exp_add:
lp15@70209
   204
  "\<And>(x::'a:: {banach,real_normed_field} star) y. ( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y"
lp15@70209
   205
  by transfer (rule exp_add)
huffman@27468
   206
huffman@27468
   207
lemma exphr_hypreal_of_real_exp_eq: "exphr x = hypreal_of_real (exp x)"
lp15@70209
   208
proof -
lp15@70209
   209
  have "(\<lambda>n. inverse (fact n) * x ^ n) sums exp x"
lp15@70209
   210
    using exp_converges [of x] by simp
lp15@70209
   211
  then have "(\<lambda>n. \<Sum>n<n. inverse (fact n) * x ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S exp x"
lp15@70209
   212
    using NSsums_def sums_NSsums_iff by blast
lp15@70209
   213
  then have "hypreal_of_real (exp x) \<approx> sumhr (0, whn, \<lambda>n. inverse (fact n) * x ^ n)"
lp15@70209
   214
    unfolding starfunNat_sumr [symmetric] atLeast0LessThan
lp15@70209
   215
    using HNatInfinite_whn NSLIMSEQ_iff approx_sym by blast
lp15@70209
   216
  then show ?thesis
lp15@70209
   217
    unfolding exphr_def using st_eq_approx_iff by auto
lp15@70209
   218
qed
huffman@27468
   219
lp15@70208
   220
lemma starfun_exp_ge_add_one_self [simp]: "\<And>x::hypreal. 0 \<le> x \<Longrightarrow> (1 + x) \<le> ( *f* exp) x"
lp15@70209
   221
  by transfer (rule exp_ge_add_one_self_aux)
huffman@27468
   222
lp15@70209
   223
text\<open>exp maps infinities to infinities\<close>
huffman@27468
   224
lemma starfun_exp_HInfinite:
lp15@70209
   225
  fixes x :: hypreal
lp15@70209
   226
  assumes "x \<in> HInfinite" "0 \<le> x"
lp15@70209
   227
  shows "( *f* exp) x \<in> HInfinite"
lp15@70209
   228
proof -
lp15@70209
   229
  have "x \<le> 1 + x"
lp15@70209
   230
    by simp
lp15@70209
   231
  also have "\<dots> \<le> (*f* exp) x"
lp15@70209
   232
    by (simp add: \<open>0 \<le> x\<close>)
lp15@70209
   233
  finally show ?thesis
lp15@70209
   234
    using HInfinite_ge_HInfinite assms by blast
lp15@70209
   235
qed
huffman@27468
   236
immler@58656
   237
lemma starfun_exp_minus:
lp15@70208
   238
  "\<And>x::'a:: {banach,real_normed_field} star. ( *f* exp) (-x) = inverse(( *f* exp) x)"
lp15@70209
   239
  by transfer (rule exp_minus)
huffman@27468
   240
lp15@70209
   241
text\<open>exp maps infinitesimals to infinitesimals\<close>
huffman@27468
   242
lemma starfun_exp_Infinitesimal:
lp15@70209
   243
  fixes x :: hypreal
lp15@70209
   244
  assumes "x \<in> HInfinite" "x \<le> 0"
lp15@70209
   245
  shows "( *f* exp) x \<in> Infinitesimal"
lp15@70209
   246
proof -
lp15@70209
   247
  obtain y where "x = -y" "y \<ge> 0"
lp15@70209
   248
    by (metis abs_of_nonpos assms(2) eq_abs_iff')
lp15@70209
   249
  then have "( *f* exp) y \<in> HInfinite"
lp15@70209
   250
    using HInfinite_minus_iff assms(1) starfun_exp_HInfinite by blast
lp15@70209
   251
  then show ?thesis
lp15@70209
   252
    by (simp add: HInfinite_inverse_Infinitesimal \<open>x = - y\<close> starfun_exp_minus)
lp15@70209
   253
qed
huffman@27468
   254
lp15@70208
   255
lemma starfun_exp_gt_one [simp]: "\<And>x::hypreal. 0 < x \<Longrightarrow> 1 < ( *f* exp) x"
lp15@70209
   256
  by transfer (rule exp_gt_one)
huffman@27468
   257
lp15@60017
   258
abbreviation real_ln :: "real \<Rightarrow> real" where 
lp15@60017
   259
  "real_ln \<equiv> ln"
lp15@60017
   260
lp15@70208
   261
lemma starfun_ln_exp [simp]: "\<And>x. ( *f* real_ln) (( *f* exp) x) = x"
lp15@70209
   262
  by transfer (rule ln_exp)
huffman@27468
   263
lp15@70208
   264
lemma starfun_exp_ln_iff [simp]: "\<And>x. (( *f* exp)(( *f* real_ln) x) = x) = (0 < x)"
lp15@70209
   265
  by transfer (rule exp_ln_iff)
huffman@27468
   266
lp15@70209
   267
lemma starfun_exp_ln_eq: "\<And>u x. ( *f* exp) u = x \<Longrightarrow> ( *f* real_ln) x = u"
lp15@70209
   268
  by transfer (rule ln_unique)
huffman@27468
   269
lp15@70208
   270
lemma starfun_ln_less_self [simp]: "\<And>x. 0 < x \<Longrightarrow> ( *f* real_ln) x < x"
lp15@70209
   271
  by transfer (rule ln_less_self)
huffman@27468
   272
lp15@70208
   273
lemma starfun_ln_ge_zero [simp]: "\<And>x. 1 \<le> x \<Longrightarrow> 0 \<le> ( *f* real_ln) x"
lp15@70209
   274
  by transfer (rule ln_ge_zero)
huffman@27468
   275
lp15@70208
   276
lemma starfun_ln_gt_zero [simp]: "\<And>x .1 < x \<Longrightarrow> 0 < ( *f* real_ln) x"
lp15@70209
   277
  by transfer (rule ln_gt_zero)
huffman@27468
   278
lp15@70208
   279
lemma starfun_ln_not_eq_zero [simp]: "\<And>x. \<lbrakk>0 < x; x \<noteq> 1\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<noteq> 0"
lp15@70209
   280
  by transfer simp
huffman@27468
   281
lp15@70208
   282
lemma starfun_ln_HFinite: "\<lbrakk>x \<in> HFinite; 1 \<le> x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<in> HFinite"
lp15@70209
   283
  by (metis HFinite_HInfinite_iff less_le_trans starfun_exp_HInfinite starfun_exp_ln_iff starfun_ln_ge_zero zero_less_one)
huffman@27468
   284
lp15@70208
   285
lemma starfun_ln_inverse: "\<And>x. 0 < x \<Longrightarrow> ( *f* real_ln) (inverse x) = -( *f* ln) x"
lp15@70209
   286
  by transfer (rule ln_inverse)
huffman@27468
   287
huffman@27468
   288
lemma starfun_abs_exp_cancel: "\<And>x. \<bar>( *f* exp) (x::hypreal)\<bar> = ( *f* exp) x"
lp15@70209
   289
  by transfer (rule abs_exp_cancel)
huffman@27468
   290
huffman@27468
   291
lemma starfun_exp_less_mono: "\<And>x y::hypreal. x < y \<Longrightarrow> ( *f* exp) x < ( *f* exp) y"
lp15@70209
   292
  by transfer (rule exp_less_mono)
huffman@27468
   293
lp15@70209
   294
lemma starfun_exp_HFinite: 
lp15@70209
   295
  fixes x :: hypreal
lp15@70209
   296
  assumes "x \<in> HFinite"
lp15@70209
   297
  shows "( *f* exp) x \<in> HFinite"
lp15@70209
   298
proof -
lp15@70209
   299
  obtain u where "u \<in> \<real>" "\<bar>x\<bar> < u"
lp15@70209
   300
    using HFiniteD assms by force
lp15@70209
   301
  with assms have "\<bar>(*f* exp) x\<bar> < (*f* exp) u" 
lp15@70209
   302
    using starfun_abs_exp_cancel starfun_exp_less_mono by auto
lp15@70209
   303
  with \<open>u \<in> \<real>\<close> show ?thesis
lp15@70209
   304
    by (force simp: HFinite_def Reals_eq_Standard)
lp15@70209
   305
qed
huffman@27468
   306
huffman@27468
   307
lemma starfun_exp_add_HFinite_Infinitesimal_approx:
lp15@70208
   308
     "\<lbrakk>x \<in> Infinitesimal; z \<in> HFinite\<rbrakk> \<Longrightarrow> ( *f* exp) (z + x::hypreal) \<approx> ( *f* exp) z"
huffman@27468
   309
apply (simp add: STAR_exp_add)
huffman@27468
   310
apply (frule STAR_exp_Infinitesimal)
huffman@27468
   311
apply (drule approx_mult2)
huffman@27468
   312
apply (auto intro: starfun_exp_HFinite)
huffman@27468
   313
done
huffman@27468
   314
huffman@27468
   315
(* using previous result to get to result *)
huffman@27468
   316
lemma starfun_ln_HInfinite:
lp15@70208
   317
     "\<lbrakk>x \<in> HInfinite; 0 < x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<in> HInfinite"
huffman@27468
   318
apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
huffman@27468
   319
apply (drule starfun_exp_HFinite)
huffman@27468
   320
apply (simp add: starfun_exp_ln_iff [THEN iffD2] HFinite_HInfinite_iff)
huffman@27468
   321
done
huffman@27468
   322
huffman@27468
   323
lemma starfun_exp_HInfinite_Infinitesimal_disj:
wenzelm@67091
   324
 "x \<in> HInfinite \<Longrightarrow> ( *f* exp) x \<in> HInfinite \<or> ( *f* exp) (x::hypreal) \<in> Infinitesimal"
huffman@27468
   325
apply (insert linorder_linear [of x 0]) 
huffman@27468
   326
apply (auto intro: starfun_exp_HInfinite starfun_exp_Infinitesimal)
huffman@27468
   327
done
huffman@27468
   328
lp15@70209
   329
(* check out this proof\<And>! *)
huffman@27468
   330
lemma starfun_ln_HFinite_not_Infinitesimal:
lp15@70208
   331
     "\<lbrakk>x \<in> HFinite - Infinitesimal; 0 < x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<in> HFinite"
huffman@27468
   332
apply (rule ccontr, drule HInfinite_HFinite_iff [THEN iffD2])
huffman@27468
   333
apply (drule starfun_exp_HInfinite_Infinitesimal_disj)
huffman@27468
   334
apply (simp add: starfun_exp_ln_iff [symmetric] HInfinite_HFinite_iff
huffman@27468
   335
            del: starfun_exp_ln_iff)
huffman@27468
   336
done
huffman@27468
   337
huffman@27468
   338
(* we do proof by considering ln of 1/x *)
huffman@27468
   339
lemma starfun_ln_Infinitesimal_HInfinite:
lp15@70208
   340
     "\<lbrakk>x \<in> Infinitesimal; 0 < x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<in> HInfinite"
huffman@27468
   341
apply (drule Infinitesimal_inverse_HInfinite)
huffman@27468
   342
apply (frule positive_imp_inverse_positive)
huffman@27468
   343
apply (drule_tac [2] starfun_ln_HInfinite)
huffman@27468
   344
apply (auto simp add: starfun_ln_inverse HInfinite_minus_iff)
huffman@27468
   345
done
huffman@27468
   346
lp15@70208
   347
lemma starfun_ln_less_zero: "\<And>x. \<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> ( *f* real_ln) x < 0"
huffman@27468
   348
by transfer (rule ln_less_zero)
huffman@27468
   349
huffman@27468
   350
lemma starfun_ln_Infinitesimal_less_zero:
lp15@70208
   351
     "\<lbrakk>x \<in> Infinitesimal; 0 < x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x < 0"
huffman@27468
   352
by (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def)
huffman@27468
   353
huffman@27468
   354
lemma starfun_ln_HInfinite_gt_zero:
lp15@70208
   355
     "\<lbrakk>x \<in> HInfinite; 0 < x\<rbrakk> \<Longrightarrow> 0 < ( *f* real_ln) x"
huffman@27468
   356
by (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def)
huffman@27468
   357
huffman@27468
   358
huffman@27468
   359
(*
lp15@70208
   360
Goalw [NSLIM_def] "(\<lambda>h. ((x powr h) - 1) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S ln x"
huffman@27468
   361
*)
huffman@27468
   362
lp15@70208
   363
lemma HFinite_sin [simp]: "sumhr (0, whn, \<lambda>n. sin_coeff n * x ^ n) \<in> HFinite"
huffman@27468
   364
unfolding sumhr_app
hoelzl@56194
   365
apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
huffman@27468
   366
apply (rule NSBseqD2)
huffman@27468
   367
apply (rule NSconvergent_NSBseq)
huffman@27468
   368
apply (rule convergent_NSconvergent_iff [THEN iffD1])
hoelzl@56194
   369
apply (rule summable_iff_convergent [THEN iffD1])
lp15@59658
   370
using summable_norm_sin [of x]
lp15@59658
   371
apply (simp add: summable_rabs_cancel)
huffman@27468
   372
done
huffman@27468
   373
huffman@27468
   374
lemma STAR_sin_zero [simp]: "( *f* sin) 0 = 0"
huffman@27468
   375
by transfer (rule sin_zero)
huffman@27468
   376
lp15@59658
   377
lemma STAR_sin_Infinitesimal [simp]:
lp15@59658
   378
  fixes x :: "'a::{real_normed_field,banach} star"
lp15@70208
   379
  shows "x \<in> Infinitesimal \<Longrightarrow> ( *f* sin) x \<approx> x"
huffman@27468
   380
apply (case_tac "x = 0")
huffman@27468
   381
apply (cut_tac [2] x = 0 in DERIV_sin)
huffman@27468
   382
apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
huffman@27468
   383
apply (drule bspec [where x = x], auto)
huffman@27468
   384
apply (drule approx_mult1 [where c = x])
huffman@27468
   385
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
haftmann@57512
   386
           simp add: mult.assoc)
huffman@27468
   387
done
huffman@27468
   388
lp15@70208
   389
lemma HFinite_cos [simp]: "sumhr (0, whn, \<lambda>n. cos_coeff n * x ^ n) \<in> HFinite"
huffman@27468
   390
unfolding sumhr_app
hoelzl@56194
   391
apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
huffman@27468
   392
apply (rule NSBseqD2)
huffman@27468
   393
apply (rule NSconvergent_NSBseq)
huffman@27468
   394
apply (rule convergent_NSconvergent_iff [THEN iffD1])
hoelzl@56194
   395
apply (rule summable_iff_convergent [THEN iffD1])
lp15@59658
   396
using summable_norm_cos [of x]
lp15@59658
   397
apply (simp add: summable_rabs_cancel)
huffman@27468
   398
done
huffman@27468
   399
huffman@27468
   400
lemma STAR_cos_zero [simp]: "( *f* cos) 0 = 1"
huffman@27468
   401
by transfer (rule cos_zero)
huffman@27468
   402
lp15@59658
   403
lemma STAR_cos_Infinitesimal [simp]:
lp15@59658
   404
  fixes x :: "'a::{real_normed_field,banach} star"
lp15@70208
   405
  shows "x \<in> Infinitesimal \<Longrightarrow> ( *f* cos) x \<approx> 1"
huffman@27468
   406
apply (case_tac "x = 0")
huffman@27468
   407
apply (cut_tac [2] x = 0 in DERIV_cos)
huffman@27468
   408
apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
huffman@27468
   409
apply (drule bspec [where x = x])
huffman@27468
   410
apply auto
huffman@27468
   411
apply (drule approx_mult1 [where c = x])
huffman@27468
   412
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
haftmann@57512
   413
            simp add: mult.assoc)
huffman@27468
   414
apply (rule approx_add_right_cancel [where d = "-1"])
haftmann@54489
   415
apply simp
huffman@27468
   416
done
huffman@27468
   417
huffman@27468
   418
lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
huffman@27468
   419
by transfer (rule tan_zero)
huffman@27468
   420
lp15@70208
   421
lemma STAR_tan_Infinitesimal: "x \<in> Infinitesimal \<Longrightarrow> ( *f* tan) x \<approx> x"
huffman@27468
   422
apply (case_tac "x = 0")
huffman@27468
   423
apply (cut_tac [2] x = 0 in DERIV_tan)
huffman@27468
   424
apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
huffman@27468
   425
apply (drule bspec [where x = x], auto)
huffman@27468
   426
apply (drule approx_mult1 [where c = x])
huffman@27468
   427
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
haftmann@57512
   428
             simp add: mult.assoc)
huffman@27468
   429
done
huffman@27468
   430
huffman@27468
   431
lemma STAR_sin_cos_Infinitesimal_mult:
lp15@59658
   432
  fixes x :: "'a::{real_normed_field,banach} star"
lp15@70208
   433
  shows "x \<in> Infinitesimal \<Longrightarrow> ( *f* sin) x * ( *f* cos) x \<approx> x"
lp15@59658
   434
using approx_mult_HFinite [of "( *f* sin) x" _ "( *f* cos) x" 1] 
lp15@59658
   435
by (simp add: Infinitesimal_subset_HFinite [THEN subsetD])
huffman@27468
   436
huffman@27468
   437
lemma HFinite_pi: "hypreal_of_real pi \<in> HFinite"
huffman@27468
   438
by simp
huffman@27468
   439
huffman@27468
   440
(* lemmas *)
huffman@27468
   441
huffman@27468
   442
lemma lemma_split_hypreal_of_real:
huffman@27468
   443
     "N \<in> HNatInfinite  
lp15@70208
   444
      \<Longrightarrow> hypreal_of_real a =  
huffman@27468
   445
          hypreal_of_hypnat N * (inverse(hypreal_of_hypnat N) * hypreal_of_real a)"
haftmann@57512
   446
by (simp add: mult.assoc [symmetric] zero_less_HNatInfinite)
huffman@27468
   447
huffman@27468
   448
lemma STAR_sin_Infinitesimal_divide:
lp15@59658
   449
  fixes x :: "'a::{real_normed_field,banach} star"
lp15@70208
   450
  shows "\<lbrakk>x \<in> Infinitesimal; x \<noteq> 0\<rbrakk> \<Longrightarrow> ( *f* sin) x/x \<approx> 1"
lp15@59658
   451
using DERIV_sin [of "0::'a"]
lp15@59658
   452
by (simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
huffman@27468
   453
huffman@27468
   454
(*------------------------------------------------------------------------*) 
wenzelm@61982
   455
(* sin* (1/n) * 1/(1/n) \<approx> 1 for n = oo                                   *)
huffman@27468
   456
(*------------------------------------------------------------------------*)
huffman@27468
   457
huffman@27468
   458
lemma lemma_sin_pi:
huffman@27468
   459
     "n \<in> HNatInfinite  
lp15@70208
   460
      \<Longrightarrow> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) \<approx> 1"
huffman@27468
   461
apply (rule STAR_sin_Infinitesimal_divide)
huffman@27468
   462
apply (auto simp add: zero_less_HNatInfinite)
huffman@27468
   463
done
huffman@27468
   464
huffman@27468
   465
lemma STAR_sin_inverse_HNatInfinite:
huffman@27468
   466
     "n \<in> HNatInfinite  
lp15@70208
   467
      \<Longrightarrow> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n \<approx> 1"
huffman@27468
   468
apply (frule lemma_sin_pi)
huffman@27468
   469
apply (simp add: divide_inverse)
huffman@27468
   470
done
huffman@27468
   471
huffman@27468
   472
lemma Infinitesimal_pi_divide_HNatInfinite: 
huffman@27468
   473
     "N \<in> HNatInfinite  
lp15@70208
   474
      \<Longrightarrow> hypreal_of_real pi/(hypreal_of_hypnat N) \<in> Infinitesimal"
huffman@27468
   475
apply (simp add: divide_inverse)
huffman@27468
   476
apply (auto intro: Infinitesimal_HFinite_mult2)
huffman@27468
   477
done
huffman@27468
   478
huffman@27468
   479
lemma pi_divide_HNatInfinite_not_zero [simp]:
lp15@70208
   480
     "N \<in> HNatInfinite \<Longrightarrow> hypreal_of_real pi/(hypreal_of_hypnat N) \<noteq> 0"
huffman@27468
   481
by (simp add: zero_less_HNatInfinite)
huffman@27468
   482
huffman@27468
   483
lemma STAR_sin_pi_divide_HNatInfinite_approx_pi:
huffman@27468
   484
     "n \<in> HNatInfinite  
lp15@70208
   485
      \<Longrightarrow> ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) * hypreal_of_hypnat n  
wenzelm@61982
   486
          \<approx> hypreal_of_real pi"
huffman@27468
   487
apply (frule STAR_sin_Infinitesimal_divide
huffman@27468
   488
               [OF Infinitesimal_pi_divide_HNatInfinite 
huffman@27468
   489
                   pi_divide_HNatInfinite_not_zero])
huffman@27468
   490
apply (auto)
huffman@27468
   491
apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"])
haftmann@57514
   492
apply (auto intro: Reals_inverse simp add: divide_inverse ac_simps)
huffman@27468
   493
done
huffman@27468
   494
huffman@27468
   495
lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2:
huffman@27468
   496
     "n \<in> HNatInfinite  
lp15@70208
   497
      \<Longrightarrow> hypreal_of_hypnat n *  
huffman@27468
   498
          ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n))  
wenzelm@61982
   499
          \<approx> hypreal_of_real pi"
haftmann@57512
   500
apply (rule mult.commute [THEN subst])
huffman@27468
   501
apply (erule STAR_sin_pi_divide_HNatInfinite_approx_pi)
huffman@27468
   502
done
huffman@27468
   503
huffman@27468
   504
lemma starfunNat_pi_divide_n_Infinitesimal: 
lp15@70208
   505
     "N \<in> HNatInfinite \<Longrightarrow> ( *f* (\<lambda>x. pi / real x)) N \<in> Infinitesimal"
huffman@27468
   506
by (auto intro!: Infinitesimal_HFinite_mult2 
huffman@27468
   507
         simp add: starfun_mult [symmetric] divide_inverse
huffman@27468
   508
                   starfun_inverse [symmetric] starfunNat_real_of_nat)
huffman@27468
   509
huffman@27468
   510
lemma STAR_sin_pi_divide_n_approx:
lp15@70208
   511
     "N \<in> HNatInfinite \<Longrightarrow>  
lp15@70208
   512
      ( *f* sin) (( *f* (\<lambda>x. pi / real x)) N) \<approx>  
huffman@27468
   513
      hypreal_of_real pi/(hypreal_of_hypnat N)"
huffman@27468
   514
apply (simp add: starfunNat_real_of_nat [symmetric])
huffman@27468
   515
apply (rule STAR_sin_Infinitesimal)
huffman@27468
   516
apply (simp add: divide_inverse)
huffman@27468
   517
apply (rule Infinitesimal_HFinite_mult2)
huffman@27468
   518
apply (subst starfun_inverse)
huffman@27468
   519
apply (erule starfunNat_inverse_real_of_nat_Infinitesimal)
huffman@27468
   520
apply simp
huffman@27468
   521
done
huffman@27468
   522
lp15@70208
   523
lemma NSLIMSEQ_sin_pi: "(\<lambda>n. real n * sin (pi / real n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S pi"
huffman@27468
   524
apply (auto simp add: NSLIMSEQ_def starfun_mult [symmetric] starfunNat_real_of_nat)
huffman@27468
   525
apply (rule_tac f1 = sin in starfun_o2 [THEN subst])
huffman@27468
   526
apply (auto simp add: starfun_mult [symmetric] starfunNat_real_of_nat divide_inverse)
huffman@27468
   527
apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
huffman@27468
   528
apply (auto dest: STAR_sin_pi_divide_HNatInfinite_approx_pi 
haftmann@57512
   529
            simp add: starfunNat_real_of_nat mult.commute divide_inverse)
huffman@27468
   530
done
huffman@27468
   531
lp15@70208
   532
lemma NSLIMSEQ_cos_one: "(\<lambda>n. cos (pi / real n))\<longlonglongrightarrow>\<^sub>N\<^sub>S 1"
huffman@27468
   533
apply (simp add: NSLIMSEQ_def, auto)
huffman@27468
   534
apply (rule_tac f1 = cos in starfun_o2 [THEN subst])
huffman@27468
   535
apply (rule STAR_cos_Infinitesimal)
huffman@27468
   536
apply (auto intro!: Infinitesimal_HFinite_mult2 
huffman@27468
   537
            simp add: starfun_mult [symmetric] divide_inverse
huffman@27468
   538
                      starfun_inverse [symmetric] starfunNat_real_of_nat)
huffman@27468
   539
done
huffman@27468
   540
huffman@27468
   541
lemma NSLIMSEQ_sin_cos_pi:
lp15@70208
   542
     "(\<lambda>n. real n * sin (pi / real n) * cos (pi / real n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S pi"
huffman@27468
   543
by (insert NSLIMSEQ_mult [OF NSLIMSEQ_sin_pi NSLIMSEQ_cos_one], simp)
huffman@27468
   544
huffman@27468
   545
wenzelm@69597
   546
text\<open>A familiar approximation to \<^term>\<open>cos x\<close> when \<^term>\<open>x\<close> is small\<close>
huffman@27468
   547
huffman@27468
   548
lemma STAR_cos_Infinitesimal_approx:
lp15@59658
   549
  fixes x :: "'a::{real_normed_field,banach} star"
lp15@70208
   550
  shows "x \<in> Infinitesimal \<Longrightarrow> ( *f* cos) x \<approx> 1 - x\<^sup>2"
huffman@27468
   551
apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
huffman@27468
   552
apply (auto simp add: Infinitesimal_approx_minus [symmetric] 
haftmann@57512
   553
            add.assoc [symmetric] numeral_2_eq_2)
huffman@27468
   554
done
huffman@27468
   555
huffman@27468
   556
lemma STAR_cos_Infinitesimal_approx2:
wenzelm@67443
   557
  fixes x :: hypreal  \<comment> \<open>perhaps could be generalised, like many other hypreal results\<close>
lp15@70208
   558
  shows "x \<in> Infinitesimal \<Longrightarrow> ( *f* cos) x \<approx> 1 - (x\<^sup>2)/2"
huffman@27468
   559
apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
lp15@59658
   560
apply (auto intro: Infinitesimal_SReal_divide Infinitesimal_mult
huffman@27468
   561
            simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2)
huffman@27468
   562
done
huffman@27468
   563
huffman@27468
   564
end