*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] enumerating primes?*From*: David Cock <david.cock at inf.ethz.ch>*Date*: Tue, 8 May 2018 16:50:52 +0200*In-reply-to*: <d0832e5cd7d537ccd3e125943c779f03@cam.ac.uk>*References*: <d0832e5cd7d537ccd3e125943c779f03@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.7.0

Angeliki,

David On 08/05/18 16:34, Dr A. Koutsoukou-Argyraki wrote:

Dear Isabelle users,I need a definition of a function taking a natural n as an input andreturning the nth prime number.But: I don't want an inductive definition because in my proof I don'twant 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 Iwant to show that assuming we have r many prime numbers, I can alwaysconstruct a prime that is bigger than p_r )Many thanks in advance, Best wishes, Angeliki

**Follow-Ups**:**Re: [isabelle] enumerating primes?***From:*Dr A. Koutsoukou-Argyraki

**References**:**[isabelle] enumerating primes?***From:*Dr A. Koutsoukou-Argyraki

- Previous by Date: [isabelle] enumerating primes?
- Next by Date: Re: [isabelle] enumerating primes?
- Previous by Thread: [isabelle] enumerating primes?
- Next by Thread: Re: [isabelle] enumerating primes?
- Cl-isabelle-users May 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list