inductive predicates [isa-0028]

With the inductive command, we define a predicate by specifying a collection of inference rules, and the inductive predicate is the smallest predicate closed under those rules.

In other words: An element satisfies the predicate exactly if it can be derived using the given rules.

From the given rules, Isabelle automatically generates an induction principle (.induct) which can be used with the induct method (see Proof Method [isa-0029]) and a cases theorem (.cases) for use with the case_tac method.