Proof Method. simp [isa-001H]

The Isabelle simplifier, or simp, is one of the most powerful proof automation features in Isabelle, but it is a very simple idea. Given a set of equations, apply (simp) will (almost) blindly rewrite the goal by all of those equations (as well as any equations that are local assumptions in the goal) left-to-right. Given a sufficiently expressive set of equations, this allows the simplifier to solve many goals (including all of the theorems in Example [isa-001E]) on its own.

The default set of equations that simp uses is called the simpset. We can add theorems to the simpset by attaching the [simp] attribute to them.

ExampleSimplifier rules for nand [isa-001I]

  • December 2, 2025

Continuing our nand example, we can prove theorems and attach the [simp] attribute simultaneously: lemma nand_t[simp]: ‹nand True A = (¬ A)› apply (unfold nand_def) apply simp done Alternatively, we can add theorems after-the-fact like so: lemma nand_f: ‹nand False A = True› apply (unfold nand_def) apply simp done (* ... *) declare nand_f[simp] Occasionally it becomes useful to remove a theorem from the simp set. This can be achieved by using the declare command and the [simp del] attribute:

declare nand_f[simp del]

We can also adjust the simpset locally when we invoke the simp method:

lemma nand_xt[simp]: ‹nand A True = (¬ A)› by (simp add: nand_def)

Problem.

Isabelle does nothing to guarantee that simp will terminate, nor that it will be confluent (i.e. the results can depend on the order in which rewrites are applied). In particular, problems with non-termination can arise if there is a cycle in the equations used for rewriting. In such cases, it can be useful to remove certain lemmas from the simpset locally:

apply (simp del: nand_t)

Or explicitly list all the theorems to use:

apply (simp only: nant_t nand_f)

Or disable the simplification and use of local assumptions:

apply (simp (no_asm))

Or disable the simplification of (but still use) local assumptions:

apply (simp (no_asm_simp))

Or disable the use of (but still simplify) local assumptions:

apply (simp (no_asm_use))

Context

    Lecture. Definitions, Datatypes, Induction, Functions [isa-001B]

    Backlinks

      Proof Method. clarsimp, slowsimp, bestsimp and fastforce [isa-002R]

      Proof Method. force and auto [isa-002S]

      Proof Method. blast, fast, slow, and best [isa-002P]

      Defining functions in Isabelle [isa-001O]

      Related

        Example. Definitions, Datatypes, Induction, Functions › Proving the axioms for nand [isa-001E]