--- a/Pearl/Paper.thy Wed Apr 07 17:37:29 2010 +0200
+++ b/Pearl/Paper.thy Wed Apr 07 22:08:46 2010 +0200
@@ -262,11 +262,9 @@
for a function @{text \<pi>} as follows:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
- i) & @{term "bij \<pi>"}\\
- ii) & @{term "finite {a. \<pi> a \<noteq> a}"}\\
- iii) & @{term "\<forall>a. sort (\<pi> a) = sort a"}
- \end{tabular}\hfill\numbered{permtype}
+ i)~~~@{term "bij \<pi>"}\hspace{5mm}
+ ii)~~~@{term "finite {a. \<pi> a \<noteq> a}"}\hspace{5mm}
+ iii)~~~@{term "\<forall>a. sort (\<pi> a) = sort a"}\hfill\numbered{permtype}
\end{isabelle}
\noindent
@@ -339,7 +337,7 @@
are \emph{equal}. We do not have to use the equivalence relation shown
in~\eqref{permequ} to identify them, as we would if they had been represented
as lists of pairs. Another advantage of the function representation is that
- they form an (additive) group provided we define
+ they form an (additive non-commutative) group provided we define
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}l}
@@ -364,9 +362,17 @@
\noindent
Again this is in contrast to the list-of-pairs representation which does not
- form a group. The technical importance of this fact is that for groups we can
- rely on Isabelle/HOL's rich simplification infrastructure. This will come in
- handy when we have to do calculations with permutations.
+ form a group. The technical importance of this fact is that for groups we
+ can rely on Isabelle/HOL's rich simplification infrastructure. This will
+ come in handy when we have to do calculations with permutations. However,
+ note that in this case Isabelle/HOL neglects well-entrenched mathematical
+ terminology that associates with an additive group a commutative
+ operation. Obviously, permutations are not commutative in general---@{text
+ "p + q \<noteq> q + p"}. However, it is quite difficult to work around this
+ idiosyncrasy of Isabelle/HOL, unless we develop our own algebraic hierarchy
+ and infrastructure. But since the point of this paper is to implement the
+ nominal theory as smoothly as possible in Isabelle/HOL, we will follow its
+ characterisation of additive groups.
By formalising permutations abstractly as functions, and using a single type
for all atoms, we can now restate the \emph{permutation properties} from
@@ -386,10 +392,17 @@
There is no need to introduce a separate type class instantiated for each
sort, like in the old approach.
- We call type @{text "\<beta>"} a \emph{permutation type} if the permutation
+ 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>"}. This notion allows us to establish generic lemmas, which are
- applicable to any permutation type. First, it follows from the laws governing
+ @{text "\<beta>"}.
+ \end{definition}
+
+ \noindent
+ 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:
@@ -489,7 +502,8 @@
%text { *
One huge advantage of using bijective permutation functions (as opposed to
- non-bijective renaming substitutions) is the property of \emph{equivariance}
+ non-bijective renaming substitutions employed in traditional works syntax) is
+ the property of \emph{equivariance}
and the fact that most HOL-functions (this includes constants) whose argument
and result types are permutation types satisfy this property:
@@ -1009,12 +1023,11 @@
\end{isabelle}
\noindent
- both variables and binders include typing information indicated by @{text
- \<alpha>} and @{text \<beta>}. In this setting, we treat @{text
- "x\<^isub>\<alpha>"} and @{text "x\<^isub>\<beta>"} as distinct variables
- (assuming @{term "\<alpha>\<noteq>\<beta>"}) so that the variable @{text
- "x\<^isub>\<alpha>"} is bound by the lambda-abstraction, but not @{text
- "x\<^isub>\<beta>"}.
+ both variables and binders include typing information indicated by @{text \<alpha>}
+ and @{text \<beta>}. In this setting, we treat @{text "x\<^isub>\<alpha>"} and @{text
+ "x\<^isub>\<beta>"} as distinct variables (assuming @{term "\<alpha>\<noteq>\<beta>"}) so that the
+ variable @{text "x\<^isub>\<alpha>"} is bound by the lambda-abstraction, but not
+ @{text "x\<^isub>\<beta>"}.
To illustrate how we can deal with this phenomenon, let us represent object
types like @{text \<alpha>} and @{text \<beta>} by the datatype
@@ -1027,11 +1040,7 @@
\noindent
If we attempt to encode a variable naively as a pair of a @{text name} and a @{text ty}, we have the
- problem that a swapping, say @{term "(x \<leftrightarrow> y)"}, applied to the pair
-
- @{text [display,indent=10] "((x, \<alpha>), (x, \<beta>))"}
-
- \noindent
+ problem that a swapping, say @{term "(x \<leftrightarrow> y)"}, applied to the pair @{text "((x, \<alpha>), (x, \<beta>))"}
will always permute \emph{both} occurrences of @{text x}, even if the types
@{text "\<alpha>"} and @{text "\<beta>"} are different. This is unwanted, because it will
eventually mean that both occurrences of @{text x} will become bound by a
@@ -1141,15 +1150,7 @@
swapping. With this we can faithfully represent bindings in languages
involving ``Church-style'' terms and bindings as shown in \eqref{church}. We
expect that the creation of such atoms can be easily automated so that the
- user just needs to specify
-
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \begin{tabular}{@ {}l}
- \isacommand{atom\_decl}~~@{text "var (ty)"}
- \end{tabular}
- \end{isabelle}
-
- \noindent
+ user just needs to specify \isacommand{atom\_decl}~~@{text "var (ty)"}
where the argument, or arguments, are datatypes for which we can automatically
define an injective function like @{text "sort_ty"} (see \eqref{sortty}).
Our hope is that with this approach Benzmueller and Paulson the authors of
@@ -1195,26 +1196,31 @@
in our older work on Nominal Isabelle, but there is no ``effect'' of such
a swapping (it is defined as the identity). This is a crucial insight
in order to make the approach based on a single type of sorted atoms to work.
+ But of course it is analogous to the well-known trick of defining division by
+ zero to return zero.
We noticed only one disadvantage of the permutations-as-functions: Over
lists we can easily perform inductions. For permutation made up from
functions, we have to manually derive an appropriate induction principle. We
- can establish such a principle, but we have no experience yet whether ours
+ can establish such a principle, but we have no real experience yet whether ours
is the most useful principle: such an induction principle was not needed in
- any of the reasoning we ported from the old Nominal Isabelle.
+ any of the reasoning we ported from the old Nominal Isabelle, except
+ when showing that if @{term "\<forall>a \<in> supp x. a \<sharp> p"} implies @{term "p \<bullet> x = x"}.
Finally, our implementation of sorted atoms turned out powerful enough to
- use it for representing variables that carry additional information, for
+ use it for representing variables that carry on additional information, for
example typing annotations. This information is encoded into the sorts. With
this we can represent conveniently binding in ``Church-style'' lambda-terms
- and HOL-based languages. We are not aware of any other approach proposed for
- language formalisations that can deal conveniently with such binders.
+ and HOL-based languages. While dealing with such additional information in
+ dependent type-theories, such as LF or Coq, is straightforward, we are not
+ aware of any other approach in a non-dependent HOL-setting that can deal
+ conveniently with such binders.
The formalisation presented here will eventually become part of the Isabelle
distribution, but for the moment it can be downloaded from the
Mercurial repository linked at
\href{http://isabelle.in.tum.de/nominal/download}
- {http://isabelle.in.tum.de/nominal/download}.\medskip
+ {http://isabelle.in.tum.de/nominal/download}.\smallskip
\noindent
{\bf Acknowledgements:} We are very grateful to Jesper Bengtson, Stefan