diff -r 9c44db3eef95 -r dcffc2f132c9 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Tue Jun 15 07:58:33 2010 +0200
+++ b/Nominal/FSet.thy	Tue Jun 15 09:12:54 2010 +0200
@@ -80,7 +80,7 @@
 
 text {* Composition Quotient *}
 
-lemma list_rel_refl:
+lemma list_rel_refl1:
   shows "(list_rel op \<approx>) r r"
   by (rule list_rel_refl) (metis equivp_def fset_equivp)
 
@@ -88,7 +88,7 @@
   shows "(list_rel op \<approx> OOO op \<approx>) r r"
 proof
   have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
-  show "list_rel op \<approx> r r" by (rule list_rel_refl)
+  show "list_rel op \<approx> r r" by (rule list_rel_refl1)
   with * show "(op \<approx> OO list_rel op \<approx>) r r" ..
 qed
 
@@ -103,6 +103,7 @@
   unfolding list_eq.simps
   by (simp only: set_map set_in_eq)
 
+
 lemma quotient_compose_list[quot_thm]:
   shows  "Quotient ((list_rel op \<approx>) OOO (op \<approx>))
     (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
@@ -112,11 +113,11 @@
   show "abs_fset (map abs_fset (map rep_fset (rep_fset a))) = a"
     by (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id)
   have b: "list_rel op \<approx> (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
-    by (rule list_rel_refl)
+    by (rule list_rel_refl1)
   have c: "(op \<approx> OO list_rel op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
     by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
   show "(list_rel op \<approx> OOO op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
-    by (rule, rule list_rel_refl) (rule c)
+    by (rule, rule list_rel_refl1) (rule c)
   show "(list_rel op \<approx> OOO op \<approx>) r s = ((list_rel op \<approx> OOO op \<approx>) r r \<and>
         (list_rel op \<approx> OOO op \<approx>) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
   proof (intro iffI conjI)
@@ -148,11 +149,11 @@
     have b: "map rep_fset (map abs_fset r) \<approx> map rep_fset (map abs_fset s)"
       by (rule map_rel_cong[OF d])
     have y: "list_rel op \<approx> (map rep_fset (map abs_fset s)) s"
-      by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_rel_refl[of s]])
+      by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_rel_refl1[of s]])
     have c: "(op \<approx> OO list_rel op \<approx>) (map rep_fset (map abs_fset r)) s"
       by (rule pred_compI) (rule b, rule y)
     have z: "list_rel op \<approx> r (map rep_fset (map abs_fset r))"
-      by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_rel_refl[of r]])
+      by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_rel_refl1[of r]])
     then show "(list_rel op \<approx> OOO op \<approx>) r s"
       using a c pred_compI by simp
   qed
@@ -653,13 +654,13 @@
   assumes a:"list_rel op \<approx> x x'"
   shows "list_rel op \<approx> (x @ z) (x' @ z)"
   using a apply (induct x x' rule: list_induct2')
-  by simp_all (rule list_rel_refl)
+  by simp_all (rule list_rel_refl1)
 
 lemma append_rsp2_pre1:
   assumes a:"list_rel op \<approx> x x'"
   shows "list_rel op \<approx> (z @ x) (z @ x')"
   using a apply (induct x x' arbitrary: z rule: list_induct2')
-  apply (rule list_rel_refl)
+  apply (rule list_rel_refl1)
   apply (simp_all del: list_eq.simps)
   apply (rule list_rel_app_l)
   apply (simp_all add: reflp_def)
@@ -674,7 +675,7 @@
   apply (rule a)
   using b apply (induct z z' rule: list_induct2')
   apply (simp_all only: append_Nil2)
-  apply (rule list_rel_refl)
+  apply (rule list_rel_refl1)
   apply simp_all
   apply (rule append_rsp2_pre1)
   apply simp
@@ -1414,9 +1415,6 @@
   | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
 *}
 
-no_notation
-  list_eq (infix "\<approx>" 50)
-
 ML {*
 open Quotient_Info;
 
@@ -1678,4 +1676,79 @@
 apply auto
 done
 
+lemma list_rel_refl:
+  assumes q: "equivp R"
+  shows "(list_rel R) r r"
+  by (rule list_rel_refl) (metis equivp_def fset_equivp q)
+
+lemma compose_list_refl2:
+  assumes q: "equivp R"
+  shows "(list_rel R OOO op \<approx>) r r"
+proof
+  have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
+  show "list_rel R r r" by (rule list_rel_refl[OF q])
+  with * show "(op \<approx> OO list_rel R) r r" ..
+qed
+
+lemma quotient_compose_list_g[quot_thm]:
+  assumes q: "Quotient R Abs Rep"
+  and     e: "equivp R"
+  shows  "Quotient ((list_rel R) OOO (op \<approx>))
+    (abs_fset \<circ> (map Abs)) ((map Rep) \<circ> rep_fset)"
+  unfolding Quotient_def comp_def
+proof (intro conjI allI)
+  fix a r s
+  show "abs_fset (map Abs (map Rep (rep_fset a))) = a"
+    by (simp add: abs_o_rep[OF q] Quotient_abs_rep[OF Quotient_fset] map_id)
+  have b: "list_rel R (map Rep (rep_fset a)) (map Rep (rep_fset a))"
+    by (rule list_rel_refl[OF e])
+  have c: "(op \<approx> OO list_rel R) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
+    by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
+  show "(list_rel R OOO op \<approx>) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
+    by (rule, rule list_rel_refl[OF e]) (rule c)
+  show "(list_rel R OOO op \<approx>) r s = ((list_rel R OOO op \<approx>) r r \<and>
+        (list_rel R OOO op \<approx>) s s \<and> abs_fset (map Abs r) = abs_fset (map Abs s))"
+  proof (intro iffI conjI)
+    show "(list_rel R OOO op \<approx>) r r" by (rule compose_list_refl2[OF e])
+    show "(list_rel R OOO op \<approx>) s s" by (rule compose_list_refl2[OF e])
+  next
+    assume a: "(list_rel R OOO op \<approx>) r s"
+    then have b: "map Abs r \<approx> map Abs s"
+    proof (elim pred_compE)
+      fix b ba
+      assume c: "list_rel R r b"
+      assume d: "b \<approx> ba"
+      assume e: "list_rel R ba s"
+      have f: "map Abs r = map Abs b"
+        using Quotient_rel[OF list_quotient[OF q]] c by blast
+      have "map Abs ba = map Abs s"
+        using Quotient_rel[OF list_quotient[OF q]] e by blast
+      then have g: "map Abs s = map Abs ba" by simp
+      then show "map Abs r \<approx> map Abs s" using d f map_rel_cong by simp
+    qed
+    then show "abs_fset (map Abs r) = abs_fset (map Abs s)"
+      using Quotient_rel[OF Quotient_fset] by blast
+  next
+    assume a: "(list_rel R OOO op \<approx>) r r \<and> (list_rel R OOO op \<approx>) s s
+      \<and> abs_fset (map Abs r) = abs_fset (map Abs s)"
+    then have s: "(list_rel R OOO op \<approx>) s s" by simp
+    have d: "map Abs r \<approx> map Abs s"
+      by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)
+    have b: "map Rep (map Abs r) \<approx> map Rep (map Abs s)"
+      by (rule map_rel_cong[OF d])
+    have y: "list_rel R (map Rep (map Abs s)) s"
+      by (fact rep_abs_rsp_left[OF list_quotient[OF q], OF list_rel_refl[OF e, of s]])
+    have c: "(op \<approx> OO list_rel R) (map Rep (map Abs r)) s"
+      by (rule pred_compI) (rule b, rule y)
+    have z: "list_rel R r (map Rep (map Abs r))"
+      by (fact rep_abs_rsp[OF list_quotient[OF q], OF list_rel_refl[OF e, of r]])
+    then show "(list_rel R OOO op \<approx>) r s"
+      using a c pred_compI by simp
+  qed
+qed
+
+no_notation
+  list_eq (infix "\<approx>" 50)
+
+
 end