--- a/Quotient-Paper/Paper.thy	Wed May 26 16:09:09 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Wed May 26 16:17:49 2010 +0200
@@ -11,6 +11,8 @@
   fun_map ("_ ---> _" [51, 51] 50)
 and
   fun_rel ("_ ===> _" [51, 51] 50)
+and
+  list_eq (infix "\<approx>" 50) (* Not sure if we want this notation...? *)
 
 ML {*
 fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n;
@@ -80,9 +82,10 @@
   @{thm concat.simps(2)[no_vars]}
 
   \noindent
-  One would like to lift this definition to the operation
-  
-  @{text [display] "union definition"}
+  One would like to lift this definition to the operation:
+
+  @{thm fconcat_empty[no_vars]}\\
+  @{thm fconcat_insert[no_vars]}
 
   \noindent
   What is special about this operation is that we have as input
@@ -102,7 +105,7 @@
   \item We define quotient composition, function map composition and
     relation map composition. This lets lifting polymorphic types with
     subtypes quotiented as well. We extend the notions of
-    respectfullness and preservation to cope with quotient
+    respectfulness and preservation to cope with quotient
     composition.
 
   \item We allow lifting only some occurrences of quotiented
@@ -141,7 +144,7 @@
 
   \end{definition}
 
-  \begin{definition}[Relation map and function map]
+  \begin{definition}[Relation map and function map]\\
   @{thm fun_rel_def[no_vars]}\\
   @{thm fun_map_def[no_vars]}
   \end{definition}
@@ -156,19 +159,23 @@
 
 section {* Constants *}
 
-(* Describe what containers are? *)
+(* Say more about containers? *)
 
 text {*
-  \begin{definition}[Composition of Relations]
-  @{abbrev "rel_conj R1 R2"}
-  \end{definition}
 
-  The first operation that we describe is the generation of
-  aggregate Abs or Rep function for two given compound types.
-  This operation will be used for the constant defnitions
-  and for the translation of theorems statements. It relies on
-  knowing map functions and relation functions for container types.
-  It follows the following algorithm:
+  To define a constant on the lifted type, an aggregate abstraction
+  function is applied to the raw constant. Below we describe the operation
+  that generates
+  an aggregate @{term "Abs"} or @{term "Rep"} function given the
+  compound raw type and the compound quotient type.
+  This operation will also be used in translations of theorem statements
+  and in the lifting procedure.
+
+  The operation is additionally able to descend into types for which
+  maps are known. Such maps for most common types (list, pair, sum,
+  option, \ldots) are described in Homeier, and our algorithm uses the
+  same kind of maps. Given the raw compound type and the quotient compound
+  type the Rep/Abs algorithm does:
 
   \begin{itemize}
   \item For equal types or free type variables return identity.
@@ -180,15 +187,65 @@
   \item For equal type constructors use the appropriate map function
      applied to the results for the arguments.
 
-  \item For unequal type constructors are unequal, we look in the
-    quotients information for a raw type quotient type pair that
-    matches the given types. We apply the environment to the arguments
-    and recurse composing it with the aggregate map function.
+  \item For unequal type constructors, look in the quotients information
+    for a quotient type that matches, and instantiate the raw type
+    appropriately getting back an instantiation environment. We apply
+    the environment to the arguments and recurse composing it with the
+    aggregate map function.
   \end{itemize}
 
+  The first three points above are identical to the algorithm present in
+  in Homeier's HOL implementation, below is the definition of @{term fconcat}
+  that shows the last step:
 
+  @{thm fconcat_def[no_vars]}
+
+  The aggregate @{term Abs} function takes a finite set of finite sets
+  and applies @{term "map rep_fset"} composed with @{term rep_fset} to
+  its input, obtaining a list of lists, passes the result to @{term concat}
+  obtaining a list and applies @{term abs_fset} obtaining the composed
+  finite set.
+*}
+
+subsection {* Respectfulness *}
+
+text {*
+
+  A respectfulness lemma for a constant states that the equivalence
+  class returned by this constant depends only on the equivalence
+  classes of the arguments applied to the constant. This can be
+  expressed in terms of an aggregate relation between the constant
+  and itself, for example the respectfullness for @{term "append"}
+  can be stated as:
+
+  @{thm append_rsp[no_vars]}
 
-  Rsp and Prs
+  Which is equivalent to:
+
+  @{thm append_rsp[no_vars,simplified fun_rel_def]}
+
+  Below we show the algorithm for finding the aggregate relation.
+  This algorithm uses
+  the relation composition which we define as:
+
+  \begin{definition}[Composition of Relations]
+  @{abbrev "rel_conj R1 R2"}
+  \end{definition}
+
+  Given an aggregate raw type and quotient type:
+
+  \begin{itemize}
+  \item ...
+  \end{itemize}
+
+  Aggregate @{term "Rep"} and @{term "Abs"} functions are also
+  present in composition quotients. An example composition quotient
+  theorem that needs to be proved is the one needed to lift theorems
+  about concat:
+
+  @{thm quotient_compose_list[no_vars]}
+
+  Prs
 *}
 
 section {* Lifting Theorems *}