(* Author: Christian Urban, Xingyuan Zhang, Chunhan Wu *)theory Closureimports Derivsbeginsection {* Closure properties of regular languages *}abbreviation regular :: "lang \<Rightarrow> bool"where "regular A \<equiv> \<exists>r. A = L_rexp r"subsection {* Closure under set operations *}lemma closure_union[intro]: assumes "regular A" "regular B" shows "regular (A \<union> B)"proof - from assms obtain r1 r2::rexp where "L_rexp r1 = A" "L_rexp r2 = B" by auto then have "A \<union> B = L_rexp (ALT r1 r2)" by simp then show "regular (A \<union> B)" by blastqedlemma closure_seq[intro]: assumes "regular A" "regular B" shows "regular (A \<cdot> B)"proof - from assms obtain r1 r2::rexp where "L_rexp r1 = A" "L_rexp r2 = B" by auto then have "A \<cdot> B = L_rexp (SEQ r1 r2)" by simp then show "regular (A \<cdot> B)" by blastqedlemma closure_star[intro]: assumes "regular A" shows "regular (A\<star>)"proof - from assms obtain r::rexp where "L_rexp r = A" by auto then have "A\<star> = L_rexp (STAR r)" by simp then show "regular (A\<star>)" by blastqedtext {* Closure under complementation is proved via the Myhill-Nerode theorem *}lemma 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 simpqedsubsection {* 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[simp]: shows "rev ` (B \<cdot> A) = (rev ` A) \<cdot> (rev ` B)"unfolding Seq_def image_defby (auto) (metis rev_append)+lemma 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[simp]: shows " rev ` (A\<star>) = (rev ` A)\<star>"using rev_star1 rev_star2 by autolemma rev_lang: shows "rev ` (L_rexp r) = L_rexp (Rev r)"by (induct r) (simp_all add: image_Un)lemma closure_reversal[intro]: assumes "regular A" shows "regular (rev ` A)"proof - from assms obtain r::rexp where "A = L_rexp r" by auto then have "L_rexp (Rev r) = rev ` A" by (simp add: rev_lang) then show "regular (rev` A)" by blastqedsubsection {* Closure under left-quotients *}lemma closure_left_quotient: assumes "regular A" shows "regular (Ders_set B A)"proof - from assms obtain r::rexp where eq: "L_rexp r = A" by auto have fin: "finite (pders_set B r)" by (rule finite_pders_set) have "Ders_set B (L_rexp r) = (\<Union> L_rexp ` (pders_set B r))" by (simp add: Ders_set_pders_set) also have "\<dots> = L_rexp (\<Uplus>(pders_set B r))" using fin by simp finally have "Ders_set B A = L_rexp (\<Uplus>(pders_set B r))" using eq by simp then show "regular (Ders_set B A)" by autoqedend