--- a/Paper/Paper.thy Fri Jul 02 01:54:19 2010 +0100
+++ b/Paper/Paper.thy Fri Jul 02 15:34:46 2010 +0100
@@ -45,7 +45,7 @@
text {*
%%% @{text "(1, (2, 3))"}
- So far, Nominal Isabelle provides a mechanism for constructing
+ So far, Nominal Isabelle provided a mechanism for constructing
$\alpha$-equated terms, for example lambda-terms
\begin{center}
@@ -366,7 +366,7 @@
conditions for $\alpha$-equated terms. We are also able to derive strong
induction principles that have the variable convention already built in.
The method behind our specification of general binders is taken
- from the Ott-tool, but we introduce restrictions, and also one extension, so
+ from the Ott-tool, but we introduce crucial restrictions, and also one extension, so
that our specifications make sense for reasoning about $\alpha$-equated terms.
@@ -404,9 +404,9 @@
\end{tabular}
\end{center}
\end{boxedminipage}
- \caption{The term-language of System @{text "F\<^isub>C"}
+ \caption{The System @{text "F\<^isub>C"}
\cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this
- version of the term-language we made a modification by separating the
+ version of @{text "F\<^isub>C"} we made a modification by separating the
grammars for type kinds and coercion kinds, as well as for types and coercion
types. For this paper the interesting term-constructor is @{text "\<CASE>"},
which binds multiple type-, coercion- and term-variables.\label{corehas}}
@@ -601,7 +601,7 @@
*}
-section {* General Binders\label{sec:binders} *}
+section {* General Bindings\label{sec:binders} *}
text {*
In Nominal Isabelle, the user is expected to write down a specification of a
@@ -683,7 +683,7 @@
\end{array}
\end{equation}
- It might be useful to consider first some examples for how these definitions
+ It might be useful to consider first some examples about how these definitions
of $\alpha$-equivalence pan out in practice. For this consider the case of
abstracting a set of variables over types (as in type-schemes). We set
@{text R} to be the usual equality @{text "="} and for @{text "fv(T)"} we
@@ -853,7 +853,7 @@
the definitions for $\alpha$-equivalence will help us in the next section.
*}
-section {* Specifying General Binders\label{sec:spec} *}
+section {* Specifying General Bindings\label{sec:spec} *}
text {*
Our choice of syntax for specifications is influenced by the existing
@@ -989,7 +989,7 @@
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 below).
+ 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
@@ -1068,10 +1068,10 @@
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 free-variable
- function and $\alpha$-equivalence relation, which we are going to define later.
+ function and $\alpha$-equivalence relation.
To make sure that variables bound by deep binders cannot be free at the
- same time, we cannot have more than one binding function for one binder.
+ same time, we cannot have more than one binding function for one deep binder.
Consequently we exclude specifications such as
\begin{center}
@@ -1089,7 +1089,7 @@
out different atoms to become bound, respectively be free, in @{text "p"}.
We also need to restrict the form of the binding functions in order
- to ensure the @{text "bn"}-functions can be lifted defined for $\alpha$-equated
+ to ensure the @{text "bn"}-functions can be defined for $\alpha$-equated
terms. As a result 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
@@ -1097,7 +1097,7 @@
In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons}
may have a binding clause involving the argument @{text t} (the only one that
is \emph{not} used in the definition of the binding function). This restriction
- means that we can lift the binding function to $\alpha$-equated terms.
+ is sufficient for defining the binding function over $\alpha$-equated terms.
In the version of
Nominal Isabelle described here, we also adopted the restriction from the
@@ -1171,8 +1171,7 @@
in Isabelle/HOL). We then define the user-specified binding
functions @{term "bn"} by recursion over the corresponding
raw datatype. We can also easily define permutation operations by
- recursion so that for each term constructor @{text "C"} with
- arguments @{text "z"}$_{1..n}$ we have that
+ recursion so that for each term constructor @{text "C"} we have that
%
\begin{equation}\label{ceqvt}
@{text "p \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (p \<bullet> z\<^isub>1) \<dots> (p \<bullet> z\<^isub>n)"}
@@ -1180,7 +1179,7 @@
The first non-trivial step we have to perform is the generation of
free-variable functions from the specifications. For the
- \emph{raw} types @{text "ty"}$_{1..n}$ of a specification,
+ \emph{raw} types @{text "ty"}$_{1..n}$ extracted from a specification,
we define the free-variable functions
%
\begin{equation}\label{fvars}
@@ -1188,7 +1187,8 @@
\end{equation}
\noindent
- We define them together with auxiliary free-variable functions for
+ by recursion over the types @{text "ty"}$_{1..n}$.
+ We define these functions together with auxiliary free-variable functions for
the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$
we define
%
@@ -1203,13 +1203,13 @@
While the idea behind these free-variable functions is clear (they just
collect all atoms that are not bound), because of our rather complicated
- binding mechanisms their definitions are somewhat involved. The functions
- are defined by recursion defining a clause for each term-constructor. Given
+ binding mechanisms their definitions are somewhat involved. Given
the 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
"fv_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be the union @{text
- "fv(bc\<^isub>1) \<union> \<dots> \<union> fv(bc\<^isub>k)"}. Given the binding clause @{text
- bc\<^isub>i} is of the form
+ "fv(bc\<^isub>1) \<union> \<dots> \<union> fv(bc\<^isub>k)"} where we define below what @{text "fv"} of a binding
+ clause with mode \isacommand{bin\_set} means (similarly for the other modes).
+ Suppose the binding clause @{text bc\<^isub>i} is of the form
%
\begin{equation}
\mbox{\isacommand{bind\_set} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
@@ -1220,7 +1220,7 @@
and the binders @{text b}$_{1..p}$
either refer to labels of atom types (in case of shallow binders) or to binding
functions taking a single label as argument (in case of deep binders). Assuming the
- set @{text "D"} stands for the free atoms in the bodies, @{text B} for the
+ set @{text "D"} stands for the free atoms in the bodies, the set @{text B} for the
binding atoms in the binders and @{text "B'"} for the free atoms in
non-recursive deep binders,
then the free atoms of the binding clause @{text bc\<^isub>i} are given by
@@ -1230,7 +1230,7 @@
\end{center}
\noindent
- The set @{text D} is defined as
+ The set @{text D} is formally defined as
%
\begin{center}
@{text "D \<equiv> fv_ty\<^isub>1 d\<^isub>1 \<union> ... \<union> fv_ty\<^isub>q d\<^isub>q"}
@@ -1238,24 +1238,24 @@
\noindent
whereby the functions @{text "fv_ty\<^isub>i"} are the ones we are defining by recursion
- (see \eqref{fvars}) provided the @{text "d\<^isub>i"} refers to one of the types
- @{text "ty"}$_{1..n}$; otherwise we set @{text "fv_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
- In order to define the set @{text B} we use the following auxiliary bn-functions
+ (see \eqref{fvars}) provided the @{text "d\<^isub>i"} refers to one of the raw types
+ @{text "ty"}$_{1..n}$ from a specification; otherwise we set @{text "fv_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
+ In order to define the set @{text B} we use the following auxiliary @{text "bn"}-functions
for atom types to which shallow binders have to refer
%
\begin{center}
\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
- @{text "bn_atom a"} & @{text "="} & @{text "{atom a}"}\\
- @{text "bn_atom_set as"} & @{text "="} & @{text "atoms as"}\\
- @{text "bn_atom_list as"} & @{text "="} & @{text "atoms (set as)"}
+ @{text "bn_atom a"} & @{text "\<equiv>"} & @{text "{atom a}"}\\
+ @{text "bn_atom_set as"} & @{text "\<equiv>"} & @{text "atoms as"}\\
+ @{text "bn_atom_list as"} & @{text "\<equiv>"} & @{text "atoms (set as)"}
\end{tabular}
\end{center}
\noindent
- In these functions, @{text "atoms"}, like @{text "atom"}, coerces
+ The function @{text "atoms"} coerces
the set of atoms to a set of the generic atom type. It is defined as
@{text "atoms as \<equiv> {atom a | a \<in> as}"}.
- The set @{text B} is then defined as
+ The set @{text B} is then formally defined as
%
\begin{center}
@{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> ... \<union> bn_ty\<^isub>p b\<^isub>p"}
@@ -1271,18 +1271,18 @@
\noindent
with none of the @{text "a"}$_{1..r}$ being among the bodies @{text
- "d"}$_{1..q}$. The set @{text "B'"} is then defined as
+ "d"}$_{1..q}$. The set @{text "B'"} is defined as
%
\begin{center}
@{text "B' \<equiv> fv_bn\<^isub>1 a\<^isub>1 \<union> ... \<union> fv_bn\<^isub>r a\<^isub>r"}
\end{center}
\noindent
- Similarly for the other binding modes.
+ This completes the definition of the free-variable functions.
Note that for non-recursive deep binders, we have to add all atoms that are left
unbound by the binding function @{text "bn"}. This is the purpose of the functions
- @{text "fv_bn"}, also defined by recursion. Assume the user has specified
+ @{text "fv_bn"}, also defined by recursion. Assume the user specified
a @{text bn}-clause of the form
%
\begin{center}
@@ -1291,25 +1291,27 @@
\noindent
where the @{text "z"}$_{1..n}$ are of types @{text "ty"}$_{1..n}$. For each of
- the arguments we calculate the free atoms as follows
+ the arguments we calculate the free atoms as follows:
%
\begin{center}
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
- $\bullet$ & @{term "fv_ty\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text "rhs"}\\
+ $\bullet$ & @{term "fv_ty\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text "rhs"}
+ (nothing gets bound in @{text "z\<^isub>i"}),\\
$\bullet$ & @{term "fv_bn\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} occurs in @{text "rhs"}
- with the recursive call @{text "bn\<^isub>i z\<^isub>i"}\\
+ with the recursive call @{text "bn\<^isub>i z\<^isub>i"}, and\\
$\bullet$ & @{term "{}"} provided @{text "z\<^isub>i"} occurs in @{text "rhs"},
but without a recursive call
\end{tabular}
\end{center}
\noindent
- For defining @{text "fv_bn (C z\<^isub>1 \<dots> z\<^isub>n)"}, we just union up all these values.
+ For defining @{text "fv_bn (C z\<^isub>1 \<dots> z\<^isub>n)"} we just union up all these values.
To see how these definitions work in practice, let us reconsider the term-constructors
- @{text "Let"} and @{text "Let_rec"} from the example shown in \eqref{letrecs}.
- For them we consider three free-variable functions, namely
- @{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"}:
+ @{text "Let"} and @{text "Let_rec"}, as well as @{text "ANil"} and @{text "ACons"}
+ from the example shown in \eqref{letrecs}.
+ For them we define three free-variable functions, namely
+ @{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"} as follows:
%
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
@@ -1317,7 +1319,7 @@
@{text "fv\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fv\<^bsub>assn\<^esub> as \<union> fv\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm]
@{text "fv\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
- @{text "fv\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "{atom a} \<union> (fv\<^bsub>trm\<^esub> t) \<union> (fv\<^bsub>assn\<^esub> as)"}\\[1mm]
+ @{text "fv\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(supp a) \<union> (fv\<^bsub>trm\<^esub> t) \<union> (fv\<^bsub>assn\<^esub> as)"}\\[1mm]
@{text "fv\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
@{text "fv\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(fv\<^bsub>trm\<^esub> t) \<union> (fv\<^bsub>bn\<^esub> as)"}
@@ -1325,42 +1327,48 @@
\end{center}
\noindent
- Since there are only (implicit) empty binding clauses for the term-constructors @{text ANil}
- and @{text "ACons"}, the corresponding free-variable function @{text
- "fv\<^bsub>assn\<^esub>"} returns all atoms occurring in an assignment. The
- binding only takes place in @{text Let} and @{text "Let_rec"}. In the @{text
- "Let"}-clause we want to bind all atoms given by @{text "set (bn as)"} in
- @{text t}. Therefore we have to subtract @{text "set (bn as)"} from @{text
+ To see the ``pattern'', recall that @{text ANil} and @{text "ACons"} have no
+ binding clause in the specification. The corresponding free-variable
+ function @{text "fv\<^bsub>assn\<^esub>"} therefore returns all atoms
+ occurring in an assignment. The binding only takes place in @{text Let} and
+ @{text "Let_rec"}. In the @{text "Let"}-clause, the binding clause specifies
+ that all atoms given by @{text "set (bn as)"} have to be bound in @{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 occurrences of the atoms
- in @{text "set (bn as)"} inside @{text "as"}. Therefore we have to subtract @{text
- "set (bn as)"} from @{text "fv\<^bsub>trm\<^esub> t"}, as well as from
- @{text "fv\<^bsub>assn\<^esub> as"}. 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} or @{text "Let_rec"} will some atoms become bound.
- This is a phenomenon
- that has also been pointed out in \cite{ott-jfp}. For us it is crucial, because
- we would not be able to lift a @{text "bn"}-function that is defined over
- arguments that are either binders or bodies. In that case @{text "bn"} would
- not respect $\alpha$-equivalence. We can also see that
+ free in @{text "as"}. In contrast, in @{text "Let_rec"} we have a recursive
+ binder where we want to also bind all occurrences of the atoms in @{text
+ "set (bn as)"} also inside @{text "as"}. Therefore we have to subtract
+ @{text "set (bn as)"} from the union @{text "fv\<^bsub>trm\<^esub> t"} and @{text "fv\<^bsub>assn\<^esub> as"}.
+
+ An interesting point in this
+ example is that a ``naked'' assignment does not bind any
+ atoms. Only in the context of a @{text Let} or @{text "Let_rec"} will
+ some atoms from an assignment become bound. This is a phenomenon that has also been pointed
+ out in \cite{ott-jfp}. For us this observation is crucial, because we would
+ not be able to lift the @{text "bn"}-function if it was defined over assignments
+ where some atoms are bound. In that case @{text "bn"} would \emph{not} respect
+ $\alpha$-equivalence.
+
+ Next we define $\alpha$-equivalence relations for the raw types @{text
+ "ty"}$_{1..n}$. We call them
%
- \begin{equation}\label{bnprop}
- @{text "fv_ty x = bn x \<union> fv_bn x"}.
- \end{equation}
+ \begin{center}
+ @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}.
+ \end{center}
\noindent
- holds for any @{text "bn"}-function defined for the type @{text "ty"}.
-
- TBD below.
+ Like with the free-variable functions, we also need to
+ define auxiliary $\alpha$-equivalence relations
+ %
+ \begin{center}
+ @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}
+ \end{center}
- Next we define $\alpha$-equivalence relations for the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}. We call them
- @{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.
- Say we have binding functions @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, then we also define @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}.
- To simplify our definitions we will use the following abbreviations for
- relations and free-variable acting on products.
+ \noindent
+ for the binding functions @{text "bn"}$_{1..m}$,
+ To simplify our definitions we will use the following abbreviations for
+ equivalence relations and free-variable functions acting on pairs
+
%
\begin{center}
\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
@@ -1370,16 +1378,17 @@
\end{center}
- The relations for $\alpha$-equivalence are inductively defined predicates, whose clauses have
- conclusions of the form
+ The relations for $\alpha$-equivalence are inductively defined
+ predicates, whose clauses have the form
%
\begin{center}
- \mbox{\infer{@{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"}}
- {@{text "prems(bc\<^isub>1)"} & @{text "\<dots>"} & @{text "prems(bc\<^isub>p)"}}}
+ \mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>n \<approx>ty C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>n"}}
+ {@{text "prems(bc\<^isub>1) \<and> \<dots> \<and> prems(bc\<^isub>k)"}}}
\end{center}
\noindent
- For what follows, let us assume @{text C} is of type @{text ty}. The task
+ assuming the term-constructor @{text C} is of type @{text ty} and has
+ the binding clauses @{term "bc"}$_{1..k}$. The task
is to specify what the premises of these clauses are. Again for this we
analyse the binding clauses and produce a corresponding premise.
*}
@@ -1397,6 +1406,8 @@
fv_trm2 ("fv\<^bsub>assn\<^esub> \<oplus> fv\<^bsub>trm\<^esub>")
(*>*)
text {*
+ *TBD below *
+
\begin{equation}\label{alpha}
\mbox{%
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
@@ -2090,6 +2101,19 @@
section {* Conclusion *}
text {*
+We can also see that
+ %
+ \begin{equation}\label{bnprop}
+ @{text "fv_ty x = bn x \<union> fv_bn x"}.
+ \end{equation}
+
+ \noindent
+ holds for any @{text "bn"}-function defined for the type @{text "ty"}.
+
+*}
+
+
+text {*
We have presented an extension of Nominal Isabelle for deriving
automatically a convenient reasoning infrastructure that can deal with
general binders, that is term-constructors binding multiple variables at