--- a/Quot/Examples/FSet3.thy	Thu Jan 07 16:51:38 2010 +0100
+++ b/Quot/Examples/FSet3.thy	Fri Jan 08 10:08:01 2010 +0100
@@ -260,36 +260,95 @@
 apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros)
 done
 
+lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B"
+  apply (rule eq_reflection)
+  apply auto
+  done
+
+lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
+  unfolding list_eq.simps
+  apply(simp only: set_map set_in_eq)
+  done
+
+lemma quotient_compose_list_pre:
+  "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) r s =
+  ((list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) r r \<and>
+  (list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) s s \<and>
+  abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
+  apply rule
+  apply rule
+  apply rule
+  apply (rule list_rel_refl)
+  apply (metis equivp_def fset_equivp)
+  apply rule
+  apply (rule equivp_reflp[OF fset_equivp])
+  apply (rule list_rel_refl)
+  apply (metis equivp_def fset_equivp)
+  apply(rule)
+  apply rule
+  apply (rule list_rel_refl)
+  apply (metis equivp_def fset_equivp)
+  apply rule
+  apply (rule equivp_reflp[OF fset_equivp])
+  apply (rule list_rel_refl)
+  apply (metis equivp_def fset_equivp)
+  apply (subgoal_tac "map abs_fset r \<approx> map abs_fset s")
+  apply (metis Quotient_rel[OF Quotient_fset])
+  apply (auto simp only:)[1]
+  apply (subgoal_tac "map abs_fset r = map abs_fset b")
+  prefer 2
+  apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])
+  apply (subgoal_tac "map abs_fset s = map abs_fset ba")
+  prefer 2
+  apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])
+  apply (simp only: map_rel_cong)
+  apply rule
+  apply (rule rep_abs_rsp[of "list_rel op \<approx>" "map abs_fset"])
+  apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
+  apply (rule list_rel_refl)
+  apply (metis equivp_def fset_equivp)
+  apply rule
+  prefer 2
+  apply (rule rep_abs_rsp_left[of "list_rel op \<approx>" "map abs_fset"])
+  apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
+  apply (rule list_rel_refl)
+  apply (metis equivp_def fset_equivp)
+  apply (erule conjE)+
+  apply (subgoal_tac "map abs_fset r \<approx> map abs_fset s")
+  prefer 2
+  apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp)
+  apply (rule map_rel_cong)
+  apply (assumption)
+  done
+
+lemma quotient_compose_list[quot_thm]:
+  shows  "Quotient ((list_rel op \<approx>) OO (op \<approx>) OO (list_rel op \<approx>))
+  (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
+  unfolding Quotient_def comp_def
+  apply (rule)+
+  apply (simp add: abs_o_rep[OF Quotient_fset] id_simps Quotient_abs_rep[OF Quotient_fset])
+  apply (rule)
+  apply (rule)
+  apply (rule)
+  apply (rule list_rel_refl)
+  apply (metis equivp_def fset_equivp)
+  apply (rule)
+  apply (rule equivp_reflp[OF fset_equivp])
+  apply (rule list_rel_refl)
+  apply (metis equivp_def fset_equivp)
+  apply rule
+  apply rule
+  apply(rule quotient_compose_list_pre)
+  done
+
 lemma fconcat_empty:
   shows "fconcat {||} = {||}"
-apply(lifting_setup concat1)
-apply(regularize)
-defer
+apply(lifting concat1)
 apply(cleaning)
 apply(simp add: comp_def)
-apply(cleaning)
 apply(fold fempty_def[simplified id_simps])
 apply(rule refl)
-apply(injection)
-apply(rule apply_rsp[of "(list_rel (op \<approx>)) OO (op \<approx>) OO (list_rel (op \<approx>))" _ _ "op \<approx>" "concat" _ "[]" "((map rep_fset \<circ> rep_fset) ((abs_fset \<circ> map abs_fset) []))"])
-prefer 2
-ML_prf {* fun dest_comb (f $ a) = (f, a) *}
-apply(tactic {* Quotient_Tacs.quot_true_tac @{context} (fst o dest_comb) 1 *})
-prefer 3
-apply(tactic {* Quotient_Tacs.quot_true_tac @{context} (snd o dest_comb) 1 *})
-apply(rule rep_abs_rsp[of _ "(abs_fset \<circ> map abs_fset)" "(map rep_fset \<circ> rep_fset)"])
-prefer 3
-apply(rule rep_abs_rsp[of _ "((map rep_fset \<circ> rep_fset) ---> abs_fset)" "(abs_fset \<circ> map abs_fset) ---> rep_fset"])
-prefer 2
-apply(rule concat_rsp)
-prefer 3
-apply(injection)
-prefer 2
-apply(thin_tac "Quot_True {||}")
-apply(unfold Quotient_def)
-
-apply(auto)
-sorry
+done
 
 lemma fconcat_insert:
   shows "fconcat (finsert x S) = x |\<union>| fconcat S"