nominal2: comparison LMCS-Paper/Paper.thy

equal deleted inserted replaced

-:02d98590454d
+:c6af56de923d
 \[
 \mbox{\begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}ll}
 @{text trm} & @{text "::="}  & @{text "\<dots>"} \\
 & @{text "|"}    & @{text "\<LET>  as::assn  s::trm"}\hspace{2mm}
-\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}\\[1mm]
+\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text "s"}\\[1mm]
 @{text assn} & @{text "::="} & @{text "\<ANIL>"}\\
 &  @{text "|"}  & @{text "\<ACONS>  name  trm  assn"}
 \end{tabular}}
 \]\smallskip
 \]\smallskip
 \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(as)"} \isacommand{in} @{text "s"}. This binding
+\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding
 clause states that all the names the function @{text "bn(as)"} returns
 should be bound in @{text s}.  This style of specifying terms and bindings
 is heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}. Our work
 extends Ott in several aspects: one is that we support three binding
 modes---Ott has only one, namely the one where the order of binders matters.
 While often the support of an object can be relatively easily
 described, for example for atoms, products, lists, function applications,
 booleans and permutations as follows
-\[\mbox{
+\begin{equation}\label{supps}\mbox{
 \begin{tabular}{c@ {\hspace{10mm}}c}
 \begin{tabular}{rcl}
 @{term "supp a"} & $=$ & @{term "{a}"}\\
 @{term "supp (x, y)"} & $=$ & @{term "supp x \<union> supp y"}\\
 @{term "supp []"} & $=$ & @{term "{}"}\\
 @{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp f \<union> supp x"}\\
 @{term "supp b"} & $=$ & @{term "{}"}\\
 @{term "supp \<pi>"} & $=$ & @{term "{a. \<pi> \<bullet> a \<noteq> a}"}
 \end{tabular}
 \end{tabular}}
-\]\smallskip
+\end{equation}\smallskip
 \noindent
 in some cases it can be difficult to characterise the support precisely, and
 only an approximation can be established (as for function applications
 above). Reasoning about such approximations can be simplified with the
 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
 @{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 use the other
+is equivalent with @{term "supp \<pi> \<sharp>* x"}, which means we could also formulate
-`direction' in Propositions \ref{supppermeq} and \ref{avoiding}.
+Propositions \ref{supppermeq} and \ref{avoiding} in the other `direction', however the
+reasoning infrastructure of Nominal Isabelle is set up so that it provides more
+automation for the original formulation.
 Most properties given in this section are described in detail in \cite{HuffmanUrban10}
 and all are formalised in Isabelle/HOL. In the next sections we will make
 use of these properties in order to define alpha-equivalence in
 the presence of multiple binders.
 relations and equivariant.
 \begin{lem}\label{alphaeq}
 The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$
 and $\approx_{\,\textit{abs\_set+}}$ are equivalence relations and equivariant.
-%, and if
-%@{term "abs_set (as, x) (bs, y)"} then also
-%@{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"} (similarly for the other two relations).
 \end{lem}
 \begin{proof}
 Reflexivity is by taking @{text "\<pi>"} to be @{text "0"}. For symmetry we have
 a permutation @{text "\<pi>"} and for the proof obligation take @{term "- \<pi>"}. In case
 of transitivity, we have two permutations @{text "\<pi>\<^isub>1"} and @{text "\<pi>\<^isub>2"}, and for the
 proof obligation use @{text "\<pi>\<^isub>1 + \<pi>\<^isub>2"}. Equivariance means
-@{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"} holds provided
+@{term "abs_set (\<pi> \<bullet> as, \<pi> \<bullet> x) (\<pi> \<bullet> bs, \<pi> \<bullet> y)"} holds provided
-@{term "abs_set (as, x) (bs, y)"}.
+@{term "abs_set (as, x) (bs, y)"}. To show this, we need to unfold the
+definitions and `pull out' the permutations, which is possible since all
+operators, such as @{text "#\<^sup>*, -, set"} and @{text "supp"}, are equivariant
+(see \cite{HuffmanUrban10}).
 \end{proof}
 \noindent
 This lemma allows us to use our quotient package for introducing
 new types @{text "\<beta> abs\<^bsub>set\<^esub>"}, @{text "\<beta> abs\<^bsub>set+\<^esub>"} and @{text "\<beta> abs\<^bsub>list\<^esub>"}
 \end{array}
 \]\smallskip
 \end{thm}
 \noindent
-This theorem states that the bound names do not appear in the support.
+In effect, this theorem states that the bound names do not appear in the support
-Below we will show the first equation. The others follow by similar
+of abstractions. This can be seen as test that our Definitions \ref{alphaset}, \ref{alphalist}
+and \ref{alphares} capture the idea of alpha-equivalence relations.
+Below we will show 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
 \begin{equation}\label{abseqiff}
-@{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\;
+@{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\;\text{if and only if}\;\;\;
 @{term "\<exists>\<pi>. alpha_set (as, x) equal supp \<pi> (bs, y)"}
 \end{equation}\smallskip
 \noindent
 and also
 \eqref{permute} and alpha-equivalence being equivariant
 (see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show
 the following lemma about swapping two atoms in an abstraction.
 \begin{lem}
-@{thm[mode=IfThen] Abs_swap1(1)[where bs="as", no_vars]}
+If @{thm (prem 1) Abs_swap1(1)[where bs="as", no_vars]} and
+@{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}
 This lemma is straightforward using \eqref{abseqiff} and observing that
 the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.
-Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}).
 \end{proof}
 \noindent
 Assuming that @{text "x"} has finite support, this lemma together
 with \eqref{absperm} allows us to show
 \begin{equation}\label{halfone}
 @{thm Abs_supports(1)[no_vars]}
-\end{equation}
+\end{equation}\smallskip
 \noindent
 which by Property~\ref{supportsprop} gives us ``one half'' of
 Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish
 it, we use a trick from \cite{Pitts04} and first define an auxiliary
-function @{text aux}, taking an abstraction as argument:
+function @{text aux}, taking an abstraction as argument
-@{thm supp_set.simps[THEN eq_reflection, no_vars]}.
+\[
+@{thm supp_set.simps[THEN eq_reflection, no_vars]}
+\]\smallskip
+\noindent
 Using the second equation in \eqref{equivariance}, we can show that
-@{text "aux"} is equivariant (since @{term "p \<bullet> (supp x - as) = (supp (p \<bullet> x)) - (p \<bullet> as)"})
+@{text "aux"} is equivariant (since @{term "\<pi> \<bullet> (supp x - as) = (supp (\<pi> \<bullet> x)) - (\<pi> \<bullet> as)"})
 and therefore has empty support.
 This in turn means
-\begin{center}
+\[
-@{term "supp (supp_gen (Abs_set as x)) \<subseteq> supp (Abs_set as x)"}
+@{term "supp (supp_set (Abs_set as x)) \<subseteq> supp (Abs_set as x)"}
-\end{center}
+\]\smallskip
 \noindent
-using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set,
+using fact about function applications in \eqref{supps}. Assuming
-we further obtain
+@{term "supp x - as"} is a finite set, we further obtain
 \begin{equation}\label{halftwo}
 @{thm (concl) Abs_supp_subset1(1)[no_vars]}
-\end{equation}
+\end{equation}\smallskip
 \noindent
-since for finite sets of atoms, @{text "bs"}, we have
+since 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
 Theorem~\ref{suppabs}.
-The method of first considering abstractions of the
+The method of first considering abstractions of the form @{term "Abs_set as
-form @{term "Abs_set as x"} etc is motivated by the fact that
+x"} etc is motivated by the fact that we can conveniently establish at the
-we can conveniently establish  at the Isabelle/HOL level
+Isabelle/HOL level properties about them.  It would be extremely laborious
-properties about them.  It would be
+to write custom ML-code that derives automatically such properties for every
-laborious to write custom ML-code that derives automatically such properties
+term-constructor that binds some atoms. Also the generality of the
-for every term-constructor that binds some atoms. Also the generality of
+definitions for alpha-equivalence will help us in the next sections.
-the definitions for alpha-equivalence will help us in the next sections.
 *}
 section {* Specifying General Bindings\label{sec:spec} *}
 text {*
 \isacommand{where}\\
 \raisebox{2mm}{$\ldots$}\\[-2mm]
 \end{tabular}}
 \end{cases}$\\
 \end{tabular}}
-\end{equation}
+\end{equation}\smallskip
 \noindent
-Every type declaration @{text ty}$^\alpha_{1..n}$ consists of a collection of
+Every type declaration @{text ty}$^\alpha_{1..n}$ consists of a collection
-term-constructors, each of which comes with a list of labelled
+of term-constructors, each of which comes with a list of labelled types that
-types that stand for the types of the arguments of the term-constructor.
+stand for the types of the arguments of the term-constructor.  For example a
-For example a term-constructor @{text "C\<^sup>\<alpha>"} might be specified with
+term-constructor @{text "C\<^sup>\<alpha>"} might be specified with
-\begin{center}
+\[
-@{text "C\<^sup>\<alpha> label\<^isub>1::ty"}$'_1$ @{text "\<dots> label\<^isub>l::ty"}$'_l\;\;$  @{text "binding_clauses"}
+@{text "C\<^sup>\<alpha> label\<^isub>1::ty"}\mbox{$'_1$} @{text "\<dots> label\<^isub>l::ty"}\mbox{$'_l\;\;$}  @{text "binding_clauses"}
-\end{center}
+\]\smallskip
 \noindent
-whereby some of the @{text ty}$'_{1..l}$ (or their components)
+whereby some of the @{text ty}$'_{1..l}$ (or their components) can be
-can be contained
+contained in the collection of @{text ty}$^\alpha_{1..n}$ declared in
-in the collection of @{text ty}$^\alpha_{1..n}$ declared in
+\eqref{scheme}. In this case we will call the corresponding argument a
-\eqref{scheme}.
+\emph{recursive argument} of @{text "C\<^sup>\<alpha>"}. The types of such
-In this case we will call the corresponding argument a
+recursive arguments need to satisfy a ``positivity'' restriction, which
-\emph{recursive argument} of @{text "C\<^sup>\<alpha>"}.
+ensures that the type has a set-theoretic semantics (see
-The types of such recursive
+\cite{Berghofer99}).  The labels annotated on the types are optional. Their
-arguments need to satisfy a  ``positivity''
+purpose is to be used in the (possibly empty) list of \emph{binding
-restriction, which ensures that the type has a set-theoretic semantics
+clauses}, which indicate the binders and their scope in a term-constructor.
-\cite{Berghofer99}.
+They come in three \emph{modes}:
-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
+\[\mbox{
-and their scope in a term-constructor.  They come in three \emph{modes}:
-%
-\begin{center}
 \begin{tabular}{@ {}l@ {}}
-\isacommand{bind} {\it binders} \isacommand{in} {\it bodies}\;\;\;\,
+\isacommand{binds} {\it binders} \isacommand{in} {\it bodies}\\
-\isacommand{bind (set)} {\it binders} \isacommand{in} {\it bodies}\;\;\;\,
+\isacommand{binds (set)} {\it binders} \isacommand{in} {\it bodies}\\
-\isacommand{bind (set+)} {\it binders} \isacommand{in} {\it bodies}
+\isacommand{binds (set+)} {\it binders} \isacommand{in} {\it bodies}
-\end{tabular}
+\end{tabular}}
-\end{center}
+\]\smallskip
-%
 \noindent
-The first mode is for binding lists of atoms (the order of binders matters);
+The first mode is for binding lists of atoms (the order of bound atoms
-the second is for sets of binders (the order does not matter, but the
+matters); the second is for sets of binders (the order does not matter, but
-cardinality does) and the last is for sets of binders (with vacuous binders
+the cardinality does) and the last is for sets of binders (with vacuous
-preserving alpha-equivalence). As indicated, the labels in the ``\isacommand{in}-part'' of a binding
+binders preserving alpha-equivalence). As indicated, the labels in the
-clause will be called \emph{bodies}; the
+``\isacommand{in}-part'' of a binding clause will be called \emph{bodies};
-``\isacommand{bind}-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.
+Ott, we allow multiple labels in binders and bodies.  For example we allow
-For example we allow
 binding clauses of the form:
-\begin{center}
+\[\mbox{
 \begin{tabular}{@ {}ll@ {}}
 @{text "Foo\<^isub>1 x::name y::name t::trm s::trm"} &
-\isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}\\
+\isacommand{binds} @{text "x y"} \isacommand{in} @{text "t s"}\\
 @{text "Foo\<^isub>2 x::name y::name t::trm s::trm"} &
-\isacommand{bind} @{text "x y"} \isacommand{in} @{text "t"},
+\isacommand{binds} @{text "x y"} \isacommand{in} @{text "t"},
-\isacommand{bind} @{text "x y"} \isacommand{in} @{text "s"}\\
+\isacommand{binds} @{text "x y"} \isacommand{in} @{text "s"}\\
-\end{tabular}
+\end{tabular}}
-\end{center}
+\]\smallskip
 \noindent
-Similarly for the other binding modes.
+Similarly for the other binding modes. Interestingly, in case of
-Interestingly, in case of \isacommand{bind (set)}
+\isacommand{binds (set)} and \isacommand{binds (set+)} the binding clauses
-and \isacommand{bind (set+)} the binding clauses above will make a difference to the semantics
+above will make a difference to the semantics of the specifications (the
-of the specifications (the corresponding alpha-equivalence will differ). We will
+corresponding alpha-equivalence will differ). We will show this later with
-show this later with an example.
+an example.
-There are also some restrictions we need to impose on our binding clauses in comparison to
-the ones of Ott. The
+There are also some restrictions we need to impose on our binding clauses in
-main idea behind these restrictions is that we obtain a sensible notion of
+comparison to the ones of Ott. The main idea behind these restrictions is
-alpha-equivalence where it is ensured that within a given scope an
+that we obtain a sensible notion of alpha-equivalence where it is ensured
-atom occurrence cannot be both bound and free at the same time.  The first
+that within a given scope an atom occurrence cannot be both bound and free
-restriction is that a body can only occur in
+at the same time.  The first restriction is that a body can only occur in
 \emph{one} binding clause of a term constructor (this ensures that the bound
-atoms of a body cannot be free at the same time by specifying an
+atoms of a body cannot be free at the same time by specifying an alternative
-alternative binder for the same body).
+binder for the same body).
-For binders we distinguish between
+For binders we distinguish between \emph{shallow} and \emph{deep} binders.
-\emph{shallow} and \emph{deep} binders.  Shallow binders are just
+Shallow binders are just labels. The restriction we need to impose on them
-labels. The restriction we need to impose on them is that in case of
+is that in case of \isacommand{binds (set)} and \isacommand{binds (set+)} the
-\isacommand{bind (set)} and \isacommand{bind (set+)} the labels must either
+labels must either refer to atom types or to sets of atom types; in case of
-refer to atom types or to sets of atom types; in case of \isacommand{bind}
+\isacommand{binds} the labels must refer to atom types or lists of atom
-the labels must refer to atom types or lists of atom types. Two examples for
+types. Two examples for the use of shallow binders are the specification of
-the use of shallow binders are the specification of lambda-terms, where a
+lambda-terms, where a single name is bound, and type-schemes, where a finite
-single name is bound, and type-schemes, where a finite set of names is
+set of names is bound:
-bound:
+\[\mbox{
-\begin{center}
+\begin{tabular}{@ {}c@ {\hspace{5mm}}c@ {}}
-\begin{tabular}{@ {}c@ {\hspace{7mm}}c@ {}}
 \begin{tabular}{@ {}l}
 \isacommand{nominal\_datatype} @{text lam} $=$\\
 \hspace{2mm}\phantom{$\mid$}~@{text "Var name"}\\
 \hspace{2mm}$\mid$~@{text "App lam lam"}\\
-\hspace{2mm}$\mid$~@{text "Lam x::name t::lam"}~~\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
+\hspace{2mm}$\mid$~@{text "Lam x::name t::lam"}\hspace{3mm}%
+\isacommand{binds} @{text x} \isacommand{in} @{text t}\\
 \end{tabular} &
 \begin{tabular}{@ {}l@ {}}
 \isacommand{nominal\_datatype}~@{text ty} $=$\\
 \hspace{5mm}\phantom{$\mid$}~@{text "TVar name"}\\
 \hspace{5mm}$\mid$~@{text "TFun ty ty"}\\
-\isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}~~%
+\isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}\hspace{3mm}%
-\isacommand{bind (set+)} @{text xs} \isacommand{in} @{text T}\\
+\isacommand{binds (set+)} @{text xs} \isacommand{in} @{text T}\\
 \end{tabular}
-\end{tabular}
+\end{tabular}}
-\end{center}
+\]\smallskip
 \noindent
 In these specifications @{text "name"} refers to an atom type, and @{text
-"fset"} to the type of finite sets.
+"fset"} to the type of finite sets.  Note that for @{text lam} it does not
-Note that for @{text lam} it does not matter which binding mode we use. The
+matter which binding mode we use. The reason is that we bind only a single
-reason is that we bind only a single @{text name}. However, having
+@{text name}. However, having \isacommand{binds (set)} or \isacommand{binds}
-\isacommand{bind (set)} or \isacommand{bind} in the second case makes a
+in the second case makes a difference to the semantics of the specification
-difference to the semantics of the specification (which we will define in the next section).
+(which we will define in the next section).
 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{bind (set)} and
+expected to return either a set of atoms (for \isacommand{binds (set)} and
-\isacommand{bind (set+)}) or a list of atoms (for \isacommand{bind}). They can
+\isacommand{binds (set+)}) or a list of atoms (for \isacommand{binds}). They need
-be defined by recursion over the corresponding type; the equations
+to be defined by recursion over the corresponding type; the equations
 must be given in the binding function part of the scheme shown in
 \eqref{scheme}. For example a term-calculus containing @{text "Let"}s with
 tuple patterns might be specified as:
-%
 \begin{equation}\label{letpat}
 \mbox{%
 \begin{tabular}{l}
 \isacommand{nominal\_datatype} @{text trm} $=$\\
 \hspace{5mm}\phantom{$\mid$}~@{term "Var name"}\\
 \hspace{5mm}$\mid$~@{term "App trm trm"}\\
 \hspace{5mm}$\mid$~@{text "Lam x::name t::trm"}
-\;\;\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
+\;\;\isacommand{binds} @{text x} \isacommand{in} @{text t}\\
 \hspace{5mm}$\mid$~@{text "Let p::pat trm t::trm"}
-\;\;\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}\\
+\;\;\isacommand{binds} @{text "bn(p)"} \isacommand{in} @{text t}\\
-\isacommand{and} @{text pat} $=$
+\isacommand{and} @{text pat} $=$\\
-@{text PNil}
+\hspace{5mm}\phantom{$\mid$}~@{text PNil}\\
-$\mid$~@{text "PVar name"}
+\hspace{5mm}$\mid$~@{text "PVar name"}\\
-$\mid$~@{text "PTup pat pat"}\\
+\hspace{5mm}$\mid$~@{text "PTup pat pat"}\\
 \isacommand{binder}~@{text "bn::pat \<Rightarrow> atom list"}\\
 \isacommand{where}~@{text "bn(PNil) = []"}\\
 \hspace{5mm}$\mid$~@{text "bn(PVar x) = [atom x]"}\\
 \hspace{5mm}$\mid$~@{text "bn(PTup p\<^isub>1 p\<^isub>2) = bn(p\<^isub>1) @ bn(p\<^isub>2)"}\smallskip\\
 \end{tabular}}
-\end{equation}
+\end{equation}\smallskip
-%
 \noindent
 In this specification the function @{text "bn"} determines which atoms of
 the pattern @{text p} are bound in the argument @{text "t"}. Note that in the
 second-last @{text bn}-clause the function @{text "atom"} 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 said above, for deep binders we allow binding clauses such as
-\begin{center}
+\[\mbox{
 \begin{tabular}{ll}
 @{text "Bar p::pat t::trm"} &
-\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p t"} \\
+\isacommand{binds} @{text "bn(p)"} \isacommand{in} @{text "p t"} \\
-\end{tabular}
+\end{tabular}}
-\end{center}
+\]\smallskip
 \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
 specification:
-%
 \begin{equation}\label{letrecs}
 \mbox{%
 \begin{tabular}{@ {}l@ {}}
 \isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\
 \hspace{5mm}$\mid$~@{text "Let as::assn t::trm"}
-\;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t}\\
+\;\;\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text t}\\
 \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}
-\;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\
+\;\;\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\
-\isacommand{and} @{text "assn"} $=$
+\isacommand{and} @{text "assn"} $=$\\
-@{text "ANil"}
+\hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\
-$\mid$~@{text "ACons name trm assn"}\\
+\hspace{5mm}$\mid$~@{text "ACons name trm assn"}\\
 \isacommand{binder} @{text "bn::assn \<Rightarrow> atom list"}\\
 \isacommand{where}~@{text "bn(ANil) = []"}\\
 \hspace{5mm}$\mid$~@{text "bn(ACons a t as) = [atom a] @ bn(as)"}\\
 \end{tabular}}
-\end{equation}
+\end{equation}\smallskip
-%
 \noindent
 The difference is that with @{text Let} we only want to bind the atoms @{text
 "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms
 inside the assignment. This difference has consequences for the associated
 notions of free-atoms and alpha-equivalence.
 Consequently we exclude specifications such as
 %
 \begin{center}
 \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
 @{text "Baz\<^isub>1 p::pat t::trm"} &
-\isacommand{bind} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\
+\isacommand{binds} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\
 @{text "Baz\<^isub>2 p::pat t\<^isub>1::trm t\<^isub>2::trm"} &
-\isacommand{bind} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "t\<^isub>1"},
+\isacommand{binds} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "t\<^isub>1"},
-\isacommand{bind} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "t\<^isub>2"}\\
+\isacommand{binds} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "t\<^isub>2"}\\
 \end{tabular}
 \end{center}
 \noindent
 Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"}  pick
 In order to simplify our definitions of free atoms and alpha-equivalence,
 we shall assume specifications
 of term-calculi are implicitly \emph{completed}. By this we mean that
 for every argument of a term-constructor that is \emph{not}
 already part of a binding clause given by the user, we add implicitly a special \emph{empty} binding
-clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case
+clause, written \isacommand{binds}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case
 of the lambda-terms, the completion produces
 \begin{center}
 \begin{tabular}{@ {}l@ {\hspace{-1mm}}}
 \isacommand{nominal\_datatype} @{text lam} =\\
 \hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"}
-\;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "x"}\\
+\;\;\isacommand{binds}~@{term "{}"}~\isacommand{in}~@{text "x"}\\
 \hspace{5mm}$\mid$~@{text "App t\<^isub>1::lam t\<^isub>2::lam"}
-\;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>1 t\<^isub>2"}\\
+\;\;\isacommand{binds}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>1 t\<^isub>2"}\\
 \hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}
-\;\;\isacommand{bind}~@{text x} \isacommand{in} @{text t}\\
+\;\;\isacommand{binds}~@{text x} \isacommand{in} @{text t}\\
 \end{tabular}
 \end{center}
 \noindent
 The point of completion is that we can make definitions over the binding
 binding mechanisms their definitions are somewhat involved.  Given
 a 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{bind (set)} (the other modes are similar).
+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{center}
-\mbox{\isacommand{bind (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
+\mbox{\isacommand{binds (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
 \end{center}
 \noindent
 in which the body-labels @{text "d"}$_{1..q}$ refer to types @{text ty}$_{1..q}$,
 and the binders @{text b}$_{1..p}$
 The task below is to specify what the premises of a binding clause are. As a
 special instance, we first treat the case where @{text "bc\<^isub>i"} is the
 empty binding clause of the form
 \begin{center}
-\mbox{\isacommand{bind (set)} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
+\mbox{\isacommand{binds (set)} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
 \end{center}
 \noindent
 In this binding clause no atom is bound and we only have to alpha-relate the bodies. For this
 we build first the tuples @{text "D \<equiv> (d\<^isub>1,\<dots>, d\<^isub>q)"} and @{text "D' \<equiv> (d\<PRIME>\<^isub>1,\<dots>, d\<PRIME>\<^isub>q)"}
 We will use the unfolded version in the examples below.
 Now suppose the binding clause @{text "bc\<^isub>i"} is of the general form
 \begin{equation}\label{nonempty}
-\mbox{\isacommand{bind (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
+\mbox{\isacommand{binds (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
 \end{equation}
 \noindent
 In this case we define a premise @{text P} using the relation
 $\approx_{\,\textit{set}}$ given in Section~\ref{sec:binders} (similarly
 %\isacommand{and}~@{text "ckind ="}\\
 %\phantom{$|$}~@{text "CKSim ty ty"}\\
 %\isacommand{and}~@{text "ty ="}\\
 %\phantom{$|$}~@{text "TVar tvar"}~$|$~@{text "T string"}~$|$~@{text "TApp ty ty"}\\
 %$|$~@{text "TFun string ty_list"}~%
-%$|$~@{text "TAll tv::tvar tkind ty::ty"}  \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text ty}\\
+%$|$~@{text "TAll tv::tvar tkind ty::ty"}  \isacommand{binds}~@{text "tv"}~\isacommand{in}~@{text ty}\\
 %$|$~@{text "TArr ckind ty"}\\
 %\isacommand{and}~@{text "ty_lst ="}\\
 %\phantom{$|$}~@{text "TNil"}~$|$~@{text "TCons ty ty_lst"}\\
 %\isacommand{and}~@{text "cty ="}\\
 %\phantom{$|$}~@{text "CVar cvar"}~%
 %$|$~@{text "C string"}~$|$~@{text "CApp cty cty"}~$|$~@{text "CFun string co_lst"}\\
-%$|$~@{text "CAll cv::cvar ckind cty::cty"}  \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text cty}\\
+%$|$~@{text "CAll cv::cvar ckind cty::cty"}  \isacommand{binds}~@{text "cv"}~\isacommand{in}~@{text cty}\\
 %$|$~@{text "CArr ckind cty"}~$|$~@{text "CRefl ty"}~$|$~@{text "CSym cty"}~$|$~@{text "CCirc cty cty"}\\
 %$|$~@{text "CAt cty ty"}~$|$~@{text "CLeft cty"}~$|$~@{text "CRight cty"}~$|$~@{text "CSim cty cty"}\\
 %$|$~@{text "CRightc cty"}~$|$~@{text "CLeftc cty"}~$|$~@{text "Coerce cty cty"}\\
 %\isacommand{and}~@{text "co_lst ="}\\
 %\phantom{$|$}@{text "CNil"}~$|$~@{text "CCons cty co_lst"}\\
 %\isacommand{and}~@{text "trm ="}\\
 %\phantom{$|$}~@{text "Var var"}~$|$~@{text "K string"}\\
-%$|$~@{text "LAM_ty tv::tvar tkind t::trm"}  \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text t}\\
+%$|$~@{text "LAM_ty tv::tvar tkind t::trm"}  \isacommand{binds}~@{text "tv"}~\isacommand{in}~@{text t}\\
-%$|$~@{text "LAM_cty cv::cvar ckind t::trm"}   \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text t}\\
+%$|$~@{text "LAM_cty cv::cvar ckind t::trm"}   \isacommand{binds}~@{text "cv"}~\isacommand{in}~@{text t}\\
 %$|$~@{text "App_ty trm ty"}~$|$~@{text "App_cty trm cty"}~$|$~@{text "App trm trm"}\\
-%$|$~@{text "Lam v::var ty t::trm"}  \isacommand{bind}~@{text "v"}~\isacommand{in}~@{text t}\\
+%$|$~@{text "Lam v::var ty t::trm"}  \isacommand{binds}~@{text "v"}~\isacommand{in}~@{text t}\\
-%$|$~@{text "Let x::var ty trm t::trm"}  \isacommand{bind}~@{text x}~\isacommand{in}~@{text t}\\
+%$|$~@{text "Let x::var ty trm t::trm"}  \isacommand{binds}~@{text x}~\isacommand{in}~@{text t}\\
 %$|$~@{text "Case trm assoc_lst"}~$|$~@{text "Cast trm co"}\\
 %\isacommand{and}~@{text "assoc_lst ="}\\
 %\phantom{$|$}~@{text ANil}~%
-%$|$~@{text "ACons p::pat t::trm assoc_lst"}  \isacommand{bind}~@{text "bv p"}~\isacommand{in}~@{text t}\\
+%$|$~@{text "ACons p::pat t::trm assoc_lst"}  \isacommand{binds}~@{text "bv p"}~\isacommand{in}~@{text t}\\
 %\isacommand{and}~@{text "pat ="}\\
 %\phantom{$|$}~@{text "Kpat string tvtk_lst tvck_lst vt_lst"}\\
 %\isacommand{and}~@{text "vt_lst ="}\\
 %\phantom{$|$}~@{text VTNil}~$|$~@{text "VTCons var ty vt_lst"}\\
 %\isacommand{and}~@{text "tvtk_lst ="}\\
 covers cases of binders depending on other binders, which just do not make
 sense for our alpha-equated terms. Third, it allows empty types that have no
 meaning in a HOL-based theorem prover. We also had to generalise slightly Ott's
 binding clauses. In Ott you specify binding clauses with a single body; we
 allow more than one. We have to do this, because this makes a difference
-for our notion of alpha-equivalence in case of \isacommand{bind (set)} and
+for our notion of alpha-equivalence in case of \isacommand{binds (set)} and
-\isacommand{bind (set+)}.
+\isacommand{binds (set+)}.
 Consider the examples
 \begin{center}
 \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
 @{text "Foo\<^isub>1 xs::name fset t::trm s::trm"} &
-\isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t s"}\\
+\isacommand{binds (set)} @{text "xs"} \isacommand{in} @{text "t s"}\\
 @{text "Foo\<^isub>2 xs::name fset t::trm s::trm"} &
-\isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t"},
+\isacommand{binds (set)} @{text "xs"} \isacommand{in} @{text "t"},
-\isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "s"}\\
+\isacommand{binds (set)} @{text "xs"} \isacommand{in} @{text "s"}\\
 \end{tabular}
 \end{center}
 \noindent
 In the first term-constructor we have a single
 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 general binders
 can be specified using special markers, written @{text "inner"} and
 @{text "outer"}. It seems our and his specifications can be
 inter-translated as long as ours use the binding mode
-\isacommand{bind} only.
+\isacommand{binds} only.
 However, we have not proved this. Pottier gives a definition for
 alpha-equivalence, which also uses a permutation operation (like ours).
 Still, this definition is rather different from ours and he only proves that
 it defines an equivalence relation. A complete
 reasoning infrastructure is well beyond the purposes of his language.
 Similar work for Haskell with similar results was reported by Cheney \cite{Cheney05a}.
 In a slightly different domain (programming with dependent types), the
 paper \cite{Altenkirch10} presents a calculus with a notion of
-alpha-equivalence related to our binding mode \isacommand{bind (set+)}.
+alpha-equivalence related to our binding mode \isacommand{binds (set+)}.
 The definition in \cite{Altenkirch10} is similar to the one by Pottier, except that it
 has a more operational flavour and calculates a partial (renaming) map.
 In this way, the definition can deal with vacuous binders. However, to our
 best knowledge, no concrete mathematical result concerning this
 definition of alpha-equivalence has been proved.

changeset 3004	c6af56de923d
parent 3002	02d98590454d
child 3005	4df720c9b660