1 (* Author: Christian Urban, Xingyuan Zhang, Chunhan Wu *)

     2 theory Closure

     3 imports Derivs

     4 begin

     5 

     6 section {* Closure properties of regular languages *}

     7 

     8 abbreviation

     9   regular :: "lang \<Rightarrow> bool"

    10 where

    11   "regular A \<equiv> \<exists>r. A = L_rexp r"

    12 

    13 subsection {* Closure under set operations *}

    14 

    15 lemma closure_union[intro]:

    16   assumes "regular A" "regular B" 

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

    18 proof -

    19   from assms obtain r1 r2::rexp where "L_rexp r1 = A" "L_rexp r2 = B" by auto

    20   then have "A \<union> B = L_rexp (ALT r1 r2)" by simp

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

    22 qed

    23 

    24 lemma closure_seq[intro]:

    25   assumes "regular A" "regular B" 

    26   shows "regular (A \<cdot> B)"

    27 proof -

    28   from assms obtain r1 r2::rexp where "L_rexp r1 = A" "L_rexp r2 = B" by auto

    29   then have "A \<cdot> B = L_rexp (SEQ r1 r2)" by simp

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

    31 qed

    32 

    33 lemma closure_star[intro]:

    34   assumes "regular A"

    35   shows "regular (A\<star>)"

    36 proof -

    37   from assms obtain r::rexp where "L_rexp r = A" by auto

    38   then have "A\<star> = L_rexp (STAR r)" by simp

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

    40 qed

    41 

    42 text {* Closure under complementation is proved via the 

    43   Myhill-Nerode theorem *}

    44 

    45 lemma closure_complement[intro]:

    46   assumes "regular A"

    47   shows "regular (- A)"

    48 proof -

    49   from assms have "finite (UNIV // \<approx>A)" by (simp add: Myhill_Nerode)

    50   then have "finite (UNIV // \<approx>(-A))" by (simp add: str_eq_rel_def)

    51   then show "regular (- A)" by (simp add: Myhill_Nerode)

    52 qed

    53 

    54 lemma closure_difference[intro]:

    55   assumes "regular A" "regular B" 

    56   shows "regular (A - B)"

    57 proof -

    58   have "A - B = - (- A \<union> B)" by blast

    59   moreover

    60   have "regular (- (- A \<union> B))" 

    61     using assms by blast

    62   ultimately show "regular (A - B)" by simp

    63 qed

    64 

    65 lemma closure_intersection[intro]:

    66   assumes "regular A" "regular B" 

    67   shows "regular (A \<inter> B)"

    68 proof -

    69   have "A \<inter> B = - (- A \<union> - B)" by blast

    70   moreover

    71   have "regular (- (- A \<union> - B))" 

    72     using assms by blast

    73   ultimately show "regular (A \<inter> B)" by simp

    74 qed

    75 

    76 subsection {* Closure under string reversal *}

    77 

    78 fun

    79   Rev :: "rexp \<Rightarrow> rexp"

    80 where

    81   "Rev NULL = NULL"

    82 | "Rev EMPTY = EMPTY"

    83 | "Rev (CHAR c) = CHAR c"

    84 | "Rev (ALT r1 r2) = ALT (Rev r1) (Rev r2)"

    85 | "Rev (SEQ r1 r2) = SEQ (Rev r2) (Rev r1)"

    86 | "Rev (STAR r) = STAR (Rev r)"

    87 

    88 lemma rev_seq[simp]:

    89   shows "rev ` (B \<cdot> A) = (rev ` A) \<cdot> (rev ` B)"

    90 unfolding Seq_def image_def

    91 by (auto) (metis rev_append)+

    92 

    93 lemma rev_star1:

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

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

    96 using a

    97 proof(induct rule: star_induct)

    98   case (step s1 s2)

    99   have inj: "inj (rev::string \<Rightarrow> string)" unfolding inj_on_def by auto

   100   have "s1 \<in> rev ` A" "s2 \<in> rev ` (A\<star>)" by fact+

   101   then obtain x1 x2 where "x1 \<in> A" "x2 \<in> A\<star>" and eqs: "s1 = rev x1" "s2 = rev x2" by auto

   102   then have "x1 \<in> A\<star>" "x2 \<in> A\<star>" by (auto intro: star_intro2)

   103   then have "x2 @ x1 \<in> A\<star>" by (auto intro: star_intro1)

   104   then have "rev (x2 @ x1) \<in> rev ` A\<star>" using inj by (simp only: inj_image_mem_iff)

   105   then show "s1 @ s2 \<in>  rev ` A\<star>" using eqs by simp

   106 qed (auto)

   107 

   108 lemma rev_star2:

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

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

   111 using a

   112 proof(induct rule: star_induct)

   113   case (step s1 s2)

   114   have inj: "inj (rev::string \<Rightarrow> string)" unfolding inj_on_def by auto

   115   have "s1 \<in> A"by fact

   116   then have "rev s1 \<in> rev ` A" using inj by (simp only: inj_image_mem_iff)

   117   then have "rev s1 \<in> (rev ` A)\<star>" by (auto intro: star_intro2)

   118   moreover

   119   have "rev s2 \<in> (rev ` A)\<star>" by fact

   120   ultimately show "rev (s1 @ s2) \<in>  (rev ` A)\<star>" by (auto intro: star_intro1)

   121 qed (auto)

   122 

   123 lemma rev_star[simp]:

   124   shows " rev ` (A\<star>) = (rev ` A)\<star>"

   125 using rev_star1 rev_star2 by auto

   126 

   127 lemma rev_lang:

   128   shows "rev ` (L_rexp r) = L_rexp (Rev r)"

   129 by (induct r) (simp_all add: image_Un)

   130 

   131 lemma closure_reversal[intro]:

   132   assumes "regular A"

   133   shows "regular (rev ` A)"

   134 proof -

   135   from assms obtain r::rexp where "A = L_rexp r" by auto

   136   then have "L_rexp (Rev r) = rev ` A" by (simp add: rev_lang)

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

   138 qed

   139   

   140 subsection {* Closure under left-quotients *}

   141 

   142 lemma closure_left_quotient:

   143   assumes "regular A"

   144   shows "regular (Ders_set B A)"

   145 proof -

   146   from assms obtain r::rexp where eq: "L_rexp r = A" by auto

   147   have fin: "finite (pders_set B r)" by (rule finite_pders_set)

   148   

   149   have "Ders_set B (L_rexp r) = (\<Union> L_rexp ` (pders_set B r))"

   150     by (simp add: Ders_set_pders_set)

   151   also have "\<dots> = L_rexp (\<Uplus>(pders_set B r))" using fin by simp

   152   finally have "Ders_set B A = L_rexp (\<Uplus>(pders_set B r))" using eq

   153     by simp

   154   then show "regular (Ders_set B A)" by auto

   155 qed

   156 

   157 

   158 end