nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:ba66fa116e05
+:8b6a285ad480
 as long as it is finitely supported) and also @{text "p"} does not affect anything
 in the support of @{text x} (that is @{term "supp x \<sharp>* p"}). The last
 fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders
 @{text as} in @{text x}, because @{term "p \<bullet> x = x"}.
-All properties given in this section are formalised in Isabelle/HOL and
+Most properties given in this section are described in \cite{HuffmanUrban10}
-most of proofs are described in \cite{HuffmanUrban10} to which we refer the
+and of course all are formalised in Isabelle/HOL. In the next sections we will make
-reader. In the next sections we will make extensively use of these
+extensively use of these properties in order to define alpha-equivalence in
-properties in order to define alpha-equivalence in the presence of multiple
+the presence of multiple binders.
-binders.
 *}
 section {* General Binders\label{sec:binders} *}
 \end{center}
 \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 is what the
+\emph{abstractions}. The important property we need to derive the support of
-support of abstractions is, namely:
+abstractions, namely:
 \begin{thm}[Support of Abstractions]\label{suppabs}
 Assuming @{text x} has finite support, then\\[-6mm]
 \begin{center}
 \begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
 \noindent
 which by Property~\ref{supportsprop} gives us ``one half'' of
 Thm~\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 taking an abstraction as argument:
+function @{text aux}, taking an abstraction as argument:
 %
 \begin{center}
 @{thm supp_gen.simps[THEN eq_reflection, no_vars]}
 \end{center}
 \begin{equation}\label{halftwo}
 @{thm (concl) supp_abs_subset1(1)[no_vars]}
 \end{equation}
 \noindent
-since for finite sets, @{text "S"}, we have @{thm (concl) supp_finite_atom_set[no_vars]}.
+since for finite sets of atoms, @{text "bs"}, we have
+@{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
-Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes of
+Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes
-Theorem~\ref{suppabs}. The method of first considering abstractions of the
+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
 for every term-constructor that binds some atoms. Also the generality of
-the definitions for alpha-equivalence will also help us 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 {*
 \begin{center}
 @{text "C\<^sup>\<alpha> label\<^isub>1::ty"}$'_1$ @{text "\<dots> label\<^isub>l::ty"}$'_l\;\;$  @{text "binding_clauses"}
 \end{center}
 \noindent
-whereby some of the @{text ty}$'_{1..l}$ (or their components) are contained
+whereby some of the @{text ty}$'_{1..l}$ (or their components) might be contained
 in the collection of @{text ty}$^\alpha_{1..n}$ declared in
-\eqref{scheme}. In this case we will call the corresponding argument a
+\eqref{scheme}.
-\emph{recursive argument} of @{text "C\<^sup>\<alpha>"}. There are ``positivity''
+%In this case we will call the corresponding argument a
-restrictions imposed in the type of such recursive arguments, which ensure
+%\emph{recursive argument} of @{text "C\<^sup>\<alpha>"}. The types of such recursive
-that the type has a set-theoretic semantics \cite{Berghofer99}.  The labels
+%arguments need to satisfy a  ``positivity''
+%restriction, which ensures that the type has a set-theoretic semantics
+%\cite{Berghofer99}.
+The labels
 annotated on the types are optional. Their purpose is to be used in the
 (possibly empty) list of \emph{binding clauses}, which indicate the binders
 and their scope in a term-constructor.  They come in three \emph{modes}:
 \begin{center}
 \noindent
 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 the \emph{body} of the abstraction; the
+clause will be called the \emph{body}; the
-``\isacommand{bind}-part'' will be the \emph{binder} of the binding clause.
+``\isacommand{bind}-part'' will be the \emph{binder}.
 In addition we distinguish between \emph{shallow} and \emph{deep}
 binders.  Shallow binders are of the form \isacommand{bind}\; {\it label}\;
 \isacommand{in}\; {\it label'} (similar for the other two modes). The
 restriction we impose on shallow binders is that the {\it label} must either
 call such binders \emph{recursive}, see below).
 The corresponding binding functions are expected to return either a set of atoms
 (for \isacommand{bind\_set} and \isacommand{bind\_res}) or a list of atoms
 (for \isacommand{bind}). They can be defined by primitive recursion over the
 corresponding type; the equations must be given in the binding function part of
-the scheme shown in \eqref{scheme}. For example a term-calculus containing lets
+the scheme shown in \eqref{scheme}. For example a term-calculus containing @{text "Let"}s
 with tuple patterns might be specified as:
 \begin{center}
 \begin{tabular}{l}
 \isacommand{nominal\_datatype} @{text trm} =\\
 \noindent
 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}.
-To see the purpose for such recursive binders, compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s:
+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{%
 \begin{tabular}{@ {}l@ {}}
 \isacommand{nominal\_datatype}~@{text "trm ="}\\
 \end{center}
 \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
-that returns us those unbound atoms.
+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
 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
 @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be the union of the values
-calculated next for each argument.
+calculated below for each argument.
 First we deal with the case that @{text "x\<^isub>i"} is a binder. From the binding clauses,
 we can determine whether the argument is a shallow or deep
 binder, and in the latter case also whether it is a recursive or
 non-recursive binder.
 whether the @{text "x\<^isub>i"} is the body of one or more binding clauses.
 In this case we first calculate the set @{text "bnds"} as follows:
 either the corresponding binders are all shallow or there is a single deep binder.
 In the former case we take @{text bnds} to be the union of all shallow
 binders; in the latter case, we just take the set of atoms specified by the
-binding function. The value for @{text "x\<^isub>i"} is then given by:
+corrsponding binding function. The value for @{text "x\<^isub>i"} is then given by:
+%
 \begin{equation}\label{deepbody}
 \mbox{%
 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
 $\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\
 $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\
 $\bullet$ & @{term "{}"} otherwise
 \end{tabular}}
 \end{equation}
 \noindent
-Like the coercion function @{text atom} used above, @{text "atoms as"} coerces
+Like the coercion function @{text atom} used earlier, @{text "atoms as"} coerces
 the set @{text as} to the generic atom type.
-It is defined as @{text "atom as \<equiv> {atom a | a \<in> as}"}.
+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
 a binder nor a body of an abstraction. In this case it is defined
 as in \eqref{deepbody}, except that we do not need to subtract the
 set @{text bnds}.
 Next, we need to define a free-variable function @{text "fv_bn\<^isub>j"} for
-each binding function @{text "bn\<^isub>j"}. The idea behind this
+each binding function @{text "bn\<^isub>j"}. The idea behind these
-function is to compute the set of free atoms that are not bound by
+functions is to compute the set of free atoms that are not bound by
 @{text "bn\<^isub>j"}. Because of the restrictions we imposed on the
 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 the binding function is
+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:
 \begin{center}
 \multicolumn{2}{l}{@{text "x\<^isub>i"} occurs in @{text "rhs"}:}\\
 $\bullet$ & @{term "{}"} provided @{term "x\<^isub>i"} is a single atom,
 atom list or atom set\\
 $\bullet$ & @{text "fv_bn x\<^isub>i"} in case @{text "rhs"} contains the
 recursive call @{text "bn x\<^isub>i"}\medskip\\
-%
+\end{tabular}
+\end{center}
+\begin{center}
+\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
 \multicolumn{2}{l}{@{text "x\<^isub>i"} does not occur in @{text "rhs"}:}\\
 $\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
 \end{tabular}
 \end{center}
 \noindent
 To see how these definitions work in practise, let us reconsider the term-constructors
-@{text "Let"} and @{text "Let_rec"} from example shown in \eqref{letrecs}.
+@{text "Let"} and @{text "Let_rec"} from the example shown in \eqref{letrecs}.
-For this specification we need to define three functions, namely
+For this specification we need to define three free-variable functions, namely
 @{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"}. They are 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>bn\<^esub> as \<union> (fv\<^bsub>trm\<^esub> t - set (bn as))"}\\
 recursive binder where we want to also bind all occurences of the atoms
 @{text "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
-context of a @{text Let} or @{text "Let_rec"} will some atoms become bound
+context of a @{text Let} or @{text "Let_rec"} will some atoms become bound.
-(the term-constructors that have binding clauses).  This is a phenomenon
+This is a phenomenon
 that has also been pointed out in \cite{ott-jfp}. We can also see that
-given a @{text "bn"}-function for a type @{text "ty"}, then we have
+given a @{text "bn"}-function for a type @{text "ty"}, we have that
 %
 \begin{equation}\label{bnprop}
 @{text "fv_ty x = bn x \<union> fv_bn x"}.
 \end{equation}
 Next we define alpha-equivalence for the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}. We call them
 @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}. Like with the free-variable functions,
 we also need to  define auxiliary alpha-equivalence relations for the binding functions.
-Say we have @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, we also define @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>b\<^isub>m"}.
+Say we have @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, then we also define @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>b\<^isub>m"}.
 To simplify our definitions we will use the following abbreviations for
 relations and free-variable acting on products.
 %
 \begin{center}
-\begin{tabular}{rcl}
+\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"}\\
 \end{tabular}
 \end{center}
 The relations for alpha-equivalence are inductively defined predicates, whose clauses have
-conclusions of the form  @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"} (let us assume
+conclusions of the form
+%
+\begin{center}
+@{text "C x\<^isub>1 \<dots> x\<^isub>n  \<approx>ty  C y\<^isub>1 \<dots> y\<^isub>n"}
+\end{center}
+\noindent
+For what follows, let us assume
 @{text C} is of type @{text ty} and its arguments are given by @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}).
 The task now is to specify what the premises of these clauses are. For this we
-consider the pairs @{text "(x\<^isub>i, y\<^isub>i)"}. We will analyse these pairs according to
+consider the pairs \mbox{@{text "(x\<^isub>i, y\<^isub>i)"}}, but instead of considering them in turn, it will
-``clusters'' of the binding clauses. There are the following cases:
+be easier to analyse these pairs according to  ``clusters'' of the binding clauses.
+Therefore we distinguish the following cases:
 *}
 (*<*)
 consts alpha_ty ::'a
 notation alpha_ty ("\<approx>ty")
 (*>*)
 text {*
 \begin{itemize}
 \item The @{text "(x\<^isub>i, y\<^isub>i)"} are bodies of shallow binders with type @{text "ty"}. We assume the
-@{text "(u\<^isub>1, v\<^isub>1),\<dots>,(u\<^isub>m, v\<^isub>m)"} are the corresponding binders. For the binding mode
+\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)"}
 \end{center}
-Similarly for the other modes.
+For the binding mode \isacommand{bind} we use $\approx_{\textit{list}}$, and for
+binding mode \isacommand{bind\_res} we use $\approx_{\textit{res}}$.
 \item The @{text "(x\<^isub>i, y\<^isub>i)"} are deep non-recursive binders with type @{text "ty"}
-and with @{text bn} being the auxiliary binding function. We assume
+and @{text bn} being the auxiliary binding function. We assume
 @{text "(u\<^isub>1, v\<^isub>1),\<dots>,(u\<^isub>m, v\<^isub>m)"} are the corresponding bodies with types @{text "ty\<^isub>1,\<dots>, ty\<^isub>m"}.
-For the binding mode \isacommand{bind\_set} we generate the two premises
+For the binding mode \isacommand{bind\_set} we generate two premises
+%
 \begin{center}
-@{text "x\<^isub>i \<approx>bn y\<^isub>i"}\\
+@{text "x\<^isub>i \<approx>bn y\<^isub>i"}\hfill
 @{term "\<exists>p. (bn x\<^isub>i, (u\<^isub>1,\<xi>,u\<^isub>m)) \<approx>gen R fv p (bn y\<^isub>i, (v\<^isub>1,\<xi>,v\<^isub>m))"}
 \end{center}
 \noindent
 where @{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"}. Similarly for the other modes.
+@{text "fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}. Similarly for the other binding modes.
 \item The @{text "(x\<^isub>i, y\<^isub>i)"} are deep recursive binders with type @{text "ty"}
 and with @{text bn} being the auxiliary binding function. We assume
 @{text "(u\<^isub>1, v\<^isub>1),\<dots>,(u\<^isub>m, v\<^isub>m)"} are the corresponding bodies with types @{text "ty\<^isub>1,\<dots>, ty\<^isub>m"}.
 For the binding mode \isacommand{bind\_set} we generate the premise
+%
 \begin{center}
 @{term "\<exists>p. (bn x\<^isub>i, (x\<^isub>i, u\<^isub>1,\<xi>,u\<^isub>m)) \<approx>gen R fv p (bn y\<^isub>i, (y\<^isub>i, v\<^isub>1,\<xi>,v\<^isub>m))"}
 \end{center}
 \noindent
 where @{text R} is @{text "\<approx>ty \<otimes> \<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fv} is
 @{text "fv_ty \<oplus> fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}. Similarly for the other modes.
 \end{itemize}
 \noindent
-The only cases that are not covered by these rules is if @{text "(x\<^isub>i, y\<^isub>i)"} is
+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
+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
 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 @{text "x\<^isub>i = y\<^isub>i"}.
+then we generate just @{text "x\<^isub>i = y\<^isub>i"}.
 TODO
 The alpha-equivalence relations for binding functions are similar to the alpha-equivalences
 for their respective types, the difference is that they ommit checking the arguments that

changeset 1737	8b6a285ad480
parent 1736	ba66fa116e05
child 1739	468c3c1adcba