generate subgoals using induction
Major Section: PROOF-CHECKER-COMMANDS
Examples: induct, (induct t) -- induct according to a heuristically-chosen scheme, creating a new subgoal for each base and induction step (induct (append (reverse x) y)) -- as above, but choose an induction scheme based on the term (append (reverse x) y) rather than on the current goal General Form: (induct &optional term)Induct as in the corresponding
:inducthint given to the theorem prover, creating new subgoals for the base and induction steps. If term is
tor is not supplied, then use the current goal to determine the induction scheme; otherwise, use that term.
Remark: As usual, abbreviations are allowed in the term.
Induct actually calls the
prove command with all
processes turned off. Thus, you must be at top of the goal for an