author  lcp 
Thu, 30 Sep 1993 10:10:21 +0100  
changeset 14  1c0926788772 
parent 0  a5a9c433f639 
child 536  5fbfa997f1b0 
permissions  rwrr 
0  1 
(* Title: ZF/domrange 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1991 University of Cambridge 

5 

6 
Converse, domain, range of a relation or function 

7 
*) 

8 

9 
(*** converse ***) 

10 

11 
val converseI = prove_goalw ZF.thy [converse_def] 

12 
"!!a b r. <a,b>:r ==> <b,a>:converse(r)" 

13 
(fn _ => [ (fast_tac pair_cs 1) ]); 

14 

15 
val converseD = prove_goalw ZF.thy [converse_def] 

16 
"!!a b r. <a,b> : converse(r) ==> <b,a> : r" 

17 
(fn _ => [ (fast_tac pair_cs 1) ]); 

18 

19 
val converseE = prove_goalw ZF.thy [converse_def] 

20 
"[ yx : converse(r); \ 

21 
\ !!x y. [ yx=<y,x>; <x,y>:r ] ==> P \ 

22 
\ ] ==> P" 

23 
(fn [major,minor]=> 

24 
[ (rtac (major RS ReplaceE) 1), 

25 
(REPEAT (eresolve_tac [exE, conjE, minor] 1)), 

26 
(hyp_subst_tac 1), 

27 
(assume_tac 1) ]); 

28 

29 
val converse_cs = pair_cs addSIs [converseI] 

30 
addSEs [converseD,converseE]; 

31 

32 
val converse_of_converse = prove_goal ZF.thy 

33 
"!!A B r. r<=Sigma(A,B) ==> converse(converse(r)) = r" 

34 
(fn _ => [ (fast_tac (converse_cs addSIs [equalityI]) 1) ]); 

35 

36 
val converse_type = prove_goal ZF.thy "!!A B r. r<=A*B ==> converse(r)<=B*A" 

37 
(fn _ => [ (fast_tac converse_cs 1) ]); 

38 

39 
val converse_of_prod = prove_goal ZF.thy "converse(A*B) = B*A" 

40 
(fn _ => [ (fast_tac (converse_cs addSIs [equalityI]) 1) ]); 

41 

42 
val converse_empty = prove_goal ZF.thy "converse(0) = 0" 

43 
(fn _ => [ (fast_tac (converse_cs addSIs [equalityI]) 1) ]); 

44 

45 
(*** domain ***) 

46 

47 
val domain_iff = prove_goalw ZF.thy [domain_def] 

48 
"a: domain(r) <> (EX y. <a,y>: r)" 

49 
(fn _=> [ (fast_tac pair_cs 1) ]); 

50 

51 
val domainI = prove_goal ZF.thy "!!a b r. <a,b>: r ==> a: domain(r)" 

52 
(fn _ => [ (etac (exI RS (domain_iff RS iffD2)) 1) ]); 

53 

54 
val domainE = prove_goal ZF.thy 

55 
"[ a : domain(r); !!y. <a,y>: r ==> P ] ==> P" 

56 
(fn prems=> 

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

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

59 

60 
val domain_of_prod = prove_goal ZF.thy "!!A B. b:B ==> domain(A*B) = A" 

61 
(fn _ => 

62 
[ (REPEAT (eresolve_tac [domainE,SigmaE2] 1 

63 
ORELSE ares_tac [domainI,equalityI,subsetI,SigmaI] 1)) ]); 

64 

65 
val domain_empty = prove_goal ZF.thy "domain(0) = 0" 

66 
(fn _ => 

67 
[ (REPEAT (eresolve_tac [domainE,emptyE] 1 

68 
ORELSE ares_tac [equalityI,subsetI] 1)) ]); 

69 

70 
val domain_subset = prove_goal ZF.thy "domain(Sigma(A,B)) <= A" 

71 
(fn _ => 

72 
[ (rtac subsetI 1), 

73 
(etac domainE 1), 

74 
(etac SigmaD1 1) ]); 

75 

76 

77 
(*** range ***) 

78 

79 
val rangeI = prove_goalw ZF.thy [range_def] "!!a b r.<a,b>: r ==> b : range(r)" 

80 
(fn _ => [ (etac (converseI RS domainI) 1) ]); 

81 

82 
val rangeE = prove_goalw ZF.thy [range_def] 

83 
"[ b : range(r); !!x. <x,b>: r ==> P ] ==> P" 

84 
(fn major::prems=> 

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

86 
(resolve_tac prems 1), 

87 
(etac converseD 1) ]); 

88 

89 
val range_of_prod = prove_goalw ZF.thy [range_def] 

90 
"!!a A B. a:A ==> range(A*B) = B" 

91 
(fn _ => 

92 
[ (rtac (converse_of_prod RS ssubst) 1), 

93 
(etac domain_of_prod 1) ]); 

94 

95 
val range_empty = prove_goalw ZF.thy [range_def] "range(0) = 0" 

96 
(fn _ => 

97 
[ (rtac (converse_empty RS ssubst) 1), 

98 
(rtac domain_empty 1) ]); 

99 

100 
val range_subset = prove_goalw ZF.thy [range_def] "range(A*B) <= B" 

101 
(fn _ => 

102 
[ (rtac (converse_of_prod RS ssubst) 1), 

103 
(rtac domain_subset 1) ]); 

104 

105 

106 
(*** field ***) 

107 

108 
val fieldI1 = prove_goalw ZF.thy [field_def] "<a,b>: r ==> a : field(r)" 

109 
(fn [prem]=> 

110 
[ (rtac (prem RS domainI RS UnI1) 1) ]); 

111 

112 
val fieldI2 = prove_goalw ZF.thy [field_def] "<a,b>: r ==> b : field(r)" 

113 
(fn [prem]=> 

114 
[ (rtac (prem RS rangeI RS UnI2) 1) ]); 

115 

116 
val fieldCI = prove_goalw ZF.thy [field_def] 

117 
"(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)" 

118 
(fn [prem]=> 

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

120 
(swap_res_tac [rangeI] 1), 

121 
(etac notnotD 1) ]); 

122 

123 
val fieldE = prove_goalw ZF.thy [field_def] 

124 
"[ a : field(r); \ 

125 
\ !!x. <a,x>: r ==> P; \ 

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

127 
(fn major::prems=> 

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

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

130 

131 
val field_of_prod = prove_goal ZF.thy "field(A*A) = A" 

132 
(fn _ => 

133 
[ (fast_tac (pair_cs addIs [fieldCI,equalityI] addSEs [fieldE]) 1) ]); 

134 

135 
val field_subset = prove_goal ZF.thy "field(A*B) <= A Un B" 

136 
(fn _ => [ (fast_tac (pair_cs addIs [fieldCI] addSEs [fieldE]) 1) ]); 

137 

138 
val domain_subset_field = prove_goalw ZF.thy [field_def] 

139 
"domain(r) <= field(r)" 

140 
(fn _ => [ (rtac Un_upper1 1) ]); 

141 

142 
val range_subset_field = prove_goalw ZF.thy [field_def] 

143 
"range(r) <= field(r)" 

144 
(fn _ => [ (rtac Un_upper2 1) ]); 

145 

146 
val domain_times_range = prove_goal ZF.thy 

147 
"!!A B r. r <= Sigma(A,B) ==> r <= domain(r)*range(r)" 

148 
(fn _ => [ (fast_tac (pair_cs addIs [domainI,rangeI]) 1) ]); 

149 

150 
val field_times_field = prove_goal ZF.thy 

151 
"!!A B r. r <= Sigma(A,B) ==> r <= field(r)*field(r)" 

152 
(fn _ => [ (fast_tac (pair_cs addIs [fieldI1,fieldI2]) 1) ]); 

153 

154 

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

156 

157 
val image_iff = prove_goalw ZF.thy [image_def] 

158 
"b : r``A <> (EX x:A. <x,b>:r)" 

159 
(fn _ => [ fast_tac (pair_cs addIs [rangeI]) 1 ]); 

160 

161 
val image_singleton_iff = prove_goal ZF.thy 

162 
"b : r``{a} <> <a,b>:r" 

163 
(fn _ => [ rtac (image_iff RS iff_trans) 1, 

164 
fast_tac pair_cs 1 ]); 

165 

166 
val imageI = prove_goalw ZF.thy [image_def] 

167 
"!!a b r. [ <a,b>: r; a:A ] ==> b : r``A" 

168 
(fn _ => [ (REPEAT (ares_tac [CollectI,rangeI,bexI] 1)) ]); 

169 

170 
val imageE = prove_goalw ZF.thy [image_def] 

171 
"[ b: r``A; !!x.[ <x,b>: r; x:A ] ==> P ] ==> P" 

172 
(fn major::prems=> 

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

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

175 

176 
val image_subset = prove_goal ZF.thy 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

177 
"!!A B r. r <= A*B ==> r``C <= B" 
0  178 
(fn _ => 
179 
[ (rtac subsetI 1), 

180 
(REPEAT (eresolve_tac [asm_rl, imageE, subsetD RS SigmaD2] 1)) ]); 

181 

182 

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

184 

185 
val vimage_iff = prove_goalw ZF.thy [vimage_def,image_def,converse_def] 

186 
"a : r``B <> (EX y:B. <a,y>:r)" 

187 
(fn _ => [ fast_tac (pair_cs addIs [rangeI]) 1 ]); 

188 

189 
val vimage_singleton_iff = prove_goal ZF.thy 

190 
"a : r``{b} <> <a,b>:r" 

191 
(fn _ => [ rtac (vimage_iff RS iff_trans) 1, 

192 
fast_tac pair_cs 1 ]); 

193 

194 
val vimageI = prove_goalw ZF.thy [vimage_def] 

195 
"!!A B r. [ <a,b>: r; b:B ] ==> a : r``B" 

196 
(fn _ => [ (REPEAT (ares_tac [converseI RS imageI] 1)) ]); 

197 

198 
val vimageE = prove_goalw ZF.thy [vimage_def] 

199 
"[ a: r``B; !!x.[ <a,x>: r; x:B ] ==> P ] ==> P" 

200 
(fn major::prems=> 

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

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

203 

204 
val vimage_subset = prove_goalw ZF.thy [vimage_def] 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

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

206 
(fn _ => [ (etac (converse_type RS image_subset) 1) ]); 
0  207 

208 

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

210 

211 
val ZF_cs = pair_cs 

212 
addSIs [converseI] 

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

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

215 

216 
val eq_cs = ZF_cs addSIs [equalityI]; 

217 

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

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

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

221 
by (fast_tac ZF_cs 1); 

222 
val rel_Union = result(); 

223 

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

225 
val rel_Un = prove_goal ZF.thy 

226 
"!!r s. [ r <= A*B; s <= C*D ] ==> (r Un s) <= (A Un C) * (B Un D)" 

227 
(fn _ => [ (fast_tac ZF_cs 1) ]); 

228 

229 