--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/document/Advanced.tex Thu Jul 26 17:16:02 2012 +0200
@@ -0,0 +1,599 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Advanced}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+The premises of introduction rules may contain universal quantifiers and
+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.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Universal Quantifiers in Introduction Rules \label{sec:gterm-datatype}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\index{ground terms example|(}%
+\index{quantifiers!and inductive definitions|(}%
+As a running example, this section develops the theory of \textbf{ground
+terms}: terms constructed from constant and function
+symbols but not variables. To simplify matters further, we regard a
+constant as a function applied to the null argument list. Let us declare a
+datatype \isa{gterm} for the type of ground terms. It is a type constructor
+whose argument is a type of function symbols.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{datatype}\isamarkupfalse%
+\ {\isaliteral{27}{\isacharprime}}f\ gterm\ {\isaliteral{3D}{\isacharequal}}\ Apply\ {\isaliteral{27}{\isacharprime}}f\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}f\ gterm\ list{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+To try it out, we declare a datatype of some integer operations:
+integer constants, the unary minus operator and the addition
+operator.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{datatype}\isamarkupfalse%
+\ integer{\isaliteral{5F}{\isacharunderscore}}op\ {\isaliteral{3D}{\isacharequal}}\ Number\ int\ {\isaliteral{7C}{\isacharbar}}\ UnaryMinus\ {\isaliteral{7C}{\isacharbar}}\ Plus%
+\begin{isamarkuptext}%
+Now the type \isa{integer{\isaliteral{5F}{\isacharunderscore}}op\ gterm} denotes the ground
+terms built over those symbols.
+
+The type constructor \isa{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{{\isaliteral{7B}{\isacharbraceleft}}Number\ {\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ UnaryMinus{\isaliteral{2C}{\isacharcomma}}\ Plus{\isaliteral{7D}{\isacharbraceright}}}.
+
+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.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse%
+\isanewline
+\ \ gterms\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}f\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}f\ gterm\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isakeyword{for}\ F\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}f\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isakeyword{where}\isanewline
+step{\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ args{\isaliteral{2E}{\isachardot}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F{\isaliteral{3B}{\isacharsemicolon}}\ \ f\ {\isaliteral{5C3C696E3E}{\isasymin}}\ F{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}Apply\ f\ args{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+To demonstrate a proof from this definition, let us
+show that the function \isa{gterms}
+is \textbf{monotone}. We shall need this concept shortly.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ gterms{\isaliteral{5F}{\isacharunderscore}}mono{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}F{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}G\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ gterms\ F\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ gterms\ G{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+\ clarify\isanewline
+\isacommand{apply}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}erule\ gterms{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{apply}\isamarkupfalse%
+\ blast\isanewline
+\isacommand{done}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+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{gterms\ F}. (We could have used \isa{intro\ subsetI}.) We then
+apply rule induction. Here is the resulting subgoal:
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\ args\ f{\isaliteral{2E}{\isachardot}}\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}F\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ G{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t{\isaliteral{5C3C696E3E}{\isasymin}}set\ args{\isaliteral{2E}{\isachardot}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F\ {\isaliteral{5C3C616E643E}{\isasymand}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ G{\isaliteral{3B}{\isacharsemicolon}}\ f\ {\isaliteral{5C3C696E3E}{\isasymin}}\ F{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\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.%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\begin{warn}
+Why do we call this function \isa{gterms} instead
+of \isa{gterm}? A constant may have the same name as a type. However,
+name clashes could arise in the theorems that Isabelle generates.
+Our choice of names keeps \isa{gterms{\isaliteral{2E}{\isachardot}}induct} separate from
+\isa{gterm{\isaliteral{2E}{\isachardot}}induct}.
+\end{warn}
+
+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.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse%
+\isanewline
+\ \ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}f\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}f\ gterm\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isakeyword{for}\ arity\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}f\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isakeyword{where}\isanewline
+step{\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ args{\isaliteral{2E}{\isachardot}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ arity{\isaliteral{3B}{\isacharsemicolon}}\ \ \isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ {\isaliteral{3D}{\isacharequal}}\ arity\ f{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}Apply\ f\ args{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ arity{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+The inductive definition neatly captures the reasoning above.
+The universal quantification over the
+\isa{set} of arguments expresses that all of them are well-formed.%
+\index{quantifiers!and inductive definitions|)}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Alternative Definition Using a Monotone Function%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\index{monotone functions!and inductive definitions|(}%
+An inductive definition may refer to the
+inductively defined 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
+function, from the Isabelle theory of lists, is analogous to the
+function \isa{gterms} declared above: if \isa{A} is a set then
+\isa{lists\ A} is the set of lists whose elements belong to
+\isa{A}.
+
+In the inductive definition of well-formed terms, examine the one
+introduction rule. The first premise states that \isa{args} belongs to
+the \isa{lists} of well-formed terms. This formulation is more
+direct, if more obscure, than using a universal quantifier.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse%
+\isanewline
+\ \ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}f\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}f\ gterm\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isakeyword{for}\ arity\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}f\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isakeyword{where}\isanewline
+step{\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lists\ {\isaliteral{28}{\isacharparenleft}}well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ arity{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ {\isaliteral{3D}{\isacharequal}}\ arity\ f{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}Apply\ f\ args{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ arity{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isakeyword{monos}\ lists{\isaliteral{5F}{\isacharunderscore}}mono%
+\begin{isamarkuptext}%
+We cite the theorem \isa{lists{\isaliteral{5F}{\isacharunderscore}}mono} to justify
+using the function \isa{lists}.%
+\footnote{This particular theorem is installed by default already, but we
+include the \isakeyword{monos} declaration in order to illustrate its syntax.}
+\begin{isabelle}%
+A\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ lists\ A\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ lists\ B\rulename{lists{\isaliteral{5F}{\isacharunderscore}}mono}%
+\end{isabelle}
+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
+the rules
+\begin{isabelle}%
+{\isadigit{0}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\isasep\isanewline%
+n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\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{trivlist}
+\item \isa{{\isadigit{0}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even}
+\item \isa{n\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Suc\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even}
+\end{trivlist}
+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\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lists\ {\isaliteral{28}{\isacharparenleft}}well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ arity{\isaliteral{29}{\isacharparenright}}%
+\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 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.%
+\index{monotone functions!and inductive definitions|)}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{A Proof of Equivalence%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+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.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ arity\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ arity{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+\ clarify\isanewline
+\isacommand{apply}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}erule\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{apply}\isamarkupfalse%
+\ auto\isanewline
+\isacommand{done}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+The \isa{clarify} method gives
+us an element of \isa{well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ arity} on which to perform
+induction. The resulting subgoal can be proved automatically:
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\ args\ f{\isaliteral{2E}{\isachardot}}\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t{\isaliteral{5C3C696E3E}{\isasymin}}set\ args{\isaliteral{2E}{\isachardot}}\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ \ \ }t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ arity\ {\isaliteral{5C3C616E643E}{\isasymand}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ arity{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ \ }length\ args\ {\isaliteral{3D}{\isacharequal}}\ arity\ f{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\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:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ arity\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ arity{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+\ clarify\isanewline
+\isacommand{apply}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}erule\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{apply}\isamarkupfalse%
+\ auto\isanewline
+\isacommand{done}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+The proof script is virtually identical,
+but the subgoal after applying induction may be surprising:
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\ args\ f{\isaliteral{2E}{\isachardot}}\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}args\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}}{\isaliteral{5C3C696E3E}{\isasymin}}\ lists\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C696E3E}{\isasymin}}\ \ }{\isaliteral{28}{\isacharparenleft}}well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ arity\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C696E3E}{\isasymin}}\ \ {\isaliteral{28}{\isacharparenleft}}}{\isaliteral{7B}{\isacharbraceleft}}a{\isaliteral{2E}{\isachardot}}\ a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ arity{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ \ }length\ args\ {\isaliteral{3D}{\isacharequal}}\ arity\ f{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ arity%
+\end{isabelle}
+The induction hypothesis contains an application of \isa{lists}. Using a
+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\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ lists\ A\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ lists\ B\rulename{lists{\isaliteral{5F}{\isacharunderscore}}Int{\isaliteral{5F}{\isacharunderscore}}eq}%
+\end{isabelle}
+Thanks to this default simplification rule, the induction hypothesis
+is quickly replaced by its two parts:
+\begin{trivlist}
+\item \isa{args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lists\ {\isaliteral{28}{\isacharparenleft}}well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ arity{\isaliteral{29}{\isacharparenright}}}
+\item \isa{args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lists\ {\isaliteral{28}{\isacharparenleft}}well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ arity{\isaliteral{29}{\isacharparenright}}}
+\end{trivlist}
+Invoking the rule \isa{well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{2E}{\isachardot}}step} completes the proof. The
+call to \isa{auto} does all this work.
+
+This example is typical of how monotone functions
+\index{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\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ f\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ f\ A\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ f\ B\rulename{mono{\isaliteral{5F}{\isacharunderscore}}Int}%
+\end{isabelle}%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isamarkupsubsection{Another Example of Rule Inversion%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\index{rule inversion|(}%
+Does \isa{gterms} distribute over intersection? We have proved that this
+function is monotone, so \isa{mono{\isaliteral{5F}{\isacharunderscore}}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\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ G}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ gterms{\isaliteral{5F}{\isacharunderscore}}IntI{\isaliteral{3A}{\isacharcolon}}\isanewline
+\ \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ G\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ {\isaliteral{28}{\isacharparenleft}}F{\isaliteral{5C3C696E7465723E}{\isasyminter}}G{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+Attempting this proof, we get the assumption
+\isa{Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ G}, which cannot be broken down.
+It looks like a job for rule inversion:\cmmdx{inductive\protect\_cases}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}\isamarkupfalse%
+\ gterm{\isaliteral{5F}{\isacharunderscore}}Apply{\isaliteral{5F}{\isacharunderscore}}elim\ {\isaliteral{5B}{\isacharbrackleft}}elim{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+Here is the result.
+\begin{isabelle}%
+{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\isaindent{\ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t{\isaliteral{5C3C696E3E}{\isasymin}}set\ args{\isaliteral{2E}{\isachardot}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F{\isaliteral{3B}{\isacharsemicolon}}\ f\ {\isaliteral{5C3C696E3E}{\isasymin}}\ F{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
+{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\rulename{gterm{\isaliteral{5F}{\isacharunderscore}}Apply{\isaliteral{5F}{\isacharunderscore}}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{\isaliteral{21}{\isacharbang}}} attribute.
+
+Now we can prove the other half of that distributive law.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ gterms{\isaliteral{5F}{\isacharunderscore}}IntI\ {\isaliteral{5B}{\isacharbrackleft}}rule{\isaliteral{5F}{\isacharunderscore}}format{\isaliteral{2C}{\isacharcomma}}\ intro{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline
+\ \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ G\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ {\isaliteral{28}{\isacharparenleft}}F{\isaliteral{5C3C696E7465723E}{\isasyminter}}G{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}erule\ gterms{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{apply}\isamarkupfalse%
+\ blast\isanewline
+\isacommand{done}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+The proof begins with rule induction over the definition of
+\isa{gterms}, which leaves a single subgoal:
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}args\ f{\isaliteral{2E}{\isachardot}}\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t{\isaliteral{5C3C696E3E}{\isasymin}}set\ args{\isaliteral{2E}{\isachardot}}\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ \ \ }t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ G\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ {\isaliteral{28}{\isacharparenleft}}F\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ G{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ \ }f\ {\isaliteral{5C3C696E3E}{\isasymin}}\ F{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ G\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ }Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ {\isaliteral{28}{\isacharparenleft}}F\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ G{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}
+To prove this, we assume \isa{Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ G}. Rule inversion,
+in the form of \isa{gterm{\isaliteral{5F}{\isacharunderscore}}Apply{\isaliteral{5F}{\isacharunderscore}}elim}, infers
+that every element of \isa{args} belongs to
+\isa{gterms\ G}; hence (by the induction hypothesis) it belongs
+to \isa{gterms\ {\isaliteral{28}{\isacharparenleft}}F\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ G{\isaliteral{29}{\isacharparenright}}}. Rule inversion also yields
+\isa{f\ {\isaliteral{5C3C696E3E}{\isasymin}}\ G} and hence \isa{f\ {\isaliteral{5C3C696E3E}{\isasymin}}\ F\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ G}.
+All of this reasoning is done by \isa{blast}.
+
+\smallskip
+Our distributive law is a trivial consequence of previously-proved results:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isacommand{lemma}\isamarkupfalse%
+\ gterms{\isaliteral{5F}{\isacharunderscore}}Int{\isaliteral{5F}{\isacharunderscore}}eq\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline
+\ \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}gterms\ {\isaliteral{28}{\isacharparenleft}}F\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ G{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ gterms\ F\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ gterms\ G{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}blast\ intro{\isaliteral{21}{\isacharbang}}{\isaliteral{3A}{\isacharcolon}}\ mono{\isaliteral{5F}{\isacharunderscore}}Int\ monoI\ gterms{\isaliteral{5F}{\isacharunderscore}}mono{\isaliteral{29}{\isacharparenright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\index{rule inversion|)}%
+\index{ground terms example|)}
+
+
+\begin{isamarkuptext}
+\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{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse%
+\isanewline
+\ \ well{\isaliteral{5F}{\isacharunderscore}}typed{\isaliteral{5F}{\isacharunderscore}}gterm\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}f\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}t\ list\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{27}{\isacharprime}}t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}f\ gterm\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{27}{\isacharprime}}t{\isaliteral{29}{\isacharparenright}}set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isakeyword{for}\ sig\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}f\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}t\ list\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{27}{\isacharprime}}t{\isaliteral{22}{\isachardoublequoteclose}}%
+\end{isabelle}
+\end{exercise}
+\end{isamarkuptext}
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: