|
16233
|
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">
|
|
16240
|
3 |
<!-- $Id$ -->
|
|
16233
|
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 |
|
|
17563
|
33 |
<dd><a href="http://isabelle.in.tum.de/documentation.html">This way, please</a>.
|
|
16233
|
34 |
Also have a look at the <a href=
|
|
17563
|
35 |
"http://isabelle.in.tum.de/dist/library/">theory library</a>.</dd>
|
|
16233
|
36 |
|
|
|
37 |
<dt>Is it available for download?</dt>
|
|
|
38 |
|
|
17563
|
39 |
<dd>Yes, it is available from several mirror sites, e. g. from
|
|
17661
|
40 |
<a href="http://isabelle.in.tum.de">Munich</a>. It runs on common
|
|
|
41 |
Unix systems (Linux, MacOS X, Solaris, etc.).</dd>
|
|
16233
|
42 |
|
|
|
43 |
</dl>
|
|
|
44 |
<h2>Syntax</h2>
|
|
|
45 |
|
|
|
46 |
<dl class="faq">
|
|
|
47 |
|
|
17661
|
48 |
<dt>There are lots of arrows in Isabelle/HOL. What's the difference between
|
|
16233
|
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 |
|
|
17661
|
84 |
<dt>Why doesn't Isabelle/HOL understand my equation?</dt>
|
|
16233
|
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
|
|
17661
|
97 |
since equality binds strongly in Isabelle/HOL, something like <tt>f x = b
|
|
16233
|
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 |
|
|
17661
|
144 |
<dd>Because it is not necessarily true. Isabelle/HOL does not assume that 1
|
|
16233
|
145 |
and 2 are natural numbers. Try <tt>"(1::nat)+1=2"</tt> instead.</dd>
|
|
|
146 |
|
|
17661
|
147 |
<dt>Can Isabelle/HOL find counterexamples?</dt>
|
|
16233
|
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>
|
|
17661
|
179 |
|
|
16233
|
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 |
|
|
16240
|
204 |
<dd>You will need to work with the <tt class="shellcmd">isatool</tt> command for this (in
|
|
16233
|
205 |
a Unix shell). The easiest way to get to a document is the following: use
|
|
16240
|
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
|
|
16233
|
208 |
your theory file(s) into the new directory and edit the file
|
|
16240
|
209 |
<tt class="shellcmd">ROOT.ML</tt> in there (following the comments) to tell Isabelle which
|
|
16233
|
210 |
of the theories to load (and in which order). Go back to the parent
|
|
16240
|
211 |
directory (where the <tt class="shellcmd">IsaMakefile</tt> is) and type <tt class="shellcmd">isatool
|
|
16233
|
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
|
|
16240
|
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>
|
|
16233
|
225 |
and have everything that is loaded in ROOT.ML instantly available.</dd>
|
|
17661
|
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>
|
|
16233
|
237 |
|
|
|
238 |
</dl>
|
|
|
239 |
|
|
|
240 |
</div>
|
|
|
241 |
<div class="hr"><hr/></div>
|
|
|
242 |
<?include file="//include/footer.include.html"?>
|
|
|
243 |
</body>
|
|
|
244 |
|
|
|
245 |
</html>
|