author  wenzelm 
Thu, 27 Sep 2001 22:22:08 +0200  
changeset 11601  9273cef990f5 
parent 11459  1b6258b288ba 
child 12338  de0f4a63baa5 
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 

5608  22 
section "id"; 
5441  23 

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

26 
qed "id_apply"; 

5608  27 
Addsimps [id_apply]; 
5441  28 

29 

5306  30 
section "o"; 
31 

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

34 
qed "o_apply"; 

5306  35 
Addsimps [o_apply]; 
36 

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

39 
by (rtac refl 1); 

40 
qed "o_assoc"; 

5306  41 

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

44 
by (Simp_tac 1); 

45 
qed "id_o"; 

5608  46 
Addsimps [id_o]; 
5306  47 

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

50 
by (Simp_tac 1); 

51 
qed "o_id"; 

5608  52 
Addsimps [o_id]; 
5306  53 

10832  54 
Goalw [o_def] "(f o g)`r = f`(g`r)"; 
5306  55 
by (Blast_tac 1); 
56 
qed "image_compose"; 

57 

10832  58 
Goal "f`A = (UN x:A. {f x})"; 
7536  59 
by (Blast_tac 1); 
7916  60 
qed "image_eq_UN"; 
7536  61 

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

64 
qed "UN_o"; 
5852  65 

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

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

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

68 

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

69 
Goalw [o_def] 
7089  70 
"[ ! x y. g (f x) = g y > f x = y; g o f = g o fa ] ==> f = fa"; 
71 
by (rtac ext 1); 

72 
by (etac allE 1); 

73 
by (etac allE 1); 

74 
by (etac mp 1); 

75 
by (etac fun_cong 1); 

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

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

77 

5306  78 

79 
section "inj"; 

6171  80 
(**NB: inj now just translates to inj_on**) 
5306  81 

923  82 
(*** inj(f): f is a onetoone function ***) 
83 

6171  84 
(*for Tools/datatype_rep_proofs*) 
85 
val [prem] = Goalw [inj_on_def] 

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

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

88 
qed "datatype_injI"; 

923  89 

6171  90 
Goalw [inj_on_def] "[ inj(f); f(x) = f(y) ] ==> x=y"; 
5316  91 
by (Blast_tac 1); 
923  92 
qed "injD"; 
93 

94 
(*Useful with the simplifier*) 

5316  95 
Goal "inj(f) ==> (f(x) = f(y)) = (x=y)"; 
923  96 
by (rtac iffI 1); 
5316  97 
by (etac arg_cong 2); 
98 
by (etac injD 1); 

5318  99 
by (assume_tac 1); 
923  100 
qed "inj_eq"; 
101 

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

102 
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

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

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

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

106 
qed "inj_o"; 
923  107 

4830  108 
(*** inj_on f A: f is onetoone over A ***) 
923  109 

5316  110 
val prems = Goalw [inj_on_def] 
11395  111 
"(!! x y. [ x:A; y:A; f(x) = f(y) ] ==> x=y) ==> inj_on f A"; 
4089  112 
by (blast_tac (claset() addIs prems) 1); 
4830  113 
qed "inj_onI"; 
9108  114 
bind_thm ("injI", inj_onI); (*for compatibility*) 
923  115 

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

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

4830  121 
qed "inj_on_inverseI"; 
9108  122 
bind_thm ("inj_inverseI", inj_on_inverseI); (*for compatibility*) 
923  123 

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

4830  126 
qed "inj_onD"; 
923  127 

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

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

923  131 

11459  132 
Goalw [o_def, inj_on_def] 
133 
"[ inj_on f A; inj_on g (f`A) ] ==> inj_on (g o f) A"; 

134 
by (Blast_tac 1); 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11446
diff
changeset

135 
qed "comp_inj_on"; 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11446
diff
changeset

136 

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

4830  139 
qed "inj_on_contraD"; 
923  140 

8156  141 
Goal "inj (%s. {s})"; 
8253  142 
by (rtac injI 1); 
143 
by (etac singleton_inject 1); 

8156  144 
qed "inj_singleton"; 
145 

5316  146 
Goalw [inj_on_def] "[ A<=B; inj_on f B ] ==> inj_on f A"; 
3341  147 
by (Blast_tac 1); 
4830  148 
qed "subset_inj_on"; 
3341  149 

923  150 

6235  151 
(** surj **) 
152 

6267  153 
val [prem] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g"; 
154 
by (blast_tac (claset() addIs [prem RS sym]) 1); 

6235  155 
qed "surjI"; 
156 

157 
Goalw [surj_def] "surj f ==> range f = UNIV"; 

158 
by Auto_tac; 

159 
qed "surj_range"; 

160 

6267  161 
Goalw [surj_def] "surj f ==> EX x. y = f x"; 
162 
by (Blast_tac 1); 

163 
qed "surjD"; 

164 

11601  165 
val [p1, p2] = Goal "surj f ==> (!!x. y = f x ==> C) ==> C"; 
166 
by (cut_facts_tac [p1 RS surjD] 1); 

167 
by (etac exE 1); 

168 
by (rtac p2 1); 

169 
by (atac 1); 

170 
qed "surjE"; 

171 

11459  172 
Goalw [o_def, surj_def] "[ surj f; surj g ] ==> surj (g o f)"; 
173 
by (Clarify_tac 1); 

174 
by (dres_inst_tac [("x","y")] spec 1); 

175 
by (Clarify_tac 1); 

176 
by (dres_inst_tac [("x","x")] spec 1); 

177 
by (Blast_tac 1); 

178 
qed "comp_surj"; 

10066  179 

8253  180 

181 
(** Bijections **) 

182 

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

184 
by (Blast_tac 1); 

185 
qed "bijI"; 

186 

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

188 
by (Blast_tac 1); 

189 
qed "bij_is_inj"; 

190 

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

192 
by (Blast_tac 1); 

193 
qed "bij_is_surj"; 

194 

195 

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

198 

10832  199 
Goal "(%x. x) ` Y = Y"; 
7514  200 
by (Blast_tac 1); 
201 
qed "image_ident"; 

202 

10832  203 
Goalw [id_def] "id ` Y = Y"; 
7514  204 
by (Blast_tac 1); 
205 
qed "image_id"; 

206 
Addsimps [image_ident, image_id]; 

207 

10832  208 
Goal "(%x. x) ` Y = Y"; 
7514  209 
by (Blast_tac 1); 
210 
qed "vimage_ident"; 

211 

10832  212 
Goalw [id_def] "id ` A = A"; 
7514  213 
by Auto_tac; 
214 
qed "vimage_id"; 

215 
Addsimps [vimage_ident, vimage_id]; 

216 

10832  217 
Goal "f ` (f ` A) = {y. EX x:A. f x = f y}"; 
7876  218 
by (blast_tac (claset() addIs [sym]) 1); 
219 
qed "vimage_image_eq"; 

220 

10832  221 
Goal "f ` (f ` A) <= A"; 
8173  222 
by (Blast_tac 1); 
223 
qed "image_vimage_subset"; 

224 

10832  225 
Goal "f ` (f ` A) = A Int range f"; 
8173  226 
by (Blast_tac 1); 
227 
qed "image_vimage_eq"; 

228 
Addsimps [image_vimage_eq]; 

229 

10832  230 
Goal "surj f ==> f ` (f ` A) = A"; 
8173  231 
by (asm_simp_tac (simpset() addsimps [surj_range]) 1); 
232 
qed "surj_image_vimage_eq"; 

233 

10832  234 
Goalw [inj_on_def] "inj f ==> f ` (f ` A) = A"; 
8173  235 
by (Blast_tac 1); 
236 
qed "inj_vimage_image_eq"; 

237 

10832  238 
Goalw [surj_def] "surj f ==> f ` B <= A ==> B <= f ` A"; 
8173  239 
by (blast_tac (claset() addIs [sym]) 1); 
240 
qed "vimage_subsetD"; 

241 

10832  242 
Goalw [inj_on_def] "inj f ==> B <= f ` A ==> f ` B <= A"; 
8173  243 
by (Blast_tac 1); 
244 
qed "vimage_subsetI"; 

245 

10832  246 
Goalw [bij_def] "bij f ==> (f ` B <= A) = (B <= f ` A)"; 
8173  247 
by (blast_tac (claset() delrules [subsetI] 
248 
addIs [vimage_subsetI, vimage_subsetD]) 1); 

249 
qed "vimage_subset_eq"; 

250 

10832  251 
Goal "f`(A Int B) <= f`A Int f`B"; 
6290  252 
by (Blast_tac 1); 
253 
qed "image_Int_subset"; 

254 

10832  255 
Goal "f`A  f`B <= f`(A  B)"; 
6290  256 
by (Blast_tac 1); 
257 
qed "image_diff_subset"; 

258 

5069  259 
Goalw [inj_on_def] 
10832  260 
"[ inj_on f C; A<=C; B<=C ] ==> f`(A Int B) = f`A Int f`B"; 
4059  261 
by (Blast_tac 1); 
4830  262 
qed "inj_on_image_Int"; 
4059  263 

5069  264 
Goalw [inj_on_def] 
10832  265 
"[ inj_on f C; A<=C; B<=C ] ==> f`(AB) = f`A  f`B"; 
4059  266 
by (Blast_tac 1); 
4830  267 
qed "inj_on_image_set_diff"; 
4059  268 

10832  269 
Goalw [inj_on_def] "inj f ==> f`(A Int B) = f`A Int f`B"; 
4059  270 
by (Blast_tac 1); 
271 
qed "image_Int"; 

272 

10832  273 
Goalw [inj_on_def] "inj f ==> f`(AB) = f`A  f`B"; 
4059  274 
by (Blast_tac 1); 
275 
qed "image_set_diff"; 

276 

10832  277 
Goal "inj f ==> (f a : f`A) = (a : A)"; 
6301  278 
by (blast_tac (claset() addDs [injD]) 1); 
279 
qed "inj_image_mem_iff"; 

280 

10832  281 
Goalw [inj_on_def] "inj f ==> (f`A <= f`B) = (A<=B)"; 
8253  282 
by (Blast_tac 1); 
283 
qed "inj_image_subset_iff"; 

284 

10832  285 
Goal "inj f ==> (f`A = f`B) = (A = B)"; 
6301  286 
by (blast_tac (claset() addSEs [equalityE] addDs [injD]) 1); 
287 
qed "inj_image_eq_iff"; 

288 

10832  289 
Goal "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))"; 
6829
50459a995aa3
renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents:
6301
diff
changeset

290 
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

291 
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

292 

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

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

294 
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

295 
"[ inj_on f C; ALL x:A. B x <= C; j:A ] \ 
10832  296 
\ ==> f ` (INTER A B) = (INT x:A. f ` B x)"; 
6829
50459a995aa3
renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents:
6301
diff
changeset

297 
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

298 
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

299 

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

10832  302 
Goalw [bij_def] "bij f ==> f ` (INTER A B) = (INT x:A. f ` B x)"; 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11446
diff
changeset

303 
by (asm_full_simp_tac (simpset() addsimps [inj_on_def, surj_def]) 1); 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11446
diff
changeset

304 
by (Blast_tac 1); 
8309  305 
qed "bij_image_INT"; 
306 

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

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

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

310 

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

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

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

314 

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

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

317 
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

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

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

320 

4089  321 
val set_cs = claset() delrules [equalityI]; 
5305  322 

323 

324 
section "fun_upd"; 

325 

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

327 
by Safe_tac; 

328 
by (etac subst 1); 

329 
by (rtac ext 2); 

330 
by Auto_tac; 

331 
qed "fun_upd_idem_iff"; 

332 

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

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

335 

336 
(* f(x := f x) = f *) 

337 
AddIffs [refl RS fun_upd_idem]; 

338 

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

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

341 
qed "fun_upd_apply"; 

342 
Addsimps [fun_upd_apply]; 

343 

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

7089  346 
Goal "(f(x:=y)) x = y"; 
347 
by (Simp_tac 1); 

348 
qed "fun_upd_same"; 

349 

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

351 
by (Asm_simp_tac 1); 

352 
qed "fun_upd_other"; 

353 

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

356 
by (Simp_tac 1); 

357 
qed "fun_upd_upd"; 

358 
Addsimps [fun_upd_upd]; 

5305  359 

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

362 
fun gen_fun_upd None T _ _ = None 

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

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

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

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

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

368 
 find t = None 

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

9422  370 
val ss = simpset (); 
9339  371 
val fun_upd_prover = K [rtac eq_reflection 1, rtac ext 1, 
9422  372 
simp_tac ss 1] 
9339  373 
fun mk_eq_cterm sg T l r = Thm.cterm_of sg (equals T $ l $ r) 
374 
in 

375 
val fun_upd2_simproc = Simplifier.mk_simproc "fun_upd2" 

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

379 
end; 

380 
Addsimprocs[fun_upd2_simproc]; 

381 

8258  382 
Goal "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)"; 
5305  383 
by (rtac ext 1); 
7089  384 
by Auto_tac; 
5305  385 
qed "fun_upd_twist"; 
5852  386 

387 

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

389 

390 
val prems = Goalw [Pi_def] 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11446
diff
changeset

391 
"[ !!x. x: A ==> f x: B x; !!x. x ~: A ==> f(x) = arbitrary] \ 
5852  392 
\ ==> f: Pi A B"; 
393 
by (auto_tac (claset(), simpset() addsimps prems)); 

394 
qed "Pi_I"; 

395 

396 
val prems = Goal 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11446
diff
changeset

397 
"[ !!x. x: A ==> f x: B; !!x. x ~: A ==> f(x) = arbitrary] ==> f: A funcset B"; 
5852  398 
by (blast_tac (claset() addIs Pi_I::prems) 1); 
399 
qed "funcsetI"; 

400 

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

402 
by Auto_tac; 

403 
qed "Pi_mem"; 

404 

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

406 
by Auto_tac; 

407 
qed "funcset_mem"; 

408 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11446
diff
changeset

409 
Goalw [Pi_def] "[f: Pi A B; x~: A] ==> f x = arbitrary"; 
5852  410 
by Auto_tac; 
411 
qed "apply_arb"; 

412 

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

414 
by (rtac ext 1); 

415 
by Auto_tac; 

9108  416 
bind_thm ("Pi_extensionality", ballI RSN (3, result())); 
5852  417 

8138  418 

5852  419 
(*** compose ***) 
420 

421 
Goalw [Pi_def, compose_def, restrict_def] 

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

423 
by Auto_tac; 

424 
qed "funcset_compose"; 

425 

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

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

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

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

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

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

432 
by Auto_tac; 

433 
qed "compose_assoc"; 

434 

11446  435 
Goal "x : A ==> compose A g f x = g(f(x))"; 
436 
by (asm_simp_tac (simpset() addsimps [compose_def, restrict_def]) 1); 

5852  437 
qed "compose_eq"; 
438 

11446  439 
Goal "[ f ` A = B; g ` B = C ] ==> compose A g f ` A = C"; 
440 
by (auto_tac (claset(), simpset() addsimps [image_def, compose_eq])); 

5852  441 
qed "surj_compose"; 
442 

11446  443 
Goal "[ f ` A = B; inj_on f A; inj_on g B ] ==> inj_on (compose A g f) A"; 
444 
by (auto_tac (claset(), simpset() addsimps [inj_on_def, compose_eq])); 

5852  445 
qed "inj_on_compose"; 
446 

447 

448 
(*** restrict / lam ***) 

8138  449 

10832  450 
Goal "f`A <= B ==> (lam x: A. f x) : A funcset B"; 
5852  451 
by (auto_tac (claset(), 
452 
simpset() addsimps [restrict_def, Pi_def])); 

453 
qed "restrict_in_funcset"; 

454 

455 
val prems = Goalw [restrict_def, Pi_def] 

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

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

458 
qed "restrictI"; 

459 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11446
diff
changeset

460 
Goal "(lam y: A. f y) x = (if x : A then f x else arbitrary)"; 
5852  461 
by (asm_simp_tac (simpset() addsimps [restrict_def]) 1); 
11395  462 
qed "restrict_apply"; 
463 
Addsimps [restrict_apply]; 

5852  464 

465 
val prems = Goal 

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

467 
by (rtac ext 1); 

468 
by (auto_tac (claset(), 

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

470 
qed "restrict_ext"; 

471 

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

474 
qed "inj_on_restrict_eq"; 

475 

5852  476 

11446  477 
Goal "f : A funcset B ==> compose A (lam y:B. y) f = f"; 
478 
by (rtac ext 1); 

479 
by (auto_tac (claset(), simpset() addsimps [compose_def, Pi_def])); 

480 
qed "Id_compose"; 

481 

482 
Goal "g : A funcset B ==> compose A g (lam x:A. x) = g"; 

483 
by (rtac ext 1); 

484 
by (auto_tac (claset(), simpset() addsimps [compose_def, Pi_def])); 

485 
qed "compose_Id"; 

486 

5852  487 

10826  488 
(*** Pi ***) 
5852  489 

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

491 
by Auto_tac; 

492 
qed "Pi_eq_empty"; 

493 

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

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

496 
qed "Pi_total1"; 

497 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11446
diff
changeset

498 
Goal "Pi {} B = { %x. arbitrary }"; 
5865
2303f5a3036d
moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents:
5852
diff
changeset

499 
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

500 
qed "Pi_empty"; 
5852  501 

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

502 
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

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

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

505 
qed "Pi_mono"; 