theory Folds+
−
imports Main+
−
begin+
−
+
−
section {* 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+
−