author | paulson |
Mon, 23 Sep 1996 18:18:18 +0200 | |
changeset 2010 | 0a22b9d63a18 |
parent 1791 | 6b38717439c6 |
child 2033 | 639de962ded4 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/Perm.ML |
0 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1991 University of Cambridge |
5 |
||
735 | 6 |
The theory underlying permutation groups |
0 | 7 |
-- Composition of relations, the identity relation |
8 |
-- Injections, surjections, bijections |
|
9 |
-- Lemmas for the Schroeder-Bernstein Theorem |
|
10 |
*) |
|
11 |
||
12 |
open Perm; |
|
13 |
||
14 |
(** Surjective function space **) |
|
15 |
||
16 |
goalw Perm.thy [surj_def] "!!f A B. f: surj(A,B) ==> f: A->B"; |
|
17 |
by (etac CollectD1 1); |
|
760 | 18 |
qed "surj_is_fun"; |
0 | 19 |
|
20 |
goalw Perm.thy [surj_def] "!!f A B. f : Pi(A,B) ==> f: surj(A,range(f))"; |
|
21 |
by (fast_tac (ZF_cs addIs [apply_equality] |
|
1461 | 22 |
addEs [range_of_fun,domain_type]) 1); |
760 | 23 |
qed "fun_is_surj"; |
0 | 24 |
|
25 |
goalw Perm.thy [surj_def] "!!f A B. f: surj(A,B) ==> range(f)=B"; |
|
26 |
by (best_tac (ZF_cs addIs [equalityI,apply_Pair] addEs [range_type]) 1); |
|
760 | 27 |
qed "surj_range"; |
0 | 28 |
|
502
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
29 |
(** A function with a right inverse is a surjection **) |
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
30 |
|
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
31 |
val prems = goalw Perm.thy [surj_def] |
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
32 |
"[| f: A->B; !!y. y:B ==> d(y): A; !!y. y:B ==> f`d(y) = y \ |
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
33 |
\ |] ==> f: surj(A,B)"; |
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
34 |
by (fast_tac (ZF_cs addIs prems) 1); |
760 | 35 |
qed "f_imp_surjective"; |
502
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
36 |
|
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
37 |
val prems = goal Perm.thy |
1461 | 38 |
"[| !!x. x:A ==> c(x): B; \ |
39 |
\ !!y. y:B ==> d(y): A; \ |
|
40 |
\ !!y. y:B ==> c(d(y)) = y \ |
|
502
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
41 |
\ |] ==> (lam x:A.c(x)) : surj(A,B)"; |
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
42 |
by (res_inst_tac [("d", "d")] f_imp_surjective 1); |
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
43 |
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps ([lam_type]@prems)) )); |
760 | 44 |
qed "lam_surjective"; |
502
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
45 |
|
735 | 46 |
(*Cantor's theorem revisited*) |
47 |
goalw Perm.thy [surj_def] "f ~: surj(A,Pow(A))"; |
|
48 |
by (safe_tac ZF_cs); |
|
49 |
by (cut_facts_tac [cantor] 1); |
|
50 |
by (fast_tac subset_cs 1); |
|
760 | 51 |
qed "cantor_surj"; |
735 | 52 |
|
0 | 53 |
|
54 |
(** Injective function space **) |
|
55 |
||
56 |
goalw Perm.thy [inj_def] "!!f A B. f: inj(A,B) ==> f: A->B"; |
|
57 |
by (etac CollectD1 1); |
|
760 | 58 |
qed "inj_is_fun"; |
0 | 59 |
|
1787 | 60 |
(*Good for dealing with sets of pairs, but a bit ugly in use [used in AC]*) |
0 | 61 |
goalw Perm.thy [inj_def] |
62 |
"!!f A B. [| <a,b>:f; <c,b>:f; f: inj(A,B) |] ==> a=c"; |
|
63 |
by (REPEAT (eresolve_tac [asm_rl, Pair_mem_PiE, CollectE] 1)); |
|
64 |
by (fast_tac ZF_cs 1); |
|
760 | 65 |
qed "inj_equality"; |
0 | 66 |
|
826 | 67 |
goalw thy [inj_def] "!!A B f. [| f:inj(A,B); a:A; b:A; f`a=f`b |] ==> a=b"; |
68 |
by (fast_tac ZF_cs 1); |
|
69 |
val inj_apply_equality = result(); |
|
70 |
||
484 | 71 |
(** A function with a left inverse is an injection **) |
72 |
||
1787 | 73 |
goal Perm.thy "!!f. [| f: A->B; ALL x:A. d(f`x)=x |] ==> f: inj(A,B)"; |
74 |
by (asm_simp_tac (ZF_ss addsimps [inj_def]) 1); |
|
75 |
by (deepen_tac (ZF_cs addEs [subst_context RS box_equals]) 0 1); |
|
76 |
bind_thm ("f_imp_injective", ballI RSN (2,result())); |
|
484 | 77 |
|
78 |
val prems = goal Perm.thy |
|
1461 | 79 |
"[| !!x. x:A ==> c(x): B; \ |
80 |
\ !!x. x:A ==> d(c(x)) = x \ |
|
484 | 81 |
\ |] ==> (lam x:A.c(x)) : inj(A,B)"; |
82 |
by (res_inst_tac [("d", "d")] f_imp_injective 1); |
|
83 |
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps ([lam_type]@prems)) )); |
|
760 | 84 |
qed "lam_injective"; |
484 | 85 |
|
86 |
(** Bijections **) |
|
0 | 87 |
|
88 |
goalw Perm.thy [bij_def] "!!f A B. f: bij(A,B) ==> f: inj(A,B)"; |
|
89 |
by (etac IntD1 1); |
|
760 | 90 |
qed "bij_is_inj"; |
0 | 91 |
|
92 |
goalw Perm.thy [bij_def] "!!f A B. f: bij(A,B) ==> f: surj(A,B)"; |
|
93 |
by (etac IntD2 1); |
|
760 | 94 |
qed "bij_is_surj"; |
0 | 95 |
|
96 |
(* f: bij(A,B) ==> f: A->B *) |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
97 |
bind_thm ("bij_is_fun", (bij_is_inj RS inj_is_fun)); |
0 | 98 |
|
502
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
99 |
val prems = goalw Perm.thy [bij_def] |
1461 | 100 |
"[| !!x. x:A ==> c(x): B; \ |
101 |
\ !!y. y:B ==> d(y): A; \ |
|
102 |
\ !!x. x:A ==> d(c(x)) = x; \ |
|
103 |
\ !!y. y:B ==> c(d(y)) = y \ |
|
502
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
104 |
\ |] ==> (lam x:A.c(x)) : bij(A,B)"; |
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
105 |
by (REPEAT (ares_tac (prems @ [IntI, lam_injective, lam_surjective]) 1)); |
760 | 106 |
qed "lam_bijective"; |
502
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
107 |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
108 |
|
0 | 109 |
(** Identity function **) |
110 |
||
111 |
val [prem] = goalw Perm.thy [id_def] "a:A ==> <a,a> : id(A)"; |
|
112 |
by (rtac (prem RS lamI) 1); |
|
760 | 113 |
qed "idI"; |
0 | 114 |
|
115 |
val major::prems = goalw Perm.thy [id_def] |
|
116 |
"[| p: id(A); !!x.[| x:A; p=<x,x> |] ==> P \ |
|
117 |
\ |] ==> P"; |
|
118 |
by (rtac (major RS lamE) 1); |
|
119 |
by (REPEAT (ares_tac prems 1)); |
|
760 | 120 |
qed "idE"; |
0 | 121 |
|
122 |
goalw Perm.thy [id_def] "id(A) : A->A"; |
|
123 |
by (rtac lam_type 1); |
|
124 |
by (assume_tac 1); |
|
760 | 125 |
qed "id_type"; |
0 | 126 |
|
826 | 127 |
goalw Perm.thy [id_def] "!!A x. x:A ==> id(A)`x = x"; |
128 |
by (asm_simp_tac ZF_ss 1); |
|
129 |
val id_conv = result(); |
|
130 |
||
0 | 131 |
val [prem] = goalw Perm.thy [id_def] "A<=B ==> id(A) <= id(B)"; |
132 |
by (rtac (prem RS lam_mono) 1); |
|
760 | 133 |
qed "id_mono"; |
0 | 134 |
|
435 | 135 |
goalw Perm.thy [inj_def,id_def] "!!A B. A<=B ==> id(A): inj(A,B)"; |
0 | 136 |
by (REPEAT (ares_tac [CollectI,lam_type] 1)); |
435 | 137 |
by (etac subsetD 1 THEN assume_tac 1); |
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
138 |
by (simp_tac ZF_ss 1); |
760 | 139 |
qed "id_subset_inj"; |
435 | 140 |
|
141 |
val id_inj = subset_refl RS id_subset_inj; |
|
0 | 142 |
|
143 |
goalw Perm.thy [id_def,surj_def] "id(A): surj(A,A)"; |
|
144 |
by (fast_tac (ZF_cs addIs [lam_type,beta]) 1); |
|
760 | 145 |
qed "id_surj"; |
0 | 146 |
|
147 |
goalw Perm.thy [bij_def] "id(A): bij(A,A)"; |
|
148 |
by (fast_tac (ZF_cs addIs [id_inj,id_surj]) 1); |
|
760 | 149 |
qed "id_bij"; |
0 | 150 |
|
517 | 151 |
goalw Perm.thy [id_def] "A <= B <-> id(A) : A->B"; |
1787 | 152 |
by (fast_tac (ZF_cs addSIs [lam_type] addDs [apply_type] addss ZF_ss) 1); |
760 | 153 |
qed "subset_iff_id"; |
517 | 154 |
|
0 | 155 |
|
502
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
156 |
(*** Converse of a function ***) |
0 | 157 |
|
1787 | 158 |
goalw Perm.thy [inj_def] "!!f. f: inj(A,B) ==> converse(f) : range(f)->A"; |
1791
6b38717439c6
Addition of converse_iff, domain_converse, range_converse as rewrites
paulson
parents:
1787
diff
changeset
|
159 |
by (asm_simp_tac (ZF_ss addsimps [Pi_iff, function_def]) 1); |
1787 | 160 |
by (eresolve_tac [CollectE] 1); |
161 |
by (asm_simp_tac (ZF_ss addsimps [apply_iff]) 1); |
|
162 |
by (fast_tac (ZF_cs addDs [fun_is_rel]) 1); |
|
760 | 163 |
qed "inj_converse_fun"; |
0 | 164 |
|
502
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
165 |
(** Equations for converse(f) **) |
0 | 166 |
|
167 |
(*The premises are equivalent to saying that f is injective...*) |
|
168 |
val prems = goal Perm.thy |
|
169 |
"[| f: A->B; converse(f): C->A; a: A |] ==> converse(f)`(f`a) = a"; |
|
170 |
by (fast_tac (ZF_cs addIs (prems@[apply_Pair,apply_equality,converseI])) 1); |
|
760 | 171 |
qed "left_inverse_lemma"; |
0 | 172 |
|
435 | 173 |
goal Perm.thy |
174 |
"!!f. [| f: inj(A,B); a: A |] ==> converse(f)`(f`a) = a"; |
|
175 |
by (fast_tac (ZF_cs addIs [left_inverse_lemma,inj_converse_fun,inj_is_fun]) 1); |
|
760 | 176 |
qed "left_inverse"; |
0 | 177 |
|
435 | 178 |
val left_inverse_bij = bij_is_inj RS left_inverse; |
179 |
||
0 | 180 |
val prems = goal Perm.thy |
181 |
"[| f: A->B; converse(f): C->A; b: C |] ==> f`(converse(f)`b) = b"; |
|
182 |
by (rtac (apply_Pair RS (converseD RS apply_equality)) 1); |
|
183 |
by (REPEAT (resolve_tac prems 1)); |
|
760 | 184 |
qed "right_inverse_lemma"; |
0 | 185 |
|
502
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
186 |
(*Should the premises be f:surj(A,B), b:B for symmetry with left_inverse? |
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
187 |
No: they would not imply that converse(f) was a function! *) |
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
188 |
goal Perm.thy "!!f. [| f: inj(A,B); b: range(f) |] ==> f`(converse(f)`b) = b"; |
0 | 189 |
by (rtac right_inverse_lemma 1); |
435 | 190 |
by (REPEAT (ares_tac [inj_converse_fun,inj_is_fun] 1)); |
760 | 191 |
qed "right_inverse"; |
0 | 192 |
|
1787 | 193 |
goal Perm.thy "!!f. [| f: bij(A,B); b: B |] ==> f`(converse(f)`b) = b"; |
194 |
by (fast_tac (ZF_cs addss |
|
195 |
(ZF_ss addsimps [bij_def, right_inverse, surj_range])) 1); |
|
760 | 196 |
qed "right_inverse_bij"; |
435 | 197 |
|
502
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
198 |
(** Converses of injections, surjections, bijections **) |
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
199 |
|
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
200 |
goal Perm.thy "!!f A B. f: inj(A,B) ==> converse(f): inj(range(f), A)"; |
1461 | 201 |
by (rtac f_imp_injective 1); |
202 |
by (etac inj_converse_fun 1); |
|
203 |
by (rtac right_inverse 1); |
|
502
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
204 |
by (REPEAT (assume_tac 1)); |
760 | 205 |
qed "inj_converse_inj"; |
0 | 206 |
|
502
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
207 |
goal Perm.thy "!!f A B. f: inj(A,B) ==> converse(f): surj(range(f), A)"; |
1787 | 208 |
by (ITER_DEEPEN (has_fewer_prems 1) |
209 |
(ares_tac [f_imp_surjective, inj_converse_fun, left_inverse, |
|
210 |
inj_is_fun, range_of_fun RS apply_type])); |
|
760 | 211 |
qed "inj_converse_surj"; |
502
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
212 |
|
0 | 213 |
goalw Perm.thy [bij_def] "!!f A B. f: bij(A,B) ==> converse(f): bij(B,A)"; |
1787 | 214 |
by (fast_tac (ZF_cs addEs [surj_range RS subst, inj_converse_inj, |
215 |
inj_converse_surj]) 1); |
|
760 | 216 |
qed "bij_converse_bij"; |
0 | 217 |
|
218 |
||
219 |
(** Composition of two relations **) |
|
220 |
||
791 | 221 |
(*The inductive definition package could derive these theorems for (r O s)*) |
0 | 222 |
|
223 |
goalw Perm.thy [comp_def] "!!r s. [| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s"; |
|
224 |
by (fast_tac ZF_cs 1); |
|
760 | 225 |
qed "compI"; |
0 | 226 |
|
227 |
val prems = goalw Perm.thy [comp_def] |
|
228 |
"[| xz : r O s; \ |
|
229 |
\ !!x y z. [| xz=<x,z>; <x,y>:s; <y,z>:r |] ==> P \ |
|
230 |
\ |] ==> P"; |
|
231 |
by (cut_facts_tac prems 1); |
|
232 |
by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1 ORELSE ares_tac prems 1)); |
|
760 | 233 |
qed "compE"; |
0 | 234 |
|
235 |
val compEpair = |
|
236 |
rule_by_tactic (REPEAT_FIRST (etac Pair_inject ORELSE' bound_hyp_subst_tac) |
|
1461 | 237 |
THEN prune_params_tac) |
238 |
(read_instantiate [("xz","<a,c>")] compE); |
|
0 | 239 |
|
735 | 240 |
val comp_cs = ZF_cs addSIs [idI] addIs [compI] addSEs [compE,idE]; |
0 | 241 |
|
242 |
(** Domain and Range -- see Suppes, section 3.1 **) |
|
243 |
||
244 |
(*Boyer et al., Set Theory in First-Order Logic, JAR 2 (1986), 287-327*) |
|
245 |
goal Perm.thy "range(r O s) <= range(r)"; |
|
246 |
by (fast_tac comp_cs 1); |
|
760 | 247 |
qed "range_comp"; |
0 | 248 |
|
249 |
goal Perm.thy "!!r s. domain(r) <= range(s) ==> range(r O s) = range(r)"; |
|
250 |
by (rtac (range_comp RS equalityI) 1); |
|
251 |
by (fast_tac comp_cs 1); |
|
760 | 252 |
qed "range_comp_eq"; |
0 | 253 |
|
254 |
goal Perm.thy "domain(r O s) <= domain(s)"; |
|
255 |
by (fast_tac comp_cs 1); |
|
760 | 256 |
qed "domain_comp"; |
0 | 257 |
|
258 |
goal Perm.thy "!!r s. range(s) <= domain(r) ==> domain(r O s) = domain(s)"; |
|
259 |
by (rtac (domain_comp RS equalityI) 1); |
|
260 |
by (fast_tac comp_cs 1); |
|
760 | 261 |
qed "domain_comp_eq"; |
0 | 262 |
|
218 | 263 |
goal Perm.thy "(r O s)``A = r``(s``A)"; |
264 |
by (fast_tac (comp_cs addIs [equalityI]) 1); |
|
760 | 265 |
qed "image_comp"; |
218 | 266 |
|
267 |
||
0 | 268 |
(** Other results **) |
269 |
||
270 |
goal Perm.thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)"; |
|
271 |
by (fast_tac comp_cs 1); |
|
760 | 272 |
qed "comp_mono"; |
0 | 273 |
|
274 |
(*composition preserves relations*) |
|
275 |
goal Perm.thy "!!r s. [| s<=A*B; r<=B*C |] ==> (r O s) <= A*C"; |
|
276 |
by (fast_tac comp_cs 1); |
|
760 | 277 |
qed "comp_rel"; |
0 | 278 |
|
279 |
(*associative law for composition*) |
|
280 |
goal Perm.thy "(r O s) O t = r O (s O t)"; |
|
281 |
by (fast_tac (comp_cs addIs [equalityI]) 1); |
|
760 | 282 |
qed "comp_assoc"; |
0 | 283 |
|
284 |
(*left identity of composition; provable inclusions are |
|
285 |
id(A) O r <= r |
|
286 |
and [| r<=A*B; B<=C |] ==> r <= id(C) O r *) |
|
287 |
goal Perm.thy "!!r A B. r<=A*B ==> id(B) O r = r"; |
|
288 |
by (fast_tac (comp_cs addIs [equalityI]) 1); |
|
760 | 289 |
qed "left_comp_id"; |
0 | 290 |
|
291 |
(*right identity of composition; provable inclusions are |
|
292 |
r O id(A) <= r |
|
293 |
and [| r<=A*B; A<=C |] ==> r <= r O id(C) *) |
|
294 |
goal Perm.thy "!!r A B. r<=A*B ==> r O id(A) = r"; |
|
295 |
by (fast_tac (comp_cs addIs [equalityI]) 1); |
|
760 | 296 |
qed "right_comp_id"; |
0 | 297 |
|
298 |
||
299 |
(** Composition preserves functions, injections, and surjections **) |
|
300 |
||
693
b89939545725
ZF/Perm/inj_converse_fun: tidied; removed uses of PiI/E
lcp
parents:
517
diff
changeset
|
301 |
goalw Perm.thy [function_def] |
b89939545725
ZF/Perm/inj_converse_fun: tidied; removed uses of PiI/E
lcp
parents:
517
diff
changeset
|
302 |
"!!f g. [| function(g); function(f) |] ==> function(f O g)"; |
735 | 303 |
by (fast_tac (ZF_cs addIs [compI] addSEs [compE, Pair_inject]) 1); |
760 | 304 |
qed "comp_function"; |
693
b89939545725
ZF/Perm/inj_converse_fun: tidied; removed uses of PiI/E
lcp
parents:
517
diff
changeset
|
305 |
|
1787 | 306 |
goal Perm.thy "!!f g. [| g: A->B; f: B->C |] ==> (f O g) : A->C"; |
307 |
by (asm_full_simp_tac |
|
308 |
(ZF_ss addsimps [Pi_def, comp_function, Pow_iff, comp_rel] |
|
309 |
setloop etac conjE) 1); |
|
310 |
by (rtac (range_rel_subset RS domain_comp_eq RS ssubst) 1 THEN assume_tac 2); |
|
311 |
by (fast_tac ZF_cs 1); |
|
760 | 312 |
qed "comp_fun"; |
0 | 313 |
|
314 |
goal Perm.thy "!!f g. [| g: A->B; f: B->C; a:A |] ==> (f O g)`a = f`(g`a)"; |
|
435 | 315 |
by (REPEAT (ares_tac [comp_fun,apply_equality,compI, |
1461 | 316 |
apply_Pair,apply_type] 1)); |
760 | 317 |
qed "comp_fun_apply"; |
0 | 318 |
|
862 | 319 |
(*Simplifies compositions of lambda-abstractions*) |
320 |
val [prem] = goal Perm.thy |
|
1461 | 321 |
"[| !!x. x:A ==> b(x): B \ |
862 | 322 |
\ |] ==> (lam y:B.c(y)) O (lam x:A. b(x)) = (lam x:A. c(b(x)))"; |
1461 | 323 |
by (rtac fun_extension 1); |
324 |
by (rtac comp_fun 1); |
|
325 |
by (rtac lam_funtype 2); |
|
862 | 326 |
by (typechk_tac (prem::ZF_typechecks)); |
327 |
by (asm_simp_tac (ZF_ss addsimps [comp_fun_apply] |
|
328 |
setsolver type_auto_tac [lam_type, lam_funtype, prem]) 1); |
|
329 |
qed "comp_lam"; |
|
330 |
||
502
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
331 |
goal Perm.thy "!!f g. [| g: inj(A,B); f: inj(B,C) |] ==> (f O g) : inj(A,C)"; |
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
332 |
by (res_inst_tac [("d", "%y. converse(g) ` (converse(f) ` y)")] |
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
333 |
f_imp_injective 1); |
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
334 |
by (REPEAT (ares_tac [comp_fun, inj_is_fun] 1)); |
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
335 |
by (asm_simp_tac (ZF_ss addsimps [comp_fun_apply, left_inverse] |
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
336 |
setsolver type_auto_tac [inj_is_fun, apply_type]) 1); |
760 | 337 |
qed "comp_inj"; |
0 | 338 |
|
339 |
goalw Perm.thy [surj_def] |
|
340 |
"!!f g. [| g: surj(A,B); f: surj(B,C) |] ==> (f O g) : surj(A,C)"; |
|
435 | 341 |
by (best_tac (ZF_cs addSIs [comp_fun,comp_fun_apply]) 1); |
760 | 342 |
qed "comp_surj"; |
0 | 343 |
|
344 |
goalw Perm.thy [bij_def] |
|
345 |
"!!f g. [| g: bij(A,B); f: bij(B,C) |] ==> (f O g) : bij(A,C)"; |
|
346 |
by (fast_tac (ZF_cs addIs [comp_inj,comp_surj]) 1); |
|
760 | 347 |
qed "comp_bij"; |
0 | 348 |
|
349 |
||
350 |
(** Dual properties of inj and surj -- useful for proofs from |
|
351 |
D Pastre. Automatic theorem proving in set theory. |
|
352 |
Artificial Intelligence, 10:1--27, 1978. **) |
|
353 |
||
354 |
goalw Perm.thy [inj_def] |
|
355 |
"!!f g. [| (f O g): inj(A,C); g: A->B; f: B->C |] ==> g: inj(A,B)"; |
|
356 |
by (safe_tac comp_cs); |
|
357 |
by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1)); |
|
435 | 358 |
by (asm_simp_tac (FOL_ss addsimps [comp_fun_apply]) 1); |
760 | 359 |
qed "comp_mem_injD1"; |
0 | 360 |
|
361 |
goalw Perm.thy [inj_def,surj_def] |
|
362 |
"!!f g. [| (f O g): inj(A,C); g: surj(A,B); f: B->C |] ==> f: inj(B,C)"; |
|
363 |
by (safe_tac comp_cs); |
|
364 |
by (res_inst_tac [("x1", "x")] (bspec RS bexE) 1); |
|
365 |
by (eres_inst_tac [("x1", "w")] (bspec RS bexE) 3); |
|
366 |
by (REPEAT (assume_tac 1)); |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
367 |
by (safe_tac comp_cs); |
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
368 |
by (res_inst_tac [("t", "op `(g)")] subst_context 1); |
0 | 369 |
by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1)); |
435 | 370 |
by (asm_simp_tac (FOL_ss addsimps [comp_fun_apply]) 1); |
760 | 371 |
qed "comp_mem_injD2"; |
0 | 372 |
|
373 |
goalw Perm.thy [surj_def] |
|
374 |
"!!f g. [| (f O g): surj(A,C); g: A->B; f: B->C |] ==> f: surj(B,C)"; |
|
435 | 375 |
by (fast_tac (comp_cs addSIs [comp_fun_apply RS sym, apply_type]) 1); |
760 | 376 |
qed "comp_mem_surjD1"; |
0 | 377 |
|
378 |
goal Perm.thy |
|
379 |
"!!f g. [| (f O g)`a = c; g: A->B; f: B->C; a:A |] ==> f`(g`a) = c"; |
|
435 | 380 |
by (REPEAT (ares_tac [comp_fun_apply RS sym RS trans] 1)); |
760 | 381 |
qed "comp_fun_applyD"; |
0 | 382 |
|
383 |
goalw Perm.thy [inj_def,surj_def] |
|
384 |
"!!f g. [| (f O g): surj(A,C); g: A->B; f: inj(B,C) |] ==> g: surj(A,B)"; |
|
385 |
by (safe_tac comp_cs); |
|
386 |
by (eres_inst_tac [("x1", "f`y")] (bspec RS bexE) 1); |
|
435 | 387 |
by (REPEAT (ares_tac [apply_type] 1 ORELSE dtac comp_fun_applyD 1)); |
0 | 388 |
by (best_tac (comp_cs addSIs [apply_type]) 1); |
760 | 389 |
qed "comp_mem_surjD2"; |
0 | 390 |
|
391 |
||
392 |
(** inverses of composition **) |
|
393 |
||
394 |
(*left inverse of composition; one inclusion is |
|
395 |
f: A->B ==> id(A) <= converse(f) O f *) |
|
1787 | 396 |
goalw Perm.thy [inj_def] "!!f. f: inj(A,B) ==> converse(f) O f = id(A)"; |
397 |
by (fast_tac (comp_cs addIs [equalityI, apply_Pair] |
|
398 |
addEs [domain_type] |
|
399 |
addss (ZF_ss addsimps [apply_iff])) 1); |
|
760 | 400 |
qed "left_comp_inverse"; |
0 | 401 |
|
402 |
(*right inverse of composition; one inclusion is |
|
1461 | 403 |
f: A->B ==> f O converse(f) <= id(B) |
735 | 404 |
*) |
0 | 405 |
val [prem] = goalw Perm.thy [surj_def] |
406 |
"f: surj(A,B) ==> f O converse(f) = id(B)"; |
|
407 |
val appfD = (prem RS CollectD1) RSN (3,apply_equality2); |
|
408 |
by (cut_facts_tac [prem] 1); |
|
409 |
by (rtac equalityI 1); |
|
410 |
by (best_tac (comp_cs addEs [domain_type, range_type, make_elim appfD]) 1); |
|
411 |
by (best_tac (comp_cs addIs [apply_Pair]) 1); |
|
760 | 412 |
qed "right_comp_inverse"; |
0 | 413 |
|
435 | 414 |
(** Proving that a function is a bijection **) |
415 |
||
416 |
goalw Perm.thy [id_def] |
|
417 |
"!!f A B. [| f: A->B; g: B->A |] ==> \ |
|
418 |
\ f O g = id(B) <-> (ALL y:B. f`(g`y)=y)"; |
|
419 |
by (safe_tac ZF_cs); |
|
420 |
by (dres_inst_tac [("t", "%h.h`y ")] subst_context 1); |
|
421 |
by (asm_full_simp_tac (ZF_ss addsimps [comp_fun_apply]) 1); |
|
437 | 422 |
by (rtac fun_extension 1); |
435 | 423 |
by (REPEAT (ares_tac [comp_fun, lam_type] 1)); |
424 |
by (asm_simp_tac (ZF_ss addsimps [comp_fun_apply]) 1); |
|
760 | 425 |
qed "comp_eq_id_iff"; |
435 | 426 |
|
502
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
427 |
goalw Perm.thy [bij_def] |
435 | 428 |
"!!f A B. [| f: A->B; g: B->A; f O g = id(B); g O f = id(A) \ |
429 |
\ |] ==> f : bij(A,B)"; |
|
430 |
by (asm_full_simp_tac (ZF_ss addsimps [comp_eq_id_iff]) 1); |
|
502
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
431 |
by (REPEAT (ares_tac [conjI, f_imp_injective, f_imp_surjective] 1 |
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
432 |
ORELSE eresolve_tac [bspec, apply_type] 1)); |
760 | 433 |
qed "fg_imp_bijective"; |
435 | 434 |
|
435 |
goal Perm.thy "!!f A. [| f: A->A; f O f = id(A) |] ==> f : bij(A,A)"; |
|
436 |
by (REPEAT (ares_tac [fg_imp_bijective] 1)); |
|
760 | 437 |
qed "nilpotent_imp_bijective"; |
435 | 438 |
|
502
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
439 |
goal Perm.thy "!!f A B. [| converse(f): B->A; f: A->B |] ==> f : bij(A,B)"; |
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
440 |
by (asm_simp_tac (ZF_ss addsimps [fg_imp_bijective, comp_eq_id_iff, |
1461 | 441 |
left_inverse_lemma, right_inverse_lemma]) 1); |
760 | 442 |
qed "invertible_imp_bijective"; |
0 | 443 |
|
444 |
(** Unions of functions -- cf similar theorems on func.ML **) |
|
445 |
||
1709 | 446 |
(*Theorem by KG, proof by LCP*) |
447 |
goal Perm.thy |
|
448 |
"!!f g. [| f: inj(A,B); g: inj(C,D); B Int D = 0 |] ==> \ |
|
449 |
\ (lam a: A Un C. if(a:A, f`a, g`a)) : inj(A Un C, B Un D)"; |
|
450 |
by (res_inst_tac [("d","%z. if(z:B, converse(f)`z, converse(g)`z)")] |
|
451 |
lam_injective 1); |
|
452 |
by (ALLGOALS |
|
453 |
(asm_simp_tac (ZF_ss addsimps [inj_is_fun RS apply_type, left_inverse] |
|
454 |
setloop (split_tac [expand_if] ORELSE' etac UnE)))); |
|
455 |
by (fast_tac (ZF_cs addSEs [inj_is_fun RS apply_type] addDs [equals0D]) 1); |
|
456 |
qed "inj_disjoint_Un"; |
|
1610 | 457 |
|
0 | 458 |
goalw Perm.thy [surj_def] |
459 |
"!!f g. [| f: surj(A,B); g: surj(C,D); A Int C = 0 |] ==> \ |
|
460 |
\ (f Un g) : surj(A Un C, B Un D)"; |
|
461 |
by (DEPTH_SOLVE_1 (eresolve_tac [fun_disjoint_apply1, fun_disjoint_apply2] 1 |
|
1461 | 462 |
ORELSE ball_tac 1 |
463 |
ORELSE (rtac trans 1 THEN atac 2) |
|
464 |
ORELSE step_tac (ZF_cs addIs [fun_disjoint_Un]) 1)); |
|
760 | 465 |
qed "surj_disjoint_Un"; |
0 | 466 |
|
467 |
(*A simple, high-level proof; the version for injections follows from it, |
|
502
77e36960fd9e
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp
parents:
484
diff
changeset
|
468 |
using f:inj(A,B) <-> f:bij(A,range(f)) *) |
0 | 469 |
goal Perm.thy |
470 |
"!!f g. [| f: bij(A,B); g: bij(C,D); A Int C = 0; B Int D = 0 |] ==> \ |
|
471 |
\ (f Un g) : bij(A Un C, B Un D)"; |
|
472 |
by (rtac invertible_imp_bijective 1); |
|
791 | 473 |
by (rtac (converse_Un RS ssubst) 1); |
0 | 474 |
by (REPEAT (ares_tac [fun_disjoint_Un, bij_is_fun, bij_converse_bij] 1)); |
760 | 475 |
qed "bij_disjoint_Un"; |
0 | 476 |
|
477 |
||
478 |
(** Restrictions as surjections and bijections *) |
|
479 |
||
480 |
val prems = goalw Perm.thy [surj_def] |
|
481 |
"f: Pi(A,B) ==> f: surj(A, f``A)"; |
|
482 |
val rls = apply_equality :: (prems RL [apply_Pair,Pi_type]); |
|
483 |
by (fast_tac (ZF_cs addIs rls) 1); |
|
760 | 484 |
qed "surj_image"; |
0 | 485 |
|
735 | 486 |
goal Perm.thy "!!f. [| f: Pi(C,B); A<=C |] ==> restrict(f,A)``A = f``A"; |
0 | 487 |
by (rtac equalityI 1); |
488 |
by (SELECT_GOAL (rewtac restrict_def) 2); |
|
489 |
by (REPEAT (eresolve_tac [imageE, apply_equality RS subst] 2 |
|
490 |
ORELSE ares_tac [subsetI,lamI,imageI] 2)); |
|
491 |
by (REPEAT (ares_tac [image_mono,restrict_subset,subset_refl] 1)); |
|
760 | 492 |
qed "restrict_image"; |
0 | 493 |
|
494 |
goalw Perm.thy [inj_def] |
|
495 |
"!!f. [| f: inj(A,B); C<=A |] ==> restrict(f,C): inj(C,B)"; |
|
496 |
by (safe_tac (ZF_cs addSEs [restrict_type2])); |
|
497 |
by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp, subsetD, |
|
498 |
box_equals, restrict] 1)); |
|
760 | 499 |
qed "restrict_inj"; |
0 | 500 |
|
501 |
val prems = goal Perm.thy |
|
502 |
"[| f: Pi(A,B); C<=A |] ==> restrict(f,C): surj(C, f``C)"; |
|
503 |
by (rtac (restrict_image RS subst) 1); |
|
504 |
by (rtac (restrict_type2 RS surj_image) 3); |
|
505 |
by (REPEAT (resolve_tac prems 1)); |
|
760 | 506 |
qed "restrict_surj"; |
0 | 507 |
|
508 |
goalw Perm.thy [inj_def,bij_def] |
|
509 |
"!!f. [| f: inj(A,B); C<=A |] ==> restrict(f,C): bij(C, f``C)"; |
|
510 |
by (safe_tac ZF_cs); |
|
511 |
by (REPEAT (eresolve_tac [bspec RS bspec RS mp, subsetD, |
|
512 |
box_equals, restrict] 1 |
|
513 |
ORELSE ares_tac [surj_is_fun,restrict_surj] 1)); |
|
760 | 514 |
qed "restrict_bij"; |
0 | 515 |
|
516 |
||
517 |
(*** Lemmas for Ramsey's Theorem ***) |
|
518 |
||
519 |
goalw Perm.thy [inj_def] "!!f. [| f: inj(A,B); B<=D |] ==> f: inj(A,D)"; |
|
520 |
by (fast_tac (ZF_cs addSEs [fun_weaken_type]) 1); |
|
760 | 521 |
qed "inj_weaken_type"; |
0 | 522 |
|
523 |
val [major] = goal Perm.thy |
|
524 |
"[| f: inj(succ(m), A) |] ==> restrict(f,m) : inj(m, A-{f`m})"; |
|
525 |
by (rtac (major RS restrict_bij RS bij_is_inj RS inj_weaken_type) 1); |
|
526 |
by (fast_tac ZF_cs 1); |
|
527 |
by (cut_facts_tac [major] 1); |
|
528 |
by (rewtac inj_def); |
|
1782 | 529 |
by (fast_tac (ZF_cs addEs [range_type, mem_irrefl] addDs [apply_equality]) 1); |
760 | 530 |
qed "inj_succ_restrict"; |
0 | 531 |
|
532 |
goalw Perm.thy [inj_def] |
|
37 | 533 |
"!!f. [| f: inj(A,B); a~:A; b~:B |] ==> \ |
0 | 534 |
\ cons(<a,b>,f) : inj(cons(a,A), cons(b,B))"; |
1787 | 535 |
by (fast_tac (ZF_cs addIs [apply_type] |
536 |
addss (ZF_ss addsimps [fun_extend, fun_extend_apply2, |
|
537 |
fun_extend_apply1]) ) 1); |
|
760 | 538 |
qed "inj_extend"; |
1787 | 539 |