nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:2eafd8ed4bbf
+:fd2913415a73
 @{text "S ::= \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. T"}
 \end{array}
 \end{equation}
 \noindent
-and the quantification $\forall$ binds a finite (possibly empty) set of
+and the @{text "\<forall>"}-quantification binds a finite (possibly empty) set of
 type-variables.  While it is possible to implement this kind of more general
 binders by iterating single binders, this leads to a rather clumsy
 formalisation of W. The need of iterating single binders is also one reason
 why Nominal Isabelle and similar theorem provers that only provide
 mechanisms for binding single variables have not fared extremely well with the
 specifications for $\mathtt{let}$s as follows
 %
 \begin{center}
 \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}
 @{text trm} & @{text "::="}  & @{text "\<dots>"}\\
-& @{text "|"}    & @{text "\<LET> a::assn s::trm"}\hspace{4mm}
+& @{text "|"}    & @{text "\<LET> as::assn s::trm"}\hspace{4mm}
-\isacommand{bind} @{text "bn(a)"} \isacommand{in} @{text "s"}\\[1mm]
+\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}\\[1mm]
 @{text assn} & @{text "::="} & @{text "\<ANIL>"}\\
 & @{text "|"}   & @{text "\<ACONS> name trm assn"}
 \end{tabular}
 \end{center}
 \end{center}
 \noindent
 The scope of the binding is indicated by labels given to the types, for
 example @{text "s::trm"}, and a binding clause, in this case
-\isacommand{bind} @{text "bn(a)"} \isacommand{in} @{text "s"}, that states
+\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding
-to bind in @{text s} all the names the function call @{text "bn(a)"} returns.
+clause states to bind in @{text s} all the names the function call @{text
-This style of specifying terms and bindings is heavily inspired by the
+"bn(as)"} returns.  This style of specifying terms and bindings is heavily
-syntax of the Ott-tool \cite{ott-jfp}.
+inspired by the syntax of the Ott-tool \cite{ott-jfp}.
+However, we will not be able to cope with all specifications that are
-However, we will not be able to deal with all specifications that are
 allowed by Ott. One reason is that Ott lets the user to specify ``empty''
 types like
 \begin{center}
 @{text "t ::= t t | \<lambda>x. t"}
 @{text "fv(t\<^isub>1 t\<^isub>2) = fv(t\<^isub>1) \<union> fv(t\<^isub>2)"}\\[1mm]
 @{text "fv(\<lambda>x.t) = fv(t) - {x}"}
 \end{center}
 \noindent
-then with the help of the quotient package we obtain a function @{text "fv\<^sup>\<alpha>"}
+then with the help of the quotient package we can obtain a function @{text "fv\<^sup>\<alpha>"}
 operating on quotients, or alpha-equivalence classes of lambda-terms. This
 lifted function is characterised by the equations
 \begin{center}
 @{text "fv\<^sup>\<alpha>(x) = {x}"}\hspace{10mm}
 The examples we have in mind where our reasoning infrastructure will be
 helpful includes the term language of System @{text "F\<^isub>C"}, also
 known as Core-Haskell (see Figure~\ref{corehas}). This term language
 involves patterns that have lists of type-, coercion- and term-variables,
 all of which are bound in @{text "\<CASE>"}-expressions. One
-difficulty is that each of these variables come with a kind or type
+difficulty is that we do not know in advance how many variables need to
+be bound. Another is that each bound variable comes with a kind or type
 annotation. Representing such binders with single binders and reasoning
 about them in a theorem prover would be a major pain.  \medskip
 \noindent
 {\bf Contributions:}  We provide new definitions for when terms
 Pitts \cite{Pitts03}. This adaptation for Isabelle/HOL is described in
 \cite{HuffmanUrban10} (including proofs). We shall briefly review this work
 to aid the description of what follows.
 Two central notions in the nominal logic work are sorted atoms and
-sort-respecting permutations of atoms. We will use the variables @{text "a,
+sort-respecting permutations of atoms. We will use the letters @{text "a,
 b, c, \<dots>"} to stand for atoms and @{text "p, q, \<dots>"} to stand for
 permutations.  The sorts of atoms can be used to represent different kinds of
-variables, such as the term-, coercion- and type-variables in Core-Haskell,
+variables, such as the term-, coercion- and type-variables in Core-Haskell.
-and it is assumed that there is an infinite supply of atoms for each
+It is assumed that there is an infinite supply of atoms for each
-sort. However, in order to simplify the description, we shall assume in what
+sort. However, in order to simplify the description, we shall restrict ourselves
-follows that there is only one sort of atoms.
+in what follows to only one sort of atoms.
 Permutations are bijective functions from atoms to atoms that are
 the identity everywhere except on a finite number of atoms. There is a
 two-place permutation operation written
 %
 over which the permutation
 acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},
 the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}},
 and the inverse permutation of @{term p} as @{text "- p"}. The permutation
 operation is defined by induction over the type-hierarchy (see \cite{HuffmanUrban10});
-for example as follows for products, lists, sets, functions and booleans:
+for example permutations acting on products, lists, sets, functions and booleans is
+given by:
 %
 \begin{equation}\label{permute}
 \mbox{\begin{tabular}{@ {}cc@ {}}
 \begin{tabular}{@ {}l@ {}}
 @{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\[2mm]
 @{term "supp p"} & = & @{term "{a. p \<bullet> a \<noteq> a}"}
 \end{eqnarray}
 \noindent
 in some cases it can be difficult to establish the support precisely, and
-only give an approximation (see the case for function applications
+only give an approximation (see \eqref{suppfun} above). Reasoning about
-above). Such approximations can be calculated with the notion
+such approximations can be made precise with the notion \emph{supports}, defined
-\emph{supports}, defined as follows
+as follows:
 \begin{defn}
 A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}
 not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.
 \end{defn}
 \noindent
-The main point of this definition is that we can show the following two properties.
+The main point of @{text supports} is that we can establish the following
+two properties.
 \begin{property}\label{supportsprop}
 {\it i)} @{thm[mode=IfThen] supp_is_subset[no_vars]}\\
 {\it ii)} @{thm supp_supports[no_vars]}.
 \end{property}
 Another important notion in the nominal logic work is \emph{equivariance}.
 For a function @{text f}, say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant
-requires that every permutation leaves @{text f} unchanged, that is
+it is required that every permutation leaves @{text f} unchanged, that is
 %
 \begin{equation}\label{equivariancedef}
 @{term "\<forall>p. p \<bullet> f = f"}
 \end{equation}
 @{text "p \<bullet> f = f"} \;\;\;\textit{if and only if}\;\;\;
 @{text "p \<bullet> (f x) = f (p \<bullet> x)"}
 \end{equation}
 \noindent
-From equation \eqref{equivariancedef} and the definition of support shown in
+From property \eqref{equivariancedef} and the definition of @{text supp}, we
-\eqref{suppdef}, we can be easily deduce that an equivariant function has
+can be easily deduce that an equivariant function has empty support.
-empty support.
+Finally, the nominal logic work provides us with convenient means to rename
-Finally, the nominal logic work provides us with elegant means to rename
 binders. While in the older version of Nominal Isabelle, we used extensively
 Property~\ref{swapfreshfresh} for renaming single binders, this property
-proved unwieldy for dealing with multiple binders. For this the following
+proved unwieldy for dealing with multiple binders. For such pinders the
-generalisations turned out to be easier to use.
+following generalisations turned out to be easier to use.
 \begin{property}\label{supppermeq}
 @{thm[mode=IfThen] supp_perm_eq[no_vars]}
 \end{property}
 @{term "supp x \<sharp>* p"}.
 \end{property}
 \noindent
 The idea behind the second property is that given a finite set @{text as}
-of binders (being bound in @{text x} which is ensured by the
+of binders (being bound, or fresh, in @{text x} is ensured by the
 assumption @{term "as \<sharp>* x"}), then there exists a permutation @{text p} such that
-the renamed binders @{term "p \<bullet> as"} avoid the @{text c} (which can be arbitrarily chosen
+the renamed binders @{term "p \<bullet> as"} avoid @{text c} (which can be arbitrarily chosen
-as long as it is finitely supported) and also does not affect anything
+as long as it is finitely supported) and also it does not affect anything
 in the support of @{text x} (that is @{term "supp x \<sharp>* p"}). The last
 fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders
-in @{text x}, because @{term "p \<bullet> x = x"}.
+@{text as} in @{text x}, because @{term "p \<bullet> x = x"}.
 All properties given in this section are formalised in Isabelle/HOL and also
-most of them are described with proofs in \cite{HuffmanUrban10}. In the next
+most of proofs are described in \cite{HuffmanUrban10} to which we refer the
-sections we will make extensively use of these properties for characterising
+reader. In the next sections we will make extensively use of these
-alpha-equivalence in the presence of multiple binders.
+properties in order to define alpha-equivalence in the presence of multiple
+binders.
 *}
 section {* General Binders\label{sec:binders} *}
 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 @{text
 "as"} in the body @{text "x"}.
-The first question we have to answer is when the pairs @{text "(as, x)"} and
+The first question we have to answer is when two pairs @{text "(as, x)"} and
 @{text "(bs, y)"} are alpha-equivalent? (At the moment we are interested in
 the notion of alpha-equivalence that is \emph{not} preserved by adding
 vacuous binders.) To answer this, we identify four conditions: {\it i)}
 given a free-variable function @{text "fv"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
 set"}}, then @{text x} and @{text y} need to have the same set of free
 existentially quantify over this @{text "p"}. Also note that the relation is
 dependent on a free-variable function @{text "fv"} and a relation @{text
 "R"}. The reason for this extra generality is that we will use
 $\approx_{\textit{set}}$ for both ``raw'' terms and alpha-equated terms. In
 the latter case, $R$ will be replaced by equality @{text "="} and we
-will prove that @{text "fv"} is equal to the support of @{text
+will prove that @{text "fv"} is equal to @{text "supp"}.
-x} and @{text y}.
 The definition in \eqref{alphaset} does not make any distinction between the
 order of abstracted variables. If we want this, then we can define alpha-equivalence
 for pairs of the form \mbox{@{text "(as, x)"}} with type @{text "(atom list) \<times> \<beta>"}
 as follows
 \end{center}
 \noindent
 Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and
 \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and
-@{text "({y, x}, y \<rightarrow> x)"} are equal according to $\approx_{\textit{set}}$ and
+@{text "({y, x}, y \<rightarrow> x)"} are alpha-equivalent according to $\approx_{\textit{set}}$ and
 $\approx_{\textit{res}}$ by taking @{text p} to be the swapping @{term "(x \<rightleftharpoons>
 y)"}. In case of @{text "x \<noteq> y"}, then @{text "([x, y], x \<rightarrow> y)"}
 $\not\approx_{\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"} since there is no permutation
 that makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and also
 leaves the type \mbox{@{text "x \<rightarrow> y"}} unchanged. Another example is
 \noindent
 This lemma allows us to use our quotient package and introduce
 new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}
 representing alpha-equivalence classes of pairs. The elements in these types
-we will, respectively, write as:
+will be, respectively, written as:
 \begin{center}
 @{term "Abs as x"} \hspace{5mm}
 @{term "Abs_lst as x"} \hspace{5mm}
 @{term "Abs_res as x"}
 \end{center}
 \noindent
 indicating that a set or list @{text as} is abstracted in @{text x}. We will
 call the types \emph{abstraction types} and their elements
-\emph{abstractions}. The important property we need is a characterisation
+\emph{abstractions}. The important property we need to know is what the
-for the support of abstractions, namely:
+support of abstractions is, namely:
 \begin{thm}[Support of Abstractions]\label{suppabs}
 Assuming @{text x} has finite support, then\\[-6mm]
 \begin{center}
 \begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
 \end{tabular}
 \end{center}
 \end{thm}
 \noindent
-We will show below the first equation as the others
+Below we will show the first equation. The others
 follow similar arguments. By definition of the abstraction type @{text "abs_set"}
 we have
 %
 \begin{equation}\label{abseqiff}
 @{thm (lhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\;
 \begin{lemma}
 @{thm[mode=IfThen] abs_swap1(1)[where bs="as", no_vars]}
 \end{lemma}
 \begin{proof}
-By using \eqref{abseqiff}, this lemma is straightforward when observing that
+This lemma is straightforward by using \eqref{abseqiff} and observing that
-the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}
+the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.
-and that @{text supp} and set difference are equivariant.
+Moreover @{text supp} and set difference are equivariant \cite{HuffmanUrban10}.
 \end{proof}
 \noindent
 This lemma allows us to show
 %
 \noindent
 which by Property~\ref{supportsprop} gives us ``one half'' of
 Thm~\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 taking an abstraction as argument
+function taking an abstraction as argument:
 %
 \begin{center}
 @{thm supp_gen.simps[THEN eq_reflection, no_vars]}
 \end{center}
 \end{equation}
 \noindent
 since for finite sets, @{text "S"}, we have @{thm (concl) supp_finite_atom_set[no_vars]}.
-Finally taking \eqref{halfone} and \eqref{halftwo} together provides us with a proof
+Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes of
-of Theorem~\ref{suppabs}. The point of these properties of abstractions is that we
+Theorem~\ref{suppabs}. This theorem gives us confidence that our
-can define and prove them aconveniently on the Isabelle/HOL level,
+abstractions behave as one expects. To consider first abstractions of the
-but also use them in what follows next when we deal with binding in
+form @{term "Abs as x"} is motivated by the fact that properties about them
-specifications of term-calculi.
+can be conveninetly established at the Isabelle/HOL level.  But we can also
+use when we deal with binding in our term-calculi specifications.
 *}
 section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *}
 text {*
-Our choice of syntax for specifications of term-calculi is influenced by the existing
+Our choice of syntax for specifications is influenced by the existing
 datatype package of Isabelle/HOL \cite{Berghofer99} and by the syntax of the Ott-tool
-\cite{ott-jfp}. A specification is a collection of (possibly mutual
+\cite{ott-jfp}. For us a specification of a term-calculus is a collection of (possibly mutual
 recursive) type declarations, say @{text "ty"}$^\alpha_1$, \ldots,
 @{text ty}$^\alpha_n$, and an associated collection
 of binding functions, say @{text bn}$^\alpha_1$, \ldots, @{text
 bn}$^\alpha_m$. The syntax in Nominal Isabelle for such specifications is
 roughly as follows:
 \end{center}
 \noindent
 whereby some of the @{text ty}$'_{1..l}$ (or their components) are 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}.  The labels annotated on
+corresponding argument a \emph{recursive argument} of @{text "C\<^sup>\<alpha>"}.  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}:
 binders.  Shallow binders are of the form \isacommand{bind}\; {\it label}\;
 \isacommand{in}\; {\it label'} (similar for the other two modes). The
 restriction we impose on shallow binders is that the {\it label} must either
 refer to a type that is an atom type or to a type that is a finite set or
 list of an atom type. Two examples for the use of shallow binders are the
-specification of lambda-terms, where a single name is bound, and of
+specification of lambda-terms, where a single name is bound, and
 type-schemes, where a finite set of names is bound:
 \begin{center}
 \begin{tabular}{@ {}cc@ {}}
 \begin{tabular}{@ {}l@ {\hspace{-1mm}}}
 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
+The corresponding binding functions are expected to return either a set of atoms
 (for \isacommand{bind\_set} and \isacommand{bind\_res}) or a list of atoms
 (for \isacommand{bind}). They can be defined by primitive recursion over the
 corresponding type; the equations must be given in the binding function part of
-the scheme shown in \eqref{scheme}. For example for a calculus containing lets
+the scheme shown in \eqref{scheme}. For example a term-calculus containing lets
-with tuple patterns, you might specify
+with tuple patterns might be specified as:
 \begin{center}
 \begin{tabular}{l}
 \isacommand{nominal\_datatype} @{text trm} =\\
 \hspace{5mm}\phantom{$\mid$}~@{term "Var name"}\\
 \end{center}
 \noindent
 In this specification the function @{text "bn"} determines which atoms of @{text  p} are
 bound in the argument @{text "t"}. Note that in the second last clause the function @{text "atom"}
-coerces a name into the generic atom type of Nominal Isabelle. This allows
+coerces a name into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}. This allows
 us to treat binders of different atom type uniformly.
 As will shortly become clear, we cannot return an atom in a binding function
 that is also bound in the corresponding term-constructor. That means in the
 example above that the term-constructors @{text PVar} and @{text PTup} must not have a
-binding clause.  In the present version of Nominal Isabelle, we also adopted
+binding clause.  In the version of Nominal Isabelle described here, we also adopted
 the restriction from the Ott-tool that binding functions can only return:
 the empty set or empty list (as in case @{text PNil}), a singleton set or singleton
 list containing an atom (case @{text PVar}), or unions of atom sets or appended atom
-lists (case @{text PTup}). This restriction will simplify proofs later on.
+lists (case @{text PTup}). This restriction will simplify definitions and
+proofs later on.
 The most drastic restriction we have to impose on deep binders is that
 we cannot have ``overlapping'' deep binders. Consider for example the
 term-constructors:
 \noindent
 In the first case we bind all atoms from the pattern @{text p} in @{text t}
 and also all atoms from @{text q} in @{text t}. As a result we have no way
 to determine whether the binder came from the binding function @{text
-"bn(p)"} or @{text "bn(q)"}. Similarly in the second case. There the binder
+"bn(p)"} or @{text "bn(q)"}. Similarly in the second case. The reason why
-@{text "bn(p)"} overlaps with the shallow binder @{text x}. The reason why
 we must exclude such specifications is that they cannot be represent by
 the general binders described in Section \ref{sec:binders}. However
 the following two term-constructors are allowed
 \begin{center}
 \noindent
 since there is no overlap of binders.
 Note that in the last example we wrote {\it\isacommand{bind}\;bn(p)\;\isacommand{in}\;p}.
 Whenever such a binding clause is present, we will call the binder \emph{recursive}.
-To see the purpose for this, compare ``plain'' Lets and Let\_recs:
+To see the purpose for such recursive binders, compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s:
 %
 \begin{equation}\label{letrecs}
 \mbox{%
 \begin{tabular}{@ {}l@ {}}
 \isacommand{nominal\_datatype}~@{text "trm ="}\\
 \hspace{5mm}$\mid$~@{text "bn(ACons a t as) = [atom a] @ bn(as)"}\\
 \end{tabular}}
 \end{equation}
 \noindent
-The difference is that with Let we only want to bind the atoms @{text
+The difference is that with @{text Let} we only want to bind the atoms @{text
-"bn(a)"} in the term @{text t}, but with Let\_rec we also want to bind the atoms
+"bn(a)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms
-inside the assignment. This requires recursive binders and also has
+inside the assignment. This difference has consequences for the free-variable
-consequences for the free variable function and alpha-equivalence relation,
+function and alpha-equivalence relation, which we are going to describe in the
-which we are going to explain in the rest of this section.
+rest of this section.
 Having dealt with all syntax matters, the problem now is how we can turn
 specifications into actual type definitions in Isabelle/HOL and then
 establish a reasoning infrastructure for them. Because of the problem
 Pottier and Cheney pointed out, we cannot in general re-arrange arguments of
 The datatype definition can be obtained by stripping off the
 binding clauses and the labels on 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 user. In our implementation we just use an affix @{text "_raw"}.
+given by user. In our implementation we just use the affix @{text "_raw"}.
-For the purpose of the paper we just use the superscript @{text "_\<^sup>\<alpha>"} to indicate
+But for the purpose of this paper, we just use the superscript @{text "_\<^sup>\<alpha>"} to indicate
 that a notion is defined over alpha-equivalence classes and leave it out
 for the corresponding notion defined on the ``raw'' level. So for example
 we have
 \begin{center}
 @{text "ty\<^sup>\<alpha> \<mapsto> ty"} \hspace{2mm}and\hspace{2mm} @{text "C\<^sup>\<alpha> \<mapsto> C"}
 \end{center}
 \noindent
+where the type @{term ty} is the type used in the quotient construction for
+@{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor on the ``raw'' type @{text "ty"}.
 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 indepth description of the datatype package
 in Isabelle/HOL). We then define the user-specified binding
 functions, called @{term "bn_ty"}, by primitive recursion over the corresponding
 \begin{center}
 @{text "fv_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set    \<dots>    fv_ty\<^isub>n :: ty\<^isub>n \<Rightarrow> atom set"}
 \end{center}
 \noindent
-We define them together with auxiliary free variable functions for
+We define them together with auxiliary free-variable functions for
 the binding functions. Given binding functions
 @{text "bn_ty\<^isub>1 \<dots> bn_ty\<^isub>m"} we need to define
 %
 \begin{center}
 @{text "fv_bn_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set  \<dots>  fv_bn_ty\<^isub>m :: ty\<^isub>m \<Rightarrow> atom set"}
 \end{center}
 \noindent
 The reason for this setup is that in a deep binder not all atoms have to be
-bound. While the idea behind these free variable functions is just to
+bound, as we shall see in an example below. While the idea behind these
-collect all atoms that are not bound, because of the rather complicated
+free-variable functions is clear (they just collect all atoms that are not bound),
-binding mechanisms their definitions are somewhat involved.
+because of the rather complicated binding mechanisms their definitions are
+somewhat involved.
 Given a term-constructor @{text "C"} of type @{text ty} with argument types
-\mbox{@{text "ty\<^isub>1 \<dots> ty\<^isub>n"}} and given some binding clauses associated with
+\mbox{@{text "ty\<^isub>1 \<dots> ty\<^isub>n"}}, the function
-this constructor, the function
 @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be the union of the values
-calculated below for each argument.
+calculated next for each argument.
+First we deal with the case that @{text "x\<^isub>i"} is a binder. From the binding clauses,
-First we deal with the case @{text "x\<^isub>i"} is a binder. From the binding clauses,
 we can determine whether the argument is a shallow or deep
 binder, and in the latter case also whether it is a recursive or
 non-recursive binder.
 \begin{center}
 \end{tabular}
 \end{center}
 \noindent
 The first clause states that shallow binders do not contribute to the
-free variables; in the second clause, we have to look up all
+free variables; in the second clause, we have to collect all
-the free variables that are left unbound by the binding function @{text "bn_ty\<^isub>i"}---this
+variables that are left unbound by the binding function @{text "bn_ty\<^isub>i"}---this
 is done with function @{text "fv_bn_ty\<^isub>i"}; in the third clause, since the
 binder is recursive, we need to bind all variables specified by
 @{text "bn_ty\<^isub>i"}---therefore we subtract @{text "bn_ty\<^isub>i x\<^isub>i"} from the free
 variables of @{text "x\<^isub>i"}.
 In case the argument is \emph{not} a binder, we need to consider
 whether the @{text "x\<^isub>i"} is the body of one or more binding clauses.
 In this case we first calculate the set @{text "bnds"} as follows:
-either the binders are all shallow or there is a single deep binder.
+either the corresponding binders are all shallow or there is a single deep binder.
 In the former case we take @{text bnds} to be the union of all shallow
 binders; in the latter case, we just take the set of atoms specified by the
 binding function. The value for @{text "x\<^isub>i"} is then given by:
-\begin{center}
+\begin{equation}\label{deepbody}
+\mbox{%
 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
 $\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\
 $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\
 $\bullet$ & @{text "(atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\
 $\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is one of the raw datatypes
 corresponding to the types specified by the user\\
 %  $\bullet$ & @{text "(fv\<^isup>\<alpha> x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a defined nominal datatype
-%     with a free variable function @{text "fv\<^isup>\<alpha>"}\\
+%     with a free-variable function @{text "fv\<^isup>\<alpha>"}\\
 $\bullet$ & @{term "{}"} otherwise
-\end{tabular}
+\end{tabular}}
-\end{center}
+\end{equation}
 \noindent
-Like the function @{text atom}, @{text "atoms"} coerces a set of atoms to the generic atom type.
+Like the coercion function @{text atom} used above, @{text "atoms as"} coerces
+the set @{text as} to the generic atom type.
 It is defined as @{text "atom as \<equiv> {atom a | a \<in> as}"}.
 The last case we need to consider is when @{text "x\<^isub>i"} is neither
 a binder nor a body of an abstraction. In this case it is defined
-as above, except that we do not subtract the set @{text bnds}.
+as in \eqref{deepbody}, except that we do not need to subtract the
+set @{text bnds}.
-Next, we need to define a free variable function @{text "fv_bn_ty\<^isub>i"} for
+Next, we need to define a free-variable function @{text "fv_bn_ty\<^isub>i"} for
 each binding function @{text "bn_ty\<^isub>i"}. The idea behind this
 function is to compute the set of free atoms that are not bound by
-the binding function. Because of the restrictions we imposed on the
+@{text "bn_ty\<^isub>i"}. Because of the restrictions we imposed on the
 form of binding functions, this can be done automatically by recursively
 building up the the set of free variables from the arguments that are
 not bound. Let us assume one clause of the binding function is
 @{text "bn_ty\<^isub>i (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then @{text "fv_bn_ty\<^isub>i"} is the
 union of the values calculated for @{text "x\<^isub>j"} of type @{text "ty\<^isub>j"}
 as follows:
 \begin{center}
 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
 \multicolumn{2}{l}{@{text "x\<^isub>j"} occurs in @{text "rhs"}:}\\
-$\bullet$ & @{term "{}"} provided @{term "x\<^isub>j"} is an atom,
+$\bullet$ & @{term "{}"} provided @{term "x\<^isub>j"} is a single atom,
 atom list or atom set\\
 $\bullet$ & @{text "fv_bn_ty\<^isub>j x\<^isub>j"} in case @{text "rhs"} contains the
 recursive call @{text "bn_ty\<^isub>j x\<^isub>j"}\\[1mm]
 %
 \multicolumn{2}{l}{@{text "x\<^isub>j"} does not occur in @{text "rhs"}:}\\
 $\bullet$ & @{text "atoms x\<^isub>j"} provided @{term "x\<^isub>j"} is a set of atoms\\
 $\bullet$ & @{term "atoms (set x\<^isub>j)"} provided @{term "x\<^isub>j"} is a list of atoms\\
 $\bullet$ & @{text "fv_ty\<^isub>j x\<^isub>j"} provided @{term "ty\<^isub>j"} is one of the raw
 types corresponding to the types specified by the user\\
 %  $\bullet$ & @{text "fv_ty\<^isup>\<alpha> x\<^isub>j - bnds"} provided @{term "x\<^isub>j"}  is not in @{text "rhs"}
-%     and is an existing nominal datatype with the free variable function @{text "fv\<^isup>\<alpha>"}\\
+%     and is an existing nominal datatype with the free-variable function @{text "fv\<^isup>\<alpha>"}\\
 $\bullet$ & @{term "{}"} otherwise
 \end{tabular}
 \end{center}
 \noindent
-To see how these definitions work, let us consider the term-constructors
+To see how these definitions work, let us consider again the term-constructors
-for @{text "Let"} and @{text "Let_rec"} from example shown in \eqref{letrecs}.
+@{text "Let"} and @{text "Let_rec"} from example shown in \eqref{letrecs}.
 For this specification we need to define three functions, namely
-@{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"}.
+@{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"}. They are as follows:
 %
 \begin{center}
 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
 @{text "fv\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "fv\<^bsub>bn\<^esub> as \<union> (fv\<^bsub>trm\<^esub> t - set (bn as))"}\\
 @{text "fv\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} &\\
 \noindent
 Since there are no binding clauses for the term-constructors @{text ANil}
 and @{text "ACons"}, the corresponding free-variable function @{text
 "fv\<^bsub>assn\<^esub>"} returns all atoms occuring in an assignment. The
-binding happens in @{text Let} and @{text "Let_rec"}. In the first clause we
+binding only takes place in @{text Let} and @{text "Let_rec"}. In the @{text
-want to bind all atoms given by @{text "set (bn as)"} in @{text
+"Let"}-clause we want to bind all atoms given by @{text "set (bn as)"} in
-t}. Therefore we have to subtract @{text "set (bn as)"} from @{text
+@{text t}. Therefore we have to subtract @{text "set (bn as)"} from @{text
 "fv\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are
 free in @{text "as"}. This is what the purpose of the function @{text
 "fv\<^bsub>bn\<^esub>"} is.  In contrast, in @{text "Let_rec"} we have a
-recursive binder where we want to also bind all occurences of atoms inside
+recursive binder where we want to also bind all occurences of the atoms
-@{text "as"}. Therefore we have to subtract @{text "set (bn as)"} from
+@{text "bn as"} inside @{text "as"}. Therefore we have to subtract @{text
-@{text "fv\<^bsub>assn\<^esub> as"}. Similarly for @{text
+"set (bn as)"} from @{text "fv\<^bsub>assn\<^esub> as"}, as well as from
-"fv\<^bsub>trm\<^esub> t - bn as"}. An interesting point in this example is
+@{text "fv\<^bsub>trm\<^esub> t"}. An interesting point in this example is
 that an assignment ``alone'' does not have any bound variables. Only in the
-context of a @{text Let} pr @{text "Let_rec"} will some atoms occuring in an
+context of a @{text Let} or @{text "Let_rec"} will some atoms become bound
-assignment become bound. This is a phenomenon that has also been pointed out
+(teh term-constructors that have binding clauses).  This is a phenomenon
-in \cite{ott-jfp}.
+that has also been pointed out in \cite{ott-jfp}.
-We then define the alpha equivalence relations. For the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}
+Next we define alpha-equivalence realtions for the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}. We call them
-we need to define
+@{text "\<approx>ty\<^isub>1 \<dots> \<approx>ty\<^isub>n"}. Like with the free-variable functions,
+we also need to  define auxiliary alpha-equivalence relations for the binding functions.
-\begin{center}
+Say we have @{text "bn_ty\<^isub>1 \<dots> bn_ty\<^isub>m"}, we also define @{text "\<approx>bn_ty\<^isub>1 \<dots> \<approx>bn_ty\<^isub>n"}.
-@{text "\<approx>\<^isub>1 :: ty\<^isub>1 \<Rightarrow> ty\<^isub>1 \<Rightarrow> bool \<dots> \<approx>\<^isub>n :: ty\<^isub>n \<Rightarrow> ty\<^isub>n \<Rightarrow> bool"}
-\end{center}
+The relations are inductively defined predicates, whose clauses have
+conclusions of the form  @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"} (let us assume
-\noindent
+@{text C} is of type @{text ty} and its arguments are specified as @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}).
-together with the auxiliary equivalences for binding functions. Given binding
+The task is to specify what the premises of these clauses are. For this we
-functions for types @{text "bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> \<dots> \<dots> bn\<^isub>m :: ty\<^isub>i\<^isub>m \<Rightarrow> \<dots>"} we need to define
+consider the pairs @{text "(x\<^isub>i, y\<^isub>i)"} which necesarily must have the same type, say
-\begin{center}
+@{text "ty\<^isub>i"}. For each of these pairs we calculate a premise as follows.
-@{text "\<approx>bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> ty\<^isub>i\<^isub>1 \<Rightarrow> bool \<dots> \<approx>bn\<^isub>n :: ty\<^isub>i\<^isub>m \<Rightarrow> ty\<^isub>i\<^isub>m \<Rightarrow> bool"}
-\end{center}
+\begin{center}
+\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-Given a term-constructor @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, of a type @{text ty}, two instances
+\multicolumn{2}{l}{@{text "x\<^isub>i"} is a binder:}\\
+$\bullet$ & @{text "True"} provided @{text "x\<^isub>i"} is a shallow binder\\
+$\bullet$ & @{text "x\<^isub>i \<approx>bn_ty\<^isub>i y\<^isub>i"} provided @{text "x\<^isub>i"} is a deep
+non-recursive binder\\
+$\bullet$ & @{text "True"} provided @{text "x\<^isub>i"} is a deep
+recursive binder\\
+\end{tabular}
+\end{center}
+TODO BELOW
+\begin{center}
+\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
+\multicolumn{2}{l}{@{text "x\<^isub>i"} is a body where the binding clause has mode \isacommand{bind}:}\\
+$\bullet$ & @{text "\<exists>p. (bnds_x\<^isub>i, x\<^isub>i) \<approx>lst (\<approx>ty\<^isub>i) fv_ty\<^isub>i p (bnds_y\<^isub>i, y\<^isub>j)"}
+provided @{text "x\<^isub>i"} has only shallow binders; in this case @{text "bnds_x\<^isub>i"} is the
+union of all these shallow binders (similarly for @{text "bnds_y\<^isub>i"}\\
+$\bullet$ & @{text "\<exists>p. (bn_ty\<^isub>j x\<^isub>j, x\<^isub>i) \<approx>lst (\<approx>ty\<^isub>i) fv_ty\<^isub>i p (bn_ty y\<^isub>j, y\<^isub>i)"}
+provided @{text "x\<^isub>i"} is a body with a deep non-recursive binder @{text x\<^isub>j}
+(similarly @{text "y\<^isub>j"} is the deep non-recursive binder for @{text "y\<^isub>i"})\\
+$\bullet$ & @{text "\<exists>p (bn_ty\<^isub>i x\<^isub>i, (x\<^isub>j, x\<^isub>n)) \<approx>lst R fvs \<pi> (bn\<^isub>m y\<^isub>j, (y\<^isub>j, y\<^isub>n))"}
+provided @{text "x\<^isub>j"} is a deep recursive binder with the auxiliary binding
+function @{text "bn\<^isub>m"} and permutation @{text "\<pi>"}, @{term "fvs"} is a compound
+free variable function returning the union of appropriate @{term "fv_ty\<^isub>x"} and
+@{term "R"} is the composition of equivalence relations @{text "\<approx>"} and @{text "\<approx>\<^isub>n"}\\
+$\bullet$ & @{text "x\<^isub>j"} has a deep recursive binding\\
+$\bullet$ & @{text "({x\<^isub>n}, x\<^isub>j) \<approx>gen R fv_ty \<pi> ({y\<^isub>n}, y\<^isub>j)"} provided @{text "x\<^isub>j"} has
+a shallow binder @{text "x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the
+alpha-equivalence for @{term "x\<^isub>j"}
+and @{term "fv_ty"} is the free-variable function for @{term "x\<^isub>j"}\\
+$\bullet$ & @{text "(bn\<^isub>m x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (bn\<^isub>m y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>j"}
+has a deep non-recursive binder @{text "bn\<^isub>m x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the
+alpha-equivalence for @{term "x\<^isub>j"}
+and @{term "fv_ty"} is the free-variable function for @{term "x\<^isub>j"}\\
+$\bullet$ & @{text "x\<^isub>j \<approx>\<^isub>j y\<^isub>j"} provided @{term "x\<^isub>j"} is one of the types being
+defined\\
+$\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} otherwise\\
+\end{tabular}
+\end{center}
+, of a type @{text ty}, two instances
 of this constructor are alpha-equivalent @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx> C y\<^isub>1 \<dots> y\<^isub>n"} if there
 exist permutations @{text "\<pi>\<^isub>1 \<dots> \<pi>\<^isub>p"} (one for each bound argument) such that
 the conjunction of equivalences defined below for each argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} holds.
 For an argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} this holds if:
-\begin{center}
-\begin{tabular}{cp{7cm}}
-$\bullet$ & @{text "x\<^isub>j"} is a shallow binder\\
-$\bullet$ & @{text "x\<^isub>j \<approx>bn\<^isub>m y\<^isub>j"} provided @{text "x\<^isub>j"} is a deep non-recursive binder
-with the auxiliary binding function @{text "bn\<^isub>m"}\\
-$\bullet$ & @{term "(bn\<^isub>m x\<^isub>j, (x\<^isub>j, x\<^isub>n)) \<approx>gen R fvs \<pi> (bn\<^isub>m y\<^isub>j, (y\<^isub>j, y\<^isub>n))"}
-provided @{term "x\<^isub>j"} is a deep recursive binder with the auxiliary binding
-function @{text "bn\<^isub>m"} and permutation @{text "\<pi>"}, @{term "fvs"} is a compound
-free variable function returning the union of appropriate @{term "fv_ty\<^isub>x"} and
-@{term "R"} is the composition of equivalence relations @{text "\<approx>"} and @{text "\<approx>\<^isub>n"}\\
-$\bullet$ & @{text "x\<^isub>j"} has a deep recursive binding\\
-$\bullet$ & @{term "({x\<^isub>n}, x\<^isub>j) \<approx>gen R fv_ty \<pi> ({y\<^isub>n}, y\<^isub>j)"} provided @{text "x\<^isub>j"} has
-a shallow binder @{text "x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the
-alpha-equivalence for @{term "x\<^isub>j"}
-and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\
-$\bullet$ & @{term "(bn\<^isub>m x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (bn\<^isub>m y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>j"}
-has a deep non-recursive binder @{text "bn\<^isub>m x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the
-alpha-equivalence for @{term "x\<^isub>j"}
-and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\
-$\bullet$ & @{text "x\<^isub>j \<approx>\<^isub>j y\<^isub>j"} provided @{term "x\<^isub>j"} is one of the types being
-defined\\
-$\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} otherwise\\
-\end{tabular}
-\end{center}
 The alpha-equivalence relations for binding functions are similar to the alpha-equivalences
 for their respective types, the difference is that they ommit checking the arguments that
 are bound. We assumed that there are no bindings in the type on which the binding function
 is defined so, there are no permutations involved. For a binding function clause

changeset 1727	fd2913415a73
parent 1726	2eafd8ed4bbf
child 1728	9bbf2a1f9b3f