# HG changeset patch
# User paulson
# Date 1106311929 -3600
# Node ID 177ffdbabf80b36bc8f908bd6a42110fd7ae4472
# Parent  b022b72ccc03108a5b1449e41181cac42301eac5
new theorem image_eq_fold

diff -r b022b72ccc03 -r 177ffdbabf80 src/HOL/Finite_Set.thy
--- 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)