\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 learning. 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@\isacommand {recdef} (command)|(}

This section introduces advanced forms of

\isacommand{recdef}: how to establish termination by means other than measure

functions, how to define recursive functions over nested recursive datatypes

and how to deal with partial functions.

If, after reading this section, you feel that the definition of recursive

functions is overly complicated by the requirement of

totality, you should ponder the alternatives.  In a logic of partial functions,

recursive definitions are always accepted.  But 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 time 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{Beyond Measure}

\label{sec:beyond-measure}

\input{Advanced/document/WFrec.tex}

\subsection{Recursion Over Nested Datatypes}

\label{sec:nested-recdef}

\input{Recdef/document/Nested0.tex}

\input{Recdef/document/Nested1.tex}

\input{Recdef/document/Nested2.tex}

\subsection{Partial Functions}

\index{functions!partial}

\input{Advanced/document/Partial.tex}

\index{recdef@\isacommand {recdef} (command)|)}

\section{Advanced Induction Techniques}

\label{sec:advanced-ind}

\index{induction|(}

\input{Misc/document/AdvancedInd.tex}

\input{CTL/document/CTLind.tex}

\index{induction|)}