223 subsubsection {* The inductive case for @{text "Times"}*} |
222 subsubsection {* The inductive case for @{text "Times"}*} |
224 |
223 |
225 definition |
224 definition |
226 "Partitions s \<equiv> {(u, v). u @ v = s}" |
225 "Partitions s \<equiv> {(u, v). u @ v = s}" |
227 |
226 |
228 lemma conc_elim: |
227 lemma conc_partitions_elim: |
229 assumes "x \<in> A \<cdot> B" |
228 assumes "x \<in> A \<cdot> B" |
230 shows "\<exists>(u, v) \<in> Partitions x. u \<in> A \<and> v \<in> B" |
229 shows "\<exists>(u, v) \<in> Partitions x. u \<in> A \<and> v \<in> B" |
231 using assms |
230 using assms |
232 unfolding conc_def Partitions_def |
231 unfolding conc_def Partitions_def |
233 by auto |
232 by auto |
234 |
233 |
235 lemma conc_intro: |
234 lemma conc_partitions_intro: |
236 assumes "(u, v) \<in> Partitions x \<and> u \<in> A \<and> v \<in> B" |
235 assumes "(u, v) \<in> Partitions x \<and> u \<in> A \<and> v \<in> B" |
237 shows "x \<in> A \<cdot> B" |
236 shows "x \<in> A \<cdot> B" |
238 using assms |
237 using assms |
239 unfolding conc_def Partitions_def |
238 unfolding conc_def Partitions_def |
240 by auto |
239 by auto |
241 |
240 |
242 |
241 lemma equiv_class_member: |
243 lemma y: |
242 assumes "x \<in> A" |
244 "\<lbrakk>x \<in> A; x \<approx>A y\<rbrakk> \<Longrightarrow> y \<in> A" |
243 and "\<approx>A `` {x} = \<approx>A `` {y}" |
245 apply(simp add: str_eq_def) |
244 shows "y \<in> A" |
246 apply(drule_tac x="[]" in spec) |
245 using assms |
247 apply(simp) |
246 apply(simp add: Image_def str_eq_def set_eq_iff) |
|
247 apply(metis append_Nil2) |
248 done |
248 done |
249 |
249 |
|
250 |
|
251 abbreviation |
|
252 tag_Times_1 :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang" |
|
253 where |
|
254 "tag_Times_1 A B \<equiv> \<lambda>x. \<approx>A `` {x}" |
|
255 |
|
256 abbreviation |
|
257 tag_Times_2 :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang) set" |
|
258 where |
|
259 "tag_Times_2 A B \<equiv> \<lambda>x. {(\<approx>A `` {u}, \<approx>B `` {v}) | u v. (u, v) \<in> Partitions x}" |
|
260 |
250 definition |
261 definition |
251 tag_Times3a :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang" |
262 tag_Times :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang \<times> ('a lang \<times> 'a lang) set" |
252 where |
263 where |
253 "tag_Times3a A B \<equiv> (\<lambda>x. \<approx>A `` {x})" |
264 "tag_Times A B \<equiv> \<lambda>x. (tag_Times_1 A B x, tag_Times_2 A B x)" |
254 |
265 |
255 definition |
266 lemma tag_Times_injI: |
256 tag_Times3b :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang) set" |
267 assumes a: "tag_Times_1 A B x = tag_Times_1 A B y" |
257 where |
268 and b: "tag_Times_2 A B x = tag_Times_2 A B y" |
258 "tag_Times3b A B \<equiv> |
|
259 (\<lambda>x. ({(\<approx>A `` {u}, \<approx>B `` {v}) | u v. (u, v) \<in> Partitions x}))" |
|
260 |
|
261 definition |
|
262 tag_Times3 :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang \<times> ('a lang \<times> 'a lang) set" |
|
263 where |
|
264 "tag_Times3 A B \<equiv> |
|
265 (\<lambda>x. (tag_Times3a A B x, tag_Times3b A B x))" |
|
266 |
|
267 lemma |
|
268 assumes a: "tag_Times3a A B x = tag_Times3a A B y" |
|
269 and b: "tag_Times3b A B x = tag_Times3b A B y" |
|
270 and c: "x @ z \<in> A \<cdot> B" |
269 and c: "x @ z \<in> A \<cdot> B" |
271 shows "y @ z \<in> A \<cdot> B" |
270 shows "y @ z \<in> A \<cdot> B" |
272 proof - |
271 proof - |
273 from c obtain u v where |
272 from c obtain u v where |
274 h1: "(u, v) \<in> Partitions (x @ z)" and |
273 h1: "(u, v) \<in> Partitions (x @ z)" and |
275 h2: "u \<in> A" and |
274 h2: "u \<in> A" and |
276 h3: "v \<in> B" by (auto dest: conc_elim) |
275 h3: "v \<in> B" by (auto dest: conc_partitions_elim) |
277 from h1 have "x @ z = u @ v" unfolding Partitions_def by simp |
276 from h1 have "x @ z = u @ v" unfolding Partitions_def by simp |
278 then obtain us |
277 then obtain us |
279 where "(x = u @ us \<and> us @ z = v) \<or> (x @ us = u \<and> z = us @ v)" |
278 where "(x = u @ us \<and> us @ z = v) \<or> (x @ us = u \<and> z = us @ v)" |
280 by (auto simp add: append_eq_append_conv2) |
279 by (auto simp add: append_eq_append_conv2) |
281 moreover |
280 moreover |
282 { assume eq: "x = u @ us" "us @ z = v" |
281 { assume eq: "x = u @ us" "us @ z = v" |
283 have "(\<approx>A `` {u}, \<approx>B `` {us}) \<in> tag_Times3b A B x" |
282 have "(\<approx>A `` {u}, \<approx>B `` {us}) \<in> tag_Times_2 A B x" |
284 unfolding tag_Times3b_def Partitions_def using eq by auto |
283 unfolding Partitions_def using eq by auto |
285 then have "(\<approx>A `` {u}, \<approx>B `` {us}) \<in> tag_Times3b A B y" |
284 then have "(\<approx>A `` {u}, \<approx>B `` {us}) \<in> tag_Times_2 A B y" |
286 using b by simp |
285 using b by simp |
287 then obtain u' us' where |
286 then obtain u' us' where |
288 q1: "\<approx>A `` {u} = \<approx>A `` {u'}" and |
287 q1: "\<approx>A `` {u} = \<approx>A `` {u'}" and |
289 q2: "\<approx>B `` {us} = \<approx>B `` {us'}" and |
288 q2: "\<approx>B `` {us} = \<approx>B `` {us'}" and |
290 q3: "(u', us') \<in> Partitions y" |
289 q3: "(u', us') \<in> Partitions y" by auto |
291 by (auto simp add: tag_Times3b_def) |
|
292 from q1 h2 have "u' \<in> A" |
290 from q1 h2 have "u' \<in> A" |
293 using y unfolding Image_def str_eq_def by blast |
291 using equiv_class_member by auto |
294 moreover from q2 h3 eq |
292 moreover from q2 h3 eq |
295 have "us' @ z \<in> B" |
293 have "us' @ z \<in> B" |
296 unfolding Image_def str_eq_def by auto |
294 unfolding Image_def str_eq_def by auto |
297 ultimately have "y @ z \<in> A \<cdot> B" using q3 |
295 ultimately have "y @ z \<in> A \<cdot> B" using q3 |
298 unfolding Partitions_def by auto |
296 unfolding Partitions_def by auto |
299 } |
297 } |
300 moreover |
298 moreover |
301 { assume eq: "x @ us = u" "z = us @ v" |
299 { assume eq: "x @ us = u" "z = us @ v" |
302 have "(\<approx>A `` {x}) = tag_Times3a A B x" |
300 have "(\<approx>A `` {x}) = tag_Times_1 A B x" by simp |
303 unfolding tag_Times3a_def by simp |
301 then have "(\<approx>A `` {x}) = tag_Times_1 A B y" |
304 then have "(\<approx>A `` {x}) = tag_Times3a A B y" |
|
305 using a by simp |
302 using a by simp |
306 then have "\<approx>A `` {x} = \<approx>A `` {y}" |
303 then have "\<approx>A `` {x} = \<approx>A `` {y}" by simp |
307 unfolding tag_Times3a_def by simp |
|
308 moreover |
304 moreover |
309 have "x @ us \<in> A" using h2 eq by simp |
305 have "x @ us \<in> A" using h2 eq by simp |
310 ultimately |
306 ultimately |
311 have "y @ us \<in> A" using y |
307 have "y @ us \<in> A" using equiv_class_member |
312 unfolding Image_def str_eq_def by blast |
308 unfolding Image_def str_eq_def by blast |
313 then have "(y @ us) @ v \<in> A \<cdot> B" |
309 then have "(y @ us) @ v \<in> A \<cdot> B" |
314 using h3 unfolding conc_def by blast |
310 using h3 unfolding conc_def by blast |
315 then have "y @ z \<in> A \<cdot> B" using eq by simp |
311 then have "y @ z \<in> A \<cdot> B" using eq by simp |
316 } |
312 } |
317 ultimately show "y @ z \<in> A \<cdot> B" by blast |
313 ultimately show "y @ z \<in> A \<cdot> B" by blast |
318 qed |
314 qed |
319 |
315 |
320 lemma conc_in_cases2: |
|
321 assumes "x @ z \<in> A \<cdot> B" |
|
322 shows "(\<exists> x' \<le> x. x' \<in> A \<and> (x - x') @ z \<in> B) \<or> |
|
323 (\<exists> z' \<le> z. (x @ z') \<in> A \<and> (z - z') \<in> B)" |
|
324 using assms |
|
325 unfolding conc_def prefix_def |
|
326 by (auto simp add: append_eq_append_conv2) |
|
327 |
|
328 definition |
|
329 tag_Times :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang set)" |
|
330 where |
|
331 "tag_Times A B \<equiv> |
|
332 (\<lambda>x. (\<approx>A `` {x}, {(\<approx>B `` {x - x'}) | x'. x' \<le> x \<and> x' \<in> A}))" |
|
333 |
|
334 lemma tag_Times_injI: |
|
335 assumes eq_tag: "tag_Times A B x = tag_Times A B y" |
|
336 shows "x \<approx>(A \<cdot> B) y" |
|
337 proof - |
|
338 { fix x y z |
|
339 assume xz_in_seq: "x @ z \<in> A \<cdot> B" |
|
340 and tag_xy: "tag_Times A B x = tag_Times A B y" |
|
341 have"y @ z \<in> A \<cdot> B" |
|
342 proof - |
|
343 { (* first case with x' in A and (x - x') @ z in B *) |
|
344 fix x' |
|
345 assume h1: "x' \<le> x" and h2: "x' \<in> A" and h3: "(x - x') @ z \<in> B" |
|
346 obtain y' |
|
347 where "y' \<le> y" |
|
348 and "y' \<in> A" |
|
349 and "(y - y') @ z \<in> B" |
|
350 proof - |
|
351 have "{\<approx>B `` {x - x'} |x'. x' \<le> x \<and> x' \<in> A} = |
|
352 {\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A}" (is "?Left = ?Right") |
|
353 using tag_xy unfolding tag_Times_def by simp |
|
354 moreover |
|
355 have "\<approx>B `` {x - x'} \<in> ?Left" using h1 h2 by auto |
|
356 ultimately |
|
357 have "\<approx>B `` {x - x'} \<in> ?Right" by simp |
|
358 then obtain y' |
|
359 where eq_xy': "\<approx>B `` {x - x'} = \<approx>B `` {y - y'}" |
|
360 and pref_y': "y' \<le> y" and y'_in: "y' \<in> A" |
|
361 by simp blast |
|
362 have "(x - x') \<approx>B (y - y')" using eq_xy' |
|
363 unfolding Image_def str_eq_def by auto |
|
364 with h3 have "(y - y') @ z \<in> B" |
|
365 unfolding str_eq_def by simp |
|
366 with pref_y' y'_in |
|
367 show ?thesis using that by blast |
|
368 qed |
|
369 then have "y @ z \<in> A \<cdot> B" |
|
370 unfolding prefix_def by auto |
|
371 } |
|
372 moreover |
|
373 { (* second case with x @ z' in A and z - z' in B *) |
|
374 fix z' |
|
375 assume h1: "z' \<le> z" and h2: "(x @ z') \<in> A" and h3: "z - z' \<in> B" |
|
376 have "\<approx>A `` {x} = \<approx>A `` {y}" |
|
377 using tag_xy unfolding tag_Times_def by simp |
|
378 with h2 have "y @ z' \<in> A" |
|
379 unfolding Image_def str_eq_def by auto |
|
380 with h1 h3 have "y @ z \<in> A \<cdot> B" |
|
381 unfolding prefix_def conc_def |
|
382 by (auto) (metis append_assoc) |
|
383 } |
|
384 ultimately show "y @ z \<in> A \<cdot> B" |
|
385 using conc_in_cases2 [OF xz_in_seq] by blast |
|
386 qed |
|
387 } |
|
388 from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]] |
|
389 show "x \<approx>(A \<cdot> B) y" unfolding str_eq_def by blast |
|
390 qed |
|
391 |
|
392 lemma quot_conc_finiteI [intro]: |
316 lemma quot_conc_finiteI [intro]: |
393 fixes A B::"'a lang" |
317 fixes A B::"'a lang" |
394 assumes fin1: "finite (UNIV // \<approx>A)" |
318 assumes fin1: "finite (UNIV // \<approx>A)" |
395 and fin2: "finite (UNIV // \<approx>B)" |
319 and fin2: "finite (UNIV // \<approx>B)" |
396 shows "finite (UNIV // \<approx>(A \<cdot> B))" |
320 shows "finite (UNIV // \<approx>(A \<cdot> B))" |
397 proof (rule_tac tag = "tag_Times A B" in tag_finite_imageD) |
321 proof (rule_tac tag = "tag_Times A B" in tag_finite_imageD) |
398 show "\<And>x y. tag_Times A B x = tag_Times A B y \<Longrightarrow> x \<approx>(A \<cdot> B) y" |
322 have "=(tag_Times A B)= \<subseteq> \<approx>(A \<cdot> B)" |
399 by (rule tag_Times_injI) |
323 apply(rule test_refined_intro) |
|
324 apply(rule tag_Times_injI) |
|
325 prefer 3 |
|
326 apply(assumption) |
|
327 apply(simp add: tag_Times_def tag_eq_def) |
|
328 apply(simp add: tag_eq_def tag_Times_def) |
|
329 done |
|
330 then show "\<And>x y. tag_Times A B x = tag_Times A B y \<Longrightarrow> x \<approx>(A \<cdot> B) y" |
|
331 unfolding tag_eq_def by auto |
400 next |
332 next |
401 have *: "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))" |
333 have *: "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>A \<times> UNIV // \<approx>B)))" |
402 using fin1 fin2 by auto |
334 using fin1 fin2 by auto |
403 show "finite (range (tag_Times A B))" |
335 show "finite (range (tag_Times A B))" |
404 unfolding tag_Times_def |
336 unfolding tag_Times_def |
405 apply(rule finite_subset[OF _ *]) |
337 apply(rule finite_subset[OF _ *]) |
406 unfolding quotient_def |
338 unfolding quotient_def |
408 qed |
340 qed |
409 |
341 |
410 |
342 |
411 subsubsection {* The inductive case for @{const "Star"} *} |
343 subsubsection {* The inductive case for @{const "Star"} *} |
412 |
344 |
413 definition |
345 lemma append_eq_append_conv3: |
414 "SPartitions s \<equiv> {(u, v). u @ v = s \<and> u < s}" |
346 assumes "xs @ ys = zs @ ts" "zs < xs" |
415 |
347 shows "\<exists>us. xs = zs @ us \<and> us @ ys = ts" |
416 lemma |
|
417 assumes "x \<in> A\<star>" "x \<noteq> []" |
|
418 shows "\<exists>(u, v) \<in> SPartitions x. u \<in> A\<star> \<and> v \<in> A\<star>" |
|
419 using assms |
348 using assms |
420 apply(subst (asm) star_unfold_left) |
349 apply(auto simp add: append_eq_append_conv2 strict_prefix_def) |
421 apply(simp) |
350 done |
422 apply(simp add: conc_def) |
351 |
423 apply(erule exE)+ |
352 lemma star_spartitions_elim: |
424 apply(erule conjE)+ |
|
425 apply(rule_tac x="([], xs @ ys)" in bexI) |
|
426 apply(simp) |
|
427 apply(simp add: SPartitions_def) |
|
428 apply(auto) |
|
429 apply (metis append_Cons list.exhaust strict_prefix_simps(2)) |
|
430 by (metis Nil_is_append_conv Nil_prefix xt1(11)) |
|
431 |
|
432 lemma |
|
433 assumes "x @ z \<in> A\<star>" "x \<noteq> []" |
353 assumes "x @ z \<in> A\<star>" "x \<noteq> []" |
434 shows "\<exists>(u, v) \<in> SPartitions x. u \<in> A\<star> \<and> v @ z \<in> A\<star>" |
354 shows "\<exists>(u, v) \<in> Partitions (x @ z). u < x \<and> u \<in> A\<star> \<and> v \<in> A\<star>" |
435 using assms |
355 proof - |
436 apply(subst (asm) star_unfold_left) |
356 have "([], x @ z) \<in> Partitions (x @ z)" "[] < x" "[] \<in> A\<star>" "x @ z \<in> A\<star>" |
437 apply(simp) |
357 using assms by (auto simp add: Partitions_def strict_prefix_def) |
438 apply(simp add: conc_def) |
358 then show "\<exists>(u, v) \<in> Partitions (x @ z). u < x \<and> u \<in> A\<star> \<and> v \<in> A\<star>" |
439 apply(erule exE)+ |
359 by blast |
440 apply(erule conjE)+ |
360 qed |
441 apply(rule_tac x="([], x)" in bexI) |
361 |
442 apply(simp) |
362 |
443 apply(simp add: SPartitions_def) |
363 lemma finite_set_has_max2: |
444 by (metis Nil_prefix xt1(11)) |
|
445 |
|
446 lemma finite_set_has_max: |
|
447 "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists> max \<in> A. \<forall> a \<in> A. length a \<le> length max" |
364 "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists> max \<in> A. \<forall> a \<in> A. length a \<le> length max" |
448 apply (induct rule:finite.induct) |
365 apply(induct rule:finite.induct) |
449 apply(simp) |
366 apply(simp) |
450 by (metis (full_types) all_not_in_conv insertI1 insert_iff linorder_linear order_eq_iff order_trans prefix_length_le) |
367 by (metis (full_types) all_not_in_conv insert_iff linorder_linear order_trans) |
451 |
|
452 |
|
453 |
|
454 definition |
|
455 tag_Star3 :: "'a lang \<Rightarrow> 'a list \<Rightarrow> (bool \<times> 'a lang) set" |
|
456 where |
|
457 "tag_Star3 A \<equiv> |
|
458 (\<lambda>x. ({(u \<in> A\<star>, \<approx>A `` {v}) | u v. (u, v) \<in> Partitions x}))" |
|
459 |
|
460 |
|
461 |
|
462 |
|
463 definition |
|
464 tag_Star :: "'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang) set" |
|
465 where |
|
466 "tag_Star A \<equiv> (\<lambda>x. {\<approx>A `` {x - xa} | xa. xa < x \<and> xa \<in> A\<star>})" |
|
467 |
|
468 text {* A technical lemma. *} |
|
469 lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> |
|
470 (\<exists> max \<in> A. \<forall> a \<in> A. f a <= (f max :: nat))" |
|
471 proof (induct rule:finite.induct) |
|
472 case emptyI thus ?case by simp |
|
473 next |
|
474 case (insertI A a) |
|
475 show ?case |
|
476 proof (cases "A = {}") |
|
477 case True thus ?thesis by (rule_tac x = a in bexI, auto) |
|
478 next |
|
479 case False |
|
480 with insertI.hyps and False |
|
481 obtain max |
|
482 where h1: "max \<in> A" |
|
483 and h2: "\<forall>a\<in>A. f a \<le> f max" by blast |
|
484 show ?thesis |
|
485 proof (cases "f a \<le> f max") |
|
486 assume "f a \<le> f max" |
|
487 with h1 h2 show ?thesis by (rule_tac x = max in bexI, auto) |
|
488 next |
|
489 assume "\<not> (f a \<le> f max)" |
|
490 thus ?thesis using h2 by (rule_tac x = a in bexI, auto) |
|
491 qed |
|
492 qed |
|
493 qed |
|
494 |
|
495 |
|
496 text {* The following is a technical lemma, which helps to show the range finiteness of tag function. *} |
|
497 |
368 |
498 lemma finite_strict_prefix_set: |
369 lemma finite_strict_prefix_set: |
499 shows "finite {xa. xa < (x::'a list)}" |
370 shows "finite {xa. xa < (x::'a list)}" |
500 apply (induct x rule:rev_induct, simp) |
371 apply (induct x rule:rev_induct, simp) |
501 apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}") |
372 apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}") |
502 by (auto simp:strict_prefix_def) |
373 by (auto simp:strict_prefix_def) |
503 |
374 |
|
375 lemma append_eq_cases: |
|
376 assumes a: "x @ y = m @ n" "m \<noteq> []" |
|
377 shows "x \<le> m \<or> m < x" |
|
378 unfolding prefix_def strict_prefix_def using a |
|
379 by (auto simp add: append_eq_append_conv2) |
|
380 |
|
381 lemma star_spartitions_elim2: |
|
382 assumes a: "x @ z \<in> A\<star>" |
|
383 and b: "x \<noteq> []" |
|
384 shows "\<exists>(u, v) \<in> Partitions x. \<exists> (u', v') \<in> Partitions z. u < x \<and> u \<in> A\<star> \<and> v @ u' \<in> A \<and> v' \<in> A\<star>" |
|
385 proof - |
|
386 def S \<equiv> "{u | u v. (u, v) \<in> Partitions x \<and> u < x \<and> u \<in> A\<star> \<and> v @ z \<in> A\<star>}" |
|
387 have "finite {u. u < x}" by (rule finite_strict_prefix_set) |
|
388 then have "finite S" unfolding S_def |
|
389 by (rule rev_finite_subset) (auto) |
|
390 moreover |
|
391 have "S \<noteq> {}" using a b unfolding S_def Partitions_def |
|
392 by (auto simp: strict_prefix_def) |
|
393 ultimately have "\<exists> u_max \<in> S. \<forall> u \<in> S. length u \<le> length u_max" |
|
394 using finite_set_has_max2 by blast |
|
395 then obtain u_max v |
|
396 where h0: "(u_max, v) \<in> Partitions x" |
|
397 and h1: "u_max < x" |
|
398 and h2: "u_max \<in> A\<star>" |
|
399 and h3: "v @ z \<in> A\<star>" |
|
400 and h4: "\<forall> u v. (u, v) \<in> Partitions x \<and> u < x \<and> u \<in> A\<star> \<and> v @ z \<in> A\<star> \<longrightarrow> length u \<le> length u_max" |
|
401 unfolding S_def Partitions_def by blast |
|
402 have q: "v \<noteq> []" using h0 h1 b unfolding Partitions_def by auto |
|
403 from h3 obtain a b |
|
404 where i1: "(a, b) \<in> Partitions (v @ z)" |
|
405 and i2: "a \<in> A" |
|
406 and i3: "b \<in> A\<star>" |
|
407 and i4: "a \<noteq> []" |
|
408 unfolding Partitions_def |
|
409 using q by (auto dest: star_decom) |
|
410 have "v \<le> a" |
|
411 proof (rule ccontr) |
|
412 assume a: "\<not>(v \<le> a)" |
|
413 from i1 have i1': "a @ b = v @ z" unfolding Partitions_def by simp |
|
414 then have "a \<le> v \<or> v < a" using append_eq_cases q by blast |
|
415 then have q: "a < v" using a unfolding strict_prefix_def prefix_def by auto |
|
416 then obtain as where eq: "a @ as = v" unfolding strict_prefix_def prefix_def by auto |
|
417 have "(u_max @ a, as) \<in> Partitions x" using eq h0 unfolding Partitions_def by auto |
|
418 moreover |
|
419 have "u_max @ a < x" using h0 eq q unfolding Partitions_def strict_prefix_def prefix_def by auto |
|
420 moreover |
|
421 have "u_max @ a \<in> A\<star>" using i2 h2 by simp |
|
422 moreover |
|
423 have "as @ z \<in> A\<star>" using i1' i2 i3 eq by auto |
|
424 ultimately have "length (u_max @ a) \<le> length u_max" using h4 by blast |
|
425 moreover |
|
426 have "a \<noteq> []" using i4 . |
|
427 ultimately show "False" by auto |
|
428 qed |
|
429 with i1 obtain za zb |
|
430 where k1: "v @ za = a" |
|
431 and k2: "(za, zb) \<in> Partitions z" |
|
432 and k4: "zb = b" |
|
433 unfolding Partitions_def prefix_def |
|
434 by (auto simp add: append_eq_append_conv2) |
|
435 show "\<exists> (u, v) \<in> Partitions x. \<exists> (u', v') \<in> Partitions z. u < x \<and> u \<in> A\<star> \<and> v @ u' \<in> A \<and> v' \<in> A\<star>" |
|
436 using h0 k2 h1 h2 i2 k1 i3 k4 unfolding Partitions_def by blast |
|
437 qed |
|
438 |
|
439 |
|
440 definition |
|
441 tag_Star :: "'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang) set" |
|
442 where |
|
443 "tag_Star A \<equiv> (\<lambda>x. {\<approx>A `` {v} | u v. u < x \<and> u \<in> A\<star> \<and> (u, v) \<in> Partitions x})" |
|
444 |
504 |
445 |
505 lemma tag_Star_injI: |
446 lemma tag_Star_injI: |
506 fixes L\<^isub>1::"('a::finite) lang" |
447 fixes x::"'a list" |
507 assumes eq_tag: "tag_Star L\<^isub>1 v = tag_Star L\<^isub>1 w" |
448 assumes a: "tag_Star A x = tag_Star A y" |
508 shows "v \<approx>(L\<^isub>1\<star>) w" |
449 and c: "x @ z \<in> A\<star>" |
509 proof- |
450 and d: "x \<noteq> []" |
510 { fix x y z |
451 shows "y @ z \<in> A\<star>" |
511 assume xz_in_star: "x @ z \<in> L\<^isub>1\<star>" |
452 using c d |
512 and tag_xy: "tag_Star L\<^isub>1 x = tag_Star L\<^isub>1 y" |
453 apply(drule_tac star_spartitions_elim2) |
513 have "y @ z \<in> L\<^isub>1\<star>" |
454 apply(simp) |
514 proof(cases "x = []") |
455 apply(simp add: Partitions_def) |
515 case True |
456 apply(erule exE | erule conjE)+ |
516 with tag_xy have "y = []" |
457 apply(subgoal_tac "((\<approx>A) `` {b}) \<in> tag_Star A x") |
517 by (auto simp add: tag_Star_def strict_prefix_def) |
458 apply(simp add: a) |
518 thus ?thesis using xz_in_star True by simp |
459 apply(simp add: tag_Star_def) |
519 next |
460 apply(erule exE | erule conjE)+ |
520 case False |
461 apply(simp add: test) |
521 let ?S = "{xa::('a::finite) list. xa < x \<and> xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>}" |
462 apply(simp add: Partitions_def) |
522 have "finite ?S" |
463 apply(subgoal_tac "v @ aa \<in> A\<star>") |
523 by (rule_tac B = "{xa. xa < x}" in finite_subset) |
464 prefer 2 |
524 (auto simp: finite_strict_prefix_set) |
465 apply(simp add: str_eq_def) |
525 moreover have "?S \<noteq> {}" using False xz_in_star |
466 apply(subgoal_tac "(u @ v) @ aa @ ba \<in> A\<star>") |
526 by (simp, rule_tac x = "[]" in exI, auto simp:strict_prefix_def) |
467 apply(simp) |
527 ultimately have "\<exists> xa_max \<in> ?S. \<forall> xa \<in> ?S. length xa \<le> length xa_max" |
468 apply(simp (no_asm_use)) |
528 using finite_set_has_max by blast |
469 apply(rule append_in_starI) |
529 then obtain xa_max |
470 apply(simp) |
530 where h1: "xa_max < x" |
471 apply(simp (no_asm) only: append_assoc[symmetric]) |
531 and h2: "xa_max \<in> L\<^isub>1\<star>" |
472 apply(rule append_in_starI) |
532 and h3: "(x - xa_max) @ z \<in> L\<^isub>1\<star>" |
473 apply(simp) |
533 and h4:"\<forall> xa < x. xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star> |
474 apply(simp) |
534 \<longrightarrow> length xa \<le> length xa_max" |
475 apply(simp add: tag_Star_def) |
535 by blast |
476 apply(rule_tac x="a" in exI) |
536 obtain ya |
477 apply(rule_tac x="b" in exI) |
537 where h5: "ya < y" and h6: "ya \<in> L\<^isub>1\<star>" |
478 apply(simp) |
538 and eq_xya: "(x - xa_max) \<approx>L\<^isub>1 (y - ya)" |
479 apply(simp add: Partitions_def) |
539 proof- |
480 done |
540 from tag_xy have "{\<approx>L\<^isub>1 `` {x - xa} |xa. xa < x \<and> xa \<in> L\<^isub>1\<star>} = |
481 |
541 {\<approx>L\<^isub>1 `` {y - xa} |xa. xa < y \<and> xa \<in> L\<^isub>1\<star>}" (is "?left = ?right") |
482 lemma tag_Star_injI2: |
542 by (auto simp:tag_Star_def) |
483 fixes x::"'a list" |
543 moreover have "\<approx>L\<^isub>1 `` {x - xa_max} \<in> ?left" using h1 h2 by auto |
484 assumes a: "tag_Star A x = tag_Star A y" |
544 ultimately have "\<approx>L\<^isub>1 `` {x - xa_max} \<in> ?right" by simp |
485 and c: "x @ z \<in> A\<star>" |
545 thus ?thesis using that |
486 and d: "x = []" |
546 apply (simp add: Image_def str_eq_def) by blast |
487 shows "y @ z \<in> A\<star>" |
547 qed |
488 using c d |
548 have "(y - ya) @ z \<in> L\<^isub>1\<star>" |
489 apply(simp) |
549 proof- |
490 using a |
550 obtain za zb where eq_zab: "z = za @ zb" |
491 apply(simp add: tag_Star_def strict_prefix_def) |
551 and l_za: "(y - ya)@za \<in> L\<^isub>1" and ls_zb: "zb \<in> L\<^isub>1\<star>" |
492 apply(auto simp add: prefix_def Partitions_def) |
552 proof - |
493 by (metis Nil_in_star append_self_conv2) |
553 from h1 have "(x - xa_max) @ z \<noteq> []" |
494 |
554 unfolding strict_prefix_def prefix_def by auto |
|
555 from star_decom [OF h3 this] |
|
556 obtain a b where a_in: "a \<in> L\<^isub>1" |
|
557 and a_neq: "a \<noteq> []" and b_in: "b \<in> L\<^isub>1\<star>" |
|
558 and ab_max: "(x - xa_max) @ z = a @ b" by blast |
|
559 let ?za = "a - (x - xa_max)" and ?zb = "b" |
|
560 have pfx: "(x - xa_max) \<le> a" (is "?P1") |
|
561 and eq_z: "z = ?za @ ?zb" (is "?P2") |
|
562 proof - |
|
563 have "((x - xa_max) \<le> a \<and> (a - (x - xa_max)) @ b = z) \<or> |
|
564 (a < (x - xa_max) \<and> ((x - xa_max) - a) @ z = b)" |
|
565 using append_eq_dest[OF ab_max] by (auto simp:strict_prefix_def) |
|
566 moreover { |
|
567 assume np: "a < (x - xa_max)" |
|
568 and b_eqs: "((x - xa_max) - a) @ z = b" |
|
569 have "False" |
|
570 proof - |
|
571 let ?xa_max' = "xa_max @ a" |
|
572 have "?xa_max' < x" |
|
573 using np h1 by (clarsimp simp:strict_prefix_def diff_prefix) |
|
574 moreover have "?xa_max' \<in> L\<^isub>1\<star>" |
|
575 using a_in h2 by (auto) |
|
576 moreover have "(x - ?xa_max') @ z \<in> L\<^isub>1\<star>" |
|
577 using b_eqs b_in np h1 by (simp add:diff_diff_append) |
|
578 moreover have "\<not> (length ?xa_max' \<le> length xa_max)" |
|
579 using a_neq by simp |
|
580 ultimately show ?thesis using h4 by blast |
|
581 qed } |
|
582 ultimately show ?P1 and ?P2 by auto |
|
583 qed |
|
584 hence "(x - xa_max)@?za \<in> L\<^isub>1" using a_in unfolding prefix_def by auto |
|
585 with eq_xya have "(y - ya) @ ?za \<in> L\<^isub>1" |
|
586 by (auto simp: str_eq_def) |
|
587 with eq_z and b_in |
|
588 show ?thesis using that by blast |
|
589 qed |
|
590 have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" using l_za ls_zb |
|
591 by (rule_tac append_in_starI) (auto) |
|
592 with eq_zab show ?thesis by simp |
|
593 qed |
|
594 with h5 h6 show ?thesis |
|
595 unfolding strict_prefix_def prefix_def by auto |
|
596 qed |
|
597 } |
|
598 from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]] |
|
599 show ?thesis unfolding str_eq_def by blast |
|
600 qed |
|
601 |
495 |
602 lemma quot_star_finiteI [intro]: |
496 lemma quot_star_finiteI [intro]: |
603 fixes A::"('a::finite) lang" |
497 fixes A::"('a::finite) lang" |
604 assumes finite1: "finite (UNIV // \<approx>A)" |
498 assumes finite1: "finite (UNIV // \<approx>A)" |
605 shows "finite (UNIV // \<approx>(A\<star>))" |
499 shows "finite (UNIV // \<approx>(A\<star>))" |
606 proof (rule_tac tag = "tag_Star A" in tag_finite_imageD) |
500 proof (rule_tac tag = "tag_Star A" in tag_finite_imageD) |
607 show "\<And>x y. tag_Star A x = tag_Star A y \<Longrightarrow> x \<approx>(A\<star>) y" |
501 have "=(tag_Star A)= \<subseteq> \<approx>(A\<star>)" |
608 by (rule tag_Star_injI) |
502 apply(rule test_refined_intro) |
|
503 apply(case_tac "x=[]") |
|
504 apply(rule tag_Star_injI2) |
|
505 prefer 3 |
|
506 apply(assumption) |
|
507 prefer 2 |
|
508 apply(assumption) |
|
509 apply(simp add: tag_eq_def) |
|
510 apply(rule tag_Star_injI) |
|
511 prefer 3 |
|
512 apply(assumption) |
|
513 prefer 2 |
|
514 apply(assumption) |
|
515 unfolding tag_eq_def |
|
516 apply(simp) |
|
517 done |
|
518 then show "\<And>x y. tag_Star A x = tag_Star A y \<Longrightarrow> x \<approx>(A\<star>) y" |
|
519 apply(simp add: tag_eq_def) |
|
520 apply(auto) |
|
521 done |
609 next |
522 next |
610 have *: "finite (Pow (UNIV // \<approx>A))" |
523 have *: "finite (Pow (UNIV // \<approx>A))" |
611 using finite1 by auto |
524 using finite1 by auto |
612 show "finite (range (tag_Star A))" |
525 show "finite (range (tag_Star A))" |
613 unfolding tag_Star_def |
526 unfolding tag_Star_def |
614 apply(rule finite_subset[OF _ *]) |
527 apply(rule finite_subset[OF _ *]) |
615 unfolding quotient_def |
528 unfolding quotient_def |
616 by auto |
529 apply(auto) |
|
530 done |
617 qed |
531 qed |
618 |
532 |
619 subsubsection{* The conclusion *} |
533 subsubsection{* The conclusion *} |
620 |
534 |
621 lemma Myhill_Nerode2: |
535 lemma Myhill_Nerode2: |