0

1 
(* Title: ZF/perm.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1991 University of Cambridge


5 


6 
For perm.thy. The theory underlying permutation groups


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);


18 
val surj_is_fun = result();


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]


22 
addEs [range_of_fun,domain_type]) 1);


23 
val fun_is_surj = result();


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);


27 
val surj_range = result();


28 


29 


30 
(** Injective function space **)


31 


32 
goalw Perm.thy [inj_def] "!!f A B. f: inj(A,B) ==> f: A>B";


33 
by (etac CollectD1 1);


34 
val inj_is_fun = result();


35 


36 
goalw Perm.thy [inj_def]


37 
"!!f A B. [ <a,b>:f; <c,b>:f; f: inj(A,B) ] ==> a=c";


38 
by (REPEAT (eresolve_tac [asm_rl, Pair_mem_PiE, CollectE] 1));


39 
by (fast_tac ZF_cs 1);


40 
val inj_equality = result();


41 


42 
(** Bijections  simple lemmas but no intro/elim rules  use unfolding **)


43 


44 
goalw Perm.thy [bij_def] "!!f A B. f: bij(A,B) ==> f: inj(A,B)";


45 
by (etac IntD1 1);


46 
val bij_is_inj = result();


47 


48 
goalw Perm.thy [bij_def] "!!f A B. f: bij(A,B) ==> f: surj(A,B)";


49 
by (etac IntD2 1);


50 
val bij_is_surj = result();


51 


52 
(* f: bij(A,B) ==> f: A>B *)


53 
val bij_is_fun = standard (bij_is_inj RS inj_is_fun);


54 


55 
(** Identity function **)


56 


57 
val [prem] = goalw Perm.thy [id_def] "a:A ==> <a,a> : id(A)";


58 
by (rtac (prem RS lamI) 1);


59 
val idI = result();


60 


61 
val major::prems = goalw Perm.thy [id_def]


62 
"[ p: id(A); !!x.[ x:A; p=<x,x> ] ==> P \


63 
\ ] ==> P";


64 
by (rtac (major RS lamE) 1);


65 
by (REPEAT (ares_tac prems 1));


66 
val idE = result();


67 


68 
goalw Perm.thy [id_def] "id(A) : A>A";


69 
by (rtac lam_type 1);


70 
by (assume_tac 1);


71 
val id_type = result();


72 


73 
val [prem] = goalw Perm.thy [id_def] "A<=B ==> id(A) <= id(B)";


74 
by (rtac (prem RS lam_mono) 1);


75 
val id_mono = result();


76 


77 
goalw Perm.thy [inj_def,id_def] "id(A): inj(A,A)";


78 
by (REPEAT (ares_tac [CollectI,lam_type] 1));


79 
by (SIMP_TAC ZF_ss 1);


80 
val id_inj = result();


81 


82 
goalw Perm.thy [id_def,surj_def] "id(A): surj(A,A)";


83 
by (fast_tac (ZF_cs addIs [lam_type,beta]) 1);


84 
val id_surj = result();


85 


86 
goalw Perm.thy [bij_def] "id(A): bij(A,A)";


87 
by (fast_tac (ZF_cs addIs [id_inj,id_surj]) 1);


88 
val id_bij = result();


89 


90 


91 
(** Converse of a relation **)


92 


93 
val [prem] = goal Perm.thy "f: inj(A,B) ==> converse(f) : range(f)>A";


94 
by (rtac (prem RS inj_is_fun RS PiE) 1);


95 
by (rtac (converse_type RS PiI) 1);


96 
by (fast_tac ZF_cs 1);


97 
by (fast_tac (ZF_cs addEs [prem RSN (3,inj_equality)]) 1);


98 
by flexflex_tac;


99 
val inj_converse_fun = result();


100 


101 
val prems = goalw Perm.thy [surj_def]


102 
"f: inj(A,B) ==> converse(f): surj(range(f), A)";


103 
by (fast_tac (ZF_cs addIs (prems@[inj_converse_fun,apply_Pair,apply_equality,


104 
converseI,inj_is_fun])) 1);


105 
val inj_converse_surj = result();


106 


107 
(*The premises are equivalent to saying that f is injective...*)


108 
val prems = goal Perm.thy


109 
"[ f: A>B; converse(f): C>A; a: A ] ==> converse(f)`(f`a) = a";


110 
by (fast_tac (ZF_cs addIs (prems@[apply_Pair,apply_equality,converseI])) 1);


111 
val left_inverse_lemma = result();


112 


113 
val prems = goal Perm.thy


114 
"[ f: inj(A,B); a: A ] ==> converse(f)`(f`a) = a";


115 
by (fast_tac (ZF_cs addIs (prems@


116 
[left_inverse_lemma,inj_converse_fun,inj_is_fun])) 1);


117 
val left_inverse = result();


118 


119 
val prems = goal Perm.thy


120 
"[ f: A>B; converse(f): C>A; b: C ] ==> f`(converse(f)`b) = b";


121 
by (rtac (apply_Pair RS (converseD RS apply_equality)) 1);


122 
by (REPEAT (resolve_tac prems 1));


123 
val right_inverse_lemma = result();


124 


125 
val prems = goal Perm.thy


126 
"[ f: inj(A,B); b: range(f) ] ==> f`(converse(f)`b) = b";


127 
by (rtac right_inverse_lemma 1);


128 
by (REPEAT (resolve_tac (prems@ [inj_converse_fun,inj_is_fun]) 1));


129 
val right_inverse = result();


130 


131 
val prems = goal Perm.thy


132 
"f: inj(A,B) ==> converse(f): inj(range(f), A)";


133 
bw inj_def; (*rewrite subgoal but not prems!!*)


134 
by (cut_facts_tac prems 1);


135 
by (safe_tac ZF_cs);


136 
(*apply f to both sides and simplify using right_inverse


137 
 could also use etac[subst_context RS box_equals] in this proof *)


138 
by (rtac simp_equals 2);


139 
by (REPEAT (eresolve_tac [inj_converse_fun, right_inverse RS sym, ssubst] 1


140 
ORELSE ares_tac [refl,rangeI] 1));


141 
val inj_converse_inj = result();


142 


143 
goalw Perm.thy [bij_def] "!!f A B. f: bij(A,B) ==> converse(f): bij(B,A)";


144 
by (etac IntE 1);


145 
by (eresolve_tac [(surj_range RS subst)] 1);


146 
by (rtac IntI 1);


147 
by (etac inj_converse_inj 1);


148 
by (etac inj_converse_surj 1);


149 
val bij_converse_bij = result();


150 


151 


152 
(** Composition of two relations **)


153 


154 
(*The inductive definition package could derive these theorems for R o S*)


155 


156 
goalw Perm.thy [comp_def] "!!r s. [ <a,b>:s; <b,c>:r ] ==> <a,c> : r O s";


157 
by (fast_tac ZF_cs 1);


158 
val compI = result();


159 


160 
val prems = goalw Perm.thy [comp_def]


161 
"[ xz : r O s; \


162 
\ !!x y z. [ xz=<x,z>; <x,y>:s; <y,z>:r ] ==> P \


163 
\ ] ==> P";


164 
by (cut_facts_tac prems 1);


165 
by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1 ORELSE ares_tac prems 1));


166 
val compE = result();


167 


168 
val compEpair =


169 
rule_by_tactic (REPEAT_FIRST (etac Pair_inject ORELSE' bound_hyp_subst_tac)


170 
THEN prune_params_tac)


171 
(read_instantiate [("xz","<a,c>")] compE);


172 


173 
val comp_cs = ZF_cs addIs [compI,idI] addSEs [compE,idE];


174 


175 
(** Domain and Range  see Suppes, section 3.1 **)


176 


177 
(*Boyer et al., Set Theory in FirstOrder Logic, JAR 2 (1986), 287327*)


178 
goal Perm.thy "range(r O s) <= range(r)";


179 
by (fast_tac comp_cs 1);


180 
val range_comp = result();


181 


182 
goal Perm.thy "!!r s. domain(r) <= range(s) ==> range(r O s) = range(r)";


183 
by (rtac (range_comp RS equalityI) 1);


184 
by (fast_tac comp_cs 1);


185 
val range_comp_eq = result();


186 


187 
goal Perm.thy "domain(r O s) <= domain(s)";


188 
by (fast_tac comp_cs 1);


189 
val domain_comp = result();


190 


191 
goal Perm.thy "!!r s. range(s) <= domain(r) ==> domain(r O s) = domain(s)";


192 
by (rtac (domain_comp RS equalityI) 1);


193 
by (fast_tac comp_cs 1);


194 
val domain_comp_eq = result();


195 


196 
(** Other results **)


197 


198 
goal Perm.thy "!!r s. [ r'<=r; s'<=s ] ==> (r' O s') <= (r O s)";


199 
by (fast_tac comp_cs 1);


200 
val comp_mono = result();


201 


202 
(*composition preserves relations*)


203 
goal Perm.thy "!!r s. [ s<=A*B; r<=B*C ] ==> (r O s) <= A*C";


204 
by (fast_tac comp_cs 1);


205 
val comp_rel = result();


206 


207 
(*associative law for composition*)


208 
goal Perm.thy "(r O s) O t = r O (s O t)";


209 
by (fast_tac (comp_cs addIs [equalityI]) 1);


210 
val comp_assoc = result();


211 


212 
(*left identity of composition; provable inclusions are


213 
id(A) O r <= r


214 
and [ r<=A*B; B<=C ] ==> r <= id(C) O r *)


215 
goal Perm.thy "!!r A B. r<=A*B ==> id(B) O r = r";


216 
by (fast_tac (comp_cs addIs [equalityI]) 1);


217 
val left_comp_id = result();


218 


219 
(*right identity of composition; provable inclusions are


220 
r O id(A) <= r


221 
and [ r<=A*B; A<=C ] ==> r <= r O id(C) *)


222 
goal Perm.thy "!!r A B. r<=A*B ==> r O id(A) = r";


223 
by (fast_tac (comp_cs addIs [equalityI]) 1);


224 
val right_comp_id = result();


225 


226 


227 
(** Composition preserves functions, injections, and surjections **)


228 


229 
goal Perm.thy "!!f g. [ g: A>B; f: B>C ] ==> (f O g) : A>C";


230 
by (REPEAT (ares_tac [PiI,comp_rel,ex1I,compI] 1


231 
ORELSE eresolve_tac [fun_is_rel,apply_Pair,apply_type] 1));


232 
by (fast_tac (comp_cs addDs [apply_equality]) 1);


233 
val comp_func = result();


234 


235 
goal Perm.thy "!!f g. [ g: A>B; f: B>C; a:A ] ==> (f O g)`a = f`(g`a)";


236 
by (REPEAT (ares_tac [comp_func,apply_equality,compI,


237 
apply_Pair,apply_type] 1));


238 
val comp_func_apply = result();


239 


240 
goalw Perm.thy [inj_def]


241 
"!!f g. [ g: inj(A,B); f: inj(B,C) ] ==> (f O g) : inj(A,C)";


242 
by (REPEAT (eresolve_tac [bspec RS bspec RS mp, box_equals] 1


243 
ORELSE step_tac (ZF_cs addSIs [comp_func,apply_type,comp_func_apply]) 1));


244 
val comp_inj = result();


245 


246 
goalw Perm.thy [surj_def]


247 
"!!f g. [ g: surj(A,B); f: surj(B,C) ] ==> (f O g) : surj(A,C)";


248 
by (best_tac (ZF_cs addSIs [comp_func,comp_func_apply]) 1);


249 
val comp_surj = result();


250 


251 
goalw Perm.thy [bij_def]


252 
"!!f g. [ g: bij(A,B); f: bij(B,C) ] ==> (f O g) : bij(A,C)";


253 
by (fast_tac (ZF_cs addIs [comp_inj,comp_surj]) 1);


254 
val comp_bij = result();


255 


256 


257 
(** Dual properties of inj and surj  useful for proofs from


258 
D Pastre. Automatic theorem proving in set theory.


259 
Artificial Intelligence, 10:127, 1978. **)


260 


261 
goalw Perm.thy [inj_def]


262 
"!!f g. [ (f O g): inj(A,C); g: A>B; f: B>C ] ==> g: inj(A,B)";


263 
by (safe_tac comp_cs);


264 
by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));


265 
by (ASM_SIMP_TAC (ZF_ss addrews [comp_func_apply]) 1);


266 
val comp_mem_injD1 = result();


267 


268 
goalw Perm.thy [inj_def,surj_def]


269 
"!!f g. [ (f O g): inj(A,C); g: surj(A,B); f: B>C ] ==> f: inj(B,C)";


270 
by (safe_tac comp_cs);


271 
by (res_inst_tac [("x1", "x")] (bspec RS bexE) 1);


272 
by (eres_inst_tac [("x1", "w")] (bspec RS bexE) 3);


273 
by (REPEAT (assume_tac 1));


274 
by (safe_tac (comp_cs addSIs ZF_congs));


275 
by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));


276 
by (ASM_SIMP_TAC (ZF_ss addrews [comp_func_apply]) 1);


277 
val comp_mem_injD2 = result();


278 


279 
goalw Perm.thy [surj_def]


280 
"!!f g. [ (f O g): surj(A,C); g: A>B; f: B>C ] ==> f: surj(B,C)";


281 
by (fast_tac (comp_cs addSIs [comp_func_apply RS sym, apply_type]) 1);


282 
val comp_mem_surjD1 = result();


283 


284 
goal Perm.thy


285 
"!!f g. [ (f O g)`a = c; g: A>B; f: B>C; a:A ] ==> f`(g`a) = c";


286 
by (REPEAT (ares_tac [comp_func_apply RS sym RS trans] 1));


287 
val comp_func_applyD = result();


288 


289 
goalw Perm.thy [inj_def,surj_def]


290 
"!!f g. [ (f O g): surj(A,C); g: A>B; f: inj(B,C) ] ==> g: surj(A,B)";


291 
by (safe_tac comp_cs);


292 
by (eres_inst_tac [("x1", "f`y")] (bspec RS bexE) 1);


293 
by (REPEAT (ares_tac [apply_type] 1 ORELSE dtac comp_func_applyD 1));


294 
by (best_tac (comp_cs addSIs [apply_type]) 1);


295 
val comp_mem_surjD2 = result();


296 


297 


298 
(** inverses of composition **)


299 


300 
(*left inverse of composition; one inclusion is


301 
f: A>B ==> id(A) <= converse(f) O f *)


302 
val [prem] = goal Perm.thy


303 
"f: inj(A,B) ==> converse(f) O f = id(A)";


304 
val injfD = prem RSN (3,inj_equality);


305 
by (cut_facts_tac [prem RS inj_is_fun] 1);


306 
by (fast_tac (comp_cs addIs [equalityI,apply_Pair]


307 
addEs [domain_type, make_elim injfD]) 1);


308 
val left_comp_inverse = result();


309 


310 
(*right inverse of composition; one inclusion is


311 
f: A>B ==> f O converse(f) <= id(B) *)


312 
val [prem] = goalw Perm.thy [surj_def]


313 
"f: surj(A,B) ==> f O converse(f) = id(B)";


314 
val appfD = (prem RS CollectD1) RSN (3,apply_equality2);


315 
by (cut_facts_tac [prem] 1);


316 
by (rtac equalityI 1);


317 
by (best_tac (comp_cs addEs [domain_type, range_type, make_elim appfD]) 1);


318 
by (best_tac (comp_cs addIs [apply_Pair]) 1);


319 
val right_comp_inverse = result();


320 


321 
(*Injective case applies converse(f) to both sides then simplifies


322 
using left_inverse_lemma*)


323 
goalw Perm.thy [bij_def,inj_def,surj_def]


324 
"!!f A B. [ converse(f): B>A; f: A>B ] ==> f : bij(A,B)";


325 
val cf_cong = read_instantiate_sg (sign_of Perm.thy)


326 
[("t","%x.?f`x")] subst_context;


327 
by (fast_tac (ZF_cs addIs [left_inverse_lemma, right_inverse_lemma, apply_type]


328 
addEs [cf_cong RS box_equals]) 1);


329 
val invertible_imp_bijective = result();


330 


331 
(** Unions of functions  cf similar theorems on func.ML **)


332 


333 
goal Perm.thy "converse(r Un s) = converse(r) Un converse(s)";


334 
by (rtac equalityI 1);


335 
by (DEPTH_SOLVE_1


336 
(resolve_tac [Un_least,converse_mono, Un_upper1,Un_upper2] 2));


337 
by (fast_tac ZF_cs 1);


338 
val converse_of_Un = result();


339 


340 
goalw Perm.thy [surj_def]


341 
"!!f g. [ f: surj(A,B); g: surj(C,D); A Int C = 0 ] ==> \


342 
\ (f Un g) : surj(A Un C, B Un D)";


343 
by (DEPTH_SOLVE_1 (eresolve_tac [fun_disjoint_apply1, fun_disjoint_apply2] 1


344 
ORELSE ball_tac 1


345 
ORELSE (rtac trans 1 THEN atac 2)


346 
ORELSE step_tac (ZF_cs addIs [fun_disjoint_Un]) 1));


347 
val surj_disjoint_Un = result();


348 


349 
(*A simple, highlevel proof; the version for injections follows from it,


350 
using f:inj(A,B)<>f:bij(A,range(f)) *)


351 
goal Perm.thy


352 
"!!f g. [ f: bij(A,B); g: bij(C,D); A Int C = 0; B Int D = 0 ] ==> \


353 
\ (f Un g) : bij(A Un C, B Un D)";


354 
by (rtac invertible_imp_bijective 1);


355 
by (rtac (converse_of_Un RS ssubst) 1);


356 
by (REPEAT (ares_tac [fun_disjoint_Un, bij_is_fun, bij_converse_bij] 1));


357 
val bij_disjoint_Un = result();


358 


359 


360 
(** Restrictions as surjections and bijections *)


361 


362 
val prems = goalw Perm.thy [surj_def]


363 
"f: Pi(A,B) ==> f: surj(A, f``A)";


364 
val rls = apply_equality :: (prems RL [apply_Pair,Pi_type]);


365 
by (fast_tac (ZF_cs addIs rls) 1);


366 
val surj_image = result();


367 


368 
goal Perm.thy


369 
"!!f. [ f: Pi(C,B); A<=C ] ==> restrict(f,A)``A = f``A";


370 
by (rtac equalityI 1);


371 
by (SELECT_GOAL (rewtac restrict_def) 2);


372 
by (REPEAT (eresolve_tac [imageE, apply_equality RS subst] 2


373 
ORELSE ares_tac [subsetI,lamI,imageI] 2));


374 
by (REPEAT (ares_tac [image_mono,restrict_subset,subset_refl] 1));


375 
val restrict_image = result();


376 


377 
goalw Perm.thy [inj_def]


378 
"!!f. [ f: inj(A,B); C<=A ] ==> restrict(f,C): inj(C,B)";


379 
by (safe_tac (ZF_cs addSEs [restrict_type2]));


380 
by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp, subsetD,


381 
box_equals, restrict] 1));


382 
val restrict_inj = result();


383 


384 
val prems = goal Perm.thy


385 
"[ f: Pi(A,B); C<=A ] ==> restrict(f,C): surj(C, f``C)";


386 
by (rtac (restrict_image RS subst) 1);


387 
by (rtac (restrict_type2 RS surj_image) 3);


388 
by (REPEAT (resolve_tac prems 1));


389 
val restrict_surj = result();


390 


391 
goalw Perm.thy [inj_def,bij_def]


392 
"!!f. [ f: inj(A,B); C<=A ] ==> restrict(f,C): bij(C, f``C)";


393 
by (safe_tac ZF_cs);


394 
by (REPEAT (eresolve_tac [bspec RS bspec RS mp, subsetD,


395 
box_equals, restrict] 1


396 
ORELSE ares_tac [surj_is_fun,restrict_surj] 1));


397 
val restrict_bij = result();


398 


399 


400 
(*** Lemmas for Ramsey's Theorem ***)


401 


402 
goalw Perm.thy [inj_def] "!!f. [ f: inj(A,B); B<=D ] ==> f: inj(A,D)";


403 
by (fast_tac (ZF_cs addSEs [fun_weaken_type]) 1);


404 
val inj_weaken_type = result();


405 


406 
val [major] = goal Perm.thy


407 
"[ f: inj(succ(m), A) ] ==> restrict(f,m) : inj(m, A{f`m})";


408 
by (rtac (major RS restrict_bij RS bij_is_inj RS inj_weaken_type) 1);


409 
by (fast_tac ZF_cs 1);


410 
by (cut_facts_tac [major] 1);


411 
by (rewtac inj_def);


412 
by (safe_tac ZF_cs);


413 
by (etac range_type 1);


414 
by (assume_tac 1);


415 
by (dtac apply_equality 1);


416 
by (assume_tac 1);


417 
by (res_inst_tac [("a","m")] mem_anti_refl 1);


418 
by (fast_tac ZF_cs 1);


419 
val inj_succ_restrict = result();


420 


421 
goalw Perm.thy [inj_def]


422 
"!!f. [ f: inj(A,B); ~ a:A; ~ b:B ] ==> \


423 
\ cons(<a,b>,f) : inj(cons(a,A), cons(b,B))";


424 
(*cannot use safe_tac: must preserve the implication*)


425 
by (etac CollectE 1);


426 
by (rtac CollectI 1);


427 
by (etac fun_extend 1);


428 
by (REPEAT (ares_tac [ballI] 1));


429 
by (REPEAT_FIRST (eresolve_tac [consE,ssubst]));


430 
(*Assumption ALL w:A. ALL x:A. f`w = f`x > w=x makes ASM_SIMP_TAC loop!*)


431 
by (ALLGOALS (SIMP_TAC (ZF_ss addrews [fun_extend_apply2,fun_extend_apply1])));


432 
by (ALLGOALS (fast_tac (ZF_cs addIs [apply_type])));


433 
val inj_extend = result();
