1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 12:09:27 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 12:09:27 2012 +0200
     1.3 @@ -10,8 +10,8 @@
     1.4    val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic
     1.5    val mk_coiter_like_tac: thm list -> thm list -> thm -> thm -> thm -> Proof.context -> tactic
     1.6    val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
     1.7 -  val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm
     1.8 -    -> tactic
     1.9 +  val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
    1.10 +    tactic
    1.11    val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic
    1.12    val mk_induct_tac: Proof.context -> int list -> int list list -> int list list -> thm list ->
    1.13      thm -> thm list list -> thm list -> tactic
    1.14 @@ -95,45 +95,49 @@
    1.15    EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac,
    1.16      REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1;
    1.17  
    1.18 -fun mk_induct_prepare_prem_prems_tac _ _ 0 = all_tac
    1.19 -  | mk_induct_prepare_prem_prems_tac nn kk r =
    1.20 -    REPEAT_DETERM_N r (rotate_tac (~1 + kk - nn) 1 THEN dtac meta_mp 1 THEN
    1.21 +fun mk_induct_prepare_prem_prems_tac 0 = all_tac
    1.22 +  | mk_induct_prepare_prem_prems_tac r =
    1.23 +    REPEAT_DETERM_N r ((rotate_tac ~1) 1 THEN dtac meta_mp 1 THEN
    1.24        defer_tac 2 THEN PRIMITIVE (Thm.permute_prems 0 ~1) THEN rotate_tac 1 1) THEN
    1.25      PRIMITIVE Raw_Simplifier.norm_hhf;
    1.26  
    1.27  val induct_prem_prem_thms =
    1.28    @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex UN_insert Un_assoc[symmetric] Un_empty_left
    1.29 -      Un_empty_right Union_Un_distrib collect_def[abs_def] fst_conv fsts_def[abs_def] image_def
    1.30 -      map_pair_simp o_apply snd_conv snds_def[abs_def] sum.cases sum_map.simps sum_setl_def[abs_def]
    1.31 -      sum_setr_def[abs_def] sup_bot_right};
    1.32 +      Un_empty_right Union_Un_distrib collect_def[abs_def] fst_conv image_def o_apply snd_conv
    1.33 +      snd_prod_fun sum.cases sup_bot_right fst_map_pair map_pair_simp sum_map.simps};
    1.34  
    1.35 +(* These rules interfere with the "set_natural'" properties of "sum" and "prod", so we explicitly
    1.36 +   delay them. *)
    1.37 +val induct_prem_prem_thms_delayed =
    1.38 +  @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]};
    1.39 +
    1.40 +(* TODO: Get rid of the "blast_tac" *)
    1.41  fun mk_induct_discharge_prem_prems_tac ctxt r pre_set_defs set_natural's =
    1.42    EVERY' (maps (fn i =>
    1.43      [dtac meta_spec, rotate_tac ~1, etac meta_mp,
    1.44 +     SELECT_GOAL (Local_Defs.unfold_tac ctxt pre_set_defs),
    1.45 +     SELECT_GOAL (Local_Defs.unfold_tac ctxt (set_natural's @ induct_prem_prem_thms)),
    1.46       SELECT_GOAL (Local_Defs.unfold_tac ctxt
    1.47 -       (set_natural's @ pre_set_defs @ induct_prem_prem_thms)),
    1.48 -     rtac (mk_UnIN r i),
    1.49 +       (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)),
    1.50 +     TRY o rtac (mk_UnIN r i), (* FIXME: crude hack, doesn't work in the general case *)
    1.51       atac ORELSE'
    1.52       rtac @{thm singletonI} ORELSE'
    1.53 -     (REPEAT_DETERM o (atac ORELSE'
    1.54 -        SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
    1.55 -        etac @{thm induct_set_step}))]) (r downto 1)) 1;
    1.56 +     (REPEAT_DETERM o (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
    1.57 +          etac @{thm induct_set_step}) THEN'
    1.58 +        (atac ORELSE' blast_tac ctxt))]) (r downto 1)) 1;
    1.59  
    1.60 -fun mk_induct_discharge_prem_tac ctxt nn kk n m k r pre_set_defs set_natural's =
    1.61 +fun mk_induct_discharge_prem_tac ctxt n m k r pre_set_defs set_natural's =
    1.62    EVERY [mk_induct_prepare_prem_tac n m k,
    1.63 -    mk_induct_prepare_prem_prems_tac nn kk r, atac 1,
    1.64 +    mk_induct_prepare_prem_prems_tac r, atac 1,
    1.65      mk_induct_discharge_prem_prems_tac ctxt r pre_set_defs set_natural's];
    1.66  
    1.67  fun mk_induct_tac ctxt ns mss rss ctr_defs fld_induct' pre_set_defss set_natural's =
    1.68 -  let
    1.69 -    val nn = length ns;
    1.70 -    val n = Integer.sum ns;
    1.71 -  in
    1.72 +  let val n = Integer.sum ns in
    1.73      mk_induct_prelude_tac ctxt ctr_defs fld_induct' THEN
    1.74 -    EVERY (map5 (fn kk => fn pre_set_defs =>
    1.75 +    EVERY (map4 (fn pre_set_defs =>
    1.76          EVERY ooo map3 (fn m => fn k => fn r =>
    1.77 -            mk_induct_discharge_prem_tac ctxt nn kk n m k r pre_set_defs set_natural's))
    1.78 -      (1 upto nn) pre_set_defss mss (unflat mss (1 upto Integer.sum ns)) rss)
    1.79 +            mk_induct_discharge_prem_tac ctxt n m k r pre_set_defs set_natural's))
    1.80 +      pre_set_defss mss (unflat mss (1 upto n)) rss)
    1.81    end;
    1.82  
    1.83  end;