--- a/Quotient-Paper/Paper.thy	Fri Jun 11 14:04:58 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Fri Jun 11 16:36:02 2010 +0200
@@ -17,7 +17,9 @@
   fempty ("\<emptyset>\<^isub>f") and
   funion ("_ \<union>\<^isub>f _") and
   finsert ("{_} \<union>\<^isub>f _") and 
-  Cons ("_::_") 
+  Cons ("_::_") and
+  concat ("flat") and
+  fconcat ("fset'_flat")
  
   
 
@@ -99,13 +101,17 @@
   proof of the substitution lemma almost trivial.
 
   The difficulty is that in order to be able to reason about integers, finite
-  sets and $\alpha$-equated lambda-terms one needs to establish a reasoning
+  sets or $\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 finite sets 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. 
+  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. In the context of HOL, there have been
+  several quotient packages (...). The most notable is the one by Homeier
+  (...) implemented in HOL4.  The fundamental construction the quotient
+  package performs can be illustrated by the following picture:
 
   \begin{center}
   \mbox{}\hspace{20mm}\begin{tikzpicture}
@@ -126,29 +132,69 @@
   
   \draw[->, very thick] (-1.8, 0.36) -- (-0.1,0.36);
   \draw[<-, very thick] (-1.8, 0.16) -- (-0.1,0.16);
-  \draw (-0.95, 0.26) node[above=0.4mm] {Rep};
-  \draw (-0.95, 0.26) node[below=0.4mm] {Abs};
+  \draw (-0.95, 0.26) node[above=0.4mm] {@{text Rep}};
+  \draw (-0.95, 0.26) node[below=0.4mm] {@{text Abs}};
 
   \end{tikzpicture}
   \end{center}
 
+  \noindent
+  The starting point is an existing type over which a user-given equivalence
+  relation is defined. With this input, the package introduces a new type,
+  which comes with two associated abstraction and representation functions,
+  @{text Abs} and @{text Rep}, that relate elements in the existing and new
+  type. These two function represent an isomorphism between the non-empty
+  subset and the new type.
 
-  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
-  surprising, none of them can deal compositions of quotients, for example with 
-  lifting theorems about @{text "concat"}:
+  The abstractions and representation functions are important for defining
+  concepts involving the new type. For example @{text "0"} and @{text "1"}
+  of type @{typ int} can be defined as
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{text "0 \<equiv> Abs (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs (1, 0)"}
+  \end{isabelle}
+
+  \noindent
+  Slightly more complicated is the definition of @{text "add"} with type 
+  @{typ "int \<Rightarrow> int \<Rightarrow> int"}. Its definition looks as follows
+
+  @{text [display, indent=10] "add x y \<equiv> Abs (add\<^bsub>nat\<times>nat\<^esub> (Rep x) (Rep y))"}
+  
+  \noindent
+  where we have to take first the representation of @{text x} and @{text y},
+  add them according to @{text "add\<^bsub>nat\<times>nat\<^esub>"} and then take the
+  abstraction of the result.  This is all straightforward and the existing
+  quotient packages can deal with such definitions. But what is surprising
+  that none of them can deal with more complicated definitions involving
+  \emph{compositions} of quotients. Such compositions are needed for example
+  when quotienting finite lists (@{text "\<alpha> list"}) to yield finite sets
+  (@{text "\<alpha> fset"}). There one would like to have a corresponding definition
+  for the operator @{term "concat"}, which flattens lists of lists as follows
 
   @{thm [display, indent=10] concat.simps(1) concat.simps(2)[no_vars]}
 
   \noindent
-  One would like to lift this definition to the operation:
+  We expect that the corresponding operator on finite sets, written @{term "fconcat"},
+  behaves as follows:
 
   @{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]}
 
   \noindent
-  What is special about this operation is that we have as input
-  lists of lists which after lifting turn into finite sets of finite
-  sets.
+  The problem is that we want to quotient lists to obtain finite sets and 
+  @{term concat} is of type @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"}. We expect
+  that @{term "fconcat"} has type @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha> fset"}. But 
+  what should its definition be? It is not possible to just take the representation
+  of the argument and then take the abstraction of the result of flattening 
+  the resulting list. The problem is that a single @{text "Rep"} only gives
+  us lists of finite sets, not lists of lists. It turns out that we need
+  to be able to build aggregate representation and abstraction function, which in
+  case of @{term "fconcat"} produce the following definition
+
+  @{text [display, indent=10] "fset_flat S \<equiv> Abs (concat ((map Rep \<circ> Rep) S))"}
+
+  \noindent
+  where @{term map} is the usual mapping function for lists.
+
 *}
 
 subsection {* Contributions *}