1 (*  Author: Tobias Nipkow, Alex Krauss  *)

     2 

     3 header "Regular sets"

     4 

     5 theory Regular_Set

     6 imports Main

     7 begin

     8 

     9 type_synonym 'a lang = "'a list set"

    10 

    11 definition conc :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a lang" (infixr "@@" 75) where

    12 "A @@ B = {xs@ys | xs ys. xs:A & ys:B}"

    13 

    14 overloading lang_pow == "compow :: nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang"

    15 begin

    16   primrec lang_pow :: "nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang" where

    17   "lang_pow 0 A = {[]}" |

    18   "lang_pow (Suc n) A = A @@ (lang_pow n A)"

    19 end

    20 

    21 definition star :: "'a lang \<Rightarrow> 'a lang" where

    22 "star A = (\<Union>n. A ^^ n)"

    23 

    24 

    25 

    26 definition deriv :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"

    27 where "deriv x L = { xs. x#xs \<in> L }"

    28 

    29 

    30 coinductive bisimilar :: "'a list set \<Rightarrow> 'a list set \<Rightarrow> bool" where

    31 "([] \<in> K \<longleftrightarrow> [] \<in> L) 

    32  \<Longrightarrow> (\<And>x. bisimilar (deriv x K) (deriv x L))

    33  \<Longrightarrow> bisimilar K L"

    34 

    35 

    36 subsection{* @{term "op @@"} *}

    37 

    38 lemma concI[simp,intro]: "u : A \<Longrightarrow> v : B \<Longrightarrow> u@v : A @@ B"

    39 by (auto simp add: conc_def)

    40 

    41 lemma concE[elim]: 

    42 assumes "w \<in> A @@ B"

    43 obtains u v where "u \<in> A" "v \<in> B" "w = u@v"

    44 using assms by (auto simp: conc_def)

    45 

    46 lemma conc_mono: "A \<subseteq> C \<Longrightarrow> B \<subseteq> D \<Longrightarrow> A @@ B \<subseteq> C @@ D"

    47 by (auto simp: conc_def) 

    48 

    49 lemma conc_empty[simp]: shows "{} @@ A = {}" and "A @@ {} = {}"

    50 by auto

    51 

    52 lemma conc_epsilon[simp]: shows "{[]} @@ A = A" and "A @@ {[]} = A"

    53 by (simp_all add:conc_def)

    54 

    55 lemma conc_assoc: "(A @@ B) @@ C = A @@ (B @@ C)"

    56 by (auto elim!: concE) (simp only: append_assoc[symmetric] concI)

    57 

    58 lemma conc_Un_distrib:

    59 shows "A @@ (B \<union> C) = A @@ B \<union> A @@ C"

    60 and   "(A \<union> B) @@ C = A @@ C \<union> B @@ C"

    61 by auto

    62 

    63 lemma conc_UNION_distrib:

    64 shows "A @@ UNION I M = UNION I (%i. A @@ M i)"

    65 and   "UNION I M @@ A = UNION I (%i. M i @@ A)"

    66 by auto

    67 

    68 

    69 subsection{* @{term "A ^^ n"} *}

    70 

    71 lemma lang_pow_add: "A ^^ (n + m) = A ^^ n @@ A ^^ m"

    72 by (induct n) (auto simp: conc_assoc)

    73 

    74 lemma lang_pow_empty: "{} ^^ n = (if n = 0 then {[]} else {})"

    75 by (induct n) auto

    76 

    77 lemma lang_pow_empty_Suc[simp]: "({}::'a lang) ^^ Suc n = {}"

    78 by (simp add: lang_pow_empty)

    79 

    80 

    81 lemma length_lang_pow_ub:

    82   "ALL w : A. length w \<le> k \<Longrightarrow> w : A^^n \<Longrightarrow> length w \<le> k*n"

    83 by(induct n arbitrary: w) (fastsimp simp: conc_def)+

    84 

    85 lemma length_lang_pow_lb:

    86   "ALL w : A. length w \<ge> k \<Longrightarrow> w : A^^n \<Longrightarrow> length w \<ge> k*n"

    87 by(induct n arbitrary: w) (fastsimp simp: conc_def)+

    88 

    89 

    90 subsection{* @{const star} *}

    91 

    92 lemma star_if_lang_pow[simp]: "w : A ^^ n \<Longrightarrow> w : star A"

    93 by (auto simp: star_def)

    94 

    95 lemma Nil_in_star[iff]: "[] : star A"

    96 proof (rule star_if_lang_pow)

    97   show "[] : A ^^ 0" by simp

    98 qed

    99 

   100 lemma star_if_lang[simp]: assumes "w : A" shows "w : star A"

   101 proof (rule star_if_lang_pow)

   102   show "w : A ^^ 1" using `w : A` by simp

   103 qed

   104 

   105 lemma append_in_starI[simp]:

   106 assumes "u : star A" and "v : star A" shows "u@v : star A"

   107 proof -

   108   from `u : star A` obtain m where "u : A ^^ m" by (auto simp: star_def)

   109   moreover

   110   from `v : star A` obtain n where "v : A ^^ n" by (auto simp: star_def)

   111   ultimately have "u@v : A ^^ (m+n)" by (simp add: lang_pow_add)

   112   thus ?thesis by simp

   113 qed

   114 

   115 lemma conc_star_star: "star A @@ star A = star A"

   116 by (auto simp: conc_def)

   117 

   118 lemma star_induct[consumes 1, case_names Nil append, induct set: star]:

   119 assumes "w : star A"

   120   and "P []"

   121   and step: "!!u v. u : A \<Longrightarrow> v : star A \<Longrightarrow> P v \<Longrightarrow> P (u@v)"

   122 shows "P w"

   123 proof -

   124   { fix n have "w : A ^^ n \<Longrightarrow> P w"

   125     by (induct n arbitrary: w) (auto intro: `P []` step star_if_lang_pow) }

   126   with `w : star A` show "P w" by (auto simp: star_def)

   127 qed

   128 

   129 lemma star_empty[simp]: "star {} = {[]}"

   130 by (auto elim: star_induct)

   131 

   132 lemma star_epsilon[simp]: "star {[]} = {[]}"

   133 by (auto elim: star_induct)

   134 

   135 lemma star_idemp[simp]: "star (star A) = star A"

   136 by (auto elim: star_induct)

   137 

   138 lemma star_unfold_left: "star A = A @@ star A \<union> {[]}" (is "?L = ?R")

   139 proof

   140   show "?L \<subseteq> ?R" by (rule, erule star_induct) auto

   141 qed auto

   142 

   143 lemma concat_in_star: "set ws \<subseteq> A \<Longrightarrow> concat ws : star A"

   144 by (induct ws) simp_all

   145 

   146 lemma in_star_iff_concat:

   147   "w : star A = (EX ws. set ws \<subseteq> A & w = concat ws)"

   148   (is "_ = (EX ws. ?R w ws)")

   149 proof

   150   assume "w : star A" thus "EX ws. ?R w ws"

   151   proof induct

   152     case Nil have "?R [] []" by simp

   153     thus ?case ..

   154   next

   155     case (append u v)

   156     moreover

   157     then obtain ws where "set ws \<subseteq> A \<and> v = concat ws" by blast

   158     ultimately have "?R (u@v) (u#ws)" by auto

   159     thus ?case ..

   160   qed

   161 next

   162   assume "EX us. ?R w us" thus "w : star A"

   163   by (auto simp: concat_in_star)

   164 qed

   165 

   166 lemma star_conv_concat: "star A = {concat ws|ws. set ws \<subseteq> A}"

   167 by (fastsimp simp: in_star_iff_concat)

   168 

   169 lemma star_insert_eps[simp]: "star (insert [] A) = star(A)"

   170 proof-

   171   { fix us

   172     have "set us \<subseteq> insert [] A \<Longrightarrow> EX vs. concat us = concat vs \<and> set vs \<subseteq> A"

   173       (is "?P \<Longrightarrow> EX vs. ?Q vs")

   174     proof

   175       let ?vs = "filter (%u. u \<noteq> []) us"

   176       show "?P \<Longrightarrow> ?Q ?vs" by (induct us) auto

   177     qed

   178   } thus ?thesis by (auto simp: star_conv_concat)

   179 qed

   180 

   181 lemma Arden:

   182 assumes "[] \<notin> A" and "X = A @@ X \<union> B"

   183 shows "X = star A @@ B"

   184 proof -

   185   { fix n have "X = A^^(n+1)@@X \<union> (\<Union>i\<le>n. A^^i@@B)"

   186     proof(induct n)

   187       case 0 show ?case using `X = A @@ X \<union> B` by simp

   188     next

   189       case (Suc n)

   190       have "X = A@@X Un B" by(rule assms(2))

   191       also have "\<dots> = A@@(A^^(n+1)@@X \<union> (\<Union>i\<le>n. A^^i@@B)) Un B"

   192         by(subst Suc)(rule refl)

   193       also have "\<dots> =  A^^(n+2)@@X \<union> (\<Union>i\<le>n. A^^(i+1)@@B) Un B"

   194         by(simp add:conc_UNION_distrib conc_assoc conc_Un_distrib)

   195       also have "\<dots> =  A^^(n+2)@@X \<union> (UN i : {1..n+1}. A^^i@@B) \<union> B"

   196         by(subst UN_le_add_shift)(rule refl)

   197       also have "\<dots> =  A^^(n+2)@@X \<union> (UN i : {1..n+1}. A^^i@@B) \<union> A^^0@@B"

   198         by(simp)

   199       also have "\<dots> =  A^^(n+2)@@X \<union> (\<Union>i\<le>n+1. A^^i@@B)"

   200         by(auto simp: UN_le_eq_Un0)

   201       finally show ?case by simp

   202     qed

   203   } note 1 = this

   204   { fix w assume "w : X"

   205     let ?n = "size w"

   206     from `[] \<notin> A` have "ALL u : A. length u \<ge> 1"

   207       by (metis Suc_eq_plus1 add_leD2 le_0_eq length_0_conv not_less_eq_eq)

   208     hence "ALL u : A^^(?n+1). length u \<ge> ?n+1"

   209       by (metis length_lang_pow_lb nat_mult_1)

   210     hence "ALL u : A^^(?n+1)@@X. length u \<ge> ?n+1"

   211       by(auto simp only: conc_def length_append)

   212     hence "w \<notin> A^^(?n+1)@@X" by auto

   213     hence "w : star A @@ B" using `w : X` 1[of ?n]

   214       by(auto simp add: star_def conc_UNION_distrib)

   215   } moreover

   216   { fix w assume "w : star A @@ B"

   217     hence "EX n. w : A^^n @@ B" by(auto simp: conc_def star_def)

   218     hence "w : X" using 1 by blast

   219   } ultimately show ?thesis by blast

   220 qed

   221 

   222 subsection{* @{const deriv} *}

   223 

   224 lemma deriv_empty[simp]: "deriv a {} = {}"

   225 and deriv_epsilon[simp]: "deriv a {[]} = {}"

   226 and deriv_char[simp]: "deriv a {[b]} = (if a = b then {[]} else {})"

   227 and deriv_union[simp]: "deriv a (A \<union> B) = deriv a A \<union> deriv a B"

   228 by (auto simp: deriv_def)

   229 

   230 lemma deriv_conc_subset:

   231 "deriv a A @@ B \<subseteq> deriv a (A @@ B)" (is "?L \<subseteq> ?R")

   232 proof 

   233   fix w assume "w \<in> ?L"

   234   then obtain u v where "w = u @ v" "a # u \<in> A" "v \<in> B"

   235     by (auto simp: deriv_def)

   236   then have "a # w \<in> A @@ B"

   237     by (auto intro: concI[of "a # u", simplified])

   238   thus "w \<in> ?R" by (auto simp: deriv_def)

   239 qed

   240 

   241 lemma deriv_conc1:

   242 assumes "[] \<notin> A"

   243 shows "deriv a (A @@ B) = deriv a A @@ B" (is "?L = ?R")

   244 proof

   245   show "?L \<subseteq> ?R"

   246   proof

   247     fix w assume "w \<in> ?L"

   248     then have "a # w \<in> A @@ B" by (simp add: deriv_def)

   249     then obtain x y 

   250       where aw: "a # w = x @ y" "x \<in> A" "y \<in> B" by auto

   251     with `[] \<notin> A` obtain x' where "x = a # x'"

   252       by (cases x) auto

   253     with aw have "w = x' @ y" "x' \<in> deriv a A"

   254       by (auto simp: deriv_def)

   255     with `y \<in> B` show "w \<in> ?R" by simp

   256   qed

   257   show "?R \<subseteq> ?L" by (fact deriv_conc_subset)

   258 qed

   259 

   260 lemma deriv_conc2:

   261 assumes "[] \<in> A"

   262 shows "deriv a (A @@ B) = deriv a A @@ B \<union> deriv a B"

   263 (is "?L = ?R")

   264 proof

   265   show "?L \<subseteq> ?R"

   266   proof

   267     fix w assume "w \<in> ?L"

   268     then have "a # w \<in> A @@ B" by (simp add: deriv_def)

   269     then obtain x y 

   270       where aw: "a # w = x @ y" "x \<in> A" "y \<in> B" by auto

   271     show "w \<in> ?R"

   272     proof (cases x)

   273       case Nil

   274       with aw have "w \<in> deriv a B" by (auto simp: deriv_def)

   275       thus ?thesis ..

   276     next

   277       case (Cons b x')

   278       with aw have "w = x' @ y" "x' \<in> deriv a A"

   279         by (auto simp: deriv_def)

   280       with `y \<in> B` show "w \<in> ?R" by simp

   281     qed

   282   qed

   283 

   284   from concI[OF `[] \<in> A`, simplified]

   285   have "B \<subseteq> A @@ B" ..

   286   then have "deriv a B \<subseteq> deriv a (A @@ B)" by (auto simp: deriv_def)

   287   with deriv_conc_subset[of a A B]

   288   show "?R \<subseteq> ?L" by auto

   289 qed

   290 

   291 lemma wlog_no_eps: 

   292 assumes PB: "\<And>B. [] \<notin> B \<Longrightarrow> P B"

   293 assumes preserved: "\<And>A. P A \<Longrightarrow> P (insert [] A)"

   294 shows "P A"

   295 proof -

   296   let ?B = "A - {[]}"

   297   have "P ?B" by (rule PB) auto

   298   thus "P A"

   299   proof cases

   300     assume "[] \<in> A"

   301     then have "(insert [] ?B) = A" by auto

   302     with preserved[OF `P ?B`]

   303     show ?thesis by simp

   304   qed auto

   305 qed

   306 

   307 lemma deriv_insert_eps[simp]: 

   308 "deriv a (insert [] A) = deriv a A"

   309 by (auto simp: deriv_def)

   310 

   311 lemma deriv_star[simp]: "deriv a (star A) = deriv a A @@ star A"

   312 proof (induct A rule: wlog_no_eps)

   313   fix B :: "'a list set" assume "[] \<notin> B"

   314   thus "deriv a (star B) = deriv a B @@ star B" 

   315     by (subst star_unfold_left) (simp add: deriv_conc1)

   316 qed auto

   317 

   318 

   319 subsection{* @{const bisimilar} *}

   320 

   321 lemma equal_if_bisimilar:

   322 assumes "bisimilar K L" shows "K = L"

   323 proof (rule set_eqI)

   324   fix w

   325   from `bisimilar K L` show "w \<in> K \<longleftrightarrow> w \<in> L"

   326   proof (induct w arbitrary: K L)

   327     case Nil thus ?case by (auto elim: bisimilar.cases)

   328   next

   329     case (Cons a w K L)

   330     from `bisimilar K L` have "bisimilar (deriv a K) (deriv a L)"

   331       by (auto elim: bisimilar.cases)

   332     then have "w \<in> deriv a K \<longleftrightarrow> w \<in> deriv a L" by (rule Cons(1))

   333     thus ?case by (auto simp: deriv_def)

   334   qed

   335 qed

   336 

   337 lemma language_coinduct:

   338 fixes R (infixl "\<sim>" 50)

   339 assumes "K \<sim> L"

   340 assumes "\<And>K L. K \<sim> L \<Longrightarrow> ([] \<in> K \<longleftrightarrow> [] \<in> L)"

   341 assumes "\<And>K L x. K \<sim> L \<Longrightarrow> deriv x K \<sim> deriv x L"

   342 shows "K = L"

   343 apply (rule equal_if_bisimilar)

   344 apply (rule bisimilar.coinduct[of R, OF `K \<sim> L`])

   345 apply (auto simp: assms)

   346 done

   347 

   348 end