3 Although we have already learned a lot about simplification and |
3 Although we have already learned a lot about simplification and |
4 induction, there are some advanced proof techniques that we have not covered |
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 |
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. |
6 independent of each other and can be read in any order. |
7 |
7 |
8 \input{Advanced/document/simp2.tex} |
8 \input{document/simp2.tex} |
9 |
9 |
10 \section{Advanced Induction Techniques} |
10 \section{Advanced Induction Techniques} |
11 \label{sec:advanced-ind} |
11 \label{sec:advanced-ind} |
12 \index{induction|(} |
12 \index{induction|(} |
13 \input{Misc/document/AdvancedInd.tex} |
13 \input{document/AdvancedInd.tex} |
14 \input{CTL/document/CTLind.tex} |
14 \input{document/CTLind.tex} |
15 \index{induction|)} |
15 \index{induction|)} |
16 |
16 |
17 %\section{Advanced Forms of Recursion} |
17 %\section{Advanced Forms of Recursion} |
18 %\index{recdef@\isacommand {recdef} (command)|(} |
18 %\index{recdef@\isacommand {recdef} (command)|(} |
19 |
19 |
32 %proof time. In HOL you may have to work hard to define a function, but proofs |
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. |
33 %can then proceed unencumbered by worries about undefinedness. |
34 |
34 |
35 %\subsection{Beyond Measure} |
35 %\subsection{Beyond Measure} |
36 %\label{sec:beyond-measure} |
36 %\label{sec:beyond-measure} |
37 %\input{Advanced/document/WFrec.tex} |
37 %\input{document/WFrec.tex} |
38 % |
38 % |
39 %\subsection{Recursion Over Nested Datatypes} |
39 %\subsection{Recursion Over Nested Datatypes} |
40 %\label{sec:nested-recdef} |
40 %\label{sec:nested-recdef} |
41 %\input{Recdef/document/Nested0.tex} |
41 %\input{document/Nested0.tex} |
42 %\input{Recdef/document/Nested1.tex} |
42 %\input{document/Nested1.tex} |
43 %\input{Recdef/document/Nested2.tex} |
43 %\input{document/Nested2.tex} |
44 % |
44 % |
45 %\subsection{Partial Functions} |
45 %\subsection{Partial Functions} |
46 %\index{functions!partial} |
46 %\index{functions!partial} |
47 %\input{Advanced/document/Partial.tex} |
47 %\input{document/Partial.tex} |
48 % |
48 % |
49 %\index{recdef@\isacommand {recdef} (command)|)} |
49 %\index{recdef@\isacommand {recdef} (command)|)} |