src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
author blanchet
Sat Sep 15 21:10:26 2012 +0200 (2012-09-15)
changeset 49389 da621dc65146
parent 49385 83b867707af2
child 49391 3a96797fd53e
permissions -rw-r--r--
tuning
blanchet@49123
     1
(*  Title:      HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
blanchet@49123
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@49123
     3
    Copyright   2012
blanchet@49123
     4
blanchet@49389
     5
Tactics for datatype and codatatype sugar.
blanchet@49123
     6
*)
blanchet@49123
     7
blanchet@49123
     8
signature BNF_FP_SUGAR_TACTICS =
blanchet@49123
     9
sig
blanchet@49130
    10
  val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic
blanchet@49226
    11
  val mk_coiter_like_tac: thm list -> thm list -> thm -> thm -> thm -> Proof.context -> tactic
blanchet@49161
    12
  val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
blanchet@49372
    13
  val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
blanchet@49372
    14
    tactic
blanchet@49127
    15
  val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic
blanchet@49376
    16
  val mk_induct_tac: Proof.context -> int list -> int list list ->
blanchet@49378
    17
    ((int * int) * (int * int)) list list list -> thm list -> thm -> thm list -> thm list list ->
blanchet@49378
    18
    tactic
blanchet@49126
    19
  val mk_inject_tac: Proof.context -> thm -> thm -> tactic
blanchet@49226
    20
  val mk_iter_like_tac: thm list -> thm list -> thm list -> thm -> thm -> Proof.context -> tactic
blanchet@49123
    21
end;
blanchet@49123
    22
blanchet@49123
    23
structure BNF_FP_Sugar_Tactics : BNF_FP_SUGAR_TACTICS =
blanchet@49123
    24
struct
blanchet@49123
    25
blanchet@49125
    26
open BNF_Tactics
blanchet@49123
    27
open BNF_Util
blanchet@49264
    28
open BNF_FP_Util
blanchet@49123
    29
blanchet@49368
    30
val meta_mp = @{thm meta_mp};
blanchet@49368
    31
val meta_spec = @{thm meta_spec};
blanchet@49368
    32
blanchet@49389
    33
(* FIXME: why not in "Pure"? *)
blanchet@49389
    34
fun prefer_tac i = defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1);
blanchet@49389
    35
blanchet@49370
    36
fun smash_spurious_fs lthy thm =
blanchet@49368
    37
  let
blanchet@49384
    38
    val fs =
blanchet@49368
    39
      Term.add_vars (prop_of thm) []
blanchet@49368
    40
      |> filter (fn (_, Type (@{type_name fun}, [_, T'])) => T' <> HOLogic.boolT | _ => false);
blanchet@49384
    41
    val cfs =
blanchet@49384
    42
      map (fn f as (_, T) => (certify lthy (Var f), certify lthy (id_abs (domain_type T)))) fs;
blanchet@49368
    43
  in
blanchet@49384
    44
    Drule.cterm_instantiate cfs thm
blanchet@49368
    45
  end;
blanchet@49368
    46
blanchet@49370
    47
val smash_spurious_fs_tac = PRIMITIVE o smash_spurious_fs;
blanchet@49368
    48
blanchet@49130
    49
fun mk_case_tac ctxt n k m case_def ctr_def unf_fld =
blanchet@49130
    50
  Local_Defs.unfold_tac ctxt [case_def, ctr_def, unf_fld] THEN
blanchet@49264
    51
  (rtac (mk_sum_casesN_balanced n k RS ssubst) THEN'
blanchet@49130
    52
   REPEAT_DETERM_N (Int.max (0, m - 1)) o rtac (@{thm split} RS ssubst) THEN'
blanchet@49130
    53
   rtac refl) 1;
blanchet@49130
    54
blanchet@49161
    55
fun mk_exhaust_tac ctxt n ctr_defs fld_iff_unf sumEN' =
blanchet@49263
    56
  Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN rtac sumEN' 1 THEN
blanchet@49125
    57
  Local_Defs.unfold_tac ctxt @{thms all_prod_eq} THEN
blanchet@49368
    58
  EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k, REPEAT_DETERM o dtac meta_spec,
blanchet@49368
    59
    etac meta_mp, atac]) (1 upto n)) 1;
blanchet@49125
    60
blanchet@49123
    61
fun mk_fld_iff_unf_tac ctxt cTs cfld cunf fld_unf unf_fld =
blanchet@49123
    62
  (rtac iffI THEN'
blanchet@49123
    63
   EVERY' (map3 (fn cTs => fn cx => fn th =>
blanchet@49123
    64
     dtac (Drule.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN'
blanchet@49123
    65
     SELECT_GOAL (Local_Defs.unfold_tac ctxt [th]) THEN'
blanchet@49123
    66
     atac) [rev cTs, cTs] [cunf, cfld] [unf_fld, fld_unf])) 1;
blanchet@49123
    67
blanchet@49127
    68
fun mk_half_distinct_tac ctxt fld_inject ctr_defs =
blanchet@49127
    69
  Local_Defs.unfold_tac ctxt (fld_inject :: @{thms sum.inject} @ ctr_defs) THEN
blanchet@49127
    70
  rtac @{thm sum.distinct(1)} 1;
blanchet@49127
    71
blanchet@49126
    72
fun mk_inject_tac ctxt ctr_def fld_inject =
blanchet@49135
    73
  Local_Defs.unfold_tac ctxt [ctr_def] THEN rtac (fld_inject RS ssubst) 1 THEN
blanchet@49135
    74
  Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
blanchet@49126
    75
blanchet@49211
    76
val iter_like_thms =
blanchet@49233
    77
  @{thms case_unit comp_def convol_def id_apply map_pair_def sum.simps(5,6) sum_map.simps
blanchet@49233
    78
      split_conv};
blanchet@49205
    79
blanchet@49229
    80
fun mk_iter_like_tac pre_map_defs map_ids iter_like_defs fld_iter_like ctr_def ctxt =
blanchet@49229
    81
  Local_Defs.unfold_tac ctxt (ctr_def :: fld_iter_like :: iter_like_defs @ pre_map_defs @ map_ids @
blanchet@49232
    82
    iter_like_thms) THEN Local_Defs.unfold_tac ctxt @{thms id_def} THEN rtac refl 1;
blanchet@49205
    83
blanchet@49213
    84
val coiter_like_ss = ss_only @{thms if_True if_False};
blanchet@49276
    85
val coiter_like_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases};
blanchet@49213
    86
blanchet@49229
    87
fun mk_coiter_like_tac coiter_like_defs map_ids fld_unf_coiter_like pre_map_def ctr_def ctxt =
blanchet@49213
    88
  Local_Defs.unfold_tac ctxt (ctr_def :: coiter_like_defs) THEN
blanchet@49226
    89
  subst_tac ctxt [fld_unf_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN
blanchet@49232
    90
  Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN
blanchet@49235
    91
  Local_Defs.unfold_tac ctxt @{thms id_def} THEN
blanchet@49362
    92
  TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1);
blanchet@49213
    93
blanchet@49389
    94
(* TODO: Get rid of "auto_tac" (or at least use a naked context) *)
blanchet@49368
    95
blanchet@49389
    96
fun mk_induct_prem_prem_endgame_tac _ 0 = atac ORELSE' rtac @{thm singletonI}
blanchet@49389
    97
  | mk_induct_prem_prem_endgame_tac ctxt qq =
blanchet@49389
    98
    REPEAT_DETERM_N qq o
blanchet@49389
    99
      (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
blanchet@49389
   100
       etac @{thm induct_set_step}) THEN'
blanchet@49389
   101
    atac ORELSE' SELECT_GOAL (auto_tac ctxt);
blanchet@49368
   102
blanchet@49368
   103
val induct_prem_prem_thms =
blanchet@49368
   104
  @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex UN_insert Un_assoc[symmetric] Un_empty_left
blanchet@49372
   105
      Un_empty_right Union_Un_distrib collect_def[abs_def] fst_conv image_def o_apply snd_conv
blanchet@49372
   106
      snd_prod_fun sum.cases sup_bot_right fst_map_pair map_pair_simp sum_map.simps};
blanchet@49368
   107
blanchet@49372
   108
(* These rules interfere with the "set_natural'" properties of "sum" and "prod", so we explicitly
blanchet@49372
   109
   delay them. *)
blanchet@49372
   110
val induct_prem_prem_thms_delayed =
blanchet@49372
   111
  @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]};
blanchet@49372
   112
blanchet@49389
   113
fun mk_induct_leverage_prem_prems_tac ctxt nn ppjjqqkks set_natural's pre_set_defs =
blanchet@49378
   114
  EVERY' (maps (fn ((pp, jj), (qq, kk)) =>
blanchet@49389
   115
    [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
blanchet@49389
   116
     SELECT_GOAL (Local_Defs.unfold_tac ctxt
blanchet@49389
   117
       (pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
blanchet@49389
   118
     SELECT_GOAL (Local_Defs.unfold_tac ctxt
blanchet@49389
   119
       (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)),
blanchet@49389
   120
     rtac (mk_UnIN pp jj) THEN' mk_induct_prem_prem_endgame_tac ctxt qq ORELSE'
blanchet@49389
   121
       SELECT_GOAL (auto_tac ctxt)]) (rev ppjjqqkks)) 1;
blanchet@49368
   122
blanchet@49389
   123
fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ppjjqqkks =
blanchet@49389
   124
  EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac,
blanchet@49389
   125
    REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN
blanchet@49389
   126
  EVERY [REPEAT_DETERM_N (length ppjjqqkks)
blanchet@49389
   127
      (rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2),
blanchet@49389
   128
    PRIMITIVE Raw_Simplifier.norm_hhf, atac 1,
blanchet@49389
   129
    mk_induct_leverage_prem_prems_tac ctxt nn ppjjqqkks set_natural's pre_set_defs];
blanchet@49368
   130
blanchet@49389
   131
fun mk_induct_tac ctxt ns mss ppjjqqkksss ctr_defs fld_induct' set_natural's pre_set_defss =
blanchet@49376
   132
  let
blanchet@49376
   133
    val nn = length ns;
blanchet@49376
   134
    val n = Integer.sum ns;
blanchet@49376
   135
  in
blanchet@49389
   136
    Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN smash_spurious_fs_tac ctxt THEN
blanchet@49376
   137
    EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's)
blanchet@49389
   138
      pre_set_defss mss (unflat mss (1 upto n)) ppjjqqkksss)
blanchet@49368
   139
  end;
blanchet@49368
   140
blanchet@49123
   141
end;