doc-src/TutorialI/fp.tex
changeset 9792 bbefb6ce5cb2
parent 9754 a123a64cadeb
child 9844 8016321c7de1
equal deleted 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}