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