10341

1 
% ID: $Id$

10303

2 
\chapter{Sets, Functions and Relations}


3 


4 
Mathematics relies heavily on set theory: not just unions and intersections


5 
but least fixed points and other concepts. In computer science, sets are


6 
used to formalize grammars, state transition systems, etc. The set theory


7 
of Isabelle/HOL should not be confused with traditional, untyped set


8 
theory, in which everything is a set. There the slogan is `set theory is


9 
the foundation of mathematics.' Our sets are typed. In a given set, all


10 
elements have the same type, say


11 
\isa{T}, and the set itself has type \isa{T set}. Sets are typed in the


12 
same way as lists.


13 


14 
Relations are simply sets of pairs. This chapter describes


15 
the main operations on relations, such as converse, composition and


16 
transitive closure. Functions are also covered below. They are not sets in


17 
Isabelle/HOL, but (for example) the range of a function is a set,


18 
and the inverse image of a function maps sets to sets.


19 


20 
This chapter ends with a case study concerning model checking for the


21 
temporal logic CTL\@. Most of the other examples are simple. The


22 
chapter presents a small selection of builtin theorems in order to point


23 
out some key properties of the various constants and to introduce you to


24 
the notation.


25 


26 
Natural deduction rules are provided for the set theory constants, but they


27 
are seldom used directly, so only a few are presented here. Many formulas


28 
involving sets can be proved automatically or simplified to a great extent.


29 
Expressing your concepts in terms of sets will probably make your proofs


30 
easier.


31 


32 


33 
\section{Sets}


34 


35 
We begin with \textbf{intersection}, \textbf{union} and \textbf{complement} (denoted


36 
by a minus sign). In addition to the \textbf{membership} relation, there


37 
is a symbol for its negation. These points can be seen below.


38 


39 
Here are the natural deduction rules for intersection. Note the


40 
resemblance to those for conjunction.


41 
\begin{isabelle}


42 
\isasymlbrakk c\ \isasymin\


43 
A;\ c\ \isasymin\


44 
B\isasymrbrakk\ \isasymLongrightarrow\ c\


45 
\isasymin\ A\ \isasyminter\ B%


46 
\rulename{IntI}\isanewline


47 
c\ \isasymin\ A\ \isasyminter\


48 
B\ \isasymLongrightarrow\ c\ \isasymin\


49 
A%


50 
\rulename{IntD1}\isanewline


51 
c\ \isasymin\ A\ \isasyminter\


52 
B\ \isasymLongrightarrow\ c\ \isasymin\


53 
B%


54 
\rulename{IntD2}%


55 
\end{isabelle}


56 


57 
Here are two of the many installed theorems concerning set complement:


58 
\begin{isabelle}


59 
(c\ \isasymin\ \isacharminus\ A)\ =\ (c\ \isasymnotin\ A)


60 
\rulename{Compl_iff}\isanewline


61 
\isacharminus\ (A\ \isasymunion\


62 
B)\ =\ \isacharminus\


63 
A\ \isasyminter\ \isacharminus\ B


64 
\rulename{Compl_Un}


65 
\end{isabelle}


66 


67 
Set \textbf{difference} means the same thing as intersection with the


68 
complement of another set. Here we also see the syntax for the


69 
empty set and for the universal set.


70 
\begin{isabelle}


71 
A\ \isasyminter\ (B\


72 
\isacharminus\ A)\ =\


73 
\isacharbraceleft{\isacharbraceright}


74 
\rulename{Diff_disjoint}%


75 
\isanewline


76 
A\ \isasymunion\ \isacharminus\ A\


77 
=\ UNIV%


78 
\rulename{Compl_partition}


79 
\end{isabelle}


80 


81 
The \textbf{subset} relation holds between two sets just if every element


82 
of one is also an element of the other. This relation is reflexive. These


83 
are its natural deduction rules:


84 
\begin{isabelle}


85 
({\isasymAnd}x.\ x\ \isasymin\ A\ \isasymLongrightarrow\ x\ \isasymin\ B)\ \isasymLongrightarrow\ A\ \isasymsubseteq\ B%


86 
\rulename{subsetI}%


87 
\par\smallskip% \isanewline didn't leave enough space


88 
\isasymlbrakk A\ \isasymsubseteq\ B;\ c\ \isasymin\


89 
A\isasymrbrakk\ \isasymLongrightarrow\ c\


90 
\isasymin\ B%


91 
\rulename{subsetD}


92 
\end{isabelle}


93 
In harder proofs, you may need to apply \isa{subsetD} giving a specific term


94 
for~\isa{c}. However, \isa{blast} can instantly prove facts such as this


95 
one:


96 
\begin{isabelle}


97 
(A\ \isasymunion\ B\


98 
\isasymsubseteq\ C)\ =\


99 
(A\ \isasymsubseteq\ C\


100 
\isasymand\ B\ \isasymsubseteq\


101 
C)


102 
\rulename{Un_subset_iff}


103 
\end{isabelle}


104 
Here is another example, also proved automatically:


105 
\begin{isabelle}


106 
\isacommand{lemma}\ "(A\


107 
\isasymsubseteq\ B)\ =\


108 
(B\ \isasymsubseteq\


109 
A)"\isanewline


110 
\isacommand{apply}\ (blast)\isanewline


111 
\isacommand{done}


112 
\end{isabelle}


113 
%


114 
This is the same example using ASCII syntax, illustrating a pitfall:


115 
\begin{isabelle}


116 
\isacommand{lemma}\ "(A\ \isacharless=\ B)\ =\ (B\ \isacharless=\


117 
A)"


118 
\end{isabelle}


119 
%


120 
The proof fails. It is not a statement about sets, due to overloading;


121 
the relation symbol~\isa{<=} can be any relation, not just


122 
subset.


123 
In this general form, the statement is not valid. Putting


124 
in a type constraint forces the variables to denote sets, allowing the


125 
proof to succeed:


126 


127 
\begin{isabelle}


128 
\isacommand{lemma}\ "((A::\ {\isacharprime}a\ set)\ \isacharless=\ B)\ =\ (B\ \isacharless=\


129 
A)"


130 
\end{isabelle}


131 
Incidentally, \isa{A\ \isasymsubseteq\ B} asserts that


132 
the sets \isa{A} and \isa{B} are disjoint.


133 


134 
\medskip


135 
Two sets are \textbf{equal} if they contain the same elements.


136 
This is


137 
the principle of \textbf{extensionality} for sets.


138 
\begin{isabelle}


139 
({\isasymAnd}x.\ (x\ {\isasymin}\ A)\ =\ (x\ {\isasymin}\ B))\


140 
{\isasymLongrightarrow}\ A\ =\ B


141 
\rulename{set_ext}


142 
\end{isabelle}


143 
Extensionality is often expressed as


144 
$A=B\iff A\subseteq B\conj B\subseteq A$.


145 
The following rules express both


146 
directions of this equivalence. Proving a set equation using


147 
\isa{equalityI} allows the two inclusions to be proved independently.


148 
\begin{isabelle}


149 
\isasymlbrakk A\ \isasymsubseteq\ B;\ B\ \isasymsubseteq\


150 
A\isasymrbrakk\ \isasymLongrightarrow\ A\ =\ B%


151 
\rulename{equalityI}


152 
\par\smallskip% \isanewline didn't leave enough space


153 
\isasymlbrakk A\ =\ B;\ \isasymlbrakk A\ \isasymsubseteq\ B;\ B\


154 
\isasymsubseteq\ A\isasymrbrakk\ \isasymLongrightarrow\ P\isasymrbrakk\


155 
\isasymLongrightarrow\ P%


156 
\rulename{equalityE}


157 
\end{isabelle}


158 


159 


160 
\subsection{Finite set notation}


161 


162 
Finite sets are expressed using the constant {\isa{insert}}, which is


163 
closely related to union:


164 
\begin{isabelle}


165 
insert\ a\ A\ =\


166 
\isacharbraceleft a\isacharbraceright\ \isasymunion\


167 
A%


168 
\rulename{insert_is_Un}


169 
\end{isabelle}


170 
%


171 
The finite set expression \isa{\isacharbraceleft


172 
a,b\isacharbraceright} abbreviates


173 
\isa{insert\ a\ (insert\ b\ \isacharbraceleft\isacharbraceright)}.


174 
Many simple facts can be proved automatically:


175 
\begin{isabelle}


176 
\isacommand{lemma}\


177 
"{\isacharbraceleft}a,b\isacharbraceright\


178 
\isasymunion\ {\isacharbraceleft}c,d\isacharbraceright\


179 
=\


180 
{\isacharbraceleft}a,b,c,d\isacharbraceright"\isanewline


181 
\isacommand{apply}\


182 
(blast)\isanewline


183 
\isacommand{done}


184 
\end{isabelle}


185 


186 


187 
Not everything that we would like to prove is valid.


188 
Consider this try:


189 
\begin{isabelle}


190 
\isacommand{lemma}\ "{\isacharbraceleft}a,b\isacharbraceright\ \isasyminter\ {\isacharbraceleft}b,c\isacharbraceright\ =\


191 
{\isacharbraceleft}b\isacharbraceright"\isanewline


192 
\isacommand{apply}\


193 
(auto)


194 
\end{isabelle}


195 
%


196 
The proof fails, leaving the subgoal \isa{b=c}. To see why it


197 
fails, consider a correct version:


198 
\begin{isabelle}


199 
\isacommand{lemma}\ "{\isacharbraceleft}a,b\isacharbraceright\ \isasyminter\ {\isacharbraceleft}b,c\isacharbraceright\ =\ (if\ a=c\ then\ {\isacharbraceleft}a,b\isacharbraceright\ else\ {\isacharbraceleft}b\isacharbraceright)"\isanewline


200 
\isacommand{apply}\ (simp)\isanewline


201 
\isacommand{apply}\ (blast)\isanewline


202 
\isacommand{done}%


203 
\end{isabelle}


204 


205 
Our mistake was to suppose that the various items were distinct. Another


206 
remark: this proof uses two methods, namely {\isa{simp}} and


207 
{\isa{blast}}. Calling {\isa{simp}} eliminates the


208 
\isa{if}\isa{then}\isa{else} expression, which {\isa{blast}}


209 
cannot break down. The combined methods (namely {\isa{force}} and


210 
{\isa{auto}}) can prove this fact in one step.


211 


212 


213 
\subsection{Set comprehension}


214 


215 
A set comprehension expresses the set of all elements that satisfy


216 
a given predicate. Formally, we do not need sets at all. We are


217 
working in higherorder logic, where variables can range over


218 
predicates. The main benefit of using sets is their notation;


219 
we can write \isa{x{\isasymin}A} and \isa{{\isacharbraceleft}z.\


220 
P\isacharbraceright} where predicates would require writing


221 
\isa{A(x)} and


222 
\isa{{\isasymlambda}z.\ P}.


223 


224 
These two laws describe the relationship between set


225 
comprehension and the membership relation.


226 
\begin{isabelle}


227 
(a\ \isasymin\


228 
{\isacharbraceleft}x.\ P\


229 
x\isacharbraceright)\ =\


230 
P\ a%


231 
\rulename{mem_Collect_eq}%


232 
\isanewline


233 
{\isacharbraceleft}x.\ x\ \isasymin\


234 
A\isacharbraceright\ =\ A%


235 
\rulename{Collect_mem_eq}


236 
\end{isabelle}


237 


238 
Facts such as these have trivial proofs:


239 
\begin{isabelle}


240 
\isacommand{lemma}\


241 
"{\isacharbraceleft}x.\ P\ x\ \isasymor\


242 
x\ \isasymin\ A\isacharbraceright\ =\


243 
{\isacharbraceleft}x.\ P\ x\isacharbraceright\


244 
\isasymunion\ A"


245 
\par\smallskip


246 
\isacommand{lemma}\


247 
"{\isacharbraceleft}x.\ P\ x\


248 
\isasymlongrightarrow\ Q\ x\isacharbraceright\ =\


249 
\isacharminus{\isacharbraceleft}x.\ P\ x\isacharbraceright\


250 
\isasymunion\ {\isacharbraceleft}x.\ Q\


251 
x\isacharbraceright"


252 
\end{isabelle}


253 


254 
Isabelle has a general syntax for comprehension, which is best


255 
described through an example:


256 
\begin{isabelle}


257 
\isacommand{lemma}\ "{\isacharbraceleft}p*q\ \isacharbar\ p\ q.\


258 
p{\isasymin}prime\ \isasymand\ q{\isasymin}prime\isacharbraceright\ =\


259 
\isanewline


260 
\ \ \ \ \ \ \ \ {\isacharbraceleft}z.\ {\isasymexists}p\ q.\ z\ =\ p*q\


261 
\isasymand\ p{\isasymin}prime\ \isasymand\


262 
q{\isasymin}prime\isacharbraceright"


263 
\end{isabelle}


264 
The proof is trivial because the left and right hand side


265 
of the expression are synonymous. The syntax appearing on the


266 
lefthand side abbreviates the righthand side: in this case, all numbers


267 
that are the product of two primes. In general, the syntax provides a neat


268 
way of expressing any set given by an expression built up from variables


269 
under specific constraints.


270 


271 


272 


273 
\subsection{Binding operators}


274 


275 
Universal and existential quantifications may range over sets,


276 
with the obvious meaning. Here are the natural deduction rules for the


277 
bounded universal quantifier. Occasionally you will need to apply


278 
\isa{bspec} with an explicit instantiation of the variable~\isa{x}:


279 
%


280 
\begin{isabelle}


281 
({\isasymAnd}x.\ x\ \isasymin\ A\ \isasymLongrightarrow\ P\ x)\ \isasymLongrightarrow\ {\isasymforall}x\isasymin


282 
A.\ P\ x%


283 
\rulename{ballI}%


284 
\isanewline


285 
\isasymlbrakk{\isasymforall}x\isasymin A.\


286 
P\ x;\ x\ \isasymin\


287 
A\isasymrbrakk\ \isasymLongrightarrow\ P\


288 
x%


289 
\rulename{bspec}


290 
\end{isabelle}


291 
%


292 
Dually, here are the natural deduction rules for the


293 
bounded existential quantifier. You may need to apply


294 
\isa{bexI} with an explicit instantiation:


295 
\begin{isabelle}


296 
\isasymlbrakk P\ x;\


297 
x\ \isasymin\ A\isasymrbrakk\


298 
\isasymLongrightarrow\


299 
{\isasymexists}x\isasymin A.\ P\


300 
x%


301 
\rulename{bexI}%


302 
\isanewline


303 
\isasymlbrakk{\isasymexists}x\isasymin A.\


304 
P\ x;\ {\isasymAnd}x.\


305 
{\isasymlbrakk}x\ \isasymin\ A;\


306 
P\ x\isasymrbrakk\ \isasymLongrightarrow\


307 
Q\isasymrbrakk\ \isasymLongrightarrow\ Q%


308 
\rulename{bexE}


309 
\end{isabelle}


310 


311 
Unions can be formed over the values of a given set. The syntax is


312 
\isa{\isasymUnion x\isasymin A.\ B} or \isa{UN


313 
x:\ A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law:


314 
\begin{isabelle}


315 
(b\ \isasymin\


316 
(\isasymUnion x\isasymin A.\ B\ x))\ =\ ({\isasymexists}x\isasymin A.\


317 
b\ \isasymin\ B\ x)


318 
\rulename{UN_iff}


319 
\end{isabelle}


320 
It has two natural deduction rules similar to those for the existential


321 
quantifier. Sometimes \isa{UN_I} must be applied explicitly:


322 
\begin{isabelle}


323 
\isasymlbrakk a\ \isasymin\


324 
A;\ b\ \isasymin\


325 
B\ a\isasymrbrakk\ \isasymLongrightarrow\


326 
b\ \isasymin\


327 
({\isasymUnion}x\isasymin A.\


328 
B\ x)


329 
\rulename{UN_I}%


330 
\isanewline


331 
\isasymlbrakk b\ \isasymin\


332 
({\isasymUnion}x\isasymin A.\


333 
B\ x);\


334 
{\isasymAnd}x.\ {\isasymlbrakk}x\ \isasymin\


335 
A;\ b\ \isasymin\


336 
B\ x\isasymrbrakk\ \isasymLongrightarrow\


337 
R\isasymrbrakk\ \isasymLongrightarrow\ R%


338 
\rulename{UN_E}


339 
\end{isabelle}


340 
%


341 
The following builtin abbreviation lets us express the union


342 
over a \emph{type}:


343 
\begin{isabelle}


344 
\ \ \ \ \


345 
({\isasymUnion}x.\ B\ x)\ {==}\


346 
({\isasymUnion}x{\isasymin}UNIV.\ B\ x)


347 
\end{isabelle}


348 
Abbreviations work as you might expect. The term on the lefthand side of


349 
the


350 
\isa{==} symbol is automatically translated to the righthand side when the


351 
term is parsed, the reverse translation being done when the term is


352 
displayed.


353 


354 
We may also express the union of a set of sets, written \isa{Union\ C} in


355 
\textsc{ascii}:


356 
\begin{isabelle}


357 
(A\ \isasymin\ \isasymUnion C)\ =\ ({\isasymexists}X\isasymin C.\ A\


358 
\isasymin\ X)


359 
\rulename{Union_iff}


360 
\end{isabelle}


361 


362 
Intersections are treated dually, although they seem to be used less often


363 
than unions. The syntax below would be \isa{INT


364 
x:\ A.\ B} and \isa{Inter\ C} in \textsc{ascii}. Among others, these


365 
theorems are available:


366 
\begin{isabelle}


367 
(b\ \isasymin\


368 
({\isasymInter}x\isasymin A.\


369 
B\ x))\


370 
=\


371 
({\isasymforall}x\isasymin A.\


372 
b\ \isasymin\ B\ x)


373 
\rulename{INT_iff}%


374 
\isanewline


375 
(A\ \isasymin\


376 
\isasymInter C)\ =\


377 
({\isasymforall}X\isasymin C.\


378 
A\ \isasymin\ X)


379 
\rulename{Inter_iff}


380 
\end{isabelle}


381 


382 
Isabelle uses logical equivalences such as those above in automatic proof.


383 
Unions, intersections and so forth are not simply replaced by their


384 
definitions. Instead, membership tests are simplified. For example, $x\in


385 
A\cup B$ is replaced by $x\in A\vee x\in B$.


386 


387 
The internal form of a comprehension involves the constant


388 
\isa{Collect}, which occasionally appears when a goal or theorem


389 
is displayed. For example, \isa{Collect\ P} is the same term as


390 
\isa{{\isacharbraceleft}z.\ P\ x\isacharbraceright}. The same thing can


391 
happen with quantifiers: for example, \isa{Ball\ A\ P} is


392 
\isa{{\isasymforall}z\isasymin A.\ P\ x} and \isa{Bex\ A\ P} is


393 
\isa{{\isasymexists}z\isasymin A.\ P\ x}. For indexed unions and


394 
intersections, you may see the constants \isa{UNION} and \isa{INTER}\@.


395 


396 
We have only scratched the surface of Isabelle/HOL's set theory.


397 
One primitive not mentioned here is the powerset operator


398 
{\isa{Pow}}. Hundreds of theorems are proved in theory \isa{Set} and its


399 
descendants.


400 


401 


402 
\subsection{Finiteness and cardinality}


403 


404 
The predicate \isa{finite} holds of all finite sets. Isabelle/HOL includes


405 
many familiar theorems about finiteness and cardinality


406 
(\isa{card}). For example, we have theorems concerning the cardinalities


407 
of unions, intersections and the powerset:


408 
%


409 
\begin{isabelle}


410 
{\isasymlbrakk}finite\ A;\ finite\ B\isasymrbrakk\isanewline


411 
\isasymLongrightarrow\ card\ A\ \isacharplus\ card\ B\ =\ card\ (A\ \isasymunion\ B)\ \isacharplus\ card\ (A\ \isasyminter\ B)


412 
\rulename{card_Un_Int}%


413 
\isanewline


414 
\isanewline


415 
finite\ A\ \isasymLongrightarrow\ card\


416 
(Pow\ A)\ =\ 2\ \isacharcircum\ card\ A%


417 
\rulename{card_Pow}%


418 
\isanewline


419 
\isanewline


420 
finite\ A\ \isasymLongrightarrow\isanewline


421 
card\ {\isacharbraceleft}B.\ B\ \isasymsubseteq\


422 
A\ \isasymand\ card\ B\ =\


423 
k\isacharbraceright\ =\ card\ A\ choose\ k%


424 
\rulename{n_subsets}


425 
\end{isabelle}


426 
Writing $A$ as $n$, the last of these theorems says that the number of


427 
$k$element subsets of~$A$ is $n \choose k$.


428 


429 
\emph{Note}: the term \isa{Finite\ A} is an abbreviation for


430 
\isa{A\ \isasymin\ Finites}, where the constant \isa{Finites} denotes the


431 
set of all finite sets of a given type. So there is no constant


432 
\isa{Finite}.


433 


434 


435 
\section{Functions}


436 


437 
This section describes a few concepts that involve functions.


438 
Some of the more important theorems are given along with the


439 
names. A few sample proofs appear. Unlike with set theory, however,


440 
we cannot simply state lemmas and expect them to be proved using {\isa{blast}}.


441 


442 
Two functions are \textbf{equal} if they yield equal results given equal arguments.


443 
This is the principle of \textbf{extensionality} for functions:


444 
\begin{isabelle}


445 
({\isasymAnd}x.\ f\ x\ =\ g\ x)\ {\isasymLongrightarrow}\ f\ =\ g


446 
\rulename{ext}


447 
\end{isabelle}


448 


449 


450 
Function \textbf{update} is useful for modelling machine states. It has


451 
the obvious definition and many useful facts are proved about


452 
it. In particular, the following equation is installed as a simplification


453 
rule:


454 
\begin{isabelle}


455 
(f(x:=y))\ z\ =\ (if\ z\ =\ x\ then\ y\ else\ f\ z)


456 
\rulename{fun_upd_apply}


457 
\end{isabelle}


458 
Two syntactic points must be noted. In


459 
\isa{(f(x:=y))\ z} we are applying an updated function to an


460 
argument; the outer parentheses are essential. A series of two or more


461 
updates can be abbreviated as shown on the lefthand side of this theorem:


462 
\begin{isabelle}


463 
f(x:=y,\ x:=z)\ =\ f(x:=z)


464 
\rulename{fun_upd_upd}


465 
\end{isabelle}


466 
Note also that we can write \isa{f(x:=z)} with only one pair of parentheses


467 
when it is not being applied to an argument.


468 


469 
\medskip


470 
The \textbf{identity} function and function \textbf{composition} are defined as


471 
follows:


472 
\begin{isabelle}%


473 
id\ \isasymequiv\ {\isasymlambda}x.\ x%


474 
\rulename{id_def}\isanewline


475 
f\ \isasymcirc\ g\ \isasymequiv\


476 
{\isasymlambda}x.\ f\


477 
(g\ x)%


478 
\rulename{o_def}


479 
\end{isabelle}


480 
%


481 
Many familiar theorems concerning the identity and composition


482 
are proved. For example, we have the associativity of composition:


483 
\begin{isabelle}


484 
f\ \isasymcirc\ (g\ \isasymcirc\ h)\ =\ f\ \isasymcirc\ g\ \isasymcirc\ h


485 
\rulename{o_assoc}


486 
\end{isabelle}


487 


488 
\medskip


489 


490 
A function may be \textbf{injective}, \textbf{surjective} or \textbf{bijective}:


491 
\begin{isabelle}


492 
inj_on\ f\ A\ \isasymequiv\ {\isasymforall}x\isasymin A.\


493 
{\isasymforall}y\isasymin A.\ f\ x\ =\ f\ y\ \isasymlongrightarrow\ x\


494 
=\ y%


495 
\rulename{inj_on_def}\isanewline


496 
surj\ f\ \isasymequiv\ {\isasymforall}y.\


497 
{\isasymexists}x.\ y\ =\ f\ x%


498 
\rulename{surj_def}\isanewline


499 
bij\ f\ \isasymequiv\ inj\ f\ \isasymand\ surj\ f


500 
\rulename{bij_def}


501 
\end{isabelle}


502 
The second argument


503 
of \isa{inj_on} lets us express that a function is injective over a


504 
given set. This refinement is useful in higherorder logic, where


505 
functions are total; in some cases, a function's natural domain is a subset


506 
of its domain type. Writing \isa{inj\ f} abbreviates \isa{inj_on\ f\


507 
UNIV}, for when \isa{f} is injective everywhere.


508 


509 
The operator {\isa{inv}} expresses the \textbf{inverse} of a function. In


510 
general the inverse may not be well behaved. We have the usual laws,


511 
such as these:


512 
\begin{isabelle}


513 
inj\ f\ \ \isasymLongrightarrow\ inv\ f\ (f\ x)\ =\ x%


514 
\rulename{inv_f_f}\isanewline


515 
surj\ f\ \isasymLongrightarrow\ f\ (inv\ f\ y)\ =\ y


516 
\rulename{surj_f_inv_f}\isanewline


517 
bij\ f\ \ \isasymLongrightarrow\ inv\ (inv\ f)\ =\ f


518 
\rulename{inv_inv_eq}


519 
\end{isabelle}


520 
%


521 
%Other useful facts are that the inverse of an injection


522 
%is a surjection and vice versa; the inverse of a bijection is


523 
%a bijection.


524 
%\begin{isabelle}


525 
%inj\ f\ \isasymLongrightarrow\ surj\


526 
%(inv\ f)


527 
%\rulename{inj_imp_surj_inv}\isanewline


528 
%surj\ f\ \isasymLongrightarrow\ inj\ (inv\ f)


529 
%\rulename{surj_imp_inj_inv}\isanewline


530 
%bij\ f\ \isasymLongrightarrow\ bij\ (inv\ f)


531 
%\rulename{bij_imp_bij_inv}


532 
%\end{isabelle}


533 
%


534 
%The converses of these results fail. Unless a function is


535 
%well behaved, little can be said about its inverse. Here is another


536 
%law:


537 
%\begin{isabelle}


538 
%{\isasymlbrakk}bij\ f;\ bij\ g\isasymrbrakk\ \isasymLongrightarrow\ inv\ (f\ \isasymcirc\ g)\ =\ inv\ g\ \isasymcirc\ inv\ f%


539 
%\rulename{o_inv_distrib}


540 
%\end{isabelle}


541 


542 
Theorems involving these concepts can be hard to prove. The following


543 
example is easy, but it cannot be proved automatically. To begin


544 
with, we need a law that relates the quality of functions to


545 
equality over all arguments:


546 
\begin{isabelle}


547 
(f\ =\ g)\ =\ ({\isasymforall}x.\ f\ x\ =\ g\ x)


548 
\rulename{expand_fun_eq}


549 
\end{isabelle}


550 


551 
This is just a restatement of extensionality. Our lemma states


552 
that an injection can be cancelled from the left


553 
side of function composition:


554 
\begin{isabelle}


555 
\isacommand{lemma}\ "inj\ f\ \isasymLongrightarrow\ (f\ o\ g\ =\ f\ o\ h)\ =\ (g\ =\ h)"\isanewline


556 
\isacommand{apply}\ (simp\ add:\ expand_fun_eq\ inj_on_def\ o_def)\isanewline


557 
\isacommand{apply}\ (auto)\isanewline


558 
\isacommand{done}


559 
\end{isabelle}


560 


561 
The first step of the proof invokes extensionality and the definitions


562 
of injectiveness and composition. It leaves one subgoal:


563 
\begin{isabelle}


564 
%inj\ f\ \isasymLongrightarrow\ (f\ \isasymcirc\ g\ =\ f\ \isasymcirc\ h)\


565 
%=\ (g\ =\ h)\isanewline


566 
\ 1.\ {\isasymforall}x\ y.\ f\ x\ =\ f\ y\ \isasymlongrightarrow\ x\ =\ y\ \isasymLongrightarrow\isanewline


567 
\ \ \ \ ({\isasymforall}x.\ f\ (g\ x)\ =\ f\ (h\ x))\ =\ ({\isasymforall}x.\ g\ x\ =\ h\ x)


568 
\end{isabelle}


569 
This can be proved using the {\isa{auto}} method.


570 


571 
\medskip


572 


573 
The \textbf{image} of a set under a function is a most useful notion. It


574 
has the obvious definition:


575 
\begin{isabelle}


576 
f\ ``\ A\ \isasymequiv\ {\isacharbraceleft}y.\ {\isasymexists}x\isasymin


577 
A.\ y\ =\ f\ x\isacharbraceright


578 
\rulename{image_def}


579 
\end{isabelle}


580 
%


581 
Here are some of the many facts proved about image:


582 
\begin{isabelle}


583 
(f\ \isasymcirc\ g)\ ``\ r\ =\ f\ ``\ g\ ``\ r


584 
\rulename{image_compose}\isanewline


585 
f``(A\ \isasymunion\ B)\ =\ f``A\ \isasymunion\ f``B


586 
\rulename{image_Un}\isanewline


587 
inj\ f\ \isasymLongrightarrow\ f``(A\ \isasyminter\


588 
B)\ =\ f``A\ \isasyminter\ f``B


589 
\rulename{image_Int}


590 
%\isanewline


591 
%bij\ f\ \isasymLongrightarrow\ f\ ``\ (\ A)\ =\ \isacharminus\ f\ ``\ A%


592 
%\rulename{bij_image_Compl_eq}


593 
\end{isabelle}


594 


595 


596 
Laws involving image can often be proved automatically. Here


597 
are two examples, illustrating connections with indexed union and with the


598 
general syntax for comprehension:


599 
\begin{isabelle}


600 
\isacommand{lemma}\ "f``A\ \isasymunion\ g``A\ =\ ({\isasymUnion}x{\isasymin}A.\ {\isacharbraceleft}f\ x,\ g\


601 
x\isacharbraceright)


602 
\par\smallskip


603 
\isacommand{lemma}\ "f\ ``\ \isacharbraceleft(x,y){.}\ P\ x\ y\isacharbraceright\ =\ {\isacharbraceleft}f(x,y)\ \isacharbar\ x\ y.\ P\ x\


604 
y\isacharbraceright"


605 
\end{isabelle}


606 


607 
\medskip


608 
A function's \textbf{range} is the set of values that the function can


609 
take on. It is, in fact, the image of the universal set under


610 
that function. There is no constant {\isa{range}}. Instead, {\isa{range}}


611 
abbreviates an application of image to {\isa{UNIV}}:


612 
\begin{isabelle}


613 
\ \ \ \ \ range\ f\


614 
{==}\ f``UNIV


615 
\end{isabelle}


616 
%


617 
Few theorems are proved specifically


618 
for {\isa{range}}; in most cases, you should look for a more general


619 
theorem concerning images.


620 


621 
\medskip


622 
\textbf{Inverse image} is also useful. It is defined as follows:


623 
\begin{isabelle}


624 
f\ \isacharminus``\ B\ \isasymequiv\ {\isacharbraceleft}x.\ f\ x\ \isasymin\ B\isacharbraceright


625 
\rulename{vimage_def}


626 
\end{isabelle}


627 
%


628 
This is one of the facts proved about it:


629 
\begin{isabelle}


630 
f\ \isacharminus``\ (\ A)\ =\ \isacharminus\ f\ \isacharminus``\ A%


631 
\rulename{vimage_Compl}


632 
\end{isabelle}


633 


634 


635 
\section{Relations}


636 


637 
A \textbf{relation} is a set of pairs. As such, the set operations apply


638 
to them. For instance, we may form the union of two relations. Other


639 
primitives are defined specifically for relations.


640 


641 
The \textbf{identity} relation, also known as equality, has the obvious


642 
definition:


643 
\begin{isabelle}


644 
Id\ \isasymequiv\ {\isacharbraceleft}p.\ {\isasymexists}x.\ p\ =\ (x,x){\isacharbraceright}%


645 
\rulename{Id_def}


646 
\end{isabelle}


647 


648 
\textbf{Composition} of relations (the infix \isa{O}) is also available:


649 
\begin{isabelle}


650 
r\ O\ s\ \isasymequiv\ \isacharbraceleft(x,z){.}\ {\isasymexists}y.\ (x,y)\ \isasymin\ s\ \isasymand\ (y,z)\ \isasymin\ r\isacharbraceright


651 
\rulename{comp_def}


652 
\end{isabelle}


653 


654 
This is one of the many lemmas proved about these concepts:


655 
\begin{isabelle}


656 
R\ O\ Id\ =\ R


657 
\rulename{R_O_Id}


658 
\end{isabelle}


659 
%


660 
Composition is monotonic, as are most of the primitives appearing


661 
in this chapter. We have many theorems similar to the following


662 
one:


663 
\begin{isabelle}


664 
\isasymlbrakk r\isacharprime\ \isasymsubseteq\ r;\ s\isacharprime\


665 
\isasymsubseteq\ s\isasymrbrakk\ \isasymLongrightarrow\ r\isacharprime\ O\


666 
s\isacharprime\ \isasymsubseteq\ r\ O\ s%


667 
\rulename{comp_mono}


668 
\end{isabelle}


669 


670 
The \textbf{converse} or inverse of a relation exchanges the roles


671 
of the two operands. Note that \isa{\isacharcircum1} is a postfix


672 
operator.


673 
\begin{isabelle}


674 
((a,b)\ \isasymin\ r\isacharcircum1)\ =\


675 
((b,a)\ \isasymin\ r)


676 
\rulename{converse_iff}


677 
\end{isabelle}


678 
%


679 
Here is a typical law proved about converse and composition:


680 
\begin{isabelle}


681 
(r\ O\ s){\isacharcircum}\isacharminus1\ =\ s\isacharcircum1\ O\ r\isacharcircum1


682 
\rulename{converse_comp}


683 
\end{isabelle}


684 


685 


686 
The \textbf{image} of a set under a relation is defined analogously


687 
to image under a function:


688 
\begin{isabelle}


689 
(b\ \isasymin\ r\ \isacharcircum{\isacharcircum}\ A)\ =\ ({\isasymexists}x\isasymin


690 
A.\ (x,b)\ \isasymin\ r)


691 
\rulename{Image_iff}


692 
\end{isabelle}


693 
It satisfies many similar laws.


694 


695 
%Image under relations, like image under functions, distributes over unions:


696 
%\begin{isabelle}


697 
%r\ \isacharcircum{\isacharcircum}\


698 
%({\isasymUnion}x\isasyminA.\


699 
%B\


700 
%x)\ =\


701 
%({\isasymUnion}x\isasyminA.\


702 
%r\ \isacharcircum{\isacharcircum}\ B\


703 
%x)


704 
%\rulename{Image_UN}


705 
%\end{isabelle}


706 


707 


708 
The \textbf{domain} and \textbf{range} of a relation are defined in the


709 
standard way:


710 
\begin{isabelle}


711 
(a\ \isasymin\ Domain\ r)\ =\ ({\isasymexists}y.\ (a,y)\ \isasymin\


712 
r)


713 
\rulename{Domain_iff}%


714 
\isanewline


715 
(a\ \isasymin\ Range\ r)\


716 
\ =\ ({\isasymexists}y.\


717 
(y,a)\


718 
\isasymin\ r)


719 
\rulename{Range_iff}


720 
\end{isabelle}


721 


722 
Iterated composition of a relation is available. The notation overloads


723 
that of exponentiation:


724 
\begin{isabelle}


725 
R\ \isacharcircum\ \isadigit{0}\ =\ Id\isanewline


726 
R\ \isacharcircum\ Suc\ n\ =\ R\ O\ R\isacharcircum n


727 
\rulename{RelPow.relpow.simps}


728 
\end{isabelle}


729 


730 
The \textbf{reflexive transitive closure} of a relation is particularly


731 
important. It has the postfix syntax \isa{r\isacharcircum{*}}. The


732 
construction is defined to be the least fixedpoint satisfying the


733 
following equation:


734 
\begin{isabelle}


735 
r\isacharcircum{*}\ =\ Id\ \isasymunion\ (r\ O\ r\isacharcircum{*})


736 
\rulename{rtrancl_unfold}


737 
\end{isabelle}


738 
%


739 
Among its basic properties are three that serve as introduction


740 
rules:


741 
\begin{isabelle}


742 
(a,a)\ \isasymin\


743 
r\isacharcircum{*}


744 
\rulename{rtrancl_refl}%


745 
\isanewline


746 
p\ \isasymin\ r\ \isasymLongrightarrow\


747 
p\ \isasymin\


748 
r\isacharcircum{*}


749 
\rulename{r_into_rtrancl}%


750 
\isanewline


751 
\isasymlbrakk(a,b)\ \isasymin\


752 
r\isacharcircum{*};\


753 
(b,c)\ \isasymin\ r\isacharcircum{*}\isasymrbrakk\


754 
\isasymLongrightarrow\


755 
(a,c)\ \isasymin\ r\isacharcircum{*}


756 
\rulename{rtrancl_trans}


757 
\end{isabelle}


758 
%


759 
Induction over the reflexive transitive closure is available:


760 
\begin{isabelle}


761 
\isasymlbrakk(a,b)\ \isasymin\ r\isacharcircum{*};\ P\ a;\isanewline


762 
\ \ {\isasymAnd}y\ z.\


763 
\isasymlbrakk(a,y)\ \isasymin\ r\isacharcircum{*};\


764 
(y,z)\ \isasymin\ r;\ P\ y\isasymrbrakk\


765 
\isasymLongrightarrow\ P\ z\isasymrbrakk\isanewline


766 
\isasymLongrightarrow\ P\ b%


767 
\rulename{rtrancl_induct}


768 
\end{isabelle}


769 
%


770 
Here is one of the many laws proved about the reflexive transitive


771 
closure:


772 
\begin{isabelle}


773 
(r\isacharcircum{*}){\isacharcircum}*\ =\ r\isacharcircum{*}


774 
\rulename{rtrancl_idemp}


775 
\end{isabelle}


776 


777 
The transitive closure is similar. It has two


778 
introduction rules:


779 
\begin{isabelle}


780 
p\ \isasymin\ r\ \isasymLongrightarrow\ p\ \isasymin\ r\isacharcircum{\isacharplus}


781 
\rulename{r_into_trancl}\isanewline


782 
\isasymlbrakk(a,b)\ \isasymin\


783 
r\isacharcircum{\isacharplus};\ (b,c)\


784 
\isasymin\ r\isacharcircum{\isacharplus}\isasymrbrakk\


785 
\isasymLongrightarrow\ (a,c)\ \isasymin\


786 
r\isacharcircum{\isacharplus}


787 
\rulename{trancl_trans}


788 
\end{isabelle}


789 
%


790 
The induction rule is similar to the one shown above.


791 
A typical lemma states that transitive closure commutes with the converse


792 
operator:


793 
\begin{isabelle}


794 
(r\isacharcircum1){\isacharcircum}\isacharplus\ =\ (r\isacharcircum{\isacharplus}){\isacharcircum}\isacharminus1


795 
\rulename{trancl_converse}


796 
\end{isabelle}


797 


798 


799 
The reflexive transitive closure also commutes with the converse.


800 
Let us examine the proof. Each direction of the equivalence is


801 
proved separately. The two proofs are almost identical. Here


802 
is the first one:


803 
\begin{isabelle}


804 
\isacommand{lemma}\ rtrancl_converseD:\ "(x,y)\ \isasymin\ (r\isacharcircum1){\isacharcircum}*\ \isasymLongrightarrow\ (x,y)\ \isasymin\ (r\isacharcircum{*}){\isacharcircum}\isacharminus1"\isanewline


805 
\isacommand{apply}\ (erule\


806 
rtrancl_induct)\isanewline


807 
\ \isacommand{apply}\ (rule\ rtrancl_refl)\isanewline


808 
\isacommand{apply}\ (blast\ intro:\ r_into_rtrancl\ rtrancl_trans)\isanewline


809 
\isacommand{done}


810 
\end{isabelle}


811 


812 
The first step of the proof applies induction, leaving these subgoals:


813 
\begin{isabelle}


814 
\ 1.\ (x,x)\ \isasymin\ r\isacharcircum{*}\isanewline


815 
\ 2.\ {\isasymAnd}y\ z.\ \isasymlbrakk(x,y)\ \isasymin\ (r\isacharcircum1){\isacharcircum}*;\ (y,z)\ \isasymin\ r\isacharcircum1;\ (y,x)\ \isasymin\ r\isacharcircum{*}\isasymrbrakk\isanewline


816 
\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow\ (z,x)\ \isasymin\ r\isacharcircum{*}


817 
\end{isabelle}


818 


819 
The first subgoal is trivial by reflexivity. The second follows


820 
by first eliminating the converse operator, yielding the


821 
assumption \isa{(z,y)\


822 
\isasymin\ r}, and then


823 
applying the introduction rules shown above. The same proof script handles


824 
the other direction:


825 
\begin{isabelle}


826 
\isacommand{lemma}\ rtrancl_converseI:\ "(x,y)\ \isasymin\ (r\isacharcircum{*}){\isacharcircum}\isacharminus1\ \isasymLongrightarrow\ (x,y)\ \isasymin\ (r\isacharcircum1){\isacharcircum}*"\isanewline


827 
\isacommand{apply}\ (drule\ converseD)\isanewline


828 
\isacommand{apply}\ (erule\ rtrancl_induct)\isanewline


829 
\ \isacommand{apply}\ (rule\ rtrancl_refl)\isanewline


830 
\isacommand{apply}\ (blast\ intro:\ r_into_rtrancl\ rtrancl_trans)\isanewline


831 
\isacommand{done}


832 
\end{isabelle}


833 


834 


835 
Finally, we combine the two lemmas to prove the desired equation:


836 
\begin{isabelle}


837 
\isacommand{lemma}\ rtrancl_converse:\ "(r\isacharcircum1){\isacharcircum}*\ =\ (r\isacharcircum{*}){\isacharcircum}\isacharminus1"\isanewline


838 
\isacommand{apply}\ (auto\ intro:\


839 
rtrancl_converseI\ dest:\


840 
rtrancl_converseD)\isanewline


841 
\isacommand{done}


842 
\end{isabelle}


843 


844 
Note one detail. The {\isa{auto}} method can prove this but


845 
{\isa{blast}} cannot. \remark{move to a later section?}


846 
This is because the


847 
lemmas we have proved only apply to ordered pairs. {\isa{Auto}} can


848 
convert a bound variable of a product type into a pair of bound variables,


849 
allowing the lemmas to be applied. A toy example demonstrates this


850 
point:


851 
\begin{isabelle}


852 
\isacommand{lemma}\ "A\ \isasymsubseteq\ Id"\isanewline


853 
\isacommand{apply}\ (rule\ subsetI)\isanewline


854 
\isacommand{apply}\ (auto)


855 
\end{isabelle}


856 
Applying the introduction rule \isa{subsetI} leaves the goal of showing


857 
that an arbitrary element of~\isa{A} belongs to~\isa{Id}.


858 
\begin{isabelle}


859 
A\ \isasymsubseteq\ Id\isanewline


860 
\ 1.\ {\isasymAnd}x.\ x\ \isasymin\ A\ \isasymLongrightarrow\ x\ \isasymin\ Id


861 
\end{isabelle}


862 
The \isa{simp} and \isa{blast} methods can do nothing here. However,


863 
\isa{x} is of product type and therefore denotes an ordered pair. The


864 
\isa{auto} method (and some others, including \isa{clarify})


865 
can replace


866 
\isa{x} by a pair, which then allows the further simplification from


867 
\isa{(a,b)\ \isasymin\ A} to \isa{a\ =\ b}.


868 
\begin{isabelle}


869 
A\ \isasymsubseteq\ Id\isanewline


870 
\ 1.\ {\isasymAnd}a\ b.\ (a,b)\ \isasymin\ A\ \isasymLongrightarrow\ a\ =\ b


871 
\end{isabelle}


872 


873 


874 


875 
\section{Wellfounded relations and induction}


876 


877 
Induction comes in many forms, including traditional mathematical


878 
induction, structural induction on lists and induction on size.


879 
More general than these is induction over a wellfounded relation.


880 
Such A relation expresses the notion of a terminating process.


881 
Intuitively, the relation~$\prec$ is \textbf{wellfounded} if it admits no


882 
infinite descending chains


883 
\[ \cdots \prec a@2 \prec a@1 \prec a@0. \]


884 
If $\prec$ is wellfounded then it can be used with the wellfounded


885 
induction rule:


886 
\[ \infer{P(a)}{\infer*{P(x)}{[\forall y.\, y\prec x \imp P(y)]}} \]


887 
To show $P(a)$ for a particular term~$a$, it suffices to show $P(x)$ for


888 
arbitrary~$x$ under the assumption that $P(y)$ holds for $y\prec x$.


889 
Intuitively, the wellfoundedness of $\prec$ ensures that the chains of


890 
reasoning are finite.


891 


892 
In Isabelle, the induction rule is expressed like this:


893 
\begin{isabelle}


894 
{\isasymlbrakk}wf\ r;\


895 
{\isasymAnd}x.\ {\isasymforall}y.\ (y,x)\ \isasymin\ r\


896 
\isasymlongrightarrow\ P\ y\ \isasymLongrightarrow\ P\ x\isasymrbrakk\


897 
\isasymLongrightarrow\ P\ a


898 
\rulename{wf_induct}


899 
\end{isabelle}


900 
Here \isa{wf\ r} expresses that relation~\isa{r} is wellfounded.


901 


902 
Many familiar induction principles are instances of this rule.


903 
For example, the predecessor relation on the natural numbers


904 
is wellfounded; induction over it is mathematical induction.


905 
The `tail of' relation on lists is wellfounded; induction over


906 
it is structural induction.


907 


908 
Wellfoundedness can be difficult to show. The various equivalent


909 
formulations are all hard to use formally. However, often a relation


910 
is obviously wellfounded by construction. The HOL library provides


911 
several theorems concerning ways of constructing a wellfounded relation.


912 
For example, a relation can be defined by means of a measure function


913 
involving an existing relation, or two relations can be


914 
combined lexicographically.


915 


916 
The library declares \isa{less_than} as a relation object,


917 
that is, a set of pairs of natural numbers. Two theorems tell us that this


918 
relation behaves as expected and that it is wellfounded:


919 
\begin{isabelle}


920 
((x,y)\ \isasymin\ less_than)\ =\ (x\ <\ y)


921 
\rulename{less_than_iff}\isanewline


922 
wf\ less_than


923 
\rulename{wf_less_than}


924 
\end{isabelle}


925 


926 
The notion of measure generalizes to the \textbf{inverse image} of


927 
relation. Given a relation~\isa{r} and a function~\isa{f}, we express a new


928 
relation using \isa{f} as a measure. An infinite descending chain on this


929 
new relation would give rise to an infinite descending chain on~\isa{r}.


930 
The library holds the definition of this concept and a theorem stating


931 
that it preserves wellfoundedness:


932 
\begin{isabelle}


933 
inv_image\ r\ f\ \isasymequiv\ \isacharbraceleft(x,y).\ (f\ x,\ f\ y)\


934 
\isasymin\ r\isacharbraceright


935 
\rulename{inv_image_def}\isanewline


936 
wf\ r\ \isasymLongrightarrow\ wf\ (inv_image\ r\ f)


937 
\rulename{wf_inv_image}


938 
\end{isabelle}


939 


940 
The most familiar notion of measure involves the natural numbers. This yields,


941 
for example, induction on the length of the list or the size


942 
of a tree. The library defines \isa{measure} specifically:


943 
\begin{isabelle}


944 
measure\ \isasymequiv\ inv_image\ less_than%


945 
\rulename{measure_def}\isanewline


946 
wf\ (measure\ f)


947 
\rulename{wf_measure}


948 
\end{isabelle}


949 


950 
Of the other constructions, the most important is the \textbf{lexicographic


951 
product} of two relations. It expresses the standard dictionary


952 
ordering over pairs. We write \isa{ra\ <*lex*>\ rb}, where \isa{ra}


953 
and \isa{rb} are the two operands. The lexicographic product satisfies the


954 
usual definition and it preserves wellfoundedness:


955 
\begin{isabelle}


956 
ra\ <*lex*>\ rb\ \isasymequiv \isanewline


957 
\ \ \isacharbraceleft ((a,b),(a',b')).\ (a,a')\ \isasymin \ ra\


958 
\isasymor\isanewline


959 
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \,a=a'\ \isasymand \ (b,b')\


960 
\isasymin \ rb\isacharbraceright


961 
\rulename{lex_prod_def}%


962 
\par\smallskip


963 
\isasymlbrakk wf\ ra;\ wf\ rb\isasymrbrakk \ \isasymLongrightarrow \ wf\ (ra\ <*lex*>\ rb)


964 
\rulename{wf_lex_prod}


965 
\end{isabelle}


966 


967 
These constructions can be used in a


968 
\textbf{recdef} declaration (\S\ref{sec:recdefsimplification}) to define


969 
the wellfounded relation used to prove termination.


970 


971 


972 


973 


974 


975 
\section{Fixed point operators}


976 


977 
Fixed point operators define sets recursively. Most users invoke


978 
them through Isabelle's inductive definition facility, which


979 
is discussed later. However, they can be invoked directly. The \textbf{least}


980 
or \textbf{strongest} fixed point yields an inductive definition;


981 
the \textbf{greatest} or \textbf{weakest} fixed point yields a coinductive


982 
definition. Mathematicians may wish to note that the existence


983 
of these fixed points is guaranteed by the KnasterTarski theorem.


984 


985 


986 
The theory works applies only to monotonic functions. Isabelle's


987 
definition of monotone is overloaded over all orderings:


988 
\begin{isabelle}


989 
mono\ f\ \isasymequiv\ {\isasymforall}A\ B.\ A\ \isasymle\ B\ \isasymlongrightarrow\ f\ A\ \isasymle\ f\ B%


990 
\rulename{mono_def}


991 
\end{isabelle}


992 
%


993 
For fixed point operators, the ordering will be the subset relation: if


994 
$A\subseteq B$ then we expect $f(A)\subseteq f(B)$. In addition to its


995 
definition, monotonicity has the obvious introduction and destruction


996 
rules:


997 
\begin{isabelle}


998 
({\isasymAnd}A\ B.\ A\ \isasymle\ B\ \isasymLongrightarrow\ f\ A\ \isasymle\ f\ B)\ \isasymLongrightarrow\ mono\ f%


999 
\rulename{monoI}%


1000 
\par\smallskip% \isanewline didn't leave enough space


1001 
{\isasymlbrakk}mono\ f;\ A\ \isasymle\ B\isasymrbrakk\


1002 
\isasymLongrightarrow\ f\ A\ \isasymle\ f\ B%


1003 
\rulename{monoD}


1004 
\end{isabelle}


1005 


1006 
The most important properties of the least fixed point are that


1007 
it is a fixed point and that it enjoys an induction rule:


1008 
\begin{isabelle}


1009 
mono\ f\ \isasymLongrightarrow\ lfp\ f\ =\ f\ (lfp\ f)


1010 
\rulename{lfp_unfold}%


1011 
\par\smallskip% \isanewline didn't leave enough space


1012 
{\isasymlbrakk}a\ \isasymin\ lfp\ f;\ mono\ f;\isanewline


1013 
\ {\isasymAnd}x.\ x\


1014 
\isasymin\ f\ (lfp\ f\ \isasyminter\ {\isacharbraceleft}x.\ P\


1015 
x\isacharbraceright)\ \isasymLongrightarrow\ P\ x\isasymrbrakk\


1016 
\isasymLongrightarrow\ P\ a%


1017 
\rulename{lfp_induct}


1018 
\end{isabelle}


1019 
%


1020 
The induction rule shown above is more convenient than the basic


1021 
one derived from the minimality of {\isa{lfp}}. Observe that both theorems


1022 
demand \isa{mono\ f} as a premise.


1023 


1024 
The greatest fixed point is similar, but it has a \textbf{coinduction} rule:


1025 
\begin{isabelle}


1026 
mono\ f\ \isasymLongrightarrow\ gfp\ f\ =\ f\ (gfp\ f)


1027 
\rulename{gfp_unfold}%


1028 
\isanewline


1029 
{\isasymlbrakk}mono\ f;\ a\ \isasymin\ X;\ X\ \isasymsubseteq\ f\ (X\


1030 
\isasymunion\ gfp\ f)\isasymrbrakk\ \isasymLongrightarrow\ a\ \isasymin\


1031 
gfp\ f%


1032 
\rulename{coinduct}


1033 
\end{isabelle}


1034 
A \textbf{bisimulation} is perhaps the bestknown concept defined as a


1035 
greatest fixed point. Exhibiting a bisimulation to prove the equality of


1036 
two agents in a process algebra is an example of coinduction.


1037 
The coinduction rule can be strengthened in various ways; see


1038 
theory {\isa{Gfp}} for details.


1039 
An example using the fixed point operators appears later in this


1040 
chapter, in the section on computation tree logic


1041 
(\S\ref{sec:ctlcasestudy}).
