Isabelle/HOL Support Wiki

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
====== Best Practices ======
This is a collection of hints and conventions that enable you to write compilable and useful functions and formula faster. There are some obvious, syntactical issues but also more subtle things you should keep in mind when building a theory.

===== Syntax =====
==== Parentheses ====
Some syntactical constructs of Isabelle/HOL are not as well-structures as you might think so you want to put parentheses around them. In particular, these applies to

  * Conditions: ''(if P then x else y)''
  * Case distinctions: ''(case x of p1 => e1 | p2 => e2)''
  * Constructors (in patterns): ''(x#xs)''

In all of these cases it is generally inadvisable to leave out the outermost parentheses.

You might also run into problems by implicitly put parentheses (by precedence rules). 

As an example, consider quantifiers: Is $\forall x. P\; x \vee Q$ to be read as $\forall x. (P\; x \vee Q)$ or as $(\forall x. P\; x) \vee Q$? One might expect the latter, but Isabelle does the former.

If in doubt, check [Isabelle → Settings → Display → Show Brackets] and find out what exactly happens.
===== Modelling =====
==== Sets and Functions ====
Sets and (boolean) functions are equivalent. However, using both worlds in parallel, e.g. using sometimes $P\; x$ and sometimes $x \in P$ or even $\{x. P\; x\}$, you might run into issues during proofs as Isabelle has to perform certain steps in order to switch from one point of view to the other. Therefore you better choose wether to express your statements in predicate or in set notation and stick with it.