
diff -r 99cf23602d36 -r 69b80ad616c5 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Wed Jun 16 02:55:52 2010 +0100
+++ b/Quotient-Paper/Paper.thy	Wed Jun 16 03:44:10 2010 +0100
@@ -641,7 +641,7 @@
   The main point of the quotient package is to automatically ``lift'' theorems
   involving constants over the raw type to theorems involving constants over
   the quotient type. Before we can describe this lifting process, we need to impose 
-  some restrictions in the form of proof obligations that arise during the
+  two restrictions in the 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 
   notably is the bound variable function, that is the constant @{text bn}, defined 
@@ -691,14 +691,16 @@
 
   @{text [display, indent=10] "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}
 
-  \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"}
+  %%% PROBLEM I do not yet completely understand the 
+  %%% form of respectfullness 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"}
 
   \noindent
-  where @{text "\<alpha>s"} are the type variables in @{text \<sigma>} and @{text \<tau>}.
+  %%%where @ {text "\<alpha>s"} are the type variables in @{text \<sigma>} and @{text \<tau>}.
   Homeier calls these proof obligations \emph{respectfullness
   theorems}. Before lifting a theorem, we require the user to discharge
   them. And the point with @{text bn} is that the respectfullness theorem
@@ -717,111 +719,80 @@
   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
 
-  @{text [display, indent=10] "(rel_list R \<doublearr> rel_list R \<doublearr> rel_listR) append append"}
+  @{text [display, indent=10] "(\<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub>) append append"}
+
+  \noindent
+  To do so, we have to establish
+  
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  if @{thm (prem1) append_rsp_unfolded[of xs ys us vs, no_vars]} and
+  @{thm (prem2) append_rsp_unfolded[of xs ys us vs, no_vars]}
+  then @{thm (concl) append_rsp_unfolded[of xs ys us vs, no_vars]} 
+  \end{isabelle}
+
+  \noindent
+  which is straightforward given the definition shown in \eqref{listequiv}.
+
+  The second restriction we have to impose arises from
+  non-lifted polymorphic constants, which are instantiated to a
+  type being quotient. For example, take the @{term "cons"} to 
+  add a pair of natural numbers to a list. The pair of natural numbers 
+  is to become an integer. But we still want to use @{text cons} for
+  adding integers to lists---just with a different type. 
+  To be able to lift such theorems, we need a \emph{preservation theorem} 
+  for @{text cons}. Assuming we have a poplymorphic raw constant 
+  @{text "c\<^isub>r :: \<sigma>"} and a corresponding quotient constant @{text "c\<^isub>q :: \<tau>"}, 
+  then a preservation theorem is as follows
+
+  @{text [display, indent=10] "Quotient R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub> implies  ABS (\<sigma>, \<tau>) c\<^isub>r = c\<^isub>r"}
+
+  \noindent
+  where the @{text "\<alpha>s"} stand for the type variables in the type of @{text "c\<^isub>r"}.
+  In case of @{text cons} we have 
+
+  @{text [display, indent=10] "(Rep ---> map Rep ---> map Abs) cons = cons"}
 
   \noindent
   under the assumption @{text "Quotient R Abs Rep"}.
 
 
-  class returned by this constant depends only on the equivalence
-  classes of the arguments applied to the constant. To automatically
-  lift a theorem that talks about a raw constant, to a theorem about
-  the quotient type a respectfulness theorem is required.
-
-  A respectfulness condition for a constant can be expressed in
-  terms of an aggregate relation between the constant and itself,
-  for example the respectfullness for @{text "append"}
-  can be stated as:
-
-  @{text [display, indent=10] "(\<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub>) append append"}
-
-  \noindent
-  Which after unfolding the definition of @{term "op ===>"} is equivalent to:
-
-  @{thm [display, indent=10] append_rsp_unfolded[no_vars]}
-
-  \noindent An aggregate relation is defined in terms of relation
-  composition, so we define it first:
-
-  
-
-  The aggregate relation for an aggregate raw type and quotient type
-  is defined as:
-
-
-  Again, the last case is novel, so lets look at the example of
-  respectfullness for @{term concat}. The statement according to
-  the definition above is:
-
-  @{thm [display, indent=10] concat_rsp[no_vars]}
-
-  \noindent
-  By unfolding the definition of relation composition and relation map
-  we can see the equivalent statement just using the primitive list
-  equivalence relation:
-
-  @{thm [display, indent=10] concat_rsp_unfolded[of "a" "a'" "b'" "b", no_vars]}
-
-  The statement reads that, for any lists of lists @{term a} and @{term b}
-  if there exist intermediate lists of lists @{term "a'"} and @{term "b'"}
-  such that each element of @{term a} is in the relation with an appropriate
-  element of @{term a'}, @{term a'} is in relation with @{term b'} and each
-  element of @{term b'} is in relation with the appropriate element of
-  @{term b}.
-
+  %%% PROBLEM I do not understand this
+  %%%This is not enough to lift theorems that talk about quotient compositions.
+  %%%For some constants (for example empty list) it is possible to show a
+  %%%general compositional theorem, but for @ {term "op #"} it is necessary
+  %%%to show that it respects the particular quotient type:
+  %%%
+  %%%@ {thm [display, indent=10] insert_preserve2[no_vars]}
 
-  Sometimes a non-lifted polymorphic constant is instantiated to a
-  type being lifted. For example take the @{term "op #"} which inserts
-  an element in a list of pairs of natural numbers. When the theorem
-  is lifted, the pairs of natural numbers are to become integers, but
-  the head constant is still supposed to be the head constant, just
-  with a different type.  To be able to lift such theorems
-  automatically, additional theorems provided by the user are
-  necessary, we call these \emph{preservation} theorems following
-  Homeier's naming.
-
-  To lift theorems that talk about insertion in lists of lifted types
-  we need to know that for any quotient type with the abstraction and
-  representation functions @{text "Abs"} and @{text Rep} we have:
-
-  @{thm [display, indent=10] (concl) cons_prs[no_vars]}
-
-  This is not enough to lift theorems that talk about quotient compositions.
-  For some constants (for example empty list) it is possible to show a
-  general compositional theorem, but for @{term "op #"} it is necessary
-  to show that it respects the particular quotient type:
-
-  @{thm [display, indent=10] insert_preserve2[no_vars]}
-
-  {\it Composition of Quotient theorems}
-
-  Given two quotients, one of which quotients a container, and the
-  other quotients the type in the container, we can write the
-  composition of those quotients. To compose two quotient theorems
-  we compose the relations with relation composition as defined above
-  and the abstraction and relation functions are the ones of the sub
-  quotients composed with the usual function composition.
-  The @{term "Rep"} and @{term "Abs"} functions that we obtain agree
-  with the definition of aggregate Abs/Rep functions and the
-  relation is the same as the one given by aggregate relations.
-  This becomes especially interesting
-  when we compose the quotient with itself, as there is no simple
-  intermediate step.
-
-  Lets take again the example of @{term flat}. To be able to lift
-  theorems that talk about it we provide the composition quotient
-  theorem which allows quotienting inside the container:
-
-  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
-  injection and cleaning proofs allowing the lifting procedure to
-  proceed in an unchanged way.
-
+  %%% PROBLEM I also do not follow this
+  %%%{\it Composition of Quotient theorems}
+  %%%
+  %%%Given two quotients, one of which quotients a container, and the
+  %%%other quotients the type in the container, we can write the
+  %%%composition of those quotients. To compose two quotient theorems
+  %%%we compose the relations with relation composition as defined above
+  %%%and the abstraction and relation functions are the ones of the sub
+  %%%quotients composed with the usual function composition.
+  %%%The @ {term "Rep"} and @ {term "Abs"} functions that we obtain agree
+  %%%with the definition of aggregate Abs/Rep functions and the
+  %%%relation is the same as the one given by aggregate relations.
+  %%%This becomes especially interesting
+  %%%when we compose the quotient with itself, as there is no simple
+  %%%intermediate step.
+  %%%
+  %%%Lets take again the example of @ {term flat}. To be able to lift
+  %%%theorems that talk about it we provide the composition quotient
+  %%%theorem which allows quotienting inside the container:
+  %%%
+  %%%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
+  %%%injection and cleaning proofs allowing the lifting procedure to
+  %%%proceed in an unchanged way.
 *}
 
 section {* Lifting of Theorems\label{sec:lift} *}




