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 ``
(defun oncep-tp-always (rune wrld) (declare (ignore rune wrld) (xargs :mode :logic :guard t)) t) (defattach oncep-tp oncep-tp-always)The second
thmform above will now fail, because only one free-variable match is permitted for the first hypothesis of rule
Now suppose that instead, we want to disallow multiple matches for free variables
in hypotheses of type-prescription rules except for the rule
above. With the following events, the second
thm form above once again
(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
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 !>