src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML
changeset 54018 bd2e127389f2
parent 53961 16d9ecdf519a
child 54024 07ab4fd922c2
equal deleted inserted replaced
54016:769fcbdf2918 54018:bd2e127389f2
    69 
    69 
    70 fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms maps map_idents map_comps f_sel k m
    70 fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms maps map_idents map_comps f_sel k m
    71     exclsss =
    71     exclsss =
    72   mk_primcorec_prelude ctxt defs (f_sel RS trans) THEN
    72   mk_primcorec_prelude ctxt defs (f_sel RS trans) THEN
    73   mk_primcorec_cases_tac ctxt k m exclsss THEN
    73   mk_primcorec_cases_tac ctxt k m exclsss THEN
    74   unfold_thms_tac ctxt (@{thms id_apply o_def split_def sum.cases} @ maps @ map_comps @
    74   unfold_thms_tac ctxt (@{thms id_apply o_def split_def} @ maps @ map_comps @ map_idents) THEN
    75     map_idents) THEN
    75   HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE' rtac ext ORELSE'
    76   HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE'
       
    77     eresolve_tac falseEs ORELSE'
    76     eresolve_tac falseEs ORELSE'
    78     resolve_tac split_connectI ORELSE'
    77     resolve_tac split_connectI ORELSE'
    79     Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
    78     Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
    80     Splitter.split_tac (split_if :: splits) ORELSE'
    79     Splitter.split_tac (split_if :: splits) ORELSE'
    81     eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
    80     eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
       
    81     (CHANGED o SELECT_GOAL (unfold_tac @{thms sum.cases} ctxt)) ORELSE'
    82     etac notE THEN' atac));
    82     etac notE THEN' atac));
    83 
    83 
    84 fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_f sel_fs =
    84 fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_f sel_fs =
    85   HEADGOAL (rtac ((if null sel_fs then collapse else collapse RS sym) RS trans) THEN'
    85   HEADGOAL (rtac ((if null sel_fs then collapse else collapse RS sym) RS trans) THEN'
    86     (the_default (K all_tac) (Option.map rtac maybe_disc_f)) THEN' REPEAT_DETERM_N m o atac) THEN
    86     (the_default (K all_tac) (Option.map rtac maybe_disc_f)) THEN' REPEAT_DETERM_N m o atac) THEN