# Pointerp

Recognizer for `pointer`.

Since our pointers are opaque,
we introduce their recognizer as a constrained function.

We constrain the recognizer to return a boolean.
We also indirectly constrain it
to hold over an infinite number of values,
by simultaneously introducing a constrained function
that, given any list as input, returns a pointer that is not in the list.
The list may include non-ponters, which are ignored.

This new-pointer function implies the infinity of pointers because
starting from the empty list nil
we can obtain an initial pointer p0,
then given the singleton list (p0)
we can obtain a different pointer p1,
then given the list (p0 p1)
we can obtain yet a different pointer p2,
and so on.
In other words, we can ``count'' pointers.

The -raw suffix in the name of the constrained new-pointer function
is because the rest of our formalization
actually uses a wrapper function (without the suffix),
defined later with a `pointer-listp` guard,
where the latter recognizer is not yet available here.

We use natural numbers as witnesses for pointers.
The new-pointer function returns a natural number
larger than all the ones that occur in the argument list.

**Definition: **pointerp

(encapsulate (((pointerp *) => *)
((new-pointer-raw *) => *))
(local (value-triple :elided))
(defrule booleanp-of-pointerp
(booleanp (pointerp x))
:rule-classes (:rewrite :type-prescription))
(local (value-triple :elided))
(defrule pointerp-of-new-pointer-raw
(pointerp (new-pointer-raw list)))
(defrule new-pointer-raw-is-new
(not (member-equal (new-pointer-raw list)
list))
:use (:instance lemma (elem (new-pointer-raw list)))
:prep-lemmas ((defruled lemma
(implies (and (natp elem)
(member-equal elem list))
(> (new-pointer-raw list) elem))))))

### Definitions and Theorems

**Theorem: **booleanp-of-pointerp

(defthm booleanp-of-pointerp
(booleanp (pointerp x))
:rule-classes (:rewrite :type-prescription))

**Theorem: **pointerp-of-new-pointer-raw

(defthm pointerp-of-new-pointer-raw
(pointerp (new-pointer-raw list)))

**Theorem: **new-pointer-raw-is-new

(defthm new-pointer-raw-is-new
(not (member-equal (new-pointer-raw list)
list)))