author  lcp 
Fri, 12 Aug 1994 18:45:33 +0200  
changeset 517  a9f93400f307 
parent 485  5e00a676a211 
child 519  98b88551e102 
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 

11 
val prems = goalw ZF.thy [Pi_def] 

12 
"[ f <= Sigma(A,B); !!x. x:A ==> EX! y. <x,y>: f ] ==> \ 

13 
\ f: Pi(A,B)"; 

14 
by (REPEAT (ares_tac (prems @ [CollectI,PowI,ballI,impI]) 1)); 

15 
val PiI = result(); 

16 

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

18 

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

20 
by (rtac (major RS CollectE) 1); 

21 
by (etac PowD 1); 

22 
val fun_is_rel = result(); 

23 

24 
val major::prems = goalw ZF.thy [Pi_def] 

25 
"[ f: Pi(A,B); a:A ] ==> EX! y. <a,y>: f"; 

26 
by (rtac (major RS CollectE) 1); 

27 
by (etac bspec 1); 

28 
by (resolve_tac prems 1); 

29 
val fun_unique_Pair = result(); 

30 

31 
val prems = goal ZF.thy 

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

33 
\ [ f <= Sigma(A,B); ALL x:A. EX! y. <x,y>: f ] ==> P \ 

34 
\ ] ==> P"; 

35 
by (REPEAT (ares_tac (prems@[ballI,fun_is_rel,fun_unique_Pair]) 1)); 

36 
val PiE = result(); 

37 

38 
val prems = goalw ZF.thy [Pi_def] 

39 
"[ 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

40 
by (simp_tac (FOL_ss addsimps prems addcongs [Sigma_cong]) 1); 
0  41 
val Pi_cong = result(); 
42 

485  43 
(*Weakening one function type to another; see also Pi_type*) 
0  44 
goalw ZF.thy [Pi_def] "!!f. [ f: A>B; B<=D ] ==> f: A>D"; 
45 
by (safe_tac ZF_cs); 

46 
by (set_mp_tac 1); 

47 
by (fast_tac ZF_cs 1); 

48 
val fun_weaken_type = result(); 

49 

50 
(*Empty function spaces*) 

51 
goalw ZF.thy [Pi_def] "Pi(0,A) = {0}"; 

52 
by (fast_tac (ZF_cs addIs [equalityI]) 1); 

53 
val Pi_empty1 = result(); 

54 

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

56 
by (fast_tac (ZF_cs addIs [equalityI]) 1); 

57 
val Pi_empty2 = result(); 

58 

59 
(*** Function Application ***) 

60 

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

62 
by (etac PiE 1); 

63 
by (etac (bspec RS ex1_equalsE) 1); 

64 
by (etac (subsetD RS SigmaD1) 1); 

65 
by (REPEAT (assume_tac 1)); 

66 
val apply_equality2 = result(); 

67 

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

69 
by (rtac the_equality 1); 

70 
by (rtac apply_equality2 2); 

71 
by (REPEAT (assume_tac 1)); 

72 
val apply_equality = result(); 

73 

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

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

77 
by (rtac the_0 1); 

78 
by (fast_tac ZF_cs 1); 

79 
val apply_0 = result(); 

80 

0  81 
val prems = goal ZF.thy 
82 
"[ f: Pi(A,B); c: f; !!x. [ x:A; c = <x,f`x> ] ==> P \ 

83 
\ ] ==> P"; 

84 
by (cut_facts_tac prems 1); 

85 
by (etac (fun_is_rel RS subsetD RS SigmaE) 1); 

86 
by (REPEAT (ares_tac prems 1)); 

87 
by (hyp_subst_tac 1); 

88 
by (etac (apply_equality RS ssubst) 1); 

89 
by (resolve_tac prems 1); 

90 
by (rtac refl 1); 

91 
val memberPiE = result(); 

92 

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

93 
(*Conclusion is flexible  use res_inst_tac or else apply_funtype below!*) 
0  94 
goal ZF.thy "!!f. [ f: Pi(A,B); a:A ] ==> f`a : B(a)"; 
95 
by (rtac (fun_unique_Pair RS ex1E) 1); 

96 
by (REPEAT (assume_tac 1)); 

97 
by (rtac (fun_is_rel RS subsetD RS SigmaE2) 1); 

98 
by (etac (apply_equality RS ssubst) 3); 

99 
by (REPEAT (assume_tac 1)); 

100 
val apply_type = result(); 

101 

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

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

103 
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

104 
by (REPEAT (ares_tac [apply_type] 1)); 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

105 
val apply_funtype = result(); 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

106 

0  107 
goal ZF.thy "!!f. [ f: Pi(A,B); a:A ] ==> <a,f`a>: f"; 
108 
by (rtac (fun_unique_Pair RS ex1E) 1); 

109 
by (resolve_tac [apply_equality RS ssubst] 3); 

110 
by (REPEAT (assume_tac 1)); 

111 
val apply_Pair = result(); 

112 

113 
val [major] = goal ZF.thy 

114 
"f: Pi(A,B) ==> <a,b>: f <> a:A & f`a = b"; 

115 
by (rtac (major RS PiE) 1); 

116 
by (fast_tac (ZF_cs addSIs [major RS apply_Pair, 

117 
major RSN (2,apply_equality)]) 1); 

118 
val apply_iff = result(); 

119 

120 
(*Refining one Pi type to another*) 

121 
val prems = goal ZF.thy 

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

123 
by (rtac (subsetI RS PiI) 1); 

124 
by (eresolve_tac (prems RL [memberPiE]) 1); 

125 
by (etac ssubst 1); 

126 
by (REPEAT (ares_tac (prems@[SigmaI,fun_unique_Pair]) 1)); 

127 
val Pi_type = result(); 

128 

129 

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

131 

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

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

134 
val domain_type = result(); 

135 

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

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

138 
by (assume_tac 1); 

139 
val range_type = result(); 

140 

141 
val prems = goal ZF.thy 

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

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

144 
\ ] ==> P"; 

145 
by (cut_facts_tac prems 1); 

146 
by (resolve_tac prems 1); 

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

148 
val Pair_mem_PiE = result(); 

149 

150 
(*** Lambda Abstraction ***) 

151 

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

153 
by (etac RepFunI 1); 

154 
val lamI = result(); 

155 

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

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

158 
\ ] ==> P"; 

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

160 
by (REPEAT (ares_tac prems 1)); 

161 
val lamE = result(); 

162 

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

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

165 
val lamD = result(); 

166 

167 
val prems = goalw ZF.thy [lam_def] 

168 
"[ !!x. x:A ==> b(x): B(x) ] ==> (lam x:A.b(x)) : Pi(A,B)"; 

169 
by (fast_tac (ZF_cs addIs (PiI::prems)) 1); 

170 
val lam_type = result(); 

171 

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

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

174 
val lam_funtype = result(); 

175 

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

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

178 
val beta = result(); 

179 

180 
(*congruence rule for lambda abstraction*) 

181 
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

182 
"[ 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

183 
by (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1); 
0  184 
val lam_cong = result(); 
185 

186 
val [major] = goal ZF.thy 

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

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

189 
by (rtac ballI 1); 

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

191 
by (assume_tac 1); 

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

193 
val lam_theI = result(); 

194 

195 

196 
(** Extensionality **) 

197 

198 
(*Semiextensionality!*) 

199 
val prems = goal ZF.thy 

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

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

202 
by (rtac subsetI 1); 

203 
by (eresolve_tac (prems RL [memberPiE]) 1); 

204 
by (etac ssubst 1); 

205 
by (resolve_tac (prems RL [ssubst]) 1); 

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

207 
val fun_subset = result(); 

208 

209 
val prems = goal ZF.thy 

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

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

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

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

214 
val fun_extension = result(); 

215 

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

217 
by (rtac fun_extension 1); 

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

219 
val eta = result(); 

220 

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

222 
val prems = goal ZF.thy 

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

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

225 
\ ] ==> P"; 

226 
by (resolve_tac prems 1); 

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

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

229 
val Pi_lamE = result(); 

230 

231 

435  232 
(** Images of functions **) 
233 

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

235 
by (fast_tac eq_cs 1); 

236 
val image_lam = result(); 

237 

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

437  239 
by (etac (eta RS subst) 1); 
435  240 
by (asm_full_simp_tac (FOL_ss addsimps [beta, image_lam, subset_iff] 
241 
addcongs [RepFun_cong]) 1); 

242 
val image_fun = result(); 

243 

244 

0  245 
(*** properties of "restrict" ***) 
246 

247 
goalw ZF.thy [restrict_def,lam_def] 

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

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

250 
val restrict_subset = result(); 

251 

252 
val prems = goalw ZF.thy [restrict_def] 

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

254 
by (rtac lam_type 1); 

255 
by (eresolve_tac prems 1); 

256 
val restrict_type = result(); 

257 

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

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

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

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

262 
val restrict_type2 = result(); 

263 

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

265 
by (etac beta 1); 

266 
val restrict = result(); 

267 

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

269 
val prems = goalw ZF.thy [restrict_def] 

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

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

272 
val restrict_eqI = result(); 

273 

274 
goalw ZF.thy [restrict_def] "domain(restrict(f,C)) = C"; 

275 
by (REPEAT (ares_tac [equalityI,subsetI,domainI,lamI] 1 

276 
ORELSE eresolve_tac [domainE,lamE,Pair_inject,ssubst] 1)); 

277 
val domain_restrict = result(); 

278 

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

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

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

129  282 
by (etac (prem RS subsetD RS beta) 1); (*easier than calling simp_tac*) 
0  283 
val restrict_lam_eq = result(); 
284 

285 

286 

287 
(*** Unions of functions ***) 

288 

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

290 
val [ex_prem,disj_prem] = goal ZF.thy 

291 
"[ ALL x:S. EX C D. x:C>D; \ 

292 
\ !!x y. [ x:S; y:S ] ==> x<=y  y<=x ] ==> \ 

293 
\ Union(S) : domain(Union(S)) > range(Union(S))"; 

294 
val premE = ex_prem RS bspec RS exE; 

295 
by (REPEAT (eresolve_tac [exE,PiE,premE] 1 

296 
ORELSE ares_tac [PiI, ballI RS rel_Union, exI] 1)); 

297 
by (REPEAT (eresolve_tac [asm_rl,domainE,UnionE,exE] 1 

298 
ORELSE ares_tac [allI,impI,ex1I,UnionI] 1)); 

299 
by (res_inst_tac [ ("x1","B") ] premE 1); 

300 
by (res_inst_tac [ ("x1","Ba") ] premE 2); 

301 
by (REPEAT (eresolve_tac [asm_rl,exE] 1)); 

302 
by (eresolve_tac [disj_prem RS disjE] 1); 

303 
by (DEPTH_SOLVE (set_mp_tac 1 

304 
ORELSE eresolve_tac [asm_rl, apply_equality2] 1)); 

305 
val fun_Union = result(); 

306 

307 

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

309 

310 
val prems = goal ZF.thy 

311 
"[ f: A>B; g: C>D; A Int C = 0 ] ==> \ 

312 
\ (f Un g) : (A Un C) > (B Un D)"; 

313 
(*Contradiction if A Int C = 0, a:A, a:B*) 

314 
val [disjoint] = prems RL ([IntI] RLN (2, [equals0D])); 

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

315 
val Pair_UnE = read_instantiate [("c","<?a,?b>")] UnE; (* ignores x: A Un C *) 
0  316 
by (cut_facts_tac prems 1); 
317 
by (rtac PiI 1); 

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

318 
by (REPEAT (ares_tac [rel_Un, fun_is_rel] 1)); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

319 
by (rtac ex_ex1I 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

320 
by (fast_tac (ZF_cs addDs [apply_Pair]) 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

321 
by (REPEAT_FIRST (eresolve_tac [asm_rl, Pair_UnE, sym RS trans] 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

322 
ORELSE' eresolve_tac [Pair_mem_PiE,disjoint] THEN' atac)); 
0  323 
val fun_disjoint_Un = result(); 
324 

325 
goal ZF.thy 

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

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

328 
by (REPEAT (ares_tac [apply_equality,UnI1,apply_Pair, 

329 
fun_disjoint_Un] 1)); 

330 
val fun_disjoint_apply1 = result(); 

331 

332 
goal ZF.thy 

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

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

335 
by (REPEAT (ares_tac [apply_equality,UnI2,apply_Pair, 

336 
fun_disjoint_Un] 1)); 

337 
val fun_disjoint_apply2 = result(); 

338 

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

340 

341 
val [major] = goal ZF.thy "f : Pi(A,B) ==> domain(f)=A"; 

342 
by (rtac equalityI 1); 

343 
by (fast_tac (ZF_cs addIs [major RS apply_Pair]) 2); 

344 
by (rtac (major RS PiE) 1); 

345 
by (fast_tac ZF_cs 1); 

346 
val domain_of_fun = result(); 

347 

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

350 
by (assume_tac 1); 

351 
val apply_rangeI = result(); 

352 

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

517  355 
by (etac (major RS apply_rangeI) 1); 
0  356 
val range_of_fun = result(); 
357 

358 
(*** Extensions of functions ***) 

359 

360 
(*Singleton function  in the underlying form of singletons*) 

361 
goal ZF.thy "Upair(<a,b>,<a,b>) : Upair(a,a) > Upair(b,b)"; 

362 
by (fast_tac (ZF_cs addIs [PiI]) 1); 

363 
val fun_single_lemma = result(); 

364 

365 
goalw ZF.thy [cons_def] 

37  366 
"!!f A B. [ f: A>B; c~:A ] ==> cons(<c,b>,f) : cons(c,A) > cons(b,B)"; 
0  367 
by (rtac (fun_single_lemma RS fun_disjoint_Un) 1); 
368 
by (assume_tac 1); 

369 
by (rtac equals0I 1); 

370 
by (fast_tac ZF_cs 1); 

371 
val fun_extend = result(); 

372 

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

376 
by (REPEAT (assume_tac 1)); 

377 
val fun_extend_apply1 = result(); 

378 

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

382 
by (REPEAT (assume_tac 1)); 

383 
val fun_extend_apply2 = result(); 

384 

385 
(*The empty function*) 

386 
goal ZF.thy "0: 0>A"; 

387 
by (fast_tac (ZF_cs addIs [PiI]) 1); 

388 
val fun_empty = result(); 

389 

390 
(*The singleton function*) 

391 
goal ZF.thy "{<a,b>} : {a} > cons(b,C)"; 

392 
by (REPEAT (ares_tac [fun_extend,fun_empty,notI] 1 ORELSE etac emptyE 1)); 

393 
val fun_single = result(); 

394 

485  395 
goal ZF.thy 
396 
"!!c. c ~: A ==> cons(c,A) > B = (UN f: A>B. UN b:B. {cons(<c,b>, f)})"; 

397 
by (safe_tac eq_cs); 

398 
(*Inclusion of right into left is easy*) 

399 
by (fast_tac (ZF_cs addEs [fun_extend RS fun_weaken_type]) 2); 

400 
(*Inclusion of left into right*) 

401 
by (subgoal_tac "restrict(x, A) : A > B" 1); 

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

403 
by (rtac UN_I 1 THEN assume_tac 1); 

404 
by (rtac UN_I 1 THEN fast_tac (ZF_cs addEs [apply_type]) 1); 

405 
by (subgoal_tac "x = cons(<c, x ` c>, restrict(x, A))" 1); 

406 
by (fast_tac ZF_cs 1); 

407 
(*Proving the lemma*) 

408 
by (resolve_tac [fun_extension] 1 THEN REPEAT (ares_tac [fun_extend] 1)); 

409 
by (etac consE 1); 

410 
by (ALLGOALS 

411 
(asm_simp_tac (FOL_ss addsimps [restrict, fun_extend_apply1, 

412 
fun_extend_apply2]))); 

413 
val cons_fun_eq = result(); 

414 