
diff -r c0c5bc4ee8cb -r bf3a29ea74f6 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Tue Jun 15 11:59:16 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Tue Jun 15 12:00:03 2010 +0200
@@ -7,7 +7,7 @@
 
 notation (latex output)
   rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and
-  pred_comp ("_ \<circ>\<circ> _") and
+  pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and
   "op -->" (infix "\<longrightarrow>" 100) and
   "==>" (infix "\<Longrightarrow>" 100) and
   fun_map ("_ \<^raw:\mbox{\singlearr}> _" 51) and
@@ -88,7 +88,7 @@
   then be defined as the empty list and the union of two finite sets, written
   @{text "\<union>"}, as list append.
 
-  Quotients are important in a variety of areas, but they are ubiquitous in
+  Quotients are important in a variety of areas, but they are really ubiquitous in
   the area of reasoning about programming language calculi. A simple example
   is the lambda-calculus, whose raw terms are defined as
 
@@ -152,14 +152,14 @@
 
   \noindent
   The starting point is an existing type, to which we refer as the
-  \emph{raw type}, over which an equivalence relation given by the user is
+  \emph{raw type} and 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 type}. This type comes with an
   \emph{abstraction} and a \emph{representation} function, written @{text Abs}
   and @{text Rep}.\footnote{Actually slightly more basic functions are given;
   the functions @{text Abs} and @{text Rep} need to be derived from them. We
-  will show the details later. } These functions relate elements in the
-  existing type to elements in the new type and vice versa; they can be uniquely
+  will show the details later. } They relate elements in the
+  existing type to elements in the new type and vice versa, and can be uniquely
   identified by their quotient type. For example for the integer quotient construction
   the types of @{text Abs} and @{text Rep} are
 
@@ -263,11 +263,11 @@
 section {* Preliminaries and General Quotients\label{sec:prelims} *}
 
 text {*
-  We describe here briefly the most basic notions of HOL we rely on, and 
+  We describe in this section briefly the most basic notions of HOL we rely on, and 
   the important definitions given by Homeier for quotients \cite{Homeier05}.
 
   At its core HOL is based on a simply-typed term language, where types are 
-  recorded in Church-style fashion (that means, we can infer the type of 
+  recorded in Church-style fashion (that means, we can always infer the type of 
   a term and its subterms without any additional information). The grammars
   for types and terms are as follows
 
@@ -283,21 +283,22 @@
   We often write just @{text \<kappa>} for @{text "() \<kappa>"}, and use @{text "\<alpha>s"} and
   @{text "\<sigma>s"} to stand for collections of type variables and types,
   respectively.  The type of a term is often made explicit by writing @{text
-  "t :: \<sigma>"}. HOL contains a type @{typ bool} for booleans and the function 
+  "t :: \<sigma>"}. HOL includes a type @{typ bool} for booleans and the function 
   type, written @{text "\<sigma> \<Rightarrow> \<tau>"}. HOL also contains
-  many primitive and defined constants; for example equality @{text "= :: \<sigma> \<Rightarrow>
-  \<sigma> \<Rightarrow> bool"} and the identity function @{text "id :: \<sigma> => \<sigma>"} (the former
+  many primitive and defined constants; this includes equality, with type @{text "= :: \<sigma> \<Rightarrow>
+  \<sigma> \<Rightarrow> bool"}, and the identity function, with type @{text "id :: \<sigma> => \<sigma>"} (the former
   being primitive and the latter being defined as @{text
   "\<lambda>x\<^sup>\<sigma>. x\<^sup>\<sigma>"}).
 
   An important point to note is that theorems in HOL can be seen as a subset
   of terms that are constructed specially (namely through axioms and prove
-  rules). As a result we are able later on to define automatic proof
+  rules). As a result we are able to define automatic proof
   procedures showing that one theorem implies another by decomposing the term
   underlying the first theorem.
 
   Like Homeier, our work relies on map-functions defined for every type constructor,
-  like @{text map} for lists. Homeier describes others for products, sums,
+  like @{text map} for lists. Homeier describes in \cite{Homeier05} map-functions
+  for products, sums,
   options and also the following map for function types
 
   @{thm [display, indent=10] fun_map_def[no_vars, THEN eq_reflection]}
@@ -309,8 +310,10 @@
   @{text [display, indent=10] "add \<equiv> (Rep_int \<singlearr> Rep_int \<singlearr> Abs_int) add_pair"}
 
   \noindent
-  We will sometimes refer to a map-function defined for a type-constructor @{text \<kappa>}
-  as @{text "map_\<kappa>"}. 
+  Using extensionality and unfolding the definition, we can get back to \eqref{adddef}. 
+  In what follows we shall use the terminology @{text "map_\<kappa>"} for a map-function 
+  defined for the type-constructor @{text \<kappa>}. In our implementation we have 
+  a database of map-functions that can be dynamically extended.
 
   It will also be necessary to have operators, referred to as @{text "rel_\<kappa>"},
   which define equivalence relations in terms of constituent equivalence
@@ -321,8 +324,8 @@
   @{text [display, indent=10] "(R\<^isub>1 \<tripple> R\<^isub>2) (x\<^isub>1, x\<^isub>2) (y\<^isub>1, y\<^isub>2) \<equiv> R\<^isub>1 x\<^isub>1 y\<^isub>1 \<and> R\<^isub>2 x\<^isub>2 y\<^isub>2"}
 
   \noindent
-  Similarly, Homeier defines the following operator for defining equivalence 
-  relations over function types:
+  Homeier gives also the following operator for defining equivalence 
+  relations over function types
   %
   @{thm [display, indent=10] fun_rel_def[of "R\<^isub>1" "R\<^isub>2", no_vars, THEN eq_reflection]}
 
@@ -341,12 +344,13 @@
   \end{definition}
 
   \noindent
-  The value of this definition is that validity of @{text Quotient} can be 
-  proved in terms of the validity of @{text "Quotient"} over the constituent types. 
+  The value of this definition is that validity of @{text "Quotient R Abs Rep"} can 
+  often be proved in terms of the validity of @{text "Quotient"} over the constituent 
+  types of @{text "R"}, @{text Abs} and @{text Rep}. 
   For example Homeier proves the following property for higher-order quotient
   types:
  
-  \begin{proposition}[Function Quotient]\label{funquot}
+  \begin{proposition}\label{funquot}
   @{thm[mode=IfThen] fun_quotient[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2" 
       and ?abs1.0="Abs\<^isub>1" and ?abs2.0="Abs\<^isub>2" and ?rep1.0="Rep\<^isub>1" and ?rep2.0="Rep\<^isub>2"]}
   \end{proposition}
@@ -356,7 +360,10 @@
   \end{definition}
 
   \noindent
-  We will heavily rely on this part of Homeier's work including an extension 
+  As a result, Homeier was able to build an automatic prover that can nearly
+  always discharge a proof obligation involving @{text "Quotient"}. Our quotient
+  package makes heavy 
+  use of this part of Homeier's work including an extension 
   to deal with compositions of equivalence relations defined as follows
 
   \begin{definition}[Composition of Relations]
@@ -381,11 +388,11 @@
   The first step in a quotient construction is to take a name for the new
   type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation, say @{text R},
   defined over a raw type, say @{text "\<sigma>"}. The type of the equivalence
-  relation must be of type @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}. The user-visible part of
-  the declaration is therefore
+  relation must be @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}. The user-visible part of
+  the quotient type declaration is therefore
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \isacommand{quotient\_type}~~@{text "\<alpha>s \<kappa>\<^isub>q = \<sigma> / R"}
+  \isacommand{quotient\_type}~~@{text "\<alpha>s \<kappa>\<^isub>q = \<sigma> / R"}\hfill\numbered{typedecl}
   \end{isabelle}
 
   \noindent
@@ -403,9 +410,9 @@
   \noindent
   which introduce the type of integers and of finite sets using the
   equivalence relations @{text "\<approx>\<^bsub>nat \<times> nat\<^esub>"} and @{text
-  "\<approx>\<^bsub>list\<^esub>"} defined earlier in \eqref{natpairequiv} and
+  "\<approx>\<^bsub>list\<^esub>"} defined in \eqref{natpairequiv} and
   \eqref{listequiv}, respectively (the proofs about being equivalence
-  relations is omitted).  Given this data, we declare internally 
+  relations is omitted).  Given this data, we declare for \eqref{typedecl} internally 
   the quotient types as
   
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -417,14 +424,14 @@
   @{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 the following
-  abstraction and representation functions having the type
+  abstraction and representation functions 
 
   \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 
-  They relate the new quotient type and equivalence classes of the raw
+  As can be seen from the type, they relate 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
 
@@ -451,7 +458,7 @@
   The next step in a quotient construction is to introduce definitions of new constants
   involving the quotient type. These definitions need to be given in terms of concepts
   of the raw type (remember this is the only way how to extend HOL
-  with new definitions). For the user visible is the declaration
+  with new definitions). For the user the visible part of such definitions is the declaration
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \isacommand{quotient\_definition}~~@{text "c :: \<tau>"}~~\isacommand{is}~~@{text "t :: \<sigma>"}
@@ -461,7 +468,7 @@
   where @{text t} is the definiens (its type @{text \<sigma>} can always be inferred)
   and @{text "c"} is the name of definiendum, whose type @{text "\<tau>"} needs to be
   given explicitly (the point is that @{text "\<tau>"} and @{text "\<sigma>"} can only differ 
-  in places where a quotient and raw type are involved). Two concrete examples are
+  in places where a quotient and raw type is involved). Two concrete examples are
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -484,8 +491,11 @@
   these two functions is to recursively descend into the raw types @{text \<sigma>} and 
   quotient types @{text \<tau>}, and generate the appropriate
   @{text "Abs"} and @{text "Rep"} in places where the types differ. Therefore
-  we generate just the identity whenever the types are equal. All clauses
-  are as follows:
+  we generate just the identity whenever the types are equal. On the ``way'' down,
+  however we might have to use map-functions to let @{text Abs} and @{text Rep} act
+  over the appropriate types. The clauses of @{text ABS} and @{text REP} 
+  are as follows (where we use the short-hand notation @{text "ABS (\<sigma>s, \<tau>s)"} to mean 
+  @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1)\<dots>ABS (\<sigma>\<^isub>i, \<tau>\<^isub>i)"}; similarly for @{text REP}):
 
   \begin{center}
   \hfill
@@ -506,7 +516,7 @@
   \end{center}
   %
   \noindent
-  where in the last two clauses we have that the quotient type @{text "\<alpha>s
+  where in the last two clauses we have that the type @{text "\<alpha>s
   \<kappa>\<^isub>q"} is the quotient of the raw type @{text "\<rho>s \<kappa>"} (for example
   @{text "int"} and @{text "nat \<times> nat"}, or @{text "\<alpha> fset"} and @{text "\<alpha>
   list"}). The quotient construction ensures that the type variables in @{text
@@ -538,7 +548,8 @@
   @{text [display, indent=10] "\<lambda>a b. map_prod (map a) b"}
   
   \noindent
-  which we need to define the aggregate abstraction and representation functions.
+  which we need in order to define the aggregate abstraction and representation 
+  functions.
   
   To see how these definitions pan out in practise, let us return to our
   example about @{term "concat"} and @{term "fconcat"}, where we have the raw type
@@ -585,7 +596,7 @@
   \end{lemma}
 
   \begin{proof}
-  By induction and analysing the definitions of @{text "ABS"}, @{text "REP"}
+  By mutual induction and analysing the definitions of @{text "ABS"}, @{text "REP"}
   and @{text "MAP"}. The cases of equal types and function types are
   straightforward (the latter follows from @{text "\<singlearr>"} having the
   type @{text "(\<alpha> \<Rightarrow> \<beta>) \<Rightarrow> (\<gamma> \<Rightarrow> \<delta>) \<Rightarrow> (\<beta> \<Rightarrow> \<gamma>) \<Rightarrow> (\<alpha> \<Rightarrow> \<delta>)"}). In case of equal type




