====== 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.

{{ :isabelle_hol.gif?nolink&200 |}}

Please use the [[faq]] page to post and view questions and the [[exam]] page to collect possible questions for the exams. The [[official:goals]] page summarizes what you should have learned by doing them.

For best practices in Isabelle/HOL, see the [[best_practices|corresponding page]].

Please also check out and add stuff concerning the [[editor]], [[syntax]] and useful [[references]].
Last but not least, you can post and check out [[code_repository|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:

<code>
theory MyTheory imports Main
begin

  ...

end
</code>

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 | $\land$  | $\lor$  | $\neg$ | $\longrightarrow$  | $\leftrightarrow$ | $\forall$   | $\exists$  |
^ type  | ''/\'' or ''&'' | ''\/'' or ''|'' | ''\not'' or ''~'' | ''<nowiki>--></nowiki>'' | ''<nowiki><-></nowiki>'' | ''\forall'' or ''!'' | ''\exists'' or ''?'' |

^ Meta  | $\bigwedge$ | $\Longrightarrow$ | $\equiv$ | $[|$ | $|]$ |
^ type | ''!!'' | ''<nowiki>==></nowiki>'' | ''=='' | ''[|'' | ''|]'' |

^ Math  | $=$ | $\neq$  | $<$ | $>$ | $\leq$ | $\geq$ |
^ type | ''='' | ''~='' | ''<'' | ''>'' | ''<='' | ''>='' |

^ Sets  | $\in$   | $\notin$ | $\subset$ | $\subseteq$ | $\cap$ | $\cup$ |
^ 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:

  * Function definition with ''primrec'', ''fun'' and ''function''
  * List constructor is ''#'', not ''::''.
  * Types and expressions have to be enclosed in double quotes

==== Definitions ====
  * Constants
    * ''definition $ident where "$ident == $expression"'' -- assigns the value of ''$expression'' to identifier ''$ident''
  * Theorems
    * ''lemma ($name :)? "$formula"'' -- states ''$formula'' as lemma, assigns it a name (if given) and creates a proof goal
    * ''theorem ($name :)? "$formula"'' -- states ''$formula'' as theorem, assigns it a name (if given) and creates a proof goal
  * Datatypes
    * ''datatype''
    * ''type_synonym''
  * Functions
    * ''primrec'' -- used for primitive recursive functions (nothing to prove, but heavy constraints)
    * ''fun'' -- used for more general functions, but have to prove termination (e.g. via well-founded order)
    * ''function'' -- used for arbitrary function definitions; have to prove all kinds of stuff
  * (Co)Inductive Stuff

===== 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 ^
| ''[[reference:assumption|assumption]]''   | ---                 |     |  x  |     | | 
| ''[[reference:cases|cases]]''             | an expression       |     |  x  |  x  | ''case_tac'' |
| ''[[reference:drule|drule]]''             | a rule              |     |     |  x  | ''drule(k)'', ''drule_tac'' |
| ''[[reference:erule|erule]]''             | a rule              |     |     |  x  | ''erule(k)'', ''erule_tac'' |
| ''[[reference:fold|fold]]''               | a definition (or equation) |  x  |  x  |     | |
| ''[[reference:frule|frule]]''             | a rule              |     |  x  |  x  | ''frule(k)'', ''frule_tac'' |
| ''[[reference:induct|induct]]''           | a variable          |     |     |  x  | ''induct_tac'' |
| ''[[reference:insert|insert]]''           | a theorem           |  x  |  x  |     | ''cut_tac'' |
| ''[[reference:rename_tac|rename_tac]]''   | list of identifiers |     |     |     | |
| ''[[reference:rotate_tac|rotate_tac]]''   | an integer          |     |  x  |     | |
| ''[[reference:rule (method)|rule]]''      | a rule              |     |     |  x  | ''rule(k)'', ''rule_tac'' |
| ''[[reference:split|split]]''             | a splitting rule    |     |  ?  |  x  | |
| ''[[reference:subgoal_tac|subgoal_tac]]'' | a formula           |     |     |  x  | |
| ''[[reference:subst|subst]]''             | a definition (or equation) |     |  x  |  x  | ''subst (asm)'' |
| ''[[reference:thin_tac|thin_tac]]''       | a formula           |     |     |     | |
| ''[[reference:unfold|unfold]]''           | a definition (or equation) |  x  |  x  |  ?  | |

=== Automated Methods ===

^ Name ^ Classical ^ Simp ^ All goals ^ Safe ^ Splits ^ Finishes ^ Strength ^ Weakness ^
| ''[[reference:arith|arith]]''       |     |     |     |  x  |     |  x  | linear arithmetics | exponentially slow for many operators |
| ''[[reference:auto|auto]]''         |  x  |  x  |  x  |     |  x  |     | | |
| ''[[reference:blast|blast]]''       |  x  |     |     |  x  |     |  x  | logics, sets; fast | |
| ''[[reference:clarify|clarify]]''   |  x  |     |     |  x  |     |     | | |
| ''[[reference:clarsimp|clarsimp]]'' |  x  |  x  |     |  x  |     |     | | |
| ''[[reference:force|force]]''       |  x  |  x  |     |  x  |     |  x  | | |
| ''[[reference:metis|metis]]''       |  x  |     |     |  x  |     |  x  | logics | no sets |
| ''[[reference:safe|safe]]''         |  x  |     |  x  |  x  |  x  |     | | |
| ''[[reference:simp|simp]]''         |     |  x  |     |  x  |  x  |     | | |
| ''[[reference:simp_all|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:

  - ''$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.
  - ''lemmas $name = $thm [$attr1, $attr2, ...]'' -- assigns a new name to the modified theorem, enabling later (re)use.
  - ''(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. ([[reference:attribute_examples#of|Example]]) |
| ''where $v1=$t1 and $v2=$t2 ...''  | Replaces the specified variables in a theorem with the given terms. ([[reference:attribute_examples#where|Example]]) |
| ''THEN $rule''                     | Applies the given rule to a theorem and returns the conclusion. ([[reference:attribute_examples#THEN|Example]]) |
| ''OF $thm1 $thm2''                 | Generates a new instance of a rule using the given theorems. ([[reference:attribute_examples#of1|Example]]) |
| ''simplified''                     | Applies ''simp'' to a theorem and returns the result. ([[reference:attribute_examples#simplified|Example]]) |
| ''rotated $k''                     | Rotates the given theorem's assumptions by ''$k'' to the left. If no value is given, ''$k=1'' is assumed. ([[reference:attribute_examples#rotated|Example]]) |
| ''symmetric''                      | Equivalent to ''THEN sym''. ([[reference:attribute_examples#symmetric|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 [[#Methods|method]] followed by ''[[reference:assumption|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 ====
  * ''conjI'', ''conjE'', ''conjunct1'', ''conjunct2''
  * ''disjI1'', ''disjI2'', ''disjE''
  * ''impI'', ''impE'', ''mp''
  * ''iffI'', ''iffE''
  * ''allI'', ''<nowiki>spec</nowiki>'', ''bspec''
  * ''exI'', ''exE'', ''bexI''
  * ''notI'', ''notE''
  * ''FalseE''
  * ''classical''
  * ''contrapos_(pp|np|pn|nn)''
  * Basically any theorem!

==== Assorted gimmicks ====
  * ''thm $name'' -- command that shows theorem with name ''$name''
  * ''value $expr'' -- command that evaluates the specified expression and prints the result
  * ''prefer $k'' -- command that moves subgoal number ''$k'' to the top of the list
  * ''defer'' -- command that moves the current subgoal to the bottom of the list  
  * ''quickcheck'' -- command that tries to find a counterexample to the current subgoal. Useful to check wether an unsafe rule did harm. Note: it might not find a counterexample even if the goal can not be proven!
  * ''refute'' and ''nitpick'' -- similar to quickcheck but try to find counterexample models, not only variable assignments. Can handle more constructs.
  * ''sledgehammer'' -- command that invokes fully automated theorem provers both locally and on remote clusters. Tries to find a (minimal) set of theorems needed to solve the current goal.
  * ''lfp $function'' -- a function that yields the least fixpoint of the given function
  * ''undefined'' -- a distinguished value for //any// type
  * ''f(x := y)'' -- the //function update//: the result of this expression is the function ''f'' updated such that it now returns ''y'' for parameter ''x''; the other values do not change.
  * ''{x. P x}'' -- the set of values fulfilling predicate ''P''. For instance, ''{x::nat. x dvd 125}'' is the set of (natural) divisors of $125$.
  * ''{E x | x. P x}'' -- the set of values created by expression ''E'', for all values fulfilling predicate ''P'', ''{x + y | x y. x < 10 /\ y < 10}'' is the set of sums of all pairs of natural numbers with a single digit.