theory Closure

begin

section {* Closure properties of regular languages *}

abbreviation

  regular :: "lang \<Rightarrow> bool"

where

lemma closure_union[intro]:

  assumes "regular A" "regular B" 

  shows "regular (A \<union> B)"

proof -

  then show "regular (A \<union> B)" by blast

qed

lemma closure_seq[intro]:

  assumes "regular A" "regular B" 

proof -

qed

lemma closure_star[intro]:

  assumes "regular A"

  shows "regular (A\<star>)"

proof -

  then show "regular (A\<star>)" by blast

qed

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)

qed

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

qed

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

qed

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

unfolding Seq_def image_def

  assumes a: "s \<in> (rev ` A)\<star>"

  shows "s \<in> rev ` (A\<star>)"

using a

proof(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 simp

qed (auto)

  assumes a: "s \<in> A\<star>"

  shows "rev s \<in> (rev ` A)\<star>"

using a

proof(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_lang:

lemma closure_reversal[intro]:

  assumes "regular A"

  shows "regular (rev ` A)"

proof -

  then show "regular (rev` A)" by blast

qed

end