summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/TutorialI/fp.tex

changeset 9754 | a123a64cadeb |

parent 9742 | 98d3ca2c18f7 |

child 9792 | bbefb6ce5cb2 |

--- a/doc-src/TutorialI/fp.tex Wed Aug 30 18:05:20 2000 +0200 +++ b/doc-src/TutorialI/fp.tex Wed Aug 30 18:09:20 2000 +0200 @@ -405,16 +405,12 @@ Simplification is one of the central theorem proving tools in Isabelle and many other systems. The tool itself is called the \bfindex{simplifier}. The -purpose of this section is twofold: to introduce the many features of the -simplifier (\S\ref{sec:SimpFeatures}) and to explain a little bit how the -simplifier works (\S\ref{sec:SimpHow}). Anybody intending to use HOL should -read \S\ref{sec:SimpFeatures}, and the serious student should read -\S\ref{sec:SimpHow} as well in order to understand what happened in case -things do not simplify as expected. - - -\subsection{Using the simplifier} -\label{sec:SimpFeatures} +purpose of this section is introduce the many features of the simplifier. +Anybody intending to use HOL should read this section. Later on +(\S\ref{sec:simplification-II}) we explain some more advanced features and a +little bit of how the simplifier works. The serious student should read that +section as well, in particular in order to understand what happened if things +do not simplify as expected. \subsubsection{What is simplification} @@ -572,11 +568,11 @@ inductive proofs. The first one we have already mentioned in our initial example: \begin{quote} -{\em 1. Theorems about recursive functions are proved by induction.} +\emph{Theorems about recursive functions are proved by induction.} \end{quote} In case the function has more than one argument \begin{quote} -{\em 2. Do induction on argument number $i$ if the function is defined by +\emph{Do induction on argument number $i$ if the function is defined by recursion in argument number $i$.} \end{quote} When we look at the proof of {\makeatother\isa{(xs @ ys) @ zs = xs @ (ys @ @@ -598,8 +594,8 @@ side, the simpler \isa{rev} on the right-hand side. This constitutes another, albeit weak heuristic that is not restricted to induction: \begin{quote} - {\em 5. The right-hand side of an equation should (in some sense) be - simpler than the left-hand side.} + \emph{The right-hand side of an equation should (in some sense) be simpler + than the left-hand side.} \end{quote} The heuristic is tricky to apply because it is not obvious that \isa{rev xs \at\ ys} is simpler than \isa{itrev xs ys}. But see what