6 Functions in Zermelo-Fraenkel Set Theory |
6 Functions in Zermelo-Fraenkel Set Theory |
7 *) |
7 *) |
8 |
8 |
9 (*** The Pi operator -- dependent function space ***) |
9 (*** The Pi operator -- dependent function space ***) |
10 |
10 |
11 goalw ZF.thy [Pi_def] |
11 goalw thy [Pi_def] |
12 "f: Pi(A,B) <-> function(f) & f<=Sigma(A,B) & A<=domain(f)"; |
12 "f: Pi(A,B) <-> function(f) & f<=Sigma(A,B) & A<=domain(f)"; |
13 by (fast_tac ZF_cs 1); |
13 by (Fast_tac 1); |
14 qed "Pi_iff"; |
14 qed "Pi_iff"; |
15 |
15 |
16 (*For upward compatibility with the former definition*) |
16 (*For upward compatibility with the former definition*) |
17 goalw ZF.thy [Pi_def, function_def] |
17 goalw thy [Pi_def, function_def] |
18 "f: Pi(A,B) <-> f<=Sigma(A,B) & (ALL x:A. EX! y. <x,y>: f)"; |
18 "f: Pi(A,B) <-> f<=Sigma(A,B) & (ALL x:A. EX! y. <x,y>: f)"; |
19 by (safe_tac ZF_cs); |
19 by (safe_tac (!claset)); |
20 by (best_tac ZF_cs 1); |
20 by (Best_tac 1); |
21 by (best_tac ZF_cs 1); |
21 by (Best_tac 1); |
22 by (set_mp_tac 1); |
22 by (set_mp_tac 1); |
23 by (deepen_tac ZF_cs 3 1); |
23 by (Deepen_tac 3 1); |
24 qed "Pi_iff_old"; |
24 qed "Pi_iff_old"; |
25 |
25 |
26 goal ZF.thy "!!f. f: Pi(A,B) ==> function(f)"; |
26 goal thy "!!f. f: Pi(A,B) ==> function(f)"; |
27 by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff]) 1); |
27 by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff]) 1); |
28 qed "fun_is_function"; |
28 qed "fun_is_function"; |
29 |
29 |
30 (**Two "destruct" rules for Pi **) |
30 (**Two "destruct" rules for Pi **) |
31 |
31 |
32 val [major] = goalw ZF.thy [Pi_def] "f: Pi(A,B) ==> f <= Sigma(A,B)"; |
32 val [major] = goalw thy [Pi_def] "f: Pi(A,B) ==> f <= Sigma(A,B)"; |
33 by (rtac (major RS CollectD1 RS PowD) 1); |
33 by (rtac (major RS CollectD1 RS PowD) 1); |
34 qed "fun_is_rel"; |
34 qed "fun_is_rel"; |
35 |
35 |
36 goal ZF.thy "!!f. [| f: Pi(A,B); a:A |] ==> EX! y. <a,y>: f"; |
36 goal thy "!!f. [| f: Pi(A,B); a:A |] ==> EX! y. <a,y>: f"; |
37 by (fast_tac (ZF_cs addSDs [Pi_iff_old RS iffD1]) 1); |
37 by (fast_tac ((!claset) addSDs [Pi_iff_old RS iffD1]) 1); |
38 qed "fun_unique_Pair"; |
38 qed "fun_unique_Pair"; |
39 |
39 |
40 val prems = goalw ZF.thy [Pi_def] |
40 val prems = goalw thy [Pi_def] |
41 "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> Pi(A,B) = Pi(A',B')"; |
41 "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> Pi(A,B) = Pi(A',B')"; |
42 by (simp_tac (FOL_ss addsimps prems addcongs [Sigma_cong]) 1); |
42 by (simp_tac (FOL_ss addsimps prems addcongs [Sigma_cong]) 1); |
43 qed "Pi_cong"; |
43 qed "Pi_cong"; |
44 |
44 |
|
45 (*Sigma_cong, Pi_cong NOT given to Addcongs: they cause |
|
46 flex-flex pairs and the "Check your prover" error. Most |
|
47 Sigmas and Pis are abbreviated as * or -> *) |
|
48 |
45 (*Weakening one function type to another; see also Pi_type*) |
49 (*Weakening one function type to another; see also Pi_type*) |
46 goalw ZF.thy [Pi_def] "!!f. [| f: A->B; B<=D |] ==> f: A->D"; |
50 goalw thy [Pi_def] "!!f. [| f: A->B; B<=D |] ==> f: A->D"; |
47 by (best_tac ZF_cs 1); |
51 by (Best_tac 1); |
48 qed "fun_weaken_type"; |
52 qed "fun_weaken_type"; |
49 |
53 |
50 (*Empty function spaces*) |
54 (*Empty function spaces*) |
51 goalw ZF.thy [Pi_def, function_def] "Pi(0,A) = {0}"; |
55 goalw thy [Pi_def, function_def] "Pi(0,A) = {0}"; |
52 by (fast_tac eq_cs 1); |
56 by (fast_tac eq_cs 1); |
53 qed "Pi_empty1"; |
57 qed "Pi_empty1"; |
54 |
58 |
55 goalw ZF.thy [Pi_def] "!!A a. a:A ==> A->0 = 0"; |
59 goalw thy [Pi_def] "!!A a. a:A ==> A->0 = 0"; |
56 by (fast_tac eq_cs 1); |
60 by (fast_tac eq_cs 1); |
57 qed "Pi_empty2"; |
61 qed "Pi_empty2"; |
58 |
62 |
59 (*The empty function*) |
63 (*The empty function*) |
60 goalw ZF.thy [Pi_def, function_def] "0: Pi(0,B)"; |
64 goalw thy [Pi_def, function_def] "0: Pi(0,B)"; |
61 by (fast_tac ZF_cs 1); |
65 by (Fast_tac 1); |
62 qed "empty_fun"; |
66 qed "empty_fun"; |
63 |
67 |
64 (*The singleton function*) |
68 (*The singleton function*) |
65 goalw ZF.thy [Pi_def, function_def] "{<a,b>} : {a} -> {b}"; |
69 goalw thy [Pi_def, function_def] "{<a,b>} : {a} -> {b}"; |
66 by (fast_tac eq_cs 1); |
70 by (fast_tac eq_cs 1); |
67 qed "singleton_fun"; |
71 qed "singleton_fun"; |
68 |
72 |
|
73 Addsimps [empty_fun, singleton_fun]; |
|
74 |
69 (*** Function Application ***) |
75 (*** Function Application ***) |
70 |
76 |
71 goalw ZF.thy [Pi_def, function_def] |
77 goalw thy [Pi_def, function_def] |
72 "!!a b f. [| <a,b>: f; <a,c>: f; f: Pi(A,B) |] ==> b=c"; |
78 "!!a b f. [| <a,b>: f; <a,c>: f; f: Pi(A,B) |] ==> b=c"; |
73 by (deepen_tac ZF_cs 3 1); |
79 by (Deepen_tac 3 1); |
74 qed "apply_equality2"; |
80 qed "apply_equality2"; |
75 |
81 |
76 goalw ZF.thy [apply_def] "!!a b f. [| <a,b>: f; f: Pi(A,B) |] ==> f`a = b"; |
82 goalw thy [apply_def] "!!a b f. [| <a,b>: f; f: Pi(A,B) |] ==> f`a = b"; |
77 by (rtac the_equality 1); |
83 by (rtac the_equality 1); |
78 by (rtac apply_equality2 2); |
84 by (rtac apply_equality2 2); |
79 by (REPEAT (assume_tac 1)); |
85 by (REPEAT (assume_tac 1)); |
80 qed "apply_equality"; |
86 qed "apply_equality"; |
81 |
87 |
82 (*Applying a function outside its domain yields 0*) |
88 (*Applying a function outside its domain yields 0*) |
83 goalw ZF.thy [apply_def] |
89 goalw thy [apply_def] |
84 "!!a b f. [| a ~: domain(f); f: Pi(A,B) |] ==> f`a = 0"; |
90 "!!a b f. [| a ~: domain(f); f: Pi(A,B) |] ==> f`a = 0"; |
85 by (rtac the_0 1); |
91 by (rtac the_0 1); |
86 by (fast_tac ZF_cs 1); |
92 by (Fast_tac 1); |
87 qed "apply_0"; |
93 qed "apply_0"; |
88 |
94 |
89 goal ZF.thy "!!f. [| f: Pi(A,B); c: f |] ==> EX x:A. c = <x,f`x>"; |
95 goal thy "!!f. [| f: Pi(A,B); c: f |] ==> EX x:A. c = <x,f`x>"; |
90 by (forward_tac [fun_is_rel] 1); |
96 by (forward_tac [fun_is_rel] 1); |
91 by (fast_tac (ZF_cs addDs [apply_equality]) 1); |
97 by (fast_tac ((!claset) addDs [apply_equality]) 1); |
92 qed "Pi_memberD"; |
98 qed "Pi_memberD"; |
93 |
99 |
94 goal ZF.thy "!!f. [| f: Pi(A,B); a:A |] ==> <a,f`a>: f"; |
100 goal thy "!!f. [| f: Pi(A,B); a:A |] ==> <a,f`a>: f"; |
95 by (rtac (fun_unique_Pair RS ex1E) 1); |
101 by (rtac (fun_unique_Pair RS ex1E) 1); |
96 by (resolve_tac [apply_equality RS ssubst] 3); |
102 by (resolve_tac [apply_equality RS ssubst] 3); |
97 by (REPEAT (assume_tac 1)); |
103 by (REPEAT (assume_tac 1)); |
98 qed "apply_Pair"; |
104 qed "apply_Pair"; |
99 |
105 |
100 (*Conclusion is flexible -- use res_inst_tac or else apply_funtype below!*) |
106 (*Conclusion is flexible -- use res_inst_tac or else apply_funtype below!*) |
101 goal ZF.thy "!!f. [| f: Pi(A,B); a:A |] ==> f`a : B(a)"; |
107 goal thy "!!f. [| f: Pi(A,B); a:A |] ==> f`a : B(a)"; |
102 by (rtac (fun_is_rel RS subsetD RS SigmaE2) 1); |
108 by (rtac (fun_is_rel RS subsetD RS SigmaE2) 1); |
103 by (REPEAT (ares_tac [apply_Pair] 1)); |
109 by (REPEAT (ares_tac [apply_Pair] 1)); |
104 qed "apply_type"; |
110 qed "apply_type"; |
105 |
111 |
106 (*This version is acceptable to the simplifier*) |
112 (*This version is acceptable to the simplifier*) |
107 goal ZF.thy "!!f. [| f: A->B; a:A |] ==> f`a : B"; |
113 goal thy "!!f. [| f: A->B; a:A |] ==> f`a : B"; |
108 by (REPEAT (ares_tac [apply_type] 1)); |
114 by (REPEAT (ares_tac [apply_type] 1)); |
109 qed "apply_funtype"; |
115 qed "apply_funtype"; |
110 |
116 |
111 val [major] = goal ZF.thy |
117 val [major] = goal thy |
112 "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b"; |
118 "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b"; |
113 by (cut_facts_tac [major RS fun_is_rel] 1); |
119 by (cut_facts_tac [major RS fun_is_rel] 1); |
114 by (fast_tac (ZF_cs addSIs [major RS apply_Pair, |
120 by (fast_tac ((!claset) addSIs [major RS apply_Pair, |
115 major RSN (2,apply_equality)]) 1); |
121 major RSN (2,apply_equality)]) 1); |
116 qed "apply_iff"; |
122 qed "apply_iff"; |
117 |
123 |
118 (*Refining one Pi type to another*) |
124 (*Refining one Pi type to another*) |
119 val pi_prem::prems = goal ZF.thy |
125 val pi_prem::prems = goal thy |
120 "[| f: Pi(A,C); !!x. x:A ==> f`x : B(x) |] ==> f : Pi(A,B)"; |
126 "[| f: Pi(A,C); !!x. x:A ==> f`x : B(x) |] ==> f : Pi(A,B)"; |
121 by (cut_facts_tac [pi_prem] 1); |
127 by (cut_facts_tac [pi_prem] 1); |
122 by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff]) 1); |
128 by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff]) 1); |
123 by (fast_tac (ZF_cs addIs prems addSDs [pi_prem RS Pi_memberD]) 1); |
129 by (fast_tac ((!claset) addIs prems addSDs [pi_prem RS Pi_memberD]) 1); |
124 qed "Pi_type"; |
130 qed "Pi_type"; |
125 |
131 |
126 |
132 |
127 (** Elimination of membership in a function **) |
133 (** Elimination of membership in a function **) |
128 |
134 |
129 goal ZF.thy "!!a A. [| <a,b> : f; f: Pi(A,B) |] ==> a : A"; |
135 goal 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)); |
136 by (REPEAT (ares_tac [fun_is_rel RS subsetD RS SigmaD1] 1)); |
131 qed "domain_type"; |
137 qed "domain_type"; |
132 |
138 |
133 goal ZF.thy "!!b B a. [| <a,b> : f; f: Pi(A,B) |] ==> b : B(a)"; |
139 goal 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); |
140 by (etac (fun_is_rel RS subsetD RS SigmaD2) 1); |
135 by (assume_tac 1); |
141 by (assume_tac 1); |
136 qed "range_type"; |
142 qed "range_type"; |
137 |
143 |
138 val prems = goal ZF.thy |
144 val prems = goal thy |
139 "[| <a,b>: f; f: Pi(A,B); \ |
145 "[| <a,b>: f; f: Pi(A,B); \ |
140 \ [| a:A; b:B(a); f`a = b |] ==> P \ |
146 \ [| a:A; b:B(a); f`a = b |] ==> P \ |
141 \ |] ==> P"; |
147 \ |] ==> P"; |
142 by (cut_facts_tac prems 1); |
148 by (cut_facts_tac prems 1); |
143 by (resolve_tac prems 1); |
149 by (resolve_tac prems 1); |
144 by (REPEAT (eresolve_tac [asm_rl,domain_type,range_type,apply_equality] 1)); |
150 by (REPEAT (eresolve_tac [asm_rl,domain_type,range_type,apply_equality] 1)); |
145 qed "Pair_mem_PiE"; |
151 qed "Pair_mem_PiE"; |
146 |
152 |
147 (*** Lambda Abstraction ***) |
153 (*** Lambda Abstraction ***) |
148 |
154 |
149 goalw ZF.thy [lam_def] "!!A b. a:A ==> <a,b(a)> : (lam x:A. b(x))"; |
155 goalw thy [lam_def] "!!A b. a:A ==> <a,b(a)> : (lam x:A. b(x))"; |
150 by (etac RepFunI 1); |
156 by (etac RepFunI 1); |
151 qed "lamI"; |
157 qed "lamI"; |
152 |
158 |
153 val major::prems = goalw ZF.thy [lam_def] |
159 val major::prems = goalw thy [lam_def] |
154 "[| p: (lam x:A. b(x)); !!x.[| x:A; p=<x,b(x)> |] ==> P \ |
160 "[| p: (lam x:A. b(x)); !!x.[| x:A; p=<x,b(x)> |] ==> P \ |
155 \ |] ==> P"; |
161 \ |] ==> P"; |
156 by (rtac (major RS RepFunE) 1); |
162 by (rtac (major RS RepFunE) 1); |
157 by (REPEAT (ares_tac prems 1)); |
163 by (REPEAT (ares_tac prems 1)); |
158 qed "lamE"; |
164 qed "lamE"; |
159 |
165 |
160 goal ZF.thy "!!a b c. [| <a,c>: (lam x:A. b(x)) |] ==> c = b(a)"; |
166 goal 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)); |
167 by (REPEAT (eresolve_tac [asm_rl,lamE,Pair_inject,ssubst] 1)); |
162 qed "lamD"; |
168 qed "lamD"; |
163 |
169 |
164 val prems = goalw ZF.thy [lam_def, Pi_def, function_def] |
170 val prems = goalw thy [lam_def, Pi_def, function_def] |
165 "[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A.b(x)) : Pi(A,B)"; |
171 "[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A.b(x)) : Pi(A,B)"; |
166 by (fast_tac (ZF_cs addIs prems) 1); |
172 by (fast_tac ((!claset) addIs prems) 1); |
167 qed "lam_type"; |
173 qed "lam_type"; |
168 |
174 |
169 goal ZF.thy "(lam x:A.b(x)) : A -> {b(x). x:A}"; |
175 goal thy "(lam x:A.b(x)) : A -> {b(x). x:A}"; |
170 by (REPEAT (ares_tac [refl,lam_type,RepFunI] 1)); |
176 by (REPEAT (ares_tac [refl,lam_type,RepFunI] 1)); |
171 qed "lam_funtype"; |
177 qed "lam_funtype"; |
172 |
178 |
173 goal ZF.thy "!!a A. a : A ==> (lam x:A.b(x)) ` a = b(a)"; |
179 goal thy "!!a A. a : A ==> (lam x:A.b(x)) ` a = b(a)"; |
174 by (REPEAT (ares_tac [apply_equality,lam_funtype,lamI] 1)); |
180 by (REPEAT (ares_tac [apply_equality,lam_funtype,lamI] 1)); |
175 qed "beta"; |
181 qed "beta"; |
176 |
182 |
|
183 goalw thy [lam_def] "(lam x:0. b(x)) = 0"; |
|
184 by (Simp_tac 1); |
|
185 qed "lam_empty"; |
|
186 |
|
187 Addsimps [beta, lam_empty]; |
|
188 |
177 (*congruence rule for lambda abstraction*) |
189 (*congruence rule for lambda abstraction*) |
178 val prems = goalw ZF.thy [lam_def] |
190 val prems = goalw thy [lam_def] |
179 "[| A=A'; !!x. x:A' ==> b(x)=b'(x) |] ==> Lambda(A,b) = Lambda(A',b')"; |
191 "[| A=A'; !!x. x:A' ==> b(x)=b'(x) |] ==> Lambda(A,b) = Lambda(A',b')"; |
180 by (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1); |
192 by (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1); |
181 qed "lam_cong"; |
193 qed "lam_cong"; |
182 |
194 |
183 val [major] = goal ZF.thy |
195 Addcongs [lam_cong]; |
|
196 |
|
197 val [major] = goal thy |
184 "(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)"; |
198 "(!!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); |
199 by (res_inst_tac [("x", "lam x: A. THE y. Q(x,y)")] exI 1); |
186 by (rtac ballI 1); |
200 by (rtac ballI 1); |
187 by (stac beta 1); |
201 by (stac beta 1); |
188 by (assume_tac 1); |
202 by (assume_tac 1); |
226 qed "Pi_lamE"; |
242 qed "Pi_lamE"; |
227 |
243 |
228 |
244 |
229 (** Images of functions **) |
245 (** Images of functions **) |
230 |
246 |
231 goalw ZF.thy [lam_def] "!!C A. C <= A ==> (lam x:A.b(x)) `` C = {b(x). x:C}"; |
247 goalw thy [lam_def] "!!C A. C <= A ==> (lam x:A.b(x)) `` C = {b(x). x:C}"; |
232 by (fast_tac eq_cs 1); |
248 by (fast_tac eq_cs 1); |
233 qed "image_lam"; |
249 qed "image_lam"; |
234 |
250 |
235 goal ZF.thy "!!C A. [| f : Pi(A,B); C <= A |] ==> f``C = {f`x. x:C}"; |
251 goal thy "!!C A. [| f : Pi(A,B); C <= A |] ==> f``C = {f`x. x:C}"; |
236 by (etac (eta RS subst) 1); |
252 by (etac (eta RS subst) 1); |
237 by (asm_full_simp_tac (FOL_ss addsimps [beta, image_lam, subset_iff] |
253 by (asm_full_simp_tac (FOL_ss addsimps [beta, image_lam, subset_iff] |
238 addcongs [RepFun_cong]) 1); |
254 addcongs [RepFun_cong]) 1); |
239 qed "image_fun"; |
255 qed "image_fun"; |
240 |
256 |
241 |
257 |
242 (*** properties of "restrict" ***) |
258 (*** properties of "restrict" ***) |
243 |
259 |
244 goalw ZF.thy [restrict_def,lam_def] |
260 goalw thy [restrict_def,lam_def] |
245 "!!f A. [| f: Pi(C,B); A<=C |] ==> restrict(f,A) <= f"; |
261 "!!f A. [| f: Pi(C,B); A<=C |] ==> restrict(f,A) <= f"; |
246 by (fast_tac (ZF_cs addIs [apply_Pair]) 1); |
262 by (fast_tac ((!claset) addIs [apply_Pair]) 1); |
247 qed "restrict_subset"; |
263 qed "restrict_subset"; |
248 |
264 |
249 val prems = goalw ZF.thy [restrict_def] |
265 val prems = goalw thy [restrict_def] |
250 "[| !!x. x:A ==> f`x: B(x) |] ==> restrict(f,A) : Pi(A,B)"; |
266 "[| !!x. x:A ==> f`x: B(x) |] ==> restrict(f,A) : Pi(A,B)"; |
251 by (rtac lam_type 1); |
267 by (rtac lam_type 1); |
252 by (eresolve_tac prems 1); |
268 by (eresolve_tac prems 1); |
253 qed "restrict_type"; |
269 qed "restrict_type"; |
254 |
270 |
255 val [pi,subs] = goal ZF.thy |
271 val [pi,subs] = goal thy |
256 "[| f: Pi(C,B); A<=C |] ==> restrict(f,A) : Pi(A,B)"; |
272 "[| f: Pi(C,B); A<=C |] ==> restrict(f,A) : Pi(A,B)"; |
257 by (rtac (pi RS apply_type RS restrict_type) 1); |
273 by (rtac (pi RS apply_type RS restrict_type) 1); |
258 by (etac (subs RS subsetD) 1); |
274 by (etac (subs RS subsetD) 1); |
259 qed "restrict_type2"; |
275 qed "restrict_type2"; |
260 |
276 |
261 goalw ZF.thy [restrict_def] "!!a A. a : A ==> restrict(f,A) ` a = f`a"; |
277 goalw thy [restrict_def] "!!a A. a : A ==> restrict(f,A) ` a = f`a"; |
262 by (etac beta 1); |
278 by (etac beta 1); |
263 qed "restrict"; |
279 qed "restrict"; |
264 |
280 |
|
281 goalw thy [restrict_def] "restrict(f,0) = 0"; |
|
282 by (Simp_tac 1); |
|
283 qed "restrict_empty"; |
|
284 |
|
285 Addsimps [restrict, restrict_empty]; |
|
286 |
265 (*NOT SAFE as a congruence rule for the simplifier! Can cause it to fail!*) |
287 (*NOT SAFE as a congruence rule for the simplifier! Can cause it to fail!*) |
266 val prems = goalw ZF.thy [restrict_def] |
288 val prems = goalw thy [restrict_def] |
267 "[| A=B; !!x. x:B ==> f`x=g`x |] ==> restrict(f,A) = restrict(g,B)"; |
289 "[| A=B; !!x. x:B ==> f`x=g`x |] ==> restrict(f,A) = restrict(g,B)"; |
268 by (REPEAT (ares_tac (prems@[lam_cong]) 1)); |
290 by (REPEAT (ares_tac (prems@[lam_cong]) 1)); |
269 qed "restrict_eqI"; |
291 qed "restrict_eqI"; |
270 |
292 |
271 goalw ZF.thy [restrict_def, lam_def] "domain(restrict(f,C)) = C"; |
293 goalw thy [restrict_def, lam_def] "domain(restrict(f,C)) = C"; |
272 by (fast_tac eq_cs 1); |
294 by (fast_tac eq_cs 1); |
273 qed "domain_restrict"; |
295 qed "domain_restrict"; |
274 |
296 |
275 val [prem] = goalw ZF.thy [restrict_def] |
297 val [prem] = goalw thy [restrict_def] |
276 "A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))"; |
298 "A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))"; |
277 by (rtac (refl RS lam_cong) 1); |
299 by (rtac (refl RS lam_cong) 1); |
278 by (etac (prem RS subsetD RS beta) 1); (*easier than calling simp_tac*) |
300 by (etac (prem RS subsetD RS beta) 1); (*easier than calling simp_tac*) |
279 qed "restrict_lam_eq"; |
301 qed "restrict_lam_eq"; |
280 |
302 |
303 |
325 |
304 val Un_rls = [Un_subset_iff, domain_Un_eq, SUM_Un_distrib1, prod_Un_distrib2, |
326 val Un_rls = [Un_subset_iff, domain_Un_eq, SUM_Un_distrib1, prod_Un_distrib2, |
305 Un_upper1 RSN (2, subset_trans), |
327 Un_upper1 RSN (2, subset_trans), |
306 Un_upper2 RSN (2, subset_trans)]; |
328 Un_upper2 RSN (2, subset_trans)]; |
307 |
329 |
308 goal ZF.thy |
330 goal thy |
309 "!!f. [| f: A->B; g: C->D; A Int C = 0 |] ==> \ |
331 "!!f. [| f: A->B; g: C->D; A Int C = 0 |] ==> \ |
310 \ (f Un g) : (A Un C) -> (B Un D)"; |
332 \ (f Un g) : (A Un C) -> (B Un D)"; |
311 (*Solve the product and domain subgoals using distributive laws*) |
333 (*Solve the product and domain subgoals using distributive laws*) |
312 by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff,extension]@Un_rls) 1); |
334 by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff,extension]@Un_rls) 1); |
313 by (asm_simp_tac (FOL_ss addsimps [function_def]) 1); |
335 by (asm_simp_tac (FOL_ss addsimps [function_def]) 1); |
314 by (safe_tac ZF_cs); |
336 by (safe_tac (!claset)); |
315 (*Solve the two cases that contradict A Int C = 0*) |
337 (*Solve the two cases that contradict A Int C = 0*) |
316 by (deepen_tac ZF_cs 2 2); |
338 by (Deepen_tac 2 2); |
317 by (deepen_tac ZF_cs 2 2); |
339 by (Deepen_tac 2 2); |
318 by (rewtac function_def); |
340 by (rewtac function_def); |
319 by (REPEAT_FIRST (dtac (spec RS spec))); |
341 by (REPEAT_FIRST (dtac (spec RS spec))); |
320 by (deepen_tac ZF_cs 1 1); |
342 by (Deepen_tac 1 1); |
321 by (deepen_tac ZF_cs 1 1); |
343 by (Deepen_tac 1 1); |
322 qed "fun_disjoint_Un"; |
344 qed "fun_disjoint_Un"; |
323 |
345 |
324 goal ZF.thy |
346 goal thy |
325 "!!f g a. [| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \ |
347 "!!f g a. [| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \ |
326 \ (f Un g)`a = f`a"; |
348 \ (f Un g)`a = f`a"; |
327 by (rtac (apply_Pair RS UnI1 RS apply_equality) 1); |
349 by (rtac (apply_Pair RS UnI1 RS apply_equality) 1); |
328 by (REPEAT (ares_tac [fun_disjoint_Un] 1)); |
350 by (REPEAT (ares_tac [fun_disjoint_Un] 1)); |
329 qed "fun_disjoint_apply1"; |
351 qed "fun_disjoint_apply1"; |
330 |
352 |
331 goal ZF.thy |
353 goal thy |
332 "!!f g c. [| c:C; f: A->B; g: C->D; A Int C = 0 |] ==> \ |
354 "!!f g c. [| c:C; f: A->B; g: C->D; A Int C = 0 |] ==> \ |
333 \ (f Un g)`c = g`c"; |
355 \ (f Un g)`c = g`c"; |
334 by (rtac (apply_Pair RS UnI2 RS apply_equality) 1); |
356 by (rtac (apply_Pair RS UnI2 RS apply_equality) 1); |
335 by (REPEAT (ares_tac [fun_disjoint_Un] 1)); |
357 by (REPEAT (ares_tac [fun_disjoint_Un] 1)); |
336 qed "fun_disjoint_apply2"; |
358 qed "fun_disjoint_apply2"; |
337 |
359 |
338 (** Domain and range of a function/relation **) |
360 (** Domain and range of a function/relation **) |
339 |
361 |
340 goalw ZF.thy [Pi_def] "!!f. f : Pi(A,B) ==> domain(f)=A"; |
362 goalw thy [Pi_def] "!!f. f : Pi(A,B) ==> domain(f)=A"; |
341 by (fast_tac eq_cs 1); |
363 by (fast_tac eq_cs 1); |
342 qed "domain_of_fun"; |
364 qed "domain_of_fun"; |
343 |
365 |
344 goal ZF.thy "!!f. [| f : Pi(A,B); a: A |] ==> f`a : range(f)"; |
366 goal thy "!!f. [| f : Pi(A,B); a: A |] ==> f`a : range(f)"; |
345 by (etac (apply_Pair RS rangeI) 1); |
367 by (etac (apply_Pair RS rangeI) 1); |
346 by (assume_tac 1); |
368 by (assume_tac 1); |
347 qed "apply_rangeI"; |
369 qed "apply_rangeI"; |
348 |
370 |
349 val [major] = goal ZF.thy "f : Pi(A,B) ==> f : A->range(f)"; |
371 val [major] = goal thy "f : Pi(A,B) ==> f : A->range(f)"; |
350 by (rtac (major RS Pi_type) 1); |
372 by (rtac (major RS Pi_type) 1); |
351 by (etac (major RS apply_rangeI) 1); |
373 by (etac (major RS apply_rangeI) 1); |
352 qed "range_of_fun"; |
374 qed "range_of_fun"; |
353 |
375 |
354 (*** Extensions of functions ***) |
376 (*** Extensions of functions ***) |
355 |
377 |
356 goal ZF.thy |
378 goal thy |
357 "!!f A B. [| f: A->B; c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)"; |
379 "!!f A B. [| f: A->B; c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)"; |
358 by (forward_tac [singleton_fun RS fun_disjoint_Un] 1); |
380 by (forward_tac [singleton_fun RS fun_disjoint_Un] 1); |
359 by (asm_full_simp_tac (FOL_ss addsimps [cons_eq]) 2); |
381 by (asm_full_simp_tac (FOL_ss addsimps [cons_eq]) 2); |
360 by (fast_tac eq_cs 1); |
382 by (fast_tac eq_cs 1); |
361 qed "fun_extend"; |
383 qed "fun_extend"; |
362 |
384 |
363 goal ZF.thy |
385 goal thy |
364 "!!f A B. [| f: A->B; c~:A; b: B |] ==> cons(<c,b>,f) : cons(c,A) -> B"; |
386 "!!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); |
387 by (fast_tac ((!claset) addEs [fun_extend RS fun_weaken_type]) 1); |
366 qed "fun_extend3"; |
388 qed "fun_extend3"; |
367 |
389 |
368 goal ZF.thy "!!f A B. [| f: A->B; a:A; c~:A |] ==> cons(<c,b>,f)`a = f`a"; |
390 goal thy "!!f A B. [| f: A->B; a:A; c~:A |] ==> cons(<c,b>,f)`a = f`a"; |
369 by (rtac (apply_Pair RS consI2 RS apply_equality) 1); |
391 by (rtac (apply_Pair RS consI2 RS apply_equality) 1); |
370 by (rtac fun_extend 3); |
392 by (rtac fun_extend 3); |
371 by (REPEAT (assume_tac 1)); |
393 by (REPEAT (assume_tac 1)); |
372 qed "fun_extend_apply1"; |
394 qed "fun_extend_apply1"; |
373 |
395 |
374 goal ZF.thy "!!f A B. [| f: A->B; c~:A |] ==> cons(<c,b>,f)`c = b"; |
396 goal thy "!!f A B. [| f: A->B; c~:A |] ==> cons(<c,b>,f)`c = b"; |
375 by (rtac (consI1 RS apply_equality) 1); |
397 by (rtac (consI1 RS apply_equality) 1); |
376 by (rtac fun_extend 1); |
398 by (rtac fun_extend 1); |
377 by (REPEAT (assume_tac 1)); |
399 by (REPEAT (assume_tac 1)); |
378 qed "fun_extend_apply2"; |
400 qed "fun_extend_apply2"; |
379 |
401 |
|
402 bind_thm ("singleton_apply", [singletonI, singleton_fun] MRS apply_equality); |
|
403 Addsimps [singleton_apply]; |
|
404 |
380 (*For Finite.ML. Inclusion of right into left is easy*) |
405 (*For Finite.ML. Inclusion of right into left is easy*) |
381 goal ZF.thy |
406 goal thy |
382 "!!c. c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})"; |
407 "!!c. c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})"; |
383 by (rtac equalityI 1); |
408 by (rtac equalityI 1); |
384 by (safe_tac (ZF_cs addSEs [fun_extend3])); |
409 by (safe_tac ((!claset) addSEs [fun_extend3])); |
385 (*Inclusion of left into right*) |
410 (*Inclusion of left into right*) |
386 by (subgoal_tac "restrict(x, A) : A -> B" 1); |
411 by (subgoal_tac "restrict(x, A) : A -> B" 1); |
387 by (fast_tac (ZF_cs addEs [restrict_type2]) 2); |
412 by (fast_tac ((!claset) addEs [restrict_type2]) 2); |
388 by (rtac UN_I 1 THEN assume_tac 1); |
413 by (rtac UN_I 1 THEN assume_tac 1); |
389 by (rtac (apply_funtype RS UN_I) 1 THEN REPEAT (ares_tac [consI1] 1)); |
414 by (rtac (apply_funtype RS UN_I) 1 THEN REPEAT (ares_tac [consI1] 1)); |
390 by (simp_tac (FOL_ss addsimps cons_iff::mem_simps) 1); |
415 by (Simp_tac 1); |
391 by (rtac fun_extension 1 THEN REPEAT (ares_tac [fun_extend] 1)); |
416 by (rtac fun_extension 1 THEN REPEAT (ares_tac [fun_extend] 1)); |
392 by (etac consE 1); |
417 by (etac consE 1); |
393 by (ALLGOALS |
418 by (ALLGOALS |
394 (asm_simp_tac (FOL_ss addsimps [restrict, fun_extend_apply1, |
419 (asm_simp_tac (!simpset addsimps [restrict, fun_extend_apply1, |
395 fun_extend_apply2]))); |
420 fun_extend_apply2]))); |
396 qed "cons_fun_eq"; |
421 qed "cons_fun_eq"; |
397 |
422 |