strengthened tactic for right-hand sides involving lambdas
authorblanchet
Tue Oct 01 23:36:02 2013 +0200 (2013-10-01)
changeset 54018bd2e127389f2
parent 54016 769fcbdf2918
child 54019 1878bab3e1c9
strengthened tactic for right-hand sides involving lambdas
src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Tue Oct 01 22:50:42 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Tue Oct 01 23:36:02 2013 +0200
     1.3 @@ -71,14 +71,14 @@
     1.4      exclsss =
     1.5    mk_primcorec_prelude ctxt defs (f_sel RS trans) THEN
     1.6    mk_primcorec_cases_tac ctxt k m exclsss THEN
     1.7 -  unfold_thms_tac ctxt (@{thms id_apply o_def split_def sum.cases} @ maps @ map_comps @
     1.8 -    map_idents) THEN
     1.9 -  HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE'
    1.10 +  unfold_thms_tac ctxt (@{thms id_apply o_def split_def} @ maps @ map_comps @ map_idents) THEN
    1.11 +  HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE' rtac ext ORELSE'
    1.12      eresolve_tac falseEs ORELSE'
    1.13      resolve_tac split_connectI ORELSE'
    1.14      Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
    1.15      Splitter.split_tac (split_if :: splits) ORELSE'
    1.16      eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
    1.17 +    (CHANGED o SELECT_GOAL (unfold_tac @{thms sum.cases} ctxt)) ORELSE'
    1.18      etac notE THEN' atac));
    1.19  
    1.20  fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_f sel_fs =