# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1262707611 -3600
# Node ID f73e2f5f17b28595db909c8e197c2033e5879430
# Parent  e9e0d181021762e9eb239579a1eea6663f5610ce
Struggling with composition

diff -r e9e0d1810217 -r f73e2f5f17b2 Quot/Examples/AbsRepTest.thy
--- a/Quot/Examples/AbsRepTest.thy	Tue Jan 05 15:25:31 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Tue Jan 05 17:06:51 2010 +0100
@@ -114,8 +114,6 @@
       @{typ "('a fset) fset \<Rightarrow> 'a fset"})
 *}
 
-thm pred_compI
-
 lemma
   assumes sr: "symp r"
   and     ss: "symp s"
@@ -123,20 +121,34 @@
 using sr ss
 unfolding symp_def
 apply (metis pred_comp.intros pred_compE ss symp_def)
+done
 
-thm rep_abs_rsp
+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)"
+using a1
+apply -
 sorry
 
-term "r^--1"
+lemma bla2:
+  assumes a2: "Quotient r1 abs1 rep_fset"
+  and         "Quotient r2 abs2 rep2"
+  shows  "Quotient ((list_rel r2) OO r1 OO (list_rel r2)) (abs1 \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)"
+sorry
+
+thm bla [OF Quotient_fset]
+thm bla2[OF Quotient_fset]
+
+thm bla [OF Quotient_fset Quotient_fset]
+thm bla2[OF Quotient_fset Quotient_fset]
 
 lemma bla:
   assumes a1: "Quotient r1 abs1 rep1"
   and     a2: "Quotient r2 abs2 rep2"
-  shows  "Quotient (r2) (abs1 \<circ> abs2) (rep2 \<circ> rep1)"
-
+  shows  "Quotient r2 (abs1 \<circ> abs2) (rep2 \<circ> rep1)"
 sorry
 
-thm bla[OF Quotient_fset list_quotient]
 
   unfolding Quotient_def
 apply auto