# HG changeset patch # User Christian Urban # Date 1272947803 -3600 # Node ID 74bd7bfb484b57190e27bb50268e786aa2414b12 # Parent 5641981ec67dbd8aae2e258f39bac9b8d0024655 some preliminary changes to the pearl-jv paper diff -r 5641981ec67d -r 74bd7bfb484b Nominal-General/Nominal2_Supp.thy --- a/Nominal-General/Nominal2_Supp.thy Mon May 03 08:52:15 2010 +0100 +++ b/Nominal-General/Nominal2_Supp.thy Tue May 04 05:36:43 2010 +0100 @@ -539,4 +539,5 @@ using fin by (simp add: supp_of_fin_sets) + end diff -r 5641981ec67d -r 74bd7bfb484b Pearl-jv/Paper.thy --- a/Pearl-jv/Paper.thy Mon May 03 08:52:15 2010 +0100 +++ b/Pearl-jv/Paper.thy Tue May 04 05:36:43 2010 +0100 @@ -2,7 +2,8 @@ theory Paper imports "../Nominal-General/Nominal2_Base" "../Nominal-General/Nominal2_Atoms" - "../Nominal-General/Nominal2_Eqvt" + "../Nominal-General/Nominal2_Eqvt" + "../Nominal-General/Nominal2_Supp" "../Nominal-General/Atoms" "LaTeXsugar" begin @@ -43,24 +44,22 @@ section {* Introduction *} text {* + The purpose of Nominal Isabelle is to provide a proving infratructure + for conveninet reasoning about programming languages. At its core + Nominal Isabelle is based on nominal logic by Pitts at al + \cite{GabbayPitts02,Pitts03}. + 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} 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}. + programming languages. At its core Nominal Isabelle is based on the nominal + logic work of Pitts et al \cite{GabbayPitts02,Pitts03}. The most basic + notion in this work is a sort-respecting permutation operation defined over + a countably infinite collection of sorted atoms. The atoms are used for + representing variables that might be bound. Multiple sorts are necessary for + being able to represent different kinds of variables. For example, in the + language Mini-ML there are bound term variables and bound type variables; + each kind needs to be represented by a different sort of atoms. - At its core Nominal Isabelle is based on the nominal logic work of Pitts et - al \cite{GabbayPitts02,Pitts03}. The most basic notion in this work is a - sort-respecting permutation operation defined over a countably infinite - collection of sorted atoms. The atoms are used for representing variables - that might be bound. Multiple sorts are necessary for being - able to represent different kinds of variables. For example, in the language - Mini-ML there are bound term variables and bound type variables; each kind - needs to be represented by a different sort of atoms. Unfortunately, the type system of Isabelle/HOL is not a good fit for the way atoms and sorts are used in the original formulation of the nominal logic work. @@ -858,9 +857,41 @@ Cheney \cite{Cheney06} gives similar examples for constructions that have infinite support. *} +section {* Support of Finite Sets *} + +text {* + Sets is one instance of a type that is not generally finitely supported. + However, it can be easily derived that finite sets of atoms are finitely + supported, because their support can be characterised as: + + \begin{lemma}\label{finatomsets} + If @{text S} is a finite set of atoms, then @{thm (concl) supp_finite_atom_set[no_vars]}. + \end{lemma} + + \begin{proof} + finite-supp-unique + \end{proof} + + More difficult is it to establish that finite sets of finitely + supported objects are finitely supported. +*} + + section {* Induction Principles *} +text {* + While the use of functions as permutation provides us with a unique + representation for permutations (for example @{term "(a \ b)"} and + @{term "(b \ a)"} are equal permutations), this representation has + one draw back: it does not come readily with an induction principle. + Such an induction principle is handy for deriving properties like + + @{thm [display, indent=10] supp_perm_eq} + \noindent + However, it is not too difficult to derive an induction principle, + given the fact that we allow only permutations with a finite domain. +*} section {* Concrete Atom Types *} @@ -1167,6 +1198,12 @@ HOL-based languages. *} +section {* Related Work *} + +text {* + Add here comparison with old work. +*} + section {* Conclusion *} diff -r 5641981ec67d -r 74bd7bfb484b Pearl-jv/ROOT.ML --- a/Pearl-jv/ROOT.ML Mon May 03 08:52:15 2010 +0100 +++ b/Pearl-jv/ROOT.ML Tue May 04 05:36:43 2010 +0100 @@ -1,6 +1,7 @@ no_document use_thys ["../Nominal-General/Nominal2_Base", "../Nominal-General/Nominal2_Atoms", "../Nominal-General/Nominal2_Eqvt", + "../Nominal-General/Nominal2_Supp", "../Nominal-General/Atoms", "LaTeXsugar"]; diff -r 5641981ec67d -r 74bd7bfb484b Pearl-jv/document/root.tex --- a/Pearl-jv/document/root.tex Mon May 03 08:52:15 2010 +0100 +++ b/Pearl-jv/document/root.tex Tue May 04 05:36:43 2010 +0100 @@ -24,28 +24,21 @@ \begin{document} -\title{Proof Pearl: A New Foundation for Nominal Isabelle} +\title{Implementing the Nominal Logic Work in Isabelle/HOL} \author{Brian Huffman\inst{1} and Christian Urban\inst{2}} \institute{Portland State University \and Technical University of Munich} \maketitle \begin{abstract} Pitts et al introduced a beautiful theory about names and binding based on the -notions of permutation and support. The engineering challenge is to smoothly -adapt this theory to a theorem prover environment, in our case Isabelle/HOL. -We present a formalisation of this work that differs from our earlier approach -in two important respects: First, instead of representing permutations as -lists of pairs of atoms, we now use a more abstract representation based on -functions. Second, whereas the earlier work modeled different sorts of atoms -using different types, we now introduce a unified atom type that includes all -sorts of atoms. Interestingly, we allow swappings, that is permutations build from -two atoms, to be ill-sorted. As a result of these design changes, we can iron -out inconveniences for the user, considerably simplify proofs and also -drastically reduce the amount of custom ML-code. Furthermore we can extend the -capabilities of Nominal Isabelle to deal with variables that carry additional -information. We end up with a pleasing and formalised theory of permutations -and support, on which we can build an improved and more powerful version of -Nominal Isabelle. +notions of atoms, permutations and support. The engineering challenge +is to smoothly adapt this theory to a theorem prover environment, in our case +Isabelle/HOL. We present a formalisation of this work that is based on a +unified atom type (that includes all sorts of atoms) and that represents +permutations by bijective functions from atoms to atoms. Interestingly, we +allow swappings, which are permutations build from two atoms, to be +ill-sorted. Furthermore we can extend the nominal logic with names that carry +additional information. \end{abstract} % generated text of all theories