--- a/Pearl-jv/Paper.thy	Fri Oct 08 23:53:51 2010 +0100
+++ b/Pearl-jv/Paper.thy	Tue Oct 12 10:07:48 2010 +0100
@@ -39,41 +39,44 @@
 
 (*>*)
 
+(*
+  TODO: write about supp of finite sets, abstraction over finite sets
+*)
+
 section {* Introduction *}
 
 text {*
-  TODO: write about supp of finite sets
+  Nominal Isabelle provides a proving infratructure for convenient reasoning
+  about programming languages involving binders such as lambda abstractions or
+  quantifications in type schemes:
 
-  Nominal Isabelle provides a proving infratructure for
-  convenient reasoning about programming languages. At its core Nominal
-  Isabelle is based on the nominal logic work by Pitts at al
-  \cite{GabbayPitts02,Pitts03}. The most basic notion in this work
-  is a sort-respecting permutation operation defined over a countably infinite
-  collection of sorted atoms. The atoms are used for representing variables
-  that might be bound. Multiple sorts are necessary for being able to
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{text "\<lambda>x. t       \<forall>{x\<^isub>1,\<dots>,x\<^isub>n}. \<tau>"}
+  \hfill\numbered{atomperm}
+  \end{isabelle}
+  
+  \noindent
+  At its core Nominal Isabelle is based on the nominal logic work by Pitts at
+  al \cite{GabbayPitts02,Pitts03}. The most basic notion in this work is a
+  sort-respecting permutation operation defined over a countably infinite
+  collection of sorted atoms. The atoms are used for representing variable names
+  that might be free or bound. Multiple sorts are necessary for being able to
   represent different kinds of variables. For example, in the language Mini-ML
-  there are bound term variables and bound type variables; each kind needs to
-  be represented by a different sort of atoms.
+  there are bound term variables in lambda abstractions and bound type variables in
+  type schemes. In order to be able to separate them, each kind of variables needs to be
+  represented by a different sort of atoms. 
 
   In our formalisation of the nominal logic work, we have to make a design decision 
   about how to represent sorted atoms and sort-respecting permutations. One possibility
-  is to 
-
-
-
-%  Unfortunately, the type system of Isabelle/HOL is not a good fit for the way
-%  atoms and sorts are used in the original formulation of the nominal logic work.
-%  The reason is that one has to ensure that permutations are sort-respecting.
-%  This was done implicitly in the original nominal logic work \cite{Pitts03}.
-
-
-  Isabelle used the two-place permutation operation with the generic type
+  is to have separate types for the different kinds of atoms. With this one can represent
+  permutations as lists of pairs of atoms and the operation of applying
+  a permutation to an object as the overloaded function
 
   @{text [display,indent=10] "_ \<bullet> _  ::  (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
 
   \noindent 
-  where @{text "\<alpha>"} stands for the type of atoms and @{text "\<beta>"} for the type
-  of the objects on which the permutation acts. For atoms of type @{text "\<alpha>"} 
+  where @{text "\<alpha>"} stands for a type of atoms and @{text "\<beta>"} for the type
+  of the objects on which the permutation acts. For atoms 
   the permutation operation is defined over the length of lists as follows
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -91,15 +94,58 @@
   @{text "b"}. For atoms of different type, the permutation operation
   is defined as @{text "\<pi> \<bullet> c \<equiv> c"}.
 
-  With the list representation of permutations it is impossible to state an
-  ``ill-sorted'' permutation, since the type system excludes lists containing
-  atoms of different type. Another advantage of the list representation is that
-  the basic operations on permutations are already defined in the list library:
-  composition of two permutations (written @{text "_ @ _"}) is just list append,
-  and inversion of a permutation (written @{text "_\<^sup>-\<^sup>1"}) is just
-  list reversal. A disadvantage is that permutations do not have unique
-  representations as lists; we had to explicitly identify permutations according
-  to the relation
+
+%  Unfortunately, the type system of Isabelle/HOL is not a good fit for the way
+%  atoms and sorts are used in the original formulation of the nominal logic work.
+%  The reason is that one has to ensure that permutations are sort-respecting.
+%  This was done implicitly in the original nominal logic work \cite{Pitts03}.
+
+
+  With the separate atom types and the list representation of permutations it
+  is impossible to state an ``ill-sorted'' permutation, since the type system
+  excludes lists containing atoms of different type. However, whenever we
+  need to generalise induction hypotheses by quantifying over permutations, we
+  have to build cumbersome quantifications like
+
+  @{text [display,indent=10] "\<forall>\<pi>\<^isub>1 \<dots> \<forall>\<pi>\<^isub>n. \<dots>"}
+
+  \noindent
+  where the @{text "\<pi>\<^isub>i"} are of type @{text "(\<alpha>\<^isub>i \<times> \<alpha>\<^isub>i) list"}. 
+  The reason is that the permutation operation behaves differently for 
+  every @{text "\<alpha>\<^isub>i"}. Similarly, the notion of support
+
+  @{text [display,indent=10] "supp _ :: \<beta> \<Rightarrow> \<alpha> set"}
+
+  \noindent
+  which we will define later, cannot be
+  used to express the support of an object over \emph{all} atoms. The reason
+  is that support can behave differently for each @{text
+  "\<alpha>\<^isub>i"}. This problem is annoying, because if we need to know in
+  a statement that an object, say @{text "x"}, is finitely supported we end up
+  with having to state premises of the form
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{text "finite ((supp x) :: \<alpha>\<^isub>1 set) , \<dots>, finite ((supp x) :: \<alpha>\<^isub>n set)"}
+  \end{tabular}\hfill\numbered{fssequence}
+  \end{isabelle}
+
+
+
+
+
+
+
+
+
+  An advantage of the
+  list representation is that the basic operations on permutations are already
+  defined in the list library: composition of two permutations (written @{text
+  "_ @ _"}) is just list append, and inversion of a permutation (written
+  @{text "_\<^sup>-\<^sup>1"}) is just list reversal. A disadvantage is that
+  permutations do not have unique representations as lists; we had to
+  explicitly identify permutations according to the relation
+
   
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}l}

--- a/Pearl-jv/document/root.tex	Fri Oct 08 23:53:51 2010 +0100
+++ b/Pearl-jv/document/root.tex	Tue Oct 12 10:07:48 2010 +0100
@@ -37,7 +37,8 @@
 unified atom type and that represents permutations by bijective functions from
 atoms to atoms. Interestingly, we allow swappings, which are permutations
 build from two atoms, to be ill-sorted.  Furthermore we extend the nominal
-logic work with names that carry additional information.
+logic work with names that carry additional information and with abstractions
+that bind finite sets of names.
 \end{abstract}
 
 % generated text of all theories