|
1 %title% |
|
2 Isabelle FAQ |
|
3 |
|
4 %meta% |
|
5 <style type="text/css"> |
|
6 <!-- |
|
7 .question { background-color:#C0C0C0; color:#000001; padding:3px; margin-top:12px; font-weight: bold; } |
|
8 .answer { background-color:#E0E0E0; padding:3px; margin-top:3px; } |
|
9 --> |
|
10 </style> |
|
11 |
|
12 |
|
13 %body% |
|
14 <h2>General Questions</h2> |
|
15 <table class="question" width="100%"> |
|
16 <tr> |
|
17 <td>What is Isabelle?</td> |
|
18 </tr> |
|
19 </table> |
|
20 |
|
21 <table class="answer" width="100%"> |
|
22 <tr><td>Isabelle is a popular generic theorem proving |
|
23 environment developed at Cambridge University (<a |
|
24 href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) |
|
25 and TU Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias |
|
26 Nipkow</a>). See the <a |
|
27 href="http://isabelle.in.tum.de/">Isabelle homepage</a> for |
|
28 more information.</td></tr> |
|
29 </table> |
|
30 |
|
31 |
|
32 <table class="question" width="100%"> |
|
33 <tr> |
|
34 <td>Where can I find documentation?</td> |
|
35 </tr> |
|
36 </table> |
|
37 <table class="answer" width="100%"> |
|
38 <tr><td><a href="http://isabelle.in.tum.de/docs.html">This |
|
39 way, please</a>. Also have a look at the <a |
|
40 href="http://isabelle.in.tum.de/library/">theory |
|
41 library</a>.</td></tr> |
|
42 </table> |
|
43 |
|
44 <table class="question" width="100%"> |
|
45 <tr> |
|
46 <td>Is it available for download?</td> |
|
47 </tr> |
|
48 </table> <table class="answer" width="100%"> <tr><td>Yes, it is |
|
49 available from <a |
|
50 href="http://isabelle.in.tum.de/dist/">several mirror |
|
51 sites</a>. It should run on most recent Unix systems (Solaris, |
|
52 Linux, MacOS X, etc.).</td></tr> |
|
53 </table> |
|
54 |
|
55 |
|
56 <h2>Syntax</h2> |
|
57 <table class="question" width="100%"> |
|
58 <tr> |
|
59 <td>There are lots of arrows in Isabelle. What's the |
|
60 difference between <tt>-></tt>, <tt>=></tt>, <tt>--></tt>, |
|
61 and <tt>==></tt> ?</td> |
|
62 </tr> |
|
63 </table> |
|
64 <table class="answer" width="100%"> |
|
65 <tr><td>Isabelle uses the <tt>=></tt> arrow for the function |
|
66 type (contrary to most functional languages which use |
|
67 <tt>-></tt>). So <tt>a => b</tt> is the type of a function |
|
68 that takes an element of <tt>a</tt> as input and gives you an |
|
69 element of <tt>b</tt> as output. The long arrow <tt>--></tt> |
|
70 and <tt>==></tt> are object and meta level |
|
71 implication. Roughly speaking, the meta level implication is |
|
72 used to write down theorems (<tt>P ==> Q</tt> is a theorem |
|
73 with <tt>P</tt> as premise and <tt>Q</tt> as conclusion), and |
|
74 the object level implication is used in usual HOL formulas |
|
75 (e.g. in definitions).</td></tr> |
|
76 </table> |
|
77 |
|
78 <table class="question" width="100%"><tr><td>Where do I have to put those double quotes?</td></tr></table> |
|
79 |
|
80 <table class="answer" width="100%"><tr><td>Isabelle distinguishes between <em>inner</em> |
|
81 and <em>outer</em> syntax. The outer syntax comes from the |
|
82 Isabelle framework, the inner syntax is the one in between |
|
83 quotation marks and comes from the object logic (in this case HOL). |
|
84 With time the distinction between the two becomes obvious, but in |
|
85 the beginning the following rules of thumb may work: types should |
|
86 be inside quotation marks, formulas and lemmas should be inside |
|
87 quotation marks, rules and equations (e.g. for definitions) should |
|
88 be inside quotation marks, commands like <tt>lemma</tt>, |
|
89 <tt>consts</tt>, <tt>primrec</tt>, <tt>constdefs</tt>, |
|
90 <tt>apply</tt>, <tt>done</tt> are without quotation marks, as are |
|
91 the names of constants in constant definitions (<tt>consts</tt> |
|
92 and <tt>constdefs</tt>) |
|
93 </td></tr></table> |
|
94 |
|
95 <table class="question" width="100%"><tr><td>What is <tt>No such |
|
96 constant: "_case_syntax"</tt> supposed to tell |
|
97 me?</td></tr></table> |
|
98 |
|
99 <table class="answer" width="100%"><tr><td>You get this message if |
|
100 you use a case construct on a datatype and have a typo in the |
|
101 names of the constructor patterns or if the order of the |
|
102 constructors in the case pattern is different from the order in |
|
103 which they where defined (in the datatype definition). |
|
104 </td></tr></table> |
|
105 |
|
106 <table class="question" width="100%"><tr><td>Why doesn't Isabelle understand my |
|
107 equation?</td></tr></table> |
|
108 |
|
109 <table class="answer" width="100%"><tr><td>Isabelle's equality <tt>=</tt> binds |
|
110 relatively strongly, so an equation like <tt>a = b & c</tt> might |
|
111 not be what you intend. Isabelle parses it as <tt>(a = b) & |
|
112 c</tt>. If you want it the other way around, you must set |
|
113 explicit parentheses as in <tt>a = (b & c)</tt>. This also applies |
|
114 to e.g. <tt>primrec</tt> definitions (see below).</td></tr></table> |
|
115 |
|
116 <table class="question" width="100%"><tr><td>What does it mean "not a proper |
|
117 equation"?</td></tr></table> |
|
118 |
|
119 <table class="answer" width="100%"><tr><td>Most commonly this is an instance of the |
|
120 question above. The <tt>primrec</tt> command (and others) expect |
|
121 equations as input, and since equality binds strongly in Isabelle, |
|
122 something like <tt>f x = b & c</tt> is not what you might expect |
|
123 it to be: Isabelle parses it as <tt>(f x = b) & c</tt> (which is |
|
124 indeed not a proper equation). To turn it into an equation you |
|
125 must set explicit parentheses: <tt>f x = (b & c)</tt>.</td></tr></table> |
|
126 |
|
127 <table class="question" width="100%"><tr><td>What does it mean |
|
128 "<tt>Not a meta-equality (==)</tt>"?</td></tr></table> |
|
129 |
|
130 <table class="answer" width="100%"><tr><td>This usually occurs if |
|
131 you use <tt>=</tt> for <tt>constdefs</tt>. The <tt>constdefs</tt> |
|
132 and <tt>defs</tt> commands expect not equations, but meta |
|
133 equivalences. Just use the <tt>\<equiv></tt> or <tt>==</tt> |
|
134 signs instead of <tt>=</tt>. </td></tr></table> |
|
135 |
|
136 |
|
137 <h2>Proving</h2> |
|
138 |
|
139 <table class="question" width="100%"><tr><td>What does "empty result sequence" |
|
140 mean?</td></tr></table> |
|
141 |
|
142 <table class="answer" width="100%"><tr><td>It means that the applied proof method (or |
|
143 tactic) was unsuccessful. It did not transform the goal in any |
|
144 way, or simply just failed to do anything. You must try another |
|
145 tactic (or give the one you used more hints or lemmas to work |
|
146 with)</td></tr></table> |
|
147 |
|
148 |
|
149 <table class="question" width="100%"><tr><td>The Simplifier doesn't want to apply my |
|
150 rule, what's wrong?</td></tr></table> |
|
151 |
|
152 <table class="answer" width="100%"><tr><td> |
|
153 Most commonly this is a typing problem. The rule you want to apply |
|
154 may require a more special (or just plain different) type from |
|
155 what you have in the current goal. Use the ProofGeneral menu |
|
156 <tt>Isabelle/Isar -> Settings -> Show Types</tt> and the |
|
157 <tt>thm</tt> command on the rule you want to apply to find out if |
|
158 the types are what you expect them to be (also take a look at the |
|
159 types in your goal). <tt>Show Sorts</tt>, <tt>Show Constants</tt>, |
|
160 and <tt>Trace Simplifier</tt> in the same menu may also be |
|
161 helpful. |
|
162 </td></tr></table> |
|
163 |
|
164 |
|
165 <table class="question" width="100%"><tr><td>If I do <tt>auto</tt>, it leaves me a goal |
|
166 <tt>False</tt>. Is my theorem wrong?</td></tr></table> |
|
167 |
|
168 <table class="answer" width="100%"><tr><td>Not necessarily. It just means that |
|
169 <tt>auto</tt> transformed the goal into something that is not |
|
170 provable any more. That could be due to <tt>auto</tt> doing |
|
171 something stupid, or e.g. due to some earlier step in the proof |
|
172 that lost important information. It is of course also possible |
|
173 that the goal was never provable in the first place.</td></tr></table> |
|
174 |
|
175 |
|
176 <table class="question" width="100%"><tr><td>Why does <tt>lemma |
|
177 "1+1=2"</tt> fail?</td></tr></table> |
|
178 |
|
179 <table class="answer" width="100%"><tr><td>Because it is not |
|
180 necessarily true. Isabelle does not assume that 1 and 2 are |
|
181 natural numbers. Try <tt>"(1::nat)+1=2"</tt> |
|
182 instead.</td></tr></table> |
|
183 |
|
184 |
|
185 <table class="question" width="100%"><tr><td>How do I show |
|
186 counter examples?</td></tr></table> |
|
187 |
|
188 <table class="answer" width="100%"><tr><td> |
|
189 There are a number of commands that try to find counter examples |
|
190 automatically. Try <code>quickcheck</code> for small executable |
|
191 examples and <code>arith</code> for Presburger arithmetic. |
|
192 Otherwise, negate the proposition |
|
193 and instantiate (some) variables with concrete values. You may |
|
194 also need additional assumptions about these values. For example, |
|
195 <tt>True & False ~= True | False</tt> is a counterexample of <tt>A |
|
196 & B = A | B</tt>, and <tt>A = ~B ==> A & B ~= A | B</tt> is |
|
197 another one. Sometimes Isabelle can help you to find the |
|
198 counter example: just negate the proposition and do <tt>auto</tt> |
|
199 or <tt>simp</tt>. If lucky, you are left with the assumptions you |
|
200 need for the counter example to work.</td></tr></table> |
|
201 |
|
202 |
|
203 <h2>Interface</h2> |
|
204 |
|
205 <table class="question" width="100%"><tr><td>X-Symbol doesn't seem to work. What can I |
|
206 do?</td></tr></table> |
|
207 |
|
208 <table class="answer" width="100%"><tr><td>The most common reason why X-Symbol doesn't |
|
209 work is: it's not switched on yet. Assuming you are using |
|
210 ProofGeneral and have installed the X-Symbol package, you still |
|
211 need to turn X-Symbol on in ProofGeneral: select the menu items |
|
212 <tt>Proof-General -> Options -> X-Symbol</tt> and (if you want to |
|
213 save the setting for future sessions) select <tt>Options -> Save |
|
214 Options</tt> in XEmacs.</td></tr></table> |
|
215 |
|
216 <table class="question" width="100%"><tr><td>How do I input those X-Symbols anyway?</td></tr></table> |
|
217 |
|
218 <table class="answer" width="100%"><tr><td> |
|
219 There are lots of ways to input x-symbols. The one that always |
|
220 works is writing it out in plain text (e.g. for the 'and' symbol |
|
221 type <tt>\<and></tt>). For common symbols you can try to "paint |
|
222 them in ASCII" and if the xsymbol package recognizes them it will |
|
223 automatically convert them into their graphical |
|
224 representation. Examples: <tt>--></tt> is converted into the long |
|
225 single arrow, <tt>/\</tt> is converted into the 'and' symbol, the |
|
226 sequence <tt>=_</tt> into the equivalence sign, <tt><_</tt> into |
|
227 less-or-equal, <tt>[|</tt> into opening semantic brackets, and so |
|
228 on. For greek characters, the <code>rotate</code> command works well: |
|
229 to input α type <code>a</code> and then <code>C-.</code> |
|
230 (control and <code>.</code>). You can also display the |
|
231 grid-of-characters in the x-symbol menu to get an overview of the |
|
232 available graphical representations (not all of them already have |
|
233 a meaning in Isabelle, though). |
|
234 </td></tr></table> |
|
235 |
|
236 <h2>System</h2> |
|
237 |
|
238 <table class="question" width="100%"><tr><td>I want to generate one of those flashy LaTeX |
|
239 documents. How?</td></tr></table> |
|
240 |
|
241 <table class="answer" width="100%"><tr><td>You will need to work with the |
|
242 <tt>isatool</tt> command for this (in a Unix shell). The easiest |
|
243 way to get to a document is the following: use <tt>isatool |
|
244 mkdir</tt> to set up a new directory. The command will also create |
|
245 a file called <tt>IsaMakefile</tt> in the current directory. Put |
|
246 your theory file(s) into the new directory and edit the file |
|
247 <tt>ROOT.ML</tt> in there (following the comments) to tell |
|
248 Isabelle which of the theories to load (and in which order). Go |
|
249 back to the parent directory (where the <tt>IsaMakefile</tt> is) |
|
250 and type <tt>isatool make</tt>. Isabelle should then process your |
|
251 theories and tell you where to find the finished document. For |
|
252 more information on generating documents see the Isabelle Tutorial, Chapter 4. |
|
253 </td></tr></table> |
|
254 |
|
255 |
|
256 <table class="question" width="100%"><tr><td>I have a large formalization with many |
|
257 theories. Must I process all of them all of the time?</td></tr></table> |
|
258 |
|
259 <table class="answer" width="100%"><tr><td>No, you can tell Isabelle to build a so-called |
|
260 heap image. This heap image can contain your preloaded |
|
261 theories. To get one, set up a directory with a <tt>ROOT.ML</tt> |
|
262 file (as for generating a document) and use the command |
|
263 <tt>isatool usedir -b HOL MyImage</tt> in that directory to create |
|
264 an image <tt>MyImage</tt> using the parent logic <tt>HOL</tt>. |
|
265 You should then be able to invoke Isabelle with <tt>Isabelle -l |
|
266 MyImage</tt> and have everything that is loaded in ROOT.ML |
|
267 instantly available.</td></tr></table> |
|
268 |
|
269 <table class="question" width="100%"><tr><td>Does Isabelle run on Windows?</td></tr></table> |
|
270 |
|
271 <table class="answer" width="100%"><tr><td> After a fashion, yes, |
|
272 but Isabelle is not being developed for Windows. A friendly user |
|
273 (Norbert Völker) has managed to get a minimal Isabelle environment |
|
274 to work on it. See the description on <a |
|
275 href="http://cswww.essex.ac.uk/Research/FSS/projects/isawin/">his |
|
276 website</a>. Be warned, though: emphasis is on <em>minimal</em>, |
|
277 working with Windows is no fun at all. To enjoy Isabelle in its |
|
278 full beauty it is recommended to get a Linux distribution (they |
|
279 are inexpensive, any reasonably recent one should work, dualboot |
|
280 Windows/Linux should pose no problems). |
|
281 </td></tr></table> |
|
282 |