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