1.1 --- a/doc-src/TutorialI/fp.tex Thu Jul 26 18:23:38 2001 +0200
1.2 +++ b/doc-src/TutorialI/fp.tex Fri Aug 03 18:04:55 2001 +0200
1.3 @@ -155,7 +155,7 @@
1.4
1.5 \index{datatypes|(}%
1.6 Inductive datatypes are part of almost every non-trivial application of HOL.
1.7 -First we take another look at a very important example, the datatype of
1.8 +First we take another look at an important example, the datatype of
1.9 lists, before we turn to datatypes in general. The section closes with a
1.10 case study.
1.11
1.12 @@ -307,18 +307,19 @@
1.13
1.14 \chapter{More Functional Programming}
1.15
1.16 -The purpose of this chapter is to deepen the reader's understanding of the
1.17 +The purpose of this chapter is to deepen your understanding of the
1.18 concepts encountered so far and to introduce advanced forms of datatypes and
1.19 recursive functions. The first two sections give a structured presentation of
1.20 theorem proving by simplification ({\S}\ref{sec:Simplification}) and discuss
1.21 -important heuristics for induction ({\S}\ref{sec:InductionHeuristics}). They can
1.22 -be skipped by readers less interested in proofs. They are followed by a case
1.23 -study, a compiler for expressions ({\S}\ref{sec:ExprCompiler}). Advanced
1.24 +important heuristics for induction ({\S}\ref{sec:InductionHeuristics}). You can
1.25 +skip them if you are not planning to perform proofs yourself.
1.26 +We then present a case
1.27 +study: a compiler for expressions ({\S}\ref{sec:ExprCompiler}). Advanced
1.28 datatypes, including those involving function spaces, are covered in
1.29 -{\S}\ref{sec:advanced-datatypes}, which closes with another case study, search
1.30 -trees (``tries''). Finally we introduce \isacommand{recdef}, a very general
1.31 -form of recursive function definition which goes well beyond what
1.32 -\isacommand{primrec} allows ({\S}\ref{sec:recdef}).
1.33 +{\S}\ref{sec:advanced-datatypes}; it closes with another case study, search
1.34 +trees (``tries''). Finally we introduce \isacommand{recdef}, a general
1.35 +form of recursive function definition that goes well beyond
1.36 +\isacommand{primrec} ({\S}\ref{sec:recdef}).
1.37
1.38
1.39 \section{Simplification}
1.40 @@ -326,21 +327,21 @@
1.41 \index{simplification|(}
1.42
1.43 So far we have proved our theorems by \isa{auto}, which simplifies
1.44 -\emph{all} subgoals. In fact, \isa{auto} can do much more than that, except
1.45 -that it did not need to so far. However, when you go beyond toy examples, you
1.46 +all subgoals. In fact, \isa{auto} can do much more than that.
1.47 +To go beyond toy examples, you
1.48 need to understand the ingredients of \isa{auto}. This section covers the
1.49 method that \isa{auto} always applies first, simplification.
1.50
1.51 Simplification is one of the central theorem proving tools in Isabelle and
1.52 -many other systems. The tool itself is called the \bfindex{simplifier}. The
1.53 -purpose of this section is to introduce the many features of the simplifier.
1.54 -Anybody intending to perform proofs in HOL should read this section. Later on
1.55 -({\S}\ref{sec:simplification-II}) we explain some more advanced features and a
1.56 +many other systems. The tool itself is called the \textbf{simplifier}.
1.57 +This section introduces the many features of the simplifier
1.58 +and is required reading if you intend to perform proofs. Later on,
1.59 +{\S}\ref{sec:simplification-II} explains some more advanced features and a
1.60 little bit of how the simplifier works. The serious student should read that
1.61 -section as well, in particular in order to understand what happened if things
1.62 -do not simplify as expected.
1.63 +section as well, in particular to understand why the simplifier did
1.64 +something unexpected.
1.65
1.66 -\subsection{What is Simplification}
1.67 +\subsection{What is Simplification?}
1.68
1.69 In its most basic form, simplification means repeated application of
1.70 equations from left to right. For example, taking the rules for \isa{\at}
1.71 @@ -350,10 +351,16 @@
1.72 (0#1#[]) @ [] \(\leadsto\) 0#((1#[]) @ []) \(\leadsto\) 0#(1#([] @ [])) \(\leadsto\) 0#1#[]
1.73 \end{ttbox}
1.74 This is also known as \bfindex{term rewriting}\indexbold{rewriting} and the
1.75 -equations are referred to as \textbf{rewrite rules}\indexbold{rewrite rule}.
1.76 +equations are referred to as \bfindex{rewrite rules}.
1.77 ``Rewriting'' is more honest than ``simplification'' because the terms do not
1.78 necessarily become simpler in the process.
1.79
1.80 +The simplifier proves arithmetic goals as described in
1.81 +{\S}\ref{sec:nat} above. Arithmetic expressions are simplified using built-in
1.82 +procedures that go beyond mere rewrite rules. New simplification procedures
1.83 +can be coded and installed, but they are definitely not a matter for this
1.84 +tutorial.
1.85 +
1.86 \input{Misc/document/simp.tex}
1.87
1.88 \index{simplification|)}
1.89 @@ -407,16 +414,16 @@
1.90 Fortunately, a limited form of recursion
1.91 involving function spaces is permitted: the recursive type may occur on the
1.92 right of a function arrow, but never on the left. Hence the above can of worms
1.93 -is ruled out but the following example of a potentially infinitely branching tree is
1.94 -accepted:
1.95 +is ruled out but the following example of a potentially
1.96 +\index{infinitely branching trees}%
1.97 +infinitely branching tree is accepted:
1.98 \smallskip
1.99
1.100 \input{Datatype/document/Fundata.tex}
1.101 -\bigskip
1.102
1.103 If you need nested recursion on the left of a function arrow, there are
1.104 alternatives to pure HOL\@. In the Logic for Computable Functions
1.105 -(LCF), types like
1.106 +(\rmindex{LCF}), types like
1.107 \begin{isabelle}
1.108 \isacommand{datatype} lam = C "lam \isasymrightarrow\ lam"
1.109 \end{isabelle}
1.110 @@ -424,7 +431,7 @@
1.111 \isa{\isasymrightarrow} instead of \isa{\isasymRightarrow},
1.112 expressing the type of \emph{continuous} functions.
1.113 There is even a version of LCF on top of HOL,
1.114 -called HOLCF~\cite{MuellerNvOS99}.
1.115 +called \rmindex{HOLCF}~\cite{MuellerNvOS99}.
1.116 \index{datatype@\isacommand {datatype} (command)|)}
1.117 \index{primrec@\isacommand {primrec} (command)|)}
1.118
1.119 @@ -432,6 +439,7 @@
1.120 \subsection{Case Study: Tries}
1.121 \label{sec:Trie}
1.122
1.123 +\index{tries|(}%
1.124 Tries are a classic search tree data structure~\cite{Knuth3-75} for fast
1.125 indexing with strings. Figure~\ref{fig:trie} gives a graphical example of a
1.126 trie containing the words ``all'', ``an'', ``ape'', ``can'', ``car'' and
1.127 @@ -482,6 +490,7 @@
1.128 nodes do not carry any value. This distinction is modeled with the help
1.129 of the predefined datatype \isa{option} (see {\S}\ref{sec:option}).
1.130 \input{Trie/document/Trie.tex}
1.131 +\index{tries|)}
1.132
1.133 \section{Total Recursive Functions}
1.134 \label{sec:recdef}
1.135 @@ -503,12 +512,12 @@
1.136
1.137 \input{Recdef/document/termination.tex}
1.138
1.139 -\subsection{Simplification with Recdef}
1.140 +\subsection{Simplification and Recursive Functions}
1.141 \label{sec:recdef-simplification}
1.142
1.143 \input{Recdef/document/simplification.tex}
1.144
1.145 -\subsection{Induction}
1.146 +\subsection{Induction and Recursive Functions}
1.147 \index{induction!recursion|(}
1.148 \index{recursion induction|(}
1.149