[isabelle] enumerating primes?
Dear Isabelle users,
I need a definition of a function taking a natural n as an input and
returning the nth prime number.
But: I don't want an inductive definition because in my proof I don't
want to imply the assumption that primes are infinitely many.
Is anyone aware of such a definition?
(my goal is to give a proof of the infinitude of primes: to this end I
want to show that assuming we have r many prime numbers, I can always
construct a prime that is bigger than p_r )
Many thanks in advance,
This archive was generated by a fusion of
Pipermail (Mailman edition) and