author | lcp |
Wed, 17 Aug 1994 10:33:23 +0200 | |
changeset 538 | b4fe3da03449 |
parent 519 | 98b88551e102 |
child 691 | b9fc536792bb |
permissions | -rw-r--r-- |
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 Zermelo-Fraenkel 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}"; |
|
519 | 52 |
by (fast_tac eq_cs 1); |
0 | 53 |
val Pi_empty1 = result(); |
54 |
||
55 |
goalw ZF.thy [Pi_def] "!!A a. a:A ==> A->0 = 0"; |
|
519 | 56 |
by (fast_tac eq_cs 1); |
0 | 57 |
val Pi_empty2 = result(); |
58 |
||
519 | 59 |
(*The empty function*) |
60 |
goal ZF.thy "0: 0->A"; |
|
61 |
by (fast_tac (ZF_cs addIs [PiI]) 1); |
|
62 |
val empty_fun = result(); |
|
63 |
||
64 |
(*The singleton function*) |
|
65 |
goalw ZF.thy [Pi_def] "{<a,b>} : {a} -> {b}"; |
|
66 |
by (fast_tac eq_cs 1); |
|
67 |
val single_fun = result(); |
|
68 |
||
0 | 69 |
(*** Function Application ***) |
70 |
||
71 |
goal ZF.thy "!!a b f. [| <a,b>: f; <a,c>: f; f: Pi(A,B) |] ==> b=c"; |
|
72 |
by (etac PiE 1); |
|
73 |
by (etac (bspec RS ex1_equalsE) 1); |
|
74 |
by (etac (subsetD RS SigmaD1) 1); |
|
75 |
by (REPEAT (assume_tac 1)); |
|
76 |
val apply_equality2 = result(); |
|
77 |
||
78 |
goalw ZF.thy [apply_def] "!!a b f. [| <a,b>: f; f: Pi(A,B) |] ==> f`a = b"; |
|
79 |
by (rtac the_equality 1); |
|
80 |
by (rtac apply_equality2 2); |
|
81 |
by (REPEAT (assume_tac 1)); |
|
82 |
val apply_equality = result(); |
|
83 |
||
517 | 84 |
(*Applying a function outside its domain yields 0*) |
85 |
goalw ZF.thy [apply_def] |
|
86 |
"!!a b f. [| a ~: domain(f); f: Pi(A,B) |] ==> f`a = 0"; |
|
87 |
by (rtac the_0 1); |
|
88 |
by (fast_tac ZF_cs 1); |
|
89 |
val apply_0 = result(); |
|
90 |
||
0 | 91 |
val prems = goal ZF.thy |
92 |
"[| f: Pi(A,B); c: f; !!x. [| x:A; c = <x,f`x> |] ==> P \ |
|
93 |
\ |] ==> P"; |
|
94 |
by (cut_facts_tac prems 1); |
|
95 |
by (etac (fun_is_rel RS subsetD RS SigmaE) 1); |
|
96 |
by (REPEAT (ares_tac prems 1)); |
|
97 |
by (hyp_subst_tac 1); |
|
98 |
by (etac (apply_equality RS ssubst) 1); |
|
99 |
by (resolve_tac prems 1); |
|
100 |
by (rtac refl 1); |
|
101 |
val memberPiE = result(); |
|
102 |
||
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
103 |
(*Conclusion is flexible -- use res_inst_tac or else apply_funtype below!*) |
0 | 104 |
goal ZF.thy "!!f. [| f: Pi(A,B); a:A |] ==> f`a : B(a)"; |
105 |
by (rtac (fun_unique_Pair RS ex1E) 1); |
|
106 |
by (REPEAT (assume_tac 1)); |
|
107 |
by (rtac (fun_is_rel RS subsetD RS SigmaE2) 1); |
|
108 |
by (etac (apply_equality RS ssubst) 3); |
|
109 |
by (REPEAT (assume_tac 1)); |
|
110 |
val apply_type = result(); |
|
111 |
||
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
112 |
(*This version is acceptable to the simplifier*) |
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
113 |
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
|
114 |
by (REPEAT (ares_tac [apply_type] 1)); |
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
115 |
val apply_funtype = result(); |
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
116 |
|
0 | 117 |
goal ZF.thy "!!f. [| f: Pi(A,B); a:A |] ==> <a,f`a>: f"; |
118 |
by (rtac (fun_unique_Pair RS ex1E) 1); |
|
119 |
by (resolve_tac [apply_equality RS ssubst] 3); |
|
120 |
by (REPEAT (assume_tac 1)); |
|
121 |
val apply_Pair = result(); |
|
122 |
||
123 |
val [major] = goal ZF.thy |
|
124 |
"f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b"; |
|
125 |
by (rtac (major RS PiE) 1); |
|
126 |
by (fast_tac (ZF_cs addSIs [major RS apply_Pair, |
|
127 |
major RSN (2,apply_equality)]) 1); |
|
128 |
val apply_iff = result(); |
|
129 |
||
130 |
(*Refining one Pi type to another*) |
|
131 |
val prems = goal ZF.thy |
|
132 |
"[| f: Pi(A,C); !!x. x:A ==> f`x : B(x) |] ==> f : Pi(A,B)"; |
|
133 |
by (rtac (subsetI RS PiI) 1); |
|
134 |
by (eresolve_tac (prems RL [memberPiE]) 1); |
|
135 |
by (etac ssubst 1); |
|
136 |
by (REPEAT (ares_tac (prems@[SigmaI,fun_unique_Pair]) 1)); |
|
137 |
val Pi_type = result(); |
|
138 |
||
139 |
||
140 |
(** Elimination of membership in a function **) |
|
141 |
||
142 |
goal ZF.thy "!!a A. [| <a,b> : f; f: Pi(A,B) |] ==> a : A"; |
|
143 |
by (REPEAT (ares_tac [fun_is_rel RS subsetD RS SigmaD1] 1)); |
|
144 |
val domain_type = result(); |
|
145 |
||
146 |
goal ZF.thy "!!b B a. [| <a,b> : f; f: Pi(A,B) |] ==> b : B(a)"; |
|
147 |
by (etac (fun_is_rel RS subsetD RS SigmaD2) 1); |
|
148 |
by (assume_tac 1); |
|
149 |
val range_type = result(); |
|
150 |
||
151 |
val prems = goal ZF.thy |
|
152 |
"[| <a,b>: f; f: Pi(A,B); \ |
|
153 |
\ [| a:A; b:B(a); f`a = b |] ==> P \ |
|
154 |
\ |] ==> P"; |
|
155 |
by (cut_facts_tac prems 1); |
|
156 |
by (resolve_tac prems 1); |
|
157 |
by (REPEAT (eresolve_tac [asm_rl,domain_type,range_type,apply_equality] 1)); |
|
158 |
val Pair_mem_PiE = result(); |
|
159 |
||
160 |
(*** Lambda Abstraction ***) |
|
161 |
||
162 |
goalw ZF.thy [lam_def] "!!A b. a:A ==> <a,b(a)> : (lam x:A. b(x))"; |
|
163 |
by (etac RepFunI 1); |
|
164 |
val lamI = result(); |
|
165 |
||
166 |
val major::prems = goalw ZF.thy [lam_def] |
|
167 |
"[| p: (lam x:A. b(x)); !!x.[| x:A; p=<x,b(x)> |] ==> P \ |
|
168 |
\ |] ==> P"; |
|
169 |
by (rtac (major RS RepFunE) 1); |
|
170 |
by (REPEAT (ares_tac prems 1)); |
|
171 |
val lamE = result(); |
|
172 |
||
173 |
goal ZF.thy "!!a b c. [| <a,c>: (lam x:A. b(x)) |] ==> c = b(a)"; |
|
174 |
by (REPEAT (eresolve_tac [asm_rl,lamE,Pair_inject,ssubst] 1)); |
|
175 |
val lamD = result(); |
|
176 |
||
177 |
val prems = goalw ZF.thy [lam_def] |
|
178 |
"[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A.b(x)) : Pi(A,B)"; |
|
179 |
by (fast_tac (ZF_cs addIs (PiI::prems)) 1); |
|
180 |
val lam_type = result(); |
|
181 |
||
182 |
goal ZF.thy "(lam x:A.b(x)) : A -> {b(x). x:A}"; |
|
183 |
by (REPEAT (ares_tac [refl,lam_type,RepFunI] 1)); |
|
184 |
val lam_funtype = result(); |
|
185 |
||
186 |
goal ZF.thy "!!a A. a : A ==> (lam x:A.b(x)) ` a = b(a)"; |
|
187 |
by (REPEAT (ares_tac [apply_equality,lam_funtype,lamI] 1)); |
|
188 |
val beta = result(); |
|
189 |
||
190 |
(*congruence rule for lambda abstraction*) |
|
191 |
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
|
192 |
"[| 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
|
193 |
by (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1); |
0 | 194 |
val lam_cong = result(); |
195 |
||
196 |
val [major] = goal ZF.thy |
|
197 |
"(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)"; |
|
198 |
by (res_inst_tac [("x", "lam x: A. THE y. Q(x,y)")] exI 1); |
|
199 |
by (rtac ballI 1); |
|
200 |
by (rtac (beta RS ssubst) 1); |
|
201 |
by (assume_tac 1); |
|
202 |
by (etac (major RS theI) 1); |
|
203 |
val lam_theI = result(); |
|
204 |
||
205 |
||
206 |
(** Extensionality **) |
|
207 |
||
208 |
(*Semi-extensionality!*) |
|
209 |
val prems = goal ZF.thy |
|
210 |
"[| f : Pi(A,B); g: Pi(C,D); A<=C; \ |
|
211 |
\ !!x. x:A ==> f`x = g`x |] ==> f<=g"; |
|
212 |
by (rtac subsetI 1); |
|
213 |
by (eresolve_tac (prems RL [memberPiE]) 1); |
|
214 |
by (etac ssubst 1); |
|
215 |
by (resolve_tac (prems RL [ssubst]) 1); |
|
216 |
by (REPEAT (ares_tac (prems@[apply_Pair,subsetD]) 1)); |
|
217 |
val fun_subset = result(); |
|
218 |
||
219 |
val prems = goal ZF.thy |
|
220 |
"[| f : Pi(A,B); g: Pi(A,D); \ |
|
221 |
\ !!x. x:A ==> f`x = g`x |] ==> f=g"; |
|
222 |
by (REPEAT (ares_tac (prems @ (prems RL [sym]) @ |
|
223 |
[subset_refl,equalityI,fun_subset]) 1)); |
|
224 |
val fun_extension = result(); |
|
225 |
||
226 |
goal ZF.thy "!!f A B. f : Pi(A,B) ==> (lam x:A. f`x) = f"; |
|
227 |
by (rtac fun_extension 1); |
|
228 |
by (REPEAT (ares_tac [lam_type,apply_type,beta] 1)); |
|
229 |
val eta = result(); |
|
230 |
||
231 |
(*Every element of Pi(A,B) may be expressed as a lambda abstraction!*) |
|
232 |
val prems = goal ZF.thy |
|
233 |
"[| f: Pi(A,B); \ |
|
234 |
\ !!b. [| ALL x:A. b(x):B(x); f = (lam x:A.b(x)) |] ==> P \ |
|
235 |
\ |] ==> P"; |
|
236 |
by (resolve_tac prems 1); |
|
237 |
by (rtac (eta RS sym) 2); |
|
238 |
by (REPEAT (ares_tac (prems@[ballI,apply_type]) 1)); |
|
239 |
val Pi_lamE = result(); |
|
240 |
||
241 |
||
435 | 242 |
(** Images of functions **) |
243 |
||
244 |
goalw ZF.thy [lam_def] "!!C A. C <= A ==> (lam x:A.b(x)) `` C = {b(x). x:C}"; |
|
245 |
by (fast_tac eq_cs 1); |
|
246 |
val image_lam = result(); |
|
247 |
||
248 |
goal ZF.thy "!!C A. [| f : Pi(A,B); C <= A |] ==> f``C = {f`x. x:C}"; |
|
437 | 249 |
by (etac (eta RS subst) 1); |
435 | 250 |
by (asm_full_simp_tac (FOL_ss addsimps [beta, image_lam, subset_iff] |
251 |
addcongs [RepFun_cong]) 1); |
|
252 |
val image_fun = result(); |
|
253 |
||
254 |
||
0 | 255 |
(*** properties of "restrict" ***) |
256 |
||
257 |
goalw ZF.thy [restrict_def,lam_def] |
|
258 |
"!!f A. [| f: Pi(C,B); A<=C |] ==> restrict(f,A) <= f"; |
|
259 |
by (fast_tac (ZF_cs addIs [apply_Pair]) 1); |
|
260 |
val restrict_subset = result(); |
|
261 |
||
262 |
val prems = goalw ZF.thy [restrict_def] |
|
263 |
"[| !!x. x:A ==> f`x: B(x) |] ==> restrict(f,A) : Pi(A,B)"; |
|
264 |
by (rtac lam_type 1); |
|
265 |
by (eresolve_tac prems 1); |
|
266 |
val restrict_type = result(); |
|
267 |
||
268 |
val [pi,subs] = goal ZF.thy |
|
269 |
"[| f: Pi(C,B); A<=C |] ==> restrict(f,A) : Pi(A,B)"; |
|
270 |
by (rtac (pi RS apply_type RS restrict_type) 1); |
|
271 |
by (etac (subs RS subsetD) 1); |
|
272 |
val restrict_type2 = result(); |
|
273 |
||
274 |
goalw ZF.thy [restrict_def] "!!a A. a : A ==> restrict(f,A) ` a = f`a"; |
|
275 |
by (etac beta 1); |
|
276 |
val restrict = result(); |
|
277 |
||
278 |
(*NOT SAFE as a congruence rule for the simplifier! Can cause it to fail!*) |
|
279 |
val prems = goalw ZF.thy [restrict_def] |
|
280 |
"[| A=B; !!x. x:B ==> f`x=g`x |] ==> restrict(f,A) = restrict(g,B)"; |
|
281 |
by (REPEAT (ares_tac (prems@[lam_cong]) 1)); |
|
282 |
val restrict_eqI = result(); |
|
283 |
||
284 |
goalw ZF.thy [restrict_def] "domain(restrict(f,C)) = C"; |
|
285 |
by (REPEAT (ares_tac [equalityI,subsetI,domainI,lamI] 1 |
|
286 |
ORELSE eresolve_tac [domainE,lamE,Pair_inject,ssubst] 1)); |
|
287 |
val domain_restrict = result(); |
|
288 |
||
289 |
val [prem] = goalw ZF.thy [restrict_def] |
|
290 |
"A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))"; |
|
291 |
by (rtac (refl RS lam_cong) 1); |
|
129 | 292 |
by (etac (prem RS subsetD RS beta) 1); (*easier than calling simp_tac*) |
0 | 293 |
val restrict_lam_eq = result(); |
294 |
||
295 |
||
296 |
||
297 |
(*** Unions of functions ***) |
|
298 |
||
299 |
(** The Union of a set of COMPATIBLE functions is a function **) |
|
300 |
val [ex_prem,disj_prem] = goal ZF.thy |
|
301 |
"[| ALL x:S. EX C D. x:C->D; \ |
|
302 |
\ !!x y. [| x:S; y:S |] ==> x<=y | y<=x |] ==> \ |
|
303 |
\ Union(S) : domain(Union(S)) -> range(Union(S))"; |
|
304 |
val premE = ex_prem RS bspec RS exE; |
|
305 |
by (REPEAT (eresolve_tac [exE,PiE,premE] 1 |
|
306 |
ORELSE ares_tac [PiI, ballI RS rel_Union, exI] 1)); |
|
307 |
by (REPEAT (eresolve_tac [asm_rl,domainE,UnionE,exE] 1 |
|
308 |
ORELSE ares_tac [allI,impI,ex1I,UnionI] 1)); |
|
309 |
by (res_inst_tac [ ("x1","B") ] premE 1); |
|
310 |
by (res_inst_tac [ ("x1","Ba") ] premE 2); |
|
311 |
by (REPEAT (eresolve_tac [asm_rl,exE] 1)); |
|
312 |
by (eresolve_tac [disj_prem RS disjE] 1); |
|
313 |
by (DEPTH_SOLVE (set_mp_tac 1 |
|
314 |
ORELSE eresolve_tac [asm_rl, apply_equality2] 1)); |
|
315 |
val fun_Union = result(); |
|
316 |
||
317 |
||
318 |
(** The Union of 2 disjoint functions is a function **) |
|
319 |
||
320 |
val prems = goal ZF.thy |
|
321 |
"[| f: A->B; g: C->D; A Int C = 0 |] ==> \ |
|
322 |
\ (f Un g) : (A Un C) -> (B Un D)"; |
|
323 |
(*Contradiction if A Int C = 0, a:A, a:B*) |
|
324 |
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
|
325 |
val Pair_UnE = read_instantiate [("c","<?a,?b>")] UnE; (* ignores x: A Un C *) |
0 | 326 |
by (cut_facts_tac prems 1); |
327 |
by (rtac PiI 1); |
|
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
328 |
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
|
329 |
by (rtac ex_ex1I 1); |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
330 |
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
|
331 |
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
|
332 |
ORELSE' eresolve_tac [Pair_mem_PiE,disjoint] THEN' atac)); |
0 | 333 |
val fun_disjoint_Un = result(); |
334 |
||
335 |
goal ZF.thy |
|
336 |
"!!f g a. [| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \ |
|
337 |
\ (f Un g)`a = f`a"; |
|
338 |
by (REPEAT (ares_tac [apply_equality,UnI1,apply_Pair, |
|
339 |
fun_disjoint_Un] 1)); |
|
340 |
val fun_disjoint_apply1 = result(); |
|
341 |
||
342 |
goal ZF.thy |
|
343 |
"!!f g c. [| c:C; f: A->B; g: C->D; A Int C = 0 |] ==> \ |
|
344 |
\ (f Un g)`c = g`c"; |
|
345 |
by (REPEAT (ares_tac [apply_equality,UnI2,apply_Pair, |
|
346 |
fun_disjoint_Un] 1)); |
|
347 |
val fun_disjoint_apply2 = result(); |
|
348 |
||
349 |
(** Domain and range of a function/relation **) |
|
350 |
||
351 |
val [major] = goal ZF.thy "f : Pi(A,B) ==> domain(f)=A"; |
|
352 |
by (rtac equalityI 1); |
|
353 |
by (fast_tac (ZF_cs addIs [major RS apply_Pair]) 2); |
|
354 |
by (rtac (major RS PiE) 1); |
|
355 |
by (fast_tac ZF_cs 1); |
|
356 |
val domain_of_fun = result(); |
|
357 |
||
517 | 358 |
goal ZF.thy "!!f. [| f : Pi(A,B); a: A |] ==> f`a : range(f)"; |
359 |
by (etac (apply_Pair RS rangeI) 1); |
|
360 |
by (assume_tac 1); |
|
361 |
val apply_rangeI = result(); |
|
362 |
||
0 | 363 |
val [major] = goal ZF.thy "f : Pi(A,B) ==> f : A->range(f)"; |
364 |
by (rtac (major RS Pi_type) 1); |
|
517 | 365 |
by (etac (major RS apply_rangeI) 1); |
0 | 366 |
val range_of_fun = result(); |
367 |
||
368 |
(*** Extensions of functions ***) |
|
369 |
||
519 | 370 |
goal ZF.thy |
37 | 371 |
"!!f A B. [| f: A->B; c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)"; |
519 | 372 |
by (forward_tac [single_fun RS fun_disjoint_Un] 1); |
373 |
by (asm_full_simp_tac (FOL_ss addsimps [cons_eq]) 2); |
|
374 |
by (fast_tac eq_cs 1); |
|
0 | 375 |
val fun_extend = result(); |
376 |
||
538 | 377 |
goal ZF.thy |
378 |
"!!f A B. [| f: A->B; c~:A; b: B |] ==> cons(<c,b>,f) : cons(c,A) -> B"; |
|
379 |
by (fast_tac (ZF_cs addEs [fun_extend RS fun_weaken_type]) 1); |
|
380 |
val fun_extend3 = result(); |
|
381 |
||
37 | 382 |
goal ZF.thy "!!f A B. [| f: A->B; a:A; c~:A |] ==> cons(<c,b>,f)`a = f`a"; |
0 | 383 |
by (rtac (apply_Pair RS consI2 RS apply_equality) 1); |
384 |
by (rtac fun_extend 3); |
|
385 |
by (REPEAT (assume_tac 1)); |
|
386 |
val fun_extend_apply1 = result(); |
|
387 |
||
37 | 388 |
goal ZF.thy "!!f A B. [| f: A->B; c~:A |] ==> cons(<c,b>,f)`c = b"; |
0 | 389 |
by (rtac (consI1 RS apply_equality) 1); |
390 |
by (rtac fun_extend 1); |
|
391 |
by (REPEAT (assume_tac 1)); |
|
392 |
val fun_extend_apply2 = result(); |
|
393 |
||
538 | 394 |
(*For Finite.ML. Inclusion of right into left is easy*) |
485 | 395 |
goal ZF.thy |
396 |
"!!c. c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})"; |
|
538 | 397 |
by (safe_tac (eq_cs addSEs [fun_extend3])); |
485 | 398 |
(*Inclusion of left into right*) |
399 |
by (subgoal_tac "restrict(x, A) : A -> B" 1); |
|
400 |
by (fast_tac (ZF_cs addEs [restrict_type2]) 2); |
|
401 |
by (rtac UN_I 1 THEN assume_tac 1); |
|
402 |
by (rtac UN_I 1 THEN fast_tac (ZF_cs addEs [apply_type]) 1); |
|
538 | 403 |
by (simp_tac (FOL_ss addsimps cons_iff::mem_simps) 1); |
485 | 404 |
by (resolve_tac [fun_extension] 1 THEN REPEAT (ares_tac [fun_extend] 1)); |
405 |
by (etac consE 1); |
|
406 |
by (ALLGOALS |
|
407 |
(asm_simp_tac (FOL_ss addsimps [restrict, fun_extend_apply1, |
|
538 | 408 |
fun_extend_apply2]))); |
485 | 409 |
val cons_fun_eq = result(); |
410 |