1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
     1.3 @@ -8,6 +8,7 @@
     1.4  signature BNF_FP_SUGAR_TACTICS =
     1.5  sig
     1.6    val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic
     1.7 +  val mk_coiter_like_tac: thm list -> thm -> thm -> thm -> Proof.context -> tactic
     1.8    val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
     1.9    val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm
    1.10      -> tactic
    1.11 @@ -56,4 +57,14 @@
    1.12    Local_Defs.unfold_tac ctxt (ctr_def :: pre_map_def :: iter_like_defs @ fld_iter_likes) THEN
    1.13    Local_Defs.unfold_tac ctxt iter_like_thms THEN rtac refl 1;
    1.14  
    1.15 +val coiter_like_ss = ss_only @{thms if_True if_False};
    1.16 +val coiter_like_thms = @{thms sum_map.simps map_pair_def id_def prod.cases};
    1.17 +
    1.18 +fun mk_coiter_like_tac coiter_like_defs fld_unf_coiter_like pre_map_def ctr_def ctxt =
    1.19 +  Local_Defs.unfold_tac ctxt (ctr_def :: coiter_like_defs) THEN
    1.20 +  subst_tac ctxt [fld_unf_coiter_like] 1 THEN
    1.21 +  asm_simp_tac coiter_like_ss 1 THEN
    1.22 +  Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms) THEN
    1.23 +  rtac refl 1;
    1.24 +
    1.25  end;