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)\ =\ f``A\ \isasymunion\ f``B
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)\ =\ f``A\ \isasyminter\ f``B
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}\ "f``A\ \isasymunion\ g``A\ =\ ({\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
{==}\ f``UNIV
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}).