theory Intro+ −
imports Base+ −
begin+ −
+ −
chapter {* Introduction *}+ −
+ −
text {*+ −
If your next project requires you to program on the ML-level of Isabelle,+ −
then this tutorial is for you. It will guide you through the first steps of+ −
Isabelle programming, and also explain tricks of the trade. The best way to+ −
get to know the ML-level of Isabelle is by experimenting with the many code+ −
examples included in the tutorial. The code is as far as possible checked+ −
against \input{version}. If something does not work, + −
then please let us know. It is impossible for us to know every environment, + −
operating system or editor in which Isabelle is used. If you have comments, + −
criticism or like to add to the tutorial, please feel free---you are most + −
welcome! The tutorial is meant to be gentle and comprehensive. To achieve + −
this we need your feedback.+ −
*}+ −
+ −
section {* Intended Audience and Prior Knowledge *}+ −
+ −
text {* + −
This tutorial targets readers who already know how to use Isabelle for+ −
writing theories and proofs. We also assume that readers are familiar with+ −
the functional programming language ML, the language in which most of+ −
Isabelle is implemented. If you are unfamiliar with either of these two+ −
subjects, you should first work through the Isabelle/HOL tutorial+ −
\cite{isa-tutorial} or Paulson's book on ML \cite{paulson-ml2}.+ −
+ −
*}+ −
+ −
section {* Existing Documentation *}+ −
+ −
text {*+ −
+ −
The following documentation about Isabelle programming already exists (and is+ −
part of the distribution of Isabelle):+ −
+ −
\begin{description}+ −
\item[The Isabelle/Isar Implementation Manual] describes Isabelle+ −
from a high-level perspective, documenting both the underlying+ −
concepts and some of the interfaces. + −
+ −
\item[The Isabelle Reference Manual] is an older document that used+ −
to be the main reference of Isabelle at a time when all proof scripts + −
were written on the ML-level. Many parts of this manual are outdated + −
now, but some parts, particularly the chapters on tactics, are still + −
useful.+ −
+ −
\item[The Isar Reference Manual] provides specification material (like grammars,+ −
examples and so on) about Isar and its implementation. It is currently in+ −
the process of being updated.+ −
\end{description}+ −
+ −
Then of course there are:+ −
+ −
\begin{description}+ −
\item[The Isabelle sources.] They are the ultimate reference for how+ −
things really work. Therefore you should not hesitate to look at the+ −
way things are actually implemented. More importantly, it is often+ −
good to look at code that does similar things as you want to do and+ −
learn from it. The GNU/UNIX command \mbox{@{text "grep -R"}} is+ −
often your best friend while programming with Isabelle, or+ −
hypersearch if you program using jEdit under MacOSX.+ −
\end{description}+ −
+ −
*}+ −
+ −
section {* Typographic Conventions in the Tutorial *}+ −
+ −
text {*+ −
+ −
All ML-code in this tutorial is typeset in shaded boxes, like the following + −
ML-expression:+ −
+ −
\begin{isabelle}+ −
\begin{graybox}+ −
\isacommand{ML}~@{text "\<verbopen>"}\isanewline+ −
\hspace{5mm}@{ML "3 + 4"}\isanewline+ −
@{text "\<verbclose>"}+ −
\end{graybox}+ −
\end{isabelle}+ −
+ −
These boxes correspond to how code can be processed inside the interactive+ −
environment of Isabelle. It is therefore easy to experiment with what is + −
displayed. However, for better readability we will drop the enclosing + −
\isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} and just write:+ −
+ −
+ −
@{ML [display,gray] "3 + 4"}+ −
+ −
Whenever appropriate we also show the response the code + −
generates when evaluated. This response is prefixed with a + −
@{text [quotes] ">"}, like:+ −
+ −
@{ML_response [display,gray] "3 + 4" "7"}+ −
+ −
The user-level commands of Isabelle (i.e., the non-ML code) are written+ −
in \isacommand{bold face} (e.g., \isacommand{lemma}, \isacommand{apply},+ −
\isacommand{foobar} and so on). We use @{text "$ \<dots>"} to indicate that a+ −
command needs to be run in a UNIX-shell, for example:+ −
+ −
@{text [display] "$ grep -R ThyOutput *"}+ −
+ −
Pointers to further information and Isabelle files are typeset in + −
\textit{italic} and highlighted as follows:+ −
+ −
\begin{readmore}+ −
Further information or pointers to files.+ −
\end{readmore}+ −
+ −
The pointers to Isabelle files are hyperlinked to the tip of the Mercurial+ −
repository of Isabelle at \href{http://isabelle.in.tum.de/repos/isabelle/}+ −
{http://isabelle.in.tum.de/repos/isabelle/}.+ −
+ −
A few exercises are scattered around the text. Their solutions are given + −
in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try+ −
to solve the exercises on your own, and then look at the solutions.+ −
*}+ −
+ −
section {* Naming Conventions in the Isabelle Sources *}+ −
+ −
text {*+ −
There are a few naming conventions in Isabelle that might aid reading + −
and writing code. (Remember that code is written once, but read numerous + −
times.) The most important conventions are:+ −
+ −
\begin{itemize}+ −
\item @{text t}, @{text u} for (raw) terms; ML-type: @{ML_type term}+ −
\item @{text ct}, @{text cu} for certified terms; ML-type: @{ML_type cterm}+ −
\item @{text "ty"}, @{text T}, @{text U} for (raw) types; ML-type: @{ML_type typ}+ −
\item @{text th}, @{text thm} for theorems; ML-type: @{ML_type thm}+ −
\item @{text "foo_tac"} for tactics; ML-type: @{ML_type tactic}+ −
\item @{text thy} for theories; ML-type: @{ML_type theory}+ −
\item @{text ctxt} for proof contexts; ML-type: @{ML_type Proof.context}+ −
\item @{text lthy} for local theories; ML-type: @{ML_type local_theory}+ −
\item @{text context} for generic contexts; ML-type @{ML_type Context.generic}+ −
\item @{text mx} for mixfix syntax annotations; ML-type @{ML_type mixfix}+ −
\end{itemize}+ −
*}+ −
+ −
section {* Acknowledgements *}+ −
+ −
text {*+ −
Financial support for this tutorial was provided by the German + −
Research Council (DFG) under grant number URB 165/5-1. The following+ −
people contributed to the text:+ −
+ −
\begin{itemize}+ −
\item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the+ −
\simpleinductive-package and the code for the @{text+ −
"chunk"}-antiquotation. He also wrote the first version of the chapter+ −
describing the package and has been helpful \emph{beyond measure} with+ −
answering questions about Isabelle.+ −
+ −
\item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, + −
\ref{rec:config}, \ref{rec:storingdata}, \ref{rec:external} and \ref{rec:oracle}.+ −
He also wrote section \ref{sec:conversion} and helped with recipe \ref{rec:timing}.+ −
+ −
\item {\bf Jeremy Dawson} wrote the first version of the chapter+ −
about parsing.+ −
+ −
\item {\bf Armin Heller} helped with recipe \ref{rec:sat}.+ −
+ −
\item {\bf Alexander Krauss} wrote the first version of the ``first-steps'' + −
chapter and also contributed the material on @{text NamedThmsFun}.+ −
+ −
\item {\bf Christian Sternagel} proofread the tutorial and made + −
comments on the text. + −
\end{itemize}+ −
+ −
Please let me know of any omissions. Responsibility for any remaining+ −
errors lies with me.\bigskip+ −
+ −
\vspace{5cm}+ −
{\Large\bf+ −
This document is still in the process of being written! All of the+ −
text is still under construction. Sections and + −
chapters that are under \underline{heavy} construction are marked + −
with TBD.}+ −
+ −
+ −
\vfill+ −
This document was compiled with:\\+ −
\input{version}\\+ −
\input{pversion}+ −
*}+ −
+ −
+ −
+ −
end+ −