--- a/Paper/Paper.thy Tue Apr 27 19:01:22 2010 +0200
+++ b/Paper/Paper.thy Tue Apr 27 19:51:35 2010 +0200
@@ -921,7 +921,7 @@
``\isacommand{bind}-part'' will be called \emph{binders}.
In contrast to Ott, we allow multiple labels in binders and bodies. For example
- we permit binding clauses as follows:
+ we have binding clauses of the form:
\begin{center}
\begin{tabular}{ll}
@@ -931,18 +931,20 @@
\end{center}
\noindent
+ Similarly for the other binding modes.
There are a few restrictions we need to impose: First, a body can only occur in
- \emph{one} binding clause of a term constructor. A binder, in contrast, may
- occur in several binding clauses, but cannot occur as a body.
+ \emph{one} binding clause of a term constructor.
- In addition we distinguish between \emph{shallow} and \emph{deep}
- binders. Shallow binders are of the form \isacommand{bind}\; {\it labels}\;
+ For binders we distinguish between \emph{shallow} and \emph{deep} binders.
+ Shallow binders are of the form \isacommand{bind}\; {\it labels}\;
\isacommand{in}\; {\it labels'} (similar for the other two modes). The
- restriction we impose on shallow binders is that the {\it labels} must either
- refer to atom types or to finite sets 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:
+ restriction we impose on shallow binders is that in case of
+ \isacommand{bind\_set} and \isacommand{bind\_res} the {\it labels} must
+ either refer to atom types or to sets of atom types; in case of
+ \isacommand{bind} we allow labels 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}{@ {}cc@ {}}
@@ -965,7 +967,8 @@
\noindent
Note that in this specification @{text "name"} refers to an atom type, and
- @{text "fset"} to the type of finite sets.
+ @{text "fset"} to the type of finite sets. Shallow binders can occur in the
+ binding part of several binding clauses.
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
@@ -1005,16 +1008,6 @@
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} may not have a
- 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 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:
@@ -1047,11 +1040,22 @@
\end{center}
\noindent
- since there is no overlap of binders.
+ since there is no overlap of binders. Unlike shallow binders, we restrict deep
+ binders to occur in only one binding clause. Therefore @{text "Bar\<^isub>2"} cannot
+ be reformulated as
+
+ \begin{center}
+ \begin{tabular}{ll}
+ @{text "Bar\<^isub>3 p::pat t::trm"} &
+ \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p"},
+ \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "t"}\\
+ \end{tabular}
+ \end{center}
- Note that in the last example we wrote \isacommand{bind}~@{text
- "bn(p)"}~\isacommand{in}~@{text "p.."}. Whenever such a binding clause is
- present, we will call the corresponding binder \emph{recursive}. To see the
+ Note that in the @{text "Bar\<^isub>2"}, we wrote \isacommand{bind}~@{text
+ "bn(p)"}~\isacommand{in}~@{text "p.."}. Whenever such a binding clause
+ is present, where the argument in the binder also occurs in the body, we will
+ call the corresponding binder \emph{recursive}. To see the
purpose of such recursive binders, compare ``plain'' @{text "Let"}s and
@{text "Let_rec"}s in the following specification:
%
@@ -1079,8 +1083,23 @@
inside the assignment. This difference has consequences for the free-variable
function and alpha-equivalence relation, which we are going to describe in the
rest of this section.
-
- In order to simplify some definitions, we shall assume specifications
+
+ We also need to restrict the form of the binding functions. 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
+ \eqref{letpat} that the term-constructors @{text PVar} and @{text PTup} may
+ not have a binding clause (all arguments are used to define @{text "bn"}).
+ In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons}
+ may have binding clause involving the argument @{text t} (the only one that
+ is \emph{not} used in the definition of the binding function). 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 some automatic proofs
+ later on.
+
+ In order to simplify some later definitions, we shall assume specifications
of term-calculi are \emph{completed}. By this we mean that
for every argument of a term-constructor that is \emph{not}
already part of a binding clause, we add implicitly a special \emph{empty} binding
@@ -1102,7 +1121,7 @@
\noindent
The point of completion is that we can make definitions over the binding
- clauses and be sure to capture all arguments of a term constructor.
+ clauses and be sure to have captured all arguments of a term constructor.
Having dealt with all syntax matters, the problem now is how we can turn
specifications into actual type definitions in Isabelle/HOL and then
@@ -1142,7 +1161,7 @@
we have that
%
\begin{equation}\label{ceqvt}
- @{text "p \<bullet> (C x\<^isub>1 \<dots> x\<^isub>n) = C (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}
+ @{text "p \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (p \<bullet> z\<^isub>1) \<dots> (p \<bullet> z\<^isub>n)"}
\end{equation}
The first non-trivial step we have to perform is the generation free-variable
@@ -1187,28 +1206,32 @@
collect all atoms that are not bound), because of our rather complicated
binding mechanisms their definitions are somewhat involved. Given a
term-constructor @{text "C"} of type @{text ty} and some associated binding
- clauses @{text bcs}, the result of the @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be
+ clauses @{text bcs}, the result of the @{text "fv_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be
the union of the values, @{text v}, calculated by the rules for empty, shallow and
deep binding clauses:
%
- \begin{equation}\label{deepbinder}
+ \begin{equation}\label{deepbinderA}
\mbox{%
\begin{tabular}{c@ {\hspace{2mm}}p{7.4cm}}
\multicolumn{2}{@ {}l}{\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\
$\bullet$ & @{term "v = fv_ty y"} provided @{text "y"} is of type @{text "ty"}\smallskip\\
-
+ %
\multicolumn{2}{@ {}l}{\isacommand{bind}~@{text "x\<^isub>1\<dots>x\<^isub>n"}~\isacommand{in}~@{text "y\<^isub>1\<dots>y\<^isub>m"}:}\\
- $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> \<dots> \<union> fv_ty\<^isub>m y\<^isub>m)"}\\
- & \hspace{15mm}@{text "- (fv_aty\<^isub>1 x\<^isub>1 \<union> \<dots> \<union> fv_aty\<^isub>n x\<^isub>n)"}\\
+ $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m)"}\\
+ & \hspace{15mm}@{text "- (fv_aty\<^isub>1 x\<^isub>1 \<union> .. \<union> fv_aty\<^isub>n x\<^isub>n)"}\\
& provided the bodies @{text "y"}$_{1..m}$ are of type @{text "ty"}$_{1..m}$ and the
binders @{text "x"}$_{1..n}$ of atomic types @{text "aty"}$_{1..n}$\smallskip\\
-
+ \end{tabular}}
+ \end{equation}
+ \begin{equation}\label{deepbinderB}
+ \mbox{%
+ \begin{tabular}{c@ {\hspace{2mm}}p{7.4cm}}
\multicolumn{2}{@ {}l}{\isacommand{bind}~@{text "bn x"}~\isacommand{in}~@{text "y\<^isub>1\<dots>y\<^isub>m"}:}\\
- $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> \<dots> \<union> fv_ty\<^isub>m y\<^isub>m) - set (bn x) \<union> (fv_bn x)"}\\
- $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> \<dots> \<union> fv_ty\<^isub>m y\<^isub>m) - set (bn x)"}\\
+ $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m) - set (bn x) \<union> (fv_bn x)"}\\
+ $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m) - set (bn x)"}\\
& provided the @{text "y"}$_{1..m}$ are of type @{text "ty"}$_{1..m}$; the first
- clause applies for @{text x} being a non-recursive deep binder, the
- second for a recursive deep binder
+ clause applies for @{text x} being a non-recursive deep binder (that is
+ @{text "x \<noteq> y"}$_{1..m}$), the second for a recursive deep binder
\end{tabular}}
\end{equation}
@@ -1217,8 +1240,8 @@
binder, we have to add all atoms that are left unbound by the binding
function @{text "bn"}. For this we define the function @{text "fv_bn"}. Assume
for the constructor @{text "C"} the binding function is of the form @{text
- "bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}. We again define a value
- @{text v} which is exactly as in \eqref{deepbinder} for shallow and deep
+ "bn (C z\<^isub>1 \<dots> z\<^isub>n) = rhs"}. We again define a value
+ @{text v} which is exactly as in \eqref{deepbinderA}/\eqref{deepbinderB} for shallow and deep
binding clauses, except for empty binding clauses are defined as follows:
%
\begin{equation}\label{bnemptybinder}