215 |
215 |
216 |
216 |
217 subsubsection {* The inductive case for @{text "Times"} *} |
217 subsubsection {* The inductive case for @{text "Times"} *} |
218 |
218 |
219 definition |
219 definition |
220 "Partitions s \<equiv> {(u, v). u @ v = s}" |
220 "Partitions x \<equiv> {(x\<^isub>p, x\<^isub>s). x\<^isub>p @ x\<^isub>s = x}" |
221 |
221 |
222 lemma conc_partitions_elim: |
222 lemma conc_partitions_elim: |
223 assumes "x \<in> A \<cdot> B" |
223 assumes "x \<in> A \<cdot> B" |
224 shows "\<exists>(u, v) \<in> Partitions x. u \<in> A \<and> v \<in> B" |
224 shows "\<exists>(u, v) \<in> Partitions x. u \<in> A \<and> v \<in> B" |
225 using assms unfolding conc_def Partitions_def |
225 using assms unfolding conc_def Partitions_def |
239 apply(simp) |
239 apply(simp) |
240 apply(simp add: str_eq_def) |
240 apply(simp add: str_eq_def) |
241 apply(metis append_Nil2) |
241 apply(metis append_Nil2) |
242 done |
242 done |
243 |
243 |
244 |
244 definition |
245 abbreviation |
245 tag_Times :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang \<times> 'a lang set" |
246 tag_Times_1 :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang" |
|
247 where |
246 where |
248 "tag_Times_1 A B \<equiv> \<lambda>x. \<approx>A `` {x}" |
247 "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})" |
249 |
|
250 abbreviation |
|
251 tag_Times_2 :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang) set" |
|
252 where |
|
253 "tag_Times_2 A B \<equiv> \<lambda>x. {(\<approx>A `` {u}, \<approx>B `` {v}) | u v. (u, v) \<in> Partitions x}" |
|
254 |
|
255 definition |
|
256 tag_Times :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang \<times> ('a lang \<times> 'a lang) set" |
|
257 where |
|
258 "tag_Times A B \<equiv> \<lambda>x. (tag_Times_1 A B x, tag_Times_2 A B x)" |
|
259 |
248 |
260 lemma tag_Times_injI: |
249 lemma tag_Times_injI: |
261 assumes a: "tag_Times_1 A B x = tag_Times_1 A B y" |
250 assumes a: "tag_Times A B x = tag_Times A B y" |
262 and b: "tag_Times_2 A B x = tag_Times_2 A B y" |
|
263 and c: "x @ z \<in> A \<cdot> B" |
251 and c: "x @ z \<in> A \<cdot> B" |
264 shows "y @ z \<in> A \<cdot> B" |
252 shows "y @ z \<in> A \<cdot> B" |
265 proof - |
253 proof - |
266 from c obtain u v where |
254 from c obtain u v where |
267 h1: "(u, v) \<in> Partitions (x @ z)" and |
255 h1: "(u, v) \<in> Partitions (x @ z)" and |
271 then obtain us |
259 then obtain us |
272 where "(x = u @ us \<and> us @ z = v) \<or> (x @ us = u \<and> z = us @ v)" |
260 where "(x = u @ us \<and> us @ z = v) \<or> (x @ us = u \<and> z = us @ v)" |
273 by (auto simp add: append_eq_append_conv2) |
261 by (auto simp add: append_eq_append_conv2) |
274 moreover |
262 moreover |
275 { assume eq: "x = u @ us" "us @ z = v" |
263 { assume eq: "x = u @ us" "us @ z = v" |
276 have "(\<approx>A `` {u}, \<approx>B `` {us}) \<in> tag_Times_2 A B x" |
264 have "(\<approx>B `` {us}) \<in> snd (tag_Times A B x)" |
277 unfolding Partitions_def using eq by (auto simp add: str_eq_def) |
265 unfolding Partitions_def tag_Times_def using h2 eq |
278 then have "(\<approx>A `` {u}, \<approx>B `` {us}) \<in> tag_Times_2 A B y" |
266 by (auto simp add: str_eq_def) |
279 using b by simp |
267 then have "(\<approx>B `` {us}) \<in> snd (tag_Times A B y)" |
|
268 using a by simp |
280 then obtain u' us' where |
269 then obtain u' us' where |
281 q1: "\<approx>A `` {u} = \<approx>A `` {u'}" and |
270 q1: "u' \<in> A" and |
282 q2: "\<approx>B `` {us} = \<approx>B `` {us'}" and |
271 q2: "\<approx>B `` {us} = \<approx>B `` {us'}" and |
283 q3: "(u', us') \<in> Partitions y" by auto |
272 q3: "(u', us') \<in> Partitions y" |
284 from q1 h2 have "u' \<in> A" |
273 unfolding tag_Times_def by auto |
285 using equiv_class_member by auto |
274 from q2 h3 eq |
286 moreover from q2 h3 eq |
|
287 have "us' @ z \<in> B" |
275 have "us' @ z \<in> B" |
288 unfolding Image_def str_eq_def by auto |
276 unfolding Image_def str_eq_def by auto |
289 ultimately have "y @ z \<in> A \<cdot> B" using q3 |
277 then have "y @ z \<in> A \<cdot> B" using q1 q3 |
290 unfolding Partitions_def by auto |
278 unfolding Partitions_def by auto |
291 } |
279 } |
292 moreover |
280 moreover |
293 { assume eq: "x @ us = u" "z = us @ v" |
281 { assume eq: "x @ us = u" "z = us @ v" |
294 have "(\<approx>A `` {x}) = tag_Times_1 A B x" by simp |
282 have "(\<approx>A `` {x}) = fst (tag_Times A B x)" |
295 then have "(\<approx>A `` {x}) = tag_Times_1 A B y" |
283 by (simp add: tag_Times_def) |
|
284 then have "(\<approx>A `` {x}) = fst (tag_Times A B y)" |
296 using a by simp |
285 using a by simp |
297 then have "\<approx>A `` {x} = \<approx>A `` {y}" by simp |
286 then have "\<approx>A `` {x} = \<approx>A `` {y}" |
|
287 by (simp add: tag_Times_def) |
298 moreover |
288 moreover |
299 have "x @ us \<in> A" using h2 eq by simp |
289 have "x @ us \<in> A" using h2 eq by simp |
300 ultimately |
290 ultimately |
301 have "y @ us \<in> A" using equiv_class_member |
291 have "y @ us \<in> A" using equiv_class_member |
302 unfolding Image_def str_eq_def by blast |
292 unfolding Image_def str_eq_def by blast |
317 (auto simp add: tag_Times_def tag_eq_def) |
307 (auto simp add: tag_Times_def tag_eq_def) |
318 then show "=tag_Times A B= \<subseteq> \<approx>(A \<cdot> B)" |
308 then show "=tag_Times A B= \<subseteq> \<approx>(A \<cdot> B)" |
319 by (rule refined_intro) |
309 by (rule refined_intro) |
320 (auto simp add: tag_eq_def) |
310 (auto simp add: tag_eq_def) |
321 next |
311 next |
322 have *: "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>A \<times> UNIV // \<approx>B)))" |
312 have *: "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))" |
323 using fin1 fin2 by auto |
313 using fin1 fin2 by auto |
324 show "finite (range (tag_Times A B))" |
314 show "finite (range (tag_Times A B))" |
325 unfolding tag_Times_def |
315 unfolding tag_Times_def |
326 apply(rule finite_subset[OF _ *]) |
316 apply(rule finite_subset[OF _ *]) |
327 unfolding quotient_def |
317 unfolding quotient_def |