equal
deleted
inserted
replaced
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: strict_suffix_def) |
379 by (force simp add: strict_suffix_def suffix_def) |
380 define f where "f \<equiv> \<lambda>(v, vs). Stars (v # vs)" |
380 define f where "f \<equiv> \<lambda>(v, vs). Stars (v # vs)" |
381 define S1 where "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 define S2 where "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) |
402 apply(rule conjI) |
402 apply(rule conjI) |
403 apply(rule_tac x="flat a" in exI) |
403 apply(rule_tac x="flat a" in exI) |
404 apply(rule conjI) |
404 apply(rule conjI) |
405 apply(rule_tac x="flats list" in exI) |
405 apply(rule_tac x="flats list" in exI) |
406 apply(simp) |
406 apply(simp) |
407 apply(blast) |
407 apply(blast) |
|
408 apply(simp add: suffix_def) |
408 using Prf.intros(6) by blast |
409 using Prf.intros(6) by blast |
409 ultimately |
410 ultimately |
410 show "finite (LV (STAR r) s)" by (simp add: finite_subset) |
411 show "finite (LV (STAR r) s)" by (simp add: finite_subset) |
411 qed |
412 qed |
412 |
413 |