1483 can be dealt with as in Lemma~\ref{alphaeq}. |
1483 can be dealt with as in Lemma~\ref{alphaeq}. |
1484 \end{proof} |
1484 \end{proof} |
1485 |
1485 |
1486 \noindent |
1486 \noindent |
1487 We can feed this lemma into our quotient package and obtain new types @{text |
1487 We can feed this lemma into our quotient package and obtain new types @{text |
1488 "ty"}$^\alpha_{1..n}$ representing alpha-equated terms of types @{text |
1488 "ty"}$^\alpha_{1..n}$ representing alpha-equated terms. We also obtain |
1489 "ty"}$_{1..n}$. We also obtain definitions for the term-constructors @{text |
1489 definitions for the term-constructors @{text |
1490 "C"}$^\alpha_{1..m}$ from the raw term-constructors @{text |
1490 "C"}$^\alpha_{1..m}$ from the raw term-constructors @{text |
1491 "C"}$_{1..m}$. Similarly for the free-variable functions @{text |
1491 "C"}$_{1..m}$, and similar definitions for the free-variable functions @{text |
1492 "fv_ty"}$^\alpha_{1..n}$ and the binding functions @{text |
1492 "fv_ty"}$^\alpha_{1..n}$ and the binding functions @{text |
1493 "bn"}$^\alpha_{1..k}$. However, these definitions are of not much use for the |
1493 "bn"}$^\alpha_{1..k}$. However, these definitions are not really useful to the |
1494 user, since the are formulated in terms of the isomorphisms we obtained by |
1494 user, since the are given in terms of the isomorphisms we obtained by |
1495 creating new types in Isabelle/HOL (recall the picture shown in the |
1495 creating new types in Isabelle/HOL (recall the picture shown in the |
1496 Introduction). |
1496 Introduction). |
1497 |
1497 |
1498 The first useful property about term-constructors |
1498 The first useful property to the user is the fact that term-constructors are |
1499 is to know that they are distinct, that is |
1499 distinct, that is |
1500 % |
1500 % |
1501 \begin{equation}\label{distinctalpha} |
1501 \begin{equation}\label{distinctalpha} |
1502 \mbox{@{text "C"}$^\alpha_i$@{text "x\<^isub>1 \<dots> x\<^isub>n"} @{text "\<noteq>"} |
1502 \mbox{@{text "C"}$^\alpha_i$@{text "x\<^isub>1 \<dots> x\<^isub>n"} @{text "\<noteq>"} |
1503 @{text "C"}$^\alpha_j$@{text "y\<^isub>1 \<dots> y\<^isub>m"} holds for @{text "i \<noteq> j"}.} |
1503 @{text "C"}$^\alpha_j$@{text "y\<^isub>1 \<dots> y\<^isub>m"} holds for @{text "i \<noteq> j"}.} |
1504 \end{equation} |
1504 \end{equation} |
1506 \noindent |
1506 \noindent |
1507 By definition of alpha-equivalence we can show that |
1507 By definition of alpha-equivalence we can show that |
1508 for the raw term-constructors |
1508 for the raw term-constructors |
1509 % |
1509 % |
1510 \begin{equation}\label{distinctraw} |
1510 \begin{equation}\label{distinctraw} |
1511 @{text "C\<^isub>i x\<^isub>1 \<dots> x\<^isub>n"}\;\not\approx@{text ty}\;@{text "C\<^isub>j y\<^isub>1 \<dots> y\<^isub>m"} holds for @{text "i \<noteq> j"}. |
1511 \mbox{@{text "C\<^isub>i x\<^isub>1 \<dots> x\<^isub>n"}\;$\not\approx$@{text ty}\;@{text "C\<^isub>j y\<^isub>1 \<dots> y\<^isub>m"} holds for @{text "i \<noteq> j"}.} |
1512 \end{equation} |
1512 \end{equation} |
1513 |
1513 |
1514 \noindent |
1514 \noindent |
1515 In order to generate \eqref{distinctalpha} from this fact, the quotient |
1515 In order to generate \eqref{distinctalpha} from \eqref{distinctraw}, the quotient |
1516 package needs to know that the term-constructors @{text "C\<^isub>i"} and @{text "C\<^isub>j"} |
1516 package needs to know that the term-constructors @{text "C\<^isub>i"} and @{text "C\<^isub>j"} |
1517 are \emph{respectful} w.r.t.~the alpha-equivalence relations \cite{Homeier05}. |
1517 are \emph{respectful} w.r.t.~the alpha-equivalence relations (see \cite{Homeier05}). |
1518 This means, given @{text "C\<^isub>i"} is of type @{text "ty"} with argument types |
1518 Assuming @{text "C\<^isub>i"} is of type @{text "ty"} with argument types |
1519 @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, we have to show that |
1519 @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, then respectfulness amounts to showing |
1520 |
1520 |
1521 \begin{center} |
1521 \begin{center} |
1522 @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"} |
1522 @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"} |
1523 \end{center} |
1523 \end{center} |
1524 |
1524 |
1525 \noindent |
1525 \noindent |
1526 under the assumption that @{text "x\<^isub>i \<approx>ty\<^isub>i y\<^isub>i"} holds for all recursive arguments |
1526 are alpha-equivalent under the assumption that @{text "x\<^isub>i \<approx>ty\<^isub>i y\<^isub>i"} holds for all recursive arguments |
1527 and @{text "x\<^isub>i = y\<^isub>i"} for all non-recursive arguments. We can prove this by |
1527 and @{text "x\<^isub>i = y\<^isub>i"} holds for all non-recursive arguments. We can prove this by |
1528 analysing the definition of @{text "\<approx>ty"}. For this to succeed we have to establish an |
1528 analysing the definition of @{text "\<approx>ty"}. For this to succeed we have to establish |
1529 auxiliary fact: given a binding function @{text bn} defined for the type @{text ty} |
1529 the following auxiliary fact about binding functions. Given a binding function @{text bn\<^isub>i} defined |
1530 we have that |
1530 for the type @{text ty\<^isub>i}, we have that |
1531 |
1531 % |
1532 \begin{center} |
1532 \begin{center} |
1533 @{text "x \<approx>ty y"} implies @{text "x \<approx>bn y"} |
1533 @{text "x \<approx>ty\<^isub>i y"} implies @{text "x \<approx>bn\<^isub>i y"} |
1534 \end{center} |
1534 \end{center} |
1535 |
1535 |
1536 \noindent |
1536 \noindent |
1537 This can be established by induction on the definition of @{text "\<approx>ty"}. |
1537 This can be established by induction on the definition of @{text "\<approx>ty\<^isub>i"}. |
1538 |
1538 |
1539 Having established respectfulness for every raw term-constructor, the |
1539 Having established respectfulness for every raw term-constructor, the |
1540 quotient package will automatically deduce \eqref{distinctalpha} from \eqref{distinctraw}. |
1540 quotient package is able to automatically deduce \eqref{distinctalpha} from \eqref{distinctraw}. |
1541 In fact we can lift any fact from the raw level to the alpha-equated level that |
1541 In fact we can from now on lift any fact from the raw level to the alpha-equated level that |
1542 apart from variables only contains the raw term-constructors @{text "C\<^isub>i"}. The |
1542 apart from variables only contains the raw term-constructors. The |
1543 induction principles derived by the datatype package of Isabelle/HOL for @{text |
1543 induction principles derived by the datatype package in Isabelle/HOL for teh types @{text |
1544 "ty"}$^\alpha_{1..n}$ fall into this category. So we can also add to our infrastructure |
1544 "ty"}$^\alpha_{1..n}$ fall into this category. So we can also add to our infrastructure |
1545 induction principles that establish |
1545 induction principles that establish |
1546 |
1546 |
1547 \begin{center} |
1547 \begin{center} |
1548 @{text "P\<^bsub>ty\<^isub>1\<^esub> y\<^isub>1 \<dots> P\<^bsub>ty\<^isub>n\<^esub> y\<^isub>n "} |
1548 @{text "P\<^bsub>ty\<^isub>1\<^esub> y\<^isub>1 \<dots> P\<^bsub>ty\<^isub>n\<^esub> y\<^isub>n "} |
1549 \end{center} |
1549 \end{center} |
1550 |
1550 |
1551 \noindent |
1551 \noindent |
1552 for every @{text "y\<^isub>i"} under the assumption we specified the types |
1552 for all @{text "y\<^isub>i"} wherby the variables @{text "P\<^bsub>ty\<^isub>i\<^esub>"} stand for properties |
1553 @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}. The premises of these induction principles look |
1553 defined over the types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}. The premises of |
|
1554 these induction principles look |
1554 as follows |
1555 as follows |
1555 |
1556 |
1556 \begin{center} |
1557 \begin{center} |
1557 @{text "\<forall>x\<^isub>1\<dots>x\<^isub>n. P\<^bsub>ty\<^isub>i\<^esub> x\<^isub>i \<and> \<dots> \<and> P\<^bsub>ty\<^isub>j\<^esub> x\<^isub>j \<Rightarrow> P\<^bsub>ty\<^esub> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"} |
1558 @{text "\<forall>x\<^isub>1\<dots>x\<^isub>n. P\<^bsub>ty\<^isub>i\<^esub> x\<^isub>i \<and> \<dots> \<and> P\<^bsub>ty\<^isub>j\<^esub> x\<^isub>j \<Rightarrow> P\<^bsub>ty\<^esub> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"} |
1558 \end{center} |
1559 \end{center} |
1559 |
1560 |
1560 \noindent |
1561 \noindent |
1561 where the @{text "x\<^isub>i, \<dots>, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\<alpha>"}. |
1562 where the @{text "x\<^isub>i, \<dots>, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\<alpha>"}. |
1562 Next we lift the permutation operations defined in \eqref{ceqvt} for |
1563 Next we lift the permutation operations defined in \eqref{ceqvt} for |
1563 the raw term-constructors @{text "C"}. These facts contain, in addition |
1564 the raw term-constructors @{text "C"}. These facts contain, in addition |
1564 to the term-constructors, also permutations operations. Therefore |
1565 to the term-constructors, also permutations operations. In order to make the |
1565 we have to know that permutation operations are respectful |
1566 lifting to go through, |
1566 w.r.t.~alpha-equivalence, which amounts to knowing that the |
1567 we have to know that the permutation operations are respectful |
1567 alpha-equivalence relations are equivariant, which we established |
1568 w.r.t.~alpha-equivalence. This amounts to showing that the |
|
1569 alpha-equivalence relations are equivariant, which we already established |
1568 in Lemma~\ref{equiv}. As a result we can add the equations |
1570 in Lemma~\ref{equiv}. As a result we can add the equations |
1569 |
1571 |
1570 \begin{equation}\label{ceqvt} |
1572 \begin{equation}\label{ceqvt} |
1571 @{text "p \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n) = C\<^sup>\<alpha> (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"} |
1573 @{text "p \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n) = C\<^sup>\<alpha> (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"} |
1572 \end{equation} |
1574 \end{equation} |
1573 |
1575 |
1574 \noindent |
1576 \noindent |
1575 to our infrastructure. In a similar fashion we can lift the equations |
1577 to our infrastructure. In a similar fashion we can lift the equations |
1576 characterising our free-variable functions and the binding functions. |
1578 characterising the free-variable functions @{text "fn_ty\<AL>\<^isub>j"} and the |
1577 The necessary respectfulness lemmas are |
1579 binding functions @{text "bn\<AL>\<^isub>k"}. The necessary respectfulness lemmas for this |
|
1580 lifting are the two properties: |
1578 % |
1581 % |
1579 \begin{equation}\label{fnresp} |
1582 \begin{equation}\label{fnresp} |
1580 \mbox{% |
1583 \mbox{% |
1581 \begin{tabular}{l} |
1584 \begin{tabular}{l} |
1582 @{text "x \<approx>ty y"} implies @{text "fv_ty x = fv_ty y"}\\ |
1585 @{text "x \<approx>ty\<^isub>j y"} implies @{text "fv_ty\<^isub>j x = fv_ty\<^isub>j y"}\\ |
1583 @{text "x \<approx>ty y"} implies @{text "bn x = bn y"} |
1586 @{text "x \<approx>ty\<^isub>j y"} implies @{text "bn\<^isub>k x = bn\<^isub>k y"} |
1584 \end{tabular}} |
1587 \end{tabular}} |
1585 \end{equation} |
1588 \end{equation} |
1586 |
1589 |
1587 \noindent |
1590 \noindent |
1588 which can be established by induction on @{text "\<approx>ty"}. While the first |
1591 which can be established by induction on @{text "\<approx>ty"}. Whereas the first |
1589 kind of lemma is always ensured by way of how we defined the free variable |
1592 property is always true by the way how we defined the free-variable |
1590 functions, the second does not hold in general. It only if the @{text bn}-functions |
1593 functions, the second does \emph{not} hold in general. There is, in principle, |
1591 do not return any atom that is also bound. Hence our restriction imposed |
1594 the possibility that the user defines @{text "bn\<^isub>k"} so that it returns an already bound |
1592 on the binding functions that excludes this possibility. |
1595 variable. Then the second property is just not true. However, our |
1593 |
1596 restrictions imposed on the binding functions |
1594 Having the facts \eqref{fnresp} at our disposal, we can finally lift the |
1597 exclude this possibility. |
|
1598 |
|
1599 Having the facts \eqref{fnresp} at our disposal, we can lift the |
1595 definitions that characterise when two terms of the form |
1600 definitions that characterise when two terms of the form |
1596 |
1601 |
1597 \begin{center} |
1602 \begin{center} |
1598 @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"} |
1603 @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"} |
1599 \end{center} |
1604 \end{center} |
1605 \begin{center} |
1610 \begin{center} |
1606 @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n = C\<^sup>\<alpha> y\<^isub>1 \<dots> y\<^isub>n"} |
1611 @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n = C\<^sup>\<alpha> y\<^isub>1 \<dots> y\<^isub>n"} |
1607 \end{center} |
1612 \end{center} |
1608 |
1613 |
1609 \noindent |
1614 \noindent |
1610 We call these conditions as \emph{quasi-injectivity}. Except for one definition we have |
1615 We call these conditions as \emph{quasi-injectivity}. Except for one function, which |
1611 to lift in the next section, this completes |
1616 we have to lift in the next section, this stage completes |
1612 the lifting part of establishing the reasoning infrastructure. From |
1617 the lifting part of establishing the reasoning infrastructure. From |
1613 now on we can ``forget'' about the raw types @{text "ty\<^bsub>1..n\<^esub>"} and only |
1618 now on, we can almost completely ``forget'' about the raw types @{text "ty\<^bsub>1..n\<^esub>"} and only |
1614 reason with @{text "ty\<AL>\<^bsub>1..n\<^esub>"} |
1619 reason about @{text "ty\<AL>\<^bsub>1..n\<^esub>"}. |
1615 |
1620 |
1616 We can first show that the free-variable function and binding functions |
1621 We can first show that the free-variable functions and binding functions |
1617 are equivariant, namely |
1622 are equivariant, namely |
1618 |
1623 |
1619 \begin{center} |
1624 \begin{center} |
1620 \begin{tabular}{rcl} |
1625 \begin{tabular}{rcl} |
1621 @{text "p \<bullet> (fv_ty\<^sup>\<alpha> x)"} & $=$ & @{text "fv_ty\<^sup>\<alpha> (p \<bullet> x)"}\\ |
1626 @{text "p \<bullet> (fv_ty\<^sup>\<alpha> x)"} & $=$ & @{text "fv_ty\<^sup>\<alpha> (p \<bullet> x)"}\\ |
1622 @{text "p \<bullet> (bn\<^sup>\<alpha> x)"} & $=$ & @{text "bn\<^sup>\<alpha> (p \<bullet> x)"} |
1627 @{text "p \<bullet> (bn\<^sup>\<alpha> x)"} & $=$ & @{text "bn\<^sup>\<alpha> (p \<bullet> x)"} |
1623 \end{tabular} |
1628 \end{tabular} |
1624 \end{center} |
1629 \end{center} |
1625 |
1630 |
1626 \noindent |
1631 \noindent |
1627 These facts can be established by structural induction over the @{text x}. |
1632 These two properties can be established by structural induction over the @{text x}. |
1628 |
1633 |
1629 Until now we have not yet derived any fact about the support of the |
1634 Until now we have not yet derived any fact about the support of the |
1630 alpha-equated terms. Using the equivariance properties in \eqref{ceqvt} we can |
1635 alpha-equated terms. Using the equivariance properties in \eqref{ceqvt} we can |
1631 show for every term-constructor @{text "C\<^sup>\<alpha>"} that |
1636 show for every term-constructor @{text "C\<^sup>\<alpha>"} that |
1632 |
1637 |
1633 \begin{center} |
1638 \begin{center} |
1634 @{text "supp x\<^isub>1 \<union> \<dots> supp x\<^isub>n supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"} |
1639 @{text "supp x\<^isub>1 \<union> \<dots> supp x\<^isub>n supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"}. |
1635 \end{center} |
1640 \end{center} |
1636 |
1641 |
1637 \noindent |
1642 \noindent |
1638 holds. This together with Property~\ref{supportsprobs} allows us to show |
1643 This together with Property~\ref{supportsprop} allows us to show |
1639 |
1644 |
1640 |
1645 |
1641 \begin{center} |
1646 \begin{center} |
1642 @{text "finite (supp x\<^isub>i)"} |
1647 @{text "finite (supp x\<^isub>i)"} |
1643 \end{center} |
1648 \end{center} |
1644 |
1649 |
1645 \noindent |
1650 \noindent |
1646 by mutual structural induction over @{text "x\<^isub>1, \<dots>, x\<^isub>n"} (whereby @{text "x\<^isub>i"} ranges over the types |
1651 by a structural induction over @{text "x\<^isub>1, \<dots>, x\<^isub>n"} (whereby @{text "x\<^isub>i"} ranges over the types |
1647 @{text "ty\<AL>\<^isub>1 \<dots> ty\<AL>\<^isub>n"}). Lastly, we can show that the support of elements in |
1652 @{text "ty\<AL>\<^isub>1 \<dots> ty\<AL>\<^isub>n"}). Lastly, we can show that the support of elements in |
1648 @{text "ty\<AL>\<^bsub>1..n\<^esub>"} coincides with @{text "fv_ty\<AL>\<^bsub>1..n\<^esub>"}. |
1653 @{text "ty\<AL>\<^bsub>1..n\<^esub>"} coincides with @{text "fv_ty\<AL>\<^bsub>1..n\<^esub>"}. |
1649 |
1654 |
1650 \begin{lemma} For every @{text "x\<^isub>i"} of type @{text "ty\<AL>\<^bsub>1..n\<^esub>"}, we have that |
1655 \begin{lemma} |
|
1656 For every @{text "x\<^isub>i"} of type @{text "ty\<AL>\<^bsub>1..n\<^esub>"}, we have that |
1651 @{text "supp x\<^isub>i = fv_ty\<AL>\<^isub>i x\<^isub>i"} holds. |
1657 @{text "supp x\<^isub>i = fv_ty\<AL>\<^isub>i x\<^isub>i"} holds. |
1652 \end{lemma} |
1658 \end{lemma} |
1653 |
1659 |
1654 \begin{proof} |
1660 \begin{proof} |
1655 The proof proceeds by structural induction over the @{text "x\<^isub>i"}. In each case |
1661 The proof proceeds by structural induction over the @{text "x\<^isub>i"}. In each case |