equal
deleted
inserted
replaced
628 -- {* |
628 -- {* |
629 The degenerated case when @{text "x"} is a null string is easy to prove: |
629 The degenerated case when @{text "x"} is a null string is easy to prove: |
630 *} |
630 *} |
631 case True |
631 case True |
632 with tag_xy have "y = []" |
632 with tag_xy have "y = []" |
633 by (auto simp:tag_str_STAR_def strict_prefix_def) |
633 by (auto simp add: tag_str_STAR_def strict_prefix_def) |
634 thus ?thesis using xz_in_star True by simp |
634 thus ?thesis using xz_in_star True by simp |
635 next |
635 next |
636 -- {* The nontrival case: |
636 -- {* The nontrival case: |
637 *} |
637 *} |
638 case False |
638 case False |
749 show ?thesis by blast |
749 show ?thesis by blast |
750 qed |
750 qed |
751 -- {* |
751 -- {* |
752 @{text "?thesis"} can easily be shown using properties of @{text "za"} and @{text "zb"}: |
752 @{text "?thesis"} can easily be shown using properties of @{text "za"} and @{text "zb"}: |
753 *} |
753 *} |
754 from step [OF l_za ls_zb] |
754 have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" using l_za ls_zb by blast |
755 have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" . |
|
756 with eq_zab show ?thesis by simp |
755 with eq_zab show ?thesis by simp |
757 qed |
756 qed |
758 with h5 h6 show ?thesis |
757 with h5 h6 show ?thesis |
759 by (drule_tac star_intro1, auto simp:strict_prefix_def elim:prefixE) |
758 by (drule_tac star_intro1, auto simp:strict_prefix_def elim:prefixE) |
760 qed |
759 qed |
860 then obtain za where z_decom: "z = za @ b" |
859 then obtain za where z_decom: "z = za @ b" |
861 and x_za: "(x - x_max) @ za \<in> L\<^isub>1" |
860 and x_za: "(x - x_max) @ za \<in> L\<^isub>1" |
862 using a_in by (auto elim:prefixE) |
861 using a_in by (auto elim:prefixE) |
863 from x_za h7 have "(y - ya) @ za \<in> L\<^isub>1" |
862 from x_za h7 have "(y - ya) @ za \<in> L\<^isub>1" |
864 by (auto simp:str_eq_def str_eq_rel_def) |
863 by (auto simp:str_eq_def str_eq_rel_def) |
865 with z_decom b_in show ?thesis by (auto dest!:step[of "(y - ya) @ za"]) |
864 with b_in have "((y - ya) @ za) @ b \<in> L\<^isub>1\<star>" by blast |
|
865 with z_decom show ?thesis by auto |
866 qed |
866 qed |
867 with h5 h6 show ?thesis |
867 with h5 h6 show ?thesis |
868 by (drule_tac star_intro1, auto simp:strict_prefix_def elim:prefixE) |
868 by (drule_tac star_intro1, auto simp:strict_prefix_def elim:prefixE) |
869 qed |
869 qed |
870 } |
870 } |
895 |
895 |
896 lemma rexp_imp_finite: |
896 lemma rexp_imp_finite: |
897 fixes r::"rexp" |
897 fixes r::"rexp" |
898 shows "finite (UNIV // \<approx>(L r))" |
898 shows "finite (UNIV // \<approx>(L r))" |
899 by (induct r) (auto) |
899 by (induct r) (auto) |
|
900 |
900 |
901 |
901 end |
902 end |
902 |
903 |
903 (* |
904 (* |
904 lemma refined_quotient_union_eq: |
905 lemma refined_quotient_union_eq: |