author | wenzelm |
Wed, 05 Jan 2000 11:58:18 +0100 | |
changeset 8102 | 424f6e663977 |
parent 8081 | 1c8de414b45d |
child 8138 | 1e4cb069b19d |
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 |
||
4656 | 9 |
|
7089 | 10 |
Goal "(f = g) = (! x. f(x)=g(x))"; |
923 | 11 |
by (rtac iffI 1); |
1264 | 12 |
by (Asm_simp_tac 1); |
13 |
by (rtac ext 1 THEN Asm_simp_tac 1); |
|
923 | 14 |
qed "expand_fun_eq"; |
15 |
||
5316 | 16 |
val prems = Goal |
923 | 17 |
"[| f(x)=u; !!x. P(x) ==> g(f(x)) = x; P(x) |] ==> x=g(u)"; |
18 |
by (rtac (arg_cong RS box_equals) 1); |
|
19 |
by (REPEAT (resolve_tac (prems@[refl]) 1)); |
|
20 |
qed "apply_inverse"; |
|
21 |
||
22 |
||
4656 | 23 |
(** "Axiom" of Choice, proved using the description operator **) |
24 |
||
5316 | 25 |
Goal "!!Q. ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)"; |
4656 | 26 |
by (fast_tac (claset() addEs [selectI]) 1); |
27 |
qed "choice"; |
|
28 |
||
5316 | 29 |
Goal "!!S. ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)"; |
4656 | 30 |
by (fast_tac (claset() addEs [selectI]) 1); |
31 |
qed "bchoice"; |
|
32 |
||
33 |
||
5608 | 34 |
section "id"; |
5441 | 35 |
|
7089 | 36 |
Goalw [id_def] "id x = x"; |
37 |
by (rtac refl 1); |
|
38 |
qed "id_apply"; |
|
5608 | 39 |
Addsimps [id_apply]; |
5441 | 40 |
|
41 |
||
5306 | 42 |
section "o"; |
43 |
||
7089 | 44 |
Goalw [o_def] "(f o g) x = f (g x)"; |
45 |
by (rtac refl 1); |
|
46 |
qed "o_apply"; |
|
5306 | 47 |
Addsimps [o_apply]; |
48 |
||
7089 | 49 |
Goalw [o_def] "f o (g o h) = f o g o h"; |
50 |
by (rtac ext 1); |
|
51 |
by (rtac refl 1); |
|
52 |
qed "o_assoc"; |
|
5306 | 53 |
|
7089 | 54 |
Goalw [id_def] "id o g = g"; |
55 |
by (rtac ext 1); |
|
56 |
by (Simp_tac 1); |
|
57 |
qed "id_o"; |
|
5608 | 58 |
Addsimps [id_o]; |
5306 | 59 |
|
7089 | 60 |
Goalw [id_def] "f o id = f"; |
61 |
by (rtac ext 1); |
|
62 |
by (Simp_tac 1); |
|
63 |
qed "o_id"; |
|
5608 | 64 |
Addsimps [o_id]; |
5306 | 65 |
|
66 |
Goalw [o_def] "(f o g)``r = f``(g``r)"; |
|
67 |
by (Blast_tac 1); |
|
68 |
qed "image_compose"; |
|
69 |
||
7916 | 70 |
Goal "f``A = (UN x:A. {f x})"; |
7536 | 71 |
by (Blast_tac 1); |
7916 | 72 |
qed "image_eq_UN"; |
7536 | 73 |
|
5852 | 74 |
Goalw [o_def] "UNION A (g o f) = UNION (f``A) g"; |
75 |
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
|
76 |
qed "UN_o"; |
5852 | 77 |
|
7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
78 |
(** lemma for proving injectivity of representation functions for **) |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
79 |
(** datatypes involving function types **) |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
80 |
|
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
81 |
Goalw [o_def] |
7089 | 82 |
"[| ! x y. g (f x) = g y --> f x = y; g o f = g o fa |] ==> f = fa"; |
83 |
by (rtac ext 1); |
|
84 |
by (etac allE 1); |
|
85 |
by (etac allE 1); |
|
86 |
by (etac mp 1); |
|
87 |
by (etac fun_cong 1); |
|
7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
88 |
qed "inj_fun_lemma"; |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
89 |
|
5306 | 90 |
|
91 |
section "inj"; |
|
6171 | 92 |
(**NB: inj now just translates to inj_on**) |
5306 | 93 |
|
923 | 94 |
(*** inj(f): f is a one-to-one function ***) |
95 |
||
6171 | 96 |
(*for Tools/datatype_rep_proofs*) |
97 |
val [prem] = Goalw [inj_on_def] |
|
98 |
"(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)"; |
|
99 |
by (blast_tac (claset() addIs [prem RS spec RS mp]) 1); |
|
100 |
qed "datatype_injI"; |
|
923 | 101 |
|
6171 | 102 |
Goalw [inj_on_def] "[| inj(f); f(x) = f(y) |] ==> x=y"; |
5316 | 103 |
by (Blast_tac 1); |
923 | 104 |
qed "injD"; |
105 |
||
106 |
(*Useful with the simplifier*) |
|
5316 | 107 |
Goal "inj(f) ==> (f(x) = f(y)) = (x=y)"; |
923 | 108 |
by (rtac iffI 1); |
5316 | 109 |
by (etac arg_cong 2); |
110 |
by (etac injD 1); |
|
5318 | 111 |
by (assume_tac 1); |
923 | 112 |
qed "inj_eq"; |
113 |
||
5316 | 114 |
Goal "inj(f) ==> (@x. f(x)=f(y)) = y"; |
115 |
by (etac injD 1); |
|
923 | 116 |
by (rtac selectI 1); |
117 |
by (rtac refl 1); |
|
118 |
qed "inj_select"; |
|
119 |
||
120 |
(*A one-to-one function has an inverse (given using select).*) |
|
5316 | 121 |
Goalw [inv_def] "inj(f) ==> inv f (f x) = x"; |
122 |
by (etac inj_select 1); |
|
2912 | 123 |
qed "inv_f_f"; |
7338 | 124 |
Addsimps [inv_f_f]; |
923 | 125 |
|
7338 | 126 |
Goal "[| inj(f); f x = y |] ==> inv f y = x"; |
127 |
by (etac subst 1); |
|
128 |
by (etac inv_f_f 1); |
|
129 |
qed "inv_f_eq"; |
|
6235 | 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"; |
6171 | 150 |
val 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"; |
6171 | 158 |
val inj_inverseI = inj_on_inverseI; (*for compatibility*) |
923 | 159 |
|
5316 | 160 |
Goalw [inj_on_def] "[| inj_on f A; f(x)=f(y); x:A; y:A |] ==> x=y"; |
161 |
by (Blast_tac 1); |
|
4830 | 162 |
qed "inj_onD"; |
923 | 163 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
164 |
Goal "[| inj_on f A; x:A; y:A |] ==> (f(x)=f(y)) = (x=y)"; |
4830 | 165 |
by (blast_tac (claset() addSDs [inj_onD]) 1); |
166 |
qed "inj_on_iff"; |
|
923 | 167 |
|
5316 | 168 |
Goalw [inj_on_def] "[| inj_on f A; ~x=y; x:A; y:A |] ==> ~ f(x)=f(y)"; |
169 |
by (Blast_tac 1); |
|
4830 | 170 |
qed "inj_on_contraD"; |
923 | 171 |
|
5316 | 172 |
Goalw [inj_on_def] "[| A<=B; inj_on f B |] ==> inj_on f A"; |
3341 | 173 |
by (Blast_tac 1); |
4830 | 174 |
qed "subset_inj_on"; |
3341 | 175 |
|
923 | 176 |
|
6235 | 177 |
(** surj **) |
178 |
||
6267 | 179 |
val [prem] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g"; |
180 |
by (blast_tac (claset() addIs [prem RS sym]) 1); |
|
6235 | 181 |
qed "surjI"; |
182 |
||
183 |
Goalw [surj_def] "surj f ==> range f = UNIV"; |
|
184 |
by Auto_tac; |
|
185 |
qed "surj_range"; |
|
186 |
||
6267 | 187 |
Goalw [surj_def] "surj f ==> EX x. y = f x"; |
188 |
by (Blast_tac 1); |
|
189 |
qed "surjD"; |
|
190 |
||
6235 | 191 |
|
7374 | 192 |
(** Bijections **) |
193 |
||
194 |
Goalw [bij_def] "[| inj f; surj f |] ==> bij f"; |
|
195 |
by (Blast_tac 1); |
|
196 |
qed "bijI"; |
|
197 |
||
198 |
Goalw [bij_def] "bij f ==> inj f"; |
|
199 |
by (Blast_tac 1); |
|
200 |
qed "bij_is_inj"; |
|
201 |
||
202 |
Goalw [bij_def] "bij f ==> surj f"; |
|
203 |
by (Blast_tac 1); |
|
204 |
qed "bij_is_surj"; |
|
205 |
||
206 |
||
6171 | 207 |
(*** Lemmas about injective functions and inv ***) |
923 | 208 |
|
7051 | 209 |
Goalw [o_def] "[| inj_on f A; inj_on g (f``A) |] ==> inj_on (g o f) A"; |
6171 | 210 |
by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1); |
211 |
qed "comp_inj_on"; |
|
923 | 212 |
|
5316 | 213 |
Goalw [inv_def] "y : range(f) ==> f(inv f y) = y"; |
214 |
by (fast_tac (claset() addIs [selectI]) 1); |
|
2912 | 215 |
qed "f_inv_f"; |
923 | 216 |
|
6235 | 217 |
Goal "surj f ==> f(inv f y) = y"; |
218 |
by (asm_simp_tac (simpset() addsimps [f_inv_f, surj_range]) 1); |
|
219 |
qed "surj_f_inv_f"; |
|
220 |
||
6171 | 221 |
Goal "[| inv f x = inv f y; x: range(f); y: range(f) |] ==> x=y"; |
2912 | 222 |
by (rtac (arg_cong RS box_equals) 1); |
5316 | 223 |
by (REPEAT (ares_tac [f_inv_f] 1)); |
2912 | 224 |
qed "inv_injective"; |
225 |
||
6235 | 226 |
Goal "A <= range(f) ==> inj_on (inv f) A"; |
4830 | 227 |
by (fast_tac (claset() addIs [inj_onI] |
6235 | 228 |
addEs [inv_injective, injD]) 1); |
4830 | 229 |
qed "inj_on_inv"; |
923 | 230 |
|
6235 | 231 |
Goal "surj f ==> inj (inv f)"; |
232 |
by (asm_simp_tac (simpset() addsimps [inj_on_inv, surj_range]) 1); |
|
233 |
qed "surj_imp_inj_inv"; |
|
234 |
||
7514 | 235 |
(** We seem to need both the id-forms and the (%x. x) forms; the latter can |
236 |
arise by rewriting, while id may be used explicitly. **) |
|
237 |
||
238 |
Goal "(%x. x) `` Y = Y"; |
|
239 |
by (Blast_tac 1); |
|
240 |
qed "image_ident"; |
|
241 |
||
242 |
Goalw [id_def] "id `` Y = Y"; |
|
243 |
by (Blast_tac 1); |
|
244 |
qed "image_id"; |
|
245 |
Addsimps [image_ident, image_id]; |
|
246 |
||
247 |
Goal "(%x. x) -`` Y = Y"; |
|
248 |
by (Blast_tac 1); |
|
249 |
qed "vimage_ident"; |
|
250 |
||
251 |
Goalw [id_def] "id -`` A = A"; |
|
252 |
by Auto_tac; |
|
253 |
qed "vimage_id"; |
|
254 |
Addsimps [vimage_ident, vimage_id]; |
|
255 |
||
7876 | 256 |
Goal "f -`` (f `` A) = {y. EX x:A. f x = f y}"; |
257 |
by (blast_tac (claset() addIs [sym]) 1); |
|
258 |
qed "vimage_image_eq"; |
|
259 |
||
6290 | 260 |
Goal "f``(A Int B) <= f``A Int f``B"; |
261 |
by (Blast_tac 1); |
|
262 |
qed "image_Int_subset"; |
|
263 |
||
264 |
Goal "f``A - f``B <= f``(A - B)"; |
|
265 |
by (Blast_tac 1); |
|
266 |
qed "image_diff_subset"; |
|
267 |
||
5069 | 268 |
Goalw [inj_on_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
269 |
"[| inj_on f C; A<=C; B<=C |] ==> f``(A Int B) = f``A Int f``B"; |
4059 | 270 |
by (Blast_tac 1); |
4830 | 271 |
qed "inj_on_image_Int"; |
4059 | 272 |
|
5069 | 273 |
Goalw [inj_on_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
274 |
"[| inj_on f C; A<=C; B<=C |] ==> f``(A-B) = f``A - f``B"; |
4059 | 275 |
by (Blast_tac 1); |
4830 | 276 |
qed "inj_on_image_set_diff"; |
4059 | 277 |
|
6171 | 278 |
Goalw [inj_on_def] "inj f ==> f``(A Int B) = f``A Int f``B"; |
4059 | 279 |
by (Blast_tac 1); |
280 |
qed "image_Int"; |
|
281 |
||
6171 | 282 |
Goalw [inj_on_def] "inj f ==> f``(A-B) = f``A - f``B"; |
4059 | 283 |
by (Blast_tac 1); |
284 |
qed "image_set_diff"; |
|
285 |
||
6235 | 286 |
Goalw [image_def] "inj(f) ==> inv(f)``(f``X) = X"; |
287 |
by Auto_tac; |
|
288 |
qed "inv_image_comp"; |
|
5847 | 289 |
|
6301 | 290 |
Goal "inj f ==> (f a : f``A) = (a : A)"; |
291 |
by (blast_tac (claset() addDs [injD]) 1); |
|
292 |
qed "inj_image_mem_iff"; |
|
293 |
||
294 |
Goal "inj f ==> (f``A = f``B) = (A = B)"; |
|
295 |
by (blast_tac (claset() addSEs [equalityE] addDs [injD]) 1); |
|
296 |
qed "inj_image_eq_iff"; |
|
297 |
||
6829
50459a995aa3
renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents:
6301
diff
changeset
|
298 |
Goal "(f `` (UNION A B)) = (UN x:A.(f `` (B x)))"; |
50459a995aa3
renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents:
6301
diff
changeset
|
299 |
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
|
300 |
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
|
301 |
|
50459a995aa3
renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents:
6301
diff
changeset
|
302 |
(*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
|
303 |
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
|
304 |
"[| inj_on f C; ALL x:A. B x <= C; j:A |] \ |
50459a995aa3
renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents:
6301
diff
changeset
|
305 |
\ ==> f `` (INTER A B) = (INT x:A. f `` B x)"; |
50459a995aa3
renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents:
6301
diff
changeset
|
306 |
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
|
307 |
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
|
308 |
|
4089 | 309 |
val set_cs = claset() delrules [equalityI]; |
5305 | 310 |
|
311 |
||
312 |
section "fun_upd"; |
|
313 |
||
314 |
Goalw [fun_upd_def] "(f(x:=y) = f) = (f x = y)"; |
|
315 |
by Safe_tac; |
|
316 |
by (etac subst 1); |
|
317 |
by (rtac ext 2); |
|
318 |
by Auto_tac; |
|
319 |
qed "fun_upd_idem_iff"; |
|
320 |
||
321 |
(* f x = y ==> f(x:=y) = f *) |
|
322 |
bind_thm("fun_upd_idem", fun_upd_idem_iff RS iffD2); |
|
323 |
||
324 |
(* f(x := f x) = f *) |
|
325 |
AddIffs [refl RS fun_upd_idem]; |
|
326 |
||
327 |
Goal "(f(x:=y))z = (if z=x then y else f z)"; |
|
328 |
by (simp_tac (simpset() addsimps [fun_upd_def]) 1); |
|
329 |
qed "fun_upd_apply"; |
|
330 |
Addsimps [fun_upd_apply]; |
|
331 |
||
7445 | 332 |
(*fun_upd_apply supersedes these two*) |
7089 | 333 |
Goal "(f(x:=y)) x = y"; |
334 |
by (Simp_tac 1); |
|
335 |
qed "fun_upd_same"; |
|
336 |
||
337 |
Goal "z~=x ==> (f(x:=y)) z = f z"; |
|
338 |
by (Asm_simp_tac 1); |
|
339 |
qed "fun_upd_other"; |
|
340 |
||
7445 | 341 |
Goal "f(x:=y,x:=z) = f(x:=z)"; |
342 |
by (rtac ext 1); |
|
343 |
by (Simp_tac 1); |
|
344 |
qed "fun_upd_upd"; |
|
345 |
Addsimps [fun_upd_upd]; |
|
5305 | 346 |
|
347 |
Goal "a ~= c ==> m(a:=b)(c:=d) = m(c:=d)(a:=b)"; |
|
348 |
by (rtac ext 1); |
|
7089 | 349 |
by Auto_tac; |
5305 | 350 |
qed "fun_upd_twist"; |
5852 | 351 |
|
352 |
||
353 |
(*** -> and Pi, by Florian Kammueller and LCP ***) |
|
354 |
||
355 |
val prems = Goalw [Pi_def] |
|
356 |
"[| !!x. x: A ==> f x: B x; !!x. x ~: A ==> f(x) = (@ y. True)|] \ |
|
357 |
\ ==> f: Pi A B"; |
|
358 |
by (auto_tac (claset(), simpset() addsimps prems)); |
|
359 |
qed "Pi_I"; |
|
360 |
||
361 |
val prems = Goal |
|
362 |
"[| !!x. x: A ==> f x: B; !!x. x ~: A ==> f(x) = (@ y. True)|] ==> f: A funcset B"; |
|
363 |
by (blast_tac (claset() addIs Pi_I::prems) 1); |
|
364 |
qed "funcsetI"; |
|
365 |
||
366 |
Goalw [Pi_def] "[|f: Pi A B; x: A|] ==> f x: B x"; |
|
367 |
by Auto_tac; |
|
368 |
qed "Pi_mem"; |
|
369 |
||
370 |
Goalw [Pi_def] "[|f: A funcset B; x: A|] ==> f x: B"; |
|
371 |
by Auto_tac; |
|
372 |
qed "funcset_mem"; |
|
373 |
||
374 |
Goalw [Pi_def] "[|f: Pi A B; x~: A|] ==> f x = (@ y. True)"; |
|
375 |
by Auto_tac; |
|
376 |
qed "apply_arb"; |
|
377 |
||
378 |
Goalw [Pi_def] "[| f: Pi A B; g: Pi A B; ! x: A. f x = g x |] ==> f = g"; |
|
379 |
by (rtac ext 1); |
|
380 |
by Auto_tac; |
|
381 |
val Pi_extensionality = ballI RSN (3, result()); |
|
382 |
||
383 |
(*** compose ***) |
|
384 |
||
385 |
Goalw [Pi_def, compose_def, restrict_def] |
|
386 |
"[| f: A funcset B; g: B funcset C |]==> compose A g f: A funcset C"; |
|
387 |
by Auto_tac; |
|
388 |
qed "funcset_compose"; |
|
389 |
||
390 |
Goal "[| f: A funcset B; g: B funcset C; h: C funcset D |]\ |
|
391 |
\ ==> compose A h (compose A g f) = compose A (compose B h g) f"; |
|
392 |
by (res_inst_tac [("A","A")] Pi_extensionality 1); |
|
393 |
by (blast_tac (claset() addIs [funcset_compose]) 1); |
|
394 |
by (blast_tac (claset() addIs [funcset_compose]) 1); |
|
395 |
by (rewrite_goals_tac [Pi_def, compose_def, restrict_def]); |
|
396 |
by Auto_tac; |
|
397 |
qed "compose_assoc"; |
|
398 |
||
399 |
Goal "[| f: A funcset B; g: B funcset C; x: A |]==> compose A g f x = g(f(x))"; |
|
400 |
by (asm_full_simp_tac (simpset() addsimps [compose_def, restrict_def]) 1); |
|
401 |
qed "compose_eq"; |
|
402 |
||
403 |
Goal "[| f : A funcset B; f `` A = B; g: B funcset C; g `` B = C |]\ |
|
404 |
\ ==> compose A g f `` A = C"; |
|
405 |
by (auto_tac (claset(), |
|
406 |
simpset() addsimps [image_def, compose_eq])); |
|
407 |
qed "surj_compose"; |
|
408 |
||
409 |
||
410 |
Goal "[| f : A funcset B; g: B funcset C; f `` A = B; inj_on f A; inj_on g B |]\ |
|
411 |
\ ==> inj_on (compose A g f) A"; |
|
412 |
by (auto_tac (claset(), |
|
8081 | 413 |
simpset() addsimps [inj_on_def, compose_eq])); |
5852 | 414 |
qed "inj_on_compose"; |
415 |
||
416 |
||
417 |
(*** restrict / lam ***) |
|
418 |
Goal "[| f `` A <= B |] ==> (lam x: A. f x) : A funcset B"; |
|
419 |
by (auto_tac (claset(), |
|
420 |
simpset() addsimps [restrict_def, Pi_def])); |
|
421 |
qed "restrict_in_funcset"; |
|
422 |
||
423 |
val prems = Goalw [restrict_def, Pi_def] |
|
424 |
"(!!x. x: A ==> f x: B x) ==> (lam x: A. f x) : Pi A B"; |
|
425 |
by (asm_simp_tac (simpset() addsimps prems) 1); |
|
426 |
qed "restrictI"; |
|
427 |
||
428 |
||
429 |
Goal "x: A ==> (lam y: A. f y) x = f x"; |
|
430 |
by (asm_simp_tac (simpset() addsimps [restrict_def]) 1); |
|
431 |
qed "restrict_apply1"; |
|
432 |
||
433 |
Goal "[| x: A; f : A funcset B |] ==> (lam y: A. f y) x : B"; |
|
434 |
by (asm_full_simp_tac (simpset() addsimps [restrict_apply1,Pi_def]) 1); |
|
435 |
qed "restrict_apply1_mem"; |
|
436 |
||
437 |
Goal "x ~: A ==> (lam y: A. f y) x = (@ y. True)"; |
|
438 |
by (asm_simp_tac (simpset() addsimps [restrict_def]) 1); |
|
439 |
qed "restrict_apply2"; |
|
440 |
||
441 |
||
442 |
val prems = Goal |
|
443 |
"(!!x. x: A ==> f x = g x) ==> (lam x: A. f x) = (lam x: A. g x)"; |
|
444 |
by (rtac ext 1); |
|
445 |
by (auto_tac (claset(), |
|
446 |
simpset() addsimps prems@[restrict_def, Pi_def])); |
|
447 |
qed "restrict_ext"; |
|
448 |
||
449 |
||
450 |
(*** Inverse ***) |
|
451 |
||
452 |
Goal "[|f `` A = B; x: B |] ==> ? y: A. f y = x"; |
|
453 |
by (Blast_tac 1); |
|
454 |
qed "surj_image"; |
|
455 |
||
456 |
Goalw [Inv_def] "[| f `` A = B; f : A funcset B |] \ |
|
457 |
\ ==> (lam x: B. (Inv A f) x) : B funcset A"; |
|
458 |
by (fast_tac (claset() addIs [restrict_in_funcset, selectI2]) 1); |
|
459 |
qed "Inv_funcset"; |
|
460 |
||
461 |
||
462 |
Goal "[| f: A funcset B; inj_on f A; f `` A = B; x: A |] \ |
|
463 |
\ ==> (lam y: B. (Inv A f) y) (f x) = x"; |
|
464 |
by (asm_simp_tac (simpset() addsimps [restrict_apply1, funcset_mem]) 1); |
|
8081 | 465 |
by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1); |
5852 | 466 |
by (rtac selectI2 1); |
467 |
by Auto_tac; |
|
468 |
qed "Inv_f_f"; |
|
469 |
||
470 |
Goal "[| f: A funcset B; f `` A = B; x: B |] \ |
|
471 |
\ ==> f ((lam y: B. (Inv A f y)) x) = x"; |
|
472 |
by (asm_simp_tac (simpset() addsimps [Inv_def, restrict_apply1]) 1); |
|
473 |
by (fast_tac (claset() addIs [selectI2]) 1); |
|
474 |
qed "f_Inv_f"; |
|
475 |
||
476 |
Goal "[| f: A funcset B; inj_on f A; f `` A = B |]\ |
|
477 |
\ ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)"; |
|
478 |
by (rtac Pi_extensionality 1); |
|
479 |
by (blast_tac (claset() addIs [funcset_compose, Inv_funcset]) 1); |
|
480 |
by (blast_tac (claset() addIs [restrict_in_funcset]) 1); |
|
481 |
by (asm_simp_tac |
|
482 |
(simpset() addsimps [restrict_apply1, compose_def, Inv_f_f]) 1); |
|
483 |
qed "compose_Inv_id"; |
|
484 |
||
485 |
||
486 |
(*** Pi and Applyall ***) |
|
487 |
||
488 |
Goalw [Pi_def] "[| B(x) = {}; x: A |] ==> (PI x: A. B x) = {}"; |
|
489 |
by Auto_tac; |
|
490 |
qed "Pi_eq_empty"; |
|
491 |
||
492 |
Goal "[| (PI x: A. B x) ~= {}; x: A |] ==> B(x) ~= {}"; |
|
493 |
by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1); |
|
494 |
qed "Pi_total1"; |
|
495 |
||
496 |
Goal "[| a : A; Pi A B ~= {} |] ==> Applyall (Pi A B) a = B a"; |
|
497 |
by (auto_tac (claset(), simpset() addsimps [Applyall_def, Pi_def])); |
|
498 |
by (rename_tac "g z" 1); |
|
499 |
by (res_inst_tac [("x","%y. if (y = a) then z else g y")] exI 1); |
|
500 |
by (auto_tac (claset(), simpset() addsimps [split_if_mem1, split_if_eq1])); |
|
501 |
qed "Applyall_beta"; |
|
502 |
||
5865
2303f5a3036d
moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents:
5852
diff
changeset
|
503 |
Goal "Pi {} B = { (%x. @ y. True) }"; |
2303f5a3036d
moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents:
5852
diff
changeset
|
504 |
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
|
505 |
qed "Pi_empty"; |
5852 | 506 |
|
5865
2303f5a3036d
moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents:
5852
diff
changeset
|
507 |
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
|
508 |
by (auto_tac (claset(), |
2303f5a3036d
moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents:
5852
diff
changeset
|
509 |
simpset() addsimps [impOfSubs major])); |
2303f5a3036d
moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents:
5852
diff
changeset
|
510 |
qed "Pi_mono"; |