1 \chapter{Advanced Simplification and Induction} |
|
2 |
|
3 Although we have already learned a lot about simplification and |
|
4 induction, there are some advanced proof techniques that we have not covered |
|
5 yet and which are worth learning. The sections of this chapter are |
|
6 independent 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)|)} |
|