killed spurious rotate_tac; use auto instead of blast
authorblanchet
Fri Sep 14 22:23:11 2012 +0200 (2012-09-14)
changeset 493830f71da2988d2
parent 49382 94e9583ea25d
child 49384 94ad5ba23541
killed spurious rotate_tac; use auto instead of blast
src/HOL/Codatatype/BNF_FP.thy
src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
     1.1 --- a/src/HOL/Codatatype/BNF_FP.thy	Fri Sep 14 22:23:11 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/BNF_FP.thy	Fri Sep 14 22:23:11 2012 +0200
     1.3 @@ -104,6 +104,7 @@
     1.4  "sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
     1.5  by simp
     1.6  
     1.7 +(* TODO: cleanup *)
     1.8  lemma UN_compreh_bex:
     1.9  "\<Union>{y. \<exists>x \<in> A. y = {}} = {}"
    1.10  "\<Union>{y. \<exists>x \<in> A. y = {x}} = A"
     2.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 22:23:11 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 22:23:11 2012 +0200
     2.3 @@ -113,22 +113,23 @@
     2.4  val induct_prem_prem_thms_delayed =
     2.5    @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]};
     2.6  
     2.7 +(* TODO: Get rid of the "auto_tac" (or at least use a naked context) *)
     2.8  fun mk_induct_prem_prem_endgame_tac _ 0 = atac ORELSE' rtac @{thm singletonI}
     2.9    | mk_induct_prem_prem_endgame_tac ctxt qq =
    2.10      REPEAT_DETERM_N qq o
    2.11        (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
    2.12         etac @{thm induct_set_step}) THEN'
    2.13 -    atac;
    2.14 +    atac ORELSE' SELECT_GOAL (auto_tac ctxt);
    2.15  
    2.16 -(* TODO: Get rid of the "blast_tac" (or at least use a naked context) *)
    2.17  fun mk_induct_discharge_prem_prems_tac ctxt nn ixs set_natural's pre_set_defs =
    2.18    EVERY' (maps (fn ((pp, jj), (qq, kk)) =>
    2.19 -      [rotate_tac (~ nn), select_prem_tac nn (dtac meta_spec) kk, rotate_tac ~1,(*###*) etac meta_mp,
    2.20 -       SELECT_GOAL (Local_Defs.unfold_tac ctxt pre_set_defs), (* ### why on a line of its own? *)
    2.21 +      [select_prem_tac nn (dtac meta_spec) kk, rotate_tac ~1 (*FIXME: needed?*), etac meta_mp,
    2.22 +       SELECT_GOAL (Local_Defs.unfold_tac ctxt pre_set_defs), (* FIXME: ### why on a line of its own? *)
    2.23         SELECT_GOAL (Local_Defs.unfold_tac ctxt (set_natural's @ induct_prem_prem_thms)),
    2.24         SELECT_GOAL (Local_Defs.unfold_tac ctxt
    2.25           (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)),
    2.26 -       rtac (mk_UnIN pp jj) THEN' mk_induct_prem_prem_endgame_tac ctxt qq ORELSE' blast_tac ctxt])
    2.27 +       rtac (mk_UnIN pp jj) THEN' mk_induct_prem_prem_endgame_tac ctxt qq ORELSE'
    2.28 +         SELECT_GOAL (auto_tac ctxt)])
    2.29      (rev ixs)) 1;
    2.30  
    2.31  fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ixs =