|
1 theory Myhill |
|
2 imports Myhill_2 "Derivatives" |
|
3 begin |
|
4 |
|
5 section {* The theorem *} |
|
6 |
|
7 theorem Myhill_Nerode: |
|
8 fixes A::"('a::finite) lang" |
|
9 shows "(\<exists>r. A = lang r) \<longleftrightarrow> finite (UNIV // \<approx>A)" |
|
10 using Myhill_Nerode1 Myhill_Nerode2 by auto |
|
11 |
|
12 |
|
13 subsection {* Second direction proved using partial derivatives *} |
|
14 |
|
15 text {* |
|
16 An alternaive proof using the notion of partial derivatives for regular |
|
17 expressions due to Antimirov \cite{Antimirov95}. |
|
18 *} |
|
19 |
|
20 lemma MN_Rel_Derivs: |
|
21 shows "x \<approx>A y \<longleftrightarrow> Derivs x A = Derivs y A" |
|
22 unfolding Derivs_def str_eq_def |
|
23 by auto |
|
24 |
|
25 lemma Myhill_Nerode3: |
|
26 fixes r::"'a rexp" |
|
27 shows "finite (UNIV // \<approx>(lang r))" |
|
28 proof - |
|
29 have "finite (UNIV // =(\<lambda>x. pderivs x r)=)" |
|
30 proof - |
|
31 have "range (\<lambda>x. pderivs x r) \<subseteq> Pow (pderivs_lang UNIV r)" |
|
32 unfolding pderivs_lang_def by auto |
|
33 moreover |
|
34 have "finite (Pow (pderivs_lang UNIV r))" by (simp add: finite_pderivs_lang) |
|
35 ultimately |
|
36 have "finite (range (\<lambda>x. pderivs x r))" |
|
37 by (simp add: finite_subset) |
|
38 then show "finite (UNIV // =(\<lambda>x. pderivs x r)=)" |
|
39 by (rule finite_eq_tag_rel) |
|
40 qed |
|
41 moreover |
|
42 have "=(\<lambda>x. pderivs x r)= \<subseteq> \<approx>(lang r)" |
|
43 unfolding tag_eq_def |
|
44 by (auto simp add: MN_Rel_Derivs Derivs_pderivs) |
|
45 moreover |
|
46 have "equiv UNIV =(\<lambda>x. pderivs x r)=" |
|
47 and "equiv UNIV (\<approx>(lang r))" |
|
48 unfolding equiv_def refl_on_def sym_def trans_def |
|
49 unfolding tag_eq_def str_eq_def |
|
50 by auto |
|
51 ultimately show "finite (UNIV // \<approx>(lang r))" |
|
52 by (rule refined_partition_finite) |
|
53 qed |
|
54 |
|
55 end |