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