10303

1 
\chapter{Sets, Functions and Relations}


2 


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


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


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


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


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


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


9 
elements have the same type, say


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


11 
same way as lists.


12 


13 
Relations are simply sets of pairs. This chapter describes


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


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


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


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


18 


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


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


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


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


23 
the notation.


24 


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


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


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


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


29 
easier.


30 


31 


32 
\section{Sets}


33 


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


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


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


37 


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


39 
resemblance to those for conjunction.


40 
\begin{isabelle}


41 
\isasymlbrakk c\ \isasymin\


42 
A;\ c\ \isasymin\


43 
B\isasymrbrakk\ \isasymLongrightarrow\ c\


44 
\isasymin\ A\ \isasyminter\ B%


45 
\rulename{IntI}\isanewline


46 
c\ \isasymin\ A\ \isasyminter\


47 
B\ \isasymLongrightarrow\ c\ \isasymin\


48 
A%


49 
\rulename{IntD1}\isanewline


50 
c\ \isasymin\ A\ \isasyminter\


51 
B\ \isasymLongrightarrow\ c\ \isasymin\


52 
B%


53 
\rulename{IntD2}%


54 
\end{isabelle}


55 


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


57 
\begin{isabelle}


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


59 
\rulename{Compl_iff}\isanewline


60 
\isacharminus\ (A\ \isasymunion\


61 
B)\ =\ \isacharminus\


62 
A\ \isasyminter\ \isacharminus\ B


63 
\rulename{Compl_Un}


64 
\end{isabelle}


65 


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


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


68 
empty set and for the universal set.


69 
\begin{isabelle}


70 
A\ \isasyminter\ (B\


71 
\isacharminus\ A)\ =\


72 
\isacharbraceleft{\isacharbraceright}


73 
\rulename{Diff_disjoint}%


74 
\isanewline


75 
A\ \isasymunion\ \isacharminus\ A\


76 
=\ UNIV%


77 
\rulename{Compl_partition}


78 
\end{isabelle}


79 


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


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


82 
are its natural deduction rules:


83 
\begin{isabelle}


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


85 
\rulename{subsetI}%


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


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


88 
A\isasymrbrakk\ \isasymLongrightarrow\ c\


89 
\isasymin\ B%


90 
\rulename{subsetD}


91 
\end{isabelle}


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


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


94 
one:


95 
\begin{isabelle}


96 
(A\ \isasymunion\ B\


97 
\isasymsubseteq\ C)\ =\


98 
(A\ \isasymsubseteq\ C\


99 
\isasymand\ B\ \isasymsubseteq\


100 
C)


101 
\rulename{Un_subset_iff}


102 
\end{isabelle}


103 
Here is another example, also proved automatically:


104 
\begin{isabelle}


105 
\isacommand{lemma}\ "(A\


106 
\isasymsubseteq\ B)\ =\


107 
(B\ \isasymsubseteq\


108 
A)"\isanewline


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


110 
\isacommand{done}


111 
\end{isabelle}


112 
%


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


114 
\begin{isabelle}


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


116 
A)"


117 
\end{isabelle}


118 
%


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


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


121 
subset.


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


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


124 
proof to succeed:


125 


126 
\begin{isabelle}


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


128 
A)"


129 
\end{isabelle}


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


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


132 


133 
\medskip


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


135 
This is


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


137 
\begin{isabelle}


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


139 
{\isasymLongrightarrow}\ A\ =\ B


140 
\rulename{set_ext}


141 
\end{isabelle}


142 
Extensionality is often expressed as


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


144 
The following rules express both


145 
directions of this equivalence. Proving a set equation using


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


147 
\begin{isabelle}


148 
\isasymlbrakk A\ \isasymsubseteq\ B;\ B\ \isasymsubseteq\


149 
A\isasymrbrakk\ \isasymLongrightarrow\ A\ =\ B%


150 
\rulename{equalityI}


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


152 
\isasymlbrakk A\ =\ B;\ \isasymlbrakk A\ \isasymsubseteq\ B;\ B\


153 
\isasymsubseteq\ A\isasymrbrakk\ \isasymLongrightarrow\ P\isasymrbrakk\


154 
\isasymLongrightarrow\ P%


155 
\rulename{equalityE}


156 
\end{isabelle}


157 


158 


159 
\subsection{Finite set notation}


160 


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


162 
closely related to union:


163 
\begin{isabelle}


164 
insert\ a\ A\ =\


165 
\isacharbraceleft a\isacharbraceright\ \isasymunion\


166 
A%


167 
\rulename{insert_is_Un}


168 
\end{isabelle}


169 
%


170 
The finite set expression \isa{\isacharbraceleft


171 
a,b\isacharbraceright} abbreviates


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


173 
Many simple facts can be proved automatically:


174 
\begin{isabelle}


175 
\isacommand{lemma}\


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


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


178 
=\


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


180 
\isacommand{apply}\


181 
(blast)\isanewline


182 
\isacommand{done}


183 
\end{isabelle}


184 


185 


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


187 
Consider this try:


188 
\begin{isabelle}


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


190 
{\isacharbraceleft}b\isacharbraceright"\isanewline


191 
\isacommand{apply}\


192 
(auto)


193 
\end{isabelle}


194 
%


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


196 
fails, consider a correct version:


197 
\begin{isabelle}


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


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


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


201 
\isacommand{done}%


202 
\end{isabelle}


203 


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


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


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


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


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


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


210 


211 


212 
\subsection{Set comprehension}


213 


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


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


216 
working in higherorder logic, where variables can range over


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


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


219 
P\isacharbraceright} where predicates would require writing


220 
\isa{A(x)} and


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


222 


223 
These two laws describe the relationship between set


224 
comprehension and the membership relation.


225 
\begin{isabelle}


226 
(a\ \isasymin\


227 
{\isacharbraceleft}x.\ P\


228 
x\isacharbraceright)\ =\


229 
P\ a%


230 
\rulename{mem_Collect_eq}%


231 
\isanewline


232 
{\isacharbraceleft}x.\ x\ \isasymin\


233 
A\isacharbraceright\ =\ A%


234 
\rulename{Collect_mem_eq}


235 
\end{isabelle}


236 


237 
Facts such as these have trivial proofs:


238 
\begin{isabelle}


239 
\isacommand{lemma}\


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


241 
x\ \isasymin\ A\isacharbraceright\ =\


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


243 
\isasymunion\ A"


244 
\par\smallskip


245 
\isacommand{lemma}\


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


247 
\isasymlongrightarrow\ Q\ x\isacharbraceright\ =\


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


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


250 
x\isacharbraceright"


251 
\end{isabelle}


252 


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


254 
described through an example:


255 
\begin{isabelle}


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


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


258 
\isanewline


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


260 
\isasymand\ p{\isasymin}prime\ \isasymand\


261 
q{\isasymin}prime\isacharbraceright"


262 
\end{isabelle}


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


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


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


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


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


268 
under specific constraints.


269 


270 


271 


272 
\subsection{Binding operators}


273 


274 
Universal and existential quantifications may range over sets,


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


276 
bounded universal quantifier. Occasionally you will need to apply


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


278 
%


279 
\begin{isabelle}


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


281 
A.\ P\ x%


282 
\rulename{ballI}%


283 
\isanewline


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


285 
P\ x;\ x\ \isasymin\


286 
A\isasymrbrakk\ \isasymLongrightarrow\ P\


287 
x%


288 
\rulename{bspec}


289 
\end{isabelle}


290 
%


291 
Dually, here are the natural deduction rules for the


292 
bounded existential quantifier. You may need to apply


293 
\isa{bexI} with an explicit instantiation:


294 
\begin{isabelle}


295 
\isasymlbrakk P\ x;\


296 
x\ \isasymin\ A\isasymrbrakk\


297 
\isasymLongrightarrow\


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


299 
x%


300 
\rulename{bexI}%


301 
\isanewline


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


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


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


305 
P\ x\isasymrbrakk\ \isasymLongrightarrow\


306 
Q\isasymrbrakk\ \isasymLongrightarrow\ Q%


307 
\rulename{bexE}


308 
\end{isabelle}


309 


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


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


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


313 
\begin{isabelle}


314 
(b\ \isasymin\


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


316 
b\ \isasymin\ B\ x)


317 
\rulename{UN_iff}


318 
\end{isabelle}


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


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


321 
\begin{isabelle}


322 
\isasymlbrakk a\ \isasymin\


323 
A;\ b\ \isasymin\


324 
B\ a\isasymrbrakk\ \isasymLongrightarrow\


325 
b\ \isasymin\


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


327 
B\ x)


328 
\rulename{UN_I}%


329 
\isanewline


330 
\isasymlbrakk b\ \isasymin\


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


332 
B\ x);\


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


334 
A;\ b\ \isasymin\


335 
B\ x\isasymrbrakk\ \isasymLongrightarrow\


336 
R\isasymrbrakk\ \isasymLongrightarrow\ R%


337 
\rulename{UN_E}


338 
\end{isabelle}


339 
%


340 
The following builtin abbreviation lets us express the union


341 
over a \emph{type}:


342 
\begin{isabelle}


343 
\ \ \ \ \


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


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


346 
\end{isabelle}


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


348 
the


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


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


351 
displayed.


352 


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


354 
\textsc{ascii}:


355 
\begin{isabelle}


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


357 
\isasymin\ X)


358 
\rulename{Union_iff}


359 
\end{isabelle}


360 


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


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


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


364 
theorems are available:


365 
\begin{isabelle}


366 
(b\ \isasymin\


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


368 
B\ x))\


369 
=\


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


371 
b\ \isasymin\ B\ x)


372 
\rulename{INT_iff}%


373 
\isanewline


374 
(A\ \isasymin\


375 
\isasymInter C)\ =\


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


377 
A\ \isasymin\ X)


378 
\rulename{Inter_iff}


379 
\end{isabelle}


380 


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


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


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


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


385 


386 
The internal form of a comprehension involves the constant


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


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


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


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


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


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


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


394 


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


396 
One primitive not mentioned here is the powerset operator


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


398 
descendants.


399 


400 


401 
\subsection{Finiteness and cardinality}


402 


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


404 
many familiar theorems about finiteness and cardinality


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


406 
of unions, intersections and the powerset:


407 
%


408 
\begin{isabelle}


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


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


411 
\rulename{card_Un_Int}%


412 
\isanewline


413 
\isanewline


414 
finite\ A\ \isasymLongrightarrow\ card\


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


416 
\rulename{card_Pow}%


417 
\isanewline


418 
\isanewline


419 
finite\ A\ \isasymLongrightarrow\isanewline


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


421 
A\ \isasymand\ card\ B\ =\


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


423 
\rulename{n_subsets}


424 
\end{isabelle}


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


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


427 


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


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


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


431 
\isa{Finite}.


432 


433 


434 
\section{Functions}


435 


436 
This section describes a few concepts that involve functions.


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


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


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


440 


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


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


443 
\begin{isabelle}


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


445 
\rulename{ext}


446 
\end{isabelle}


447 


448 


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


450 
the obvious definition and many useful facts are proved about


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


452 
rule:


453 
\begin{isabelle}


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


455 
\rulename{fun_upd_apply}


456 
\end{isabelle}


457 
Two syntactic points must be noted. In


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


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


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


461 
\begin{isabelle}


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


463 
\rulename{fun_upd_upd}


464 
\end{isabelle}


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


466 
when it is not being applied to an argument.


467 


468 
\medskip


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


470 
follows:


471 
\begin{isabelle}%


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


473 
\rulename{id_def}\isanewline


474 
f\ \isasymcirc\ g\ \isasymequiv\


475 
{\isasymlambda}x.\ f\


476 
(g\ x)%


477 
\rulename{o_def}


478 
\end{isabelle}


479 
%


480 
Many familiar theorems concerning the identity and composition


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


482 
\begin{isabelle}


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


484 
\rulename{o_assoc}


485 
\end{isabelle}


486 


487 
\medskip


488 


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 
\rulename{inj_on_def}\isanewline


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


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


497 
\rulename{surj_def}\isanewline


498 
bij\ f\ \isasymequiv\ inj\ f\ \isasymand\ surj\ f


499 
\rulename{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 higherorder 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.


507 


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


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


510 
such as these:


511 
\begin{isabelle}


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


513 
\rulename{inv_f_f}\isanewline


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


515 
\rulename{surj_f_inv_f}\isanewline


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


517 
\rulename{inv_inv_eq}


518 
\end{isabelle}


519 
%


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


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


522 
%a bijection.


523 
%\begin{isabelle}


524 
%inj\ f\ \isasymLongrightarrow\ surj\


525 
%(inv\ f)


526 
%\rulename{inj_imp_surj_inv}\isanewline


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


528 
%\rulename{surj_imp_inj_inv}\isanewline


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


530 
%\rulename{bij_imp_bij_inv}


531 
%\end{isabelle}


532 
%


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


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


535 
%law:


536 
%\begin{isabelle}


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


538 
%\rulename{o_inv_distrib}


539 
%\end{isabelle}


540 


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


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


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


544 
equality over all arguments:


545 
\begin{isabelle}


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


547 
\rulename{expand_fun_eq}


548 
\end{isabelle}


549 


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


551 
that an injection can be cancelled from the left


552 
side of function composition:


553 
\begin{isabelle}


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


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


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


557 
\isacommand{done}


558 
\end{isabelle}


559 


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


561 
of injectiveness and composition. It leaves one subgoal:


562 
\begin{isabelle}


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


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


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


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


567 
\end{isabelle}


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


569 


570 
\medskip


571 


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


573 
has the obvious definition:


574 
\begin{isabelle}


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


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


577 
\rulename{image_def}


578 
\end{isabelle}


579 
%


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


581 
\begin{isabelle}


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


583 
\rulename{image_compose}\isanewline


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


585 
\rulename{image_Un}\isanewline


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


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


588 
\rulename{image_Int}


589 
%\isanewline


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


591 
%\rulename{bij_image_Compl_eq}


592 
\end{isabelle}


593 


594 


595 
Laws involving image can often be proved automatically. Here


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


597 
general syntax for comprehension:


598 
\begin{isabelle}


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


600 
x\isacharbraceright)


601 
\par\smallskip


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


603 
y\isacharbraceright"


604 
\end{isabelle}


605 


606 
\medskip


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


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


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


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


611 
\begin{isabelle}


612 
\ \ \ \ \ range\ f\


613 
{==}\ f``UNIV


614 
\end{isabelle}


615 
%


616 
Few theorems are proved specifically


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


618 
theorem concerning images.


619 


620 
\medskip


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


622 
\begin{isabelle}


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


624 
\rulename{vimage_def}


625 
\end{isabelle}


626 
%


627 
This is one of the facts proved about it:


628 
\begin{isabelle}


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


630 
\rulename{vimage_Compl}


631 
\end{isabelle}


632 


633 


634 
\section{Relations}


635 


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


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


638 
primitives are defined specifically for relations.


639 


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


641 
definition:


642 
\begin{isabelle}


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


644 
\rulename{Id_def}


645 
\end{isabelle}


646 


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


648 
\begin{isabelle}


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


650 
\rulename{comp_def}


651 
\end{isabelle}


652 


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


654 
\begin{isabelle}


655 
R\ O\ Id\ =\ R


656 
\rulename{R_O_Id}


657 
\end{isabelle}


658 
%


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


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


661 
one:


662 
\begin{isabelle}


663 
\isasymlbrakk r\isacharprime\ \isasymsubseteq\ r;\ s\isacharprime\


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


665 
s\isacharprime\ \isasymsubseteq\ r\ O\ s%


666 
\rulename{comp_mono}


667 
\end{isabelle}


668 


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


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


671 
operator.


672 
\begin{isabelle}


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


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


675 
\rulename{converse_iff}


676 
\end{isabelle}


677 
%


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


679 
\begin{isabelle}


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


681 
\rulename{converse_comp}


682 
\end{isabelle}


683 


684 


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


686 
to image under a function:


687 
\begin{isabelle}


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


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


690 
\rulename{Image_iff}


691 
\end{isabelle}


692 
It satisfies many similar laws.


693 


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


695 
%\begin{isabelle}


696 
%r\ \isacharcircum{\isacharcircum}\


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


698 
%B\


699 
%x)\ =\


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


701 
%r\ \isacharcircum{\isacharcircum}\ B\


702 
%x)


703 
%\rulename{Image_UN}


704 
%\end{isabelle}


705 


706 


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


708 
standard way:


709 
\begin{isabelle}


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


711 
r)


712 
\rulename{Domain_iff}%


713 
\isanewline


714 
(a\ \isasymin\ Range\ r)\


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


716 
(y,a)\


717 
\isasymin\ r)


718 
\rulename{Range_iff}


719 
\end{isabelle}


720 


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


722 
that of exponentiation:


723 
\begin{isabelle}


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


725 
R\ \isacharcircum\ Suc\ n\ =\ R\ O\ R\isacharcircum n


726 
\rulename{RelPow.relpow.simps}


727 
\end{isabelle}


728 


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


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


731 
construction is defined to be the least fixedpoint satisfying the


732 
following equation:


733 
\begin{isabelle}


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


735 
\rulename{rtrancl_unfold}


736 
\end{isabelle}


737 
%


738 
Among its basic properties are three that serve as introduction


739 
rules:


740 
\begin{isabelle}


741 
(a,a)\ \isasymin\


742 
r\isacharcircum{*}


743 
\rulename{rtrancl_refl}%


744 
\isanewline


745 
p\ \isasymin\ r\ \isasymLongrightarrow\


746 
p\ \isasymin\


747 
r\isacharcircum{*}


748 
\rulename{r_into_rtrancl}%


749 
\isanewline


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


751 
r\isacharcircum{*};\


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


753 
\isasymLongrightarrow\


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


755 
\rulename{rtrancl_trans}


756 
\end{isabelle}


757 
%


758 
Induction over the reflexive transitive closure is available:


759 
\begin{isabelle}


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


761 
\ \ {\isasymAnd}y\ z.\


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


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


764 
\isasymLongrightarrow\ P\ z\isasymrbrakk\isanewline


765 
\isasymLongrightarrow\ P\ b%


766 
\rulename{rtrancl_induct}


767 
\end{isabelle}


768 
%


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


770 
closure:


771 
\begin{isabelle}


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


773 
\rulename{rtrancl_idemp}


774 
\end{isabelle}


775 


776 
The transitive closure is similar. It has two


777 
introduction rules:


778 
\begin{isabelle}


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


780 
\rulename{r_into_trancl}\isanewline


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


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


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


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


785 
r\isacharcircum{\isacharplus}


786 
\rulename{trancl_trans}


787 
\end{isabelle}


788 
%


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


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


791 
operator:


792 
\begin{isabelle}


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


794 
\rulename{trancl_converse}


795 
\end{isabelle}


796 


797 


798 
The reflexive transitive closure also commutes with the converse.


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


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


801 
is the first one:


802 
\begin{isabelle}


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


804 
\isacommand{apply}\ (erule\


805 
rtrancl_induct)\isanewline


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


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


808 
\isacommand{done}


809 
\end{isabelle}


810 


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


812 
\begin{isabelle}


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


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


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


816 
\end{isabelle}


817 


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


819 
by first eliminating the converse operator, yielding the


820 
assumption \isa{(z,y)\


821 
\isasymin\ r}, and then


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


823 
the other direction:


824 
\begin{isabelle}


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


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


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


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


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


830 
\isacommand{done}


831 
\end{isabelle}


832 


833 


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


835 
\begin{isabelle}


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


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


838 
rtrancl_converseI\ dest:\


839 
rtrancl_converseD)\isanewline


840 
\isacommand{done}


841 
\end{isabelle}


842 


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


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


845 
This is because the


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


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


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


849 
point:


850 
\begin{isabelle}


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


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


853 
\isacommand{apply}\ (auto)


854 
\end{isabelle}


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


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


857 
\begin{isabelle}


858 
A\ \isasymsubseteq\ Id\isanewline


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


860 
\end{isabelle}


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


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


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


864 
can replace


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


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


867 
\begin{isabelle}


868 
A\ \isasymsubseteq\ Id\isanewline


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


870 
\end{isabelle}


871 


872 


873 


874 
\section{Wellfounded relations and induction}


875 


876 
Induction comes in many forms, including traditional mathematical


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


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


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


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


881 
infinite descending chains


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


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


884 
induction rule:


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


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


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


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


889 
reasoning are finite.


890 


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


892 
\begin{isabelle}


893 
{\isasymlbrakk}wf\ r;\


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


895 
\isasymlongrightarrow\ P\ y\ \isasymLongrightarrow\ P\ x\isasymrbrakk\


896 
\isasymLongrightarrow\ P\ a


897 
\rulename{wf_induct}


898 
\end{isabelle}


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


900 


901 
Many familiar induction principles are instances of this rule.


902 
For example, the predecessor relation on the natural numbers


903 
is wellfounded; induction over it is mathematical induction.


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


905 
it is structural induction.


906 


907 
Wellfoundedness can be difficult to show. The various equivalent


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


909 
is obviously wellfounded by construction. The HOL library provides


910 
several theorems concerning ways of constructing a wellfounded relation.


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


912 
involving an existing relation, or two relations can be


913 
combined lexicographically.


914 


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


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


917 
relation behaves as expected and that it is wellfounded:


918 
\begin{isabelle}


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


920 
\rulename{less_than_iff}\isanewline


921 
wf\ less_than


922 
\rulename{wf_less_than}


923 
\end{isabelle}


924 


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


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


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


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


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


930 
that it preserves wellfoundedness:


931 
\begin{isabelle}


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


933 
\isasymin\ r\isacharbraceright


934 
\rulename{inv_image_def}\isanewline


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


936 
\rulename{wf_inv_image}


937 
\end{isabelle}


938 


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


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


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


942 
\begin{isabelle}


943 
measure\ \isasymequiv\ inv_image\ less_than%


944 
\rulename{measure_def}\isanewline


945 
wf\ (measure\ f)


946 
\rulename{wf_measure}


947 
\end{isabelle}


948 


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


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


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


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


953 
usual definition and it preserves wellfoundedness:


954 
\begin{isabelle}


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


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


957 
\isasymor\isanewline


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


959 
\isasymin \ rb\isacharbraceright


960 
\rulename{lex_prod_def}%


961 
\par\smallskip


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


963 
\rulename{wf_lex_prod}


964 
\end{isabelle}


965 


966 
These constructions can be used in a


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


968 
the wellfounded relation used to prove termination.


969 


970 


971 


972 


973 


974 
\section{Fixed point operators}


975 


976 
Fixed point operators define sets recursively. Most users invoke


977 
them through Isabelle's inductive definition facility, which


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


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


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


981 
definition. Mathematicians may wish to note that the existence


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


983 


984 


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


986 
definition of monotone is overloaded over all orderings:


987 
\begin{isabelle}


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


989 
\rulename{mono_def}


990 
\end{isabelle}


991 
%


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


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


994 
definition, monotonicity has the obvious introduction and destruction


995 
rules:


996 
\begin{isabelle}


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


998 
\rulename{monoI}%


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


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


1001 
\isasymLongrightarrow\ f\ A\ \isasymle\ f\ B%


1002 
\rulename{monoD}


1003 
\end{isabelle}


1004 


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


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


1007 
\begin{isabelle}


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


1009 
\rulename{lfp_unfold}%


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


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


1012 
\ {\isasymAnd}x.\ x\


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


1014 
x\isacharbraceright)\ \isasymLongrightarrow\ P\ x\isasymrbrakk\


1015 
\isasymLongrightarrow\ P\ a%


1016 
\rulename{lfp_induct}


1017 
\end{isabelle}


1018 
%


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


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


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


1022 


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


1024 
\begin{isabelle}


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


1026 
\rulename{gfp_unfold}%


1027 
\isanewline


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


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


1030 
gfp\ f%


1031 
\rulename{coinduct}


1032 
\end{isabelle}


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


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


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


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


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


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


1039 
chapter, in the section on computation tree logic


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