--- a/Paper/Paper.thy Wed Dec 08 17:07:08 2010 +0000
+++ b/Paper/Paper.thy Thu Dec 09 17:10:08 2010 +0000
@@ -99,18 +99,13 @@
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
want to make a distinction about the order of the bound variables. Therefore
- we would like to regard the following two type-schemes as $\alpha$-equivalent
+ we would like to regard the first pair of type-schemes as $\alpha$-equivalent,
+ but assuming that @{text x}, @{text y} and @{text z} are distinct variables,
+ 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}. x \<rightarrow> y"}
- \end{equation}
- %
- \noindent
- but assuming that @{text x}, @{text y} and @{text z} are distinct variables,
- the following two should \emph{not} be $\alpha$-equivalent
- %
- \begin{equation}\label{ex2}
- @{text "\<forall>{x, y}. x \<rightarrow> y \<notapprox>\<^isub>\<alpha> \<forall>{z}. z \<rightarrow> z"}
+ @{text "\<forall>{x, y}. x \<rightarrow> y \<approx>\<^isub>\<alpha> \<forall>{y, x}. x \<rightarrow> y"}\hspace{10mm}
+ @{text "\<forall>{x, y}. x \<rightarrow> y \<notapprox>\<^isub>\<alpha> \<forall>{z}. z \<rightarrow> z"}
\end{equation}
%
\noindent
@@ -139,7 +134,7 @@
\noindent
we might not care in which order the assignments @{text "x = 3"} and
- \mbox{@{text "y = 2"}} are given, but it would be unusual to regard
+ \mbox{@{text "y = 2"}} are given, but it would be often unusual to regard
\eqref{one} as $\alpha$-equivalent with
%
\begin{center}
@@ -382,7 +377,7 @@
The main improvement over Ott is that we introduce three binding modes
(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 from ``first principles''.
+ for our specifications from ``first principles''.
%\begin{figure}
@@ -440,8 +435,8 @@
sort-respecting permutations of atoms. We will use the letters @{text "a,
b, c, \<dots>"} to stand for atoms and @{text "p, q, \<dots>"} to stand for
permutations. The purpose of atoms is to represent variables, be they bound or free.
- The sorts of atoms can be used to represent different kinds of
- variables, such as the term-, coercion- and type-variables in Core-Haskell.
+ %The sorts of atoms can be used to represent different kinds of
+ %variables, such as the term-, coercion- and type-variables in Core-Haskell.
It is assumed that there is an infinite supply of atoms for each
sort. In the interest of brevity, we shall restrict ourselves
in what follows to only one sort of atoms.
@@ -731,7 +726,7 @@
\end{center}
\noindent
- Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and
+ 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
$\approx_{\,\textit{set}}$ and $\approx_{\,\textit{res}}$ by taking @{text p} to
@@ -800,9 +795,10 @@
\begin{center}
\begin{tabular}{l}
- @{thm (lhs) supp_Abs(1)[no_vars]} $=$
- @{thm supp_Abs(2)[no_vars]}, and\\
- @{thm supp_Abs(3)[where bs="as", no_vars]}
+ @{thm (lhs) supp_Abs(1)[no_vars]} $\;\;=\;\;$
+ @{thm (lhs) supp_Abs(2)[no_vars]} $\;\;=\;\;$ @{thm (rhs) supp_Abs(2)[no_vars]}, and\\
+ @{thm (lhs) supp_Abs(3)[where bs="as", no_vars]} $\;\;=\;\;$
+ @{thm (rhs) supp_Abs(3)[where bs="as", no_vars]}
\end{tabular}
\end{center}
\end{theorem}
@@ -810,7 +806,7 @@
\noindent
This theorem states that the bound names do not appear in the support.
For brevity we omit the proof and again refer the reader to
- our formalisation in Isabelle/HOL (or the appendix).
+ our formalisation in Isabelle/HOL.
%\noindent
%Below we will show the first equation. The others
@@ -1010,20 +1006,19 @@
bound:
\begin{center}\small
- \begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
+ \begin{tabular}{@ {}c@ {\hspace{7mm}}c@ {}}
\begin{tabular}{@ {}l}
\isacommand{nominal\_datatype} @{text lam} $=$\\
- \hspace{5mm}\phantom{$\mid$}~@{text "Var name"}\\
- \hspace{5mm}$\mid$~@{text "App lam lam"}\\
- \hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}\\
- \hspace{24mm}\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
+ \hspace{2mm}\phantom{$\mid$}~@{text "Var name"}\\
+ \hspace{2mm}$\mid$~@{text "App lam lam"}\\
+ \hspace{2mm}$\mid$~@{text "Lam x::name t::lam"}~~\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
\end{tabular} &
\begin{tabular}{@ {}l@ {}}
\isacommand{nominal\_datatype}~@{text ty} $=$\\
\hspace{5mm}\phantom{$\mid$}~@{text "TVar name"}\\
\hspace{5mm}$\mid$~@{text "TFun ty ty"}\\
- \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}\\
- \hspace{29mm}\isacommand{bind (res)} @{text xs} \isacommand{in} @{text T}\\
+ \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}~~%
+ \isacommand{bind (res)} @{text xs} \isacommand{in} @{text T}\\
\end{tabular}
\end{tabular}
\end{center}
@@ -1118,7 +1113,7 @@
same time, we cannot have more than one binding function for a deep binder.
Consequently we exclude specifications such as
%
- \begin{center}
+ \begin{center}\small
\begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
@{text "Baz\<^isub>1 p::pat t::trm"} &
\isacommand{bind} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\
@@ -1921,13 +1916,13 @@
term-constructor \mbox{@{text "C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r"}}
the induction hypothesis requires us to establish the implications \eqref{weakprem}.
The problem with these implications is that in general they are difficult to establish.
- The reason is that we cannot make any assumption about the binders that might be in @{text "C\<^sup>\<alpha>"}.
+ The reason is that we cannot make any assumption about the bound atoms that might be in @{text "C\<^sup>\<alpha>"}.
%%(for example we cannot assume the variable convention for them).
In \cite{UrbanTasson05} we introduced a method for automatically
strengthening weak induction principles for terms containing single
binders. These stronger induction principles allow the user to make additional
- assumptions about binders.
+ assumptions about bound atoms.
%These additional assumptions amount to a formal
%version of the informal variable convention for binders.
To sketch how this strengthening extends to the case of multiple binders, we use as
@@ -1947,7 +1942,7 @@
In \cite{UrbanTasson05} we showed how the weaker induction principles imply
the stronger ones. This was done by some quite complicated, nevertheless automated,
- induction proofs. In this paper we simplify this work by leveraging the automated proof
+ induction proof. In this paper we simplify this work by leveraging the automated proof
methods from the function package of Isabelle/HOL.
The reasoning principle these methods employ is well-founded induction.
To use them in our setting, we have to discharge
@@ -1956,8 +1951,8 @@
every induction step and the other is that we have covered all cases.
As measures we use the size functions
@{text "size_ty"}$^\alpha_{1..n}$, which we lifted in the previous section and which are
- all well-founded. It is straightforward to establish that these measures decrease
- in every induction step.
+ all well-founded. %It is straightforward to establish that these measures decrease
+ %in every induction step.
What is left to show is that we covered all cases. To do so, we use
a cases lemma derived for each type. For the terms in \eqref{letpat}
@@ -2009,7 +2004,7 @@
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"} \;\; with
+ @{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"}}\\
@@ -2248,13 +2243,13 @@
this tool have also put forward (on paper) a definition for
$\alpha$-equivalence of terms that can be specified in Ott. This definition is
rather different from ours, not using any nominal techniques. To our
- knowledge there is also no concrete mathematical result concerning this
+ knowledge there is no concrete mathematical result concerning this
notion of $\alpha$-equivalence. Also the definition for the
notion of free variables
is work in progress.
Although we were heavily inspired by the syntax of Ott,
- its definition of $\alpha$-equivalence is unsuitable for our extension of
+ its definition of $\alpha$-equi\-valence 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
covers cases of binders depending on other binders, which just do not make
@@ -2340,18 +2335,19 @@
exist in Ott.
We have tried out the extension with calculi such as Core-Haskell, type-schemes
and approximately a dozen of other typical examples from programming
- language research~\cite{SewellBestiary}. The code
- will eventually become part of the next Isabelle distribution.\footnote{For the moment
- it can be downloaded from the Mercurial repository linked at
- \href{http://isabelle.in.tum.de/nominal/download}
- {http://isabelle.in.tum.de/nominal/download}.}
+ language research~\cite{SewellBestiary}.
+ %The code
+ %will eventually become part of the next Isabelle distribution.\footnote{For the moment
+ %it can be downloaded from the Mercurial repository linked at
+ %\href{http://isabelle.in.tum.de/nominal/download}
+ %{http://isabelle.in.tum.de/nominal/download}.}
We have left out a discussion about how functions can be defined over
$\alpha$-equated terms involving general binders. In earlier versions of Nominal
- Isabelle \cite{UrbanBerghofer06} this turned out to be a thorny issue. We
+ Isabelle 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 we can
+ definitions to equivariant functions (for them we can
provide more automation).
%There are some restrictions we imposed in this paper that we would like to lift in
@@ -2386,7 +2382,7 @@
%many discussions about Nominal Isabelle.
We thank Peter Sewell for
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.
+ also for patiently explaining some of the finer points of the Ott-tool.\\[-7mm]
%Stephanie Weirich suggested to separate the subgrammars
%of kinds and types in our Core-Haskell example. \\[-6mm]
*}