756 assume "(1)": "x \<in> X" |
752 assume "(1)": "x \<in> X" |
757 show "x \<in> L xrhs" |
753 show "x \<in> L xrhs" |
758 proof (cases "x = []") |
754 proof (cases "x = []") |
759 assume empty: "x = []" |
755 assume empty: "x = []" |
760 hence "x \<in> L (empty_rhs X)" using "(1)" |
756 hence "x \<in> L (empty_rhs X)" using "(1)" |
761 unfolding empty_rhs_def |
757 by (auto simp:empty_rhs_def lang_seq_def) |
762 by (simp add: lang_seq_def) |
|
763 thus ?thesis using X_in_equas False empty "(1)" |
758 thus ?thesis using X_in_equas False empty "(1)" |
764 unfolding equations_def equation_rhs_def by auto |
759 unfolding equations_def equation_rhs_def by auto |
765 next |
760 next |
766 assume not_empty: "x \<noteq> []" |
761 assume not_empty: "x \<noteq> []" |
767 then obtain clist c where decom: "x = clist @ [c]" |
762 hence "\<exists> clist c. x = clist @ [c]" by (case_tac x rule:rev_cases, auto) |
768 using rev_cases by blast |
763 then obtain clist c where decom: "x = clist @ [c]" by blast |
769 moreover have "\<And> Y. Y-c\<rightarrow>X \<Longrightarrow> [c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})" |
764 moreover have "\<And> Y. \<lbrakk>Y \<in> UNIV Quo Lang; Y-c\<rightarrow>X; clist \<in> Y\<rbrakk> |
|
765 \<Longrightarrow> [c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})" |
770 proof - |
766 proof - |
771 fix Y |
767 fix Y |
772 assume Y_CT_X: "Y-c\<rightarrow>X" |
768 assume Y_is_eq_cl: "Y \<in> UNIV Quo Lang" |
|
769 and Y_CT_X: "Y-c\<rightarrow>X" |
|
770 and clist_in_Y: "clist \<in> Y" |
773 with finite_charset_rS |
771 with finite_charset_rS |
774 show "[c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})" |
772 show "[c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})" |
775 by (auto simp: fold_alt_null_eqs) |
773 by (auto simp :fold_alt_null_eqs) |
776 qed |
774 qed |
777 hence "\<exists>Xa. Xa \<in> UNIV Quo Lang \<and> clist @ [c] \<in> Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})" |
775 hence "\<exists>Xa. Xa \<in> UNIV Quo Lang \<and> clist @ [c] \<in> Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})" |
778 using X_in_equas False not_empty "(1)" decom |
776 using X_in_equas False not_empty "(1)" decom |
779 by (auto dest!: every_eqclass_has_ascendent simp: equations_def equation_rhs_def lang_seq_def) |
777 by (auto dest!:every_eqclass_has_ascendent simp:equations_def equation_rhs_def lang_seq_def) |
780 then obtain Xa where |
778 then obtain Xa where |
781 "Xa \<in> UNIV Quo Lang" "clist @ [c] \<in> Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})" by blast |
779 "Xa \<in> UNIV Quo Lang \<and> clist @ [c] \<in> Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})" by blast |
782 hence "x \<in> L {(S, folds ALT NULL {CHAR c |c. S-c\<rightarrow>X}) |S. S \<in> UNIV Quo Lang}" |
780 hence "x \<in> L {(S, folds ALT NULL {CHAR c |c. S-c\<rightarrow>X}) |S. S \<in> UNIV Quo Lang}" |
783 using X_in_equas "(1)" decom |
781 using X_in_equas "(1)" decom |
784 by (auto simp add:equations_def equation_rhs_def intro!:exI[where x = Xa]) |
782 by (auto simp add:equations_def equation_rhs_def intro!:exI[where x = Xa]) |
785 thus "x \<in> L xrhs" using X_in_equas False not_empty |
783 thus "x \<in> L xrhs" using X_in_equas False not_empty unfolding equations_def equation_rhs_def |
786 unfolding equations_def equation_rhs_def |
|
787 by auto |
784 by auto |
788 qed |
785 qed |
789 qed |
786 qed |
790 next |
787 next |
791 show "L xrhs \<subseteq> X" |
788 show "L xrhs \<subseteq> X" |
792 proof |
789 proof |
793 fix x |
790 fix x |
794 assume "(2)": "x \<in> L xrhs" |
791 assume "(2)": "x \<in> L xrhs" |
795 have "(2_1)": "\<And> s1 s2 r Xa. \<lbrakk>s1 \<in> Xa; s2 \<in> L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> X" |
792 have "(2_1)": "\<And> s1 s2 r Xa. \<lbrakk>s1 \<in> Xa; s2 \<in> L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> X" |
796 using finite_charset_rS |
793 using finite_charset_rS |
797 unfolding CT_def |
794 by (auto simp:CT_def lang_seq_def fold_alt_null_eqs) |
798 by (simp add: lang_seq_def fold_alt_null_eqs) (auto) |
|
799 have "(2_2)": "\<And> s1 s2 Xa r.\<lbrakk>s1 \<in> Xa; s2 \<in> L r; (Xa, r) \<in> empty_rhs X\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> X" |
795 have "(2_2)": "\<And> s1 s2 Xa r.\<lbrakk>s1 \<in> Xa; s2 \<in> L r; (Xa, r) \<in> empty_rhs X\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> X" |
800 by (simp add: empty_rhs_def split: if_splits) |
796 by (simp add:empty_rhs_def split:if_splits) |
801 show "x \<in> X" using X_in_equas False "(2)" |
797 show "x \<in> X" using X_in_equas False "(2)" |
802 unfolding equations_def |
798 by (auto intro:"(2_1)" "(2_2)" simp:equations_def equation_rhs_def lang_seq_def) |
803 unfolding equation_rhs_def |
|
804 by (auto intro:"(2_1)" "(2_2)" simp: lang_seq_def) |
|
805 qed |
799 qed |
806 qed |
800 qed |
807 qed |
801 qed |
808 |
802 |
809 |
803 |
1316 qed |
1310 qed |
1317 |
1311 |
1318 |
1312 |
1319 text {* tests by Christian *} |
1313 text {* tests by Christian *} |
1320 |
1314 |
1321 (* compatibility with stable Isabelle *) |
|
1322 lemma temp_set_ext[no_atp]: "(\<And>x. (x:A) = (x:B)) \<Longrightarrow> (A = B)" |
1315 lemma temp_set_ext[no_atp]: "(\<And>x. (x:A) = (x:B)) \<Longrightarrow> (A = B)" |
1323 by(auto intro:set_eqI) |
1316 by(auto intro:set_eqI) |
1324 |
1317 |
1325 lemma folds_simp_null [simp]: |
1318 fun |
1326 "finite rs \<Longrightarrow> x \<in> L (folds ALT NULL rs) = (\<exists>r \<in> rs. x \<in> L r)" |
1319 MNRel |
1327 apply (simp add: folds_def) |
1320 where |
1328 apply (rule someI2_ex) |
1321 "MNRel Lang (x, y) = (x \<equiv>Lang\<equiv> y)" |
1329 apply (erule finite_imp_fold_graph) |
1322 |
1330 apply (erule fold_graph.induct) |
1323 lemma |
1331 apply (auto) |
1324 "equiv UNIV (MNRel Lang)" |
1332 done |
|
1333 |
|
1334 lemma folds_simp_empty [simp]: |
|
1335 "finite rs \<Longrightarrow> x \<in> L (folds ALT EMPTY rs) = ((\<exists>r \<in> rs. x \<in> L r) \<or> x = [])" |
|
1336 apply (simp add: folds_def) |
|
1337 apply (rule someI2_ex) |
|
1338 apply (erule finite_imp_fold_graph) |
|
1339 apply (erule fold_graph.induct) |
|
1340 apply (auto) |
|
1341 done |
|
1342 |
|
1343 abbreviation |
|
1344 str_eq ("_ \<approx>_ _") |
|
1345 where |
|
1346 "x \<approx>Lang y \<equiv> (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)" |
|
1347 |
|
1348 abbreviation |
|
1349 lang_eq ("\<approx>_") |
|
1350 where |
|
1351 "\<approx>Lang \<equiv> (\<lambda>(x, y). x \<approx>Lang y)" |
|
1352 |
|
1353 lemma lang_eq_is_equiv: |
|
1354 "equiv UNIV (\<approx>Lang)" |
|
1355 unfolding equiv_def |
1325 unfolding equiv_def |
1356 unfolding refl_on_def sym_def trans_def |
1326 unfolding refl_on_def sym_def trans_def |
1357 by (simp add: mem_def equiv_str_def) |
1327 apply(auto simp add: mem_def equiv_str_def) |
1358 |
1328 done |
1359 text {* |
|
1360 equivalence classes of x can be written |
|
1361 |
|
1362 UNIV // (\<approx>Lang)``{x} |
|
1363 |
|
1364 the language quotient can be written |
|
1365 |
|
1366 UNIV // (\<approx>Lang) |
|
1367 *} |
|
1368 |
1329 |
1369 lemma |
1330 lemma |
1370 "(\<approx>Lang)``{x} = \<lbrakk>x\<rbrakk>Lang" |
1331 "(MNRel Lang)``{x} = \<lbrakk>x\<rbrakk>Lang" |
1371 unfolding equiv_class_def equiv_str_def Image_def mem_def |
1332 unfolding equiv_class_def Image_def mem_def |
1372 by (simp) |
1333 by (simp) |
1373 |
1334 |
|
1335 lemma tt: "\<lbrakk>A = B; C \<subseteq> B\<rbrakk> \<Longrightarrow> C \<subseteq> A" by simp |
|
1336 |
1374 lemma |
1337 lemma |
1375 "UNIV // (\<approx>Lang) = UNIV Quo Lang" |
1338 "UNIV//(MNRel (L1 \<union> L2)) \<subseteq> (UNIV//(MNRel L1)) \<union> (UNIV//(MNRel L2))" |
1376 unfolding quotient_def quot_def |
1339 unfolding quotient_def |
1377 unfolding equiv_class_def equiv_str_def |
1340 unfolding UNION_eq_Union_image |
1378 unfolding Image_def mem_def |
1341 apply(rule tt) |
1379 by auto |
1342 apply(rule Un_Union_image[symmetric]) |
1380 |
1343 apply(simp) |
1381 lemma |
1344 apply(rule UN_mono) |
1382 "{} \<notin> UNIV // (\<approx>Lang)" |
1345 apply(simp) |
1383 unfolding quotient_def |
1346 apply(simp) |
1384 unfolding Image_def |
1347 unfolding Image_def |
1385 apply(auto) |
|
1386 apply(rule_tac x="x" in exI) |
|
1387 unfolding mem_def |
1348 unfolding mem_def |
|
1349 unfolding MNRel.simps |
1388 apply(simp) |
1350 apply(simp) |
1389 done |
|
1390 |
|
1391 definition |
|
1392 transitions :: "string set \<Rightarrow> string set \<Rightarrow> rexp set" ("_\<Turnstile>\<Rightarrow>_") |
|
1393 where |
|
1394 "Y \<Turnstile>\<Rightarrow> X \<equiv> {CHAR c | c. Y ; {[c]} \<subseteq> X}" |
|
1395 |
|
1396 definition |
|
1397 transitions_rexp ("_ \<turnstile>\<rightarrow> _") |
|
1398 where |
|
1399 "Y \<turnstile>\<rightarrow> X \<equiv> if [] \<in> X then folds ALT EMPTY (Y \<Turnstile>\<Rightarrow>X) else folds ALT NULL (Y \<Turnstile>\<Rightarrow>X)" |
|
1400 |
|
1401 definition |
|
1402 "rhs CS X \<equiv> { (Y, Y \<turnstile>\<rightarrow>X) | Y. Y \<in> CS }" |
|
1403 |
|
1404 definition |
|
1405 "rhs_sem CS X \<equiv> { (Y; L (Y \<turnstile>\<rightarrow> X)) | Y. Y \<in> CS }" |
|
1406 |
|
1407 definition |
|
1408 "eqs CS \<equiv> (\<Union>X \<in> CS. {(X, rhs CS X)})" |
|
1409 |
|
1410 definition |
|
1411 "eqs_sem CS \<equiv> (\<Union>X \<in> CS. {(X, rhs_sem CS X)})" |
|
1412 |
|
1413 (* |
|
1414 lemma |
|
1415 assumes X_in_equas: "(X, rhss) \<in> (eqs_sem (UNIV // (\<approx>Lang)))" |
|
1416 shows "X = \<Union>rhss" |
|
1417 using assms |
|
1418 proof (cases "X = {[]}") |
|
1419 case True |
|
1420 thus ?thesis using X_in_equas |
|
1421 by (simp add:equations_def equation_rhs_def lang_seq_def) |
|
1422 next |
|
1423 case False |
|
1424 show ?thesis |
|
1425 proof |
|
1426 show "X \<subseteq> L xrhs" |
|
1427 proof |
|
1428 fix x |
|
1429 assume "(1)": "x \<in> X" |
|
1430 show "x \<in> L xrhs" |
|
1431 proof (cases "x = []") |
|
1432 assume empty: "x = []" |
|
1433 hence "x \<in> L (empty_rhs X)" using "(1)" |
|
1434 by (auto simp:empty_rhs_def lang_seq_def) |
|
1435 thus ?thesis using X_in_equas False empty "(1)" |
|
1436 unfolding equations_def equation_rhs_def by auto |
|
1437 next |
|
1438 assume not_empty: "x \<noteq> []" |
|
1439 hence "\<exists> clist c. x = clist @ [c]" by (case_tac x rule:rev_cases, auto) |
|
1440 then obtain clist c where decom: "x = clist @ [c]" by blast |
|
1441 moreover have "\<And> Y. \<lbrakk>Y \<in> UNIV Quo Lang; Y-c\<rightarrow>X; clist \<in> Y\<rbrakk> |
|
1442 \<Longrightarrow> [c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})" |
|
1443 proof - |
|
1444 fix Y |
|
1445 assume Y_is_eq_cl: "Y \<in> UNIV Quo Lang" |
|
1446 and Y_CT_X: "Y-c\<rightarrow>X" |
|
1447 and clist_in_Y: "clist \<in> Y" |
|
1448 with finite_charset_rS |
|
1449 show "[c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})" |
|
1450 by (auto simp :fold_alt_null_eqs) |
|
1451 qed |
|
1452 hence "\<exists>Xa. Xa \<in> UNIV Quo Lang \<and> clist @ [c] \<in> Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})" |
|
1453 using X_in_equas False not_empty "(1)" decom |
|
1454 by (auto dest!:every_eqclass_has_ascendent simp:equations_def equation_rhs_def lang_seq_def) |
|
1455 then obtain Xa where |
|
1456 "Xa \<in> UNIV Quo Lang \<and> clist @ [c] \<in> Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})" by blast |
|
1457 hence "x \<in> L {(S, folds ALT NULL {CHAR c |c. S-c\<rightarrow>X}) |S. S \<in> UNIV Quo Lang}" |
|
1458 using X_in_equas "(1)" decom |
|
1459 by (auto simp add:equations_def equation_rhs_def intro!:exI[where x = Xa]) |
|
1460 thus "x \<in> L xrhs" using X_in_equas False not_empty unfolding equations_def equation_rhs_def |
|
1461 by auto |
|
1462 qed |
|
1463 qed |
|
1464 next |
|
1465 *) |
|
1466 |
|
1467 lemma finite_rhs: |
|
1468 assumes fin: "finite CS" |
|
1469 shows "finite (rhs CS X)" |
|
1470 using fin unfolding rhs_def by (auto) |
|
1471 |
|
1472 lemma finite_eqs: |
|
1473 assumes fin: "finite CS" |
|
1474 shows "finite (eqs CS)" |
|
1475 unfolding eqs_def |
|
1476 apply(rule finite_UN_I) |
|
1477 apply(rule fin) |
|
1478 apply(simp add: eq_def) |
|
1479 done |
|
1480 |
|
1481 lemma |
|
1482 shows "X ; L (folds ALT NULL (X \<Turnstile>\<Rightarrow> Y)) \<subseteq> Y" |
|
1483 by (auto simp add: transitions_def lang_seq_def) |
|
1484 |
|
1485 lemma |
|
1486 shows "X ; L (X \<turnstile>\<rightarrow> Y) \<subseteq> Y" |
|
1487 apply (auto simp add: transitions_rexp_def transitions_def lang_seq_def) |
|
1488 oops |
|
1489 |
|
1490 lemma |
|
1491 "equation_rhs CS X = rhs CS X" |
|
1492 apply(simp only: rhs_def empty_rhs_def CT_def transitions_rexp_def transitions_def equation_rhs_def) |
|
1493 oops |
|
1494 |
|
1495 |
|
1496 |
|
1497 lemma |
|
1498 shows "X ; L (X \<turnstile>\<rightarrow> Y) \<subseteq> Y" |
|
1499 apply (auto simp add: transitions_rexp_def transitions_def lang_seq_def) |
|
1500 oops |
|
1501 |
|
1502 lemma |
|
1503 assumes a: "X \<in> (UNIV // (\<approx>Lang))" |
|
1504 shows "X \<subseteq> \<Union> (rhs_sem (UNIV // (\<approx>Lang)) X)" |
|
1505 unfolding rhs_sem_def |
|
1506 apply (auto simp add: transitions_def lang_seq_def fold_alt_null_eqs) |
|
1507 apply(rule_tac x="X" in exI) |
|
1508 apply(simp) |
|
1509 apply(simp add: quotient_def Image_def) |
|
1510 apply(subst (4) mem_def) |
|
1511 oops |
|
1512 |
|
1513 |
|
1514 lemma UNIV_eq_complement: |
|
1515 "UNIV // (\<approx>Lang) = UNIV // (\<approx>(- Lang))" |
|
1516 by auto |
|
1517 |
|
1518 lemma eq_inter: |
|
1519 fixes x y::"string" |
|
1520 shows "\<lbrakk>x \<approx>L1 y; x \<approx>L2 y\<rbrakk> \<Longrightarrow> (x \<approx>(L1 \<inter> L2) y)" |
|
1521 by auto |
|
1522 |
|
1523 lemma equ_union: |
|
1524 fixes x y::"string" |
|
1525 shows "\<lbrakk>x \<approx>L1 y; x \<approx>L2 y\<rbrakk> \<Longrightarrow> (x \<approx>(L1 \<union> L2) y)" |
|
1526 by auto |
|
1527 |
|
1528 (* HERE *) |
|
1529 |
|
1530 lemma tt: |
|
1531 "R1 \<subseteq> R2 \<Longrightarrow> R1 `` {x} \<subseteq> R2 `` {x}" |
|
1532 unfolding Image_def |
|
1533 by auto |
|
1534 |
|
1535 lemma tt_aux: |
|
1536 "(\<approx>Lang) `` {x} = \<lbrakk>x\<rbrakk>Lang" |
|
1537 unfolding Image_def |
|
1538 unfolding equiv_class_def |
|
1539 unfolding equiv_str_def |
|
1540 unfolding mem_def |
|
1541 apply(simp) |
|
1542 done |
|
1543 |
|
1544 lemma tt_old: |
|
1545 "(\<approx>L1) \<subseteq> (\<approx>L2) \<Longrightarrow> \<lbrakk>x\<rbrakk>L1 \<subseteq> \<lbrakk>x\<rbrakk>L2" |
|
1546 unfolding tt_aux[symmetric] |
|
1547 apply(simp add: tt) |
|
1548 done |
|
1549 |
|
1550 |
|
1551 |
|
1552 |
|
1553 lemma |
|
1554 assumes a: "finite (A // R1)" "R1 \<subseteq> R2" |
|
1555 shows "card (A // R2) <= card (A // R1)" |
|
1556 using assms |
|
1557 apply(induct ) |
|
1558 unfolding quotient_def |
|
1559 apply(drule_tac tt) |
|
1560 sorry |
|
1561 |
|
1562 lemma other_direction_cu: |
|
1563 fixes r::"rexp" |
|
1564 shows "finite (UNIV // (\<approx>(L r)))" |
|
1565 apply(induct r) |
|
1566 apply(simp_all) |
|
1567 oops |
1351 oops |
1568 |
1352 |
1569 |
1353 |
1570 |
1354 |
1571 text {* Alternative definition for Quo *} |
1355 text {* Alternative definition for Quo *} |
1572 definition |
1356 definition |
1573 QUOT :: "string set \<Rightarrow> (string set) set" |
1357 QUOT :: "string set \<Rightarrow> (string set) set" |
1574 where |
1358 where |
1575 "QUOT Lang \<equiv> (\<Union>x. {\<lbrakk>x\<rbrakk>Lang})" |
1359 "QUOT Lang \<equiv> (\<Union>x. {\<lbrakk>x\<rbrakk>Lang})" |
1576 |
|
1577 |
1360 |
1578 lemma test_01: |
1361 lemma test_01: |
1579 "Lang \<subseteq> (\<Union> QUOT Lang)" |
1362 "Lang \<subseteq> (\<Union> QUOT Lang)" |
1580 unfolding QUOT_def equiv_class_def equiv_str_def |
1363 unfolding QUOT_def equiv_class_def equiv_str_def |
1581 by (blast) |
1364 by (blast) |
1582 |
1365 |
1583 text{* by chunhan *} |
1366 |
|
1367 (* by chunhan *) |
1584 lemma quot_lambda: "QUOT {[]} = {{[]}, UNIV - {[]}}" |
1368 lemma quot_lambda: "QUOT {[]} = {{[]}, UNIV - {[]}}" |
1585 proof |
1369 proof |
1586 show "QUOT {[]} \<subseteq> {{[]}, UNIV - {[]}}" |
1370 show "QUOT {[]} \<subseteq> {{[]}, UNIV - {[]}}" |
1587 proof |
1371 proof |
1588 fix x |
1372 fix x |
1757 "UNIV Quo Lang = QUOT Lang" |
1541 "UNIV Quo Lang = QUOT Lang" |
1758 by (auto simp add: quot_def QUOT_def) |
1542 by (auto simp add: quot_def QUOT_def) |
1759 |
1543 |
1760 |
1544 |
1761 |
1545 |
|
1546 |
|
1547 (* by chunhan *) |
|
1548 |
|
1549 |
|
1550 lemma finite_tag_image: |
|
1551 "finite (range tag) \<Longrightarrow> finite (((op `) tag) ` S)" |
|
1552 apply (rule_tac B = "Pow (tag ` UNIV)" in finite_subset) |
|
1553 by (auto simp add:image_def Pow_def) |
|
1554 |
|
1555 lemma str_inj_imps: |
|
1556 assumes str_inj: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<equiv>lang\<equiv> n" |
|
1557 shows "inj_on ((op `) tag) (QUOT lang)" |
|
1558 proof (clarsimp simp add:inj_on_def QUOT_def) |
|
1559 fix x y |
|
1560 assume eq_tag: "tag ` \<lbrakk>x\<rbrakk>lang = tag ` \<lbrakk>y\<rbrakk>lang" |
|
1561 show "\<lbrakk>x\<rbrakk>lang = \<lbrakk>y\<rbrakk>lang" |
|
1562 proof - |
|
1563 have aux1:"\<And>a b. a \<in> (\<lbrakk>b\<rbrakk>lang) \<Longrightarrow> (a \<equiv>lang\<equiv> b)" |
|
1564 by (simp add:equiv_class_def equiv_str_def) |
|
1565 have aux2: "\<And> A B f. \<lbrakk>f ` A = f ` B; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists> a b. a \<in> A \<and> b \<in> B \<and> f a = f b" |
|
1566 by auto |
|
1567 have aux3: "\<And> a l. \<lbrakk>a\<rbrakk>l \<noteq> {}" |
|
1568 by (auto simp:equiv_class_def equiv_str_def) |
|
1569 show ?thesis using eq_tag |
|
1570 apply (drule_tac aux2, simp add:aux3, clarsimp) |
|
1571 apply (drule_tac str_inj, (drule_tac aux1)+) |
|
1572 by (simp add:equiv_str_def equiv_class_def) |
|
1573 qed |
|
1574 qed |
|
1575 |
|
1576 definition tag_str_ALT :: "string set \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> (string set \<times> string set)" |
|
1577 where |
|
1578 "tag_str_ALT L\<^isub>1 L\<^isub>2 x \<equiv> (\<lbrakk>x\<rbrakk>L\<^isub>1, \<lbrakk>x\<rbrakk>L\<^isub>2)" |
|
1579 |
|
1580 lemma tag_str_alt_range_finite: |
|
1581 assumes finite1: "finite (QUOT L\<^isub>1)" |
|
1582 and finite2: "finite (QUOT L\<^isub>2)" |
|
1583 shows "finite (range (tag_str_ALT L\<^isub>1 L\<^isub>2))" |
|
1584 proof - |
|
1585 have "{y. \<exists>x. y = (\<lbrakk>x\<rbrakk>L\<^isub>1, \<lbrakk>x\<rbrakk>L\<^isub>2)} \<subseteq> (QUOT L\<^isub>1) \<times> (QUOT L\<^isub>2)" |
|
1586 by (auto simp:QUOT_def) |
|
1587 thus ?thesis using finite1 finite2 |
|
1588 by (auto simp: image_def tag_str_ALT_def UNION_def |
|
1589 intro: finite_subset[where B = "(QUOT L\<^isub>1) \<times> (QUOT L\<^isub>2)"]) |
|
1590 qed |
|
1591 |
|
1592 lemma tag_str_alt_inj: |
|
1593 "tag_str_ALT L\<^isub>1 L\<^isub>2 x = tag_str_ALT L\<^isub>1 L\<^isub>2 y \<Longrightarrow> x \<equiv>(L\<^isub>1 \<union> L\<^isub>2)\<equiv> y" |
|
1594 apply (simp add:tag_str_ALT_def equiv_class_def equiv_str_def) |
|
1595 by blast |
|
1596 |
|
1597 lemma quot_alt: |
|
1598 assumes finite1: "finite (QUOT L\<^isub>1)" |
|
1599 and finite2: "finite (QUOT L\<^isub>2)" |
|
1600 shows "finite (QUOT (L\<^isub>1 \<union> L\<^isub>2))" |
|
1601 proof (rule_tac f = "(op `) (tag_str_ALT L\<^isub>1 L\<^isub>2)" in finite_imageD) |
|
1602 show "finite (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2) ` QUOT (L\<^isub>1 \<union> L\<^isub>2))" |
|
1603 using finite_tag_image tag_str_alt_range_finite finite1 finite2 |
|
1604 by auto |
|
1605 next |
|
1606 show "inj_on (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2)) (QUOT (L\<^isub>1 \<union> L\<^isub>2))" |
|
1607 apply (rule_tac str_inj_imps) |
|
1608 by (erule_tac tag_str_alt_inj) |
|
1609 qed |
|
1610 |
|
1611 (* list_diff:: list substract, once different return tailer *) |
|
1612 fun list_diff :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "-" 51) |
|
1613 where |
|
1614 "list_diff [] xs = []" | |
|
1615 "list_diff (x#xs) [] = x#xs" | |
|
1616 "list_diff (x#xs) (y#ys) = (if x = y then list_diff xs ys else (x#xs))" |
|
1617 |
|
1618 definition tag_str_SEQ:: "string set \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> (string set) set" |
|
1619 where |
|
1620 "tag_str_SEQ L\<^isub>1 L\<^isub>2 x \<equiv> if (\<exists> y. y \<le> x \<and> y \<in> L\<^isub>1) |
|
1621 then {(\<lbrakk>(x - y)\<rbrakk>L\<^isub>2) | y. y \<le> x \<and> y \<in> L\<^isub>1} |
|
1622 else { \<lbrakk>x\<rbrakk>L\<^isub>1 }" |
|
1623 |
|
1624 lemma tag_str_seq_range_finite: |
|
1625 assumes finite1: "finite (QUOT L\<^isub>1)" |
|
1626 and finite2: "finite (QUOT L\<^isub>2)" |
|
1627 shows "finite (range (tag_str_SEQ L\<^isub>1 L\<^isub>2))" |
|
1628 proof - |
|
1629 have "(range (tag_str_SEQ L\<^isub>1 L\<^isub>2)) \<subseteq> Pow ((QUOT L\<^isub>1) \<union> (QUOT L\<^isub>2))" |
|
1630 by (auto simp:image_def tag_str_SEQ_def QUOT_def) |
|
1631 thus ?thesis using finite1 finite2 |
|
1632 by (rule_tac B = "Pow ((QUOT L\<^isub>1) \<union> (QUOT L\<^isub>2))" in finite_subset, auto) |
|
1633 qed |
|
1634 |
|
1635 lemma tag_str_seq_inj: |
|
1636 assumes tag_eq: "tag_str_SEQ L\<^isub>1 L\<^isub>2 x = tag_str_SEQ L\<^isub>1 L\<^isub>2 y" |
|
1637 shows "(x::string) \<equiv>(L\<^isub>1 ; L\<^isub>2)\<equiv> y" |
|
1638 proof (cases "\<exists> xa. xa \<le> x \<and> xa \<in> L\<^isub>1") |
|
1639 have equiv_str_sym: "\<And> x y lang. (x::string) \<equiv>lang\<equiv> y \<Longrightarrow> y \<equiv>lang\<equiv> x" |
|
1640 by (auto simp:equiv_str_def) |
|
1641 have set_equ_D: "\<And> A a B b. \<lbrakk>A = B; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists> a b. a \<in> A \<and> b \<in> B \<and> a = b " by auto |
|
1642 have eqset_equ_D: "\<And> x y lang. {y. x \<equiv>lang\<equiv> y} = {ya. y \<equiv>lang\<equiv> ya} \<Longrightarrow> x \<equiv>lang\<equiv> y" |
|
1643 by (drule set_equ_D, auto simp:equiv_str_def) |
|
1644 assume x_left_l1: "\<exists>xa\<le>x. xa \<in> L\<^isub>1" |
|
1645 show "x \<equiv>L\<^isub>1 ; L\<^isub>2\<equiv> y" |
|
1646 proof (cases "\<exists> ya. ya \<le> y \<and> ya \<in> L\<^isub>1") |
|
1647 assume y_left_l1: "\<exists>ya\<le>y. ya \<in> L\<^isub>1" |
|
1648 with tag_eq x_left_l1 |
|
1649 show "x \<equiv>L\<^isub>1 ; L\<^isub>2\<equiv> y" |
|
1650 apply (simp add:tag_str_SEQ_def) |
|
1651 apply (drule set_equ_D) |
|
1652 apply (auto simp:equiv_class_def equiv_str_def)[1] |
|
1653 apply (clarsimp simp:equiv_str_def) |
|
1654 apply (rule iffI) |
|
1655 apply |
|
1656 apply ( |
|
1657 next |
|
1658 assume y_in_l1: "\<not> (\<exists>ya\<le>y. ya \<in> L\<^isub>1)" |
|
1659 show "x \<equiv>L\<^isub>1 ; L\<^isub>2\<equiv> y" |
|
1660 sorry |
|
1661 qed |
|
1662 next |
|
1663 assume x_in_l1: "\<not> (\<exists>xa\<le>x. xa \<in> L\<^isub>1)" |
|
1664 show "x \<equiv>L\<^isub>1 ; L\<^isub>2\<equiv> y" |
|
1665 proof (cases "\<exists> ya. ya \<le> y \<and> ya \<in> L\<^isub>1") |
|
1666 assume y_left_l1: "\<exists>ya\<le>y. ya \<in> L\<^isub>1" |
|
1667 show "x \<equiv>L\<^isub>1 ; L\<^isub>2\<equiv> y" |
|
1668 sorry |
|
1669 next |
|
1670 assume y_in_l1: "\<not> (\<exists>ya\<le>y. ya \<in> L\<^isub>1)" |
|
1671 with tag_eq x_in_l1 |
|
1672 have "\<lbrakk>x\<rbrakk>(L\<^isub>1;L\<^isub>2) = \<lbrakk>y\<rbrakk>(L\<^isub>1;L\<^isub>2)" |
|
1673 sorry |
|
1674 thus "x \<equiv>L\<^isub>1 ; L\<^isub>2\<equiv> y" |
|
1675 by (auto simp:equiv_class_def equiv_str_def) |
|
1676 qed |
|
1677 qed |
|
1678 |
|
1679 apply (simp add:tag_str_SEQ_def split:if_splits) |
|
1680 prefer 4 |
|
1681 apply (clarsimp simp add:equiv_str_def) |
|
1682 apply (rule iffI) |
|
1683 apply (simp add:lang_seq_def equiv_class_def equiv_str_def) |
|
1684 apply blast |
|
1685 apply ( |
|
1686 sorry |
|
1687 |
|
1688 |
|
1689 lemma quot_seq: |
|
1690 assumes finite1: "finite (QUOT L\<^isub>1)" |
|
1691 and finite2: "finite (QUOT L\<^isub>2)" |
|
1692 shows "finite (QUOT (L\<^isub>1;L\<^isub>2))" |
|
1693 proof (rule_tac f = "(op `) (tag_str_SEQ L\<^isub>1 L\<^isub>2)" in finite_imageD) |
|
1694 show "finite (op ` (tag_str_SEQ L\<^isub>1 L\<^isub>2) ` QUOT (L\<^isub>1 ; L\<^isub>2))" |
|
1695 using finite_tag_image tag_str_seq_range_finite finite1 finite2 |
|
1696 by auto |
|
1697 next |
|
1698 show "inj_on (op ` (tag_str_SEQ L\<^isub>1 L\<^isub>2)) (QUOT (L\<^isub>1 ; L\<^isub>2))" |
|
1699 apply (rule_tac str_inj_imps) |
|
1700 by (erule_tac tag_str_seq_inj) |
|
1701 qed |
|
1702 |
|
1703 definition tag_str_STAR:: "string set \<Rightarrow> string \<Rightarrow> (string set) set" |
|
1704 where |
|
1705 "tag_str_STAR L\<^isub>1 x = {\<lbrakk>y\<rbrakk>L\<^isub>1 | y. y \<le> x}" |
|
1706 |
|
1707 lemma tag_str_star_range_finite: |
|
1708 assumes finite1: "finite (QUOT L\<^isub>1)" |
|
1709 shows "finite (range (tag_str_STAR L\<^isub>1))" |
|
1710 proof - |
|
1711 have "range (tag_str_STAR L\<^isub>1) \<subseteq> Pow (QUOT L\<^isub>1)" |
|
1712 by (auto simp:image_def tag_str_STAR_def QUOT_def) |
|
1713 thus ?thesis using finite1 |
|
1714 by (rule_tac B = "Pow (QUOT L\<^isub>1)" in finite_subset, auto) |
|
1715 qed |
|
1716 |
|
1717 lemma tag_str_star_inj: |
|
1718 "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 (y::string) \<Longrightarrow> x \<equiv>L\<^isub>1\<star>\<equiv> y" |
|
1719 proof - |
|
1720 have "\<forall> x lang. (x = []) = (tag_str_STAR lang x = {\<lbrakk>[]\<rbrakk>lang})" |
|
1721 proof (rule_tac allI, rule_tac allI, rule_tac iffI) |
|
1722 fix x lang |
|
1723 show "x = [] \<Longrightarrow> tag_str_STAR lang x = {\<lbrakk>[]\<rbrakk>lang}" |
|
1724 by (simp add:tag_str_STAR_def) |
|
1725 next |
|
1726 fix x lang |
|
1727 show "tag_str_STAR lang x = {\<lbrakk>[]\<rbrakk>lang} \<Longrightarrow> x = []" |
|
1728 apply (simp add:tag_str_STAR_def) |
|
1729 apply (drule equalityD1) |
|
1730 apply (case_tac x) |
|
1731 apply simp |
|
1732 thm in_mono |
|
1733 apply (drule_tac x = "\<lbrakk>[a]\<rbrakk>lang" in in_mono) |
|
1734 apply simp |
|
1735 apply auto |
|
1736 |
|
1737 apply (erule subsetCE) |
|
1738 |
|
1739 apply (case_tac y) |
|
1740 |
|
1741 sorry |
|
1742 next |
|
1743 qed |
|
1744 apply (simp add:tag_str_STAR_def equiv_class_def equiv_str_def) |
|
1745 apply (rule iffI) |
|
1746 |
|
1747 apply (auto simp:tag_str_STAR_def equiv_class_def equiv_str_def) |
|
1748 have "\<And> x y z xstr. xstr \<in> L\<^isub>1\<star> \<Longrightarrow> |
|
1749 xstr = x @ z \<and> tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y \<longrightarrow> y @ z \<in> L\<^isub>1\<star> " |
|
1750 proof (erule Star.induct) |
|
1751 fix x y z xstr |
|
1752 show "[] = x @ z \<and> tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y \<longrightarrow> y @ z \<in> L\<^isub>1\<star>" |
|
1753 apply (clarsimp simp add:tag_str_STAR_def equiv_str_def equiv_class_def) |
|
1754 apply (blast) |
|
1755 apply (simp add:tag_str_STAR_def equiv_class_def QUOT_def) |
|
1756 apply (simp add:equiv_str_def) |
|
1757 apply (rule allI, rule_tac iffI) |
|
1758 apply (erule_tac star.induct) |
|
1759 apply blast |
|
1760 |
|
1761 sorry |
|
1762 |
|
1763 |
|
1764 lemma quot_star: |
|
1765 assumes finite1: "finite (QUOT L\<^isub>1)" |
|
1766 shows "finite (QUOT (L\<^isub>1\<star>))" |
|
1767 proof (rule_tac f = "(op `) (tag_str_STAR L\<^isub>1)" in finite_imageD) |
|
1768 show "finite (op ` (tag_str_STAR L\<^isub>1) ` QUOT (L\<^isub>1\<star>))" |
|
1769 using finite_tag_image tag_str_star_range_finite finite1 |
|
1770 by auto |
|
1771 next |
|
1772 show "inj_on (op ` (tag_str_STAR L\<^isub>1)) (QUOT (L\<^isub>1\<star>))" |
|
1773 apply (rule_tac str_inj_imps) |
|
1774 by (erule_tac tag_str_star_inj) |
|
1775 qed |
|
1776 |
|
1777 lemma other_direction: |
|
1778 "Lang = L (r::rexp) \<Longrightarrow> finite (QUOT Lang)" |
|
1779 apply (induct arbitrary:Lang rule:rexp.induct) |
|
1780 apply (simp add:QUOT_def equiv_class_def equiv_str_def) |
|
1781 by (simp_all add:quot_lambda quot_single quot_seq quot_alt quot_star) |
|
1782 |
|
1783 |
|
1784 |
|
1785 |
1762 end |
1786 end |