		Search-engine friendly clone of the ACL2 documentation.

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