1 theory Regular

     2 imports Main Folds

     3 begin

     4 

     5 section {* Preliminary definitions *}

     6 

     7 type_synonym lang = "string set"

     8 

     9 

    10 text {*  Sequential composition of two languages *}

    11 

    12 definition 

    13   Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" (infixr ";;" 100)

    14 where 

    15   "A ;; B = {s\<^isub>1 @ s\<^isub>2 | s\<^isub>1 s\<^isub>2. s\<^isub>1 \<in> A \<and> s\<^isub>2 \<in> B}"

    16 

    17 

    18 text {* Some properties of operator @{text ";;"}. *}

    19 

    20 lemma seq_add_left:

    21   assumes a: "A = B"

    22   shows "C ;; A = C ;; B"

    23 using a by simp

    24 

    25 lemma seq_union_distrib_right:

    26   shows "(A \<union> B) ;; C = (A ;; C) \<union> (B ;; C)"

    27 unfolding Seq_def by auto

    28 

    29 lemma seq_union_distrib_left:

    30   shows "C ;; (A \<union> B) = (C ;; A) \<union> (C ;; B)"

    31 unfolding Seq_def by  auto

    32 

    33 lemma seq_intro:

    34   assumes a: "x \<in> A" "y \<in> B"

    35   shows "x @ y \<in> A ;; B "

    36 using a by (auto simp: Seq_def)

    37 

    38 lemma seq_assoc:

    39   shows "(A ;; B) ;; C = A ;; (B ;; C)"

    40 unfolding Seq_def

    41 apply(auto)

    42 apply(blast)

    43 by (metis append_assoc)

    44 

    45 lemma seq_empty [simp]:

    46   shows "A ;; {[]} = A"

    47   and   "{[]} ;; A = A"

    48 by (simp_all add: Seq_def)

    49 

    50 lemma seq_null [simp]:

    51   shows "A ;; {} = {}"

    52   and   "{} ;; A = {}"

    53 by (simp_all add: Seq_def)

    54 

    55 

    56 text {* Power and Star of a language *}

    57 

    58 fun 

    59   pow :: "lang \<Rightarrow> nat \<Rightarrow> lang" (infixl "\<up>" 100)

    60 where

    61   "A \<up> 0 = {[]}"

    62 | "A \<up> (Suc n) =  A ;; (A \<up> n)" 

    63 

    64 definition

    65   Star :: "lang \<Rightarrow> lang" ("_\<star>" [101] 102)

    66 where

    67   "A\<star> \<equiv> (\<Union>n. A \<up> n)"

    68 

    69 

    70 lemma star_start[intro]:

    71   shows "[] \<in> A\<star>"

    72 proof -

    73   have "[] \<in> A \<up> 0" by auto

    74   then show "[] \<in> A\<star>" unfolding Star_def by blast

    75 qed

    76 

    77 lemma star_step [intro]:

    78   assumes a: "s1 \<in> A" 

    79   and     b: "s2 \<in> A\<star>"

    80   shows "s1 @ s2 \<in> A\<star>"

    81 proof -

    82   from b obtain n where "s2 \<in> A \<up> n" unfolding Star_def by auto

    83   then have "s1 @ s2 \<in> A \<up> (Suc n)" using a by (auto simp add: Seq_def)

    84   then show "s1 @ s2 \<in> A\<star>" unfolding Star_def by blast

    85 qed

    86 

    87 lemma star_induct[consumes 1, case_names start step]:

    88   assumes a: "x \<in> A\<star>" 

    89   and     b: "P []"

    90   and     c: "\<And>s1 s2. \<lbrakk>s1 \<in> A; s2 \<in> A\<star>; P s2\<rbrakk> \<Longrightarrow> P (s1 @ s2)"

    91   shows "P x"

    92 proof -

    93   from a obtain n where "x \<in> A \<up> n" unfolding Star_def by auto

    94   then show "P x"

    95     by (induct n arbitrary: x)

    96        (auto intro!: b c simp add: Seq_def Star_def)

    97 qed

    98     

    99 lemma star_intro1:

   100   assumes a: "x \<in> A\<star>"

   101   and     b: "y \<in> A\<star>"

   102   shows "x @ y \<in> A\<star>"

   103 using a b

   104 by (induct rule: star_induct) (auto)

   105 

   106 lemma star_intro2: 

   107   assumes a: "y \<in> A"

   108   shows "y \<in> A\<star>"

   109 proof -

   110   from a have "y @ [] \<in> A\<star>" by blast

   111   then show "y \<in> A\<star>" by simp

   112 qed

   113 

   114 lemma star_intro3:

   115   assumes a: "x \<in> A\<star>"

   116   and     b: "y \<in> A"

   117   shows "x @ y \<in> A\<star>"

   118 using a b by (blast intro: star_intro1 star_intro2)

   119 

   120 lemma star_cases:

   121   shows "A\<star> =  {[]} \<union> A ;; A\<star>"

   122 proof

   123   { fix x

   124     have "x \<in> A\<star> \<Longrightarrow> x \<in> {[]} \<union> A ;; A\<star>"

   125       unfolding Seq_def

   126     by (induct rule: star_induct) (auto)

   127   }

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

   129 next

   130   show "{[]} \<union> A ;; A\<star> \<subseteq> A\<star>"

   131     unfolding Seq_def by auto

   132 qed

   133 

   134 lemma star_decom: 

   135   assumes a: "x \<in> A\<star>" "x \<noteq> []"

   136   shows "\<exists>a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> A\<star>"

   137 using a

   138 by (induct rule: star_induct) (blast)+

   139 

   140 lemma

   141   shows seq_Union_left:  "B ;; (\<Union>n. A \<up> n) = (\<Union>n. B ;; (A \<up> n))"

   142   and   seq_Union_right: "(\<Union>n. A \<up> n) ;; B = (\<Union>n. (A \<up> n) ;; B)"

   143 unfolding Seq_def by auto

   144 

   145 lemma seq_pow_comm:

   146   shows "A ;; (A \<up> n) = (A \<up> n) ;; A"

   147 by (induct n) (simp_all add: seq_assoc[symmetric])

   148 

   149 lemma seq_star_comm:

   150   shows "A ;; A\<star> = A\<star> ;; A"

   151 unfolding Star_def seq_Union_left

   152 unfolding seq_pow_comm seq_Union_right 

   153 by simp

   154 

   155 

   156 text {* Two lemmas about the length of strings in @{text "A \<up> n"} *}

   157 

   158 lemma pow_length:

   159   assumes a: "[] \<notin> A"

   160   and     b: "s \<in> A \<up> Suc n"

   161   shows "n < length s"

   162 using b

   163 proof (induct n arbitrary: s)

   164   case 0

   165   have "s \<in> A \<up> Suc 0" by fact

   166   with a have "s \<noteq> []" by auto

   167   then show "0 < length s" by auto

   168 next

   169   case (Suc n)

   170   have ih: "\<And>s. s \<in> A \<up> Suc n \<Longrightarrow> n < length s" by fact

   171   have "s \<in> A \<up> Suc (Suc n)" by fact

   172   then obtain s1 s2 where eq: "s = s1 @ s2" and *: "s1 \<in> A" and **: "s2 \<in> A \<up> Suc n"

   173     by (auto simp add: Seq_def)

   174   from ih ** have "n < length s2" by simp

   175   moreover have "0 < length s1" using * a by auto

   176   ultimately show "Suc n < length s" unfolding eq 

   177     by (simp only: length_append)

   178 qed

   179 

   180 lemma seq_pow_length:

   181   assumes a: "[] \<notin> A"

   182   and     b: "s \<in> B ;; (A \<up> Suc n)"

   183   shows "n < length s"

   184 proof -

   185   from b obtain s1 s2 where eq: "s = s1 @ s2" and *: "s2 \<in> A \<up> Suc n"

   186     unfolding Seq_def by auto

   187   from * have " n < length s2" by (rule pow_length[OF a])

   188   then show "n < length s" using eq by simp

   189 qed

   190 

   191 

   192 section {* A modified version of Arden's lemma *}

   193 

   194 text {*  A helper lemma for Arden *}

   195 

   196 lemma arden_helper:

   197   assumes eq: "X = X ;; A \<union> B"

   198   shows "X = X ;; (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))"

   199 proof (induct n)

   200   case 0 

   201   show "X = X ;; (A \<up> Suc 0) \<union> (\<Union>(m::nat)\<in>{0..0}. B ;; (A \<up> m))"

   202     using eq by simp

   203 next

   204   case (Suc n)

   205   have ih: "X = X ;; (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))" by fact

   206   also have "\<dots> = (X ;; A \<union> B) ;; (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))" using eq by simp

   207   also have "\<dots> = X ;; (A \<up> Suc (Suc n)) \<union> (B ;; (A \<up> Suc n)) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))"

   208     by (simp add: seq_union_distrib_right seq_assoc)

   209   also have "\<dots> = X ;; (A \<up> Suc (Suc n)) \<union> (\<Union>m\<in>{0..Suc n}. B ;; (A \<up> m))"

   210     by (auto simp add: le_Suc_eq)

   211   finally show "X = X ;; (A \<up> Suc (Suc n)) \<union> (\<Union>m\<in>{0..Suc n}. B ;; (A \<up> m))" .

   212 qed

   213 

   214 theorem arden:

   215   assumes nemp: "[] \<notin> A"

   216   shows "X = X ;; A \<union> B \<longleftrightarrow> X = B ;; A\<star>"

   217 proof

   218   assume eq: "X = B ;; A\<star>"

   219   have "A\<star> = {[]} \<union> A\<star> ;; A" 

   220     unfolding seq_star_comm[symmetric]

   221     by (rule star_cases)

   222   then have "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"

   223     by (rule seq_add_left)

   224   also have "\<dots> = B \<union> B ;; (A\<star> ;; A)"

   225     unfolding seq_union_distrib_left by simp

   226   also have "\<dots> = B \<union> (B ;; A\<star>) ;; A" 

   227     by (simp only: seq_assoc)

   228   finally show "X = X ;; A \<union> B" 

   229     using eq by blast 

   230 next

   231   assume eq: "X = X ;; A \<union> B"

   232   { fix n::nat

   233     have "B ;; (A \<up> n) \<subseteq> X" using arden_helper[OF eq, of "n"] by auto }

   234   then have "B ;; A\<star> \<subseteq> X" 

   235     unfolding Seq_def Star_def UNION_def by auto

   236   moreover

   237   { fix s::string

   238     obtain k where "k = length s" by auto

   239     then have not_in: "s \<notin> X ;; (A \<up> Suc k)" 

   240       using seq_pow_length[OF nemp] by blast

   241     assume "s \<in> X"

   242     then have "s \<in> X ;; (A \<up> Suc k) \<union> (\<Union>m\<in>{0..k}. B ;; (A \<up> m))"

   243       using arden_helper[OF eq, of "k"] by auto

   244     then have "s \<in> (\<Union>m\<in>{0..k}. B ;; (A \<up> m))" using not_in by auto

   245     moreover

   246     have "(\<Union>m\<in>{0..k}. B ;; (A \<up> m)) \<subseteq> (\<Union>n. B ;; (A \<up> n))" by auto

   247     ultimately 

   248     have "s \<in> B ;; A\<star>" 

   249       unfolding seq_Union_left Star_def by auto }

   250   then have "X \<subseteq> B ;; A\<star>" by auto

   251   ultimately 

   252   show "X = B ;; A\<star>" by simp

   253 qed

   254 

   255 

   256 section {* Regular Expressions *}

   257 

   258 datatype rexp =

   259   NULL

   260 | EMPTY

   261 | CHAR char

   262 | SEQ rexp rexp

   263 | ALT rexp rexp

   264 | STAR rexp

   265 

   266 

   267 text {* 

   268   The function @{text L} is overloaded, with the idea that @{text "L x"} 

   269   evaluates to the language represented by the object @{text x}.

   270 *}

   271 

   272 consts L:: "'a \<Rightarrow> lang"

   273 

   274 overloading L_rexp \<equiv> "L::  rexp \<Rightarrow> lang"

   275 begin

   276 fun

   277   L_rexp :: "rexp \<Rightarrow> lang"

   278 where

   279     "L_rexp (NULL) = {}"

   280   | "L_rexp (EMPTY) = {[]}"

   281   | "L_rexp (CHAR c) = {[c]}"

   282   | "L_rexp (SEQ r1 r2) = (L_rexp r1) ;; (L_rexp r2)"

   283   | "L_rexp (ALT r1 r2) = (L_rexp r1) \<union> (L_rexp r2)"

   284   | "L_rexp (STAR r) = (L_rexp r)\<star>"

   285 end

   286 

   287 

   288 text {* ALT-combination for a set of regular expressions *}

   289 

   290 abbreviation

   291   Setalt  ("\<Uplus>_" [1000] 999) 

   292 where

   293   "\<Uplus>A \<equiv> folds ALT NULL A"

   294 

   295 text {* 

   296   For finite sets, @{term Setalt} is preserved under @{term L}.

   297 *}

   298 

   299 lemma folds_alt_simp [simp]:

   300   fixes rs::"rexp set"

   301   assumes a: "finite rs"

   302   shows "L (\<Uplus>rs) = \<Union> (L ` rs)"

   303 unfolding folds_def

   304 apply(rule set_eqI)

   305 apply(rule someI2_ex)

   306 apply(rule_tac finite_imp_fold_graph[OF a])

   307 apply(erule fold_graph.induct)

   308 apply(auto)

   309 done

   310 

   311 end