--- a/Quotient-Paper/Paper.thy	Fri Jun 11 17:52:06 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Fri Jun 11 21:58:25 2010 +0200
@@ -14,12 +14,12 @@
   fun_map (infix "\<longrightarrow>" 51) and
   fun_rel (infix "\<Longrightarrow>" 51) and
   list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *)
-  fempty ("\<emptyset>\<^isub>f") and
-  funion ("_ \<union>\<^isub>f _") and
-  finsert ("{_} \<union>\<^isub>f _") and 
+  fempty ("\<emptyset>") and
+  funion ("_ \<union> _") and
+  finsert ("{_} \<union> _") and 
   Cons ("_::_") and
   concat ("flat") and
-  fconcat ("fset'_flat")
+  fconcat ("\<Union>")
  
   
 
@@ -58,7 +58,7 @@
   very restricted mechanisms for extending the logic: one is the definition of
   new constants in terms of existing ones; the other is the introduction of
   new types by identifying non-empty subsets in existing types. It is well
-  understood how to use both mechanisms for dealing with many quotient
+  understood how to use both mechanisms for dealing with quotient
   constructions in HOL (see \cite{Homeier05,Paulson06}).  For example the
   integers in Isabelle/HOL are constructed by a quotient construction over the
   type @{typ "nat \<times> nat"} and the equivalence relation
@@ -74,7 +74,7 @@
   "add\<^bsub>nat\<times>nat\<^esub> (n\<^isub>1, m\<^isub>1) (n\<^isub>2,
   m\<^isub>2) \<equiv> (n\<^isub>1 + n\<^isub>2, m\<^isub>1 + m\<^isub>2)"}).
   Similarly one can construct the type of finite sets, written @{term "\<alpha> fset"}, 
-  by quotienting @{text "\<alpha> list"} according to the equivalence relation
+  by quotienting the type @{text "\<alpha> list"} according to the equivalence relation
 
   @{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"}
 
@@ -82,7 +82,7 @@
   which states that two lists are equivalent if every element in one list is also
   member in the other (@{text "\<in>"} stands here for membership in lists). The
   empty finite set, written @{term "{||}"}, can then be defined as the 
-  empty list and the union of two finite sets, written @{text "\<union>\<^isub>f"}, as list append. 
+  empty list and the union of two finite sets, written @{text "\<union>"}, as list append. 
 
   An area where quotients are ubiquitous is reasoning about programming language
   calculi. A simple example is the lambda-calculus, whose ``raw'' terms are defined as
@@ -96,8 +96,8 @@
   \cite[Pages 94--104]{CurryFeys58} for some ``rough'' sketches of a proof
   about ``raw'' lambda-terms). In contrast, if we reason about
   $\alpha$-equated lambda-terms, that means terms quotient according to
-  $\alpha$-equivalence, then the reasoning infrastructure provided by, 
-  for example, Nominal Isabelle \cite{UrbanKaliszyk11} makes the formal 
+  $\alpha$-equivalence, then the reasoning infrastructure provided, 
+  for example, by Nominal Isabelle \cite{UrbanKaliszyk11} makes the formal 
   proof of the substitution lemma almost trivial. 
 
   The difficulty is that in order to be able to reason about integers, finite
@@ -106,16 +106,16 @@
   from the ``raw'' type @{typ "nat \<times> nat"} to the quotient type @{typ int}
   (similarly for finite sets and $\alpha$-equated lambda-terms). This lifting
   usually requires a \emph{lot} of tedious reasoning effort \cite{Paulson06}.  
-  It is feasible to to this work manually if one has only a few quotient
-  constructions, but if they have to be done over and over again as in 
+  It is feasible to to this work manually, if one has only a few quotient
+  constructions at hand. But if they have to be done over and over again as in 
   Nominal Isabelle, then manual reasoning is not an option.
 
-  The purpose of a \emph{quotient package} is to ease the lifting and automate
-  the 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{Homeier05} implemented in HOL4.
-  The fundamental construction these quotient packages perform can be
-  illustrated by the following picture:
+  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{Homeier05} implemented in HOL4.  The fundamental construction these
+  quotient packages perform can be illustrated by the following picture:
 
   \begin{center}
   \mbox{}\hspace{20mm}\begin{tikzpicture}
@@ -143,15 +143,15 @@
   \end{center}
 
   \noindent
-  The starting point is an existing type over which a user-given equivalence
-  relation is defined. With this input, the package introduces a new type,
-  which comes with two associated abstraction and representation functions, written
-  @{text Abs} and @{text Rep}. They relate elements in the existing and new
-  type and can be uniquely identified by their type (which however we omit for 
-  better readability). These two function represent an isomorphism between 
-  the non-empty subset and the new type. They are necessary making definitions
-  over the new type. For example @{text "0"} and @{text "1"}
-  of type @{typ int} can be defined as
+  The starting point is an existing type over which an equivalence relation
+  given by the user is defined. With this input the package introduces a new
+  type, which comes with two associated abstraction and representation
+  functions, written @{text Abs} and @{text Rep}. These functions relate
+  elements in the existing and new type, and can be uniquely identified by
+  their type (which however we often omit for better readability). They
+  represent an isomorphism between the non-empty subset and elements in the
+  new type. They are necessary for making definitions involving the new type. For
+  example @{text "0"} and @{text "1"} of type @{typ int} can be defined as
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   @{text "0 \<equiv> Abs (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs (1, 0)"}
@@ -168,11 +168,10 @@
   add them according to @{text "add\<^bsub>nat\<times>nat\<^esub>"} and then take the
   abstraction of the result.  This is all straightforward and the existing
   quotient packages can deal with such definitions. But what is surprising
-  that none of them can deal with more complicated definitions involving
+  that none of them can deal with slightly more complicated definitions involving
   \emph{compositions} of quotients. Such compositions are needed for example
-  in case of finite sets. There one would like to have a corresponding definition
-  for finite sets for the operator @{term "concat"} defined over lists. This
-  operator flattens lists of lists as follows
+  in case of finite sets.  For example over lists one can define an operator
+  that flattens lists of lists as follows
 
   @{thm [display, indent=10] concat.simps(1) concat.simps(2)[no_vars]}
 
@@ -183,20 +182,25 @@
   @{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]}
 
   \noindent
-  The problem is that we want to quotient lists to obtain finite sets and 
-  @{term concat} is of type @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"}. We expect
-  that @{term "fconcat"} has type @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha> fset"}. But 
-  what should its definition be? It is not possible to just take the representation
-  of the argument and then take the abstraction of the result of flattening 
-  the resulting list. The problem is that a single @{text "Rep"} only gives
-  us lists of finite sets, not lists of lists. It turns out that we need
-  to be able to build aggregate representation and abstraction function, which in
+  The quotient package should provide us with a definition for @{text "\<Union>"} in
+  terms of @{text flat}, @{text Rep} and @{text Abs}. The problem is that it
+  is not enough to just take the representation of the argument and then
+  take the abstraction of the result, because in that case we obtain an operator
+  with type @{text "(\<alpha> list) fset \<Rightarrow> \<alpha> fset"}, not the expected 
+  @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha> fset"}. It turns out that we need
+  to build aggregate representation and abstraction functions, which in
   case of @{term "fconcat"} produce the following definition
 
-  @{text [display, indent=10] "fset_flat S \<equiv> Abs (concat ((map Rep \<circ> Rep) S))"}
+  @{text [display, indent=10] "\<Union> S \<equiv> Abs (concat ((map Rep \<circ> Rep) S))"}
 
   \noindent
-  where @{term map} is the usual mapping function for lists.
+  where @{term map} is the usual mapping function for lists. In this paper we
+  will present a formal definition for our aggregate abstraction and
+  representation functions (this definition was omitted in \cite{Homeier05}). 
+  They generate definitions like the one above for @{text add} and @{text "\<Union>"} 
+  according to the type of the ``raw'' constant and the type
+  of the quotient constant.
+
 
 *}