Mercurial Mercurial > hg > lexing / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/PDerivs.thy
changeset 309 a7769a89c529
parent 308 496a37d816e9
child 311 8b8db9558ecf
equal deleted inserted replaced
308:496a37d816e9 309:a7769a89c529 
     1    
     1    
     2 theory PDerivs
 
     2 theory PDerivs
 
     3   imports Spec
 
     3   imports Spec
 
     4 begin
 
     4 begin
 
     5 
     5 
     6 (*
 
       
     7   ZERO
 
       
     8 | ONE
 
       
     9 | CHAR char
 
       
    10 | SEQ rexp rexp
 
       
    11 | ALT rexp rexp
 
       
    12 | STAR rexp
 
       
    13 *)
 
       
    14 
       
    15 abbreviation
 
     6 abbreviation
 
    16   "SEQs rs r \<equiv> (\<Union>r' \<in> rs. {SEQ r' r})"
 
     7   "SEQs rs r \<equiv> (\<Union>r' \<in> rs. {SEQ r' r})"
 
    17 
     8 
    18 lemma Timess_eq_image:
 
     9 lemma SEQs_eq_image:
 
    19   "SEQs rs r = (\<lambda>r'. SEQ r' r) ` rs"
 
    10   "SEQs rs r = (\<lambda>r'. SEQ r' r) ` rs"
 
    20   by auto
 
    11   by auto
 
    21 
    12 
    22 primrec
 
    13 primrec
 
    23   pder :: "char \<Rightarrow> rexp \<Rightarrow> rexp set"
 
    14   pder :: "char \<Rightarrow> rexp \<Rightarrow> rexp set"
 
    65 by (induct s) (simp_all)
 
    56 by (induct s) (simp_all)
 
    66 
    57 
    67 subsection \<open>Relating left-quotients and partial derivatives\<close>
 
    58 subsection \<open>Relating left-quotients and partial derivatives\<close>
 
    68 
    59 
    69 lemma Sequ_UNION_distrib:
 
    60 lemma Sequ_UNION_distrib:
 
    70 shows "A ;; \<Union>(M ` I) = \<Union>((%i. A ;; M i) ` I)"
 
    61 shows "A ;; \<Union>(M ` I) = \<Union>((\<lambda>i. A ;; M i) ` I)"
 
    71 and   "\<Union>(M ` I) ;; A = \<Union>((%i. M i ;; A) ` I)"
 
    62 and   "\<Union>(M ` I) ;; A = \<Union>((\<lambda>i. M i ;; A) ` I)"
 
    72 by (auto simp add: Sequ_def)
 
    63 by (auto simp add: Sequ_def)
 
    73 
    64 
    74 
    65 
    75 lemma Der_pder:
 
    66 lemma Der_pder:
 
    76   shows "Der c (L r) = \<Union> (L ` pder c r)"
 
    67   shows "Der c (L r) = \<Union> (L ` pder c r)"
 
   166 lemma pders_Set_snoc:
 
   157 lemma pders_Set_snoc:
 
   167   shows "pders_Set (PSuf s ;; {[c]}) r = (pder_set c (pders_Set (PSuf s) r))"
 
   158   shows "pders_Set (PSuf s ;; {[c]}) r = (pder_set c (pders_Set (PSuf s) r))"
 
   168 unfolding pders_Set_def
 
   159 unfolding pders_Set_def
 
   169 by (simp add: PSuf_Union pders_snoc)
 
   160 by (simp add: PSuf_Union pders_snoc)
 
   170 
   161 
   171 lemma pderivs_Times:
 
   162 lemma pderivs_SEQ:
 
   172   shows "pders s (SEQ r1 r2) \<subseteq> SEQs (pders s r1) r2 \<union> (pders_Set (PSuf s) r2)"
 
   163   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)
 
   164 proof (induct s rule: rev_induct)
 
   174   case (snoc c s)
 
   165   case (snoc c s)
 
   175   have ih: "pders s (SEQ r1 r2) \<subseteq> SEQs (pders s r1) r2 \<union> (pders_Set (PSuf s) r2)" 
   166   have ih: "pders s (SEQ r1 r2) \<subseteq> SEQs (pders s r1) r2 \<union> (pders_Set (PSuf s) r2)" 
   176     by fact
 
   167     by fact
 
   207 
   198 
   208 lemma pders_Set_SEQ:
 
   199 lemma pders_Set_SEQ:
 
   209   shows "pders_Set UNIV1 (SEQ r1 r2) \<subseteq> SEQs (pders_Set UNIV1 r1) r2 \<union> pders_Set UNIV1 r2"
 
   200   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)
 
   201 apply(rule pders_Set_subsetI)
 
   211 apply(rule subset_trans)
 
   202 apply(rule subset_trans)
 
   212 apply(rule pderivs_Times)
 
   203 apply(rule pderivs_SEQ)
 
   213 using pders_Set_SEQ_aux1 pders_Set_SEQ_aux2
 
   204 using pders_Set_SEQ_aux1 pders_Set_SEQ_aux2
 
   214 apply auto
 
   205 apply auto
 
   215 apply blast
 
   206 apply blast
 
   216 done
 
   207 done
 
   217 
   208 
   278 lemma finite_pders_set:
 
   269 lemma finite_pders_set:
 
   279   shows "finite (pders_Set A r)"
 
   270   shows "finite (pders_Set A r)"
 
   280 by (metis finite_pders_Set_UNIV pders_Set_subset rev_finite_subset subset_UNIV)
 
   271 by (metis finite_pders_Set_UNIV pders_Set_subset rev_finite_subset subset_UNIV)
 
   281 
   272 
   282 
   273 
   283 text\<open>The following relationship between the alphabetic width of regular expressions
 
   274 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
 
   275 (called \<open>awidth\<close> below) and the number of partial derivatives was proved
 
   285 by Antimirov~\cite{Antimirov95} and formalized by Max Haslbeck.\<close>
 
   276 by Antimirov~\cite{Antimirov95} and formalized by Max Haslbeck.\<close>
 
   286 
   277 
   287 fun awidth :: "rexp \<Rightarrow> nat" where
 
   278 fun awidth :: "rexp \<Rightarrow> nat" where
 
   288 "awidth ZERO = 0" |
 
   279 "awidth ZERO = 0" |
 
   291 "awidth (ALT r1 r2) = awidth r1 + awidth r2" |
 
   282 "awidth (ALT r1 r2) = awidth r1 + awidth r2" |
 
   292 "awidth (SEQ r1 r2) = awidth r1 + awidth r2" |
 
   283 "awidth (SEQ r1 r2) = awidth r1 + awidth r2" |
 
   293 "awidth (STAR r1) = awidth r1"
 
   284 "awidth (STAR r1) = awidth r1"
 
   294 
   285 
   295 lemma card_SEQs_pders_Set_le:
 
   286 lemma card_SEQs_pders_Set_le:
 
   296   "card (SEQs (pders_Set A r) s) \<le> card (pders_Set A r)"
 
   287   shows  "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)
 
   288   using finite_pders_set 
   298 
   289   unfolding SEQs_eq_image 
   299 lemma card_pders_set_UNIV1_le_awidth: "card (pders_Set UNIV1 r) \<le> awidth r"
 
   290   by (rule card_image_le)
 
       
   291 
       
   292 lemma card_pders_set_UNIV1_le_awidth: 
       
   293   shows "card (pders_Set UNIV1 r) \<le> awidth r"
 
   300 proof (induction r)
 
   294 proof (induction r)
 
   301   case (ALT r1 r2)
 
   295   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
 
   296   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)"
 
   297   also have "\<dots> \<le> card (pders_Set UNIV1 r1) + card (pders_Set UNIV1 r2)"
 
   304     by(simp add: card_Un_le)
 
   298     by(simp add: card_Un_le)
 
   322   also have "\<dots> \<le> awidth (STAR r)" by (simp add: STAR.IH)
 
   316   also have "\<dots> \<le> awidth (STAR r)" by (simp add: STAR.IH)
 
   323   finally show ?case .
 
   317   finally show ?case .
 
   324 qed (auto)
 
   318 qed (auto)
 
   325 
   319 
   326 text\<open>Antimirov's Theorem 3.4:\<close>
 
   320 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"
 
   321 
       
   322 theorem card_pders_set_UNIV_le_awidth: 
       
   323   shows "card (pders_Set UNIV r) \<le> awidth r + 1"
 
   328 proof -
 
   324 proof -
 
   329   have "card (insert r (pders_Set UNIV1 r)) \<le> Suc (card (pders_Set UNIV1 r))"
 
   325   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])
 
   326     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)
 
   327   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)
 
   328   finally show ?thesis by(simp add: pders_Set_UNIV)
 
   333 qed 
   329 qed 
   334 
   330 
   335 text\<open>Antimirov's Corollary 3.5:\<close>
 
   331 text\<open>Antimirov's Corollary 3.5:\<close>
 
   336 corollary card_pders_set_le_awidth: "card (pders_Set A r) \<le> awidth r + 1"
 
   332 
   337 by(rule order_trans[OF
 
   333 corollary card_pders_set_le_awidth: 
   338   card_mono[OF finite_pders_Set_UNIV pders_Set_subset[OF subset_UNIV]]
 
   334   shows "card (pders_Set A r) \<le> awidth r + 1"
 
   339   card_pders_set_UNIV_le_awidth])
 
   335 proof -
 
       
   336   have "card (pders_Set A r) \<le> card (pders_Set UNIV r)"
 
       
   337     by (simp add: card_mono finite_pders_set pders_Set_subset)
 
       
   338   also have "... \<le> awidth r + 1"
 
       
   339     by (rule card_pders_set_UNIV_le_awidth)
 
       
   340   finally show "card (pders_Set A r) \<le> awidth r + 1" by simp
 
       
   341 qed
 
   340 
   342 
   341 
   343 
   342 end
 
   344 end
lexing