--- a/Quotient-Paper/Paper.thy	Wed May 26 16:28:35 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Wed May 26 16:56:38 2010 +0200
@@ -78,19 +78,19 @@
   surprising, none of them can deal compositions of quotients, for example with 
   lifting theorems about @{text "concat"}:
 
-  @{thm concat.simps(1)}\\
-  @{thm concat.simps(2)[no_vars]}
+  @{thm [display] concat.simps(1)}
+  @{thm [display] concat.simps(2)[no_vars]}
 
   \noindent
   One would like to lift this definition to the operation:
 
-  @{thm fconcat_empty[no_vars]}\\
-  @{thm fconcat_insert[no_vars]}
+  @{thm [display] fconcat_empty[no_vars]}
+  @{thm [display] fconcat_insert[no_vars]}
 
   \noindent
   What is special about this operation is that we have as input
   lists of lists which after lifting turn into finite sets of finite
-  sets. 
+  sets.
 *}
 
 subsection {* Contributions *}
@@ -145,7 +145,7 @@
   \end{definition}
 
   \begin{definition}[Relation map and function map]\\
-  @{thm fun_rel_def[no_vars]}\\
+  @{thm fun_rel_def[of "R1" "R2", no_vars]}\\
   @{thm fun_map_def[no_vars]}
   \end{definition}
 
@@ -219,18 +219,20 @@
   and itself, for example the respectfullness for @{term "append"}
   can be stated as:
 
-  @{thm append_rsp[no_vars]}
+  @{thm [display] append_rsp[no_vars]}
 
+  \noindent
   Which is equivalent to:
 
-  @{thm append_rsp[no_vars,simplified fun_rel_def]}
+  @{thm [display] append_rsp_unfolded[no_vars]}
 
   Below we show the algorithm for finding the aggregate relation.
   This algorithm uses
   the relation composition which we define as:
 
   \begin{definition}[Composition of Relations]
-  @{abbrev "rel_conj R1 R2"}
+  @{abbrev "rel_conj R1 R2"} where @{text OO} is the predicate
+  composition @{thm pred_compI[no_vars]}
   \end{definition}
 
   Given an aggregate raw type and quotient type:
@@ -250,16 +252,35 @@
   \end{itemize}
 
   Again, the the behaviour of our algorithm in the last situation is
-  novel, so lets look at the example of respectfullness for @{term concat}:
+  novel, so lets look at the example of respectfullness for @{term concat}.
+  The statement as computed by the algorithm above is:
+
+  @{thm [display] concat_rsp[no_vars]}
 
-  @{thm concat_rsp}
+  \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]}
 
-  This means...
+  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}.
 
 *}
 
 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.
+*}
+
 section {* Lifting Theorems *}
 
 text{*
@@ -268,7 +289,7 @@
   theorem that needs to be proved is the one needed to lift theorems
   about concat:
 
-  @{thm quotient_compose_list[no_vars]}
+  @{thm [display] quotient_compose_list[no_vars]}
 *}
 
 text {* TBD *}