diff -r 86fba2c4eeef -r 57bde65f6eb2 FSet.thy --- a/FSet.thy Wed Nov 25 10:52:21 2009 +0100 +++ b/FSet.thy Wed Nov 25 11:41:42 2009 +0100 @@ -176,8 +176,6 @@ term fmap thm fmap_def -ML {* prop_of @{thm fmap_def} *} - ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def FOLD_def} *} lemma memb_rsp: @@ -303,8 +301,6 @@ @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} @ @{thms ho_all_prs ho_ex_prs} *} -ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} -ML {* fun lift_thm_g_fset lthy t g = lift_thm_goal lthy qty "fset" rsp_thms defs t g *} ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} ML {* val consts = lookup_quot_consts defs *} @@ -378,9 +374,6 @@ ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *} - -ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} -ML {* fun lift_thm_g_fset lthy t g = lift_thm_goal lthy qty "fset" rsp_thms defs t g *} ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *} ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.recs(2)})) *} @@ -397,9 +390,6 @@ ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.cases(2)})) *} ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} - - -ML {* map (lift_thm_fset @{context}) @{thms list.cases(2)} *} lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa" apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *}) apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *}) @@ -417,100 +407,14 @@ done - -(* Construction site starts here *) - +ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} -ML {* val consts = lookup_quot_consts defs *} -ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} -ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *} - -ML {* val t_a = atomize_thm @{thm list_induct_part} *} -(* prove {* build_regularize_goal t_a rty rel @{context} *} - ML_prf {* fun tac ctxt = FIRST' [ - rtac rel_refl, - atac, - rtac @{thm universal_twice}, - (rtac @{thm impI} THEN' atac), - rtac @{thm implication_twice}, - //comented out rtac @{thm equality_twice}, // - EqSubst.eqsubst_tac ctxt [0] - [(@{thm equiv_res_forall} OF [rel_eqv]), - (@{thm equiv_res_exists} OF [rel_eqv])], - (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl), - (rtac @{thm RIGHT_RES_FORALL_REGULAR}) - ]; *} - apply (atomize(full)) - apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *}) - done *) -ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} -ML {* - val rt = build_repabs_term @{context} t_r consts rty qty - val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); -*} -prove {* Syntax.check_term @{context} rg *} -ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} -apply(atomize(full)) -apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) -done -ML {* -val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms -*} - -ML {* val abs = findabs rty (prop_of (t_a)) *} -ML {* val aps = findaps rty (prop_of (t_a)) *} -ML {* val lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} -ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} -ML {* val lam_prs_thms = map Thm.varifyT lam_prs_thms *} -ML {* t_t *} -ML {* val (alls, exs) = findallex @{context} rty qty (prop_of t_a); *} -ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *} -ML {* val t_l0 = repeat_eqsubst_thm @{context} (app_prs_thms) t_t *} -ML app_prs_thms -ML {* val t_l = repeat_eqsubst_thm @{context} (lam_prs_thms) t_l0 *} -ML lam_prs_thms -ML {* val t_id = simp_ids @{context} t_l *} -thm INSERT_def -ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *} -ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_id *} -ML allthms -thm FORALL_PRS -ML {* val t_al = MetaSimplifier.rewrite_rule (allthms) t_d *} -ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_al *} -ML {* ObjectLogic.rulify t_s *} - -ML {* val gl = @{term "P (x :: 'a list) (EMPTY :: 'a fset) \ (\e t. P x t \ P x (INSERT e t)) \ P x l"} *} -ML {* val gla = atomize_goal @{theory} gl *} - -prove t_r: {* mk_REGULARIZE_goal @{context} (prop_of t_a) gla *} - -ML_prf {* fun tac ctxt = FIRST' [ - rtac rel_refl, - atac, - rtac @{thm universal_twice}, - (rtac @{thm impI} THEN' atac), - rtac @{thm implication_twice}, - (*rtac @{thm equality_twice},*) - EqSubst.eqsubst_tac ctxt [0] - [(@{thm equiv_res_forall} OF [rel_eqv]), - (@{thm equiv_res_exists} OF [rel_eqv])], - (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl), - (rtac @{thm RIGHT_RES_FORALL_REGULAR}) - ]; *} - - apply (atomize(full)) - apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *}) - done - -ML {* val t_r = @{thm t_r} OF [t_a] *} - -ML {* val ttt = mk_inj_REPABS_goal @{context} (prop_of t_r, gla) *} -ML {* val si = simp_ids_trm (cterm_of @{theory} ttt) *} -prove t_t: {* term_of si *} -ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} -apply(atomize(full)) +(* Construction site starts here *) +lemma "P (x :: 'a list) (EMPTY :: 'a fset) \ (\e t. P x t \ P x (INSERT e t)) \ P x l" +apply (tactic {* procedure_tac @{thm list_induct_part} @{context} 1 *}) +apply (tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) apply (rule FUN_QUOTIENT) apply (rule FUN_QUOTIENT) @@ -579,13 +483,7 @@ apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) +apply (tactic {* clean_tac @{context} quot defs reps_same 1 *}) done -thm t_t -ML {* val t_t = @{thm Pure.equal_elim_rule1} OF [@{thm t_t}, t_r] *} -ML {* val t_l = repeat_eqsubst_thm @{context} (lam_prs_thms) t_t *} -ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_l *} -ML {* val t_al = MetaSimplifier.rewrite_rule (allthms) t_d *} -ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_al *} - end