Tell witness-cp how to instantiate the free variables of definstantiate rules.
:pattern (member-equal k y)
Instructs witness-cp to find terms of the form (member-equal k y)
throughout the clause, and for each such k, for any match of one of the
instance-rules listed, add an instance using that k.
For example, if we have a hypothesis (subsetp-equal a b) and terms
are present somewhere in the clause, then this rule, along with the
subsetp-equal-instancing rule described in definstantiate, will
cause the following hyps to be added:
(implies (member-equal (foo x) a)
(member-equal (bar x) a))
(implies (member-equal q a)
(member-equal q b)).
The name of the rule can be used in Witness Rulesets; see def-witness-ruleset.
When witness-cp is given a Witness Ruleset that includes name,
and it has already found matches for one of these instance-rules, it then
it will look through the clause for terms matching pattern, and use the
corresponding pattern in place of the vars in the definstantiate rules.
The instance-rulename can be used, instead of instance-rules, when
there is only a single rule. BOZO we should deprecate this.
You can syntactically restrict the use of defexample forms by giving a
restriction. The restriction may have free variables that occur also
in the pattern, as well as acl2::world, standing for the ACL2 world.
If a restriction is given, then this example will only be used if it
evaluates to a non-nil value.