src/HOL/Fun.thy
changeset 51598 5dbe537087aa
parent 49905 a81f95693c68
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/Fun.thy	Tue Apr 02 20:19:38 2013 +0200
     1.2 +++ b/src/HOL/Fun.thy	Wed Apr 03 10:15:43 2013 +0200
     1.3 @@ -286,6 +286,22 @@
     1.4    "inj_on (f' o f) A \<Longrightarrow> inj_on f A"
     1.5  by(auto simp add: comp_inj_on inj_on_def)
     1.6  
     1.7 +lemma inj_img_insertE:
     1.8 +  assumes "inj_on f A"
     1.9 +  assumes "x \<notin> B" and "insert x B = f ` A"
    1.10 +  obtains x' A' where "x' \<notin> A'" and "A = insert x' A'"
    1.11 +    and "x = f x'" and "B = f ` A'" 
    1.12 +proof -
    1.13 +  from assms have "x \<in> f ` A" by auto
    1.14 +  then obtain x' where *: "x' \<in> A" "x = f x'" by auto
    1.15 +  then have "A = insert x' (A - {x'})" by auto
    1.16 +  with assms * have "B = f ` (A - {x'})"
    1.17 +    by (auto dest: inj_on_contraD)
    1.18 +  have "x' \<notin> A - {x'}" by simp
    1.19 +  from `x' \<notin> A - {x'}` `A = insert x' (A - {x'})` `x = f x'` `B = image f (A - {x'})`
    1.20 +  show ?thesis ..
    1.21 +qed
    1.22 +
    1.23  lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
    1.24    by auto
    1.25