--- a/Paper/Paper.thy Mon Apr 26 20:19:42 2010 +0200
+++ b/Paper/Paper.thy Tue Apr 27 12:23:06 2010 +0200
@@ -706,34 +706,6 @@
It can also relatively easily be shown that all tree notions of alpha-equivalence
coincide, if we only abstract a single atom.
- % looks too ugly
- %\noindent
- %Let $\star$ range over $\{set, res, list\}$. We prove next under which
- %conditions the $\approx\hspace{0.05mm}_\star^{\fv, R, p}$ are equivalence
- %relations and equivariant:
- %
- %\begin{lemma}
- %{\it i)} Given the fact that $x\;R\;x$ holds, then
- %$(as, x) \approx\hspace{0.05mm}^{\fv, R, 0}_\star (as, x)$. {\it ii)} Given
- %that @{text "(p \<bullet> x) R y"} implies @{text "(-p \<bullet> y) R x"}, then
- %$(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$ implies
- %$(bs, y) \approx\hspace{0.05mm}^{\fv, R, - p}_\star (as, x)$. {\it iii)} Given
- %that @{text "(p \<bullet> x) R y"} and @{text "(q \<bullet> y) R z"} implies
- %@{text "((q + p) \<bullet> x) R z"}, then $(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$
- %and $(bs, y) \approx\hspace{0.05mm}^{\fv, R, q}_\star (cs, z)$ implies
- %$(as, x) \approx\hspace{0.05mm}^{\fv, R, q + p}_\star (cs, z)$. Given
- %@{text "(q \<bullet> x) R y"} implies @{text "(p \<bullet> (q \<bullet> x)) R (p \<bullet> y)"} and
- %@{text "p \<bullet> (fv x) = fv (p \<bullet> x)"} then @{text "p \<bullet> (fv y) = fv (p \<bullet> y)"}, then
- %$(as, x) \approx\hspace{0.05mm}^{\fv, R, q}_\star (bs, y)$ implies
- %$(p \;\isasymbullet\; as, p \;\isasymbullet\; x) \approx\hspace{0.05mm}^{\fv, R, q}_\star
- %(p \;\isasymbullet\; bs, p \;\isasymbullet\; y)$.
- %\end{lemma}
-
- %\begin{proof}
- %All properties are by unfolding the definitions and simple calculations.
- %\end{proof}
-
-
In the rest of this section we are going to introduce three abstraction
types. For this we define
%
@@ -742,8 +714,8 @@
\end{equation}
\noindent
- (similarly for $\approx_{\textit{abs\_list}}$
- and $\approx_{\textit{abs\_res}}$). We can show that these relations are equivalence
+ (similarly for $\approx_{\textit{abs\_res}}$
+ and $\approx_{\textit{abs\_list}}$). We can show that these relations are equivalence
relations and equivariant.
\begin{lemma}\label{alphaeq}
@@ -866,11 +838,12 @@
Theorem~\ref{suppabs}.
The method of first considering abstractions of the
- form @{term "Abs as x"} etc is motivated by the fact that properties about them
- can be conveninetly established at the Isabelle/HOL level. It would be
- difficult to write custom ML-code that derives automatically such properties
+ form @{term "Abs as x"} etc is motivated by the fact that
+ we can conveniently establish at the Isabelle/HOL level
+ properties about them. It would be
+ laborious 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 definitions in the next section.
+ the definitions for alpha-equivalence will help us in the next section.
*}
section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *}
@@ -945,9 +918,22 @@
cardinality does) and the last is for sets of binders (with vacuous binders
preserving alpha-equivalence). The ``\isacommand{in}-part'' of a binding
clause will be called \emph{bodies} (there can be more than one); the
- ``\isacommand{bind}-part'' will be called \emph{binders}. A body can only occur
- in \emph{one} binding clause. A binder, in contrast, may occur in several binding
- clauses, but cannot occur as a body.
+ ``\isacommand{bind}-part'' will be called \emph{binders}.
+
+ In contrast to Ott, we allow multiple labels in binders and bodies. For example
+ we permit binding clauses as follows:
+
+ \begin{center}
+ \begin{tabular}{ll}
+ @{text "Foo x::name y::name t::lam s::lam"} &
+ \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ There are a few restrictions we need to impose: First, a body can only occur in
+ \emph{one} binding clause of a term constructor. A binder, in contrast, may
+ occur in several binding clauses, but cannot occur as a body.
In addition we distinguish between \emph{shallow} and \emph{deep}
binders. Shallow binders are of the form \isacommand{bind}\; {\it labels}\;
@@ -978,17 +964,9 @@
\end{center}
\noindent
- Note that in this specification \emph{name} refers to an atom type.
- Shallow binders may also ``share'' several bodies, for instance @{text t}
- and @{text s} in the following term-constructor
-
- \begin{center}
- \begin{tabular}{ll}
- @{text "Foo x::name y::name t::lam s::lam"} &
- \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}
- \end{tabular}
- \end{center}
-
+ Note that in this specification @{text "name"} refers to an atom type, and
+ @{text "fset"} to the type of finite sets.
+
A \emph{deep} binder uses an auxiliary binding function that ``picks'' out
the atoms in one argument of the term-constructor, which can be bound in
other arguments and also in the same argument (we will
@@ -1055,7 +1033,7 @@
and also all atoms from @{text q} in @{text t}. Unfortunately, we have no way
to determine whether the binder came from the binding function @{text
"bn(p)"} or @{text "bn(q)"}. Similarly in the second case. The reason why
- we must exclude such specifications is that they cannot be represent by
+ we must exclude such specifications is that they cannot be represented by
the general binders described in Section \ref{sec:binders}. However
the following two term-constructors are allowed
@@ -1071,10 +1049,11 @@
\noindent
since there is no overlap of binders.
- Note that in the last example we wrote \isacommand{bind}~@{text "bn(p)"}~\isacommand{in}~@{text "p.."}.
- 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:
+ Note that in the last example we wrote \isacommand{bind}~@{text
+ "bn(p)"}~\isacommand{in}~@{text "p.."}. 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:
%
\begin{equation}\label{letrecs}
\mbox{%
@@ -1101,12 +1080,12 @@
function and alpha-equivalence relation, which we are going to describe in the
rest of this section.
- In order to simplify matters below, we shall assume specifications
+ In order to simplify some definitions, we shall assume specifications
of term-calculi are \emph{completed}. By this we mean that
for every argument of a term-constructor that is \emph{not}
already part of a binding clause, we add implicitly a special \emph{empty} binding
- clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "\<dots>"}. In case
- of the lambda-calculus, the comletion is as follows:
+ clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "label"}. In case
+ of the lambda-calculus, the completion produces
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{-1mm}}}
@@ -1123,17 +1102,15 @@
\noindent
The point of completion is that we can make definitions over the binding
- clauses, which defined purely over arguments, turned out to be unwieldy.
+ clauses and be sure to capture all arguments of a term constructor.
Having dealt with all syntax matters, the problem now is how we can turn
specifications into actual type definitions in Isabelle/HOL and then
establish a reasoning infrastructure for them. As
- Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, by just
+ Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, just
re-arranging the arguments of
- term-constructors so that binders and their bodies are next to each other, and
- then use directly the type constructors @{text "abs_set"}, @{text "abs_res"} and
- @{text "abs_list"} from Section \ref{sec:binders}, will result in an inadequate
- representatation. Therefore we will first
+ term-constructors so that binders and their bodies are next to each other will
+ result in inadequate representations. Therefore we will first
extract datatype definitions from the specification and then define
expicitly an alpha-equivalence relation over them.
@@ -1181,12 +1158,12 @@
\end{center}
\noindent
- Like the coercion function @{text atom} used earlier, @{text "atoms"} coerces
+ Like the coercion function @{text atom}, @{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}"}.
- Given the raw types @{text "ty\<^isub>1 \<dots> ty\<^isub>n"}
- we define now free-variable functions
+ Given the raw types @{text "ty\<^isub>1 \<dots> ty\<^isub>n"} we define now the
+ free-variable functions
\begin{center}
@{text "fv_ty\<^isub>1, \<dots>, fv_ty\<^isub>n"}
@@ -1210,24 +1187,25 @@
collect all atoms that are not bound), because of our rather complicated
binding mechanisms their definitions are somewhat involved. Given a
term-constructor @{text "C"} of type @{text ty} and some associated binding
- clauses, the function @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be
- the union of the values, @{text v}, calculated below for each binding
- clause.
-
+ clauses @{text bcs}, the result of the @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be
+ the union of the values, @{text v}, calculated by the rules for empty, shallow and
+ deep binding clauses:
+ %
\begin{equation}\label{deepbinder}
\mbox{%
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
- \multicolumn{2}{@ {}l}{Empty binding clauses of the form
- \isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\
+ \multicolumn{2}{@ {}l}{\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\
$\bullet$ & @{term "v = fv_ty y"} provided @{text "y"} is of type @{text "ty"}\smallskip\\
- \multicolumn{2}{@ {}l}{Shallow binders of the form
- \isacommand{bind\_set}~@{text "x\<^isub>1\<dots>x\<^isub>n"}~\isacommand{in}~@{text "y\<^isub>1\<dots>y\<^isub>m"}:}\\
- $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> fv_ty\<^isub>m y\<^isub>m) - (x\<^isub>1 \<union> \<dots> \<union> x\<^isub>n)"}
- provided the @{text "y\<^isub>i"} are of type @{text "ty\<^isub>i"}\smallskip\\
- \multicolumn{2}{@ {}l}{Deep binders of the form
- \isacommand{bind\_set}~@{text "bn x"}~\isacommand{in}~@{text "y\<^isub>1\<dots>y\<^isub>m"}:}\\
- $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> fv_ty\<^isub>m y\<^isub>m) - (bn x) \<union> (fv_bn x)"}\\
- $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> fv_ty\<^isub>m y\<^isub>m) - (bn x)"}\\
+
+ \multicolumn{2}{@ {}l}{\isacommand{bind}~@{text "x\<^isub>1..x\<^isub>n"}~\isacommand{in}~@{text "y\<^isub>1..y\<^isub>m"}:}\\
+ $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m)"}\\
+ & \hspace{10mm}@{text "- (fv_aty\<^isub>1 x\<^isub>1 \<union> .. \<union> fv_aty\<^isub>n x\<^isub>n)"}\\
+ & provided the bodies @{text "y"}$_{1..m}$ are of type @{text "ty"}$_{1..m}$ and the
+ binders @{text "x"}$_{1..n}$ of atomic types @{text "aty"}$_{1..n}$\smallskip\\
+
+ \multicolumn{2}{@ {}l}{\isacommand{bind}~@{text "bn x"}~\isacommand{in}~@{text "y\<^isub>1..y\<^isub>m"}:}\\
+ $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m) - (bn x) \<union> (fv_bn x)"}\\
+ $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m) - (bn x)"}\\
& provided the @{text "y\<^isub>i"} are of type @{text "ty\<^isub>i"}; the first
clause applies for @{text x} being a non-recursive deep binder, the
second for a recursive deep binder
@@ -1237,22 +1215,20 @@
\noindent
Similarly for the other binding modes. Note that in a non-recursive deep
binder, we have to add all atoms that are left unbound by the binding
- function @{text "bn"}. For this we use the function @{text "fv_bn"}. Assume
- for the constructor @{text "C"} the binding function equation is of the form @{text
+ function @{text "bn"}. For this we define the function @{text "fv_bn"}. Assume
+ for the constructor @{text "C"} the binding function is of the form @{text
"bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}. We again define a value
@{text v} which is exactly as in \eqref{deepbinder} for shallow and deep
- binders. We only modify the clause for empty binding clauses as follows:
-
-
+ binding clauses, except for empty binding clauses are defined as follows:
+ %
\begin{equation}\label{bnemptybinder}
\mbox{%
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
- \multicolumn{2}{@ {}l}{Empty binding clauses of the form
- \isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\
- $\bullet$ & @{term "v = fv_ty\<^isub>i y"} provided @{text "y"} does not occur in @{text "rhs"}
- and the free-variable function for the type of @{text "y"} is @{text "fv_ty\<^isub>i"}\\
- $\bullet$ & @{term "v = fv_bn\<^isub>i y"} provided @{text "y"} occurs in @{text "rhs"}
- with a recursive call @{text "bn\<^isub>i y"}\\
+ \multicolumn{2}{@ {}l}{\isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\
+ $\bullet$ & @{term "v = fv_ty y"} provided @{text "y"} does not occur in @{text "rhs"}
+ and the free-variable function for the type of @{text "y"} is @{text "fv_ty"}\\
+ $\bullet$ & @{term "v = fv_bn y"} provided @{text "y"} occurs in @{text "rhs"}
+ with a recursive call @{text "bn y"}\\
$\bullet$ & @{term "v = {}"} provided @{text "y"} occurs in @{text "rhs"},
but without a recursive call\\
\end{tabular}}
@@ -1559,7 +1535,7 @@
alpha-equivalence relations are equivariant, which we already established
in Lemma~\ref{equiv}. As a result we can establish the equations
- \begin{equation}\label{ceqvt}
+ \begin{equation}\label{calphaeqvt}
@{text "p \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n) = C\<^sup>\<alpha> (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}
\end{equation}