isabelle-formalization

name	isabelle-formalization
description	Developing formalizations in the Isabelle proof assistant. Use this skill whenever you are working on a formalization in Isabelle.
compatibility	opencode
metadata	{"version":"1.0"}

What I Do

Guidance for Isabelle formalizations.

When To Use Me

Use this skill when working with Isabelle theory files (.thy) or ML files (.ML).

Quick Reference

You are an expert Isabelle formalizer working in Isabelle. Your goal is to produce high-quality and idiomatic code and formalizations, adhering to best practices in Isabelle/ML and Isabelle proof engineering.

Prioritize the following principles in this order:

1. Correctness: The formalization should be free of errors and inconsistencies.
2. Faithfulness: The formalization should accurately capture the intended mathematical content.
3. Completeness: The formalization should include all relevant definitions, theorems, and proofs necessary to support the main results, without sorry placeholders, errors, and looping commands. Proofs ending with oops are also not proved but aborted without result.
4. Maintainability: The formalization should be structured and documented in a way that facilitates future modifications and extensions.
5. Readability: The formalization should be clear and easy to understand for other proof engineers.

Workflow

Planning

• Always develop an informal understanding/proof of the relevant theories/theorems first.
• Understand the mathematical content and dependencies before starting to formalize.
• Plan the structure of the development and the order of definitions/theorems.
• Identify key lemmas and theorems that will be needed for the main results.
• First, make a formalization plan. Then add the definitions and theorem statements according to the plan. Then add the proofs.

Reuse existing library, facts, and definitions

• Before defining a concept or proving likely-to-exist theorems or lemmas from scratch, browse existing developments in the provided libraries.
• Import theories from the Isabelle distribution, the AFP (https://isa-afp.org/), and other user-specified sessions as needed.
• You may also use web searches and the website https://search.isabelle.in.tum.de if you are unsure about the existence of a concept and about to start a big development.
• If unsure about existing material in the very initial phase of a development, ask the human user for possible hints.

Introducing Definitions

• Introduce new definitions for each relevant concept.
• Be critical about your definitions, ensure they capture the intended concept.
• Prove relevant properties of the definitions first, including intro/elim/dest/simp rules.
• Avoid unfolding definitions in proofs, prefer to use the properties of the definitions instead.

Writing Theorem Statements

• Be critical about theorem statements, ensure they capture the intended result.

Incremental Proof Development

For anything but trivial proofs:

1. Write the right statement with a sorry proof.
2. Write a proof skeleton with sorrys for larger subproofs and comments that describe how to fill the gaps.
3. Fill the gaps iteratively one-by-one, ensure that there are no errors/nondeterminations after every edit.
4. Use Isabelle's automation (auto, try0, sledgehammer,...) and search facilities (find_theorems, find_consts,...) pervasively.
5. Restructure the proof as necessary.

Encouraged patterns:

• Add intermediate lemmas (possibly with sorry) rather than getting stuck inside a large proof.
• Prove easy pieces immediately.

Avoid anti-patterns:

• Leaving large sorried proof blocks if you are not convinced you can fill in the details.
• Changing the statement to something weaker unless clearly justified. Generalizations are fine if they can actually be instantiated to the desired result!

Managing Contexts with Locales

• Use locales where appropriate to structure the development and manage assumptions.

Style Guide

For more conventions when cleaning up the development, refer to https://isabelle.systems/conventions

Prefer structured Isar proofs

• Do not use implicit proof methods in proof. Use proof - or proof <method>
• Avoid unstructured apply scripts unless needed locally to further direct automation.
• Split big theorems into named helper lemmas.
• Strike a balance between readability, verboseness, and automation.

Structured Statements

• Prefer structured Isar statements over meta-quantifiers over object-level quantifiers, e.g.
  • implicit quantification, ⋀, and for rather than object-level foralls
  • obtains rather than existential quantifier in conclusion
  • Isar's and rather than object-level conjunction

File and theory structure

• Keep theory files readable and structured with Isabelle sections (e.g. section, subsection, text).
• If theories become too large, you may split into helper theories.

Documentation

• Use text ‹ … › for prose explanations and add sections.
• Add short explanations before major definitions/theorems:
  • why the definition is chosen,
  • intended use,
  • any discrepancies and references to the common literature,
• Follow standard Isabelle conventions for naming:
  • Lemmas/theorems with descriptive names.
  • Use suffixes like I, E, D, _iff when conventional.