(* Author: Xingyuan Zhang, Chunhan Wu, Christian Urban *) theory Folds imports"Regular-Sets.Regular_Exp" begin
section‹``Summation'' for regular expressions›
text‹
To obtain equational system out of finite set of equivalence classes, a fold operation
on finite sets ‹folds› is defined. The use of ‹SOME› makes ‹folds›
more robust than the ‹fold› in the Isabelle library. The expression ‹folds f›
makes sense when ‹f› is not ‹associative› and ‹commutitive›,
while ‹fold f› does not. ›
definition
folds :: "('a ==> 'b ==> 'b) ==> 'b ==> 'a set ==> 'b" where "folds f z S ≡ SOME x. fold_graph f z S x"
text‹Plus-combination for a set of regular expressions›
abbreviation
Setalt :: "'a rexp set ==> 'a rexp" (‹⊎_› [1000] 999) where "⊎A ≡ folds Plus Zero A"
text‹
For finite sets, @{term Setalt} is preserved under @{term lang}. ›
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
