
diff -r 8f833ebc4b58 -r 64a03564bc24 Pearl-jv/Paper.thy
--- a/Pearl-jv/Paper.thy	Sun Apr 10 07:41:52 2011 +0800
+++ b/Pearl-jv/Paper.thy	Sun Apr 10 14:13:55 2011 +0800
@@ -351,6 +351,7 @@
   \end{isabelle} 
 
   \noindent
+  and will be defined over the hierarchie of types.
   Isabelle/HOL allows us to give a definition of this operation for
   `base' types, such as atoms, permutations, booleans and natural numbers:
 
@@ -388,9 +389,8 @@
   \end{isabelle} 
 
   \noindent
-  From these properties and the laws about groups
-  (\ref{grouplaws}.{\it iv }) follows that a permutation and its inverse
-  cancel each other. That is
+  From these properties and law (\ref{grouplaws}.{\it iv}) about groups 
+  follows that a permutation and its inverse cancel each other. That is
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -478,10 +478,11 @@
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}[b]{@ {}rcl}
-  @{text "0 \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "0 + \<pi>' - 0 = \<pi>'"}\\
+  @{text "0 \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "0 + \<pi>' - 0 = \<pi>'"}\smallskip\\
   @{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}
@@ -491,9 +492,10 @@
 
 text {*
   An important notion in the nominal logic work is
-  \emph{equivariance}.  In order to prove properties about this notion, 
-  let us first define \emph{HOL-terms}. They are given 
-  by the grammar
+  \emph{equivariance}.  It will enable us to characterise how
+  permutations act upon compound statements in HOL by analysing how
+  these statements are constructed.  To do so, let us first define
+  \emph{HOL-terms}. They are given by the grammar
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   @{text "t ::= c | x | t\<^isub>1 t\<^isub>2 | \<lambda>x. t"}
@@ -501,26 +503,26 @@
   \end{isabelle} 
 
   \noindent
-  whereby @{text c} stands for constant symbols, or short constants, and
-  @{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.
+  whereby @{text c} stands for constants and @{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.  Furthermore, it is custom in HOL to regard terms as 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 
+  An \emph{equivariant} HOL-term is one that is invariant under the
+  permutation operation. This can be defined in Isabelle/HOL 
   as follows:
 
   \begin{definition}[Equivariance]\label{equivariance}
-  A  HOL-term @{text t} with permutation type is \emph{equivariant} provided 
+  A  HOL-term @{text t} is \emph{equivariant} provided 
   @{term "\<pi> \<bullet> t = t"} holds for all permutations @{text "\<pi>"}.
   \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.  
+  We will primarily be interested in the cases where @{text t} is a constant, but
+  of course there is no way to restrict this definition in Isabelle/HOL so that it
+  applies to just constants.  
 
   There are a number of equivalent formulations for the equivariance
   property.  For example, assuming @{text t} is of permutation type @{text "\<alpha> \<Rightarrow>
@@ -533,15 +535,17 @@
   \end{isabelle} 
 
   \noindent
+  We will call this formulation of equivariance in \emph{fully applied form}.
   To see that this formulation implies the definition, we just unfold
   the definition of the permutation operation for functions and
   simplify with the equation and the cancellation property shown in
   \eqref{cancel}. To see the other direction, we use
   \eqref{permutefunapp}. Similarly for HOL-terms that take more than
-  one argument.
+  one argument. The point to note is that equivariance and equivariance in fully
+  applied form are always interderivable.
 
   Both formulations of equivariance have their advantages and
-  disadvantages: \eqref{altequivariance} is usually easier to
+  disadvantages: \eqref{altequivariance} is usually more convenient to
   establish, since statements in Isabelle/HOL are commonly given in a
   form where functions are fully applied. For example we can easily
   show that equality is equivariant
@@ -570,113 +574,139 @@
   \noindent
   for all @{text a}, @{text b} and @{text \<pi>}. Also the booleans
   @{const True} and @{const False} are equivariant by the definition
-  of the permutation operation for booleans.  It is also easy to see
+  of the permutation operation for booleans. It is easy to see
   that the boolean operators, like @{text "\<and>"}, @{text "\<or>"}, @{text
-  "\<not>"} and @{text "\<longrightarrow>"} are all equivariant (see ??? intro)
+  "\<not>"} and @{text "\<longrightarrow>"}, are all equivariant too. (see ??? intro)
 
   In contrast, the advantage of Definition \ref{equivariance} is that
-  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 into
-  applications and abstractions in a HOL-term as follows
+  it leads to a relatively simple rewrite system that allows us to `push' a permutation,
+  say @{text \<pi>}, towards the leaves of a HOL-term (i.e.~constants and
+  variables).  Then the permutation disappears in cases where the
+  constants are equivariant, since by Definition \ref{equivariance} we
+  have @{term "\<pi> \<bullet> c = c"}. What we will show next is that for a HOL-term
+  @{term t} containing only equivariant constants, a permutation can be pushed
+  inside this term and the only instances remaining are in front of
+  the free variables of @{text t}. We can only show this by a meta-argument, 
+  that means one we cannot formalise inside Isabelle/HOL. But we can invoke
+  it in form of a tactic programmed on the ML-level of Isabelle/HOL.
+  This tactic is a rewrite systems consisting of `oriented' equations. 
+
+  A permutation @{text \<pi>} can be 
+  pushed into applications and abstractions 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])"}\\
+  i) & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & $\stackrel{\rightharpoonup}{=}$ 
+        & @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\\
+  ii) & @{text "\<pi> \<bullet> (\<lambda>x. t)"} & $\stackrel{\rightharpoonup}{=}$ & @{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 first rule we established 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
+  and the fact that HOL-terms are equal modulo beta-equivalence.
+  Once the permutations are pushed towards the leaves we need the
+  following two rules
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \begin{tabular}{@ {}rcl}
-  @{term "\<pi> \<bullet> (- \<pi>) \<bullet> x"} & @{text "\<longmapsto>"} & @{term "x"}
-  \end{tabular}\hfill\numbered{rewriteunpermute}
+  \begin{tabular}{@ {}lrcl}
+  iii) & @{term "\<pi> \<bullet> (- \<pi>) \<bullet> x"} & $\stackrel{\rightharpoonup}{=}$ & @{term "x"}\\
+  iv) &  @{term "\<pi> \<bullet> c"} & $\stackrel{\rightharpoonup}{=}$ & 
+            @{term "c"}\hspace{6mm}provided @{text c} is equivariant\\
+  \end{tabular}\hfill\numbered{rewriteother}
   \end{isabelle}
 
   \noindent
-  and permutations in front of equivariant constants can be removed by the
-  rule
+  in order to remove permuations in front of bound variables and equivariant constants.
+  
+  In order to obtain a terminating rewrite system, we have to be
+  careful with rule ({\it i}). It can lead to a loop whenever
+  \mbox{@{text "t\<^isub>1 t\<^isub>2"}} is of the form @{text "\<pi>' \<bullet> t'"}. Consider
+  for example the infinite reduction sequence
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \begin{tabular}{@ {}rcl}
-  @{term "\<pi> \<bullet> c"} & @{text "\<longmapsto>"} & @{term "c"}
-  \end{tabular}\hfill\numbered{rewriteconsts}
+  \begin{tabular}{@ {}l}
+  @{text "\<pi> \<bullet> (\<pi>' \<bullet> t)"}~~$\stackrel{\rightharpoonup}{=}\ldots\stackrel{\rightharpoonup}{=}$\\
+  @{text "(\<pi> \<bullet> \<pi>') \<bullet> (\<pi> \<bullet> t)"}~~$\stackrel{\rightharpoonup}{=}\ldots\stackrel{\rightharpoonup}{=}$\\
+  @{text "((\<pi> \<bullet> \<pi>') \<bullet> \<pi>) \<bullet> ((\<pi> \<bullet> \<pi>') \<bullet> t)"}~~$\stackrel{\rightharpoonup}{=}\ldots$\\
+  \end{tabular}
   \end{isabelle}
 
-
   \noindent
-  By a meta-argument, that means one we cannot formalise inside
-  Isabelle/HOL, we can convince ourselves that the strategy of 
-  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
+  where the last step is again an instance of the first term, but it is
+  bigger (note that for the permutation operation we have that @{text
+  "\<pi> \<bullet> (op \<bullet>) = (op \<bullet>)"} since as shown in Lemma \ref{permutecompose}
+  \mbox{@{text "(op \<bullet>)"}} is equivariant). In order to avoid this loop
+  we need to apply these rules using an `outside to inside' strategy.
+  This strategy is sufficient since we are only interested of rewriting
+  terms of the form @{term "\<pi> \<bullet> t"}.
+
+  Another problem we have to avoid is that the rules ({\it i}) and
+  ({\it iii}) can `overlap'. For this note that
+  the term @{term "\<pi> \<bullet>(\<lambda>x. x)"} reduces to @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet>
+  x"}, to which we can apply rule ({\it iii}) in order to obtain
+  @{term "\<lambda>x. x"}, as is desired.  However, the subterm term @{text
+  "(- \<pi>) \<bullet> x"} is also an application. Consequently, the term 
+  @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet>x"} can reduce to @{text "\<lambda>x. (- (\<pi> \<bullet> \<pi>)) \<bullet> (\<pi> \<bullet> x)"} using
+  ({\it i}).  Now we cannot apply rule ({\it iii}) anymore and even
+  worse the measure we will introduce shortly increases. On the
+  other hand, if we started with the term @{text "\<pi> \<bullet> ((- \<pi>) \<bullet> x)"}
+  where @{text \<pi>} and @{text x} are free variables, then we do
+  want to apply rule  ({\it i}), rather than rule ({\it iii}) which
+  would eliminate @{text \<pi>} completely. This is a problem because we 
+  want to keep the shape of the HOL-term intact during rewriting.
+  As a remedy 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
+  The point is that we will always start with a term that does not
+  contain any @{text unpermutes}.  With this trick we can reformulate
+  our rewrite rules 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{}\\
+  i') & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & $\stackrel{\rightharpoonup}{=}$ & 
+    @{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\\
+  ii') & @{text "\<pi> \<bullet> (\<lambda>x. t)"} & $\stackrel{\rightharpoonup}{=}$ & @{text "\<lambda>x. \<pi> \<bullet> (t[x := unpermute \<pi> x])"}\\
+  iii') & @{text "\<pi> \<bullet> (unpermute \<pi> x)"} & $\stackrel{\rightharpoonup}{=}$ & @{term x}\\
+  iv') &  @{term "\<pi> \<bullet> c"} & $\stackrel{\rightharpoonup}{=}$ & @{term "c"}
+    \hspace{6mm}provided @{text c} is equivariant\\
   \end{tabular}
   \end{isabelle}
 
   \noindent
-  In this rewrite systems no rule overlaps. Taking the measure
+  None of these rules overlap. To see that the permutation on the
+  right-hand side is applied to a smaller term, we take 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.
-
+  is the size of a term (without counting @{text unpermutes}) and the
+  second is the number of occurences of @{text "unpermute \<pi> x"} and
+  @{text "\<pi> \<bullet> c"}. This means the process of applying these rules 
+  with our `outside-to-inside' strategy 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
-  equivariant constants disappear. This helps us to establish equivariance
-  for any notion in HOL that is defined in terms of more primitive notions. To
-  see this let us 
+  With the rewriting system in plcae, we are able to establish the
+  fact that for a HOL-term @{text t} whose constants are all equivariant,
+  the HOL-term @{text "\<pi> \<bullet> t"} is equal to @{text "t'"} wherby
+  @{text "t'"} is equal to @{text t} except that every free variable
+  @{text x} of @{text t} is replaced by @{text "\<pi> \<bullet> x"}.  Pitts calls
+  this fact \emph{equivariance principle}. In our setting the precise
+  statement of this fact is a bit more involved because of the fact
+  that @{text unpermute} needs to be treated specially.
+  
+  \begin{theorem}[Equivariance Principle]
+  Suppose a HOL-term @{text t} does not contain any @{text unpermutes} and all
+  its constants are equivariant. For any permutation @{text \<pi>}, let @{text t'} 
+  be the HOL-term @{text t} except every free variable @{text x} in @{term t} is 
+  replaced by @{text "\<pi> \<bullet> x"}, then @{text "\<pi> \<bullet> t = t'"}.
+  \end{theorem}
+  
+
 
   With these definitions in place we can define the notion of an \emph{equivariant}
   HOL-term
@@ -714,6 +744,10 @@
   Such a rewrite system is often very helpful
   in determining whether @{text "\<pi> \<bullet> t = t"} holds for a compound term @{text t}. ???
  
+  For this we have implemented in Isabelle/HOL a
+  database of equivariant constants that can be used to rewrite
+  HOL-terms.
+
 *}
 
 




