1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 22:23:10 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 22:23:10 2012 +0200
     1.3 @@ -14,7 +14,8 @@
     1.4      tactic
     1.5    val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic
     1.6    val mk_induct_tac: Proof.context -> int list -> int list list ->
     1.7 -    ((int * int) * int) list list list -> thm list -> thm -> thm list -> thm list list -> tactic
     1.8 +    ((int * int) * (int * int)) list list list -> thm list -> thm -> thm list -> thm list list ->
     1.9 +    tactic
    1.10    val mk_inject_tac: Proof.context -> thm -> thm -> tactic
    1.11    val mk_iter_like_tac: thm list -> thm list -> thm list -> thm -> thm -> Proof.context -> tactic
    1.12  end;
    1.13 @@ -111,34 +112,37 @@
    1.14  val induct_prem_prem_thms_delayed =
    1.15    @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]};
    1.16  
    1.17 +fun mk_induct_prem_prem_endgame_tac ctxt qq =
    1.18 +  atac ORELSE'
    1.19 +  rtac @{thm singletonI} ORELSE'
    1.20 +  (REPEAT_DETERM o (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
    1.21 +     etac @{thm induct_set_step}) THEN'
    1.22 +   (atac ORELSE' blast_tac ctxt));
    1.23 +
    1.24  (* TODO: Get rid of the "blast_tac" *)
    1.25 -fun mk_induct_discharge_prem_prems_tac ctxt nn ppjjkks set_natural's pre_set_defs =
    1.26 -  EVERY' (maps (fn ((pp, jj), kk) =>
    1.27 -    [select_prem_tac nn (dtac meta_spec) (nn - kk + 1), rotate_tac ~1, etac meta_mp,
    1.28 +fun mk_induct_discharge_prem_prems_tac ctxt nn ixs set_natural's pre_set_defs =
    1.29 +  EVERY' (maps (fn ((pp, jj), (qq, kk)) =>
    1.30 +    [select_prem_tac nn (dtac meta_spec) (nn - kk + 1), rotate_tac ~1,(*###*) etac meta_mp,
    1.31       SELECT_GOAL (Local_Defs.unfold_tac ctxt pre_set_defs), (* ### why on a line of its own? *)
    1.32       SELECT_GOAL (Local_Defs.unfold_tac ctxt (set_natural's @ induct_prem_prem_thms)),
    1.33       SELECT_GOAL (Local_Defs.unfold_tac ctxt
    1.34         (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)),
    1.35       rtac (mk_UnIN pp jj),
    1.36 -     atac ORELSE'
    1.37 -     rtac @{thm singletonI} ORELSE'
    1.38 -     (REPEAT_DETERM o (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
    1.39 -          etac @{thm induct_set_step}) THEN'
    1.40 -      (atac ORELSE' blast_tac ctxt))]) (rev ppjjkks)) 1;
    1.41 +     mk_induct_prem_prem_endgame_tac ctxt qq]) (rev ixs)) 1;
    1.42  
    1.43 -fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ppjjkks =
    1.44 +fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ixs =
    1.45    EVERY [mk_induct_prepare_prem_tac n m k,
    1.46 -    mk_induct_prepare_prem_prems_tac (length ppjjkks), atac 1,
    1.47 -    mk_induct_discharge_prem_prems_tac ctxt nn ppjjkks set_natural's pre_set_defs];
    1.48 +    mk_induct_prepare_prem_prems_tac (length ixs), atac 1,
    1.49 +    mk_induct_discharge_prem_prems_tac ctxt nn ixs set_natural's pre_set_defs];
    1.50  
    1.51 -fun mk_induct_tac ctxt ns mss ppjjkksss ctr_defs fld_induct' set_natural's pre_set_defss =
    1.52 +fun mk_induct_tac ctxt ns mss ixsss ctr_defs fld_induct' set_natural's pre_set_defss =
    1.53    let
    1.54      val nn = length ns;
    1.55      val n = Integer.sum ns;
    1.56    in
    1.57      mk_induct_prelude_tac ctxt ctr_defs fld_induct' THEN
    1.58      EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's)
    1.59 -      pre_set_defss mss (unflat mss (1 upto n)) ppjjkksss)
    1.60 +      pre_set_defss mss (unflat mss (1 upto n)) ixsss)
    1.61    end;
    1.62  
    1.63  end;