--- a/Pearl-jv/Paper.thy Fri Apr 08 03:47:50 2011 +0800
+++ b/Pearl-jv/Paper.thy Fri Apr 08 14:23:28 2011 +0800
@@ -64,20 +64,19 @@
\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 aim of this paper is to describe how to
- adapt this work so that it can be implemented in a theorem prover based
- on Higher-Order Logic (HOL). For this we present the definition we made
- in the implementation and also review many proofs. There are a two main
- design choices to be made. One is
- how to represent sorted atoms. We opt here for a single unified atom type to
- represent atoms of different sorts. The other is how to present sort-respecting
- permutations. For them we use the standard technique of
- HOL-formalisations of introducing an appropriate substype of functions from
- atoms to atoms.
-
+ 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 aim of this paper is to
+ describe how to adapt this work so that it can be implemented in a
+ theorem prover based on Higher-Order Logic (HOL). For this we
+ present the definition we made in the implementation and also review
+ many proofs. There are a two main design choices to be made. One is
+ how to represent sorted atoms. We opt here for a single unified atom
+ type to represent atoms of different sorts. The other is how to
+ present sort-respecting permutations. For them we use the standard
+ technique of HOL-formalisations of introducing an appropriate
+ substype of functions from atoms to 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
@@ -164,25 +163,28 @@
text {*
The two most basic notions in the nominal logic work are a countably
- infinite collection of sorted atoms and sort-respecting permutations of 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.
+ infinite collection of sorted atoms and sort-respecting permutations
+ of 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 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 sorts of
- atoms. However, we found that this does not blend well with type-classes in
- Isabelle/HOL (see Section~\ref{related} 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
+ The existing nominal logic work usually leaves implicit the sorting
+ information for atoms and 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 different sorts of
+ atoms. However, we found that this does not blend well with
+ type-classes in Isabelle/HOL (see Section~\ref{related} 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
*}
@@ -330,18 +332,34 @@
nominal theory as smoothly as possible in Isabelle/HOL, we tolerate
the non-standard notation in order to reuse the existing libraries.
-
- A permutation operation, written @{text "\<pi> \<bullet> x"}, applies a permutation
- @{text "\<pi>"} to an object @{text "x"}. This operation has the generic type
+ A \emph{permutation operation}, written @{text "\<pi> \<bullet> x"}, applies a permutation
+ @{text "\<pi>"} to an object @{text "x"} of type @{text \<beta>}, say.
+ This operation has the 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,
+ Isabelle/HOL will allow us to give a definition of this operation for
+ `base' types, such as atoms, permutations, booleans and natural numbers,
+ and for type-constructors, such as functions, sets, lists and products.
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}}
+ atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\
+ permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\
+ booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+ nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+ functions: & @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\
+ sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+ 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]}\\
+ products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+ \end{tabular}\hfill\numbered{permdefs}
+ \end{isabelle}
+
+ 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}:
@@ -353,26 +371,9 @@
\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 satisfy them and that type-constructors
- preserve them. Isabelle/HOL will use this information and determine whether
- an object @{text x} with a compound type satisfies the permutation properties.
- For this we define the notion of a \emph{permutation type}:
+ From these properties and the laws about groups follows that a
+ permutation and its inverse cancel each other. That is
- \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>"}.
- \end{definition}
-
- \noindent
- The type classes 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}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}l}
@{thm permute_minus_cancel(1)[where p="\<pi>", no_vars]}\hspace{10mm}
@@ -381,7 +382,7 @@
\end{isabelle}
\noindent
- Consequently, in a permutation type the permutation operation @{text "\<pi> \<bullet> _"}~~is bijective,
+ Consequently, the permutation operation @{text "\<pi> \<bullet> _"}~~is bijective,
which in turn implies the property
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -393,10 +394,10 @@
\end{isabelle}
\noindent
- We can also show that the following property holds for any permutation type.
+ We can also show that the following property holds for the permutation
+ operation.
\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}
@@ -412,23 +413,37 @@
\end{proof}
\noindent
- Next we define the permutation operation for some types:
+ Note that the permutation operation for functions is defined so that
+ we have for applications the property
\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))"}\\
- 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]}\\
- booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
- 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]}\\
- products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\
- nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
- \end{tabular}\hfill\numbered{permdefs}
+ @{text "\<pi> \<bullet> (f x) ="}
+ @{thm (rhs) permute_fun_app_eq[where p="\<pi>", no_vars]}
+ \hfill\numbered{permutefunapp}
\end{isabelle}
\noindent
+ whenever the permutation properties hold for @{text x}. This property can
+ be easily shown by unfolding the permutation operation for functions on
+ the right-hand side, simplifying the beta-redex and eliminating the permutations
+ in front of @{text x} using \eqref{cancel}.
+
+ The use of type classes allows us to delegate much of the routine
+ resoning involved in determining whether the permutation properties
+ are satisfied to Isabelle/HOL's type system: we only have to
+ establish that base types satisfy them and that type-constructors
+ preserve them. Isabelle/HOL will use this information and determine
+ whether 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>"}.
+ \end{definition}
+
+ \noindent
and establish:
\begin{theorem}
@@ -439,9 +454,9 @@
\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
+ 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}
@@ -452,54 +467,58 @@
\end{tabular}\hfill\qed
\end{isabelle}
\end{proof}
-
- \noindent
- Note that the permutation operation for functions is defined so that we have the property
-
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- @{text "\<pi> \<bullet> (f x) ="}
- @{thm (rhs) permute_fun_app_eq[where p="\<pi>", no_vars]}
- \hfill\numbered{permutefunapp}
- \end{isabelle}
-
- \noindent
- which is a simple consequence of the definition and the cancellation property in \eqref{cancel}.
*}
section {* Equivariance *}
text {*
- An important notion in the nominal logic work is \emph{equivariance}.
- An equivariant function is one that is invariant under the
- permutation operation. This notion can be defined
- uniformly for all constants in HOL as follows:
+ An important notion in the nominal logic work is
+ \emph{equivariance}. To give a definition for this notion, 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 and @{text x} for
+ variables. 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.
+
+ An equivariant HOL-term is one that is invariant under the
+ permutation operation. This notion can be defined as follows:
\begin{definition}[Equivariance]\label{equivariance}
- A constant @{text c} is \emph{equivariant} if @{term "\<forall>\<pi>. \<pi> \<bullet> c = c"}.
+ A HOL-term @{text t} is \emph{equivariant} if @{term "\<forall>\<pi>. \<pi> \<bullet> t = t"}.
\end{definition}
\noindent
- There are a number of equivalent formulations for the equivariance property.
- For example, assuming @{text c} is of type @{text "\<alpha> \<Rightarrow> \<beta>"}, then equivariance
- can also be stated as
+ There are a number of equivalent formulations for the equivariance
+ property. For example, assuming @{text t} 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> (c x) = c (\<pi> \<bullet> x)"}
+ @{text "\<forall>\<pi> x. \<pi> \<bullet> (t x) = t (\<pi> \<bullet> 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
- \eqref{permutefunapp}. Similarly for functions with more than one argument.
+ 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
+ \eqref{permutefunapp}. Similarly for HOL-terms that take more than
+ one argument.
- Both formulations of equivariance have their advantages and disadvantages:
- \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
+ Both formulations of equivariance have their advantages and
+ disadvantages: \eqref{altequivariance} is usually easier to
+ establish, since statements in Isabelle/HOL 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}
@@ -508,14 +527,14 @@
\end{isabelle}
\noindent
- using the permutation operation on booleans and property \eqref{permuteequ}.
- Lemma~\ref{permutecompose} establishes that the permutation operation is
- equivariant. The permutation operation for lists and products, shown in \eqref{permdefs},
- 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
-
+ using the permutation operation on booleans and property
+ \eqref{permuteequ}. Lemma~\ref{permutecompose} establishes that the
+ permutation operation is equivariant. The permutation operation for
+ lists and products, shown in \eqref{permdefs}, state that the
+ constructors for products, @{text "Nil"} and @{text Cons} are
+ 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="\<pi>", no_vars]}
@@ -523,27 +542,35 @@
\end{isabelle}
\noindent
- for all @{text a}, @{text b} and @{text \<pi>}.
- It is also easy to see that the boolean operators, like
- @{text "\<and>"}, @{text "\<or>"}, @{text "\<not>"} and @{text "\<longrightarrow>"} are all equivariant.
+ for all @{text a}, @{text b} and @{text \<pi>}. Also the booleans
+ @{const True} and @{const False} are equivariant by the definition
+ of the permutation operation for booleans. It is also easy to see
+ that the boolean operators, like @{text "\<and>"}, @{text "\<or>"}, @{text
+ "\<not>"} and @{text "\<longrightarrow>"} are all equivariant.
+
+ In contrast, the advantage of Definition \ref{equivariance} is that
+ it leads to a simple rewrite system. Consider the following oriented
+ versions
- In contrast, the equation in Definition~\ref{equivariance} together with the permutation
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{tabular}{@ {}rcl}
+ @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & @{text "\<longmapsto>"} & @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\\
+ @{text "\<pi> \<bullet> (\<lambda>x. t)"} & @{text "\<longmapsto>"} & @{text "\<lambda>x. \<pi> \<bullet> (t[x := (-\<pi>) \<bullet> x])"}\\
+ @{term "\<pi> \<bullet> (- \<pi>) \<bullet> x"} & @{text "\<longmapsto>"} & @{term "x"}\\
+ \end{tabular}\hfill\numbered{swapeqvt}
+ \end{isabelle}
+
+ of the equations
+
+
+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 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
+ see this let us
- \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