src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML
author blanchet
Tue Sep 11 18:39:47 2012 +0200 (2012-09-11)
changeset 49286 dde4967c9233
parent 49213 975ccb0130cb
child 49463 83ac281bcdc2
permissions -rw-r--r--
added "defaults" option
     1 (*  Title:      HOL/Codatatype/Tools/bnf_wrap_tactics.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2012
     4 
     5 Tactics for wrapping datatypes.
     6 *)
     7 
     8 signature BNF_WRAP_TACTICS =
     9 sig
    10   val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
    11   val mk_case_cong_tac: thm -> thm list -> tactic
    12   val mk_case_eq_tac: Proof.context -> int -> thm -> thm list -> thm list list -> thm list list ->
    13     tactic
    14   val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
    15   val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
    16   val mk_half_disc_exclude_tac: int -> thm -> thm -> tactic
    17   val mk_nchotomy_tac: int -> thm -> tactic
    18   val mk_other_half_disc_exclude_tac: thm -> tactic
    19   val mk_split_tac: thm -> thm list -> thm list list -> thm list list list -> tactic
    20   val mk_split_asm_tac: Proof.context -> thm -> tactic
    21   val mk_unique_disc_def_tac: int -> thm -> tactic
    22 end;
    23 
    24 structure BNF_Wrap_Tactics : BNF_WRAP_TACTICS =
    25 struct
    26 
    27 open BNF_Util
    28 open BNF_Tactics
    29 
    30 fun if_P_or_not_P_OF pos thm = thm RS (if pos then @{thm if_P} else @{thm if_not_P});
    31 
    32 fun mk_nchotomy_tac n exhaust =
    33   (rtac allI THEN' rtac exhaust THEN'
    34    EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1;
    35 
    36 fun mk_unique_disc_def_tac m exhaust' =
    37   EVERY' [rtac iffI, rtac exhaust', REPEAT_DETERM_N m o rtac exI, atac, rtac refl] 1;
    38 
    39 fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct exhaust' =
    40   EVERY' ([subst_tac ctxt [other_disc_def], rtac @{thm iffI_np}, REPEAT_DETERM o etac exE,
    41     hyp_subst_tac, SELECT_GOAL (Local_Defs.unfold_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
    42     rtac distinct, rtac exhaust'] @
    43     (([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac])
    44      |> k = 1 ? swap |> op @)) 1;
    45 
    46 fun mk_half_disc_exclude_tac m discD disc'_thm =
    47   (dtac discD THEN'
    48    REPEAT_DETERM_N m o etac exE THEN'
    49    hyp_subst_tac THEN'
    50    rtac disc'_thm) 1;
    51 
    52 fun mk_other_half_disc_exclude_tac half_thm =
    53   (etac @{thm contrapos_pn} THEN' etac half_thm) 1;
    54 
    55 fun mk_disc_exhaust_tac n exhaust discIs =
    56   (rtac exhaust THEN'
    57    EVERY' (map2 (fn k => fn discI =>
    58      dtac discI THEN' select_prem_tac n (etac @{thm meta_mp}) k THEN' atac) (1 upto n) discIs)) 1;
    59 
    60 fun mk_collapse_tac ctxt m discD sel_thms =
    61   (dtac discD THEN'
    62    (if m = 0 then
    63       atac
    64     else
    65       REPEAT_DETERM_N m o etac exE THEN'
    66       hyp_subst_tac THEN'
    67       SELECT_GOAL (Local_Defs.unfold_tac ctxt sel_thms) THEN'
    68       rtac refl)) 1;
    69 
    70 fun mk_case_eq_tac ctxt n exhaust' case_thms disc_thmss' sel_thmss =
    71   (rtac exhaust' THEN'
    72    EVERY' (map3 (fn case_thm => fn if_disc_thms => fn sel_thms =>
    73        EVERY' [hyp_subst_tac, SELECT_GOAL (Local_Defs.unfold_tac ctxt (if_disc_thms @ sel_thms)),
    74          rtac case_thm])
    75      case_thms (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) disc_thmss') sel_thmss)) 1;
    76 
    77 fun mk_case_cong_tac exhaust' case_thms =
    78   (rtac exhaust' THEN'
    79    EVERY' (maps (fn case_thm => [dtac sym, asm_simp_tac (ss_only [case_thm])]) case_thms)) 1;
    80 
    81 val naked_ctxt = Proof_Context.init_global @{theory HOL};
    82 
    83 fun mk_split_tac exhaust' case_thms injectss distinctsss =
    84   rtac exhaust' 1 THEN
    85   ALLGOALS (fn k => (hyp_subst_tac THEN'
    86      simp_tac (ss_only (@{thms simp_thms} @ case_thms @ nth injectss (k - 1) @
    87        flat (nth distinctsss (k - 1))))) k) THEN
    88   ALLGOALS (blast_tac naked_ctxt);
    89 
    90 val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};
    91 
    92 fun mk_split_asm_tac ctxt split =
    93   rtac (split RS trans) 1 THEN Local_Defs.unfold_tac ctxt split_asm_thms THEN rtac refl 1;
    94 
    95 end;