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