--- a/LMCS-Paper/Paper.thy Wed Feb 29 04:56:06 2012 +0000
+++ b/LMCS-Paper/Paper.thy Wed Feb 29 16:23:11 2012 +0000
@@ -115,7 +115,8 @@
type-variables. While it is possible to implement this kind of more general
binders by iterating single binders, like @{text "\<forall>x\<^isub>1.\<forall>x\<^isub>2...\<forall>x\<^isub>n.T"}, this leads to a rather clumsy
formalisation of W. For example, the usual definition when a
- type is an instance of a type-scheme requires the following auxiliary \emph{unbinding relation}
+ type is an instance of a type-scheme requires in the iterated version
+ the following auxiliary \emph{unbinding relation}
\[
\infer{@{text T} \hookrightarrow ([], @{text T})}{}\qquad
@@ -124,11 +125,12 @@
\]\smallskip
\noindent
- which relates a type-scheme with a list of variables and a type. The point of this
- definition is to get access to the bound variables and the type-part of a type-scheme
- @{text S}, though in general
- we will only get access to some variables and some type @{text T} that are
- ``alpha-equivalent'' to @{text S}. This is because unbinding is a relation, not a function.
+ which relates a type-scheme with a list of type-variables and a type. The point of this
+ definition is: given a type-scheme @{text S}, how to get access to the bound type-variables
+ and the type-part of this type-scheme? The unbinding relation gives an answer, though in general
+ we will only get access to some type-variables and some type that are
+ ``alpha-equivalent'' to @{text S}. This is because unbinding is a relation; it cannot be a function
+ for alpha-equated type-schemes.
Still, with this
definition in place we can formally define when a type is an instance of a type-scheme as
@@ -137,19 +139,20 @@
\]\smallskip
\noindent
- meaning there exists a list of variables @{text xs} and a type @{text T'} to which
+ meaning there exists a list of type-variables @{text xs} and a type @{text T'} to which
the type-scheme @{text S} unbinds, and there exists a substitution whose domain is
@{text xs} (seen as set) such that @{text "\<sigma>(T') = T"}.
The problem with this definition is that we cannot follow the usual proofs
that are by induction on the type-part of the type-scheme (since it is under
- an existential quantifier). The representation of type-schemes using iterations of single binders
- prevents us from directly ``unbinding'' the bound variables and the type-part of
- a type-scheme. The purpose of this paper is to introduce general binders, which
+ an existential quantifier and only an alpha-variant). The representation of
+ type-schemes using iterations of single binders
+ prevents us from directly ``unbinding'' the bound thye-variables and the type-part.
+ The purpose of this paper is to introduce general binders, which
allow us to represent type-schemes so that they can bind multiple variables at once
and as a result solve this problem.
The need of iterating single binders is also one reason
why Nominal Isabelle and similar theorem provers that only provide
- mechanisms for binding single variables have not fared extremely well with
+ mechanisms for binding single variables have so far not fared very well with
the more advanced tasks in the POPLmark challenge \cite{challenge05},
because also there one would like to bind multiple variables at once.
@@ -500,7 +503,7 @@
Permutations are bijective functions from atoms to atoms that are
the identity everywhere except on a finite number of atoms. There is a
two-place permutation operation written
- @{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
+ @{text "_ \<bullet> _ "} and having the type @{text "perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
where the generic type @{text "\<beta>"} is the type of the object
over which the permutation
acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},
@@ -623,7 +626,7 @@
\end{equation}\smallskip
\noindent
- If a function is of type @{text "\<alpha> \<Rightarrow> \<beta>"}, this definition is equivalent to
+ If a function is of type @{text "\<alpha> \<Rightarrow> \<beta>"}, say, this definition is equivalent to
the fact that a permutation applied to the application
@{text "f x"} can be moved to the argument @{text x}. That means for
such functions, we have for all permutations @{text "\<pi>"}:
@@ -898,16 +901,14 @@
\end{equation}\smallskip
\noindent
- and also
+ and also set
\begin{equation}\label{absperm}
- @{thm permute_Abs(1)[where p="\<pi>", no_vars]}
+ @{thm permute_Abs(1)[where p="\<pi>", no_vars, THEN eq_reflection]}
\end{equation}\smallskip
\noindent
- The second fact derives from the definition of permutations acting on pairs
- \eqref{permute} and alpha-equivalence being equivariant
- (see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show
+ With this at our disposal, we can show
the following lemma about swapping two atoms in an abstraction.
\begin{lem}
@@ -963,7 +964,8 @@
\noindent
This is because for every finite set of atoms, say @{text "bs"}, we have
- @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
+ @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.\footnote{Note that this is not
+ the case for infinite sets.}
Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes
the first equation of Theorem~\ref{suppabs}. The others are similar.
@@ -1043,7 +1045,7 @@
recursive arguments need to satisfy a `positivity' restriction, which
ensures that the type has a set-theoretic semantics (see
\cite{Berghofer99}). If the types are polymorphic, we require the
- type variables stand for types that are finitely supported and over which
+ type variables to stand for types that are finitely supported and over which
a permutation operation is defined.
The labels @{text "label"}$_{1..l}$ annotated on the types are optional. Their
purpose is to be used in the (possibly empty) list of \emph{binding
@@ -1200,7 +1202,8 @@
\begin{equation}\label{letrecs}
\mbox{%
\begin{tabular}{@ {}l@ {}l}
- \isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\
+ \isacommand{nominal\_datatype}~@{text "trm ="}\\
+ \hspace{5mm}\phantom{$\mid$}~\ldots\\
\hspace{5mm}$\mid$~@{text "Let as::assn t::trm"}
& \hspace{-19mm}\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text t}\\
\hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}
@@ -1236,11 +1239,14 @@
\noindent
Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"} pick
- out different atoms to become bound, respectively be free, in @{text "p"}.
- (Since the Ott-tool does not derive a reasoning infrastructure for
- alpha-equated terms with deep binders, it can permit such specifications.)
- For convenience we exlude such specifications even if @{text "bn\<^isub>1"} and
- @{text "bn\<^isub>2"} are the same binding functions, which would otherwise be harmless.
+ out different atoms to become bound, respectively be free,
+ in @{text "p"}.\footnote{Although harmless, in our implementation
+ we exlude such specifications even
+ if @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"} are the same binding
+ functions.}$^,$\footnote{Since the Ott-tool does not derive a reasoning
+ infrastructure for
+ alpha-equated terms with deep binders, it can permit such specifications.}
+
We also need to restrict the form of the binding functions in order to
ensure the @{text "bn"}-functions can be defined for alpha-equated
@@ -2228,7 +2234,7 @@
is straightforward to establish that the sizes decrease in every
induction step. What is left to show is that we covered all cases.
To do so, we have to derive stronger cases lemmas, which look in our
- running example are as follows:
+ running example as follows:
\[\mbox{
\begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}