
diff -r 3c82b641b642 -r 094b76968484 doc-src/TutorialI/Inductive/advanced-examples.tex
--- a/doc-src/TutorialI/Inductive/advanced-examples.tex	Wed Feb 21 12:07:00 2001 +0100
+++ b/doc-src/TutorialI/Inductive/advanced-examples.tex	Wed Feb 21 12:57:55 2001 +0100
@@ -1,7 +1,11 @@
 % $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.
+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}
@@ -40,7 +44,7 @@
 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 
+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
@@ -53,7 +57,7 @@
 
 To demonstrate a proof from this definition, let us 
 show that the function \isa{gterms}
-is \textbf{monotonic}.  We shall need this concept shortly.
+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
@@ -85,162 +89,16 @@
 {\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 some suitable \isa{n}
-that belongs to
-\isa{even}.  That is the gist of the \isa{cases} rule, which Isabelle proves
-for us when it accepts an inductive definition:
-\begin{isabelle}
-\isasymlbrakk a\ \isasymin \ even;\isanewline
-\ a\ =\ 0\ \isasymLongrightarrow \ P;\isanewline
-\ \isasymAnd n.\ \isasymlbrakk a\ =\ Suc(Suc\ n);\ n\ \isasymin \
-even\isasymrbrakk \ \isasymLongrightarrow \ P\isasymrbrakk \
-\isasymLongrightarrow \ P
-\rulename{even.cases}
-\end{isabelle}
-
-This general rule is less useful than instances of it for
-specific patterns.  For example, if \isa{a} has the form
-\isa{Suc(Suc~n)} then the first case becomes irrelevant, while the second
-case tells us that \isa{n} belongs to \isa{even}.  Isabelle will generate
-this instance for us:
-\begin{isabelle}
-\isacommand{inductive\_cases}\ Suc_Suc_cases\ [elim!]:
-\ "Suc(Suc\ n)\ \isasymin \ even"
-\end{isabelle}
-The \isacommand{inductive\_cases} command generates an instance of the
-\isa{cases} rule for the supplied pattern and gives it the supplied name:
-%
-\begin{isabelle}
-\isasymlbrakk Suc\ (Suc\ n)\ \isasymin \ even;\ n\ \isasymin \ even\
-\isasymLongrightarrow \ P\isasymrbrakk \ \isasymLongrightarrow \ P%
-\rulename{Suc_Suc_cases}
-\end{isabelle}
-%
-Applying this as an elimination rule yields one case where \isa{even.cases}
-would yield two.  Rule inversion works well when the conclusions of the
-introduction rules involve datatype constructors like \isa{Suc} and \isa{\#}
-(list ``cons''); freeness reasoning discards all but one or two cases.
-
-In the \isacommand{inductive\_cases} command we supplied an
-attribute, \isa{elim!}, indicating that this elimination rule can be applied
-aggressively.  The original
-\isa{cases} rule would loop if used in that manner because the
-pattern~\isa{a} matches everything.
-
-The rule \isa{Suc_Suc_cases} is equivalent to the following implication:
-\begin{isabelle}
-Suc (Suc\ n)\ \isasymin \ even\ \isasymLongrightarrow \ n\ \isasymin \
-even
-\end{isabelle}
-%
-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. 
+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
@@ -252,14 +110,14 @@
 \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
+The universal quantification over the
 \isa{set} of arguments expresses that all of them are well-formed.
 
-\subsection{Alternative Definition Using a Monotonic Function}
+
+\subsection{Alternative Definition Using a monotone Function}
 
 An inductive definition may refer to the inductively defined 
-set through an arbitrary monotonic function.  To demonstrate this
+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
@@ -289,7 +147,7 @@
 \ lists\ B\rulename{lists_mono}
 \end{isabelle}
 %
-Why must the function be monotonic?  An inductive definition describes
+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
@@ -321,7 +179,7 @@
 \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,
+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.
@@ -372,9 +230,9 @@
 \ \ \ \ \ \ \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:
+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}
@@ -390,10 +248,9 @@
 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:
+This example is typical of how 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%
@@ -401,15 +258,76 @@
 \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. 
+\subsection{Another Example of 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}.
+
+Attempting this proof, we get the assumption 
+\isa{Apply\ f\ args\ \isasymin\ gterms\ F}, which cannot be broken down. 
+It looks like a job for rule inversion:
+\begin{isabelle}
+\isacommand{inductive\_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}
+The \isa{intro!}\ attribute of \isa{gterms_IntI} makes it available for
+this proof.
 
 
 \begin{exercise}




