diff -r 9fb315392493 -r 8732ff59068b Paper/Paper.thy
--- a/Paper/Paper.thy	Wed May 26 15:34:54 2010 +0200
+++ b/Paper/Paper.thy	Wed May 26 15:37:56 2010 +0200
@@ -1,6 +1,6 @@
 (*<*)
 theory Paper
-imports "../Nominal/Test" "LaTeXsugar"
+imports "../Nominal/Test" "../Nominal/FSet" "LaTeXsugar"
 begin
 
 consts
@@ -85,7 +85,7 @@
   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
   %
@@ -183,10 +183,10 @@
   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
   %
@@ -220,7 +220,7 @@
   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}
@@ -556,7 +556,7 @@
  
   \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
   %
@@ -593,7 +593,7 @@
 
   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.
 *}
 
@@ -623,7 +623,7 @@
   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:
   %
@@ -638,7 +638,7 @@
   \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
@@ -692,20 +692,20 @@
   \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
-  $\approx_{\textit{res}}$ by taking @{text p} 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{res}}$ @{text "({x, y}, x)"} which holds by 
-  taking @{text p} 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 tree notions of alpha-equivalence
-  coincide, if we only abstract a single atom. 
+  @{text "({y, x}, y \<rightarrow> x)"} are alpha-equivalent according to
+  $\approx_{\textit{set}}$ and $\approx_{\textit{res}}$ by taking @{text p} 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{res}}$
+  @{text "({x, y}, x)"} which holds by taking @{text p} 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 
@@ -941,16 +941,16 @@
   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
-  in \emph{one} binding clause of a term constructor. 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{bind\_set} and \isacommand{bind\_res} the labels must either
-  refer to atom types or to sets of atom types; in case of \isacommand{bind}
-  the labels must refer to atom types or lists of atom types. Two examples for
-  the use of shallow binders are the specification of lambda-terms, where a
-  single name is bound, and type-schemes, where a finite set of names is
-  bound:
+  There are some restrictions we need to impose on binding clasues: First, a
+  body can only occur in \emph{one} binding clause of a term constructor. 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{bind\_set} and \isacommand{bind\_res} the
+  labels must either refer to atom types or to sets of atom types; in case of
+  \isacommand{bind} the labels must refer to atom types or lists of atom
+  types. Two examples for the use of shallow binders are the specification of
+  lambda-terms, where a single name is bound, and type-schemes, where a finite
+  set of names is bound:
 
   \begin{center}
   \begin{tabular}{@ {}cc@ {}}
@@ -974,7 +974,7 @@
   \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.
@@ -1119,7 +1119,7 @@
   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 
@@ -1152,7 +1152,7 @@
   @{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:
 
@@ -1455,7 +1455,7 @@
 
   \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}
@@ -1526,7 +1526,7 @@
   \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
@@ -1540,7 +1540,7 @@
   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 
@@ -1567,7 +1567,7 @@
 
   \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 
@@ -1864,7 +1864,7 @@
   \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}
@@ -1894,7 +1894,7 @@
   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}. 
 *}