799 lemma Myhill_Nerode2:

   799 lemma Myhill_Nerode2:

   800   fixes r::"rexp"

   800   fixes r::"rexp"

   801   shows "finite (UNIV // \<approx>(L r))"

   801   shows "finite (UNIV // \<approx>(L r))"

   802 by (induct r) (auto)

   802 by (induct r) (auto)

   803 

   803 

   804 

   807 

   805 (*

   808 (*

   806 section {* Closure properties *}

   809 section {* Closure properties *}

   807 

   810 

   808 abbreviation

   811 abbreviation

   809   reg :: "lang \<Rightarrow> bool"

   812   reg :: "lang \<Rightarrow> bool"

   810 where

   813 where

   811   "reg A \<equiv> \<exists>r::rexp. A = L r"

   814   "reg A \<equiv> \<exists>r::rexp. A = L r"

   812 

   815 

   813 

   816 

   817 

   817 

   818 lemma closure_union[intro]:

   818 lemma closure_union[intro]:

   819   assumes "reg A" "reg B" 

   819   assumes "reg A" "reg B" 

   820   shows "reg (A \<union> B)"

   820   shows "reg (A \<union> B)"

   821 using assms

   821 using assms