--- a/FSet.thy	Fri Nov 13 16:44:36 2009 +0100
+++ b/FSet.thy	Fri Nov 13 19:32:12 2009 +0100
@@ -307,8 +307,12 @@
 
 thm m2
 
-thm append_assoc
-(* ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *} *)
+thm neq_Nil_conv
+term REP_fset
+term "op --->"
+thm INSERT_def
+ML {* val defs_sym = flat (map (add_lower_defs @{context}) @{thms INSERT_def}) *}
+(*ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *}*)
 ML {* lift_thm_fset @{context} @{thm m1} *}
 ML {* lift_thm_fset @{context} @{thm m2} *}
 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *}
@@ -398,16 +402,6 @@
 prove {* Syntax.check_term @{context} rg *}
 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}
 apply(atomize(full))
-apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
-apply (rule FUN_QUOTIENT)
-apply (rule FUN_QUOTIENT)
-apply (rule QUOTIENT_fset)
-apply (rule FUN_QUOTIENT)
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
-apply (rule IDENTITY_QUOTIENT)
-apply (rule IDENTITY_QUOTIENT)
-apply (tactic {*  (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 done
 ML {*
@@ -460,11 +454,18 @@
   | _ => f trm trm2
 *}
 
+(*ML_prf {*
+val concl = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ()))))
+val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP2})
+val insts = Thm.first_order_match (pat, concl)
+val t = Drule.instantiate insts @{thm APPLY_RSP2}
+*}*)
+
 ML {*
 fun tyRel2 lthy ty gty =
   if ty = gty then HOLogic.eq_const ty else
 
-  case find_first (fn x => Sign.typ_instance (ProofContext.theory_of lthy) (gty, (#qtyp x))) (quotdata_lookup lthy) of
+  case quotdata_lookup lthy (fst (dest_Type gty)) of
     SOME quotdata =>
       if Sign.typ_instance (ProofContext.theory_of lthy) (ty, #rtyp quotdata) then
         case #rel quotdata of
@@ -712,41 +713,22 @@
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
-apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
-apply (rule IDENTITY_QUOTIENT)
-apply (rule FUN_QUOTIENT)
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
-
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
+apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
+apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *})
+apply assumption
+apply (rule refl)
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
-apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
-apply (rule IDENTITY_QUOTIENT)
-apply (rule FUN_QUOTIENT)
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
-
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
+apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
+apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
-apply (rule IDENTITY_QUOTIENT)
-apply (rule FUN_QUOTIENT)
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
+apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})

--- a/QuotScript.thy	Fri Nov 13 16:44:36 2009 +0100
+++ b/QuotScript.thy	Fri Nov 13 19:32:12 2009 +0100
@@ -390,6 +390,11 @@
   shows "R2 (f x) (g y)"
 using a by (rule FUN_REL_IMP)
 
+lemma APPLY_RSP2:
+  assumes a: "(R1 ===> R2) f g" "R1 x y"
+  shows "R2 (f x) (g y)"
+using a by (rule FUN_REL_IMP)
+
 
 (* combinators: I, K, o, C, W *)