# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1276691183 -7200
# Node ID 816204c76e90fb5261b6eb647ca78e107cdbb1c6
# Parent  0d561216f1f99608dece5ed9b92e1c99d0758339
Answer questions in comments

diff -r 0d561216f1f9 -r 816204c76e90 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Wed Jun 16 03:47:38 2010 +0100
+++ b/Quotient-Paper/Paper.thy	Wed Jun 16 14:26:23 2010 +0200
@@ -257,7 +257,7 @@
   The paper is organised as follows: Section \ref{sec:prelims} presents briefly
   some necessary preliminaries; Section \ref{sec:type} describes the definitions 
   of quotient types and shows how definitions of constants can be made over 
-  quotient types. Section \ref{sec:resp} introduces the notions of respectfullness
+  quotient types. Section \ref{sec:resp} introduces the notions of respectfulness
   and preservation; Section \ref{sec:lift} describes the lifting of theorems;
   Section \ref{sec:examples} presents some examples
   and Section \ref{sec:conc} concludes and compares our results to existing 
@@ -658,7 +658,7 @@
   But this constant does \emph{not} respect @{text "\<alpha>"}-equivalence and 
   consequently no theorem involving this constant can be lifted to @{text
   "\<alpha>"}-equated lambda terms. Homeier formulates the restrictions in terms of
-  the properties of \emph{respectfullness} and \emph{preservation}. We have
+  the properties of \emph{respectfulness} and \emph{preservation}. We have
   to slightly extend Homeier's definitions in order to deal with quotient
   compositions. 
 
@@ -692,18 +692,21 @@
   @{text [display, indent=10] "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}
 
   %%% PROBLEM I do not yet completely understand the 
-  %%% form of respectfullness theorems
+  %%% form of respectfulness theorems
   %%%\noindent
   %%%if @ {text \<sigma>} and @ {text \<tau>} have no type variables. In case they have, then
   %%%the proof obligation is of the form
   %%% 
   %%%@ {text [display, indent=10] "Quotient R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub>  implies  REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}
 
+  %%% ANSWER: The respectfulness theorems never have any quotient assumptions,
+  %%% So the commited version is ok.
+
   \noindent
   %%%where @ {text "\<alpha>s"} are the type variables in @{text \<sigma>} and @{text \<tau>}.
-  Homeier calls these proof obligations \emph{respectfullness
+  Homeier calls these proof obligations \emph{respectfulness
   theorems}. Before lifting a theorem, we require the user to discharge
-  them. And the point with @{text bn} is that the respectfullness theorem
+  them. And the point with @{text bn} is that the respectfulness theorem
   looks as follows
 
   @{text [display, indent=10] "(\<approx>\<^isub>\<alpha> \<doublearr> =) bn bn"}
@@ -755,6 +758,14 @@
   \noindent
   under the assumption @{text "Quotient R Abs Rep"}.
 
+  %%% ANSWER
+  %%% There are 3 things needed to lift things that involve composition of quotients
+  %%% - The compositional quotient theorem
+  %%% - Compositional respectfullness theorems
+  %%% - and compositional preservation theorems.
+  %%% And the case of preservation for nil is special, because we prove some property
+  %%% of all elements in an empty list, so any property is true so we can write it
+  %%% more general, but a version restricted to the particular quotient is true as well
 
   %%% PROBLEM I do not understand this
   %%%This is not enough to lift theorems that talk about quotient compositions.
@@ -951,7 +962,7 @@
   two terms, and is defined for a goal being a relation between these two terms.
 
   \begin{itemize}
-  \item For two constants, an appropriate constant respectfullness assumption is used.
+  \item For two constants, an appropriate constant respectfulness assumption is used.
   \item For two variables, we use the assumptions proved in regularization.
   \item For two abstractions, they are eta-expanded and beta-reduced.
   \item For two applications, if the right side is an application of
@@ -1113,12 +1124,12 @@
   "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;
+  We extended the notions of respectfulness and preservation;
   with quotient compositions there is more than one condition needed
   for a constant.
 
   Our package is modularized, so that single definitions, single
-  theorems or single respectfullness conditions etc can be added,
+  theorems or single respectfulness 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
@@ -1135,8 +1146,8 @@
   \medskip
   \noindent
   {\bf Acknowledgements:} We would like to thank Peter Homeier for the
-  discussions about his HOL4 quotient package and explaining to us 
-  some its finer points in the implementation.
+  discussions about his HOL4 quotient package and explaining to us
+  some of its finer points in the implementation.
 
 *}