src/ZF/Perm.thy

   -- Composition of relations, the identity relation
   -- Injections, surjections, bijections
   -- Lemmas for the Schroeder-Bernstein Theorem
 *)
 
+header{*Injections, Surjections, Bijections, Composition*}
+
 theory Perm = mono + func:
 
 constdefs
 
   (*composition of relations and functions; NOT Suppes's relative product*)

 
   (*one-to-one and onto functions*)
   bij   :: "[i,i]=>i"
     "bij(A,B) == inj(A,B) Int surj(A,B)"
 
+
+subsection{*Surjections*}
 
 (** Surjective function space **)
 
 lemma surj_is_fun: "f: surj(A,B) ==> f: A->B"
 apply (unfold surj_def)

 apply (cut_tac cantor)
 apply (best del: subsetI) 
 done
 
 
+subsection{*Injections*}
+
 (** Injective function space **)
 
 lemma inj_is_fun: "f: inj(A,B) ==> f: A->B"
 apply (unfold inj_def)
 apply (erule CollectD1)

      ==> (lam x:A. c(x)) : inj(A,B)"
 apply (rule_tac d = "d" in f_imp_injective)
 apply (simp_all add: lam_type)
 done
 
-(** Bijections **)
+subsection{*Bijections*}
 
 lemma bij_is_inj: "f: bij(A,B) ==> f: inj(A,B)"
 apply (unfold bij_def)
 apply (erule IntD1)
 done

 apply (rule_tac d = "f" in lam_bijective)
 apply (auto simp add: the_equality2)
 done
 
 
-(** Identity function **)
+subsection{*Identity Function*}
 
 lemma idI [intro!]: "a:A ==> <a,a> : id(A)"
 apply (unfold id_def)
 apply (erule lamI)
 done

 by (blast intro: right_inverse_lemma inj_converse_fun inj_is_fun)
 
 lemma right_inverse_bij: "[| f: bij(A,B);  b: B |] ==> f`(converse(f)`b) = b"
 by (force simp add: bij_def surj_range)
 
-(** Converses of injections, surjections, bijections **)
+subsection{*Converses of Injections, Surjections, Bijections*}
 
 lemma inj_converse_inj: "f: inj(A,B) ==> converse(f): inj(range(f), A)"
 apply (rule f_imp_injective)
 apply (erule inj_converse_fun, clarify) 
 apply (rule right_inverse)

 apply (fast elim: surj_range [THEN subst] inj_converse_inj inj_converse_surj)
 done
 
 
 
-(** Composition of two relations **)
+subsection{*Composition of Two Relations*}
 
 (*The inductive definition package could derive these theorems for (r O s)*)
 
 lemma compI [intro]: "[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s"
 by (unfold comp_def, blast)

 
 lemma converse_comp: "converse(R O S) = converse(S) O converse(R)"
 by blast
 
 
-(** Domain and Range -- see Suppes, section 3.1 **)
+subsection{*Domain and Range -- see Suppes, Section 3.1*}
 
 (*Boyer et al., Set Theory in First-Order Logic, JAR 2 (1986), 287-327*)
 lemma range_comp: "range(r O s) <= range(r)"
 by blast
 

 
 lemma image_comp: "(r O s)``A = r``(s``A)"
 by blast
 
 
-(** Other results **)
+subsection{*Other Results*}
 
 lemma comp_mono: "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)"
 by blast
 
 (*composition preserves relations*)

   and   [| r<=A*B; A<=C |] ==> r <= r O id(C) *)
 lemma right_comp_id: "r<=A*B ==> r O id(A) = r"
 by blast
 
 
-(** Composition preserves functions, injections, and surjections **)
+subsection{*Composition Preserves Functions, Injections, and Surjections*}
 
 lemma comp_function: "[| function(g);  function(f) |] ==> function(f O g)"
 by (unfold function_def, blast)
 
 (*Don't think the premises can be weakened much*)

 apply (unfold bij_def)
 apply (blast intro: comp_inj comp_surj)
 done
 
 
-(** Dual properties of inj and surj -- useful for proofs from
+subsection{*Dual Properties of @{term inj} and @{term surj}*}
+
+text{*Useful for proofs from
     D Pastre.  Automatic theorem proving in set theory. 
-    Artificial Intelligence, 10:1--27, 1978. **)
+    Artificial Intelligence, 10:1--27, 1978.*}
 
 lemma comp_mem_injD1: 
     "[| (f O g): inj(A,C);  g: A->B;  f: B->C |] ==> g: inj(A,B)"
-apply (unfold inj_def, force) 
-done
+by (unfold inj_def, force) 
 
 lemma comp_mem_injD2: 
     "[| (f O g): inj(A,C);  g: surj(A,B);  f: B->C |] ==> f: inj(B,C)"
 apply (unfold inj_def surj_def, safe)
 apply (rule_tac x1 = "x" in bspec [THEN bexE])

 apply (unfold inj_def surj_def, safe)
 apply (drule_tac x = "f`y" in bspec, auto)  
 apply (blast intro: apply_funtype)
 done
 
-(** inverses of composition **)
+subsubsection{*Inverses of Composition*}
 
 (*left inverse of composition; one inclusion is
         f: A->B ==> id(A) <= converse(f) O f *)
 lemma left_comp_inverse: "f: inj(A,B) ==> converse(f) O f = id(A)"
 apply (unfold inj_def, clarify) 

 apply (best elim: domain_type range_type dest: apply_equality2)
 apply (blast intro: apply_Pair)
 done
 
 
-(** Proving that a function is a bijection **)
+subsubsection{*Proving that a Function is a Bijection*}
 
 lemma comp_eq_id_iff: 
     "[| f: A->B;  g: B->A |] ==> f O g = id(B) <-> (ALL y:B. f`(g`y)=y)"
 apply (unfold id_def, safe)
  apply (drule_tac t = "%h. h`y " in subst_context)

 lemma invertible_imp_bijective:
      "[| converse(f): B->A;  f: A->B |] ==> f : bij(A,B)"
 by (simp add: fg_imp_bijective comp_eq_id_iff 
               left_inverse_lemma right_inverse_lemma)
 
-(** Unions of functions -- cf similar theorems on func.ML **)
+subsubsection{*Unions of Functions*}
+
+text{*See similar theorems in func.thy*}
 
 (*Theorem by KG, proof by LCP*)
 lemma inj_disjoint_Un:
      "[| f: inj(A,B);  g: inj(C,D);  B Int D = 0 |]  
       ==> (lam a: A Un C. if a:A then f`a else g`a) : inj(A Un C, B Un D)"

 apply (subst converse_Un)
 apply (auto intro: fun_disjoint_Un bij_is_fun bij_converse_bij)
 done
 
 
-(** Restrictions as surjections and bijections *)
+subsubsection{*Restrictions as Surjections and Bijections*}
 
 lemma surj_image:
     "f: Pi(A,B) ==> f: surj(A, f``A)"
 apply (simp add: surj_def) 
 apply (blast intro: apply_equality apply_Pair Pi_type) 

 apply (simp add: inj_def bij_def)
 apply (blast intro: restrict_surj surj_is_fun)
 done
 
 
-(*** Lemmas for Ramsey's Theorem ***)
+subsubsection{*Lemmas for Ramsey's Theorem*}
 
 lemma inj_weaken_type: "[| f: inj(A,B);  B<=D |] ==> f: inj(A,D)"
 apply (unfold inj_def)
 apply (blast intro: fun_weaken_type)
 done