### FREE-VARIABLES-TYPE-PRESCRIPTION

matching for free variable in type-prescription rules
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)

The second `thm`

form above will now fail, because only one free-variable
match is permitted for the first hypothesis of rule `f1-prop`

above.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 !>