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