nominal2: comparison Pearl-jv/Paper.thy

equal deleted inserted replaced

-:d7a2c45b447a
+:08e4d3cbcf8c
 with the large amounts of custom ML-code for generating multiple variants
 for some basic definitions. The result is that we can implement a pleasingly
 simple formalisation of the nominal logic work.\smallskip
 \noindent
-{\bf Contributions of the paper:} Our use of a single atom type for representing
+{\bf Contributions of the paper:} Using a single atom type to represent
-atoms of different sorts and of functions for representing
+atoms of different sorts and representing permutations as functions are not
-permutations is not novel, but drastically reduces the number of type classes to just
+new ideas.  The main contribution of this paper is to show an example of how
-two (permutation types and finitely supported types) that we need in order
+to make better theorem proving tools by choosing the right level of
-reason abstractly about properties from the nominal logic work. The novel
+abstraction for the underlying theory---our design choices take advantage of
-technical contribution of this paper is a mechanism for dealing with
+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.
 *}
 section {* Sorted Atoms and Sort-Respecting Permutations *}
 text {*
 \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 non-commutative) group provided we define
+they form a (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
+form a group.  The technical importance of this fact is that we can rely on
-can rely on Isabelle/HOL's rich simplification infrastructure.  This will
+Isabelle/HOL's existing simplification infrastructure for groups, which will
 come in handy when we have to do calculations with permutations.
 Note that Isabelle/HOL defies standard conventions of mathematical notation
 by using additive syntax even for non-commutative groups.  Obviously,
 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
 section {* Equivariance *}
 text {*
-One huge advantage of using bijective permutation functions (as opposed to
+An \emph{equivariant} function or predicate is one that is invariant under
-non-bijective renaming substitutions employed in traditional works syntax) is
+the swapping of atoms.  Having a notion of equivariance with nice logical
-the property of \emph{equivariance}
+properties is a major advantage of bijective permutations over traditional
-and the fact that most HOL-functions (this includes constants) whose argument
+renaming substitutions \cite[\S2]{Pitts03}.  Equivariance can be defined
-and result types are permutation types satisfy this property:
+uniformly for all permutation types, and it is satisfied by most HOL
+functions and constants.
 \begin{definition}\label{equivariance}
 A function @{text f} is \emph{equivariant} if @{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}.
 \end{definition}
 \begin{lemma}\label{optimised} Let @{text x} be of permutation type.
 We have that @{thm (concl) finite_supp_unique[no_vars]}
 provided @{thm (prem 1) finite_supp_unique[no_vars]},
 @{thm (prem 2) finite_supp_unique[no_vars]}, and for
 all @{text "a \<in> S"} and all @{text "b \<notin> S"}, with @{text a}
-and @{text b} having the same sort, then \mbox{@{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"}}
+and @{text b} having the same sort, \mbox{@{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"}}
 \end{lemma}
 \begin{proof}
 By Lemma \ref{supports}@{text ".iii)"} we have to show that for every finite
 set @{text S'} that supports @{text x}, \mbox{@{text "S \<subseteq> S'"}} holds. We will
 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 \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
+Our hope is that with this approach Benzmueller and Paulson can make
-\cite{PaulsonBenzmueller}, can make headway with formalising their results
+headway with formalising their results
-about simple type theory.
+about simple type theory \cite{PaulsonBenzmueller}.
 Because of its limitations, they did not attempt this with the old version
 of Nominal Isabelle. We also hope we can make progress with formalisations of
 HOL-based languages.
 *}
 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
+lists we can easily perform inductions. For permutations made up from
 functions, we have to manually derive an appropriate induction principle. We
 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, except
 when showing that if @{term "\<forall>a \<in> supp x. a \<sharp> p"} implies @{term "p \<bullet> x = x"}.

changeset 1809	08e4d3cbcf8c
parent 1790	000e680b6b6e
child 2005	233bb805a4df