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