Defexample
Tell witness-cp how to instantiate the free variables of definstantiate rules.
Example:
(defexample set-reasoning-member-template
:pattern (member-equal k y)
:templates (k)
:instance-rules (subsetp-equal-instancing
intersectp-equal-instancing
set-equiv-instancing
set-consp-instancing))
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)).
General form:
(defexample name
:pattern pattern
:templates templates
[:instance-rulename instance-rulename]
[:instance-rules instance-rules]
[:restriction restriction])
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.
Additional arguments:
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.
