doc-src/TutorialI/Inductive/Advanced.tex

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