--- a/Quotient-Paper/Paper.thy	Tue May 25 18:38:52 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Wed May 26 12:11:58 2010 +0200
@@ -5,8 +5,28 @@
 begin
 
 notation (latex output)
+  rel_conj ("_ OOO _" [53, 53] 52)
+and
+  fun_map ("_ ---> _" [51, 51] 50)
+and
   fun_rel ("_ ===> _" [51, 51] 50)
 
+ML {*
+fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n;
+fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
+  let
+    val concl =
+      Object_Logic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t)
+  in
+    case concl of (_ $ l $ r) => proj (l, r)
+    | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
+  end);
+*}
+setup {*
+  Term_Style.setup "rhs1" (style_lhs_rhs (nth_conj 0)) #>
+  Term_Style.setup "rhs2" (style_lhs_rhs (nth_conj 1)) #>
+  Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2))
+*}
 (*>*)
 
 section {* Introduction *}
@@ -27,6 +47,8 @@
   For example the integers in Isabelle/HOL are constructed by a quotient construction over 
   the type @{typ "nat \<times> nat"} and the equivalence relation
 
+% I would avoid substraction for natural numbers.
+
   @{text [display] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 - n \<^isub>2 = m\<^isub>1 - m \<^isub>2"}
 
   \noindent
@@ -84,12 +106,9 @@
   \item We allow lifting only some occurrences of quotiented
     types. Rsp/Prs extended. (used in nominal)
 
-  \item We regularize more thanks to new lemmas. (inductions in
-    nominal).
-
   \item The quotient package is very modular. Definitions can be added
     separately, rsp and prs can be proved separately and theorems can
-    be lifted on a need basis. (useful with type-classes).
+    be lifted on a need basis. (useful with type-classes). 
 
   \item Can be used both manually (attribute, separate tactics,
     rsp/prs databases) and programatically (automated definition of
@@ -101,18 +120,73 @@
 
 section {* Quotient Type*}
 
+
+
 text {*
-  Defintion of quotient,
+  In this section we present the definitions of a quotient that follow
+  those by Homeier, the proofs can be found there.
+
+  \begin{definition}[Quotient]
+  A relation $R$ with an abstraction function $Abs$
+  and a representation function $Rep$ is a \emph{quotient}
+  if and only if:
 
-  Equivalence,
+  \begin{enumerate}
+  \item @{thm (rhs1) Quotient_def[of "R", no_vars]}
+  \item @{thm (rhs2) Quotient_def[of "R", no_vars]}
+  \item @{thm (rhs3) Quotient_def[of "R", no_vars]}
+  \end{enumerate}
+
+  \end{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}
+
+  The main theorems for building higher order quotients is:
+  \begin{lemma}[Function Quotient]
+  If @{thm (prem 1) fun_quotient[no_vars]} and @{thm (prem 2) fun_quotient[no_vars]}
+  then @{thm (concl) fun_quotient[no_vars]}
+  \end{lemma}
+
 *}
 
 section {* Constants *}
 
+(* Describe what containers are? *)
+
 text {*
-  Rep and Abs, Rsp and Prs
+  \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:
+
+  \begin{itemize}
+  \item For equal types or free type variables return identity.
+
+  \item For function types recurse, change the Rep/Abs flag to
+     the opposite one for the domain type and compose the
+     results with @{term "fun_map"}.
+
+  \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.
+  \end{itemize}
+
+
+
+  Rsp and Prs
 *}
 
 section {* Lifting Theorems *}