added directory for journal version; took uptodate version of the theory files
theory Closureimports Myhill_2beginsection {* Closure properties of regular languages *}abbreviation regular :: "lang \<Rightarrow> bool"where "regular A \<equiv> \<exists>r::rexp. A = L r"lemma closure_union[intro]: assumes "regular A" "regular B" shows "regular (A \<union> B)"proof - from assms obtain r1 r2::rexp where "L r1 = A" "L r2 = B" by auto then have "A \<union> B = L (ALT r1 r2)" by simp then show "regular (A \<union> B)" by blastqedlemma closure_seq[intro]: assumes "regular A" "regular B" shows "regular (A ;; B)"proof - from assms obtain r1 r2::rexp where "L r1 = A" "L r2 = B" by auto then have "A ;; B = L (SEQ r1 r2)" by simp then show "regular (A ;; B)" by blastqedlemma closure_star[intro]: assumes "regular A" shows "regular (A\<star>)"proof - from assms obtain r::rexp where "L r = A" by auto then have "A\<star> = L (STAR r)" by simp then show "regular (A\<star>)" by blastqedlemma closure_complement[intro]: assumes "regular A" shows "regular (- A)"proof - from assms have "finite (UNIV // \<approx>A)" by (simp add: Myhill_Nerode) then have "finite (UNIV // \<approx>(-A))" by (simp add: str_eq_rel_def) then show "regular (- A)" by (simp add: Myhill_Nerode)qedlemma closure_difference[intro]: assumes "regular A" "regular B" shows "regular (A - B)"proof - have "A - B = - (- A \<union> B)" by blast moreover have "regular (- (- A \<union> B))" using assms by blast ultimately show "regular (A - B)" by simpqedlemma closure_intersection[intro]: assumes "regular A" "regular B" shows "regular (A \<inter> B)"proof - have "A \<inter> B = - (- A \<union> - B)" by blast moreover have "regular (- (- A \<union> - B))" using assms by blast ultimately show "regular (A \<inter> B)" by simpqedtext {* closure under string reversal *}fun Rev :: "rexp \<Rightarrow> rexp"where "Rev NULL = NULL"| "Rev EMPTY = EMPTY"| "Rev (CHAR c) = CHAR c"| "Rev (ALT r1 r2) = ALT (Rev r1) (Rev r2)"| "Rev (SEQ r1 r2) = SEQ (Rev r2) (Rev r1)"| "Rev (STAR r) = STAR (Rev r)"lemma rev_Seq: "(rev ` A) ;; (rev ` B) = rev ` (B ;; A)"unfolding Seq_def image_defapply(auto)apply(rule_tac x="xb @ xa" in exI)apply(auto)donelemma rev_Star1: assumes a: "s \<in> (rev ` A)\<star>" shows "s \<in> rev ` (A\<star>)"using aproof(induct rule: star_induct) case (step s1 s2) have inj: "inj (rev::string \<Rightarrow> string)" unfolding inj_on_def by auto have "s1 \<in> rev ` A" "s2 \<in> rev ` (A\<star>)" by fact+ then obtain x1 x2 where "x1 \<in> A" "x2 \<in> A\<star>" and eqs: "s1 = rev x1" "s2 = rev x2" by auto then have "x1 \<in> A\<star>" "x2 \<in> A\<star>" by (auto intro: star_intro2) then have "x2 @ x1 \<in> A\<star>" by (auto intro: star_intro1) then have "rev (x2 @ x1) \<in> rev ` A\<star>" using inj by (simp only: inj_image_mem_iff) then show "s1 @ s2 \<in> rev ` A\<star>" using eqs by simpqed (auto)lemma rev_Star2: assumes a: "s \<in> A\<star>" shows "rev s \<in> (rev ` A)\<star>"using aproof(induct rule: star_induct) case (step s1 s2) have inj: "inj (rev::string \<Rightarrow> string)" unfolding inj_on_def by auto have "s1 \<in> A"by fact then have "rev s1 \<in> rev ` A" using inj by (simp only: inj_image_mem_iff) then have "rev s1 \<in> (rev ` A)\<star>" by (auto intro: star_intro2) moreover have "rev s2 \<in> (rev ` A)\<star>" by fact ultimately show "rev (s1 @ s2) \<in> (rev ` A)\<star>" by (auto intro: star_intro1)qed (auto)lemma rev_Star: "(rev ` A)\<star> = rev ` (A\<star>)"using rev_Star1 rev_Star2 by autolemma rev_lang: "L (Rev r) = rev ` (L r)"by (induct r) (simp_all add: rev_Star rev_Seq image_Un)lemma closure_reversal[intro]: assumes "regular A" shows "regular (rev ` A)"proof - from assms obtain r::rexp where "L r = A" by auto then have "L (Rev r) = rev ` A" by (simp add: rev_lang) then show "regular (rev` A)" by blastqedend