--- a/LMCS-Paper/Paper.thy Wed Feb 22 12:10:17 2012 +0000
+++ b/LMCS-Paper/Paper.thy Wed Feb 29 03:12:52 2012 +0000
@@ -113,11 +113,39 @@
\noindent
and the @{text "\<forall>"}-quantification binds a finite (possibly empty) set of
type-variables. While it is possible to implement this kind of more general
- binders by iterating single binders, this leads to a rather clumsy
- formalisation of W.
+ 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}
+
+ \[
+ \infer{@{text T} \hookrightarrow ([], @{text T})}{}\qquad
+ \infer{\forall @{text x.S} \hookrightarrow (@{text x}\!::\!@{text xs}, @{text T})}
+ {@{text S} \hookrightarrow (@{text xs}, @{text T})}
+ \]\smallskip
- {\bf add example about W}
+ \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}---it is an unbinding \emph{relation}. Still, with this
+ definition in place we can formally define when a type is an instance of a type-scheme as
+ \[
+ @{text "T \<prec> S \<equiv> \<exists>xs T' \<sigma>. S \<hookrightarrow> (xs, T') \<and> dom \<sigma> = set xs \<and> \<sigma>(T') = T"}
+ \]\smallskip
+
+ \noindent
+ meaning there exists a list of 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 pain 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 by iterating 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
+ allow us to represent type-schemes following closely informal practice 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
@@ -393,7 +421,7 @@
\noindent
{\bf Contributions:} We provide three new definitions for when terms
involving general binders are alpha-equivalent. These definitions are
- inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic
+ inspired by earlier work of Pitts \cite{Pitts04}. By means of automatically-generated
proofs, we establish a reasoning infrastructure for alpha-equated terms,
including properties about support, freshness and equality conditions for
alpha-equated terms. We are also able to automatically derive strong
@@ -578,24 +606,26 @@
two properties.
\begin{prop}\label{supportsprop}
- Given a set @{text "as"} of atoms.\\
- {\it (i)} If @{thm (prem 1) supp_is_subset[where S="as", no_vars]}
- and @{thm (prem 2) supp_is_subset[where S="as", no_vars]} then
- @{thm (concl) supp_is_subset[where S="as", no_vars]}.\\
+ Given a set @{text "bs"} of atoms.\\
+ {\it (i)} If @{thm (prem 1) supp_is_subset[where S="bs", no_vars]}
+ and @{thm (prem 2) supp_is_subset[where S="bs", no_vars]} then
+ @{thm (concl) supp_is_subset[where S="bs", no_vars]}.\\
{\it (ii)} @{thm supp_supports[no_vars]}.
\end{prop}
Another important notion in the nominal logic work is \emph{equivariance}.
- For a function @{text f}, say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant
+ For a function @{text f} to be equivariant
it is required that every permutation leaves @{text f} unchanged, that is
\begin{equation}\label{equivariancedef}
@{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}
\end{equation}\smallskip
- \noindent or equivalently that a permutation applied to the application
- @{text "f x"} can be moved to the argument @{text x}. That means for equivariant
- functions @{text f}, we have for all permutations @{text "\<pi>"}:
+ \noindent
+ If a function is of type @{text "\<alpha> \<Rightarrow> \<beta>"}, 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
+ functions @{text f} of type @{text "\<alpha> \<Rightarrow> \<beta>"}, we have for all permutations @{text "\<pi>"}:
\begin{equation}\label{equivariance}
@{text "\<pi> \<bullet> f = f"} \;\;\;\;\textit{if and only if}\;\;\;\;
@@ -603,21 +633,26 @@
\end{equation}\smallskip
\noindent
- From property \eqref{equivariancedef} and the definition of @{text supp}, we
- can easily deduce that equivariant functions have empty support. There is
- also a similar notion for equivariant relations, say @{text R}, namely the property
- that
+ There is
+ also a similar property for relations, which are in HOL functions of type @{text "\<alpha> \<Rightarrow> \<beta> \<Rightarrow> bool"}.
+ Suppose a relation @{text R}, then
+ that for all permutations @{text \<pi>}:
\[
- @{text "x R y"} \;\;\textit{implies}\;\; @{text "(\<pi> \<bullet> x) R (\<pi> \<bullet> y)"}
+ @{text "\<pi> \<bullet> R = R"} \;\;\;\;\textit{if and only if}\;\;\;\;
+ @{text "\<forall>x y."}~~@{text "x R y"} \;\textit{implies}\; @{text "(\<pi> \<bullet> x) R (\<pi> \<bullet> y)"}
\]\smallskip
-
+
+ \noindent
+ Note that from property \eqref{equivariancedef} and the definition of @{text supp}, we
+ can easily deduce that equivariant functions have empty support.
+
Using freshness, the nominal logic work provides us with general means for renaming
binders.
\noindent
While in the older version of Nominal Isabelle, we used extensively
- Property~\ref{swapfreshfresh} to rename single binders, this property
+ Proposition~\ref{swapfreshfresh} to rename single binders, this property
proved too unwieldy for dealing with multiple binders. For such binders the
following generalisations turned out to be easier to use.
@@ -677,9 +712,9 @@
the notion of alpha-equivalence that is \emph{not} preserved by adding
vacuous binders.) To answer this question, we identify four conditions: {\it (i)}
given a free-atom function @{text "fa"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
- set"}}, then @{text x} and @{text y} need to have the same set of free
+ set"}}, then @{text "(as, x)"} and @{text "(bs, y)"} need to have the same set of free
atoms; moreover there must be a permutation @{text \<pi>} such that {\it
- (ii)} @{text \<pi>} leaves the free atoms of @{text x} and @{text y} unchanged, but
+ (ii)} @{text \<pi>} leaves the free atoms of @{text "(as, x)"} and @{text "(bs, y)"} unchanged, but
{\it (iii)} `moves' their bound names so that we obtain modulo a relation,
say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)}
@{text \<pi>} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
@@ -755,7 +790,7 @@
\noindent
Now recall the examples shown in \eqref{ex1} and
\eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and
- @{text "({y, x}, y \<rightarrow> x)"} are alpha-equivalent according to
+ @{text "({x, y}, y \<rightarrow> x)"} are alpha-equivalent according to
$\approx_{\,\textit{set}}$ and $\approx_{\,\textit{set+}}$ by taking @{text "\<pi>"} to
be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"}, then @{text
"([x, y], x \<rightarrow> y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"}
@@ -891,7 +926,7 @@
\end{proof}
\noindent
- Assuming that @{text "x"} has finite support, this lemma together
+ This lemma together
with \eqref{absperm} allows us to show
\begin{equation}\label{halfone}
@@ -900,8 +935,8 @@
\noindent
which by Property~\ref{supportsprop} gives us `one half' of
- Theorem~\ref{suppabs}. The `other half' is a bit more involved. To establish
- it, we use a trick from \cite{Pitts04} and first define an auxiliary
+ Theorem~\ref{suppabs}. To establish the `other half', we
+ use a trick from \cite{Pitts04} and first define an auxiliary
function @{text aux}, taking an abstraction as argument
\[
@@ -1007,7 +1042,9 @@
\emph{recursive argument} of @{text "C\<^sup>\<alpha>"}. The types of such
recursive arguments need to satisfy a `positivity' restriction, which
ensures that the type has a set-theoretic semantics (see
- \cite{Berghofer99}). The labels annotated on the types are optional. Their
+ \cite{Berghofer99}). If the types are polymorphic, we require the
+ type variables are of finitely supported type.
+ The labels annotated on the types are optional. Their
purpose is to be used in the (possibly empty) list of \emph{binding
clauses}, which indicate the binders and their scope in a term-constructor.
They come in three \emph{modes}:
@@ -2468,7 +2505,8 @@
Isabelle. First, it is far too complicated to be a basis for automated
proofs implemented on the ML-level of Isabelle/HOL. Second, it covers cases
of binders depending on other binders, which just do not make sense for our
- alpha-equated terms. Third, it allows empty types that have no meaning in a
+ alpha-equated terms (the corresponding @{text "fa"}-functions would not lift).
+ Third, it allows empty types that have no meaning in a
HOL-based theorem prover. We also had to generalise slightly Ott's binding
clauses. In Ott one specifies binding clauses with a single body; we allow
more than one. We have to do this, because this makes a difference for our