1 theory Derivs

     2 imports Closure

     3 begin

     4 

     5 section {* Experiments with Derivatives -- independent of Myhill-Nerode *}

     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 ;; B) = (Der c A) ;; B \<union> (Delta A ;; 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) ;; A\<star>"

    62 apply(subst star_cases)

    63 apply(simp only: Delta_def Der_union Der_seq Der_empty)

    64 apply(simp add: Der_def Seq_def)

    65 apply(auto)

    66 apply(drule star_decom)

    67 apply(auto simp add: Cons_eq_append_conv)

    68 done

    69 

    70 lemma Ders_singleton:

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

    72 unfolding Der_def Ders_def

    73 by simp

    74 

    75 lemma Ders_append:

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

    77 unfolding Ders_def by simp 

    78 

    79 lemma MN_Rel_Ders:

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

    81 unfolding Ders_def str_eq_def str_eq_rel_def

    82 by auto

    83 

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

    85 

    86 fun

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

    88 where

    89   "nullable (NULL) = False"

    90 | "nullable (EMPTY) = True"

    91 | "nullable (CHAR c) = False"

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

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

    94 | "nullable (STAR r) = True"

    95 

    96 fun

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

    98 where

    99   "der c (NULL) = NULL"

   100 | "der c (EMPTY) = NULL"

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

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

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

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

   105 

   106 function 

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

   108 where

   109   "ders [] r = r"

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

   111 by (auto) (metis rev_cases)

   112 

   113 termination

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

   115 

   116 lemma Delta_nullable:

   117   shows "Delta (L r) = (if nullable r then {[]} else {})"

   118 unfolding Delta_def

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

   120 

   121 lemma Der_der:

   122   fixes r::rexp

   123   shows "Der c (L r) = L (der c r)"

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

   125 

   126 lemma Ders_ders:

   127   fixes r::rexp

   128   shows "Ders s (L r) = L (ders s r)"

   129 apply(induct s rule: rev_induct)

   130 apply(simp add: Ders_def)

   131 apply(simp only: ders.simps)

   132 apply(simp only: Ders_append)

   133 apply(simp only: Ders_singleton)

   134 apply(simp only: Der_der)

   135 done

   136 

   137 

   138 subsection {* Antimirov's Partial Derivatives *}

   139 

   140 abbreviation

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

   142 

   143 fun

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

   145 where

   146   "pder c NULL = {NULL}"

   147 | "pder c EMPTY = {NULL}"

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

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

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

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

   152 

   153 abbreviation

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

   155 

   156 function 

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

   158 where

   159   "pders [] r = {r}"

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

   161 by (auto) (metis rev_cases)

   162 

   163 termination

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

   165 

   166 abbreviation

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

   168 

   169 

   170 lemma pders_append:

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

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

   173 apply(simp)

   174 apply(subst append_assoc[symmetric])

   175 apply(simp only: pders.simps)

   176 apply(auto)

   177 done

   178 

   179 lemma pders_singleton:

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

   181 apply(subst append_Nil[symmetric])

   182 apply(simp only: pders.simps)

   183 apply(simp)

   184 done

   185 

   186 lemma pder_set_lang:

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

   188 unfolding image_def 

   189 by auto

   190 

   191 lemma

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

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

   194 unfolding Seq_def by auto

   195 

   196 lemma Der_pder:

   197   fixes r::rexp

   198   shows "Der c (L r) = \<Union> L ` (pder c r)"

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

   200 

   201 lemma Ders_pders:

   202   fixes r::rexp

   203   shows "Ders s (L r) = \<Union> L ` (pders s r)"

   204 proof (induct s rule: rev_induct)

   205   case (snoc c s)

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

   207   have "Ders (s @ [c]) (L r) = Ders [c] (Ders s (L r))"

   208     by (simp add: Ders_append)

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

   210     by (simp add: Ders_singleton)

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

   212     unfolding Der_def image_def by auto

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

   214     by (simp add: Der_pder)

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

   216     by (simp add: pder_set_lang)

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

   218     by simp

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

   220 qed (simp add: Ders_def)

   221 

   222 lemma Ders_set_pders_set:

   223   fixes r::rexp

   224   shows "Ders_set A (L r) = (\<Union> L ` (pders_set A r))"

   225 by (simp add: Ders_set_Ders Ders_pders)

   226 

   227 lemma pders_NULL [simp]:

   228   shows "pders s NULL = {NULL}"

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

   230 

   231 lemma pders_EMPTY [simp]:

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

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

   234 

   235 lemma pders_CHAR [simp]:

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

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

   238 

   239 lemma pders_ALT [simp]:

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

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

   242 

   243 definition

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

   245 

   246 lemma Suf:

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

   248 unfolding Suf_def Seq_def

   249 by (auto simp add: append_eq_append_conv2 append_eq_Cons_conv)

   250 

   251 lemma Suf_Union:

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

   253 by (auto simp add: Seq_def)

   254 

   255 lemma inclusion1:

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

   257 apply(auto simp add: if_splits)

   258 apply(blast)

   259 done

   260 

   261 lemma pders_SEQ:

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

   263 proof (induct s rule: rev_induct)

   264   case (snoc c s)

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

   266     by fact

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

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

   269     using ih by auto 

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

   271     by (simp)

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

   273     by (simp)

   274   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)"

   275     by (auto)

   276   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)"

   277     using inclusion1 by blast

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

   279     apply(subst (2) pders.simps)

   280     apply(simp only: Suf)

   281     apply(simp add: Suf_Union pders_singleton)

   282     apply(auto)

   283     done

   284   finally show ?case .

   285 qed (simp)

   286 

   287 lemma pders_STAR:

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

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

   290 using a

   291 proof (induct s rule: rev_induct)

   292   case (snoc c s)

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

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

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

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

   297       using ih[OF asm] by blast

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

   299       by simp

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

   301       using inclusion1 by blast

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

   303       using asm by (auto simp add: Suf_def)

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

   305       by simp

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

   307       apply(simp only: Suf)

   308       apply(simp add: Suf_Union pders_singleton)

   309       apply(auto)

   310       done

   311     finally have ?case .

   312   }

   313   moreover

   314   { assume asm: "s = []"

   315     then have ?case

   316       apply(simp add: pders_singleton Suf_def)

   317       apply(auto)

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

   319       apply(simp add: pders_singleton)

   320       done

   321   }

   322   ultimately show ?case by blast

   323 qed (simp)

   324 

   325 abbreviation 

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

   327 

   328 lemma pders_set_NULL:

   329   shows "pders_set UNIV1 NULL = {NULL}"

   330 by auto

   331 

   332 lemma pders_set_EMPTY:

   333   shows "pders_set UNIV1 EMPTY = {NULL}"

   334 by (auto split: if_splits)

   335 

   336 lemma pders_set_CHAR:

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

   338 by (auto split: if_splits)

   339 

   340 lemma pders_set_ALT:

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

   342 by auto

   343 

   344 lemma pders_set_SEQ_aux:

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

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

   347 using a by (auto simp add: Suf_def)

   348 

   349 lemma pders_set_SEQ:

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

   351 apply(rule UN_least)

   352 apply(rule subset_trans)

   353 apply(rule pders_SEQ)

   354 apply(simp)

   355 apply(rule conjI) 

   356 apply(auto)[1]

   357 apply(rule subset_trans)

   358 apply(rule pders_set_SEQ_aux)

   359 apply(auto)

   360 done

   361 

   362 lemma pders_set_STAR:

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

   364 apply(rule UN_least)

   365 apply(rule subset_trans)

   366 apply(rule pders_STAR)

   367 apply(simp)

   368 apply(simp add: Suf_def)

   369 apply(auto)

   370 done

   371 

   372 lemma finite_SEQS:

   373   assumes a: "finite A"

   374   shows "finite (SEQS A r)"

   375 using a by (auto)

   376 

   377 lemma finite_pders_set_UNIV1:

   378   shows "finite (pders_set UNIV1 r)"

   379 apply(induct r)

   380 apply(simp)

   381 apply(simp only: pders_set_EMPTY)

   382 apply(simp)

   383 apply(rule finite_subset)

   384 apply(rule pders_set_CHAR)

   385 apply(simp)

   386 apply(rule finite_subset)

   387 apply(rule pders_set_SEQ)

   388 apply(simp only: finite_SEQS finite_Un)

   389 apply(simp)

   390 apply(simp only: pders_set_ALT)

   391 apply(simp)

   392 apply(rule finite_subset)

   393 apply(rule pders_set_STAR)

   394 apply(simp only: finite_SEQS)

   395 done

   396     

   397 lemma pders_set_UNIV_UNIV1:

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

   399 apply(auto)

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

   401 apply(simp)

   402 done

   403 

   404 lemma finite_pders_set_UNIV:

   405   shows "finite (pders_set UNIV r)"

   406 unfolding pders_set_UNIV_UNIV1

   407 by (simp add: finite_pders_set_UNIV1)

   408 

   409 lemma finite_pders_set:

   410   shows "finite (pders_set A r)"

   411 apply(rule rev_finite_subset)

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

   413 apply(auto)

   414 done

   415 

   416 lemma finite_pders:

   417   shows "finite (pders s r)"

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

   419 by simp

   420 

   421 

   422 lemma test: 

   423   shows "pders_set A r = (\<Union> {pders s r | s. s \<in> A})"

   424 by auto

   425 

   426 lemma finite_pow_pders:

   427   shows "finite (Pow (\<Union> {pders s r | s. s \<in> A}))"

   428 using finite_pders_set

   429 by (simp add: test)

   430 

   431 lemma test2:

   432   shows "{pders s r | s. s \<in> A} \<subseteq> Pow (\<Union> {pders s r | s. s \<in> A})"

   433   by auto

   434 

   435 lemma test3:

   436   shows "finite ({pders s r | s. s \<in> A})"

   437 apply(rule finite_subset)

   438 apply(rule test2)

   439 apply(rule finite_pow_pders)

   440 done

   441 

   442 lemma Myhill_Nerode_aux:

   443   fixes r::"rexp"

   444   shows "finite (UNIV // =(\<lambda>x. pders x r)=)"

   445 apply(rule finite_eq_tag_rel)

   446 apply(rule rev_finite_subset)

   447 apply(rule test3)

   448 apply(auto)

   449 done

   450 

   451 lemma Myhill_Nerode3:

   452   fixes r::"rexp"

   453   shows "finite (UNIV // \<approx>(L r))"

   454 apply(rule refined_partition_finite)

   455 apply(rule Myhill_Nerode_aux[where r="r"])

   456 apply(simp add: tag_eq_rel_def)

   457 apply(auto)[1]

   458 unfolding str_eq_def[symmetric]

   459 unfolding MN_Rel_Ders

   460 apply(simp add: Ders_pders)

   461 apply(rule equivI)

   462 apply(auto simp add: tag_eq_rel_def refl_on_def sym_def trans_def)

   463 apply(rule equivI)

   464 apply(auto simp add: str_eq_rel_def refl_on_def sym_def trans_def)

   465 done

   466 

   467 

   468 section {* Closure under Left-Quotients *}

   469 

   470 lemma closure_left_quotient:

   471   assumes "regular A"

   472   shows "regular (Ders_set B A)"

   473 proof -

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

   475   have fin: "finite (pders_set B r)" by (rule finite_pders_set)

   476   

   477   have "Ders_set B (L r) = (\<Union> L ` (pders_set B r))"

   478     by (simp add: Ders_set_pders_set)

   479   also have "\<dots> = L (\<Uplus>(pders_set B r))" using fin by simp

   480   finally have "Ders_set B A = L (\<Uplus>(pders_set B r))" using eq

   481     by simp

   482   then show "regular (Ders_set B A)" by auto

   483 qed

   484 

   485 

   486 section {* Relating standard and partial derivations *}

   487 

   488 lemma

   489   shows "(\<Union> L ` (pder c r)) = L (der c r)"

   490 unfolding Der_der[symmetric] Der_pder by simp

   491 

   492 lemma

   493   shows "(\<Union> L ` (pders s r)) = L (ders s r)"

   494 unfolding Ders_ders[symmetric] Ders_pders by simp

   495 

   496 

   497 section {* attempt to prove MN *}

   498 (*

   499 lemma Myhill_Nerode3:

   500   fixes r::"rexp"

   501   shows "finite (UNIV // =(\<lambda>x. pders x r)=)"

   502 apply(rule finite_eq_tag_rel)

   503 apply(rule finite_pders_set)

   504 apply(simp add: Range_def)

   505 unfolding Quotien_def

   506 by (induct r) (auto)

   507 *)

   508 

   509 fun

   510   width :: "rexp \<Rightarrow> nat"

   511 where

   512   "width (NULL) = 0"

   513 | "width (EMPTY) = 0"

   514 | "width (CHAR c) = 1"

   515 | "width (ALT r1 r2) = width r1 + width r2"

   516 | "width (SEQ r1 r2) = width r1 + width r2"

   517 | "width (STAR r) = width r"

   518 

   519 

   520  

   521 end