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