
diff -r d19bfc6e7631 -r 5f3387b7474f Pearl-jv/Paper.thy
--- a/Pearl-jv/Paper.thy	Mon May 02 13:01:02 2011 +0800
+++ b/Pearl-jv/Paper.thy	Wed May 04 15:27:04 2011 +0800
@@ -290,7 +290,7 @@
   a function in @{typ perm}. 
 
   One advantage of using functions as a representation for
-  permutations is that it is unique. For example the swappings
+  permutations is that it is a unique representation. For example the swappings
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -352,7 +352,7 @@
   \end{isabelle} 
 
   \noindent
-  whereby @{text "\<beta>"} is a generic type for @{text x}. The definition of this operation will be 
+  whereby @{text "\<beta>"} is a generic type for the object @{text x}. The definition of this operation will be 
   given by in terms of `induction' over this generic type. The type-class mechanism
   of Isabelle/HOL \cite{Wenzel04} allows us to give a definition for
   `base' types, such as atoms, permutations, booleans and natural numbers:
@@ -435,7 +435,7 @@
 
   \noindent
   Note that the permutation operation for functions is defined so that
-  we have for applications the property
+  we have for applications the equation
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   @{text "\<pi> \<bullet> (f x) ="}
@@ -444,7 +444,7 @@
   \end{isabelle}
 
   \noindent
-  whenever the permutation properties hold for @{text x}. This property can
+  whenever the permutation properties hold for @{text x}. This equation can
   be easily shown by unfolding the permutation operation for functions on
   the right-hand side, simplifying the beta-redex and eliminating the permutations
   in front of @{text x} using \eqref{cancel}.
@@ -454,7 +454,7 @@
   are satisfied to Isabelle/HOL's type system: we only have to
   establish that base types satisfy them and that type-constructors
   preserve them. Isabelle/HOL will use this information and determine
-  whether an object @{text x} with a compound type satisfies the
+  whether an object @{text x} with a compound type, like @{typ "atom \<Rightarrow> (atom set * nat)"}, satisfies the
   permutation properties.  For this we define the notion of a
   \emph{permutation type}:
 
@@ -506,13 +506,13 @@
   \end{isabelle} 
 
   \noindent
-  where @{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.
+  where @{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, HOL-terms are regarded as equal modulo alpha-, beta-
+  and eta-equivalence.  Statements in HOL are HOL-terms of type @{text
+  "bool"}.
 
   An \emph{equivariant} HOL-term is one that is invariant under the
   permutation operation. This can be defined in Isabelle/HOL 
@@ -546,11 +546,11 @@
   \eqref{cancel}. To see the other direction, we use
   \eqref{permutefunapp}. Similarly for HOL-terms that take more than
   one argument. The point to note is that equivariance and equivariance in fully
-  applied form are (for permutation types) always interderivable.
+  applied form are always interderivable (for permutation types).
 
   Both formulations of equivariance have their advantages and
   disadvantages: \eqref{altequivariance} is usually more convenient to
-  establish, since statements in Isabelle/HOL are commonly given in a
+  establish, since statements in HOL are commonly given in a
   form where functions are fully applied. For example we can easily
   show that equality is equivariant
 
@@ -579,41 +579,91 @@
   \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 easy to see
-  that the boolean operators, like @{text "\<and>"}, @{text "\<or>"}, @{text
-  "\<not>"} and @{text "\<longrightarrow>"}, are equivariant too; for example we have
+  of the permutation operation for booleans. Given this definition, it 
+  is also easy to see that the boolean operators, like @{text "\<and>"}, 
+  @{text "\<or>"}, @{text "\<longrightarrow>"} and  @{text "\<not>"} are equivariant too:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}lcl}
   @{text "\<pi> \<bullet> (A \<and> B) = (\<pi> \<bullet> A) \<and> (\<pi> \<bullet> B)"}\\
+  @{text "\<pi> \<bullet> (A \<or> B) = (\<pi> \<bullet> A) \<or> (\<pi> \<bullet> B)"}\\
   @{text "\<pi> \<bullet> (A \<longrightarrow> B) = (\<pi> \<bullet> A) \<longrightarrow> (\<pi> \<bullet> B)"}\\
+  @{text "\<pi> \<bullet> (\<not>A) = \<not>(\<pi> \<bullet> A)"}\\
   \end{tabular}
   \end{isabelle}
-
-  \noindent
-  by the definition of the permutation operation acting on booleans.
   
   In contrast, the advantage of Definition \ref{equivariance} is that
-  it leads to a relatively simple rewrite system that allows us to `push' a permutation
-  towards the leaves of a HOL-term (i.e.~constants and
-  variables).  Then the permutation disappears in cases where the
-  constants are equivariant. We have implemented this rewrite system
-  as a simplification tactic on the ML-level of Isabelle/HOL.  Having this tactic 
-  at our disposal, together with a collection of constants for which 
-  equivariance is already established, we can automatically establish 
-  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.  In what follows 
-  we shall specify this tactic and argue that it terminates and 
-  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). 
+  it leads to rewrite system that allows us to
+  `push' a permutation towards the leaves of a HOL-term
+  (i.e.~constants and variables).  Then the permutation disappears in
+  cases where the constants are equivariant. This can be stated more
+  formally as the following \emph{equivariance principle}:
+
+  \begin{theorem}[Equivariance Principle]\label{eqvtprin}
+  Suppose a HOL-term @{text t} whose constants are all 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}
+  
+  \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 "All"}, also written @{text "\<forall>"}, is 
+  of type @{text "(\<alpha> \<Rightarrow> bool) \<Rightarrow> bool"} and in HOL is definied as 
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{thm All_def[no_vars]}
+  \end{isabelle} 
+
+  \noindent
+  Now @{text All} must be equivariant, because by the equivariance
+  principle we only have to test whether the contants in the HOL-term
+  @{thm (rhs) All_def[no_vars]}, namely @{text "="} and @{text
+  "True"}, are equivariant. We shown this above. Taking all equations
+  together, we can establish
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{text "\<pi> \<bullet> (All P)   \<equiv>   \<pi> \<bullet> (P = (\<lambda>x. True))   =   ((\<pi> \<bullet> P) = (\<lambda>x. True))   \<equiv>   All (\<pi> \<bullet> P)"}
+  \end{isabelle} 
 
-  The simplifiaction tactic is a rewrite systems consisting of four `oriented' 
-  equations. We will first give a naive version of this tactic, which however 
-  is in some cornercases incorrect and does not terminate, and then modify 
-  it in order to obtain the desired properties. A permutation @{text \<pi>} can 
-  be pushed into applications and abstractions as follows
+  \noindent
+  where the equation in the `middle' is given by Theorem~\ref{eqvtprin}.
+  As a consequence, the constant @{text "All"} is equivariant. Given this
+  fact we can further show that the existential quantifier @{text Ex},
+  written also as @{text "\<exists>"}, is equivariant, since it is defined as
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{thm Ex_def[no_vars]}
+  \end{isabelle} 
+
+  \noindent
+  and the HOL-term on the right-hand side contains equivariant constants only
+  (namely @{text "\<forall>"} and @{text "\<longrightarrow>"}). In this way we can establish step by step 
+  equivariance for constants in HOL. 
+
+  In order to establish Theorem~\ref{eqvtprin}, we use a rewrite system
+  consisting of a series of equalities 
+  
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{text "\<pi> \<cdot> t = ... = t'"}
+  \end{isabelle}
+  
+  \noindent
+  that establish the equality between @{term "\<pi> \<bullet> t"} and @{text
+  "t'"}.  We have implemented this rewrite system as a conversion
+  tactic on the ML-level of Isabelle/HOL.
+  We shall next specify this tactic and show that it terminates and 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 resolts or does not
+  terminate.  We then give a modification it in order to obtain the
+  desired properties. A permutation @{text \<pi>} can be pushed into
+  applications and abstractions as follows
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}lr@ {\hspace{3mm}}c@ {\hspace{3mm}}l}
@@ -732,12 +782,6 @@
   involved because of the fact that @{text unpermutes} 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}
   
 
 




