# HG changeset patch # User Christian Urban # Date 1316684575 -7200 # Node ID a609eea06119b62adade3cdce7d9f52f3c4fc7f4 # Parent 3f32a3eb56180740e57c9b3b5e9f693b97975130 final polishing? diff -r 3f32a3eb5618 -r a609eea06119 LMCS-Paper/Paper.thy --- a/LMCS-Paper/Paper.thy Thu Sep 22 21:43:04 2011 +0900 +++ b/LMCS-Paper/Paper.thy Thu Sep 22 11:42:55 2011 +0200 @@ -724,7 +724,7 @@ If we do not want to make any difference between the order of binders \emph{and} also allow vacuous binders, that means according to Pitts~\cite{Pitts04} - \emph{restrict} names, then we keep sets of binders, but drop + \emph{restrict} atoms, then we keep sets of binders, but drop condition {\it (iv)} in Definition~\ref{alphaset}: \begin{defi}[Alpha-Equivalence for Set+-Bindings]\label{alphares}\mbox{}\\ @@ -745,7 +745,7 @@ define \[ - @{text "fa(x) \ {x}"} \hspace{5mm} @{text "fa(T\<^isub>1 \ T\<^isub>2) \ fa(T\<^isub>1) \ fa(T\<^isub>2)"} + @{text "fa(x) \ {x}"} \hspace{10mm} @{text "fa(T\<^isub>1 \ T\<^isub>2) \ fa(T\<^isub>1) \ fa(T\<^isub>2)"} \]\smallskip \noindent @@ -803,7 +803,7 @@ \ \ x) equal supp (\ \ bs, \ \ y)"} holds provided \mbox{@{term "alpha_set_ex (as, x) equal supp(bs, y)"}} holds. From the assumption we have a permutation @{text "\'"} and for the proof obligation use @{text "\ \ - \'"}. To show then equivariance, we need to `pull out' the permutations, + \'"}. To show equivariance, we need to `pull out' the permutations, which is possible since all operators, namely as @{text "#\<^sup>*, -, =, \, set"} and @{text "supp"}, are equivariant (see \cite{HuffmanUrban10}). Finally, we apply the permutation operation on @@ -923,7 +923,7 @@ \end{equation}\smallskip \noindent - This is because for every finite sets of atoms, say @{text "bs"}, we have + This is because for every finite set 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 others are similar. @@ -1926,7 +1926,7 @@ \end{equation}\smallskip \noindent - where @{text "y"} is a variable of type @{text "ty"}$_i$ and @{text "P"} is the + where @{text "y"} is a variable of type @{text "ty\"}$_i$ and @{text "P"} is the property that is established by the case analysis. Similarly, we have a (mutual) induction principle for the types @{text "ty\"}$_{1..n}$, which is of the form @@ -1992,7 +1992,7 @@ \end{equation}\smallskip By working now completely on the alpha-equated level, we - can first show using \eqref{calphaeqvt} that the support of each term + can first show using \eqref{calphaeqvt} and Property~\ref{swapfreshfresh} that the support of each term constructor is included in the support of its arguments, namely @@ -2112,7 +2112,7 @@ "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---for example assuming the variable convention. One obvious way around this - problem is to rename them. Unfortunately, this leads to very clunky proofs + problem is to rename bound atoms. Unfortunately, this leads to very clunky proofs and makes formalisations grievous experiences (especially in the context of multiple bound atoms). @@ -2158,7 +2158,7 @@ line). In order to see how an instantiation for @{text "c"} in the conclusion `controls' the premises, one has 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 + with, for example, a pair, 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 @@ -2214,7 +2214,7 @@ the right-hand side) since the weak and strong cases lemma coincide (there is no binding in patterns). Interesting are only the cases for @{text "Lam\<^sup>\"} and @{text "Let_pat\<^sup>\"}, where we have some binders and - therefore have an addition assumption about avoiding @{text "c"}. Let us + therefore have an additional assumption about avoiding @{text "c"}. Let us first establish the case for @{text "Lam\<^sup>\"}. By the weak cases lemma \eqref{inductex} we can assume that @@ -2328,7 +2328,7 @@ \[\mbox{ \begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}} $\bullet$ & @{text "y\<^isub>i \ x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\ - $\bullet$ & @{text "y\<^isub>i \ \ \\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\ + $\bullet$ & @{text "y\<^isub>i \ \ \\<^bsub>bn\<^esub> x\<^isub>i"} provided @{text "bn x\<^isub>i"} is in @{text "rhs"}\\ $\bullet$ & @{text "y\<^isub>i \ \ \ x\<^isub>i"} otherwise \end{tabular}} \]\smallskip @@ -2336,7 +2336,7 @@ \noindent Using again the quotient package we can lift the auxiliary permutation operations @{text "_ \\<^bsub>bn\<^esub> _"} - to alpha-equated terms. Moreover we can prove the following two properties + to alpha-equated terms. Moreover we can prove the following two properties: \begin{lem}\label{permutebn} Given a binding function @{text "bn\<^sup>\"} and auxiliary equivalence @{text "\\\<^bsub>bn\<^esub>"} @@ -2384,9 +2384,9 @@ Consequently, we can discharge all proof-obligations about having covered all cases. This completes the proof establishing that the weak induction principles imply - the strong induction principles. These strong induction principles have proved - already to be very useful in practice, particularly for proving properties about - capture-avoiding substitution. + the strong induction principles. These strong induction principles have already proved + being very useful in practice, particularly for proving properties about + capture-avoiding substitution \cite{Urban08}. *} @@ -2455,7 +2455,7 @@ have proved that our definitions lead to alpha-equated terms, whose support 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 + alpha-equivalence classes. For this we have established (automatically) that every term-constructor and function defined for `raw' types is respectful w.r.t.~alpha-equivalence. @@ -2616,7 +2616,7 @@ in Ott. We have tried out the extension with calculi such as Core-Haskell, type-schemes and approximately a dozen of other typical examples from programming language research~\cite{SewellBestiary}. The code will - eventually become part of the next Isabelle distribution.\footnote{It + eventually become part of the Isabelle distribution.\footnote{It can be downloaded already from \href{http://isabelle.in.tum.de/nominal/download} {http://isabelle.in.tum.de/nominal/download}.}