Def-fgl-thm
Prove a theorem using FGL
Def-fgl-thm is the main macro used for proving a theorem using FGL. It
produces a defthm form containing hints that cause the FGL clause
processor to be used to attempt the proof of the theorem. Basic usage is as
follows:
(def-fgl-thm <thmname>
<theorem-body>
<keyword-args>)
However, for backward compatibility with GL, the following usage is also supported:
(def-fgl-thm <thmname>
:hyp <hyp-term>
:concl <concl-term>
<keyword-args>)
The main keyword arguments supported include the fields of the fgl-config object, and a few others listed below. Each field of the
fgl-config object is assigned as follows:
- The explicit value given in the def-fgl-thm form, if there is one
- Else if the table fgl::fgl-config-table has an entry for the keyword field name, the value to which it is bound
- Else if the keyword field name is bound as a state global, its global value
- Else the default value defined by make-fgl-config.
The non-fgl-config keywords recognized are:
- :hyp and :concl, used with the backward-compatible usage form above
- :rule-classes, giving the rule classes of the theorem proved
- :hints, a list of subgoal or computed hints that are listed before the
FGL clause processor hints.
- :parents, :short, :long, the usual xdoc documentation
arguments. If any of these are provided, a defsection containing the
theorem is created, rather than just the theorem.
For now, other keyword arguments are accepted and ignored without complaint.
This probably will someday need to change.
Subtopics
- Fgl-config
- Config object for the FGL clause processor
