equal
deleted
inserted
replaced
479 *} |
479 *} |
480 |
480 |
481 definition |
481 definition |
482 tag_str_STAR :: "lang \<Rightarrow> string \<Rightarrow> lang set" |
482 tag_str_STAR :: "lang \<Rightarrow> string \<Rightarrow> lang set" |
483 where |
483 where |
484 "tag_str_STAR L1 \<equiv> (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<star>})" |
484 "tag_str_STAR L1 \<equiv> (\<lambda>x. {\<approx>L1 `` {x - x'} | x'. x' < x \<and> x' \<in> L1\<star>})" |
485 |
485 |
486 text {* A technical lemma. *} |
486 text {* A technical lemma. *} |
487 lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> |
487 lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> |
488 (\<exists> max \<in> A. \<forall> a \<in> A. f a <= (f max :: nat))" |
488 (\<exists> max \<in> A. \<forall> a \<in> A. f a <= (f max :: nat))" |
489 proof (induct rule:finite.induct) |
489 proof (induct rule:finite.induct) |