theory Foldsimports Mainbeginsection {* Folds for Sets *}text {* To obtain equational system out of finite set of equivalence classes, a fold operation on finite sets @{text "folds"} is defined. The use of @{text "SOME"} makes @{text "folds"} more robust than the @{text "fold"} in the Isabelle library. The expression @{text "folds f"} makes sense when @{text "f"} is not @{text "associative"} and @{text "commutitive"}, while @{text "fold f"} does not. *}definition folds :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"where "folds f z S \<equiv> SOME x. fold_graph f z S x"end