User Tools

Site Tools


best_practices

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
best_practices [2011/07/20 13:00]
131.246.161.187 [Sets and Functions]
best_practices [2012/04/13 15:36] (current)
paddy [Parentheses]
Line 7: Line 7:
  
   * Conditions: ''​(if P then x else y)''​   * Conditions: ''​(if P then x else y)''​
-  * Case distinctions:​ ''​(case x of p1 => e1 | p2 => e2)+  * Case distinctions:​ ''​(case x of p1 => e1 | p2 => e2)''​
   * Constructors (in patterns): ''​(x#​xs)''​   * Constructors (in patterns): ''​(x#​xs)''​
  
 In all of these cases it is generally inadvisable to leave out the outermost parentheses. In all of these cases it is generally inadvisable to leave out the outermost parentheses.
  
-You might also often have to overwrite how Isabelle puts parentheses ​implicitly, for example ​around ​quantifiers: ​''​(ALL x. P x)''​. If in doubt, check [Isabelle → Settings → Display → Show Brackets] and find out what exactly happens.+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 ===== ===== Modelling =====
 ==== Sets and Functions ==== ==== 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.+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.
best_practices.1311159604.txt.gz · Last modified: 2011/07/20 13:00 by 131.246.161.187