src/HOL/Fun.thy
changeset 15111 c108189645f8
parent 14565 c6dc17aab88a
child 15131 c69542757a4d
     1.1 --- a/src/HOL/Fun.thy	Wed Aug 04 19:10:45 2004 +0200
     1.2 +++ b/src/HOL/Fun.thy	Wed Aug 04 19:11:02 2004 +0200
     1.3 @@ -162,9 +162,30 @@
     1.4  lemma inj_singleton: "inj (%s. {s})"
     1.5  by (simp add: inj_on_def)
     1.6  
     1.7 +lemma inj_on_empty[iff]: "inj_on f {}"
     1.8 +by(simp add: inj_on_def)
     1.9 +
    1.10  lemma subset_inj_on: "[| A<=B; inj_on f B |] ==> inj_on f A"
    1.11  by (unfold inj_on_def, blast)
    1.12  
    1.13 +lemma inj_on_Un:
    1.14 + "inj_on f (A Un B) =
    1.15 +  (inj_on f A & inj_on f B & f`(A-B) Int f`(B-A) = {})"
    1.16 +apply(unfold inj_on_def)
    1.17 +apply (blast intro:sym)
    1.18 +done
    1.19 +
    1.20 +lemma inj_on_insert[iff]:
    1.21 +  "inj_on f (insert a A) = (inj_on f A & f a ~: f`(A-{a}))"
    1.22 +apply(unfold inj_on_def)
    1.23 +apply (blast intro:sym)
    1.24 +done
    1.25 +
    1.26 +lemma inj_on_diff: "inj_on f A ==> inj_on f (A-B)"
    1.27 +apply(unfold inj_on_def)
    1.28 +apply (blast)
    1.29 +done
    1.30 +
    1.31  
    1.32  subsection{*The Predicate @{term surj}: Surjectivity*}
    1.33