diff -r 61d30863e5d1 -r a9e63abf3feb Pearl-jv/Paper.thy --- a/Pearl-jv/Paper.thy Wed Mar 02 00:06:28 2011 +0000 +++ b/Pearl-jv/Paper.thy Tue Mar 08 09:07:27 2011 +0000 @@ -44,11 +44,10 @@ text {* Nominal Isabelle provides a proving infratructure for convenient reasoning - about programming language calculi involving binders, such as lambda abstractions or - quantifications in type schemes: + about syntax involving binders, such as lambda terms or type schemes: \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - @{text "\x. t \{x\<^isub>1,\,x\<^isub>n}. \"} + @{text "\x. t \{x\<^isub>1,\, x\<^isub>n}. \"} \hfill\numbered{atomperm} \end{isabelle} @@ -56,12 +55,59 @@ 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 nominal logic work has been starting - point for a number of formalisations, most notable Norrish \cite{norrish04} - in HOL4, Aydemir et al \cite{AydemirBohannonWeirich07} in Coq and our own - work in Isabelle/HOL. + collection of sorted atoms. The atoms are used for representing variable names + that might be bound or free. Multiple sorts are necessary for being able to + represent different kinds of variables. For example, in the language Mini-ML + there are bound term variables in lambda abstractions and bound type variables in + type schemes. In order to be able to separate them, each kind of variables needs to be + represented by a different sort of atoms. + + The 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 teh 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 and even functions. The notion of support + is derived from the permutation operation defined over atoms. This + permutation operation, written @{text "_ \ _"}, has proved to be very + convenient for reasoning about syntax, in comparison to, say, arbitrary + renaming substitutions of atoms. The 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 exist in general, since renaming substitutions are only injective. + Permutations also preserve many constructions when reasoning about syntax. + For example validity of a typing context is preserved under permutations. + 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 is preserved under + permutations in the sense that if @{text \} is valid then so is @{text "\ \ \"} for + all permutations @{text "\"}. This is \emph{not} the case for arbitrary + renaming substitutions, as they might identify some variables in @{text \}. + Permutations fit well with HOL's definitions. For example + + Because + of the good properties of permutations, we will be able to automate reasoning + steps determining when a construction in HOL is + \emph{equivariant}. By equivariance we mean the property that every + permutation leaves an object unchanged, that is @{term "\\. \ \ x = x"}. + This will often simplify arguments involving the notion of support. + + + There are a number of subtle differences between the nominal logic work by Pitts + and the one we will present in this paper. Nominal + + In the nominal logic work, the `new quantifier' plays a prominent role. + + + 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 @@ -74,34 +120,30 @@ depend on type annotations. The paper is organised as follows\ldots + + + Two binders *} section {* Sorted Atoms and Sort-Respecting Permutations *} text {* - The most basic notion in this work is a + The two most basic notions in the nominal logic work are sort-respecting permutation operation defined over a countably infinite - collection of sorted atoms. The atoms are used for representing variable names - that might be bound or free. Multiple sorts are necessary for being able to - represent different kinds of variables. For example, in the language Mini-ML - there are bound term variables in lambda abstractions and bound type variables in - type schemes. In order to be able to separate them, each kind of variables needs to be - represented by a different sort of atoms. - - + collection of sorted atoms. The existing nominal logic work usually leaves implicit the sorting information for atoms and as far as we know leaves out a description of how sorts are represented. In our formalisation, we therefore have to make a design decision about how to implement sorted atoms and sort-respecting - permutations. One possibility, which we described in \cite{Urban08}, is to - have separate types for the different - kinds of atoms, say types @{text "\\<^isub>1,\,\\<^isub>n"}. + permutations. One possibility, which we described in \cite{Urban08}, is to + have separate types for the different kinds of atoms, say types @{text + "\\<^isub>1,\,\\<^isub>n"}. However, this does not blend well with the + resoning infrastructure of type-classes in Isabelle/HOL (see Section ??? + about related work). Therefore we use here a single unified atom type to + represent atoms of different sorts. A basic requirement is that there must + be a countably infinite number of atoms of each sort. This can be + implemented as the datatype - In the nominal logic work of Pitts, binders and bound variables are - represented by \emph{atoms}. As stated above, we need to have different - \emph{sorts} of atoms to be able to bind different kinds of variables. A - basic requirement is that there must be a countably infinite number of atoms - of each sort. We implement these atoms as *} datatype atom\ = Atom\ string nat @@ -110,13 +152,19 @@ \noindent whereby the string argument specifies the sort of the atom.\footnote{A similar design choice was made by Gunter et al \cite{GunterOsbornPopescu09} - for their variables.} (The use of type \emph{string} is merely for - convenience; any countably infinite type would work as well.) We have an - auxiliary function @{text sort} that is defined as @{thm - sort_of.simps[no_vars]}, and we clearly have for every finite set @{text X} + for their variables.} The use of type \emph{string} for sorts is merely for + convenience; any countably infinite type would work as well. We have an + auxiliary function @{text sort} that is defined as + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + @{thm sort_of.simps[no_vars, THEN eq_reflection]} + \end{isabelle} + + \noindent + and we clearly have for every finite set @{text S} of atoms and every sort @{text s} the property: - \begin{proposition}\label{choosefresh} + \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} @@ -174,8 +222,8 @@ 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 + 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}\ \ \ \ \ \ \ \ \ \ %%% @@ -191,7 +239,7 @@ @{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 + One advantage of using functions as a representation for permutations is that for example the swappings \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% @@ -202,16 +250,17 @@ \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 + are \emph{equal}. Therfore we can use for permutations HOL's built-in + principle of `replacing equals by equals in any context'. 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 zero_perm_def[no_vars, THEN eq_reflection]} \hspace{5mm} + @{thm plus_perm_def[where p="\\<^isub>1" and q="\\<^isub>2", THEN eq_reflection]} \hspace{5mm} + @{thm uminus_perm_def[where p="\", THEN eq_reflection]} \hspace{5mm} @{thm minus_perm_def[where ?p1.0="\\<^isub>1" and ?p2.0="\\<^isub>2"]} \end{tabular} \end{isabelle} @@ -221,16 +270,15 @@ \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 add_assoc[where a="\\<^isub>1" and b="\\<^isub>2" and c="\\<^isub>3"]} \hspace{5mm} + @{thm monoid_add_class.add_0_left[where a="\::perm"]} \hspace{5mm} + @{thm monoid_add_class.add_0_right[where a="\::perm"]} \hspace{5mm} @{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 + 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 @@ -240,9 +288,8 @@ 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 + In order to reason abstractly about permutations, we state the following two + \emph{permutation properties} \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}} @@ -252,14 +299,11 @@ \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. + We state these properties in terms of Isabelle/HOL's type class + mechanism \cite{}. + This allows us to delegate much of the resoning involved in + determining whether these properties are satisfied to the type system. + For this we define \begin{definition} A type @{text "\"} is a \emph{permutation type} if the permutation @@ -268,7 +312,8 @@ \end{definition} \noindent - First, it follows from the laws governing + The type class also allows us to establish generic lemmas involving the + permutation operation. 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: @@ -281,6 +326,7 @@ \end{isabelle} \noindent + ??? Proof Consequently, in a permutation type the permutation operation @{text "\ \ _"}~~is bijective, which in turn implies the property @@ -316,16 +362,16 @@ \begin{equation}\label{permdefs} \mbox{ - \begin{tabular}{@ {}ll@ {\hspace{2mm}}l@ {}} - 1) & atoms: & @{thm permute_atom_def[where p="\",no_vars, THEN eq_reflection]}\\ - 2) & functions: & @{text "\ \ f \ \x. \ \ (f ((-\) \ x))"}\\ - 3) & permutations: & @{thm permute_perm_def[where p="\" and q="\'", THEN eq_reflection]}\\ - 4) & sets: & @{thm permute_set_eq[where p="\", no_vars, THEN eq_reflection]}\\ - 5) & booleans: & @{thm permute_bool_def[where p="\", no_vars, THEN eq_reflection]}\\ - 6) & lists: & @{thm permute_list.simps(1)[where p="\", no_vars, THEN eq_reflection]}\\ + \begin{tabular}{@ {}ll@ {\hspace{4mm}}l@ {}} + a) & atoms: & @{thm permute_atom_def[where p="\",no_vars, THEN eq_reflection]}\\ + b) & functions: & @{text "\ \ f \ \x. \ \ (f ((-\) \ x))"}\\ + c) & permutations: & @{thm permute_perm_def[where p="\" and q="\'", THEN eq_reflection]}\\ + d) & sets: & @{thm permute_set_eq[where p="\", no_vars, THEN eq_reflection]}\\ + e) & booleans: & @{thm permute_bool_def[where p="\", no_vars, THEN eq_reflection]}\\ + f) & 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]}\\ - 7) & products: & @{thm permute_prod.simps[where p="\", no_vars, THEN eq_reflection]}\\ - 8) & nats: & @{thm permute_nat_def[where p="\", no_vars, THEN eq_reflection]}\\ + g) & products: & @{thm permute_prod.simps[where p="\", no_vars, THEN eq_reflection]}\\ + h) & nats: & @{thm permute_nat_def[where p="\", no_vars, THEN eq_reflection]}\\ \end{tabular}} \end{equation}