diff -r 86122d793f32 -r 0c958e385691 Pearl/Paper.thy
--- a/Pearl/Paper.thy	Tue Apr 06 07:36:15 2010 +0200
+++ b/Pearl/Paper.thy	Tue Apr 06 14:08:06 2010 +0200
@@ -68,7 +68,7 @@
   separate type for each sort of atoms and let the type system enforce the
   sort-respecting property of permutations. Inspired by the work on nominal
   unification \cite{UrbanPittsGabbay04}, it seemed best at the time to also
-  implement permutations concretely as list of pairs of atoms. Thus Nominal
+  implement permutations concretely as lists of pairs of atoms. Thus Nominal
   Isabelle used the two-place permutation operation with the generic type
 
   @{text [display,indent=10] "_ \<bullet> _  ::  (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
@@ -81,6 +81,8 @@
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
   @{text "[] \<bullet> c"} & @{text "="} & @{text c}\\
+  \end{tabular}\hspace{12mm}
+  \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
   @{text "(a b)::\<pi> \<bullet> c"} & @{text "="} & 
      $\begin{cases} @{text a} & \textrm{if}~@{text "\<pi> \<bullet> c = b"}\\ 
                     @{text b} & \textrm{if}~@{text "\<pi> \<bullet> c = a"}\\
@@ -132,7 +134,7 @@
   support operations with only a single type parameter and the permutation
   operations @{text "_ \<bullet> _"} used above in the permutation properties
   contain two! To work around this obstacle, Nominal Isabelle 
-  required from the user to
+  required the user to
   declare up-front the collection of \emph{all} atom types, say @{text
   "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}. From this collection it used custom ML-code to
   generate @{text n} type classes corresponding to the permutation properties,
@@ -144,7 +146,7 @@
   This operation has only a single type parameter @{text "\<beta>"} (the @{text "\<alpha>\<^isub>i"} are the
   atom types given by the user). 
 
-  While the representation of permutations-as-list solved the
+  While the representation of permutations-as-lists solved the
   ``sort-respecting'' requirement and the declaration of all atom types
   up-front solved the problem with Isabelle/HOL's type classes, this setup
   caused several problems for formalising the nominal logic work: First,
@@ -214,10 +216,10 @@
   simple formalisation of the nominal logic work.\smallskip
 
   \noindent
-  {\bf Contributions of the paper:} We use a single atom type for representing
-  atoms of different sorts and use functions for representing
-  permutations. This drastically reduces the number of type classes to just
-  two (permutation types and finitely supported types), which we need in order
+  {\bf Contributions of the paper:} Our use of a single atom type for representing
+  atoms of different sorts and of functions for representing
+  permutations drastically reduces the number of type classes to just
+  two (permutation types and finitely supported types) that we need in order
   reason abstractly about properties from the nominal logic work. The novel
   technical contribution of this paper is a mechanism for dealing with
   ``Church-style'' lambda-terms \cite{Church40} and HOL-based languages
@@ -242,7 +244,9 @@
   \noindent
   whereby the string argument specifies the sort of the atom.  (We use type
   \emph{string} merely for convenience; any countably infinite type would work
-  as well.)  We have an auxiliary function @{text sort} that is defined as @{thm
+  as well.)  A similar design choice was made by Gunter et al \cite{GunterOsbornPopescu09} 
+  for their variables. 
+  We have an auxiliary function @{text sort} that is defined as @{thm
   sort_of.simps[no_vars]}, and we clearly have for every finite set @{text X} of
   atoms and every sort @{text s} the property:
   
@@ -275,7 +279,7 @@
   @{text "i"}-@{text "iii"}. 
 
   However, a moment of thought is needed about how to construct non-trivial
-  permutations? In the nominal logic work it turned out to be most convenient
+  permutations. In the nominal logic work it turned out to be most convenient
   to work with swappings, written @{text "(a b)"}.  In our setting the
   type of swappings must be
 
@@ -435,7 +439,7 @@
 
   \begin{theorem}
   If @{text \<beta>}, @{text "\<beta>\<^isub>1"} and @{text "\<beta>\<^isub>2"} are permutation types, 
-  then so are: @{text "atom"}, @{text "\<beta>\<^isub>1 \<Rightarrow> \<beta>\<^isub>2"}, 
+  then so are @{text "atom"}, @{text "\<beta>\<^isub>1 \<Rightarrow> \<beta>\<^isub>2"}, 
   @{text perm}, @{term "\<beta> set"}, @{term "\<beta> list"}, @{term "\<beta>\<^isub>1 \<times> \<beta>\<^isub>2"},
   @{text bool} and @{text "nat"}.
   \end{theorem}
@@ -450,8 +454,7 @@
   @{text "0 \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "0 + \<pi>' - 0 = \<pi>'"}\\
   @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) + \<pi>' - (\<pi>\<^isub>1 + \<pi>\<^isub>2)"}\\
   & @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) + \<pi>' - \<pi>\<^isub>2 - \<pi>\<^isub>1"}\\
-  & @{text "="} & @{text "\<pi>\<^isub>1 + (\<pi>\<^isub>2 + \<pi>' - \<pi>\<^isub>2) - \<pi>\<^isub>1"}\\
-  & @{text "\<equiv>"} & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> \<pi>'"} 
+  & @{text "="} & @{text "\<pi>\<^isub>1 + (\<pi>\<^isub>2 + \<pi>' - \<pi>\<^isub>2) - \<pi>\<^isub>1"} @{text "\<equiv>"} @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> \<pi>'"} 
   \end{tabular}\hfill\qed
   \end{isabelle}
   \end{proof}
@@ -624,11 +627,8 @@
   \begin{proof}
   \begin{isabelle}
   \begin{tabular}[t]{c@ {\hspace{2mm}}l@ {\hspace{5mm}}l}
-  & @{thm (lhs) fresh_permute_iff[where p="\<pi>",no_vars]}
-  & \\
-  @{text "\<Leftrightarrow>"}
-  & @{term "finite {b. (\<pi> \<bullet> a \<rightleftharpoons> b) \<bullet> \<pi> \<bullet> x \<noteq> \<pi> \<bullet> x}"}
-  & by definition\\
+  & \multicolumn{2}{@ {}l}{@{thm (lhs) fresh_permute_iff[where p="\<pi>",no_vars]} @{text "\<equiv>"}
+    @{term "finite {b. (\<pi> \<bullet> a \<rightleftharpoons> b) \<bullet> \<pi> \<bullet> x \<noteq> \<pi> \<bullet> x}"}}\\
   @{text "\<Leftrightarrow>"}
   & @{term "finite {b. (\<pi> \<bullet> a \<rightleftharpoons> \<pi> \<bullet> b) \<bullet> \<pi> \<bullet> x \<noteq> \<pi> \<bullet> x}"} 
   & since @{text "\<pi> \<bullet> _"} is bijective\\ 
@@ -636,11 +636,9 @@
   & @{term "finite {b. \<pi> \<bullet> (a \<rightleftharpoons> b) \<bullet> x \<noteq> \<pi> \<bullet> x}"}
   & by \eqref{permutecompose} and \eqref{swapeqvt}\\
   @{text "\<Leftrightarrow>"}
-  & @{term "finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"}
+  & @{term "finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"} @{text "\<equiv>"}
+    @{thm (rhs) fresh_permute_iff[where p="\<pi>",no_vars]}
   & by \eqref{permuteequ}\\
-  @{text "\<Leftrightarrow>"}
-  & @{thm (rhs) fresh_permute_iff[where p="\<pi>",no_vars]}
-  & by definition\\
   \end{tabular}
   \end{isabelle}\hfill\qed
   \end{proof}
@@ -700,10 +698,9 @@
   iii)  & @{thm (concl) supp_is_least_supports[no_vars]}
          provided @{thm (prem 1) supp_is_least_supports[no_vars]},
          @{thm (prem 2) supp_is_least_supports[no_vars]}
-         and @{text "S"} is the least such set, that means formally:\\[2mm]
-
-        & \multicolumn{1}{c}{for all @{text "S'"}, if @{term "finite S'"} and 
-           @{term "S' supports x"} then @{text "S \<subseteq> S'"}.}
+         and @{text "S"} is the least such set, that means formally,
+         for all @{text "S'"}, if @{term "finite S'"} and 
+         @{term "S' supports x"} then @{text "S \<subseteq> S'"}.
   \end{tabular}
   \end{isabelle} 
   \end{lemma}
@@ -727,11 +724,11 @@
   more useful:
 
   \begin{lemma}\label{optimised} Let @{text x} be of permutation type.
-  Then @{thm (concl) finite_supp_unique[no_vars]}
+  We have that @{thm (concl) finite_supp_unique[no_vars]}
   provided @{thm (prem 1) finite_supp_unique[no_vars]},
   @{thm (prem 2) finite_supp_unique[no_vars]}, and for
   all @{text "a \<in> S"} and all @{text "b \<notin> S"}, with @{text a}
-  and @{text b} having the same sort, then @{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"}
+  and @{text b} having the same sort, then \mbox{@{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"}}
   \end{lemma}
 
   \begin{proof}
@@ -795,7 +792,7 @@
   \noindent
   holds by a simple calculation using the group properties of permutations.
   The proof-obligation can then be discharged by analysing the inequality
-  between the permutations @{term "(p \<bullet> a \<rightleftharpoons> b)"} and @{term "(a \<rightleftharpoons> b)"}.
+  between the permutations @{term "(\<pi> \<bullet> a \<rightleftharpoons> b)"} and @{term "(a \<rightleftharpoons> b)"}.
 
   The main point about support is that whenever an object @{text x} has finite
   support, then Proposition~\ref{choosefresh} allows us to choose for @{text x} a 
@@ -836,15 +833,15 @@
   @{text "nat_of a"} & @{text "="} & @{text "(a \<rightleftharpoons> c) \<bullet> (nat_of a)"} & by def.~of permutations on nats\\
   & @{text "="} & @{term "((a \<rightleftharpoons> c) \<bullet> nat_of) ((a \<rightleftharpoons> c) \<bullet> a)"} & by \eqref{permutefunapp}\\
   & @{text "="} & @{term "nat_of c"} & by assumptions on @{text c}\\
-  \end{tabular}\hfill\qed
+  \end{tabular}
   \end{isabelle}
   
 
   \noindent
   But this means we have that @{term "nat_of a = nat_of c"} and @{term "sort_of a = sort_of c"}.
   This implies that atoms @{term a} and @{term c} must be equal, which clashes with our
-  assumption @{term "c \<noteq> a"} about how we chose @{text c}. Similar examples for 
-  constructions that have infinite support are given in~\cite{Cheney06}.
+  assumption @{term "c \<noteq> a"} about how we chose @{text c}. 
+  Cheney \cite{Cheney06} gives similar examples for constructions that have infinite support.
 *}
 
 section {* Concrete Atom Types *}
@@ -918,11 +915,10 @@
   must all have the same sort.
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
-  i) & if @{thm (lhs) atom_eq_iff [no_vars]} then @{thm (rhs) atom_eq_iff [no_vars]}\\
-  ii) & @{thm atom_eqvt[where p="\<pi>", no_vars]}\\
-  iii) & @{thm sort_of_atom_eq [no_vars]}
-  \end{tabular}\hfill\numbered{atomprops}
+  i)   \hspace{1mm}if @{thm (lhs) atom_eq_iff [no_vars]} then @{thm (rhs) atom_eq_iff [no_vars]}\hspace{4mm}
+  ii)  \hspace{1mm}@{thm atom_eqvt[where p="\<pi>", no_vars]}\hspace{4mm}
+  iii) \hspace{1mm}@{thm sort_of_atom_eq [no_vars]}
+  \hfill\numbered{atomprops}
   \end{isabelle}
 
   \noindent
@@ -1093,7 +1089,7 @@
   \noindent
   which can easily be shown to be injective.  
   
-  Having settled on what the the sorts should be for ``Church-like'' atoms, we have to
+  Having settled on what the sorts should be for ``Church-like'' atoms, we have to
   give a subtype definition for concrete atoms. Previously we identified a subtype consisting 
   of atoms of only one specified sort. This must be generalised to all sorts the
   function @{text "sort_ty"} might produce, i.e.~the
@@ -1156,8 +1152,9 @@
   \noindent
   where the argument, or arguments, are datatypes for which we can automatically
   define an injective function like @{text "sort_ty"} (see \eqref{sortty}).
-  Our hope is that with this approach the authors of \cite{PaulsonBenzmueller} 
-  can make headway with formalising their results about simple type theory.  
+  Our hope is that with this approach Benzmueller and Paulson the authors of 
+  \cite{PaulsonBenzmueller} can make headway with formalising their results 
+  about simple type theory.  
   Because of its limitations, they did not attempt this with the old version 
   of Nominal Isabelle. We also hope we can make progress with formalisations of
   HOL-based languages.
@@ -1185,9 +1182,9 @@
   swap different kinds of atoms. This simplifies considerably the reasoning
   involved in building Nominal Isabelle.
 
-  Second, we represented permutation as functions so that the associated
-  permutation operation has only a single type parameter. From this we derive
-  most benefits because the abstract reasoning about permutations fits cleanly
+  Second, we represented permutations as functions so that the associated
+  permutation operation has only a single type parameter. This is very convenient
+  because the abstract reasoning about permutations fits cleanly
   with Isabelle/HOL's type classes. No custom ML-code is required to work
   around rough edges. Moreover, by establishing that our permutations-as-functions
   representation satisfy the group properties, we were able to use extensively 
@@ -1222,8 +1219,8 @@
   \noindent
   {\bf Acknowledgements:} We are very grateful to Jesper Bengtson, Stefan 
   Berghofer and Cezary Kaliszyk for their comments on earlier versions 
-  of this paper.
-  
+  of this paper. We are also grateful to the anonymous referee who helped us to
+  put the work into the right context.  
 *}