Implementation of defisar.
The implementation functions have arguments and results
consistently named as follows
(unless otherwise stated, explicitly or implicitly,
in the functions):
- state is the ACL2 state.
- ctx is the context used for errors.
- name is the homonymous input to the event macro.
- formula is the homonymous input to the event macro.
- proof is the homonymous input to the event macro.
- disable is the homonymous input to the event macro.
- rule-classes is the homonymous input to the event macro.
- hyps is the list of hypotheses of formula.
- concl is the conclusion of formula
- facts is an alist from keyword that identify facts
to information about those facts.
- bindings is an alist from variable symbols to formulas,
corresponding to the :let bindings.
Implementation functions' arguments and results
that are not listed above
are described in, or clear from,
those functions' documentation.
- Recognize alists from keywords to fact information.
- Execute an :assume command.
- Execute a :derive command.
- Execute a sequence of commands.
- Recognize information about facts.
- Execute the :qed command.
- Execute a :let command.
- Generate the hypotheses for the theorem generated for
a :derive command.
- Execute a proof.
- Recognize lists of information about facts.
- Generate and submit the defisar events.
- Lift fact-info->thm-name to lists.
- Decompose the input formula into hypotheses and conclusion.
- Synonym of defisar in the "ACL2" package.
- Definition of the defisar macro.