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

doc-src/TutorialI/fp.tex

changeset 9933 | 9feb1e0c4cb3 |

parent 9844 | 8016321c7de1 |

child 10181 | c07860c826c5 |

--- a/doc-src/TutorialI/fp.tex Tue Sep 12 14:59:44 2000 +0200 +++ b/doc-src/TutorialI/fp.tex Tue Sep 12 15:43:15 2000 +0200 @@ -225,29 +225,7 @@ \end{warn} -\subsection{Case study: boolean expressions} -\label{sec:boolex} - -The aim of this case study is twofold: it shows how to model boolean -expressions and some algorithms for manipulating them, and it demonstrates -the constructs introduced above. - \input{Ifexpr/document/Ifexpr.tex} -\medskip - -How does one come up with the required lemmas? Try to prove the main theorems -without them and study carefully what \isa{auto} leaves unproved. This has -to provide the clue. The necessity of universal quantification -(\isa{\isasymforall{}t e}) in the two lemmas is explained in -\S\ref{sec:InductionHeuristics} - -\begin{exercise} - We strengthen the definition of a \isa{normal} If-expression as follows: - the first argument of all \isa{IF}s must be a variable. Adapt the above - development to this changed requirement. (Hint: you may need to formulate - some of the goals as implications (\isasymimp) rather than equalities - (\isa{=}).) -\end{exercise} \section{Some basic types} @@ -417,9 +395,10 @@ \begin{ttbox}\makeatother (0#1#[]) @ [] \(\leadsto\) 0#((1#[]) @ []) \(\leadsto\) 0#(1#([] @ [])) \(\leadsto\) 0#1#[] \end{ttbox} -This is also known as \bfindex{term rewriting} and the equations are referred -to as \bfindex{rewrite rules}. ``Rewriting'' is more honest than ``simplification'' -because the terms do not necessarily become simpler in the process. +This is also known as \bfindex{term rewriting}\indexbold{rewriting} and the +equations are referred to as \textbf{rewrite rules}\indexbold{rewrite rule}. +``Rewriting'' is more honest than ``simplification'' because the terms do not +necessarily become simpler in the process. \input{Misc/document/simp.tex} @@ -592,12 +571,4 @@ \index{induction!recursion|)} \index{recursion induction|)} - -\subsection{Advanced forms of recursion} -\label{sec:advanced-recdef} - -\input{Recdef/document/Nested0.tex} -\input{Recdef/document/Nested1.tex} -\input{Recdef/document/Nested2.tex} - \index{*recdef|)}