author  nipkow 
Wed, 21 Jul 1999 11:34:59 +0200  
changeset 7051  9b6bdced3dc6 
parent 7014  11ee650edcd2 
child 7089  9bfb8e218b99 
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 

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

7051  177 
Goalw [o_def] "[ inj_on f A; inj_on g (f``A) ] ==> inj_on (g o f) A"; 
6171  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``(AB) = 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``(AB) = 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. 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

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"; 