| name | isabelle-proof-tool-development |
| description | Techniques for developing proof tools in Isabelle, including understanding HHF (Hereditary Harrop Formula) proof state representation |
Isabelle Proof Tool Development: HHF Proof State Techniques
This skill provides essential techniques for implementing proof tools in Isabelle, with a focus on understanding how Isabelle represents proof states using HHF (Hereditary Harrop Formula) format. This knowledge is fundamental to building tactics, automated provers, and other proof automation tools in Isabelle.
What is HHF (Hereditary Harrop Formula)?
HHF has the general form:
⋀x₁...xₘ. H₁ ⟹ ... ⟹ Hₙ ⟹ A
Where m, n ≥ 0; A is atomic or recursively HHF; H₁, ..., Hₙ are recursively HHF.
CRITICAL: HHF MUST use meta-logic operators ⋀ and ⟹, NOT object-logic operators ∀ and →
HHF as Proof State
IMPORTANT: When an HHF sequent represents a proof state, it encodes subgoals in a specific way.
Example:
(⋀x y. A ⟹ B ⟹ C) ⟹ (⋀z. D ⟹ E) ⟹ F
This represents a proof state where:
- Ultimate goal: F (the rightmost element)
- Subgoal 1:
- Local variables: x, y (arbitrary but fixed)
- Premises: A, B
- Goal to show: C
- Subgoal 2:
- Local variable: z (arbitrary but fixed)
- Premise: D
- Goal to show: E
How to read: At the top level, each (⋀vars. premises ⟹ goal) structure before the rightmost element represents one subgoal. Within each subgoal, the meta-quantifiers (⋀) bind local variables, and the nested ⟹ separate premises from the subgoal's conclusion. The rightmost element is the ultimate goal, shown once all subgoals are solved.
The Pure.prop Protector
The ultimate goal is actually wrapped by an invisible operator Pure.prop :: prop ⇒ prop (not printed). This distinguishes the ultimate goal from intermediate subgoals.
Why needed: Consider these two different proof states:
... ⟹ Pure.prop (A ⟹ B) - Ultimate goal is A ⟹ B; no subgoals remain... ⟹ A ⟹ Pure.prop B - Ultimate goal is B; one subgoal remains (premise A → show B)
Without Pure.prop, these would be ambiguous.
Normal Form
Isabelle maintains HHF in normal form where:
- Quantifiers are pulled to the front at each nesting level
- Implications are right-associative:
A ⟹ B ⟹ C means A ⟹ (B ⟹ C)
Related ML Code
Key modules in contrib/Isabelle2024/src/Pure/:
Pure/logic.ML - Meta-logic operations including HHF manipulationPure/term.ML - Term structure (handles ⋀ and ⟹)Pure/thm.ML - Theorem representationPure/goal.ML - Goal/subgoal operationsPure/Proof/proof.ML - Proof state structure
