--- a/LMCS-Paper/Paper.thy Tue Apr 10 16:02:30 2012 +0100
+++ b/LMCS-Paper/Paper.thy Thu Apr 12 01:39:54 2012 +0100
@@ -114,9 +114,9 @@
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, 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 in the iterated version
- the following auxiliary \emph{unbinding relation}
+ formalisation of W. For example, the usual definition for a
+ type being an instance of a type-scheme requires in the iterated version
+ the following auxiliary \emph{unbinding relation}:
\[
\infer{@{text T} \hookrightarrow ([], @{text T})}{}\qquad
@@ -127,14 +127,12 @@
\noindent
Its purpose is to relate a type-scheme with a list of type-variables and a type. It is used to
address the following problem:
- Given a type-scheme @{text S}, how does one get access to the bound type-variables
- and the type-part of @{text S}? The unbinding relation gives an answer, though in general
- we will only get access to some type-variables and some type that are
+ Given a type-scheme, say @{text S}, how does one get access to the bound type-variables
+ and the type-part of @{text S}? The unbinding relation gives an answer to this problem, though
+ in general it will only provide some list of type-variables together with a 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 follows:
+ for alpha-equated type-schemes. With this
+ definition in place we can formally define when a type is an instance of a type-scheme as follows:
\[
@{text "T \<prec> S \<equiv> \<exists>xs T' \<sigma>. S \<hookrightarrow> (xs, T') \<and> dom \<sigma> = set xs \<and> \<sigma>(T') = T"}
@@ -142,16 +140,17 @@
\noindent
This means 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
+ the type-scheme @{text S} unbinds, and there exists a substitution @{text "\<sigma>"} 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 and only an alpha-variant). The representation of
type-schemes using iterations of single binders
prevents us from directly ``unbinding'' the bound type-variables and the type-part.
+ Clearly, some more dignified approach to formalising algorithm W is desirable.
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.
+ and as a result solve this problem more straightforwardly.
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 so far not fared very well with
@@ -509,7 +508,8 @@
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"},
- the composition of two permutations @{term "\<pi>\<^isub>1"} and @{term "\<pi>\<^isub>2"} as \mbox{@{term "\<pi>\<^isub>1 + \<pi>\<^isub>2"}},
+ the composition of two permutations @{term "\<pi>\<^isub>1"} and @{term "\<pi>\<^isub>2"} as \mbox{@{term "\<pi>\<^isub>1 + \<pi>\<^isub>2"}}
+ (even if this operation is non-commutative),
and the inverse permutation of @{term "\<pi>"} as @{text "- \<pi>"}. The permutation
operation is defined over Isabelle/HOL's type-hierarchy \cite{HuffmanUrban10};
for example permutations acting on atoms, products, lists, permutations, sets,
@@ -1232,20 +1232,17 @@
\[\mbox{
\begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
@{text "Baz\<^isub>1 p::pat t::trm"} &
- \isacommand{binds} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\
+ \isacommand{binds} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text "p t"}\\
@{text "Baz\<^isub>2 p::pat t\<^isub>1::trm t\<^isub>2::trm"} &
- \isacommand{binds} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "t\<^isub>1"},
- \isacommand{binds} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "t\<^isub>2"}\\
+ \isacommand{binds} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "p t\<^isub>1"},
+ \isacommand{binds} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "p t\<^isub>2"}\\
\end{tabular}}
\]\smallskip
\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"}.\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
+ in @{text "p"}.\footnote{Since the Ott-tool does not derive a reasoning
infrastructure for
alpha-equated terms with deep binders, it can permit such specifications.}
@@ -1291,13 +1288,35 @@
unions of atom sets or appended atom lists (case @{text ACons'}). This
restriction will simplify some automatic definitions and proofs later on.
- In order to simplify our definitions of free atoms and alpha-equivalence,
- we shall assume specifications
- of term-calculi are implicitly \emph{completed}. By this we mean that
- for every argument of a term-constructor that is \emph{not}
- already part of a binding clause given by the user, we add implicitly a special \emph{empty} binding
- clause, written \isacommand{binds}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case
- of the lambda-terms, the completion produces
+ To sum up this section, we introduced nominal datatype
+ specifications, which are like standard datatype specifications in
+ Isabelle/HOL extended with specifications for binding
+ functions. Each constructor argument in our specification can also
+ have an optional label. These labels are used in the binding clauses
+ of a constructor; there can be several binding clauses for each
+ constructor, but bodies of binding clauses can only occur in a
+ single one. Binding clauses come in three modes: \isacommand{binds},
+ \isacommand{binds (set)} and \isacommand{binds (set+)}. Binders
+ fall into two categories: shallow binders and deep binders. Shallow
+ binders can occur in more than one binding clause and only have to
+ respect the binding mode (i.e.~be of the right type). Deep binders
+ can also occur in more than one binding clause, unless they are
+ recursive in which case they can only occur once. Each of the deep
+ binders can only have a single binding function. Binding functions
+ are defined by recursion over a nominal datatype. They can only
+ return the empty set, singleton atoms and unions of sets of atoms
+ (for binding modes \isacommand{binds (set)} and \isacommand{binds
+ (set+)}), and the empty list, singleton atoms and appended lists of
+ atoms (for mode \isacommand{bind}). However, they can only return
+ atoms that are not mentioned in any binding clause. In order to
+ simplify our definitions of free atoms and alpha-equivalence, we
+ shall assume specifications of term-calculi are implicitly
+ \emph{completed}. By this we mean that for every argument of a
+ term-constructor that is \emph{not} already part of a binding clause
+ given by the user, we add implicitly a special \emph{empty} binding
+ clause, written \isacommand{binds}~@{term
+ "{}"}~\isacommand{in}~@{text "labels"}. In case of the lambda-terms,
+ the completion produces
\[\mbox{
\begin{tabular}{@ {}l@ {\hspace{-1mm}}}