--- a/LMCS-Paper/Paper.thy Wed Feb 29 03:13:45 2012 +0000
+++ b/LMCS-Paper/Paper.thy Wed Feb 29 04:56:06 2012 +0000
@@ -128,7 +128,8 @@
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
+ ``alpha-equivalent'' to @{text S}. This is because unbinding is a relation, not a function.
+ Still, with this
definition in place we can formally define when a type is an instance of a type-scheme as
\[
@@ -139,13 +140,13 @@
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
+ 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 by iterating single binders
+ 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
- allow us to represent type-schemes following closely informal practice and as
- a result solve this problem.
+ 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
@@ -160,7 +161,7 @@
the second pair should \emph{not} be alpha-equivalent:
\begin{equation}\label{ex1}
- @{text "\<forall>{x, y}. x \<rightarrow> y \<approx>\<^isub>\<alpha> \<forall>{y, x}. y \<rightarrow> x"}\hspace{10mm}
+ @{text "\<forall>{x, y}. x \<rightarrow> y \<approx>\<^isub>\<alpha> \<forall>{x, y}. y \<rightarrow> x"}\hspace{10mm}
@{text "\<forall>{x, y}. x \<rightarrow> y \<notapprox>\<^isub>\<alpha> \<forall>{z}. z \<rightarrow> z"}
\end{equation}\smallskip
@@ -421,7 +422,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 automatically-generated
+ inspired by earlier work of Pitts \cite{Pitts04}. By means of automati\-cally-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
@@ -519,7 +520,7 @@
\end{tabular} &
\begin{tabular}{@ {}l@ {}}
@{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", no_vars, THEN eq_reflection]}\\
- @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+ @{thm permute_set_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
@{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f (- \<pi> \<bullet> x))"}\\
@{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}
\end{tabular}
@@ -618,34 +619,33 @@
it is required that every permutation leaves @{text f} unchanged, that is
\begin{equation}\label{equivariancedef}
- @{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}
+ @{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}\;.
\end{equation}\smallskip
\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>"}:
+ such functions, we have for all permutations @{text "\<pi>"}:
\begin{equation}\label{equivariance}
@{text "\<pi> \<bullet> f = f"} \;\;\;\;\textit{if and only if}\;\;\;\;
- @{text "\<forall>x. \<pi> \<bullet> (f x) = f (\<pi> \<bullet> x)"}
+ @{text "\<forall>x. \<pi> \<bullet> (f x) = f (\<pi> \<bullet> x)"}\;.
\end{equation}\smallskip
\noindent
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>}:
+ Suppose a relation @{text R}, then for all permutations @{text \<pi>}:
\[
@{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)"}
+ @{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.
+ can easily deduce that for a function being equivariant is equivalent to having empty support.
Using freshness, the nominal logic work provides us with general means for renaming
binders.
@@ -1043,8 +1043,9 @@
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 are of finitely supported type.
- The labels annotated on the types are optional. Their
+ type variables 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
clauses}, which indicate the binders and their scope in a term-constructor.
They come in three \emph{modes}:
@@ -1238,7 +1239,9 @@
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.
+
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
terms. The main restriction is that we cannot return an atom in a binding