doc-src/TutorialI/Inductive/Advanced.tex
author nipkow
Wed Dec 06 13:22:58 2000 +0100 (2000-12-06)
changeset 10608 620647438780
parent 10475 77fafa07fc8f
permissions -rw-r--r--
*** empty log message ***
     1 
     2 This section describes advanced features of inductive definitions. 
     3 The premises of introduction rules may contain universal quantifiers and
     4 monotonic functions.  Theorems may be proved by rule inversion.
     5 
     6 \subsection{Universal quantifiers in introduction rules}
     7 \label{sec:gterm-datatype}
     8 
     9 As a running example, this section develops the theory of \textbf{ground
    10 terms}: terms constructed from constant and function 
    11 symbols but not variables. To simplify matters further, we regard a
    12 constant as a function applied to the null argument  list.  Let us declare a
    13 datatype \isa{gterm} for the type of ground  terms. It is a type constructor
    14 whose argument is a type of  function symbols. 
    15 \begin{isabelle}
    16 \isacommand{datatype}\ 'f\ gterm\ =\ Apply\ 'f\ "'f\ gterm\ list"
    17 \end{isabelle}
    18 To try it out, we declare a datatype of some integer operations: 
    19 integer constants, the unary minus operator and the addition 
    20 operator. 
    21 \begin{isabelle}
    22 \isacommand{datatype}\ integer_op\ =\ Number\ int\ |\ UnaryMinus\ |\ Plus
    23 \end{isabelle}
    24 Now the type \isa{integer\_op gterm} denotes the ground 
    25 terms built over those symbols.
    26 
    27 The type constructor \texttt{gterm} can be generalized to a function 
    28 over sets.  It returns 
    29 the set of ground terms that can be formed over a set \isa{F} of function symbols. For
    30 example,  we could consider the set of ground terms formed from the finite 
    31 set {\isa{\{Number 2, UnaryMinus, Plus\}}}.
    32 
    33 This concept is inductive. If we have a list \isa{args} of ground terms 
    34 over~\isa{F} and a function symbol \isa{f} in \isa{F}, then we 
    35 can apply \isa{f} to  \isa{args} to obtain another ground term. 
    36 The only difficulty is that the argument list may be of any length. Hitherto, 
    37 each rule in an inductive definition referred to the inductively 
    38 defined set a fixed number of times, typically once or twice. 
    39 A universal quantifier in the premise of the introduction rule 
    40 expresses that every element of \isa{args} belongs
    41 to our inductively defined set: is a ground term 
    42 over~\isa{F}.  The function {\isa{set}} denotes the set of elements in a given 
    43 list. 
    44 \begin{isabelle}
    45 \isacommand{consts}\ gterms\ ::\ "'f\ set\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline
    46 \isacommand{inductive}\ "gterms\ F"\isanewline
    47 \isakeyword{intros}\isanewline
    48 step[intro!]:\ "\isasymlbrakk \isasymforall t\ \isasymin \ set\ args.\ t\ \isasymin \ gterms\ F;\ \ f\ \isasymin \ F\isasymrbrakk \isanewline
    49 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ gterms\
    50 F"
    51 \end{isabelle}
    52 
    53 To demonstrate a proof from this definition, let us 
    54 show that the function \isa{gterms}
    55 is \textbf{monotonic}.  We shall need this concept shortly.
    56 \begin{isabelle}
    57 \isacommand{lemma}\ "F\isasymsubseteq G\ \isasymLongrightarrow \ gterms\ F\ \isasymsubseteq \ gterms\ G"\isanewline
    58 \isacommand{apply}\ clarify\isanewline
    59 \isacommand{apply}\ (erule\ gterms.induct)\isanewline
    60 \isacommand{apply}\ blast\isanewline
    61 \isacommand{done}
    62 \end{isabelle}
    63 Intuitively, this theorem says that
    64 enlarging the set of function symbols enlarges the set of ground 
    65 terms. The proof is a trivial rule induction.
    66 First we use the \isa{clarify} method to assume the existence of an element of
    67 \isa{terms~F}.  (We could have used \isa{intro subsetI}.)  We then
    68 apply rule induction. Here is the resulting subgoal: 
    69 \begin{isabelle}
    70 1.\ \isasymAnd x\ f\ args.\isanewline
    71 \ \ \ \ \ \ \isasymlbrakk F\ \isasymsubseteq \ G;\ \isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F\ \isasymand \ t\ \isasymin \ gterms\ G;\ f\ \isasymin \ F\isasymrbrakk \isanewline
    72 \ \ \ \ \ \ \isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ G%
    73 \end{isabelle}
    74 %
    75 The assumptions state that \isa{f} belongs 
    76 to~\isa{F}, which is included in~\isa{G}, and that every element of the list \isa{args} is
    77 a ground term over~\isa{G}.  The \isa{blast} method finds this chain of reasoning easily.  
    78 
    79 \textit{Remark}: why do we call this function \isa{gterms} instead 
    80 of {\isa{gterm}}? Isabelle maintains separate name spaces for types 
    81 and constants, so there is no danger of confusion. However, name 
    82 clashes could arise in the theorems that Isabelle generates. 
    83 Our choice of names keeps {\isa{gterms.induct}} separate from {\isa{gterm.induct}}.
    84 
    85 \subsection{Rule inversion}\label{sec:rule-inversion}
    86 
    87 Case analysis on an inductive definition is called \textbf{rule inversion}. 
    88 It is frequently used in proofs about operational semantics.  It can be
    89 highly effective when it is applied automatically.  Let us look at how rule
    90 inversion is done in Isabelle.
    91 
    92 Recall that \isa{even} is the minimal set closed under these two rules:
    93 \begin{isabelle}
    94 0\ \isasymin \ even\isanewline
    95 n\ \isasymin \ even\ \isasymLongrightarrow \ (Suc\ (Suc\ n))\ \isasymin
    96 \ even
    97 \end{isabelle}
    98 Minimality means that \isa{even} contains only the elements that these
    99 rules force it to contain.  If we are told that \isa{a}
   100 belongs to
   101 \isa{even} then there are only two possibilities.  Either \isa{a} is \isa{0}
   102 or else \isa{a} has the form \isa{Suc(Suc~n)}, for an arbitrary \isa{n}
   103 that belongs to
   104 \isa{even}.  That is the gist of the \isa{cases} rule, which Isabelle proves
   105 for us when it accepts an inductive definition:
   106 \begin{isabelle}
   107 \isasymlbrakk a\ \isasymin \ even;\isanewline
   108 \ a\ =\ 0\ \isasymLongrightarrow \ P;\isanewline
   109 \ \isasymAnd n.\ \isasymlbrakk a\ =\ Suc(Suc\ n);\ n\ \isasymin \
   110 even\isasymrbrakk \ \isasymLongrightarrow \ P\isasymrbrakk \
   111 \isasymLongrightarrow \ P
   112 \rulename{even.cases}
   113 \end{isabelle}
   114 
   115 This general rule is less useful than instances of it for
   116 specific patterns.  For example, if \isa{a} has the form
   117 \isa{Suc(Suc~n)} then the first case becomes irrelevant, while the second
   118 case tells us that \isa{n} belongs to \isa{even}.  Isabelle will generate
   119 this instance for us:
   120 \begin{isabelle}
   121 \isacommand{inductive\_cases}\ Suc_Suc_cases\ [elim!]:
   122 \ "Suc(Suc\ n)\ \isasymin \ even"
   123 \end{isabelle}
   124 The \isacommand{inductive\_cases} command generates an instance of the
   125 \isa{cases} rule for the supplied pattern and gives it the supplied name:
   126 %
   127 \begin{isabelle}
   128 \isasymlbrakk Suc\ (Suc\ n)\ \isasymin \ even;\ n\ \isasymin \ even\
   129 \isasymLongrightarrow \ P\isasymrbrakk \ \isasymLongrightarrow \ P%
   130 \rulename{Suc_Suc_cases}
   131 \end{isabelle}
   132 %
   133 Applying this as an elimination rule yields one case where \isa{even.cases}
   134 would yield two.  Rule inversion works well when the conclusions of the
   135 introduction rules involve datatype constructors like \isa{Suc} and \isa{\#}
   136 (list `cons'); freeness reasoning discards all but one or two cases.
   137 
   138 In the \isacommand{inductive\_cases} command we supplied an
   139 attribute, \isa{elim!}, indicating that this elimination rule can be applied
   140 aggressively.  The original
   141 \isa{cases} rule would loop if used in that manner because the
   142 pattern~\isa{a} matches everything.
   143 
   144 The rule \isa{Suc_Suc_cases} is equivalent to the following implication:
   145 \begin{isabelle}
   146 Suc (Suc\ n)\ \isasymin \ even\ \isasymLongrightarrow \ n\ \isasymin \
   147 even
   148 \end{isabelle}
   149 %
   150 In \S\ref{sec:gen-rule-induction} we devoted some effort to proving precisely
   151 this result.  Yet we could have obtained it by a one-line declaration. 
   152 This example also justifies the terminology \textbf{rule inversion}: the new
   153 rule inverts the introduction rule \isa{even.step}.
   154 
   155 For one-off applications of rule inversion, use the \isa{ind_cases} method. 
   156 Here is an example:
   157 \begin{isabelle}
   158 \isacommand{apply}\ (ind_cases\ "Suc(Suc\ n)\ \isasymin \ even")
   159 \end{isabelle}
   160 The specified instance of the \isa{cases} rule is generated, applied, and
   161 discarded.
   162 
   163 \medskip
   164 Let us try rule inversion on our ground terms example:
   165 \begin{isabelle}
   166 \isacommand{inductive\_cases}\ gterm_Apply_elim\ [elim!]:\ "Apply\ f\ args\
   167 \isasymin\ gterms\ F"
   168 \end{isabelle}
   169 %
   170 Here is the result.  No cases are discarded (there was only one to begin
   171 with) but the rule applies specifically to the pattern \isa{Apply\ f\ args}.
   172 It can be applied repeatedly as an elimination rule without looping, so we
   173 have given the
   174 \isa{elim!}\ attribute. 
   175 \begin{isabelle}
   176 \isasymlbrakk Apply\ f\ args\ \isasymin \ gterms\ F;\isanewline
   177 \ \isasymlbrakk
   178 \isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F;\ f\ \isasymin
   179 \ F\isasymrbrakk \ \isasymLongrightarrow \ P\isasymrbrakk\isanewline
   180 \isasymLongrightarrow \ P%
   181 \rulename{gterm_Apply_elim}
   182 \end{isabelle}
   183 
   184 This rule replaces an assumption about \isa{Apply\ f\ args} by 
   185 assumptions about \isa{f} and~\isa{args}.  Here is a proof in which this
   186 inference is essential.  We show that if \isa{t} is a ground term over both
   187 of the sets
   188 \isa{F} and~\isa{G} then it is also a ground term over their intersection,
   189 \isa{F\isasyminter G}.
   190 \begin{isabelle}
   191 \isacommand{lemma}\ gterms_IntI\ [rule_format]:\isanewline
   192 \ \ \ \ \ "t\ \isasymin \ gterms\ F\ \isasymLongrightarrow \ t\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ t\ \isasymin \ gterms\ (F\isasyminter G)"\isanewline
   193 \isacommand{apply}\ (erule\ gterms.induct)\isanewline
   194 \isacommand{apply}\ blast\isanewline
   195 \isacommand{done}
   196 \end{isabelle}
   197 %
   198 The proof begins with rule induction over the definition of
   199 \isa{gterms}, which leaves a single subgoal:  
   200 \begin{isabelle}
   201 1.\ \isasymAnd args\ f.\isanewline
   202 \ \ \ \ \ \ \isasymlbrakk \isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F\ \isasymand\isanewline
   203 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (t\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ t\ \isasymin \ gterms\ (F\ \isasyminter \ G));\isanewline
   204 \ \ \ \ \ \ \ f\ \isasymin \ F\isasymrbrakk \isanewline
   205 \ \ \ \ \ \ \isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ (F\ \isasyminter \ G)
   206 \end{isabelle}
   207 %
   208 The induction hypothesis states that every element of \isa{args} belongs to 
   209 \isa{gterms\ (F\ \isasyminter \ G)} --- provided it already belongs to
   210 \isa{gterms\ G}.  How do we meet that condition?  
   211 
   212 By assuming (as we may) the formula \isa{Apply\ f\ args\ \isasymin \ gterms\
   213 G}.  Rule inversion, in the form of \isa{gterm_Apply_elim}, infers that every
   214 element of \isa{args} belongs to 
   215 \isa{gterms~G}.  It also yields \isa{f\ \isasymin \ G}, which will allow us
   216 to conclude \isa{f\ \isasymin \ F\ \isasyminter \ G}.  All of this reasoning
   217 is done by \isa{blast}.
   218 
   219 \medskip
   220 
   221 To summarize, every inductive definition produces a \isa{cases} rule.  The
   222 \isacommand{inductive\_cases} command stores an instance of the \isa{cases}
   223 rule for a given pattern.  Within a proof, the \isa{ind_cases} method
   224 applies an instance of the \isa{cases}
   225 rule.
   226 
   227 
   228 \subsection{Continuing the `ground terms' example}
   229 
   230 Call a term \textbf{well-formed} if each symbol occurring in it has 
   231 the correct number of arguments. To formalize this concept, we 
   232 introduce a function mapping each symbol to its arity, a natural 
   233 number. 
   234 
   235 Let us define the set of well-formed ground terms. 
   236 Suppose we are given a function called \isa{arity}, specifying the arities to be used.
   237 In the inductive step, we have a list \isa{args} of such terms and a function 
   238 symbol~\isa{f}. If the length of the list matches the function's arity 
   239 then applying \isa{f} to \isa{args} yields a well-formed term. 
   240 \begin{isabelle}
   241 \isacommand{consts}\ well_formed_gterm\ ::\ "('f\ \isasymRightarrow \ nat)\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline
   242 \isacommand{inductive}\ "well_formed_gterm\ arity"\isanewline
   243 \isakeyword{intros}\isanewline
   244 step[intro!]:\ "\isasymlbrakk \isasymforall t\ \isasymin \ set\ args.\ t\ \isasymin \ well_formed_gterm\ arity;\ \ \isanewline
   245 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ =\ arity\ f\isasymrbrakk \isanewline
   246 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ well_formed_gterm\
   247 arity"
   248 \end{isabelle}
   249 %
   250 The inductive definition neatly captures the reasoning above.
   251 It is just an elaboration of the previous one, consisting of a single 
   252 introduction rule. The universal quantification over the
   253 \isa{set} of arguments expresses that all of them are well-formed.
   254 
   255 \subsection{Alternative definition using a monotonic function}
   256 
   257 An inductive definition may refer to the inductively defined 
   258 set through an arbitrary monotonic function.  To demonstrate this
   259 powerful feature, let us
   260 change the  inductive definition above, replacing the
   261 quantifier by a use of the function \isa{lists}. This
   262 function, from the Isabelle library, is analogous to the
   263 function \isa{gterms} declared above. If \isa{A} is a set then
   264 {\isa{lists A}} is the set of lists whose elements belong to
   265 \isa{A}.  
   266 
   267 In the inductive definition of well-formed terms, examine the one
   268 introduction rule.  The first premise states that \isa{args} belongs to
   269 the \isa{lists} of well-formed terms.  This formulation is more
   270 direct, if more obscure, than using a universal quantifier.
   271 \begin{isabelle}
   272 \isacommand{consts}\ well_formed_gterm'\ ::\ "('f\ \isasymRightarrow \ nat)\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline
   273 \isacommand{inductive}\ "well_formed_gterm'\ arity"\isanewline
   274 \isakeyword{intros}\isanewline
   275 step[intro!]:\ "\isasymlbrakk args\ \isasymin \ lists\ (well_formed_gterm'\ arity);\ \ \isanewline
   276 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ =\ arity\ f\isasymrbrakk \isanewline
   277 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ well_formed_gterm'\ arity"\isanewline
   278 \isakeyword{monos}\ lists_mono
   279 \end{isabelle}
   280 
   281 We must cite the theorem \isa{lists_mono} in order to justify 
   282 using the function \isa{lists}. 
   283 \begin{isabelle}
   284 A\ \isasymsubseteq\ B\ \isasymLongrightarrow \ lists\ A\ \isasymsubseteq
   285 \ lists\ B\rulename{lists_mono}
   286 \end{isabelle}
   287 %
   288 Why must the function be monotonic?  An inductive definition describes
   289 an iterative construction: each element of the set is constructed by a
   290 finite number of introduction rule applications.  For example, the
   291 elements of \isa{even} are constructed by finitely many applications of
   292 the rules 
   293 \begin{isabelle}
   294 0\ \isasymin \ even\isanewline
   295 n\ \isasymin \ even\ \isasymLongrightarrow \ (Suc\ (Suc\ n))\ \isasymin
   296 \ even
   297 \end{isabelle}
   298 All references to a set in its
   299 inductive definition must be positive.  Applications of an
   300 introduction rule cannot invalidate previous applications, allowing the
   301 construction process to converge.
   302 The following pair of rules do not constitute an inductive definition:
   303 \begin{isabelle}
   304 0\ \isasymin \ even\isanewline
   305 n\ \isasymnotin \ even\ \isasymLongrightarrow \ (Suc\ n)\ \isasymin
   306 \ even
   307 \end{isabelle}
   308 %
   309 Showing that 4 is even using these rules requires showing that 3 is not
   310 even.  It is far from trivial to show that this set of rules
   311 characterizes the even numbers.  
   312 
   313 Even with its use of the function \isa{lists}, the premise of our
   314 introduction rule is positive:
   315 \begin{isabelle}
   316 args\ \isasymin \ lists\ (well_formed_gterm'\ arity)
   317 \end{isabelle}
   318 To apply the rule we construct a list \isa{args} of previously
   319 constructed well-formed terms.  We obtain a
   320 new term, \isa{Apply\ f\ args}.  Because \isa{lists} is monotonic,
   321 applications of the rule remain valid as new terms are constructed.
   322 Further lists of well-formed
   323 terms become available and none are taken away.
   324 
   325 
   326 \subsection{A proof of equivalence}
   327 
   328 We naturally hope that these two inductive definitions of `well-formed' 
   329 coincide.  The equality can be proved by separate inclusions in 
   330 each direction.  Each is a trivial rule induction. 
   331 \begin{isabelle}
   332 \isacommand{lemma}\ "well_formed_gterm\ arity\ \isasymsubseteq \ well_formed_gterm'\ arity"\isanewline
   333 \isacommand{apply}\ clarify\isanewline
   334 \isacommand{apply}\ (erule\ well_formed_gterm.induct)\isanewline
   335 \isacommand{apply}\ auto\isanewline
   336 \isacommand{done}
   337 \end{isabelle}
   338 
   339 The \isa{clarify} method gives
   340 us an element of \isa{well_formed_gterm\ arity} on which to perform 
   341 induction.  The resulting subgoal can be proved automatically:
   342 \begin{isabelle}
   343 {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline
   344 \ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline
   345 \ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymand}\ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline
   346 \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
   347 \ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity%
   348 \end{isabelle}
   349 %
   350 This proof resembles the one given in
   351 \S\ref{sec:gterm-datatype} above, especially in the form of the
   352 induction hypothesis.  Next, we consider the opposite inclusion:
   353 \begin{isabelle}
   354 \isacommand{lemma}\ "well_formed_gterm'\ arity\ \isasymsubseteq \ well_formed_gterm\ arity"\isanewline
   355 \isacommand{apply}\ clarify\isanewline
   356 \isacommand{apply}\ (erule\ well_formed_gterm'.induct)\isanewline
   357 \isacommand{apply}\ auto\isanewline
   358 \isacommand{done}
   359 \end{isabelle}
   360 %
   361 The proof script is identical, but the subgoal after applying induction may
   362 be surprising:
   363 \begin{isabelle}
   364 1.\ \isasymAnd x\ args\ f.\isanewline
   365 \ \ \ \ \ \ \isasymlbrakk args\ \isasymin \ lists\ (well_formed_gterm'\ arity\ \isasyminter\isanewline
   366 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacharbraceleft u.\ u\ \isasymin \ well_formed_gterm\ arity\isacharbraceright );\isanewline
   367 \ \ \ \ \ \ \ length\ args\ =\ arity\ f\isasymrbrakk \isanewline
   368 \ \ \ \ \ \ \isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ well_formed_gterm\ arity%
   369 \end{isabelle}
   370 The induction hypothesis contains an application of \isa{lists}.  Using a
   371 monotonic function in the inductive definition always has this effect.  The
   372 subgoal may look uninviting, but fortunately a useful rewrite rule concerning
   373 \isa{lists} is available:
   374 \begin{isabelle}
   375 lists\ (A\ \isasyminter \ B)\ =\ lists\ A\ \isasyminter \ lists\ B
   376 \rulename{lists_Int_eq}
   377 \end{isabelle}
   378 %
   379 Thanks to this default simplification rule, the induction hypothesis 
   380 is quickly replaced by its two parts:
   381 \begin{isabelle}
   382 \ \ \ \ \ \ \ args\ \isasymin \ lists\ (well_formed_gterm'\ arity)\isanewline
   383 \ \ \ \ \ \ \ args\ \isasymin \ lists\ (well_formed_gterm\ arity)
   384 \end{isabelle}
   385 Invoking the rule \isa{well_formed_gterm.step} completes the proof.  The
   386 call to
   387 \isa{auto} does all this work.
   388 
   389 This example is typical of how monotonic functions can be used.  In
   390 particular, a rewrite rule analogous to \isa{lists_Int_eq} holds in most
   391 cases.  Monotonicity implies one direction of this set equality; we have
   392 this theorem:
   393 \begin{isabelle}
   394 mono\ f\ \isasymLongrightarrow \ f\ (A\ \isasyminter \ B)\ \isasymsubseteq \
   395 f\ A\ \isasyminter \ f\ B%
   396 \rulename{mono_Int}
   397 \end{isabelle}
   398 
   399 
   400 To summarize: a universal quantifier in an introduction rule 
   401 lets it refer to any number of instances of 
   402 the inductively defined set.  A monotonic function in an introduction 
   403 rule lets it refer to constructions over the inductively defined 
   404 set.  Each element of an inductively defined set is created 
   405 through finitely many applications of the introduction rules.  So each rule
   406 must be positive, and never can it refer to \textit{infinitely} many
   407 previous instances of the inductively defined set. 
   408 
   409 
   410 
   411 \begin{exercise}
   412 Prove this theorem, one direction of which was proved in
   413 \S\ref{sec:rule-inversion} above.
   414 \begin{isabelle}
   415 \isacommand{lemma}\ gterms_Int_eq\ [simp]:\ "gterms\ (F\isasyminter G)\ =\
   416 gterms\ F\ \isasyminter \ gterms\ G"\isanewline
   417 \end{isabelle}
   418 \end{exercise}
   419 
   420 
   421 \begin{exercise}
   422 A function mapping function symbols to their 
   423 types is called a \textbf{signature}.  Given a type 
   424 ranging over type symbols, we can represent a function's type by a
   425 list of argument types paired with the result type. 
   426 Complete this inductive definition:
   427 \begin{isabelle}
   428 \isacommand{consts}\ well_typed_gterm::\ "('f\ \isasymRightarrow \ 't\ list\ *\ 't)\ \isasymRightarrow \ ('f\ gterm\ *\ 't)set"\isanewline
   429 \isacommand{inductive}\ "well_typed_gterm\ sig"\isanewline
   430 \end{isabelle}
   431 \end{exercise}