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.

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.

We define well, an inductive wellformedness predicate for oots sequences, that state there are no segments of zero length, and that no two adjacent segments have the same oot value.

Some methods (like erule when there are multiple matching assumptions) are nondeterministic, producing multiple alternative proof states.

The back command interactively explores a different alternative branch produced by the previous step.

This is useful for interactive exploration, but is very brittle and considered poor style.

Instead, we can combine methods with the comma operator ,: The command apply (m1, m2) first runs m1, and then runs m2, accepting only the nondeterministic branches where the second method m2 succeeds. This avoids the need for back:

For a method m:

Repeatedly applies the m as many times as possible until it fails. It stops automatically when m can no longer make progress; and does not backtrack.

By default, structural induction induct t produces an induction hypothesis for the variables directly mentioned in t, and rule induction induct rule: p.induct produces a hypothesis for the variables directly mentioned by the eliminated p assumption.

Sometimes you need a stronger hypothesis that generalises across additional variables in the goal. The arbitrary option tells the induct method to generalise certain variables, so the induction hypothesis assumes the property holds for all values of those variables.

blast is a method for automatic classical first-order reasoning, based on a tableaux prover. apply blast attempts a thorough search using sets of intro and elim rules. Like simp, rules can be annotated with [intro] and [elim] annotations, or they can be passed locally to blast (i.e. apply (blast intro: nandI1 nandI2 elim: nandE))

The methods fast, slow, and best use a different classical proof search engine than blast, each with a different proof search strategy. fast performs a quick, depth-bounded search, and is generally faster. slow is a more exhaustive search and more backtracking, and best performs a best-first search strategy using a heuristic based on the size of the goal. In general, if fast or blast can solve your goal, it will be the most efficient at solving it, whereas slow and best are only used if no other automated technique works.

Rules such as conjI, impI, or disjE that cannot change a provable goal into unprovable goal(s) are called safe. Isabelle's automation strategies like safe rules because they can apply them without fear, or the need for backtracking. You can mark a rule as safe by marking it [intro!] or [elim!]. This can also be done locally when invoking methods like blast, fast, slow, and best.

The method safe applies only safe rules to the current goal. The method clarify is similar, but it only applies safe rules that do not split the goal into multiple subgoals. Like blast etc., rules can be added to these methods with intro!: etc.

clarsimp the combination of clarify and simp, and is very useful when doing exploratory proving. slowsimp is the combination of slow and simp. bestsimp is the combination of best and simp. The combination of fast and simp is, for inexplicable reasons, called fastforce.

force is a very thorough proof search that can often solve goals other methods can't. It can be thought of as a very thorough version of blast combined with simp. The method auto, by contrast, is a more lightweight search that attempts to simulateneously solve all goals, rather than just the first one. Unlike the other automated methods, auto will leave behind goals that it is unable to prove.

Because the behaviour of auto differs greatly between Isabelle versions and is very sensitive to what theories are loaded, it's considered bad style to use auto as anything but the final step in a proof, but it can nonetheless be useful to see what goals auto outputs to see where it's getting stuck.

Isabelle includes a feature called the sledgehammer that invokes external proof search procedures (such as SMT solvers) and provides them with lemmas that appear to be relevant. If the tools find a proof, it can often replay them in Isabelle's proof kernel, giving an Isabelle proof that matches what the external proof tool found.

To invoke this procedure on a goal, searching automatically for related lemmas, type the word try in an open subgoal.