# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1262701531 -3600
# Node ID e9e0d181021762e9eb239579a1eea6663f5610ce
# Parent  90bde96f5dd17486ff52299728f3aed9e9f06fb4
Trying to state composition quotient.

diff -r 90bde96f5dd1 -r e9e0d1810217 Quot/Examples/AbsRepTest.thy
--- a/Quot/Examples/AbsRepTest.thy	Tue Jan 05 14:23:45 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Tue Jan 05 15:25:31 2010 +0100
@@ -114,8 +114,51 @@
       @{typ "('a fset) fset \<Rightarrow> 'a fset"})
 *}
 
+thm pred_compI
+
+lemma
+  assumes sr: "symp r"
+  and     ss: "symp s"
+  shows "(r OO s) x y = (s OO r) y x"
+using sr ss
+unfolding symp_def
+apply (metis pred_comp.intros pred_compE ss symp_def)
+
+thm rep_abs_rsp
+sorry
+
+term "r^--1"
+
+lemma bla:
+  assumes a1: "Quotient r1 abs1 rep1"
+  and     a2: "Quotient r2 abs2 rep2"
+  shows  "Quotient (r2) (abs1 \<circ> abs2) (rep2 \<circ> rep1)"
+
+sorry
+
+thm bla[OF Quotient_fset list_quotient]
+
+  unfolding Quotient_def
+apply auto
+term rep_fset
+
+lemma
+  assumes sr: "equivp r"
+  and     ss: "equivp s"
+  shows "r OO s = s OO r"
+apply(rule ext)
+apply(rule ext)
+using sr ss
+nitpick
+
+apply(auto)
+apply(rule pred_compI)
+
+definition
+  relation_compose
+where
+  "relation_compose R1 R2 = \<lambda>x y. \<exists> z. (R1 x z \<and> R2 z y)"
 
 
 
-
-end
\ No newline at end of file
+end