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

1. 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.
2. 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.
3. 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.
4. 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.
5. 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.