1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Mon Sep 17 21:13:30 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Mon Sep 17 21:13:30 2012 +0200
     1.3 @@ -43,6 +43,52 @@
     1.4  
     1.5  val inst_spurious_fs_tac = PRIMITIVE o inst_spurious_fs;
     1.6  
     1.7 +fun mk_set_rhs set_lhs T =
     1.8 +  let
     1.9 +    val Type (_, Ts0) = domain_type (fastype_of set_lhs);
    1.10 +    val Type (_, Ts) = domain_type T;
    1.11 +  in
    1.12 +    Term.subst_atomic_types (Ts0 ~~ Ts) set_lhs
    1.13 +  end;
    1.14 +
    1.15 +val mk_fsts_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm fsts_def[abs_def]})));
    1.16 +val mk_snds_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm snds_def[abs_def]})));
    1.17 +val mk_setl_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm sum_setl_def[abs_def]})));
    1.18 +val mk_setr_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm sum_setr_def[abs_def]})));
    1.19 +
    1.20 +(* TODO: Put this in "Balanced_Tree" *)
    1.21 +fun balanced_tree_middle n = n div 2;
    1.22 +
    1.23 +val sum_prod_sel_defs =
    1.24 +  @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]};
    1.25 +
    1.26 +fun unfold_sum_prod_sets ctxt ms thm =
    1.27 +  let
    1.28 +    fun unf_prod 0 f = f
    1.29 +      | unf_prod 1 f = f
    1.30 +      | unf_prod m (t1 $ (t2 $ (t3 $ (t4 $ Const (_, T1) $ (t5 $ Const (_, T2) $ t6))))
    1.31 +          $ (t7 $ f $ g)) =
    1.32 +        t1 $ (t2 $ (t3 $ (t4 $ mk_fsts_rhs T1 $ (t5 $ mk_snds_rhs T2 $ t6))))
    1.33 +          $ (t7 $ f $ unf_prod (m - 1) g)
    1.34 +      | unf_prod _ f = f;
    1.35 +    fun unf_sum [m] f = unf_prod m f
    1.36 +      | unf_sum ms (t1 $ (t2 $ (t3 $ (t4 $ Const (_, T1) $ (t5 $ Const (_, T2) $ t6))))
    1.37 +          $ (t7 $ f $ g)) =
    1.38 +        let val (ms1, ms2) = chop (balanced_tree_middle (length ms)) ms in
    1.39 +          t1 $ (t2 $ (t3 $ (t4 $ mk_setl_rhs T1 $ (t5 $ mk_setr_rhs T2 $ t6))))
    1.40 +            $ (t7 $ unf_sum ms1 f $ unf_sum ms2 g)
    1.41 +        end
    1.42 +      | unf_sum _ f = f;
    1.43 +
    1.44 +    val P = prop_of thm;
    1.45 +    val P' = Logic.dest_equals P ||> unf_sum ms;
    1.46 +    val goal = Logic.mk_implies (P, Logic.mk_equals P');
    1.47 +  in
    1.48 +    Skip_Proof.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
    1.49 +      Local_Defs.unfold_tac ctxt sum_prod_sel_defs THEN atac 1)
    1.50 +    OF [thm]
    1.51 +  end;
    1.52 +
    1.53  fun mk_case_tac ctxt n k m case_def ctr_def unf_fld =
    1.54    Local_Defs.unfold_tac ctxt [case_def, ctr_def, unf_fld] THEN
    1.55    (rtac (mk_sum_casesN_balanced n k RS ssubst) THEN'
    1.56 @@ -88,14 +134,14 @@
    1.57    Local_Defs.unfold_tac ctxt @{thms id_def} THEN
    1.58    TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1);
    1.59  
    1.60 -(* TODO: Get rid of "auto_tac" (or at least use a naked context) *)
    1.61 +val maybe_singletonI_tac = atac ORELSE' rtac @{thm singletonI};
    1.62  
    1.63 -fun mk_induct_prem_prem_endgame_tac _ 0 = atac ORELSE' rtac @{thm singletonI}
    1.64 +fun mk_induct_prem_prem_endgame_tac _ 0 = maybe_singletonI_tac
    1.65    | mk_induct_prem_prem_endgame_tac ctxt qq =
    1.66      REPEAT_DETERM_N qq o
    1.67 -      (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
    1.68 -       etac @{thm induct_set_step}) THEN'
    1.69 -    atac ORELSE' SELECT_GOAL (auto_tac ctxt);
    1.70 +      (SELECT_GOAL (Local_Defs.unfold_tac ctxt
    1.71 +         @{thms trans[OF Union_iff bex_simps(6)] mem_compreh_eq_iff ex_mem_singleton}) THEN'
    1.72 +       eresolve_tac @{thms induct_set_step}) THEN' maybe_singletonI_tac;
    1.73  
    1.74  fun gen_UN_comprehI_tac UnI = REPEAT_DETERM o resolve_tac @{thms mem_UN_comprehI} THEN' rtac UnI;
    1.75  
    1.76 @@ -109,19 +155,12 @@
    1.77        image_def o_apply snd_conv snd_prod_fun sum.cases sup_bot_right fst_map_pair map_pair_simp
    1.78        sum_map.simps};
    1.79  
    1.80 -(* These rules interfere with the "set_natural'" properties of "sum" and "prod", so we explicitly
    1.81 -   delay them. *)
    1.82 -val induct_prem_prem_thms_delayed =
    1.83 -  @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]};
    1.84 -
    1.85  fun mk_induct_leverage_prem_prems_tac ctxt nn ppjjqqkks set_natural's pre_set_defs =
    1.86    EVERY' (maps (fn ((pp, jj), (qq, kk)) =>
    1.87      [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
    1.88       SELECT_GOAL (Local_Defs.unfold_tac ctxt
    1.89         (pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
    1.90 -     SELECT_GOAL (Local_Defs.unfold_tac ctxt
    1.91 -       (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)),
    1.92 -     gen_UnIN_tac pp jj THEN' mk_induct_prem_prem_endgame_tac ctxt qq]) (rev ppjjqqkks)) 1;
    1.93 +     gen_UnIN_tac pp jj, mk_induct_prem_prem_endgame_tac ctxt qq]) (rev ppjjqqkks)) 1;
    1.94  
    1.95  fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ppjjqqkks =
    1.96    let val r = length ppjjqqkks in
    1.97 @@ -137,10 +176,11 @@
    1.98    let
    1.99      val nn = length ns;
   1.100      val n = Integer.sum ns;
   1.101 +    val pre_set_defss' = map2 (map o unfold_sum_prod_sets ctxt) mss pre_set_defss;
   1.102    in
   1.103      Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN inst_spurious_fs_tac ctxt THEN
   1.104      EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's)
   1.105 -      pre_set_defss mss (unflat mss (1 upto n)) ppjjqqkksss)
   1.106 +      pre_set_defss' mss (unflat mss (1 upto n)) ppjjqqkksss)
   1.107    end;
   1.108  
   1.109  end;