author | paulson |
Wed, 28 Jun 2000 12:34:08 +0200 | |
changeset 9180 | 3bda56c0d70d |
parent 5325 | f7a5e06adea1 |
child 9211 | 6236c5285bd8 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/domrange |
0 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1991 University of Cambridge |
5 |
||
6 |
Converse, domain, range of a relation or function |
|
7 |
*) |
|
8 |
||
9 |
(*** converse ***) |
|
10 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
11 |
qed_goalw "converse_iff" thy [converse_def] |
687 | 12 |
"<a,b>: converse(r) <-> <b,a>:r" |
2877 | 13 |
(fn _ => [ (Blast_tac 1) ]); |
687 | 14 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
15 |
qed_goalw "converseI" thy [converse_def] |
0 | 16 |
"!!a b r. <a,b>:r ==> <b,a>:converse(r)" |
2877 | 17 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 18 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
19 |
qed_goalw "converseD" thy [converse_def] |
0 | 20 |
"!!a b r. <a,b> : converse(r) ==> <b,a> : r" |
2877 | 21 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 22 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
23 |
qed_goalw "converseE" thy [converse_def] |
0 | 24 |
"[| yx : converse(r); \ |
25 |
\ !!x y. [| yx=<y,x>; <x,y>:r |] ==> P \ |
|
26 |
\ |] ==> P" |
|
27 |
(fn [major,minor]=> |
|
28 |
[ (rtac (major RS ReplaceE) 1), |
|
29 |
(REPEAT (eresolve_tac [exE, conjE, minor] 1)), |
|
30 |
(hyp_subst_tac 1), |
|
31 |
(assume_tac 1) ]); |
|
32 |
||
2469 | 33 |
Addsimps [converse_iff]; |
34 |
AddSIs [converseI]; |
|
35 |
AddSEs [converseD,converseE]; |
|
0 | 36 |
|
9180 | 37 |
Goal "r<=Sigma(A,B) ==> converse(converse(r)) = r"; |
38 |
by (Blast_tac 1) ; |
|
39 |
qed "converse_converse"; |
|
40 |
||
41 |
Goal "r<=A*B ==> converse(r)<=B*A"; |
|
42 |
by (Blast_tac 1) ; |
|
43 |
qed "converse_type"; |
|
0 | 44 |
|
9180 | 45 |
Goal "converse(A*B) = B*A"; |
46 |
by (Blast_tac 1) ; |
|
47 |
qed "converse_prod"; |
|
0 | 48 |
|
9180 | 49 |
Goal "converse(0) = 0"; |
50 |
by (Blast_tac 1) ; |
|
51 |
qed "converse_empty"; |
|
2469 | 52 |
|
53 |
Addsimps [converse_prod, converse_empty]; |
|
0 | 54 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
55 |
val converse_subset_iff = prove_goal thy |
5202 | 56 |
"!!z. A <= Sigma(X,Y) ==> converse(A) <= converse(B) <-> A <= B" |
57 |
(fn _=> [ (Blast_tac 1) ]); |
|
58 |
||
59 |
||
0 | 60 |
(*** domain ***) |
61 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
62 |
qed_goalw "domain_iff" thy [domain_def] |
0 | 63 |
"a: domain(r) <-> (EX y. <a,y>: r)" |
2877 | 64 |
(fn _=> [ (Blast_tac 1) ]); |
0 | 65 |
|
9180 | 66 |
Goal "<a,b>: r ==> a: domain(r)"; |
67 |
by (etac (exI RS (domain_iff RS iffD2)) 1) ; |
|
68 |
qed "domainI"; |
|
0 | 69 |
|
9180 | 70 |
val prems= Goal |
71 |
"[| a : domain(r); !!y. <a,y>: r ==> P |] ==> P"; |
|
72 |
by (rtac (domain_iff RS iffD1 RS exE) 1); |
|
73 |
by (REPEAT (ares_tac prems 1)) ; |
|
74 |
qed "domainE"; |
|
0 | 75 |
|
2469 | 76 |
AddIs [domainI]; |
77 |
AddSEs [domainE]; |
|
0 | 78 |
|
9180 | 79 |
Goal "domain(Sigma(A,B)) <= A"; |
80 |
by (Blast_tac 1) ; |
|
81 |
qed "domain_subset"; |
|
0 | 82 |
|
83 |
(*** range ***) |
|
84 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
85 |
qed_goalw "rangeI" thy [range_def] "!!a b r.<a,b>: r ==> b : range(r)" |
0 | 86 |
(fn _ => [ (etac (converseI RS domainI) 1) ]); |
87 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
88 |
qed_goalw "rangeE" thy [range_def] |
0 | 89 |
"[| b : range(r); !!x. <x,b>: r ==> P |] ==> P" |
90 |
(fn major::prems=> |
|
91 |
[ (rtac (major RS domainE) 1), |
|
92 |
(resolve_tac prems 1), |
|
93 |
(etac converseD 1) ]); |
|
94 |
||
2469 | 95 |
AddIs [rangeI]; |
96 |
AddSEs [rangeE]; |
|
97 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
98 |
qed_goalw "range_subset" thy [range_def] "range(A*B) <= B" |
0 | 99 |
(fn _ => |
2033 | 100 |
[ (stac converse_prod 1), |
0 | 101 |
(rtac domain_subset 1) ]); |
102 |
||
103 |
||
104 |
(*** field ***) |
|
105 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
106 |
qed_goalw "fieldI1" thy [field_def] "!!r. <a,b>: r ==> a : field(r)" |
2877 | 107 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 108 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
109 |
qed_goalw "fieldI2" thy [field_def] "!!r. <a,b>: r ==> b : field(r)" |
2877 | 110 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 111 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
112 |
qed_goalw "fieldCI" thy [field_def] |
0 | 113 |
"(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)" |
4091 | 114 |
(fn [prem]=> [ (blast_tac (claset() addIs [prem]) 1) ]); |
0 | 115 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
116 |
qed_goalw "fieldE" thy [field_def] |
0 | 117 |
"[| a : field(r); \ |
118 |
\ !!x. <a,x>: r ==> P; \ |
|
119 |
\ !!x. <x,a>: r ==> P |] ==> P" |
|
120 |
(fn major::prems=> |
|
121 |
[ (rtac (major RS UnE) 1), |
|
122 |
(REPEAT (eresolve_tac (prems@[domainE,rangeE]) 1)) ]); |
|
123 |
||
2469 | 124 |
AddIs [fieldCI]; |
125 |
AddSEs [fieldE]; |
|
0 | 126 |
|
9180 | 127 |
Goal "field(A*B) <= A Un B"; |
128 |
by (Blast_tac 1) ; |
|
129 |
qed "field_subset"; |
|
2469 | 130 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
131 |
qed_goalw "domain_subset_field" thy [field_def] |
0 | 132 |
"domain(r) <= field(r)" |
133 |
(fn _ => [ (rtac Un_upper1 1) ]); |
|
134 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
135 |
qed_goalw "range_subset_field" thy [field_def] |
0 | 136 |
"range(r) <= field(r)" |
137 |
(fn _ => [ (rtac Un_upper2 1) ]); |
|
138 |
||
9180 | 139 |
Goal "r <= Sigma(A,B) ==> r <= domain(r)*range(r)"; |
140 |
by (Blast_tac 1) ; |
|
141 |
qed "domain_times_range"; |
|
0 | 142 |
|
9180 | 143 |
Goal "r <= Sigma(A,B) ==> r <= field(r)*field(r)"; |
144 |
by (Blast_tac 1) ; |
|
145 |
qed "field_times_field"; |
|
0 | 146 |
|
147 |
||
148 |
(*** Image of a set under a function/relation ***) |
|
149 |
||
9180 | 150 |
Goalw [image_def] "b : r``A <-> (EX x:A. <x,b>:r)"; |
151 |
by (Blast_tac 1); |
|
152 |
qed "image_iff"; |
|
0 | 153 |
|
9180 | 154 |
Goal "b : r``{a} <-> <a,b>:r"; |
155 |
by (rtac (image_iff RS iff_trans) 1); |
|
156 |
by (Blast_tac 1) ; |
|
157 |
qed "image_singleton_iff"; |
|
0 | 158 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
159 |
qed_goalw "imageI" thy [image_def] |
0 | 160 |
"!!a b r. [| <a,b>: r; a:A |] ==> b : r``A" |
2877 | 161 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 162 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
163 |
qed_goalw "imageE" thy [image_def] |
0 | 164 |
"[| b: r``A; !!x.[| <x,b>: r; x:A |] ==> P |] ==> P" |
165 |
(fn major::prems=> |
|
166 |
[ (rtac (major RS CollectE) 1), |
|
167 |
(REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]); |
|
168 |
||
2469 | 169 |
AddIs [imageI]; |
170 |
AddSEs [imageE]; |
|
171 |
||
9180 | 172 |
Goal "r <= A*B ==> r``C <= B"; |
173 |
by (Blast_tac 1) ; |
|
174 |
qed "image_subset"; |
|
0 | 175 |
|
176 |
||
177 |
(*** Inverse image of a set under a function/relation ***) |
|
178 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
179 |
qed_goalw "vimage_iff" thy [vimage_def,image_def,converse_def] |
0 | 180 |
"a : r-``B <-> (EX y:B. <a,y>:r)" |
2877 | 181 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 182 |
|
9180 | 183 |
Goal "a : r-``{b} <-> <a,b>:r"; |
184 |
by (rtac (vimage_iff RS iff_trans) 1); |
|
185 |
by (Blast_tac 1) ; |
|
186 |
qed "vimage_singleton_iff"; |
|
0 | 187 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
188 |
qed_goalw "vimageI" thy [vimage_def] |
0 | 189 |
"!!A B r. [| <a,b>: r; b:B |] ==> a : r-``B" |
2877 | 190 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 191 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
192 |
qed_goalw "vimageE" thy [vimage_def] |
0 | 193 |
"[| a: r-``B; !!x.[| <a,x>: r; x:B |] ==> P |] ==> P" |
194 |
(fn major::prems=> |
|
195 |
[ (rtac (major RS imageE) 1), |
|
196 |
(REPEAT (etac converseD 1 ORELSE ares_tac prems 1)) ]); |
|
197 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
198 |
qed_goalw "vimage_subset" thy [vimage_def] |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset
|
199 |
"!!A B r. r <= A*B ==> r-``C <= A" |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset
|
200 |
(fn _ => [ (etac (converse_type RS image_subset) 1) ]); |
0 | 201 |
|
202 |
||
203 |
(** Theorem-proving for ZF set theory **) |
|
204 |
||
2469 | 205 |
AddIs [vimageI]; |
206 |
AddSEs [vimageE]; |
|
207 |
||
4091 | 208 |
val ZF_cs = claset() delrules [equalityI]; |
0 | 209 |
|
210 |
(** The Union of a set of relations is a relation -- Lemma for fun_Union **) |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
211 |
Goal "(ALL x:S. EX A B. x <= A*B) ==> \ |
0 | 212 |
\ Union(S) <= domain(Union(S)) * range(Union(S))"; |
2877 | 213 |
by (Blast_tac 1); |
760 | 214 |
qed "rel_Union"; |
0 | 215 |
|
216 |
(** The Union of 2 relations is a relation (Lemma for fun_Un) **) |
|
9180 | 217 |
Goal "[| r <= A*B; s <= C*D |] ==> (r Un s) <= (A Un C) * (B Un D)"; |
218 |
by (Blast_tac 1) ; |
|
219 |
qed "rel_Un"; |
|
0 | 220 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
221 |
Goal "[| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)"; |
2877 | 222 |
by (Blast_tac 1); |
2469 | 223 |
qed "domain_Diff_eq"; |
224 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
225 |
Goal "[| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = range(r)"; |
2877 | 226 |
by (Blast_tac 1); |
2469 | 227 |
qed "range_Diff_eq"; |
228 |