author  paulson 
Mon, 16 Nov 1998 10:36:30 +0100  
changeset 5865  2303f5a3036d 
parent 5852  4d7320490be4 
child 6171  cd237a10cbf8 
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); 

63 
qed "UNION_o"; 

64 

5306  65 

66 
section "inj"; 

67 

923  68 
(*** inj(f): f is a onetoone function ***) 
69 

5316  70 
val prems = Goalw [inj_def] 
923  71 
"[ !! x y. f(x) = f(y) ==> x=y ] ==> inj(f)"; 
4089  72 
by (blast_tac (claset() addIs prems) 1); 
923  73 
qed "injI"; 
74 

5316  75 
val [major] = Goal "(!!x. g(f(x)) = x) ==> inj(f)"; 
923  76 
by (rtac injI 1); 
77 
by (etac (arg_cong RS box_equals) 1); 

78 
by (rtac major 1); 

79 
by (rtac major 1); 

80 
qed "inj_inverseI"; 

81 

5316  82 
Goalw [inj_def] "[ inj(f); f(x) = f(y) ] ==> x=y"; 
83 
by (Blast_tac 1); 

923  84 
qed "injD"; 
85 

86 
(*Useful with the simplifier*) 

5316  87 
Goal "inj(f) ==> (f(x) = f(y)) = (x=y)"; 
923  88 
by (rtac iffI 1); 
5316  89 
by (etac arg_cong 2); 
90 
by (etac injD 1); 

5318  91 
by (assume_tac 1); 
923  92 
qed "inj_eq"; 
93 

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

923  96 
by (rtac selectI 1); 
97 
by (rtac refl 1); 

98 
qed "inj_select"; 

99 

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

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

2912  103 
qed "inv_f_f"; 
923  104 

105 
(* Useful??? *) 

5316  106 
val [oneone,minor] = Goal 
2912  107 
"[ inj(f); !!y. y: range(f) ==> P(inv f y) ] ==> P(x)"; 
108 
by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1); 

923  109 
by (rtac (rangeI RS minor) 1); 
110 
qed "inj_transfer"; 

111 

112 

4830  113 
(*** inj_on f A: f is onetoone over A ***) 
923  114 

5316  115 
val prems = Goalw [inj_on_def] 
4830  116 
"(!! x y. [ f(x) = f(y); x:A; y:A ] ==> x=y) ==> inj_on f A"; 
4089  117 
by (blast_tac (claset() addIs prems) 1); 
4830  118 
qed "inj_onI"; 
923  119 

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

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

4830  125 
qed "inj_on_inverseI"; 
923  126 

5316  127 
Goalw [inj_on_def] "[ inj_on f A; f(x)=f(y); x:A; y:A ] ==> x=y"; 
128 
by (Blast_tac 1); 

4830  129 
qed "inj_onD"; 
923  130 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

131 
Goal "[ inj_on f A; x:A; y:A ] ==> (f(x)=f(y)) = (x=y)"; 
4830  132 
by (blast_tac (claset() addSDs [inj_onD]) 1); 
133 
qed "inj_on_iff"; 

923  134 

5316  135 
Goalw [inj_on_def] "[ inj_on f A; ~x=y; x:A; y:A ] ==> ~ f(x)=f(y)"; 
136 
by (Blast_tac 1); 

4830  137 
qed "inj_on_contraD"; 
923  138 

5316  139 
Goalw [inj_on_def] "[ A<=B; inj_on f B ] ==> inj_on f A"; 
3341  140 
by (Blast_tac 1); 
4830  141 
qed "subset_inj_on"; 
3341  142 

923  143 

144 
(*** Lemmas about inj ***) 

145 

5316  146 
Goalw [o_def] "[ inj(f); inj_on g (range f) ] ==> inj(g o f)"; 
4830  147 
by (fast_tac (claset() addIs [injI] addEs [injD, inj_onD]) 1); 
923  148 
qed "comp_inj"; 
149 

5316  150 
Goal "inj(f) ==> inj_on f A"; 
151 
by (blast_tac (claset() addIs [injD, inj_onI]) 1); 

923  152 
qed "inj_imp"; 
153 

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

2912  156 
qed "f_inv_f"; 
923  157 

5316  158 
Goal "[ inv f x=inv f y; x: range(f); y: range(f) ] ==> x=y"; 
2912  159 
by (rtac (arg_cong RS box_equals) 1); 
5316  160 
by (REPEAT (ares_tac [f_inv_f] 1)); 
2912  161 
qed "inv_injective"; 
162 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

163 
Goal "[ inj(f); A<=range(f) ] ==> inj_on (inv f) A"; 
4830  164 
by (fast_tac (claset() addIs [inj_onI] 
2912  165 
addEs [inv_injective,injD]) 1); 
4830  166 
qed "inj_on_inv"; 
923  167 

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

169 
"[ inj_on f C; A<=C; B<=C ] ==> f``(A Int B) = f``A Int f``B"; 
4059  170 
by (Blast_tac 1); 
4830  171 
qed "inj_on_image_Int"; 
4059  172 

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

174 
"[ inj_on f C; A<=C; B<=C ] ==> f``(AB) = f``A  f``B"; 
4059  175 
by (Blast_tac 1); 
4830  176 
qed "inj_on_image_set_diff"; 
4059  177 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

178 
Goalw [inj_def] "inj f ==> f``(A Int B) = f``A Int f``B"; 
4059  179 
by (Blast_tac 1); 
180 
qed "image_Int"; 

181 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

182 
Goalw [inj_def] "inj f ==> f``(AB) = f``A  f``B"; 
4059  183 
by (Blast_tac 1); 
184 
qed "image_set_diff"; 

185 

923  186 

5847  187 

188 
val [major] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g"; 

189 
by (blast_tac (claset() addIs [major RS sym]) 1); 

190 
qed "surjI"; 

191 

192 

4089  193 
val set_cs = claset() delrules [equalityI]; 
5305  194 

195 

196 
section "fun_upd"; 

197 

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

199 
by Safe_tac; 

200 
by (etac subst 1); 

201 
by (rtac ext 2); 

202 
by Auto_tac; 

203 
qed "fun_upd_idem_iff"; 

204 

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

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

207 

208 
(* f(x := f x) = f *) 

209 
AddIffs [refl RS fun_upd_idem]; 

210 

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

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

213 
qed "fun_upd_apply"; 

214 
Addsimps [fun_upd_apply]; 

215 

216 
qed_goal "fun_upd_same" thy "(f(x:=y)) x = y" 

217 
(K [Simp_tac 1]); 

5306  218 
qed_goal "fun_upd_other" thy "!!X. z~=x ==> (f(x:=y)) z = f z" 
5305  219 
(K [Asm_simp_tac 1]); 
220 
(*Addsimps [fun_upd_same, fun_upd_other];*) 

221 

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

223 
by (rtac ext 1); 

224 
by (Auto_tac); 

225 
qed "fun_upd_twist"; 

5852  226 

227 

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

229 

230 
val prems = Goalw [Pi_def] 

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

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

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

234 
qed "Pi_I"; 

235 

236 
val prems = Goal 

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

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

239 
qed "funcsetI"; 

240 

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

242 
by Auto_tac; 

243 
qed "Pi_mem"; 

244 

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

246 
by Auto_tac; 

247 
qed "funcset_mem"; 

248 

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

250 
by Auto_tac; 

251 
qed "apply_arb"; 

252 

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

254 
by (rtac ext 1); 

255 
by Auto_tac; 

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

257 

258 
(*** compose ***) 

259 

260 
Goalw [Pi_def, compose_def, restrict_def] 

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

262 
by Auto_tac; 

263 
qed "funcset_compose"; 

264 

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

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

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

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

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

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

271 
by Auto_tac; 

272 
qed "compose_assoc"; 

273 

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

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

276 
qed "compose_eq"; 

277 

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

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

280 
by (auto_tac (claset(), 

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

282 
qed "surj_compose"; 

283 

284 

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

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

287 
by (auto_tac (claset(), 

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

289 
qed "inj_on_compose"; 

290 

291 

292 
(*** restrict / lam ***) 

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

294 
by (auto_tac (claset(), 

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

296 
qed "restrict_in_funcset"; 

297 

298 
val prems = Goalw [restrict_def, Pi_def] 

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

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

301 
qed "restrictI"; 

302 

303 

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

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

306 
qed "restrict_apply1"; 

307 

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

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

310 
qed "restrict_apply1_mem"; 

311 

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

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

314 
qed "restrict_apply2"; 

315 

316 

317 
val prems = Goal 

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

319 
by (rtac ext 1); 

320 
by (auto_tac (claset(), 

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

322 
qed "restrict_ext"; 

323 

324 

325 
(*** Inverse ***) 

326 

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

328 
by (Blast_tac 1); 

329 
qed "surj_image"; 

330 

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

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

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

334 
qed "Inv_funcset"; 

335 

336 

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

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

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

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

341 
by (rtac selectI2 1); 

342 
by Auto_tac; 

343 
qed "Inv_f_f"; 

344 

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

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

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

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

349 
qed "f_Inv_f"; 

350 

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

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

353 
by (rtac Pi_extensionality 1); 

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

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

356 
by (asm_simp_tac 

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

358 
qed "compose_Inv_id"; 

359 

360 

361 
(*** Pi and Applyall ***) 

362 

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

364 
by Auto_tac; 

365 
qed "Pi_eq_empty"; 

366 

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

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

369 
qed "Pi_total1"; 

370 

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

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

373 
by (rename_tac "g z" 1); 

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

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

376 
qed "Applyall_beta"; 

377 

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

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

379 
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

380 
qed "Pi_empty"; 
5852  381 

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

382 
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

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

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

385 
qed "Pi_mono"; 