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 induction over regular expressions. |
22 While base cases (cases for @{const "NULL"}, @{const "EMPTY"}, @{const "CHAR"}) are quite straight forward, |
22 where base cases (cases for @{const "NULL"}, @{const "EMPTY"}, @{const "CHAR"}) are quite straightforward to |
23 the inductive cases are rather involved. What we have when starting to prove these inductive caes is that |
23 proof. Real difficulty lies in inductive cases. By inductive hypothesis, languages defined by |
24 the partitions induced by the componet language are finite. The basic idea to show the finiteness of the |
24 sub-expressions induce finite partitiions. Under such hypothsis, we need to prove that the language |
25 partition induced by the composite language is to attach a tag @{text "tag(x)"} to every string |
25 defined by the composite regular expression gives rise to finite partion. |
26 @{text "x"}. The tags are made of equivalent classes from the component partitions. Let @{text "tag"} |
26 The basic idea is to attach a tag @{text "tag(x)"} to every string |
27 be the tagging function and @{text "Lang"} be the composite language, it can be proved that |
27 @{text "x"}. The tagging fuction @{text "tag"} is carefully devised, which returns tags |
28 if strings with the same tag are equivalent with respect to @{text "Lang"}, expressed as: |
28 made of equivalent classes of the partitions induced by subexpressoins, and therefore has a finite |
|
29 range. Let @{text "Lang"} be the composite language, it is proved that: |
|
30 \begin{quote} |
|
31 If strings with the same tag are equivalent with respect to @{text "Lang"}, expressed as: |
29 \[ |
32 \[ |
30 @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"} |
33 @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"} |
31 \] |
34 \] |
32 then the partition induced by @{text "Lang"} must be finite. There are two arguments for this. |
35 then the partition induced by @{text "Lang"} must be finite. |
33 The first goes as the following: |
36 \end{quote} |
|
37 There are two arguments for this. The first goes as the following: |
34 \begin{enumerate} |
38 \begin{enumerate} |
35 \item First, the tagging function @{text "tag"} induces an equivalent relation @{text "(=tag=)"} |
39 \item First, the tagging function @{text "tag"} induces an equivalent relation @{text "(=tag=)"} |
36 (defiintion of @{text "f_eq_rel"} and lemma @{text "equiv_f_eq_rel"}). |
40 (defiintion of @{text "f_eq_rel"} and lemma @{text "equiv_f_eq_rel"}). |
37 \item It is shown that: if the range of @{text "tag"} (denoted @{text "range(tag)"}) is finite, |
41 \item It is shown that: if the range of @{text "tag"} (denoted @{text "range(tag)"}) is finite, |
38 the partition given rise by @{text "(=tag=)"} is finite (lemma @{text "finite_eq_f_rel"}). |
42 the partition given rise by @{text "(=tag=)"} is finite (lemma @{text "finite_eq_f_rel"}). |