|
149
|
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 |