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