author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 1610  60ab5844fe81 
permissions  rwrr 
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 SchroederBernstein 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 FirstOrder Logic, JAR 2 (1986), 287327*) 

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 lambdaabstractions*) 
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:127, 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, highlevel 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"; 