*To*: "Dr A. Koutsoukou-Argyraki" <ak2110 at cam.ac.uk>*Subject*: Re: [isabelle] enumerating primes?*From*: David Cock <david.cock at inf.ethz.ch>*Date*: Tue, 8 May 2018 22:00:54 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <11e2e8b6909a1650b3210293a34e902b@cam.ac.uk>*References*: <d0832e5cd7d537ccd3e125943c779f03@cam.ac.uk> <f4a8bbf2-9118-3616-1a03-4baec66bd809@inf.ethz.ch> <11e2e8b6909a1650b3210293a34e902b@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.7.0

On 08/05/18 18:13, Dr A. Koutsoukou-Argyraki wrote:

On 2018-05-08 15:50, David Cock wrote:Whether or not the definition is inductive doesn't affect the end function. From the existence of any function "N -> Nth prime", one can trivially show the infinitude of primes from the infinitude of the natural numbers. Indeed, that such a function exists at all *is* a proof that there are infinitely many primes.indeed- so let me rephrase my question: I should have written that Iwant this enumerating function to be defined only on a segment of thenaturals, i.e. up to some r \in nat , having assumed that there existr many primes

David

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

**Re: [isabelle] enumerating primes?***From:*David Cock

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

- Previous by Date: Re: [isabelle] enumerating primes?
- Next by Date: Re: [isabelle] Code generation in the AFP
- Previous by Thread: Re: [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