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

 % $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 \isacommand{inductive} declaration gives it the
+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

 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 
+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}

 \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

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

 \ 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.
+\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 \isa{iff}
-attribute because of its obvious value for simplification.
+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}
 
-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\@.
+\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

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

 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
+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}

 \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}
+\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.
+used.  Later examples will show that they are actually worth using.%
+\index{rule inversion|)}%
+\index{even numbers!defining inductively|)}