equal
deleted
inserted
replaced
205 |
205 |
206 |
206 |
207 subsection {* Case for @{text "Times"} *} |
207 subsection {* Case for @{text "Times"} *} |
208 |
208 |
209 definition |
209 definition |
210 "Partitions x \<equiv> {(x\<^isub>p, x\<^isub>s). x\<^isub>p @ x\<^isub>s = x}" |
210 "Partitions x \<equiv> {(x\<^sub>p, x\<^sub>s). x\<^sub>p @ x\<^sub>s = x}" |
211 |
211 |
212 lemma conc_partitions_elim: |
212 lemma conc_partitions_elim: |
213 assumes "x \<in> A \<cdot> B" |
213 assumes "x \<in> A \<cdot> B" |
214 shows "\<exists>(u, v) \<in> Partitions x. u \<in> A \<and> v \<in> B" |
214 shows "\<exists>(u, v) \<in> Partitions x. u \<in> A \<and> v \<in> B" |
215 using assms unfolding conc_def Partitions_def |
215 using assms unfolding conc_def Partitions_def |
232 done |
232 done |
233 |
233 |
234 definition |
234 definition |
235 tag_Times :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang \<times> 'a lang set" |
235 tag_Times :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang \<times> 'a lang set" |
236 where |
236 where |
237 "tag_Times A B \<equiv> \<lambda>x. (\<approx>A `` {x}, {(\<approx>B `` {x\<^isub>s}) | x\<^isub>p x\<^isub>s. x\<^isub>p \<in> A \<and> (x\<^isub>p, x\<^isub>s) \<in> Partitions x})" |
237 "tag_Times A B \<equiv> \<lambda>x. (\<approx>A `` {x}, {(\<approx>B `` {x\<^sub>s}) | x\<^sub>p x\<^sub>s. x\<^sub>p \<in> A \<and> (x\<^sub>p, x\<^sub>s) \<in> Partitions x})" |
238 |
238 |
239 lemma tag_Times_injI: |
239 lemma tag_Times_injI: |
240 assumes a: "tag_Times A B x = tag_Times A B y" |
240 assumes a: "tag_Times A B x = tag_Times A B y" |
241 and c: "x @ z \<in> A \<cdot> B" |
241 and c: "x @ z \<in> A \<cdot> B" |
242 shows "y @ z \<in> A \<cdot> B" |
242 shows "y @ z \<in> A \<cdot> B" |