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