--- /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}