src/HOL/Complex/ex/NSPrimes.thy

new session Complex for the complex numbers

(*  Title       : NSPrimes.thy
    Author      : Jacques D. Fleuriot
    Copyright   : 2002 University of Edinburgh
    Description : The nonstandard primes as an extension of 
                  the prime numbers

These can be used to derive an alternative proof of the infinitude of primes by
considering a property of nonstandard sets.
*)

NSPrimes = Factorization + HSeries +

consts
  hdvd  :: [hypnat, hypnat] => bool       (infixl 50) 
  
defs
  hdvd_def "(M::hypnat) hdvd N ==
	           EX X Y. X: Rep_hypnat(M) & Y: Rep_hypnat(N) & 
                               {n::nat. X n dvd Y n} : FreeUltrafilterNat"

constdefs
  starprime :: hypnat set
  "starprime == ( *sNat* prime)"

constdefs
  choicefun :: 'a set => 'a
  "choicefun E == (@x. EX X: Pow(E) -{{}}. x : X)" 

consts injf_max :: "nat => ('a::{order} set) => 'a"  
primrec
  injf_max_zero "injf_max 0 E = choicefun E"
  injf_max_Suc  "injf_max (Suc n) E = choicefun({e. e : E & injf_max n E < e})"

end