equal
deleted
inserted
replaced
1 theory Myhill_2 |
1 theory Myhill_2 |
2 imports Myhill_1 |
2 imports Myhill_1 "~~/src/HOL/Library/List_Prefix" |
3 "~~/src/HOL/Library/List_Prefix" |
|
4 begin |
3 begin |
5 |
4 |
6 section {* Direction @{text "regular language \<Rightarrow> finite partition"} *} |
5 section {* Second direction of MN: @{text "regular language \<Rightarrow> finite partition"} *} |
|
6 |
|
7 subsection {* Tagging functions *} |
7 |
8 |
8 definition |
9 definition |
9 tag_eq :: "('a list \<Rightarrow> 'b) \<Rightarrow> ('a list \<times> 'a list) set" ("=_=") |
10 tag_eq :: "('a list \<Rightarrow> 'b) \<Rightarrow> ('a list \<times> 'a list) set" ("=_=") |
10 where |
11 where |
11 "=tag= \<equiv> {(x, y). tag x = tag y}" |
12 "=tag= \<equiv> {(x, y). tag x = tag y}" |
113 unfolding equiv_def str_eq_def tag_eq_def refl_on_def sym_def trans_def |
114 unfolding equiv_def str_eq_def tag_eq_def refl_on_def sym_def trans_def |
114 by auto |
115 by auto |
115 qed |
116 qed |
116 |
117 |
117 |
118 |
118 subsection {* The proof *} |
119 subsection {* Base cases: @{const Zero}, @{const One} and @{const Atom} *} |
119 |
|
120 subsubsection {* The base case for @{const "Zero"} *} |
|
121 |
120 |
122 lemma quot_zero_eq: |
121 lemma quot_zero_eq: |
123 shows "UNIV // \<approx>{} = {UNIV}" |
122 shows "UNIV // \<approx>{} = {UNIV}" |
124 unfolding quotient_def Image_def str_eq_def by auto |
123 unfolding quotient_def Image_def str_eq_def by auto |
125 |
124 |
126 lemma quot_zero_finiteI [intro]: |
125 lemma quot_zero_finiteI [intro]: |
127 shows "finite (UNIV // \<approx>{})" |
126 shows "finite (UNIV // \<approx>{})" |
128 unfolding quot_zero_eq by simp |
127 unfolding quot_zero_eq by simp |
129 |
128 |
130 |
|
131 subsubsection {* The base case for @{const "One"} *} |
|
132 |
129 |
133 lemma quot_one_subset: |
130 lemma quot_one_subset: |
134 shows "UNIV // \<approx>{[]} \<subseteq> {{[]}, UNIV - {[]}}" |
131 shows "UNIV // \<approx>{[]} \<subseteq> {{[]}, UNIV - {[]}}" |
135 proof |
132 proof |
136 fix x |
133 fix x |
149 |
146 |
150 lemma quot_one_finiteI [intro]: |
147 lemma quot_one_finiteI [intro]: |
151 shows "finite (UNIV // \<approx>{[]})" |
148 shows "finite (UNIV // \<approx>{[]})" |
152 by (rule finite_subset[OF quot_one_subset]) (simp) |
149 by (rule finite_subset[OF quot_one_subset]) (simp) |
153 |
150 |
154 |
|
155 subsubsection {* The base case for @{const "Atom"} *} |
|
156 |
151 |
157 lemma quot_atom_subset: |
152 lemma quot_atom_subset: |
158 "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}" |
153 "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}" |
159 proof |
154 proof |
160 fix x |
155 fix x |
183 lemma quot_atom_finiteI [intro]: |
178 lemma quot_atom_finiteI [intro]: |
184 shows "finite (UNIV // \<approx>{[c]})" |
179 shows "finite (UNIV // \<approx>{[c]})" |
185 by (rule finite_subset[OF quot_atom_subset]) (simp) |
180 by (rule finite_subset[OF quot_atom_subset]) (simp) |
186 |
181 |
187 |
182 |
188 subsubsection {* The inductive case for @{const Plus} *} |
183 subsection {* Case for @{const Plus} *} |
189 |
184 |
190 definition |
185 definition |
191 tag_Plus :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang)" |
186 tag_Plus :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang)" |
192 where |
187 where |
193 "tag_Plus A B \<equiv> \<lambda>x. (\<approx>A `` {x}, \<approx>B `` {x})" |
188 "tag_Plus A B \<equiv> \<lambda>x. (\<approx>A `` {x}, \<approx>B `` {x})" |
206 show "=tag_Plus A B= \<subseteq> \<approx>(A \<union> B)" |
201 show "=tag_Plus A B= \<subseteq> \<approx>(A \<union> B)" |
207 unfolding tag_eq_def tag_Plus_def str_eq_def by auto |
202 unfolding tag_eq_def tag_Plus_def str_eq_def by auto |
208 qed |
203 qed |
209 |
204 |
210 |
205 |
211 subsubsection {* The inductive case for @{text "Times"} *} |
206 subsection {* Case for @{text "Times"} *} |
212 |
207 |
213 definition |
208 definition |
214 "Partitions x \<equiv> {(x\<^isub>p, x\<^isub>s). x\<^isub>p @ x\<^isub>s = x}" |
209 "Partitions x \<equiv> {(x\<^isub>p, x\<^isub>s). x\<^isub>p @ x\<^isub>s = x}" |
215 |
210 |
216 lemma conc_partitions_elim: |
211 lemma conc_partitions_elim: |
311 unfolding quotient_def |
306 unfolding quotient_def |
312 by auto |
307 by auto |
313 qed |
308 qed |
314 |
309 |
315 |
310 |
316 subsubsection {* The inductive case for @{const "Star"} *} |
311 subsection {* Case for @{const "Star"} *} |
317 |
312 |
318 lemma star_partitions_elim: |
313 lemma star_partitions_elim: |
319 assumes "x @ z \<in> A\<star>" "x \<noteq> []" |
314 assumes "x @ z \<in> A\<star>" "x \<noteq> []" |
320 shows "\<exists>(u, v) \<in> Partitions (x @ z). u < x \<and> u \<in> A\<star> \<and> v \<in> A\<star>" |
315 shows "\<exists>(u, v) \<in> Partitions (x @ z). u < x \<and> u \<in> A\<star> \<and> v \<in> A\<star>" |
321 proof - |
316 proof - |
461 unfolding tag_Star_def |
456 unfolding tag_Star_def |
462 by (rule finite_subset[OF _ *]) |
457 by (rule finite_subset[OF _ *]) |
463 (auto simp add: quotient_def) |
458 (auto simp add: quotient_def) |
464 qed |
459 qed |
465 |
460 |
466 subsubsection{* The conclusion *} |
461 subsection {* The conclusion of the second direction *} |
467 |
462 |
468 lemma Myhill_Nerode2: |
463 lemma Myhill_Nerode2: |
469 fixes r::"'a rexp" |
464 fixes r::"'a rexp" |
470 shows "finite (UNIV // \<approx>(lang r))" |
465 shows "finite (UNIV // \<approx>(lang r))" |
471 by (induct r) (auto) |
466 by (induct r) (auto) |
472 |
467 |
473 theorem Myhill_Nerode: |
|
474 fixes A::"('a::finite) lang" |
|
475 shows "(\<exists>r. A = lang r) \<longleftrightarrow> finite (UNIV // \<approx>A)" |
|
476 using Myhill_Nerode1 Myhill_Nerode2 by auto |
|
477 |
|
478 end |
468 end |