--- a/Paper/Paper.thy Tue Mar 30 17:52:16 2010 +0200
+++ b/Paper/Paper.thy Tue Mar 30 17:55:46 2010 +0200
@@ -955,8 +955,8 @@
\begin{center}
\begin{tabular}{ll}
@{text "Foo x::name y::name t::lam"} &
- \isacommand{bind} @{text x} \isacommand{in} @{text t},\;
- \isacommand{bind} @{text y} \isacommand{in} @{text t}
+ \isacommand{bind} @{text x} \isacommand{in} @{text t},\;
+ \isacommand{bind} @{text y} \isacommand{in} @{text t}
\end{tabular}
\end{center}
@@ -1004,12 +1004,12 @@
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
+ example above that the term-constructors @{text PVar} and @{text 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 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 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
@@ -1097,10 +1097,10 @@
given by user. In our implementation we just use an affix @{text "_raw"}.
For the purpose of the paper we just use superscripts to indicate a
notion defined over alpha-equivalence classes and leave out the superscript
- for the corresponding notion on the ``raw'' level. So for example:
+ for the corresponding notion on the ``raw'' level. So for example we have
\begin{center}
- @{text "ty\<^sup>\<alpha> \<mapsto> ty"} \hspace{7mm} @{text "C\<^sup>\<alpha> \<mapsto> C"}
+ @{text "ty\<^sup>\<alpha> \<mapsto> ty"} \hspace{2mm}and\hspace{2mm} @{text "C\<^sup>\<alpha> \<mapsto> C"}
\end{center}
\noindent
@@ -1123,20 +1123,20 @@
%the @{text "ty"}s.
The first non-trivial step we have to perform is the generation free-variable
- functions from the specifications. Given types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}
- we need to define the free-variable functions
+ functions from the specifications. Given the raw types @{text "ty\<^isub>1 \<dots> ty\<^isub>n"}
+ we need to define 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"}
+ @{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
We define them together with the auxiliary free variable functions for
- binding functions. Given binding functions of types
- @{text "bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> \<dots> \<dots> bn\<^isub>m :: ty\<^isub>i\<^isub>m \<Rightarrow> \<dots>"} we need to define
+ binding functions. Given binding functions for raw types
+ @{text "bn_ty\<^isub>1 \<dots> bn_ty\<^isub>m"} we need to define
\begin{center}
- @{text "fv_bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> atom set \<dots> fv_bn\<^isub>m :: ty\<^isub>i\<^isub>m \<Rightarrow> atom set"}
+ @{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}
\noindent
@@ -1144,31 +1144,33 @@
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 ty\<^isub>1 \<dots> ty\<^isub>n"}, of type @{text ty} together with
- some binding clauses, the function @{text "fv_ty (C 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:
+ Given a term-constructor @{text "C"} of type @{text ty} with argument types
+ @{text "ty\<^isub>1 \<dots> ty\<^isub>n"} and some binding clauses, the function
+ @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be the union of the values
+ defined below for each argument. From the binding clause of this term
+ constructor, we can determine whether the argument is a shallow or deep
+ binder, and in the latter case also whether it is a recursive or
+ non-recursive binder. In case the argument, say @{text "x\<^isub>i"} with
+ type @{text "ty\<^isub>i"}, is a binder, the value is:
\begin{center}
\begin{tabular}{cp{7cm}}
$\bullet$ & @{term "{}"} provided @{text "x\<^isub>i"} is a shallow binder\\
- $\bullet$ & @{text "fv_bn\<^isub>j x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep
- non-recursive binder with the auxiliary function @{text "bn\<^isub>j"}\\
- $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i - bn\<^isub>j x\<^isub>i"} provided @{text "x\<^isub>i"} is
- a deep recursive binder with the auxiliary function @{text "bn\<^isub>j"}
+ $\bullet$ & @{text "fv_bn_ty\<^isub>i x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep
+ non-recursive binder with the auxiliary function @{text "bn_ty\<^isub>i"}\\
+ $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i - bn_ty\<^isub>i x\<^isub>i"} provided @{text "x\<^isub>i"} is
+ a deep recursive binder with the auxiliary function @{text "bn_ty\<^isub>i"}
\end{tabular}
\end{center}
\noindent
In case the argument @{text "x\<^isub>i"} is not a binder, it might be a body of
- one or more abstractions. Let @{text "bnds"} be the bound atoms computed
+ one or more abstractions. Let @{text "bnds"} be the set of bound atoms calculated
as follows: If @{text "x\<^isub>i"} is not a body of an abstraction @{term "{}"}.
Otherwise 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
+ later case we just take the set of atoms specified binding
function returns. With @{text "bnds"} computed as above the value of
for @{text "x\<^isub>i"} is given by:
@@ -1177,17 +1179,18 @@
$\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\
$\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\
$\bullet$ & @{text "(atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\
- $\bullet$ & @{text "(fv_ty\<^isub>m x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is one of the datatypes
- we are defining, with the free variable function @{text "fv_ty\<^isub>m"}\\
+ $\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is one of the datatypes
+ we are defining with the free variable function @{text "fv_ty\<^isub>i"}\\
% $\bullet$ & @{text "(fv\<^isup>\<alpha> x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a defined nominal datatype
% with a free variable function @{text "fv\<^isup>\<alpha>"}\\
$\bullet$ & @{term "{}"} otherwise
\end{tabular}
\end{center}
- \noindent Next, for each binding function @{text "bn"} we define a
- free variable function @{text "fv_bn"}. The basic idea behind this
- function is to compute all the free atoms under this binding
+ \noindent
+ Next, for each binding function @{text "bn_ty"} we define a
+ free variable function @{text "fv_bn_ty"}. The basic idea behind this
+ function is to compute all the free atoms that are not bound by the binding
function. So given that @{text "bn"} is a binding function for type
@{text "ty\<^isub>i"} it will be the same as @{text "fv_ty\<^isub>i"} with the
omission of the arguments present in @{text "bn"}.