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