# HG changeset patch
# User paulson
# Date 974217756 -3600
# Node ID 87dda999decad1a2a2c4623ec760935e892d1853
# Parent  e6e7205e9e91ac4b2e51782737f3d1e03f2ddc51
first version of Advanced Inductive Defs section

diff -r e6e7205e9e91 -r 87dda999deca doc-src/TutorialI/Inductive/Advanced.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Inductive/Advanced.tex	Tue Nov 14 17:02:36 2000 +0100
@@ -0,0 +1,431 @@
+
+The next examples illustrate 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}
+
+A \textbf{ground} term is a term constructed from constant and function 
+symbols alone: no 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}
diff -r e6e7205e9e91 -r 87dda999deca doc-src/TutorialI/Inductive/Advanced.thy
--- a/doc-src/TutorialI/Inductive/Advanced.thy	Tue Nov 14 13:26:48 2000 +0100
+++ b/doc-src/TutorialI/Inductive/Advanced.thy	Tue Nov 14 17:02:36 2000 +0100
@@ -1,67 +1,222 @@
 (* ID:         $Id$ *)
 theory Advanced = Even:
 
-text{* We completely forgot about "rule inversion", or whatever we may want
-to call it. Just as a demo I include the two forms that Markus has made available. First the one for binding the result to a name *}
+
+datatype 'f gterm = Apply 'f "'f gterm list"
+
+datatype integer_op = Number int | UnaryMinus | Plus;
+
+consts gterms :: "'f set \<Rightarrow> 'f gterm set"
+inductive "gterms F"
+intros
+step[intro!]: "\<lbrakk>\<forall>t \<in> set args. t \<in> gterms F;  f \<in> F\<rbrakk>
+               \<Longrightarrow> (Apply f args) \<in> gterms F"
+
+lemma gterms_mono: "F\<subseteq>G \<Longrightarrow> gterms F \<subseteq> gterms G"
+apply clarify
+apply (erule gterms.induct)
+apply blast
+done
+
+text{*
+The situation after induction
 
-inductive_cases even_cases [elim!]:
+proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{2}}\isanewline
+\isanewline
+goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline
+F\ {\isasymsubseteq}\ G\ {\isasymLongrightarrow}\ gterms\ F\ {\isasymsubseteq}\ gterms\ G\isanewline
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline
+\ \ \ \ \ \ \ {\isasymlbrakk}F\ {\isasymsubseteq}\ G{\isacharsemicolon}\ {\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F\ {\isasymand}\ t\ {\isasymin}\ gterms\ G{\isacharsemicolon}\ f\ {\isasymin}\ F{\isasymrbrakk}\isanewline
+\ \ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G
+*}
+
+text{* We completely forgot about "rule inversion". 
+
+@{thm[display] even.cases[no_vars]}
+\rulename{even.cases}
+
+Just as a demo I include
+the two forms that Markus has made available. First the one for binding the
+result to a name 
+
+*}
+
+inductive_cases Suc_Suc_cases [elim!]:
   "Suc(Suc n) \<in> even"
 
-thm even_cases;
+thm Suc_Suc_cases;
+
+text{*
+@{thm[display] Suc_Suc_cases[no_vars]}
+\rulename{Suc_Suc_cases}
+
+and now the one for local usage:
+*}
+
+lemma "Suc(Suc n) \<in> even \<Longrightarrow> P n";
+apply (ind_cases "Suc(Suc n) \<in> even");
+oops
+
+inductive_cases gterm_Apply_elim [elim!]: "Apply f args \<in> gterms F"
+
+text{*this is what we get:
+
+@{thm[display] gterm_Apply_elim[no_vars]}
+\rulename{gterm_Apply_elim}
+*}
 
-text{*and now the one for local usage:*}
+lemma gterms_IntI [rule_format]:
+     "t \<in> gterms F \<Longrightarrow> t \<in> gterms G \<longrightarrow> t \<in> gterms (F\<inter>G)"
+apply (erule gterms.induct)
+apply blast
+done
+
+
+text{*
+Subgoal after induction.  How would we cope without rule inversion?
+
+pr(latex xsymbols symbols)
+
+proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline
+\isanewline
+goal\ {\isacharparenleft}lemma\ gterms{\isacharunderscore}IntI{\isacharparenright}{\isacharcolon}\isanewline
+t\ {\isasymin}\ gterms\ F\ {\isasymLongrightarrow}\ t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}\isanewline
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}args\ f{\isachardot}\isanewline
+\ \ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F\ {\isasymand}\ {\isacharparenleft}t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ \ \ \ \ \ \ \ \ f\ {\isasymin}\ F{\isasymrbrakk}\isanewline
+\ \ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}
+
+
+*}
+
+text{*
+@{thm[display] mono_Int[no_vars]}
+\rulename{mono_Int}
+*}
 
-lemma "Suc(Suc n) \<in> even \<Longrightarrow> n \<in> even";
-by(ind_cases "Suc(Suc n) \<in> even");
+lemma gterms_Int_eq [simp]:
+     "gterms (F\<inter>G) = gterms F \<inter> gterms G"
+apply (rule equalityI)
+apply (blast intro!: mono_Int monoI gterms_mono)
+apply (blast intro!: gterms_IntI)
+done
+
+
+consts integer_arity :: "integer_op \<Rightarrow> nat"
+primrec
+"integer_arity (Number n)        = #0"
+"integer_arity UnaryMinus        = #1"
+"integer_arity Plus              = #2"
+
+consts well_formed_gterm :: "('f \<Rightarrow> nat) \<Rightarrow> 'f gterm set"
+inductive "well_formed_gterm arity"
+intros
+step[intro!]: "\<lbrakk>\<forall>t \<in> set args. t \<in> well_formed_gterm arity;  
+                length args = arity f\<rbrakk>
+               \<Longrightarrow> (Apply f args) \<in> well_formed_gterm arity"
+
 
-text{*Both forms accept lists of strings.
+consts well_formed_gterm' :: "('f \<Rightarrow> nat) \<Rightarrow> 'f gterm set"
+inductive "well_formed_gterm' arity"
+intros
+step[intro!]: "\<lbrakk>args \<in> lists (well_formed_gterm' arity);  
+                length args = arity f\<rbrakk>
+               \<Longrightarrow> (Apply f args) \<in> well_formed_gterm' arity"
+monos lists_mono
+
+lemma "well_formed_gterm arity \<subseteq> well_formed_gterm' arity"
+apply clarify
+apply (erule well_formed_gterm.induct)
+apply auto
+done
+
 
-Hope you can find some more exciting examples, although these may do
+text{*
+The situation after clarify (note the induction hypothesis!)
+
+pr(latex xsymbols symbols)
+
+proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{2}}\isanewline
+\isanewline
+goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline
+well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\isanewline
+\ {\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
 *}
 
 
-datatype 'f "term" = Apply 'f "'f term list"
-
-consts terms :: "'f set \<Rightarrow> 'f term set"
-inductive "terms F"
-intros
-step[intro]: "\<lbrakk>\<forall>t \<in> set term_list. t \<in> terms F;  f \<in> F\<rbrakk>
-              \<Longrightarrow> (Apply f term_list) \<in> terms F"
+lemma "well_formed_gterm' arity \<subseteq> well_formed_gterm arity"
+apply clarify
+apply (erule well_formed_gterm'.induct)
+apply auto
+done
 
 
-lemma "F\<subseteq>G \<Longrightarrow> terms F \<subseteq> terms G"
-apply clarify
-apply (erule terms.induct)
-apply blast
-done
+text{*
+@{thm[display] lists_Int_eq[no_vars]}
+\rulename{lists_Int_eq}
+
+The situation after clarify (note the strange induction hypothesis!)
+
+pr(latex xsymbols symbols)
 
-consts term_type :: "('f \<Rightarrow> 't list * 't) \<Rightarrow> ('f term * 't)set"
-inductive "term_type sig"
+proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{2}}\isanewline
+\isanewline
+goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline
+well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\isanewline
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline
+\ \ \ \ \ \ \ {\isasymlbrakk}args\isanewline
+\ \ \ \ \ \ \ \ {\isasymin}\ lists\isanewline
+\ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasyminter}\ {\isacharbraceleft}u{\isachardot}\ u\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharbraceright}{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ \ \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
+\ \ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity
+*}
+
+text{* the rest isn't used: too complicated.  OK for an exercise though.*}
+
+consts integer_signature :: "(integer_op * (unit list * unit)) set"
+inductive "integer_signature"
 intros
-step[intro]: "\<lbrakk>\<forall>et \<in> set term_type_list. et \<in> term_type sig; 
-               sig f = (map snd term_type_list, rtype)\<rbrakk>
-              \<Longrightarrow> (Apply f (map fst term_type_list), rtype) \<in> term_type sig"
+Number:     "(Number n,   ([], ())) \<in> integer_signature"
+UnaryMinus: "(UnaryMinus, ([()], ())) \<in> integer_signature"
+Plus:       "(Plus,       ([(),()], ())) \<in> integer_signature"
+
 
-consts term_type' :: "('f \<Rightarrow> 't list * 't) \<Rightarrow> ('f term * 't)set"
-inductive "term_type' sig"
+consts well_typed_gterm :: "('f \<Rightarrow> 't list * 't) \<Rightarrow> ('f gterm * 't)set"
+inductive "well_typed_gterm sig"
 intros
-step[intro]: "\<lbrakk>term_type_list \<in> lists(term_type' sig); 
-                 sig f = (map snd term_type_list, rtype)\<rbrakk>
-              \<Longrightarrow> (Apply f (map fst term_type_list), rtype) \<in> term_type' sig"
+step[intro!]: 
+    "\<lbrakk>\<forall>pair \<in> set args. pair \<in> well_typed_gterm sig; 
+      sig f = (map snd args, rtype)\<rbrakk>
+     \<Longrightarrow> (Apply f (map fst args), rtype) 
+         \<in> well_typed_gterm sig"
+
+consts well_typed_gterm' :: "('f \<Rightarrow> 't list * 't) \<Rightarrow> ('f gterm * 't)set"
+inductive "well_typed_gterm' sig"
+intros
+step[intro!]: 
+    "\<lbrakk>args \<in> lists(well_typed_gterm' sig); 
+      sig f = (map snd args, rtype)\<rbrakk>
+     \<Longrightarrow> (Apply f (map fst args), rtype) 
+         \<in> well_typed_gterm' sig"
 monos lists_mono
 
 
-lemma "term_type sig \<subseteq> term_type' sig"
+lemma "well_typed_gterm sig \<subseteq> well_typed_gterm' sig"
 apply clarify
-apply (erule term_type.induct)
+apply (erule well_typed_gterm.induct)
 apply auto
 done
 
-lemma "term_type' sig \<subseteq> term_type sig"
+lemma "well_typed_gterm' sig \<subseteq> well_typed_gterm sig"
 apply clarify
-apply (erule term_type'.induct)
+apply (erule well_typed_gterm'.induct)
 apply auto
 done
 
+
 end
 
diff -r e6e7205e9e91 -r 87dda999deca doc-src/TutorialI/Inductive/inductive.tex
--- a/doc-src/TutorialI/Inductive/inductive.tex	Tue Nov 14 13:26:48 2000 +0100
+++ b/doc-src/TutorialI/Inductive/inductive.tex	Tue Nov 14 17:02:36 2000 +0100
@@ -18,7 +18,7 @@
 \input{Inductive/document/AB}
 
 \section{Advanced inductive definitions}
-\input{Inductive/document/Advanced}
+\input{Inductive/Advanced}
 
 \index{inductive definition|)}
 \index{*inductive|)}