# Re: [isabelle] enumerating primes?

```Angeliki,

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