1 theory Myhill_2 |
1 theory Myhill_2 |
2 imports Myhill_1 Prefix_subtract |
2 imports Myhill_1 Prefix_subtract |
3 "~~/src/HOL/Library/List_Prefix" |
3 "~~/src/HOL/Library/List_Prefix" |
4 begin |
4 begin |
5 |
5 |
6 section {* Direction @{text "regular language \<Rightarrow>finite partition"} *} |
6 section {* Direction @{text "regular language \<Rightarrow> finite partition"} *} |
7 |
7 |
8 definition |
8 definition |
9 str_eq :: "string \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> bool" ("_ \<approx>_ _") |
9 str_eq :: "string \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> bool" ("_ \<approx>_ _") |
10 where |
10 where |
11 "x \<approx>A y \<equiv> (x, y) \<in> (\<approx>A)" |
11 "x \<approx>A y \<equiv> (x, y) \<in> (\<approx>A)" |
12 |
12 |
|
13 lemma str_eq_def2: |
|
14 shows "\<approx>A = {(x, y) | x y. x \<approx>A y}" |
|
15 unfolding str_eq_def |
|
16 by simp |
|
17 |
13 definition |
18 definition |
14 tag_eq_rel :: "(string \<Rightarrow> 'b) \<Rightarrow> (string \<times> string) set" ("=_=") |
19 tag_eq_rel :: "(string \<Rightarrow> 'b) \<Rightarrow> (string \<times> string) set" ("=_=") |
15 where |
20 where |
16 "=tag= \<equiv> {(x, y) | x y. tag x = tag y}" |
21 "=tag= \<equiv> {(x, y). tag x = tag y}" |
17 |
22 |
18 lemma finite_eq_tag_rel: |
23 lemma finite_eq_tag_rel: |
19 assumes rng_fnt: "finite (range tag)" |
24 assumes rng_fnt: "finite (range tag)" |
20 shows "finite (UNIV // =tag=)" |
25 shows "finite (UNIV // =tag=)" |
21 proof - |
26 proof - |
214 where |
219 where |
215 "tag_str_SEQ L1 L2 \<equiv> |
220 "tag_str_SEQ L1 L2 \<equiv> |
216 (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa. xa \<le> x \<and> xa \<in> L1}))" |
221 (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa. xa \<le> x \<and> xa \<in> L1}))" |
217 |
222 |
218 lemma Seq_in_cases: |
223 lemma Seq_in_cases: |
219 assumes "x @ z \<in> A ;; B" |
224 assumes "x @ z \<in> A \<cdot> B" |
220 shows "(\<exists> x' \<le> x. x' \<in> A \<and> (x - x') @ z \<in> B) \<or> |
225 shows "(\<exists> x' \<le> x. x' \<in> A \<and> (x - x') @ z \<in> B) \<or> |
221 (\<exists> z' \<le> z. (x @ z') \<in> A \<and> (z - z') \<in> B)" |
226 (\<exists> z' \<le> z. (x @ z') \<in> A \<and> (z - z') \<in> B)" |
222 using assms |
227 using assms |
223 unfolding Seq_def prefix_def |
228 unfolding Seq_def prefix_def |
224 by (auto simp add: append_eq_append_conv2) |
229 by (auto simp add: append_eq_append_conv2) |
225 |
230 |
226 lemma tag_str_SEQ_injI: |
231 lemma tag_str_SEQ_injI: |
227 assumes eq_tag: "tag_str_SEQ A B x = tag_str_SEQ A B y" |
232 assumes eq_tag: "tag_str_SEQ A B x = tag_str_SEQ A B y" |
228 shows "x \<approx>(A ;; B) y" |
233 shows "x \<approx>(A \<cdot> B) y" |
229 proof - |
234 proof - |
230 { fix x y z |
235 { fix x y z |
231 assume xz_in_seq: "x @ z \<in> A ;; B" |
236 assume xz_in_seq: "x @ z \<in> A \<cdot> B" |
232 and tag_xy: "tag_str_SEQ A B x = tag_str_SEQ A B y" |
237 and tag_xy: "tag_str_SEQ A B x = tag_str_SEQ A B y" |
233 have"y @ z \<in> A ;; B" |
238 have"y @ z \<in> A \<cdot> B" |
234 proof - |
239 proof - |
235 { (* first case with x' in A and (x - x') @ z in B *) |
240 { (* first case with x' in A and (x - x') @ z in B *) |
236 fix x' |
241 fix x' |
237 assume h1: "x' \<le> x" and h2: "x' \<in> A" and h3: "(x - x') @ z \<in> B" |
242 assume h1: "x' \<le> x" and h2: "x' \<in> A" and h3: "(x - x') @ z \<in> B" |
238 obtain y' |
243 obtain y' |
257 with h3 have "(y - y') @ z \<in> B" |
262 with h3 have "(y - y') @ z \<in> B" |
258 unfolding str_eq_rel_def str_eq_def by simp |
263 unfolding str_eq_rel_def str_eq_def by simp |
259 with pref_y' y'_in |
264 with pref_y' y'_in |
260 show ?thesis using that by blast |
265 show ?thesis using that by blast |
261 qed |
266 qed |
262 then have "y @ z \<in> A ;; B" by (erule_tac prefixE) (auto simp: Seq_def) |
267 then have "y @ z \<in> A \<cdot> B" by (erule_tac prefixE) (auto simp: Seq_def) |
263 } |
268 } |
264 moreover |
269 moreover |
265 { (* second case with x @ z' in A and z - z' in B *) |
270 { (* second case with x @ z' in A and z - z' in B *) |
266 fix z' |
271 fix z' |
267 assume h1: "z' \<le> z" and h2: "(x @ z') \<in> A" and h3: "z - z' \<in> B" |
272 assume h1: "z' \<le> z" and h2: "(x @ z') \<in> A" and h3: "z - z' \<in> B" |
268 have "\<approx>A `` {x} = \<approx>A `` {y}" |
273 have "\<approx>A `` {x} = \<approx>A `` {y}" |
269 using tag_xy unfolding tag_str_SEQ_def by simp |
274 using tag_xy unfolding tag_str_SEQ_def by simp |
270 with h2 have "y @ z' \<in> A" |
275 with h2 have "y @ z' \<in> A" |
271 unfolding Image_def str_eq_rel_def str_eq_def by auto |
276 unfolding Image_def str_eq_rel_def str_eq_def by auto |
272 with h1 h3 have "y @ z \<in> A ;; B" |
277 with h1 h3 have "y @ z \<in> A \<cdot> B" |
273 unfolding prefix_def Seq_def |
278 unfolding prefix_def Seq_def |
274 by (auto) (metis append_assoc) |
279 by (auto) (metis append_assoc) |
275 } |
280 } |
276 ultimately show "y @ z \<in> A ;; B" |
281 ultimately show "y @ z \<in> A \<cdot> B" |
277 using Seq_in_cases [OF xz_in_seq] by blast |
282 using Seq_in_cases [OF xz_in_seq] by blast |
278 qed |
283 qed |
279 } |
284 } |
280 from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]] |
285 from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]] |
281 show "x \<approx>(A ;; B) y" unfolding str_eq_def str_eq_rel_def by blast |
286 show "x \<approx>(A \<cdot> B) y" unfolding str_eq_def str_eq_rel_def by blast |
282 qed |
287 qed |
283 |
288 |
284 lemma quot_seq_finiteI [intro]: |
289 lemma quot_seq_finiteI [intro]: |
285 fixes L1 L2::"lang" |
290 fixes L1 L2::"lang" |
286 assumes fin1: "finite (UNIV // \<approx>L1)" |
291 assumes fin1: "finite (UNIV // \<approx>L1)" |
287 and fin2: "finite (UNIV // \<approx>L2)" |
292 and fin2: "finite (UNIV // \<approx>L2)" |
288 shows "finite (UNIV // \<approx>(L1 ;; L2))" |
293 shows "finite (UNIV // \<approx>(L1 \<cdot> L2))" |
289 proof (rule_tac tag = "tag_str_SEQ L1 L2" in tag_finite_imageD) |
294 proof (rule_tac tag = "tag_str_SEQ L1 L2" in tag_finite_imageD) |
290 show "\<And>x y. tag_str_SEQ L1 L2 x = tag_str_SEQ L1 L2 y \<Longrightarrow> x \<approx>(L1 ;; L2) y" |
295 show "\<And>x y. tag_str_SEQ L1 L2 x = tag_str_SEQ L1 L2 y \<Longrightarrow> x \<approx>(L1 \<cdot> L2) y" |
291 by (rule tag_str_SEQ_injI) |
296 by (rule tag_str_SEQ_injI) |
292 next |
297 next |
293 have *: "finite ((UNIV // \<approx>L1) \<times> (Pow (UNIV // \<approx>L2)))" |
298 have *: "finite ((UNIV // \<approx>L1) \<times> (Pow (UNIV // \<approx>L2)))" |
294 using fin1 fin2 by auto |
299 using fin1 fin2 by auto |
295 show "finite (range (tag_str_SEQ L1 L2))" |
300 show "finite (range (tag_str_SEQ L1 L2))" |
429 qed |
434 qed |
430 have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" using l_za ls_zb by blast |
435 have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" using l_za ls_zb by blast |
431 with eq_zab show ?thesis by simp |
436 with eq_zab show ?thesis by simp |
432 qed |
437 qed |
433 with h5 h6 show ?thesis |
438 with h5 h6 show ?thesis |
434 by (drule_tac star_intro1) (auto simp:strict_prefix_def elim:prefixE) |
439 by (drule_tac star_intro1) (auto simp:strict_prefix_def elim: prefixE) |
435 qed |
440 qed |
436 } |
441 } |
437 from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]] |
442 from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]] |
438 show ?thesis unfolding str_eq_def str_eq_rel_def by blast |
443 show ?thesis unfolding str_eq_def str_eq_rel_def by blast |
439 qed |
444 qed |
440 |
445 |
441 lemma quot_star_finiteI [intro]: |
446 lemma quot_star_finiteI [intro]: |
442 assumes finite1: "finite (UNIV // \<approx>L1)" |
447 assumes finite1: "finite (UNIV // \<approx>A)" |
443 shows "finite (UNIV // \<approx>(L1\<star>))" |
448 shows "finite (UNIV // \<approx>(A\<star>))" |
444 proof (rule_tac tag = "tag_str_STAR L1" in tag_finite_imageD) |
449 proof (rule_tac tag = "tag_str_STAR A" in tag_finite_imageD) |
445 show "\<And>x y. tag_str_STAR L1 x = tag_str_STAR L1 y \<Longrightarrow> x \<approx>(L1\<star>) y" |
450 show "\<And>x y. tag_str_STAR A x = tag_str_STAR A y \<Longrightarrow> x \<approx>(A\<star>) y" |
446 by (rule tag_str_STAR_injI) |
451 by (rule tag_str_STAR_injI) |
447 next |
452 next |
448 have *: "finite (Pow (UNIV // \<approx>L1))" |
453 have *: "finite (Pow (UNIV // \<approx>A))" |
449 using finite1 by auto |
454 using finite1 by auto |
450 show "finite (range (tag_str_STAR L1))" |
455 show "finite (range (tag_str_STAR A))" |
451 unfolding tag_str_STAR_def |
456 unfolding tag_str_STAR_def |
452 apply(rule finite_subset[OF _ *]) |
457 apply(rule finite_subset[OF _ *]) |
453 unfolding quotient_def |
458 unfolding quotient_def |
454 by auto |
459 by auto |
455 qed |
460 qed |
456 |
461 |
457 subsubsection{* The conclusion *} |
462 subsubsection{* The conclusion *} |
458 |
463 |
459 lemma Myhill_Nerode2: |
464 lemma Myhill_Nerode2: |
460 fixes r::"rexp" |
465 shows "finite (UNIV // \<approx>(L_rexp r))" |
461 shows "finite (UNIV // \<approx>(L r))" |
|
462 by (induct r) (auto) |
466 by (induct r) (auto) |
463 |
467 |
464 |
468 |
465 theorem Myhill_Nerode: |
469 theorem Myhill_Nerode: |
466 shows "(\<exists>r::rexp. A = L r) \<longleftrightarrow> finite (UNIV // \<approx>A)" |
470 shows "(\<exists>r. A = L_rexp r) \<longleftrightarrow> finite (UNIV // \<approx>A)" |
467 using Myhill_Nerode1 Myhill_Nerode2 by auto |
471 using Myhill_Nerode1 Myhill_Nerode2 by auto |
468 |
472 |
469 end |
473 end |