911 

   912 section {* Closure properties *}

   913 

   914 abbreviation

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

   916 where

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

   918 

   919 

   920 theorem Myhill_Nerode:

   921   shows "reg A \<longleftrightarrow> finite (UNIV // \<approx>A)"

   922 using Myhill_Nerode1 Myhill_Nerode2 by auto

   923 

   924 lemma closure_union[intro]:

   925   assumes "reg A" "reg B" 

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

   927 using assms

   928 apply(auto)

   929 apply(rule_tac x="ALT r ra" in exI)

   930 apply(auto)

   931 done

   932 

   933 lemma closure_seq[intro]:

   934   assumes "reg A" "reg B" 

   935   shows "reg (A ;; B)"

   936 using assms

   937 apply(auto)

   938 apply(rule_tac x="SEQ r ra" in exI)

   939 apply(auto)

   940 done

   941 

   942 lemma closure_star[intro]:

   943   assumes "reg A"

   944   shows "reg (A\<star>)"

   945 using assms

   946 apply(auto)

   947 apply(rule_tac x="STAR r" in exI)

   948 apply(auto)

   949 done

   950 

   951 lemma closure_complement[intro]:

   952   assumes "reg A"

   953   shows "reg (- A)"

   954 using assms

   955 unfolding Myhill_Nerode

   956 unfolding str_eq_rel_def

   957 by auto

   958 

   959 lemma closure_difference[intro]:

   960   assumes "reg A" "reg B" 

   961   shows "reg (A - B)"

   962 proof -

   963   have "A - B = - ((- A) \<union> B)" by blast

   964   moreover

   965   have "reg (- ((- A) \<union> B))" 

   966     using assms by blast

   967   ultimately show "reg (A - B)" by simp

   968 qed

   969 

   970 lemma closure_intersection[intro]:

   971   assumes "reg A" "reg B" 

   972   shows "reg (A \<inter> B)"

   973 proof -

   974   have "A \<inter> B = - ((- A) \<union> (- B))" by blast

   975   moreover

   976   have "reg (- ((- A) \<union> (- B)))" 

   977     using assms by blast

   978   ultimately show "reg (A \<inter> B)" by simp

   979 qed

   980 

   981