User Tools
start
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
start [2012/07/19 14:59] 131.246.92.39 [Assorted gimmicks] |
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. | ||
| Line 14: | Line 14: | ||
| Help us to improve the Wiki by checking and complementing existing content, as well as creating [[wanted pages]]! | 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-x C-s'' -- save the current file | + | |
| - | * ''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) | ||
| - | * [Proof-General -> Advanced -> Customize -> Faces -> Proof Locked Face] -- change the color of the "locked" region of proofs (e.g. Khaki: #F0E68C) | ||
| ===== Syntax ===== | ===== Syntax ===== | ||
| Line 55: | Line 30: | ||
| <code> | <code> | ||
| - | theory Name imports Main | + | theory MyTheory imports Main |
| begin | begin | ||
| - | |||
| - | ... | ||
| - | | ||
| - | $definitions | ||
| ... | ... | ||
| Line 67: | 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>'' | ''<nowiki><-></nowiki>'' or ''='' | ''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 ==== | ||
start.txt · Last modified: 2014/04/30 15:28 by peter
Page Tools
