% $Id$

\section{The Set of Even Numbers}

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 \isacommand{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!}, 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}

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}

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.

\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 \isa{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}

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 \isacommand{inductive\_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!}, 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

\isacommand{inductive\_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.