
diff -r d97e04126a3d -r 61d30863e5d1 Pearl-jv/Paper.thy
--- a/Pearl-jv/Paper.thy	Tue Mar 01 00:14:02 2011 +0000
+++ b/Pearl-jv/Paper.thy	Wed Mar 02 00:06:28 2011 +0000
@@ -1,7 +1,6 @@
 (*<*)
 theory Paper
 imports "../Nominal/Nominal2_Base" 
-        "../Nominal/Nominal2_Eqvt"
         "../Nominal/Atoms" 
         "../Nominal/Nominal2_Abs"
         "LaTeXsugar"
@@ -41,15 +40,11 @@
 
 (*>*)
 
-(*
-  TODO: write about supp of finite sets, abstraction over finite sets
-*)
-
 section {* Introduction *}
 
 text {*
   Nominal Isabelle provides a proving infratructure for convenient reasoning
-  about programming language calculi involving binders such as lambda abstractions or
+  about programming language calculi involving binders, such as lambda abstractions or
   quantifications in type schemes:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -59,129 +54,14 @@
   
   \noindent
   At its core Nominal Isabelle is based on the nominal logic work by Pitts at
-  al \cite{GabbayPitts02,Pitts03}. The most basic notion in this work is a
+  al \cite{GabbayPitts02,Pitts03}, whose most basic notion is a
   sort-respecting permutation operation defined over a countably infinite
-  collection of sorted atoms. The atoms are used for representing variable names
-  that might be bound or free. Multiple sorts are necessary for being able to
-  represent different kinds of variables. For example, in the language Mini-ML
-  there are bound term variables in lambda abstractions and bound type variables in
-  type schemes. In order to be able to separate them, each kind of variables needs to be
-  represented by a different sort of atoms. 
-
-  The existing nominal logic work usually leaves implicit the sorting
-  information for atoms and as far as we know leaves out a description of how
-  sorts are represented.  In our formalisation, we therefore have to make a
-  design decision about how to implement sorted atoms and sort-respecting
-  permutations. One possibility, which we described in \cite{Urban08}, is to 
-  have separate types for the different
-  kinds of atoms, say types @{text "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}. With this
-  design one can represent permutations as lists of pairs of atoms and the
-  operation of applying a permutation to an object as the function
-
-
-  @{text [display,indent=10] "_ \<bullet> _  ::  (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
-
-  \noindent 
-  where @{text "\<alpha>"} stands for a type of atoms and @{text "\<beta>"} for the type
-  of the objects on which the permutation acts. For atoms 
-  the permutation operation is defined over the length of lists as follows
-
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-  @{text "[] \<bullet> c"} & @{text "="} & @{text c}\\
-  @{text "(a b)::\<pi> \<bullet> c"} & @{text "="} & 
-     $\begin{cases} @{text a} & \textrm{if}~@{text "\<pi> \<bullet> c = b"}\\ 
-                    @{text b} & \textrm{if}~@{text "\<pi> \<bullet> c = a"}\\
-                    @{text "\<pi> \<bullet> c"} & \textrm{otherwise}\end{cases}$
-  \end{tabular}\hfill\numbered{atomperm}
-  \end{isabelle}
-
-  \noindent
-  where we write @{text "(a b)"} for a swapping of atoms @{text "a"} and
-  @{text "b"}. For atoms with different type than the permutation, we 
-  define @{text "\<pi> \<bullet> c \<equiv> c"}.
-
-  With the separate atom types and the list representation of permutations it
-  is impossible in systems like Isabelle/HOL to state an ``ill-sorted''
-  permutation, since the type system excludes lists containing atoms of
-  different type. However, a disadvantage is that whenever we need to
-  generalise induction hypotheses by quantifying over permutations, we have to
-  build quantifications like
-
-  @{text [display,indent=10] "\<forall>\<pi>\<^isub>1 \<dots> \<forall>\<pi>\<^isub>n. \<dots>"}
-
-  \noindent
-  where the @{text "\<pi>\<^isub>i"} are of type @{text "(\<alpha>\<^isub>i \<times> \<alpha>\<^isub>i) list"}. 
-  The reason is that the permutation operation behaves differently for 
-  every @{text "\<alpha>\<^isub>i"} and the type system does not allow use to have a
-  single quantification to stand for all permutations. Similarly, the 
-  notion of support
-
-  @{text [display,indent=10] "supp _ :: \<beta> \<Rightarrow> \<alpha> set"}
-
-  \noindent
-  which we will define later, cannot be
-  used to express the support of an object over \emph{all} atoms. The reason
-  is that support can behave differently for each @{text
-  "\<alpha>\<^isub>i"}. This problem is annoying, because if we need to know in
-  a statement that an object, say @{text "x"}, is finitely supported we end up
-  with having to state premises of the form
-
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \begin{tabular}{@ {}l}
-  @{text "finite ((supp x) :: \<alpha>\<^isub>1 set) , \<dots>, finite ((supp x) :: \<alpha>\<^isub>n set)"}
-  \end{tabular}\hfill\numbered{fssequence}
-  \end{isabelle}
-
-  \noindent
-  Because of these disadvantages, we will use in this paper a single unified atom type to 
-  represent atoms of different sorts. Consequently, we have to deal with the
-  case that a swapping of two atoms is ill-sorted: we cannot rely anymore on
-  the type systems to exclude them. 
-
-  We also will not represent permutations as lists of pairs of atoms (as done in
-  \cite{Urban08}).  Although an
-  advantage of this representation is that the basic operations on
-  permutations are already defined in Isabelle's list library: composition of
-  two permutations (written @{text "_ @ _"}) is just list append, and
-  inversion of a permutation (written @{text "_\<^sup>-\<^sup>1"}) is just
-  list reversal, and another advantage is that there is a well-understood
-  induction principle for lists, a disadvantage is that permutations 
-  do not have unique representations as lists. We have to explicitly identify
-  them according to the relation
+  collection of sorted atoms. The nominal logic work has been starting
+  point for a number of formalisations, most notable Norrish \cite{norrish04} 
+  in HOL4, Aydemir et al \cite{AydemirBohannonWeirich07} in Coq and our own 
+  work in Isabelle/HOL.
 
   
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \begin{tabular}{@ {}l}
-  @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2  \<equiv>  \<forall>a. \<pi>\<^isub>1 \<bullet> a = \<pi>\<^isub>2 \<bullet> a"}
-  \end{tabular}\hfill\numbered{permequ}
-  \end{isabelle}
-
-  \noindent
-  This is a problem when lifting the permutation operation to other types, for
-  example sets, functions and so on. For this we need to ensure that every definition
-  is well-behaved in the sense that it satisfies some
-  \emph{permutation properties}. In the list representation we need
-  to state these properties as follows:
-
-
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
-  i) & @{text "[] \<bullet> x = x"}\\
-  ii) & @{text "(\<pi>\<^isub>1 @ \<pi>\<^isub>2) \<bullet> x = \<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x)"}\\
-  iii) & if @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2"} then @{text "\<pi>\<^isub>1 \<bullet> x = \<pi>\<^isub>2 \<bullet> x"}
-  \end{tabular}\hfill\numbered{permprops}
-  \end{isabelle}
-
-  \noindent
-  where the last clause explicitly states that the permutation operation has
-  to produce the same result for related permutations.  Moreover, 
-  ``permutations-as-lists'' do not satisfy the group properties. This means by
-  using this representation we will not be able to reuse the extensive
-  reasoning infrastructure in Isabelle about groups.  Because of this, we will represent
-  in this paper permutations as functions from atoms to atoms. This representation
-  is unique and satisfies the laws of non-commutative groups.
-
   Using a single atom type to represent atoms of different sorts and
   representing permutations as functions are not new ideas; see
   \cite{GunterOsbornPopescu09} \footnote{function rep.}  The main contribution
@@ -199,6 +79,24 @@
 section {* Sorted Atoms and Sort-Respecting Permutations *}
 
 text {*
+  The most basic notion in this work is a
+  sort-respecting permutation operation defined over a countably infinite
+  collection of sorted atoms. The atoms are used for representing variable names
+  that might be bound or free. Multiple sorts are necessary for being able to
+  represent different kinds of variables. For example, in the language Mini-ML
+  there are bound term variables in lambda abstractions and bound type variables in
+  type schemes. In order to be able to separate them, each kind of variables needs to be
+  represented by a different sort of atoms. 
+
+
+  The existing nominal logic work usually leaves implicit the sorting
+  information for atoms and as far as we know leaves out a description of how
+  sorts are represented.  In our formalisation, we therefore have to make a
+  design decision about how to implement sorted atoms and sort-respecting
+  permutations. One possibility, which we described in \cite{Urban08}, is to 
+  have separate types for the different
+  kinds of atoms, say types @{text "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}. 
+
   In the nominal logic work of Pitts, binders and bound variables are
   represented by \emph{atoms}.  As stated above, we need to have different
   \emph{sorts} of atoms to be able to bind different kinds of variables.  A
@@ -314,7 +212,7 @@
   @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm}
   @{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{4mm}
   @{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{4mm}
-  @{thm diff_def[where M="\<pi>\<^isub>1" and N="\<pi>\<^isub>2"]} 
+  @{thm minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^isub>2"]} 
   \end{tabular}
   \end{isabelle}
 
@@ -1202,184 +1100,123 @@
 *}
 
 
-section {* Multi-Sorted Concrete Atoms *}
-
-(*<*)
-datatype ty = TVar string | Fun ty ty ("_ \<rightarrow> _") 
-(*>*)
-
-text {*
-  The formalisation presented so far allows us to streamline proofs and reduce
-  the amount of custom ML-code in the existing implementation of Nominal
-  Isabelle. In this section we describe a mechanism that extends the
-  capabilities of Nominal Isabelle. This mechanism is about variables with 
-  additional information, for example typing constraints.
-  While we leave a detailed treatment of binders and binding of variables for a 
-  later paper, we will have a look here at how such variables can be 
-  represented by concrete atoms.
-  
-  In the previous section we considered concrete atoms that can be used in
-  simple binders like \emph{@{text "\<lambda>x. x"}}.  Such concrete atoms do
-  not carry any information beyond their identities---comparing for equality
-  is really the only way to analyse ordinary concrete atoms.
-  However, in ``Church-style'' lambda-terms \cite{Church40} and in the terms
-  underlying HOL-systems \cite{PittsHOL4} binders and bound variables have a
-  more complicated structure. For example in the ``Church-style'' lambda-term
-
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \begin{tabular}{@ {}l}
-  @{text "\<lambda>x\<^isub>\<alpha>. x\<^isub>\<alpha> x\<^isub>\<beta>"}
-  \end{tabular}\hfill\numbered{church}
-  \end{isabelle}
-
-  \noindent
-  both variables and binders include typing information indicated by @{text \<alpha>}
-  and @{text \<beta>}. In this setting, we treat @{text "x\<^isub>\<alpha>"} and @{text
-  "x\<^isub>\<beta>"} as distinct variables (assuming @{term "\<alpha>\<noteq>\<beta>"}) so that the
-  variable @{text "x\<^isub>\<alpha>"} is bound by the lambda-abstraction, but not
-  @{text "x\<^isub>\<beta>"}.
-
-  To illustrate how we can deal with this phenomenon, let us represent object
-  types like @{text \<alpha>} and @{text \<beta>} by the datatype
-
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \begin{tabular}{@ {}l}
-  \isacommand{datatype}~~@{text "ty = TVar string | ty \<rightarrow> ty"}
-  \end{tabular}
-  \end{isabelle}
-
-  \noindent
-  If we attempt to encode a variable naively as a pair of a @{text name} and a @{text ty}, we have the 
-  problem that a swapping, say @{term "(x \<leftrightarrow> y)"}, applied to the pair @{text "((x, \<alpha>), (x, \<beta>))"}
-  will always permute \emph{both} occurrences of @{text x}, even if the types
-  @{text "\<alpha>"} and @{text "\<beta>"} are different. This is unwanted, because it will
-  eventually mean that both occurrences of @{text x} will become bound by a
-  corresponding binder. 
-
-  Another attempt might be to define variables as an instance of the concrete
-  atom type class, where a @{text ty} is somehow encoded within each variable.
-  Remember we defined atoms as the datatype:
-*}
-
-          datatype  atom\<iota>\<iota> = Atom\<iota>\<iota> string nat
-  
-text {*
-  \noindent
-  Considering our method of defining concrete atom types, the usage of a string
-  for the sort of atoms seems a natural choice.  However, none of the results so
-  far depend on this choice and we are free to change it.
-  One possibility is to encode types or any other information by making the sort
-  argument parametric as follows:
-*}
-
-          datatype  'a \<iota>atom\<iota>\<iota>\<iota> = \<iota>Atom\<iota>\<iota> 'a nat
-
-text {*
-  \noindent
-  The problem with this possibility is that we are then back in the old
-  situation where our permutation operation is parametric in two types and
-  this would require to work around Isabelle/HOL's restriction on type
-  classes. Fortunately, encoding the types in a separate parameter is not
-  necessary for what we want to achieve, as we only have to know when two
-  types are equal or not. The solution is to use a different sort for each
-  object type.  Then we can use the fact that permutations respect \emph{sorts} to
-  ensure that permutations also respect \emph{object types}.  In order to do
-  this, we must define an injective function @{text "sort_ty"} mapping from
-  object types to sorts.  For defining functions like @{text "sort_ty"}, it is
-  more convenient to use a tree datatype for sorts. Therefore we define
-*}
-
-          datatype  sort = Sort string "(sort list)"
-          datatype  atom\<iota>\<iota>\<iota>\<iota> = Atom\<iota>\<iota>\<iota>\<iota> sort nat
-
-text {*
-  \noindent
-  With this definition,
-  the sorts we considered so far can be encoded just as \mbox{@{text "Sort s []"}}.
-  The point, however, is that we can now define the function @{text sort_ty} simply as
-
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \begin{tabular}{@ {}l}
-  @{text "sort_ty (TVar s) = Sort ''TVar'' [Sort s []]"}\\
-  @{text "sort_ty (\<tau>\<^isub>1 \<rightarrow> \<tau>\<^isub>2) = Sort ''Fun''  [sort_ty \<tau>\<^isub>1, sort_ty \<tau>\<^isub>2]"}
-  \end{tabular}\hfill\numbered{sortty}
-  \end{isabelle}
-
-  \noindent
-  which can easily be shown to be injective.  
-  
-  Having settled on what the sorts should be for ``Church-like'' atoms, we have to
-  give a subtype definition for concrete atoms. Previously we identified a subtype consisting 
-  of atoms of only one specified sort. This must be generalised to all sorts the
-  function @{text "sort_ty"} might produce, i.e.~the
-  range of @{text "sort_ty"}. Therefore we define
-
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \isacommand{typedef}\ \ @{text var} = @{term "{a. sort a : range sort_ty}"}
-  \end{isabelle}
-
-  \noindent
-  This command gives us again injective representation and abstraction
-  functions. We will write them also as \mbox{@{text "\<lfloor>_\<rfloor> :: var \<Rightarrow> atom"}} and
-  @{text "\<lceil>_\<rceil> :: atom \<Rightarrow> var"}, respectively. 
-
-  We can define the permutation operation for @{text var} as @{thm
-  permute_var_def[where p="\<pi>", THEN eq_reflection, no_vars]} and the
-  injective function to type @{typ atom} as @{thm atom_var_def[THEN
-  eq_reflection, no_vars]}. Finally, we can define a constructor function that
-  makes a @{text var} from a variable name and an object type:
-
-  @{thm [display,indent=10] Var_def[where t="\<alpha>", THEN eq_reflection, no_vars]}
-
-  \noindent
-  With these definitions we can verify all the properties for concrete atom
-  types except Property \ref{atomprops}@{text ".iii)"}, which requires every
-  atom to have the same sort.  This last property is clearly not true for type
-  @{text "var"}.
-  This fact is slightly unfortunate since this
-  property allowed us to use the type-checker in order to shield the user from
-  all sort-constraints.  But this failure is expected here, because we cannot
-  burden the type-system of Isabelle/HOL with the task of deciding when two
-  object types are equal.  This means we sometimes need to explicitly state sort
-  constraints or explicitly discharge them, but as we will see in the lemma
-  below this seems a natural price to pay in these circumstances.
-
-  To sum up this section, the encoding of type-information into atoms allows us 
-  to form the swapping @{term "(Var x \<alpha> \<leftrightarrow> Var y \<alpha>)"} and to prove the following 
-  lemma
-*}
-
-          lemma
-	    assumes asm: "\<alpha> \<noteq> \<beta>" 
-	    shows "(Var x \<alpha> \<leftrightarrow> Var y \<alpha>) \<bullet> (Var x \<alpha>, Var x \<beta>) = (Var y \<alpha>, Var x \<beta>)"
-	    using asm by simp
-
-text {*
-  \noindent 
-  As we expect, the atom @{term "Var x \<beta>"} is left unchanged by the
-  swapping. With this we can faithfully represent bindings in languages
-  involving ``Church-style'' terms and bindings as shown in \eqref{church}. We
-  expect that the creation of such atoms can be easily automated so that the
-  user just needs to specify \isacommand{atom\_decl}~~@{text "var (ty)"}
-  where the argument, or arguments, are datatypes for which we can automatically
-  define an injective function like @{text "sort_ty"} (see \eqref{sortty}).
-  Our hope is that with this approach Benzmueller and Paulson can make
-  headway with formalising their results
-  about simple type theory \cite{PaulsonBenzmueller}.
-  Because of its limitations, they did not attempt this with the old version 
-  of Nominal Isabelle. We also hope we can make progress with formalisations of
-  HOL-based languages.
-*}
 
 section {* Related Work *}
 
 text {*
   Add here comparison with old work.
 
-
   The main point is that the above reasoning blends smoothly with the reasoning
   infrastructure of Isabelle/HOL; no custom ML-code is necessary and a single
   type class suffices. 
+
+  With this
+  design one can represent permutations as lists of pairs of atoms and the
+  operation of applying a permutation to an object as the function
+
+
+  @{text [display,indent=10] "_ \<bullet> _  ::  (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
+
+  \noindent 
+  where @{text "\<alpha>"} stands for a type of atoms and @{text "\<beta>"} for the type
+  of the objects on which the permutation acts. For atoms 
+  the permutation operation is defined over the length of lists as follows
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
+  @{text "[] \<bullet> c"} & @{text "="} & @{text c}\\
+  @{text "(a b)::\<pi> \<bullet> c"} & @{text "="} & 
+     $\begin{cases} @{text a} & \textrm{if}~@{text "\<pi> \<bullet> c = b"}\\ 
+                    @{text b} & \textrm{if}~@{text "\<pi> \<bullet> c = a"}\\
+                    @{text "\<pi> \<bullet> c"} & \textrm{otherwise}\end{cases}$
+  \end{tabular}\hfill\numbered{atomperm}
+  \end{isabelle}
+
+  \noindent
+  where we write @{text "(a b)"} for a swapping of atoms @{text "a"} and
+  @{text "b"}. For atoms with different type than the permutation, we 
+  define @{text "\<pi> \<bullet> c \<equiv> c"}.
+
+  With the separate atom types and the list representation of permutations it
+  is impossible in systems like Isabelle/HOL to state an ``ill-sorted''
+  permutation, since the type system excludes lists containing atoms of
+  different type. However, a disadvantage is that whenever we need to
+  generalise induction hypotheses by quantifying over permutations, we have to
+  build quantifications like
+
+  @{text [display,indent=10] "\<forall>\<pi>\<^isub>1 \<dots> \<forall>\<pi>\<^isub>n. \<dots>"}
+
+  \noindent
+  where the @{text "\<pi>\<^isub>i"} are of type @{text "(\<alpha>\<^isub>i \<times> \<alpha>\<^isub>i) list"}. 
+  The reason is that the permutation operation behaves differently for 
+  every @{text "\<alpha>\<^isub>i"} and the type system does not allow use to have a
+  single quantification to stand for all permutations. Similarly, the 
+  notion of support
+
+  @{text [display,indent=10] "supp _ :: \<beta> \<Rightarrow> \<alpha> set"}
+
+  \noindent
+  which we will define later, cannot be
+  used to express the support of an object over \emph{all} atoms. The reason
+  is that support can behave differently for each @{text
+  "\<alpha>\<^isub>i"}. This problem is annoying, because if we need to know in
+  a statement that an object, say @{text "x"}, is finitely supported we end up
+  with having to state premises of the form
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{text "finite ((supp x) :: \<alpha>\<^isub>1 set) , \<dots>, finite ((supp x) :: \<alpha>\<^isub>n set)"}
+  \end{tabular}\hfill\numbered{fssequence}
+  \end{isabelle}
+
+  \noindent
+  Because of these disadvantages, we will use in this paper a single unified atom type to 
+  represent atoms of different sorts. Consequently, we have to deal with the
+  case that a swapping of two atoms is ill-sorted: we cannot rely anymore on
+  the type systems to exclude them. 
+
+  We also will not represent permutations as lists of pairs of atoms (as done in
+  \cite{Urban08}).  Although an
+  advantage of this representation is that the basic operations on
+  permutations are already defined in Isabelle's list library: composition of
+  two permutations (written @{text "_ @ _"}) is just list append, and
+  inversion of a permutation (written @{text "_\<^sup>-\<^sup>1"}) is just
+  list reversal, and another advantage is that there is a well-understood
+  induction principle for lists, a disadvantage is that permutations 
+  do not have unique representations as lists. We have to explicitly identify
+  them according to the relation
+
+  
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2  \<equiv>  \<forall>a. \<pi>\<^isub>1 \<bullet> a = \<pi>\<^isub>2 \<bullet> a"}
+  \end{tabular}\hfill\numbered{permequ}
+  \end{isabelle}
+
+  \noindent
+  This is a problem when lifting the permutation operation to other types, for
+  example sets, functions and so on. For this we need to ensure that every definition
+  is well-behaved in the sense that it satisfies some
+  \emph{permutation properties}. In the list representation we need
+  to state these properties as follows:
+
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
+  i) & @{text "[] \<bullet> x = x"}\\
+  ii) & @{text "(\<pi>\<^isub>1 @ \<pi>\<^isub>2) \<bullet> x = \<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x)"}\\
+  iii) & if @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2"} then @{text "\<pi>\<^isub>1 \<bullet> x = \<pi>\<^isub>2 \<bullet> x"}
+  \end{tabular}\hfill\numbered{permprops}
+  \end{isabelle}
+
+  \noindent
+  where the last clause explicitly states that the permutation operation has
+  to produce the same result for related permutations.  Moreover, 
+  ``permutations-as-lists'' do not satisfy the group properties. This means by
+  using this representation we will not be able to reuse the extensive
+  reasoning infrastructure in Isabelle about groups.  Because of this, we will represent
+  in this paper permutations as functions from atoms to atoms. This representation
+  is unique and satisfies the laws of non-commutative groups.
 *}
 
 




