# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1269948174 -7200
# Node ID 55cb244b020cd985d74d6d8e28f4f255334f614d
# Parent  62b87efcef29ccfc8190d684f52cd674a7c5f811
changes to section 2

diff -r 62b87efcef29 -r 55cb244b020c Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Mar 30 11:45:41 2010 +0200
+++ b/Paper/Paper.thy	Tue Mar 30 13:22:54 2010 +0200
@@ -148,7 +148,7 @@
   \noindent
   As a result, we provide three general binding mechanisms each of which binds
   multiple variables at once, and let the user chose which one is intended
-  when formalising a programming language calculus.
+  when formalising a term-calculus.
 
   By providing these general binding mechanisms, however, we have to work
   around a problem that has been pointed out by Pottier \cite{Pottier06} and
@@ -342,7 +342,7 @@
   The examples we have in mind where our reasoning infrastructure will be
   helpful includes the term language of System @{text "F\<^isub>C"}, also
   known as Core-Haskell (see Figure~\ref{corehas}). This term language
-  involves patterns that have lists of type-, coercion- and term-variables
+  involves patterns that have lists of type-, coercion- and term-variables,
   all of which are bound in @{text "\<CASE>"}-expressions. One
   difficulty is that each of these variables come with a kind or type
   annotation. Representing such binders with single binders and reasoning
@@ -395,7 +395,7 @@
   \caption{The term-language of System @{text "F\<^isub>C"}
   \cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this
   version of the term-language we made a modification by separating the
-  grammars for type and coercion kinds, as well as for types and coercion
+  grammars for type kinds and coercion kinds, as well as for types and coercion
   types. For this paper the interesting term-constructor is @{text "\<CASE>"},
   which binds multiple type-, coercion- and term-variables.\label{corehas}}
   \end{figure}
@@ -409,13 +409,14 @@
   \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. The
-  sorts can be used to represent different kinds of variables, such as the
-  term-, coercion- and type-variables in Core-Haskell, and it is assumed that there is an
-  infinite supply of atoms for each sort. However, in order to simplify the
-  description, we shall assume in what follows that there is only one sort of
-  atoms.
+  Two central notions in the nominal logic work are sorted atoms and
+  sort-respecting permutations of atoms. We will use the variables @{text "a,
+  b, c, \<dots>"} to stand for atoms and @{text "p, q, \<dots>"} to stand for
+  permutations.  The sorts of atoms can be used to represent different kinds of
+  variables, such as the term-, coercion- and type-variables in Core-Haskell,
+  and it is assumed that there is an infinite supply of atoms for each
+  sort. However, in order to simplify the description, we shall assume in what
+  follows that there is 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 
@@ -486,19 +487,18 @@
   swapping two fresh atoms, say @{text a} and @{text b}, leave 
   @{text x} unchanged. 
 
-  \begin{property}
+  \begin{property}\label{swapfreshfresh}
   @{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
   \end{property}
 
-  \noindent
-  While often the support of an object can be easily described, for
-  example\\[-6mm]
+  While often the support of an object can be relatively easily 
+  described, for example\\[-6mm]
   %
   \begin{eqnarray}
   @{term "supp a"} & = & @{term "{a}"}\\
   @{term "supp (x, y)"} & = & @{term "supp x \<union> supp y"}\\
   @{term "supp []"} & = & @{term "{}"}\\
-  @{term "supp (x#xs)"} & = & @{term "supp (x, xs)"}\\
+  @{term "supp (x#xs)"} & = & @{term "supp x \<union> supp xs"}\\
   @{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp (f, x)"}\label{suppfun}\\
   @{term "supp b"} & = & @{term "{}"}\\
   @{term "supp p"} & = & @{term "{a. p \<bullet> a \<noteq> a}"}
@@ -507,7 +507,7 @@
   \noindent 
   in some cases it can be difficult to establish the support precisely, and
   only give an approximation (see the case for function applications
-  above). Such approximations can be made precise with the notion
+  above). Such approximations can be calculated with the notion
   \emph{supports}, defined as follows
 
   \begin{defn}
@@ -525,21 +525,57 @@
 
   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 
-  requires that every permutation leaves @{text f} unchanged, or equivalently that
-  a permutation applied to the application @{text "f x"} can be moved to its 
-  arguments. That is
+  requires that every permutation leaves @{text f} unchanged, that is
+  %
+  \begin{equation}\label{equivariancedef}
+  @{term "\<forall>p. p \<bullet> f = f"}
+  \end{equation}
+
+  \noindent or equivalently that a permutation applied to the application
+  @{text "f x"} can be moved to the argument @{text x}. That means we have for
+  all permutations @{text p}
   %
   \begin{equation}\label{equivariance}
-  @{text "\<forall>p. p \<bullet> f = f"} \;\;if and only if\;\;
-  @{text "\<forall>p. p \<bullet> (f x) = f (p \<bullet> x)"}
+  @{text "p \<bullet> f = f"} \;\;\;\textit{if and only if}\;\;\;
+  @{text "p \<bullet> (f x) = f (p \<bullet> x)"}
   \end{equation}
  
   \noindent
-  From the first equation and the definition of support shown in \eqref{suppdef}, 
-  we can be easily deduce that an equivariant function has empty support.
+  From equation \eqref{equivariancedef} and the definition of support shown in
+  \eqref{suppdef}, we can be easily deduce that an equivariant function has
+  empty support.
+
+  Finally, the nominal logic work provides us with elegant means to rename 
+  binders. While in the older version of Nominal Isabelle, we used extensively 
+  Property~\ref{swapfreshfresh} for renaming single binders, this property 
+  proved unwieldy for dealing with multiple binders. For this the following
+  generalisations turned out to be easier to use.
+
+  \begin{property}\label{supppermeq}
+  @{thm[mode=IfThen] supp_perm_eq[no_vars]}
+  \end{property}
 
-  In the next section we use @{text "supp"} and permutations for characterising
-  alpha-equivalence in the presence of multiple binders.
+  \begin{property}
+  For a finite set @{text xs} and a finitely supported @{text x} with
+  @{term "xs \<sharp>* x"} and also a finitely supported @{text c}, there
+  exists a permutation @{text p} such that @{term "(p \<bullet> xs) \<sharp>* c"} and
+  @{term "supp x \<sharp>* p"}.
+  \end{property}
+
+  \noindent
+  The idea behind the second property is that given a finite set @{text xs}
+  of binders (being bound in @{text x} which is ensured by the
+  assumption @{term "xs \<sharp>* x"}), then there exists a permutation @{text p} such that
+  the renamed binders @{term "p \<bullet> xs"} avoid the @{text c} (which can be arbitrarily chosen
+  as long as it is finitely supported) and also does not affect anything
+  in the support of @{text x} (that is @{term "supp x \<sharp>* p"}). The last 
+  fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders 
+  in @{text x}, because @{term "p \<bullet> x = x"}.
+
+  All properties given in this section are formalised in Isabelle/HOL and also
+  most of them are described with proofs in \cite{HuffmanUrban10}. In the next section 
+  we make extensively use of the properties of @{text "supp"} and permutations 
+  for characterising alpha-equivalence in the presence of multiple binders.
  
 *}