--- 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(\<ANIL>) ="} @{term "{}"} \hspace{10mm}
+ @{text "bn(\<ANIL>) ="}~@{term "{}"} \hspace{10mm}
@{text "bn(\<ACONS> x t as) = {x} \<union> 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 "(\<pi> \<bullet> x) R (\<pi> \<bullet> 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 \<rightleftharpoons> b) = 0"}.
+ If @{term "a = b"} the lemma is immediate, since @{term "(a \<rightleftharpoons> 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 \<rightleftharpoons> b) \<bullet> (supp x - as) =
- (supp x - as)"}. We therefore can use the swapping @{term "(a \<rightleftharpoons> b)"}. as
- the permutation fpr the proof obligation.
+ (supp x - as)"}. We therefore can use the swapping @{term "(a \<rightleftharpoons> 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 \<union> 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>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}
- 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>\<alpha>"} and the term-constructors @{text "C\<^sup>\<alpha>"}.
+ In our implementation we just use the affix ``@{text "_raw"}''.
But for the purpose of this paper, we use the superscript @{text "_\<^sup>\<alpha>"} 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>\<alpha> / ty"} and @{text "C\<^sup>\<alpha> / C"}
where @{term ty} is the type used in the quotient construction for
- @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor of the `raw' type @{text "ty"},
+ @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor of the raw type @{text "ty"},
respectively @{text "C\<^sup>\<alpha>"} is the corresponding term-constructor of @{text "ty\<^sup>\<alpha>"}.
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\<dots>bc\<^isub>k"}, the result of @{text
"fa_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be the union @{text
"fa(bc\<^isub>1) \<union> \<dots> \<union> 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 "\<approx>ty"}$_{1..n}$ and
@{text "\<approx>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\<AL>"}$_{1..n}$ and
@{text "fa_bn\<AL>"}$_{1..m}$ as well as of the binding functions @{text
"bn\<AL>"}$_{1..m}$ and size functions @{text "size_ty\<AL>"}$_{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 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^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\<AL>"}$_{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\<AL>"}$_i$, can be
+ analysing how an element of a type, say @{text "ty\<AL>"}$_i$, can be
constructed (that means one case for each of the term-constructors in @{text
"ty\<AL>"}$_i\,$). The lifted cases lemma for the type @{text
"ty\<AL>"}$_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>\<alpha> x\<^isub>1\<dots>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>\<alpha>"} we can assume the bound atom @{text "x\<^isub>1"} is fresh
for @{text "c"} (third line); for @{text "Let_pat\<^sup>\<alpha>"} 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 "\<pi>"}, for the abstraction @{term "Abs_lst (bn_al x\<^isub>1)
x\<^isub>3"}. As a result we have \mbox{@{term "set (bn_al (\<pi> \<bullet> 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>\<alpha>"} in
- the example \eqref{letrecs}. In such cases @{text "(\<pi> \<bullet> x\<^isub>1)
+ \eqref{letrecs}. In such cases @{text "(\<pi> \<bullet> x\<^isub>1)
\<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} does not hold in general. The idea however is
that @{text "\<pi>"} only renames atoms that become bound. In this way @{text "\<pi>"}
- does not affect @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"}. However, the problem is that the
+ does not affect @{text "\<approx>\<AL>\<^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 "\<pi> \<bullet> x\<^isub>1"} applies to all attoms in @{text "x\<^isub>1"}. To avoid this
we introduce an auxiliary permutation operations, written @{text "_
\<bullet>\<^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 "_ \<bullet>\<^bsub>bn\<^esub> _"} functions to
+ Using again the quotient package we can lift the auxiliary permutation operations
+ @{text "_ \<bullet>\<^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 "_ \<bullet>\<^bsub>bn\<^esub> _"} preserves
+ atoms. The second states that @{text "_ \<bullet>\<AL>\<^bsub>bn\<^esub> _"} preserves
@{text "\<approx>\<AL>\<^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>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1)) #\<^sup>* c"} and
- @{text "[bn\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1)]\<^bsub>list\<^esub>. (\<pi> \<bullet> x\<^isub>2) = [bn\<^sup>\<alpha> x\<^isub>1]\<^bsub>list\<^esub>. x\<^isub>2"}. Since
- @{text "(\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1) \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} holds by teh second part,
+ \mbox{@{text "[bn\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1)]\<^bsub>list\<^esub>. (\<pi> \<bullet> x\<^isub>2) = [bn\<^sup>\<alpha> x\<^isub>1]\<^bsub>list\<^esub>. x\<^isub>2"}}. Since
+ @{text "(\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1) \<approx>\<AL>\<^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.