# Isabelle Cheat Sheet

Jump to: navigation, search

Throughout this page, `{placeholders}` are placed in between curly braces.

### Definitions in Lemmas/Theorems

When stating a lemma or theorem, use the following syntax to define new symbols which abbreviate an expression.

`defines "{symbol} \<equiv> {expression}"`

The fact of such a definition then becomes accessible by `{symbol}_def`. Note that a meta-equality `\<equiv>` (also `==` or `≡`) needs to be used here .

Example: `defines "m ≡ n mod k"` (access through `m_def`)

### Definitions in Proofs

Similarly, within an ISAR proof, new symbols may be defined using the following syntax. The fact of such definitions becomes accessible through `{symbol}_def`.

define {expression} where "{expression} = {definition}"

Example: `define m where "m = n mod k"` (access through `m_def`)

### Custom Case Distinctions

When a proof requires to consider different custom cases c1, c2, ... instead of the cases generated by `proof (cases ...)`

```proof -
consider ({nameC1}) "{case1}" | ({nameC2}) "{case2}" | ... by {proof of totality of all cases}
then show ?thesis
proof cases
case {nameC1}
then show ?thesis
{proof}
next
case {nameC2}
then show ?thesis
{proof}
...
qed
qed
```

### Proof by contradiction

```lemma "{statement}"
proof(rule ccontr)
assume "¬ {statement}"
then show False
{proof}
qed
```

### Obtain from existence statement

In order to work with a variable that satisfies certain conditions, e.g. as part of an existential quantifier, use the `obtain` keyword.

`obtain {symbol(s)} where {name}: "{condition(s) involving the symbol(s)}" by {proof of existence}`

Naming the statement is optional, but allows to refer to the fact containing the conditions that are satisfied.

Example: `obtain k t where "k mod t = 3 ∧ k > t" by {proof}`

### Accessing elements of a datatype

In the definition of a datatype, `get`-functions that return a specific attribute can be defined, too.

Example: `datatype mat2 = Mat (mat_a : int) (mat_b : int) (mat_c : int) (mat_d : int)`