1 theory Derivatives

     2 imports Myhill_2

     3 begin

     4 

     5 section {* Left-Quotients and Derivatives *}

     6 

     7 subsection {* Left-Quotients *}

     8 

     9 definition

    10   Delta :: "'a lang \<Rightarrow> 'a lang"

    11 where

    12   "Delta A = (if [] \<in> A then {[]} else {})"

    13 

    14 definition

    15   Der :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"

    16 where

    17   "Der c A \<equiv> {s. [c] @ s \<in> A}"

    18 

    19 definition

    20   Ders :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang"

    21 where

    22   "Ders s A \<equiv> {s'. s @ s' \<in> A}"

    23 

    24 definition

    25   Ders_set :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a lang"

    26 where

    27   "Ders_set A B \<equiv> {s' | s s'. s @ s' \<in> B \<and> s \<in> A}"

    28 

    29 lemma Ders_set_Ders:

    30   shows "Ders_set A B = (\<Union>s \<in> A. Ders s B)"

    31 unfolding Ders_set_def Ders_def

    32 by auto

    33 

    34 lemma Der_zero [simp]:

    35   shows "Der c {} = {}"

    36 unfolding Der_def

    37 by auto

    38 

    39 lemma Der_one [simp]:

    40   shows "Der c {[]} = {}"

    41 unfolding Der_def

    42 by auto

    43 

    44 lemma Der_atom [simp]:

    45   shows "Der c {[d]} = (if c = d then {[]} else {})"

    46 unfolding Der_def

    47 by auto

    48 

    49 lemma Der_union [simp]:

    50   shows "Der c (A \<union> B) = Der c A \<union> Der c B"

    51 unfolding Der_def

    52 by auto

    53 

    54 lemma Der_conc [simp]:

    55   shows "Der c (A \<cdot> B) = (Der c A) \<cdot> B \<union> (Delta A \<cdot> Der c B)"

    56 unfolding Der_def Delta_def conc_def

    57 by (auto simp add: Cons_eq_append_conv)

    58 

    59 lemma Der_star [simp]:

    60   shows "Der c (A\<star>) = (Der c A) \<cdot> A\<star>"

    61 proof -

    62   have incl: "Delta A \<cdot> Der c (A\<star>) \<subseteq> (Der c A) \<cdot> A\<star>"

    63     unfolding Der_def Delta_def 

    64     apply(auto)

    65     apply(drule star_decom)

    66     apply(auto simp add: Cons_eq_append_conv)

    67     done

    68     

    69   have "Der c (A\<star>) = Der c ({[]} \<union> A \<cdot> A\<star>)"

    70     by (simp only: star_cases[symmetric])

    71   also have "... = Der c (A \<cdot> A\<star>)"

    72     by (simp only: Der_union Der_one) (simp)

    73   also have "... = (Der c A) \<cdot> A\<star> \<union> (Delta A \<cdot> Der c (A\<star>))"

    74     by simp

    75   also have "... =  (Der c A) \<cdot> A\<star>"

    76     using incl by auto

    77   finally show "Der c (A\<star>) = (Der c A) \<cdot> A\<star>" . 

    78 qed

    79 

    80 

    81 lemma Ders_singleton:

    82   shows "Ders [c] A = Der c A"

    83 unfolding Der_def Ders_def

    84 by simp

    85 

    86 lemma Ders_append:

    87   shows "Ders (s1 @ s2) A = Ders s2 (Ders s1 A)"

    88 unfolding Ders_def by simp 

    89 

    90 

    91 text {* Relating the Myhill-Nerode relation with left-quotients. *}

    92 

    93 lemma MN_Rel_Ders:

    94   shows "x \<approx>A y \<longleftrightarrow> Ders x A = Ders y A"

    95 unfolding Ders_def str_eq_def str_eq_rel_def

    96 by auto

    97 

    98 

    99 subsection {* Brozowsky's derivatives of regular expressions *}

   100 

   101 fun

   102   nullable :: "'a rexp \<Rightarrow> bool"

   103 where

   104   "nullable (Zero) = False"

   105 | "nullable (One) = True"

   106 | "nullable (Atom c) = False"

   107 | "nullable (Plus r1 r2) = (nullable r1 \<or> nullable r2)"

   108 | "nullable (Times r1 r2) = (nullable r1 \<and> nullable r2)"

   109 | "nullable (Star r) = True"

   110 

   111 fun

   112   der :: "'a \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"

   113 where

   114   "der c (Zero) = Zero"

   115 | "der c (One) = Zero"

   116 | "der c (Atom c') = (if c = c' then One else Zero)"

   117 | "der c (Plus r1 r2) = Plus (der c r1) (der c r2)"

   118 | "der c (Times r1 r2) = Plus (Times (der c r1) r2) (if nullable r1 then der c r2 else Zero)"

   119 | "der c (Star r) = Times (der c r) (Star r)"

   120 

   121 function 

   122   ders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"

   123 where

   124   "ders [] r = r"

   125 | "ders (s @ [c]) r = der c (ders s r)"

   126 by (auto) (metis rev_cases)

   127 

   128 termination

   129   by (relation "measure (length o fst)") (auto)

   130 

   131 lemma Delta_nullable:

   132   shows "Delta (lang r) = (if nullable r then {[]} else {})"

   133 unfolding Delta_def

   134 by (induct r) (auto simp add: conc_def split: if_splits)

   135 

   136 lemma Der_der:

   137   shows "Der c (lang r) = lang (der c r)"

   138 by (induct r) (simp_all add: Delta_nullable)

   139 

   140 lemma Ders_ders:

   141   shows "Ders s (lang r) = lang (ders s r)"

   142 apply(induct s rule: rev_induct)

   143 apply(simp add: Ders_def)

   144 apply(simp only: ders.simps)

   145 apply(simp only: Ders_append)

   146 apply(simp only: Ders_singleton)

   147 apply(simp only: Der_der)

   148 done

   149 

   150 

   151 subsection {* Antimirov's Partial Derivatives *}

   152 

   153 abbreviation

   154   "Times_set rs r \<equiv> {Times r' r | r'. r' \<in> rs}"

   155 

   156 fun

   157   pder :: "'a \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"

   158 where

   159   "pder c Zero = {Zero}"

   160 | "pder c One = {Zero}"

   161 | "pder c (Atom c') = (if c = c' then {One} else {Zero})"

   162 | "pder c (Plus r1 r2) = (pder c r1) \<union> (pder c r2)"

   163 | "pder c (Times r1 r2) = Times_set (pder c r1) r2 \<union> (if nullable r1 then pder c r2 else {})"

   164 | "pder c (Star r) = Times_set (pder c r) (Star r)"

   165 

   166 abbreviation

   167   "pder_set c rs \<equiv> \<Union>r \<in> rs. pder c r"

   168 

   169 function 

   170   pders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"

   171 where

   172   "pders [] r = {r}"

   173 | "pders (s @ [c]) r = pder_set c (pders s r)"

   174 by (auto) (metis rev_cases)

   175 

   176 termination

   177   by (relation "measure (length o fst)") (auto)

   178 

   179 abbreviation

   180   "pders_set A r \<equiv> \<Union>s \<in> A. pders s r"

   181 

   182 lemma pders_append:

   183   "pders (s1 @ s2) r = \<Union> (pders s2) ` (pders s1 r)"

   184 apply(induct s2 arbitrary: s1 r rule: rev_induct)

   185 apply(simp)

   186 apply(subst append_assoc[symmetric])

   187 apply(simp only: pders.simps)

   188 apply(auto)

   189 done

   190 

   191 lemma pders_singleton:

   192   "pders [c] r = pder c r"

   193 apply(subst append_Nil[symmetric])

   194 apply(simp only: pders.simps)

   195 apply(simp)

   196 done

   197 

   198 lemma pders_set_lang:

   199   shows "(\<Union> (lang ` pder_set c rs)) = (\<Union>r \<in> rs. (\<Union>lang ` (pder c r)))"

   200 unfolding image_def 

   201 by auto

   202 

   203 lemma pders_Zero [simp]:

   204   shows "pders s Zero = {Zero}"

   205 by (induct s rule: rev_induct) (simp_all)

   206 

   207 lemma pders_One [simp]:

   208   shows "pders s One = (if s = [] then {One} else {Zero})"

   209 by (induct s rule: rev_induct) (auto)

   210 

   211 lemma pders_Atom [simp]:

   212   shows "pders s (Atom c) = (if s = [] then {Atom c} else (if s = [c] then {One} else {Zero}))"

   213 by (induct s rule: rev_induct) (auto)

   214 

   215 lemma pders_Plus [simp]:

   216   shows "pders s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pders s r1) \<union> (pders s r2))"

   217 by (induct s rule: rev_induct) (auto)

   218 

   219 text {* Non-empty suffixes of a string *}

   220 

   221 definition

   222   "Suf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}"

   223 

   224 lemma Suf:

   225   shows "Suf (s @ [c]) = (Suf s) \<cdot> {[c]} \<union> {[c]}"

   226 unfolding Suf_def conc_def

   227 by (auto simp add: append_eq_append_conv2 append_eq_Cons_conv)

   228 

   229 lemma Suf_Union:

   230   shows "(\<Union>v \<in> Suf s \<cdot> {[c]}. P v) = (\<Union>v \<in> Suf s. P (v @ [c]))"

   231 by (auto simp add: conc_def)

   232 

   233 lemma pders_Times:

   234   shows "pders s (Times r1 r2) \<subseteq> Times_set (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2)"

   235 proof (induct s rule: rev_induct)

   236   case (snoc c s)

   237   have ih: "pders s (Times r1 r2) \<subseteq> Times_set (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2)" 

   238     by fact

   239   have "pders (s @ [c]) (Times r1 r2) = pder_set c (pders s (Times r1 r2))" by simp

   240   also have "\<dots> \<subseteq> pder_set c (Times_set (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2))"

   241     using ih by (auto) (blast)

   242   also have "\<dots> = pder_set c (Times_set (pders s r1) r2) \<union> pder_set c (\<Union>v \<in> Suf s. pders v r2)"

   243     by (simp)

   244   also have "\<dots> = pder_set c (Times_set (pders s r1) r2) \<union> (\<Union>v \<in> Suf s. pder_set c (pders v r2))"

   245     by (simp)

   246   also have "\<dots> \<subseteq> pder_set c (Times_set (pders s r1) r2) \<union> (pder c r2) \<union> (\<Union>v \<in> Suf s. pders (v @ [c]) r2)"

   247     by (auto)

   248   also have "\<dots> \<subseteq> Times_set (pder_set c (pders s r1)) r2 \<union> (pder c r2) \<union> (\<Union>v \<in> Suf s. pders (v @ [c]) r2)"

   249     by (auto simp add: if_splits) (blast)

   250   also have "\<dots> = Times_set (pders (s @ [c]) r1) r2 \<union> (\<Union>v \<in> Suf (s @ [c]). pders v r2)"

   251     apply(subst (2) pders.simps)

   252     apply(simp only: Suf)

   253     apply(simp add: Suf_Union pders_singleton)

   254     apply(auto)

   255     done

   256   finally show ?case .

   257 qed (simp)

   258 

   259 lemma pders_Star:

   260   assumes a: "s \<noteq> []"

   261   shows "pders s (Star r) \<subseteq> (\<Union>v \<in> Suf s. Times_set (pders v r) (Star r))"

   262 using a

   263 proof (induct s rule: rev_induct)

   264   case (snoc c s)

   265   have ih: "s \<noteq> [] \<Longrightarrow> pders s (Star r) \<subseteq> (\<Union>v\<in>Suf s. Times_set (pders v r) (Star r))" by fact

   266   { assume asm: "s \<noteq> []"

   267     have "pders (s @ [c]) (Star r) = pder_set c (pders s (Star r))" by simp

   268     also have "\<dots> \<subseteq> (pder_set c (\<Union>v\<in>Suf s. Times_set (pders v r) (Star r)))"

   269       using ih[OF asm] by blast

   270     also have "\<dots> = (\<Union>v\<in>Suf s. pder_set c (Times_set (pders v r) (Star r)))"

   271       by simp

   272     also have "\<dots> \<subseteq> (\<Union>v\<in>Suf s. (Times_set (pder_set c (pders v r)) (Star r) \<union> pder c (Star r)))"

   273       by (auto split: if_splits) 

   274     also have "\<dots> = (\<Union>v\<in>Suf s. (Times_set (pder_set c (pders v r)) (Star r))) \<union> pder c (Star r)"

   275       using asm by (auto simp add: Suf_def)

   276     also have "\<dots> = (\<Union>v\<in>Suf s. (Times_set (pders (v @ [c]) r) (Star r))) \<union> (Times_set (pder c r) (Star r))"

   277       by simp

   278     also have "\<dots> = (\<Union>v\<in>Suf (s @ [c]). (Times_set (pders v r) (Star r)))"

   279       apply(simp only: Suf)

   280       apply(simp add: Suf_Union pders_singleton)

   281       apply(auto)

   282       done

   283     finally have ?case .

   284   }

   285   moreover

   286   { assume asm: "s = []"

   287     then have ?case

   288       apply(simp add: pders_singleton Suf_def)

   289       apply(auto)

   290       apply(rule_tac x="[c]" in exI)

   291       apply(simp add: pders_singleton)

   292       done

   293   }

   294   ultimately show ?case by blast

   295 qed (simp)

   296 

   297 abbreviation 

   298   "UNIV1 \<equiv> UNIV - {[]}"

   299 

   300 lemma pders_set_Zero:

   301   shows "pders_set UNIV1 Zero = {Zero}"

   302 by auto

   303 

   304 lemma pders_set_One:

   305   shows "pders_set UNIV1 One = {Zero}"

   306 by (auto split: if_splits)

   307 

   308 lemma pders_set_Atom:

   309   shows "pders_set UNIV1 (Atom c) \<subseteq> {One, Zero}"

   310 by (auto split: if_splits)

   311 

   312 lemma pders_set_Plus:

   313   shows "pders_set UNIV1 (Plus r1 r2) = pders_set UNIV1 r1 \<union> pders_set UNIV1 r2"

   314 by auto

   315 

   316 lemma pders_set_Times_aux:

   317   assumes a: "s \<in> UNIV1"

   318   shows "pders_set (Suf s) r2 \<subseteq> pders_set UNIV1 r2"

   319 using a by (auto simp add: Suf_def)

   320 

   321 lemma pders_set_Times:

   322   shows "pders_set UNIV1 (Times r1 r2) \<subseteq> Times_set (pders_set UNIV1 r1) r2 \<union> pders_set UNIV1 r2"

   323 apply(rule UN_least)

   324 apply(rule subset_trans)

   325 apply(rule pders_Times)

   326 apply(simp)

   327 apply(rule conjI) 

   328 apply(auto)[1]

   329 apply(rule subset_trans)

   330 apply(rule pders_set_Times_aux)

   331 apply(auto)

   332 done

   333 

   334 lemma pders_set_Star:

   335   shows "pders_set UNIV1 (Star r) \<subseteq> Times_set (pders_set UNIV1 r) (Star r)"

   336 apply(rule UN_least)

   337 apply(rule subset_trans)

   338 apply(rule pders_Star)

   339 apply(simp)

   340 apply(simp add: Suf_def)

   341 apply(auto)

   342 done

   343 

   344 lemma finite_Times_set:

   345   assumes a: "finite A"

   346   shows "finite (Times_set A r)"

   347 using a by (auto)

   348 

   349 lemma finite_pders_set_UNIV1:

   350   shows "finite (pders_set UNIV1 r)"

   351 apply(induct r)

   352 apply(simp)

   353 apply(simp only: pders_set_One)

   354 apply(simp)

   355 apply(rule finite_subset)

   356 apply(rule pders_set_Atom)

   357 apply(simp)

   358 apply(simp only: pders_set_Plus)

   359 apply(simp)

   360 apply(rule finite_subset)

   361 apply(rule pders_set_Times)

   362 apply(simp only: finite_Times_set finite_Un)

   363 apply(simp)

   364 apply(rule finite_subset)

   365 apply(rule pders_set_Star)

   366 apply(simp only: finite_Times_set)

   367 done

   368     

   369 lemma pders_set_UNIV_UNIV1:

   370   shows "pders_set UNIV r = pders [] r \<union> pders_set UNIV1 r"

   371 apply(auto)

   372 apply(rule_tac x="[]" in exI)

   373 apply(simp)

   374 done

   375 

   376 lemma finite_pders_set_UNIV:

   377   shows "finite (pders_set UNIV r)"

   378 unfolding pders_set_UNIV_UNIV1

   379 by (simp add: finite_pders_set_UNIV1)

   380 

   381 lemma finite_pders_set:

   382   shows "finite (pders_set A r)"

   383 apply(rule rev_finite_subset)

   384 apply(rule_tac r="r" in finite_pders_set_UNIV)

   385 apply(auto)

   386 done

   387 

   388 lemma finite_pders:

   389   shows "finite (pders s r)"

   390 using finite_pders_set[where A="{s}" and r="r"]

   391 by simp

   392 

   393 lemma finite_pders2:

   394   shows "finite {pders s r | s. s \<in> A}"

   395 proof -

   396   have "{pders s r | s. s \<in> A} \<subseteq> Pow (pders_set A r)" by auto

   397   moreover

   398   have "finite (Pow (pders_set A r))"

   399     using finite_pders_set by simp

   400   ultimately 

   401   show "finite {pders s r | s. s \<in> A}"

   402     by(rule finite_subset)

   403 qed

   404 

   405 

   406 subsection {* Relating left-quotients and partial derivatives *}

   407 

   408 lemma Der_pder:

   409   shows "Der c (lang r) = \<Union> lang ` (pder c r)"

   410 by (induct r) (auto simp add: Delta_nullable conc_UNION_distrib)

   411 

   412 lemma Ders_pders:

   413   shows "Ders s (lang r) = \<Union> lang ` (pders s r)"

   414 proof (induct s rule: rev_induct)

   415   case (snoc c s)

   416   have ih: "Ders s (lang r) = \<Union> lang ` (pders s r)" by fact

   417   have "Ders (s @ [c]) (lang r) = Ders [c] (Ders s (lang r))"

   418     by (simp add: Ders_append)

   419   also have "\<dots> = Der c (\<Union> lang ` (pders s r))" using ih

   420     by (simp add: Ders_singleton)

   421   also have "\<dots> = (\<Union>r\<in>pders s r. Der c (lang r))" 

   422     unfolding Der_def image_def by auto

   423   also have "\<dots> = (\<Union>r\<in>pders s r. (\<Union> lang `  (pder c r)))"

   424     by (simp add: Der_pder)

   425   also have "\<dots> = (\<Union>lang ` (pder_set c (pders s r)))"

   426     by (simp add: pders_set_lang)

   427   also have "\<dots> = (\<Union>lang ` (pders (s @ [c]) r))"

   428     by simp

   429   finally show "Ders (s @ [c]) (lang r) = \<Union> lang ` pders (s @ [c]) r" .

   430 qed (simp add: Ders_def)

   431 

   432 lemma Ders_set_pders_set:

   433   shows "Ders_set A (lang r) = (\<Union> lang ` (pders_set A r))"

   434 by (simp add: Ders_set_Ders Ders_pders)

   435 

   436 

   437 subsection {* Relating derivatives and partial derivatives *}

   438 

   439 lemma

   440   shows "(\<Union> lang ` (pder c r)) = lang (der c r)"

   441 unfolding Der_der[symmetric] Der_pder by simp

   442 

   443 lemma

   444   shows "(\<Union> lang ` (pders s r)) = lang (ders s r)"

   445 unfolding Ders_ders[symmetric] Ders_pders by simp

   446 

   447 

   448 

   449 subsection {*

   450   The second direction of the Myhill-Nerode theorem using

   451   partial derivatives.

   452 *}

   453 

   454 lemma Myhill_Nerode3:

   455   fixes r::"'a rexp"

   456   shows "finite (UNIV // \<approx>(lang r))"

   457 proof -

   458   have "finite (UNIV // =(\<lambda>x. pders x r)=)"

   459   proof - 

   460     have "range (\<lambda>x. pders x r) = {pders s r | s. s \<in> UNIV}" by auto

   461     moreover 

   462     have "finite {pders s r | s. s \<in> UNIV}" by (rule finite_pders2)

   463     ultimately

   464     have "finite (range (\<lambda>x. pders x r))"

   465       by simp

   466     then show "finite (UNIV // =(\<lambda>x. pders x r)=)" 

   467       by (rule finite_eq_tag_rel)

   468   qed

   469   moreover 

   470   have "=(\<lambda>x. pders x r)= \<subseteq> \<approx>(lang r)"

   471     unfolding tag_eq_rel_def

   472     unfolding str_eq_def2

   473     unfolding MN_Rel_Ders

   474     unfolding Ders_pders

   475     by auto

   476   moreover 

   477   have "equiv UNIV =(\<lambda>x. pders x r)="

   478     unfolding equiv_def refl_on_def sym_def trans_def

   479     unfolding tag_eq_rel_def

   480     by auto

   481   moreover

   482   have "equiv UNIV (\<approx>(lang r))"

   483     unfolding equiv_def refl_on_def sym_def trans_def

   484     unfolding str_eq_rel_def

   485     by auto

   486   ultimately show "finite (UNIV // \<approx>(lang r))" 

   487     by (rule refined_partition_finite)

   488 qed

   489 

   490 end