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
However, for backward compatibility with GL, the following usage is also supported:
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.
- Config object for the FGL clause processor