doc-src/TutorialI/Sets/sets.tex
 author wenzelm Wed Jul 25 12:38:54 2012 +0200 (2012-07-25) changeset 48497 ba61aceaa18a parent 44050 f7634e2300bc permissions -rw-r--r--
some updates on "Building a repository version of Isabelle";
1 \chapter{Sets, Functions and Relations}
3 This chapter describes the formalization of typed set theory, which is
4 the basis of much else in HOL\@.  For example, an
5 inductive definition yields a set, and the abstract theories of relations
6 regard a relation as a set of pairs.  The chapter introduces the well-known
7 constants such as union and intersection, as well as the main operations on relations, such as converse, composition and
8 transitive closure.  Functions are also covered.  They are not sets in
9 HOL, but many of their properties concern sets: the range of a
10 function is a set, and the inverse image of a function maps sets to sets.
12 This chapter will be useful to anybody who plans to develop a substantial
13 proof.  Sets are convenient for formalizing  computer science concepts such
14 as grammars, logical calculi and state transition systems.  Isabelle can
15 prove many statements involving sets automatically.
17 This chapter ends with a case study concerning model checking for the
18 temporal logic CTL\@.  Most of the other examples are simple.  The
19 chapter presents a small selection of built-in theorems in order to point
20 out some key properties of the various constants and to introduce you to
21 the notation.
23 Natural deduction rules are provided for the set theory constants, but they
24 are seldom used directly, so only a few are presented here.
27 \section{Sets}
29 \index{sets|(}%
30 HOL's set theory should not be confused with traditional,  untyped set
31 theory, in which everything is a set.  Our sets are typed. In a given set,
32 all elements have the same type, say~$\tau$,  and the set itself has type
33 $\tau$~\tydx{set}.
35 We begin with \textbf{intersection}, \textbf{union} and
36 \textbf{complement}. In addition to the
37 \textbf{membership relation}, there  is a symbol for its negation. These
38 points can be seen below.
40 Here are the natural deduction rules for \rmindex{intersection}.  Note
41 the  resemblance to those for conjunction.
42 \begin{isabelle}
43 \isasymlbrakk c\ \isasymin\ A;\ c\ \isasymin\ B\isasymrbrakk\
44 \isasymLongrightarrow\ c\ \isasymin\ A\ \isasyminter\ B%
45 \rulenamedx{IntI}\isanewline
46 c\ \isasymin\ A\ \isasyminter\ B\ \isasymLongrightarrow\ c\ \isasymin\ A
47 \rulenamedx{IntD1}\isanewline
48 c\ \isasymin\ A\ \isasyminter\ B\ \isasymLongrightarrow\ c\ \isasymin\ B
49 \rulenamedx{IntD2}
50 \end{isabelle}
52 Here are two of the many installed theorems concerning set
53 complement.\index{complement!of a set}
54 Note that it is denoted by a minus sign.
55 \begin{isabelle}
56 (c\ \isasymin\ -\ A)\ =\ (c\ \isasymnotin\ A)
57 \rulenamedx{Compl_iff}\isanewline
58 -\ (A\ \isasymunion\ B)\ =\ -\ A\ \isasyminter\ -\ B
59 \rulename{Compl_Un}
60 \end{isabelle}
62 Set \textbf{difference}\indexbold{difference!of sets} is the intersection
63 of a set with the  complement of another set. Here we also see the syntax
64 for the  empty set and for the universal set.
65 \begin{isabelle}
66 A\ \isasyminter\ (B\ -\ A)\ =\ \isacharbraceleft\isacharbraceright
67 \rulename{Diff_disjoint}\isanewline
68 A\ \isasymunion\ -\ A\ =\ UNIV%
69 \rulename{Compl_partition}
70 \end{isabelle}
72 The \bfindex{subset relation} holds between two sets just if every element
73 of one is also an element of the other. This relation is reflexive.  These
74 are its natural deduction rules:
75 \begin{isabelle}
76 ({\isasymAnd}x.\ x\ \isasymin\ A\ \isasymLongrightarrow\ x\ \isasymin\ B)\ \isasymLongrightarrow\ A\ \isasymsubseteq\ B%
77 \rulenamedx{subsetI}%
78 \par\smallskip%          \isanewline didn't leave enough space
79 \isasymlbrakk A\ \isasymsubseteq\ B;\ c\ \isasymin\
80 A\isasymrbrakk\ \isasymLongrightarrow\ c\
81 \isasymin\ B%
82 \rulenamedx{subsetD}
83 \end{isabelle}
84 In harder proofs, you may need to apply \isa{subsetD} giving a specific term
85 for~\isa{c}.  However, \isa{blast} can instantly prove facts such as this
86 one:
87 \begin{isabelle}
88 (A\ \isasymunion\ B\ \isasymsubseteq\ C)\ =\
89 (A\ \isasymsubseteq\ C\ \isasymand\ B\ \isasymsubseteq\ C)
90 \rulenamedx{Un_subset_iff}
91 \end{isabelle}
92 Here is another example, also proved automatically:
93 \begin{isabelle}
94 \isacommand{lemma}\ "(A\
95 \isasymsubseteq\ -B)\ =\ (B\ \isasymsubseteq\ -A)"\isanewline
96 \isacommand{by}\ blast
97 \end{isabelle}
98 %
99 This is the same example using \textsc{ascii} syntax, illustrating a pitfall:
100 \begin{isabelle}
101 \isacommand{lemma}\ "(A\ <=\ -B)\ =\ (B\ <=\ -A)"
102 \end{isabelle}
103 %
104 The proof fails.  It is not a statement about sets, due to overloading;
105 the relation symbol~\isa{<=} can be any relation, not just
106 subset.
107 In this general form, the statement is not valid.  Putting
108 in a type constraint forces the variables to denote sets, allowing the
109 proof to succeed:
111 \begin{isabelle}
112 \isacommand{lemma}\ "((A::\ {\isacharprime}a\ set)\ <=\ -B)\ =\ (B\ <=\
113 -A)"
114 \end{isabelle}
116 \isa{A~\isasymsubseteq~-B} asserts that the sets \isa{A} and \isa{B} are
117 disjoint.
119 \medskip
120 Two sets are \textbf{equal}\indexbold{equality!of sets} if they contain the
121 same elements.   This is
122 the principle of \textbf{extensionality}\indexbold{extensionality!for sets}
123 for sets.
124 \begin{isabelle}
125 ({\isasymAnd}x.\ (x\ {\isasymin}\ A)\ =\ (x\ {\isasymin}\ B))\
126 {\isasymLongrightarrow}\ A\ =\ B
127 \rulenamedx{set_ext}
128 \end{isabelle}
129 Extensionality can be expressed as
130 $A=B\iff (A\subseteq B)\conj (B\subseteq A)$.
131 The following rules express both
132 directions of this equivalence.  Proving a set equation using
133 \isa{equalityI} allows the two inclusions to be proved independently.
134 \begin{isabelle}
135 \isasymlbrakk A\ \isasymsubseteq\ B;\ B\ \isasymsubseteq\
136 A\isasymrbrakk\ \isasymLongrightarrow\ A\ =\ B
137 \rulenamedx{equalityI}
138 \par\smallskip%          \isanewline didn't leave enough space
139 \isasymlbrakk A\ =\ B;\ \isasymlbrakk A\ \isasymsubseteq\ B;\ B\
140 \isasymsubseteq\ A\isasymrbrakk\ \isasymLongrightarrow\ P\isasymrbrakk\
141 \isasymLongrightarrow\ P%
142 \rulenamedx{equalityE}
143 \end{isabelle}
146 \subsection{Finite Set Notation}
148 \indexbold{sets!notation for finite}
149 Finite sets are expressed using the constant \cdx{insert}, which is
150 a form of union:
151 \begin{isabelle}
152 insert\ a\ A\ =\ \isacharbraceleft a\isacharbraceright\ \isasymunion\ A
153 \rulename{insert_is_Un}
154 \end{isabelle}
155 %
156 The finite set expression \isa{\isacharbraceleft
157 a,b\isacharbraceright} abbreviates
158 \isa{insert\ a\ (insert\ b\ \isacharbraceleft\isacharbraceright)}.
159 Many facts about finite sets can be proved automatically:
160 \begin{isabelle}
161 \isacommand{lemma}\
162 "\isacharbraceleft a,b\isacharbraceright\
163 \isasymunion\ \isacharbraceleft c,d\isacharbraceright\ =\
164 \isacharbraceleft a,b,c,d\isacharbraceright"\isanewline
165 \isacommand{by}\ blast
166 \end{isabelle}
169 Not everything that we would like to prove is valid.
170 Consider this attempt:
171 \begin{isabelle}
172 \isacommand{lemma}\ "\isacharbraceleft a,b\isacharbraceright\ \isasyminter\ \isacharbraceleft b,c\isacharbraceright\ =\
173 \isacharbraceleft b\isacharbraceright"\isanewline
174 \isacommand{apply}\ auto
175 \end{isabelle}
176 %
177 The proof fails, leaving the subgoal \isa{b=c}. To see why it
178 fails, consider a correct version:
179 \begin{isabelle}
180 \isacommand{lemma}\ "\isacharbraceleft a,b\isacharbraceright\ \isasyminter\
181 \isacharbraceleft b,c\isacharbraceright\ =\ (if\ a=c\ then\
182 \isacharbraceleft a,b\isacharbraceright\ else\ \isacharbraceleft
183 b\isacharbraceright)"\isanewline
184 \isacommand{apply}\ simp\isanewline
185 \isacommand{by}\ blast
186 \end{isabelle}
188 Our mistake was to suppose that the various items were distinct.  Another
189 remark: this proof uses two methods, namely {\isa{simp}}  and
190 {\isa{blast}}. Calling {\isa{simp}} eliminates the
191 \isa{if}-\isa{then}-\isa{else} expression,  which {\isa{blast}}
192 cannot break down. The combined methods (namely {\isa{force}}  and
193 \isa{auto}) can prove this fact in one step.
196 \subsection{Set Comprehension}
198 \index{set comprehensions|(}%
199 The set comprehension \isa{\isacharbraceleft x.\
200 P\isacharbraceright} expresses the set of all elements that satisfy the
201 predicate~\isa{P}.  Two laws describe the relationship between set
202 comprehension and the membership relation:
203 \begin{isabelle}
204 (a\ \isasymin\
205 \isacharbraceleft x.\ P\ x\isacharbraceright)\ =\ P\ a
206 \rulename{mem_Collect_eq}\isanewline
207 \isacharbraceleft x.\ x\ \isasymin\ A\isacharbraceright\ =\ A
208 \rulename{Collect_mem_eq}
209 \end{isabelle}
211 \smallskip
212 Facts such as these have trivial proofs:
213 \begin{isabelle}
214 \isacommand{lemma}\ "\isacharbraceleft x.\ P\ x\ \isasymor\
215 x\ \isasymin\ A\isacharbraceright\ =\
216 \isacharbraceleft x.\ P\ x\isacharbraceright\ \isasymunion\ A"
217 \par\smallskip
218 \isacommand{lemma}\ "\isacharbraceleft x.\ P\ x\
219 \isasymlongrightarrow\ Q\ x\isacharbraceright\ =\
220 -\isacharbraceleft x.\ P\ x\isacharbraceright\
221 \isasymunion\ \isacharbraceleft x.\ Q\ x\isacharbraceright"
222 \end{isabelle}
224 \smallskip
225 Isabelle has a general syntax for comprehension, which is best
226 described through an example:
227 \begin{isabelle}
228 \isacommand{lemma}\ "\isacharbraceleft p*q\ \isacharbar\ p\ q.\
229 p{\isasymin}prime\ \isasymand\ q{\isasymin}prime\isacharbraceright\ =\
230 \isanewline
231 \ \ \ \ \ \ \ \ \isacharbraceleft z.\ \isasymexists p\ q.\ z\ =\ p*q\
232 \isasymand\ p{\isasymin}prime\ \isasymand\
233 q{\isasymin}prime\isacharbraceright"
234 \end{isabelle}
235 The left and right hand sides
236 of this equation are identical. The syntax used in the
237 left-hand side abbreviates the right-hand side: in this case, all numbers
238 that are the product of two primes.  The syntax provides a neat
239 way of expressing any set given by an expression built up from variables
240 under specific constraints.  The drawback is that it hides the true form of
241 the expression, with its existential quantifiers.
243 \smallskip
244 \emph{Remark}.  We do not need sets at all.  They are essentially equivalent
245 to predicate variables, which are allowed in  higher-order logic.  The main
246 benefit of sets is their notation;  we can write \isa{x{\isasymin}A}
247 and
248 \isa{\isacharbraceleft z.\ P\isacharbraceright} where predicates would
249 require writing
250 \isa{A(x)} and
251 \isa{{\isasymlambda}z.\ P}.
252 \index{set comprehensions|)}
255 \subsection{Binding Operators}
257 \index{quantifiers!for sets|(}%
258 Universal and existential quantifications may range over sets,
259 with the obvious meaning.  Here are the natural deduction rules for the
260 bounded universal quantifier.  Occasionally you will need to apply
261 \isa{bspec} with an explicit instantiation of the variable~\isa{x}:
262 %
263 \begin{isabelle}
264 ({\isasymAnd}x.\ x\ \isasymin\ A\ \isasymLongrightarrow\ P\ x)\ \isasymLongrightarrow\ {\isasymforall}x\isasymin
265 A.\ P\ x%
266 \rulenamedx{ballI}%
267 \isanewline
268 \isasymlbrakk{\isasymforall}x\isasymin A.\
269 P\ x;\ x\ \isasymin\
270 A\isasymrbrakk\ \isasymLongrightarrow\ P\
271 x%
272 \rulenamedx{bspec}
273 \end{isabelle}
274 %
275 Dually, here are the natural deduction rules for the
276 bounded existential quantifier.  You may need to apply
277 \isa{bexI} with an explicit instantiation:
278 \begin{isabelle}
279 \isasymlbrakk P\ x;\
280 x\ \isasymin\ A\isasymrbrakk\
281 \isasymLongrightarrow\
282 \isasymexists x\isasymin A.\ P\
283 x%
284 \rulenamedx{bexI}%
285 \isanewline
286 \isasymlbrakk\isasymexists x\isasymin A.\
287 P\ x;\ {\isasymAnd}x.\
288 {\isasymlbrakk}x\ \isasymin\ A;\
289 P\ x\isasymrbrakk\ \isasymLongrightarrow\
290 Q\isasymrbrakk\ \isasymLongrightarrow\ Q%
291 \rulenamedx{bexE}
292 \end{isabelle}
293 \index{quantifiers!for sets|)}
295 \index{union!indexed}%
296 Unions can be formed over the values of a given  set.  The syntax is
297 \mbox{\isa{\isasymUnion x\isasymin A.\ B}} or
298 \isa{UN x:A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law:
299 \begin{isabelle}
300 (b\ \isasymin\
301 (\isasymUnion x\isasymin A. B\ x)) =\ (\isasymexists x\isasymin A.\
302 b\ \isasymin\ B\ x)
303 \rulenamedx{UN_iff}
304 \end{isabelle}
305 It has two natural deduction rules similar to those for the existential
306 quantifier.  Sometimes \isa{UN_I} must be applied explicitly:
307 \begin{isabelle}
308 \isasymlbrakk a\ \isasymin\
309 A;\ b\ \isasymin\
310 B\ a\isasymrbrakk\ \isasymLongrightarrow\
311 b\ \isasymin\
312 (\isasymUnion x\isasymin A. B\ x)
313 \rulenamedx{UN_I}%
314 \isanewline
315 \isasymlbrakk b\ \isasymin\
316 (\isasymUnion x\isasymin A. B\ x);\
317 {\isasymAnd}x.\ {\isasymlbrakk}x\ \isasymin\
318 A;\ b\ \isasymin\
319 B\ x\isasymrbrakk\ \isasymLongrightarrow\
320 R\isasymrbrakk\ \isasymLongrightarrow\ R%
321 \rulenamedx{UN_E}
322 \end{isabelle}
323 %
324 The following built-in abbreviation (see {\S}\ref{sec:abbreviations})
325 lets us express the union over a \emph{type}:
326 \begin{isabelle}
327 \ \ \ \ \
328 ({\isasymUnion}x.\ B\ x)\ {\isasymequiv}\
329 ({\isasymUnion}x{\isasymin}UNIV. B\ x)
330 \end{isabelle}
332 We may also express the union of a set of sets, written \isa{Union\ C} in
333 \textsc{ascii}:
334 \begin{isabelle}
335 (A\ \isasymin\ \isasymUnion C)\ =\ (\isasymexists X\isasymin C.\ A\
336 \isasymin\ X)
337 \rulenamedx{Union_iff}
338 \end{isabelle}
340 \index{intersection!indexed}%
341 Intersections are treated dually, although they seem to be used less often
342 than unions.  The syntax below would be \isa{INT
343 x:\ A.\ B} and \isa{Inter\ C} in \textsc{ascii}.  Among others, these
344 theorems are available:
345 \begin{isabelle}
346 (b\ \isasymin\
347 (\isasymInter x\isasymin A. B\ x))\
348 =\
349 ({\isasymforall}x\isasymin A.\
350 b\ \isasymin\ B\ x)
351 \rulenamedx{INT_iff}%
352 \isanewline
353 (A\ \isasymin\
354 \isasymInter C)\ =\
355 ({\isasymforall}X\isasymin C.\
356 A\ \isasymin\ X)
357 \rulenamedx{Inter_iff}
358 \end{isabelle}
360 Isabelle uses logical equivalences such as those above in automatic proof.
361 Unions, intersections and so forth are not simply replaced by their
362 definitions.  Instead, membership tests are simplified.  For example,  $x\in 363 A\cup B$ is replaced by $x\in A\lor x\in B$.
365 The internal form of a comprehension involves the constant
366 \cdx{Collect},
367 which occasionally appears when a goal or theorem
368 is displayed.  For example, \isa{Collect\ P}  is the same term as
369 \isa{\isacharbraceleft x.\ P\ x\isacharbraceright}.  The same thing can
370 happen with quantifiers:   \hbox{\isa{All\ P}}\index{*All (constant)}
371 is
372 \isa{{\isasymforall}x.\ P\ x} and
373 \hbox{\isa{Ex\ P}}\index{*Ex (constant)} is \isa{\isasymexists x.\ P\ x};
374 also \isa{Ball\ A\ P}\index{*Ball (constant)} is
375 \isa{{\isasymforall}x\isasymin A.\ P\ x} and
376 \isa{Bex\ A\ P}\index{*Bex (constant)} is
377 \isa{\isasymexists x\isasymin A.\ P\ x}.  For indexed unions and
378 intersections, you may see the constants
379 \cdx{UNION} and  \cdx{INTER}\@.
380 The internal constant for $\varepsilon x.P(x)$ is~\cdx{Eps}.
382 We have only scratched the surface of Isabelle/HOL's set theory, which provides
383 hundreds of theorems for your use.
386 \subsection{Finiteness and Cardinality}
388 \index{sets!finite}%
389 The predicate \sdx{finite} holds of all finite sets.  Isabelle/HOL
390 includes many familiar theorems about finiteness and cardinality
391 (\cdx{card}). For example, we have theorems concerning the
392 cardinalities of unions, intersections and the
393 powerset:\index{cardinality}
394 %
395 \begin{isabelle}
396 {\isasymlbrakk}finite\ A;\ finite\ B\isasymrbrakk\isanewline
397 \isasymLongrightarrow\ card\ A\ \isacharplus\ card\ B\ =\ card\ (A\ \isasymunion\ B)\ \isacharplus\ card\ (A\ \isasyminter\ B)
398 \rulenamedx{card_Un_Int}%
399 \isanewline
400 \isanewline
401 finite\ A\ \isasymLongrightarrow\ card\
402 (Pow\ A)\  =\ 2\ \isacharcircum\ card\ A%
403 \rulenamedx{card_Pow}%
404 \isanewline
405 \isanewline
406 finite\ A\ \isasymLongrightarrow\isanewline
407 card\ \isacharbraceleft B.\ B\ \isasymsubseteq\
408 A\ \isasymand\ card\ B\ =\
409 k\isacharbraceright\ =\ card\ A\ choose\ k%
410 \rulename{n_subsets}
411 \end{isabelle}
412 Writing $|A|$ as $n$, the last of these theorems says that the number of
413 $k$-element subsets of~$A$ is \index{binomial coefficients}
414 $\binom{n}{k}$.
416 %\begin{warn}
417 %The term \isa{finite\ A} is defined via a syntax translation as an
418 %abbreviation for \isa{A {\isasymin} Finites}, where the constant
419 %\cdx{Finites} denotes the set of all finite sets of a given type.  There
420 %is no constant \isa{finite}.
421 %\end{warn}
422 \index{sets|)}
425 \section{Functions}
427 \index{functions|(}%
428 This section describes a few concepts that involve
429 functions.  Some of the more important theorems are given along with the
430 names. A few sample proofs appear. Unlike with set theory, however,
431 we cannot simply state lemmas and expect them to be proved using
432 \isa{blast}.
434 \subsection{Function Basics}
436 Two functions are \textbf{equal}\indexbold{equality!of functions}
437 if they yield equal results given equal
438 arguments.  This is the principle of
439 \textbf{extensionality}\indexbold{extensionality!for functions} for
440 functions:
441 \begin{isabelle}
442 ({\isasymAnd}x.\ f\ x\ =\ g\ x)\ {\isasymLongrightarrow}\ f\ =\ g
443 \rulenamedx{ext}
444 \end{isabelle}
446 \indexbold{updating a function}%
447 Function \textbf{update} is useful for modelling machine states. It has
448 the obvious definition and many useful facts are proved about
449 it.  In particular, the following equation is installed as a simplification
450 rule:
451 \begin{isabelle}
452 (f(x:=y))\ z\ =\ (if\ z\ =\ x\ then\ y\ else\ f\ z)
453 \rulename{fun_upd_apply}
454 \end{isabelle}
455 Two syntactic points must be noted.  In
456 \isa{(f(x:=y))\ z} we are applying an updated function to an
457 argument; the outer parentheses are essential.  A series of two or more
458 updates can be abbreviated as shown on the left-hand side of this theorem:
459 \begin{isabelle}
460 f(x:=y,\ x:=z)\ =\ f(x:=z)
461 \rulename{fun_upd_upd}
462 \end{isabelle}
463 Note also that we can write \isa{f(x:=z)} with only one pair of parentheses
464 when it is not being applied to an argument.
466 \medskip
467 The \bfindex{identity function} and function
468 \textbf{composition}\indexbold{composition!of functions} are
469 defined:
470 \begin{isabelle}%
471 id\ \isasymequiv\ {\isasymlambda}x.\ x%
472 \rulenamedx{id_def}\isanewline
473 f\ \isasymcirc\ g\ \isasymequiv\
474 {\isasymlambda}x.\ f\
475 (g\ x)%
476 \rulenamedx{o_def}
477 \end{isabelle}
478 %
479 Many familiar theorems concerning the identity and composition
480 are proved. For example, we have the associativity of composition:
481 \begin{isabelle}
482 f\ \isasymcirc\ (g\ \isasymcirc\ h)\ =\ f\ \isasymcirc\ g\ \isasymcirc\ h
483 \rulename{o_assoc}
484 \end{isabelle}
486 \subsection{Injections, Surjections, Bijections}
488 \index{injections}\index{surjections}\index{bijections}%
489 A function may be \textbf{injective}, \textbf{surjective} or \textbf{bijective}:
490 \begin{isabelle}
491 inj_on\ f\ A\ \isasymequiv\ {\isasymforall}x\isasymin A.\
492 {\isasymforall}y\isasymin  A.\ f\ x\ =\ f\ y\ \isasymlongrightarrow\ x\
493 =\ y%
494 \rulenamedx{inj_on_def}\isanewline
495 surj\ f\ \isasymequiv\ {\isasymforall}y.\
496 \isasymexists x.\ y\ =\ f\ x%
497 \rulenamedx{surj_def}\isanewline
498 bij\ f\ \isasymequiv\ inj\ f\ \isasymand\ surj\ f
499 \rulenamedx{bij_def}
500 \end{isabelle}
501 The second argument
502 of \isa{inj_on} lets us express that a function is injective over a
503 given set. This refinement is useful in higher-order logic, where
504 functions are total; in some cases, a function's natural domain is a subset
505 of its domain type.  Writing \isa{inj\ f} abbreviates \isa{inj_on\ f\
506 UNIV}, for when \isa{f} is injective everywhere.
508 The operator \isa{inv} expresses the
509 \textbf{inverse}\indexbold{inverse!of a function}
510 of a function. In
511 general the inverse may not be well behaved.  We have the usual laws,
512 such as these:
513 \begin{isabelle}
514 inj\ f\ \ \isasymLongrightarrow\ inv\ f\ (f\ x)\ =\ x%
515 \rulename{inv_f_f}\isanewline
516 surj\ f\ \isasymLongrightarrow\ f\ (inv\ f\ y)\ =\ y
517 \rulename{surj_f_inv_f}\isanewline
518 bij\ f\ \ \isasymLongrightarrow\ inv\ (inv\ f)\ =\ f
519 \rulename{inv_inv_eq}
520 \end{isabelle}
521 %
522 %Other useful facts are that the inverse of an injection
523 %is a surjection and vice versa; the inverse of a bijection is
524 %a bijection.
525 %\begin{isabelle}
526 %inj\ f\ \isasymLongrightarrow\ surj\
527 %(inv\ f)
528 %\rulename{inj_imp_surj_inv}\isanewline
529 %surj\ f\ \isasymLongrightarrow\ inj\ (inv\ f)
530 %\rulename{surj_imp_inj_inv}\isanewline
531 %bij\ f\ \isasymLongrightarrow\ bij\ (inv\ f)
532 %\rulename{bij_imp_bij_inv}
533 %\end{isabelle}
534 %
535 %The converses of these results fail.  Unless a function is
536 %well behaved, little can be said about its inverse. Here is another
537 %law:
538 %\begin{isabelle}
539 %{\isasymlbrakk}bij\ f;\ bij\ g\isasymrbrakk\ \isasymLongrightarrow\ inv\ (f\ \isasymcirc\ g)\ =\ inv\ g\ \isasymcirc\ inv\ f%
540 %\rulename{o_inv_distrib}
541 %\end{isabelle}
543 Theorems involving these concepts can be hard to prove. The following
544 example is easy, but it cannot be proved automatically. To begin
545 with, we need a law that relates the equality of functions to
546 equality over all arguments:
547 \begin{isabelle}
548 (f\ =\ g)\ =\ ({\isasymforall}x.\ f\ x\ =\ g\ x)
549 \rulename{fun_eq_iff}
550 \end{isabelle}
551 %
552 This is just a restatement of
553 extensionality.\indexbold{extensionality!for functions}
554 Our lemma
555 states  that an injection can be cancelled from the left  side of
556 function composition:
557 \begin{isabelle}
558 \isacommand{lemma}\ "inj\ f\ \isasymLongrightarrow\ (f\ o\ g\ =\ f\ o\ h)\ =\ (g\ =\ h)"\isanewline
559 \isacommand{apply}\ (simp\ add:\ fun_eq_iff\ inj_on_def)\isanewline
560 \isacommand{apply}\ auto\isanewline
561 \isacommand{done}
562 \end{isabelle}
564 The first step of the proof invokes extensionality and the definitions
565 of injectiveness and composition. It leaves one subgoal:
566 \begin{isabelle}
567 \ 1.\ {\isasymforall}x\ y.\ f\ x\ =\ f\ y\ \isasymlongrightarrow\ x\ =\ y\
568 \isasymLongrightarrow\isanewline
569 \ \ \ \ ({\isasymforall}x.\ f\ (g\ x)\ =\ f\ (h\ x))\ =\ ({\isasymforall}x.\ g\ x\ =\ h\ x)
570 \end{isabelle}
571 This can be proved using the \isa{auto} method.
574 \subsection{Function Image}
576 The \textbf{image}\indexbold{image!under a function}
577 of a set under a function is a most useful notion.  It
578 has the obvious definition:
579 \begin{isabelle}
580 f\ \ A\ \isasymequiv\ \isacharbraceleft y.\ \isasymexists x\isasymin
581 A.\ y\ =\ f\ x\isacharbraceright
582 \rulenamedx{image_def}
583 \end{isabelle}
584 %
585 Here are some of the many facts proved about image:
586 \begin{isabelle}
587 (f\ \isasymcirc\ g)\ \ r\ =\ f\ \ g\ \ r
588 \rulename{image_compose}\isanewline
589 f(A\ \isasymunion\ B)\ =\ fA\ \isasymunion\ fB
590 \rulename{image_Un}\isanewline
591 inj\ f\ \isasymLongrightarrow\ f(A\ \isasyminter\
592 B)\ =\ fA\ \isasyminter\ fB
593 \rulename{image_Int}
594 %\isanewline
595 %bij\ f\ \isasymLongrightarrow\ f\ \ (-\ A)\ =\ -\ f\ \ A%
596 %\rulename{bij_image_Compl_eq}
597 \end{isabelle}
600 Laws involving image can often be proved automatically. Here
601 are two examples, illustrating connections with indexed union and with the
602 general syntax for comprehension:
603 \begin{isabelle}
604 \isacommand{lemma}\ "fA\ \isasymunion\ gA\ =\ ({\isasymUnion}x{\isasymin}A.\ \isacharbraceleft f\ x,\ g\
605 x\isacharbraceright)"
606 \par\smallskip
607 \isacommand{lemma}\ "f\ \ \isacharbraceleft(x,y){.}\ P\ x\ y\isacharbraceright\ =\ \isacharbraceleft f(x,y)\ \isacharbar\ x\ y.\ P\ x\
608 y\isacharbraceright"
609 \end{isabelle}
611 \medskip
612 \index{range!of a function}%
613 A function's \textbf{range} is the set of values that the function can
614 take on. It is, in fact, the image of the universal set under
615 that function. There is no constant \isa{range}.  Instead,
616 \sdx{range}  abbreviates an application of image to \isa{UNIV}:
617 \begin{isabelle}
618 \ \ \ \ \ range\ f\
619 {\isasymrightleftharpoons}\ fUNIV
620 \end{isabelle}
621 %
622 Few theorems are proved specifically
623 for {\isa{range}}; in most cases, you should look for a more general
624 theorem concerning images.
626 \medskip
627 \textbf{Inverse image}\index{inverse image!of a function} is also  useful.
628 It is defined as follows:
629 \begin{isabelle}
630 f\ -\ B\ \isasymequiv\ \isacharbraceleft x.\ f\ x\ \isasymin\ B\isacharbraceright
631 \rulenamedx{vimage_def}
632 \end{isabelle}
633 %
634 This is one of the facts proved about it:
635 \begin{isabelle}
636 f\ -\ (-\ A)\ =\ -\ f\ -\ A%
637 \rulename{vimage_Compl}
638 \end{isabelle}
639 \index{functions|)}
642 \section{Relations}
643 \label{sec:Relations}
645 \index{relations|(}%
646 A \textbf{relation} is a set of pairs.  As such, the set operations apply
647 to them.  For instance, we may form the union of two relations.  Other
648 primitives are defined specifically for relations.
650 \subsection{Relation Basics}
652 The \bfindex{identity relation}, also known as equality, has the obvious
653 definition:
654 \begin{isabelle}
655 Id\ \isasymequiv\ \isacharbraceleft p.\ \isasymexists x.\ p\ =\ (x,x){\isacharbraceright}%
656 \rulenamedx{Id_def}
657 \end{isabelle}
659 \indexbold{composition!of relations}%
660 \textbf{Composition} of relations (the infix \sdx{O}) is also
661 available:
662 \begin{isabelle}
663 r\ O\ s\ \isasymequiv\ \isacharbraceleft(x,z).\ \isasymexists y.\ (x,y)\ \isasymin\ s\ \isasymand\ (y,z)\ \isasymin\ r\isacharbraceright
664 \rulenamedx{rel_comp_def}
665 \end{isabelle}
666 %
667 This is one of the many lemmas proved about these concepts:
668 \begin{isabelle}
669 R\ O\ Id\ =\ R
670 \rulename{R_O_Id}
671 \end{isabelle}
672 %
673 Composition is monotonic, as are most of the primitives appearing
674 in this chapter.  We have many theorems similar to the following
675 one:
676 \begin{isabelle}
677 \isasymlbrakk r\isacharprime\ \isasymsubseteq\ r;\ s\isacharprime\
678 \isasymsubseteq\ s\isasymrbrakk\ \isasymLongrightarrow\ r\isacharprime\ O\
679 s\isacharprime\ \isasymsubseteq\ r\ O\ s%
680 \rulename{rel_comp_mono}
681 \end{isabelle}
683 \indexbold{converse!of a relation}%
684 \indexbold{inverse!of a relation}%
685 The \textbf{converse} or inverse of a
686 relation exchanges the roles  of the two operands.  We use the postfix
687 notation~\isa{r\isasyminverse} or
688 \isa{r\isacharcircum-1} in ASCII\@.
689 \begin{isabelle}
690 ((a,b)\ \isasymin\ r\isasyminverse)\ =\
691 ((b,a)\ \isasymin\ r)
692 \rulenamedx{converse_iff}
693 \end{isabelle}
694 %
695 Here is a typical law proved about converse and composition:
696 \begin{isabelle}
697 (r\ O\ s)\isasyminverse\ =\ s\isasyminverse\ O\ r\isasyminverse
698 \rulename{converse_rel_comp}
699 \end{isabelle}
701 \indexbold{image!under a relation}%
702 The \textbf{image} of a set under a relation is defined
703 analogously  to image under a function:
704 \begin{isabelle}
705 (b\ \isasymin\ r\ \ A)\ =\ (\isasymexists x\isasymin
706 A.\ (x,b)\ \isasymin\ r)
707 \rulenamedx{Image_iff}
708 \end{isabelle}
709 It satisfies many similar laws.
711 \index{domain!of a relation}%
712 \index{range!of a relation}%
713 The \textbf{domain} and \textbf{range} of a relation are defined in the
714 standard way:
715 \begin{isabelle}
716 (a\ \isasymin\ Domain\ r)\ =\ (\isasymexists y.\ (a,y)\ \isasymin\
717 r)
718 \rulenamedx{Domain_iff}%
719 \isanewline
720 (a\ \isasymin\ Range\ r)\
721 \ =\ (\isasymexists y.\
722 (y,a)\
723 \isasymin\ r)
724 \rulenamedx{Range_iff}
725 \end{isabelle}
727 Iterated composition of a relation is available.  The notation overloads
728 that of exponentiation.  Two simplification rules are installed:
729 \begin{isabelle}
730 R\ \isacharcircum\ \isadigit{0}\ =\ Id\isanewline
731 R\ \isacharcircum\ Suc\ n\ =\ R\ O\ R\isacharcircum n
732 \end{isabelle}
734 \subsection{The Reflexive and Transitive Closure}
736 \index{reflexive and transitive closure|(}%
737 The \textbf{reflexive and transitive closure} of the
738 relation~\isa{r} is written with a
739 postfix syntax.  In ASCII we write \isa{r\isacharcircum*} and in
740 symbol notation~\isa{r\isactrlsup *}.  It is the least solution of the
741 equation
742 \begin{isabelle}
743 r\isactrlsup *\ =\ Id\ \isasymunion \ (r\ O\ r\isactrlsup *)
744 \rulename{rtrancl_unfold}
745 \end{isabelle}
746 %
747 Among its basic properties are three that serve as introduction
748 rules:
749 \begin{isabelle}
750 (a,\ a)\ \isasymin \ r\isactrlsup *
751 \rulenamedx{rtrancl_refl}\isanewline
752 p\ \isasymin \ r\ \isasymLongrightarrow \ p\ \isasymin \ r\isactrlsup *
753 \rulenamedx{r_into_rtrancl}\isanewline
754 \isasymlbrakk (a,b)\ \isasymin \ r\isactrlsup *;\
755 (b,c)\ \isasymin \ r\isactrlsup *\isasymrbrakk \ \isasymLongrightarrow \
756 (a,c)\ \isasymin \ r\isactrlsup *
757 \rulenamedx{rtrancl_trans}
758 \end{isabelle}
759 %
760 Induction over the reflexive transitive closure is available:
761 \begin{isabelle}
762 \isasymlbrakk (a,\ b)\ \isasymin \ r\isactrlsup *;\ P\ a;\ \isasymAnd y\ z.\ \isasymlbrakk (a,\ y)\ \isasymin \ r\isactrlsup *;\ (y,\ z)\ \isasymin \ r;\ P\ y\isasymrbrakk \ \isasymLongrightarrow \ P\ z\isasymrbrakk \isanewline
763 \isasymLongrightarrow \ P\ b%
764 \rulename{rtrancl_induct}
765 \end{isabelle}
766 %
767 Idempotence is one of the laws proved about the reflexive transitive
768 closure:
769 \begin{isabelle}
770 (r\isactrlsup *)\isactrlsup *\ =\ r\isactrlsup *
771 \rulename{rtrancl_idemp}
772 \end{isabelle}
774 \smallskip
775 The transitive closure is similar.  The ASCII syntax is
776 \isa{r\isacharcircum+}.  It has two  introduction rules:
777 \begin{isabelle}
778 p\ \isasymin \ r\ \isasymLongrightarrow \ p\ \isasymin \ r\isactrlsup +
779 \rulenamedx{r_into_trancl}\isanewline
780 \isasymlbrakk (a,\ b)\ \isasymin \ r\isactrlsup +;\ (b,\ c)\ \isasymin \ r\isactrlsup +\isasymrbrakk \ \isasymLongrightarrow \ (a,\ c)\ \isasymin \ r\isactrlsup +
781 \rulenamedx{trancl_trans}
782 \end{isabelle}
783 %
784 The induction rule resembles the one shown above.
785 A typical lemma states that transitive closure commutes with the converse
786 operator:
787 \begin{isabelle}
788 (r\isasyminverse )\isactrlsup +\ =\ (r\isactrlsup +)\isasyminverse
789 \rulename{trancl_converse}
790 \end{isabelle}
792 \subsection{A Sample Proof}
794 The reflexive transitive closure also commutes with the converse
795 operator.  Let us examine the proof. Each direction of the equivalence
796 is  proved separately. The two proofs are almost identical. Here
797 is the first one:
798 \begin{isabelle}
799 \isacommand{lemma}\ rtrancl_converseD:\ "(x,y)\ \isasymin \
800 (r\isasyminverse)\isactrlsup *\ \isasymLongrightarrow \ (y,x)\ \isasymin
801 \ r\isactrlsup *"\isanewline
802 \isacommand{apply}\ (erule\ rtrancl_induct)\isanewline
803 \ \isacommand{apply}\ (rule\ rtrancl_refl)\isanewline
804 \isacommand{apply}\ (blast\ intro:\ rtrancl_trans)\isanewline
805 \isacommand{done}
806 \end{isabelle}
807 %
808 The first step of the proof applies induction, leaving these subgoals:
809 \begin{isabelle}
810 \ 1.\ (x,\ x)\ \isasymin \ r\isactrlsup *\isanewline
811 \ 2.\ \isasymAnd y\ z.\ \isasymlbrakk (x,y)\ \isasymin \
812 (r\isasyminverse)\isactrlsup *;\ (y,z)\ \isasymin \ r\isasyminverse ;\
813 (y,x)\ \isasymin \ r\isactrlsup *\isasymrbrakk \isanewline
814 \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (z,x)\ \isasymin \ r\isactrlsup *
815 \end{isabelle}
816 %
817 The first subgoal is trivial by reflexivity. The second follows
818 by first eliminating the converse operator, yielding the
819 assumption \isa{(z,y)\
820 \isasymin\ r}, and then
821 applying the introduction rules shown above.  The same proof script handles
822 the other direction:
823 \begin{isabelle}
824 \isacommand{lemma}\ rtrancl_converseI:\ "(y,x)\ \isasymin \ r\isactrlsup *\ \isasymLongrightarrow \ (x,y)\ \isasymin \ (r\isasyminverse)\isactrlsup *"\isanewline
825 \isacommand{apply}\ (erule\ rtrancl_induct)\isanewline
826 \ \isacommand{apply}\ (rule\ rtrancl_refl)\isanewline
827 \isacommand{apply}\ (blast\ intro:\ rtrancl_trans)\isanewline
828 \isacommand{done}
829 \end{isabelle}
832 Finally, we combine the two lemmas to prove the desired equation:
833 \begin{isabelle}
834 \isacommand{lemma}\ rtrancl_converse:\ "(r\isasyminverse)\isactrlsup *\ =\ (r\isactrlsup *)\isasyminverse"\isanewline
835 \isacommand{by}\ (auto\ intro:\ rtrancl_converseI\ dest:\
836 rtrancl_converseD)
837 \end{isabelle}
839 \begin{warn}
840 This trivial proof requires \isa{auto} rather than \isa{blast} because
841 of a subtle issue involving ordered pairs.  Here is a subgoal that
842 arises internally after  the rules
843 \isa{equalityI} and \isa{subsetI} have been applied:
844 \begin{isabelle}
845 \ 1.\ \isasymAnd x.\ x\ \isasymin \ (r\isasyminverse )\isactrlsup *\ \isasymLongrightarrow \ x\ \isasymin \ (r\isactrlsup
846 *)\isasyminverse
847 %ignore subgoal 2
848 %\ 2.\ \isasymAnd x.\ x\ \isasymin \ (r\isactrlsup *)\isasyminverse \
849 %\isasymLongrightarrow \ x\ \isasymin \ (r\isasyminverse )\isactrlsup *
850 \end{isabelle}
851 \par\noindent
852 We cannot apply \isa{rtrancl_converseD}\@.  It refers to
853 ordered pairs, while \isa{x} is a variable of product type.
854 The \isa{simp} and \isa{blast} methods can do nothing, so let us try
855 \isa{clarify}:
856 \begin{isabelle}
857 \ 1.\ \isasymAnd a\ b.\ (a,b)\ \isasymin \ (r\isasyminverse )\isactrlsup *\ \isasymLongrightarrow \ (b,a)\ \isasymin \ r\isactrlsup
858 *
859 \end{isabelle}
860 Now that \isa{x} has been replaced by the pair \isa{(a,b)}, we can
861 proceed.  Other methods that split variables in this way are \isa{force},
862 \isa{auto}, \isa{fast} and \isa{best}.  Section~\ref{sec:products} will discuss proof
863 techniques for ordered pairs in more detail.
864 \end{warn}
865 \index{relations|)}\index{reflexive and transitive closure|)}
868 \section{Well-Founded Relations and Induction}
869 \label{sec:Well-founded}
871 \index{relations!well-founded|(}%
872 A well-founded relation captures the notion of a terminating
873 process. Complex recursive functions definitions must specify a
874 well-founded relation that justifies their
875 termination~\cite{isabelle-function}. Most of the forms of induction found
876 in mathematics are merely special cases of induction over a
877 well-founded relation.
879 Intuitively, the relation~$\prec$ is \textbf{well-founded} if it admits no
880 infinite  descending chains
881 $\cdots \prec a@2 \prec a@1 \prec a@0.$
882 Well-foundedness can be hard to show. The various
883 formulations are all complicated.  However,  often a relation
884 is well-founded by construction.  HOL provides
885 theorems concerning ways of constructing  a well-founded relation.  The
886 most familiar way is to specify a
887 \index{measure functions}\textbf{measure function}~\isa{f} into
888 the natural numbers, when $\isa{x}\prec \isa{y}\iff \isa{f x} < \isa{f y}$;
889 we write this particular relation as
890 \isa{measure~f}.
892 \begin{warn}
893 You may want to skip the rest of this section until you need to perform a
894 complex recursive function definition or induction.  The induction rule
895 returned by
896 \isacommand{fun} is good enough for most purposes.  We use an explicit
897 well-founded induction only in {\S}\ref{sec:CTL-revisited}.
898 \end{warn}
900 Isabelle/HOL declares \cdx{less_than} as a relation object,
901 that is, a set of pairs of natural numbers. Two theorems tell us that this
902 relation  behaves as expected and that it is well-founded:
903 \begin{isabelle}
904 ((x,y)\ \isasymin\ less_than)\ =\ (x\ <\ y)
905 \rulenamedx{less_than_iff}\isanewline
906 wf\ less_than
907 \rulenamedx{wf_less_than}
908 \end{isabelle}
910 The notion of measure generalizes to the
911 \index{inverse image!of a relation}\textbf{inverse image} of
912 a relation. Given a relation~\isa{r} and a function~\isa{f}, we express  a
913 new relation using \isa{f} as a measure.  An infinite descending chain on
914 this new relation would give rise to an infinite descending chain
915 on~\isa{r}.  Isabelle/HOL defines this concept and proves a
916 theorem stating that it preserves well-foundedness:
917 \begin{isabelle}
918 inv_image\ r\ f\ \isasymequiv\ \isacharbraceleft(x,y).\ (f\ x,\ f\ y)\
919 \isasymin\ r\isacharbraceright
920 \rulenamedx{inv_image_def}\isanewline
921 wf\ r\ \isasymLongrightarrow\ wf\ (inv_image\ r\ f)
922 \rulenamedx{wf_inv_image}
923 \end{isabelle}
925 A measure function involves the natural numbers.  The relation \isa{measure
926 size} justifies primitive recursion and structural induction over a
927 datatype.  Isabelle/HOL defines
928 \isa{measure} as shown:
929 \begin{isabelle}
930 measure\ \isasymequiv\ inv_image\ less_than%
931 \rulenamedx{measure_def}\isanewline
932 wf\ (measure\ f)
933 \rulenamedx{wf_measure}
934 \end{isabelle}
936 Of the other constructions, the most important is the
937 \bfindex{lexicographic product} of two relations. It expresses the
938 standard dictionary  ordering over pairs.  We write \isa{ra\ <*lex*>\
939 rb}, where \isa{ra} and \isa{rb} are the two operands.  The
940 lexicographic product satisfies the usual  definition and it preserves
941 well-foundedness:
942 \begin{isabelle}
943 ra\ <*lex*>\ rb\ \isasymequiv \isanewline
944 \ \ \isacharbraceleft ((a,b),(a',b')).\ (a,a')\ \isasymin \ ra\
945 \isasymor\isanewline
946 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \,a=a'\ \isasymand \ (b,b')\
947 \isasymin \ rb\isacharbraceright
948 \rulenamedx{lex_prod_def}%
949 \par\smallskip
950 \isasymlbrakk wf\ ra;\ wf\ rb\isasymrbrakk \ \isasymLongrightarrow \ wf\ (ra\ <*lex*>\ rb)
951 \rulenamedx{wf_lex_prod}
952 \end{isabelle}
954 %These constructions can be used in a
955 %\textbf{recdef} declaration ({\S}\ref{sec:recdef-simplification}) to define
956 %the well-founded relation used to prove termination.
958 The \bfindex{multiset ordering}, useful for hard termination proofs, is
959 available in the Library~\cite{HOL-Library}.
960 Baader and Nipkow \cite[{\S}2.5]{Baader-Nipkow} discuss it.
962 \medskip
963 Induction\index{induction!well-founded|(}
964 comes in many forms,
965 including traditional mathematical  induction, structural induction on
966 lists and induction on size.  All are instances of the following rule,
967 for a suitable well-founded relation~$\prec$:
968 $\infer{P(a)}{\infer*{P(x)}{[\forall y.\, y\prec x \imp P(y)]}}$
969 To show $P(a)$ for a particular term~$a$, it suffices to show $P(x)$ for
970 arbitrary~$x$ under the assumption that $P(y)$ holds for $y\prec x$.
971 Intuitively, the well-foundedness of $\prec$ ensures that the chains of
972 reasoning are finite.
974 \smallskip
975 In Isabelle, the induction rule is expressed like this:
976 \begin{isabelle}
977 {\isasymlbrakk}wf\ r;\
978   {\isasymAnd}x.\ {\isasymforall}y.\ (y,x)\ \isasymin\ r\
979 \isasymlongrightarrow\ P\ y\ \isasymLongrightarrow\ P\ x\isasymrbrakk\
980 \isasymLongrightarrow\ P\ a
981 \rulenamedx{wf_induct}
982 \end{isabelle}
983 Here \isa{wf\ r} expresses that the relation~\isa{r} is well-founded.
985 Many familiar induction principles are instances of this rule.
986 For example, the predecessor relation on the natural numbers
987 is well-founded; induction over it is mathematical induction.
988 The `tail of'' relation on lists is well-founded; induction over
989 it is structural induction.%
990 \index{induction!well-founded|)}%
991 \index{relations!well-founded|)}
994 \section{Fixed Point Operators}
996 \index{fixed points|(}%
997 Fixed point operators define sets
998 recursively.  They are invoked implicitly when making an inductive
999 definition, as discussed in Chap.\ts\ref{chap:inductive} below.  However,
1000 they can be used directly, too. The
1001 \emph{least}  or \emph{strongest} fixed point yields an inductive
1002 definition;  the \emph{greatest} or \emph{weakest} fixed point yields a
1003 coinductive  definition.  Mathematicians may wish to note that the
1004 existence  of these fixed points is guaranteed by the Knaster-Tarski
1005 theorem.
1007 \begin{warn}
1008 Casual readers should skip the rest of this section.  We use fixed point
1009 operators only in {\S}\ref{sec:VMC}.
1010 \end{warn}
1012 The theory applies only to monotonic functions.\index{monotone functions|bold}
1013 Isabelle's definition of monotone is overloaded over all orderings:
1014 \begin{isabelle}
1015 mono\ f\ \isasymequiv\ {\isasymforall}A\ B.\ A\ \isasymle\ B\ \isasymlongrightarrow\ f\ A\ \isasymle\ f\ B%
1016 \rulenamedx{mono_def}
1017 \end{isabelle}
1018 %
1019 For fixed point operators, the ordering will be the subset relation: if
1020 $A\subseteq B$ then we expect $f(A)\subseteq f(B)$.  In addition to its
1021 definition, monotonicity has the obvious introduction and destruction
1022 rules:
1023 \begin{isabelle}
1024 ({\isasymAnd}A\ B.\ A\ \isasymle\ B\ \isasymLongrightarrow\ f\ A\ \isasymle\ f\ B)\ \isasymLongrightarrow\ mono\ f%
1025 \rulename{monoI}%
1026 \par\smallskip%          \isanewline didn't leave enough space
1027 {\isasymlbrakk}mono\ f;\ A\ \isasymle\ B\isasymrbrakk\
1028 \isasymLongrightarrow\ f\ A\ \isasymle\ f\ B%
1029 \rulename{monoD}
1030 \end{isabelle}
1032 The most important properties of the least fixed point are that
1033 it is a fixed point and that it enjoys an induction rule:
1034 \begin{isabelle}
1035 mono\ f\ \isasymLongrightarrow\ lfp\ f\ =\ f\ (lfp\ f)
1036 \rulename{lfp_unfold}%
1037 \par\smallskip%          \isanewline didn't leave enough space
1038 {\isasymlbrakk}a\ \isasymin\ lfp\ f;\ mono\ f;\isanewline
1039   \ {\isasymAnd}x.\ x\
1040 \isasymin\ f\ (lfp\ f\ \isasyminter\ \isacharbraceleft x.\ P\
1041 x\isacharbraceright)\ \isasymLongrightarrow\ P\ x\isasymrbrakk\
1042 \isasymLongrightarrow\ P\ a%
1043 \rulename{lfp_induct}
1044 \end{isabelle}
1045 %
1046 The induction rule shown above is more convenient than the basic
1047 one derived from the minimality of {\isa{lfp}}.  Observe that both theorems
1048 demand \isa{mono\ f} as a premise.
1050 The greatest fixed point is similar, but it has a \bfindex{coinduction} rule:
1051 \begin{isabelle}
1052 mono\ f\ \isasymLongrightarrow\ gfp\ f\ =\ f\ (gfp\ f)
1053 \rulename{gfp_unfold}%
1054 \isanewline
1055 {\isasymlbrakk}mono\ f;\ a\ \isasymin\ X;\ X\ \isasymsubseteq\ f\ (X\
1056 \isasymunion\ gfp\ f)\isasymrbrakk\ \isasymLongrightarrow\ a\ \isasymin\
1057 gfp\ f%
1058 \rulename{coinduct}
1059 \end{isabelle}
1060 A \textbf{bisimulation}\index{bisimulations}
1061 is perhaps the best-known concept defined as a
1062 greatest fixed point.  Exhibiting a bisimulation to prove the equality of
1063 two agents in a process algebra is an example of coinduction.
1064 The coinduction rule can be strengthened in various ways.
1065 \index{fixed points|)}
1067 %The section "Case Study: Verified Model Checking" is part of this chapter
1068 \input{CTL/ctl}
1069 \endinput