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"
  http://www21.in.tum.de/~wenzelm/papers/romantic.pdf

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

  http://isabelle.in.tum.de/dist/library/HOL/HOL-Proofs-Extraction/document.pdf

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

Greetings,
Stefan




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