(*<*)

theory Paper

imports "../Nominal-General/Nominal2_Base" 

        "../Nominal-General/Nominal2_Atoms" 

        "../Nominal-General/Nominal2_Eqvt"

        "../Nominal-General/Nominal2_Supp" 

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

(*>*)

section {* Introduction *}

text {*

  Nominal Isabelle provides a proving infratructure for

  convenient reasoning about programming languages. 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 variables

  that might be bound. 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 and bound type variables; each kind needs to

  be represented by a different sort of atoms.

  Unfortunately, the type system of Isabelle/HOL is not a good fit for the way

  atoms and sorts are used in the original formulation of the nominal logic work.

  The reason is that one has to ensure that permutations are sort-respecting.

  This was done implicitly in the original nominal logic work \cite{Pitts03}.

  Isabelle used the two-place permutation operation with the generic type

  @{text [display,indent=10] "_ \<bullet> _  ::  (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}

  \noindent 

  where @{text "\<alpha>"} stands for the type of atoms and @{text "\<beta>"} for the type

  of the objects on which the permutation acts. For atoms of type @{text "\<alpha>"} 

  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 list representation of permutations it is impossible to state an

  ``ill-sorted'' permutation, since the type system excludes lists containing

  atoms of different type. Another advantage of the list representation is that

  the basic operations on permutations are already defined in the 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. A disadvantage is that permutations do not have unique

  representations as lists; we had to explicitly identify permutations 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}

  When lifting the permutation operation to other types, for example sets,

  functions and so on, we needed to ensure that every definition is

  well-behaved in the sense that it satisfies the following three 

  \emph{permutation properties}:

  \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

  From these properties we were able to derive most facts about permutations, and 

  the type classes of Isabelle/HOL allowed us to reason abstractly about these

  three properties, and then let the type system automatically enforce these

  properties for each type.

  The major problem with Isabelle/HOL's type classes, however, is that they

  support operations with only a single type parameter and the permutation

  operations @{text "_ \<bullet> _"} used above in the permutation properties

  contain two! To work around this obstacle, Nominal Isabelle 

  required the user to

  declare up-front the collection of \emph{all} atom types, say @{text

  "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}. From this collection it used custom ML-code to

  generate @{text n} type classes corresponding to the permutation properties,

  whereby in these type classes the permutation operation is restricted to

  @{text [display,indent=10] "_ \<bullet> _ :: (\<alpha>\<^isub>i \<times> \<alpha>\<^isub>i) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}

  \noindent

  This operation has only a single type parameter @{text "\<beta>"} (the @{text "\<alpha>\<^isub>i"} are the

  atom types given by the user). 

  While the representation of permutations-as-lists solved the

  ``sort-respecting'' requirement and the declaration of all atom types

  up-front solved the problem with Isabelle/HOL's type classes, this setup

  caused several problems for formalising the nominal logic work: First,

  Nominal Isabelle had to generate @{text "n\<^sup>2"} definitions for the

  permutation operation over @{text "n"} types of atoms.  Second, whenever we

  need to generalise induction hypotheses by quantifying over permutations, we

  have to build cumbersome 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"}. Third, although the notion of support

  @{text [display,indent=10] "supp _ :: \<beta> \<Rightarrow> \<alpha> set"}

  \noindent

  which we will define later, has a generic type @{text "\<alpha> set"}, it cannot be

  used to express the support of an object over \emph{all} atoms. The reason

  is again 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

  Sometimes we can avoid such premises completely, if @{text x} is a member of a

  \emph{finitely supported type}.  However, keeping track of finitely supported

  types requires another @{text n} type classes, and for technical reasons not

  all types can be shown to be finitely supported.

  The real pain of having a separate type for each atom sort arises, however, 

  from another permutation property

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

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

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

  \end{tabular}

  \end{isabelle}

  \noindent

  where permutation @{text "\<pi>\<^isub>1"} has type @{text "(\<alpha> \<times> \<alpha>) list"},

  @{text "\<pi>\<^isub>2"} type @{text "(\<alpha>' \<times> \<alpha>') list"} and @{text x} type @{text

  "\<beta>"}. This property is needed in order to derive facts about how

  permutations of different types interact, which is not covered by the

  permutation properties @{text "i"}-@{text "iii"} shown in

  \eqref{permprops}. The problem is that this property involves three type

  parameters. In order to use again Isabelle/HOL's type class mechanism with

  only permitting a single type parameter, we have to instantiate the atom

  types. Consequently we end up with an additional @{text "n\<^sup>2"}

  slightly different type classes for this permutation property.

  While the problems and pain can be almost completely hidden from the user in

  the existing implementation of Nominal Isabelle, the work is \emph{not}

  pretty. It requires a large amount of custom ML-code and also forces the

  user to declare up-front all atom-types that are ever going to be used in a

  formalisation. In this paper we set out to solve the problems with multiple

  type parameters in the permutation operation, and in this way can dispense

  with the large amounts of custom ML-code for generating multiple variants

  for some basic definitions. The result is that we can implement a pleasingly

  simple formalisation of the nominal logic work.\smallskip

  \noindent

  {\bf Contributions of the paper:} Using a single atom type to represent

  atoms of different sorts and representing permutations as functions are not

  new ideas.  The main contribution of this paper is to show an example of how

  to make better theorem proving tools by choosing the right level of

  abstraction for the underlying theory---our design choices take advantage of

  Isabelle's type system, type classes, and reasoning infrastructure.

  The novel

  technical contribution is a mechanism for dealing with

  ``Church-style'' lambda-terms \cite{Church40} and HOL-based languages

  \cite{PittsHOL4} where variables and variable binding depend on type

  annotations.

   Therefore it was decided in earlier versions of Nominal Isabelle to use a

  separate type for each sort of atoms and let the type system enforce the

  sort-respecting property of permutations. Inspired by the work on nominal

  unification \cite{UrbanPittsGabbay04}, it seemed best at the time to also

  implement permutations concretely as lists of pairs of atoms.

*}

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.  Unlike in our earlier work, where we identified each sort with

  a separate type, we implement here atoms to be

*}

          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} 

  for their variables.}  (The use type

  \emph{string} is merely for 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 "If finite X then there exists an atom a such that

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

  \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 earlier 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 x="\<pi>\<^isub>1" and y="\<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]}