diff -r d65d071798ff -r 62fdb4bf7239 Myhill_2.thy
--- a/Myhill_2.thy	Thu Feb 17 13:25:29 2011 +0000
+++ b/Myhill_2.thy	Thu Feb 17 21:30:26 2011 +0000
@@ -903,9 +903,80 @@
 
 subsubsection{* The conclusion *}
 
-lemma rexp_imp_finite:
+lemma Myhill_Nerode2:
   fixes r::"rexp"
   shows "finite (UNIV // \<approx>(L r))"
 by (induct r) (auto)
 
+
+section {* Closure properties *}
+
+abbreviation
+  reg :: "lang \<Rightarrow> bool"
+where
+  "reg A \<equiv> \<exists>r::rexp. A = L r"
+
+
+theorem Myhill_Nerode:
+  shows "reg A \<longleftrightarrow> finite (UNIV // \<approx>A)"
+using Myhill_Nerode1 Myhill_Nerode2 by auto
+
+lemma closure_union[intro]:
+  assumes "reg A" "reg B" 
+  shows "reg (A \<union> B)"
+using assms
+apply(auto)
+apply(rule_tac x="ALT r ra" in exI)
+apply(auto)
+done
+
+lemma closure_seq[intro]:
+  assumes "reg A" "reg B" 
+  shows "reg (A ;; B)"
+using assms
+apply(auto)
+apply(rule_tac x="SEQ r ra" in exI)
+apply(auto)
+done
+
+lemma closure_star[intro]:
+  assumes "reg A"
+  shows "reg (A\<star>)"
+using assms
+apply(auto)
+apply(rule_tac x="STAR r" in exI)
+apply(auto)
+done
+
+lemma closure_complement[intro]:
+  assumes "reg A"
+  shows "reg (- A)"
+using assms
+unfolding Myhill_Nerode
+unfolding str_eq_rel_def
+by auto
+
+lemma closure_difference[intro]:
+  assumes "reg A" "reg B" 
+  shows "reg (A - B)"
+proof -
+  have "A - B = - ((- A) \<union> B)" by blast
+  moreover
+  have "reg (- ((- A) \<union> B))" 
+    using assms by blast
+  ultimately show "reg (A - B)" by simp
+qed
+
+lemma closure_intersection[intro]:
+  assumes "reg A" "reg B" 
+  shows "reg (A \<inter> B)"
+proof -
+  have "A \<inter> B = - ((- A) \<union> (- B))" by blast
+  moreover
+  have "reg (- ((- A) \<union> (- B)))" 
+    using assms by blast
+  ultimately show "reg (A \<inter> B)" by simp
+qed
+
+
 end