equal
deleted
inserted
replaced
415 |
415 |
416 text {* Relating the Myhill-Nerode relation with left-quotients. *} |
416 text {* Relating the Myhill-Nerode relation with left-quotients. *} |
417 |
417 |
418 lemma MN_Rel_Ders: |
418 lemma MN_Rel_Ders: |
419 shows "x \<approx>A y \<longleftrightarrow> Ders x A = Ders y A" |
419 shows "x \<approx>A y \<longleftrightarrow> Ders x A = Ders y A" |
420 unfolding Ders_def str_eq_def str_eq_rel_def |
420 unfolding Ders_def str_eq_def |
421 by auto |
421 by auto |
422 |
422 |
423 subsection {* |
423 subsection {* |
424 The second direction of the Myhill-Nerode theorem using |
424 The second direction of the Myhill-Nerode theorem using |
425 partial derivatives. |
425 partial derivatives. |
440 then show "finite (UNIV // =(\<lambda>x. pders x r)=)" |
440 then show "finite (UNIV // =(\<lambda>x. pders x r)=)" |
441 by (rule finite_eq_tag_rel) |
441 by (rule finite_eq_tag_rel) |
442 qed |
442 qed |
443 moreover |
443 moreover |
444 have "=(\<lambda>x. pders x r)= \<subseteq> \<approx>(lang r)" |
444 have "=(\<lambda>x. pders x r)= \<subseteq> \<approx>(lang r)" |
445 unfolding tag_eq_rel_def |
445 unfolding tag_eq_def |
446 unfolding str_eq_def2 |
446 by (auto simp add: MN_Rel_Ders Ders_pders) |
447 unfolding MN_Rel_Ders |
|
448 unfolding Ders_pders |
|
449 by auto |
|
450 moreover |
447 moreover |
451 have "equiv UNIV =(\<lambda>x. pders x r)=" |
448 have "equiv UNIV =(\<lambda>x. pders x r)=" |
452 unfolding equiv_def refl_on_def sym_def trans_def |
449 unfolding equiv_def refl_on_def sym_def trans_def |
453 unfolding tag_eq_rel_def |
450 unfolding tag_eq_def |
454 by auto |
451 by auto |
455 moreover |
452 moreover |
456 have "equiv UNIV (\<approx>(lang r))" |
453 have "equiv UNIV (\<approx>(lang r))" |
457 unfolding equiv_def refl_on_def sym_def trans_def |
454 unfolding equiv_def refl_on_def sym_def trans_def |
458 unfolding str_eq_rel_def |
455 unfolding str_eq_def |
459 by auto |
456 by auto |
460 ultimately show "finite (UNIV // \<approx>(lang r))" |
457 ultimately show "finite (UNIV // \<approx>(lang r))" |
461 by (rule refined_partition_finite) |
458 by (rule refined_partition_finite) |
462 qed |
459 qed |
463 |
460 |