nominal2: comparison Pearl-jv/Paper.thy

equal deleted inserted replaced

-:0cb0c88b2cad
+:e903c32ec24f
 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
 section {* Introduction *}
 text {*
 Nominal Isabelle provides a proving infratructure for convenient reasoning
-about programming languages involving binders such as lambda abstractions or
+about programming language calculi involving binders such as lambda abstractions or
 quantifications in type schemes:
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 @{text "\<lambda>x. t       \<forall>{x\<^isub>1,\<dots>,x\<^isub>n}. \<tau>"}
 \hfill\numbered{atomperm}
 \noindent
 At its core Nominal Isabelle is based on the nominal logic work by Pitts at
 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 variable names
-that might be binding, bound or free. Multiple sorts are necessary for being able to
+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.
-In our formalisation of the nominal logic work, we have to make a design decision
+The existing nominal logic work usually leaves implicit the sorting
-about how to represent sorted atoms and sort-respecting permutations. One possibility
+information for atoms and as far as we know leaves out a description of how
-is to have separate types for the different kinds of atoms, say @{text "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}.
+sorts are represented.  In our formalisation, we therefore have to make a
-With this design one can represent
+design decision about how to implement sorted atoms and sort-respecting
-permutations as lists of pairs of atoms and the operation of applying
+permutations. One possibility, which we described in \cite{Urban08}, is to
-a permutation to an object as the overloaded function
+have separate types for the different
+kinds of atoms, say types @{text "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}. With this
+design one can represent permutations as lists of pairs of atoms and the
+operation of applying a permutation to an object as the function
 @{text [display,indent=10] "_ \<bullet> _  ::  (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
 \noindent
 where @{text "\<alpha>"} stands for a type of atoms and @{text "\<beta>"} for the type
 \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
+@{text "b"}. For atoms with different type than the permutation, we
-is defined as @{text "\<pi> \<bullet> c \<equiv> c"}.
+define @{text "\<pi> \<bullet> c \<equiv> c"}.
 With the separate atom types and the list representation of permutations it
 is impossible in systems like Isabelle/HOL to state an ``ill-sorted''
 permutation, since the type system excludes lists containing atoms of
 different type. However, a disadvantage is that whenever we need to
 @{text [display,indent=10] "\<forall>\<pi>\<^isub>1 \<dots> \<forall>\<pi>\<^isub>n. \<dots>"}
 \noindent
 where the @{text "\<pi>\<^isub>i"} are of type @{text "(\<alpha>\<^isub>i \<times> \<alpha>\<^isub>i) list"}.
 The reason is that the permutation operation behaves differently for
-every @{text "\<alpha>\<^isub>i"}. Similarly, the notion of support
+every @{text "\<alpha>\<^isub>i"} and the type system does not allow use to have a
+single quantification to stand for all permutations. Similarly, the
+notion of support
 @{text [display,indent=10] "supp _ :: \<beta> \<Rightarrow> \<alpha> set"}
 \noindent
 which we will define later, cannot be
 @{text "finite ((supp x) :: \<alpha>\<^isub>1 set) , \<dots>, finite ((supp x) :: \<alpha>\<^isub>n set)"}
 \end{tabular}\hfill\numbered{fssequence}
 \end{isabelle}
 \noindent
-Because of these disadvantages, we will use a single unified atom type to
+Because of these disadvantages, we will use in this paper a single unified atom type to
-represent atoms of different sorts. As a result, we have to deal with the
+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.  An
+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. Another advantage is that there is a well-understood
+list reversal, and another advantage is that there is a well-understood
-induction principle for lists. A disadvantage, however, is that permutations
+induction principle for lists, a disadvantage is that permutations
-do not have unique representations as lists; we have to explicitly identify
+do not have unique representations as lists. We have to explicitly identify
 them according to the relation
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 \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, we need to ensure that every definition
+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:
 \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
+to produce the same result for related permutations.  Moreover,
-as list do not satisfy the usual properties about groups. This means by
+``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.  Therefore, we will use
+reasoning infrastructure in Isabelle about groups.  Because of this, we will represent
-in this paper a unique representation for permutations by representing them
+in this paper permutations as functions from atoms to atoms. This representation
-as functions from atoms to atoms.
+is unique and satisfies the laws of non-commutative groups.
 Using a single atom type to represent atoms of different sorts and
-representing permutations as functions are not new ideas.  The main
+representing permutations as functions are not new ideas; see
-contribution of this paper is to show an example of how to make better
+\cite{GunterOsbornPopescu09} \footnote{function rep.}  The main contribution
-theorem proving tools by choosing the right level of abstraction for the
+of this paper is to show an example of how to make better theorem proving
-underlying theory---our design choices take advantage of Isabelle's type
+tools by choosing the right level of abstraction for the underlying
-system, type classes and reasoning infrastructure.  The novel technical
+theory---our design choices take advantage of Isabelle's type system, type
-contribution is a mechanism for dealing with ``Church-style'' lambda-terms
+classes and reasoning infrastructure.  The novel technical contribution is a
-\cite{Church40} and HOL-based languages \cite{PittsHOL4} where variables and
+mechanism for dealing with ``Church-style'' lambda-terms \cite{Church40} and
-variable binding depend on type annotations.
+HOL-based languages \cite{PittsHOL4} where variables and variable binding
+depend on type annotations.
-The paper is organised as follows
+The paper is organised as follows\ldots
 *}
 section {* Sorted Atoms and Sort-Respecting Permutations *}
 text {*
 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
+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}
 of atoms and every sort @{text s} the property:
 @{thm permute_minus_cancel(2)[where p="\<pi>", no_vars]}
 \end{tabular}\hfill\numbered{cancel}
 \end{isabelle}
 \noindent
-Consequently, in a permutation type the permutation operation @{text "\<pi> \<bullet> _"} is bijective,
+Consequently, in a permutation type the permutation operation @{text "\<pi> \<bullet> _"}~~is bijective,
 which in turn implies the property
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm (lhs) permute_eq_iff[where p="\<pi>", no_vars]}
 @{thm (rhs) permute_eq_iff[where p="\<pi>", no_vars]}.
 \end{tabular}\hfill\numbered{permuteequ}
 \end{isabelle}
 \noindent
+We can also show that the following property holds for any permutation type.
+\begin{lemma}\label{permutecompose}
+Given @{term x} is of permutation type, then
+@{text "\<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x) = (\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}.
+\end{lemma}
+\begin{proof} The proof is as follows:
+\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+\begin{tabular}[b]{@ {}rcl@ {\hspace{8mm}}l}
+@{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> x"}
+& @{text "="} & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> (-\<pi>\<^isub>1) \<bullet> \<pi>\<^isub>1 \<bullet> x"} & by \eqref{cancel}\\
+& @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2 - \<pi>\<^isub>1) \<bullet> \<pi>\<^isub>1 \<bullet> x"}  & by {\rm(\ref{newpermprops}.@{text "ii"})}\\
+& @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}\\
+\end{tabular}\hfill\qed
+\end{isabelle}
+\end{proof}
+\noindent
 In order to lift the permutation operation to other types, we can define for:
-\begin{isabelle}
+\begin{equation}\label{permdefs}
-\begin{tabular}{@ {}c@ {\hspace{-1mm}}c@ {}}
+\mbox{
-\begin{tabular}{@ {}r@ {\hspace{2mm}}l@ {}}
+\begin{tabular}{@ {}ll@ {\hspace{2mm}}l@ {}}
-atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\
+1) & atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\
-functions: &  @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\
+2) & functions: &  @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\
-permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\
+3) & permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\
-sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+4) & sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+5) & booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-\end{tabular} &
+6) & lists: & @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-\begin{tabular}{@ {}r@ {\hspace{2mm}}l@ {}}
+& & @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-lists: & @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+7) & products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-& @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\[2mm]
+8) & nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+\end{tabular}}
-nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+\end{equation}
-\end{tabular}
-\end{tabular}
-\end{isabelle}
 \noindent
 and then establish:
 \begin{theorem}
 & @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) + \<pi>' - \<pi>\<^isub>2 - \<pi>\<^isub>1"}\\
 & @{text "="} & @{text "\<pi>\<^isub>1 + (\<pi>\<^isub>2 + \<pi>' - \<pi>\<^isub>2) - \<pi>\<^isub>1"} @{text "\<equiv>"} @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> \<pi>'"}
 \end{tabular}\hfill\qed
 \end{isabelle}
 \end{proof}
-\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 "\<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x) = (\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}.
-\end{lemma}
-\begin{proof} The proof is as follows:
-\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-\begin{tabular}[b]{@ {}rcl@ {\hspace{8mm}}l}
-@{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> x"}
-& @{text "="} & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> (-\<pi>\<^isub>1) \<bullet> \<pi>\<^isub>1 \<bullet> x"} & by \eqref{cancel}\\
-& @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2 - \<pi>\<^isub>1) \<bullet> \<pi>\<^isub>1 \<bullet> x"}  & by {\rm(\ref{newpermprops}.@{text "ii"})}\\
-& @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}\\
-\end{tabular}\hfill\qed
-\end{isabelle}
-\end{proof}
 *}
 section {* Equivariance *}
 text {*
+An important notion in the nominal logic work is \emph{equivariance}.
-An \emph{equivariant} function or predicate is one that is invariant under
+An equivariant function or predicate is one that is invariant under
-the swapping of atoms.  Having a notion of equivariance with nice logical
+the swapping of atoms. This notion can be defined
-properties is a major advantage of bijective permutations over traditional
+uniformly as follows:
-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 "\<forall>\<pi>. \<pi> \<bullet> f = f"}.
 \end{definition}
 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
+the definition, \eqref{permutefunapp} and (\ref{permdefs}.2) lead to a simple
-can easily show that equality is equivariant
+rewrite system that pushes permutations inside a term until they reach
+either function constants or variables. The permutations in front of
+equivariant functions disappear. Such a rewrite system is often very helpful
+in determining whether @{text "p \<bullet> t = t"} holds for a compound term @{text t}. In contrast
+\eqref{altequivariance} is usually easier to establish, since statements are
+commonly given in a form where functions are fully applied. For example we can
+easily show that equality is equivariant
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm eq_eqvt[where p="\<pi>", no_vars]}
 \end{tabular}
 @{thm swap_eqvt[where p="\<pi>", no_vars]}
 \end{tabular}\hfill\numbered{swapeqvt}
 \end{isabelle}
 \noindent
-for all @{text a}, @{text b} and @{text \<pi>}.  These equivariance properties
+for all @{text a}, @{text b} and @{text \<pi>}.
-are tremendously helpful later on when we have to push permutations inside
-terms.
 *}
 section {* Support and Freshness *}
 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
+We also use the notation @{thm (lhs) fresh_star_def[no_vars]} for sets ot atoms
+defined as follows
+@{thm [display,indent=10] fresh_star_def[no_vars]}
 \noindent
 A striking consequence of these definitions is that we can prove
 without knowing anything about the structure of @{term x} that
 swapping two fresh atoms, say @{text a} and @{text b}, leave
 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{equation}
-\begin{tabular}{@ {}c@ {\hspace{2mm}}c@ {}}
+\mbox{
 \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{tabular}
+\end{equation}
-\end{center}
+\noindent
-\noindent
+But establishing the support of atoms and permutations is a bit
-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 \<rightleftharpoons> b) \<bullet> x = x"}.
 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
+renamed. To allow such a choice, we only have to assume that
-of the form @{text "finite (supp x)"}
+@{text "finite (supp x)"} holds. For more convenience we
-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,
+booleans are instances of this type class.
-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.\footnote{Isabelle/HOL takes the type @{text "\<alpha> set"} as an abbreviation
-Unfortunately, this does not work for sets or Isabelle/HOL's function type.
+of @{text "\<alpha> \<Rightarrow> bool"}.}  There are functions and sets definable in
-There are functions and sets definable in Isabelle/HOL for which the finite
+Isabelle/HOL for which the finite support property does not hold.  A simple
-support property does not hold.  A simple example of a function with
+example of a function with infinite support is the function that returns the
-infinite support is the function that returns the natural number of an atom
+natural number of an atom
 @{text [display, indent=10] "nat_of (Atom s i) \<equiv> i"}
 \noindent
 This function's support is the set of \emph{all} atoms. To establish this we show @{term "\<not> a \<sharp> nat_of"}.
 This is equivalent to assuming the set @{term "{b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"} is finite
 & @{text "="} & @{term "((a \<rightleftharpoons> c) \<bullet> nat_of) ((a \<rightleftharpoons> c) \<bullet> a)"} & by \eqref{permutefunapp}\\
 & @{text "="} & @{term "nat_of c"} & by assumptions on @{text c}\\
 \end{tabular}
 \end{isabelle}
 \noindent
 But this means we have that @{term "nat_of a = nat_of c"} and @{term "sort_of a = sort_of c"}.
 This implies that atoms @{term a} and @{term c} must be equal, which clashes with our
 assumption @{term "c \<noteq> a"} about how we chose @{text c}.
 Cheney \cite{Cheney06} gives similar examples for constructions that have infinite support.
 *}
 section {* Support of Finite Sets *}
 text {*
-Sets is one instance of a type that is not generally finitely supported.
+As shown above, sets is one instance of a type that is not generally finitely supported.
-However, it can be easily derived that finite sets of atoms are finitely
+However, we can easily show that finite sets of atoms are finitely
 supported, because their support can be characterised as:
 \begin{lemma}\label{finatomsets}
 If @{text S} is a finite set of atoms, then @{thm (concl) supp_finite_atom_set[no_vars]}.
 \end{lemma}
 \begin{proof}
 finite-supp-unique
 \end{proof}
-More difficult is it to establish that finite sets of finitely
+\noindent
+More difficult, however, is it to establish that finite sets of finitely
 supported objects are finitely supported.
 *}
 section {* Induction Principles *}
 representation for permutations (for example @{term "(a \<rightleftharpoons> b)"} and
 @{term "(b \<rightleftharpoons> a)"} are equal permutations), this representation has
 one draw back: it does not come readily with an induction principle.
 Such an induction principle is handy for deriving properties like
-@{thm [display, indent=10] supp_perm_eq}
+@{thm [display, indent=10] supp_perm_eq[no_vars]}
 \noindent
 However, it is not too difficult to derive an induction principle,
 given the fact that we allow only permutations with a finite domain.
 *}
 section {* Related Work *}
 text {*
 Add here comparison with old work.
+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.
 *}
 section {* Conclusion *}

changeset 2523	e903c32ec24f
parent 2522	0cb0c88b2cad
child 2568	8193bbaa07fe