Def-fgl-param-thm
Prove a theorem using FGL with case-splitting.
Def-fgl-param-thm is similar to def-fgl-thm, but runs a clause
processor prior to FGL that splits the goal into several cases based on the
provided arguments. It somewhat replicates the behavior of ACL2::def-gl-param-thm, but ignores the shape specifiers provided for the
various cases.
The usage of def-fgl-param-thm is similar to that of def-fgl-thm, but it accepts several more keyword arguments:
- :param-bindings is the same as in ACL2::def-gl-param-thm, but
the shape specifier alist in each entry is ignored.
- :param-hyp is the same as in ACL2::def-gl-param-thm.
- :split-params provides the fgl-sat-check parameters object for
proving that case split provided covers all cases.
- :solve-params provides the fgl-sat-check object for proving each case.
- :repeat-concl controls whether the conclusion is (if nil)
rewritten/symbolically executed once and then solved separately for each case,
or (if nonnil) rewritten/symbolically executed (and also solved) separately for
each case.
- :hints gives a list of hints (computed or subgoal) that are provided
before the casesplit and FGL interpreter clause processor hints. Practically
speaking, if these hints don't trigger immediately, then they won't trigger
until after the casesplit and FGL interpreter hints, since those occur
unconditionally.
- :split-concl pertains to cases where previous hints have allowed ACL2
to clausify the conjecture -- normally, the case split happens on the original,
unclausified conjecture. If :split-concl is non-nil (the default), then
the last literal in the clause is considered the conclusion and previous
literals are bundled into the hypothesis; if nil, then the whole clause is
bundled into the conclusion and the hyp is just T.
