author | paulson |
Wed, 11 Nov 1998 15:49:15 +0100 | |
changeset 5847 | 17c869f24c5f |
parent 5608 | a82a038a3e7a |
child 5852 | 4d7320490be4 |
permissions | -rw-r--r-- |
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 |
||
61 |
||
62 |
section "inj"; |
|
63 |
||
923 | 64 |
(*** inj(f): f is a one-to-one function ***) |
65 |
||
5316 | 66 |
val prems = Goalw [inj_def] |
923 | 67 |
"[| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)"; |
4089 | 68 |
by (blast_tac (claset() addIs prems) 1); |
923 | 69 |
qed "injI"; |
70 |
||
5316 | 71 |
val [major] = Goal "(!!x. g(f(x)) = x) ==> inj(f)"; |
923 | 72 |
by (rtac injI 1); |
73 |
by (etac (arg_cong RS box_equals) 1); |
|
74 |
by (rtac major 1); |
|
75 |
by (rtac major 1); |
|
76 |
qed "inj_inverseI"; |
|
77 |
||
5316 | 78 |
Goalw [inj_def] "[| inj(f); f(x) = f(y) |] ==> x=y"; |
79 |
by (Blast_tac 1); |
|
923 | 80 |
qed "injD"; |
81 |
||
82 |
(*Useful with the simplifier*) |
|
5316 | 83 |
Goal "inj(f) ==> (f(x) = f(y)) = (x=y)"; |
923 | 84 |
by (rtac iffI 1); |
5316 | 85 |
by (etac arg_cong 2); |
86 |
by (etac injD 1); |
|
5318 | 87 |
by (assume_tac 1); |
923 | 88 |
qed "inj_eq"; |
89 |
||
5316 | 90 |
Goal "inj(f) ==> (@x. f(x)=f(y)) = y"; |
91 |
by (etac injD 1); |
|
923 | 92 |
by (rtac selectI 1); |
93 |
by (rtac refl 1); |
|
94 |
qed "inj_select"; |
|
95 |
||
96 |
(*A one-to-one function has an inverse (given using select).*) |
|
5316 | 97 |
Goalw [inv_def] "inj(f) ==> inv f (f x) = x"; |
98 |
by (etac inj_select 1); |
|
2912 | 99 |
qed "inv_f_f"; |
923 | 100 |
|
101 |
(* Useful??? *) |
|
5316 | 102 |
val [oneone,minor] = Goal |
2912 | 103 |
"[| inj(f); !!y. y: range(f) ==> P(inv f y) |] ==> P(x)"; |
104 |
by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1); |
|
923 | 105 |
by (rtac (rangeI RS minor) 1); |
106 |
qed "inj_transfer"; |
|
107 |
||
108 |
||
4830 | 109 |
(*** inj_on f A: f is one-to-one over A ***) |
923 | 110 |
|
5316 | 111 |
val prems = Goalw [inj_on_def] |
4830 | 112 |
"(!! x y. [| f(x) = f(y); x:A; y:A |] ==> x=y) ==> inj_on f A"; |
4089 | 113 |
by (blast_tac (claset() addIs prems) 1); |
4830 | 114 |
qed "inj_onI"; |
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"; |
923 | 122 |
|
5316 | 123 |
Goalw [inj_on_def] "[| inj_on f A; f(x)=f(y); x:A; y:A |] ==> x=y"; |
124 |
by (Blast_tac 1); |
|
4830 | 125 |
qed "inj_onD"; |
923 | 126 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
127 |
Goal "[| inj_on f A; x:A; y:A |] ==> (f(x)=f(y)) = (x=y)"; |
4830 | 128 |
by (blast_tac (claset() addSDs [inj_onD]) 1); |
129 |
qed "inj_on_iff"; |
|
923 | 130 |
|
5316 | 131 |
Goalw [inj_on_def] "[| inj_on f A; ~x=y; x:A; y:A |] ==> ~ f(x)=f(y)"; |
132 |
by (Blast_tac 1); |
|
4830 | 133 |
qed "inj_on_contraD"; |
923 | 134 |
|
5316 | 135 |
Goalw [inj_on_def] "[| A<=B; inj_on f B |] ==> inj_on f A"; |
3341 | 136 |
by (Blast_tac 1); |
4830 | 137 |
qed "subset_inj_on"; |
3341 | 138 |
|
923 | 139 |
|
140 |
(*** Lemmas about inj ***) |
|
141 |
||
5316 | 142 |
Goalw [o_def] "[| inj(f); inj_on g (range f) |] ==> inj(g o f)"; |
4830 | 143 |
by (fast_tac (claset() addIs [injI] addEs [injD, inj_onD]) 1); |
923 | 144 |
qed "comp_inj"; |
145 |
||
5316 | 146 |
Goal "inj(f) ==> inj_on f A"; |
147 |
by (blast_tac (claset() addIs [injD, inj_onI]) 1); |
|
923 | 148 |
qed "inj_imp"; |
149 |
||
5316 | 150 |
Goalw [inv_def] "y : range(f) ==> f(inv f y) = y"; |
151 |
by (fast_tac (claset() addIs [selectI]) 1); |
|
2912 | 152 |
qed "f_inv_f"; |
923 | 153 |
|
5316 | 154 |
Goal "[| inv f x=inv f y; x: range(f); y: range(f) |] ==> x=y"; |
2912 | 155 |
by (rtac (arg_cong RS box_equals) 1); |
5316 | 156 |
by (REPEAT (ares_tac [f_inv_f] 1)); |
2912 | 157 |
qed "inv_injective"; |
158 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
159 |
Goal "[| inj(f); A<=range(f) |] ==> inj_on (inv f) A"; |
4830 | 160 |
by (fast_tac (claset() addIs [inj_onI] |
2912 | 161 |
addEs [inv_injective,injD]) 1); |
4830 | 162 |
qed "inj_on_inv"; |
923 | 163 |
|
5069 | 164 |
Goalw [inj_on_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
165 |
"[| inj_on f C; A<=C; B<=C |] ==> f``(A Int B) = f``A Int f``B"; |
4059 | 166 |
by (Blast_tac 1); |
4830 | 167 |
qed "inj_on_image_Int"; |
4059 | 168 |
|
5069 | 169 |
Goalw [inj_on_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
170 |
"[| inj_on f C; A<=C; B<=C |] ==> f``(A-B) = f``A - f``B"; |
4059 | 171 |
by (Blast_tac 1); |
4830 | 172 |
qed "inj_on_image_set_diff"; |
4059 | 173 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
174 |
Goalw [inj_def] "inj f ==> f``(A Int B) = f``A Int f``B"; |
4059 | 175 |
by (Blast_tac 1); |
176 |
qed "image_Int"; |
|
177 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
178 |
Goalw [inj_def] "inj f ==> f``(A-B) = f``A - f``B"; |
4059 | 179 |
by (Blast_tac 1); |
180 |
qed "image_set_diff"; |
|
181 |
||
923 | 182 |
|
5847 | 183 |
|
184 |
val [major] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g"; |
|
185 |
by (blast_tac (claset() addIs [major RS sym]) 1); |
|
186 |
qed "surjI"; |
|
187 |
||
188 |
||
4089 | 189 |
val set_cs = claset() delrules [equalityI]; |
5305 | 190 |
|
191 |
||
192 |
section "fun_upd"; |
|
193 |
||
194 |
Goalw [fun_upd_def] "(f(x:=y) = f) = (f x = y)"; |
|
195 |
by Safe_tac; |
|
196 |
by (etac subst 1); |
|
197 |
by (rtac ext 2); |
|
198 |
by Auto_tac; |
|
199 |
qed "fun_upd_idem_iff"; |
|
200 |
||
201 |
(* f x = y ==> f(x:=y) = f *) |
|
202 |
bind_thm("fun_upd_idem", fun_upd_idem_iff RS iffD2); |
|
203 |
||
204 |
(* f(x := f x) = f *) |
|
205 |
AddIffs [refl RS fun_upd_idem]; |
|
206 |
||
207 |
Goal "(f(x:=y))z = (if z=x then y else f z)"; |
|
208 |
by (simp_tac (simpset() addsimps [fun_upd_def]) 1); |
|
209 |
qed "fun_upd_apply"; |
|
210 |
Addsimps [fun_upd_apply]; |
|
211 |
||
212 |
qed_goal "fun_upd_same" thy "(f(x:=y)) x = y" |
|
213 |
(K [Simp_tac 1]); |
|
5306 | 214 |
qed_goal "fun_upd_other" thy "!!X. z~=x ==> (f(x:=y)) z = f z" |
5305 | 215 |
(K [Asm_simp_tac 1]); |
216 |
(*Addsimps [fun_upd_same, fun_upd_other];*) |
|
217 |
||
218 |
Goal "a ~= c ==> m(a:=b)(c:=d) = m(c:=d)(a:=b)"; |
|
219 |
by (rtac ext 1); |
|
220 |
by (Auto_tac); |
|
221 |
qed "fun_upd_twist"; |