src/Doc/Tutorial/document/advanced0.tex

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Tutorial/document/advanced0.tex	Tue Aug 28 18:57:32 2012 +0200
@@ -0,0 +1,49 @@
+\chapter{Advanced Simplification and Induction}
+
+Although we have already learned a lot about simplification and
+induction, there are some advanced proof techniques that we have not covered
+yet and which are worth learning. The sections of this chapter are
+independent of each other and can be read in any order.
+
+\input{simp2.tex}
+
+\section{Advanced Induction Techniques}
+\label{sec:advanced-ind}
+\index{induction|(}
+\input{AdvancedInd.tex}
+\input{CTLind.tex}
+\index{induction|)}
+
+%\section{Advanced Forms of Recursion}
+%\index{recdef@\isacommand {recdef} (command)|(}
+
+%This section introduces advanced forms of
+%\isacommand{recdef}: how to establish termination by means other than measure
+%functions, how to define recursive functions over nested recursive datatypes
+%and how to deal with partial functions.
+%
+%If, after reading this section, you feel that the definition of recursive
+%functions is overly complicated by the requirement of
+%totality, you should ponder the alternatives.  In a logic of partial functions,
+%recursive definitions are always accepted.  But there are many
+%such logics, and no clear winner has emerged. And in all of these logics you
+%are (more or less frequently) required to reason about the definedness of
+%terms explicitly. Thus one shifts definedness arguments from definition time to
+%proof time. In HOL you may have to work hard to define a function, but proofs
+%can then proceed unencumbered by worries about undefinedness.
+
+%\subsection{Beyond Measure}
+%\label{sec:beyond-measure}
+%\input{WFrec.tex}
+%
+%\subsection{Recursion Over Nested Datatypes}
+%\label{sec:nested-recdef}
+%\input{Nested0.tex}
+%\input{Nested1.tex}
+%\input{Nested2.tex}
+%
+%\subsection{Partial Functions}
+%\index{functions!partial}
+%\input{Partial.tex}
+%
+%\index{recdef@\isacommand {recdef} (command)|)}