# Isabelle Cheat Sheet

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

cf. https://stackoverflow.com/questions/48386895/access-elements-of-data-types