# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1276443632 -7200
# Node ID ad725de6e39be8ee6cbb51d743abbd6589298806
# Parent  8035515bbbc6df9f0854bb4fc0b9ed57439182ce
more on the constant lifting section

diff -r 8035515bbbc6 -r ad725de6e39b Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Sun Jun 13 17:01:15 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Sun Jun 13 17:40:32 2010 +0200
@@ -305,42 +305,59 @@
   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
+  bool"}. The user-visible part of the declaration is therefore 
 
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \isacommand{quotient\_type}~~@{text "\<alpha>s \<kappa>\<^isub>q = \<sigma> / R"}
+  \end{isabelle}
+
+  \noindent
+  and a proof that @{text "R"} is indeed an equivalence relation.
+  Given this data, we can internally 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
+  being the (non-empty) 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
 
   \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
-  
+  \noindent 
+  and relating the new quotient type and equivalence classes of the raw
+  type. However, as Homeier \cite{Homeier05} noted, it is much more convenient
+  to work with the following derived abstraction and representation functions
+
   \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
+  on the expense of having to use Hilbert's choice operator @{text "\<epsilon>"} in the
+  definition of @{text "Rep_\<kappa>\<^isub>q"}. These derived notions relate the quotient type
+  and the raw type directly, as can be seen from their type, namely @{text "\<sigma>
+  \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"} and @{text "\<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma>"}, respectively.  Given that
+  @{text "R"} is an equivalence relation, the following property
 
   @{text [display, indent=10] "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}
 
   \noindent
   holds (for the proof see \cite{Homeier05}).
 
+  The next step is to lift definitions over the raw type to definitions over the
+  quotient type. For this we providing the declaration
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \isacommand{quotient\_definition}~~@{text "c :: \<tau>"}~\isacommand{is}~@{text "c' :: \<sigma>"}
+  \end{isabelle}
+
   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
@@ -415,7 +432,7 @@
   where we already performed some @{text "\<beta>"}-simplifications. In our implementation
   we further simplified this by noticing the usual laws about @{text "map"}s and @{text "id"},
   namely @{term "map id = id"} and 
-  @{text "f \<circ> id = id \<circ> f = f"}. This gives us the simplified abstarction function
+  @{text "f \<circ> id = id \<circ> f = f"}. This gives us the simplified abstraction function
   
   @{text [display, indent=10] "(map Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}
 
@@ -439,7 +456,7 @@
 
   For every type map function we require the property that @{term "map id = id"}.
   With this we can compactify the term, removing the identity mappings,
-  obtaining a definition that is the same as the one privided by Homeier
+  obtaining a definition that is the same as the one provided by Homeier
   in the cases where the internal type does not change.
 
   {\it we should be able to prove}