--- a/Quotient-Paper/Paper.thy	Sun Jun 13 07:14:53 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Sun Jun 13 13:42:37 2010 +0200
@@ -161,11 +161,12 @@
 
   \noindent
   However we often leave this typing information implicit for better
-  readability. Every abstraction and representation function stands for an
-  isomorphism between the non-empty subset and elements in the new type. They
-  are necessary for making definitions involving the new type. For example
-  @{text "0"} and @{text "1"} of type @{typ int} can be defined as
-
+  readability, but sometimes write @{text Abs_int} and @{text Rep_int} if the
+  typing information is important. Every abstraction and representation
+  function stands for an isomorphism between the non-empty subset and elements
+  in the new type. They are necessary for making definitions 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)"}
@@ -334,22 +335,39 @@
   @{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 "\<kappa>_map (ABS (\<sigma>s, \<tau>s))"}\\
-  @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "\<kappa>_map (REP (\<sigma>s, \<tau>s))"}\smallskip\\
+  @{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\\
   \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\\
-  @{text "ABS (\<sigma>s \<kappa>\<^isub>1, \<tau>s \<kappa>\<^isub>2)"} & $\dn$ & @{text "\<kappa>\<^isub>2_Abs \<circ> \<kappa>\<^isub>1_map (ABS (\<sigma>s', \<tau>s'))"}\\
-  @{text "REP (\<sigma>s \<kappa>\<^isub>1, \<tau>s \<kappa>\<^isub>2)"} & $\dn$ & @{text "\<kappa>\<^isub>1_map (REP (\<sigma>s', \<tau>s')) \<circ> \<kappa>\<^isub>2_Rep"}\\
+  @{text "ABS (\<sigma>s \<kappa>\<^isub>1, \<tau>s \<kappa>\<^isub>2)"} & $\dn$ & @{text "Abs_\<kappa>\<^isub>2 \<circ> (MAP(\<rho>s \<kappa>\<^isub>1) (ABS (\<sigma>s', \<tau>s')))"}\\
+  @{text "REP (\<sigma>s \<kappa>\<^isub>1, \<tau>s \<kappa>\<^isub>2)"} & $\dn$ & @{text "(MAP(\<rho>s \<kappa>\<^isub>1) (REP (\<sigma>s', \<tau>s'))) \<circ> Rep_\<kappa>\<^isub>2"}\\
   \end{tabular}
   \end{center}
 
+  \noindent
+  where in the last two clauses we have that the quotient type @{text "\<alpha>s \<kappa>\<^isub>2"} is a quotient of
+  the raw type @{text "\<rho>s \<kappa>\<^isub>1"} (for example @{text "\<alpha> fset"} and @{text "\<alpha> list"}). 
+  The quotient construction ensures that the type variables in @{text "\<rho>s"} 
+  must be amongst the @{text "\<alpha>s"}. Now the @{text "\<sigma>s'"} are given by the matchers 
+  for the @{text "\<alpha>s"} 
+  when matching  @{text "\<sigma>s \<kappa>\<^isub>2"} against @{text "\<alpha>s \<kappa>\<^isub>2"}; similarly the @{text "\<tau>s'"} are given by the 
+  same type-variables when matching @{text "\<tau>s \<kappa>\<^isub>1"} against @{text "\<rho>s \<kappa>\<^isub>1"}.
+  The function @{text "MAP"} calculates an \emph{aggregate map-function} for a type 
+  as follows:
+
   \begin{center}
   \begin{tabular}{rcl}
-  @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n) \<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m) \<kappa>\<^isub>2)"}  =  @{text "Abs_\<kappa>\<^isub>2 \<circ> (map \<kappa>\<^isub>1) (ABS(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (ABS(\<rho>\<^isub>p,\<nu>\<^isub>p)"}\\ 
-  @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n) \<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m) \<kappa>\<^isub>2)"}  =  @{text "(map \<kappa>\<^isub>1) (REP(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REP(\<rho>\<^isub>p,\<nu>\<^isub>p) \<circ> Rep_\<kappa>\<^isub>2"}\\
-  provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}
+  @{text "MAP' (\<alpha>)"} & $\dn$ & @{text "\<alpha>"}\\
+  @{text "MAP' (\<sigma>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (MAP'(\<sigma>s))"}\smallskip\\
+  @{text "MAP (\<sigma>)"} & $\dn$ & @{text "\<lambda>\<alpha>s. 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
+  term-variables inside the aggregate map-function generated by @{text "MAP'"}.
+
+
   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
   for compositional quotients. We illustrate the different behaviour of the