doc-src/TutorialI/fp.tex
 changeset 9792 bbefb6ce5cb2 parent 9754 a123a64cadeb child 9844 8016321c7de1
equal inserted replaced
9791:a39e5d43de55 9792:bbefb6ce5cb2
   506   If you have defined $f\,x\,y~\isasymequiv~t$ then you can only expand
   506   If you have defined $f\,x\,y~\isasymequiv~t$ then you can only expand
   507   occurrences of $f$ with at least two arguments. Thus it is safer to define
   507   occurrences of $f$ with at least two arguments. Thus it is safer to define
   508   $f$~\isasymequiv~\isasymlambda$x\,y.\;t$.
   508   $f$~\isasymequiv~\isasymlambda$x\,y.\;t$.
   509 \end{warn}
   509 \end{warn}
   510
   510
   511 \subsubsection{Simplifying let-expressions}
   511 \input{Misc/document/let_rewr.tex}
   512 \index{simplification!of let-expressions}

   513

   514 Proving a goal containing \isaindex{let}-expressions almost invariably

   515 requires the \isa{let}-con\-structs to be expanded at some point. Since

   516 \isa{let}-\isa{in} is just syntactic sugar for a predefined constant (called

   517 \isa{Let}), expanding \isa{let}-constructs means rewriting with

   518 \isa{Let_def}:

   519

   520 {\makeatother\input{Misc/document/let_rewr.tex}}

   521
   512
   522 \subsubsection{Conditional equations}
   513 \subsubsection{Conditional equations}
   523
   514
   524 \input{Misc/document/cond_rewr.tex}
   515 \input{Misc/document/cond_rewr.tex}
   525
   516
   595 another, albeit weak heuristic that is not restricted to induction:
   586 another, albeit weak heuristic that is not restricted to induction:
   596 \begin{quote}
   587 \begin{quote}
   597   \emph{The right-hand side of an equation should (in some sense) be simpler
   588   \emph{The right-hand side of an equation should (in some sense) be simpler
   598     than the left-hand side.}
   589     than the left-hand side.}
   599 \end{quote}
   590 \end{quote}
   600 The heuristic is tricky to apply because it is not obvious that
   591 This heuristic is tricky to apply because it is not obvious that
   601 \isa{rev xs \at\ ys} is simpler than \isa{itrev xs ys}. But see what
   592 \isa{rev xs \at\ ys} is simpler than \isa{itrev xs ys}. But see what
   602 happens if you try to prove \isa{rev xs \at\ ys = itrev xs ys}!
   593 happens if you try to prove \isa{rev xs \at\ ys = itrev xs ys}!
   603
   594
   604 \begin{exercise}
   595 \begin{exercise}
   605 \input{Misc/document/Tree2.tex}%
   596 \input{Misc/document/Tree2.tex}%
   633 \subsection{The limits of nested recursion}
   624 \subsection{The limits of nested recursion}
   634
   625
   635 How far can we push nested recursion? By the unfolding argument above, we can
   626 How far can we push nested recursion? By the unfolding argument above, we can
   636 reduce nested to mutual recursion provided the nested recursion only involves
   627 reduce nested to mutual recursion provided the nested recursion only involves
   637 previously defined datatypes. This does not include functions:
   628 previously defined datatypes. This does not include functions:
   638 \begin{ttbox}
   629 \begin{isabelle}
   639 datatype t = C (t => bool)
   630 \isacommand{datatype} t = C "t \isasymRightarrow\ bool"
   640 \end{ttbox}
   631 \end{isabelle}
   641 is a real can of worms: in HOL it must be ruled out because it requires a type
   632 is a real can of worms: in HOL it must be ruled out because it requires a type
   642 \isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the
   633 \isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the
   643 same cardinality---an impossibility. For the same reason it is not possible
   634 same cardinality---an impossibility. For the same reason it is not possible
   644 to allow recursion involving the type \isa{set}, which is isomorphic to
   635 to allow recursion involving the type \isa{set}, which is isomorphic to
   645 \isa{t \isasymFun\ bool}.
   636 \isa{t \isasymFun\ bool}.
   652 \smallskip
   643 \smallskip
   653
   644
   654 \input{Datatype/document/Fundata.tex}
   645 \input{Datatype/document/Fundata.tex}
   655 \bigskip
   646 \bigskip
   656
   647
   657 If you need nested recursion on the left of a function arrow,
   648 If you need nested recursion on the left of a function arrow, there are
   658 there are alternatives to pure HOL: LCF~\cite{paulson87} is a logic where types like
   649 alternatives to pure HOL: LCF~\cite{paulson87} is a logic where types like
   659 \begin{ttbox}
   650 \begin{isabelle}
   660 datatype lam = C (lam -> lam)
   651 \isacommand{datatype} lam = C "lam \isasymrightarrow\ lam"
   661 \end{ttbox}
   652 \end{isabelle}
   662 do indeed make sense (note the intentionally different arrow \isa{->}).
   653 do indeed make sense (but note the intentionally different arrow
   663 There is even a version of LCF on top of HOL, called
   654 \isa{\isasymrightarrow}). There is even a version of LCF on top of HOL,
   664 HOLCF~\cite{MuellerNvOS99}.
   655 called HOLCF~\cite{MuellerNvOS99}.
   665
   656
   666 \index{*primrec|)}
   657 \index{*primrec|)}
   667 \index{*datatype|)}
   658 \index{*datatype|)}
   668
   659
   669 \subsection{Case study: Tries}
   660 \subsection{Case study: Tries}