Re: [isabelle] enumerating primes?



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 I want this enumerating function to be defined only on a segment of the naturals, i.e. up to some r \in nat , having assumed that there exist r many primes


  The textbook proof of this should be possible in HOL, if you really
want to avoid defining a function.  There's nothing special about
inductive functions in HOL, they just happen to be defined as the LFP
of a set of recurrent equations.  They're logically exactly equivalent
to any other function.

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 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.