# HG changeset patch
# User haftmann
# Date 1301823632 -7200
# Node ID 2bda5eddadf3895507cec0c72c7c18ff777ad9e2
# Parent  0920f709610f47d85752814c74f44c534d8b0b95
tuned proofs

diff -r 0920f709610f -r 2bda5eddadf3 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sat Apr 02 18:07:29 2011 +0200
+++ b/src/HOL/Finite_Set.thy	Sun Apr 03 11:40:32 2011 +0200
@@ -355,34 +355,32 @@
   by (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product)
 
 lemma finite_cartesian_productD1:
-  "finite (A \<times> B) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> finite A"
-apply (auto simp add: finite_conv_nat_seg_image) 
-apply (drule_tac x=n in spec) 
-apply (drule_tac x="fst o f" in spec) 
-apply (auto simp add: o_def) 
- prefer 2 apply (force dest!: equalityD2) 
-apply (drule equalityD1) 
-apply (rename_tac y x)
-apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)") 
- prefer 2 apply force
-apply clarify
-apply (rule_tac x=k in image_eqI, auto)
-done
+  assumes "finite (A \<times> B)" and "B \<noteq> {}"
+  shows "finite A"
+proof -
+  from assms obtain n f where "A \<times> B = f ` {i::nat. i < n}"
+    by (auto simp add: finite_conv_nat_seg_image)
+  then have "fst ` (A \<times> B) = fst ` f ` {i::nat. i < n}" by simp
+  with `B \<noteq> {}` have "A = (fst \<circ> f) ` {i::nat. i < n}"
+    by (simp add: image_compose)
+  then have "\<exists>n f. A = f ` {i::nat. i < n}" by blast
+  then show ?thesis
+    by (auto simp add: finite_conv_nat_seg_image)
+qed
 
 lemma finite_cartesian_productD2:
-     "[| finite (A <*> B); A \<noteq> {} |] ==> finite B"
-apply (auto simp add: finite_conv_nat_seg_image) 
-apply (drule_tac x=n in spec) 
-apply (drule_tac x="snd o f" in spec) 
-apply (auto simp add: o_def) 
- prefer 2 apply (force dest!: equalityD2) 
-apply (drule equalityD1)
-apply (rename_tac x y)
-apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)") 
- prefer 2 apply force
-apply clarify
-apply (rule_tac x=k in image_eqI, auto)
-done
+  assumes "finite (A \<times> B)" and "A \<noteq> {}"
+  shows "finite B"
+proof -
+  from assms obtain n f where "A \<times> B = f ` {i::nat. i < n}"
+    by (auto simp add: finite_conv_nat_seg_image)
+  then have "snd ` (A \<times> B) = snd ` f ` {i::nat. i < n}" by simp
+  with `A \<noteq> {}` have "B = (snd \<circ> f) ` {i::nat. i < n}"
+    by (simp add: image_compose)
+  then have "\<exists>n f. B = f ` {i::nat. i < n}" by blast
+  then show ?thesis
+    by (auto simp add: finite_conv_nat_seg_image)
+qed
 
 lemma finite_Pow_iff [iff]:
   "finite (Pow A) \<longleftrightarrow> finite A"