nominal2: comparison LMCS-Paper/Paper.thy

equal deleted inserted replaced

-:4df720c9b660
+:4baa2fccfb61
 Abs_print :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
 definition
 "equal \<equiv> (op =)"
+fun alpha_set_ex where
+"alpha_set_ex (bs, x) R f (cs, y) = (\<exists>pi. alpha_set (bs, x) R f pi (cs, y))"
+fun alpha_res_ex where
+"alpha_res_ex (bs, x) R f pi (cs, y) = (\<exists>pi. alpha_res (bs, x) R f pi (cs, y))"
+fun alpha_lst_ex where
+"alpha_lst_ex (bs, x) R f pi (cs, y) = (\<exists>pi. alpha_lst (bs, x) R f pi (cs, y))"
 notation (latex output)
 swap ("'(_ _')" [1000, 1000] 1000) and
 fresh ("_ # _" [51, 51] 50) and
 fresh_star ("_ #\<^sup>* _" [51, 51] 50) and
 supp ("supp _" [78] 73) and
 uminus ("-_" [78] 73) and
 If  ("if _ then _ else _" 10) and
-alpha_set ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and
+alpha_set_ex ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _\<^esup> _") and
-alpha_lst ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and
+alpha_lst_ex ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _\<^esup> _") and
-alpha_res ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set+}}$}}>\<^bsup>_, _, _\<^esup> _") and
+alpha_res_ex ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set+}}$}}>\<^bsup>_, _\<^esup> _") and
 abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
 abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup>  _") and
 fv ("fa'(_')" [100] 100) and
 equal ("=") and
 alpha_abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
 @{text \<pi>} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
 requirements {\it (i)} to {\it (iv)} can be stated formally as the conjunction of:
 \begin{defi}[Alpha-Equivalence for Set-Bindings]\label{alphaset}\mbox{}\\
 \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}
-@{term "(as, x) \<approx>set R fa \<pi> (bs, y)"}\hspace{2mm}@{text "\<equiv>"}
+@{term "alpha_set_ex (as, x) R fa (bs, y)"}\hspace{2mm}@{text "\<equiv>"} &
+\multicolumn{2}{@ {}l}{if there exists a @{text "\<pi>"} such that:}\\
 & \mbox{\it (i)}   & @{term "fa(x) - as = fa(y) - bs"}\\
 & \mbox{\it (ii)}  & @{term "(fa(x) - as) \<sharp>* \<pi>"}\\
 & \mbox{\it (iii)} &  @{text "(\<pi> \<bullet> x) R y"} \\
 & \mbox{\it (iv)}  & @{term "(\<pi> \<bullet> as) = bs"} \\
 \end{tabular}
 \end{defi}
 \noindent
-Note that this relation depends on the permutation @{text
+Note that the relation is
-"\<pi>"}; alpha-equivalence between two pairs is then the relation where we
-existentially quantify over this @{text "\<pi>"}. Also note that the relation is
 dependent on a free-atom function @{text "fa"} and a relation @{text
 "R"}. The reason for this extra generality is that we will use
 $\approx_{\,\textit{set}}$ for both ``raw'' terms and alpha-equated terms. In
 the latter case, @{text R} will be replaced by equality @{text "="} and we
 will prove that @{text "fa"} is equal to @{text "supp"}.
 for pairs of the form \mbox{@{text "(as, x)"}} with type @{text "(atom list) \<times> \<beta>"}
 as follows
 \begin{defi}[Alpha-Equivalence for List-Bindings]\label{alphalist}\mbox{}\\
 \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}
-@{term "(as, x) \<approx>lst R fa \<pi> (bs, y)"}\hspace{2mm}@{text "\<equiv>"}
+@{term "alpha_lst_ex (as, x) R fa (bs, y)"}\hspace{2mm}@{text "\<equiv>"} &
+\multicolumn{2}{@ {}l}{if there exists a @{text "\<pi>"} such that:}\\
 & \mbox{\it (i)}   & @{term "fa(x) - (set as) = fa(y) - (set bs)"}\\
 & \mbox{\it (ii)}  & @{term "(fa(x) - set as) \<sharp>* \<pi>"}\\
 & \mbox{\it (iii)} & @{text "(\<pi> \<bullet> x) R y"}\\
 & \mbox{\it (iv)}  & @{term "(\<pi> \<bullet> as) = bs"}\\
 \end{tabular}
 also allow vacuous binders, that means \emph{restrict} names, then we keep sets of binders, but drop
 condition {\it (iv)} in Definition~\ref{alphaset}:
 \begin{defi}[Alpha-Equivalence for Set+-Bindings]\label{alphares}\mbox{}\\
 \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}
-@{term "(as, x) \<approx>res R fa \<pi> (bs, y)"}\hspace{2mm}@{text "\<equiv>"}
+@{term "alpha_res_ex (as, x) R fa (bs, y)"}\hspace{2mm}@{text "\<equiv>"} &
+\multicolumn{2}{@ {}l}{if there exists a @{text "\<pi>"} such that:}\\
 & \mbox{\it (i)}   & @{term "fa(x) - as = fa(y) - bs"}\\
 & \mbox{\it (ii)}  & @{term "(fa(x) - as) \<sharp>* \<pi>"}\\
 & \mbox{\it (iii)} & @{text "(\<pi> \<bullet> x) R y"}\\
 \end{tabular}
 \end{defi}
 permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal
 (similarly for $\approx_{\,\textit{list}}$).  It can also relatively easily be
 shown that all three notions of alpha-equivalence coincide, if we only
 abstract a single atom.
-In the rest of this section we are going to introduce three abstraction
+In the rest of this section we are going to show that the alpha-equivalences really
-types. For this we define the relations
+lead to abstractions where some atoms are bound.  For this we are going to introduce
+three abstraction types that are quotients with respect to the relations
 \begin{equation}
 \begin{array}{r}
-@{term "alpha_abs_set (as, x) (bs, y) \<equiv> \<exists>\<pi>. alpha_set (as, x) equal supp \<pi> (bs, y)"}\\
+@{term "alpha_abs_set (as, x) (bs, y)"}~~@{text "\<equiv>"}~~@{term "alpha_set_ex (as, x) equal supp (bs, y)"}\\
-@{term "alpha_abs_res (as, x) (bs, y) \<equiv> \<exists>\<pi>. alpha_res (as, x) equal supp \<pi> (bs, y)"}\\
+@{term "alpha_abs_res (as, x) (bs, y)"}~~@{text "\<equiv>"}~~@{term "alpha_res_ex (as, x) equal supp (bs, y)"}\\
-@{term "alpha_abs_lst (as, x) (bs, y) \<equiv> \<exists>\<pi>. alpha_lst (as, x) equal supp \<pi> (bs, y)"}\\
+@{term "alpha_abs_lst (as, x) (bs, y)"}~~@{text "\<equiv>"}~~@{term "alpha_lst_ex (as, x) equal supp (bs, y)"}\\
 \end{array}
 \end{equation}\smallskip
 \noindent
-We can show that these relations are equivalence
+In these relation we replaced the free-atom function @{text "fa"} with @{term "supp"} and the
-relations and equivariant.
+relation @{text R} with equality. We can show the following properties:
 \begin{lem}\label{alphaeq}
-The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$
+The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_set+}}$
-and $\approx_{\,\textit{abs\_set+}}$ are equivalence relations and equivariant.
+and $\approx_{\,\textit{abs\_list}}$ are equivalence relations and equivariant.
 \end{lem}
 \begin{proof}
 Reflexivity is by taking @{text "\<pi>"} to be @{text "0"}. For symmetry we have
 a permutation @{text "\<pi>"} and for the proof obligation take @{term "- \<pi>"}. In case
 of transitivity, we have two permutations @{text "\<pi>\<^isub>1"} and @{text "\<pi>\<^isub>2"}, and for the
 proof obligation use @{text "\<pi>\<^isub>1 + \<pi>\<^isub>2"}. Equivariance means
 @{term "abs_set (\<pi> \<bullet> as, \<pi> \<bullet> x) (\<pi> \<bullet> bs, \<pi> \<bullet> y)"} holds provided
-@{term "abs_set (as, x) (bs, y)"}. To show this, we need to unfold the
+\mbox{@{term "abs_set (as, x) (bs, y)"}} holds. To show this, we need to unfold the
 definitions and `pull out' the permutations, which is possible since all
 operators, such as @{text "#\<^sup>*, -, set"} and @{text "supp"}, are equivariant
-(see \cite{HuffmanUrban10}).
+(see \cite{HuffmanUrban10}). Finally we apply the permutation operation on booleans.
 \end{proof}
 \noindent
 This lemma allows us to use our quotient package for introducing
 new types @{text "\<beta> abs\<^bsub>set\<^esub>"}, @{text "\<beta> abs\<^bsub>set+\<^esub>"} and @{text "\<beta> abs\<^bsub>list\<^esub>"}
 \end{array}
 \]\smallskip
 \end{thm}
 \noindent
-In effect, this theorem states that the bound names do not appear in the support
+In effect, this theorem states that the atoms @{text "as"} are bound in the
-of abstractions. This can be seen as test that our Definitions \ref{alphaset}, \ref{alphalist}
+abstraction. As stated earlier, this can be seen as test that our
-and \ref{alphares} capture the idea of alpha-equivalence relations.
+Definitions \ref{alphaset}, \ref{alphalist} and \ref{alphares} capture the
-Below we will show the first equation of Theorem \ref{suppabs}. The others follow by similar
+idea of alpha-equivalence relations. Below we will give the proof for the
-arguments. By definition of the abstraction type @{text "abs\<^bsub>set\<^esub>"} we have
+first equation of Theorem \ref{suppabs}. The others follow by similar
+arguments. By definition of the abstraction type @{text
+"abs\<^bsub>set\<^esub>"} we have
 \begin{equation}\label{abseqiff}
 @{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\;\text{if and only if}\;\;\;
-@{term "\<exists>\<pi>. alpha_set (as, x) equal supp \<pi> (bs, y)"}
+@{term "alpha_set_ex (as, x) equal supp (bs, y)"}
 \end{equation}\smallskip
 \noindent
 and also
 \end{lem}
 \begin{proof}
 This lemma is straightforward using \eqref{abseqiff} and observing that
 the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.
+We therefore can use as permutation the swapping @{term "(a \<rightleftharpoons> b)"}.
 \end{proof}
 \noindent
 Assuming that @{text "x"} has finite support, this lemma together
 with \eqref{absperm} allows us to show
 \[
 @{term "supp (supp_set (Abs_set as x)) \<subseteq> supp (Abs_set as x)"}
 \]\smallskip
 \noindent
-using fact about function applications in \eqref{supps}. Assuming
+using the fact about the support of function applications in \eqref{supps}. Assuming
 @{term "supp x - as"} is a finite set, we further obtain
 \begin{equation}\label{halftwo}
 @{thm (concl) Abs_supp_subset1(1)[no_vars]}
 \end{equation}\smallskip
 \noindent
-since for every finite sets of atoms, say @{text "bs"}, we have
+This is because for every finite sets of atoms, say @{text "bs"}, we have
 @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
 Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes
 Theorem~\ref{suppabs}.
 The method of first considering abstractions of the form @{term "Abs_set as
 and by the syntax of the
 Ott-tool \cite{ott-jfp}. For us a specification of a term-calculus is a
 collection of (possibly mutual recursive) type declarations, say @{text
 "ty\<AL>\<^isub>1, \<dots>, ty\<AL>\<^isub>n"}, and an associated collection of
 binding functions, say @{text "bn\<AL>\<^isub>1, \<dots>, bn\<AL>\<^isub>m"}. The
-syntax in Nominal Isabelle for such specifications is roughly as follows:
+syntax in Nominal Isabelle for such specifications is schematically as follows:
 \begin{equation}\label{scheme}
 \mbox{\begin{tabular}{@ {}p{2.5cm}l}
 type \mbox{declaration part} &
 $\begin{cases}
 \isacommand{nominal\_datatype} @{text "ty\<AL>\<^isub>1 = \<dots>"}\\
 \isacommand{and} @{text "ty\<AL>\<^isub>2 = \<dots>"}\\
 \raisebox{2mm}{$\ldots$}\\[-2mm]
 \isacommand{and} @{text "ty\<AL>\<^isub>n = \<dots>"}\\
 \end{tabular}}
-\end{cases}$\\
+\end{cases}$\\[2mm]
 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}\\
 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 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
+\emph{one} binding clause of a term constructor. So for example
-atoms of a body cannot be free at the same time by specifying an alternative
-binder for the same body).
+\[\mbox{
+@{text "Foo x::name y::name t::trm"}\hspace{3mm}
+\isacommand{binds} @{text "x"} \isacommand{in} @{text "t"},
+\isacommand{binds} @{text "y"} \isacommand{in} @{text "t"}}
+\]\smallskip
+\noindent
+is not allowed. 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 labels. The restriction we need to impose on them
 is that in case of \isacommand{binds (set)} and \isacommand{binds (set+)} the
 labels must either refer to atom types or to sets of atom types; in case of
 \]\smallskip
 \noindent
 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
+"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{binds (set)} or \isacommand{binds}
+@{text name}. However, having \isacommand{binds (set)} or just \isacommand{binds}
 in the second case makes a 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
 notions of free-atoms and alpha-equivalence.
 To make sure that atoms bound by deep binders cannot be free at the
 same time, we cannot have more than one binding function for a deep binder.
 Consequently we exclude specifications such as
-%
-\begin{center}
+\[\mbox{
 \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
 @{text "Baz\<^isub>1 p::pat t::trm"} &
 \isacommand{binds} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\
 @{text "Baz\<^isub>2 p::pat t\<^isub>1::trm t\<^isub>2::trm"} &
 \isacommand{binds} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "t\<^isub>1"},
 \isacommand{binds} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "t\<^isub>2"}\\
-\end{tabular}
+\end{tabular}}
-\end{center}
+\]\smallskip
 \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"}.
 (Since the Ott-tool does not derive a reasoning infrastructure for
 alpha-equated terms with deep binders, it can permit such specifications.)
-We also need to restrict the form of the binding functions in order
+We also need to restrict the form of the binding functions in order to
-to ensure the @{text "bn"}-functions can be defined for alpha-equated
+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
+terms. The main restriction is that we cannot return an atom in a binding
-bound in the corresponding term-constructor. That means in \eqref{letpat}
+function that is also bound in the corresponding term-constructor.
-that the term-constructors @{text PVar} and @{text PTup} may
+Consider again the specification for @{text "trm"} and a contrived
-not have a binding clause (all arguments are used to define @{text "bn"}).
+version for assignments, @{text "assn"}:
-In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons}
-may have a binding clause involving the argument @{text trm} (the only one that
+\begin{equation}\label{bnexp}
-is \emph{not} used in the definition of the binding function). This restriction
+\mbox{%
-is sufficient for lifting the binding function to alpha-equated terms.
+\begin{tabular}{@ {}l@ {}}
+\isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\
-In the version of
+\isacommand{and} @{text "assn"} $=$\\
-Nominal Isabelle described here, we also adopted the restriction from the
+\hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\
-Ott-tool that binding functions can only return: the empty set or empty list
+\hspace{5mm}$\mid$~@{text "ACons x::name y::name t::trm assn"}
-(as in case @{text PNil}), a singleton set or singleton list containing an
+\;\;\isacommand{binds} @{text "y"} \isacommand{in} @{text t}\\
-atom (case @{text PVar}), or unions of atom sets or appended atom lists
+\isacommand{binder} @{text "bn::assn \<Rightarrow> atom list"}\\
-(case @{text PTup}). This restriction will simplify some automatic definitions and proofs
+\isacommand{where}~@{text "bn(ANil) = []"}\\
-later on.
+\hspace{5mm}$\mid$~@{text "bn(ACons x y t as) = [atom x] @ bn(as)"}\\
+\end{tabular}}
+\end{equation}\smallskip
+\noindent
+In this example the term constructor @{text "ACons"} contains a binding
+clause, and also is used in the definition of the binding function. The
+restriction we have to impose is that the binding function can only return
+free atoms, that is the ones that are not mentioned in a binding clause.
+Therefore @{text "y"} cannot be used in the binding function, @{text "bn"}
+(since it is bound in @{text "ACons"} by the binding clause), but @{text x}
+can (since it is a free atom). This restriction is sufficient for lifting
+the binding function to alpha-equated terms. If we would allow that @{text "bn"}
+can return also @{text "y"}, then it would not be respectful and therefore
+cannot be lifted.
+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 ANil}), a singleton set or
+singleton list containing an atom (case @{text PVar} in \eqref{letpat}), or
+unions of atom sets or appended atom lists (case @{text ACons}). This
+restriction will simplify some automatic definitions and proofs later on.
 In order to simplify our definitions of free atoms and alpha-equivalence,
 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{binds}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case
 of the lambda-terms, the completion produces
-\begin{center}
+\[\mbox{
 \begin{tabular}{@ {}l@ {\hspace{-1mm}}}
 \isacommand{nominal\_datatype} @{text lam} =\\
 \hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"}
 \;\;\isacommand{binds}~@{term "{}"}~\isacommand{in}~@{text "x"}\\
 \hspace{5mm}$\mid$~@{text "App t\<^isub>1::lam t\<^isub>2::lam"}
 \;\;\isacommand{binds}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>1 t\<^isub>2"}\\
 \hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}
 \;\;\isacommand{binds}~@{text x} \isacommand{in} @{text t}\\
-\end{tabular}
+\end{tabular}}
-\end{center}
+\]\smallskip
 \noindent
 The point of completion is that we can make definitions over the binding
 clauses and be sure to have captured all arguments of a term constructor.
 *}
 section {* Alpha-Equivalence and Free Atoms\label{sec:alpha} *}
 text {*
 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
+establish a reasoning infrastructure for them. As Pottier and Cheney pointed
-Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, just
+out \cite{Cheney05,Pottier06}, just re-arranging the arguments of
-re-arranging the arguments of
+term-constructors so that binders and their bodies are next to each other
-term-constructors so that binders and their bodies are next to each other will
+will result in inadequate representations in cases like \mbox{@{text "Let
-result in inadequate representations in cases like @{text "Let x\<^isub>1 = t\<^isub>1\<dots>x\<^isub>n = t\<^isub>n in s"}.
+x\<^isub>1 = t\<^isub>1\<dots>x\<^isub>n = t\<^isub>n in s"}}. Therefore we will
-Therefore we will first
+first extract ``raw'' datatype definitions from the specification and then
-extract ``raw'' datatype definitions from the specification and then define
+define explicitly an alpha-equivalence relation over them. We subsequently
-explicitly an alpha-equivalence relation over them. We subsequently
 construct the quotient of the datatypes according to our alpha-equivalence.
 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"}''.
 in Isabelle/HOL).
 We subsequently define each of the user-specified binding
 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)"}
+@{text "\<pi> \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (\<pi> \<bullet> z\<^isub>1) \<dots> (\<pi> \<bullet> z\<^isub>n)"}
-\end{equation}
+\end{equation}\smallskip
 The first non-trivial step we have to perform is the generation of
-free-atom functions from the specification. For the
+\emph{free-atom functions} from the specification.\footnote{Admittedly, the
+details of our definitions are somewhat involved. However they are still
+conceptually simple in comparison with the ``positional'' approach taken in
+Ott \cite[Pages 88--95]{ott-jfp}, which uses \emph{occurences} and
+\emph{partial equivalence relations} over sets of occurences.} For the
 \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions
 \begin{equation}\label{fvars}
 \mbox{@{text "fa_ty"}$_{1..n}$}
-\end{equation}
+\end{equation}\smallskip
 \noindent
 by recursion.
 We define these functions together with auxiliary free-atom functions for
 the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$
 we define
-\begin{center}
+\[
-@{text "fa_bn"}$_{1..m}$.
+@{text "fa_bn"}\mbox{$_{1..m}$}.
-\end{center}
+\]\smallskip
 \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 free atoms in a deep binder.
 "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{binds (set)} (the other modes are similar).
 Suppose the binding clause @{text bc\<^isub>i} is of the form
-\begin{center}
+\[
 \mbox{\isacommand{binds (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
-\end{center}
+\]\smallskip
 \noindent
-in which the body-labels @{text "d"}$_{1..q}$ refer to types @{text ty}$_{1..q}$,
+in which the body-labels @{text "d"}$_{1..q}$ refer to types @{text
-and the binders @{text b}$_{1..p}$
+ty}$_{1..q}$, and the binders @{text b}$_{1..p}$ either refer to labels of
-either refer to labels of atom types (in case of shallow binders) or to binding
+atom types (in case of shallow binders) or to binding functions taking a
-functions taking a single label as argument (in case of deep binders). Assuming
+single label as argument (in case of deep binders). Assuming @{text "D"}
-@{text "D"} stands for the set of free atoms of the bodies, @{text B} for the
+stands for the set of free atoms of the bodies, @{text B} for the set of
-set of binding atoms in the binders and @{text "B'"} for the set of free atoms in
+binding atoms in the binders and @{text "B'"} for the set of free atoms in
-non-recursive deep binders,
+non-recursive deep binders, then the free atoms of the binding clause @{text
-then the free atoms of the binding clause @{text bc\<^isub>i} are\\[-2mm]
+bc\<^isub>i} are
-%
 \begin{equation}\label{fadef}
 \mbox{@{text "fa(bc\<^isub>i) \<equiv> (D - B) \<union> B'"}}.
-\end{equation}
+\end{equation}\smallskip
-%
 \noindent
 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}
+\]\smallskip
 \noindent
 where in case @{text "d\<^isub>i"} refers to one of the raw types @{text "ty"}$_{1..n}$ from the
 specification, the function @{text "fa_ty\<^isub>i"} is the corresponding free-atom function
-we are defining by recursion;
+we are defining by recursion; otherwise we set \mbox{@{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}}. The reason
-(see \eqref{fvars});
+for the latter choice is that @{text "ty"}$_i$ is not a type that is part of the specification, and
-otherwise we set @{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
+we assume @{text supp} is the generic notion that characterises the free variables of
+a type (in fact in the next section we will show that the free-variable functions we
+define here, are equal to the support once lifted to alpha-equivalence classes).
 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\\[-4mm]
-\begin{center}
+\[\mbox{
 \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-@{text "bn_atom a"} & @{text "\<equiv>"} & @{text "{atom a}"}\\
+@{text "bn\<^bsub>atom\<^esup> a"} & @{text "\<equiv>"} & @{text "{atom a}"}\\
-@{text "bn_atom_set as"} & @{text "\<equiv>"} & @{text "atoms as"}\\
+@{text "bn\<^bsub>atom_set\<^esup> as"} & @{text "\<equiv>"} & @{text "atoms as"}\\
-@{text "bn_atom_list as"} & @{text "\<equiv>"} & @{text "atoms (set as)"}
+@{text "bn\<^bsub>atom_list\<^esub> as"} & @{text "\<equiv>"} & @{text "atoms (set as)"}
-\end{tabular}
+\end{tabular}}
-\end{center}
+\]\smallskip
-\begin{center}
-@{text "bn\<^bsub>atom\<^esub> a \<equiv> {atom a}"}\hfill
-@{text "bn\<^bsub>atom_set\<^esub> as \<equiv> atoms as"}\hfill
-@{text "bn\<^bsub>atom_list\<^esub> 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  @{text "atoms as \<equiv> {atom a | a \<in> as}"}.
-The set @{text B} is then formally defined as\\[-4mm]
+The set @{text B} is then formally defined as
-%
-\begin{center}
+\begin{equation}\label{bdef}
 @{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> ... \<union> bn_ty\<^isub>p b\<^isub>p"}
-\end{center}
+\end{equation}\smallskip
-%
 \noindent
-where we use the auxiliary binding functions for shallow binders.
+where we use the auxiliary binding functions for shallow binders (that means
-The set @{text "B'"} collects all free atoms in non-recursive deep
+when @{text "ty"}$_i$ is of type @{text "atom"}, @{text "atom set"} or
-binders. Let us assume these binders in @{text "bc\<^isub>i"} are
+@{text "atom list"}). The set @{text "B'"} collects all free atoms in
+non-recursive deep binders. Let us assume these binders in the binding
-\begin{center}
+clause @{text "bc\<^isub>i"} are
+\[
 \mbox{@{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}}
-\end{center}
+\]\smallskip
 \noindent
-with @{text "l"}$_{1..r}$ $\subseteq$ @{text "b"}$_{1..p}$ and none of the
+with @{text "l"}$_{1..r}$ $\subseteq$ @{text "b"}$_{1..p}$ (see
-@{text "l"}$_{1..r}$ being among the bodies @{text
+\eqref{bdef}) and none of the @{text "l"}$_{1..r}$ being among the bodies
-"d"}$_{1..q}$. The set @{text "B'"} is defined as\\[-5mm]
+@{text "d"}$_{1..q}$. The set @{text "B'"} is defined as
-%
-\begin{center}
+\begin{equation}\label{bprimedef}
-@{text "B' \<equiv> fa_bn\<^isub>1 l\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r l\<^isub>r"}\\[-9mm]
+@{text "B' \<equiv> fa_bn\<^isub>1 l\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r l\<^isub>r"}
-\end{center}
+\end{equation}\smallskip
-%
 \noindent
 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 in \eqref{fadef}
 the set of atoms that are left unbound by the binding functions @{text
-"bn"}$_{1..m}$. We used for the definition of
+"bn"}$_{1..m}$, see also the definition in \eqref{bprimedef}. We used for
-this set the functions @{text "fa_bn"}$_{1..m}$, which are also defined by mutual
+the definition of this set the functions @{text "fa_bn"}$_{1..m}$. The
-recursion. Assume the user specified a @{text bn}-clause of the form
+definition for those functions needs to be extracted from the clauses the
+user provided for @{text "bn"}$_{1..m}$ Assume the user specified a @{text
-\begin{center}
+bn}-clause of the form
+\[
 @{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
-\end{center}
+\]\smallskip
 \noindent
-where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$. For each of
+where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$. For
-the arguments we calculate the free atoms as follows:
+each of the arguments we calculate the free atoms as follows:
-\begin{center}
+\[\mbox{
 \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"}
+$\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),\\
+& (that means nothing is bound in @{text "z\<^isub>i"} by the binding function),\smallskip\\
 $\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\\
+with the recursive call @{text "bn\<^isub>i z\<^isub>i"}, and\smallskip\\
 $\bullet$ & @{term "{}"} provided @{text "z\<^isub>i"} occurs in  @{text "rhs"},
-but without a recursive call.
+but without a recursive call\\
-\end{tabular}
+& (that means @{text "z\<^isub>i"} is supposed to become bound by the binding function)\\
-\end{center}
+\end{tabular}}
+\]\smallskip
 \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
 \eqref{letrecs} together with the term-constructors for assignments @{text
 "ANil"} and @{text "ACons"}. Since there is a binding function defined for
 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}
+\[\mbox{
 \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>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fa\<^bsub>assn\<^esub> as \<union> fa\<^bsub>trm\<^esub> t) - set (bn as)"}\smallskip\\
 @{text "fa\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
-@{text "fa\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(supp a) \<union> (fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>assn\<^esub> as)"}\\[1mm]
+@{text "fa\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(supp a) \<union> (fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>assn\<^esub> as)"}\smallskip\\
 @{text "fa\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
 @{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{tabular}}
-\end{center}
+\]\smallskip
-\noindent
-Recall that @{text ANil} and @{text "ACons"} have no
+\noindent
-binding clause in the specification. The corresponding free-atom
+Recall that @{text ANil} and @{text "ACons"} have no binding clause in the
-function @{text "fa\<^bsub>assn\<^esub>"} therefore returns all free atoms
+specification. The corresponding free-atom function @{text
-of an assignment (in case of @{text "ACons"}, they are given in
+"fa\<^bsub>assn\<^esub>"} therefore returns all free atoms of an assignment
-terms of @{text supp}, @{text "fa\<^bsub>trm\<^esub>"} and @{text "fa\<^bsub>assn\<^esub>"}).
+(in case of @{text "ACons"}, they are given in terms of @{text supp}, @{text
-The binding only takes place in @{text Let} and
+"fa\<^bsub>trm\<^esub>"} and @{text "fa\<^bsub>assn\<^esub>"}). The binding
-@{text "Let_rec"}. In case of @{text "Let"}, the binding clause specifies
+only takes place in @{text Let} and @{text "Let_rec"}. In case of @{text
-that all atoms given by @{text "set (bn as)"} have to be bound in @{text
+"Let"}, the binding clause specifies that all atoms given by @{text "set (bn
-t}. Therefore we have to subtract @{text "set (bn as)"} from @{text
+as)"} have to be bound in @{text t}. Therefore we have to subtract @{text
-"fa\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are
+"set (bn as)"} from @{text "fa\<^bsub>trm\<^esub> t"}. However, we also need
-free in @{text "as"}. This is
+to add all atoms that are free in @{text "as"}. This is in contrast with
-in contrast with @{text "Let_rec"} where we have a recursive
+@{text "Let_rec"} where we have a recursive binder to bind all occurrences
-binder to bind all occurrences of the atoms in @{text
+of the atoms in @{text "set (bn as)"} also inside @{text "as"}. Therefore we
-"set (bn as)"} also inside @{text "as"}. Therefore we have to subtract
+have to subtract @{text "set (bn as)"} from both @{text
-@{text "set (bn as)"} from both @{text "fa\<^bsub>trm\<^esub> t"} and @{text "fa\<^bsub>assn\<^esub> as"}.
+"fa\<^bsub>trm\<^esub> t"} and @{text "fa\<^bsub>assn\<^esub> as"}. Like the
-Like the function @{text "bn"}, the function @{text "fa\<^bsub>bn\<^esub>"} traverses the
+function @{text "bn"}, the function @{text "fa\<^bsub>bn\<^esub>"} traverses
-list of assignments, but instead returns the free atoms, which means in this
+the list of assignments, but instead returns the free atoms, which means in
-example the free atoms in the argument @{text "t"}.
+this 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
+An interesting point in this example is that a ``naked'' assignment (@{text
-atoms, even if the binding function is specified over assignments.
+"ANil"} or @{text "ACons"}) does not bind any atoms, even if the binding
-Only in the context of a @{text Let} or @{text "Let_rec"}, where the binding clauses are given, will
+function is specified over assignments. Only in the context of a @{text Let}
-some atoms actually become bound.  This is a phenomenon that has also been pointed
+or @{text "Let_rec"}, where the binding clauses are given, will some atoms
-out in \cite{ott-jfp}. For us this observation is crucial, because we would
+actually become bound.  This is a phenomenon that has also been pointed out
-not be able to lift the @{text "bn"}-functions to alpha-equated terms if they act on
+in \cite{ott-jfp}. For us this observation is crucial, because we would not
-atoms that are bound. In that case, these functions would \emph{not} respect
+be able to lift the @{text "bn"}-functions to alpha-equated terms if they
-alpha-equivalence.
+act on atoms that are bound. In that case, these functions would \emph{not}
+respect alpha-equivalence.
-Next we define the alpha-equivalence relations for the raw types @{text
-"ty"}$_{1..n}$ from the specification. We write them as
+Having the free atom functions at our disposal, we can next define the
+alpha-equivalence relations for the raw types @{text
-\begin{center}
+"ty"}$_{1..n}$. We write them as
-@{text "\<approx>ty"}$_{1..n}$.
-\end{center}
+\[
+\mbox{@{text "\<approx>ty"}$_{1..n}$}.
+\]\smallskip
 \noindent
 Like with the free-atom functions, we also need to
 define auxiliary alpha-equivalence relations
-\begin{center}
+\[
-@{text "\<approx>bn\<^isub>"}$_{1..m}$
+\mbox{@{text "\<approx>bn\<^isub>"}$_{1..m}$}
-\end{center}
+\]\smallskip
 \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}
+\[\mbox{
 \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-@{text "(x\<^isub>1,\<dots>, x\<^isub>n) (R\<^isub>1,\<dots>, R\<^isub>n) (x\<PRIME>\<^isub>1,\<dots>, x\<PRIME>\<^isub>n)"} & @{text "\<equiv>"} &
+@{text "(x\<^isub>1,\<dots>, x\<^isub>n) (R\<^isub>1,\<dots>, R\<^isub>n) (y\<^isub>1,\<dots>, y\<^isub>n)"} & @{text "\<equiv>"} &
-@{text "x\<^isub>1 R\<^isub>1 x\<PRIME>\<^isub>1 \<and> \<dots> \<and> x\<^isub>n R\<^isub>n x\<PRIME>\<^isub>n"}\\
+@{text "x\<^isub>1 R\<^isub>1 y\<^isub>1 \<and> \<dots> \<and> x\<^isub>n R\<^isub>n y\<^isub>n"}\\
 @{text "(fa\<^isub>1,\<dots>, fa\<^isub>n) (x\<^isub>1,\<dots>, x\<^isub>n)"} & @{text "\<equiv>"} & @{text "fa\<^isub>1 x\<^isub>1 \<union> \<dots> \<union> fa\<^isub>n x\<^isub>n"}\\
-\end{tabular}
+\end{tabular}}
-\end{center}
+\]\smallskip
 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) \<dots> prems(bc\<^isub>k)"}}}
-\end{center}
+\]\smallskip
 \noindent
-The task below is to specify what the premises of a binding clause are. As a
+The task below is to specify what the premises corresponding to a binding
-special instance, we first treat the case where @{text "bc\<^isub>i"} is the
+clause are. To understand better whet the general pattern is, let us first
-empty binding clause of the form
+treat the special instance where @{text "bc\<^isub>i"} is the empty binding clause
+of the form
-\begin{center}
+\[
 \mbox{\isacommand{binds (set)} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
-\end{center}
+\]\smallskip
 \noindent
-In this binding clause no atom is bound and we only have to alpha-relate the bodies. For this
+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
 \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{center}
-\mbox{@{term "P \<equiv> \<exists>p. (B, D) \<approx>set R fa p (B', D')"}}\;.
+\mbox{@{term "P \<equiv> alpha_set_ex (B, D) R fa (B', D')"}}\;.
 \end{center}
 \noindent
 This premise accounts for alpha-equivalence of the bodies of the binding
 clause.
 $\approx_{\textit{bn}}$ with the following clauses:
 \begin{center}
 \begin{tabular}{@ {}c @ {}}
 \infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
-{@{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\
+{@{term "alpha_lst_ex (bn as, t) alpha_trm fa_trm (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\
 \makebox[0mm]{\infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
-{@{term "\<exists>p. (bn as, ast) \<approx>lst alpha_trm2 fa_trm2 p (bn as', ast')"}}}
+{@{term "alpha_lst_ex (bn as, ast) alpha_trm2 fa_trm2 (bn as', ast')"}}}
 \end{tabular}
 \end{center}
 \begin{center}
 \begin{tabular}{@ {}c @ {}}

changeset 3006	4baa2fccfb61
parent 3005	4df720c9b660
child 3007	c5de60da0bcf