1 (*<*)

     2 theory Paper

     3 imports "../Nominal-General/Nominal2_Base" 

     4         "../Nominal-General/Nominal2_Atoms" 

     5         "../Nominal-General/Nominal2_Eqvt" 

     6         "../Nominal-General/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} 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 lists 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 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:} Our use of a single atom type for representing

   218   atoms of different sorts and of functions for representing

   219   permutations is not novel, but drastically reduces the number of type classes to just

   220   two (permutation types and finitely supported types) that 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.\footnote{A similar 

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

   245   for their variables.}  (The use type

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

   247   as well.) 

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

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

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

   251   

   252   \begin{proposition}\label{choosefresh}

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

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

   255   \end{proposition}

   256 

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

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

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

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

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

   262   

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

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

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

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

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

   268   \end{tabular}\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 an (additive 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 diff_def[where x="\<pi>\<^isub>1" and y="\<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 for groups we

   367   can rely on Isabelle/HOL's rich simplification infrastructure.  This will

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

   369   note that in this case Isabelle/HOL neglects well-entrenched mathematical

   370   terminology that associates with an additive group a commutative

   371   operation. Obviously, permutations are not commutative in general, because @{text

   372   "p + q \<noteq> q + p"}. However, it is quite difficult to work around this

   373   idiosyncrasy of Isabelle/HOL, unless we develop our own algebraic hierarchy

   374   and infrastructure. But since the point of this paper is to implement the

   375   nominal theory as smoothly as possible in Isabelle/HOL, we will follow its

   376   characterisation of additive groups.

   377 

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

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

   380   \eqref{permprops} as just the two equations

   381   

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

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

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

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

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

   387   \end{isabelle} 

   388 

   389   \noindent

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

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

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

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

   394   sort, like in the old approach.

   395 

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

   397   permutation operation.

   398 

   399   \begin{definition}

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

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

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

   403   \end{definition}

   404 

   405   \noindent

   406   First, it follows from the laws governing

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

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

   409 

   410   

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

   412   \begin{tabular}{@ {}l}

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

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

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

   416   \end{isabelle} 

   417   

   418   \noindent

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

   420   which in turn implies the property

   421 

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

   423   \begin{tabular}{@ {}l}

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

   425   $\;$if and only if$\;$

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

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

   428   \end{isabelle} 

   429   

   430   \noindent

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

   432 

   433   \begin{isabelle}

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

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

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

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

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

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

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

   441   \end{tabular} &

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

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

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

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

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

   447   \end{tabular}

   448   \end{tabular}

   449   \end{isabelle}

   450 

   451   \noindent

   452   and then establish:

   453 

   454   \begin{theorem}

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

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

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

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

   459   \end{theorem}

   460 

   461   \begin{proof}

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

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

   464   have

   465 

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

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

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

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

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

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

   472   \end{tabular}\hfill\qed

   473   \end{isabelle}

   474   \end{proof}

   475 

   476   \noindent

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

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

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

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

   481   permutation type.

   482 

   483   \begin{lemma}\label{permutecompose} 

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

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

   486   \end{lemma}

   487 

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

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

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

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

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

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

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

   495   \end{tabular}\hfill\qed

   496   \end{isabelle}

   497   \end{proof}

   498 

   499 *}

   500 

   501 section {* Equivariance *}

   502 

   503 text {*

   504 

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

   506   non-bijective renaming substitutions employed in traditional works syntax) is 

   507   the property of \emph{equivariance}

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

   509   and result types are permutation types satisfy this property:

   510 

   511   \begin{definition}\label{equivariance}

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

   513   \end{definition}

   514 

   515   \noindent

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

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

   518   can also be stated as 

   519 

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

   521   \begin{tabular}{@ {}l}

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

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

   524   \end{isabelle} 

   525 

   526   \noindent

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

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

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

   530   the fact 

   531   

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

   533   \begin{tabular}{@ {}l}

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

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

   536   \end{isabelle} 

   537 

   538   \noindent

   539   which follows again directly 

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

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

   542 

   543   Both formulations of equivariance have their advantages and disadvantages:

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

   545   can easily show that equality is equivariant

   546 

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

   548   \begin{tabular}{@ {}l}

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

   550   \end{tabular}

   551   \end{isabelle} 

   552 

   553   \noindent

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

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

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

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

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

   559   

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

   561   \begin{tabular}{@ {}l}

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

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

   564   \end{isabelle} 

   565 

   566   \noindent

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

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

   569   terms.

   570 *}

   571 

   572 

   573 section {* Support and Freshness *}

   574 

   575 text {*

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

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

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

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

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

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

   582 

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

   584 

   585   \noindent

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

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

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

   589   for an @{text x}, defined as

   590   

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

   592 

   593   \noindent

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

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

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

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

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

   599 

   600   \begin{lemma}\label{swaptriple}

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

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

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

   604   \end{lemma}

   605 

   606   \begin{proof}

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

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

   609   that the permutations

   610 

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

   612   

   613   \noindent

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

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

   616   \end{proof}

   617 

   618   \begin{theorem}\label{swapfreshfresh}

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

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

   621   \end{theorem}

   622 

   623   \begin{proof}

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

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

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

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

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

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

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

   631   \end{proof}

   632   

   633   \noindent

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

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

   636 

   637   \begin{lemma}\label{half}

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

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

   640   \end{lemma}

   641 

   642   \begin{proof}

   643   \begin{isabelle}

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

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

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

   647   @{text "\<Leftrightarrow>"}

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

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

   650   @{text "\<Leftrightarrow>"}

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

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

   653   @{text "\<Leftrightarrow>"}

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

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

   656   & by \eqref{permuteequ}\\

   657   \end{tabular}

   658   \end{isabelle}\hfill\qed

   659   \end{proof}

   660 

   661   \noindent

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

   663   we can immediately infer equivariance of freshness: 

   664 

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

   666 

   667   \noindent

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

   669   

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

   671   

   672   \noindent

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

   674   the logical connectives are equivariant.

   675 

   676   While the abstract properties of support and freshness, particularly 

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

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

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

   680 

   681   \begin{center}

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

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

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

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

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

   687   \end{tabular} &

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

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

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

   691   \end{tabular}

   692   \end{tabular}

   693   \end{center}

   694 

   695   \noindent

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

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

   698   

   699   \begin{definition}

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

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

   702   \end{definition}

   703 

   704   \noindent

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

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

   707 

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

   709   \begin{isabelle}

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

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

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

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

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

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

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

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

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

   719   \end{tabular}

   720   \end{isabelle} 

   721   \end{lemma}

   722 

   723   \begin{proof}

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

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

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

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

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

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

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

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

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

   733   \end{proof}

   734 

   735   \noindent

   736   These are all relatively straightforward proofs adapted from the existing 

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

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

   739   more useful:

   740 

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

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

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

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

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

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

   747   \end{lemma}

   748 

   749   \begin{proof}

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

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

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

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

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

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

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

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

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

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

   760   contradiction.\hfill\qed

   761   \end{proof}

   762 

   763   \noindent

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

   765 

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

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

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

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

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

   771   \end{tabular}

   772   \end{isabelle} 

   773 

   774   \noindent

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

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

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

   778   permutations, which is

   779 

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

   781   \begin{tabular}{@ {}l}

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

   783   \end{tabular}

   784   \end{isabelle}

   785 

   786   \noindent

   787   The only proof-obligation that is 

   788   interesting is the one where we have to show that

   789 

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

   791   \begin{tabular}{@ {}l}

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

   793   \end{tabular}

   794   \end{isabelle}

   795 

   796   \noindent

   797   For this we observe that 

   798 

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

   800   \begin{tabular}{@ {}rcl}

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

   802   if and only if &

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

   804   \end{tabular}

   805   \end{isabelle}

   806 

   807   \noindent

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

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

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

   811 

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

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

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

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

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

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

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

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

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

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

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

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

   824   is finitely supported.

   825 

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

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

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

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

   830   

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

   832 

   833   \noindent

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

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

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

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

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

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

   840   Now we can reason as follows:

   841 

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

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

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

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

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

   847   \end{tabular}

   848   \end{isabelle}

   849   

   850 

   851   \noindent

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

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

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

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

   856 *}

   857 

   858 section {* Induction Principles *}

   859 

   860 

   861 

   862 

   863 section {* Concrete Atom Types *}

   864 

   865 text {*

   866 

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

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

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

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

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

   872   atom type makes this possible.  

   873 

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

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

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

   877   means subgoals involving sorts must be discharged explicitly within proof

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

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

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

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

   882   Isabelle/HOL as:

   883 *}

   884 

   885           lemma

   886 	    fixes a b :: "atom"

   887 	    assumes asm: "sort a = sort b"

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

   889           using asm by simp

   890 

   891 text {*

   892   \noindent

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

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

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

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

   897 

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

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

   900   "''name''"}.

   901 

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

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

   904   \end{isabelle}

   905 

   906   \noindent

   907   This command automatically generates injective functions that map from the

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

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

   910   functions as follows:

   911 

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

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

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

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

   916   \end{tabular}

   917   \end{isabelle}

   918 

   919   \noindent

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

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

   922   @{typ name} is a permutation type.

   923 

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

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

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

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

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

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

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

   931   must all have the same sort, that is

   932 

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

   934   \begin{tabular}{r@ {\hspace{3mm}}l}

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

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

   937   iii) @{thm sort_of_atom_eq [no_vars]}

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

   939   \end{isabelle}

   940 

   941   \noindent

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

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

   944   type.

   945 

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

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

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

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

   950 

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

   952 

   953   \noindent

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

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

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

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

   958   simplification rule:

   959 

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

   961 

   962   \noindent

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

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

   965 *}

   966 

   967           lemma

   968 	    fixes a b :: "name"

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

   970 	  by simp

   971 

   972 text {*

   973   \noindent

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

   975 

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

   977   can define a new one simply by issuing the command 

   978 

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

   980   \begin{tabular}{@ {}l}

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

   982   \end{tabular}

   983   \end{isabelle}

   984 

   985   \noindent

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

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

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

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

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

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

   992   theories that separately declare different atom types can be merged

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

   994   place.

   995 *}

   996 

   997 

   998 section {* Multi-Sorted Concrete Atoms *}

   999 

  1000 (*<*)

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

  1002 (*>*)

  1003 

  1004 text {*

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

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

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

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

  1009   additional information, for example typing constraints.

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

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

  1012   represented by concrete atoms.

  1013   

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

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

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

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

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

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

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

  1021 

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

  1023   \begin{tabular}{@ {}l}

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

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

  1026   \end{isabelle}

  1027 

  1028   \noindent

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

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

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

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

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

  1034 

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

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

  1037 

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

  1039   \begin{tabular}{@ {}l}

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

  1041   \end{tabular}

  1042   \end{isabelle}

  1043 

  1044   \noindent

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

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

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

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

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

  1050   corresponding binder. 

  1051 

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

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

  1054   Remember we defined atoms as the datatype:

  1055 *}

  1056 

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

  1058   

  1059 text {*

  1060   \noindent

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

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

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

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

  1065   argument parametric as follows:

  1066 *}

  1067 

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

  1069 

  1070 text {*

  1071   \noindent

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

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

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

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

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

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

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

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

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

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

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

  1083 *}

  1084 

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

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

  1087 

  1088 text {*

  1089   \noindent

  1090   With this definition,

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

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

  1093 

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

  1095   \begin{tabular}{@ {}l}

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

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

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

  1099   \end{isabelle}

  1100 

  1101   \noindent

  1102   which can easily be shown to be injective.  

  1103   

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

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

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

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

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

  1109 

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

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

  1112   \end{isabelle}

  1113 

  1114   \noindent

  1115   This command gives us again injective representation and abstraction

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

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

  1118 

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

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

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

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

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

  1124 

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

  1126 

  1127   \noindent

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

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

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

  1131   @{text "var"}.

  1132   This fact is slightly unfortunate since this

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

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

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