(*<*)
theory Paper
imports "../Nominal-General/Nominal2_Base"
"../Nominal-General/Nominal2_Eqvt"
"../Nominal-General/Atoms"
"../Nominal/Abs"
"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
fresh_star ("_ #\<^sup>* _" [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"
(*>*)
(*
TODO: write about supp of finite sets, abstraction over finite sets
*)
section {* Introduction *}
text {*
Nominal Isabelle provides a proving infratructure for convenient reasoning
about programming language calculi involving binders such as lambda abstractions or
quantifications in type schemes:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@{text "\<lambda>x. t \<forall>{x\<^isub>1,\<dots>,x\<^isub>n}. \<tau>"}
\hfill\numbered{atomperm}
\end{isabelle}
\noindent
At its core Nominal Isabelle is based on the nominal logic work by Pitts at
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 variable names
that might be bound or free. 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 in lambda abstractions and bound type variables in
type schemes. In order to be able to separate them, each kind of variables needs to be
represented by a different sort of atoms.
The existing nominal logic work usually leaves implicit the sorting
information for atoms and as far as we know leaves out a description of how
sorts are represented. In our formalisation, we therefore have to make a
design decision about how to implement sorted atoms and sort-respecting
permutations. One possibility, which we described in \cite{Urban08}, is to
have separate types for the different
kinds of atoms, say types @{text "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}. With this
design one can represent permutations as lists of pairs of atoms and the
operation of applying a permutation to an object as the function
@{text [display,indent=10] "_ \<bullet> _ :: (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
\noindent
where @{text "\<alpha>"} stands for a type of atoms and @{text "\<beta>"} for the type
of the objects on which the permutation acts. For atoms
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}\\
@{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 with different type than the permutation, we
define @{text "\<pi> \<bullet> c \<equiv> c"}.
With the separate atom types and the list representation of permutations it
is impossible in systems like Isabelle/HOL to state an ``ill-sorted''
permutation, since the type system excludes lists containing atoms of
different type. However, a disadvantage is that whenever we need to
generalise induction hypotheses by quantifying over permutations, we have to
build 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"} and the type system does not allow use to have a
single quantification to stand for all permutations. Similarly, the
notion of support
@{text [display,indent=10] "supp _ :: \<beta> \<Rightarrow> \<alpha> set"}
\noindent
which we will define later, cannot be
used to express the support of an object over \emph{all} atoms. The reason
is 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
Because of these disadvantages, we will use in this paper a single unified atom type to
represent atoms of different sorts. Consequently, we have to deal with the
case that a swapping of two atoms is ill-sorted: we cannot rely anymore on
the type systems to exclude them.
We also will not represent permutations as lists of pairs of atoms (as done in
\cite{Urban08}). Although an
advantage of this representation is that the basic operations on
permutations are already defined in Isabelle's 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, and another advantage is that there is a well-understood
induction principle for lists, a disadvantage is that permutations
do not have unique representations as lists. We have to explicitly identify
them 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}
\noindent
This is a problem when lifting the permutation operation to other types, for
example sets, functions and so on. For this we need to ensure that every definition
is well-behaved in the sense that it satisfies some
\emph{permutation properties}. In the list representation we need
to state these properties as follows:
\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
where the last clause explicitly states that the permutation operation has
to produce the same result for related permutations. Moreover,
``permutations-as-lists'' do not satisfy the group properties. This means by
using this representation we will not be able to reuse the extensive
reasoning infrastructure in Isabelle about groups. Because of this, we will represent
in this paper permutations as functions from atoms to atoms. This representation
is unique and satisfies the laws of non-commutative groups.
Using a single atom type to represent atoms of different sorts and
representing permutations as functions are not new ideas; see
\cite{GunterOsbornPopescu09} \footnote{function rep.} 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.
The paper is organised as follows\ldots
*}
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. We implement these atoms as
*}
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 of 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 "For a finite set of atoms S, there exists an atom a such that
sort a = s and a \<notin> S"}.
\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}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{r@ {\hspace{4mm}}l}
i) & @{term "bij \<pi>"}\\
ii) & @{term "finite {a. \<pi> a \<noteq> a}"}\\
iii) & @{term "\<forall>a. sort (\<pi> a) = sort a"}
\end{tabular}\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 early 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, because @{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
We can also show that the following property 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}
\noindent
In order to lift the permutation operation to other types, we can define for:
\begin{equation}\label{permdefs}
\mbox{
\begin{tabular}{@ {}ll@ {\hspace{2mm}}l@ {}}
1) & atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\
2) & functions: & @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\
3) & permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\
4) & sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
5) & booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
6) & 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]}\\
7) & products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\
8) & nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
\end{tabular}}
\end{equation}
\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}
*}
section {* Equivariance *}
text {*
An important notion in the nominal logic work is \emph{equivariance}.
An equivariant function or predicate is one that is invariant under
the swapping of atoms. This notion can be defined
uniformly as follows:
\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:
the definition, \eqref{permutefunapp} and (\ref{permdefs}.2) lead to a simple
rewrite system that pushes permutations inside a term until they reach
either function constants or variables. The permutations in front of
equivariant functions disappear. Such a rewrite system is often very helpful
in determining whether @{text "p \<bullet> t = t"} holds for a compound term @{text t}. In contrast
\eqref{altequivariance} is usually easier to establish, since statements are
commonly given in a form where functions are fully applied. 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>}.
*}
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
We also use the notation @{thm (lhs) fresh_star_def[no_vars]} for sets ot atoms
defined as follows
@{thm [display,indent=10] fresh_star_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{equation}
\mbox{
\begin{tabular}{@ {}r@ {\hspace{2mm}}l}
@{text "booleans"}: & @{term "supp b = {}"}\\
@{text "nats"}: & @{term "supp n = {}"}\\
@{text "products"}: & @{thm supp_Pair[no_vars]}\\
@{text "lists:"} & @{thm supp_Nil[no_vars]}\\
& @{thm supp_Cons[no_vars]}\\
\end{tabular}}
\end{equation}
\noindent
But establishing the support of atoms and permutations 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 that
@{text "finite (supp x)"} holds. 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.
Unfortunately, this does not work for sets or Isabelle/HOL's function
type.\footnote{Isabelle/HOL takes the type @{text "\<alpha> set"} as an abbreviation
of @{text "\<alpha> \<Rightarrow> bool"}.} 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 {* Support of Finite Sets *}
text {*
As shown above, sets is one instance of a type that is not generally finitely supported.
However, we can easily show that finite sets of atoms are finitely
supported, because their support can be characterised as:
\begin{lemma}\label{finatomsets}
If @{text S} is a finite set of atoms, then @{thm (concl) supp_finite_atom_set[no_vars]}.
\end{lemma}
\begin{proof}
finite-supp-unique
\end{proof}
\noindent
More difficult, however, is it to establish that finite sets of finitely
supported objects are finitely supported.
*}
section {* Induction Principles *}
text {*
While the use of functions as permutation provides us with a unique
representation for permutations (for example @{term "(a \<rightleftharpoons> b)"} and
@{term "(b \<rightleftharpoons> a)"} are equal permutations), this representation has
one draw back: it does not come readily with an induction principle.
Such an induction principle is handy for deriving properties like
@{thm [display, indent=10] supp_perm_eq[no_vars]}
\noindent
However, it is not too difficult to derive an induction principle,
given the fact that we allow only permutations with a finite domain.
*}
section {* An Abstraction Type *}
text {*
To that end, we will consider
first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}. These pairs
are intended to represent the abstraction, or binding, of the set of atoms @{text
"as"} in the body @{text "x"}.
The first question we have to answer is when two pairs @{text "(as, x)"} and
@{text "(bs, y)"} are $\alpha$-equivalent? (For the moment we are interested in
the notion of $\alpha$-equivalence that is \emph{not} preserved by adding
vacuous binders.) To answer this question, we identify four conditions: {\it (i)}
given a free-atom function @{text "fa"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
set"}}, then @{text x} and @{text y} need to have the same set of free
atoms; moreover there must be a permutation @{text p} such that {\it
(ii)} @{text p} leaves the free atoms of @{text x} and @{text y} unchanged, but
{\it (iii)} ``moves'' their bound names so that we obtain modulo a relation,
say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)}
@{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
requirements {\it (i)} to {\it (iv)} can be stated formally as follows:
%
\begin{equation}\label{alphaset}
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
\multicolumn{3}{l}{@{text "(as, x) \<approx>set R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
& @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\
@{text "\<and>"} & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
@{text "\<and>"} & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
@{text "\<and>"} & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\
\end{array}
\end{equation}
\noindent
Note that this relation depends on the permutation @{text
"p"}; $\alpha$-equivalence between two pairs is then the relation where we
existentially quantify over this @{text "p"}. Also note that the relation is
dependent on a free-atom function @{text "fa"} and a relation @{text
"R"}. The reason for this extra generality is that we will use
$\approx_{\,\textit{set}}$ for both ``raw'' terms and $\alpha$-equated terms. In
the latter case, @{text R} will be replaced by equality @{text "="} and we
will prove that @{text "fa"} is equal to @{text "supp"}.
It might be useful to consider first some examples about how these definitions
of $\alpha$-equivalence pan out in practice. For this consider the case of
abstracting a set of atoms over types (as in type-schemes). We set
@{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we
define
\begin{center}
@{text "fa(x) = {x}"} \hspace{5mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) = fa(T\<^isub>1) \<union> fa(T\<^isub>2)"}
\end{center}
\noindent
Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and
\eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and
@{text "({y, x}, y \<rightarrow> x)"} are $\alpha$-equivalent according to
$\approx_{\,\textit{set}}$ and $\approx_{\,\textit{res}}$ by taking @{text p} to
be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"}, then @{text
"([x, y], x \<rightarrow> y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"}
since there is no permutation that makes the lists @{text "[x, y]"} and
@{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \<rightarrow> y"}}
unchanged. Another example is @{text "({x}, x)"} $\approx_{\,\textit{res}}$
@{text "({x, y}, x)"} which holds by taking @{text p} to be the identity
permutation. However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}
$\not\approx_{\,\textit{set}}$ @{text "({x, y}, x)"} since there is no
permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal
(similarly for $\approx_{\,\textit{list}}$). It can also relatively easily be
shown that all three notions of $\alpha$-equivalence coincide, if we only
abstract a single atom.
In the rest of this section we are going to introduce three abstraction
types. For this we define
%
\begin{equation}
@{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_set (as, x) equal supp p (bs, x)"}
\end{equation}
\noindent
(similarly for $\approx_{\,\textit{abs\_res}}$
and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence
relations and equivariant.
\begin{lemma}\label{alphaeq}
The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$
and $\approx_{\,\textit{abs\_res}}$ are equivalence relations, and if @{term
"abs_set (as, x) (bs, y)"} then also @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet>
bs, p \<bullet> y)"} (similarly for the other two relations).
\end{lemma}
\begin{proof}
Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have
a permutation @{text p} and for the proof obligation take @{term "-p"}. In case
of transitivity, we have two permutations @{text p} and @{text q}, and for the
proof obligation use @{text "q + p"}. All conditions are then by simple
calculations.
\end{proof}
\noindent
This lemma allows us to use our quotient package for introducing
new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}
representing $\alpha$-equivalence classes of pairs of type
@{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}
(in the third case).
The elements in these types will be, respectively, written as:
\begin{center}
@{term "Abs_set as x"} \hspace{5mm}
@{term "Abs_res as x"} \hspace{5mm}
@{term "Abs_lst as x"}
\end{center}
\noindent
indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will
call the types \emph{abstraction types} and their elements
\emph{abstractions}. The important property we need to derive is the support of
abstractions, namely:
\begin{theorem}[Support of Abstractions]\label{suppabs}
Assuming @{text x} has finite support, then\\[-6mm]
\begin{center}
\begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
%@ {thm (lhs) supp_abs(1)[no_vars]} & $=$ & @ {thm (rhs) supp_abs(1)[no_vars]}\\
%@ {thm (lhs) supp_abs(2)[no_vars]} & $=$ & @ {thm (rhs) supp_abs(2)[no_vars]}\\
%@ {thm (lhs) supp_abs(3)[where bs="as", no_vars]} & $=$ & @ {thm (rhs) supp_abs(3)[where bs="as", no_vars]}
\end{tabular}
\end{center}
\end{theorem}
\noindent
Below we will show the first equation. The others
follow by similar arguments. By definition of the abstraction type @{text "abs_set"}
we have
%
\begin{equation}\label{abseqiff}
%@ {thm (lhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\;
%@ {thm (rhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}
\end{equation}
\noindent
and also
%
\begin{equation}\label{absperm}
@{thm permute_Abs[no_vars]}
\end{equation}
\noindent
The second fact derives from the definition of permutations acting on pairs
\eqref{permute} and $\alpha$-equivalence being equivariant
(see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show
the following lemma about swapping two atoms in an abstraction.
\begin{lemma}
%@ {thm[mode=IfThen] abs_swap1(1)[where bs="as", no_vars]}
\end{lemma}
\begin{proof}
This lemma is straightforward using \eqref{abseqiff} and observing that
the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.
Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}).
\end{proof}
\noindent
Assuming that @{text "x"} has finite support, this lemma together
with \eqref{absperm} allows us to show
%
\begin{equation}\label{halfone}
%@ {thm abs_supports(1)[no_vars]}
\end{equation}
\noindent
which by Property~\ref{supportsprop} gives us ``one half'' of
Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish
it, we use a trick from \cite{Pitts04} and first define an auxiliary
function @{text aux}, taking an abstraction as argument:
%
\begin{center}
@{thm supp_set.simps[THEN eq_reflection, no_vars]}
\end{center}
\noindent
Using the second equation in \eqref{equivariance}, we can show that
@{text "aux"} is equivariant (since @{term "p \<bullet> (supp x - as) =
(supp (p \<bullet> x)) - (p \<bullet> as)"}) and therefore has empty support.
This in turn means
%
\begin{center}
@{term "supp (supp_gen (Abs_set as x)) \<subseteq> supp (Abs_set as x)"}
\end{center}
\noindent
using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set,
we further obtain
%
\begin{equation}\label{halftwo}
%@ {thm (concl) supp_abs_subset1(1)[no_vars]}
\end{equation}
\noindent
since for finite sets of atoms, @{text "bs"}, we have
@{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes
Theorem~\ref{suppabs}.
The method of first considering abstractions of the
form @{term "Abs_set as x"} etc is motivated by the fact that
we can conveniently establish at the Isabelle/HOL level
properties about them. It would be
laborious to write custom ML-code that derives automatically such properties
for every term-constructor that binds some atoms. Also the generality of
the definitions for $\alpha$-equivalence will help us in the next section.
*}
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}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{r@ {\hspace{3mm}}l}
i) if @{thm (lhs) atom_eq_iff [no_vars]} then @{thm (rhs) atom_eq_iff [no_vars]}\\
ii) @{thm atom_eqvt[where p="\<pi>", no_vars]}\\
iii) @{thm sort_of_atom_eq [no_vars]}
\end{tabular}\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 {* Related Work *}
text {*
Add here comparison with old work.
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.
*}
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
(*>*)