nominal2: comparison LMCS-Paper/Paper.thy

equal deleted inserted replaced

-:10e476d6f4b8
+:204a488c71c6
 and @{text bn} an auxiliary function identifying the variables to be bound
 by the @{text "\<LET>"}. This function can be defined by recursion over @{text
 assn} as follows
 \[
-@{text "bn(\<ANIL>) ="} @{term "{}"} \hspace{10mm}
+@{text "bn(\<ANIL>) ="}~@{term "{}"} \hspace{10mm}
 @{text "bn(\<ACONS> x t as) = {x} \<union> bn(as)"}
 \]\smallskip
 \noindent
 The scope of the binding is indicated by labels given to the types, for
 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"}
 to).
 Our insistence on reasoning with alpha-equated terms comes from the
 wealth of experience we gained with the older version of Nominal Isabelle:
 for non-trivial properties, reasoning with alpha-equated terms is much
-easier than reasoning with raw terms. The fundamental reason for this is
+easier than reasoning with `raw' terms. The fundamental reason for this is
 that the HOL-logic underlying Nominal Isabelle allows us to replace
 `equals-by-equals'. In contrast, replacing
 `alpha-equals-by-alpha-equals' in a representation based on `raw' terms
 requires a lot of extra reasoning work.
 inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic
 proofs, we establish a reasoning infrastructure for alpha-equated terms,
 including properties about support, freshness and equality conditions for
 alpha-equated terms. We are also able to automatically derive strong
 induction principles that have the variable convention already built in.
-For this we simplify the earlier automated proofs by using the proof tools
+For this we simplify the earlier automated proofs by using the proving tools
 from the function package~\cite{Krauss09} of Isabelle/HOL.  The method
 behind our specification of general binders is taken from the Ott-tool, but
 we introduce crucial restrictions, and also extensions, so that our
 specifications make sense for reasoning about alpha-equated terms.  The main
 improvement over Ott is that we introduce three binding modes (only one is
 From property \eqref{equivariancedef} and the definition of @{text supp}, we
 can easily deduce that equivariant functions have empty support. There is
 also a similar notion for equivariant relations, say @{text R}, namely the property
 that
-\begin{center}
+\[
 @{text "x R y"} \;\;\textit{implies}\;\; @{text "(\<pi> \<bullet> x) R (\<pi> \<bullet> y)"}
-\end{center}
+\]\smallskip
 Using freshness, the nominal logic work provides us with general means for renaming
 binders.
 \noindent
 \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
 (similarly for $\approx_{\,\textit{list}}$).  It can also relatively easily be
 shown that all three notions of alpha-equivalence coincide, if we only
 abstract a single atom.
 In the rest of this section we are going to show that the alpha-equivalences
-really lead to abstractions where some atoms are bound (more precisely
+really lead to abstractions where some atoms are bound (or more precisely
 removed from the support).  For this we will consider three abstraction
 types that are quotients of the relations
 \begin{equation}
 \begin{array}{r}
 \]\smallskip
 \end{thm}
 \noindent
 In effect, this theorem states that the atoms @{text "as"} are bound in the
-abstraction. As stated earlier, this can be seen as litmus test that our
+abstraction. As stated earlier, this can be seen as a litmus test that our
 Definitions \ref{alphaset}, \ref{alphalist} and \ref{alphares} capture the
 idea of alpha-equivalence relations. Below we will give the proof for the
 first equation of Theorem \ref{suppabs}. The others follow by similar
 arguments. By definition of the abstraction type @{text
 "abs\<^bsub>set\<^esub>"} we have
 @{thm (prem 2) Abs_swap1(1)[where bs="as", no_vars]} then
 @{thm (concl) Abs_swap1(1)[where bs="as", no_vars]}
 \end{lem}
 \begin{proof}
-If @{term "a = b"} the lemma is immediate, since @{term "(a \<rightleftharpoons> b) = 0"}.
+If @{term "a = b"} the lemma is immediate, since @{term "(a \<rightleftharpoons> b)"} is then
+the identity permutation.
 Also in the other case the lemma is straightforward using \eqref{abseqiff}
 and observing that the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) =
-(supp x - as)"}.  We therefore can use the swapping @{term "(a \<rightleftharpoons> b)"}. as
+(supp x - as)"}.  We therefore can use the swapping @{term "(a \<rightleftharpoons> b)"} as
-the permutation fpr the proof obligation.
+the permutation for the proof obligation.
 \end{proof}
 \noindent
 Assuming that @{text "x"} has finite support, this lemma together
 with \eqref{absperm} allows us to show
 \noindent
 This is because for every finite sets of atoms, say @{text "bs"}, we have
 @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
 Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes
-the first equation of Theorem~\ref{suppabs}.
+the first equation of Theorem~\ref{suppabs}. The others are similar.
 Recall the definition of support given in \eqref{suppdef}, and note the difference between
-the support of a `raw' pair and an abstraction
+the support of a raw pair and an abstraction
 \[
 @{term "supp (as, x) = supp as \<union> supp x"}\hspace{15mm}
 @{term "supp (Abs_set as x) = supp x - as"}
 \]\smallskip
 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
-binding clauses and the labels from the types. We also have to invent
+binding clauses and the labels from the types given by the user. We also have to invent
-new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}
+new names for the  types @{text "ty\<^sup>\<alpha>"} and the term-constructors @{text "C\<^sup>\<alpha>"}.
-given by the user. In our implementation we just use the affix `@{text "_raw"}'.
+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
 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{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 the free-atom functions are terminating. From this the function
-package derives an induction principle \cite{Krauss09}.} The second is by a
+package derives an induction principle~\cite{Krauss09}.} The second is by a
 straightforward induction over the rules of @{text "\<approx>ty"}$_{1..n}$ and
 @{text "\<approx>bn"}$_{1..m}$ using the first part.
 \end{proof}
 \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
 \end{equation}\smallskip
 We can also add to our infrastructure cases lemmas and a (mutual)
 induction principle for the types @{text "ty\<AL>"}$_{1..n}$. The cases
 lemmas allow the user to deduce a property @{text "P"} by exhaustively
-analysing how an element in a type, say @{text "ty\<AL>"}$_i$, can be
+analysing how an element of a type, say @{text "ty\<AL>"}$_i$, can be
 constructed (that means one case for each of the term-constructors in @{text
 "ty\<AL>"}$_i\,$). The lifted cases lemma for the type @{text
 "ty\<AL>"}$_i\,$ looks as follows
 \begin{equation}\label{cases}
 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 that example to the following three inference
-rules (the cases lemmas are on the left-hand side; the induction principle
+rules:
-on the right):
 \begin{equation}\label{inductex}\mbox{
 \begin{tabular}{c}
 \multicolumn{1}{@ {\hspace{-5mm}}l}{cases lemmas:}\smallskip\\
 \infer{@{text "P\<^bsub>trm\<^esub>"}}
 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
-any assumptions about the atoms that are bound. One obvious way around this
+any assumptions about the atoms that are bound---for example assuming the variable convention.
+One obvious way around this
 problem is to rename them. Unfortunately, this leads to very clunky proofs
 and makes formalisations grievous experiences (especially in the context of
 multiple bound atoms).
 For the older versions of Nominal Isabelle we described in \cite{Urban08} a
 `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
+line). In order to see how an instantiation for @{text "c"} in the
-principle, then the user can mimic the usual `pencil-and-paper' reasoning
+conclusion `controls' the premises, you have to take into account that
-employing the variable convention about bound and free variables being
+Isabelle/HOL is a typed logic. That means if @{text "c"} is instantiated
-distinct \cite{Urban08}.
+with a pair, for example, then this type-constraint will be propagated to
+the premises. The main point is that if @{text "c"} is instantiated
+appropriately, then the user can mimic the usual `pencil-and-paper'
+reasoning employing the variable convention about bound and free variables
+being distinct \cite{Urban08}.
 In what follows we will show that the weak induction principle in
 \eqref{inductex} implies the strong one \eqref{stronginduct}. This fact was established for
 single binders in \cite{Urban08} by some quite involved, nevertheless
 automated, induction proof. In this paper we simplify the proof by
 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
+infrastructure of the function package will automatically derive the
 stronger induction principle. This way of establishing the stronger induction
 principle is considerably simpler than the earlier work presented \cite{Urban08}.
 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
 \begin{equation}\label{imp}
 @{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
+which we must use in order to infer @{text "P\<^bsub>trm\<^esub>"}. Clearly, we cannot
 use this implication directly, because we have no information whether or not @{text
 "x\<^isub>1"} is fresh for @{text "c"}.  However, we can use Properties
 \ref{supppermeq} and \ref{avoiding} to rename @{text "x\<^isub>1"}: we know
 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 -
 \[
 @{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
+where @{text x} and @{text y} are bound in the term, but are also free
 in the right-hand side of the assignment. We can, however, obtain such a renaming permutation, say
 @{text "\<pi>"}, for the abstraction @{term "Abs_lst (bn_al x\<^isub>1)
 x\<^isub>3"}. As a result we have \mbox{@{term "set (bn_al (\<pi> \<bullet> x\<^isub>1))
 \<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
 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 some atoms that are
 bound and some that are free. An example is @{text "Let\<^sup>\<alpha>"} in
-the example \eqref{letrecs}.  In such cases @{text "(\<pi> \<bullet> x\<^isub>1)
+\eqref{letrecs}.  In such cases @{text "(\<pi> \<bullet> x\<^isub>1)
 \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} does not hold in general. The idea however is
 that @{text "\<pi>"} only renames atoms that become bound. In this way @{text "\<pi>"}
-does not affect @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"}. However, the problem is that the
+does not affect @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"} (which only tracks alpha-equivalence of terms that are not
+under the binder). However, the problem is that the
 permutation operation @{text "\<pi> \<bullet> x\<^isub>1"} applies to all attoms in @{text "x\<^isub>1"}. To avoid this
 we introduce an auxiliary permutation operations, written @{text "_
 \<bullet>\<^bsub>bn\<^esub> _"}, for deep binders that only permutes bound atoms (or
 more precisely the atoms specified by the @{text "bn"}-functions) and leaves
 the other atoms unchanged. Like the functions @{text "fa_bn"}$_{1..m}$, we
-can define these operations over raw terms analysing how the functions @{text
+can define these permutation operations over raw terms analysing how the functions @{text
 "bn"}$_{1..m}$ are defined. Assuming the user specified a clause
 \[
 @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}
 \]\smallskip
 $\bullet$ & @{text "y\<^isub>i \<equiv> \<pi> \<bullet> x\<^isub>i"} otherwise
 \end{tabular}}
 \]\smallskip
 \noindent
-Using again the quotient package  we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} functions to
+Using again the quotient package  we can lift the auxiliary permutation operations
+@{text "_ \<bullet>\<^bsub>bn\<^esub> _"}
 alpha-equated terms. Moreover we can prove the following two properties
 \begin{lem}\label{permutebn}
 Given a binding function @{text "bn\<^sup>\<alpha>"} and auxiliary equivalence @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"}
 then for all @{text "\<pi>"}\smallskip\\
 \end{proof}
 \noindent
 The first property states that a permutation applied to a binding function
 is equivalent to first permuting the binders and then calculating the bound
-atoms. The second states that @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} preserves
+atoms. The second states that @{text "_ \<bullet>\<AL>\<^bsub>bn\<^esub> _"} preserves
 @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"}.  The main point of the auxiliary
 permutation functions is that they allow us to rename just the binders in a
 term, without changing anything else.
 Having the auxiliary permutation function in place, we can now solve all remaining cases.
 \]\smallskip
 \noindent
 hold. Using the first part of Lemma \ref{permutebn}, we can simplify this
 to @{text "set (bn\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1)) #\<^sup>* c"} and
-@{text "[bn\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1)]\<^bsub>list\<^esub>. (\<pi> \<bullet> x\<^isub>2) = [bn\<^sup>\<alpha> x\<^isub>1]\<^bsub>list\<^esub>. x\<^isub>2"}. Since
+\mbox{@{text "[bn\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1)]\<^bsub>list\<^esub>. (\<pi> \<bullet> x\<^isub>2) = [bn\<^sup>\<alpha> x\<^isub>1]\<^bsub>list\<^esub>. x\<^isub>2"}}. Since
-@{text "(\<pi>  \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1) \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} holds by teh second part,
+@{text "(\<pi>  \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1) \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} holds by the second part,
 we can infer that
 \[
 @{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.
+lemma, and we are done.
 Conseqently,  we can discharge all proof-obligations about having covered all
 cases. This completes the proof establishing that the weak induction principles imply
 the strong induction principles. These strong induction principles have proved
 already to be very useful in practice, particularly for proving properties about
 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
+is as expected (that means bound atoms are removed from the support). We
 also showed that our specifications lift from `raw' types to types of
 alpha-equivalence classes. For this we had to establish (automatically) that every
 term-constructor and function defined for `raw' types
 is respectful w.r.t.~alpha-equivalence.
 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 the Core-Haskell language from the Introduction. With the work
-presented in this paper we can define formally this language as shown in
+presented in this paper we can define it formally as shown in
 Figure~\ref{nominalcorehas} and then Nominal Isabelle derives automatically
 a corresponding reasoning infrastructure.
 \begin{figure}[p]
 \begin{boxedminipage}{\linewidth}
 $|$~@{text "bv\<^isub>3 (TVCKCons c cty tl) = (atom c)::(bv\<^isub>3 tl)"}\\
 \end{tabular}
 \end{boxedminipage}
 \caption{A definition for Core-Haskell in Nominal Isabelle. For the moment we
 do not support nested types; therefore we explicitly have to unfold the
-lists @{text "co_lst"}, @{text "assoc_lst"} and so on. Apart from that, the
+lists @{text "co_lst"}, @{text "assoc_lst"} and so on. Apart from that limitation, the
 definition follows closely the original shown in Figure~\ref{corehas}. The
 point of our work is that having made such a definition in Nominal Isabelle,
 one obtains automatically a reasoning infrastructure for Core-Haskell.
 \label{nominalcorehas}}
 \end{figure}

changeset 3025	204a488c71c6
parent 3024	10e476d6f4b8
child 3029	6fd3fc3254ee