# HG changeset patch
# User haftmann
# Date 1249977953 -7200
# Node ID 84a6d701e36fa23fccbc2f8c7fa897fd58ce5db7
# Parent  e73eb2db47274969c84e59ddab68c799f579fd85# Parent  e11cd88e6ade0a23abf2061e150ba01e05d32d22
merged

diff -r e11cd88e6ade -r 84a6d701e36f src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Tue Aug 11 10:05:16 2009 +0200
+++ b/src/HOL/Fun.thy	Tue Aug 11 10:05:53 2009 +0200
@@ -250,6 +250,9 @@
 lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
 by (simp add: bij_betw_def)
 
+lemma bij_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> bij (g o f)"
+by(fastsimp intro: comp_inj_on comp_surj simp: bij_def surj_range)
+
 lemma bij_betw_trans:
   "bij_betw f A B \<Longrightarrow> bij_betw g B C \<Longrightarrow> bij_betw (g o f) A C"
 by(auto simp add:bij_betw_def comp_inj_on)
diff -r e11cd88e6ade -r 84a6d701e36f src/HOL/Library/Nat_Int_Bij.thy
--- a/src/HOL/Library/Nat_Int_Bij.thy	Tue Aug 11 10:05:16 2009 +0200
+++ b/src/HOL/Library/Nat_Int_Bij.thy	Tue Aug 11 10:05:53 2009 +0200
@@ -165,5 +165,11 @@
 lemma inj_int_to_nat_bij: "inj int_to_nat_bij"
 by(simp add:inv_nat_to_int_bij[symmetric] surj_nat_to_int_bij surj_imp_inj_inv)
 
+lemma bij_nat_to_int_bij: "bij nat_to_int_bij"
+by(simp add:bij_def inj_nat_to_int_bij surj_nat_to_int_bij)
+
+lemma bij_int_to_nat_bij: "bij int_to_nat_bij"
+by(simp add:bij_def inj_int_to_nat_bij surj_int_to_nat_bij)
+
 
 end