
diff -r 61d30863e5d1 -r a9e63abf3feb Pearl-jv/Paper.thy
--- a/Pearl-jv/Paper.thy	Wed Mar 02 00:06:28 2011 +0000
+++ b/Pearl-jv/Paper.thy	Tue Mar 08 09:07:27 2011 +0000
@@ -44,11 +44,10 @@
 
 text {*
   Nominal Isabelle provides a proving infratructure for convenient reasoning
-  about programming language calculi involving binders, such as lambda abstractions or
-  quantifications in type schemes:
+  about syntax involving binders, such as lambda terms or type schemes:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  @{text "\<lambda>x. t       \<forall>{x\<^isub>1,\<dots>,x\<^isub>n}. \<tau>"}
+  @{text "\<lambda>x. t       \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. \<tau>"}
   \hfill\numbered{atomperm}
   \end{isabelle}
   
@@ -56,12 +55,59 @@
   At its core Nominal Isabelle is based on the nominal logic work by Pitts at
   al \cite{GabbayPitts02,Pitts03}, whose most basic notion is a
   sort-respecting permutation operation defined over a countably infinite
-  collection of sorted atoms. The nominal logic work has been starting
-  point for a number of formalisations, most notable Norrish \cite{norrish04} 
-  in HOL4, Aydemir et al \cite{AydemirBohannonWeirich07} in Coq and our own 
-  work in Isabelle/HOL.
+  collection of sorted atoms. The atoms are used for representing variable names
+  that might be bound or free. 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 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. 
+
+  The nominal logic work has been the starting point for a number of proving
+  infrastructures, most notable by Norrish \cite{norrish04} in HOL4, by
+  Aydemir et al \cite{AydemirBohannonWeirich07} in Coq and teh work by Urban
+  and Berghofer in Isabelle/HOL \cite{Urban08}. Its key attraction is a very
+  general notion, called \emph{support}, for the `set of free variables, or
+  atoms' of an object that applies not just to lambda terms and type schemes,
+  but also to sets, products, lists and even functions. The notion of support
+  is derived from the permutation operation defined over atoms. This
+  permutation operation, written @{text "_ \<bullet> _"}, has proved to be very
+  convenient for reasoning about syntax, in comparison to, say, arbitrary
+  renaming substitutions of atoms. The reason is that permutations are
+  bijective renamings of atoms and thus they can be easily `undone'---namely
+  by applying the inverse permutation. A corresponding inverse substitution 
+  might not exist in general, since renaming substitutions are only injective.  
+  Permutations also preserve many constructions when reasoning about syntax. 
+  For example validity of a typing context is preserved under permutations. 
+  Suppose a typing context @{text "\<Gamma>"} of the form
 
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{text "x\<^isub>1:\<tau>\<^isub>1, \<dots>, x\<^isub>n:\<tau>\<^isub>n"}
+  \end{isabelle}
+
+  \noindent
+  is said to be \emph{valid} provided none of its variables, or atoms, @{text "x\<^isub>i"}
+  occur twice. Then validity is preserved under
+  permutations in the sense that if @{text \<Gamma>} is valid then so is @{text "\<pi> \<bullet> \<Gamma>"} for
+  all permutations @{text "\<pi>"}. This is \emph{not} the case for arbitrary
+  renaming substitutions, as they might identify some variables in @{text \<Gamma>}. 
+  Permutations fit well with HOL's definitions. For example 
   
+
+  Because
+  of the good properties of permutations, we will be able to automate reasoning 
+  steps determining when a construction in HOL is
+  \emph{equivariant}. By equivariance we mean the property that every
+  permutation leaves an object unchanged, that is @{term "\<forall>\<pi>. \<pi> \<bullet> x = x"}.
+  This will often simplify arguments involving the notion of support.
+
+
+  There are a number of subtle differences between the nominal logic work by Pitts 
+  and the one we will present in this paper. Nominal 
+
+  In the nominal logic work, the `new quantifier' plays a prominent role.
+  
+
+
   Using a single atom type to represent atoms of different sorts and
   representing permutations as functions are not new ideas; see
   \cite{GunterOsbornPopescu09} \footnote{function rep.}  The main contribution
@@ -74,34 +120,30 @@
   depend on type annotations.
 
   The paper is organised as follows\ldots
+
+
+  Two binders
 *}
 
 section {* Sorted Atoms and Sort-Respecting Permutations *}
 
 text {*
-  The most basic notion in this work is a
+  The two most basic notions in the nominal logic work are
   sort-respecting permutation operation defined over a countably infinite
-  collection of sorted atoms. The atoms are used for representing variable names
-  that might be bound or free. 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 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. 
-
-
+  collection of sorted atoms. 
   The existing nominal logic work usually leaves implicit the sorting
   information for atoms and as far as we know leaves out a description of how
   sorts are represented.  In our formalisation, we therefore have to make a
   design decision about how to implement sorted atoms and sort-respecting
-  permutations. One possibility, which we described in \cite{Urban08}, is to 
-  have separate types for the different
-  kinds of atoms, say types @{text "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}. 
+  permutations. One possibility, which we described in \cite{Urban08}, is to
+  have separate types for the different kinds of atoms, say types @{text
+  "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}. However, this does not blend well with the
+  resoning infrastructure of type-classes in Isabelle/HOL (see Section ??? 
+  about related work).  Therefore we use here a single unified atom type to
+  represent atoms of different sorts. A basic requirement is that there must
+  be a countably infinite number of atoms of each sort.  This can be
+  implemented as the datatype
 
-  In the nominal logic work of Pitts, binders and bound variables are
-  represented by \emph{atoms}.  As stated above, we need to have different
-  \emph{sorts} of atoms to be able to bind different kinds of variables.  A
-  basic requirement is that there must be a countably infinite number of atoms
-  of each sort.  We implement these atoms as
 *}
 
           datatype atom\<iota> = Atom\<iota> string nat
@@ -110,13 +152,19 @@
   \noindent
   whereby the string argument specifies the sort of the atom.\footnote{A
   similar design choice was made by Gunter et al \cite{GunterOsbornPopescu09}
-  for their variables.}  (The use of type \emph{string} is merely for
-  convenience; any countably infinite type would work as well.) 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}
+  for their variables.}  The use of type \emph{string} for sorts is merely for
+  convenience; any countably infinite type would work as well. We have an
+  auxiliary function @{text sort} that is defined as 
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{thm sort_of.simps[no_vars, THEN eq_reflection]}
+  \end{isabelle}
+
+  \noindent
+  and we clearly have for every finite set @{text S}
   of atoms and every sort @{text s} the property:
 
-  \begin{proposition}\label{choosefresh}
+  \begin{proposition}\label{choosefresh}\mbox{}\\
   @{text "For a finite set of atoms S, there exists an atom a such that
   sort a = s and a \<notin> S"}.
   \end{proposition}
@@ -174,8 +222,8 @@
   the value of @{text "(a b)"} is unspecified.  However, this looked like a
   cumbersome solution, since sort-related side conditions would be required
   everywhere, even to unfold the definition.  It turned out to be more
-  convenient to actually allow the user to state ``ill-sorted'' swappings but
-  limit their ``damage'' by defaulting to the identity permutation in the
+  convenient to actually allow the user to state `ill-sorted' swappings but
+  limit their `damage' by defaulting to the identity permutation in the
   ill-sorted case:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -191,7 +239,7 @@
   @{text a} and @{text b}, and sort respecting. Therefore it is 
   a function in @{typ perm}. 
 
-  One advantage of using functions instead of lists as a representation for
+  One advantage of using functions as a representation for
   permutations is that for example the swappings
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -202,16 +250,17 @@
   \end{isabelle}
 
   \noindent
-  are \emph{equal}.  We do not have to use the equivalence relation shown
-  in~\eqref{permequ} to identify them, as we would if they had been represented
-  as lists of pairs.  Another advantage of the function representation is that
-  they form a (non-commutative) group provided we define
+  are \emph{equal}.  Therfore we can use for permutations HOL's built-in
+  principle of `replacing equals by equals in any context'. Another advantage
+  of the function representation is that they form a (non-commutative) group
+  provided we define
+
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm}
-  @{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{4mm}
-  @{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{4mm}
+  @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{5mm}
+  @{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{5mm}
+  @{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{5mm}
   @{thm minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^isub>2"]} 
   \end{tabular}
   \end{isabelle}
@@ -221,16 +270,15 @@
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  @{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]} \hspace{3mm}
-  @{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{3mm}
-  @{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{3mm}
+  @{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]} \hspace{5mm}
+  @{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{5mm}
+  @{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{5mm}
   @{thm group_add_class.left_minus[where a="\<pi>::perm"]} 
   \end{tabular}
   \end{isabelle}
 
   \noindent
-  Again this is in contrast to the list-of-pairs representation which does not
-  form a group.  The technical importance of this fact is that we can rely on
+  The technical importance of this fact is that we can rely on
   Isabelle/HOL's existing simplification infrastructure for groups, which will
   come in handy when we have to do calculations with permutations.
   Note that Isabelle/HOL defies standard conventions of mathematical notation
@@ -240,9 +288,8 @@
   nominal theory as smoothly as possible in Isabelle/HOL, we tolerate
   the non-standard notation in order to reuse the existing libraries.
 
-  By formalising permutations abstractly as functions, and using a single type
-  for all atoms, we can now restate the \emph{permutation properties} from
-  \eqref{permprops} as just the two equations
+  In order to reason abstractly about permutations, we state the following two 
+  \emph{permutation properties} 
   
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
@@ -252,14 +299,11 @@
   \end{isabelle} 
 
   \noindent
-  in which the permutation operations are of type @{text "perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} and so
-  have only a single type parameter.  Consequently, these properties are
-  compatible with the one-parameter restriction of Isabelle/HOL's type classes.
-  There is no need to introduce a separate type class instantiated for each
-  sort, like in the old approach.
-
-  The next notion allows us to establish generic lemmas involving the
-  permutation operation.
+  We state these properties in terms of Isabelle/HOL's type class 
+  mechanism \cite{}.
+  This allows us to delegate much of the resoning involved in 
+  determining whether these properties are satisfied to the type system.
+  For this we define
 
   \begin{definition}
   A type @{text "\<beta>"} is a \emph{permutation type} if the permutation
@@ -268,7 +312,8 @@
   \end{definition}
 
   \noindent
-  First, it follows from the laws governing
+  The type class also allows us to establish generic lemmas involving the
+  permutation operation. First, it follows from the laws governing
   groups that a permutation and its inverse cancel each other.  That is, for any
   @{text "x"} of a permutation type:
 
@@ -281,6 +326,7 @@
   \end{isabelle} 
   
   \noindent
+  ??? Proof
   Consequently, in a permutation type the permutation operation @{text "\<pi> \<bullet> _"}~~is bijective, 
   which in turn implies the property
 
@@ -316,16 +362,16 @@
 
   \begin{equation}\label{permdefs}
   \mbox{
-  \begin{tabular}{@ {}ll@ {\hspace{2mm}}l@ {}}
-  1) & atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\
-  2) & functions: &  @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\
-  3) & permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\
-  4) & sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-  5) & booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-  6) & lists: & @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+  \begin{tabular}{@ {}ll@ {\hspace{4mm}}l@ {}}
+  a) & atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\
+  b) & functions: &  @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\
+  c) & permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\
+  d) & sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+  e) & booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+  f) & lists: & @{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]}\\
-  7) & products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-  8) & nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+  g) & products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+  h) & nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
   \end{tabular}}
   \end{equation}
 




