nominal2: comparison Pearl-jv/Paper.thy

equal deleted inserted replaced

-:7085ab735de7
+:56b8d977d1c0
 renaming substitutions of atoms. One reason is that permutations are
 bijective renamings of atoms and thus they can be easily `undone'---namely
 by applying the inverse permutation. A corresponding inverse substitution
 might not always exist, since renaming substitutions are in general only injective.
 Another reason is that permutations preserve many constructions when reasoning about syntax.
-For example the validity of a typing context is preserved under any permutation.
+For example, suppose a typing context @{text "\<Gamma>"} of the form
-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
+occur twice. Then validity of typing contexts is preserved under
-permutations in the sense that if @{text \<Gamma>} is valid then so is @{text "\<pi> \<bullet> \<Gamma>"} for
+permutations in the sense that if @{text \<Gamma>} is valid then so is \mbox{@{text "\<pi> \<bullet> \<Gamma>"}} for
-all permutations @{text "\<pi>"}. This is again \emph{not} the case for arbitrary
+all permutations @{text "\<pi>"}. Again, this is \emph{not} the case for arbitrary
 renaming substitutions, as they might identify some of the @{text "x\<^isub>i"} in @{text \<Gamma>}.
 Permutations also behave uniformly with respect to HOL's logic connectives.
 Applying a permutation to a formula gives, for example
 \noindent
 This uniform behaviour can also be extended to quantifiers and functions.
 Because of these good properties of permutations, we are able to automate
 reasoning to do with \emph{equivariance}. By equivariance we mean the property
-that every permutation leaves an object unchanged, that is @{term "\<pi> \<bullet> x = x"}
+that every permutation leaves a function unchanged, that is @{term "\<pi> \<bullet> f = f"}
 for all @{text "\<pi>"}. This will often simplify arguments involving support
-and functions, since equivariant objects have empty support---or
+of functions, since if they are equivariant then they have empty support---or
 `no free atoms'.
 There are a number of subtle differences between the nominal logic work by
 Pitts and the formalisation we will present in this paper. One difference
 is that our
 section {* Sorted Atoms and Sort-Respecting Permutations *}
 text {*
 The two most basic notions in the nominal logic work are a countably
-infinite collection of sorted atoms and sort-respecting permutations.
+infinite collection of sorted atoms and sort-respecting permutations 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
 whereby the string argument specifies the sort of the atom.\footnote{A
 similar design choice was made by Gunter et al \cite{GunterOsbornPopescu09}
 for their variables.}  The use of type \emph{string} for sorts is merely for
 convenience; any countably infinite type would work as well.
 The set of all atoms we shall write as @{term "UNIV::atom set"}.
-We have two
+We have two auxiliary functions for atoms, namely @{text sort}
-auxiliary functions @{text sort} and @{const nat_of} that are defined as
+and @{const nat_of} which are defined as
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
 @{thm (lhs) sort_of.simps[no_vars]} & @{text "\<equiv>"} & @{thm (rhs) sort_of.simps[no_vars]}\\
 @{thm (lhs) nat_of.simps[no_vars]} & @{text "\<equiv>"}  & @{thm (rhs) nat_of.simps[no_vars]}
 \noindent
 but since permutations are required to respect sorts, we must carefully
 consider what happens if a user states a swapping of atoms with different
 sorts.  The following definition\footnote{To increase legibility, we omit
 here and in what follows the @{term Rep_perm} and @{term "Abs_perm"}
-wrappers that are needed in our implementation since we defined permutation
+wrappers that are needed in our implementation in Isabelle/HOL since we defined permutation
 not to be the full function space, but only those functions of type @{typ
 perm} satisfying properties @{text i}-@{text "iii"} in \eqref{permtype}.}
 @{text [display,indent=10] "(a b) \<equiv> \<lambda>c. if a = c then b else (if b = c then a else c)"}
 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.
-In order to reason abstractly about permutations, we use Isabelle/HOL's
-type classes~\cite{Wenzel04} and state the following two
+A permutation operation, written @{text "\<pi> \<bullet> x"}, applies a permutation
+@{text "\<pi>"} to an object @{text "x"}. This operation has the generic type
+\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+@{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
+\end{isabelle}
+\noindent
+and Isabelle/HOL will allow us to give a definition of this operation for
+`base' types, such as booleans and atoms, and for type-constructors, such as
+products and lists. In order to reason abstractly about this operation,
+we use Isabelle/HOL's type classes~\cite{Wenzel04} and state the following two
 \emph{permutation properties}:
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
 i) & @{thm permute_zero[no_vars]}\\
 \end{isabelle}
 \noindent
 The use of type classes allows us to delegate much of the routine resoning involved in
 determining whether these properties are satisfied to Isabelle/HOL's type system:
-we only have to establish that `base' types, such as @{text booleans} and
+we only have to establish that base types satisfy them and that type-constructors
-@{text atoms}, satisfy them and that type-constructors, such as products and lists,
+preserve them. Isabelle/HOL will use this information and determine whether
-preserve them.  For this we define
+an object @{text x} with a compound type satisfies the permutation properties.
+For this we define the notion of a \emph{permutation type}:
 \begin{definition}[Permutation type]
 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>"}.
 @{thm (rhs) permute_eq_iff[where p="\<pi>", no_vars]}.
 \end{tabular}\hfill\numbered{permuteequ}
 \end{isabelle}
 \noindent
-In order to lift the permutation operation to other types, we can define for:
+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]{@ {}c@ {\hspace{2mm}}l@ {\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
+Next we define the permutation operation for some types:
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}}
 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))"}\\
 nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
 \end{tabular}\hfill\numbered{permdefs}
 \end{isabelle}
 \noindent
-and then establish:
+and establish:
 \begin{theorem}
 If @{text \<beta>}, @{text "\<beta>\<^isub>1"} and @{text "\<beta>\<^isub>2"} are permutation types,
 then so are @{text "atom"}, @{text "\<beta>\<^isub>1 \<Rightarrow> \<beta>\<^isub>2"},
 @{text perm}, @{term "\<beta> set"}, @{term "\<beta> list"}, @{term "\<beta>\<^isub>1 \<times> \<beta>\<^isub>2"},
 \hfill\numbered{permutefunapp}
 \end{isabelle}
 \noindent
 which is a simple consequence of the definition and the cancellation property in \eqref{cancel}.
-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]{@ {}c@ {\hspace{2mm}}l@ {\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 equivariant function is one that is invariant under
+An equivariant function is one that is invariant under the
-permutations of atoms. This notion can be defined
+permutation operation. This notion can be defined
-uniformly as follows:
+uniformly for all constants in HOL as follows:
 \begin{definition}[Equivariance]\label{equivariance}
-A function @{text f} is \emph{equivariant} if @{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}.
+A constant @{text c} is \emph{equivariant} if @{term "\<forall>\<pi>. \<pi> \<bullet> c = c"}.
 \end{definition}
 \noindent
 There are a number of equivalent formulations for the equivariance property.
-For example, assuming @{text f} is of type @{text "\<alpha> \<Rightarrow> \<beta>"}, then equivariance
+For example, assuming @{text c} is of type @{text "\<alpha> \<Rightarrow> \<beta>"}, then equivariance
 can also be stated as
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
-@{text "\<forall>\<pi> x.  \<pi> \<bullet> (f x) = f (\<pi> \<bullet> x)"}
+@{text "\<forall>\<pi> x.  \<pi> \<bullet> (c x) = c (\<pi> \<bullet> x)"}
 \end{tabular}\hfill\numbered{altequivariance}
 \end{isabelle}
 \noindent
 To see that this formulation implies the definition, we just unfold the
 \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
+equivariant. The permutation operation for lists and products, shown in \eqref{permdefs},
-@{text "\<and>"}, @{text "\<or>"}, @{text "\<not>"} and @{text "\<longrightarrow>"} are all equivariant. Furthermore
+state that the constructors for products, @{text "Nil"} and @{text Cons} are equivariant. Also
+the booleans @{const True} and @{const False} are equivariant by the permutation
+operation. Furthermore
 a simple calculation will show that our swapping functions are equivariant, that is
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{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>}.
+It is also easy to see that the boolean operators, like
-In contrast, Definition~\ref{equivariance} together with the permutation
+@{text "\<and>"}, @{text "\<or>"}, @{text "\<not>"} and @{text "\<longrightarrow>"} are all equivariant.
-operation for functions and \eqref{permutefunapp} lead to a simple
-rewrite system that pushes permutations inside a term until they reach
+In contrast, the equation in Definition~\ref{equivariance} together with the permutation
+operation for functions and the properties in \eqref{permutefunapp} and \eqref{cancel}
+leads to a simple 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
+equivariant constants disappear. This helps us to establish equivariance
+for any notion in HOL that is defined in terms of more primitive notions. To
+see this let us define \emph{HOL-terms}. They are given by the grammar
+\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+@{text "t ::= c | x | t\<^isub>1 t\<^isub>2 | \<lambda>x. t"}
+\hfill\numbered{holterms}
+\end{isabelle}
+\noindent
+whereby @{text c} stands for constants. We assume HOL-terms are fully typed, but
+for the sake of greater legibility we leave the typing information implicit.
+We also assume the usual notions for free and bound variables of a HOL-term.
+With these definitions in place we can define the notion of an \emph{equivariant}
+HOL-term
+\begin{definition}[Equivariant HOL-term]
+A HOL-term is \emph{equivariant}, provided it is closed and composed of applications,
+abstractions and equivariant constants only.
+\end{definition}
+\noindent
+For equivariant terms we have
+\begin{lemma}
+For an equivariant HOL-term @{text "t"},  @{term "\<pi> \<bullet> t = t"} for all permutations @{term "\<pi>"}.
+\end{lemma}
+\begin{proof}
+By induction on the grammar of HOL-terms. The case for variables cannot arise since
+equivariant HOL-terms are closed. The case for constants is clear by Definition
+\ref{equivariance}. The case for applications is also straightforward since by
+\eqref{permutefunapp} we have @{term "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2) = (\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}.
+For the case of abstractions we can reason as follows
+\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+\begin{tabular}[b]{@ {}c@ {\hspace{2mm}}l@ {\hspace{8mm}}l}
+& @{text "\<pi> \<bullet> (\<lambda>x. t)"}\\
+@{text "\<equiv>"} & @{text "\<lambda>y. \<pi> \<bullet> ((\<lambda>x. t) ((-\<pi>) \<bullet> y))"} & by \eqref{permdefs}\\
+\end{tabular}\hfill\qed
+\end{isabelle}
+\end{proof}
+database of equivariant functions
+Such a rewrite system is often very helpful
 in determining whether @{text "\<pi> \<bullet> t = t"} holds for a compound term @{text t}. ???
 *}

changeset 2744	56b8d977d1c0
parent 2742	f1192e3474e0
child 2746	6aa98a113e6c