752 assume "(1)": "x \<in> X" |
756 assume "(1)": "x \<in> X" |
753 show "x \<in> L xrhs" |
757 show "x \<in> L xrhs" |
754 proof (cases "x = []") |
758 proof (cases "x = []") |
755 assume empty: "x = []" |
759 assume empty: "x = []" |
756 hence "x \<in> L (empty_rhs X)" using "(1)" |
760 hence "x \<in> L (empty_rhs X)" using "(1)" |
757 by (auto simp:empty_rhs_def lang_seq_def) |
761 unfolding empty_rhs_def |
|
762 by (simp add: lang_seq_def) |
758 thus ?thesis using X_in_equas False empty "(1)" |
763 thus ?thesis using X_in_equas False empty "(1)" |
759 unfolding equations_def equation_rhs_def by auto |
764 unfolding equations_def equation_rhs_def by auto |
760 next |
765 next |
761 assume not_empty: "x \<noteq> []" |
766 assume not_empty: "x \<noteq> []" |
762 hence "\<exists> clist c. x = clist @ [c]" by (case_tac x rule:rev_cases, auto) |
767 then obtain clist c where decom: "x = clist @ [c]" |
763 then obtain clist c where decom: "x = clist @ [c]" by blast |
768 using rev_cases by blast |
764 moreover have "\<And> Y. \<lbrakk>Y \<in> UNIV Quo Lang; Y-c\<rightarrow>X; clist \<in> Y\<rbrakk> |
769 moreover have "\<And> Y. Y-c\<rightarrow>X \<Longrightarrow> [c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})" |
765 \<Longrightarrow> [c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})" |
|
766 proof - |
770 proof - |
767 fix Y |
771 fix Y |
768 assume Y_is_eq_cl: "Y \<in> UNIV Quo Lang" |
772 assume Y_CT_X: "Y-c\<rightarrow>X" |
769 and Y_CT_X: "Y-c\<rightarrow>X" |
|
770 and clist_in_Y: "clist \<in> Y" |
|
771 with finite_charset_rS |
773 with finite_charset_rS |
772 show "[c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})" |
774 show "[c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})" |
773 by (auto simp :fold_alt_null_eqs) |
775 by (auto simp: fold_alt_null_eqs) |
774 qed |
776 qed |
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})" |
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})" |
776 using X_in_equas False not_empty "(1)" decom |
778 using X_in_equas False not_empty "(1)" decom |
777 by (auto dest!:every_eqclass_has_ascendent simp:equations_def equation_rhs_def lang_seq_def) |
779 by (auto dest!: every_eqclass_has_ascendent simp: equations_def equation_rhs_def lang_seq_def) |
778 then obtain Xa where |
780 then obtain Xa where |
779 "Xa \<in> UNIV Quo Lang \<and> clist @ [c] \<in> Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})" by blast |
781 "Xa \<in> UNIV Quo Lang" "clist @ [c] \<in> Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})" by blast |
780 hence "x \<in> L {(S, folds ALT NULL {CHAR c |c. S-c\<rightarrow>X}) |S. S \<in> UNIV Quo Lang}" |
782 hence "x \<in> L {(S, folds ALT NULL {CHAR c |c. S-c\<rightarrow>X}) |S. S \<in> UNIV Quo Lang}" |
781 using X_in_equas "(1)" decom |
783 using X_in_equas "(1)" decom |
782 by (auto simp add:equations_def equation_rhs_def intro!:exI[where x = Xa]) |
784 by (auto simp add:equations_def equation_rhs_def intro!:exI[where x = Xa]) |
783 thus "x \<in> L xrhs" using X_in_equas False not_empty unfolding equations_def equation_rhs_def |
785 thus "x \<in> L xrhs" using X_in_equas False not_empty |
|
786 unfolding equations_def equation_rhs_def |
784 by auto |
787 by auto |
785 qed |
788 qed |
786 qed |
789 qed |
787 next |
790 next |
788 show "L xrhs \<subseteq> X" |
791 show "L xrhs \<subseteq> X" |
789 proof |
792 proof |
790 fix x |
793 fix x |
791 assume "(2)": "x \<in> L xrhs" |
794 assume "(2)": "x \<in> L xrhs" |
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" |
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" |
793 using finite_charset_rS |
796 using finite_charset_rS |
794 by (auto simp:CT_def lang_seq_def fold_alt_null_eqs) |
797 unfolding CT_def |
|
798 by (simp add: lang_seq_def fold_alt_null_eqs) (auto) |
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" |
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" |
796 by (simp add:empty_rhs_def split:if_splits) |
800 by (simp add: empty_rhs_def split: if_splits) |
797 show "x \<in> X" using X_in_equas False "(2)" |
801 show "x \<in> X" using X_in_equas False "(2)" |
798 by (auto intro:"(2_1)" "(2_2)" simp:equations_def equation_rhs_def lang_seq_def) |
802 unfolding equations_def |
|
803 unfolding equation_rhs_def |
|
804 by (auto intro:"(2_1)" "(2_2)" simp: lang_seq_def) |
799 qed |
805 qed |
800 qed |
806 qed |
801 qed |
807 qed |
802 |
808 |
803 |
809 |
1314 |
1320 |
1315 (* compatibility with stable Isabelle *) |
1321 (* compatibility with stable Isabelle *) |
1316 lemma temp_set_ext[no_atp]: "(\<And>x. (x:A) = (x:B)) \<Longrightarrow> (A = B)" |
1322 lemma temp_set_ext[no_atp]: "(\<And>x. (x:A) = (x:B)) \<Longrightarrow> (A = B)" |
1317 by(auto intro:set_eqI) |
1323 by(auto intro:set_eqI) |
1318 |
1324 |
|
1325 lemma folds_simp_null [simp]: |
|
1326 "finite rs \<Longrightarrow> x \<in> L (folds ALT NULL rs) = (\<exists>r \<in> rs. x \<in> L r)" |
|
1327 apply (simp add: folds_def) |
|
1328 apply (rule someI2_ex) |
|
1329 apply (erule finite_imp_fold_graph) |
|
1330 apply (erule fold_graph.induct) |
|
1331 apply (auto) |
|
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 |
1319 abbreviation |
1343 abbreviation |
1320 str_eq ("_ \<approx>_ _") |
1344 str_eq ("_ \<approx>_ _") |
1321 where |
1345 where |
1322 "x \<approx>Lang y \<equiv> (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)" |
1346 "x \<approx>Lang y \<equiv> (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)" |
1323 |
1347 |
1365 done |
1389 done |
1366 |
1390 |
1367 definition |
1391 definition |
1368 transitions :: "string set \<Rightarrow> string set \<Rightarrow> rexp set" ("_\<Turnstile>\<Rightarrow>_") |
1392 transitions :: "string set \<Rightarrow> string set \<Rightarrow> rexp set" ("_\<Turnstile>\<Rightarrow>_") |
1369 where |
1393 where |
1370 "X \<Turnstile>\<Rightarrow> Y \<equiv> {CHAR c | c. X ; {[c]} \<subseteq> Y}" |
1394 "Y \<Turnstile>\<Rightarrow> X \<equiv> {CHAR c | c. Y ; {[c]} \<subseteq> X}" |
1371 |
1395 |
1372 definition |
1396 definition |
1373 "rhs CS X \<equiv> { (Y, X \<Turnstile>\<Rightarrow>Y) | Y. Y \<in> CS }" |
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)" |
1374 |
1400 |
1375 definition |
1401 definition |
1376 "rhs_sem CS X \<equiv> { (Y; L (folds ALT NULL (X \<Turnstile>\<Rightarrow>Y))) | Y. Y \<in> CS }" |
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 }" |
1377 |
1406 |
1378 definition |
1407 definition |
1379 "eqs CS \<equiv> (\<Union>X \<in> CS. {(X, rhs CS X)})" |
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 *) |
1380 |
1466 |
1381 lemma finite_rhs: |
1467 lemma finite_rhs: |
1382 assumes fin: "finite CS" |
1468 assumes fin: "finite CS" |
1383 shows "finite (rhs CS X)" |
1469 shows "finite (rhs CS X)" |
1384 using fin unfolding rhs_def by (auto) |
1470 using fin unfolding rhs_def by (auto) |
1391 apply(rule fin) |
1477 apply(rule fin) |
1392 apply(simp add: eq_def) |
1478 apply(simp add: eq_def) |
1393 done |
1479 done |
1394 |
1480 |
1395 lemma |
1481 lemma |
1396 shows "X ; L (folds ALT NULL X \<Turnstile>\<Rightarrow> Y) \<subseteq> Y" |
1482 shows "X ; L (folds ALT NULL (X \<Turnstile>\<Rightarrow> Y)) \<subseteq> Y" |
1397 by (auto simp add: transitions_def lang_seq_def fold_alt_null_eqs) |
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 |
1398 |
1501 |
1399 lemma |
1502 lemma |
1400 assumes a: "X \<in> (UNIV // (\<approx>Lang))" |
1503 assumes a: "X \<in> (UNIV // (\<approx>Lang))" |
1401 shows "X \<subseteq> \<Union> (rhs_sem (UNIV // (\<approx>Lang)) X)" |
1504 shows "X \<subseteq> \<Union> (rhs_sem (UNIV // (\<approx>Lang)) X)" |
1402 unfolding rhs_sem_def |
1505 unfolding rhs_sem_def |
1403 apply (auto simp add: transitions_def lang_seq_def fold_alt_null_eqs) |
1506 apply (auto simp add: transitions_def lang_seq_def fold_alt_null_eqs) |
1404 apply(rule_tac x="X" in exI) |
1507 apply(rule_tac x="X" in exI) |
1405 apply(simp) |
1508 apply(simp) |
1406 apply(simp add: quotient_def Image_def) |
1509 apply(simp add: quotient_def Image_def) |
1407 apply(subst (4) mem_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 |
1408 apply(simp) |
1541 apply(simp) |
1409 using a |
1542 done |
1410 apply(simp add: quotient_def Image_def) |
1543 |
1411 apply(subst (asm) (2) mem_def) |
1544 lemma tt_old: |
1412 apply(simp) |
1545 "(\<approx>L1) \<subseteq> (\<approx>L2) \<Longrightarrow> \<lbrakk>x\<rbrakk>L1 \<subseteq> \<lbrakk>x\<rbrakk>L2" |
1413 apply(rule_tac x="X" in exI) |
1546 unfolding tt_aux[symmetric] |
1414 apply(simp) |
1547 apply(simp add: tt) |
1415 apply(erule exE) |
1548 done |
1416 apply(simp) |
1549 |
1417 apply(rule temp_set_ext) |
1550 |
1418 apply(simp) |
1551 |
1419 apply(rule iffI) |
|
1420 apply(rule_tac x="x" in exI) |
|
1421 apply(simp) |
|
1422 oops |
|
1423 |
|
1424 lemma tt: "\<lbrakk>A = B; C \<subseteq> B\<rbrakk> \<Longrightarrow> C \<subseteq> A" by simp |
|
1425 |
1552 |
1426 lemma |
1553 lemma |
1427 "UNIV//(\<approx>(L1 \<union> L2)) \<subseteq> (UNIV//(\<approx>L1)) \<union> (UNIV//(\<approx>L2))" |
1554 assumes a: "finite (A // R1)" "R1 \<subseteq> R2" |
1428 unfolding quotient_def Image_def |
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) |
1429 oops |
1567 oops |
1430 |
1568 |
1431 |
1569 |
1432 |
1570 |
1433 text {* Alternative definition for Quo *} |
1571 text {* Alternative definition for Quo *} |