1 (*<*)

     2 theory Paper

     3 imports "../Nominal/Nominal2_Base" 

     4         "../Nominal/Nominal2_Atoms" 

     5         "../Nominal/Nominal2_Eqvt" 

     6         "../Nominal/Atoms" 

     7         "LaTeXsugar"

     8 begin

     9 

    10 notation (latex output)

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

    12   Abs_perm ("_") and

    13   Rep_perm ("_") and

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

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

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

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

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

    19   atom ("|_|") and

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

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

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

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

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

    25   sort_of_ty ("sort'_ty _")

    26 

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

    28 syntax (latex output)

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

    30 *)

    31 

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

    33 hide const sort

    34 

    35 abbreviation

    36   "sort \<equiv> sort_of"

    37 

    38 abbreviation

    39   "sort_ty \<equiv> sort_of_ty"

    40 

    41 (*>*)

    42 

    43 section {* Introduction *}

    44 

    45 text {*

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

    47   prover providing a proving infrastructure for convenient reasoning about

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

    49   algorithm for LF \cite{UrbanCheneyBerghofer08}, 

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

    51   \cite{BengtsonParrow07,BengtsonParow09} and a strong normalisation result for

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

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

    54   \cite{SatoPollack10}.

    55 

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

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

    58   sort-respecting permutation operation defined over a countably infinite

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

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

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

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

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

    64 

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

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

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

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

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

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

    71   implement permutations concretely as list of pairs of atoms. Thus Nominal

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

    73 

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

    75 

    76   \noindent 

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

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

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

    80 

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

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

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

    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 from 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-list 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:} We use a single atom type for representing

   218   atoms of different sorts and use functions for representing

   219   permutations. This drastically reduces the number of type classes to just

   220   two (permutation types and finitely supported types), which we need in order

   221   reason abstractly about properties from the nominal logic work. The novel

   222   technical contribution of this paper is a mechanism for dealing with

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

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

   225   annotations.

   226 *}

   227 

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

   229 

   230 text {*

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

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

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

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

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

   236   a separate type, we implement here atoms to be

   237 *}

   238 

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

   240 

   241 text {*

   242   \noindent

   243   whereby the string argument specifies the sort of the atom.  (We use type

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

   245   as well.)  We have an auxiliary function @{text sort} that is defined as @{thm

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

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

   248   

   249   \begin{proposition}\label{choosefresh}

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

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

   252   \end{proposition}

   253 

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

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

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

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

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

   259   

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

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

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

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

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

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

   266   \end{isabelle}

   267 

   268   \noindent

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

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

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

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

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

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

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

   276 

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

   278   permutations? In the nominal logic work it turned out to be most convenient

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

   280   type of swappings must be

   281 

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

   283 

   284   \noindent

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

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

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

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

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

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

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

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

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

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

   295 

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

   297 

   298   \noindent

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

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

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

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

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

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

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

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

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

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

   309   ill-sorted case:

   310 

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

   312   \begin{tabular}{@ {}rl}

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

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

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

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

   317   \end{isabelle}

   318 

   319   \noindent

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

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

   322   a function in @{typ perm}. 

   323 

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

   325   permutations is that for example the swappings

   326 

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

   328   \begin{tabular}{@ {}l}

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

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

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

   332   \end{isabelle}

   333 

   334   \noindent

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

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

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

   338   they form an (additive) group provided we define

   339 

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

   341   \begin{tabular}{@ {}l}

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

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

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

   345   @{thm diff_def[where x="\<pi>\<^isub>1" and y="\<pi>\<^isub>2"]} 

   346   \end{tabular}

   347   \end{isabelle}

   348 

   349   \noindent

   350   and verify the simple properties

   351 

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

   353   \begin{tabular}{@ {}l}

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

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

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

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

   358   \end{tabular}

   359   \end{isabelle}

   360 

   361   \noindent

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

   363   form a group. The technical importance of this fact is that for groups we can

   364   rely on Isabelle/HOL's rich simplification infrastructure.  This will come in

   365   handy when we have to do calculations with permutations.

   366 

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

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

   369   \eqref{permprops} as just the two equations

   370   

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

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

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

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

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

   376   \end{isabelle} 

   377 

   378   \noindent

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

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

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

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

   383   sort, like in the old approach.

   384 

   385   We call type @{text "\<beta>"} a \emph{permutation type} if the permutation

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

   387   @{text "\<beta>"}.  This notion allows us to establish generic lemmas, which are

   388   applicable to any permutation type.  First, it follows from the laws governing

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

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

   391 

   392   

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

   394   \begin{tabular}{@ {}l}

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

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

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

   398   \end{isabelle} 

   399   

   400   \noindent

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

   402   which in turn implies the property

   403 

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

   405   \begin{tabular}{@ {}l}

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

   407   $\;$if and only if$\;$

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

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

   410   \end{isabelle} 

   411   

   412   \noindent

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

   414 

   415   \begin{isabelle}

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

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

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

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

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

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

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

   423   \end{tabular} &

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

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

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

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

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

   429   \end{tabular}

   430   \end{tabular}

   431   \end{isabelle}

   432 

   433   \noindent

   434   and then establish:

   435 

   436   \begin{theorem}

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

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

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

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

   441   \end{theorem}

   442 

   443   \begin{proof}

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

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

   446   have

   447 

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

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

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

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

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

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

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

   455   \end{tabular}\hfill\qed

   456   \end{isabelle}

   457   \end{proof}

   458 

   459   \noindent

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

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

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

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

   464   permutation type.

   465 

   466   \begin{lemma}\label{permutecompose} 

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

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

   469   \end{lemma}

   470 

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

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

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

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

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

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

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

   478   \end{tabular}\hfill\qed

   479   \end{isabelle}

   480   \end{proof}

   481 

   482 %* }

   483 %

   484 %section { * Equivariance * }

   485 %

   486 %text { *

   487 

   488   One huge advantage of using bijective permutation functions (as opposed to

   489   non-bijective renaming substitutions) is the property of \emph{equivariance}

   490   and the fact that most HOL-functions (this includes constants) whose argument

   491   and result types are permutation types satisfy this property:

   492 

   493   \begin{definition}\label{equivariance}

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

   495   \end{definition}

   496 

   497   \noindent

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

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

   500   can also be stated as 

   501 

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

   503   \begin{tabular}{@ {}l}

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

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

   506   \end{isabelle} 

   507 

   508   \noindent

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

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

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

   512   the fact 

   513   

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

   515   \begin{tabular}{@ {}l}

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

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

   518   \end{isabelle} 

   519 

   520   \noindent

   521   which follows again directly 

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

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

   524 

   525   Both formulations of equivariance have their advantages and disadvantages:

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

   527   can easily show that equality is equivariant

   528 

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

   530   \begin{tabular}{@ {}l}

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

   532   \end{tabular}

   533   \end{isabelle} 

   534 

   535   \noindent

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

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

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

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

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

   541   

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

   543   \begin{tabular}{@ {}l}

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

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

   546   \end{isabelle} 

   547 

   548   \noindent

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

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

   551   terms.

   552 *}

   553 

   554 

   555 section {* Support and Freshness *}

   556 

   557 text {*

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

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

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

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

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

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

   564 

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

   566 

   567   \noindent

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

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

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

   571   for an @{text x}, defined as

   572   

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

   574 

   575   \noindent

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

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

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

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

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

   581 

   582   \begin{lemma}\label{swaptriple}

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

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

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

   586   \end{lemma}

   587 

   588   \begin{proof}

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

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

   591   that the permutations

   592 

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

   594   

   595   \noindent

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

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

   598   \end{proof}

   599 

   600   \begin{theorem}\label{swapfreshfresh}

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

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

   603   \end{theorem}

   604 

   605   \begin{proof}

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

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

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

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

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

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

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

   613   \end{proof}

   614   

   615   \noindent

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

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

   618 

   619   \begin{lemma}\label{half}

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

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

   622   \end{lemma}

   623 

   624   \begin{proof}

   625   \begin{isabelle}

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

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

   628   & \\

   629   @{text "\<Leftrightarrow>"}

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

   631   & by definition\\

   632   @{text "\<Leftrightarrow>"}

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

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

   635   @{text "\<Leftrightarrow>"}

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

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

   638   @{text "\<Leftrightarrow>"}

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

   640   & by \eqref{permuteequ}\\

   641   @{text "\<Leftrightarrow>"}

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

   643   & by definition\\

   644   \end{tabular}

   645   \end{isabelle}\hfill\qed

   646   \end{proof}

   647 

   648   \noindent

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

   650   we can immediately infer equivariance of freshness: 

   651 

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

   653 

   654   \noindent

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

   656   

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

   658   

   659   \noindent

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

   661   the logical connectives are equivariant.

   662 

   663   While the abstract properties of support and freshness, particularly 

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

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

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

   667 

   668   \begin{center}

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

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

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

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

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

   674   \end{tabular} &

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

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

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

   678   \end{tabular}

   679   \end{tabular}

   680   \end{center}

   681 

   682   \noindent

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

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

   685   

   686   \begin{definition}

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

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

   689   \end{definition}

   690 

   691   \noindent

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

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

   694 

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

   696   \begin{isabelle}

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

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

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

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

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

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

   703          and @{text "S"} is the least such set, that means formally:\\[2mm]

   704 

   705         & \multicolumn{1}{c}{for all @{text "S'"}, if @{term "finite S'"} and 

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

   707   \end{tabular}

   708   \end{isabelle} 

   709   \end{lemma}

   710 

   711   \begin{proof}

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

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

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

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

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

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

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

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

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

   721   \end{proof}

   722 

   723   \noindent

   724   These are all relatively straightforward proofs adapted from the existing 

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

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

   727   more useful:

   728 

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

   730   Then @{thm (concl) finite_supp_unique[no_vars]}

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

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

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

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

   735   \end{lemma}

   736 

   737   \begin{proof}

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

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

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

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

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

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

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

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

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

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

   748   contradiction.\hfill\qed

   749   \end{proof}

   750 

   751   \noindent

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

   753 

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

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

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

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

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

   759   \end{tabular}

   760   \end{isabelle} 

   761 

   762   \noindent

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

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

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

   766   permutations, which is

   767 

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

   769   \begin{tabular}{@ {}l}

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

   771   \end{tabular}

   772   \end{isabelle}

   773 

   774   \noindent

   775   The only proof-obligation that is 

   776   interesting is the one where we have to show that

   777 

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

   779   \begin{tabular}{@ {}l}

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

   781   \end{tabular}

   782   \end{isabelle}

   783 

   784   \noindent

   785   For this we observe that 

   786 

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

   788   \begin{tabular}{@ {}rcl}

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

   790   if and only if &

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

   792   \end{tabular}

   793   \end{isabelle}

   794 

   795   \noindent

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

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

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

   799 

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

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

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

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

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

   805   of the form

   806 

   807   @{text [display,indent=10] "finite (supp x)"}

   808 

   809   \noindent

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

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

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

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

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

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

   816   is finitely supported.

   817 

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

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

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

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

   822   

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

   824 

   825   \noindent

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

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

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

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

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

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

   832   Now we can reason as follows:

   833 

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

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

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

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

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

   839   \end{tabular}\hfill\qed

   840   \end{isabelle}

   841   

   842 

   843   \noindent

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

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

   846   assumption @{term "c \<noteq> a"} about how we chose @{text c}. Similar examples for 

   847   constructions that have infinite support are given in~\cite{Cheney06}.

   848 *}

   849 

   850 section {* Concrete Atom Types *}

   851 

   852 text {*

   853 

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

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

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

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

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

   859   atom type makes this possible.  

   860 

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

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

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

   864   means subgoals involving sorts must be discharged explicitly within proof

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

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

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

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

   869   Isabelle/HOL as:

   870 *}

   871 

   872           lemma

   873 	    fixes a b :: "atom"

   874 	    assumes asm: "sort a = sort b"

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

   876           using asm by simp

   877 

   878 text {*

   879   \noindent

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

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

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

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

   884 

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

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

   887   "''name''"}.

   888 

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

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

   891   \end{isabelle}

   892 

   893   \noindent

   894   This command automatically generates injective functions that map from the

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

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

   897   functions as follows:

   898 

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

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

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

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

   903   \end{tabular}

   904   \end{isabelle}

   905 

   906   \noindent

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

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

   909   @{typ name} is a permutation type.

   910 

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

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

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

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

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

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

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

   918   must all have the same sort.

   919 

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

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

   922   i) & if @{thm (lhs) atom_eq_iff [no_vars]} then @{thm (rhs) atom_eq_iff [no_vars]}\\

   923   ii) & @{thm atom_eqvt[where p="\<pi>", no_vars]}\\

   924   iii) & @{thm sort_of_atom_eq [no_vars]}

   925   \end{tabular}\hfill\numbered{atomprops}

   926   \end{isabelle}

   927 

   928   \noindent

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

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

   931   type.

   932 

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

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

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

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

   937 

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

   939 

   940   \noindent

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

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

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

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

   945   simplification rule:

   946 

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

   948 

   949   \noindent

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

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

   952 *}

   953 

   954           lemma

   955 	    fixes a b :: "name"

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

   957 	  by simp

   958 

   959 text {*

   960   \noindent

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

   962 

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

   964   can define a new one simply by issuing the command 

   965 

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

   967   \begin{tabular}{@ {}l}

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

   969   \end{tabular}

   970   \end{isabelle}

   971 

   972   \noindent

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

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

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

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

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

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

   979   theories that separately declare different atom types can be merged

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

   981   place.

   982 *}

   983 

   984 

   985 section {* Multi-Sorted Concrete Atoms *}

   986 

   987 (*<*)

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

   989 (*>*)

   990 

   991 text {*

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

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

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

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

   996   additional information, for example typing constraints.

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

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

   999   represented by concrete atoms.

  1000   

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

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

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

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

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

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

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

  1008 

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

  1010   \begin{tabular}{@ {}l}

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

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

  1013   \end{isabelle}

  1014 

  1015   \noindent

  1016   both variables and binders include typing information indicated by @{text

  1017   \<alpha>} and @{text \<beta>}. In this setting, we treat @{text

  1018   "x\<^isub>\<alpha>"} and @{text "x\<^isub>\<beta>"} as distinct variables

  1019   (assuming @{term "\<alpha>\<noteq>\<beta>"}) so that the variable @{text

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

  1021   "x\<^isub>\<beta>"}.

  1022 

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

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

  1025 

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

  1027   \begin{tabular}{@ {}l}

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

  1029   \end{tabular}

  1030   \end{isabelle}

  1031 

  1032   \noindent

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

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

  1035 

  1036   @{text [display,indent=10] "((x, \<alpha>), (x, \<beta>))"}

  1037 

  1038   \noindent

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

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

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

  1042   corresponding binder. 

  1043 

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

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

  1046   Remember we defined atoms as the datatype:

  1047 *}

  1048 

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

  1050   

  1051 text {*

  1052   \noindent

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

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

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

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

  1057   argument parametric as follows:

  1058 *}

  1059 

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

  1061 

  1062 text {*

  1063   \noindent

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

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

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

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

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

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

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

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

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

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

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

  1075 *}

  1076 

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

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

  1079 

  1080 text {*

  1081   \noindent

  1082   With this definition,

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

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

  1085 

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

  1087   \begin{tabular}{@ {}l}

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

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

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

  1091   \end{isabelle}

  1092 

  1093   \noindent

  1094   which can easily be shown to be injective.  

  1095   

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

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

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

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

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

  1101 

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

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

  1104   \end{isabelle}

  1105 

  1106   \noindent

  1107   This command gives us again injective representation and abstraction

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

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

  1110 

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

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

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

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

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

  1116 

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

  1118 

  1119   \noindent

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

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

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

  1123   @{text "var"}.

  1124   This fact is slightly unfortunate since this

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

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

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

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

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

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

  1131 

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

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

  1134   lemma

  1135 *}