doc-src/TutorialI/Inductive/even-example.tex

A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.

% $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_tac\ 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 induction on
a non-variable term discards information, and usually fails.
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}.  In general, a rule can be inverted when the set of elements
it introduces is disjoint from those of the other introduction rules.

For one-off applications of rule inversion, use the \methdx{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|)}