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