(* 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}.
›
lemma folds_plus_simp [simp]:
fixes rs::"('a rexp) set"
assumes a: "finite rs"
shows "lang (⊎rs) = ∪ (lang ` rs)"
unfolding folds_def
apply(rule set_eqI)
apply(rule someI2_ex)
apply(rule_tac finite_imp_fold_graph[OF a])
apply(erule fold_graph.induct)
apply(auto)
done
end
¤ Dauer der Verarbeitung: 0.2 Sekunden
¤
*© Formatika GbR, Deutschland
