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

doc-src/TutorialI/fp.tex

changeset 9792 | bbefb6ce5cb2 |

parent 9754 | a123a64cadeb |

child 9844 | 8016321c7de1 |

--- a/doc-src/TutorialI/fp.tex Fri Sep 01 18:29:52 2000 +0200 +++ b/doc-src/TutorialI/fp.tex Fri Sep 01 19:09:44 2000 +0200 @@ -508,16 +508,7 @@ $f$~\isasymequiv~\isasymlambda$x\,y.\;t$. \end{warn} -\subsubsection{Simplifying let-expressions} -\index{simplification!of let-expressions} - -Proving a goal containing \isaindex{let}-expressions almost invariably -requires the \isa{let}-con\-structs to be expanded at some point. Since -\isa{let}-\isa{in} is just syntactic sugar for a predefined constant (called -\isa{Let}), expanding \isa{let}-constructs means rewriting with -\isa{Let_def}: - -{\makeatother\input{Misc/document/let_rewr.tex}} +\input{Misc/document/let_rewr.tex} \subsubsection{Conditional equations} @@ -597,7 +588,7 @@ \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 +This 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 happens if you try to prove \isa{rev xs \at\ ys = itrev xs ys}! @@ -635,9 +626,9 @@ How far can we push nested recursion? By the unfolding argument above, we can reduce nested to mutual recursion provided the nested recursion only involves previously defined datatypes. This does not include functions: -\begin{ttbox} -datatype t = C (t => bool) -\end{ttbox} +\begin{isabelle} +\isacommand{datatype} t = C "t \isasymRightarrow\ bool" +\end{isabelle} is a real can of worms: in HOL it must be ruled out because it requires a type \isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the same cardinality---an impossibility. For the same reason it is not possible @@ -654,14 +645,14 @@ \input{Datatype/document/Fundata.tex} \bigskip -If you need nested recursion on the left of a function arrow, -there are alternatives to pure HOL: LCF~\cite{paulson87} is a logic where types like -\begin{ttbox} -datatype lam = C (lam -> lam) -\end{ttbox} -do indeed make sense (note the intentionally different arrow \isa{->}). -There is even a version of LCF on top of HOL, called -HOLCF~\cite{MuellerNvOS99}. +If you need nested recursion on the left of a function arrow, there are +alternatives to pure HOL: LCF~\cite{paulson87} is a logic where types like +\begin{isabelle} +\isacommand{datatype} lam = C "lam \isasymrightarrow\ lam" +\end{isabelle} +do indeed make sense (but note the intentionally different arrow +\isa{\isasymrightarrow}). There is even a version of LCF on top of HOL, +called HOLCF~\cite{MuellerNvOS99}. \index{*primrec|)} \index{*datatype|)}