182 |
182 |
183 lemma |
183 lemma |
184 shows "L\<star> \<subseteq> L\<star>\<star>" |
184 shows "L\<star> \<subseteq> L\<star>\<star>" |
185 by (rule lang_star_simple) |
185 by (rule lang_star_simple) |
186 |
186 |
187 section {* tricky section *} |
|
188 |
|
189 lemma k1: |
|
190 assumes b: "s \<in> L\<star>" |
|
191 and a: "s \<noteq> []" |
|
192 shows "s \<in> (L - {[]}); L\<star>" |
|
193 using b a |
|
194 apply(induct rule: Star.induct) |
|
195 apply(simp) |
|
196 apply(case_tac "s1=[]") |
|
197 apply(simp) |
|
198 apply(simp add: lang_seq_def) |
|
199 apply(blast) |
|
200 done |
|
201 |
|
202 section {* (relies on lemma k1) *} |
|
203 |
|
204 lemma zzz: |
|
205 shows "{s. c#s \<in> L1\<star>} = {s. c#s \<in> L1} ; (L1\<star>)" |
|
206 apply(auto simp add: lang_seq_def Cons_eq_append_conv) |
|
207 apply(drule k1) |
|
208 apply(auto)[1] |
|
209 apply(auto simp add: lang_seq_def)[1] |
|
210 apply(rule_tac x="tl s1" in exI) |
|
211 apply(rule_tac x="s2" in exI) |
|
212 apply(auto)[1] |
|
213 apply(auto simp add: Cons_eq_append_conv)[2] |
|
214 apply(drule lang_seq_append) |
|
215 apply(assumption) |
|
216 apply(rotate_tac 1) |
|
217 apply(drule rev_subsetD) |
|
218 apply(rule lang_star_seq_subseteq) |
|
219 apply(simp) |
|
220 done |
|
221 |
|
222 |
|
223 |
187 |
224 section {* regular expressions *} |
188 section {* regular expressions *} |
225 |
189 |
226 datatype rexp = |
190 datatype rexp = |
227 NULL |
191 NULL |
246 | "L_rexp (ALT r1 r2) = (L_rexp r1) \<union> (L_rexp r2)" |
210 | "L_rexp (ALT r1 r2) = (L_rexp r1) \<union> (L_rexp r2)" |
247 | "L_rexp (STAR r) = (L_rexp r)\<star>" |
211 | "L_rexp (STAR r) = (L_rexp r)\<star>" |
248 end |
212 end |
249 |
213 |
250 |
214 |
251 (* ************ now is the codes writen by chunhan ************************************* *) |
215 text{* ************ now is the codes writen by chunhan ************************************* *} |
252 |
216 |
253 section {* Arden's Lemma revised *} |
217 section {* Arden's Lemma revised *} |
254 |
218 |
255 lemma arden_aux1: |
219 lemma arden_aux1: |
256 assumes a: "X \<subseteq> X ; A \<union> B" |
220 assumes a: "X \<subseteq> X ; A \<union> B" |
309 section {* equiv class' definition *} |
273 section {* equiv class' definition *} |
310 |
274 |
311 definition |
275 definition |
312 equiv_str :: "string \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> bool" ("_ \<equiv>_\<equiv> _" [100, 100, 100] 100) |
276 equiv_str :: "string \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> bool" ("_ \<equiv>_\<equiv> _" [100, 100, 100] 100) |
313 where |
277 where |
314 "x \<equiv>L'\<equiv> y \<longleftrightarrow> (\<forall>z. x@z \<in> L' \<longleftrightarrow> y@z \<in> L')" |
278 "x \<equiv>Lang\<equiv> y \<longleftrightarrow> (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)" |
315 |
279 |
316 definition |
280 definition |
317 equiv_class :: "string \<Rightarrow> (string set) \<Rightarrow> string set" ("\<lbrakk>_\<rbrakk>_" [100, 100] 100) |
281 equiv_class :: "string \<Rightarrow> (string set) \<Rightarrow> string set" ("\<lbrakk>_\<rbrakk>_" [100, 100] 100) |
318 where |
282 where |
319 "\<lbrakk>x\<rbrakk>L' \<equiv> {y. x \<equiv>L'\<equiv> y}" |
283 "\<lbrakk>x\<rbrakk>Lang \<equiv> {y. x \<equiv>Lang\<equiv> y}" |
320 |
284 |
321 text {* Chunhan modifies Q to Quo *} |
285 text {* Chunhan modifies Q to Quo *} |
|
286 |
322 definition |
287 definition |
323 quot :: "string set \<Rightarrow> (string set) \<Rightarrow> (string set) set" ("_ Quo _" [100, 100] 100) |
288 quot :: "string set \<Rightarrow> string set \<Rightarrow> (string set) set" ("_ Quo _" [100, 100] 100) |
324 where |
289 where |
325 "L' Quo R \<equiv> { \<lbrakk>x\<rbrakk>R | x. x \<in> L'}" |
290 "L1 Quo L2 \<equiv> { \<lbrakk>x\<rbrakk>L2 | x. x \<in> L1}" |
|
291 |
|
292 |
|
293 |
|
294 |
326 |
295 |
327 lemma lang_eqs_union_of_eqcls: |
296 lemma lang_eqs_union_of_eqcls: |
328 "Lang = \<Union> {X. X \<in> (UNIV Quo Lang) \<and> (\<forall> x \<in> X. x \<in> Lang)}" |
297 "Lang = \<Union> {X. X \<in> (UNIV Quo Lang) \<and> (\<forall> x \<in> X. x \<in> Lang)}" |
329 proof |
298 proof |
330 show "Lang \<subseteq> \<Union>{X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}" |
299 show "Lang \<subseteq> \<Union>{X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}" |
365 |
334 |
366 types t_equa = "(string set \<times> t_equa_rhs)" |
335 types t_equa = "(string set \<times> t_equa_rhs)" |
367 |
336 |
368 types t_equas = "t_equa set" |
337 types t_equas = "t_equa set" |
369 |
338 |
370 text {* "empty_rhs" generates "\<lambda>" for init-state, just like "\<lambda>" for final states in Brzozowski method. |
339 text {* |
371 But if the init-state is "{[]}" ("\<lambda>" itself) then empty set is returned, see definition of "equation_rhs" *} |
340 "empty_rhs" generates "\<lambda>" for init-state, just like "\<lambda>" for final states |
|
341 in Brzozowski method. But if the init-state is "{[]}" ("\<lambda>" itself) then |
|
342 empty set is returned, see definition of "equation_rhs" |
|
343 *} |
|
344 |
372 definition |
345 definition |
373 empty_rhs :: "string set \<Rightarrow> t_equa_rhs" |
346 empty_rhs :: "string set \<Rightarrow> t_equa_rhs" |
374 where |
347 where |
375 "empty_rhs X \<equiv> if ([] \<in> X) then {({[]}, EMPTY)} else {}" |
348 "empty_rhs X \<equiv> if ([] \<in> X) then {({[]}, EMPTY)} else {}" |
376 |
349 |
1322 show "L (folds ALT NULL rS) \<subseteq> Lang" using finite_rS lang_eqs_union_of_eqcls[of Lang] has_cl_each |
1295 show "L (folds ALT NULL rS) \<subseteq> Lang" using finite_rS lang_eqs_union_of_eqcls[of Lang] has_cl_each |
1323 by (clarsimp simp:fold_alt_null_eqs) |
1296 by (clarsimp simp:fold_alt_null_eqs) |
1324 qed |
1297 qed |
1325 thus ?thesis by blast |
1298 thus ?thesis by blast |
1326 qed |
1299 qed |
1327 |
1300 |
|
1301 |
|
1302 text {* tests by Christian *} |
|
1303 |
|
1304 abbreviation |
|
1305 reg :: "string set => bool" |
|
1306 where |
|
1307 "reg L1 \<equiv> (\<exists>r::rexp. L r = L1)" |
|
1308 |
|
1309 lemma test1: |
|
1310 assumes finite_CS: "finite (UNIV Quo Lang)" |
|
1311 shows "reg Lang" |
|
1312 using finite_CS |
|
1313 by (auto dest: myhill_nerode) |
|
1314 |
|
1315 lemma t1: "(UNIV Quo {}) = {UNIV}" |
|
1316 apply(simp only: quot_def equiv_class_def equiv_str_def) |
|
1317 apply(simp) |
|
1318 done |
|
1319 |
|
1320 lemma |
|
1321 fixes r :: "rexp" |
|
1322 shows "finite (UNIV Quo (L r))" |
|
1323 apply(induct r) |
|
1324 apply(simp add: t1) |
|
1325 oops |
|
1326 |
|
1327 |
|
1328 |
1328 end |
1329 end |