equal
deleted
inserted
replaced
|
1 header "Derivatives of regular expressions" |
|
2 |
|
3 (* Author: Christian Urban *) |
|
4 |
1 theory Derivatives |
5 theory Derivatives |
2 imports Regular_Exp |
6 imports Regular_Exp |
3 begin |
7 begin |
4 |
|
5 section {* Leftquotients, Derivatives and Partial Derivatives *} |
|
6 |
8 |
7 text{* This theory is based on work by Brozowski \cite{Brzozowski64} and Antimirov \cite{Antimirov95}. *} |
9 text{* This theory is based on work by Brozowski \cite{Brzozowski64} and Antimirov \cite{Antimirov95}. *} |
8 |
10 |
9 subsection {* Left-Quotients of languages *} |
11 subsection {* Left-Quotients of languages *} |
10 |
12 |
67 shows "Derivs [] A = A" |
69 shows "Derivs [] A = A" |
68 and "Derivs (c # s) A = Derivs s (Deriv c A)" |
70 and "Derivs (c # s) A = Derivs s (Deriv c A)" |
69 and "Derivs (s1 @ s2) A = Derivs s2 (Derivs s1 A)" |
71 and "Derivs (s1 @ s2) A = Derivs s2 (Derivs s1 A)" |
70 unfolding Derivs_def Deriv_def by auto |
72 unfolding Derivs_def Deriv_def by auto |
71 |
73 |
72 (* |
74 |
73 lemma Deriv_insert_eps[simp]: |
75 subsection {* Brozowski's derivatives of regular expressions *} |
74 "Deriv a (insert [] A) = Deriv a A" |
|
75 by (auto simp: Deriv_def) |
|
76 *) |
|
77 |
|
78 |
|
79 |
|
80 subsection {* Brozowsky's derivatives of regular expressions *} |
|
81 |
76 |
82 fun |
77 fun |
83 nullable :: "'a rexp \<Rightarrow> bool" |
78 nullable :: "'a rexp \<Rightarrow> bool" |
84 where |
79 where |
85 "nullable (Zero) = False" |
80 "nullable (Zero) = False" |
381 lemma finite_pderivs_lang: |
376 lemma finite_pderivs_lang: |
382 shows "finite (pderivs_lang A r)" |
377 shows "finite (pderivs_lang A r)" |
383 by (metis finite_pderivs_lang_UNIV pderivs_lang_subset rev_finite_subset subset_UNIV) |
378 by (metis finite_pderivs_lang_UNIV pderivs_lang_subset rev_finite_subset subset_UNIV) |
384 |
379 |
385 |
380 |
|
381 subsection {* A regular expression matcher based on Brozowski's derivatives *} |
|
382 |
|
383 fun |
|
384 matcher :: "'a rexp \<Rightarrow> 'a list \<Rightarrow> bool" |
|
385 where |
|
386 "matcher r s = nullable (derivs s r)" |
|
387 |
|
388 lemma matcher_correctness: |
|
389 shows "matcher r s \<longleftrightarrow> s \<in> lang r" |
|
390 by (induct s arbitrary: r) |
|
391 (simp_all add: nullable_iff Deriv_deriv[symmetric] Deriv_def) |
|
392 |
|
393 |
386 end |
394 end |