src/HOL/Hyperreal/HTranscendental.thy
author nipkow
Mon Aug 16 14:22:27 2004 +0200 (2004-08-16)
changeset 15131 c69542757a4d
parent 15077 89840837108e
child 15140 322485b816ac
permissions -rw-r--r--
New theory header syntax.
paulson@13958
     1
(*  Title       : HTranscendental.thy
paulson@13958
     2
    Author      : Jacques D. Fleuriot
paulson@13958
     3
    Copyright   : 2001 University of Edinburgh
paulson@14420
     4
paulson@14420
     5
Converted to Isar and polished by lcp
paulson@13958
     6
*)
paulson@13958
     7
paulson@14420
     8
header{*Nonstandard Extensions of Transcendental Functions*}
paulson@14420
     9
nipkow@15131
    10
theory HTranscendental
nipkow@15131
    11
import Transcendental Integration
nipkow@15131
    12
begin
paulson@13958
    13
paulson@15013
    14
text{*really belongs in Transcendental*}
paulson@15013
    15
lemma sqrt_divide_self_eq:
paulson@15013
    16
  assumes nneg: "0 \<le> x"
paulson@15013
    17
  shows "sqrt x / x = inverse (sqrt x)"
paulson@15013
    18
proof cases
paulson@15013
    19
  assume "x=0" thus ?thesis by simp
paulson@15013
    20
next
paulson@15013
    21
  assume nz: "x\<noteq>0" 
paulson@15013
    22
  hence pos: "0<x" using nneg by arith
paulson@15013
    23
  show ?thesis
paulson@15013
    24
  proof (rule right_inverse_eq [THEN iffD1, THEN sym]) 
paulson@15013
    25
    show "sqrt x / x \<noteq> 0" by (simp add: divide_inverse nneg nz) 
paulson@15013
    26
    show "inverse (sqrt x) / (sqrt x / x) = 1"
paulson@15013
    27
      by (simp add: divide_inverse mult_assoc [symmetric] 
paulson@15013
    28
                  power2_eq_square [symmetric] real_inv_sqrt_pow2 pos nz) 
paulson@15013
    29
  qed
paulson@15013
    30
qed
paulson@15013
    31
paulson@15013
    32
paulson@13958
    33
constdefs
paulson@13958
    34
paulson@14420
    35
  exphr :: "real => hypreal"
paulson@14420
    36
    --{*define exponential function using standard part *}
paulson@13958
    37
    "exphr x ==  st(sumhr (0, whn, %n. inverse(real (fact n)) * (x ^ n)))" 
paulson@13958
    38
paulson@14420
    39
  sinhr :: "real => hypreal"
paulson@13958
    40
    "sinhr x == st(sumhr (0, whn, %n. (if even(n) then 0 else
paulson@13958
    41
             ((-1) ^ ((n - 1) div 2))/(real (fact n))) * (x ^ n)))"
paulson@13958
    42
  
paulson@14420
    43
  coshr :: "real => hypreal"
paulson@13958
    44
    "coshr x == st(sumhr (0, whn, %n. (if even(n) then
paulson@13958
    45
            ((-1) ^ (n div 2))/(real (fact n)) else 0) * x ^ n))"
paulson@14420
    46
paulson@14420
    47
paulson@14420
    48
subsection{*Nonstandard Extension of Square Root Function*}
paulson@14420
    49
paulson@14420
    50
lemma STAR_sqrt_zero [simp]: "( *f* sqrt) 0 = 0"
paulson@14420
    51
by (simp add: starfun hypreal_zero_num)
paulson@14420
    52
paulson@14420
    53
lemma STAR_sqrt_one [simp]: "( *f* sqrt) 1 = 1"
paulson@14420
    54
by (simp add: starfun hypreal_one_num)
paulson@14420
    55
paulson@14420
    56
lemma hypreal_sqrt_pow2_iff: "(( *f* sqrt)(x) ^ 2 = x) = (0 \<le> x)"
paulson@14468
    57
apply (cases x)
paulson@14420
    58
apply (auto simp add: hypreal_le hypreal_zero_num starfun hrealpow 
paulson@14420
    59
                      real_sqrt_pow2_iff 
paulson@14420
    60
            simp del: hpowr_Suc realpow_Suc)
paulson@14420
    61
done
paulson@14420
    62
paulson@14420
    63
lemma hypreal_sqrt_gt_zero_pow2: "0 < x ==> ( *f* sqrt) (x) ^ 2 = x"
paulson@14468
    64
apply (cases x)
paulson@15077
    65
apply (auto intro: FreeUltrafilterNat_subset 
paulson@14420
    66
            simp add: hypreal_less starfun hrealpow hypreal_zero_num 
paulson@14420
    67
            simp del: hpowr_Suc realpow_Suc)
paulson@14420
    68
done
paulson@14420
    69
paulson@14420
    70
lemma hypreal_sqrt_pow2_gt_zero: "0 < x ==> 0 < ( *f* sqrt) (x) ^ 2"
paulson@14420
    71
by (frule hypreal_sqrt_gt_zero_pow2, auto)
paulson@14420
    72
paulson@14420
    73
lemma hypreal_sqrt_not_zero: "0 < x ==> ( *f* sqrt) (x) \<noteq> 0"
paulson@14420
    74
apply (frule hypreal_sqrt_pow2_gt_zero)
paulson@14420
    75
apply (auto simp add: numeral_2_eq_2)
paulson@14420
    76
done
paulson@14420
    77
paulson@14420
    78
lemma hypreal_inverse_sqrt_pow2:
paulson@14420
    79
     "0 < x ==> inverse (( *f* sqrt)(x)) ^ 2 = inverse x"
paulson@14420
    80
apply (cut_tac n1 = 2 and a1 = "( *f* sqrt) x" in power_inverse [symmetric])
paulson@14420
    81
apply (auto dest: hypreal_sqrt_gt_zero_pow2)
paulson@14420
    82
done
paulson@14420
    83
paulson@14420
    84
lemma hypreal_sqrt_mult_distrib: 
paulson@14420
    85
    "[|0 < x; 0 <y |] ==> ( *f* sqrt)(x*y) =  ( *f* sqrt)(x) * ( *f* sqrt)(y)"
paulson@14468
    86
apply (cases x, cases y)
paulson@14420
    87
apply (simp add: hypreal_zero_def starfun hypreal_mult hypreal_less hypreal_zero_num, ultra)
paulson@14420
    88
apply (auto intro: real_sqrt_mult_distrib) 
paulson@14420
    89
done
paulson@14420
    90
paulson@14420
    91
lemma hypreal_sqrt_mult_distrib2:
paulson@14420
    92
     "[|0\<le>x; 0\<le>y |] ==>  
paulson@14420
    93
     ( *f* sqrt)(x*y) =  ( *f* sqrt)(x) * ( *f* sqrt)(y)"
paulson@14420
    94
by (auto intro: hypreal_sqrt_mult_distrib simp add: order_le_less)
paulson@14420
    95
paulson@14420
    96
lemma hypreal_sqrt_approx_zero [simp]:
paulson@14420
    97
     "0 < x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)"
paulson@14420
    98
apply (auto simp add: mem_infmal_iff [symmetric])
paulson@14420
    99
apply (rule hypreal_sqrt_gt_zero_pow2 [THEN subst])
paulson@14420
   100
apply (auto intro: Infinitesimal_mult 
paulson@14420
   101
            dest!: hypreal_sqrt_gt_zero_pow2 [THEN ssubst] 
paulson@14420
   102
            simp add: numeral_2_eq_2)
paulson@14420
   103
done
paulson@14420
   104
paulson@14420
   105
lemma hypreal_sqrt_approx_zero2 [simp]:
paulson@14420
   106
     "0 \<le> x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)"
paulson@14420
   107
by (auto simp add: order_le_less)
paulson@14420
   108
paulson@14420
   109
lemma hypreal_sqrt_sum_squares [simp]:
paulson@14420
   110
     "(( *f* sqrt)(x*x + y*y + z*z) @= 0) = (x*x + y*y + z*z @= 0)"
paulson@14420
   111
apply (rule hypreal_sqrt_approx_zero2)
paulson@14420
   112
apply (rule hypreal_le_add_order)+
paulson@14420
   113
apply (auto simp add: zero_le_square)
paulson@14420
   114
done
paulson@14420
   115
paulson@14420
   116
lemma hypreal_sqrt_sum_squares2 [simp]:
paulson@14420
   117
     "(( *f* sqrt)(x*x + y*y) @= 0) = (x*x + y*y @= 0)"
paulson@14420
   118
apply (rule hypreal_sqrt_approx_zero2)
paulson@14420
   119
apply (rule hypreal_le_add_order)
paulson@14420
   120
apply (auto simp add: zero_le_square)
paulson@14420
   121
done
paulson@14420
   122
paulson@14420
   123
lemma hypreal_sqrt_gt_zero: "0 < x ==> 0 < ( *f* sqrt)(x)"
paulson@14468
   124
apply (cases x)
paulson@14420
   125
apply (auto simp add: starfun hypreal_zero_def hypreal_less hypreal_zero_num, ultra)
paulson@14420
   126
apply (auto intro: real_sqrt_gt_zero)
paulson@14420
   127
done
paulson@14420
   128
paulson@14420
   129
lemma hypreal_sqrt_ge_zero: "0 \<le> x ==> 0 \<le> ( *f* sqrt)(x)"
paulson@14420
   130
by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less)
paulson@14420
   131
paulson@14420
   132
lemma hypreal_sqrt_hrabs [simp]: "( *f* sqrt)(x ^ 2) = abs(x)"
paulson@14468
   133
apply (cases x)
paulson@14420
   134
apply (simp add: starfun hypreal_hrabs hypreal_mult numeral_2_eq_2)
paulson@14420
   135
done
paulson@14420
   136
paulson@14420
   137
lemma hypreal_sqrt_hrabs2 [simp]: "( *f* sqrt)(x*x) = abs(x)"
paulson@14420
   138
apply (rule hrealpow_two [THEN subst])
paulson@14420
   139
apply (rule numeral_2_eq_2 [THEN subst])
paulson@14420
   140
apply (rule hypreal_sqrt_hrabs)
paulson@14420
   141
done
paulson@14420
   142
paulson@14420
   143
lemma hypreal_sqrt_hyperpow_hrabs [simp]:
paulson@14420
   144
     "( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)"
paulson@14468
   145
apply (cases x)
paulson@14420
   146
apply (simp add: starfun hypreal_hrabs hypnat_of_nat_eq hyperpow)
paulson@14420
   147
done
paulson@14420
   148
paulson@14420
   149
lemma star_sqrt_HFinite: "\<lbrakk>x \<in> HFinite; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> HFinite"
paulson@14420
   150
apply (rule HFinite_square_iff [THEN iffD1])
paulson@14420
   151
apply (simp only: hypreal_sqrt_mult_distrib2 [symmetric], simp) 
paulson@14420
   152
done
paulson@14420
   153
paulson@14420
   154
lemma st_hypreal_sqrt:
paulson@14420
   155
     "[| x \<in> HFinite; 0 \<le> x |] ==> st(( *f* sqrt) x) = ( *f* sqrt)(st x)"
paulson@14420
   156
apply (rule power_inject_base [where n=1])
paulson@14420
   157
apply (auto intro!: st_zero_le hypreal_sqrt_ge_zero)
paulson@14420
   158
apply (rule st_mult [THEN subst])
paulson@14420
   159
apply (rule_tac [3] hypreal_sqrt_mult_distrib2 [THEN subst])
paulson@14420
   160
apply (rule_tac [5] hypreal_sqrt_mult_distrib2 [THEN subst])
paulson@14420
   161
apply (auto simp add: st_hrabs st_zero_le star_sqrt_HFinite)
paulson@14420
   162
done
paulson@14420
   163
paulson@14420
   164
lemma hypreal_sqrt_sum_squares_ge1 [simp]: "x \<le> ( *f* sqrt)(x ^ 2 + y ^ 2)"
paulson@14468
   165
apply (cases x, cases y)
paulson@14420
   166
apply (simp add: starfun hypreal_add hrealpow hypreal_le 
paulson@14420
   167
            del: hpowr_Suc realpow_Suc)
paulson@14420
   168
done
paulson@14420
   169
paulson@14420
   170
lemma HFinite_hypreal_sqrt:
paulson@14420
   171
     "[| 0 \<le> x; x \<in> HFinite |] ==> ( *f* sqrt) x \<in> HFinite"
paulson@14420
   172
apply (auto simp add: order_le_less)
paulson@14420
   173
apply (rule HFinite_square_iff [THEN iffD1])
paulson@14420
   174
apply (drule hypreal_sqrt_gt_zero_pow2)
paulson@14420
   175
apply (simp add: numeral_2_eq_2)
paulson@14420
   176
done
paulson@14420
   177
paulson@14420
   178
lemma HFinite_hypreal_sqrt_imp_HFinite:
paulson@14420
   179
     "[| 0 \<le> x; ( *f* sqrt) x \<in> HFinite |] ==> x \<in> HFinite"
paulson@14420
   180
apply (auto simp add: order_le_less)
paulson@14420
   181
apply (drule HFinite_square_iff [THEN iffD2])
paulson@14420
   182
apply (drule hypreal_sqrt_gt_zero_pow2)
paulson@14420
   183
apply (simp add: numeral_2_eq_2 del: HFinite_square_iff)
paulson@14420
   184
done
paulson@14420
   185
paulson@14420
   186
lemma HFinite_hypreal_sqrt_iff [simp]:
paulson@14420
   187
     "0 \<le> x ==> (( *f* sqrt) x \<in> HFinite) = (x \<in> HFinite)"
paulson@14420
   188
by (blast intro: HFinite_hypreal_sqrt HFinite_hypreal_sqrt_imp_HFinite)
paulson@14420
   189
paulson@14420
   190
lemma HFinite_sqrt_sum_squares [simp]:
paulson@14420
   191
     "(( *f* sqrt)(x*x + y*y) \<in> HFinite) = (x*x + y*y \<in> HFinite)"
paulson@14420
   192
apply (rule HFinite_hypreal_sqrt_iff)
paulson@14420
   193
apply (rule hypreal_le_add_order)
paulson@14420
   194
apply (auto simp add: zero_le_square)
paulson@14420
   195
done
paulson@14420
   196
paulson@14420
   197
lemma Infinitesimal_hypreal_sqrt:
paulson@14420
   198
     "[| 0 \<le> x; x \<in> Infinitesimal |] ==> ( *f* sqrt) x \<in> Infinitesimal"
paulson@14420
   199
apply (auto simp add: order_le_less)
paulson@14420
   200
apply (rule Infinitesimal_square_iff [THEN iffD2])
paulson@14420
   201
apply (drule hypreal_sqrt_gt_zero_pow2)
paulson@14420
   202
apply (simp add: numeral_2_eq_2)
paulson@14420
   203
done
paulson@14420
   204
paulson@14420
   205
lemma Infinitesimal_hypreal_sqrt_imp_Infinitesimal:
paulson@14420
   206
     "[| 0 \<le> x; ( *f* sqrt) x \<in> Infinitesimal |] ==> x \<in> Infinitesimal"
paulson@14420
   207
apply (auto simp add: order_le_less)
paulson@14420
   208
apply (drule Infinitesimal_square_iff [THEN iffD1])
paulson@14420
   209
apply (drule hypreal_sqrt_gt_zero_pow2)
paulson@14420
   210
apply (simp add: numeral_2_eq_2 del: Infinitesimal_square_iff [symmetric])
paulson@14420
   211
done
paulson@14420
   212
paulson@14420
   213
lemma Infinitesimal_hypreal_sqrt_iff [simp]:
paulson@14420
   214
     "0 \<le> x ==> (( *f* sqrt) x \<in> Infinitesimal) = (x \<in> Infinitesimal)"
paulson@14420
   215
by (blast intro: Infinitesimal_hypreal_sqrt_imp_Infinitesimal Infinitesimal_hypreal_sqrt)
paulson@14420
   216
paulson@14420
   217
lemma Infinitesimal_sqrt_sum_squares [simp]:
paulson@14420
   218
     "(( *f* sqrt)(x*x + y*y) \<in> Infinitesimal) = (x*x + y*y \<in> Infinitesimal)"
paulson@14420
   219
apply (rule Infinitesimal_hypreal_sqrt_iff)
paulson@14420
   220
apply (rule hypreal_le_add_order)
paulson@14420
   221
apply (auto simp add: zero_le_square)
paulson@14420
   222
done
paulson@14420
   223
paulson@14420
   224
lemma HInfinite_hypreal_sqrt:
paulson@14420
   225
     "[| 0 \<le> x; x \<in> HInfinite |] ==> ( *f* sqrt) x \<in> HInfinite"
paulson@14420
   226
apply (auto simp add: order_le_less)
paulson@14420
   227
apply (rule HInfinite_square_iff [THEN iffD1])
paulson@14420
   228
apply (drule hypreal_sqrt_gt_zero_pow2)
paulson@14420
   229
apply (simp add: numeral_2_eq_2)
paulson@14420
   230
done
paulson@14420
   231
paulson@14420
   232
lemma HInfinite_hypreal_sqrt_imp_HInfinite:
paulson@14420
   233
     "[| 0 \<le> x; ( *f* sqrt) x \<in> HInfinite |] ==> x \<in> HInfinite"
paulson@14420
   234
apply (auto simp add: order_le_less)
paulson@14420
   235
apply (drule HInfinite_square_iff [THEN iffD2])
paulson@14420
   236
apply (drule hypreal_sqrt_gt_zero_pow2)
paulson@14420
   237
apply (simp add: numeral_2_eq_2 del: HInfinite_square_iff)
paulson@14420
   238
done
paulson@14420
   239
paulson@14420
   240
lemma HInfinite_hypreal_sqrt_iff [simp]:
paulson@14420
   241
     "0 \<le> x ==> (( *f* sqrt) x \<in> HInfinite) = (x \<in> HInfinite)"
paulson@14420
   242
by (blast intro: HInfinite_hypreal_sqrt HInfinite_hypreal_sqrt_imp_HInfinite)
paulson@14420
   243
paulson@14420
   244
lemma HInfinite_sqrt_sum_squares [simp]:
paulson@14420
   245
     "(( *f* sqrt)(x*x + y*y) \<in> HInfinite) = (x*x + y*y \<in> HInfinite)"
paulson@14420
   246
apply (rule HInfinite_hypreal_sqrt_iff)
paulson@14420
   247
apply (rule hypreal_le_add_order)
paulson@14420
   248
apply (auto simp add: zero_le_square)
paulson@14420
   249
done
paulson@14420
   250
paulson@14420
   251
lemma HFinite_exp [simp]:
paulson@14420
   252
     "sumhr (0, whn, %n. inverse (real (fact n)) * x ^ n) \<in> HFinite"
paulson@14420
   253
by (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq 
paulson@14420
   254
         simp add: starfunNat_sumr [symmetric] starfunNat hypnat_omega_def
paulson@14420
   255
                   convergent_NSconvergent_iff [symmetric] 
paulson@14420
   256
                   summable_convergent_sumr_iff [symmetric] summable_exp)
paulson@14420
   257
paulson@14420
   258
lemma exphr_zero [simp]: "exphr 0 = 1"
paulson@14420
   259
apply (simp add: exphr_def sumhr_split_add
paulson@14420
   260
                   [OF hypnat_one_less_hypnat_omega, symmetric]) 
paulson@14420
   261
apply (simp add: sumhr hypnat_zero_def starfunNat hypnat_one_def hypnat_add
paulson@14420
   262
                 hypnat_omega_def hypreal_add 
paulson@14420
   263
            del: hypnat_add_zero_left)
paulson@14420
   264
apply (simp add: hypreal_one_num [symmetric])
paulson@14420
   265
done
paulson@14420
   266
paulson@14420
   267
lemma coshr_zero [simp]: "coshr 0 = 1"
paulson@14420
   268
apply (simp add: coshr_def sumhr_split_add
paulson@14420
   269
                   [OF hypnat_one_less_hypnat_omega, symmetric]) 
paulson@14420
   270
apply (simp add: sumhr hypnat_zero_def starfunNat hypnat_one_def 
paulson@14420
   271
         hypnat_add hypnat_omega_def st_add [symmetric] 
paulson@14420
   272
         hypreal_one_def [symmetric] hypreal_zero_def [symmetric]
paulson@14420
   273
       del: hypnat_add_zero_left)
paulson@14420
   274
done
paulson@14420
   275
paulson@14420
   276
lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) 0 @= 1"
paulson@14420
   277
by (simp add: hypreal_zero_def hypreal_one_def starfun hypreal_one_num)
paulson@14420
   278
paulson@14420
   279
lemma STAR_exp_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* exp) x @= 1"
paulson@14420
   280
apply (case_tac "x = 0")
paulson@14420
   281
apply (cut_tac [2] x = 0 in DERIV_exp)
paulson@14420
   282
apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
paulson@14420
   283
apply (drule_tac x = x in bspec, auto)
paulson@14420
   284
apply (drule_tac c = x in approx_mult1)
paulson@14420
   285
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] 
paulson@14420
   286
            simp add: mult_assoc)
paulson@14420
   287
apply (rule approx_add_right_cancel [where d="-1"])
paulson@14420
   288
apply (rule approx_sym [THEN [2] approx_trans2])
paulson@14420
   289
apply (auto simp add: mem_infmal_iff)
paulson@14420
   290
done
paulson@14420
   291
paulson@14420
   292
lemma STAR_exp_epsilon [simp]: "( *f* exp) epsilon @= 1"
paulson@14420
   293
by (auto intro: STAR_exp_Infinitesimal)
paulson@14420
   294
paulson@14420
   295
lemma STAR_exp_add: "( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y"
paulson@14468
   296
apply (cases x, cases y)
paulson@14420
   297
apply (simp add: starfun hypreal_add hypreal_mult exp_add)
paulson@14420
   298
done
paulson@14420
   299
paulson@14420
   300
lemma exphr_hypreal_of_real_exp_eq: "exphr x = hypreal_of_real (exp x)"
paulson@14420
   301
apply (simp add: exphr_def)
paulson@14420
   302
apply (rule st_hypreal_of_real [THEN subst])
paulson@14420
   303
apply (rule approx_st_eq, auto)
paulson@14420
   304
apply (rule approx_minus_iff [THEN iffD2])
paulson@14420
   305
apply (auto simp add: mem_infmal_iff [symmetric] hypreal_of_real_def hypnat_zero_def hypnat_omega_def sumhr hypreal_minus hypreal_add)
paulson@14420
   306
apply (rule NSLIMSEQ_zero_Infinitesimal_hypreal)
paulson@14420
   307
apply (insert exp_converges [of x]) 
paulson@14420
   308
apply (simp add: sums_def) 
paulson@14420
   309
apply (drule LIMSEQ_const [THEN [2] LIMSEQ_add, where b = "- exp x"])
paulson@14420
   310
apply (simp add: LIMSEQ_NSLIMSEQ_iff)
paulson@14420
   311
done
paulson@14420
   312
paulson@14420
   313
lemma starfun_exp_ge_add_one_self [simp]: "0 \<le> x ==> (1 + x) \<le> ( *f* exp) x"
paulson@14468
   314
apply (cases x)
paulson@14420
   315
apply (simp add: starfun hypreal_add hypreal_le hypreal_zero_num hypreal_one_num, ultra)
paulson@14420
   316
done
paulson@14420
   317
paulson@14420
   318
(* exp (oo) is infinite *)
paulson@14420
   319
lemma starfun_exp_HInfinite:
paulson@14420
   320
     "[| x \<in> HInfinite; 0 \<le> x |] ==> ( *f* exp) x \<in> HInfinite"
paulson@14420
   321
apply (frule starfun_exp_ge_add_one_self)
paulson@14420
   322
apply (rule HInfinite_ge_HInfinite, assumption)
paulson@14420
   323
apply (rule order_trans [of _ "1+x"], auto) 
paulson@14420
   324
done
paulson@14420
   325
paulson@14420
   326
lemma starfun_exp_minus: "( *f* exp) (-x) = inverse(( *f* exp) x)"
paulson@14468
   327
apply (cases x)
paulson@14420
   328
apply (simp add: starfun hypreal_inverse hypreal_minus exp_minus)
paulson@14420
   329
done
paulson@14420
   330
paulson@14420
   331
(* exp (-oo) is infinitesimal *)
paulson@14420
   332
lemma starfun_exp_Infinitesimal:
paulson@14420
   333
     "[| x \<in> HInfinite; x \<le> 0 |] ==> ( *f* exp) x \<in> Infinitesimal"
paulson@14420
   334
apply (subgoal_tac "\<exists>y. x = - y")
paulson@14420
   335
apply (rule_tac [2] x = "- x" in exI)
paulson@14420
   336
apply (auto intro!: HInfinite_inverse_Infinitesimal starfun_exp_HInfinite
paulson@14420
   337
            simp add: starfun_exp_minus HInfinite_minus_iff)
paulson@14420
   338
done
paulson@14420
   339
paulson@14420
   340
lemma starfun_exp_gt_one [simp]: "0 < x ==> 1 < ( *f* exp) x"
paulson@14468
   341
apply (cases x)
paulson@14420
   342
apply (simp add: starfun hypreal_one_num hypreal_zero_num hypreal_less, ultra)
paulson@14420
   343
done
paulson@14420
   344
paulson@14420
   345
(* needs derivative of inverse function
paulson@14420
   346
   TRY a NS one today!!!
paulson@14420
   347
paulson@14420
   348
Goal "x @= 1 ==> ( *f* ln) x @= 1"
paulson@14420
   349
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
paulson@14420
   350
by (auto_tac (claset(),simpset() addsimps [hypreal_one_def]));
paulson@14420
   351
paulson@14420
   352
paulson@14420
   353
Goalw [nsderiv_def] "0r < x ==> NSDERIV ln x :> inverse x";
paulson@14420
   354
paulson@14420
   355
*)
paulson@14420
   356
paulson@14420
   357
paulson@14420
   358
lemma starfun_ln_exp [simp]: "( *f* ln) (( *f* exp) x) = x"
paulson@14468
   359
apply (cases x)
paulson@14420
   360
apply (simp add: starfun)
paulson@14420
   361
done
paulson@14420
   362
paulson@14420
   363
lemma starfun_exp_ln_iff [simp]: "(( *f* exp)(( *f* ln) x) = x) = (0 < x)"
paulson@14468
   364
apply (cases x)
paulson@14420
   365
apply (simp add: starfun hypreal_zero_num hypreal_less)
paulson@14420
   366
done
paulson@14420
   367
paulson@14420
   368
lemma starfun_exp_ln_eq: "( *f* exp) u = x ==> ( *f* ln) x = u"
paulson@14420
   369
by (auto simp add: starfun)
paulson@14420
   370
paulson@14420
   371
lemma starfun_ln_less_self [simp]: "0 < x ==> ( *f* ln) x < x"
paulson@14468
   372
apply (cases x)
paulson@14420
   373
apply (simp add: starfun hypreal_zero_num hypreal_less, ultra)
paulson@14420
   374
done
paulson@14420
   375
paulson@14420
   376
lemma starfun_ln_ge_zero [simp]: "1 \<le> x ==> 0 \<le> ( *f* ln) x"
paulson@14468
   377
apply (cases x)
paulson@14420
   378
apply (simp add: starfun hypreal_zero_num hypreal_le hypreal_one_num, ultra)
paulson@14420
   379
done
paulson@14420
   380
paulson@14420
   381
lemma starfun_ln_gt_zero [simp]: "1 < x ==> 0 < ( *f* ln) x"
paulson@14468
   382
apply (cases x)
paulson@14420
   383
apply (simp add: starfun hypreal_zero_num hypreal_less hypreal_one_num, ultra)
paulson@14420
   384
done
paulson@14420
   385
paulson@14420
   386
lemma starfun_ln_not_eq_zero [simp]: "[| 0 < x; x \<noteq> 1 |] ==> ( *f* ln) x \<noteq> 0"
paulson@14468
   387
apply (cases x)
paulson@14420
   388
apply (auto simp add: starfun hypreal_zero_num hypreal_less hypreal_one_num, ultra)
paulson@14420
   389
apply (auto dest: ln_not_eq_zero) 
paulson@14420
   390
done
paulson@14420
   391
paulson@14420
   392
lemma starfun_ln_HFinite: "[| x \<in> HFinite; 1 \<le> x |] ==> ( *f* ln) x \<in> HFinite"
paulson@14420
   393
apply (rule HFinite_bounded)
paulson@14420
   394
apply (rule_tac [2] order_less_imp_le)
paulson@14420
   395
apply (rule_tac [2] starfun_ln_less_self)
paulson@14420
   396
apply (rule_tac [2] order_less_le_trans, auto)
paulson@14420
   397
done
paulson@14420
   398
paulson@14420
   399
lemma starfun_ln_inverse: "0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x"
paulson@14468
   400
apply (cases x)
paulson@14420
   401
apply (simp add: starfun hypreal_zero_num hypreal_minus hypreal_inverse hypreal_less, ultra)
paulson@14420
   402
apply (simp add: ln_inverse)
paulson@14420
   403
done
paulson@14420
   404
paulson@14420
   405
lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) x \<in> HFinite"
paulson@14468
   406
apply (cases x)
paulson@14420
   407
apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff)
paulson@14420
   408
apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
paulson@14420
   409
apply (rule_tac x = "exp u" in exI)
paulson@14420
   410
apply (ultra, arith)
paulson@14420
   411
done
paulson@14420
   412
paulson@14420
   413
lemma starfun_exp_add_HFinite_Infinitesimal_approx:
paulson@14420
   414
     "[|x \<in> Infinitesimal; z \<in> HFinite |] ==> ( *f* exp) (z + x) @= ( *f* exp) z"
paulson@14420
   415
apply (simp add: STAR_exp_add)
paulson@14420
   416
apply (frule STAR_exp_Infinitesimal)
paulson@14420
   417
apply (drule approx_mult2)
paulson@14420
   418
apply (auto intro: starfun_exp_HFinite)
paulson@14420
   419
done
paulson@14420
   420
paulson@14420
   421
(* using previous result to get to result *)
paulson@14420
   422
lemma starfun_ln_HInfinite:
paulson@14420
   423
     "[| x \<in> HInfinite; 0 < x |] ==> ( *f* ln) x \<in> HInfinite"
paulson@14420
   424
apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
paulson@14420
   425
apply (drule starfun_exp_HFinite)
paulson@14420
   426
apply (simp add: starfun_exp_ln_iff [THEN iffD2] HFinite_HInfinite_iff)
paulson@14420
   427
done
paulson@14420
   428
paulson@14420
   429
lemma starfun_exp_HInfinite_Infinitesimal_disj:
paulson@14420
   430
 "x \<in> HInfinite ==> ( *f* exp) x \<in> HInfinite | ( *f* exp) x \<in> Infinitesimal"
paulson@14420
   431
apply (insert linorder_linear [of x 0]) 
paulson@14420
   432
apply (auto intro: starfun_exp_HInfinite starfun_exp_Infinitesimal)
paulson@14420
   433
done
paulson@14420
   434
paulson@14420
   435
(* check out this proof!!! *)
paulson@14420
   436
lemma starfun_ln_HFinite_not_Infinitesimal:
paulson@14420
   437
     "[| x \<in> HFinite - Infinitesimal; 0 < x |] ==> ( *f* ln) x \<in> HFinite"
paulson@14420
   438
apply (rule ccontr, drule HInfinite_HFinite_iff [THEN iffD2])
paulson@14420
   439
apply (drule starfun_exp_HInfinite_Infinitesimal_disj)
paulson@14420
   440
apply (simp add: starfun_exp_ln_iff [symmetric] HInfinite_HFinite_iff
paulson@14420
   441
            del: starfun_exp_ln_iff)
paulson@14420
   442
done
paulson@14420
   443
paulson@14420
   444
(* we do proof by considering ln of 1/x *)
paulson@14420
   445
lemma starfun_ln_Infinitesimal_HInfinite:
paulson@14420
   446
     "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x \<in> HInfinite"
paulson@14420
   447
apply (drule Infinitesimal_inverse_HInfinite)
paulson@14420
   448
apply (frule positive_imp_inverse_positive)
paulson@14420
   449
apply (drule_tac [2] starfun_ln_HInfinite)
paulson@14420
   450
apply (auto simp add: starfun_ln_inverse HInfinite_minus_iff)
paulson@14420
   451
done
paulson@14420
   452
paulson@14420
   453
lemma starfun_ln_less_zero: "[| 0 < x; x < 1 |] ==> ( *f* ln) x < 0"
paulson@14468
   454
apply (cases x)
paulson@14420
   455
apply (simp add: hypreal_zero_num hypreal_one_num hypreal_less starfun, ultra)
paulson@14420
   456
apply (auto intro: ln_less_zero) 
paulson@14420
   457
done
paulson@14420
   458
paulson@14420
   459
lemma starfun_ln_Infinitesimal_less_zero:
paulson@14420
   460
     "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x < 0"
paulson@14420
   461
apply (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def)
paulson@14420
   462
apply (drule bspec [where x = 1])
paulson@14420
   463
apply (auto simp add: abs_if)
paulson@14420
   464
done
paulson@14420
   465
paulson@14420
   466
lemma starfun_ln_HInfinite_gt_zero:
paulson@14420
   467
     "[| x \<in> HInfinite; 0 < x |] ==> 0 < ( *f* ln) x"
paulson@14420
   468
apply (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def)
paulson@14420
   469
apply (drule bspec [where x = 1])
paulson@14420
   470
apply (auto simp add: abs_if)
paulson@14420
   471
done
paulson@14420
   472
paulson@14420
   473
(*
paulson@14420
   474
Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) -- 0 --NS> ln x"
paulson@14420
   475
*)
paulson@14420
   476
paulson@14420
   477
lemma HFinite_sin [simp]:
paulson@14420
   478
     "sumhr (0, whn, %n. (if even(n) then 0 else  
paulson@14420
   479
              ((- 1) ^ ((n - 1) div 2))/(real (fact n))) * x ^ n)  
paulson@14420
   480
              \<in> HFinite"
paulson@14420
   481
apply (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq 
paulson@14420
   482
            simp add: starfunNat_sumr [symmetric] starfunNat hypnat_omega_def
paulson@14420
   483
                      convergent_NSconvergent_iff [symmetric] 
paulson@14420
   484
                      summable_convergent_sumr_iff [symmetric])
paulson@14420
   485
apply (simp only: One_nat_def summable_sin)
paulson@14420
   486
done
paulson@14420
   487
paulson@14420
   488
lemma STAR_sin_zero [simp]: "( *f* sin) 0 = 0"
paulson@14420
   489
by (simp add: starfun hypreal_zero_num)
paulson@14420
   490
paulson@14420
   491
lemma STAR_sin_Infinitesimal [simp]: "x \<in> Infinitesimal ==> ( *f* sin) x @= x"
paulson@14420
   492
apply (case_tac "x = 0")
paulson@14420
   493
apply (cut_tac [2] x = 0 in DERIV_sin)
paulson@14420
   494
apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def hypreal_of_real_zero)
paulson@14420
   495
apply (drule bspec [where x = x], auto)
paulson@14420
   496
apply (drule approx_mult1 [where c = x])
paulson@14420
   497
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
paulson@14420
   498
           simp add: mult_assoc)
paulson@14420
   499
done
paulson@14420
   500
paulson@14420
   501
lemma HFinite_cos [simp]:
paulson@14420
   502
     "sumhr (0, whn, %n. (if even(n) then  
paulson@14420
   503
            ((- 1) ^ (n div 2))/(real (fact n)) else  
paulson@14420
   504
            0) * x ^ n) \<in> HFinite"
paulson@14420
   505
by (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq 
paulson@14420
   506
         simp add: starfunNat_sumr [symmetric] starfunNat hypnat_omega_def
paulson@14420
   507
                   convergent_NSconvergent_iff [symmetric] 
paulson@14420
   508
                   summable_convergent_sumr_iff [symmetric] summable_cos)
paulson@14420
   509
paulson@14420
   510
lemma STAR_cos_zero [simp]: "( *f* cos) 0 = 1"
paulson@14420
   511
by (simp add: starfun hypreal_zero_num hypreal_one_num)
paulson@14420
   512
paulson@14420
   513
lemma STAR_cos_Infinitesimal [simp]: "x \<in> Infinitesimal ==> ( *f* cos) x @= 1"
paulson@14420
   514
apply (case_tac "x = 0")
paulson@14420
   515
apply (cut_tac [2] x = 0 in DERIV_cos)
paulson@14420
   516
apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def hypreal_of_real_zero)
paulson@14420
   517
apply (drule bspec [where x = x])
paulson@14420
   518
apply (auto simp add: hypreal_of_real_zero hypreal_of_real_one)
paulson@14420
   519
apply (drule approx_mult1 [where c = x])
paulson@14420
   520
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
paulson@14420
   521
            simp add: mult_assoc hypreal_of_real_one)
paulson@14420
   522
apply (rule approx_add_right_cancel [where d = "-1"], auto)
paulson@14420
   523
done
paulson@14420
   524
paulson@14420
   525
lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
paulson@14420
   526
by (simp add: starfun hypreal_zero_num)
paulson@14420
   527
paulson@14420
   528
lemma STAR_tan_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* tan) x @= x"
paulson@14420
   529
apply (case_tac "x = 0")
paulson@14420
   530
apply (cut_tac [2] x = 0 in DERIV_tan)
paulson@14420
   531
apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def hypreal_of_real_zero)
paulson@14420
   532
apply (drule bspec [where x = x], auto)
paulson@14420
   533
apply (drule approx_mult1 [where c = x])
paulson@14420
   534
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
paulson@14420
   535
             simp add: mult_assoc)
paulson@14420
   536
done
paulson@14420
   537
paulson@14420
   538
lemma STAR_sin_cos_Infinitesimal_mult:
paulson@14420
   539
     "x \<in> Infinitesimal ==> ( *f* sin) x * ( *f* cos) x @= x"
paulson@14420
   540
apply (insert approx_mult_HFinite [of "( *f* sin) x" _ "( *f* cos) x" 1]) 
paulson@14420
   541
apply (simp add: Infinitesimal_subset_HFinite [THEN subsetD])
paulson@14420
   542
done
paulson@14420
   543
paulson@14420
   544
lemma HFinite_pi: "hypreal_of_real pi \<in> HFinite"
paulson@14420
   545
by simp
paulson@14420
   546
paulson@14420
   547
(* lemmas *)
paulson@14420
   548
paulson@14420
   549
lemma lemma_split_hypreal_of_real:
paulson@14420
   550
     "N \<in> HNatInfinite  
paulson@14420
   551
      ==> hypreal_of_real a =  
paulson@14420
   552
          hypreal_of_hypnat N * (inverse(hypreal_of_hypnat N) * hypreal_of_real a)"
paulson@14420
   553
by (simp add: mult_assoc [symmetric] HNatInfinite_not_eq_zero)
paulson@14420
   554
paulson@14420
   555
lemma STAR_sin_Infinitesimal_divide:
paulson@14420
   556
     "[|x \<in> Infinitesimal; x \<noteq> 0 |] ==> ( *f* sin) x/x @= 1"
paulson@14420
   557
apply (cut_tac x = 0 in DERIV_sin)
paulson@14420
   558
apply (simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def hypreal_of_real_zero hypreal_of_real_one)
paulson@14420
   559
done
paulson@14420
   560
paulson@14420
   561
(*------------------------------------------------------------------------*) 
paulson@14420
   562
(* sin* (1/n) * 1/(1/n) @= 1 for n = oo                                   *)
paulson@14420
   563
(*------------------------------------------------------------------------*)
paulson@14420
   564
paulson@14420
   565
lemma lemma_sin_pi:
paulson@14420
   566
     "n \<in> HNatInfinite  
paulson@14420
   567
      ==> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) @= 1"
paulson@14420
   568
apply (rule STAR_sin_Infinitesimal_divide)
paulson@14420
   569
apply (auto simp add: HNatInfinite_not_eq_zero)
paulson@14420
   570
done
paulson@14420
   571
paulson@14420
   572
lemma STAR_sin_inverse_HNatInfinite:
paulson@14420
   573
     "n \<in> HNatInfinite  
paulson@14420
   574
      ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n @= 1"
paulson@14420
   575
apply (frule lemma_sin_pi)
paulson@14430
   576
apply (simp add: divide_inverse)
paulson@14420
   577
done
paulson@14420
   578
paulson@14420
   579
lemma Infinitesimal_pi_divide_HNatInfinite: 
paulson@14420
   580
     "N \<in> HNatInfinite  
paulson@14420
   581
      ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<in> Infinitesimal"
paulson@14430
   582
apply (simp add: divide_inverse)
paulson@14420
   583
apply (auto intro: Infinitesimal_HFinite_mult2)
paulson@14420
   584
done
paulson@14420
   585
paulson@14420
   586
lemma pi_divide_HNatInfinite_not_zero [simp]:
paulson@14420
   587
     "N \<in> HNatInfinite ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<noteq> 0"
paulson@14420
   588
by (simp add: HNatInfinite_not_eq_zero)
paulson@14420
   589
paulson@14420
   590
lemma STAR_sin_pi_divide_HNatInfinite_approx_pi:
paulson@14420
   591
     "n \<in> HNatInfinite  
paulson@14420
   592
      ==> ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) * hypreal_of_hypnat n  
paulson@14420
   593
          @= hypreal_of_real pi"
paulson@14420
   594
apply (frule STAR_sin_Infinitesimal_divide
paulson@14420
   595
               [OF Infinitesimal_pi_divide_HNatInfinite 
paulson@14420
   596
                   pi_divide_HNatInfinite_not_zero])
paulson@14477
   597
apply (auto simp add: inverse_mult_distrib)
paulson@14420
   598
apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"])
paulson@14430
   599
apply (auto intro: SReal_inverse simp add: divide_inverse mult_ac)
paulson@14420
   600
done
paulson@14420
   601
paulson@14420
   602
lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2:
paulson@14420
   603
     "n \<in> HNatInfinite  
paulson@14420
   604
      ==> hypreal_of_hypnat n *  
paulson@14420
   605
          ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n))  
paulson@14420
   606
          @= hypreal_of_real pi"
paulson@14420
   607
apply (rule mult_commute [THEN subst])
paulson@14420
   608
apply (erule STAR_sin_pi_divide_HNatInfinite_approx_pi)
paulson@14420
   609
done
paulson@14420
   610
paulson@14420
   611
lemma starfunNat_pi_divide_n_Infinitesimal: 
paulson@14420
   612
     "N \<in> HNatInfinite ==> ( *fNat* (%x. pi / real x)) N \<in> Infinitesimal"
paulson@14420
   613
by (auto intro!: Infinitesimal_HFinite_mult2 
paulson@14430
   614
         simp add: starfunNat_mult [symmetric] divide_inverse
paulson@14420
   615
                   starfunNat_inverse [symmetric] starfunNat_real_of_nat)
paulson@14420
   616
paulson@14420
   617
lemma STAR_sin_pi_divide_n_approx:
paulson@14420
   618
     "N \<in> HNatInfinite ==>  
paulson@14420
   619
      ( *f* sin) (( *fNat* (%x. pi / real x)) N) @=  
paulson@14420
   620
      hypreal_of_real pi/(hypreal_of_hypnat N)"
paulson@14420
   621
by (auto intro!: STAR_sin_Infinitesimal Infinitesimal_HFinite_mult2 
paulson@14430
   622
         simp add: starfunNat_mult [symmetric] divide_inverse
paulson@14420
   623
                   starfunNat_inverse_real_of_nat_eq)
paulson@14420
   624
paulson@14420
   625
lemma NSLIMSEQ_sin_pi: "(%n. real n * sin (pi / real n)) ----NS> pi"
paulson@14420
   626
apply (auto simp add: NSLIMSEQ_def starfunNat_mult [symmetric] starfunNat_real_of_nat)
paulson@14420
   627
apply (rule_tac f1 = sin in starfun_stafunNat_o2 [THEN subst])
paulson@14430
   628
apply (auto simp add: starfunNat_mult [symmetric] starfunNat_real_of_nat divide_inverse)
paulson@14420
   629
apply (rule_tac f1 = inverse in starfun_stafunNat_o2 [THEN subst])
paulson@14420
   630
apply (auto dest: STAR_sin_pi_divide_HNatInfinite_approx_pi 
paulson@14430
   631
            simp add: starfunNat_real_of_nat mult_commute divide_inverse)
paulson@14420
   632
done
paulson@14420
   633
paulson@14420
   634
lemma NSLIMSEQ_cos_one: "(%n. cos (pi / real n))----NS> 1"
paulson@14420
   635
apply (simp add: NSLIMSEQ_def, auto)
paulson@14420
   636
apply (rule_tac f1 = cos in starfun_stafunNat_o2 [THEN subst])
paulson@14420
   637
apply (rule STAR_cos_Infinitesimal)
paulson@14420
   638
apply (auto intro!: Infinitesimal_HFinite_mult2 
paulson@14430
   639
            simp add: starfunNat_mult [symmetric] divide_inverse
paulson@14420
   640
                      starfunNat_inverse [symmetric] starfunNat_real_of_nat)
paulson@14420
   641
done
paulson@14420
   642
paulson@14420
   643
lemma NSLIMSEQ_sin_cos_pi:
paulson@14420
   644
     "(%n. real n * sin (pi / real n) * cos (pi / real n)) ----NS> pi"
paulson@14420
   645
by (insert NSLIMSEQ_mult [OF NSLIMSEQ_sin_pi NSLIMSEQ_cos_one], simp)
paulson@14420
   646
paulson@14420
   647
paulson@14420
   648
text{*A familiar approximation to @{term "cos x"} when @{term x} is small*}
paulson@14420
   649
paulson@14420
   650
lemma STAR_cos_Infinitesimal_approx:
paulson@14420
   651
     "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - x ^ 2"
paulson@14420
   652
apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
paulson@14420
   653
apply (auto simp add: Infinitesimal_approx_minus [symmetric] 
paulson@14420
   654
            diff_minus add_assoc [symmetric] numeral_2_eq_2)
paulson@14420
   655
done
paulson@14420
   656
paulson@14420
   657
lemma STAR_cos_Infinitesimal_approx2:
paulson@14420
   658
     "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - (x ^ 2)/2"
paulson@14420
   659
apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
paulson@14420
   660
apply (auto intro: Infinitesimal_SReal_divide 
paulson@14420
   661
            simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2)
paulson@14420
   662
done
paulson@14420
   663
paulson@14420
   664
ML
paulson@14420
   665
{*
paulson@14420
   666
val STAR_sqrt_zero = thm "STAR_sqrt_zero";
paulson@14420
   667
val STAR_sqrt_one = thm "STAR_sqrt_one";
paulson@14420
   668
val hypreal_sqrt_pow2_iff = thm "hypreal_sqrt_pow2_iff";
paulson@14420
   669
val hypreal_sqrt_gt_zero_pow2 = thm "hypreal_sqrt_gt_zero_pow2";
paulson@14420
   670
val hypreal_sqrt_pow2_gt_zero = thm "hypreal_sqrt_pow2_gt_zero";
paulson@14420
   671
val hypreal_sqrt_not_zero = thm "hypreal_sqrt_not_zero";
paulson@14420
   672
val hypreal_inverse_sqrt_pow2 = thm "hypreal_inverse_sqrt_pow2";
paulson@14420
   673
val hypreal_sqrt_mult_distrib = thm "hypreal_sqrt_mult_distrib";
paulson@14420
   674
val hypreal_sqrt_mult_distrib2 = thm "hypreal_sqrt_mult_distrib2";
paulson@14420
   675
val hypreal_sqrt_approx_zero = thm "hypreal_sqrt_approx_zero";
paulson@14420
   676
val hypreal_sqrt_approx_zero2 = thm "hypreal_sqrt_approx_zero2";
paulson@14420
   677
val hypreal_sqrt_sum_squares = thm "hypreal_sqrt_sum_squares";
paulson@14420
   678
val hypreal_sqrt_sum_squares2 = thm "hypreal_sqrt_sum_squares2";
paulson@14420
   679
val hypreal_sqrt_gt_zero = thm "hypreal_sqrt_gt_zero";
paulson@14420
   680
val hypreal_sqrt_ge_zero = thm "hypreal_sqrt_ge_zero";
paulson@14420
   681
val hypreal_sqrt_hrabs = thm "hypreal_sqrt_hrabs";
paulson@14420
   682
val hypreal_sqrt_hrabs2 = thm "hypreal_sqrt_hrabs2";
paulson@14420
   683
val hypreal_sqrt_hyperpow_hrabs = thm "hypreal_sqrt_hyperpow_hrabs";
paulson@14420
   684
val star_sqrt_HFinite = thm "star_sqrt_HFinite";
paulson@14420
   685
val st_hypreal_sqrt = thm "st_hypreal_sqrt";
paulson@14420
   686
val hypreal_sqrt_sum_squares_ge1 = thm "hypreal_sqrt_sum_squares_ge1";
paulson@14420
   687
val HFinite_hypreal_sqrt = thm "HFinite_hypreal_sqrt";
paulson@14420
   688
val HFinite_hypreal_sqrt_imp_HFinite = thm "HFinite_hypreal_sqrt_imp_HFinite";
paulson@14420
   689
val HFinite_hypreal_sqrt_iff = thm "HFinite_hypreal_sqrt_iff";
paulson@14420
   690
val HFinite_sqrt_sum_squares = thm "HFinite_sqrt_sum_squares";
paulson@14420
   691
val Infinitesimal_hypreal_sqrt = thm "Infinitesimal_hypreal_sqrt";
paulson@14420
   692
val Infinitesimal_hypreal_sqrt_imp_Infinitesimal = thm "Infinitesimal_hypreal_sqrt_imp_Infinitesimal";
paulson@14420
   693
val Infinitesimal_hypreal_sqrt_iff = thm "Infinitesimal_hypreal_sqrt_iff";
paulson@14420
   694
val Infinitesimal_sqrt_sum_squares = thm "Infinitesimal_sqrt_sum_squares";
paulson@14420
   695
val HInfinite_hypreal_sqrt = thm "HInfinite_hypreal_sqrt";
paulson@14420
   696
val HInfinite_hypreal_sqrt_imp_HInfinite = thm "HInfinite_hypreal_sqrt_imp_HInfinite";
paulson@14420
   697
val HInfinite_hypreal_sqrt_iff = thm "HInfinite_hypreal_sqrt_iff";
paulson@14420
   698
val HInfinite_sqrt_sum_squares = thm "HInfinite_sqrt_sum_squares";
paulson@14420
   699
val HFinite_exp = thm "HFinite_exp";
paulson@14420
   700
val exphr_zero = thm "exphr_zero";
paulson@14420
   701
val coshr_zero = thm "coshr_zero";
paulson@14420
   702
val STAR_exp_zero_approx_one = thm "STAR_exp_zero_approx_one";
paulson@14420
   703
val STAR_exp_Infinitesimal = thm "STAR_exp_Infinitesimal";
paulson@14420
   704
val STAR_exp_epsilon = thm "STAR_exp_epsilon";
paulson@14420
   705
val STAR_exp_add = thm "STAR_exp_add";
paulson@14420
   706
val exphr_hypreal_of_real_exp_eq = thm "exphr_hypreal_of_real_exp_eq";
paulson@14420
   707
val starfun_exp_ge_add_one_self = thm "starfun_exp_ge_add_one_self";
paulson@14420
   708
val starfun_exp_HInfinite = thm "starfun_exp_HInfinite";
paulson@14420
   709
val starfun_exp_minus = thm "starfun_exp_minus";
paulson@14420
   710
val starfun_exp_Infinitesimal = thm "starfun_exp_Infinitesimal";
paulson@14420
   711
val starfun_exp_gt_one = thm "starfun_exp_gt_one";
paulson@14420
   712
val starfun_ln_exp = thm "starfun_ln_exp";
paulson@14420
   713
val starfun_exp_ln_iff = thm "starfun_exp_ln_iff";
paulson@14420
   714
val starfun_exp_ln_eq = thm "starfun_exp_ln_eq";
paulson@14420
   715
val starfun_ln_less_self = thm "starfun_ln_less_self";
paulson@14420
   716
val starfun_ln_ge_zero = thm "starfun_ln_ge_zero";
paulson@14420
   717
val starfun_ln_gt_zero = thm "starfun_ln_gt_zero";
paulson@14420
   718
val starfun_ln_not_eq_zero = thm "starfun_ln_not_eq_zero";
paulson@14420
   719
val starfun_ln_HFinite = thm "starfun_ln_HFinite";
paulson@14420
   720
val starfun_ln_inverse = thm "starfun_ln_inverse";
paulson@14420
   721
val starfun_exp_HFinite = thm "starfun_exp_HFinite";
paulson@14420
   722
val starfun_exp_add_HFinite_Infinitesimal_approx = thm "starfun_exp_add_HFinite_Infinitesimal_approx";
paulson@14420
   723
val starfun_ln_HInfinite = thm "starfun_ln_HInfinite";
paulson@14420
   724
val starfun_exp_HInfinite_Infinitesimal_disj = thm "starfun_exp_HInfinite_Infinitesimal_disj";
paulson@14420
   725
val starfun_ln_HFinite_not_Infinitesimal = thm "starfun_ln_HFinite_not_Infinitesimal";
paulson@14420
   726
val starfun_ln_Infinitesimal_HInfinite = thm "starfun_ln_Infinitesimal_HInfinite";
paulson@14420
   727
val starfun_ln_less_zero = thm "starfun_ln_less_zero";
paulson@14420
   728
val starfun_ln_Infinitesimal_less_zero = thm "starfun_ln_Infinitesimal_less_zero";
paulson@14420
   729
val starfun_ln_HInfinite_gt_zero = thm "starfun_ln_HInfinite_gt_zero";
paulson@14420
   730
val HFinite_sin = thm "HFinite_sin";
paulson@14420
   731
val STAR_sin_zero = thm "STAR_sin_zero";
paulson@14420
   732
val STAR_sin_Infinitesimal = thm "STAR_sin_Infinitesimal";
paulson@14420
   733
val HFinite_cos = thm "HFinite_cos";
paulson@14420
   734
val STAR_cos_zero = thm "STAR_cos_zero";
paulson@14420
   735
val STAR_cos_Infinitesimal = thm "STAR_cos_Infinitesimal";
paulson@14420
   736
val STAR_tan_zero = thm "STAR_tan_zero";
paulson@14420
   737
val STAR_tan_Infinitesimal = thm "STAR_tan_Infinitesimal";
paulson@14420
   738
val STAR_sin_cos_Infinitesimal_mult = thm "STAR_sin_cos_Infinitesimal_mult";
paulson@14420
   739
val HFinite_pi = thm "HFinite_pi";
paulson@14420
   740
val lemma_split_hypreal_of_real = thm "lemma_split_hypreal_of_real";
paulson@14420
   741
val STAR_sin_Infinitesimal_divide = thm "STAR_sin_Infinitesimal_divide";
paulson@14420
   742
val lemma_sin_pi = thm "lemma_sin_pi";
paulson@14420
   743
val STAR_sin_inverse_HNatInfinite = thm "STAR_sin_inverse_HNatInfinite";
paulson@14420
   744
val Infinitesimal_pi_divide_HNatInfinite = thm "Infinitesimal_pi_divide_HNatInfinite";
paulson@14420
   745
val pi_divide_HNatInfinite_not_zero = thm "pi_divide_HNatInfinite_not_zero";
paulson@14420
   746
val STAR_sin_pi_divide_HNatInfinite_approx_pi = thm "STAR_sin_pi_divide_HNatInfinite_approx_pi";
paulson@14420
   747
val STAR_sin_pi_divide_HNatInfinite_approx_pi2 = thm "STAR_sin_pi_divide_HNatInfinite_approx_pi2";
paulson@14420
   748
val starfunNat_pi_divide_n_Infinitesimal = thm "starfunNat_pi_divide_n_Infinitesimal";
paulson@14420
   749
val STAR_sin_pi_divide_n_approx = thm "STAR_sin_pi_divide_n_approx";
paulson@14420
   750
val NSLIMSEQ_sin_pi = thm "NSLIMSEQ_sin_pi";
paulson@14420
   751
val NSLIMSEQ_cos_one = thm "NSLIMSEQ_cos_one";
paulson@14420
   752
val NSLIMSEQ_sin_cos_pi = thm "NSLIMSEQ_sin_cos_pi";
paulson@14420
   753
val STAR_cos_Infinitesimal_approx = thm "STAR_cos_Infinitesimal_approx";
paulson@14420
   754
val STAR_cos_Infinitesimal_approx2 = thm "STAR_cos_Infinitesimal_approx2";
paulson@14420
   755
*}
paulson@14420
   756
paulson@14420
   757
paulson@14420
   758
end