--- a/FSet.thy	Tue Oct 27 16:15:56 2009 +0100
+++ b/FSet.thy	Tue Oct 27 17:08:47 2009 +0100
@@ -185,23 +185,19 @@
 
 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *}
 
-ML {* MetaSimplifier.rewrite_rule*}
-
-
 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)
-    val defs_sym = map (fn t => eq_reflection OF [t]) defs_all
-    val defs_id = map (MetaSimplifier.rewrite_rule @{thms id_def_sym}) defs_sym
   in
-    map Thm.varifyT defs_id
+    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"
@@ -410,7 +406,7 @@
 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
@@ -456,47 +452,16 @@
   apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10)
 done
 
-(*ML {* val ind_r_l1 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l *}
+ML {* val ind_r_l1 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l *}
 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} quot ind_r_l *}
-(*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 {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a *}
+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} 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 {* 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 {* val thm = atomize_thm @{thm fmap_def[symmetric]} *}
-ML {* val e1 = @{thm fun_cong} OF [thm] *}
-ML {* val f1 = eqsubst_thm @{context} @{thms fun_map.simps} e1 *}
-ML {* val e2 = @{thm fun_cong} OF [f1] *}
-ML {* val f2 = eqsubst_thm @{context} @{thms fun_map.simps} e2 *}
-ML {* val h2 = MetaSimplifier.rewrite_rule @{thms id_def_sym} f2 *}
-ML {* val h3 = eqsubst_thm @{context} @{thms FUN_MAP_I} h2 *}
-ML {* val h2 = MetaSimplifier.rewrite_rule @{thms id_apply2} h3 *}
-ML {* val h4 = eq_reflection OF [h2] *}
-
-ML {*
-fun eqsubst_thm ctxt thms thm =
-  let
-    val goalstate = Goal.init (Thm.cprop_of thm)
-    val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
-      NONE => error "eqsubst_thm"
-    | SOME th => cprem_of th 1
-    val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1
-    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
-    @{thm Pure.equal_elim_rule1} OF [rt,thm]
-  end
-*}
-
-ML {* val ind_r_d = eqsubst_thm @{context} [h4] ind_r_s *}
-ML {* val ind_r_d' = eqsubst_thm @{context} [h4] ind_r_d *}
-ML {* val ind_r_d'' = eqsubst_thm @{context} [h4] ind_r_d' *}
-ML {* ObjectLogic.rulify ind_r_d'' *}
-
-
-
+ML {* ObjectLogic.rulify ind_r_s *}
 
 ML {*
 fun lift thm =
@@ -506,11 +471,11 @@
   val (g, t, ot) =
     repabs_eq @{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});
+     (@{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_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} quot ind_r_l;
-  val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a;
+  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
@@ -524,6 +489,8 @@
 ML {* lift @{thm list_eq.intros(4)} *}
 ML {* lift @{thm list_eq.intros(5)} *}
 ML {* lift @{thm card1_suc} *}
+ML {* lift @{thm map_append} *}
+
 (* ML {* lift @{thm append_assoc} *} *)
 
 thm 

--- a/QuotMain.thy	Tue Oct 27 16:15:56 2009 +0100
+++ b/QuotMain.thy	Tue Oct 27 17:08:47 2009 +0100
@@ -786,18 +786,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]
 *}