
diff -r 77e1d9f2925e -r c7d4bd9e89e0 Pearl-jv/Paper.thy
--- a/Pearl-jv/Paper.thy	Mon Jun 06 13:11:04 2011 +0100
+++ b/Pearl-jv/Paper.thy	Tue Jun 07 08:52:59 2011 +0100
@@ -80,7 +80,7 @@
   type to represent atoms of different sorts. The other is how to
   present sort-respecting permutations. For them we use the standard
   technique of HOL-formalisations of introducing an appropriate
-  substype of functions from atoms to atoms.
+  subtype of functions from atoms to 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
@@ -323,7 +323,7 @@
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  i)~~@{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]}\\
+  i)~~@{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]}\smallskip\\
   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"]} 
@@ -357,7 +357,7 @@
 
   \noindent
   whereby @{text "\<beta>"} is a generic type for the object @{text
-  x}.\footnote{We will use the standard notation @{text "((op \<bullet>) \<pi>)
+  x}.\footnote{We will write @{text "((op \<bullet>) \<pi>)
   x"} for this operation in the few cases where we need to indicate
   that it is a function applied with two arguments.}  The definition
   of this operation will be given by in terms of `induction' over this
@@ -506,7 +506,8 @@
   \emph{equivariance} and the \emph{equivariance principle}.  These
   notions allows us to characterise how permutations act upon compound
   statements in HOL by analysing how these statements are constructed.
-  The notion of equivariance can defined as follows:
+  The notion of equivariance means that an object is invariant under
+  any permutations. This can be defined as follows:
 
   \begin{definition}[Equivariance]\label{equivariance}
   An object @{text "x"} of permutation type is \emph{equivariant} provided 
@@ -518,8 +519,8 @@
   @{text x} is a constant, but of course there is no way in
   Isabelle/HOL to restrict this definition to just these cases.
 
-  There are a number of equivalent formulations for the equivariance
-  property.  For example, assuming @{text f} is a function of permutation 
+  There are a number of equivalent formulations for equivariance.  
+  For example, assuming @{text f} is a function of permutation 
   type @{text "\<alpha> \<Rightarrow> \<beta>"}, then equivariance of @{text f} can also be stated as
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -529,7 +530,7 @@
   \end{isabelle} 
 
   \noindent
-  We will call this formulation of equivariance in \emph{fully applied form}.
+  We will say this formulation of equivariance is 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
@@ -602,8 +603,8 @@
   legibility we leave the typing information implicit.  We also assume
   the usual notions for free and bound variables of a HOL-term.
   Furthermore, HOL-terms are regarded as equal modulo alpha-, beta-
-  and eta-equivalence. The equivariance principle can now be stated
-  formally as follows:
+  and eta-equivalence. The equivariance principle can now 
+  be stated formally as follows:
 
   \begin{theorem}[Equivariance Principle]\label{eqvtprin}
   Suppose a HOL-term @{text t} whose constants are all equivariant. For any 
@@ -615,9 +616,20 @@
   \noindent
   The significance of this principle is that we can automatically establish
   the equivariance of a constant for which equivariance is not yet
-  known. For this we only have to make sure that the definiens of this
-  constant is a HOL-term whose constants are all equivariant. For example
-  the universal quantifier @{text "\<forall>"} is definied in HOL as 
+  known. For this we only have to establish that the definiens of this
+  constant is a HOL-term whose constants are all equivariant. 
+  This meshes well with how HOL is designed: except for a few axioms, every constant 
+  is defined in terms of existing constants. For example an alternative way
+  to deduce that @{term True} is equivariant is to look at its
+  definition
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{thm True_def}
+  \end{isabelle} 
+
+  \noindent
+  and observing that the only constant in the definiens, namely @{text "="}, is 
+  equivariant. Similarly, the universal quantifier @{text "\<forall>"} is definied in HOL as 
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   @{text "\<forall>x. P x \<equiv> "}~@{thm (rhs) All_def[no_vars]}
@@ -629,7 +641,11 @@
   the equivariance principle gives us
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  @{text "\<pi> \<bullet> (\<forall>x. P x)  \<equiv>  \<pi> \<bullet> (P = (\<lambda>x. True))  =  ((\<pi> \<bullet> P) = (\<lambda>x. True))  \<equiv>  \<forall>x. (\<pi> \<bullet> P) x"}
+  \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+  @{text "\<pi> \<bullet> (\<forall>x. P x)"} & @{text "\<equiv>"} & @{text "\<pi> \<bullet> (P = (\<lambda>x. True))"}\\  
+                           & @{text "="} & @{text "(\<pi> \<bullet> P) = (\<lambda>x. True)"}\\  
+                           & @{text "\<equiv>"} & @{text "\<forall>x. (\<pi> \<bullet> P) x"}
+  \end{tabular}
   \end{isabelle} 
 
   \noindent
@@ -653,7 +669,8 @@
 
   \noindent
   with all constants on the right-hand side being equivariant. With this kind
-  of reasoning we can build up a database of equivariant constants.
+  of reasoning we can build up a database of equivariant constants, which will
+  be handy for more complex calculations later on. 
 
   Before we proceed, let us give a justification for the equivariance principle. 
   This justification cannot be given directly inside Isabelle/HOL since we cannot
@@ -670,14 +687,15 @@
   permutation inside the term @{text t}. We have implemented this as a
   conversion tactic on the ML-level of Isabelle/HOL.  In what follows,
   we will show that this tactic produces only finitely many equations
-  and also show that is correct (in the sense of pushing a permutation
+  and also show that it is correct (in the sense of pushing a permutation
   @{text "\<pi>"} inside a term and the only remaining instances of @{text
-  "\<pi>"} are in front of the term's free variables).  The tactic applies
-  four `oriented' equations. We will first give a naive version of
-  this tactic, which however in some cornercases produces incorrect
+  "\<pi>"} are in front of the term's free variables).  
+
+  The tactic applies four `oriented' equations. 
+  We will first give a naive version of
+  our tactic, which however in some corner cases produces incorrect
   results or does not terminate.  We then give a modification in order
   to obtain the desired properties.
-
   Consider the following for oriented equations
   
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -697,10 +715,9 @@
   and the fact that HOL-terms are equal modulo beta-equivalence.
   The third is a consequence of \eqref{cancel} and the fourth from 
   Definition~\ref{equivariance}. Unfortunately, we have to be careful with
-  the rules {\it i)} and {\it iv}) since they can lead to a loop whenever
-  \mbox{@{text "t\<^isub>1 t\<^isub>2"}} is of the form @{text "((op \<bullet>) \<pi>') t"}.\footnote{Note we 
-  deviate here from our usual convention of writing the permutation operation infix, 
-  instead as an application.} Recall that we established in Lemma \ref{permutecompose} that the
+  the rules {\it i)} and {\it iv}) since they can lead to loops whenever
+  \mbox{@{text "t\<^isub>1 t\<^isub>2"}} is of the form @{text "((op \<bullet>) \<pi>') t"}.
+  Recall that we established in Lemma \ref{permutecompose} that the
   constant @{text "(op \<bullet>)"} is equivariant and consider the infinite
   reduction sequence
 
@@ -716,7 +733,7 @@
   \end{isabelle}
 
   \noindent
-  where the last term is again an instance of rewrite rule {\it i}), but bigger.  
+  where the last term is again an instance of rewrite rule {\it i}), but larger.  
   To avoid this loop we will apply the rewrite rule
   using an `outside to inside' strategy.  This strategy is sufficient
   since we are only interested of rewriting terms of the form @{term
@@ -726,8 +743,8 @@
   iii)} can `overlap'. For this note that the term @{term "\<pi>
   \<bullet>(\<lambda>x. x)"} reduces by {\it ii)} 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---since there is no free variable in the original
-  term. the permutation should completely vanish. However, the
+  "\<lambda>x. x"}, as is desired: since there is no free variable in the original
+  term, the permutation should completely vanish. However, the
   subterm @{text "(- \<pi>) \<bullet> x"} is also an application. Consequently,
   the term @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet>x"} can also reduce to @{text "\<lambda>x. (- (\<pi>
   \<bullet> \<pi>)) \<bullet> (\<pi> \<bullet> x)"} using {\it i)}.  Given our strategy, we cannot
@@ -1222,11 +1239,11 @@
   representation for permutations (for example @{term "(a \<rightleftharpoons> b)"} and
   @{term "(b \<rightleftharpoons> a)"} are equal permutations), this representation does
   not come automatically with an induction principle.  Such an
-  induction principle is however handy for generalising
-  Lemma~\ref{swapfreshfresh} from swappings to permutations
+  induction principle is however useful for generalising
+  Lemma~\ref{swapfreshfresh} from swappings to permutations, namely
   
   \begin{lemma}
-  @{thm [mode=IfThen] perm_supp_eq[no_vars]}
+  @{thm [mode=IfThen] perm_supp_eq[where p="\<pi>", no_vars]}
   \end{lemma}
 
   \noindent
@@ -1238,7 +1255,7 @@
   Using a the property from \cite{???}
 
   \begin{lemma}\label{smallersupp}
-  @{thm [mode=IfThen] smaller_supp[no_vars]}
+  @{thm [mode=IfThen] smaller_supp[where p="\<pi>", no_vars]}
   \end{lemma}
 *}
 




