nominal2: comparison LMCS-Paper/Paper.thy

equal deleted inserted replaced

-:3c8d3aaf292c
+:8d7d85e915b5
 because also there one would like to bind multiple variables at once.
 Binding multiple variables has interesting properties that cannot be captured
 easily by iterating single binders. For example in the case of type-schemes we do not
 want to make a distinction about the order of the bound variables. Therefore
-we would like to regard below the first pair of type-schemes as alpha-equivalent,
+we would like to regard in \eqref{ex1} below  the first pair of type-schemes as alpha-equivalent,
 but assuming that @{text x}, @{text y} and @{text z} are distinct variables,
 the second pair should \emph{not} be alpha-equivalent:
 \begin{equation}\label{ex1}
 @{text "\<forall>{x, y}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{y, x}. y \<rightarrow> x"}\hspace{10mm}
 from the Ott-tool, but we introduce crucial restrictions, and also extensions, so
 that our specifications make sense for reasoning about alpha-equated terms.
 The main improvement over Ott is that we introduce three binding modes
 (only one is present in Ott), provide formalised definitions for alpha-equivalence and
 for free variables of our terms, and also derive a reasoning infrastructure
-for our specifications from ``first principles''.
+for our specifications from ``first principles'' inside a theorem prover.
 \begin{figure}
 \begin{boxedminipage}{\linewidth}
 \begin{center}
 Pitts \cite{Pitts03}. This adaptation for Isabelle/HOL is described in
 \cite{HuffmanUrban10} (including proofs). We shall briefly review this work
 to aid the description of what follows.
 Two central notions in the nominal logic work are sorted atoms and
-sort-respecting permutations of atoms. We will use the letters @{text "a,
+sort-respecting permutations of atoms. We will use the letters @{text "a, b,
-b, c, \<dots>"} to stand for atoms and @{text "\<pi>, \<dots>"} to stand for
+c, \<dots>"} to stand for atoms and @{text "\<pi>, \<dots>"} to stand for permutations,
-permutations. The purpose of atoms is to represent variables, be they bound or free.
+which in Nominal Isabelle have type @{typ perm}. The purpose of atoms is to
-The sorts of atoms can be used to represent different kinds of
+represent variables, be they bound or free. The sorts of atoms can be used
-variables, such as the term-, coercion- and type-variables in Core-Haskell.
+to represent different kinds of variables, such as the term-, coercion- and
-It is assumed that there is an infinite supply of atoms for each
+type-variables in Core-Haskell.  It is assumed that there is an infinite
-sort. In the interest of brevity, we shall restrict ourselves
+supply of atoms for each sort. In the interest of brevity, we shall restrict
-in what follows to only one sort of atoms.
+ourselves in what follows to only one sort of atoms.
 Permutations are bijective functions from atoms to atoms that are
 the identity everywhere except on a finite number of atoms. There is a
 two-place permutation operation written
 @{text "_ \<bullet> _  ::  perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
 permutation operation and on the notion of equality defined for the type of
 @{text x}, namely:
 \begin{equation}\label{suppdef}
 @{thm supp_def[no_vars, THEN eq_reflection]}
-\end{equation}
+\end{equation}\smallskip
 \noindent
 There is also the derived notion for when an atom @{text a} is \emph{fresh}
 for an @{text x}, defined as
 swapping two fresh atoms, say @{text a} and @{text b}, leaves
 @{text x} unchanged, namely
 \begin{prop}\label{swapfreshfresh}
 If @{thm (prem 1) swap_fresh_fresh[no_vars]} and @{thm (prem 2) swap_fresh_fresh[no_vars]}
-then @{thm (concl) swap_fresh_fresh[no_vars]}
+then @{thm (concl) swap_fresh_fresh[no_vars]}.
 \end{prop}
 While often the support of an object can be relatively easily
 described, for example for atoms, products, lists, function applications,
 booleans and permutations as follows
 only an approximation can be established (as for function applications
 above). Reasoning about such approximations can be simplified with the
 notion \emph{supports}, defined as follows:
 \begin{defi}
-A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}
+A set @{text S} \emph{supports} @{text x}, if for all atoms @{text a} and @{text b}
 not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.
 \end{defi}
 \noindent
 The main point of @{text supports} is that we can establish the following
 two properties.
 \begin{prop}\label{supportsprop}
-Given a set @{text "as"} of atoms.
+Given a set @{text "as"} of atoms.\\
-{\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]}
+{\it (i)} If @{thm (prem 1) supp_is_subset[where S="as", no_vars]}
+and @{thm (prem 2) supp_is_subset[where S="as", no_vars]} then
+@{thm (concl) supp_is_subset[where S="as", no_vars]}.\\
 {\it (ii)} @{thm supp_supports[no_vars]}.
 \end{prop}
 Another important notion in the nominal logic work is \emph{equivariance}.
 For a function @{text f}, say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant
 it is required that every permutation leaves @{text f} unchanged, that is
 \begin{equation}\label{equivariancedef}
-@{term "\<forall>p. p \<bullet> f = f"}
+@{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}
-\end{equation}
+\end{equation}\smallskip
 \noindent or equivalently that a permutation applied to the application
 @{text "f x"} can be moved to the argument @{text x}. That means for equivariant
-functions @{text f}, we have for all permutations @{text p}:
+functions @{text f}, we have for all permutations @{text "\<pi>"}:
 \begin{equation}\label{equivariance}
-@{text "p \<bullet> f = f"} \;\;\;\textit{if and only if}\;\;\;
+@{text "\<pi> \<bullet> f = f"} \;\;\;\;\textit{if and only if}\;\;\;\;
-@{text "p \<bullet> (f x) = f (p \<bullet> x)"}
+@{text "\<pi> \<bullet> (f x) = f (\<pi> \<bullet> x)"}
-\end{equation}
+\end{equation}\smallskip
 \noindent
 From property \eqref{equivariancedef} and the definition of @{text supp}, we
 can easily deduce that equivariant functions have empty support. There is
 also a similar notion for equivariant relations, say @{text R}, namely the property
 that
 \begin{center}
-@{text "x R y"} \;\;\textit{implies}\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}
+@{text "x R y"} \;\;\textit{implies}\;\; @{text "(\<pi> \<bullet> x) R (\<pi> \<bullet> y)"}
 \end{center}
 Using freshness, the nominal logic work provides us with general means for renaming
 binders.
 \noindent
 While in the older version of Nominal Isabelle, we used extensively
-Property~\ref{swapfreshfresh}
+Property~\ref{swapfreshfresh} to rename single binders, this property
-this property to rename single binders, it this property
 proved too unwieldy for dealing with multiple binders. For such binders the
 following generalisations turned out to be easier to use.
 \begin{prop}\label{supppermeq}
-@{thm[mode=IfThen] supp_perm_eq[no_vars]}
+@{thm[mode=IfThen] supp_perm_eq[where p="\<pi>", no_vars]}
 \end{prop}
 \begin{prop}\label{avoiding}
 For a finite set @{text as} and a finitely supported @{text x} with
 @{term "as \<sharp>* x"} and also a finitely supported @{text c}, there
-exists a permutation @{text p} such that @{term "(p \<bullet> as) \<sharp>* c"} and
+exists a permutation @{text "\<pi>"} such that @{term "(\<pi> \<bullet> as) \<sharp>* c"} and
-@{term "supp x \<sharp>* p"}.
+@{term "supp x \<sharp>* \<pi>"}.
 \end{prop}
 \noindent
 The idea behind the second property is that given a finite set @{text as}
 of binders (being bound, or fresh, in @{text x} is ensured by the
-assumption @{term "as \<sharp>* x"}), then there exists a permutation @{text p} such that
+assumption @{term "as \<sharp>* x"}), then there exists a permutation @{text "\<pi>"} such that
-the renamed binders @{term "p \<bullet> as"} avoid @{text c} (which can be arbitrarily chosen
+the renamed binders @{term "\<pi> \<bullet> as"} avoid @{text c} (which can be arbitrarily chosen
-as long as it is finitely supported) and also @{text "p"} does not affect anything
+as long as it is finitely supported) and also @{text "\<pi>"} does not affect anything
-in the support of @{text x} (that is @{term "supp x \<sharp>* p"}). The last
+in the support of @{text x} (that is @{term "supp x \<sharp>* \<pi>"}). The last
 fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders
-@{text as} in @{text x}, because @{term "p \<bullet> x = x"}.
+@{text as} in @{text x}, because @{term "\<pi> \<bullet> x = x"}.
 Most properties given in this section are described in detail in \cite{HuffmanUrban10}
 and all are formalised in Isabelle/HOL. In the next sections we will make
-extensive use of these properties in order to define alpha-equivalence in
+use of these properties in order to define alpha-equivalence in
 the presence of multiple binders.
 *}
 section {* General Bindings\label{sec:binders} *}
 from this specification (remember that Nominal Isabelle is a definitional
 extension of Isabelle/HOL, which does not introduce any new axioms).
 In order to keep our work with deriving the reasoning infrastructure
 manageable, we will wherever possible state definitions and perform proofs
-on the ``user-level'' of Isabelle/HOL, as opposed to write custom ML-code.  that
+on the ``user-level'' of Isabelle/HOL, as opposed to write custom ML-code that
 generates them anew for each specification.
 To that end, we will consider
 first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}.  These pairs
 are intended to represent the abstraction, or binding, of the set of atoms @{text
 "as"} in the body @{text "x"}.
 @{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
-atoms; moreover there must be a permutation @{text p} such that {\it
+atoms; moreover there must be a permutation @{text \<pi>} such that {\it
-(ii)} @{text p} leaves the free atoms of @{text x} and @{text y} unchanged, but
+(ii)} @{text \<pi>} 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
+@{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{equation}\label{alphaset}
+\begin{defi}[Alpha-Equivalence for Set-Bindings]\label{alphaset}\mbox{}\\
-\begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l}
+\begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}
-\multicolumn{4}{l}{@{term "(as, x) \<approx>set R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+@{term "(as, x) \<approx>set R fa \<pi> (bs, y)"}\hspace{2mm}@{text "\<equiv>"}
-\mbox{\it (i)}   & @{term "fa(x) - as = fa(y) - bs"} &
+& \mbox{\it (i)}   & @{term "fa(x) - as = fa(y) - bs"}\\
-\mbox{\it (iii)} &  @{text "(p \<bullet> x) R y"} \\
+& \mbox{\it (ii)}  & @{term "(fa(x) - as) \<sharp>* \<pi>"}\\
-\mbox{\it (ii)}  & @{term "(fa(x) - as) \<sharp>* p"} &
+& \mbox{\it (iii)} &  @{text "(\<pi> \<bullet> x) R y"} \\
-\mbox{\it (iv)}  & @{term "(p \<bullet> as) = bs"} \\
+& \mbox{\it (iv)}  & @{term "(\<pi> \<bullet> as) = bs"} \\
-\end{array}
+\end{tabular}
-\end{equation}
+\end{defi}
-%
 \noindent
 Note that this relation depends on the permutation @{text
-"p"}; alpha-equivalence between two pairs is then the relation where we
+"\<pi>"}; alpha-equivalence between two pairs is then the relation where we
-existentially quantify over this @{text "p"}. Also note that the relation is
+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"}.
-The definition in \eqref{alphaset} does not make any distinction between the
+Definition \ref{alphaset} does not make any distinction between the
 order of abstracted atoms. If we want this, then we can define alpha-equivalence
 for pairs of the form \mbox{@{text "(as, x)"}} with type @{text "(atom list) \<times> \<beta>"}
 as follows
-%
-\begin{equation}\label{alphalist}
+\begin{defi}[Alpha-Equivalence for List-Bindings]\label{alphalist}\mbox{}\\
-\begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l}
+\begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}
-\multicolumn{4}{l}{@{term "(as, x) \<approx>lst R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+@{term "(as, x) \<approx>lst R fa \<pi> (bs, y)"}\hspace{2mm}@{text "\<equiv>"}
-\mbox{\it (i)}   & @{term "fa(x) - (set as) = fa(y) - (set bs)"} &
+& \mbox{\it (i)}   & @{term "fa(x) - (set as) = fa(y) - (set bs)"}\\
-\mbox{\it (iii)} & @{text "(p \<bullet> x) R y"}\\
+& \mbox{\it (ii)}  & @{term "(fa(x) - set as) \<sharp>* \<pi>"}\\
-\mbox{\it (ii)}  & @{term "(fa(x) - set as) \<sharp>* p"} &
+& \mbox{\it (iii)} & @{text "(\<pi> \<bullet> x) R y"}\\
-\mbox{\it (iv)}  & @{term "(p \<bullet> as) = bs"}\\
+& \mbox{\it (iv)}  & @{term "(\<pi> \<bullet> as) = bs"}\\
-\end{array}
+\end{tabular}
-\end{equation}
+\end{defi}
-%
 \noindent
 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, that means \emph{restrict} names, then we keep sets of binders, but drop
-condition {\it (iv)} in \eqref{alphaset}:
+condition {\it (iv)} in Definition~\ref{alphaset}:
-%
-\begin{equation}\label{alphares}
+\begin{defi}[Alpha-Equivalence for Set+-Bindings]\label{alphares}\mbox{}\\
-\begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l}
+\begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}
-\multicolumn{2}{l}{@{term "(as, x) \<approx>res R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+@{term "(as, x) \<approx>res R fa \<pi> (bs, y)"}\hspace{2mm}@{text "\<equiv>"}
-\mbox{\it (i)}   & @{term "fa(x) - as = fa(y) - bs"} &
+& \mbox{\it (i)}   & @{term "fa(x) - as = fa(y) - bs"}\\
-\mbox{\it (iii)} & @{text "(p \<bullet> x) R y"}\\
+& \mbox{\it (ii)}  & @{term "(fa(x) - as) \<sharp>* \<pi>"}\\
-\mbox{\it (ii)}  & @{term "(fa(x) - as) \<sharp>* p"}\\
+& \mbox{\it (iii)} & @{text "(\<pi> \<bullet> x) R y"}\\
-\end{array}
+\end{tabular}
-\end{equation}
+\end{defi}
 It might be useful to consider first some examples how these definitions
 of alpha-equivalence pan out in practice.  For this consider the case of
 abstracting a set of atoms over types (as in type-schemes). We set
 @{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we
 define
-%
-\begin{center}
+\[
 @{text "fa(x) = {x}"}  \hspace{5mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) = fa(T\<^isub>1) \<union> fa(T\<^isub>2)"}
-\end{center}
+\]\smallskip
 \noindent
 Now recall the examples shown in \eqref{ex1} and
 \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and
 @{text "({y, x}, y \<rightarrow> x)"} are alpha-equivalent according to
-$\approx_{\,\textit{set}}$ and $\approx_{\,\textit{set+}}$ by taking @{text p} to
+$\approx_{\,\textit{set}}$ and $\approx_{\,\textit{set+}}$ by taking @{text "\<pi>"} to
 be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"}, then @{text
 "([x, y], x \<rightarrow> y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"}
 since there is no permutation that makes the lists @{text "[x, y]"} and
 @{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \<rightarrow> y"}}
 unchanged. Another example is @{text "({x}, x)"} $\approx_{\,\textit{set+}}$
-@{text "({x, y}, x)"} which holds by taking @{text p} to be the identity
+@{text "({x, y}, x)"} which holds by taking @{text "\<pi>"} to be the identity
 permutation.  However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}
 $\not\approx_{\,\textit{set}}$ @{text "({x, y}, x)"} since there is no
 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
 types. For this we define
-%
 \begin{equation}
-@{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_set (as, x) equal supp p (bs, x)"}
+\begin{array}{l}
+@{term "abs_set (as, x) (bs, x) \<equiv> \<exists>\<pi>. alpha_set (as, x) equal supp \<pi> (bs, x)"}\\
+@{term "abs_res (as, x) (bs, x) \<equiv> \<exists>\<pi>. alpha_res (as, x) equal supp \<pi> (bs, x)"}\\
+@{term "abs_lst (as, x) (bs, x) \<equiv> \<exists>\<pi>. alpha_lst (as, x) equal supp \<pi> (bs, x)"}\\
+\end{array}
 \end{equation}
 \noindent
-(similarly for $\approx_{\,\textit{abs\_set+}}$
+We can show that these relations are equivalence
-and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence
+relations and equivariant.
-relations. %% and equivariant.
 \begin{lem}\label{alphaeq}
 The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$
 and $\approx_{\,\textit{abs\_set+}}$ are equivalence relations. %, and if
 %@{term "abs_set (as, x) (bs, y)"} then also
 %@{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"} (similarly for the other two relations).
 \end{lem}
 \begin{proof}
-Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have
+Reflexivity is by taking @{text "\<pi>"} to be @{text "0"}. For symmetry we have
-a permutation @{text p} and for the proof obligation take @{term "-p"}. In case
+a permutation @{text p} and for the proof obligation take @{term "- \<pi>"}. In case
-of transitivity, we have two permutations @{text p} and @{text q}, and for the
+of transitivity, we have two permutations @{text "\<pi>\<^isub>1"} and @{text "\<pi>\<^isub>2"}, and for the
-proof obligation use @{text "q + p"}. All conditions are then by simple
+proof obligation use @{text "\<pi>\<^isub>1 + \<pi>\<^isub>2"}. All conditions are then by simple
 calculations.
 \end{proof}
 \noindent
 This lemma allows us to use our quotient package for introducing

changeset 3001	8d7d85e915b5
parent 3000	3c8d3aaf292c
child 3002	02d98590454d