
diff -r 68c894c513f6 -r 3c8d3aaf292c LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Sun Aug 28 14:50:13 2011 +0100
+++ b/LMCS-Paper/Paper.thy	Tue Sep 06 12:18:02 2011 +0100
@@ -101,7 +101,7 @@
   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 the first pair of type-schemes as alpha-equivalent,
+  we would like to regard 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:
 
@@ -226,9 +226,9 @@
   is heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}. Our work
   extends Ott in several aspects: one is that we support three binding
   modes---Ott has only one, namely the one where the order of binders matters.
-  Another is that our reasoning infrastructure, like the notion of support and
-  strong induction principles, is derived from first principles within the
-  Isabelle/HOL theorem prover.
+  Another is that our reasoning infrastructure, like strong induction principles
+  and the notion of free variables, is derived from first principles within 
+  the Isabelle/HOL theorem prover.
 
   However, we will not be able to cope with all specifications that are
   allowed by Ott. One reason is that Ott lets the user specify ``empty'' types
@@ -331,7 +331,7 @@
   
   \noindent
   then with the help of the quotient package we can obtain a function @{text "fv\<^sup>\<alpha>"}
-  operating on quotients, or alpha-equivalence classes of lambda-terms. This
+  operating on quotients, that is alpha-equivalence classes of lambda-terms. This
   lifted function is characterised by the equations
 
   \[
@@ -361,8 +361,8 @@
   Figure~\ref{corehas}). This term language involves patterns that have lists
   of type-, coercion- and term-variables, all of which are bound in @{text
   "\<CASE>"}-expressions. In these patterns we do not know in advance how many
-  variables need to be bound. Another example is the specification of SML,
-  which includes includes bindings as in type-schemes.\medskip
+  variables need to be bound. Another example is the algorithm W
+  which includes multiple binders in type-schemes.\medskip
 
   \noindent
   {\bf Contributions:}  We provide three new definitions for when terms
@@ -432,7 +432,7 @@
 
   Two central notions in the nominal logic work are sorted atoms and
   sort-respecting permutations of atoms. We will use the letters @{text "a,
-  b, c, \<dots>"} to stand for atoms and @{text "p, q, \<dots>"} to stand for
+  b, c, \<dots>"} to stand for atoms and @{text "\<pi>, \<dots>"} to stand for
   permutations. The purpose of atoms is to represent variables, be they bound or free. 
   The sorts of atoms can be used to represent different kinds of
   variables, such as the term-, coercion- and type-variables in Core-Haskell.
@@ -447,8 +447,8 @@
   where the generic type @{text "\<beta>"} is the type of the object 
   over which the permutation 
   acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},
-  the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}}, 
-  and the inverse permutation of @{term p} as @{text "- p"}. The permutation
+  the composition of two permutations @{term "\<pi>\<^isub>1"} and @{term "\<pi>\<^isub>2"} as \mbox{@{term "\<pi>\<^isub>1 + \<pi>\<^isub>2"}}, 
+  and the inverse permutation of @{term "\<pi>"} as @{text "- \<pi>"}. The permutation
   operation is defined over the type-hierarchy \cite{HuffmanUrban10};
   for example permutations acting on products, lists, sets, functions and booleans are
   given by:
@@ -456,43 +456,26 @@
   \begin{equation}\label{permute}
   \mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
   \begin{tabular}{@ {}l@ {}}
-  @{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\[2mm]
-  @{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\
-  @{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\
+  @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\[2mm]
+  @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+  @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
   \end{tabular} &
   \begin{tabular}{@ {}l@ {}}
-  @{thm permute_set_eq[no_vars, THEN eq_reflection]}\\
-  @{text "p \<bullet> f \<equiv> \<lambda>x. p \<bullet> (f (- p \<bullet> x))"}\\
-  @{thm permute_bool_def[no_vars, THEN eq_reflection]}
+  @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+  @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f (- \<pi> \<bullet> x))"}\\
+  @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}
   \end{tabular}
   \end{tabular}}
-  \end{equation}
+  \end{equation}\smallskip
   
-  \begin{center}
-  \mbox{\begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {\hspace{4mm}}c@ {}}
-  \begin{tabular}{@ {}l@ {}}
-  @{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\
-  @{thm permute_bool_def[no_vars, THEN eq_reflection]}
-  \end{tabular} &
-  \begin{tabular}{@ {}l@ {}}
-  @{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\
-  @{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\
-  \end{tabular} &
-  \begin{tabular}{@ {}l@ {}}
-  @{thm permute_set_eq[no_vars, THEN eq_reflection]}\\
-  @{text "p \<bullet> f \<equiv> \<lambda>x. p \<bullet> (f (- p \<bullet> x))"}\\
-  \end{tabular}
-  \end{tabular}}
-  \end{center}
-
   \noindent
   Concrete permutations in Nominal Isabelle are built up from swappings, 
   written as \mbox{@{text "(a b)"}}, which are permutations that behave 
   as follows:
   
-  \begin{center}
+  \[
   @{text "(a b) = \<lambda>c. if a = c then b else if b = c then a else c"}
-  \end{center}
+  \]\smallskip
 
   The most original aspect of the nominal logic work of Pitts is a general
   definition for the notion of the ``set of free variables of an object @{text
@@ -508,25 +491,31 @@
 
   \noindent
   There is also the derived notion for when an atom @{text a} is \emph{fresh}
-  for an @{text x}, defined as @{thm fresh_def[no_vars]}.
+  for an @{text x}, defined as 
+
+  \[
+  @{thm fresh_def[no_vars]}
+  \]\smallskip
+
+  \noindent
   We use for sets of atoms the abbreviation 
   @{thm (lhs) fresh_star_def[no_vars]}, defined as 
   @{thm (rhs) fresh_star_def[no_vars]}.
   A striking consequence of these definitions is that we can prove
   without knowing anything about the structure of @{term x} that
   swapping two fresh atoms, say @{text a} and @{text b}, leaves 
-  @{text x} unchanged, namely if @{text "a \<FRESH> x"} and @{text "b \<FRESH> x"}
-  then @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.
+  @{text x} unchanged, namely 
   
   \begin{prop}\label{swapfreshfresh}
-  @{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
+  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]}
   \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
   
-  \begin{center}
+  \[\mbox{
   \begin{tabular}{c@ {\hspace{10mm}}c}
   \begin{tabular}{rcl}
   @{term "supp a"} & $=$ & @{term "{a}"}\\
@@ -538,18 +527,16 @@
   \begin{tabular}{rcl}
   @{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp f \<union> supp x"}\\
   @{term "supp b"} & $=$ & @{term "{}"}\\
-  @{term "supp p"} & $=$ & @{term "{a. p \<bullet> a \<noteq> a}"}
+  @{term "supp \<pi>"} & $=$ & @{term "{a. \<pi> \<bullet> a \<noteq> a}"}
   \end{tabular}
-  \end{tabular}
-  \end{center}
+  \end{tabular}}
+  \]\smallskip
   
   \noindent 
   in some cases it can be difficult to characterise the support precisely, and
-  only an approximation can be established (as for functions above). 
-  
-  Reasoning about
-  such approximations can be simplified with the notion \emph{supports}, defined 
-  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}




