1 theory "RegSet"

     1 theory Closure

     2   imports "Main" 

     2 imports Myhill_2

     6 text {* Sequential composition of sets *}

     7 abbreviation

     7 

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

     8 definition

     9 where

     9   lang_seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ; _" [100,100] 100)

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

    10 where 

    11   "L1 ; L2 = {s1@s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"

    14 section {* Kleene star for sets *}

    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

    16 inductive_set

    22 lemma closure_seq[intro]:

    17   Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)

    23   assumes "regular A" "regular B" 

    18   for L :: "string set"

    24   shows "regular (A ;; B)"

    19 where

    25 proof -

    20   start[intro]: "[] \<in> L\<star>"

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

    21 | step[intro]:  "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> L\<star>"

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

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

    29 qed

    24 text {* A standard property of star *}

    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

    26 lemma lang_star_cases:

    49 lemma closure_difference[intro]:

    27   shows "L\<star> =  {[]} \<union> L ; L\<star>"

    50   assumes "regular A" "regular B" 

    28 proof

    51   shows "regular (A - B)"

    29   { fix x

    52 proof -

    30     have "x \<in> L\<star> \<Longrightarrow> x \<in> {[]} \<union> L ; L\<star>"

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

    31       unfolding lang_seq_def

    54   moreover

    32     by (induct rule: Star.induct) (auto)

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

    33   }

    56     using assms by blast

    34   then show "L\<star> \<subseteq> {[]} \<union> L ; L\<star>" by auto

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

    35 next

    58 qed

    36   show "{[]} \<union> L ; L\<star> \<subseteq> L\<star>" 

    59 

    37     unfolding lang_seq_def by auto

    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

    41 lemma lang_star_cases2:

    72 text {* closure under string reversal *}

    42   shows "[] \<notin> L \<Longrightarrow> L\<star> - {[]} =  L ; L\<star>"

    43 by (subst lang_star_cases)

    44    (simp add: lang_seq_def)

    45 

    46 

    47 section {* Regular Expressions *}

    48 

    49 datatype rexp =

    50   NULL

    51 | EMPTY

    52 | CHAR char

    53 | SEQ rexp rexp

    54 | ALT rexp rexp

    55 | STAR rexp

    56 

    57 

    58 section {* Semantics of Regular Expressions *}

    61   L :: "rexp \<Rightarrow> string set"

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

    63   "L (NULL) = {}"

    77   "Rev NULL = NULL"

    64 | "L (EMPTY) = {[]}"

    78 | "Rev EMPTY = EMPTY"

    65 | "L (CHAR c) = {[c]}"

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

    66 | "L (SEQ r1 r2) = (L r1) ; (L r2)"

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

    67 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"

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

    68 | "L (STAR r) = (L r)\<star>"

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

    70 abbreviation

    84 lemma rev_Seq:

    71   CUNIV :: "string set"

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

    72 where

    86 unfolding Seq_def image_def

    73   "CUNIV \<equiv> (\<lambda>x. [x]) ` (UNIV::char set)"

    87 apply(auto)

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

    89 apply(auto)

    90 done

    75 lemma CUNIV_star_minus:

    92 lemma rev_Star1:

    76   "(CUNIV\<star> - {[c]}) = {[]} \<union> (CUNIV - {[c]}; (CUNIV\<star>))"

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

    77 apply(subst lang_star_cases)

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

    78 apply(simp add: lang_seq_def)

    95 using a

    79 oops

    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)

    82 lemma string_in_CUNIV:

   122 lemma rev_Star:

    83   shows "s \<in> CUNIV\<star>"

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

    84 proof (induct s)

   124 using rev_Star1 rev_Star2 by auto

    85   case Nil

    86   show "[] \<in> CUNIV\<star>" by (rule start)

    87 next

    88   case (Cons c s)

    89   have "[c] \<in> CUNIV" by simp

    90   moreover

    91   have "s \<in> CUNIV\<star>" by fact

    92   ultimately have "[c] @ s \<in> CUNIV\<star>" by (rule step)

    93   then show "c # s \<in> CUNIV\<star>" by simp

    94 qed

    96 lemma UNIV_CUNIV_star: 

   126 lemma rev_lang:

    97   shows "UNIV = CUNIV\<star>"

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

    98 using string_in_CUNIV

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

    99 by (auto)

   101 abbreviation 

   130 lemma closure_reversal[intro]:

   102   reg :: "string set => bool"

   131   assumes "regular A"

   103 where

   132   shows "regular (rev ` A)"

   104   "reg L1 \<equiv> (\<exists>r. L r = L1)"

   133 proof -

   105 

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

   106 lemma reg_null [intro]:

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

   107   shows "reg {}"

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

   108 by (metis L.simps(1))

   109 

   110 lemma reg_empty [intro]:

   111   shows "reg {[]}"

   112 by (metis L.simps(2))

   113 

   114 lemma reg_star [intro]:

   115   shows "reg L1 \<Longrightarrow> reg (L1\<star>)"

   116 by (metis L.simps(6))

   117 

   118 lemma reg_seq [intro]:

   119   assumes a: "reg L1" "reg L2"

   120   shows "reg (L1 ; L2)"

   121 using a

   122 by (metis L.simps(4)) 

   123 

   124 lemma reg_union [intro]:

   125   assumes a: "reg L1" "reg L2"

   126   shows "reg (L1 \<union> L2)"

   127 using a

   128 by (metis L.simps(5)) 

   129 

   130 lemma reg_string [intro]:

   131   fixes s::string

   132   shows "reg {s}"

   133 proof (induct s)

   134   case Nil

   135   show "reg {[]}" by (rule reg_empty)

   136 next

   137   case (Cons c s)

   138   have "reg {s}" by fact

   139   then obtain r where "L r = {s}" by auto

   140   then have "L (SEQ (CHAR c) r) = {[c]} ; {s}" by simp

   141   also have "\<dots> = {c # s}" by (simp add: lang_seq_def)

   142   finally show "reg {c # s}" by blast 

   143 qed

   144 

   145 lemma reg_finite [intro]:

   146   assumes a: "finite L1"

   147   shows "reg L1"

   148 using a

   149 proof(induct)

   150   case empty

   151   show "reg {}" by (rule reg_null)

   152 next

   153   case (insert s S)

   154   have "reg {s}" by (rule reg_string)

   155   moreover 

   156   have "reg S" by fact

   157   ultimately have "reg ({s} \<union> S)" by (rule reg_union)

   158   then show "reg (insert s S)" by simp

   165 lemma reg_univ:

   140 end

   166   shows "reg (UNIV::string set)"

   167 proof -

   168   have "reg CUNIV" by (rule reg_cuniv)

   169   then have "reg (CUNIV\<star>)" by (rule reg_star)

   170   then show "reg UNIV" by (simp add: UNIV_CUNIV_star)

   171 qed

   172 

   173 lemma reg_finite_subset:

   174   assumes a: "finite L1"

   175   and     b: "reg L1" "L2 \<subseteq> L1"

   176   shows "reg L2"

   177 using a b

   178 apply(induct arbitrary: L2)

   179 apply(simp add: reg_empty)

   180 oops

   181 

   182 

   183 lemma reg_not:

   184   shows "reg (UNIV - L r)"

   185 proof (induct r)

   186   case NULL

   187   have "reg UNIV" by (rule reg_univ)

   188   then show "reg (UNIV - L NULL)" by simp

   189 next

   190   case EMPTY

   191   have "[] \<notin> CUNIV" by auto

   192   moreover

   193   have "reg (CUNIV; CUNIV\<star>)" by auto

   194   ultimately have "reg (CUNIV\<star> - {[]})" 

   195     using lang_star_cases2 by simp

   196   then show "reg (UNIV - L EMPTY)" by (simp add: UNIV_CUNIV_star)

   197 next

   198   case (CHAR c)

   199   then show "?case"

   200     apply(simp)

   201    

   202 using reg_UNIV

   203 apply(simp)

   204 apply(simp add: char_star2[symmetric])

   205 apply(rule reg_seq)

   206 apply(rule reg_cuniv)

   207 apply(rule reg_star)

   208 apply(rule reg_cuniv)

   209 oops

   210 

   211 

   212 

   213 end    

   214    

   215 

   216 

   217 

   218   

   219 

   220   

   221   

   222 

   223