Proof Method. `force` and `auto` [isa-002S]

December 5, 2025
Liam O'Connor

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.

Proof Method. `force` and `auto` [isa-002S]

`inductive` predicates [isa-0028]

Example. Even numbers as an `inductive` [isa-002K]

Proof Method. `induct` (for rule induction) [isa-0029]

Exercise. Even numbers are multiples of two [isa-002L]

Solution.

Example. Wellformedness for `oots` [isa-002A]

Theorem. `compress_expand` [isa-002B]

Solution.

Definition. List subsequence relation [isa-002C]

Theorem. Reflexivity of `subsequence` [isa-002D]

Solution.

Theorem. Length of `subsequence` [isa-002E]

Solution.

Controlling backtracking, chaining methods with comma [isa-002F]

Repeating methods with `+` [isa-002G]

Theorem. Antisymmetry of `subsequence` [isa-002H]

Solution.

Generalising the induction hypothesis with `arbitrary` [isa-002I]

Example. Inequality as an `inductive` [isa-002M]

Theorem. Transitivity of `subsequence` [isa-002J]

Solution.

Proof Method. `blast`, `fast`, `slow`, and `best` [isa-002P]

Safe vs Unsafe Rules [isa-002O]

Proof Method. `safe` and `clarify` [isa-002Q]

Proof Method. `clarsimp`, `slowsimp`, `bestsimp` and `fastforce` [isa-002R]

Proof Method. `force` and `auto` [isa-002S]

`try` and the famous Isabelle sledgehammer. [isa-002T]

Example. Simplifier rules for `nand` [isa-001I]

Problem.