author  lcp 
Thu, 30 Sep 1993 10:10:21 +0100  
changeset 14  1c0926788772 
parent 6  8ce8c4d13d4d 
child 37  cebe01deba80 
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 

43 
(*Weaking one function type to another*) 

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 

60 
(*** Function Application ***) 

61 

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

63 
by (etac PiE 1); 

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

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

66 
by (REPEAT (assume_tac 1)); 

67 
val apply_equality2 = result(); 

68 

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

70 
by (rtac the_equality 1); 

71 
by (rtac apply_equality2 2); 

72 
by (REPEAT (assume_tac 1)); 

73 
val apply_equality = result(); 

74 

75 
val prems = goal ZF.thy 

76 
"[ f: Pi(A,B); c: f; !!x. [ x:A; c = <x,f`x> ] ==> P \ 

77 
\ ] ==> P"; 

78 
by (cut_facts_tac prems 1); 

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

80 
by (REPEAT (ares_tac prems 1)); 

81 
by (hyp_subst_tac 1); 

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

83 
by (resolve_tac prems 1); 

84 
by (rtac refl 1); 

85 
val memberPiE = result(); 

86 

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

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

90 
by (REPEAT (assume_tac 1)); 

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

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

93 
by (REPEAT (assume_tac 1)); 

94 
val apply_type = result(); 

95 

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

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

97 
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

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

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

100 

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

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

104 
by (REPEAT (assume_tac 1)); 

105 
val apply_Pair = result(); 

106 

107 
val [major] = goal ZF.thy 

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

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

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

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

112 
val apply_iff = result(); 

113 

114 
(*Refining one Pi type to another*) 

115 
val prems = goal ZF.thy 

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

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

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

119 
by (etac ssubst 1); 

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

121 
val Pi_type = result(); 

122 

123 

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

125 

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

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

128 
val domain_type = result(); 

129 

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

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

132 
by (assume_tac 1); 

133 
val range_type = result(); 

134 

135 
val prems = goal ZF.thy 

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

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

138 
\ ] ==> P"; 

139 
by (cut_facts_tac prems 1); 

140 
by (resolve_tac prems 1); 

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

142 
val Pair_mem_PiE = result(); 

143 

144 
(*** Lambda Abstraction ***) 

145 

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

147 
by (etac RepFunI 1); 

148 
val lamI = result(); 

149 

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

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

152 
\ ] ==> P"; 

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

154 
by (REPEAT (ares_tac prems 1)); 

155 
val lamE = result(); 

156 

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

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

159 
val lamD = result(); 

160 

161 
val prems = goalw ZF.thy [lam_def] 

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

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

164 
val lam_type = result(); 

165 

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

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

168 
val lam_funtype = result(); 

169 

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

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

172 
val beta = result(); 

173 

174 
(*congruence rule for lambda abstraction*) 

175 
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

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

177 
by (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1); 
0  178 
val lam_cong = result(); 
179 

180 
val [major] = goal ZF.thy 

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

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

183 
by (rtac ballI 1); 

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

185 
by (assume_tac 1); 

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

187 
val lam_theI = result(); 

188 

189 

190 
(** Extensionality **) 

191 

192 
(*Semiextensionality!*) 

193 
val prems = goal ZF.thy 

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

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

196 
by (rtac subsetI 1); 

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

198 
by (etac ssubst 1); 

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

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

201 
val fun_subset = result(); 

202 

203 
val prems = goal ZF.thy 

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

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

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

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

208 
val fun_extension = result(); 

209 

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

211 
by (rtac fun_extension 1); 

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

213 
val eta = result(); 

214 

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

216 
val prems = goal ZF.thy 

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

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

219 
\ ] ==> P"; 

220 
by (resolve_tac prems 1); 

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

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

223 
val Pi_lamE = result(); 

224 

225 

226 
(*** properties of "restrict" ***) 

227 

228 
goalw ZF.thy [restrict_def,lam_def] 

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

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

231 
val restrict_subset = result(); 

232 

233 
val prems = goalw ZF.thy [restrict_def] 

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

235 
by (rtac lam_type 1); 

236 
by (eresolve_tac prems 1); 

237 
val restrict_type = result(); 

238 

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

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

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

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

243 
val restrict_type2 = result(); 

244 

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

246 
by (etac beta 1); 

247 
val restrict = result(); 

248 

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

250 
val prems = goalw ZF.thy [restrict_def] 

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

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

253 
val restrict_eqI = result(); 

254 

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

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

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

258 
val domain_restrict = result(); 

259 

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

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

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

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

263 
be (prem RS subsetD RS beta) 1; (*easier than calling simp_tac*) 
0  264 
val restrict_lam_eq = result(); 
265 

266 

267 

268 
(*** Unions of functions ***) 

269 

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

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

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

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

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

275 
val premE = ex_prem RS bspec RS exE; 

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

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

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

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

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

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

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

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

284 
by (DEPTH_SOLVE (set_mp_tac 1 

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

286 
val fun_Union = result(); 

287 

288 

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

290 

291 
val prems = goal ZF.thy 

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

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

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

295 
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

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

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

299 
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

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

301 
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

302 
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

303 
ORELSE' eresolve_tac [Pair_mem_PiE,disjoint] THEN' atac)); 
0  304 
val fun_disjoint_Un = result(); 
305 

306 
goal ZF.thy 

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

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

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

310 
fun_disjoint_Un] 1)); 

311 
val fun_disjoint_apply1 = result(); 

312 

313 
goal ZF.thy 

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

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

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

317 
fun_disjoint_Un] 1)); 

318 
val fun_disjoint_apply2 = result(); 

319 

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

321 

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

323 
by (rtac equalityI 1); 

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

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

326 
by (fast_tac ZF_cs 1); 

327 
val domain_of_fun = result(); 

328 

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

330 
by (rtac (major RS Pi_type) 1); 

331 
by (etac (major RS apply_Pair RS rangeI) 1); 

332 
val range_of_fun = result(); 

333 

334 
(*** Extensions of functions ***) 

335 

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

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

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

339 
val fun_single_lemma = result(); 

340 

341 
goalw ZF.thy [cons_def] 

342 
"!!f A B. [ f: A>B; ~c:A ] ==> cons(<c,b>,f) : cons(c,A) > cons(b,B)"; 

343 
by (rtac (fun_single_lemma RS fun_disjoint_Un) 1); 

344 
by (assume_tac 1); 

345 
by (rtac equals0I 1); 

346 
by (fast_tac ZF_cs 1); 

347 
val fun_extend = result(); 

348 

349 
goal ZF.thy "!!f A B. [ f: A>B; a:A; ~ c:A ] ==> cons(<c,b>,f)`a = f`a"; 

350 
by (rtac (apply_Pair RS consI2 RS apply_equality) 1); 

351 
by (rtac fun_extend 3); 

352 
by (REPEAT (assume_tac 1)); 

353 
val fun_extend_apply1 = result(); 

354 

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

356 
by (rtac (consI1 RS apply_equality) 1); 

357 
by (rtac fun_extend 1); 

358 
by (REPEAT (assume_tac 1)); 

359 
val fun_extend_apply2 = result(); 

360 

361 
(*The empty function*) 

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

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

364 
val fun_empty = result(); 

365 

366 
(*The singleton function*) 

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

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

369 
val fun_single = result(); 

370 