doc-src/TutorialI/Advanced/advanced.tex
author paulson
Fri Jan 12 16:32:01 2001 +0100 (2001-01-12)
changeset 10885 90695f46440b
parent 10654 458068404143
child 11196 bb4ede27fcb7
permissions -rw-r--r--
lcp's pass over the book, chapters 1-8
     1 \chapter{Advanced Simplification, Recursion and Induction}
     2 
     3 Although we have already learned a lot about simplification, recursion and
     4 induction, there are some advanced proof techniques that we have not covered
     5 yet and which are worth learning. The three sections of this chapter are almost
     6 independent of each other and can be read in any order. Only the notion of
     7 \emph{congruence rules}, introduced in the section on simplification, is
     8 required for parts of the section on recursion.
     9 
    10 \input{Advanced/document/simp.tex}
    11 
    12 \section{Advanced forms of recursion}
    13 \index{*recdef|(}
    14 
    15 The purpose of this section is to introduce advanced forms of
    16 \isacommand{recdef}: how to define recursive function over nested recursive
    17 datatypes, how to establish termination by means other than measure functions,
    18 and how to deal with partial functions.
    19 
    20 If, after reading this section, you feel that the definition of recursive
    21 functions is overly complicated by the requirement of
    22 totality, you should ponder the alternative, a logic of partial functions,
    23 where recursive definitions are always wellformed. For a start, there are many
    24 such logics, and no clear winner has emerged. And in all of these logics you
    25 are (more or less frequently) required to reason about the definedness of
    26 terms explicitly. Thus one shifts definedness arguments from definition time to
    27 proof time. In HOL you may have to work hard to define a function, but proofs
    28 can then proceed unencumbered by worries about undefinedness.
    29 
    30 \subsection{Recursion over nested datatypes}
    31 \label{sec:nested-recdef}
    32 \input{Recdef/document/Nested0.tex}
    33 \input{Recdef/document/Nested1.tex}
    34 \input{Recdef/document/Nested2.tex}
    35 
    36 \subsection{Beyond measure}
    37 \label{sec:beyond-measure}
    38 \input{Advanced/document/WFrec.tex}
    39 
    40 \subsection{Partial functions}
    41 \index{partial function}
    42 \input{Advanced/document/Partial.tex}
    43 
    44 \index{*recdef|)}
    45 
    46 \section{Advanced induction techniques}
    47 \label{sec:advanced-ind}
    48 \index{induction|(}
    49 \input{Misc/document/AdvancedInd.tex}
    50 \input{CTL/document/CTLind.tex}
    51 \index{induction|)}