[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,
Best wishes,

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.