--- a/Quotient-Paper/Paper.thy	Thu Jun 10 14:53:28 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Thu Jun 10 14:53:45 2010 +0200
@@ -10,17 +10,16 @@
 print_syntax
 
 notation (latex output)
-  rel_conj ("_ OOO _" [53, 53] 52)
-and
-  "op -->" (infix "\<rightarrow>" 100)
-and
-  "==>" (infix "\<Rightarrow>" 100)
-and
-  fun_map (infix "\<longrightarrow>" 51)
-and
-  fun_rel (infix "\<Longrightarrow>" 51)
-and
-  list_eq (infix "\<approx>" 50) (* Not sure if we want this notation...? *)
+  rel_conj ("_ OOO _" [53, 53] 52) and
+  "op -->" (infix "\<rightarrow>" 100) and
+  "==>" (infix "\<Rightarrow>" 100) and
+  fun_map (infix "\<longrightarrow>" 51) and
+  fun_rel (infix "\<Longrightarrow>" 51) and
+  list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *)
+  fempty ("\<emptyset>\<^isub>f") and
+  funion ("_ \<union>\<^isub>f _") and
+  Cons ("_::_") 
+  
 
 ML {*
 fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n;
@@ -50,41 +49,72 @@
   \end{flushright}\smallskip
 
   \noindent
-  Isabelle is a generic theorem prover in which many logics can be implemented. 
-  The most widely used one, however, is
-  Higher-Order Logic (HOL). This logic consists of a small number of 
-  axioms and inference
-  rules over a simply-typed term-language. Safe reasoning in HOL is ensured by two very restricted 
-  mechanisms for extending the logic: one is the definition of new constants
-  in terms of existing ones; the other is the introduction of new types
-  by identifying non-empty subsets in existing types. It is well understood 
-  to use both mechanisms for dealing with quotient constructions in HOL (see for example 
-  \cite{Paulson06}).
-  For example the integers in Isabelle/HOL are constructed by a quotient construction over 
-  the type @{typ "nat \<times> nat"} and the equivalence relation
+  Isabelle is a generic theorem prover in which many logics can be
+  implemented. The most widely used one, however, is Higher-Order Logic
+  (HOL). This logic consists of a small number of axioms and inference rules
+  over a simply-typed term-language. Safe reasoning in HOL is ensured by two
+  very restricted mechanisms for extending the logic: one is the definition of
+  new constants in terms of existing ones; the other is the introduction of
+  new types by identifying non-empty subsets in existing types. It is well
+  understood how to use both mechanisms for dealing with quotient constructions in
+  HOL (see \cite{Homeier05,Paulson06}).  For example the integers
+  in Isabelle/HOL are constructed by a quotient construction over the type
+  @{typ "nat \<times> nat"} and the equivalence relation
 
-% I would avoid substraction for natural numbers.
+  @{text [display, indent=10] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 + n\<^isub>2 = m\<^isub>1 + m\<^isub>2"}
 
-  @{text [display] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 - n \<^isub>2 = m\<^isub>1 - m \<^isub>2"}
+  \noindent
+  This constructions yields the new type @{typ int} and definitions for @{text
+  "0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of 
+  natural numbers (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations 
+  such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined 
+  in terms of operations on pairs of natural numbers (namely @{text "add\<^bsub>nat\<times>nat\<^esub>
+  (x\<^isub>1, y\<^isub>1) (x\<^isub>2, y\<^isub>2) \<equiv> (x\<^isub>1 +
+  x\<^isub>2, y\<^isub>1 + y\<^isub>2)"}).  Similarly one can construct the
+  type of finite sets by quotienting lists according to the equivalence
+  relation
+
+  @{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"}
 
   \noindent
-  Similarly one can construct the type of finite sets by quotienting lists
-  according to the equivalence relation
+  which states that two lists are equivalent if every element in one list is also
+  member in the other (@{text "\<in>"} stands here for membership in lists). The
+  empty finite set, written @{term "{||}"} can then be defined as the 
+  empty list and union of two finite sets, written @{text "\<union>\<^isub>f"}, as list append. 
 
-  @{text [display] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"}
+  Another important area of quotients is reasoning about programming language
+  calculi. A simple example are lambda-terms defined as
+
+  \begin{center}
+  @{text "t ::= x | t t | \<lambda>x.t"}
+  \end{center}
 
   \noindent
-  where @{text "\<in>"} stands for membership in a list.
+  The difficulty with this definition of lambda-terms arises when, for 
+  example, proving formally the substitution lemma ...
+  On the other hand if we reason about alpha-equated lambda-terms, that means
+  terms quotient according to alpha-equivalence, then reasoning infrastructure
+  can be introduced that make the formal proof of the substitution lemma
+  almost trivial. 
+
 
-  The problem is that in order to start reasoning about, for example integers, 
-  definitions and theorems need to be transferred, or \emph{lifted}, 
-  from the ``raw'' type @{typ "nat \<times> nat"} to the quotient type @{typ int}. 
-  This lifting usually requires a lot of tedious reasoning effort.
-  The purpose of a \emph{quotient package} is to ease the lifting and automate
-  the reasoning involved as much as possible. Such a package is a central
-  component of the new version of Nominal Isabelle where representations 
-  of alpha-equated terms are constructed according to specifications given by
-  the user. 
+  The problem is that in order to be able to reason about integers, finite sets
+  and alpha-equated lambda-terms one needs to establish a reasoning infrastructure by
+  transferring, or \emph{lifting}, definitions and theorems from the ``raw''
+  type @{typ "nat \<times> nat"} to the quotient type @{typ int} (similarly for
+  @{text "\<alpha> list"} and finite sets of type @{text "\<alpha>"}, and also for raw lambda-terms
+  and alpha-equated lambda-terms). This lifting usually
+  requires a \emph{lot} of tedious reasoning effort.  The purpose of a \emph{quotient
+  package} is to ease the lifting and automate the reasoning as much as
+  possible. While for integers and finite sets teh tedious reasoning needs
+  to be done only once, Nominal Isabelle providing a reasoning infrastructure 
+  for binders and @{text "\<alpha>"}-equated terms it needs to be done over and over 
+  again.
+
+  Such a package is a central component of the new version of
+  Nominal Isabelle where representations of alpha-equated terms are
+  constructed according to specifications given by the user.
+
   
   In the context of HOL, there have been several quotient packages (...). The
   most notable is the one by Homeier (...) implemented in HOL4. However, what is