author | berghofe |
Mon, 19 Jul 1999 17:21:40 +0200 | |
changeset 7047 | d103b875ef1d |
parent 7014 | 11ee650edcd2 |
child 7051 | 9b6bdced3dc6 |
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 |
|
5069 | 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 |
|
5608 | 36 |
qed_goalw "id_apply" thy [id_def] "id x = x" (K [rtac refl 1]); |
37 |
Addsimps [id_apply]; |
|
5441 | 38 |
|
39 |
||
5306 | 40 |
section "o"; |
41 |
||
42 |
qed_goalw "o_apply" thy [o_def] "(f o g) x = f (g x)" |
|
43 |
(K [rtac refl 1]); |
|
44 |
Addsimps [o_apply]; |
|
45 |
||
46 |
qed_goalw "o_assoc" thy [o_def] "f o (g o h) = f o g o h" |
|
47 |
(K [rtac ext 1, rtac refl 1]); |
|
48 |
||
5608 | 49 |
qed_goalw "id_o" thy [id_def] "id o g = g" |
5306 | 50 |
(K [rtac ext 1, Simp_tac 1]); |
5608 | 51 |
Addsimps [id_o]; |
5306 | 52 |
|
5608 | 53 |
qed_goalw "o_id" thy [id_def] "f o id = f" |
5306 | 54 |
(K [rtac ext 1, Simp_tac 1]); |
5608 | 55 |
Addsimps [o_id]; |
5306 | 56 |
|
57 |
Goalw [o_def] "(f o g)``r = f``(g``r)"; |
|
58 |
by (Blast_tac 1); |
|
59 |
qed "image_compose"; |
|
60 |
||
5852 | 61 |
Goalw [o_def] "UNION A (g o f) = UNION (f``A) g"; |
62 |
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
|
63 |
qed "UN_o"; |
5852 | 64 |
|
7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
65 |
(** lemma for proving injectivity of representation functions for **) |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
66 |
(** datatypes involving function types **) |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
67 |
|
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
68 |
Goalw [o_def] |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
69 |
"[| !x y. g (f x) = g y --> f x = y; g o f = g o fa |] ==> f = fa"; |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
70 |
br ext 1; |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
71 |
be allE 1; |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
72 |
be allE 1; |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
73 |
be mp 1; |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
74 |
be fun_cong 1; |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
75 |
qed "inj_fun_lemma"; |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
76 |
|
5306 | 77 |
|
78 |
section "inj"; |
|
6171 | 79 |
(**NB: inj now just translates to inj_on**) |
5306 | 80 |
|
923 | 81 |
(*** inj(f): f is a one-to-one function ***) |
82 |
||
6171 | 83 |
(*for Tools/datatype_rep_proofs*) |
84 |
val [prem] = Goalw [inj_on_def] |
|
85 |
"(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)"; |
|
86 |
by (blast_tac (claset() addIs [prem RS spec RS mp]) 1); |
|
87 |
qed "datatype_injI"; |
|
923 | 88 |
|
6171 | 89 |
Goalw [inj_on_def] "[| inj(f); f(x) = f(y) |] ==> x=y"; |
5316 | 90 |
by (Blast_tac 1); |
923 | 91 |
qed "injD"; |
92 |
||
93 |
(*Useful with the simplifier*) |
|
5316 | 94 |
Goal "inj(f) ==> (f(x) = f(y)) = (x=y)"; |
923 | 95 |
by (rtac iffI 1); |
5316 | 96 |
by (etac arg_cong 2); |
97 |
by (etac injD 1); |
|
5318 | 98 |
by (assume_tac 1); |
923 | 99 |
qed "inj_eq"; |
100 |
||
5316 | 101 |
Goal "inj(f) ==> (@x. f(x)=f(y)) = y"; |
102 |
by (etac injD 1); |
|
923 | 103 |
by (rtac selectI 1); |
104 |
by (rtac refl 1); |
|
105 |
qed "inj_select"; |
|
106 |
||
107 |
(*A one-to-one function has an inverse (given using select).*) |
|
5316 | 108 |
Goalw [inv_def] "inj(f) ==> inv f (f x) = x"; |
109 |
by (etac inj_select 1); |
|
2912 | 110 |
qed "inv_f_f"; |
923 | 111 |
|
6235 | 112 |
Addsimps [inv_f_f]; |
113 |
||
923 | 114 |
(* Useful??? *) |
5316 | 115 |
val [oneone,minor] = Goal |
2912 | 116 |
"[| inj(f); !!y. y: range(f) ==> P(inv f y) |] ==> P(x)"; |
117 |
by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1); |
|
923 | 118 |
by (rtac (rangeI RS minor) 1); |
119 |
qed "inj_transfer"; |
|
120 |
||
7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
121 |
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
|
122 |
by (rtac ext 1); |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
123 |
by (etac injD 1); |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
124 |
by (etac fun_cong 1); |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset
|
125 |
qed "inj_o"; |
923 | 126 |
|
4830 | 127 |
(*** inj_on f A: f is one-to-one over A ***) |
923 | 128 |
|
5316 | 129 |
val prems = Goalw [inj_on_def] |
4830 | 130 |
"(!! x y. [| f(x) = f(y); x:A; y:A |] ==> x=y) ==> inj_on f A"; |
4089 | 131 |
by (blast_tac (claset() addIs prems) 1); |
4830 | 132 |
qed "inj_onI"; |
6171 | 133 |
val injI = inj_onI; (*for compatibility*) |
923 | 134 |
|
5316 | 135 |
val [major] = Goal |
4830 | 136 |
"(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A"; |
137 |
by (rtac inj_onI 1); |
|
923 | 138 |
by (etac (apply_inverse RS trans) 1); |
139 |
by (REPEAT (eresolve_tac [asm_rl,major] 1)); |
|
4830 | 140 |
qed "inj_on_inverseI"; |
6171 | 141 |
val inj_inverseI = inj_on_inverseI; (*for compatibility*) |
923 | 142 |
|
5316 | 143 |
Goalw [inj_on_def] "[| inj_on f A; f(x)=f(y); x:A; y:A |] ==> x=y"; |
144 |
by (Blast_tac 1); |
|
4830 | 145 |
qed "inj_onD"; |
923 | 146 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
147 |
Goal "[| inj_on f A; x:A; y:A |] ==> (f(x)=f(y)) = (x=y)"; |
4830 | 148 |
by (blast_tac (claset() addSDs [inj_onD]) 1); |
149 |
qed "inj_on_iff"; |
|
923 | 150 |
|
5316 | 151 |
Goalw [inj_on_def] "[| inj_on f A; ~x=y; x:A; y:A |] ==> ~ f(x)=f(y)"; |
152 |
by (Blast_tac 1); |
|
4830 | 153 |
qed "inj_on_contraD"; |
923 | 154 |
|
5316 | 155 |
Goalw [inj_on_def] "[| A<=B; inj_on f B |] ==> inj_on f A"; |
3341 | 156 |
by (Blast_tac 1); |
4830 | 157 |
qed "subset_inj_on"; |
3341 | 158 |
|
923 | 159 |
|
6235 | 160 |
(** surj **) |
161 |
||
6267 | 162 |
val [prem] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g"; |
163 |
by (blast_tac (claset() addIs [prem RS sym]) 1); |
|
6235 | 164 |
qed "surjI"; |
165 |
||
166 |
Goalw [surj_def] "surj f ==> range f = UNIV"; |
|
167 |
by Auto_tac; |
|
168 |
qed "surj_range"; |
|
169 |
||
6267 | 170 |
Goalw [surj_def] "surj f ==> EX x. y = f x"; |
171 |
by (Blast_tac 1); |
|
172 |
qed "surjD"; |
|
173 |
||
6235 | 174 |
|
6171 | 175 |
(*** Lemmas about injective functions and inv ***) |
923 | 176 |
|
6171 | 177 |
Goalw [o_def] "[| inj_on f A; inj_on g (range f) |] ==> inj_on (g o f) A"; |
178 |
by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1); |
|
179 |
qed "comp_inj_on"; |
|
923 | 180 |
|
5316 | 181 |
Goalw [inv_def] "y : range(f) ==> f(inv f y) = y"; |
182 |
by (fast_tac (claset() addIs [selectI]) 1); |
|
2912 | 183 |
qed "f_inv_f"; |
923 | 184 |
|
6235 | 185 |
Goal "surj f ==> f(inv f y) = y"; |
186 |
by (asm_simp_tac (simpset() addsimps [f_inv_f, surj_range]) 1); |
|
187 |
qed "surj_f_inv_f"; |
|
188 |
||
6171 | 189 |
Goal "[| inv f x = inv f y; x: range(f); y: range(f) |] ==> x=y"; |
2912 | 190 |
by (rtac (arg_cong RS box_equals) 1); |
5316 | 191 |
by (REPEAT (ares_tac [f_inv_f] 1)); |
2912 | 192 |
qed "inv_injective"; |
193 |
||
6235 | 194 |
Goal "A <= range(f) ==> inj_on (inv f) A"; |
4830 | 195 |
by (fast_tac (claset() addIs [inj_onI] |
6235 | 196 |
addEs [inv_injective, injD]) 1); |
4830 | 197 |
qed "inj_on_inv"; |
923 | 198 |
|
6235 | 199 |
Goal "surj f ==> inj (inv f)"; |
200 |
by (asm_simp_tac (simpset() addsimps [inj_on_inv, surj_range]) 1); |
|
201 |
qed "surj_imp_inj_inv"; |
|
202 |
||
6290 | 203 |
Goal "f``(A Int B) <= f``A Int f``B"; |
204 |
by (Blast_tac 1); |
|
205 |
qed "image_Int_subset"; |
|
206 |
||
207 |
Goal "f``A - f``B <= f``(A - B)"; |
|
208 |
by (Blast_tac 1); |
|
209 |
qed "image_diff_subset"; |
|
210 |
||
5069 | 211 |
Goalw [inj_on_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
212 |
"[| inj_on f C; A<=C; B<=C |] ==> f``(A Int B) = f``A Int f``B"; |
4059 | 213 |
by (Blast_tac 1); |
4830 | 214 |
qed "inj_on_image_Int"; |
4059 | 215 |
|
5069 | 216 |
Goalw [inj_on_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
217 |
"[| inj_on f C; A<=C; B<=C |] ==> f``(A-B) = f``A - f``B"; |
4059 | 218 |
by (Blast_tac 1); |
4830 | 219 |
qed "inj_on_image_set_diff"; |
4059 | 220 |
|
6171 | 221 |
Goalw [inj_on_def] "inj f ==> f``(A Int B) = f``A Int f``B"; |
4059 | 222 |
by (Blast_tac 1); |
223 |
qed "image_Int"; |
|
224 |
||
6171 | 225 |
Goalw [inj_on_def] "inj f ==> f``(A-B) = f``A - f``B"; |
4059 | 226 |
by (Blast_tac 1); |
227 |
qed "image_set_diff"; |
|
228 |
||
6235 | 229 |
Goalw [image_def] "inj(f) ==> inv(f)``(f``X) = X"; |
230 |
by Auto_tac; |
|
231 |
qed "inv_image_comp"; |
|
5847 | 232 |
|
6301 | 233 |
Goal "inj f ==> (f a : f``A) = (a : A)"; |
234 |
by (blast_tac (claset() addDs [injD]) 1); |
|
235 |
qed "inj_image_mem_iff"; |
|
236 |
||
237 |
Goal "inj f ==> (f``A = f``B) = (A = B)"; |
|
238 |
by (blast_tac (claset() addSEs [equalityE] addDs [injD]) 1); |
|
239 |
qed "inj_image_eq_iff"; |
|
240 |
||
6829
50459a995aa3
renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents:
6301
diff
changeset
|
241 |
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
|
242 |
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
|
243 |
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
|
244 |
|
50459a995aa3
renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents:
6301
diff
changeset
|
245 |
(*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
|
246 |
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
|
247 |
"[| 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
|
248 |
\ ==> 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
|
249 |
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
|
250 |
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
|
251 |
|
4089 | 252 |
val set_cs = claset() delrules [equalityI]; |
5305 | 253 |
|
254 |
||
255 |
section "fun_upd"; |
|
256 |
||
257 |
Goalw [fun_upd_def] "(f(x:=y) = f) = (f x = y)"; |
|
258 |
by Safe_tac; |
|
259 |
by (etac subst 1); |
|
260 |
by (rtac ext 2); |
|
261 |
by Auto_tac; |
|
262 |
qed "fun_upd_idem_iff"; |
|
263 |
||
264 |
(* f x = y ==> f(x:=y) = f *) |
|
265 |
bind_thm("fun_upd_idem", fun_upd_idem_iff RS iffD2); |
|
266 |
||
267 |
(* f(x := f x) = f *) |
|
268 |
AddIffs [refl RS fun_upd_idem]; |
|
269 |
||
270 |
Goal "(f(x:=y))z = (if z=x then y else f z)"; |
|
271 |
by (simp_tac (simpset() addsimps [fun_upd_def]) 1); |
|
272 |
qed "fun_upd_apply"; |
|
273 |
Addsimps [fun_upd_apply]; |
|
274 |
||
275 |
qed_goal "fun_upd_same" thy "(f(x:=y)) x = y" |
|
276 |
(K [Simp_tac 1]); |
|
5306 | 277 |
qed_goal "fun_upd_other" thy "!!X. z~=x ==> (f(x:=y)) z = f z" |
5305 | 278 |
(K [Asm_simp_tac 1]); |
279 |
(*Addsimps [fun_upd_same, fun_upd_other];*) |
|
280 |
||
281 |
Goal "a ~= c ==> m(a:=b)(c:=d) = m(c:=d)(a:=b)"; |
|
282 |
by (rtac ext 1); |
|
283 |
by (Auto_tac); |
|
284 |
qed "fun_upd_twist"; |
|
5852 | 285 |
|
286 |
||
287 |
(*** -> and Pi, by Florian Kammueller and LCP ***) |
|
288 |
||
289 |
val prems = Goalw [Pi_def] |
|
290 |
"[| !!x. x: A ==> f x: B x; !!x. x ~: A ==> f(x) = (@ y. True)|] \ |
|
291 |
\ ==> f: Pi A B"; |
|
292 |
by (auto_tac (claset(), simpset() addsimps prems)); |
|
293 |
qed "Pi_I"; |
|
294 |
||
295 |
val prems = Goal |
|
296 |
"[| !!x. x: A ==> f x: B; !!x. x ~: A ==> f(x) = (@ y. True)|] ==> f: A funcset B"; |
|
297 |
by (blast_tac (claset() addIs Pi_I::prems) 1); |
|
298 |
qed "funcsetI"; |
|
299 |
||
300 |
Goalw [Pi_def] "[|f: Pi A B; x: A|] ==> f x: B x"; |
|
301 |
by Auto_tac; |
|
302 |
qed "Pi_mem"; |
|
303 |
||
304 |
Goalw [Pi_def] "[|f: A funcset B; x: A|] ==> f x: B"; |
|
305 |
by Auto_tac; |
|
306 |
qed "funcset_mem"; |
|
307 |
||
308 |
Goalw [Pi_def] "[|f: Pi A B; x~: A|] ==> f x = (@ y. True)"; |
|
309 |
by Auto_tac; |
|
310 |
qed "apply_arb"; |
|
311 |
||
312 |
Goalw [Pi_def] "[| f: Pi A B; g: Pi A B; ! x: A. f x = g x |] ==> f = g"; |
|
313 |
by (rtac ext 1); |
|
314 |
by Auto_tac; |
|
315 |
val Pi_extensionality = ballI RSN (3, result()); |
|
316 |
||
317 |
(*** compose ***) |
|
318 |
||
319 |
Goalw [Pi_def, compose_def, restrict_def] |
|
320 |
"[| f: A funcset B; g: B funcset C |]==> compose A g f: A funcset C"; |
|
321 |
by Auto_tac; |
|
322 |
qed "funcset_compose"; |
|
323 |
||
324 |
Goal "[| f: A funcset B; g: B funcset C; h: C funcset D |]\ |
|
325 |
\ ==> compose A h (compose A g f) = compose A (compose B h g) f"; |
|
326 |
by (res_inst_tac [("A","A")] Pi_extensionality 1); |
|
327 |
by (blast_tac (claset() addIs [funcset_compose]) 1); |
|
328 |
by (blast_tac (claset() addIs [funcset_compose]) 1); |
|
329 |
by (rewrite_goals_tac [Pi_def, compose_def, restrict_def]); |
|
330 |
by Auto_tac; |
|
331 |
qed "compose_assoc"; |
|
332 |
||
333 |
Goal "[| f: A funcset B; g: B funcset C; x: A |]==> compose A g f x = g(f(x))"; |
|
334 |
by (asm_full_simp_tac (simpset() addsimps [compose_def, restrict_def]) 1); |
|
335 |
qed "compose_eq"; |
|
336 |
||
337 |
Goal "[| f : A funcset B; f `` A = B; g: B funcset C; g `` B = C |]\ |
|
338 |
\ ==> compose A g f `` A = C"; |
|
339 |
by (auto_tac (claset(), |
|
340 |
simpset() addsimps [image_def, compose_eq])); |
|
341 |
qed "surj_compose"; |
|
342 |
||
343 |
||
344 |
Goal "[| f : A funcset B; g: B funcset C; f `` A = B; inj_on f A; inj_on g B |]\ |
|
345 |
\ ==> inj_on (compose A g f) A"; |
|
346 |
by (auto_tac (claset(), |
|
347 |
simpset() addsimps [inj_on_def, compose_eq])); |
|
348 |
qed "inj_on_compose"; |
|
349 |
||
350 |
||
351 |
(*** restrict / lam ***) |
|
352 |
Goal "[| f `` A <= B |] ==> (lam x: A. f x) : A funcset B"; |
|
353 |
by (auto_tac (claset(), |
|
354 |
simpset() addsimps [restrict_def, Pi_def])); |
|
355 |
qed "restrict_in_funcset"; |
|
356 |
||
357 |
val prems = Goalw [restrict_def, Pi_def] |
|
358 |
"(!!x. x: A ==> f x: B x) ==> (lam x: A. f x) : Pi A B"; |
|
359 |
by (asm_simp_tac (simpset() addsimps prems) 1); |
|
360 |
qed "restrictI"; |
|
361 |
||
362 |
||
363 |
Goal "x: A ==> (lam y: A. f y) x = f x"; |
|
364 |
by (asm_simp_tac (simpset() addsimps [restrict_def]) 1); |
|
365 |
qed "restrict_apply1"; |
|
366 |
||
367 |
Goal "[| x: A; f : A funcset B |] ==> (lam y: A. f y) x : B"; |
|
368 |
by (asm_full_simp_tac (simpset() addsimps [restrict_apply1,Pi_def]) 1); |
|
369 |
qed "restrict_apply1_mem"; |
|
370 |
||
371 |
Goal "x ~: A ==> (lam y: A. f y) x = (@ y. True)"; |
|
372 |
by (asm_simp_tac (simpset() addsimps [restrict_def]) 1); |
|
373 |
qed "restrict_apply2"; |
|
374 |
||
375 |
||
376 |
val prems = Goal |
|
377 |
"(!!x. x: A ==> f x = g x) ==> (lam x: A. f x) = (lam x: A. g x)"; |
|
378 |
by (rtac ext 1); |
|
379 |
by (auto_tac (claset(), |
|
380 |
simpset() addsimps prems@[restrict_def, Pi_def])); |
|
381 |
qed "restrict_ext"; |
|
382 |
||
383 |
||
384 |
(*** Inverse ***) |
|
385 |
||
386 |
Goal "[|f `` A = B; x: B |] ==> ? y: A. f y = x"; |
|
387 |
by (Blast_tac 1); |
|
388 |
qed "surj_image"; |
|
389 |
||
390 |
Goalw [Inv_def] "[| f `` A = B; f : A funcset B |] \ |
|
391 |
\ ==> (lam x: B. (Inv A f) x) : B funcset A"; |
|
392 |
by (fast_tac (claset() addIs [restrict_in_funcset, selectI2]) 1); |
|
393 |
qed "Inv_funcset"; |
|
394 |
||
395 |
||
396 |
Goal "[| f: A funcset B; inj_on f A; f `` A = B; x: A |] \ |
|
397 |
\ ==> (lam y: B. (Inv A f) y) (f x) = x"; |
|
398 |
by (asm_simp_tac (simpset() addsimps [restrict_apply1, funcset_mem]) 1); |
|
399 |
by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1); |
|
400 |
by (rtac selectI2 1); |
|
401 |
by Auto_tac; |
|
402 |
qed "Inv_f_f"; |
|
403 |
||
404 |
Goal "[| f: A funcset B; f `` A = B; x: B |] \ |
|
405 |
\ ==> f ((lam y: B. (Inv A f y)) x) = x"; |
|
406 |
by (asm_simp_tac (simpset() addsimps [Inv_def, restrict_apply1]) 1); |
|
407 |
by (fast_tac (claset() addIs [selectI2]) 1); |
|
408 |
qed "f_Inv_f"; |
|
409 |
||
410 |
Goal "[| f: A funcset B; inj_on f A; f `` A = B |]\ |
|
411 |
\ ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)"; |
|
412 |
by (rtac Pi_extensionality 1); |
|
413 |
by (blast_tac (claset() addIs [funcset_compose, Inv_funcset]) 1); |
|
414 |
by (blast_tac (claset() addIs [restrict_in_funcset]) 1); |
|
415 |
by (asm_simp_tac |
|
416 |
(simpset() addsimps [restrict_apply1, compose_def, Inv_f_f]) 1); |
|
417 |
qed "compose_Inv_id"; |
|
418 |
||
419 |
||
420 |
(*** Pi and Applyall ***) |
|
421 |
||
422 |
Goalw [Pi_def] "[| B(x) = {}; x: A |] ==> (PI x: A. B x) = {}"; |
|
423 |
by Auto_tac; |
|
424 |
qed "Pi_eq_empty"; |
|
425 |
||
426 |
Goal "[| (PI x: A. B x) ~= {}; x: A |] ==> B(x) ~= {}"; |
|
427 |
by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1); |
|
428 |
qed "Pi_total1"; |
|
429 |
||
430 |
Goal "[| a : A; Pi A B ~= {} |] ==> Applyall (Pi A B) a = B a"; |
|
431 |
by (auto_tac (claset(), simpset() addsimps [Applyall_def, Pi_def])); |
|
432 |
by (rename_tac "g z" 1); |
|
433 |
by (res_inst_tac [("x","%y. if (y = a) then z else g y")] exI 1); |
|
434 |
by (auto_tac (claset(), simpset() addsimps [split_if_mem1, split_if_eq1])); |
|
435 |
qed "Applyall_beta"; |
|
436 |
||
5865
2303f5a3036d
moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents:
5852
diff
changeset
|
437 |
Goal "Pi {} B = { (%x. @ y. True) }"; |
2303f5a3036d
moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents:
5852
diff
changeset
|
438 |
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
|
439 |
qed "Pi_empty"; |
5852 | 440 |
|
5865
2303f5a3036d
moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents:
5852
diff
changeset
|
441 |
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
|
442 |
by (auto_tac (claset(), |
2303f5a3036d
moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents:
5852
diff
changeset
|
443 |
simpset() addsimps [impOfSubs major])); |
2303f5a3036d
moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents:
5852
diff
changeset
|
444 |
qed "Pi_mono"; |