1.1 --- a/src/HOL/Finite_Set.thy	Fri Apr 01 18:29:10 2011 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Sat Apr 02 18:07:29 2011 +0200
     1.3 @@ -246,24 +246,20 @@
     1.4    by (simp add: image_Collect [symmetric])
     1.5  
     1.6  lemma finite_imageD:
     1.7 -  "finite (f ` A) \<Longrightarrow> inj_on f A \<Longrightarrow> finite A"
     1.8 -proof -
     1.9 -  have aux: "!!A. finite (A - {}) = finite A" by simp
    1.10 -  fix B :: "'a set"
    1.11 -  assume "finite B"
    1.12 -  thus "!!A. f`A = B ==> inj_on f A ==> finite A"
    1.13 -    apply induct
    1.14 -     apply simp
    1.15 -    apply (subgoal_tac "EX y:A. f y = x & F = f ` (A - {y})")
    1.16 -     apply clarify
    1.17 -     apply (simp (no_asm_use) add: inj_on_def)
    1.18 -     apply (blast dest!: aux [THEN iffD1], atomize)
    1.19 -    apply (erule_tac V = "ALL A. ?PP (A)" in thin_rl)
    1.20 -    apply (frule subsetD [OF equalityD2 insertI1], clarify)
    1.21 -    apply (rule_tac x = xa in bexI)
    1.22 -     apply (simp_all add: inj_on_image_set_diff)
    1.23 -    done
    1.24 -qed (rule refl)
    1.25 +  assumes "finite (f ` A)" and "inj_on f A"
    1.26 +  shows "finite A"
    1.27 +using assms proof (induct "f ` A" arbitrary: A)
    1.28 +  case empty then show ?case by simp
    1.29 +next
    1.30 +  case (insert x B)
    1.31 +  then have B_A: "insert x B = f ` A" by simp
    1.32 +  then obtain y where "x = f y" and "y \<in> A" by blast
    1.33 +  from B_A `x \<notin> B` have "B = f ` A - {x}" by blast
    1.34 +  with B_A `x \<notin> B` `x = f y` `inj_on f A` `y \<in> A` have "B = f ` (A - {y})" by (simp add: inj_on_image_set_diff)
    1.35 +  moreover from `inj_on f A` have "inj_on f (A - {y})" by (rule inj_on_diff)
    1.36 +  ultimately have "finite (A - {y})" by (rule insert.hyps)
    1.37 +  then show "finite A" by simp
    1.38 +qed
    1.39  
    1.40  lemma finite_surj:
    1.41    "finite A \<Longrightarrow> B \<subseteq> f ` A \<Longrightarrow> finite B"