269 consts L:: "'a \<Rightarrow> lang"

   269 consts L:: "'a \<Rightarrow> lang"

   270 

   270 

   271 overloading L_rexp \<equiv> "L::  rexp \<Rightarrow> lang"

   271 overloading L_rexp \<equiv> "L::  rexp \<Rightarrow> lang"

   272 begin

   272 begin

   273 fun

   273 fun

   275 where

   275 where

   276     "L_rexp (NULL) = {}"

   276     "L_rexp (NULL) = {}"

   277   | "L_rexp (EMPTY) = {[]}"

   277   | "L_rexp (EMPTY) = {[]}"

   278   | "L_rexp (CHAR c) = {[c]}"

   278   | "L_rexp (CHAR c) = {[c]}"

   279   | "L_rexp (SEQ r1 r2) = (L_rexp r1) ;; (L_rexp r2)"

   279   | "L_rexp (SEQ r1 r2) = (L_rexp r1) ;; (L_rexp r2)"

   280   | "L_rexp (ALT r1 r2) = (L_rexp r1) \<union> (L_rexp r2)"

   280   | "L_rexp (ALT r1 r2) = (L_rexp r1) \<union> (L_rexp r2)"

   281   | "L_rexp (STAR r) = (L_rexp r)\<star>"

   281   | "L_rexp (STAR r) = (L_rexp r)\<star>"

   282 end

   282 end

   283 

   283 

   284 text {* ALT-combination of a set or regulare expressions *}

   285 text {* ALT-combination of a set or regulare expressions *}

   285 

   286 

   286 abbreviation

   287 abbreviation

   287   Setalt  ("\<Uplus>_" [1000] 999) 

   288   Setalt  ("\<Uplus>_" [1000] 999) 

   288 where

   289 where

   291 text {* 

   292 text {* 

   292   For finite sets, @{term Setalt} is preserved under @{term L}.

   293   For finite sets, @{term Setalt} is preserved under @{term L}.

   293 *}

   294 *}

   294 

   295 

   295 lemma folds_alt_simp [simp]:

   296 lemma folds_alt_simp [simp]:

   296   assumes a: "finite rs"

   298   assumes a: "finite rs"

   297   shows "L (\<Uplus>rs) = \<Union> (L ` rs)"

   299   shows "L (\<Uplus>rs) = \<Union> (L ` rs)"

   298 apply(rule set_eqI)

   300 apply(rule set_eqI)

   299 apply(simp add: folds_def)

   301 apply(simp add: folds_def)

   300 apply(rule someI2_ex)

   302 apply(rule someI2_ex)