author  paulson 
Fri, 10 Sep 1999 18:37:04 +0200  
changeset 7536  5c094aec523d 
parent 7514  3235863a069a 
child 7876  1b3b683c092e 
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 

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 

7536  70 
Goal "f``g``A = (UN x:A. {f (g x)})"; 
71 
by (Blast_tac 1); 

72 
qed "image_image_eq_UN"; 

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 onetoone 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 onetoone 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 onetoone 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 idforms 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 

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

258 
qed "image_Int_subset"; 

259 

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

261 
by (Blast_tac 1); 

262 
qed "image_diff_subset"; 

263 

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

265 
"[ inj_on f C; A<=C; B<=C ] ==> f``(A Int B) = f``A Int f``B"; 
4059  266 
by (Blast_tac 1); 
4830  267 
qed "inj_on_image_Int"; 
4059  268 

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

270 
"[ inj_on f C; A<=C; B<=C ] ==> f``(AB) = f``A  f``B"; 
4059  271 
by (Blast_tac 1); 
4830  272 
qed "inj_on_image_set_diff"; 
4059  273 

6171  274 
Goalw [inj_on_def] "inj f ==> f``(A Int B) = f``A Int f``B"; 
4059  275 
by (Blast_tac 1); 
276 
qed "image_Int"; 

277 

6171  278 
Goalw [inj_on_def] "inj f ==> f``(AB) = f``A  f``B"; 
4059  279 
by (Blast_tac 1); 
280 
qed "image_set_diff"; 

281 

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

284 
qed "inv_image_comp"; 

5847  285 

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

288 
qed "inj_image_mem_iff"; 

289 

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

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

292 
qed "inj_image_eq_iff"; 

293 

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

294 
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

295 
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

296 
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

297 

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

298 
(*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

299 
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

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

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

302 
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

303 
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

304 

4089  305 
val set_cs = claset() delrules [equalityI]; 
5305  306 

307 

308 
section "fun_upd"; 

309 

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

311 
by Safe_tac; 

312 
by (etac subst 1); 

313 
by (rtac ext 2); 

314 
by Auto_tac; 

315 
qed "fun_upd_idem_iff"; 

316 

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

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

319 

320 
(* f(x := f x) = f *) 

321 
AddIffs [refl RS fun_upd_idem]; 

322 

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

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

325 
qed "fun_upd_apply"; 

326 
Addsimps [fun_upd_apply]; 

327 

7445  328 
(*fun_upd_apply supersedes these two*) 
7089  329 
Goal "(f(x:=y)) x = y"; 
330 
by (Simp_tac 1); 

331 
qed "fun_upd_same"; 

332 

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

334 
by (Asm_simp_tac 1); 

335 
qed "fun_upd_other"; 

336 

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

339 
by (Simp_tac 1); 

340 
qed "fun_upd_upd"; 

341 
Addsimps [fun_upd_upd]; 

5305  342 

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

344 
by (rtac ext 1); 

7089  345 
by Auto_tac; 
5305  346 
qed "fun_upd_twist"; 
5852  347 

348 

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

350 

351 
val prems = Goalw [Pi_def] 

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

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

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

355 
qed "Pi_I"; 

356 

357 
val prems = Goal 

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

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

360 
qed "funcsetI"; 

361 

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

363 
by Auto_tac; 

364 
qed "Pi_mem"; 

365 

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

367 
by Auto_tac; 

368 
qed "funcset_mem"; 

369 

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

371 
by Auto_tac; 

372 
qed "apply_arb"; 

373 

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

375 
by (rtac ext 1); 

376 
by Auto_tac; 

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

378 

379 
(*** compose ***) 

380 

381 
Goalw [Pi_def, compose_def, restrict_def] 

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

383 
by Auto_tac; 

384 
qed "funcset_compose"; 

385 

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

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

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

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

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

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

392 
by Auto_tac; 

393 
qed "compose_assoc"; 

394 

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

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

397 
qed "compose_eq"; 

398 

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

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

401 
by (auto_tac (claset(), 

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

403 
qed "surj_compose"; 

404 

405 

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

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

408 
by (auto_tac (claset(), 

409 
simpset() addsimps [inj_on_def, compose_eq])); 

410 
qed "inj_on_compose"; 

411 

412 

413 
(*** restrict / lam ***) 

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

415 
by (auto_tac (claset(), 

416 
simpset() addsimps [restrict_def, Pi_def])); 

417 
qed "restrict_in_funcset"; 

418 

419 
val prems = Goalw [restrict_def, Pi_def] 

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

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

422 
qed "restrictI"; 

423 

424 

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

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

427 
qed "restrict_apply1"; 

428 

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

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

431 
qed "restrict_apply1_mem"; 

432 

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

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

435 
qed "restrict_apply2"; 

436 

437 

438 
val prems = Goal 

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

440 
by (rtac ext 1); 

441 
by (auto_tac (claset(), 

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

443 
qed "restrict_ext"; 

444 

445 

446 
(*** Inverse ***) 

447 

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

449 
by (Blast_tac 1); 

450 
qed "surj_image"; 

451 

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

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

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

455 
qed "Inv_funcset"; 

456 

457 

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

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

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

461 
by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1); 

462 
by (rtac selectI2 1); 

463 
by Auto_tac; 

464 
qed "Inv_f_f"; 

465 

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

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

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

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

470 
qed "f_Inv_f"; 

471 

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

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

474 
by (rtac Pi_extensionality 1); 

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

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

477 
by (asm_simp_tac 

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

479 
qed "compose_Inv_id"; 

480 

481 

482 
(*** Pi and Applyall ***) 

483 

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

485 
by Auto_tac; 

486 
qed "Pi_eq_empty"; 

487 

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

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

490 
qed "Pi_total1"; 

491 

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

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

494 
by (rename_tac "g z" 1); 

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

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

497 
qed "Applyall_beta"; 

498 

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

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

500 
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

501 
qed "Pi_empty"; 
5852  502 

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

503 
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

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

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

506 
qed "Pi_mono"; 