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