(*<*)

theory Paper

imports "../Nominal/Nominal2_Base" 

        "../Nominal/Atoms" 

        "../Nominal/Nominal2_Abs"

        "~~/src/HOL/Library/LaTeXsugar"

begin

abbreviation

 UNIV_atom ("\<allatoms>")

where

 "UNIV_atom \<equiv> UNIV::atom set" 

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"

lemma infinite_collect:

  assumes "\<forall>x \<in> S. P x" "infinite S"

  shows "infinite {x \<in> S. P x}"

using assms

apply(subgoal_tac "infinite {x. x \<in> S}")

apply(simp only: Inf_many_def[symmetric])

apply(erule INFM_mono)

apply(auto)

done

(*>*)

section {* Introduction *}

text {*

  Nominal Isabelle provides a proving infratructure for convenient reasoning

  about syntax involving binders, such as lambda terms or type schemes in Mini-ML:

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

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

  \end{isabelle}

  \noindent

  At its core Nominal Isabelle is based on the nominal logic work by

  Pitts at al \cite{GabbayPitts02,Pitts03}, whose most basic notion is

  a sort-respecting permutation operation defined over a countably

  infinite collection of sorted atoms. 

  The aim of this paper is to

  describe how we adapted this work so that it can be implemented in a

  theorem prover based on Higher-Order Logic (HOL). For this we

  present the definition we made in the implementation and also review

  many proofs. There are a two main design choices to be made. One is

  how to represent sorted atoms. We opt here for a single unified atom

  type to represent atoms of different sorts. The other is how to

  present sort-respecting permutations. For them we use the standard

  technique of HOL-formalisations of introducing an appropriate

  substype of functions from atoms to atoms.

  The nominal logic work has been the starting point for a number of proving

  infrastructures, most notable by Norrish \cite{norrish04} in HOL4, by

  Aydemir et al \cite{AydemirBohannonWeirich07} in Coq and the work by Urban

  and Berghofer in Isabelle/HOL \cite{Urban08}. Its key attraction is a very

  general notion, called \emph{support}, for the `set of free variables, or

  atoms, of an object' that applies not just to lambda terms and type schemes,

  but also to sets, products, lists, booleans and even functions. The notion of support

  is derived from the permutation operation defined over the 

  hierarchy of types. This

  permutation operation, written @{text "_ \<bullet> _"}, has proved to be much more

  convenient for reasoning about syntax, in comparison to, say, arbitrary

  renaming substitutions of atoms. One reason is that permutations are

  bijective renamings of atoms and thus they can be easily `undone'---namely

  by applying the inverse permutation. A corresponding inverse substitution 

  might not always exist, since renaming substitutions are in general only injective.  

  Another reason is that permutations preserve many constructions when reasoning about syntax. 

  For example, suppose a typing context @{text "\<Gamma>"} of the form

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

  @{text "x\<^isub>1:\<tau>\<^isub>1, \<dots>, x\<^isub>n:\<tau>\<^isub>n"}

  \end{isabelle}

  \noindent

  is said to be \emph{valid} provided none of its variables, or atoms, @{text "x\<^isub>i"}

  occur twice. Then validity of typing contexts is preserved under

  permutations in the sense that if @{text \<Gamma>} is valid then so is \mbox{@{text "\<pi> \<bullet> \<Gamma>"}} for

  all permutations @{text "\<pi>"}. Again, this is \emph{not} the case for arbitrary

  renaming substitutions, as they might identify some of the @{text "x\<^isub>i"} in @{text \<Gamma>}. 

  Permutations also behave uniformly with respect to HOL's logic connectives. 

  Applying a permutation to a formula gives, for example 

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

  \begin{tabular}{@ {}lcl}

  @{term "\<pi> \<bullet> (A \<and> B)"} & if and only if & @{text "(\<pi> \<bullet> A) \<and> (\<pi> \<bullet> B)"}\\

  @{term "\<pi> \<bullet> (A \<longrightarrow> B)"} & if and only if & @{text "(\<pi> \<bullet> A) \<longrightarrow> (\<pi> \<bullet> B)"}\\

  \end{tabular}

  \end{isabelle}

  \noindent

  This uniform behaviour can also be extended to quantifiers and functions. 

  Because of these good properties of permutations, we are able to automate 

  reasoning to do with \emph{equivariance}. By equivariance we mean the property 

  that every permutation leaves a function unchanged, that is @{term "\<pi> \<bullet> f = f"}

  for all @{text "\<pi>"}. This will often simplify arguments involving support 

  of functions, since if they are equivariant then they have empty support---or

  `no free atoms'.

  There are a number of subtle differences between the nominal logic work by

  Pitts and the formalisation we will present in this paper. One difference 

  is that our

  formalisation is compatible with HOL, in the sense that we only extend

  HOL by some definitions, withouth the introduction of any new axioms.

  The reason why the original nominal logic work is

  incompatible with HOL has to do with the way how the finite support property

  is enforced: FM-set theory is defined in \cite{Pitts01b} so that every set

  in the FM-set-universe has finite support.  In nominal logic \cite{Pitts03},

  the axioms (E3) and (E4) imply that every function symbol and proposition

  has finite support. However, there are notions in HOL that do \emph{not}

  have finite support (we will give some examples).  In our formalisation, we 

  will avoid the incompatibility of the original nominal logic work by not a

  priory restricting our discourse to only finitely supported entities, rather

  we will explicitly assume this property whenever it is needed in proofs. One

  consequence is that we state our basic definitions not in terms of nominal

  sets (as done for example in \cite{Pitts06}), but in terms of the weaker

  notion of permutation types---essentially sets equipped with a ``sensible''

  notion of permutation operation.

  In the nominal logic woworkrk, the `new quantifier' plays a prominent role.

  $\new$

  Two binders

  A preliminary version 

*}

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

text {*

  The two most basic notions in the nominal logic work are a countably

  infinite collection of sorted atoms and sort-respecting permutations

  of 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 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 different sorts of

  atoms. However, we found that this does not blend well with

  type-classes in Isabelle/HOL (see Section~\ref{related} about

  related work).  Therefore we use here a single unified atom type to

  represent atoms of different sorts. A basic requirement is that

  there must be a countably infinite number of atoms of each sort.

*}

          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} for sorts is merely for convenience; any countably

  infinite type would work as well.  In what follows we shall write

  @{term "UNIV::atom set"} for the set of all atoms.  We also have two

  auxiliary functions for atoms, namely @{text sort} and @{const

  nat_of} which are defined as

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

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

  @{thm (lhs) sort_of.simps[no_vars]} & @{text "\<equiv>"} & @{thm (rhs) sort_of.simps[no_vars]}\\

  @{thm (lhs) nat_of.simps[no_vars]} & @{text "\<equiv>"}  & @{thm (rhs) nat_of.simps[no_vars]}

  \end{tabular}\hfill\numbered{sortnatof}

  \end{isabelle}

  \noindent

  We clearly have for every finite set @{text S}

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

  \begin{proposition}\label{choosefresh}\mbox{}\\

  @{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 are bijective; are the

  identity on all atoms, except a finite number of them; and map

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

  in Isabelle/HOL 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 

  (\ref{permtype}.@{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.  The following definition\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 in Isabelle/HOL 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"} in \eqref{permtype}.}

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

  \noindent

  does not work in general, because @{text a} and @{text b} may have different

  sorts---in which case the function would violate property @{text iii} in \eqref{permtype}.  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 as a representation for

  permutations is that it is a unique representation. 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} and can be used interchangeably. Another advantage of the function 

  representation is that they form a (non-com\-mu\-ta\-tive) group provided we define

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

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

  @{thm (lhs) zero_perm_def[no_vars]} & @{text "\<equiv>"} & @{thm (rhs) zero_perm_def[no_vars]} &

  @{thm (lhs) plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2"]} & @{text "\<equiv>"} & 

     @{thm (rhs) plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2"]}\\

  @{thm (lhs) uminus_perm_def[where p="\<pi>"]} & @{text "\<equiv>"} & @{thm (rhs) uminus_perm_def[where p="\<pi>"]} &

  @{thm (lhs) minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^isub>2"]} & @{text "\<equiv>"} &

     @{thm (rhs) minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^isub>2"]}

  \end{tabular}\hfill\numbered{groupprops}

  \end{isabelle}

  \noindent

  and verify the four simple properties

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

  \begin{tabular}{@ {}l}

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

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

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

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

  \end{tabular}\hfill\numbered{grouplaws}

  \end{isabelle}

  \noindent

  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; for example

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

  @{text "(a b) + (b c) \<noteq> (b c) + (a b)"}\;.

  \end{isabelle} 

  \noindent

  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.

  A \emph{permutation operation}, written infix as @{text "\<pi> \<bullet> x"},

  applies a permutation @{text "\<pi>"} to an object @{text "x"}.  This 

  operation has the type

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

  @{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}

  \end{isabelle} 

  \noindent

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

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

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

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

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

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

  \end{tabular}\hfill\numbered{permdefsbase}

  \end{isabelle}

  \noindent

  and for type-constructors, such as functions, sets, lists and products:

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

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

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

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

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

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

  \end{tabular}\hfill\numbered{permdefsconstrs}

  \end{isabelle}

  \noindent

  The type classes also allow us to reason abstractly about the permutation operation. 

  For this we state the following two 

  \emph{permutation properties}: 

  \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

  From these properties and law (\ref{grouplaws}.{\it iv}) about groups 

  follows that a permutation and its inverse cancel each other. That is

  \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, 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 the permutation 

  operation.

  \begin{lemma}\label{permutecompose} 

  @{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]{@ {}c@ {\hspace{2mm}}l@ {\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

  Note that the permutation operation for functions is defined so that

  we have for applications the equation

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

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

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

  \hfill\numbered{permutefunapp}

  \end{isabelle}

  \noindent

  be easily shown by unfolding the permutation operation for functions on

  The main benefit of the use of type classes is that it allows us to delegate 

  much of the routine resoning involved in determining whether the permutation properties

  are satisfied to Isabelle/HOL's type system: we only have to

  establish that base types satisfy them and that type-constructors

  whether an object @{text x} with a compound type, like @{typ "atom \<Rightarrow> (atom set * nat)"}, satisfies the

  permutation properties.  For this we define the notion of a

  \emph{permutation type}:

  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

  and establish:

  \begin{theorem}

  The types @{type atom}, @{type perm}, @{type bool} and @{type nat}

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

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

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

  \end{theorem}

  \begin{proof}

  All statements are by unfolding the definitions of the permutation

  operations and simple calculations involving addition and

  minus. In case of permutations for example we have

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

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

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

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