# HG changeset patch # User Christian Urban # Date 1270670926 -7200 # Node ID 4c2e424cb8586680187e63ac5ea963697441c6f7 # Parent 88ec05a097725742d7711e7a3ad4a2455b7cb323 my final version of the paper diff -r 88ec05a09772 -r 4c2e424cb858 Nominal-General/Nominal2_Atoms.thy --- a/Nominal-General/Nominal2_Atoms.thy Wed Apr 07 17:37:29 2010 +0200 +++ b/Nominal-General/Nominal2_Atoms.thy Wed Apr 07 22:08:46 2010 +0200 @@ -242,12 +242,6 @@ setup {* Sign.add_const_constraint (@{const_name "atom"}, SOME @{typ "'a::at_base \ atom"}) *} -ML {* - Theory_Target.instantiation; - Local_Theory.exit_global -*} - - section {* Automation for creating concrete atom types *} text {* at the moment only single-sort concrete atoms are supported *} diff -r 88ec05a09772 -r 4c2e424cb858 Pearl/Paper.thy --- 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 \} as follows: \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}} - i) & @{term "bij \"}\\ - ii) & @{term "finite {a. \ a \ a}"}\\ - iii) & @{term "\a. sort (\ a) = sort a"} - \end{tabular}\hfill\numbered{permtype} + i)~~~@{term "bij \"}\hspace{5mm} + ii)~~~@{term "finite {a. \ a \ a}"}\hspace{5mm} + iii)~~~@{term "\a. sort (\ 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 \ 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 "\"} 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 "\"} is a \emph{permutation type} if the permutation properties in \eqref{newpermprops} are satisfied for every @{text "x"} of type - @{text "\"}. This notion allows us to establish generic lemmas, which are - applicable to any permutation type. First, it follows from the laws governing + @{text "\"}. + \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 - \} and @{text \}. In this setting, we treat @{text - "x\<^isub>\"} and @{text "x\<^isub>\"} as distinct variables - (assuming @{term "\\\"}) so that the variable @{text - "x\<^isub>\"} is bound by the lambda-abstraction, but not @{text - "x\<^isub>\"}. + both variables and binders include typing information indicated by @{text \} + and @{text \}. In this setting, we treat @{text "x\<^isub>\"} and @{text + "x\<^isub>\"} as distinct variables (assuming @{term "\\\"}) so that the + variable @{text "x\<^isub>\"} is bound by the lambda-abstraction, but not + @{text "x\<^isub>\"}. To illustrate how we can deal with this phenomenon, let us represent object types like @{text \} and @{text \} 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 \ y)"}, applied to the pair - - @{text [display,indent=10] "((x, \), (x, \))"} - - \noindent + problem that a swapping, say @{term "(x \ y)"}, applied to the pair @{text "((x, \), (x, \))"} will always permute \emph{both} occurrences of @{text x}, even if the types @{text "\"} and @{text "\"} 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 "\a \ supp x. a \ p"} implies @{term "p \ 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