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 190 b73478aaf33e
parent 187 9f46a9571e37
child 191 f6a603be52d6
equal deleted inserted replaced
189:48b452a2d4df 190:b73478aaf33e 
   171   finally show "Ders (c # s) (lang r) = \<Union> lang ` pders (c # s) r" .
 
   171   finally show "Ders (c # s) (lang r) = \<Union> lang ` pders (c # s) r" .
 
   172 qed (simp add: Ders_def)
 
   172 qed (simp add: Ders_def)
 
   173 
   173 
   174 subsection {* Relating derivatives and partial derivatives *}
 
   174 subsection {* Relating derivatives and partial derivatives *}
 
   175 
   175 
   176 lemma
 
   176 lemma der_pder:
 
   177   shows "(\<Union> lang ` (pder c r)) = lang (der c r)"
 
   177   shows "(\<Union> lang ` (pder c r)) = lang (der c r)"
 
   178 unfolding Der_der[symmetric] Der_pder by simp
 
   178 unfolding Der_der[symmetric] Der_pder by simp
 
   179 
   179 
   180 lemma
 
   180 lemma ders_pders:
 
   181   shows "(\<Union> lang ` (pders s r)) = lang (ders s r)"
 
   181   shows "(\<Union> lang ` (pders s r)) = lang (ders s r)"
 
   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 abbreviation
 
   188   "pders_set 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 text {* Non-empty suffixes of a string *}
 
   191 
   191 
   192 definition
 
   192 definition
 
   193   "Suf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}"
 
   193   "Suf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}"
 
   199 
   199 
   200 lemma Suf_Union:
 
   200 lemma Suf_Union:
 
   201   shows "(\<Union>v \<in> Suf s \<cdot> {[c]}. f v) = (\<Union>v \<in> Suf s. f (v @ [c]))"
 
   201   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)
 
   202 by (auto simp add: conc_def)
 
   203 
   203 
   204 lemma pders_set_snoc:
 
   204 lemma pders_lang_snoc:
 
   205   shows "pders_set (Suf s \<cdot> {[c]}) r = (pder_set c (pders_set (Suf s) r))"
 
   205   shows "pders_lang (Suf s \<cdot> {[c]}) r = (pder_set c (pders_lang (Suf s) r))"
 
   206 by (simp add: Suf_Union pders_snoc)
 
   206 by (simp add: Suf_Union pders_snoc)
 
   207 
   207 
   208 lemma pders_Times:
 
   208 lemma pders_Times:
 
   209   shows "pders s (Times r1 r2) \<subseteq> Timess (pders s r1) r2 \<union> (pders_set (Suf s) r2)"
 
   209   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)
 
   210 proof (induct s rule: rev_induct)
 
   211   case (snoc c s)
 
   211   case (snoc c s)
 
   212   have ih: "pders s (Times r1 r2) \<subseteq> Timess (pders s r1) r2 \<union> (pders_set (Suf s) r2)" 
   212   have ih: "pders s (Times r1 r2) \<subseteq> Timess (pders s r1) r2 \<union> (pders_lang (Suf s) r2)" 
   213     by fact
 
   213     by fact
 
   214   have "pders (s @ [c]) (Times r1 r2) = pder_set c (pders s (Times r1 r2))" 
   214   have "pders (s @ [c]) (Times r1 r2) = pder_set c (pders s (Times r1 r2))" 
   215     by (simp add: pders_snoc)
 
   215     by (simp add: pders_snoc)
 
   216   also have "\<dots> \<subseteq> pder_set c (Timess (pders s r1) r2 \<union> (pders_set (Suf s) r2))"
 
   216   also have "\<dots> \<subseteq> pder_set c (Timess (pders s r1) r2 \<union> (pders_lang (Suf s) r2))"
 
   217     using ih by (auto) (blast)
 
   217     using ih by (auto) (blast)
 
   218   also have "\<dots> = pder_set c (Timess (pders s r1) r2) \<union> pder_set c (pders_set (Suf s) r2)"
 
   218   also have "\<dots> = pder_set c (Timess (pders s r1) r2) \<union> pder_set c (pders_lang (Suf s) r2)"
 
   219     by (simp)
 
   219     by (simp)
 
   220   also have "\<dots> = pder_set c (Timess (pders s r1) r2) \<union> pders_set (Suf s \<cdot> {[c]}) r2"
 
   220   also have "\<dots> = pder_set c (Timess (pders s r1) r2) \<union> pders_lang (Suf s \<cdot> {[c]}) r2"
 
   221     by (simp add: pders_set_snoc)
 
   221     by (simp add: pders_lang_snoc)
 
   222   also have "\<dots> \<subseteq> pder_set c (Timess (pders s r1) r2) \<union> pder c r2 \<union> pders_set (Suf s \<cdot> {[c]}) r2"
 
   222   also have "\<dots> \<subseteq> pder_set c (Timess (pders s r1) r2) \<union> pder c r2 \<union> pders_lang (Suf s \<cdot> {[c]}) r2"
 
   223     by auto
 
   223     by auto
 
   224   also have "\<dots> \<subseteq> Timess (pders (s @ [c]) r1) r2 \<union> pder c r2 \<union> pders_set (Suf s \<cdot> {[c]}) r2"
 
   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"
 
   225     by (auto simp add: if_splits pders_snoc) (blast)
 
   225     by (auto simp add: if_splits) (blast)
 
   226   also have "\<dots> = Timess (pders (s @ [c]) r1) r2 \<union> pders_set (Suf (s @ [c])) r2"
 
   226   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)
 
       
   228   also have "\<dots> \<subseteq> Timess (pders (s @ [c]) r1) r2 \<union> pders_lang (Suf (s @ [c])) r2"
 
   227     by (auto simp add: Suf_snoc)  
   229     by (auto simp add: Suf_snoc)  
   228   finally show ?case .
 
   230   finally show ?case .
 
   229 qed (simp) 
   231 qed (simp) 
   230 
   232 
   231 
       
   232 lemma pders_Star:
 
   233 lemma pders_Star:
 
   233   assumes a: "s \<noteq> []"
 
   234   assumes a: "s \<noteq> []"
 
   234   shows "pders s (Star r) \<subseteq> (\<Union>v \<in> Suf s. Timess (pders v r) (Star r))"
 
   235   shows "pders s (Star r) \<subseteq> Timess (pders_lang (Suf s) r) (Star r)"
 
   235 using a
 
   236 using a
 
   236 proof (induct s rule: rev_induct)
 
   237 proof (induct s rule: rev_induct)
 
   237   case (snoc c s)
 
   238   case (snoc c s)
 
   238   have ih: "s \<noteq> [] \<Longrightarrow> pders s (Star r) \<subseteq> (\<Union>v\<in>Suf s. Timess (pders v r) (Star r))" by fact
 
   239   have ih: "s \<noteq> [] \<Longrightarrow> pders s (Star r) \<subseteq> Timess (pders_lang (Suf s) r) (Star r)" by fact
 
   239   { assume asm: "s \<noteq> []"
 
   240   { assume asm: "s \<noteq> []"
 
   240     have "pders (s @ [c]) (Star r) = pder_set c (pders s (Star r))" by (simp add: pders_snoc)
 
   241     have "pders (s @ [c]) (Star r) = pder_set c (pders s (Star r))" by (simp add: pders_snoc)
 
   241     also have "\<dots> \<subseteq> (pder_set c (\<Union>v\<in>Suf s. Timess (pders v r) (Star r)))"
 
   242     also have "\<dots> \<subseteq> pder_set c (Timess (pders_lang (Suf s) r) (Star r))"
 
   242       using ih[OF asm] by (auto) (blast)
 
   243       using ih[OF asm] by (auto) (blast)
 
   243     also have "\<dots> = (\<Union>v\<in>Suf s. pder_set c (Timess (pders v r) (Star r)))"
 
   244     also have "\<dots> \<subseteq> Timess (pder_set c (pders_lang (Suf s) r)) (Star r) \<union> pder c (Star r)"
 
   244       by simp
 
   245       by (auto split: if_splits) (blast)+
 
   245     also have "\<dots> \<subseteq> (\<Union>v\<in>Suf s. (Timess (pder_set c (pders v r)) (Star r) \<union> pder c (Star r)))"
 
   246     also have "\<dots> \<subseteq> Timess (pders_lang (Suf (s @ [c])) r) (Star r) \<union> (Timess (pder c r) (Star r))"
 
   246       by (auto split: if_splits) 
   247       by (auto simp add: Suf_snoc pders_lang_snoc)
 
   247     also have "\<dots> = (\<Union>v\<in>Suf s. (Timess (pder_set c (pders v r)) (Star r))) \<union> pder c (Star r)"
 
   248     also have "\<dots> = Timess (pders_lang (Suf (s @ [c])) r) (Star r)"
 
   248       using asm by (auto simp add: Suf_def)
 
       
   249     also have "\<dots> = (\<Union>v\<in>Suf s. (Timess (pders (v @ [c]) r) (Star r))) \<union> (Timess (pder c r) (Star r))"
 
       
   250       by (simp add: pders_snoc)
 
       
   251     also have "\<dots> = (\<Union>v\<in>Suf (s @ [c]). (Timess (pders v r) (Star r)))"
 
       
   252       by (auto simp add: Suf_snoc Suf_Union pders_snoc)
 
   249       by (auto simp add: Suf_snoc Suf_Union pders_snoc)
 
   253     finally have ?case .
 
   250     finally have ?case .
 
   254   }
 
   251   }
 
   255   moreover
 
   252   moreover
 
   256   { assume asm: "s = []"
 
   253   { assume asm: "s = []"
 
   257     then have ?case
 
   254     then have ?case
 
   258       by (auto simp add: pders_snoc Suf_def)
 
   255       apply (auto simp add: pders_snoc Suf_def)
 
       
   256       apply(rule_tac x = "[c]" in exI)
 
       
   257       apply(auto)
 
       
   258       done
 
   259   }
 
   259   }
 
   260   ultimately show ?case by blast
 
   260   ultimately show ?case by blast
 
   261 qed (simp)
 
   261 qed (simp)
 
   262 
   262 
   263 definition
 
   263 definition
 
   264   "UNIV1 \<equiv> UNIV - {[]}"
 
   264   "UNIV1 \<equiv> UNIV - {[]}"
 
   265 
   265 
   266 lemma pders_set_Zero:
 
   266 lemma pders_lang_Zero [simp]:
 
   267   shows "pders_set UNIV1 Zero = {Zero}"
 
   267   shows "pders_lang UNIV1 Zero = {Zero}"
 
   268 unfolding UNIV1_def by auto
 
   268 unfolding UNIV1_def by auto
 
   269 
   269 
   270 lemma pders_set_One:
 
   270 lemma pders_lang_One [simp]:
 
   271   shows "pders_set UNIV1 One = {Zero}"
 
   271   shows "pders_lang UNIV1 One = {Zero}"
 
   272 unfolding UNIV1_def by (auto split: if_splits)
 
   272 unfolding UNIV1_def by (auto split: if_splits)
 
   273 
   273 
   274 lemma pders_set_Atom:
 
   274 lemma pders_lang_Atom:
 
   275   shows "pders_set UNIV1 (Atom c) \<subseteq> {One, Zero}"
 
   275   shows "pders_lang UNIV1 (Atom c) \<subseteq> {One, Zero}"
 
   276 unfolding UNIV1_def by (auto split: if_splits)
 
   276 unfolding UNIV1_def by (auto split: if_splits)
 
   277 
   277 
   278 lemma pders_set_Plus:
 
   278 lemma pders_lang_Plus:
 
   279   shows "pders_set UNIV1 (Plus r1 r2) = pders_set UNIV1 r1 \<union> pders_set UNIV1 r2"
 
   279   shows "pders_lang UNIV1 (Plus r1 r2) = pders_lang UNIV1 r1 \<union> pders_lang UNIV1 r2"
 
   280 unfolding UNIV1_def by auto
 
   280 unfolding UNIV1_def by auto
 
   281 
   281 
   282 lemma pders_set_Times_aux:
 
   282 lemma pders_lang_Times_aux:
 
   283   assumes a: "s \<in> UNIV1"
 
   283   assumes a: "s \<in> UNIV1"
 
   284   shows "pders_set (Suf s) r2 \<subseteq> pders_set UNIV1 r2"
 
   284   shows "pders_lang (Suf s) r \<subseteq> pders_lang UNIV1 r"
 
   285 using a unfolding UNIV1_def Suf_def by (auto)
 
   285 using a unfolding UNIV1_def Suf_def by auto
 
   286 
   286 
   287 lemma pders_set_Times:
 
   287 lemma pders_lang_Times [intro]:
 
   288   shows "pders_set UNIV1 (Times r1 r2) \<subseteq> Timess (pders_set UNIV1 r1) r2 \<union> pders_set UNIV1 r2"
 
   288   shows "pders_lang UNIV1 (Times r1 r2) \<subseteq> Timess (pders_lang UNIV1 r1) r2 \<union> pders_lang UNIV1 r2"
 
   289 unfolding UNIV1_def
 
   289 unfolding UNIV1_def
 
   290 apply(rule UN_least)
 
   290 apply(rule UN_least)
 
   291 apply(rule subset_trans)
 
   291 apply(rule subset_trans)
 
   292 apply(rule pders_Times)
 
   292 apply(rule pders_Times)
 
   293 apply(simp)
 
   293 apply(simp)
 
   294 apply(rule conjI) 
   294 apply(rule conjI) 
   295 apply(auto)[1]
 
   295 apply(auto)[1]
 
   296 apply(rule subset_trans)
 
   296 apply(rule subset_trans)
 
   297 apply(rule pders_set_Times_aux)
 
   297 apply(rule pders_lang_Times_aux)
 
   298 apply(auto simp add: UNIV1_def)
 
   298 apply(auto simp add: UNIV1_def)
 
   299 done
 
   299 done
 
   300 
   300 
   301 lemma pders_set_Star:
 
   301 lemma pders_lang_Star [intro]:
 
   302   shows "pders_set UNIV1 (Star r) \<subseteq> Timess (pders_set UNIV1 r) (Star r)"
 
   302   shows "pders_lang UNIV1 (Star r) \<subseteq> Timess (pders_lang UNIV1 r) (Star r)"
 
   303 unfolding UNIV1_def
 
   303 unfolding UNIV1_def
 
   304 apply(rule UN_least)
 
   304 apply(rule UN_least)
 
   305 apply(rule subset_trans)
 
   305 apply(rule subset_trans)
 
   306 apply(rule pders_Star)
 
   306 apply(rule pders_Star)
 
   307 apply(simp)
 
   307 apply(simp)
 
   310 done
 
   310 done
 
   311 
   311 
   312 lemma finite_Timess:
 
   312 lemma finite_Timess:
 
   313   assumes a: "finite A"
 
   313   assumes a: "finite A"
 
   314   shows "finite (Timess A r)"
 
   314   shows "finite (Timess A r)"
 
   315 using a by (auto)
 
   315 using a by auto
 
   316 
   316 
   317 lemma finite_pders_set_UNIV1:
 
   317 lemma finite_pders_lang_UNIV1:
 
   318   shows "finite (pders_set UNIV1 r)"
 
   318   shows "finite (pders_lang UNIV1 r)"
 
   319 apply(induct r)
 
   319 apply(induct r)
 
   320 apply(simp)
 
   320 apply(simp)
 
   321 apply(simp only: pders_set_One)
 
   321 apply(simp only: pders_lang_One)
 
   322 apply(simp)
 
   322 apply(simp)
 
   323 apply(rule finite_subset)
 
   323 apply(rule finite_subset)
 
   324 apply(rule pders_set_Atom)
 
   324 apply(rule pders_lang_Atom)
 
   325 apply(simp)
 
   325 apply(simp)
 
   326 apply(simp only: pders_set_Plus)
 
   326 apply(simp only: pders_lang_Plus)
 
   327 apply(simp)
 
   327 apply(simp)
 
   328 apply(rule finite_subset)
 
   328 apply(rule finite_subset)
 
   329 apply(rule pders_set_Times)
 
   329 apply(rule pders_lang_Times)
 
   330 apply(simp only: finite_Timess finite_Un)
 
   330 apply(simp only: finite_Timess finite_Un)
 
   331 apply(simp)
 
   331 apply(simp)
 
   332 apply(rule finite_subset)
 
   332 apply(rule finite_subset)
 
   333 apply(rule pders_set_Star)
 
   333 apply(rule pders_lang_Star)
 
   334 apply(simp only: finite_Timess)
 
   334 apply(simp only: finite_Timess)
 
   335 done
 
   335 done
 
   336     
   336     
   337 lemma pders_set_UNIV_UNIV1:
 
   337 lemma pders_lang_UNIV_UNIV1:
 
   338   shows "pders_set UNIV r = pders [] r \<union> pders_set UNIV1 r"
 
   338   shows "pders_lang UNIV r = pders [] r \<union> pders_lang UNIV1 r"
 
   339 unfolding UNIV1_def
 
   339 unfolding UNIV1_def
 
   340 apply(auto)
 
   340 apply(auto)
 
   341 apply(rule_tac x="[]" in exI)
 
   341 apply(rule_tac x="[]" in exI)
 
   342 apply(simp)
 
   342 apply(simp)
 
   343 done
 
   343 done
 
   344 
   344 
   345 lemma finite_pders_set_UNIV:
 
   345 lemma finite_pders_lang_UNIV:
 
   346   shows "finite (pders_set UNIV r)"
 
   346   shows "finite (pders_lang UNIV r)"
 
   347 unfolding pders_set_UNIV_UNIV1
 
   347 unfolding pders_lang_UNIV_UNIV1
 
   348 by (simp add: finite_pders_set_UNIV1)
 
   348 by (simp add: finite_pders_lang_UNIV1)
 
   349 
   349 
   350 lemma finite_pders_set:
 
   350 lemma finite_pders_lang:
 
   351   shows "finite (pders_set A r)"
 
   351   shows "finite (pders_lang A r)"
 
   352 apply(rule rev_finite_subset)
 
   352 apply(rule rev_finite_subset)
 
   353 apply(rule_tac r="r" in finite_pders_set_UNIV)
 
   353 apply(rule_tac r="r" in finite_pders_lang_UNIV)
 
   354 apply(auto)
 
   354 apply(auto)
 
   355 done
 
   355 done
 
   356 
   356 
   357 lemma finite_pders:
 
   357 lemma finite_pders:
 
   358   shows "finite (pders s r)"
 
   358   shows "finite (pders s r)"
 
   359 using finite_pders_set[where A="{s}" and r="r"]
 
   359 using finite_pders_lang[where A="{s}" and r="r"]
 
   360 by simp
 
   360 by simp
 
   361 
   361 
   362 lemma finite_pders2:
 
   362 lemma finite_pders2:
 
   363   shows "finite {pders s r | s. s \<in> A}"
 
   363   shows "finite {pders s r | s. s \<in> A}"
 
   364 proof -
 
   364 proof -
 
   365   have "{pders s r | s. s \<in> A} \<subseteq> Pow (pders_set A r)" by auto
 
   365   have "{pders s r | s. s \<in> A} \<subseteq> Pow (pders_lang A r)" by auto
 
   366   moreover
 
   366   moreover
 
   367   have "finite (Pow (pders_set A r))"
 
   367   have "finite (Pow (pders_lang A r))"
 
   368     using finite_pders_set by simp
 
   368     using finite_pders_lang by simp
 
   369   ultimately 
   369   ultimately 
   370   show "finite {pders s r | s. s \<in> A}"
 
   370   show "finite {pders s r | s. s \<in> A}"
 
   371     by(rule finite_subset)
 
   371     by(rule finite_subset)
 
   372 qed
 
   372 qed
 
   373 
   373 
   403   have "=(\<lambda>x. pders x r)= \<subseteq> \<approx>(lang r)"
 
   403   have "=(\<lambda>x. pders x r)= \<subseteq> \<approx>(lang r)"
 
   404     unfolding tag_eq_def
 
   404     unfolding tag_eq_def
 
   405     by (auto simp add: MN_Rel_Ders Ders_pders)
 
   405     by (auto simp add: MN_Rel_Ders Ders_pders)
 
   406   moreover 
   406   moreover 
   407   have "equiv UNIV =(\<lambda>x. pders x r)="
 
   407   have "equiv UNIV =(\<lambda>x. pders x r)="
 
       
   408   and  "equiv UNIV (\<approx>(lang r))"
 
   408     unfolding equiv_def refl_on_def sym_def trans_def
 
   409     unfolding equiv_def refl_on_def sym_def trans_def
 
   409     unfolding tag_eq_def
 
   410     unfolding tag_eq_def str_eq_def
 
   410     by auto
 
       
   411   moreover
 
       
   412   have "equiv UNIV (\<approx>(lang r))"
 
       
   413     unfolding equiv_def refl_on_def sym_def trans_def
 
       
   414     unfolding str_eq_def
 
       
   415     by auto
 
   411     by auto
 
   416   ultimately show "finite (UNIV // \<approx>(lang r))" 
   412   ultimately show "finite (UNIV // \<approx>(lang r))" 
   417     by (rule refined_partition_finite)
 
   413     by (rule refined_partition_finite)
 
   418 qed
 
   414 qed
 
   419 
   415
regexp