diff -r 22c6b6144abd -r 8035515bbbc6 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Sun Jun 13 14:39:55 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Sun Jun 13 17:01:15 2010 +0200
@@ -114,7 +114,7 @@
   The purpose of a \emph{quotient package} is to ease the lifting of theorems
   and automate the definitions and reasoning as much as possible. In the
   context of HOL, there have been a few quotient packages already
-  \cite{harrison-thesis,Slotosch97}. The most notable is the one by Homeier
+  \cite{harrison-thesis,Slotosch97}. The most notable one is by Homeier
   \cite{Homeier05} implemented in HOL4.  The fundamental construction these
   quotient packages perform can be illustrated by the following picture:
 
@@ -144,19 +144,19 @@
   \end{center}
 
   \noindent
-  The starting point is an existing type, often referred to as the
-  \emph{raw level}, over which an equivalence relation given by the user is
+  The starting point is an existing type, often referred to as the \emph{raw
+  type}, over which an equivalence relation given by the user is
   defined. With this input the package introduces a new type, to which we
-  refer as the \emph{quotient level}. This type comes with an
+  refer as the \emph{quotient type}. This type comes with an
   \emph{abstraction} and a \emph{representation} function, written @{text Abs}
-  and @{text Rep}. These functions relate elements in the existing type to
-  ones in the new type and vice versa; they can be uniquely identified by
-  their type. For example for the integer quotient construction the types of
-  @{text Abs} and @{text Rep} are
-
+  and @{text Rep}.\footnote{Actually they need to be derived from slightly
+  more basic functions. We will show the details later. } These functions
+  relate elements in the existing type to ones in the new type and vice versa;
+  they can be uniquely identified by their type. For example for the integer
+  quotient construction the types of @{text Abs} and @{text Rep} are
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  @{text "Abs::nat \<times> nat \<Rightarrow> int"}\hspace{10mm}@{text "Rep::int \<Rightarrow> nat \<times> nat"}
+  @{text "Abs :: nat \<times> nat \<Rightarrow> int"}\hspace{10mm}@{text "Rep :: int \<Rightarrow> nat \<times> nat"}
   \end{isabelle}
 
   \noindent
@@ -192,7 +192,7 @@
 
   \noindent
   We expect that the corresponding operator on finite sets, written @{term "fconcat"},
-  behaves as follows:
+  builds the union of finite sets of finite sets:
 
   @{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]}
 
@@ -205,7 +205,7 @@
   the abstraction of the result is \emph{not} enough. The reason is that case in case
   of @{text "\<Union>"} we obtain the incorrect definition
 
-  @{text [display, indent=10] "\<Union> S \<equiv> Abs (flat (Rep S))"}
+  @{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat (Rep_fset S))"}
 
   \noindent
   where the right-hand side is not even typable! This problem can be remedied in the
@@ -216,7 +216,7 @@
   representation and abstraction functions, which in case of @{text "\<Union>"}
   generate the following definition
 
-  @{text [display, indent=10] "\<Union> S \<equiv> Abs (flat ((map Rep \<circ> Rep) S))"}
+  @{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat ((map Rep_fset \<circ> Rep_fset) S))"}
 
   \noindent
   where @{term map} is the usual mapping function for lists. In this paper we
@@ -294,13 +294,52 @@
       @{text "|"} & @{text "\<lambda>x\<^isup>\<sigma>. t"} & \textrm{(abstraction)} \\ \nonumber
   \end{eqnarray}
 
+  {\it Say more about containers / maping functions }
+
 *}
 
 section {* Quotient Types and Lifting of Definitions *}
 
-(* Say more about containers? *)
+text {*
+  The first step in a quotient constructions is to take a name for the new
+  type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation defined over a
+  raw type, say @{text "\<sigma>"}. The equivalence relation for the quotient
+  construction, lets say @{text "R"}, must then be of type @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow>
+  bool"}. Given this data, we can automatically declare the quotient type as
+
+  
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \isacommand{typedef}~~@{text "\<alpha>s \<kappa>\<^isub>q = {c. \<exists>x. c = R x}"}
+  \end{isabelle}
+
+  \noindent
+  being the set of equivalence classes of @{text "R"}. The restriction in this declaration
+  is that the type variables in the raw type @{text "\<sigma>"} must be included in the 
+  type variables @{text "\<alpha>s"} declared for @{text "\<kappa>\<^isub>q"}. HOL will provide us 
+  with abstraction and representation functions having the type
 
-text {*
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{text "abs_\<kappa>\<^isub>q :: \<sigma> set \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"}\hspace{10mm}@{text "rep_\<kappa>\<^isub>q :: \<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma> set"}
+  \end{isabelle}
+
+  \noindent
+  relating the new quotient type and raw type. However, as Homeier noted, it is easier 
+  to work with the following derived definitions
+  
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{text "Abs_\<kappa>\<^isub>q x \<equiv> abs_\<kappa>\<^isub>q (R x)"}\hspace{10mm}@{text "Rep_\<kappa>\<^isub>q x \<equiv> \<epsilon> (rep_\<kappa>\<^isub>q x)"}
+  \end{isabelle}
+  
+  \noindent
+  on the expense of having to use Hilbert's choice operator @{text "\<epsilon>"}. With these
+  definitions the abstraction and representation functions relate directly the 
+  quotient and raw types (their type is  @{text "\<sigma> \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"} and @{text "\<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma>"}, 
+  respectively). We can show that the property
+
+  @{text [display, indent=10] "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}
+
+  \noindent
+  holds (for the proof see \cite{Homeier05}).
 
   To define a constant on the lifted type, an aggregate abstraction
   function is applied to the raw constant. Below we describe the operation
@@ -317,17 +356,9 @@
   as follows:
 
   {\it the first argument is the raw type and the second argument the quotient type}
-
-
+  %
   \begin{center}
-  \begin{tabular}{rcl}
-
-  % type variable case says that variables must be equal...therefore subsumed by the equal case below
-  %
-  %\multicolumn{3}{@ {\hspace{-4mm}}l}{type variables:}\\ 
-  %@{text "ABS (\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} & $\dn$ & @{text "id"}\\
-  %@{text "REP (\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} & $\dn$ & @{text "id"}\smallskip\\
-
+  \begin{longtable}{rcl}
   \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\ 
   @{text "ABS (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\\
   @{text "REP (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\smallskip\\
@@ -338,19 +369,19 @@
   @{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 "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}
+  @{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{longtable}
   \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"}). 
+  where in the last two clauses we have that the quotient type @{text "\<alpha>s \<kappa>\<^isub>q"} is a quotient of
+  the raw type @{text "\<rho>s \<kappa>"} (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"}.
+  when matching  @{text "\<sigma>s \<kappa>\<^isub>q"} against @{text "\<alpha>s \<kappa>\<^isub>q"}; similarly the @{text "\<tau>s'"} are given by the 
+  same type-variables when matching @{text "\<tau>s \<kappa>"} against @{text "\<rho>s \<kappa>"}.
   The function @{text "MAP"} calculates an \emph{aggregate map-function} for a type 
   as follows: