--- a/Paper/Paper.thy Sun Nov 21 02:17:19 2010 +0000
+++ b/Paper/Paper.thy Wed Nov 24 01:08:48 2010 +0000
@@ -274,7 +274,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
+ Isabelle/HOL is a rather non-trivial task. For every
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
@@ -441,10 +441,9 @@
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.
+ 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. However, in the interest of brevity, we shall restrict ourselves
+ sort. In the interest of brevity, we shall restrict ourselves
in what follows to only one sort of atoms.
Permutations are bijective functions from atoms to atoms that are
@@ -457,7 +456,7 @@
the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}},
and the inverse permutation of @{term p} as @{text "- p"}. The permutation
operation is defined over the type-hierarchy \cite{HuffmanUrban10};
- for example permutations acting on products, lists, sets, functions and booleans is
+ for example permutations acting on products, lists, sets, functions and booleans are
given by:
%
%\begin{equation}\label{permute}
@@ -1429,7 +1428,7 @@
%\noindent
for the binding functions @{text "bn"}$_{1..m}$,
To simplify our definitions we will use the following abbreviations for
- \emph{compound equivalence relations} and \emph{compound free-atom functions} acting on tuples
+ \emph{compound equivalence relations} and \emph{compound free-atom functions} acting on tuples.
%
\begin{center}
\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
@@ -1619,7 +1618,7 @@
Note the difference between $\approx_{\textit{assn}}$ and
$\approx_{\textit{bn}}$: the latter only ``tracks'' $\alpha$-equivalence of
the components in an assignment that are \emph{not} bound. This is needed in the
- in the clause for @{text "Let"} (which is has
+ clause for @{text "Let"} (which has
a non-recursive binder).
%The underlying reason is that the terms inside an assignment are not meant
%to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"},
@@ -1834,7 +1833,7 @@
\end{proof}
\noindent
- To sum up this section, we can established automatically a reasoning infrastructure
+ To sum up this section, we can establish 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
@@ -1949,7 +1948,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
- methods from the function package of Isabelle/HOL generates.
+ 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
two proof obligations: one is that we have
@@ -2032,8 +2031,8 @@
\noindent
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"}. T
- hese facts establish that @{text "Let (q \<bullet>\<^bsub>bn\<^esub> p) (p \<bullet> t) = Let p t"}, as we need. This
+ 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"}.
+ These facts establish that @{text "Let (q \<bullet>\<^bsub>bn\<^esub> p) (p \<bullet> t) = Let p t"}, as we need. This
completes the non-trivial cases in \eqref{letpat} for strengthening the corresponding induction
principle.
@@ -2203,7 +2202,7 @@
de-Bruijn representation), but to different bound variables. A similar idea
has been recently explored for general binders in the locally nameless
approach to binding \cite{chargueraud09}. There, de-Bruijn indices consist
- of two numbers, one referring to the place where a variable is bound and the
+ of two numbers, one referring to the place where a variable is bound, and the
other to which variable is bound. The reasoning infrastructure for both
representations of bindings comes for free in theorem provers like Isabelle/HOL or
Coq, since the corresponding term-calculi can be implemented as ``normal''
@@ -2250,8 +2249,9 @@
$\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
- notion of $\alpha$-equivalence. A definition for the notion of free variables
- is in Ott work in progress.
+ 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