--- 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