author | wenzelm |
Sat, 15 Apr 2000 15:00:57 +0200 | |
changeset 8717 | 20c42415c07d |
parent 5325 | f7a5e06adea1 |
child 9180 | 3bda56c0d70d |
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 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
37 |
qed_goal "converse_converse" thy |
0 | 38 |
"!!A B r. r<=Sigma(A,B) ==> converse(converse(r)) = r" |
2877 | 39 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 40 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
41 |
qed_goal "converse_type" thy "!!A B r. r<=A*B ==> converse(r)<=B*A" |
2877 | 42 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 43 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
44 |
qed_goal "converse_prod" thy "converse(A*B) = B*A" |
2877 | 45 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 46 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
47 |
qed_goal "converse_empty" thy "converse(0) = 0" |
2877 | 48 |
(fn _ => [ (Blast_tac 1) ]); |
2469 | 49 |
|
50 |
Addsimps [converse_prod, converse_empty]; |
|
0 | 51 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
52 |
val converse_subset_iff = prove_goal thy |
5202 | 53 |
"!!z. A <= Sigma(X,Y) ==> converse(A) <= converse(B) <-> A <= B" |
54 |
(fn _=> [ (Blast_tac 1) ]); |
|
55 |
||
56 |
||
0 | 57 |
(*** domain ***) |
58 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
59 |
qed_goalw "domain_iff" thy [domain_def] |
0 | 60 |
"a: domain(r) <-> (EX y. <a,y>: r)" |
2877 | 61 |
(fn _=> [ (Blast_tac 1) ]); |
0 | 62 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
63 |
qed_goal "domainI" thy "!!a b r. <a,b>: r ==> a: domain(r)" |
2469 | 64 |
(fn _=> [ (etac (exI RS (domain_iff RS iffD2)) 1) ]); |
0 | 65 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
66 |
qed_goal "domainE" thy |
0 | 67 |
"[| a : domain(r); !!y. <a,y>: r ==> P |] ==> P" |
68 |
(fn prems=> |
|
69 |
[ (rtac (domain_iff RS iffD1 RS exE) 1), |
|
70 |
(REPEAT (ares_tac prems 1)) ]); |
|
71 |
||
2469 | 72 |
AddIs [domainI]; |
73 |
AddSEs [domainE]; |
|
0 | 74 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
75 |
qed_goal "domain_subset" thy "domain(Sigma(A,B)) <= A" |
2877 | 76 |
(fn _=> [ (Blast_tac 1) ]); |
0 | 77 |
|
78 |
(*** range ***) |
|
79 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
80 |
qed_goalw "rangeI" thy [range_def] "!!a b r.<a,b>: r ==> b : range(r)" |
0 | 81 |
(fn _ => [ (etac (converseI RS domainI) 1) ]); |
82 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
83 |
qed_goalw "rangeE" thy [range_def] |
0 | 84 |
"[| b : range(r); !!x. <x,b>: r ==> P |] ==> P" |
85 |
(fn major::prems=> |
|
86 |
[ (rtac (major RS domainE) 1), |
|
87 |
(resolve_tac prems 1), |
|
88 |
(etac converseD 1) ]); |
|
89 |
||
2469 | 90 |
AddIs [rangeI]; |
91 |
AddSEs [rangeE]; |
|
92 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
93 |
qed_goalw "range_subset" thy [range_def] "range(A*B) <= B" |
0 | 94 |
(fn _ => |
2033 | 95 |
[ (stac converse_prod 1), |
0 | 96 |
(rtac domain_subset 1) ]); |
97 |
||
98 |
||
99 |
(*** field ***) |
|
100 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
101 |
qed_goalw "fieldI1" thy [field_def] "!!r. <a,b>: r ==> a : field(r)" |
2877 | 102 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 103 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
104 |
qed_goalw "fieldI2" thy [field_def] "!!r. <a,b>: r ==> b : field(r)" |
2877 | 105 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 106 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
107 |
qed_goalw "fieldCI" thy [field_def] |
0 | 108 |
"(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)" |
4091 | 109 |
(fn [prem]=> [ (blast_tac (claset() addIs [prem]) 1) ]); |
0 | 110 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
111 |
qed_goalw "fieldE" thy [field_def] |
0 | 112 |
"[| a : field(r); \ |
113 |
\ !!x. <a,x>: r ==> P; \ |
|
114 |
\ !!x. <x,a>: r ==> P |] ==> P" |
|
115 |
(fn major::prems=> |
|
116 |
[ (rtac (major RS UnE) 1), |
|
117 |
(REPEAT (eresolve_tac (prems@[domainE,rangeE]) 1)) ]); |
|
118 |
||
2469 | 119 |
AddIs [fieldCI]; |
120 |
AddSEs [fieldE]; |
|
0 | 121 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
122 |
qed_goal "field_subset" thy "field(A*B) <= A Un B" |
2877 | 123 |
(fn _ => [ (Blast_tac 1) ]); |
2469 | 124 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
125 |
qed_goalw "domain_subset_field" thy [field_def] |
0 | 126 |
"domain(r) <= field(r)" |
127 |
(fn _ => [ (rtac Un_upper1 1) ]); |
|
128 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
129 |
qed_goalw "range_subset_field" thy [field_def] |
0 | 130 |
"range(r) <= field(r)" |
131 |
(fn _ => [ (rtac Un_upper2 1) ]); |
|
132 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
133 |
qed_goal "domain_times_range" thy |
0 | 134 |
"!!A B r. r <= Sigma(A,B) ==> r <= domain(r)*range(r)" |
2877 | 135 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 136 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
137 |
qed_goal "field_times_field" thy |
0 | 138 |
"!!A B r. r <= Sigma(A,B) ==> r <= field(r)*field(r)" |
2877 | 139 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 140 |
|
141 |
||
142 |
(*** Image of a set under a function/relation ***) |
|
143 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
144 |
qed_goalw "image_iff" thy [image_def] "b : r``A <-> (EX x:A. <x,b>:r)" |
2877 | 145 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 146 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
147 |
qed_goal "image_singleton_iff" thy "b : r``{a} <-> <a,b>:r" |
0 | 148 |
(fn _ => [ rtac (image_iff RS iff_trans) 1, |
2877 | 149 |
Blast_tac 1 ]); |
0 | 150 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
151 |
qed_goalw "imageI" thy [image_def] |
0 | 152 |
"!!a b r. [| <a,b>: r; a:A |] ==> b : r``A" |
2877 | 153 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 154 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
155 |
qed_goalw "imageE" thy [image_def] |
0 | 156 |
"[| b: r``A; !!x.[| <x,b>: r; x:A |] ==> P |] ==> P" |
157 |
(fn major::prems=> |
|
158 |
[ (rtac (major RS CollectE) 1), |
|
159 |
(REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]); |
|
160 |
||
2469 | 161 |
AddIs [imageI]; |
162 |
AddSEs [imageE]; |
|
163 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
164 |
qed_goal "image_subset" thy "!!A B r. r <= A*B ==> r``C <= B" |
2877 | 165 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 166 |
|
167 |
||
168 |
(*** Inverse image of a set under a function/relation ***) |
|
169 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
170 |
qed_goalw "vimage_iff" thy [vimage_def,image_def,converse_def] |
0 | 171 |
"a : r-``B <-> (EX y:B. <a,y>:r)" |
2877 | 172 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 173 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
174 |
qed_goal "vimage_singleton_iff" thy |
0 | 175 |
"a : r-``{b} <-> <a,b>:r" |
176 |
(fn _ => [ rtac (vimage_iff RS iff_trans) 1, |
|
2877 | 177 |
Blast_tac 1 ]); |
0 | 178 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
179 |
qed_goalw "vimageI" thy [vimage_def] |
0 | 180 |
"!!A B r. [| <a,b>: r; b:B |] ==> a : r-``B" |
2877 | 181 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 182 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
183 |
qed_goalw "vimageE" thy [vimage_def] |
0 | 184 |
"[| a: r-``B; !!x.[| <a,x>: r; x:B |] ==> P |] ==> P" |
185 |
(fn major::prems=> |
|
186 |
[ (rtac (major RS imageE) 1), |
|
187 |
(REPEAT (etac converseD 1 ORELSE ares_tac prems 1)) ]); |
|
188 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
189 |
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
|
190 |
"!!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
|
191 |
(fn _ => [ (etac (converse_type RS image_subset) 1) ]); |
0 | 192 |
|
193 |
||
194 |
(** Theorem-proving for ZF set theory **) |
|
195 |
||
2469 | 196 |
AddIs [vimageI]; |
197 |
AddSEs [vimageE]; |
|
198 |
||
4091 | 199 |
val ZF_cs = claset() delrules [equalityI]; |
0 | 200 |
|
201 |
(** 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
|
202 |
Goal "(ALL x:S. EX A B. x <= A*B) ==> \ |
0 | 203 |
\ Union(S) <= domain(Union(S)) * range(Union(S))"; |
2877 | 204 |
by (Blast_tac 1); |
760 | 205 |
qed "rel_Union"; |
0 | 206 |
|
207 |
(** The Union of 2 relations is a relation (Lemma for fun_Un) **) |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
208 |
qed_goal "rel_Un" thy |
0 | 209 |
"!!r s. [| r <= A*B; s <= C*D |] ==> (r Un s) <= (A Un C) * (B Un D)" |
2877 | 210 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 211 |
|
212 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
213 |
Goal "[| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)"; |
2877 | 214 |
by (Blast_tac 1); |
2469 | 215 |
qed "domain_Diff_eq"; |
216 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5202
diff
changeset
|
217 |
Goal "[| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = range(r)"; |
2877 | 218 |
by (Blast_tac 1); |
2469 | 219 |
qed "range_Diff_eq"; |
220 |