
diff -r e4699a240d2c -r 4ae32dd02d14 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Tue Jun 15 08:56:13 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Tue Jun 15 09:44:16 2010 +0200
@@ -357,6 +357,10 @@
       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}
 
+  \begin{definition}[Respects]
+  An element @{text "x"} respects a relation @{text "R"} if and only if @{text "R x x"}.
+  \end{definition}
+
   \noindent
   As a result, Homeier was able to build an automatic prover that can nearly
   always discharge a proof obligation involving @{text "Quotient"}. Our quotient
@@ -372,10 +376,12 @@
   \end{definition}
 
   \noindent
-  Unfortunately, restrictions in HOL's type-system prevent us from stating
-  and proving a quotient type theorem, like Proposition \ref{funquot}, for compositions 
-  of relations. However, we can prove all instances where @{text R\<^isub>1} and 
-  @{text "R\<^isub>2"} are built up by constituent equivalence relations.
+  Unfortunately a quotient type theorem, like Proposition \ref{funquot}, for
+  the composition of any two quotients in not true (it is not even typable in
+  the HOL type system). However, we can prove useful instances for compatible
+  containers. We will show such example in Section \ref{sec:resp}.
+
+
 *}
 
 section {* Quotient Types and Quotient Definitions\label{sec:type} *}
@@ -739,9 +745,12 @@
 
   Lets take again the example of @{term flat}. To be able to lift
   theorems that talk about it we provide the composition quotient
-  theorem:
+  theorem which allows quotienting inside the container:
 
-  @{thm [display, indent=10] quotient_compose_list[no_vars]}
+  If @{term R} is an equivalence relation and @{term "Quotient R Abs Rep"}
+  then
+
+  @{text [display, indent=10] "Quotient (list_rel R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> map Abs) (map Rep o rep_fset)"}
 
   \noindent
   this theorem will then instantiate the quotients needed in the
@@ -792,10 +801,10 @@
   \begin{tabular}{rcl}
   \multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions (with same types and different types):}\\
   @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma>. REG (t, s)"}\\
-  @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}\\
+  @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}\\
   \multicolumn{3}{@ {\hspace{-4mm}}l}{quantification (over same types and different types):}\\
   @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma>. REG (t, s)"}\\
-  @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}\\
+  @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}\\
   \multicolumn{3}{@ {\hspace{-4mm}}l}{equalities (with same types and different types):}\\
   @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>)"} & $\dn$ & @{text "(op =) : \<sigma>"}\\
   @{text "REG ((op =) : \<sigma>, (op =) : \<tau>)"} & $\dn$ & @{text "REL (\<sigma>, \<tau>) : \<sigma>"}\\
@@ -1036,27 +1045,8 @@
 
 text {*
 
-  Oscar Slotosch~\cite{Slotosch97} implemented a mechanism that automatically
-  defines quotient types for Isabelle/HOL. It did not include theorem lifting.
-  John Harrison's quotient package~\cite{harrison-thesis} is the first one to
-  lift theorems, however only first order. There is work on quotient types in
-  non-HOL based systems and logical frameworks, namely theory interpretations
-  in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, or
-  the use of setoids in Coq, with some higher order issues~\cite{ChicliPS02}.
-  Larry Paulson shows a construction of quotients that does not require the
-  Hilbert Choice operator, again only first order~\cite{Paulson06}.
-
-  The closest to our package is the package for HOL4 by Peter Homeier~\cite{Homeier05},
-  which is the first one to support lifting of higher order theorems. In
-  comparison with this package we explore the notion of composition of quotients,
-  which allows lifting constants like @{term "concat"} and theorems about it.
-  The HOL4 package requires a big lists of constants, theorems to lift,
-  respectfullness conditions as input. Our package is modularized, so that
-  single definitions, single theorems or single respectfullness conditions etc
-  can be added, which allows a natural use of the quotient package together
-  with type-classes and locales.
-
-  The code of the quotient package described here is already included in the
+  The code of the quotient package and the examples described here are
+  already included in the
   standard distribution of Isabelle.\footnote{Available from
   \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} It is
   heavily used in Nominal Isabelle, which provides a convenient reasoning
@@ -1067,38 +1057,42 @@
   concurrency \cite{BengtsonParow09} and a strong normalisation result for
   cut-elimination in classical logic \cite{UrbanZhu08}.
 
-*}
+  Oscar Slotosch~\cite{Slotosch97} implemented a mechanism that automatically
+  defines quotient types for Isabelle/HOL. It did not include theorem lifting.
+  John Harrison's quotient package~\cite{harrison-thesis} is the first one to
+  lift theorems, however only first order. There is work on quotient types in
+  non-HOL based systems and logical frameworks, namely theory interpretations
+  in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, or
+  the use of setoids in Coq, with some higher order issues~\cite{ChicliPS02}.
+  Larry Paulson shows a construction of quotients that does not require the
+  Hilbert Choice operator, again only first order~\cite{Paulson06}.
+  The closest to our package is the package for HOL4 by Peter Homeier~\cite{Homeier05},
+  which is the first one to support lifting of higher order theorems.
 
 
-subsection {* Contributions *}
-
-text {*
-  We present the detailed lifting procedure, which was not shown before.
-
-  The quotient package presented in this paper has the following
-  advantages over existing packages:
-  \begin{itemize}
-
-  \item We define quotient composition, function map composition and
-    relation map composition. This lets lifting polymorphic types with
-    subtypes quotiented as well. We extend the notions of
-    respectfulness and preservation to cope with quotient
-    composition.
+  Our quotient package for the first time explore the notion of
+  composition of quotients, which allows lifting constants like @{term
+  "concat"} and theorems about it. We defined the composition of
+  relations and showed examples of compositions of quotients which
+  allows lifting polymorphic types with subtypes quotiented as well.
+  We extended the notions of respectfullness and preservation;
+  with quotient compositions there is more than one condition needed
+  for a constant.
 
-  \item We allow lifting only some occurrences of quotiented
-    types. Rsp/Prs extended. (used in nominal)
+  Our package is modularized, so that single definitions, single
+  theorems or single respectfullness conditions etc can be added,
+  which allows the use of the quotient package together with
+  type-classes and locales. This has the advantage over packages
+  requiring big lists as input for the user of being able to develop
+  a theory progressively.
 
-  \item The quotient package is very modular. Definitions can be added
-    separately, rsp and prs can be proved separately, Quotients and maps
-    can be defined separately and theorems can
-    be lifted on a need basis. (useful with type-classes).
-
-  \item Can be used both manually (attribute, separate tactics,
-    rsp/prs databases) and programatically (automated definition of
-    lifted constants, the rsp proof obligations and theorem statement
-    translation according to given quotients).
-
-  \end{itemize}
+  We allow lifting only some occurrences of quotiented types, which
+  is useful in Nominal. The package can be used automatically with
+  an attribute, manually with separate tactics for parts of the lifting
+  procedure, and programatically. Automated definitions of constants
+  and respectfulness proof obligations are used in Nominal. Finally
+  we streamlined and showed the detailed lifting procedure, which
+  has not been presented before.
 
   \medskip
   \noindent




