(*<*)

theory Paper

imports "../Nominal-General/Nominal2_Base" 

        "../Nominal-General/Nominal2_Eqvt"

        "../Nominal-General/Atoms" 

        "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

  about programming languages involving binders such as lambda abstractions or

  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. 

  In our formalisation of the nominal logic work, we have to make a design decision 

  about how to represent sorted atoms and sort-respecting permutations. One possibility

  permutations as lists of pairs of atoms and the operation of applying

  a permutation to an object as the overloaded 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 of different type, the permutation operation

  is defined as @{text "\<pi> \<bullet> c \<equiv> c"}.

  With the separate atom types and the list representation of permutations it

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

  \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}

  \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

*}

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

*}

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

text {*

  \noindent

  \begin{proposition}\label{choosefresh}

  \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

  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

  Consequently, in a permutation type the permutation operation @{text "\<pi> \<bullet> _"} is bijective, 

  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:

  \begin{isabelle}

  \begin{tabular}{@ {}c@ {\hspace{-1mm}}c@ {}}

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

  atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\

  functions: &  @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\

  permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\

  sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\

   booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\

  \end{tabular} &

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

  lists: & @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\

         & @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\[2mm]

  products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\

  nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\

  \end{tabular}

  \end{tabular}

  \end{isabelle}

  \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}

  \noindent

  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. We can also show once and for all that the following

  property---which caused so many headaches in our earlier setup---holds for any

  permutation type.

  \begin{lemma}\label{permutecompose} 

  Given @{term x} is of permutation type, then 

  @{text "\<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x) = (\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}.

  \end{lemma}

  \begin{proof} The proof is as follows:

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

  \begin{tabular}[b]{@ {}rcl@ {\hspace{8mm}}l}

  @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> x"}

  & @{text "="} & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> (-\<pi>\<^isub>1) \<bullet> \<pi>\<^isub>1 \<bullet> x"} & by \eqref{cancel}\\

  & @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2 - \<pi>\<^isub>1) \<bullet> \<pi>\<^isub>1 \<bullet> x"}  & by {\rm(\ref{newpermprops}.@{text "ii"})}\\

  & @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}\\

  \end{tabular}\hfill\qed

  \end{isabelle}

  \end{proof}

*}

section {* Equivariance *}

text {*

  An \emph{equivariant} function or predicate is one that is invariant under

  the swapping of atoms.  Having a notion of equivariance with nice logical

  properties is a major advantage of bijective permutations over traditional

  renaming substitutions \cite[\S2]{Pitts03}.  Equivariance can be defined

  uniformly for all permutation types, and it is satisfied by most HOL

  functions and constants.

  \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:

  \eqref{altequivariance} is often easier to establish. For example we 

  can easily show that equality is equivariant

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

  \begin{tabular}{@ {}l}

  @{thm eq_eqvt[where p="\<pi>", no_vars]}

  \end{tabular}

  \end{isabelle} 

  \noindent

  using the permutation operation on booleans and property \eqref{permuteequ}. 

  Lemma~\ref{permutecompose} establishes that the permutation operation is 

  equivariant. It is also easy to see that the boolean operators, like