415 lemma finite_pders: |
416 lemma finite_pders: |
416 shows "finite (pders s r)" |
417 shows "finite (pders s r)" |
417 using finite_pders_set[where A="{s}" and r="r"] |
418 using finite_pders_set[where A="{s}" and r="r"] |
418 by simp |
419 by simp |
419 |
420 |
|
421 |
|
422 lemma test: |
|
423 shows "pders_set A r = (\<Union> {pders s r | s. s \<in> A})" |
|
424 by auto |
|
425 |
|
426 lemma finite_pow_pders: |
|
427 shows "finite (Pow (\<Union> {pders s r | s. s \<in> A}))" |
|
428 using finite_pders_set |
|
429 by (simp add: test) |
|
430 |
|
431 lemma test2: |
|
432 shows "{pders s r | s. s \<in> A} \<subseteq> Pow (\<Union> {pders s r | s. s \<in> A})" |
|
433 by auto |
|
434 |
|
435 lemma test3: |
|
436 shows "finite ({pders s r | s. s \<in> A})" |
|
437 apply(rule finite_subset) |
|
438 apply(rule test2) |
|
439 apply(rule finite_pow_pders) |
|
440 done |
|
441 |
|
442 lemma Myhill_Nerode_aux: |
|
443 fixes r::"rexp" |
|
444 shows "finite (UNIV // =(\<lambda>x. pders x r)=)" |
|
445 apply(rule finite_eq_tag_rel) |
|
446 apply(rule rev_finite_subset) |
|
447 apply(rule test3) |
|
448 apply(auto) |
|
449 done |
|
450 |
|
451 lemma Myhill_Nerode3: |
|
452 fixes r::"rexp" |
|
453 shows "finite (UNIV // \<approx>(L r))" |
|
454 apply(rule refined_partition_finite) |
|
455 apply(rule Myhill_Nerode_aux[where r="r"]) |
|
456 apply(simp add: tag_eq_rel_def) |
|
457 apply(auto)[1] |
|
458 unfolding str_eq_def[symmetric] |
|
459 unfolding MN_Rel_Ders |
|
460 apply(simp add: Ders_pders) |
|
461 apply(rule equivI) |
|
462 apply(auto simp add: tag_eq_rel_def refl_on_def sym_def trans_def) |
|
463 apply(rule equivI) |
|
464 apply(auto simp add: str_eq_rel_def refl_on_def sym_def trans_def) |
|
465 done |
|
466 |
|
467 |
|
468 section {* Closure under Left-Quotients *} |
|
469 |
420 lemma closure_left_quotient: |
470 lemma closure_left_quotient: |
421 assumes "regular A" |
471 assumes "regular A" |
422 shows "regular (Ders_set B A)" |
472 shows "regular (Ders_set B A)" |
423 proof - |
473 proof - |
424 from assms obtain r::rexp where eq: "L r = A" by auto |
474 from assms obtain r::rexp where eq: "L r = A" by auto |
431 by simp |
481 by simp |
432 then show "regular (Ders_set B A)" by auto |
482 then show "regular (Ders_set B A)" by auto |
433 qed |
483 qed |
434 |
484 |
435 |
485 |
|
486 section {* Relating standard and partial derivations *} |
|
487 |
|
488 lemma |
|
489 shows "(\<Union> L ` (pder c r)) = L (der c r)" |
|
490 unfolding Der_der[symmetric] Der_pder by simp |
|
491 |
|
492 lemma |
|
493 shows "(\<Union> L ` (pders s r)) = L (ders s r)" |
|
494 unfolding Ders_ders[symmetric] Ders_pders by simp |
|
495 |
|
496 |
|
497 section {* attempt to prove MN *} |
|
498 (* |
|
499 lemma Myhill_Nerode3: |
|
500 fixes r::"rexp" |
|
501 shows "finite (UNIV // =(\<lambda>x. pders x r)=)" |
|
502 apply(rule finite_eq_tag_rel) |
|
503 apply(rule finite_pders_set) |
|
504 apply(simp add: Range_def) |
|
505 unfolding Quotien_def |
|
506 by (induct r) (auto) |
|
507 *) |
|
508 |
436 fun |
509 fun |
437 width :: "rexp \<Rightarrow> nat" |
510 width :: "rexp \<Rightarrow> nat" |
438 where |
511 where |
439 "width (NULL) = 0" |
512 "width (NULL) = 0" |
440 | "width (EMPTY) = 0" |
513 | "width (EMPTY) = 0" |