# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1288363044 -3600
# Node ID 2668486b684a4d590a8fc581ebef5debbc44be2c
# Parent  ea0cdb7c645548aca16ada5b731b254a22fa5a9e
squeezed qpaper to 6 pages

diff -r ea0cdb7c6455 -r 2668486b684a Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Fri Oct 29 14:25:50 2010 +0900
+++ b/Quotient-Paper/Paper.thy	Fri Oct 29 15:37:24 2010 +0100
@@ -114,14 +114,15 @@
   \end{isabelle}
 
   \noindent
-  This constructions yields the new type @{typ int} and definitions for @{text
+  This constructions yields the new type @{typ int}, and definitions for @{text
   "0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of
   natural numbers (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations
   such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined in
   terms of operations on pairs of natural numbers (namely @{text
   "add_pair (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"}, 
+  Similarly one can construct %%the type of 
+  finite sets, written @{term "\<alpha> fset"}, 
   by quotienting the type @{text "\<alpha> list"} according to the equivalence relation
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -137,13 +138,12 @@
   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
-
-
-  \begin{isabelle}\ \ \ \ \ %%%
-  @{text "t ::= x | t t | \<lambda>x.t"}\hfill\numbered{lambda}
-  \end{isabelle}
-
-  \noindent
+  %
+  %\begin{isabelle}\ \ \ \ \ %%%
+  @{text "t ::= x | t t | \<lambda>x.t"}%\hfill\numbered{lambda}
+  %\end{isabelle}
+  %
+  %\noindent
   The problem with this definition arises, for instance, when one attempts to
   prove formally the substitution lemma \cite{Barendregt81} by induction
   over the structure of terms. This can be fiendishly complicated (see
@@ -181,7 +181,7 @@
 %%% I wouldn't change it.
 
   \begin{center}
-  \mbox{}\hspace{20mm}\begin{tikzpicture}
+  \mbox{}\hspace{20mm}\begin{tikzpicture}[scale=0.9]
   %%\draw[step=2mm] (-4,-1) grid (4,1);
   
   \draw[very thick] (0.7,0.3) circle (4.85mm);
@@ -201,20 +201,20 @@
   \draw[<-, very thick] (-1.8, 0.16) -- (-0.1,0.16);
   \draw (-0.95, 0.26) node[above=0.4mm] {@{text Rep}};
   \draw (-0.95, 0.26) node[below=0.4mm] {@{text Abs}};
-
   \end{tikzpicture}
   \end{center}
 
   \noindent
   The starting point is an existing type, to which we refer as the
-  \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
+  \emph{raw type} and over which an equivalence relation is given by the user. 
+  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. } They relate elements in the
-  existing type to elements in the new type and vice versa, and can be uniquely
+  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
 
@@ -262,7 +262,8 @@
   \end{isabelle}
 
   \noindent
-  where @{text "@"} is the usual list append. We expect that the corresponding 
+  where @{text "@"} is %the usual 
+  list append. We expect that the corresponding 
   operator on finite sets, written @{term "fconcat"},
   builds finite unions of finite sets:
 
@@ -290,7 +291,8 @@
   cumbersome and inelegant in light of our work, which can deal with such
   definitions directly. The solution is that we need to build aggregate
   representation and abstraction functions, which in case of @{text "\<Union>"}
-  generate the following definition
+  generate the %%%following 
+  definition
 
   \begin{isabelle}\ \ \ \ \ %%%
   @{text "\<Union> S \<equiv> Abs_fset (flat ((map_list Rep_fset \<circ> Rep_fset) S))"}
@@ -391,7 +393,7 @@
   which define equivalence relations in terms of constituent equivalence
   relations. For example given two equivalence relations @{text "R\<^isub>1"}
   and @{text "R\<^isub>2"}, we can define an equivalence relations over 
-  products as follows
+  products as %% follows
   
   \begin{isabelle}\ \ \ \ \ %%%
   @{text "(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"}
@@ -481,8 +483,7 @@
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{r@ {\hspace{1mm}}l}
   @{text  "Quot"} & @{text "(rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>)"}\\
-                  & @{text "(Abs_fset \<circ> map_list Abs)"}\\ 
-                  & @{text "(map_list Rep \<circ> Rep_fset)"}\\
+                  & @{text "(Abs_fset \<circ> map_list Abs)"} @{text "(map_list Rep \<circ> Rep_fset)"}\\
   \end{tabular}
   \end{isabelle}
 *}
@@ -606,7 +607,7 @@
   \hfill
   \begin{tabular}{@ {\hspace{2mm}}l@ {}}
   \multicolumn{1}{@ {}l}{equal types:}\\ 
-  @{text "ABS (\<sigma>, \<sigma>)"} $\dn$ @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\\
+  @{text "ABS (\<sigma>, \<sigma>)"} $\dn$ @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\hspace{5mm}%\\
   @{text "REP (\<sigma>, \<sigma>)"} $\dn$ @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\smallskip\\
   \multicolumn{1}{@ {}l}{function types:}\\ 
   @{text "ABS (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} $\dn$ @{text "REP (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> ABS (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\\
@@ -689,7 +690,7 @@
   In our implementation we further
   simplify this function by rewriting with the usual laws about @{text
   "map"}s and @{text "id"}, for example @{term "map_list id = id"} and @{text "f \<circ> id =
-  id \<circ> f = f"}. This gives us the simpler abstraction function
+  id \<circ> f = f"}. This gives us %%%the simpler abstraction function
 
   \begin{isabelle}\ \ \ \ \ %%%
   @{text "(map_list Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}
@@ -708,12 +709,12 @@
   distinguish between arguments and results, but can deal with them uniformly.
   Consequently, all definitions in the quotient package 
   are of the general form
-
-  \begin{isabelle}\ \ \ \ \ %%%
-  @{text "c \<equiv> ABS (\<sigma>, \<tau>) t"}
-  \end{isabelle}
-
-  \noindent
+  %
+  %\begin{isabelle}\ \ \ \ \ %%%
+  \mbox{@{text "c \<equiv> ABS (\<sigma>, \<tau>) t"}}
+  %\end{isabelle}
+  %
+  %\noindent
   where @{text \<sigma>} is the type of the definiens @{text "t"} and @{text "\<tau>"} the
   type of the defined quotient constant @{text "c"}. This data can be easily
   generated from the declaration given by the user.
@@ -757,7 +758,8 @@
   two restrictions in form of proof obligations that arise during the
   lifting. The reason is that even if definitions for all raw constants 
   can be given, \emph{not} all theorems can be lifted to the quotient type. Most 
-  notable is the bound variable function, that is the constant @{text bn}, defined 
+  notable is the bound variable function %%, that is the constant @{text bn}, 
+  defined 
   for raw lambda-terms as follows
 
   \begin{isabelle}
@@ -790,7 +792,7 @@
   \begin{center}
   \hfill
   \begin{tabular}{l}
-  \multicolumn{1}{@ {}l}{equal types:}\\ 
+  \multicolumn{1}{@ {}l}{equal types:} 
   @{text "REL (\<sigma>, \<sigma>)"} $\dn$ @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}\smallskip\\
    \multicolumn{1}{@ {}l}{equal type constructors:}\\ 
   @{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} $\dn$ @{text "rel_\<kappa> (REL (\<sigma>s, \<tau>s))"}\smallskip\\
@@ -810,12 +812,12 @@
   lift to a theorem where @{text "c\<^isub>r"} is replaced by the corresponding
   constant @{text "c\<^isub>q :: \<tau>"} defined over a quotient type. In this situation 
   we generate the following proof obligation
-
-  \begin{isabelle}\ \ \ \ \ %%%
-  @{text "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}
-  \end{isabelle}
-
-  \noindent
+  %
+  %\begin{isabelle}\ \ \ \ \ %%%
+  @{text "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}.
+  %\end{isabelle}
+  %
+  %\noindent
   Homeier calls these proof obligations \emph{respectfulness
   theorems}. However, unlike his quotient package, we might have several
   respectfulness theorems for one constant---he has at most one.
@@ -826,13 +828,13 @@
 
   Before lifting a theorem, we require the user to discharge
   respectfulness proof obligations. In case of @{text bn}
-  this obligation is as follows
-
-  \begin{isabelle}\ \ \ \ \ %%%
+  this obligation is %%as follows
+  % 
+  %\begin{isabelle}\ \ \ \ \ %%%
   @{text  "(\<approx>\<^isub>\<alpha> \<doublearr> =) bn bn"}
-  \end{isabelle}
-
-  \noindent
+  %\end{isabelle}
+  %
+  %\noindent
   and the point is that the user cannot discharge it: because it is not true. To see this,
   we can just unfold the definition of @{text "\<doublearr>"} \eqref{relfun} 
   using extensionality to obtain the false statement
@@ -842,8 +844,8 @@
   \end{isabelle}
 
   \noindent
-  In contrast, if we lift a theorem about @{text "append"} to a theorem describing 
-  the union of finite sets, then we need to discharge the proof obligation
+  In contrast, lifting a theorem about @{text "append"} to a theorem describing 
+  the union of finite sets will mean to discharge the proof obligation
 
   \begin{isabelle}\ \ \ \ \ %%%
   @{text "(\<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub>) append append"}
@@ -1007,21 +1009,21 @@
   %
   \begin{center}
   \begin{tabular}{@ {}l@ {}}
-  \multicolumn{1}{@ {}l@ {}}{abstractions:}\smallskip\\
+  \multicolumn{1}{@ {}l@ {}}{abstractions:}\\%%\smallskip\\
   @{text "REG (\<lambda>x\<^sup>\<sigma>. t, \<lambda>x\<^sup>\<tau>. s)"} $\dn$ 
   $\begin{cases}
   @{text "\<lambda>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
   @{text "\<lambda>x\<^sup>\<sigma> \<in> Resp (REL (\<sigma>, \<tau>)). REG (t, s)"}
-  \end{cases}$\smallskip\\
+  \end{cases}$\\%%\smallskip\\
   \multicolumn{1}{@ {}l@ {}}{universal quantifiers:}\\
   @{text "REG (\<forall>x\<^sup>\<sigma>. t, \<forall>x\<^sup>\<tau>. s)"} $\dn$
   $\begin{cases}
   @{text "\<forall>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
   @{text "\<forall>x\<^sup>\<sigma> \<in> Resp (REL (\<sigma>, \<tau>)). REG (t, s)"}
-  \end{cases}$\smallskip\\
-  \multicolumn{1}{@ {}l@ {}}{equality:}\smallskip\\
+  \end{cases}$\\%%\smallskip\\
+  \multicolumn{1}{@ {}l@ {}}{equality:  \hspace{3mm}%%}\smallskip\\
   %% REL of two equal types is the equality so we do not need a separate case
-  @{text "REG (=\<^bsup>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool\<^esup>, =\<^bsup>\<tau>\<Rightarrow>\<tau>\<Rightarrow>bool\<^esup>)"} $\dn$ @{text "REL (\<sigma>, \<tau>)"}\smallskip\\
+  @{text "REG (=\<^bsup>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool\<^esup>, =\<^bsup>\<tau>\<Rightarrow>\<tau>\<Rightarrow>bool\<^esup>)"} $\dn$ @{text "REL (\<sigma>, \<tau>)"}}\smallskip\\
   \multicolumn{1}{@ {}l@ {}}{applications, variables and constants:}\\
   @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2)"} $\dn$ @{text "REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}\\
   @{text "REG (x\<^isub>1, x\<^isub>2)"} $\dn$ @{text "x\<^isub>1"}\\
@@ -1236,13 +1238,13 @@
 %%
 %% give an example for this
 %%
-  \medskip
+  \smallskip
 
   \noindent
   {\bf Acknowledgements:} We would like to thank Peter Homeier for the many
-  discussions about his HOL4 quotient package and explaining to us
-  some of its finer points in the implementation. Without his patient
-  help, this work would have been impossible.
+  discussions about his HOL4 quotient package.\\[-5mm]% and explaining to us
+  %some of its finer points in the implementation. Without his patient
+  %help, this work would have been impossible.
 
 %  \appendix
 
diff -r ea0cdb7c6455 -r 2668486b684a Quotient-Paper/document/root.bib
--- a/Quotient-Paper/document/root.bib	Fri Oct 29 14:25:50 2010 +0900
+++ b/Quotient-Paper/document/root.bib	Fri Oct 29 15:37:24 2010 +0100
@@ -1,13 +1,13 @@
 @inproceedings{Nogin02,
   author    = {Aleksey Nogin},
   title     = {Quotient Types: A Modular Approach},
-  booktitle = {TPHOLs},
+  booktitle = {Proc.~of the 15th TPHOLs conference},
   year      = {2002},
   pages     = {263-280},
-  ee        = {http://link.springer.de/link/service/series/0558/bibs/2410/24100263.htm},
-  crossref  = {DBLP:conf/tphol/2002},
-  bibsource = {DBLP, http://dblp.uni-trier.de}
+  series    = {LNCS},
+  volume    = {2646}
 }
+
 @proceedings{DBLP:conf/tphol/2002,
   editor    = {Victor Carre{\~n}o and
                C{\'e}sar Mu{\~n}oz and
@@ -38,12 +38,11 @@
                Loic Pottier and
                Carlos Simpson},
   title     = {{M}athematical {Q}uotients and {Q}uotient {T}ypes in {C}oq},
-  booktitle = {TYPES},
+  booktitle = {Proc of the TYPES workshop},
   year      = {2002},
   pages     = {95-107},
-  ee        = {http://link.springer.de/link/service/series/0558/bibs/2646/26460095.htm},
-  crossref  = {DBLP:conf/types/2002},
-  bibsource = {DBLP, http://dblp.uni-trier.de}
+  series    = {LNCS},
+  volume    = {2646}
 }
 
 @proceedings{DBLP:conf/types/2002,
@@ -77,13 +76,13 @@
   author    = {Oscar Slotosch},
   title     = {Higher Order Quotients and their Implementation in Isabelle
                HOL},
-  booktitle = {TPHOLs},
+  booktitle = {Proc.~of the 10th TPHOLs conference},
   year      = {1997},
   pages     = {291-306},
-  ee        = {http://dx.doi.org/10.1007/BFb0028401},
-  crossref  = {DBLP:conf/tphol/1997},
-  bibsource = {DBLP, http://dblp.uni-trier.de}
+  series    = {LNCS},
+  volume    = {1275}
 }
+
 @proceedings{DBLP:conf/tphol/1997,
   editor    = {Elsa L. Gunter and
                Amy P. Felty},
@@ -102,13 +101,13 @@
 @inproceedings{Homeier05,
   author    = {Peter V. Homeier},
   title     = {A Design Structure for Higher Order Quotients},
-  booktitle = {TPHOLs},
+  booktitle = {Proc of the 18th TPHOLs conference},
   year      = {2005},
   pages     = {130-146},
-  ee        = {http://dx.doi.org/10.1007/11541868_9},
-  crossref  = {DBLP:conf/tphol/2005},
-  bibsource = {DBLP, http://dblp.uni-trier.de}
+  series    = {LNCS},
+  volume    = {3603}
 }
+
 @proceedings{DBLP:conf/tphol/2005,
   editor    = {Joe Hurd and
                Thomas F. Melham},
diff -r ea0cdb7c6455 -r 2668486b684a Quotient-Paper/document/root.tex
--- a/Quotient-Paper/document/root.tex	Fri Oct 29 14:25:50 2010 +0900
+++ b/Quotient-Paper/document/root.tex	Fri Oct 29 15:37:24 2010 +0100
@@ -64,7 +64,8 @@
 mechanism for extension is the introduction of safe definitions and of
 non-empty types. Both extensions are often performed in quotient
 constructions. To ease the work involved with such quotient constructions, we
-re-implemented in the popular Isabelle/HOL theorem prover the quotient 
+re-implemented in the %popular 
+Isabelle/HOL theorem prover the quotient 
 package by Homeier. In doing so we extended his work in order to deal with 
 compositions of quotients and also specified completely the procedure 
 of lifting theorems from the raw level to the quotient level.
@@ -81,6 +82,8 @@
 \input{session}
 
 % optional bibliography
+\small
+
 \bibliographystyle{abbrv}
 \bibliography{root}