1 (*<*)

     2 theory Paper

     3 imports "../Nominal/Nominal2_Base" 

     4         "../Nominal/Atoms" 

     5         "../Nominal/Nominal2_Abs"

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

     7 begin

     8 

     9 abbreviation

    10  UNIV_atom ("\<allatoms>")

    11 where

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

    13 

    14 notation (latex output)

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

    16   Abs_perm ("_") and

    17   Rep_perm ("_") and

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

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

    20   fresh_star ("_ #\<^sup>* _" [51, 51] 50) and

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

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

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

    24   atom ("|_|") and

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

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

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

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

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

    30   sort_of_ty ("sort'_ty _") 

    31 

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

    33 syntax (latex output)

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

    35 *)

    36 

    37 (* sort is used in Lists for sorting *)

    38 hide_const sort

    39 

    40 abbreviation

    41   "sort \<equiv> sort_of"

    42 

    43 lemma infinite_collect:

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

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

    46 using assms

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

    48 apply(simp only: Inf_many_def[symmetric])

    49 apply(erule INFM_mono)

    50 apply(auto)

    51 done

    52 

    53 

    54 (*>*)

    55 

    56 section {* Introduction *}

    57 

    58 text {*

    59   Nominal Isabelle provides a proving infratructure for convenient reasoning

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

    61 

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

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

    64   \end{isabelle}

    65   

    66   \noindent

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

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

    69   a sort-respecting permutation operation defined over a countably

    70   infinite collection of sorted atoms. 

    71 

    72 

    73 

    74   The aim of this paper is to

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

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

    77   present the definition we made in the implementation and also review

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

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

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

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

    82   technique of HOL-formalisations of introducing an appropriate

    83   subtype of functions from atoms to atoms.

    84 

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

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

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

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

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

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

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

    92   is derived from the permutation operation defined over the 

    93   hierarchy of types. This

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

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

    96   renaming substitutions of atoms. One reason is that permutations are

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

    98   by applying the inverse permutation. A corresponding inverse substitution 

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

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

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

   102 

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

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

   105   \end{isabelle}

   106 

   107   \noindent

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

   109   occur twice. Then validity of typing contexts is preserved under

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

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

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

   113 

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

   115   Applying a permutation to a formula gives, for example 

   116   

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

   118   \begin{tabular}{@ {}lcl}

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

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

   121   \end{tabular}

   122   \end{isabelle}

   123 

   124   \noindent

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

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

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

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

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

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

   131   `no free atoms'.

   132 

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

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

   135   is that our

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

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

   138   The reason why the original nominal logic work is

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

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

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

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

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

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

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

   146   priory restricting our discourse to only finitely supported entities, rather

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

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

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

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

   151   notion of permutation operation.

   152 

   153 

   154 

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

   156   $\new$

   157 

   158 

   159   Obstacles for Coq; no type-classes, difficulties with quotient types,

   160   need for classical reasoning

   161 

   162   Two binders

   163 

   164   A preliminary version 

   165 *}

   166 

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

   168 

   169 text {*

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

   171   infinite collection of sorted atoms and sort-respecting permutations

   172   of atoms.  The atoms are used for representing variable names that

   173   might be bound or free. Multiple sorts are necessary for being able

   174   to represent different kinds of variables. For example, in the

   175   language Mini-ML there are bound term variables in lambda

   176   abstractions and bound type variables in type schemes. In order to

   177   be able to separate them, each kind of variables needs to be

   178   represented by a different sort of atoms.

   179 

   180 

   181   The existing nominal logic work usually leaves implicit the sorting

   182   information for atoms and leaves out a description of how sorts are

   183   represented.  In our formalisation, we therefore have to make a

   184   design decision about how to implement sorted atoms and

   185   sort-respecting permutations. One possibility, which we described in

   186   \cite{Urban08}, is to have separate types for different sorts of

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

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

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

   190   represent atoms of different sorts. A basic requirement is that

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

   192   This can be implemented in Isabelle/HOL as the datatype

   193 

   194 *}

   195 

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

   197 

   198 text {*

   199   \noindent

   200   whereby the string argument specifies the sort of the

   201   atom.\footnote{A similar design choice was made by Gunter et al

   202   \cite{GunterOsbornPopescu09} for their variables.}  The use of type

   203   \emph{string} for sorts is merely for convenience; any countably

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

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

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

   207   nat_of} which are defined as

   208 

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

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

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

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

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

   214   \end{isabelle}

   215 

   216   \noindent

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

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

   219 

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

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

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

   223   \end{proposition}

   224 

   225   \noindent

   226   This property will be used later whenever we have to chose a `fresh' atom.

   227 

   228   For implementing sort-respecting permutations, we use functions of type @{typ

   229   "atom => atom"} that are bijective; are the

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

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

   232   in Isabelle/HOL for a function @{text \<pi>} as follows:

   233   

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

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

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

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

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

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

   240   \end{isabelle}

   241 

   242   \noindent

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

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

   245   satisfying all three properties. For example the identity function,

   246   written @{term id}, is included in @{typ perm}. Also function composition, 

   247   written  \mbox{@{text "_ \<circ> _"}}, and function inversion, given by Isabelle/HOL's 

   248   inverse operator and written \mbox{@{text "inv _"}}, preserve the properties 

   249   (\ref{permtype}.@{text "i"}-@{text "iii"}). 

   250 

   251   However, a moment of thought is needed about how to construct non-trivial

   252   permutations. In the nominal logic work it turned out to be most convenient

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

   254   type of swappings must be

   255 

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

   257 

   258   \noindent

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

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

   261   sorts.  The following definition\footnote{To increase legibility, we omit

   262   here and in what follows the @{term Rep_perm} and @{term "Abs_perm"}

   263   wrappers that are needed in our implementation in Isabelle/HOL since we defined permutation

   264   not to be the full function space, but only those functions of type @{typ

   265   perm} satisfying properties @{text i}-@{text "iii"} in \eqref{permtype}.}

   266 

   267 

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

   269 

   270   \noindent

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

   272   sorts---in which case the function would violate property @{text iii} in \eqref{permtype}.  We

   273   could make the definition of swappings partial by adding the precondition

   274   @{term "sort a = sort b"}, which would mean that in case @{text a} and

   275   @{text b} have different sorts, the value of @{text "(a b)"} is unspecified.

   276   However, this looked like a cumbersome solution, since sort-related side

   277   conditions would be required everywhere, even to unfold the definition.  It

   278   turned out to be more convenient to actually allow the user to state

   279   `ill-sorted' swappings but limit their `damage' by defaulting to the

   280   identity permutation in the ill-sorted case:

   281 

   282 

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

   284   \begin{tabular}{@ {}rl}

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

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

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

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

   289   \end{isabelle}

   290 

   291   \noindent

   292   This function is bijective, the identity on all atoms except

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

   294   a function in @{typ perm}. 

   295 

   296   One advantage of using functions as a representation for

   297   permutations is that it is a unique representation. For example the swappings

   298 

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

   300   \begin{tabular}{@ {}l}

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

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

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

   304   \end{isabelle}

   305 

   306   \noindent

   307   are \emph{equal} and can be used interchangeably. Another advantage of the function 

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

   309 

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

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

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

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

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

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

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

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

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

   319   \end{isabelle}

   320 

   321   \noindent

   322   and verify the four simple properties

   323 

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

   325   \begin{tabular}{@ {}l}

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

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

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

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

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

   331   \end{isabelle}

   332 

   333   \noindent

   334   The technical importance of this fact is that we can rely on

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

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

   337   Note that Isabelle/HOL defies standard conventions of mathematical notation

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

   339   composition of permutations is not commutative in general; for example

   340 

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

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

   343   \end{isabelle} 

   344 

   345   \noindent

   346   But since the point of this paper is to implement the

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

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

   349 

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

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

   352   operation has the type

   353 

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

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

   356   \end{isabelle} 

   357 

   358   \noindent

   359   whereby @{text "\<beta>"} is a generic type for the object @{text

   360   x}.\footnote{We will write @{text "((op \<bullet>) \<pi>)

   361   x"} for this operation in the few cases where we need to indicate

   362   that it is a function applied with two arguments.}  The definition

   363   of this operation will be given by in terms of `induction' over this

   364   generic type. The type-class mechanism of Isabelle/HOL

   365   \cite{Wenzel04} allows us to give a definition for `base' types,

   366   such as atoms, permutations, booleans and natural numbers:

   367 

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

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

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

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

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

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

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

   375   \end{isabelle}

   376 

   377   \noindent

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

   379   

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

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

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

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

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

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

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

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

   388   \end{isabelle}

   389 

   390   \noindent

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

   392   For this we state the following two 

   393   \emph{permutation properties}: 

   394   

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

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

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

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

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

   400   \end{isabelle} 

   401 

   402   \noindent

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

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

   405 

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

   407   \begin{tabular}{@ {}l}

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

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

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

   411   \end{isabelle} 

   412   

   413   \noindent

   414   Consequently, the permutation operation @{text "\<pi> \<bullet> _"}~~is bijective, 

   415   which in turn implies the property

   416 

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

   418   \begin{tabular}{@ {}l}

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

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

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

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

   423   \end{isabelle} 

   424 

   425   \noindent

   426   We can also show that the following property holds for the permutation 

   427   operation.

   428 

   429   \begin{lemma}\label{permutecompose} 

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

   431   \end{lemma}

   432 

   433   \begin{proof} The proof is as follows:

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

   435   \begin{tabular}[b]{@ {}c@ {\hspace{2mm}}l@ {\hspace{8mm}}l}

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

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

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

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

   440   \end{tabular}\hfill\qed

   441   \end{isabelle}

   442   \end{proof}

   443 

   444   \noindent

   445   Note that the permutation operation for functions is defined so that

   446   we have for applications the equation

   447 

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

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

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

   451   \hfill\numbered{permutefunapp}

   452   \end{isabelle}

   453 

   454   \noindent

   455   provided the permutation properties hold for @{text x}. This equation can

   456   be easily shown by unfolding the permutation operation for functions on

   457   the right-hand side of the equation, simplifying the resulting beta-redex 

   458   and eliminating the permutations in front of @{text x} using \eqref{cancel}.

   459 

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

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

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

   463   establish that base types satisfy them and that type-constructors

   464   preserve them. Then Isabelle/HOL will use this information and determine

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

   466   permutation properties.  For this we define the notion of a

   467   \emph{permutation type}:

   468 

   469   \begin{definition}[Permutation Type]

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

   471   properties in \eqref{newpermprops} are satisfied for every @{text

   472   "x"} of type @{text "\<beta>"}.

   473   \end{definition}

   474  

   475   \noindent

   476   and establish:

   477 

   478   \begin{theorem}

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

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

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

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

   483   \end{theorem}

   484 

   485   \begin{proof}

   486   All statements are by unfolding the definitions of the permutation

   487   operations and simple calculations involving addition and

   488   minus. In case of permutations for example we have

   489 

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

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

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

   493   @{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)"}\\

   494   & @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) + \<pi>' - \<pi>\<^isub>2 - \<pi>\<^isub>1"}\\

   495   & @{text "="} & @{text "\<pi>\<^isub>1 + (\<pi>\<^isub>2 + \<pi>' - \<pi>\<^isub>2) - \<pi>\<^isub>1"}\\

   496   & @{text "\<equiv>"} & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> \<pi>'"} 

   497   \end{tabular}\hfill\qed

   498   \end{isabelle}

   499   \end{proof}

   500 *}

   501 

   502 section {* Equivariance *}

   503 

   504 text {*

   505   (mention alpha-structural paper by Andy)

   506 

   507   Two important notions in the nominal logic work are what Pitts calls

   508   \emph{equivariance} and the \emph{equivariance principle}.  These

   509   notions allows us to characterise how permutations act upon compound

   510   statements in HOL by analysing how these statements are constructed.

   511   The notion of equivariance means that an object is invariant under

   512   any permutations. This can be defined as follows:

   513 

   514   \begin{definition}[Equivariance]\label{equivariance}

   515   An object @{text "x"} of permutation type is \emph{equivariant} provided 

   516   for all permutations @{text "\<pi>"}, \mbox{@{term "\<pi> \<bullet> x = x"}} holds.

   517   \end{definition}

   518 

   519   \noindent

   520   In what follows we will primarily be interested in the cases where

   521   @{text x} is a constant, but of course there is no way in

   522   Isabelle/HOL to restrict this definition to just these cases.

   523 

   524   There are a number of equivalent formulations for equivariance.  

   525   For example, assuming @{text f} is a function of permutation 

   526   type @{text "\<alpha> \<Rightarrow> \<beta>"}, then equivariance of @{text f} can also be stated as

   527 

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

   529   \begin{tabular}{@ {}l}

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

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

   532   \end{isabelle} 

   533 

   534   \noindent

   535   We will say this formulation of equivariance is in \emph{fully applied form}.

   536   To see that this formulation implies the definition, we just unfold

   537   the definition of the permutation operation for functions and

   538   simplify with the equation and the cancellation property shown in

   539   \eqref{cancel}. To see the other direction, we use

   540   \eqref{permutefunapp}. Similarly for functions that take more than

   541   one argument. The point to note is that equivariance and equivariance in fully

   542   applied form are always interderivable (for permutation types).

   543 

   544   Both formulations of equivariance have their advantages and

   545   disadvantages: \eqref{altequivariance} is usually more convenient to

   546   establish, since statements in HOL are commonly given in a

   547   form where functions are fully applied. For example we can easily

   548   show that equality is equivariant

   549 

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

   551   \begin{tabular}{@ {}l}

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

   553   \end{tabular}\hfill\numbered{eqeqvt}

   554   \end{isabelle} 

   555 

   556   \noindent

   557   using the permutation operation on booleans and property

   558   \eqref{permuteequ}. 

   559   Lemma~\ref{permutecompose} establishes that the

   560   permutation operation is equivariant. The permutation operation for

   561   lists and products, shown in \eqref{permdefsconstrs}, state that the

   562   constructors for products, @{text "Nil"} and @{text Cons} are

   563   equivariant. Furthermore a simple calculation will show that our

   564   swapping functions are equivariant, that is

   565 

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

   567   \begin{tabular}{@ {}l}

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

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

   570   \end{isabelle} 

   571 

   572   \noindent

   573   for all @{text a}, @{text b} and @{text \<pi>}. Also the booleans

   574   @{const True} and @{const False} are equivariant by the definition

   575   of the permutation operation for booleans. Given this definition, it 

   576   is also easy to see that the boolean operators, like @{text "\<and>"}, 

   577   @{text "\<or>"}, @{text "\<longrightarrow>"} and  @{text "\<not>"} are equivariant:

   578 

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

   580   \begin{tabular}{@ {}lcl}

   581   @{text "\<pi> \<bullet> (A \<and> B) = (\<pi> \<bullet> A) \<and> (\<pi> \<bullet> B)"}\\

   582   @{text "\<pi> \<bullet> (A \<or> B) = (\<pi> \<bullet> A) \<or> (\<pi> \<bullet> B)"}\\

   583   @{text "\<pi> \<bullet> (A \<longrightarrow> B) = (\<pi> \<bullet> A) \<longrightarrow> (\<pi> \<bullet> B)"}\\

   584   @{text "\<pi> \<bullet> (\<not>A) = \<not>(\<pi> \<bullet> A)"}\\

   585   \end{tabular}

   586   \end{isabelle}

   587   

   588   In contrast, the advantage of Definition \ref{equivariance} is that

   589   it allows us to state a general principle how permutations act on

   590   statements in HOL.  For this we will define a rewrite system that

   591   `pushes' a permutation towards the leaves of statements (i.e.~constants

   592   and variables).  Then the permutations disappear in cases where the

   593   constants are equivariant.  To do so, let us first define

   594   \emph{HOL-terms}, which are the building blocks of statements in HOL.

   595   They are given by the grammar

   596 

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

   598   @{text "t ::= c | x | t\<^isub>1 t\<^isub>2 | \<lambda>x. t"}

   599   \hfill\numbered{holterms}

   600   \end{isabelle} 

   601 

   602   \noindent

   603   where @{text c} stands for constants and @{text x} for variables.

   604   We assume HOL-terms are fully typed, but for the sake of better

   605   legibility we leave the typing information implicit.  We also assume

   606   the usual notions for free and bound variables of a HOL-term.

   607   Furthermore, HOL-terms are regarded as equal modulo alpha-, beta-

   608   and eta-equivalence. The equivariance principle can now 

   609   be stated formally as follows:

   610 

   611   \begin{theorem}[Equivariance Principle]\label{eqvtprin}

   612   Suppose a HOL-term @{text t} whose constants are all equivariant. For any 

   613   permutation @{text \<pi>}, let @{text t'} be @{text t} except every 

   614   free variable @{text x} in @{term t} is replaced by @{text "\<pi> \<bullet> x"}, then 

   615   @{text "\<pi> \<bullet> t = t'"}.

   616   \end{theorem}

   617   

   618   \noindent

   619   The significance of this principle is that we can automatically establish

   620   the equivariance of a constant for which equivariance is not yet

   621   known. For this we only have to establish that the definiens of this

   622   constant is a HOL-term whose constants are all equivariant. 

   623   This meshes well with how HOL is designed: except for a few axioms, every constant 

   624   is defined in terms of existing constants. For example an alternative way

   625   to deduce that @{term True} is equivariant is to look at its

   626   definition

   627 

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

   629   @{thm True_def}

   630   \end{isabelle} 

   631 

   632   \noindent

   633   and observing that the only constant in the definiens, namely @{text "="}, is 

   634   equivariant. Similarly, the universal quantifier @{text "\<forall>"} is definied in HOL as 

   635 

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

   637   @{text "\<forall>x. P x \<equiv> "}~@{thm (rhs) All_def[no_vars]}

   638   \end{isabelle} 

   639 

   640   \noindent

   641   The constants in the definiens @{thm (rhs) All_def[no_vars]}, namely @{text "="}

   642   and @{text "True"}, are equivariant (we shown this above). Therefore

   643   the equivariance principle gives us

   644 

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

   646   \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}

   647   @{text "\<pi> \<bullet> (\<forall>x. P x)"} & @{text "\<equiv>"} & @{text "\<pi> \<bullet> (P = (\<lambda>x. True))"}\\  

   648                            & @{text "="} & @{text "(\<pi> \<bullet> P) = (\<lambda>x. True)"}\\  

   649                            & @{text "\<equiv>"} & @{text "\<forall>x. (\<pi> \<bullet> P) x"}

   650   \end{tabular}

   651   \end{isabelle} 

   652 

   653   \noindent

   654   which means the constant @{text "\<forall>"} must be equivariant. From this

   655   we can deduce that the existential quantifier @{text "\<exists>"} is equivariant. 

   656   Its definition in HOL is

   657 

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

   659   @{text "\<exists>x. P x \<equiv> "}~@{thm (rhs) Ex_def[no_vars]}

   660   \end{isabelle} 

   661 

   662   \noindent

   663   where again the HOL-term on the right-hand side only contains equivariant constants 

   664   (namely @{text "\<forall>"} and @{text "\<longrightarrow>"}). Taking both facts together, we can deduce that

   665   the unique existential quantifier @{text "\<exists>!"} is equivariant. Its definition 

   666   is

   667 

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

   669   @{text "\<exists>!x. P x \<equiv> "}~@{thm (rhs) Ex1_def[no_vars]}

   670   \end{isabelle} 

   671 

   672   \noindent

   673   with all constants on the right-hand side being equivariant. With this kind

   674   of reasoning we can build up a database of equivariant constants, which will

   675   be handy for more complex calculations later on. 

   676 

   677   Before we proceed, let us give a justification for the equivariance principle. 

   678   This justification cannot be given directly inside Isabelle/HOL since we cannot

   679   prove any statement about HOL-terms. Instead, we will use a rewrite 

   680   system consisting of a series of equalities 

   681   

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

   683   @{text "\<pi> \<cdot> t  =  ...  =  t'"}

   684   \end{isabelle}

   685   

   686   \noindent 

   687   that establish the equality between @{term "\<pi> \<bullet> t"} and

   688   @{text "t'"}. The idea of the rewrite system is to push the

   689   permutation inside the term @{text t}. We have implemented this as a

   690   conversion tactic on the ML-level of Isabelle/HOL.  In what follows,

   691   we will show that this tactic produces only finitely many equations

   692   and also show that it is correct (in the sense of pushing a permutation

   693   @{text "\<pi>"} inside a term and the only remaining instances of @{text

   694   "\<pi>"} are in front of the term's free variables).  

   695 

   696   The tactic applies four `oriented' equations. 

   697   We will first give a naive version of

   698   our tactic, which however in some corner cases produces incorrect

   699   results or does not terminate.  We then give a modification in order

   700   to obtain the desired properties.

   701   Consider the following for oriented equations

   702   

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

   704   \begin{tabular}{@ {}lr@ {\hspace{3mm}}c@ {\hspace{3mm}}l}

   705   i) & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & \rrh & @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\\

   706   ii) & @{text "\<pi> \<bullet> (\<lambda>x. t)"} & \rrh & @{text "\<lambda>x. \<pi> \<bullet> (t[x :=  (-\<pi>) \<bullet> x])"}\\

   707   iii) & @{term "\<pi> \<bullet> (- \<pi>) \<bullet> x"} & \rrh & @{term "x"}\\

   708   iv) &  @{term "\<pi> \<bullet> c"} & \rrh & 

   709             {\rm @{term "c"}\hspace{6mm}provided @{text c} is equivariant}\\

   710   \end{tabular}\hfill\numbered{rewriteapplam}

   711   \end{isabelle}

   712 

   713   \noindent

   714   These equation are oriented in the sense of being applied in the left-to-right

   715   direction. The first equation we established in \eqref{permutefunapp};

   716   the second follows from the definition of permutations acting on functions

   717   and the fact that HOL-terms are equal modulo beta-equivalence.

   718   The third is a consequence of \eqref{cancel} and the fourth from 

   719   Definition~\ref{equivariance}. Unfortunately, we have to be careful with

   720   the rules {\it i)} and {\it iv}) since they can lead to loops whenever

   721   \mbox{@{text "t\<^isub>1 t\<^isub>2"}} is of the form @{text "((op \<bullet>) \<pi>') t"}.

   722   Recall that we established in Lemma \ref{permutecompose} that the

   723   constant @{text "(op \<bullet>)"} is equivariant and consider the infinite

   724   reduction sequence

   725 

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

   727   \begin{tabular}{@ {}l}

   728   @{text "\<pi> \<bullet> (\<pi>' \<bullet> t)"}

   729   $\;\;\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it iv)}}{\rrh}\;\;$

   730   @{text "(\<pi> \<bullet> \<pi>') \<bullet> (\<pi> \<bullet> t)"}

   731   $\;\;\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it iv)}}{\rrh}\;\;$

   732   @{text "((\<pi> \<bullet> \<pi>') \<bullet> \<pi>) \<bullet> ((\<pi> \<bullet> \<pi>') \<bullet> t)"}~~\ldots%

   733   

   734   \end{tabular}

   735   \end{isabelle}

   736 

   737   \noindent

   738   where the last term is again an instance of rewrite rule {\it i}), but larger.  

   739   To avoid this loop we will apply the rewrite rule

   740   using an `outside to inside' strategy.  This strategy is sufficient

   741   since we are only interested of rewriting terms of the form @{term

   742   "\<pi> \<bullet> t"}, where an outermost permutation needs to pushed inside a term.

   743 

   744   Another problem we have to avoid is that the rules {\it i)} and {\it

   745   iii)} can `overlap'. For this note that the term @{term "\<pi>

   746   \<bullet>(\<lambda>x. x)"} reduces by {\it ii)} to @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet> x"}, to

   747   which we can apply rule {\it iii)} in order to obtain @{term

   748   "\<lambda>x. x"}, as is desired: since there is no free variable in the original

   749   term, the permutation should completely vanish. However, the

   750   subterm @{text "(- \<pi>) \<bullet> x"} is also an application. Consequently,

   751   the term @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet>x"} can also reduce to @{text "\<lambda>x. (- (\<pi>

   752   \<bullet> \<pi>)) \<bullet> (\<pi> \<bullet> x)"} using {\it i)}.  Given our strategy, we cannot

   753   apply rule {\it iii)} anymore in order to eliminate the permutation. 

   754   In contrast, if we start 

   755   with the term @{text "\<pi> \<bullet> ((- \<pi>) \<bullet> x)"} where @{text \<pi>} and @{text

   756   x} are free variables, then we \emph{do} want to apply rule {\it i)}

   757   in order to obtain @{text "(\<pi> \<bullet> (- \<pi>)) \<bullet> (\<pi> \<bullet> x)"}

   758   and not rule {\it iii)}. The latter would eliminate @{text \<pi>}

   759   completely and thus violating our correctness property. The problem is that 

   760   rule {\it iii)} should only apply to

   761   instances where the corresponding variable is to bound; for free variables we want

   762   to use {\it ii)}.  In order to distinguish these cases we have to

   763   maintain the information which variable is bound when inductively

   764   taking a term `apart'. This, unfortunately, does not mesh well with

   765   the way how conversion tactics are implemented in Isabelle/HOL.

   766 

   767   Our remedy is to use a standard trick in HOL: we introduce a

   768   separate definition for terms of the form @{text "(- \<pi>) \<bullet> x"},

   769   namely as

   770 

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

   772   @{term "unpermute \<pi> x \<equiv> (- \<pi>) \<bullet> x"}

   773   \end{isabelle}

   774 

   775   \noindent

   776   The point is that now we can re-formulate the rewrite rules as follows

   777   

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

   779   \begin{tabular}{@ {}lrcl}

   780   i') & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & \rrh & 

   781     @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\hspace{45mm}\mbox{}\\

   782   \multicolumn{4}{r}{\rm provided @{text "t\<^isub>1 t\<^isub>2"} is not of the form @{text "unpermute \<pi> x"}}\smallskip\\

   783   ii') & @{text "\<pi> \<bullet> (\<lambda>x. t)"} & \rrh & @{text "\<lambda>x. \<pi> \<bullet> (t[x := unpermute \<pi> x])"}\\

   784   iii') & @{text "\<pi> \<bullet> (unpermute \<pi> x)"} & \rrh & @{term x}\\

   785   iv') &  @{term "\<pi> \<bullet> c"} & \rrh & @{term "c"}

   786     \hspace{6mm}{\rm provided @{text c} is equivariant}\\

   787   \end{tabular}

   788   \end{isabelle}

   789 

   790   \noindent

   791   where @{text unpermutes} are only generated in case of bound variables.

   792   Clearly none of these rules overlap. Moreover, given our

   793   outside-to-inside strategy, applying them repeatedly must terminate. 

   794 To see this, notice that

   795   the permutation on the right-hand side of the rewrite rules is

   796   always applied to a smaller term, provided we take the measure consisting

   797   of lexicographically ordered pairs whose first component is the size

   798   of a term (counting terms of the form @{text "unpermute \<pi> x"} as

   799   leaves) and the second is the number of occurences of @{text

   800   "unpermute \<pi> x"} and @{text "\<pi> \<bullet> c"}.

   801 

   802   With the rewrite rules of the conversions tactic in place, we can

   803   establish its correctness. The property we are after is that 

   804   for a HOL-term @{text t} whose constants are all equivariant the 

   805   term \mbox{@{text "\<pi> \<bullet> t"}} is equal to @{text "t'"} with @{text "t'"}

   806   being equal to @{text t} except that every free variable @{text x}

   807   in @{text t} is replaced by \mbox{@{text "\<pi> \<bullet> x"}}. Let us call

   808   a variable @{text x} \emph{really free}, if it is free and not occuring

   809   in an @{term unpermute}, such as @{text "unpermute _ x"} and @{text "unpermute x _"}.

   810   We need the following technical notion characterising \emph{@{text "\<pi>"}-proper} HOL-terms

   811 

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

   813   \begin{tabular}{@ {}ll}

   814   $\bullet$ & variables and constants are @{text \<pi>}-proper,\\

   815   $\bullet$ & @{term "unpermute \<pi> x"} is @{text \<pi>}-proper,\\

   816   $\bullet$ & @{term "\<lambda>x. t"} is @{text \<pi>}-proper, if @{text t} is @{text \<pi>}-proper and @{text x} is 

   817   really free in @{text t}, and\\

   818   $\bullet$ & @{term "t\<^isub>1 t\<^isub>2"} is @{text \<pi>}-proper, if @{text "t\<^isub>1"} and @{text "t\<^isub>2"} are 

   819   @{text \<pi>}-proper.

   820   \end{tabular}

   821   \end{isabelle}

   822 

   823   \begin{proof}[Theorem~\ref{eqvtprin}] We establish the property if @{text t} 

   824   is @{text \<pi>}-proper and only contains equivaraint constants, then 

   825   @{text "\<pi> \<bullet> t = t'"} where @{text "t'"} is equal to @{text "t"} except all really

   826   free variables @{text x} are replaced by @{text "\<pi> \<bullet> x"}, and all semi-free variables 

   827   @{text "unpermute \<pi> x"} by @{text "x"}. We establish this property by induction

   828   on the size of HOL-terms, counting terms like @{text "unpermuting \<pi> x"} as leafes,

   829   like variables and constants. The cases for variables, constants and @{text unpermutes}

   830   are routine. In the case of abstractions we have by induction hypothesis that 

   831   @{text "\<pi> \<bullet> (t[x := unpermute \<pi> x]) = t'"} with @{text "t'"} satisfying our

   832   correctness property. This implies that @{text "\<lambda>x. \<pi> \<bullet> (t[x := unpermute \<pi> x]) = \<lambda>x. t'"}

   833   and hence @{text "\<pi> \<bullet> (\<lambda>x. t) = \<lambda>x. t'"} as needed.\hfill\qed  

   834   \end{proof}

   835 

   836   Pitts calls this property \emph{equivariance principle} (book ref ???). 

   837   

   838   Problems with @{text undefined}

   839   

   840   Lines of code

   841 *}

   842 

   843 

   844 section {* Support and Freshness *}

   845 

   846 text {*

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

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

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

   850   but to any type for which a permutation operation is defined 

   851   (like lists, sets, functions and so on). 

   852 

   853   \begin{definition}[Support] \label{support} 

   854   Given @{text x} is of permutation type, then 

   855   

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

   857   \end{definition}

   858 

   859   \noindent

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

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

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

   863   for an @{text x} of permutation type, defined as

   864   

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

   866 

   867   \noindent

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

   869   defined as follows

   870   

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

   872 

   873   \noindent

   874   Using the equivariance principle, it can be easily checked that all three notions

   875   are equivariant. A simple consequence of the definition of support and equivariance 

   876   is that if @{text x} is equivariant then we have 

   877 

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

   879   \begin{tabular}{@ {}l}

   880   @{thm  (concl) supp_fun_eqvt[where f="x", no_vars]}

   881   \end{tabular}\hfill\numbered{suppeqvtfun}

   882   \end{isabelle} 

   883 

   884   \noindent

   885   For function applications we can establish the following two properties.

   886 

   887   \begin{lemma}\label{suppfunapp} Let @{text f} and @{text x} be of permutation type, then

   888   \begin{isabelle}

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

   890   {\it i)} & @{thm[mode=IfThen] fresh_fun_app[no_vars]}\\

   891   {\it ii)} & @{thm supp_fun_app[no_vars]}\\

   892   \end{tabular}

   893   \end{isabelle}

   894   \end{lemma}

   895 

   896   \begin{proof}

   897   For the first property, we know from the assumption that @{term

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

   899   x}"} hold. That means for all, but finitely many @{text b} we have

   900   @{term "(a \<rightleftharpoons> b) \<bullet> f = f"} and @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}. Similarly,

   901   we have to show that for but, but finitely @{text b} the equation

   902   @{term "(a \<rightleftharpoons> b) \<bullet> f x = f x"} holds. The left-hand side of this

   903   equation is equal to @{term "((a \<rightleftharpoons> b) \<bullet> f) ((a \<rightleftharpoons> b) \<bullet> x)"} by

   904   \eqref{permutefunapp}, which we know by the previous two facts for

   905   @{text f} and @{text x} is equal to the right-hand side for all,

   906   but finitely many @{text b}. This establishes the first

   907   property. The second is a simple corollary of {\it i)} by

   908   unfolding the definition of freshness.\qed

   909   \end{proof}

   910 

   911   A striking consequence of the definitions for support and freshness

   912   is that we can prove without knowing anything about the structure of

   913   @{term x} that swapping two fresh atoms, say @{text a} and @{text

   914   b}, leave @{text x} unchanged. For the proof we use the following

   915   lemma about swappings applied to an @{text x}:

   916 

   917   \begin{lemma}\label{swaptriple}

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

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

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

   921   \end{lemma}

   922 

   923   \begin{proof}

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

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

   926   that the permutations

   927 

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

   929   

   930   \noindent

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

   932   property shown in~\eqref{newpermprops}.\qed

   933   \end{proof}

   934 

   935   \begin{theorem}\label{swapfreshfresh}

   936   Let @{text x} be of permutation type.

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

   938   \end{theorem}

   939 

   940   \begin{proof}

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

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

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

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

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

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

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

   948   \end{proof}

   949   

   950   While the abstract properties of support and freshness, particularly 

   951   Theorem~\ref{swapfreshfresh}, are useful for developing Nominal Isabelle, 

   952   one often has to calculate the support of concrete objects.

   953   For booleans, nats, products and lists it is easy to check that

   954 

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

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

   957   @{text "booleans"}: & @{term "supp b = {}"}\\

   958   @{text "nats"}:     & @{term "supp n = {}"}\\

   959   @{text "products"}: & @{thm supp_Pair[no_vars]}\\

   960   @{text "lists:"} & @{thm supp_Nil[no_vars]}\\

   961                    & @{thm supp_Cons[no_vars]}\\

   962   \end{tabular}

   963   \end{isabelle}

   964 

   965   \noindent 

   966   hold.  Establishing the support of atoms and permutations is a bit 

   967   trickier. To do so we will use the following notion about a \emph{supporting set}.

   968   

   969   \begin{definition}[Supporting Set]

   970   A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}

   971   not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.

   972   \end{definition}

   973 

   974   \noindent

   975   The main motivation for this notion is that we can characterise @{text "supp x"} 

   976   as the smallest finite set that supports @{text "x"}. For this we prove:

   977 

   978   \begin{lemma}\label{supports} Let @{text x} be of permutation type.

   979   \begin{isabelle}

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

   981   i)    & @{thm[mode=IfThen] supp_is_subset[no_vars]}\\

   982   ii)   & @{thm[mode=IfThen] supp_supports[no_vars]}\\

   983   iii)  & @{thm (concl) supp_is_least_supports[no_vars]}

   984          provided @{thm (prem 1) supp_is_least_supports[no_vars]},

   985          @{thm (prem 2) supp_is_least_supports[no_vars]}

   986          and @{text "S"} is the least such set, that means formally,

   987          for all @{text "S'"}, if @{term "finite S'"} and 

   988          @{term "S' supports x"} then @{text "S \<subseteq> S'"}.

   989   \end{tabular}

   990   \end{isabelle} 

   991   \end{lemma}

   992 

   993   \begin{proof}

   994   For {\it i)} we derive a contradiction by assuming there is an atom @{text a}

   995   with @{term "a \<in> supp x"} and @{text "a \<notin> S"}. Using the second fact, the 

   996   assumption that @{term "S supports x"} gives us that @{text S} is a superset of 

   997   @{term "{b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"}, which is finite by the assumption of @{text S}

   998   being finite. But this means @{term "a \<notin> supp x"}, contradicting our assumption.

   999   Property {\it ii)} is by a direct application of 

  1000   Theorem~\ref{swapfreshfresh}. For the last property, part {\it i)} proves

  1001   one ``half'' of the claimed equation. The other ``half'' is by property 

  1002   {\it ii)} and the fact that @{term "supp x"} is finite by {\it i)}.\hfill\qed  

  1003   \end{proof}

  1004 

  1005   \noindent

  1006   These are all relatively straightforward proofs adapted from the existing 

  1007   nominal logic work. However for establishing the support of atoms and 

  1008   permutations we found  the following `optimised' variant of {\it iii)} 

  1009   more useful:

  1010 

  1011   \begin{lemma}\label{optimised} Let @{text x} be of permutation type.

  1012   We have that @{thm (concl) finite_supp_unique[no_vars]}

  1013   provided @{thm (prem 1) finite_supp_unique[no_vars]},

  1014   @{thm (prem 2) finite_supp_unique[no_vars]}, and for

  1015   all @{text "a \<in> S"} and all @{text "b \<notin> S"}, with @{text a}

  1016   and @{text b} having the same sort, \mbox{@{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"}}

  1017   \end{lemma}

  1018 

  1019   \begin{proof}

  1020   By Lemma \ref{supports}@{text ".iii)"} we have to show that for every finite

  1021   set @{text S'} that supports @{text x}, \mbox{@{text "S \<subseteq> S'"}} holds. We will

  1022   assume that there is an atom @{text "a"} that is element of @{text S}, but

  1023   not @{text "S'"} and derive a contradiction.  Since both @{text S} and

  1024   @{text S'} are finite, we can by Proposition \ref{choosefresh} obtain an atom

  1025   @{text b}, which has the same sort as @{text "a"} and for which we know

  1026   @{text "b \<notin> S"} and @{text "b \<notin> S'"}. Since we assumed @{text "a \<notin> S'"} and

  1027   we have that @{text "S' supports x"}, we have on one hand @{term "(a \<rightleftharpoons> b) \<bullet> x

  1028   = x"}. On the other hand, the fact @{text "a \<in> S"} and @{text "b \<notin> S"} imply

  1029   @{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"} using the assumed implication. This gives us the

  1030   contradiction.\hfill\qed

  1031   \end{proof}

  1032 

  1033   \noindent

  1034   Using this lemma we only have to show the following three proof-obligations

  1035 

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

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

  1038   i)   & @{term "{c} supports c"}\\

  1039   ii)  & @{term "finite {c}"}\\

  1040   iii) & @{text "\<forall>a \<in> {c} b \<notin> {c}. sort a = sort b \<longrightarrow> (a b) \<bullet> c \<noteq> c"}

  1041   \end{tabular}

  1042   \end{isabelle} 

  1043 

  1044   \noindent

  1045   in order to establish that @{thm supp_atom[where a="c", no_vars]} holds.  In

  1046   Isabelle/HOL these proof-obligations can be discharged by easy

  1047   simplifications. Similar proof-obligations arise for the support of

  1048   permutations, which is

  1049 

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

  1051   \begin{tabular}{@ {}l}

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

  1053   \end{tabular}

  1054   \end{isabelle}

  1055 

  1056   \noindent

  1057   The only proof-obligation that is 

  1058   interesting is the one where we have to show that

  1059 

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

  1061   \begin{tabular}{@ {}l}

  1062   @{text "If \<pi> \<bullet> a \<noteq> a, \<pi> \<bullet> b = b and sort a = sort b, then (a b) \<bullet> \<pi> \<noteq> \<pi>"}.

  1063   \end{tabular}

  1064   \end{isabelle}

  1065 

  1066   \noindent

  1067   For this we observe that 

  1068 

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

  1070   \begin{tabular}{@ {}rcl}

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

  1072   if and only if &

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

  1074   \end{tabular}

  1075   \end{isabelle}

  1076 

  1077   \noindent

  1078   holds by a simple calculation using the group properties of permutations.

  1079   The proof-obligation can then be discharged by analysing the inequality

  1080   between the permutations @{term "(\<pi> \<bullet> a \<rightleftharpoons> b)"} and @{term "(a \<rightleftharpoons> b)"}.

  1081 

  1082   The main point about support is that whenever an object @{text x} has finite

  1083   support, then Proposition~\ref{choosefresh} allows us to choose for @{text x} a 

  1084   fresh atom with arbitrary sort. This is a crucial operation in Nominal

  1085   Isabelle in situations where, for example, a bound variable needs to be

  1086   renamed. To allow such a choice, we only have to assume that 

  1087   @{text "finite (supp x)"} holds. For more convenience we

  1088   can define a type class in Isabelle/HOL corresponding to the 

  1089   property:

  1090   

  1091   \begin{definition}[Finitely Supported Type]

  1092   A type @{text "\<beta>"} is \emph{finitely supported} if @{term "finite (supp x)"}

  1093   holds for all @{text x} of type @{text "\<beta>"}.

  1094   \end{definition}

  1095  

  1096   \noindent

  1097   By the calculations above we can easily establish 

  1098 

  1099   \begin{theorem}\label{finsuptype} 

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

  1101   are fintitely supported, and assuming @{text \<beta>}, @{text "\<beta>\<^isub>1"} and

  1102   @{text "\<beta>\<^isub>2"} are finitely supported types, then @{text "\<beta> list"} and

  1103   @{text "\<beta>\<^isub>1 \<times> \<beta>\<^isub>2"} are finitely supported.

  1104   \end{theorem}

  1105 

  1106   \noindent

  1107   The main benefit of using the finite support property for choosing a

  1108   fresh atom is that the reasoning is `compositional'. To see this,

  1109   assume we have a list of atoms and a method of choosing a fresh atom

  1110   that is not a member in this list---for example the maximum plus

  1111   one.  Then if we enlarge this list \emph{after} the choice, then

  1112   obviously the fresh atom might not be fresh anymore. In contrast, by

  1113   the classical reasoning of Proposition~\ref{choosefresh} we know a

  1114   fresh atom exists for every list of atoms and no matter how we

  1115   extend this list of atoms, we always preserve the property of being

  1116   finitely supported. Consequently the existence of a fresh atom is

  1117   still guarantied by Proposition~\ref{choosefresh}.  Using the method

  1118   of `maximum plus one' we might have to adapt the choice of a fresh

  1119   atom.

  1120 

  1121   Unfortunately, Theorem~\ref{finsuptype} does not work in general for the

  1122   types of sets and functions.  There are functions definable in HOL

  1123   for which the finite support property does not hold.  A simple

  1124   example of a function with infinite support is @{const nat_of} shown

  1125   in \eqref{sortnatof}.  This function's support is the set of

  1126   \emph{all} atoms @{term "UNIV::atom set"}.  To establish this we

  1127   show @{term "\<not> a \<sharp> nat_of"}. This is equivalent to assuming the set

  1128   @{term "{b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"} is finite and deriving a

  1129   contradiction. From the assumption we also know that @{term "{a} \<union>

  1130   {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"} is finite. Then we can use

  1131   Proposition~\ref{choosefresh} to choose an atom @{text c} such that

  1132   @{term "c \<noteq> a"}, @{term "sort_of c = sort_of a"} and @{term "(a \<rightleftharpoons> c)

  1133   \<bullet> nat_of = nat_of"}.  Now we can reason as follows:

  1134