src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML
author blanchet
Tue Oct 01 14:05:25 2013 +0200 (2013-10-01)
changeset 54006 9fe1bd54d437
parent 53920 c6de7f20c845
permissions -rw-r--r--
renamed theory file
blanchet@51797
     1
(*  Title:      HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML
blanchet@49020
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@49020
     3
    Copyright   2012
blanchet@49020
     4
blanchet@51797
     5
Tactics for wrapping existing freely generated type's constructors.
blanchet@49020
     6
*)
blanchet@49020
     7
blanchet@54006
     8
signature CTR_SUGAR_TACTICS =
blanchet@49020
     9
sig
blanchet@49148
    10
  val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
blanchet@52968
    11
  val mk_case_tac: Proof.context -> int -> int -> thm -> thm list -> thm list list -> tactic
wenzelm@51717
    12
  val mk_case_cong_tac: Proof.context -> thm -> thm list -> tactic
blanchet@53857
    13
  val mk_case_conv_if_tac: Proof.context -> int -> thm -> thm list -> thm list list ->
blanchet@53857
    14
    thm list list -> tactic
blanchet@49118
    15
  val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
blanchet@49029
    16
  val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
wenzelm@51717
    17
  val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list ->
wenzelm@51717
    18
    thm list list list -> thm list list list -> tactic
wenzelm@51798
    19
  val mk_half_disc_exclude_tac: Proof.context -> int -> thm -> thm -> tactic
blanchet@49020
    20
  val mk_nchotomy_tac: int -> thm -> tactic
blanchet@49122
    21
  val mk_other_half_disc_exclude_tac: thm -> tactic
blanchet@53916
    22
  val mk_sel_exhaust_tac: int -> thm -> thm list -> tactic
blanchet@53917
    23
  val mk_split_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> thm list
blanchet@53917
    24
    list list -> tactic
blanchet@49044
    25
  val mk_split_asm_tac: Proof.context -> thm -> tactic
blanchet@49137
    26
  val mk_unique_disc_def_tac: int -> thm -> tactic
blanchet@49020
    27
end;
blanchet@49020
    28
blanchet@54006
    29
structure Ctr_Sugar_Tactics : CTR_SUGAR_TACTICS =
blanchet@49020
    30
struct
blanchet@49020
    31
blanchet@49050
    32
open BNF_Util
blanchet@49029
    33
open BNF_Tactics
blanchet@49020
    34
blanchet@49486
    35
val meta_mp = @{thm meta_mp};
blanchet@49486
    36
blanchet@49212
    37
fun if_P_or_not_P_OF pos thm = thm RS (if pos then @{thm if_P} else @{thm if_not_P});
blanchet@49031
    38
blanchet@49020
    39
fun mk_nchotomy_tac n exhaust =
blanchet@52325
    40
  HEADGOAL (rtac allI THEN' rtac exhaust THEN'
blanchet@52966
    41
   EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n)));
blanchet@49020
    42
blanchet@49486
    43
fun mk_unique_disc_def_tac m uexhaust =
blanchet@52325
    44
  HEADGOAL (EVERY' [rtac iffI, rtac uexhaust, REPEAT_DETERM_N m o rtac exI, atac, rtac refl]);
blanchet@49137
    45
blanchet@49486
    46
fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust =
blanchet@52325
    47
  HEADGOAL (EVERY' ([rtac (other_disc_def RS @{thm arg_cong[of _ _ Not]} RS trans),
traytel@49630
    48
    rtac @{thm iffI_np}, REPEAT_DETERM o etac exE,
wenzelm@51798
    49
    hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
blanchet@49486
    50
    rtac distinct, rtac uexhaust] @
blanchet@49174
    51
    (([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac])
blanchet@52325
    52
     |> k = 1 ? swap |> op @)));
blanchet@49116
    53
wenzelm@51798
    54
fun mk_half_disc_exclude_tac ctxt m discD disc' =
blanchet@52325
    55
  HEADGOAL (dtac discD THEN' REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN'
blanchet@52325
    56
    rtac disc');
blanchet@49028
    57
blanchet@52325
    58
fun mk_other_half_disc_exclude_tac half = HEADGOAL (etac @{thm contrapos_pn} THEN' etac half);
blanchet@49028
    59
blanchet@53916
    60
fun mk_disc_or_sel_exhaust_tac n exhaust destIs =
blanchet@52325
    61
  HEADGOAL (rtac exhaust THEN'
blanchet@53916
    62
    EVERY' (map2 (fn k => fn destI => dtac destI THEN'
blanchet@53916
    63
      select_prem_tac n (etac meta_mp) k THEN' atac) (1 upto n) destIs));
blanchet@53916
    64
blanchet@53916
    65
val mk_disc_exhaust_tac = mk_disc_or_sel_exhaust_tac;
blanchet@53916
    66
blanchet@53916
    67
fun mk_sel_exhaust_tac n disc_exhaust collapses =
blanchet@53920
    68
  mk_disc_or_sel_exhaust_tac n disc_exhaust collapses ORELSE
blanchet@53920
    69
  HEADGOAL (etac meta_mp THEN' resolve_tac collapses);
blanchet@49029
    70
blanchet@49484
    71
fun mk_collapse_tac ctxt m discD sels =
blanchet@52325
    72
  HEADGOAL (dtac discD THEN'
blanchet@52325
    73
    (if m = 0 then
blanchet@52325
    74
       atac
blanchet@52325
    75
     else
blanchet@52325
    76
       REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN'
blanchet@52325
    77
       SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl));
blanchet@49030
    78
blanchet@51742
    79
fun mk_expand_tac ctxt n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss
blanchet@51742
    80
    disc_excludesss' =
blanchet@49486
    81
  if ms = [0] then
blanchet@52325
    82
    HEADGOAL (rtac (@{thm trans_sym} OF (replicate 2 (the_single uncollapses))) THEN'
blanchet@52325
    83
      TRY o EVERY' [rtac udisc_exhaust, atac, rtac vdisc_exhaust, atac])
blanchet@49486
    84
  else
blanchet@51742
    85
    let val ks = 1 upto n in
blanchet@52325
    86
      HEADGOAL (rtac udisc_exhaust THEN'
blanchet@52325
    87
        EVERY' (map5 (fn k => fn m => fn disc_excludess => fn disc_excludess' =>
blanchet@52325
    88
            fn uuncollapse =>
blanchet@52325
    89
          EVERY' [rtac (uuncollapse RS trans) THEN' TRY o atac,
blanchet@52325
    90
            rtac sym, rtac vdisc_exhaust,
blanchet@52325
    91
            EVERY' (map4 (fn k' => fn disc_excludes => fn disc_excludes' => fn vuncollapse =>
blanchet@52325
    92
              EVERY'
blanchet@52325
    93
                (if k' = k then
blanchet@52325
    94
                   [rtac (vuncollapse RS trans), TRY o atac] @
blanchet@52325
    95
                   (if m = 0 then
blanchet@52325
    96
                      [rtac refl]
blanchet@52325
    97
                    else
blanchet@52325
    98
                      [if n = 1 then K all_tac else EVERY' [dtac meta_mp, atac, dtac meta_mp, atac],
blanchet@52325
    99
                       REPEAT_DETERM_N (Int.max (0, m - 1)) o etac conjE,
blanchet@52325
   100
                       asm_simp_tac (ss_only [] ctxt)])
blanchet@52325
   101
                 else
blanchet@52325
   102
                   [dtac (the_single (if k = n then disc_excludes else disc_excludes')),
blanchet@52325
   103
                    etac (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}),
blanchet@52325
   104
                    atac, atac]))
blanchet@52325
   105
              ks disc_excludess disc_excludess' uncollapses)])
blanchet@52325
   106
          ks ms disc_excludesss disc_excludesss' uncollapses))
blanchet@49486
   107
    end;
blanchet@49486
   108
blanchet@52967
   109
fun mk_case_same_ctr_tac ctxt injects =
blanchet@52967
   110
  REPEAT_DETERM o etac exE THEN' etac conjE THEN'
blanchet@52967
   111
    (case injects of
blanchet@52967
   112
      [] => atac
blanchet@52967
   113
    | [inject] => dtac (inject RS iffD1) THEN' REPEAT_DETERM o etac conjE THEN'
blanchet@52967
   114
        hyp_subst_tac ctxt THEN' rtac refl);
blanchet@52967
   115
blanchet@52967
   116
fun mk_case_distinct_ctrs_tac ctxt distincts =
blanchet@52967
   117
  REPEAT_DETERM o etac exE THEN' etac conjE THEN' full_simp_tac (ss_only distincts ctxt);
blanchet@52967
   118
blanchet@52968
   119
fun mk_case_tac ctxt n k case_def injects distinctss =
blanchet@52968
   120
  let
blanchet@52968
   121
    val case_def' = mk_unabs_def (n + 1) (case_def RS meta_eq_to_obj_eq);
blanchet@52968
   122
    val ks = 1 upto n;
blanchet@52968
   123
  in
blanchet@52968
   124
    HEADGOAL (rtac (case_def' RS trans) THEN' rtac @{thm the_equality} THEN'
blanchet@52968
   125
      rtac (mk_disjIN n k) THEN' REPEAT_DETERM o rtac exI THEN' rtac conjI THEN' rtac refl THEN'
blanchet@52968
   126
      rtac refl THEN'
blanchet@52967
   127
      EVERY' (map2 (fn k' => fn distincts =>
blanchet@52967
   128
        (if k' < n then etac disjE else K all_tac) THEN'
blanchet@52967
   129
        (if k' = k then mk_case_same_ctr_tac ctxt injects
blanchet@52967
   130
         else mk_case_distinct_ctrs_tac ctxt distincts)) ks distinctss))
blanchet@52967
   131
  end;
blanchet@52967
   132
blanchet@53857
   133
fun mk_case_conv_if_tac ctxt n uexhaust cases discss' selss =
blanchet@52325
   134
  HEADGOAL (rtac uexhaust THEN'
blanchet@52325
   135
    EVERY' (map3 (fn casex => fn if_discs => fn sels =>
blanchet@52325
   136
        EVERY' [hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)),
blanchet@52325
   137
          rtac casex])
blanchet@52325
   138
      cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss));
blanchet@49031
   139
wenzelm@51717
   140
fun mk_case_cong_tac ctxt uexhaust cases =
blanchet@52325
   141
  HEADGOAL (rtac uexhaust THEN'
blanchet@52325
   142
    EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex] ctxt)]) cases));
blanchet@49043
   143
blanchet@53917
   144
fun mk_split_tac ctxt uexhaust cases selss injectss distinctsss =
blanchet@52325
   145
  HEADGOAL (rtac uexhaust) THEN
wenzelm@51798
   146
  ALLGOALS (fn k => (hyp_subst_tac ctxt THEN'
blanchet@53917
   147
     simp_tac (ss_only (@{thms simp_thms} @ cases @ nth selss (k - 1) @ nth injectss (k - 1) @
wenzelm@51717
   148
       flat (nth distinctsss (k - 1))) ctxt)) k) THEN
wenzelm@51937
   149
  ALLGOALS (blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt));
blanchet@49032
   150
blanchet@49044
   151
val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};
blanchet@49044
   152
blanchet@49044
   153
fun mk_split_asm_tac ctxt split =
blanchet@52325
   154
  HEADGOAL (rtac (split RS trans)) THEN unfold_thms_tac ctxt split_asm_thms THEN
blanchet@52325
   155
  HEADGOAL (rtac refl);
blanchet@49044
   156
blanchet@49020
   157
end;