--- 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

--- 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 \<rightleftharpoons> b)"} and 
+  @{term "(b \<rightleftharpoons> 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 *}
 

--- 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"];
 

--- 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