# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1262854542 -3600
# Node ID 11a23fe266c4de07753f680511280a49a3276a9e
# Parent  5edb6facc8339d80d380b09865bdbbd84a6a6fc2
cleaning in AbsRepTest.

diff -r 5edb6facc833 -r 11a23fe266c4 Quot/Examples/AbsRepTest.thy
--- a/Quot/Examples/AbsRepTest.thy	Wed Jan 06 16:24:21 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Thu Jan 07 09:55:42 2010 +0100
@@ -212,7 +212,9 @@
 apply rule
 apply (rule equivp_reflp[OF fset_equivp])
 apply (rule list_rel_refl)
-apply (metis equivp_def fset_equivp)
+apply (metis equivp_def fset_equivp) 
+thm pred_comp_def
+term "op OO"
 apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s")
 apply (metis Quotient_rel[OF Quotient_fset])
 prefer 2
@@ -229,7 +231,6 @@
 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
 apply (rule list_rel_refl)
 apply (metis equivp_def fset_equivp)
-apply auto
 sorry
 
 lemma bla:
@@ -242,8 +243,6 @@
 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
@@ -258,36 +257,7 @@
 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)"
-sorry
-
-
-  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)"
-
-
+(* Doesn't work: *)
+(* thm bla2[OF Quotient_fset Quotient_fset] *)
 
 end