author | blanchet |
Wed, 05 Sep 2012 11:08:18 +0200 | |
changeset 50164 | 166f19b4677b |
parent 50162 | 0da8120bd2aa |
child 50175 | 056d6010b6d2 |
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@50145 | 10 |
val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic |
blanchet@50140 | 11 |
val mk_exhaust_tac: Proof.context -> int -> int list -> thm list -> thm -> thm -> tactic |
blanchet@50138 | 12 |
val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm |
blanchet@50138 | 13 |
-> tactic |
blanchet@50142 | 14 |
val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic |
blanchet@50141 | 15 |
val mk_inject_tac: Proof.context -> thm -> thm -> tactic |
blanchet@50138 | 16 |
end; |
blanchet@50138 | 17 |
|
blanchet@50138 | 18 |
structure BNF_FP_Sugar_Tactics : BNF_FP_SUGAR_TACTICS = |
blanchet@50138 | 19 |
struct |
blanchet@50138 | 20 |
|
blanchet@50140 | 21 |
open BNF_Tactics |
blanchet@50138 | 22 |
open BNF_Util |
blanchet@50138 | 23 |
|
blanchet@50145 | 24 |
fun mk_case_tac ctxt n k m case_def ctr_def unf_fld = |
blanchet@50145 | 25 |
Local_Defs.unfold_tac ctxt [case_def, ctr_def, unf_fld] THEN |
blanchet@50145 | 26 |
(rtac (BNF_FP_Util.mk_sum_casesN n k RS ssubst) THEN' |
blanchet@50145 | 27 |
REPEAT_DETERM_N (Int.max (0, m - 1)) o rtac (@{thm split} RS ssubst) THEN' |
blanchet@50145 | 28 |
rtac refl) 1; |
blanchet@50145 | 29 |
|
blanchet@50140 | 30 |
fun mk_exhaust_tac ctxt n ms ctr_defs fld_iff_unf sumEN' = |
blanchet@50150 | 31 |
Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN rtac sumEN' 1 THEN |
blanchet@50140 | 32 |
Local_Defs.unfold_tac ctxt @{thms all_prod_eq} THEN |
blanchet@50162 | 33 |
EVERY' (map2 (fn k => fn m => |
blanchet@50164 | 34 |
select_prem_tac k (REPEAT_DETERM_N m o dtac @{thm meta_spec} THEN' rotate_tac ~1 THEN' |
blanchet@50162 | 35 |
etac @{thm meta_mp}) k THEN' atac) (1 upto n) ms) 1; |
blanchet@50140 | 36 |
|
blanchet@50138 | 37 |
fun mk_fld_iff_unf_tac ctxt cTs cfld cunf fld_unf unf_fld = |
blanchet@50138 | 38 |
(rtac iffI THEN' |
blanchet@50138 | 39 |
EVERY' (map3 (fn cTs => fn cx => fn th => |
blanchet@50138 | 40 |
dtac (Drule.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN' |
blanchet@50138 | 41 |
SELECT_GOAL (Local_Defs.unfold_tac ctxt [th]) THEN' |
blanchet@50138 | 42 |
atac) [rev cTs, cTs] [cunf, cfld] [unf_fld, fld_unf])) 1; |
blanchet@50138 | 43 |
|
blanchet@50142 | 44 |
fun mk_half_distinct_tac ctxt fld_inject ctr_defs = |
blanchet@50142 | 45 |
Local_Defs.unfold_tac ctxt (fld_inject :: @{thms sum.inject} @ ctr_defs) THEN |
blanchet@50142 | 46 |
rtac @{thm sum.distinct(1)} 1; |
blanchet@50142 | 47 |
|
blanchet@50141 | 48 |
fun mk_inject_tac ctxt ctr_def fld_inject = |
blanchet@50150 | 49 |
Local_Defs.unfold_tac ctxt [ctr_def] THEN rtac (fld_inject RS ssubst) 1 THEN |
blanchet@50150 | 50 |
Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1; |
blanchet@50141 | 51 |
|
blanchet@50138 | 52 |
end; |