--- a/LMCS-Paper/Paper.thy Thu Sep 08 11:21:03 2011 +0100
+++ b/LMCS-Paper/Paper.thy Thu Sep 08 13:03:19 2011 +0100
@@ -202,7 +202,7 @@
\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}}
@@ -222,7 +222,7 @@
\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
@@ -517,7 +517,7 @@
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}"}\\
@@ -532,7 +532,7 @@
@{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
@@ -613,8 +613,10 @@
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
- `direction' in Propositions \ref{supppermeq} and \ref{avoiding}.
+ is equivalent with @{term "supp \<pi> \<sharp>* x"}, which means we could also formulate
+ Propositions \ref{supppermeq} and \ref{avoiding} in the other `direction', however the
+ 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
@@ -753,9 +755,6 @@
\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}
@@ -763,9 +762,11 @@
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 (as, x) (bs, y)"}.
-
+ @{term "abs_set (\<pi> \<bullet> as, \<pi> \<bullet> x) (\<pi> \<bullet> bs, \<pi> \<bullet> y)"} holds provided
+ @{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
@@ -802,13 +803,14 @@
\end{thm}
\noindent
- 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
+ In effect, this theorem states that the bound names do not appear in the support
+ 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
@@ -826,13 +828,14 @@
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
@@ -841,45 +844,48 @@
\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:
- @{thm supp_set.simps[THEN eq_reflection, no_vars]}.
-
+ function @{text aux}, taking an abstraction as argument
+
+ \[
+ @{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)"}
- \end{center}
+ \[
+ @{term "supp (supp_set (Abs_set as x)) \<subseteq> supp (Abs_set as x)"}
+ \]\smallskip
\noindent
- using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set,
- we further obtain
+ using fact about function applications in \eqref{supps}. Assuming
+ @{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
- form @{term "Abs_set as x"} etc is motivated by the fact that
- we can conveniently establish at the Isabelle/HOL level
- properties about them. It would be
- laborious to write custom ML-code that derives automatically such properties
- for every term-constructor that binds some atoms. Also the generality of
- the definitions for alpha-equivalence will help us in the next sections.
+ The method of first considering abstractions of the form @{term "Abs_set as
+ x"} etc is motivated by the fact that we can conveniently establish at the
+ Isabelle/HOL level properties about them. It would be extremely laborious
+ to write custom ML-code that derives automatically such properties for every
+ term-constructor that binds some atoms. Also the generality of the
+ definitions for alpha-equivalence will help us in the next sections.
*}
section {* Specifying General Bindings\label{sec:spec} *}
@@ -914,129 +920,124 @@
\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
- term-constructors, each of which comes with a list of labelled
- types that stand for the types of the arguments of the term-constructor.
- For example a term-constructor @{text "C\<^sup>\<alpha>"} might be specified with
+ Every type declaration @{text ty}$^\alpha_{1..n}$ consists of a collection
+ of term-constructors, each of which comes with a list of labelled types that
+ stand for the types of the arguments of the term-constructor. For example a
+ 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"}
- \end{center}
+ \[
+ @{text "C\<^sup>\<alpha> label\<^isub>1::ty"}\mbox{$'_1$} @{text "\<dots> label\<^isub>l::ty"}\mbox{$'_l\;\;$} @{text "binding_clauses"}
+ \]\smallskip
+
+ \noindent
+ whereby some of the @{text ty}$'_{1..l}$ (or their components) can be
+ contained in the collection of @{text ty}$^\alpha_{1..n}$ declared in
+ \eqref{scheme}. In this case we will call the corresponding argument a
+ \emph{recursive argument} of @{text "C\<^sup>\<alpha>"}. The types of such
+ recursive arguments need to satisfy a ``positivity'' restriction, which
+ ensures that the type has a set-theoretic semantics (see
+ \cite{Berghofer99}). The labels annotated on the types are optional. Their
+ purpose is to be used in the (possibly empty) list of \emph{binding
+ clauses}, which indicate the binders and their scope in a term-constructor.
+ They come in three \emph{modes}:
+
+
+ \[\mbox{
+ \begin{tabular}{@ {}l@ {}}
+ \isacommand{binds} {\it binders} \isacommand{in} {\it bodies}\\
+ \isacommand{binds (set)} {\it binders} \isacommand{in} {\it bodies}\\
+ \isacommand{binds (set+)} {\it binders} \isacommand{in} {\it bodies}
+ \end{tabular}}
+ \]\smallskip
\noindent
- whereby some of the @{text ty}$'_{1..l}$ (or their components)
- can be contained
- in the collection of @{text ty}$^\alpha_{1..n}$ declared in
- \eqref{scheme}.
- In this case we will call the corresponding argument a
- \emph{recursive argument} of @{text "C\<^sup>\<alpha>"}.
- The types of such recursive
- arguments need to satisfy a ``positivity''
- restriction, which ensures that the type has a set-theoretic semantics
- \cite{Berghofer99}.
- The labels
- annotated on the types are optional. Their purpose is to be used in the
- (possibly empty) list of \emph{binding clauses}, which indicate the binders
- and their scope in a term-constructor. They come in three \emph{modes}:
- %
- \begin{center}
- \begin{tabular}{@ {}l@ {}}
- \isacommand{bind} {\it binders} \isacommand{in} {\it bodies}\;\;\;\,
- \isacommand{bind (set)} {\it binders} \isacommand{in} {\it bodies}\;\;\;\,
- \isacommand{bind (set+)} {\it binders} \isacommand{in} {\it bodies}
- \end{tabular}
- \end{center}
- %
- \noindent
- The first mode is for binding lists of atoms (the order of binders matters);
- the second is for sets of binders (the order does not matter, but the
- cardinality does) and the last is for sets of binders (with vacuous binders
- preserving alpha-equivalence). As indicated, the labels in the ``\isacommand{in}-part'' of a binding
- clause will be called \emph{bodies}; the
- ``\isacommand{bind}-part'' will be called \emph{binders}. In contrast to
- Ott, we allow multiple labels in binders and bodies.
-
- For example we allow
+ The first mode is for binding lists of atoms (the order of bound atoms
+ matters); the second is for sets of binders (the order does not matter, but
+ the cardinality does) and the last is for sets of binders (with vacuous
+ binders preserving alpha-equivalence). As indicated, the labels in the
+ ``\isacommand{in}-part'' of a binding clause will be called \emph{bodies};
+ the ``\isacommand{binds}-part'' will be called \emph{binders}. In contrast to
+ Ott, we allow multiple labels in binders and bodies. For example we allow
binding clauses of the form:
-
- \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{bind} @{text "x y"} \isacommand{in} @{text "s"}\\
- \end{tabular}
- \end{center}
+ \isacommand{binds} @{text "x y"} \isacommand{in} @{text "t"},
+ \isacommand{binds} @{text "x y"} \isacommand{in} @{text "s"}\\
+ \end{tabular}}
+ \]\smallskip
\noindent
- Similarly for the other binding modes.
- Interestingly, in case of \isacommand{bind (set)}
- and \isacommand{bind (set+)} the binding clauses above will make a difference to the semantics
- of the specifications (the corresponding alpha-equivalence will differ). We will
- show this later with an example.
+ Similarly for the other binding modes. Interestingly, in case of
+ \isacommand{binds (set)} and \isacommand{binds (set+)} the binding clauses
+ above will make a difference to the semantics of the specifications (the
+ corresponding alpha-equivalence will differ). We will show this later with
+ an example.
+
- There are also some restrictions we need to impose on our binding clauses in comparison to
- the ones of Ott. The
- main idea behind these restrictions is that we obtain a sensible notion of
- alpha-equivalence where it is ensured that within a given scope an
- atom occurrence cannot be both bound and free at the same time. The first
- restriction is that a body can only occur in
+ There are also some restrictions we need to impose on our binding clauses in
+ comparison to the ones of Ott. The main idea behind these restrictions is
+ that we obtain a sensible notion of alpha-equivalence where it is ensured
+ that within a given scope an atom occurrence cannot be both bound and free
+ 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
- alternative binder for the same body).
+ atoms of a body cannot be free at the same time by specifying an alternative
+ binder for the same body).
- For binders we distinguish between
- \emph{shallow} and \emph{deep} binders. Shallow binders are just
- labels. The restriction we need to impose on them is that in case of
- \isacommand{bind (set)} and \isacommand{bind (set+)} the labels must either
- refer to atom types or to sets of atom types; in case of \isacommand{bind}
- the labels must refer to atom types or lists of atom types. Two examples for
- the use of shallow binders are the specification of lambda-terms, where a
- single name is bound, and type-schemes, where a finite set of names is
- bound:
+ For binders we distinguish between \emph{shallow} and \emph{deep} binders.
+ Shallow binders are just labels. The restriction we need to impose on them
+ is that in case of \isacommand{binds (set)} and \isacommand{binds (set+)} the
+ labels must either refer to atom types or to sets of atom types; in case of
+ \isacommand{binds} the labels must refer to atom types or lists of atom
+ types. Two examples for the use of shallow binders are the 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}{@ {}c@ {\hspace{7mm}}c@ {}}
+ \[\mbox{
+ \begin{tabular}{@ {}c@ {\hspace{5mm}}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{bind (set+)} @{text xs} \isacommand{in} @{text T}\\
+ \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}\hspace{3mm}%
+ \isacommand{binds (set+)} @{text xs} \isacommand{in} @{text T}\\
\end{tabular}
- \end{tabular}
- \end{center}
+ \end{tabular}}
+ \]\smallskip
+
\noindent
In these specifications @{text "name"} refers to an atom type, and @{text
- "fset"} to the type of finite sets.
- Note that for @{text lam} it does not matter which binding mode we use. The
- reason is that we bind only a single @{text name}. However, having
- \isacommand{bind (set)} or \isacommand{bind} in the second case makes a
- difference to the semantics of the specification (which we will define in the next section).
-
+ "fset"} to the type of finite sets. Note that for @{text lam} it does not
+ matter which binding mode we use. The reason is that we bind only a single
+ @{text name}. However, having \isacommand{binds (set)} or \isacommand{binds}
+ in the second case makes a difference to the semantics of the specification
+ (which we will define in the next section).
A \emph{deep} binder uses an auxiliary binding function that ``picks'' out
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
- \isacommand{bind (set+)}) or a list of atoms (for \isacommand{bind}). They can
- be defined by recursion over the corresponding type; the equations
+ expected to return either a set of atoms (for \isacommand{binds (set)} and
+ \isacommand{binds (set+)}) or a list of atoms (for \isacommand{binds}). They need
+ 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}
@@ -1044,20 +1045,20 @@
\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{and} @{text pat} $=$
- @{text PNil}
- $\mid$~@{text "PVar name"}
- $\mid$~@{text "PTup pat pat"}\\
+ \;\;\isacommand{binds} @{text "bn(p)"} \isacommand{in} @{text t}\\
+ \isacommand{and} @{text pat} $=$\\
+ \hspace{5mm}\phantom{$\mid$}~@{text PNil}\\
+ \hspace{5mm}$\mid$~@{text "PVar name"}\\
+ \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
@@ -1067,36 +1068,37 @@
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"} \\
- \end{tabular}
- \end{center}
+ \isacommand{binds} @{text "bn(p)"} \isacommand{in} @{text "p t"} \\
+ \end{tabular}}
+ \]\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{and} @{text "assn"} $=$
- @{text "ANil"}
- $\mid$~@{text "ACons name trm assn"}\\
+ \;\;\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\
+ \isacommand{and} @{text "assn"} $=$\\
+ \hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\
+ \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
@@ -1110,10 +1112,10 @@
\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{bind} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "t\<^isub>2"}\\
+ \isacommand{binds} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "t\<^isub>1"},
+ \isacommand{binds} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "t\<^isub>2"}\\
\end{tabular}
\end{center}
@@ -1147,18 +1149,18 @@
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}
@@ -1236,11 +1238,11 @@
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
@@ -1443,7 +1445,7 @@
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
@@ -1475,7 +1477,7 @@
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
@@ -1842,14 +1844,14 @@
%\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"}\\
@@ -1857,15 +1859,15 @@
%\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_cty cv::cvar ckind t::trm"} \isacommand{bind}~@{text "cv"}~\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{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 "Let x::var ty trm t::trm"} \isacommand{bind}~@{text x}~\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{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 ="}\\
@@ -2250,18 +2252,18 @@
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
- \isacommand{bind (set+)}.
+ for our notion of alpha-equivalence in case of \isacommand{binds (set)} and
+ \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{bind (set)} @{text "xs"} \isacommand{in} @{text "s"}\\
+ \isacommand{binds (set)} @{text "xs"} \isacommand{in} @{text "t"},
+ \isacommand{binds (set)} @{text "xs"} \isacommand{in} @{text "s"}\\
\end{tabular}
\end{center}
@@ -2296,7 +2298,7 @@
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
@@ -2306,7 +2308,7 @@
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