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}

10372

636 
\label{sec:Relations}

10303

637 


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


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


640 
primitives are defined specifically for relations.


641 


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


643 
definition:


644 
\begin{isabelle}


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


646 
\rulename{Id_def}


647 
\end{isabelle}


648 


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


650 
\begin{isabelle}


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


652 
\rulename{comp_def}


653 
\end{isabelle}


654 


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


656 
\begin{isabelle}


657 
R\ O\ Id\ =\ R


658 
\rulename{R_O_Id}


659 
\end{isabelle}


660 
%


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


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


663 
one:


664 
\begin{isabelle}


665 
\isasymlbrakk r\isacharprime\ \isasymsubseteq\ r;\ s\isacharprime\


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


667 
s\isacharprime\ \isasymsubseteq\ r\ O\ s%


668 
\rulename{comp_mono}


669 
\end{isabelle}


670 


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


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


673 
operator.


674 
\begin{isabelle}


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


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


677 
\rulename{converse_iff}


678 
\end{isabelle}


679 
%


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


681 
\begin{isabelle}


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


683 
\rulename{converse_comp}


684 
\end{isabelle}


685 


686 


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


688 
to image under a function:


689 
\begin{isabelle}


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


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


692 
\rulename{Image_iff}


693 
\end{isabelle}


694 
It satisfies many similar laws.


695 


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


697 
%\begin{isabelle}


698 
%r\ \isacharcircum{\isacharcircum}\


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


700 
%B\


701 
%x)\ =\


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


703 
%r\ \isacharcircum{\isacharcircum}\ B\


704 
%x)


705 
%\rulename{Image_UN}


706 
%\end{isabelle}


707 


708 


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


710 
standard way:


711 
\begin{isabelle}


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


713 
r)


714 
\rulename{Domain_iff}%


715 
\isanewline


716 
(a\ \isasymin\ Range\ r)\


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


718 
(y,a)\


719 
\isasymin\ r)


720 
\rulename{Range_iff}


721 
\end{isabelle}


722 


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


724 
that of exponentiation:


725 
\begin{isabelle}


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


727 
R\ \isacharcircum\ Suc\ n\ =\ R\ O\ R\isacharcircum n


728 
\rulename{RelPow.relpow.simps}


729 
\end{isabelle}


730 


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


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


733 
construction is defined to be the least fixedpoint satisfying the


734 
following equation:


735 
\begin{isabelle}


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


737 
\rulename{rtrancl_unfold}


738 
\end{isabelle}


739 
%


740 
Among its basic properties are three that serve as introduction


741 
rules:


742 
\begin{isabelle}


743 
(a,a)\ \isasymin\


744 
r\isacharcircum{*}


745 
\rulename{rtrancl_refl}%


746 
\isanewline


747 
p\ \isasymin\ r\ \isasymLongrightarrow\


748 
p\ \isasymin\


749 
r\isacharcircum{*}


750 
\rulename{r_into_rtrancl}%


751 
\isanewline


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


753 
r\isacharcircum{*};\


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


755 
\isasymLongrightarrow\


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


757 
\rulename{rtrancl_trans}


758 
\end{isabelle}


759 
%


760 
Induction over the reflexive transitive closure is available:


761 
\begin{isabelle}


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


763 
\ \ {\isasymAnd}y\ z.\


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


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


766 
\isasymLongrightarrow\ P\ z\isasymrbrakk\isanewline


767 
\isasymLongrightarrow\ P\ b%


768 
\rulename{rtrancl_induct}


769 
\end{isabelle}


770 
%


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


772 
closure:


773 
\begin{isabelle}


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


775 
\rulename{rtrancl_idemp}


776 
\end{isabelle}


777 


778 
The transitive closure is similar. It has two


779 
introduction rules:


780 
\begin{isabelle}


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


782 
\rulename{r_into_trancl}\isanewline


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


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


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


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


787 
r\isacharcircum{\isacharplus}


788 
\rulename{trancl_trans}


789 
\end{isabelle}


790 
%


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


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


793 
operator:


794 
\begin{isabelle}


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


796 
\rulename{trancl_converse}


797 
\end{isabelle}


798 


799 


800 
The reflexive transitive closure also commutes with the converse.


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


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


803 
is the first one:


804 
\begin{isabelle}


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


806 
\isacommand{apply}\ (erule\


807 
rtrancl_induct)\isanewline


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


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


810 
\isacommand{done}


811 
\end{isabelle}


812 


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


814 
\begin{isabelle}


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


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


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


818 
\end{isabelle}


819 


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


821 
by first eliminating the converse operator, yielding the


822 
assumption \isa{(z,y)\


823 
\isasymin\ r}, and then


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


825 
the other direction:


826 
\begin{isabelle}


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


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


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


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


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


832 
\isacommand{done}


833 
\end{isabelle}


834 


835 


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


837 
\begin{isabelle}


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


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


840 
rtrancl_converseI\ dest:\


841 
rtrancl_converseD)\isanewline


842 
\isacommand{done}


843 
\end{isabelle}


844 


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


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


847 
This is because the


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


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


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


851 
point:


852 
\begin{isabelle}


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


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


855 
\isacommand{apply}\ (auto)


856 
\end{isabelle}


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


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


859 
\begin{isabelle}


860 
A\ \isasymsubseteq\ Id\isanewline


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


862 
\end{isabelle}


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


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


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


866 
can replace


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


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


869 
\begin{isabelle}


870 
A\ \isasymsubseteq\ Id\isanewline


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


872 
\end{isabelle}


873 


874 


875 


876 
\section{Wellfounded relations and induction}

10373

877 
\label{sec:Wellfounded}

10303

878 


879 
Induction comes in many forms, including traditional mathematical


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


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


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


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


884 
infinite descending chains


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

10374

886 
If $\prec$ is wellfounded then it can be used with the \textbf{wellfounded


887 
induction}\indexbold{induction!wellfounded}\index{wellfounded


888 
inductionsee{induction, wellfounded}} rule:

10303

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


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


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


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

10374

893 
reasoning are finite. For a fuller account of wellfounded relations and


894 
induction see, for example, \cite{BaaderNipkow}.

10303

895 


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


897 
\begin{isabelle}


898 
{\isasymlbrakk}wf\ r;\


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


900 
\isasymlongrightarrow\ P\ y\ \isasymLongrightarrow\ P\ x\isasymrbrakk\


901 
\isasymLongrightarrow\ P\ a


902 
\rulename{wf_induct}


903 
\end{isabelle}


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


905 


906 
Many familiar induction principles are instances of this rule.


907 
For example, the predecessor relation on the natural numbers


908 
is wellfounded; induction over it is mathematical induction.


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


910 
it is structural induction.


911 


912 
Wellfoundedness can be difficult to show. The various equivalent


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


914 
is obviously wellfounded by construction. The HOL library provides


915 
several theorems concerning ways of constructing a wellfounded relation.


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


917 
involving an existing relation, or two relations can be


918 
combined lexicographically.


919 


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


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


922 
relation behaves as expected and that it is wellfounded:


923 
\begin{isabelle}


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


925 
\rulename{less_than_iff}\isanewline


926 
wf\ less_than


927 
\rulename{wf_less_than}


928 
\end{isabelle}


929 


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


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


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


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


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


935 
that it preserves wellfoundedness:


936 
\begin{isabelle}


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


938 
\isasymin\ r\isacharbraceright


939 
\rulename{inv_image_def}\isanewline


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


941 
\rulename{wf_inv_image}


942 
\end{isabelle}


943 


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


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


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


947 
\begin{isabelle}


948 
measure\ \isasymequiv\ inv_image\ less_than%


949 
\rulename{measure_def}\isanewline


950 
wf\ (measure\ f)


951 
\rulename{wf_measure}


952 
\end{isabelle}


953 


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


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


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


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


958 
usual definition and it preserves wellfoundedness:


959 
\begin{isabelle}


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


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


962 
\isasymor\isanewline


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


964 
\isasymin \ rb\isacharbraceright


965 
\rulename{lex_prod_def}%


966 
\par\smallskip


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


968 
\rulename{wf_lex_prod}


969 
\end{isabelle}


970 


971 
These constructions can be used in a


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


973 
the wellfounded relation used to prove termination.


974 


975 


976 


977 


978 


979 
\section{Fixed point operators}


980 


981 
Fixed point operators define sets recursively. Most users invoke


982 
them through Isabelle's inductive definition facility, which


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


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


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


986 
definition. Mathematicians may wish to note that the existence


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


988 


989 


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


991 
definition of monotone is overloaded over all orderings:


992 
\begin{isabelle}


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


994 
\rulename{mono_def}


995 
\end{isabelle}


996 
%


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


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


999 
definition, monotonicity has the obvious introduction and destruction


1000 
rules:


1001 
\begin{isabelle}


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


1003 
\rulename{monoI}%


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


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


1006 
\isasymLongrightarrow\ f\ A\ \isasymle\ f\ B%


1007 
\rulename{monoD}


1008 
\end{isabelle}


1009 


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


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


1012 
\begin{isabelle}


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


1014 
\rulename{lfp_unfold}%


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


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


1017 
\ {\isasymAnd}x.\ x\


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


1019 
x\isacharbraceright)\ \isasymLongrightarrow\ P\ x\isasymrbrakk\


1020 
\isasymLongrightarrow\ P\ a%


1021 
\rulename{lfp_induct}


1022 
\end{isabelle}


1023 
%


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


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


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


1027 


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


1029 
\begin{isabelle}


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


1031 
\rulename{gfp_unfold}%


1032 
\isanewline


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


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


1035 
gfp\ f%


1036 
\rulename{coinduct}


1037 
\end{isabelle}


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


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


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


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


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


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


1044 
chapter, in the section on computation tree logic


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