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)\ =\ f`A\ \isasymunion\ f`B
   590 \rulename{image_Un}\isanewline
   591 inj\ f\ \isasymLongrightarrow\ f`(A\ \isasyminter\
   592 B)\ =\ 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 
   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}\ "f`A\ \isasymunion\ g`A\ =\ ({\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}\ f`UNIV
   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