doc-src/TutorialI/Advanced/advanced.tex

*** empty log message ***

\chapter{Advanced Simplification, Recursion and Induction}
\markboth{}{CHAPTER 4: ADVANCED SIMPLIFICATION, RECURSION ...}

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.

\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}
\index{induction|)}