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