% $Id$
\section{The Set of Even Numbers}
\index{even numbers!defining inductively|(}%
The set of even numbers can be inductively defined as the least set
containing 0 and closed under the operation $+2$. Obviously,
\emph{even} can also be expressed using the divides relation (\isa{dvd}).
We shall prove below that the two formulations coincide. On the way we
shall examine the primary means of reasoning about inductively defined
sets: rule induction.
\subsection{Making an Inductive Definition}
Using \isacommand{consts}, we declare the constant \isa{even} to be a set
of natural numbers. The \commdx{inductive} declaration gives it the
desired properties.
\begin{isabelle}
\isacommand{consts}\ even\ ::\ "nat\ set"\isanewline
\isacommand{inductive}\ even\isanewline
\isakeyword{intros}\isanewline
zero[intro!]:\ "0\ \isasymin \ even"\isanewline
step[intro!]:\ "n\ \isasymin \ even\ \isasymLongrightarrow \ (Suc\ (Suc\
n))\ \isasymin \ even"
\end{isabelle}
An inductive definition consists of introduction rules. The first one
above states that 0 is even; the second states that if $n$ is even, then so
is~$n+2$. Given this declaration, Isabelle generates a fixed point
definition for \isa{even} and proves theorems about it,
thus following the definitional approach (see \S\ref{sec:definitional}).
These theorems
include the introduction rules specified in the declaration, an elimination
rule for case analysis and an induction rule. We can refer to these
theorems by automatically-generated names. Here are two examples:
%
\begin{isabelle}
0\ \isasymin \ even
\rulename{even.zero}
\par\smallskip
n\ \isasymin \ even\ \isasymLongrightarrow \ Suc\ (Suc\ n)\ \isasymin \
even%
\rulename{even.step}
\end{isabelle}
The introduction rules can be given attributes. Here
both rules are specified as \isa{intro!},%
\index{intro"!@\isa {intro"!} (attribute)}
directing the classical reasoner to
apply them aggressively. Obviously, regarding 0 as even is safe. The
\isa{step} rule is also safe because $n+2$ is even if and only if $n$ is
even. We prove this equivalence later.
\subsection{Using Introduction Rules}
Our first lemma states that numbers of the form $2\times k$ are even.
Introduction rules are used to show that specific values belong to the
inductive set. Such proofs typically involve
induction, perhaps over some other inductive set.
\begin{isabelle}
\isacommand{lemma}\ two_times_even[intro!]:\ "\#2*k\ \isasymin \ even"
\isanewline
\isacommand{apply}\ (induct\ "k")\isanewline
\ \isacommand{apply}\ auto\isanewline
\isacommand{done}
\end{isabelle}
%
The first step is induction on the natural number \isa{k}, which leaves
two subgoals:
\begin{isabelle}
\ 1.\ \#2\ *\ 0\ \isasymin \ even\isanewline
\ 2.\ \isasymAnd n.\ \#2\ *\ n\ \isasymin \ even\ \isasymLongrightarrow \ \#2\ *\ Suc\ n\ \isasymin \ even
\end{isabelle}
%
Here \isa{auto} simplifies both subgoals so that they match the introduction
rules, which are then applied automatically.
Our ultimate goal is to prove the equivalence between the traditional
definition of \isa{even} (using the divides relation) and our inductive
definition. One direction of this equivalence is immediate by the lemma
just proved, whose \isa{intro!} attribute ensures it is applied automatically.
\begin{isabelle}
\isacommand{lemma}\ dvd_imp_even:\ "\#2\ dvd\ n\ \isasymLongrightarrow \ n\ \isasymin \ even"\isanewline
\isacommand{by}\ (auto\ simp\ add:\ dvd_def)
\end{isabelle}
\subsection{Rule Induction}
\label{sec:rule-induction}
\index{rule induction|(}%
From the definition of the set
\isa{even}, Isabelle has
generated an induction rule:
\begin{isabelle}
\isasymlbrakk xa\ \isasymin \ even;\isanewline
\ P\ 0;\isanewline
\ \isasymAnd n.\ \isasymlbrakk n\ \isasymin \ even;\ P\ n\isasymrbrakk \
\isasymLongrightarrow \ P\ (Suc\ (Suc\ n))\isasymrbrakk\isanewline
\ \isasymLongrightarrow \ P\ xa%
\rulename{even.induct}
\end{isabelle}
A property \isa{P} holds for every even number provided it
holds for~\isa{0} and is closed under the operation
\isa{Suc(Suc \(\cdot\))}. Then \isa{P} is closed under the introduction
rules for \isa{even}, which is the least set closed under those rules.
This type of inductive argument is called \textbf{rule induction}.
Apart from the double application of \isa{Suc}, the induction rule above
resembles the familiar mathematical induction, which indeed is an instance
of rule induction; the natural numbers can be defined inductively to be
the least set containing \isa{0} and closed under~\isa{Suc}.
Induction is the usual way of proving a property of the elements of an
inductively defined set. Let us prove that all members of the set
\isa{even} are multiples of two.
\begin{isabelle}
\isacommand{lemma}\ even_imp_dvd:\ "n\ \isasymin \ even\ \isasymLongrightarrow \ \#2\ dvd\ n"
\end{isabelle}
%
We begin by applying induction. Note that \isa{even.induct} has the form
of an elimination rule, so we use the method \isa{erule}. We get two
subgoals:
\begin{isabelle}
\isacommand{apply}\ (erule\ even.induct)
\isanewline\isanewline
\ 1.\ \#2\ dvd\ 0\isanewline
\ 2.\ \isasymAnd n.\ \isasymlbrakk n\ \isasymin \ even;\ \#2\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ \#2\ dvd\ Suc\ (Suc\ n)
\end{isabelle}
%
We unfold the definition of \isa{dvd} in both subgoals, proving the first
one and simplifying the second:
\begin{isabelle}
\isacommand{apply}\ (simp_all\ add:\ dvd_def)
\isanewline\isanewline
\ 1.\ \isasymAnd n.\ \isasymlbrakk n\ \isasymin \ even;\ \isasymexists k.\
n\ =\ \#2\ *\ k\isasymrbrakk \ \isasymLongrightarrow \ \isasymexists k.\
Suc\ (Suc\ n)\ =\ \#2\ *\ k
\end{isabelle}
%
The next command eliminates the existential quantifier from the assumption
and replaces \isa{n} by \isa{\#2\ *\ k}.
\begin{isabelle}
\isacommand{apply}\ clarify
\isanewline\isanewline
\ 1.\ \isasymAnd n\ k.\ \#2\ *\ k\ \isasymin \ even\ \isasymLongrightarrow \ \isasymexists ka.\ Suc\ (Suc\ (\#2\ *\ k))\ =\ \#2\ *\ ka%
\end{isabelle}
%
To conclude, we tell Isabelle that the desired value is
\isa{Suc\ k}. With this hint, the subgoal falls to \isa{simp}.
\begin{isabelle}
\isacommand{apply}\ (rule_tac\ x\ =\ "Suc\ k"\ \isakeyword{in}\ exI, simp)
\end{isabelle}
\medskip
Combining the previous two results yields our objective, the
equivalence relating \isa{even} and \isa{dvd}.
%
%we don't want [iff]: discuss?
\begin{isabelle}
\isacommand{theorem}\ even_iff_dvd:\ "(n\ \isasymin \ even)\ =\ (\#2\ dvd\ n)"\isanewline
\isacommand{by}\ (blast\ intro:\ dvd_imp_even\ even_imp_dvd)
\end{isabelle}
\subsection{Generalization and Rule Induction}
\label{sec:gen-rule-induction}
\index{generalizing for induction}%
Before applying induction, we typically must generalize
the induction formula. With rule induction, the required generalization
can be hard to find and sometimes requires a complete reformulation of the
problem. In this example, our first attempt uses the obvious statement of
the result. It fails:
%
\begin{isabelle}
\isacommand{lemma}\ "Suc\ (Suc\ n)\ \isasymin \ even\
\isasymLongrightarrow \ n\ \isasymin \ even"\isanewline
\isacommand{apply}\ (erule\ even.induct)\isanewline
\isacommand{oops}
\end{isabelle}
%
Rule induction finds no occurrences of \isa{Suc(Suc\ n)} in the
conclusion, which it therefore leaves unchanged. (Look at
\isa{even.induct} to see why this happens.) We have these subgoals:
\begin{isabelle}
\ 1.\ n\ \isasymin \ even\isanewline
\ 2.\ \isasymAnd na.\ \isasymlbrakk na\ \isasymin \ even;\ n\ \isasymin \ even\isasymrbrakk \ \isasymLongrightarrow \ n\ \isasymin \ even%
\end{isabelle}
The first one is hopeless. Rule inductions involving
non-trivial terms usually fail. How to deal with such situations
in general is described in {\S}\ref{sec:ind-var-in-prems} below.
In the current case the solution is easy because
we have the necessary inverse, subtraction:
\begin{isabelle}
\isacommand{lemma}\ even_imp_even_minus_2:\ "n\ \isasymin \ even\ \isasymLongrightarrow \ n-\#2\ \isasymin \ even"\isanewline
\isacommand{apply}\ (erule\ even.induct)\isanewline
\ \isacommand{apply}\ auto\isanewline
\isacommand{done}
\end{isabelle}
%
This lemma is trivially inductive. Here are the subgoals:
\begin{isabelle}
\ 1.\ 0\ -\ \#2\ \isasymin \ even\isanewline
\ 2.\ \isasymAnd n.\ \isasymlbrakk n\ \isasymin \ even;\ n\ -\ \#2\ \isasymin \ even\isasymrbrakk \ \isasymLongrightarrow \ Suc\ (Suc\ n)\ -\ \#2\ \isasymin \ even%
\end{isabelle}
The first is trivial because \isa{0\ -\ \#2} simplifies to \isa{0}, which is
even. The second is trivial too: \isa{Suc\ (Suc\ n)\ -\ \#2} simplifies to
\isa{n}, matching the assumption.%
\index{rule induction|)} %the sequel isn't really about induction
\medskip
Using our lemma, we can easily prove the result we originally wanted:
\begin{isabelle}
\isacommand{lemma}\ Suc_Suc_even_imp_even:\ "Suc\ (Suc\ n)\ \isasymin \ even\ \isasymLongrightarrow \ n\ \isasymin \ even"\isanewline
\isacommand{by}\ (drule\ even_imp_even_minus_2, simp)
\end{isabelle}
We have just proved the converse of the introduction rule \isa{even.step}.
This suggests proving the following equivalence. We give it the
\attrdx{iff} attribute because of its obvious value for simplification.
\begin{isabelle}
\isacommand{lemma}\ [iff]:\ "((Suc\ (Suc\ n))\ \isasymin \ even)\ =\ (n\
\isasymin \ even)"\isanewline
\isacommand{by}\ (blast\ dest:\ Suc_Suc_even_imp_even)
\end{isabelle}
\subsection{Rule Inversion}\label{sec:rule-inversion}
\index{rule inversion|(}%
Case analysis on an inductive definition is called \textbf{rule
inversion}. It is frequently used in proofs about operational
semantics. It can be highly effective when it is applied
automatically. Let us look at how rule inversion is done in
Isabelle/HOL\@.
Recall that \isa{even} is the minimal set closed under these two rules:
\begin{isabelle}
0\ \isasymin \ even\isanewline
n\ \isasymin \ even\ \isasymLongrightarrow \ Suc\ (Suc\ n)\ \isasymin
\ even
\end{isabelle}
Minimality means that \isa{even} contains only the elements that these
rules force it to contain. If we are told that \isa{a}
belongs to
\isa{even} then there are only two possibilities. Either \isa{a} is \isa{0}
or else \isa{a} has the form \isa{Suc(Suc~n)}, for some suitable \isa{n}
that belongs to
\isa{even}. That is the gist of the \isa{cases} rule, which Isabelle proves
for us when it accepts an inductive definition:
\begin{isabelle}
\isasymlbrakk a\ \isasymin \ even;\isanewline
\ a\ =\ 0\ \isasymLongrightarrow \ P;\isanewline
\ \isasymAnd n.\ \isasymlbrakk a\ =\ Suc(Suc\ n);\ n\ \isasymin \
even\isasymrbrakk \ \isasymLongrightarrow \ P\isasymrbrakk \
\isasymLongrightarrow \ P
\rulename{even.cases}
\end{isabelle}
This general rule is less useful than instances of it for
specific patterns. For example, if \isa{a} has the form
\isa{Suc(Suc~n)} then the first case becomes irrelevant, while the second
case tells us that \isa{n} belongs to \isa{even}. Isabelle will generate
this instance for us:
\begin{isabelle}
\isacommand{inductive\_cases}\ Suc_Suc_cases\ [elim!]:
\ "Suc(Suc\ n)\ \isasymin \ even"
\end{isabelle}
The \commdx{inductive\protect\_cases} command generates an instance of
the
\isa{cases} rule for the supplied pattern and gives it the supplied name:
%
\begin{isabelle}
\isasymlbrakk Suc(Suc\ n)\ \isasymin \ even;\ n\ \isasymin \ even\
\isasymLongrightarrow \ P\isasymrbrakk \ \isasymLongrightarrow \ P%
\rulename{Suc_Suc_cases}
\end{isabelle}
%
Applying this as an elimination rule yields one case where \isa{even.cases}
would yield two. Rule inversion works well when the conclusions of the
introduction rules involve datatype constructors like \isa{Suc} and \isa{\#}
(list ``cons''); freeness reasoning discards all but one or two cases.
In the \isacommand{inductive\_cases} command we supplied an
attribute, \isa{elim!},
\index{elim"!@\isa {elim"!} (attribute)}%
indicating that this elimination rule can be
applied aggressively. The original
\isa{cases} rule would loop if used in that manner because the
pattern~\isa{a} matches everything.
The rule \isa{Suc_Suc_cases} is equivalent to the following implication:
\begin{isabelle}
Suc (Suc\ n)\ \isasymin \ even\ \isasymLongrightarrow \ n\ \isasymin \
even
\end{isabelle}
%
Just above we devoted some effort to reaching precisely
this result. Yet we could have obtained it by a one-line declaration,
dispensing with the lemma \isa{even_imp_even_minus_2}.
This example also justifies the terminology
\textbf{rule inversion}: the new rule inverts the introduction rule
\isa{even.step}.
For one-off applications of rule inversion, use the \isa{ind_cases} method.
Here is an example:
\begin{isabelle}
\isacommand{apply}\ (ind_cases\ "Suc(Suc\ n)\ \isasymin \ even")
\end{isabelle}
The specified instance of the \isa{cases} rule is generated, then applied
as an elimination rule.
To summarize, every inductive definition produces a \isa{cases} rule. The
\commdx{inductive\protect\_cases} command stores an instance of the
\isa{cases} rule for a given pattern. Within a proof, the
\isa{ind_cases} method applies an instance of the \isa{cases}
rule.
The even numbers example has shown how inductive definitions can be
used. Later examples will show that they are actually worth using.%
\index{rule inversion|)}%
\index{even numbers!defining inductively|)}