FREE-VARIABLES-TYPE-PRESCRIPTION

Major Section:  FREE-VARIABLES

We assume familiarity with the issue of dealing with free variables in hypotheses; see free-variables.

By default, starting with Version 4.3, ACL2 attempts all possible matches for free variables. Consider the following example.

(defstub f1 (x) t)
(defstub f2 (x y) t)
(defstub f3 (y) t)

(defaxiom f1-prop
  (implies (and (f2 x y) ; <-- y is free in this hypothesis
                (f3 y))
           (f1 x))       ; <-- (f1 x) is the type-term (type is `non-nil')
  :rule-classes :type-prescription)

; Succeeds:
(thm (implies (and (f2 a b)
                   (f3 b))
              (f1 a)))

; The following fails unless we try more than one match for free variables in
; hypotheses.
(thm (implies (and (f2 a b)
                   (f2 a c)
                   (f2 a d)
                   (f3 b))
              (f1 a)))

There may be times when you want to match only the first free variable. In that case, you can write a function of two arguments, the type-prescription rune being applied and the current ACL2 world, that prohibits multiple matching for those times. Your function is then `attached' to the built-in constrained function, oncep-ts. The following examples are intended to explain how this works.

First, let us disallow all mutliple matching of free variables (i.e., implement the behavior often referred to as ``:match-free :once''; see free-variables).

(defun oncep-tp-always (rune wrld)
  (declare (ignore rune wrld)
           (xargs :mode :logic :guard t))
  t)

(defattach oncep-tp oncep-tp-always)

Now suppose that instead, we want to disallow multiple matches for free variables in hypotheses of type-prescription rules except for the rule f1-prop above. With the following events, the second thm form above once again succeeds.

(defun oncep-tp-always-except-f1-prop (rune wrld)
  (declare (ignore wrld)
           (xargs :mode :logic :guard (and (consp rune)
                                           (consp (cdr rune))
                                           (symbolp (cadr rune)))))
  (not (eq (base-symbol rune) 'f1-prop)))

(defattach oncep-tp oncep-tp-always-except-f1-prop)

In general, your defattach event will attach a function symbol to oncep-tp. The guard of that function symbol must be implied by the tuard of oncep-tp:

ACL2 !>:args oncep-tp

Function         ONCEP-TP
Formals:         (RUNE WRLD)
Signature:       (ONCEP-TP * *)
                 => *
Guard:           (AND (PLIST-WORLDP WRLD)
                      (CONSP RUNE)
                      (CONSP (CDR RUNE))
                      (SYMBOLP (CADR RUNE)))
Guards Verified: T
Defun-Mode:      :logic
Type:            built-in (or unrestricted)

 ONCEP-TP
ACL2 !>