1 theory Folds

     2 imports Main

     3 begin

     4 

     5 section {* Folds for Sets *}

     6 

     7 text {*

     8   To obtain equational system out of finite set of equivalence classes, a fold operation

     9   on finite sets @{text "folds"} is defined. The use of @{text "SOME"} makes @{text "folds"}

    10   more robust than the @{text "fold"} in the Isabelle library. The expression @{text "folds f"}

    11   makes sense when @{text "f"} is not @{text "associative"} and @{text "commutitive"},

    12   while @{text "fold f"} does not.  

    13 *}

    14 

    15 

    16 definition 

    17   folds :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"

    18 where

    19   "folds f z S \<equiv> SOME x. fold_graph f z S x"

    20 

    21 

    22 end