--- a/FSet.thy	Sun Nov 29 02:51:42 2009 +0100
+++ b/FSet.thy	Sun Nov 29 03:59:18 2009 +0100
@@ -178,37 +178,38 @@
 
 ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def FOLD_def} *}
 
-lemma memb_rsp:
+lemma memb_rsp[quot_rsp]:
   fixes z
-  assumes a: "list_eq x y"
+  assumes a: "x \<approx> y"
   shows "(z memb x) = (z memb y)"
   using a by induct auto
 
-lemma ho_memb_rsp:
+lemma ho_memb_rsp[quot_rsp]:
   "(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)"
   by (simp add: memb_rsp)
 
-lemma card1_rsp:
+lemma card1_rsp[quot_rsp]:
   fixes a b :: "'a list"
   assumes e: "a \<approx> b"
   shows "card1 a = card1 b"
   using e by induct (simp_all add:memb_rsp)
 
-lemma ho_card1_rsp: "(op \<approx> ===> op =) card1 card1"
+lemma ho_card1_rsp[quot_rsp]: 
+  "(op \<approx> ===> op =) card1 card1"
   by (simp add: card1_rsp)
 
-lemma cons_rsp:
+lemma cons_rsp[quot_rsp]:
   fixes z
   assumes a: "xs \<approx> ys"
   shows "(z # xs) \<approx> (z # ys)"
   using a by (rule list_eq.intros(5))
 
-lemma ho_cons_rsp:
+lemma ho_cons_rsp[quot_rsp]:
   "(op = ===> op \<approx> ===> op \<approx>) op # op #"
   by (simp add: cons_rsp)
 
 lemma append_rsp_fst:
-  assumes a : "list_eq l1 l2"
+  assumes a : "l1 \<approx> l2"
   shows "(l1 @ s) \<approx> (l2 @ s)"
   using a
   by (induct) (auto intro: list_eq.intros list_eq_refl)
@@ -245,9 +246,9 @@
   apply (rule rev_rsp)
   done
 
-lemma append_rsp:
-  assumes a : "list_eq l1 r1"
-  assumes b : "list_eq l2 r2 "
+lemma append_rsp[quot_rsp]:
+  assumes a : "l1 \<approx> r1"
+  assumes b : "l2 \<approx> r2 "
   shows "(l1 @ l2) \<approx> (r1 @ r2)"
   apply (rule list_eq.intros(6))
   apply (rule append_rsp_fst)
@@ -260,11 +261,11 @@
   apply (rule append_sym_rsp)
   done
 
-lemma ho_append_rsp:
+lemma ho_append_rsp[quot_rsp]:
   "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
   by (simp add: append_rsp)
 
-lemma map_rsp:
+lemma map_rsp[quot_rsp]:
   assumes a: "a \<approx> b"
   shows "map f a \<approx> map f b"
   using a
@@ -272,16 +273,15 @@
   apply(auto intro: list_eq.intros)
   done
 
-lemma ho_map_rsp:
+lemma ho_map_rsp[quot_rsp]:
   "(op = ===> op \<approx> ===> op \<approx>) map map"
   by (simp add: map_rsp)
 
 lemma map_append:
-  "(map f (a @ b)) \<approx>
-  (map f a) @ (map f b)"
+  "(map f (a @ b)) \<approx> (map f a) @ (map f b)"
  by simp (rule list_eq_refl)
 
-lemma ho_fold_rsp:
+lemma ho_fold_rsp[quot_rsp]:
   "(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1"
   apply (auto simp add: FUN_REL_EQ)
   apply (case_tac "rsp_fold x")
@@ -295,7 +295,6 @@
 
 print_quotients
 
-
 ML {* val qty = @{typ "'a fset"} *}
 ML {* val rsp_thms =
   @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp}
@@ -304,7 +303,7 @@
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *}
 ML {* val consts = lookup_quot_consts defs *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs *}
+ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *}
 
 lemma "IN x EMPTY = False"
 by (tactic {* lift_tac_fset @{context} @{thm m1} 1 *})
@@ -328,7 +327,7 @@
 apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *})
 done
 
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
 
 lemma "FOLD f g (z::'b) (INSERT a x) =
   (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"
@@ -393,9 +392,6 @@
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 done
 
 quotient_def
@@ -409,21 +405,21 @@
   "fset_case \<equiv> list_case"
 
 (* Probably not true without additional assumptions about the function *)
-lemma list_rec_rsp:
+lemma list_rec_rsp[quot_rsp]:
   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
   apply (auto simp add: FUN_REL_EQ)
   apply (erule_tac list_eq.induct)
   apply (simp_all)
   sorry
 
-lemma list_case_rsp:
+lemma list_case_rsp[quot_rsp]:
   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
   apply (auto simp add: FUN_REL_EQ)
   sorry
 
 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs *}
+ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *}
 
 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *})
@@ -443,7 +439,7 @@
   apply (assumption)
   done
 
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
 
 (* Construction site starts here *)
 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"