10857

1 
% $Id$

10303

2 
\chapter{Sets, Functions and Relations}


3 

10857

4 
\REMARK{The old version used lots of bold. I've cut down,


5 
changing some \texttt{textbf} to \texttt{relax}. This can be undone.


6 
See the source.}

10303

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

10857

8 
but images, least fixed points and other concepts. In computer science,


9 
sets are used to formalize grammars, state transition systems, etc. The set


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


11 
theory, in which everything is a set. Our sets are typed. In a given set,


12 
all elements have the same type, say~$\tau$, and the set itself has type


13 
\isa{$\tau$~set}.

10303

14 


15 
Relations are simply sets of pairs. This chapter describes


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

10857

17 
transitive closure. Functions are also covered. They are not sets in


18 
Isabelle/HOL, but many of their properties concern sets. The range of a


19 
function is a set, and the inverse image of a function maps sets to sets.

10303

20 


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


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


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


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


25 
the notation.


26 


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


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


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


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


31 
easier.


32 


33 


34 
\section{Sets}


35 

10857

36 
We begin with \relax{intersection}, \relax{union} and


37 
\relax{complement}. In addition to the


38 
\relax{membership} relation, there is a symbol for its negation. These


39 
points can be seen below.

10303

40 


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


42 
resemblance to those for conjunction.


43 
\begin{isabelle}

10857

44 
\isasymlbrakk c\ \isasymin\ A;\ c\ \isasymin\ B\isasymrbrakk\


45 
\isasymLongrightarrow\ c\ \isasymin\ A\ \isasyminter\ B%

10303

46 
\rulename{IntI}\isanewline

10857

47 
c\ \isasymin\ A\ \isasyminter\ B\ \isasymLongrightarrow\ c\ \isasymin\ A

10303

48 
\rulename{IntD1}\isanewline

10857

49 
c\ \isasymin\ A\ \isasyminter\ B\ \isasymLongrightarrow\ c\ \isasymin\ B


50 
\rulename{IntD2}

10303

51 
\end{isabelle}


52 

10857

53 
Here are two of the many installed theorems concerning set complement.


54 
Note that it is denoted by a minus sign.

10303

55 
\begin{isabelle}

10857

56 
(c\ \isasymin\ \ A)\ =\ (c\ \isasymnotin\ A)

10303

57 
\rulename{Compl_iff}\isanewline

10857

58 
\ (A\ \isasymunion\ B)\ =\ \ A\ \isasyminter\ \ B

10303

59 
\rulename{Compl_Un}


60 
\end{isabelle}


61 

10857

62 
Set \relax{difference} is the intersection of a set with the

10303

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


64 
empty set and for the universal set.


65 
\begin{isabelle}

10857

66 
A\ \isasyminter\ (B\ \ A)\ =\ \isacharbraceleft\isacharbraceright


67 
\rulename{Diff_disjoint}\isanewline


68 
A\ \isasymunion\ \ A\ =\ UNIV%

10303

69 
\rulename{Compl_partition}


70 
\end{isabelle}


71 

10857

72 
The \relax{subset} relation holds between two sets just if every element

10303

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


74 
are its natural deduction rules:


75 
\begin{isabelle}


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


77 
\rulename{subsetI}%


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


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


80 
A\isasymrbrakk\ \isasymLongrightarrow\ c\


81 
\isasymin\ B%


82 
\rulename{subsetD}


83 
\end{isabelle}


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


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


86 
one:


87 
\begin{isabelle}

10857

88 
(A\ \isasymunion\ B\ \isasymsubseteq\ C)\ =\


89 
(A\ \isasymsubseteq\ C\ \isasymand\ B\ \isasymsubseteq\ C)

10303

90 
\rulename{Un_subset_iff}


91 
\end{isabelle}


92 
Here is another example, also proved automatically:


93 
\begin{isabelle}


94 
\isacommand{lemma}\ "(A\

10857

95 
\isasymsubseteq\ B)\ =\ (B\ \isasymsubseteq\ A)"\isanewline


96 
\isacommand{by}\ blast

10303

97 
\end{isabelle}


98 
%


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


100 
\begin{isabelle}

10857

101 
\isacommand{lemma}\ "(A\ <=\ B)\ =\ (B\ <=\ A)"

10303

102 
\end{isabelle}


103 
%


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


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


106 
subset.


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


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


109 
proof to succeed:


110 


111 
\begin{isabelle}

10857

112 
\isacommand{lemma}\ "((A::\ {\isacharprime}a\ set)\ <=\ B)\ =\ (B\ <=\

10303

113 
A)"


114 
\end{isabelle}

10857

115 
Section~\ref{sec:axclass} below describes overloading. Incidentally,


116 
\isa{A~\isasymsubseteq~B} asserts that the sets \isa{A} and \isa{B} are


117 
disjoint.

10303

118 


119 
\medskip

10857

120 
Two sets are \relax{equal} if they contain the same elements.

10303

121 
This is


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


123 
\begin{isabelle}


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


125 
{\isasymLongrightarrow}\ A\ =\ B


126 
\rulename{set_ext}


127 
\end{isabelle}


128 
Extensionality is often expressed as


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


130 
The following rules express both


131 
directions of this equivalence. Proving a set equation using


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


133 
\begin{isabelle}


134 
\isasymlbrakk A\ \isasymsubseteq\ B;\ B\ \isasymsubseteq\

10857

135 
A\isasymrbrakk\ \isasymLongrightarrow\ A\ =\ B

10303

136 
\rulename{equalityI}


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


138 
\isasymlbrakk A\ =\ B;\ \isasymlbrakk A\ \isasymsubseteq\ B;\ B\


139 
\isasymsubseteq\ A\isasymrbrakk\ \isasymLongrightarrow\ P\isasymrbrakk\


140 
\isasymLongrightarrow\ P%


141 
\rulename{equalityE}


142 
\end{isabelle}


143 


144 

10857

145 
\subsection{Finite Set Notation}

10303

146 


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

10857

148 
a form of union:

10303

149 
\begin{isabelle}

10857

150 
insert\ a\ A\ =\ \isacharbraceleft a\isacharbraceright\ \isasymunion\ A

10303

151 
\rulename{insert_is_Un}


152 
\end{isabelle}


153 
%


154 
The finite set expression \isa{\isacharbraceleft


155 
a,b\isacharbraceright} abbreviates


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

10857

157 
Many facts about finite sets can be proved automatically:

10303

158 
\begin{isabelle}


159 
\isacommand{lemma}\

10857

160 
"\isacharbraceleft a,b\isacharbraceright\


161 
\isasymunion\ \isacharbraceleft c,d\isacharbraceright\ =\


162 
\isacharbraceleft a,b,c,d\isacharbraceright"\isanewline


163 
\isacommand{by}\ blast

10303

164 
\end{isabelle}


165 


166 


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

10857

168 
Consider this attempt:

10303

169 
\begin{isabelle}

10857

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


171 
\isacharbraceleft b\isacharbraceright"\isanewline


172 
\isacommand{apply}\ auto

10303

173 
\end{isabelle}


174 
%


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


176 
fails, consider a correct version:


177 
\begin{isabelle}

10857

178 
\isacommand{lemma}\ "\isacharbraceleft a,b\isacharbraceright\ \isasyminter\


179 
\isacharbraceleft b,c\isacharbraceright\ =\ (if\ a=c\ then\


180 
\isacharbraceleft a,b\isacharbraceright\ else\ \isacharbraceleft


181 
b\isacharbraceright)"\isanewline


182 
\isacommand{apply}\ simp\isanewline


183 
\isacommand{by}\ blast

10303

184 
\end{isabelle}


185 


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


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


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


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


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

10857

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

10303

192 


193 

10857

194 
\subsection{Set Comprehension}

10303

195 

10857

196 
The set comprehension \isa{\isacharbraceleft x.\


197 
P\isacharbraceright} expresses the set of all elements that satisfy the


198 
predicate~\isa{P}. Two laws describe the relationship between set


199 
comprehension and the membership relation:

10303

200 
\begin{isabelle}


201 
(a\ \isasymin\

10857

202 
\isacharbraceleft x.\ P\ x\isacharbraceright)\ =\ P\ a


203 
\rulename{mem_Collect_eq}\isanewline


204 
\isacharbraceleft x.\ x\ \isasymin\ A\isacharbraceright\ =\ A

10303

205 
\rulename{Collect_mem_eq}


206 
\end{isabelle}


207 

10857

208 
\smallskip

10303

209 
Facts such as these have trivial proofs:


210 
\begin{isabelle}

10857

211 
\isacommand{lemma}\ "\isacharbraceleft x.\ P\ x\ \isasymor\

10303

212 
x\ \isasymin\ A\isacharbraceright\ =\

10857

213 
\isacharbraceleft x.\ P\ x\isacharbraceright\ \isasymunion\ A"

10303

214 
\par\smallskip

10857

215 
\isacommand{lemma}\ "\isacharbraceleft x.\ P\ x\

10303

216 
\isasymlongrightarrow\ Q\ x\isacharbraceright\ =\

10857

217 
\isacharbraceleft x.\ P\ x\isacharbraceright\


218 
\isasymunion\ \isacharbraceleft x.\ Q\ x\isacharbraceright"

10303

219 
\end{isabelle}


220 

10857

221 
\smallskip

10303

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


223 
described through an example:


224 
\begin{isabelle}

10857

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

10303

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


227 
\isanewline

10857

228 
\ \ \ \ \ \ \ \ \isacharbraceleft z.\ \isasymexists p\ q.\ z\ =\ p*q\

10303

229 
\isasymand\ p{\isasymin}prime\ \isasymand\


230 
q{\isasymin}prime\isacharbraceright"


231 
\end{isabelle}


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


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


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

10857

235 
that are the product of two primes. The syntax provides a neat

10303

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

10857

237 
under specific constraints. The drawback is that it hides the true form of


238 
the expression, with its existential quantifiers.


239 


240 
\smallskip


241 
\emph{Remark}. We do not need sets at all. They are essentially equivalent


242 
to predicate variables, which are allowed in higherorder logic. The main


243 
benefit of sets is their notation; we can write \isa{x{\isasymin}A}


244 
and


245 
\isa{\isacharbraceleft z.\ P\isacharbraceright} where predicates would


246 
require writing


247 
\isa{A(x)} and


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

10303

249 


250 

10857

251 
\subsection{Binding Operators}

10303

252 


253 
Universal and existential quantifications may range over sets,


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


255 
bounded universal quantifier. Occasionally you will need to apply


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


257 
%


258 
\begin{isabelle}


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


260 
A.\ P\ x%


261 
\rulename{ballI}%


262 
\isanewline


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


264 
P\ x;\ x\ \isasymin\


265 
A\isasymrbrakk\ \isasymLongrightarrow\ P\


266 
x%


267 
\rulename{bspec}


268 
\end{isabelle}


269 
%


270 
Dually, here are the natural deduction rules for the


271 
bounded existential quantifier. You may need to apply


272 
\isa{bexI} with an explicit instantiation:


273 
\begin{isabelle}


274 
\isasymlbrakk P\ x;\


275 
x\ \isasymin\ A\isasymrbrakk\


276 
\isasymLongrightarrow\

10857

277 
\isasymexists x\isasymin A.\ P\

10303

278 
x%


279 
\rulename{bexI}%


280 
\isanewline

10857

281 
\isasymlbrakk\isasymexists x\isasymin A.\

10303

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


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


284 
P\ x\isasymrbrakk\ \isasymLongrightarrow\


285 
Q\isasymrbrakk\ \isasymLongrightarrow\ Q%


286 
\rulename{bexE}


287 
\end{isabelle}


288 


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


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


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


292 
\begin{isabelle}


293 
(b\ \isasymin\

10857

294 
(\isasymUnion x\isasymin A.\ B\ x))\ =\ (\isasymexists x\isasymin A.\

10303

295 
b\ \isasymin\ B\ x)


296 
\rulename{UN_iff}


297 
\end{isabelle}


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


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


300 
\begin{isabelle}


301 
\isasymlbrakk a\ \isasymin\


302 
A;\ b\ \isasymin\


303 
B\ a\isasymrbrakk\ \isasymLongrightarrow\


304 
b\ \isasymin\


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


306 
B\ x)


307 
\rulename{UN_I}%


308 
\isanewline


309 
\isasymlbrakk b\ \isasymin\


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


311 
B\ x);\


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


313 
A;\ b\ \isasymin\


314 
B\ x\isasymrbrakk\ \isasymLongrightarrow\


315 
R\isasymrbrakk\ \isasymLongrightarrow\ R%


316 
\rulename{UN_E}


317 
\end{isabelle}


318 
%


319 
The following builtin abbreviation lets us express the union


320 
over a \emph{type}:


321 
\begin{isabelle}


322 
\ \ \ \ \


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


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


325 
\end{isabelle}


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


327 
the


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


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


330 
displayed.


331 


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


333 
\textsc{ascii}:


334 
\begin{isabelle}

10857

335 
(A\ \isasymin\ \isasymUnion C)\ =\ (\isasymexists X\isasymin C.\ A\

10303

336 
\isasymin\ X)


337 
\rulename{Union_iff}


338 
\end{isabelle}


339 


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


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


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


343 
theorems are available:


344 
\begin{isabelle}


345 
(b\ \isasymin\


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


347 
B\ x))\


348 
=\


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


350 
b\ \isasymin\ B\ x)


351 
\rulename{INT_iff}%


352 
\isanewline


353 
(A\ \isasymin\


354 
\isasymInter C)\ =\


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


356 
A\ \isasymin\ X)


357 
\rulename{Inter_iff}


358 
\end{isabelle}


359 


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


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


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


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


364 


365 
The internal form of a comprehension involves the constant


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


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

10857

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

10303

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


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

10857

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

10303

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


373 


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


375 
One primitive not mentioned here is the powerset operator


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


377 
descendants.


378 


379 

10857

380 
\subsection{Finiteness and Cardinality}

10303

381 


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


383 
many familiar theorems about finiteness and cardinality


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


385 
of unions, intersections and the powerset:


386 
%


387 
\begin{isabelle}


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


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


390 
\rulename{card_Un_Int}%


391 
\isanewline


392 
\isanewline


393 
finite\ A\ \isasymLongrightarrow\ card\


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


395 
\rulename{card_Pow}%


396 
\isanewline


397 
\isanewline


398 
finite\ A\ \isasymLongrightarrow\isanewline

10857

399 
card\ \isacharbraceleft B.\ B\ \isasymsubseteq\

10303

400 
A\ \isasymand\ card\ B\ =\


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


402 
\rulename{n_subsets}


403 
\end{isabelle}


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

10888

405 
$k$element subsets of~$A$ is $\binom{n}{k}$.

10303

406 

10857

407 
\begin{warn}


408 
The term \isa{Finite\ A} is an abbreviation for

10303

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

10857

410 
set of all finite sets of a given type. There is no constant

10303

411 
\isa{Finite}.

10857

412 
\end{warn}

10303

413 


414 


415 
\section{Functions}


416 


417 
This section describes a few concepts that involve functions.


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


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

10857

420 
we cannot simply state lemmas and expect them to be proved using


421 
\isa{blast}.

10303

422 

10857

423 
\subsection{Function Basics}


424 


425 
Two functions are \relax{equal} if they yield equal results given equal arguments.

10303

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


427 
\begin{isabelle}


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


429 
\rulename{ext}


430 
\end{isabelle}


431 


432 


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


434 
the obvious definition and many useful facts are proved about


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


436 
rule:


437 
\begin{isabelle}


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


439 
\rulename{fun_upd_apply}


440 
\end{isabelle}


441 
Two syntactic points must be noted. In


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


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


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


445 
\begin{isabelle}


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


447 
\rulename{fun_upd_upd}


448 
\end{isabelle}


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


450 
when it is not being applied to an argument.


451 


452 
\medskip

10857

453 
The \relax{identity} function and function \relax{composition} are defined:

10303

454 
\begin{isabelle}%


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


456 
\rulename{id_def}\isanewline


457 
f\ \isasymcirc\ g\ \isasymequiv\


458 
{\isasymlambda}x.\ f\


459 
(g\ x)%


460 
\rulename{o_def}


461 
\end{isabelle}


462 
%


463 
Many familiar theorems concerning the identity and composition


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


465 
\begin{isabelle}


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


467 
\rulename{o_assoc}


468 
\end{isabelle}


469 

10857

470 
\subsection{Injections, Surjections, Bijections}

10303

471 

10857

472 
A function may be \relax{injective}, \relax{surjective} or \relax{bijective}:

10303

473 
\begin{isabelle}


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


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


476 
=\ y%


477 
\rulename{inj_on_def}\isanewline


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

10857

479 
\isasymexists x.\ y\ =\ f\ x%

10303

480 
\rulename{surj_def}\isanewline


481 
bij\ f\ \isasymequiv\ inj\ f\ \isasymand\ surj\ f


482 
\rulename{bij_def}


483 
\end{isabelle}


484 
The second argument


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


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


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


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


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


490 

10857

491 
The operator {\isa{inv}} expresses the \relax{inverse} of a function. In

10303

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


493 
such as these:


494 
\begin{isabelle}


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


496 
\rulename{inv_f_f}\isanewline


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


498 
\rulename{surj_f_inv_f}\isanewline


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


500 
\rulename{inv_inv_eq}


501 
\end{isabelle}


502 
%


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


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


505 
%a bijection.


506 
%\begin{isabelle}


507 
%inj\ f\ \isasymLongrightarrow\ surj\


508 
%(inv\ f)


509 
%\rulename{inj_imp_surj_inv}\isanewline


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


511 
%\rulename{surj_imp_inj_inv}\isanewline


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


513 
%\rulename{bij_imp_bij_inv}


514 
%\end{isabelle}


515 
%


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


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


518 
%law:


519 
%\begin{isabelle}


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


521 
%\rulename{o_inv_distrib}


522 
%\end{isabelle}


523 


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


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


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


527 
equality over all arguments:


528 
\begin{isabelle}


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


530 
\rulename{expand_fun_eq}


531 
\end{isabelle}

10857

532 
%

10303

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


534 
that an injection can be cancelled from the left


535 
side of function composition:


536 
\begin{isabelle}


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


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

10857

539 
\isacommand{apply}\ auto\isanewline

10303

540 
\isacommand{done}


541 
\end{isabelle}


542 


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


544 
of injectiveness and composition. It leaves one subgoal:


545 
\begin{isabelle}

10857

546 
\ 1.\ {\isasymforall}x\ y.\ f\ x\ =\ f\ y\ \isasymlongrightarrow\ x\ =\ y\


547 
\isasymLongrightarrow\isanewline

10303

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


549 
\end{isabelle}

10857

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


551 

10303

552 

10857

553 
\subsection{Function Image}

10303

554 

10857

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

10303

556 
has the obvious definition:


557 
\begin{isabelle}

10857

558 
f\ `\ A\ \isasymequiv\ \isacharbraceleft y.\ \isasymexists x\isasymin

10303

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


560 
\rulename{image_def}


561 
\end{isabelle}


562 
%


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


564 
\begin{isabelle}

10857

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

10303

566 
\rulename{image_compose}\isanewline

10857

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

10303

568 
\rulename{image_Un}\isanewline

10857

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


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

10303

571 
\rulename{image_Int}


572 
%\isanewline

10857

573 
%bij\ f\ \isasymLongrightarrow\ f\ `\ (\ A)\ =\ \ f\ `\ A%

10303

574 
%\rulename{bij_image_Compl_eq}


575 
\end{isabelle}


576 


577 


578 
Laws involving image can often be proved automatically. Here


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


580 
general syntax for comprehension:


581 
\begin{isabelle}

10857

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

10303

583 
x\isacharbraceright)


584 
\par\smallskip

10857

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

10303

586 
y\isacharbraceright"


587 
\end{isabelle}


588 


589 
\medskip


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


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


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


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


594 
\begin{isabelle}


595 
\ \ \ \ \ range\ f\

10857

596 
{==}\ f`UNIV

10303

597 
\end{isabelle}


598 
%


599 
Few theorems are proved specifically


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


601 
theorem concerning images.


602 


603 
\medskip

10857

604 
\relax{Inverse image} is also useful. It is defined as follows:

10303

605 
\begin{isabelle}

10857

606 
f\ `\ B\ \isasymequiv\ \isacharbraceleft x.\ f\ x\ \isasymin\ B\isacharbraceright

10303

607 
\rulename{vimage_def}


608 
\end{isabelle}


609 
%


610 
This is one of the facts proved about it:


611 
\begin{isabelle}

10857

612 
f\ `\ (\ A)\ =\ \ f\ `\ A%

10303

613 
\rulename{vimage_Compl}


614 
\end{isabelle}


615 


616 


617 
\section{Relations}

10513

618 
\label{sec:Relations}

10303

619 

10857

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

10303

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


622 
primitives are defined specifically for relations.


623 

10857

624 
\subsection{Relation Basics}


625 


626 
The \relax{identity} relation, also known as equality, has the obvious

10303

627 
definition:


628 
\begin{isabelle}

10857

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

10303

630 
\rulename{Id_def}


631 
\end{isabelle}


632 

10857

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

10303

634 
\begin{isabelle}

10857

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

10303

636 
\rulename{comp_def}


637 
\end{isabelle}

10857

638 
%

10303

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


640 
\begin{isabelle}


641 
R\ O\ Id\ =\ R


642 
\rulename{R_O_Id}


643 
\end{isabelle}


644 
%


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


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


647 
one:


648 
\begin{isabelle}


649 
\isasymlbrakk r\isacharprime\ \isasymsubseteq\ r;\ s\isacharprime\


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


651 
s\isacharprime\ \isasymsubseteq\ r\ O\ s%


652 
\rulename{comp_mono}


653 
\end{isabelle}


654 

10857

655 
The \relax{converse} or inverse of a relation exchanges the roles

10303

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


657 
operator.


658 
\begin{isabelle}


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


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


661 
\rulename{converse_iff}


662 
\end{isabelle}


663 
%


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


665 
\begin{isabelle}

10857

666 
(r\ O\ s){\isacharcircum}1\ =\ s\isacharcircum1\ O\ r\isacharcircum1

10303

667 
\rulename{converse_comp}


668 
\end{isabelle}


669 

10857

670 
The \relax{image} of a set under a relation is defined analogously

10303

671 
to image under a function:


672 
\begin{isabelle}

10857

673 
(b\ \isasymin\ r\ ``\ A)\ =\ (\isasymexists x\isasymin

10303

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


675 
\rulename{Image_iff}


676 
\end{isabelle}


677 
It satisfies many similar laws.


678 


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


680 
%\begin{isabelle}

10857

681 
%r\ ``\

10303

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


683 
%B\


684 
%x)\ =\


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

10857

686 
%r\ ``\ B\

10303

687 
%x)


688 
%\rulename{Image_UN}


689 
%\end{isabelle}


690 


691 

10857

692 
The \relax{domain} and \relax{range} of a relation are defined in the

10303

693 
standard way:


694 
\begin{isabelle}

10857

695 
(a\ \isasymin\ Domain\ r)\ =\ (\isasymexists y.\ (a,y)\ \isasymin\

10303

696 
r)


697 
\rulename{Domain_iff}%


698 
\isanewline


699 
(a\ \isasymin\ Range\ r)\

10857

700 
\ =\ (\isasymexists y.\

10303

701 
(y,a)\


702 
\isasymin\ r)


703 
\rulename{Range_iff}


704 
\end{isabelle}


705 


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


707 
that of exponentiation:


708 
\begin{isabelle}


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


710 
R\ \isacharcircum\ Suc\ n\ =\ R\ O\ R\isacharcircum n


711 
\rulename{RelPow.relpow.simps}


712 
\end{isabelle}


713 

10857

714 
\subsection{The Reflexive Transitive Closure}


715 


716 
The \relax{reflexive transitive closure} of the

10398

717 
relation~\isa{r} is written with the

10857

718 
postfix syntax \isa{r\isacharcircum{*}} and appears in Xsymbol notation


719 
as~\isa{r\isactrlsup *}. It is the least solution of the equation

10303

720 
\begin{isabelle}

10857

721 
r\isactrlsup *\ =\ Id\ \isasymunion \ (r\ O\ r\isactrlsup *)

10303

722 
\rulename{rtrancl_unfold}


723 
\end{isabelle}


724 
%


725 
Among its basic properties are three that serve as introduction


726 
rules:


727 
\begin{isabelle}

10857

728 
(a,\ a)\ \isasymin \ r\isactrlsup *


729 
\rulename{rtrancl_refl}\isanewline


730 
p\ \isasymin \ r\ \isasymLongrightarrow \ p\ \isasymin \ r\isactrlsup *


731 
\rulename{r_into_rtrancl}\isanewline


732 
\isasymlbrakk (a,b)\ \isasymin \ r\isactrlsup *;\


733 
(b,c)\ \isasymin \ r\isactrlsup *\isasymrbrakk \ \isasymLongrightarrow \


734 
(a,c)\ \isasymin \ r\isactrlsup *

10303

735 
\rulename{rtrancl_trans}


736 
\end{isabelle}


737 
%


738 
Induction over the reflexive transitive closure is available:


739 
\begin{isabelle}

10857

740 
\isasymlbrakk (a,\ b)\ \isasymin \ r\isactrlsup *;\ P\ a;\ \isasymAnd y\ z.\ \isasymlbrakk (a,\ y)\ \isasymin \ r\isactrlsup *;\ (y,\ z)\ \isasymin \ r;\ P\ y\isasymrbrakk \ \isasymLongrightarrow \ P\ z\isasymrbrakk \isanewline


741 
\isasymLongrightarrow \ P\ b%

10303

742 
\rulename{rtrancl_induct}


743 
\end{isabelle}


744 
%

10857

745 
Idempotence is one of the laws proved about the reflexive transitive

10303

746 
closure:


747 
\begin{isabelle}

10857

748 
(r\isactrlsup *)\isactrlsup *\ =\ r\isactrlsup *

10303

749 
\rulename{rtrancl_idemp}


750 
\end{isabelle}


751 

10857

752 
\smallskip

10303

753 
The transitive closure is similar. It has two


754 
introduction rules:


755 
\begin{isabelle}

10857

756 
p\ \isasymin \ r\ \isasymLongrightarrow \ p\ \isasymin \ r\isactrlsup +

10303

757 
\rulename{r_into_trancl}\isanewline

10857

758 
\isasymlbrakk (a,\ b)\ \isasymin \ r\isactrlsup +;\ (b,\ c)\ \isasymin \ r\isactrlsup +\isasymrbrakk \ \isasymLongrightarrow \ (a,\ c)\ \isasymin \ r\isactrlsup +

10303

759 
\rulename{trancl_trans}


760 
\end{isabelle}


761 
%

10857

762 
The induction rule resembles the one shown above.

10303

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


764 
operator:


765 
\begin{isabelle}

10857

766 
(r\isasyminverse )\isactrlsup +\ =\ (r\isactrlsup +)\isasyminverse

10303

767 
\rulename{trancl_converse}


768 
\end{isabelle}


769 

10857

770 
\subsection{A Sample Proof}

10303

771 


772 
The reflexive transitive closure also commutes with the converse.


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


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


775 
is the first one:


776 
\begin{isabelle}

10857

777 
\isacommand{lemma}\ rtrancl_converseD:\ "(x,y)\ \isasymin \ (r\isacharcircum 1)\isacharcircum *\ \isasymLongrightarrow \ (y,x)\ \isasymin \ r\isacharcircum *"\isanewline


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

10303

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

10857

780 
\isacommand{apply}\ (blast\ intro:\ r_into_rtrancl\


781 
rtrancl_trans)\isanewline

10303

782 
\isacommand{done}


783 
\end{isabelle}

10857

784 
%

10303

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


786 
\begin{isabelle}

10857

787 
\ 1.\ (x,\ x)\ \isasymin \ r\isactrlsup *\isanewline


788 
\ 2.\ \isasymAnd y\ z.\ \isasymlbrakk (x,y)\ \isasymin \ (r\isasyminverse )\isactrlsup *;\ (y,z)\ \isasymin \ r\isasyminverse ;\ (y,x)\ \isasymin \ r\isactrlsup *\isasymrbrakk \isanewline


789 
\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (z,x)\ \isasymin \ r\isactrlsup *

10303

790 
\end{isabelle}

10857

791 
%

10303

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


793 
by first eliminating the converse operator, yielding the


794 
assumption \isa{(z,y)\


795 
\isasymin\ r}, and then


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


797 
the other direction:


798 
\begin{isabelle}

10857

799 
\isacommand{lemma}\ rtrancl_converseI:\ "(y,x)\ \isasymin \ r\isacharcircum *\ \isasymLongrightarrow \ (x,y)\ \isasymin \ (r\isacharcircum 1)\isacharcircum *"\isanewline

10303

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


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


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


803 
\isacommand{done}


804 
\end{isabelle}


805 


806 


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


808 
\begin{isabelle}

10857

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


810 
\isacommand{by}\ (auto\ intro:\ rtrancl_converseI\ dest:\


811 
rtrancl_converseD)

10303

812 
\end{isabelle}


813 

10857

814 
\begin{warn}


815 
Note that \isa{blast} cannot prove this theorem. Here is a subgoal that


816 
arises internally after the rules \isa{equalityI} and \isa{subsetI} have


817 
been applied:

10303

818 
\begin{isabelle}

10857

819 
\ 1.\ \isasymAnd x.\ x\ \isasymin \ (r\isasyminverse )\isactrlsup *\ \isasymLongrightarrow \ x\ \isasymin \ (r\isactrlsup


820 
*)\isasyminverse


821 
%ignore subgoal 2


822 
%\ 2.\ \isasymAnd x.\ x\ \isasymin \ (r\isactrlsup *)\isasyminverse \


823 
%\isasymLongrightarrow \ x\ \isasymin \ (r\isasyminverse )\isactrlsup *

10303

824 
\end{isabelle}

10857

825 
\par\noindent


826 
We cannot use \isa{rtrancl_converseD}\@. It refers to


827 
ordered pairs, while \isa{x} is a variable of product type.


828 
The \isa{simp} and \isa{blast} methods can do nothing, so let us try


829 
\isa{clarify}:

10303

830 
\begin{isabelle}

10857

831 
\ 1.\ \isasymAnd a\ b.\ (a,b)\ \isasymin \ (r\isasyminverse )\isactrlsup *\ \isasymLongrightarrow \ (b,a)\ \isasymin \ r\isactrlsup


832 
*

10303

833 
\end{isabelle}

10857

834 
Now that \isa{x} has been replaced by the pair \isa{(a,b)}, we can


835 
proceed. Other methods that split variables in this way are \isa{force}


836 
and \isa{auto}. Section~\ref{sec:products} will discuss proof techniques


837 
for ordered pairs in more detail.


838 
\end{warn}

10303

839 


840 

10857

841 


842 
\section{WellFounded Relations and Induction}

10513

843 
\label{sec:Wellfounded}

10303

844 


845 
Induction comes in many forms, including traditional mathematical


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


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


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


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


850 
infinite descending chains


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

10398

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


853 
induction rule:

10303

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


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


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


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

10398

858 
reasoning are finite.

10303

859 

10857

860 
\smallskip

10303

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


862 
\begin{isabelle}


863 
{\isasymlbrakk}wf\ r;\


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


865 
\isasymlongrightarrow\ P\ y\ \isasymLongrightarrow\ P\ x\isasymrbrakk\


866 
\isasymLongrightarrow\ P\ a


867 
\rulename{wf_induct}


868 
\end{isabelle}

10857

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

10303

870 


871 
Many familiar induction principles are instances of this rule.


872 
For example, the predecessor relation on the natural numbers


873 
is wellfounded; induction over it is mathematical induction.


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


875 
it is structural induction.


876 

10857

877 
Wellfoundedness can be difficult to show. The various


878 
formulations are all complicated. However, often a relation


879 
is wellfounded by construction. HOL provides


880 
theorems concerning ways of constructing a wellfounded relation.

10303

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


882 
involving an existing relation, or two relations can be


883 
combined lexicographically.


884 

10857

885 
Isabelle/HOL declares \isa{less_than} as a relation object,

10303

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


887 
relation behaves as expected and that it is wellfounded:


888 
\begin{isabelle}


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


890 
\rulename{less_than_iff}\isanewline


891 
wf\ less_than


892 
\rulename{wf_less_than}


893 
\end{isabelle}


894 


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

10857

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


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


898 
this new relation would give rise to an infinite descending chain


899 
on~\isa{r}. Isabelle/HOL holds the definition of this concept and a


900 
theorem stating that it preserves wellfoundedness:

10303

901 
\begin{isabelle}


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


903 
\isasymin\ r\isacharbraceright


904 
\rulename{inv_image_def}\isanewline


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


906 
\rulename{wf_inv_image}


907 
\end{isabelle}


908 


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

10857

910 
for example, induction on the length of a list (\isa{measure length}).


911 
Isabelle/HOL defines


912 
\isa{measure} specifically:

10303

913 
\begin{isabelle}


914 
measure\ \isasymequiv\ inv_image\ less_than%


915 
\rulename{measure_def}\isanewline


916 
wf\ (measure\ f)


917 
\rulename{wf_measure}


918 
\end{isabelle}


919 


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


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


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


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


924 
usual definition and it preserves wellfoundedness:


925 
\begin{isabelle}


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


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


928 
\isasymor\isanewline


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


930 
\isasymin \ rb\isacharbraceright


931 
\rulename{lex_prod_def}%


932 
\par\smallskip


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


934 
\rulename{wf_lex_prod}


935 
\end{isabelle}


936 


937 
These constructions can be used in a


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


939 
the wellfounded relation used to prove termination.


940 

10857

941 
The \textbf{multiset ordering}, useful for hard termination proofs, is available


942 
in the Library. Baader and Nipkow \cite[\S2.5]{BaaderNipkow} discuss it.

10303

943 


944 

10857

945 
\section{Fixed Point Operators}

10303

946 


947 
Fixed point operators define sets recursively. Most users invoke

10857

948 
them by making an inductive definition, as discussed in


949 
Chap.\ts\ref{chap:inductive} below. However, they can be used directly.


950 
The


951 
\relax{least} or \relax{strongest} fixed point yields an inductive


952 
definition; the \relax{greatest} or \relax{weakest} fixed point yields a


953 
coinductive definition. Mathematicians may wish to note that the


954 
existence of these fixed points is guaranteed by the KnasterTarski


955 
theorem.

10303

956 


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


958 
definition of monotone is overloaded over all orderings:


959 
\begin{isabelle}


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


961 
\rulename{mono_def}


962 
\end{isabelle}


963 
%


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


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


966 
definition, monotonicity has the obvious introduction and destruction


967 
rules:


968 
\begin{isabelle}


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


970 
\rulename{monoI}%


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


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


973 
\isasymLongrightarrow\ f\ A\ \isasymle\ f\ B%


974 
\rulename{monoD}


975 
\end{isabelle}


976 


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


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


979 
\begin{isabelle}


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


981 
\rulename{lfp_unfold}%


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


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


984 
\ {\isasymAnd}x.\ x\

10857

985 
\isasymin\ f\ (lfp\ f\ \isasyminter\ \isacharbraceleft x.\ P\

10303

986 
x\isacharbraceright)\ \isasymLongrightarrow\ P\ x\isasymrbrakk\


987 
\isasymLongrightarrow\ P\ a%


988 
\rulename{lfp_induct}


989 
\end{isabelle}


990 
%


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


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


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


994 

10857

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

10303

996 
\begin{isabelle}


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


998 
\rulename{gfp_unfold}%


999 
\isanewline


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


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


1002 
gfp\ f%


1003 
\rulename{coinduct}


1004 
\end{isabelle}

10857

1005 
A \relax{bisimulation} is perhaps the bestknown concept defined as a

10303

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


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


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

10857

1009 
theory \isa{Gfp} for details.
