99 ultimately show "finite (UNIV // R2)" by (rule finite_imageD) |
99 ultimately show "finite (UNIV // R2)" by (rule finite_imageD) |
100 qed |
100 qed |
101 |
101 |
102 lemma tag_finite_imageD: |
102 lemma tag_finite_imageD: |
103 assumes rng_fnt: "finite (range tag)" |
103 assumes rng_fnt: "finite (range tag)" |
104 and same_tag_eqvt: "=tag= \<subseteq> \<approx>A" |
104 and refined: "=tag= \<subseteq> \<approx>A" |
105 shows "finite (UNIV // \<approx>A)" |
105 shows "finite (UNIV // \<approx>A)" |
106 proof (rule_tac refined_partition_finite [of "=tag="]) |
106 proof (rule_tac refined_partition_finite [of "=tag="]) |
107 show "finite (UNIV // =tag=)" by (rule finite_eq_tag_rel[OF rng_fnt]) |
107 show "finite (UNIV // =tag=)" by (rule finite_eq_tag_rel[OF rng_fnt]) |
108 next |
108 next |
109 from same_tag_eqvt |
109 show "=tag= \<subseteq> \<approx>A" using refined . |
110 show "=tag= \<subseteq> \<approx>A" . |
|
111 next |
110 next |
112 show "equiv UNIV =tag=" |
111 show "equiv UNIV =tag=" |
113 unfolding equiv_def tag_eq_def refl_on_def sym_def trans_def |
112 and "equiv UNIV (\<approx>A)" |
|
113 unfolding equiv_def str_eq_def tag_eq_def refl_on_def sym_def trans_def |
114 by auto |
114 by auto |
115 next |
|
116 show "equiv UNIV (\<approx>A)" |
|
117 unfolding equiv_def str_eq_def sym_def refl_on_def trans_def |
|
118 by blast |
|
119 qed |
115 qed |
120 |
116 |
121 |
117 |
122 subsection {* The proof *} |
118 subsection {* The proof *} |
123 |
119 |
137 lemma quot_one_subset: |
133 lemma quot_one_subset: |
138 shows "UNIV // \<approx>{[]} \<subseteq> {{[]}, UNIV - {[]}}" |
134 shows "UNIV // \<approx>{[]} \<subseteq> {{[]}, UNIV - {[]}}" |
139 proof |
135 proof |
140 fix x |
136 fix x |
141 assume "x \<in> UNIV // \<approx>{[]}" |
137 assume "x \<in> UNIV // \<approx>{[]}" |
142 then obtain y where h: "x = {z. (y, z) \<in> \<approx>{[]}}" |
138 then obtain y where h: "x = {z. y \<approx>{[]} z}" |
143 unfolding quotient_def Image_def by blast |
139 unfolding quotient_def Image_def by blast |
144 show "x \<in> {{[]}, UNIV - {[]}}" |
140 { assume "y = []" |
145 proof (cases "y = []") |
141 with h have "x = {[]}" by (auto simp: str_eq_def) |
146 case True with h |
142 then have "x \<in> {{[]}, UNIV - {[]}}" by simp } |
147 have "x = {[]}" by (auto simp: str_eq_def) |
143 moreover |
148 thus ?thesis by simp |
144 { assume "y \<noteq> []" |
149 next |
145 with h have "x = UNIV - {[]}" by (auto simp: str_eq_def) |
150 case False with h |
146 then have "x \<in> {{[]}, UNIV - {[]}}" by simp } |
151 have "x = UNIV - {[]}" by (auto simp: str_eq_def) |
147 ultimately show "x \<in> {{[]}, UNIV - {[]}}" by blast |
152 thus ?thesis by simp |
|
153 qed |
|
154 qed |
148 qed |
155 |
149 |
156 lemma quot_one_finiteI [intro]: |
150 lemma quot_one_finiteI [intro]: |
157 shows "finite (UNIV // \<approx>{[]})" |
151 shows "finite (UNIV // \<approx>{[]})" |
158 by (rule finite_subset[OF quot_one_subset]) (simp) |
152 by (rule finite_subset[OF quot_one_subset]) (simp) |
406 qed |
400 qed |
407 |
401 |
408 definition |
402 definition |
409 tag_Star :: "'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang) set" |
403 tag_Star :: "'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang) set" |
410 where |
404 where |
411 "tag_Star A \<equiv> (\<lambda>x. {\<approx>A `` {v} | u v. u < x \<and> u \<in> A\<star> \<and> (u, v) \<in> Partitions x})" |
405 "tag_Star A \<equiv> \<lambda>x. {\<approx>A `` {v} | u v. u < x \<and> u \<in> A\<star> \<and> (u, v) \<in> Partitions x}" |
412 |
406 |
413 lemma tag_Star_non_empty_injI: |
407 lemma tag_Star_non_empty_injI: |
414 assumes a: "tag_Star A x = tag_Star A y" |
408 assumes a: "tag_Star A x = tag_Star A y" |
415 and c: "x @ z \<in> A\<star>" |
409 and c: "x @ z \<in> A\<star>" |
416 and d: "x \<noteq> []" |
410 and d: "x \<noteq> []" |
442 lemma tag_Star_empty_injI: |
436 lemma tag_Star_empty_injI: |
443 assumes a: "tag_Star A x = tag_Star A y" |
437 assumes a: "tag_Star A x = tag_Star A y" |
444 and c: "x @ z \<in> A\<star>" |
438 and c: "x @ z \<in> A\<star>" |
445 and d: "x = []" |
439 and d: "x = []" |
446 shows "y @ z \<in> A\<star>" |
440 shows "y @ z \<in> A\<star>" |
447 using assms |
441 proof - |
448 apply(simp) |
442 from a have "{} = tag_Star A y" unfolding tag_Star_def using d by auto |
449 apply(simp add: tag_Star_def strict_prefix_def) |
443 then have "y = []" |
450 apply(auto simp add: prefix_def Partitions_def) |
444 unfolding tag_Star_def Partitions_def strict_prefix_def prefix_def |
451 by (metis Nil_in_star append_self_conv2) |
445 by (auto) (metis Nil_in_star append_self_conv2) |
|
446 then show "y @ z \<in> A\<star>" using c d by simp |
|
447 qed |
452 |
448 |
453 lemma quot_star_finiteI [intro]: |
449 lemma quot_star_finiteI [intro]: |
454 assumes finite1: "finite (UNIV // \<approx>A)" |
450 assumes finite1: "finite (UNIV // \<approx>A)" |
455 shows "finite (UNIV // \<approx>(A\<star>))" |
451 shows "finite (UNIV // \<approx>(A\<star>))" |
456 proof (rule_tac tag = "tag_Star A" in tag_finite_imageD) |
452 proof (rule_tac tag = "tag_Star A" in tag_finite_imageD) |