User Tools

Site Tools


start

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
start [2012/04/13 11:55]
131.246.92.39 [Methods]
start [2014/04/30 15:28] (current)
peter jedit symbols
Line 1: Line 1:
 ====== Isabelle/​HOL and Proof General Reference ====== ====== Isabelle/​HOL and Proof General Reference ======
  
-This site is intended to help getting started with using Isabelle/​HOL and the Proof General.+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. This page in particular is the quick //cheat sheet// and can be used as a reference.
  
 {{ :​isabelle_hol.gif?​nolink&​200 |}} {{ :​isabelle_hol.gif?​nolink&​200 |}}
  
-Please use the [[faq|FAQ - Ask Questions]] page to post and view questions and the [[exam|Exam Questions]] page to collect possible questions for the exams. The [[official:​goals|Goals of the Exercises]] page summarizes what you should have learned by doing them.+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]]. For best practices in Isabelle/​HOL,​ see the [[best_practices|corresponding page]].
  
-Please also check out and add stuff concerning the [[editor|Editor]], [[syntax|Isabelle/​HOL Syntax]] and useful [[references|External References]].+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]]. 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|needed entries]]! +Help us to improve the Wiki by checking and complementing existing content, as well as creating [[wanted pages]]!
-===== Shortcuts =====+
  
-We denote ''​CTRL + $key''​ by ''​C-$key''​ and ''​ALT + $key''​ by ''​M-$key''​. 
-==== General Emacs ==== 
  
-  * ''​C-x C-f''​ -- open a file +===== Getting Started =====
-  * ''​C-k''​ -- delete the rest of the line +
-  * ''​C-a''​ -- jump to the beginning of the current line +
-  * ''​C-e''​ -- jump to the end of the current line+
  
-==== Proof General ==== +You can download and install Isabelle from [[http://​isabelle.in.tum.de/​]]. 
-Press ''​C-c C-☐''​ to control the proof buffer (i.e. processing the theory), with ''​☐''​ one of: +To run Isabelle you can run `isabelle jedit -m brackets`
-  * ''​b''​ -- process as far as possible + 
-  * ''​c''​ -- cancel: interrupt a running calculation +Isabelle ​is already installed on the SCI machines tux1tux2, tux3 and tux9.  
-  * ''​f''​ -- [[reference:theorem search|search]] in the available theorems (e.g''​name:​ mp''​) +On those machines you can start it by simply typing `isabelle` into terminal.
-  * ''​n''​ -- next: process the next line in Isabelle +
-  * ''​p''​ -- show the current state of a proof (for instancein place of an error message currently being shown) +
-  * ''​r''​ -- retract: go back to the beginning +
-  * ''​u'' ​ -- undo: push back the processed part of the text by one line +
-  * ''​v''​ -- enter command whose result is send to the response panel (see [[start#​Assorted gimmicks|below]] for some examples) +
-  * ''​RETURN''​ -- go here: evaluate up to where the cursor is+
  
-==== Advanced Tools ==== 
-  * ''​C-c C-a C-q''​ -- ''​quickcheck''​ (see below) 
-  * ''​C-c C-a r''​ -- ''​refute''​ (see below) 
-  * ''​C-c C-a C-n''​ -- ''​nitpick''​ (see below) 
-  * ''​C-c C-a C-s''​ -- ''​sledgehammer''​ (see below) 
  
-==== Menu Magic ==== 
-  * [Options → C-x/C-c/C-v Cut and Paste (CUA)] -- enable standard hotkeys for copy and paste 
-  * [Isabelle → Show Me → Methods] -- Prints a list of all available methods 
-  * [Isabelle → Settings → Display] -- show hidden symbols such as types or parentheses for debugging. (in theory mode) 
-  * [Isabelle → Help → Isabelle Documentation] -- documentation 
-  * [Proof-General → Quick Options → Display → Use Three Panes] -- check to have a more comfortable setup (in theory mode) 
 ===== Syntax ===== ===== Syntax =====
  
Line 53: Line 30:
  
 <​code>​ <​code>​
-theory ​Name imports Main+theory ​MyTheory ​imports Main
 begin begin
- 
-  ... 
-  ​ 
-$definitions 
  
   ...   ...
Line 65: Line 38:
 </​code>​ </​code>​
  
-==== Formulae ​==== +It is important that the name of the theory is equal to the name of the file. 
-Basic logical formula ​are written ​in the usual way. See below for the ASCII encodings of common symbols:+ 
 +==== 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$ ​ | ^ Logics | $\land$ ​ | $\lor$ ​ | $\neg$ | $\longrightarrow$ ​ | $\leftrightarrow$ | $\forall$ ​  | $\exists$ ​ |
-ASCII  | ''/​\''​ | ''​\/''​ | ''​\not''​ | ''<​nowiki>​--></​nowiki>''​ | ''​=''​ | ''​ALL''​ | ''​EX''​ |+type  | ''/​\''​ or ''&​''​ | ''​\/​''​ or ''​|''​ | ''​\not''​ or ''​~''​ | ''<​nowiki>​--></​nowiki>''​ | ''​<​nowiki><​-></​nowiki>​''​ | ''​\forall''​ or ''​!''​ | ''​\exists''​ or ''?​''​ |
  
 ^ Meta  | $\bigwedge$ | $\Longrightarrow$ | $\equiv$ | $[|$ | $|]$ | ^ Meta  | $\bigwedge$ | $\Longrightarrow$ | $\equiv$ | $[|$ | $|]$ |
-ASCII | ''​!!''​ | ''<​nowiki>​==></​nowiki>''​ | ''​==''​ | ''​[|''​ | ''​|]''​ |+type | ''​!!''​ | ''<​nowiki>​==></​nowiki>''​ | ''​==''​ | ''​[|''​ | ''​|]''​ |
  
 ^ Math  | $=$ | $\neq$ ​ | $<$ | $>$ | $\leq$ | $\geq$ | ^ Math  | $=$ | $\neq$ ​ | $<$ | $>$ | $\leq$ | $\geq$ |
-ASCII | ''​=''​ | ''​~=''​ | ''<''​ | ''>''​ | ''​\le''​ | ''​\ge''​ |+type | ''​=''​ | ''​~=''​ | ''<''​ | ''>''​ | ''​<=''​ | ''​>=''​ |
  
 ^ Sets  | $\in$   | $\notin$ | $\subset$ | $\subseteq$ | $\cap$ | $\cup$ | ^ Sets  | $\in$   | $\notin$ | $\subset$ | $\subseteq$ | $\cap$ | $\cup$ |
-ASCII | ''​\in''​ | ''​\notin''​ | ''​\subset''​ | ''​\subseteq''​ | ''​\inter''​ | ''​\union''​ |+type | ''​\in''​ or '':​''​ | ''​\notin''​ or ''​~:​''​ | ''​\subset''​ | ''​\subseteq''​ | ''​\inter''​ | ''​\union''​ |
  
-Find more symbols via [Tokens → List Shortcuts]. ​If you know LaTeX, try using commands you know from there.+If you know LaTeX, try using commands you know from there.
  
 ==== Functions ==== ==== Functions ====
Line 112: Line 88:
     done     done
 ==== Methods ==== ==== Methods ====
 +
 === Basic Methods === === Basic Methods ===
-^ Name ^ Parameters ^ All goals ^ Safe ^ New Goals ^ Variants ^ + 
-| ''​[[reference:​assumption]]'' ​ | ---                 ​| ​    ​| ​ x  |     | |  +^ Name                                      ^ Parameters ​   ^ All goals ^ Safe ^ New Goals ^ Variants ^ 
-| ''​[[reference:​cases]]'' ​      ​| an expression ​      ​| ​    ​| ​ x  |  x  | ''​case_tac''​ | +| ''​[[reference:​assumption|assumption]]'' ​  ​| ---                 ​| ​    ​| ​ x  |     | |  
-| ''​[[reference:​drule]]'' ​      ​| a rule              |     ​| ​    ​| ​ x  | ''​drule(k)'',​ ''​drule_tac''​ | +| ''​[[reference:​cases|cases]]'' ​            ​| an expression ​      ​| ​    ​| ​ x  |  x  | ''​case_tac''​ | 
-| ''​[[reference:​erule]]'' ​      ​| a rule              |     ​| ​    ​| ​ x  | ''​erule(k)'',​ ''​erule_tac''​ | +| ''​[[reference:​drule|drule]]'' ​            ​| a rule              |     ​| ​    ​| ​ x  | ''​drule(k)'',​ ''​drule_tac''​ | 
-| ''​[[reference:​fold]]'' ​       ?                   |  x  |  x  |  ?  ​| | +| ''​[[reference:​erule|erule]]'' ​            ​| a rule              |     ​| ​    ​| ​ x  | ''​erule(k)'',​ ''​erule_tac''​ | 
-| ''​[[reference:​frule]]'' ​      ​| a rule              |     ​| ​ x  |  x  | ''​frule(k)'',​ ''​frule_tac''​ | +| ''​[[reference:​fold|fold]]'' ​              ​a definition (or equation) ​|  x  |  x  |     ​| | 
-| ''​[[reference:​induct]]'' ​     | a variable ​         |     ​| ​    ​| ​ x  | ''​induct_tac''​ | +| ''​[[reference:​frule|frule]]'' ​            ​| a rule              |     ​| ​ x  |  x  | ''​frule(k)'',​ ''​frule_tac''​ | 
-| ''​[[reference:​insert]]'' ​     | a theorem ​          ​| ​ x  |  x  |     | ''​cut_tac''​ | +| ''​[[reference:​induct|induct]]'' ​          ​| a variable ​         |     ​| ​    ​| ​ x  | ''​induct_tac''​ | 
-| ''​[[reference:​rename_tac]]'' ​ | list of identifiers |     ​| ​    ​| ​    | | +| ''​[[reference:​insert|insert]]'' ​          ​| a theorem ​          ​| ​ x  |  x  |     | ''​cut_tac''​ | 
-| ''​[[reference:​rotate_tac]]'' ​ | an integer ​         |     ​| ​ x  |     | | +| ''​[[reference:​rename_tac|rename_tac]]'' ​  ​| list of identifiers |     ​| ​    ​| ​    | | 
-| ''​[[reference:​rule (method)|rule]]''​ | a rule       ​|     ​| ​    ​| ​ x  | ''​rule(k)'',​ ''​rule_tac''​ | +| ''​[[reference:​rotate_tac|rotate_tac]]'' ​  ​| an integer ​         |     ​| ​ x  |     | | 
-| ''​[[reference:​split]]'' ​      ​| a splitting rule    |     ​| ​ ?  |  x  | | +| ''​[[reference:​rule (method)|rule]]'' ​     | a rule              |     ​| ​    ​| ​ x  | ''​rule(k)'',​ ''​rule_tac''​ | 
-| ''​[[reference:​subgoal_tac]]''​ | a formula ​          ​| ​    ​| ​    ​| ​ x  | | +| ''​[[reference:​split|split]]'' ​            ​| a splitting rule    |     ​| ​ ?  |  x  | | 
-| ''​[[reference:​subst]]'' ​      ​?                   |     ​| ​ x  |  x  | ''​subst (asm)''​ | +| ''​[[reference:​subgoal_tac|subgoal_tac]]''​ | a formula ​          ​| ​    ​| ​    ​| ​ x  | | 
-| ''​[[reference:​thin_tac]]'' ​   | a formula ​          ​| ​    ​| ​    ​| ​    | | +| ''​[[reference:​subst|subst]]'' ​            ​a definition (or equation) ​|     ​| ​ x  |  x  | ''​subst (asm)''​ | 
-| ''​[[reference:​unfold]]'' ​     | a definition ​       |  x  |  x  |  ?  | |+| ''​[[reference:​thin_tac|thin_tac]]'' ​      ​| a formula ​          ​| ​    ​| ​    ​| ​    | | 
 +| ''​[[reference:​unfold|unfold]]'' ​          ​| a definition ​(or equation) ​|  x  |  x  |  ?  | |
  
 === Automated Methods === === Automated Methods ===
 +
 ^ Name ^ Classical ^ Simp ^ All goals ^ Safe ^ Splits ^ Finishes ^ Strength ^ Weakness ^ ^ Name ^ Classical ^ Simp ^ All goals ^ Safe ^ Splits ^ Finishes ^ Strength ^ Weakness ^
-| ''​[[reference:​arith]]'' ​   |     ​| ​    ​| ​    ​| ​ x  |     ​| ​ x  | linear arithmetics | exponentially slow for many operators | +| ''​[[reference:​arith|arith]]'' ​      ​|     ​| ​    ​| ​    ​| ​ x  |     ​| ​ x  | linear arithmetics | exponentially slow for many operators | 
-| ''​[[reference:​auto]]'' ​    ​|  x  |  x  |  x  |     ​| ​ x  |     | | | +| ''​[[reference:​auto|auto]]'' ​        ​|  x  |  x  |  x  |     ​| ​ x  |     | | | 
-| ''​[[reference:​blast]]'' ​   |  x  |     ​| ​    ​| ​ x  |     ​| ​ x  | logics, sets; fast | | +| ''​[[reference:​blast|blast]]'' ​      ​|  x  |     ​| ​    ​| ​ x  |     ​| ​ x  | logics, sets; fast | | 
-| ''​[[reference:​clarify]]'' ​ |  x  |     ​| ​    ​| ​ x  |     ​| ​    | | | +| ''​[[reference:​clarify|clarify]]'' ​  ​|  x  |     ​| ​    ​| ​ x  |     ​| ​    | | | 
-| ''​[[reference:​clarsimp]]''​ |  x  |  x  |     ​| ​ x  |     ​| ​    | | | +| ''​[[reference:​clarsimp|clarsimp]]''​ |  x  |  x  |     ​| ​ x  |     ​| ​    | | | 
-| ''​[[reference:​force]]'' ​   |  x  |  x  |     ​| ​ x  |     ​| ​ x  | | | +| ''​[[reference:​force|force]]'' ​      ​|  x  |  x  |     ​| ​ x  |     ​| ​ x  | | | 
-| ''​[[reference:​metis]]'' ​   |  x  |     ​| ​    ​| ​ x  |     ​| ​ x  | logics | no sets | +| ''​[[reference:​metis|metis]]'' ​      ​|  x  |     ​| ​    ​| ​ x  |     ​| ​ x  | logics | no sets | 
-| ''​[[reference:​safe]]'' ​    ​|  x  |     ​| ​ x  |  x  |  x  |     | | | +| ''​[[reference:​safe|safe]]'' ​        ​|  x  |     ​| ​ x  |  x  |  x  |     | | | 
-| ''​[[reference:​simp]]'' ​    ​|     ​| ​ x  |     ​| ​ x  |  x  |     | | | +| ''​[[reference:​simp|simp]]'' ​        ​|     ​| ​ x  |     ​| ​ x  |  x  |     | | | 
-| ''​[[reference:​simp_all]]''​ |     ​| ​ x  |  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. Note that safety of automated proof methods can be sabotaged by adding unsafe rules to rule sets used.
  
Line 211: Line 191:
   * ''​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.   * ''​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$.   * ''​{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.
start.1334310913.txt.gz · Last modified: 2012/04/13 11:55 by 131.246.92.39