Table of Contents

Isabelle/HOL and Proof General Reference

This site is intended to help getting started with using Isabelle/HOL and the Isabelle jEdit editor. This page in particular is the quick cheat sheet and can be used as a reference.

Please use the FAQ - Ask Questions page to post and view questions and the Exam Questions page to collect possible questions for the exams. The Goals of the Exercises page summarizes what you should have learned by doing them.

For best practices in Isabelle/HOL, see the corresponding page.

Please also check out and add stuff concerning the Editor, Isabelle/HOL Syntax and useful External References. Last but not least, you can post and check out Example Code.

Help us to improve the Wiki by checking and complementing existing content, as well as creating wanted pages!

Getting Started

You can download and install Isabelle from http://isabelle.in.tum.de/. To run Isabelle you can run `isabelle jedit -m brackets`.

Isabelle is already installed on the SCI machines tux1, tux2, tux3 and tux9. On those machines you can start it by simply typing `isabelle` into a terminal.

Syntax

Every Isabelle/HOL theory looks like this:

theory MyTheory imports Main
begin

  ...

end

It is important that the name of the theory is equal to the name of the file.

Special symbols

Isabelle uses many symbols which are not available on a normal keyboard. You can either use the “Symbols” tab in jedit or type the following shortcuts and use autocomplete with “TAB” to get the correct symbol.

Logics
type /\ or & \/ or | \not or ~ --> <-> \forall or ! \exists or ?
Meta
type !! ==> == [| |]
Math
type = ~= < > >=
Sets
type \in or : \notin or ~: \subset \subseteq \inter \union

If you know LaTeX, try using commands you know from there.

Functions

Heuristic: try ML! Major differences:

Definitions

Proofs

Apply method $method with parameters $params by entering apply ($method $params). If you have no parameters, you can just write apply $method. For example, a (very simple) proof can look like this:

  lemma "[| A; A --> B |] ==> B"
  apply (frule mp)
  apply assumption+
  done

Methods

Basic Methods

Name Parameters All goals Safe New Goals Variants
assumption x
cases an expression x x case_tac
drule a rule x drule(k), drule_tac
erule a rule x erule(k), erule_tac
fold a definition (or equation) x x
frule a rule x x frule(k), frule_tac
induct a variable x induct_tac
insert a theorem x x cut_tac
rename_tac list of identifiers
rotate_tac an integer x
rule a rule x rule(k), rule_tac
split a splitting rule ? x
subgoal_tac a formula x
subst a definition (or equation) x x subst (asm)
thin_tac a formula
unfold a definition (or equation) x x ?

Automated Methods

Name Classical Simp All goals Safe Splits Finishes Strength Weakness
arith x x linear arithmetics exponentially slow for many operators
auto x x x x
blast x x x logics, sets; fast
clarify x x
clarsimp x x x
force x x x x
metis x x x logics no sets
safe x x x x
simp x x x
simp_all x x x x

Note that safety of automated proof methods can be sabotaged by adding unsafe rules to rule sets used.

There are many more methods. You can print them by issuing the command print_methods, key combination C-c C-a h m or via [Isabelle → Show Me → Methods].

Method Combinators

Symbol Semantics Example
 + Applies the method as often as applicable, but at least once. assumption+
(_,_) Applies all the methods in sequence and fails if any one is not applicable. (rule mp, simp)
[n] Applies the method only to the first n subgoals. auto[5]

The sequencing of methods has the additional effect that backtracking is used to make the whole sequence work. As many methods could be applied in different ways, e.g. by matching the premise with a different assumption, failure of one step of the sequence just leads to trying another possibility for one of the steps before.

Theorem Modification

Attributes (also: directives) can be used to obtain new, more specific theorems from already proven, more general ones. In other words, they allow you to adapt theorems to your current needs. There are two major uses:

  1. $thm [$attr1, $attr2, …] – can be used in any place where you would put a theorem or rule. Instead of $thm itself, the result of applying the given attributes from left to right is used.
  2. lemmas $name = $thm [$attr1, $attr2, …] – assigns a new name to the modified theorem, enabling later (re)use.
  3. (lemma|theorem) $name [$attr1, $attr2, …] : $formula – applies the given attributes from left to right after the proof is finished, assigning the result to the given name.
Attribute Semantics
of $t1 $t2 … Replaces variables with the given terms in order. Use _ for keeping the variable. (Example)
where $v1=$t1 and $v2=$t2 … Replaces the specified variables in a theorem with the given terms. (Example)
THEN $rule Applies the given rule to a theorem and returns the conclusion. (Example)
OF $thm1 $thm2 Generates a new instance of a rule using the given theorems. (Example)
simplified Applies simp to a theorem and returns the result. (Example)
rotated $k Rotates the given theorem's assumptions by $k to the left. If no value is given, $k=1 is assumed. (Example)
symmetric Equivalent to THEN sym. (Example)

Other attributes perform some action with a theorem. They probably only make sense in lemma/theorem definitions or together with lemmas (see above):

Attribute Action
iff Enables both simplifier and classical reasoner to use this theorem. Only use with equivalences whose right-hand side is “simpler” than left-hand side.
rule_format Lifts a top-level implication into Pure logic, i.e. enables reasoners to use the theorem as rule.
simp Allows the simplifier to use this theorem.

There are many more attributes. You can print them by issuing the command print_attributes, key combination C-c C-a h a or via [Isabelle → Show Me → Attributes].

Finishers

Command Semantics
done finishes the proof if no more subgoals left
by $method tries to finish the rest of the proof with the given method followed by assumption+
sorry forces an unfinished proof to be considered successful (i.e. lemma/theorem is usable!)
oops aborts the proof and drops the lemma/theorem

Rules

Assorted gimmicks