11 string @{text "x"} and @{text "y"} are equivalent with respect to |
11 string @{text "x"} and @{text "y"} are equivalent with respect to |
12 language @{text "Lang"}. |
12 language @{text "Lang"}. |
13 *} |
13 *} |
14 |
14 |
15 definition |
15 definition |
16 str_eq :: "string \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> bool" ("_ \<approx>_ _") |
16 str_eq ("_ \<approx>_ _") |
17 where |
17 where |
18 "x \<approx>Lang y \<equiv> (x, y) \<in> (\<approx>Lang)" |
18 "x \<approx>Lang y \<equiv> (x, y) \<in> (\<approx>Lang)" |
19 |
19 |
20 text {* |
20 text {* |
21 The very basic scheme to show the finiteness of the partion generated by a language @{text "Lang"} |
21 The basic idea to show the finiteness of the partition induced by relation @{text "\<approx>Lang"} |
22 is by attaching a tag to every string. The set of tags are carfully choosen to be finite so that |
22 is to attach a tag @{text "tag(x)"} to every string @{text "x"}, the set of tags are carfully |
23 the range of tagging function is finite. If it can be proved that strings with the same tag |
23 choosen, so that the range of tagging function @{text "tag"} (denoted @{text "range(tag)"}) is finite. |
24 are equivlent with respect @{text "Lang"}, then the partition given rise by @{text "Lang"} must be finite. |
24 If strings with the same tag are equivlent with respect @{text "\<approx>Lang"}, |
25 The detailed argjument for this is formalized by the following lemma @{text "tag_finite_imageD"}. |
25 i.e. @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"} (this property is named `injectivity' in the following), |
26 The basic idea is using lemma @{thm [source] "finite_imageD"} |
26 then it can be proved that: the partition given rise by @{text "(\<approx>Lang)"} is finite. |
27 from standard library: |
27 |
28 \[ |
28 There are two arguments for this. The first goes as the following: |
29 @{thm "finite_imageD" [no_vars]} |
29 \begin{enumerate} |
30 \] |
30 \item First, the tagging function @{text "tag"} induces an equivalent relation @{text "(=tag=)"} |
31 which says: if the image of injective function @{text "f"} over set @{text "A"} is |
31 (defiintion of @{text "f_eq_rel"} and lemma @{text "equiv_f_eq_rel"}). |
32 finite, then @{text "A"} must be finte. |
32 \item It is shown that: if the range of @{text "tag"} is finite, |
33 *} |
33 the partition given rise by @{text "(=tag=)"} is finite (lemma @{text "finite_eq_f_rel"}). |
34 |
34 \item It is proved that if equivalent relation @{text "R1"} is more refined than @{text "R2"} |
35 |
35 (expressed as @{text "R1 \<subseteq> R2"}), |
36 |
36 and the partition induced by @{text "R1"} is finite, then the partition induced by @{text "R2"} |
37 (* I am trying to reduce the following proof to even simpler principles. But not yet succeed. *) |
37 is finite as well (lemma @{text "refined_partition_finite"}). |
|
38 \item The injectivity assumption @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"} implies that |
|
39 @{text "(=tag=)"} is more refined than @{text "(\<approx>Lang)"}. |
|
40 \item Combining the points above, we have: the partition induced by language @{text "Lang"} |
|
41 is finite (lemma @{text "tag_finite_imageD"}). |
|
42 \end{enumerate} |
|
43 *} |
|
44 |
38 definition |
45 definition |
39 f_eq_rel ("\<cong>_") |
46 f_eq_rel ("=_=") |
40 where |
47 where |
41 "\<cong>(f::'a \<Rightarrow> 'b) = {(x, y) | x y. f x = f y}" |
48 "(=f=) = {(x, y) | x y. f x = f y}" |
42 |
49 |
43 thm finite.induct |
50 lemma equiv_f_eq_rel:"equiv UNIV (=f=)" |
|
51 by (auto simp:equiv_def f_eq_rel_def refl_on_def sym_def trans_def) |
44 |
52 |
45 lemma finite_range_image: "finite (range f) \<Longrightarrow> finite (f ` A)" |
53 lemma finite_range_image: "finite (range f) \<Longrightarrow> finite (f ` A)" |
46 by (rule_tac B = "{y. \<exists>x. y = f x}" in finite_subset, auto simp:image_def) |
54 by (rule_tac B = "{y. \<exists>x. y = f x}" in finite_subset, auto simp:image_def) |
47 |
55 |
48 lemma "equiv UNIV (\<cong>f)" |
56 lemma finite_eq_f_rel: |
49 by (auto simp:equiv_def f_eq_rel_def refl_on_def sym_def trans_def) |
|
50 |
|
51 lemma |
|
52 assumes rng_fnt: "finite (range tag)" |
57 assumes rng_fnt: "finite (range tag)" |
53 shows "finite (UNIV // (\<cong>tag))" |
58 shows "finite (UNIV // (=tag=))" |
54 proof - |
59 proof - |
55 let "?f" = "op ` tag" and ?A = "(UNIV // (\<cong>tag))" |
60 let "?f" = "op ` tag" and ?A = "(UNIV // (=tag=))" |
56 show ?thesis |
61 show ?thesis |
57 proof (rule_tac f = "?f" and A = ?A in finite_imageD) |
62 proof (rule_tac f = "?f" and A = ?A in finite_imageD) |
58 -- {* |
63 -- {* |
59 The finiteness of @{text "f"}-image is a simple consequence of assumption @{text "rng_fnt"}: |
64 The finiteness of @{text "f"}-image is a simple consequence of assumption @{text "rng_fnt"}: |
60 *} |
65 *} |
66 by (auto simp only:image_def intro:finite_subset) |
71 by (auto simp only:image_def intro:finite_subset) |
67 from finite_range_image [OF this] show ?thesis . |
72 from finite_range_image [OF this] show ?thesis . |
68 qed |
73 qed |
69 next |
74 next |
70 -- {* |
75 -- {* |
71 The injectivity of @{text "f"}-image is a consequence of the definition of @{text "\<cong>tag"} |
76 The injectivity of @{text "f"}-image is a consequence of the definition of @{text "(=tag=)"}: |
72 *} |
77 *} |
73 show "inj_on ?f ?A" |
78 show "inj_on ?f ?A" |
74 proof- |
79 proof- |
75 { fix X Y |
80 { fix X Y |
76 assume X_in: "X \<in> ?A" |
81 assume X_in: "X \<in> ?A" |
77 and Y_in: "Y \<in> ?A" |
82 and Y_in: "Y \<in> ?A" |
78 and tag_eq: "?f X = ?f Y" |
83 and tag_eq: "?f X = ?f Y" |
79 have "X = Y" |
84 have "X = Y" |
80 proof - |
85 proof - |
81 from X_in Y_in tag_eq |
86 from X_in Y_in tag_eq |
82 obtain x y where x_in: "x \<in> X" and y_in: "y \<in> Y" and eq_tg: "tag x = tag y" |
87 obtain x y |
83 unfolding quotient_def Image_def str_eq_rel_def str_eq_def image_def f_eq_rel_def |
88 where x_in: "x \<in> X" and y_in: "y \<in> Y" and eq_tg: "tag x = tag y" |
|
89 unfolding quotient_def Image_def str_eq_rel_def |
|
90 str_eq_def image_def f_eq_rel_def |
84 apply simp by blast |
91 apply simp by blast |
85 with X_in Y_in show ?thesis |
92 with X_in Y_in show ?thesis |
86 by (auto simp:quotient_def str_eq_rel_def str_eq_def f_eq_rel_def) |
93 by (auto simp:quotient_def str_eq_rel_def str_eq_def f_eq_rel_def) |
87 qed |
94 qed |
88 } thus ?thesis unfolding inj_on_def by auto |
95 } thus ?thesis unfolding inj_on_def by auto |
89 qed |
96 qed |
90 qed |
97 qed |
91 qed |
98 qed |
92 |
99 |
93 |
100 lemma finite_image_finite: "\<lbrakk>\<forall> x \<in> A. f x \<in> B; finite B\<rbrakk> \<Longrightarrow> finite (f ` A)" |
94 (* |
101 by (rule finite_subset [of _ B], auto) |
95 lemma finite_range_image: "finite (range f) \<Longrightarrow> finite (f ` A)" |
102 |
96 by (rule_tac B = "{y. \<exists>x. y = f x}" in finite_subset, auto simp:image_def) |
103 lemma refined_partition_finite: |
97 *) |
104 fixes R1 R2 A |
|
105 assumes fnt: "finite (A // R1)" |
|
106 and refined: "R1 \<subseteq> R2" |
|
107 and eq1: "equiv A R1" and eq2: "equiv A R2" |
|
108 shows "finite (A // R2)" |
|
109 proof - |
|
110 let ?f = "\<lambda> X. {R1 `` {x} | x. x \<in> X}" |
|
111 and ?A = "(A // R2)" and ?B = "(A // R1)" |
|
112 show ?thesis |
|
113 proof(rule_tac f = ?f and A = ?A in finite_imageD) |
|
114 show "finite (?f ` ?A)" |
|
115 proof(rule finite_subset [of _ "Pow ?B"]) |
|
116 from fnt show "finite (Pow (A // R1))" by simp |
|
117 next |
|
118 from eq2 |
|
119 show " ?f ` A // R2 \<subseteq> Pow ?B" |
|
120 apply (unfold image_def Pow_def quotient_def, auto) |
|
121 by (rule_tac x = xb in bexI, simp, |
|
122 unfold equiv_def sym_def refl_on_def, blast) |
|
123 qed |
|
124 next |
|
125 show "inj_on ?f ?A" |
|
126 proof - |
|
127 { fix X Y |
|
128 assume X_in: "X \<in> ?A" and Y_in: "Y \<in> ?A" |
|
129 and eq_f: "?f X = ?f Y" (is "?L = ?R") |
|
130 have "X = Y" using X_in |
|
131 proof(rule quotientE) |
|
132 fix x |
|
133 assume "X = R2 `` {x}" and "x \<in> A" with eq2 |
|
134 have x_in: "x \<in> X" |
|
135 by (unfold equiv_def quotient_def refl_on_def, auto) |
|
136 with eq_f have "R1 `` {x} \<in> ?R" by auto |
|
137 then obtain y where |
|
138 y_in: "y \<in> Y" and eq_r: "R1 `` {x} = R1 ``{y}" by auto |
|
139 have "(x, y) \<in> R1" |
|
140 proof - |
|
141 from x_in X_in y_in Y_in eq2 |
|
142 have "x \<in> A" and "y \<in> A" |
|
143 by (unfold equiv_def quotient_def refl_on_def, auto) |
|
144 from eq_equiv_class_iff [OF eq1 this] and eq_r |
|
145 show ?thesis by simp |
|
146 qed |
|
147 with refined have xy_r2: "(x, y) \<in> R2" by auto |
|
148 from quotient_eqI [OF eq2 X_in Y_in x_in y_in this] |
|
149 show ?thesis . |
|
150 qed |
|
151 } thus ?thesis by (auto simp:inj_on_def) |
|
152 qed |
|
153 qed |
|
154 qed |
|
155 |
|
156 lemma equiv_lang_eq: "equiv UNIV (\<approx>Lang)" |
|
157 apply (unfold equiv_def str_eq_rel_def sym_def refl_on_def trans_def) |
|
158 by blast |
98 |
159 |
99 lemma tag_finite_imageD: |
160 lemma tag_finite_imageD: |
100 fixes L :: "lang" |
161 fixes tag |
101 assumes rng_fnt: "finite (range tag)" |
162 assumes rng_fnt: "finite (range tag)" |
102 -- {* Suppose the range of tagging fucntion @{text "tag"} is finite. *} |
163 -- {* Suppose the rang of tagging fucntion @{text "tag"} is finite. *} |
103 and same_tag_eqvt: "\<And> m n. tag m = tag n \<Longrightarrow> m \<approx>L n" |
164 and same_tag_eqvt: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<approx>Lang n" |
104 -- {* And strings with same tag are equivalent *} |
165 -- {* And strings with same tag are equivalent *} |
105 shows "finite (UNIV // \<approx>L)" |
166 shows "finite (UNIV // (\<approx>Lang))" |
106 -- {* Then the partition generated by @{text "\<approx>L"} is finite. *} |
167 proof - |
|
168 let ?R1 = "(=tag=)" |
|
169 show ?thesis |
|
170 proof(rule_tac refined_partition_finite [of _ ?R1]) |
|
171 from finite_eq_f_rel [OF rng_fnt] |
|
172 show "finite (UNIV // =tag=)" . |
|
173 next |
|
174 from same_tag_eqvt |
|
175 show "(=tag=) \<subseteq> (\<approx>Lang)" |
|
176 by (auto simp:f_eq_rel_def str_eq_def) |
|
177 next |
|
178 from equiv_f_eq_rel |
|
179 show "equiv UNIV (=tag=)" by blast |
|
180 next |
|
181 from equiv_lang_eq |
|
182 show "equiv UNIV (\<approx>Lang)" by blast |
|
183 qed |
|
184 qed |
|
185 |
|
186 text {* |
|
187 A more concise, but less intelligible argument for @{text "tag_finite_imageD"} |
|
188 is given as the following. The basic idea is still using standard library |
|
189 lemma @{thm [source] "finite_imageD"}: |
|
190 \[ |
|
191 @{thm "finite_imageD" [no_vars]} |
|
192 \] |
|
193 which says: if the image of injective function @{text "f"} over set @{text "A"} is |
|
194 finite, then @{text "A"} must be finte, as we did in the lemmas above. |
|
195 *} |
|
196 |
|
197 lemma |
|
198 fixes tag |
|
199 assumes rng_fnt: "finite (range tag)" |
|
200 -- {* Suppose the rang of tagging fucntion @{text "tag"} is finite. *} |
|
201 and same_tag_eqvt: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<approx>Lang n" |
|
202 -- {* And strings with same tag are equivalent *} |
|
203 shows "finite (UNIV // (\<approx>Lang))" |
|
204 -- {* Then the partition generated by @{text "(\<approx>Lang)"} is finite. *} |
107 proof - |
205 proof - |
108 -- {* The particular @{text "f"} and @{text "A"} used in @{thm [source] "finite_imageD"} are:*} |
206 -- {* The particular @{text "f"} and @{text "A"} used in @{thm [source] "finite_imageD"} are:*} |
109 let "?f" = "op ` tag" and ?A = "(UNIV // \<approx>L)" |
207 let "?f" = "op ` tag" and ?A = "(UNIV // \<approx>Lang)" |
110 show ?thesis |
208 show ?thesis |
111 proof (rule_tac f = "?f" and A = ?A in finite_imageD) |
209 proof (rule_tac f = "?f" and A = ?A in finite_imageD) |
112 -- {* |
210 -- {* |
113 The finiteness of @{text "f"}-image is a simple consequence of assumption @{text "rng_fnt"}: |
211 The finiteness of @{text "f"}-image is a simple consequence of assumption @{text "rng_fnt"}: |
114 *} |
212 *} |
146 qed |
244 qed |
147 |
245 |
148 subsection {* Lemmas for basic cases *} |
246 subsection {* Lemmas for basic cases *} |
149 |
247 |
150 text {* |
248 text {* |
151 The the final result of this direction is in @{text "rexp_imp_finite"}, |
249 The the final result of this direction is in @{text "easier_direction"}, which |
152 which is an induction on the structure of regular expressions. There is one |
250 is an induction on the structure of regular expressions. There is one case |
153 case for each regular expression operator. For basic operators such as |
251 for each regular expression operator. For basic operators such as @{text "NULL, EMPTY, CHAR c"}, |
154 @{const NULL}, @{const EMPTY}, @{const CHAR}, the finiteness of their |
252 the finiteness of their language partition can be established directly with no need |
155 language partition can be established directly with no need of tagging. |
253 of taggiing. This section contains several technical lemma for these base cases. |
156 This section contains several technical lemma for these base cases. |
254 |
157 |
255 The inductive cases involve operators @{text "ALT, SEQ"} and @{text "STAR"}. |
158 The inductive cases involve operators @{const ALT}, @{const SEQ} and @{const |
256 Tagging functions need to be defined individually for each of them. There will be one |
159 STAR}. Tagging functions need to be defined individually for each of |
257 dedicated section for each of these cases, and each section goes virtually the same way: |
160 them. There will be one dedicated section for each of these cases, and each |
258 gives definition of the tagging function and prove that strings |
161 section goes virtually the same way: gives definition of the tagging |
259 with the same tag are equivalent. |
162 function and prove that strings with the same tag are equivalent. |
260 *} |
163 *} |
|
164 |
|
165 subsection {* The case for @{const "NULL"} *} |
|
166 |
|
167 lemma quot_null_eq: |
|
168 shows "(UNIV // \<approx>{}) = ({UNIV}::lang set)" |
|
169 unfolding quotient_def Image_def str_eq_rel_def by auto |
|
170 |
|
171 lemma quot_null_finiteI [intro]: |
|
172 shows "finite ((UNIV // \<approx>{})::lang set)" |
|
173 unfolding quot_null_eq by simp |
|
174 |
|
175 |
|
176 subsection {* The case for @{const "EMPTY"} *} |
|
177 |
|
178 |
261 |
179 lemma quot_empty_subset: |
262 lemma quot_empty_subset: |
180 "UNIV // (\<approx>{[]}) \<subseteq> {{[]}, UNIV - {[]}}" |
263 "UNIV // (\<approx>{[]}) \<subseteq> {{[]}, UNIV - {[]}}" |
181 proof |
264 proof |
182 fix x |
265 fix x |
183 assume "x \<in> UNIV // \<approx>{[]}" |
266 assume "x \<in> UNIV // \<approx>{[]}" |
184 then obtain y where h: "x = {z. (y, z) \<in> \<approx>{[]}}" |
267 then obtain y where h: "x = {z. (y, z) \<in> \<approx>{[]}}" |
185 unfolding quotient_def Image_def by blast |
268 unfolding quotient_def Image_def by blast |
186 show "x \<in> {{[]}, UNIV - {[]}}" |
269 show "x \<in> {{[]}, UNIV - {[]}}" |
187 proof (cases "y = []") |
270 proof (cases "y = []") |
188 case True with h |
271 case True with h |
189 have "x = {[]}" by (auto simp: str_eq_rel_def) |
272 have "x = {[]}" by (auto simp:str_eq_rel_def) |
190 thus ?thesis by simp |
273 thus ?thesis by simp |
191 next |
274 next |
192 case False with h |
275 case False with h |
193 have "x = UNIV - {[]}" by (auto simp: str_eq_rel_def) |
276 have "x = UNIV - {[]}" by (auto simp:str_eq_rel_def) |
194 thus ?thesis by simp |
277 thus ?thesis by simp |
195 qed |
278 qed |
196 qed |
279 qed |
197 |
|
198 lemma quot_empty_finiteI [intro]: |
|
199 shows "finite (UNIV // (\<approx>{[]}))" |
|
200 by (rule finite_subset[OF quot_empty_subset]) (simp) |
|
201 |
|
202 |
|
203 subsection {* The case for @{const "CHAR"} *} |
|
204 |
280 |
205 lemma quot_char_subset: |
281 lemma quot_char_subset: |
206 "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}" |
282 "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}" |
207 proof |
283 proof |
208 fix x |
284 fix x |
225 by (auto simp add:str_eq_rel_def) |
301 by (auto simp add:str_eq_rel_def) |
226 } ultimately show ?thesis by blast |
302 } ultimately show ?thesis by blast |
227 qed |
303 qed |
228 qed |
304 qed |
229 |
305 |
230 lemma quot_char_finiteI [intro]: |
306 subsection {* The case for @{text "SEQ"}*} |
231 shows "finite (UNIV // (\<approx>{[c]}))" |
|
232 by (rule finite_subset[OF quot_char_subset]) (simp) |
|
233 |
|
234 |
|
235 subsection {* The case for @{const SEQ}*} |
|
236 |
307 |
237 definition |
308 definition |
238 tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)" |
309 "tag_str_SEQ L\<^isub>1 L\<^isub>2 x \<equiv> |
239 where |
310 ((\<approx>L\<^isub>1) `` {x}, {(\<approx>L\<^isub>2) `` {x - xa}| xa. xa \<le> x \<and> xa \<in> L\<^isub>1})" |
240 "tag_str_SEQ L1 L2 = (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa. xa \<le> x \<and> xa \<in> L1}))" |
311 |
241 |
312 lemma tag_str_seq_range_finite: |
|
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) |
242 |
317 |
243 lemma append_seq_elim: |
318 lemma append_seq_elim: |
244 assumes "x @ y \<in> L\<^isub>1 ;; L\<^isub>2" |
319 assumes "x @ y \<in> L\<^isub>1 ;; L\<^isub>2" |
245 shows "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> L\<^isub>2) \<or> |
320 shows "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> L\<^isub>2) \<or> |
246 (\<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> L\<^isub>2)" |
321 (\<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> L\<^isub>2)" |
304 } |
379 } |
305 ultimately show ?thesis by blast |
380 ultimately show ?thesis by blast |
306 qed |
381 qed |
307 } 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" |
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" |
308 by (auto simp add: str_eq_def str_eq_rel_def) |
383 by (auto simp add: str_eq_def str_eq_rel_def) |
309 qed |
384 qed |
310 |
385 |
311 lemma quot_seq_finiteI [intro]: |
386 lemma quot_seq_finiteI: |
312 fixes L1 L2::"lang" |
387 "\<lbrakk>finite (UNIV // \<approx>L\<^isub>1); finite (UNIV // \<approx>L\<^isub>2)\<rbrakk> |
313 assumes fin1: "finite (UNIV // \<approx>L1)" |
388 \<Longrightarrow> finite (UNIV // \<approx>(L\<^isub>1 ;; L\<^isub>2))" |
314 and fin2: "finite (UNIV // \<approx>L2)" |
389 apply (rule_tac tag = "tag_str_SEQ L\<^isub>1 L\<^isub>2" in tag_finite_imageD) |
315 shows "finite (UNIV // \<approx>(L1 ;; L2))" |
390 by (auto intro:tag_str_SEQ_injI elim:tag_str_seq_range_finite) |
316 proof (rule_tac tag = "tag_str_SEQ L1 L2" in tag_finite_imageD) |
391 |
317 show "\<And>x y. tag_str_SEQ L1 L2 x = tag_str_SEQ L1 L2 y \<Longrightarrow> x \<approx>(L1 ;; L2) y" |
392 subsection {* The case for @{text "ALT"} *} |
318 by (rule tag_str_SEQ_injI) |
393 |
|
394 definition |
|
395 "tag_str_ALT L\<^isub>1 L\<^isub>2 (x::string) \<equiv> ((\<approx>L\<^isub>1) `` {x}, (\<approx>L\<^isub>2) `` {x})" |
|
396 |
|
397 lemma quot_union_finiteI: |
|
398 assumes finite1: "finite (UNIV // \<approx>(L\<^isub>1::string set))" |
|
399 and finite2: "finite (UNIV // \<approx>L\<^isub>2)" |
|
400 shows "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))" |
|
401 proof (rule_tac tag = "tag_str_ALT L\<^isub>1 L\<^isub>2" in tag_finite_imageD) |
|
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" |
|
403 unfolding tag_str_ALT_def str_eq_def Image_def str_eq_rel_def by auto |
319 next |
404 next |
320 have *: "finite ((UNIV // \<approx>L1) \<times> (Pow (UNIV // \<approx>L2)))" |
405 show "finite (range (tag_str_ALT L\<^isub>1 L\<^isub>2))" using finite1 finite2 |
321 using fin1 fin2 by auto |
406 apply (rule_tac B = "(UNIV // \<approx>L\<^isub>1) \<times> (UNIV // \<approx>L\<^isub>2)" in finite_subset) |
322 show "finite (range (tag_str_SEQ L1 L2))" |
407 by (auto simp:tag_str_ALT_def Image_def quotient_def) |
323 unfolding tag_str_SEQ_def |
408 qed |
324 apply(rule finite_subset[OF _ *]) |
409 |
325 unfolding quotient_def |
410 subsection {* |
326 by auto |
411 The case for @{text "STAR"} |
327 qed |
412 *} |
328 |
|
329 |
|
330 subsection {* The case for @{const ALT} *} |
|
331 |
|
332 definition |
|
333 tag_str_ALT :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang)" |
|
334 where |
|
335 "tag_str_ALT L1 L2 = (\<lambda>x. (\<approx>L1 `` {x}, \<approx>L2 `` {x}))" |
|
336 |
|
337 |
|
338 lemma quot_union_finiteI [intro]: |
|
339 fixes L1 L2::"lang" |
|
340 assumes finite1: "finite (UNIV // \<approx>L1)" |
|
341 and finite2: "finite (UNIV // \<approx>L2)" |
|
342 shows "finite (UNIV // \<approx>(L1 \<union> L2))" |
|
343 proof (rule_tac tag = "tag_str_ALT L1 L2" in tag_finite_imageD) |
|
344 show "\<And>x y. tag_str_ALT L1 L2 x = tag_str_ALT L1 L2 y \<Longrightarrow> x \<approx>(L1 \<union> L2) y" |
|
345 unfolding tag_str_ALT_def |
|
346 unfolding str_eq_def |
|
347 unfolding Image_def |
|
348 unfolding str_eq_rel_def |
|
349 by auto |
|
350 next |
|
351 have *: "finite ((UNIV // \<approx>L1) \<times> (UNIV // \<approx>L2))" |
|
352 using finite1 finite2 by auto |
|
353 show "finite (range (tag_str_ALT L1 L2))" |
|
354 unfolding tag_str_ALT_def |
|
355 apply(rule finite_subset[OF _ *]) |
|
356 unfolding quotient_def |
|
357 by auto |
|
358 qed |
|
359 |
|
360 subsection {* The case for @{const "STAR"} *} |
|
361 |
413 |
362 text {* |
414 text {* |
363 This turned out to be the trickiest case. |
415 This turned out to be the trickiest case. |
364 *} (* I will make some illustrations for it. *) |
416 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"}. |
|
418 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. |
|
420 *} |
|
421 |
|
422 (* I will make some illustrations for it. *) |
365 |
423 |
366 definition |
424 definition |
367 tag_str_STAR :: "lang \<Rightarrow> string \<Rightarrow> lang set" |
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>}" |
368 where |
426 |
369 "tag_str_STAR L1 = (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<star>})" |
427 text {* A technical lemma. *} |
370 |
428 lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> |
371 |
429 (\<exists> max \<in> A. \<forall> a \<in> A. f a <= (f max :: nat))" |
372 lemma finite_set_has_max: |
|
373 "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> (\<exists> max \<in> A. \<forall> a \<in> A. f a <= (f max :: nat))" |
|
374 proof (induct rule:finite.induct) |
430 proof (induct rule:finite.induct) |
375 case emptyI thus ?case by simp |
431 case emptyI thus ?case by simp |
376 next |
432 next |
377 case (insertI A a) |
433 case (insertI A a) |
378 show ?case |
434 show ?case |
392 thus ?thesis using h2 by (rule_tac x = a in bexI, auto) |
448 thus ?thesis using h2 by (rule_tac x = a in bexI, auto) |
393 qed |
449 qed |
394 qed |
450 qed |
395 qed |
451 qed |
396 |
452 |
|
453 |
|
454 text {* Technical lemma. *} |
397 lemma finite_strict_prefix_set: "finite {xa. xa < (x::string)}" |
455 lemma finite_strict_prefix_set: "finite {xa. xa < (x::string)}" |
398 apply (induct x rule:rev_induct, simp) |
456 apply (induct x rule:rev_induct, simp) |
399 apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}") |
457 apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}") |
400 by (auto simp:strict_prefix_def) |
458 by (auto simp:strict_prefix_def) |
401 |
459 |
|
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 |
|
470 text {* |
|
471 The following lemma @{text "tag_str_STAR_injI"} establishes the injectivity of |
|
472 the tagging function for case @{text "STAR"}. |
|
473 *} |
|
474 |
402 lemma tag_str_STAR_injI: |
475 lemma tag_str_STAR_injI: |
403 "tag_str_STAR L\<^isub>1 m = tag_str_STAR L\<^isub>1 n \<Longrightarrow> m \<approx>(L\<^isub>1\<star>) n" |
476 fixes v w |
|
477 assumes eq_tag: "tag_str_STAR L\<^isub>1 v = tag_str_STAR L\<^isub>1 w" |
|
478 shows "(v::string) \<approx>(L\<^isub>1\<star>) w" |
404 proof- |
479 proof- |
|
480 -- {* |
|
481 \begin{minipage}{0.9\textwidth} |
|
482 According to the definition of @{text "\<approx>Lang"}, |
|
483 proving @{text "v \<approx>(L\<^isub>1\<star>) w"} amounts to |
|
484 showing: for any string @{text "u"}, |
|
485 if @{text "v @ u \<in> (L\<^isub>1\<star>)"} then @{text "w @ u \<in> (L\<^isub>1\<star>)"} and vice versa. |
|
486 The reasoning pattern for both directions are the same, as derived |
|
487 in the following: |
|
488 \end{minipage} |
|
489 *} |
405 { fix x y z |
490 { fix x y z |
406 assume xz_in_star: "x @ z \<in> L\<^isub>1\<star>" |
491 assume xz_in_star: "x @ z \<in> L\<^isub>1\<star>" |
407 and tag_xy: "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y" |
492 and tag_xy: "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y" |
408 have "y @ z \<in> L\<^isub>1\<star>" |
493 have "y @ z \<in> L\<^isub>1\<star>" |
409 proof(cases "x = []") |
494 proof(cases "x = []") |
|
495 -- {* |
|
496 The degenerated case when @{text "x"} is a null string is easy to prove: |
|
497 *} |
410 case True |
498 case True |
411 with tag_xy have "y = []" |
499 with tag_xy have "y = []" |
412 by (auto simp:tag_str_STAR_def strict_prefix_def) |
500 by (auto simp:tag_str_STAR_def strict_prefix_def) |
413 thus ?thesis using xz_in_star True by simp |
501 thus ?thesis using xz_in_star True by simp |
414 next |
502 next |
|
503 -- {* |
|
504 \begin{minipage}{0.9\textwidth} |
|
505 The case when @{text "x"} is not null, and |
|
506 @{text "x @ z"} is in @{text "L\<^isub>1\<star>"}, |
|
507 \end{minipage} |
|
508 *} |
415 case False |
509 case False |
416 obtain x_max |
510 obtain x_max |
417 where h1: "x_max < x" |
511 where h1: "x_max < x" |
418 and h2: "x_max \<in> L\<^isub>1\<star>" |
512 and h2: "x_max \<in> L\<^isub>1\<star>" |
419 and h3: "(x - x_max) @ z \<in> L\<^isub>1\<star>" |
513 and h3: "(x - x_max) @ z \<in> L\<^isub>1\<star>" |
476 by (auto simp:str_eq_def str_eq_rel_def) |
570 by (auto simp:str_eq_def str_eq_rel_def) |
477 with z_decom b_in show ?thesis by (auto dest!:step[of "(y - ya) @ za"]) |
571 with z_decom b_in show ?thesis by (auto dest!:step[of "(y - ya) @ za"]) |
478 qed |
572 qed |
479 with h5 h6 show ?thesis |
573 with h5 h6 show ?thesis |
480 by (drule_tac star_intro1, auto simp:strict_prefix_def elim:prefixE) |
574 by (drule_tac star_intro1, auto simp:strict_prefix_def elim:prefixE) |
481 qed |
575 qed |
482 } thus "tag_str_STAR L\<^isub>1 m = tag_str_STAR L\<^isub>1 n \<Longrightarrow> m \<approx>(L\<^isub>1\<star>) n" |
576 } |
483 by (auto simp add:str_eq_def str_eq_rel_def) |
577 -- {* By instantiating the reasoning pattern just derived for both directions:*} |
484 qed |
578 from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]] |
485 |
579 -- {* The thesis is proved as a trival consequence: *} |
486 lemma quot_star_finiteI [intro]: |
580 show ?thesis by (unfold str_eq_def str_eq_rel_def, blast) |
487 fixes L1::"lang" |
581 qed |
488 assumes finite1: "finite (UNIV // \<approx>L1)" |
582 |
489 shows "finite (UNIV // \<approx>(L1\<star>))" |
583 lemma quot_star_finiteI: |
490 proof (rule_tac tag = "tag_str_STAR L1" in tag_finite_imageD) |
584 "finite (UNIV // \<approx>L\<^isub>1) \<Longrightarrow> finite (UNIV // \<approx>(L\<^isub>1\<star>))" |
491 show "\<And>x y. tag_str_STAR L1 x = tag_str_STAR L1 y \<Longrightarrow> x \<approx>(L1\<star>) y" |
585 apply (rule_tac tag = "tag_str_STAR L\<^isub>1" in tag_finite_imageD) |
492 by (rule tag_str_STAR_injI) |
586 by (auto intro:tag_str_STAR_injI elim:tag_str_star_range_finite) |
|
587 |
|
588 subsection {* |
|
589 The main lemma |
|
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) |
493 next |
599 next |
494 have *: "finite (Pow (UNIV // \<approx>L1))" |
600 case EMPTY |
495 using finite1 by auto |
601 have "UNIV // (\<approx>{[]}) \<subseteq> {{[]}, UNIV - {[]}}" |
496 show "finite (range (tag_str_STAR L1))" |
602 by (rule quot_empty_subset) |
497 unfolding tag_str_STAR_def |
603 with prems show ?case by (auto intro:finite_subset) |
498 apply(rule finite_subset[OF _ *]) |
604 next |
499 unfolding quotient_def |
605 case (CHAR c) |
500 by auto |
606 have "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}" |
501 qed |
607 by (rule quot_char_subset) |
502 |
608 with prems show ?case by (auto intro:finite_subset) |
503 |
609 next |
504 subsection {* The main lemma *} |
610 case (SEQ r\<^isub>1 r\<^isub>2) |
505 |
611 have "\<lbrakk>finite (UNIV // \<approx>(L r\<^isub>1)); finite (UNIV // \<approx>(L r\<^isub>2))\<rbrakk> |
506 lemma rexp_imp_finite: |
612 \<Longrightarrow> finite (UNIV // \<approx>(L r\<^isub>1 ;; L r\<^isub>2))" |
507 fixes r::"rexp" |
613 by (erule quot_seq_finiteI, simp) |
508 shows "finite (UNIV // \<approx>(L r))" |
614 with prems show ?case by simp |
509 by (induct r) (auto) |
615 next |
510 |
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 |
511 |
628 |
512 end |
629 end |
513 |
630 |
|
631 (* |
|
632 lemma refined_quotient_union_eq: |
|
633 assumes refined: "R1 \<subseteq> R2" |
|
634 and eq1: "equiv A R1" and eq2: "equiv A R2" |
|
635 and y_in: "y \<in> A" |
|
636 shows "\<Union>{R1 `` {x} | x. x \<in> (R2 `` {y})} = R2 `` {y}" |
|
637 proof |
|
638 show "\<Union>{R1 `` {x} |x. x \<in> R2 `` {y}} \<subseteq> R2 `` {y}" (is "?L \<subseteq> ?R") |
|
639 proof - |
|
640 { fix z |
|
641 assume zl: "z \<in> ?L" and nzr: "z \<notin> ?R" |
|
642 have "False" |
|
643 proof - |
|
644 from zl and eq1 eq2 and y_in |
|
645 obtain x where xy2: "(x, y) \<in> R2" and zx1: "(z, x) \<in> R1" |
|
646 by (simp only:equiv_def sym_def, blast) |
|
647 have "(z, y) \<in> R2" |
|
648 proof - |
|
649 from zx1 and refined have "(z, x) \<in> R2" by blast |
|
650 moreover from xy2 have "(x, y) \<in> R2" . |
|
651 ultimately show ?thesis using eq2 |
|
652 by (simp only:equiv_def, unfold trans_def, blast) |
|
653 qed |
|
654 with nzr eq2 show ?thesis by (auto simp:equiv_def sym_def) |
|
655 qed |
|
656 } thus ?thesis by blast |
|
657 qed |
|
658 next |
|
659 show "R2 `` {y} \<subseteq> \<Union>{R1 `` {x} |x. x \<in> R2 `` {y}}" (is "?L \<subseteq> ?R") |
|
660 proof |
|
661 fix x |
|
662 assume x_in: "x \<in> ?L" |
|
663 with eq1 eq2 have "x \<in> R1 `` {x}" |
|
664 by (unfold equiv_def refl_on_def, auto) |
|
665 with x_in show "x \<in> ?R" by auto |
|
666 qed |
|
667 qed |
|
668 *) |
|
669 |
|
670 (* |
|
671 lemma refined_partition_finite: |
|
672 fixes R1 R2 A |
|
673 assumes fnt: "finite (A // R1)" |
|
674 and refined: "R1 \<subseteq> R2" |
|
675 and eq1: "equiv A R1" and eq2: "equiv A R2" |
|
676 shows "finite (A // R2)" |
|
677 proof - |
|
678 let ?f = "\<lambda> X. {R1 `` {x} | x. x \<in> X}" |
|
679 and ?A = "(A // R2)" and ?B = "(A // R1)" |
|
680 show ?thesis |
|
681 proof(rule_tac f = ?f and A = ?A in finite_imageD) |
|
682 show "finite (?f ` ?A)" |
|
683 proof(rule finite_subset [of _ "Pow ?B"]) |
|
684 from fnt show "finite (Pow (A // R1))" by simp |
|
685 next |
|
686 from eq2 |
|
687 show " ?f ` A // R2 \<subseteq> Pow ?B" |
|
688 apply (unfold image_def Pow_def quotient_def, auto) |
|
689 by (rule_tac x = xb in bexI, simp, |
|
690 unfold equiv_def sym_def refl_on_def, blast) |
|
691 qed |
|
692 next |
|
693 show "inj_on ?f ?A" |
|
694 proof - |
|
695 { fix X Y |
|
696 assume X_in: "X \<in> ?A" and Y_in: "Y \<in> ?A" |
|
697 and eq_f: "?f X = ?f Y" (is "?L = ?R") |
|
698 hence "X = Y" |
|
699 proof - |
|
700 from X_in eq2 |
|
701 obtain x |
|
702 where x_in: "x \<in> A" |
|
703 and eq_x: "X = R2 `` {x}" (is "X = ?X") |
|
704 by (unfold quotient_def equiv_def refl_on_def, auto) |
|
705 from Y_in eq2 obtain y |
|
706 where y_in: "y \<in> A" |
|
707 and eq_y: "Y = R2 `` {y}" (is "Y = ?Y") |
|
708 by (unfold quotient_def equiv_def refl_on_def, auto) |
|
709 have "?X = ?Y" |
|
710 proof - |
|
711 from eq_f have "\<Union> ?L = \<Union> ?R" by auto |
|
712 moreover have "\<Union> ?L = ?X" |
|
713 proof - |
|
714 from eq_x have "\<Union> ?L = \<Union>{R1 `` {x} |x. x \<in> ?X}" by simp |
|
715 also from refined_quotient_union_eq [OF refined eq1 eq2 x_in] |
|
716 have "\<dots> = ?X" . |
|
717 finally show ?thesis . |
|
718 qed |
|
719 moreover have "\<Union> ?R = ?Y" |
|
720 proof - |
|
721 from eq_y have "\<Union> ?R = \<Union>{R1 `` {y} |y. y \<in> ?Y}" by simp |
|
722 also from refined_quotient_union_eq [OF refined eq1 eq2 y_in] |
|
723 have "\<dots> = ?Y" . |
|
724 finally show ?thesis . |
|
725 qed |
|
726 ultimately show ?thesis by simp |
|
727 qed |
|
728 with eq_x eq_y show ?thesis by auto |
|
729 qed |
|
730 } thus ?thesis by (auto simp:inj_on_def) |
|
731 qed |
|
732 qed |
|
733 qed |
|
734 *) |