equal
deleted
inserted
replaced
8 header{*Nonstandard Extensions of Transcendental Functions*} |
8 header{*Nonstandard Extensions of Transcendental Functions*} |
9 |
9 |
10 theory HTranscendental |
10 theory HTranscendental |
11 imports Transcendental Integration HSeries |
11 imports Transcendental Integration HSeries |
12 begin |
12 begin |
13 |
|
14 text{*really belongs in Transcendental*} |
|
15 lemma sqrt_divide_self_eq: |
|
16 assumes nneg: "0 \<le> x" |
|
17 shows "sqrt x / x = inverse (sqrt x)" |
|
18 proof cases |
|
19 assume "x=0" thus ?thesis by simp |
|
20 next |
|
21 assume nz: "x\<noteq>0" |
|
22 hence pos: "0<x" using nneg by arith |
|
23 show ?thesis |
|
24 proof (rule right_inverse_eq [THEN iffD1, THEN sym]) |
|
25 show "sqrt x / x \<noteq> 0" by (simp add: divide_inverse nneg nz) |
|
26 show "inverse (sqrt x) / (sqrt x / x) = 1" |
|
27 by (simp add: divide_inverse mult_assoc [symmetric] |
|
28 power2_eq_square [symmetric] real_inv_sqrt_pow2 pos nz) |
|
29 qed |
|
30 qed |
|
31 |
|
32 |
13 |
33 definition |
14 definition |
34 exphr :: "real => hypreal" where |
15 exphr :: "real => hypreal" where |
35 --{*define exponential function using standard part *} |
16 --{*define exponential function using standard part *} |
36 "exphr x = st(sumhr (0, whn, %n. inverse(real (fact n)) * (x ^ n)))" |
17 "exphr x = st(sumhr (0, whn, %n. inverse(real (fact n)) * (x ^ n)))" |