nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:9fb315392493
+:8732ff59068b
 (*<*)
 theory Paper
-imports "../Nominal/Test" "LaTeXsugar"
+imports "../Nominal/Test" "../Nominal/FSet" "LaTeXsugar"
 begin
 consts
 fv :: "'a \<Rightarrow> 'b"
 abs_set :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
 mechanisms for binding single variables have not fared extremely well with the
 more advanced tasks in the POPLmark challenge \cite{challenge05}, 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 case of type-schemes we do not
+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 the following two type-schemes as alpha-equivalent
 %
 \begin{equation}\label{ex1}
 @{text "\<forall>{x, y}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{y, x}. y \<rightarrow> x"}
 \noindent
 where the notation @{text "[_]._"} indicates that the list of @{text "x\<^isub>i"}
 becomes bound in @{text s}. In this representation the term
 \mbox{@{text "\<LET> [x].s [t\<^isub>1, t\<^isub>2]"}} is a perfectly legal
-instance, but the lengths of two lists do not agree. To exclude such terms,
+instance, but the lengths of the two lists do not agree. To exclude such terms,
 additional predicates about well-formed
 terms are needed in order to ensure that the two lists are of equal
-length. This can result into very messy reasoning (see for
+length. This can result in very messy reasoning (see for
 example~\cite{BengtsonParow09}). To avoid this, we will allow type
 specifications for $\mathtt{let}$s as follows
 %
 \begin{center}
 \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}
 clause states to bind in @{text s} all the names the function @{text
 "bn(as)"} returns.  This style of specifying terms and bindings is heavily
 inspired by the syntax of the Ott-tool \cite{ott-jfp}.
 However, we will not be able to cope with all specifications that are
-allowed by Ott. One reason is that Ott lets the user to specify ``empty''
+allowed by Ott. One reason is that Ott lets the user specify ``empty''
 types like
 \begin{center}
 @{text "t ::= t t | \<lambda>x. t"}
 \end{center}
 @{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 three 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.
 Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, just
 re-arranging the arguments of
 term-constructors so that binders and their bodies are next to each other will
 result in inadequate representations. Therefore we will first
 extract datatype definitions from the specification and then define
-expicitly an alpha-equivalence relation over them.
+explicitly an alpha-equivalence relation over them.
 The 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>"}
 %
 \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 free-variable
+The first non-trivial step we have to perform is the generation of free-variable
 functions from the specifications. For atomic types we define the auxilary
 free variable functions:
 \begin{center}
 \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
 @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"} are equivalence relations and equivariant.
 \end{lemma}
 \begin{proof}
 The proof is by mutual induction over the definitions. The non-trivial
-cases involve premises build up by $\approx_{\textit{set}}$,
+cases involve premises built up by $\approx_{\textit{set}}$,
 $\approx_{\textit{res}}$ and $\approx_{\textit{list}}$. They
 can be dealt with as in Lemma~\ref{alphaeq}.
 \end{proof}
 \noindent
 \begin{center}
 @{text "P\<^bsub>ty\<AL>\<^esub>\<^isub>1 y\<^isub>1 \<dots> P\<^bsub>ty\<AL>\<^esub>\<^isub>n y\<^isub>n "}
 \end{center}
 \noindent
-for all @{text "y\<^isub>i"} wherby the variables @{text "P\<^bsub>ty\<AL>\<^esub>\<^isub>i"} stand for properties
+for all @{text "y\<^isub>i"} whereby the variables @{text "P\<^bsub>ty\<AL>\<^esub>\<^isub>i"} stand for properties
 defined over the types @{text "ty\<AL>\<^isub>1 \<dots> ty\<AL>\<^isub>n"}. The premises of
 these induction principles look
 as follows
 \begin{center}
 \noindent
 where the @{text "x\<^isub>i, \<dots>, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\<alpha>"}.
 Next we lift the permutation operations defined in \eqref{ceqvt} for
 the raw term-constructors @{text "C"}. These facts contain, in addition
 to the term-constructors, also permutation operations. In order to make the
-lifting to go through,
+lifting go through,
 we have to know that the permutation operations are respectful
 w.r.t.~alpha-equivalence. This amounts to showing that the
 alpha-equivalence relations are equivariant, which we already established
 in Lemma~\ref{equiv}. As a result we can establish the equations
 \end{tabular}}
 \end{equation}
 \noindent
 which can be established by induction on @{text "\<approx>ty"}. Whereas the first
-property is always true by the way how we defined the free-variable
+property is always true by the way we defined the free-variable
 functions for types, the second and third do \emph{not} hold in general. There is, in principle,
 the possibility that the user defines @{text "bn\<^isub>k"} so that it returns an already bound
 variable. Then the third property is just not true. However, our
 restrictions imposed on the binding functions
 exclude this possibility.
 \hspace{15mm}@{text "Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2))"}
 \end{tabular}
 \end{center}
 \noindent
-So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we are can equally
+So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we can equally
 establish
 \begin{center}
 @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}
 \end{center}
 Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps},
 we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}.
 This completes the proof showing that the strong induction principle derives from
 the weak induction principle. For the moment we can derive the difficult cases of
-the strong induction principles only by hand, but they are very schematically
+the strong induction principles only by hand, but they are very schematic
 so that with little effort we can even derive them for
 Core-Haskell given in Figure~\ref{nominalcorehas}.
 *}

changeset 2301	8732ff59068b
parent 2184	665b645b4a10
child 2186	762a739c9eb4