nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:6df6468f3c05
+:028705c98304
 that makes the
 sets @{text "{x}"} and @{text "{x, y}"} equal (similarly for $\approx_{\textit{list}}$).
 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
 %
 \begin{equation}
 @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_gen (as, x) equal supp p (bs, x)"}
 \end{equation}
 \noindent
-(similarly for $\approx_{\textit{abs\_list}}$
+(similarly for $\approx_{\textit{abs\_res}}$
-and $\approx_{\textit{abs\_res}}$). We can show that these relations are equivalence
+and $\approx_{\textit{abs\_list}}$). We can show that these relations are equivalence
 relations and equivariant.
 \begin{lemma}\label{alphaeq}
 The relations $\approx_{\textit{abs\_set}}$, $\approx_{\textit{abs\_list}}$
 and $\approx_{\textit{abs\_res}}$ are equivalence relations, and if @{term
 @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
 Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes
 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
+form @{term "Abs as x"} etc is motivated by the fact that
-can be conveninetly established at the Isabelle/HOL level.  It would be
+we can conveniently establish  at the Isabelle/HOL level
-difficult to write custom ML-code that derives automatically such properties
+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} *}
 text {*
 The first mode is for binding lists of atoms (the order of binders matters);
 the second is for sets of binders (the order does not matter, but the
 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
+``\isacommand{bind}-part'' will be called \emph{binders}.
-in \emph{one} binding clause. A binder, in contrast, may occur in several binding
-clauses, but cannot occur as a body.
+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}\;
 \isacommand{in}\; {\it labels'} (similar for the other two modes). The
 restriction we impose on shallow binders is that the {\it labels} must either
 \end{tabular}
 \end{tabular}
 \end{center}
 \noindent
-Note that in this specification \emph{name} refers to an atom type.
+Note that in this specification @{text "name"} refers to an atom type, and
-Shallow binders may also ``share'' several bodies, for instance @{text t}
+@{text "fset"} to the type of finite sets.
-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}
 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
 call such binders \emph{recursive}, see below).
 The corresponding binding functions are expected to return either a set of atoms
 \noindent
 In the first case the intention is to bind all atoms from the pattern @{text p} in @{text t}
 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
 \begin{center}
 \begin{tabular}{ll}
 \end{center}
 \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.."}.
+Note that in the last example we wrote \isacommand{bind}~@{text
-Whenever such a binding clause is present, we will call the corresponding binder \emph{recursive}.
+"bn(p)"}~\isacommand{in}~@{text "p.."}.  Whenever such a binding clause is
-To see the purpose of such recursive binders, compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s
+present, we will call the corresponding binder \emph{recursive}.  To see the
-in the following specification:
+purpose of such recursive binders, compare ``plain'' @{text "Let"}s and
+@{text "Let_rec"}s in the following specification:
 %
 \begin{equation}\label{letrecs}
 \mbox{%
 \begin{tabular}{@ {}l@ {}}
 \isacommand{nominal\_datatype}~@{text "trm ="}\\
 "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 free-variable
 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
+clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "label"}. In case
-of the lambda-calculus, the comletion is as follows:
+of the lambda-calculus, the completion produces
 \begin{center}
 \begin{tabular}{@ {}l@ {\hspace{-1mm}}}
 \isacommand{nominal\_datatype} @{text lam} =\\
 \hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"}
 \end{tabular}
 \end{center}
 \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
+term-constructors so that binders and their bodies are next to each other will
-then use directly the type constructors @{text "abs_set"}, @{text "abs_res"} and
+result in inadequate representations. Therefore we will first
-@{text "abs_list"} from Section \ref{sec:binders}, will result in an inadequate
-representatation. Therefore we will first
 extract datatype definitions from the specification and then define
 expicitly an alpha-equivalence relation over them.
 The datatype definition can be obtained by stripping off the
 @{text "fv_atom_list as"} & @{text "="} & @{text "atoms (set as)"}\\
 \end{tabular}
 \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"}
+Given the raw types @{text "ty\<^isub>1 \<dots> ty\<^isub>n"} we define now the
-we define now free-variable functions
+free-variable functions
 \begin{center}
 @{text "fv_ty\<^isub>1, \<dots>, fv_ty\<^isub>n"}
 \end{center}
 While the idea behind these free-variable 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, the function @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be
+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 below for each binding
+the union of the values, @{text v}, calculated by the rules for empty, shallow and
-clause.
+deep binding clauses:
+%
 \begin{equation}\label{deepbinder}
 \mbox{%
 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-\multicolumn{2}{@ {}l}{Empty binding clauses of the form
+\multicolumn{2}{@ {}l}{\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\
-\isacommand{bind\_set}~@{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"}:}\\
+\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> fv_ty\<^isub>m y\<^isub>m) - (x\<^isub>1 \<union> \<dots> \<union> x\<^isub>n)"}
+$\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m)"}\\
-provided the @{text "y\<^isub>i"} are of type @{text "ty\<^isub>i"}\smallskip\\
+& \hspace{10mm}@{text "- (fv_aty\<^isub>1 x\<^isub>1 \<union> .. \<union> fv_aty\<^isub>n x\<^isub>n)"}\\
-\multicolumn{2}{@ {}l}{Deep binders of the form
+& provided the bodies @{text "y"}$_{1..m}$ are of type @{text "ty"}$_{1..m}$ and the
-\isacommand{bind\_set}~@{text "bn x"}~\isacommand{in}~@{text "y\<^isub>1\<dots>y\<^isub>m"}:}\\
+binders @{text "x"}$_{1..n}$ of atomic types @{text "aty"}$_{1..n}$\smallskip\\
-$\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 "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
 \end{tabular}}
 \end{equation}
 \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
+function @{text "bn"}. For this we define the function @{text "fv_bn"}. Assume
-for the constructor @{text "C"} the binding function equation is of the form @{text
+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
+\multicolumn{2}{@ {}l}{\isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\
-\isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\
+$\bullet$ & @{term "v = fv_ty y"} provided @{text "y"} does not occur in @{text "rhs"}
-$\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"}\\
-and the free-variable function for the type of @{text "y"} is @{text "fv_ty\<^isub>i"}\\
+$\bullet$ & @{term "v = fv_bn y"} provided @{text "y"} occurs in  @{text "rhs"}
-$\bullet$ & @{term "v = fv_bn\<^isub>i y"} provided @{text "y"} occurs in  @{text "rhs"}
+with a recursive call @{text "bn y"}\\
-with a recursive call @{text "bn\<^isub>i y"}\\
 $\bullet$ & @{term "v = {}"} provided @{text "y"} occurs in  @{text "rhs"},
 but without a recursive call\\
 \end{tabular}}
 \end{equation}
 we have to know that the permutation operations are respectful
 w.r.t.~alpha-equivalence. This amounts to showing that the
 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}
 \noindent
 for our infrastructure. In a similar fashion we can lift the equations

changeset 1956	028705c98304
parent 1954	23480003f9c5
child 1957	47430fe78912