--- a/Paper/Paper.thy Wed Mar 24 19:50:42 2010 +0100
+++ b/Paper/Paper.thy Thu Mar 25 07:21:41 2010 +0100
@@ -528,30 +528,30 @@
section {* Alpha-Equivalence and Free Variables *}
text {*
- Our specifications for term-calculi are heavily
- inspired by the syntax of the Ott-tool \cite{ott-jfp}. A specification is
- a collection of (possibly mutual recursive) type declarations, say
- $ty^\alpha_1$, $ty^\alpha_2$, \ldots $ty^\alpha_n$, and an
- associated collection of binding functions, say
- $bn^\alpha_1$, \ldots, $bn^\alpha_m$. The syntax in Nominal Isabelle
- for such specifications is rougly as follows:
+ Our specifications for term-calculi are heavily inspired by the existing
+ datatype package of Isabelle/HOL and by the syntax of the Ott-tool
+ \cite{ott-jfp}. A specification is a collection of (possibly mutual
+ recursive) type declarations, say @{text "ty"}$^\alpha_1$, \ldots,
+ @{text ty}$^\alpha_n$, and an associated collection
+ of binding functions, say @{text bn}$^\alpha_1$, \ldots, @{text
+ bn}$^\alpha_m$. The syntax in Nominal Isabelle for such specifications is
+ rougly as follows:
%
\begin{equation}\label{scheme}
\mbox{\begin{tabular}{@ {\hspace{-5mm}}p{1.8cm}l}
type \mbox{declaration part} &
$\begin{cases}
\mbox{\begin{tabular}{l}
- \isacommand{nominal\_datatype} $ty^\alpha_1 = \ldots$\\
- \isacommand{and} $ty^\alpha_2 = \ldots$\\
+ \isacommand{nominal\_datatype} @{text ty}$^\alpha_1 = \ldots$\\
+ \isacommand{and} @{text ty}$^\alpha_2 = \ldots$\\
$\ldots$\\
- \isacommand{and} $ty^\alpha_n = \ldots$\\
+ \isacommand{and} @{text ty}$^\alpha_n = \ldots$\\
\end{tabular}}
\end{cases}$\\
binding \mbox{function part} &
$\begin{cases}
\mbox{\begin{tabular}{l}
- \isacommand{with} $bn^\alpha_1$ \isacommand{and} \ldots \isacommand{and} $bn^\alpha_m$
- $\ldots$\\
+ \isacommand{with} @{text bn}$^\alpha_1$ \isacommand{and} \ldots \isacommand{and} @{text bn}$^\alpha_m$\\
\isacommand{where}\\
$\ldots$\\
\end{tabular}}
@@ -560,22 +560,22 @@
\end{equation}
\noindent
- Every type declaration $ty^\alpha_i$ consists of a collection of
+ 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 $C^\alpha$ might have
+ For example a term-constructor @{text "C\<^sup>\<alpha>"} might have
\begin{center}
- $C^\alpha\;label_1\!::\!ty'_1\;\ldots label_l\!::\!ty'_l\;\;\textit{binding\_clauses}$
+ @{text "C\<^sup>\<alpha> label\<^isub>1::ty"}$'_1$ @{text "\<dots> label\<^isub>l::ty"}$'_l\;\;$ @{text "binding_clauses"}
\end{center}
\noindent
- whereby some of the $ty'_k$ (or their components) are contained in the collection
- of $ty^\alpha_i$ declared in \eqref{scheme}. In this case we will call the
+ whereby some of the @{text ty}$'_{1..l}$ (or their components) are contained in the collection
+ of @{text ty}$^\alpha_{1..n}$ declared in \eqref{scheme}. In this case we will call the
corresponding argument a \emph{recursive argument}. The labels annotated on
the types are optional and can be used in the (possibly empty) list of
- \emph{binding clauses}. These clauses indicate the binders and the scope of
- the binders in a term-constructor. They come in three \emph{modes}
+ \emph{binding clauses}. These clauses indicate the binders and their scope of
+ in a term-constructor. They come in three \emph{modes}:
\begin{center}
@@ -588,17 +588,17 @@
\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 cardinality does) and the last is for
+ 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).
In addition we distinguish between \emph{shallow} binders and \emph{deep}
binders. Shallow binders are of the form \isacommand{bind}\; {\it label}\;
- \isacommand{in}\; {\it another\_label} (similar for the other two modes). The
+ \isacommand{in}\; {\it label'} (similar for the other two modes). The
restriction we impose on shallow binders is that the {\it label} must either
refer to a type that is an atom type or to a type that is a finite set or
- list of an atom type. For example the specifications for lambda-terms, where
- a single name is bound, and type-schemes, where a finite set of names is
- bound, use shallow binders (the type \emph{name} is an atom type):
+ list of an atom type. Two examples for the use of shallow binders are the
+ specification of lambda-terms, where a single name is bound, and of
+ type-schemes, where a finite set of names is bound:
\begin{center}
\begin{tabular}{@ {}cc@ {}}
@@ -620,12 +620,13 @@
\end{center}
\noindent
+ Note that in this specification \emph{name} refers to an atom type.
If we have shallow binders that ``share'' a body, for instance $t$ in
- the term-constructor Foo$_0$
+ the following term-constructor
\begin{center}
\begin{tabular}{ll}
- \it {\rm Foo}$_0$ x::name y::name t::lam & \it
+ \it {\rm Foo} x::name y::name t::lam & \it
\isacommand{bind}\;x\;\isacommand{in}\;t,\;
\isacommand{bind}\;y\;\isacommand{in}\;t
\end{tabular}
@@ -633,19 +634,19 @@
\noindent
then we have to make sure the modes of the binders agree. We cannot
- have in the first binding clause the mode \isacommand{bind} and in the second
- \isacommand{bind\_set}.
+ have, for instance, in the first binding clause the mode \isacommand{bind}
+ and in the second \isacommand{bind\_set}.
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}).
+ 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\_res}) or a list of atoms
(for \isacommand{bind}). They can be defined by primitive recursion over the
corresponding type; the equations must be given in the binding function part of
the scheme shown in \eqref{scheme}. For example for a calculus containing lets
- with tuple patterns, you might declare
+ with tuple patterns, you might specify
\begin{center}
\begin{tabular}{l}
@@ -657,52 +658,59 @@
\hspace{5mm}$\mid$ Let\;{\it p::pat}\;{\it trm}\; {\it t::trm}
\;\;\isacommand{bind} {\it bn(p)} \isacommand{in} {\it t}\\
\isacommand{and} {\it pat} =\\
- \hspace{5mm}\phantom{$\mid$} PNo\\
- \hspace{5mm}$\mid$ PVr\;{\it name}\\
- \hspace{5mm}$\mid$ PPr\;{\it pat}\;{\it pat}\\
+ \hspace{5mm}\phantom{$\mid$} PNil\\
+ \hspace{5mm}$\mid$ PVar\;{\it name}\\
+ \hspace{5mm}$\mid$ PTup\;{\it pat}\;{\it pat}\\
\isacommand{with} {\it bn::pat $\Rightarrow$ atom list}\\
- \isacommand{where} $bn(\textrm{PNil}) = []$\\
- \hspace{5mm}$\mid$ $bn(\textrm{PVar}\;x) = [atom\; x]$\\
- \hspace{5mm}$\mid$ $bn(\textrm{PPrd}\;p_1\;p_2) = bn(p_1)\; @\;bn(p_2)$\\
+ \isacommand{where} $\textit{bn}(\textrm{PNil}) = []$\\
+ \hspace{5mm}$\mid$ $\textit{bn}(\textrm{PVar}\;x) = [\textit{atom}\; x]$\\
+ \hspace{5mm}$\mid$ $\textit{bn}(\textrm{PTup}\;p_1\;p_2) = \textit{bn}(p_1)\; @\;\textit{bn}(p_2)$\\
\end{tabular}
\end{center}
\noindent
- In this specification the function $atom$ coerces a name into the generic
- atom type of Nominal Isabelle. 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 also is bound in the term-constructor. In the present
- version of Nominal Isabelle, we adopted the restriction the Ott-tool imposes
- on the binding functions, namely a binding function can only return the
- empty set (case PNil), a singleton set containing an atom (case PVar) or
- unions of atom sets (case PPrd). Moreover, as with shallow binders, deep
- binders with shared body need to have the same binding mode. Finally, 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:
+ In this specification the function @{text "bn"} determines which atoms of @{text p} are
+ bound in the argument @{text "t"}. Note that the second last clause the function @{text "atom"}
+ coerces a name into the generic atom type of Nominal Isabelle. 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 PVar and PTup must not have a
+ binding clause. In the present version of Nominal Isabelle, we also adopted
+ the restriction from the Ott-tool that binding functions can only return:
+ the empty set or empty list (as in case PNil), a singleton set or singleton
+ list containing an atom (case PVar), or unions of atom sets or appended atom
+ lists (case PTup). This restriction will simplify proofs later on.
+ The 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:
\begin{center}
\begin{tabular}{ll}
- \it {\rm Foo}$_1$ p::pat q::pat t::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\;
+ \it {\rm Foo} p::pat q::pat t::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\;
\isacommand{bind}\;bn(q)\;\isacommand{in}\;t\\
- \it {\rm Foo}$_2$ x::name p::pat t::trm & \it \it \isacommand{bind}\;x\;\isacommand{in}\;t,\;
+ \it {\rm Foo}$'$x::name p::pat t::trm & \it \it \isacommand{bind}\;x\;\isacommand{in}\;t,\;
\isacommand{bind}\;bn(p)\;\isacommand{in}\;t
\end{tabular}
\end{center}
\noindent
- In the first case we bind all atoms from the pattern $p$ in $t$ and also all atoms
- from $q$ in $t$. As a result we have no way to determine whether the binder came from the
- binding function in $p$ or $q$. Similarly in the second case:
- the binder $bn(p)$ overlaps with the shallow binder $x$. We must exclude such specifiactions,
- as we will not be able to represent them using the general binders described in
- Section \ref{sec:binders}. However the following two term-constructors are allowed:
+ In the first case we bind all atoms from the pattern @{text p} in @{text t}
+ and also all atoms from @{text q} in @{text t}. As a result we have no way
+ to determine whether the binder came from the binding function @{text
+ "bn(p)"} or @{text "bn(q)"}. Similarly in the second case. There the binder
+ @{text "bn(p)"} overlaps with the shallow binder @{text x}. The reason why
+ we must exclude such specifiactions is that they cannot be represent by
+ the general binders described in Section \ref{sec:binders}. However
+ the following two term-constructors are allowed
\begin{center}
\begin{tabular}{ll}
- \it {\rm Bar}$_1$ p::pat t::trm s::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\;
+ \it {\rm Bar} p::pat t::trm s::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\;
\isacommand{bind}\;bn(p)\;\isacommand{in}\;s\\
- \it {\rm Bar}$_2$ p::pat t::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;p,\;
+ \it {\rm Bar}$'$p::pat t::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;p,\;
\isacommand{bind}\;bn(p)\;\isacommand{in}\;t\\
\end{tabular}
\end{center}
@@ -710,15 +718,19 @@
\noindent
since there is no overlap of binders.
- Let us come back one more time to the specification of simultaneous lets.
- A specification for them looks as follows:
+ Note that in the last example we wrote {\it\isacommand{bind}\;bn(p)\;\isacommand{in}\;p}.
+ Whenver such a binding clause is present, we will call the binder \emph{recursive}.
+ To see the purpose for this, consider ``plain'' Lets and Let\_recs:
\begin{center}
- \begin{tabular}{l}
+ \begin{tabular}{@ {}l@ {}}
\isacommand{nominal\_datatype} {\it trm} =\\
\hspace{5mm}\phantom{$\mid$}\ldots\\
\hspace{5mm}$\mid$ Let\;{\it a::assn}\; {\it t::trm}
\;\;\isacommand{bind} {\it bn(a)} \isacommand{in} {\it t}\\
+ \hspace{5mm}$\mid$ Let\_rec\;{\it a::assn}\; {\it t::trm}
+ \;\;\isacommand{bind} {\it bn(a)} \isacommand{in} {\it t},
+ \isacommand{bind} {\it bn(a)} \isacommand{in} {\it a}\\
\isacommand{and} {\it assn} =\\
\hspace{5mm}\phantom{$\mid$} ANil\\
\hspace{5mm}$\mid$ ACons\;{\it name}\;{\it trm}\;{\it assn}\\
@@ -729,65 +741,77 @@
\end{center}
\noindent
- The intention with this specification is to bind all variables
- from the assignments inside the body @{text t}. However one might
- like to consider the variant where the variables are not just
- bound in @{term t}, but also in the assignments themselves. In
- this case we need to specify
+ The difference is that with Let we only want to bind the atoms @{text
+ "bn(a)"} in the term @{text t}, but with Let\_rec we also want to bind the atoms
+ inside the assignment. This requires recursive binders and also has
+ consequences for the free variable function and alpha-equivalence relation,
+ which we are going to explain in the rest of this section.
+
+ Having dealt with all syntax matters, the problem now is how we can turn
+ specifications into actual type definitions in Isabelle/HOL and then
+ establish a reasoning infrastructure for them. Because of the problem
+ Pottier and Cheney pointed out, we cannot in general re-arrange arguments of
+ term-constructors so that binders and their bodies are next to each other, and
+ then use the type constructors @{text "abs_set"}, @{text "abs_res"} and
+ @{text "abs_list"} from Section \ref{sec:binders}. Therefore we will first
+ extract datatype definitions from the specification and then define an
+ alpha-equiavlence relation over them.
+
+
+ The datatype definition can be obtained by just stripping off the
+ binding clauses and the labels on the types. We also have to invent
+ new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}
+ given by user. In our implementation we just use an affix like
\begin{center}
- \begin{tabular}{l}
- Let\_rec\;{\it a::assn}\; {\it t::trm}
- \;\;\isacommand{bind} {\it bn(a)} \isacommand{in} {\it t},
- \isacommand{bind} {\it bn(a)} \isacommand{in} {\it a}\\
- \end{tabular}
+ @{text "ty\<^sup>\<alpha> \<mapsto> ty_raw"} \hspace{7mm} @{text "C\<^sup>\<alpha> \<mapsto> C_raw"}
\end{center}
\noindent
- where we bind also in @{text a} all the atoms @{text bn} returns. In this
- case we will say the binder is a \emph{recursive binder}.
-
- Having dealt with all syntax matters, the problem now is how we can turn
- specifications into actual type
- definitions in Isabelle/HOL and then establish a reasoning infrastructure
- for them. Because of the problem Pottier and Cheney pointed out, we cannot
- in general re-arrange arguments of term-constructors so that binders and
- their bodies next to each other, an then use the type constructors
- @{text "abs_set"}, @{text "abs_res"} and @{text "abs_list"} from Section
- \ref{sec:binders}. Therefore
- we will first extract datatype definitions from the specification and
- then define an alpha-equiavlence relation over them.
-
- The datatype definition can be obtained by just stripping of the
- binding clauses and the labels on the types. We also have to invent
- new names for the types, $ty^\alpha$ and term-constructors $C^\alpha$
- given by user. We just use an affix like
+ The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are
+ non-empty and the types in the constructors only occur in positive
+ position (see \cite{} for an indepth explanataion of the datatype package
+ in Isabelle/HOL). We then define the user-specified binding
+ functions by primitive recursion over the raw datatypes. We can also
+ easily define a permutation operation by primitive recursion so that for each
+ term constructor @{text "C_raw ty\<^isub>1 \<dots> ty\<^isub>n"} we have that
\begin{center}
- $ty^\alpha \mapsto ty\_raw \qquad C^\alpha \mapsto C\_raw$
+ @{text "p \<bullet> (C_raw x\<^isub>1 \<dots> x\<^isub>n) \<equiv> C_raw (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}
\end{center}
\noindent
- The datatype definition can be made, provided the usual conditions hold:
- the datatypes must be non-empty and they must only occur in positive
- position (see \cite{}). We then consider the user-specified binding
- functions and define them by primitive recursion over the raw datatypes.
+ From this definition we can easily show that the raw datatypes are
+ all permutation types (Def ??) by a simple structural induction over
+ the @{text "ty_raw"}s.
+
+ The first non-trivial step we have to perform is the generatation free-variable
+ functions from the specifications. Given types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}
+ we need to define the free-variable functions
+
+ \begin{center}
+ @{text "fv_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set \<dots> fv_ty\<^isub>n :: ty\<^isub>n \<Rightarrow> atom set"}
+ \end{center}
+
+ \noindent
+ and given binding functions @{text "bn_ty\<^isub>1, \<dots>, bn_ty\<^isub>m"} we also need to define
+ the free-variable functions
- The first non-trivial step we have to generate free-variable
- functions from the specifications. The basic idea is to collect
- all atoms that are not bound, but because of the rather complicated
- binding mechanisms the details are somewhat involved.
- There are two kinds of free-variable functions: one corresponds to types,
- written $\fv\_ty$, and the other corresponds to binding functions,
- written $\fv\_bn$. They have to be defined at the same time, since there can
- be dependencies between them.
+ \begin{center}
+ @{text "fv_bn_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set \<dots> fv_bn_ty\<^isub>m :: ty\<^isub>m \<Rightarrow> atom set"}
+ \end{center}
- Given a term-constructor $C\_raw\;ty_1 \ldots ty_n$, of type $ty$ together with
- some binding clauses, the function $\fv\_ty (C\_raw\;x_1 \ldots x_n)$ will be
- the union of the values generated for each argument, say $x_i$ with type $ty_i$.
- By the binding clause we know whether the argument $x_i$ is a shallow or deep
- binder and in the latter case also whether it is a recursive or non-recursive
- of a binder. In these cases we return as value:
+ \noindent
+ The basic idea behind these free-variable functions is to collect all atoms
+ that are not bound in a term constructor, but because of the rather
+ complicated binding mechanisms the details are somewhat involved.
+
+ Given a term-constructor @{text "C_raw ty\<^isub>1 \<dots> ty\<^isub>n"}, of type @{text ty} together with
+ some binding clauses, the function @{text "fv_ty (C_raw x\<^isub>1 \<dots> x\<^isub>n)"} will be
+ the union of the values defined below for each argument, say @{text "x\<^isub>i"} with type @{text "ty\<^isub>i"}.
+ From the binding clause of this term constructor, we can determine whether the
+ argument @{text "x\<^isub>i"} is a shallow or deep binder, and in the latter case also
+ whether it is a recursive or non-recursive of a binder. In these cases the value is:
\begin{center}
\begin{tabular}{cp{7cm}}
@@ -798,12 +822,13 @@
\end{center}
\noindent
- The binding clause will also give us whether the argument @{term "x\<^isub>i"} is
- a body of one or more abstractions. There are two cases: either the
+ In case the argument @{text "x\<^isub>i"} is not a binder, it might be a body of
+ one or more abstractions. There are two cases: either the
corresponding binders are all shallow or there is a single deep binder.
In the former case we build the union of all shallow binders; in the
later case we just take set or list of atoms the specified binding
- function returns. Below use @{text "bnds"} to stand for them.
+ function returns. Let @{text "bnds"} be an abbreviation of the bound
+ atoms. Then the value is given by:
\begin{center}
\begin{tabular}{cp{7cm}}
@@ -816,13 +841,37 @@
\end{center}
\noindent
- If the argument is neither a binder, nor a body, then it is defined as
- the four clauses above, except that @{text "bnds"} is empty. i.e.~no atoms
+ If the argument is neither a binder, nor a body of an abstraction, then the
+ value is defined as above, except that @{text "bnds"} is empty. i.e.~no atoms
are abstracted.
+ TODO
+
+ Given a clause of a binding function of the form
+
+ \begin{center}
+ @{text "bn_ty (C_raw x\<^isub>1 \<dots> x\<^isub>n) = rhs"}
+ \end{center}
+
+ \noindent
+ then the corresponding free-variable function @{text "fv_bn_ty\<^isub>i"} is the
+ union of the values calculated for the @{text "x\<^isub>j"} as follows:
+
+ \begin{center}
+ \begin{tabular}{cp{7cm}}
+ $\bullet$ & @{text "{}"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} and is an atom\\
+ $\bullet$ & @{text "fv_bn_ty x\<^isub>j"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"}
+ with the recursive call @{text "bn_ty x\<^isub>j"}\\
+ $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\
+ $\bullet$ & @{text "(atoml x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\
+ $\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is a nominal datatype\\
+ $\bullet$ & @{term "{}"} otherwise
+ \end{tabular}
+ \end{center}
+
*}
-
+section {* The Lifting of Definitions and Properties *}
text {*
Restrictions