theory Closure
imports Myhill_2
begin

section {* 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 blast
qed

lemma 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 blast
qed

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


text {* 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_def
apply(auto)
apply(rule_tac x="xb @ xa" in exI)
apply(auto)
done

lemma rev_Star1:
  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)

lemma rev_Star2:
  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_Star:
  "(rev ` A)\<star> = rev ` (A\<star>)"
using rev_Star1 rev_Star2 by auto

lemma 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 blast
qed
  

end