19 |
19 |
20 consts |
20 consts |
21 "1hn" :: hypnat ("1hn") |
21 "1hn" :: hypnat ("1hn") |
22 "whn" :: hypnat ("whn") |
22 "whn" :: hypnat ("whn") |
23 |
23 |
24 defs |
|
25 |
|
26 hypnat_zero_def "0 == Abs_hypnat(hypnatrel^^{%n::nat. 0})" |
|
27 hypnat_one_def "1hn == Abs_hypnat(hypnatrel^^{%n::nat. 1})" |
|
28 |
|
29 (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *) |
|
30 hypnat_omega_def "whn == Abs_hypnat(hypnatrel^^{%n::nat. n})" |
|
31 |
|
32 |
|
33 constdefs |
24 constdefs |
34 |
25 |
35 (* embedding the naturals in the hypernaturals *) |
26 (* embedding the naturals in the hypernaturals *) |
36 hypnat_of_nat :: nat => hypnat |
27 hypnat_of_nat :: nat => hypnat |
37 "hypnat_of_nat m == Abs_hypnat(hypnatrel^^{%n::nat. m})" |
28 "hypnat_of_nat m == Abs_hypnat(hypnatrel^^{%n::nat. m})" |
38 |
|
39 (* set of naturals embedded in the hypernaturals*) |
|
40 SHNat :: "hypnat set" |
|
41 "SHNat == {n. EX N. n = hypnat_of_nat N}" |
|
42 |
|
43 (* embedding the naturals in the hyperreals*) |
|
44 SNat :: "hypreal set" |
|
45 "SNat == {n. EX N. n = hypreal_of_nat N}" |
|
46 |
29 |
47 (* hypernaturals as members of the hyperreals; the set is defined as *) |
30 (* hypernaturals as members of the hyperreals; the set is defined as *) |
48 (* the nonstandard extension of set of naturals embedded in the reals *) |
31 (* the nonstandard extension of set of naturals embedded in the reals *) |
49 HNat :: "hypreal set" |
32 HNat :: "hypreal set" |
50 "HNat == *s* {n. EX no. n = real_of_nat no}" |
33 "HNat == *s* {n. EX no. n = real_of_nat no}" |
51 |
34 |
52 (* the set of infinite hypernatural numbers *) |
35 (* the set of infinite hypernatural numbers *) |
53 HNatInfinite :: "hypnat set" |
36 HNatInfinite :: "hypnat set" |
54 "HNatInfinite == {n. n ~: SHNat}" |
37 "HNatInfinite == {n. n ~: SNat}" |
55 |
38 |
56 (* explicit embedding of the hypernaturals in the hyperreals *) |
39 (* explicit embedding of the hypernaturals in the hyperreals *) |
57 hypreal_of_hypnat :: hypnat => hypreal |
40 hypreal_of_hypnat :: hypnat => hypreal |
58 "hypreal_of_hypnat N == Abs_hypreal(UN X: Rep_hypnat(N). |
41 "hypreal_of_hypnat N == Abs_hypreal(UN X: Rep_hypnat(N). |
59 hyprel^^{%n::nat. real_of_nat (X n)})" |
42 hyprel^^{%n::nat. real_of_nat (X n)})" |
60 |
43 |
61 defs |
44 defs |
|
45 |
|
46 (** the overloaded constant "SNat" **) |
|
47 |
|
48 (* set of naturals embedded in the hyperreals*) |
|
49 SNat_def "SNat == {n. EX N. n = hypreal_of_nat N}" |
|
50 |
|
51 (* set of naturals embedded in the hypernaturals*) |
|
52 SHNat_def "SNat == {n. EX N. n = hypnat_of_nat N}" |
|
53 |
|
54 (** hypernatural arithmetic **) |
|
55 |
|
56 hypnat_zero_def "0 == Abs_hypnat(hypnatrel^^{%n::nat. 0})" |
|
57 hypnat_one_def "1hn == Abs_hypnat(hypnatrel^^{%n::nat. 1})" |
|
58 |
|
59 (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *) |
|
60 hypnat_omega_def "whn == Abs_hypnat(hypnatrel^^{%n::nat. n})" |
|
61 |
62 hypnat_add_def |
62 hypnat_add_def |
63 "P + Q == Abs_hypnat(UN X:Rep_hypnat(P). UN Y:Rep_hypnat(Q). |
63 "P + Q == Abs_hypnat(UN X:Rep_hypnat(P). UN Y:Rep_hypnat(Q). |
64 hypnatrel^^{%n::nat. X n + Y n})" |
64 hypnatrel^^{%n::nat. X n + Y n})" |
65 |
65 |
66 hypnat_mult_def |
66 hypnat_mult_def |