--- a/Quot/Examples/AbsRepTest.thy	Thu Jan 07 09:55:42 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Thu Jan 07 10:13:15 2010 +0100
@@ -135,22 +135,15 @@
   apply(simp add: Quotient_abs_rep[OF a])
 done
 
+(* Trying to use induction: *)
 lemma help1: "list_rel op \<approx>1 ba [] \<equiv> ba = []"
 apply(induct ba)
 apply (auto)
 done
-
 lemma help2: "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) (x # xs) [] \<equiv> False"
 sorry
 lemma help2a: "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) [] (x # xs) \<equiv> False"
 sorry
-
-(* not used anymore *)
-lemma help3: "list_rel op \<approx>1 [] b \<equiv> b = []"
-apply (induct b)
-apply auto
-done
-
 lemma help4: "abs_fset (a # b) = abs_fset [] \<equiv> False"
 sorry
 lemma help4a: "abs_fset [] = abs_fset (a # b) \<equiv> False"
@@ -159,7 +152,7 @@
 lemma help5: "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) x x"
 sorry
 
-lemma bla0pre:
+lemma quotient_compose_list_pre_ind:
  "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r s =
        ((list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r r \<and>
         (list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
@@ -172,27 +165,9 @@
 apply (auto simp add: help2a help4a help5 help1 help2 help4 )
 sorry
 
-lemma bla0:
-  shows  "Quotient ((list_rel op \<approx>1) OO (op \<approx>1) OO (list_rel op \<approx>1)) 
-               (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 bla0pre)
-done
+(* Trying to solve it directly: *)
 
-lemma bla0pre2:
+lemma quotient_compose_list_pre:
  "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r s =
        ((list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r r \<and>
         (list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
@@ -212,15 +187,11 @@
 apply rule
 apply (rule equivp_reflp[OF fset_equivp])
 apply (rule list_rel_refl)
-apply (metis equivp_def fset_equivp) 
-thm pred_comp_def
-term "op OO"
+apply (metis equivp_def fset_equivp)
 apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s")
 apply (metis Quotient_rel[OF Quotient_fset])
 prefer 2
 apply rule
-thm rep_abs_rsp
-thm rep_abs_rsp[of "list_rel op \<approx>1" "map abs_fset"]
 apply (rule rep_abs_rsp[of "list_rel op \<approx>1" "map abs_fset"])
 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
 apply (rule list_rel_refl)
@@ -233,10 +204,30 @@
 apply (metis equivp_def fset_equivp)
 sorry
 
-lemma bla:
+lemma quotient_compose_list:
+  shows  "Quotient ((list_rel op \<approx>1) OO (op \<approx>1) OO (list_rel op \<approx>1))
+               (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 quotient_compose_ok:
   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)) 
+  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)+
@@ -247,17 +238,19 @@
 apply -
 sorry
 
-lemma bla2:
+(* This is the general statement but the types are wrong as in following exanples *)
+lemma quotient_compose_general:
   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)"
+  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 quotient_compose_ok     [OF Quotient_fset]
+thm quotient_compose_general[OF Quotient_fset]
 
-thm bla [OF Quotient_fset Quotient_fset]
+thm quotient_compose_ok     [OF Quotient_fset Quotient_fset]
 (* Doesn't work: *)
-(* thm bla2[OF Quotient_fset Quotient_fset] *)
+(* thm quotient_compose_general[OF Quotient_fset Quotient_fset] *)
 
 end