--- a/Quotient-Paper/Paper.thy	Sun Jun 13 13:42:37 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Sun Jun 13 14:39:55 2010 +0200
@@ -332,8 +332,8 @@
   @{text "ABS (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\\
   @{text "REP (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\smallskip\\
   \multicolumn{3}{@ {\hspace{-4mm}}l}{function types:}\\ 
-  @{text "ABS (\<sigma>\<^isub>1 \<rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "REP (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> ABS (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\\
-  @{text "REP (\<sigma>\<^isub>1 \<rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> REP (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\smallskip\\
+  @{text "ABS (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "REP (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> ABS (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\\
+  @{text "REP (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> REP (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\smallskip\\
   \multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\ 
   @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (ABS (\<sigma>s, \<tau>s))"}\\
   @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (REP (\<sigma>s, \<tau>s))"}\smallskip\\
@@ -356,17 +356,42 @@
 
   \begin{center}
   \begin{tabular}{rcl}
-  @{text "MAP' (\<alpha>)"} & $\dn$ & @{text "\<alpha>"}\\
+  @{text "MAP' (\<alpha>)"} & $\dn$ & @{text "a"}\\
+  @{text "MAP' (\<kappa>)"} & $\dn$ & @{text "id"}\\
   @{text "MAP' (\<sigma>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (MAP'(\<sigma>s))"}\smallskip\\
-  @{text "MAP (\<sigma>)"} & $\dn$ & @{text "\<lambda>\<alpha>s. MAP'(\<sigma>)"}  
+  @{text "MAP (\<sigma>)"} & $\dn$ & @{text "\<lambda>as. MAP'(\<sigma>)"}  
   \end{tabular}
   \end{center}
 
   \noindent
-  In this definition we abuse the fact that we can interpret type-variables as 
-  term variables, and in the last clause build the abstraction over all
+  In this definition we abuse the fact that we can interpret type-variables @{text \<alpha>} as 
+  term variables @{text a}, and in the last clause build an abstraction over all
   term-variables inside the aggregate map-function generated by @{text "MAP'"}.
+  This aggregate map-function is necessary if we build quotients, say @{text "(\<alpha>, \<beta>) foo"},
+  out of compound raw types, say @{text "(\<alpha> list) \<times> \<beta>"}. In this case @{text MAP}
+  generates the aggregate map-function:
 
+  @{text [display, indent=10] "\<lambda>a b. map_prod (map a) b"}
+  
+  \noindent
+  Returning to our example about @{term "concat"} and @{term "fconcat"} which have the
+  types @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"} and @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha> fset"}. Feeding this
+  into @{text ABS} gives us the abstraction function:
+
+  @{text [display, indent=10] "(map (map id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr> Abs_fset \<circ> map id"}
+
+  \noindent
+  where we already performed some @{text "\<beta>"}-simplifications. In our implementation
+  we further simplified this by noticing the usual laws about @{text "map"}s and @{text "id"},
+  namely @{term "map id = id"} and 
+  @{text "f \<circ> id = id \<circ> f = f"}. This gives us the simplified abstarction function
+  
+  @{text [display, indent=10] "(map Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}
+
+  \noindent
+  which we can use for defining @{term "fconcat"} as follows
+
+  @{text [display, indent=10] "\<Union> \<equiv> ((map Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset) flat"}
 
   Apart from the last 2 points the definition is same as the one implemented in
   in Homeier's HOL package. Adding composition in last two cases is necessary
@@ -394,6 +419,9 @@
   then @{text "Abs"} is of type @{text "\<sigma> \<Rightarrow> \<tau>"} and @{text "Rep"} of type
   @{text "\<tau> \<Rightarrow> \<sigma>"}.
   \end{lemma}
+
+  This lemma fails in the over-simplified abstraction and representation function used
+  in Homeier's quotient package.
 *}
 
 subsection {* Respectfulness *}