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