243 qed |
243 qed |
244 qed |
244 qed |
245 |
245 |
246 subsection {* Lemmas for basic cases *} |
246 subsection {* Lemmas for basic cases *} |
247 |
247 |
248 text {* |
248 subsection {* The case for @{const "NULL"} *} |
249 The the final result of this direction is in @{text "easier_direction"}, which |
249 |
250 is an induction on the structure of regular expressions. There is one case |
250 lemma quot_null_eq: |
251 for each regular expression operator. For basic operators such as @{text "NULL, EMPTY, CHAR c"}, |
251 shows "(UNIV // \<approx>{}) = ({UNIV}::lang set)" |
252 the finiteness of their language partition can be established directly with no need |
252 unfolding quotient_def Image_def str_eq_rel_def by auto |
253 of taggiing. This section contains several technical lemma for these base cases. |
253 |
254 |
254 lemma quot_null_finiteI [intro]: |
255 The inductive cases involve operators @{text "ALT, SEQ"} and @{text "STAR"}. |
255 shows "finite ((UNIV // \<approx>{})::lang set)" |
256 Tagging functions need to be defined individually for each of them. There will be one |
256 unfolding quot_null_eq by simp |
257 dedicated section for each of these cases, and each section goes virtually the same way: |
257 |
258 gives definition of the tagging function and prove that strings |
258 |
259 with the same tag are equivalent. |
259 subsection {* The case for @{const "EMPTY"} *} |
260 *} |
260 |
261 |
261 |
262 lemma quot_empty_subset: |
262 lemma quot_empty_subset: |
263 "UNIV // (\<approx>{[]}) \<subseteq> {{[]}, UNIV - {[]}}" |
263 "UNIV // (\<approx>{[]}) \<subseteq> {{[]}, UNIV - {[]}}" |
264 proof |
264 proof |
265 fix x |
265 fix x |
266 assume "x \<in> UNIV // \<approx>{[]}" |
266 assume "x \<in> UNIV // \<approx>{[]}" |
267 then obtain y where h: "x = {z. (y, z) \<in> \<approx>{[]}}" |
267 then obtain y where h: "x = {z. (y, z) \<in> \<approx>{[]}}" |
268 unfolding quotient_def Image_def by blast |
268 unfolding quotient_def Image_def by blast |
269 show "x \<in> {{[]}, UNIV - {[]}}" |
269 show "x \<in> {{[]}, UNIV - {[]}}" |
270 proof (cases "y = []") |
270 proof (cases "y = []") |
271 case True with h |
271 case True with h |
272 have "x = {[]}" by (auto simp:str_eq_rel_def) |
272 have "x = {[]}" by (auto simp: str_eq_rel_def) |
273 thus ?thesis by simp |
273 thus ?thesis by simp |
274 next |
274 next |
275 case False with h |
275 case False with h |
276 have "x = UNIV - {[]}" by (auto simp:str_eq_rel_def) |
276 have "x = UNIV - {[]}" by (auto simp: str_eq_rel_def) |
277 thus ?thesis by simp |
277 thus ?thesis by simp |
278 qed |
278 qed |
279 qed |
279 qed |
|
280 |
|
281 lemma quot_empty_finiteI [intro]: |
|
282 shows "finite (UNIV // (\<approx>{[]}))" |
|
283 by (rule finite_subset[OF quot_empty_subset]) (simp) |
|
284 |
|
285 |
|
286 subsection {* The case for @{const "CHAR"} *} |
280 |
287 |
281 lemma quot_char_subset: |
288 lemma quot_char_subset: |
282 "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}" |
289 "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}" |
283 proof |
290 proof |
284 fix x |
291 fix x |
301 by (auto simp add:str_eq_rel_def) |
308 by (auto simp add:str_eq_rel_def) |
302 } ultimately show ?thesis by blast |
309 } ultimately show ?thesis by blast |
303 qed |
310 qed |
304 qed |
311 qed |
305 |
312 |
|
313 lemma quot_char_finiteI [intro]: |
|
314 shows "finite (UNIV // (\<approx>{[c]}))" |
|
315 by (rule finite_subset[OF quot_char_subset]) (simp) |
|
316 |
|
317 |
|
318 |
306 subsection {* The case for @{text "SEQ"}*} |
319 subsection {* The case for @{text "SEQ"}*} |
307 |
320 |
308 definition |
321 definition |
309 "tag_str_SEQ L\<^isub>1 L\<^isub>2 x \<equiv> |
322 tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)" |
310 ((\<approx>L\<^isub>1) `` {x}, {(\<approx>L\<^isub>2) `` {x - xa}| xa. xa \<le> x \<and> xa \<in> L\<^isub>1})" |
323 where |
311 |
324 "tag_str_SEQ L1 L2 = (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa. xa \<le> x \<and> xa \<in> L1}))" |
312 lemma tag_str_seq_range_finite: |
325 |
313 "\<lbrakk>finite (UNIV // \<approx>L\<^isub>1); finite (UNIV // \<approx>L\<^isub>2)\<rbrakk> |
|
314 \<Longrightarrow> finite (range (tag_str_SEQ L\<^isub>1 L\<^isub>2))" |
|
315 apply (rule_tac B = "(UNIV // \<approx>L\<^isub>1) \<times> (Pow (UNIV // \<approx>L\<^isub>2))" in finite_subset) |
|
316 by (auto simp:tag_str_SEQ_def Image_def quotient_def split:if_splits) |
|
317 |
326 |
318 lemma append_seq_elim: |
327 lemma append_seq_elim: |
319 assumes "x @ y \<in> L\<^isub>1 ;; L\<^isub>2" |
328 assumes "x @ y \<in> L\<^isub>1 ;; L\<^isub>2" |
320 shows "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> L\<^isub>2) \<or> |
329 shows "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> L\<^isub>2) \<or> |
321 (\<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> L\<^isub>2)" |
330 (\<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> L\<^isub>2)" |
381 qed |
390 qed |
382 } thus "tag_str_SEQ L\<^isub>1 L\<^isub>2 m = tag_str_SEQ L\<^isub>1 L\<^isub>2 n \<Longrightarrow> m \<approx>(L\<^isub>1 ;; L\<^isub>2) n" |
391 } thus "tag_str_SEQ L\<^isub>1 L\<^isub>2 m = tag_str_SEQ L\<^isub>1 L\<^isub>2 n \<Longrightarrow> m \<approx>(L\<^isub>1 ;; L\<^isub>2) n" |
383 by (auto simp add: str_eq_def str_eq_rel_def) |
392 by (auto simp add: str_eq_def str_eq_rel_def) |
384 qed |
393 qed |
385 |
394 |
386 lemma quot_seq_finiteI: |
395 lemma quot_seq_finiteI [intro]: |
387 "\<lbrakk>finite (UNIV // \<approx>L\<^isub>1); finite (UNIV // \<approx>L\<^isub>2)\<rbrakk> |
396 fixes L1 L2::"lang" |
388 \<Longrightarrow> finite (UNIV // \<approx>(L\<^isub>1 ;; L\<^isub>2))" |
397 assumes fin1: "finite (UNIV // \<approx>L1)" |
389 apply (rule_tac tag = "tag_str_SEQ L\<^isub>1 L\<^isub>2" in tag_finite_imageD) |
398 and fin2: "finite (UNIV // \<approx>L2)" |
390 by (auto intro:tag_str_SEQ_injI elim:tag_str_seq_range_finite) |
399 shows "finite (UNIV // \<approx>(L1 ;; L2))" |
391 |
400 proof (rule_tac tag = "tag_str_SEQ L1 L2" in tag_finite_imageD) |
392 subsection {* The case for @{text "ALT"} *} |
401 show "\<And>x y. tag_str_SEQ L1 L2 x = tag_str_SEQ L1 L2 y \<Longrightarrow> x \<approx>(L1 ;; L2) y" |
|
402 by (rule tag_str_SEQ_injI) |
|
403 next |
|
404 have *: "finite ((UNIV // \<approx>L1) \<times> (Pow (UNIV // \<approx>L2)))" |
|
405 using fin1 fin2 by auto |
|
406 show "finite (range (tag_str_SEQ L1 L2))" |
|
407 unfolding tag_str_SEQ_def |
|
408 apply(rule finite_subset[OF _ *]) |
|
409 unfolding quotient_def |
|
410 by auto |
|
411 qed |
|
412 |
|
413 subsection {* The case for @{const ALT} *} |
393 |
414 |
394 definition |
415 definition |
395 "tag_str_ALT L\<^isub>1 L\<^isub>2 (x::string) \<equiv> ((\<approx>L\<^isub>1) `` {x}, (\<approx>L\<^isub>2) `` {x})" |
416 tag_str_ALT :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang)" |
396 |
417 where |
397 lemma quot_union_finiteI: |
418 "tag_str_ALT L1 L2 = (\<lambda>x. (\<approx>L1 `` {x}, \<approx>L2 `` {x}))" |
398 assumes finite1: "finite (UNIV // \<approx>(L\<^isub>1::string set))" |
419 |
399 and finite2: "finite (UNIV // \<approx>L\<^isub>2)" |
420 |
400 shows "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))" |
421 lemma quot_union_finiteI [intro]: |
401 proof (rule_tac tag = "tag_str_ALT L\<^isub>1 L\<^isub>2" in tag_finite_imageD) |
422 fixes L1 L2::"lang" |
402 show "\<And>m n. tag_str_ALT L\<^isub>1 L\<^isub>2 m = tag_str_ALT L\<^isub>1 L\<^isub>2 n \<Longrightarrow> m \<approx>(L\<^isub>1 \<union> L\<^isub>2) n" |
423 assumes finite1: "finite (UNIV // \<approx>L1)" |
403 unfolding tag_str_ALT_def str_eq_def Image_def str_eq_rel_def by auto |
424 and finite2: "finite (UNIV // \<approx>L2)" |
|
425 shows "finite (UNIV // \<approx>(L1 \<union> L2))" |
|
426 proof (rule_tac tag = "tag_str_ALT L1 L2" in tag_finite_imageD) |
|
427 show "\<And>x y. tag_str_ALT L1 L2 x = tag_str_ALT L1 L2 y \<Longrightarrow> x \<approx>(L1 \<union> L2) y" |
|
428 unfolding tag_str_ALT_def |
|
429 unfolding str_eq_def |
|
430 unfolding Image_def |
|
431 unfolding str_eq_rel_def |
|
432 by auto |
404 next |
433 next |
405 show "finite (range (tag_str_ALT L\<^isub>1 L\<^isub>2))" using finite1 finite2 |
434 have *: "finite ((UNIV // \<approx>L1) \<times> (UNIV // \<approx>L2))" |
406 apply (rule_tac B = "(UNIV // \<approx>L\<^isub>1) \<times> (UNIV // \<approx>L\<^isub>2)" in finite_subset) |
435 using finite1 finite2 by auto |
407 by (auto simp:tag_str_ALT_def Image_def quotient_def) |
436 show "finite (range (tag_str_ALT L1 L2))" |
408 qed |
437 unfolding tag_str_ALT_def |
409 |
438 apply(rule finite_subset[OF _ *]) |
410 subsection {* |
439 unfolding quotient_def |
411 The case for @{text "STAR"} |
440 by auto |
412 *} |
441 qed |
|
442 |
|
443 subsection {* The case for @{const "STAR"} *} |
413 |
444 |
414 text {* |
445 text {* |
415 This turned out to be the trickiest case. |
446 This turned out to be the trickiest case. |
416 Any string @{text "x"} in language @{text "L\<^isub>1\<star>"}, |
447 Any string @{text "x"} in language @{text "L\<^isub>1\<star>"}, |
417 can be splited into a prefix @{text "xa \<in> L\<^isub>1\<star>"} and a suffix @{text "x - xa \<in> L\<^isub>1"}. |
448 can be splited into a prefix @{text "xa \<in> L\<^isub>1\<star>"} and a suffix @{text "x - xa \<in> L\<^isub>1"}. |
418 For one such @{text "x"}, there can be many such splits. The tagging of @{text "x"} is then |
449 For one such @{text "x"}, there can be many such splits. The tagging of @{text "x"} is then |
419 defined by collecting the @{text "L\<^isub>1"}-state of the suffixes from every possible split. |
450 defined by collecting the @{text "L\<^isub>1"}-state of the suffixes from every possible split. |
420 *} |
451 *} |
421 |
|
422 (* I will make some illustrations for it. *) |
|
423 |
452 |
424 definition |
453 definition |
425 "tag_str_STAR L\<^isub>1 x \<equiv> {(\<approx>L\<^isub>1) `` {x - xa} | xa. xa < x \<and> xa \<in> L\<^isub>1\<star>}" |
454 tag_str_STAR :: "lang \<Rightarrow> string \<Rightarrow> lang set" |
|
455 where |
|
456 "tag_str_STAR L1 = (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<star>})" |
|
457 |
|
458 |
426 |
459 |
427 text {* A technical lemma. *} |
460 text {* A technical lemma. *} |
428 lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> |
461 lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> |
429 (\<exists> max \<in> A. \<forall> a \<in> A. f a <= (f max :: nat))" |
462 (\<exists> max \<in> A. \<forall> a \<in> A. f a <= (f max :: nat))" |
430 proof (induct rule:finite.induct) |
463 proof (induct rule:finite.induct) |
455 lemma finite_strict_prefix_set: "finite {xa. xa < (x::string)}" |
488 lemma finite_strict_prefix_set: "finite {xa. xa < (x::string)}" |
456 apply (induct x rule:rev_induct, simp) |
489 apply (induct x rule:rev_induct, simp) |
457 apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}") |
490 apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}") |
458 by (auto simp:strict_prefix_def) |
491 by (auto simp:strict_prefix_def) |
459 |
492 |
460 text {* |
|
461 The following lemma @{text "tag_str_star_range_finite"} establishes the range finiteness |
|
462 of the tagging function. |
|
463 *} |
|
464 lemma tag_str_star_range_finite: |
|
465 "finite (UNIV // \<approx>L\<^isub>1) \<Longrightarrow> finite (range (tag_str_STAR L\<^isub>1))" |
|
466 apply (rule_tac B = "Pow (UNIV // \<approx>L\<^isub>1)" in finite_subset) |
|
467 by (auto simp:tag_str_STAR_def Image_def |
|
468 quotient_def split:if_splits) |
|
469 |
493 |
470 text {* |
494 text {* |
471 The following lemma @{text "tag_str_STAR_injI"} establishes the injectivity of |
495 The following lemma @{text "tag_str_STAR_injI"} establishes the injectivity of |
472 the tagging function for case @{text "STAR"}. |
496 the tagging function for case @{text "STAR"}. |
473 *} |
497 *} |
578 from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]] |
602 from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]] |
579 -- {* The thesis is proved as a trival consequence: *} |
603 -- {* The thesis is proved as a trival consequence: *} |
580 show ?thesis by (unfold str_eq_def str_eq_rel_def, blast) |
604 show ?thesis by (unfold str_eq_def str_eq_rel_def, blast) |
581 qed |
605 qed |
582 |
606 |
583 lemma quot_star_finiteI: |
607 lemma quot_star_finiteI [intro]: |
584 "finite (UNIV // \<approx>L\<^isub>1) \<Longrightarrow> finite (UNIV // \<approx>(L\<^isub>1\<star>))" |
608 fixes L1::"lang" |
585 apply (rule_tac tag = "tag_str_STAR L\<^isub>1" in tag_finite_imageD) |
609 assumes finite1: "finite (UNIV // \<approx>L1)" |
586 by (auto intro:tag_str_STAR_injI elim:tag_str_star_range_finite) |
610 shows "finite (UNIV // \<approx>(L1\<star>))" |
587 |
611 proof (rule_tac tag = "tag_str_STAR L1" in tag_finite_imageD) |
588 subsection {* |
612 show "\<And>x y. tag_str_STAR L1 x = tag_str_STAR L1 y \<Longrightarrow> x \<approx>(L1\<star>) y" |
589 The main lemma |
613 by (rule tag_str_STAR_injI) |
590 *} |
|
591 |
|
592 lemma easier_direction: |
|
593 "Lang = L (r::rexp) \<Longrightarrow> finite (UNIV // (\<approx>Lang))" |
|
594 proof (induct arbitrary:Lang rule:rexp.induct) |
|
595 case NULL |
|
596 have "UNIV // (\<approx>{}) \<subseteq> {UNIV} " |
|
597 by (auto simp:quotient_def str_eq_rel_def str_eq_def) |
|
598 with prems show "?case" by (auto intro:finite_subset) |
|
599 next |
614 next |
600 case EMPTY |
615 have *: "finite (Pow (UNIV // \<approx>L1))" |
601 have "UNIV // (\<approx>{[]}) \<subseteq> {{[]}, UNIV - {[]}}" |
616 using finite1 by auto |
602 by (rule quot_empty_subset) |
617 show "finite (range (tag_str_STAR L1))" |
603 with prems show ?case by (auto intro:finite_subset) |
618 unfolding tag_str_STAR_def |
604 next |
619 apply(rule finite_subset[OF _ *]) |
605 case (CHAR c) |
620 unfolding quotient_def |
606 have "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}" |
621 by auto |
607 by (rule quot_char_subset) |
622 qed |
608 with prems show ?case by (auto intro:finite_subset) |
623 |
609 next |
624 |
610 case (SEQ r\<^isub>1 r\<^isub>2) |
625 lemma rexp_imp_finite: |
611 have "\<lbrakk>finite (UNIV // \<approx>(L r\<^isub>1)); finite (UNIV // \<approx>(L r\<^isub>2))\<rbrakk> |
626 fixes r::"rexp" |
612 \<Longrightarrow> finite (UNIV // \<approx>(L r\<^isub>1 ;; L r\<^isub>2))" |
627 shows "finite (UNIV // \<approx>(L r))" |
613 by (erule quot_seq_finiteI, simp) |
628 by (induct r) (auto) |
614 with prems show ?case by simp |
|
615 next |
|
616 case (ALT r\<^isub>1 r\<^isub>2) |
|
617 have "\<lbrakk>finite (UNIV // \<approx>(L r\<^isub>1)); finite (UNIV // \<approx>(L r\<^isub>2))\<rbrakk> |
|
618 \<Longrightarrow> finite (UNIV // \<approx>(L r\<^isub>1 \<union> L r\<^isub>2))" |
|
619 by (erule quot_union_finiteI, simp) |
|
620 with prems show ?case by simp |
|
621 next |
|
622 case (STAR r) |
|
623 have "finite (UNIV // \<approx>(L r)) |
|
624 \<Longrightarrow> finite (UNIV // \<approx>((L r)\<star>))" |
|
625 by (erule quot_star_finiteI) |
|
626 with prems show ?case by simp |
|
627 qed |
|
628 |
629 |
629 end |
630 end |
630 |
631 |
631 (* |
632 (* |
632 lemma refined_quotient_union_eq: |
633 lemma refined_quotient_union_eq: |