Mercurial Mercurial > hg > regexp / 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.
Derivatives.thy
changeset 191 f6a603be52d6
parent 190 b73478aaf33e
child 193 2a5ac68db24b
equal deleted inserted replaced
190:b73478aaf33e 191:f6a603be52d6 
   182 unfolding Ders_ders[symmetric] Ders_pders by simp
 
   182 unfolding Ders_ders[symmetric] Ders_pders by simp
 
   183 
   183 
   184 
   184 
   185 subsection {* There are only finitely many partial derivatives for a language *}
 
   185 subsection {* There are only finitely many partial derivatives for a language *}
 
   186 
   186 
   187 abbreviation
 
   187 definition
 
   188   "pders_lang A r \<equiv> \<Union>s \<in> A. pders s r"
 
   188   "pders_lang A r \<equiv> \<Union>s \<in> A. pders s r"
 
   189 
   189 
   190 text {* Non-empty suffixes of a string *}
 
   190 lemma pders_lang_subsetI [intro]:
 
       
   191   assumes "\<And>s. s \<in> A \<Longrightarrow> pders s r \<subseteq> C"
 
       
   192   shows "pders_lang A r \<subseteq> C"
 
       
   193 using assms unfolding pders_lang_def by (rule UN_least)
 
       
   194 
       
   195 lemma pders_lang_union:
 
       
   196   shows "pders_lang (A \<union> B) r = (pders_lang A r \<union> pders_lang B r)"
 
       
   197 by (simp add: pders_lang_def)
 
       
   198 
       
   199 definition
 
       
   200   "UNIV1 \<equiv> UNIV - {[]}"
 
       
   201 
       
   202 lemma pders_lang_Zero [simp]:
 
       
   203   shows "pders_lang UNIV1 Zero = {Zero}"
 
       
   204 unfolding UNIV1_def pders_lang_def by auto
 
       
   205 
       
   206 lemma pders_lang_One [simp]:
 
       
   207   shows "pders_lang UNIV1 One = {Zero}"
 
       
   208 unfolding UNIV1_def pders_lang_def by (auto split: if_splits)
 
       
   209 
       
   210 lemma pders_lang_Atom:
 
       
   211   shows "pders_lang UNIV1 (Atom c) \<subseteq> {One, Zero}"
 
       
   212 unfolding UNIV1_def pders_lang_def by (auto split: if_splits)
 
       
   213 
       
   214 lemma pders_lang_Plus [simp]:
 
       
   215   shows "pders_lang UNIV1 (Plus r1 r2) = pders_lang UNIV1 r1 \<union> pders_lang UNIV1 r2"
 
       
   216 unfolding UNIV1_def pders_lang_def by auto
 
       
   217 
       
   218 
       
   219 text {* Non-empty suffixes of a string (needed for teh cases of @{const Times} and @{const Star} *}
 
   191 
   220 
   192 definition
 
   221 definition
 
   193   "Suf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}"
 
   222   "Suf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}"
 
   194 
   223 
   195 lemma Suf_snoc:
 
   224 lemma Suf_snoc:
 
   201   shows "(\<Union>v \<in> Suf s \<cdot> {[c]}. f v) = (\<Union>v \<in> Suf s. f (v @ [c]))"
 
   230   shows "(\<Union>v \<in> Suf s \<cdot> {[c]}. f v) = (\<Union>v \<in> Suf s. f (v @ [c]))"
 
   202 by (auto simp add: conc_def)
 
   231 by (auto simp add: conc_def)
 
   203 
   232 
   204 lemma pders_lang_snoc:
 
   233 lemma pders_lang_snoc:
 
   205   shows "pders_lang (Suf s \<cdot> {[c]}) r = (pder_set c (pders_lang (Suf s) r))"
 
   234   shows "pders_lang (Suf s \<cdot> {[c]}) r = (pder_set c (pders_lang (Suf s) r))"
 
       
   235 unfolding pders_lang_def
 
   206 by (simp add: Suf_Union pders_snoc)
 
   236 by (simp add: Suf_Union pders_snoc)
 
   207 
   237 
   208 lemma pders_Times:
 
   238 lemma pders_Times:
 
   209   shows "pders s (Times r1 r2) \<subseteq> Timess (pders s r1) r2 \<union> (pders_lang (Suf s) r2)"
 
   239   shows "pders s (Times r1 r2) \<subseteq> Timess (pders s r1) r2 \<union> (pders_lang (Suf s) r2)"
 
   210 proof (induct s rule: rev_induct)
 
   240 proof (induct s rule: rev_induct)
 
   224   also have "\<dots> \<subseteq> Timess (pder_set c (pders s r1)) r2 \<union> pder c r2 \<union> pders_lang (Suf s \<cdot> {[c]}) r2"
 
   254   also have "\<dots> \<subseteq> Timess (pder_set c (pders s r1)) r2 \<union> pder c r2 \<union> pders_lang (Suf s \<cdot> {[c]}) r2"
 
   225     by (auto simp add: if_splits) (blast)
 
   255     by (auto simp add: if_splits) (blast)
 
   226   also have "\<dots> = Timess (pders (s @ [c]) r1) r2 \<union> pder c r2 \<union> pders_lang (Suf s \<cdot> {[c]}) r2"
 
   256   also have "\<dots> = Timess (pders (s @ [c]) r1) r2 \<union> pder c r2 \<union> pders_lang (Suf s \<cdot> {[c]}) r2"
 
   227     by (simp add: pders_snoc)
 
   257     by (simp add: pders_snoc)
 
   228   also have "\<dots> \<subseteq> Timess (pders (s @ [c]) r1) r2 \<union> pders_lang (Suf (s @ [c])) r2"
 
   258   also have "\<dots> \<subseteq> Timess (pders (s @ [c]) r1) r2 \<union> pders_lang (Suf (s @ [c])) r2"
 
   229     by (auto simp add: Suf_snoc)  
   259     unfolding pders_lang_def by (auto simp add: Suf_snoc)  
   230   finally show ?case .
 
   260   finally show ?case .
 
   231 qed (simp) 
   261 qed (simp) 
       
   262 
       
   263 lemma pders_lang_Times_aux1:
 
       
   264   assumes a: "s \<in> UNIV1"
 
       
   265   shows "pders_lang (Suf s) r \<subseteq> pders_lang UNIV1 r"
 
       
   266 using a unfolding UNIV1_def Suf_def pders_lang_def by auto
 
       
   267 
       
   268 lemma pders_lang_Times_aux2:
 
       
   269   assumes a: "s \<in> UNIV1"
 
       
   270   shows "Timess (pders s r1) r2 \<subseteq> Timess (pders_lang UNIV1 r1) r2"
 
       
   271 using a unfolding pders_lang_def by auto
 
       
   272 
       
   273 lemma pders_lang_Times [intro]:
 
       
   274   shows "pders_lang UNIV1 (Times r1 r2) \<subseteq> Timess (pders_lang UNIV1 r1) r2 \<union> pders_lang UNIV1 r2"
 
       
   275 apply(rule pders_lang_subsetI)
 
       
   276 apply(rule subset_trans)
 
       
   277 apply(rule pders_Times)
 
       
   278 using pders_lang_Times_aux1 pders_lang_Times_aux2
 
       
   279 apply(blast)
 
       
   280 done
 
   232 
   281 
   233 lemma pders_Star:
 
   282 lemma pders_Star:
 
   234   assumes a: "s \<noteq> []"
 
   283   assumes a: "s \<noteq> []"
 
   235   shows "pders s (Star r) \<subseteq> Timess (pders_lang (Suf s) r) (Star r)"
 
   284   shows "pders s (Star r) \<subseteq> Timess (pders_lang (Suf s) r) (Star r)"
 
   236 using a
 
   285 using a
 
   242     also have "\<dots> \<subseteq> pder_set c (Timess (pders_lang (Suf s) r) (Star r))"
 
   291     also have "\<dots> \<subseteq> pder_set c (Timess (pders_lang (Suf s) r) (Star r))"
 
   243       using ih[OF asm] by (auto) (blast)
 
   292       using ih[OF asm] by (auto) (blast)
 
   244     also have "\<dots> \<subseteq> Timess (pder_set c (pders_lang (Suf s) r)) (Star r) \<union> pder c (Star r)"
 
   293     also have "\<dots> \<subseteq> Timess (pder_set c (pders_lang (Suf s) r)) (Star r) \<union> pder c (Star r)"
 
   245       by (auto split: if_splits) (blast)+
 
   294       by (auto split: if_splits) (blast)+
 
   246     also have "\<dots> \<subseteq> Timess (pders_lang (Suf (s @ [c])) r) (Star r) \<union> (Timess (pder c r) (Star r))"
 
   295     also have "\<dots> \<subseteq> Timess (pders_lang (Suf (s @ [c])) r) (Star r) \<union> (Timess (pder c r) (Star r))"
 
   247       by (auto simp add: Suf_snoc pders_lang_snoc)
 
   296       by (simp only: Suf_snoc pders_lang_snoc pders_lang_union)
 
       
   297          (auto simp add: pders_lang_def)
 
   248     also have "\<dots> = Timess (pders_lang (Suf (s @ [c])) r) (Star r)"
 
   298     also have "\<dots> = Timess (pders_lang (Suf (s @ [c])) r) (Star r)"
 
   249       by (auto simp add: Suf_snoc Suf_Union pders_snoc)
 
   299       by (auto simp add: Suf_snoc Suf_Union pders_snoc pders_lang_def)
 
   250     finally have ?case .
 
   300     finally have ?case .
 
   251   }
 
   301   }
 
   252   moreover
 
   302   moreover
 
   253   { assume asm: "s = []"
 
   303   { assume asm: "s = []"
 
   254     then have ?case
 
   304     then have ?case
 
   255       apply (auto simp add: pders_snoc Suf_def)
 
   305       apply (auto simp add: pders_lang_def pders_snoc Suf_def)
 
   256       apply(rule_tac x = "[c]" in exI)
 
   306       apply(rule_tac x = "[c]" in exI)
 
   257       apply(auto)
 
   307       apply(auto)
 
   258       done
 
   308       done
 
   259   }
 
   309   }
 
   260   ultimately show ?case by blast
 
   310   ultimately show ?case by blast
 
   261 qed (simp)
 
   311 qed (simp)
 
   262 
   312 
   263 definition
 
       
   264   "UNIV1 \<equiv> UNIV - {[]}"
 
       
   265 
       
   266 lemma pders_lang_Zero [simp]:
 
       
   267   shows "pders_lang UNIV1 Zero = {Zero}"
 
       
   268 unfolding UNIV1_def by auto
 
       
   269 
       
   270 lemma pders_lang_One [simp]:
 
       
   271   shows "pders_lang UNIV1 One = {Zero}"
 
       
   272 unfolding UNIV1_def by (auto split: if_splits)
 
       
   273 
       
   274 lemma pders_lang_Atom:
 
       
   275   shows "pders_lang UNIV1 (Atom c) \<subseteq> {One, Zero}"
 
       
   276 unfolding UNIV1_def by (auto split: if_splits)
 
       
   277 
       
   278 lemma pders_lang_Plus:
 
       
   279   shows "pders_lang UNIV1 (Plus r1 r2) = pders_lang UNIV1 r1 \<union> pders_lang UNIV1 r2"
 
       
   280 unfolding UNIV1_def by auto
 
       
   281 
       
   282 lemma pders_lang_Times_aux:
 
       
   283   assumes a: "s \<in> UNIV1"
 
       
   284   shows "pders_lang (Suf s) r \<subseteq> pders_lang UNIV1 r"
 
       
   285 using a unfolding UNIV1_def Suf_def by auto
 
       
   286 
       
   287 lemma pders_lang_Times [intro]:
 
       
   288   shows "pders_lang UNIV1 (Times r1 r2) \<subseteq> Timess (pders_lang UNIV1 r1) r2 \<union> pders_lang UNIV1 r2"
 
       
   289 unfolding UNIV1_def
 
       
   290 apply(rule UN_least)
 
       
   291 apply(rule subset_trans)
 
       
   292 apply(rule pders_Times)
 
       
   293 apply(simp)
 
       
   294 apply(rule conjI) 
       
   295 apply(auto)[1]
 
       
   296 apply(rule subset_trans)
 
       
   297 apply(rule pders_lang_Times_aux)
 
       
   298 apply(auto simp add: UNIV1_def)
 
       
   299 done
 
       
   300 
       
   301 lemma pders_lang_Star [intro]:
 
   313 lemma pders_lang_Star [intro]:
 
   302   shows "pders_lang UNIV1 (Star r) \<subseteq> Timess (pders_lang UNIV1 r) (Star r)"
 
   314   shows "pders_lang UNIV1 (Star r) \<subseteq> Timess (pders_lang UNIV1 r) (Star r)"
 
   303 unfolding UNIV1_def
 
   315 apply(rule pders_lang_subsetI)
 
   304 apply(rule UN_least)
 
       
   305 apply(rule subset_trans)
 
   316 apply(rule subset_trans)
 
   306 apply(rule pders_Star)
 
   317 apply(rule pders_Star)
 
   307 apply(simp)
 
   318 apply(simp add: UNIV1_def)
 
   308 apply(simp add: Suf_def)
 
   319 apply(simp add: UNIV1_def Suf_def)
 
   309 apply(auto)
 
   320 apply(auto simp add: pders_lang_def)
 
   310 done
 
   321 done
 
   311 
   322 
   312 lemma finite_Timess:
 
   323 lemma finite_Timess [simp]:
 
   313   assumes a: "finite A"
 
   324   assumes a: "finite A"
 
   314   shows "finite (Timess A r)"
 
   325   shows "finite (Timess A r)"
 
   315 using a by auto
 
   326 using a by auto
 
   316 
   327 
   317 lemma finite_pders_lang_UNIV1:
 
   328 lemma finite_pders_lang_UNIV1:
 
   318   shows "finite (pders_lang UNIV1 r)"
 
   329   shows "finite (pders_lang UNIV1 r)"
 
   319 apply(induct r)
 
   330 apply(induct r)
 
   320 apply(simp)
 
   331 apply(simp)
 
   321 apply(simp only: pders_lang_One)
 
   332 apply(simp)
 
   322 apply(simp)
 
   333 apply(rule finite_subset[OF pders_lang_Atom])
 
   323 apply(rule finite_subset)
 
   334 apply(simp)
 
   324 apply(rule pders_lang_Atom)
 
   335 apply(simp)
 
   325 apply(simp)
 
   336 apply(rule finite_subset[OF pders_lang_Times])
 
   326 apply(simp only: pders_lang_Plus)
 
   337 apply(simp)
 
   327 apply(simp)
 
   338 apply(rule finite_subset[OF pders_lang_Star])
 
   328 apply(rule finite_subset)
 
   339 apply(simp)
 
   329 apply(rule pders_lang_Times)
 
       
   330 apply(simp only: finite_Timess finite_Un)
 
       
   331 apply(simp)
 
       
   332 apply(rule finite_subset)
 
       
   333 apply(rule pders_lang_Star)
 
       
   334 apply(simp only: finite_Timess)
 
       
   335 done
 
   340 done
 
   336     
   341     
   337 lemma pders_lang_UNIV_UNIV1:
 
   342 lemma pders_lang_UNIV:
 
   338   shows "pders_lang UNIV r = pders [] r \<union> pders_lang UNIV1 r"
 
   343   shows "pders_lang UNIV r = pders [] r \<union> pders_lang UNIV1 r"
 
   339 unfolding UNIV1_def
 
   344 unfolding UNIV1_def pders_lang_def
 
   340 apply(auto)
 
   345 by blast
 
   341 apply(rule_tac x="[]" in exI)
 
       
   342 apply(simp)
 
       
   343 done
 
       
   344 
   346 
   345 lemma finite_pders_lang_UNIV:
 
   347 lemma finite_pders_lang_UNIV:
 
   346   shows "finite (pders_lang UNIV r)"
 
   348   shows "finite (pders_lang UNIV r)"
 
   347 unfolding pders_lang_UNIV_UNIV1
 
   349 unfolding pders_lang_UNIV
 
   348 by (simp add: finite_pders_lang_UNIV1)
 
   350 by (simp add: finite_pders_lang_UNIV1)
 
   349 
   351 
   350 lemma finite_pders_lang:
 
   352 lemma finite_pders_lang:
 
   351   shows "finite (pders_lang A r)"
 
   353   shows "finite (pders_lang A r)"
 
   352 apply(rule rev_finite_subset)
 
   354 apply(rule rev_finite_subset)
 
   353 apply(rule_tac r="r" in finite_pders_lang_UNIV)
 
   355 apply(rule_tac r="r" in finite_pders_lang_UNIV)
 
   354 apply(auto)
 
   356 apply(auto simp add: pders_lang_def)
 
   355 done
 
   357 done
 
   356 
       
   357 lemma finite_pders:
 
       
   358   shows "finite (pders s r)"
 
       
   359 using finite_pders_lang[where A="{s}" and r="r"]
 
       
   360 by simp
 
       
   361 
       
   362 lemma finite_pders2:
 
       
   363   shows "finite {pders s r | s. s \<in> A}"
 
       
   364 proof -
 
       
   365   have "{pders s r | s. s \<in> A} \<subseteq> Pow (pders_lang A r)" by auto
 
       
   366   moreover
 
       
   367   have "finite (Pow (pders_lang A r))"
 
       
   368     using finite_pders_lang by simp
 
       
   369   ultimately 
       
   370   show "finite {pders s r | s. s \<in> A}"
 
       
   371     by(rule finite_subset)
 
       
   372 qed
 
       
   373 
       
   374 
   358 
   375 text {* Relating the Myhill-Nerode relation with left-quotients. *}
 
   359 text {* Relating the Myhill-Nerode relation with left-quotients. *}
 
   376 
   360 
   377 lemma MN_Rel_Ders:
 
   361 lemma MN_Rel_Ders:
 
   378   shows "x \<approx>A y \<longleftrightarrow> Ders x A = Ders y A"
 
   362   shows "x \<approx>A y \<longleftrightarrow> Ders x A = Ders y A"
 
   388   fixes r::"'a rexp"
 
   372   fixes r::"'a rexp"
 
   389   shows "finite (UNIV // \<approx>(lang r))"
 
   373   shows "finite (UNIV // \<approx>(lang r))"
 
   390 proof -
 
   374 proof -
 
   391   have "finite (UNIV // =(\<lambda>x. pders x r)=)"
 
   375   have "finite (UNIV // =(\<lambda>x. pders x r)=)"
 
   392   proof - 
   376   proof - 
   393     have "range (\<lambda>x. pders x r) = {pders s r | s. s \<in> UNIV}" by auto
 
   377     have "range (\<lambda>x. pders x r) \<subseteq> Pow (pders_lang UNIV r)"
 
       
   378       unfolding pders_lang_def by auto
 
   394     moreover 
   379     moreover 
   395     have "finite {pders s r | s. s \<in> UNIV}" by (rule finite_pders2)
 
   380     have "finite (Pow (pders_lang UNIV r))" by (simp add: finite_pders_lang)
 
   396     ultimately
 
   381     ultimately
 
   397     have "finite (range (\<lambda>x. pders x r))"
 
   382     have "finite (range (\<lambda>x. pders x r))"
 
   398       by simp
 
   383       by (simp add: finite_subset)
 
   399     then show "finite (UNIV // =(\<lambda>x. pders x r)=)" 
   384     then show "finite (UNIV // =(\<lambda>x. pders x r)=)" 
   400       by (rule finite_eq_tag_rel)
 
   385       by (rule finite_eq_tag_rel)
 
   401   qed
 
   386   qed
 
   402   moreover 
   387   moreover 
   403   have "=(\<lambda>x. pders x r)= \<subseteq> \<approx>(lang r)"
 
   388   have "=(\<lambda>x. pders x r)= \<subseteq> \<approx>(lang r)"
regexp