--- a/Paper/Paper.thy Thu Oct 07 14:23:32 2010 +0900
+++ b/Paper/Paper.thy Fri Oct 08 13:41:54 2010 +0100
@@ -87,13 +87,14 @@
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. The need of iterating single binders is also one reason
- why Nominal Isabelle
+ formalisation of W.
+ %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
- has not fared extremely well with the
- more advanced tasks in the POPLmark challenge \cite{challenge05}, because
- also there one would like to bind multiple variables at once.
+ %has not fared extremely well with the
+ %more advanced tasks in the POPLmark challenge \cite{challenge05}, because
+ %also there one would like to bind multiple variables at once.
Binding multiple variables has interesting properties that cannot be captured
easily by iterating single binders. For example in the case of type-schemes we do not
@@ -274,7 +275,7 @@
Although in informal settings a reasoning infrastructure for $\alpha$-equated
terms is nearly always taken for granted, establishing it automatically in
the Isabelle/HOL is a rather non-trivial task. For every
- specification we will need to construct a type containing as elements the
+ specification we will need to construct type(s) containing as elements the
$\alpha$-equated terms. To do so, we use the standard HOL-technique of defining
a new type by identifying a non-empty subset of an existing type. The
construction we perform in Isabelle/HOL can be illustrated by the following picture:
@@ -309,8 +310,8 @@
the type of sets of raw terms according to our $\alpha$-equivalence relation,
and finally define the new type as these $\alpha$-equivalence classes
(non-emptiness is satisfied whenever the raw terms are definable as datatype
- in Isabelle/HOL and the property that our relation for $\alpha$-equivalence is
- indeed an equivalence relation).
+ in Isabelle/HOL and our relation for $\alpha$-equivalence is
+ an equivalence relation).
%The fact that we obtain an isomorphism between the new type and the
%non-empty subset shows that the new type is a faithful representation of
@@ -379,9 +380,9 @@
from the Ott-tool, but we introduce crucial restrictions, and also extensions, so
that our specifications make sense for reasoning about $\alpha$-equated terms.
The main improvement over Ott is that we introduce three binding modes
- (only one is present in Ott), provide definitions for $\alpha$-equivalence and
+ (only one is present in Ott), provide formalised definitions for $\alpha$-equivalence and
for free variables of our terms, and also derive a reasoning infrastructure
- for our specifications inside Isabelle/HOL.
+ for our specifications inside Isabelle/HOL from ``first principles''.
%\begin{figure}
@@ -459,20 +460,37 @@
for example permutations acting on products, lists, sets, functions and booleans is
given by:
%
- \begin{equation}\label{permute}
- \mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
+ %\begin{equation}\label{permute}
+ %\mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
+ %\begin{tabular}{@ {}l@ {}}
+ %@{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\[2mm]
+ %@{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\
+ %@{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\
+ %\end{tabular} &
+ %\begin{tabular}{@ {}l@ {}}
+ %@{thm permute_set_eq[no_vars, THEN eq_reflection]}\\
+ %@{text "p \<bullet> f \<equiv> \<lambda>x. p \<bullet> (f (- p \<bullet> x))"}\\
+ %@{thm permute_bool_def[no_vars, THEN eq_reflection]}
+ %\end{tabular}
+ %\end{tabular}}
+ %\end{equation}
+ %
+ \begin{center}
+ \mbox{\begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {\hspace{4mm}}c@ {}}
\begin{tabular}{@ {}l@ {}}
- @{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\[2mm]
+ @{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\
+ @{thm permute_bool_def[no_vars, THEN eq_reflection]}
+ \end{tabular} &
+ \begin{tabular}{@ {}l@ {}}
@{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\
@{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\
\end{tabular} &
\begin{tabular}{@ {}l@ {}}
@{thm permute_set_eq[no_vars, THEN eq_reflection]}\\
@{text "p \<bullet> f \<equiv> \<lambda>x. p \<bullet> (f (- p \<bullet> x))"}\\
- @{thm permute_bool_def[no_vars, THEN eq_reflection]}
\end{tabular}
\end{tabular}}
- \end{equation}
+ \end{center}
\noindent
Concrete permutations in Nominal Isabelle are built up from swappings,
@@ -504,11 +522,12 @@
A striking consequence of these definitions is that we can prove
without knowing anything about the structure of @{term x} that
swapping two fresh atoms, say @{text a} and @{text b}, leaves
- @{text x} unchanged:
+ @{text x} unchanged, namely if @{text "a \<FRESH> x"} and @{text "b \<FRESH> x"}
+ then @{term "(a \<rightleftharpoons> b) \<bullet> x"}.
- \begin{myproperty}\label{swapfreshfresh}
- @{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
- \end{myproperty}
+ %\begin{myproperty}\label{swapfreshfresh}
+ %@{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
+ %\end{myproperty}
%While often the support of an object can be relatively easily
%described, for example for atoms, products, lists, function applications,
@@ -629,8 +648,9 @@
In order to keep our work with deriving the reasoning infrastructure
manageable, we will wherever possible state definitions and perform proofs
- on the ``user-level'' of Isabelle/HOL, as opposed to write custom ML-code that
- generates them anew for each specification. To that end, we will consider
+ on the ``user-level'' of Isabelle/HOL, as opposed to write custom ML-code. % that
+ %generates them anew for each specification.
+ To that end, we will consider
first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}. These pairs
are intended to represent the abstraction, or binding, of the set of atoms @{text
"as"} in the body @{text "x"}.
@@ -657,7 +677,7 @@
\mbox{\it (iv)} & @{term "(p \<bullet> as) = bs"} \\
\end{array}
\end{equation}
-
+ %
\noindent
Note that this relation depends on the permutation @{text
"p"}; $\alpha$-equivalence between two pairs is then the relation where we
@@ -682,7 +702,7 @@
\mbox{\it (iv)} & @{term "(p \<bullet> as) = bs"}\\
\end{array}
\end{equation}
-
+ %
\noindent
where @{term set} is the function that coerces a list of atoms into a set of atoms.
Now the last clause ensures that the order of the binders matters (since @{text as}
@@ -701,12 +721,12 @@
\end{array}
\end{equation}
- It might be useful to consider first some examples about how these definitions
+ It might be useful to consider first some examples how these definitions
of $\alpha$-equivalence pan out in practice. For this consider the case of
abstracting a set of atoms over types (as in type-schemes). We set
@{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we
define
-
+ %
\begin{center}
@{text "fa(x) = {x}"} \hspace{5mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) = fa(T\<^isub>1) \<union> fa(T\<^isub>2)"}
\end{center}
@@ -1049,7 +1069,7 @@
\hspace{5mm}$\mid$~@{text "bn(PTup p\<^isub>1 p\<^isub>2) = bn(p\<^isub>1) @ bn(p\<^isub>2)"}\smallskip\\
\end{tabular}}
\end{equation}
-
+ %
\noindent
In this specification the function @{text "bn"} determines which atoms of
the pattern @{text p} are bound in the argument @{text "t"}. Note that in the
@@ -1059,14 +1079,14 @@
As said above, for deep binders we allow binding clauses such as
%
- \begin{center}
- \begin{tabular}{ll}
- @{text "Bar p::pat t::trm"} &
- \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p t"}\\
- \end{tabular}
- \end{center}
-
- \noindent
+ %\begin{center}
+ %\begin{tabular}{ll}
+ @{text "Bar p::pat t::trm"} %%%&
+ \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p t"} %%\\
+ %\end{tabular}
+ %\end{center}
+ %
+ %\noindent
where the argument of the deep binder also occurs in the body. We call such
binders \emph{recursive}. To see the purpose of such recursive binders,
compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s in the following
@@ -1088,7 +1108,7 @@
\hspace{5mm}$\mid$~@{text "bn(ACons a t as) = [atom a] @ bn(as)"}\\
\end{tabular}}
\end{equation}
-
+ %
\noindent
The difference is that with @{text Let} we only want to bind the atoms @{text
"bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms
@@ -1098,7 +1118,7 @@
To make sure that atoms bound by deep binders cannot be free at the
same time, we cannot have more than one binding function for a deep binder.
Consequently we exclude specifications such as
-
+ %
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
@{text "Baz\<^isub>1 p::pat t::trm"} &
@@ -1244,20 +1264,20 @@
@{text "D"} stands for the set of free atoms of the bodies, @{text B} for the
set of binding atoms in the binders and @{text "B'"} for the set of free atoms in
non-recursive deep binders,
- then the free atoms of the binding clause @{text bc\<^isub>i} are
+ then the free atoms of the binding clause @{text bc\<^isub>i} are\\[-2mm]
%
\begin{equation}\label{fadef}
\mbox{@{text "fa(bc\<^isub>i) \<equiv> (D - B) \<union> B'"}}.
\end{equation}
-
+ %
\noindent
The set @{text D} is formally defined as
%
- \begin{center}
+ %\begin{center}
@{text "D \<equiv> fa_ty\<^isub>1 d\<^isub>1 \<union> ... \<union> fa_ty\<^isub>q d\<^isub>q"}
- \end{center}
-
- \noindent
+ %\end{center}
+ %
+ %\noindent
where in case @{text "d\<^isub>i"} refers to one of the raw types @{text "ty"}$_{1..n}$ from the
specification, the function @{text "fa_ty\<^isub>i"} is the corresponding free-atom function
we are defining by recursion;
@@ -1265,7 +1285,7 @@
otherwise we set @{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
In order to formally define the set @{text B} we use the following auxiliary @{text "bn"}-functions
- for atom types to which shallow binders may refer
+ for atom types to which shallow binders may refer\\[-4mm]
%
%\begin{center}
%\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
@@ -1276,21 +1296,21 @@
%\end{center}
%
\begin{center}
- @{text "bn_atom a \<equiv> {atom a}"}\hspace{17mm}
- @{text "bn_atom_set as \<equiv> atoms as"}\\
- @{text "bn_atom_list as \<equiv> atoms (set as)"}
+ @{text "bn\<^bsub>atom\<^esub> a \<equiv> {atom a}"}\hfill
+ @{text "bn\<^bsub>atom_set\<^esub> as \<equiv> atoms as"}\hfill
+ @{text "bn\<^bsub>atom_list\<^esub> as \<equiv> atoms (set as)"}
\end{center}
-
+ %
\noindent
Like the function @{text atom}, the function @{text "atoms"} coerces
a set of atoms to a set of the generic atom type.
%It is defined as @{text "atoms as \<equiv> {atom a | a \<in> as}"}.
- The set @{text B} is then formally defined as
+ The set @{text B} is then formally defined as\\[-4mm]
%
\begin{center}
@{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> ... \<union> bn_ty\<^isub>p b\<^isub>p"}
\end{center}
-
+ %
\noindent
where we use the auxiliary binding functions for shallow binders.
The set @{text "B'"} collects all free atoms in non-recursive deep
@@ -1303,12 +1323,12 @@
%\noindent
with @{text "l"}$_{1..r}$ $\subseteq$ @{text "b"}$_{1..p}$ and none of the
@{text "l"}$_{1..r}$ being among the bodies @{text
- "d"}$_{1..q}$. The set @{text "B'"} is defined as
+ "d"}$_{1..q}$. The set @{text "B'"} is defined as\\[-5mm]
%
\begin{center}
- @{text "B' \<equiv> fa_bn\<^isub>1 l\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r l\<^isub>r"}
- \end{center}
-
+ @{text "B' \<equiv> fa_bn\<^isub>1 l\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r l\<^isub>r"}\\[-9mm]
+ \end{center}
+ %
\noindent
This completes the definition of the free-atom functions @{text "fa_ty"}$_{1..n}$.
@@ -1365,7 +1385,7 @@
Recall that @{text ANil} and @{text "ACons"} have no
binding clause in the specification. The corresponding free-atom
function @{text "fa\<^bsub>assn\<^esub>"} therefore returns all free atoms
- occurring in an assignment (in case of @{text "ACons"}, they are given in
+ of an assignment (in case of @{text "ACons"}, they are given in
terms of @{text supp}, @{text "fa\<^bsub>trm\<^esub>"} and @{text "fa\<^bsub>assn\<^esub>"}).
The binding only takes place in @{text Let} and
@{text "Let_rec"}. In case of @{text "Let"}, the binding clause specifies
@@ -1988,20 +2008,26 @@
clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, we define
%
\begin{center}
- @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"}
+ @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"} \;\; with
+ $\begin{cases}
+ \text{@{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}}\\
+ \text{@{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}}\\
+ \text{@{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise}
+ \end{cases}$
\end{center}
%
+ %\noindent
+ %with @{text "y\<^isub>i"} determined as follows:
+ %
+ %\begin{center}
+ %\begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}}
+ %$\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\
+ %$\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\
+ %$\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise
+ %\end{tabular}
+ %\end{center}
+ %
\noindent
- with @{text "y\<^isub>i"} determined as follows:
- %
- \begin{center}
- \begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}}
- $\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\
- $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\
- $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise
- \end{tabular}
- \end{center}
- %
Now Properties \ref{supppermeq} and \ref{avoiding} give us a permutation @{text q} such that
@{text "(set (bn (q \<bullet>\<^bsub>bn\<^esub> p)) \<FRESH>\<^sup>* c"} holds and such that @{text "[q \<bullet>\<^bsub>bn\<^esub> p]\<^bsub>list\<^esub>.(q \<bullet> t)"}
is equal to @{text "[p]\<^bsub>list\<^esub>. t"}. We can also show that @{text "(q \<bullet>\<^bsub>bn\<^esub> p) \<approx>\<^bsub>bn\<^esub> p"}. But
@@ -2186,17 +2212,19 @@
%unwanted terms. Our guess is that such predicates result in rather
%intricate formal reasoning.
- Another representation technique for binding is higher-order abstract syntax
- (HOAS), which for example is implemented in the Twelf system. This representation
+ Another technique for representing binding is higher-order abstract syntax
+ (HOAS). %, which for example is implemented in the Twelf system.
+ This %%representation
technique supports very elegantly many aspects of \emph{single} binding, and
impressive work has been done that uses HOAS for mechanising the metatheory
of SML~\cite{LeeCraryHarper07}. We are, however, not aware how multiple
binders of SML are represented in this work. Judging from the submitted
Twelf-solution for the POPLmark challenge, HOAS cannot easily deal with
- binding constructs where the number of bound variables is not fixed. For
- example in the second part of this challenge, @{text "Let"}s involve
+ binding constructs where the number of bound variables is not fixed. %For
+ example
+ In the second part of this challenge, @{text "Let"}s involve
patterns that bind multiple variables at once. In such situations, HOAS
- representations have to resort to the iterated-single-binders-approach with
+ seems to have to resort to the iterated-single-binders-approach with
all the unwanted consequences when reasoning about the resulting terms.
%Two formalisations involving general binders have been
@@ -2224,7 +2252,7 @@
notion of $\alpha$-equivalence. A definition for the notion of free variables
is work in progress in Ott.
- Although we were heavily inspired by the syntax in Ott,
+ Although we were heavily inspired by the syntax of Ott,
its definition of $\alpha$-equivalence is unsuitable for our extension of
Nominal Isabelle. First, it is far too complicated to be a basis for
automated proofs implemented on the ML-level of Isabelle/HOL. Second, it
@@ -2294,7 +2322,7 @@
has a more operational flavour and calculates a partial (renaming) map.
In this way, the definition can deal with vacuous binders. However, to our
best knowledge, no concrete mathematical result concerning this
- definition of $\alpha$-equivalence has been proved.
+ definition of $\alpha$-equivalence has been proved.\\[-7mm]
*}
section {* Conclusion *}
@@ -2321,7 +2349,7 @@
Isabelle \cite{UrbanBerghofer06} this turned out to be a thorny issue. We
hope to do better this time by using the function package that has recently
been implemented in Isabelle/HOL and also by restricting function
- definitions to equivariant functions (for such functions it is possible to
+ definitions to equivariant functions (for such functions we can
provide more automation).
%There are some restrictions we imposed in this paper that we would like to lift in
@@ -2349,8 +2377,8 @@
%where instead of lists, we abstract lists of distinct elements.
%Once we feel confident about such binding modes, our implementation
%can be easily extended to accommodate them.
-
- \medskip
+ %
+ \smallskip
\noindent
{\bf Acknowledgements:} %We are very grateful to Andrew Pitts for
%many discussions about Nominal Isabelle.
@@ -2358,7 +2386,7 @@
making the informal notes \cite{SewellBestiary} available to us and
also for patiently explaining some of the finer points of the work on the Ott-tool.
%Stephanie Weirich suggested to separate the subgrammars
- %of kinds and types in our Core-Haskell example.
+ %of kinds and types in our Core-Haskell example. \\[-6mm]
*}