1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 15 20:14:29 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 15 21:10:26 2012 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Jasmin Blanchette, TU Muenchen
     1.5      Copyright   2012
     1.6  
     1.7 -Tactics for the LFP/GFP sugar.
     1.8 +Tactics for datatype and codatatype sugar.
     1.9  *)
    1.10  
    1.11  signature BNF_FP_SUGAR_TACTICS =
    1.12 @@ -30,6 +30,9 @@
    1.13  val meta_mp = @{thm meta_mp};
    1.14  val meta_spec = @{thm meta_spec};
    1.15  
    1.16 +(* FIXME: why not in "Pure"? *)
    1.17 +fun prefer_tac i = defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1);
    1.18 +
    1.19  fun smash_spurious_fs lthy thm =
    1.20    let
    1.21      val fs =
    1.22 @@ -88,19 +91,14 @@
    1.23    Local_Defs.unfold_tac ctxt @{thms id_def} THEN
    1.24    TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1);
    1.25  
    1.26 -fun mk_induct_prelude_tac ctxt ctr_defs fld_induct' =
    1.27 -  Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN smash_spurious_fs_tac ctxt;
    1.28 +(* TODO: Get rid of "auto_tac" (or at least use a naked context) *)
    1.29  
    1.30 -fun mk_induct_prepare_prem_tac n m k =
    1.31 -  EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac,
    1.32 -    REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1;
    1.33 -
    1.34 -(* FIXME: why not in "Pure"? *)
    1.35 -fun prefer_tac i = defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1);
    1.36 -
    1.37 -fun mk_induct_prepare_prem_prems_tac r =
    1.38 -  REPEAT_DETERM_N r (rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2) THEN
    1.39 -  PRIMITIVE Raw_Simplifier.norm_hhf;
    1.40 +fun mk_induct_prem_prem_endgame_tac _ 0 = atac ORELSE' rtac @{thm singletonI}
    1.41 +  | mk_induct_prem_prem_endgame_tac ctxt qq =
    1.42 +    REPEAT_DETERM_N qq o
    1.43 +      (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
    1.44 +       etac @{thm induct_set_step}) THEN'
    1.45 +    atac ORELSE' SELECT_GOAL (auto_tac ctxt);
    1.46  
    1.47  val induct_prem_prem_thms =
    1.48    @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex UN_insert Un_assoc[symmetric] Un_empty_left
    1.49 @@ -112,38 +110,32 @@
    1.50  val induct_prem_prem_thms_delayed =
    1.51    @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]};
    1.52  
    1.53 -(* TODO: Get rid of "auto_tac" (or at least use a naked context) *)
    1.54 -fun mk_induct_prem_prem_endgame_tac _ 0 = atac ORELSE' rtac @{thm singletonI}
    1.55 -  | mk_induct_prem_prem_endgame_tac ctxt qq =
    1.56 -    REPEAT_DETERM_N qq o
    1.57 -      (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
    1.58 -       etac @{thm induct_set_step}) THEN'
    1.59 -    atac ORELSE' SELECT_GOAL (auto_tac ctxt);
    1.60 +fun mk_induct_leverage_prem_prems_tac ctxt nn ppjjqqkks set_natural's pre_set_defs =
    1.61 +  EVERY' (maps (fn ((pp, jj), (qq, kk)) =>
    1.62 +    [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
    1.63 +     SELECT_GOAL (Local_Defs.unfold_tac ctxt
    1.64 +       (pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
    1.65 +     SELECT_GOAL (Local_Defs.unfold_tac ctxt
    1.66 +       (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)),
    1.67 +     rtac (mk_UnIN pp jj) THEN' mk_induct_prem_prem_endgame_tac ctxt qq ORELSE'
    1.68 +       SELECT_GOAL (auto_tac ctxt)]) (rev ppjjqqkks)) 1;
    1.69  
    1.70 -fun mk_induct_discharge_prem_prems_tac ctxt nn ixs set_natural's pre_set_defs =
    1.71 -  EVERY' (maps (fn ((pp, jj), (qq, kk)) =>
    1.72 -      [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
    1.73 -       SELECT_GOAL (Local_Defs.unfold_tac ctxt
    1.74 -         (pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
    1.75 -       SELECT_GOAL (Local_Defs.unfold_tac ctxt
    1.76 -         (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)),
    1.77 -       rtac (mk_UnIN pp jj) THEN' mk_induct_prem_prem_endgame_tac ctxt qq ORELSE'
    1.78 -         SELECT_GOAL (auto_tac ctxt)])
    1.79 -    (rev ixs)) 1;
    1.80 +fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ppjjqqkks =
    1.81 +  EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac,
    1.82 +    REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN
    1.83 +  EVERY [REPEAT_DETERM_N (length ppjjqqkks)
    1.84 +      (rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2),
    1.85 +    PRIMITIVE Raw_Simplifier.norm_hhf, atac 1,
    1.86 +    mk_induct_leverage_prem_prems_tac ctxt nn ppjjqqkks set_natural's pre_set_defs];
    1.87  
    1.88 -fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ixs =
    1.89 -  EVERY [mk_induct_prepare_prem_tac n m k,
    1.90 -    mk_induct_prepare_prem_prems_tac (length ixs), atac 1,
    1.91 -    mk_induct_discharge_prem_prems_tac ctxt nn ixs set_natural's pre_set_defs];
    1.92 -
    1.93 -fun mk_induct_tac ctxt ns mss ixsss ctr_defs fld_induct' set_natural's pre_set_defss =
    1.94 +fun mk_induct_tac ctxt ns mss ppjjqqkksss ctr_defs fld_induct' set_natural's pre_set_defss =
    1.95    let
    1.96      val nn = length ns;
    1.97      val n = Integer.sum ns;
    1.98    in
    1.99 -    mk_induct_prelude_tac ctxt ctr_defs fld_induct' THEN
   1.100 +    Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN smash_spurious_fs_tac ctxt THEN
   1.101      EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's)
   1.102 -      pre_set_defss mss (unflat mss (1 upto n)) ixsss)
   1.103 +      pre_set_defss mss (unflat mss (1 upto n)) ppjjqqkksss)
   1.104    end;
   1.105  
   1.106  end;