diff -r 3c82b641b642 -r 094b76968484 doc-src/TutorialI/Inductive/even-example.tex
--- a/doc-src/TutorialI/Inductive/even-example.tex	Wed Feb 21 12:07:00 2001 +0100
+++ b/doc-src/TutorialI/Inductive/even-example.tex	Wed Feb 21 12:57:55 2001 +0100
@@ -24,12 +24,11 @@
 
 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:
+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
@@ -217,5 +216,92 @@
 \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.
+
+\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.