|
1 theory My |
|
2 imports Main |
|
3 begin |
|
4 |
|
5 |
|
6 definition |
|
7 lang_seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ; _" [100,100] 100) |
|
8 where |
|
9 "L1 ; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}" |
|
10 |
|
11 inductive_set |
|
12 Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102) |
|
13 for L :: "string set" |
|
14 where |
|
15 start[intro]: "[] \<in> L\<star>" |
|
16 | step[intro]: "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1@s2 \<in> L\<star>" |
|
17 |
|
18 |
|
19 datatype rexp = |
|
20 NULL |
|
21 | EMPTY |
|
22 | CHAR char |
|
23 | SEQ rexp rexp |
|
24 | ALT rexp rexp |
|
25 | STAR rexp |
|
26 |
|
27 fun |
|
28 L_rexp :: "rexp \<Rightarrow> string set" |
|
29 where |
|
30 "L_rexp (NULL) = {}" |
|
31 | "L_rexp (EMPTY) = {[]}" |
|
32 | "L_rexp (CHAR c) = {[c]}" |
|
33 | "L_rexp (SEQ r1 r2) = (L_rexp r1) ; (L_rexp r2)" |
|
34 | "L_rexp (ALT r1 r2) = (L_rexp r1) \<union> (L_rexp r2)" |
|
35 | "L_rexp (STAR r) = (L_rexp r)\<star>" |
|
36 |
|
37 definition |
|
38 folds :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b" |
|
39 where |
|
40 "folds f z S \<equiv> SOME x. fold_graph f z S x" |
|
41 |
|
42 lemma folds_simp_null [simp]: |
|
43 "finite rs \<Longrightarrow> x \<in> L_rexp (folds ALT NULL rs) = (\<exists>r \<in> rs. x \<in> L_rexp r)" |
|
44 apply (simp add: folds_def) |
|
45 apply (rule someI2_ex) |
|
46 apply (erule finite_imp_fold_graph) |
|
47 apply (erule fold_graph.induct) |
|
48 apply (auto) |
|
49 done |
|
50 |
|
51 lemma folds_simp_empty [simp]: |
|
52 "finite rs \<Longrightarrow> x \<in> L_rexp (folds ALT EMPTY rs) = ((\<exists>r \<in> rs. x \<in> L_rexp r) \<or> x = [])" |
|
53 apply (simp add: folds_def) |
|
54 apply (rule someI2_ex) |
|
55 apply (erule finite_imp_fold_graph) |
|
56 apply (erule fold_graph.induct) |
|
57 apply (auto) |
|
58 done |
|
59 |
|
60 lemma [simp]: |
|
61 "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y" |
|
62 by simp |
|
63 |
|
64 definition |
|
65 str_eq ("_ \<approx>_ _") |
|
66 where |
|
67 "x \<approx>Lang y \<equiv> (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)" |
|
68 |
|
69 definition |
|
70 str_eq_rel ("\<approx>_") |
|
71 where |
|
72 "\<approx>Lang \<equiv> {(x, y). x \<approx>Lang y}" |
|
73 |
|
74 definition |
|
75 final :: "string set \<Rightarrow> string set \<Rightarrow> bool" |
|
76 where |
|
77 "final X Lang \<equiv> (X \<in> UNIV // \<approx>Lang) \<and> (\<forall>s \<in> X. s \<in> Lang)" |
|
78 |
|
79 lemma lang_is_union_of_finals: |
|
80 "Lang = \<Union> {X. final X Lang}" |
|
81 proof - |
|
82 have "Lang \<subseteq> \<Union> {X. final X Lang}" |
|
83 unfolding final_def |
|
84 unfolding quotient_def Image_def |
|
85 unfolding str_eq_rel_def |
|
86 apply(simp) |
|
87 apply(auto) |
|
88 apply(rule_tac x="(\<approx>Lang) `` {x}" in exI) |
|
89 unfolding Image_def |
|
90 unfolding str_eq_rel_def |
|
91 apply(auto) |
|
92 unfolding str_eq_def |
|
93 apply(auto) |
|
94 apply(drule_tac x="[]" in spec) |
|
95 apply(simp) |
|
96 done |
|
97 moreover |
|
98 have "\<Union>{X. final X Lang} \<subseteq> Lang" |
|
99 unfolding final_def by auto |
|
100 ultimately |
|
101 show "Lang = \<Union> {X. final X Lang}" |
|
102 by blast |
|
103 qed |
|
104 |
|
105 lemma all_rexp: |
|
106 "\<lbrakk>finite (UNIV // \<approx>Lang); X \<in> (UNIV // \<approx>Lang)\<rbrakk> \<Longrightarrow> \<exists>r. X = L_rexp r" |
|
107 sorry |
|
108 |
|
109 lemma final_rexp: |
|
110 "\<lbrakk>finite (UNIV // (\<approx>Lang)); final X Lang\<rbrakk> \<Longrightarrow> \<exists>r. X = L_rexp r" |
|
111 unfolding final_def |
|
112 using all_rexp by blast |
|
113 |
|
114 lemma finite_f_one_to_one: |
|
115 assumes "finite B" |
|
116 and "\<forall>x \<in> B. \<exists>y. f y = x" |
|
117 shows "\<exists>rs. finite rs \<and> (B = {f y | y . y \<in> rs})" |
|
118 using assms |
|
119 by (induct) (auto) |
|
120 |
|
121 lemma finite_final: |
|
122 assumes "finite (UNIV // (\<approx>Lang))" |
|
123 shows "finite {X. final X Lang}" |
|
124 using assms |
|
125 proof - |
|
126 have "{X. final X Lang} \<subseteq> (UNIV // (\<approx>Lang))" |
|
127 unfolding final_def by auto |
|
128 with assms show "finite {X. final X Lang}" |
|
129 using finite_subset by auto |
|
130 qed |
|
131 |
|
132 lemma finite_regular_aux: |
|
133 fixes Lang :: "string set" |
|
134 assumes "finite (UNIV // (\<approx>Lang))" |
|
135 shows "\<exists>rs. Lang = L_rexp (folds ALT NULL rs)" |
|
136 apply(subst lang_is_union_of_finals) |
|
137 using assms |
|
138 apply - |
|
139 apply(drule finite_final) |
|
140 apply(drule_tac f="L_rexp" in finite_f_one_to_one) |
|
141 apply(clarify) |
|
142 apply(drule final_rexp[OF assms]) |
|
143 apply(auto)[1] |
|
144 apply(clarify) |
|
145 apply(rule_tac x="rs" in exI) |
|
146 apply(simp) |
|
147 apply(rule set_eqI) |
|
148 apply(auto) |
|
149 done |
|
150 |
|
151 lemma finite_regular: |
|
152 fixes Lang :: "string set" |
|
153 assumes "finite (UNIV // (\<approx>Lang))" |
|
154 shows "\<exists>r. Lang = L_rexp r" |
|
155 using assms finite_regular_aux |
|
156 by auto |
|
157 |
|
158 |
|
159 |
|
160 section {* other direction *} |
|
161 |
|
162 |
|
163 lemma inj_image_lang: |
|
164 fixes f::"string \<Rightarrow> 'a" |
|
165 assumes str_inj: "\<And>x y. f x = f y \<Longrightarrow> x \<approx>Lang y" |
|
166 shows "inj_on (image f) (UNIV // (\<approx>Lang))" |
|
167 proof - |
|
168 { fix x y::string |
|
169 assume eq_tag: "f ` {z. x \<approx>Lang z} = f ` {z. y \<approx>Lang z}" |
|
170 moreover |
|
171 have "{z. x \<approx>Lang z} \<noteq> {}" unfolding str_eq_def by auto |
|
172 ultimately obtain a b where "x \<approx>Lang a" "y \<approx>Lang b" "f a = f b" by blast |
|
173 then have "x \<approx>Lang a" "y \<approx>Lang b" "a \<approx>Lang b" using str_inj by auto |
|
174 then have "x \<approx>Lang y" unfolding str_eq_def by simp |
|
175 then have "{z. x \<approx>Lang z} = {z. y \<approx>Lang z}" unfolding str_eq_def by simp |
|
176 } |
|
177 then have "\<forall>x\<in>UNIV // \<approx>Lang. \<forall>y\<in>UNIV // \<approx>Lang. f ` x = f ` y \<longrightarrow> x = y" |
|
178 unfolding quotient_def Image_def str_eq_rel_def by simp |
|
179 then show "inj_on (image f) (UNIV // (\<approx>Lang))" |
|
180 unfolding inj_on_def by simp |
|
181 qed |
|
182 |
|
183 |
|
184 lemma finite_range_image: |
|
185 assumes fin: "finite (range f)" |
|
186 shows "finite ((image f) ` X)" |
|
187 proof - |
|
188 from fin have "finite (Pow (f ` UNIV))" by auto |
|
189 moreover |
|
190 have "(image f) ` X \<subseteq> Pow (f ` UNIV)" by auto |
|
191 ultimately show "finite ((image f) ` X)" using finite_subset by auto |
|
192 qed |
|
193 |
|
194 definition |
|
195 tag1 :: "string set \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> (string set \<times> string set)" |
|
196 where |
|
197 "tag1 L\<^isub>1 L\<^isub>2 \<equiv> \<lambda>x. ((\<approx>L\<^isub>1) `` {x}, (\<approx>L\<^isub>2) `` {x})" |
|
198 |
|
199 lemma tag1_range_finite: |
|
200 assumes finite1: "finite (UNIV // \<approx>L\<^isub>1)" |
|
201 and finite2: "finite (UNIV // \<approx>L\<^isub>2)" |
|
202 shows "finite (range (tag1 L\<^isub>1 L\<^isub>2))" |
|
203 proof - |
|
204 have "finite (UNIV // \<approx>L\<^isub>1 \<times> UNIV // \<approx>L\<^isub>2)" using finite1 finite2 by auto |
|
205 moreover |
|
206 have "range (tag1 L\<^isub>1 L\<^isub>2) \<subseteq> (UNIV // \<approx>L\<^isub>1) \<times> (UNIV // \<approx>L\<^isub>2)" |
|
207 unfolding tag1_def quotient_def by auto |
|
208 ultimately show "finite (range (tag1 L\<^isub>1 L\<^isub>2))" |
|
209 using finite_subset by blast |
|
210 qed |
|
211 |
|
212 lemma tag1_inj: |
|
213 "tag1 L\<^isub>1 L\<^isub>2 x = tag1 L\<^isub>1 L\<^isub>2 y \<Longrightarrow> x \<approx>(L\<^isub>1 \<union> L\<^isub>2) y" |
|
214 unfolding tag1_def Image_def str_eq_rel_def str_eq_def |
|
215 by auto |
|
216 |
|
217 lemma quot_alt_cu: |
|
218 fixes L\<^isub>1 L\<^isub>2::"string set" |
|
219 assumes fin1: "finite (UNIV // \<approx>L\<^isub>1)" |
|
220 and fin2: "finite (UNIV // \<approx>L\<^isub>2)" |
|
221 shows "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))" |
|
222 proof - |
|
223 have "finite (range (tag1 L\<^isub>1 L\<^isub>2))" |
|
224 using fin1 fin2 tag1_range_finite by simp |
|
225 then have "finite (image (tag1 L\<^isub>1 L\<^isub>2) ` (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2)))" |
|
226 using finite_range_image by blast |
|
227 moreover |
|
228 have "\<And>x y. tag1 L\<^isub>1 L\<^isub>2 x = tag1 L\<^isub>1 L\<^isub>2 y \<Longrightarrow> x \<approx>(L\<^isub>1 \<union> L\<^isub>2) y" |
|
229 using tag1_inj by simp |
|
230 then have "inj_on (image (tag1 L\<^isub>1 L\<^isub>2)) (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))" |
|
231 using inj_image_lang by blast |
|
232 ultimately |
|
233 show "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))" by (rule finite_imageD) |
|
234 qed |
|
235 |
|
236 |
|
237 section {* finite \<Rightarrow> regular *} |
|
238 |
|
239 definition |
|
240 transitions :: "string set \<Rightarrow> string set \<Rightarrow> rexp set" ("_\<Turnstile>\<Rightarrow>_") |
|
241 where |
|
242 "Y \<Turnstile>\<Rightarrow> X \<equiv> {CHAR c | c. Y ; {[c]} \<subseteq> X}" |
|
243 |
|
244 definition |
|
245 transitions_rexp ("_ \<turnstile>\<rightarrow> _") |
|
246 where |
|
247 "Y \<turnstile>\<rightarrow> X \<equiv> if [] \<in> X then folds ALT EMPTY (Y \<Turnstile>\<Rightarrow>X) else folds ALT NULL (Y \<Turnstile>\<Rightarrow>X)" |
|
248 |
|
249 definition |
|
250 "rhs CS X \<equiv> if X = {[]} then {({[]}, EMPTY)} else {(Y, Y \<turnstile>\<rightarrow>X) | Y. Y \<in> CS}" |
|
251 |
|
252 definition |
|
253 "rhs_sem CS X \<equiv> \<Union> {(Y; L_rexp r) | Y r . (Y, r) \<in> rhs CS X}" |
|
254 |
|
255 definition |
|
256 "eqs CS \<equiv> (\<Union>X \<in> CS. {(X, rhs CS X)})" |
|
257 |
|
258 definition |
|
259 "eqs_sem CS \<equiv> (\<Union>X \<in> CS. {(X, rhs_sem CS X)})" |
|
260 |
|
261 lemma [simp]: |
|
262 shows "finite (Y \<Turnstile>\<Rightarrow> X)" |
|
263 unfolding transitions_def |
|
264 by auto |
|
265 |
|
266 |
|
267 lemma defined_by_str: |
|
268 assumes "s \<in> X" |
|
269 and "X \<in> UNIV // (\<approx>Lang)" |
|
270 shows "X = (\<approx>Lang) `` {s}" |
|
271 using assms |
|
272 unfolding quotient_def Image_def |
|
273 unfolding str_eq_rel_def str_eq_def |
|
274 by auto |
|
275 |
|
276 lemma every_eqclass_has_transition: |
|
277 assumes has_str: "s @ [c] \<in> X" |
|
278 and in_CS: "X \<in> UNIV // (\<approx>Lang)" |
|
279 obtains Y where "Y \<in> UNIV // (\<approx>Lang)" and "Y ; {[c]} \<subseteq> X" and "s \<in> Y" |
|
280 proof - |
|
281 def Y \<equiv> "(\<approx>Lang) `` {s}" |
|
282 have "Y \<in> UNIV // (\<approx>Lang)" |
|
283 unfolding Y_def quotient_def by auto |
|
284 moreover |
|
285 have "X = (\<approx>Lang) `` {s @ [c]}" |
|
286 using has_str in_CS defined_by_str by blast |
|
287 then have "Y ; {[c]} \<subseteq> X" |
|
288 unfolding Y_def Image_def lang_seq_def |
|
289 unfolding str_eq_rel_def |
|
290 by (auto) (simp add: str_eq_def) |
|
291 moreover |
|
292 have "s \<in> Y" unfolding Y_def |
|
293 unfolding Image_def str_eq_rel_def str_eq_def by simp |
|
294 moreover |
|
295 have "True" by simp (* FIXME *) |
|
296 note that |
|
297 ultimately show thesis by blast |
|
298 qed |
|
299 |
|
300 lemma test: |
|
301 assumes "[] \<in> X" |
|
302 shows "[] \<in> L_rexp (Y \<turnstile>\<rightarrow> X)" |
|
303 using assms |
|
304 by (simp add: transitions_rexp_def) |
|
305 |
|
306 lemma rhs_sem: |
|
307 assumes "X \<in> (UNIV // (\<approx>Lang))" |
|
308 shows "X \<subseteq> rhs_sem (UNIV // (\<approx>Lang)) X" |
|
309 apply(case_tac "X = {[]}") |
|
310 apply(simp) |
|
311 apply(simp add: rhs_sem_def rhs_def lang_seq_def) |
|
312 apply(rule subsetI) |
|
313 apply(case_tac "x = []") |
|
314 apply(simp add: rhs_sem_def rhs_def) |
|
315 apply(rule_tac x = "X" in exI) |
|
316 apply(simp) |
|
317 apply(rule_tac x = "X" in exI) |
|
318 apply(simp add: assms) |
|
319 apply(simp add: transitions_rexp_def) |
|
320 oops |