nominal2: comparison Pearl-jv/Paper.thy

equal deleted inserted replaced

-:61d30863e5d1
+:a9e63abf3feb
 section {* Introduction *}
 text {*
 Nominal Isabelle provides a proving infratructure for convenient reasoning
-about programming language calculi involving binders, such as lambda abstractions or
+about syntax involving binders, such as lambda terms or type schemes:
-quantifications in type schemes:
+\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+@{text "\<lambda>x. t       \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. \<tau>"}
-@{text "\<lambda>x. t       \<forall>{x\<^isub>1,\<dots>,x\<^isub>n}. \<tau>"}
 \hfill\numbered{atomperm}
 \end{isabelle}
 \noindent
 At its core Nominal Isabelle is based on the nominal logic work by Pitts at
 al \cite{GabbayPitts02,Pitts03}, 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
+collection of sorted atoms. The atoms are used for representing variable names
-point for a number of formalisations, most notable Norrish \cite{norrish04}
+that might be bound or free. Multiple sorts are necessary for being able to
-in HOL4, Aydemir et al \cite{AydemirBohannonWeirich07} in Coq and our own
+represent different kinds of variables. For example, in the language Mini-ML
-work in Isabelle/HOL.
+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 "_ \<bullet> _"}, 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 "\<Gamma>"} of the form
+\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+@{text "x\<^isub>1:\<tau>\<^isub>1, \<dots>, x\<^isub>n:\<tau>\<^isub>n"}
+\end{isabelle}
+\noindent
+is said to be \emph{valid} provided none of its variables, or atoms, @{text "x\<^isub>i"}
+occur twice. Then validity is preserved under
+permutations in the sense that if @{text \<Gamma>} is valid then so is @{text "\<pi> \<bullet> \<Gamma>"} for
+all permutations @{text "\<pi>"}. This is \emph{not} the case for arbitrary
+renaming substitutions, as they might identify some variables in @{text \<Gamma>}.
+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 "\<forall>\<pi>. \<pi> \<bullet> 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
 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
 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
+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
+collection of sorted atoms.
-that might be bound or free. Multiple sorts are necessary for being able to
-represent different kinds of variables. For example, in the language Mini-ML
-there are bound term variables in lambda abstractions and bound type variables in
-type schemes. In order to be able to separate them, each kind of variables needs to be
-represented by a different sort of atoms.
 The existing nominal logic work usually leaves implicit the sorting
 information for atoms and as far as we know leaves out a description of how
 sorts are represented.  In our formalisation, we therefore have to make a
 design decision about how to implement sorted atoms and sort-respecting
 permutations. One possibility, which we described in \cite{Urban08}, is to
-have separate types for the different
+have separate types for the different kinds of atoms, say types @{text
-kinds of atoms, say types @{text "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}.
+"\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}. However, this does not blend well with the
+resoning infrastructure of type-classes in Isabelle/HOL (see Section ???
-In the nominal logic work of Pitts, binders and bound variables are
+about related work).  Therefore we use here a single unified atom type to
-represented by \emph{atoms}.  As stated above, we need to have different
+represent atoms of different sorts. A basic requirement is that there must
-\emph{sorts} of atoms to be able to bind different kinds of variables.  A
+be a countably infinite number of atoms of each sort.  This can be
-basic requirement is that there must be a countably infinite number of atoms
+implemented as the datatype
-of each sort.  We implement these atoms as
 *}
 datatype atom\<iota> = Atom\<iota> string nat
 text {*
 \noindent
 whereby the string argument specifies the sort of the atom.\footnote{A
 similar design choice was made by Gunter et al \cite{GunterOsbornPopescu09}
-for their variables.}  (The use of type \emph{string} is merely for
+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
+convenience; any countably infinite type would work as well. We have an
-auxiliary function @{text sort} that is defined as @{thm
+auxiliary function @{text sort} that is defined as
-sort_of.simps[no_vars]}, and we clearly have for every finite set @{text X}
+\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 \<notin> S"}.
 \end{proposition}
 For implementing sort-respecting permutations, we use functions of type @{typ
 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
+convenient to actually allow the user to state `ill-sorted' swappings but
-limit their ``damage'' by defaulting to the identity permutation in the
+limit their `damage' by defaulting to the identity permutation in the
 ill-sorted case:
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \begin{tabular}{@ {}rl}
 @{text "(a b) \<equiv>"} & @{text "if (sort a = sort b)"}\\
 \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
+One advantage of using functions 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
+are \emph{equal}.  Therfore we can use for permutations HOL's built-in
-in~\eqref{permequ} to identify them, as we would if they had been represented
+principle of `replacing equals by equals in any context'. Another advantage
-as lists of pairs.  Another advantage of the function representation is that
+of the function representation is that they form a (non-commutative) group
-they form a (non-commutative) group provided we define
+provided we define
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
-@{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm}
+@{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{5mm}
-@{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{4mm}
+@{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{5mm}
-@{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{4mm}
+@{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{5mm}
 @{thm minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^isub>2"]}
 \end{tabular}
 \end{isabelle}
 \noindent
 and verify the simple properties
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
-@{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]} \hspace{3mm}
+@{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]} \hspace{5mm}
-@{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{3mm}
+@{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{5mm}
-@{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{3mm}
+@{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{5mm}
 @{thm group_add_class.left_minus[where a="\<pi>::perm"]}
 \end{tabular}
 \end{isabelle}
 \noindent
-Again this is in contrast to the list-of-pairs representation which does not
+The technical importance of this fact is that we can rely on
-form a group.  The technical importance of this fact is that we can rely on
 Isabelle/HOL's existing simplification infrastructure for groups, which will
 come in handy when we have to do calculations with permutations.
 Note that Isabelle/HOL defies standard conventions of mathematical notation
 by using additive syntax even for non-commutative groups.  Obviously,
 composition of permutations is not commutative in general, because @{text
 "\<pi>\<^sub>1 + \<pi>\<^sub>2 \<noteq>  \<pi>\<^sub>2 + \<pi>\<^sub>1"}.  But since the point of this paper is to implement the
 nominal theory as smoothly as possible in Isabelle/HOL, we tolerate
 the non-standard notation in order to reuse the existing libraries.
-By formalising permutations abstractly as functions, and using a single type
+In order to reason abstractly about permutations, we state the following two
-for all atoms, we can now restate the \emph{permutation properties} from
+\emph{permutation properties}
-\eqref{permprops} as just the two equations
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
 i) & @{thm permute_zero[no_vars]}\\
 ii) & @{thm permute_plus[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2",no_vars]}
 \end{tabular}\hfill\numbered{newpermprops}
 \end{isabelle}
 \noindent
-in which the permutation operations are of type @{text "perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} and so
+We state these properties in terms of Isabelle/HOL's type class
-have only a single type parameter.  Consequently, these properties are
+mechanism \cite{}.
-compatible with the one-parameter restriction of Isabelle/HOL's type classes.
+This allows us to delegate much of the resoning involved in
-There is no need to introduce a separate type class instantiated for each
+determining whether these properties are satisfied to the type system.
-sort, like in the old approach.
+For this we define
-The next notion allows us to establish generic lemmas involving the
-permutation operation.
 \begin{definition}
 A type @{text "\<beta>"} is a \emph{permutation type} if the permutation
 properties in \eqref{newpermprops} are satisfied for every @{text "x"} of type
 @{text "\<beta>"}.
 \end{definition}
 \noindent
-First, it follows from the laws governing
+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:
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 @{thm permute_minus_cancel(2)[where p="\<pi>", no_vars]}
 \end{tabular}\hfill\numbered{cancel}
 \end{isabelle}
 \noindent
+??? Proof
 Consequently, in a permutation type the permutation operation @{text "\<pi> \<bullet> _"}~~is bijective,
 which in turn implies the property
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 \noindent
 In order to lift the permutation operation to other types, we can define for:
 \begin{equation}\label{permdefs}
 \mbox{
-\begin{tabular}{@ {}ll@ {\hspace{2mm}}l@ {}}
+\begin{tabular}{@ {}ll@ {\hspace{4mm}}l@ {}}
-1) & atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\
+a) & atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\
-2) & functions: &  @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\
+b) & functions: &  @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\
-3) & permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\
+c) & permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\
-4) & sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+d) & sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-5) & booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+e) & booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-6) & lists: & @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+f) & lists: & @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
 & & @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-7) & products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+g) & products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-8) & nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+h) & nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
 \end{tabular}}
 \end{equation}
 \noindent
 and then establish:

changeset 2740	a9e63abf3feb
parent 2736	61d30863e5d1
child 2742	f1192e3474e0