Matching for free variable in type-prescription rules
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,
First, let us disallow all multiple 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-system 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
(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-system oncep-tp oncep-tp-always-except-f1-prop)