|
1 theory Myhill_2 |
|
2 imports Myhill_1 Prefix_subtract |
|
3 "~~/src/HOL/Library/List_Prefix" |
|
4 begin |
|
5 |
|
6 section {* Direction @{text "regular language \<Rightarrow> finite partition"} *} |
|
7 |
|
8 definition |
|
9 str_eq :: "string \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> bool" ("_ \<approx>_ _") |
|
10 where |
|
11 "x \<approx>A y \<equiv> (x, y) \<in> (\<approx>A)" |
|
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 |
|
18 definition |
|
19 tag_eq_rel :: "(string \<Rightarrow> 'b) \<Rightarrow> (string \<times> string) set" ("=_=") |
|
20 where |
|
21 "=tag= \<equiv> {(x, y). tag x = tag y}" |
|
22 |
|
23 lemma finite_eq_tag_rel: |
|
24 assumes rng_fnt: "finite (range tag)" |
|
25 shows "finite (UNIV // =tag=)" |
|
26 proof - |
|
27 let "?f" = "\<lambda>X. tag ` X" and ?A = "(UNIV // =tag=)" |
|
28 have "finite (?f ` ?A)" |
|
29 proof - |
|
30 have "range ?f \<subseteq> (Pow (range tag))" unfolding Pow_def by auto |
|
31 moreover |
|
32 have "finite (Pow (range tag))" using rng_fnt by simp |
|
33 ultimately |
|
34 have "finite (range ?f)" unfolding image_def by (blast intro: finite_subset) |
|
35 moreover |
|
36 have "?f ` ?A \<subseteq> range ?f" by auto |
|
37 ultimately show "finite (?f ` ?A)" by (rule rev_finite_subset) |
|
38 qed |
|
39 moreover |
|
40 have "inj_on ?f ?A" |
|
41 proof - |
|
42 { fix X Y |
|
43 assume X_in: "X \<in> ?A" |
|
44 and Y_in: "Y \<in> ?A" |
|
45 and tag_eq: "?f X = ?f Y" |
|
46 then obtain x y |
|
47 where "x \<in> X" "y \<in> Y" "tag x = tag y" |
|
48 unfolding quotient_def Image_def image_def tag_eq_rel_def |
|
49 by (simp) (blast) |
|
50 with X_in Y_in |
|
51 have "X = Y" |
|
52 unfolding quotient_def tag_eq_rel_def by auto |
|
53 } |
|
54 then show "inj_on ?f ?A" unfolding inj_on_def by auto |
|
55 qed |
|
56 ultimately show "finite (UNIV // =tag=)" by (rule finite_imageD) |
|
57 qed |
|
58 |
|
59 lemma refined_partition_finite: |
|
60 assumes fnt: "finite (UNIV // R1)" |
|
61 and refined: "R1 \<subseteq> R2" |
|
62 and eq1: "equiv UNIV R1" and eq2: "equiv UNIV R2" |
|
63 shows "finite (UNIV // R2)" |
|
64 proof - |
|
65 let ?f = "\<lambda>X. {R1 `` {x} | x. x \<in> X}" |
|
66 and ?A = "UNIV // R2" and ?B = "UNIV // R1" |
|
67 have "?f ` ?A \<subseteq> Pow ?B" |
|
68 unfolding image_def Pow_def quotient_def by auto |
|
69 moreover |
|
70 have "finite (Pow ?B)" using fnt by simp |
|
71 ultimately |
|
72 have "finite (?f ` ?A)" by (rule finite_subset) |
|
73 moreover |
|
74 have "inj_on ?f ?A" |
|
75 proof - |
|
76 { fix X Y |
|
77 assume X_in: "X \<in> ?A" and Y_in: "Y \<in> ?A" and eq_f: "?f X = ?f Y" |
|
78 from quotientE [OF X_in] |
|
79 obtain x where "X = R2 `` {x}" by blast |
|
80 with equiv_class_self[OF eq2] have x_in: "x \<in> X" by simp |
|
81 then have "R1 ``{x} \<in> ?f X" by auto |
|
82 with eq_f have "R1 `` {x} \<in> ?f Y" by simp |
|
83 then obtain y |
|
84 where y_in: "y \<in> Y" and eq_r1_xy: "R1 `` {x} = R1 `` {y}" by auto |
|
85 with eq_equiv_class[OF _ eq1] |
|
86 have "(x, y) \<in> R1" by blast |
|
87 with refined have "(x, y) \<in> R2" by auto |
|
88 with quotient_eqI [OF eq2 X_in Y_in x_in y_in] |
|
89 have "X = Y" . |
|
90 } |
|
91 then show "inj_on ?f ?A" unfolding inj_on_def by blast |
|
92 qed |
|
93 ultimately show "finite (UNIV // R2)" by (rule finite_imageD) |
|
94 qed |
|
95 |
|
96 lemma tag_finite_imageD: |
|
97 assumes rng_fnt: "finite (range tag)" |
|
98 and same_tag_eqvt: "\<And>m n. tag m = tag n \<Longrightarrow> m \<approx>A n" |
|
99 shows "finite (UNIV // \<approx>A)" |
|
100 proof (rule_tac refined_partition_finite [of "=tag="]) |
|
101 show "finite (UNIV // =tag=)" by (rule finite_eq_tag_rel[OF rng_fnt]) |
|
102 next |
|
103 from same_tag_eqvt |
|
104 show "=tag= \<subseteq> \<approx>A" unfolding tag_eq_rel_def str_eq_def |
|
105 by auto |
|
106 next |
|
107 show "equiv UNIV =tag=" |
|
108 unfolding equiv_def tag_eq_rel_def refl_on_def sym_def trans_def |
|
109 by auto |
|
110 next |
|
111 show "equiv UNIV (\<approx>A)" |
|
112 unfolding equiv_def str_eq_rel_def sym_def refl_on_def trans_def |
|
113 by blast |
|
114 qed |
|
115 |
|
116 |
|
117 subsection {* The proof *} |
|
118 |
|
119 subsubsection {* The base case for @{const "NULL"} *} |
|
120 |
|
121 lemma quot_null_eq: |
|
122 shows "UNIV // \<approx>{} = {UNIV}" |
|
123 unfolding quotient_def Image_def str_eq_rel_def by auto |
|
124 |
|
125 lemma quot_null_finiteI [intro]: |
|
126 shows "finite (UNIV // \<approx>{})" |
|
127 unfolding quot_null_eq by simp |
|
128 |
|
129 |
|
130 subsubsection {* The base case for @{const "EMPTY"} *} |
|
131 |
|
132 lemma quot_empty_subset: |
|
133 shows "UNIV // \<approx>{[]} \<subseteq> {{[]}, UNIV - {[]}}" |
|
134 proof |
|
135 fix x |
|
136 assume "x \<in> UNIV // \<approx>{[]}" |
|
137 then obtain y where h: "x = {z. (y, z) \<in> \<approx>{[]}}" |
|
138 unfolding quotient_def Image_def by blast |
|
139 show "x \<in> {{[]}, UNIV - {[]}}" |
|
140 proof (cases "y = []") |
|
141 case True with h |
|
142 have "x = {[]}" by (auto simp: str_eq_rel_def) |
|
143 thus ?thesis by simp |
|
144 next |
|
145 case False with h |
|
146 have "x = UNIV - {[]}" by (auto simp: str_eq_rel_def) |
|
147 thus ?thesis by simp |
|
148 qed |
|
149 qed |
|
150 |
|
151 lemma quot_empty_finiteI [intro]: |
|
152 shows "finite (UNIV // \<approx>{[]})" |
|
153 by (rule finite_subset[OF quot_empty_subset]) (simp) |
|
154 |
|
155 |
|
156 subsubsection {* The base case for @{const "CHAR"} *} |
|
157 |
|
158 lemma quot_char_subset: |
|
159 "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}" |
|
160 proof |
|
161 fix x |
|
162 assume "x \<in> UNIV // \<approx>{[c]}" |
|
163 then obtain y where h: "x = {z. (y, z) \<in> \<approx>{[c]}}" |
|
164 unfolding quotient_def Image_def by blast |
|
165 show "x \<in> {{[]},{[c]}, UNIV - {[], [c]}}" |
|
166 proof - |
|
167 { assume "y = []" hence "x = {[]}" using h |
|
168 by (auto simp:str_eq_rel_def) } |
|
169 moreover |
|
170 { assume "y = [c]" hence "x = {[c]}" using h |
|
171 by (auto dest!:spec[where x = "[]"] simp:str_eq_rel_def) } |
|
172 moreover |
|
173 { assume "y \<noteq> []" and "y \<noteq> [c]" |
|
174 hence "\<forall> z. (y @ z) \<noteq> [c]" by (case_tac y, auto) |
|
175 moreover have "\<And> p. (p \<noteq> [] \<and> p \<noteq> [c]) = (\<forall> q. p @ q \<noteq> [c])" |
|
176 by (case_tac p, auto) |
|
177 ultimately have "x = UNIV - {[],[c]}" using h |
|
178 by (auto simp add:str_eq_rel_def) |
|
179 } |
|
180 ultimately show ?thesis by blast |
|
181 qed |
|
182 qed |
|
183 |
|
184 lemma quot_char_finiteI [intro]: |
|
185 shows "finite (UNIV // \<approx>{[c]})" |
|
186 by (rule finite_subset[OF quot_char_subset]) (simp) |
|
187 |
|
188 |
|
189 subsubsection {* The inductive case for @{const ALT} *} |
|
190 |
|
191 definition |
|
192 tag_str_ALT :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang)" |
|
193 where |
|
194 "tag_str_ALT A B \<equiv> (\<lambda>x. (\<approx>A `` {x}, \<approx>B `` {x}))" |
|
195 |
|
196 lemma quot_union_finiteI [intro]: |
|
197 assumes finite1: "finite (UNIV // \<approx>A)" |
|
198 and finite2: "finite (UNIV // \<approx>B)" |
|
199 shows "finite (UNIV // \<approx>(A \<union> B))" |
|
200 proof (rule_tac tag = "tag_str_ALT A B" in tag_finite_imageD) |
|
201 have "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))" |
|
202 using finite1 finite2 by auto |
|
203 then show "finite (range (tag_str_ALT A B))" |
|
204 unfolding tag_str_ALT_def quotient_def |
|
205 by (rule rev_finite_subset) (auto) |
|
206 next |
|
207 show "\<And>x y. tag_str_ALT A B x = tag_str_ALT A B y \<Longrightarrow> x \<approx>(A \<union> B) y" |
|
208 unfolding tag_str_ALT_def |
|
209 unfolding str_eq_def |
|
210 unfolding str_eq_rel_def |
|
211 by auto |
|
212 qed |
|
213 |
|
214 |
|
215 subsubsection {* The inductive case for @{text "SEQ"}*} |
|
216 |
|
217 definition |
|
218 tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)" |
|
219 where |
|
220 "tag_str_SEQ L1 L2 \<equiv> |
|
221 (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa. xa \<le> x \<and> xa \<in> L1}))" |
|
222 |
|
223 lemma Seq_in_cases: |
|
224 assumes "x @ z \<in> A \<cdot> B" |
|
225 shows "(\<exists> x' \<le> x. x' \<in> A \<and> (x - x') @ z \<in> B) \<or> |
|
226 (\<exists> z' \<le> z. (x @ z') \<in> A \<and> (z - z') \<in> B)" |
|
227 using assms |
|
228 unfolding Seq_def prefix_def |
|
229 by (auto simp add: append_eq_append_conv2) |
|
230 |
|
231 lemma tag_str_SEQ_injI: |
|
232 assumes eq_tag: "tag_str_SEQ A B x = tag_str_SEQ A B y" |
|
233 shows "x \<approx>(A \<cdot> B) y" |
|
234 proof - |
|
235 { fix x y z |
|
236 assume xz_in_seq: "x @ z \<in> A \<cdot> B" |
|
237 and tag_xy: "tag_str_SEQ A B x = tag_str_SEQ A B y" |
|
238 have"y @ z \<in> A \<cdot> B" |
|
239 proof - |
|
240 { (* first case with x' in A and (x - x') @ z in B *) |
|
241 fix x' |
|
242 assume h1: "x' \<le> x" and h2: "x' \<in> A" and h3: "(x - x') @ z \<in> B" |
|
243 obtain y' |
|
244 where "y' \<le> y" |
|
245 and "y' \<in> A" |
|
246 and "(y - y') @ z \<in> B" |
|
247 proof - |
|
248 have "{\<approx>B `` {x - x'} |x'. x' \<le> x \<and> x' \<in> A} = |
|
249 {\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A}" (is "?Left = ?Right") |
|
250 using tag_xy unfolding tag_str_SEQ_def by simp |
|
251 moreover |
|
252 have "\<approx>B `` {x - x'} \<in> ?Left" using h1 h2 by auto |
|
253 ultimately |
|
254 have "\<approx>B `` {x - x'} \<in> ?Right" by simp |
|
255 then obtain y' |
|
256 where eq_xy': "\<approx>B `` {x - x'} = \<approx>B `` {y - y'}" |
|
257 and pref_y': "y' \<le> y" and y'_in: "y' \<in> A" |
|
258 by simp blast |
|
259 |
|
260 have "(x - x') \<approx>B (y - y')" using eq_xy' |
|
261 unfolding Image_def str_eq_rel_def str_eq_def by auto |
|
262 with h3 have "(y - y') @ z \<in> B" |
|
263 unfolding str_eq_rel_def str_eq_def by simp |
|
264 with pref_y' y'_in |
|
265 show ?thesis using that by blast |
|
266 qed |
|
267 then have "y @ z \<in> A \<cdot> B" by (erule_tac prefixE) (auto simp: Seq_def) |
|
268 } |
|
269 moreover |
|
270 { (* second case with x @ z' in A and z - z' in B *) |
|
271 fix z' |
|
272 assume h1: "z' \<le> z" and h2: "(x @ z') \<in> A" and h3: "z - z' \<in> B" |
|
273 have "\<approx>A `` {x} = \<approx>A `` {y}" |
|
274 using tag_xy unfolding tag_str_SEQ_def by simp |
|
275 with h2 have "y @ z' \<in> A" |
|
276 unfolding Image_def str_eq_rel_def str_eq_def by auto |
|
277 with h1 h3 have "y @ z \<in> A \<cdot> B" |
|
278 unfolding prefix_def Seq_def |
|
279 by (auto) (metis append_assoc) |
|
280 } |
|
281 ultimately show "y @ z \<in> A \<cdot> B" |
|
282 using Seq_in_cases [OF xz_in_seq] by blast |
|
283 qed |
|
284 } |
|
285 from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]] |
|
286 show "x \<approx>(A \<cdot> B) y" unfolding str_eq_def str_eq_rel_def by blast |
|
287 qed |
|
288 |
|
289 lemma quot_seq_finiteI [intro]: |
|
290 fixes L1 L2::"lang" |
|
291 assumes fin1: "finite (UNIV // \<approx>L1)" |
|
292 and fin2: "finite (UNIV // \<approx>L2)" |
|
293 shows "finite (UNIV // \<approx>(L1 \<cdot> L2))" |
|
294 proof (rule_tac tag = "tag_str_SEQ L1 L2" in tag_finite_imageD) |
|
295 show "\<And>x y. tag_str_SEQ L1 L2 x = tag_str_SEQ L1 L2 y \<Longrightarrow> x \<approx>(L1 \<cdot> L2) y" |
|
296 by (rule tag_str_SEQ_injI) |
|
297 next |
|
298 have *: "finite ((UNIV // \<approx>L1) \<times> (Pow (UNIV // \<approx>L2)))" |
|
299 using fin1 fin2 by auto |
|
300 show "finite (range (tag_str_SEQ L1 L2))" |
|
301 unfolding tag_str_SEQ_def |
|
302 apply(rule finite_subset[OF _ *]) |
|
303 unfolding quotient_def |
|
304 by auto |
|
305 qed |
|
306 |
|
307 |
|
308 subsubsection {* The inductive case for @{const "STAR"} *} |
|
309 |
|
310 definition |
|
311 tag_str_STAR :: "lang \<Rightarrow> string \<Rightarrow> lang set" |
|
312 where |
|
313 "tag_str_STAR L1 \<equiv> (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<star>})" |
|
314 |
|
315 text {* A technical lemma. *} |
|
316 lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> |
|
317 (\<exists> max \<in> A. \<forall> a \<in> A. f a <= (f max :: nat))" |
|
318 proof (induct rule:finite.induct) |
|
319 case emptyI thus ?case by simp |
|
320 next |
|
321 case (insertI A a) |
|
322 show ?case |
|
323 proof (cases "A = {}") |
|
324 case True thus ?thesis by (rule_tac x = a in bexI, auto) |
|
325 next |
|
326 case False |
|
327 with insertI.hyps and False |
|
328 obtain max |
|
329 where h1: "max \<in> A" |
|
330 and h2: "\<forall>a\<in>A. f a \<le> f max" by blast |
|
331 show ?thesis |
|
332 proof (cases "f a \<le> f max") |
|
333 assume "f a \<le> f max" |
|
334 with h1 h2 show ?thesis by (rule_tac x = max in bexI, auto) |
|
335 next |
|
336 assume "\<not> (f a \<le> f max)" |
|
337 thus ?thesis using h2 by (rule_tac x = a in bexI, auto) |
|
338 qed |
|
339 qed |
|
340 qed |
|
341 |
|
342 |
|
343 text {* The following is a technical lemma, which helps to show the range finiteness of tag function. *} |
|
344 |
|
345 lemma finite_strict_prefix_set: "finite {xa. xa < (x::string)}" |
|
346 apply (induct x rule:rev_induct, simp) |
|
347 apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}") |
|
348 by (auto simp:strict_prefix_def) |
|
349 |
|
350 |
|
351 lemma tag_str_STAR_injI: |
|
352 assumes eq_tag: "tag_str_STAR L\<^isub>1 v = tag_str_STAR L\<^isub>1 w" |
|
353 shows "v \<approx>(L\<^isub>1\<star>) w" |
|
354 proof- |
|
355 { fix x y z |
|
356 assume xz_in_star: "x @ z \<in> L\<^isub>1\<star>" |
|
357 and tag_xy: "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y" |
|
358 have "y @ z \<in> L\<^isub>1\<star>" |
|
359 proof(cases "x = []") |
|
360 case True |
|
361 with tag_xy have "y = []" |
|
362 by (auto simp add: tag_str_STAR_def strict_prefix_def) |
|
363 thus ?thesis using xz_in_star True by simp |
|
364 next |
|
365 case False |
|
366 let ?S = "{xa. xa < x \<and> xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>}" |
|
367 have "finite ?S" |
|
368 by (rule_tac B = "{xa. xa < x}" in finite_subset, |
|
369 auto simp:finite_strict_prefix_set) |
|
370 moreover have "?S \<noteq> {}" using False xz_in_star |
|
371 by (simp, rule_tac x = "[]" in exI, auto simp:strict_prefix_def) |
|
372 ultimately have "\<exists> xa_max \<in> ?S. \<forall> xa \<in> ?S. length xa \<le> length xa_max" |
|
373 using finite_set_has_max by blast |
|
374 then obtain xa_max |
|
375 where h1: "xa_max < x" |
|
376 and h2: "xa_max \<in> L\<^isub>1\<star>" |
|
377 and h3: "(x - xa_max) @ z \<in> L\<^isub>1\<star>" |
|
378 and h4:"\<forall> xa < x. xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star> |
|
379 \<longrightarrow> length xa \<le> length xa_max" |
|
380 by blast |
|
381 obtain ya |
|
382 where h5: "ya < y" and h6: "ya \<in> L\<^isub>1\<star>" |
|
383 and eq_xya: "(x - xa_max) \<approx>L\<^isub>1 (y - ya)" |
|
384 proof- |
|
385 from tag_xy have "{\<approx>L\<^isub>1 `` {x - xa} |xa. xa < x \<and> xa \<in> L\<^isub>1\<star>} = |
|
386 {\<approx>L\<^isub>1 `` {y - xa} |xa. xa < y \<and> xa \<in> L\<^isub>1\<star>}" (is "?left = ?right") |
|
387 by (auto simp:tag_str_STAR_def) |
|
388 moreover have "\<approx>L\<^isub>1 `` {x - xa_max} \<in> ?left" using h1 h2 by auto |
|
389 ultimately have "\<approx>L\<^isub>1 `` {x - xa_max} \<in> ?right" by simp |
|
390 thus ?thesis using that |
|
391 apply (simp add:Image_def str_eq_rel_def str_eq_def) by blast |
|
392 qed |
|
393 have "(y - ya) @ z \<in> L\<^isub>1\<star>" |
|
394 proof- |
|
395 obtain za zb where eq_zab: "z = za @ zb" |
|
396 and l_za: "(y - ya)@za \<in> L\<^isub>1" and ls_zb: "zb \<in> L\<^isub>1\<star>" |
|
397 proof - |
|
398 from h1 have "(x - xa_max) @ z \<noteq> []" |
|
399 by (auto simp:strict_prefix_def elim:prefixE) |
|
400 from star_decom [OF h3 this] |
|
401 obtain a b where a_in: "a \<in> L\<^isub>1" |
|
402 and a_neq: "a \<noteq> []" and b_in: "b \<in> L\<^isub>1\<star>" |
|
403 and ab_max: "(x - xa_max) @ z = a @ b" by blast |
|
404 let ?za = "a - (x - xa_max)" and ?zb = "b" |
|
405 have pfx: "(x - xa_max) \<le> a" (is "?P1") |
|
406 and eq_z: "z = ?za @ ?zb" (is "?P2") |
|
407 proof - |
|
408 have "((x - xa_max) \<le> a \<and> (a - (x - xa_max)) @ b = z) \<or> |
|
409 (a < (x - xa_max) \<and> ((x - xa_max) - a) @ z = b)" |
|
410 using append_eq_dest[OF ab_max] by (auto simp:strict_prefix_def) |
|
411 moreover { |
|
412 assume np: "a < (x - xa_max)" |
|
413 and b_eqs: "((x - xa_max) - a) @ z = b" |
|
414 have "False" |
|
415 proof - |
|
416 let ?xa_max' = "xa_max @ a" |
|
417 have "?xa_max' < x" |
|
418 using np h1 by (clarsimp simp:strict_prefix_def diff_prefix) |
|
419 moreover have "?xa_max' \<in> L\<^isub>1\<star>" |
|
420 using a_in h2 by (simp add:star_intro3) |
|
421 moreover have "(x - ?xa_max') @ z \<in> L\<^isub>1\<star>" |
|
422 using b_eqs b_in np h1 by (simp add:diff_diff_append) |
|
423 moreover have "\<not> (length ?xa_max' \<le> length xa_max)" |
|
424 using a_neq by simp |
|
425 ultimately show ?thesis using h4 by blast |
|
426 qed } |
|
427 ultimately show ?P1 and ?P2 by auto |
|
428 qed |
|
429 hence "(x - xa_max)@?za \<in> L\<^isub>1" using a_in by (auto elim:prefixE) |
|
430 with eq_xya have "(y - ya) @ ?za \<in> L\<^isub>1" |
|
431 by (auto simp:str_eq_def str_eq_rel_def) |
|
432 with eq_z and b_in |
|
433 show ?thesis using that by blast |
|
434 qed |
|
435 have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" using l_za ls_zb by blast |
|
436 with eq_zab show ?thesis by simp |
|
437 qed |
|
438 with h5 h6 show ?thesis |
|
439 by (drule_tac star_intro1) (auto simp:strict_prefix_def elim: prefixE) |
|
440 qed |
|
441 } |
|
442 from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]] |
|
443 show ?thesis unfolding str_eq_def str_eq_rel_def by blast |
|
444 qed |
|
445 |
|
446 lemma quot_star_finiteI [intro]: |
|
447 assumes finite1: "finite (UNIV // \<approx>A)" |
|
448 shows "finite (UNIV // \<approx>(A\<star>))" |
|
449 proof (rule_tac tag = "tag_str_STAR A" in tag_finite_imageD) |
|
450 show "\<And>x y. tag_str_STAR A x = tag_str_STAR A y \<Longrightarrow> x \<approx>(A\<star>) y" |
|
451 by (rule tag_str_STAR_injI) |
|
452 next |
|
453 have *: "finite (Pow (UNIV // \<approx>A))" |
|
454 using finite1 by auto |
|
455 show "finite (range (tag_str_STAR A))" |
|
456 unfolding tag_str_STAR_def |
|
457 apply(rule finite_subset[OF _ *]) |
|
458 unfolding quotient_def |
|
459 by auto |
|
460 qed |
|
461 |
|
462 subsubsection{* The conclusion *} |
|
463 |
|
464 lemma Myhill_Nerode2: |
|
465 shows "finite (UNIV // \<approx>(L_rexp r))" |
|
466 by (induct r) (auto) |
|
467 |
|
468 |
|
469 theorem Myhill_Nerode: |
|
470 shows "(\<exists>r. A = L_rexp r) \<longleftrightarrow> finite (UNIV // \<approx>A)" |
|
471 using Myhill_Nerode1 Myhill_Nerode2 by auto |
|
472 |
|
473 end |