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