Theory Closures

(* Author: Christian Urban, Xingyuan Zhang, Chunhan Wu *)
theory Closures
imports Myhill "HOL-Library.Infinite_Set"
begin

section ‹Closure properties of regular languages›

abbreviation
  regular :: "'a lang ⇒ bool"
where
  "regular A ≡ ∃r. A = lang r"

subsection ‹Closure under ‹∪›, ‹⋅› and ‹⋆››

lemma closure_union [intro]:
  assumes "regular A" "regular B" 
  shows "regular (A ∪ B)"
proof -
  from assms obtain r1 r2::"'a rexp" where "lang r1 = A" "lang r2 = B" by auto
  then have "A ∪ B = lang (Plus r1 r2)" by simp
  then show "regular (A ∪ B)" by blast
qed

lemma closure_seq [intro]:
  assumes "regular A" "regular B" 
  shows "regular (A ⋅ B)"
proof -
  from assms obtain r1 r2::"'a rexp" where "lang r1 = A" "lang r2 = B" by auto
  then have "A ⋅ B = lang (Times r1 r2)" by simp
  then show "regular (A ⋅ B)" by blast
qed

lemma closure_star [intro]:
  assumes "regular A"
  shows "regular (A⋆)"
proof -
  from assms obtain r::"'a rexp" where "lang r = A" by auto
  then have "A⋆ = lang (Star r)" by simp
  then show "regular (A⋆)" by blast
qed

subsection ‹Closure under complementation›

text ‹Closure under complementation is proved via the 
  Myhill-Nerode theorem›

lemma closure_complement [intro]:
  fixes A::"('a::finite) lang"
  assumes "regular A"
  shows "regular (- A)"
proof -
  from assms have "finite (UNIV // ≈A)" by (simp add: Myhill_Nerode)
  then have "finite (UNIV // ≈(-A))" by (simp add: str_eq_def)
  then show "regular (- A)" by (simp add: Myhill_Nerode)
qed

subsection ‹Closure under ‹-› and ‹∩››

lemma closure_difference [intro]:
  fixes A::"('a::finite) lang"
  assumes "regular A" "regular B" 
  shows "regular (A - B)"
proof -
  have "A - B = - (- A ∪ B)" by blast
  moreover
  have "regular (- (- A ∪ B))" 
    using assms by blast
  ultimately show "regular (A - B)" by simp
qed

lemma closure_intersection [intro]:
  fixes A::"('a::finite) lang"
  assumes "regular A" "regular B" 
  shows "regular (A ∩ B)"
proof -
  have "A ∩ B = - (- A ∪ - B)" by blast
  moreover
  have "regular (- (- A ∪ - B))" 
    using assms by blast
  ultimately show "regular (A ∩ B)" by simp
qed

subsection ‹Closure under string reversal›

fun
  Rev :: "'a rexp ⇒ 'a rexp"
where
  "Rev Zero = Zero"
| "Rev One = One"
| "Rev (Atom c) = Atom c"
| "Rev (Plus r1 r2) = Plus (Rev r1) (Rev r2)"
| "Rev (Times r1 r2) = Times (Rev r2) (Rev r1)"
| "Rev (Star r) = Star (Rev r)"

lemma rev_seq[simp]:
  shows "rev ` (B ⋅ A) = (rev ` A) ⋅ (rev ` B)"
unfolding conc_def image_def
by (auto) (metis rev_append)+

lemma rev_star1:
  assumes a: "s ∈ (rev ` A)⋆"
  shows "s ∈ rev ` (A⋆)"
using a
proof(induct rule: star_induct)
  case (append s1 s2)
  have inj: "inj (rev::'a list ⇒ 'a list)" unfolding inj_on_def by auto
  have "s1 ∈ rev ` A" "s2 ∈ rev ` (A⋆)" by fact+
  then obtain x1 x2 where "x1 ∈ A" "x2 ∈ A⋆" and eqs: "s1 = rev x1" "s2 = rev x2" by auto
  then have "x1 ∈ A⋆" "x2 ∈ A⋆" by (auto)
  then have "x2 @ x1 ∈ A⋆" by (auto)
  then have "rev (x2 @ x1) ∈ rev ` A⋆" using inj by (simp only: inj_image_mem_iff)
  then show "s1 @ s2 ∈  rev ` A⋆" using eqs by simp
qed (auto)

lemma rev_star2:
  assumes a: "s ∈ A⋆"
  shows "rev s ∈ (rev ` A)⋆"
using a
proof(induct rule: star_induct)
  case (append s1 s2)
  have inj: "inj (rev::'a list ⇒ 'a list)" unfolding inj_on_def by auto
  have "s1 ∈ A"by fact
  then have "rev s1 ∈ rev ` A" using inj by (simp only: inj_image_mem_iff)
  then have "rev s1 ∈ (rev ` A)⋆" by (auto)
  moreover
  have "rev s2 ∈ (rev ` A)⋆" by fact
  ultimately show "rev (s1 @ s2) ∈  (rev ` A)⋆" by (auto)
qed (auto)

lemma rev_star [simp]:
  shows " rev ` (A⋆) = (rev ` A)⋆"
using rev_star1 rev_star2 by auto

lemma rev_lang:
  shows "rev ` (lang r) = lang (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::"'a rexp" where "A = lang r" by auto
  then have "lang (Rev r) = rev ` A" by (simp add: rev_lang)
  then show "regular (rev` A)" by blast
qed
  
subsection ‹Closure under left-quotients›

abbreviation
  "Deriv_lang A B ≡ ⋃x ∈ A. Derivs x B"

lemma closure_left_quotient:
  assumes "regular A"
  shows "regular (Deriv_lang B A)"
proof -
  from assms obtain r::"'a rexp" where eq: "lang r = A" by auto
  have fin: "finite (pderivs_lang B r)" by (rule finite_pderivs_lang)
  
  have "Deriv_lang B (lang r) = (⋃ (lang ` pderivs_lang B r))"
    by (simp add: Derivs_pderivs pderivs_lang_def)
  also have "… = lang (⨄(pderivs_lang B r))" using fin by simp
  finally have "Deriv_lang B A = lang (⨄(pderivs_lang B r))" using eq
    by simp
  then show "regular (Deriv_lang B A)" by auto
qed

subsection ‹Finite and co-finite sets are regular›

lemma singleton_regular:
  shows "regular {s}"
proof (induct s)
  case Nil
  have "{[]} = lang (One)" by simp
  then show "regular {[]}" by blast
next
  case (Cons c s)
  have "regular {s}" by fact
  then obtain r where "{s} = lang r" by blast
  then have "{c # s} = lang (Times (Atom c) r)" 
    by (auto simp add: conc_def)
  then show "regular {c # s}" by blast
qed

lemma finite_regular:
  assumes "finite A"
  shows "regular A"
using assms
proof (induct)
  case empty
  have "{} = lang (Zero)" by simp
  then show "regular {}" by blast
next
  case (insert s A)
  have "regular {s}" by (simp add: singleton_regular)
  moreover
  have "regular A" by fact
  ultimately have "regular ({s} ∪ A)" by (rule closure_union)
  then show "regular (insert s A)" by simp
qed

lemma cofinite_regular:
  fixes A::"'a::finite lang"
  assumes "finite (- A)"
  shows "regular A"
proof -
  from assms have "regular (- A)" by (simp add: finite_regular)
  then have "regular (-(- A))" by (rule closure_complement)
  then show "regular A" by simp
qed


subsection ‹Continuation lemma for showing non-regularity of languages›

lemma continuation_lemma:
  fixes A B::"'a::finite lang"
  assumes reg: "regular A"
  and     inf: "infinite B"
  shows "∃x ∈ B. ∃y ∈ B. x ≠ y ∧ x ≈A y"
proof -
  define eqfun where "eqfun = (λA x::('a::finite list). (≈A) `` {x})"
  have "finite (UNIV // ≈A)" using reg by (simp add: Myhill_Nerode)
  moreover
  have "(eqfun A) ` B ⊆ UNIV // (≈A)"
    unfolding eqfun_def quotient_def by auto
  ultimately have "finite ((eqfun A) ` B)" by (rule rev_finite_subset)
  with inf have "∃a ∈ B. infinite {b ∈ B. eqfun A b = eqfun A a}"
    by (rule pigeonhole_infinite)
  then obtain a where in_a: "a ∈ B" and "infinite {b ∈ B. eqfun A b = eqfun A a}"
    by blast
  moreover 
  have "{b ∈ B. eqfun A b = eqfun A a} = {b ∈ B. b ≈A a}"
    unfolding eqfun_def Image_def str_eq_def by auto
  ultimately have "infinite {b ∈ B. b ≈A a}" by simp
  then have "infinite ({b ∈ B. b ≈A a} - {a})" by simp
  moreover
  have "{b ∈ B. b ≈A a} - {a} = {b ∈ B. b ≈A a ∧ b ≠ a}" by auto
  ultimately have "infinite {b ∈ B. b ≈A a ∧ b ≠ a}" by simp
  then have "{b ∈ B. b ≈A a ∧ b ≠ a} ≠ {}"
    by (metis finite.emptyI)
  then obtain b where "b ∈ B" "b ≠ a" "b ≈A a" by blast
  with in_a show "∃x ∈ B. ∃y ∈ B. x ≠ y ∧ x ≈A y"
    by blast
qed


subsection ‹The language ‹a⇧n b⇧n› is not regular›

abbreviation
  replicate_rev ("_ ^^^ _" [100, 100] 100)
where
  "a ^^^ n ≡ replicate n a"

lemma an_bn_not_regular:
  shows "¬ regular (⋃n. {CHR ''a'' ^^^ n @ CHR ''b'' ^^^ n})"
proof
  define A where "A = (⋃n. {CHR ''a'' ^^^ n @ CHR ''b'' ^^^ n})"
  assume as: "regular A"
  define B where "B = (⋃n. {CHR ''a'' ^^^ n})"

  have sameness: "⋀i j. CHR ''a'' ^^^ i @ CHR ''b'' ^^^ j ∈ A ⟷ i = j"
    unfolding A_def 
    apply auto
    apply(drule_tac f="λs. length (filter ((=) (CHR ''a'')) s) = length (filter ((=) (CHR ''b'')) s)" 
      in arg_cong)
    apply(simp)
    done

  have b: "infinite B"
    unfolding infinite_iff_countable_subset
    unfolding inj_on_def B_def
    by (rule_tac x="λn. CHR ''a'' ^^^ n" in exI) (auto)
  moreover
  have "∀x ∈ B. ∀y ∈ B. x ≠ y ⟶ ¬ (x ≈A y)"
    apply(auto)
    unfolding B_def
    apply(auto)
    apply(simp add: str_eq_def)
    apply(drule_tac x="CHR ''b'' ^^^ xa" in spec)
    apply(simp add: sameness)
    done
  ultimately 
  show "False" using continuation_lemma[OF as] by blast
qed


end