LaTeX code is now generated directly from theory file.

--- a/doc-src/TutorialI/Inductive/Advanced.thy	Wed Jul 18 14:46:59 2007 +0200
+++ b/doc-src/TutorialI/Inductive/Advanced.thy	Thu Jul 19 15:29:51 2007 +0200
@@ -1,10 +1,61 @@
 (* ID:         $Id$ *)
-theory Advanced imports Even begin
+(*<*)theory Advanced imports Even uses "../../antiquote_setup.ML" begin(*>*)
+
+text {*
+The premises of introduction rules may contain universal quantifiers and
+monotone functions.  A universal quantifier lets the rule 
+refer to any number of instances of 
+the inductively defined set.  A monotone function lets the rule refer
+to existing constructions (such as ``list of'') over the inductively defined
+set.  The examples below show how to use the additional expressiveness
+and how to reason from the resulting definitions.
+*}
 
+subsection{* Universal Quantifiers in Introduction Rules \label{sec:gterm-datatype} *}
+
+text {*
+\index{ground terms example|(}%
+\index{quantifiers!and inductive definitions|(}%
+As a running example, this section develops the theory of \textbf{ground
+terms}: terms constructed from constant and function 
+symbols but not variables. To simplify matters further, we regard a
+constant as a function applied to the null argument  list.  Let us declare a
+datatype @{text gterm} for the type of ground  terms. It is a type constructor
+whose argument is a type of  function symbols. 
+*}
 
 datatype 'f gterm = Apply 'f "'f gterm list"
 
-datatype integer_op = Number int | UnaryMinus | Plus;
+text {*
+To try it out, we declare a datatype of some integer operations: 
+integer constants, the unary minus operator and the addition 
+operator.
+*}
+
+datatype integer_op = Number int | UnaryMinus | Plus
+
+text {*
+Now the type @{typ "integer_op gterm"} denotes the ground 
+terms built over those symbols.
+
+The type constructor @{text gterm} can be generalized to a function 
+over sets.  It returns 
+the set of ground terms that can be formed over a set @{text F} of function symbols. For
+example,  we could consider the set of ground terms formed from the finite 
+set @{text "{Number 2, UnaryMinus, Plus}"}.
+
+This concept is inductive. If we have a list @{text args} of ground terms 
+over~@{text F} and a function symbol @{text f} in @{text F}, then we 
+can apply @{text f} to @{text args} to obtain another ground term. 
+The only difficulty is that the argument list may be of any length. Hitherto, 
+each rule in an inductive definition referred to the inductively 
+defined set a fixed number of times, typically once or twice. 
+A universal quantifier in the premise of the introduction rule 
+expresses that every element of @{text args} belongs
+to our inductively defined set: is a ground term 
+over~@{text F}.  The function @{term set} denotes the set of elements in a given 
+list. 
+*}
 
 inductive_set
   gterms :: "'f set \<Rightarrow> 'f gterm set"
@@ -13,77 +64,56 @@
 step[intro!]: "\<lbrakk>\<forall>t \<in> set args. t \<in> gterms F;  f \<in> F\<rbrakk>
                \<Longrightarrow> (Apply f args) \<in> gterms F"
 
+text {*
+To demonstrate a proof from this definition, let us 
+show that the function @{term gterms}
+is \textbf{monotone}.  We shall need this concept shortly.
+*}
+
+lemma gterms_mono: "F\<subseteq>G \<Longrightarrow> gterms F \<subseteq> gterms G"
+apply clarify
+apply (erule gterms.induct)
+apply blast
+done
+(*<*)
 lemma gterms_mono: "F\<subseteq>G \<Longrightarrow> gterms F \<subseteq> gterms G"
 apply clarify
 apply (erule gterms.induct)
+(*>*)
 txt{*
-@{subgoals[display,indent=0,margin=65]}
-*};
-apply blast
-done
-
-
-text{*
-@{thm[display] even.cases[no_vars]}
-\rulename{even.cases}
-
-Just as a demo I include
-the two forms that Markus has made available. First the one for binding the
-result to a name 
-
+Intuitively, this theorem says that
+enlarging the set of function symbols enlarges the set of ground 
+terms. The proof is a trivial rule induction.
+First we use the @{text clarify} method to assume the existence of an element of
+@{term "gterms F"}.  (We could have used @{text "intro subsetI"}.)  We then
+apply rule induction. Here is the resulting subgoal:
+@{subgoals[display,indent=0]}
+The assumptions state that @{text f} belongs 
+to~@{text F}, which is included in~@{text G}, and that every element of the list @{text args} is
+a ground term over~@{text G}.  The @{text blast} method finds this chain of reasoning easily.  
 *}
-
-inductive_cases Suc_Suc_cases [elim!]:
-  "Suc(Suc n) \<in> even"
-
-thm Suc_Suc_cases;
-
-text{*
-@{thm[display] Suc_Suc_cases[no_vars]}
-\rulename{Suc_Suc_cases}
-
-and now the one for local usage:
-*}
-
-lemma "Suc(Suc n) \<in> even \<Longrightarrow> P n";
-apply (ind_cases "Suc(Suc n) \<in> even");
-oops
+(*<*)oops(*>*)
+text {*
+\begin{warn}
+Why do we call this function @{text gterms} instead 
+of @{text gterm}?  A constant may have the same name as a type.  However,
+name  clashes could arise in the theorems that Isabelle generates. 
+Our choice of names keeps @{text gterms.induct} separate from 
+@{text gterm.induct}.
+\end{warn}
 
-inductive_cases gterm_Apply_elim [elim!]: "Apply f args \<in> gterms F"
-
-text{*this is what we get:
-
-@{thm[display] gterm_Apply_elim[no_vars]}
-\rulename{gterm_Apply_elim}
+Call a term \textbf{well-formed} if each symbol occurring in it is applied
+to the correct number of arguments.  (This number is called the symbol's
+\textbf{arity}.)  We can express well-formedness by
+generalizing the inductive definition of
+\isa{gterms}.
+Suppose we are given a function called @{text arity}, specifying the arities
+of all symbols.  In the inductive step, we have a list @{text args} of such
+terms and a function  symbol~@{text f}. If the length of the list matches the
+function's arity  then applying @{text f} to @{text args} yields a well-formed
+term.
 *}
 
-lemma gterms_IntI [rule_format, intro!]:
-     "t \<in> gterms F \<Longrightarrow> t \<in> gterms G \<longrightarrow> t \<in> gterms (F\<inter>G)"
-apply (erule gterms.induct)
-txt{*
-@{subgoals[display,indent=0,margin=65]}
-*};
-apply blast
-done
-
-
-text{*
-@{thm[display] mono_Int[no_vars]}
-\rulename{mono_Int}
-*}
-
-lemma gterms_Int_eq [simp]:
-     "gterms (F\<inter>G) = gterms F \<inter> gterms G"
-by (blast intro!: mono_Int monoI gterms_mono)
-
-
-text{*the following declaration isn't actually used*}
-consts integer_arity :: "integer_op \<Rightarrow> nat"
-primrec
-"integer_arity (Number n)        = 0"
-"integer_arity UnaryMinus        = 1"
-"integer_arity Plus              = 2"
-
 inductive_set
   well_formed_gterm :: "('f \<Rightarrow> nat) \<Rightarrow> 'f gterm set"
   for arity :: "'f \<Rightarrow> nat"
@@ -92,6 +122,32 @@
                 length args = arity f\<rbrakk>
                \<Longrightarrow> (Apply f args) \<in> well_formed_gterm arity"
 
+text {*
+The inductive definition neatly captures the reasoning above.
+The universal quantification over the
+@{text set} of arguments expresses that all of them are well-formed.%
+\index{quantifiers!and inductive definitions|)}
+*}
+
+subsection{* Alternative Definition Using a Monotone Function *}
+
+text {*
+\index{monotone functions!and inductive definitions|(}% 
+An inductive definition may refer to the
+inductively defined  set through an arbitrary monotone function.  To
+demonstrate this powerful feature, let us
+change the  inductive definition above, replacing the
+quantifier by a use of the function @{term lists}. This
+function, from the Isabelle theory of lists, is analogous to the
+function @{term gterms} declared above: if @{text A} is a set then
+@{term "lists A"} is the set of lists whose elements belong to
+@{term A}.  
+
+In the inductive definition of well-formed terms, examine the one
+introduction rule.  The first premise states that @{text args} belongs to
+the @{text lists} of well-formed terms.  This formulation is more
+direct, if more obscure, than using a universal quantifier.
+*}
 
 inductive_set
   well_formed_gterm' :: "('f \<Rightarrow> nat) \<Rightarrow> 'f gterm set"
@@ -102,41 +158,214 @@
                \<Longrightarrow> (Apply f args) \<in> well_formed_gterm' arity"
 monos lists_mono
 
+text {*
+We cite the theorem @{text lists_mono} to justify 
+using the function @{term lists}.%
+\footnote{This particular theorem is installed by default already, but we
+include the \isakeyword{monos} declaration in order to illustrate its syntax.}
+@{named_thms [display,indent=0] lists_mono [no_vars] (lists_mono)}
+Why must the function be monotone?  An inductive definition describes
+an iterative construction: each element of the set is constructed by a
+finite number of introduction rule applications.  For example, the
+elements of \isa{even} are constructed by finitely many applications of
+the rules
+@{thm [display,indent=0] even.intros [no_vars]}
+All references to a set in its
+inductive definition must be positive.  Applications of an
+introduction rule cannot invalidate previous applications, allowing the
+construction process to converge.
+The following pair of rules do not constitute an inductive definition:
+\begin{trivlist}
+\item @{term "0 \<in> even"}
+\item @{term "n \<notin> even \<Longrightarrow> (Suc n) \<in> even"}
+\end{trivlist}
+Showing that 4 is even using these rules requires showing that 3 is not
+even.  It is far from trivial to show that this set of rules
+characterizes the even numbers.  
+
+Even with its use of the function \isa{lists}, the premise of our
+introduction rule is positive:
+@{thm_style [display,indent=0] prem1 step [no_vars]}
+To apply the rule we construct a list @{term args} of previously
+constructed well-formed terms.  We obtain a
+new term, @{term "Apply f args"}.  Because @{term lists} is monotone,
+applications of the rule remain valid as new terms are constructed.
+Further lists of well-formed
+terms become available and none are taken away.%
+\index{monotone functions!and inductive definitions|)} 
+*}
+
+subsection{* A Proof of Equivalence *}
+
+text {*
+We naturally hope that these two inductive definitions of ``well-formed'' 
+coincide.  The equality can be proved by separate inclusions in 
+each direction.  Each is a trivial rule induction. 
+*}
+
 lemma "well_formed_gterm arity \<subseteq> well_formed_gterm' arity"
 apply clarify
-txt{*
-The situation after clarify
-@{subgoals[display,indent=0,margin=65]}
-*};
+apply (erule well_formed_gterm.induct)
+apply auto
+done
+(*<*)
+lemma "well_formed_gterm arity \<subseteq> well_formed_gterm' arity"
+apply clarify
 apply (erule well_formed_gterm.induct)
-txt{*
-note the induction hypothesis!
-@{subgoals[display,indent=0,margin=65]}
-*};
+(*>*)
+txt {*
+The @{text clarify} method gives
+us an element of @{term "well_formed_gterm arity"} on which to perform 
+induction.  The resulting subgoal can be proved automatically:
+@{subgoals[display,indent=0]}
+This proof resembles the one given in
+{\S}\ref{sec:gterm-datatype} above, especially in the form of the
+induction hypothesis.  Next, we consider the opposite inclusion:
+*}
+(*<*)oops(*>*)
+lemma "well_formed_gterm' arity \<subseteq> well_formed_gterm arity"
+apply clarify
+apply (erule well_formed_gterm'.induct)
 apply auto
 done
+(*<*)
+lemma "well_formed_gterm' arity \<subseteq> well_formed_gterm arity"
+apply clarify
+apply (erule well_formed_gterm'.induct)
+(*>*)
+txt {*
+The proof script is identical, but the subgoal after applying induction may
+be surprising:
+@{subgoals[display,indent=0,margin=65]}
+The induction hypothesis contains an application of @{term lists}.  Using a
+monotone function in the inductive definition always has this effect.  The
+subgoal may look uninviting, but fortunately 
+@{term lists} distributes over intersection:
+@{named_thms [display,indent=0] lists_Int_eq [no_vars] (lists_Int_eq)}
+Thanks to this default simplification rule, the induction hypothesis 
+is quickly replaced by its two parts:
+\begin{trivlist}
+\item @{term "args \<in> lists (well_formed_gterm' arity)"}
+\item @{term "args \<in> lists (well_formed_gterm arity)"}
+\end{trivlist}
+Invoking the rule @{text well_formed_gterm.step} completes the proof.  The
+call to @{text auto} does all this work.
 
+This example is typical of how monotone functions
+\index{monotone functions} can be used.  In particular, many of them
+distribute over intersection.  Monotonicity implies one direction of
+this set equality; we have this theorem:
+@{named_thms [display,indent=0] mono_Int [no_vars] (mono_Int)}
+*}
+(*<*)oops(*>*)
 
 
-lemma "well_formed_gterm' arity \<subseteq> well_formed_gterm arity"
-apply clarify
-txt{*
-The situation after clarify
+subsection{* Another Example of Rule Inversion *}
+
+text {*
+\index{rule inversion|(}%
+Does @{term gterms} distribute over intersection?  We have proved that this
+function is monotone, so @{text mono_Int} gives one of the inclusions.  The
+opposite inclusion asserts that if @{term t} is a ground term over both of the
+sets
+@{term F} and~@{term G} then it is also a ground term over their intersection,
+@{term "F \<inter> G"}.
+*}
+
+lemma gterms_IntI:
+     "t \<in> gterms F \<Longrightarrow> t \<in> gterms G \<longrightarrow> t \<in> gterms (F\<inter>G)"
+(*<*)oops(*>*)
+text {*
+Attempting this proof, we get the assumption 
+@{term "Apply f args \<in> gterms G"}, which cannot be broken down. 
+It looks like a job for rule inversion:\cmmdx{inductive\protect\_cases}
+*}
+
+inductive_cases gterm_Apply_elim [elim!]: "Apply f args \<in> gterms F"
+
+text {*
+Here is the result.
+@{named_thms [display,indent=0,margin=50] gterm_Apply_elim [no_vars] (gterm_Apply_elim)}
+This rule replaces an assumption about @{term "Apply f args"} by 
+assumptions about @{term f} and~@{term args}.  
+No cases are discarded (there was only one to begin
+with) but the rule applies specifically to the pattern @{term "Apply f args"}.
+It can be applied repeatedly as an elimination rule without looping, so we
+have given the @{text "elim!"} attribute. 
+
+Now we can prove the other half of that distributive law.
+*}
+
+lemma gterms_IntI [rule_format, intro!]:
+     "t \<in> gterms F \<Longrightarrow> t \<in> gterms G \<longrightarrow> t \<in> gterms (F\<inter>G)"
+apply (erule gterms.induct)
+apply blast
+done
+(*<*)
+lemma "t \<in> gterms F \<Longrightarrow> t \<in> gterms G \<longrightarrow> t \<in> gterms (F\<inter>G)"
+apply (erule gterms.induct)
+(*>*)
+txt {*
+The proof begins with rule induction over the definition of
+@{term gterms}, which leaves a single subgoal:  
 @{subgoals[display,indent=0,margin=65]}
-*};
-apply (erule well_formed_gterm'.induct)
-txt{*
-note the induction hypothesis!
-@{subgoals[display,indent=0,margin=65]}
-*};
-apply auto
-done
+To prove this, we assume @{term "Apply f args \<in> gterms G"}.  Rule inversion,
+in the form of @{text gterm_Apply_elim}, infers
+that every element of @{term args} belongs to 
+@{term "gterms G"}; hence (by the induction hypothesis) it belongs
+to @{term "gterms (F \<inter> G)"}.  Rule inversion also yields
+@{term "f \<in> G"} and hence @{term "f \<in> F \<inter> G"}. 
+All of this reasoning is done by @{text blast}.
+
+\smallskip
+Our distributive law is a trivial consequence of previously-proved results:
+*}
+(*<*)oops(*>*)
+lemma gterms_Int_eq [simp]:
+     "gterms (F \<inter> G) = gterms F \<inter> gterms G"
+by (blast intro!: mono_Int monoI gterms_mono)
+
+text_raw {*
+\index{rule inversion|)}%
+\index{ground terms example|)}
 
 
-text{*
-@{thm[display] lists_Int_eq[no_vars]}
+\begin{isamarkuptext}
+\begin{exercise}
+A function mapping function symbols to their 
+types is called a \textbf{signature}.  Given a type 
+ranging over type symbols, we can represent a function's type by a
+list of argument types paired with the result type. 
+Complete this inductive definition:
+\begin{isabelle}
 *}
 
+inductive_set
+  well_typed_gterm :: "('f \<Rightarrow> 't list * 't) \<Rightarrow> ('f gterm * 't)set"
+  for sig :: "'f \<Rightarrow> 't list * 't"
+(*<*)
+where
+step[intro!]: 
+    "\<lbrakk>\<forall>pair \<in> set args. pair \<in> well_typed_gterm sig; 
+      sig f = (map snd args, rtype)\<rbrakk>
+     \<Longrightarrow> (Apply f (map fst args), rtype) 
+         \<in> well_typed_gterm sig"
+(*>*)
+text_raw {*
+\end{isabelle}
+\end{exercise}
+\end{isamarkuptext}
+*}
+
+(*<*)
+
+text{*the following declaration isn't actually used*}
+consts integer_arity :: "integer_op \<Rightarrow> nat"
+primrec
+"integer_arity (Number n)        = 0"
+"integer_arity UnaryMinus        = 1"
+"integer_arity Plus              = 2"
+
 text{* the rest isn't used: too complicated.  OK for an exercise though.*}
 
 inductive_set
@@ -146,17 +375,6 @@
 | UnaryMinus: "(UnaryMinus, ([()], ())) \<in> integer_signature"
 | Plus:       "(Plus,       ([(),()], ())) \<in> integer_signature"
 
-
-inductive_set
-  well_typed_gterm :: "('f \<Rightarrow> 't list * 't) \<Rightarrow> ('f gterm * 't)set"
-  for sig :: "'f \<Rightarrow> 't list * 't"
-where
-step[intro!]: 
-    "\<lbrakk>\<forall>pair \<in> set args. pair \<in> well_typed_gterm sig; 
-      sig f = (map snd args, rtype)\<rbrakk>
-     \<Longrightarrow> (Apply f (map fst args), rtype) 
-         \<in> well_typed_gterm sig"
-
 inductive_set
   well_typed_gterm' :: "('f \<Rightarrow> 't list * 't) \<Rightarrow> ('f gterm * 't)set"
   for sig :: "'f \<Rightarrow> 't list * 't"
@@ -183,4 +401,4 @@
 
 
 end
-
+(*>*)

--- a/doc-src/TutorialI/Inductive/Even.thy	Wed Jul 18 14:46:59 2007 +0200
+++ b/doc-src/TutorialI/Inductive/Even.thy	Thu Jul 19 15:29:51 2007 +0200
@@ -1,89 +1,290 @@
 (* ID:         $Id$ *)
-theory Even imports Main begin
+(*<*)theory Even imports Main uses "../../antiquote_setup.ML" begin(*>*)
+
+section{* The Set of Even Numbers *}
 
+text {*
+\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 (@{text 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 *}
+
+text {*
+Using \commdx{inductive\_set}, we declare the constant @{text even} to be
+a set of natural numbers with the desired properties.
+*}
 
 inductive_set even :: "nat set"
 where
   zero[intro!]: "0 \<in> even"
 | step[intro!]: "n \<in> even \<Longrightarrow> (Suc (Suc n)) \<in> even"
 
-text{*An inductive definition consists of introduction rules. 
-
-@{thm[display] even.step[no_vars]}
-\rulename{even.step}
+text {*
+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 @{term 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:
+@{named_thms[display,indent=0] even.zero[no_vars] (even.zero) even.step[no_vars] (even.step)}
 
-@{thm[display] even.induct[no_vars]}
-\rulename{even.induct}
+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
+@{text step} rule is also safe because $n+2$ is even if and only if $n$ is
+even.  We prove this equivalence later.
+*}
 
-Attributes can be given to the introduction rules.  Here both rules are
-specified as \isa{intro!}
+subsection{*Using Introduction Rules*}
 
-Our first lemma states that numbers of the form $2\times k$ are even. *}
+text {*
+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.
+*}
+
 lemma two_times_even[intro!]: "2*k \<in> even"
 apply (induct_tac k)
-txt{*
-The first step is induction on the natural number \isa{k}, which leaves
+ apply auto
+done
+(*<*)
+lemma "2*k \<in> even"
+apply (induct_tac k)
+(*>*)
+txt {*
+\noindent
+The first step is induction on the natural number @{text k}, which leaves
 two subgoals:
 @{subgoals[display,indent=0,margin=65]}
-Here \isa{auto} simplifies both subgoals so that they match the introduction
-rules, which then are applied automatically.*};
- apply auto
-done
+Here @{text auto} simplifies both subgoals so that they match the introduction
+rules, which are then applied automatically.
 
-text{*Our goal is to prove the equivalence between the traditional definition
-of even (using the divides relation) and our inductive definition.  Half of
-this equivalence is trivial using the lemma just proved, whose \isa{intro!}
-attribute ensures it will be applied automatically.  *}
-
+Our ultimate goal is to prove the equivalence between the traditional
+definition of @{text even} (using the divides relation) and our inductive
+definition.  One direction of this equivalence is immediate by the lemma
+just proved, whose @{text "intro!"} attribute ensures it is applied automatically.
+*}
+(*<*)oops(*>*)
 lemma dvd_imp_even: "2 dvd n \<Longrightarrow> n \<in> even"
 by (auto simp add: dvd_def)
 
-text{*our first rule induction!*}
+subsection{* Rule Induction \label{sec:rule-induction} *}
+
+text {*
+\index{rule induction|(}%
+From the definition of the set
+@{term even}, Isabelle has
+generated an induction rule:
+@{named_thms [display,indent=0,margin=40] even.induct [no_vars] (even.induct)}
+A property @{term P} holds for every even number provided it
+holds for~@{text 0} and is closed under the operation
+\isa{Suc(Suc \(\cdot\))}.  Then @{term P} is closed under the introduction
+rules for @{term 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 @{term 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 @{text 0} and closed under~@{term 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
+@{term even} are multiples of two.
+*}
+
 lemma even_imp_dvd: "n \<in> even \<Longrightarrow> 2 dvd n"
+txt {*
+We begin by applying induction.  Note that @{text even.induct} has the form
+of an elimination rule, so we use the method @{text erule}.  We get two
+subgoals:
+*}
 apply (erule even.induct)
-txt{*
-@{subgoals[display,indent=0,margin=65]}
-*};
+txt {*
+@{subgoals[display,indent=0]}
+We unfold the definition of @{text dvd} in both subgoals, proving the first
+one and simplifying the second:
+*}
 apply (simp_all add: dvd_def)
-txt{*
-@{subgoals[display,indent=0,margin=65]}
-*};
+txt {*
+@{subgoals[display,indent=0]}
+The next command eliminates the existential quantifier from the assumption
+and replaces @{text n} by @{text "2 * k"}.
+*}
 apply clarify
-txt{*
-@{subgoals[display,indent=0,margin=65]}
-*};
+txt {*
+@{subgoals[display,indent=0]}
+To conclude, we tell Isabelle that the desired value is
+@{term "Suc k"}.  With this hint, the subgoal falls to @{text simp}.
+*}
 apply (rule_tac x = "Suc k" in exI, simp)
-done
+(*<*)done(*>*)
 
+text {*
+Combining the previous two results yields our objective, the
+equivalence relating @{term even} and @{text dvd}. 
+%
+%we don't want [iff]: discuss?
+*}
 
-text{*no iff-attribute because we don't always want to use it*}
 theorem even_iff_dvd: "(n \<in> even) = (2 dvd n)"
 by (blast intro: dvd_imp_even even_imp_dvd)
 
-text{*this result ISN'T inductive...*}
-lemma Suc_Suc_even_imp_even: "Suc (Suc n) \<in> even \<Longrightarrow> n \<in> even"
+
+subsection{* Generalization and Rule Induction \label{sec:gen-rule-induction} *}
+
+text {*
+\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:
+*}
+
+lemma "Suc (Suc n) \<in> even \<Longrightarrow> n \<in> even"
 apply (erule even.induct)
-txt{*
-@{subgoals[display,indent=0,margin=65]}
-*};
 oops
-
-text{*...so we need an inductive lemma...*}
+(*<*)
+lemma "Suc (Suc n) \<in> even \<Longrightarrow> n \<in> even"
+apply (erule even.induct)
+(*>*)
+txt {*
+Rule induction finds no occurrences of @{term "Suc(Suc n)"} in the
+conclusion, which it therefore leaves unchanged.  (Look at
+@{text even.induct} to see why this happens.)  We have these subgoals:
+@{subgoals[display,indent=0]}
+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:
+*}
+(*<*)oops(*>*)
 lemma even_imp_even_minus_2: "n \<in> even \<Longrightarrow> n - 2 \<in> even"
 apply (erule even.induct)
-txt{*
-@{subgoals[display,indent=0,margin=65]}
-*};
-apply auto
+ apply auto
 done
+(*<*)
+lemma "n \<in>  even \<Longrightarrow> n - 2 \<in> even"
+apply (erule even.induct)
+(*>*)
+txt {*
+This lemma is trivially inductive.  Here are the subgoals:
+@{subgoals[display,indent=0]}
+The first is trivial because @{text "0 - 2"} simplifies to @{text 0}, which is
+even.  The second is trivial too: @{term "Suc (Suc n) - 2"} simplifies to
+@{term n}, matching the assumption.%
+\index{rule induction|)}  %the sequel isn't really about induction
 
-text{*...and prove it in a separate step*}
+\medskip
+Using our lemma, we can easily prove the result we originally wanted:
+*}
+(*<*)oops(*>*)
 lemma Suc_Suc_even_imp_even: "Suc (Suc n) \<in> even \<Longrightarrow> n \<in> even"
 by (drule even_imp_even_minus_2, simp)
 
+text {*
+We have just proved the converse of the introduction rule @{text even.step}.
+This suggests proving the following equivalence.  We give it the
+\attrdx{iff} attribute because of its obvious value for simplification.
+*}
 
 lemma [iff]: "((Suc (Suc n)) \<in> even) = (n \<in> even)"
 by (blast dest: Suc_Suc_even_imp_even)
 
-end
+
+subsection{* Rule Inversion \label{sec:rule-inversion} *}
+
+text {*
+\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 @{term even} is the minimal set closed under these two rules:
+@{thm [display,indent=0] even.intros [no_vars]}
+Minimality means that @{term even} contains only the elements that these
+rules force it to contain.  If we are told that @{term a}
+belongs to
+@{term even} then there are only two possibilities.  Either @{term a} is @{text 0}
+or else @{term a} has the form @{term "Suc(Suc n)"}, for some suitable @{term n}
+that belongs to
+@{term even}.  That is the gist of the @{term cases} rule, which Isabelle proves
+for us when it accepts an inductive definition:
+@{named_thms [display,indent=0,margin=40] even.cases [no_vars] (even.cases)}
+This general rule is less useful than instances of it for
+specific patterns.  For example, if @{term a} has the form
+@{term "Suc(Suc n)"} then the first case becomes irrelevant, while the second
+case tells us that @{term n} belongs to @{term even}.  Isabelle will generate
+this instance for us:
+*}
+
+inductive_cases Suc_Suc_cases [elim!]: "Suc(Suc n) \<in> even"
+
+text {*
+The \commdx{inductive\protect\_cases} command generates an instance of
+the @{text cases} rule for the supplied pattern and gives it the supplied name:
+@{named_thms [display,indent=0] Suc_Suc_cases [no_vars] (Suc_Suc_cases)}
+Applying this as an elimination rule yields one case where @{text even.cases}
+would yield two.  Rule inversion works well when the conclusions of the
+introduction rules involve datatype constructors like @{term Suc} and @{text "#"}
+(list ``cons''); freeness reasoning discards all but one or two cases.
 
+In the \isacommand{inductive\_cases} command we supplied an
+attribute, @{text "elim!"},
+\index{elim"!@\isa {elim"!} (attribute)}%
+indicating that this elimination rule can be
+applied aggressively.  The original
+@{term cases} rule would loop if used in that manner because the
+pattern~@{term a} matches everything.
+
+The rule @{text Suc_Suc_cases} is equivalent to the following implication:
+@{term [display,indent=0] "Suc (Suc n) \<in> even \<Longrightarrow> n \<in> even"}
+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 @{text even_imp_even_minus_2}. 
+This example also justifies the terminology
+\textbf{rule inversion}: the new rule inverts the introduction rule
+@{text 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:
+*}
+
+(*<*)lemma "Suc(Suc n) \<in> even \<Longrightarrow> P"(*>*)
+apply (ind_cases "Suc(Suc n) \<in> even")
+(*<*)oops(*>*)
+
+text {*
+The specified instance of the @{text cases} rule is generated, then applied
+as an elimination rule.
+
+To summarize, every inductive definition produces a @{text cases} rule.  The
+\commdx{inductive\protect\_cases} command stores an instance of the
+@{text cases} rule for a given pattern.  Within a proof, the
+@{text ind_cases} method applies an instance of the @{text 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|)}
+*}
+
+(*<*)end(*>*)