nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:9bbf2a1f9b3f
+:cfd3a7368543
 \end{tabular}
 \end{tabular}}
 \end{equation}
 \noindent
-Concrete permutations are built up from swappings, written as \mbox{@{text "(a
+Concrete permutations in Nominal Isabelle are built up from swappings,
-b)"}}, which are permutations that behave as follows:
+written as \mbox{@{text "(a b)"}}, which are permutations that behave
+as follows:
 %
 \begin{center}
 @{text "(a b) = \<lambda>c. if a = c then b else if b = c then a else c"}
 \end{center}
 \begin{property}\label{swapfreshfresh}
 @{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
 \end{property}
 While often the support of an object can be relatively easily
-described, for example\\[-6mm]
+described, for example for atoms, products, lists, function applications,
+booleans and permutations\\[-6mm]
 %
 \begin{eqnarray}
 @{term "supp a"} & = & @{term "{a}"}\\
 @{term "supp (x, y)"} & = & @{term "supp x \<union> supp y"}\\
 @{term "supp []"} & = & @{term "{}"}\\
 @{term "supp (x#xs)"} & = & @{term "supp x \<union> supp xs"}\\
-@{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp (f, x)"}\label{suppfun}\\
+@{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp f \<union> supp x"}\label{suppfun}\\
 @{term "supp b"} & = & @{term "{}"}\\
 @{term "supp p"} & = & @{term "{a. p \<bullet> a \<noteq> a}"}
 \end{eqnarray}
 \noindent
-in some cases it can be difficult to establish the support precisely, and
+in some cases it can be difficult to characterise the support precisely, and
-only give an approximation (see \eqref{suppfun} above). Reasoning about
+only an approximation can be established (see \eqref{suppfun} above). Reasoning about
-such approximations can be made precise with the notion \emph{supports}, defined
+such approximations can be simplified with the notion \emph{supports}, defined
 as follows:
 \begin{defn}
 A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}
 not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.
 \begin{equation}\label{equivariancedef}
 @{term "\<forall>p. p \<bullet> f = f"}
 \end{equation}
 \noindent or equivalently that a permutation applied to the application
-@{text "f x"} can be moved to the argument @{text x}. That means we have for
+@{text "f x"} can be moved to the argument @{text x}. That means for equivariant
-all permutations @{text p}
+functions @{text f} we have for all permutations @{text p}
 %
 \begin{equation}\label{equivariance}
 @{text "p \<bullet> f = f"} \;\;\;\textit{if and only if}\;\;\;
 @{text "p \<bullet> (f x) = f (p \<bullet> x)"}
 \end{equation}
 \noindent
 The idea behind the second property is that given a finite set @{text as}
 of binders (being bound, or fresh, in @{text x} is ensured by the
 assumption @{term "as \<sharp>* x"}), then there exists a permutation @{text p} such that
 the renamed binders @{term "p \<bullet> as"} avoid @{text c} (which can be arbitrarily chosen
-as long as it is finitely supported) and also it does not affect anything
+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 also
+All properties given in this section are formalised in Isabelle/HOL and
 most of proofs are described in \cite{HuffmanUrban10} to which we refer the
 reader. In the next sections we will make extensively use of these
 properties in order to define alpha-equivalence in the presence of multiple
 binders.
 *}
 %\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 a type- and term-constructors
+In the rest of this section we are going to introduce three abstraction
-for abstraction. For this we define
+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}
 @{term "Abs_lst as x"} \hspace{5mm}
 @{term "Abs_res as x"}
 \end{center}
 \noindent
-indicating that a set or list @{text as} is abstracted in @{text x}. We will
+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 know is what the
+\emph{abstractions}. The important property we need to derive is what the
 support of abstractions is, namely:
 \begin{thm}[Support of Abstractions]\label{suppabs}
 Assuming @{text x} has finite support, then\\[-6mm]
 \begin{center}
 \end{center}
 \end{thm}
 \noindent
 Below we will show the first equation. The others
-follow similar arguments. By definition of the abstraction type @{text "abs_set"}
+follow by similar arguments. By definition of the abstraction type @{text "abs_set"}
 we have
 %
 \begin{equation}\label{abseqiff}
 @{thm (lhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\;
 @{thm (rhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}
 \begin{lemma}
 @{thm[mode=IfThen] abs_swap1(1)[where bs="as", no_vars]}
 \end{lemma}
 \begin{proof}
-This lemma is straightforward by using \eqref{abseqiff} and observing that
+This lemma is straightforward using \eqref{abseqiff} and observing that
 the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.
-Moreover @{text supp} and set difference are equivariant \cite{HuffmanUrban10}.
+Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}).
 \end{proof}
 \noindent
 This lemma allows us to show
 %
 \noindent
 since for finite sets, @{text "S"}, we have @{thm (concl) supp_finite_atom_set[no_vars]}.
 Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes of
-Theorem~\ref{suppabs}. This theorem gives us confidence that our
+Theorem~\ref{suppabs}. The method of first considering abstractions of the
-abstractions behave as one expects. To consider first abstractions of the
+form @{term "Abs as x"} etc is motivated by the fact that properties about them
-form @{term "Abs as x"} is motivated by the fact that properties about them
+can be conveninetly established at the Isabelle/HOL level.  It would be
-can be conveninetly established at the Isabelle/HOL level.  But we can also
+difficult to write custom ML-code that derives automatically such properties
-use when we deal with binding in our term-calculi specifications.
+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.
 *}
 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 in the collection
+whereby some of the @{text ty}$'_{1..l}$ (or their components) are contained
-of @{text ty}$^\alpha_{1..n}$ declared in \eqref{scheme}. In this case we will call the
+in the collection of @{text ty}$^\alpha_{1..n}$ declared in
-corresponding argument a \emph{recursive argument} of @{text "C\<^sup>\<alpha>"}.  The labels annotated on
+\eqref{scheme}. In this case we will call the corresponding argument a
-the types are optional. Their purpose is to be used in the (possibly empty) list of
+\emph{recursive argument} of @{text "C\<^sup>\<alpha>"}. There are ``positivity''
-\emph{binding clauses}, which indicate the binders and their scope
+restrictions imposed in the type of such recursive arguments, which ensure
-in a term-constructor.  They come in three \emph{modes}:
+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}
 \begin{tabular}{l}
 \isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it label}\\
 \isacommand{bind\_set}\; {\it binders}\; \isacommand{in}\; {\it label}\\
 \isacommand{bind\_res}\; {\it binders}\; \isacommand{in}\; {\it label}\\
 \end{tabular}
 \end{center}
 \noindent
-The first mode is for binding lists of atoms (the order of binders matters); the second is for sets
+The first mode is for binding lists of atoms (the order of binders matters);
-of binders (the order does not matter, but the cardinality does) and the last is for
+the second is for sets of binders (the order does not matter, but the
-sets of binders (with vacuous binders preserving alpha-equivalence).
+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
+``\isacommand{bind}-part'' will be the \emph{binder} of the binding clause.
 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
 \end{tabular}
 \end{center}
 \noindent
-In the first case we bind all atoms from the pattern @{text p} in @{text t}
+In the first case we might bind all atoms from the pattern @{text p} in @{text t}
 and also all atoms from @{text q} in @{text t}. As a result 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
 the general binders described in Section \ref{sec:binders}. However
 \end{tabular}}
 \end{equation}
 \noindent
 The difference is that with @{text Let} we only want to bind the atoms @{text
-"bn(a)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms
+"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.
 Having dealt with all syntax matters, the problem now is how we can turn
 The datatype definition can be obtained by stripping off the
 binding clauses and the labels on the types. We also have to invent
 new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}
-given by user. In our implementation we just use the affix @{text "_raw"}.
+given by user. In our implementation we just use the affix ``@{text "_raw"}''.
 But for the purpose of this paper, we just use the superscript @{text "_\<^sup>\<alpha>"} to indicate
 that a notion is defined over alpha-equivalence classes and leave it out
 for the corresponding notion defined on the ``raw'' level. So for example
 we have
 \begin{center}
 @{text "ty\<^sup>\<alpha> \<mapsto> ty"} \hspace{2mm}and\hspace{2mm} @{text "C\<^sup>\<alpha> \<mapsto> C"}
 \end{center}
 \noindent
-where the type @{term ty} is the type used in the quotient construction for
+where @{term ty} is the type used in the quotient construction for
 @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor on the ``raw'' type @{text "ty"}.
 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, called @{term "bn_ty"}, by primitive recursion over the corresponding
+functions, called @{term "bn"}, by primitive recursion over the corresponding
-raw datatype @{text ty}. We can also easily define permutation operations by
+raw datatype. We can also easily define permutation operations by
 primitive recursion so that for each term constructor @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}
 we have that
 \begin{center}
 @{text "p \<bullet> (C x\<^isub>1 \<dots> x\<^isub>n) = C (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}
 \end{center}
 \noindent
 We define them together with auxiliary free-variable functions for
 the binding functions. Given binding functions
-@{text "bn_ty\<^isub>1 \<dots> bn_ty\<^isub>m"} we need to define
+@{text "bn\<^isub>1 \<dots> bn\<^isub>m"} we need to define
 %
 \begin{center}
-@{text "fv_bn_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set  \<dots>  fv_bn_ty\<^isub>m :: ty\<^isub>m \<Rightarrow> atom set"}
+@{text "fv_bn\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set  \<dots>  fv_bn\<^isub>m :: ty\<^isub>m \<Rightarrow> atom set"}
 \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. While the idea behind these
+bound, as we shall see in an example below. We need therefore the function
+that returns us 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.
 First we deal with the case that @{text "x\<^isub>i"} is a binder. From the binding clauses,
 non-recursive binder.
 \begin{center}
 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
 $\bullet$ & @{term "{}"} provided @{text "x\<^isub>i"} is a shallow binder\\
-$\bullet$ & @{text "fv_bn_ty\<^isub>i x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep
+$\bullet$ & @{text "fv_bn x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep
-non-recursive binder with the auxiliary function @{text "bn_ty\<^isub>i"}\\
+non-recursive binder with the auxiliary binding function @{text "bn"}\\
-$\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i - bn_ty\<^isub>i x\<^isub>i"} provided @{text "x\<^isub>i"} is
+$\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i - bn x\<^isub>i"} provided @{text "x\<^isub>i"} is
-a deep recursive binder with the auxiliary function @{text "bn_ty\<^isub>i"}
+a deep recursive binder with the auxiliary binding function @{text "bn"}
 \end{tabular}
 \end{center}
 \noindent
 The first clause states that shallow binders do not contribute to the
 free variables; in the second clause, we have to collect all
-variables that are left unbound by the binding function @{text "bn_ty\<^isub>i"}---this
+variables that are left unbound by the binding function @{text "bn"}---this
-is done with function @{text "fv_bn_ty\<^isub>i"}; in the third clause, since the
+is done with function @{text "fv_bn"}; in the third clause, since the
 binder is recursive, we need to bind all variables specified by
-@{text "bn_ty\<^isub>i"}---therefore we subtract @{text "bn_ty\<^isub>i x\<^isub>i"} from the free
+@{text "bn"}---therefore we subtract @{text "bn x\<^isub>i"} from the free
 variables of @{text "x\<^isub>i"}.
 In case the argument is \emph{not} a binder, we need to consider
 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:
 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_ty\<^isub>i"} for
+Next, we need to define a free-variable function @{text "fv_bn\<^isub>j"} for
-each binding function @{text "bn_ty\<^isub>i"}. The idea behind this
+each binding function @{text "bn\<^isub>j"}. The idea behind this
 function is to compute the set of free atoms that are not bound by
-@{text "bn_ty\<^isub>i"}. Because of the restrictions we imposed on the
+@{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
-@{text "bn_ty\<^isub>i (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then @{text "fv_bn_ty\<^isub>i"} is the
+@{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>j"} of type @{text "ty\<^isub>j"}
+union of the values calculated for @{text "x\<^isub>i"} of type @{text "ty\<^isub>i"}
 as follows:
 \begin{center}
 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-\multicolumn{2}{l}{@{text "x\<^isub>j"} occurs in @{text "rhs"}:}\\
+\multicolumn{2}{l}{@{text "x\<^isub>i"} occurs in @{text "rhs"}:}\\
-$\bullet$ & @{term "{}"} provided @{term "x\<^isub>j"} is a single atom,
+$\bullet$ & @{term "{}"} provided @{term "x\<^isub>i"} is a single atom,
 atom list or atom set\\
-$\bullet$ & @{text "fv_bn_ty\<^isub>j x\<^isub>j"} in case @{text "rhs"} contains the
+$\bullet$ & @{text "fv_bn x\<^isub>i"} in case @{text "rhs"} contains the
-recursive call @{text "bn_ty\<^isub>j x\<^isub>j"}\\[1mm]
+recursive call @{text "bn x\<^isub>i"}\\[1mm]
 %
-\multicolumn{2}{l}{@{text "x\<^isub>j"} does not occur in @{text "rhs"}:}\\
+\multicolumn{2}{l}{@{text "x\<^isub>i"} does not occur in @{text "rhs"}:}\\
-$\bullet$ & @{text "atoms x\<^isub>j"} provided @{term "x\<^isub>j"} is a set of atoms\\
+$\bullet$ & @{text "atoms x\<^isub>i"} provided @{term "x\<^isub>i"} is a set of atoms\\
-$\bullet$ & @{term "atoms (set x\<^isub>j)"} provided @{term "x\<^isub>j"} is a list of atoms\\
+$\bullet$ & @{term "atoms (set x\<^isub>i)"} provided @{term "x\<^isub>i"} is a list of atoms\\
-$\bullet$ & @{text "fv_ty\<^isub>j x\<^isub>j"} provided @{term "ty\<^isub>j"} is one of the raw
+$\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i"} provided @{term "ty\<^isub>i"} is one of the raw
 types corresponding to the types specified by the user\\
-%  $\bullet$ & @{text "fv_ty\<^isup>\<alpha> x\<^isub>j - bnds"} provided @{term "x\<^isub>j"}  is not in @{text "rhs"}
+%  $\bullet$ & @{text "fv_ty\<^isup>\<alpha> x\<^isub>i - bnds"} provided @{term "x\<^isub>i"}  is not in @{text "rhs"}
 %     and is an existing nominal datatype with the free-variable function @{text "fv\<^isup>\<alpha>"}\\
 $\bullet$ & @{term "{}"} otherwise
 \end{tabular}
 \end{center}
 section {* Adequacy *}
 section {* Related Work *}
 text {*
-The earliest usage we know of general binders in a theorem prover setting is
+To our knowledge the earliest usage of general binders in a theorem prover setting is
 in the paper \cite{NaraschewskiNipkow99}, which describes a formalisation of
 the algorithm W. This formalisation implements binding in type schemes using a
 a de-Bruijn indices representation. Also recently an extension for general binders
 has been proposed for the locally nameless approach to binding \cite{chargueraud09}. .
 But we have not yet seen it to be employed in a non-trivial formal verification.

changeset 1730	cfd3a7368543
parent 1728	9bbf2a1f9b3f
child 1732	6eaae2651292