
diff -r 0cb0c88b2cad -r e903c32ec24f Pearl-jv/Paper.thy
--- a/Pearl-jv/Paper.thy	Tue Oct 12 13:06:18 2010 +0100
+++ b/Pearl-jv/Paper.thy	Wed Oct 13 22:55:58 2010 +0100
@@ -13,6 +13,7 @@
   Rep_perm ("_") and
   swap ("'(_ _')" [1000, 1000] 1000) and
   fresh ("_ # _" [51, 51] 50) and
+  fresh_star ("_ #\<^sup>* _" [51, 51] 50) and
   Cons ("_::_" [78,77] 73) and
   supp ("supp _" [78] 73) and
   uminus ("-_" [78] 73) and
@@ -48,7 +49,7 @@
 
 text {*
   Nominal Isabelle provides a proving infratructure for convenient reasoning
-  about programming languages involving binders such as lambda abstractions or
+  about programming language calculi involving binders such as lambda abstractions or
   quantifications in type schemes:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -61,18 +62,22 @@
   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 binding, bound or free. Multiple sorts are necessary for being able to
+  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. 
 
-  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 have separate types for the different kinds of atoms, say @{text "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}. 
-  With this design one can represent
-  permutations as lists of pairs of atoms and the operation of applying
-  a permutation to an object as the overloaded function
+  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"}. With this
+  design one can represent permutations as lists of pairs of atoms and the
+  operation of applying a permutation to an object as the function
+
 
   @{text [display,indent=10] "_ \<bullet> _  ::  (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
 
@@ -93,8 +98,8 @@
 
   \noindent
   where we write @{text "(a b)"} for a swapping of atoms @{text "a"} and
-  @{text "b"}. For atoms of different type, the permutation operation
-  is defined as @{text "\<pi> \<bullet> c \<equiv> c"}.
+  @{text "b"}. For atoms with different type than the permutation, we 
+  define @{text "\<pi> \<bullet> c \<equiv> c"}.
 
   With the separate atom types and the list representation of permutations it
   is impossible in systems like Isabelle/HOL to state an ``ill-sorted''
@@ -108,7 +113,9 @@
   \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
+  every @{text "\<alpha>\<^isub>i"} and the type system does not allow use to have a
+  single quantification to stand for all permutations. Similarly, the 
+  notion of support
 
   @{text [display,indent=10] "supp _ :: \<beta> \<Rightarrow> \<alpha> set"}
 
@@ -127,19 +134,20 @@
   \end{isabelle}
 
   \noindent
-  Because of these disadvantages, we will use a single unified atom type to 
-  represent atoms of different sorts. As a result, we have to deal with the
+  Because of these disadvantages, we will use in this paper a single unified atom type to 
+  represent atoms of different sorts. Consequently, we have to deal with the
   case that a swapping of two atoms is ill-sorted: we cannot rely anymore on
-  the type systems to exclude them.
+  the type systems to exclude them. 
 
-  We also will not represent permutations as lists of pairs of atoms.  An
+  We also will not represent permutations as lists of pairs of atoms (as done in
+  \cite{Urban08}).  Although an
   advantage of this representation is that the basic operations on
   permutations are already defined in Isabelle's 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. Another advantage is that there is a well-understood
-  induction principle for lists. A disadvantage, however, is that permutations 
-  do not have unique representations as lists; we have to explicitly identify
+  list reversal, and another advantage is that there is a well-understood
+  induction principle for lists, a disadvantage is that permutations 
+  do not have unique representations as lists. We have to explicitly identify
   them according to the relation
 
   
@@ -151,7 +159,7 @@
 
   \noindent
   This is a problem when lifting the permutation operation to other types, for
-  example sets, functions and so on, we need to ensure that every definition
+  example sets, functions and so on. For this we need to ensure that every definition
   is well-behaved in the sense that it satisfies some
   \emph{permutation properties}. In the list representation we need
   to state these properties as follows:
@@ -167,24 +175,25 @@
 
   \noindent
   where the last clause explicitly states that the permutation operation has
-  to produce the same result for related permutations.  Moreover, permutations
-  as list do not satisfy the usual properties about groups. This means by
+  to produce the same result for related permutations.  Moreover, 
+  ``permutations-as-lists'' do not satisfy the group properties. This means by
   using this representation we will not be able to reuse the extensive
-  reasoning infrastructure in Isabelle about groups.  Therefore, we will use
-  in this paper a unique representation for permutations by representing them
-  as functions from atoms to atoms.
+  reasoning infrastructure in Isabelle about groups.  Because of this, we will represent
+  in this paper permutations as functions from atoms to atoms. This representation
+  is unique and satisfies the laws of non-commutative groups.
 
   Using a single atom type to represent atoms of different sorts and
-  representing permutations as functions are not new ideas.  The main
-  contribution of this paper is to show an example of how to make better
-  theorem proving tools by choosing the right level of abstraction for the
-  underlying theory---our design choices take advantage of Isabelle's type
-  system, type classes and reasoning infrastructure.  The novel technical
-  contribution is a mechanism for dealing with ``Church-style'' lambda-terms
-  \cite{Church40} and HOL-based languages \cite{PittsHOL4} where variables and
-  variable binding depend on type annotations.
+  representing permutations as functions are not new ideas; see
+  \cite{GunterOsbornPopescu09} \footnote{function rep.}  The main contribution
+  of this paper is to show an example of how to make better theorem proving
+  tools by choosing the right level of abstraction for the underlying
+  theory---our design choices take advantage of Isabelle's type system, type
+  classes and reasoning infrastructure.  The novel technical contribution is a
+  mechanism for dealing with ``Church-style'' lambda-terms \cite{Church40} and
+  HOL-based languages \cite{PittsHOL4} where variables and variable binding
+  depend on type annotations.
 
-  The paper is organised as follows
+  The paper is organised as follows\ldots
 *}
 
 section {* Sorted Atoms and Sort-Respecting Permutations *}
@@ -203,7 +212,7 @@
   \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 type \emph{string} is merely for
+  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}
@@ -374,7 +383,7 @@
   \end{isabelle} 
   
   \noindent
-  Consequently, in a permutation type the permutation operation @{text "\<pi> \<bullet> _"} is bijective, 
+  Consequently, in a permutation type the permutation operation @{text "\<pi> \<bullet> _"}~~is bijective, 
   which in turn implies the property
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -386,25 +395,41 @@
   \end{isabelle} 
   
   \noindent
+  We can also show that the following property holds for any permutation type.
+
+  \begin{lemma}\label{permutecompose} 
+  Given @{term x} is of permutation type, then 
+  @{text "\<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x) = (\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}.
+  \end{lemma}
+
+  \begin{proof} The proof is as follows:
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}[b]{@ {}rcl@ {\hspace{8mm}}l}
+  @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> x"}
+  & @{text "="} & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> (-\<pi>\<^isub>1) \<bullet> \<pi>\<^isub>1 \<bullet> x"} & by \eqref{cancel}\\
+  & @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2 - \<pi>\<^isub>1) \<bullet> \<pi>\<^isub>1 \<bullet> x"}  & by {\rm(\ref{newpermprops}.@{text "ii"})}\\
+  & @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}\\
+  \end{tabular}\hfill\qed
+  \end{isabelle}
+  \end{proof}
+
+  \noindent
   In order to lift the permutation operation to other types, we can define for:
 
-  \begin{isabelle}
-  \begin{tabular}{@ {}c@ {\hspace{-1mm}}c@ {}}
-  \begin{tabular}{@ {}r@ {\hspace{2mm}}l@ {}}
-  atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\
-  functions: &  @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\
-  permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\
-  sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-   booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-  \end{tabular} &
-  \begin{tabular}{@ {}r@ {\hspace{2mm}}l@ {}}
-  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]}\\[2mm]
-  products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-  nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-  \end{tabular}
-  \end{tabular}
-  \end{isabelle}
+  \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]}\\
+      & & @{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]}\\
+  \end{tabular}}
+  \end{equation}
 
   \noindent
   and then establish:
@@ -430,42 +455,15 @@
   \end{tabular}\hfill\qed
   \end{isabelle}
   \end{proof}
-
-  \noindent
-  The main point is that the above reasoning blends smoothly with the reasoning
-  infrastructure of Isabelle/HOL; no custom ML-code is necessary and a single
-  type class suffices. We can also show once and for all that the following
-  property---which caused so many headaches in our earlier setup---holds for any
-  permutation type.
-
-  \begin{lemma}\label{permutecompose} 
-  Given @{term x} is of permutation type, then 
-  @{text "\<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x) = (\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}.
-  \end{lemma}
-
-  \begin{proof} The proof is as follows:
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \begin{tabular}[b]{@ {}rcl@ {\hspace{8mm}}l}
-  @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> x"}
-  & @{text "="} & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> (-\<pi>\<^isub>1) \<bullet> \<pi>\<^isub>1 \<bullet> x"} & by \eqref{cancel}\\
-  & @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2 - \<pi>\<^isub>1) \<bullet> \<pi>\<^isub>1 \<bullet> x"}  & by {\rm(\ref{newpermprops}.@{text "ii"})}\\
-  & @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}\\
-  \end{tabular}\hfill\qed
-  \end{isabelle}
-  \end{proof}
-
 *}
 
 section {* Equivariance *}
 
 text {*
-
-  An \emph{equivariant} function or predicate is one that is invariant under
-  the swapping of atoms.  Having a notion of equivariance with nice logical
-  properties is a major advantage of bijective permutations over traditional
-  renaming substitutions \cite[\S2]{Pitts03}.  Equivariance can be defined
-  uniformly for all permutation types, and it is satisfied by most HOL
-  functions and constants.
+  An important notion in the nominal logic work is \emph{equivariance}.
+  An equivariant function or predicate is one that is invariant under
+  the swapping of atoms. This notion can be defined
+  uniformly as follows:
 
 
   \begin{definition}\label{equivariance}
@@ -501,8 +499,14 @@
   property. Similarly for functions with more than one argument. 
 
   Both formulations of equivariance have their advantages and disadvantages:
-  \eqref{altequivariance} is often easier to establish. For example we 
-  can easily show that equality is equivariant
+  the definition, \eqref{permutefunapp} and (\ref{permdefs}.2) lead to a simple
+  rewrite system that pushes permutations inside a term until they reach
+  either function constants or variables. The permutations in front of
+  equivariant functions disappear. Such a rewrite system is often very helpful
+  in determining whether @{text "p \<bullet> t = t"} holds for a compound term @{text t}. In contrast
+  \eqref{altequivariance} is usually easier to establish, since statements are
+  commonly given in a form where functions are fully applied. For example we can
+  easily show that equality is equivariant
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -524,9 +528,7 @@
   \end{isabelle} 
 
   \noindent
-  for all @{text a}, @{text b} and @{text \<pi>}.  These equivariance properties
-  are tremendously helpful later on when we have to push permutations inside
-  terms.
+  for all @{text a}, @{text b} and @{text \<pi>}.  
 *}
 
 
@@ -551,6 +553,12 @@
   @{thm [display,indent=10] fresh_def[no_vars]}
 
   \noindent
+  We also use the notation @{thm (lhs) fresh_star_def[no_vars]} for sets ot atoms 
+  defined as follows
+  
+  @{thm [display,indent=10] fresh_star_def[no_vars]}
+
+  \noindent
   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}, leave 
@@ -638,22 +646,19 @@
   one often has to calculate the support of some concrete object. This is 
   straightforward for example for booleans, nats, products and lists:
 
-  \begin{center}
-  \begin{tabular}{@ {}c@ {\hspace{2mm}}c@ {}}
+  \begin{equation}
+  \mbox{
   \begin{tabular}{@ {}r@ {\hspace{2mm}}l}
   @{text "booleans"}: & @{term "supp b = {}"}\\
   @{text "nats"}:     & @{term "supp n = {}"}\\
   @{text "products"}: & @{thm supp_Pair[no_vars]}\\
-  \end{tabular} &
-  \begin{tabular}{r@ {\hspace{2mm}}l@ {}}
   @{text "lists:"} & @{thm supp_Nil[no_vars]}\\
                    & @{thm supp_Cons[no_vars]}\\
-  \end{tabular}
-  \end{tabular}
-  \end{center}
+  \end{tabular}}
+  \end{equation}
 
   \noindent
-  But establishing the support of atoms and permutations in our setup here is a bit 
+  But establishing the support of atoms and permutations is a bit 
   trickier. To do so we will use the following notion about a \emph{supporting set}.
   
   \begin{definition}
@@ -773,21 +778,19 @@
   support, then Proposition~\ref{choosefresh} allows us to choose for @{text x} a 
   fresh atom with arbitrary sort. This is an important operation in Nominal
   Isabelle in situations where, for example, a bound variable needs to be
-  renamed. To allow such a choice, we only have to assume \emph{one} premise
-  of the form @{text "finite (supp x)"}
-  for each @{text x}. Compare that with the sequence of premises in our earlier
-  version of Nominal Isabelle (see~\eqref{fssequence}). For more convenience we
+  renamed. To allow such a choice, we only have to assume that 
+  @{text "finite (supp x)"} holds. For more convenience we
   can define a type class for types where every element has finite support, and
   prove that the types @{term "atom"}, @{term "perm"}, lists, products and
-  booleans are instances of this type class. Then \emph{no} premise is needed,
-  as the type system of Isabelle/HOL can figure out automatically when an object
-  is finitely supported.
+  booleans are instances of this type class. 
 
-  Unfortunately, this does not work for sets or Isabelle/HOL's function type.
-  There are functions and sets definable in Isabelle/HOL for which the finite
-  support property does not hold.  A simple example of a function with
-  infinite support is the function that returns the natural number of an atom
-  
+  Unfortunately, this does not work for sets or Isabelle/HOL's function
+  type.\footnote{Isabelle/HOL takes the type @{text "\<alpha> set"} as an abbreviation
+  of @{text "\<alpha> \<Rightarrow> bool"}.}  There are functions and sets definable in
+  Isabelle/HOL for which the finite support property does not hold.  A simple
+  example of a function with infinite support is the function that returns the
+  natural number of an atom
+
   @{text [display, indent=10] "nat_of (Atom s i) \<equiv> i"}
 
   \noindent
@@ -807,7 +810,6 @@
   \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
@@ -818,8 +820,8 @@
 section {* Support of Finite Sets *}
 
 text {*
-  Sets is one instance of a type that is not generally finitely supported. 
-  However, it can be easily derived that finite sets of atoms are finitely
+  As shown above, sets is one instance of a type that is not generally finitely supported. 
+  However, we can easily show that finite sets of atoms are finitely
   supported, because their support can be characterised as:
 
   \begin{lemma}\label{finatomsets}
@@ -830,7 +832,8 @@
   finite-supp-unique
   \end{proof}
 
-  More difficult is it to establish that finite sets of finitely 
+  \noindent
+  More difficult, however, is it to establish that finite sets of finitely 
   supported objects are finitely supported. 
 *}
 
@@ -844,7 +847,7 @@
   one draw back: it does not come readily with an induction principle. 
   Such an induction principle is handy for deriving properties like
   
-  @{thm [display, indent=10] supp_perm_eq}
+  @{thm [display, indent=10] supp_perm_eq[no_vars]}
 
   \noindent
   However, it is not too difficult to derive an induction principle, 
@@ -1372,6 +1375,11 @@
 
 text {*
   Add here comparison with old work.
+
+
+  The main point is that the above reasoning blends smoothly with the reasoning
+  infrastructure of Isabelle/HOL; no custom ML-code is necessary and a single
+  type class suffices. 
 *}
 
 




