--- a/Paper/Paper.thy Fri Jul 16 03:22:24 2010 +0100
+++ b/Paper/Paper.thy Fri Jul 16 04:58:46 2010 +0100
@@ -1689,7 +1689,7 @@
any bound atoms. In Ott, in contrast, the user may
define @{text "bn"}$_{1..m}$ so that they return bound
atoms and in this case the third implication is \emph{not} true. A
- result is that the lifing of the corresponding binding functions to $\alpha$-equated
+ result is that the lifing of the corresponding binding functions in Ott to $\alpha$-equated
terms is impossible.
Having established respectfulness for the raw term-constructors, the
@@ -1728,7 +1728,7 @@
to our infrastructure. In a similar fashion we can lift the defining equations
of the free-atom functions @{text "fn_ty\<AL>"}$_{1..n}$ and
@{text "fa_bn\<AL>"}$_{1..m}$ as well as of the binding functions @{text
- "bn\<AL>"}$_{1..m}$ and of the size functions @{text "size_ty\<AL>"}$_{1..n}$.
+ "bn\<AL>"}$_{1..m}$ and the size functions @{text "size_ty\<AL>"}$_{1..n}$.
The latter are defined automatically for the raw types @{text "ty"}$_{1..n}$
by the datatype package of Isabelle/HOL.
@@ -1772,17 +1772,17 @@
show for every term-constructor @{text "C\<^sup>\<alpha>"} that
\begin{center}
- @{text "(supp x\<^isub>1 \<union> \<dots> supp x\<^isub>r) supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}
+ @{text "(supp x\<^isub>1 \<union> \<dots> \<union> supp x\<^isub>r) supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}
\end{center}
\noindent
- holds. This together with Property~\ref{supportsprop} allows us to show
- for every @{text x} of type @{text "ty\<AL>"}$_{1..n}$ is finitely supported,
+ holds. This together with Property~\ref{supportsprop} allows us to prove
+ that every @{text x} of type @{text "ty\<AL>"}$_{1..n}$ is finitely supported,
namely @{text "finite (supp x)"}. This can be again shown by induction
over @{text "ty\<AL>"}$_{1..n}$. Lastly, we can show that the support of
elements in @{text "ty\<AL>"}$_{1..n}$ is the same as @{text "fa_ty\<AL>"}$_{1..n}$.
- This important fact provides evidence that our notions of free-atoms and
- $\alpha$-equivalence are correct.
+ This fact is important in a nominal setting, but also provides evidence
+ that our notions of free-atoms and $\alpha$-equivalence are correct.
\begin{lemma}
For every @{text "x"} of type @{text "ty\<AL>"}$_{1..n}$, we have
@@ -1797,12 +1797,12 @@
\end{proof}
\noindent
- To sum up, we can established automatically a reasoning infrastructure
+ To sum up this section, we can established automatically a reasoning infrastructure
for the types @{text "ty\<AL>"}$_{1..n}$
by first lifting definitions from the raw level to the quotient level and
then by establishing facts about these lifted definitions. All necessary proofs
are generated automatically by custom ML-code. This code can deal with
- specifications like the one shown in Figure~\ref{nominalcorehas} for Core-Haskell.
+ specifications such as the one shown in Figure~\ref{nominalcorehas} for Core-Haskell.
\begin{figure}[t!]
\begin{boxedminipage}{\linewidth}
@@ -1880,9 +1880,10 @@
text {*
In the previous section we were able to provide induction principles that
allow us to perform structural inductions over $\alpha$-equated terms.
- We call such induction principles \emph{weak}, because in case of a term-constructor @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r"},
+ We call such induction principles \emph{weak}, because in case of the
+ term-constructor @{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 not easy to establish.
+ 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>"}
(for example we cannot assume the variable convention for them).
@@ -1898,8 +1899,21 @@
Given a binding function @{text "bn"} we define an auxiliary permutation
operation @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} which permutes only bound arguments in a deep binder.
- Assuming a clause of @{text bn} is defined as @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then
- we define @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>n) \<equiv> C y\<^isub>1 \<dots> y\<^isub>n"} with @{text "y\<^isub>i"} determined as follows:
+ Assuming a clause of @{text bn} is given as
+ %
+ \begin{center}
+ @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"},
+ \end{center}
+
+ \noindent
+ then 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"}
+ \end{center}
+
+ \noindent
+ with @{text "y\<^isub>i"} determined as follows:
%
\begin{center}
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
@@ -1915,8 +1929,8 @@
\begin{lemma}\label{permutebn}
Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p}
- {\it i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<^bsub>bn\<^esub>\<^sup>\<alpha> x)"} and {\it ii)}
- @{text "fa_bn\<^isup>\<alpha> x = fa_bn\<^isup>\<alpha> (p \<bullet>\<^bsub>bn\<^esub>\<^sup>\<alpha> x)"}.
+ {\it (i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"} and {\it (ii)}
+ @{text "fa_bn\<^isup>\<alpha> x = fa_bn\<^isup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"}.
\end{lemma}
\begin{proof}
@@ -1933,18 +1947,21 @@
for the support of an object @{text x}, then we can use this permutation
to rename the binders in @{text x}, without ``changing'' @{text x}. In case of the
@{text "Let"} term-constructor from the example shown
- \eqref{letpat} this means for a permutation @{text "r"}:
+ in \eqref{letpat} this means for a permutation @{text "r"}
%
\begin{equation}\label{renaming}
\begin{array}{l}
\mbox{if @{term "supp (Abs_lst (bn p) t\<^isub>2) \<sharp>* r"}}\\
- \qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \<bullet>\<^bsub>bnpat\<^esub> p) t\<^isub>1 (r \<bullet> t\<^isub>2)"}}
+ \qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \<bullet>\<AL>\<^bsub>bn_pat\<^esub> p) t\<^isub>1 (r \<bullet> t\<^isub>2)"}}
\end{array}
\end{equation}
\noindent
- This fact will be crucial when establishing the strong induction principles.
- In our running example about @{text "Let"}, they state that instead
+ This fact will be crucial when establishing the strong induction principles below.
+
+
+ In our running example about @{text "Let"}, the strong induction
+ principle means that instead
of establishing the implication
%
\begin{center}
@@ -1966,7 +1983,7 @@
\noindent
While this implication contains an additional argument, namely @{text c}, and
also additional universal quantifications, it is usually easier to establish.
- The reason is that we can make the freshness
+ The reason is that we have the freshness
assumption @{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c"}, whereby @{text c} can be arbitrarily
chosen by the user as long as it has finite support.
@@ -1976,7 +1993,7 @@
%
\begin{equation}\label{hyps}
@{text "\<forall>q c. P\<^bsub>trm\<^esub> c (q \<bullet> t)"} \hspace{4mm}
- @{text "\<forall>q\<^isub>1 q\<^isub>2 c. P\<^bsub>pat\<^esub> (q\<^isub>1 \<bullet>\<^bsub>bn\<^esub> (q\<^isub>2 \<bullet> p))"}
+ @{text "\<forall>q\<^isub>1 q\<^isub>2 c. P\<^bsub>pat\<^esub> (q\<^isub>1 \<bullet>\<AL>\<^bsub>bn\<^esub> (q\<^isub>2 \<bullet> p))"}
\end{equation}
\noindent
@@ -1996,38 +2013,35 @@
\begin{center}
\begin{tabular}{l}
@{text "Let (q \<bullet> p) (q \<bullet> t\<^isub>1) (q \<bullet> t\<^isub>2) ="} \\
- \hspace{15mm}@{text "Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2))"}
+ \hspace{15mm}@{text "Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2))"}
\end{tabular}
\end{center}
\noindent
So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we can equally
- establish @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}.
+ establish @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}.
To do so, we will use the implication \eqref{strong} of the strong induction
principle, which requires us to discharge
the following four proof obligations:
%
\begin{center}
\begin{tabular}{rl}
- {\it i)} & @{text "set (bn (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p))) #\<^sup>* c"}\\
- {\it ii)} & @{text "\<forall>d. P\<^bsub>pat\<^esub> d (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p))"}\\
- {\it iii)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (q \<bullet> t\<^isub>1)"}\\
- {\it iv)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (r \<bullet> (q \<bullet> t\<^isub>2))"}\\
+ {\it (i)} & @{text "set (bn (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))) #\<^sup>* c"}\\
+ {\it (ii)} & @{text "\<forall>d. P\<^bsub>pat\<^esub> d (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))"}\\
+ {\it (iii)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (q \<bullet> t\<^isub>1)"}\\
+ {\it (iv)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (r \<bullet> (q \<bullet> t\<^isub>2))"}\\
\end{tabular}
\end{center}
\noindent
- The first follows from \eqref{rprops} and Lemma~\ref{permutebn}.{\it i)}; the
+ The first follows from \eqref{rprops} and Lemma~\ref{permutebn}.{\it (i)}; the
others from the induction hypotheses in \eqref{hyps} (in the fourth case
we have to use the fact that @{term "(r \<bullet> (q \<bullet> t\<^isub>2)) = (r + q) \<bullet> t\<^isub>2"}).
Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps},
we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}.
- This completes the proof showing that the strong induction principle derives from
- the weak induction principle. For the moment we can derive the difficult cases of
- the strong induction principles only by hand, but they are very schematic
- so that with little effort we can even derive them for
- Core-Haskell given in Figure~\ref{nominalcorehas}.
+ This completes the proof showing that the weak induction principles imply
+ the strong induction principles.
*}
@@ -2073,7 +2087,7 @@
use the approach based on iterated single binders. Our experience with
the latter formalisation has been disappointing. The major pain arose from
the need to ``unbind'' variables. This can be done in one step with our
- general binders, but needs a cumbersome
+ general binders described in this paper, but needs a cumbersome
iteration with single binders. The resulting formal reasoning turned out to
be rather unpleasant. The hope is that the extension presented in this paper
is a substantial improvement.
@@ -2097,11 +2111,11 @@
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 HOL-based theorem prover. We also had to generalise slightly their
+ meaning in a HOL-based theorem prover. We also had to generalise slightly Ott's
binding clauses. In Ott you specify binding clauses with a single body; we
allow more than one. We have to do this, because this makes a difference
for our notion of $\alpha$-equivalence in case of \isacommand{bind\_set} and
- \isacommand{bind\_res}. For example
+ \isacommand{bind\_res}. Consider the examples
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
@@ -2114,7 +2128,7 @@
\end{center}
\noindent
- in the first term-constructor we have a single
+ In the first term-constructor we have a single
body that happens to be ``spread'' over two arguments; in the second term-constructor we have
two independent bodies in which the same variables are bound. As a result we
have
@@ -2153,11 +2167,11 @@
In a slightly different domain (programming with dependent types), the
paper \cite{Altenkirch10} presents a calculus with a notion of
$\alpha$-equivalence related to our binding mode \isacommand{bind\_res}.
- The corresponding definition is similar to the one by Pottier, except that it
+ The definition in \cite{Altenkirch10} is similar to the one by Pottier, except that it
has a more operational flavour and calculates a partial (renaming) map.
- In this way Altenkirch et al can deal with vacuous binders. However, to our
- best knowledge, no concrete mathematical result concerning their notion
- of equality has been proved.
+ 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.
*}
section {* Conclusion *}
@@ -2167,8 +2181,11 @@
general binders, that is term-constructors having multiple bound
variables. For this extension we introduced novel definitions of
$\alpha$-equivalence and automated all necessary proofs in Isabelle/HOL.
- We have tried out the extension with terms from Core-Haskell and our code
- will become part of the Isabelle distribution.\footnote{For the moment
+ To specify general binders we used the syntax from Ott, but modified
+ it so that it makes sense in our context of $\alpha$-equated terms.
+ We have tried out the extension with terms from Core-Haskell, type-schemes
+ and the lambda-calculus, and our 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}.}
@@ -2181,7 +2198,7 @@
definitions to equivariant functions (for such functions it is possible to
provide more automation).
- There are some restrictions we imposed in this paper, that we would like to lift in
+ There are some restrictions we imposed in this paper that we would like to lift in
future work. One is the exclusion of nested datatype definitions. Nested
datatype definitions allow one to specify, for instance, the function kinds
in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded
@@ -2189,7 +2206,7 @@
achieve this, we need a slightly more clever implementation than we have at the moment.
A more interesting line of investigation is whether we can go beyond the
- simple-minded form for binding functions that we adopted from Ott. At the moment, binding
+ simple-minded form of binding functions that we adopted from Ott. At the moment, binding
functions can only return the empty set, a singleton atom set or unions
of atom sets (similarly for lists). It remains to be seen whether
properties like