equal
deleted
inserted
replaced
300 |
300 |
301 definition |
301 definition |
302 tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)" |
302 tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)" |
303 where |
303 where |
304 "tag_str_SEQ L1 L2 \<equiv> |
304 "tag_str_SEQ L1 L2 \<equiv> |
305 (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa. xa \<le> x \<and> xa \<in> L1}))" |
305 (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - x'}) | x'. x' \<le> x \<and> x' \<in> L1}))" |
306 |
306 |
307 text {* The following is a techical lemma which helps to split the @{text "x @ z \<in> L\<^isub>1 ;; L\<^isub>2"} mentioned above.*} |
307 text {* The following is a techical lemma which helps to split the @{text "x @ z \<in> L\<^isub>1 ;; L\<^isub>2"} mentioned above.*} |
308 |
308 |
309 lemma append_seq_elim: |
309 lemma append_seq_elim: |
310 assumes "x @ y \<in> L\<^isub>1 ;; L\<^isub>2" |
310 assumes "x @ y \<in> L\<^isub>1 ;; L\<^isub>2" |