1 (*<*)

     2 theory Paper

     3 imports "../Nominal/Nominal2_Base" 

     4         "../Nominal/Atoms" 

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

     6 begin

     7 

     8 notation (latex output)

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

    10   Abs_perm ("_") and

    11   Rep_perm ("_") and

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

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

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

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

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

    17   atom ("|_|") and

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

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

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

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

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

    23   sort_of_ty ("sort'_ty _")

    24 

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

    26 syntax (latex output)

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

    28 *)

    29 

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

    31 hide_const sort

    32 

    33 abbreviation

    34   "sort \<equiv> sort_of"

    35 

    36 abbreviation

    37   "sort_ty \<equiv> sort_of_ty"

    38 

    39 (*>*)

    40 

    41 section {* Introduction *}

    42 

    43 text {*

    44   Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem

    45   prover providing a proving infrastructure for convenient reasoning about

    46   programming languages. It has been used to formalise an equivalence checking

    47   algorithm for LF \cite{UrbanCheneyBerghofer08}, 

    48   Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency

    49   \cite{BengtsonParrow07} and a strong normalisation result for

    50   cut-elimination in classical logic \cite{UrbanZhu08}. It has also been used

    51   by Pollack for formalisations in the locally-nameless approach to binding

    52   \cite{SatoPollack10}.

    53 

    54   At its core Nominal Isabelle is based on the nominal logic work of Pitts et

    55   al \cite{GabbayPitts02,Pitts03}.  The most basic notion in this work is a

    56   sort-respecting permutation operation defined over a countably infinite

    57   collection of sorted atoms. The atoms are used for representing variables

    58   that might be bound. Multiple sorts are necessary for being

    59   able to represent different kinds of variables. For example, in the language

    60   Mini-ML there are bound term variables and bound type variables; each kind

    61   needs to be represented by a different sort of atoms.

    62 

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

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

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

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

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

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

    69   implement permutations concretely as lists of pairs of atoms. Thus Nominal

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

    71 

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

    73 

    74   \noindent 

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

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

    77   the permutation operation is defined over the length of lists as follows

    78 

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

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

    81   @{text "[] \<bullet> c"} & @{text "="} & @{text c}\\

    82   \end{tabular}\hspace{12mm}

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

    84   @{text "(a b)::\<pi> \<bullet> c"} & @{text "="} & 

    85      $\begin{cases} @{text a} & \textrm{if}~@{text "\<pi> \<bullet> c = b"}\\ 

    86                     @{text b} & \textrm{if}~@{text "\<pi> \<bullet> c = a"}\\

    87                     @{text "\<pi> \<bullet> c"} & \textrm{otherwise}\end{cases}$

    88   \end{tabular}\hfill\numbered{atomperm}

    89   \end{isabelle}

    90 

    91   \noindent

    92   where we write @{text "(a b)"} for a swapping of atoms @{text "a"} and

    93   @{text "b"}. For atoms of different type, the permutation operation

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

    95 

    96   With the list representation of permutations it is impossible to state an

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

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

    99   the basic operations on permutations are already defined in the list library:

   100   composition of two permutations (written @{text "_ @ _"}) is just list append,

   101   and inversion of a permutation (written @{text "_\<^sup>-\<^sup>1"}) is just

   102   list reversal. A disadvantage is that permutations do not have unique

   103   representations as lists; we had to explicitly identify permutations according

   104   to the relation

   105   

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

   107   \begin{tabular}{@ {}l}

   108   @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2  \<equiv>  \<forall>a. \<pi>\<^isub>1 \<bullet> a = \<pi>\<^isub>2 \<bullet> a"}

   109   \end{tabular}\hfill\numbered{permequ}

   110   \end{isabelle}

   111 

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

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

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

   115   \emph{permutation properties}:

   116 

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

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

   119   i) & @{text "[] \<bullet> x = x"}\\

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

   121   iii) & if @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2"} then @{text "\<pi>\<^isub>1 \<bullet> x = \<pi>\<^isub>2 \<bullet> x"}

   122   \end{tabular}\hfill\numbered{permprops}

   123   \end{isabelle}

   124 

   125   \noindent

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

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

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

   129   properties for each type.

   130 

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

   132   support operations with only a single type parameter and the permutation

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

   134   contain two! To work around this obstacle, Nominal Isabelle 

   135   required the user to

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

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

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

   139   whereby in these type classes the permutation operation is restricted to

   140 

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

   142 

   143   \noindent

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

   145   atom types given by the user). 

   146 

   147   While the representation of permutations-as-lists solved the

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

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

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

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

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

   153   need to generalise induction hypotheses by quantifying over permutations, we

   154   have to build cumbersome quantifications like

   155 

   156   @{text [display,indent=10] "\<forall>\<pi>\<^isub>1 \<dots> \<forall>\<pi>\<^isub>n. \<dots>"}

   157 

   158   \noindent

   159   where the @{text "\<pi>\<^isub>i"} are of type @{text "(\<alpha>\<^isub>i \<times> \<alpha>\<^isub>i) list"}. 

   160   The reason is that the permutation operation behaves differently for 

   161   every @{text "\<alpha>\<^isub>i"}. Third, although the notion of support

   162 

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

   164 

   165   \noindent

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

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

   168   is again that support can behave differently for each @{text

   169   "\<alpha>\<^isub>i"}. This problem is annoying, because if we need to know in

   170   a statement that an object, say @{text "x"}, is finitely supported we end up

   171   with having to state premises of the form

   172 

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

   174   \begin{tabular}{@ {}l}

   175   @{text "finite ((supp x) :: \<alpha>\<^isub>1 set) , \<dots>, finite ((supp x) :: \<alpha>\<^isub>n set)"}

   176   \end{tabular}\hfill\numbered{fssequence}

   177   \end{isabelle}

   178 

   179   \noindent

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

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

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

   183   all types can be shown to be finitely supported.

   184 

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

   186   from another permutation property

   187 

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

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

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

   191   \end{tabular}

   192   \end{isabelle}

   193 

   194   \noindent

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

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

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

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

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

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

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

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

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

   204   slightly different type classes for this permutation property.

   205   

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

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

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

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

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

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

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

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

   214   simple formalisation of the nominal logic work.\smallskip

   215 

   216   \noindent

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

   218   atoms of different sorts and representing permutations as functions are not

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

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

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

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

   223   The novel

   224   technical contribution is a mechanism for dealing with

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

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

   227   annotations.

   228 *}

   229 

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

   231 

   232 text {*

   233   In the nominal logic work of Pitts, binders and bound variables are

   234   represented by \emph{atoms}.  As stated above, we need to have different

   235   \emph{sorts} of atoms to be able to bind different kinds of variables.  A

   236   basic requirement is that there must be a countably infinite number of atoms

   237   of each sort.  Unlike in our earlier work, where we identified each sort with

   238   a separate type, we implement here atoms to be

   239 *}

   240 

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

   242 

   243 text {*

   244   \noindent

   245   whereby the string argument specifies the sort of the atom.\footnote{A similar 

   246   design choice was made by Gunter et al \cite{GunterOsbornPopescu09} 

   247   for their variables.}  (The use type

   248   \emph{string} is merely for convenience; any countably infinite type would work

   249   as well.) 

   250   We have an auxiliary function @{text sort} that is defined as @{thm

   251   sort_of.simps[no_vars]}, and we clearly have for every finite set @{text X} of

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

   253   

   254   \begin{proposition}\label{choosefresh}

   255   @{text "If finite X then there exists an atom a such that

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

   257   \end{proposition}

   258 

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

   260   "atom => atom"} that @{text "i)"} are bijective; @{text "ii)"} are the

   261   identity on all atoms, except a finite number of them; and @{text "iii)"} map

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

   263   for a function @{text \<pi>} as follows:

   264   

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

   266   i)~~~@{term "bij \<pi>"}\hspace{5mm}

   267   ii)~~~@{term "finite {a. \<pi> a \<noteq> a}"}\hspace{5mm}

   268   iii)~~~@{term "\<forall>a. sort (\<pi> a) = sort a"}\hfill\numbered{permtype}

   269   \end{isabelle}

   270 

   271   \noindent

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

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

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

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

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

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

   278   @{text "i"}-@{text "iii"}. 

   279 

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

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

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

   283   type of swappings must be

   284 

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

   286 

   287   \noindent

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

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

   290   sorts.  In earlier versions of Nominal Isabelle, we avoided this problem by

   291   using different types for different sorts; the type system prevented users

   292   from stating ill-sorted swappings.  Here, however, definitions such 

   293   as\footnote{To increase legibility, we omit here and in what follows the

   294   @{term Rep_perm} and @{term "Abs_perm"} wrappers that are needed in our

   295   implementation since we defined permutation not to be the full function space,

   296   but only those functions of type @{typ perm} satisfying properties @{text

   297   i}-@{text "iii"}.}

   298 

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

   300 

   301   \noindent

   302   do not work in general, because the type system does not prevent @{text a}

   303   and @{text b} from having different sorts---in which case the function would

   304   violate property @{text iii}.  We could make the definition of swappings

   305   partial by adding the precondition @{term "sort a = sort b"},

   306   which would mean that in case @{text a} and @{text b} have different sorts,

   307   the value of @{text "(a b)"} is unspecified.  However, this looked like a

   308   cumbersome solution, since sort-related side conditions would be required

   309   everywhere, even to unfold the definition.  It turned out to be more

   310   convenient to actually allow the user to state ``ill-sorted'' swappings but

   311   limit their ``damage'' by defaulting to the identity permutation in the

   312   ill-sorted case:

   313 

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

   315   \begin{tabular}{@ {}rl}

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

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

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

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

   320   \end{isabelle}

   321 

   322   \noindent

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

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

   325   a function in @{typ perm}. 

   326 

   327   One advantage of using functions instead of lists as a representation for

   328   permutations is that for example the swappings

   329 

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

   331   \begin{tabular}{@ {}l}

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

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

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

   335   \end{isabelle}

   336 

   337   \noindent

   338   are \emph{equal}.  We do not have to use the equivalence relation shown

   339   in~\eqref{permequ} to identify them, as we would if they had been represented

   340   as lists of pairs.  Another advantage of the function representation is that

   341   they form a (non-commutative) group, provided we define

   342 

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

   344   \begin{tabular}{@ {}l}

   345   @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm}

   346   @{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{4mm}

   347   @{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{4mm}

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

   349   \end{tabular}

   350   \end{isabelle}

   351 

   352   \noindent

   353   and verify the simple properties

   354 

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

   356   \begin{tabular}{@ {}l}

   357   @{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]} \hspace{3mm}

   358   @{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{3mm}

   359   @{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{3mm}

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

   361   \end{tabular}

   362   \end{isabelle}

   363 

   364   \noindent

   365   Again this is in contrast to the list-of-pairs representation which does not

   366   form a group.  The technical importance of this fact is that we can rely on

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

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

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

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

   371   composition of permutations is not commutative in general---@{text

   372   "\<pi>\<^sub>1 + \<pi>\<^sub>2 \<noteq> \<pi>\<^sub>2 + \<pi>\<^sub>1"}.  But since the point of this paper is to implement the

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

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

   375 

   376   By formalising permutations abstractly as functions, and using a single type

   377   for all atoms, we can now restate the \emph{permutation properties} from

   378   \eqref{permprops} as just the two equations

   379   

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

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

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

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

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

   385   \end{isabelle} 

   386 

   387   \noindent

   388   in which the permutation operations are of type @{text "perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} and so

   389   have only a single type parameter.  Consequently, these properties are

   390   compatible with the one-parameter restriction of Isabelle/HOL's type classes.

   391   There is no need to introduce a separate type class instantiated for each

   392   sort, like in the old approach.

   393 

   394   The next notion allows us to establish generic lemmas involving the

   395   permutation operation.

   396 

   397   \begin{definition}

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

   399   properties in \eqref{newpermprops} are satisfied for every @{text "x"} of type

   400   @{text "\<beta>"}.  

   401   \end{definition}

   402 

   403   \noindent

   404   First, it follows from the laws governing

   405   groups that a permutation and its inverse cancel each other.  That is, for any

   406   @{text "x"} of a permutation type:

   407 

   408   

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

   410   \begin{tabular}{@ {}l}

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

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

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

   414   \end{isabelle} 

   415   

   416   \noindent

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

   418   which in turn implies the property

   419 

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

   421   \begin{tabular}{@ {}l}

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

   423   $\;$if and only if$\;$

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

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

   426   \end{isabelle} 

   427   

   428   \noindent

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

   430 

   431   \begin{isabelle}

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

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

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

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

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

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

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

   439   \end{tabular} &

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

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

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

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

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

   445   \end{tabular}

   446   \end{tabular}

   447   \end{isabelle}

   448 

   449   \noindent

   450   and then establish:

   451 

   452   \begin{theorem}

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

   454   then so are @{text "atom"}, @{text "\<beta>\<^isub>1 \<Rightarrow> \<beta>\<^isub>2"}, 

   455   @{text perm}, @{term "\<beta> set"}, @{term "\<beta> list"}, @{term "\<beta>\<^isub>1 \<times> \<beta>\<^isub>2"},

   456   @{text bool} and @{text "nat"}.

   457   \end{theorem}

   458 

   459   \begin{proof}

   460   All statements are by unfolding the definitions of the permutation operations and simple 

   461   calculations involving addition and minus. With permutations for example we 

   462   have

   463 

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

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

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

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

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

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

   470   \end{tabular}\hfill\qed

   471   \end{isabelle}

   472   \end{proof}

   473 

   474   \noindent

   475   The main point is that the above reasoning blends smoothly with the reasoning

   476   infrastructure of Isabelle/HOL; no custom ML-code is necessary and a single

   477   type class suffices. We can also show once and for all that the following

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

   479   permutation type.

   480 

   481   \begin{lemma}\label{permutecompose} 

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

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

   484   \end{lemma}

   485 

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

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

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

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

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

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

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

   493   \end{tabular}\hfill\qed

   494   \end{isabelle}

   495   \end{proof}

   496 

   497 %* }

   498 %

   499 %section { * Equivariance * }

   500 %

   501 %text { *

   502 

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

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

   505   properties is a major advantage of bijective permutations over traditional

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

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

   508   functions and constants.

   509 

   510   \begin{definition}\label{equivariance}

   511   A function @{text f} is \emph{equivariant} if @{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}.

   512   \end{definition}

   513 

   514   \noindent

   515   There are a number of equivalent formulations for the equivariance property. 

   516   For example, assuming @{text f} is of type @{text "\<alpha> \<Rightarrow> \<beta>"}, then equivariance 

   517   can also be stated as 

   518 

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

   520   \begin{tabular}{@ {}l}

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

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

   523   \end{isabelle} 

   524 

   525   \noindent

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

   527   definition of the permutation operation for functions and simplify with the equation

   528   and the cancellation property shown in \eqref{cancel}. To see the other direction, we use 

   529   the fact 

   530   

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

   532   \begin{tabular}{@ {}l}

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

   534   \end{tabular}\hfill\numbered{permutefunapp}

   535   \end{isabelle} 

   536 

   537   \noindent

   538   which follows again directly 

   539   from the definition of the permutation operation for functions and the cancellation 

   540   property. Similarly for functions with more than one argument. 

   541 

   542   Both formulations of equivariance have their advantages and disadvantages:

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

   544   can easily show that equality is equivariant

   545 

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

   547   \begin{tabular}{@ {}l}

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

   549   \end{tabular}

   550   \end{isabelle} 

   551 

   552   \noindent

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

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

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

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

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

   558   

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

   560   \begin{tabular}{@ {}l}

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

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

   563   \end{isabelle} 

   564 

   565   \noindent

   566   for all @{text a}, @{text b} and @{text \<pi>}.  These equivariance properties

   567   are tremendously helpful later on when we have to push permutations inside

   568   terms.

   569 *}

   570 

   571 

   572 section {* Support and Freshness *}

   573 

   574 text {*

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

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

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

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

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

   580   the type of @{text x}, namely:

   581 

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

   583 

   584   \noindent

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

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

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

   588   for an @{text x}, defined as

   589   

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

   591 

   592   \noindent

   593   A striking consequence of these definitions is that we can prove

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

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

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

   597   about swappings applied to an @{text x}:

   598 

   599   \begin{lemma}\label{swaptriple}

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

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

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

   603   \end{lemma}

   604 

   605   \begin{proof}

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

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

   608   that the permutations

   609 

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

   611   

   612   \noindent

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

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

   615   \end{proof}

   616 

   617   \begin{theorem}\label{swapfreshfresh}

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

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

   620   \end{theorem}

   621 

   622   \begin{proof}

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

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

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

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

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

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

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

   630   \end{proof}

   631   

   632   \noindent

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

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

   635 

   636   \begin{lemma}\label{half}

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

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

   639   \end{lemma}

   640 

   641   \begin{proof}

   642   \begin{isabelle}

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

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

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

   646   @{text "\<Leftrightarrow>"}

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

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

   649   @{text "\<Leftrightarrow>"}

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

   651   & by \eqref{permutecompose} and \eqref{swapeqvt}\\

   652   @{text "\<Leftrightarrow>"}

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

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

   655   & by \eqref{permuteequ}\\

   656   \end{tabular}

   657   \end{isabelle}\hfill\qed

   658   \end{proof}

   659 

   660   \noindent

   661   Together with the definition of the permutation operation on booleans,

   662   we can immediately infer equivariance of freshness: 

   663 

   664   @{thm [display,indent=10] fresh_eqvt[where p="\<pi>",no_vars]}

   665 

   666   \noindent

   667   Now equivariance of @{text "supp"}, namely

   668   

   669   @{thm [display,indent=10] supp_eqvt[where p="\<pi>",no_vars]}

   670   

   671   \noindent

   672   is by noting that @{thm supp_conv_fresh[no_vars]} and that freshness and 

   673   the logical connectives are equivariant.

   674 

   675   While the abstract properties of support and freshness, particularly 

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

   677   one often has to calculate the support of some concrete object. This is 

   678   straightforward for example for booleans, nats, products and lists:

   679 

   680   \begin{center}

   681   \begin{tabular}{@ {}c@ {\hspace{2mm}}c@ {}}

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

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

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

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

   686   \end{tabular} &

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

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

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

   690   \end{tabular}

   691   \end{tabular}

   692   \end{center}

   693 

   694   \noindent

   695   But establishing the support of atoms and permutations in our setup here is a bit 

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

   697   

   698   \begin{definition}

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

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

   701   \end{definition}

   702 

   703   \noindent

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

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

   706 

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

   708   \begin{isabelle}

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

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

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

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

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

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

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

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

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

   718   \end{tabular}

   719   \end{isabelle} 

   720   \end{lemma}

   721 

   722   \begin{proof}

   723   For @{text "i)"} we derive a contradiction by assuming there is an atom @{text a}

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

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

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

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

   728   Property @{text "ii)"} is by a direct application of 

   729   Theorem~\ref{swapfreshfresh}. For the last property, part @{text "i)"} proves

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

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

   732   \end{proof}

   733 

   734   \noindent

   735   These are all relatively straightforward proofs adapted from the existing 

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

   737   permutations we found  the following ``optimised'' variant of @{text "iii)"} 

   738   more useful:

   739 

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

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

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

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

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

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

   746   \end{lemma}

   747 

   748   \begin{proof}

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

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

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

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

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

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

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

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

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

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

   759   contradiction.\hfill\qed

   760   \end{proof}

   761 

   762   \noindent

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

   764 

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

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

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

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

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

   770   \end{tabular}

   771   \end{isabelle} 

   772 

   773   \noindent

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

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

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

   777   permutations, which is

   778 

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

   780   \begin{tabular}{@ {}l}

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

   782   \end{tabular}

   783   \end{isabelle}

   784 

   785   \noindent

   786   The only proof-obligation that is 

   787   interesting is the one where we have to show that

   788 

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

   790   \begin{tabular}{@ {}l}

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

   792   \end{tabular}

   793   \end{isabelle}

   794 

   795   \noindent

   796   For this we observe that 

   797 

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

   799   \begin{tabular}{@ {}rcl}

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

   801   if and only if &

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

   803   \end{tabular}

   804   \end{isabelle}

   805 

   806   \noindent

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

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

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

   810 

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

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

   813   fresh atom with arbitrary sort. This is an important operation in Nominal

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

   815   renamed. To allow such a choice, we only have to assume \emph{one} premise

   816   of the form @{text "finite (supp x)"}

   817   for each @{text x}. Compare that with the sequence of premises in our earlier

   818   version of Nominal Isabelle (see~\eqref{fssequence}). For more convenience we

   819   can define a type class for types where every element has finite support, and

   820   prove that the types @{term "atom"}, @{term "perm"}, lists, products and

   821   booleans are instances of this type class. Then \emph{no} premise is needed,

   822   as the type system of Isabelle/HOL can figure out automatically when an object

   823   is finitely supported.

   824 

   825   Unfortunately, this does not work for sets or Isabelle/HOL's function type.

   826   There are functions and sets definable in Isabelle/HOL for which the finite

   827   support property does not hold.  A simple example of a function with

   828   infinite support is the function that returns the natural number of an atom

   829   

   830   @{text [display, indent=10] "nat_of (Atom s i) \<equiv> i"}

   831 

   832   \noindent

   833   This function's support is the set of \emph{all} atoms. To establish this we show @{term "\<not> a \<sharp> nat_of"}. 

   834   This is equivalent to assuming the set @{term "{b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"} is finite

   835   and deriving a contradiction. From the assumption we also know that 

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

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

   838   @{term "c \<noteq> a"}, @{term "sort_of c = sort_of a"} and @{term "(a \<rightleftharpoons> c) \<bullet> nat_of = nat_of"}.

   839   Now we can reason as follows:

   840 

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

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

   843   @{text "nat_of a"} & @{text "="} & @{text "(a \<rightleftharpoons> c) \<bullet> (nat_of a)"} & by def.~of permutations on nats\\

   844   & @{text "="} & @{term "((a \<rightleftharpoons> c) \<bullet> nat_of) ((a \<rightleftharpoons> c) \<bullet> a)"} & by \eqref{permutefunapp}\\

   845   & @{text "="} & @{term "nat_of c"} & by assumptions on @{text c}\\

   846   \end{tabular}

   847   \end{isabelle}

   848   

   849 

   850   \noindent

   851   But this means we have that @{term "nat_of a = nat_of c"} and @{term "sort_of a = sort_of c"}.

   852   This implies that atoms @{term a} and @{term c} must be equal, which clashes with our

   853   assumption @{term "c \<noteq> a"} about how we chose @{text c}. 

   854   Cheney \cite{Cheney06} gives similar examples for constructions that have infinite support.

   855 *}

   856 

   857 section {* Concrete Atom Types *}

   858 

   859 text {*

   860 

   861   So far, we have presented a system that uses only a single multi-sorted atom

   862   type.  This design gives us the flexibility to define operations and prove

   863   theorems that are generic with respect to atom sorts.  For example, as

   864   illustrated above the @{term supp} function returns a set that includes the

   865   free atoms of \emph{all} sorts together; the flexibility offered by the new

   866   atom type makes this possible.  

   867 

   868   However, the single multi-sorted atom type does not make an ideal interface

   869   for end-users of Nominal Isabelle.  If sorts are not distinguished by

   870   Isabelle's type system, users must reason about atom sorts manually.  That

   871   means subgoals involving sorts must be discharged explicitly within proof

   872   scripts, instead of being inferred by Isabelle/HOL's type checker.  In other

   873   cases, lemmas might require additional side conditions about sorts to be true.

   874   For example, swapping @{text a} and @{text b} in the pair \mbox{@{term "(a,

   875   b)"}} will only produce the expected result if we state the lemma in

   876   Isabelle/HOL as:

   877 *}

   878 

   879           lemma

   880 	    fixes a b :: "atom"

   881 	    assumes asm: "sort a = sort b"

   882 	    shows "(a \<rightleftharpoons> b) \<bullet> (a, b) = (b, a)" 

   883           using asm by simp

   884 

   885 text {*

   886   \noindent

   887   Fortunately, it is possible to regain most of the type-checking automation

   888   that is lost by moving to a single atom type.  We accomplish this by defining

   889   \emph{subtypes} of the generic atom type that only include atoms of a single

   890   specific sort.  We call such subtypes \emph{concrete atom types}.

   891 

   892   The following Isabelle/HOL command defines a concrete atom type called

   893   \emph{name}, which consists of atoms whose sort equals the string @{term

   894   "''name''"}.

   895 

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

   897   \isacommand{typedef}\ \ @{typ name} = @{term "{a. sort\<iota> a = ''name''}"}

   898   \end{isabelle}

   899 

   900   \noindent

   901   This command automatically generates injective functions that map from the

   902   concrete atom type into the generic atom type and back, called

   903   representation and abstraction functions, respectively. We will write these

   904   functions as follows:

   905 

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

   907   \begin{tabular}{@ {}l@ {\hspace{10mm}}l}

   908   @{text "\<lfloor>_\<rfloor> :: name \<Rightarrow> atom"} & 

   909   @{text "\<lceil>_\<rceil> :: atom \<Rightarrow> name"}

   910   \end{tabular}

   911   \end{isabelle}

   912 

   913   \noindent

   914   With the definition @{thm permute_name_def [where p="\<pi>", THEN

   915   eq_reflection, no_vars]}, it is straightforward to verify that the type 

   916   @{typ name} is a permutation type.

   917 

   918   In order to reason uniformly about arbitrary concrete atom types, we define a

   919   type class that characterises type @{typ name} and other similarly-defined

   920   types.  The definition of the concrete atom type class is as follows: First,

   921   every concrete atom type must be a permutation type.  In addition, the class

   922   defines an overloaded function that maps from the concrete type into the

   923   generic atom type, which we will write @{text "|_|"}.  For each class

   924   instance, this function must be injective and equivariant, and its outputs

   925   must all have the same sort, that is

   926 

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

   928   i)   \hspace{1mm}if @{thm (lhs) atom_eq_iff [no_vars]} then @{thm (rhs) atom_eq_iff [no_vars]}\hspace{4mm}

   929   ii)  \hspace{1mm}@{thm atom_eqvt[where p="\<pi>", no_vars]}\hspace{4mm}

   930   iii) \hspace{1mm}@{thm sort_of_atom_eq [no_vars]}

   931   \hfill\numbered{atomprops}

   932   \end{isabelle}

   933 

   934   \noindent

   935   With the definition @{thm atom_name_def [THEN eq_reflection, no_vars]} we can

   936   show that @{typ name} satisfies all the above requirements of a concrete atom

   937   type.

   938 

   939   The whole point of defining the concrete atom type class was to let users

   940   avoid explicit reasoning about sorts.  This benefit is realised by defining a

   941   special swapping operation of type @{text "\<alpha> \<Rightarrow> \<alpha>

   942   \<Rightarrow> perm"}, where @{text "\<alpha>"} is a concrete atom type:

   943 

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

   945 

   946   \noindent

   947   As a consequence of its type, the @{text "\<leftrightarrow>"}-swapping

   948   operation works just like the generic swapping operation, but it does not

   949   require any sort-checking side conditions---the sort-correctness is ensured by

   950   the types!  For @{text "\<leftrightarrow>"} we can establish the following

   951   simplification rule:

   952 

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

   954 

   955   \noindent

   956   If we now want to swap the \emph{concrete} atoms @{text a} and @{text b}

   957   in the pair @{term "(a, b)"} we can establish the lemma as follows:

   958 *}

   959 

   960           lemma

   961 	    fixes a b :: "name"

   962 	    shows "(a \<leftrightarrow> b) \<bullet> (a, b) = (b, a)" 

   963 	  by simp

   964 

   965 text {*

   966   \noindent

   967   There is no need to state an explicit premise involving sorts.

   968 

   969   We can automate the process of creating concrete atom types, so that users 

   970   can define a new one simply by issuing the command 

   971 

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

   973   \begin{tabular}{@ {}l}

   974   \isacommand{atom\_decl}~~@{text "name"}

   975   \end{tabular}

   976   \end{isabelle}

   977 

   978   \noindent

   979   This command can be implemented using less than 100 lines of custom ML-code.

   980   In comparison, the old version of Nominal Isabelle included more than 1000

   981   lines of ML-code for creating concrete atom types, and for defining various

   982   type classes and instantiating generic lemmas for them.  In addition to

   983   simplifying the ML-code, the setup here also offers user-visible improvements:

   984   Now concrete atoms can be declared at any point of a formalisation, and

   985   theories that separately declare different atom types can be merged

   986   together---it is no longer required to collect all atom declarations in one

   987   place.

   988 *}

   989 

   990 

   991 section {* Multi-Sorted Concrete Atoms *}

   992 

   993 (*<*)

   994 datatype ty = TVar string | Fun ty ty ("_ \<rightarrow> _") 

   995 (*>*)

   996 

   997 text {*

   998   The formalisation presented so far allows us to streamline proofs and reduce

   999   the amount of custom ML-code in the existing implementation of Nominal

  1000   Isabelle. In this section we describe a mechanism that extends the

  1001   capabilities of Nominal Isabelle. This mechanism is about variables with 

  1002   additional information, for example typing constraints.

  1003   While we leave a detailed treatment of binders and binding of variables for a 

  1004   later paper, we will have a look here at how such variables can be 

  1005   represented by concrete atoms.

  1006   

  1007   In the previous section we considered concrete atoms that can be used in

  1008   simple binders like \emph{@{text "\<lambda>x. x"}}.  Such concrete atoms do

  1009   not carry any information beyond their identities---comparing for equality

  1010   is really the only way to analyse ordinary concrete atoms.

  1011   However, in ``Church-style'' lambda-terms \cite{Church40} and in the terms

  1012   underlying HOL-systems \cite{PittsHOL4} binders and bound variables have a

  1013   more complicated structure. For example in the ``Church-style'' lambda-term

  1014 

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

  1016   \begin{tabular}{@ {}l}

  1017   @{text "\<lambda>x\<^isub>\<alpha>. x\<^isub>\<alpha> x\<^isub>\<beta>"}

  1018   \end{tabular}\hfill\numbered{church}

  1019   \end{isabelle}

  1020 

  1021   \noindent

  1022   both variables and binders include typing information indicated by @{text \<alpha>}

  1023   and @{text \<beta>}. In this setting, we treat @{text "x\<^isub>\<alpha>"} and @{text

  1024   "x\<^isub>\<beta>"} as distinct variables (assuming @{term "\<alpha>\<noteq>\<beta>"}) so that the

  1025   variable @{text "x\<^isub>\<alpha>"} is bound by the lambda-abstraction, but not

  1026   @{text "x\<^isub>\<beta>"}.

  1027 

  1028   To illustrate how we can deal with this phenomenon, let us represent object

  1029   types like @{text \<alpha>} and @{text \<beta>} by the datatype

  1030 

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

  1032   \begin{tabular}{@ {}l}

  1033   \isacommand{datatype}~~@{text "ty = TVar string | ty \<rightarrow> ty"}

  1034   \end{tabular}

  1035   \end{isabelle}

  1036 

  1037   \noindent

  1038   If we attempt to encode a variable naively as a pair of a @{text name} and a @{text ty}, we have the 

  1039   problem that a swapping, say @{term "(x \<leftrightarrow> y)"}, applied to the pair @{text "((x, \<alpha>), (x, \<beta>))"}

  1040   will always permute \emph{both} occurrences of @{text x}, even if the types

  1041   @{text "\<alpha>"} and @{text "\<beta>"} are different. This is unwanted, because it will

  1042   eventually mean that both occurrences of @{text x} will become bound by a

  1043   corresponding binder. 

  1044 

  1045   Another attempt might be to define variables as an instance of the concrete

  1046   atom type class, where a @{text ty} is somehow encoded within each variable.

  1047   Remember we defined atoms as the datatype:

  1048 *}

  1049 

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

  1051   

  1052 text {*

  1053   \noindent

  1054   Considering our method of defining concrete atom types, the usage of a string

  1055   for the sort of atoms seems a natural choice.  However, none of the results so

  1056   far depend on this choice and we are free to change it.

  1057   One possibility is to encode types or any other information by making the sort

  1058   argument parametric as follows:

  1059 *}

  1060 

  1061           datatype  'a \<iota>atom\<iota>\<iota>\<iota> = \<iota>Atom\<iota>\<iota> 'a nat

  1062 

  1063 text {*

  1064   \noindent

  1065   The problem with this possibility is that we are then back in the old

  1066   situation where our permutation operation is parametric in two types and

  1067   this would require to work around Isabelle/HOL's restriction on type

  1068   classes. Fortunately, encoding the types in a separate parameter is not

  1069   necessary for what we want to achieve, as we only have to know when two

  1070   types are equal or not. The solution is to use a different sort for each

  1071   object type.  Then we can use the fact that permutations respect \emph{sorts} to

  1072   ensure that permutations also respect \emph{object types}.  In order to do

  1073   this, we must define an injective function @{text "sort_ty"} mapping from

  1074   object types to sorts.  For defining functions like @{text "sort_ty"}, it is

  1075   more convenient to use a tree datatype for sorts. Therefore we define

  1076 *}

  1077 

  1078           datatype  sort = Sort string "(sort list)"

  1079           datatype  atom\<iota>\<iota>\<iota>\<iota> = Atom\<iota>\<iota>\<iota>\<iota> sort nat

  1080 

  1081 text {*

  1082   \noindent

  1083   With this definition,

  1084   the sorts we considered so far can be encoded just as \mbox{@{text "Sort s []"}}.

  1085   The point, however, is that we can now define the function @{text sort_ty} simply as

  1086 

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

  1088   \begin{tabular}{@ {}l}

  1089   @{text "sort_ty (TVar s) = Sort ''TVar'' [Sort s []]"}\\

  1090   @{text "sort_ty (\<tau>\<^isub>1 \<rightarrow> \<tau>\<^isub>2) = Sort ''Fun''  [sort_ty \<tau>\<^isub>1, sort_ty \<tau>\<^isub>2]"}

  1091   \end{tabular}\hfill\numbered{sortty}

  1092   \end{isabelle}

  1093 

  1094   \noindent

  1095   which can easily be shown to be injective.  

  1096   

  1097   Having settled on what the sorts should be for ``Church-like'' atoms, we have to

  1098   give a subtype definition for concrete atoms. Previously we identified a subtype consisting 

  1099   of atoms of only one specified sort. This must be generalised to all sorts the

  1100   function @{text "sort_ty"} might produce, i.e.~the

  1101   range of @{text "sort_ty"}. Therefore we define

  1102 

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

  1104   \isacommand{typedef}\ \ @{text var} = @{term "{a. sort a : range sort_ty}"}

  1105   \end{isabelle}

  1106 

  1107   \noindent

  1108   This command gives us again injective representation and abstraction

  1109   functions. We will write them also as \mbox{@{text "\<lfloor>_\<rfloor> :: var \<Rightarrow> atom"}} and

  1110   @{text "\<lceil>_\<rceil> :: atom \<Rightarrow> var"}, respectively. 

  1111 

  1112   We can define the permutation operation for @{text var} as @{thm

  1113   permute_var_def[where p="\<pi>", THEN eq_reflection, no_vars]} and the

  1114   injective function to type @{typ atom} as @{thm atom_var_def[THEN

  1115   eq_reflection, no_vars]}. Finally, we can define a constructor function that

  1116   makes a @{text var} from a variable name and an object type:

  1117 

  1118   @{thm [display,indent=10] Var_def[where t="\<alpha>", THEN eq_reflection, no_vars]}

  1119 

  1120   \noindent

  1121   With these definitions we can verify all the properties for concrete atom

  1122   types except Property \ref{atomprops}@{text ".iii)"}, which requires every

  1123   atom to have the same sort.  This last property is clearly not true for type

  1124   @{text "var"}.

  1125   This fact is slightly unfortunate since this

  1126   property allowed us to use the type-checker in order to shield the user from

  1127   all sort-constraints.  But this failure is expected here, because we cannot

  1128   burden the type-system of Isabelle/HOL with the task of deciding when two

  1129   object types are equal.  This means we sometimes need to explicitly state sort

  1130   constraints or explicitly discharge them, but as we will see in the lemma

  1131   below this seems a natural price to pay in these circumstances.

  1132 

  1133   To sum up this section, the encoding of type-information into atoms allows us 

  1134   to form the swapping @{term "(Var x \<alpha> \<leftrightarrow> Var y \<alpha>)"} and to prove the following