author nipkow Mon, 29 Jul 2013 22:17:19 +0200 changeset 52782 b11d73dbfb76 parent 52758 7ffcd6f2890d child 52783 084ac81e9871
tuned intro
 src/Doc/ProgProve/Bool_nat_list.thy file | annotate | diff | comparison | revisions src/Doc/ProgProve/Logic.thy file | annotate | diff | comparison | revisions src/Doc/ProgProve/document/intro-isabelle.tex file | annotate | diff | comparison | revisions src/Doc/ProgProve/document/root.bib file | annotate | diff | comparison | revisions src/Doc/ProgProve/document/root.tex file | annotate | diff | comparison | revisions
--- a/src/Doc/ProgProve/Bool_nat_list.thy	Mon Jul 29 18:06:39 2013 +0200
+++ b/src/Doc/ProgProve/Bool_nat_list.thy	Mon Jul 29 22:17:19 2013 +0200
@@ -397,7 +397,8 @@
@{text"\""}@{thm map.simps(1)}@{text"\" |"}\\
@{text"\""}@{thm map.simps(2)}@{text"\""}
\end{isabelle}
-\sem
+
+\ifsem
Also useful are the \concept{head} of a list, its first element,
and the \concept{tail}, the rest of the list:
\begin{isabelle}
@@ -412,7 +413,7 @@
Note that since HOL is a logic of total functions, @{term"hd []"} is defined,
but we do now know what the result is. That is, @{term"hd []"} is not undefined
but underdefined.
-\endsem
+\fi
%

\subsection{Exercises}
--- a/src/Doc/ProgProve/Logic.thy	Mon Jul 29 18:06:39 2013 +0200
+++ b/src/Doc/ProgProve/Logic.thy	Mon Jul 29 22:17:19 2013 +0200
@@ -477,10 +477,10 @@

Inductive definitions are the third important definition facility, after
datatypes and recursive function.
-\sem
+\ifsem
In fact, they are the key construct in the
definition of operational semantics in the second part of the book.
-\endsem
+\fi

\subsection{An Example: Even Numbers}
\label{sec:Logic:even}
@@ -670,10 +670,10 @@
Evenness is really more conveniently expressed recursively than inductively.
As a second and very typical example of an inductive definition we define the
reflexive transitive closure.
-\sem
+\ifsem
It will also be an important building block for
some of the semantics considered in the second part of the book.
-\endsem
+\fi

The reflexive transitive closure, called @{text star} below, is a function
that maps a binary predicate to another binary predicate: if @{text r} is of
--- a/src/Doc/ProgProve/document/intro-isabelle.tex	Mon Jul 29 18:06:39 2013 +0200
+++ b/src/Doc/ProgProve/document/intro-isabelle.tex	Mon Jul 29 22:17:19 2013 +0200
@@ -3,17 +3,22 @@
of Isabelle for HOL, which abbreviates Higher-Order Logic. We introduce
HOL step by step following the equation
$\mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}.$
-We assume that the reader is familiar with the basic concepts of functional
-programming and is used to logical and set theoretic notation.
+We assume that the reader is used to logical and set theoretic notation
+and is familiar with the basic concepts of functional programming.
+\ifsem
+Open-minded readers have been known to pick up functional
+programming through the wealth of examples in \autoref{sec:FP}
+and \autoref{sec:CaseStudyExp}.
+\fi

\autoref{sec:FP} introduces HOL as a functional programming language and
explains how to write simple inductive proofs of mostly equational properties
of recursive functions.
-\sem
+\ifsem
\autoref{sec:CaseStudyExp} contains a
little case study: arithmetic and boolean expressions, their evaluation,
optimization and compilation.
-\endsem
+\fi
\autoref{ch:Logic} introduces the rest of HOL: the
language of formulas beyond equality, automatic proof tools, single
step proofs, and inductive definitions, an essential specification construct.
@@ -32,16 +37,33 @@
This introduction to the core of Isabelle is intentionally concrete and
example-based: we concentrate on examples that illustrate the typical cases;
we do not explain the general case if it can be inferred from the examples.
+We cover the essentials (from a functional programming point of view) as
+quickly and compactly as possible.
+\ifsem
+After all, this book is primarily about semantics.
+\fi
+
For a comprehensive treatment of all things Isabelle we recommend the
\emph{Isabelle/Isar Reference Manual}~\cite{IsarRef}, which comes with the
Isabelle distribution.
The tutorial by Nipkow, Paulson and Wenzel~\cite{LNCS2283} (in its updated version that comes with the Isabelle distribution) is still recommended for the wealth of examples and material, but its proof style is outdated. In particular it fails to cover the structured proof language Isar.

-This introduction has grown out of many years of teaching Isabelle courses.
-It tries to cover the essentials (from a functional programming point of
-view) as quickly and compactly as possible. There is also an accompanying
-set of \LaTeX-based slides available from the author on request.
+%This introduction to Isabelle has grown out of many years of teaching
+%Isabelle courses.
+
+\ifsem\else
+If you want to apply what you have learned about Isabelle we recommend you
+\href{http://www.in.tum.de/~nipkow/Concrete/}{Concrete
+Semantics}~\cite{ConcreteSemantics}, a guided tour of the wonderful world of
+programming langage semantics formalised in Isabelle.  In fact,
+\emph{Programming and Proving in Isabelle/HOL} constitutes part~I of
+\href{http://www.in.tum.de/~nipkow/Concrete/}{Concrete Semantics}.  The web
+pages for \href{http://www.in.tum.de/~nipkow/Concrete/}{Concrete Semantics}
+also provide a set of \LaTeX-based slides for teaching \emph{Programming and
+Proving in Isabelle/HOL}.
+\fi

\paragraph{Acknowledgements}
-I wish to thank the following people for their comments on this text:
+\ifsem We \else I \fi wish to thank the following people for their comments:
Florian Haftmann, Ren\'{e} Thiemann and Christian Sternagel.
\ No newline at end of file
--- a/src/Doc/ProgProve/document/root.bib	Mon Jul 29 18:06:39 2013 +0200
+++ b/src/Doc/ProgProve/document/root.bib	Mon Jul 29 22:17:19 2013 +0200
@@ -16,6 +16,10 @@
title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
publisher=Springer,series=LNCS,volume=2283,year=2002}

+@book{ConcreteSemantics,author={Tobias Nipkow and Gerwin Klein},
+title="Concrete Semantics. A Proof Assistant Approach",
+publisher={\url{http://www.in.tum.de/~nipkow/Concrete}},year=2013}
+
@manual{IsarRef,author={Makarius Wenzel},
title={The Isabelle/Isar Reference Manual},
note={\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}}
--- a/src/Doc/ProgProve/document/root.tex	Mon Jul 29 18:06:39 2013 +0200
+++ b/src/Doc/ProgProve/document/root.tex	Mon Jul 29 22:17:19 2013 +0200
@@ -2,7 +2,7 @@

\input{prelude}

-\excludecomment{sem}
+\newif\ifsem

\begin{document}