equal
deleted
inserted
replaced
13 {n::nat. X(n) = Y(n)} : FreeUltrafilterNat}" |
13 {n::nat. X(n) = Y(n)} : FreeUltrafilterNat}" |
14 |
14 |
15 typedef hypnat = "UNIV//hypnatrel" (Equiv.quotient_def) |
15 typedef hypnat = "UNIV//hypnatrel" (Equiv.quotient_def) |
16 |
16 |
17 instance |
17 instance |
18 hypnat :: {ord,zero,plus,times,minus} |
18 hypnat :: {ord, zero, one, plus, times, minus} |
19 |
19 |
20 consts |
20 consts |
21 "1hn" :: hypnat ("1hn") |
|
22 "whn" :: hypnat ("whn") |
21 "whn" :: hypnat ("whn") |
23 |
22 |
24 constdefs |
23 constdefs |
25 |
24 |
26 (* embedding the naturals in the hypernaturals *) |
25 (* embedding the naturals in the hypernaturals *) |
52 SHNat_def "Nats == {n. EX N. n = hypnat_of_nat N}" |
51 SHNat_def "Nats == {n. EX N. n = hypnat_of_nat N}" |
53 |
52 |
54 (** hypernatural arithmetic **) |
53 (** hypernatural arithmetic **) |
55 |
54 |
56 hypnat_zero_def "0 == Abs_hypnat(hypnatrel``{%n::nat. 0})" |
55 hypnat_zero_def "0 == Abs_hypnat(hypnatrel``{%n::nat. 0})" |
57 hypnat_one_def "1hn == Abs_hypnat(hypnatrel``{%n::nat. 1})" |
56 hypnat_one_def "1 == Abs_hypnat(hypnatrel``{%n::nat. 1})" |
58 |
57 |
59 (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *) |
58 (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *) |
60 hypnat_omega_def "whn == Abs_hypnat(hypnatrel``{%n::nat. n})" |
59 hypnat_omega_def "whn == Abs_hypnat(hypnatrel``{%n::nat. n})" |
61 |
60 |
62 hypnat_add_def |
61 hypnat_add_def |