doc-src/TutorialI/Sets/sets.tex
 author wenzelm Wed Jul 25 12:38:54 2012 +0200 (2012-07-25) changeset 48497 ba61aceaa18a parent 44050 f7634e2300bc permissions -rw-r--r--
some updates on "Building a repository version of Isabelle";
     1 \chapter{Sets, Functions and Relations}

     2

     3 This chapter describes the formalization of typed set theory, which is

     4 the basis of much else in HOL\@.  For example, an

     5 inductive definition yields a set, and the abstract theories of relations

     6 regard a relation as a set of pairs.  The chapter introduces the well-known

     7 constants such as union and intersection, as well as the main operations on relations, such as converse, composition and

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

     9 HOL, but many of their properties concern sets: the range of a

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

    11

    12 This chapter will be useful to anybody who plans to develop a substantial

    13 proof.  Sets are convenient for formalizing  computer science concepts such

    14 as grammars, logical calculi and state transition systems.  Isabelle can

    15 prove many statements involving sets automatically.

    16

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

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

    19 chapter presents a small selection of built-in theorems in order to point

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

    21 the notation.

    22

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

    24 are seldom used directly, so only a few are presented here.

    25

    26

    27 \section{Sets}

    28

    29 \index{sets|(}%

    30 HOL's set theory should not be confused with traditional,  untyped set

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

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

    33 $\tau$~\tydx{set}.

    34

    35 We 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

    38 points can be seen below.

    39

    40 Here are the natural deduction rules for \rmindex{intersection}.  Note

    41 the  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

    46 c\ \isasymin\ A\ \isasyminter\ B\ \isasymLongrightarrow\ c\ \isasymin\ A

    47 \rulenamedx{IntD1}\isanewline

    48 c\ \isasymin\ A\ \isasyminter\ B\ \isasymLongrightarrow\ c\ \isasymin\ B

    49 \rulenamedx{IntD2}

    50 \end{isabelle}

    51

    52 Here are two of the many installed theorems concerning set

    53 complement.\index{complement!of a set}

    54 Note 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

    62 Set \textbf{difference}\indexbold{difference!of sets} is the intersection

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

    64 for the  empty set and for the universal set.

    65 \begin{isabelle}

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

    67 \rulename{Diff_disjoint}\isanewline

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

    69 \rulename{Compl_partition}

    70 \end{isabelle}

    71

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

    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 \rulenamedx{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 \rulenamedx{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}

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

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

    90 \rulenamedx{Un_subset_iff}

    91 \end{isabelle}

    92 Here 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 %

    99 This 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 %

   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}

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

   113 -A)"

   114 \end{isabelle}

   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.

   118

   119 \medskip

   120 Two sets are \textbf{equal}\indexbold{equality!of sets} if they contain the

   121 same elements.   This is

   122 the principle of \textbf{extensionality}\indexbold{extensionality!for sets}

   123 for sets.

   124 \begin{isabelle}

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

   126 {\isasymLongrightarrow}\ A\ =\ B

   127 \rulenamedx{set_ext}

   128 \end{isabelle}

   129 Extensionality can be expressed as

   130 $A=B\iff (A\subseteq B)\conj (B\subseteq A)$.

   131 The following rules express both

   132 directions 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\

   136 A\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}

   149 Finite sets are expressed using the constant \cdx{insert}, which is

   150 a form of union:

   151 \begin{isabelle}

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

   153 \rulename{insert_is_Un}

   154 \end{isabelle}

   155 %

   156 The finite set expression \isa{\isacharbraceleft

   157 a,b\isacharbraceright} abbreviates

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

   159 Many 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

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

   170 Consider 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 %

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

   178 fails, 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

   183 b\isacharbraceright)"\isanewline

   184 \isacommand{apply}\ simp\isanewline

   185 \isacommand{by}\ blast

   186 \end{isabelle}

   187

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

   189 remark: 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}}

   192 cannot 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|(}%

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

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

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

   202 comprehension 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

   212 Facts such as these have trivial proofs:

   213 \begin{isabelle}

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

   215 x\ \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

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

   226 described through an example:

   227 \begin{isabelle}

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

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

   230 \isanewline

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

   232 \isasymand\ p{\isasymin}prime\ \isasymand\

   233 q{\isasymin}prime\isacharbraceright"

   234 \end{isabelle}

   235 The left and right hand sides

   236 of this equation are identical. The syntax used in the

   237 left-hand side abbreviates the right-hand side: in this case, all numbers

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

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

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

   241 the expression, with its existential quantifiers.

   242

   243 \smallskip

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

   245 to predicate variables, which are allowed in  higher-order logic.  The main

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

   247 and

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

   249 require 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|(}%

   258 Universal and existential quantifications may range over sets,

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

   260 bounded 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

   265 A.\ P\ x%

   266 \rulenamedx{ballI}%

   267 \isanewline

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

   269 P\ x;\ x\ \isasymin\

   270 A\isasymrbrakk\ \isasymLongrightarrow\ P\

   271 x%

   272 \rulenamedx{bspec}

   273 \end{isabelle}

   274 %

   275 Dually, here are the natural deduction rules for the

   276 bounded existential quantifier.  You may need to apply

   277 \isa{bexI} with an explicit instantiation:

   278 \begin{isabelle}

   279 \isasymlbrakk P\ x;\

   280 x\ \isasymin\ A\isasymrbrakk\

   281 \isasymLongrightarrow\

   282 \isasymexists x\isasymin A.\ P\

   283 x%

   284 \rulenamedx{bexI}%

   285 \isanewline

   286 \isasymlbrakk\isasymexists x\isasymin A.\

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

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

   289 P\ x\isasymrbrakk\ \isasymLongrightarrow\

   290 Q\isasymrbrakk\ \isasymLongrightarrow\ Q%

   291 \rulenamedx{bexE}

   292 \end{isabelle}

   293 \index{quantifiers!for sets|)}

   294

   295 \index{union!indexed}%

   296 Unions 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.\

   302 b\ \isasymin\ B\ x)

   303 \rulenamedx{UN_iff}

   304 \end{isabelle}

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

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

   307 \begin{isabelle}

   308 \isasymlbrakk a\ \isasymin\

   309 A;\ b\ \isasymin\

   310 B\ a\isasymrbrakk\ \isasymLongrightarrow\

   311 b\ \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\

   318 A;\ b\ \isasymin\

   319 B\ x\isasymrbrakk\ \isasymLongrightarrow\

   320 R\isasymrbrakk\ \isasymLongrightarrow\ R%

   321 \rulenamedx{UN_E}

   322 \end{isabelle}

   323 %

   324 The following built-in abbreviation (see {\S}\ref{sec:abbreviations})

   325 lets 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

   332 We 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}%

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

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

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

   344 theorems are available:

   345 \begin{isabelle}

   346 (b\ \isasymin\

   347 (\isasymInter x\isasymin A. B\ x))\

   348 =\

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

   350 b\ \isasymin\ B\ x)

   351 \rulenamedx{INT_iff}%

   352 \isanewline

   353 (A\ \isasymin\

   354 \isasymInter C)\ =\

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

   356 A\ \isasymin\ X)

   357 \rulenamedx{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\lor x\in B$.

   364

   365 The internal form of a comprehension involves the constant

   366 \cdx{Collect},

   367 which occasionally appears when a goal or theorem

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

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

   370 happen with quantifiers:   \hbox{\isa{All\ P}}\index{*All (constant)}

   371 is

   372 \isa{{\isasymforall}x.\ P\ x} and

   373 \hbox{\isa{Ex\ P}}\index{*Ex (constant)} is \isa{\isasymexists x.\ P\ x};

   374 also \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

   378 intersections, you may see the constants

   379 \cdx{UNION} and  \cdx{INTER}\@.

   380 The internal constant for $\varepsilon x.P(x)$ is~\cdx{Eps}.

   381

   382 We have only scratched the surface of Isabelle/HOL's set theory, which provides

   383 hundreds of theorems for your use.

   384

   385

   386 \subsection{Finiteness and Cardinality}

   387

   388 \index{sets!finite}%

   389 The predicate \sdx{finite} holds of all finite sets.  Isabelle/HOL

   390 includes many familiar theorems about finiteness and cardinality

   391 (\cdx{card}). For example, we have theorems concerning the

   392 cardinalities of unions, intersections and the

   393 powerset:\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

   401 finite\ A\ \isasymLongrightarrow\ card\

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

   403 \rulenamedx{card_Pow}%

   404 \isanewline

   405 \isanewline

   406 finite\ A\ \isasymLongrightarrow\isanewline

   407 card\ \isacharbraceleft B.\ B\ \isasymsubseteq\

   408 A\ \isasymand\ card\ B\ =\

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

   410 \rulename{n_subsets}

   411 \end{isabelle}

   412 Writing $|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|(}%

   428 This section describes a few concepts that involve

   429 functions.  Some of the more important theorems are given along with the

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

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

   432 \isa{blast}.

   433

   434 \subsection{Function Basics}

   435

   436 Two functions are \textbf{equal}\indexbold{equality!of functions}

   437 if they yield equal results given equal

   438 arguments.  This is the principle of

   439 \textbf{extensionality}\indexbold{extensionality!for functions} for

   440 functions:

   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}%

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

   448 the obvious definition and many useful facts are proved about

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

   450 rule:

   451 \begin{isabelle}

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

   453 \rulename{fun_upd_apply}

   454 \end{isabelle}

   455 Two syntactic points must be noted.  In

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

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

   458 updates can be abbreviated as shown on the left-hand side of this theorem:

   459 \begin{isabelle}

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

   461 \rulename{fun_upd_upd}

   462 \end{isabelle}

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

   464 when it is not being applied to an argument.

   465

   466 \medskip

   467 The \bfindex{identity function} and function

   468 \textbf{composition}\indexbold{composition!of functions} are

   469 defined:

   470 \begin{isabelle}%

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

   472 \rulenamedx{id_def}\isanewline

   473 f\ \isasymcirc\ g\ \isasymequiv\

   474 {\isasymlambda}x.\ f\

   475 (g\ x)%

   476 \rulenamedx{o_def}

   477 \end{isabelle}

   478 %

   479 Many familiar theorems concerning the identity and composition

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

   481 \begin{isabelle}

   482 f\ \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}%

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

   490 \begin{isabelle}

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

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

   493 =\ y%

   494 \rulenamedx{inj_on_def}\isanewline

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

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

   497 \rulenamedx{surj_def}\isanewline

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

   499 \rulenamedx{bij_def}

   500 \end{isabelle}

   501 The second argument

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

   503 given set. This refinement is useful in higher-order logic, where

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

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

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

   507

   508 The operator \isa{inv} expresses the

   509 \textbf{inverse}\indexbold{inverse!of a function}

   510 of a function. In

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

   512 such as these:

   513 \begin{isabelle}

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

   515 \rulename{inv_f_f}\isanewline

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

   517 \rulename{surj_f_inv_f}\isanewline

   518 bij\ 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

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

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

   545 with, we need a law that relates the equality of functions to

   546 equality over all arguments:

   547 \begin{isabelle}

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

   549 \rulename{fun_eq_iff}

   550 \end{isabelle}

   551 %

   552 This is just a restatement of

   553 extensionality.\indexbold{extensionality!for functions}

   554 Our lemma

   555 states  that an injection can be cancelled from the left  side of

   556 function 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

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

   565 of 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}

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

   572

   573

   574 \subsection{Function Image}

   575

   576 The \textbf{image}\indexbold{image!under a function}

   577 of a set under a function is a most useful notion.  It

   578 has the obvious definition:

   579 \begin{isabelle}

   580 f\ \ A\ \isasymequiv\ \isacharbraceleft y.\ \isasymexists x\isasymin

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

   582 \rulenamedx{image_def}

   583 \end{isabelle}

   584 %

   585 Here 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

   589 f(A\ \isasymunion\ B)\ =\ fA\ \isasymunion\ fB

   590 \rulename{image_Un}\isanewline

   591 inj\ f\ \isasymLongrightarrow\ f(A\ \isasyminter\

   592 B)\ =\ fA\ \isasyminter\ fB

   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

   600 Laws involving image can often be proved automatically. Here

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

   602 general syntax for comprehension:

   603 \begin{isabelle}

   604 \isacommand{lemma}\ "fA\ \isasymunion\ gA\ =\ ({\isasymUnion}x{\isasymin}A.\ \isacharbraceleft f\ x,\ g\

   605 x\isacharbraceright)"

   606 \par\smallskip

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

   608 y\isacharbraceright"

   609 \end{isabelle}

   610

   611 \medskip

   612 \index{range!of a function}%

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

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

   615 that 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}\ fUNIV

   620 \end{isabelle}

   621 %

   622 Few theorems are proved specifically

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

   624 theorem concerning images.

   625

   626 \medskip

   627 \textbf{Inverse image}\index{inverse image!of a function} is also  useful.

   628 It is defined as follows:

   629 \begin{isabelle}

   630 f\ -\ B\ \isasymequiv\ \isacharbraceleft x.\ f\ x\ \isasymin\ B\isacharbraceright

   631 \rulenamedx{vimage_def}

   632 \end{isabelle}

   633 %

   634 This is one of the facts proved about it:

   635 \begin{isabelle}

   636 f\ -\ (-\ 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|(}%

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

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

   648 primitives are defined specifically for relations.

   649

   650 \subsection{Relation Basics}

   651

   652 The \bfindex{identity relation}, also known as equality, has the obvious

   653 definition:

   654 \begin{isabelle}

   655 Id\ \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

   661 available:

   662 \begin{isabelle}

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

   664 \rulenamedx{rel_comp_def}

   665 \end{isabelle}

   666 %

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

   668 \begin{isabelle}

   669 R\ O\ Id\ =\ R

   670 \rulename{R_O_Id}

   671 \end{isabelle}

   672 %

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

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

   675 one:

   676 \begin{isabelle}

   677 \isasymlbrakk r\isacharprime\ \isasymsubseteq\ r;\ s\isacharprime\

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

   679 s\isacharprime\ \isasymsubseteq\ r\ O\ s%

   680 \rulename{rel_comp_mono}

   681 \end{isabelle}

   682

   683 \indexbold{converse!of a relation}%

   684 \indexbold{inverse!of a relation}%

   685 The \textbf{converse} or inverse of a

   686 relation exchanges the roles  of the two operands.  We use the postfix

   687 notation~\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 %

   695 Here 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_rel_comp}

   699 \end{isabelle}

   700

   701 \indexbold{image!under a relation}%

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

   703 analogously  to image under a function:

   704 \begin{isabelle}

   705 (b\ \isasymin\ r\ \ A)\ =\ (\isasymexists x\isasymin

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

   707 \rulenamedx{Image_iff}

   708 \end{isabelle}

   709 It satisfies many similar laws.

   710

   711 \index{domain!of a relation}%

   712 \index{range!of a relation}%

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

   714 standard way:

   715 \begin{isabelle}

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

   717 r)

   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

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

   728 that of exponentiation.  Two simplification rules are installed:

   729 \begin{isabelle}

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

   731 R\ \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|(}%

   737 The \textbf{reflexive and transitive closure} of the

   738 relation~\isa{r} is written with a

   739 postfix syntax.  In ASCII we write \isa{r\isacharcircum*} and in

   740 symbol notation~\isa{r\isactrlsup *}.  It is the least solution of the

   741 equation

   742 \begin{isabelle}

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

   744 \rulename{rtrancl_unfold}

   745 \end{isabelle}

   746 %

   747 Among its basic properties are three that serve as introduction

   748 rules:

   749 \begin{isabelle}

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

   751 \rulenamedx{rtrancl_refl}\isanewline

   752 p\ \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 %

   760 Induction 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 %

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

   768 closure:

   769 \begin{isabelle}

   770 (r\isactrlsup *)\isactrlsup *\ =\ r\isactrlsup *

   771 \rulename{rtrancl_idemp}

   772 \end{isabelle}

   773

   774 \smallskip

   775 The transitive closure is similar.  The ASCII syntax is

   776 \isa{r\isacharcircum+}.  It has two  introduction rules:

   777 \begin{isabelle}

   778 p\ \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 %

   784 The induction rule resembles the one shown above.

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

   786 operator:

   787 \begin{isabelle}

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

   789 \rulename{trancl_converse}

   790 \end{isabelle}

   791

   792 \subsection{A Sample Proof}

   793

   794 The reflexive transitive closure also commutes with the converse

   795 operator.  Let us examine the proof. Each direction of the equivalence

   796 is  proved separately. The two proofs are almost identical. Here

   797 is 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 %

   808 The 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 %

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

   818 by first eliminating the converse operator, yielding the

   819 assumption \isa{(z,y)\

   820 \isasymin\ r}, and then

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

   822 the 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

   832 Finally, 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:\

   836 rtrancl_converseD)

   837 \end{isabelle}

   838

   839 \begin{warn}

   840 This trivial proof requires \isa{auto} rather than \isa{blast} because

   841 of a subtle issue involving ordered pairs.  Here is a subgoal that

   842 arises 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

   852 We cannot apply \isa{rtrancl_converseD}\@.  It refers to

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

   854 The \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}

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

   861 proceed.  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

   863 techniques 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|(}%

   872 A well-founded relation captures the notion of a terminating

   873 process. Complex recursive functions definitions must specify a

   874 well-founded relation that justifies their

   875 termination~\cite{isabelle-function}. Most of the forms of induction found

   876 in mathematics are merely special cases of induction over a

   877 well-founded relation.

   878

   879 Intuitively, the relation~$\prec$ is \textbf{well-founded} if it admits no

   880 infinite  descending chains

   881 $\cdots \prec a@2 \prec a@1 \prec a@0.$

   882 Well-foundedness can be hard to show. The various

   883 formulations are all complicated.  However,  often a relation

   884 is well-founded by construction.  HOL provides

   885 theorems concerning ways of constructing  a well-founded relation.  The

   886 most familiar way is to specify a

   887 \index{measure functions}\textbf{measure function}~\isa{f} into

   888 the natural numbers, when $\isa{x}\prec \isa{y}\iff \isa{f x} < \isa{f y}$;

   889 we write this particular relation as

   890 \isa{measure~f}.

   891

   892 \begin{warn}

   893 You may want to skip the rest of this section until you need to perform a

   894 complex recursive function definition or induction.  The induction rule

   895 returned by

   896 \isacommand{fun} is good enough for most purposes.  We use an explicit

   897 well-founded induction only in {\S}\ref{sec:CTL-revisited}.

   898 \end{warn}

   899

   900 Isabelle/HOL declares \cdx{less_than} as a relation object,

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

   902 relation  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

   906 wf\ less_than

   907 \rulenamedx{wf_less_than}

   908 \end{isabelle}

   909

   910 The notion of measure generalizes to the

   911 \index{inverse image!of a relation}\textbf{inverse image} of

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

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

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

   915 on~\isa{r}.  Isabelle/HOL defines this concept and proves a

   916 theorem stating that it preserves well-foundedness:

   917 \begin{isabelle}

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

   919 \isasymin\ r\isacharbraceright

   920 \rulenamedx{inv_image_def}\isanewline

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

   922 \rulenamedx{wf_inv_image}

   923 \end{isabelle}

   924

   925 A measure function involves the natural numbers.  The relation \isa{measure

   926 size} justifies primitive recursion and structural induction over a

   927 datatype.  Isabelle/HOL defines

   928 \isa{measure} as shown:

   929 \begin{isabelle}

   930 measure\ \isasymequiv\ inv_image\ less_than%

   931 \rulenamedx{measure_def}\isanewline

   932 wf\ (measure\ f)

   933 \rulenamedx{wf_measure}

   934 \end{isabelle}

   935

   936 Of the other constructions, the most important is the

   937 \bfindex{lexicographic product} of two relations. It expresses the

   938 standard dictionary  ordering over pairs.  We write \isa{ra\ <*lex*>\

   939 rb}, where \isa{ra} and \isa{rb} are the two operands.  The

   940 lexicographic product satisfies the usual  definition and it preserves

   941 well-foundedness:

   942 \begin{isabelle}

   943 ra\ <*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

   958 The \bfindex{multiset ordering}, useful for hard termination proofs, is

   959 available in the Library~\cite{HOL-Library}.

   960 Baader and Nipkow \cite[{\S}2.5]{Baader-Nipkow} discuss it.

   961

   962 \medskip

   963 Induction\index{induction!well-founded|(}

   964 comes in many forms,

   965 including traditional mathematical  induction, structural induction on

   966 lists and induction on size.  All are instances of the following rule,

   967 for a suitable well-founded relation~$\prec$:

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

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

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

   971 Intuitively, the well-foundedness of $\prec$ ensures that the chains of

   972 reasoning are finite.

   973

   974 \smallskip

   975 In 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}

   983 Here \isa{wf\ r} expresses that the relation~\isa{r} is well-founded.

   984

   985 Many familiar induction principles are instances of this rule.

   986 For example, the predecessor relation on the natural numbers

   987 is well-founded; induction over it is mathematical induction.

   988 The tail of'' relation on lists is well-founded; induction over

   989 it 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|(}%

   997 Fixed point operators define sets

   998 recursively.  They are invoked implicitly when making an inductive

   999 definition, as discussed in Chap.\ts\ref{chap:inductive} below.  However,

  1000 they can be used directly, too. The

  1001 \emph{least}  or \emph{strongest} fixed point yields an inductive

  1002 definition;  the \emph{greatest} or \emph{weakest} fixed point yields a

  1003 coinductive  definition.  Mathematicians may wish to note that the

  1004 existence  of these fixed points is guaranteed by the Knaster-Tarski

  1005 theorem.

  1006

  1007 \begin{warn}

  1008 Casual readers should skip the rest of this section.  We use fixed point

  1009 operators only in {\S}\ref{sec:VMC}.

  1010 \end{warn}

  1011

  1012 The theory applies only to monotonic functions.\index{monotone functions|bold}

  1013 Isabelle's definition of monotone is overloaded over all orderings:

  1014 \begin{isabelle}

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

  1016 \rulenamedx{mono_def}

  1017 \end{isabelle}

  1018 %

  1019 For 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

  1021 definition, monotonicity has the obvious introduction and destruction

  1022 rules:

  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

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

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

  1034 \begin{isabelle}

  1035 mono\ 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\

  1041 x\isacharbraceright)\ \isasymLongrightarrow\ P\ x\isasymrbrakk\

  1042 \isasymLongrightarrow\ P\ a%

  1043 \rulename{lfp_induct}

  1044 \end{isabelle}

  1045 %

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

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

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

  1049

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

  1051 \begin{isabelle}

  1052 mono\ 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\

  1057 gfp\ f%

  1058 \rulename{coinduct}

  1059 \end{isabelle}

  1060 A \textbf{bisimulation}\index{bisimulations}

  1061 is perhaps the best-known concept defined as a

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

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

  1064 The 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{CTL/ctl}

  1069 \endinput
`