# 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`