diff -r b254d5ad6dd4 -r ca2b00c4bba7 doc-src/TutorialI/Inductive/even-example.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Inductive/even-example.tex	Fri Jan 12 16:09:33 2001 +0100
@@ -0,0 +1,222 @@
+% $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 ${\cdots}+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.  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 will be used.
+\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\(\cdots\))}.  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, 
+\isacommand{apply}\ 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, the obvious statement of the result is not
+inductive:
+%
+\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, \isacommand{apply}\ 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}
+
+The even numbers example has shown how inductive definitions can be used. 
+Later examples will show that they are actually worth using.