# HG changeset patch
# User haftmann
# Date 1282319215 -7200
# Node ID b40524b74f7741ee1f18c42b6949b5c340741c81
# Parent  25e401d5390066f3fdffbde36b86ce130e0cf0f9
inj_comp and inj_fun

diff -r 25e401d53900 -r b40524b74f77 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Fri Aug 20 08:52:01 2010 +0200
+++ b/src/HOL/Fun.thy	Fri Aug 20 17:46:55 2010 +0200
@@ -162,6 +162,13 @@
 lemma inj_on_eq_iff: "inj_on f A ==> x:A ==> y:A ==> (f(x) = f(y)) = (x=y)"
 by (force simp add: inj_on_def)
 
+lemma inj_comp:
+  "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (f \<circ> g)"
+  by (simp add: inj_on_def)
+
+lemma inj_fun: "inj f \<Longrightarrow> inj (\<lambda>x y. f x)"
+  by (simp add: inj_on_def expand_fun_eq)
+
 lemma inj_eq: "inj f ==> (f(x) = f(y)) = (x=y)"
 by (simp add: inj_on_eq_iff)