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

December 5, 2025
Liam O'Connor

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.

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

`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]