src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML
author blanchet
Thu Aug 30 14:27:26 2012 +0200 (2012-08-30)
changeset 49029 f0ecfa9575a9
parent 49028 487427a02bee
child 49030 d0f4f113e43d
permissions -rw-r--r--
generate "disc_exhaust" property
     1 (*  Title:      HOL/Codatatype/Tools/bnf_sugar_tactics.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2012
     4 
     5 Tactics for sugar on top of a BNF.
     6 *)
     7 
     8 signature BNF_SUGAR_TACTICS =
     9 sig
    10   val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
    11   val mk_half_disc_disjoint_tac: int -> thm -> thm -> tactic
    12   val mk_nchotomy_tac: int -> thm -> tactic
    13   val mk_other_half_disc_disjoint_tac: thm -> tactic
    14 end;
    15 
    16 structure BNF_Sugar_Tactics : BNF_SUGAR_TACTICS =
    17 struct
    18 
    19 open BNF_Tactics
    20 open BNF_FP_Util
    21 
    22 fun mk_nchotomy_tac n exhaust =
    23   (rtac allI THEN' rtac exhaust THEN'
    24    EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1;
    25 
    26 fun mk_half_disc_disjoint_tac m disc_def disc'_thm =
    27   (dtac (disc_def RS iffD1) THEN'
    28    REPEAT_DETERM_N m o etac exE THEN'
    29    hyp_subst_tac THEN'
    30    rtac disc'_thm) 1;
    31 
    32 fun mk_other_half_disc_disjoint_tac half_thm =
    33   (etac @{thm contrapos_pn} THEN' etac half_thm) 1;
    34 
    35 fun mk_disc_exhaust_tac n exhaust discIs =
    36   (rtac exhaust THEN'
    37    EVERY' (map2 (fn k => fn discI =>
    38      dtac discI THEN' select_prem_tac n (etac @{thm meta_mp}) k THEN' atac) (1 upto n) discIs)) 1;
    39 
    40 end;