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