author  clasohm 
Wed, 07 Dec 1994 13:12:04 +0100  
changeset 760  f0200e91b272 
parent 737  436019ca97d7 
child 824  120fc7e857ba 
permissions  rwrr 
0  1 
(* Title: ZF/func 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1991 University of Cambridge 

5 

6 
Functions in ZermeloFraenkel Set Theory 

7 
*) 

8 

9 
(*** The Pi operator  dependent function space ***) 

10 

691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

11 
goalw ZF.thy [Pi_def] 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

12 
"f: Pi(A,B) <> function(f) & f<=Sigma(A,B) & A<=domain(f)"; 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

13 
by (fast_tac ZF_cs 1); 
760  14 
qed "Pi_iff"; 
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

15 

b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

16 
(*For upward compatibility with the former definition*) 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

17 
goalw ZF.thy [Pi_def, function_def] 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

18 
"f: Pi(A,B) <> f<=Sigma(A,B) & (ALL x:A. EX! y. <x,y>: f)"; 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

19 
by (safe_tac ZF_cs); 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

20 
by (best_tac ZF_cs 1); 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

21 
by (best_tac ZF_cs 1); 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

22 
by (set_mp_tac 1); 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

23 
by (deepen_tac ZF_cs 3 1); 
760  24 
qed "Pi_iff_old"; 
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

25 

b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

26 
goal ZF.thy "!!f. f: Pi(A,B) ==> function(f)"; 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

27 
by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff]) 1); 
760  28 
qed "fun_is_function"; 
0  29 

30 
(**Two "destruct" rules for Pi **) 

31 

32 
val [major] = goalw ZF.thy [Pi_def] "f: Pi(A,B) ==> f <= Sigma(A,B)"; 

691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

33 
by (rtac (major RS CollectD1 RS PowD) 1); 
760  34 
qed "fun_is_rel"; 
0  35 

691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

36 
goal ZF.thy "!!f. [ f: Pi(A,B); a:A ] ==> EX! y. <a,y>: f"; 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

37 
by (fast_tac (ZF_cs addSDs [Pi_iff_old RS iffD1]) 1); 
760  38 
qed "fun_unique_Pair"; 
0  39 

40 
val prems = goalw ZF.thy [Pi_def] 

41 
"[ A=A'; !!x. x:A' ==> B(x)=B'(x) ] ==> Pi(A,B) = Pi(A',B')"; 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

42 
by (simp_tac (FOL_ss addsimps prems addcongs [Sigma_cong]) 1); 
760  43 
qed "Pi_cong"; 
0  44 

485  45 
(*Weakening one function type to another; see also Pi_type*) 
0  46 
goalw ZF.thy [Pi_def] "!!f. [ f: A>B; B<=D ] ==> f: A>D"; 
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

47 
by (best_tac ZF_cs 1); 
760  48 
qed "fun_weaken_type"; 
0  49 

50 
(*Empty function spaces*) 

691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

51 
goalw ZF.thy [Pi_def, function_def] "Pi(0,A) = {0}"; 
519  52 
by (fast_tac eq_cs 1); 
760  53 
qed "Pi_empty1"; 
0  54 

55 
goalw ZF.thy [Pi_def] "!!A a. a:A ==> A>0 = 0"; 

519  56 
by (fast_tac eq_cs 1); 
760  57 
qed "Pi_empty2"; 
0  58 

519  59 
(*The empty function*) 
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

60 
goalw ZF.thy [Pi_def, function_def] "0: 0>A"; 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

61 
by (fast_tac ZF_cs 1); 
760  62 
qed "empty_fun"; 
519  63 

64 
(*The singleton function*) 

691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

65 
goalw ZF.thy [Pi_def, function_def] "{<a,b>} : {a} > {b}"; 
519  66 
by (fast_tac eq_cs 1); 
760  67 
qed "single_fun"; 
519  68 

0  69 
(*** Function Application ***) 
70 

691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

71 
goalw ZF.thy [Pi_def, function_def] 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

72 
"!!a b f. [ <a,b>: f; <a,c>: f; f: Pi(A,B) ] ==> b=c"; 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

73 
by (deepen_tac ZF_cs 3 1); 
760  74 
qed "apply_equality2"; 
0  75 

76 
goalw ZF.thy [apply_def] "!!a b f. [ <a,b>: f; f: Pi(A,B) ] ==> f`a = b"; 

77 
by (rtac the_equality 1); 

78 
by (rtac apply_equality2 2); 

79 
by (REPEAT (assume_tac 1)); 

760  80 
qed "apply_equality"; 
0  81 

517  82 
(*Applying a function outside its domain yields 0*) 
83 
goalw ZF.thy [apply_def] 

84 
"!!a b f. [ a ~: domain(f); f: Pi(A,B) ] ==> f`a = 0"; 

85 
by (rtac the_0 1); 

86 
by (fast_tac ZF_cs 1); 

760  87 
qed "apply_0"; 
517  88 

691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

89 
goal ZF.thy "!!f. [ f: Pi(A,B); c: f ] ==> EX x:A. c = <x,f`x>"; 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

90 
by (forward_tac [fun_is_rel] 1); 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

91 
by (fast_tac (ZF_cs addDs [apply_equality]) 1); 
760  92 
qed "Pi_memberD"; 
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

93 

b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

94 
goal ZF.thy "!!f. [ f: Pi(A,B); a:A ] ==> <a,f`a>: f"; 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

95 
by (rtac (fun_unique_Pair RS ex1E) 1); 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

96 
by (resolve_tac [apply_equality RS ssubst] 3); 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

97 
by (REPEAT (assume_tac 1)); 
760  98 
qed "apply_Pair"; 
0  99 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

100 
(*Conclusion is flexible  use res_inst_tac or else apply_funtype below!*) 
0  101 
goal ZF.thy "!!f. [ f: Pi(A,B); a:A ] ==> f`a : B(a)"; 
102 
by (rtac (fun_is_rel RS subsetD RS SigmaE2) 1); 

691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

103 
by (REPEAT (ares_tac [apply_Pair] 1)); 
760  104 
qed "apply_type"; 
0  105 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

106 
(*This version is acceptable to the simplifier*) 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

107 
goal ZF.thy "!!f. [ f: A>B; a:A ] ==> f`a : B"; 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

108 
by (REPEAT (ares_tac [apply_type] 1)); 
760  109 
qed "apply_funtype"; 
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

110 

0  111 
val [major] = goal ZF.thy 
112 
"f: Pi(A,B) ==> <a,b>: f <> a:A & f`a = b"; 

691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

113 
by (cut_facts_tac [major RS fun_is_rel] 1); 
0  114 
by (fast_tac (ZF_cs addSIs [major RS apply_Pair, 
115 
major RSN (2,apply_equality)]) 1); 

760  116 
qed "apply_iff"; 
0  117 

118 
(*Refining one Pi type to another*) 

691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

119 
val pi_prem::prems = goal ZF.thy 
0  120 
"[ f: Pi(A,C); !!x. x:A ==> f`x : B(x) ] ==> f : Pi(A,B)"; 
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

121 
by (cut_facts_tac [pi_prem] 1); 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

122 
by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff]) 1); 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

123 
by (fast_tac (ZF_cs addIs prems addSDs [pi_prem RS Pi_memberD]) 1); 
760  124 
qed "Pi_type"; 
0  125 

126 

127 
(** Elimination of membership in a function **) 

128 

129 
goal ZF.thy "!!a A. [ <a,b> : f; f: Pi(A,B) ] ==> a : A"; 

130 
by (REPEAT (ares_tac [fun_is_rel RS subsetD RS SigmaD1] 1)); 

760  131 
qed "domain_type"; 
0  132 

133 
goal ZF.thy "!!b B a. [ <a,b> : f; f: Pi(A,B) ] ==> b : B(a)"; 

134 
by (etac (fun_is_rel RS subsetD RS SigmaD2) 1); 

135 
by (assume_tac 1); 

760  136 
qed "range_type"; 
0  137 

138 
val prems = goal ZF.thy 

139 
"[ <a,b>: f; f: Pi(A,B); \ 

140 
\ [ a:A; b:B(a); f`a = b ] ==> P \ 

141 
\ ] ==> P"; 

142 
by (cut_facts_tac prems 1); 

143 
by (resolve_tac prems 1); 

144 
by (REPEAT (eresolve_tac [asm_rl,domain_type,range_type,apply_equality] 1)); 

760  145 
qed "Pair_mem_PiE"; 
0  146 

147 
(*** Lambda Abstraction ***) 

148 

149 
goalw ZF.thy [lam_def] "!!A b. a:A ==> <a,b(a)> : (lam x:A. b(x))"; 

150 
by (etac RepFunI 1); 

760  151 
qed "lamI"; 
0  152 

153 
val major::prems = goalw ZF.thy [lam_def] 

154 
"[ p: (lam x:A. b(x)); !!x.[ x:A; p=<x,b(x)> ] ==> P \ 

155 
\ ] ==> P"; 

156 
by (rtac (major RS RepFunE) 1); 

157 
by (REPEAT (ares_tac prems 1)); 

760  158 
qed "lamE"; 
0  159 

160 
goal ZF.thy "!!a b c. [ <a,c>: (lam x:A. b(x)) ] ==> c = b(a)"; 

161 
by (REPEAT (eresolve_tac [asm_rl,lamE,Pair_inject,ssubst] 1)); 

760  162 
qed "lamD"; 
0  163 

691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

164 
val prems = goalw ZF.thy [lam_def, Pi_def, function_def] 
0  165 
"[ !!x. x:A ==> b(x): B(x) ] ==> (lam x:A.b(x)) : Pi(A,B)"; 
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

166 
by (fast_tac (ZF_cs addIs prems) 1); 
760  167 
qed "lam_type"; 
0  168 

169 
goal ZF.thy "(lam x:A.b(x)) : A > {b(x). x:A}"; 

170 
by (REPEAT (ares_tac [refl,lam_type,RepFunI] 1)); 

760  171 
qed "lam_funtype"; 
0  172 

173 
goal ZF.thy "!!a A. a : A ==> (lam x:A.b(x)) ` a = b(a)"; 

174 
by (REPEAT (ares_tac [apply_equality,lam_funtype,lamI] 1)); 

760  175 
qed "beta"; 
0  176 

177 
(*congruence rule for lambda abstraction*) 

178 
val prems = goalw ZF.thy [lam_def] 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

179 
"[ A=A'; !!x. x:A' ==> b(x)=b'(x) ] ==> Lambda(A,b) = Lambda(A',b')"; 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

180 
by (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1); 
760  181 
qed "lam_cong"; 
0  182 

183 
val [major] = goal ZF.thy 

184 
"(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)"; 

185 
by (res_inst_tac [("x", "lam x: A. THE y. Q(x,y)")] exI 1); 

186 
by (rtac ballI 1); 

187 
by (rtac (beta RS ssubst) 1); 

188 
by (assume_tac 1); 

189 
by (etac (major RS theI) 1); 

760  190 
qed "lam_theI"; 
0  191 

192 

193 
(** Extensionality **) 

194 

195 
(*Semiextensionality!*) 

196 
val prems = goal ZF.thy 

197 
"[ f : Pi(A,B); g: Pi(C,D); A<=C; \ 

198 
\ !!x. x:A ==> f`x = g`x ] ==> f<=g"; 

199 
by (rtac subsetI 1); 

691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

200 
by (eresolve_tac (prems RL [Pi_memberD RS bexE]) 1); 
0  201 
by (etac ssubst 1); 
202 
by (resolve_tac (prems RL [ssubst]) 1); 

203 
by (REPEAT (ares_tac (prems@[apply_Pair,subsetD]) 1)); 

760  204 
qed "fun_subset"; 
0  205 

206 
val prems = goal ZF.thy 

207 
"[ f : Pi(A,B); g: Pi(A,D); \ 

208 
\ !!x. x:A ==> f`x = g`x ] ==> f=g"; 

209 
by (REPEAT (ares_tac (prems @ (prems RL [sym]) @ 

210 
[subset_refl,equalityI,fun_subset]) 1)); 

760  211 
qed "fun_extension"; 
0  212 

213 
goal ZF.thy "!!f A B. f : Pi(A,B) ==> (lam x:A. f`x) = f"; 

214 
by (rtac fun_extension 1); 

215 
by (REPEAT (ares_tac [lam_type,apply_type,beta] 1)); 

760  216 
qed "eta"; 
0  217 

218 
(*Every element of Pi(A,B) may be expressed as a lambda abstraction!*) 

219 
val prems = goal ZF.thy 

220 
"[ f: Pi(A,B); \ 

221 
\ !!b. [ ALL x:A. b(x):B(x); f = (lam x:A.b(x)) ] ==> P \ 

222 
\ ] ==> P"; 

223 
by (resolve_tac prems 1); 

224 
by (rtac (eta RS sym) 2); 

225 
by (REPEAT (ares_tac (prems@[ballI,apply_type]) 1)); 

760  226 
qed "Pi_lamE"; 
0  227 

228 

435  229 
(** Images of functions **) 
230 

231 
goalw ZF.thy [lam_def] "!!C A. C <= A ==> (lam x:A.b(x)) `` C = {b(x). x:C}"; 

232 
by (fast_tac eq_cs 1); 

760  233 
qed "image_lam"; 
435  234 

235 
goal ZF.thy "!!C A. [ f : Pi(A,B); C <= A ] ==> f``C = {f`x. x:C}"; 

437  236 
by (etac (eta RS subst) 1); 
435  237 
by (asm_full_simp_tac (FOL_ss addsimps [beta, image_lam, subset_iff] 
238 
addcongs [RepFun_cong]) 1); 

760  239 
qed "image_fun"; 
435  240 

241 

0  242 
(*** properties of "restrict" ***) 
243 

244 
goalw ZF.thy [restrict_def,lam_def] 

245 
"!!f A. [ f: Pi(C,B); A<=C ] ==> restrict(f,A) <= f"; 

246 
by (fast_tac (ZF_cs addIs [apply_Pair]) 1); 

760  247 
qed "restrict_subset"; 
0  248 

249 
val prems = goalw ZF.thy [restrict_def] 

250 
"[ !!x. x:A ==> f`x: B(x) ] ==> restrict(f,A) : Pi(A,B)"; 

251 
by (rtac lam_type 1); 

252 
by (eresolve_tac prems 1); 

760  253 
qed "restrict_type"; 
0  254 

255 
val [pi,subs] = goal ZF.thy 

256 
"[ f: Pi(C,B); A<=C ] ==> restrict(f,A) : Pi(A,B)"; 

257 
by (rtac (pi RS apply_type RS restrict_type) 1); 

258 
by (etac (subs RS subsetD) 1); 

760  259 
qed "restrict_type2"; 
0  260 

261 
goalw ZF.thy [restrict_def] "!!a A. a : A ==> restrict(f,A) ` a = f`a"; 

262 
by (etac beta 1); 

760  263 
qed "restrict"; 
0  264 

265 
(*NOT SAFE as a congruence rule for the simplifier! Can cause it to fail!*) 

266 
val prems = goalw ZF.thy [restrict_def] 

267 
"[ A=B; !!x. x:B ==> f`x=g`x ] ==> restrict(f,A) = restrict(g,B)"; 

268 
by (REPEAT (ares_tac (prems@[lam_cong]) 1)); 

760  269 
qed "restrict_eqI"; 
0  270 

691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

271 
goalw ZF.thy [restrict_def, lam_def] "domain(restrict(f,C)) = C"; 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

272 
by (fast_tac eq_cs 1); 
760  273 
qed "domain_restrict"; 
0  274 

275 
val [prem] = goalw ZF.thy [restrict_def] 

276 
"A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))"; 

277 
by (rtac (refl RS lam_cong) 1); 

129  278 
by (etac (prem RS subsetD RS beta) 1); (*easier than calling simp_tac*) 
760  279 
qed "restrict_lam_eq"; 
0  280 

281 

282 

283 
(*** Unions of functions ***) 

284 

285 
(** The Union of a set of COMPATIBLE functions is a function **) 

691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

286 

b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

287 
goalw ZF.thy [function_def] 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

288 
"!!S. [ ALL x:S. function(x); \ 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

289 
\ ALL x:S. ALL y:S. x<=y  y<=x ] ==> \ 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

290 
\ function(Union(S))"; 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

291 
by (fast_tac (ZF_cs addSDs [bspec RS bspec]) 1); 
760  292 
qed "function_Union"; 
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

293 

b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

294 
goalw ZF.thy [Pi_def] 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

295 
"!!S. [ ALL f:S. EX C D. f:C>D; \ 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

296 
\ ALL f:S. ALL y:S. f<=y  y<=f ] ==> \ 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

297 
\ Union(S) : domain(Union(S)) > range(Union(S))"; 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

298 
by (fast_tac (subset_cs addSIs [rel_Union, function_Union]) 1); 
760  299 
qed "fun_Union"; 
0  300 

301 

302 
(** The Union of 2 disjoint functions is a function **) 

303 

691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

304 
val Un_rls = [Un_subset_iff, domain_Un_eq, SUM_Un_distrib1, prod_Un_distrib2, 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

305 
Un_upper1 RSN (2, subset_trans), 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

306 
Un_upper2 RSN (2, subset_trans)]; 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

307 

b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

308 
goal ZF.thy 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

309 
"!!f. [ f: A>B; g: C>D; A Int C = 0 ] ==> \ 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

310 
\ (f Un g) : (A Un C) > (B Un D)"; 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

311 
(*Solve the product and domain subgoals using distributive laws*) 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

312 
by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff,extension]@Un_rls) 1); 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

313 
by (asm_simp_tac (FOL_ss addsimps [function_def]) 1); 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

314 
by (safe_tac ZF_cs); 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

315 
(*Solve the two cases that contradict A Int C = 0*) 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

316 
by (deepen_tac ZF_cs 2 2); 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

317 
by (deepen_tac ZF_cs 2 2); 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

318 
bw function_def; 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

319 
by (REPEAT_FIRST (dtac (spec RS spec))); 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

320 
by (deepen_tac ZF_cs 1 1); 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

321 
by (deepen_tac ZF_cs 1 1); 
760  322 
qed "fun_disjoint_Un"; 
0  323 

324 
goal ZF.thy 

325 
"!!f g a. [ a:A; f: A>B; g: C>D; A Int C = 0 ] ==> \ 

326 
\ (f Un g)`a = f`a"; 

691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

327 
by (rtac (apply_Pair RS UnI1 RS apply_equality) 1); 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

328 
by (REPEAT (ares_tac [fun_disjoint_Un] 1)); 
760  329 
qed "fun_disjoint_apply1"; 
0  330 

331 
goal ZF.thy 

332 
"!!f g c. [ c:C; f: A>B; g: C>D; A Int C = 0 ] ==> \ 

333 
\ (f Un g)`c = g`c"; 

691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

334 
by (rtac (apply_Pair RS UnI2 RS apply_equality) 1); 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

335 
by (REPEAT (ares_tac [fun_disjoint_Un] 1)); 
760  336 
qed "fun_disjoint_apply2"; 
0  337 

338 
(** Domain and range of a function/relation **) 

339 

691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

340 
goalw ZF.thy [Pi_def] "!!f. f : Pi(A,B) ==> domain(f)=A"; 
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset

341 
by (fast_tac eq_cs 1); 
760  342 
qed "domain_of_fun"; 
0  343 

517  344 
goal ZF.thy "!!f. [ f : Pi(A,B); a: A ] ==> f`a : range(f)"; 
345 
by (etac (apply_Pair RS rangeI) 1); 

346 
by (assume_tac 1); 

760  347 
qed "apply_rangeI"; 
517  348 

0  349 
val [major] = goal ZF.thy "f : Pi(A,B) ==> f : A>range(f)"; 
350 
by (rtac (major RS Pi_type) 1); 

517  351 
by (etac (major RS apply_rangeI) 1); 
760  352 
qed "range_of_fun"; 
0  353 

354 
(*** Extensions of functions ***) 

355 

519  356 
goal ZF.thy 
37  357 
"!!f A B. [ f: A>B; c~:A ] ==> cons(<c,b>,f) : cons(c,A) > cons(b,B)"; 
519  358 
by (forward_tac [single_fun RS fun_disjoint_Un] 1); 
359 
by (asm_full_simp_tac (FOL_ss addsimps [cons_eq]) 2); 

360 
by (fast_tac eq_cs 1); 

760  361 
qed "fun_extend"; 
0  362 

538  363 
goal ZF.thy 
364 
"!!f A B. [ f: A>B; c~:A; b: B ] ==> cons(<c,b>,f) : cons(c,A) > B"; 

365 
by (fast_tac (ZF_cs addEs [fun_extend RS fun_weaken_type]) 1); 

760  366 
qed "fun_extend3"; 
538  367 

37  368 
goal ZF.thy "!!f A B. [ f: A>B; a:A; c~:A ] ==> cons(<c,b>,f)`a = f`a"; 
0  369 
by (rtac (apply_Pair RS consI2 RS apply_equality) 1); 
370 
by (rtac fun_extend 3); 

371 
by (REPEAT (assume_tac 1)); 

760  372 
qed "fun_extend_apply1"; 
0  373 

37  374 
goal ZF.thy "!!f A B. [ f: A>B; c~:A ] ==> cons(<c,b>,f)`c = b"; 
0  375 
by (rtac (consI1 RS apply_equality) 1); 
376 
by (rtac fun_extend 1); 

377 
by (REPEAT (assume_tac 1)); 

760  378 
qed "fun_extend_apply2"; 
0  379 

538  380 
(*For Finite.ML. Inclusion of right into left is easy*) 
485  381 
goal ZF.thy 
382 
"!!c. c ~: A ==> cons(c,A) > B = (UN f: A>B. UN b:B. {cons(<c,b>, f)})"; 

737
436019ca97d7
cons_fun_eq: modified strange uses of classical reasoner
lcp
parents:
691
diff
changeset

383 
by (rtac equalityI 1); 
436019ca97d7
cons_fun_eq: modified strange uses of classical reasoner
lcp
parents:
691
diff
changeset

384 
by (safe_tac (ZF_cs addSEs [fun_extend3])); 
485  385 
(*Inclusion of left into right*) 
386 
by (subgoal_tac "restrict(x, A) : A > B" 1); 

387 
by (fast_tac (ZF_cs addEs [restrict_type2]) 2); 

388 
by (rtac UN_I 1 THEN assume_tac 1); 

737
436019ca97d7
cons_fun_eq: modified strange uses of classical reasoner
lcp
parents:
691
diff
changeset

389 
by (rtac (apply_funtype RS UN_I) 1 THEN REPEAT (ares_tac [consI1] 1)); 
538  390 
by (simp_tac (FOL_ss addsimps cons_iff::mem_simps) 1); 
485  391 
by (resolve_tac [fun_extension] 1 THEN REPEAT (ares_tac [fun_extend] 1)); 
392 
by (etac consE 1); 

393 
by (ALLGOALS 

394 
(asm_simp_tac (FOL_ss addsimps [restrict, fun_extend_apply1, 

538  395 
fun_extend_apply2]))); 
760  396 
qed "cons_fun_eq"; 
485  397 