src/HOL/Complex/ex/NSPrimes.thy
author paulson
Thu Jul 01 12:29:53 2004 +0200 (2004-07-01)
changeset 15013 34264f5e4691
parent 14051 4b61bbb0dcab
child 15093 49ede01e9ee6
permissions -rw-r--r--
new treatment of binary numerals
     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 
    11 NSPrimes = Factorization + Complex_Main +
    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