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