Defthm<w
Attempt to prove a theorem directly from previously-proved theorems.
The macro defthm<w takes the same arguments as defthm:
a name, a form, and (optional) keyword arguments. It also takes one additional
keyword argument, :prove, discussed below.
General Form:
(defthm<w name form
:prove p ; default :when-hints
:rule-classes rule-classes
:instructions instructions
:hints hints
:otf-flg otf-flg)
More examples may be found in the community-book,
kestrel/utilities/auto-instance-tests.lisp.
The name ``defthm<w'' is intended to suggest using the world (w) to do
the proof: ``Prove this using input from the logical world.''
Example Form:
; Prove car-cons by appealing to an already-proved theorem, car-cons:
(defthm<w my-car-cons
(equal (first (cons a b)) a))
The world is searched for previous theorems that, together, trivially imply
the given form. If such theorems are found, then a defthm event is
generated for the given form, with the given keyword arguments except for
:prove and also excepting :hints: rather, a value for :hints is generated that reference those previous theorems and that only allow
simplification in proofs of the subsequent goals, if any (so for example, not
destructor elimination or induction). In this case, the supplied value of
:hints (if any) is ignored. Also see previous-subsumer-hints
for documentation of the utility that generates the hints.
The behavior described above takes place with the default value of the
keyword argument, :prove, which is :when-hints. With this default,
a call of defthm<w fails when suitable hints fail to be generated. The
other two legal values for :prove are nil and t. With
:prove nil, no proof is attempted: instead, the event (value-triple
h) is generated, where h is the generated hints; note that h is
nil when hints fail to be generated. With :prove t, the proof is
attempted even when no hints are generated; in that case, if :hints are
supplied then they are used.
Note: This utility searches for previous defthm and defaxiom events (including, of course, defthm events generated
from macros such as defrule). In particular, it does not search for
corollaries, termination or guard theorems, or defchoose
axioms.
Subtopics
- Previous-subsumer-hints
- Hints to prove a theorem directly from previously-proved theorems.
- Thm<w
- Attempt to prove a theorem directly from previously-proved theorems.
- Defthmd<w
- Attempt to prove a theorem directly from previously-proved theorems.
