Safe vs Unsafe Rules [isa-002O]

December 5, 2025
Liam O'Connor

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.

Safe vs Unsafe Rules [isa-002O]

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