nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:e90f6a26d74b
+:a908ea36054f
 section {* Introduction *}
 text {*
 %%%  @{text "(1, (2, 3))"}
-So far, Nominal Isabelle provides a mechanism for constructing
+So far, Nominal Isabelle provided a mechanism for constructing
 $\alpha$-equated terms, for example lambda-terms
 \begin{center}
 @{text "t ::= x | t t | \<lambda>x. t"}
 \end{center}
 proofs, we establish a reasoning infrastructure for $\alpha$-equated
 terms, including properties about support, freshness and equality
 conditions for $\alpha$-equated terms. We are also able to derive strong
 induction principles that have the variable convention already built in.
 The method behind our specification of general binders is taken
-from the Ott-tool, but we introduce restrictions, and also one extension, so
+from the Ott-tool, but we introduce crucial restrictions, and also one extension, so
 that our specifications make sense for reasoning about $\alpha$-equated terms.
 \begin{figure}
 \begin{boxedminipage}{\linewidth}
 & @{text c} & coercion variables\\
 & @{text x} & term variables\\
 \end{tabular}
 \end{center}
 \end{boxedminipage}
-\caption{The term-language of System @{text "F\<^isub>C"}
+\caption{The System @{text "F\<^isub>C"}
 \cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this
-version of the term-language we made a modification by separating the
+version of @{text "F\<^isub>C"} we made a modification by separating the
 grammars for type kinds and coercion kinds, as well as for types and coercion
 types. For this paper the interesting term-constructor is @{text "\<CASE>"},
 which binds multiple type-, coercion- and term-variables.\label{corehas}}
 \end{figure}
 *}
 extensive use of these properties in order to define $\alpha$-equivalence in
 the presence of multiple binders.
 *}
-section {* General Binders\label{sec:binders} *}
+section {* General Bindings\label{sec:binders} *}
 text {*
 In Nominal Isabelle, the user is expected to write down a specification of a
 term-calculus and then a reasoning infrastructure is automatically derived
 from this specification (remember that Nominal Isabelle is a definitional
 \wedge     & @{term "(fv(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 for how these definitions
+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
 define
 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 the next section.
 *}
-section {* Specifying General Binders\label{sec:spec} *}
+section {* Specifying General Bindings\label{sec:spec} *}
 text {*
 Our choice of syntax for specifications is influenced by the existing
 datatype package of Isabelle/HOL \cite{Berghofer99} and by the syntax of the
 Ott-tool \cite{ott-jfp}. For us a specification of a term-calculus is a
 In these specifications @{text "name"} refers to an atom type, and @{text
 "fset"} to the type of finite sets.
 Note that for @{text lam} it does not matter which binding mode we use. The
 reason is that we bind only a single @{text name}. However, having
 \isacommand{bind\_set} or \isacommand{bind} in the second case makes a
-difference to the semantics of the specification (which we will define below).
+difference to the semantics of the specification (which we will define in the next section).
 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
 \noindent
 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 free-variable
-function and $\alpha$-equivalence relation, which we are going to define later.
+function and $\alpha$-equivalence relation.
 To make sure that variables bound by deep binders cannot be free at the
-same time, we cannot have more than one binding function for one binder.
+same time, we cannot have more than one binding function for one deep binder.
 Consequently we exclude specifications such as
 \begin{center}
 \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
 @{text "Baz\<^isub>1 p::pat t::trm"} &
 \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"}.
 We also need to restrict the form of the binding functions in order
-to ensure the @{text "bn"}-functions can be lifted defined for $\alpha$-equated
+to ensure the @{text "bn"}-functions can be defined for $\alpha$-equated
 terms. As a result we cannot return an atom in a binding function that is also
 bound in the corresponding term-constructor. That means in the example
 \eqref{letpat} that the term-constructors @{text PVar} and @{text PTup} may
 not have a binding clause (all arguments are used to define @{text "bn"}).
 In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons}
 may have a binding clause involving the argument @{text t} (the only one that
 is \emph{not} used in the definition of the binding function). This restriction
-means that we can lift the binding function to $\alpha$-equated terms.
+is sufficient for defining the binding function over $\alpha$-equated terms.
 In the version of
 Nominal Isabelle described here, we also adopted the restriction from the
 Ott-tool that binding functions can only return: the empty set or empty list
 (as in case @{text PNil}), a singleton set or singleton list containing an
 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
 raw datatype. We can also easily define permutation operations by
-recursion so that for each term constructor @{text "C"} with
+recursion so that for each term constructor @{text "C"} we have that
-arguments @{text "z"}$_{1..n}$ we have that
 %
 \begin{equation}\label{ceqvt}
 @{text "p \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (p \<bullet> z\<^isub>1) \<dots> (p \<bullet> z\<^isub>n)"}
 \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}$ of a specification,
+\emph{raw} types @{text "ty"}$_{1..n}$ extracted from  a specification,
 we define the free-variable functions
 %
 \begin{equation}\label{fvars}
 @{text "fv_ty\<^isub>1, \<dots>, fv_ty\<^isub>n"}
 \end{equation}
 \noindent
-We define them together with auxiliary free-variable functions for
+by recursion over the types @{text "ty"}$_{1..n}$.
+We define these functions together with auxiliary free-variable 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"}
 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
 collect all atoms that are not bound), because of our rather complicated
-binding mechanisms their definitions are somewhat involved. The functions
+binding mechanisms their definitions are somewhat involved.  Given
-are defined by recursion defining a clause for each term-constructor.  Given
 the 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)"}. Given the binding clause @{text
+"fv(bc\<^isub>1) \<union> \<dots> \<union> fv(bc\<^isub>k)"} where we define below what @{text "fv"} of a binding
-bc\<^isub>i} is of the form
+clause with mode \isacommand{bin\_set} means (similarly for the other modes).
+Suppose the binding clause @{text bc\<^isub>i} is of the form
 %
 \begin{equation}
 \mbox{\isacommand{bind\_set} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
 \end{equation}
 \noindent
 in which the body-labels @{text "d"}$_{1..q}$ refer to types @{text ty}$_{1..q}$,
 and the binders @{text b}$_{1..p}$
 either refer to labels of atom types (in case of shallow binders) or to binding
 functions taking a single label as argument (in case of deep binders). Assuming the
-set @{text "D"} stands for the free atoms in the bodies, @{text B} for the
+set @{text "D"} stands for the free atoms in the bodies, the set @{text B} for the
 binding atoms in the binders and @{text "B'"} for the free atoms in
 non-recursive deep binders,
 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'"}
 \end{center}
 \noindent
-The set @{text D} is defined as
+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"}
 \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 types
+(see \eqref{fvars}) provided the @{text "d\<^isub>i"} refers to one of the raw types
-@{text "ty"}$_{1..n}$; otherwise we set @{text "fv_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
+@{text "ty"}$_{1..n}$ from a specification; otherwise we set @{text "fv_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
-In order to define the set @{text B} we use the following auxiliary bn-functions
+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
 %
 \begin{center}
 \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-@{text "bn_atom a"} & @{text "="} & @{text "{atom a}"}\\
+@{text "bn_atom a"} & @{text "\<equiv>"} & @{text "{atom a}"}\\
-@{text "bn_atom_set as"} & @{text "="} & @{text "atoms as"}\\
+@{text "bn_atom_set as"} & @{text "\<equiv>"} & @{text "atoms as"}\\
-@{text "bn_atom_list as"} & @{text "="} & @{text "atoms (set as)"}
+@{text "bn_atom_list as"} & @{text "\<equiv>"} & @{text "atoms (set as)"}
 \end{tabular}
 \end{center}
 \noindent
-In these functions, @{text "atoms"}, like @{text "atom"}, coerces
+The function @{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}"}.
-The set @{text B} is then defined as
+The set @{text B} is then formally defined as
 %
 \begin{center}
 @{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> ... \<union> bn_ty\<^isub>p b\<^isub>p"}
 \end{center}
 @{text "bn\<^isub>1 a\<^isub>1, \<dots>, bn\<^isub>r a\<^isub>r"}
 \end{center}
 \noindent
 with none of the @{text "a"}$_{1..r}$ being among the bodies @{text
-"d"}$_{1..q}$. The set @{text "B'"} is then defined as
+"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"}
 \end{center}
 \noindent
-Similarly for the other binding modes.
+This completes the definition of the free-variable 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 has specified
+@{text "fv_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"}
 \end{center}
 \noindent
 where the @{text "z"}$_{1..n}$ are of types @{text "ty"}$_{1..n}$. For each of
-the arguments we calculate the free atoms as follows
+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"}\\
+$\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"}
-with the recursive call @{text "bn\<^isub>i z\<^isub>i"}\\
+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
 \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 "fv_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"} from the example shown in \eqref{letrecs}.
+@{text "Let"} and @{text "Let_rec"}, as well as @{text "ANil"} and @{text "ACons"}
-For them we consider three free-variable functions, namely
+from the example shown in \eqref{letrecs}.
-@{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"}:
+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:
 %
 \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 "fv\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
-@{text "fv\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "{atom a} \<union> (fv\<^bsub>trm\<^esub> t) \<union> (fv\<^bsub>assn\<^esub> as)"}\\[1mm]
+@{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 "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)"}
 \end{tabular}
 \end{center}
 \noindent
-Since there are only (implicit) empty binding clauses for the term-constructors @{text ANil}
+To see the ``pattern'', recall that @{text ANil} and @{text "ACons"} have no
-and @{text "ACons"}, the corresponding free-variable function @{text
+binding clause in the specification. The corresponding free-variable
-"fv\<^bsub>assn\<^esub>"} returns all atoms occurring in an assignment. The
+function @{text "fv\<^bsub>assn\<^esub>"} therefore returns all atoms
-binding only takes place in @{text Let} and @{text "Let_rec"}. In the @{text
+occurring in an assignment. The binding only takes place in @{text Let} and
-"Let"}-clause we want to bind all atoms given by @{text "set (bn as)"} in
+@{text "Let_rec"}. In the @{text "Let"}-clause, the binding clause specifies
-@{text t}. Therefore we have to subtract @{text "set (bn as)"} from @{text
+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
-free in @{text "as"}. This is what the purpose of the function @{text
+free in @{text "as"}.  In contrast, in @{text "Let_rec"} we have a recursive
-"fv\<^bsub>bn\<^esub>"} is.  In contrast, in @{text "Let_rec"} we have a
+binder where we want to also bind all occurrences of the atoms in @{text
-recursive binder where we want to also bind all occurrences of the atoms
+"set (bn as)"} also inside @{text "as"}. Therefore we have to subtract
-in @{text "set (bn as)"} inside @{text "as"}. Therefore we have to subtract @{text
+@{text "set (bn as)"} from the union @{text "fv\<^bsub>trm\<^esub> t"} and @{text "fv\<^bsub>assn\<^esub> as"}.
-"set (bn as)"} from @{text "fv\<^bsub>trm\<^esub> t"}, as well as from
-@{text "fv\<^bsub>assn\<^esub> as"}. An interesting point in this example is
+An interesting point in this
-that an assignment ``alone'' does not have any bound variables. Only in the
+example is that a ``naked'' assignment does not bind any
-context of a @{text Let} or @{text "Let_rec"} will some atoms become bound.
+atoms. Only in the context of a @{text Let} or @{text "Let_rec"} will
-This is a phenomenon
+some atoms from an assignment become bound.  This is a phenomenon that has also been pointed
-that has also been pointed out in \cite{ott-jfp}. For us it is crucial, because
+out in \cite{ott-jfp}. For us this observation is crucial, because we would
-we would not be able to lift a @{text "bn"}-function that is defined over
+not be able to lift the @{text "bn"}-function if it was defined over assignments
-arguments that are either binders or bodies. In that case @{text "bn"} would
+where some atoms are bound. In that case @{text "bn"} would \emph{not} respect
-not respect $\alpha$-equivalence. We can also see that
+$\alpha$-equivalence.
-%
-\begin{equation}\label{bnprop}
+Next we define $\alpha$-equivalence relations for the raw types @{text
-@{text "fv_ty x  =  bn x \<union> fv_bn x"}.
+"ty"}$_{1..n}$. We call them
-\end{equation}
+%
+\begin{center}
-\noindent
+@{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}.
-holds for any @{text "bn"}-function defined for the type @{text "ty"}.
+\end{center}
-TBD below.
+\noindent
+Like with the free-variable functions, we also need to
-Next we define $\alpha$-equivalence relations for the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}. We call them
+define auxiliary $\alpha$-equivalence relations
-@{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.
+\begin{center}
-Say we have binding functions @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, then we also define @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}.
+@{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}
-To simplify our definitions we will use the following abbreviations for
+\end{center}
-relations and free-variable acting on products.
+\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
 %
 \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"}\\
 \end{tabular}
 \end{center}
-The relations for $\alpha$-equivalence are inductively defined predicates, whose clauses have
+The relations for $\alpha$-equivalence are inductively defined
-conclusions of the form
+predicates, whose clauses have the form
 %
 \begin{center}
-\mbox{\infer{@{text "C x\<^isub>1 \<dots> x\<^isub>n  \<approx>ty  C y\<^isub>1 \<dots> y\<^isub>n"}}
+\mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>n  \<approx>ty  C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>n"}}
-{@{text "prems(bc\<^isub>1)"} & @{text "\<dots>"} & @{text "prems(bc\<^isub>p)"}}}
+{@{text "prems(bc\<^isub>1) \<and> \<dots> \<and> prems(bc\<^isub>k)"}}}
 \end{center}
 \noindent
-For what follows, let us assume @{text C} is of type @{text ty}.  The task
+assuming the term-constructor @{text C} is of type @{text ty} and has
+the binding clauses @{term "bc"}$_{1..k}$.  The task
 is to specify what the premises of these clauses are. Again for this we
 analyse the binding clauses and produce a corresponding premise.
 *}
 (*<*)
 consts alpha_ty ::'a
 fv_trm ("fv\<^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>")
 (*>*)
 text {*
+*TBD below *
 \begin{equation}\label{alpha}
 \mbox{%
 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
 \multicolumn{2}{@ {}l}{Empty binding clauses of the form
 \isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "x\<^isub>i"}:}\\
 *}
 section {* Conclusion *}
 text {*
+We can also see that
+%
+\begin{equation}\label{bnprop}
+@{text "fv_ty x  =  bn x \<union> fv_bn x"}.
+\end{equation}
+\noindent
+holds for any @{text "bn"}-function defined for the type @{text "ty"}.
+*}
+text {*
 We have presented an extension of Nominal Isabelle for deriving
 automatically a convenient reasoning infrastructure that can deal with
 general binders, that is term-constructors binding multiple variables at
 once. This extension has been tried out with the Core-Haskell
 term-calculus. For such general binders, we can also extend

changeset 2345	a908ea36054f
parent 2344	e90f6a26d74b
child 2346	4c5881455923