--- 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.