1 theory Closure

     2 imports Myhill_2

     3 begin

     4 

     5 section {* Closure properties of regular languages *}

     6 

     7 abbreviation

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

     9 where

    10   "regular A \<equiv> \<exists>r::rexp. A = L r"

    11 

    12 

    13 lemma closure_union[intro]:

    14   assumes "regular A" "regular B" 

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

    16 proof -

    17   from assms obtain r1 r2::rexp where "L r1 = A" "L r2 = B" by auto

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

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

    20 qed

    21 

    22 lemma closure_seq[intro]:

    23   assumes "regular A" "regular B" 

    24   shows "regular (A ;; B)"

    25 proof -

    26   from assms obtain r1 r2::rexp where "L r1 = A" "L r2 = B" by auto

    27   then have "A ;; B = L (SEQ r1 r2)" by simp

    28   then show "regular (A ;; B)" by blast

    29 qed

    30 

    31 lemma closure_star[intro]:

    32   assumes "regular A"

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

    34 proof -

    35   from assms obtain r::rexp where "L r = A" by auto

    36   then have "A\<star> = L (STAR r)" by simp

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

    38 qed

    39 

    40 lemma closure_complement[intro]:

    41   assumes "regular A"

    42   shows "regular (- A)"

    43 proof -

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

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

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

    47 qed

    48 

    49 lemma closure_difference[intro]:

    50   assumes "regular A" "regular B" 

    51   shows "regular (A - B)"

    52 proof -

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

    54   moreover

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

    56     using assms by blast

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

    58 qed

    59 

    60 lemma closure_intersection[intro]:

    61   assumes "regular A" "regular B" 

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

    63 proof -

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

    65   moreover

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

    67     using assms by blast

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

    69 qed

    70 

    71 

    72 text {* closure under string reversal *}

    73 

    74 fun

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

    76 where

    77   "Rev NULL = NULL"

    78 | "Rev EMPTY = EMPTY"

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

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

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

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

    83 

    84 lemma rev_Seq:

    85   "(rev ` A) ;; (rev ` B) = rev ` (B ;; A)"

    86 unfolding Seq_def image_def

    87 apply(auto)

    88 apply(rule_tac x="xb @ xa" in exI)

    89 apply(auto)

    90 done

    91 

    92 lemma rev_Star1:

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

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

    95 using a

    96 proof(induct rule: star_induct)

    97   case (step s1 s2)

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

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

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

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

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

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

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

   105 qed (auto)

   106 

   107 lemma rev_Star2:

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

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

   110 using a

   111 proof(induct rule: star_induct)

   112   case (step s1 s2)

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

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

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

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

   117   moreover

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

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

   120 qed (auto)

   121 

   122 lemma rev_Star:

   123   "(rev ` A)\<star> = rev ` (A\<star>)"

   124 using rev_Star1 rev_Star2 by auto

   125 

   126 lemma rev_lang:

   127   "L (Rev r) = rev ` (L r)"

   128 by (induct r) (simp_all add: rev_Star rev_Seq image_Un)

   129 

   130 lemma closure_reversal[intro]:

   131   assumes "regular A"

   132   shows "regular (rev ` A)"

   133 proof -

   134   from assms obtain r::rexp where "L r = A" by auto

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

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

   137 qed

   138   

   139 

   140 end