(*<*)+ −
theory Paper+ −
imports "../Nominal-General/Nominal2_Base" + −
"../Nominal-General/Nominal2_Eqvt" + −
"../Nominal-General/Atoms" + −
"LaTeXsugar"+ −
begin+ −
+ −
notation (latex output)+ −
sort_of ("sort _" [1000] 100) and+ −
Abs_perm ("_") and+ −
Rep_perm ("_") and+ −
swap ("'(_ _')" [1000, 1000] 1000) and+ −
fresh ("_ # _" [51, 51] 50) and+ −
Cons ("_::_" [78,77] 73) and+ −
supp ("supp _" [78] 73) and+ −
uminus ("-_" [78] 73) and+ −
atom ("|_|") and+ −
If ("if _ then _ else _" 10) and+ −
Rep_name ("\<lfloor>_\<rfloor>") and+ −
Abs_name ("\<lceil>_\<rceil>") and+ −
Rep_var ("\<lfloor>_\<rfloor>") and+ −
Abs_var ("\<lceil>_\<rceil>") and+ −
sort_of_ty ("sort'_ty _")+ −
+ −
(* BH: uncomment if you really prefer the dot notation+ −
syntax (latex output)+ −
"_Collect" :: "pttrn => bool => 'a set" ("(1{_ . _})")+ −
*)+ −
+ −
(* sort is used in Lists for sorting *)+ −
hide_const sort+ −
+ −
abbreviation+ −
"sort \<equiv> sort_of"+ −
+ −
abbreviation+ −
"sort_ty \<equiv> sort_of_ty"+ −
+ −
(*>*)+ −
+ −
section {* Introduction *}+ −
+ −
text {*+ −
Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem+ −
prover providing a proving infrastructure for convenient reasoning about+ −
programming languages. It has been used to formalise an equivalence checking+ −
algorithm for LF \cite{UrbanCheneyBerghofer08}, + −
Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency+ −
\cite{BengtsonParrow07} and a strong normalisation result for+ −
cut-elimination in classical logic \cite{UrbanZhu08}. It has also been used+ −
by Pollack for formalisations in the locally-nameless approach to binding+ −
\cite{SatoPollack10}.+ −
+ −
At its core Nominal Isabelle is based on the nominal logic work of Pitts et+ −
al \cite{GabbayPitts02,Pitts03}. The most basic notion in this work is a+ −
sort-respecting permutation operation defined over a countably infinite+ −
collection of sorted atoms. The atoms are used for representing variables+ −
that might be bound. Multiple sorts are necessary for being+ −
able to represent different kinds of variables. For example, in the language+ −
Mini-ML there are bound term variables and bound type variables; each kind+ −
needs to be represented by a different sort of atoms.+ −
+ −
Unfortunately, the type system of Isabelle/HOL is not a good fit for the way+ −
atoms and sorts are used in the original formulation of the nominal logic work.+ −
Therefore it was decided in earlier versions of Nominal Isabelle to use a+ −
separate type for each sort of atoms and let the type system enforce the+ −
sort-respecting property of permutations. Inspired by the work on nominal+ −
unification \cite{UrbanPittsGabbay04}, it seemed best at the time to also+ −
implement permutations concretely as lists of pairs of atoms. Thus Nominal+ −
Isabelle used the two-place permutation operation with the generic type+ −
+ −
@{text [display,indent=10] "_ \<bullet> _ :: (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}+ −
+ −
\noindent + −
where @{text "\<alpha>"} stands for the type of atoms and @{text "\<beta>"} for the type+ −
of the objects on which the permutation acts. For atoms of type @{text "\<alpha>"} + −
the permutation operation is defined over the length of lists as follows+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}+ −
@{text "[] \<bullet> c"} & @{text "="} & @{text c}\\+ −
\end{tabular}\hspace{12mm}+ −
\begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}+ −
@{text "(a b)::\<pi> \<bullet> c"} & @{text "="} & + −
$\begin{cases} @{text a} & \textrm{if}~@{text "\<pi> \<bullet> c = b"}\\ + −
@{text b} & \textrm{if}~@{text "\<pi> \<bullet> c = a"}\\+ −
@{text "\<pi> \<bullet> c"} & \textrm{otherwise}\end{cases}$+ −
\end{tabular}\hfill\numbered{atomperm}+ −
\end{isabelle}+ −
+ −
\noindent+ −
where we write @{text "(a b)"} for a swapping of atoms @{text "a"} and+ −
@{text "b"}. For atoms of different type, the permutation operation+ −
is defined as @{text "\<pi> \<bullet> c \<equiv> c"}.+ −
+ −
With the list representation of permutations it is impossible to state an+ −
``ill-sorted'' permutation, since the type system excludes lists containing+ −
atoms of different type. Another advantage of the list representation is that+ −
the basic operations on permutations are already defined in the list library:+ −
composition of two permutations (written @{text "_ @ _"}) is just list append,+ −
and inversion of a permutation (written @{text "_\<^sup>-\<^sup>1"}) is just+ −
list reversal. A disadvantage is that permutations do not have unique+ −
representations as lists; we had to explicitly identify permutations according+ −
to the relation+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2 \<equiv> \<forall>a. \<pi>\<^isub>1 \<bullet> a = \<pi>\<^isub>2 \<bullet> a"}+ −
\end{tabular}\hfill\numbered{permequ}+ −
\end{isabelle}+ −
+ −
When lifting the permutation operation to other types, for example sets,+ −
functions and so on, we needed to ensure that every definition is+ −
well-behaved in the sense that it satisfies the following three + −
\emph{permutation properties}:+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}+ −
i) & @{text "[] \<bullet> x = x"}\\+ −
ii) & @{text "(\<pi>\<^isub>1 @ \<pi>\<^isub>2) \<bullet> x = \<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x)"}\\+ −
iii) & if @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2"} then @{text "\<pi>\<^isub>1 \<bullet> x = \<pi>\<^isub>2 \<bullet> x"}+ −
\end{tabular}\hfill\numbered{permprops}+ −
\end{isabelle}+ −
+ −
\noindent+ −
From these properties we were able to derive most facts about permutations, and + −
the type classes of Isabelle/HOL allowed us to reason abstractly about these+ −
three properties, and then let the type system automatically enforce these+ −
properties for each type.+ −
+ −
The major problem with Isabelle/HOL's type classes, however, is that they+ −
support operations with only a single type parameter and the permutation+ −
operations @{text "_ \<bullet> _"} used above in the permutation properties+ −
contain two! To work around this obstacle, Nominal Isabelle + −
required the user to+ −
declare up-front the collection of \emph{all} atom types, say @{text+ −
"\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}. From this collection it used custom ML-code to+ −
generate @{text n} type classes corresponding to the permutation properties,+ −
whereby in these type classes the permutation operation is restricted to+ −
+ −
@{text [display,indent=10] "_ \<bullet> _ :: (\<alpha>\<^isub>i \<times> \<alpha>\<^isub>i) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}+ −
+ −
\noindent+ −
This operation has only a single type parameter @{text "\<beta>"} (the @{text "\<alpha>\<^isub>i"} are the+ −
atom types given by the user). + −
+ −
While the representation of permutations-as-lists solved the+ −
``sort-respecting'' requirement and the declaration of all atom types+ −
up-front solved the problem with Isabelle/HOL's type classes, this setup+ −
caused several problems for formalising the nominal logic work: First,+ −
Nominal Isabelle had to generate @{text "n\<^sup>2"} definitions for the+ −
permutation operation over @{text "n"} types of atoms. Second, whenever we+ −
need to generalise induction hypotheses by quantifying over permutations, we+ −
have to build cumbersome quantifications like+ −
+ −
@{text [display,indent=10] "\<forall>\<pi>\<^isub>1 \<dots> \<forall>\<pi>\<^isub>n. \<dots>"}+ −
+ −
\noindent+ −
where the @{text "\<pi>\<^isub>i"} are of type @{text "(\<alpha>\<^isub>i \<times> \<alpha>\<^isub>i) list"}. + −
The reason is that the permutation operation behaves differently for + −
every @{text "\<alpha>\<^isub>i"}. Third, although the notion of support+ −
+ −
@{text [display,indent=10] "supp _ :: \<beta> \<Rightarrow> \<alpha> set"}+ −
+ −
\noindent+ −
which we will define later, has a generic type @{text "\<alpha> set"}, it cannot be+ −
used to express the support of an object over \emph{all} atoms. The reason+ −
is again that support can behave differently for each @{text+ −
"\<alpha>\<^isub>i"}. This problem is annoying, because if we need to know in+ −
a statement that an object, say @{text "x"}, is finitely supported we end up+ −
with having to state premises of the form+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{text "finite ((supp x) :: \<alpha>\<^isub>1 set) , \<dots>, finite ((supp x) :: \<alpha>\<^isub>n set)"}+ −
\end{tabular}\hfill\numbered{fssequence}+ −
\end{isabelle}+ −
+ −
\noindent+ −
Sometimes we can avoid such premises completely, if @{text x} is a member of a+ −
\emph{finitely supported type}. However, keeping track of finitely supported+ −
types requires another @{text n} type classes, and for technical reasons not+ −
all types can be shown to be finitely supported.+ −
+ −
The real pain of having a separate type for each atom sort arises, however, + −
from another permutation property+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}+ −
iv) & @{text "\<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x) = (\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
where permutation @{text "\<pi>\<^isub>1"} has type @{text "(\<alpha> \<times> \<alpha>) list"},+ −
@{text "\<pi>\<^isub>2"} type @{text "(\<alpha>' \<times> \<alpha>') list"} and @{text x} type @{text+ −
"\<beta>"}. This property is needed in order to derive facts about how+ −
permutations of different types interact, which is not covered by the+ −
permutation properties @{text "i"}-@{text "iii"} shown in+ −
\eqref{permprops}. The problem is that this property involves three type+ −
parameters. In order to use again Isabelle/HOL's type class mechanism with+ −
only permitting a single type parameter, we have to instantiate the atom+ −
types. Consequently we end up with an additional @{text "n\<^sup>2"}+ −
slightly different type classes for this permutation property.+ −
+ −
While the problems and pain can be almost completely hidden from the user in+ −
the existing implementation of Nominal Isabelle, the work is \emph{not}+ −
pretty. It requires a large amount of custom ML-code and also forces the+ −
user to declare up-front all atom-types that are ever going to be used in a+ −
formalisation. In this paper we set out to solve the problems with multiple+ −
type parameters in the permutation operation, and in this way can dispense+ −
with the large amounts of custom ML-code for generating multiple variants+ −
for some basic definitions. The result is that we can implement a pleasingly+ −
simple formalisation of the nominal logic work.\smallskip+ −
+ −
\noindent+ −
{\bf Contributions of the paper:} Using a single atom type to represent+ −
atoms of different sorts and representing permutations as functions are not+ −
new ideas. The main contribution of this paper is to show an example of how+ −
to make better theorem proving tools by choosing the right level of+ −
abstraction for the underlying theory---our design choices take advantage of+ −
Isabelle's type system, type classes, and reasoning infrastructure.+ −
The novel+ −
technical contribution is a mechanism for dealing with+ −
``Church-style'' lambda-terms \cite{Church40} and HOL-based languages+ −
\cite{PittsHOL4} where variables and variable binding depend on type+ −
annotations.+ −
*}+ −
+ −
section {* Sorted Atoms and Sort-Respecting Permutations *}+ −
+ −
text {*+ −
In the nominal logic work of Pitts, binders and bound variables are+ −
represented by \emph{atoms}. As stated above, we need to have different+ −
\emph{sorts} of atoms to be able to bind different kinds of variables. A+ −
basic requirement is that there must be a countably infinite number of atoms+ −
of each sort. Unlike in our earlier work, where we identified each sort with+ −
a separate type, we implement here atoms to be+ −
*}+ −
+ −
datatype atom\<iota> = Atom\<iota> string nat+ −
+ −
text {*+ −
\noindent+ −
whereby the string argument specifies the sort of the atom.\footnote{A similar + −
design choice was made by Gunter et al \cite{GunterOsbornPopescu09} + −
for their variables.} (The use type+ −
\emph{string} is merely for convenience; any countably infinite type would work+ −
as well.) + −
We have an auxiliary function @{text sort} that is defined as @{thm+ −
sort_of.simps[no_vars]}, and we clearly have for every finite set @{text X} of+ −
atoms and every sort @{text s} the property:+ −
+ −
\begin{proposition}\label{choosefresh}+ −
@{text "If finite X then there exists an atom a such that+ −
sort a = s and a \<notin> X"}.+ −
\end{proposition}+ −
+ −
For implementing sort-respecting permutations, we use functions of type @{typ+ −
"atom => atom"} that @{text "i)"} are bijective; @{text "ii)"} are the+ −
identity on all atoms, except a finite number of them; and @{text "iii)"} map+ −
each atom to one of the same sort. These properties can be conveniently stated+ −
for a function @{text \<pi>} as follows:+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
i)~~~@{term "bij \<pi>"}\hspace{5mm}+ −
ii)~~~@{term "finite {a. \<pi> a \<noteq> a}"}\hspace{5mm}+ −
iii)~~~@{term "\<forall>a. sort (\<pi> a) = sort a"}\hfill\numbered{permtype}+ −
\end{isabelle}+ −
+ −
\noindent+ −
Like all HOL-based theorem provers, Isabelle/HOL allows us to+ −
introduce a new type @{typ perm} that includes just those functions+ −
satisfying all three properties. For example the identity function,+ −
written @{term id}, is included in @{typ perm}. Also function composition, + −
written \mbox{@{text "_ \<circ> _"}}, and function inversion, given by Isabelle/HOL's + −
inverse operator and written \mbox{@{text "inv _"}}, preserve the properties + −
@{text "i"}-@{text "iii"}. + −
+ −
However, a moment of thought is needed about how to construct non-trivial+ −
permutations. In the nominal logic work it turned out to be most convenient+ −
to work with swappings, written @{text "(a b)"}. In our setting the+ −
type of swappings must be+ −
+ −
@{text [display,indent=10] "(_ _) :: atom \<Rightarrow> atom \<Rightarrow> perm"}+ −
+ −
\noindent+ −
but since permutations are required to respect sorts, we must carefully+ −
consider what happens if a user states a swapping of atoms with different+ −
sorts. In earlier versions of Nominal Isabelle, we avoided this problem by+ −
using different types for different sorts; the type system prevented users+ −
from stating ill-sorted swappings. Here, however, definitions such + −
as\footnote{To increase legibility, we omit here and in what follows the+ −
@{term Rep_perm} and @{term "Abs_perm"} wrappers that are needed in our+ −
implementation since we defined permutation not to be the full function space,+ −
but only those functions of type @{typ perm} satisfying properties @{text+ −
i}-@{text "iii"}.}+ −
+ −
@{text [display,indent=10] "(a b) \<equiv> \<lambda>c. if a = c then b else (if b = c then a else c)"}+ −
+ −
\noindent+ −
do not work in general, because the type system does not prevent @{text a}+ −
and @{text b} from having different sorts---in which case the function would+ −
violate property @{text iii}. We could make the definition of swappings+ −
partial by adding the precondition @{term "sort a = sort b"},+ −
which would mean that in case @{text a} and @{text b} have different sorts,+ −
the value of @{text "(a b)"} is unspecified. However, this looked like a+ −
cumbersome solution, since sort-related side conditions would be required+ −
everywhere, even to unfold the definition. It turned out to be more+ −
convenient to actually allow the user to state ``ill-sorted'' swappings but+ −
limit their ``damage'' by defaulting to the identity permutation in the+ −
ill-sorted case:+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}rl}+ −
@{text "(a b) \<equiv>"} & @{text "if (sort a = sort b)"}\\ + −
& \hspace{3mm}@{text "then \<lambda>c. if a = c then b else (if b = c then a else c)"}\\ + −
& \hspace{3mm}@{text "else id"}+ −
\end{tabular}\hfill\numbered{swapdef}+ −
\end{isabelle}+ −
+ −
\noindent+ −
This function is bijective, the identity on all atoms except+ −
@{text a} and @{text b}, and sort respecting. Therefore it is + −
a function in @{typ perm}. + −
+ −
One advantage of using functions instead of lists as a representation for+ −
permutations is that for example the swappings+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{thm swap_commute[no_vars]}\hspace{10mm}+ −
@{text "(a a) = id"}+ −
\end{tabular}\hfill\numbered{swapeqs}+ −
\end{isabelle}+ −
+ −
\noindent+ −
are \emph{equal}. We do not have to use the equivalence relation shown+ −
in~\eqref{permequ} to identify them, as we would if they had been represented+ −
as lists of pairs. Another advantage of the function representation is that+ −
they form a (non-commutative) group, provided we define+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm}+ −
@{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{4mm}+ −
@{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{4mm}+ −
@{thm diff_def[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2"]} + −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
and verify the simple properties+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]} \hspace{3mm}+ −
@{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{3mm}+ −
@{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{3mm}+ −
@{thm group_add_class.left_minus[where a="\<pi>::perm"]} + −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
Again this is in contrast to the list-of-pairs representation which does not+ −
form a group. The technical importance of this fact is that we can rely on+ −
Isabelle/HOL's existing simplification infrastructure for groups, which will+ −
come in handy when we have to do calculations with permutations.+ −
Note that Isabelle/HOL defies standard conventions of mathematical notation+ −
by using additive syntax even for non-commutative groups. Obviously,+ −
composition of permutations is not commutative in general---@{text+ −
"\<pi>\<^sub>1 + \<pi>\<^sub>2 \<noteq> \<pi>\<^sub>2 + \<pi>\<^sub>1"}. But since the point of this paper is to implement the+ −
nominal theory as smoothly as possible in Isabelle/HOL, we tolerate+ −
the non-standard notation in order to reuse the existing libraries.+ −
+ −
By formalising permutations abstractly as functions, and using a single type+ −
for all atoms, we can now restate the \emph{permutation properties} from+ −
\eqref{permprops} as just the two equations+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}+ −
i) & @{thm permute_zero[no_vars]}\\+ −
ii) & @{thm permute_plus[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2",no_vars]}+ −
\end{tabular}\hfill\numbered{newpermprops}+ −
\end{isabelle} + −
+ −
\noindent+ −
in which the permutation operations are of type @{text "perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} and so+ −
have only a single type parameter. Consequently, these properties are+ −
compatible with the one-parameter restriction of Isabelle/HOL's type classes.+ −
There is no need to introduce a separate type class instantiated for each+ −
sort, like in the old approach.+ −
+ −
The next notion allows us to establish generic lemmas involving the+ −
permutation operation.+ −
+ −
\begin{definition}+ −
A type @{text "\<beta>"} is a \emph{permutation type} if the permutation+ −
properties in \eqref{newpermprops} are satisfied for every @{text "x"} of type+ −
@{text "\<beta>"}. + −
\end{definition}+ −
+ −
\noindent+ −
First, it follows from the laws governing+ −
groups that a permutation and its inverse cancel each other. That is, for any+ −
@{text "x"} of a permutation type:+ −
+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{thm permute_minus_cancel(1)[where p="\<pi>", no_vars]}\hspace{10mm}+ −
@{thm permute_minus_cancel(2)[where p="\<pi>", no_vars]}+ −
\end{tabular}\hfill\numbered{cancel}+ −
\end{isabelle} + −
+ −
\noindent+ −
Consequently, in a permutation type the permutation operation @{text "\<pi> \<bullet> _"} is bijective, + −
which in turn implies the property+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{thm (lhs) permute_eq_iff[where p="\<pi>", no_vars]}+ −
$\;$if and only if$\;$+ −
@{thm (rhs) permute_eq_iff[where p="\<pi>", no_vars]}.+ −
\end{tabular}\hfill\numbered{permuteequ}+ −
\end{isabelle} + −
+ −
\noindent+ −
In order to lift the permutation operation to other types, we can define for:+ −
+ −
\begin{isabelle}+ −
\begin{tabular}{@ {}c@ {\hspace{-1mm}}c@ {}}+ −
\begin{tabular}{@ {}r@ {\hspace{2mm}}l@ {}}+ −
atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\+ −
functions: & @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\+ −
permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\+ −
sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\+ −
booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\+ −
\end{tabular} &+ −
\begin{tabular}{@ {}r@ {\hspace{2mm}}l@ {}}+ −
lists: & @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\+ −
& @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\[2mm]+ −
products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\+ −
nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\+ −
\end{tabular}+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
and then establish:+ −
+ −
\begin{theorem}+ −
If @{text \<beta>}, @{text "\<beta>\<^isub>1"} and @{text "\<beta>\<^isub>2"} are permutation types, + −
then so are @{text "atom"}, @{text "\<beta>\<^isub>1 \<Rightarrow> \<beta>\<^isub>2"}, + −
@{text perm}, @{term "\<beta> set"}, @{term "\<beta> list"}, @{term "\<beta>\<^isub>1 \<times> \<beta>\<^isub>2"},+ −
@{text bool} and @{text "nat"}.+ −
\end{theorem}+ −
+ −
\begin{proof}+ −
All statements are by unfolding the definitions of the permutation operations and simple + −
calculations involving addition and minus. With permutations for example we + −
have+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}[b]{@ {}rcl}+ −
@{text "0 \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "0 + \<pi>' - 0 = \<pi>'"}\\+ −
@{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) + \<pi>' - (\<pi>\<^isub>1 + \<pi>\<^isub>2)"}\\+ −
& @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) + \<pi>' - \<pi>\<^isub>2 - \<pi>\<^isub>1"}\\+ −
& @{text "="} & @{text "\<pi>\<^isub>1 + (\<pi>\<^isub>2 + \<pi>' - \<pi>\<^isub>2) - \<pi>\<^isub>1"} @{text "\<equiv>"} @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> \<pi>'"} + −
\end{tabular}\hfill\qed+ −
\end{isabelle}+ −
\end{proof}+ −
+ −
\noindent+ −
The main point is that the above reasoning blends smoothly with the reasoning+ −
infrastructure of Isabelle/HOL; no custom ML-code is necessary and a single+ −
type class suffices. We can also show once and for all that the following+ −
property---which caused so many headaches in our earlier setup---holds for any+ −
permutation type.+ −
+ −
\begin{lemma}\label{permutecompose} + −
Given @{term x} is of permutation type, then + −
@{text "\<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x) = (\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}.+ −
\end{lemma}+ −
+ −
\begin{proof} The proof is as follows:+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}[b]{@ {}rcl@ {\hspace{8mm}}l}+ −
@{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> x"}+ −
& @{text "="} & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> (-\<pi>\<^isub>1) \<bullet> \<pi>\<^isub>1 \<bullet> x"} & by \eqref{cancel}\\+ −
& @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2 - \<pi>\<^isub>1) \<bullet> \<pi>\<^isub>1 \<bullet> x"} & by {\rm(\ref{newpermprops}.@{text "ii"})}\\+ −
& @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}\\+ −
\end{tabular}\hfill\qed+ −
\end{isabelle}+ −
\end{proof}+ −
+ −
%* }+ −
%+ −
%section { * Equivariance * }+ −
%+ −
%text { *+ −
+ −
An \emph{equivariant} function or predicate is one that is invariant under+ −
the swapping of atoms. Having a notion of equivariance with nice logical+ −
properties is a major advantage of bijective permutations over traditional+ −
renaming substitutions \cite[\S2]{Pitts03}. Equivariance can be defined+ −
uniformly for all permutation types, and it is satisfied by most HOL+ −
functions and constants.+ −
+ −
\begin{definition}\label{equivariance}+ −
A function @{text f} is \emph{equivariant} if @{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}.+ −
\end{definition}+ −
+ −
\noindent+ −
There are a number of equivalent formulations for the equivariance property. + −
For example, assuming @{text f} is of type @{text "\<alpha> \<Rightarrow> \<beta>"}, then equivariance + −
can also be stated as + −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{text "\<forall>\<pi> x. \<pi> \<bullet> (f x) = f (\<pi> \<bullet> x)"}+ −
\end{tabular}\hfill\numbered{altequivariance}+ −
\end{isabelle} + −
+ −
\noindent+ −
To see that this formulation implies the definition, we just unfold the+ −
definition of the permutation operation for functions and simplify with the equation+ −
and the cancellation property shown in \eqref{cancel}. To see the other direction, we use + −
the fact + −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{text "\<pi> \<bullet> (f x) = (\<pi> \<bullet> f) (\<pi> \<bullet> x)"}+ −
\end{tabular}\hfill\numbered{permutefunapp}+ −
\end{isabelle} + −
+ −
\noindent+ −
which follows again directly + −
from the definition of the permutation operation for functions and the cancellation + −
property. Similarly for functions with more than one argument. + −
+ −
Both formulations of equivariance have their advantages and disadvantages:+ −
\eqref{altequivariance} is often easier to establish. For example we + −
can easily show that equality is equivariant+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{thm eq_eqvt[where p="\<pi>", no_vars]}+ −
\end{tabular}+ −
\end{isabelle} + −
+ −
\noindent+ −
using the permutation operation on booleans and property \eqref{permuteequ}. + −
Lemma~\ref{permutecompose} establishes that the permutation operation is + −
equivariant. It is also easy to see that the boolean operators, like + −
@{text "\<and>"}, @{text "\<or>"} and @{text "\<longrightarrow>"} are all equivariant. Furthermore + −
a simple calculation will show that our swapping functions are equivariant, that is+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{thm swap_eqvt[where p="\<pi>", no_vars]}+ −
\end{tabular}\hfill\numbered{swapeqvt}+ −
\end{isabelle} + −
+ −
\noindent+ −
for all @{text a}, @{text b} and @{text \<pi>}. These equivariance properties+ −
are tremendously helpful later on when we have to push permutations inside+ −
terms.+ −
*}+ −
+ −
+ −
section {* Support and Freshness *}+ −
+ −
text {*+ −
The most original aspect of the nominal logic work of Pitts et al is a general+ −
definition for ``the set of free variables of an object @{text "x"}''. This+ −
definition is general in the sense that it applies not only to lambda-terms,+ −
but also to lists, products, sets and even functions. The definition depends+ −
only on the permutation operation and on the notion of equality defined for+ −
the type of @{text x}, namely:+ −
+ −
@{thm [display,indent=10] supp_def[no_vars, THEN eq_reflection]}+ −
+ −
\noindent+ −
(Note that due to the definition of swapping in \eqref{swapdef}, we do not+ −
need to explicitly restrict @{text a} and @{text b} to have the same sort.)+ −
There is also the derived notion for when an atom @{text a} is \emph{fresh}+ −
for an @{text x}, defined as+ −
+ −
@{thm [display,indent=10] fresh_def[no_vars]}+ −
+ −
\noindent+ −
A striking consequence of these definitions is that we can prove+ −
without knowing anything about the structure of @{term x} that+ −
swapping two fresh atoms, say @{text a} and @{text b}, leave + −
@{text x} unchanged. For the proof we use the following lemma + −
about swappings applied to an @{text x}:+ −
+ −
\begin{lemma}\label{swaptriple}+ −
Assuming @{text x} is of permutation type, and @{text a}, @{text b} and @{text c} + −
have the same sort, then @{thm (prem 3) swap_rel_trans[no_vars]} and + −
@{thm (prem 4) swap_rel_trans[no_vars]} imply @{thm (concl) swap_rel_trans[no_vars]}.+ −
\end{lemma}+ −
+ −
\begin{proof}+ −
The cases where @{text "a = c"} and @{text "b = c"} are immediate.+ −
For the remaining case it is, given our assumptions, easy to calculate + −
that the permutations+ −
+ −
@{thm [display,indent=10] (concl) swap_triple[no_vars]}+ −
+ −
\noindent+ −
are equal. The lemma is then by application of the second permutation + −
property shown in \eqref{newpermprops}.\hfill\qed+ −
\end{proof}+ −
+ −
\begin{theorem}\label{swapfreshfresh}+ −
Let @{text x} be of permutation type.+ −
@{thm [mode=IfThen] swap_fresh_fresh[no_vars]}+ −
\end{theorem}+ −
+ −
\begin{proof}+ −
If @{text a} and @{text b} have different sort, then the swapping is the identity.+ −
If they have the same sort, we know by definition of support that both+ −
@{term "finite {c. (a \<rightleftharpoons> c) \<bullet> x \<noteq> x}"} and @{term "finite {c. (b \<rightleftharpoons> c) \<bullet> x \<noteq> x}"}+ −
hold. So the union of these sets is finite too, and we know by Proposition~\ref{choosefresh} + −
that there is an atom @{term c}, with the same sort as @{term a} and @{term b}, + −
that satisfies \mbox{@{term "(a \<rightleftharpoons> c) \<bullet> x = x"}} and @{term "(b \<rightleftharpoons> c) \<bullet> x = x"}. + −
Now the theorem follows from Lemma~\ref{swaptriple}.\hfill\qed+ −
\end{proof}+ −
+ −
\noindent+ −
Two important properties that need to be established for later calculations is + −
that @{text "supp"} and freshness are equivariant. For this we first show that:+ −
+ −
\begin{lemma}\label{half}+ −
If @{term x} is a permutation type, then @{thm (lhs) fresh_permute_iff[where p="\<pi>",no_vars]} + −
if and only if @{thm (rhs) fresh_permute_iff[where p="\<pi>",no_vars]}.+ −
\end{lemma}+ −
+ −
\begin{proof}+ −
\begin{isabelle}+ −
\begin{tabular}[t]{c@ {\hspace{2mm}}l@ {\hspace{5mm}}l}+ −
& \multicolumn{2}{@ {}l}{@{thm (lhs) fresh_permute_iff[where p="\<pi>",no_vars]} @{text "\<equiv>"}+ −
@{term "finite {b. (\<pi> \<bullet> a \<rightleftharpoons> b) \<bullet> \<pi> \<bullet> x \<noteq> \<pi> \<bullet> x}"}}\\+ −
@{text "\<Leftrightarrow>"}+ −
& @{term "finite {b. (\<pi> \<bullet> a \<rightleftharpoons> \<pi> \<bullet> b) \<bullet> \<pi> \<bullet> x \<noteq> \<pi> \<bullet> x}"} + −
& since @{text "\<pi> \<bullet> _"} is bijective\\ + −
@{text "\<Leftrightarrow>"}+ −
& @{term "finite {b. \<pi> \<bullet> (a \<rightleftharpoons> b) \<bullet> x \<noteq> \<pi> \<bullet> x}"}+ −
& by \eqref{permutecompose} and \eqref{swapeqvt}\\+ −
@{text "\<Leftrightarrow>"}+ −
& @{term "finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"} @{text "\<equiv>"}+ −
@{thm (rhs) fresh_permute_iff[where p="\<pi>",no_vars]}+ −
& by \eqref{permuteequ}\\+ −
\end{tabular}+ −
\end{isabelle}\hfill\qed+ −
\end{proof}+ −
+ −
\noindent+ −
Together with the definition of the permutation operation on booleans,+ −
we can immediately infer equivariance of freshness: + −
+ −
@{thm [display,indent=10] fresh_eqvt[where p="\<pi>",no_vars]}+ −
+ −
\noindent+ −
Now equivariance of @{text "supp"}, namely+ −
+ −
@{thm [display,indent=10] supp_eqvt[where p="\<pi>",no_vars]}+ −
+ −
\noindent+ −
is by noting that @{thm supp_conv_fresh[no_vars]} and that freshness and + −
the logical connectives are equivariant.+ −
+ −
While the abstract properties of support and freshness, particularly + −
Theorem~\ref{swapfreshfresh}, are useful for developing Nominal Isabelle, + −
one often has to calculate the support of some concrete object. This is + −
straightforward for example for booleans, nats, products and lists:+ −
+ −
\begin{center}+ −
\begin{tabular}{@ {}c@ {\hspace{2mm}}c@ {}}+ −
\begin{tabular}{@ {}r@ {\hspace{2mm}}l}+ −
@{text "booleans"}: & @{term "supp b = {}"}\\+ −
@{text "nats"}: & @{term "supp n = {}"}\\+ −
@{text "products"}: & @{thm supp_Pair[no_vars]}\\+ −
\end{tabular} &+ −
\begin{tabular}{r@ {\hspace{2mm}}l@ {}}+ −
@{text "lists:"} & @{thm supp_Nil[no_vars]}\\+ −
& @{thm supp_Cons[no_vars]}\\+ −
\end{tabular}+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
But establishing the support of atoms and permutations in our setup here is a bit + −
trickier. To do so we will use the following notion about a \emph{supporting set}.+ −
+ −
\begin{definition}+ −
A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}+ −
not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.+ −
\end{definition}+ −
+ −
\noindent+ −
The main motivation for this notion is that we can characterise @{text "supp x"} + −
as the smallest finite set that supports @{text "x"}. For this we prove:+ −
+ −
\begin{lemma}\label{supports} Let @{text x} be of permutation type.+ −
\begin{isabelle}+ −
\begin{tabular}{r@ {\hspace{4mm}}p{10cm}}+ −
i) & @{thm[mode=IfThen] supp_is_subset[no_vars]}\\+ −
ii) & @{thm[mode=IfThen] supp_supports[no_vars]}\\+ −
iii) & @{thm (concl) supp_is_least_supports[no_vars]}+ −
provided @{thm (prem 1) supp_is_least_supports[no_vars]},+ −
@{thm (prem 2) supp_is_least_supports[no_vars]}+ −
and @{text "S"} is the least such set, that means formally,+ −
for all @{text "S'"}, if @{term "finite S'"} and + −
@{term "S' supports x"} then @{text "S \<subseteq> S'"}.+ −
\end{tabular}+ −
\end{isabelle} + −
\end{lemma}+ −
+ −
\begin{proof}+ −
For @{text "i)"} we derive a contradiction by assuming there is an atom @{text a}+ −
with @{term "a \<in> supp x"} and @{text "a \<notin> S"}. Using the second fact, the + −
assumption that @{term "S supports x"} gives us that @{text S} is a superset of + −
@{term "{b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"}, which is finite by the assumption of @{text S}+ −
being finite. But this means @{term "a \<notin> supp x"}, contradicting our assumption.+ −
Property @{text "ii)"} is by a direct application of + −
Theorem~\ref{swapfreshfresh}. For the last property, part @{text "i)"} proves+ −
one ``half'' of the claimed equation. The other ``half'' is by property + −
@{text "ii)"} and the fact that @{term "supp x"} is finite by @{text "i)"}.\hfill\qed + −
\end{proof}+ −
+ −
\noindent+ −
These are all relatively straightforward proofs adapted from the existing + −
nominal logic work. However for establishing the support of atoms and + −
permutations we found the following ``optimised'' variant of @{text "iii)"} + −
more useful:+ −
+ −
\begin{lemma}\label{optimised} Let @{text x} be of permutation type.+ −
We have that @{thm (concl) finite_supp_unique[no_vars]}+ −
provided @{thm (prem 1) finite_supp_unique[no_vars]},+ −
@{thm (prem 2) finite_supp_unique[no_vars]}, and for+ −
all @{text "a \<in> S"} and all @{text "b \<notin> S"}, with @{text a}+ −
and @{text b} having the same sort, \mbox{@{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"}}+ −
\end{lemma}+ −
+ −
\begin{proof}+ −
By Lemma \ref{supports}@{text ".iii)"} we have to show that for every finite+ −
set @{text S'} that supports @{text x}, \mbox{@{text "S \<subseteq> S'"}} holds. We will+ −
assume that there is an atom @{text "a"} that is element of @{text S}, but+ −
not @{text "S'"} and derive a contradiction. Since both @{text S} and+ −
@{text S'} are finite, we can by Proposition \ref{choosefresh} obtain an atom+ −
@{text b}, which has the same sort as @{text "a"} and for which we know+ −
@{text "b \<notin> S"} and @{text "b \<notin> S'"}. Since we assumed @{text "a \<notin> S'"} and+ −
we have that @{text "S' supports x"}, we have on one hand @{term "(a \<rightleftharpoons> b) \<bullet> x+ −
= x"}. On the other hand, the fact @{text "a \<in> S"} and @{text "b \<notin> S"} imply+ −
@{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"} using the assumed implication. This gives us the+ −
contradiction.\hfill\qed+ −
\end{proof}+ −
+ −
\noindent+ −
Using this lemma we only have to show the following three proof-obligations+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}r@ {\hspace{4mm}}l}+ −
i) & @{term "{c} supports c"}\\+ −
ii) & @{term "finite {c}"}\\+ −
iii) & @{text "\<forall>a \<in> {c} b \<notin> {c}. sort a = sort b \<longrightarrow> (a b) \<bullet> c \<noteq> c"}+ −
\end{tabular}+ −
\end{isabelle} + −
+ −
\noindent+ −
in order to establish that @{thm supp_atom[where a="c", no_vars]} holds. In+ −
Isabelle/HOL these proof-obligations can be discharged by easy+ −
simplifications. Similar proof-obligations arise for the support of+ −
permutations, which is+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{thm supp_perm[where p="\<pi>", no_vars]}+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
The only proof-obligation that is + −
interesting is the one where we have to show that+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{text "If \<pi> \<bullet> a \<noteq> a, \<pi> \<bullet> b = b and sort a = sort b, then (a b) \<bullet> \<pi> \<noteq> \<pi>"}.+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
For this we observe that + −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}rcl}+ −
@{thm (lhs) perm_swap_eq[where p="\<pi>", no_vars]} &+ −
if and only if &+ −
@{thm (rhs) perm_swap_eq[where p="\<pi>", no_vars]}+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
holds by a simple calculation using the group properties of permutations.+ −
The proof-obligation can then be discharged by analysing the inequality+ −
between the permutations @{term "(\<pi> \<bullet> a \<rightleftharpoons> b)"} and @{term "(a \<rightleftharpoons> b)"}.+ −
+ −
The main point about support is that whenever an object @{text x} has finite+ −
support, then Proposition~\ref{choosefresh} allows us to choose for @{text x} a + −
fresh atom with arbitrary sort. This is an important operation in Nominal+ −
Isabelle in situations where, for example, a bound variable needs to be+ −
renamed. To allow such a choice, we only have to assume \emph{one} premise+ −
of the form @{text "finite (supp x)"}+ −
for each @{text x}. Compare that with the sequence of premises in our earlier+ −
version of Nominal Isabelle (see~\eqref{fssequence}). For more convenience we+ −
can define a type class for types where every element has finite support, and+ −
prove that the types @{term "atom"}, @{term "perm"}, lists, products and+ −
booleans are instances of this type class. Then \emph{no} premise is needed,+ −
as the type system of Isabelle/HOL can figure out automatically when an object+ −
is finitely supported.+ −
+ −
Unfortunately, this does not work for sets or Isabelle/HOL's function type.+ −
There are functions and sets definable in Isabelle/HOL for which the finite+ −
support property does not hold. A simple example of a function with+ −
infinite support is the function that returns the natural number of an atom+ −
+ −
@{text [display, indent=10] "nat_of (Atom s i) \<equiv> i"}+ −
+ −
\noindent+ −
This function's support is the set of \emph{all} atoms. To establish this we show @{term "\<not> a \<sharp> nat_of"}. + −
This is equivalent to assuming the set @{term "{b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"} is finite+ −
and deriving a contradiction. From the assumption we also know that + −
@{term "{a} \<union> {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"} is finite. Then we can use + −
Proposition~\ref{choosefresh} to choose an atom @{text c} such that+ −
@{term "c \<noteq> a"}, @{term "sort_of c = sort_of a"} and @{term "(a \<rightleftharpoons> c) \<bullet> nat_of = nat_of"}.+ −
Now we can reason as follows:+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}[b]{@ {}rcl@ {\hspace{5mm}}l}+ −
@{text "nat_of a"} & @{text "="} & @{text "(a \<rightleftharpoons> c) \<bullet> (nat_of a)"} & by def.~of permutations on nats\\+ −
& @{text "="} & @{term "((a \<rightleftharpoons> c) \<bullet> nat_of) ((a \<rightleftharpoons> c) \<bullet> a)"} & by \eqref{permutefunapp}\\+ −
& @{text "="} & @{term "nat_of c"} & by assumptions on @{text c}\\+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
+ −
\noindent+ −
But this means we have that @{term "nat_of a = nat_of c"} and @{term "sort_of a = sort_of c"}.+ −
This implies that atoms @{term a} and @{term c} must be equal, which clashes with our+ −
assumption @{term "c \<noteq> a"} about how we chose @{text c}. + −
Cheney \cite{Cheney06} gives similar examples for constructions that have infinite support.+ −
*}+ −
+ −
section {* Concrete Atom Types *}+ −
+ −
text {*+ −
+ −
So far, we have presented a system that uses only a single multi-sorted atom+ −
type. This design gives us the flexibility to define operations and prove+ −
theorems that are generic with respect to atom sorts. For example, as+ −
illustrated above the @{term supp} function returns a set that includes the+ −
free atoms of \emph{all} sorts together; the flexibility offered by the new+ −
atom type makes this possible. + −
+ −
However, the single multi-sorted atom type does not make an ideal interface+ −
for end-users of Nominal Isabelle. If sorts are not distinguished by+ −
Isabelle's type system, users must reason about atom sorts manually. That+ −
means subgoals involving sorts must be discharged explicitly within proof+ −
scripts, instead of being inferred by Isabelle/HOL's type checker. In other+ −
cases, lemmas might require additional side conditions about sorts to be true.+ −
For example, swapping @{text a} and @{text b} in the pair \mbox{@{term "(a,+ −
b)"}} will only produce the expected result if we state the lemma in+ −
Isabelle/HOL as:+ −
*}+ −
+ −
lemma+ −
fixes a b :: "atom"+ −
assumes asm: "sort a = sort b"+ −
shows "(a \<rightleftharpoons> b) \<bullet> (a, b) = (b, a)" + −
using asm by simp+ −
+ −
text {*+ −
\noindent+ −
Fortunately, it is possible to regain most of the type-checking automation+ −
that is lost by moving to a single atom type. We accomplish this by defining+ −
\emph{subtypes} of the generic atom type that only include atoms of a single+ −
specific sort. We call such subtypes \emph{concrete atom types}.+ −
+ −
The following Isabelle/HOL command defines a concrete atom type called+ −
\emph{name}, which consists of atoms whose sort equals the string @{term+ −
"''name''"}.+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\isacommand{typedef}\ \ @{typ name} = @{term "{a. sort\<iota> a = ''name''}"}+ −
\end{isabelle}+ −
+ −
\noindent+ −
This command automatically generates injective functions that map from the+ −
concrete atom type into the generic atom type and back, called+ −
representation and abstraction functions, respectively. We will write these+ −
functions as follows:+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l@ {\hspace{10mm}}l}+ −
@{text "\<lfloor>_\<rfloor> :: name \<Rightarrow> atom"} & + −
@{text "\<lceil>_\<rceil> :: atom \<Rightarrow> name"}+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
With the definition @{thm permute_name_def [where p="\<pi>", THEN+ −
eq_reflection, no_vars]}, it is straightforward to verify that the type + −
@{typ name} is a permutation type.+ −
+ −
In order to reason uniformly about arbitrary concrete atom types, we define a+ −
type class that characterises type @{typ name} and other similarly-defined+ −
types. The definition of the concrete atom type class is as follows: First,+ −
every concrete atom type must be a permutation type. In addition, the class+ −
defines an overloaded function that maps from the concrete type into the+ −
generic atom type, which we will write @{text "|_|"}. For each class+ −
instance, this function must be injective and equivariant, and its outputs+ −
must all have the same sort, that is+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
i) \hspace{1mm}if @{thm (lhs) atom_eq_iff [no_vars]} then @{thm (rhs) atom_eq_iff [no_vars]}\hspace{4mm}+ −
ii) \hspace{1mm}@{thm atom_eqvt[where p="\<pi>", no_vars]}\hspace{4mm}+ −
iii) \hspace{1mm}@{thm sort_of_atom_eq [no_vars]}+ −
\hfill\numbered{atomprops}+ −
\end{isabelle}+ −
+ −
\noindent+ −
With the definition @{thm atom_name_def [THEN eq_reflection, no_vars]} we can+ −
show that @{typ name} satisfies all the above requirements of a concrete atom+ −
type.+ −
+ −
The whole point of defining the concrete atom type class was to let users+ −
avoid explicit reasoning about sorts. This benefit is realised by defining a+ −
special swapping operation of type @{text "\<alpha> \<Rightarrow> \<alpha>+ −
\<Rightarrow> perm"}, where @{text "\<alpha>"} is a concrete atom type:+ −
+ −
@{thm [display,indent=10] flip_def [THEN eq_reflection, no_vars]}+ −
+ −
\noindent+ −
As a consequence of its type, the @{text "\<leftrightarrow>"}-swapping+ −
operation works just like the generic swapping operation, but it does not+ −
require any sort-checking side conditions---the sort-correctness is ensured by+ −
the types! For @{text "\<leftrightarrow>"} we can establish the following+ −
simplification rule:+ −
+ −
@{thm [display,indent=10] permute_flip_at[no_vars]} + −
+ −
\noindent+ −
If we now want to swap the \emph{concrete} atoms @{text a} and @{text b}+ −
in the pair @{term "(a, b)"} we can establish the lemma as follows:+ −
*}+ −
+ −
lemma+ −
fixes a b :: "name"+ −
shows "(a \<leftrightarrow> b) \<bullet> (a, b) = (b, a)" + −
by simp+ −
+ −
text {*+ −
\noindent+ −
There is no need to state an explicit premise involving sorts.+ −
+ −
We can automate the process of creating concrete atom types, so that users + −
can define a new one simply by issuing the command + −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
\isacommand{atom\_decl}~~@{text "name"}+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
This command can be implemented using less than 100 lines of custom ML-code.+ −
In comparison, the old version of Nominal Isabelle included more than 1000+ −
lines of ML-code for creating concrete atom types, and for defining various+ −
type classes and instantiating generic lemmas for them. In addition to+ −
simplifying the ML-code, the setup here also offers user-visible improvements:+ −
Now concrete atoms can be declared at any point of a formalisation, and+ −
theories that separately declare different atom types can be merged+ −
together---it is no longer required to collect all atom declarations in one+ −
place.+ −
*}+ −
+ −
+ −
section {* Multi-Sorted Concrete Atoms *}+ −
+ −
(*<*)+ −
datatype ty = TVar string | Fun ty ty ("_ \<rightarrow> _") + −
(*>*)+ −
+ −
text {*+ −
The formalisation presented so far allows us to streamline proofs and reduce+ −
the amount of custom ML-code in the existing implementation of Nominal+ −
Isabelle. In this section we describe a mechanism that extends the+ −
capabilities of Nominal Isabelle. This mechanism is about variables with + −
additional information, for example typing constraints.+ −
While we leave a detailed treatment of binders and binding of variables for a + −
later paper, we will have a look here at how such variables can be + −
represented by concrete atoms.+ −
+ −
In the previous section we considered concrete atoms that can be used in+ −
simple binders like \emph{@{text "\<lambda>x. x"}}. Such concrete atoms do+ −
not carry any information beyond their identities---comparing for equality+ −
is really the only way to analyse ordinary concrete atoms.+ −
However, in ``Church-style'' lambda-terms \cite{Church40} and in the terms+ −
underlying HOL-systems \cite{PittsHOL4} binders and bound variables have a+ −
more complicated structure. For example in the ``Church-style'' lambda-term+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{text "\<lambda>x\<^isub>\<alpha>. x\<^isub>\<alpha> x\<^isub>\<beta>"}+ −
\end{tabular}\hfill\numbered{church}+ −
\end{isabelle}+ −
+ −
\noindent+ −
both variables and binders include typing information indicated by @{text \<alpha>}+ −
and @{text \<beta>}. In this setting, we treat @{text "x\<^isub>\<alpha>"} and @{text+ −
"x\<^isub>\<beta>"} as distinct variables (assuming @{term "\<alpha>\<noteq>\<beta>"}) so that the+ −
variable @{text "x\<^isub>\<alpha>"} is bound by the lambda-abstraction, but not+ −
@{text "x\<^isub>\<beta>"}.+ −
+ −
To illustrate how we can deal with this phenomenon, let us represent object+ −
types like @{text \<alpha>} and @{text \<beta>} by the datatype+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
\isacommand{datatype}~~@{text "ty = TVar string | ty \<rightarrow> ty"}+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
If we attempt to encode a variable naively as a pair of a @{text name} and a @{text ty}, we have the + −
problem that a swapping, say @{term "(x \<leftrightarrow> y)"}, applied to the pair @{text "((x, \<alpha>), (x, \<beta>))"}+ −
will always permute \emph{both} occurrences of @{text x}, even if the types+ −
@{text "\<alpha>"} and @{text "\<beta>"} are different. This is unwanted, because it will+ −
eventually mean that both occurrences of @{text x} will become bound by a+ −
corresponding binder. + −
+ −
Another attempt might be to define variables as an instance of the concrete+ −
atom type class, where a @{text ty} is somehow encoded within each variable.+ −
Remember we defined atoms as the datatype:+ −
*}+ −
+ −
datatype atom\<iota>\<iota> = Atom\<iota>\<iota> string nat+ −
+ −
text {*+ −
\noindent+ −
Considering our method of defining concrete atom types, the usage of a string+ −
for the sort of atoms seems a natural choice. However, none of the results so+ −
far depend on this choice and we are free to change it.+ −
One possibility is to encode types or any other information by making the sort+ −
argument parametric as follows:+ −
*}+ −
+ −
datatype 'a \<iota>atom\<iota>\<iota>\<iota> = \<iota>Atom\<iota>\<iota> 'a nat+ −
+ −
text {*+ −
\noindent+ −
The problem with this possibility is that we are then back in the old+ −
situation where our permutation operation is parametric in two types and+ −
this would require to work around Isabelle/HOL's restriction on type+ −
classes. Fortunately, encoding the types in a separate parameter is not+ −
necessary for what we want to achieve, as we only have to know when two+ −
types are equal or not. The solution is to use a different sort for each+ −
object type. Then we can use the fact that permutations respect \emph{sorts} to+ −
ensure that permutations also respect \emph{object types}. In order to do+ −
this, we must define an injective function @{text "sort_ty"} mapping from+ −
object types to sorts. For defining functions like @{text "sort_ty"}, it is+ −
more convenient to use a tree datatype for sorts. Therefore we define+ −
*}+ −
+ −
datatype sort = Sort string "(sort list)"+ −
datatype atom\<iota>\<iota>\<iota>\<iota> = Atom\<iota>\<iota>\<iota>\<iota> sort nat+ −
+ −
text {*+ −
\noindent+ −
With this definition,+ −
the sorts we considered so far can be encoded just as \mbox{@{text "Sort s []"}}.+ −
The point, however, is that we can now define the function @{text sort_ty} simply as+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{text "sort_ty (TVar s) = Sort ''TVar'' [Sort s []]"}\\+ −
@{text "sort_ty (\<tau>\<^isub>1 \<rightarrow> \<tau>\<^isub>2) = Sort ''Fun'' [sort_ty \<tau>\<^isub>1, sort_ty \<tau>\<^isub>2]"}+ −
\end{tabular}\hfill\numbered{sortty}+ −
\end{isabelle}+ −
+ −
\noindent+ −
which can easily be shown to be injective. + −
+ −
Having settled on what the sorts should be for ``Church-like'' atoms, we have to+ −
give a subtype definition for concrete atoms. Previously we identified a subtype consisting + −
of atoms of only one specified sort. This must be generalised to all sorts the+ −
function @{text "sort_ty"} might produce, i.e.~the+ −
range of @{text "sort_ty"}. Therefore we define+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\isacommand{typedef}\ \ @{text var} = @{term "{a. sort a : range sort_ty}"}+ −
\end{isabelle}+ −
+ −
\noindent+ −
This command gives us again injective representation and abstraction+ −
functions. We will write them also as \mbox{@{text "\<lfloor>_\<rfloor> :: var \<Rightarrow> atom"}} and+ −
@{text "\<lceil>_\<rceil> :: atom \<Rightarrow> var"}, respectively. + −
+ −
We can define the permutation operation for @{text var} as @{thm+ −
permute_var_def[where p="\<pi>", THEN eq_reflection, no_vars]} and the+ −
injective function to type @{typ atom} as @{thm atom_var_def[THEN+ −
eq_reflection, no_vars]}. Finally, we can define a constructor function that+ −
makes a @{text var} from a variable name and an object type:+ −
+ −
@{thm [display,indent=10] Var_def[where t="\<alpha>", THEN eq_reflection, no_vars]}+ −
+ −
\noindent+ −
With these definitions we can verify all the properties for concrete atom+ −
types except Property \ref{atomprops}@{text ".iii)"}, which requires every+ −
atom to have the same sort. This last property is clearly not true for type+ −
@{text "var"}.+ −
This fact is slightly unfortunate since this+ −
property allowed us to use the type-checker in order to shield the user from+ −
all sort-constraints. But this failure is expected here, because we cannot+ −
burden the type-system of Isabelle/HOL with the task of deciding when two+ −
object types are equal. This means we sometimes need to explicitly state sort+ −
constraints or explicitly discharge them, but as we will see in the lemma+ −
below this seems a natural price to pay in these circumstances.+ −
+ −
To sum up this section, the encoding of type-information into atoms allows us + −
to form the swapping @{term "(Var x \<alpha> \<leftrightarrow> Var y \<alpha>)"} and to prove the following + −
lemma+ −
*}+ −
+ −
lemma+ −
assumes asm: "\<alpha> \<noteq> \<beta>" + −
shows "(Var x \<alpha> \<leftrightarrow> Var y \<alpha>) \<bullet> (Var x \<alpha>, Var x \<beta>) = (Var y \<alpha>, Var x \<beta>)"+ −
using asm by simp+ −
+ −
text {*+ −
\noindent + −
As we expect, the atom @{term "Var x \<beta>"} is left unchanged by the+ −
swapping. With this we can faithfully represent bindings in languages+ −
involving ``Church-style'' terms and bindings as shown in \eqref{church}. We+ −
expect that the creation of such atoms can be easily automated so that the+ −
user just needs to specify \isacommand{atom\_decl}~~@{text "var (ty)"}+ −
where the argument, or arguments, are datatypes for which we can automatically+ −
define an injective function like @{text "sort_ty"} (see \eqref{sortty}).+ −
Our hope is that with this approach Benzmueller and Paulson can make+ −
headway with formalising their results+ −
about simple type theory \cite{PaulsonBenzmueller}.+ −
Because of its limitations, they did not attempt this with the old version + −
of Nominal Isabelle. We also hope we can make progress with formalisations of+ −
HOL-based languages.+ −
*}+ −
+ −
+ −
section {* Conclusion *}+ −
+ −
text {*+ −
This proof pearl describes a new formalisation of the nominal logic work by+ −
Pitts et al. With the definitions we presented here, the formal reasoning blends + −
smoothly with the infrastructure of the Isabelle/HOL theorem prover. + −
Therefore the formalisation will be the underlying theory for a + −
new version of Nominal Isabelle.+ −
+ −
The main difference of this paper with respect to existing work on Nominal+ −
Isabelle is the representation of atoms and permutations. First, we used a+ −
single type for sorted atoms. This design choice means for a term @{term t},+ −
say, that its support is completely characterised by @{term "supp t"}, even+ −
if the term contains different kinds of atoms. Also, whenever we have to+ −
generalise an induction so that a property @{text P} is not just established+ −
for all @{text t}, but for all @{text t} \emph{and} under all permutations+ −
@{text \<pi>}, then we only have to state @{term "\<forall>\<pi>. P (\<pi> \<bullet> t)"}. The reason is+ −
that permutations can now consist of multiple swapping each of which can+ −
swap different kinds of atoms. This simplifies considerably the reasoning+ −
involved in building Nominal Isabelle.+ −
+ −
Second, we represented permutations as functions so that the associated+ −
permutation operation has only a single type parameter. This is very convenient+ −
because the abstract reasoning about permutations fits cleanly+ −
with Isabelle/HOL's type classes. No custom ML-code is required to work+ −
around rough edges. Moreover, by establishing that our permutations-as-functions+ −
representation satisfy the group properties, we were able to use extensively + −
Isabelle/HOL's reasoning infrastructure for groups. This often reduced proofs + −
to simple calculations over @{text "+"}, @{text "-"} and @{text "0"}.+ −
An interesting point is that we defined the swapping operation so that a + −
swapping of two atoms with different sorts is \emph{not} excluded, like + −
in our older work on Nominal Isabelle, but there is no ``effect'' of such + −
a swapping (it is defined as the identity). This is a crucial insight+ −
in order to make the approach based on a single type of sorted atoms to work.+ −
But of course it is analogous to the well-known trick of defining division by + −
zero to return zero.+ −
+ −
We noticed only one disadvantage of the permutations-as-functions: Over+ −
lists we can easily perform inductions. For permutations made up from+ −
functions, we have to manually derive an appropriate induction principle. We+ −
can establish such a principle, but we have no real experience yet whether ours+ −
is the most useful principle: such an induction principle was not needed in+ −
any of the reasoning we ported from the old Nominal Isabelle, except+ −
when showing that if @{term "\<forall>a \<in> supp x. a \<sharp> p"} implies @{term "p \<bullet> x = x"}.+ −
+ −
Finally, our implementation of sorted atoms turned out powerful enough to+ −
use it for representing variables that carry on additional information, for+ −
example typing annotations. This information is encoded into the sorts. With+ −
this we can represent conveniently binding in ``Church-style'' lambda-terms+ −
and HOL-based languages. While dealing with such additional information in + −
dependent type-theories, such as LF or Coq, is straightforward, we are not + −
aware of any other approach in a non-dependent HOL-setting that can deal + −
conveniently with such binders.+ −
+ −
The formalisation presented here will eventually become part of the Isabelle + −
distribution, but for the moment it can be downloaded from the + −
Mercurial repository linked at + −
\href{http://isabelle.in.tum.de/nominal/download}+ −
{http://isabelle.in.tum.de/nominal/download}.\smallskip+ −
+ −
\noindent+ −
{\bf Acknowledgements:} We are very grateful to Jesper Bengtson, Stefan + −
Berghofer and Cezary Kaliszyk for their comments on earlier versions + −
of this paper. We are also grateful to the anonymous referee who helped us to+ −
put the work into the right context. + −
*}+ −
+ −
+ −
(*<*)+ −
end+ −
(*>*)+ −