# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1276406093 -7200
# Node ID 01d08af79f0149e105701c2501ce248e8427eaaa
# Parent  fec38b7ceeb303bf3a94cc272d05b17d88bbd53a
qpaper.

diff -r fec38b7ceeb3 -r 01d08af79f01 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Sun Jun 13 06:50:34 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Sun Jun 13 07:14:53 2010 +0200
@@ -224,8 +224,8 @@
   They generate definitions, like the one above for @{text "\<Union>"}, 
   according to the type of the raw constant and the type
   of the quotient constant. This means we also have to extend the notions
-  of \emph{respectfulness} and \emph{preservation} from Homeier 
-  \cite{Homeier05}.
+  of \emph{aggregate relation}, \emph{respectfulness} and \emph{preservation}
+  from Homeier \cite{Homeier05}.
 
   We will also address the criticism by Paulson \cite{Paulson06} cited at the
   beginning of this section about having to collect theorems that are lifted from the raw
@@ -363,7 +363,10 @@
   obtaining a list and applies @{term abs_fset} obtaining the composed
   finite set.
 
-  {\it we can compactify the term by noticing that map id\ldots id = id}
+  For every type map function we require the property that @{term "map id = id"}.
+  With this we can compactify the term, removing the identity mappings,
+  obtaining a definition that is the same as the one privided by Homeier
+  in the cases where the internal type does not change.
 
   {\it we should be able to prove}
 
@@ -581,7 +584,7 @@
   how the proof is performed. The first step is always the application of
   of the following lemma:
 
-  @{term "[|A; A --> B; B = C; C = D|] ==> D"}
+  @{term [display, indent=10] "[|A; A --> B; B = C; C = D|] ==> D"}
 
   With @{text A} instantiated to the original raw theorem, 
        @{text B} instantiated to @{text "REG(A)"},
@@ -617,24 +620,26 @@
 
   First, bounded universal quantifiers can be removed on the right:
 
-  @{thm [display] ball_reg_right[no_vars]}
+  @{thm [display, indent=10] ball_reg_right[no_vars]}
 
   They can be removed anywhere if the relation is an equivalence relation:
 
-  @{thm [display] ball_reg_eqv[no_vars]}
+  @{thm [display, indent=10] ball_reg_eqv[no_vars]}
 
   And finally it can be removed anywhere if @{term R2} is an equivalence relation, then:
-  \[
-  @{thm (rhs) ball_reg_eqv_range[no_vars]} = @{thm (lhs) ball_reg_eqv_range[no_vars]}
-  \]
+
+  @{thm [display, indent=10] (concl) ball_reg_eqv_range[no_vars]}
 
-  The last theorem is new in comparison with Homeier's package; it allows separating
-  regularization from injection.
+  The last theorem is new in comparison with Homeier's package, there the
+  injection procedure would be used to prove goals with such shape, and there
+  the equivalence assumption would be useful. We use it directly also for
+  composed relations where the range type is a type for which we know an
+  equivalence theorem. This allows separating regularization from injection.
 
 *}
 
 (*
-  @{thm (rhs) bex_reg_eqv_range[no_vars]} = @{thm (lhs) bex_reg_eqv_range[no_vars]}
+  @{thm bex_reg_eqv_range[no_vars]}
   @{thm [display] bex_reg_left[no_vars]}
   @{thm [display] bex1_bexeq_reg[no_vars]}
   @{thm [display] bex_reg_eqv[no_vars]}