2
|
1 |
theory Intro
|
75
|
2 |
imports Base
|
2
|
3 |
begin
|
|
4 |
|
346
|
5 |
(*<*)
|
|
6 |
setup{*
|
|
7 |
open_file_with_prelude
|
|
8 |
"Intro_Code.thy"
|
|
9 |
["theory Intro", "imports Main", "begin"]
|
|
10 |
*}
|
|
11 |
(*>*)
|
|
12 |
|
2
|
13 |
chapter {* Introduction *}
|
|
14 |
|
|
15 |
text {*
|
295
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
16 |
\begin{flushright}
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
17 |
{\em
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
18 |
``My thesis is that programming is not at the bottom of the intellectual \\
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
19 |
pyramid, but at the top. It's creative design of the highest order. It \\
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
20 |
isn't monkey or donkey work; rather, as Edsger Dijkstra famously \\
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
21 |
claimed, it's amongst the hardest intellectual tasks ever attempted.''} \\[1ex]
|
324
|
22 |
Richard Bornat, In {\em Defence of Programming}. \cite{Bornat-lecture}
|
295
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
23 |
\end{flushright}
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
24 |
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
25 |
\medskip
|
89
|
26 |
If your next project requires you to program on the ML-level of Isabelle,
|
106
bdd82350cf22
renamed in the pdf all instances of cookbook to tutorial (in order to sound more serious)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
27 |
then this tutorial is for you. It will guide you through the first steps of
|
353
|
28 |
Isabelle programming, and also explain tricks of the trade. We also hope
|
|
29 |
the tutorial will encourage researchers to play with Isabelle. The best way to
|
89
|
30 |
get to know the ML-level of Isabelle is by experimenting with the many code
|
106
bdd82350cf22
renamed in the pdf all instances of cookbook to tutorial (in order to sound more serious)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
31 |
examples included in the tutorial. The code is as far as possible checked
|
254
|
32 |
against the Isabelle distribution.\footnote{\input{version}} If something does not work,
|
235
|
33 |
then please let us know. It is impossible for us to know every environment,
|
|
34 |
operating system or editor in which Isabelle is used. If you have comments,
|
|
35 |
criticism or like to add to the tutorial, please feel free---you are most
|
|
36 |
welcome! The tutorial is meant to be gentle and comprehensive. To achieve
|
|
37 |
this we need your feedback.
|
2
|
38 |
*}
|
|
39 |
|
|
40 |
section {* Intended Audience and Prior Knowledge *}
|
|
41 |
|
|
42 |
text {*
|
106
bdd82350cf22
renamed in the pdf all instances of cookbook to tutorial (in order to sound more serious)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
43 |
This tutorial targets readers who already know how to use Isabelle for
|
75
|
44 |
writing theories and proofs. We also assume that readers are familiar with
|
|
45 |
the functional programming language ML, the language in which most of
|
|
46 |
Isabelle is implemented. If you are unfamiliar with either of these two
|
329
|
47 |
subjects, then you should first work through the Isabelle/HOL tutorial
|
75
|
48 |
\cite{isa-tutorial} or Paulson's book on ML \cite{paulson-ml2}.
|
2
|
49 |
*}
|
|
50 |
|
5
|
51 |
section {* Existing Documentation *}
|
2
|
52 |
|
|
53 |
text {*
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
54 |
The following documentation about Isabelle programming already exists (and is
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
55 |
part of the distribution of Isabelle):
|
2
|
56 |
|
|
57 |
\begin{description}
|
162
|
58 |
\item[The Isabelle/Isar Implementation Manual] describes Isabelle
|
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
59 |
from a high-level perspective, documenting both the underlying
|
6
|
60 |
concepts and some of the interfaces.
|
2
|
61 |
|
5
|
62 |
\item[The Isabelle Reference Manual] is an older document that used
|
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
63 |
to be the main reference of Isabelle at a time when all proof scripts
|
89
|
64 |
were written on the ML-level. Many parts of this manual are outdated
|
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
65 |
now, but some parts, particularly the chapters on tactics, are still
|
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
66 |
useful.
|
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
67 |
|
153
|
68 |
\item[The Isar Reference Manual] provides specification material (like grammars,
|
298
|
69 |
examples and so on) about Isar and its implementation.
|
5
|
70 |
\end{description}
|
2
|
71 |
|
234
|
72 |
Then of course there are:
|
5
|
73 |
|
|
74 |
\begin{description}
|
234
|
75 |
\item[The Isabelle sources.] They are the ultimate reference for how
|
2
|
76 |
things really work. Therefore you should not hesitate to look at the
|
|
77 |
way things are actually implemented. More importantly, it is often
|
89
|
78 |
good to look at code that does similar things as you want to do and
|
329
|
79 |
learn from it. This tutorial contains frequently pointers to the
|
|
80 |
Isabelle sources. Still, the UNIX command \mbox{@{text "grep -R"}} is
|
233
|
81 |
often your best friend while programming with Isabelle, or
|
263
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
82 |
hypersearch if you program using jEdit under MacOSX. To understand the sources,
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
83 |
it is often also necessary to track the change history of a file or
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
84 |
files. The Mercurial repository\footnote{\url{http://isabelle.in.tum.de/repos/isabelle/}}
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
85 |
for Isabelle provides convenient interfaces to query the history of
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
86 |
files and ``change sets''.
|
2
|
87 |
\end{description}
|
|
88 |
*}
|
|
89 |
|
252
|
90 |
section {* Typographic Conventions *}
|
68
|
91 |
|
|
92 |
text {*
|
181
|
93 |
All ML-code in this tutorial is typeset in shaded boxes, like the following
|
329
|
94 |
simple ML-expression:
|
75
|
95 |
|
|
96 |
\begin{isabelle}
|
|
97 |
\begin{graybox}
|
85
|
98 |
\isacommand{ML}~@{text "\<verbopen>"}\isanewline
|
75
|
99 |
\hspace{5mm}@{ML "3 + 4"}\isanewline
|
85
|
100 |
@{text "\<verbclose>"}
|
75
|
101 |
\end{graybox}
|
|
102 |
\end{isabelle}
|
|
103 |
|
195
|
104 |
These boxes correspond to how code can be processed inside the interactive
|
343
|
105 |
environment of Isabelle. It is therefore easy to experiment with the code
|
|
106 |
that is given in this tutorial. However, for better readability we will drop
|
|
107 |
the enclosing \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} and just
|
|
108 |
write:
|
81
|
109 |
|
75
|
110 |
@{ML [display,gray] "3 + 4"}
|
|
111 |
|
89
|
112 |
Whenever appropriate we also show the response the code
|
81
|
113 |
generates when evaluated. This response is prefixed with a
|
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
114 |
@{text [quotes] ">"}, like:
|
75
|
115 |
|
|
116 |
@{ML_response [display,gray] "3 + 4" "7"}
|
|
117 |
|
195
|
118 |
The user-level commands of Isabelle (i.e., the non-ML code) are written
|
|
119 |
in \isacommand{bold face} (e.g., \isacommand{lemma}, \isacommand{apply},
|
|
120 |
\isacommand{foobar} and so on). We use @{text "$ \<dots>"} to indicate that a
|
234
|
121 |
command needs to be run in a UNIX-shell, for example:
|
75
|
122 |
|
181
|
123 |
@{text [display] "$ grep -R ThyOutput *"}
|
75
|
124 |
|
89
|
125 |
Pointers to further information and Isabelle files are typeset in
|
195
|
126 |
\textit{italic} and highlighted as follows:
|
75
|
127 |
|
|
128 |
\begin{readmore}
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
129 |
Further information or pointers to files.
|
75
|
130 |
\end{readmore}
|
|
131 |
|
182
|
132 |
The pointers to Isabelle files are hyperlinked to the tip of the Mercurial
|
|
133 |
repository of Isabelle at \href{http://isabelle.in.tum.de/repos/isabelle/}
|
|
134 |
{http://isabelle.in.tum.de/repos/isabelle/}.
|
|
135 |
|
177
|
136 |
A few exercises are scattered around the text. Their solutions are given
|
156
|
137 |
in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try
|
162
|
138 |
to solve the exercises on your own, and then look at the solutions.
|
233
|
139 |
*}
|
156
|
140 |
|
263
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
141 |
section {* Aaaaargh! My Code Does not Work Anymore *}
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
142 |
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
143 |
text {*
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
144 |
One unpleasant aspect of any code development inside a larger system is that
|
329
|
145 |
one has to aim at a ``moving target''. Isabelle is no exception. Every
|
263
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
146 |
update lets potentially all hell break loose, because other developers have
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
147 |
changed code you are relying on. Cursing is somewhat helpful in such situations,
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
148 |
but taking the view that incompatible code changes are a fact of life
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
149 |
might be more gratifying. Isabelle is a research project. In most circumstances
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
150 |
it is just impossible to make research backward compatible (imagine Darwin
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
151 |
attempting to make the Theory of Evolution backward compatible).
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
152 |
|
329
|
153 |
However, there are a few steps you can take to mitigate unwanted
|
|
154 |
interferences with code changes from other developers. First, you can base
|
|
155 |
your code on the latest stable release of Isabelle (it is aimed to have one
|
|
156 |
such release at least once every year). This might cut you off from the
|
|
157 |
latest feature implemented in Isabelle, but at least you do not have to
|
|
158 |
track side-steps or dead-ends in the Isabelle development. Of course this
|
|
159 |
means also you have to synchronise your code at the next stable release. If
|
|
160 |
you do not synchronise, be warned that code seems to ``rot'' very
|
|
161 |
quickly. Another possibility is to get your code into the Isabelle
|
|
162 |
distribution. For this you have to convince other developers that your code
|
|
163 |
or project is of general interest. If you managed to do this, then the
|
|
164 |
problem of the moving target goes away, because when checking in new code,
|
|
165 |
developers are strongly urged to test it against Isabelle's code base. If
|
|
166 |
your project is part of that code base, then maintenance is done by
|
|
167 |
others. Unfortunately, this might not be a helpful advice for all types of
|
|
168 |
projects. A lower threshold for inclusion has the Archive of Formalised
|
|
169 |
Proofs, short AFP.\footnote{\url{http://afp.sourceforge.net/}} This archive
|
|
170 |
has been created mainly for formalisations that are interesting but not
|
|
171 |
necessarily of general interest. If you have ML-code as part of a
|
|
172 |
formalisation, then this might be the right place for you. There is no
|
|
173 |
problem with updating your code after submission. At the moment developers
|
|
174 |
are not as diligent with checking their code against the AFP than with
|
|
175 |
checking agains the distribution, but generally problems will be caught and
|
|
176 |
the developer, who caused them, is expected to fix them. So also in this
|
|
177 |
case code maintenance is done for you.
|
263
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
178 |
*}
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
179 |
|
252
|
180 |
section {* Some Naming Conventions in the Isabelle Sources *}
|
233
|
181 |
|
|
182 |
text {*
|
254
|
183 |
There are a few naming conventions in the Isabelle code that might aid reading
|
|
184 |
and writing code. (Remember that code is written once, but read many
|
233
|
185 |
times.) The most important conventions are:
|
|
186 |
|
|
187 |
\begin{itemize}
|
302
|
188 |
\item @{text t}, @{text u}, @{text trm} for (raw) terms; ML-type: @{ML_type term}
|
234
|
189 |
\item @{text ct}, @{text cu} for certified terms; ML-type: @{ML_type cterm}
|
|
190 |
\item @{text "ty"}, @{text T}, @{text U} for (raw) types; ML-type: @{ML_type typ}
|
|
191 |
\item @{text th}, @{text thm} for theorems; ML-type: @{ML_type thm}
|
|
192 |
\item @{text "foo_tac"} for tactics; ML-type: @{ML_type tactic}
|
|
193 |
\item @{text thy} for theories; ML-type: @{ML_type theory}
|
|
194 |
\item @{text ctxt} for proof contexts; ML-type: @{ML_type Proof.context}
|
|
195 |
\item @{text lthy} for local theories; ML-type: @{ML_type local_theory}
|
|
196 |
\item @{text context} for generic contexts; ML-type @{ML_type Context.generic}
|
235
|
197 |
\item @{text mx} for mixfix syntax annotations; ML-type @{ML_type mixfix}
|
248
11851b20fb78
added more to the pretty section and updated the acknowledgements
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
198 |
\item @{text prt} for pretty printing; ML-type @{ML_type Pretty.T}
|
233
|
199 |
\end{itemize}
|
68
|
200 |
*}
|
|
201 |
|
119
|
202 |
section {* Acknowledgements *}
|
|
203 |
|
|
204 |
text {*
|
|
205 |
Financial support for this tutorial was provided by the German
|
122
|
206 |
Research Council (DFG) under grant number URB 165/5-1. The following
|
156
|
207 |
people contributed to the text:
|
119
|
208 |
|
|
209 |
\begin{itemize}
|
122
|
210 |
\item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the
|
|
211 |
\simpleinductive-package and the code for the @{text
|
264
|
212 |
"chunk"}-antiquotation. He also wrote the first version of this chapter
|
122
|
213 |
describing the package and has been helpful \emph{beyond measure} with
|
|
214 |
answering questions about Isabelle.
|
119
|
215 |
|
248
11851b20fb78
added more to the pretty section and updated the acknowledgements
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
216 |
\item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty}.
|
11851b20fb78
added more to the pretty section and updated the acknowledgements
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
217 |
|
119
|
218 |
\item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout},
|
328
|
219 |
\ref{rec:external} and \ref{rec:oracle}. He also wrote section \ref{sec:conversion}
|
329
|
220 |
and helped with recipe \ref{rec:timing}. Parts of section \ref{sec:storing}
|
328
|
221 |
are by him.
|
119
|
222 |
|
|
223 |
\item {\bf Jeremy Dawson} wrote the first version of the chapter
|
|
224 |
about parsing.
|
|
225 |
|
180
|
226 |
\item {\bf Armin Heller} helped with recipe \ref{rec:sat}.
|
|
227 |
|
119
|
228 |
\item {\bf Alexander Krauss} wrote the first version of the ``first-steps''
|
343
|
229 |
chapter and also contributed the material on @{ML_funct Named_Thms}.
|
194
|
230 |
|
207
|
231 |
\item {\bf Christian Sternagel} proofread the tutorial and made
|
293
|
232 |
many improvemets to the text.
|
119
|
233 |
\end{itemize}
|
|
234 |
|
121
|
235 |
Please let me know of any omissions. Responsibility for any remaining
|
153
|
236 |
errors lies with me.\bigskip
|
|
237 |
|
233
|
238 |
\vspace{5cm}
|
153
|
239 |
{\Large\bf
|
335
|
240 |
This tutorial is still in the process of being written! All of the
|
192
|
241 |
text is still under construction. Sections and
|
153
|
242 |
chapters that are under \underline{heavy} construction are marked
|
|
243 |
with TBD.}
|
|
244 |
|
|
245 |
\vfill
|
306
|
246 |
|
|
247 |
This document (version \input{tip}\hspace{-0.5ex}) was compiled with:\\
|
228
|
248 |
\input{version}\\
|
|
249 |
\input{pversion}
|
119
|
250 |
*}
|
2
|
251 |
|
153
|
252 |
|
|
253 |
|
195
|
254 |
end
|