(*<*)

theory Paper

imports "../Nominal/Nominal2_Base" 

        "../Nominal/Atoms" 

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

  fresh_star ("_ #\<^sup>* _" [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

  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

  sort-respecting permutation operation defined over a countably infinite

  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

  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.

  The paper is organised as follows\ldots

*}

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}

  for their variables.}  (The use of 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 "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}

  \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

  We can also show that the following property 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}

  \noindent

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

  \begin{equation}\label{permdefs}

  \mbox{

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

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

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

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

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

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

  6) & 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]}\\

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

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

  \end{tabular}}

  \end{equation}

  \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 {*

  An important notion in the nominal logic work is \emph{equivariance}.

  An equivariant function or predicate is one that is invariant under

  the swapping of atoms. This notion can be defined

  uniformly as follows:

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

  the definition, \eqref{permutefunapp} and (\ref{permdefs}.2) lead to a simple

  rewrite system that pushes permutations inside a term until they reach

  either function constants or variables. The permutations in front of

  equivariant functions disappear. Such a rewrite system is often very helpful

  in determining whether @{text "p \<bullet> t = t"} holds for a compound term @{text t}. In contrast

  \eqref{altequivariance} is usually easier to establish, since statements are

  commonly given in a form where functions are fully applied. 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 

  @{text "\<and>"}, @{text "\<or>"} and @{text "\<longrightarrow>"} are all equivariant. Furthermore 

  a simple calculation will show that our swapping functions are equivariant, that is

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

  \begin{tabular}{@ {}l}

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

  \end{tabular}\hfill\numbered{swapeqvt}

  \end{isabelle} 

  \noindent

  for all @{text a}, @{text b} and @{text \<pi>}.  

*}

section {* Support and Freshness *}

text {*

  The most original aspect of the nominal logic work of Pitts et al is a general

  definition for ``the set of free variables of an object @{text "x"}''.  This

  definition is general in the sense that it applies not only to lambda-terms,

  but also to lists, products, sets and even functions. The definition depends

  only on the permutation operation and on the notion of equality defined for

  the type of @{text x}, namely:

  @{thm [display,indent=10] supp_def[no_vars, THEN eq_reflection]}

  \noindent

  (Note that due to the definition of swapping in \eqref{swapdef}, we do not

  need to explicitly restrict @{text a} and @{text b} to have the same sort.)

  There is also the derived notion for when an atom @{text a} is \emph{fresh}

  for an @{text x}, defined as

  @{thm [display,indent=10] fresh_def[no_vars]}

  \noindent

  We also use the notation @{thm (lhs) fresh_star_def[no_vars]} for sets ot atoms 

  defined as follows

  @{thm [display,indent=10] fresh_star_def[no_vars]}

  \noindent

  A striking consequence of these definitions is that we can prove

  without knowing anything about the structure of @{term x} that

  swapping two fresh atoms, say @{text a} and @{text b}, leave 

  @{text x} unchanged. For the proof we use the following lemma 

  about swappings applied to an @{text x}:

  \begin{lemma}\label{swaptriple}

  Assuming @{text x} is of permutation type, and @{text a}, @{text b} and @{text c} 

  have the same sort, then @{thm (prem 3) swap_rel_trans[no_vars]} and 

  @{thm (prem 4) swap_rel_trans[no_vars]} imply @{thm (concl) swap_rel_trans[no_vars]}.

  \end{lemma}

  \begin{proof}

  The cases where @{text "a = c"} and @{text "b = c"} are immediate.

  For the remaining case it is, given our assumptions, easy to calculate 

  that the permutations

  @{thm [display,indent=10] (concl) swap_triple[no_vars]}

  \noindent

  are equal. The lemma is then by application of the second permutation 

  property shown in \eqref{newpermprops}.\hfill\qed

  \end{proof}

  \begin{theorem}\label{swapfreshfresh}

  Let @{text x} be of permutation type.

  @{thm [mode=IfThen] swap_fresh_fresh[no_vars]}

  \end{theorem}

  \begin{proof}

  If @{text a} and @{text b} have different sort, then the swapping is the identity.

  If they have the same sort, we know by definition of support that both

  @{term "finite {c. (a \<rightleftharpoons> c) \<bullet> x \<noteq> x}"} and  @{term "finite {c. (b \<rightleftharpoons> c) \<bullet> x \<noteq> x}"}

  hold. So the union of these sets is finite too, and we know by Proposition~\ref{choosefresh} 

  that there is an atom @{term c}, with the same sort as @{term a} and @{term b}, 

  that satisfies \mbox{@{term "(a \<rightleftharpoons> c) \<bullet> x = x"}} and @{term "(b \<rightleftharpoons> c) \<bullet> x = x"}. 

  Now the theorem follows from Lemma~\ref{swaptriple}.\hfill\qed

  \end{proof}

  \noindent

  Two important properties that need to be established for later calculations is 

  that @{text "supp"} and freshness are equivariant. For this we first show that:

  \begin{lemma}\label{half}

  If @{term x} is a permutation type, then @{thm (lhs) fresh_permute_iff[where p="\<pi>",no_vars]} 

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

  \end{lemma}

  \begin{proof}

  \begin{isabelle}

  \begin{tabular}[t]{c@ {\hspace{2mm}}l@ {\hspace{5mm}}l}

  & \multicolumn{2}{@ {}l}{@{thm (lhs) fresh_permute_iff[where p="\<pi>",no_vars]} @{text "\<equiv>"}

    @{term "finite {b. (\<pi> \<bullet> a \<rightleftharpoons> b) \<bullet> \<pi> \<bullet> x \<noteq> \<pi> \<bullet> x}"}}\\

  @{text "\<Leftrightarrow>"}

  & @{term "finite {b. (\<pi> \<bullet> a \<rightleftharpoons> \<pi> \<bullet> b) \<bullet> \<pi> \<bullet> x \<noteq> \<pi> \<bullet> x}"} 

  & since @{text "\<pi> \<bullet> _"} is bijective\\ 

  @{text "\<Leftrightarrow>"}