--- a/doc-src/TutorialI/Inductive/Advanced.tex Fri Jan 12 16:07:20 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,431 +0,0 @@
-
-This section describes advanced features of inductive definitions.
-The premises of introduction rules may contain universal quantifiers and
-monotonic functions. Theorems may be proved by rule inversion.
-
-\subsection{Universal quantifiers in introduction rules}
-\label{sec:gterm-datatype}
-
-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{\{Number 2, UnaryMinus, Plus\}}}.
-
-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{monotonic}. We shall need this concept shortly.
-\begin{isabelle}
-\isacommand{lemma}\ "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{terms~F}. (We could have used \isa{intro subsetI}.) We then
-apply rule induction. Here is the resulting subgoal:
-\begin{isabelle}
-1.\ \isasymAnd x\ f\ args.\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.
-
-\textit{Remark}: why do we call this function \isa{gterms} instead
-of {\isa{gterm}}? Isabelle maintains separate name spaces for types
-and constants, so there is no danger of confusion. However, name
-clashes could arise in the theorems that Isabelle generates.
-Our choice of names keeps {\isa{gterms.induct}} separate from {\isa{gterm.induct}}.
-
-\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.
-
-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 an arbitrary \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}
-%
-In \S\ref{sec:gen-rule-induction} we devoted some effort to proving precisely
-this result. Yet we could have obtained it by a one-line declaration.
-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, applied, and
-discarded.
-
-\medskip
-Let us try rule inversion on our ground terms example:
-\begin{isabelle}
-\isacommand{inductive\_cases}\ gterm_Apply_elim\ [elim!]:\ "Apply\ f\ args\
-\isasymin\ gterms\ F"
-\end{isabelle}
-%
-Here is the result. 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.
-\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}. Here is a proof in which this
-inference is essential. We show 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\ [rule_format]:\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}
-%
-The induction hypothesis states that every element of \isa{args} belongs to
-\isa{gterms\ (F\ \isasyminter \ G)} --- provided it already belongs to
-\isa{gterms\ G}. How do we meet that condition?
-
-By assuming (as we may) the formula \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}. It also yields \isa{f\ \isasymin \ G}, which will allow us
-to conclude \isa{f\ \isasymin \ F\ \isasyminter \ G}. All of this reasoning
-is done by \isa{blast}.
-
-\medskip
-
-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.
-
-
-\subsection{Continuing the `ground terms' example}
-
-Call a term \textbf{well-formed} if each symbol occurring in it has
-the correct number of arguments. To formalize this concept, we
-introduce a function mapping each symbol to its arity, a natural
-number.
-
-Let us define the set of well-formed ground terms.
-Suppose we are given a function called \isa{arity}, specifying the arities to be used.
-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.
-It is just an elaboration of the previous one, consisting of a single
-introduction rule. The universal quantification over the
-\isa{set} of arguments expresses that all of them are well-formed.
-
-\subsection{Alternative definition using a monotonic function}
-
-An inductive definition may refer to the inductively defined
-set through an arbitrary monotonic 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 library, 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 must cite the theorem \isa{lists_mono} in order to justify
-using the function \isa{lists}.
-\begin{isabelle}
-A\ \isasymsubseteq\ B\ \isasymLongrightarrow \ lists\ A\ \isasymsubseteq
-\ lists\ B\rulename{lists_mono}
-\end{isabelle}
-%
-Why must the function be monotonic? 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 monotonic,
-applications of the rule remain valid as new terms are constructed.
-Further lists of well-formed
-terms become available and none are taken away.
-
-
-\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{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymand}\ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline
-\ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
-\ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}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
-monotonic function in the inductive definition always has this effect. The
-subgoal may look uninviting, but fortunately a useful rewrite rule concerning
-\isa{lists} is available:
-\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 monotonic functions can be used. In
-particular, a rewrite rule analogous to \isa{lists_Int_eq} holds in most
-cases. 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}
-
-
-To summarize: a universal quantifier in an introduction rule
-lets it refer to any number of instances of
-the inductively defined set. A monotonic function in an introduction
-rule lets it refer to constructions over the inductively defined
-set. Each element of an inductively defined set is created
-through finitely many applications of the introduction rules. So each rule
-must be positive, and never can it refer to \textit{infinitely} many
-previous instances of the inductively defined set.
-
-
-
-\begin{exercise}
-Prove this theorem, one direction of which was proved in
-\S\ref{sec:rule-inversion} above.
-\begin{isabelle}
-\isacommand{lemma}\ gterms_Int_eq\ [simp]:\ "gterms\ (F\isasyminter G)\ =\
-gterms\ F\ \isasyminter \ gterms\ G"\isanewline
-\end{isabelle}
-\end{exercise}
-
-
-\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}
--- a/doc-src/TutorialI/Inductive/Even.tex Fri Jan 12 16:07:20 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,223 +0,0 @@
-\section{The set of even numbers}
-
-The set of even numbers can be inductively defined as the least set
-containing 0 and closed under the operation ${\cdots}+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
-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. 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!}, 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\ "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 will be used.
-\begin{isabelle}
-\isacommand{lemma}\ dvd_imp_even:\ "\#2\ dvd\ n\ \isasymLongrightarrow \ n\ \isasymin \ even"\isanewline
-\isacommand{apply}\ (auto\ simp\ add:\ dvd_def)\isanewline
-\isacommand{done}
-\end{isabelle}
-
-\subsection{Rule induction}
-\label{sec: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\(\cdots\))}. 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"\isanewline
-\isacommand{apply}\ (erule\ even.induct)\isanewline
-\ \isacommand{apply}\ simp\isanewline
-\isacommand{apply}\ (simp\ add:\ dvd_def)\isanewline
-\isacommand{apply}\ clarify\isanewline
-\isacommand{apply}\ (rule_tac\ x\ =\ "Suc\ k"\ \isakeyword{in}\ exI)\isanewline
-\isacommand{apply}\ simp\isanewline
-\isacommand{done}
-\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}
-\ 1.\ \#2\ dvd\ 0\isanewline
-\ 2.\ \isasymAnd n.\ \isasymlbrakk n\ \isasymin \ even;\ \#2\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ \#2\ dvd\ Suc\ (Suc\ n)
-\end{isabelle}
-%
-The first subgoal is trivial (by \isa{simp}). For the second
-subgoal, we unfold the definition of \isa{dvd}:
-\begin{isabelle}
-\ 1.\ \isasymAnd n.\ \isasymlbrakk n\ \isasymin \ even;\ \isasymexists k.\
-n\ =\ \#2\ *\ k\isasymrbrakk \ \isasymLongrightarrow \ \isasymexists k.\
-Suc\ (Suc\ n)\ =\ \#2\ *\ k
-\end{isabelle}
-%
-Then we use
-\isa{clarify} to eliminate the existential quantifier from the assumption
-and replace \isa{n} by \isa{\#2\ *\ k}.
-\begin{isabelle}
-\ 1.\ \isasymAnd n\ k.\ \#2\ *\ k\ \isasymin \ even\ \isasymLongrightarrow \ \isasymexists ka.\ Suc\ (Suc\ (\#2\ *\ k))\ =\ \#2\ *\ ka%
-\end{isabelle}
-%
-The \isa{rule_tac\ldots exI} tells Isabelle that the desired
-\isa{ka} is
-\isa{Suc\ k}. With this hint, the subgoal becomes trivial, and \isa{simp}
-concludes the proof.
-
-\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{apply}\ (blast\ intro:\ dvd_imp_even\ even_imp_dvd)\isanewline
-\isacommand{done}
-\end{isabelle}
-
-\subsection{Generalization and rule induction}
-\label{sec:gen-rule-induction}
-
-Everybody knows that when before applying induction we often must generalize
-the induction formula. This step is just as important with rule induction,
-and the required generalizations can be complicated. In this
-example, the obvious statement of the result is not inductive:
-%
-\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 get 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. In general, rule inductions involving
-non-trivial terms will probably go wrong. 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.
-
-\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{apply}\ (drule\ even_imp_even_minus_2)\isanewline
-\isacommand{apply}\ simp\isanewline
-\isacommand{done}
-\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.
-\begin{isabelle}
-\isacommand{lemma}\ [iff]:\ "((Suc\ (Suc\ n))\ \isasymin \ even)\ =\ (n\
-\isasymin \ even)"\isanewline
-\isacommand{apply}\ (blast\ dest:\ Suc_Suc_even_imp_even)\isanewline
-\isacommand{done}
-\end{isabelle}
-
-The even numbers example has shown how inductive definitions can be used.
-Later examples will show that they are actually worth using.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Inductive/advanced-examples.tex Fri Jan 12 16:09:33 2001 +0100
@@ -0,0 +1,434 @@
+% $Id$
+This section describes advanced features of inductive definitions.
+The premises of introduction rules may contain universal quantifiers and
+monotonic functions. Theorems may be proved by rule inversion.
+
+\subsection{Universal Quantifiers in Introduction Rules}
+\label{sec:gterm-datatype}
+
+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{\{Number 2, UnaryMinus, Plus\}}}.
+
+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{monotonic}. 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{terms~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}
+
+
+\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.
+
+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 an arbitrary \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}
+%
+In {\S}\ref{sec:gen-rule-induction} we devoted some effort to proving precisely
+this result. Yet we could have obtained it by a one-line declaration.
+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, applied, and
+discarded.
+
+\medskip
+Let us try rule inversion on our ground terms example:
+\begin{isabelle}
+\isacommand{inductive\_cases}\ gterm_Apply_elim\ [elim!]:\ "Apply\ f\ args\
+\isasymin\ gterms\ F"
+\end{isabelle}
+%
+Here is the result. 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.
+\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}. Here is a proof in which this
+inference is essential. We show 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\ [rule_format]:\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}
+%
+The induction hypothesis states that every element of \isa{args} belongs to
+\isa{gterms\ (F\ \isasyminter \ G)} --- provided it already belongs to
+\isa{gterms\ G}. How do we meet that condition?
+
+By assuming (as we may) the formula \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}. It also yields \isa{f\ \isasymin \ G}, which will allow us
+to conclude \isa{f\ \isasymin \ F\ \isasyminter \ G}. All of this reasoning
+is done by \isa{blast}.
+
+\medskip
+
+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.
+
+
+\subsection{Continuing the Ground Terms Example}
+
+Call a term \textbf{well-formed} if each symbol occurring in it has
+the correct number of arguments. To formalize this concept, we
+introduce a function mapping each symbol to its \textbf{arity}, a natural
+number.
+
+Let us define the set of well-formed ground terms.
+Suppose we are given a function called \isa{arity}, specifying the arities to be used.
+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.
+It is just an elaboration of the previous one, consisting of a single
+introduction rule. The universal quantification over the
+\isa{set} of arguments expresses that all of them are well-formed.
+
+\subsection{Alternative Definition Using a Monotonic Function}
+
+An inductive definition may refer to the inductively defined
+set through an arbitrary monotonic 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 must cite the theorem \isa{lists_mono} in order to justify
+using the function \isa{lists}.
+\begin{isabelle}
+A\ \isasymsubseteq\ B\ \isasymLongrightarrow \ lists\ A\ \isasymsubseteq
+\ lists\ B\rulename{lists_mono}
+\end{isabelle}
+%
+Why must the function be monotonic? 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 monotonic,
+applications of the rule remain valid as new terms are constructed.
+Further lists of well-formed
+terms become available and none are taken away.
+
+
+\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{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymand}\ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline
+\ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
+\ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}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
+monotonic function in the inductive definition always has this effect. The
+subgoal may look uninviting, but fortunately a useful rewrite rule concerning
+\isa{lists} is available:
+\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 monotonic functions can be used. In
+particular, a rewrite rule analogous to \isa{lists_Int_eq} holds in most
+cases. 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}
+
+
+To summarize: a universal quantifier in an introduction rule
+lets it refer to any number of instances of
+the inductively defined set. A monotonic function in an introduction
+rule lets it refer to constructions over the inductively defined
+set. Each element of an inductively defined set is created
+through finitely many applications of the introduction rules. So each rule
+must be positive, and never can it refer to \textit{infinitely} many
+previous instances of the inductively defined set.
+
+
+
+\begin{exercise}
+Prove this theorem, one direction of which was proved in
+{\S}\ref{sec:rule-inversion} above.
+\begin{isabelle}
+\isacommand{lemma}\ gterms_Int_eq\ [simp]:\ "gterms\ (F\isasyminter G)\ =\
+gterms\ F\ \isasyminter \ gterms\ G"\isanewline
+\end{isabelle}
+\end{exercise}
+
+
+\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}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Inductive/even-example.tex Fri Jan 12 16:09:33 2001 +0100
@@ -0,0 +1,222 @@
+% $Id$
+\section{The Set of Even Numbers}
+
+The set of even numbers can be inductively defined as the least set
+containing 0 and closed under the operation ${\cdots}+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
+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. 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!}, 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\ "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 will be used.
+\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}
+
+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\(\cdots\))}. 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,
+\isacommand{apply}\ 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}
+
+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, the obvious statement of the result is not
+inductive:
+%
+\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 inductions involving
+non-trivial terms usually fail. 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.
+
+\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, \isacommand{apply}\ 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.
+\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}
+
+The even numbers example has shown how inductive definitions can be used.
+Later examples will show that they are actually worth using.