src/HOL/Finite_Set.thy
changeset 15447 177ffdbabf80
parent 15409 a063687d24eb
child 15479 fbc473ea9d3c
     1.1 --- a/src/HOL/Finite_Set.thy	Fri Jan 21 13:51:39 2005 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri Jan 21 13:52:09 2005 +0100
     1.3 @@ -444,7 +444,6 @@
     1.4  
     1.5  
     1.6  subsubsection {* Commutative monoids *}
     1.7 -
     1.8  locale ACf =
     1.9    fixes f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
    1.10    assumes commute: "x \<cdot> y = y \<cdot> x"
    1.11 @@ -1547,6 +1546,13 @@
    1.12  
    1.13  subsubsection {* Cardinality of image *}
    1.14  
    1.15 +text{*The image of a finite set can be expressed using @{term fold}.*}
    1.16 +lemma image_eq_fold: "finite A ==> f ` A = fold (op Un) (%x. {f x}) {} A"
    1.17 +  apply (erule finite_induct, simp)
    1.18 +  apply (subst ACf.fold_insert) 
    1.19 +  apply (auto simp add: ACf_def) 
    1.20 +  done
    1.21 +
    1.22  lemma card_image_le: "finite A ==> card (f ` A) <= card A"
    1.23    apply (induct set: Finites, simp)
    1.24    apply (simp add: le_SucI finite_imageI card_insert_if)