src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML
author wenzelm
Fri, 19 Dec 2014 20:09:31 +0100
changeset 59153 b5e253703ebd
parent 58634 9f10d82e8188
child 59266 776964a0589f
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
54701
4ed7454aebde tuning -- moved ML files to subdirectory
blanchet
parents: 54491
diff changeset
     1
(*  Title:      HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
54397
f4b4fa25ce56 tuned headers
blanchet
parents: 54396
diff changeset
     3
    Copyright   2012, 2013
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
     4
51797
182454c06a80 tuned ML and thy file names
blanchet
parents: 51742
diff changeset
     5
Tactics for wrapping existing freely generated type's constructors.
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
     6
*)
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
     7
54008
b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents: 54007
diff changeset
     8
signature CTR_SUGAR_GENERAL_TACTICS =
b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents: 54007
diff changeset
     9
sig
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54844
diff changeset
    10
  val clean_blast_tac: Proof.context -> int -> tactic
54008
b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents: 54007
diff changeset
    11
  val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic
b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents: 54007
diff changeset
    12
  val unfold_thms_tac: Proof.context -> thm list -> tactic
b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents: 54007
diff changeset
    13
end;
b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents: 54007
diff changeset
    14
54006
9fe1bd54d437 renamed theory file
blanchet
parents: 53920
diff changeset
    15
signature CTR_SUGAR_TACTICS =
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
    16
sig
54008
b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents: 54007
diff changeset
    17
  include CTR_SUGAR_GENERAL_TACTICS
b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents: 54007
diff changeset
    18
49148
93f281430e77 fixed "mk_alternate_disc_def_tac" in the case where the constructors are swapped compared with the common Nil/Cons case
blanchet
parents: 49137
diff changeset
    19
  val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
52968
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52967
diff changeset
    20
  val mk_case_tac: Proof.context -> int -> int -> thm -> thm list -> thm list list -> tactic
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51686
diff changeset
    21
  val mk_case_cong_tac: Proof.context -> thm -> thm list -> tactic
54491
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54422
diff changeset
    22
  val mk_case_eq_if_tac: Proof.context -> int -> thm -> thm list -> thm list list ->
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54422
diff changeset
    23
    thm list list -> tactic
49118
b815fa776b91 renamed theorem
blanchet
parents: 49116
diff changeset
    24
  val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57525
diff changeset
    25
  val mk_exhaust_disc_tac: int -> thm -> thm list -> tactic
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57525
diff changeset
    26
  val mk_exhaust_sel_tac: int -> thm -> thm list -> tactic
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51686
diff changeset
    27
  val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list ->
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51686
diff changeset
    28
    thm list list list -> thm list list list -> tactic
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57525
diff changeset
    29
  val mk_half_distinct_disc_tac: Proof.context -> int -> thm -> thm -> tactic
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
    30
  val mk_nchotomy_tac: int -> thm -> tactic
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57525
diff changeset
    31
  val mk_other_half_distinct_disc_tac: thm -> tactic
54491
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54422
diff changeset
    32
  val mk_split_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list ->
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54422
diff changeset
    33
    thm list list list -> tactic
49044
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
    34
  val mk_split_asm_tac: Proof.context -> thm -> tactic
49137
5c8fefe0f103 fixed bugs in one-constructor case
blanchet
parents: 49122
diff changeset
    35
  val mk_unique_disc_def_tac: int -> thm -> tactic
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
    36
end;
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
    37
54006
9fe1bd54d437 renamed theory file
blanchet
parents: 53920
diff changeset
    38
structure Ctr_Sugar_Tactics : CTR_SUGAR_TACTICS =
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
    39
struct
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
    40
54008
b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents: 54007
diff changeset
    41
open Ctr_Sugar_Util
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
    42
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
    43
val meta_mp = @{thm meta_mp};
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
    44
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54844
diff changeset
    45
fun clean_blast_tac ctxt = blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt);
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54844
diff changeset
    46
54008
b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents: 54007
diff changeset
    47
fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl,
b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents: 54007
diff changeset
    48
  tac, REPEAT_DETERM_N (n - k) o etac thin_rl]);
b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents: 54007
diff changeset
    49
b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents: 54007
diff changeset
    50
fun unfold_thms_tac _ [] = all_tac
b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents: 54007
diff changeset
    51
  | unfold_thms_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms);
b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents: 54007
diff changeset
    52
49212
ca59649170b0 more sugar on codatatypes
blanchet
parents: 49174
diff changeset
    53
fun if_P_or_not_P_OF pos thm = thm RS (if pos then @{thm if_P} else @{thm if_not_P});
49031
632ee0da3c5b generate "case_disc" property
blanchet
parents: 49030
diff changeset
    54
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
    55
fun mk_nchotomy_tac n exhaust =
52325
blanchet
parents: 51937
diff changeset
    56
  HEADGOAL (rtac allI THEN' rtac exhaust THEN'
57525
f9dd8a33f820 generate 'rel_cases' theorem for (co)datatypes
desharna
parents: 54905
diff changeset
    57
    EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n)));
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
    58
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
    59
fun mk_unique_disc_def_tac m uexhaust =
52325
blanchet
parents: 51937
diff changeset
    60
  HEADGOAL (EVERY' [rtac iffI, rtac uexhaust, REPEAT_DETERM_N m o rtac exI, atac, rtac refl]);
49137
5c8fefe0f103 fixed bugs in one-constructor case
blanchet
parents: 49122
diff changeset
    61
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
    62
fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust =
52325
blanchet
parents: 51937
diff changeset
    63
  HEADGOAL (EVERY' ([rtac (other_disc_def RS @{thm arg_cong[of _ _ Not]} RS trans),
49630
9f6ca87ab405 tuned tactics
traytel
parents: 49594
diff changeset
    64
    rtac @{thm iffI_np}, REPEAT_DETERM o etac exE,
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51797
diff changeset
    65
    hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
    66
    rtac distinct, rtac uexhaust] @
49174
41790d616f63 by default, only generate one discriminator for a two-value datatype
blanchet
parents: 49168
diff changeset
    67
    (([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac])
52325
blanchet
parents: 51937
diff changeset
    68
     |> k = 1 ? swap |> op @)));
49116
3d520eec2746 allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
blanchet
parents: 49075
diff changeset
    69
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57525
diff changeset
    70
fun mk_half_distinct_disc_tac ctxt m discD disc' =
52325
blanchet
parents: 51937
diff changeset
    71
  HEADGOAL (dtac discD THEN' REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN'
blanchet
parents: 51937
diff changeset
    72
    rtac disc');
49028
487427a02bee generate "disc_distinct" theorems
blanchet
parents: 49022
diff changeset
    73
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57525
diff changeset
    74
fun mk_other_half_distinct_disc_tac half = HEADGOAL (etac @{thm contrapos_pn} THEN' etac half);
49028
487427a02bee generate "disc_distinct" theorems
blanchet
parents: 49022
diff changeset
    75
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57525
diff changeset
    76
fun mk_exhaust_disc_or_sel_tac n exhaust destIs =
52325
blanchet
parents: 51937
diff changeset
    77
  HEADGOAL (rtac exhaust THEN'
53916
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53857
diff changeset
    78
    EVERY' (map2 (fn k => fn destI => dtac destI THEN'
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53857
diff changeset
    79
      select_prem_tac n (etac meta_mp) k THEN' atac) (1 upto n) destIs));
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53857
diff changeset
    80
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57525
diff changeset
    81
val mk_exhaust_disc_tac = mk_exhaust_disc_or_sel_tac;
53916
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53857
diff changeset
    82
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57525
diff changeset
    83
fun mk_exhaust_sel_tac n exhaust_disc collapses =
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57525
diff changeset
    84
  mk_exhaust_disc_or_sel_tac n exhaust_disc collapses ORELSE
53920
c6de7f20c845 made tactic more robust in case somebody specified a discriminator for a one-constructor type
blanchet
parents: 53917
diff changeset
    85
  HEADGOAL (etac meta_mp THEN' resolve_tac collapses);
49029
f0ecfa9575a9 generate "disc_exhaust" property
blanchet
parents: 49028
diff changeset
    86
49484
0194a18f80cf finished "disc_coiter_iff" etc. generation
blanchet
parents: 49463
diff changeset
    87
fun mk_collapse_tac ctxt m discD sels =
52325
blanchet
parents: 51937
diff changeset
    88
  HEADGOAL (dtac discD THEN'
blanchet
parents: 51937
diff changeset
    89
    (if m = 0 then
blanchet
parents: 51937
diff changeset
    90
       atac
blanchet
parents: 51937
diff changeset
    91
     else
blanchet
parents: 51937
diff changeset
    92
       REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN'
blanchet
parents: 51937
diff changeset
    93
       SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl));
49030
d0f4f113e43d generate "ctr_sels" theorems
blanchet
parents: 49029
diff changeset
    94
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57525
diff changeset
    95
fun mk_expand_tac ctxt n ms uexhaust_disc vexhaust_disc uncollapses distinct_discsss
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57525
diff changeset
    96
    distinct_discsss' =
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
    97
  if ms = [0] then
52325
blanchet
parents: 51937
diff changeset
    98
    HEADGOAL (rtac (@{thm trans_sym} OF (replicate 2 (the_single uncollapses))) THEN'
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57525
diff changeset
    99
      TRY o EVERY' [rtac uexhaust_disc, atac, rtac vexhaust_disc, atac])
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   100
  else
51742
b5ff7393642d fix bugs in expand tactic w.r.t. datatypes with "needless" discriminators (e.g. lists with is_Nil instead of ~= Nil)
blanchet
parents: 51717
diff changeset
   101
    let val ks = 1 upto n in
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57525
diff changeset
   102
      HEADGOAL (rtac uexhaust_disc THEN'
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 57983
diff changeset
   103
        EVERY' (@{map 5} (fn k => fn m => fn distinct_discss => fn distinct_discss' => fn uuncollapse =>
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57525
diff changeset
   104
          EVERY' [rtac (uuncollapse RS trans) THEN' TRY o atac, rtac sym, rtac vexhaust_disc,
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 57983
diff changeset
   105
            EVERY' (@{map 4} (fn k' => fn distinct_discs => fn distinct_discs' => fn vuncollapse =>
52325
blanchet
parents: 51937
diff changeset
   106
              EVERY'
blanchet
parents: 51937
diff changeset
   107
                (if k' = k then
blanchet
parents: 51937
diff changeset
   108
                   [rtac (vuncollapse RS trans), TRY o atac] @
blanchet
parents: 51937
diff changeset
   109
                   (if m = 0 then
blanchet
parents: 51937
diff changeset
   110
                      [rtac refl]
blanchet
parents: 51937
diff changeset
   111
                    else
blanchet
parents: 51937
diff changeset
   112
                      [if n = 1 then K all_tac else EVERY' [dtac meta_mp, atac, dtac meta_mp, atac],
blanchet
parents: 51937
diff changeset
   113
                       REPEAT_DETERM_N (Int.max (0, m - 1)) o etac conjE,
blanchet
parents: 51937
diff changeset
   114
                       asm_simp_tac (ss_only [] ctxt)])
blanchet
parents: 51937
diff changeset
   115
                 else
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57525
diff changeset
   116
                   [dtac (the_single (if k = n then distinct_discs else distinct_discs')),
52325
blanchet
parents: 51937
diff changeset
   117
                    etac (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}),
blanchet
parents: 51937
diff changeset
   118
                    atac, atac]))
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57525
diff changeset
   119
              ks distinct_discss distinct_discss' uncollapses)])
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57525
diff changeset
   120
          ks ms distinct_discsss distinct_discsss' uncollapses))
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   121
    end;
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   122
52967
5e25877c51d4 introduced case tactics
blanchet
parents: 52966
diff changeset
   123
fun mk_case_same_ctr_tac ctxt injects =
5e25877c51d4 introduced case tactics
blanchet
parents: 52966
diff changeset
   124
  REPEAT_DETERM o etac exE THEN' etac conjE THEN'
5e25877c51d4 introduced case tactics
blanchet
parents: 52966
diff changeset
   125
    (case injects of
5e25877c51d4 introduced case tactics
blanchet
parents: 52966
diff changeset
   126
      [] => atac
5e25877c51d4 introduced case tactics
blanchet
parents: 52966
diff changeset
   127
    | [inject] => dtac (inject RS iffD1) THEN' REPEAT_DETERM o etac conjE THEN'
5e25877c51d4 introduced case tactics
blanchet
parents: 52966
diff changeset
   128
        hyp_subst_tac ctxt THEN' rtac refl);
5e25877c51d4 introduced case tactics
blanchet
parents: 52966
diff changeset
   129
5e25877c51d4 introduced case tactics
blanchet
parents: 52966
diff changeset
   130
fun mk_case_distinct_ctrs_tac ctxt distincts =
5e25877c51d4 introduced case tactics
blanchet
parents: 52966
diff changeset
   131
  REPEAT_DETERM o etac exE THEN' etac conjE THEN' full_simp_tac (ss_only distincts ctxt);
5e25877c51d4 introduced case tactics
blanchet
parents: 52966
diff changeset
   132
52968
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52967
diff changeset
   133
fun mk_case_tac ctxt n k case_def injects distinctss =
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52967
diff changeset
   134
  let
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52967
diff changeset
   135
    val case_def' = mk_unabs_def (n + 1) (case_def RS meta_eq_to_obj_eq);
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52967
diff changeset
   136
    val ks = 1 upto n;
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52967
diff changeset
   137
  in
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52967
diff changeset
   138
    HEADGOAL (rtac (case_def' RS trans) THEN' rtac @{thm the_equality} THEN'
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52967
diff changeset
   139
      rtac (mk_disjIN n k) THEN' REPEAT_DETERM o rtac exI THEN' rtac conjI THEN' rtac refl THEN'
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52967
diff changeset
   140
      rtac refl THEN'
52967
5e25877c51d4 introduced case tactics
blanchet
parents: 52966
diff changeset
   141
      EVERY' (map2 (fn k' => fn distincts =>
5e25877c51d4 introduced case tactics
blanchet
parents: 52966
diff changeset
   142
        (if k' < n then etac disjE else K all_tac) THEN'
5e25877c51d4 introduced case tactics
blanchet
parents: 52966
diff changeset
   143
        (if k' = k then mk_case_same_ctr_tac ctxt injects
5e25877c51d4 introduced case tactics
blanchet
parents: 52966
diff changeset
   144
         else mk_case_distinct_ctrs_tac ctxt distincts)) ks distinctss))
5e25877c51d4 introduced case tactics
blanchet
parents: 52966
diff changeset
   145
  end;
5e25877c51d4 introduced case tactics
blanchet
parents: 52966
diff changeset
   146
54491
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54422
diff changeset
   147
fun mk_case_cong_tac ctxt uexhaust cases =
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54422
diff changeset
   148
  HEADGOAL (rtac uexhaust THEN'
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54422
diff changeset
   149
    EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex] ctxt)]) cases));
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54422
diff changeset
   150
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54422
diff changeset
   151
fun mk_case_eq_if_tac ctxt n uexhaust cases discss' selss =
52325
blanchet
parents: 51937
diff changeset
   152
  HEADGOAL (rtac uexhaust THEN'
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 57983
diff changeset
   153
    EVERY' (@{map 3} (fn casex => fn if_discs => fn sels =>
52325
blanchet
parents: 51937
diff changeset
   154
        EVERY' [hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)),
blanchet
parents: 51937
diff changeset
   155
          rtac casex])
blanchet
parents: 51937
diff changeset
   156
      cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss));
49031
632ee0da3c5b generate "case_disc" property
blanchet
parents: 49030
diff changeset
   157
53917
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   158
fun mk_split_tac ctxt uexhaust cases selss injectss distinctsss =
52325
blanchet
parents: 51937
diff changeset
   159
  HEADGOAL (rtac uexhaust) THEN
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51797
diff changeset
   160
  ALLGOALS (fn k => (hyp_subst_tac ctxt THEN'
53917
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   161
     simp_tac (ss_only (@{thms simp_thms} @ cases @ nth selss (k - 1) @ nth injectss (k - 1) @
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51686
diff changeset
   162
       flat (nth distinctsss (k - 1))) ctxt)) k) THEN
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54844
diff changeset
   163
  ALLGOALS (clean_blast_tac ctxt);
49032
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   164
49044
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   165
val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   166
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   167
fun mk_split_asm_tac ctxt split =
52325
blanchet
parents: 51937
diff changeset
   168
  HEADGOAL (rtac (split RS trans)) THEN unfold_thms_tac ctxt split_asm_thms THEN
blanchet
parents: 51937
diff changeset
   169
  HEADGOAL (rtac refl);
49044
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   170
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
   171
end;
54008
b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents: 54007
diff changeset
   172
54491
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54422
diff changeset
   173
structure Ctr_Sugar_General_Tactics : CTR_SUGAR_GENERAL_TACTICS = Ctr_Sugar_Tactics;