2 (*<*)theory Advanced imports Even uses "../../antiquote_setup.ML" begin(*>*)
5 The premises of introduction rules may contain universal quantifiers and
6 monotone functions. A universal quantifier lets the rule
7 refer to any number of instances of
8 the inductively defined set. A monotone function lets the rule refer
9 to existing constructions (such as ``list of'') over the inductively defined
10 set. The examples below show how to use the additional expressiveness
11 and how to reason from the resulting definitions.
14 subsection{* Universal Quantifiers in Introduction Rules \label{sec:gterm-datatype} *}
17 \index{ground terms example|(}%
18 \index{quantifiers!and inductive definitions|(}%
19 As a running example, this section develops the theory of \textbf{ground
20 terms}: terms constructed from constant and function
21 symbols but not variables. To simplify matters further, we regard a
22 constant as a function applied to the null argument list. Let us declare a
23 datatype @{text gterm} for the type of ground terms. It is a type constructor
24 whose argument is a type of function symbols.
27 datatype 'f gterm = Apply 'f "'f gterm list"
30 To try it out, we declare a datatype of some integer operations:
31 integer constants, the unary minus operator and the addition
35 datatype integer_op = Number int | UnaryMinus | Plus
38 Now the type @{typ "integer_op gterm"} denotes the ground
39 terms built over those symbols.
41 The type constructor @{text gterm} can be generalized to a function
43 the set of ground terms that can be formed over a set @{text F} of function symbols. For
44 example, we could consider the set of ground terms formed from the finite
45 set @{text "{Number 2, UnaryMinus, Plus}"}.
47 This concept is inductive. If we have a list @{text args} of ground terms
48 over~@{text F} and a function symbol @{text f} in @{text F}, then we
49 can apply @{text f} to @{text args} to obtain another ground term.
50 The only difficulty is that the argument list may be of any length. Hitherto,
51 each rule in an inductive definition referred to the inductively
52 defined set a fixed number of times, typically once or twice.
53 A universal quantifier in the premise of the introduction rule
54 expresses that every element of @{text args} belongs
55 to our inductively defined set: is a ground term
56 over~@{text F}. The function @{term set} denotes the set of elements in a given
61 gterms :: "'f set \<Rightarrow> 'f gterm set"
64 step[intro!]: "\<lbrakk>\<forall>t \<in> set args. t \<in> gterms F; f \<in> F\<rbrakk>
65 \<Longrightarrow> (Apply f args) \<in> gterms F"
68 To demonstrate a proof from this definition, let us
69 show that the function @{term gterms}
70 is \textbf{monotone}. We shall need this concept shortly.
73 lemma gterms_mono: "F\<subseteq>G \<Longrightarrow> gterms F \<subseteq> gterms G"
75 apply (erule gterms.induct)
79 lemma gterms_mono: "F\<subseteq>G \<Longrightarrow> gterms F \<subseteq> gterms G"
81 apply (erule gterms.induct)
84 Intuitively, this theorem says that
85 enlarging the set of function symbols enlarges the set of ground
86 terms. The proof is a trivial rule induction.
87 First we use the @{text clarify} method to assume the existence of an element of
88 @{term "gterms F"}. (We could have used @{text "intro subsetI"}.) We then
89 apply rule induction. Here is the resulting subgoal:
90 @{subgoals[display,indent=0]}
91 The assumptions state that @{text f} belongs
92 to~@{text F}, which is included in~@{text G}, and that every element of the list @{text args} is
93 a ground term over~@{text G}. The @{text blast} method finds this chain of reasoning easily.
98 Why do we call this function @{text gterms} instead
99 of @{text gterm}? A constant may have the same name as a type. However,
100 name clashes could arise in the theorems that Isabelle generates.
101 Our choice of names keeps @{text gterms.induct} separate from
102 @{text gterm.induct}.
105 Call a term \textbf{well-formed} if each symbol occurring in it is applied
106 to the correct number of arguments. (This number is called the symbol's
107 \textbf{arity}.) We can express well-formedness by
108 generalizing the inductive definition of
110 Suppose we are given a function called @{text arity}, specifying the arities
111 of all symbols. In the inductive step, we have a list @{text args} of such
112 terms and a function symbol~@{text f}. If the length of the list matches the
113 function's arity then applying @{text f} to @{text args} yields a well-formed
118 well_formed_gterm :: "('f \<Rightarrow> nat) \<Rightarrow> 'f gterm set"
119 for arity :: "'f \<Rightarrow> nat"
121 step[intro!]: "\<lbrakk>\<forall>t \<in> set args. t \<in> well_formed_gterm arity;
122 length args = arity f\<rbrakk>
123 \<Longrightarrow> (Apply f args) \<in> well_formed_gterm arity"
126 The inductive definition neatly captures the reasoning above.
127 The universal quantification over the
128 @{text set} of arguments expresses that all of them are well-formed.%
129 \index{quantifiers!and inductive definitions|)}
132 subsection{* Alternative Definition Using a Monotone Function *}
135 \index{monotone functions!and inductive definitions|(}%
136 An inductive definition may refer to the
137 inductively defined set through an arbitrary monotone function. To
138 demonstrate this powerful feature, let us
139 change the inductive definition above, replacing the
140 quantifier by a use of the function @{term lists}. This
141 function, from the Isabelle theory of lists, is analogous to the
142 function @{term gterms} declared above: if @{text A} is a set then
143 @{term "lists A"} is the set of lists whose elements belong to
146 In the inductive definition of well-formed terms, examine the one
147 introduction rule. The first premise states that @{text args} belongs to
148 the @{text lists} of well-formed terms. This formulation is more
149 direct, if more obscure, than using a universal quantifier.
153 well_formed_gterm' :: "('f \<Rightarrow> nat) \<Rightarrow> 'f gterm set"
154 for arity :: "'f \<Rightarrow> nat"
156 step[intro!]: "\<lbrakk>args \<in> lists (well_formed_gterm' arity);
157 length args = arity f\<rbrakk>
158 \<Longrightarrow> (Apply f args) \<in> well_formed_gterm' arity"
162 We cite the theorem @{text lists_mono} to justify
163 using the function @{term lists}.%
164 \footnote{This particular theorem is installed by default already, but we
165 include the \isakeyword{monos} declaration in order to illustrate its syntax.}
166 @{named_thms [display,indent=0] lists_mono [no_vars] (lists_mono)}
167 Why must the function be monotone? An inductive definition describes
168 an iterative construction: each element of the set is constructed by a
169 finite number of introduction rule applications. For example, the
170 elements of \isa{even} are constructed by finitely many applications of
172 @{thm [display,indent=0] even.intros [no_vars]}
173 All references to a set in its
174 inductive definition must be positive. Applications of an
175 introduction rule cannot invalidate previous applications, allowing the
176 construction process to converge.
177 The following pair of rules do not constitute an inductive definition:
179 \item @{term "0 \<in> even"}
180 \item @{term "n \<notin> even \<Longrightarrow> (Suc n) \<in> even"}
182 Showing that 4 is even using these rules requires showing that 3 is not
183 even. It is far from trivial to show that this set of rules
184 characterizes the even numbers.
186 Even with its use of the function \isa{lists}, the premise of our
187 introduction rule is positive:
188 @{thm [display,indent=0] (prem 1) step [no_vars]}
189 To apply the rule we construct a list @{term args} of previously
190 constructed well-formed terms. We obtain a
191 new term, @{term "Apply f args"}. Because @{term lists} is monotone,
192 applications of the rule remain valid as new terms are constructed.
193 Further lists of well-formed
194 terms become available and none are taken away.%
195 \index{monotone functions!and inductive definitions|)}
198 subsection{* A Proof of Equivalence *}
201 We naturally hope that these two inductive definitions of ``well-formed''
202 coincide. The equality can be proved by separate inclusions in
203 each direction. Each is a trivial rule induction.
206 lemma "well_formed_gterm arity \<subseteq> well_formed_gterm' arity"
208 apply (erule well_formed_gterm.induct)
212 lemma "well_formed_gterm arity \<subseteq> well_formed_gterm' arity"
214 apply (erule well_formed_gterm.induct)
217 The @{text clarify} method gives
218 us an element of @{term "well_formed_gterm arity"} on which to perform
219 induction. The resulting subgoal can be proved automatically:
220 @{subgoals[display,indent=0]}
221 This proof resembles the one given in
222 {\S}\ref{sec:gterm-datatype} above, especially in the form of the
223 induction hypothesis. Next, we consider the opposite inclusion:
226 lemma "well_formed_gterm' arity \<subseteq> well_formed_gterm arity"
228 apply (erule well_formed_gterm'.induct)
232 lemma "well_formed_gterm' arity \<subseteq> well_formed_gterm arity"
234 apply (erule well_formed_gterm'.induct)
237 The proof script is virtually identical,
238 but the subgoal after applying induction may be surprising:
239 @{subgoals[display,indent=0,margin=65]}
240 The induction hypothesis contains an application of @{term lists}. Using a
241 monotone function in the inductive definition always has this effect. The
242 subgoal may look uninviting, but fortunately
243 @{term lists} distributes over intersection:
244 @{named_thms [display,indent=0] lists_Int_eq [no_vars] (lists_Int_eq)}
245 Thanks to this default simplification rule, the induction hypothesis
246 is quickly replaced by its two parts:
248 \item @{term "args \<in> lists (well_formed_gterm' arity)"}
249 \item @{term "args \<in> lists (well_formed_gterm arity)"}
251 Invoking the rule @{text well_formed_gterm.step} completes the proof. The
252 call to @{text auto} does all this work.
254 This example is typical of how monotone functions
255 \index{monotone functions} can be used. In particular, many of them
256 distribute over intersection. Monotonicity implies one direction of
257 this set equality; we have this theorem:
258 @{named_thms [display,indent=0] mono_Int [no_vars] (mono_Int)}
263 subsection{* Another Example of Rule Inversion *}
266 \index{rule inversion|(}%
267 Does @{term gterms} distribute over intersection? We have proved that this
268 function is monotone, so @{text mono_Int} gives one of the inclusions. The
269 opposite inclusion asserts that if @{term t} is a ground term over both of the
271 @{term F} and~@{term G} then it is also a ground term over their intersection,
272 @{term "F \<inter> G"}.
276 "t \<in> gterms F \<Longrightarrow> t \<in> gterms G \<longrightarrow> t \<in> gterms (F\<inter>G)"
279 Attempting this proof, we get the assumption
280 @{term "Apply f args \<in> gterms G"}, which cannot be broken down.
281 It looks like a job for rule inversion:\cmmdx{inductive\protect\_cases}
284 inductive_cases gterm_Apply_elim [elim!]: "Apply f args \<in> gterms F"
288 @{named_thms [display,indent=0,margin=50] gterm_Apply_elim [no_vars] (gterm_Apply_elim)}
289 This rule replaces an assumption about @{term "Apply f args"} by
290 assumptions about @{term f} and~@{term args}.
291 No cases are discarded (there was only one to begin
292 with) but the rule applies specifically to the pattern @{term "Apply f args"}.
293 It can be applied repeatedly as an elimination rule without looping, so we
294 have given the @{text "elim!"} attribute.
296 Now we can prove the other half of that distributive law.
299 lemma gterms_IntI [rule_format, intro!]:
300 "t \<in> gterms F \<Longrightarrow> t \<in> gterms G \<longrightarrow> t \<in> gterms (F\<inter>G)"
301 apply (erule gterms.induct)
305 lemma "t \<in> gterms F \<Longrightarrow> t \<in> gterms G \<longrightarrow> t \<in> gterms (F\<inter>G)"
306 apply (erule gterms.induct)
309 The proof begins with rule induction over the definition of
310 @{term gterms}, which leaves a single subgoal:
311 @{subgoals[display,indent=0,margin=65]}
312 To prove this, we assume @{term "Apply f args \<in> gterms G"}. Rule inversion,
313 in the form of @{text gterm_Apply_elim}, infers
314 that every element of @{term args} belongs to
315 @{term "gterms G"}; hence (by the induction hypothesis) it belongs
316 to @{term "gterms (F \<inter> G)"}. Rule inversion also yields
317 @{term "f \<in> G"} and hence @{term "f \<in> F \<inter> G"}.
318 All of this reasoning is done by @{text blast}.
321 Our distributive law is a trivial consequence of previously-proved results:
324 lemma gterms_Int_eq [simp]:
325 "gterms (F \<inter> G) = gterms F \<inter> gterms G"
326 by (blast intro!: mono_Int monoI gterms_mono)
329 \index{rule inversion|)}%
330 \index{ground terms example|)}
333 \begin{isamarkuptext}
335 A function mapping function symbols to their
336 types is called a \textbf{signature}. Given a type
337 ranging over type symbols, we can represent a function's type by a
338 list of argument types paired with the result type.
339 Complete this inductive definition:
344 well_typed_gterm :: "('f \<Rightarrow> 't list * 't) \<Rightarrow> ('f gterm * 't)set"
345 for sig :: "'f \<Rightarrow> 't list * 't"
349 "\<lbrakk>\<forall>pair \<in> set args. pair \<in> well_typed_gterm sig;
350 sig f = (map snd args, rtype)\<rbrakk>
351 \<Longrightarrow> (Apply f (map fst args), rtype)
352 \<in> well_typed_gterm sig"
362 text{*the following declaration isn't actually used*}
363 consts integer_arity :: "integer_op \<Rightarrow> nat"
365 "integer_arity (Number n) = 0"
366 "integer_arity UnaryMinus = 1"
367 "integer_arity Plus = 2"
369 text{* the rest isn't used: too complicated. OK for an exercise though.*}
372 integer_signature :: "(integer_op * (unit list * unit)) set"
374 Number: "(Number n, ([], ())) \<in> integer_signature"
375 | UnaryMinus: "(UnaryMinus, ([()], ())) \<in> integer_signature"
376 | Plus: "(Plus, ([(),()], ())) \<in> integer_signature"
379 well_typed_gterm' :: "('f \<Rightarrow> 't list * 't) \<Rightarrow> ('f gterm * 't)set"
380 for sig :: "'f \<Rightarrow> 't list * 't"
383 "\<lbrakk>args \<in> lists(well_typed_gterm' sig);
384 sig f = (map snd args, rtype)\<rbrakk>
385 \<Longrightarrow> (Apply f (map fst args), rtype)
386 \<in> well_typed_gterm' sig"
390 lemma "well_typed_gterm sig \<subseteq> well_typed_gterm' sig"
392 apply (erule well_typed_gterm.induct)
396 lemma "well_typed_gterm' sig \<subseteq> well_typed_gterm sig"
398 apply (erule well_typed_gterm'.induct)