nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:47e2e91705f3
+:774d631726ad
 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}.
 In contrast to Ott, we allow multiple labels in binders and bodies. For example
-we permit binding clauses as follows:
+we have binding clauses of the form:
 \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
+Similarly for the other binding modes.
 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
+\emph{one} binding clause of a term constructor.
-occur in several binding clauses, but cannot occur as a body.
+For binders we distinguish between \emph{shallow} and \emph{deep} binders.
-In addition we distinguish between \emph{shallow} and \emph{deep}
+Shallow binders are of the form \isacommand{bind}\; {\it labels}\;
-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
+restriction we impose on shallow binders is that in case of
-refer to atom types or to finite sets or
+\isacommand{bind\_set} and \isacommand{bind\_res} the {\it labels} must
-lists of atom types. Two examples for the use of shallow binders are the
+either refer to atom types or to sets of atom types; in case of
-specification of lambda-terms, where a single name is bound, and
+\isacommand{bind} we allow labels to atom types or lists of atom types. Two
-type-schemes, where a finite set of names is bound:
+examples for the use of shallow binders are the specification of
+lambda-terms, where a single name is bound, and type-schemes, where a finite
+set of names is bound:
 \begin{center}
 \begin{tabular}{@ {}cc@ {}}
 \begin{tabular}{@ {}l@ {\hspace{-1mm}}}
 \isacommand{nominal\_datatype} @{text lam} =\\
 \end{tabular}
 \end{center}
 \noindent
 Note that in this specification @{text "name"} refers to an atom type, and
-@{text "fset"} to the type of finite sets.
+@{text "fset"} to the type of finite sets. Shallow binders can occur in the
+binding part of several binding clauses.
 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).
 In this specification the function @{text "bn"} determines which atoms of @{text  p} are
 bound in the argument @{text "t"}. Note that in the second-last clause the function @{text "atom"}
 coerces a name into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}. This allows
 us to treat binders of different atom type uniformly.
-As will shortly become clear, we cannot return an atom in a binding function
-that is also bound in the corresponding term-constructor. That means in the
-example above that the term-constructors @{text PVar} and @{text PTup} may not have a
-binding clause.  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 atom (case @{text PVar}), or unions of atom sets or appended atom
-lists (case @{text PTup}). This restriction will simplify definitions and
-proofs later on.
 The most drastic restriction we have to impose on deep binders is that
 we cannot have ``overlapping'' deep binders. Consider for example the
 term-constructors:
 \begin{center}
 \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p t"}\\
 \end{tabular}
 \end{center}
 \noindent
-since there is no overlap of binders.
+since there is no overlap of binders. Unlike shallow binders, we restrict deep
+binders to occur in only one binding clause. Therefore @{text "Bar\<^isub>2"} cannot
-Note that in the last example we wrote \isacommand{bind}~@{text
+be reformulated as
-"bn(p)"}~\isacommand{in}~@{text "p.."}.  Whenever such a binding clause is
-present, we will call the corresponding binder \emph{recursive}.  To see the
+\begin{center}
+\begin{tabular}{ll}
+@{text "Bar\<^isub>3 p::pat t::trm"} &
+\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p"},
+\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "t"}\\
+\end{tabular}
+\end{center}
+Note that in the @{text "Bar\<^isub>2"}, we wrote \isacommand{bind}~@{text
+"bn(p)"}~\isacommand{in}~@{text "p.."}.  Whenever such a binding clause
+is present, where the argument in the binder also occurs in the body, we will
+call the corresponding binder \emph{recursive}.  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{%
 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 describe in the
 rest of this section.
-In order to simplify some definitions, we shall assume specifications
+We also need to restrict the form of the binding functions. As will shortly
+become clear, 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 binding clause involving the argument @{text t} (the only one that
+is \emph{not} used in the definition of the binding function).  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
+atom (case @{text PVar}), or unions of atom sets or appended atom lists
+(case @{text PTup}). This restriction will simplify some automatic proofs
+later on.
+In order to simplify some later 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 "label"}. In case
 of the lambda-calculus, the completion produces
 \end{tabular}
 \end{center}
 \noindent
 The point of completion is that we can make definitions over the binding
-clauses and be sure to capture all arguments of a term constructor.
+clauses and be sure to have captured 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}, just
 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{equation}\label{ceqvt}
-@{text "p \<bullet> (C x\<^isub>1 \<dots> x\<^isub>n) = C (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}
+@{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 free-variable
 functions from the specifications. For atomic types we define the auxilary
 free variable functions:
 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 @{text bcs}, the result of the @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be
+clauses @{text bcs}, the result of the @{text "fv_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be
 the union of the values, @{text v}, calculated by the rules for empty, shallow and
 deep binding clauses:
 %
-\begin{equation}\label{deepbinder}
+\begin{equation}\label{deepbinderA}
 \mbox{%
 \begin{tabular}{c@ {\hspace{2mm}}p{7.4cm}}
 \multicolumn{2}{@ {}l}{\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\
 $\bullet$ & @{term "v = fv_ty y"} provided @{text "y"} is of type @{text "ty"}\smallskip\\
+%
 \multicolumn{2}{@ {}l}{\isacommand{bind}~@{text "x\<^isub>1\<dots>x\<^isub>n"}~\isacommand{in}~@{text "y\<^isub>1\<dots>y\<^isub>m"}:}\\
-$\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> \<dots> \<union> fv_ty\<^isub>m y\<^isub>m)"}\\
+$\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m)"}\\
-& \hspace{15mm}@{text "- (fv_aty\<^isub>1 x\<^isub>1 \<union> \<dots> \<union> fv_aty\<^isub>n x\<^isub>n)"}\\
+& \hspace{15mm}@{text "- (fv_aty\<^isub>1 x\<^isub>1 \<union> .. \<union> fv_aty\<^isub>n x\<^isub>n)"}\\
 & provided the bodies @{text "y"}$_{1..m}$ are of type @{text "ty"}$_{1..m}$ and the
 binders @{text "x"}$_{1..n}$ of atomic types @{text "aty"}$_{1..n}$\smallskip\\
+\end{tabular}}
+\end{equation}
+\begin{equation}\label{deepbinderB}
+\mbox{%
+\begin{tabular}{c@ {\hspace{2mm}}p{7.4cm}}
 \multicolumn{2}{@ {}l}{\isacommand{bind}~@{text "bn x"}~\isacommand{in}~@{text "y\<^isub>1\<dots>y\<^isub>m"}:}\\
-$\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> \<dots> \<union> fv_ty\<^isub>m y\<^isub>m) - set (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) - set (bn x) \<union> (fv_bn x)"}\\
-$\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> \<dots> \<union> fv_ty\<^isub>m y\<^isub>m) - set (bn x)"}\\
+$\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m) - set (bn x)"}\\
 & provided the @{text "y"}$_{1..m}$ are of type @{text "ty"}$_{1..m}$; the first
-clause applies for @{text x} being a non-recursive deep binder, the
+clause applies for @{text x} being a non-recursive deep binder (that is
-second for a recursive deep binder
+@{text "x \<noteq> y"}$_{1..m}$), 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 define the function @{text "fv_bn"}. Assume
 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
+"bn (C z\<^isub>1 \<dots> z\<^isub>n) = rhs"}. We again define a value
-@{text v} which is exactly as in \eqref{deepbinder} for shallow and deep
+@{text v} which is exactly as in \eqref{deepbinderA}/\eqref{deepbinderB} for shallow and deep
 binding clauses, except for empty binding clauses are defined as follows:
 %
 \begin{equation}\label{bnemptybinder}
 \mbox{%
 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}

changeset 1961	774d631726ad
parent 1957	47430fe78912
child 2128	abd46dfc0212