--- a/Paper/Paper.thy Thu Apr 01 14:50:58 2010 +0200
+++ b/Paper/Paper.thy Thu Apr 01 14:53:14 2010 +0200
@@ -499,7 +499,7 @@
While often the support of an object can be relatively easily
described, for example for atoms, products, lists, function applications,
- booleans and permutations\\[-6mm]
+ booleans and permutations as follows\\[-6mm]
%
\begin{eqnarray}
@{term "supp a"} & = & @{term "{a}"}\\
@@ -550,12 +550,12 @@
\noindent
From property \eqref{equivariancedef} and the definition of @{text supp}, we
- can be easily deduce that an equivariant function has empty support.
+ can be easily deduce that equivariant functions have empty support.
Finally, the nominal logic work provides us with convenient means to rename
binders. While in the older version of Nominal Isabelle, we used extensively
Property~\ref{swapfreshfresh} for renaming single binders, this property
- proved unwieldy for dealing with multiple binders. For such pinders the
+ proved unwieldy for dealing with multiple binders. For such binders the
following generalisations turned out to be easier to use.
\begin{property}\label{supppermeq}
@@ -652,7 +652,8 @@
\noindent
where @{term set} is a function that coerces a list of atoms into a set of atoms.
- Now the last clause ensures that the order of the binders matters.
+ Now the last clause ensures that the order of the binders matters (since @{text as}
+ and @{text bs} are lists of atoms).
If we do not want to make any difference between the order of binders \emph{and}
also allow vacuous binders, then we keep sets of binders, but drop the fourth
@@ -764,7 +765,7 @@
\noindent
indicating that a set (or list) @{text as} is abstracted in @{text x}. We will
call the types \emph{abstraction types} and their elements
- \emph{abstractions}. The important property we need to derive the support of
+ \emph{abstractions}. The important property we need to derive is the support of
abstractions, namely:
\begin{thm}[Support of Abstractions]\label{suppabs}
@@ -820,7 +821,7 @@
\noindent
which by Property~\ref{supportsprop} gives us ``one half'' of
- Thm~\ref{suppabs}. The ``other half'' is a bit more involved. To establish
+ Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish
it, we use a trick from \cite{Pitts04} and first define an auxiliary
function @{text aux}, taking an abstraction as argument:
%
@@ -857,7 +858,7 @@
can be conveninetly established at the Isabelle/HOL level. It would be
difficult to write custom ML-code that derives automatically such properties
for every term-constructor that binds some atoms. Also the generality of
- the definitions for alpha-equivalence will help us in the next section.
+ the definitions for alpha-equivalence will help us in definitions in the next section.
*}
section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *}
@@ -1013,7 +1014,7 @@
\noindent
In this specification the function @{text "bn"} determines which atoms of @{text p} are
- bound in the argument @{text "t"}. Note that in the second last clause the function @{text "atom"}
+ bound in the argument @{text "t"}. Note that in the second-last clause the function @{text "atom"}
coerces a name into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}. This allows
us to treat binders of different atom type uniformly.
@@ -1067,7 +1068,7 @@
since there is no overlap of binders.
Note that in the last example we wrote {\it\isacommand{bind}\;bn(p)\;\isacommand{in}\;p}.
- Whenever such a binding clause is present, we will call the binder \emph{recursive}.
+ Whenever such a binding clause is present, we will call the corresponding binder \emph{recursive}.
To see the purpose of such recursive binders, compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s
in the following specification:
%
@@ -1105,7 +1106,7 @@
then use the type constructors @{text "abs_set"}, @{text "abs_res"} and
@{text "abs_list"} from Section \ref{sec:binders}. Therefore we will first
extract datatype definitions from the specification and then define
- independently an alpha-equivalence relation over them.
+ expicitly an alpha-equivalence relation over them.
The datatype definition can be obtained by stripping off the
@@ -1163,12 +1164,12 @@
\noindent
The reason for this setup is that in a deep binder not all atoms have to be
- bound, as we shall see in an example below. We need therefore the function
+ bound, as we shall see in an example below. We need therefore a function
that calculates those unbound atoms.
While the idea behind these
free-variable functions is clear (they just collect all atoms that are not bound),
- because of the rather complicated binding mechanisms their definitions are
+ because of our rather complicated binding mechanisms their definitions are
somewhat involved.
Given a term-constructor @{text "C"} of type @{text ty} with argument types
\mbox{@{text "ty\<^isub>1 \<dots> ty\<^isub>n"}}, the function
@@ -1221,8 +1222,8 @@
\end{equation}
\noindent
- Like the coercion function @{text atom} used earlier, @{text "atoms as"} coerces
- the set @{text as} to the generic atom type.
+ Like the coercion function @{text atom} used earlier, @{text "atoms"} coerces
+ the 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 last case we need to consider is when @{text "x\<^isub>i"} is neither
@@ -1237,9 +1238,8 @@
form of binding functions, this can be done automatically by recursively
building up the the set of free variables from the arguments that are
not bound. Let us assume one clause of a binding function is
- @{text "bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then @{text "fv_bn\<^isub>j"} is the
- union of the values calculated for @{text "x\<^isub>i"} of type @{text "ty\<^isub>i"}
- as follows:
+ @{text "bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then @{text "fv_bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n)"} is the
+ union of the values calculated for @{text "x\<^isub>i"} as follows:
\begin{center}
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
@@ -1257,7 +1257,7 @@
$\bullet$ & @{text "atom x\<^isub>i"} provided @{term "x\<^isub>i"} is an atom\\
$\bullet$ & @{text "atoms x\<^isub>i"} provided @{term "x\<^isub>i"} is a set of atoms\\
$\bullet$ & @{term "atoms (set x\<^isub>i)"} provided @{term "x\<^isub>i"} is a list of atoms\\
- $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i"} provided @{term "ty\<^isub>i"} is one of the raw
+ $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i"} provided @{term "ty\<^isub>i"} is the type of @{text "x\<^isub>i"} and one of the raw
types corresponding to the types specified by the user\\
% $\bullet$ & @{text "fv_ty\<^isup>\<alpha> x\<^isub>i - bnds"} provided @{term "x\<^isub>i"} is not in @{text "rhs"}
% and is an existing nominal datatype with the free-variable function @{text "fv\<^isup>\<alpha>"}\\
@@ -1296,7 +1296,7 @@
free in @{text "as"}. This is what the purpose of the function @{text
"fv\<^bsub>bn\<^esub>"} is. In contrast, in @{text "Let_rec"} we have a
recursive binder where we want to also bind all occurrences of the atoms
- @{text "bn as"} inside @{text "as"}. Therefore we have to subtract @{text
+ in @{text "set (bn as)"} inside @{text "as"}. Therefore we have to subtract @{text
"set (bn as)"} from @{text "fv\<^bsub>assn\<^esub> as"}, as well as from
@{text "fv\<^bsub>trm\<^esub> t"}. An interesting point in this example is
that an assignment ``alone'' does not have any bound variables. Only in the
@@ -1358,11 +1358,11 @@
\mbox{@{text "(u\<^isub>1, v\<^isub>1),\<dots>,(u\<^isub>m, v\<^isub>m)"}} are the corresponding binders. For the binding mode
\isacommand{bind\_set} we generate the premise
\begin{center}
- @{term "\<exists>p. (u\<^isub>1 \<union> \<xi> \<union> u\<^isub>m, x\<^isub>i) \<approx>gen alpha_ty fv_ty\<^isub>i p (v\<^isub>1 \<union> \<xi> \<union> v\<^isub>m, y\<^isub>i)"}
+ @{term "\<exists>p. (u\<^isub>1 \<union> \<xi> \<union> u\<^isub>m, x\<^isub>i) \<approx>gen alpha_ty fv_ty p (v\<^isub>1 \<union> \<xi> \<union> v\<^isub>m, y\<^isub>i)"}
\end{center}
- For the binding mode \isacommand{bind} we use $\approx_{\textit{list}}$, and for
- binding mode \isacommand{bind\_res} we use $\approx_{\textit{res}}$.
+ For the binding mode \isacommand{bind}, we use $\approx_{\textit{list}}$, and for
+ binding mode \isacommand{bind\_res} we use $\approx_{\textit{res}}$ instead.
\item The @{text "(x\<^isub>i, y\<^isub>i)"} are deep non-recursive binders with type @{text "ty"}
and @{text bn} being the auxiliary binding function. We assume
@@ -1396,36 +1396,34 @@
From these definition it is clear why we can only support one binding mode per binder
and body, as we cannot mix the relations $\approx_{\textit{set}}$, $\approx_{\textit{list}}$
and $\approx_{\textit{res}}$. It is also clear why we had to impose the restriction
- of excluding overlapping binders, as these would need to be translated to separate
+ of excluding overlapping binders, as these would need to be translated into separate
abstractions.
The only cases that are not covered by the rules above are the cases where @{text "(x\<^isub>i, y\<^isub>i)"} is
- neither a binder nor a body. Then we just generate @{text "x\<^isub>i \<approx>ty y\<^isub>i"} provided
+ neither a binder nor a body in a binding clause. Then we just generate @{text "x\<^isub>i \<approx>ty y\<^isub>i"} provided
the type of @{text "x\<^isub>i"} and @{text "y\<^isub>i"} is @{text ty} and the arguments are
- recursive arguments of the term-constructor. If they are non-recursive arguments
+ recursive arguments of the term-constructor. If they are non-recursive arguments,
then we generate just @{text "x\<^isub>i = y\<^isub>i"}.
- {\bf TODO (I do not understand the definition below yet).}
+
+ The definition of the alpha-equivalence relations @{text "\<approx>bn"} for binding functions
+ are similar. We again have conclusions of the form \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>bn C y\<^isub>1 \<dots> y\<^isub>n"}}. We
+ need to generate premises for each pair @{text "(x\<^isub>i, y\<^isub>i)"} depending on whether @{text "x\<^isub>i"}
+ occurs in @{text "rhs"} of the clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}:
- The alpha-equivalence relations for binding functions are similar to the alpha-equivalences
- for their respective types, the difference is that they omit checking the arguments that
- are bound. We assumed that there are no bindings in the type on which the binding function
- is defined so, there are no permutations involved. For a binding function clause
- @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, two instances of the constructor are equivalent
- @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx> C y\<^isub>1 \<dots> y\<^isub>n"} if:
\begin{center}
- \begin{tabular}{cp{7cm}}
- $\bullet$ & @{text "x\<^isub>j"} is not of a type being defined and occurs in @{text "rhs"}\\
- $\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} provided @{text "x\<^isub>j"} is not of a type being defined
- and does not occur in @{text "rhs"}\\
- $\bullet$ & @{text "x\<^isub>j \<approx>bn\<^isub>m y\<^isub>j"} provided @{text "x\<^isub>j"} is of a type being defined
- occuring in @{text "rhs"} under the binding function @{text "bn\<^isub>m"}\\
- $\bullet$ & @{text "x\<^isub>j \<approx> y\<^isub>j"} otherwise\\
+ \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
+ $\bullet$ & @{text "x\<^isub>i \<approx>ty y\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text rhs}
+ and the type of @{text "x\<^isub>i"} is @{text "ty"}\\
+ $\bullet$ & @{text "x\<^isub>i \<approx>bn y\<^isub>i"} provided @{text "x\<^isub>i"} occurs in @{text rhs}
+ with the recursive call @{text "bn x\<^isub>i"}\\
+ $\bullet$ & none provided @{text "x\<^isub>i"} occurs in @{text rhs} but it is not
+ in a recursive call involving a @{text "bn"}
\end{tabular}
\end{center}
- Again lets take a look at an example for these definitions. For \eqref{letrecs}
+ Again lets take a look at an example for these definitions. For \eqref{letrecs}
we have three relations, namely $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
$\approx_{\textit{bn}}$, with the clauses as follows:
@@ -1459,7 +1457,7 @@
$\approx_{\textit{bn}}$: the latter only ``tracks'' alpha-equivalence of
the components in an assignment that are \emph{not} bound. Therefore we have
a $\approx_{\textit{bn}}$-premise in the clause for @{text "Let"} (which is
- a non-recursive binder), since the terms inside an assignment are not meant
+ a non-recursive binder). The reason is that the terms inside an assignment are not meant
to be under the binder. Such a premise is not needed in @{text "Let_rec"},
because there everything from the assignment is under the binder.
*}
@@ -1467,8 +1465,8 @@
section {* Establishing the Reasoning Infrastructure *}
text {*
- Having made all these definition for raw terms, we can start to introduce
- the resoning infrastructure for the specified types. For this we first
+ Having made all crucial definitions for raw terms, we can start introducing
+ the resoning infrastructure for the types the user specified. For this we first
have to show that the alpha-equivalence relation defined in the previous
sections are indeed equivalence relations.
@@ -1479,10 +1477,10 @@
\end{lemma}
\begin{proof}
- The proof is by induction over the definitions. The non-trivial
- cases involves premises build up by $\approx_{\textit{set}}$,
+ The proof is by mutual induction over the definitions. The non-trivial
+ cases involve premises build up by $\approx_{\textit{set}}$,
$\approx_{\textit{res}}$ and $\approx_{\textit{list}}$. They
- can be dealt with like in Lemma~\ref{alphaeq}.
+ can be dealt with as in Lemma~\ref{alphaeq}.
\end{proof}
\noindent