16 str_eq :: "string \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> bool" ("_ \<approx>_ _") |
16 str_eq :: "string \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> bool" ("_ \<approx>_ _") |
17 where |
17 where |
18 "x \<approx>A y \<equiv> (x, y) \<in> (\<approx>A)" |
18 "x \<approx>A y \<equiv> (x, y) \<in> (\<approx>A)" |
19 |
19 |
20 text {* |
20 text {* |
21 The main lemma (@{text "rexp_imp_finite"}) is proved by a structural induction over regular expressions. |
21 The main lemma (@{text "rexp_imp_finite"}) is proved by a structural |
22 where base cases (cases for @{const "NULL"}, @{const "EMPTY"}, @{const "CHAR"}) are quite straightforward to |
22 induction over regular expressions. where base cases (cases for @{const |
23 proof. Real difficulty lies in inductive cases. By inductive hypothesis, languages defined by |
23 "NULL"}, @{const "EMPTY"}, @{const "CHAR"}) are quite straightforward to |
24 sub-expressions induce finite partitiions. Under such hypothsis, we need to prove that the language |
24 proof. Real difficulty lies in inductive cases. By inductive hypothesis, |
25 defined by the composite regular expression gives rise to finite partion. |
25 languages defined by sub-expressions induce finite partitiions. Under such |
26 The basic idea is to attach a tag @{text "tag(x)"} to every string |
26 hypothsis, we need to prove that the language defined by the composite |
27 @{text "x"}. The tagging fuction @{text "tag"} is carefully devised, which returns tags |
27 regular expression gives rise to finite partion. The basic idea is to |
28 made of equivalent classes of the partitions induced by subexpressoins, and therefore has a finite |
28 attach a tag @{text "tag(x)"} to every string @{text "x"}. The tagging |
29 range. Let @{text "Lang"} be the composite language, it is proved that: |
29 fuction @{text "tag"} is carefully devised, which returns tags made of |
|
30 equivalent classes of the partitions induced by subexpressoins, and |
|
31 therefore has a finite range. Let @{text "Lang"} be the composite language, |
|
32 it is proved that: |
30 \begin{quote} |
33 \begin{quote} |
31 If strings with the same tag are equivalent with respect to @{text "Lang"}, expressed as: |
34 If strings with the same tag are equivalent with respect to @{text "Lang"}, expressed as: |
32 \[ |
35 \[ |
33 @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"} |
36 @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"} |
34 \] |
37 \] |
55 *} |
58 *} |
56 |
59 |
57 definition |
60 definition |
58 f_eq_rel ("=_=") |
61 f_eq_rel ("=_=") |
59 where |
62 where |
60 "(=f=) = {(x, y) | x y. f x = f y}" |
63 "=f= \<equiv> {(x, y) | x y. f x = f y}" |
61 |
64 |
62 lemma equiv_f_eq_rel:"equiv UNIV (=f=)" |
65 lemma equiv_f_eq_rel:"equiv UNIV (=f=)" |
63 by (auto simp:equiv_def f_eq_rel_def refl_on_def sym_def trans_def) |
66 by (auto simp:equiv_def f_eq_rel_def refl_on_def sym_def trans_def) |
64 |
67 |
65 lemma finite_range_image: "finite (range f) \<Longrightarrow> finite (f ` A)" |
68 lemma finite_range_image: |
66 by (rule_tac B = "{y. \<exists>x. y = f x}" in finite_subset, auto simp:image_def) |
69 assumes "finite (range f)" |
|
70 shows "finite (f ` A)" |
|
71 using assms unfolding image_def |
|
72 by (rule_tac finite_subset) (auto) |
67 |
73 |
68 lemma finite_eq_f_rel: |
74 lemma finite_eq_f_rel: |
69 assumes rng_fnt: "finite (range tag)" |
75 assumes rng_fnt: "finite (range tag)" |
70 shows "finite (UNIV // (=tag=))" |
76 shows "finite (UNIV // =tag=)" |
71 proof - |
77 proof - |
72 let "?f" = "op ` tag" and ?A = "(UNIV // (=tag=))" |
78 let "?f" = "op ` tag" and ?A = "(UNIV // =tag=)" |
73 show ?thesis |
79 show ?thesis |
74 proof (rule_tac f = "?f" and A = ?A in finite_imageD) |
80 proof (rule_tac f = "?f" and A = ?A in finite_imageD) |
75 -- {* |
81 -- {* |
76 The finiteness of @{text "f"}-image is a simple consequence of assumption @{text "rng_fnt"}: |
82 The finiteness of @{text "f"}-image is a simple consequence of assumption @{text "rng_fnt"}: |
77 *} |
83 *} |
107 } thus ?thesis unfolding inj_on_def by auto |
113 } thus ?thesis unfolding inj_on_def by auto |
108 qed |
114 qed |
109 qed |
115 qed |
110 qed |
116 qed |
111 |
117 |
112 lemma finite_image_finite: "\<lbrakk>\<forall> x \<in> A. f x \<in> B; finite B\<rbrakk> \<Longrightarrow> finite (f ` A)" |
118 lemma finite_image_finite: |
|
119 "\<lbrakk>\<forall> x \<in> A. f x \<in> B; finite B\<rbrakk> \<Longrightarrow> finite (f ` A)" |
113 by (rule finite_subset [of _ B], auto) |
120 by (rule finite_subset [of _ B], auto) |
114 |
121 |
115 lemma refined_partition_finite: |
122 lemma refined_partition_finite: |
116 fixes R1 R2 A |
123 fixes R1 R2 A |
117 assumes fnt: "finite (A // R1)" |
124 assumes fnt: "finite (A // R1)" |
355 subsubsection {* The inductive case for @{const ALT} *} |
362 subsubsection {* The inductive case for @{const ALT} *} |
356 |
363 |
357 definition |
364 definition |
358 tag_str_ALT :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang)" |
365 tag_str_ALT :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang)" |
359 where |
366 where |
360 "tag_str_ALT L1 L2 = (\<lambda>x. (\<approx>L1 `` {x}, \<approx>L2 `` {x}))" |
367 "tag_str_ALT L1 L2 \<equiv> (\<lambda>x. (\<approx>L1 `` {x}, \<approx>L2 `` {x}))" |
361 |
368 |
362 lemma quot_union_finiteI [intro]: |
369 lemma quot_union_finiteI [intro]: |
363 fixes L1 L2::"lang" |
370 fixes L1 L2::"lang" |
364 assumes finite1: "finite (UNIV // \<approx>L1)" |
371 assumes finite1: "finite (UNIV // \<approx>L1)" |
365 and finite2: "finite (UNIV // \<approx>L2)" |
372 and finite2: "finite (UNIV // \<approx>L2)" |
399 *} |
406 *} |
400 |
407 |
401 definition |
408 definition |
402 tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)" |
409 tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)" |
403 where |
410 where |
404 "tag_str_SEQ L1 L2 = |
411 "tag_str_SEQ L1 L2 \<equiv> |
405 (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa. xa \<le> x \<and> xa \<in> L1}))" |
412 (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa. xa \<le> x \<and> xa \<in> L1}))" |
406 |
413 |
407 text {* The following is a techical lemma which helps to split the @{text "x @ z \<in> L\<^isub>1 ;; L\<^isub>2"} mentioned above.*} |
414 text {* The following is a techical lemma which helps to split the @{text "x @ z \<in> L\<^isub>1 ;; L\<^isub>2"} mentioned above.*} |
408 |
415 |
409 lemma append_seq_elim: |
416 lemma append_seq_elim: |
579 *} |
586 *} |
580 |
587 |
581 definition |
588 definition |
582 tag_str_STAR :: "lang \<Rightarrow> string \<Rightarrow> lang set" |
589 tag_str_STAR :: "lang \<Rightarrow> string \<Rightarrow> lang set" |
583 where |
590 where |
584 "tag_str_STAR L1 = (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<star>})" |
591 "tag_str_STAR L1 \<equiv> (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<star>})" |
585 |
592 |
586 text {* A technical lemma. *} |
593 text {* A technical lemma. *} |
587 lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> |
594 lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> |
588 (\<exists> max \<in> A. \<forall> a \<in> A. f a <= (f max :: nat))" |
595 (\<exists> max \<in> A. \<forall> a \<in> A. f a <= (f max :: nat))" |
589 proof (induct rule:finite.induct) |
596 proof (induct rule:finite.induct) |