1 theory Derivs

     2 imports Myhill_2

     3 begin

     4 

     5 section {* Left-Quotients and Derivatives *}

     6 

     7 subsection {* Left-Quotients *}

     8 

     9 definition

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

    11 where

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

    13 

    14 definition

    15   Der :: "char \<Rightarrow> lang \<Rightarrow> lang"

    16 where

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

    18 

    19 definition

    20   Ders :: "string \<Rightarrow> lang \<Rightarrow> lang"

    21 where

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

    23 

    24 definition

    25   Ders_set :: "lang \<Rightarrow> lang \<Rightarrow> 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_null [simp]:

    35   shows "Der c {} = {}"

    36 unfolding Der_def

    37 by auto

    38 

    39 lemma Der_empty [simp]:

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

    41 unfolding Der_def

    42 by auto

    43 

    44 lemma Der_char [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_seq [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

    57 unfolding Seq_def

    58 by (auto simp add: Cons_eq_append_conv)

    59 

    60 lemma Der_star [simp]:

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

    62 proof -

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

    64     unfolding Der_def Delta_def Seq_def

    65     apply(auto)

    66     apply(drule star_decom)

    67     apply(auto simp add: Cons_eq_append_conv)

    68     done

    69     

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

    71     by (simp only: star_cases[symmetric])

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

    73     by (simp only: Der_union Der_empty) (simp)

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

    75     by simp

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

    77     using incl by auto

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

    79 qed

    80 

    81 

    82 lemma Ders_singleton:

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

    84 unfolding Der_def Ders_def

    85 by simp

    86 

    87 lemma Ders_append:

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

    89 unfolding Ders_def by simp 

    90 

    91 lemma MN_Rel_Ders:

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

    93 unfolding Ders_def str_eq_def str_eq_rel_def

    94 by auto

    95 

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

    97 

    98 fun

    99   nullable :: "rexp \<Rightarrow> bool"

   100 where

   101   "nullable (NULL) = False"

   102 | "nullable (EMPTY) = True"

   103 | "nullable (CHAR c) = False"

   104 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"

   105 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"

   106 | "nullable (STAR r) = True"

   107 

   108 fun

   109   der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"

   110 where

   111   "der c (NULL) = NULL"

   112 | "der c (EMPTY) = NULL"

   113 | "der c (CHAR c') = (if c = c' then EMPTY else NULL)"

   114 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"

   115 | "der c (SEQ r1 r2) = ALT (SEQ (der c r1) r2) (if nullable r1 then der c r2 else NULL)"

   116 | "der c (STAR r) = SEQ (der c r) (STAR r)"

   117 

   118 function 

   119   ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"

   120 where

   121   "ders [] r = r"

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

   123 by (auto) (metis rev_cases)

   124 

   125 termination

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

   127 

   128 lemma Delta_nullable:

   129   shows "Delta (L_rexp r) = (if nullable r then {[]} else {})"

   130 unfolding Delta_def

   131 by (induct r) (auto simp add: Seq_def split: if_splits)

   132 

   133 lemma Der_der:

   134   fixes r::rexp

   135   shows "Der c (L_rexp r) = L_rexp (der c r)"

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

   137 

   138 lemma Ders_ders:

   139   fixes r::rexp

   140   shows "Ders s (L_rexp r) = L_rexp (ders s r)"

   141 apply(induct s rule: rev_induct)

   142 apply(simp add: Ders_def)

   143 apply(simp only: ders.simps)

   144 apply(simp only: Ders_append)

   145 apply(simp only: Ders_singleton)

   146 apply(simp only: Der_der)

   147 done

   148 

   149 

   150 subsection {* Antimirov's Partial Derivatives *}

   151 

   152 abbreviation

   153   "SEQS R r \<equiv> {SEQ r' r | r'. r' \<in> R}"

   154 

   155 fun

   156   pder :: "char \<Rightarrow> rexp \<Rightarrow> rexp set"

   157 where

   158   "pder c NULL = {NULL}"

   159 | "pder c EMPTY = {NULL}"

   160 | "pder c (CHAR c') = (if c = c' then {EMPTY} else {NULL})"

   161 | "pder c (ALT r1 r2) = (pder c r1) \<union> (pder c r2)"

   162 | "pder c (SEQ r1 r2) = SEQS (pder c r1) r2 \<union> (if nullable r1 then pder c r2 else {})"

   163 | "pder c (STAR r) = SEQS (pder c r) (STAR r)"

   164 

   165 abbreviation

   166   "pder_set c R \<equiv> \<Union>r \<in> R. pder c r"

   167 

   168 function 

   169   pders :: "string \<Rightarrow> rexp \<Rightarrow> rexp set"

   170 where

   171   "pders [] r = {r}"

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

   173 by (auto) (metis rev_cases)

   174 

   175 termination

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

   177 

   178 abbreviation

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

   180 

   181 lemma pders_append:

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

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

   184 apply(simp)

   185 apply(subst append_assoc[symmetric])

   186 apply(simp only: pders.simps)

   187 apply(auto)

   188 done

   189 

   190 lemma pders_singleton:

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

   192 apply(subst append_Nil[symmetric])

   193 apply(simp only: pders.simps)

   194 apply(simp)

   195 done

   196 

   197 lemma pder_set_lang:

   198   shows "(\<Union> (L_rexp ` pder_set c R)) = (\<Union>r \<in> R. (\<Union>L_rexp ` (pder c r)))"

   199 unfolding image_def 

   200 by auto

   201 

   202 lemma

   203   shows seq_UNION_left:  "B \<cdot> (\<Union>n\<in>C. A n) = (\<Union>n\<in>C. B \<cdot> A n)"

   204   and   seq_UNION_right: "(\<Union>n\<in>C. A n) \<cdot> B = (\<Union>n\<in>C. A n \<cdot> B)"

   205 unfolding Seq_def by auto

   206 

   207 lemma Der_pder:

   208   fixes r::rexp

   209   shows "Der c (L_rexp r) = \<Union> L_rexp ` (pder c r)"

   210 by (induct r) (auto simp add: Delta_nullable seq_UNION_right)

   211 

   212 lemma Ders_pders:

   213   fixes r::rexp

   214   shows "Ders s (L_rexp r) = \<Union> L_rexp ` (pders s r)"

   215 proof (induct s rule: rev_induct)

   216   case (snoc c s)

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

   218   have "Ders (s @ [c]) (L_rexp r) = Ders [c] (Ders s (L_rexp r))"

   219     by (simp add: Ders_append)

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

   221     by (simp add: Ders_singleton)

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

   223     unfolding Der_def image_def by auto

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

   225     by (simp add: Der_pder)

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

   227     by (simp add: pder_set_lang)

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

   229     by simp

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

   231 qed (simp add: Ders_def)

   232 

   233 lemma Ders_set_pders_set:

   234   fixes r::rexp

   235   shows "Ders_set A (L_rexp r) = (\<Union> L_rexp ` (pders_set A r))"

   236 by (simp add: Ders_set_Ders Ders_pders)

   237 

   238 lemma pders_NULL [simp]:

   239   shows "pders s NULL = {NULL}"

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

   241 

   242 lemma pders_EMPTY [simp]:

   243   shows "pders s EMPTY = (if s = [] then {EMPTY} else {NULL})"

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

   245 

   246 lemma pders_CHAR [simp]:

   247   shows "pders s (CHAR c) = (if s = [] then {CHAR c} else (if s = [c] then {EMPTY} else {NULL}))"

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

   249 

   250 lemma pders_ALT [simp]:

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

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

   253 

   254 definition

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

   256 

   257 lemma Suf:

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

   259 unfolding Suf_def Seq_def

   260 by (auto simp add: append_eq_append_conv2 append_eq_Cons_conv)

   261 

   262 lemma Suf_Union:

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

   264 by (auto simp add: Seq_def)

   265 

   266 lemma inclusion1:

   267   shows "pder_set c (SEQS R r2) \<subseteq> SEQS (pder_set c R) r2 \<union> (pder c r2)"

   268 apply(auto simp add: if_splits)

   269 apply(blast)

   270 done

   271 

   272 lemma pders_SEQ:

   273   shows "pders s (SEQ r1 r2) \<subseteq> SEQS (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2)"

   274 proof (induct s rule: rev_induct)

   275   case (snoc c s)

   276   have ih: "pders s (SEQ r1 r2) \<subseteq> SEQS (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2)" 

   277     by fact

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

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

   280     using ih by (auto) (blast)

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

   282     by (simp)

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

   284     by (simp)

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

   286     by (auto)

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

   288     using inclusion1 by blast

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

   290     apply(subst (2) pders.simps)

   291     apply(simp only: Suf)

   292     apply(simp add: Suf_Union pders_singleton)

   293     apply(auto)

   294     done

   295   finally show ?case .

   296 qed (simp)

   297 

   298 lemma pders_STAR:

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

   300   shows "pders s (STAR r) \<subseteq> (\<Union>v \<in> Suf s. SEQS (pders v r) (STAR r))"

   301 using a

   302 proof (induct s rule: rev_induct)

   303   case (snoc c s)

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

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

   306     have "pders (s @ [c]) (STAR r) = pder_set c (pders s (STAR r))" by simp

   307     also have "\<dots> \<subseteq> (pder_set c (\<Union>v\<in>Suf s. SEQS (pders v r) (STAR r)))"

   308       using ih[OF asm] by blast

   309     also have "\<dots> = (\<Union>v\<in>Suf s. pder_set c (SEQS (pders v r) (STAR r)))"

   310       by simp

   311     also have "\<dots> \<subseteq> (\<Union>v\<in>Suf s. (SEQS (pder_set c (pders v r)) (STAR r) \<union> pder c (STAR r)))"

   312       using inclusion1 by (auto split: if_splits) 

   313     also have "\<dots> = (\<Union>v\<in>Suf s. (SEQS (pder_set c (pders v r)) (STAR r))) \<union> pder c (STAR r)"

   314       using asm by (auto simp add: Suf_def)

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

   316       by simp

   317     also have "\<dots> = (\<Union>v\<in>Suf (s @ [c]). (SEQS (pders v r) (STAR r)))"

   318       apply(simp only: Suf)

   319       apply(simp add: Suf_Union pders_singleton)

   320       apply(auto)

   321       done

   322     finally have ?case .

   323   }

   324   moreover

   325   { assume asm: "s = []"

   326     then have ?case

   327       apply(simp add: pders_singleton Suf_def)

   328       apply(auto)

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

   330       apply(simp add: pders_singleton)

   331       done

   332   }

   333   ultimately show ?case by blast

   334 qed (simp)

   335 

   336 abbreviation 

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

   338 

   339 lemma pders_set_NULL:

   340   shows "pders_set UNIV1 NULL = {NULL}"

   341 by auto

   342 

   343 lemma pders_set_EMPTY:

   344   shows "pders_set UNIV1 EMPTY = {NULL}"

   345 by (auto split: if_splits)

   346 

   347 lemma pders_set_CHAR:

   348   shows "pders_set UNIV1 (CHAR c) \<subseteq> {EMPTY, NULL}"

   349 by (auto split: if_splits)

   350 

   351 lemma pders_set_ALT:

   352   shows "pders_set UNIV1 (ALT r1 r2) = pders_set UNIV1 r1 \<union> pders_set UNIV1 r2"

   353 by auto

   354 

   355 lemma pders_set_SEQ_aux:

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

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

   358 using a by (auto simp add: Suf_def)

   359 

   360 lemma pders_set_SEQ:

   361   shows "pders_set UNIV1 (SEQ r1 r2) \<subseteq> SEQS (pders_set UNIV1 r1) r2 \<union> pders_set UNIV1 r2"

   362 apply(rule UN_least)

   363 apply(rule subset_trans)

   364 apply(rule pders_SEQ)

   365 apply(simp)

   366 apply(rule conjI) 

   367 apply(auto)[1]

   368 apply(rule subset_trans)

   369 apply(rule pders_set_SEQ_aux)

   370 apply(auto)

   371 done

   372 

   373 lemma pders_set_STAR:

   374   shows "pders_set UNIV1 (STAR r) \<subseteq> SEQS (pders_set UNIV1 r) (STAR r)"

   375 apply(rule UN_least)

   376 apply(rule subset_trans)

   377 apply(rule pders_STAR)

   378 apply(simp)

   379 apply(simp add: Suf_def)

   380 apply(auto)

   381 done

   382 

   383 lemma finite_SEQS:

   384   assumes a: "finite A"

   385   shows "finite (SEQS A r)"

   386 using a by (auto)

   387 

   388 lemma finite_pders_set_UNIV1:

   389   shows "finite (pders_set UNIV1 r)"

   390 apply(induct r)

   391 apply(simp)

   392 apply(simp only: pders_set_EMPTY)

   393 apply(simp)

   394 apply(rule finite_subset)

   395 apply(rule pders_set_CHAR)

   396 apply(simp)

   397 apply(rule finite_subset)

   398 apply(rule pders_set_SEQ)

   399 apply(simp only: finite_SEQS finite_Un)

   400 apply(simp)

   401 apply(simp only: pders_set_ALT)

   402 apply(simp)

   403 apply(rule finite_subset)

   404 apply(rule pders_set_STAR)

   405 apply(simp only: finite_SEQS)

   406 done

   407     

   408 lemma pders_set_UNIV_UNIV1:

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

   410 apply(auto)

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

   412 apply(simp)

   413 done

   414 

   415 lemma finite_pders_set_UNIV:

   416   shows "finite (pders_set UNIV r)"

   417 unfolding pders_set_UNIV_UNIV1

   418 by (simp add: finite_pders_set_UNIV1)

   419 

   420 lemma finite_pders_set:

   421   shows "finite (pders_set A r)"

   422 apply(rule rev_finite_subset)

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

   424 apply(auto)

   425 done

   426 

   427 lemma finite_pders:

   428   shows "finite (pders s r)"

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

   430 by simp

   431 

   432 lemma finite_pders2:

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

   434 proof -

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

   436   moreover

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

   438     using finite_pders_set by simp

   439   ultimately 

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

   441     by(rule finite_subset)

   442 qed

   443 

   444 

   445 lemma Myhill_Nerode3:

   446   fixes r::"rexp"

   447   shows "finite (UNIV // \<approx>(L_rexp r))"

   448 proof -

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

   450   proof - 

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

   452     moreover 

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

   454     ultimately

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

   456       by simp

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

   458       by (rule finite_eq_tag_rel)

   459   qed

   460   moreover 

   461   have "=(\<lambda>x. pders x r)= \<subseteq> \<approx>(L_rexp r)"

   462     unfolding tag_eq_rel_def

   463     unfolding str_eq_def2

   464     unfolding MN_Rel_Ders

   465     unfolding Ders_pders

   466     by auto

   467   moreover 

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

   469     unfolding equiv_def refl_on_def sym_def trans_def

   470     unfolding tag_eq_rel_def

   471     by auto

   472   moreover

   473   have "equiv UNIV (\<approx>(L_rexp r))"

   474     unfolding equiv_def refl_on_def sym_def trans_def

   475     unfolding str_eq_rel_def

   476     by auto

   477   ultimately show "finite (UNIV // \<approx>(L_rexp r))" 

   478     by (rule refined_partition_finite)

   479 qed

   480 

   481 

   482 section {* Relating derivatives and partial derivatives *}

   483 

   484 lemma

   485   shows "(\<Union> L_rexp ` (pder c r)) = L_rexp (der c r)"

   486 unfolding Der_der[symmetric] Der_pder by simp

   487 

   488 lemma

   489   shows "(\<Union> L_rexp ` (pders s r)) = L_rexp (ders s r)"

   490 unfolding Ders_ders[symmetric] Ders_pders by simp

   491 

   492 end