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