Otf-flg
Allow more than one initial subgoal to be pushed for induction
This keyword argument for certain events controls whether
the theorem prover will abandon its initial work upon encountering the second
subgoal to push for proof by induction: :otf-flg is nil for that
behavior, but t if it should instead continue “Onward Through the
Fog” and complete waterfall processing before starting any proof
by induction.
The default value for :otf-flg is nil except during processing of
defun events, where the default is t for both termination and
guard proofs (see defun). Note that the default for
:otf-flg is thus t for processing verify-termination events,
since they abbreviate defun events. However, the default for
:otf-flg is nil for processing verify-guards events.
Further Explanation
Suppose you submit a conjecture to the theorem prover and the system splits
it up into many subgoals. Any subgoal not proved by other methods is
eventually set aside for an attempted induction proof. But upon setting aside
the second such subgoal, the system chickens out and decides that rather than
prove n>1 subgoals inductively, it will abandon its initial work and
attempt induction on the originally submitted conjecture. The :otf-flg
(Onward Thru the Fog) allows you to override this chickening out. When
:otf-flg is t, the system will push all the initial subgoals and
proceed to try to prove each, independently, by induction.
Even when you don't expect induction to be used or to succeed, setting the
:otf-flg is a good way to force the system to generate and display all
the initial subgoals.
For defthm and thm, :otf-flg is a keyword argument
that is a peer to :rule-classes and :hints. It may
be supplied as in the following examples; also see defthm.
(thm (my-predicate x y) :rule-classes nil :otf-flg t)
(defthm append-assoc
(equal (append (append x y) z)
(append x (append y z)))
:hints (("Goal" :induct t))
:otf-flg t)
The :otf-flg may be supplied to defun via the xargs
declare option. When you supply an :otf-flg hint to defun, the flag
is effective for the termination proofs and the guard proofs, if any.
