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 @@ -13,6 +13,7 @@
1.4 -> tactic
1.5 val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic
1.6 val mk_inject_tac: Proof.context -> thm -> thm -> tactic
1.7 + val mk_iter_or_rec_tac: thm list -> thm list -> thm -> thm -> Proof.context -> tactic
1.8 end;
1.9
1.10 structure BNF_FP_Sugar_Tactics : BNF_FP_SUGAR_TACTICS =
1.11 @@ -48,4 +49,11 @@
1.12 Local_Defs.unfold_tac ctxt [ctr_def] THEN rtac (fld_inject RS ssubst) 1 THEN
1.13 Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
1.14
1.15 +val iter_or_rec_thms =
1.16 + @{thms sum_map.simps sum.simps(5,6) convol_def case_unit map_pair_def split_conv id_def};
1.17 +
1.18 +fun mk_iter_or_rec_tac iter_or_rec_defs fld_iter_or_recs ctr_def bnf_map_def ctxt =
1.19 + Local_Defs.unfold_tac ctxt (ctr_def :: bnf_map_def :: iter_or_rec_defs @ fld_iter_or_recs) THEN
1.20 + Local_Defs.unfold_tac ctxt iter_or_rec_thms THEN rtac refl 1;
1.21 +
1.22 end;