# HG changeset patch
# User berghofe
# Date 1184851890 -7200
# Node ID 7da8f260d9208a48f3c647f47fb5960a57a54cb7
# Parent  4cd60e5d29996d3171b35f718c7046b8624949c6
LaTeX code is now generated directly from theory files.

diff -r 4cd60e5d2999 -r 7da8f260d920 doc-src/TutorialI/Inductive/advanced-examples.tex
--- a/doc-src/TutorialI/Inductive/advanced-examples.tex	Thu Jul 19 15:30:35 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,356 +0,0 @@
-% $Id$
-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}
-
-\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 \isa{gterm} for the type of ground  terms. It is a type constructor
-whose argument is a type of  function symbols. 
-\begin{isabelle}
-\isacommand{datatype}\ 'f\ gterm\ =\ Apply\ 'f\ "'f\ gterm\ list"
-\end{isabelle}
-To try it out, we declare a datatype of some integer operations: 
-integer constants, the unary minus operator and the addition 
-operator. 
-\begin{isabelle}
-\isacommand{datatype}\ integer_op\ =\ Number\ int\ |\ UnaryMinus\ |\ Plus
-\end{isabelle}
-Now the type \isa{integer\_op gterm} denotes the ground 
-terms built over those symbols.
-
-The type constructor \texttt{gterm} can be generalized to a function 
-over sets.  It returns 
-the set of ground terms that can be formed over a set \isa{F} of function symbols. For
-example,  we could consider the set of ground terms formed from the finite 
-set \isa{\isacharbraceleft Number 2, UnaryMinus,
-Plus\isacharbraceright}.
-
-This concept is inductive. If we have a list \isa{args} of ground terms 
-over~\isa{F} and a function symbol \isa{f} in \isa{F}, then we 
-can apply \isa{f} to  \isa{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 \isa{args} belongs
-to our inductively defined set: is a ground term 
-over~\isa{F}.  The function \isa{set} denotes the set of elements in a given 
-list. 
-\begin{isabelle}
-\isacommand{consts}\ gterms\ ::\ "'f\ set\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline
-\isacommand{inductive}\ "gterms\ F"\isanewline
-\isakeyword{intros}\isanewline
-step[intro!]:\ "\isasymlbrakk \isasymforall t\ \isasymin \ set\ args.\ t\ \isasymin \ gterms\ F;\ \ f\ \isasymin \ F\isasymrbrakk \isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ gterms\
-F"
-\end{isabelle}
-
-To demonstrate a proof from this definition, let us 
-show that the function \isa{gterms}
-is \textbf{monotone}.  We shall need this concept shortly.
-\begin{isabelle}
-\isacommand{lemma}\ gterms_mono:\ "F\isasymsubseteq G\ \isasymLongrightarrow \ gterms\ F\ \isasymsubseteq \ gterms\ G"\isanewline
-\isacommand{apply}\ clarify\isanewline
-\isacommand{apply}\ (erule\ gterms.induct)\isanewline
-\isacommand{apply}\ blast\isanewline
-\isacommand{done}
-\end{isabelle}
-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 \isa{clarify} method to assume the existence of an element of
-\isa{gterms~F}.  (We could have used \isa{intro subsetI}.)  We then
-apply rule induction. Here is the resulting subgoal: 
-\begin{isabelle}
-\ 1.\ \isasymAnd x\ args\ f.\isanewline
-\ \ \ \ \ \ \ \isasymlbrakk F\ \isasymsubseteq \ G;\ \isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F\ \isasymand \ t\ \isasymin \ gterms\ G;\ f\ \isasymin \ F\isasymrbrakk \isanewline
-\ \ \ \ \ \ \ \isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ G%
-\end{isabelle}
-%
-The assumptions state that \isa{f} belongs 
-to~\isa{F}, which is included in~\isa{G}, and that every element of the list \isa{args} is
-a ground term over~\isa{G}.  The \isa{blast} method finds this chain of reasoning easily.  
-
-\begin{warn}
-Why do we call this function \isa{gterms} instead 
-of {\isa{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 {\isa{gterms.induct}} separate from 
-{\isa{gterm.induct}}.
-\end{warn}
-
-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 \isa{arity}, specifying the arities
-of all symbols.  In the inductive step, we have a list \isa{args} of such
-terms and a function  symbol~\isa{f}. If the length of the list matches the
-function's arity  then applying \isa{f} to \isa{args} yields a well-formed
-term. 
-\begin{isabelle}
-\isacommand{consts}\ well_formed_gterm\ ::\ "('f\ \isasymRightarrow \ nat)\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline
-\isacommand{inductive}\ "well_formed_gterm\ arity"\isanewline
-\isakeyword{intros}\isanewline
-step[intro!]:\ "\isasymlbrakk \isasymforall t\ \isasymin \ set\ args.\ t\ \isasymin \ well_formed_gterm\ arity;\ \ \isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ =\ arity\ f\isasymrbrakk \isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ well_formed_gterm\
-arity"
-\end{isabelle}
-%
-The inductive definition neatly captures the reasoning above.
-The universal quantification over the
-\isa{set} of arguments expresses that all of them are well-formed.%
-\index{quantifiers!and inductive definitions|)}
-
-
-\subsection{Alternative Definition Using a Monotone Function}
-
-\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 \isa{lists}. This
-function, from the Isabelle theory of lists, is analogous to the
-function \isa{gterms} declared above: if \isa{A} is a set then
-{\isa{lists A}} is the set of lists whose elements belong to
-\isa{A}.  
-
-In the inductive definition of well-formed terms, examine the one
-introduction rule.  The first premise states that \isa{args} belongs to
-the \isa{lists} of well-formed terms.  This formulation is more
-direct, if more obscure, than using a universal quantifier.
-\begin{isabelle}
-\isacommand{consts}\ well_formed_gterm'\ ::\ "('f\ \isasymRightarrow \ nat)\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline
-\isacommand{inductive}\ "well_formed_gterm'\ arity"\isanewline
-\isakeyword{intros}\isanewline
-step[intro!]:\ "\isasymlbrakk args\ \isasymin \ lists\ (well_formed_gterm'\ arity);\ \ \isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ =\ arity\ f\isasymrbrakk \isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ well_formed_gterm'\ arity"\isanewline
-\isakeyword{monos}\ lists_mono
-\end{isabelle}
-
-We cite the theorem \isa{lists_mono} to justify 
-using the function \isa{lists}.%
-\footnote{This particular theorem is installed by default already, but we
-include the \isakeyword{monos} declaration in order to illustrate its syntax.}
-\begin{isabelle}
-A\ \isasymsubseteq\ B\ \isasymLongrightarrow \ lists\ A\ \isasymsubseteq
-\ lists\ B\rulenamedx{lists_mono}
-\end{isabelle}
-%
-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 
-\begin{isabelle}
-0\ \isasymin \ even\isanewline
-n\ \isasymin \ even\ \isasymLongrightarrow \ (Suc\ (Suc\ n))\ \isasymin
-\ even
-\end{isabelle}
-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{isabelle}
-0\ \isasymin \ even\isanewline
-n\ \isasymnotin \ even\ \isasymLongrightarrow \ (Suc\ n)\ \isasymin
-\ even
-\end{isabelle}
-%
-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:
-\begin{isabelle}
-args\ \isasymin \ lists\ (well_formed_gterm'\ arity)
-\end{isabelle}
-To apply the rule we construct a list \isa{args} of previously
-constructed well-formed terms.  We obtain a
-new term, \isa{Apply\ f\ args}.  Because \isa{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}
-
-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. 
-\begin{isabelle}
-\isacommand{lemma}\ "well_formed_gterm\ arity\ \isasymsubseteq \ well_formed_gterm'\ arity"\isanewline
-\isacommand{apply}\ clarify\isanewline
-\isacommand{apply}\ (erule\ well_formed_gterm.induct)\isanewline
-\isacommand{apply}\ auto\isanewline
-\isacommand{done}
-\end{isabelle}
-
-The \isa{clarify} method gives
-us an element of \isa{well_formed_gterm\ arity} on which to perform 
-induction.  The resulting subgoal can be proved automatically:
-\begin{isabelle}
-{\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline
-\ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline
-\ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ well\_formed\_gterm\ arity\ {\isasymand}\ t\ {\isasymin}\ well\_formed\_gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline
-\ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
-\ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well\_formed\_gterm{\isacharprime}\ arity%
-\end{isabelle}
-%
-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:
-\begin{isabelle}
-\isacommand{lemma}\ "well_formed_gterm'\ arity\ \isasymsubseteq \ well_formed_gterm\ arity"\isanewline
-\isacommand{apply}\ clarify\isanewline
-\isacommand{apply}\ (erule\ well_formed_gterm'.induct)\isanewline
-\isacommand{apply}\ auto\isanewline
-\isacommand{done}
-\end{isabelle}
-%
-The proof script is identical, but the subgoal after applying induction may
-be surprising:
-\begin{isabelle}
-1.\ \isasymAnd x\ args\ f.\isanewline
-\ \ \ \ \ \ \isasymlbrakk args\ \isasymin \ lists\ (well_formed_gterm'\ arity\ \isasyminter\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacharbraceleft u.\ u\ \isasymin \ well_formed_gterm\ arity\isacharbraceright );\isanewline
-\ \ \ \ \ \ \ length\ args\ =\ arity\ f\isasymrbrakk \isanewline
-\ \ \ \ \ \ \isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ well_formed_gterm\ arity%
-\end{isabelle}
-The induction hypothesis contains an application of \isa{lists}.  Using a
-monotone function in the inductive definition always has this effect.  The
-subgoal may look uninviting, but fortunately 
-\isa{lists} distributes over intersection:
-\begin{isabelle}
-lists\ (A\ \isasyminter \ B)\ =\ lists\ A\ \isasyminter \ lists\ B
-\rulename{lists_Int_eq}
-\end{isabelle}
-%
-Thanks to this default simplification rule, the induction hypothesis 
-is quickly replaced by its two parts:
-\begin{isabelle}
-\ \ \ \ \ \ \ args\ \isasymin \ lists\ (well_formed_gterm'\ arity)\isanewline
-\ \ \ \ \ \ \ args\ \isasymin \ lists\ (well_formed_gterm\ arity)
-\end{isabelle}
-Invoking the rule \isa{well_formed_gterm.step} completes the proof.  The
-call to
-\isa{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:
-\begin{isabelle}
-mono\ f\ \isasymLongrightarrow \ f\ (A\ \isasyminter \ B)\ \isasymsubseteq \
-f\ A\ \isasyminter \ f\ B%
-\rulename{mono_Int}
-\end{isabelle}
-
-
-\subsection{Another Example of Rule Inversion}
-
-\index{rule inversion|(}%
-Does \isa{gterms} distribute over intersection?  We have proved that this
-function is monotone, so \isa{mono_Int} gives one of the inclusions.  The
-opposite inclusion asserts that if \isa{t} is a ground term over both of the
-sets
-\isa{F} and~\isa{G} then it is also a ground term over their intersection,
-\isa{F\isasyminter G}.
-\begin{isabelle}
-\isacommand{lemma}\ gterms_IntI:\isanewline
-\ \ \ \ \ "t\ \isasymin \ gterms\ F\ \isasymLongrightarrow \ t\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ t\ \isasymin \ gterms\ (F\isasyminter
-G)"
-\end{isabelle}
-Attempting this proof, we get the assumption 
-\isa{Apply\ f\ args\ \isasymin\ gterms\ G}, which cannot be broken down. 
-It looks like a job for rule inversion:
-\begin{isabelle}
-\commdx{inductive\protect\_cases}\ gterm_Apply_elim\ [elim!]:\ "Apply\ f\ args\
-\isasymin\ gterms\ F"
-\end{isabelle}
-%
-Here is the result.
-\begin{isabelle}
-\isasymlbrakk Apply\ f\ args\ \isasymin \ gterms\ F;\isanewline
-\ \isasymlbrakk
-\isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F;\ f\ \isasymin
-\ F\isasymrbrakk \ \isasymLongrightarrow \ P\isasymrbrakk\isanewline
-\isasymLongrightarrow \ P%
-\rulename{gterm_Apply_elim}
-\end{isabelle}
-This rule replaces an assumption about \isa{Apply\ f\ args} by 
-assumptions about \isa{f} and~\isa{args}.  
-No cases are discarded (there was only one to begin
-with) but the rule applies specifically to the pattern \isa{Apply\ f\ args}.
-It can be applied repeatedly as an elimination rule without looping, so we
-have given the
-\isa{elim!}\ attribute. 
-
-Now we can prove the other half of that distributive law.
-\begin{isabelle}
-\isacommand{lemma}\ gterms_IntI\ [rule_format,\ intro!]:\isanewline
-\ \ \ \ \ "t\ \isasymin \ gterms\ F\ \isasymLongrightarrow \ t\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ t\ \isasymin \ gterms\ (F\isasyminter G)"\isanewline
-\isacommand{apply}\ (erule\ gterms.induct)\isanewline
-\isacommand{apply}\ blast\isanewline
-\isacommand{done}
-\end{isabelle}
-%
-The proof begins with rule induction over the definition of
-\isa{gterms}, which leaves a single subgoal:  
-\begin{isabelle}
-1.\ \isasymAnd args\ f.\isanewline
-\ \ \ \ \ \ \isasymlbrakk \isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F\ \isasymand\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (t\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ t\ \isasymin \ gterms\ (F\ \isasyminter \ G));\isanewline
-\ \ \ \ \ \ \ f\ \isasymin \ F\isasymrbrakk \isanewline
-\ \ \ \ \ \ \isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ (F\ \isasyminter \ G)
-\end{isabelle}
-%
-To prove this, we assume \isa{Apply\ f\ args\ \isasymin \
-gterms\ G}.  Rule inversion, in the form of \isa{gterm_Apply_elim}, infers
-that every element of \isa{args} belongs to 
-\isa{gterms~G}; hence (by the induction hypothesis) it belongs
-to \isa{gterms\ (F\ \isasyminter \ G)}.  Rule inversion also yields
-\isa{f\ \isasymin\ G} and hence \isa{f\ \isasymin \ F\ \isasyminter \ G}. 
-All of this reasoning is done by \isa{blast}.
-
-\smallskip
-Our distributive law is a trivial consequence of previously-proved results:
-\begin{isabelle}
-\isacommand{theorem}\ gterms_Int_eq\ [simp]:\isanewline
-\ \ \ \ \ "gterms\ (F\isasyminter G)\ =\ gterms\ F\ \isasyminter \ gterms\ G"\isanewline
-\isacommand{by}\ (blast\ intro!:\ mono_Int\ monoI\ gterms_mono)
-\end{isabelle}
-\index{rule inversion|)}%
-\index{ground terms example|)}
-
-
-\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}
-\isacommand{consts}\ well_typed_gterm::\ "('f\ \isasymRightarrow \ 't\ list\ *\ 't)\ \isasymRightarrow \ ('f\ gterm\ *\ 't)set"\isanewline
-\isacommand{inductive}\ "well_typed_gterm\ sig"\isanewline
-\end{isabelle}
-\end{exercise}
diff -r 4cd60e5d2999 -r 7da8f260d920 doc-src/TutorialI/Inductive/even-example.tex
--- a/doc-src/TutorialI/Inductive/even-example.tex	Thu Jul 19 15:30:35 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,324 +0,0 @@
-% $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 \commdx{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,
-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:
-%
-\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!},%
-\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}
-
-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_tac\ 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 is applied automatically.
-\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}
-
-\index{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 \(\cdot\))}.  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, 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}
-
-\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:
-%
-\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 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:
-\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.%
-\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
-\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}
-
-\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
-\ 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 \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%
-\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!},
-\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}
-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}.  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:
-\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
-\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.%
-\index{rule inversion|)}%
-\index{even numbers!defining inductively|)}