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