1\chapter{Advanced Simplification and Induction}
2
3Although we have already learned a lot about simplification and
4induction, there are some advanced proof techniques that we have not covered
5yet and which are worth learning. The sections of this chapter are
6independent of each other and can be read in any order.
7
8\input{simp2.tex}
9
10\section{Advanced Induction Techniques}
11\label{sec:advanced-ind}
12\index{induction|(}
13\input{AdvancedInd.tex}
14\input{CTLind.tex}
15\index{induction|)}
16
17%\section{Advanced Forms of Recursion}
18%\index{recdef@\isacommand {recdef} (command)|(}
19
20%This section introduces advanced forms of
21%\isacommand{recdef}: how to establish termination by means other than measure
22%functions, how to define recursive functions over nested recursive datatypes
23%and how to deal with partial functions.
24%
25%If, after reading this section, you feel that the definition of recursive
26%functions is overly complicated by the requirement of
27%totality, you should ponder the alternatives.  In a logic of partial functions,
28%recursive definitions are always accepted.  But there are many
29%such logics, and no clear winner has emerged. And in all of these logics you
30%are (more or less frequently) required to reason about the definedness of
31%terms explicitly. Thus one shifts definedness arguments from definition time to
32%proof time. In HOL you may have to work hard to define a function, but proofs
33%can then proceed unencumbered by worries about undefinedness.
34
35%\subsection{Beyond Measure}
36%\label{sec:beyond-measure}
37%\input{WFrec.tex}
38%
39%\subsection{Recursion Over Nested Datatypes}
40%\label{sec:nested-recdef}
41%\input{Nested0.tex}
42%\input{Nested1.tex}
43%\input{Nested2.tex}
44%
45%\subsection{Partial Functions}
46%\index{functions!partial}
47%\input{Partial.tex}
48%
49%\index{recdef@\isacommand {recdef} (command)|)}
50