--- a/Myhill_1.thy	Mon Feb 07 20:30:10 2011 +0000
+++ b/Myhill_1.thy	Tue Feb 08 09:51:27 2011 +0000
@@ -320,11 +320,17 @@
   while @{text "fold f"} does not.  
 *}
 
+
 definition 
   folds :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"
 where
   "folds f z S \<equiv> SOME x. fold_graph f z S x"
 
+abbreviation
+  Setalt  ("\<Uplus>_" [1000] 999) 
+where
+  "\<Uplus>A == folds ALT NULL A"
+
 text {* 
   The following lemma ensures that the arbitrary choice made by the 
   @{text "SOME"} in @{text "folds"} does not affect the @{text "L"}-value 
@@ -333,7 +339,7 @@
 
 lemma folds_alt_simp [simp]:
   assumes a: "finite rs"
-  shows "L (folds ALT NULL rs) = \<Union> (L ` rs)"
+  shows "L (\<Uplus>rs) = \<Union> (L ` rs)"
 apply(rule set_eqI)
 apply(simp add: folds_def)
 apply(rule someI2_ex)
@@ -382,6 +388,12 @@
 apply(auto)
 done
 
+lemma finals_included_in_UNIV:
+  shows "finals A \<subseteq> UNIV // \<approx>A"
+unfolding finals_def
+unfolding quotient_def
+by auto
+
 
 section {* Direction @{text "finite partition \<Rightarrow> regular language"}*}
 
@@ -503,7 +515,7 @@
 
 text {* 
   The following @{text "items_of rhs X"} returns all @{text "X"}-items in @{text "rhs"}.
-  *}
+*}
 
 definition
   "items_of rhs X \<equiv> {Trn X r | r. (Trn X r) \<in> rhs}"
@@ -515,7 +527,7 @@
   *}
 
 definition 
-  "rexp_of rhs X \<equiv> folds ALT NULL ((snd o the_Trn) ` items_of rhs X)"
+  "rexp_of rhs X \<equiv> \<Uplus>((snd o the_Trn) ` items_of rhs X)"
 
 text {* 
   The following @{text "lam_of rhs"} returns all pure regular expression items in @{text "rhs"}.
@@ -531,8 +543,9 @@
   is used to compute compute the regular expression corresponds to @{text "rhs"}.
 *}
 
+
 definition
-  "rexp_of_lam rhs \<equiv> folds ALT NULL (the_r ` lam_of rhs)"
+  "rexp_of_lam rhs \<equiv> \<Uplus>(the_r ` lam_of rhs)"
 
 text {*
   The following @{text "attach_rexp rexp' itm"} attach 
@@ -1282,7 +1295,7 @@
     by (auto dest: bchoice)
   def rs \<equiv> "f ` (finals A)"  
   have "A = \<Union> (finals A)" using lang_is_union_of_finals by auto
-  also have "\<dots> = L (folds ALT NULL rs)" 
+  also have "\<dots> = L (\<Uplus>rs)" 
   proof -
     have "finite rs"
     proof -