16 |
16 |
17 abbreviation |
17 abbreviation |
18 hypreal_of_real :: "real => real star" |
18 hypreal_of_real :: "real => real star" |
19 "hypreal_of_real == star_of" |
19 "hypreal_of_real == star_of" |
20 |
20 |
21 constdefs |
21 definition |
22 |
|
23 omega :: hypreal -- {*an infinite number @{text "= [<1,2,3,...>]"} *} |
22 omega :: hypreal -- {*an infinite number @{text "= [<1,2,3,...>]"} *} |
24 "omega == star_n (%n. real (Suc n))" |
23 "omega = star_n (%n. real (Suc n))" |
25 |
24 |
26 epsilon :: hypreal -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *} |
25 epsilon :: hypreal -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *} |
27 "epsilon == star_n (%n. inverse (real (Suc n)))" |
26 "epsilon = star_n (%n. inverse (real (Suc n)))" |
28 |
27 |
29 syntax (xsymbols) |
28 const_syntax (xsymbols) |
30 omega :: hypreal ("\<omega>") |
29 omega ("\<omega>") |
31 epsilon :: hypreal ("\<epsilon>") |
30 epsilon ("\<epsilon>") |
32 |
31 |
33 syntax (HTML output) |
32 const_syntax (HTML output) |
34 omega :: hypreal ("\<omega>") |
33 omega ("\<omega>") |
35 epsilon :: hypreal ("\<epsilon>") |
34 epsilon ("\<epsilon>") |
36 |
35 |
37 |
36 |
38 subsection{*Existence of Free Ultrafilter over the Naturals*} |
37 subsection{*Existence of Free Ultrafilter over the Naturals*} |
39 |
38 |
40 text{*Also, proof of various properties of @{term FreeUltrafilterNat}: |
39 text{*Also, proof of various properties of @{term FreeUltrafilterNat}: |
300 del: star_of_zero) |
299 del: star_of_zero) |
301 |
300 |
302 lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)" |
301 lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)" |
303 by (simp add: epsilon_def omega_def star_n_inverse) |
302 by (simp add: epsilon_def omega_def star_n_inverse) |
304 |
303 |
305 |
|
306 ML |
|
307 {* |
|
308 val omega_def = thm "omega_def"; |
|
309 val epsilon_def = thm "epsilon_def"; |
|
310 |
|
311 val FreeUltrafilterNat_Ex = thm "FreeUltrafilterNat_Ex"; |
|
312 val FreeUltrafilterNat_mem = thm "FreeUltrafilterNat_mem"; |
|
313 val FreeUltrafilterNat_finite = thm "FreeUltrafilterNat_finite"; |
|
314 val FreeUltrafilterNat_not_finite = thm "FreeUltrafilterNat_not_finite"; |
|
315 val FreeUltrafilterNat_empty = thm "FreeUltrafilterNat_empty"; |
|
316 val FreeUltrafilterNat_Int = thm "FreeUltrafilterNat_Int"; |
|
317 val FreeUltrafilterNat_subset = thm "FreeUltrafilterNat_subset"; |
|
318 val FreeUltrafilterNat_Compl = thm "FreeUltrafilterNat_Compl"; |
|
319 val FreeUltrafilterNat_Compl_mem = thm "FreeUltrafilterNat_Compl_mem"; |
|
320 val FreeUltrafilterNat_Compl_iff1 = thm "FreeUltrafilterNat_Compl_iff1"; |
|
321 val FreeUltrafilterNat_Compl_iff2 = thm "FreeUltrafilterNat_Compl_iff2"; |
|
322 val FreeUltrafilterNat_UNIV = thm "FreeUltrafilterNat_UNIV"; |
|
323 val FreeUltrafilterNat_Nat_set_refl = thm "FreeUltrafilterNat_Nat_set_refl"; |
|
324 val FreeUltrafilterNat_P = thm "FreeUltrafilterNat_P"; |
|
325 val FreeUltrafilterNat_Ex_P = thm "FreeUltrafilterNat_Ex_P"; |
|
326 val FreeUltrafilterNat_all = thm "FreeUltrafilterNat_all"; |
|
327 val FreeUltrafilterNat_Un = thm "FreeUltrafilterNat_Un"; |
|
328 val starrel_iff = thm "starrel_iff"; |
|
329 val starrel_in_hypreal = thm "starrel_in_hypreal"; |
|
330 val Abs_star_inverse = thm "Abs_star_inverse"; |
|
331 val lemma_starrel_refl = thm "lemma_starrel_refl"; |
|
332 val hypreal_empty_not_mem = thm "hypreal_empty_not_mem"; |
|
333 val Rep_hypreal_nonempty = thm "Rep_hypreal_nonempty"; |
|
334 val inj_hypreal_of_real = thm "inj_hypreal_of_real"; |
|
335 (* val eq_Abs_star = thm "eq_Abs_star"; *) |
|
336 val star_n_minus = thm "star_n_minus"; |
|
337 val star_n_add = thm "star_n_add"; |
|
338 val star_n_diff = thm "star_n_diff"; |
|
339 val star_n_mult = thm "star_n_mult"; |
|
340 val star_n_inverse = thm "star_n_inverse"; |
|
341 val hypreal_mult_left_cancel = thm "hypreal_mult_left_cancel"; |
|
342 val hypreal_mult_right_cancel = thm "hypreal_mult_right_cancel"; |
|
343 val hypreal_not_refl2 = thm "hypreal_not_refl2"; |
|
344 val star_n_less = thm "star_n_less"; |
|
345 val hypreal_eq_minus_iff = thm "hypreal_eq_minus_iff"; |
|
346 val star_n_le = thm "star_n_le"; |
|
347 val star_n_zero_num = thm "star_n_zero_num"; |
|
348 val star_n_one_num = thm "star_n_one_num"; |
|
349 val hypreal_omega_gt_zero = thm "hypreal_omega_gt_zero"; |
|
350 |
|
351 val lemma_omega_empty_singleton_disj = thm"lemma_omega_empty_singleton_disj"; |
|
352 val lemma_finite_omega_set = thm"lemma_finite_omega_set"; |
|
353 val not_ex_hypreal_of_real_eq_omega = thm"not_ex_hypreal_of_real_eq_omega"; |
|
354 val hypreal_of_real_not_eq_omega = thm"hypreal_of_real_not_eq_omega"; |
|
355 val not_ex_hypreal_of_real_eq_epsilon = thm"not_ex_hypreal_of_real_eq_epsilon"; |
|
356 val hypreal_of_real_not_eq_epsilon = thm"hypreal_of_real_not_eq_epsilon"; |
|
357 val hypreal_epsilon_not_zero = thm"hypreal_epsilon_not_zero"; |
|
358 val hypreal_epsilon_inverse_omega = thm"hypreal_epsilon_inverse_omega"; |
|
359 *} |
|
360 |
|
361 end |
304 end |