author  paulson 
Thu, 10 Feb 2000 11:08:42 +0100  
changeset 8226  07284f7ad262 
parent 8173  a9966d5ab84d 
child 8253  975eb12aa040 
permissions  rwrr 
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 

8226  41 
Goal "inv id = id"; 
42 
by (simp_tac (simpset() addsimps [inv_def,id_def]) 1); 

43 
qed "inv_id"; 

44 
Addsimps [inv_id]; 

45 

5441  46 

5306  47 
section "o"; 
48 

7089  49 
Goalw [o_def] "(f o g) x = f (g x)"; 
50 
by (rtac refl 1); 

51 
qed "o_apply"; 

5306  52 
Addsimps [o_apply]; 
53 

7089  54 
Goalw [o_def] "f o (g o h) = f o g o h"; 
55 
by (rtac ext 1); 

56 
by (rtac refl 1); 

57 
qed "o_assoc"; 

5306  58 

7089  59 
Goalw [id_def] "id o g = g"; 
60 
by (rtac ext 1); 

61 
by (Simp_tac 1); 

62 
qed "id_o"; 

5608  63 
Addsimps [id_o]; 
5306  64 

7089  65 
Goalw [id_def] "f o id = f"; 
66 
by (rtac ext 1); 

67 
by (Simp_tac 1); 

68 
qed "o_id"; 

5608  69 
Addsimps [o_id]; 
5306  70 

71 
Goalw [o_def] "(f o g)``r = f``(g``r)"; 

72 
by (Blast_tac 1); 

73 
qed "image_compose"; 

74 

7916  75 
Goal "f``A = (UN x:A. {f x})"; 
7536  76 
by (Blast_tac 1); 
7916  77 
qed "image_eq_UN"; 
7536  78 

5852  79 
Goalw [o_def] "UNION A (g o f) = UNION (f``A) g"; 
80 
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

81 
qed "UN_o"; 
5852  82 

7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset

83 
(** lemma for proving injectivity of representation functions for **) 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset

84 
(** datatypes involving function types **) 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset

85 

11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset

86 
Goalw [o_def] 
7089  87 
"[ ! x y. g (f x) = g y > f x = y; g o f = g o fa ] ==> f = fa"; 
88 
by (rtac ext 1); 

89 
by (etac allE 1); 

90 
by (etac allE 1); 

91 
by (etac mp 1); 

92 
by (etac fun_cong 1); 

7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset

93 
qed "inj_fun_lemma"; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset

94 

5306  95 

96 
section "inj"; 

6171  97 
(**NB: inj now just translates to inj_on**) 
5306  98 

923  99 
(*** inj(f): f is a onetoone function ***) 
100 

6171  101 
(*for Tools/datatype_rep_proofs*) 
102 
val [prem] = Goalw [inj_on_def] 

103 
"(!! x. ALL y. f(x) = f(y) > x=y) ==> inj(f)"; 

104 
by (blast_tac (claset() addIs [prem RS spec RS mp]) 1); 

105 
qed "datatype_injI"; 

923  106 

6171  107 
Goalw [inj_on_def] "[ inj(f); f(x) = f(y) ] ==> x=y"; 
5316  108 
by (Blast_tac 1); 
923  109 
qed "injD"; 
110 

111 
(*Useful with the simplifier*) 

5316  112 
Goal "inj(f) ==> (f(x) = f(y)) = (x=y)"; 
923  113 
by (rtac iffI 1); 
5316  114 
by (etac arg_cong 2); 
115 
by (etac injD 1); 

5318  116 
by (assume_tac 1); 
923  117 
qed "inj_eq"; 
118 

5316  119 
Goal "inj(f) ==> (@x. f(x)=f(y)) = y"; 
120 
by (etac injD 1); 

923  121 
by (rtac selectI 1); 
122 
by (rtac refl 1); 

123 
qed "inj_select"; 

124 

125 
(*A onetoone function has an inverse (given using select).*) 

5316  126 
Goalw [inv_def] "inj(f) ==> inv f (f x) = x"; 
127 
by (etac inj_select 1); 

2912  128 
qed "inv_f_f"; 
7338  129 
Addsimps [inv_f_f]; 
923  130 

7338  131 
Goal "[ inj(f); f x = y ] ==> inv f y = x"; 
132 
by (etac subst 1); 

133 
by (etac inv_f_f 1); 

134 
qed "inv_f_eq"; 

6235  135 

923  136 
(* Useful??? *) 
5316  137 
val [oneone,minor] = Goal 
2912  138 
"[ inj(f); !!y. y: range(f) ==> P(inv f y) ] ==> P(x)"; 
139 
by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1); 

923  140 
by (rtac (rangeI RS minor) 1); 
141 
qed "inj_transfer"; 

142 

7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset

143 
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

144 
by (rtac ext 1); 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset

145 
by (etac injD 1); 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset

146 
by (etac fun_cong 1); 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6829
diff
changeset

147 
qed "inj_o"; 
923  148 

4830  149 
(*** inj_on f A: f is onetoone over A ***) 
923  150 

5316  151 
val prems = Goalw [inj_on_def] 
4830  152 
"(!! x y. [ f(x) = f(y); x:A; y:A ] ==> x=y) ==> inj_on f A"; 
4089  153 
by (blast_tac (claset() addIs prems) 1); 
4830  154 
qed "inj_onI"; 
6171  155 
val injI = inj_onI; (*for compatibility*) 
923  156 

5316  157 
val [major] = Goal 
4830  158 
"(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A"; 
159 
by (rtac inj_onI 1); 

923  160 
by (etac (apply_inverse RS trans) 1); 
161 
by (REPEAT (eresolve_tac [asm_rl,major] 1)); 

4830  162 
qed "inj_on_inverseI"; 
6171  163 
val inj_inverseI = inj_on_inverseI; (*for compatibility*) 
923  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})"; 
178 
br injI 1; 

179 
be singleton_inject 1; 

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 

6235  201 

7374  202 
(** Bijections **) 
203 

204 
Goalw [bij_def] "[ inj f; surj f ] ==> bij f"; 

205 
by (Blast_tac 1); 

206 
qed "bijI"; 

207 

208 
Goalw [bij_def] "bij f ==> inj f"; 

209 
by (Blast_tac 1); 

210 
qed "bij_is_inj"; 

211 

212 
Goalw [bij_def] "bij f ==> surj f"; 

213 
by (Blast_tac 1); 

214 
qed "bij_is_surj"; 

215 

216 

6171  217 
(*** Lemmas about injective functions and inv ***) 
923  218 

7051  219 
Goalw [o_def] "[ inj_on f A; inj_on g (f``A) ] ==> inj_on (g o f) A"; 
6171  220 
by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1); 
221 
qed "comp_inj_on"; 

923  222 

5316  223 
Goalw [inv_def] "y : range(f) ==> f(inv f y) = y"; 
224 
by (fast_tac (claset() addIs [selectI]) 1); 

2912  225 
qed "f_inv_f"; 
923  226 

6235  227 
Goal "surj f ==> f(inv f y) = y"; 
228 
by (asm_simp_tac (simpset() addsimps [f_inv_f, surj_range]) 1); 

229 
qed "surj_f_inv_f"; 

230 

6171  231 
Goal "[ inv f x = inv f y; x: range(f); y: range(f) ] ==> x=y"; 
2912  232 
by (rtac (arg_cong RS box_equals) 1); 
5316  233 
by (REPEAT (ares_tac [f_inv_f] 1)); 
2912  234 
qed "inv_injective"; 
235 

6235  236 
Goal "A <= range(f) ==> inj_on (inv f) A"; 
4830  237 
by (fast_tac (claset() addIs [inj_onI] 
6235  238 
addEs [inv_injective, injD]) 1); 
4830  239 
qed "inj_on_inv"; 
923  240 

6235  241 
Goal "surj f ==> inj (inv f)"; 
242 
by (asm_simp_tac (simpset() addsimps [inj_on_inv, surj_range]) 1); 

243 
qed "surj_imp_inj_inv"; 

244 

7514  245 
(** We seem to need both the idforms and the (%x. x) forms; the latter can 
246 
arise by rewriting, while id may be used explicitly. **) 

247 

248 
Goal "(%x. x) `` Y = Y"; 

249 
by (Blast_tac 1); 

250 
qed "image_ident"; 

251 

252 
Goalw [id_def] "id `` Y = Y"; 

253 
by (Blast_tac 1); 

254 
qed "image_id"; 

255 
Addsimps [image_ident, image_id]; 

256 

257 
Goal "(%x. x) `` Y = Y"; 

258 
by (Blast_tac 1); 

259 
qed "vimage_ident"; 

260 

261 
Goalw [id_def] "id `` A = A"; 

262 
by Auto_tac; 

263 
qed "vimage_id"; 

264 
Addsimps [vimage_ident, vimage_id]; 

265 

7876  266 
Goal "f `` (f `` A) = {y. EX x:A. f x = f y}"; 
267 
by (blast_tac (claset() addIs [sym]) 1); 

268 
qed "vimage_image_eq"; 

269 

8173  270 
Goal "f `` (f `` A) <= A"; 
271 
by (Blast_tac 1); 

272 
qed "image_vimage_subset"; 

273 

274 
Goal "f `` (f `` A) = A Int range f"; 

275 
by (Blast_tac 1); 

276 
qed "image_vimage_eq"; 

277 
Addsimps [image_vimage_eq]; 

278 

279 
Goal "surj f ==> f `` (f `` A) = A"; 

280 
by (asm_simp_tac (simpset() addsimps [surj_range]) 1); 

281 
qed "surj_image_vimage_eq"; 

282 

283 
Goalw [inj_on_def] "inj f ==> f `` (f `` A) = A"; 

284 
by (Blast_tac 1); 

285 
qed "inj_vimage_image_eq"; 

286 

287 
Goalw [surj_def] "surj f ==> f `` B <= A ==> B <= f `` A"; 

288 
by (blast_tac (claset() addIs [sym]) 1); 

289 
qed "vimage_subsetD"; 

290 

291 
Goalw [inj_on_def] "inj f ==> B <= f `` A ==> f `` B <= A"; 

292 
by (Blast_tac 1); 

293 
qed "vimage_subsetI"; 

294 

295 
Goalw [bij_def] "bij f ==> (f `` B <= A) = (B <= f `` A)"; 

296 
by (blast_tac (claset() delrules [subsetI] 

297 
addIs [vimage_subsetI, vimage_subsetD]) 1); 

298 
qed "vimage_subset_eq"; 

299 

6290  300 
Goal "f``(A Int B) <= f``A Int f``B"; 
301 
by (Blast_tac 1); 

302 
qed "image_Int_subset"; 

303 

304 
Goal "f``A  f``B <= f``(A  B)"; 

305 
by (Blast_tac 1); 

306 
qed "image_diff_subset"; 

307 

5069  308 
Goalw [inj_on_def] 
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

309 
"[ inj_on f C; A<=C; B<=C ] ==> f``(A Int B) = f``A Int f``B"; 
4059  310 
by (Blast_tac 1); 
4830  311 
qed "inj_on_image_Int"; 
4059  312 

5069  313 
Goalw [inj_on_def] 
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

314 
"[ inj_on f C; A<=C; B<=C ] ==> f``(AB) = f``A  f``B"; 
4059  315 
by (Blast_tac 1); 
4830  316 
qed "inj_on_image_set_diff"; 
4059  317 

6171  318 
Goalw [inj_on_def] "inj f ==> f``(A Int B) = f``A Int f``B"; 
4059  319 
by (Blast_tac 1); 
320 
qed "image_Int"; 

321 

6171  322 
Goalw [inj_on_def] "inj f ==> f``(AB) = f``A  f``B"; 
4059  323 
by (Blast_tac 1); 
324 
qed "image_set_diff"; 

325 

6235  326 
Goalw [image_def] "inj(f) ==> inv(f)``(f``X) = X"; 
327 
by Auto_tac; 

328 
qed "inv_image_comp"; 

5847  329 

6301  330 
Goal "inj f ==> (f a : f``A) = (a : A)"; 
331 
by (blast_tac (claset() addDs [injD]) 1); 

332 
qed "inj_image_mem_iff"; 

333 

334 
Goal "inj f ==> (f``A = f``B) = (A = B)"; 

335 
by (blast_tac (claset() addSEs [equalityE] addDs [injD]) 1); 

336 
qed "inj_image_eq_iff"; 

337 

6829
50459a995aa3
renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents:
6301
diff
changeset

338 
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

339 
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

340 
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

341 

50459a995aa3
renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents:
6301
diff
changeset

342 
(*injectivity's required. Lefttoright 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

343 
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

344 
"[ 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

345 
\ ==> 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

346 
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

347 
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

348 

4089  349 
val set_cs = claset() delrules [equalityI]; 
5305  350 

351 

352 
section "fun_upd"; 

353 

354 
Goalw [fun_upd_def] "(f(x:=y) = f) = (f x = y)"; 

355 
by Safe_tac; 

356 
by (etac subst 1); 

357 
by (rtac ext 2); 

358 
by Auto_tac; 

359 
qed "fun_upd_idem_iff"; 

360 

361 
(* f x = y ==> f(x:=y) = f *) 

362 
bind_thm("fun_upd_idem", fun_upd_idem_iff RS iffD2); 

363 

364 
(* f(x := f x) = f *) 

365 
AddIffs [refl RS fun_upd_idem]; 

366 

367 
Goal "(f(x:=y))z = (if z=x then y else f z)"; 

368 
by (simp_tac (simpset() addsimps [fun_upd_def]) 1); 

369 
qed "fun_upd_apply"; 

370 
Addsimps [fun_upd_apply]; 

371 

7445  372 
(*fun_upd_apply supersedes these two*) 
7089  373 
Goal "(f(x:=y)) x = y"; 
374 
by (Simp_tac 1); 

375 
qed "fun_upd_same"; 

376 

377 
Goal "z~=x ==> (f(x:=y)) z = f z"; 

378 
by (Asm_simp_tac 1); 

379 
qed "fun_upd_other"; 

380 

7445  381 
Goal "f(x:=y,x:=z) = f(x:=z)"; 
382 
by (rtac ext 1); 

383 
by (Simp_tac 1); 

384 
qed "fun_upd_upd"; 

385 
Addsimps [fun_upd_upd]; 

5305  386 

387 
Goal "a ~= c ==> m(a:=b)(c:=d) = m(c:=d)(a:=b)"; 

388 
by (rtac ext 1); 

7089  389 
by Auto_tac; 
5305  390 
qed "fun_upd_twist"; 
5852  391 

392 

393 
(*** > and Pi, by Florian Kammueller and LCP ***) 

394 

395 
val prems = Goalw [Pi_def] 

396 
"[ !!x. x: A ==> f x: B x; !!x. x ~: A ==> f(x) = (@ y. True)] \ 

397 
\ ==> f: Pi A B"; 

398 
by (auto_tac (claset(), simpset() addsimps prems)); 

399 
qed "Pi_I"; 

400 

401 
val prems = Goal 

402 
"[ !!x. x: A ==> f x: B; !!x. x ~: A ==> f(x) = (@ y. True)] ==> f: A funcset B"; 

403 
by (blast_tac (claset() addIs Pi_I::prems) 1); 

404 
qed "funcsetI"; 

405 

406 
Goalw [Pi_def] "[f: Pi A B; x: A] ==> f x: B x"; 

407 
by Auto_tac; 

408 
qed "Pi_mem"; 

409 

410 
Goalw [Pi_def] "[f: A funcset B; x: A] ==> f x: B"; 

411 
by Auto_tac; 

412 
qed "funcset_mem"; 

413 

414 
Goalw [Pi_def] "[f: Pi A B; x~: A] ==> f x = (@ y. True)"; 

415 
by Auto_tac; 

416 
qed "apply_arb"; 

417 

418 
Goalw [Pi_def] "[ f: Pi A B; g: Pi A B; ! x: A. f x = g x ] ==> f = g"; 

419 
by (rtac ext 1); 

420 
by Auto_tac; 

421 
val Pi_extensionality = ballI RSN (3, result()); 

422 

8138  423 

5852  424 
(*** compose ***) 
425 

426 
Goalw [Pi_def, compose_def, restrict_def] 

427 
"[ f: A funcset B; g: B funcset C ]==> compose A g f: A funcset C"; 

428 
by Auto_tac; 

429 
qed "funcset_compose"; 

430 

431 
Goal "[ f: A funcset B; g: B funcset C; h: C funcset D ]\ 

432 
\ ==> compose A h (compose A g f) = compose A (compose B h g) f"; 

433 
by (res_inst_tac [("A","A")] Pi_extensionality 1); 

434 
by (blast_tac (claset() addIs [funcset_compose]) 1); 

435 
by (blast_tac (claset() addIs [funcset_compose]) 1); 

436 
by (rewrite_goals_tac [Pi_def, compose_def, restrict_def]); 

437 
by Auto_tac; 

438 
qed "compose_assoc"; 

439 

440 
Goal "[ f: A funcset B; g: B funcset C; x: A ]==> compose A g f x = g(f(x))"; 

441 
by (asm_full_simp_tac (simpset() addsimps [compose_def, restrict_def]) 1); 

442 
qed "compose_eq"; 

443 

444 
Goal "[ f : A funcset B; f `` A = B; g: B funcset C; g `` B = C ]\ 

445 
\ ==> compose A g f `` A = C"; 

446 
by (auto_tac (claset(), 

447 
simpset() addsimps [image_def, compose_eq])); 

448 
qed "surj_compose"; 

449 

450 
Goal "[ f : A funcset B; g: B funcset C; f `` A = B; inj_on f A; inj_on g B ]\ 

451 
\ ==> inj_on (compose A g f) A"; 

452 
by (auto_tac (claset(), 

8081  453 
simpset() addsimps [inj_on_def, compose_eq])); 
5852  454 
qed "inj_on_compose"; 
455 

456 

457 
(*** restrict / lam ***) 

8138  458 

459 
Goal "f``A <= B ==> (lam x: A. f x) : A funcset B"; 

5852  460 
by (auto_tac (claset(), 
461 
simpset() addsimps [restrict_def, Pi_def])); 

462 
qed "restrict_in_funcset"; 

463 

464 
val prems = Goalw [restrict_def, Pi_def] 

465 
"(!!x. x: A ==> f x: B x) ==> (lam x: A. f x) : Pi A B"; 

466 
by (asm_simp_tac (simpset() addsimps prems) 1); 

467 
qed "restrictI"; 

468 

469 
Goal "x: A ==> (lam y: A. f y) x = f x"; 

470 
by (asm_simp_tac (simpset() addsimps [restrict_def]) 1); 

471 
qed "restrict_apply1"; 

472 

473 
Goal "[ x: A; f : A funcset B ] ==> (lam y: A. f y) x : B"; 

474 
by (asm_full_simp_tac (simpset() addsimps [restrict_apply1,Pi_def]) 1); 

475 
qed "restrict_apply1_mem"; 

476 

477 
Goal "x ~: A ==> (lam y: A. f y) x = (@ y. True)"; 

478 
by (asm_simp_tac (simpset() addsimps [restrict_def]) 1); 

479 
qed "restrict_apply2"; 

480 

481 
val prems = Goal 

482 
"(!!x. x: A ==> f x = g x) ==> (lam x: A. f x) = (lam x: A. g x)"; 

483 
by (rtac ext 1); 

484 
by (auto_tac (claset(), 

485 
simpset() addsimps prems@[restrict_def, Pi_def])); 

486 
qed "restrict_ext"; 

487 

8138  488 
Goalw [inj_on_def, restrict_def] "inj_on (restrict f A) A = inj_on f A"; 
489 
by Auto_tac; 

490 
qed "inj_on_restrict_eq"; 

491 

5852  492 

493 
(*** Inverse ***) 

494 

495 
Goal "[f `` A = B; x: B ] ==> ? y: A. f y = x"; 

496 
by (Blast_tac 1); 

497 
qed "surj_image"; 

498 

499 
Goalw [Inv_def] "[ f `` A = B; f : A funcset B ] \ 

500 
\ ==> (lam x: B. (Inv A f) x) : B funcset A"; 

501 
by (fast_tac (claset() addIs [restrict_in_funcset, selectI2]) 1); 

502 
qed "Inv_funcset"; 

503 

504 

505 
Goal "[ f: A funcset B; inj_on f A; f `` A = B; x: A ] \ 

506 
\ ==> (lam y: B. (Inv A f) y) (f x) = x"; 

507 
by (asm_simp_tac (simpset() addsimps [restrict_apply1, funcset_mem]) 1); 

8081  508 
by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1); 
5852  509 
by (rtac selectI2 1); 
510 
by Auto_tac; 

511 
qed "Inv_f_f"; 

512 

513 
Goal "[ f: A funcset B; f `` A = B; x: B ] \ 

514 
\ ==> f ((lam y: B. (Inv A f y)) x) = x"; 

515 
by (asm_simp_tac (simpset() addsimps [Inv_def, restrict_apply1]) 1); 

516 
by (fast_tac (claset() addIs [selectI2]) 1); 

517 
qed "f_Inv_f"; 

518 

519 
Goal "[ f: A funcset B; inj_on f A; f `` A = B ]\ 

520 
\ ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)"; 

521 
by (rtac Pi_extensionality 1); 

522 
by (blast_tac (claset() addIs [funcset_compose, Inv_funcset]) 1); 

523 
by (blast_tac (claset() addIs [restrict_in_funcset]) 1); 

524 
by (asm_simp_tac 

525 
(simpset() addsimps [restrict_apply1, compose_def, Inv_f_f]) 1); 

526 
qed "compose_Inv_id"; 

527 

528 

529 
(*** Pi and Applyall ***) 

530 

531 
Goalw [Pi_def] "[ B(x) = {}; x: A ] ==> (PI x: A. B x) = {}"; 

532 
by Auto_tac; 

533 
qed "Pi_eq_empty"; 

534 

535 
Goal "[ (PI x: A. B x) ~= {}; x: A ] ==> B(x) ~= {}"; 

536 
by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1); 

537 
qed "Pi_total1"; 

538 

539 
Goal "[ a : A; Pi A B ~= {} ] ==> Applyall (Pi A B) a = B a"; 

540 
by (auto_tac (claset(), simpset() addsimps [Applyall_def, Pi_def])); 

541 
by (rename_tac "g z" 1); 

542 
by (res_inst_tac [("x","%y. if (y = a) then z else g y")] exI 1); 

543 
by (auto_tac (claset(), simpset() addsimps [split_if_mem1, split_if_eq1])); 

544 
qed "Applyall_beta"; 

545 

5865
2303f5a3036d
moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents:
5852
diff
changeset

546 
Goal "Pi {} B = { (%x. @ y. True) }"; 
2303f5a3036d
moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents:
5852
diff
changeset

547 
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

548 
qed "Pi_empty"; 
5852  549 

5865
2303f5a3036d
moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents:
5852
diff
changeset

550 
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

551 
by (auto_tac (claset(), 
2303f5a3036d
moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents:
5852
diff
changeset

552 
simpset() addsimps [impOfSubs major])); 
2303f5a3036d
moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents:
5852
diff
changeset

553 
qed "Pi_mono"; 