diff -r a2d5f9ea17ad -r e6a5651a1d81 Paper/Paper.thy --- a/Paper/Paper.thy Fri Apr 02 06:45:50 2010 +0200 +++ b/Paper/Paper.thy Fri Apr 02 07:30:25 2010 +0200 @@ -1465,8 +1465,8 @@ text {* Having made all necessary definitions for raw terms, we can start introducing the reasoning infrastructure for the alpha-equated types the - user specified. We sketch in this section the facts we need for establishing - this reasoning infrastructure. We first have to show that the + user originally specified. We sketch in this section the facts we need for establishing + this reasoning infrastructure. First we have to show that the alpha-equivalence relations defined in the previous section are indeed equivalence relations. @@ -1485,18 +1485,18 @@ \noindent We can feed this lemma into our quotient package and obtain new types @{text - "ty"}$^\alpha_{1..n}$ representing alpha-equated terms of types @{text - "ty"}$_{1..n}$. We also obtain definitions for the term-constructors @{text + "ty"}$^\alpha_{1..n}$ representing alpha-equated terms. We also obtain + definitions for the term-constructors @{text "C"}$^\alpha_{1..m}$ from the raw term-constructors @{text - "C"}$_{1..m}$. Similarly for the free-variable functions @{text + "C"}$_{1..m}$, and similar definitions for the free-variable functions @{text "fv_ty"}$^\alpha_{1..n}$ and the binding functions @{text - "bn"}$^\alpha_{1..k}$. However, these definitions are of not much use for the - user, since the are formulated in terms of the isomorphisms we obtained by + "bn"}$^\alpha_{1..k}$. However, these definitions are not really useful to the + user, since the are given in terms of the isomorphisms we obtained by creating new types in Isabelle/HOL (recall the picture shown in the Introduction). - The first useful property about term-constructors - is to know that they are distinct, that is + The first useful property to the user is the fact that term-constructors are + distinct, that is % \begin{equation}\label{distinctalpha} \mbox{@{text "C"}$^\alpha_i$@{text "x\<^isub>1 \ x\<^isub>n"} @{text "\"} @@ -1508,39 +1508,39 @@ for the raw term-constructors % \begin{equation}\label{distinctraw} - @{text "C\<^isub>i x\<^isub>1 \ x\<^isub>n"}\;\not\approx@{text ty}\;@{text "C\<^isub>j y\<^isub>1 \ y\<^isub>m"} holds for @{text "i \ j"}. + \mbox{@{text "C\<^isub>i x\<^isub>1 \ x\<^isub>n"}\;$\not\approx$@{text ty}\;@{text "C\<^isub>j y\<^isub>1 \ y\<^isub>m"} holds for @{text "i \ j"}.} \end{equation} \noindent - In order to generate \eqref{distinctalpha} from this fact, the quotient + In order to generate \eqref{distinctalpha} from \eqref{distinctraw}, the quotient package needs to know that the term-constructors @{text "C\<^isub>i"} and @{text "C\<^isub>j"} - are \emph{respectful} w.r.t.~the alpha-equivalence relations \cite{Homeier05}. - This means, given @{text "C\<^isub>i"} is of type @{text "ty"} with argument types - @{text "C ty\<^isub>1 \ ty\<^isub>n"}, we have to show that + are \emph{respectful} w.r.t.~the alpha-equivalence relations (see \cite{Homeier05}). + Assuming @{text "C\<^isub>i"} is of type @{text "ty"} with argument types + @{text "C ty\<^isub>1 \ ty\<^isub>n"}, then respectfulness amounts to showing \begin{center} @{text "C x\<^isub>1 \ x\<^isub>n \ty C y\<^isub>1 \ y\<^isub>n"} \end{center} \noindent - under the assumption that @{text "x\<^isub>i \ty\<^isub>i y\<^isub>i"} holds for all recursive arguments - and @{text "x\<^isub>i = y\<^isub>i"} for all non-recursive arguments. We can prove this by - analysing the definition of @{text "\ty"}. For this to succeed we have to establish an - auxiliary fact: given a binding function @{text bn} defined for the type @{text ty} - we have that - + are alpha-equivalent under the assumption that @{text "x\<^isub>i \ty\<^isub>i y\<^isub>i"} holds for all recursive arguments + and @{text "x\<^isub>i = y\<^isub>i"} holds for all non-recursive arguments. We can prove this by + analysing the definition of @{text "\ty"}. For this to succeed we have to establish + the following auxiliary fact about binding functions. Given a binding function @{text bn\<^isub>i} defined + for the type @{text ty\<^isub>i}, we have that + % \begin{center} - @{text "x \ty y"} implies @{text "x \bn y"} + @{text "x \ty\<^isub>i y"} implies @{text "x \bn\<^isub>i y"} \end{center} \noindent - This can be established by induction on the definition of @{text "\ty"}. + This can be established by induction on the definition of @{text "\ty\<^isub>i"}. Having established respectfulness for every raw term-constructor, the - quotient package will automatically deduce \eqref{distinctalpha} from \eqref{distinctraw}. - In fact we can lift any fact from the raw level to the alpha-equated level that - apart from variables only contains the raw term-constructors @{text "C\<^isub>i"}. The - induction principles derived by the datatype package of Isabelle/HOL for @{text + quotient package is able to automatically deduce \eqref{distinctalpha} from \eqref{distinctraw}. + In fact we can from now on lift any fact from the raw level to the alpha-equated level that + apart from variables only contains the raw term-constructors. The + induction principles derived by the datatype package in Isabelle/HOL for teh types @{text "ty"}$^\alpha_{1..n}$ fall into this category. So we can also add to our infrastructure induction principles that establish @@ -1549,8 +1549,9 @@ \end{center} \noindent - for every @{text "y\<^isub>i"} under the assumption we specified the types - @{text "ty\<^isub>1\<^isup>\ \ ty\<^isub>n\<^isup>\"}. The premises of these induction principles look + for all @{text "y\<^isub>i"} wherby the variables @{text "P\<^bsub>ty\<^isub>i\<^esub>"} stand for properties + defined over the types @{text "ty\<^isub>1\<^isup>\ \ ty\<^isub>n\<^isup>\"}. The premises of + these induction principles look as follows \begin{center} @@ -1561,10 +1562,11 @@ where the @{text "x\<^isub>i, \, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\"}. Next we lift the permutation operations defined in \eqref{ceqvt} for the raw term-constructors @{text "C"}. These facts contain, in addition - to the term-constructors, also permutations operations. Therefore - we have to know that permutation operations are respectful - w.r.t.~alpha-equivalence, which amounts to knowing that the - alpha-equivalence relations are equivariant, which we established + to the term-constructors, also permutations operations. In order to make the + lifting to go through, + we have to know that the permutation operations are respectful + w.r.t.~alpha-equivalence. This amounts to showing that the + alpha-equivalence relations are equivariant, which we already established in Lemma~\ref{equiv}. As a result we can add the equations \begin{equation}\label{ceqvt} @@ -1573,25 +1575,28 @@ \noindent to our infrastructure. In a similar fashion we can lift the equations - characterising our free-variable functions and the binding functions. - The necessary respectfulness lemmas are + characterising the free-variable functions @{text "fn_ty\\<^isub>j"} and the + binding functions @{text "bn\\<^isub>k"}. The necessary respectfulness lemmas for this + lifting are the two properties: % \begin{equation}\label{fnresp} \mbox{% \begin{tabular}{l} - @{text "x \ty y"} implies @{text "fv_ty x = fv_ty y"}\\ - @{text "x \ty y"} implies @{text "bn x = bn y"} + @{text "x \ty\<^isub>j y"} implies @{text "fv_ty\<^isub>j x = fv_ty\<^isub>j y"}\\ + @{text "x \ty\<^isub>j y"} implies @{text "bn\<^isub>k x = bn\<^isub>k y"} \end{tabular}} \end{equation} \noindent - which can be established by induction on @{text "\ty"}. While the first - kind of lemma is always ensured by way of how we defined the free variable - functions, the second does not hold in general. It only if the @{text bn}-functions - do not return any atom that is also bound. Hence our restriction imposed - on the binding functions that excludes this possibility. + which can be established by induction on @{text "\ty"}. Whereas the first + property is always true by the way how we defined the free-variable + functions, the second does \emph{not} hold in general. There is, in principle, + the possibility that the user defines @{text "bn\<^isub>k"} so that it returns an already bound + variable. Then the second property is just not true. However, our + restrictions imposed on the binding functions + exclude this possibility. - Having the facts \eqref{fnresp} at our disposal, we can finally lift the + Having the facts \eqref{fnresp} at our disposal, we can lift the definitions that characterise when two terms of the form \begin{center} @@ -1607,13 +1612,13 @@ \end{center} \noindent - We call these conditions as \emph{quasi-injectivity}. Except for one definition we have - to lift in the next section, this completes + We call these conditions as \emph{quasi-injectivity}. Except for one function, which + we have to lift in the next section, this stage completes the lifting part of establishing the reasoning infrastructure. From - now on we can ``forget'' about the raw types @{text "ty\<^bsub>1..n\<^esub>"} and only - reason with @{text "ty\\<^bsub>1..n\<^esub>"} + now on, we can almost completely ``forget'' about the raw types @{text "ty\<^bsub>1..n\<^esub>"} and only + reason about @{text "ty\\<^bsub>1..n\<^esub>"}. - We can first show that the free-variable function and binding functions + We can first show that the free-variable functions and binding functions are equivariant, namely \begin{center} @@ -1624,18 +1629,18 @@ \end{center} \noindent - These facts can be established by structural induction over the @{text x}. + These two properties can be established by structural induction over the @{text x}. Until now we have not yet derived any fact about the support of the alpha-equated terms. Using the equivariance properties in \eqref{ceqvt} we can show for every term-constructor @{text "C\<^sup>\"} that \begin{center} - @{text "supp x\<^isub>1 \ \ supp x\<^isub>n supports (C\<^sup>\ x\<^isub>1 \ x\<^isub>n)"} + @{text "supp x\<^isub>1 \ \ supp x\<^isub>n supports (C\<^sup>\ x\<^isub>1 \ x\<^isub>n)"}. \end{center} \noindent - holds. This together with Property~\ref{supportsprobs} allows us to show + This together with Property~\ref{supportsprop} allows us to show \begin{center} @@ -1643,11 +1648,12 @@ \end{center} \noindent - by mutual structural induction over @{text "x\<^isub>1, \, x\<^isub>n"} (whereby @{text "x\<^isub>i"} ranges over the types + by a structural induction over @{text "x\<^isub>1, \, x\<^isub>n"} (whereby @{text "x\<^isub>i"} ranges over the types @{text "ty\\<^isub>1 \ ty\\<^isub>n"}). Lastly, we can show that the support of elements in @{text "ty\\<^bsub>1..n\<^esub>"} coincides with @{text "fv_ty\\<^bsub>1..n\<^esub>"}. - \begin{lemma} For every @{text "x\<^isub>i"} of type @{text "ty\\<^bsub>1..n\<^esub>"}, we have that + \begin{lemma} + For every @{text "x\<^isub>i"} of type @{text "ty\\<^bsub>1..n\<^esub>"}, we have that @{text "supp x\<^isub>i = fv_ty\\<^isub>i x\<^isub>i"} holds. \end{lemma}