# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1262711343 -3600
# Node ID 18b71981c1f0fbecdb42148a2e785af9b04abc4f
# Parent  f73e2f5f17b28595db909c8e197c2033e5879430
Trying the proof

diff -r f73e2f5f17b2 -r 18b71981c1f0 Quot/Examples/AbsRepTest.thy
--- a/Quot/Examples/AbsRepTest.thy	Tue Jan 05 17:06:51 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Tue Jan 05 18:09:03 2010 +0100
@@ -123,10 +123,24 @@
 apply (metis pred_comp.intros pred_compE ss symp_def)
 done
 
+lemma abs_o_rep:
+  assumes a: "Quotient r absf repf"
+  shows "absf o repf = id"
+  apply(rule ext)
+  apply(simp add: Quotient_abs_rep[OF a])
+done
+
 lemma bla:
   assumes a1: "Quotient (op \<approx>1) abs_fset rep_fset"
   and     a2:  "Quotient r2 abs2 rep2"
   shows  "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2)) (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)"
+  unfolding Quotient_def comp_def
+apply (rule)+
+apply (simp add: abs_o_rep[OF a2] id_simps Quotient_abs_rep[OF Quotient_fset])
+apply (rule)
+apply (rule)
+sledgehammer
+apply (metis Quotient_def a2 equivp_reflp fset_equivp list_quotient list_rel_rel pred_comp.cases pred_comp.intros rep_fset_def)
 using a1
 apply -
 sorry