--- a/Pearl-jv/Paper.thy Tue Oct 12 13:06:18 2010 +0100
+++ b/Pearl-jv/Paper.thy Wed Oct 13 22:55:58 2010 +0100
@@ -13,6 +13,7 @@
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
@@ -48,7 +49,7 @@
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}\ \ \ \ \ \ \ \ \ \ %%%
@@ -61,18 +62,22 @@
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
- about how to represent sorted atoms and sort-respecting permutations. One possibility
- is to have separate types for the different kinds of atoms, say @{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 overloaded function
+ 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 "\<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>"}
@@ -93,8 +98,8 @@
\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
- is defined as @{text "\<pi> \<bullet> c \<equiv> c"}.
+ @{text "b"}. For atoms with different type than the permutation, we
+ 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''
@@ -108,7 +113,9 @@
\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"}
@@ -127,19 +134,20 @@
\end{isabelle}
\noindent
- Because of these disadvantages, we will use a single unified atom type to
- represent atoms of different sorts. As a result, we have to deal with the
+ Because of these disadvantages, we will use in this paper a single unified atom type to
+ 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.
+ 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
- induction principle for lists. A disadvantage, however, is that permutations
- do not have unique representations as lists; we have to explicitly identify
+ list reversal, and another advantage is that there is a well-understood
+ induction principle for lists, a disadvantage is that permutations
+ do not have unique representations as lists. We have to explicitly identify
them according to the relation
@@ -151,7 +159,7 @@
\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:
@@ -167,24 +175,25 @@
\noindent
where the last clause explicitly states that the permutation operation has
- to produce the same result for related permutations. Moreover, permutations
- as list do not satisfy the usual properties about groups. This means by
+ to produce the same result for related permutations. Moreover,
+ ``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
- in this paper a unique representation for permutations by representing them
- as functions from atoms to atoms.
+ reasoning infrastructure in Isabelle about groups. Because of this, we will represent
+ in this paper permutations as functions from atoms to atoms. This representation
+ 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
- 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 theory---our design choices take advantage of Isabelle's type
- system, type classes and reasoning infrastructure. The novel technical
- contribution is a 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.
+ 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
+ theory---our design choices take advantage of Isabelle's type system, type
+ classes and reasoning infrastructure. The novel technical contribution is a
+ 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
+ The paper is organised as follows\ldots
*}
section {* Sorted Atoms and Sort-Respecting Permutations *}
@@ -203,7 +212,7 @@
\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}
@@ -374,7 +383,7 @@
\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}\ \ \ \ \ \ \ \ \ \ %%%
@@ -386,25 +395,41 @@
\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{tabular}{@ {}c@ {\hspace{-1mm}}c@ {}}
- \begin{tabular}{@ {}r@ {\hspace{2mm}}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]}\\
- \end{tabular} &
- \begin{tabular}{@ {}r@ {\hspace{2mm}}l@ {}}
- 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]}\\[2mm]
- 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}
- \end{tabular}
- \end{isabelle}
+ \begin{equation}\label{permdefs}
+ \mbox{
+ \begin{tabular}{@ {}ll@ {\hspace{2mm}}l@ {}}
+ 1) & 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))"}\\
+ 3) & 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]}\\
+ 5) & 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]}\\
+ & & @{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]}\\
+ 8) & nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+ \end{tabular}}
+ \end{equation}
\noindent
and then establish:
@@ -430,42 +455,15 @@
\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 \emph{equivariant} function or predicate is one that is invariant under
- the swapping of atoms. Having a notion of equivariance with nice logical
- properties is a major advantage of bijective permutations over traditional
- renaming substitutions \cite[\S2]{Pitts03}. Equivariance can be defined
- uniformly for all permutation types, and it is satisfied by most HOL
- functions and constants.
+ An important notion in the nominal logic work is \emph{equivariance}.
+ An equivariant function or predicate is one that is invariant under
+ the swapping of atoms. This notion can be defined
+ uniformly as follows:
\begin{definition}\label{equivariance}
@@ -501,8 +499,14 @@
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
- can easily show that equality is equivariant
+ the definition, \eqref{permutefunapp} and (\ref{permdefs}.2) lead 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
+ 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}
@@ -524,9 +528,7 @@
\end{isabelle}
\noindent
- for all @{text a}, @{text b} and @{text \<pi>}. These equivariance properties
- are tremendously helpful later on when we have to push permutations inside
- terms.
+ for all @{text a}, @{text b} and @{text \<pi>}.
*}
@@ -551,6 +553,12 @@
@{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
@@ -638,22 +646,19 @@
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{tabular}{@ {}c@ {\hspace{2mm}}c@ {}}
+ \begin{equation}
+ \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{center}
+ \end{tabular}}
+ \end{equation}
\noindent
- But establishing the support of atoms and permutations in our setup here is a bit
+ But establishing the support of atoms and permutations is a bit
trickier. To do so we will use the following notion about a \emph{supporting set}.
\begin{definition}
@@ -773,21 +778,19 @@
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
- of the form @{text "finite (supp x)"}
- 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
+ renamed. To allow such a choice, we only have to assume that
+ @{text "finite (supp x)"} holds. 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,
- as the type system of Isabelle/HOL can figure out automatically when an object
- is finitely supported.
+ booleans are instances of this type class.
- Unfortunately, this does not work for sets or Isabelle/HOL's function type.
- There are functions and sets definable in Isabelle/HOL for which the finite
- support property does not hold. A simple example of a function with
- infinite support is the function that returns the natural number of an atom
-
+ 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
+ of @{text "\<alpha> \<Rightarrow> bool"}.} There are functions and sets definable in
+ Isabelle/HOL for which the finite support property does not hold. A simple
+ example of a function with infinite support is the function that returns the
+ natural number of an atom
+
@{text [display, indent=10] "nat_of (Atom s i) \<equiv> i"}
\noindent
@@ -807,7 +810,6 @@
\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
@@ -818,8 +820,8 @@
section {* Support of Finite Sets *}
text {*
- 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
+ As shown above, sets is one instance of a type that is not generally finitely supported.
+ However, we can easily show that finite sets of atoms are finitely
supported, because their support can be characterised as:
\begin{lemma}\label{finatomsets}
@@ -830,7 +832,8 @@
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.
*}
@@ -844,7 +847,7 @@
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,
@@ -1372,6 +1375,11 @@
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.
*}