# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1279364464 -3600
# Node ID 46be4145b922304c22459df3eb902cb159cbd227
# Parent  467123396e5a131ee3e658e37be93d652339bb57
changes suggested by Peter Homeier

diff -r 467123396e5a -r 46be4145b922 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Sat Jul 17 10:25:29 2010 +0100
+++ b/Quotient-Paper/Paper.thy	Sat Jul 17 12:01:04 2010 +0100
@@ -398,13 +398,14 @@
   @{abbrev "rel_conj R\<^isub>1 R\<^isub>2"} where @{text "\<circ>\<circ>"} is the predicate
   composition defined by 
   @{thm (concl) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}
-  holds if and only if @{thm (prem 1) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} and
+  holds if and only if there exists a @{text y} such that @{thm (prem 1) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} and
   @{thm (prem 2) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}.
   \end{definition}
 
   \noindent
   Unfortunately, there are two predicaments with compositions of relations.
-  First, a general quotient theorem, like the one given in Proposition \ref{funquot},
+  First, a general quotient theorem for @{text "\<circ>\<circ>\<circ>"}, like the one for @{text "\<singlearr>"} 
+  given in Proposition \ref{funquot},
   cannot be stated inside HOL, because of restrictions on types.
   Second, even if we were able to state such a quotient theorem, it
   would not be true in general. However, we can prove specific instances of a
@@ -569,7 +570,7 @@
   \end{center}
   %
   \noindent
-  In this definition we rely on the fact that we can interpret type-variables @{text \<alpha>} as 
+  In this definition we rely on the fact that in the first clause we can interpret type-variables @{text \<alpha>} as 
   term variables @{text a}. In the last clause we build an abstraction over all
   term-variables of the map-function generated by the auxiliary function 
   @{text "MAP'"}.
@@ -646,10 +647,6 @@
   equivalent to @{text "\<sigma>s \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}, which we just have to compose with
   @{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s \<kappa>\<^isub>q"} according to the type of @{text "\<circ>"}.\qed
   \end{proof}
-  
-  \noindent
-  The reader should note that this lemma fails for the abstraction and representation 
-  functions used in Homeier's quotient package.
 *}
 
 section {* Respectfulness and Preservation \label{sec:resp} *}