--- a/FSet.thy	Tue Dec 01 18:22:48 2009 +0100
+++ b/FSet.thy	Tue Dec 01 18:41:01 2009 +0100
@@ -12,12 +12,6 @@
 | "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys"
 | "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3"
 
-lemma
-  "(list_eq ===> (list_eq ===> (op =))) (list_eq) (list_eq)"
-apply(simp add: FUN_REL.simps)
-apply(rule allI | rule impI)+
-sorry
-
 lemma list_eq_refl:
   shows "xs \<approx> xs"
   by (induct xs) (auto intro: list_eq.intros)
@@ -297,6 +291,24 @@
   apply (auto simp add: memb_rsp rsp_fold_def)
 done
 
+lemma list_eq_rsp[quot_rsp]:
+  "(op \<approx> ===> op \<approx> ===> op =) (op \<approx>) (op \<approx>)"
+apply(simp add: FUN_REL.simps)
+apply(auto)
+apply(blast intro: list_eq.intros)
+apply(blast intro: list_eq.intros)
+done
+
+lemma list_eq_rsp2[quot_rsp]:
+  "(op \<approx> ===> op =) (op \<approx>) (op \<approx>)"
+apply(simp add: FUN_REL.simps)
+apply(rule allI)+
+apply(rule impI)
+apply(simp add: expand_fun_eq)
+apply(rule allI)
+apply(blast intro: list_eq.intros)
+done
+
 print_quotients
 
 ML {* val qty = @{typ "'a fset"} *}
@@ -310,6 +322,7 @@
 
 thm m1
 
+
 lemma "IN x EMPTY = False"
 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
 apply(tactic {* regularize_tac @{context}  [rel_eqv] 1 *})
@@ -344,6 +357,51 @@
 done
 
 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
+apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
+ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
+apply(tactic {* procedure_tac @{context} @{thm map_append} 1 *})
+apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
+prefer 2
+apply(tactic {* clean_tac @{context} [quot] defs 1 *})
+apply(tactic {* inj_repabs_tac_fset @{context} 1*})
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*})
+ 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*})
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*})
+back 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*})
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+
 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
 done