This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
start [2011/07/20 12:56] 131.246.161.187 |
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 tux1, tux2, 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 a terminal. |
- | * ''n'' -- next: process the next line in Isabelle | + | |
- | * ''p'' -- show the current state of a proof (for instance, in 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 a 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 105: | Line 81: | ||
===== Proofs ===== | ===== Proofs ===== | ||
- | Apply method ''$method'' with parameters ''$params'' by entering ''apply ($method $params)''. If you have no parameters, you can just write ''apply $method''. | + | 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 ==== | ==== Methods ==== | ||
+ | |||
=== Basic Methods === | === Basic Methods === | ||
- | ^ Name ^ Parameters ^ All goals ^ Safe ^ New Goals ^ Variants ^ | + | |
- | | ''[[reference:assumption]]'' | --- | | ⚫ | | | | + | ^ Name ^ Parameters ^ All goals ^ Safe ^ New Goals ^ Variants ^ |
- | | ''[[reference:cases]]'' | an expression | | ⚫ | ⚫ | ''case_tac'' | | + | | ''[[reference:assumption|assumption]]'' | --- | | x | | | |
- | | ''[[reference:drule]]'' | a rule | | | ⚫ | ''drule(k)'', ''drule_tac'' | | + | | ''[[reference:cases|cases]]'' | an expression | | x | x | ''case_tac'' | |
- | | ''[[reference:erule]]'' | a rule | | | ⚫ | ''erule(k)'', ''erule_tac'' | | + | | ''[[reference:drule|drule]]'' | a rule | | | x | ''drule(k)'', ''drule_tac'' | |
- | | ''[[reference:fold]]'' | ? | ⚫ | ⚫ | ? | | | + | | ''[[reference:erule|erule]]'' | a rule | | | x | ''erule(k)'', ''erule_tac'' | |
- | | ''[[reference:frule]]'' | a rule | | ⚫ | ⚫ | ''frule(k)'', ''frule_tac'' | | + | | ''[[reference:fold|fold]]'' | a definition (or equation) | x | x | | | |
- | | ''[[reference:induct]]'' | a variable | | | ⚫ | ''induct_tac'' | | + | | ''[[reference:frule|frule]]'' | a rule | | x | x | ''frule(k)'', ''frule_tac'' | |
- | | ''[[reference:insert]]'' | a theorem | ⚫ | ⚫ | | ''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 | | ⚫ | | | | + | | ''[[reference:rename_tac|rename_tac]]'' | list of identifiers | | | | | |
- | | ''[[reference:rule (method)|rule]]'' | a rule | | | ⚫ | ''rule(k)'', ''rule_tac'' | | + | | ''[[reference:rotate_tac|rotate_tac]]'' | an integer | | x | | | |
- | | ''[[reference:split]]'' | a splitting rule | | ? | ⚫ | | | + | | ''[[reference:rule (method)|rule]]'' | a rule | | | x | ''rule(k)'', ''rule_tac'' | |
- | | ''[[reference:subgoal_tac]]'' | a formula | | | ⚫ | | | + | | ''[[reference:split|split]]'' | a splitting rule | | ? | x | | |
- | | ''[[reference:subst]]'' | ? | | ⚫ | ⚫ | ''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 | ⚫ | ⚫ | ? | | | + | | ''[[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]]'' | | | | ⚫ | | ⚫ | linear arithmetics | exponentially slow for many operators | | + | | ''[[reference:arith|arith]]'' | | | | x | | x | linear arithmetics | exponentially slow for many operators | |
- | | ''[[reference:auto]]'' | ⚫ | ⚫ | ⚫ | | ⚫ | | | | | + | | ''[[reference:auto|auto]]'' | x | x | x | | x | | | | |
- | | ''[[reference:blast]]'' | ⚫ | | | ⚫ | | ⚫ | logics, sets; fast | | | + | | ''[[reference:blast|blast]]'' | x | | | x | | x | logics, sets; fast | | |
- | | ''[[reference:clarify]]'' | ⚫ | | | ⚫ | | | | | | + | | ''[[reference:clarify|clarify]]'' | x | | | x | | | | | |
- | | ''[[reference:clarsimp]]'' | ⚫ | ⚫ | | ⚫ | | | | | | + | | ''[[reference:clarsimp|clarsimp]]'' | x | x | | x | | | | | |
- | | ''[[reference:force]]'' | ⚫ | ⚫ | | ⚫ | | ⚫ | | | | + | | ''[[reference:force|force]]'' | x | x | | x | | x | | | |
- | | ''[[reference:metis]]'' | ⚫ | | | ⚫ | | ⚫ | logics | no sets | | + | | ''[[reference:metis|metis]]'' | x | | | x | | x | logics | no sets | |
- | | ''[[reference:safe]]'' | ⚫ | | ⚫ | ⚫ | ⚫ | | | | | + | | ''[[reference:safe|safe]]'' | x | | x | x | x | | | | |
- | | ''[[reference:simp]]'' | | ⚫ | | ⚫ | ⚫ | | | | | + | | ''[[reference:simp|simp]]'' | | x | | x | x | | | | |
- | | ''[[reference:simp_all]]'' | | ⚫ | ⚫ | ⚫ | ⚫ | | | | | + | | ''[[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 207: | 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. |