%

\begin{isabellebody}%

\def\isabellecontext{AdvancedInd}%

%

\isadelimtheory

%

\endisadelimtheory

%

\isatagtheory

%

\endisatagtheory

{\isafoldtheory}%

%

\isadelimtheory

%

\endisadelimtheory

%

\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}\isamarkupfalse%

\ {\isachardoublequoteopen}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequoteclose}\isanewline

%

\isadelimproof

%

\endisadelimproof

%

\isatagproof

\isacommand{apply}\isamarkupfalse%

{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}%

\begin{isamarkuptxt}%

\noindent

But induction produces the warning

\begin{quote}\tt

Induction variable occurs also among premises!

\end{quote}

and leads to the base case

\begin{isabelle}%

\ {\isadigit{1}}{\isachardot}\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ last\ {\isacharbrackleft}{\isacharbrackright}%

\end{isabelle}

Simplification reduces the base case to this:

\begin{isabelle}

\ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ []

\end{isabelle}

We cannot prove this equality because we do not know what \isa{hd} and

\isa{last} return when applied to \isa{{\isacharbrackleft}{\isacharbrackright}}.

We should not have ignored the warning. Because the induction

formula is only the conclusion, induction does not affect the occurrence of \isa{xs} in the premises.  

Thus the case that should have been trivial

becomes unprovable. Fortunately, the solution is easy:\footnote{A similar

heuristic applies to rule inductions; see \S\ref{sec:rtc}.}

\begin{quote}

\emph{Pull all occurrences of the induction variable into the conclusion

using \isa{{\isasymlongrightarrow}}.}

\end{quote}

Thus we should state the lemma as an ordinary 

implication~(\isa{{\isasymlongrightarrow}}), letting

\attrdx{rule_format} (\S\ref{sec:forward}) convert the

result to the usual \isa{{\isasymLongrightarrow}} form:%

\end{isamarkuptxt}%

\isamarkuptrue%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

\isacommand{lemma}\isamarkupfalse%

\ hd{\isacharunderscore}rev\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequoteclose}%

\isadelimproof

%

\endisadelimproof

%

\isatagproof

%

\begin{isamarkuptxt}%

\noindent

This time, induction leaves us with a trivial base case:

\begin{isabelle}%

\ {\isadigit{1}}{\isachardot}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ last\ {\isacharbrackleft}{\isacharbrackright}%

\end{isabelle}

And \isa{auto} completes the proof.

If there are multiple premises $A@1$, \dots, $A@n$ containing the

induction variable, you should turn the conclusion $C$ into

\[ A@1 \longrightarrow \cdots A@n \longrightarrow C. \]

Additionally, you may also have to universally quantify some other variables,

which can yield a fairly complex conclusion.  However, \isa{rule{\isacharunderscore}format} 

can remove any number of occurrences of \isa{{\isasymforall}} and

\isa{{\isasymlongrightarrow}}.

\index{induction!on a term}%

A second reason why your proposition may not be amenable to induction is that

you want to induct on a complex term, rather than a variable. In

general, induction on a term~$t$ requires rephrasing the conclusion~$C$

as

\begin{equation}\label{eqn:ind-over-term}

\forall y@1 \dots y@n.~ x = t \longrightarrow C.

\end{equation}

where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is a new variable.

Now you can perform induction on~$x$. An example appears in

\S\ref{sec:complete-ind} below.

The very same problem may occur in connection with rule induction. Remember

that it requires a premise of the form $(x@1,\dots,x@k) \in R$, where $R$ is

some inductively defined set and the $x@i$ are variables.  If instead we have

a premise $t \in R$, where $t$ is not just an $n$-tuple of variables, we

replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as

\[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C. \]

For an example see \S\ref{sec:CTL-revisited} below.

Of course, all premises that share free variables with $t$ need to be pulled into

the conclusion as well, under the \isa{{\isasymforall}}, again using \isa{{\isasymlongrightarrow}} as shown above.

Readers who are puzzled by the form of statement

(\ref{eqn:ind-over-term}) above should remember that the

transformation is only performed to permit induction. Once induction

has been applied, the statement can be transformed back into something quite

intuitive. For example, applying wellfounded induction on $x$ (w.r.t.\

$\prec$) to (\ref{eqn:ind-over-term}) and transforming the result a

little leads to the goal

\[ \bigwedge\overline{y}.\ 

   \forall \overline{z}.\ t\,\overline{z} \prec t\,\overline{y}\ \longrightarrow\ C\,\overline{z}

    \ \Longrightarrow\ C\,\overline{y} \]

where $\overline{y}$ stands for $y@1 \dots y@n$ and the dependence of $t$ and

$C$ on the free variables of $t$ has been made explicit.

Unfortunately, this induction schema cannot be expressed as a

single theorem because it depends on the number of free variables in $t$ ---

the notation $\overline{y}$ is merely an informal device.%

\end{isamarkuptxt}%

\isamarkuptrue%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\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}\isamarkupfalse%

\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline

\isacommand{axioms}\isamarkupfalse%

\ f{\isacharunderscore}ax{\isacharcolon}\ {\isachardoublequoteopen}f{\isacharparenleft}f{\isacharparenleft}n{\isacharparenright}{\isacharparenright}\ {\isacharless}\ f{\isacharparenleft}Suc{\isacharparenleft}n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%

\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}\isamarkupfalse%

\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequoteclose}%

\isadelimproof

%

\endisadelimproof

%

\isatagproof

%

\begin{isamarkuptxt}%

\noindent

To perform induction on \isa{k} using \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}, we use

the same general induction method as for recursion induction (see

\S\ref{sec:fun-induction}):%

\end{isamarkuptxt}%

\isamarkuptrue%

\isacommand{apply}\isamarkupfalse%

{\isacharparenleft}induct{\isacharunderscore}tac\ k\ rule{\isacharcolon}\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharparenright}%

\begin{isamarkuptxt}%

\noindent

We get the following proof state:

\begin{isabelle}%

\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ {\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i\ {\isasymLongrightarrow}\ {\isasymforall}i{\isachardot}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i%

\end{isabelle}

After stripping the \isa{{\isasymforall}i}, the proof continues with a case

distinction on \isa{i}. The case \isa{i\ {\isacharequal}\ {\isadigit{0}}} is trivial and we focus on

the other case:%

\end{isamarkuptxt}%

\isamarkuptrue%

\isacommand{apply}\isamarkupfalse%

{\isacharparenleft}rule\ allI{\isacharparenright}\isanewline

\isacommand{apply}\isamarkupfalse%

{\isacharparenleft}case{\isacharunderscore}tac\ i{\isacharparenright}\isanewline

\ \isacommand{apply}\isamarkupfalse%

{\isacharparenleft}simp{\isacharparenright}%

\begin{isamarkuptxt}%

\begin{isabelle}%

\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n\ i\ nat{\isachardot}\isanewline

\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}m{\isacharless}n{\isachardot}\ {\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isacharsemicolon}\ i\ {\isacharequal}\ Suc\ nat{\isasymrbrakk}\ {\isasymLongrightarrow}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i%

\end{isabelle}%

\end{isamarkuptxt}%

\isamarkuptrue%

\isacommand{by}\isamarkupfalse%

{\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}\ le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\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}x\ {\isasymle}\ y{\isacharsemicolon}\ y\ {\isacharless}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}\ z}

\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}\isamarkupfalse%

\ f{\isacharunderscore}incr\ {\isacharequal}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}%

\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}\isamarkupfalse%

\ f{\isacharunderscore}incr{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequoteclose}%

\isadelimproof

%

\endisadelimproof

%

\isatagproof

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\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 conclusion of the first subgoal.

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}\isamarkupfalse%

\ induct{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequoteopen}{\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{\isachardoublequoteclose}\isanewline

%

\isadelimproof

%

\endisadelimproof

%

\isatagproof

\isacommand{apply}\isamarkupfalse%

{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}%

\begin{isamarkuptxt}%

\noindent

The base case is vacuously true. For the induction step (\isa{m\ {\isacharless}\ Suc\ n}) we distinguish two cases: case \isa{m\ {\isacharless}\ n} is true by induction

hypothesis and case \isa{m\ {\isacharequal}\ n} follows from the assumption, again using

the induction hypothesis:%

\end{isamarkuptxt}%

\isamarkuptrue%

\ \isacommand{apply}\isamarkupfalse%

{\isacharparenleft}blast{\isacharparenright}\isanewline

\isacommand{by}\isamarkupfalse%

{\isacharparenleft}blast\ elim{\isacharcolon}\ less{\isacharunderscore}SucE{\isacharparenright}%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\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}\isamarkupfalse%

\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymAnd}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n{\isachardoublequoteclose}\isanewline

%

\isadelimproof

%

\endisadelimproof

%

\isatagproof

\isacommand{by}\isamarkupfalse%

{\isacharparenleft}insert\ induct{\isacharunderscore}lem{\isacharcomma}\ blast{\isacharparenright}%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\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%

%

\isadelimtheory

%

\endisadelimtheory

%

\isatagtheory

%

\endisatagtheory

{\isafoldtheory}%

%

\isadelimtheory

%

\endisadelimtheory

\end{isabellebody}%

%%% Local Variables:

%%% mode: latex

%%% TeX-master: "root"

%%% End: