| author | blanchet |
| Tue, 04 Sep 2012 13:06:41 +0200 | |
| changeset 50138 | 263b0e330d8b |
| child 50140 | 5fc5211cf104 |
| permissions | -rw-r--r-- |
| blanchet@50138 | 1 |
(* Title: HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML |
| blanchet@50138 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
| blanchet@50138 | 3 |
Copyright 2012 |
| blanchet@50138 | 4 |
|
| blanchet@50138 | 5 |
Tactics for the LFP/GFP sugar. |
| blanchet@50138 | 6 |
*) |
| blanchet@50138 | 7 |
|
| blanchet@50138 | 8 |
signature BNF_FP_SUGAR_TACTICS = |
| blanchet@50138 | 9 |
sig |
| blanchet@50138 | 10 |
val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm |
| blanchet@50138 | 11 |
-> tactic |
| blanchet@50138 | 12 |
end; |
| blanchet@50138 | 13 |
|
| blanchet@50138 | 14 |
structure BNF_FP_Sugar_Tactics : BNF_FP_SUGAR_TACTICS = |
| blanchet@50138 | 15 |
struct |
| blanchet@50138 | 16 |
|
| blanchet@50138 | 17 |
open BNF_Util |
| blanchet@50138 | 18 |
|
| blanchet@50138 | 19 |
fun mk_fld_iff_unf_tac ctxt cTs cfld cunf fld_unf unf_fld = |
| blanchet@50138 | 20 |
(rtac iffI THEN' |
| blanchet@50138 | 21 |
EVERY' (map3 (fn cTs => fn cx => fn th => |
| blanchet@50138 | 22 |
dtac (Drule.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN' |
| blanchet@50138 | 23 |
SELECT_GOAL (Local_Defs.unfold_tac ctxt [th]) THEN' |
| blanchet@50138 | 24 |
atac) [rev cTs, cTs] [cunf, cfld] [unf_fld, fld_unf])) 1; |
| blanchet@50138 | 25 |
|
| blanchet@50138 | 26 |
end; |