src/ZF/Perm.thy
 author wenzelm Sun Oct 07 21:19:31 2007 +0200 (2007-10-07) changeset 24893 b8ef7afe3a6b parent 16417 9bc16273c2d4 child 32960 69916a850301 permissions -rw-r--r--
modernized specifications;
removed legacy ML bindings;
```     1 (*  Title:      ZF/perm
```
```     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 header{*Injections, Surjections, Bijections, Composition*}
```
```    13
```
```    14 theory Perm imports func begin
```
```    15
```
```    16 definition
```
```    17   (*composition of relations and functions; NOT Suppes's relative product*)
```
```    18   comp     :: "[i,i]=>i"      (infixr "O" 60)  where
```
```    19     "r O s == {xz : domain(s)*range(r) .
```
```    20                EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
```
```    21
```
```    22 definition
```
```    23   (*the identity function for A*)
```
```    24   id    :: "i=>i"  where
```
```    25     "id(A) == (lam x:A. x)"
```
```    26
```
```    27 definition
```
```    28   (*one-to-one functions from A to B*)
```
```    29   inj   :: "[i,i]=>i"  where
```
```    30     "inj(A,B) == { f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x}"
```
```    31
```
```    32 definition
```
```    33   (*onto functions from A to B*)
```
```    34   surj  :: "[i,i]=>i"  where
```
```    35     "surj(A,B) == { f: A->B . ALL y:B. EX x:A. f`x=y}"
```
```    36
```
```    37 definition
```
```    38   (*one-to-one and onto functions*)
```
```    39   bij   :: "[i,i]=>i"  where
```
```    40     "bij(A,B) == inj(A,B) Int surj(A,B)"
```
```    41
```
```    42
```
```    43 subsection{*Surjections*}
```
```    44
```
```    45 (** Surjective function space **)
```
```    46
```
```    47 lemma surj_is_fun: "f: surj(A,B) ==> f: A->B"
```
```    48 apply (unfold surj_def)
```
```    49 apply (erule CollectD1)
```
```    50 done
```
```    51
```
```    52 lemma fun_is_surj: "f : Pi(A,B) ==> f: surj(A,range(f))"
```
```    53 apply (unfold surj_def)
```
```    54 apply (blast intro: apply_equality range_of_fun domain_type)
```
```    55 done
```
```    56
```
```    57 lemma surj_range: "f: surj(A,B) ==> range(f)=B"
```
```    58 apply (unfold surj_def)
```
```    59 apply (best intro: apply_Pair elim: range_type)
```
```    60 done
```
```    61
```
```    62 (** A function with a right inverse is a surjection **)
```
```    63
```
```    64 lemma f_imp_surjective:
```
```    65     "[| f: A->B;  !!y. y:B ==> d(y): A;  !!y. y:B ==> f`d(y) = y |]
```
```    66      ==> f: surj(A,B)"
```
```    67 apply (simp add: surj_def, blast)
```
```    68 done
```
```    69
```
```    70 lemma lam_surjective:
```
```    71     "[| !!x. x:A ==> c(x): B;
```
```    72         !!y. y:B ==> d(y): A;
```
```    73         !!y. y:B ==> c(d(y)) = y
```
```    74      |] ==> (lam x:A. c(x)) : surj(A,B)"
```
```    75 apply (rule_tac d = d in f_imp_surjective)
```
```    76 apply (simp_all add: lam_type)
```
```    77 done
```
```    78
```
```    79 (*Cantor's theorem revisited*)
```
```    80 lemma cantor_surj: "f ~: surj(A,Pow(A))"
```
```    81 apply (unfold surj_def, safe)
```
```    82 apply (cut_tac cantor)
```
```    83 apply (best del: subsetI)
```
```    84 done
```
```    85
```
```    86
```
```    87 subsection{*Injections*}
```
```    88
```
```    89 (** Injective function space **)
```
```    90
```
```    91 lemma inj_is_fun: "f: inj(A,B) ==> f: A->B"
```
```    92 apply (unfold inj_def)
```
```    93 apply (erule CollectD1)
```
```    94 done
```
```    95
```
```    96 (*Good for dealing with sets of pairs, but a bit ugly in use [used in AC]*)
```
```    97 lemma inj_equality:
```
```    98     "[| <a,b>:f;  <c,b>:f;  f: inj(A,B) |] ==> a=c"
```
```    99 apply (unfold inj_def)
```
```   100 apply (blast dest: Pair_mem_PiD)
```
```   101 done
```
```   102
```
```   103 lemma inj_apply_equality: "[| f:inj(A,B);  f`a=f`b;  a:A;  b:A |] ==> a=b"
```
```   104 by (unfold inj_def, blast)
```
```   105
```
```   106
```
```   107 (** A function with a left inverse is an injection **)
```
```   108
```
```   109 lemma f_imp_injective: "[| f: A->B;  ALL x:A. d(f`x)=x |] ==> f: inj(A,B)"
```
```   110 apply (simp (no_asm_simp) add: inj_def)
```
```   111 apply (blast intro: subst_context [THEN box_equals])
```
```   112 done
```
```   113
```
```   114 lemma lam_injective:
```
```   115     "[| !!x. x:A ==> c(x): B;
```
```   116         !!x. x:A ==> d(c(x)) = x |]
```
```   117      ==> (lam x:A. c(x)) : inj(A,B)"
```
```   118 apply (rule_tac d = d in f_imp_injective)
```
```   119 apply (simp_all add: lam_type)
```
```   120 done
```
```   121
```
```   122 subsection{*Bijections*}
```
```   123
```
```   124 lemma bij_is_inj: "f: bij(A,B) ==> f: inj(A,B)"
```
```   125 apply (unfold bij_def)
```
```   126 apply (erule IntD1)
```
```   127 done
```
```   128
```
```   129 lemma bij_is_surj: "f: bij(A,B) ==> f: surj(A,B)"
```
```   130 apply (unfold bij_def)
```
```   131 apply (erule IntD2)
```
```   132 done
```
```   133
```
```   134 (* f: bij(A,B) ==> f: A->B *)
```
```   135 lemmas bij_is_fun = bij_is_inj [THEN inj_is_fun, standard]
```
```   136
```
```   137 lemma lam_bijective:
```
```   138     "[| !!x. x:A ==> c(x): B;
```
```   139         !!y. y:B ==> d(y): A;
```
```   140         !!x. x:A ==> d(c(x)) = x;
```
```   141         !!y. y:B ==> c(d(y)) = y
```
```   142      |] ==> (lam x:A. c(x)) : bij(A,B)"
```
```   143 apply (unfold bij_def)
```
```   144 apply (blast intro!: lam_injective lam_surjective)
```
```   145 done
```
```   146
```
```   147 lemma RepFun_bijective: "(ALL y : x. EX! y'. f(y') = f(y))
```
```   148       ==> (lam z:{f(y). y:x}. THE y. f(y) = z) : bij({f(y). y:x}, x)"
```
```   149 apply (rule_tac d = f in lam_bijective)
```
```   150 apply (auto simp add: the_equality2)
```
```   151 done
```
```   152
```
```   153
```
```   154 subsection{*Identity Function*}
```
```   155
```
```   156 lemma idI [intro!]: "a:A ==> <a,a> : id(A)"
```
```   157 apply (unfold id_def)
```
```   158 apply (erule lamI)
```
```   159 done
```
```   160
```
```   161 lemma idE [elim!]: "[| p: id(A);  !!x.[| x:A; p=<x,x> |] ==> P |] ==>  P"
```
```   162 by (simp add: id_def lam_def, blast)
```
```   163
```
```   164 lemma id_type: "id(A) : A->A"
```
```   165 apply (unfold id_def)
```
```   166 apply (rule lam_type, assumption)
```
```   167 done
```
```   168
```
```   169 lemma id_conv [simp]: "x:A ==> id(A)`x = x"
```
```   170 apply (unfold id_def)
```
```   171 apply (simp (no_asm_simp))
```
```   172 done
```
```   173
```
```   174 lemma id_mono: "A<=B ==> id(A) <= id(B)"
```
```   175 apply (unfold id_def)
```
```   176 apply (erule lam_mono)
```
```   177 done
```
```   178
```
```   179 lemma id_subset_inj: "A<=B ==> id(A): inj(A,B)"
```
```   180 apply (simp add: inj_def id_def)
```
```   181 apply (blast intro: lam_type)
```
```   182 done
```
```   183
```
```   184 lemmas id_inj = subset_refl [THEN id_subset_inj, standard]
```
```   185
```
```   186 lemma id_surj: "id(A): surj(A,A)"
```
```   187 apply (unfold id_def surj_def)
```
```   188 apply (simp (no_asm_simp))
```
```   189 done
```
```   190
```
```   191 lemma id_bij: "id(A): bij(A,A)"
```
```   192 apply (unfold bij_def)
```
```   193 apply (blast intro: id_inj id_surj)
```
```   194 done
```
```   195
```
```   196 lemma subset_iff_id: "A <= B <-> id(A) : A->B"
```
```   197 apply (unfold id_def)
```
```   198 apply (force intro!: lam_type dest: apply_type)
```
```   199 done
```
```   200
```
```   201 text{*@{term id} as the identity relation*}
```
```   202 lemma id_iff [simp]: "<x,y> \<in> id(A) <-> x=y & y \<in> A"
```
```   203 by auto
```
```   204
```
```   205
```
```   206
```
```   207 subsection{*Converse of a Function*}
```
```   208
```
```   209 lemma inj_converse_fun: "f: inj(A,B) ==> converse(f) : range(f)->A"
```
```   210 apply (unfold inj_def)
```
```   211 apply (simp (no_asm_simp) add: Pi_iff function_def)
```
```   212 apply (erule CollectE)
```
```   213 apply (simp (no_asm_simp) add: apply_iff)
```
```   214 apply (blast dest: fun_is_rel)
```
```   215 done
```
```   216
```
```   217 (** Equations for converse(f) **)
```
```   218
```
```   219 text{*The premises are equivalent to saying that f is injective...*}
```
```   220 lemma left_inverse_lemma:
```
```   221      "[| f: A->B;  converse(f): C->A;  a: A |] ==> converse(f)`(f`a) = a"
```
```   222 by (blast intro: apply_Pair apply_equality converseI)
```
```   223
```
```   224 lemma left_inverse [simp]: "[| f: inj(A,B);  a: A |] ==> converse(f)`(f`a) = a"
```
```   225 by (blast intro: left_inverse_lemma inj_converse_fun inj_is_fun)
```
```   226
```
```   227 lemma left_inverse_eq:
```
```   228      "[|f \<in> inj(A,B); f ` x = y; x \<in> A|] ==> converse(f) ` y = x"
```
```   229 by auto
```
```   230
```
```   231 lemmas left_inverse_bij = bij_is_inj [THEN left_inverse, standard]
```
```   232
```
```   233 lemma right_inverse_lemma:
```
```   234      "[| f: A->B;  converse(f): C->A;  b: C |] ==> f`(converse(f)`b) = b"
```
```   235 by (rule apply_Pair [THEN converseD [THEN apply_equality]], auto)
```
```   236
```
```   237 (*Should the premises be f:surj(A,B), b:B for symmetry with left_inverse?
```
```   238   No: they would not imply that converse(f) was a function! *)
```
```   239 lemma right_inverse [simp]:
```
```   240      "[| f: inj(A,B);  b: range(f) |] ==> f`(converse(f)`b) = b"
```
```   241 by (blast intro: right_inverse_lemma inj_converse_fun inj_is_fun)
```
```   242
```
```   243 lemma right_inverse_bij: "[| f: bij(A,B);  b: B |] ==> f`(converse(f)`b) = b"
```
```   244 by (force simp add: bij_def surj_range)
```
```   245
```
```   246 subsection{*Converses of Injections, Surjections, Bijections*}
```
```   247
```
```   248 lemma inj_converse_inj: "f: inj(A,B) ==> converse(f): inj(range(f), A)"
```
```   249 apply (rule f_imp_injective)
```
```   250 apply (erule inj_converse_fun, clarify)
```
```   251 apply (rule right_inverse)
```
```   252  apply assumption
```
```   253 apply blast
```
```   254 done
```
```   255
```
```   256 lemma inj_converse_surj: "f: inj(A,B) ==> converse(f): surj(range(f), A)"
```
```   257 by (blast intro: f_imp_surjective inj_converse_fun left_inverse inj_is_fun
```
```   258                  range_of_fun [THEN apply_type])
```
```   259
```
```   260 (*Adding this as an intro! rule seems to cause looping*)
```
```   261 lemma bij_converse_bij [TC]: "f: bij(A,B) ==> converse(f): bij(B,A)"
```
```   262 apply (unfold bij_def)
```
```   263 apply (fast elim: surj_range [THEN subst] inj_converse_inj inj_converse_surj)
```
```   264 done
```
```   265
```
```   266
```
```   267
```
```   268 subsection{*Composition of Two Relations*}
```
```   269
```
```   270 (*The inductive definition package could derive these theorems for (r O s)*)
```
```   271
```
```   272 lemma compI [intro]: "[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s"
```
```   273 by (unfold comp_def, blast)
```
```   274
```
```   275 lemma compE [elim!]:
```
```   276     "[| xz : r O s;
```
```   277         !!x y z. [| xz=<x,z>;  <x,y>:s;  <y,z>:r |] ==> P |]
```
```   278      ==> P"
```
```   279 by (unfold comp_def, blast)
```
```   280
```
```   281 lemma compEpair:
```
```   282     "[| <a,c> : r O s;
```
```   283         !!y. [| <a,y>:s;  <y,c>:r |] ==> P |]
```
```   284      ==> P"
```
```   285 by (erule compE, simp)
```
```   286
```
```   287 lemma converse_comp: "converse(R O S) = converse(S) O converse(R)"
```
```   288 by blast
```
```   289
```
```   290
```
```   291 subsection{*Domain and Range -- see Suppes, Section 3.1*}
```
```   292
```
```   293 (*Boyer et al., Set Theory in First-Order Logic, JAR 2 (1986), 287-327*)
```
```   294 lemma range_comp: "range(r O s) <= range(r)"
```
```   295 by blast
```
```   296
```
```   297 lemma range_comp_eq: "domain(r) <= range(s) ==> range(r O s) = range(r)"
```
```   298 by (rule range_comp [THEN equalityI], blast)
```
```   299
```
```   300 lemma domain_comp: "domain(r O s) <= domain(s)"
```
```   301 by blast
```
```   302
```
```   303 lemma domain_comp_eq: "range(s) <= domain(r) ==> domain(r O s) = domain(s)"
```
```   304 by (rule domain_comp [THEN equalityI], blast)
```
```   305
```
```   306 lemma image_comp: "(r O s)``A = r``(s``A)"
```
```   307 by blast
```
```   308
```
```   309
```
```   310 subsection{*Other Results*}
```
```   311
```
```   312 lemma comp_mono: "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)"
```
```   313 by blast
```
```   314
```
```   315 (*composition preserves relations*)
```
```   316 lemma comp_rel: "[| s<=A*B;  r<=B*C |] ==> (r O s) <= A*C"
```
```   317 by blast
```
```   318
```
```   319 (*associative law for composition*)
```
```   320 lemma comp_assoc: "(r O s) O t = r O (s O t)"
```
```   321 by blast
```
```   322
```
```   323 (*left identity of composition; provable inclusions are
```
```   324         id(A) O r <= r
```
```   325   and   [| r<=A*B; B<=C |] ==> r <= id(C) O r *)
```
```   326 lemma left_comp_id: "r<=A*B ==> id(B) O r = r"
```
```   327 by blast
```
```   328
```
```   329 (*right identity of composition; provable inclusions are
```
```   330         r O id(A) <= r
```
```   331   and   [| r<=A*B; A<=C |] ==> r <= r O id(C) *)
```
```   332 lemma right_comp_id: "r<=A*B ==> r O id(A) = r"
```
```   333 by blast
```
```   334
```
```   335
```
```   336 subsection{*Composition Preserves Functions, Injections, and Surjections*}
```
```   337
```
```   338 lemma comp_function: "[| function(g);  function(f) |] ==> function(f O g)"
```
```   339 by (unfold function_def, blast)
```
```   340
```
```   341 (*Don't think the premises can be weakened much*)
```
```   342 lemma comp_fun: "[| g: A->B;  f: B->C |] ==> (f O g) : A->C"
```
```   343 apply (auto simp add: Pi_def comp_function Pow_iff comp_rel)
```
```   344 apply (subst range_rel_subset [THEN domain_comp_eq], auto)
```
```   345 done
```
```   346
```
```   347 (*Thanks to the new definition of "apply", the premise f: B->C is gone!*)
```
```   348 lemma comp_fun_apply [simp]:
```
```   349      "[| g: A->B;  a:A |] ==> (f O g)`a = f`(g`a)"
```
```   350 apply (frule apply_Pair, assumption)
```
```   351 apply (simp add: apply_def image_comp)
```
```   352 apply (blast dest: apply_equality)
```
```   353 done
```
```   354
```
```   355 (*Simplifies compositions of lambda-abstractions*)
```
```   356 lemma comp_lam:
```
```   357     "[| !!x. x:A ==> b(x): B |]
```
```   358      ==> (lam y:B. c(y)) O (lam x:A. b(x)) = (lam x:A. c(b(x)))"
```
```   359 apply (subgoal_tac "(lam x:A. b(x)) : A -> B")
```
```   360  apply (rule fun_extension)
```
```   361    apply (blast intro: comp_fun lam_funtype)
```
```   362   apply (rule lam_funtype)
```
```   363  apply simp
```
```   364 apply (simp add: lam_type)
```
```   365 done
```
```   366
```
```   367 lemma comp_inj:
```
```   368      "[| g: inj(A,B);  f: inj(B,C) |] ==> (f O g) : inj(A,C)"
```
```   369 apply (frule inj_is_fun [of g])
```
```   370 apply (frule inj_is_fun [of f])
```
```   371 apply (rule_tac d = "%y. converse (g) ` (converse (f) ` y)" in f_imp_injective)
```
```   372  apply (blast intro: comp_fun, simp)
```
```   373 done
```
```   374
```
```   375 lemma comp_surj:
```
```   376     "[| g: surj(A,B);  f: surj(B,C) |] ==> (f O g) : surj(A,C)"
```
```   377 apply (unfold surj_def)
```
```   378 apply (blast intro!: comp_fun comp_fun_apply)
```
```   379 done
```
```   380
```
```   381 lemma comp_bij:
```
```   382     "[| g: bij(A,B);  f: bij(B,C) |] ==> (f O g) : bij(A,C)"
```
```   383 apply (unfold bij_def)
```
```   384 apply (blast intro: comp_inj comp_surj)
```
```   385 done
```
```   386
```
```   387
```
```   388 subsection{*Dual Properties of @{term inj} and @{term surj}*}
```
```   389
```
```   390 text{*Useful for proofs from
```
```   391     D Pastre.  Automatic theorem proving in set theory.
```
```   392     Artificial Intelligence, 10:1--27, 1978.*}
```
```   393
```
```   394 lemma comp_mem_injD1:
```
```   395     "[| (f O g): inj(A,C);  g: A->B;  f: B->C |] ==> g: inj(A,B)"
```
```   396 by (unfold inj_def, force)
```
```   397
```
```   398 lemma comp_mem_injD2:
```
```   399     "[| (f O g): inj(A,C);  g: surj(A,B);  f: B->C |] ==> f: inj(B,C)"
```
```   400 apply (unfold inj_def surj_def, safe)
```
```   401 apply (rule_tac x1 = x in bspec [THEN bexE])
```
```   402 apply (erule_tac [3] x1 = w in bspec [THEN bexE], assumption+, safe)
```
```   403 apply (rule_tac t = "op ` (g) " in subst_context)
```
```   404 apply (erule asm_rl bspec [THEN bspec, THEN mp])+
```
```   405 apply (simp (no_asm_simp))
```
```   406 done
```
```   407
```
```   408 lemma comp_mem_surjD1:
```
```   409     "[| (f O g): surj(A,C);  g: A->B;  f: B->C |] ==> f: surj(B,C)"
```
```   410 apply (unfold surj_def)
```
```   411 apply (blast intro!: comp_fun_apply [symmetric] apply_funtype)
```
```   412 done
```
```   413
```
```   414
```
```   415 lemma comp_mem_surjD2:
```
```   416     "[| (f O g): surj(A,C);  g: A->B;  f: inj(B,C) |] ==> g: surj(A,B)"
```
```   417 apply (unfold inj_def surj_def, safe)
```
```   418 apply (drule_tac x = "f`y" in bspec, auto)
```
```   419 apply (blast intro: apply_funtype)
```
```   420 done
```
```   421
```
```   422 subsubsection{*Inverses of Composition*}
```
```   423
```
```   424 (*left inverse of composition; one inclusion is
```
```   425         f: A->B ==> id(A) <= converse(f) O f *)
```
```   426 lemma left_comp_inverse: "f: inj(A,B) ==> converse(f) O f = id(A)"
```
```   427 apply (unfold inj_def, clarify)
```
```   428 apply (rule equalityI)
```
```   429  apply (auto simp add: apply_iff, blast)
```
```   430 done
```
```   431
```
```   432 (*right inverse of composition; one inclusion is
```
```   433                 f: A->B ==> f O converse(f) <= id(B) *)
```
```   434 lemma right_comp_inverse:
```
```   435     "f: surj(A,B) ==> f O converse(f) = id(B)"
```
```   436 apply (simp add: surj_def, clarify)
```
```   437 apply (rule equalityI)
```
```   438 apply (best elim: domain_type range_type dest: apply_equality2)
```
```   439 apply (blast intro: apply_Pair)
```
```   440 done
```
```   441
```
```   442
```
```   443 subsubsection{*Proving that a Function is a Bijection*}
```
```   444
```
```   445 lemma comp_eq_id_iff:
```
```   446     "[| f: A->B;  g: B->A |] ==> f O g = id(B) <-> (ALL y:B. f`(g`y)=y)"
```
```   447 apply (unfold id_def, safe)
```
```   448  apply (drule_tac t = "%h. h`y " in subst_context)
```
```   449  apply simp
```
```   450 apply (rule fun_extension)
```
```   451   apply (blast intro: comp_fun lam_type)
```
```   452  apply auto
```
```   453 done
```
```   454
```
```   455 lemma fg_imp_bijective:
```
```   456     "[| f: A->B;  g: B->A;  f O g = id(B);  g O f = id(A) |] ==> f : bij(A,B)"
```
```   457 apply (unfold bij_def)
```
```   458 apply (simp add: comp_eq_id_iff)
```
```   459 apply (blast intro: f_imp_injective f_imp_surjective apply_funtype)
```
```   460 done
```
```   461
```
```   462 lemma nilpotent_imp_bijective: "[| f: A->A;  f O f = id(A) |] ==> f : bij(A,A)"
```
```   463 by (blast intro: fg_imp_bijective)
```
```   464
```
```   465 lemma invertible_imp_bijective:
```
```   466      "[| converse(f): B->A;  f: A->B |] ==> f : bij(A,B)"
```
```   467 by (simp add: fg_imp_bijective comp_eq_id_iff
```
```   468               left_inverse_lemma right_inverse_lemma)
```
```   469
```
```   470 subsubsection{*Unions of Functions*}
```
```   471
```
```   472 text{*See similar theorems in func.thy*}
```
```   473
```
```   474 (*Theorem by KG, proof by LCP*)
```
```   475 lemma inj_disjoint_Un:
```
```   476      "[| f: inj(A,B);  g: inj(C,D);  B Int D = 0 |]
```
```   477       ==> (lam a: A Un C. if a:A then f`a else g`a) : inj(A Un C, B Un D)"
```
```   478 apply (rule_tac d = "%z. if z:B then converse (f) `z else converse (g) `z"
```
```   479        in lam_injective)
```
```   480 apply (auto simp add: inj_is_fun [THEN apply_type])
```
```   481 done
```
```   482
```
```   483 lemma surj_disjoint_Un:
```
```   484     "[| f: surj(A,B);  g: surj(C,D);  A Int C = 0 |]
```
```   485      ==> (f Un g) : surj(A Un C, B Un D)"
```
```   486 apply (simp add: surj_def fun_disjoint_Un)
```
```   487 apply (blast dest!: domain_of_fun
```
```   488 	     intro!: fun_disjoint_apply1 fun_disjoint_apply2)
```
```   489 done
```
```   490
```
```   491 (*A simple, high-level proof; the version for injections follows from it,
```
```   492   using  f:inj(A,B) <-> f:bij(A,range(f))  *)
```
```   493 lemma bij_disjoint_Un:
```
```   494      "[| f: bij(A,B);  g: bij(C,D);  A Int C = 0;  B Int D = 0 |]
```
```   495       ==> (f Un g) : bij(A Un C, B Un D)"
```
```   496 apply (rule invertible_imp_bijective)
```
```   497 apply (subst converse_Un)
```
```   498 apply (auto intro: fun_disjoint_Un bij_is_fun bij_converse_bij)
```
```   499 done
```
```   500
```
```   501
```
```   502 subsubsection{*Restrictions as Surjections and Bijections*}
```
```   503
```
```   504 lemma surj_image:
```
```   505     "f: Pi(A,B) ==> f: surj(A, f``A)"
```
```   506 apply (simp add: surj_def)
```
```   507 apply (blast intro: apply_equality apply_Pair Pi_type)
```
```   508 done
```
```   509
```
```   510 lemma restrict_image [simp]: "restrict(f,A) `` B = f `` (A Int B)"
```
```   511 by (auto simp add: restrict_def)
```
```   512
```
```   513 lemma restrict_inj:
```
```   514     "[| f: inj(A,B);  C<=A |] ==> restrict(f,C): inj(C,B)"
```
```   515 apply (unfold inj_def)
```
```   516 apply (safe elim!: restrict_type2, auto)
```
```   517 done
```
```   518
```
```   519 lemma restrict_surj: "[| f: Pi(A,B);  C<=A |] ==> restrict(f,C): surj(C, f``C)"
```
```   520 apply (insert restrict_type2 [THEN surj_image])
```
```   521 apply (simp add: restrict_image)
```
```   522 done
```
```   523
```
```   524 lemma restrict_bij:
```
```   525     "[| f: inj(A,B);  C<=A |] ==> restrict(f,C): bij(C, f``C)"
```
```   526 apply (simp add: inj_def bij_def)
```
```   527 apply (blast intro: restrict_surj surj_is_fun)
```
```   528 done
```
```   529
```
```   530
```
```   531 subsubsection{*Lemmas for Ramsey's Theorem*}
```
```   532
```
```   533 lemma inj_weaken_type: "[| f: inj(A,B);  B<=D |] ==> f: inj(A,D)"
```
```   534 apply (unfold inj_def)
```
```   535 apply (blast intro: fun_weaken_type)
```
```   536 done
```
```   537
```
```   538 lemma inj_succ_restrict:
```
```   539      "[| f: inj(succ(m), A) |] ==> restrict(f,m) : inj(m, A-{f`m})"
```
```   540 apply (rule restrict_bij [THEN bij_is_inj, THEN inj_weaken_type], assumption, blast)
```
```   541 apply (unfold inj_def)
```
```   542 apply (fast elim: range_type mem_irrefl dest: apply_equality)
```
```   543 done
```
```   544
```
```   545
```
```   546 lemma inj_extend:
```
```   547     "[| f: inj(A,B);  a~:A;  b~:B |]
```
```   548      ==> cons(<a,b>,f) : inj(cons(a,A), cons(b,B))"
```
```   549 apply (unfold inj_def)
```
```   550 apply (force intro: apply_type  simp add: fun_extend)
```
```   551 done
```
```   552
```
```   553 end
```