nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:679cef364022
+:734341a79028
 \draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);
 \draw (-2.0, 0.845) --  (0.7,0.845);
 \draw (-2.0,-0.045)  -- (0.7,-0.045);
-\draw ( 0.7, 0.4) node {\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]clas.\end{tabular}};
+\draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]clas.\end{tabular}};
-\draw (-2.4, 0.4) node {\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};
+\draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};
 \draw (1.8, 0.48) node[right=-0.1mm]
-{\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}};
+{\footnotesize\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}};
-\draw (0.9, -0.35) node {\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};
+\draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};
-\draw (-3.25, 0.55) node {\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};
+\draw (-3.25, 0.55) node {\footnotesize\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};
 \draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);
-\draw (-0.95, 0.3) node[above=0mm] {isomorphism};
+\draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};
 \end{tikzpicture}
 \end{center}
 %
 \noindent
 this function can be defined for raw terms, it does not respect
 $\alpha$-equivalence and therefore cannot be lifted. To sum up, every lifting
 of theorems to the quotient level needs proofs of some respectfulness
 properties (see \cite{Homeier05}). In the paper we show that we are able to
 automate these proofs and as a result can automatically establish a reasoning
-infrastructure for $\alpha$-equated terms.
+infrastructure for $\alpha$-equated terms.\smallskip
-The examples we have in mind where our reasoning infrastructure will be
+%The examples we have in mind where our reasoning infrastructure will be
-helpful includes the term language of Core-Haskell. This term language
+%helpful includes the term language of Core-Haskell. This term language
-involves patterns that have lists of type-, coercion- and term-variables,
+%involves patterns that have lists of type-, coercion- and term-variables,
-all of which are bound in @{text "\<CASE>"}-expressions. In these
+%all of which are bound in @{text "\<CASE>"}-expressions. In these
-patterns we do not know in advance how many variables need to
+%patterns we do not know in advance how many variables need to
-be bound. Another example is the specification of SML, which includes
+%be bound. Another example is the specification of SML, which includes
-includes bindings as in type-schemes.\medskip
+%includes bindings as in type-schemes.\medskip
 \noindent
 {\bf Contributions:}  We provide three new definitions for when terms
 involving general binders are $\alpha$-equivalent. These definitions are
 inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic
 Two central notions in the nominal logic work are sorted atoms and
 sort-respecting permutations of atoms. We will use the letters @{text "a,
 b, c, \<dots>"} to stand for atoms and @{text "p, q, \<dots>"} to stand for
 permutations. The purpose of atoms is to represent variables, be they bound or free.
 The sorts of atoms can be used to represent different kinds of
-variables, such as the term-, coercion- and type-variables in Core-Haskell.
+variables.
+%%, such as the term-, coercion- and type-variables in Core-Haskell.
 It is assumed that there is an infinite supply of atoms for each
 sort. However, in the interest of brevity, we shall restrict ourselves
 in what follows to only one sort of atoms.
 Permutations are bijective functions from atoms to atoms that are
 where @{term set} is the function that coerces a list of atoms into a set of atoms.
 Now the last clause ensures that the order of the binders matters (since @{text as}
 and @{text bs} are lists of atoms).
 If we do not want to make any difference between the order of binders \emph{and}
-also allow vacuous binders, then we keep sets of binders, but drop the fourth
+also allow vacuous binders, that means \emph{restrict} names, then we keep sets of binders, but drop
-condition in \eqref{alphaset}:
+condition {\it (iv)} in \eqref{alphaset}:
 %
 \begin{equation}\label{alphares}
 \begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l}
 \multicolumn{2}{l}{@{term "(as, x) \<approx>res R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
 \mbox{\it (i)}   & @{term "fa(x) - as = fa(y) - bs"} &
 \end{tabular}
 \end{center}
 \end{theorem}
 \noindent
-This theorem states that the bound names do not appear in the support, as expected.
+This theorem states that the bound names do not appear in the support.
-For brevity we omit the proof of this resul and again refer the reader to
+For brevity we omit the proof and again refer the reader to
 our formalisation in Isabelle/HOL.
 %\noindent
 %Below we will show the first equation. The others
 %follow by similar arguments. By definition of the abstraction type @{text "abs_set"}
 form @{term "Abs_set as x"} etc is motivated by the fact that
 we can conveniently establish  at the Isabelle/HOL level
 properties about them.  It would be
 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.
+the definitions for $\alpha$-equivalence will help us in the next sections.
 *}
 section {* Specifying General Bindings\label{sec:spec} *}
 text {*
 type \mbox{declaration part} &
 $\begin{cases}
 \mbox{\begin{tabular}{l}
 \isacommand{nominal\_datatype} @{text "ty\<AL>\<^isub>1 = \<dots>"}\\
 \isacommand{and} @{text "ty\<AL>\<^isub>2 = \<dots>"}\\
-$\ldots$\\
+\raisebox{2mm}{$\ldots$}\\[-2mm]
 \isacommand{and} @{text "ty\<AL>\<^isub>n = \<dots>"}\\
 \end{tabular}}
 \end{cases}$\\
 binding \mbox{function part} &
 $\begin{cases}
 \mbox{\begin{tabular}{l}
 \isacommand{binder} @{text "bn\<AL>\<^isub>1"} \isacommand{and} \ldots \isacommand{and} @{text "bn\<AL>\<^isub>m"}\\
 \isacommand{where}\\
-$\ldots$\\
+\raisebox{2mm}{$\ldots$}\\[-2mm]
 \end{tabular}}
 \end{cases}$\\
 \end{tabular}}
 \end{equation}
 \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) can be contained
+whereby some of the @{text ty}$'_{1..l}$ %%(or their components)
+can be contained
 in the collection of @{text ty}$^\alpha_{1..n}$ declared in
 \eqref{scheme}.
 In this case we will call the corresponding argument a
 \emph{recursive argument} of @{text "C\<^sup>\<alpha>"}.
 %The types of such recursive
 the second is for sets of binders (the order does not matter, but the
 cardinality does) and the last is for sets of binders (with vacuous binders
 preserving $\alpha$-equivalence). As indicated, the labels in the ``\isacommand{in}-part'' of a binding
 clause will be called \emph{bodies}; the
 ``\isacommand{bind}-part'' will be called \emph{binders}. In contrast to
-Ott, we allow multiple labels in binders and bodies. For example we allow
+Ott, we allow multiple labels in binders and bodies.
-binding clauses of the form:
+%For example we allow
-\begin{center}
+%binding clauses of the form:
-\begin{tabular}{@ {}ll@ {}}
+%
-@{text "Foo\<^isub>1 x::name y::name t::trm s::trm"} &
+%\begin{center}
-\isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}\\
+%\begin{tabular}{@ {}ll@ {}}
-@{text "Foo\<^isub>2 x::name y::name t::trm s::trm"} &
+%@{text "Foo\<^isub>1 x::name y::name t::trm s::trm"} &
-\isacommand{bind} @{text "x y"} \isacommand{in} @{text "t"},
+%    \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}\\
-\isacommand{bind} @{text "x y"} \isacommand{in} @{text "s"}\\
+%@{text "Foo\<^isub>2 x::name y::name t::trm s::trm"} &
-\end{tabular}
+%    \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t"},
-\end{center}
+%    \isacommand{bind} @{text "x y"} \isacommand{in} @{text "s"}\\
+%\end{tabular}
-\noindent
+%\end{center}
-Similarly for the other binding modes.
+\noindent
+%Similarly for the other binding modes.
 %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.
 \begin{tabular}{@ {}l}
 \isacommand{nominal\_datatype} @{text lam} $=$\\
 \hspace{5mm}\phantom{$\mid$}~@{text "Var name"}\\
 \hspace{5mm}$\mid$~@{text "App lam lam"}\\
 \hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}\\
-\hspace{21mm}\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
+\hspace{24mm}\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
 \end{tabular} &
 \begin{tabular}{@ {}l@ {}}
 \isacommand{nominal\_datatype}~@{text ty} $=$\\
 \hspace{5mm}\phantom{$\mid$}~@{text "TVar name"}\\
 \hspace{5mm}$\mid$~@{text "TFun ty ty"}\\
 \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}\\
-\hspace{21mm}\isacommand{bind (res)} @{text xs} \isacommand{in} @{text T}\\
+\hspace{29mm}\isacommand{bind (res)} @{text xs} \isacommand{in} @{text T}\\
 \end{tabular}
 \end{tabular}
 \end{center}
 \noindent
 specification:
 %
 \begin{equation}\label{letrecs}
 \mbox{%
 \begin{tabular}{@ {}l@ {}}
-\isacommand{nominal\_datatype}~@{text "trm ="}\\
+\isacommand{nominal\_datatype}~@{text "trm ="}\ldots\\
-\hspace{5mm}\phantom{$\mid$}\ldots\\
 \hspace{5mm}$\mid$~@{text "Let as::assn t::trm"}
 \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t}\\
 \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}
 \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\
 \isacommand{and} @{text "ass"} =\\
 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
-is sufficient for having the binding function over $\alpha$-equated terms.
+is sufficient for lifting the binding function to $\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
 we shall assume specifications
 of term-calculi are implicitly \emph{completed}. By this we mean that
 for every argument of a term-constructor that is \emph{not}
 already part of a binding clause given by the user, we add implicitly a special \emph{empty} binding
 clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case
-of the lambda-calculus, the completion produces
+of the lambda-terms, the completion produces
 \begin{center}
 \begin{tabular}{@ {}l@ {\hspace{-1mm}}}
 \isacommand{nominal\_datatype} @{text lam} =\\
 \hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"}
 The ``raw'' datatype definition can be obtained by stripping off the
 binding clauses and the labels from 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 the user. In our implementation we just use the affix ``@{text "_raw"}''.
 But for the purpose of this paper, we use the superscript @{text "_\<^sup>\<alpha>"} to indicate
-that a notion is defined over $\alpha$-equivalence classes and leave it out
+that a notion is given for $\alpha$-equivalence classes and leave it out
-for the corresponding notion defined on the ``raw'' level. So for example
+for the corresponding notion given 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}
 "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 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{center}
+%\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{center}
+%\end{center}
+%
-\noindent
+%\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
 @{text "D"} stands for the set of free atoms of the bodies, @{text B} for the
 (see \eqref{fvars}); otherwise we set @{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
 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{center}
-\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
+%\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-@{text "bn_atom a"} & @{text "\<equiv>"} & @{text "{atom a}"}\\
+%@{text "bn_atom a"} & @{text "\<equiv>"} & @{text "{atom a}"}\\
-@{text "bn_atom_set as"} & @{text "\<equiv>"} & @{text "atoms as"}\\
+%@{text "bn_atom_set as"} & @{text "\<equiv>"} & @{text "atoms as"}\\
-@{text "bn_atom_list as"} & @{text "\<equiv>"} & @{text "atoms (set as)"}
+%@{text "bn_atom_list as"} & @{text "\<equiv>"} & @{text "atoms (set as)"}
-\end{tabular}
+%\end{tabular}
+%\end{center}
+%
+\begin{center}
+@{text "bn_atom a \<equiv> {atom a}"}\hspace{17mm}
+@{text "bn_atom_set as \<equiv> atoms as"}\\
+@{text "bn_atom_list as \<equiv> atoms (set as)"}
 \end{center}
 \noindent
 Like the function @{text atom}, the function @{text "atoms"} coerces
 a set of atoms to a set of the generic atom type. It is defined as
 \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}
+%\begin{center}
-@{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}
+\mbox{@{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}}
-\end{center}
+%\end{center}
+%
-\noindent
+%\noindent
 with @{text "l"}$_{1..r}$ $\subseteq$ @{text "b"}$_{1..p}$ and none of the
 @{text "l"}$_{1..r}$ being among the bodies @{text
 "d"}$_{1..q}$. The set @{text "B'"} is defined as
 %
 \begin{center}
 the set of atoms that are left unbound by the binding functions @{text
 "bn"}$_{1..m}$. We used for the definition of
 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}
+%\begin{center}
 @{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
-\end{center}
+%\end{center}
+%
-\noindent
+%\noindent
 where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$. For each of
 the arguments we calculate the free atoms as follows:
 %
 \begin{center}
-\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
+\begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}}
 $\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"} 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 sets.
 To see how these definitions work in practice, let us reconsider the
 term-constructors @{text "Let"} and @{text "Let_rec"} shown in
 free in @{text "as"}. This is
 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 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
+%Like the function @{text "bn"}, the function @{text "fa\<^bsub>bn\<^esub>"} traverses the
-list of assignments, but instead returns the free atoms, which means in this
+%list of assignments, but instead returns the free atoms, which means in this
-example the free atoms in the argument @{text "t"}.
+%example the free atoms in the argument @{text "t"}.
 An interesting point in this
 example is that a ``naked'' assignment (@{text "ANil"} or @{text "ACons"}) does not bind any
 atoms, even if the binding function is specified over assignments.
 Only in the context of a @{text Let} or @{text "Let_rec"}, where the binding clauses are given, will
 $\alpha$-equivalence.
 Next we define the $\alpha$-equivalence relations for the raw types @{text
 "ty"}$_{1..n}$ from the specification. We write them as
 %
-\begin{center}
+%\begin{center}
 @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}.
-\end{center}
+%\end{center}
+%
-\noindent
+%\noindent
 Like with the free-atom functions, we also need to
 define auxiliary $\alpha$-equivalence relations
 %
-\begin{center}
+%\begin{center}
 @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}
-\end{center}
+%\end{center}
+%
-\noindent
+%\noindent
 for the binding functions @{text "bn"}$_{1..m}$,
 To simplify our definitions we will use the following abbreviations for
 \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,.., x\<^isub>n) (R\<^isub>1,.., R\<^isub>n) (x\<PRIME>\<^isub>1,.., x\<PRIME>\<^isub>n)"} & @{text "\<equiv>"} & \\
+@{text "(x\<^isub>1,.., x\<^isub>n) (R\<^isub>1,.., R\<^isub>n) (x\<PRIME>\<^isub>1,.., x\<PRIME>\<^isub>n)"} & @{text "\<equiv>"} &
-\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"}}\\
+@{text "x\<^isub>1 R\<^isub>1 x\<PRIME>\<^isub>1 \<and> .. \<and> x\<^isub>n R\<^isub>n x\<PRIME>\<^isub>n"}\\
 @{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{tabular}
 \end{center}
 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}
+%\begin{center}
-@{text "d\<^isub>1 R\<^isub>1 d\<PRIME>\<^isub>1  \<dots> d\<^isub>q R\<^isub>q d\<PRIME>\<^isub>q"}
+@{text "d\<^isub>1 R\<^isub>1 d\<PRIME>\<^isub>1  \<dots> d\<^isub>q R\<^isub>q d\<PRIME>\<^isub>q"}.
-\end{center}
+%\end{center}
+%
-\noindent
+%\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}
 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
 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}
+%\begin{center}
 @{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}.
-\end{center}
+%\end{center}
+%
-\noindent
+%\noindent
 The tuple @{text L} is then @{text "(l\<^isub>1,\<dots>,l\<^isub>r)"} (similarly @{text "L'"})
 and the compound equivalence relation @{text "R'"} is @{text "(\<approx>bn\<^isub>1,\<dots>,\<approx>bn\<^isub>r)"}.
 All premises for @{text "bc\<^isub>i"} are then given by
 %
 \begin{center}
 \noindent
 The auxiliary $\alpha$-equivalence relations @{text "\<approx>bn"}$_{1..m}$
 in @{text "R'"} are defined as follows: assuming a @{text bn}-clause is of the form
 %
-\begin{center}
+%\begin{center}
 @{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
-\end{center}
+%\end{center}
+%
-\noindent
+%\noindent
 where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$,
 then the corresponding $\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"}}
 \noindent
 In this clause the relations @{text "R"}$_{1..s}$ are given by
 \begin{center}
-\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
+\begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}}
 $\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}
 \end{tabular}
 \end{center}
 \begin{center}
 \begin{tabular}{@ {}c @ {}}
-\infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\smallskip\\
+\infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\hspace{9mm}
 \infer{@{text "ACons a t as \<approx>\<^bsub>assn\<^esub> ACons a' t' as"}}
 {@{text "a = a'"} & @{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>assn\<^esub> as'"}}
 \end{tabular}
 \end{center}
 \begin{center}
 \begin{tabular}{@ {}c @ {}}
-\infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\smallskip\\
+\infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\hspace{9mm}
 \infer{@{text "ACons a t as \<approx>\<^bsub>bn\<^esub> ACons a' t' as"}}
 {@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}
 \end{tabular}
 \end{center}
 \noindent
 Note the difference between  $\approx_{\textit{assn}}$ and
 $\approx_{\textit{bn}}$: the latter only ``tracks'' $\alpha$-equivalence of
 the components in an assignment that are \emph{not} bound. This is needed in the
 in the clause for @{text "Let"} (which is has
-a non-recursive binder). The underlying reason is that the terms inside an assignment are not meant
+a non-recursive binder).
-to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"},
+%The underlying reason is that the terms inside an assignment are not meant
-because there all components of an assignment are ``under'' the binder.
+%to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"},
+%because there all components of an assignment are ``under'' the binder.
 *}
 section {* Establishing the Reasoning Infrastructure *}
 text {*

changeset 2510	734341a79028
parent 2509	679cef364022
child 2511	2ccf3086142b