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

December 3, 2025
Liam O'Connor

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.

inductive well :: ‹oots ⇒ bool› where ‹well Empty› | ‹n > 0 ⟹ well (ONEs n Empty)› | ‹n > 0 ⟹ well (TWOs n Empty)› | ‹n > 0 ⟹ well (ONEs m r) ⟹ well (TWOs n (ONEs m r))› | ‹n > 0 ⟹ well (TWOs m r) ⟹ well (ONEs n (TWOs m r))›

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

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