Writing Isabelle proofs
Contract
| Field |
Bound contract |
| Trigger |
The task is to write, review, or maintain Isabelle/HOL proofs, to drive Sledgehammer against a goal, or to build on an AFP entry. Methodology stays with proof-driven. |
| Authority |
Reversible local: writes only theory files, session ROOT files, and Isabelle configuration inside the target project; rollback is version control. No remote mutation. |
| Side effect |
Local writes to .thy sources, ROOT session definitions, and the AFP checkout already on disk. No remote mutation. |
| Done |
isabelle build of the session succeeds, no sorry remains, and no axiomatization enters the delivered diff. |
Inputs
- Isabelle2025-2, made available January 2026. Install the platform bundle from isabelle.in.tum.de:
Isabelle2025-2_linux.tar.gz, Isabelle2025-2_linux_arm.tar.gz, Isabelle2025-2.exe for Windows, or Isabelle2025-2_macos.tar.gz. There is no LTS, so pin the bundle version.
- The theory sources (
.thy), the session ROOT file, and for AFP work, the AFP release matching the Isabelle version.
- Sledgehammer provers ship with the official package: CVC4, cvc5, E, SPASS, Vampire, veriT, Z3, and Zipperposition.
Procedure
- Open the session in the Prover IDE. Run
isabelle jedit FILES to edit theories in the bundled jEdit Prover IDE, where the prover checks continuously. Define the session in a ROOT file (session Name = HOL with its theories), and extend the session search with -d DIR or a ROOTS catalog when sessions span directories. Done when: the theory holds a checked state in the IDE and isabelle build -D . finds the session.
- State the skeleton before proving. Write the target lemma and every helper lemma with
sorry in place of a proof, then have the IDE check the skeleton: sorry is accepted in the IDE and by the batch build alike, and the build only warns, so the IDE is for iterating and the log scan is the completion check. Each sorry marks an independent work unit. Done when: every sorry is an identified work unit and the IDE checks the skeleton.
- Fill goals: automation first, then structure. Close routine goals with
by simp or by auto. For a nontrivial goal, run sledgehammer: it drives the bundled external provers and returns a one-line proof such as by (metis ...), which is pasted into the theory. try0 runs a basket of standard methods; nitpick and quickcheck search for counterexamples. Structure what automation cannot close as Isar: proof ... qed with fix, assume, and show (thus expands to then show), with the induction and cases methods for recursive and case goals. Keep apply chains short; the manual defines apply m as backwards refinement, and long chains hide the proof state. Done when: every sorry is replaced and the build is green.
- Gate the result. The batch build does not fail on
sorry: with the default quick_and_dirty = false it only emits a warning (the theorem is recorded as an oracle), and quick_and_dirty merely relaxes proof checking rather than gating sorry. Scan the build log for sorry and the delivered diff for sorry and axiomatization, and rebuild the session rather than trusting the IDE's incremental state. Done when: isabelle build succeeds at the defaults and the build log and delivered diff contain no sorry and no new axiomatization.
- Build on AFP entries. Register the extracted AFP with
isabelle components -u <path-to-afp>/thys, then import an entry by its own session name, for example imports "ABC.Some_ABC_Theory". AFP sessions carry no extra namespace prefix. Done when: the AFP import resolves and the session builds.
Failure and recovery
Sledgehammer finds nothing: run nitpick for a countermodel; if none appears, split the lemma or add the missing intermediate lemma, because the statement may be true but unprovable as stated. A pasted hammer one-liner fails on rebuild: it depended on facts visible only in the IDE state, so supply them with using or write the Isar proof by hand. Build error: fix the theory at the reported line; the build names the session. Timeout: split the proof into intermediate have steps instead of raising any time budget. Session drift: rebuild the session from the ROOT definition. Scope creep: stop and roll back to the last verified state.
Output
Theory files and a ROOT session that build green under isabelle build at the defaults, delivered lemmas with no sorry, Sledgehammer one-liners confirmed by the batch build, and, where AFP is used, imports that resolve by AFP entry session name.
1---2name: writing-isabelle-proofs3description: Use when a proof needs Isabelle/HOL, its Sledgehammer automation, or an AFP session. Not for Lean 4: use writing-lean-proofs.4---56# Writing Isabelle proofs78## Contract910| Field | Bound contract |11|---|---|12| Trigger | The task is to write, review, or maintain Isabelle/HOL proofs, to drive Sledgehammer against a goal, or to build on an AFP entry. Methodology stays with proof-driven. |13| Authority | Reversible local: writes only theory files, session ROOT files, and Isabelle configuration inside the target project; rollback is version control. No remote mutation. |14| Side effect | Local writes to `.thy` sources, ROOT session definitions, and the AFP checkout already on disk. No remote mutation. |15| Done | `isabelle build` of the session succeeds, no `sorry` remains, and no `axiomatization` enters the delivered diff. |1617## Inputs1819- Isabelle2025-2, made available January 2026. Install the platform bundle from isabelle.in.tum.de: `Isabelle2025-2_linux.tar.gz`, `Isabelle2025-2_linux_arm.tar.gz`, `Isabelle2025-2.exe` for Windows, or `Isabelle2025-2_macos.tar.gz`. There is no LTS, so pin the bundle version.20- The theory sources (`.thy`), the session `ROOT` file, and for AFP work, the AFP release matching the Isabelle version.21- Sledgehammer provers ship with the official package: CVC4, cvc5, E, SPASS, Vampire, veriT, Z3, and Zipperposition.2223## Procedure24251. **Open the session in the Prover IDE.** Run `isabelle jedit FILES` to edit theories in the bundled jEdit Prover IDE, where the prover checks continuously. Define the session in a `ROOT` file (`session Name = HOL` with its theories), and extend the session search with `-d DIR` or a `ROOTS` catalog when sessions span directories. Done when: the theory holds a checked state in the IDE and `isabelle build -D .` finds the session.262. **State the skeleton before proving.** Write the target lemma and every helper lemma with `sorry` in place of a proof, then have the IDE check the skeleton: `sorry` is accepted in the IDE and by the batch build alike, and the build only warns, so the IDE is for iterating and the log scan is the completion check. Each `sorry` marks an independent work unit. Done when: every `sorry` is an identified work unit and the IDE checks the skeleton.273. **Fill goals: automation first, then structure.** Close routine goals with `by simp` or `by auto`. For a nontrivial goal, run `sledgehammer`: it drives the bundled external provers and returns a one-line proof such as `by (metis ...)`, which is pasted into the theory. `try0` runs a basket of standard methods; `nitpick` and `quickcheck` search for counterexamples. Structure what automation cannot close as Isar: `proof ... qed` with `fix`, `assume`, and `show` (`thus` expands to `then show`), with the `induction` and `cases` methods for recursive and case goals. Keep `apply` chains short; the manual defines `apply m` as backwards refinement, and long chains hide the proof state. Done when: every `sorry` is replaced and the build is green.284. **Gate the result.** The batch build does not fail on `sorry`: with the default `quick_and_dirty = false` it only emits a warning (the theorem is recorded as an oracle), and `quick_and_dirty` merely relaxes proof checking rather than gating `sorry`. Scan the build log for `sorry` and the delivered diff for `sorry` and `axiomatization`, and rebuild the session rather than trusting the IDE's incremental state. Done when: `isabelle build` succeeds at the defaults and the build log and delivered diff contain no `sorry` and no new `axiomatization`.295. **Build on AFP entries.** Register the extracted AFP with `isabelle components -u <path-to-afp>/thys`, then import an entry by its own session name, for example `imports "ABC.Some_ABC_Theory"`. AFP sessions carry no extra namespace prefix. Done when: the AFP import resolves and the session builds.3031## Failure and recovery3233Sledgehammer finds nothing: run `nitpick` for a countermodel; if none appears, split the lemma or add the missing intermediate lemma, because the statement may be true but unprovable as stated. A pasted hammer one-liner fails on rebuild: it depended on facts visible only in the IDE state, so supply them with `using` or write the Isar proof by hand. Build error: fix the theory at the reported line; the build names the session. Timeout: split the proof into intermediate `have` steps instead of raising any time budget. Session drift: rebuild the session from the ROOT definition. Scope creep: stop and roll back to the last verified state.3435## Output3637Theory files and a ROOT session that build green under `isabelle build` at the defaults, delivered lemmas with no `sorry`, Sledgehammer one-liners confirmed by the batch build, and, where AFP is used, imports that resolve by AFP entry session name.
OutlineDriven