clasohm@1465
|
1 |
(* Title: Relation.ML
|
nipkow@1128
|
2 |
ID: $Id$
|
paulson@1985
|
3 |
Authors: Lawrence C Paulson, Cambridge University Computer Laboratory
|
paulson@1985
|
4 |
Copyright 1996 University of Cambridge
|
nipkow@1128
|
5 |
*)
|
nipkow@1128
|
6 |
|
nipkow@1128
|
7 |
(** Identity relation **)
|
nipkow@1128
|
8 |
|
nipkow@5608
|
9 |
Goalw [Id_def] "(a,a) : Id";
|
paulson@2891
|
10 |
by (Blast_tac 1);
|
nipkow@5608
|
11 |
qed "IdI";
|
nipkow@1128
|
12 |
|
nipkow@5608
|
13 |
val major::prems = Goalw [Id_def]
|
nipkow@5608
|
14 |
"[| p: Id; !!x.[| p = (x,x) |] ==> P \
|
nipkow@1128
|
15 |
\ |] ==> P";
|
nipkow@1128
|
16 |
by (rtac (major RS CollectE) 1);
|
nipkow@1128
|
17 |
by (etac exE 1);
|
nipkow@1128
|
18 |
by (eresolve_tac prems 1);
|
nipkow@5608
|
19 |
qed "IdE";
|
nipkow@1128
|
20 |
|
nipkow@5608
|
21 |
Goalw [Id_def] "(a,b):Id = (a=b)";
|
paulson@2891
|
22 |
by (Blast_tac 1);
|
nipkow@5608
|
23 |
qed "pair_in_Id_conv";
|
nipkow@5608
|
24 |
Addsimps [pair_in_Id_conv];
|
nipkow@1128
|
25 |
|
paulson@6806
|
26 |
Goalw [refl_def] "reflexive Id";
|
paulson@6806
|
27 |
by Auto_tac;
|
paulson@6806
|
28 |
qed "reflexive_Id";
|
paulson@6806
|
29 |
|
paulson@6806
|
30 |
(*A strange result, since Id is also symmetric.*)
|
paulson@6806
|
31 |
Goalw [antisym_def] "antisym Id";
|
paulson@6806
|
32 |
by Auto_tac;
|
paulson@6806
|
33 |
qed "antisym_Id";
|
paulson@6806
|
34 |
|
paulson@6806
|
35 |
Goalw [trans_def] "trans Id";
|
paulson@6806
|
36 |
by Auto_tac;
|
paulson@6806
|
37 |
qed "trans_Id";
|
paulson@6806
|
38 |
|
nipkow@1128
|
39 |
|
paulson@5978
|
40 |
(** Diagonal relation: indentity restricted to some set **)
|
paulson@5978
|
41 |
|
paulson@5978
|
42 |
(*** Equality : the diagonal relation ***)
|
paulson@5978
|
43 |
|
paulson@5978
|
44 |
Goalw [diag_def] "[| a=b; a:A |] ==> (a,b) : diag(A)";
|
paulson@5978
|
45 |
by (Blast_tac 1);
|
paulson@5978
|
46 |
qed "diag_eqI";
|
paulson@5978
|
47 |
|
paulson@5978
|
48 |
val diagI = refl RS diag_eqI |> standard;
|
paulson@5978
|
49 |
|
paulson@5978
|
50 |
(*The general elimination rule*)
|
paulson@5978
|
51 |
val major::prems = Goalw [diag_def]
|
paulson@5978
|
52 |
"[| c : diag(A); \
|
paulson@5978
|
53 |
\ !!x y. [| x:A; c = (x,x) |] ==> P \
|
paulson@5978
|
54 |
\ |] ==> P";
|
paulson@5978
|
55 |
by (rtac (major RS UN_E) 1);
|
paulson@5978
|
56 |
by (REPEAT (eresolve_tac [asm_rl,singletonE] 1 ORELSE resolve_tac prems 1));
|
paulson@5978
|
57 |
qed "diagE";
|
paulson@5978
|
58 |
|
paulson@5978
|
59 |
AddSIs [diagI];
|
paulson@5978
|
60 |
AddSEs [diagE];
|
paulson@5978
|
61 |
|
paulson@5978
|
62 |
Goal "((x,y) : diag A) = (x=y & x : A)";
|
paulson@5978
|
63 |
by (Blast_tac 1);
|
paulson@5978
|
64 |
qed "diag_iff";
|
paulson@5978
|
65 |
|
paulson@5978
|
66 |
Goal "diag(A) <= A Times A";
|
paulson@5978
|
67 |
by (Blast_tac 1);
|
paulson@5995
|
68 |
qed "diag_subset_Times";
|
paulson@5978
|
69 |
|
paulson@5978
|
70 |
|
paulson@5978
|
71 |
|
nipkow@1128
|
72 |
(** Composition of two relations **)
|
nipkow@1128
|
73 |
|
wenzelm@5069
|
74 |
Goalw [comp_def]
|
paulson@5148
|
75 |
"[| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
|
paulson@2891
|
76 |
by (Blast_tac 1);
|
nipkow@1128
|
77 |
qed "compI";
|
nipkow@1128
|
78 |
|
nipkow@1128
|
79 |
(*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
|
paulson@5316
|
80 |
val prems = Goalw [comp_def]
|
nipkow@1128
|
81 |
"[| xz : r O s; \
|
nipkow@1128
|
82 |
\ !!x y z. [| xz = (x,z); (x,y):s; (y,z):r |] ==> P \
|
nipkow@1128
|
83 |
\ |] ==> P";
|
nipkow@1128
|
84 |
by (cut_facts_tac prems 1);
|
paulson@1985
|
85 |
by (REPEAT (eresolve_tac [CollectE, splitE, exE, conjE] 1
|
paulson@1985
|
86 |
ORELSE ares_tac prems 1));
|
nipkow@1128
|
87 |
qed "compE";
|
nipkow@1128
|
88 |
|
paulson@5316
|
89 |
val prems = Goal
|
nipkow@1128
|
90 |
"[| (a,c) : r O s; \
|
nipkow@1128
|
91 |
\ !!y. [| (a,y):s; (y,c):r |] ==> P \
|
nipkow@1128
|
92 |
\ |] ==> P";
|
nipkow@1128
|
93 |
by (rtac compE 1);
|
nipkow@1128
|
94 |
by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Pair_inject,ssubst] 1));
|
nipkow@1128
|
95 |
qed "compEpair";
|
nipkow@1128
|
96 |
|
nipkow@5608
|
97 |
AddIs [compI, IdI];
|
nipkow@5608
|
98 |
AddSEs [compE, IdE];
|
berghofe@1754
|
99 |
|
nipkow@5608
|
100 |
Goal "R O Id = R";
|
paulson@4673
|
101 |
by (Fast_tac 1);
|
nipkow@5608
|
102 |
qed "R_O_Id";
|
paulson@4673
|
103 |
|
nipkow@5608
|
104 |
Goal "Id O R = R";
|
paulson@4673
|
105 |
by (Fast_tac 1);
|
nipkow@5608
|
106 |
qed "Id_O_R";
|
paulson@4673
|
107 |
|
nipkow@5608
|
108 |
Addsimps [R_O_Id,Id_O_R];
|
paulson@4673
|
109 |
|
wenzelm@5069
|
110 |
Goal "(R O S) O T = R O (S O T)";
|
nipkow@4830
|
111 |
by (Blast_tac 1);
|
nipkow@4830
|
112 |
qed "O_assoc";
|
nipkow@4830
|
113 |
|
paulson@5143
|
114 |
Goal "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
|
paulson@2891
|
115 |
by (Blast_tac 1);
|
nipkow@1128
|
116 |
qed "comp_mono";
|
nipkow@1128
|
117 |
|
paulson@5148
|
118 |
Goal "[| s <= A Times B; r <= B Times C |] ==> (r O s) <= A Times C";
|
paulson@2891
|
119 |
by (Blast_tac 1);
|
nipkow@1128
|
120 |
qed "comp_subset_Sigma";
|
nipkow@1128
|
121 |
|
paulson@6806
|
122 |
(** Natural deduction for refl(r) **)
|
paulson@6806
|
123 |
|
paulson@6806
|
124 |
val prems = Goalw [refl_def]
|
paulson@6806
|
125 |
"[| r <= A Times A; !! x. x:A ==> (x,x):r |] ==> refl A r";
|
paulson@6806
|
126 |
by (REPEAT (ares_tac (prems@[ballI,conjI]) 1));
|
paulson@6806
|
127 |
qed "reflI";
|
paulson@6806
|
128 |
|
paulson@6806
|
129 |
Goalw [refl_def] "[| refl A r; a:A |] ==> (a,a):r";
|
paulson@6806
|
130 |
by (Blast_tac 1);
|
paulson@6806
|
131 |
qed "reflD";
|
paulson@6806
|
132 |
|
paulson@6806
|
133 |
(** Natural deduction for antisym(r) **)
|
paulson@6806
|
134 |
|
paulson@6806
|
135 |
val prems = Goalw [antisym_def]
|
paulson@6806
|
136 |
"(!! x y. [| (x,y):r; (y,x):r |] ==> x=y) ==> antisym(r)";
|
paulson@6806
|
137 |
by (REPEAT (ares_tac (prems@[allI,impI]) 1));
|
paulson@6806
|
138 |
qed "antisymI";
|
paulson@6806
|
139 |
|
paulson@6806
|
140 |
Goalw [antisym_def] "[| antisym(r); (a,b):r; (b,a):r |] ==> a=b";
|
paulson@6806
|
141 |
by (Blast_tac 1);
|
paulson@6806
|
142 |
qed "antisymD";
|
paulson@6806
|
143 |
|
nipkow@1128
|
144 |
(** Natural deduction for trans(r) **)
|
nipkow@1128
|
145 |
|
paulson@5316
|
146 |
val prems = Goalw [trans_def]
|
nipkow@1128
|
147 |
"(!! x y z. [| (x,y):r; (y,z):r |] ==> (x,z):r) ==> trans(r)";
|
nipkow@1128
|
148 |
by (REPEAT (ares_tac (prems@[allI,impI]) 1));
|
nipkow@1128
|
149 |
qed "transI";
|
nipkow@1128
|
150 |
|
paulson@5148
|
151 |
Goalw [trans_def] "[| trans(r); (a,b):r; (b,c):r |] ==> (a,c):r";
|
paulson@2891
|
152 |
by (Blast_tac 1);
|
nipkow@1128
|
153 |
qed "transD";
|
nipkow@1128
|
154 |
|
nipkow@3439
|
155 |
(** Natural deduction for r^-1 **)
|
nipkow@1128
|
156 |
|
paulson@5143
|
157 |
Goalw [converse_def] "((a,b): r^-1) = ((b,a):r)";
|
paulson@1985
|
158 |
by (Simp_tac 1);
|
paulson@4746
|
159 |
qed "converse_iff";
|
paulson@1985
|
160 |
|
paulson@4746
|
161 |
AddIffs [converse_iff];
|
paulson@1985
|
162 |
|
paulson@5143
|
163 |
Goalw [converse_def] "(a,b):r ==> (b,a): r^-1";
|
clasohm@1264
|
164 |
by (Simp_tac 1);
|
paulson@4746
|
165 |
qed "converseI";
|
nipkow@1128
|
166 |
|
paulson@5143
|
167 |
Goalw [converse_def] "(a,b) : r^-1 ==> (b,a) : r";
|
paulson@2891
|
168 |
by (Blast_tac 1);
|
paulson@4746
|
169 |
qed "converseD";
|
nipkow@1128
|
170 |
|
paulson@4746
|
171 |
(*More general than converseD, as it "splits" the member of the relation*)
|
paulson@7031
|
172 |
|
paulson@7031
|
173 |
val [major,minor] = Goalw [converse_def]
|
nipkow@3439
|
174 |
"[| yx : r^-1; \
|
nipkow@1128
|
175 |
\ !!x y. [| yx=(y,x); (x,y):r |] ==> P \
|
paulson@7031
|
176 |
\ |] ==> P";
|
paulson@7031
|
177 |
by (rtac (major RS CollectE) 1);
|
paulson@7031
|
178 |
by (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1));
|
paulson@7031
|
179 |
by (assume_tac 1);
|
paulson@7031
|
180 |
qed "converseE";
|
paulson@4746
|
181 |
AddSEs [converseE];
|
nipkow@1128
|
182 |
|
wenzelm@5069
|
183 |
Goalw [converse_def] "(r^-1)^-1 = r";
|
paulson@2891
|
184 |
by (Blast_tac 1);
|
paulson@4746
|
185 |
qed "converse_converse";
|
paulson@4746
|
186 |
Addsimps [converse_converse];
|
nipkow@3413
|
187 |
|
wenzelm@5069
|
188 |
Goal "(r O s)^-1 = s^-1 O r^-1";
|
wenzelm@4423
|
189 |
by (Blast_tac 1);
|
paulson@4746
|
190 |
qed "converse_comp";
|
nipkow@1605
|
191 |
|
nipkow@5608
|
192 |
Goal "Id^-1 = Id";
|
paulson@4644
|
193 |
by (Blast_tac 1);
|
nipkow@5608
|
194 |
qed "converse_Id";
|
nipkow@5608
|
195 |
Addsimps [converse_Id];
|
paulson@4644
|
196 |
|
paulson@5995
|
197 |
Goal "(diag A) ^-1 = diag A";
|
paulson@5995
|
198 |
by (Blast_tac 1);
|
paulson@5995
|
199 |
qed "converse_diag";
|
paulson@5995
|
200 |
Addsimps [converse_diag];
|
paulson@5995
|
201 |
|
paulson@7083
|
202 |
Goalw [refl_def] "refl A r ==> refl A (converse r)";
|
paulson@7083
|
203 |
by (Blast_tac 1);
|
paulson@7083
|
204 |
qed "refl_converse";
|
paulson@7083
|
205 |
|
paulson@7083
|
206 |
Goalw [antisym_def] "antisym (converse r) = antisym r";
|
paulson@7083
|
207 |
by (Blast_tac 1);
|
paulson@7083
|
208 |
qed "antisym_converse";
|
paulson@7083
|
209 |
|
paulson@7083
|
210 |
Goalw [trans_def] "trans (converse r) = trans r";
|
paulson@7083
|
211 |
by (Blast_tac 1);
|
paulson@7083
|
212 |
qed "trans_converse";
|
paulson@7083
|
213 |
|
nipkow@1128
|
214 |
(** Domain **)
|
nipkow@1128
|
215 |
|
paulson@5811
|
216 |
Goalw [Domain_def] "a: Domain(r) = (EX y. (a,y): r)";
|
paulson@5811
|
217 |
by (Blast_tac 1);
|
paulson@5811
|
218 |
qed "Domain_iff";
|
nipkow@1128
|
219 |
|
paulson@7007
|
220 |
Goal "(a,b): r ==> a: Domain(r)";
|
paulson@7007
|
221 |
by (etac (exI RS (Domain_iff RS iffD2)) 1) ;
|
paulson@7007
|
222 |
qed "DomainI";
|
nipkow@1128
|
223 |
|
paulson@7007
|
224 |
val prems= Goal "[| a : Domain(r); !!y. (a,y): r ==> P |] ==> P";
|
paulson@7007
|
225 |
by (rtac (Domain_iff RS iffD1 RS exE) 1);
|
paulson@7007
|
226 |
by (REPEAT (ares_tac prems 1)) ;
|
paulson@7007
|
227 |
qed "DomainE";
|
nipkow@1128
|
228 |
|
paulson@1985
|
229 |
AddIs [DomainI];
|
paulson@1985
|
230 |
AddSEs [DomainE];
|
paulson@1985
|
231 |
|
nipkow@5608
|
232 |
Goal "Domain Id = UNIV";
|
paulson@4644
|
233 |
by (Blast_tac 1);
|
nipkow@5608
|
234 |
qed "Domain_Id";
|
nipkow@5608
|
235 |
Addsimps [Domain_Id];
|
paulson@4644
|
236 |
|
paulson@5978
|
237 |
Goal "Domain (diag A) = A";
|
paulson@5978
|
238 |
by Auto_tac;
|
paulson@5978
|
239 |
qed "Domain_diag";
|
paulson@5978
|
240 |
Addsimps [Domain_diag];
|
paulson@5978
|
241 |
|
paulson@5811
|
242 |
Goal "Domain(A Un B) = Domain(A) Un Domain(B)";
|
paulson@5811
|
243 |
by (Blast_tac 1);
|
paulson@5811
|
244 |
qed "Domain_Un_eq";
|
paulson@5811
|
245 |
|
paulson@5811
|
246 |
Goal "Domain(A Int B) <= Domain(A) Int Domain(B)";
|
paulson@5811
|
247 |
by (Blast_tac 1);
|
paulson@5811
|
248 |
qed "Domain_Int_subset";
|
paulson@5811
|
249 |
|
paulson@5811
|
250 |
Goal "Domain(A) - Domain(B) <= Domain(A - B)";
|
paulson@5811
|
251 |
by (Blast_tac 1);
|
paulson@5811
|
252 |
qed "Domain_Diff_subset";
|
paulson@5811
|
253 |
|
paulson@6005
|
254 |
Goal "Domain (Union S) = (UN A:S. Domain A)";
|
paulson@6005
|
255 |
by (Blast_tac 1);
|
paulson@6005
|
256 |
qed "Domain_Union";
|
paulson@6005
|
257 |
|
paulson@7822
|
258 |
Goal "r <= s ==> Domain r <= Domain s";
|
paulson@7822
|
259 |
by (Blast_tac 1);
|
paulson@7822
|
260 |
qed "Domain_mono";
|
paulson@7822
|
261 |
|
paulson@5811
|
262 |
|
nipkow@1128
|
263 |
(** Range **)
|
nipkow@1128
|
264 |
|
paulson@5811
|
265 |
Goalw [Domain_def, Range_def] "a: Range(r) = (EX y. (y,a): r)";
|
paulson@5811
|
266 |
by (Blast_tac 1);
|
paulson@5811
|
267 |
qed "Range_iff";
|
paulson@5811
|
268 |
|
paulson@7031
|
269 |
Goalw [Range_def] "(a,b): r ==> b : Range(r)";
|
paulson@7031
|
270 |
by (etac (converseI RS DomainI) 1);
|
paulson@7031
|
271 |
qed "RangeI";
|
nipkow@1128
|
272 |
|
paulson@7031
|
273 |
val major::prems = Goalw [Range_def]
|
paulson@7031
|
274 |
"[| b : Range(r); !!x. (x,b): r ==> P |] ==> P";
|
paulson@7031
|
275 |
by (rtac (major RS DomainE) 1);
|
paulson@7031
|
276 |
by (resolve_tac prems 1);
|
paulson@7031
|
277 |
by (etac converseD 1) ;
|
paulson@7031
|
278 |
qed "RangeE";
|
nipkow@1128
|
279 |
|
paulson@1985
|
280 |
AddIs [RangeI];
|
paulson@1985
|
281 |
AddSEs [RangeE];
|
paulson@1985
|
282 |
|
nipkow@5608
|
283 |
Goal "Range Id = UNIV";
|
paulson@4644
|
284 |
by (Blast_tac 1);
|
nipkow@5608
|
285 |
qed "Range_Id";
|
nipkow@5608
|
286 |
Addsimps [Range_Id];
|
paulson@4644
|
287 |
|
paulson@5995
|
288 |
Goal "Range (diag A) = A";
|
paulson@5995
|
289 |
by Auto_tac;
|
paulson@5995
|
290 |
qed "Range_diag";
|
paulson@5995
|
291 |
Addsimps [Range_diag];
|
paulson@5995
|
292 |
|
paulson@5811
|
293 |
Goal "Range(A Un B) = Range(A) Un Range(B)";
|
paulson@5811
|
294 |
by (Blast_tac 1);
|
paulson@5811
|
295 |
qed "Range_Un_eq";
|
paulson@5811
|
296 |
|
paulson@5811
|
297 |
Goal "Range(A Int B) <= Range(A) Int Range(B)";
|
paulson@5811
|
298 |
by (Blast_tac 1);
|
paulson@5811
|
299 |
qed "Range_Int_subset";
|
paulson@5811
|
300 |
|
paulson@5811
|
301 |
Goal "Range(A) - Range(B) <= Range(A - B)";
|
paulson@5811
|
302 |
by (Blast_tac 1);
|
paulson@5811
|
303 |
qed "Range_Diff_subset";
|
paulson@5811
|
304 |
|
paulson@6005
|
305 |
Goal "Range (Union S) = (UN A:S. Range A)";
|
paulson@6005
|
306 |
by (Blast_tac 1);
|
paulson@6005
|
307 |
qed "Range_Union";
|
paulson@6005
|
308 |
|
paulson@5811
|
309 |
|
nipkow@1128
|
310 |
(*** Image of a set under a relation ***)
|
nipkow@1128
|
311 |
|
paulson@8004
|
312 |
overload_1st_set "Relation.Image";
|
paulson@5335
|
313 |
|
paulson@7031
|
314 |
Goalw [Image_def] "b : r^^A = (? x:A. (x,b):r)";
|
paulson@7031
|
315 |
by (Blast_tac 1);
|
paulson@7031
|
316 |
qed "Image_iff";
|
nipkow@1128
|
317 |
|
paulson@7031
|
318 |
Goalw [Image_def] "r^^{a} = {b. (a,b):r}";
|
paulson@7031
|
319 |
by (Blast_tac 1);
|
paulson@7031
|
320 |
qed "Image_singleton";
|
paulson@4673
|
321 |
|
paulson@7031
|
322 |
Goal "(b : r^^{a}) = ((a,b):r)";
|
paulson@7007
|
323 |
by (rtac (Image_iff RS trans) 1);
|
paulson@7007
|
324 |
by (Blast_tac 1);
|
paulson@7007
|
325 |
qed "Image_singleton_iff";
|
nipkow@1128
|
326 |
|
paulson@4673
|
327 |
AddIffs [Image_singleton_iff];
|
paulson@4673
|
328 |
|
paulson@7007
|
329 |
Goalw [Image_def] "[| (a,b): r; a:A |] ==> b : r^^A";
|
paulson@7007
|
330 |
by (Blast_tac 1);
|
paulson@7007
|
331 |
qed "ImageI";
|
nipkow@1128
|
332 |
|
paulson@7031
|
333 |
val major::prems = Goalw [Image_def]
|
paulson@7031
|
334 |
"[| b: r^^A; !!x.[| (x,b): r; x:A |] ==> P |] ==> P";
|
paulson@7031
|
335 |
by (rtac (major RS CollectE) 1);
|
paulson@7031
|
336 |
by (Clarify_tac 1);
|
paulson@7031
|
337 |
by (rtac (hd prems) 1);
|
paulson@7031
|
338 |
by (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ;
|
paulson@7031
|
339 |
qed "ImageE";
|
nipkow@1128
|
340 |
|
paulson@1985
|
341 |
AddIs [ImageI];
|
paulson@1985
|
342 |
AddSEs [ImageE];
|
paulson@1985
|
343 |
|
paulson@4593
|
344 |
|
paulson@7031
|
345 |
Goal "R^^{} = {}";
|
paulson@7007
|
346 |
by (Blast_tac 1);
|
paulson@7007
|
347 |
qed "Image_empty";
|
paulson@4593
|
348 |
|
paulson@4593
|
349 |
Addsimps [Image_empty];
|
paulson@4593
|
350 |
|
nipkow@5608
|
351 |
Goal "Id ^^ A = A";
|
paulson@4601
|
352 |
by (Blast_tac 1);
|
nipkow@5608
|
353 |
qed "Image_Id";
|
paulson@4601
|
354 |
|
paulson@5998
|
355 |
Goal "diag A ^^ B = A Int B";
|
paulson@5995
|
356 |
by (Blast_tac 1);
|
paulson@5995
|
357 |
qed "Image_diag";
|
paulson@5995
|
358 |
|
paulson@5995
|
359 |
Addsimps [Image_Id, Image_diag];
|
paulson@4601
|
360 |
|
paulson@7007
|
361 |
Goal "R ^^ (A Int B) <= R ^^ A Int R ^^ B";
|
paulson@7007
|
362 |
by (Blast_tac 1);
|
paulson@7007
|
363 |
qed "Image_Int_subset";
|
paulson@4593
|
364 |
|
paulson@7007
|
365 |
Goal "R ^^ (A Un B) = R ^^ A Un R ^^ B";
|
paulson@7007
|
366 |
by (Blast_tac 1);
|
paulson@7007
|
367 |
qed "Image_Un";
|
paulson@4593
|
368 |
|
paulson@7007
|
369 |
Goal "r <= A Times B ==> r^^C <= B";
|
paulson@7007
|
370 |
by (rtac subsetI 1);
|
paulson@7007
|
371 |
by (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ;
|
paulson@7007
|
372 |
qed "Image_subset";
|
nipkow@1128
|
373 |
|
paulson@4733
|
374 |
(*NOT suitable for rewriting*)
|
wenzelm@5069
|
375 |
Goal "r^^B = (UN y: B. r^^{y})";
|
paulson@4673
|
376 |
by (Blast_tac 1);
|
paulson@4733
|
377 |
qed "Image_eq_UN";
|
oheimb@4760
|
378 |
|
paulson@7913
|
379 |
Goal "[| r'<=r; A'<=A |] ==> (r' ^^ A') <= (r ^^ A)";
|
paulson@7913
|
380 |
by (Blast_tac 1);
|
paulson@7913
|
381 |
qed "Image_mono";
|
paulson@7913
|
382 |
|
paulson@7913
|
383 |
Goal "(r ^^ (UNION A B)) = (UN x:A.(r ^^ (B x)))";
|
paulson@7913
|
384 |
by (Blast_tac 1);
|
paulson@7913
|
385 |
qed "Image_UN";
|
paulson@7913
|
386 |
|
paulson@7913
|
387 |
(*Converse inclusion fails*)
|
paulson@7913
|
388 |
Goal "(r ^^ (INTER A B)) <= (INT x:A.(r ^^ (B x)))";
|
paulson@7913
|
389 |
by (Blast_tac 1);
|
paulson@7913
|
390 |
qed "Image_INT_subset";
|
paulson@7913
|
391 |
|
paulson@8004
|
392 |
Goal "(r^^A <= B) = (A <= - ((r^-1) ^^ (-B)))";
|
paulson@8004
|
393 |
by (Blast_tac 1);
|
paulson@8004
|
394 |
qed "Image_subset_eq";
|
oheimb@4760
|
395 |
|
oheimb@4760
|
396 |
section "Univalent";
|
oheimb@4760
|
397 |
|
paulson@7031
|
398 |
Goalw [Univalent_def]
|
paulson@7031
|
399 |
"!x y. (x,y):r --> (!z. (x,z):r --> y=z) ==> Univalent r";
|
paulson@7031
|
400 |
by (assume_tac 1);
|
paulson@7031
|
401 |
qed "UnivalentI";
|
oheimb@4760
|
402 |
|
paulson@7031
|
403 |
Goalw [Univalent_def]
|
paulson@7031
|
404 |
"[| Univalent r; (x,y):r; (x,z):r|] ==> y=z";
|
paulson@7031
|
405 |
by Auto_tac;
|
paulson@7031
|
406 |
qed "UnivalentD";
|
paulson@5231
|
407 |
|
paulson@5231
|
408 |
|
paulson@5231
|
409 |
(** Graphs of partial functions **)
|
paulson@5231
|
410 |
|
paulson@5231
|
411 |
Goal "Domain{(x,y). y = f x & P x} = {x. P x}";
|
paulson@5231
|
412 |
by (Blast_tac 1);
|
paulson@5231
|
413 |
qed "Domain_partial_func";
|
paulson@5231
|
414 |
|
paulson@5231
|
415 |
Goal "Range{(x,y). y = f x & P x} = f``{x. P x}";
|
paulson@5231
|
416 |
by (Blast_tac 1);
|
paulson@5231
|
417 |
qed "Range_partial_func";
|
paulson@5231
|
418 |
|
berghofe@7014
|
419 |
|
berghofe@7014
|
420 |
(** Composition of function and relation **)
|
berghofe@7014
|
421 |
|
berghofe@7014
|
422 |
Goalw [fun_rel_comp_def] "A <= B ==> fun_rel_comp f A <= fun_rel_comp f B";
|
berghofe@7014
|
423 |
by (Fast_tac 1);
|
berghofe@7014
|
424 |
qed "fun_rel_comp_mono";
|
berghofe@7014
|
425 |
|
berghofe@7014
|
426 |
Goalw [fun_rel_comp_def] "! x. ?! y. (f x, y) : R ==> ?! g. g : fun_rel_comp f R";
|
berghofe@7014
|
427 |
by (res_inst_tac [("a","%x. @y. (f x, y) : R")] ex1I 1);
|
berghofe@7014
|
428 |
by (rtac CollectI 1);
|
berghofe@7014
|
429 |
by (rtac allI 1);
|
berghofe@7014
|
430 |
by (etac allE 1);
|
berghofe@7014
|
431 |
by (rtac (select_eq_Ex RS iffD2) 1);
|
berghofe@7014
|
432 |
by (etac ex1_implies_ex 1);
|
berghofe@7014
|
433 |
by (rtac ext 1);
|
berghofe@7014
|
434 |
by (etac CollectE 1);
|
berghofe@7014
|
435 |
by (REPEAT (etac allE 1));
|
berghofe@7014
|
436 |
by (rtac (select1_equality RS sym) 1);
|
berghofe@7014
|
437 |
by (atac 1);
|
berghofe@7014
|
438 |
by (atac 1);
|
berghofe@7014
|
439 |
qed "fun_rel_comp_unique";
|