nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:36aeb97fabb0
+:e90f6a26d74b
 %Interestingly, in case of \isacommand{bind\_set}
 %and \isacommand{bind\_res} the binding clauses above will make a difference to the semantics
 %of the specifications (the corresponding $\alpha$-equivalence will differ). We will
 %show this later with an example.
-There are also some restrictions we need to impose on binding clauses: the
+There are also some restrictions we need to impose on binding clauses. The
 main idea behind these restrictions is that we obtain a sensible notion of
 $\alpha$-equivalence where it is ensured that within a given scope a
-variable occurence cannot be bound and free at the same time.  First, a body can only occur in
+variable occurence cannot be both bound and free at the same time.  The first
+restriction is that a body can only occur in
 \emph{one} binding clause of a term constructor (this ensures that the bound
 variables of a body cannot be free at the same time by specifying an
-alternative binder for the body). For binders we distinguish between
+alternative binder for the same body). For binders we distinguish between
 \emph{shallow} and \emph{deep} binders.  Shallow binders are just
 labels. The restriction we need to impose on them is that in case of
 \isacommand{bind\_set} and \isacommand{bind\_res} the labels must either
 refer to atom types or to sets of atom types; in case of \isacommand{bind}
 the labels must refer to atom types or lists of atom types. Two examples for
 \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p t"}\\
 \end{tabular}
 \end{center}
 \noindent
-where the argument of the deep binder is also in the body. We call such
+where the argument of the deep binder also occurs in the body. We call such
 binders \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}
 "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.
 To make sure that variables bound by deep binders cannot be free at the
-same time, we have to impose some further restrictions. First,
+same time, we cannot have more than one binding function for one binder.
-we cannot have more than one binding function for one binder. So we exclude:
+Consequently we exclude specifications such as
 \begin{center}
 \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
 @{text "Baz\<^isub>1 p::pat t::trm"} &
 \isacommand{bind} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\
 \isacommand{bind} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "t\<^isub>2"}\\
 \end{tabular}
 \end{center}
 \noindent
-Otherwise it is be possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"}  pick
+Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"}  pick
-out different atoms to become bound in @{text "p"}.
+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
-We also need to restrict the form of the binding functions. As will shortly
+to ensure the @{text "bn"}-functions can be lifted defined for $\alpha$-equated
-become clear, we cannot return an atom in a binding function that is also
+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
 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"}, by recursion over the corresponding
+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 the
+recursion so that for each term constructor @{text "C"} with
-argument types @{text "ty"}$_{1..n}$ 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}
-\noindent
-where the variables @{text "z"}$_{1..n}$ are of types @{text "ty"}$_{1..n}$.
 The first non-trivial step we have to perform is the generation of
-free-variable functions from the specifications. Given a raw term, these
+free-variable functions from the specifications. For the
-functions return sets of atoms. Assuming a nominal datatype
+\emph{raw} types @{text "ty"}$_{1..n}$ of a specification,
-specification as in \eqref{scheme} and its \emph{raw} types @{text "ty"}$_{1..n}$,
 we define the free-variable functions
 %
 \begin{equation}\label{fvars}
 @{text "fv_ty\<^isub>1, \<dots>, fv_ty\<^isub>n"}
 \end{equation}
 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.  Given a
+binding mechanisms their definitions are somewhat involved. The functions
-term-constructor @{text "C"} of type @{text ty} and some associated binding
+are defined by recursion defining a clause for each term-constructor.  Given
-clauses @{text "bc\<^isub>1\<dots>bc\<^isub>k"}, the result of the @{text "fv_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be
+the term-constructor @{text "C"} of type @{text ty} and some associated
-the union @{text "fv(bc\<^isub>1) \<union> \<dots> \<union> fv(bc\<^isub>k)"} of free variables calculated for
+binding clauses @{text "bc\<^isub>1\<dots>bc\<^isub>k"}, the result of @{text
-each binding clause. Given a binding clause @{text bc} is of the form
+"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
+bc\<^isub>i} is of the form
 %
 \begin{equation}
-\mbox{\isacommand{bind} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
+\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
-where the body labels @{text "d"}$_{1..q}$ refer to types @{text ty}$_{1..q}$; the binders
+in which the body-labels @{text "d"}$_{1..q}$ refer to types @{text ty}$_{1..q}$,
-@{text b}$_{1..p}$
+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
-free variables of the bodies is the set @{text "D"}, the bound variables of the binders
+set @{text "D"} stands for the free atoms in the bodies, @{text B} for the
-is the set @{text B} and the free variables of the non-recursive deep binders is @{text "B'"}
+binding atoms in the binders and @{text "B'"} for the free atoms in
-then the free variables of the binding clause @{text bc} is
+non-recursive deep binders,
-%
+then the free atoms of the binding clause @{text bc\<^isub>i} are given by
-\begin{center}
+%
-@{text "fv(bc) = (D - B) \<union> B'"}
+\begin{center}
-\end{center}
+@{text "fv(bc\<^isub>i) \<equiv> (D - B) \<union> B'"}
+\end{center}
-\noindent
-Formally the set @{text D} is the union of the free variables for the bodies
+\noindent
-%
+The set @{text D} is defined as
-\begin{center}
+%
-@{text "D = fv_ty\<^isub>1 d\<^isub>1 \<union> ... \<union> fv_ty\<^isub>q d\<^isub>q"}
+\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 free variable functions @{text "fv_ty\<^isub>i"} are the ones in \eqref{fvars}
+whereby the functions @{text "fv_ty\<^isub>i"} are the ones we are defining by recursion
-provided the @{text "d\<^isub>i"} refers to one of the types @{text "ty"}$_{1..n}$;
+(see \eqref{fvars}) provided the @{text "d\<^isub>i"} refers to one of the types
-otherwise we set @{text "fv_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
+@{text "ty"}$_{1..n}$; 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
+for atom types to which shallow binders have to refer
-if @{text "d\<^isub>i"} is a label
+%
-for an atomic type we use the following auxiliary free variable functions
 \begin{center}
 \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-@{text "fv_atom a"} & @{text "="} & @{text "{atom a}"}\\
+@{text "bn_atom a"} & @{text "="} & @{text "{atom a}"}\\
-@{text "fv_atom_set as"} & @{text "="} & @{text "atoms as"}\\
+@{text "bn_atom_set as"} & @{text "="} & @{text "atoms as"}\\
-@{text "fv_atom_list as"} & @{text "="} & @{text "atoms (set as)"}\\
+@{text "bn_atom_list as"} & @{text "="} & @{text "atoms (set as)"}
 \end{tabular}
 \end{center}
 \noindent
 In these functions, @{text "atoms"}, like @{text "atom"}, coerces
-the set of atoms to a set of the generic atom type.
+the set of atoms to a set of the generic atom type. It is defined as
-It is defined as @{text "atoms as \<equiv> {atom a | a \<in> as}"}. Otherwise
+@{text "atoms as \<equiv> {atom a | a \<in> as}"}.
+The set @{text B} is then defined as
+%
+\begin{center}
-the values, @{text v}, calculated by the rules for each bining clause:
+@{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> ... \<union> bn_ty\<^isub>p b\<^isub>p"}
-%
+\end{center}
-\begin{equation}\label{deepbinderA}
-\mbox{%
+\noindent
-\begin{tabular}{c@ {\hspace{2mm}}p{7.4cm}}
+The set @{text "B'"} collects all free atoms in non-recursive deep
-\multicolumn{2}{@ {}l}{\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\
+binders. Lets assume these binders in @{text "bc\<^isub>i"} are
-$\bullet$ & @{term "v = fv_ty y"} provided @{text "y"} is of type @{text "ty"}\smallskip\\
+%
-%
+\begin{center}
-\multicolumn{2}{@ {}l}{\isacommand{bind}~@{text "x\<^isub>1\<dots>x\<^isub>n"}~\isacommand{in}~@{text "y\<^isub>1\<dots>y\<^isub>m"}:}\\
+@{text "bn\<^isub>1 a\<^isub>1, \<dots>, bn\<^isub>r a\<^isub>r"}
-$\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m)"}\\
+\end{center}
-& \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
+\noindent
-binders @{text "x"}$_{1..n}$ of atomic types @{text "aty"}$_{1..n}$\smallskip\\
+with none of the @{text "a"}$_{1..r}$ being among the bodies @{text
-\end{tabular}}
+"d"}$_{1..q}$. The set @{text "B'"} is then defined as
-\end{equation}
+%
-\begin{equation}\label{deepbinderB}
+\begin{center}
-\mbox{%
+@{text "B' \<equiv> fv_bn\<^isub>1 a\<^isub>1 \<union> ... \<union> fv_bn\<^isub>r a\<^isub>r"}
-\begin{tabular}{c@ {\hspace{2mm}}p{7.4cm}}
+\end{center}
-\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> .. \<union> fv_ty\<^isub>m y\<^isub>m) - set (bn x) \<union> (fv_bn x)"}\\
+\noindent
-$\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m) - set (bn x)"}\\
+Similarly for the other binding modes.
-& 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 (that is
+Note that for non-recursive deep binders, we have to add all atoms that are left
-@{text "x \<noteq> y"}$_{1..m}$), the second for a recursive deep binder
+unbound by the binding function @{text "bn"}. This is the purpose of the functions
-\end{tabular}}
+@{text "fv_bn"}, also defined by recursion. Assume the user has specified
-\end{equation}
+a @{text bn}-clause of the form
+%
-\noindent
+\begin{center}
-Similarly for the other binding modes. Note that in a non-recursive deep
+@{text "bn (C z\<^isub>1 \<dots> z\<^isub>n) = rhs"}
-binder, we have to add all atoms that are left unbound by the binding
+\end{center}
-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
+\noindent
-"bn (C z\<^isub>1 \<dots> z\<^isub>n) = rhs"}. We again define a value
+where the @{text "z"}$_{1..n}$ are of types @{text "ty"}$_{1..n}$. For each of
-@{text v} which is exactly as in \eqref{deepbinderA}/\eqref{deepbinderB} for shallow and deep
+the arguments we calculate the free atoms as follows
-binding clauses, except for empty binding clauses are defined as follows:
+%
-%
+\begin{center}
-\begin{equation}\label{bnemptybinder}
-\mbox{%
 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-\multicolumn{2}{@ {}l}{\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\
+$\bullet$ & @{term "fv_ty\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text "rhs"}\\
-$\bullet$ & @{term "v = fv_ty y"} provided @{text "y"} does not occur in @{text "rhs"}
+$\bullet$ & @{term "fv_bn\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} occurs in  @{text "rhs"}
-and the free-variable function for the type of @{text "y"} is @{text "fv_ty"}\\
+with the recursive call @{text "bn\<^isub>i z\<^isub>i"}\\
-$\bullet$ & @{term "v = fv_bn y"} provided @{text "y"} occurs in  @{text "rhs"}
+$\bullet$ & @{term "{}"} provided @{text "z\<^isub>i"} occurs in  @{text "rhs"},
-with a recursive call @{text "bn y"}\\
+but without a recursive call
-$\bullet$ & @{term "v = {}"} provided @{text "y"} occurs in  @{text "rhs"},
+\end{tabular}
-but without a recursive call\\
+\end{center}
-\end{tabular}}
-\end{equation}
+\noindent
+For defining @{text "fv_bn (C z\<^isub>1 \<dots> z\<^isub>n)"}, we just union up all these values.
-\noindent
-The reason why we only have to treat the empty binding clauses specially in
-the definition of @{text "fv_bn"} is that binding functions can only use arguments
-that do not occur in binding clauses. Otherwise the @{text "bn"} function cannot
-be lifted to $\alpha$-equated terms.
 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}.
-For this specification we need to define three free-variable functions, namely
+For them we consider 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:
+@{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"}:
 %
 \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]
 \end{equation}
 \noindent
 holds for any @{text "bn"}-function defined for the type @{text "ty"}.
+TBD below.
 Next we define $\alpha$-equivalence relations 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 binding functions @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, then we also define @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}.
 To simplify our definitions we will use the following abbreviations for
 The relations for $\alpha$-equivalence are inductively defined predicates, whose clauses have
 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"}
+\mbox{\infer{@{text "C x\<^isub>1 \<dots> x\<^isub>n  \<approx>ty  C y\<^isub>1 \<dots> y\<^isub>n"}}
+{@{text "prems(bc\<^isub>1)"} & @{text "\<dots>"} & @{text "prems(bc\<^isub>p)"}}}
 \end{center}
 \noindent
 For what follows, let us assume @{text C} is of type @{text ty}.  The task
 is to specify what the premises of these clauses are. Again for this we
 @{text "Foo\<^isub>2 {a, b} (a, b) (a, b)"} & $=$ &
 @{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\
 \end{tabular}
 \end{center}
-To see this, consider the following equations
-\begin{center}
-\begin{tabular}{c}
-@{term "Abs_print [a,b] (a, b) = Abs_print [a,b] (b, a)"}\\
-@{term "Abs_print [a,b] (a, b) = Abs_print [a,b] (a, b)"}\\
-\end{tabular}
-\end{center}
-\noindent
-The interesting point is that they do not imply
-\begin{center}
-\begin{tabular}{c}
-@{term "Abs_print [a,b] ((a, b), (a, b)) = Abs_print [a,b] ((a, b), (b, a))"}\\
-\end{tabular}
-\end{center}
 Because of how we set up our definitions, we had to impose restrictions,
 like a single binding function for a deep binder, that are not present in Ott. Our
 expectation is that we can still cover many interesting term-calculi from
 programming language research, for example Core-Haskell. For providing support
 of neat features in Ott, such as subgrammars, the existing datatype

changeset 2344	e90f6a26d74b
parent 2343	36aeb97fabb0
child 2345	a908ea36054f