# HG changeset patch
# User haftmann
# Date 1301760449 -7200
# Node ID 0920f709610f47d85752814c74f44c534d8b0b95
# Parent  d49ffc7a19f8368a79b3dedba868f2cf89fecd5c
tuned proof

diff -r d49ffc7a19f8 -r 0920f709610f src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Apr 01 18:29:10 2011 +0200
+++ b/src/HOL/Finite_Set.thy	Sat Apr 02 18:07:29 2011 +0200
@@ -246,24 +246,20 @@
   by (simp add: image_Collect [symmetric])
 
 lemma finite_imageD:
-  "finite (f ` A) \<Longrightarrow> inj_on f A \<Longrightarrow> finite A"
-proof -
-  have aux: "!!A. finite (A - {}) = finite A" by simp
-  fix B :: "'a set"
-  assume "finite B"
-  thus "!!A. f`A = B ==> inj_on f A ==> finite A"
-    apply induct
-     apply simp
-    apply (subgoal_tac "EX y:A. f y = x & F = f ` (A - {y})")
-     apply clarify
-     apply (simp (no_asm_use) add: inj_on_def)
-     apply (blast dest!: aux [THEN iffD1], atomize)
-    apply (erule_tac V = "ALL A. ?PP (A)" in thin_rl)
-    apply (frule subsetD [OF equalityD2 insertI1], clarify)
-    apply (rule_tac x = xa in bexI)
-     apply (simp_all add: inj_on_image_set_diff)
-    done
-qed (rule refl)
+  assumes "finite (f ` A)" and "inj_on f A"
+  shows "finite A"
+using assms proof (induct "f ` A" arbitrary: A)
+  case empty then show ?case by simp
+next
+  case (insert x B)
+  then have B_A: "insert x B = f ` A" by simp
+  then obtain y where "x = f y" and "y \<in> A" by blast
+  from B_A `x \<notin> B` have "B = f ` A - {x}" by blast
+  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)
+  moreover from `inj_on f A` have "inj_on f (A - {y})" by (rule inj_on_diff)
+  ultimately have "finite (A - {y})" by (rule insert.hyps)
+  then show "finite A" by simp
+qed
 
 lemma finite_surj:
   "finite A \<Longrightarrow> B \<subseteq> f ` A \<Longrightarrow> finite B"