(*<*)

theory Paper

imports "../Nominal-General/Nominal2_Base" 

        "../Nominal-General/Nominal2_Eqvt"

        "../Nominal-General/Atoms" 

        "../Nominal/Abs"

        "LaTeXsugar"

begin

notation (latex output)

  sort_of ("sort _" [1000] 100) and

  Abs_perm ("_") and

  Rep_perm ("_") and

  swap ("'(_ _')" [1000, 1000] 1000) and

  fresh ("_ # _" [51, 51] 50) and

  Cons ("_::_" [78,77] 73) and

  supp ("supp _" [78] 73) and

  uminus ("-_" [78] 73) and

  atom ("|_|") and

  If  ("if _ then _ else _" 10) and

  Rep_name ("\<lfloor>_\<rfloor>") and

  Abs_name ("\<lceil>_\<rceil>") and

  Rep_var ("\<lfloor>_\<rfloor>") and

  Abs_var ("\<lceil>_\<rceil>") and

  sort_of_ty ("sort'_ty _")

(* BH: uncomment if you really prefer the dot notation

syntax (latex output)

  "_Collect" :: "pttrn => bool => 'a set" ("(1{_ . _})")

*)

(* sort is used in Lists for sorting *)

hide_const sort

abbreviation

  "sort \<equiv> sort_of"

abbreviation

  "sort_ty \<equiv> sort_of_ty"

(*>*)

(*

  TODO: write about supp of finite sets, abstraction over finite sets

*)

section {* Introduction *}

text {*

  Nominal Isabelle provides a proving infratructure for convenient reasoning

  quantifications in type schemes:

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

  @{text "\<lambda>x. t       \<forall>{x\<^isub>1,\<dots>,x\<^isub>n}. \<tau>"}

  \hfill\numbered{atomperm}

  \end{isabelle}

  \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

  sort-respecting permutation operation defined over a countably infinite

  collection of sorted atoms. The atoms are used for representing variable names

  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. 

  @{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

  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 

  @{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

  case that a swapping of two atoms is ill-sorted: we cannot rely anymore on

  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

  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

  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

  using this representation we will not be able to reuse the extensive

  Using a single atom type to represent atoms of different sorts and

*}

section {* Sorted Atoms and Sort-Respecting Permutations *}

text {*

  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

  basic requirement is that there must be a countably infinite number of atoms

  of each sort.  We implement these atoms as

*}

          datatype atom\<iota> = Atom\<iota> string nat

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}

  convenience; any countably infinite type would work as well.) We have an

  auxiliary function @{text sort} that is defined as @{thm

  sort_of.simps[no_vars]}, and we clearly have for every finite set @{text X}

  of atoms and every sort @{text s} the property:

  \begin{proposition}\label{choosefresh}

  @{text "For a finite set of atoms S, there exists an atom a such that

  sort a = s and a \<notin> S"}.

  \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

  each atom to one of the same sort. These properties can be conveniently stated

  for a function @{text \<pi>} as follows:

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

  \begin{tabular}{r@ {\hspace{4mm}}l}

  i)   & @{term "bij \<pi>"}\\

  ii)  & @{term "finite {a. \<pi> a \<noteq> a}"}\\

  iii) & @{term "\<forall>a. sort (\<pi> a) = sort a"}

  \end{tabular}\hfill\numbered{permtype}

  \end{isabelle}

  \noindent

  Like all HOL-based theorem provers, Isabelle/HOL allows us to

  introduce a new type @{typ perm} that includes just those functions

  satisfying all three properties. For example the identity function,

  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"}. 

  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

  to work with swappings, written @{text "(a b)"}.  In our setting the

  type of swappings must be

  @{text [display,indent=10] "(_ _) :: atom \<Rightarrow> atom \<Rightarrow> perm"}

  \noindent

  but since permutations are required to respect sorts, we must carefully

  consider what happens if a user states a swapping of atoms with different

  sorts.  In early versions of Nominal Isabelle, we avoided this problem by

  using different types for different sorts; the type system prevented users

  from stating ill-sorted swappings.  Here, however, definitions such 

  as\footnote{To increase legibility, we omit here and in what follows the

  @{term Rep_perm} and @{term "Abs_perm"} wrappers that are needed in our

  implementation since we defined permutation not to be the full function space,

  but only those functions of type @{typ perm} satisfying properties @{text

  i}-@{text "iii"}.}

  @{text [display,indent=10] "(a b) \<equiv> \<lambda>c. if a = c then b else (if b = c then a else c)"}

  \noindent

  do not work in general, because the type system does not prevent @{text a}

  and @{text b} from having different sorts---in which case the function would

  violate property @{text iii}.  We could make the definition of swappings

  partial by adding the precondition @{term "sort a = sort b"},

  which would mean that in case @{text a} and @{text b} have different sorts,

  the value of @{text "(a b)"} is unspecified.  However, this looked like a

  cumbersome solution, since sort-related side conditions would be required

  everywhere, even to unfold the definition.  It turned out to be more

  convenient to actually allow the user to state ``ill-sorted'' swappings but

  limit their ``damage'' by defaulting to the identity permutation in the

  ill-sorted case:

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

  \begin{tabular}{@ {}rl}

  @{text "(a b) \<equiv>"} & @{text "if (sort a = sort b)"}\\ 

   & \hspace{3mm}@{text "then \<lambda>c. if a = c then b else (if b = c then a else c)"}\\ 

   & \hspace{3mm}@{text "else id"}

  \end{tabular}\hfill\numbered{swapdef}

  \end{isabelle}

  \noindent

  This function is bijective, the identity on all atoms except

  @{text a} and @{text b}, and sort respecting. Therefore it is 

  a function in @{typ perm}. 

  One advantage of using functions instead of lists as a representation for

  permutations is that for example the swappings

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

  \begin{tabular}{@ {}l}

  @{thm swap_commute[no_vars]}\hspace{10mm}

  @{text "(a a) = id"}

  \end{tabular}\hfill\numbered{swapeqs}

  \end{isabelle}

  \noindent

  are \emph{equal}.  We do not have to use the equivalence relation shown

  in~\eqref{permequ} to identify them, as we would if they had been represented

  as lists of pairs.  Another advantage of the function representation is that

  they form a (non-commutative) group provided we define

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

  \begin{tabular}{@ {}l}

  @{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 a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2"]} 

  \end{tabular}

  \end{isabelle}

  \noindent

  and verify the simple properties

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

  \begin{tabular}{@ {}l}

  @{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]} \hspace{3mm}

  @{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{3mm}

  @{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{3mm}

  @{thm group_add_class.left_minus[where a="\<pi>::perm"]} 

  \end{tabular}

  \end{isabelle}

  \noindent

  Again this is in contrast to the list-of-pairs representation which does not

  form a group.  The technical importance of this fact is that we can rely on

  Isabelle/HOL's existing simplification infrastructure for groups, which will

  come in handy when we have to do calculations with permutations.

  Note that Isabelle/HOL defies standard conventions of mathematical notation

  by using additive syntax even for non-commutative groups.  Obviously,

  composition of permutations is not commutative in general, because @{text

  "\<pi>\<^sub>1 + \<pi>\<^sub>2 \<noteq>  \<pi>\<^sub>2 + \<pi>\<^sub>1"}.  But since the point of this paper is to implement the

  nominal theory as smoothly as possible in Isabelle/HOL, we tolerate

  the non-standard notation in order to reuse the existing libraries.

  By formalising permutations abstractly as functions, and using a single type

  for all atoms, we can now restate the \emph{permutation properties} from

  \eqref{permprops} as just the two equations

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

  \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}

  i) & @{thm permute_zero[no_vars]}\\

  ii) & @{thm permute_plus[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2",no_vars]}

  \end{tabular}\hfill\numbered{newpermprops}

  \end{isabelle} 

  \noindent

  in which the permutation operations are of type @{text "perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} and so

  have only a single type parameter.  Consequently, these properties are

  compatible with the one-parameter restriction of Isabelle/HOL's type classes.

  There is no need to introduce a separate type class instantiated for each

  sort, like in the old approach.

  The next notion allows us to establish generic lemmas involving the

  permutation operation.

  \begin{definition}

  A type @{text "\<beta>"} is a \emph{permutation type} if the permutation

  properties in \eqref{newpermprops} are satisfied for every @{text "x"} of type

  @{text "\<beta>"}.  

  \end{definition}

  \noindent

  First, it follows from the laws governing

  groups that a permutation and its inverse cancel each other.  That is, for any

  @{text "x"} of a permutation type:

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

  \begin{tabular}{@ {}l}

  @{thm permute_minus_cancel(1)[where p="\<pi>", no_vars]}\hspace{10mm}

  @{thm permute_minus_cancel(2)[where p="\<pi>", no_vars]}

  \end{tabular}\hfill\numbered{cancel}

  \end{isabelle} 

  \noindent

  which in turn implies the property

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

  \begin{tabular}{@ {}l}

  @{thm (lhs) permute_eq_iff[where p="\<pi>", no_vars]}

  $\;$if and only if$\;$

  @{thm (rhs) permute_eq_iff[where p="\<pi>", no_vars]}.

  \end{tabular}\hfill\numbered{permuteequ}

  \end{isabelle} 

  \noindent

  In order to lift the permutation operation to other types, we can define for:

  \noindent

  and then establish:

  \begin{theorem}

  If @{text \<beta>}, @{text "\<beta>\<^isub>1"} and @{text "\<beta>\<^isub>2"} are permutation types, 

  then so are @{text "atom"}, @{text "\<beta>\<^isub>1 \<Rightarrow> \<beta>\<^isub>2"}, 

  @{text perm}, @{term "\<beta> set"}, @{term "\<beta> list"}, @{term "\<beta>\<^isub>1 \<times> \<beta>\<^isub>2"},

  @{text bool} and @{text "nat"}.

  \end{theorem}

  \begin{proof}

  All statements are by unfolding the definitions of the permutation operations and simple 

  calculations involving addition and minus. With permutations for example we 

  have

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

  \begin{tabular}[b]{@ {}rcl}

  @{text "0 \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "0 + \<pi>' - 0 = \<pi>'"}\\

  @{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>'"} 

  \end{tabular}\hfill\qed

  \end{isabelle}

  \end{proof}

*}

section {* Equivariance *}

text {*

  \begin{definition}\label{equivariance}

  A function @{text f} is \emph{equivariant} if @{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}.

  \end{definition}

  \noindent

  There are a number of equivalent formulations for the equivariance property. 

  For example, assuming @{text f} is of type @{text "\<alpha> \<Rightarrow> \<beta>"}, then equivariance 

  can also be stated as 

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

  \begin{tabular}{@ {}l}

  @{text "\<forall>\<pi> x.  \<pi> \<bullet> (f x) = f (\<pi> \<bullet> x)"}

  \end{tabular}\hfill\numbered{altequivariance}

  \end{isabelle} 

  \noindent

  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 

  the fact 

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

  \begin{tabular}{@ {}l}

  @{text "\<pi> \<bullet> (f x) = (\<pi> \<bullet> f) (\<pi> \<bullet> x)"}

  \end{tabular}\hfill\numbered{permutefunapp}

  \end{isabelle} 

  \noindent

  which follows again directly 

  from the definition of the permutation operation for functions and the cancellation 

  property. Similarly for functions with more than one argument. 

  Both formulations of equivariance have their advantages and disadvantages:

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%