doc-src/TutorialI/Advanced/advanced.tex

*** empty log message ***

\chapter{Advanced Simplification, Recursion and Induction}

Although we have already learned a lot about simplification, recursion and
induction, there are some advanced proof techniques that we have not covered
yet and which are worth knowing about if you intend to beome a serious
(human) theorem prover. The three sections of this chapter are almost
independent of each other and can be read in any order. Only the notion of
\emph{congruence rules}, introduced in the section on simplification, is
required for parts of the section on recursion.

\input{Advanced/document/simp.tex}

\section{Advanced forms of recursion}
\index{*recdef|(}

The purpose of this section is to introduce advanced forms of \isacommand{recdef}. It
covers two topics: how to define recursive function over nested recursive datatypes
and how to establish termination by means other than measure functions.

If, after reading this section, you feel that the definition of recursive
functions is overly and maybe unnecessarily complicated by the requirement of
totality, you should ponder the alternative, a logic of partial functions,
where recursive definitions are always wellformed. For a start, there are many
such logics, and no clear winner has emerged. And in all of these logics you
are (more or less frequently) required to reason about the definedness of
terms explicitly. Thus one shifts definedness arguments from definition to
proof time. In HOL you may have to work hard to define a function, but proofs
can then proceed unencumbered by worries about undefinedness.

\subsection{Recursion over nested datatypes}
\label{sec:nested-recdef}
\input{Recdef/document/Nested0.tex}
\input{Recdef/document/Nested1.tex}
\input{Recdef/document/Nested2.tex}
\index{*recdef|)}

\subsection{Beyond measure}
\label{sec:wellfounded}
\input{Advanced/document/WFrec.tex}

\section{Advanced induction techniques}
\label{sec:advanced-ind}
\index{induction|(}
\input{Misc/document/AdvancedInd.tex}
\input{CTL/document/CTLind.tex}
\index{induction|)}