# HG changeset patch
# User paulson
# Date 1084546373 -7200
# Node ID 001323d6d75bd115509bd23165e8f50d223c69e5
# Parent  2eaff69d3d10a59d5445bb08e68d7d27d08fa4bb
removed a premise of card_inj_on_le

diff -r 2eaff69d3d10 -r 001323d6d75b src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri May 14 16:50:33 2004 +0200
+++ b/src/HOL/Finite_Set.thy	Fri May 14 16:52:53 2004 +0200
@@ -1004,8 +1004,8 @@
   by (auto simp add: setprod_def LC_def LC.fold_insert
       mult_left_commute)
 
-lemma setprod_reindex [rule_format]: "finite B ==>
-                  inj_on f B --> setprod h (f ` B) = setprod (h \<circ> f) B"
+lemma setprod_reindex [rule_format]:
+     "finite B ==> inj_on f B --> setprod h (f ` B) = setprod (h \<circ> f) B"
 apply (rule finite_induct, assumption, force)
 apply (rule impI, auto)
 apply (simp add: inj_on_def)
@@ -1013,7 +1013,7 @@
 apply (subgoal_tac "finite (f ` F)")
 apply (auto simp add: setprod_insert)
 apply (simp add: inj_on_def)
-  done
+done
 
 lemma setprod_reindex_id: "finite B ==> inj_on f B ==>
     setprod f B = setprod id (f ` B)"
@@ -1325,8 +1325,11 @@
   done
 
 lemma card_inj_on_le:
-    "[|inj_on f A; f ` A \<subseteq> B; finite A; finite B |] ==> card A <= card B"
-  by (auto intro: card_mono simp add: card_image [symmetric])
+    "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
+apply (subgoal_tac "finite A") 
+ apply (force intro: card_mono simp add: card_image [symmetric])
+apply (blast intro: Finite_Set.finite_imageD dest: finite_subset) 
+done
 
 lemma card_bij_eq:
     "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;