author | oheimb |
Thu, 01 Feb 2001 20:51:48 +0100 | |
changeset 11025 | a70b796d9af8 |
parent 10832 | e33b47e4246d |
child 11395 | 2eeaa1077b73 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/Fun |
923 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Tobias Nipkow, Cambridge University Computer Laboratory |
923 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
6 |
Lemmas about functions. |
|
7 |
*) |
|
8 |
||
7089 | 9 |
Goal "(f = g) = (! x. f(x)=g(x))"; |
923 | 10 |
by (rtac iffI 1); |
1264 | 11 |
by (Asm_simp_tac 1); |
12 |
by (rtac ext 1 THEN Asm_simp_tac 1); |
|
923 | 13 |
qed "expand_fun_eq"; |
14 |
||
5316 | 15 |
val prems = Goal |
923 | 16 |
"[| f(x)=u; !!x. P(x) ==> g(f(x)) = x; P(x) |] ==> x=g(u)"; |
17 |
by (rtac (arg_cong RS box_equals) 1); |
|
18 |
by (REPEAT (resolve_tac (prems@[refl]) 1)); |
|
19 |
qed "apply_inverse"; |
|
20 |
||
21 |
||
4656 | 22 |
(** "Axiom" of Choice, proved using the description operator **) |
23 |
||
9838 | 24 |
(*"choice" is now proved in Tools/meson.ML*) |
4656 | 25 |
|
5316 | 26 |
Goal "!!S. ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)"; |
9970 | 27 |
by (fast_tac (claset() addEs [someI]) 1); |
4656 | 28 |
qed "bchoice"; |
29 |
||
30 |
||
5608 | 31 |
section "id"; |
5441 | 32 |
|
7089 | 33 |
Goalw [id_def] "id x = x"; |
34 |
by (rtac refl 1); |
|
35 |
qed "id_apply"; |
|
5608 | 36 |
Addsimps [id_apply]; |
5441 | 37 |
|
8226 | 38 |
Goal "inv id = id"; |
39 |
by (simp_tac (simpset() addsimps [inv_def,id_def]) 1); |
|
40 |
qed "inv_id"; |
|
41 |
Addsimps [inv_id]; |
|
42 |
||
5441 | 43 |
|
5306 | 44 |
section "o"; |
45 |
||
7089 | 46 |
Goalw [o_def] "(f o g) x = f (g x)"; |
47 |
by (rtac refl 1); |
|
48 |
qed "o_apply"; |
|
5306 | 49 |
Addsimps [o_apply]; |
50 |
||
7089 | 51 |
Goalw [o_def] "f o (g o h) = f o g o h"; |
52 |
by (rtac ext 1); |
|
53 |
by (rtac refl 1); |
|
54 |
qed "o_assoc"; |
|
5306 | 55 |
|
7089 | 56 |
Goalw [id_def] "id o g = g"; |
57 |
by (rtac ext 1); |
|
58 |
by (Simp_tac 1); |
|
59 |
qed "id_o"; |
|
5608 | 60 |
Addsimps [id_o]; |
5306 | 61 |
|
7089 | 62 |
Goalw [id_def] "f o id = f"; |
63 |
by (rtac ext 1); |
|
64 |
by (Simp_tac 1); |
|
65 |
qed "o_id"; |
|
5608 | 66 |
Addsimps [o_id]; |
5306 | 67 |
|
10832 | 68 |
Goalw [o_def] "(f o g)`r = f`(g`r)"; |
5306 | 69 |
by (Blast_tac 1); |
70 |
qed "image_compose"; |
|
71 |
||
10832 | 72 |
Goal "f`A = (UN x:A. {f x})"; |
7536 | 73 |
by (Blast_tac 1); |
7916 | 74 |
qed "image_eq_UN"; |
7536 | 75 |
|
10832 | 76 |
Goalw [o_def] "UNION A (g o f) = UNION (f`A) g"; |
5852 | 77 |
by (Blast_tac 1); |
6829
50459a995aa3
renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents:
6301
diff
changeset
|
78 |
qed "UN_o"; |
5852 | 79 |
|
7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
80 |
(** lemma for proving injectivity of representation functions for **) |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
81 |
(** datatypes involving function types **) |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
82 |
|
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
83 |
Goalw [o_def] |
7089 | 84 |
"[| ! x y. g (f x) = g y --> f x = y; g o f = g o fa |] ==> f = fa"; |
85 |
by (rtac ext 1); |
|
86 |
by (etac allE 1); |
|
87 |
by (etac allE 1); |
|
88 |
by (etac mp 1); |
|
89 |
by (etac fun_cong 1); |
|
7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
90 |
qed "inj_fun_lemma"; |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
91 |
|
5306 | 92 |
|
93 |
section "inj"; |
|
6171 | 94 |
(**NB: inj now just translates to inj_on**) |
5306 | 95 |
|
923 | 96 |
(*** inj(f): f is a one-to-one function ***) |
97 |
||
6171 | 98 |
(*for Tools/datatype_rep_proofs*) |
99 |
val [prem] = Goalw [inj_on_def] |
|
100 |
"(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)"; |
|
101 |
by (blast_tac (claset() addIs [prem RS spec RS mp]) 1); |
|
102 |
qed "datatype_injI"; |
|
923 | 103 |
|
6171 | 104 |
Goalw [inj_on_def] "[| inj(f); f(x) = f(y) |] ==> x=y"; |
5316 | 105 |
by (Blast_tac 1); |
923 | 106 |
qed "injD"; |
107 |
||
108 |
(*Useful with the simplifier*) |
|
5316 | 109 |
Goal "inj(f) ==> (f(x) = f(y)) = (x=y)"; |
923 | 110 |
by (rtac iffI 1); |
5316 | 111 |
by (etac arg_cong 2); |
112 |
by (etac injD 1); |
|
5318 | 113 |
by (assume_tac 1); |
923 | 114 |
qed "inj_eq"; |
115 |
||
116 |
(*A one-to-one function has an inverse (given using select).*) |
|
5316 | 117 |
Goalw [inv_def] "inj(f) ==> inv f (f x) = x"; |
10076
2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset
|
118 |
by (asm_simp_tac (simpset() addsimps [inj_eq]) 1); |
2912 | 119 |
qed "inv_f_f"; |
7338 | 120 |
Addsimps [inv_f_f]; |
923 | 121 |
|
7338 | 122 |
Goal "[| inj(f); f x = y |] ==> inv f y = x"; |
123 |
by (etac subst 1); |
|
124 |
by (etac inv_f_f 1); |
|
125 |
qed "inv_f_eq"; |
|
6235 | 126 |
|
10066 | 127 |
Goal "[| inj f; ALL x. f(g x) = x |] ==> inv f = g"; |
128 |
by (blast_tac (claset() addIs [ext, inv_f_eq]) 1); |
|
129 |
qed "inj_imp_inv_eq"; |
|
130 |
||
923 | 131 |
(* Useful??? *) |
5316 | 132 |
val [oneone,minor] = Goal |
2912 | 133 |
"[| inj(f); !!y. y: range(f) ==> P(inv f y) |] ==> P(x)"; |
134 |
by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1); |
|
923 | 135 |
by (rtac (rangeI RS minor) 1); |
136 |
qed "inj_transfer"; |
|
137 |
||
7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
138 |
Goalw [o_def] "[| inj f; f o g = f o h |] ==> g = h"; |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
139 |
by (rtac ext 1); |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
140 |
by (etac injD 1); |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
141 |
by (etac fun_cong 1); |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
142 |
qed "inj_o"; |
923 | 143 |
|
4830 | 144 |
(*** inj_on f A: f is one-to-one over A ***) |
923 | 145 |
|
5316 | 146 |
val prems = Goalw [inj_on_def] |
4830 | 147 |
"(!! x y. [| f(x) = f(y); x:A; y:A |] ==> x=y) ==> inj_on f A"; |
4089 | 148 |
by (blast_tac (claset() addIs prems) 1); |
4830 | 149 |
qed "inj_onI"; |
9108 | 150 |
bind_thm ("injI", inj_onI); (*for compatibility*) |
923 | 151 |
|
5316 | 152 |
val [major] = Goal |
4830 | 153 |
"(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A"; |
154 |
by (rtac inj_onI 1); |
|
923 | 155 |
by (etac (apply_inverse RS trans) 1); |
156 |
by (REPEAT (eresolve_tac [asm_rl,major] 1)); |
|
4830 | 157 |
qed "inj_on_inverseI"; |
9108 | 158 |
bind_thm ("inj_inverseI", inj_on_inverseI); (*for compatibility*) |
923 | 159 |
|
8285 | 160 |
Goal "(inj f) = (inv f o f = id)"; |
161 |
by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1); |
|
162 |
by (blast_tac (claset() addIs [inj_inverseI, inv_f_f]) 1); |
|
163 |
qed "inj_iff"; |
|
164 |
||
5316 | 165 |
Goalw [inj_on_def] "[| inj_on f A; f(x)=f(y); x:A; y:A |] ==> x=y"; |
166 |
by (Blast_tac 1); |
|
4830 | 167 |
qed "inj_onD"; |
923 | 168 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
169 |
Goal "[| inj_on f A; x:A; y:A |] ==> (f(x)=f(y)) = (x=y)"; |
4830 | 170 |
by (blast_tac (claset() addSDs [inj_onD]) 1); |
171 |
qed "inj_on_iff"; |
|
923 | 172 |
|
5316 | 173 |
Goalw [inj_on_def] "[| inj_on f A; ~x=y; x:A; y:A |] ==> ~ f(x)=f(y)"; |
174 |
by (Blast_tac 1); |
|
4830 | 175 |
qed "inj_on_contraD"; |
923 | 176 |
|
8156 | 177 |
Goal "inj (%s. {s})"; |
8253 | 178 |
by (rtac injI 1); |
179 |
by (etac singleton_inject 1); |
|
8156 | 180 |
qed "inj_singleton"; |
181 |
||
5316 | 182 |
Goalw [inj_on_def] "[| A<=B; inj_on f B |] ==> inj_on f A"; |
3341 | 183 |
by (Blast_tac 1); |
4830 | 184 |
qed "subset_inj_on"; |
3341 | 185 |
|
923 | 186 |
|
6235 | 187 |
(** surj **) |
188 |
||
6267 | 189 |
val [prem] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g"; |
190 |
by (blast_tac (claset() addIs [prem RS sym]) 1); |
|
6235 | 191 |
qed "surjI"; |
192 |
||
193 |
Goalw [surj_def] "surj f ==> range f = UNIV"; |
|
194 |
by Auto_tac; |
|
195 |
qed "surj_range"; |
|
196 |
||
6267 | 197 |
Goalw [surj_def] "surj f ==> EX x. y = f x"; |
198 |
by (Blast_tac 1); |
|
199 |
qed "surjD"; |
|
200 |
||
8253 | 201 |
Goal "inj f ==> surj (inv f)"; |
202 |
by (blast_tac (claset() addIs [surjI, inv_f_f]) 1); |
|
203 |
qed "inj_imp_surj_inv"; |
|
7374 | 204 |
|
205 |
||
6171 | 206 |
(*** Lemmas about injective functions and inv ***) |
923 | 207 |
|
10832 | 208 |
Goalw [o_def] "[| inj_on f A; inj_on g (f`A) |] ==> inj_on (g o f) A"; |
6171 | 209 |
by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1); |
210 |
qed "comp_inj_on"; |
|
923 | 211 |
|
5316 | 212 |
Goalw [inv_def] "y : range(f) ==> f(inv f y) = y"; |
9970 | 213 |
by (fast_tac (claset() addIs [someI]) 1); |
2912 | 214 |
qed "f_inv_f"; |
923 | 215 |
|
6235 | 216 |
Goal "surj f ==> f(inv f y) = y"; |
217 |
by (asm_simp_tac (simpset() addsimps [f_inv_f, surj_range]) 1); |
|
218 |
qed "surj_f_inv_f"; |
|
219 |
||
6171 | 220 |
Goal "[| inv f x = inv f y; x: range(f); y: range(f) |] ==> x=y"; |
2912 | 221 |
by (rtac (arg_cong RS box_equals) 1); |
5316 | 222 |
by (REPEAT (ares_tac [f_inv_f] 1)); |
2912 | 223 |
qed "inv_injective"; |
224 |
||
6235 | 225 |
Goal "A <= range(f) ==> inj_on (inv f) A"; |
4830 | 226 |
by (fast_tac (claset() addIs [inj_onI] |
6235 | 227 |
addEs [inv_injective, injD]) 1); |
4830 | 228 |
qed "inj_on_inv"; |
923 | 229 |
|
6235 | 230 |
Goal "surj f ==> inj (inv f)"; |
231 |
by (asm_simp_tac (simpset() addsimps [inj_on_inv, surj_range]) 1); |
|
232 |
qed "surj_imp_inj_inv"; |
|
233 |
||
8285 | 234 |
Goal "(surj f) = (f o inv f = id)"; |
235 |
by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1); |
|
236 |
by (blast_tac (claset() addIs [surjI, surj_f_inv_f]) 1); |
|
237 |
qed "surj_iff"; |
|
238 |
||
10066 | 239 |
Goal "[| surj f; ALL x. g(f x) = x |] ==> inv f = g"; |
240 |
by (rtac ext 1); |
|
241 |
by (dres_inst_tac [("x","inv f x")] spec 1); |
|
242 |
by (asm_full_simp_tac (simpset() addsimps [surj_f_inv_f]) 1); |
|
243 |
qed "surj_imp_inv_eq"; |
|
244 |
||
8253 | 245 |
|
246 |
(** Bijections **) |
|
247 |
||
248 |
Goalw [bij_def] "[| inj f; surj f |] ==> bij f"; |
|
249 |
by (Blast_tac 1); |
|
250 |
qed "bijI"; |
|
251 |
||
252 |
Goalw [bij_def] "bij f ==> inj f"; |
|
253 |
by (Blast_tac 1); |
|
254 |
qed "bij_is_inj"; |
|
255 |
||
256 |
Goalw [bij_def] "bij f ==> surj f"; |
|
257 |
by (Blast_tac 1); |
|
258 |
qed "bij_is_surj"; |
|
259 |
||
260 |
Goalw [bij_def] "bij f ==> bij (inv f)"; |
|
261 |
by (asm_simp_tac (simpset() addsimps [inj_imp_surj_inv, surj_imp_inj_inv]) 1); |
|
262 |
qed "bij_imp_bij_inv"; |
|
263 |
||
264 |
val prems = |
|
265 |
Goalw [inv_def] "[| !! x. g (f x) = x; !! y. f (g y) = y |] ==> inv f = g"; |
|
266 |
by (rtac ext 1); |
|
267 |
by (auto_tac (claset(), simpset() addsimps prems)); |
|
268 |
qed "inv_equality"; |
|
269 |
||
270 |
Goalw [bij_def] "bij f ==> inv (inv f) = f"; |
|
271 |
by (rtac inv_equality 1); |
|
272 |
by (auto_tac (claset(), simpset() addsimps [surj_f_inv_f])); |
|
273 |
qed "inv_inv_eq"; |
|
274 |
||
10066 | 275 |
(** bij(inv f) implies little about f. Consider f::bool=>bool such that |
276 |
f(True)=f(False)=True. Then it's consistent with axiom someI that |
|
277 |
inv(f) could be any function at all, including the identity function. |
|
278 |
If inv(f)=id then inv(f) is a bijection, but inj(f), surj(f) and |
|
279 |
inv(inv(f))=f all fail. |
|
280 |
**) |
|
281 |
||
8253 | 282 |
Goalw [bij_def] "[| bij f; bij g |] ==> inv (f o g) = inv g o inv f"; |
283 |
by (rtac (inv_equality) 1); |
|
284 |
by (auto_tac (claset(), simpset() addsimps [surj_f_inv_f])); |
|
285 |
qed "o_inv_distrib"; |
|
286 |
||
287 |
||
7514 | 288 |
(** We seem to need both the id-forms and the (%x. x) forms; the latter can |
289 |
arise by rewriting, while id may be used explicitly. **) |
|
290 |
||
10832 | 291 |
Goal "(%x. x) ` Y = Y"; |
7514 | 292 |
by (Blast_tac 1); |
293 |
qed "image_ident"; |
|
294 |
||
10832 | 295 |
Goalw [id_def] "id ` Y = Y"; |
7514 | 296 |
by (Blast_tac 1); |
297 |
qed "image_id"; |
|
298 |
Addsimps [image_ident, image_id]; |
|
299 |
||
10832 | 300 |
Goal "(%x. x) -` Y = Y"; |
7514 | 301 |
by (Blast_tac 1); |
302 |
qed "vimage_ident"; |
|
303 |
||
10832 | 304 |
Goalw [id_def] "id -` A = A"; |
7514 | 305 |
by Auto_tac; |
306 |
qed "vimage_id"; |
|
307 |
Addsimps [vimage_ident, vimage_id]; |
|
308 |
||
10832 | 309 |
Goal "f -` (f ` A) = {y. EX x:A. f x = f y}"; |
7876 | 310 |
by (blast_tac (claset() addIs [sym]) 1); |
311 |
qed "vimage_image_eq"; |
|
312 |
||
10832 | 313 |
Goal "f ` (f -` A) <= A"; |
8173 | 314 |
by (Blast_tac 1); |
315 |
qed "image_vimage_subset"; |
|
316 |
||
10832 | 317 |
Goal "f ` (f -` A) = A Int range f"; |
8173 | 318 |
by (Blast_tac 1); |
319 |
qed "image_vimage_eq"; |
|
320 |
Addsimps [image_vimage_eq]; |
|
321 |
||
10832 | 322 |
Goal "surj f ==> f ` (f -` A) = A"; |
8173 | 323 |
by (asm_simp_tac (simpset() addsimps [surj_range]) 1); |
324 |
qed "surj_image_vimage_eq"; |
|
325 |
||
10832 | 326 |
Goal "surj f ==> f ` (inv f ` A) = A"; |
8253 | 327 |
by (asm_simp_tac (simpset() addsimps [image_eq_UN, surj_f_inv_f]) 1); |
328 |
qed "image_surj_f_inv_f"; |
|
329 |
||
10832 | 330 |
Goalw [inj_on_def] "inj f ==> f -` (f ` A) = A"; |
8173 | 331 |
by (Blast_tac 1); |
332 |
qed "inj_vimage_image_eq"; |
|
333 |
||
10832 | 334 |
Goal "inj f ==> (inv f) ` (f ` A) = A"; |
8253 | 335 |
by (asm_simp_tac (simpset() addsimps [image_eq_UN]) 1); |
336 |
qed "image_inv_f_f"; |
|
337 |
||
10832 | 338 |
Goalw [surj_def] "surj f ==> f -` B <= A ==> B <= f ` A"; |
8173 | 339 |
by (blast_tac (claset() addIs [sym]) 1); |
340 |
qed "vimage_subsetD"; |
|
341 |
||
10832 | 342 |
Goalw [inj_on_def] "inj f ==> B <= f ` A ==> f -` B <= A"; |
8173 | 343 |
by (Blast_tac 1); |
344 |
qed "vimage_subsetI"; |
|
345 |
||
10832 | 346 |
Goalw [bij_def] "bij f ==> (f -` B <= A) = (B <= f ` A)"; |
8173 | 347 |
by (blast_tac (claset() delrules [subsetI] |
348 |
addIs [vimage_subsetI, vimage_subsetD]) 1); |
|
349 |
qed "vimage_subset_eq"; |
|
350 |
||
10832 | 351 |
Goal "f`(A Int B) <= f`A Int f`B"; |
6290 | 352 |
by (Blast_tac 1); |
353 |
qed "image_Int_subset"; |
|
354 |
||
10832 | 355 |
Goal "f`A - f`B <= f`(A - B)"; |
6290 | 356 |
by (Blast_tac 1); |
357 |
qed "image_diff_subset"; |
|
358 |
||
5069 | 359 |
Goalw [inj_on_def] |
10832 | 360 |
"[| inj_on f C; A<=C; B<=C |] ==> f`(A Int B) = f`A Int f`B"; |
4059 | 361 |
by (Blast_tac 1); |
4830 | 362 |
qed "inj_on_image_Int"; |
4059 | 363 |
|
5069 | 364 |
Goalw [inj_on_def] |
10832 | 365 |
"[| inj_on f C; A<=C; B<=C |] ==> f`(A-B) = f`A - f`B"; |
4059 | 366 |
by (Blast_tac 1); |
4830 | 367 |
qed "inj_on_image_set_diff"; |
4059 | 368 |
|
10832 | 369 |
Goalw [inj_on_def] "inj f ==> f`(A Int B) = f`A Int f`B"; |
4059 | 370 |
by (Blast_tac 1); |
371 |
qed "image_Int"; |
|
372 |
||
10832 | 373 |
Goalw [inj_on_def] "inj f ==> f`(A-B) = f`A - f`B"; |
4059 | 374 |
by (Blast_tac 1); |
375 |
qed "image_set_diff"; |
|
376 |
||
10832 | 377 |
Goalw [image_def] "inj(f) ==> inv(f)`(f`X) = X"; |
6235 | 378 |
by Auto_tac; |
379 |
qed "inv_image_comp"; |
|
5847 | 380 |
|
10832 | 381 |
Goal "inj f ==> (f a : f`A) = (a : A)"; |
6301 | 382 |
by (blast_tac (claset() addDs [injD]) 1); |
383 |
qed "inj_image_mem_iff"; |
|
384 |
||
10832 | 385 |
Goalw [inj_on_def] "inj f ==> (f`A <= f`B) = (A<=B)"; |
8253 | 386 |
by (Blast_tac 1); |
387 |
qed "inj_image_subset_iff"; |
|
388 |
||
10832 | 389 |
Goal "inj f ==> (f`A = f`B) = (A = B)"; |
6301 | 390 |
by (blast_tac (claset() addSEs [equalityE] addDs [injD]) 1); |
391 |
qed "inj_image_eq_iff"; |
|
392 |
||
10832 | 393 |
Goal "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))"; |
6829
50459a995aa3
renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents:
6301
diff
changeset
|
394 |
by (Blast_tac 1); |
50459a995aa3
renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents:
6301
diff
changeset
|
395 |
qed "image_UN"; |
50459a995aa3
renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents:
6301
diff
changeset
|
396 |
|
50459a995aa3
renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents:
6301
diff
changeset
|
397 |
(*injectivity's required. Left-to-right inclusion holds even if A is empty*) |
50459a995aa3
renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents:
6301
diff
changeset
|
398 |
Goalw [inj_on_def] |
50459a995aa3
renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents:
6301
diff
changeset
|
399 |
"[| inj_on f C; ALL x:A. B x <= C; j:A |] \ |
10832 | 400 |
\ ==> f ` (INTER A B) = (INT x:A. f ` B x)"; |
6829
50459a995aa3
renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents:
6301
diff
changeset
|
401 |
by (Blast_tac 1); |
50459a995aa3
renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents:
6301
diff
changeset
|
402 |
qed "image_INT"; |
50459a995aa3
renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents:
6301
diff
changeset
|
403 |
|
8309 | 404 |
(*Compare with image_INT: no use of inj_on, and if f is surjective then |
405 |
it doesn't matter whether A is empty*) |
|
10832 | 406 |
Goalw [bij_def] "bij f ==> f ` (INTER A B) = (INT x:A. f ` B x)"; |
8309 | 407 |
by (force_tac (claset() addSIs [surj_f_inv_f RS sym RS image_eqI], |
408 |
simpset()) 1); |
|
409 |
qed "bij_image_INT"; |
|
410 |
||
10832 | 411 |
Goal "bij f ==> f ` Collect P = {y. P (inv f y)}"; |
8309 | 412 |
by Auto_tac; |
413 |
by (force_tac (claset(), simpset() addsimps [bij_is_inj]) 1); |
|
414 |
by (blast_tac (claset() addIs [bij_is_surj RS surj_f_inv_f RS sym]) 1); |
|
415 |
qed "bij_image_Collect_eq"; |
|
416 |
||
10832 | 417 |
Goal "bij f ==> f -` A = inv f ` A"; |
8767 | 418 |
by Safe_tac; |
8309 | 419 |
by (asm_simp_tac (simpset() addsimps [bij_is_surj RS surj_f_inv_f]) 2); |
420 |
by (blast_tac (claset() addIs [bij_is_inj RS inv_f_f RS sym]) 1); |
|
421 |
qed "bij_vimage_eq_inv_image"; |
|
422 |
||
10832 | 423 |
Goal "surj f ==> -(f`A) <= f`(-A)"; |
10076
2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset
|
424 |
by (auto_tac (claset(), simpset() addsimps [surj_def])); |
2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset
|
425 |
qed "surj_Compl_image_subset"; |
2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset
|
426 |
|
10832 | 427 |
Goal "inj f ==> f`(-A) <= -(f`A)"; |
10076
2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset
|
428 |
by (auto_tac (claset(), simpset() addsimps [inj_on_def])); |
2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset
|
429 |
qed "inj_image_Compl_subset"; |
2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset
|
430 |
|
10832 | 431 |
Goalw [bij_def] "bij f ==> f`(-A) = -(f`A)"; |
10076
2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset
|
432 |
by (rtac equalityI 1); |
2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset
|
433 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [inj_image_Compl_subset, |
2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset
|
434 |
surj_Compl_image_subset]))); |
2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset
|
435 |
qed "bij_image_Compl_eq"; |
2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset
|
436 |
|
4089 | 437 |
val set_cs = claset() delrules [equalityI]; |
5305 | 438 |
|
439 |
||
440 |
section "fun_upd"; |
|
441 |
||
442 |
Goalw [fun_upd_def] "(f(x:=y) = f) = (f x = y)"; |
|
443 |
by Safe_tac; |
|
444 |
by (etac subst 1); |
|
445 |
by (rtac ext 2); |
|
446 |
by Auto_tac; |
|
447 |
qed "fun_upd_idem_iff"; |
|
448 |
||
449 |
(* f x = y ==> f(x:=y) = f *) |
|
450 |
bind_thm("fun_upd_idem", fun_upd_idem_iff RS iffD2); |
|
451 |
||
452 |
(* f(x := f x) = f *) |
|
453 |
AddIffs [refl RS fun_upd_idem]; |
|
454 |
||
455 |
Goal "(f(x:=y))z = (if z=x then y else f z)"; |
|
456 |
by (simp_tac (simpset() addsimps [fun_upd_def]) 1); |
|
457 |
qed "fun_upd_apply"; |
|
458 |
Addsimps [fun_upd_apply]; |
|
459 |
||
9339 | 460 |
(* fun_upd_apply supersedes these two, but they are useful |
461 |
if fun_upd_apply is intentionally removed from the simpset *) |
|
7089 | 462 |
Goal "(f(x:=y)) x = y"; |
463 |
by (Simp_tac 1); |
|
464 |
qed "fun_upd_same"; |
|
465 |
||
466 |
Goal "z~=x ==> (f(x:=y)) z = f z"; |
|
467 |
by (Asm_simp_tac 1); |
|
468 |
qed "fun_upd_other"; |
|
469 |
||
7445 | 470 |
Goal "f(x:=y,x:=z) = f(x:=z)"; |
471 |
by (rtac ext 1); |
|
472 |
by (Simp_tac 1); |
|
473 |
qed "fun_upd_upd"; |
|
474 |
Addsimps [fun_upd_upd]; |
|
5305 | 475 |
|
9339 | 476 |
(* simplifies terms of the form f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *) |
477 |
local |
|
478 |
fun gen_fun_upd None T _ _ = None |
|
479 |
| gen_fun_upd (Some f) T x y = Some (Const ("Fun.fun_upd",T) $ f $ x $ y) |
|
480 |
fun dest_fun_T1 (Type (_,T::Ts)) = T |
|
481 |
fun find_double (t as Const ("Fun.fun_upd",T) $ f $ x $ y) = let |
|
482 |
fun find (Const ("Fun.fun_upd",T) $ g $ v $ w) = |
|
483 |
if v aconv x then Some g else gen_fun_upd (find g) T v w |
|
484 |
| find t = None |
|
485 |
in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end |
|
9422 | 486 |
val ss = simpset (); |
9339 | 487 |
val fun_upd_prover = K [rtac eq_reflection 1, rtac ext 1, |
9422 | 488 |
simp_tac ss 1] |
9339 | 489 |
fun mk_eq_cterm sg T l r = Thm.cterm_of sg (equals T $ l $ r) |
490 |
in |
|
491 |
val fun_upd2_simproc = Simplifier.mk_simproc "fun_upd2" |
|
9422 | 492 |
[Thm.read_cterm (sign_of (the_context ())) ("f(v:=w,x:=y)", HOLogic.termT)] |
9339 | 493 |
(fn sg => (K (fn t => case find_double t of (T,None)=> None | (T,Some rhs)=> |
494 |
Some (prove_goalw_cterm [] (mk_eq_cterm sg T t rhs) fun_upd_prover)))) |
|
495 |
end; |
|
496 |
Addsimprocs[fun_upd2_simproc]; |
|
497 |
||
8258 | 498 |
Goal "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)"; |
5305 | 499 |
by (rtac ext 1); |
7089 | 500 |
by Auto_tac; |
5305 | 501 |
qed "fun_upd_twist"; |
5852 | 502 |
|
503 |
||
504 |
(*** -> and Pi, by Florian Kammueller and LCP ***) |
|
505 |
||
506 |
val prems = Goalw [Pi_def] |
|
507 |
"[| !!x. x: A ==> f x: B x; !!x. x ~: A ==> f(x) = (@ y. True)|] \ |
|
508 |
\ ==> f: Pi A B"; |
|
509 |
by (auto_tac (claset(), simpset() addsimps prems)); |
|
510 |
qed "Pi_I"; |
|
511 |
||
512 |
val prems = Goal |
|
513 |
"[| !!x. x: A ==> f x: B; !!x. x ~: A ==> f(x) = (@ y. True)|] ==> f: A funcset B"; |
|
514 |
by (blast_tac (claset() addIs Pi_I::prems) 1); |
|
515 |
qed "funcsetI"; |
|
516 |
||
517 |
Goalw [Pi_def] "[|f: Pi A B; x: A|] ==> f x: B x"; |
|
518 |
by Auto_tac; |
|
519 |
qed "Pi_mem"; |
|
520 |
||
521 |
Goalw [Pi_def] "[|f: A funcset B; x: A|] ==> f x: B"; |
|
522 |
by Auto_tac; |
|
523 |
qed "funcset_mem"; |
|
524 |
||
525 |
Goalw [Pi_def] "[|f: Pi A B; x~: A|] ==> f x = (@ y. True)"; |
|
526 |
by Auto_tac; |
|
527 |
qed "apply_arb"; |
|
528 |
||
529 |
Goalw [Pi_def] "[| f: Pi A B; g: Pi A B; ! x: A. f x = g x |] ==> f = g"; |
|
530 |
by (rtac ext 1); |
|
531 |
by Auto_tac; |
|
9108 | 532 |
bind_thm ("Pi_extensionality", ballI RSN (3, result())); |
5852 | 533 |
|
8138 | 534 |
|
5852 | 535 |
(*** compose ***) |
536 |
||
537 |
Goalw [Pi_def, compose_def, restrict_def] |
|
538 |
"[| f: A funcset B; g: B funcset C |]==> compose A g f: A funcset C"; |
|
539 |
by Auto_tac; |
|
540 |
qed "funcset_compose"; |
|
541 |
||
542 |
Goal "[| f: A funcset B; g: B funcset C; h: C funcset D |]\ |
|
543 |
\ ==> compose A h (compose A g f) = compose A (compose B h g) f"; |
|
544 |
by (res_inst_tac [("A","A")] Pi_extensionality 1); |
|
545 |
by (blast_tac (claset() addIs [funcset_compose]) 1); |
|
546 |
by (blast_tac (claset() addIs [funcset_compose]) 1); |
|
547 |
by (rewrite_goals_tac [Pi_def, compose_def, restrict_def]); |
|
548 |
by Auto_tac; |
|
549 |
qed "compose_assoc"; |
|
550 |
||
551 |
Goal "[| f: A funcset B; g: B funcset C; x: A |]==> compose A g f x = g(f(x))"; |
|
552 |
by (asm_full_simp_tac (simpset() addsimps [compose_def, restrict_def]) 1); |
|
553 |
qed "compose_eq"; |
|
554 |
||
10832 | 555 |
Goal "[| f : A funcset B; f ` A = B; g: B funcset C; g ` B = C |]\ |
556 |
\ ==> compose A g f ` A = C"; |
|
5852 | 557 |
by (auto_tac (claset(), |
558 |
simpset() addsimps [image_def, compose_eq])); |
|
559 |
qed "surj_compose"; |
|
560 |
||
10832 | 561 |
Goal "[| f : A funcset B; g: B funcset C; f ` A = B; inj_on f A; inj_on g B |]\ |
5852 | 562 |
\ ==> inj_on (compose A g f) A"; |
563 |
by (auto_tac (claset(), |
|
8081 | 564 |
simpset() addsimps [inj_on_def, compose_eq])); |
5852 | 565 |
qed "inj_on_compose"; |
566 |
||
567 |
||
568 |
(*** restrict / lam ***) |
|
8138 | 569 |
|
10832 | 570 |
Goal "f`A <= B ==> (lam x: A. f x) : A funcset B"; |
5852 | 571 |
by (auto_tac (claset(), |
572 |
simpset() addsimps [restrict_def, Pi_def])); |
|
573 |
qed "restrict_in_funcset"; |
|
574 |
||
575 |
val prems = Goalw [restrict_def, Pi_def] |
|
576 |
"(!!x. x: A ==> f x: B x) ==> (lam x: A. f x) : Pi A B"; |
|
577 |
by (asm_simp_tac (simpset() addsimps prems) 1); |
|
578 |
qed "restrictI"; |
|
579 |
||
580 |
Goal "x: A ==> (lam y: A. f y) x = f x"; |
|
581 |
by (asm_simp_tac (simpset() addsimps [restrict_def]) 1); |
|
582 |
qed "restrict_apply1"; |
|
583 |
||
584 |
Goal "[| x: A; f : A funcset B |] ==> (lam y: A. f y) x : B"; |
|
585 |
by (asm_full_simp_tac (simpset() addsimps [restrict_apply1,Pi_def]) 1); |
|
586 |
qed "restrict_apply1_mem"; |
|
587 |
||
588 |
Goal "x ~: A ==> (lam y: A. f y) x = (@ y. True)"; |
|
589 |
by (asm_simp_tac (simpset() addsimps [restrict_def]) 1); |
|
590 |
qed "restrict_apply2"; |
|
591 |
||
592 |
val prems = Goal |
|
593 |
"(!!x. x: A ==> f x = g x) ==> (lam x: A. f x) = (lam x: A. g x)"; |
|
594 |
by (rtac ext 1); |
|
595 |
by (auto_tac (claset(), |
|
596 |
simpset() addsimps prems@[restrict_def, Pi_def])); |
|
597 |
qed "restrict_ext"; |
|
598 |
||
8138 | 599 |
Goalw [inj_on_def, restrict_def] "inj_on (restrict f A) A = inj_on f A"; |
600 |
by Auto_tac; |
|
601 |
qed "inj_on_restrict_eq"; |
|
602 |
||
5852 | 603 |
|
604 |
(*** Inverse ***) |
|
605 |
||
10832 | 606 |
Goal "[|f ` A = B; x: B |] ==> ? y: A. f y = x"; |
5852 | 607 |
by (Blast_tac 1); |
608 |
qed "surj_image"; |
|
609 |
||
10832 | 610 |
Goalw [Inv_def] "[| f ` A = B; f : A funcset B |] \ |
5852 | 611 |
\ ==> (lam x: B. (Inv A f) x) : B funcset A"; |
9969 | 612 |
by (fast_tac (claset() addIs [restrict_in_funcset, someI2]) 1); |
5852 | 613 |
qed "Inv_funcset"; |
614 |
||
615 |
||
10832 | 616 |
Goal "[| f: A funcset B; inj_on f A; f ` A = B; x: A |] \ |
5852 | 617 |
\ ==> (lam y: B. (Inv A f) y) (f x) = x"; |
618 |
by (asm_simp_tac (simpset() addsimps [restrict_apply1, funcset_mem]) 1); |
|
8081 | 619 |
by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1); |
9969 | 620 |
by (rtac someI2 1); |
5852 | 621 |
by Auto_tac; |
622 |
qed "Inv_f_f"; |
|
623 |
||
10832 | 624 |
Goal "[| f: A funcset B; f ` A = B; x: B |] \ |
5852 | 625 |
\ ==> f ((lam y: B. (Inv A f y)) x) = x"; |
626 |
by (asm_simp_tac (simpset() addsimps [Inv_def, restrict_apply1]) 1); |
|
9969 | 627 |
by (fast_tac (claset() addIs [someI2]) 1); |
5852 | 628 |
qed "f_Inv_f"; |
629 |
||
10832 | 630 |
Goal "[| f: A funcset B; inj_on f A; f ` A = B |]\ |
5852 | 631 |
\ ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)"; |
632 |
by (rtac Pi_extensionality 1); |
|
633 |
by (blast_tac (claset() addIs [funcset_compose, Inv_funcset]) 1); |
|
634 |
by (blast_tac (claset() addIs [restrict_in_funcset]) 1); |
|
635 |
by (asm_simp_tac |
|
636 |
(simpset() addsimps [restrict_apply1, compose_def, Inv_f_f]) 1); |
|
637 |
qed "compose_Inv_id"; |
|
638 |
||
639 |
||
10826 | 640 |
(*** Pi ***) |
5852 | 641 |
|
642 |
Goalw [Pi_def] "[| B(x) = {}; x: A |] ==> (PI x: A. B x) = {}"; |
|
643 |
by Auto_tac; |
|
644 |
qed "Pi_eq_empty"; |
|
645 |
||
646 |
Goal "[| (PI x: A. B x) ~= {}; x: A |] ==> B(x) ~= {}"; |
|
647 |
by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1); |
|
648 |
qed "Pi_total1"; |
|
649 |
||
10826 | 650 |
Goal "Pi {} B = { %x. @y. True }"; |
5865
2303f5a3036d
moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents:
5852
diff
changeset
|
651 |
by (auto_tac (claset() addIs [ext], simpset() addsimps [Pi_def])); |
2303f5a3036d
moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents:
5852
diff
changeset
|
652 |
qed "Pi_empty"; |
5852 | 653 |
|
5865
2303f5a3036d
moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents:
5852
diff
changeset
|
654 |
val [major] = Goalw [Pi_def] "(!!x. x: A ==> B x <= C x) ==> Pi A B <= Pi A C"; |
2303f5a3036d
moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents:
5852
diff
changeset
|
655 |
by (auto_tac (claset(), |
2303f5a3036d
moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents:
5852
diff
changeset
|
656 |
simpset() addsimps [impOfSubs major])); |
2303f5a3036d
moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents:
5852
diff
changeset
|
657 |
qed "Pi_mono"; |