1510 "\<lbrakk>x \<equiv>L1\<equiv> y \<and> x \<equiv>L2\<equiv> y\<rbrakk> \<Longrightarrow> x \<equiv>(L1 \<union> L2)\<equiv> y" |
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) |
1511 apply(simp add: equiv_str_def) |
1512 done |
1512 done |
1513 |
1513 |
1514 |
1514 |
1515 lemma QUOT_union: |
1515 (* |
1516 "(QUOT (L1 \<union> L2)) \<subseteq> ((QUOT L1) \<union> (QUOT L2))" |
|
1517 sorry |
|
1518 |
|
1519 |
|
1520 lemma quot_alt: |
|
1521 assumes finite1: "finite (QUOT L\<^isub>1)" |
|
1522 and finite2: "finite (QUOT L\<^isub>2)" |
|
1523 shows "finite (QUOT (L\<^isub>1 \<union> L\<^isub>2))" |
|
1524 apply(rule finite_subset) |
|
1525 apply(rule QUOT_union) |
|
1526 apply(simp add: finite1 finite2) |
|
1527 done |
|
1528 |
|
1529 lemma quot_star: |
1516 lemma quot_star: |
1530 assumes finite1: "finite (QUOT L\<^isub>1)" |
1517 assumes finite1: "finite (QUOT L\<^isub>1)" |
1531 shows "finite (QUOT (L\<^isub>1\<star>))" |
1518 shows "finite (QUOT (L\<^isub>1\<star>))" |
1532 sorry |
1519 sorry |
|
1520 |
1533 |
1521 |
1534 lemma other_direction: |
1522 lemma other_direction: |
1535 "Lang = L (r::rexp) \<Longrightarrow> finite (QUOT Lang)" |
1523 "Lang = L (r::rexp) \<Longrightarrow> finite (QUOT Lang)" |
1536 apply (induct arbitrary:Lang rule:rexp.induct) |
1524 apply (induct arbitrary:Lang rule:rexp.induct) |
1537 apply (simp add:QUOT_def equiv_class_def equiv_str_def) |
1525 apply (simp add:QUOT_def equiv_class_def equiv_str_def) |
1538 by (simp_all add:quot_lambda quot_single quot_seq quot_alt quot_star) |
1526 by (simp_all add:quot_lambda quot_single quot_seq quot_alt quot_star) |
1539 |
1527 |
1540 lemma test: |
1528 lemma test: |
1541 "UNIV Quo Lang = QUOT Lang" |
1529 "UNIV Quo Lang = QUOT Lang" |
1542 by (auto simp add: quot_def QUOT_def) |
1530 by (auto simp add: quot_def QUOT_def) |
1543 |
1531 *) |
1544 |
|
1545 |
1532 |
1546 |
1533 |
1547 (* by chunhan *) |
1534 (* by chunhan *) |
1548 |
1535 |
1549 |
1536 |
1550 lemma finite_tag_image: |
1537 lemma finite_tag_image: |
1551 "finite (range tag) \<Longrightarrow> finite (((op `) tag) ` S)" |
1538 "finite (range tag) \<Longrightarrow> finite (((op `) tag) ` S)" |
1552 apply (rule_tac B = "Pow (tag ` UNIV)" in finite_subset) |
1539 apply (rule_tac B = "Pow (tag ` UNIV)" in finite_subset) |
1553 by (auto simp add:image_def Pow_def) |
1540 by (auto simp add:image_def Pow_def) |
1554 |
1541 |
|
1542 term image |
|
1543 term "(op `) tag" |
|
1544 |
1555 lemma str_inj_imps: |
1545 lemma str_inj_imps: |
1556 assumes str_inj: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<equiv>lang\<equiv> n" |
1546 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)" |
1547 shows "inj_on (image tag) (QUOT lang)" |
1558 proof (clarsimp simp add:inj_on_def QUOT_def) |
1548 proof (clarsimp simp add:inj_on_def QUOT_def) |
1559 fix x y |
1549 fix x y |
1560 assume eq_tag: "tag ` \<lbrakk>x\<rbrakk>lang = tag ` \<lbrakk>y\<rbrakk>lang" |
1550 assume eq_tag: "tag ` \<lbrakk>x\<rbrakk>lang = tag ` \<lbrakk>y\<rbrakk>lang" |
1561 show "\<lbrakk>x\<rbrakk>lang = \<lbrakk>y\<rbrakk>lang" |
1551 show "\<lbrakk>x\<rbrakk>lang = \<lbrakk>y\<rbrakk>lang" |
1562 proof - |
1552 proof - |
1571 apply (drule_tac str_inj, (drule_tac aux1)+) |
1561 apply (drule_tac str_inj, (drule_tac aux1)+) |
1572 by (simp add:equiv_str_def equiv_class_def) |
1562 by (simp add:equiv_str_def equiv_class_def) |
1573 qed |
1563 qed |
1574 qed |
1564 qed |
1575 |
1565 |
1576 definition tag_str_ALT :: "string set \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> (string set \<times> string set)" |
1566 definition |
|
1567 tag_str_ALT :: "string set \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> (string set \<times> string set)" |
1577 where |
1568 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)" |
1569 "tag_str_ALT L\<^isub>1 L\<^isub>2 x \<equiv> (\<lbrakk>x\<rbrakk>L\<^isub>1, \<lbrakk>x\<rbrakk>L\<^isub>2)" |
|
1570 |
|
1571 lemma |
|
1572 "{(\<lbrakk>x\<rbrakk>L\<^isub>1, \<lbrakk>x\<rbrakk>L\<^isub>2) | x. True} \<subseteq> (QUOT L\<^isub>1) \<times> (QUOT L\<^isub>2)" |
|
1573 unfolding QUOT_def |
|
1574 by (auto) |
1579 |
1575 |
1580 lemma tag_str_alt_range_finite: |
1576 lemma tag_str_alt_range_finite: |
1581 assumes finite1: "finite (QUOT L\<^isub>1)" |
1577 assumes finite1: "finite (QUOT L\<^isub>1)" |
1582 and finite2: "finite (QUOT L\<^isub>2)" |
1578 and finite2: "finite (QUOT L\<^isub>2)" |
1583 shows "finite (range (tag_str_ALT L\<^isub>1 L\<^isub>2))" |
1579 shows "finite (range (tag_str_ALT L\<^isub>1 L\<^isub>2))" |
1584 proof - |
1580 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)" |
1581 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) |
1582 unfolding QUOT_def |
|
1583 by auto |
1587 thus ?thesis using finite1 finite2 |
1584 thus ?thesis using finite1 finite2 |
1588 by (auto simp: image_def tag_str_ALT_def UNION_def |
1585 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)"]) |
1586 intro: finite_subset[where B = "(QUOT L\<^isub>1) \<times> (QUOT L\<^isub>2)"]) |
1590 qed |
1587 qed |
1591 |
1588 |
1596 |
1593 |
1597 lemma quot_alt: |
1594 lemma quot_alt: |
1598 assumes finite1: "finite (QUOT L\<^isub>1)" |
1595 assumes finite1: "finite (QUOT L\<^isub>1)" |
1599 and finite2: "finite (QUOT L\<^isub>2)" |
1596 and finite2: "finite (QUOT L\<^isub>2)" |
1600 shows "finite (QUOT (L\<^isub>1 \<union> L\<^isub>2))" |
1597 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) |
1598 proof - |
1602 show "finite (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2) ` QUOT (L\<^isub>1 \<union> L\<^isub>2))" |
1599 have "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 |
1600 using finite_tag_image tag_str_alt_range_finite finite1 finite2 |
1604 by auto |
1601 by auto |
1605 next |
1602 moreover |
1606 show "inj_on (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2)) (QUOT (L\<^isub>1 \<union> L\<^isub>2))" |
1603 have "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) |
1604 apply (rule_tac str_inj_imps) |
1608 by (erule_tac tag_str_alt_inj) |
1605 by (erule_tac tag_str_alt_inj) |
1609 qed |
1606 ultimately |
|
1607 show "finite (QUOT (L\<^isub>1 \<union> L\<^isub>2))" by (rule finite_imageD) |
|
1608 qed |
|
1609 |
|
1610 |
|
1611 (*by cu *) |
|
1612 |
|
1613 |
|
1614 definition |
|
1615 str_eq ("_ \<approx>_ _") |
|
1616 where |
|
1617 "x \<approx>Lang y \<equiv> (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)" |
|
1618 |
|
1619 definition |
|
1620 str_eq_rel ("\<approx>_") |
|
1621 where |
|
1622 "\<approx>Lang \<equiv> {(x, y). x \<approx>Lang y}" |
|
1623 |
|
1624 lemma [simp]: |
|
1625 "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y" |
|
1626 by simp |
|
1627 |
|
1628 lemma inj_image_lang: |
|
1629 fixes f::"string \<Rightarrow> 'a" |
|
1630 assumes str_inj: "\<And>x y. f x = f y \<Longrightarrow> x \<approx>Lang y" |
|
1631 shows "inj_on (image f) (UNIV // (\<approx>Lang))" |
|
1632 proof - |
|
1633 { fix x y::string |
|
1634 assume eq_tag: "f ` {z. x \<approx>Lang z} = f ` {z. y \<approx>Lang z}" |
|
1635 moreover |
|
1636 have "{z. x \<approx>Lang z} \<noteq> {}" unfolding str_eq_def by auto |
|
1637 ultimately obtain a b where "x \<approx>Lang a" "y \<approx>Lang b" "f a = f b" by blast |
|
1638 then have "x \<approx>Lang a" "y \<approx>Lang b" "a \<approx>Lang b" using str_inj by auto |
|
1639 then have "x \<approx>Lang y" unfolding str_eq_def by simp |
|
1640 then have "{z. x \<approx>Lang z} = {z. y \<approx>Lang z}" unfolding str_eq_def by simp |
|
1641 } |
|
1642 then have "\<forall>x\<in>UNIV // \<approx>Lang. \<forall>y\<in>UNIV // \<approx>Lang. f ` x = f ` y \<longrightarrow> x = y" |
|
1643 unfolding quotient_def Image_def str_eq_rel_def by simp |
|
1644 then show "inj_on (image f) (UNIV // (\<approx>Lang))" |
|
1645 unfolding inj_on_def by simp |
|
1646 qed |
|
1647 |
|
1648 |
|
1649 lemma finite_range_image: |
|
1650 assumes fin: "finite (range f)" |
|
1651 shows "finite ((image f) ` X)" |
|
1652 proof - |
|
1653 from fin have "finite (Pow (f ` UNIV))" by auto |
|
1654 moreover |
|
1655 have "(image f) ` X \<subseteq> Pow (f ` UNIV)" by auto |
|
1656 ultimately show "finite ((image f) ` X)" using finite_subset by auto |
|
1657 qed |
|
1658 |
|
1659 definition |
|
1660 tag1 :: "string set \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> (string set \<times> string set)" |
|
1661 where |
|
1662 "tag1 L\<^isub>1 L\<^isub>2 \<equiv> \<lambda>x. ((\<approx>L\<^isub>1) `` {x}, (\<approx>L\<^isub>2) `` {x})" |
|
1663 |
|
1664 lemma tag1_range_finite: |
|
1665 assumes finite1: "finite (UNIV // \<approx>L\<^isub>1)" |
|
1666 and finite2: "finite (UNIV // \<approx>L\<^isub>2)" |
|
1667 shows "finite (range (tag1 L\<^isub>1 L\<^isub>2))" |
|
1668 proof - |
|
1669 have "finite (UNIV // \<approx>L\<^isub>1 \<times> UNIV // \<approx>L\<^isub>2)" using finite1 finite2 by auto |
|
1670 moreover |
|
1671 have "range (tag1 L\<^isub>1 L\<^isub>2) \<subseteq> (UNIV // \<approx>L\<^isub>1) \<times> (UNIV // \<approx>L\<^isub>2)" |
|
1672 unfolding tag1_def quotient_def by auto |
|
1673 ultimately show "finite (range (tag1 L\<^isub>1 L\<^isub>2))" |
|
1674 using finite_subset by blast |
|
1675 qed |
|
1676 |
|
1677 lemma tag1_inj: |
|
1678 "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" |
|
1679 unfolding tag1_def Image_def str_eq_rel_def str_eq_def |
|
1680 by auto |
|
1681 |
|
1682 lemma quot_alt_cu: |
|
1683 fixes L\<^isub>1 L\<^isub>2::"string set" |
|
1684 assumes fin1: "finite (UNIV // \<approx>L\<^isub>1)" |
|
1685 and fin2: "finite (UNIV // \<approx>L\<^isub>2)" |
|
1686 shows "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))" |
|
1687 proof - |
|
1688 have "finite (range (tag1 L\<^isub>1 L\<^isub>2))" |
|
1689 using fin1 fin2 tag1_range_finite by simp |
|
1690 then have "finite (image (tag1 L\<^isub>1 L\<^isub>2) ` (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2)))" |
|
1691 using finite_range_image by blast |
|
1692 moreover |
|
1693 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" |
|
1694 using tag1_inj by simp |
|
1695 then have "inj_on (image (tag1 L\<^isub>1 L\<^isub>2)) (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))" |
|
1696 using inj_image_lang by blast |
|
1697 ultimately |
|
1698 show "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))" by (rule finite_imageD) |
|
1699 qed |
|
1700 |
|
1701 (* by chunhan *) |
1610 |
1702 |
1611 (* list_diff:: list substract, once different return tailer *) |
1703 (* list_diff:: list substract, once different return tailer *) |
1612 fun list_diff :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "-" 51) |
1704 fun list_diff :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "-" 51) |
1613 where |
1705 where |
1614 "list_diff [] xs = []" | |
1706 "list_diff [] xs = []" | |