--- a/Nominal/Nominal2_Base.thy	Wed Apr 13 13:44:25 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Fri Apr 22 00:18:25 2011 +0800
@@ -2398,11 +2398,6 @@
 lemma list_renaming_perm:
   shows "\<exists>q. (\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set bs \<union> (p \<bullet> set bs)"
 proof (induct bs)
-  case Nil
-  have "(\<forall>b \<in> set []. 0 \<bullet> b = p \<bullet> b) \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []" 
-    by (simp add: supp_zero_perm)
-  then show "\<exists>q. (\<forall>b \<in> set []. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set [] \<union> p \<bullet> (set [])" by blast
-next
   case (Cons a bs)
   then have " \<exists>q. (\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set bs \<union> p \<bullet> (set bs)"  by simp
   then obtain q where *: "\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> set bs \<union> p \<bullet> (set bs)"
@@ -2443,6 +2438,11 @@
   }
   ultimately show "\<exists>q. (\<forall>b \<in> set (a # bs). q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
     by blast
+next
+ case Nil
+  have "(\<forall>b \<in> set []. 0 \<bullet> b = p \<bullet> b) \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []" 
+    by (simp add: supp_zero_perm)
+  then show "\<exists>q. (\<forall>b \<in> set []. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set [] \<union> p \<bullet> (set [])" by blast
 qed
 
 

--- a/Pearl-jv/Paper.thy	Wed Apr 13 13:44:25 2011 +0100
+++ b/Pearl-jv/Paper.thy	Fri Apr 22 00:18:25 2011 +0800
@@ -57,7 +57,7 @@
 
 text {*
   Nominal Isabelle provides a proving infratructure for convenient reasoning
-  about syntax involving binders, such as lambda terms or type schemes:
+  about syntax involving binders, such as lambda terms or type schemes in Mini-ML:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   @{text "\<lambda>x. t       \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. \<tau>"} 
@@ -196,13 +196,14 @@
 
 text {*
   \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 of type \emph{string} for sorts is merely for
-  convenience; any countably infinite type would work as well. 
-  The set of all atoms we shall write as @{term "UNIV::atom set"}.
-  We have two auxiliary functions for atoms, namely @{text sort} 
-  and @{const nat_of} which are defined as 
+  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 of type
+  \emph{string} for sorts is merely for convenience; any countably
+  infinite type would work as well.  In what follows we shall write
+  @{term "UNIV::atom set"} for the set of all atoms.  We also have two
+  auxiliary functions for atoms, namely @{text sort} and @{const
+  nat_of} which are defined as
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
@@ -221,8 +222,8 @@
   \end{proposition}
 
   For implementing sort-respecting permutations, we use functions of type @{typ
-  "atom => atom"} that @{text "i)"} are bijective; @{text "ii)"} are the
-  identity on all atoms, except a finite number of them; and @{text "iii)"} map
+  "atom => atom"} that are bijective; are the
+  identity on all atoms, except a finite number of them; and map
   each atom to one of the same sort. These properties can be conveniently stated
   in Isabelle/HOL for a function @{text \<pi>} as follows:
   
@@ -241,7 +242,7 @@
   written @{term id}, is included in @{typ perm}. Also function composition, 
   written  \mbox{@{text "_ \<circ> _"}}, and function inversion, given by Isabelle/HOL's 
   inverse operator and written \mbox{@{text "inv _"}}, preserve the properties 
-  @{text "i"}-@{text "iii"}. 
+  (\ref{permtype}.@{text "i"}-@{text "iii"}). 
 
   However, a moment of thought is needed about how to construct non-trivial
   permutations. In the nominal logic work it turned out to be most convenient
@@ -299,8 +300,8 @@
   \end{isabelle}
 
   \noindent
-  are \emph{equal}. Another advantage of the function representation is that
-  they form a (non-com\-mu\-ta\-tive) group provided we define
+  are \emph{equal} and can be used interchangeably. Another advantage of the function 
+  representation is that they form a (non-com\-mu\-ta\-tive) group provided we define
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{10mm}}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
@@ -334,7 +335,7 @@
   composition of permutations is not commutative in general; for example
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  @{text "(a b) + (b c) \<noteq> (b c) + (a b)"}
+  @{text "(a b) + (b c) \<noteq> (b c) + (a b)"}\;.
   \end{isabelle} 
 
   \noindent
@@ -343,16 +344,17 @@
   the non-standard notation in order to reuse the existing libraries.
 
   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
+  applies a permutation @{text "\<pi>"} to an object @{text "x"}.  This 
+  operation has the type
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   @{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
   \end{isabelle} 
 
   \noindent
-  and will be defined over the hierarchie of types.
-  Isabelle/HOL allows us to give a definition of this operation for
+  whereby @{text "\<beta>"} is a generic type for @{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:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -377,8 +379,9 @@
   \end{tabular}\hfill\numbered{permdefsconstrs}
   \end{isabelle}
 
-  In order to reason abstractly about this operation, 
-  we use Isabelle/HOL's type classes~\cite{Wenzel04} and state the following two 
+  \noindent
+  The type classes also allow us to reason abstractly about the permutation operation. 
+  For this we state the following two 
   \emph{permutation properties}: 
   
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -446,8 +449,8 @@
   the right-hand side, simplifying the beta-redex and eliminating the permutations
   in front of @{text x} using \eqref{cancel}.
 
-  The use of type classes allows us to delegate much of the routine
-  resoning involved in determining whether the permutation properties
+  The main benefit of the use of type classes is that it allows us to delegate 
+  much of the routine resoning involved in determining whether the permutation properties
   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
@@ -503,8 +506,9 @@
   \end{isabelle} 
 
   \noindent
-  whereby @{text c} stands for constants and @{text x} for
-  variables. We assume HOL-terms are fully typed, but for the sake of
+  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
@@ -520,9 +524,9 @@
   \end{definition}
 
   \noindent
-  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.  
+  In what follows we will primarily be interested in the cases where @{text t} 
+  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 t} is of permutation type @{text "\<alpha> \<Rightarrow>
@@ -542,7 +546,7 @@
   \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 always interderivable.
+  applied form are (for permutation types) always interderivable.
 
   Both formulations of equivariance have their advantages and
   disadvantages: \eqref{altequivariance} is usually more convenient to
@@ -553,12 +557,13 @@
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
   @{thm eq_eqvt[where p="\<pi>", no_vars]}
-  \end{tabular}
+  \end{tabular}\hfill\numbered{eqeqvt}
   \end{isabelle} 
 
   \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{permdefsconstrs}, state that the
   constructors for products, @{text "Nil"} and @{text Cons} are
@@ -576,128 +581,156 @@
   @{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 all equivariant too. (see ??? intro)
-
-  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,
-  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
+  "\<not>"} and @{text "\<longrightarrow>"}, are equivariant too; for example we have
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \begin{tabular}{@ {}lrcl}
-  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])"}\\
+  \begin{tabular}{@ {}lcl}
+  @{text "\<pi> \<bullet> (A \<and> B) = (\<pi> \<bullet> A) \<and> (\<pi> \<bullet> B)"}\\
+  @{text "\<pi> \<bullet> (A \<longrightarrow> B) = (\<pi> \<bullet> A) \<longrightarrow> (\<pi> \<bullet> B)"}\\
+  \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). 
+
+  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
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}lr@ {\hspace{3mm}}c@ {\hspace{3mm}}l}
+  i) & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & \rrh & @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\\
+  ii) & @{text "\<pi> \<bullet> (\<lambda>x. t)"} & \rrh & @{text "\<lambda>x. \<pi> \<bullet> (t[x :=  (-\<pi>) \<bullet> x])"}\\
   \end{tabular}\hfill\numbered{rewriteapplam}
   \end{isabelle}
 
   \noindent
-  The first rule we established in \eqref{permutefunapp};
+  The first equation we established in \eqref{permutefunapp};
   the second follows from the definition of permutations acting on functions
   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
+  following two equations
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \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\\
+  \begin{tabular}{@ {}lr@ {\hspace{3mm}}c@ {\hspace{3mm}}l}
+  iii) & @{term "\<pi> \<bullet> (- \<pi>) \<bullet> x"} & \rrh & @{term "x"}\\
+  iv) &  @{term "\<pi> \<bullet> c"} & \rrh & 
+            {\rm @{term "c"}\hspace{6mm}provided @{text c} is equivariant}\\
   \end{tabular}\hfill\numbered{rewriteother}
   \end{isabelle}
 
   \noindent
-  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
+  in order to remove permuations in front of bound variables and
+  equivariant constants.  Unfortunately, we have to be careful with
+  the rules {\it i)} and {\it iv}): they can lead to a loop whenever
+  \mbox{@{text "t\<^isub>1 t\<^isub>2"}} is of the form @{text "((op \<bullet>) \<pi>') t"}. Note
+  that we usually write this application using infix notation as
+  @{text "\<pi> \<bullet> t"} and recall that by Lemma \ref{permutecompose} the
+  constant @{text "(op \<bullet>)"} is equivariant. Now consider the infinite
+  reduction sequence
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \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$\\
+  @{text "\<pi> \<bullet> (\<pi>' \<bullet> t)"}
+  $\;\;\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it iv)}}{\rrh}\;\;$
+  @{text "(\<pi> \<bullet> \<pi>') \<bullet> (\<pi> \<bullet> t)"}
+  $\;\;\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it iv)}}{\rrh}\;\;$
+  @{text "((\<pi> \<bullet> \<pi>') \<bullet> \<pi>) \<bullet> ((\<pi> \<bullet> \<pi>') \<bullet> t)"}~~\ldots%
+  
   \end{tabular}
   \end{isabelle}
 
   \noindent
-  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"}.
+  where the last step is again an instance of the first term, but it
+  is bigger.  To avoid this loop we need to apply our rewrite rule
+  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"}, where an outermost permutation needs to pushed inside a term.
 
-  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
+  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 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---there is no 
+  free variable in the original term and so 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 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
+  {\it i)}.  Given our strategy we cannot apply rule {\it iii)} anymore and 
+  even worse the measure we will introduce shortly increased. On the
+  other hand, if we had started with the term @{text "\<pi> \<bullet> ((- \<pi>) \<bullet> x)"}
+  where @{text \<pi>} and @{text x} are free variables, then we \emph{do}
+  want to apply rule  {\it i)} and not rule {\it iii)}. The latter 
+  would eliminate @{text \<pi>} completely. The problem is that rule {\it iii)}
+  should only apply to instances where the variable is to bound; for free variables 
+  we want to use {\it ii)}. 
+
+  The problem is that in order to distinguish both cases when
+  inductively taking a term `apart', we have to maintain the
+  information which variable is bound. This, unfortunately, does not
+  mesh well with the way how simplification tactics are implemented in
+  Isabelle/HOL. Our remedy is to 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
-  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
+  The point is that now we can formulate the rewrite rules as follows
   
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}lrcl}
-  i') & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & $\stackrel{\rightharpoonup}{=}$ & 
+  i') & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & \rrh & 
     @{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)"} & $\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\\
+  \multicolumn{4}{r}{\rm 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)"} & \rrh & @{text "\<lambda>x. \<pi> \<bullet> (t[x := unpermute \<pi> x])"}\\
+  iii') & @{text "\<pi> \<bullet> (unpermute \<pi> x)"} & \rrh & @{term x}\\
+  iv') &  @{term "\<pi> \<bullet> c"} & \rrh & @{term "c"}
+    \hspace{6mm}{\rm provided @{text c} is equivariant}\\
   \end{tabular}
   \end{isabelle}
 
   \noindent
-  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 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.
+  and @{text unpermutes} are only generated in case of bound variables.
+  Clearly none of these rules overlap. Moreover, given our
+  outside-to-inside strategy, they terminate. To see this, notice that
+  the permutation on the right-hand side of the rewrite rules is
+  always applied to a smaller term, provided we take the measure consisting
+  of lexicographically ordered pairs whose first component is the size
+  of a term (counting terms of the form @{text "unpermute \<pi> x"} as
+  leaves) and the second is the number of occurences of @{text
+  "unpermute \<pi> x"} and @{text "\<pi> \<bullet> c"}.
 
-  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.
+  With the definition of the simplification tactic in place, we can
+  establish its correctness. The property we are after is that for for
+  a HOL-term @{text t} whose constants are all equivariant, the
+  HOL-term @{text "\<pi> \<bullet> t"} is equal to @{text "t'"} with @{text "t'"}
+  being equal to @{text t} except that every free variable @{text x}
+  in @{text t} is replaced by @{text "\<pi> \<bullet> x"}.  Pitts calls this
+  property \emph{equivariance principle} (book ref ???). In our
+  setting the precise statement of this property is a slightly more
+  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
@@ -723,30 +756,7 @@
   For an equivariant HOL-term @{text "t"},  @{term "\<pi> \<bullet> t = t"} for all permutations @{term "\<pi>"}.
   \end{lemma}
 
-  \begin{proof}
-  By induction on the grammar of HOL-terms. The case for variables cannot arise since
-  equivariant HOL-terms are closed. The case for constants is clear by Definition 
-  \ref{equivariance}. The case for applications is also straightforward since by
-  \eqref{permutefunapp} we have @{term "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2) = (\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}.
-  For the case of abstractions we can reason as follows
-  
-  \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{permdefsconstrs}\\
-
-  \end{tabular}\hfill\qed
-  \end{isabelle}
-  \end{proof}
-
-  database of equivariant functions
-
-  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.
+  Let us now see how to use the equivariance principle. We have 
 
 *}
 

--- a/Pearl-jv/document/root.tex	Wed Apr 13 13:44:25 2011 +0100
+++ b/Pearl-jv/document/root.tex	Fri Apr 22 00:18:25 2011 +0800
@@ -4,6 +4,7 @@
 \usepackage{isabellesym}
 \usepackage{amsmath}
 \usepackage{amssymb}
+\usepackage{mathabx}
 \usepackage{longtable}
 \usepackage{graphics}
 \usepackage{pdfsetup}
@@ -19,10 +20,13 @@
 \renewcommand{\isasymrightleftharpoons}{}
 \renewcommand{\isasymemptyset}{$\varnothing$}
 \newcommand{\isasymallatoms}{\ensuremath{\mathbb{A}}}
+\newcommand{\rrh}{\mbox{\footnotesize$\rightrightharpoons$}}
 
 \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
 \newcommand\new[0]{\reflectbox{\ensuremath{\mathsf{N}}}}
 
+\changenotsign
+
 \begin{document}
 
 \title{Implementing the Nominal Logic Work in Isabelle/HOL}

--- a/Slides/Slides6.thy	Wed Apr 13 13:44:25 2011 +0100
+++ b/Slides/Slides6.thy	Fri Apr 22 00:18:25 2011 +0800
@@ -12,7 +12,7 @@
 (*>*)
 
 text_raw {*
-  \renewcommand{\slidecaption}{Shanghai, 12.~April 2011}
+  \renewcommand{\slidecaption}{Hefei, 15.~April 2011}
 
   \newcommand{\abst}[2]{#1.#2}% atom-abstraction
   \newcommand{\pair}[2]{\langle #1,#2\rangle} % pairing
@@ -128,6 +128,23 @@
 *}
 
 
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{3 Points}
+  \large
+  \begin{itemize}
+  \item It is easy to make mistakes.\bigskip
+  \item Theorem provers can prevent mistakes, {\bf if} the problem
+  is formulated so that it is suitable for theorem provers.\bigskip
+  \item This re-formulation can be done, even in domains where
+  we do not expect it.
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
 
 text_raw {*
 
@@ -186,15 +203,12 @@
 
   \end{tabular}\medskip
 
-
-  
-
-
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 
 *}
 
+
 text_raw {*
 
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -333,7 +347,7 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}<1->[c]
-  \frametitle{Theorem Provers}
+  \frametitle{Lessons Learned}
 
   \begin{itemize}
   \item Theorem provers help with keeping large proofs consistent;
@@ -738,13 +752,13 @@
 
   \begin{textblock}{6}(9.5,6.18)
   \begin{flushright}
-  \color{gray}``derivative for a char'' 
+  \color{gray}``derivative w.r.t.~a char'' 
   \end{flushright}
   \end{textblock}
 
   \begin{textblock}{6}(9.5,12.1)
   \begin{flushright}
-  \color{gray}``deriv.~for a string'' 
+  \color{gray}``deriv.~w.r.t.~a string'' 
   \end{flushright}
   \end{textblock}
 
@@ -861,10 +875,10 @@
   \end{itemize}
 
 
-  I can think of two reasons why this is a good definition:\medskip
+  There are many reasons why this is a good definition:\medskip
   \begin{itemize}
   \item pumping lemma
-  \item closure properties of regular languages (closed under complement)
+  \item closure properties of regular languages\\ (e.g.~closure under complement)
   \end{itemize}
 
   \end{frame}}
@@ -909,6 +923,24 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
+  \frametitle{}
+  \large
+  \begin{center}
+  \begin{tabular}{p{9cm}}
+  My point:\bigskip\\
+
+  The theory about regular languages can be reformulated 
+  to be more suitable for theorem proving.
+  \end{tabular}
+  \end{center}
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
   \frametitle{\LARGE The Myhill-Nerode Theorem}
 
   \begin{itemize}
@@ -925,7 +957,6 @@
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-
 *}
 
 text_raw {*
@@ -1055,7 +1086,7 @@
   \smath{R_1}: & \smath{\{[]\}}\\
   \smath{R_2}: & \smath{\{[c]\}}\\
   \smath{R_3}: & \smath{U\!N\!IV - \{[], [c]\}}\\[6mm]
-  \multicolumn{2}{l}{\onslide<2->{\smath{X \stackrel{c}{\longrightarrow} Y \dn X ; [c] \subseteq Y}}}
+  \multicolumn{2}{l}{\onslide<2->{\smath{X \stackrel{c}{\longrightarrow} Y \dn X ;; [c] \subseteq Y}}}
   \end{tabular}
 
   \end{tabular}
@@ -1345,7 +1376,7 @@
   \begin{itemize}
   \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_L) \;\Leftrightarrow\; L\; \text{is regular}}
   \bigskip\pause
-  \item regular languages are closed under complementation; this is easy
+  \item regular languages are closed under complementation; this is now easy\medskip
   \begin{center}
   \smath{U\!N\!IV /\!/ \approx_L \;\;=\;\; U\!N\!IV /\!/ \approx_{-L}}
   \end{center}
@@ -1423,7 +1454,7 @@
 
   \begin{itemize}
   \item We formalised the Myhill-Nerode theorem based on 
-  regular expressions (DFA are difficult to deal with in a theorem prover).\smallskip
+  regular expressions only (DFAs are difficult to deal with in a theorem prover).\smallskip
 
   \item Seems to be a common theme: algorithms need to be reformulated
   to better suit formal treatment.\smallskip
@@ -1432,7 +1463,7 @@
   implement the matcher directly inside the theorem prover
   (ongoing work).\smallskip
 
-  \item Parsing is a vast field and seems to offer new results. 
+  \item Parsing is a vast field which seem to offer new results. 
   \end{itemize}
 
   \end{frame}}
@@ -1450,23 +1481,126 @@
   \alert{\Large Questions?}
   \end{tabular}}
 
-  %\begin{center}
-  %\bf \underline{Short Bio:}
-  %\end{center}
-  %\mbox{}\\[-17mm]\mbox{}\small
-  %\begin{itemize}
-  %\item PhD in Cambridge
-  %\item Emmy-Noether Fellowship in Munich
-  %\item main results in nominal reasoning and nominal unification
-  %\end{itemize}
+  \begin{center}
+  \bf \underline{Short Bio:}
+  \end{center}
+  \mbox{}\\[-17mm]\mbox{}\small
+  \begin{itemize}
+  \item PhD in Cambridge
+  \item Emmy-Noether Research Fellowship at the TU Munich
+  \item talks at: CMU, Yale, Princeton, MIT,$\ldots$
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Future Research}
+
+  My existing strengths:\bigskip
+
+  \begin{itemize}
+  \item Isabelle (implementation)\bigskip
+  \item background in logic, programming languages, formal methods
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Future Research}
+
+  I want to have a single logic framework in which I can
+  write programs and prove their correctness.\bigskip
+
+  \begin{itemize}
+  \item extensions of HOL (IO, modules, advanced types)
+  \item high-level programming languages
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Future Research}
+
+  Compilers\bigskip
+
+  \begin{itemize}
+  \item the high-level language needs to be compiled to correct machine
+  code
+  \item compiler verification, machine code verification
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Future Research}
+
+  Stronger type-systems\bigskip
+
+  \begin{itemize}
+  \item ``correct by construction''
+  \item GADTs, dependent types
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Future Research}
+
+  Proof automation\bigskip
+
+  \begin{itemize}
+  \item external tools generate ``proof-certificates''
+  \item certificates are imported into Isabelle
+  \item GPU based external provers
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Future Research}
+
+  Large-scale applications\bigskip
+
+  \begin{itemize}
+  \item verification of Java-Script, Scala,$\ldots$
+  \item interesting code (INTEL in Shanghai)
+  \end{itemize}
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 *}
 
 
-
-
 (*<*)
 end
 (*>*)
\ No newline at end of file