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