(*<*)+ −
theory Paper+ −
imports "../Nominal/Nominal2_Base" + −
"../Nominal/Atoms" + −
"../Nominal/Nominal2_Abs"+ −
"~~/src/HOL/Library/LaTeXsugar"+ −
begin+ −
+ −
abbreviation+ −
UNIV_atom ("\<allatoms>")+ −
where+ −
"UNIV_atom \<equiv> UNIV::atom set" + −
+ −
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"+ −
+ −
lemma infinite_collect:+ −
assumes "\<forall>x \<in> S. P x" "infinite S"+ −
shows "infinite {x \<in> S. P x}"+ −
using assms+ −
apply(subgoal_tac "infinite {x. x \<in> S}")+ −
apply(simp only: Inf_many_def[symmetric])+ −
apply(erule INFM_mono)+ −
apply(auto)+ −
done+ −
+ −
+ −
(*>*)+ −
+ −
section {* Introduction *}+ −
+ −
text {*+ −
Nominal Isabelle provides a proving infratructure for convenient reasoning+ −
about syntax involving binders, such as lambda terms or type schemes in Mini-ML:+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
@{text "\<lambda>x. t \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. \<tau>"} + −
\end{isabelle}+ −
+ −
\noindent+ −
At its core Nominal Isabelle is based on the nominal logic work by+ −
Pitts at al \cite{GabbayPitts02,Pitts03}, whose most basic notion is+ −
a sort-respecting permutation operation defined over a countably+ −
infinite collection of sorted atoms. + −
+ −
+ −
+ −
The aim of this paper is to+ −
describe how we adapted this work so that it can be implemented in a+ −
theorem prover based on Higher-Order Logic (HOL). For this we+ −
present the definition we made in the implementation and also review+ −
many proofs. There are a two main design choices to be made. One is+ −
how to represent sorted atoms. We opt here for a single unified atom+ −
type to represent atoms of different sorts. The other is how to+ −
present sort-respecting permutations. For them we use the standard+ −
technique of HOL-formalisations of introducing an appropriate+ −
substype of functions from atoms to atoms.+ −
+ −
The nominal logic work has been the starting point for a number of proving+ −
infrastructures, most notable by Norrish \cite{norrish04} in HOL4, by+ −
Aydemir et al \cite{AydemirBohannonWeirich07} in Coq and the work by Urban+ −
and Berghofer in Isabelle/HOL \cite{Urban08}. Its key attraction is a very+ −
general notion, called \emph{support}, for the `set of free variables, or+ −
atoms, of an object' that applies not just to lambda terms and type schemes,+ −
but also to sets, products, lists, booleans and even functions. The notion of support+ −
is derived from the permutation operation defined over the + −
hierarchy of types. This+ −
permutation operation, written @{text "_ \<bullet> _"}, has proved to be much more+ −
convenient for reasoning about syntax, in comparison to, say, arbitrary+ −
renaming substitutions of atoms. One reason is that permutations are+ −
bijective renamings of atoms and thus they can be easily `undone'---namely+ −
by applying the inverse permutation. A corresponding inverse substitution + −
might not always exist, since renaming substitutions are in general only injective. + −
Another reason is that permutations preserve many constructions when reasoning about syntax. + −
For example, suppose a typing context @{text "\<Gamma>"} of the form+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
@{text "x\<^isub>1:\<tau>\<^isub>1, \<dots>, x\<^isub>n:\<tau>\<^isub>n"}+ −
\end{isabelle}+ −
+ −
\noindent+ −
is said to be \emph{valid} provided none of its variables, or atoms, @{text "x\<^isub>i"}+ −
occur twice. Then validity of typing contexts is preserved under+ −
permutations in the sense that if @{text \<Gamma>} is valid then so is \mbox{@{text "\<pi> \<bullet> \<Gamma>"}} for+ −
all permutations @{text "\<pi>"}. Again, this is \emph{not} the case for arbitrary+ −
renaming substitutions, as they might identify some of the @{text "x\<^isub>i"} in @{text \<Gamma>}. + −
+ −
Permutations also behave uniformly with respect to HOL's logic connectives. + −
Applying a permutation to a formula gives, for example + −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}lcl}+ −
@{term "\<pi> \<bullet> (A \<and> B)"} & if and only if & @{text "(\<pi> \<bullet> A) \<and> (\<pi> \<bullet> B)"}\\+ −
@{term "\<pi> \<bullet> (A \<longrightarrow> B)"} & if and only if & @{text "(\<pi> \<bullet> A) \<longrightarrow> (\<pi> \<bullet> B)"}\\+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
This uniform behaviour can also be extended to quantifiers and functions. + −
Because of these good properties of permutations, we are able to automate + −
reasoning to do with \emph{equivariance}. By equivariance we mean the property + −
that every permutation leaves a function unchanged, that is @{term "\<pi> \<bullet> f = f"}+ −
for all @{text "\<pi>"}. This will often simplify arguments involving support + −
of functions, since if they are equivariant then they have empty support---or+ −
`no free atoms'.+ −
+ −
There are a number of subtle differences between the nominal logic work by+ −
Pitts and the formalisation we will present in this paper. One difference + −
is that our+ −
formalisation is compatible with HOL, in the sense that we only extend+ −
HOL by some definitions, withouth the introduction of any new axioms.+ −
The reason why the original nominal logic work is+ −
incompatible with HOL has to do with the way how the finite support property+ −
is enforced: FM-set theory is defined in \cite{Pitts01b} so that every set+ −
in the FM-set-universe has finite support. In nominal logic \cite{Pitts03},+ −
the axioms (E3) and (E4) imply that every function symbol and proposition+ −
has finite support. However, there are notions in HOL that do \emph{not}+ −
have finite support (we will give some examples). In our formalisation, we + −
will avoid the incompatibility of the original nominal logic work by not a+ −
priory restricting our discourse to only finitely supported entities, rather+ −
we will explicitly assume this property whenever it is needed in proofs. One+ −
consequence is that we state our basic definitions not in terms of nominal+ −
sets (as done for example in \cite{Pitts06}), but in terms of the weaker+ −
notion of permutation types---essentially sets equipped with a ``sensible''+ −
notion of permutation operation.+ −
+ −
+ −
+ −
In the nominal logic woworkrk, the `new quantifier' plays a prominent role.+ −
$\new$+ −
+ −
+ −
+ −
+ −
Two binders+ −
+ −
A preliminary version + −
*}+ −
+ −
section {* Sorted Atoms and Sort-Respecting Permutations *}+ −
+ −
text {*+ −
The two most basic notions in the nominal logic work are a countably+ −
infinite collection of sorted atoms and sort-respecting permutations+ −
of 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 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 different sorts of+ −
atoms. However, we found that this does not blend well with+ −
type-classes in Isabelle/HOL (see Section~\ref{related} about+ −
related work). Therefore we use here a single unified atom type to+ −
represent atoms of different sorts. A basic requirement is that+ −
there must be a countably infinite number of atoms of each sort.+ −
This can be implemented as the datatype+ −
+ −
*}+ −
+ −
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} for sorts is merely for convenience; any countably+ −
infinite type would work as well. In what follows we shall write+ −
@{term "UNIV::atom set"} for the set of all atoms. We also have two+ −
auxiliary functions for atoms, namely @{text sort} and @{const+ −
nat_of} which are defined as+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}+ −
@{thm (lhs) sort_of.simps[no_vars]} & @{text "\<equiv>"} & @{thm (rhs) sort_of.simps[no_vars]}\\+ −
@{thm (lhs) nat_of.simps[no_vars]} & @{text "\<equiv>"} & @{thm (rhs) nat_of.simps[no_vars]}+ −
\end{tabular}\hfill\numbered{sortnatof}+ −
\end{isabelle}+ −
+ −
\noindent+ −
We clearly have for every finite set @{text S}+ −
of atoms and every sort @{text s} the property:+ −
+ −
\begin{proposition}\label{choosefresh}\mbox{}\\+ −
@{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 are bijective; are the+ −
identity on all atoms, except a finite number of them; and map+ −
each atom to one of the same sort. These properties can be conveniently stated+ −
in Isabelle/HOL 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 + −
(\ref{permtype}.@{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. The following definition\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 in Isabelle/HOL 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"} in \eqref{permtype}.}+ −
+ −
+ −
@{text [display,indent=10] "(a b) \<equiv> \<lambda>c. if a = c then b else (if b = c then a else c)"}+ −
+ −
\noindent+ −
does not work in general, because @{text a} and @{text b} may have different+ −
sorts---in which case the function would violate property @{text iii} in \eqref{permtype}. 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 as a representation for+ −
permutations is that it is unique. 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} and can be used interchangeably. Another advantage of the function + −
representation is that they form a (non-com\-mu\-ta\-tive) group provided we define+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{10mm}}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}+ −
@{thm (lhs) zero_perm_def[no_vars]} & @{text "\<equiv>"} & @{thm (rhs) zero_perm_def[no_vars]} &+ −
@{thm (lhs) plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2"]} & @{text "\<equiv>"} & + −
@{thm (rhs) plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2"]}\\+ −
@{thm (lhs) uminus_perm_def[where p="\<pi>"]} & @{text "\<equiv>"} & @{thm (rhs) uminus_perm_def[where p="\<pi>"]} &+ −
@{thm (lhs) minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^isub>2"]} & @{text "\<equiv>"} &+ −
@{thm (rhs) minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^isub>2"]}+ −
\end{tabular}\hfill\numbered{groupprops}+ −
\end{isabelle}+ −
+ −
\noindent+ −
and verify the four simple properties+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
i)~~@{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]}\\+ −
ii)~~@{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{9mm}+ −
iii)~~@{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{9mm}+ −
iv)~~@{thm group_add_class.left_minus[where a="\<pi>::perm"]} + −
\end{tabular}\hfill\numbered{grouplaws}+ −
\end{isabelle}+ −
+ −
\noindent+ −
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; for example+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
@{text "(a b) + (b c) \<noteq> (b c) + (a b)"}\;.+ −
\end{isabelle} + −
+ −
\noindent+ −
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.+ −
+ −
A \emph{permutation operation}, written infix as @{text "\<pi> \<bullet> x"},+ −
applies a permutation @{text "\<pi>"} to an object @{text "x"}. This + −
operation has the type+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
@{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}+ −
\end{isabelle} + −
+ −
\noindent+ −
whereby @{text "\<beta>"} is a generic type for @{text x}. The definition of this operation will be + −
given by in terms of `induction' over this generic type. The type-class mechanism+ −
of Isabelle/HOL \cite{Wenzel04} allows us to give a definition for+ −
`base' types, such as atoms, permutations, booleans and natural numbers:+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}}+ −
atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\+ −
permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\+ −
booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\+ −
nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\+ −
\end{tabular}\hfill\numbered{permdefsbase}+ −
\end{isabelle}+ −
+ −
\noindent+ −
and for type-constructors, such as functions, sets, lists and products:+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}}+ −
functions: & @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\+ −
sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\+ −
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]}\\+ −
products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\+ −
\end{tabular}\hfill\numbered{permdefsconstrs}+ −
\end{isabelle}+ −
+ −
\noindent+ −
The type classes also allow us to reason abstractly about the permutation operation. + −
For this we state the following two + −
\emph{permutation properties}: + −
+ −
\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+ −
From these properties and law (\ref{grouplaws}.{\it iv}) about groups + −
follows that a permutation and its inverse cancel each other. That is+ −
+ −
\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, 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 the permutation + −
operation.+ −
+ −
\begin{lemma}\label{permutecompose} + −
@{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]{@ {}c@ {\hspace{2mm}}l@ {\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+ −
Note that the permutation operation for functions is defined so that+ −
we have for applications the property+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
@{text "\<pi> \<bullet> (f x) ="}+ −
@{thm (rhs) permute_fun_app_eq[where p="\<pi>", no_vars]}+ −
\hfill\numbered{permutefunapp}+ −
\end{isabelle}+ −
+ −
\noindent+ −
whenever the permutation properties hold for @{text x}. This property can+ −
be easily shown by unfolding the permutation operation for functions on+ −
the right-hand side, simplifying the beta-redex and eliminating the permutations+ −
in front of @{text x} using \eqref{cancel}.+ −
+ −
The main benefit of the use of type classes is that it allows us to delegate + −
much of the routine resoning involved in determining whether the permutation properties+ −
are satisfied to Isabelle/HOL's type system: we only have to+ −
establish that base types satisfy them and that type-constructors+ −
preserve them. Isabelle/HOL will use this information and determine+ −
whether an object @{text x} with a compound type satisfies the+ −
permutation properties. For this we define the notion of a+ −
\emph{permutation type}:+ −
+ −
\begin{definition}[Permutation type]+ −
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+ −
and establish:+ −
+ −
\begin{theorem}+ −
The types @{type atom}, @{type perm}, @{type bool} and @{type nat}+ −
are permutation types, and if @{text \<beta>}, @{text "\<beta>\<^isub>1"} and @{text+ −
"\<beta>\<^isub>2"} are permutation types, then so are \mbox{@{text "\<beta>\<^isub>1 \<Rightarrow> \<beta>\<^isub>2"}},+ −
@{text "\<beta> set"}, @{text "\<beta> list"} and @{text "\<beta>\<^isub>1 \<times> \<beta>\<^isub>2"}.+ −
\end{theorem}+ −
+ −
\begin{proof}+ −
All statements are by unfolding the definitions of the permutation+ −
operations and simple calculations involving addition and+ −
minus. In case of permutations for example we have+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}[b]{@ {}rcl}+ −
@{text "0 \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "0 + \<pi>' - 0 = \<pi>'"}\smallskip\\+ −
@{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}. It will enable us to characterise how+ −
permutations act upon compound statements in HOL by analysing how+ −
these statements are constructed. To do so, let us first define+ −
\emph{HOL-terms}. They are given by the grammar+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
@{text "t ::= c | x | t\<^isub>1 t\<^isub>2 | \<lambda>x. t"}+ −
\hfill\numbered{holterms}+ −
\end{isabelle} + −
+ −
\noindent+ −
where @{text c} stands for constants and @{text x} for+ −
variables. + −
We assume HOL-terms are fully typed, but for the sake of+ −
greater legibility we leave the typing information implicit. We+ −
also assume the usual notions for free and bound variables of a+ −
HOL-term. Furthermore, it is custom in HOL to regard terms as equal+ −
modulo alpha-, beta- and eta-equivalence.+ −
+ −
An \emph{equivariant} HOL-term is one that is invariant under the+ −
permutation operation. This can be defined in Isabelle/HOL + −
as follows:+ −
+ −
\begin{definition}[Equivariance]\label{equivariance}+ −
A HOL-term @{text t} is \emph{equivariant} provided + −
@{term "\<pi> \<bullet> t = t"} holds for all permutations @{text "\<pi>"}.+ −
\end{definition}+ −
+ −
\noindent+ −
In what follows we will primarily be interested in the cases where @{text t} + −
is a constant, but of course there is no way in Isabelle/HOL to restrict + −
this definition to just these cases.+ −
+ −
There are a number of equivalent formulations for the equivariance+ −
property. For example, assuming @{text t} is of permutation type @{text "\<alpha> \<Rightarrow>+ −
\<beta>"}, then equivariance can also be stated as+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{text "\<forall>\<pi> x. \<pi> \<bullet> (t x) = t (\<pi> \<bullet> x)"}+ −
\end{tabular}\hfill\numbered{altequivariance}+ −
\end{isabelle} + −
+ −
\noindent+ −
We will call this formulation of equivariance in \emph{fully applied form}.+ −
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+ −
\eqref{permutefunapp}. Similarly for HOL-terms that take more than+ −
one argument. The point to note is that equivariance and equivariance in fully+ −
applied form are (for permutation types) always interderivable.+ −
+ −
Both formulations of equivariance have their advantages and+ −
disadvantages: \eqref{altequivariance} is usually more convenient to+ −
establish, since statements in Isabelle/HOL 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}\hfill\numbered{eqeqvt}+ −
\end{isabelle} + −
+ −
\noindent+ −
using the permutation operation on booleans and property+ −
\eqref{permuteequ}. + −
Lemma~\ref{permutecompose} establishes that the+ −
permutation operation is equivariant. The permutation operation for+ −
lists and products, shown in \eqref{permdefsconstrs}, state that the+ −
constructors for products, @{text "Nil"} and @{text Cons} are+ −
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>}. Also the booleans+ −
@{const True} and @{const False} are equivariant by the definition+ −
of the permutation operation for booleans. It is easy to see+ −
that the boolean operators, like @{text "\<and>"}, @{text "\<or>"}, @{text+ −
"\<not>"} and @{text "\<longrightarrow>"}, are equivariant too; for example we have+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}lcl}+ −
@{text "\<pi> \<bullet> (A \<and> B) = (\<pi> \<bullet> A) \<and> (\<pi> \<bullet> B)"}\\+ −
@{text "\<pi> \<bullet> (A \<longrightarrow> B) = (\<pi> \<bullet> A) \<longrightarrow> (\<pi> \<bullet> B)"}\\+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
by the definition of the permutation operation acting on booleans.+ −
+ −
In contrast, the advantage of Definition \ref{equivariance} is that+ −
it leads to a relatively simple rewrite system that allows us to `push' a permutation+ −
towards the leaves of a HOL-term (i.e.~constants and+ −
variables). Then the permutation disappears in cases where the+ −
constants are equivariant. We have implemented this rewrite system+ −
as a simplification tactic on the ML-level of Isabelle/HOL. Having this tactic + −
at our disposal, together with a collection of constants for which + −
equivariance is already established, we can automatically establish + −
equivariance of a constant for which equivariance is not yet known. For this we only have to + −
make sure that the definiens of this constant + −
is a HOL-term whose constants are all equivariant. In what follows + −
we shall specify this tactic and argue that it terminates and + −
is correct (in the sense of pushing a + −
permutation @{text "\<pi>"} inside a term and the only remaining + −
instances of @{text "\<pi>"} are in front of the term's free variables). + −
+ −
The simplifiaction tactic is a rewrite systems consisting of four `oriented' + −
equations. We will first give a naive version of this tactic, which however + −
is in some cornercases incorrect and does not terminate, and then modify + −
it in order to obtain the desired properties. A permutation @{text \<pi>} can + −
be pushed into applications and abstractions as follows+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}lr@ {\hspace{3mm}}c@ {\hspace{3mm}}l}+ −
i) & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & \rrh & @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\\+ −
ii) & @{text "\<pi> \<bullet> (\<lambda>x. t)"} & \rrh & @{text "\<lambda>x. \<pi> \<bullet> (t[x := (-\<pi>) \<bullet> x])"}\\+ −
\end{tabular}\hfill\numbered{rewriteapplam}+ −
\end{isabelle}+ −
+ −
\noindent+ −
The first equation we established in \eqref{permutefunapp};+ −
the second follows from the definition of permutations acting on functions+ −
and the fact that HOL-terms are equal modulo beta-equivalence.+ −
Once the permutations are pushed towards the leaves we need the+ −
following two equations+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}lr@ {\hspace{3mm}}c@ {\hspace{3mm}}l}+ −
iii) & @{term "\<pi> \<bullet> (- \<pi>) \<bullet> x"} & \rrh & @{term "x"}\\+ −
iv) & @{term "\<pi> \<bullet> c"} & \rrh & + −
{\rm @{term "c"}\hspace{6mm}provided @{text c} is equivariant}\\+ −
\end{tabular}\hfill\numbered{rewriteother}+ −
\end{isabelle}+ −
+ −
\noindent+ −
in order to remove permuations in front of bound variables and+ −
equivariant constants. Unfortunately, we have to be careful with+ −
the rules {\it i)} and {\it iv}): they can lead to a loop whenever+ −
\mbox{@{text "t\<^isub>1 t\<^isub>2"}} is of the form @{text "((op \<bullet>) \<pi>') t"}. Note+ −
that we usually write this application using infix notation as+ −
@{text "\<pi> \<bullet> t"} and recall that by Lemma \ref{permutecompose} the+ −
constant @{text "(op \<bullet>)"} is equivariant. Now consider the infinite+ −
reduction sequence+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{text "\<pi> \<bullet> (\<pi>' \<bullet> t)"}+ −
$\;\;\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it iv)}}{\rrh}\;\;$+ −
@{text "(\<pi> \<bullet> \<pi>') \<bullet> (\<pi> \<bullet> t)"}+ −
$\;\;\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it iv)}}{\rrh}\;\;$+ −
@{text "((\<pi> \<bullet> \<pi>') \<bullet> \<pi>) \<bullet> ((\<pi> \<bullet> \<pi>') \<bullet> t)"}~~\ldots%+ −
+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
where the last step is again an instance of the first term, but it+ −
is bigger. To avoid this loop we need to apply our rewrite rule+ −
using an `outside to inside' strategy. This strategy is sufficient+ −
since we are only interested of rewriting terms of the form @{term+ −
"\<pi> \<bullet> t"}, where an outermost permutation needs to pushed inside a term.+ −
+ −
Another problem we have to avoid is that the rules {\it i)} and+ −
{\it iii)} can `overlap'. For this note that+ −
the term @{term "\<pi> \<bullet>(\<lambda>x. x)"} reduces by {\it ii)} to + −
@{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet> x"}, to which we can apply rule {\it iii)} + −
in order to obtain @{term "\<lambda>x. x"}, as is desired---there is no + −
free variable in the original term and so the permutation should completely+ −
vanish. However, the subterm @{text+ −
"(- \<pi>) \<bullet> x"} is also an application. Consequently, the term + −
@{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet>x"} can reduce to @{text "\<lambda>x. (- (\<pi> \<bullet> \<pi>)) \<bullet> (\<pi> \<bullet> x)"} using+ −
{\it i)}. Given our strategy we cannot apply rule {\it iii)} anymore and + −
even worse the measure we will introduce shortly increased. On the+ −
other hand, if we had started with the term @{text "\<pi> \<bullet> ((- \<pi>) \<bullet> x)"}+ −
where @{text \<pi>} and @{text x} are free variables, then we \emph{do}+ −
want to apply rule {\it i)} and not rule {\it iii)}. The latter + −
would eliminate @{text \<pi>} completely. The problem is that rule {\it iii)}+ −
should only apply to instances where the variable is to bound; for free variables + −
we want to use {\it ii)}. + −
+ −
The problem is that in order to distinguish both cases when+ −
inductively taking a term `apart', we have to maintain the+ −
information which variable is bound. This, unfortunately, does not+ −
mesh well with the way how simplification tactics are implemented in+ −
Isabelle/HOL. Our remedy is to use a standard trick in HOL: we+ −
introduce a separate definition for terms of the form @{text "(- \<pi>)+ −
\<bullet> x"}, namely as+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
@{term "unpermute \<pi> x \<equiv> (- \<pi>) \<bullet> x"}+ −
\end{isabelle}+ −
+ −
\noindent+ −
The point is that now we can formulate the rewrite rules as follows+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}lrcl}+ −
i') & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & \rrh & + −
@{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\hspace{45mm}\mbox{}\\+ −
\multicolumn{4}{r}{\rm provided @{text "t\<^isub>1 t\<^isub>2"} is not of the form @{text "unpermute \<pi> x"}}\smallskip\\+ −
ii') & @{text "\<pi> \<bullet> (\<lambda>x. t)"} & \rrh & @{text "\<lambda>x. \<pi> \<bullet> (t[x := unpermute \<pi> x])"}\\+ −
iii') & @{text "\<pi> \<bullet> (unpermute \<pi> x)"} & \rrh & @{term x}\\+ −
iv') & @{term "\<pi> \<bullet> c"} & \rrh & @{term "c"}+ −
\hspace{6mm}{\rm provided @{text c} is equivariant}\\+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
and @{text unpermutes} are only generated in case of bound variables.+ −
Clearly none of these rules overlap. Moreover, given our+ −
outside-to-inside strategy, they terminate. To see this, notice that+ −
the permutation on the right-hand side of the rewrite rules is+ −
always applied to a smaller term, provided we take the measure consisting+ −
of lexicographically ordered pairs whose first component is the size+ −
of a term (counting terms of the form @{text "unpermute \<pi> x"} as+ −
leaves) and the second is the number of occurences of @{text+ −
"unpermute \<pi> x"} and @{text "\<pi> \<bullet> c"}.+ −
+ −
With the definition of the simplification tactic in place, we can+ −
establish its correctness. The property we are after is that for for+ −
a HOL-term @{text t} whose constants are all equivariant, the+ −
HOL-term @{text "\<pi> \<bullet> t"} is equal to @{text "t'"} with @{text "t'"}+ −
being equal to @{text t} except that every free variable @{text x}+ −
in @{text t} is replaced by @{text "\<pi> \<bullet> x"}. Pitts calls this+ −
property \emph{equivariance principle} (book ref ???). In our+ −
setting the precise statement of this property is a slightly more+ −
involved because of the fact that @{text unpermutes} needs to be+ −
treated specially.+ −
+ −
\begin{theorem}[Equivariance Principle]+ −
Suppose a HOL-term @{text t} does not contain any @{text unpermutes} and all+ −
its constants are equivariant. For any permutation @{text \<pi>}, let @{text t'} + −
be the HOL-term @{text t} except every free variable @{text x} in @{term t} is + −
replaced by @{text "\<pi> \<bullet> x"}, then @{text "\<pi> \<bullet> t = t'"}.+ −
\end{theorem}+ −
+ −
+ −
+ −
With these definitions in place we can define the notion of an \emph{equivariant}+ −
HOL-term+ −
+ −
\begin{definition}[Equivariant HOL-term]+ −
A HOL-term is \emph{equivariant}, provided it is closed and composed of applications, + −
abstractions and equivariant constants only.+ −
\end{definition}+ −
+ −
\noindent+ −
For equivariant terms we have+ −
+ −
\begin{lemma}+ −
For an equivariant HOL-term @{text "t"}, @{term "\<pi> \<bullet> t = t"} for all permutations @{term "\<pi>"}.+ −
\end{lemma}+ −
+ −
Let us now see how to use the equivariance principle. We have + −
+ −
*}+ −
+ −
+ −
section {* Support and Freshness *}+ −
+ −
text {*+ −
The most original aspect of the nominal logic work of Pitts is a general+ −
definition for `the set of free variables, or free atoms, of an object @{text "x"}'. This+ −
definition is general in the sense that it applies not only to lambda terms,+ −
but to any type for which a permutation operation is defined + −
(like lists, sets, functions and so on). + −
+ −
\begin{definition}[Support] Given @{text x} is of permutation type, then + −
+ −
@{thm [display,indent=10] supp_def[no_vars, THEN eq_reflection]}+ −
\end{definition}+ −
+ −
\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} of permutation type, 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 \mbox{@{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}+ −
& @{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 Lemma~\ref{permutecompose} and \eqref{swapeqvt}\\+ −
@{text "\<Leftrightarrow>"}+ −
& @{term "finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"}+ −
& by \eqref{permuteequ}\\+ −
@{text "\<equiv>"}+ −
& @{thm (rhs) fresh_permute_iff[where p="\<pi>",no_vars]}+ −
\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. ??? Equivariance+ −
+ −
A simple consequence of the definition of support and equivariance is that + −
if a function @{text f} is equivariant then we have + −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{thm (concl) supp_fun_eqvt[no_vars]}+ −
\end{tabular}\hfill\numbered{suppeqvtfun}+ −
\end{isabelle} + −
+ −
\noindent + −
For function applications we can establish the two following properties.+ −
+ −
\begin{lemma} Let @{text f} and @{text x} be of permutation type, then+ −
\begin{isabelle}+ −
\begin{tabular}{r@ {\hspace{4mm}}p{10cm}}+ −
@{text "i)"} & @{thm[mode=IfThen] fresh_fun_app[no_vars]}\\+ −
@{text "ii)"} & @{thm supp_fun_app[no_vars]}\\+ −
\end{tabular}+ −
\end{isabelle}+ −
\end{lemma}+ −
+ −
\begin{proof}+ −
???+ −
\end{proof}+ −
+ −
+ −
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{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l@ {\hspace{4mm}}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{isabelle}+ −
+ −
\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}[Supporting Set]+ −
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. 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 @{const nat_of} shown in \eqref{sortnatof}. This+ −
function's support is the set of \emph{all} atoms @{term "UNIV::atom set"}. + −
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}.\footnote{Cheney \cite{Cheney06} + −
gives similar examples for constructions that have infinite support.}+ −
*}+ −
+ −
section {* Support of Finite Sets *}+ −
+ −
text {*+ −
Also the set type is one instance whose elements are not generally finitely + −
supported (we will give an example in Section~\ref{concrete}). + −
However, we can easily show that finite sets and co-finite sets of atoms are finitely+ −
supported, because their support can be characterised as:+ −
+ −
\begin{lemma}\label{finatomsets}\mbox{}\\+ −
@{text "i)"} If @{text S} is a finite set of atoms, then @{thm (concl) supp_finite_atom_set[no_vars]}.\\+ −
@{text "ii)"} If @{term "UNIV - (S::atom set)"} is a finite set of atoms, then + −
@{thm (concl) supp_cofinite_atom_set[no_vars]}.+ −
\end{lemma}+ −
+ −
\begin{proof}+ −
Both parts can be easily shown by Lemma~\ref{optimised}. We only have to observe+ −
that a swapping @{text "(a b)"} leaves a set @{text S} unchanged provided both+ −
@{text a} and @{text b} are elements in @{text S} or both are not in @{text S}.+ −
However if the sorts of a @{text a} and @{text b} agree, then the swapping will+ −
change @{text S} if either of them is an element in @{text S} and the other is + −
not.\hfill\qed+ −
\end{proof}+ −
+ −
\noindent+ −
Note that a consequence of the second part of this lemma is that + −
@{term "supp (UNIV::atom set) = {}"}.+ −
More difficult, however, is it to establish that finite sets of finitely + −
supported objects are finitely supported. For this we first show that+ −
the union of the suports of finitely many and finitely supported objects + −
is finite, namely+ −
+ −
\begin{lemma}\label{unionsupp}+ −
If @{text S} is a finite set whose elements are all finitely supported, then\\+ −
@{text "i)"} @{thm (concl) Union_of_finite_supp_sets[no_vars]} and\\+ −
@{text "ii)"} @{thm (concl) Union_included_in_supp[no_vars]}.+ −
\end{lemma}+ −
+ −
\begin{proof}+ −
The first part is by a straightforward induction on the finiteness of @{text S}. + −
For the second part, we know that @{term "\<Union>x\<in>S. supp x"} is a set of atoms, which+ −
by the first part is finite. Therefore we know by Lemma~\ref{finatomsets}.@{text "i)"}+ −
that @{term "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"}. Taking @{text "f"} to be+ −
\mbox{@{text "\<lambda>S. \<Union> (supp ` S)"}}, we can write the right hand side as @{text "supp (f S)"}.+ −
Since @{text "f"} is an equivariant function, we have that + −
@{text "supp (f S) \<subseteq> supp S"} by ??? This completes the second part.\hfill\qed+ −
\end{proof}+ −
+ −
\noindent+ −
With this lemma in place we can establish that+ −
+ −
\begin{lemma}+ −
@{thm[mode=IfThen] supp_of_finite_sets[no_vars]}+ −
\end{lemma}+ −
+ −
\begin{proof}+ −
The right-to-left inclusion is proved in Lemma~\ref{unionsupp}.@{text "ii)"}. To show the inclusion + −
in the other direction we have to show Lemma~\ref{supports}.@{text "i)"}+ −
\end{proof}+ −
*}+ −
+ −
+ −
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\label{concrete} *}+ −
+ −
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 {* Related Work\label{related} *}+ −
+ −
text {*+ −
Add here comparison with old work.+ −
+ −
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+ −
+ −
+ −
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. + −
+ −
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.+ −
*}+ −
+ −
+ −
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+ −
(*>*)+ −