nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:9807d30c0e54
+:09b476c20fe1
 @{text "(bs, y)"} are $\alpha$-equivalent? (For the moment we are interested in
 the notion of $\alpha$-equivalence that is \emph{not} preserved by adding
 vacuous binders.) To answer this question, we identify four conditions: {\it (i)}
 given a free-atom function @{text "fa"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
 set"}}, then @{text x} and @{text y} need to have the same set of free
-atomss; moreover there must be a permutation @{text p} such that {\it
+atoms; moreover there must be a permutation @{text p} such that {\it
 (ii)} @{text p} leaves the free atoms of @{text x} and @{text y} unchanged, but
 {\it (iii)} ``moves'' their bound names so that we obtain modulo a relation,
 say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)}
 @{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
 requirements {\it (i)} to {\it (iv)} can be stated formally as follows:
 There are also some restrictions we need to impose on our binding clauses in comparison to
 the ones of Ott. 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 an
-atom occurence cannot be both bound and free at the same time.  The first
+atom occurrence 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
 atoms of a body cannot be free at the same time by specifying an
 alternative binder for the same body). For binders we distinguish between
 \emph{shallow} and \emph{deep} binders.  Shallow binders are just
 \end{tabular}
 \end{center}
 \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"}
+out different atoms to become bound, respectively be free, in @{text "p"}.
-(since the Ott-tool does not derive a reasoning for $\alpha$-equated terms, it can permit
+(Since the Ott-tool does not derive a reasoning for $\alpha$-equated terms, it can permit
-such specifications).
+such specifications.)
 We also need to restrict the form of the binding functions in order
 to ensure the @{text "bn"}-functions can be defined for $\alpha$-equated
 terms. The main restriction is that we cannot return an atom in a binding function that is also
 bound in the corresponding term-constructor. That means in \eqref{letpat}
 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
+position (see \cite{Berghofer99} for an in-depth description of the datatype package
-in Isabelle/HOL). We then define each of the user-specified binding
+in Isabelle/HOL). We subsequently define each of the user-specified binding
-function @{term "bn\<^isub>i"} by recursion over the corresponding
+functions @{term "bn"}$_{1..m}$ by recursion over the corresponding
 raw datatype. We can also easily define permutation operations by
 recursion so that for each term constructor @{text "C"} 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-atom functions from the specifications. For the
+free-atom functions from the specification. For the
 \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions
 %
 \begin{equation}\label{fvars}
 @{text "fa_ty\<^isub>1, \<dots>, fa_ty\<^isub>n"}
 \end{equation}
 \end{center}
 \noindent
 The reason for this setup is that in a deep binder not all atoms have to be
 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.
+that calculates those free atoms in a deep binder.
 While the idea behind these free-atom 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 "bc\<^isub>1\<dots>bc\<^isub>k"}, the result of @{text
 "fa_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be the union @{text
-"fa(bc\<^isub>1) \<union> \<dots> \<union> fa(bc\<^isub>k)"} where we define below what @{text "fa"} for a binding
+"fa(bc\<^isub>1) \<union> \<dots> \<union> fa(bc\<^isub>k)"} where we will define below what @{text "fa"} for a binding
 clause means. We only show the details for the mode \isacommand{bind\_set} (the other modes are similar).
 Suppose the binding clause @{text bc\<^isub>i} is of the form
 %
-\begin{equation}
+\begin{center}
 \mbox{\isacommand{bind\_set} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
-\end{equation}
+\end{center}
 \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
+functions taking a single label as argument (in case of deep binders). Assuming
-set @{text "D"} stands for the free atoms in the bodies, the set @{text B} for the
+@{text "D"} stands for the set of free atoms of the bodies, @{text B} for the
-binding atoms in the binders and @{text "B'"} for the free atoms in
+set of binding atoms in the binders and @{text "B'"} for the set of free atoms in
 non-recursive deep binders,
-then the free atoms of the binding clause @{text bc\<^isub>i} are given by
+then the free atoms of the binding clause @{text bc\<^isub>i} are
 %
-\begin{center}
+\begin{equation}\label{fadef}
-@{text "fa(bc\<^isub>i) \<equiv> (D - B) \<union> B'"}
+\mbox{@{text "fa(bc\<^isub>i) \<equiv> (D - B) \<union> B'"}}.
-\end{center}
+\end{equation}
 \noindent
-whereby the set @{text D} is formally defined as
+The set @{text D} is formally defined as
 %
 \begin{center}
 @{text "D \<equiv> fa_ty\<^isub>1 d\<^isub>1 \<union> ... \<union> fa_ty\<^isub>q d\<^isub>q"}
 \end{center}
 \noindent
-The functions @{text "fa_ty\<^isub>i"} are the ones we are defining by recursion
+where in case @{text "d\<^isub>i"} refers to one of the raw types @{text "ty"}$_{1..n}$ from the
-(see \eqref{fvars}) in case the @{text "d\<^isub>i"} refers to one of the raw types
+specification, the function @{text "fa_ty\<^isub>i"} is the corresponding free-atom function
-@{text "ty"}$_{1..n}$ from the specification; otherwise we set @{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
+we are defining by recursion
-In order to define the set @{text B} we use the following auxiliary @{text "bn"}-functions
+(see \eqref{fvars}); otherwise we set @{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
-for atom types to which shallow binders have to refer
+In order to formally define the set @{text B} we use the following auxiliary @{text "bn"}-functions
+for atom types to which shallow binders may refer
 %
 \begin{center}
 \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
 @{text "bn_atom a"} & @{text "\<equiv>"} & @{text "{atom a}"}\\
 @{text "bn_atom_set as"} & @{text "\<equiv>"} & @{text "atoms as"}\\
 @{text "bn_atom_list as"} & @{text "\<equiv>"} & @{text "atoms (set as)"}
 \end{tabular}
 \end{center}
 \noindent
-The function @{text "atoms"} coerces
+Like the function @{text atom}, the function @{text "atoms"} coerces
-the set of atoms to a set of the generic atom type. It is defined as
+a 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 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}
 \noindent
+where we use the auxiliary binding functions for shallow binders.
 The set @{text "B'"} collects all free atoms in non-recursive deep
 binders. Let us assume these binders in @{text "bc\<^isub>i"} are
 %
 \begin{center}
-@{text "bn\<^isub>1 a\<^isub>1, \<dots>, bn\<^isub>r a\<^isub>r"}
+@{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}
 \end{center}
 \noindent
-with none of the @{text "a"}$_{1..r}$ being among the bodies @{text
+with none of the @{text "l"}$_{1..r}$ being among the bodies @{text
 "d"}$_{1..q}$. The set @{text "B'"} is defined as
 %
 \begin{center}
-@{text "B' \<equiv> fa_bn\<^isub>1 a\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r a\<^isub>r"}
+@{text "B' \<equiv> fa_bn\<^isub>1 l\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r l\<^isub>r"}
 \end{center}
 \noindent
-This completes the definition of the free-atom functions.
+This completes the definition of the free-atom functions @{text "fa_ty"}$_{1..n}$.
-Note that for non-recursive deep binders, we have to add all atoms that are left
+Note that for non-recursive deep binders, we have to add in \eqref{fadef}
-unbound by the binding function @{text "bn"} (the set @{text "B'"}). We use for this
+the set of atoms that are left unbound by the binding functions @{text
-the functions @{text "fa_bn"}, also defined by recursion. Assume the user specified
+"bn"}$_{1..m}$. We use for the definition of
-a @{text bn}-clause of the form
+this set the functions @{text "fa_bn"}$_{1..m}$, which are also defined by mutual
+recursion. Assume the user specified a @{text bn}-clause of the form
 %
 \begin{center}
 @{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
 \end{center}
 the arguments we calculate the free atoms as follows:
 %
 \begin{center}
 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
 $\bullet$ & @{term "fa_ty\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text "rhs"}
-(that means nothing is bound in @{text "z\<^isub>i"}),\\
+(that means nothing is bound in @{text "z\<^isub>i"} by the binding function),\\
 $\bullet$ & @{term "fa_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"}, 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 "fa_bn (C z\<^isub>1 \<dots> z\<^isub>n)"} we just union up all these values.
+For defining @{text "fa_bn (C z\<^isub>1 \<dots> z\<^isub>n)"} we just union up all these sets.
-To see how these definitions work in practice, let us reconsider the term-constructors
+To see how these definitions work in practice, let us reconsider the
-@{text "Let"} and @{text "Let_rec"}, as well as @{text "ANil"} and @{text "ACons"}
+term-constructors @{text "Let"} and @{text "Let_rec"} shown in
-from the example shown in \eqref{letrecs}.
+\eqref{letrecs} together with the term-constructors for assignments @{text
-For them we define three free-atom functions, namely
+"ANil"} and @{text "ACons"}. Since there is a binding function defined for
-@{text "fa\<^bsub>trm\<^esub>"}, @{text "fa\<^bsub>assn\<^esub>"} and @{text "fa\<^bsub>bn\<^esub>"} as follows:
+assignments, we have three free-atom functions, namely @{text
+"fa\<^bsub>trm\<^esub>"}, @{text "fa\<^bsub>assn\<^esub>"} and @{text
+"fa\<^bsub>bn\<^esub>"} as follows:
 %
 \begin{center}
 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
 @{text "fa\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t - set (bn as)) \<union> fa\<^bsub>bn\<^esub> as"}\\
 @{text "fa\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fa\<^bsub>assn\<^esub> as \<union> fa\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm]
 @{text "fa\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>bn\<^esub> as)"}
 \end{tabular}
 \end{center}
 \noindent
-To see the pattern, recall that @{text ANil} and @{text "ACons"} have no
+For these definitions, recall that @{text ANil} and @{text "ACons"} have no
 binding clause in the specification. The corresponding free-atom
-function @{text "fa\<^bsub>assn\<^esub>"} therefore returns all atoms
+function @{text "fa\<^bsub>assn\<^esub>"} therefore returns all free atoms
-occurring in an assignment. The binding only takes place in @{text Let} and
+occurring in an assignment (in case of @{text "ACons"}, they are given by
-@{text "Let_rec"}. In the @{text "Let"}-clause, the binding clause specifies
+calls to @{text supp}, @{text "fa\<^bsub>trm\<^esub>"} and @{text "fa\<^bsub>assn\<^esub>"}).
+The binding only takes place in @{text Let} and
+@{text "Let_rec"}. In case of @{text "Let"}, the binding clause specifies
 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
 "fa\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are
-free in @{text "as"}.  In contrast, in @{text "Let_rec"} we have a recursive
+free in @{text "as"}. This is
-binder where we want to also bind all occurrences of the atoms in @{text
+in contrast with @{text "Let_rec"} where we have a recursive
+binder to bind all occurrences of the atoms in @{text
 "set (bn as)"} also inside @{text "as"}. Therefore we have to subtract
-@{text "set (bn as)"} from the union @{text "fa\<^bsub>trm\<^esub> t"} and @{text "fa\<^bsub>assn\<^esub> as"}.
+@{text "set (bn as)"} from both @{text "fa\<^bsub>trm\<^esub> t"} and @{text "fa\<^bsub>assn\<^esub> as"}.
+Like the function @{text "bn"}, the function @{text "fa\<^bsub>bn\<^esub>"} traverses the
+list of assignments, but instead returns the free atoms, that means in this
+example the free atoms in the argument @{text "t"}.
 An interesting point in this
-example is that a ``naked'' assignment does not bind any
+example is that a ``naked'' assignment (@{text "ANil"} or @{text "ACons"}) does not bind any
-atoms. Only in the context of a @{text Let} or @{text "Let_rec"} will
+atoms, even if the binding function is specified over assignments.
-some atoms from an assignment become bound.  This is a phenomenon that has also been pointed
+Only in the context of a @{text Let} or @{text "Let_rec"}, where the binding clauses are given, will
+some atoms actually become bound.  This is a phenomenon that has also been pointed
 out in \cite{ott-jfp}. For us this observation is crucial, because we would
-not be able to lift the @{text "bn"}-function if it was defined over assignments
+not be able to lift the @{text "bn"}-functions to $\alpha$-equated terms if they act on
-where some atoms are bound. In that case @{text "bn"} would \emph{not} respect
+atoms that are bound. In that case, these functions would \emph{not} respect
 $\alpha$-equivalence.
-Next we define $\alpha$-equivalence relations for the raw types @{text
+Next we define the $\alpha$-equivalence relations for the raw types @{text
-"ty"}$_{1..n}$. We write them
+"ty"}$_{1..n}$ from the specification. We write them as
 %
 \begin{center}
 @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}.
 \end{center}
 \end{center}
 \noindent
 for the binding functions @{text "bn"}$_{1..m}$,
 To simplify our definitions we will use the following abbreviations for
-equivalence relations and free-atom functions acting on pairs
+\emph{compound equivalence relations} and \emph{compound free-atom functions} acting on tuples
 %
 \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 "(x\<^isub>1,.., x\<^isub>n) (R\<^isub>1,.., R\<^isub>n) (x\<PRIME>\<^isub>1,.., x\<PRIME>\<^isub>n)"} & @{text "\<equiv>"} & \\
-@{text "(fa\<^isub>1 \<oplus> fa\<^isub>2) (x, y)"} & @{text "\<equiv>"} & @{text "fa\<^isub>1 x \<union> fa\<^isub>2 y"}\\
+\multicolumn{3}{r}{@{text "x\<^isub>1 R\<^isub>1 x\<PRIME>\<^isub>1 \<and> .. \<and> x\<^isub>n R\<^isub>n x\<PRIME>\<^isub>n"}}\\
-\end{tabular}
+@{text "(fa\<^isub>1,.., fa\<^isub>n) (x\<^isub>1,.., x\<^isub>n)"} & @{text "\<equiv>"} & @{text "fa\<^isub>1 x\<^isub>1 \<union> .. \<union> fa\<^isub>n x\<^isub>n"}\\
-\end{center}
+\end{tabular}
+\end{center}
-The relations for $\alpha$-equivalence are inductively defined
-predicates, whose clauses have the form
+The $\alpha$-equivalence relations are defined as inductive predicates
+having a single clause for each term-constructor. Assuming a
+term-constructor @{text C} is of type @{text ty} and has the binding clauses
+@{term "bc"}$_{1..k}$, then the $\alpha$-equivalence clause has the form
 %
 \begin{center}
 \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) \<and> \<dots> \<and> prems(bc\<^isub>k)"}}}
+{@{text "prems(bc\<^isub>1) \<dots> prems(bc\<^isub>k)"}}}
 \end{center}
 \noindent
-assuming the term-constructor @{text C} is of type @{text ty} and has
+The task below is to specify what the premises of a binding clause are. As a
-the binding clauses @{term "bc"}$_{1..k}$.  The task
+special instance, we first treat the case where @{text "bc\<^isub>i"} is the
-is to specify what the premises of these clauses are. Again for this we
+empty binding clause of the form
-analyse the binding clauses and produce a corresponding premise.
+%
+\begin{center}
+\mbox{\isacommand{bind\_set} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
+\end{center}
+\noindent
+In this binding clause no atom is bound and we only have to $\alpha$-relate the bodies. For this
+we build first the tuples @{text "D \<equiv> (d\<^isub>1,\<dots>, d\<^isub>q)"} and @{text "D' \<equiv> (d\<PRIME>\<^isub>1,\<dots>, d\<PRIME>\<^isub>q)"}
+whereby the labels @{text "d"}$_{1..q}$ refer to arguments @{text "z"}$_{1..n}$ and
+respectively @{text "d\<PRIME>"}$_{1..q}$ to @{text "z\<PRIME>"}$_{1..n}$. In order to relate
+two such tuples we define the compound $\alpha$-equivalence relation @{text "R"} as follows
+%
+\begin{equation}\label{rempty}
+\mbox{@{text "R \<equiv> (R\<^isub>1,\<dots>, R\<^isub>q)"}}
+\end{equation}
+\noindent
+with @{text "R\<^isub>i"} being @{text "\<approx>ty\<^isub>i"} if the corresponding labels @{text "d\<^isub>i"} and
+@{text "d\<PRIME>\<^isub>i"} refer
+to a recursive argument of @{text C} with type @{text "ty\<^isub>i"}; otherwise
+we take @{text "R\<^isub>i"} to be the equality @{text "="}. This lets us define
+the premise for an empty binding clause succinctly as @{text "prems(bc\<^isub>i) \<equiv> D R D'"},
+which can be unfolded to the series of premises
+%
+\begin{center}
+@{text "d\<^isub>1 R\<^isub>1 d\<PRIME>\<^isub>1  \<dots> d\<^isub>q R\<^isub>q d\<PRIME>\<^isub>q"}
+\end{center}
+\noindent
+We will use the unfolded version in the examples below.
+Now suppose the binding clause @{text "bc\<^isub>i"} is of the general form
+%
+\begin{equation}\label{nonempty}
+\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 this case we define a premise @{text P} using the relation
+$\approx_{\,\textit{set}}$ given in Section~\ref{sec:binders} (similarly
+$\approx_{\,\textit{res}}$ and $\approx_{\,\textit{list}}$ for the other
+binding modes). This premise defines $\alpha$-equivalence of two abstractions
+involving multiple binders. We first define as above the tuples @{text "D"} and
+@{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding
+compound $\alpha$-relation @{text "R"} (shown in \eqref{rempty}).
+For $\approx_{\,\textit{set}}$ we also need
+a compound free-atom function for the bodies defined as
+%
+\begin{center}
+\mbox{@{text "fa \<equiv> (fa_ty\<^isub>1,\<dots>, fa_ty\<^isub>q)"}}
+\end{center}
+\noindent
+with assumption that the @{text "d"}$_{1..q}$ refer to arguments of types @{text "ty"}$_{1..q}$.
+The last ingredient we need are the sets of atoms bound in the bodies.
+For this we take
+\begin{center}
+@{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> \<dots> \<union> bn_ty\<^isub>p b\<^isub>p"}\;.\\
+\end{center}
+\noindent
+Similarly for @{text "B'"} using the labels @{text "b\<PRIME>"}$_{1..p}$. This
+lets us formally define the premise @{text P} for a non-empty binding clause as:
+%
+\begin{equation}\label{pprem}
+\mbox{@{term "P \<equiv> \<exists>p. (B, D) \<approx>gen R fa p (B', D')"}}\;.
+\end{equation}
+\noindent
+This premise accounts for $\alpha$-equivalence of the bodies of the binding
+clause. However, in case the binders have non-recursive deep binders, then
+we also have to ``propagate'' $\alpha$-equivalence inside the structure of
+these binders. An example is @{text "Let"} where we have to make sure the
+right-hand sides of assignments are $\alpha$-equivalent. For this we use the
+relations @{text "\<approx>bn"}$_{1..m}$ (which we will formally define shortly).
+Let us assume the non-recursive deep binders in @{text "bc\<^isub>i"} are
+%
+\begin{center}
+@{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}.
+\end{center}
+\noindent
+The premises for @{text "bc\<^isub>i"} are then defined as
+%
+\begin{center}
+@{text "prems(bc\<^isub>i) \<equiv> P  \<and>  l\<^isub>1 \<approx>bn\<^isub>1 l\<PRIME>\<^isub>1  \<and> ... \<and>  l\<^isub>r \<approx>bn\<^isub>r l\<PRIME>\<^isub>r"}
+\end{center}
+\noindent
+where @{text "P"} is defined in \eqref{pprem}.
+The $\alpha$-equivalence relations @{text "\<approx>bn"}$_{1..m}$ are defined as follows:
+given a @{text bn}-clause of the form
+%
+\begin{center}
+@{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
+\end{center}
+\noindent
+where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$,
+then the $\alpha$-equivalence clause for @{text "\<approx>bn"} has the form
+%
+\begin{center}
+\mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>s \<approx>bn C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>s"}}
+{@{text "z\<^isub>1 R\<^isub>1 z\<PRIME>\<^isub>1 \<dots> z\<^isub>s R\<^isub>s z\<PRIME>\<^isub>s"}}}
+\end{center}
+\noindent
+whereby the relations @{text "R"}$_{1..s}$ are given by
+\begin{center}
+\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
+$\bullet$ & @{text "z\<^isub>i \<approx>ty z\<PRIME>\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text rhs} and
+is a recursive argument of @{text C},\\
+$\bullet$ & @{text "z\<^isub>i = z\<PRIME>\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text rhs}
+and is a non-recursive argument of @{text C},\\
+$\bullet$ & @{text "z\<^isub>i \<approx>bn\<^isub>i z\<PRIME>\<^isub>i"} provided @{text "z\<^isub>i"} occurs in @{text rhs}
+with the recursive call @{text "bn\<^isub>i x\<^isub>i"} and\\
+$\bullet$ & @{text True} provided @{text "z\<^isub>i"} occurs in @{text rhs} but without a
+recursive call.
+\end{tabular}
+\end{center}
+\noindent
+This completes the definition of $\alpha$-equivalence. As a sanity check, we can show
+that the premises of empty binding clauses are a special case of the clauses for
+non-empty ones (we just have to unfold the definition of $\approx_{\,\textit{set}}$ and take @{text "0"}
+as the permutation).
 *}
-(*<*)
+(*<*)consts alpha_ty ::'a
-consts alpha_ty ::'a
 consts alpha_trm ::'a
 consts fa_trm :: 'a
 consts alpha_trm2 ::'a
 consts fa_trm2 :: 'a
 notation (latex output)
 alpha_ty ("\<approx>ty") and
 alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and
 fa_trm ("fa\<^bsub>trm\<^esub>") and
 alpha_trm2 ("\<approx>\<^bsub>assn\<^esub> \<otimes> \<approx>\<^bsub>trm\<^esub>") and
-fa_trm2 ("fa\<^bsub>assn\<^esub> \<oplus> fa\<^bsub>trm\<^esub>")
+fa_trm2 ("fa\<^bsub>assn\<^esub> \<oplus> fa\<^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"}:}\\
-$\bullet$ & @{text "x\<^isub>i \<approx>ty y\<^isub>i"} provided @{text "x\<^isub>i"} and @{text "y\<^isub>i"}
-are recursive arguments of @{text "C"}\\
-$\bullet$ & @{term "x\<^isub>i = y\<^isub>i"} provided @{text "x\<^isub>i"} and @{text "y\<^isub>i"} are
-non-recursive arguments\smallskip\\
-\multicolumn{2}{@ {}l}{Shallow binders of the form
-\isacommand{bind\_set}~@{text "x\<^isub>1\<dots>x\<^isub>n"}~\isacommand{in}~@{text "x'\<^isub>1\<dots>x'\<^isub>m"}:}\\
-$\bullet$ & Assume the bodies @{text "x'\<^isub>1\<dots>x'\<^isub>m"} are of type @{text "ty\<^isub>1\<dots>ty\<^isub>m"},
-@{text "R"} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fa} is
-@{text "fa_ty\<^isub>1 \<oplus> ... \<oplus> fa_ty\<^isub>m"}, then
-\begin{center}
-@{term "\<exists>p. (x\<^isub>1 \<union> \<xi> \<union> x\<^isub>n, (x'\<^isub>1,\<xi>,x'\<^isub>m)) \<approx>gen R fa p (y\<^isub>1 \<union> \<xi> \<union> y\<^isub>n, (y'\<^isub>1,\<xi>,y'\<^isub>m))"}
-\end{center}\\
-\multicolumn{2}{@ {}l}{Deep binders of the form
-\isacommand{bind\_set}~@{text "bn x"}~\isacommand{in}~@{text "x'\<^isub>1\<dots>x'\<^isub>m"}:}\\
-$\bullet$ & Assume the bodies @{text "x'\<^isub>1\<dots>x'\<^isub>m"} are of type @{text "ty\<^isub>1\<dots>ty\<^isub>m"},
-@{text "R"} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fa} is
-@{text "fa_ty\<^isub>1 \<oplus> ... \<oplus> fa_ty\<^isub>m"}, then for recursive deep binders
-\begin{center}
-@{term "\<exists>p. (bn x, (x'\<^isub>1,\<xi>,x'\<^isub>m)) \<approx>gen R fa p (bn y, (y'\<^isub>1,\<xi>,y'\<^isub>m))"}
-\end{center}\\
-$\bullet$ & for non-recursive binders we generate in addition @{text "x \<approx>bn y"}\\
-\end{tabular}}
-\end{equation}
-\noindent
-Similarly for the other binding modes.
-From this definition it is clear why we have to impose the restriction
-of excluding overlapping deep binders, as these would need to be translated into separate
-abstractions.
-The $\alpha$-equivalence relations @{text "\<approx>bn\<^isub>j"} for binding functions
-are similar. We again have conclusions of the form \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>bn C y\<^isub>1 \<dots> y\<^isub>n"}}
-and need to generate appropriate premises. We generate first premises according to the first three
-rules given above. Only the ``left-over'' pairs  @{text "(x\<^isub>i, y\<^isub>i)"} need to be treated
-differently. They depend on whether @{text "x\<^isub>i"}  occurs in @{text "rhs"} of  the
-clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}:
-\begin{center}
-\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-$\bullet$ & @{text "x\<^isub>i \<approx>ty y\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text rhs}
-and the type of @{text "x\<^isub>i"} is @{text ty} and @{text "x\<^isub>i"} is a recursive argument
-in the term-constructor\\
-$\bullet$ & @{text "x\<^isub>i = y\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text rhs}
-and @{text "x\<^isub>i"} is not a recursive argument in the term-constructor\\
-$\bullet$ & @{text "x\<^isub>i \<approx>bn y\<^isub>i"} provided @{text "x\<^isub>i"} occurs in @{text rhs}
-with the recursive call @{text "bn x\<^isub>i"}\\
-$\bullet$ & none provided @{text "x\<^isub>i"} occurs in @{text rhs} but it is not
-in a recursive call involving a @{text "bn"}
-\end{tabular}
-\end{center}
 Again lets take a look at a concrete example for these definitions. For \eqref{letrecs}
-we have three relations, namely $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
+we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
-$\approx_{\textit{bn}}$, with the clauses as follows:
+$\approx_{\textit{bn}}$ with the following clauses:
 \begin{center}
 \begin{tabular}{@ {}c @ {}}
 \infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
-{@{text "as \<approx>\<^bsub>bn\<^esub> as'"} & @{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"}}\smallskip\\
+{@{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\
 \infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
 {@{term "\<exists>p. (bn as, (as, t)) \<approx>lst alpha_trm2 fa_trm2 p (bn as', (as', t'))"}}
 \end{tabular}
 \end{center}

changeset 2348	09b476c20fe1
parent 2347	9807d30c0e54
child 2349	eaf5209669de