Re: [isabelle] enumerating primes?


maybe you could use a choice operator (THE or SOME), and define
something along the lines of:

nth_prime n == THE p. is_prime p & card { p'. p'<p & is_prime p' } = n

(I have no idea whether this is suited for your purpose)

Alternatively, a non-constructive inductive definition might be

p_0 = 1
p_(n+1) = LEAST p. is_prime p & p>p_n 


p_(n+1) = SOME p. is_prime p & p>p_n (may skip primes, but probably
enough to show infinitude)

Both definitions come with no further assumptions, however, in order to
show any interesting facts about them, you'll have to come up with a
large enough prime.

You would then prove "is_prime (p_n)" by induction on n,
in each step coming up with the next-larger prime.


On Di, 2018-05-08 at 15:34 +0100, 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.