1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Tue Sep 04 13:06:41 2012 +0200
1.3 @@ -0,0 +1,26 @@
1.4 +(* Title: HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
1.5 + Author: Jasmin Blanchette, TU Muenchen
1.6 + Copyright 2012
1.7 +
1.8 +Tactics for the LFP/GFP sugar.
1.9 +*)
1.10 +
1.11 +signature BNF_FP_SUGAR_TACTICS =
1.12 +sig
1.13 + val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm
1.14 + -> tactic
1.15 +end;
1.16 +
1.17 +structure BNF_FP_Sugar_Tactics : BNF_FP_SUGAR_TACTICS =
1.18 +struct
1.19 +
1.20 +open BNF_Util
1.21 +
1.22 +fun mk_fld_iff_unf_tac ctxt cTs cfld cunf fld_unf unf_fld =
1.23 + (rtac iffI THEN'
1.24 + EVERY' (map3 (fn cTs => fn cx => fn th =>
1.25 + dtac (Drule.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN'
1.26 + SELECT_GOAL (Local_Defs.unfold_tac ctxt [th]) THEN'
1.27 + atac) [rev cTs, cTs] [cunf, cfld] [unf_fld, fld_unf])) 1;
1.28 +
1.29 +end;