# Proof Patterns

Chapter 1 of the Isabelle/Isar Reference Manual and Chapter 4 of the official Programming and Proving in Isabelle/HOL tutorial provide a comprehensive guide for common proof patterns. Here we list some additional patterns. Throughout this page, placeholders are put between angle braces `<...>`.

## Definitions in Lemmas

When stating a lemma, you can use the following syntax to introduce a local definition:

``````defines "<symbol> ≡ <expression>"
``````

The fact of such a definition then becomes accessible by `<symbol>_def`.

Example: `defines "m ≡ n mod k"`; accessible through `m_def`

## Definitions in Proofs

Inside a proof, you can use the following syntax to introduce a local definition:

``````define <symbol> where "<symbol> ≡ <expression>"
``````

The fact of such a definition then becomes accessible by `<symbol>_def`.

Note that local definitions are different from term abbreviations introduced by `let` (cf Isabelle/Isar Reference Manual): the former are visible within the logic as actual equations while the latter disappear when Isabelle processes the input.

Example: `define m where "m ≡ n mod k"`; accessible through `m_def`