Re: [isabelle] enumerating primes?


It is a bit hard to say what the best approach is for your use case.
Defining an ‘n-th prime’ function before you have even shown that there
are infinitely many of them (i.e. that there /is/ an n-th prime for
every n in the first place) is probably always going to involve
something like the "The" operator (unique choice) or its variant
"Least", and one can certainly do that, but it might get somewhat ugly.

Can you perhaps phrase your proof differently? E.g. something like ‘For
each prime number p, there exists a larger prime number p'’?

In the proof of this, you can, of course, refer to the prime numbers up
to p e.g. with {q. prime q ∧ q ≤ p}.


On 2018-05-08 16:34, Dr A. Koutsoukou-Argyraki wrote:
> 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,
> Angeliki

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