--- a/Quotient-Paper/Paper.thy	Mon Jun 07 16:17:35 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Thu Jun 10 10:53:51 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;
@@ -57,7 +56,7 @@
   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
+  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
@@ -65,11 +64,11 @@
   @{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"}
 
   \noindent
-  This constructions yields the type @{typ int} and definitions for @{text
-  "0::int"} and @{text "1::int"} in terms of pairs of natural numbers can be
-  given (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>
+  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
@@ -79,13 +78,32 @@
 
   \noindent
   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).
+  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. 
+
+  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}
 
-  The problem is that in order to be able to reason about integers and
-  finite sets, one needs to establish a reasoning infrastructure by
+  \noindent
+  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 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>"}). This lifting usually
+  @{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