328 unfolding LV_def |
328 unfolding LV_def |
329 by (auto intro: Prf.intros elim: Prf.cases) |
329 by (auto intro: Prf.intros elim: Prf.cases) |
330 |
330 |
331 |
331 |
332 abbreviation |
332 abbreviation |
333 "Prefixes s \<equiv> {s'. prefixeq s' s}" |
333 "Prefixes s \<equiv> {s'. prefix s' s}" |
334 |
334 |
335 abbreviation |
335 abbreviation |
336 "Suffixes s \<equiv> {s'. suffixeq s' s}" |
336 "Suffixes s \<equiv> {s'. suffix s' s}" |
337 |
337 |
338 abbreviation |
338 abbreviation |
339 "SSuffixes s \<equiv> {s'. suffix s' s}" |
339 "SSuffixes s \<equiv> {s'. strict_suffix s' s}" |
340 |
340 |
341 lemma Suffixes_cons [simp]: |
341 lemma Suffixes_cons [simp]: |
342 shows "Suffixes (c # s) = Suffixes s \<union> {c # s}" |
342 shows "Suffixes (c # s) = Suffixes s \<union> {c # s}" |
343 by (auto simp add: suffixeq_def Cons_eq_append_conv) |
343 by (auto simp add: suffix_def Cons_eq_append_conv) |
344 |
344 |
345 |
345 |
346 lemma finite_Suffixes: |
346 lemma finite_Suffixes: |
347 shows "finite (Suffixes s)" |
347 shows "finite (Suffixes s)" |
348 by (induct s) (simp_all) |
348 by (induct s) (simp_all) |
349 |
349 |
350 lemma finite_SSuffixes: |
350 lemma finite_SSuffixes: |
351 shows "finite (SSuffixes s)" |
351 shows "finite (SSuffixes s)" |
352 proof - |
352 proof - |
353 have "SSuffixes s \<subseteq> Suffixes s" |
353 have "SSuffixes s \<subseteq> Suffixes s" |
354 unfolding suffix_def suffixeq_def by auto |
354 unfolding strict_suffix_def suffix_def by auto |
355 then show "finite (SSuffixes s)" |
355 then show "finite (SSuffixes s)" |
356 using finite_Suffixes finite_subset by blast |
356 using finite_Suffixes finite_subset by blast |
357 qed |
357 qed |
358 |
358 |
359 lemma finite_Prefixes: |
359 lemma finite_Prefixes: |
362 have "finite (Suffixes (rev s))" |
362 have "finite (Suffixes (rev s))" |
363 by (rule finite_Suffixes) |
363 by (rule finite_Suffixes) |
364 then have "finite (rev ` Suffixes (rev s))" by simp |
364 then have "finite (rev ` Suffixes (rev s))" by simp |
365 moreover |
365 moreover |
366 have "rev ` (Suffixes (rev s)) = Prefixes s" |
366 have "rev ` (Suffixes (rev s)) = Prefixes s" |
367 unfolding suffixeq_def prefixeq_def image_def |
367 unfolding suffix_def prefix_def image_def |
368 by (auto)(metis rev_append rev_rev_ident)+ |
368 by (auto)(metis rev_append rev_rev_ident)+ |
369 ultimately show "finite (Prefixes s)" by simp |
369 ultimately show "finite (Prefixes s)" by simp |
370 qed |
370 qed |
371 |
371 |
372 lemma LV_STAR_finite: |
372 lemma LV_STAR_finite: |
374 shows "finite (LV (STAR r) s)" |
374 shows "finite (LV (STAR r) s)" |
375 proof(induct s rule: length_induct) |
375 proof(induct s rule: length_induct) |
376 fix s::"char list" |
376 fix s::"char list" |
377 assume "\<forall>s'. length s' < length s \<longrightarrow> finite (LV (STAR r) s')" |
377 assume "\<forall>s'. length s' < length s \<longrightarrow> finite (LV (STAR r) s')" |
378 then have IH: "\<forall>s' \<in> SSuffixes s. finite (LV (STAR r) s')" |
378 then have IH: "\<forall>s' \<in> SSuffixes s. finite (LV (STAR r) s')" |
379 by (auto simp add: suffix_def) |
379 by (auto simp add: strict_suffix_def) |
380 def f \<equiv> "\<lambda>(v, vs). Stars (v # vs)" |
380 define f where "f \<equiv> \<lambda>(v, vs). Stars (v # vs)" |
381 def S1 \<equiv> "\<Union>s' \<in> Prefixes s. LV r s'" |
381 define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r s'" |
382 def S2 \<equiv> "\<Union>s2 \<in> SSuffixes s. Stars -` (LV (STAR r) s2)" |
382 define S2 where "S2 \<equiv> \<Union>s2 \<in> SSuffixes s. Stars -` (LV (STAR r) s2)" |
383 have "finite S1" using assms |
383 have "finite S1" using assms |
384 unfolding S1_def by (simp_all add: finite_Prefixes) |
384 unfolding S1_def by (simp_all add: finite_Prefixes) |
385 moreover |
385 moreover |
386 with IH have "finite S2" unfolding S2_def |
386 with IH have "finite S2" unfolding S2_def |
387 by (auto simp add: finite_SSuffixes inj_on_def finite_vimageI) |
387 by (auto simp add: finite_SSuffixes inj_on_def finite_vimageI) |
388 ultimately |
388 ultimately |
389 have "finite ({Stars []} \<union> f ` (S1 \<times> S2))" by simp |
389 have "finite ({Stars []} \<union> f ` (S1 \<times> S2))" by simp |
390 moreover |
390 moreover |
391 have "LV (STAR r) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)" |
391 have "LV (STAR r) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)" |
392 unfolding S1_def S2_def f_def |
392 unfolding S1_def S2_def f_def |
393 unfolding LV_def image_def prefixeq_def suffix_def |
393 unfolding LV_def image_def prefix_def strict_suffix_def |
|
394 apply(auto) |
|
395 apply(case_tac x) |
394 apply(auto elim: Prf_elims) |
396 apply(auto elim: Prf_elims) |
395 apply(erule Prf_elims) |
397 apply(erule Prf_elims) |
396 apply(auto) |
398 apply(auto) |
397 apply(case_tac vs) |
399 apply(case_tac vs) |
398 apply(auto intro: Prf.intros) |
400 apply(auto intro: Prf.intros) |
399 done |
401 apply(rule exI) |
|
402 apply(rule conjI) |
|
403 apply(rule_tac x="flat a" in exI) |
|
404 apply(rule conjI) |
|
405 apply(rule_tac x="flats list" in exI) |
|
406 apply(simp) |
|
407 apply(blast) |
|
408 using Prf.intros(6) by blast |
400 ultimately |
409 ultimately |
401 show "finite (LV (STAR r) s)" by (simp add: finite_subset) |
410 show "finite (LV (STAR r) s)" by (simp add: finite_subset) |
402 qed |
411 qed |
403 |
412 |
404 |
413 |
416 next |
425 next |
417 case (ALT r1 r2 s) |
426 case (ALT r1 r2 s) |
418 then show "finite (LV (ALT r1 r2) s)" by (simp add: LV_simps) |
427 then show "finite (LV (ALT r1 r2) s)" by (simp add: LV_simps) |
419 next |
428 next |
420 case (SEQ r1 r2 s) |
429 case (SEQ r1 r2 s) |
421 def f \<equiv> "\<lambda>(v1, v2). Seq v1 v2" |
430 define f where "f \<equiv> \<lambda>(v1, v2). Seq v1 v2" |
422 def S1 \<equiv> "\<Union>s' \<in> Prefixes s. LV r1 s'" |
431 define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r1 s'" |
423 def S2 \<equiv> "\<Union>s' \<in> Suffixes s. LV r2 s'" |
432 define S2 where "S2 \<equiv> \<Union>s' \<in> Suffixes s. LV r2 s'" |
424 have IHs: "\<And>s. finite (LV r1 s)" "\<And>s. finite (LV r2 s)" by fact+ |
433 have IHs: "\<And>s. finite (LV r1 s)" "\<And>s. finite (LV r2 s)" by fact+ |
425 then have "finite S1" "finite S2" unfolding S1_def S2_def |
434 then have "finite S1" "finite S2" unfolding S1_def S2_def |
426 by (simp_all add: finite_Prefixes finite_Suffixes) |
435 by (simp_all add: finite_Prefixes finite_Suffixes) |
427 moreover |
436 moreover |
428 have "LV (SEQ r1 r2) s \<subseteq> f ` (S1 \<times> S2)" |
437 have "LV (SEQ r1 r2) s \<subseteq> f ` (S1 \<times> S2)" |
429 unfolding f_def S1_def S2_def |
438 unfolding f_def S1_def S2_def |
430 unfolding LV_def image_def prefixeq_def suffixeq_def |
439 unfolding LV_def image_def prefix_def suffix_def |
431 by (auto elim: Prf.cases) |
440 apply (auto elim!: Prf_elims) |
|
441 by (metis (mono_tags, lifting) mem_Collect_eq) |
432 ultimately |
442 ultimately |
433 show "finite (LV (SEQ r1 r2) s)" |
443 show "finite (LV (SEQ r1 r2) s)" |
434 by (simp add: finite_subset) |
444 by (simp add: finite_subset) |
435 next |
445 next |
436 case (STAR r s) |
446 case (STAR r s) |