# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1276403662 -7200
# Node ID a827d36fa467deccb5374f528775b28b2bbf095a
# Parent  42d576c547047c62e983c5e1a4bf7b7be4269e63
qpaper / tuning in preservation and general display

diff -r 42d576c54704 -r a827d36fa467 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Sun Jun 13 04:06:06 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Sun Jun 13 06:34:22 2010 +0200
@@ -390,15 +390,15 @@
   for example the respectfullness for @{term "append"}
   can be stated as:
 
-  @{thm [display] append_rsp[no_vars]}
+  @{thm [display, indent=10] append_rsp[no_vars]}
 
   \noindent
-  Which after unfolding @{term "op \<Longrightarrow>"} is equivalent to:
+  Which after unfolding the definition of @{term "op ===>"} is equivalent to:
 
-  @{thm [display] append_rsp_unfolded[no_vars]}
+  @{thm [display, indent=10] append_rsp_unfolded[no_vars]}
 
-  An aggregate relation is defined in terms of relation composition,
-  so we define it first:
+  \noindent An aggregate relation is defined in terms of relation
+  composition, so we define it first:
 
   \begin{definition}[Composition of Relations]
   @{abbrev "rel_conj R1 R2"} where @{text OO} is the predicate
@@ -420,14 +420,14 @@
   respectfullness for @{term concat}. The statement according to
   the definition above is:
 
-  @{thm [display] concat_rsp[no_vars]}
+  @{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] concat_rsp_unfolded[of "a" "a'" "b'" "b", no_vars]}
+  @{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'"}
@@ -441,22 +441,28 @@
 subsection {* Preservation *}
 
 text {*
-  To be able to lift theorems that talk about constants that are not
-  lifted but whose type changes when lifting is performed additionally
-  preservation theorems are needed.
+  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] (concl) cons_prs[no_vars]}
+  @{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] insert_preserve2[no_vars]}
+  @{thm [display, indent=10] insert_preserve2[no_vars]}
 *}
 
 subsection {* Composition of Quotient theorems *}