diff -r e5109811c4d4 -r 5edb6facc833 Quot/Examples/AbsRepTest.thy
--- a/Quot/Examples/AbsRepTest.thy	Wed Jan 06 09:19:23 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Wed Jan 06 16:24:21 2010 +0100
@@ -135,6 +135,103 @@
   apply(simp add: Quotient_abs_rep[OF a])
 done
 
+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"
+sorry
+
+lemma help5: "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) x x"
+sorry
+
+lemma bla0pre:
+ "(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))"
+apply(induct r s rule: list_induct2')
+  apply(simp)
+  apply(simp add: help2 help4 help5)
+  apply(simp add: help2a help4a help5)
+  apply(simp add: help5)
+  apply rule
+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
+
+lemma bla0pre2:
+ "(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))"
+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 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 (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)
+apply (metis equivp_def fset_equivp)
+apply rule
+prefer 2
+apply (rule rep_abs_rsp_left[of "list_rel op \<approx>1" "map abs_fset"])
+apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
+apply (rule list_rel_refl)
+apply (metis equivp_def fset_equivp)
+apply auto
+sorry
+
 lemma bla:
   assumes a1: "Quotient (op \<approx>1) abs_fset rep_fset"
   and     a2:  "Quotient r2 abs2 rep2"