author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 2033  639de962ded4 
permissions  rwrr 
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 

760  11 
qed_goalw "converse_iff" ZF.thy [converse_def] 
687  12 
"<a,b>: converse(r) <> <b,a>:r" 
13 
(fn _ => [ (fast_tac pair_cs 1) ]); 

14 

760  15 
qed_goalw "converseI" ZF.thy [converse_def] 
0  16 
"!!a b r. <a,b>:r ==> <b,a>:converse(r)" 
17 
(fn _ => [ (fast_tac pair_cs 1) ]); 

18 

760  19 
qed_goalw "converseD" ZF.thy [converse_def] 
0  20 
"!!a b r. <a,b> : converse(r) ==> <b,a> : r" 
21 
(fn _ => [ (fast_tac pair_cs 1) ]); 

22 

760  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 

33 
val converse_cs = pair_cs addSIs [converseI] 

1461  34 
addSEs [converseD,converseE]; 
0  35 

795  36 
qed_goal "converse_converse" ZF.thy 
0  37 
"!!A B r. r<=Sigma(A,B) ==> converse(converse(r)) = r" 
38 
(fn _ => [ (fast_tac (converse_cs addSIs [equalityI]) 1) ]); 

39 

760  40 
qed_goal "converse_type" ZF.thy "!!A B r. r<=A*B ==> converse(r)<=B*A" 
0  41 
(fn _ => [ (fast_tac converse_cs 1) ]); 
42 

795  43 
qed_goal "converse_prod" ZF.thy "converse(A*B) = B*A" 
0  44 
(fn _ => [ (fast_tac (converse_cs addSIs [equalityI]) 1) ]); 
45 

760  46 
qed_goal "converse_empty" ZF.thy "converse(0) = 0" 
0  47 
(fn _ => [ (fast_tac (converse_cs addSIs [equalityI]) 1) ]); 
48 

49 
(*** domain ***) 

50 

760  51 
qed_goalw "domain_iff" ZF.thy [domain_def] 
0  52 
"a: domain(r) <> (EX y. <a,y>: r)" 
53 
(fn _=> [ (fast_tac pair_cs 1) ]); 

54 

760  55 
qed_goal "domainI" ZF.thy "!!a b r. <a,b>: r ==> a: domain(r)" 
0  56 
(fn _ => [ (etac (exI RS (domain_iff RS iffD2)) 1) ]); 
57 

760  58 
qed_goal "domainE" ZF.thy 
0  59 
"[ a : domain(r); !!y. <a,y>: r ==> P ] ==> P" 
60 
(fn prems=> 

61 
[ (rtac (domain_iff RS iffD1 RS exE) 1), 

62 
(REPEAT (ares_tac prems 1)) ]); 

63 

760  64 
qed_goal "domain_subset" ZF.thy "domain(Sigma(A,B)) <= A" 
536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
14
diff
changeset

65 
(fn _ => [ (rtac subsetI 1), (etac domainE 1), (etac SigmaD1 1) ]); 
0  66 

67 

68 
(*** range ***) 

69 

760  70 
qed_goalw "rangeI" ZF.thy [range_def] "!!a b r.<a,b>: r ==> b : range(r)" 
0  71 
(fn _ => [ (etac (converseI RS domainI) 1) ]); 
72 

760  73 
qed_goalw "rangeE" ZF.thy [range_def] 
0  74 
"[ b : range(r); !!x. <x,b>: r ==> P ] ==> P" 
75 
(fn major::prems=> 

76 
[ (rtac (major RS domainE) 1), 

77 
(resolve_tac prems 1), 

78 
(etac converseD 1) ]); 

79 

760  80 
qed_goalw "range_subset" ZF.thy [range_def] "range(A*B) <= B" 
0  81 
(fn _ => 
795  82 
[ (rtac (converse_prod RS ssubst) 1), 
0  83 
(rtac domain_subset 1) ]); 
84 

85 

86 
(*** field ***) 

87 

760  88 
qed_goalw "fieldI1" ZF.thy [field_def] "<a,b>: r ==> a : field(r)" 
0  89 
(fn [prem]=> 
90 
[ (rtac (prem RS domainI RS UnI1) 1) ]); 

91 

760  92 
qed_goalw "fieldI2" ZF.thy [field_def] "<a,b>: r ==> b : field(r)" 
0  93 
(fn [prem]=> 
94 
[ (rtac (prem RS rangeI RS UnI2) 1) ]); 

95 

760  96 
qed_goalw "fieldCI" ZF.thy [field_def] 
0  97 
"(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)" 
98 
(fn [prem]=> 

99 
[ (rtac (prem RS domainI RS UnCI) 1), 

100 
(swap_res_tac [rangeI] 1), 

101 
(etac notnotD 1) ]); 

102 

760  103 
qed_goalw "fieldE" ZF.thy [field_def] 
0  104 
"[ a : field(r); \ 
105 
\ !!x. <a,x>: r ==> P; \ 

106 
\ !!x. <x,a>: r ==> P ] ==> P" 

107 
(fn major::prems=> 

108 
[ (rtac (major RS UnE) 1), 

109 
(REPEAT (eresolve_tac (prems@[domainE,rangeE]) 1)) ]); 

110 

760  111 
qed_goal "field_subset" ZF.thy "field(A*B) <= A Un B" 
0  112 
(fn _ => [ (fast_tac (pair_cs addIs [fieldCI] addSEs [fieldE]) 1) ]); 
113 

760  114 
qed_goalw "domain_subset_field" ZF.thy [field_def] 
0  115 
"domain(r) <= field(r)" 
116 
(fn _ => [ (rtac Un_upper1 1) ]); 

117 

760  118 
qed_goalw "range_subset_field" ZF.thy [field_def] 
0  119 
"range(r) <= field(r)" 
120 
(fn _ => [ (rtac Un_upper2 1) ]); 

121 

760  122 
qed_goal "domain_times_range" ZF.thy 
0  123 
"!!A B r. r <= Sigma(A,B) ==> r <= domain(r)*range(r)" 
124 
(fn _ => [ (fast_tac (pair_cs addIs [domainI,rangeI]) 1) ]); 

125 

760  126 
qed_goal "field_times_field" ZF.thy 
0  127 
"!!A B r. r <= Sigma(A,B) ==> r <= field(r)*field(r)" 
128 
(fn _ => [ (fast_tac (pair_cs addIs [fieldI1,fieldI2]) 1) ]); 

129 

130 

131 
(*** Image of a set under a function/relation ***) 

132 

760  133 
qed_goalw "image_iff" ZF.thy [image_def] 
0  134 
"b : r``A <> (EX x:A. <x,b>:r)" 
135 
(fn _ => [ fast_tac (pair_cs addIs [rangeI]) 1 ]); 

136 

760  137 
qed_goal "image_singleton_iff" ZF.thy 
0  138 
"b : r``{a} <> <a,b>:r" 
139 
(fn _ => [ rtac (image_iff RS iff_trans) 1, 

1461  140 
fast_tac pair_cs 1 ]); 
0  141 

760  142 
qed_goalw "imageI" ZF.thy [image_def] 
0  143 
"!!a b r. [ <a,b>: r; a:A ] ==> b : r``A" 
144 
(fn _ => [ (REPEAT (ares_tac [CollectI,rangeI,bexI] 1)) ]); 

145 

760  146 
qed_goalw "imageE" ZF.thy [image_def] 
0  147 
"[ b: r``A; !!x.[ <x,b>: r; x:A ] ==> P ] ==> P" 
148 
(fn major::prems=> 

149 
[ (rtac (major RS CollectE) 1), 

150 
(REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]); 

151 

760  152 
qed_goal "image_subset" ZF.thy 
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

153 
"!!A B r. r <= A*B ==> r``C <= B" 
674  154 
(fn _ => [ (fast_tac (pair_cs addSEs [imageE]) 1) ]); 
0  155 

156 

157 
(*** Inverse image of a set under a function/relation ***) 

158 

760  159 
qed_goalw "vimage_iff" ZF.thy [vimage_def,image_def,converse_def] 
0  160 
"a : r``B <> (EX y:B. <a,y>:r)" 
161 
(fn _ => [ fast_tac (pair_cs addIs [rangeI]) 1 ]); 

162 

760  163 
qed_goal "vimage_singleton_iff" ZF.thy 
0  164 
"a : r``{b} <> <a,b>:r" 
165 
(fn _ => [ rtac (vimage_iff RS iff_trans) 1, 

1461  166 
fast_tac pair_cs 1 ]); 
0  167 

760  168 
qed_goalw "vimageI" ZF.thy [vimage_def] 
0  169 
"!!A B r. [ <a,b>: r; b:B ] ==> a : r``B" 
170 
(fn _ => [ (REPEAT (ares_tac [converseI RS imageI] 1)) ]); 

171 

760  172 
qed_goalw "vimageE" ZF.thy [vimage_def] 
0  173 
"[ a: r``B; !!x.[ <a,x>: r; x:B ] ==> P ] ==> P" 
174 
(fn major::prems=> 

175 
[ (rtac (major RS imageE) 1), 

176 
(REPEAT (etac converseD 1 ORELSE ares_tac prems 1)) ]); 

177 

760  178 
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

179 
"!!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

180 
(fn _ => [ (etac (converse_type RS image_subset) 1) ]); 
0  181 

182 

183 
(** Theoremproving for ZF set theory **) 

184 

185 
val ZF_cs = pair_cs 

186 
addSIs [converseI] 

187 
addIs [imageI, vimageI, domainI, rangeI, fieldCI] 

188 
addSEs [imageE, vimageE, domainE, rangeE, fieldE, converseD, converseE]; 

189 

190 
val eq_cs = ZF_cs addSIs [equalityI]; 

191 

192 
(** The Union of a set of relations is a relation  Lemma for fun_Union **) 

193 
goal ZF.thy "!!S. (ALL x:S. EX A B. x <= A*B) ==> \ 

194 
\ Union(S) <= domain(Union(S)) * range(Union(S))"; 

195 
by (fast_tac ZF_cs 1); 

760  196 
qed "rel_Union"; 
0  197 

198 
(** The Union of 2 relations is a relation (Lemma for fun_Un) **) 

760  199 
qed_goal "rel_Un" ZF.thy 
0  200 
"!!r s. [ r <= A*B; s <= C*D ] ==> (r Un s) <= (A Un C) * (B Un D)" 
201 
(fn _ => [ (fast_tac ZF_cs 1) ]); 

202 

203 