--- a/src/HOL/Finite_Set.thy Fri Jan 21 13:51:39 2005 +0100
+++ b/src/HOL/Finite_Set.thy Fri Jan 21 13:52:09 2005 +0100
@@ -444,7 +444,6 @@
subsubsection {* Commutative monoids *}
-
locale ACf =
fixes f :: "'a => 'a => 'a" (infixl "\<cdot>" 70)
assumes commute: "x \<cdot> y = y \<cdot> x"
@@ -1547,6 +1546,13 @@
subsubsection {* Cardinality of image *}
+text{*The image of a finite set can be expressed using @{term fold}.*}
+lemma image_eq_fold: "finite A ==> f ` A = fold (op Un) (%x. {f x}) {} A"
+ apply (erule finite_induct, simp)
+ apply (subst ACf.fold_insert)
+ apply (auto simp add: ACf_def)
+ done
+
lemma card_image_le: "finite A ==> card (f ` A) <= card A"
apply (induct set: Finites, simp)
apply (simp add: le_SucI finite_imageI card_insert_if)