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