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