Proof Method. induct (for rule induction) [isa-0029]
You’ve already seen how to use induct for structural induction. Exactly the same induct method can also be used for rule induction, when your induction is over an inductively defined predicate, not over the structure of some datatype.
When you define a predicate p with the inductive command, Isabelle automatically produces an induction rule named p.induct. This rule expresses how to perform induction over derivations of p x, one case for each introduction rule of the predicate.
Although you could apply the raw rule with rule or erule, it is almost always easier to use:
This behaves just like structural induction: The goal is split into one subgoal per introduction rule of the predicate, and recursive premises of the rules give rise to induction hypotheses, added to your assumptions.