1    

     2 theory PDerivs

     3   imports Spec

     4 begin

     5 

     6 (*

     7   ZERO

     8 | ONE

     9 | CHAR char

    10 | SEQ rexp rexp

    11 | ALT rexp rexp

    12 | STAR rexp

    13 *)

    14 

    15 abbreviation

    16   "SEQs rs r \<equiv> (\<Union>r' \<in> rs. {SEQ r' r})"

    17 

    18 lemma Timess_eq_image:

    19   "SEQs rs r = (\<lambda>r'. SEQ r' r) ` rs"

    20   by auto

    21 

    22 primrec

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

    24 where

    25   "pder c ZERO = {}"

    26 | "pder c ONE = {}"

    27 | "pder c (CHAR d) = (if c = d then {ONE} else {})"

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

    29 | "pder c (SEQ r1 r2) = 

    30     (if nullable r1 then SEQs (pder c r1) r2 \<union> pder c r2 else SEQs (pder c r1) r2)"

    31 | "pder c (STAR r) = SEQs (pder c r) (STAR r)"

    32 

    33 primrec

    34   pders :: "char list \<Rightarrow> rexp \<Rightarrow> rexp set"

    35 where

    36   "pders [] r = {r}"

    37 | "pders (c # s) r = \<Union> (pders s ` pder c r)"

    38 

    39 abbreviation

    40  pder_set :: "char \<Rightarrow> rexp set \<Rightarrow> rexp set"

    41 where

    42   "pder_set c rs \<equiv> \<Union> (pder c ` rs)"

    43 

    44 abbreviation

    45   pders_set :: "char list \<Rightarrow> rexp set \<Rightarrow> rexp set"

    46 where

    47   "pders_set s rs \<equiv> \<Union> (pders s ` rs)"

    48 

    49 lemma pders_append:

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

    51 by (induct s1 arbitrary: r) (simp_all)

    52 

    53 lemma pders_snoc:

    54   shows "pders (s @ [c]) r = pder_set c (pders s r)"

    55 by (simp add: pders_append)

    56 

    57 lemma pders_simps [simp]:

    58   shows "pders s ZERO = (if s = [] then {ZERO} else {})"

    59   and   "pders s ONE = (if s = [] then {ONE} else {})"

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

    61 by (induct s) (simp_all)

    62 

    63 lemma pders_CHAR:

    64   shows "pders s (CHAR c) \<subseteq> {CHAR c, ONE}"

    65 by (induct s) (simp_all)

    66 

    67 subsection \<open>Relating left-quotients and partial derivatives\<close>

    68 

    69 lemma Sequ_UNION_distrib:

    70 shows "A ;; \<Union>(M ` I) = \<Union>((%i. A ;; M i) ` I)"

    71 and   "\<Union>(M ` I) ;; A = \<Union>((%i. M i ;; A) ` I)"

    72 by (auto simp add: Sequ_def)

    73 

    74 

    75 lemma Der_pder:

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

    77 by (induct r) (simp_all add: nullable_correctness Sequ_UNION_distrib)

    78   

    79 lemma Ders_pders:

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

    81 proof (induct s arbitrary: r)

    82   case (Cons c s)

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

    84   have "Ders (c # s) (L r) = Ders s (Der c (L r))" by (simp add: Ders_def Der_def)

    85   also have "\<dots> = Ders s (\<Union> (L ` pder c r))" by (simp add: Der_pder)

    86   also have "\<dots> = (\<Union>A\<in>(L ` (pder c r)). (Ders s A))"

    87     by (auto simp add:  Ders_def)

    88   also have "\<dots> = \<Union> (L ` (pders_set s (pder c r)))"

    89     using ih by auto

    90   also have "\<dots> = \<Union> (L ` (pders (c # s) r))" by simp

    91   finally show "Ders (c # s) (L r) = \<Union> (L ` pders (c # s) r)" .

    92 qed (simp add: Ders_def)

    93 

    94 subsection \<open>Relating derivatives and partial derivatives\<close>

    95 

    96 lemma der_pder:

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

    98 unfolding der_correctness Der_pder by simp

    99 

   100 lemma ders_pders:

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

   102 unfolding der_correctness ders_correctness Ders_pders by simp

   103 

   104 

   105 subsection \<open>Finiteness property of partial derivatives\<close>

   106 

   107 definition

   108   pders_Set :: "string set \<Rightarrow> rexp \<Rightarrow> rexp set"

   109 where

   110   "pders_Set A r \<equiv> \<Union>x \<in> A. pders x r"

   111 

   112 lemma pders_Set_subsetI:

   113   assumes "\<And>s. s \<in> A \<Longrightarrow> pders s r \<subseteq> C"

   114   shows "pders_Set A r \<subseteq> C"

   115 using assms unfolding pders_Set_def by (rule UN_least)

   116 

   117 lemma pders_Set_union:

   118   shows "pders_Set (A \<union> B) r = (pders_Set A r \<union> pders_Set B r)"

   119 by (simp add: pders_Set_def)

   120 

   121 lemma pders_Set_subset:

   122   shows "A \<subseteq> B \<Longrightarrow> pders_Set A r \<subseteq> pders_Set B r"

   123 by (auto simp add: pders_Set_def)

   124 

   125 definition

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

   127 

   128 lemma pders_Set_ZERO [simp]:

   129   shows "pders_Set UNIV1 ZERO = {}"

   130 unfolding UNIV1_def pders_Set_def by auto

   131 

   132 lemma pders_Set_ONE [simp]:

   133   shows "pders_Set UNIV1 ONE = {}"

   134 unfolding UNIV1_def pders_Set_def by (auto split: if_splits)

   135 

   136 lemma pders_Set_CHAR [simp]:

   137   shows "pders_Set UNIV1 (CHAR c) = {ONE}"

   138 unfolding UNIV1_def pders_Set_def 

   139 apply(auto)

   140 apply(frule rev_subsetD)

   141 apply(rule pders_CHAR)

   142 apply(simp)

   143 apply(case_tac xa)

   144 apply(auto split: if_splits)

   145 done

   146 

   147 lemma pders_Set_ALT [simp]:

   148   shows "pders_Set UNIV1 (ALT r1 r2) = pders_Set UNIV1 r1 \<union> pders_Set UNIV1 r2"

   149 unfolding UNIV1_def pders_Set_def by auto

   150 

   151 

   152 text \<open>Non-empty suffixes of a string (needed for the cases of @{const SEQ} and @{const STAR} below)\<close>

   153 

   154 definition

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

   156 

   157 lemma PSuf_snoc:

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

   159 unfolding PSuf_def Sequ_def

   160 by (auto simp add: append_eq_append_conv2 append_eq_Cons_conv)

   161 

   162 lemma PSuf_Union:

   163   shows "(\<Union>v \<in> PSuf s ;; {[c]}. f v) = (\<Union>v \<in> PSuf s. f (v @ [c]))"

   164 by (auto simp add: Sequ_def)

   165 

   166 lemma pders_Set_snoc:

   167   shows "pders_Set (PSuf s ;; {[c]}) r = (pder_set c (pders_Set (PSuf s) r))"

   168 unfolding pders_Set_def

   169 by (simp add: PSuf_Union pders_snoc)

   170 

   171 lemma pderivs_Times:

   172   shows "pders s (SEQ r1 r2) \<subseteq> SEQs (pders s r1) r2 \<union> (pders_Set (PSuf s) r2)"

   173 proof (induct s rule: rev_induct)

   174   case (snoc c s)

   175   have ih: "pders s (SEQ r1 r2) \<subseteq> SEQs (pders s r1) r2 \<union> (pders_Set (PSuf s) r2)" 

   176     by fact

   177   have "pders (s @ [c]) (SEQ r1 r2) = pder_set c (pders s (SEQ r1 r2))" 

   178     by (simp add: pders_snoc)

   179   also have "\<dots> \<subseteq> pder_set c (SEQs (pders s r1) r2 \<union> (pders_Set (PSuf s) r2))"

   180     using ih by fastforce

   181   also have "\<dots> = pder_set c (SEQs (pders s r1) r2) \<union> pder_set c (pders_Set (PSuf s) r2)"

   182     by (simp)

   183   also have "\<dots> = pder_set c (SEQs (pders s r1) r2) \<union> pders_Set (PSuf s ;; {[c]}) r2"

   184     by (simp add: pders_Set_snoc)

   185   also 

   186   have "\<dots> \<subseteq> pder_set c (SEQs (pders s r1) r2) \<union> pder c r2 \<union> pders_Set (PSuf s ;; {[c]}) r2"

   187     by auto

   188   also 

   189   have "\<dots> \<subseteq> SEQs (pder_set c (pders s r1)) r2 \<union> pder c r2 \<union> pders_Set (PSuf s ;; {[c]}) r2"

   190     by (auto simp add: if_splits)

   191   also have "\<dots> = SEQs (pders (s @ [c]) r1) r2 \<union> pder c r2 \<union> pders_Set (PSuf s ;; {[c]}) r2"

   192     by (simp add: pders_snoc)

   193   also have "\<dots> \<subseteq> SEQs (pders (s @ [c]) r1) r2 \<union> pders_Set (PSuf (s @ [c])) r2"

   194     unfolding pders_Set_def by (auto simp add: PSuf_snoc)  

   195   finally show ?case .

   196 qed (simp) 

   197 

   198 lemma pders_Set_SEQ_aux1:

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

   200   shows "pders_Set (PSuf s) r \<subseteq> pders_Set UNIV1 r"

   201 using a unfolding UNIV1_def PSuf_def pders_Set_def by auto

   202 

   203 lemma pders_Set_SEQ_aux2:

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

   205   shows "SEQs (pders s r1) r2 \<subseteq> SEQs (pders_Set UNIV1 r1) r2"

   206 using a unfolding pders_Set_def by auto

   207 

   208 lemma pders_Set_SEQ:

   209   shows "pders_Set UNIV1 (SEQ r1 r2) \<subseteq> SEQs (pders_Set UNIV1 r1) r2 \<union> pders_Set UNIV1 r2"

   210 apply(rule pders_Set_subsetI)

   211 apply(rule subset_trans)

   212 apply(rule pderivs_Times)

   213 using pders_Set_SEQ_aux1 pders_Set_SEQ_aux2

   214 apply auto

   215 apply blast

   216 done

   217 

   218 lemma pders_STAR:

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

   220   shows "pders s (STAR r) \<subseteq> SEQs (pders_Set (PSuf s) r) (STAR r)"

   221 using a

   222 proof (induct s rule: rev_induct)

   223   case (snoc c s)

   224   have ih: "s \<noteq> [] \<Longrightarrow> pders s (STAR r) \<subseteq> SEQs (pders_Set (PSuf s) r) (STAR r)" by fact

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

   226     have "pders (s @ [c]) (STAR r) = pder_set c (pders s (STAR r))" by (simp add: pders_snoc)

   227     also have "\<dots> \<subseteq> pder_set c (SEQs (pders_Set (PSuf s) r) (STAR r))"

   228       using ih[OF asm] by fast

   229     also have "\<dots> \<subseteq> SEQs (pder_set c (pders_Set (PSuf s) r)) (STAR r) \<union> pder c (STAR r)"

   230       by (auto split: if_splits)

   231     also have "\<dots> \<subseteq> SEQs (pders_Set (PSuf (s @ [c])) r) (STAR r) \<union> (SEQs (pder c r) (STAR r))"

   232       by (simp only: PSuf_snoc pders_Set_snoc pders_Set_union)

   233          (auto simp add: pders_Set_def)

   234     also have "\<dots> = SEQs (pders_Set (PSuf (s @ [c])) r) (STAR r)"

   235       by (auto simp add: PSuf_snoc PSuf_Union pders_snoc pders_Set_def)

   236     finally have ?case .

   237   }

   238   moreover

   239   { assume asm: "s = []"

   240     then have ?case by (auto simp add: pders_Set_def pders_snoc PSuf_def)

   241   }

   242   ultimately show ?case by blast

   243 qed (simp)

   244 

   245 lemma pders_Set_STAR:

   246   shows "pders_Set UNIV1 (STAR r) \<subseteq> SEQs (pders_Set UNIV1 r) (STAR r)"

   247 apply(rule pders_Set_subsetI)

   248 apply(rule subset_trans)

   249 apply(rule pders_STAR)

   250 apply(simp add: UNIV1_def)

   251 apply(simp add: UNIV1_def PSuf_def)

   252 apply(auto simp add: pders_Set_def)

   253 done

   254 

   255 lemma finite_SEQs [simp]:

   256   assumes a: "finite A"

   257   shows "finite (SEQs A r)"

   258 using a by auto

   259 

   260 lemma finite_pders_Set_UNIV1:

   261   shows "finite (pders_Set UNIV1 r)"

   262 apply(induct r)

   263 apply(simp_all add: 

   264   finite_subset[OF pders_Set_SEQ]

   265   finite_subset[OF pders_Set_STAR])

   266 done

   267     

   268 lemma pders_Set_UNIV:

   269   shows "pders_Set UNIV r = pders [] r \<union> pders_Set UNIV1 r"

   270 unfolding UNIV1_def pders_Set_def

   271 by blast

   272 

   273 lemma finite_pders_Set_UNIV:

   274   shows "finite (pders_Set UNIV r)"

   275 unfolding pders_Set_UNIV

   276 by (simp add: finite_pders_Set_UNIV1)

   277 

   278 lemma finite_pders_set:

   279   shows "finite (pders_Set A r)"

   280 by (metis finite_pders_Set_UNIV pders_Set_subset rev_finite_subset subset_UNIV)

   281 

   282 

   283 text\<open>The following relationship between the alphabetic width of regular expressions

   284 (called \<open>awidth\<close> below) and the number of partial derivatives was proved

   285 by Antimirov~\cite{Antimirov95} and formalized by Max Haslbeck.\<close>

   286 

   287 fun awidth :: "rexp \<Rightarrow> nat" where

   288 "awidth ZERO = 0" |

   289 "awidth ONE = 0" |

   290 "awidth (CHAR a) = 1" |

   291 "awidth (ALT r1 r2) = awidth r1 + awidth r2" |

   292 "awidth (SEQ r1 r2) = awidth r1 + awidth r2" |

   293 "awidth (STAR r1) = awidth r1"

   294 

   295 lemma card_SEQs_pders_Set_le:

   296   "card (SEQs (pders_Set A r) s) \<le> card (pders_Set A r)"

   297   using finite_pders_set unfolding Timess_eq_image by (rule card_image_le)

   298 

   299 lemma card_pders_set_UNIV1_le_awidth: "card (pders_Set UNIV1 r) \<le> awidth r"

   300 proof (induction r)

   301   case (ALT r1 r2)

   302   have "card (pders_Set UNIV1 (ALT r1 r2)) = card (pders_Set UNIV1 r1 \<union> pders_Set UNIV1 r2)" by simp

   303   also have "\<dots> \<le> card (pders_Set UNIV1 r1) + card (pders_Set UNIV1 r2)"

   304     by(simp add: card_Un_le)

   305   also have "\<dots> \<le> awidth (ALT r1 r2)" using ALT.IH by simp

   306   finally show ?case .

   307 next

   308   case (SEQ r1 r2)

   309   have "card (pders_Set UNIV1 (SEQ r1 r2)) \<le> card (SEQs (pders_Set UNIV1 r1) r2 \<union> pders_Set UNIV1 r2)"

   310     by (simp add: card_mono finite_pders_set pders_Set_SEQ)

   311   also have "\<dots> \<le> card (SEQs (pders_Set UNIV1 r1) r2) + card (pders_Set UNIV1 r2)"

   312     by (simp add: card_Un_le)

   313   also have "\<dots> \<le> card (pders_Set UNIV1 r1) + card (pders_Set UNIV1 r2)"

   314     by (simp add: card_SEQs_pders_Set_le)

   315   also have "\<dots> \<le> awidth (SEQ r1 r2)" using SEQ.IH by simp

   316   finally show ?case .

   317 next

   318   case (STAR r)

   319   have "card (pders_Set UNIV1 (STAR r)) \<le> card (SEQs (pders_Set UNIV1 r) (STAR r))"

   320     by (simp add: card_mono finite_pders_set pders_Set_STAR)

   321   also have "\<dots> \<le> card (pders_Set UNIV1 r)" by (rule card_SEQs_pders_Set_le)

   322   also have "\<dots> \<le> awidth (STAR r)" by (simp add: STAR.IH)

   323   finally show ?case .

   324 qed (auto)

   325 

   326 text\<open>Antimirov's Theorem 3.4:\<close>

   327 theorem card_pders_set_UNIV_le_awidth: "card (pders_Set UNIV r) \<le> awidth r + 1"

   328 proof -

   329   have "card (insert r (pders_Set UNIV1 r)) \<le> Suc (card (pders_Set UNIV1 r))"

   330     by(auto simp: card_insert_if[OF finite_pders_Set_UNIV1])

   331   also have "\<dots> \<le> Suc (awidth r)" by(simp add: card_pders_set_UNIV1_le_awidth)

   332   finally show ?thesis by(simp add: pders_Set_UNIV)

   333 qed 

   334 

   335 text\<open>Antimirov's Corollary 3.5:\<close>

   336 corollary card_pders_set_le_awidth: "card (pders_Set A r) \<le> awidth r + 1"

   337 by(rule order_trans[OF

   338   card_mono[OF finite_pders_Set_UNIV pders_Set_subset[OF subset_UNIV]]

   339   card_pders_set_UNIV_le_awidth])

   340 

   341 

   342 end