nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:157e8a4a6556
+:f11dd09fa3a7
 @{text "p \<bullet> (f x) = f (p \<bullet> x)"}
 \end{equation}
 \noindent
 From property \eqref{equivariancedef} and the definition of @{text supp}, we
-can be easily deduce that equivariant functions have empty support. There is
+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"} \;\;implies\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}
 fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders
 @{text as} in @{text x}, because @{term "p \<bullet> x = x"}.
 Most properties given in this section are described in detail in \cite{HuffmanUrban10}
 and of course all are formalised in Isabelle/HOL. In the next sections we will make
-extensively use of these properties in order to define alpha-equivalence in
+extensive use of these properties in order to define alpha-equivalence in
 the presence of multiple binders.
 *}
 section {* General Binders\label{sec:binders} *}
 given a free-variable function @{text "fv"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
 set"}}, then @{text x} and @{text y} need to have the same set of free
 variables; moreover there must be a permutation @{text p} such that {\it
 ii)} @{text p} leaves the free variables 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 {\it iv)} that
+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:
 %
 \begin{equation}\label{alphaset}
 \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
 @{text "\<and>"} & @{term "(p \<bullet> as) = bs"}\\
 \end{array}
 \end{equation}
 \noindent
-Note that this relation is dependent on the permutation @{text
+Note that this relation depends on the permutation @{text
 "p"}. Alpha-equivalence between two pairs is then the relation where we
 existentially quantify over this @{text "p"}. Also note that the relation is
 dependent on a free-variable function @{text "fv"} 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
 \end{center}
 \noindent
 Now recall the examples shown in \eqref{ex1}, \eqref{ex2} 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
+@{text "({y, x}, y \<rightarrow> x)"} are alpha-equivalent according to
-$\approx_{\textit{res}}$ by taking @{text p} to be the swapping @{term "(x \<rightleftharpoons>
+$\approx_{\textit{set}}$ and $\approx_{\textit{res}}$ by taking @{text p} to
-y)"}. In case of @{text "x \<noteq> y"}, then @{text "([x, y], x \<rightarrow> y)"}
+be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"}, then @{text
-$\not\approx_{\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"} since there is no permutation
+"([x, y], x \<rightarrow> y)"} $\not\approx_{\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"}
-that makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and also
+since there is no permutation that makes the lists @{text "[x, y]"} and
-leaves the type \mbox{@{text "x \<rightarrow> y"}} unchanged. Another example is
+@{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \<rightarrow> y"}}
-@{text "({x}, x)"} $\approx_{\textit{res}}$ @{text "({x, y}, x)"} which holds by
+unchanged. Another example is @{text "({x}, x)"} $\approx_{\textit{res}}$
-taking @{text p} to be the
+@{text "({x, y}, x)"} which holds by taking @{text p} to be the identity
-identity permutation.  However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}
+permutation.  However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}
-$\not\approx_{\textit{set}}$ @{text "({x, y}, x)"} since there is no permutation
+$\not\approx_{\textit{set}}$ @{text "({x, y}, x)"} since there is no
-that makes the
+permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal
-sets @{text "{x}"} and @{text "{x, y}"} equal (similarly for $\approx_{\textit{list}}$).
+(similarly for $\approx_{\textit{list}}$).  It can also relatively easily be
-It can also relatively easily be shown that all tree notions of alpha-equivalence
+shown that all tree notions of alpha-equivalence coincide, if we only
-coincide, if we only abstract a single atom.
+abstract a single atom.
 In the rest of this section we are going to introduce three abstraction
 types. For this we define
 %
 \begin{equation}
 Similarly for the other binding modes. Interestingly, in case of \isacommand{bind\_set}
 and \isacommand{bind\_res} the binding clauses will make a difference to the semantics
 of the specification (the corresponding alpha-equivalence will differ). We will
 show this later with an example.
-There are some restrictions we need to impose: First, a body can only occur
+There are some restrictions we need to impose on binding clasues: First, a
-in \emph{one} binding clause of a term constructor. For binders we
+body can only occur in \emph{one} binding clause of a term constructor. For
-distinguish between \emph{shallow} and \emph{deep} binders.  Shallow binders
+binders we distinguish between \emph{shallow} and \emph{deep} binders.
-are just labels. The restriction we need to impose on them is that in case
+Shallow binders are just labels. The restriction we need to impose on them
-of \isacommand{bind\_set} and \isacommand{bind\_res} the labels must either
+is that in case of \isacommand{bind\_set} and \isacommand{bind\_res} the
-refer to atom types or to sets of atom types; in case of \isacommand{bind}
+labels must either refer to atom types or to sets of atom types; in case of
-the labels must refer to atom types or lists of atom types. Two examples for
+\isacommand{bind} the labels must refer to atom types or lists of atom
-the use of shallow binders are the specification of lambda-terms, where a
+types. Two examples for the use of shallow binders are the specification of
-single name is bound, and type-schemes, where a finite set of names is
+lambda-terms, where a single name is bound, and type-schemes, where a finite
-bound:
+set of names is bound:
 \begin{center}
 \begin{tabular}{@ {}cc@ {}}
 \begin{tabular}{@ {}l@ {\hspace{-1mm}}}
 \isacommand{nominal\_datatype} @{text lam} =\\
 \end{center}
 \noindent
 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{bind\_set} or \isacommand{bind} in the second case makes again a
+\isacommand{bind\_set} or \isacommand{bind} in the second case makes a
 difference to the semantics of the specification. Note also that in
 these specifications @{text "name"} refers to an atom type, and @{text
 "fset"} to the type of finite sets.

changeset 2175	f11dd09fa3a7
parent 2163	5dc48e1af733
child 2176	5054f170024e