6 *) |
6 *) |
7 |
7 |
8 header{*Construction of Hyperreals Using Ultrafilters*} |
8 header{*Construction of Hyperreals Using Ultrafilters*} |
9 |
9 |
10 theory HyperDef |
10 theory HyperDef |
11 (*imports Filter "../Real/Real"*) |
|
12 imports StarClasses "../Real/Real" |
11 imports StarClasses "../Real/Real" |
13 uses ("fuf.ML") (*Warning: file fuf.ML refers to the name Hyperdef!*) |
12 uses ("fuf.ML") (*Warning: file fuf.ML refers to the name Hyperdef!*) |
14 begin |
13 begin |
15 |
14 |
16 types hypreal = "real star" |
15 types hypreal = "real star" |
17 (* |
16 |
|
17 syntax hypreal_of_real :: "real => real star" |
|
18 translations "hypreal_of_real" => "star_of :: real => real star" |
|
19 |
|
20 typed_print_translation {* |
|
21 let |
|
22 fun hr_tr' _ (Type ("fun", (Type ("real", []) :: _))) [t] = |
|
23 Syntax.const "hypreal_of_real" $ t |
|
24 | hr_tr' _ _ _ = raise Match; |
|
25 in [("star_of", hr_tr')] end |
|
26 *} |
|
27 |
18 constdefs |
28 constdefs |
19 |
29 |
20 FreeUltrafilterNat :: "nat set set" ("\<U>") |
|
21 "FreeUltrafilterNat == (SOME U. freeultrafilter U)" |
|
22 |
|
23 hyprel :: "((nat=>real)*(nat=>real)) set" |
|
24 "hyprel == {p. \<exists>X Y. p = ((X::nat=>real),Y) & |
|
25 {n::nat. X(n) = Y(n)} \<in> FreeUltrafilterNat}" |
|
26 |
|
27 typedef hypreal = "UNIV//hyprel" |
|
28 by (auto simp add: quotient_def) |
|
29 |
|
30 instance hypreal :: "{ord, zero, one, plus, times, minus, inverse}" .. |
|
31 |
|
32 defs (overloaded) |
|
33 |
|
34 hypreal_zero_def: |
|
35 "0 == Abs_hypreal(hyprel``{%n. 0})" |
|
36 |
|
37 hypreal_one_def: |
|
38 "1 == Abs_hypreal(hyprel``{%n. 1})" |
|
39 |
|
40 hypreal_minus_def: |
|
41 "- P == Abs_hypreal(\<Union>X \<in> Rep_hypreal(P). hyprel``{%n. - (X n)})" |
|
42 |
|
43 hypreal_diff_def: |
|
44 "x - y == x + -(y::hypreal)" |
|
45 |
|
46 hypreal_inverse_def: |
|
47 "inverse P == Abs_hypreal(\<Union>X \<in> Rep_hypreal(P). |
|
48 hyprel``{%n. if X n = 0 then 0 else inverse (X n)})" |
|
49 |
|
50 hypreal_divide_def: |
|
51 "P / Q::hypreal == P * inverse Q" |
|
52 *) |
|
53 |
|
54 lemma hypreal_zero_def: "0 == Abs_star(starrel``{%n. 0})" |
|
55 by (simp only: star_zero_def star_of_def star_n_def) |
|
56 |
|
57 lemma hypreal_one_def: "1 == Abs_star(starrel``{%n. 1})" |
|
58 by (simp only: star_one_def star_of_def star_n_def) |
|
59 |
|
60 lemma hypreal_diff_def: "x - y == x + -(y::hypreal)" |
|
61 by (rule diff_def) |
|
62 |
|
63 lemma hypreal_divide_def: "P / Q::hypreal == P * inverse Q" |
|
64 by (rule divide_inverse [THEN eq_reflection]) |
|
65 |
|
66 constdefs |
|
67 |
|
68 hypreal_of_real :: "real => hypreal" |
|
69 (* "hypreal_of_real r == Abs_hypreal(hyprel``{%n. r})" *) |
|
70 "hypreal_of_real r == star_of r" |
|
71 |
|
72 omega :: hypreal -- {*an infinite number @{text "= [<1,2,3,...>]"} *} |
30 omega :: hypreal -- {*an infinite number @{text "= [<1,2,3,...>]"} *} |
73 (* "omega == Abs_hypreal(hyprel``{%n. real (Suc n)})" *) |
|
74 "omega == star_n (%n. real (Suc n))" |
31 "omega == star_n (%n. real (Suc n))" |
75 |
32 |
76 epsilon :: hypreal -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *} |
33 epsilon :: hypreal -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *} |
77 (* "epsilon == Abs_hypreal(hyprel``{%n. inverse (real (Suc n))})" *) |
|
78 "epsilon == star_n (%n. inverse (real (Suc n)))" |
34 "epsilon == star_n (%n. inverse (real (Suc n)))" |
79 |
35 |
80 syntax (xsymbols) |
36 syntax (xsymbols) |
81 omega :: hypreal ("\<omega>") |
37 omega :: hypreal ("\<omega>") |
82 epsilon :: hypreal ("\<epsilon>") |
38 epsilon :: hypreal ("\<epsilon>") |
83 |
39 |
84 syntax (HTML output) |
40 syntax (HTML output) |
85 omega :: hypreal ("\<omega>") |
41 omega :: hypreal ("\<omega>") |
86 epsilon :: hypreal ("\<epsilon>") |
42 epsilon :: hypreal ("\<epsilon>") |
87 |
43 |
88 (* |
|
89 defs (overloaded) |
|
90 |
|
91 hypreal_add_def: |
|
92 "P + Q == Abs_hypreal(\<Union>X \<in> Rep_hypreal(P). \<Union>Y \<in> Rep_hypreal(Q). |
|
93 hyprel``{%n. X n + Y n})" |
|
94 |
|
95 hypreal_mult_def: |
|
96 "P * Q == Abs_hypreal(\<Union>X \<in> Rep_hypreal(P). \<Union>Y \<in> Rep_hypreal(Q). |
|
97 hyprel``{%n. X n * Y n})" |
|
98 |
|
99 hypreal_le_def: |
|
100 "P \<le> (Q::hypreal) == \<exists>X Y. X \<in> Rep_hypreal(P) & |
|
101 Y \<in> Rep_hypreal(Q) & |
|
102 {n. X n \<le> Y n} \<in> FreeUltrafilterNat" |
|
103 |
|
104 hypreal_less_def: "(x < (y::hypreal)) == (x \<le> y & x \<noteq> y)" |
|
105 |
|
106 hrabs_def: "abs (r::hypreal) == (if 0 \<le> r then r else -r)" |
|
107 *) |
|
108 |
44 |
109 subsection{*The Set of Naturals is not Finite*} |
45 subsection{*The Set of Naturals is not Finite*} |
110 |
46 |
111 (*** based on James' proof that the set of naturals is not finite ***) |
47 (*** based on James' proof that the set of naturals is not finite ***) |
112 lemma finite_exhausts [rule_format]: |
48 lemma finite_exhausts [rule_format]: |
275 |
211 |
276 subsection{*@{term hypreal_of_real}: |
212 subsection{*@{term hypreal_of_real}: |
277 the Injection from @{typ real} to @{typ hypreal}*} |
213 the Injection from @{typ real} to @{typ hypreal}*} |
278 |
214 |
279 lemma inj_hypreal_of_real: "inj(hypreal_of_real)" |
215 lemma inj_hypreal_of_real: "inj(hypreal_of_real)" |
280 apply (rule inj_onI) |
216 by (rule inj_onI, simp) |
281 apply (simp add: hypreal_of_real_def split: split_if_asm) |
|
282 done |
|
283 |
217 |
284 lemma eq_Abs_star: |
218 lemma eq_Abs_star: |
285 "(!!x. z = Abs_star(starrel``{x}) ==> P) ==> P" |
219 "(!!x. z = Abs_star(starrel``{x}) ==> P) ==> P" |
286 by (fold star_n_def, auto intro: star_cases) |
220 by (fold star_n_def, auto intro: star_cases) |
287 |
221 |
288 (* |
222 lemma Rep_star_star_n_iff [simp]: |
289 theorem hypreal_cases [case_names Abs_hypreal, cases type: hypreal]: |
223 "(X \<in> Rep_star (star_n Y)) = ({n. Y n = X n} \<in> \<U>)" |
290 "(!!x. z = star_n x ==> P) ==> P" |
224 by (simp add: star_n_def) |
291 by (rule eq_Abs_hypreal [of z], blast) |
225 |
292 *) |
226 lemma Rep_star_star_n: "X \<in> Rep_star (star_n X)" |
|
227 by simp |
293 |
228 |
294 subsection{*Hyperreal Addition*} |
229 subsection{*Hyperreal Addition*} |
295 (* |
230 |
296 lemma hypreal_add_congruent2: |
231 lemma star_n_add: |
297 "congruent2 starrel starrel (%X Y. starrel``{%n. X n + Y n})" |
|
298 by (simp add: congruent2_def, auto, ultra) |
|
299 *) |
|
300 lemma hypreal_add [unfolded star_n_def]: |
|
301 "star_n X + star_n Y = star_n (%n. X n + Y n)" |
232 "star_n X + star_n Y = star_n (%n. X n + Y n)" |
302 by (simp add: star_add_def Ifun2_of_def star_of_def Ifun_star_n) |
233 by (simp add: star_add_def Ifun2_of_def star_of_def Ifun_star_n) |
303 |
234 |
304 lemma hypreal_add_commute: "(z::hypreal) + w = w + z" |
|
305 by (rule add_commute) |
|
306 |
|
307 lemma hypreal_add_assoc: "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)" |
|
308 by (rule add_assoc) |
|
309 |
|
310 lemma hypreal_add_zero_left: "(0::hypreal) + z = z" |
|
311 by (rule comm_monoid_add_class.add_0) |
|
312 |
|
313 (*instance hypreal :: comm_monoid_add |
|
314 by intro_classes |
|
315 (assumption | |
|
316 rule hypreal_add_commute hypreal_add_assoc hypreal_add_zero_left)+*) |
|
317 |
|
318 lemma hypreal_add_zero_right [simp]: "z + (0::hypreal) = z" |
|
319 by (rule OrderedGroup.add_0_right) |
|
320 |
|
321 |
|
322 subsection{*Additive inverse on @{typ hypreal}*} |
235 subsection{*Additive inverse on @{typ hypreal}*} |
323 (* |
236 |
324 lemma hypreal_minus_congruent: "(%X. starrel``{%n. - (X n)}) respects starrel" |
237 lemma star_n_minus: |
325 by (force simp add: congruent_def) |
|
326 *) |
|
327 lemma hypreal_minus [unfolded star_n_def]: |
|
328 "- star_n X = star_n (%n. -(X n))" |
238 "- star_n X = star_n (%n. -(X n))" |
329 by (simp add: star_minus_def Ifun_of_def star_of_def Ifun_star_n) |
239 by (simp add: star_minus_def Ifun_of_def star_of_def Ifun_star_n) |
330 |
240 |
331 lemma hypreal_diff [unfolded star_n_def]: |
241 lemma star_n_diff: |
332 "star_n X - star_n Y = star_n (%n. X n - Y n)" |
242 "star_n X - star_n Y = star_n (%n. X n - Y n)" |
333 by (simp add: star_diff_def Ifun2_of_def star_of_def Ifun_star_n) |
243 by (simp add: star_diff_def Ifun2_of_def star_of_def Ifun_star_n) |
334 |
244 |
335 lemma hypreal_add_minus [simp]: "z + -z = (0::hypreal)" |
|
336 by (rule right_minus) |
|
337 |
|
338 lemma hypreal_add_minus_left: "-z + z = (0::hypreal)" |
|
339 by (rule left_minus) |
|
340 |
|
341 |
245 |
342 subsection{*Hyperreal Multiplication*} |
246 subsection{*Hyperreal Multiplication*} |
343 (* |
247 |
344 lemma hypreal_mult_congruent2: |
248 lemma star_n_mult: |
345 "congruent2 starrel starrel (%X Y. starrel``{%n. X n * Y n})" |
|
346 by (simp add: congruent2_def, auto, ultra) |
|
347 *) |
|
348 |
|
349 lemma hypreal_mult [unfolded star_n_def]: |
|
350 "star_n X * star_n Y = star_n (%n. X n * Y n)" |
249 "star_n X * star_n Y = star_n (%n. X n * Y n)" |
351 by (simp add: star_mult_def Ifun2_of_def star_of_def Ifun_star_n) |
250 by (simp add: star_mult_def Ifun2_of_def star_of_def Ifun_star_n) |
352 |
251 |
353 lemma hypreal_mult_commute: "(z::hypreal) * w = w * z" |
|
354 by (rule mult_commute) |
|
355 |
|
356 lemma hypreal_mult_assoc: "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)" |
|
357 by (rule mult_assoc) |
|
358 |
|
359 lemma hypreal_mult_1: "(1::hypreal) * z = z" |
|
360 by (rule mult_1_left) |
|
361 |
|
362 lemma hypreal_add_mult_distrib: |
|
363 "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)" |
|
364 by (rule left_distrib) |
|
365 |
|
366 text{*one and zero are distinct*} |
|
367 lemma hypreal_zero_not_eq_one: "0 \<noteq> (1::hypreal)" |
|
368 by (rule zero_neq_one) |
|
369 |
|
370 |
252 |
371 subsection{*Multiplicative Inverse on @{typ hypreal} *} |
253 subsection{*Multiplicative Inverse on @{typ hypreal} *} |
372 (* |
254 |
373 lemma hypreal_inverse_congruent: |
255 lemma star_n_inverse: |
374 "(%X. starrel``{%n. if X n = 0 then 0 else inverse(X n)}) respects starrel" |
|
375 by (auto simp add: congruent_def, ultra) |
|
376 *) |
|
377 lemma hypreal_inverse [unfolded star_n_def]: |
|
378 "inverse (star_n X) = star_n (%n. if X n = (0::real) then 0 else inverse(X n))" |
256 "inverse (star_n X) = star_n (%n. if X n = (0::real) then 0 else inverse(X n))" |
379 apply (simp add: star_inverse_def Ifun_of_def star_of_def Ifun_star_n) |
257 apply (simp add: star_inverse_def Ifun_of_def star_of_def Ifun_star_n) |
380 apply (rule_tac f=star_n in arg_cong) |
258 apply (rule_tac f=star_n in arg_cong) |
381 apply (rule ext) |
259 apply (rule ext) |
382 apply simp |
260 apply simp |
383 done |
261 done |
384 |
262 |
385 lemma hypreal_inverse2 [unfolded star_n_def]: |
263 lemma star_n_inverse2: |
386 "inverse (star_n X) = star_n (%n. inverse(X n))" |
264 "inverse (star_n X) = star_n (%n. inverse(X n))" |
387 by (simp add: star_inverse_def Ifun_of_def star_of_def Ifun_star_n) |
265 by (simp add: star_inverse_def Ifun_of_def star_of_def Ifun_star_n) |
388 |
266 |
389 lemma hypreal_mult_inverse: |
|
390 "x \<noteq> 0 ==> x*inverse(x) = (1::hypreal)" |
|
391 by (rule right_inverse) |
|
392 |
|
393 lemma hypreal_mult_inverse_left: |
|
394 "x \<noteq> 0 ==> inverse(x)*x = (1::hypreal)" |
|
395 by (rule left_inverse) |
|
396 |
|
397 (* |
|
398 instance hypreal :: field |
|
399 proof |
|
400 fix x y z :: hypreal |
|
401 show "- x + x = 0" by (simp add: hypreal_add_minus_left) |
|
402 show "x - y = x + (-y)" by (simp add: hypreal_diff_def) |
|
403 show "(x * y) * z = x * (y * z)" by (rule hypreal_mult_assoc) |
|
404 show "x * y = y * x" by (rule hypreal_mult_commute) |
|
405 show "1 * x = x" by (simp add: hypreal_mult_1) |
|
406 show "(x + y) * z = x * z + y * z" by (simp add: hypreal_add_mult_distrib) |
|
407 show "0 \<noteq> (1::hypreal)" by (rule hypreal_zero_not_eq_one) |
|
408 show "x \<noteq> 0 ==> inverse x * x = 1" by (simp add: hypreal_mult_inverse_left) |
|
409 show "x / y = x * inverse y" by (simp add: hypreal_divide_def) |
|
410 qed |
|
411 |
|
412 |
|
413 instance hypreal :: division_by_zero |
|
414 proof |
|
415 show "inverse 0 = (0::hypreal)" |
|
416 by (simp add: hypreal_inverse hypreal_zero_def) |
|
417 qed |
|
418 *) |
|
419 |
267 |
420 subsection{*Properties of The @{text "\<le>"} Relation*} |
268 subsection{*Properties of The @{text "\<le>"} Relation*} |
421 |
269 |
422 lemma hypreal_le [unfolded star_n_def]: |
270 lemma star_n_le: |
423 "star_n X \<le> star_n Y = |
271 "star_n X \<le> star_n Y = |
424 ({n. X n \<le> Y n} \<in> FreeUltrafilterNat)" |
272 ({n. X n \<le> Y n} \<in> FreeUltrafilterNat)" |
425 by (simp add: star_le_def Ipred2_of_def star_of_def Ifun_star_n unstar_star_n) |
273 by (simp add: star_le_def Ipred2_of_def star_of_def Ifun_star_n unstar_star_n) |
426 |
274 |
427 lemma hypreal_le_refl: "w \<le> (w::hypreal)" |
|
428 by (rule order_refl) |
|
429 |
|
430 lemma hypreal_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::hypreal)" |
|
431 by (rule order_trans) |
|
432 |
|
433 lemma hypreal_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::hypreal)" |
|
434 by (rule order_antisym) |
|
435 |
|
436 (* Axiom 'order_less_le' of class 'order': *) |
|
437 lemma hypreal_less_le: "((w::hypreal) < z) = (w \<le> z & w \<noteq> z)" |
|
438 by (rule order_less_le) |
|
439 |
|
440 (* |
|
441 instance hypreal :: order |
|
442 by intro_classes |
|
443 (assumption | |
|
444 rule hypreal_le_refl hypreal_le_trans hypreal_le_anti_sym hypreal_less_le)+ |
|
445 *) |
|
446 |
|
447 (* Axiom 'linorder_linear' of class 'linorder': *) |
|
448 lemma hypreal_le_linear: "(z::hypreal) \<le> w | w \<le> z" |
|
449 by (rule linorder_linear) |
|
450 |
|
451 (* |
|
452 instance hypreal :: linorder |
|
453 by intro_classes (rule hypreal_le_linear) |
|
454 *) |
|
455 |
|
456 lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y" |
275 lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y" |
457 by (auto) |
276 by (auto) |
458 |
277 |
459 lemma hypreal_add_left_mono: "x \<le> y ==> z + x \<le> z + (y::hypreal)" |
|
460 by (rule add_left_mono) |
|
461 |
|
462 lemma hypreal_mult_less_mono2: "[| (0::hypreal)<z; x<y |] ==> z*x<z*y" |
|
463 by (rule mult_strict_left_mono) |
|
464 |
|
465 |
|
466 subsection{*The Hyperreals Form an Ordered Field*} |
278 subsection{*The Hyperreals Form an Ordered Field*} |
467 |
|
468 (* |
|
469 instance hypreal :: ordered_field |
|
470 proof |
|
471 fix x y z :: hypreal |
|
472 show "x \<le> y ==> z + x \<le> z + y" |
|
473 by (rule hypreal_add_left_mono) |
|
474 show "x < y ==> 0 < z ==> z * x < z * y" |
|
475 by (simp add: hypreal_mult_less_mono2) |
|
476 show "\<bar>x\<bar> = (if x < 0 then -x else x)" |
|
477 by (auto dest: order_le_less_trans simp add: hrabs_def linorder_not_le) |
|
478 qed |
|
479 *) |
|
480 |
279 |
481 lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)" |
280 lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)" |
482 by auto |
281 by auto |
483 |
282 |
484 lemma hypreal_mult_left_cancel: "(c::hypreal) \<noteq> 0 ==> (c*a=c*b) = (a=b)" |
283 lemma hypreal_mult_left_cancel: "(c::hypreal) \<noteq> 0 ==> (c*a=c*b) = (a=b)" |
486 |
285 |
487 lemma hypreal_mult_right_cancel: "(c::hypreal) \<noteq> 0 ==> (a*c=b*c) = (a=b)" |
286 lemma hypreal_mult_right_cancel: "(c::hypreal) \<noteq> 0 ==> (a*c=b*c) = (a=b)" |
488 by auto |
287 by auto |
489 |
288 |
490 |
289 |
491 subsection{*The Embedding @{term hypreal_of_real} Preserves Field and |
|
492 Order Properties*} |
|
493 |
|
494 lemma hypreal_of_real_add [simp]: |
|
495 "hypreal_of_real (w + z) = hypreal_of_real w + hypreal_of_real z" |
|
496 by (simp add: hypreal_of_real_def) |
|
497 |
|
498 lemma hypreal_of_real_minus [simp]: |
|
499 "hypreal_of_real (-r) = - hypreal_of_real r" |
|
500 by (simp add: hypreal_of_real_def) |
|
501 |
|
502 lemma hypreal_of_real_diff [simp]: |
|
503 "hypreal_of_real (w - z) = hypreal_of_real w - hypreal_of_real z" |
|
504 by (simp add: hypreal_of_real_def) |
|
505 |
|
506 lemma hypreal_of_real_mult [simp]: |
|
507 "hypreal_of_real (w * z) = hypreal_of_real w * hypreal_of_real z" |
|
508 by (simp add: hypreal_of_real_def) |
|
509 |
|
510 lemma hypreal_of_real_one [simp]: "hypreal_of_real 1 = (1::hypreal)" |
|
511 by (simp add: hypreal_of_real_def) |
|
512 |
|
513 lemma hypreal_of_real_zero [simp]: "hypreal_of_real 0 = 0" |
|
514 by (simp add: hypreal_of_real_def) |
|
515 |
|
516 lemma hypreal_of_real_le_iff [simp]: |
|
517 "(hypreal_of_real w \<le> hypreal_of_real z) = (w \<le> z)" |
|
518 by (simp add: hypreal_of_real_def) |
|
519 |
|
520 lemma hypreal_of_real_less_iff [simp]: |
|
521 "(hypreal_of_real w < hypreal_of_real z) = (w < z)" |
|
522 by (simp add: hypreal_of_real_def) |
|
523 |
|
524 lemma hypreal_of_real_eq_iff [simp]: |
|
525 "(hypreal_of_real w = hypreal_of_real z) = (w = z)" |
|
526 by (simp add: hypreal_of_real_def) |
|
527 |
|
528 text{*As above, for 0*} |
|
529 |
|
530 declare hypreal_of_real_less_iff [of 0, simplified, simp] |
|
531 declare hypreal_of_real_le_iff [of 0, simplified, simp] |
|
532 declare hypreal_of_real_eq_iff [of 0, simplified, simp] |
|
533 |
|
534 declare hypreal_of_real_less_iff [of _ 0, simplified, simp] |
|
535 declare hypreal_of_real_le_iff [of _ 0, simplified, simp] |
|
536 declare hypreal_of_real_eq_iff [of _ 0, simplified, simp] |
|
537 |
|
538 text{*As above, for 1*} |
|
539 |
|
540 declare hypreal_of_real_less_iff [of 1, simplified, simp] |
|
541 declare hypreal_of_real_le_iff [of 1, simplified, simp] |
|
542 declare hypreal_of_real_eq_iff [of 1, simplified, simp] |
|
543 |
|
544 declare hypreal_of_real_less_iff [of _ 1, simplified, simp] |
|
545 declare hypreal_of_real_le_iff [of _ 1, simplified, simp] |
|
546 declare hypreal_of_real_eq_iff [of _ 1, simplified, simp] |
|
547 |
|
548 lemma hypreal_of_real_inverse [simp]: |
|
549 "hypreal_of_real (inverse r) = inverse (hypreal_of_real r)" |
|
550 by (simp add: hypreal_of_real_def) |
|
551 |
|
552 lemma hypreal_of_real_divide [simp]: |
|
553 "hypreal_of_real (w / z) = hypreal_of_real w / hypreal_of_real z" |
|
554 by (simp add: hypreal_of_real_def) |
|
555 |
|
556 lemma hypreal_of_real_of_nat [simp]: "hypreal_of_real (of_nat n) = of_nat n" |
|
557 by (simp add: hypreal_of_real_def) |
|
558 |
|
559 lemma hypreal_of_real_of_int [simp]: "hypreal_of_real (of_int z) = of_int z" |
|
560 by (simp add: hypreal_of_real_def) |
|
561 |
|
562 |
|
563 subsection{*Misc Others*} |
290 subsection{*Misc Others*} |
564 |
291 |
565 lemma hypreal_less [unfolded star_n_def]: |
292 lemma star_n_less: |
566 "star_n X < star_n Y = ({n. X n < Y n} \<in> FreeUltrafilterNat)" |
293 "star_n X < star_n Y = ({n. X n < Y n} \<in> FreeUltrafilterNat)" |
567 by (simp add: star_less_def Ipred2_of_def star_of_def Ifun_star_n unstar_star_n) |
294 by (simp add: star_less_def Ipred2_of_def star_of_def Ifun_star_n unstar_star_n) |
568 |
295 |
569 lemma hypreal_zero_num [unfolded star_n_def]: "0 = star_n (%n. 0)" |
296 lemma star_n_zero_num: "0 = star_n (%n. 0)" |
570 by (simp add: star_zero_def star_of_def) |
297 by (simp add: star_zero_def star_of_def) |
571 |
298 |
572 lemma hypreal_one_num [unfolded star_n_def]: "1 = star_n (%n. 1)" |
299 lemma star_n_one_num: "1 = star_n (%n. 1)" |
573 by (simp add: star_one_def star_of_def) |
300 by (simp add: star_one_def star_of_def) |
574 |
301 |
575 lemma hypreal_omega_gt_zero [simp]: "0 < omega" |
302 lemma hypreal_omega_gt_zero [simp]: "0 < omega" |
576 apply (simp only: omega_def star_zero_def star_less_def star_of_def) |
303 apply (simp only: omega_def star_zero_def star_less_def star_of_def) |
577 apply (simp add: Ipred2_of_def star_of_def Ifun_star_n unstar_star_n) |
304 apply (simp add: Ipred2_of_def star_of_def Ifun_star_n unstar_star_n) |
578 done |
305 done |
579 |
306 |
580 lemma hypreal_hrabs [unfolded star_n_def]: |
307 lemma star_n_abs: |
581 "abs (star_n X) = star_n (%n. abs (X n))" |
308 "abs (star_n X) = star_n (%n. abs (X n))" |
582 by (simp add: star_abs_def Ifun_of_def star_of_def Ifun_star_n) |
309 by (simp add: star_abs_def Ifun_of_def star_of_def Ifun_star_n) |
583 |
310 |
584 subsection{*Existence of Infinite Hyperreal Number*} |
311 subsection{*Existence of Infinite Hyperreal Number*} |
585 (* |
312 |
586 lemma Rep_hypreal_omega: "Rep_hypreal(omega) \<in> hypreal" |
|
587 by (simp add: omega_def) |
|
588 *) |
|
589 text{*Existence of infinite number not corresponding to any real number. |
313 text{*Existence of infinite number not corresponding to any real number. |
590 Use assumption that member @{term FreeUltrafilterNat} is not finite.*} |
314 Use assumption that member @{term FreeUltrafilterNat} is not finite.*} |
591 |
315 |
592 |
316 |
593 text{*A few lemmas first*} |
317 text{*A few lemmas first*} |
684 val lemma_starrel_refl = thm "lemma_starrel_refl"; |
393 val lemma_starrel_refl = thm "lemma_starrel_refl"; |
685 val hypreal_empty_not_mem = thm "hypreal_empty_not_mem"; |
394 val hypreal_empty_not_mem = thm "hypreal_empty_not_mem"; |
686 val Rep_hypreal_nonempty = thm "Rep_hypreal_nonempty"; |
395 val Rep_hypreal_nonempty = thm "Rep_hypreal_nonempty"; |
687 val inj_hypreal_of_real = thm "inj_hypreal_of_real"; |
396 val inj_hypreal_of_real = thm "inj_hypreal_of_real"; |
688 val eq_Abs_star = thm "eq_Abs_star"; |
397 val eq_Abs_star = thm "eq_Abs_star"; |
689 (* val hypreal_minus_congruent = thm "hypreal_minus_congruent"; *) |
398 val star_n_minus = thm "star_n_minus"; |
690 val hypreal_minus = thm "hypreal_minus"; |
399 val star_n_add = thm "star_n_add"; |
691 val hypreal_add = thm "hypreal_add"; |
400 val star_n_diff = thm "star_n_diff"; |
692 val hypreal_diff = thm "hypreal_diff"; |
401 val star_n_mult = thm "star_n_mult"; |
693 val hypreal_add_commute = thm "hypreal_add_commute"; |
402 val star_n_inverse = thm "star_n_inverse"; |
694 val hypreal_add_assoc = thm "hypreal_add_assoc"; |
|
695 val hypreal_add_zero_left = thm "hypreal_add_zero_left"; |
|
696 val hypreal_add_zero_right = thm "hypreal_add_zero_right"; |
|
697 val hypreal_add_minus = thm "hypreal_add_minus"; |
|
698 val hypreal_add_minus_left = thm "hypreal_add_minus_left"; |
|
699 val hypreal_mult = thm "hypreal_mult"; |
|
700 val hypreal_mult_commute = thm "hypreal_mult_commute"; |
|
701 val hypreal_mult_assoc = thm "hypreal_mult_assoc"; |
|
702 val hypreal_mult_1 = thm "hypreal_mult_1"; |
|
703 val hypreal_zero_not_eq_one = thm "hypreal_zero_not_eq_one"; |
|
704 (* val hypreal_inverse_congruent = thm "hypreal_inverse_congruent"; *) |
|
705 val hypreal_inverse = thm "hypreal_inverse"; |
|
706 val hypreal_mult_inverse = thm "hypreal_mult_inverse"; |
|
707 val hypreal_mult_inverse_left = thm "hypreal_mult_inverse_left"; |
|
708 val hypreal_mult_left_cancel = thm "hypreal_mult_left_cancel"; |
403 val hypreal_mult_left_cancel = thm "hypreal_mult_left_cancel"; |
709 val hypreal_mult_right_cancel = thm "hypreal_mult_right_cancel"; |
404 val hypreal_mult_right_cancel = thm "hypreal_mult_right_cancel"; |
710 val hypreal_not_refl2 = thm "hypreal_not_refl2"; |
405 val hypreal_not_refl2 = thm "hypreal_not_refl2"; |
711 val hypreal_less = thm "hypreal_less"; |
406 val star_n_less = thm "star_n_less"; |
712 val hypreal_eq_minus_iff = thm "hypreal_eq_minus_iff"; |
407 val hypreal_eq_minus_iff = thm "hypreal_eq_minus_iff"; |
713 val hypreal_le = thm "hypreal_le"; |
408 val star_n_le = thm "star_n_le"; |
714 val hypreal_le_refl = thm "hypreal_le_refl"; |
409 val star_n_zero_num = thm "star_n_zero_num"; |
715 val hypreal_le_linear = thm "hypreal_le_linear"; |
410 val star_n_one_num = thm "star_n_one_num"; |
716 val hypreal_le_trans = thm "hypreal_le_trans"; |
|
717 val hypreal_le_anti_sym = thm "hypreal_le_anti_sym"; |
|
718 val hypreal_less_le = thm "hypreal_less_le"; |
|
719 val hypreal_of_real_add = thm "hypreal_of_real_add"; |
|
720 val hypreal_of_real_mult = thm "hypreal_of_real_mult"; |
|
721 val hypreal_of_real_less_iff = thm "hypreal_of_real_less_iff"; |
|
722 val hypreal_of_real_le_iff = thm "hypreal_of_real_le_iff"; |
|
723 val hypreal_of_real_eq_iff = thm "hypreal_of_real_eq_iff"; |
|
724 val hypreal_of_real_minus = thm "hypreal_of_real_minus"; |
|
725 val hypreal_of_real_one = thm "hypreal_of_real_one"; |
|
726 val hypreal_of_real_zero = thm "hypreal_of_real_zero"; |
|
727 val hypreal_of_real_inverse = thm "hypreal_of_real_inverse"; |
|
728 val hypreal_of_real_divide = thm "hypreal_of_real_divide"; |
|
729 val hypreal_zero_num = thm "hypreal_zero_num"; |
|
730 val hypreal_one_num = thm "hypreal_one_num"; |
|
731 val hypreal_omega_gt_zero = thm "hypreal_omega_gt_zero"; |
411 val hypreal_omega_gt_zero = thm "hypreal_omega_gt_zero"; |
732 |
412 |
733 (* val Rep_hypreal_omega = thm"Rep_hypreal_omega"; *) |
|
734 val lemma_omega_empty_singleton_disj = thm"lemma_omega_empty_singleton_disj"; |
413 val lemma_omega_empty_singleton_disj = thm"lemma_omega_empty_singleton_disj"; |
735 val lemma_finite_omega_set = thm"lemma_finite_omega_set"; |
414 val lemma_finite_omega_set = thm"lemma_finite_omega_set"; |
736 val not_ex_hypreal_of_real_eq_omega = thm"not_ex_hypreal_of_real_eq_omega"; |
415 val not_ex_hypreal_of_real_eq_omega = thm"not_ex_hypreal_of_real_eq_omega"; |
737 val hypreal_of_real_not_eq_omega = thm"hypreal_of_real_not_eq_omega"; |
416 val hypreal_of_real_not_eq_omega = thm"hypreal_of_real_not_eq_omega"; |
738 val not_ex_hypreal_of_real_eq_epsilon = thm"not_ex_hypreal_of_real_eq_epsilon"; |
417 val not_ex_hypreal_of_real_eq_epsilon = thm"not_ex_hypreal_of_real_eq_epsilon"; |