nominal2: comparison LMCS-Paper/Paper.thy

equal deleted inserted replaced

-:4de1d6ab04f7
+:a5a6aebec1fb
 @{text "\<LET> x = 3 \<AND> y = 2 \<AND> z = foo \<IN> x - y \<END>"}
 \]\smallskip
 \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
 language constructs frequently occurring in programming language
 research. For example in @{text "\<LET>"}s containing patterns like
 Another is that our reasoning infrastructure, like strong induction principles
 and the notion of free variables, is derived from first principles within
 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
 where every datatype must have a non-empty set-theoretic model
 \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
 \[
 @{text "\<forall>{x}. x \<rightarrow> y  = \<forall>{x, z}. x \<rightarrow> y"}
 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
 that the HOL-logic underlying Nominal Isabelle allows us to replace
-``equals-by-equals''. In contrast, replacing
+`equals-by-equals'. In contrast, replacing
-``alpha-equals-by-alpha-equals'' in a representation based on ``raw'' terms
+`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
 terms is nearly always taken for granted, establishing it automatically in
 Isabelle/HOL is a rather non-trivial task. For every
 The fact that we obtain an isomorphism between the new type and the
 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
 system. This package allows us to lift definitions and theorems involving
 raw terms to definitions and theorems involving alpha-equated terms. For
 \noindent
 (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.
 To sum up, every lifting
 of theorems to the quotient level needs proofs of some respectfulness
 we introduce crucial restrictions, and also extensions, so that our
 specifications make sense for reasoning about alpha-equated terms.  The main
 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]
 \begin{boxedminipage}{\linewidth}
 \begin{center}
 \[
 @{text "(a b) = \<lambda>c. if a = c then b else if b = c then a else c"}
 \]\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
+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
+"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
 @{text x}, namely:
 of binders (being bound, or fresh, in @{text x} is ensured by the
 assumption @{term "as \<sharp>* x"}), then there exists a permutation @{text "\<pi>"} such that
 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>"}
 is equivalent with @{term "supp \<pi> \<sharp>* x"}, which means we could also formulate
 Propositions \ref{supppermeq} and \ref{avoiding} in the other `direction'; however the
 from this specification (remember that Nominal Isabelle is a definitional
 extension of Isabelle/HOL, which does not introduce any new axioms).
 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
 are intended to represent the abstraction, or binding, of the set of atoms @{text
 "as"} in the body @{text "x"}.
 vacuous binders.) To answer this question, we identify four conditions: {\it (i)}
 given a free-atom function @{text "fa"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
 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:
 \begin{defi}[Alpha-Equivalence for Set-Bindings]\label{alphaset}\mbox{}\\
 \noindent
 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"}.
 Definition \ref{alphaset} does not make any distinction between the
 \begin{equation}\label{halfone}
 @{thm Abs_supports(1)[no_vars]}
 \end{equation}\smallskip
 \noindent
-which by Property~\ref{supportsprop} gives us ``one half'' of
+which by Property~\ref{supportsprop} gives us `one half' of
-Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish
+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
 \[
 @{thm supp_set.simps[THEN eq_reflection, no_vars]}
 @{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}.
 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}
 @{term "supp (Abs_set as x) = supp x - as"}
 \]\smallskip
 \noindent
 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
+we have established in Theorem~\ref{suppabs} that bound atoms are removed from
-abstractions' bodies.
+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
 Isabelle/HOL level properties about them.  It would be extremely laborious
 to write custom ML-code that derives automatically such properties for every
 \noindent
 whereby some of the @{text ty}$'_{1..l}$ (or their components) can be
 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
 clauses}, which indicate the binders and their scope in a term-constructor.
 They come in three \emph{modes}:
 \noindent
 The first mode is for binding lists of atoms (the order of bound atoms
 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};
+`\isacommand{in}-part' of a binding clause will be called \emph{bodies};
-the ``\isacommand{binds}-part'' will be called \emph{binders}. In contrast to
+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:
 \[\mbox{
 \begin{tabular}{@ {}ll@ {}}
 @{text name}, in which case all three binding modes coincide. However, having
 \isacommand{binds (set)} or just \isacommand{binds}
 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
 expected to return either a set of atoms (for \isacommand{binds (set)} and
 \isacommand{binds (set+)}) or a list of atoms (for \isacommand{binds}). They need
 \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}
 \mbox{%
 \begin{tabular}{@ {}l@ {}}
 establish a reasoning infrastructure for them. As Pottier and Cheney pointed
 out \cite{Cheney05,Pottier06}, just re-arranging the arguments of
 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
 non-empty and the types in the constructors only occur in positive
 position (see \cite{Berghofer99} for an in-depth description of the datatype package
 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}
 @{text "\<pi> \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (\<pi> \<bullet> z\<^isub>1) \<dots> (\<pi> \<bullet> z\<^isub>n)"}
 \end{equation}\smallskip
 We will need this operation later when we define the notion of alpha-equivalence.
 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
 \begin{equation}\label{fvars}
 @{text "fa_bn"}\mbox{$_{1..m}$}.
 \]\smallskip
 \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
 clause means. We only show the details for the mode \isacommand{binds (set)} (the other modes are similar).
 Suppose the binding clause @{text bc\<^isub>i} is of the form
 \begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}}
 $\bullet$ & @{term "fa_ty\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text "rhs"}\\
 & (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)\\
 \end{tabular}}
 \]\smallskip
 function @{text "bn"}, the function @{text "fa\<^bsub>bn\<^esub>"} traverses
 the list of assignments, but instead returns the free atoms, which means in
 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
 actually become bound.  This is a phenomenon that has also been pointed out
 in \cite{ott-jfp}. For us this observation is crucial, because we would not
 be able to lift the @{text "bn"}-functions to alpha-equated terms if they
 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
 \[
 \mbox{@{text "\<approx>ty"}$_{1..n}$}.
 \]\smallskip
 \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
 will define shortly).  Let us assume the non-recursive deep binders
 in @{text "bc\<^isub>i"} are
 \end{tabular}}
 \end{equation}\smallskip
 \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"},
+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.
+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
 corresponding binding clause specifies a binder with two bodies, namely
 @{text "as"} and @{text "t"}.
 \end{lem}
 \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
+that the free-atom functions are terminating. From this the function
-derived by the function package \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}
 \noindent
 \noindent
 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
 are not really useful to the user, since they are given in terms of the
 isomorphisms we obtained by creating new types in Isabelle/HOL (recall the
 \begin{equation}\label{distinctraw}
 \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>r"}\;$\not\approx$@{text ty}\;@{text "D y\<^isub>1 \<dots> y\<^isub>s"}}
 \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
 \[\mbox{
 restriction imposed on the form of the binding functions---namely \emph{not}
 to return any bound atoms. In Ott, in contrast, the user may define @{text
 "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}.
 Next we can lift the permutation operations defined in \eqref{ceqvt}. In
 order to make this lifting to go through, we have to show that the
 \noindent
 to our infrastructure. In a similar fashion we can lift the defining equations
 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"}}
 \]\smallskip
 recursive arguments of this term constructor (similarly for the other
 term-constructors).
 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):
 \begin{equation}\label{inductex}\mbox{
 \begin{tabular}{c}
 \]\smallskip
 \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
 @{text "supp x\<^isub>i = fa_ty\<AL>\<^isub>i x\<^isub>i"}.
 \end{thm}
 for which we have to know that every body of an abstraction is finitely supported.
 This, we have proved earlier.
 \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>"}
 \[\mbox{
 \begin{tabular}{@ {}c @ {}}
 \noindent
 using the support of abstractions derived in Theorem~\ref{suppabs}.
 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.
 *}
 text {*
 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
 @{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
 P\<^bsub>trm\<^esub> y\<^isub>1 \<and> P\<^bsub>pat\<^esub> y\<^isub>2"}, as the
 weak one does, the stronger induction principle establishes the properties
 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}.
 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
 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
+leveraging the automated proving tools from the function package of
-Isabelle/HOL \cite{Krauss09}. The reasoning principle behind these methods
+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
 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
 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
 is straightforward to establish that the sizes decrease in every
 induction step. What is left to show is that we covered all cases.
 \noindent
 They are stronger in the sense that they allow us to assume in the @{text
 "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
 "Lam\<^sup>\<alpha>"} and @{text "Let_pat\<^sup>\<alpha>"}, where we have some binders and
 therefore have an addition assumption about avoiding @{text "c"}.  Let us
 @{text "\<forall>x\<^isub>1 x\<^isub>2. atom x\<^isub>1 # c \<and> y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}
 \end{equation}\smallskip
 \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>
 x\<^isub>1 x\<^isub>2"} (since its support is @{text "supp x\<^isub>2 -
 {atom x\<^isub>1}"}). Property \ref{avoiding} provides us then with a
 \begin{equation}\label{impletpat}
 @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. set (bn\<^sup>\<alpha> x\<^isub>1) #\<^sup>* c \<and> y = Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub>"}
 \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)"}
 \]\smallskip
 \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) =
 Abs_lst (bn_al x\<^isub>1) x\<^isub>3"} (remember @{text "set"} and @{text
 "bn\<^sup>\<alpha>"} are equivariant).  Now the quasi-injective property for @{text
 @{text "p \<approx>\<AL>\<^bsub>bn\<^esub> p\<PRIME>"}\;\; & @{text "t\<^isub>1 = t\<PRIME>\<^isub>1"}}
 \]\smallskip
 \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
+The remaining difficulty is when a deep binder contains some atoms that are
-bound, but also some that are free. An example is @{text "Let\<^sup>\<alpha>"} in
+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
+\<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} does not hold in general. The idea however is
-that we only want to rename binders that will become bound. This does not
+that @{text "\<pi>"} only renames atoms that become bound. In this way @{text "\<pi>"}
-affect @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"}. However, the problem is that the
+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
+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
+the other atoms unchanged. Like the functions @{text "fa_bn"}$_{1..m}$, we
-can define these operations over raw terms analysing how the @{text
+can define these operations over raw terms analysing how the functions @{text
-"bn"}$_{1..m}$-functions are defined. Assuming the user specified a clause
+"bn"}$_{1..m}$ are defined. Assuming the user specified a clause
 \[
 @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}
 \]\smallskip
 \noindent
 Using again the quotient package  we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} functions to
 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}
 \begin{proof}
 @{text "(\<pi> \<bullet> (set (bn\<^sup>\<alpha> x\<^isub>1)) #\<^sup>* c"} \hspace{10mm}
 @{text "\<pi> \<bullet> [bn\<^sup>\<alpha> x\<^isub>1]\<^bsub>list\<^esub>. x\<^isub>2 = [bn\<^sup>\<alpha> x\<^isub>1]\<^bsub>list\<^esub>. x\<^isub>2"}
 \]\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
 \[
 @{text "Let\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1) (\<pi> \<bullet> x\<^isub>2) = Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2"}
 \]\smallskip
 \noindent
 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
+Conseqently,  we can discharge all proof-obligations about having covered all
-cases. This completes the proof showing that the weak induction principles imply
+cases. This completes the proof establishing that the weak induction principles imply
-the strong induction principles.
+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.
 *}
 section {* Related Work\label{related} *}
 formalisation of the algorithm W. This formalisation implements binding in
 type-schemes using a de-Bruijn indices representation. Since type-schemes in
 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
+recently explored for general binders by Chargu\'eraud \cite{chargueraud09}
-approach to
+in the locally nameless approach to
-binding \cite{chargueraud09}.  There, de-Bruijn indices consist of two
+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
+as `normal' datatypes.  However, in both approaches it seems difficult to
-achieve our fine-grained control over the ``semantics'' of bindings
+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
 rather intricate formal reasoning. We are not aware of any formalisation of
 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
+(HOAS), which for example is implemented in the Twelf system \cite{pfenningsystem}.
-representation technique supports very elegantly many aspects of
+This representation technique supports very elegantly many aspects of
-\emph{single} binding, and impressive work by Lee et al has been done that
+\emph{single} binding, and impressive work by Lee et al ~\cite{LeeCraryHarper07}
-uses HOAS for mechanising the metatheory of SML~\cite{LeeCraryHarper07}. We
+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
 reasoning about the resulting terms.
 performed in older
 versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W
 \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.
 The most closely related work to the one presented here is the Ott-tool by
 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
 specified in Ott.  This definition is rather different from ours, not using
 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
-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
 Isabelle. First, it is far too complicated to be a basis for automated
 proofs implemented on the ML-level of Isabelle/HOL. Second, it covers cases
 \end{tabular}}
 \]\smallskip
 \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
 there are two permutations so that we can make @{text "(a, b)"} and @{text
 "(a, b)"} equal with one permutation, and @{text "(a, b)"} and @{text "(b,
 and therefore need the extra generality to be able to distinguish between
 both specifications.  Because of how we set up our definitions, we also had
 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
-\begin{figure}[t]
+Figure~\ref{nominalcorehas} and then Nominal Isabelle derives automatically
+a corresponding reasoning infrastructure.
+\begin{figure}[p]
 \begin{boxedminipage}{\linewidth}
 \small
 \begin{tabular}{l}
 \isacommand{atom\_decl}~@{text "var cvar tvar"}\\[1mm]
 \isacommand{nominal\_datatype}~@{text "tkind ="}~@{text "KStar"}~$|$~@{text "KFun tkind tkind"}\\
 $|$~@{text "bv\<^isub>2 (TVTKCons a ty tl) = (atom a)::(bv\<^isub>2 tl)"}\\
 $|$~@{text "bv\<^isub>3 TVCKNil = []"}\\
 $|$~@{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
+definition follows closely the original shown in Figure~\ref{corehas}. The
-point of our work is that having made such a declaration in Nominal Isabelle,
+point of our work is that having made such a definition in Nominal Isabelle,
-one obtains automatically a reasoning infrastructure for Core-Haskell.\bigskip\bigskip
+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
 language is implemented as a front-end that can be translated to OCaml with
 the help of a library. He presents a type-system in which the scope of
 section {* Conclusion *}
 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
 alpha-equated terms involving general binders. In earlier versions of
 Nominal Isabelle this turned out to be a thorny issue.  We hope to do better
 datatype definitions allow one to specify, for instance, the function kinds
 in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded
 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
 functions can only return the empty set, a singleton atom set or unions
 of atom sets (similarly for lists). It remains to be seen whether
 We have also not yet played with other binding modes. For example we can
 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
 discussions about Nominal Isabelle. We thank Peter Sewell for making the
 informal notes \cite{SewellBestiary} available to us and also for patiently

changeset 3023	a5a6aebec1fb
parent 3022	4de1d6ab04f7
child 3024	10e476d6f4b8