--- a/FSet.thy	Tue Oct 27 12:20:57 2009 +0100
+++ b/FSet.thy	Tue Oct 27 14:59:00 2009 +0100
@@ -292,7 +292,7 @@
 (* The all_prs and ex_prs should be proved for the instance... *)
 ML {*
 fun r_mk_comb_tac_fset ctxt =
-  r_mk_comb_tac ctxt @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
+  r_mk_comb_tac ctxt @{typ "'a list"} @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
   (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs})
 *}
 
@@ -301,6 +301,15 @@
 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
 
+ML {* val rty = @{typ "'a list"} *}
+
+ML {*
+fun r_mk_comb_tac_fset ctxt =
+  r_mk_comb_tac ctxt rty @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
+  (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs})
+*}
+
+
 ML {* trm_r *}
 prove list_induct_tr: trm_r
 apply (atomize(full))
@@ -336,27 +345,6 @@
 lemma id_apply2 [simp]: "id x \<equiv> x"
   by (simp add: id_def)
 
-ML {*
-   val lpis = @{thm LAMBDA_PRS} OF [@{thm QUOTIENT_fset}, @{thm IDENTITY_QUOTIENT}];
-   val lpist = @{thm "HOL.sym"} OF [lpis];
-   val lam_prs = MetaSimplifier.rewrite_rule [@{thm id_apply2}] lpist
-*}
-
-text {* the proper way to do it *}
-ML {*
-  fun findabs rty tm =
-    case tm of
-      Abs(_, T, b) =>
-        let
-          val b' = subst_bound ((Free ("x", T)), b);
-          val tys = findabs rty b'
-          val ty = fastype_of tm
-        in if needs_lift rty ty then (ty :: tys) else tys
-        end
-    | f $ a => (findabs rty f) @ (findabs rty a)
-    | _ => []
-*}
-
 ML {* val quot = @{thm QUOTIENT_fset} *}
 ML {* val abs = findabs @{typ "'a list"} (prop_of (atomize_thm @{thm list_induct_hol4})) *}
 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}
@@ -367,10 +355,9 @@
     handle _ => thm
 *}
 
-ML {* val m2_t' = eqsubst_thm @{context} [lam_prs] @{thm m2_t} *}
+ML {* val m2_t' = simp_lam_prs @{context} @{thm m2_t} *}
 
 ML {* val ithm = simp_allex_prs @{context} quot m2_t' *}
-ML fset_defs_sym
 
 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *}
 ML {* ObjectLogic.rulify rthm *}
@@ -405,8 +392,9 @@
 
 thm fold1.simps(2)
 thm list.recs(2)
+thm map_append
 
-ML {* val ind_r_a = atomize_thm @{thm map_append} *}
+ML {* val ind_r_a = atomize_thm @{thm list_induct_hol4} *}
 (*  prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
   ML_prf {*  fun tac ctxt =
        (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
@@ -420,10 +408,10 @@
   val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
   val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt);
 *}
+
 prove rg
 apply(atomize(full))
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (auto)
 done
 
 ML {* val (g, thm, othm) =
@@ -433,6 +421,7 @@
    (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs})
   )
 *}
+
 ML {*
     fun tac2 ctxt =
      (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm]))
@@ -455,12 +444,9 @@
 ML {* val ind_r_l2 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l1 *}
 ML {* val ind_r_l3 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l2 *}
 ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *}
-ML {* val ind_r_a = simp_allex_prs @{context} ind_r_l4 *}
+ML {* val ind_r_a = simp_allex_prs @{context} quot ind_r_l4 *}
 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *}
 ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *}
-
-
-ML {* hd fset_defs_sym *}
 ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a1 *}
 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *}
 ML {* ObjectLogic.rulify ind_r_s *}
@@ -476,7 +462,7 @@
      (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp} @ @{thms ho_all_prs ho_ex_prs});
   val ind_r_t = repabs_eq2 @{context} (g, t, ot);
   val ind_r_l = simp_lam_prs @{context} ind_r_t;
-  val ind_r_a = simp_allex_prs @{context} ind_r_l;
+  val ind_r_a = simp_allex_prs @{context} quot ind_r_l;
   val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a;
   val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d
 in

--- a/IntEx.thy	Tue Oct 27 12:20:57 2009 +0100
+++ b/IntEx.thy	Tue Oct 27 14:59:00 2009 +0100
@@ -3,7 +3,7 @@
 begin
 
 fun
-  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" 
+  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
 where
   "intrel (x, y) (u, v) = (x + v = u + y)"
 
@@ -123,7 +123,7 @@
 lemma intrel_refl: "intrel a a"
   sorry
 
-lemma ho_plus_rsp : 
+lemma ho_plus_rsp:
   "IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel my_plus my_plus"
   by (simp)
 

--- a/QuotMain.thy	Tue Oct 27 12:20:57 2009 +0100
+++ b/QuotMain.thy	Tue Oct 27 14:59:00 2009 +0100
@@ -701,14 +701,26 @@
   | _ => fn _ => no_tac) i st
 *}
 
+ML {*
+fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} =>
+  let
+    val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl;
+    val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
+    val insts = Thm.match (pat, concl)
+in
+  if needs_lift rty (type_of f) then
+    rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
+  else no_tac
+end
+handle _ => no_tac)
+*}
 
 ML {*
-fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms =
+fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
   (FIRST' [
     rtac @{thm FUN_QUOTIENT},
     rtac quot_thm,
     rtac @{thm IDENTITY_QUOTIENT},
-    rtac @{thm ext},
     rtac trans_thm,
     LAMBDA_RES_TAC ctxt,
     res_forall_rsp_tac ctxt,
@@ -719,8 +731,10 @@
     ),
     (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
     rtac refl,
-    rtac @{thm arg_cong2[of _ _ _ _ "op ="]},
-    (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
+(*    rtac @{thm arg_cong2[of _ _ _ _ "op ="]},*)
+    (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
+    Cong_Tac.cong_tac @{thm cong},
+    rtac @{thm ext},
     rtac reflex_thm,
     atac,
     (
@@ -737,7 +751,7 @@
     val rt = build_repabs_term lthy thm constructors rty qty;
     val rg = Logic.mk_equals ((Thm.prop_of thm), rt);
     fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'
-      (REPEAT_ALL_NEW (r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms));
+      (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms));
     val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);
   in
     (rt, cthm, thm)