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