# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1279377864 -3600
# Node ID 34af7f2ca490efa033b580308d5959651cec77d0
# Parent  46be4145b922304c22459df3eb902cb159cbd227
some minor changes

diff -r 46be4145b922 -r 34af7f2ca490 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Sat Jul 17 12:01:04 2010 +0100
+++ b/Quotient-Paper/Paper.thy	Sat Jul 17 15:44:24 2010 +0100
@@ -243,10 +243,10 @@
   representation and abstraction functions, which in case of @{text "\<Union>"}
   generate the following definition
 
-  @{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat ((map Rep_fset \<circ> Rep_fset) S))"}
+  @{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat ((map_list Rep_fset \<circ> Rep_fset) S))"}
 
   \noindent
-  where @{term map} is the usual mapping function for lists. In this paper we
+  where @{term map_list} is the usual mapping function for lists. In this paper we
   will present a formal definition of our aggregate abstraction and
   representation functions (this definition was omitted in \cite{Homeier05}). 
   They generate definitions, like the one above for @{text "\<Union>"}, 
@@ -312,7 +312,7 @@
   underlying the first theorem.
 
   Like Homeier's, our work relies on map-functions defined for every type
-  constructor taking some arguments, for example @{text map} for lists. Homeier
+  constructor taking some arguments, for example @{text map_list} for lists. Homeier
   describes in \cite{Homeier05} map-functions for products, sums, options and
   also the following map for function types
 
@@ -414,7 +414,7 @@
   composing @{text "\<approx>\<^bsub>list\<^esub>"} will be necessary: given @{term "Quotient R Abs Rep"} 
   with @{text R} being an equivalence relation, then
 
-  @{text [display, indent=10] "Quotient (rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (Abs_fset \<circ> map Abs) (map Rep \<circ> Rep_fset)"}
+  @{text [display, indent=2] "Quotient (rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (Abs_fset \<circ> map_list Abs) (map_list Rep \<circ> Rep_fset)"}
 
   \vspace{-.5mm}
 *}
@@ -543,20 +543,21 @@
   \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\\
-  \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\\
+  \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors with @{text "\<alpha>s
+  \<kappa>\<^isub>q"} being the quotient of the raw type @{text "\<rho>s \<kappa>"}:}\\
   @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "Abs_\<kappa>\<^isub>q \<circ> (MAP(\<rho>s \<kappa>) (ABS (\<sigma>s', \<tau>s)))"}\\
   @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "(MAP(\<rho>s \<kappa>) (REP (\<sigma>s', \<tau>s))) \<circ> Rep_\<kappa>\<^isub>q"}
   \end{tabular}\hfill\numbered{ABSREP}
   \end{center}
   %
   \noindent
-  In the last two clauses we have that the type @{text "\<alpha>s
+  In the last two clauses we rely on the fact that the type @{text "\<alpha>s
   \<kappa>\<^isub>q"} is the quotient of the raw type @{text "\<rho>s \<kappa>"} (for example
   @{text "int"} and @{text "nat \<times> nat"}, or @{text "\<alpha> fset"} and @{text "\<alpha>
   list"}). The quotient construction ensures that the type variables in @{text
-  "\<rho>s"} must be among the @{text "\<alpha>s"}. The @{text "\<sigma>s'"} are given by the
-  matchers for the @{text "\<alpha>s"} when matching @{text "\<rho>s \<kappa>"} against
-  @{text "\<sigma>s \<kappa>"}.  The
+  "\<rho>s \<kappa>"} must be among the @{text "\<alpha>s"}. The @{text "\<sigma>s'"} are given by the
+  substitutions for the @{text "\<alpha>s"} when matching  @{text "\<sigma>s \<kappa>"} against
+  @{text "\<rho>s \<kappa>"}.  The
   function @{text "MAP"} calculates an \emph{aggregate map-function} for a raw
   type as follows:
   %
@@ -579,7 +580,7 @@
   In this case @{text MAP} generates  the 
   aggregate map-function:
 
-  @{text [display, indent=10] "\<lambda>a b. map_prod (map a) b"}
+  @{text [display, indent=10] "\<lambda>a b. map_prod (map_list a) b"}
   
   \noindent
   which is essential in order to define the corresponding aggregate 
@@ -591,20 +592,20 @@
   fset"}. Feeding these types into @{text ABS} gives us (after some @{text "\<beta>"}-simplifications)
   the abstraction function
 
-  @{text [display, indent=10] "(map (map id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr> Abs_fset \<circ> map id"}
+  @{text [display, indent=10] "(map_list (map_list id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr> Abs_fset \<circ> map_list id"}
 
   \noindent
   In our implementation we further
   simplify this function by rewriting with the usual laws about @{text
-  "map"}s and @{text "id"}, namely @{term "map id = id"} and @{text "f \<circ> id =
+  "map"}s and @{text "id"}, for example @{term "map_list id = id"} and @{text "f \<circ> id =
   id \<circ> f = f"}. This gives us the simpler abstraction function
 
-  @{text [display, indent=10] "(map Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}
+  @{text [display, indent=10] "(map_list 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"}
+  @{text [display, indent=10] "\<Union> \<equiv> ((map_list Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset) flat"}
 
   \noindent
   Note that by using the operator @{text "\<singlearr>"} and special clauses
@@ -686,7 +687,8 @@
   @{text "REL (\<sigma>, \<sigma>)"} & $\dn$ & @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}\smallskip\\
    \multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\ 
   @{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "rel_\<kappa> (REL (\<sigma>s, \<tau>s))"}\smallskip\\
-  \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\smallskip\\
+  \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors with @{text "\<alpha>s
+  \<kappa>\<^isub>q"} being the quotient of the raw type @{text "\<rho>s \<kappa>"}:}\smallskip\\
   @{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "rel_\<kappa>\<^isub>q (REL (\<sigma>s', \<tau>s))"}\\
   \end{tabular}\hfill\numbered{REL}
   \end{center}
@@ -694,7 +696,7 @@
   \noindent
   The @{text "\<sigma>s'"} in the last clause are calculated as in \eqref{ABSREP}:
   we know that type @{text "\<alpha>s \<kappa>\<^isub>q"} is the quotient of the raw type 
-  @{text "\<rho>s \<kappa>"}. The @{text "\<sigma>s'"} are determined by matching 
+  @{text "\<rho>s \<kappa>"}. The @{text "\<sigma>s'"} are the substitutions for @{text "\<alpha>s"} obtained by matching 
   @{text "\<rho>s \<kappa>"} and @{text "\<sigma>s \<kappa>"}.
 
   Let us return to the lifting procedure of theorems. Assume we have a theorem
@@ -762,7 +764,7 @@
   where the @{text "\<alpha>s"} stand for the type variables in the type of @{text "c\<^isub>r"}.
   In case of @{text cons} (which has type @{text "\<alpha> \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list"}) we have 
 
-  @{text [display, indent=10] "(Rep ---> map Rep ---> map Abs) cons = cons"}
+  @{text [display, indent=10] "(Rep ---> map_list Rep ---> map_list Abs) cons = cons"}
 
   \noindent
   under the assumption @{text "Quotient R Abs Rep"}. Interestingly, if we have
@@ -792,7 +794,7 @@
   %If @ {term R} is an equivalence relation and @ {term "Quotient R Abs Rep"}
   %then
   % 
-  %@ {text [display, indent=10] "Quotient (list_rel R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> map Abs) (map Rep o rep_fset)"}
+  %@ {text [display, indent=10] "Quotient (list_rel R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> map_list Abs) (map_list Rep o rep_fset)"}
   %%%
   %%%\noindent
   %%%this theorem will then instantiate the quotients needed in the