1 <?xml version='1.0' encoding='iso-8859-1' ?> |
|
2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> |
|
3 <!-- $Id$ --> |
|
4 <html xmlns="http://www.w3.org/1999/xhtml"> |
|
5 |
|
6 <head> |
|
7 <title>Isabelle FAQ</title> |
|
8 <?include file="//include/htmlheader.include.html"?> |
|
9 </head> |
|
10 |
|
11 <body class="main"> |
|
12 <?include file="//include/header.include.html"?> |
|
13 <div class="hr"><hr/></div> |
|
14 <?include file="//include/navigation.include.html"?> |
|
15 <div class="hr"><hr/></div> |
|
16 <div id="content"> |
|
17 |
|
18 <h2>General Questions</h2> |
|
19 |
|
20 <dl class="faq"> |
|
21 |
|
22 <dt>What is Isabelle?</dt> |
|
23 |
|
24 <dd>Isabelle is a popular generic theorem proving environment developed |
|
25 at Cambridge University (<a href= |
|
26 "http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TU Munich |
|
27 (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>). See the |
|
28 <a href="http://isabelle.in.tum.de/">Isabelle homepage</a> for more |
|
29 information.</dd> |
|
30 |
|
31 <dt>Where can I find documentation?</dt> |
|
32 |
|
33 <dd><a href="http://isabelle.in.tum.de/documentation.html">This way, please</a>. |
|
34 Also have a look at the <a href= |
|
35 "http://isabelle.in.tum.de/dist/library/">theory library</a>.</dd> |
|
36 |
|
37 <dt>Is it available for download?</dt> |
|
38 |
|
39 <dd>Yes, it is available from several mirror sites, e. g. from |
|
40 <a href="http://isabelle.in.tum.de">Munich</a>. It runs on common |
|
41 Unix systems (Linux, MacOS X, Solaris, etc.).</dd> |
|
42 |
|
43 </dl> |
|
44 <h2>Syntax</h2> |
|
45 |
|
46 <dl class="faq"> |
|
47 |
|
48 <dt>There are lots of arrows in Isabelle/HOL. What's the difference between |
|
49 <tt>-></tt>, <tt>=></tt>, <tt>--></tt>, and <tt>==></tt> |
|
50 ?</dt> |
|
51 |
|
52 <dd>Isabelle uses the <tt>=></tt> arrow for the function type |
|
53 (contrary to most functional languages which use <tt>-></tt>). So |
|
54 <tt>a => b</tt> is the type of a function that takes an element of |
|
55 <tt>a</tt> as input and gives you an element of <tt>b</tt> as output. The |
|
56 long arrow <tt>--></tt> and <tt>==></tt> are object and meta level |
|
57 implication. Roughly speaking, the meta level implication should only be |
|
58 used when stating theorems where it separates the assumptions from the |
|
59 conclusion. Whenever you need an implication inside a HOL formula, use |
|
60 <code>--></code>.</dd> |
|
61 |
|
62 <dt>Where do I have to put those double quotes?</dt> |
|
63 |
|
64 <dd>Isabelle distinguishes between <em>inner</em> and <em>outer</em> |
|
65 syntax. The outer syntax comes from the Isabelle framework, the inner |
|
66 syntax is the one in between quotation marks and comes from the object |
|
67 logic (in this case HOL). With time the distinction between the two |
|
68 becomes obvious, but in the beginning the following rules of thumb may |
|
69 work: types should be inside quotation marks, formulas and lemmas should |
|
70 be inside quotation marks, rules and equations (e.g. for definitions) |
|
71 should be inside quotation marks, commands like <tt>lemma</tt>, |
|
72 <tt>consts</tt>, <tt>primrec</tt>, <tt>constdefs</tt>, <tt>apply</tt>, |
|
73 <tt>done</tt> are without quotation marks, as are the names of constants |
|
74 in constant definitions (<tt>consts</tt> and <tt>constdefs</tt>)</dd> |
|
75 |
|
76 <dt>What is <tt>"No such constant: _case_syntax"</tt> supposed to tell |
|
77 me?</dt> |
|
78 |
|
79 <dd>You get this message if you use a case construct on a datatype and |
|
80 have a typo in the names of the constructor patterns or if the order of |
|
81 the constructors in the case pattern is different from the order in which |
|
82 they where defined (in the datatype definition).</dd> |
|
83 |
|
84 <dt>Why doesn't Isabelle/HOL understand my equation?</dt> |
|
85 |
|
86 <dd>Isabelle's equality <tt>=</tt> binds relatively strongly, so an |
|
87 equation like <tt>a = b & c</tt> might not be what you intend. |
|
88 Isabelle parses it as <tt>(a = b) & c</tt>. If you want it the other |
|
89 way around, you must set explicit parentheses as in <tt>a = (b & |
|
90 c)</tt>. This also applies to e.g. <tt>primrec</tt> definitions (see |
|
91 below).</dd> |
|
92 |
|
93 <dt>What does it mean "not a proper equation"?</dt> |
|
94 |
|
95 <dd>Most commonly this is an instance of the question above. The |
|
96 <tt>primrec</tt> command (and others) expect equations as input, and |
|
97 since equality binds strongly in Isabelle/HOL, something like <tt>f x = b |
|
98 & c</tt> is not what you might expect it to be: Isabelle parses it as |
|
99 <tt>(f x = b) & c</tt> (which is indeed not a proper equation). To |
|
100 turn it into an equation you must set explicit parentheses: <tt>f x = (b |
|
101 & c)</tt>.</dd> |
|
102 |
|
103 <dt>What does it mean "<tt>Not a meta-equality (==)</tt>"?</dt> |
|
104 |
|
105 <dd>This usually occurs if you use <tt>=</tt> for <tt>constdefs</tt>. The |
|
106 <tt>constdefs</tt> and <tt>defs</tt> commands expect not equations, but |
|
107 meta equivalences. Just use the <tt>\<equiv></tt> or <tt>==</tt> |
|
108 signs instead of <tt>=</tt>.</dd> |
|
109 |
|
110 </dl> |
|
111 <h2>Proving</h2> |
|
112 |
|
113 <dl class="faq"> |
|
114 |
|
115 <dt>What does "empty result sequence" mean?</dt> |
|
116 |
|
117 <dd>It means that the applied proof method (or tactic) was unsuccessful. |
|
118 It did not transform the goal in any way, or simply just failed to do |
|
119 anything. You must try another tactic (or give the one you used more |
|
120 hints or lemmas to work with)</dd> |
|
121 |
|
122 <dt>The Simplifier doesn't want to apply my rule, what's wrong?</dt> |
|
123 |
|
124 <dd>Most commonly this is a typing problem. The rule you want to apply |
|
125 may require a more special (or just plain different) type from what you |
|
126 have in the current goal. Use the ProofGeneral menu <tt>Isabelle/Isar |
|
127 -> Settings -> Show Types</tt> and the <tt>thm</tt> command on the |
|
128 rule you want to apply to find out if the types are what you expect them |
|
129 to be (also take a look at the types in your goal). <tt>Show Sorts</tt>, |
|
130 <tt>Show Constants</tt>, and <tt>Trace Simplifier</tt> in the same menu |
|
131 may also be helpful.</dd> |
|
132 |
|
133 <dt>If I do <tt>auto</tt>, it leaves me a goal <tt>False</tt>. Is my |
|
134 theorem wrong?</dt> |
|
135 |
|
136 <dd>Not necessarily. It just means that <tt>auto</tt> transformed the |
|
137 goal into something that is not provable any more. That could be due to |
|
138 <tt>auto</tt> doing something stupid, or e.g. due to some earlier step in |
|
139 the proof that lost important information. It is of course also possible |
|
140 that the goal was never provable in the first place.</dd> |
|
141 |
|
142 <dt>Why does <tt>lemma "1+1=2"</tt> fail?</dt> |
|
143 |
|
144 <dd>Because it is not necessarily true. Isabelle/HOL does not assume that 1 |
|
145 and 2 are natural numbers. Try <tt>"(1::nat)+1=2"</tt> instead.</dd> |
|
146 |
|
147 <dt>Can Isabelle/HOL find counterexamples?</dt> |
|
148 |
|
149 <dd> |
|
150 <p>For arithmetic goals, <code>arith</code> finds counterexamples. For |
|
151 executable goals, <code>quickcheck</code> tries to find a |
|
152 counterexample. For goals of a more logical nature (including |
|
153 quantifiers, sets and inductive definitions) <code>refute</code> |
|
154 searches for a countermodel.</p> |
|
155 |
|
156 <p>Otherwise, negate the proposition and instantiate (some) variables |
|
157 with concrete values. You may also need additional assumptions about |
|
158 these values. For example, <tt>True & False ~= True | False</tt> is |
|
159 a counterexample of <tt>A & B = A | B</tt>, and <tt>A = ~B ==> A |
|
160 & B ~= A | B</tt> is another one. Sometimes Isabelle can help you |
|
161 to find the counterexample: just negate the proposition and do |
|
162 <tt>auto</tt> or <tt>simp</tt>. If lucky, you are left with the |
|
163 assumptions you need for the counterexample to work.</p> |
|
164 </dd> |
|
165 |
|
166 </dl> |
|
167 <h2>Interface</h2> |
|
168 |
|
169 <dl class="faq"> |
|
170 |
|
171 <dt>X-Symbol doesn't seem to work. What can I do?</dt> |
|
172 |
|
173 <dd>The most common reason why X-Symbol doesn't work is: it's not |
|
174 switched on yet. Assuming you are using ProofGeneral and have installed |
|
175 the X-Symbol package, you still need to turn X-Symbol on in ProofGeneral: |
|
176 select the menu items <tt>Proof-General -> Options -> X-Symbol</tt> |
|
177 and (if you want to save the setting for future sessions) select |
|
178 <tt>Options -> Save Options</tt> in XEmacs.</dd> |
|
179 |
|
180 <dt>How do I input those X-Symbols anyway?</dt> |
|
181 |
|
182 <dd>There are lots of ways to input x-symbols. The one that always works |
|
183 is writing it out in plain text (e.g. for the 'and' symbol type |
|
184 <tt>\<and></tt>). For common symbols you can try to "paint them in |
|
185 ASCII" and if the xsymbol package recognizes them it will automatically |
|
186 convert them into their graphical representation. Examples: |
|
187 <tt>--></tt> is converted into the long single arrow, <tt>/\</tt> is |
|
188 converted into the 'and' symbol, the sequence <tt>=_</tt> into the |
|
189 equivalence sign, <tt><_</tt> into less-or-equal, <tt>[|</tt> into |
|
190 opening semantic brackets, and so on. For greek characters, the |
|
191 <code>rotate</code> command works well: to input α type |
|
192 <code>a</code> and then <code>C-.</code> (control and <code>.</code>). |
|
193 You can also display the grid-of-characters in the x-symbol menu to get |
|
194 an overview of the available graphical representations (not all of them |
|
195 already have a meaning in Isabelle, though).</dd> |
|
196 |
|
197 </dl> |
|
198 <h2>System</h2> |
|
199 |
|
200 <dl class="faq"> |
|
201 |
|
202 <dt>I want to generate one of those flashy LaTeX documents. How?</dt> |
|
203 |
|
204 <dd>You will need to work with the <tt class="shellcmd">isatool</tt> command for this (in |
|
205 a Unix shell). The easiest way to get to a document is the following: use |
|
206 <tt class="shellcmd">isatool mkdir</tt> to set up a new directory. The command will also |
|
207 create a file called <tt class="shellcmd">IsaMakefile</tt> in the current directory. Put |
|
208 your theory file(s) into the new directory and edit the file |
|
209 <tt class="shellcmd">ROOT.ML</tt> in there (following the comments) to tell Isabelle which |
|
210 of the theories to load (and in which order). Go back to the parent |
|
211 directory (where the <tt class="shellcmd">IsaMakefile</tt> is) and type <tt class="shellcmd">isatool |
|
212 make</tt>. Isabelle should then process your theories and tell you where |
|
213 to find the finished document. For more information on generating |
|
214 documents see the Isabelle Tutorial, Chapter 4.</dd> |
|
215 |
|
216 <dt>I have a large formalization with many theories. Must I process all |
|
217 of them all of the time?</dt> |
|
218 |
|
219 <dd>No, you can tell Isabelle to build a so-called heap image. This heap |
|
220 image can contain your preloaded theories. To get one, set up a directory |
|
221 with a <tt class="shellcmd">ROOT.ML</tt> file (as for generating a document) and use the |
|
222 command <tt class="shellcmd">isatool usedir -b HOL MyImage</tt> in that directory to |
|
223 create an image <tt class="shellcmd">MyImage</tt> using the parent logic <tt class="shellcmd">HOL</tt>. You |
|
224 should then be able to invoke Isabelle with <tt class="shellcmd">Isabelle -l MyImage</tt> |
|
225 and have everything that is loaded in ROOT.ML instantly available.</dd> |
|
226 |
|
227 <dt>Can I run Isabelle on Windows?</dt> |
|
228 |
|
229 <dd>Not really. The Cygwin environment provides a Unixoid |
|
230 look-and-feel that is sufficient for very basic Isabelle |
|
231 functionality. See also <a |
|
232 href="installation_notes_cygwin.html">Installation notes for |
|
233 Cygwin/Windows.</a> |
|
234 |
|
235 To try out Isabelle it might be much easier to use a Linux boot |
|
236 CD, such as <a href="http://www.knoppix.org/">Knoppix</a>.</dd> |
|
237 |
|
238 </dl> |
|
239 |
|
240 </div> |
|
241 <div class="hr"><hr/></div> |
|
242 <?include file="//include/footer.include.html"?> |
|
243 </body> |
|
244 |
|
245 </html> |
|