src/HOL/Nonstandard_Analysis/HTranscendental.thy
author paulson <lp15@cam.ac.uk>
Sun Apr 28 16:50:19 2019 +0100 (7 months ago)
changeset 70208 65b3bfc565b5
parent 69597 ff784d5a5bfb
child 70209 ab29bd01b8b2
permissions -rw-r--r--
removal of ASCII connectives; some 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"
huffman@27468
   168
apply (simp add: coshr_def sumhr_split_add
huffman@27468
   169
                   [OF hypnat_one_less_hypnat_omega, symmetric]) 
huffman@27468
   170
apply (rule st_unique, simp)
huffman@27468
   171
apply (rule subst [where P="\<lambda>x. 1 \<approx> x", OF _ approx_refl])
huffman@27468
   172
apply (rule rev_mp [OF hypnat_one_less_hypnat_omega])
huffman@27468
   173
apply (rule_tac x="whn" in spec)
hoelzl@56194
   174
apply (unfold sumhr_app, transfer, simp add: cos_coeff_def power_0_left)
huffman@27468
   175
done
huffman@27468
   176
wenzelm@61982
   177
lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) (0::hypreal) \<approx> 1"
huffman@27468
   178
apply (subgoal_tac "( *f* exp) (0::hypreal) = 1", simp)
huffman@27468
   179
apply (transfer, simp)
huffman@27468
   180
done
huffman@27468
   181
lp15@70208
   182
lemma STAR_exp_Infinitesimal: "x \<in> Infinitesimal \<Longrightarrow> ( *f* exp) (x::hypreal) \<approx> 1"
huffman@27468
   183
apply (case_tac "x = 0")
huffman@27468
   184
apply (cut_tac [2] x = 0 in DERIV_exp)
huffman@27468
   185
apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
huffman@27468
   186
apply (drule_tac x = x in bspec, auto)
huffman@27468
   187
apply (drule_tac c = x in approx_mult1)
huffman@27468
   188
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] 
haftmann@57512
   189
            simp add: mult.assoc)
huffman@27468
   190
apply (rule approx_add_right_cancel [where d="-1"])
huffman@27468
   191
apply (rule approx_sym [THEN [2] approx_trans2])
haftmann@54489
   192
apply (auto simp add: mem_infmal_iff)
huffman@27468
   193
done
huffman@27468
   194
wenzelm@61982
   195
lemma STAR_exp_epsilon [simp]: "( *f* exp) \<epsilon> \<approx> 1"
huffman@27468
   196
by (auto intro: STAR_exp_Infinitesimal)
huffman@27468
   197
immler@58656
   198
lemma STAR_exp_add:
immler@58656
   199
  "!!(x::'a:: {banach,real_normed_field} star) y. ( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y"
huffman@27468
   200
by transfer (rule exp_add)
huffman@27468
   201
huffman@27468
   202
lemma exphr_hypreal_of_real_exp_eq: "exphr x = hypreal_of_real (exp x)"
huffman@27468
   203
apply (simp add: exphr_def)
huffman@27468
   204
apply (rule st_unique, simp)
huffman@27468
   205
apply (subst starfunNat_sumr [symmetric])
hoelzl@56194
   206
unfolding atLeast0LessThan
huffman@27468
   207
apply (rule NSLIMSEQ_D [THEN approx_sym])
huffman@27468
   208
apply (rule LIMSEQ_NSLIMSEQ)
huffman@27468
   209
apply (subst sums_def [symmetric])
huffman@27468
   210
apply (cut_tac exp_converges [where x=x], simp)
huffman@27468
   211
apply (rule HNatInfinite_whn)
huffman@27468
   212
done
huffman@27468
   213
lp15@70208
   214
lemma starfun_exp_ge_add_one_self [simp]: "\<And>x::hypreal. 0 \<le> x \<Longrightarrow> (1 + x) \<le> ( *f* exp) x"
huffman@27468
   215
by transfer (rule exp_ge_add_one_self_aux)
huffman@27468
   216
huffman@27468
   217
(* exp (oo) is infinite *)
huffman@27468
   218
lemma starfun_exp_HInfinite:
lp15@70208
   219
     "\<lbrakk>x \<in> HInfinite; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* exp) (x::hypreal) \<in> HInfinite"
huffman@27468
   220
apply (frule starfun_exp_ge_add_one_self)
huffman@27468
   221
apply (rule HInfinite_ge_HInfinite, assumption)
huffman@27468
   222
apply (rule order_trans [of _ "1+x"], auto) 
huffman@27468
   223
done
huffman@27468
   224
immler@58656
   225
lemma starfun_exp_minus:
lp15@70208
   226
  "\<And>x::'a:: {banach,real_normed_field} star. ( *f* exp) (-x) = inverse(( *f* exp) x)"
huffman@27468
   227
by transfer (rule exp_minus)
huffman@27468
   228
huffman@27468
   229
(* exp (-oo) is infinitesimal *)
huffman@27468
   230
lemma starfun_exp_Infinitesimal:
lp15@70208
   231
     "\<lbrakk>x \<in> HInfinite; x \<le> 0\<rbrakk> \<Longrightarrow> ( *f* exp) (x::hypreal) \<in> Infinitesimal"
huffman@27468
   232
apply (subgoal_tac "\<exists>y. x = - y")
huffman@27468
   233
apply (rule_tac [2] x = "- x" in exI)
huffman@27468
   234
apply (auto intro!: HInfinite_inverse_Infinitesimal starfun_exp_HInfinite
huffman@27468
   235
            simp add: starfun_exp_minus HInfinite_minus_iff)
huffman@27468
   236
done
huffman@27468
   237
lp15@70208
   238
lemma starfun_exp_gt_one [simp]: "\<And>x::hypreal. 0 < x \<Longrightarrow> 1 < ( *f* exp) x"
huffman@27468
   239
by transfer (rule exp_gt_one)
huffman@27468
   240
lp15@60017
   241
abbreviation real_ln :: "real \<Rightarrow> real" where 
lp15@60017
   242
  "real_ln \<equiv> ln"
lp15@60017
   243
lp15@70208
   244
lemma starfun_ln_exp [simp]: "\<And>x. ( *f* real_ln) (( *f* exp) x) = x"
huffman@27468
   245
by transfer (rule ln_exp)
huffman@27468
   246
lp15@70208
   247
lemma starfun_exp_ln_iff [simp]: "\<And>x. (( *f* exp)(( *f* real_ln) x) = x) = (0 < x)"
huffman@27468
   248
by transfer (rule exp_ln_iff)
huffman@27468
   249
lp15@70208
   250
lemma starfun_exp_ln_eq: "!!u x. ( *f* exp) u = x \<Longrightarrow> ( *f* real_ln) x = u"
huffman@44316
   251
by transfer (rule ln_unique)
huffman@27468
   252
lp15@70208
   253
lemma starfun_ln_less_self [simp]: "\<And>x. 0 < x \<Longrightarrow> ( *f* real_ln) x < x"
huffman@27468
   254
by transfer (rule ln_less_self)
huffman@27468
   255
lp15@70208
   256
lemma starfun_ln_ge_zero [simp]: "\<And>x. 1 \<le> x \<Longrightarrow> 0 \<le> ( *f* real_ln) x"
huffman@27468
   257
by transfer (rule ln_ge_zero)
huffman@27468
   258
lp15@70208
   259
lemma starfun_ln_gt_zero [simp]: "\<And>x .1 < x \<Longrightarrow> 0 < ( *f* real_ln) x"
huffman@27468
   260
by transfer (rule ln_gt_zero)
huffman@27468
   261
lp15@70208
   262
lemma starfun_ln_not_eq_zero [simp]: "\<And>x. \<lbrakk>0 < x; x \<noteq> 1\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<noteq> 0"
huffman@27468
   263
by transfer simp
huffman@27468
   264
lp15@70208
   265
lemma starfun_ln_HFinite: "\<lbrakk>x \<in> HFinite; 1 \<le> x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<in> HFinite"
huffman@27468
   266
apply (rule HFinite_bounded)
huffman@27468
   267
apply assumption 
huffman@27468
   268
apply (simp_all add: starfun_ln_less_self order_less_imp_le)
huffman@27468
   269
done
huffman@27468
   270
lp15@70208
   271
lemma starfun_ln_inverse: "\<And>x. 0 < x \<Longrightarrow> ( *f* real_ln) (inverse x) = -( *f* ln) x"
huffman@27468
   272
by transfer (rule ln_inverse)
huffman@27468
   273
huffman@27468
   274
lemma starfun_abs_exp_cancel: "\<And>x. \<bar>( *f* exp) (x::hypreal)\<bar> = ( *f* exp) x"
huffman@27468
   275
by transfer (rule abs_exp_cancel)
huffman@27468
   276
huffman@27468
   277
lemma starfun_exp_less_mono: "\<And>x y::hypreal. x < y \<Longrightarrow> ( *f* exp) x < ( *f* exp) y"
huffman@27468
   278
by transfer (rule exp_less_mono)
huffman@27468
   279
lp15@70208
   280
lemma starfun_exp_HFinite: "x \<in> HFinite \<Longrightarrow> ( *f* exp) (x::hypreal) \<in> HFinite"
huffman@27468
   281
apply (auto simp add: HFinite_def, rename_tac u)
huffman@27468
   282
apply (rule_tac x="( *f* exp) u" in rev_bexI)
huffman@27468
   283
apply (simp add: Reals_eq_Standard)
huffman@27468
   284
apply (simp add: starfun_abs_exp_cancel)
huffman@27468
   285
apply (simp add: starfun_exp_less_mono)
huffman@27468
   286
done
huffman@27468
   287
huffman@27468
   288
lemma starfun_exp_add_HFinite_Infinitesimal_approx:
lp15@70208
   289
     "\<lbrakk>x \<in> Infinitesimal; z \<in> HFinite\<rbrakk> \<Longrightarrow> ( *f* exp) (z + x::hypreal) \<approx> ( *f* exp) z"
huffman@27468
   290
apply (simp add: STAR_exp_add)
huffman@27468
   291
apply (frule STAR_exp_Infinitesimal)
huffman@27468
   292
apply (drule approx_mult2)
huffman@27468
   293
apply (auto intro: starfun_exp_HFinite)
huffman@27468
   294
done
huffman@27468
   295
huffman@27468
   296
(* using previous result to get to result *)
huffman@27468
   297
lemma starfun_ln_HInfinite:
lp15@70208
   298
     "\<lbrakk>x \<in> HInfinite; 0 < x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<in> HInfinite"
huffman@27468
   299
apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
huffman@27468
   300
apply (drule starfun_exp_HFinite)
huffman@27468
   301
apply (simp add: starfun_exp_ln_iff [THEN iffD2] HFinite_HInfinite_iff)
huffman@27468
   302
done
huffman@27468
   303
huffman@27468
   304
lemma starfun_exp_HInfinite_Infinitesimal_disj:
wenzelm@67091
   305
 "x \<in> HInfinite \<Longrightarrow> ( *f* exp) x \<in> HInfinite \<or> ( *f* exp) (x::hypreal) \<in> Infinitesimal"
huffman@27468
   306
apply (insert linorder_linear [of x 0]) 
huffman@27468
   307
apply (auto intro: starfun_exp_HInfinite starfun_exp_Infinitesimal)
huffman@27468
   308
done
huffman@27468
   309
huffman@27468
   310
(* check out this proof!!! *)
huffman@27468
   311
lemma starfun_ln_HFinite_not_Infinitesimal:
lp15@70208
   312
     "\<lbrakk>x \<in> HFinite - Infinitesimal; 0 < x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<in> HFinite"
huffman@27468
   313
apply (rule ccontr, drule HInfinite_HFinite_iff [THEN iffD2])
huffman@27468
   314
apply (drule starfun_exp_HInfinite_Infinitesimal_disj)
huffman@27468
   315
apply (simp add: starfun_exp_ln_iff [symmetric] HInfinite_HFinite_iff
huffman@27468
   316
            del: starfun_exp_ln_iff)
huffman@27468
   317
done
huffman@27468
   318
huffman@27468
   319
(* we do proof by considering ln of 1/x *)
huffman@27468
   320
lemma starfun_ln_Infinitesimal_HInfinite:
lp15@70208
   321
     "\<lbrakk>x \<in> Infinitesimal; 0 < x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<in> HInfinite"
huffman@27468
   322
apply (drule Infinitesimal_inverse_HInfinite)
huffman@27468
   323
apply (frule positive_imp_inverse_positive)
huffman@27468
   324
apply (drule_tac [2] starfun_ln_HInfinite)
huffman@27468
   325
apply (auto simp add: starfun_ln_inverse HInfinite_minus_iff)
huffman@27468
   326
done
huffman@27468
   327
lp15@70208
   328
lemma starfun_ln_less_zero: "\<And>x. \<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> ( *f* real_ln) x < 0"
huffman@27468
   329
by transfer (rule ln_less_zero)
huffman@27468
   330
huffman@27468
   331
lemma starfun_ln_Infinitesimal_less_zero:
lp15@70208
   332
     "\<lbrakk>x \<in> Infinitesimal; 0 < x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x < 0"
huffman@27468
   333
by (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def)
huffman@27468
   334
huffman@27468
   335
lemma starfun_ln_HInfinite_gt_zero:
lp15@70208
   336
     "\<lbrakk>x \<in> HInfinite; 0 < x\<rbrakk> \<Longrightarrow> 0 < ( *f* real_ln) x"
huffman@27468
   337
by (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def)
huffman@27468
   338
huffman@27468
   339
huffman@27468
   340
(*
lp15@70208
   341
Goalw [NSLIM_def] "(\<lambda>h. ((x powr h) - 1) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S ln x"
huffman@27468
   342
*)
huffman@27468
   343
lp15@70208
   344
lemma HFinite_sin [simp]: "sumhr (0, whn, \<lambda>n. sin_coeff n * x ^ n) \<in> HFinite"
huffman@27468
   345
unfolding sumhr_app
hoelzl@56194
   346
apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
huffman@27468
   347
apply (rule NSBseqD2)
huffman@27468
   348
apply (rule NSconvergent_NSBseq)
huffman@27468
   349
apply (rule convergent_NSconvergent_iff [THEN iffD1])
hoelzl@56194
   350
apply (rule summable_iff_convergent [THEN iffD1])
lp15@59658
   351
using summable_norm_sin [of x]
lp15@59658
   352
apply (simp add: summable_rabs_cancel)
huffman@27468
   353
done
huffman@27468
   354
huffman@27468
   355
lemma STAR_sin_zero [simp]: "( *f* sin) 0 = 0"
huffman@27468
   356
by transfer (rule sin_zero)
huffman@27468
   357
lp15@59658
   358
lemma STAR_sin_Infinitesimal [simp]:
lp15@59658
   359
  fixes x :: "'a::{real_normed_field,banach} star"
lp15@70208
   360
  shows "x \<in> Infinitesimal \<Longrightarrow> ( *f* sin) x \<approx> x"
huffman@27468
   361
apply (case_tac "x = 0")
huffman@27468
   362
apply (cut_tac [2] x = 0 in DERIV_sin)
huffman@27468
   363
apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
huffman@27468
   364
apply (drule bspec [where x = x], auto)
huffman@27468
   365
apply (drule approx_mult1 [where c = x])
huffman@27468
   366
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
haftmann@57512
   367
           simp add: mult.assoc)
huffman@27468
   368
done
huffman@27468
   369
lp15@70208
   370
lemma HFinite_cos [simp]: "sumhr (0, whn, \<lambda>n. cos_coeff n * x ^ n) \<in> HFinite"
huffman@27468
   371
unfolding sumhr_app
hoelzl@56194
   372
apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
huffman@27468
   373
apply (rule NSBseqD2)
huffman@27468
   374
apply (rule NSconvergent_NSBseq)
huffman@27468
   375
apply (rule convergent_NSconvergent_iff [THEN iffD1])
hoelzl@56194
   376
apply (rule summable_iff_convergent [THEN iffD1])
lp15@59658
   377
using summable_norm_cos [of x]
lp15@59658
   378
apply (simp add: summable_rabs_cancel)
huffman@27468
   379
done
huffman@27468
   380
huffman@27468
   381
lemma STAR_cos_zero [simp]: "( *f* cos) 0 = 1"
huffman@27468
   382
by transfer (rule cos_zero)
huffman@27468
   383
lp15@59658
   384
lemma STAR_cos_Infinitesimal [simp]:
lp15@59658
   385
  fixes x :: "'a::{real_normed_field,banach} star"
lp15@70208
   386
  shows "x \<in> Infinitesimal \<Longrightarrow> ( *f* cos) x \<approx> 1"
huffman@27468
   387
apply (case_tac "x = 0")
huffman@27468
   388
apply (cut_tac [2] x = 0 in DERIV_cos)
huffman@27468
   389
apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
huffman@27468
   390
apply (drule bspec [where x = x])
huffman@27468
   391
apply auto
huffman@27468
   392
apply (drule approx_mult1 [where c = x])
huffman@27468
   393
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
haftmann@57512
   394
            simp add: mult.assoc)
huffman@27468
   395
apply (rule approx_add_right_cancel [where d = "-1"])
haftmann@54489
   396
apply simp
huffman@27468
   397
done
huffman@27468
   398
huffman@27468
   399
lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
huffman@27468
   400
by transfer (rule tan_zero)
huffman@27468
   401
lp15@70208
   402
lemma STAR_tan_Infinitesimal: "x \<in> Infinitesimal \<Longrightarrow> ( *f* tan) x \<approx> x"
huffman@27468
   403
apply (case_tac "x = 0")
huffman@27468
   404
apply (cut_tac [2] x = 0 in DERIV_tan)
huffman@27468
   405
apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
huffman@27468
   406
apply (drule bspec [where x = x], auto)
huffman@27468
   407
apply (drule approx_mult1 [where c = x])
huffman@27468
   408
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
haftmann@57512
   409
             simp add: mult.assoc)
huffman@27468
   410
done
huffman@27468
   411
huffman@27468
   412
lemma STAR_sin_cos_Infinitesimal_mult:
lp15@59658
   413
  fixes x :: "'a::{real_normed_field,banach} star"
lp15@70208
   414
  shows "x \<in> Infinitesimal \<Longrightarrow> ( *f* sin) x * ( *f* cos) x \<approx> x"
lp15@59658
   415
using approx_mult_HFinite [of "( *f* sin) x" _ "( *f* cos) x" 1] 
lp15@59658
   416
by (simp add: Infinitesimal_subset_HFinite [THEN subsetD])
huffman@27468
   417
huffman@27468
   418
lemma HFinite_pi: "hypreal_of_real pi \<in> HFinite"
huffman@27468
   419
by simp
huffman@27468
   420
huffman@27468
   421
(* lemmas *)
huffman@27468
   422
huffman@27468
   423
lemma lemma_split_hypreal_of_real:
huffman@27468
   424
     "N \<in> HNatInfinite  
lp15@70208
   425
      \<Longrightarrow> hypreal_of_real a =  
huffman@27468
   426
          hypreal_of_hypnat N * (inverse(hypreal_of_hypnat N) * hypreal_of_real a)"
haftmann@57512
   427
by (simp add: mult.assoc [symmetric] zero_less_HNatInfinite)
huffman@27468
   428
huffman@27468
   429
lemma STAR_sin_Infinitesimal_divide:
lp15@59658
   430
  fixes x :: "'a::{real_normed_field,banach} star"
lp15@70208
   431
  shows "\<lbrakk>x \<in> Infinitesimal; x \<noteq> 0\<rbrakk> \<Longrightarrow> ( *f* sin) x/x \<approx> 1"
lp15@59658
   432
using DERIV_sin [of "0::'a"]
lp15@59658
   433
by (simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
huffman@27468
   434
huffman@27468
   435
(*------------------------------------------------------------------------*) 
wenzelm@61982
   436
(* sin* (1/n) * 1/(1/n) \<approx> 1 for n = oo                                   *)
huffman@27468
   437
(*------------------------------------------------------------------------*)
huffman@27468
   438
huffman@27468
   439
lemma lemma_sin_pi:
huffman@27468
   440
     "n \<in> HNatInfinite  
lp15@70208
   441
      \<Longrightarrow> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) \<approx> 1"
huffman@27468
   442
apply (rule STAR_sin_Infinitesimal_divide)
huffman@27468
   443
apply (auto simp add: zero_less_HNatInfinite)
huffman@27468
   444
done
huffman@27468
   445
huffman@27468
   446
lemma STAR_sin_inverse_HNatInfinite:
huffman@27468
   447
     "n \<in> HNatInfinite  
lp15@70208
   448
      \<Longrightarrow> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n \<approx> 1"
huffman@27468
   449
apply (frule lemma_sin_pi)
huffman@27468
   450
apply (simp add: divide_inverse)
huffman@27468
   451
done
huffman@27468
   452
huffman@27468
   453
lemma Infinitesimal_pi_divide_HNatInfinite: 
huffman@27468
   454
     "N \<in> HNatInfinite  
lp15@70208
   455
      \<Longrightarrow> hypreal_of_real pi/(hypreal_of_hypnat N) \<in> Infinitesimal"
huffman@27468
   456
apply (simp add: divide_inverse)
huffman@27468
   457
apply (auto intro: Infinitesimal_HFinite_mult2)
huffman@27468
   458
done
huffman@27468
   459
huffman@27468
   460
lemma pi_divide_HNatInfinite_not_zero [simp]:
lp15@70208
   461
     "N \<in> HNatInfinite \<Longrightarrow> hypreal_of_real pi/(hypreal_of_hypnat N) \<noteq> 0"
huffman@27468
   462
by (simp add: zero_less_HNatInfinite)
huffman@27468
   463
huffman@27468
   464
lemma STAR_sin_pi_divide_HNatInfinite_approx_pi:
huffman@27468
   465
     "n \<in> HNatInfinite  
lp15@70208
   466
      \<Longrightarrow> ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) * hypreal_of_hypnat n  
wenzelm@61982
   467
          \<approx> hypreal_of_real pi"
huffman@27468
   468
apply (frule STAR_sin_Infinitesimal_divide
huffman@27468
   469
               [OF Infinitesimal_pi_divide_HNatInfinite 
huffman@27468
   470
                   pi_divide_HNatInfinite_not_zero])
huffman@27468
   471
apply (auto)
huffman@27468
   472
apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"])
haftmann@57514
   473
apply (auto intro: Reals_inverse simp add: divide_inverse ac_simps)
huffman@27468
   474
done
huffman@27468
   475
huffman@27468
   476
lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2:
huffman@27468
   477
     "n \<in> HNatInfinite  
lp15@70208
   478
      \<Longrightarrow> hypreal_of_hypnat n *  
huffman@27468
   479
          ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n))  
wenzelm@61982
   480
          \<approx> hypreal_of_real pi"
haftmann@57512
   481
apply (rule mult.commute [THEN subst])
huffman@27468
   482
apply (erule STAR_sin_pi_divide_HNatInfinite_approx_pi)
huffman@27468
   483
done
huffman@27468
   484
huffman@27468
   485
lemma starfunNat_pi_divide_n_Infinitesimal: 
lp15@70208
   486
     "N \<in> HNatInfinite \<Longrightarrow> ( *f* (\<lambda>x. pi / real x)) N \<in> Infinitesimal"
huffman@27468
   487
by (auto intro!: Infinitesimal_HFinite_mult2 
huffman@27468
   488
         simp add: starfun_mult [symmetric] divide_inverse
huffman@27468
   489
                   starfun_inverse [symmetric] starfunNat_real_of_nat)
huffman@27468
   490
huffman@27468
   491
lemma STAR_sin_pi_divide_n_approx:
lp15@70208
   492
     "N \<in> HNatInfinite \<Longrightarrow>  
lp15@70208
   493
      ( *f* sin) (( *f* (\<lambda>x. pi / real x)) N) \<approx>  
huffman@27468
   494
      hypreal_of_real pi/(hypreal_of_hypnat N)"
huffman@27468
   495
apply (simp add: starfunNat_real_of_nat [symmetric])
huffman@27468
   496
apply (rule STAR_sin_Infinitesimal)
huffman@27468
   497
apply (simp add: divide_inverse)
huffman@27468
   498
apply (rule Infinitesimal_HFinite_mult2)
huffman@27468
   499
apply (subst starfun_inverse)
huffman@27468
   500
apply (erule starfunNat_inverse_real_of_nat_Infinitesimal)
huffman@27468
   501
apply simp
huffman@27468
   502
done
huffman@27468
   503
lp15@70208
   504
lemma NSLIMSEQ_sin_pi: "(\<lambda>n. real n * sin (pi / real n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S pi"
huffman@27468
   505
apply (auto simp add: NSLIMSEQ_def starfun_mult [symmetric] starfunNat_real_of_nat)
huffman@27468
   506
apply (rule_tac f1 = sin in starfun_o2 [THEN subst])
huffman@27468
   507
apply (auto simp add: starfun_mult [symmetric] starfunNat_real_of_nat divide_inverse)
huffman@27468
   508
apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
huffman@27468
   509
apply (auto dest: STAR_sin_pi_divide_HNatInfinite_approx_pi 
haftmann@57512
   510
            simp add: starfunNat_real_of_nat mult.commute divide_inverse)
huffman@27468
   511
done
huffman@27468
   512
lp15@70208
   513
lemma NSLIMSEQ_cos_one: "(\<lambda>n. cos (pi / real n))\<longlonglongrightarrow>\<^sub>N\<^sub>S 1"
huffman@27468
   514
apply (simp add: NSLIMSEQ_def, auto)
huffman@27468
   515
apply (rule_tac f1 = cos in starfun_o2 [THEN subst])
huffman@27468
   516
apply (rule STAR_cos_Infinitesimal)
huffman@27468
   517
apply (auto intro!: Infinitesimal_HFinite_mult2 
huffman@27468
   518
            simp add: starfun_mult [symmetric] divide_inverse
huffman@27468
   519
                      starfun_inverse [symmetric] starfunNat_real_of_nat)
huffman@27468
   520
done
huffman@27468
   521
huffman@27468
   522
lemma NSLIMSEQ_sin_cos_pi:
lp15@70208
   523
     "(\<lambda>n. real n * sin (pi / real n) * cos (pi / real n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S pi"
huffman@27468
   524
by (insert NSLIMSEQ_mult [OF NSLIMSEQ_sin_pi NSLIMSEQ_cos_one], simp)
huffman@27468
   525
huffman@27468
   526
wenzelm@69597
   527
text\<open>A familiar approximation to \<^term>\<open>cos x\<close> when \<^term>\<open>x\<close> is small\<close>
huffman@27468
   528
huffman@27468
   529
lemma STAR_cos_Infinitesimal_approx:
lp15@59658
   530
  fixes x :: "'a::{real_normed_field,banach} star"
lp15@70208
   531
  shows "x \<in> Infinitesimal \<Longrightarrow> ( *f* cos) x \<approx> 1 - x\<^sup>2"
huffman@27468
   532
apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
huffman@27468
   533
apply (auto simp add: Infinitesimal_approx_minus [symmetric] 
haftmann@57512
   534
            add.assoc [symmetric] numeral_2_eq_2)
huffman@27468
   535
done
huffman@27468
   536
huffman@27468
   537
lemma STAR_cos_Infinitesimal_approx2:
wenzelm@67443
   538
  fixes x :: hypreal  \<comment> \<open>perhaps could be generalised, like many other hypreal results\<close>
lp15@70208
   539
  shows "x \<in> Infinitesimal \<Longrightarrow> ( *f* cos) x \<approx> 1 - (x\<^sup>2)/2"
huffman@27468
   540
apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
lp15@59658
   541
apply (auto intro: Infinitesimal_SReal_divide Infinitesimal_mult
huffman@27468
   542
            simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2)
huffman@27468
   543
done
huffman@27468
   544
huffman@27468
   545
end