
diff -r 860df8e1262f -r d3d5225f4f24 LMCS-Paper/Paper.thy
--- 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




