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