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
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.
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and