Theory Folds

(* 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