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