--- a/Folds.thy	Fri Aug 19 20:39:07 2011 +0000
+++ b/Folds.thy	Mon Aug 22 12:49:27 2011 +0000
@@ -1,8 +1,8 @@
 theory Folds
-imports Main
+imports "Regular_Exp"
 begin
 
-section {* Folds for Sets *}
+section {* ``Summation'' for regular expressions *}
 
 text {*
   To obtain equational system out of finite set of equivalence classes, a fold operation
@@ -18,5 +18,27 @@
 where
   "folds f z S \<equiv> SOME x. fold_graph f z S x"
 
+text {* Plus-combination for a set of regular expressions *}
+
+abbreviation
+  Setalt :: "'a rexp set \<Rightarrow> 'a rexp" ("\<Uplus>_" [1000] 999) 
+where
+  "\<Uplus>A \<equiv> 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 (\<Uplus>rs) = \<Union> (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
\ No newline at end of file