author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 10076  2683ff181047 
child 10826  f3b7201dda27 
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 

7089  9 
Goal "(f = g) = (! x. f(x)=g(x))"; 
923  10 
by (rtac iffI 1); 
1264  11 
by (Asm_simp_tac 1); 
12 
by (rtac ext 1 THEN Asm_simp_tac 1); 

923  13 
qed "expand_fun_eq"; 
14 

5316  15 
val prems = Goal 
923  16 
"[ f(x)=u; !!x. P(x) ==> g(f(x)) = x; P(x) ] ==> x=g(u)"; 
17 
by (rtac (arg_cong RS box_equals) 1); 

18 
by (REPEAT (resolve_tac (prems@[refl]) 1)); 

19 
qed "apply_inverse"; 

20 

21 

4656  22 
(** "Axiom" of Choice, proved using the description operator **) 
23 

9838  24 
(*"choice" is now proved in Tools/meson.ML*) 
4656  25 

5316  26 
Goal "!!S. ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)"; 
9970  27 
by (fast_tac (claset() addEs [someI]) 1); 
4656  28 
qed "bchoice"; 
29 

30 

5608  31 
section "id"; 
5441  32 

7089  33 
Goalw [id_def] "id x = x"; 
34 
by (rtac refl 1); 

35 
qed "id_apply"; 

5608  36 
Addsimps [id_apply]; 
5441  37 

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

40 
qed "inv_id"; 

41 
Addsimps [inv_id]; 

42 

5441  43 

5306  44 
section "o"; 
45 

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

48 
qed "o_apply"; 

5306  49 
Addsimps [o_apply]; 
50 

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

53 
by (rtac refl 1); 

54 
qed "o_assoc"; 

5306  55 

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

58 
by (Simp_tac 1); 

59 
qed "id_o"; 

5608  60 
Addsimps [id_o]; 
5306  61 

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

64 
by (Simp_tac 1); 

65 
qed "o_id"; 

5608  66 
Addsimps [o_id]; 
5306  67 

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

69 
by (Blast_tac 1); 

70 
qed "image_compose"; 

71 

7916  72 
Goal "f``A = (UN x:A. {f x})"; 
7536  73 
by (Blast_tac 1); 
7916  74 
qed "image_eq_UN"; 
7536  75 

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

78 
qed "UN_o"; 
5852  79 

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

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

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

82 

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

83 
Goalw [o_def] 
7089  84 
"[ ! x y. g (f x) = g y > f x = y; g o f = g o fa ] ==> f = fa"; 
85 
by (rtac ext 1); 

86 
by (etac allE 1); 

87 
by (etac allE 1); 

88 
by (etac mp 1); 

89 
by (etac fun_cong 1); 

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

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

91 

5306  92 

93 
section "inj"; 

6171  94 
(**NB: inj now just translates to inj_on**) 
5306  95 

923  96 
(*** inj(f): f is a onetoone function ***) 
97 

6171  98 
(*for Tools/datatype_rep_proofs*) 
99 
val [prem] = Goalw [inj_on_def] 

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

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

102 
qed "datatype_injI"; 

923  103 

6171  104 
Goalw [inj_on_def] "[ inj(f); f(x) = f(y) ] ==> x=y"; 
5316  105 
by (Blast_tac 1); 
923  106 
qed "injD"; 
107 

108 
(*Useful with the simplifier*) 

5316  109 
Goal "inj(f) ==> (f(x) = f(y)) = (x=y)"; 
923  110 
by (rtac iffI 1); 
5316  111 
by (etac arg_cong 2); 
112 
by (etac injD 1); 

5318  113 
by (assume_tac 1); 
923  114 
qed "inj_eq"; 
115 

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

5316  117 
Goalw [inv_def] "inj(f) ==> inv f (f x) = x"; 
10076
2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset

118 
by (asm_simp_tac (simpset() addsimps [inj_eq]) 1); 
2912  119 
qed "inv_f_f"; 
7338  120 
Addsimps [inv_f_f]; 
923  121 

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

124 
by (etac inv_f_f 1); 

125 
qed "inv_f_eq"; 

6235  126 

10066  127 
Goal "[ inj f; ALL x. f(g x) = x ] ==> inv f = g"; 
128 
by (blast_tac (claset() addIs [ext, inv_f_eq]) 1); 

129 
qed "inj_imp_inv_eq"; 

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"; 
9108  150 
bind_thm ("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"; 
9108  158 
bind_thm ("inj_inverseI", inj_on_inverseI); (*for compatibility*) 
923  159 

8285  160 
Goal "(inj f) = (inv f o f = id)"; 
161 
by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1); 

162 
by (blast_tac (claset() addIs [inj_inverseI, inv_f_f]) 1); 

163 
qed "inj_iff"; 

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})"; 
8253  178 
by (rtac injI 1); 
179 
by (etac singleton_inject 1); 

8156  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 

8253  201 
Goal "inj f ==> surj (inv f)"; 
202 
by (blast_tac (claset() addIs [surjI, inv_f_f]) 1); 

203 
qed "inj_imp_surj_inv"; 

7374  204 

205 

6171  206 
(*** Lemmas about injective functions and inv ***) 
923  207 

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

923  211 

5316  212 
Goalw [inv_def] "y : range(f) ==> f(inv f y) = y"; 
9970  213 
by (fast_tac (claset() addIs [someI]) 1); 
2912  214 
qed "f_inv_f"; 
923  215 

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

218 
qed "surj_f_inv_f"; 

219 

6171  220 
Goal "[ inv f x = inv f y; x: range(f); y: range(f) ] ==> x=y"; 
2912  221 
by (rtac (arg_cong RS box_equals) 1); 
5316  222 
by (REPEAT (ares_tac [f_inv_f] 1)); 
2912  223 
qed "inv_injective"; 
224 

6235  225 
Goal "A <= range(f) ==> inj_on (inv f) A"; 
4830  226 
by (fast_tac (claset() addIs [inj_onI] 
6235  227 
addEs [inv_injective, injD]) 1); 
4830  228 
qed "inj_on_inv"; 
923  229 

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

232 
qed "surj_imp_inj_inv"; 

233 

8285  234 
Goal "(surj f) = (f o inv f = id)"; 
235 
by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1); 

236 
by (blast_tac (claset() addIs [surjI, surj_f_inv_f]) 1); 

237 
qed "surj_iff"; 

238 

10066  239 
Goal "[ surj f; ALL x. g(f x) = x ] ==> inv f = g"; 
240 
by (rtac ext 1); 

241 
by (dres_inst_tac [("x","inv f x")] spec 1); 

242 
by (asm_full_simp_tac (simpset() addsimps [surj_f_inv_f]) 1); 

243 
qed "surj_imp_inv_eq"; 

244 

8253  245 

246 
(** Bijections **) 

247 

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

249 
by (Blast_tac 1); 

250 
qed "bijI"; 

251 

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

253 
by (Blast_tac 1); 

254 
qed "bij_is_inj"; 

255 

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

257 
by (Blast_tac 1); 

258 
qed "bij_is_surj"; 

259 

260 
Goalw [bij_def] "bij f ==> bij (inv f)"; 

261 
by (asm_simp_tac (simpset() addsimps [inj_imp_surj_inv, surj_imp_inj_inv]) 1); 

262 
qed "bij_imp_bij_inv"; 

263 

264 
val prems = 

265 
Goalw [inv_def] "[ !! x. g (f x) = x; !! y. f (g y) = y ] ==> inv f = g"; 

266 
by (rtac ext 1); 

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

268 
qed "inv_equality"; 

269 

270 
Goalw [bij_def] "bij f ==> inv (inv f) = f"; 

271 
by (rtac inv_equality 1); 

272 
by (auto_tac (claset(), simpset() addsimps [surj_f_inv_f])); 

273 
qed "inv_inv_eq"; 

274 

10066  275 
(** bij(inv f) implies little about f. Consider f::bool=>bool such that 
276 
f(True)=f(False)=True. Then it's consistent with axiom someI that 

277 
inv(f) could be any function at all, including the identity function. 

278 
If inv(f)=id then inv(f) is a bijection, but inj(f), surj(f) and 

279 
inv(inv(f))=f all fail. 

280 
**) 

281 

8253  282 
Goalw [bij_def] "[ bij f; bij g ] ==> inv (f o g) = inv g o inv f"; 
283 
by (rtac (inv_equality) 1); 

284 
by (auto_tac (claset(), simpset() addsimps [surj_f_inv_f])); 

285 
qed "o_inv_distrib"; 

286 

287 

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

290 

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

292 
by (Blast_tac 1); 

293 
qed "image_ident"; 

294 

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

296 
by (Blast_tac 1); 

297 
qed "image_id"; 

298 
Addsimps [image_ident, image_id]; 

299 

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

301 
by (Blast_tac 1); 

302 
qed "vimage_ident"; 

303 

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

305 
by Auto_tac; 

306 
qed "vimage_id"; 

307 
Addsimps [vimage_ident, vimage_id]; 

308 

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

311 
qed "vimage_image_eq"; 

312 

8173  313 
Goal "f `` (f `` A) <= A"; 
314 
by (Blast_tac 1); 

315 
qed "image_vimage_subset"; 

316 

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

318 
by (Blast_tac 1); 

319 
qed "image_vimage_eq"; 

320 
Addsimps [image_vimage_eq]; 

321 

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

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

324 
qed "surj_image_vimage_eq"; 

325 

8253  326 
Goal "surj f ==> f `` (inv f `` A) = A"; 
327 
by (asm_simp_tac (simpset() addsimps [image_eq_UN, surj_f_inv_f]) 1); 

328 
qed "image_surj_f_inv_f"; 

329 

8173  330 
Goalw [inj_on_def] "inj f ==> f `` (f `` A) = A"; 
331 
by (Blast_tac 1); 

332 
qed "inj_vimage_image_eq"; 

333 

8253  334 
Goal "inj f ==> (inv f) `` (f `` A) = A"; 
335 
by (asm_simp_tac (simpset() addsimps [image_eq_UN]) 1); 

336 
qed "image_inv_f_f"; 

337 

8173  338 
Goalw [surj_def] "surj f ==> f `` B <= A ==> B <= f `` A"; 
339 
by (blast_tac (claset() addIs [sym]) 1); 

340 
qed "vimage_subsetD"; 

341 

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

343 
by (Blast_tac 1); 

344 
qed "vimage_subsetI"; 

345 

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

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

348 
addIs [vimage_subsetI, vimage_subsetD]) 1); 

349 
qed "vimage_subset_eq"; 

350 

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

353 
qed "image_Int_subset"; 

354 

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

356 
by (Blast_tac 1); 

357 
qed "image_diff_subset"; 

358 

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

360 
"[ inj_on f C; A<=C; B<=C ] ==> f``(A Int B) = f``A Int f``B"; 
4059  361 
by (Blast_tac 1); 
4830  362 
qed "inj_on_image_Int"; 
4059  363 

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

365 
"[ inj_on f C; A<=C; B<=C ] ==> f``(AB) = f``A  f``B"; 
4059  366 
by (Blast_tac 1); 
4830  367 
qed "inj_on_image_set_diff"; 
4059  368 

6171  369 
Goalw [inj_on_def] "inj f ==> f``(A Int B) = f``A Int f``B"; 
4059  370 
by (Blast_tac 1); 
371 
qed "image_Int"; 

372 

6171  373 
Goalw [inj_on_def] "inj f ==> f``(AB) = f``A  f``B"; 
4059  374 
by (Blast_tac 1); 
375 
qed "image_set_diff"; 

376 

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

379 
qed "inv_image_comp"; 

5847  380 

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

383 
qed "inj_image_mem_iff"; 

384 

8253  385 
Goalw [inj_on_def] "inj f ==> (f``A <= f``B) = (A<=B)"; 
386 
by (Blast_tac 1); 

387 
qed "inj_image_subset_iff"; 

388 

6301  389 
Goal "inj f ==> (f``A = f``B) = (A = B)"; 
390 
by (blast_tac (claset() addSEs [equalityE] addDs [injD]) 1); 

391 
qed "inj_image_eq_iff"; 

392 

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

393 
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

394 
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

395 
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

396 

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

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

398 
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

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

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

401 
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

402 
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

403 

8309  404 
(*Compare with image_INT: no use of inj_on, and if f is surjective then 
405 
it doesn't matter whether A is empty*) 

406 
Goalw [bij_def] "bij f ==> f `` (INTER A B) = (INT x:A. f `` B x)"; 

407 
by (force_tac (claset() addSIs [surj_f_inv_f RS sym RS image_eqI], 

408 
simpset()) 1); 

409 
qed "bij_image_INT"; 

410 

411 
Goal "bij f ==> f `` Collect P = {y. P (inv f y)}"; 

412 
by Auto_tac; 

413 
by (force_tac (claset(), simpset() addsimps [bij_is_inj]) 1); 

414 
by (blast_tac (claset() addIs [bij_is_surj RS surj_f_inv_f RS sym]) 1); 

415 
qed "bij_image_Collect_eq"; 

416 

417 
Goal "bij f ==> f `` A = inv f `` A"; 

8767  418 
by Safe_tac; 
8309  419 
by (asm_simp_tac (simpset() addsimps [bij_is_surj RS surj_f_inv_f]) 2); 
420 
by (blast_tac (claset() addIs [bij_is_inj RS inv_f_f RS sym]) 1); 

421 
qed "bij_vimage_eq_inv_image"; 

422 

10076
2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset

423 
Goal "surj f ==> (f``A) <= f``(A)"; 
2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset

424 
by (auto_tac (claset(), simpset() addsimps [surj_def])); 
2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset

425 
qed "surj_Compl_image_subset"; 
2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset

426 

2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset

427 
Goal "inj f ==> f``(A) <= (f``A)"; 
2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset

428 
by (auto_tac (claset(), simpset() addsimps [inj_on_def])); 
2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset

429 
qed "inj_image_Compl_subset"; 
2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset

430 

2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset

431 
Goalw [bij_def] "bij f ==> f``(A) = (f``A)"; 
2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset

432 
by (rtac equalityI 1); 
2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset

433 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [inj_image_Compl_subset, 
2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset

434 
surj_Compl_image_subset]))); 
2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset

435 
qed "bij_image_Compl_eq"; 
2683ff181047
removed the obsolete (and badly named) inj_select
paulson
parents:
10066
diff
changeset

436 

4089  437 
val set_cs = claset() delrules [equalityI]; 
5305  438 

439 

440 
section "fun_upd"; 

441 

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

443 
by Safe_tac; 

444 
by (etac subst 1); 

445 
by (rtac ext 2); 

446 
by Auto_tac; 

447 
qed "fun_upd_idem_iff"; 

448 

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

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

451 

452 
(* f(x := f x) = f *) 

453 
AddIffs [refl RS fun_upd_idem]; 

454 

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

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

457 
qed "fun_upd_apply"; 

458 
Addsimps [fun_upd_apply]; 

459 

9339  460 
(* fun_upd_apply supersedes these two, but they are useful 
461 
if fun_upd_apply is intentionally removed from the simpset *) 

7089  462 
Goal "(f(x:=y)) x = y"; 
463 
by (Simp_tac 1); 

464 
qed "fun_upd_same"; 

465 

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

467 
by (Asm_simp_tac 1); 

468 
qed "fun_upd_other"; 

469 

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

472 
by (Simp_tac 1); 

473 
qed "fun_upd_upd"; 

474 
Addsimps [fun_upd_upd]; 

5305  475 

9339  476 
(* simplifies terms of the form f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *) 
477 
local 

478 
fun gen_fun_upd None T _ _ = None 

479 
 gen_fun_upd (Some f) T x y = Some (Const ("Fun.fun_upd",T) $ f $ x $ y) 

480 
fun dest_fun_T1 (Type (_,T::Ts)) = T 

481 
fun find_double (t as Const ("Fun.fun_upd",T) $ f $ x $ y) = let 

482 
fun find (Const ("Fun.fun_upd",T) $ g $ v $ w) = 

483 
if v aconv x then Some g else gen_fun_upd (find g) T v w 

484 
 find t = None 

485 
in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end 

9422  486 
val ss = simpset (); 
9339  487 
val fun_upd_prover = K [rtac eq_reflection 1, rtac ext 1, 
9422  488 
simp_tac ss 1] 
9339  489 
fun mk_eq_cterm sg T l r = Thm.cterm_of sg (equals T $ l $ r) 
490 
in 

491 
val fun_upd2_simproc = Simplifier.mk_simproc "fun_upd2" 

9422  492 
[Thm.read_cterm (sign_of (the_context ())) ("f(v:=w,x:=y)", HOLogic.termT)] 
9339  493 
(fn sg => (K (fn t => case find_double t of (T,None)=> None  (T,Some rhs)=> 
494 
Some (prove_goalw_cterm [] (mk_eq_cterm sg T t rhs) fun_upd_prover)))) 

495 
end; 

496 
Addsimprocs[fun_upd2_simproc]; 

497 

8258  498 
Goal "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)"; 
5305  499 
by (rtac ext 1); 
7089  500 
by Auto_tac; 
5305  501 
qed "fun_upd_twist"; 
5852  502 

503 

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

505 

506 
val prems = Goalw [Pi_def] 

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

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

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

510 
qed "Pi_I"; 

511 

512 
val prems = Goal 

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

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

515 
qed "funcsetI"; 

516 

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

518 
by Auto_tac; 

519 
qed "Pi_mem"; 

520 

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

522 
by Auto_tac; 

523 
qed "funcset_mem"; 

524 

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

526 
by Auto_tac; 

527 
qed "apply_arb"; 

528 

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

530 
by (rtac ext 1); 

531 
by Auto_tac; 

9108  532 
bind_thm ("Pi_extensionality", ballI RSN (3, result())); 
5852  533 

8138  534 

5852  535 
(*** compose ***) 
536 

537 
Goalw [Pi_def, compose_def, restrict_def] 

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

539 
by Auto_tac; 

540 
qed "funcset_compose"; 

541 

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

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

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

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

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

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

548 
by Auto_tac; 

549 
qed "compose_assoc"; 

550 

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

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

553 
qed "compose_eq"; 

554 

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

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

557 
by (auto_tac (claset(), 

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

559 
qed "surj_compose"; 

560 

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

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

563 
by (auto_tac (claset(), 

8081  564 
simpset() addsimps [inj_on_def, compose_eq])); 
5852  565 
qed "inj_on_compose"; 
566 

567 

568 
(*** restrict / lam ***) 

8138  569 

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

5852  571 
by (auto_tac (claset(), 
572 
simpset() addsimps [restrict_def, Pi_def])); 

573 
qed "restrict_in_funcset"; 

574 

575 
val prems = Goalw [restrict_def, Pi_def] 

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

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

578 
qed "restrictI"; 

579 

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

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

582 
qed "restrict_apply1"; 

583 

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

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

586 
qed "restrict_apply1_mem"; 

587 

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

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

590 
qed "restrict_apply2"; 

591 

592 
val prems = Goal 

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

594 
by (rtac ext 1); 

595 
by (auto_tac (claset(), 

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

597 
qed "restrict_ext"; 

598 

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

601 
qed "inj_on_restrict_eq"; 

602 

5852  603 

604 
(*** Inverse ***) 

605 

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

607 
by (Blast_tac 1); 

608 
qed "surj_image"; 

609 

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

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

9969  612 
by (fast_tac (claset() addIs [restrict_in_funcset, someI2]) 1); 
5852  613 
qed "Inv_funcset"; 
614 

615 

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

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

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

8081  619 
by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1); 
9969  620 
by (rtac someI2 1); 
5852  621 
by Auto_tac; 
622 
qed "Inv_f_f"; 

623 

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

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

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

9969  627 
by (fast_tac (claset() addIs [someI2]) 1); 
5852  628 
qed "f_Inv_f"; 
629 

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

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

632 
by (rtac Pi_extensionality 1); 

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

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

635 
by (asm_simp_tac 

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

637 
qed "compose_Inv_id"; 

638 

639 

640 
(*** Pi and Applyall ***) 

641 

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

643 
by Auto_tac; 

644 
qed "Pi_eq_empty"; 

645 

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

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

648 
qed "Pi_total1"; 

649 

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

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

652 
by (rename_tac "g z" 1); 

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

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

655 
qed "Applyall_beta"; 

656 

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

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

658 
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

659 
qed "Pi_empty"; 
5852  660 

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

661 
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

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

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

664 
qed "Pi_mono"; 