nominal2: comparison Pearl/Paper.thy

equal deleted inserted replaced

-:88ec05a09772
+:4c2e424cb858
 identity on all atoms, except a finite number of them; and @{text "iii)"} map
 each atom to one of the same sort. These properties can be conveniently stated
 for a function @{text \<pi>} as follows:
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-\begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
+i)~~~@{term "bij \<pi>"}\hspace{5mm}
-i) & @{term "bij \<pi>"}\\
+ii)~~~@{term "finite {a. \<pi> a \<noteq> a}"}\hspace{5mm}
-ii) & @{term "finite {a. \<pi> a \<noteq> a}"}\\
+iii)~~~@{term "\<forall>a. sort (\<pi> a) = sort a"}\hfill\numbered{permtype}
-iii) & @{term "\<forall>a. sort (\<pi> a) = sort a"}
-\end{tabular}\hfill\numbered{permtype}
 \end{isabelle}
 \noindent
 Like all HOL-based theorem provers, Isabelle/HOL allows us to
 introduce a new type @{typ perm} that includes just those functions
 \noindent
 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}
 @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm}
 @{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{4mm}
 \end{tabular}
 \end{isabelle}
 \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
+form a group. The technical importance of this fact is that for groups we
-rely on Isabelle/HOL's rich simplification infrastructure.  This will come in
+can rely on Isabelle/HOL's rich simplification infrastructure.  This will
-handy when we have to do calculations with permutations.
+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
 \eqref{permprops} as just the two equations
 have only a single type parameter.  Consequently, these properties are
 compatible with the one-parameter restriction of Isabelle/HOL's type classes.
 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
+@{text "\<beta>"}.
-applicable to any permutation type.  First, it follows from the laws governing
+\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:
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 %section { * Equivariance * }
 %
 %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:
 \begin{definition}\label{equivariance}
 A function @{text f} is \emph{equivariant} if @{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}.
 @{text "\<lambda>x\<^isub>\<alpha>. x\<^isub>\<alpha> x\<^isub>\<beta>"}
 \end{tabular}\hfill\numbered{church}
 \end{isabelle}
 \noindent
-both variables and binders include typing information indicated by @{text
+both variables and binders include typing information indicated by @{text \<alpha>}
-\<alpha>} and @{text \<beta>}. In this setting, we treat @{text
+and @{text \<beta>}. In this setting, we treat @{text "x\<^isub>\<alpha>"} and @{text
-"x\<^isub>\<alpha>"} and @{text "x\<^isub>\<beta>"} as distinct variables
+"x\<^isub>\<beta>"} as distinct variables (assuming @{term "\<alpha>\<noteq>\<beta>"}) so that the
-(assuming @{term "\<alpha>\<noteq>\<beta>"}) so that the variable @{text
+variable @{text "x\<^isub>\<alpha>"} is bound by the lambda-abstraction, but not
-"x\<^isub>\<alpha>"} is bound by the lambda-abstraction, but not @{text
+@{text "x\<^isub>\<beta>"}.
-"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
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \end{tabular}
 \end{isabelle}
 \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
+problem that a swapping, say @{term "(x \<leftrightarrow> y)"}, applied to the pair @{text "((x, \<alpha>), (x, \<beta>))"}
-@{text [display,indent=10] "((x, \<alpha>), (x, \<beta>))"}
-\noindent
 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
 corresponding binder.
 \noindent
 As we expect, the atom @{term "Var x \<beta>"} is left unchanged by the
 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
+user just needs to specify \isacommand{atom\_decl}~~@{text "var (ty)"}
-\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-\begin{tabular}{@ {}l}
-\isacommand{atom\_decl}~~@{text "var (ty)"}
-\end{tabular}
-\end{isabelle}
-\noindent
 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
 \cite{PaulsonBenzmueller} can make headway with formalising their results
 about simple type theory.
 An interesting point is that we defined the swapping operation so that a
 swapping of two atoms with different sorts is \emph{not} excluded, like
 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
+and HOL-based languages. While dealing with such additional information in
-language formalisations that can deal conveniently with such binders.
+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
 Berghofer and Cezary Kaliszyk for their comments on earlier versions
 of this paper. We are also grateful to the anonymous referee who helped us to

changeset 1779	4c2e424cb858
parent 1776	0c958e385691
child 1780	b7e524e7ee83
child 1781	6454f5c9d211