Paper/Paper.thy
changeset 1767 e6a5651a1d81
parent 1766 a2d5f9ea17ad
child 1768 375e15002efc
equal deleted inserted replaced
1766:a2d5f9ea17ad 1767:e6a5651a1d81
  1463 section {* Establishing the Reasoning Infrastructure *}
  1463 section {* Establishing the Reasoning Infrastructure *}
  1464 
  1464 
  1465 text {*
  1465 text {*
  1466   Having made all necessary definitions for raw terms, we can start
  1466   Having made all necessary definitions for raw terms, we can start
  1467   introducing the reasoning infrastructure for the alpha-equated types the
  1467   introducing the reasoning infrastructure for the alpha-equated types the
  1468   user specified. We sketch in this section the facts we need for establishing
  1468   user originally specified. We sketch in this section the facts we need for establishing
  1469   this reasoning infrastructure. We first have to show that the
  1469   this reasoning infrastructure. First we have to show that the
  1470   alpha-equivalence relations defined in the previous section are indeed
  1470   alpha-equivalence relations defined in the previous section are indeed
  1471   equivalence relations.
  1471   equivalence relations.
  1472 
  1472 
  1473   \begin{lemma}\label{equiv} 
  1473   \begin{lemma}\label{equiv} 
  1474   Given the raw types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} and binding functions
  1474   Given the raw types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} and binding functions
  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