--- a/LMCS-Paper/Paper.thy Sun Sep 18 22:52:56 2011 +0200
+++ b/LMCS-Paper/Paper.thy Mon Sep 19 21:52:59 2011 +0200
@@ -166,7 +166,7 @@
\noindent
Therefore we will also provide a separate binding mechanism for cases in
- which the order of binders does not matter, but the ``cardinality'' of the
+ which the order of binders does not matter, but the `cardinality' of the
binders has to agree.
However, we found that this is still not sufficient for dealing with
@@ -253,7 +253,7 @@
the Isabelle/HOL theorem prover.
However, we will not be able to cope with all specifications that are
- allowed by Ott. One reason is that Ott lets the user specify ``empty'' types
+ allowed by Ott. One reason is that Ott lets the user specify `empty' types
like \mbox{@{text "t ::= t t | \<lambda>x. t"}} where no clause for variables is
given. Arguably, such specifications make some sense in the context of Coq's
type theory (which Ott supports), but not at all in a HOL-based environment
@@ -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
@@ -281,8 +281,8 @@
for non-trivial properties, reasoning with alpha-equated terms is much
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
+ `equals-by-equals'. In contrast, replacing
+ `alpha-equals-by-alpha-equals' in a representation based on `raw' terms
requires a lot of extra reasoning work.
Although in informal settings a reasoning infrastructure for alpha-equated
@@ -330,11 +330,11 @@
non-empty subset shows that the new type is a faithful representation of
alpha-equated terms. That is not the case for example for terms using the
locally nameless representation of binders \cite{McKinnaPollack99}: in this
- representation there are ``junk'' terms that need to be excluded by
+ representation there are `junk' terms that need to be excluded by
reasoning about a well-formedness predicate.
The problem with introducing a new type in Isabelle/HOL is that in order to
- be useful, a reasoning infrastructure needs to be ``lifted'' from the
+ be useful, a reasoning infrastructure needs to be `lifted' from the
underlying subset to the new type. This is usually a tricky and arduous
task. To ease it, we re-implemented in Isabelle/HOL \cite{KaliszykUrban11}
the quotient package described by Homeier \cite{Homeier05} for the HOL4
@@ -368,7 +368,7 @@
(Note that this means also the term-constructors for variables, applications
and lambda are lifted to the quotient level.) This construction, of course,
only works if alpha-equivalence is indeed an equivalence relation, and the
- ``raw'' definitions and theorems are respectful w.r.t.~alpha-equivalence.
+ `raw' definitions and theorems are respectful w.r.t.~alpha-equivalence.
For example, we will not be able to lift a bound-variable function. Although
this function can be defined for raw terms, it does not respect
alpha-equivalence and therefore cannot be lifted.
@@ -402,7 +402,7 @@
improvement over Ott is that we introduce three binding modes (only one is
present in Ott), provide formalised definitions for alpha-equivalence and
for free variables of our terms, and also derive a reasoning infrastructure
- for our specifications from ``first principles'' inside a theorem prover.
+ for our specifications from `first principles' inside a theorem prover.
\begin{figure}[t]
@@ -504,8 +504,8 @@
\]\smallskip
The most original aspect of the nominal logic work of Pitts is a general
- definition for the notion of the ``set of free variables of an object @{text
- "x"}''. This notion, written @{term "supp x"}, is general in the sense that
+ definition for the notion of the `set of free variables of an object @{text
+ "x"}'. This notion, written @{term "supp x"}, is general in the sense that
it applies not only to lambda-terms (alpha-equated or not), but also to lists,
products, sets and even functions. Its definition depends only on the
permutation operation and on the notion of equality defined for the type of
@@ -635,7 +635,7 @@
the renamed binders @{term "\<pi> \<bullet> as"} avoid @{text c} (which can be arbitrarily chosen
as long as it is finitely supported) and also @{text "\<pi>"} does not affect anything
in the support of @{text x} (that is @{term "supp x \<sharp>* \<pi>"}). The last
- fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders
+ fact and Property~\ref{supppermeq} allow us to `rename' just the binders
@{text as} in @{text x}, because @{term "\<pi> \<bullet> x = x"}.
Note that @{term "supp x \<sharp>* \<pi>"}
@@ -661,7 +661,7 @@
In order to keep our work with deriving the reasoning infrastructure
manageable, we will wherever possible state definitions and perform proofs
- on the ``user-level'' of Isabelle/HOL, as opposed to writing custom ML-code that
+ on the `user-level' of Isabelle/HOL, as opposed to writing custom ML-code that
generates them anew for each specification.
To that end, we will consider
first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}. These pairs
@@ -676,7 +676,7 @@
set"}}, then @{text x} and @{text y} need to have the same set of free
atoms; moreover there must be a permutation @{text \<pi>} such that {\it
(ii)} @{text \<pi>} leaves the free atoms of @{text x} and @{text y} unchanged, but
- {\it (iii)} ``moves'' their bound names so that we obtain modulo a relation,
+ {\it (iii)} `moves' their bound names so that we obtain modulo a relation,
say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)}
@{text \<pi>} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
requirements {\it (i)} to {\it (iv)} can be stated formally as:
@@ -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"}.
@@ -891,8 +891,8 @@
\end{equation}\smallskip
\noindent
- which by Property~\ref{supportsprop} gives us ``one half'' of
- Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish
+ which by Property~\ref{supportsprop} gives us `one half' of
+ Theorem~\ref{suppabs}. The `other half' is a bit more involved. To establish
it, we use a trick from \cite{Pitts04} and first define an auxiliary
function @{text aux}, taking an abstraction as argument
@@ -925,7 +925,7 @@
the first equation of Theorem~\ref{suppabs}.
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}
@@ -936,8 +936,8 @@
While the permutation operations behave in both cases the same (a permutation
is just moved to the arguments), the notion of equality is different for pairs and
abstractions. Therefore we have different supports. In case of abstractions,
- we have established that bound atoms are removed from the support of the
- abstractions' bodies.
+ we have established in Theorem~\ref{suppabs} that bound atoms are removed from
+ the support of the abstractions' bodies.
The method of first considering abstractions of the form @{term "Abs_set as
x"} etc is motivated by the fact that we can conveniently establish at the
@@ -997,7 +997,7 @@
contained in the collection of @{text ty}$^\alpha_{1..n}$ declared in
\eqref{scheme}. In this case we will call the corresponding argument a
\emph{recursive argument} of @{text "C\<^sup>\<alpha>"}. The types of such
- recursive arguments need to satisfy a ``positivity'' restriction, which
+ recursive arguments need to satisfy a `positivity' restriction, which
ensures that the type has a set-theoretic semantics (see
\cite{Berghofer99}). The labels annotated on the types are optional. Their
purpose is to be used in the (possibly empty) list of \emph{binding
@@ -1018,8 +1018,8 @@
matters); the second is for sets of binders (the order does not matter, but
the cardinality does) and the last is for sets of binders (with vacuous
binders preserving alpha-equivalence). As indicated, the labels in the
- ``\isacommand{in}-part'' of a binding clause will be called \emph{bodies};
- the ``\isacommand{binds}-part'' will be called \emph{binders}. In contrast to
+ `\isacommand{in}-part' of a binding clause will be called \emph{bodies};
+ the `\isacommand{binds}-part' will be called \emph{binders}. In contrast to
Ott, we allow multiple labels in binders and bodies. For example we allow
binding clauses of the form:
@@ -1098,7 +1098,7 @@
in the second case makes a difference to the semantics of the specification
(which we will define in the next section).
- A \emph{deep} binder uses an auxiliary binding function that ``picks'' out
+ A \emph{deep} binder uses an auxiliary binding function that `picks' out
the atoms in one argument of the term-constructor, which can be bound in
other arguments and also in the same argument (we will call such binders
\emph{recursive}, see below). The binding functions are
@@ -1150,7 +1150,7 @@
\noindent
where the argument of the deep binder also occurs in the body. We call such
binders \emph{recursive}. To see the purpose of such recursive binders,
- compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s in the following
+ compare `plain' @{text "Let"}s and @{text "Let_rec"}s in the following
specification:
\begin{equation}\label{letrecs}
@@ -1272,21 +1272,21 @@
term-constructors so that binders and their bodies are next to each other
will result in inadequate representations in cases like \mbox{@{text "Let
x\<^isub>1 = t\<^isub>1\<dots>x\<^isub>n = t\<^isub>n in s"}}. Therefore we will
- first extract ``raw'' datatype definitions from the specification and then
+ first extract `raw' datatype definitions from the specification and then
define explicitly an alpha-equivalence relation over them. We subsequently
construct the quotient of the datatypes according to our alpha-equivalence.
- The ``raw'' datatype definition can be obtained by stripping off the
+ 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"}''.
+ given by the user. 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 +1295,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}
@@ -1308,7 +1308,7 @@
The first non-trivial step we have to perform is the generation of
\emph{free-atom functions} from the specifications.\footnote{Admittedly, the
details of our definitions will be somewhat involved. However they are still
- conceptually simple in comparison with the ``positional'' approach taken in
+ conceptually simple in comparison with the `positional' approach taken in
Ott \cite[Pages 88--95]{ott-jfp}, which uses the notions of \emph{occurrences} and
\emph{partial equivalence relations} over sets of occurrences.} For the
\emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions
@@ -1329,13 +1329,13 @@
\noindent
The reason for this setup is that in a deep binder not all atoms have to be
- bound, as we saw in \eqref{letrecs} with the example of ``plain'' @{text Let}s. We need
+ bound, as we saw in \eqref{letrecs} with the example of `plain' @{text Let}s. We need
therefore functions that calculate those free atoms in deep binders.
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
@@ -1444,7 +1444,7 @@
& (that means nothing is bound in @{text "z\<^isub>i"} by the binding function),\smallskip\\
$\bullet$ & @{term "fa_bn\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} occurs in @{text "rhs"}
with the recursive call @{text "bn\<^isub>i z\<^isub>i"}\\
- & (that means whatever is ``left over'' from the @{text "bn"}-function is free)\smallskip\\
+ & (that means whatever is `left over' from the @{text "bn"}-function is free)\smallskip\\
$\bullet$ & @{term "{}"} provided @{text "z\<^isub>i"} occurs in @{text "rhs"},
but without a recursive call\\
& (that means @{text "z\<^isub>i"} is supposed to become bound by the binding function)\\
@@ -1496,7 +1496,7 @@
this example the free atoms in the argument @{text "t"}.
- An interesting point in this example is that a ``naked'' assignment (@{text
+ An interesting point in this example is that a `naked' assignment (@{text
"ANil"} or @{text "ACons"}) does not bind any atoms, even if the binding
function is specified over assignments. Only in the context of a @{text Let}
or @{text "Let_rec"}, where the binding clauses are given, will some atoms
@@ -1506,7 +1506,7 @@
act on atoms that are bound. In that case, these functions would \emph{not}
respect alpha-equivalence.
- Having the free atom functions at our disposal, we can next define the
+ Having the free-atom functions at our disposal, we can next define the
alpha-equivalence relations for the raw types @{text
"ty"}$_{1..n}$. We write them as
@@ -1629,7 +1629,7 @@
\noindent
This premise accounts for alpha-equivalence of the bodies of the binding
clause. However, in case the binders have non-recursive deep binders, this
- premise is not enough: we also have to ``propagate'' alpha-equivalence
+ premise is not enough: we also have to `propagate' alpha-equivalence
inside the structure of these binders. An example is @{text "Let"} where we
have to make sure the right-hand sides of assignments are
alpha-equivalent. For this we use relations @{text "\<approx>bn"}$_{1..m}$ (which we
@@ -1721,13 +1721,13 @@
\noindent
Notice the difference between $\approx_{\textit{assn}}$ and
- $\approx_{\textit{bn}}$: the latter only ``tracks'' alpha-equivalence of
+ $\approx_{\textit{bn}}$: the latter only `tracks' alpha-equivalence of
the components in an assignment that are \emph{not} bound. This is needed in the
clause for @{text "Let"} (which has
a non-recursive binder).
The underlying reason is that the terms inside an assignment are not meant
- to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"},
- because there all components of an assignment are ``under'' the binder.
+ to be `under' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"},
+ because there all components of an assignment are `under' the binder.
Note also that in case of more than one body (that is in the @{text "Let_rec"}-case above)
we need to parametrise the relation $\approx_{\textit{list}}$ with a compound
equivalence relation and a compound free-atom function. This is because the
@@ -1758,8 +1758,8 @@
\begin{proof}
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 they are terminating functions. From this an induction principle is
- derived by the function package \cite{Krauss09}.} The second is by a
+ that the free-atom functions are terminating. From this the function
+ 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 +1785,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 +1811,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 +1849,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 +1869,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"}}
@@ -1955,7 +1955,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 this example to the following three inference
+ \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):
@@ -2019,11 +2019,11 @@
\noindent
Lastly, we can show that the support of elements in @{text
- "ty\<AL>"}$_{1..n}$ is the same as the free atom functions @{text
+ "ty\<AL>"}$_{1..n}$ is the same as the free-atom functions @{text
"fa_ty\<AL>"}$_{1..n}$. This fact is important in the nominal setting where
the general theory is formulated in terms of support and freshness, but also
provides evidence that our notions of free-atoms and alpha-equivalence
- ``match up'' correctly.
+ `match up' correctly.
\begin{thm}\label{suppfa}
For @{text "x"}$_{1..n}$ with type @{text "ty\<AL>"}$_{1..n}$, we have
@@ -2040,7 +2040,7 @@
\end{proof}
\noindent
- Consequently, we can replace the free atom functions by @{text "supp"} in
+ Consequently, we can replace the free-atom functions by @{text "supp"} in
our quasi-injection lemmas. In the examples shown in \eqref{alphalift}, for instance,
we obtain for @{text "Let\<^sup>\<alpha>"} and @{text "Let_rec\<^sup>\<alpha>"}
@@ -2091,7 +2091,7 @@
To sum up this section, we have established a reasoning infrastructure for the
types @{text "ty\<AL>"}$_{1..n}$ by first lifting definitions from the
- ``raw'' level to the quotient level and then by proving facts about
+ `raw' level to the quotient level and then by proving facts about
these lifted definitions. All necessary proofs are generated automatically
by custom ML-code.
*}
@@ -2103,9 +2103,9 @@
In the previous section we derived induction principles for alpha-equated
terms (see \eqref{induct} for the general form and \eqref{inductex} for an
example). This was done by lifting the corresponding inductions principles
- for ``raw'' terms. We already employed these induction principles for
+ for `raw' terms. We already employed these induction principles for
deriving several facts about alpha-equated terms, including the property that
- the free-variable functions and the notion of support coincide. Still, we
+ the free-atom functions and the notion of support coincide. Still, we
call these induction principles \emph{weak}, because for a term-constructor,
say \mbox{@{text "C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r"}}, the induction
hypothesis requires us to establish (under some assumptions) a property
@@ -2151,13 +2151,13 @@
of the form @{text " P\<^bsub>trm\<^esub> c y\<^isub>1 \<and>
P\<^bsub>pat\<^esub> c y\<^isub>2"} in which the additional parameter @{text
c} is assumed to be of finite support. The purpose of @{text "c"} is to
- ``control'' which freshness assumptions the binders should satisfy in the
+ `control' which freshness assumptions the binders should satisfy in the
@{text "Lam\<^sup>\<alpha>"} and @{text "Let_pat\<^sup>\<alpha>"} cases: for @{text
"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, the user can mimic the usual ``pencil-and-paper'' reasoning
+ 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}.
@@ -2165,8 +2165,8 @@
\eqref{inductex} implies the strong one \eqref{stronginduct}. This fact was established for
single binders in \cite{Urban08} by some quite involved, nevertheless
automated, induction proof. In this paper we simplify the proof by
- leveraging the automated proving methods from the function package of
- Isabelle/HOL \cite{Krauss09}. The reasoning principle behind these methods
+ leveraging the automated proving tools from the function package of
+ Isabelle/HOL \cite{Krauss09}. The reasoning principle behind these tools
is well-founded induction. To use them in our setting, we have to discharge
two proof obligations: one is that we have well-founded measures (one for
each type @{text "ty"}$^\alpha_{1..n}$) that decrease in every induction
@@ -2174,7 +2174,7 @@
principle. Once these two proof obligations are discharged, the reasoning
infrastructure in the function package will automatically derive the
stronger induction principle. This way of establishing the stronger induction
- principle is considerably simpler than the work presented \cite{Urban08}.
+ principle is considerably simpler than the earlier work presented \cite{Urban08}.
As measures we can use the size functions @{text "size_ty"}$^\alpha_{1..n}$,
which we lifted in the previous section and which are all well-founded. It
@@ -2207,7 +2207,7 @@
"Lam\<^sup>\<alpha>"} and @{text "Let_pat\<^sup>\<alpha>"} cases that the bound atoms
avoid a context @{text "c"} (which is assumed to be finitely supported).
- These stronger cases lemmas need to be derived from the `weak' cases lemmas
+ These stronger cases lemmas can be derived from the `weak' cases lemmas
given in \eqref{inductex}. This is trivial in case of patterns (the one on
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
@@ -2230,7 +2230,7 @@
\noindent
which we must use to infer @{text "P\<^bsub>trm\<^esub>"}. Clearly, we cannot
- use this implication directly, because we have no information whether @{text
+ 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
by Theorem~\ref{suppfa} that @{text "{atom x\<^isub>1} #\<^sup>* Lam\<^sup>\<alpha>
@@ -2264,10 +2264,10 @@
\end{equation}\smallskip
\noindent
- The reason that this case is more complicated is that we cannot apply directly Property
+ The reason that this case is more complicated is that we cannot directly apply Property
\ref{avoiding} for obtaining a renaming permutation. Property \ref{avoiding} requires
that the binders are fresh for the term in which we want to perform the renaming. But
- this is not true in cases like (using informal notation)
+ this is not true in terms such as (using an informal notation)
\[
@{text "Let (x, y) := (x, y) in (x, y)"}
@@ -2275,7 +2275,7 @@
\noindent
where @{text x} and @{text y} are bound in the term, but they are also free
- in the assignment. We can, however, obtain such a renaming permutation, say
+ 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))
\<sharp>* c"}} and @{term "Abs_lst (bn_al (\<pi> \<bullet> x\<^isub>1)) (\<pi> \<bullet> x\<^isub>3) =
@@ -2291,29 +2291,29 @@
\noindent
Since all atoms in a pattern are bound by @{text "Let_pat\<^sup>\<alpha>"}, we can infer
- @{text "(\<pi> \<bullet> x\<^isub>1) \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} holds for every @{text "\<pi>"}. Therefore we have that
+ that @{text "(\<pi> \<bullet> x\<^isub>1) \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} holds for every @{text "\<pi>"}. Therefore we have that
\[
@{text "Let_pat\<^sup>\<alpha> (\<pi> \<bullet> x\<^isub>1) x\<^isub>2 (\<pi> \<bullet> x\<^isub>3) = Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3"}
\]\smallskip
\noindent
- Taking the left-hand side in the assumption from \eqref{assmtwo}, we can use
+ Taking the left-hand side in the assumption shown in \eqref{assmtwo}, we can use
the implication \eqref{impletpat} from the stronger cases lemma to infer @{text "P\<^bsub>trm\<^esub>"}, as needed.
- The remaining difficulty is when a deep binder contains atoms that are
- bound, but also some that are free. An example is @{text "Let\<^sup>\<alpha>"} in
+ 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)
- \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} does not hold in general. The idea is
- that we only want to rename binders that will become bound. This does not
- affect @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"}. However, the problem is that the
- permutation operation @{text "_ \<bullet> _"} applies to all of them. To avoid this
+ \<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
+ 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 @{text "fa_bn"}$_{1..m}$-functions, we
- can define these operations over raw terms analysing how the @{text
- "bn"}$_{1..m}$-functions are defined. Assuming the user specified a clause
+ 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
+ "bn"}$_{1..m}$ are defined. Assuming the user specified a clause
\[
@{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}
@@ -2335,7 +2335,8 @@
alpha-equated terms. Moreover we can prove the following two properties
\begin{lem}\label{permutebn}
- Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text "\<pi>"}\smallskip\\
+ Given a binding function @{text "bn\<^sup>\<alpha>"} and auxiliary equivalence @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"}
+ then for all @{text "\<pi>"}\smallskip\\
{\it (i)} @{text "\<pi> \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x)"} and\\
{\it (ii)} @{text "(\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x) \<approx>\<AL>\<^bsub>bn\<^esub> x"}.
\end{lem}
@@ -2363,10 +2364,10 @@
\]\smallskip
\noindent
- hold. Using Lemma \ref{permutebn}{\it (i)} we can simplify this
+ 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 Lemma \ref{permutebn}{\it (ii)},
+ @{text "(\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1) \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} holds by teh second part,
we can infer that
\[
@@ -2377,9 +2378,11 @@
holds. This allows us to use the implication from the strong cases
lemma.
- Conseqently, we can discharge all proof-obligations to do with having covered all
- cases. This completes the proof showing that the weak induction principles imply
- the strong induction principles.
+ Conseqently, 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.
*}
@@ -2393,15 +2396,15 @@
W contain only a single place where variables are bound, different indices
do not refer to different binders (as in the usual de-Bruijn
representation), but to different bound variables. A similar idea has been
- recently explored for general binders by Chargu\'eraud in the locally nameless
- approach to
- binding \cite{chargueraud09}. There, de-Bruijn indices consist of two
+ recently explored for general binders by Chargu\'eraud \cite{chargueraud09}
+ in the locally nameless approach to
+ binding. There, de-Bruijn indices consist of two
numbers, one referring to the place where a variable is bound, and the other
to which variable is bound. The reasoning infrastructure for both
representations of bindings comes for free in theorem provers like
Isabelle/HOL and Coq, since the corresponding term-calculi can be implemented
- as ``normal'' datatypes. However, in both approaches it seems difficult to
- achieve our fine-grained control over the ``semantics'' of bindings
+ as `normal' datatypes. However, in both approaches it seems difficult to
+ achieve our fine-grained control over the `semantics' of bindings
(i.e.~whether the order of binders should matter, or vacuous binders should
be taken into account). To do so, one would require additional predicates
that filter out unwanted terms. Our guess is that such predicates result in
@@ -2409,14 +2412,14 @@
a non-trivial language that uses Chargu\'eraud's idea.
Another technique for representing binding is higher-order abstract syntax
- (HOAS), which for example is implemented in the Twelf system. This
- representation technique supports very elegantly many aspects of
- \emph{single} binding, and impressive work by Lee et al has been done that
- uses HOAS for mechanising the metatheory of SML~\cite{LeeCraryHarper07}. We
+ (HOAS), which for example is implemented in the Twelf system \cite{pfenningsystem}.
+ This representation technique supports very elegantly many aspects of
+ \emph{single} binding, and impressive work by Lee et al ~\cite{LeeCraryHarper07}
+ has been done that uses HOAS for mechanising the metatheory of SML. We
are, however, not aware how multiple binders of SML are represented in this
work. Judging from the submitted Twelf-solution for the POPLmark challenge,
HOAS cannot easily deal with binding constructs where the number of bound
- variables is not fixed. For example In the second part of this challenge,
+ variables is not fixed. For example, in the second part of this challenge,
@{text "Let"}s involve patterns that bind multiple variables at once. In
such situations, HOAS seems to have to resort to the
iterated-single-binders-approach with all the unwanted consequences when
@@ -2429,7 +2432,7 @@
\cite{BengtsonParow09,UrbanNipkow09}). Both
use the approach based on iterated single binders. Our experience with
the latter formalisation has been disappointing. The major pain arose from
- the need to ``unbind'' variables. This can be done in one step with our
+ the need to `unbind' variables. This can be done in one step with our
general binders described in this paper, but needs a cumbersome
iteration with single binders. The resulting formal reasoning turned out to
be rather unpleasant.
@@ -2438,7 +2441,7 @@
Sewell et al \cite{ott-jfp} and the C$\alpha$ml language by Pottier
\cite{Pottier06}. Ott is a nifty front-end for creating \LaTeX{} documents
from specifications of term-calculi involving general binders. For a subset
- of the specifications Ott can also generate theorem prover code using a ``raw''
+ of the specifications Ott can also generate theorem prover code using a `raw'
representation of terms, and in Coq also a locally nameless
representation. The developers of this tool have also put forward (on paper)
a definition for alpha-equivalence and free variables for terms that can be
@@ -2447,9 +2450,10 @@
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
- also showed that our specifications lift from ``raw'' types to types of
+ 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 is respectful w.r.t.~alpha-equivalence.
+ term-constructor and function defined for `raw' types
+ is respectful w.r.t.~alpha-equivalence.
Although we were heavily inspired by the syntax of Ott, its definition of
alpha-equi\-valence is unsuitable for our extension of Nominal
@@ -2475,7 +2479,7 @@
\noindent
In the first term-constructor we have a single body that happens to be
- ``spread'' over two arguments; in the second term-constructor we have two
+ `spread' over two arguments; in the second term-constructor we have two
independent bodies in which the same variables are bound. As a result we
have\footnote{Assuming @{term "a \<noteq> b"}, there is no permutation that can
make @{text "(a, b)"} equal with both @{text "(a, b)"} and @{text "(b, a)"}, but
@@ -2507,9 +2511,12 @@
to impose some restrictions (like a single binding function for a deep
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 Core-Haskell (see Figure~\ref{nominalcorehas}).
+ example the Core-Haskell language from the Introduction. With the work
+ presented in this paper we can define formally this language as shown in
+ Figure~\ref{nominalcorehas} and then Nominal Isabelle derives automatically
+ a corresponding reasoning infrastructure.
- \begin{figure}[t]
+ \begin{figure}[p]
\begin{boxedminipage}{\linewidth}
\small
\begin{tabular}{l}
@@ -2556,15 +2563,15 @@
$|$~@{text "bv\<^isub>3 (TVCKCons c cty tl) = (atom c)::(bv\<^isub>3 tl)"}\\
\end{tabular}
\end{boxedminipage}
- \caption{The nominal datatype declaration for Core-Haskell. For the moment we
+ \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
- declaration follows closely the original in Figure~\ref{corehas}. The
- point of our work is that having made such a declaration in Nominal Isabelle,
- one obtains automatically a reasoning infrastructure for Core-Haskell.\bigskip\bigskip
+ 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.
\label{nominalcorehas}}
\end{figure}
-
+ \afterpage{\clearpage}
Pottier presents a programming language, called C$\alpha$ml, for
representing terms with general binders inside OCaml \cite{Pottier06}. This
@@ -2596,17 +2603,17 @@
text {*
We have presented an extension of Nominal Isabelle for dealing with general
- binders, that is term-constructors having multiple bound variables. For this
+ binders, that is where term-constructors have multiple bound atoms. For this
extension we introduced new definitions of alpha-equivalence and automated
all necessary proofs in Isabelle/HOL. To specify general binders we used
the syntax from Ott, but extended it in some places and restricted
- it in others so that they make sense in the context of alpha-equated
+ it in others so that the definitions make sense in the context of alpha-equated
terms. We also introduced two binding modes (set and set+) that do not exist
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
- can be downloaded from \href{http://isabelle.in.tum.de/nominal/download}
+ can be downloaded already from \href{http://isabelle.in.tum.de/nominal/download}
{http://isabelle.in.tum.de/nominal/download}.}
We have left out a discussion about how functions can be defined over
@@ -2624,7 +2631,7 @@
version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). To
achieve this, we need more clever implementation than we have
at the moment. However, really lifting this restriction will involve major
- work on the datatype package of Isabelle/HOL.
+ work on the underlying datatype package of Isabelle/HOL.
A more interesting line of investigation is whether we can go beyond the
simple-minded form of binding functions that we adopted from Ott. At the moment, binding
@@ -2643,7 +2650,7 @@
imagine that there is need for a binding mode where instead of usual lists,
we abstract lists of distinct elements (the corresponding type @{text
"dlist"} already exists in the library of Isabelle/HOL). We expect the
- presented work can be easily extended to accommodate them.\medskip
+ presented work can be easily extended to accommodate such binding modes.\medskip
\noindent
{\bf Acknowledgements:} We are very grateful to Andrew Pitts for many