src/Doc/Tutorial/document/advanced0.tex

added lemmas relpowp_right_unique and relpow_right_unique

\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)|)}