--- a/CookBook/FirstSteps.thy Sat Sep 06 04:32:18 2008 +0200
+++ b/CookBook/FirstSteps.thy Tue Sep 09 14:57:23 2008 +0200
@@ -24,13 +24,23 @@
chapter {* First Steps *}
+
text {*
- Isabelle programming happens in an enhanced dialect of Standard ML,
- which adds antiquotations containing references to the logical
- context.
+ Isabelle programming is done Standard ML, however it often uses an
+ antiquotation mehanism to refer to the logical context of Isabelle.
+ The ML-code that one writes is, just like lemmas and proofs in Isabelle,
+ part of a theory. If you want to follow the code written in this
+ chapter, we assume you are working inside the theory defined as
- Just like all lemmas or proofs, all ML code that you write lives in
- a theory, where it is embedded using the \isacommand{ML} command:
+ \begin{tabular}{@ {}l}
+ \isacommand{theory} CookBook\\
+ \isacommand{imports} Main\\
+ \isacommand{begin}\\
+ \end{tabular}
+
+
+ The easiest and quickest way to include code in a theory is
+ by using the \isacommand{ML} command. For example
*}
ML {*
@@ -38,25 +48,34 @@
*}
text {*
- The \isacommand{ML} command takes an arbitrary ML expression, which
- is evaluated. It can also contain value or function bindings.
+ The expression inside \isacommand{ML} commands is emmediately evaluated
+ like ``normal'' proof scripts by using the advance and retreat buttons of
+ your Isabelle environment. The code inside the \isacommand{ML} command
+ can also contain value- and function bindings. \marginpar{\tiny FIXME can one undo them like
+ Isabelle lemmas/proofs - probably not}
*}
section {* Antiquotations *}
text {*
The main advantage of embedding all code in a theory is that the
- code can contain references to entities that are defined in the
- theory. Let us for example, print out the name of the current
- theory:
+ code can contain references to entities that are defined on the
+ logical level of Isabelle. This is done using antiquotations.
+ For example, one can print out the name of
+ the current theory by typing
*}
ML {* Context.theory_name @{theory} *}
-text {* The @{text "@{theory}"} antiquotation is substituted with the
- current theory, whose name can then be extracted using a the
- function @{ML "Context.theory_name"}. Note that antiquotations are
- statically scoped. The function
+text {*
+ where @{text "@{theory}"} is an antiquotation that is substituted with the
+ current theory (remember that we assumed we are inside the theory CookBook).
+ The name of this theory can be extrated using a the function @{ML "Context.theory_name"}.
+ So the code above returns the string @{ML "\"CookBook\""}.
+
+ Note that antiquotations are statically scoped, that is the value is
+ determined at ``compile-time'' not ``run-time''. For example the function
+
*}
ML {*
@@ -64,16 +83,16 @@
*}
text {*
- does \emph{not} return the name of the current theory. Instead, we have
- defined the constant function that always returns the string @{ML "\"CookBook\""}, which is
- the name of @{text "@{theory}"} at the point where the code
- is embedded. Operationally speaking, @{text "@{theory}"} is \emph{not}
- replaced with code that will look up the current theory in some
- (destructive) data structure and return it. Instead, it is really
- replaced with the theory value.
+ does \emph{not} return the name of the current theory, if it is run in a
+ different theory. Instead, the code above defines the constant function
+ that always returns the string @{ML "\"CookBook\""}, no matter where the
+ function is called. Operationally speaking, @{text "@{theory}"} is
+ \emph{not} replaced with code that will look up the current theory in
+ some data structure and return it. Instead, it is literally
+ replaced with the value representing the theory name.
- In the course of this introduction, we will learn about more of
- these antoquotations, which greatly simplify programming, since you
+ In the course of this introduction, we will learn more about
+ these antoquotations: they greatly simplify Isabelle programming since one
can directly access all kinds of logical elements from ML.
*}
@@ -88,14 +107,14 @@
text {*
This shows the term @{term "(a::nat) + b = c"} in the internal
- representation, with all gory details. Terms are just an ML
+ representation with all gory details. Terms are just an ML
datatype, and they are defined in @{ML_file "Pure/term.ML"}.
- The representation of terms uses deBruin indices: Bound variables
+ The representation of terms uses deBruin indices: bound variables
are represented by the constructor @{ML Bound}, and the index refers to
the number of lambdas we have to skip until we hit the lambda that
binds the variable. The names of bound variables are kept at the
- abstractions, but they are just comments.
+ abstractions, but they should be treated just as comments.
See \ichcite{ch:logic} for more details.
\begin{readmore}
--- a/CookBook/Intro.thy Sat Sep 06 04:32:18 2008 +0200
+++ b/CookBook/Intro.thy Tue Sep 09 14:57:23 2008 +0200
@@ -6,7 +6,7 @@
chapter {* Introduction *}
text {*
- The purpose of this document is to guide the reader through the
+ The purpose of this cookbook is to guide the reader through the
first steps in Isabelle programming, and to provide recipes for
solving common problems.
*}
@@ -14,31 +14,37 @@
section {* Intended Audience and Prior Knowledge *}
text {*
- This cookbook targets an audience who already knows how to use the Isabelle
- system to write theories and proofs, but without using ML.
- You should also be familiar with the \emph{Standard ML} programming
- language, which is used for Isabelle programming. If you are unfamiliar with any of
+ This cookbook targets an audience who already knows how to use Isabelle
+ for writing theories and proofs. It is also assumed that the reader is
+ familiar with the \emph{Standard ML} programming language, in which
+ most of Isabelle is implemented. If you are unfamiliar with any of
these two subjects, you should first work through the Isabelle/HOL
tutorial \cite{isa-tutorial} and Paulson's book on Standard ML
\cite{paulson-ml2}.
*}
-section {* Primary Documentation *}
+section {* Existing Documentation *}
text {*
+ The following documents about ML-coding for Isabelle already exist (they are
+ included in the Isabelle distribution):
\begin{description}
- \item[The Implementation Manual \cite{isa-imp}] describes Isabelle
+ \item[The Implementation Manual] describes Isabelle
from a programmer's perspective, documenting both the underlying
concepts and the concrete interfaces.
- \item[The Isabelle Reference Manual \cite{isabelle-ref}] is an older document that used
+ \item[The Isabelle Reference Manual] is an older document that used
to be the main reference, when all reasoning happened on the ML
level. Many parts of it are outdated now, but some parts, mainly the
chapters on tactics, are still useful.
+ \end{description}
+ Then of ourse there is:
+
+ \begin{description}
\item[The code] is of course 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
@@ -48,8 +54,8 @@
Since Isabelle is not a finished product, these manuals, just like
the implementation itself, are always under construction. This can
- be dificult and frustrating at times, when interfaces are changing
- frequently. But it is a reality that progress means changing
+ be difficult and frustrating at times, especially when interfaces changes
+ occur frequently. But it is a reality that progress means changing
things (FIXME: need some short and convincing comment that this
is a strategy, not a problem that should be solved).
*}
--- a/CookBook/document/cookbook.bib Sat Sep 06 04:32:18 2008 +0200
+++ b/CookBook/document/cookbook.bib Tue Sep 09 14:57:23 2008 +0200
@@ -4,3 +4,18 @@
title = {The {Isabelle/Isar} Implementation},
institution = {Technische Universit\"at M\"unchen},
note = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}}
+
+
+@Book{isa-tutorial,
+ author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
+ title = {Isabelle/HOL: A Proof Assistant for Higher-Order Logic},
+ publisher = {Springer},
+ year = 2002,
+ note = {LNCS Tutorial 2283}}
+
+@book{paulson-ml2,
+ author = {Lawrence C. Paulson},
+ title = {{ML} for the Working Programmer},
+ year = 1996,
+ edition = {2nd},
+ publisher = {Cambridge University Press}}
\ No newline at end of file
--- a/CookBook/document/root.tex Sat Sep 06 04:32:18 2008 +0200
+++ b/CookBook/document/root.tex Tue Sep 09 14:57:23 2008 +0200
@@ -6,11 +6,13 @@
\usepackage[pdftex]{graphicx}
% Cross references to other manuals:
-\usepackage{xr}
-\externaldocument[I-]{implementation}
-\newcommand{\impref}[1]{\ref{I-#1}}
-\newcommand{\ichcite}[1]{[Impl.\,Man., ch.~\impref{#1}]}
-\newcommand{\isccite}[1]{[Impl.\,Man., sec.~\impref{#1}]}
+%\usepackage{xr}
+%\externaldocument[I-]{implementation}
+%\newcommand{\impref}[1]{\ref{I-#1}}
+%\newcommand{\ichcite}[1]{[Impl.\,Man., ch.~\impref{#1}]}
+\newcommand{\ichcite}[1]{[FIXME ref]}
+%\newcommand{\isccite}[1]{[Impl.\,Man., sec.~\impref{#1}]}
+\newcommand{\isccite}[1]{[FIXME ref]}
\usepackage{pdfsetup}
@@ -19,8 +21,16 @@
\renewcommand{\isastyle}{\isastyleminor}% use same formatting for txt and text
\isadroptag{theory}
-\newenvironment{readmore}
-{\makebox[0pt][r]{\fbox{\textbf{Read More}}~~}\it}{}
+% sane default for proof documents
+\parindent 0pt\parskip 0.6ex
+
+
+% for comments on the margin
+\newcommand{\readmoremarginpar}[1]%
+{\marginpar[\raggedleft\small{#1}]{\raggedright\small{#1}}}
+
+\newenvironment{readmore}%
+{\hspace{-3pt}\readmoremarginpar{\fbox{\textbf{Read More}}}\it}{}
\newtheorem{exercise}{Exercise}[section]
@@ -40,15 +50,13 @@
\tableofcontents
-% sane default for proof documents
-\parindent 0pt\parskip 0.5ex
% generated text of all theories
\input{session}
\newpage
\bibliographystyle{abbrv}
-\bibliography{manul,cookbook}
+\bibliography{cookbook}
\end{document}
Binary file cookbook.pdf has changed