Consideration
An object indicating that some instantiation is relevant.
Considerations are the objects one provides as part of
:consider hints. The most convenient form of a consideration is
simply the name of a lemma. The system will then search for a relevant
instantiation of the left-hand side of the conclusion of that lemma inside the
specified goal clause, starting with the last literal. The system uses a
heuristically modified version of the Huet-Lang second-order pattern matching
algorithm and, in general, produces instantiations of both variable symbols and
constrained function symbols in the lemma. If an instance is found, the
consideration is turned into a lemma-instance and :used.
For example, suppose the following theorem has been proved:
(defthm map-h-append
(implies (and (true-listp x)
(true-listp y))
(equal (map-h-append (append x y))
(append (map-h x) (map-h y))))
:rule-classes nil)
and suppose map-h is a defined function involving some constrained
function symbol h. Then the consideration map-h-append attached to a
clause identifier will cause the system to find the identified clause and
search through it for an instance and/or functional instance of
(map-h-append (append x y)) and to add that (functional) instance as a
hypothesis when it finds it. If no instance is found, an error is signaled.
The more elaborate form of a consideration allows you to specify what is used
as the pattern and where that pattern is searched for in the clause.
The most general form of a consideration is
(name
:pattern pterm ; term or :lhs
:target tterm ; term or :conclusion or :clause
:instance vsubst ; variable substitution
:functional-instance fsubst) ; functional substitution
where name is the name of a previously proved theorem, pterm is
either a term or the keyword :lhs, tterm is either a term or the
keyword conclusion or the keyword :clause, vsubst is a variable
substitution as might be given in an :instance, e.g., ((x (rev
a)) (y (sort b))), and fsubst is a functional substitution as might be
given in a :functional-instance, e.g., ((map-h sumer)).
If pterm is a term, that term is used as the pattern we try to
instantiate. If pterm is the keyword :lhs, the left-hand side of the
conclusion of name is used as the pattern. If no :pattern is
specified, :lhs is used by default.
If tterm is a term, that term is matched against the pattern to
generate the instantiation. If tterm is :conclusion, a match of the
pattern is searched for in the conclusion of the specified subgoal clause. If
tterm is :clause, a match of the pattern is searched for in the
entire subgoal clause, starting with the conclusion and searching backwards
toward the first hypothesis. The search is outer-most first, left-to-right
recursive descent. The first subterm of the target producing a match of the
pattern stops the search and generates the instantiation. Note that if
tterm is given explicitly, no search occurs. Note also that because we
cannot do the search until we know what the subgoal clause is, the work for
this hint -- the Huet-Lang second-order matching algorithm -- cannot commence
until the indicated subgoal arises.
The substitutions produced by second-order matching are what we called
``mixed substitutions'' by which we mean a given substitution will substitute
both for variable symbols and hereditarily constrained function symbols. The
effect, however, is the same as
(:INSTANCE (:FUNCTIONAL-INSTANCE name (fn1 (lambda ...)) ...)
(var1 term1)
...).
Second-order matching typically produces a plethora of such substitutions.
We rule many out on heuristic grounds. Thus, our heuristic modification of the
Huet-Lang algorithm makes it incomplete. Still, it is typical for a lot of
substitutions to be found and the system selects some to pursue in an
DISJUNCTIVE way. That is, it takes each of the ``winning'' substitutions and
generates a :use hint for each of them separately to see if any one of
them will prove the indicated subgoal.
It is frequently necessary to give the matcher a ``hint'' to limit its
consideration of all possible substitutions. The vsubst and fsubst
are treated as ``seed'' substitutions. Any computed instance is an extension
of the two seeds. That is, the variable pairs in the mixed substitutions
extend vsubst and the functional pairs in the mixed substitutions extend
fsubst. Both vsubst and fsubst default to nil.
