# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1256656556 -3600
# Node ID 3f15f5e6032489db42d95476b525a70fdfcf03d3
# Parent  18d7d9dc75cbf07c7a8b204e1e89c859fbdeba4d
Manually lifted Map_Append.

diff -r 18d7d9dc75cb -r 3f15f5e60324 FSet.thy
--- a/FSet.thy	Tue Oct 27 15:00:15 2009 +0100
+++ b/FSet.thy	Tue Oct 27 16:15:56 2009 +0100
@@ -184,6 +184,22 @@
 *}
 
 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
+  end
+*}
 ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *}
 
 lemma memb_rsp:
@@ -394,7 +410,7 @@
 thm list.recs(2)
 thm map_append
 
-ML {* val ind_r_a = atomize_thm @{thm list_induct_hol4} *}
+ML {* val ind_r_a = atomize_thm @{thm map_append} *}
 (*  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
@@ -440,16 +456,47 @@
   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_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 = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a1 *}
+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_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *}
-ML {* ObjectLogic.rulify ind_r_s *}
+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 {*
 fun lift thm =