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