# HG changeset patch # User Christian Urban # Date 1220965043 -7200 # Node ID e91f54791e14eb630d269e1d73b5bc8183cf4806 # Parent 2a69b119cdeee74e8c82493310a1d3da8d6a7b6b minor modifiations to the Intro and FirstSteps chapters diff -r 2a69b119cdee -r e91f54791e14 CookBook/FirstSteps.thy --- 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} diff -r 2a69b119cdee -r e91f54791e14 CookBook/Intro.thy --- 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). *} diff -r 2a69b119cdee -r e91f54791e14 CookBook/document/cookbook.bib --- 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 diff -r 2a69b119cdee -r e91f54791e14 CookBook/document/root.tex --- 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} diff -r 2a69b119cdee -r e91f54791e14 cookbook.pdf Binary file cookbook.pdf has changed