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