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