diff -r 3f15f5e60324 -r 1e8e1b736586 FSet.thy --- 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