--- a/FSet.thy	Wed Oct 28 01:48:45 2009 +0100
+++ b/FSet.thy	Wed Oct 28 01:49:31 2009 +0100
@@ -187,8 +187,20 @@
 *}
 
 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *}
+
+ML {*
+fun add_lower_defs ctxt defs =
+  let
+    val defs_pre_sym = map symmetric defs
+    val defs_atom = map atomize_thm defs_pre_sym
+    val defs_all = flat (map (add_lower_defs_aux ctxt) defs_atom)
+  in
+    map Thm.varifyT defs_all
+  end
+*}
 ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *}
 
+
 lemma memb_rsp:
   fixes z
   assumes a: "list_eq x y"
@@ -295,7 +307,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})
 *}
 
@@ -304,6 +316,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))
@@ -339,27 +360,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 *}
@@ -370,10 +370,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 *}
@@ -408,8 +407,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} *}
 (*  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
@@ -423,33 +423,20 @@
   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) =
+ML {* val ind_r_t =
   Toplevel.program (fn () =>
-  repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
+  repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
    @{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 {*
-    fun tac2 ctxt =
-     (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm]))
-     THEN' (rtac othm); *}
-(* ML {*    val cthm = Goal.prove @{context} [] [] g (fn x => tac2 (#context x) 1);
-*} *)
-
-ML {*
-  val ind_r_t2 =
-  Toplevel.program (fn () =>
-    repabs_eq2 @{context} (g, thm, othm)
-  )
-*}
-ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t2 *}
+ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t *}
 lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1"
   apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10)
 done
@@ -458,13 +445,10 @@
 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_d = repeat_eqsubst_thm @{context} 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 *}
 
@@ -473,14 +457,13 @@
 let
   val ind_r_a = atomize_thm thm;
   val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context};
-  val (g, t, ot) =
-    repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
+  val ind_r_t =
+    repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
      @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
-     (@{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);
+     (@{thms ho_memb_rsp ho_cons_rsp  ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs});
   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_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a;
+  val ind_r_a = simp_allex_prs @{context} quot ind_r_l;
+  val ind_r_d = repeat_eqsubst_thm @{context} fset_defs_sym ind_r_a;
   val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d
 in
   ObjectLogic.rulify ind_r_s
@@ -488,15 +471,19 @@
 *}
 ML fset_defs
 
+lemma eq_r: "a = b \<Longrightarrow> a \<approx> b"
+by (simp add: list_eq_refl)
+
 
 ML {* lift @{thm m2} *}
 ML {* lift @{thm m1} *}
 ML {* lift @{thm list_eq.intros(4)} *}
 ML {* lift @{thm list_eq.intros(5)} *}
 ML {* lift @{thm card1_suc} *}
-(* ML {* lift @{thm append_assoc} *} *)
+ML {* lift @{thm map_append} *}
+ML {* lift @{thm eq_r[OF append_assoc]} *}
 
-thm 
+thm
 
 
 (*notation ( output) "prop" ("#_" [1000] 1000) *)

--- a/IntEx.thy	Wed Oct 28 01:48:45 2009 +0100
+++ b/IntEx.thy	Wed Oct 28 01:49:31 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)
 
@@ -168,22 +168,16 @@
 ML {* val t_a = atomize_thm @{thm plus_assoc_pre} *}
 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *}
 
-ML {* val (g, thm, othm) =
+ML {* val t_t =
   Toplevel.program (fn () =>
-  repabs_eq @{context} t_r consts rty qty
+  repabs @{context} t_r consts rty qty
    quot rel_refl trans2
    rsp_thms
   )
 *}
-ML {*
-  val t_t2 =
-  Toplevel.program (fn () =>
-    repabs_eq2 @{context} (g, thm, othm)
-  )
-*}
-
 
 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *}
+
 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}
 
 ML {*
@@ -191,8 +185,8 @@
     simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm)
     handle _ => thm
 *}
-ML {* t_t2 *}
-ML {* val t_l = simp_lam_prs @{context} t_t2 *}
+ML {* t_t *}
+ML {* val t_l = simp_lam_prs @{context} t_t *}
 
 ML {* val t_a = simp_allex_prs @{context} quot t_l *}
 

--- a/QuotMain.thy	Wed Oct 28 01:48:45 2009 +0100
+++ b/QuotMain.thy	Wed Oct 28 01:49:31 2009 +0100
@@ -708,14 +708,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,
@@ -726,8 +738,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,
     (
@@ -739,27 +753,15 @@
 *}
 
 ML {*
-fun repabs_eq lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms =
+fun repabs lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms =
   let
     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)
-  end
-*}
-
-ML {*
-fun repabs_eq2 lthy (rt, thm, othm) =
-  let
-    fun tac2 ctxt =
-     (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm]))
-     THEN' (rtac othm);
-    val cthm = Goal.prove lthy [] [] rt (fn x => tac2 (#context x) 1);
-  in
-    cthm
+    @{thm Pure.equal_elim_rule1} OF [cthm, thm]
   end
 *}
 
@@ -777,18 +779,27 @@
     val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'))
     val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac));
   in
-    Simplifier.rewrite_rule [rt] thm
+    @{thm Pure.equal_elim_rule1} OF [rt,thm]
   end
 *}
 
+ML {*
+  fun repeat_eqsubst_thm ctxt thms thm =
+    repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm)
+    handle _ => thm
+*}
+
 text {* expects atomized definition *}
 ML {*
   fun add_lower_defs_aux ctxt thm =
     let
-      val e1 = @{thm fun_cong} OF [thm]
-      val f = eqsubst_thm ctxt @{thms fun_map.simps} e1
+      val e1 = @{thm fun_cong} OF [thm];
+      val f = eqsubst_thm ctxt @{thms fun_map.simps} e1;
+      val g = MetaSimplifier.rewrite_rule @{thms id_def_sym} f;
+      val h = repeat_eqsubst_thm ctxt @{thms FUN_MAP_I} g;
+      val i = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] h
     in
-      thm :: (add_lower_defs_aux ctxt f)
+      thm :: (add_lower_defs_aux ctxt i)
     end
     handle _ => [thm]
 *}
@@ -855,14 +866,13 @@
 fun lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same t_defs t = let
   val t_a = atomize_thm t;
   val t_r = regularize t_a rty rel rel_eqv lthy;
-  val t_t1 = repabs_eq lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;
-  val t_t2 = repabs_eq2 lthy t_t1;
+  val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;
   val abs = findabs rty (prop_of t_a);
   val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs;
   fun simp_lam_prs lthy thm =
     simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm)
     handle _ => thm
-  val t_l = simp_lam_prs lthy t_t2;
+  val t_l = simp_lam_prs lthy t_t;
   val t_a = simp_allex_prs lthy quot t_l;
   val t_defs_sym = add_lower_defs lthy t_defs;
   val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a;