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