--- a/Paper/Paper.thy Mon Mar 22 16:22:28 2010 +0100
+++ b/Paper/Paper.thy Mon Mar 22 18:19:13 2010 +0100
@@ -385,36 +385,34 @@
section {* General Binders *}
text {*
- In order to keep our work manageable we give need to give definitions
- and perform proofs inside Isabelle wherever possible, as opposed to write
- custom ML-code that generates them for each
- instance of a term-calculus. To this end we will first consider pairs
+ In Nominal Isabelle the user is expected to write down a specification of a
+ term-calculus and a reasoning infrastructure is then automatically derived
+ from this specifcation (remember that Nominal Isabelle is a definitional
+ extension of Isabelle/HOL and cannot introduce new axioms).
+
- \begin{equation}\label{three}
- \mbox{@{text "(as, x) :: (atom set) \<times> \<beta>"}}
- \end{equation}
-
- \noindent
- consisting of a set of atoms and an object of generic type. These pairs
- are intended to represent the abstraction or binding of the set $as$
- in the body $x$ (similarly to type-schemes given in \eqref{tysch}).
+ In order to keep our work manageable, we will wherever possible state
+ definitions and perform proofs inside Isabelle, as opposed to write custom
+ ML-code that generates them for each instance of a term-calculus. To that
+ end, we will consider pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}.
+ These pairs are intended to represent the abstraction, or binding, of the set $as$
+ in the body $x$.
- The first question we have to answer is when we should consider pairs such as
- $(as, x)$ and $(bs, y)$ as alpha-equivalent? (At the moment we are interested in
+ The first question we have to answer is when the pairs $(as, x)$ and $(bs, y)$ are
+ alpha-equivalent? (At the moment we are interested in
the notion of alpha-equivalence that is \emph{not} preserved by adding
- vacuous binders.) To answer this we identify four conditions: {\it i)} given
- a free-variable function of type \mbox{@{text "fv :: \<beta> \<Rightarrow> atom set"}}, then $x$ and $y$
+ vacuous binders.) To answer this, we identify four conditions: {\it i)} given
+ a free-variable function $\fv$ of type \mbox{@{text "\<beta> \<Rightarrow> atom set"}}, then $x$ and $y$
need to have the same set of free variables; moreover there must be a permutation,
- $p$ that {\it ii)} leaves the free variables $x$ and $y$ unchanged,
- but {\it iii)} ``moves'' their bound names so that we obtain modulo a relation,
+ $p$ so that {\it ii)} it leaves the free variables $x$ and $y$ unchanged,
+ but {\it iii)} ``moves'' their bound names such that we obtain modulo a relation,
say \mbox{@{text "_ R _"}}, two equal terms. We also require {\it iv)} that $p$ makes
- the abstracted sets $as$ and $bs$ equal (since at the moment we do not want
- that the sets $as$ and $bs$ differ on vacuous binders). These requirements can
- be stated formally as follows
+ the abstracted sets $as$ and $bs$ equal. The requirements {\it i)} to {\it iv)} can
+ be stated formally as follows:
%
\begin{equation}\label{alphaset}
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
- \multicolumn{2}{l}{(as, x) \approx_{set}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
+ \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{set}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
& @{text "fv(x) - as = fv(y) - bs"}\\
\wedge & @{text "fv(x) - as #* p"}\\
\wedge & @{text "(p \<bullet> x) R y"}\\
@@ -423,20 +421,23 @@
\end{equation}
\noindent
- Alpha equivalence between such pairs is then the relation with the additional
- existential quantification over $p$. Note that this relation is additionally
- dependent on the free-variable function $\fv$ and the relation $R$. The reason
- for this generality is that we want to use $\approx_{set}$ for both ``raw'' terms
- and alpha-equated terms. In the latter case, $R$ can be replaced by equality $(op =)$ and
- we are going to prove that $\fv$ will be equal to the support of $x$ and $y$.
+ Note that this relation is dependent on $p$. Alpha-equivalence is then the relation where
+ we existentially quantify over this $p$.
+ Also note that the relation is dependent on a free-variable function $\fv$ and a relation
+ $R$. The reason for this extra generality is that we will use $\approx_{set}$ for both
+ ``raw'' terms and alpha-equated terms. In the latter case, $R$ will be replaced by
+ equality $(op =)$ and we are going to prove that $\fv$ will be equal to the support
+ of $x$ and $y$. To have these parameters means, however, we can derive properties about
+ them generically.
The definition in \eqref{alphaset} does not make any distinction between the
- order of abstracted variables. If we do want this then we can define alpha-equivalence
- for pairs of the form \mbox{@{text "(as, x) :: (atom list) \<times> \<beta>"}} by
+ order of abstracted variables. 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}
- \multicolumn{2}{l}{(as, x) \approx_{list}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
+ \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{list}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
& @{text "fv(x) - (set as) = fv(y) - (set bs)"}\\
\wedge & @{text "fv(x) - (set as) #* p"}\\
\wedge & @{text "(p \<bullet> x) R y"}\\
@@ -448,34 +449,65 @@
where $set$ is just the function that coerces a list of atoms into a set of atoms.
If we do not want to make any difference between the order of binders and
- allow vacuous binders, then we just need to drop the fourth condition in \eqref{alphaset}
- and define
+ also allow vacuous binders, then we keep sets of binders, but drop the fourth
+ condition in \eqref{alphaset}:
%
- \begin{equation}\label{alphaset}
+ \begin{equation}\label{alphares}
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
- \multicolumn{2}{l}{(as, x) \approx_{res}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
+ \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{res}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
& @{text "fv(x) - as = fv(y) - bs"}\\
\wedge & @{text "fv(x) - as #* p"}\\
\wedge & @{text "(p \<bullet> x) R y"}\\
\end{array}
\end{equation}
- To get a feeling how these definitions pan out in practise consider the case of
- abstracting names over types (like in type-schemes). For this we set $R$ to be
- the equality and for $\fv(T)$ we define
+ \begin{exmple}\rm
+ It might be useful to consider some examples for how these definitions pan out in practise.
+ For this consider the case of abstracting a set of variables over types (as in type-schemes).
+ We set $R$ to be the equality and for $\fv(T)$ we define
\begin{center}
$\fv(x) = \{x\} \qquad \fv(T_1 \rightarrow T_2) = \fv(T_1) \cup \fv(T_2)$
\end{center}
\noindent
- Now reacall the examples in \eqref{ex1}, \eqref{ex2} and \eqref{ex3}: it can be easily
- checked that @{text "({x,y}, x \<rightarrow> y)"} and
- @{text "({y,x}, y \<rightarrow> x)"} are equal according to $\approx_{set}$ and $\approx_{ref}$ by taking $p$ to
- be the swapping @{text "(x \<rightleftharpoons> y)"}; but assuming @{text "x \<noteq> y"} then for instance
- $([x,y], x \rightarrow y) \not\approx_{list} ([y,x], x \rightarrow y)$ since there is no permutation that
- makes the lists @{text "[x,y]"} and @{text "[y,x]"} equal, but leaves the type \mbox{@{text "x \<rightarrow> y"}}
- unchanged.
+ Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and \eqref{ex3}. It can be easily
+ checked that @{text "({x, y}, x \<rightarrow> y)"} and
+ @{text "({y, x}, y \<rightarrow> x)"} are equal according to $\approx_{set}$ and $\approx_{res}$ by taking $p$ to
+ be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"} then
+ $([x, y], x \rightarrow y) \not\approx_{list} ([y,x], x \rightarrow y)$ since there is no permutation that
+ makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and in addition leaves the
+ type \mbox{@{text "x \<rightarrow> y"}} unchanged. Again if @{text "x \<noteq> y"}, we have that
+ $(\{x\}, x) \approx_{res} (\{x,y\}, x)$ by taking $p$ to be the identity permutation.
+ However $(\{x\}, x) \not\approx_{set} (\{x,y\}, x)$ since there is no permutation that makes
+ the sets $\{x\}$ and $\{x,y\}$ equal (similarly for $\approx_{list}$).
+ \end{exmple}
+
+ \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}
*}
section {* Alpha-Equivalence and Free Variables *}