--- a/Paper/Paper.thy Wed Jul 07 09:34:00 2010 +0100
+++ b/Paper/Paper.thy Wed Jul 07 13:13:18 2010 +0100
@@ -26,7 +26,7 @@
alpha_res ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and
abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup> _") and
- fv ("fv'(_')" [100] 100) and
+ fv ("fa'(_')" [100] 100) and
equal ("=") and
alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
Abs ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and
@@ -43,7 +43,6 @@
section {* Introduction *}
text {*
-%%% @{text "(1, (2, 3))"}
So far, Nominal Isabelle provided a mechanism for constructing
$\alpha$-equated terms, for example lambda-terms
@@ -358,7 +357,7 @@
about them in a theorem prover would be a major pain. \medskip
\noindent
- {\bf Contributions:} We provide novel three definitions for when terms
+ {\bf Contributions:} We provide three novel definitions for when terms
involving general binders are $\alpha$-equivalent. These definitions are
inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic
proofs, we establish a reasoning infrastructure for $\alpha$-equated
@@ -424,7 +423,8 @@
Two central notions in the nominal logic work are sorted atoms and
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 sorts of atoms can be used to represent different kinds of
+ 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.
It is assumed that there is an infinite supply of atoms for each
sort. However, in the interest of brevity, we shall restrict ourselves
@@ -520,7 +520,7 @@
\end{eqnarray}
\noindent
- In some cases it can be difficult to characterise the support precisely, and
+ in some cases it can be difficult to characterise the support precisely, and
only an approximation can be established (see \eqref{suppfun} above). Reasoning about
such approximations can be simplified with the notion \emph{supports}, defined
as follows:
@@ -621,10 +621,10 @@
@{text "(bs, y)"} are $\alpha$-equivalent? (For the moment we are interested in
the notion of $\alpha$-equivalence that is \emph{not} preserved by adding
vacuous binders.) To answer this question, we identify four conditions: {\it (i)}
- given a free-variable function @{text "fv"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
+ given a free-atom function @{text "fa"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
set"}}, then @{text x} and @{text y} need to have the same set of free
- variables; moreover there must be a permutation @{text p} such that {\it
- (ii)} @{text p} leaves the free variables of @{text x} and @{text y} unchanged, but
+ atomss; moreover there must be a permutation @{text p} such that {\it
+ (ii)} @{text p} leaves the free atoms of @{text x} and @{text y} unchanged, but
{\it (iii)} ``moves'' their bound names so that we obtain modulo a relation,
say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)}
@{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
@@ -632,9 +632,9 @@
%
\begin{equation}\label{alphaset}
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
- \multicolumn{3}{l}{@{term "(as, x) \<approx>gen R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
- & @{term "fv(x) - as = fv(y) - bs"} & \mbox{\it (i)}\\
- @{text "\<and>"} & @{term "(fv(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
+ \multicolumn{3}{l}{@{term "(as, x) \<approx>gen R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+ & @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\
+ @{text "\<and>"} & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
@{text "\<and>"} & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
@{text "\<and>"} & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\
\end{array}
@@ -644,22 +644,22 @@
Note that this relation depends on the permutation @{text
"p"}; $\alpha$-equivalence between two pairs is then the relation where we
existentially quantify over this @{text "p"}. Also note that the relation is
- dependent on a free-variable function @{text "fv"} and a relation @{text
+ dependent on a free-atom function @{text "fa"} and a relation @{text
"R"}. The reason for this extra generality is that we will use
$\approx_{\,\textit{set}}$ for both ``raw'' terms and $\alpha$-equated terms. In
the latter case, @{text R} will be replaced by equality @{text "="} and we
- will prove that @{text "fv"} is equal to @{text "supp"}.
+ will prove that @{text "fa"} is equal to @{text "supp"}.
The definition in \eqref{alphaset} does not make any distinction between the
- order of abstracted variables. If we want this, then we can define $\alpha$-equivalence
+ order of abstracted atoms. If we want this, then we can define $\alpha$-equivalence
for pairs of the form \mbox{@{text "(as, x)"}} with type @{text "(atom list) \<times> \<beta>"}
as follows
%
\begin{equation}\label{alphalist}
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
- \multicolumn{2}{l}{@{term "(as, x) \<approx>lst R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
- & @{term "fv(x) - (set as) = fv(y) - (set bs)"} & \mbox{\it (i)}\\
- \wedge & @{term "(fv(x) - set as) \<sharp>* p"} & \mbox{\it (ii)}\\
+ \multicolumn{2}{l}{@{term "(as, x) \<approx>lst R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+ & @{term "fa(x) - (set as) = fa(y) - (set bs)"} & \mbox{\it (i)}\\
+ \wedge & @{term "(fa(x) - set as) \<sharp>* p"} & \mbox{\it (ii)}\\
\wedge & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
\wedge & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\
\end{array}
@@ -676,21 +676,21 @@
%
\begin{equation}\label{alphares}
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
- \multicolumn{2}{l}{@{term "(as, x) \<approx>res R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
- & @{term "fv(x) - as = fv(y) - bs"} & \mbox{\it (i)}\\
- \wedge & @{term "(fv(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
+ \multicolumn{2}{l}{@{term "(as, x) \<approx>res R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+ & @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\
+ \wedge & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
\wedge & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
\end{array}
\end{equation}
It might be useful to consider first some examples about how these definitions
of $\alpha$-equivalence pan out in practice. For this consider the case of
- abstracting a set of variables over types (as in type-schemes). We set
- @{text R} to be the usual equality @{text "="} and for @{text "fv(T)"} we
+ abstracting a set of atoms over types (as in type-schemes). We set
+ @{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we
define
\begin{center}
- @{text "fv(x) = {x}"} \hspace{5mm} @{text "fv(T\<^isub>1 \<rightarrow> T\<^isub>2) = fv(T\<^isub>1) \<union> fv(T\<^isub>2)"}
+ @{text "fa(x) = {x}"} \hspace{5mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) = fa(T\<^isub>1) \<union> fa(T\<^isub>2)"}
\end{center}
\noindent
@@ -946,13 +946,14 @@
%of the specifications (the corresponding $\alpha$-equivalence will differ). We will
%show this later with an example.
- There are also some restrictions we need to impose on binding clauses. The
+ There are also some restrictions we need to impose on our binding clauses in comparison to
+ the ones of Ott. The
main idea behind these restrictions is that we obtain a sensible notion of
- $\alpha$-equivalence where it is ensured that within a given scope a
- variable occurence cannot be both bound and free at the same time. The first
+ $\alpha$-equivalence where it is ensured that within a given scope an
+ atom occurence cannot be both bound and free at the same time. The first
restriction is that a body can only occur in
\emph{one} binding clause of a term constructor (this ensures that the bound
- variables of a body cannot be free at the same time by specifying an
+ atoms of a body cannot be free at the same time by specifying an
alternative binder for the same body). For binders we distinguish between
\emph{shallow} and \emph{deep} binders. Shallow binders are just
labels. The restriction we need to impose on them is that in case of
@@ -1068,9 +1069,9 @@
The difference is that with @{text Let} we only want to bind the atoms @{text
"bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms
inside the assignment. This difference has consequences for the associated
- notions of free-variables and $\alpha$-equivalence.
+ notions of free-atoms and $\alpha$-equivalence.
- To make sure that variables bound by deep binders cannot be free at the
+ To make sure that atoms bound by deep binders cannot be free at the
same time, we cannot have more than one binding function for a deep binder.
Consequently we exclude specifications such as
@@ -1086,7 +1087,9 @@
\noindent
Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"} pick
- out different atoms to become bound, respectively be free, in @{text "p"}.
+ out different atoms to become bound, respectively be free, in @{text "p"}
+ (since the Ott-tool does not derive a reasoning for $\alpha$-equated terms, it can permit
+ such specifications).
We also need to restrict the form of the binding functions in order
to ensure the @{text "bn"}-functions can be defined for $\alpha$-equated
@@ -1107,7 +1110,7 @@
(case @{text PTup}). This restriction will simplify some automatic definitions and proofs
later on.
- In order to simplify our definitions of free variables and $\alpha$-equivalence,
+ In order to simplify our definitions of free atoms and $\alpha$-equivalence,
we shall assume specifications
of term-calculi are implicitly \emph{completed}. By this we mean that
for every argument of a term-constructor that is \emph{not}
@@ -1132,7 +1135,7 @@
clauses and be sure to have captured all arguments of a term constructor.
*}
-section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *}
+section {* Alpha-Equivalence and Free Atoms\label{sec:alpha} *}
text {*
Having dealt with all syntax matters, the problem now is how we can turn
@@ -1141,7 +1144,7 @@
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 will
- result in inadequate representations in cases like @{text "Let x\<^isub>1=t\<^isub>1\<dots>x\<^isub>n=t\<^isub>n in s"}.
+ result in inadequate representations in cases like @{text "Let x\<^isub>1 = t\<^isub>1\<dots>x\<^isub>n = t\<^isub>n in s"}.
Therefore we will first
extract ``raw'' datatype definitions from the specification and then define
explicitly an $\alpha$-equivalence relation over them. We subsequently
@@ -1168,8 +1171,8 @@
The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are
non-empty and the types in the constructors only occur in positive
position (see \cite{Berghofer99} for an indepth description of the datatype package
- in Isabelle/HOL). We then define the user-specified binding
- functions @{term "bn"} by recursion over the corresponding
+ in Isabelle/HOL). We then define each of the user-specified binding
+ function @{term "bn\<^isub>i"} by recursion over the corresponding
raw datatype. We can also easily define permutation operations by
recursion so that for each term constructor @{text "C"} we have that
%
@@ -1178,21 +1181,21 @@
\end{equation}
The first non-trivial step we have to perform is the generation of
- free-variable functions from the specifications. For the
- \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-variable functions
+ free-atom functions from the specifications. For the
+ \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions
%
\begin{equation}\label{fvars}
- @{text "fv_ty\<^isub>1, \<dots>, fv_ty\<^isub>n"}
+ @{text "fa_ty\<^isub>1, \<dots>, fa_ty\<^isub>n"}
\end{equation}
\noindent
by mutual recursion.
- We define these functions together with auxiliary free-variable functions for
+ We define these functions together with auxiliary free-atom functions for
the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$
we define
%
\begin{center}
- @{text "fv_bn\<^isub>1, \<dots>, fv_bn\<^isub>m"}
+ @{text "fa_bn\<^isub>1, \<dots>, fa_bn\<^isub>m"}
\end{center}
\noindent
@@ -1200,14 +1203,14 @@
bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function
that calculates those unbound atoms in a deep binder.
- While the idea behind these free-variable functions is clear (they just
+ While the idea behind these free-atom functions is clear (they just
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 @{text "bc\<^isub>1\<dots>bc\<^isub>k"}, the result of @{text
- "fv_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be the union @{text
- "fv(bc\<^isub>1) \<union> \<dots> \<union> fv(bc\<^isub>k)"} where we define below what @{text "fv"} of a binding
- clause means. We only show the mode \isacommand{bind\_set} (the other modes are similar).
+ "fa_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be the union @{text
+ "fa(bc\<^isub>1) \<union> \<dots> \<union> fa(bc\<^isub>k)"} where we define below what @{text "fa"} for a binding
+ clause means. We only show the details for the mode \isacommand{bind\_set} (the other modes are similar).
Suppose the binding clause @{text bc\<^isub>i} is of the form
%
\begin{equation}
@@ -1225,20 +1228,20 @@
then the free atoms of the binding clause @{text bc\<^isub>i} are given by
%
\begin{center}
- @{text "fv(bc\<^isub>i) \<equiv> (D - B) \<union> B'"}
+ @{text "fa(bc\<^isub>i) \<equiv> (D - B) \<union> B'"}
\end{center}
\noindent
- The set @{text D} is formally defined as
+ whereby the set @{text D} is formally defined as
%
\begin{center}
- @{text "D \<equiv> fv_ty\<^isub>1 d\<^isub>1 \<union> ... \<union> fv_ty\<^isub>q d\<^isub>q"}
+ @{text "D \<equiv> fa_ty\<^isub>1 d\<^isub>1 \<union> ... \<union> fa_ty\<^isub>q d\<^isub>q"}
\end{center}
\noindent
- whereby the functions @{text "fv_ty\<^isub>i"} are the ones we are defining by recursion
- (see \eqref{fvars}) provided the @{text "d\<^isub>i"} refers to one of the raw types
- @{text "ty"}$_{1..n}$ from the specification; otherwise we set @{text "fv_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
+ The functions @{text "fa_ty\<^isub>i"} are the ones we are defining by recursion
+ (see \eqref{fvars}) in case the @{text "d\<^isub>i"} refers to one of the raw types
+ @{text "ty"}$_{1..n}$ from the specification; otherwise we set @{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
In order to define the set @{text B} we use the following auxiliary @{text "bn"}-functions
for atom types to which shallow binders have to refer
%
@@ -1262,7 +1265,7 @@
\noindent
The set @{text "B'"} collects all free atoms in non-recursive deep
- binders. Lets assume these binders in @{text "bc\<^isub>i"} are
+ binders. Let us assume these binders in @{text "bc\<^isub>i"} are
%
\begin{center}
@{text "bn\<^isub>1 a\<^isub>1, \<dots>, bn\<^isub>r a\<^isub>r"}
@@ -1273,71 +1276,71 @@
"d"}$_{1..q}$. The set @{text "B'"} is defined as
%
\begin{center}
- @{text "B' \<equiv> fv_bn\<^isub>1 a\<^isub>1 \<union> ... \<union> fv_bn\<^isub>r a\<^isub>r"}
+ @{text "B' \<equiv> fa_bn\<^isub>1 a\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r a\<^isub>r"}
\end{center}
\noindent
- This completes the definition of the free-variable functions.
+ This completes the definition of the free-atom functions.
Note that for non-recursive deep binders, we have to add all atoms that are left
- unbound by the binding function @{text "bn"}. This is the purpose of the functions
- @{text "fv_bn"}, also defined by recursion. Assume the user specified
+ unbound by the binding function @{text "bn"} (the set @{text "B'"}). We use for this
+ the functions @{text "fa_bn"}, also defined by recursion. Assume the user specified
a @{text bn}-clause of the form
%
\begin{center}
- @{text "bn (C z\<^isub>1 \<dots> z\<^isub>n) = rhs"}
+ @{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
\end{center}
\noindent
- where the @{text "z"}$_{1..n}$ are of types @{text "ty"}$_{1..n}$. For each of
+ where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$. For each of
the arguments we calculate the free atoms as follows:
%
\begin{center}
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
- $\bullet$ & @{term "fv_ty\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text "rhs"}
- (nothing gets bound in @{text "z\<^isub>i"}),\\
- $\bullet$ & @{term "fv_bn\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} occurs in @{text "rhs"}
+ $\bullet$ & @{term "fa_ty\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text "rhs"}
+ (that means nothing is bound in @{text "z\<^isub>i"}),\\
+ $\bullet$ & @{term "fa_bn\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} occurs in @{text "rhs"}
with the recursive call @{text "bn\<^isub>i z\<^isub>i"}, and\\
$\bullet$ & @{term "{}"} provided @{text "z\<^isub>i"} occurs in @{text "rhs"},
- but without a recursive call
+ but without a recursive call.
\end{tabular}
\end{center}
\noindent
- For defining @{text "fv_bn (C z\<^isub>1 \<dots> z\<^isub>n)"} we just union up all these values.
+ For defining @{text "fa_bn (C z\<^isub>1 \<dots> z\<^isub>n)"} we just union up all these values.
To see how these definitions work in practice, let us reconsider the term-constructors
@{text "Let"} and @{text "Let_rec"}, as well as @{text "ANil"} and @{text "ACons"}
from the example shown in \eqref{letrecs}.
- For them we define three free-variable functions, namely
- @{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"} as follows:
+ For them we define three free-atom functions, namely
+ @{text "fa\<^bsub>trm\<^esub>"}, @{text "fa\<^bsub>assn\<^esub>"} and @{text "fa\<^bsub>bn\<^esub>"} as follows:
%
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
- @{text "fv\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "(fv\<^bsub>trm\<^esub> t - set (bn as)) \<union> fv\<^bsub>bn\<^esub> as"}\\
- @{text "fv\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fv\<^bsub>assn\<^esub> as \<union> fv\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm]
+ @{text "fa\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t - set (bn as)) \<union> fa\<^bsub>bn\<^esub> as"}\\
+ @{text "fa\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fa\<^bsub>assn\<^esub> as \<union> fa\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm]
- @{text "fv\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
- @{text "fv\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(supp a) \<union> (fv\<^bsub>trm\<^esub> t) \<union> (fv\<^bsub>assn\<^esub> as)"}\\[1mm]
+ @{text "fa\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
+ @{text "fa\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(supp a) \<union> (fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>assn\<^esub> as)"}\\[1mm]
- @{text "fv\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
- @{text "fv\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(fv\<^bsub>trm\<^esub> t) \<union> (fv\<^bsub>bn\<^esub> as)"}
+ @{text "fa\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
+ @{text "fa\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>bn\<^esub> as)"}
\end{tabular}
\end{center}
\noindent
- To see the ``pattern'', recall that @{text ANil} and @{text "ACons"} have no
- binding clause in the specification. The corresponding free-variable
- function @{text "fv\<^bsub>assn\<^esub>"} therefore returns all atoms
+ To see the pattern, recall that @{text ANil} and @{text "ACons"} have no
+ binding clause in the specification. The corresponding free-atom
+ function @{text "fa\<^bsub>assn\<^esub>"} therefore returns all atoms
occurring in an assignment. The binding only takes place in @{text Let} and
@{text "Let_rec"}. In the @{text "Let"}-clause, the binding clause specifies
that all atoms given by @{text "set (bn as)"} have to be bound in @{text
t}. Therefore we have to subtract @{text "set (bn as)"} from @{text
- "fv\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are
+ "fa\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are
free in @{text "as"}. In contrast, in @{text "Let_rec"} we have a recursive
binder where we want to also bind all occurrences of the atoms in @{text
"set (bn as)"} also inside @{text "as"}. Therefore we have to subtract
- @{text "set (bn as)"} from the union @{text "fv\<^bsub>trm\<^esub> t"} and @{text "fv\<^bsub>assn\<^esub> as"}.
+ @{text "set (bn as)"} from the union @{text "fa\<^bsub>trm\<^esub> t"} and @{text "fa\<^bsub>assn\<^esub> as"}.
An interesting point in this
example is that a ``naked'' assignment does not bind any
@@ -1349,14 +1352,14 @@
$\alpha$-equivalence.
Next we define $\alpha$-equivalence relations for the raw types @{text
- "ty"}$_{1..n}$. We call them
+ "ty"}$_{1..n}$. We write them
%
\begin{center}
@{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}.
\end{center}
\noindent
- Like with the free-variable functions, we also need to
+ Like with the free-atom functions, we also need to
define auxiliary $\alpha$-equivalence relations
%
\begin{center}
@@ -1366,13 +1369,13 @@
\noindent
for the binding functions @{text "bn"}$_{1..m}$,
To simplify our definitions we will use the following abbreviations for
- equivalence relations and free-variable functions acting on pairs
+ equivalence relations and free-atom functions acting on pairs
%
\begin{center}
\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
@{text "(x\<^isub>1, y\<^isub>1) (R\<^isub>1 \<otimes> R\<^isub>2) (x\<^isub>2, y\<^isub>2)"} & @{text "\<equiv>"} & @{text "x\<^isub>1 R\<^isub>1 y\<^isub>1 \<and> x\<^isub>2 R\<^isub>2 y\<^isub>2"}\\
- @{text "(fv\<^isub>1 \<oplus> fv\<^isub>2) (x, y)"} & @{text "\<equiv>"} & @{text "fv\<^isub>1 x \<union> fv\<^isub>2 y"}\\
+ @{text "(fa\<^isub>1 \<oplus> fa\<^isub>2) (x, y)"} & @{text "\<equiv>"} & @{text "fa\<^isub>1 x \<union> fa\<^isub>2 y"}\\
\end{tabular}
\end{center}
@@ -1394,15 +1397,15 @@
(*<*)
consts alpha_ty ::'a
consts alpha_trm ::'a
-consts fv_trm :: 'a
+consts fa_trm :: 'a
consts alpha_trm2 ::'a
-consts fv_trm2 :: 'a
+consts fa_trm2 :: 'a
notation (latex output)
alpha_ty ("\<approx>ty") and
alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and
- fv_trm ("fv\<^bsub>trm\<^esub>") and
+ fa_trm ("fa\<^bsub>trm\<^esub>") and
alpha_trm2 ("\<approx>\<^bsub>assn\<^esub> \<otimes> \<approx>\<^bsub>trm\<^esub>") and
- fv_trm2 ("fv\<^bsub>assn\<^esub> \<oplus> fv\<^bsub>trm\<^esub>")
+ fa_trm2 ("fa\<^bsub>assn\<^esub> \<oplus> fa\<^bsub>trm\<^esub>")
(*>*)
text {*
*TBD below *
@@ -1419,18 +1422,18 @@
\multicolumn{2}{@ {}l}{Shallow binders of the form
\isacommand{bind\_set}~@{text "x\<^isub>1\<dots>x\<^isub>n"}~\isacommand{in}~@{text "x'\<^isub>1\<dots>x'\<^isub>m"}:}\\
$\bullet$ & Assume the bodies @{text "x'\<^isub>1\<dots>x'\<^isub>m"} are of type @{text "ty\<^isub>1\<dots>ty\<^isub>m"},
- @{text "R"} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fv} is
- @{text "fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}, then
+ @{text "R"} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fa} is
+ @{text "fa_ty\<^isub>1 \<oplus> ... \<oplus> fa_ty\<^isub>m"}, then
\begin{center}
- @{term "\<exists>p. (x\<^isub>1 \<union> \<xi> \<union> x\<^isub>n, (x'\<^isub>1,\<xi>,x'\<^isub>m)) \<approx>gen R fv p (y\<^isub>1 \<union> \<xi> \<union> y\<^isub>n, (y'\<^isub>1,\<xi>,y'\<^isub>m))"}
+ @{term "\<exists>p. (x\<^isub>1 \<union> \<xi> \<union> x\<^isub>n, (x'\<^isub>1,\<xi>,x'\<^isub>m)) \<approx>gen R fa p (y\<^isub>1 \<union> \<xi> \<union> y\<^isub>n, (y'\<^isub>1,\<xi>,y'\<^isub>m))"}
\end{center}\\
\multicolumn{2}{@ {}l}{Deep binders of the form
\isacommand{bind\_set}~@{text "bn x"}~\isacommand{in}~@{text "x'\<^isub>1\<dots>x'\<^isub>m"}:}\\
$\bullet$ & Assume the bodies @{text "x'\<^isub>1\<dots>x'\<^isub>m"} are of type @{text "ty\<^isub>1\<dots>ty\<^isub>m"},
- @{text "R"} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fv} is
- @{text "fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}, then for recursive deep binders
+ @{text "R"} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fa} is
+ @{text "fa_ty\<^isub>1 \<oplus> ... \<oplus> fa_ty\<^isub>m"}, then for recursive deep binders
\begin{center}
- @{term "\<exists>p. (bn x, (x'\<^isub>1,\<xi>,x'\<^isub>m)) \<approx>gen R fv p (bn y, (y'\<^isub>1,\<xi>,y'\<^isub>m))"}
+ @{term "\<exists>p. (bn x, (x'\<^isub>1,\<xi>,x'\<^isub>m)) \<approx>gen R fa p (bn y, (y'\<^isub>1,\<xi>,y'\<^isub>m))"}
\end{center}\\
$\bullet$ & for non-recursive binders we generate in addition @{text "x \<approx>bn y"}\\
\end{tabular}}
@@ -1472,9 +1475,9 @@
\begin{center}
\begin{tabular}{@ {}c @ {}}
\infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
- {@{text "as \<approx>\<^bsub>bn\<^esub> as'"} & @{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fv_trm p (bn as', t')"}}\smallskip\\
+ {@{text "as \<approx>\<^bsub>bn\<^esub> as'"} & @{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"}}\smallskip\\
\infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
- {@{term "\<exists>p. (bn as, (as, t)) \<approx>lst alpha_trm2 fv_trm2 p (bn as', (as', t'))"}}
+ {@{term "\<exists>p. (bn as, (as, t)) \<approx>lst alpha_trm2 fa_trm2 p (bn as', (as', t'))"}}
\end{tabular}
\end{center}
@@ -1532,8 +1535,8 @@
"ty\<AL>\<^bsub>1..n\<^esub>"} representing $\alpha$-equated terms of types @{text "ty\<^bsub>1..n\<^esub>"}. We also obtain
definitions for the term-constructors @{text
"C"}$^\alpha_{1..m}$ from the raw term-constructors @{text
- "C"}$_{1..m}$, and similar definitions for the free-variable functions @{text
- "fv_ty"}$^\alpha_{1..n}$ and the binding functions @{text
+ "C"}$_{1..m}$, and similar definitions for the free-atom functions @{text
+ "fa_ty"}$^\alpha_{1..n}$ and the binding functions @{text
"bn"}$^\alpha_{1..k}$. However, these definitions are not really useful to the
user, since they are given in terms of the isomorphisms we obtained by
creating new types in Isabelle/HOL (recall the picture shown in the
@@ -1619,25 +1622,25 @@
\noindent
for our infrastructure. In a similar fashion we can lift the equations
- characterising the free-variable functions @{text "fn_ty\<AL>\<^isub>j"} and @{text "fv_bn\<AL>\<^isub>k"}, and the
+ characterising the free-atom functions @{text "fn_ty\<AL>\<^isub>j"} and @{text "fa_bn\<AL>\<^isub>k"}, and the
binding functions @{text "bn\<AL>\<^isub>k"}. The necessary respectfulness lemmas for these
lifting are the properties:
%
\begin{equation}\label{fnresp}
\mbox{%
\begin{tabular}{l}
- @{text "x \<approx>ty\<^isub>j y"} implies @{text "fv_ty\<^isub>j x = fv_ty\<^isub>j y"}\\
- @{text "x \<approx>ty\<^isub>k y"} implies @{text "fv_bn\<^isub>k x = fv_bn\<^isub>k y"}\\
+ @{text "x \<approx>ty\<^isub>j y"} implies @{text "fa_ty\<^isub>j x = fa_ty\<^isub>j y"}\\
+ @{text "x \<approx>ty\<^isub>k y"} implies @{text "fa_bn\<^isub>k x = fa_bn\<^isub>k y"}\\
@{text "x \<approx>ty\<^isub>k y"} implies @{text "bn\<^isub>k x = bn\<^isub>k y"}
\end{tabular}}
\end{equation}
\noindent
which can be established by induction on @{text "\<approx>ty"}. Whereas the first
- property is always true by the way we defined the free-variable
+ property is always true by the way we defined the free-atom
functions for types, the second and third do \emph{not} hold in general. There is, in principle,
the possibility that the user defines @{text "bn\<^isub>k"} so that it returns an already bound
- variable. Then the third property is just not true. However, our
+ atom. Then the third property is just not true. However, our
restrictions imposed on the binding functions
exclude this possibility.
@@ -1662,13 +1665,13 @@
the lifting part of establishing the reasoning infrastructure.
By working now completely on the $\alpha$-equated level, we can first show that
- the free-variable functions and binding functions
+ the free-atom functions and binding functions
are equivariant, namely
\begin{center}
\begin{tabular}{rcl}
- @{text "p \<bullet> (fv_ty\<^sup>\<alpha> x)"} & $=$ & @{text "fv_ty\<^sup>\<alpha> (p \<bullet> x)"}\\
- @{text "p \<bullet> (fv_bn\<^sup>\<alpha> x)"} & $=$ & @{text "fv_bn\<^sup>\<alpha> (p \<bullet> x)"}\\
+ @{text "p \<bullet> (fa_ty\<^sup>\<alpha> x)"} & $=$ & @{text "fa_ty\<^sup>\<alpha> (p \<bullet> x)"}\\
+ @{text "p \<bullet> (fa_bn\<^sup>\<alpha> x)"} & $=$ & @{text "fa_bn\<^sup>\<alpha> (p \<bullet> x)"}\\
@{text "p \<bullet> (bn\<^sup>\<alpha> x)"} & $=$ & @{text "bn\<^sup>\<alpha> (p \<bullet> x)"}
\end{tabular}
\end{center}
@@ -1697,11 +1700,11 @@
\noindent
by a structural induction over @{text "x\<^isub>1, \<dots>, x\<^isub>n"} (whereby @{text "x\<^isub>i"} ranges over the types
@{text "ty\<AL>\<^isub>1 \<dots> ty\<AL>\<^isub>n"}). Lastly, we can show that the support of elements in
- @{text "ty\<AL>\<^bsub>1..n\<^esub>"} coincides with @{text "fv_ty\<AL>\<^bsub>1..n\<^esub>"}.
+ @{text "ty\<AL>\<^bsub>1..n\<^esub>"} coincides with @{text "fa_ty\<AL>\<^bsub>1..n\<^esub>"}.
\begin{lemma}
For every @{text "x\<^isub>i"} of type @{text "ty\<AL>\<^bsub>1..n\<^esub>"}, we have that
- @{text "supp x\<^isub>i = fv_ty\<AL>\<^isub>i x\<^isub>i"} holds.
+ @{text "supp x\<^isub>i = fa_ty\<AL>\<^isub>i x\<^isub>i"} holds.
\end{lemma}
\begin{proof}
@@ -1846,7 +1849,7 @@
\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 "fv_bn\<^isup>\<alpha> x = fv_bn\<^isup>\<alpha> (p \<bullet>\<^bsub>bn\<^esub>\<^sup>\<alpha> x)"}.
+ @{text "fa_bn\<^isup>\<alpha> x = fa_bn\<^isup>\<alpha> (p \<bullet>\<^bsub>bn\<^esub>\<^sup>\<alpha> x)"}.
\end{lemma}
\begin{proof}
@@ -1857,8 +1860,8 @@
\noindent
The first property states that a permutation applied to a binding function is
equivalent to first permuting the binders and then calculating the bound
- variables. The second amounts to the fact that permuting the binders has no
- effect on the free-variable function. The main point of this permutation
+ atoms. The second amounts to the fact that permuting the binders has no
+ effect on the free-atom function. The main point of this permutation
function, however, is that if we have a permutation that is fresh
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
@@ -2103,7 +2106,7 @@
We can also see that
%
\begin{equation}\label{bnprop}
- @{text "fv_ty x = bn x \<union> fv_bn x"}.
+ @{text "fa_ty x = bn x \<union> fa_bn x"}.
\end{equation}
\noindent