Re: [isabelle] enumerating primes?

On 05/08/2018 04:34 PM, 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?

Hi Angeliki,

a (constructive) proof of the existence of infinitely many primes can e.g. be found in the paper

  "A comparison of the mathematical proof languages Mizar and Isar"

by Markus Wenzel and Freek Wiedijk. You can find a formalization of this proof in section 7 of the

together with an explanation of how a program can be extracted from this proof.


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