author | paulson |
Mon, 27 Jul 1998 16:04:20 +0200 | |
changeset 5202 | 084ceb3844f5 |
parent 4091 | 771b1f6422a8 |
child 5325 | f7a5e06adea1 |
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 |
||
2877 | 11 |
qed_goalw "converse_iff" ZF.thy [converse_def] |
687 | 12 |
"<a,b>: converse(r) <-> <b,a>:r" |
2877 | 13 |
(fn _ => [ (Blast_tac 1) ]); |
687 | 14 |
|
2877 | 15 |
qed_goalw "converseI" ZF.thy [converse_def] |
0 | 16 |
"!!a b r. <a,b>:r ==> <b,a>:converse(r)" |
2877 | 17 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 18 |
|
2877 | 19 |
qed_goalw "converseD" ZF.thy [converse_def] |
0 | 20 |
"!!a b r. <a,b> : converse(r) ==> <b,a> : r" |
2877 | 21 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 22 |
|
2877 | 23 |
qed_goalw "converseE" ZF.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 |
|
2877 | 37 |
qed_goal "converse_converse" ZF.thy |
0 | 38 |
"!!A B r. r<=Sigma(A,B) ==> converse(converse(r)) = r" |
2877 | 39 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 40 |
|
2877 | 41 |
qed_goal "converse_type" ZF.thy "!!A B r. r<=A*B ==> converse(r)<=B*A" |
42 |
(fn _ => [ (Blast_tac 1) ]); |
|
0 | 43 |
|
2877 | 44 |
qed_goal "converse_prod" ZF.thy "converse(A*B) = B*A" |
45 |
(fn _ => [ (Blast_tac 1) ]); |
|
0 | 46 |
|
2877 | 47 |
qed_goal "converse_empty" ZF.thy "converse(0) = 0" |
48 |
(fn _ => [ (Blast_tac 1) ]); |
|
2469 | 49 |
|
50 |
Addsimps [converse_prod, converse_empty]; |
|
0 | 51 |
|
5202 | 52 |
val converse_subset_iff = prove_goal ZF.thy |
53 |
"!!z. A <= Sigma(X,Y) ==> converse(A) <= converse(B) <-> A <= B" |
|
54 |
(fn _=> [ (Blast_tac 1) ]); |
|
55 |
||
56 |
||
0 | 57 |
(*** domain ***) |
58 |
||
2877 | 59 |
qed_goalw "domain_iff" ZF.thy [domain_def] |
0 | 60 |
"a: domain(r) <-> (EX y. <a,y>: r)" |
2877 | 61 |
(fn _=> [ (Blast_tac 1) ]); |
0 | 62 |
|
2877 | 63 |
qed_goal "domainI" ZF.thy "!!a b r. <a,b>: r ==> a: domain(r)" |
2469 | 64 |
(fn _=> [ (etac (exI RS (domain_iff RS iffD2)) 1) ]); |
0 | 65 |
|
2877 | 66 |
qed_goal "domainE" ZF.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 |
|
2877 | 75 |
qed_goal "domain_subset" ZF.thy "domain(Sigma(A,B)) <= A" |
76 |
(fn _=> [ (Blast_tac 1) ]); |
|
0 | 77 |
|
78 |
(*** range ***) |
|
79 |
||
2877 | 80 |
qed_goalw "rangeI" ZF.thy [range_def] "!!a b r.<a,b>: r ==> b : range(r)" |
0 | 81 |
(fn _ => [ (etac (converseI RS domainI) 1) ]); |
82 |
||
2877 | 83 |
qed_goalw "rangeE" ZF.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 |
||
2877 | 93 |
qed_goalw "range_subset" ZF.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 |
||
2877 | 101 |
qed_goalw "fieldI1" ZF.thy [field_def] "!!r. <a,b>: r ==> a : field(r)" |
102 |
(fn _ => [ (Blast_tac 1) ]); |
|
0 | 103 |
|
2877 | 104 |
qed_goalw "fieldI2" ZF.thy [field_def] "!!r. <a,b>: r ==> b : field(r)" |
105 |
(fn _ => [ (Blast_tac 1) ]); |
|
0 | 106 |
|
2877 | 107 |
qed_goalw "fieldCI" ZF.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 |
|
2877 | 111 |
qed_goalw "fieldE" ZF.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 |
|
2877 | 122 |
qed_goal "field_subset" ZF.thy "field(A*B) <= A Un B" |
123 |
(fn _ => [ (Blast_tac 1) ]); |
|
2469 | 124 |
|
2877 | 125 |
qed_goalw "domain_subset_field" ZF.thy [field_def] |
0 | 126 |
"domain(r) <= field(r)" |
127 |
(fn _ => [ (rtac Un_upper1 1) ]); |
|
128 |
||
2877 | 129 |
qed_goalw "range_subset_field" ZF.thy [field_def] |
0 | 130 |
"range(r) <= field(r)" |
131 |
(fn _ => [ (rtac Un_upper2 1) ]); |
|
132 |
||
2877 | 133 |
qed_goal "domain_times_range" ZF.thy |
0 | 134 |
"!!A B r. r <= Sigma(A,B) ==> r <= domain(r)*range(r)" |
2877 | 135 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 136 |
|
2877 | 137 |
qed_goal "field_times_field" ZF.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 |
||
2877 | 144 |
qed_goalw "image_iff" ZF.thy [image_def] "b : r``A <-> (EX x:A. <x,b>:r)" |
145 |
(fn _ => [ (Blast_tac 1) ]); |
|
0 | 146 |
|
2877 | 147 |
qed_goal "image_singleton_iff" ZF.thy "b : r``{a} <-> <a,b>:r" |
0 | 148 |
(fn _ => [ rtac (image_iff RS iff_trans) 1, |
2877 | 149 |
Blast_tac 1 ]); |
0 | 150 |
|
2877 | 151 |
qed_goalw "imageI" ZF.thy [image_def] |
0 | 152 |
"!!a b r. [| <a,b>: r; a:A |] ==> b : r``A" |
2877 | 153 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 154 |
|
2877 | 155 |
qed_goalw "imageE" ZF.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 |
||
2877 | 164 |
qed_goal "image_subset" ZF.thy "!!A B r. r <= A*B ==> r``C <= B" |
165 |
(fn _ => [ (Blast_tac 1) ]); |
|
0 | 166 |
|
167 |
||
168 |
(*** Inverse image of a set under a function/relation ***) |
|
169 |
||
2877 | 170 |
qed_goalw "vimage_iff" ZF.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 |
|
2877 | 174 |
qed_goal "vimage_singleton_iff" ZF.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 |
|
2877 | 179 |
qed_goalw "vimageI" ZF.thy [vimage_def] |
0 | 180 |
"!!A B r. [| <a,b>: r; b:B |] ==> a : r-``B" |
2877 | 181 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 182 |
|
2877 | 183 |
qed_goalw "vimageE" ZF.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 |
||
2877 | 189 |
qed_goalw "vimage_subset" ZF.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 **) |
|
2877 | 202 |
goal ZF.thy "!!S. (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) **) |
|
2877 | 208 |
qed_goal "rel_Un" ZF.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 |
||
2877 | 213 |
goal ZF.thy "!!r. [| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)"; |
214 |
by (Blast_tac 1); |
|
2469 | 215 |
qed "domain_Diff_eq"; |
216 |
||
2877 | 217 |
goal ZF.thy "!!r. [| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = range(r)"; |
218 |
by (Blast_tac 1); |
|
2469 | 219 |
qed "range_Diff_eq"; |
220 |