diff -r cdc96d79bbba -r 6ba52f3a1542 Pearl-jv/Paper.thy
--- a/Pearl-jv/Paper.thy	Sat Apr 09 00:29:40 2011 +0100
+++ b/Pearl-jv/Paper.thy	Sat Apr 09 13:44:49 2011 +0800
@@ -67,7 +67,11 @@
   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 aim of this paper is to
+  infinite collection of sorted atoms. 
+
+
+
+  The aim of this paper is to
   describe how we adapted this work so that it can be implemented in a
   theorem prover based on Higher-Order Logic (HOL). For this we
   present the definition we made in the implementation and also review
@@ -314,11 +318,11 @@
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  @{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]}\\
-  @{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{9mm}
-  @{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{9mm}
-  @{thm group_add_class.left_minus[where a="\<pi>::perm"]} 
-  \end{tabular}
+  i)~~@{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]}\\
+  ii)~~@{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{9mm}
+  iii)~~@{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{9mm}
+  iv)~~@{thm group_add_class.left_minus[where a="\<pi>::perm"]} 
+  \end{tabular}\hfill\numbered{grouplaws}
   \end{isabelle}
 
   \noindent
@@ -327,23 +331,28 @@
   come in handy when we have to do calculations with permutations.
   Note that Isabelle/HOL defies standard conventions of mathematical notation
   by using additive syntax even for non-commutative groups.  Obviously,
-  composition of permutations is not commutative in general, because @{text
-  "\<pi>\<^sub>1 + \<pi>\<^sub>2 \<noteq>  \<pi>\<^sub>2 + \<pi>\<^sub>1"}.  But since the point of this paper is to implement the
+  composition of permutations is not commutative in general; for example
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{text "(a b) + (b c) \<noteq> (b c) + (a b)"}
+  \end{isabelle} 
+
+  \noindent
+  But since the point of this paper is to implement the
   nominal theory as smoothly as possible in Isabelle/HOL, we tolerate
   the non-standard notation in order to reuse the existing libraries.
 
-  A \emph{permutation operation}, written @{text "\<pi> \<bullet> x"}, applies a permutation 
-  @{text "\<pi>"} to an object @{text "x"} of type @{text \<beta>}, say. 
-  This operation has the type
+  A \emph{permutation operation}, written infix as @{text "\<pi> \<bullet> x"},
+  applies a permutation @{text "\<pi>"} to an object @{text "x"} of type
+  @{text \<beta>}, say.  This operation has the type
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   @{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
   \end{isabelle} 
 
   \noindent
-  Isabelle/HOL will allow us to give a definition of this operation for
-  `base' types, such as atoms, permutations, booleans and natural numbers, 
-  and for type-constructors, such as functions, sets, lists and products. 
+  Isabelle/HOL allows us to give a definition of this operation for
+  `base' types, such as atoms, permutations, booleans and natural numbers:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}}
@@ -351,12 +360,20 @@
   permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\
   booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
   nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+  \end{tabular}\hfill\numbered{permdefsbase}
+  \end{isabelle}
+
+  \noindent
+  and for type-constructors, such as functions, sets, lists and products:
+  
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}}
   functions: &  @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\
   sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
   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]}\\
   products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-  \end{tabular}\hfill\numbered{permdefs}
+  \end{tabular}\hfill\numbered{permdefsconstrs}
   \end{isabelle}
 
   In order to reason abstractly about this operation, 
@@ -371,8 +388,9 @@
   \end{isabelle} 
 
   \noindent
-  From these properties and the laws about groups follows that a 
-  permutation and its inverse cancel each other. That is
+  From these properties and the laws about groups
+  (\ref{grouplaws}.{\it iv }) follows that a permutation and its inverse
+  cancel each other. That is
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -447,16 +465,16 @@
   and establish:
 
   \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"}, 
-  @{text perm}, @{term "\<beta> set"}, @{term "\<beta> list"}, @{term "\<beta>\<^isub>1 \<times> \<beta>\<^isub>2"},
-  @{text bool} and @{text "nat"}.
+  The types @{type atom}, @{type perm}, @{type bool} and @{type nat}
+  are permutation types, and if @{text \<beta>}, @{text "\<beta>\<^isub>1"} and @{text
+  "\<beta>\<^isub>2"} are permutation types, then so are \mbox{@{text "\<beta>\<^isub>1 \<Rightarrow> \<beta>\<^isub>2"}},
+  @{text "\<beta> set"}, @{text "\<beta> list"} and @{text "\<beta>\<^isub>1 \<times> \<beta>\<^isub>2"}.
   \end{theorem}
 
   \begin{proof}
   All statements are by unfolding the definitions of the permutation
   operations and simple calculations involving addition and
-  minus. With permutations for example we have
+  minus. In case of permutations for example we have
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}[b]{@ {}rcl}
@@ -487,6 +505,8 @@
   @{text x} for variables. We assume HOL-terms are fully typed, but for the
   sake of greater legibility we leave the typing information implicit.  We
   also assume the usual notions for free and bound variables of a HOL-term.
+  It is custom in HOL to regard terms equal modulo alpha-, beta- and 
+  eta-equivalence.
 
   An equivariant HOL-term is one that is invariant under the
   permutation operation. This notion can be defined in Isabelle/HOL 
@@ -498,6 +518,10 @@
   \end{definition}
 
   \noindent
+  We will be mainly interested in the case where @{text t} is a constant, but
+  of course there is no way to restrict this definition in Isabelle/HOL to just
+  this case.  
+
   There are a number of equivalent formulations for the equivariance
   property.  For example, assuming @{text t} is of permutation type @{text "\<alpha> \<Rightarrow>
   \<beta>"}, then equivariance can also be stated as
@@ -530,12 +554,11 @@
 
   \noindent
   using the permutation operation on booleans and property
-  \eqref{permuteequ}. 
-  Lemma~\ref{permutecompose} establishes that the
+  \eqref{permuteequ}.  Lemma~\ref{permutecompose} establishes that the
   permutation operation is equivariant. The permutation operation for
-  lists and products, shown in \eqref{permdefs}, state that the
+  lists and products, shown in \eqref{permdefsconstrs}, state that the
   constructors for products, @{text "Nil"} and @{text Cons} are
-  equivariant. Furthermore a simple calculation will show that our 
+  equivariant. Furthermore a simple calculation will show that our
   swapping functions are equivariant, that is
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -552,21 +575,102 @@
   "\<not>"} and @{text "\<longrightarrow>"} are all equivariant (see ??? intro)
 
   In contrast, the advantage of Definition \ref{equivariance} is that
-  it leads to a simple rewrite system. Consider the following oriented
-  versions
+  it leads to a simple rewrite system that allows us to `push' a
+  permutation towards the leaves in a HOL-term (i.e.~constants and free
+  variables).  The permutation disappears in cases where the
+  constants are equivariant. Given a database of equivariant constants, 
+  we can implement a decision procedure that helps to find out when
+  a compound term is equivariant. A permutation @{text \<pi>} can be pushed over
+  applications and abstractions in a HOL-term as follows
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}lrcl}
+  i) & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & @{text "\<longmapsto>"} & @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\\
+  ii) & @{text "\<pi> \<bullet> (\<lambda>x. t)"} & @{text "\<longmapsto>"} & @{text "\<lambda>x. \<pi> \<bullet> (t[x :=  (-\<pi>) \<bullet> x])"}\\
+  \end{tabular}\hfill\numbered{rewriteapplam}
+  \end{isabelle}
+
+  \noindent
+  The first rewrite rule we established as equation in \eqref{permutefunapp};
+  the second follows from the definition of permutations acting on functions
+  and the fact that HOL-terms are considered equal modulo beta-reduction.
+  The inverse permutations that are introduced by the second rewrite rule
+  can be removed using the additional rewrite rule
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}rcl}
+  @{term "\<pi> \<bullet> (- \<pi>) \<bullet> x"} & @{text "\<longmapsto>"} & @{term "x"}
+  \end{tabular}\hfill\numbered{rewriteunpermute}
+  \end{isabelle}
+
+  \noindent
+  and permutations in front of equivariant constants can be removed by the
+  rule
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}rcl}
-  @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & @{text "\<longmapsto>"} & @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\\
-  @{text "\<pi> \<bullet> (\<lambda>x. t)"} & @{text "\<longmapsto>"} & @{text "\<lambda>x. \<pi> \<bullet> (t[x :=  (-\<pi>) \<bullet> x])"}\\
-  @{term "\<pi> \<bullet> (- \<pi>) \<bullet> x"} & @{text "\<longmapsto>"} & @{term "x"}\\
-  \end{tabular}\hfill\numbered{swapeqvt}
+  @{term "\<pi> \<bullet> c"} & @{text "\<longmapsto>"} & @{term "c"}
+  \end{tabular}\hfill\numbered{rewriteconsts}
   \end{isabelle}
-  
-  of the equations 
 
 
-together with the permutation 
+  \noindent
+  By a meta-argument, that means one we cannot formalise inside
+  Isabelle/HOL, we can convince ourselves that the rewriting process
+  of first pushing a permutation inside a term using
+  \eqref{rewriteapplam}, then removing permutation in front of bound
+  variables using \eqref{rewriteunpermute} and finally removing all
+  permutations in front of equivariant constants must terminate: the
+  size of the term gets smaller in \eqref{rewriteapplam} if we do not
+  count the inverse permutations introduced by the second rewrite rule
+  and there can only be finitely many bound variables in a term
+  (similarly equivariant constants), therefore only finitely many
+  applications of \eqref{rewriteunpermute} and
+  \eqref{rewriteconsts}. The only problem is that instances where
+  rules (\ref{rewriteapplam}.{\it i}) or rules
+  \eqref{rewriteunpermute} apply `overlap' and potentially our measure
+  increases.  Consider for example the term @{term "\<pi> \<bullet> (\<lambda>x. x)"},
+  whose final reduct should just be \mbox{@{term "\<lambda>x. x"}}. Using
+  (\ref{rewriteapplam}.{\it ii}), the term can reduce to @{term
+  "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet> x"}, to which we can apply \eqref{rewriteunpermute}
+  in order to obtain the desired result.  However, the subterm term @{text "(-
+  \<pi>) \<bullet> x"} is also an application (in fact three nested ones). Therefore
+  @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet> x"} can also rewrite 
+  to @{text "\<lambda>x. (- (\<pi> \<bullet> \<pi>)) \<bullet> (\<pi> \<bullet> x)"} to which we cannot apply 
+  (\ref{rewriteapplam}.{\it i}) directly and even worse our measure 
+  increased. In order to distinguish situations where \eqref{rewriteconsts}
+  should apply instead of  (\ref{rewriteapplam}.{\it i}) we use a standard
+  trick in HOL. We introduce a separate definition for terms of the form
+  @{text "(- \<pi>) \<bullet> x"}, namely as
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{term "unpermute \<pi> x \<equiv> (- \<pi>) \<bullet> x"}
+  \end{isabelle}
+
+  \noindent
+  With this trick, we can reformulate our rewrite rules pushing a permutation @{text \<pi>}
+  inside a term as follows
+  
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}lrcl}
+  i) & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & @{text "\<longmapsto>"} & @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\hspace{45mm}\mbox{}\\
+  \multicolumn{4}{r}{provided @{text "t\<^isub>1 t\<^isub>2"} is not of the form @{text "unpermute \<pi> x"}}\smallskip\\
+  ii) & @{text "\<pi> \<bullet> (\<lambda>x. t)"} & @{text "\<longmapsto>"} & @{text "\<lambda>x. \<pi> \<bullet> (t[x := unpermute \<pi> x])"}\\
+  iii) & @{text "\<pi> \<bullet> (unpermute \<pi> x)"} & @{text "\<longmapsto>"} & @{term x}\\
+  iv) &  @{term "\<pi> \<bullet> c"} & @{text "\<longmapsto>"} & @{term "c"}\hspace{6mm}provided @{text c} is equivariant\\
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  In this rewrite systems no rule overlaps. Taking the measure
+  consisting of lexicographically ordered pairs whose first component
+  is the size of the term (without counting @{text unpermutes}) and
+  the second is the number of occurences of @{text "unpermute \<pi> x"}
+  and @{text "\<pi> \<bullet> c"}, then each rule is strictly decreasing.
+  Consequently the process of applying these rules must terminate.
+
+
+  together with the permutation 
   operation for functions and the properties in \eqref{permutefunapp} and \eqref{cancel}
   leads to a simple rewrite system that pushes permutations inside a term until they reach
   either function constants or variables. The permutations in front of
@@ -599,7 +703,7 @@
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}[b]{@ {}c@ {\hspace{2mm}}l@ {\hspace{8mm}}l}
   & @{text "\<pi> \<bullet> (\<lambda>x. t)"}\\
-  @{text "\<equiv>"} & @{text "\<lambda>y. \<pi> \<bullet> ((\<lambda>x. t) ((-\<pi>) \<bullet> y))"} & by \eqref{permdefs}\\
+  @{text "\<equiv>"} & @{text "\<lambda>y. \<pi> \<bullet> ((\<lambda>x. t) ((-\<pi>) \<bullet> y))"} & by \eqref{permdefsconstrs}\\
 
   \end{tabular}\hfill\qed
   \end{isabelle}