%
\begin{isabellebody}%
\def\isabellecontext{AdvancedInd}%
\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
Now that we have learned about rules and logic, we take another look at the
finer points of induction. We consider two questions: what to do if the
proposition to be proved is not directly amenable to induction
(\S\ref{sec:ind-var-in-prems}), and how to utilize (\S\ref{sec:complete-ind})
and even derive (\S\ref{sec:derive-ind}) new induction schemas. We conclude
with an extended example of induction (\S\ref{sec:CTL-revisited}).%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Massaging the Proposition%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\label{sec:ind-var-in-prems}
Often we have assumed that the theorem to be proved is already in a form
that is amenable to induction, but sometimes it isn't.
Here is an example.
Since \isa{hd} and \isa{last} return the first and last element of a
non-empty list, this lemma looks easy to prove:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}\isanewline
\isamarkupfalse%
\isamarkupfalse%
\isamarkuptrue%
\isamarkupfalse%
\isacommand{lemma}\ hd{\isacharunderscore}rev\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}\isamarkupfalse%
\isamarkupfalse%
\isamarkuptrue%
\isamarkupfalse%
%
\isamarkupsubsection{Beyond Structural and Recursion Induction%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\label{sec:complete-ind}
So far, inductive proofs were by structural induction for
primitive recursive functions and recursion induction for total recursive
functions. But sometimes structural induction is awkward and there is no
recursive function that could furnish a more appropriate
induction schema. In such cases a general-purpose induction schema can
be helpful. We show how to apply such induction schemas by an example.
Structural induction on \isa{nat} is
usually known as mathematical induction. There is also \textbf{complete}
\index{induction!complete}%
induction, where you prove $P(n)$ under the assumption that $P(m)$
holds for all $m<n$. In Isabelle, this is the theorem \tdx{nat_less_induct}:
\begin{isabelle}%
\ \ \ \ \ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n%
\end{isabelle}
As an application, we prove a property of the following
function:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
\isamarkupfalse%
\isacommand{axioms}\ f{\isacharunderscore}ax{\isacharcolon}\ {\isachardoublequote}f{\isacharparenleft}f{\isacharparenleft}n{\isacharparenright}{\isacharparenright}\ {\isacharless}\ f{\isacharparenleft}Suc{\isacharparenleft}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
%
\begin{isamarkuptext}%
\begin{warn}
We discourage the use of axioms because of the danger of
inconsistencies. Axiom \isa{f{\isacharunderscore}ax} does
not introduce an inconsistency because, for example, the identity function
satisfies it. Axioms can be useful in exploratory developments, say when
you assume some well-known theorems so that you can quickly demonstrate some
point about methodology. If your example turns into a substantial proof
development, you should replace axioms by theorems.
\end{warn}\noindent
The axiom for \isa{f} implies \isa{n\ {\isasymle}\ f\ n}, which can
be proved by induction on \mbox{\isa{f\ n}}. Following the recipe outlined
above, we have to phrase the proposition as follows to allow induction:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}\isamarkupfalse%
\isamarkuptrue%
\isamarkupfalse%
\isamarkuptrue%
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
\isamarkuptrue%
\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
If you find the last step puzzling, here are the two lemmas it employs:
\begin{isabelle}
\isa{m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ Suc\ m\ {\isasymle}\ n}
\rulename{Suc_leI}\isanewline
\isa{{\isasymlbrakk}i\ {\isasymle}\ j{\isacharsemicolon}\ j\ {\isacharless}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharless}\ k}
\rulename{le_less_trans}
\end{isabelle}
%
The proof goes like this (writing \isa{j} instead of \isa{nat}).
Since \isa{i\ {\isacharequal}\ Suc\ j} it suffices to show
\hbox{\isa{j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}}},
by \isa{Suc{\isacharunderscore}leI}\@. This is
proved as follows. From \isa{f{\isacharunderscore}ax} we have \isa{f\ {\isacharparenleft}f\ j{\isacharparenright}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}}
(1) which implies \isa{f\ j\ {\isasymle}\ f\ {\isacharparenleft}f\ j{\isacharparenright}} by the induction hypothesis.
Using (1) once more we obtain \isa{f\ j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (2) by the transitivity
rule \isa{le{\isacharunderscore}less{\isacharunderscore}trans}.
Using the induction hypothesis once more we obtain \isa{j\ {\isasymle}\ f\ j}
which, together with (2) yields \isa{j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (again by
\isa{le{\isacharunderscore}less{\isacharunderscore}trans}).
This last step shows both the power and the danger of automatic proofs. They
will usually not tell you how the proof goes, because it can be hard to
translate the internal proof into a human-readable format. Automatic
proofs are easy to write but hard to read and understand.
The desired result, \isa{i\ {\isasymle}\ f\ i}, follows from \isa{f{\isacharunderscore}incr{\isacharunderscore}lem}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemmas}\ f{\isacharunderscore}incr\ {\isacharequal}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
The final \isa{refl} gets rid of the premise \isa{{\isacharquery}k\ {\isacharequal}\ f\ {\isacharquery}i}.
We could have included this derivation in the original statement of the lemma:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ f{\isacharunderscore}incr{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
\begin{exercise}
From the axiom and lemma for \isa{f}, show that \isa{f} is the
identity function.
\end{exercise}
Method \methdx{induct_tac} can be applied with any rule $r$
whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the
format is
\begin{quote}
\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $y@1 \dots y@n$ \isa{rule{\isacharcolon}} $r$\isa{{\isacharparenright}}
\end{quote}
where $y@1, \dots, y@n$ are variables in the first subgoal.
The conclusion of $r$ can even be an (iterated) conjunction of formulae of
the above form in which case the application is
\begin{quote}
\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $y@1 \dots y@n$ \isa{and} \dots\ \isa{and} $z@1 \dots z@m$ \isa{rule{\isacharcolon}} $r$\isa{{\isacharparenright}}
\end{quote}
A further useful induction rule is \isa{length{\isacharunderscore}induct},
induction on the length of a list\indexbold{*length_induct}
\begin{isabelle}%
\ \ \ \ \ {\isacharparenleft}{\isasymAnd}xs{\isachardot}\ {\isasymforall}ys{\isachardot}\ length\ ys\ {\isacharless}\ length\ xs\ {\isasymlongrightarrow}\ P\ ys\ {\isasymLongrightarrow}\ P\ xs{\isacharparenright}\ {\isasymLongrightarrow}\ P\ xs%
\end{isabelle}
which is a special case of \isa{measure{\isacharunderscore}induct}
\begin{isabelle}%
\ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ {\isasymforall}y{\isachardot}\ f\ y\ {\isacharless}\ f\ x\ {\isasymlongrightarrow}\ P\ y\ {\isasymLongrightarrow}\ P\ x{\isacharparenright}\ {\isasymLongrightarrow}\ P\ a%
\end{isabelle}
where \isa{f} may be any function into type \isa{nat}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Derivation of New Induction Schemas%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\label{sec:derive-ind}
\index{induction!deriving new schemas}%
Induction schemas are ordinary theorems and you can derive new ones
whenever you wish. This section shows you how, using the example
of \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}. Assume we only have structural induction
available for \isa{nat} and want to derive complete induction. We
must generalize the statement as shown:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ induct{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isasymAnd}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m{\isachardoublequote}\isanewline
\isamarkupfalse%
\isamarkupfalse%
\isamarkuptrue%
\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
The elimination rule \isa{less{\isacharunderscore}SucE} expresses the case distinction:
\begin{isabelle}%
\ \ \ \ \ {\isasymlbrakk}m\ {\isacharless}\ Suc\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ m\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
\end{isabelle}
Now it is straightforward to derive the original version of
\isa{nat{\isacharunderscore}less{\isacharunderscore}induct} by manipulating the conclusion of the above
lemma: instantiate \isa{n} by \isa{Suc\ n} and \isa{m} by \isa{n}
and remove the trivial condition \isa{n\ {\isacharless}\ Suc\ n}. Fortunately, this
happens automatically when we add the lemma as a new premise to the
desired goal:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{theorem}\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isasymAnd}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n{\isachardoublequote}\isanewline
\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
HOL already provides the mother of
all inductions, well-founded induction (see \S\ref{sec:Well-founded}). For
example theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} is
a special case of \isa{wf{\isacharunderscore}induct} where \isa{r} is \isa{{\isacharless}} on
\isa{nat}. The details can be found in theory \isa{Wellfounded_Recursion}.%
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: