--- 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)
--- 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