279 definition |
279 definition |
280 quot :: "string set \<Rightarrow> string set \<Rightarrow> (string set) set" ("_ Quo _" [100, 100] 100) |
280 quot :: "string set \<Rightarrow> string set \<Rightarrow> (string set) set" ("_ Quo _" [100, 100] 100) |
281 where |
281 where |
282 "L1 Quo L2 \<equiv> { \<lbrakk>x\<rbrakk>L2 | x. x \<in> L1}" |
282 "L1 Quo L2 \<equiv> { \<lbrakk>x\<rbrakk>L2 | x. x \<in> L1}" |
283 |
283 |
284 |
|
285 lemma lang_eqs_union_of_eqcls: |
284 lemma lang_eqs_union_of_eqcls: |
286 "Lang = \<Union> {X. X \<in> (UNIV Quo Lang) \<and> (\<forall> x \<in> X. x \<in> Lang)}" |
285 "Lang = (\<Union> {X. X \<in> (UNIV Quo Lang) \<and> (\<forall> x \<in> X. x \<in> Lang)})" |
287 proof |
286 proof |
288 show "Lang \<subseteq> \<Union>{X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}" |
287 show "Lang \<subseteq> \<Union>{X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}" |
289 proof |
288 proof |
290 fix x |
289 fix x |
291 assume "x \<in> Lang" |
290 assume "x \<in> Lang" |
303 next |
302 next |
304 show "\<Union>{X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang} \<subseteq> Lang" |
303 show "\<Union>{X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang} \<subseteq> Lang" |
305 by auto |
304 by auto |
306 qed |
305 qed |
307 |
306 |
|
307 |
308 lemma empty_notin_CS: "{} \<notin> UNIV Quo Lang" |
308 lemma empty_notin_CS: "{} \<notin> UNIV Quo Lang" |
309 apply (clarsimp simp:quot_def equiv_class_def) |
309 apply (clarsimp simp:quot_def equiv_class_def) |
310 by (rule_tac x = x in exI, auto simp:equiv_str_def) |
310 by (rule_tac x = x in exI, auto simp:equiv_str_def) |
311 |
311 |
312 lemma no_two_cls_inters: |
312 lemma no_two_cls_inters: |
315 |
315 |
316 text {* equiv_class transition *} |
316 text {* equiv_class transition *} |
317 definition |
317 definition |
318 CT :: "string set \<Rightarrow> char \<Rightarrow> string set \<Rightarrow> bool" ("_-_\<rightarrow>_" [99,99]99) |
318 CT :: "string set \<Rightarrow> char \<Rightarrow> string set \<Rightarrow> bool" ("_-_\<rightarrow>_" [99,99]99) |
319 where |
319 where |
320 "X-c\<rightarrow>Y \<equiv> ((X;{[c]}) \<subseteq> Y)" |
320 "X-c\<rightarrow>Y \<equiv> ( X; {[c]} \<subseteq> Y)" |
321 |
321 |
322 types t_equa_rhs = "(string set \<times> rexp) set" |
322 types t_equa_rhs = "(string set \<times> rexp) set" |
323 |
323 |
324 types t_equa = "(string set \<times> t_equa_rhs)" |
324 types t_equa = "(string set \<times> t_equa_rhs)" |
325 |
325 |
343 |
343 |
344 definition |
344 definition |
345 equation_rhs :: "(string set) set \<Rightarrow> string set \<Rightarrow> t_equa_rhs" |
345 equation_rhs :: "(string set) set \<Rightarrow> string set \<Rightarrow> t_equa_rhs" |
346 where |
346 where |
347 "equation_rhs CS X \<equiv> if (X = {[]}) then {({[]}, EMPTY)} |
347 "equation_rhs CS X \<equiv> if (X = {[]}) then {({[]}, EMPTY)} |
348 else {(S, folds ALT NULL {CHAR c| c. S-c\<rightarrow>X} )| S. S \<in> CS} \<union> empty_rhs X" |
348 else {(S, folds ALT NULL {CHAR c| c. S-c\<rightarrow>X} )| S. S \<in> CS} \<union> empty_rhs X" |
349 |
349 |
350 definition |
350 definition |
351 equations :: "(string set) set \<Rightarrow> t_equas" |
351 equations :: "(string set) set \<Rightarrow> t_equas" |
352 where |
352 where |
353 "equations CS \<equiv> {(X, equation_rhs CS X) | X. X \<in> CS}" |
353 "equations CS \<equiv> {(X, equation_rhs CS X) | X. X \<in> CS}" |
503 definition |
503 definition |
504 merge_rhs :: "t_equa_rhs \<Rightarrow> t_equa_rhs \<Rightarrow> t_equa_rhs" |
504 merge_rhs :: "t_equa_rhs \<Rightarrow> t_equa_rhs \<Rightarrow> t_equa_rhs" |
505 where |
505 where |
506 "merge_rhs rhs rhs' \<equiv> {(X, r). (\<exists> r1 r2. ((X,r1) \<in> rhs \<and> (X, r2) \<in> rhs') \<and> r = ALT r1 r2) \<or> |
506 "merge_rhs rhs rhs' \<equiv> {(X, r). (\<exists> r1 r2. ((X,r1) \<in> rhs \<and> (X, r2) \<in> rhs') \<and> r = ALT r1 r2) \<or> |
507 (\<exists> r1. (X, r1) \<in> rhs \<and> (\<not> (\<exists> r2. (X, r2) \<in> rhs')) \<and> r = r1) \<or> |
507 (\<exists> r1. (X, r1) \<in> rhs \<and> (\<not> (\<exists> r2. (X, r2) \<in> rhs')) \<and> r = r1) \<or> |
508 (\<exists> r2. (X, r2) \<in> rhs' \<and> (\<not> (\<exists> r1. (X, r1) \<in> rhs)) \<and> r = r2) }" |
508 (\<exists> r2. (X, r2) \<in> rhs' \<and> (\<not> (\<exists> r1. (X, r1) \<in> rhs)) \<and> r = r2) }" |
509 |
509 |
510 |
510 |
511 text {* rhs_subst rhs X=xrhs r: substitude all occurence of X in rhs((X,r) \<in> rhs) with xrhs *} |
511 text {* rhs_subst rhs X=xrhs r: substitude all occurence of X in rhs((X,r) \<in> rhs) with xrhs *} |
512 definition |
512 definition |
513 rhs_subst :: "t_equa_rhs \<Rightarrow> string set \<Rightarrow> t_equa_rhs \<Rightarrow> rexp \<Rightarrow> t_equa_rhs" |
513 rhs_subst :: "t_equa_rhs \<Rightarrow> string set \<Rightarrow> t_equa_rhs \<Rightarrow> rexp \<Rightarrow> t_equa_rhs" |
629 Inv: Invairance of the equation-system, during the decrease of the equation-system, Inv holds. |
629 Inv: Invairance of the equation-system, during the decrease of the equation-system, Inv holds. |
630 *} |
630 *} |
631 definition Inv :: "string set \<Rightarrow> t_equas \<Rightarrow> bool" |
631 definition Inv :: "string set \<Rightarrow> t_equas \<Rightarrow> bool" |
632 where |
632 where |
633 "Inv X ES \<equiv> finite ES \<and> (\<exists> rhs. (X, rhs) \<in> ES) \<and> distinct_equas ES \<and> |
633 "Inv X ES \<equiv> finite ES \<and> (\<exists> rhs. (X, rhs) \<in> ES) \<and> distinct_equas ES \<and> |
634 (\<forall> X xrhs. (X, xrhs) \<in> ES \<longrightarrow> ardenable (X, xrhs) \<and> X \<noteq> {} \<and> rhs_eq_cls xrhs \<subseteq> insert {[]} (left_eq_cls ES))" |
634 (\<forall> X xrhs. (X, xrhs) \<in> ES \<longrightarrow> ardenable (X, xrhs) \<and> X \<noteq> {} \<and> rhs_eq_cls xrhs |
|
635 \<subseteq> insert {[]} (left_eq_cls ES))" |
635 |
636 |
636 text {* |
637 text {* |
637 TCon: Termination Condition of the equation-system decreasion. |
638 TCon: Termination Condition of the equation-system decreasion. |
638 *} |
639 *} |
639 definition TCon:: "'a set \<Rightarrow> bool" |
640 definition TCon:: "'a set \<Rightarrow> bool" |
641 "TCon ES \<equiv> card ES = 1" |
642 "TCon ES \<equiv> card ES = 1" |
642 |
643 |
643 |
644 |
644 text {* |
645 text {* |
645 The following is a iteration principle, and is the main framework for the proof: |
646 The following is a iteration principle, and is the main framework for the proof: |
646 1: We can form the initial equation-system using "equations" defined above, and prove it has invariance Inv by lemma "init_ES_satisfy_Inv"; |
|
647 2: We can decrease the number of the equation-system using ardens_lemma_revised and substitution ("equas_subst", defined above), |
|
648 and prove it holds the property "step" in "wf_iter" by lemma "iteration_step" |
|
649 and finally using property Inv and TCon to prove the myhill-nerode theorem |
|
650 |
647 |
|
648 1: We can form the initial equation-system using "equations" defined above, |
|
649 and prove it has invariance Inv by lemma "init_ES_satisfy_Inv"; |
|
650 |
|
651 2: We can decrease the number of the equation-system using ardens_lemma_revised |
|
652 and substitution ("equas_subst", defined above), |
|
653 and prove it holds the property "step" in "wf_iter" by lemma "iteration_step" |
|
654 and finally using property Inv and TCon to prove the myhill-nerode theorem |
651 *} |
655 *} |
652 lemma wf_iter [rule_format]: |
656 lemma wf_iter [rule_format]: |
653 fixes f |
657 fixes f |
654 assumes step: "\<And> e. \<lbrakk>P e; \<not> Q e\<rbrakk> \<Longrightarrow> (\<exists> e'. P e' \<and> (f(e'), f(e)) \<in> less_than)" |
658 assumes step: "\<And> e. \<lbrakk>P e; \<not> Q e\<rbrakk> \<Longrightarrow> (\<exists> e'. P e' \<and> (f(e'), f(e)) \<in> less_than)" |
655 shows pe: "P e \<longrightarrow> (\<exists> e'. P e' \<and> Q e')" |
659 shows pe: "P e \<longrightarrow> (\<exists> e'. P e' \<and> Q e')" |
800 |
804 |
801 lemma no_EMPTY_equations: |
805 lemma no_EMPTY_equations: |
802 "(X, xrhs) \<in> equations CS \<Longrightarrow> no_EMPTY_rhs xrhs" |
806 "(X, xrhs) \<in> equations CS \<Longrightarrow> no_EMPTY_rhs xrhs" |
803 apply (clarsimp simp add:equations_def equation_rhs_def) |
807 apply (clarsimp simp add:equations_def equation_rhs_def) |
804 apply (simp add:no_EMPTY_rhs_def empty_rhs_def, auto) |
808 apply (simp add:no_EMPTY_rhs_def empty_rhs_def, auto) |
805 apply (subgoal_tac "finite {CHAR c |c. Xa-c\<rightarrow>X}", drule_tac x = "[]" in fold_alt_null_eqs, clarsimp, rule finite_charset_rS)+ |
809 apply (subgoal_tac "finite {CHAR c |c. Xa-c\<rightarrow>X}", |
|
810 drule_tac x = "[]" in fold_alt_null_eqs, clarsimp, rule finite_charset_rS)+ |
806 done |
811 done |
807 |
812 |
808 lemma init_ES_satisfy_ardenable: |
813 lemma init_ES_satisfy_ardenable: |
809 "(X, xrhs) \<in> equations (UNIV Quo Lang) \<Longrightarrow> ardenable (X, xrhs)" |
814 "(X, xrhs) \<in> equations (UNIV Quo Lang) \<Longrightarrow> ardenable (X, xrhs)" |
810 unfolding ardenable_def |
815 unfolding ardenable_def |
887 by (auto simp:insert_absorb) |
892 by (auto simp:insert_absorb) |
888 |
893 |
889 lemma ardenable_prop: |
894 lemma ardenable_prop: |
890 assumes not_lambda: "Y \<noteq> {[]}" |
895 assumes not_lambda: "Y \<noteq> {[]}" |
891 and ardable: "ardenable (Y, yrhs)" |
896 and ardable: "ardenable (Y, yrhs)" |
892 shows "\<exists> yrhs'. Y = L yrhs' \<and> distinct_rhs yrhs' \<and> rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" (is "\<exists> yrhs'. ?P yrhs'") |
897 shows "\<exists> yrhs'. Y = L yrhs' \<and> distinct_rhs yrhs' \<and> rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" |
|
898 (is "\<exists> yrhs'. ?P yrhs'") |
893 proof (cases "(\<exists> reg. (Y, reg) \<in> yrhs)") |
899 proof (cases "(\<exists> reg. (Y, reg) \<in> yrhs)") |
894 case True |
900 case True |
895 thus ?thesis |
901 thus ?thesis |
896 proof |
902 proof |
897 fix reg |
903 fix reg |
1304 qed |
1310 qed |
1305 |
1311 |
1306 |
1312 |
1307 text {* tests by Christian *} |
1313 text {* tests by Christian *} |
1308 |
1314 |
1309 (* Alternative definition for Quo *) |
1315 lemma temp_set_ext[no_atp]: "(\<And>x. (x:A) = (x:B)) \<Longrightarrow> (A = B)" |
|
1316 by(auto intro:set_eqI) |
|
1317 |
|
1318 fun |
|
1319 MNRel |
|
1320 where |
|
1321 "MNRel Lang (x, y) = (x \<equiv>Lang\<equiv> y)" |
|
1322 |
|
1323 lemma |
|
1324 "equiv UNIV (MNRel Lang)" |
|
1325 unfolding equiv_def |
|
1326 unfolding refl_on_def sym_def trans_def |
|
1327 apply(auto simp add: mem_def equiv_str_def) |
|
1328 done |
|
1329 |
|
1330 lemma |
|
1331 "(MNRel Lang)``{x} = \<lbrakk>x\<rbrakk>Lang" |
|
1332 unfolding equiv_class_def Image_def mem_def |
|
1333 by (simp) |
|
1334 |
|
1335 lemma tt: "\<lbrakk>A = B; C \<subseteq> B\<rbrakk> \<Longrightarrow> C \<subseteq> A" by simp |
|
1336 |
|
1337 lemma |
|
1338 "UNIV//(MNRel (L1 \<union> L2)) \<subseteq> (UNIV//(MNRel L1)) \<union> (UNIV//(MNRel L2))" |
|
1339 unfolding quotient_def |
|
1340 unfolding UNION_eq_Union_image |
|
1341 apply(rule tt) |
|
1342 apply(rule Un_Union_image[symmetric]) |
|
1343 apply(simp) |
|
1344 apply(rule UN_mono) |
|
1345 apply(simp) |
|
1346 apply(simp) |
|
1347 unfolding Image_def |
|
1348 unfolding mem_def |
|
1349 unfolding MNRel.simps |
|
1350 apply(simp) |
|
1351 oops |
|
1352 |
|
1353 |
|
1354 |
|
1355 text {* Alternative definition for Quo *} |
1310 definition |
1356 definition |
1311 QUOT :: "string set \<Rightarrow> (string set) set" |
1357 QUOT :: "string set \<Rightarrow> (string set) set" |
1312 where |
1358 where |
1313 "QUOT Lang \<equiv> (\<Union>x. {\<lbrakk>x\<rbrakk>Lang})" |
1359 "QUOT Lang \<equiv> (\<Union>x. {\<lbrakk>x\<rbrakk>Lang})" |
|
1360 |
|
1361 lemma test_01: |
|
1362 "Lang \<subseteq> (\<Union> QUOT Lang)" |
|
1363 unfolding QUOT_def equiv_class_def equiv_str_def |
|
1364 by (blast) |
|
1365 |
1314 |
1366 |
1315 (* by chunhan *) |
1367 (* by chunhan *) |
1316 lemma quot_lambda: "QUOT {[]} = {{[]}, UNIV - {[]}}" |
1368 lemma quot_lambda: "QUOT {[]} = {{[]}, UNIV - {[]}}" |
1317 proof |
1369 proof |
1318 show "QUOT {[]} \<subseteq> {{[]}, UNIV - {[]}}" |
1370 show "QUOT {[]} \<subseteq> {{[]}, UNIV - {[]}}" |
1392 by (auto simp add:equiv_str_def) |
1444 by (auto simp add:equiv_str_def) |
1393 moreover have "xa = [c] \<Longrightarrow> x = {[c]}" |
1445 moreover have "xa = [c] \<Longrightarrow> x = {[c]}" |
1394 proof - |
1446 proof - |
1395 have "xa = [c] \<Longrightarrow> {y. xa \<equiv>{[c]}\<equiv> y} = {[c]}" using in_eqiv |
1447 have "xa = [c] \<Longrightarrow> {y. xa \<equiv>{[c]}\<equiv> y} = {[c]}" using in_eqiv |
1396 apply (simp add:equiv_str_def) |
1448 apply (simp add:equiv_str_def) |
1397 apply (rule set_ext, rule iffI, simp) |
1449 apply (rule temp_set_ext, rule iffI, simp) |
1398 apply (drule_tac x = "[]" in spec, auto) |
1450 apply (drule_tac x = "[]" in spec, auto) |
1399 done |
1451 done |
1400 thus "xa = [c] \<Longrightarrow> x = {[c]}" using in_eqiv by simp |
1452 thus "xa = [c] \<Longrightarrow> x = {[c]}" using in_eqiv by simp |
1401 qed |
1453 qed |
1402 moreover have "\<lbrakk>xa \<noteq> []; xa \<noteq> [c]\<rbrakk> \<Longrightarrow> x = UNIV - {[],[c]}" |
1454 moreover have "\<lbrakk>xa \<noteq> []; xa \<noteq> [c]\<rbrakk> \<Longrightarrow> x = UNIV - {[],[c]}" |
1403 proof - |
1455 proof - |
1404 have "\<lbrakk>xa \<noteq> []; xa \<noteq> [c]\<rbrakk> \<Longrightarrow> {y. xa \<equiv>{[c]}\<equiv> y} = UNIV - {[],[c]}" |
1456 have "\<lbrakk>xa \<noteq> []; xa \<noteq> [c]\<rbrakk> \<Longrightarrow> {y. xa \<equiv>{[c]}\<equiv> y} = UNIV - {[],[c]}" |
1405 apply (clarsimp simp add:equiv_str_def) |
1457 apply (clarsimp simp add:equiv_str_def) |
1406 apply (rule set_ext, rule iffI, simp) |
1458 apply (rule temp_set_ext, rule iffI, simp) |
1407 apply (rule conjI) |
1459 apply (rule conjI) |
1408 apply (drule_tac x = "[c]" in spec, simp) |
1460 apply (drule_tac x = "[c]" in spec, simp) |
1409 apply (drule_tac x = "[]" in spec, simp) |
1461 apply (drule_tac x = "[]" in spec, simp) |
1410 by (auto dest:quot_single_aux) |
1462 by (auto dest:quot_single_aux) |
1411 thus "\<lbrakk>xa \<noteq> []; xa \<noteq> [c]\<rbrakk> \<Longrightarrow> x = UNIV - {[],[c]}" using in_eqiv by simp |
1463 thus "\<lbrakk>xa \<noteq> []; xa \<noteq> [c]\<rbrakk> \<Longrightarrow> x = UNIV - {[],[c]}" using in_eqiv by simp |
1427 apply (simp add:QUOT_def equiv_class_def equiv_str_def) |
1479 apply (simp add:QUOT_def equiv_class_def equiv_str_def) |
1428 by (rule_tac x = "[]" in exI, auto) |
1480 by (rule_tac x = "[]" in exI, auto) |
1429 moreover have "x = {[c]} \<Longrightarrow> x \<in> QUOT {[c]}" |
1481 moreover have "x = {[c]} \<Longrightarrow> x \<in> QUOT {[c]}" |
1430 apply (simp add:QUOT_def equiv_class_def equiv_str_def) |
1482 apply (simp add:QUOT_def equiv_class_def equiv_str_def) |
1431 apply (rule_tac x = "[c]" in exI, simp) |
1483 apply (rule_tac x = "[c]" in exI, simp) |
1432 apply (rule set_ext, rule iffI, simp+) |
1484 apply (rule temp_set_ext, rule iffI, simp+) |
1433 by (drule_tac x = "[]" in spec, simp) |
1485 by (drule_tac x = "[]" in spec, simp) |
1434 moreover have "x = UNIV - {[],[c]} \<Longrightarrow> x \<in> QUOT {[c]}" |
1486 moreover have "x = UNIV - {[],[c]} \<Longrightarrow> x \<in> QUOT {[c]}" |
1435 using exist_another |
1487 using exist_another |
1436 apply (clarsimp simp add:QUOT_def equiv_class_def equiv_str_def) |
1488 apply (clarsimp simp add:QUOT_def equiv_class_def equiv_str_def) |
1437 apply (rule_tac x = "[a]" in exI, simp) |
1489 apply (rule_tac x = "[a]" in exI, simp) |
1438 apply (rule set_ext, rule iffI, simp) |
1490 apply (rule temp_set_ext, rule iffI, simp) |
1439 apply (clarsimp simp:quot_single_aux, simp) |
1491 apply (clarsimp simp:quot_single_aux, simp) |
1440 apply (rule conjI) |
1492 apply (rule conjI) |
1441 apply (drule_tac x = "[c]" in spec, simp) |
1493 apply (drule_tac x = "[c]" in spec, simp) |
1442 by (drule_tac x = "[]" in spec, simp) |
1494 by (drule_tac x = "[]" in spec, simp) |
1443 ultimately show ?thesis using in_res by blast |
1495 ultimately show ?thesis using in_res by blast |
1451 and finite2: "finite (QUOT L\<^isub>2)" |
1503 and finite2: "finite (QUOT L\<^isub>2)" |
1452 shows "finite (QUOT (L\<^isub>1;L\<^isub>2))" |
1504 shows "finite (QUOT (L\<^isub>1;L\<^isub>2))" |
1453 apply (simp add:QUOT_def equiv_class_def equiv_str_def) |
1505 apply (simp add:QUOT_def equiv_class_def equiv_str_def) |
1454 sorry |
1506 sorry |
1455 |
1507 |
|
1508 |
|
1509 lemma a: |
|
1510 "\<lbrakk>x \<equiv>L1\<equiv> y \<and> x \<equiv>L2\<equiv> y\<rbrakk> \<Longrightarrow> x \<equiv>(L1 \<union> L2)\<equiv> y" |
|
1511 apply(simp add: equiv_str_def) |
|
1512 done |
|
1513 |
|
1514 |
|
1515 lemma QUOT_union: |
|
1516 "(QUOT (L1 \<union> L2)) \<subseteq> ((QUOT L1) \<union> (QUOT L2))" |
|
1517 sorry |
|
1518 |
|
1519 |
1456 lemma quot_alt: |
1520 lemma quot_alt: |
1457 assumes finite1: "finite (QUOT L\<^isub>1)" |
1521 assumes finite1: "finite (QUOT L\<^isub>1)" |
1458 and finite2: "finite (QUOT L\<^isub>2)" |
1522 and finite2: "finite (QUOT L\<^isub>2)" |
1459 shows "finite (QUOT (L\<^isub>1 \<union> L\<^isub>2))" |
1523 shows "finite (QUOT (L\<^isub>1 \<union> L\<^isub>2))" |
1460 sorry |
1524 apply(rule finite_subset) |
|
1525 apply(rule QUOT_union) |
|
1526 apply(simp add: finite1 finite2) |
|
1527 done |
1461 |
1528 |
1462 lemma quot_star: |
1529 lemma quot_star: |
1463 assumes finite1: "finite (QUOT L\<^isub>1)" |
1530 assumes finite1: "finite (QUOT L\<^isub>1)" |
1464 shows "finite (QUOT (L\<^isub>1\<star>))" |
1531 shows "finite (QUOT (L\<^isub>1\<star>))" |
1465 sorry |
1532 sorry |
1468 "Lang = L (r::rexp) \<Longrightarrow> finite (QUOT Lang)" |
1535 "Lang = L (r::rexp) \<Longrightarrow> finite (QUOT Lang)" |
1469 apply (induct arbitrary:Lang rule:rexp.induct) |
1536 apply (induct arbitrary:Lang rule:rexp.induct) |
1470 apply (simp add:QUOT_def equiv_class_def equiv_str_def) |
1537 apply (simp add:QUOT_def equiv_class_def equiv_str_def) |
1471 by (simp_all add:quot_lambda quot_single quot_seq quot_alt quot_star) |
1538 by (simp_all add:quot_lambda quot_single quot_seq quot_alt quot_star) |
1472 |
1539 |
1473 |
|
1474 |
|
1475 |
|
1476 |
|
1477 |
|
1478 lemma test: |
1540 lemma test: |
1479 "UNIV Quo Lang = QUOT Lang" |
1541 "UNIV Quo Lang = QUOT Lang" |
1480 by (auto simp add: quot_def QUOT_def) |
1542 by (auto simp add: quot_def QUOT_def) |
1481 |
1543 |
1482 lemma test1: |
|
1483 assumes finite_CS: "finite (QUOT Lang)" |
|
1484 shows "reg Lang" |
|
1485 using finite_CS |
|
1486 unfolding test[symmetric] |
|
1487 by (auto dest: myhill_nerode) |
|
1488 |
|
1489 lemma t1: "(QUOT {}) = {UNIV}" |
|
1490 apply(simp only: QUOT_def equiv_class_def equiv_str_def) |
|
1491 apply(simp) |
|
1492 done |
|
1493 |
|
1494 lemma t2: "{[]} \<in> (QUOT {[]})" |
|
1495 apply(simp only: QUOT_def equiv_class_def equiv_str_def) |
|
1496 apply(simp) |
|
1497 apply(simp add: set_eq_iff) |
|
1498 apply(rule_tac x="[]" in exI) |
|
1499 apply(simp) |
|
1500 by (metis eq_commute) |
|
1501 |
|
1502 |
|
1503 lemma t2': "X \<in> (QUOT {[]})" |
|
1504 apply(simp only: QUOT_def equiv_class_def equiv_str_def) |
|
1505 apply(simp) |
|
1506 apply(simp add: set_eq_iff) |
|
1507 apply(rule_tac x="[]" in exI) |
|
1508 apply(simp) |
|
1509 apply(rule allI) |
|
1510 |
|
1511 by (metis eq_commute) |
|
1512 |
|
1513 oops |
|
1514 |
|
1515 lemma |
|
1516 fixes r :: "rexp" |
|
1517 shows "finite (QUOT (L r))" |
|
1518 apply(induct r) |
|
1519 apply(simp add: t1) |
|
1520 apply(simp add: QUOT_def) |
|
1521 apply(simp add: equiv_class_def equiv_str_def) |
|
1522 apply(rule finite_UN_I) |
|
1523 oops |
|
1524 |
|
1525 lemma |
|
1526 fixes r :: "rexp" |
|
1527 shows "finite (UNIV Quo (L r))" |
|
1528 apply(induct r) |
|
1529 prefer 2 |
|
1530 apply(simp add: quot_def) |
|
1531 apply(simp add: equiv_class_def equiv_str_def) |
|
1532 apply(rule finite_UN_I) |
|
1533 apply(simp) |
|
1534 |
1544 |
1535 |
1545 |
1536 end |
1546 end |