nominal2: comparison Pearl/Paper.thy

equal deleted inserted replaced

-:4c2e424cb858
+:b7e524e7ee83
 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
 prover providing a proving infrastructure for convenient reasoning about
 programming languages. It has been used to formalise an equivalence checking
 algorithm for LF \cite{UrbanCheneyBerghofer08},
 Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
-\cite{BengtsonParrow07,BengtsonParow09} and a strong normalisation result for
+\cite{BengtsonParrow07} and a strong normalisation result for
 cut-elimination in classical logic \cite{UrbanZhu08}. It has also been used
 by Pollack for formalisations in the locally-nameless approach to binding
 \cite{SatoPollack10}.
 At its core Nominal Isabelle is based on the nominal logic work of Pitts et
 simple formalisation of the nominal logic work.\smallskip
 \noindent
 {\bf Contributions of the paper:} Our use of a single atom type for representing
 atoms of different sorts and of functions for representing
-permutations drastically reduces the number of type classes to just
+permutations is not novel, but drastically reduces the number of type classes to just
 two (permutation types and finitely supported types) that we need in order
 reason abstractly about properties from the nominal logic work. The novel
 technical contribution of this paper 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
 datatype atom\<iota> = Atom\<iota> string nat
 text {*
 \noindent
-whereby the string argument specifies the sort of the atom.  (We use type
+whereby the string argument specifies the sort of the atom.\footnote{A similar
-\emph{string} merely for convenience; any countably infinite type would work
+design choice was made by Gunter et al \cite{GunterOsbornPopescu09}
-as well.)  A similar design choice was made by Gunter et al \cite{GunterOsbornPopescu09}
+for their variables.}  (The use type
-for their variables.
+\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} of
 atoms and every sort @{text s} the property:
 \begin{proposition}\label{choosefresh}
 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
+operation. Obviously, permutations are not commutative in general, because @{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.
 The main point about support is that whenever an object @{text x} has finite
 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
+of the form @{text "finite (supp x)"}
-@{text [display,indent=10] "finite (supp x)"}
-\noindent
 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
 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,
 types.  The definition of the concrete atom type class is as follows: First,
 every concrete atom type must be a permutation type.  In addition, the class
 defines an overloaded function that maps from the concrete type into the
 generic atom type, which we will write @{text "|_|"}.  For each class
 instance, this function must be injective and equivariant, and its outputs
-must all have the same sort.
+must all have the same sort, that is
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 i)   \hspace{1mm}if @{thm (lhs) atom_eq_iff [no_vars]} then @{thm (rhs) atom_eq_iff [no_vars]}\hspace{4mm}
 ii)  \hspace{1mm}@{thm atom_eqvt[where p="\<pi>", no_vars]}\hspace{4mm}
 iii) \hspace{1mm}@{thm sort_of_atom_eq [no_vars]}
 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, the authors of
-\cite{PaulsonBenzmueller} can make headway with formalising their results
+\cite{PaulsonBenzmueller}, can make headway with formalising their results
 about simple type theory.
 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.
 *}

changeset 1780	b7e524e7ee83
parent 1779	4c2e424cb858
child 1783	ed1dc87d1e3b