diff -r 10e476d6f4b8 -r 204a488c71c6 LMCS-Paper/Paper.thy --- a/LMCS-Paper/Paper.thy Tue Sep 20 14:44:50 2011 +0900 +++ b/LMCS-Paper/Paper.thy Tue Sep 20 09:17:29 2011 +0200 @@ -235,7 +235,7 @@ assn} as follows \[ - @{text "bn(\) ="} @{term "{}"} \hspace{10mm} + @{text "bn(\) ="}~@{term "{}"} \hspace{10mm} @{text "bn(\ x t as) = {x} \ bn(as)"} \]\smallskip @@ -261,7 +261,7 @@ \cite{Berghofer99}. Another reason is that we establish the reasoning infrastructure for alpha-\emph{equated} terms. In contrast, Ott produces a reasoning infrastructure in Isabelle/HOL for \emph{non}-alpha-equated, or - `raw', terms. While our alpha-equated terms and the raw terms produced by + `raw', terms. While our alpha-equated terms and the `raw' terms produced by Ott use names for bound variables, there is a key difference: working with alpha-equated terms means, for example, that the two type-schemes @@ -279,7 +279,7 @@ Our insistence on reasoning with alpha-equated terms comes from the wealth of experience we gained with the older version of Nominal Isabelle: for non-trivial properties, reasoning with alpha-equated terms is much - easier than reasoning with raw terms. The fundamental reason for this is + easier than reasoning with `raw' terms. The fundamental reason for this is that the HOL-logic underlying Nominal Isabelle allows us to replace `equals-by-equals'. In contrast, replacing `alpha-equals-by-alpha-equals' in a representation based on `raw' terms @@ -394,7 +394,7 @@ including properties about support, freshness and equality conditions for alpha-equated terms. We are also able to automatically derive strong induction principles that have the variable convention already built in. - For this we simplify the earlier automated proofs by using the proof tools + For this we simplify the earlier automated proofs by using the proving tools from the function package~\cite{Krauss09} of Isabelle/HOL. The method behind our specification of general binders is taken from the Ott-tool, but we introduce crucial restrictions, and also extensions, so that our @@ -604,9 +604,9 @@ also a similar notion for equivariant relations, say @{text R}, namely the property that - \begin{center} + \[ @{text "x R y"} \;\;\textit{implies}\;\; @{text "(\ \ x) R (\ \ y)"} - \end{center} + \]\smallskip Using freshness, the nominal logic work provides us with general means for renaming binders. @@ -696,7 +696,7 @@ Note that the relation is dependent on a free-atom function @{text "fa"} and a relation @{text "R"}. The reason for this extra generality is that we will use - $\approx_{\,\textit{set}}^{\textit{R}, \textit{fa}}$ for both `raw' terms and + $\approx_{\,\textit{set}}^{\textit{R}, \textit{fa}}$ for both raw terms and alpha-equated terms. In the latter case, @{text R} will be replaced by equality @{text "="} and we will prove that @{text "fa"} is equal to @{text "supp"}. @@ -767,7 +767,7 @@ abstract a single atom. In the rest of this section we are going to show that the alpha-equivalences - really lead to abstractions where some atoms are bound (more precisely + really lead to abstractions where some atoms are bound (or more precisely removed from the support). For this we will consider three abstraction types that are quotients of the relations @@ -843,7 +843,7 @@ \noindent In effect, this theorem states that the atoms @{text "as"} are bound in the - abstraction. As stated earlier, this can be seen as litmus test that our + abstraction. As stated earlier, this can be seen as a litmus test that our Definitions \ref{alphaset}, \ref{alphalist} and \ref{alphares} capture the idea of alpha-equivalence relations. Below we will give the proof for the first equation of Theorem \ref{suppabs}. The others follow by similar @@ -875,11 +875,12 @@ \end{lem} \begin{proof} - If @{term "a = b"} the lemma is immediate, since @{term "(a \ b) = 0"}. + If @{term "a = b"} the lemma is immediate, since @{term "(a \ b)"} is then + the identity permutation. Also in the other case the lemma is straightforward using \eqref{abseqiff} and observing that the assumptions give us @{term "(a \ b) \ (supp x - as) = - (supp x - as)"}. We therefore can use the swapping @{term "(a \ b)"}. as - the permutation fpr the proof obligation. + (supp x - as)"}. We therefore can use the swapping @{term "(a \ b)"} as + the permutation for the proof obligation. \end{proof} \noindent @@ -922,10 +923,10 @@ This is because for every finite sets of atoms, say @{text "bs"}, we have @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}. Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes - the first equation of Theorem~\ref{suppabs}. + the first equation of Theorem~\ref{suppabs}. The others are similar. Recall the definition of support given in \eqref{suppdef}, and note the difference between - the support of a `raw' pair and an abstraction + the support of a raw pair and an abstraction \[ @{term "supp (as, x) = supp as \ supp x"}\hspace{15mm} @@ -1278,15 +1279,15 @@ The `raw' datatype definition can be obtained by stripping off the - binding clauses and the labels from the types. We also have to invent - new names for the types @{text "ty\<^sup>\"} and term-constructors @{text "C\<^sup>\"} - given by the user. In our implementation we just use the affix `@{text "_raw"}'. + binding clauses and the labels from the types given by the user. We also have to invent + new names for the types @{text "ty\<^sup>\"} and the term-constructors @{text "C\<^sup>\"}. + In our implementation we just use the affix ``@{text "_raw"}''. But for the purpose of this paper, we use the superscript @{text "_\<^sup>\"} to indicate that a notion is given for alpha-equivalence classes and leave it out - for the corresponding notion given on the `raw' level. So for example + for the corresponding notion given on the raw level. So for example we have @{text "ty\<^sup>\ / ty"} and @{text "C\<^sup>\ / C"} where @{term ty} is the type used in the quotient construction for - @{text "ty\<^sup>\"} and @{text "C"} is the term-constructor of the `raw' type @{text "ty"}, + @{text "ty\<^sup>\"} and @{text "C"} is the term-constructor of the raw type @{text "ty"}, respectively @{text "C\<^sup>\"} is the corresponding term-constructor of @{text "ty\<^sup>\"}. The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are @@ -1295,7 +1296,7 @@ in Isabelle/HOL). We subsequently define each of the user-specified binding functions @{term "bn"}$_{1..m}$ by recursion over the corresponding - `raw' datatype. We also define permutation operations by + raw datatype. We also define permutation operations by recursion so that for each term constructor @{text "C"} we have that \begin{equation}\label{ceqvt} @@ -1335,7 +1336,7 @@ While the idea behind these free-atom functions is simple (they just collect all atoms that are not bound), because of our rather complicated binding mechanisms their definitions are somewhat involved. Given - a `raw' term-constructor @{text "C"} of type @{text ty} and some associated + a raw term-constructor @{text "C"} of type @{text ty} and some associated binding clauses @{text "bc\<^isub>1\bc\<^isub>k"}, the result of @{text "fa_ty (C z\<^isub>1 \ z\<^isub>n)"} will be the union @{text "fa(bc\<^isub>1) \ \ \ fa(bc\<^isub>k)"} where we will define below what @{text "fa"} for a binding @@ -1759,7 +1760,7 @@ The function package of Isabelle/HOL allows us to prove the first part by mutual induction over the definitions of the functions.\footnote{We have that the free-atom functions are terminating. From this the function - package derives an induction principle \cite{Krauss09}.} The second is by a + package derives an induction principle~\cite{Krauss09}.} The second is by a straightforward induction over the rules of @{text "\ty"}$_{1..n}$ and @{text "\bn"}$_{1..m}$ using the first part. \end{proof} @@ -1785,7 +1786,7 @@ We can feed the last 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 "C"}$^\alpha_{1..k}$ from the `raw' term-constructors @{text + @{text "C"}$^\alpha_{1..k}$ from the raw term-constructors @{text "C"}$_{1..k}$, and similar definitions for the free-atom functions @{text "fa_ty"}$^\alpha_{1..n}$ and @{text "fa_bn"}$^\alpha_{1..m}$ as well as the binding functions @{text "bn"}$^\alpha_{1..m}$. However, these definitions @@ -1811,9 +1812,9 @@ \end{equation}\smallskip \noindent - holds for the corresponding `raw' term-constructors. + holds for the corresponding raw term-constructors. In order to deduce \eqref{distinctalpha} from \eqref{distinctraw}, our quotient - package needs to know that the `raw' term-constructors @{text "C"} and @{text "D"} + package needs to know that the raw term-constructors @{text "C"} and @{text "D"} are \emph{respectful} w.r.t.~the alpha-equivalence relations (see \cite{Homeier05}). Given, for example, @{text "C"} is of type @{text "ty"} with argument types @{text "ty"}$_{1..r}$, respectfulness amounts to showing that @@ -1849,7 +1850,7 @@ "bn"}$_{1..m}$ so that they return bound atoms and in this case the third implication is \emph{not} true. A result is that in general the lifting of the corresponding binding functions in Ott to alpha-equated terms is impossible. - Having established respectfulness for the `raw' term-constructors, the + Having established respectfulness for the raw term-constructors, the quotient package is able to automatically deduce \eqref{distinctalpha} from \eqref{distinctraw}. @@ -1869,10 +1870,10 @@ of the free-atom functions @{text "fa_ty\"}$_{1..n}$ and @{text "fa_bn\"}$_{1..m}$ as well as of the binding functions @{text "bn\"}$_{1..m}$ and size functions @{text "size_ty\"}$_{1..n}$. - The latter are defined automatically for the `raw' types @{text "ty"}$_{1..n}$ + The latter are defined automatically for the raw types @{text "ty"}$_{1..n}$ by the datatype package of Isabelle/HOL. - We also need to lift the properties that characterise when two `raw' terms of the form + We also need to lift the properties that characterise when two raw terms of the form \[ \mbox{@{text "C x\<^isub>1 \ x\<^isub>r \ty C x\\<^isub>1 \ x\\<^isub>r"}} @@ -1909,7 +1910,7 @@ We can also add to our infrastructure cases lemmas and a (mutual) induction principle for the types @{text "ty\"}$_{1..n}$. The cases lemmas allow the user to deduce a property @{text "P"} by exhaustively - analysing how an element in a type, say @{text "ty\"}$_i$, can be + analysing how an element of a type, say @{text "ty\"}$_i$, can be constructed (that means one case for each of the term-constructors in @{text "ty\"}$_i\,$). The lifted cases lemma for the type @{text "ty\"}$_i\,$ looks as follows @@ -1956,8 +1957,7 @@ Recall the lambda-calculus with @{text "Let"}-patterns shown in \eqref{letpat}. The cases lemmas and the induction principle shown in \eqref{cases} and \eqref{induct} boil down in that example to the following three inference - rules (the cases lemmas are on the left-hand side; the induction principle - on the right): + rules: \begin{equation}\label{inductex}\mbox{ \begin{tabular}{c} @@ -2111,7 +2111,8 @@ hypothesis requires us to establish (under some assumptions) a property @{text "P (C\<^sup>\ x\<^isub>1\x\<^isub>r)"} for \emph{all} @{text "x"}$_{1..r}$. The problem with this is that in the presence of binders we cannot make - any assumptions about the atoms that are bound. One obvious way around this + any assumptions about the atoms that are bound---for example assuming the variable convention. + One obvious way around this problem is to rename them. Unfortunately, this leads to very clunky proofs and makes formalisations grievous experiences (especially in the context of multiple bound atoms). @@ -2156,10 +2157,14 @@ "Lam\<^sup>\"} we can assume the bound atom @{text "x\<^isub>1"} is fresh for @{text "c"} (third line); for @{text "Let_pat\<^sup>\"} we can assume all bound atoms from an assignment are fresh for @{text "c"} (fourth - line). If @{text "c"} is instantiated appropriately in the strong induction - principle, then the user can mimic the usual `pencil-and-paper' reasoning - employing the variable convention about bound and free variables being - distinct \cite{Urban08}. + line). In order to see how an instantiation for @{text "c"} in the + conclusion `controls' the premises, you have to take into account that + Isabelle/HOL is a typed logic. That means if @{text "c"} is instantiated + with a pair, for example, then this type-constraint will be propagated to + the premises. The main point is that if @{text "c"} is instantiated + appropriately, then the user can mimic the usual `pencil-and-paper' + reasoning employing the variable convention about bound and free variables + being distinct \cite{Urban08}. In what follows we will show that the weak induction principle in \eqref{inductex} implies the strong one \eqref{stronginduct}. This fact was established for @@ -2172,7 +2177,7 @@ each type @{text "ty"}$^\alpha_{1..n}$) that decrease in every induction step and the other is that we have covered all cases in the induction principle. Once these two proof obligations are discharged, the reasoning - infrastructure in the function package will automatically derive the + infrastructure of the function package will automatically derive the stronger induction principle. This way of establishing the stronger induction principle is considerably simpler than the earlier work presented \cite{Urban08}. @@ -2229,7 +2234,7 @@ \end{equation}\smallskip \noindent - which we must use to infer @{text "P\<^bsub>trm\<^esub>"}. Clearly, we cannot + which we must use in order to infer @{text "P\<^bsub>trm\<^esub>"}. Clearly, we cannot use this implication directly, because we have no information whether or not @{text "x\<^isub>1"} is fresh for @{text "c"}. However, we can use Properties \ref{supppermeq} and \ref{avoiding} to rename @{text "x\<^isub>1"}: we know @@ -2274,7 +2279,7 @@ \]\smallskip \noindent - where @{text x} and @{text y} are bound in the term, but they are also free + where @{text x} and @{text y} are bound in the term, but are also free in the right-hand side of the assignment. We can, however, obtain such a renaming permutation, say @{text "\"}, for the abstraction @{term "Abs_lst (bn_al x\<^isub>1) x\<^isub>3"}. As a result we have \mbox{@{term "set (bn_al (\ \ x\<^isub>1)) @@ -2303,16 +2308,17 @@ The remaining difficulty is when a deep binder contains some atoms that are bound and some that are free. An example is @{text "Let\<^sup>\"} in - the example \eqref{letrecs}. In such cases @{text "(\ \ x\<^isub>1) + \eqref{letrecs}. In such cases @{text "(\ \ x\<^isub>1) \\\<^bsub>bn\<^esub> x\<^isub>1"} does not hold in general. The idea however is that @{text "\"} only renames atoms that become bound. In this way @{text "\"} - does not affect @{text "\\\<^bsub>bn\<^esub>"}. However, the problem is that the + does not affect @{text "\\\<^bsub>bn\<^esub>"} (which only tracks alpha-equivalence of terms that are not + under the binder). However, the problem is that the permutation operation @{text "\ \ x\<^isub>1"} applies to all attoms in @{text "x\<^isub>1"}. To avoid this we introduce an auxiliary permutation operations, written @{text "_ \\<^bsub>bn\<^esub> _"}, for deep binders that only permutes bound atoms (or more precisely the atoms specified by the @{text "bn"}-functions) and leaves the other atoms unchanged. Like the functions @{text "fa_bn"}$_{1..m}$, we - can define these operations over raw terms analysing how the functions @{text + can define these permutation operations over raw terms analysing how the functions @{text "bn"}$_{1..m}$ are defined. Assuming the user specified a clause \[ @@ -2331,7 +2337,8 @@ \]\smallskip \noindent - Using again the quotient package we can lift the @{text "_ \\<^bsub>bn\<^esub> _"} functions to + Using again the quotient package we can lift the auxiliary permutation operations + @{text "_ \\<^bsub>bn\<^esub> _"} alpha-equated terms. Moreover we can prove the following two properties \begin{lem}\label{permutebn} @@ -2349,7 +2356,7 @@ \noindent The first property states that a permutation applied to a binding function is equivalent to first permuting the binders and then calculating the bound - atoms. The second states that @{text "_ \\<^bsub>bn\<^esub> _"} preserves + atoms. The second states that @{text "_ \\\<^bsub>bn\<^esub> _"} preserves @{text "\\\<^bsub>bn\<^esub>"}. The main point of the auxiliary permutation functions is that they allow us to rename just the binders in a term, without changing anything else. @@ -2366,8 +2373,8 @@ \noindent hold. Using the first part of Lemma \ref{permutebn}, we can simplify this to @{text "set (bn\<^sup>\ (\ \\\<^bsub>bn\<^esub> x\<^isub>1)) #\<^sup>* c"} and - @{text "[bn\<^sup>\ (\ \\\<^bsub>bn\<^esub> x\<^isub>1)]\<^bsub>list\<^esub>. (\ \ x\<^isub>2) = [bn\<^sup>\ x\<^isub>1]\<^bsub>list\<^esub>. x\<^isub>2"}. Since - @{text "(\ \\\<^bsub>bn\<^esub> x\<^isub>1) \\\<^bsub>bn\<^esub> x\<^isub>1"} holds by teh second part, + \mbox{@{text "[bn\<^sup>\ (\ \\\<^bsub>bn\<^esub> x\<^isub>1)]\<^bsub>list\<^esub>. (\ \ x\<^isub>2) = [bn\<^sup>\ x\<^isub>1]\<^bsub>list\<^esub>. x\<^isub>2"}}. Since + @{text "(\ \\\<^bsub>bn\<^esub> x\<^isub>1) \\\<^bsub>bn\<^esub> x\<^isub>1"} holds by the second part, we can infer that \[ @@ -2376,7 +2383,7 @@ \noindent holds. This allows us to use the implication from the strong cases - lemma. + lemma, and we are done. Conseqently, we can discharge all proof-obligations about having covered all cases. This completes the proof establishing that the weak induction principles imply @@ -2449,7 +2456,7 @@ any nominal techniques. To our knowledge there is no concrete mathematical result concerning this notion of alpha-equivalence and free variables. We have proved that our definitions lead to alpha-equated terms, whose support - is as expected (that means bound names are removed from the support). We + is as expected (that means bound atoms are removed from the support). We also showed that our specifications lift from `raw' types to types of alpha-equivalence classes. For this we had to establish (automatically) that every term-constructor and function defined for `raw' types @@ -2512,7 +2519,7 @@ binder) that are not present in Ott. Our expectation is that we can still cover many interesting term-calculi from programming language research, for example the Core-Haskell language from the Introduction. With the work - presented in this paper we can define formally this language as shown in + presented in this paper we can define it formally as shown in Figure~\ref{nominalcorehas} and then Nominal Isabelle derives automatically a corresponding reasoning infrastructure. @@ -2565,7 +2572,7 @@ \end{boxedminipage} \caption{A definition for Core-Haskell in Nominal Isabelle. For the moment we do not support nested types; therefore we explicitly have to unfold the - lists @{text "co_lst"}, @{text "assoc_lst"} and so on. Apart from that, the + lists @{text "co_lst"}, @{text "assoc_lst"} and so on. Apart from that limitation, the definition follows closely the original shown in Figure~\ref{corehas}. The point of our work is that having made such a definition in Nominal Isabelle, one obtains automatically a reasoning infrastructure for Core-Haskell.