equal
deleted
inserted
replaced
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 letexpressions} 
511 \input{Misc/document/let_rewr.tex} 
512 \index{simplification!of letexpressions} 

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 righthand side of an equation should (in some sense) be simpler 
588 \emph{The righthand side of an equation should (in some sense) be simpler 
598 than the lefthand side.} 
589 than the lefthand 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 cardinalityan impossibility. For the same reason it is not possible 
634 same cardinalityan 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} 