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

--- a/Quotient-Paper/document/root.tex	Mon Jun 07 16:17:35 2010 +0200
+++ b/Quotient-Paper/document/root.tex	Thu Jun 10 10:53:51 2010 +0200
@@ -33,7 +33,7 @@
 quotient package by Homeier. In doing so we extended his work in order to deal
 with compositions of quotients. Also, we designed our quotient package so that
 every step in a quotient construction can be performed separately and as a
-result were able to specify completely the procedure of lifting theorems from
+result we were able to specify completely the procedure of lifting theorems from
 the raw level to the quotient level.  The importance to programming language
 research is that many properties of programming languages are more convenient
 to verify over $\alpha$-quotient terms, than over raw terms.