13957
|
1 |
(* Title : NSPrimes.thy
|
|
2 |
Author : Jacques D. Fleuriot
|
|
3 |
Copyright : 2002 University of Edinburgh
|
|
4 |
Description : The nonstandard primes as an extension of
|
|
5 |
the prime numbers
|
|
6 |
|
|
7 |
These can be used to derive an alternative proof of the infinitude of primes by
|
|
8 |
considering a property of nonstandard sets.
|
|
9 |
*)
|
|
10 |
|
14051
|
11 |
NSPrimes = Factorization + Complex_Main +
|
13957
|
12 |
|
|
13 |
consts
|
|
14 |
hdvd :: [hypnat, hypnat] => bool (infixl 50)
|
|
15 |
|
|
16 |
defs
|
|
17 |
hdvd_def "(M::hypnat) hdvd N ==
|
|
18 |
EX X Y. X: Rep_hypnat(M) & Y: Rep_hypnat(N) &
|
|
19 |
{n::nat. X n dvd Y n} : FreeUltrafilterNat"
|
|
20 |
|
|
21 |
constdefs
|
|
22 |
starprime :: hypnat set
|
|
23 |
"starprime == ( *sNat* prime)"
|
|
24 |
|
|
25 |
constdefs
|
|
26 |
choicefun :: 'a set => 'a
|
|
27 |
"choicefun E == (@x. EX X: Pow(E) -{{}}. x : X)"
|
|
28 |
|
|
29 |
consts injf_max :: "nat => ('a::{order} set) => 'a"
|
|
30 |
primrec
|
|
31 |
injf_max_zero "injf_max 0 E = choicefun E"
|
|
32 |
injf_max_Suc "injf_max (Suc n) E = choicefun({e. e : E & injf_max n E < e})"
|
|
33 |
|
|
34 |
end
|
|
35 |
|
|
36 |
|