--- a/Nominal/FSet.thy	Wed May 26 16:28:35 2010 +0200
+++ b/Nominal/FSet.thy	Wed May 26 16:56:38 2010 +0200
@@ -164,6 +164,10 @@
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
   by auto
 
+lemma append_rsp_unfolded:
+  "\<lbrakk>x \<approx> y; v \<approx> w\<rbrakk> \<Longrightarrow> x @ v \<approx> y @ w"
+  by auto
+
 lemma [quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
   by (auto simp add: sub_list_def)
@@ -373,6 +377,31 @@
   then show "concat a \<approx> concat b" by simp
 qed
 
+
+
+lemma concat_rsp_unfolded:
+  "\<lbrakk>list_rel op \<approx> a ba; ba \<approx> bb; list_rel op \<approx> bb b\<rbrakk> \<Longrightarrow> concat a \<approx> concat b"
+proof -
+  fix a b ba bb
+  assume a: "list_rel op \<approx> a ba"
+  assume b: "ba \<approx> bb"
+  assume c: "list_rel op \<approx> bb b"
+  have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
+    fix x
+    show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
+      assume d: "\<exists>xa\<in>set a. x \<in> set xa"
+      show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
+    next
+      assume e: "\<exists>xa\<in>set b. x \<in> set xa"
+      have a': "list_rel op \<approx> ba a" by (rule list_rel_symp[OF list_eq_equivp, OF a])
+      have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b])
+      have c': "list_rel op \<approx> b bb" by (rule list_rel_symp[OF list_eq_equivp, OF c])
+      show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
+    qed
+  qed
+  then show "concat a \<approx> concat b" by simp
+qed
+
 lemma [quot_respect]:
   "((op =) ===> op \<approx> ===> op \<approx>) filter filter"
   by auto

--- 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 *}