diff -r a6f3e1b08494 -r b6873d123f9b Pearl-jv/Paper.thy --- a/Pearl-jv/Paper.thy Sat May 12 21:05:59 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1819 +0,0 @@ -(*<*) -theory Paper -imports "../Nominal/Nominal2_Base" - "../Nominal/Atoms" - "../Nominal/Nominal2_Abs" - "~~/src/HOL/Library/LaTeXsugar" -begin - -abbreviation - UNIV_atom ("\") -where - "UNIV_atom \ 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 ("\_\") and - Abs_name ("\_\") and - Rep_var ("\_\") and - Abs_var ("\_\") 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 \ sort_of" - -lemma infinite_collect: - assumes "\x \ S. P x" "infinite S" - shows "infinite {x \ S. P x}" -using assms -apply(subgoal_tac "infinite {x. x \ 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 "\x. t \{x\<^isub>1,\, x\<^isub>n}. \"} - \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 - subtype 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 "_ \ _"}, 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 "\"} of the form - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - @{text "x\<^isub>1:\\<^isub>1, \, x\<^isub>n:\\<^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 \} is valid then so is \mbox{@{text "\ \ \"}} for - all permutations @{text "\"}. Again, this is \emph{not} the case for arbitrary - renaming substitutions, as they might identify some of the @{text "x\<^isub>i"} in @{text \}. - - 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 "\ \ (A \ B)"} & if and only if & @{text "(\ \ A) \ (\ \ B)"}\\ - @{term "\ \ (A \ B)"} & if and only if & @{text "(\ \ A) \ (\ \ 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 "\ \ f = f"} - for all @{text "\"}. 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$ - - - Obstacles for Coq; no type-classes, difficulties with quotient types, - need for classical reasoning - - 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 in Isabelle/HOL as the datatype - -*} - - datatype atom\ = Atom\ 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 "\"} & @{thm (rhs) sort_of.simps[no_vars]}\\ - @{thm (lhs) nat_of.simps[no_vars]} & @{text "\"} & @{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 \ S"}. - \end{proposition} - - \noindent - This property will be used later whenever we have to chose a `fresh' atom. - - 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 \} as follows: - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{r@ {\hspace{4mm}}l} - i) & @{term "bij \"}\\ - ii) & @{term "finite {a. \ a \ a}"}\\ - iii) & @{term "\a. sort (\ 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 "_ \ _"}}, 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 \ atom \ 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) \ \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) \"} & @{text "if (sort a = sort b)"}\\ - & \hspace{3mm}@{text "then \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 a unique representation. 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 "\"} & @{thm (rhs) zero_perm_def[no_vars]} & - @{thm (lhs) plus_perm_def[where p="\\<^isub>1" and q="\\<^isub>2"]} & @{text "\"} & - @{thm (rhs) plus_perm_def[where p="\\<^isub>1" and q="\\<^isub>2"]}\\ - @{thm (lhs) uminus_perm_def[where p="\"]} & @{text "\"} & @{thm (rhs) uminus_perm_def[where p="\"]} & - @{thm (lhs) minus_perm_def[where ?p1.0="\\<^isub>1" and ?p2.0="\\<^isub>2"]} & @{text "\"} & - @{thm (rhs) minus_perm_def[where ?p1.0="\\<^isub>1" and ?p2.0="\\<^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="\\<^isub>1" and b="\\<^isub>2" and c="\\<^isub>3"]}\smallskip\\ - ii)~~@{thm monoid_add_class.add_0_left[where a="\::perm"]} \hspace{9mm} - iii)~~@{thm monoid_add_class.add_0_right[where a="\::perm"]} \hspace{9mm} - iv)~~@{thm group_add_class.left_minus[where a="\::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) \ (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 "\ \ x"}, - applies a permutation @{text "\"} to an object @{text "x"}. This - operation has the type - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - @{text "_ \ _ :: perm \ \ \ \"} - \end{isabelle} - - \noindent - whereby @{text "\"} is a generic type for the object @{text - x}.\footnote{We will write @{text "((op \) \) - x"} for this operation in the few cases where we need to indicate - that it is a function applied with two arguments.} 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="\",no_vars, THEN eq_reflection]}\\ - permutations: & @{thm permute_perm_def[where p="\" and q="\'", THEN eq_reflection]}\\ - booleans: & @{thm permute_bool_def[where p="\", no_vars, THEN eq_reflection]}\\ - nats: & @{thm permute_nat_def[where p="\", 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 "\ \ f \ \x. \ \ (f ((-\) \ x))"}\\ - sets: & @{thm permute_set_eq[where p="\", no_vars, THEN eq_reflection]}\\ - lists: & @{thm permute_list.simps(1)[where p="\", no_vars, THEN eq_reflection]}\\ - & @{thm permute_list.simps(2)[where p="\", no_vars, THEN eq_reflection]}\\ - products: & @{thm permute_prod.simps[where p="\", 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="\\<^isub>1" and q="\\<^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="\", no_vars]}\hspace{10mm} - @{thm permute_minus_cancel(2)[where p="\", no_vars]} - \end{tabular}\hfill\numbered{cancel} - \end{isabelle} - - \noindent - Consequently, the permutation operation @{text "\ \ _"}~~is bijective, - which in turn implies the property - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}l} - @{thm (lhs) permute_eq_iff[where p="\", no_vars]} - $\;$if and only if$\;$ - @{thm (rhs) permute_eq_iff[where p="\", 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 "\\<^isub>1 \ (\\<^isub>2 \ x) = (\\<^isub>1 \ \\<^isub>2) \ (\\<^isub>1 \ x)"}. - \end{lemma} - - \begin{proof} The proof is as follows: - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}[b]{@ {}c@ {\hspace{2mm}}l@ {\hspace{8mm}}l} - & @{text "\\<^isub>1 \ \\<^isub>2 \ x"}\\ - @{text "="} & @{text "\\<^isub>1 \ \\<^isub>2 \ (-\\<^isub>1) \ \\<^isub>1 \ x"} & by \eqref{cancel}\\ - @{text "="} & @{text "(\\<^isub>1 + \\<^isub>2 - \\<^isub>1) \ (\\<^isub>1 \ x)"} & by {\rm(\ref{newpermprops}.@{text "ii"})}\\ - @{text "\"} & @{text "(\\<^isub>1 \ \\<^isub>2) \ (\\<^isub>1 \ 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 equation - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - @{text "\ \ (f x) ="} - @{thm (rhs) permute_fun_app_eq[where p="\", no_vars]} - \hfill\numbered{permutefunapp} - \end{isabelle} - - \noindent - provided the permutation properties hold for @{text x}. This equation can - be easily shown by unfolding the permutation operation for functions on - the right-hand side of the equation, simplifying the resulting 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. Then Isabelle/HOL will use this information and determine - whether an object @{text x} with a compound type, like @{typ "atom \ (atom set * nat)"}, satisfies the - permutation properties. For this we define the notion of a - \emph{permutation type}: - - \begin{definition}[Permutation Type] - A type @{text "\"} is a \emph{permutation type} if the permutation - properties in \eqref{newpermprops} are satisfied for every @{text - "x"} of type @{text "\"}. - \end{definition} - - \noindent - and establish: - - \begin{theorem} - The types @{type atom}, @{type perm}, @{type bool} and @{type nat} - are permutation types, and if @{text \}, @{text "\\<^isub>1"} and @{text - "\\<^isub>2"} are permutation types, then so are \mbox{@{text "\\<^isub>1 \ \\<^isub>2"}}, - @{text "\ set"}, @{text "\ list"} and @{text "\\<^isub>1 \ \\<^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 \ \'"} & @{text "\"} & @{text "0 + \' - 0 = \'"}\smallskip\\ - @{text "(\\<^isub>1 + \\<^isub>2) \ \'"} & @{text "\"} & @{text "(\\<^isub>1 + \\<^isub>2) + \' - (\\<^isub>1 + \\<^isub>2)"}\\ - & @{text "="} & @{text "(\\<^isub>1 + \\<^isub>2) + \' - \\<^isub>2 - \\<^isub>1"}\\ - & @{text "="} & @{text "\\<^isub>1 + (\\<^isub>2 + \' - \\<^isub>2) - \\<^isub>1"}\\ - & @{text "\"} & @{text "\\<^isub>1 \ \\<^isub>2 \ \'"} - \end{tabular}\hfill\qed - \end{isabelle} - \end{proof} -*} - -section {* Equivariance *} - -text {* - (mention alpha-structural paper by Andy) - - Two important notions in the nominal logic work are what Pitts calls - \emph{equivariance} and the \emph{equivariance principle}. These - notions allows us to characterise how permutations act upon compound - statements in HOL by analysing how these statements are constructed. - The notion of equivariance means that an object is invariant under - any permutations. This can be defined as follows: - - \begin{definition}[Equivariance]\label{equivariance} - An object @{text "x"} of permutation type is \emph{equivariant} provided - for all permutations @{text "\"}, \mbox{@{term "\ \ x = x"}} holds. - \end{definition} - - \noindent - In what follows we will primarily be interested in the cases where - @{text x} 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 equivariance. - For example, assuming @{text f} is a function of permutation - type @{text "\ \ \"}, then equivariance of @{text f} can also be stated as - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}l} - @{text "\\ x. \ \ (f x) = f (\ \ x)"} - \end{tabular}\hfill\numbered{altequivariance} - \end{isabelle} - - \noindent - We will say this formulation of equivariance is 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 functions that take more than - one argument. The point to note is that equivariance and equivariance in fully - applied form are always interderivable (for permutation types). - - Both formulations of equivariance have their advantages and - disadvantages: \eqref{altequivariance} is usually more convenient to - establish, since statements in 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="\", 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="\", no_vars]} - \end{tabular}\hfill\numbered{swapeqvt} - \end{isabelle} - - \noindent - for all @{text a}, @{text b} and @{text \}. Also the booleans - @{const True} and @{const False} are equivariant by the definition - of the permutation operation for booleans. Given this definition, it - is also easy to see that the boolean operators, like @{text "\"}, - @{text "\"}, @{text "\"} and @{text "\"} are equivariant: - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}lcl} - @{text "\ \ (A \ B) = (\ \ A) \ (\ \ B)"}\\ - @{text "\ \ (A \ B) = (\ \ A) \ (\ \ B)"}\\ - @{text "\ \ (A \ B) = (\ \ A) \ (\ \ B)"}\\ - @{text "\ \ (\A) = \(\ \ A)"}\\ - \end{tabular} - \end{isabelle} - - In contrast, the advantage of Definition \ref{equivariance} is that - it allows us to state a general principle how permutations act on - statements in HOL. For this we will define a rewrite system that - `pushes' a permutation towards the leaves of statements (i.e.~constants - and variables). Then the permutations disappear in cases where the - constants are equivariant. To do so, let us first define - \emph{HOL-terms}, which are the building blocks of statements in HOL. - They are given by the grammar - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - @{text "t ::= c | x | t\<^isub>1 t\<^isub>2 | \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 better - legibility we leave the typing information implicit. We also assume - the usual notions for free and bound variables of a HOL-term. - Furthermore, HOL-terms are regarded as equal modulo alpha-, beta- - and eta-equivalence. The equivariance principle can now - be stated formally as follows: - - \begin{theorem}[Equivariance Principle]\label{eqvtprin} - Suppose a HOL-term @{text t} whose constants are all equivariant. For any - permutation @{text \}, let @{text t'} be @{text t} except every - free variable @{text x} in @{term t} is replaced by @{text "\ \ x"}, then - @{text "\ \ t = t'"}. - \end{theorem} - - \noindent - The significance of this principle is that we can automatically establish - the equivariance of a constant for which equivariance is not yet - known. For this we only have to establish that the definiens of this - constant is a HOL-term whose constants are all equivariant. - This meshes well with how HOL is designed: except for a few axioms, every constant - is defined in terms of existing constants. For example an alternative way - to deduce that @{term True} is equivariant is to look at its - definition - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - @{thm True_def} - \end{isabelle} - - \noindent - and observing that the only constant in the definiens, namely @{text "="}, is - equivariant. Similarly, the universal quantifier @{text "\"} is definied in HOL as - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - @{text "\x. P x \ "}~@{thm (rhs) All_def[no_vars]} - \end{isabelle} - - \noindent - The constants in the definiens @{thm (rhs) All_def[no_vars]}, namely @{text "="} - and @{text "True"}, are equivariant (we shown this above). Therefore - the equivariance principle gives us - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l} - @{text "\ \ (\x. P x)"} & @{text "\"} & @{text "\ \ (P = (\x. True))"}\\ - & @{text "="} & @{text "(\ \ P) = (\x. True)"}\\ - & @{text "\"} & @{text "\x. (\ \ P) x"} - \end{tabular} - \end{isabelle} - - \noindent - which means the constant @{text "\"} must be equivariant. From this - we can deduce that the existential quantifier @{text "\"} is equivariant. - Its definition in HOL is - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - @{text "\x. P x \ "}~@{thm (rhs) Ex_def[no_vars]} - \end{isabelle} - - \noindent - where again the HOL-term on the right-hand side only contains equivariant constants - (namely @{text "\"} and @{text "\"}). Taking both facts together, we can deduce that - the unique existential quantifier @{text "\!"} is equivariant. Its definition - is - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - @{text "\!x. P x \ "}~@{thm (rhs) Ex1_def[no_vars]} - \end{isabelle} - - \noindent - with all constants on the right-hand side being equivariant. With this kind - of reasoning we can build up a database of equivariant constants, which will - be handy for more complex calculations later on. - - Before we proceed, let us give a justification for the equivariance principle. - This justification cannot be given directly inside Isabelle/HOL since we cannot - prove any statement about HOL-terms. Instead, we will use a rewrite - system consisting of a series of equalities - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - @{text "\ \ t = ... = t'"} - \end{isabelle} - - \noindent - that establish the equality between @{term "\ \ t"} and - @{text "t'"}. The idea of the rewrite system is to push the - permutation inside the term @{text t}. We have implemented this as a - conversion tactic on the ML-level of Isabelle/HOL. In what follows, - we will show that this tactic produces only finitely many equations - and also show that it is correct (in the sense of pushing a permutation - @{text "\"} inside a term and the only remaining instances of @{text - "\"} are in front of the term's free variables). - - The tactic applies four `oriented' equations. - We will first give a naive version of - our tactic, which however in some corner cases produces incorrect - results or does not terminate. We then give a modification in order - to obtain the desired properties. - Consider the following for oriented equations - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}lr@ {\hspace{3mm}}c@ {\hspace{3mm}}l} - i) & @{text "\ \ (t\<^isub>1 t\<^isub>2)"} & \rrh & @{term "(\ \ t\<^isub>1) (\ \ t\<^isub>2)"}\\ - ii) & @{text "\ \ (\x. t)"} & \rrh & @{text "\x. \ \ (t[x := (-\) \ x])"}\\ - iii) & @{term "\ \ (- \) \ x"} & \rrh & @{term "x"}\\ - iv) & @{term "\ \ c"} & \rrh & - {\rm @{term "c"}\hspace{6mm}provided @{text c} is equivariant}\\ - \end{tabular}\hfill\numbered{rewriteapplam} - \end{isabelle} - - \noindent - These equation are oriented in the sense of being applied in the left-to-right - direction. 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. - The third is a consequence of \eqref{cancel} and the fourth from - Definition~\ref{equivariance}. Unfortunately, we have to be careful with - the rules {\it i)} and {\it iv}) since they can lead to loops whenever - \mbox{@{text "t\<^isub>1 t\<^isub>2"}} is of the form @{text "((op \) \') t"}. - Recall that we established in Lemma \ref{permutecompose} that the - constant @{text "(op \)"} is equivariant and consider the infinite - reduction sequence - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}l} - @{text "\ \ (\' \ t)"} - $\;\;\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it iv)}}{\rrh}\;\;$ - @{text "(\ \ \') \ (\ \ t)"} - $\;\;\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it iv)}}{\rrh}\;\;$ - @{text "((\ \ \') \ \) \ ((\ \ \') \ t)"}~~\ldots% - - \end{tabular} - \end{isabelle} - - \noindent - where the last term is again an instance of rewrite rule {\it i}), but larger. - To avoid this loop we will apply the rewrite rule - using an `outside to inside' strategy. This strategy is sufficient - since we are only interested of rewriting terms of the form @{term - "\ \ 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 "\ - \(\x. x)"} reduces by {\it ii)} to @{term "\x. \ \ (- \) \ x"}, to - which we can apply rule {\it iii)} in order to obtain @{term - "\x. x"}, as is desired: since there is no free variable in the original - term, the permutation should completely vanish. However, the - subterm @{text "(- \) \ x"} is also an application. Consequently, - the term @{term "\x. \ \ (- \) \x"} can also reduce to @{text "\x. (- (\ - \ \)) \ (\ \ x)"} using {\it i)}. Given our strategy, we cannot - apply rule {\it iii)} anymore in order to eliminate the permutation. - In contrast, if we start - with the term @{text "\ \ ((- \) \ x)"} where @{text \} and @{text - x} are free variables, then we \emph{do} want to apply rule {\it i)} - in order to obtain @{text "(\ \ (- \)) \ (\ \ x)"} - and not rule {\it iii)}. The latter would eliminate @{text \} - completely and thus violating our correctness property. The problem is that - rule {\it iii)} should only apply to - instances where the corresponding variable is to bound; for free variables we want - to use {\it ii)}. In order to distinguish these cases we have to - maintain the information which variable is bound when inductively - taking a term `apart'. This, unfortunately, does not mesh well with - the way how conversion 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 "(- \) \ x"}, - namely as - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - @{term "unpermute \ x \ (- \) \ x"} - \end{isabelle} - - \noindent - The point is that now we can re-formulate the rewrite rules as follows - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}lrcl} - i') & @{text "\ \ (t\<^isub>1 t\<^isub>2)"} & \rrh & - @{term "(\ \ t\<^isub>1) (\ \ 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 \ x"}}\smallskip\\ - ii') & @{text "\ \ (\x. t)"} & \rrh & @{text "\x. \ \ (t[x := unpermute \ x])"}\\ - iii') & @{text "\ \ (unpermute \ x)"} & \rrh & @{term x}\\ - iv') & @{term "\ \ c"} & \rrh & @{term "c"} - \hspace{6mm}{\rm provided @{text c} is equivariant}\\ - \end{tabular} - \end{isabelle} - - \noindent - where @{text unpermutes} are only generated in case of bound variables. - Clearly none of these rules overlap. Moreover, given our - outside-to-inside strategy, applying them repeatedly must 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 \ x"} as - leaves) and the second is the number of occurences of @{text - "unpermute \ x"} and @{text "\ \ c"}. - - With the rewrite rules of the conversions tactic in place, we can - establish its correctness. The property we are after is that - for a HOL-term @{text t} whose constants are all equivariant the - term \mbox{@{text "\ \ 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 \mbox{@{text "\ \ x"}}. Let us call - a variable @{text x} \emph{really free}, if it is free and not occuring - in an @{term unpermute}, such as @{text "unpermute _ x"} and @{text "unpermute x _"}. - We need the following technical notion characterising \emph{@{text "\"}-proper} HOL-terms - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}ll} - $\bullet$ & variables and constants are @{text \}-proper,\\ - $\bullet$ & @{term "unpermute \ x"} is @{text \}-proper,\\ - $\bullet$ & @{term "\x. t"} is @{text \}-proper, if @{text t} is @{text \}-proper and @{text x} is - really free in @{text t}, and\\ - $\bullet$ & @{term "t\<^isub>1 t\<^isub>2"} is @{text \}-proper, if @{text "t\<^isub>1"} and @{text "t\<^isub>2"} are - @{text \}-proper. - \end{tabular} - \end{isabelle} - - \begin{proof}[Theorem~\ref{eqvtprin}] We establish the property if @{text t} - is @{text \}-proper and only contains equivaraint constants, then - @{text "\ \ t = t'"} where @{text "t'"} is equal to @{text "t"} except all really - free variables @{text x} are replaced by @{text "\ \ x"}, and all semi-free variables - @{text "unpermute \ x"} by @{text "x"}. We establish this property by induction - on the size of HOL-terms, counting terms like @{text "unpermuting \ x"} as leafes, - like variables and constants. The cases for variables, constants and @{text unpermutes} - are routine. In the case of abstractions we have by induction hypothesis that - @{text "\ \ (t[x := unpermute \ x]) = t'"} with @{text "t'"} satisfying our - correctness property. This implies that @{text "\x. \ \ (t[x := unpermute \ x]) = \x. t'"} - and hence @{text "\ \ (\x. t) = \x. t'"} as needed.\hfill\qed - \end{proof} - - Pitts calls this property \emph{equivariance principle} (book ref ???). - - Problems with @{text undefined} - - Lines of code -*} - - -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] \label{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 - Using the equivariance principle, it can be easily checked that all three notions - are equivariant. A simple consequence of the definition of support and equivariance - is that if @{text x} is equivariant then we have - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}l} - @{thm (concl) supp_fun_eqvt[where f="x", no_vars]} - \end{tabular}\hfill\numbered{suppeqvtfun} - \end{isabelle} - - \noindent - For function applications we can establish the following two properties. - - \begin{lemma}\label{suppfunapp} Let @{text f} and @{text x} be of permutation type, then - \begin{isabelle} - \begin{tabular}{r@ {\hspace{4mm}}p{10cm}} - {\it i)} & @{thm[mode=IfThen] fresh_fun_app[no_vars]}\\ - {\it ii)} & @{thm supp_fun_app[no_vars]}\\ - \end{tabular} - \end{isabelle} - \end{lemma} - - \begin{proof} - For the first property, we know from the assumption that @{term - "finite {b. (a \ b) \ f \ f}"} and @{term "finite {b . (a \ b) \ x \ - x}"} hold. That means for all, but finitely many @{text b} we have - @{term "(a \ b) \ f = f"} and @{term "(a \ b) \ x = x"}. Similarly, - we have to show that for but, but finitely @{text b} the equation - @{term "(a \ b) \ f x = f x"} holds. The left-hand side of this - equation is equal to @{term "((a \ b) \ f) ((a \ b) \ x)"} by - \eqref{permutefunapp}, which we know by the previous two facts for - @{text f} and @{text x} is equal to the right-hand side for all, - but finitely many @{text b}. This establishes the first - property. The second is a simple corollary of {\it i)} by - unfolding the definition of freshness.\qed - \end{proof} - - A striking consequence of the definitions for support and freshness - 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}.\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 \ c) \ x \ x}"} and @{term "finite {c. (b \ c) \ x \ 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 \ c) \ x = x"}} and @{term "(b \ c) \ x = x"}. - Now the theorem follows from Lemma~\ref{swaptriple}.\hfill\qed - \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 concrete objects. - For booleans, nats, products and lists it is easy to check that - - \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 - hold. 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 \ b) \ 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 \ S'"}. - \end{tabular} - \end{isabelle} - \end{lemma} - - \begin{proof} - For {\it i)} we derive a contradiction by assuming there is an atom @{text a} - with @{term "a \ supp x"} and @{text "a \ S"}. Using the second fact, the - assumption that @{term "S supports x"} gives us that @{text S} is a superset of - @{term "{b. (a \ b) \ x \ x}"}, which is finite by the assumption of @{text S} - being finite. But this means @{term "a \ supp x"}, contradicting our assumption. - Property {\it ii)} is by a direct application of - Theorem~\ref{swapfreshfresh}. For the last property, part {\it i)} proves - one ``half'' of the claimed equation. The other ``half'' is by property - {\it ii)} and the fact that @{term "supp x"} is finite by {\it 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 {\it 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 \ S"} and all @{text "b \ S"}, with @{text a} - and @{text b} having the same sort, \mbox{@{term "(a \ b) \ x \ 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 \ 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 \ S"} and @{text "b \ S'"}. Since we assumed @{text "a \ S'"} and - we have that @{text "S' supports x"}, we have on one hand @{term "(a \ b) \ x - = x"}. On the other hand, the fact @{text "a \ S"} and @{text "b \ S"} imply - @{term "(a \ b) \ x \ 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 "\a \ {c} b \ {c}. sort a = sort b \ (a b) \ c \ 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="\", 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 \ \ a \ a, \ \ b = b and sort a = sort b, then (a b) \ \ \ \"}. - \end{tabular} - \end{isabelle} - - \noindent - For this we observe that - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}rcl} - @{thm (lhs) perm_swap_eq[where p="\", no_vars]} & - if and only if & - @{thm (rhs) perm_swap_eq[where p="\", 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 "(\ \ a \ b)"} and @{term "(a \ 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 a crucial 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 in Isabelle/HOL corresponding to the - property: - - \begin{definition}[Finitely Supported Type] - A type @{text "\"} is \emph{finitely supported} if @{term "finite (supp x)"} - holds for all @{text x} of type @{text "\"}. - \end{definition} - - \noindent - By the calculations above we can easily establish - - \begin{theorem}\label{finsuptype} - The types @{type atom}, @{type perm}, @{type bool} and @{type nat} - are fintitely supported, and assuming @{text \}, @{text "\\<^isub>1"} and - @{text "\\<^isub>2"} are finitely supported types, then @{text "\ list"} and - @{text "\\<^isub>1 \ \\<^isub>2"} are finitely supported. - \end{theorem} - - \noindent - The main benefit of using the finite support property for choosing a - fresh atom is that the reasoning is `compositional'. To see this, - assume we have a list of atoms and a method of choosing a fresh atom - that is not a member in this list---for example the maximum plus - one. Then if we enlarge this list \emph{after} the choice, then - obviously the fresh atom might not be fresh anymore. In contrast, by - the classical reasoning of Proposition~\ref{choosefresh} we know a - fresh atom exists for every list of atoms and no matter how we - extend this list of atoms, we always preserve the property of being - finitely supported. Consequently the existence of a fresh atom is - still guarantied by Proposition~\ref{choosefresh}. Using the method - of `maximum plus one' we might have to adapt the choice of a fresh - atom. - - Unfortunately, Theorem~\ref{finsuptype} does not work in general for the - types of sets and functions. There are functions definable in 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 "\ a \ nat_of"}. This is equivalent to assuming the set - @{term "{b. (a \ b) \ nat_of \ nat_of}"} is finite and deriving a - contradiction. From the assumption we also know that @{term "{a} \ - {b. (a \ b) \ nat_of \ nat_of}"} is finite. Then we can use - Proposition~\ref{choosefresh} to choose an atom @{text c} such that - @{term "c \ a"}, @{term "sort_of c = sort_of a"} and @{term "(a \ c) - \ 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 \ c) \ (nat_of a)"} & by def.~of permutations on nats\\ - & @{text "="} & @{term "((a \ c) \ nat_of) ((a \ c) \ 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 \ 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 an 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. Their support can be characterised as: - - \begin{lemma}\label{finatomsets} - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}[b]{@ {}rl} - {\it i)} & If @{text S} is a finite set of atoms, then @{thm (concl) supp_finite_atom_set[no_vars]}.\\ - {\it ii)} & If @{term "UNIV - (S::atom set)"} is a finite set of atoms, then - @{thm (concl) supp_cofinite_atom_set[no_vars]}. - \end{tabular} - \end{isabelle} - \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 supports 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 - % - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}[b]{@ {}rl} - {\it i)} & @{thm (concl) Union_of_finite_supp_sets[no_vars]} and\\ - {\it ii)} & @{thm (concl) Union_included_in_supp[no_vars]}. - \end{tabular} - \end{isabelle} - \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 "\x\S. supp - x"} is a set of atoms, which by the first part is finite. Therefore - we know by Lemma~\ref{finatomsets}.{\it i)} that @{term "(\x\S. supp - x) = supp (\x\S. supp x)"}. Taking @{text "f"} to be the function - \mbox{@{text "\S. \ (supp ` S)"}}, we can write the right-hand side - as @{text "supp (f S)"}. Since @{text "f"} is an equivariant - function (can be easily checked by the equivariance principle), we - have that @{text "supp (f S) \ supp S"} by - Lemma~\ref{suppfunapp}.{\it ii)}. 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}.{\it ii)}. To show the inclusion - in the other direction we can use Lemma~\ref{supports}.{\it i)}. This means - for all @{text a} and @{text b} that are not in @{text S} we have to show that - @{term "(a \ b) \ (\x \ S. supp x) = (\x \ S. supp x)"} holds. By the equivariance - principle, the left-hand side is equal to @{term "\x \ ((a \ b) \ S). supp x"}. Now - the swapping in front of @{text S} disappears, since @{term "a \ S"} and @{term "b \ S"} - whenever @{text "a, b \ S"}. Thus we are done.\hfill\qed - \end{proof} - - \noindent - To sum up, every finite set of finitely supported elements has - finite support. Unfortunately, we cannot use - Theorem~\ref{finsuptype} to let Isabelle/HOL find this out - automatically. This would require to introduce a separate type of - finite sets, which however is not so convenient to reason about as - Isabelle's standard set type. -*} - - -section {* Induction Principles for Permutations *} - -text {* - While the use of functions as permutation provides us with a unique - representation for permutations (for example @{term "(a \ b)"} and - @{term "(b \ a)"} are equal permutations), this representation does - not come automatically with an induction principle. Such an - induction principle is however useful for generalising - Lemma~\ref{swapfreshfresh} from swappings to permutations, namely - - \begin{lemma} - @{thm [mode=IfThen] perm_supp_eq[where p="\", no_vars]} - \end{lemma} - - \noindent - In this section we will establish an induction principle for permutations - with which this lemma can be easily proved. It is not too difficult to derive - an induction principle for permutations, given the fact that we allow only - permutations having a finite support. - - Using a the property from \cite{???} - - \begin{lemma}\label{smallersupp} - @{thm [mode=IfThen] smaller_supp[where p="\", no_vars]} - \end{lemma} -*} - - -section {* An Abstraction Type *} - -text {* - To that end, we will consider - first pairs @{text "(as, x)"} of type @{text "(atom set) \ \"}. 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 "\ \ 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) \set R fa p (bs, y)"}\hspace{2mm}@{text "\"}}\\[1mm] - & @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\ - @{text "\"} & @{term "(fa(x) - as) \* p"} & \mbox{\it (ii)}\\ - @{text "\"} & @{text "(p \ x) R y"} & \mbox{\it (iii)}\\ - @{text "\"} & @{term "(p \ 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 \ T\<^isub>2) = fa(T\<^isub>1) \ 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 \ y)"} and - @{text "({y, x}, y \ x)"} are $\alpha$-equivalent according to - $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{res}}$ by taking @{text p} to - be the swapping @{term "(x \ y)"}. In case of @{text "x \ y"}, then @{text - "([x, y], x \ y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \ 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 \ 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 \ 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) \ \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 \ as, p \ x) (p \ - bs, p \ 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 "\ abs_set"}, @{text "\ abs_res"} and @{text "\ abs_list"} - representing $\alpha$-equivalence classes of pairs of type - @{text "(atom set) \ \"} (in the first two cases) and of type @{text "(atom list) \ \"} - (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 \ b) \ (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 \ (supp x - as) = - (supp (p \ x)) - (p \ as)"}) and therefore has empty support. - This in turn means - % - \begin{center} - @{term "supp (supp_gen (Abs_set as x)) \ 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. - - 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 for example that subgoals involving sorts must be discharged explicitly within proof - scripts, instead of being inferred automatically. 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 \ b) \ (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\ 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 "\_\ :: name \ atom"} & - @{text "\_\ :: atom \ name"} - \end{tabular} - \end{isabelle} - - \noindent - With the definition @{thm permute_name_def [where p="\", 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="\", 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 is to let users - avoid explicit reasoning about sorts. This benefit is realised by defining a - special swapping operation of type @{text "\ \ \ - \ perm"}, where @{text "\"} 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 "\"}-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 "\"} 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 \ b) \ (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. - -*} - - - -section {* Related Work\label{related} *} - -text {* - Coq-tries, but failed - - Add here comparison with old work. - - 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. - - 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] "_ \ _ :: (\ \ \) list \ \ \ \"} - - \noindent - where @{text "\"} stands for a type of atoms and @{text "\"} 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 "[] \ c"} & @{text "="} & @{text c}\\ - @{text "(a b)::\ \ c"} & @{text "="} & - $\begin{cases} @{text a} & \textrm{if}~@{text "\ \ c = b"}\\ - @{text b} & \textrm{if}~@{text "\ \ c = a"}\\ - @{text "\ \ 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 "\ \ c \ 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] "\\\<^isub>1 \ \\\<^isub>n. \"} - - \noindent - where the @{text "\\<^isub>i"} are of type @{text "(\\<^isub>i \ \\<^isub>i) list"}. - The reason is that the permutation operation behaves differently for - every @{text "\\<^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 _ :: \ \ \ 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 - "\\<^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) :: \\<^isub>1 set) , \, finite ((supp x) :: \\<^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 "\\<^isub>1 \ \\<^isub>2 \ \a. \\<^isub>1 \ a = \\<^isub>2 \ 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 "[] \ x = x"}\\ - ii) & @{text "(\\<^isub>1 @ \\<^isub>2) \ x = \\<^isub>1 \ (\\<^isub>2 \ x)"}\\ - iii) & if @{text "\\<^isub>1 \ \\<^isub>2"} then @{text "\\<^isub>1 \ x = \\<^isub>2 \ 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 \}, then we only have to state @{term "\\. P (\ \ 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 "\a \ supp x. a \ p"} implies @{term "p \ 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 -(*>*) \ No newline at end of file