src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML
author blanchet
Tue, 04 Sep 2012 13:02:31 +0200
changeset 49118 b815fa776b91
parent 49116 3d520eec2746
child 49122 83515378d4d7
permissions -rw-r--r--
renamed theorem
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
49074
d8af889dcbe3 renamed three BNF/(co)datatype-related commands
blanchet
parents: 49053
diff changeset
     1
(*  Title:      HOL/Codatatype/Tools/bnf_wrap_tactics.ML
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
     3
    Copyright   2012
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
     4
49074
d8af889dcbe3 renamed three BNF/(co)datatype-related commands
blanchet
parents: 49053
diff changeset
     5
Tactics for wrapping datatypes.
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
49074
d8af889dcbe3 renamed three BNF/(co)datatype-related commands
blanchet
parents: 49053
diff changeset
     8
signature BNF_WRAP_TACTICS =
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
     9
sig
49049
blanchet
parents: 49048
diff changeset
    10
  val mk_case_cong_tac: thm -> thm list -> tactic
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
    11
  val mk_case_eq_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> tactic
49118
b815fa776b91 renamed theorem
blanchet
parents: 49116
diff changeset
    12
  val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
49029
f0ecfa9575a9 generate "disc_exhaust" property
blanchet
parents: 49028
diff changeset
    13
  val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
49053
a6df36ecc2a8 renamed "disc_disjoint" property "disj_exclus"
blanchet
parents: 49052
diff changeset
    14
  val mk_half_disc_exclus_tac: int -> thm -> thm -> tactic
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
    15
  val mk_nchotomy_tac: int -> thm -> tactic
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
    16
  val mk_not_other_disc_def_tac: Proof.context -> thm -> thm -> thm -> tactic
49053
a6df36ecc2a8 renamed "disc_disjoint" property "disj_exclus"
blanchet
parents: 49052
diff changeset
    17
  val mk_other_half_disc_exclus_tac: thm -> tactic
49052
3510b943dd5b optimized "mk_split_tac" + use "notes"
blanchet
parents: 49051
diff changeset
    18
  val mk_split_tac: thm -> thm list -> thm list list -> thm list list list -> tactic
49044
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
    19
  val mk_split_asm_tac: Proof.context -> thm -> tactic
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
    20
end;
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
    21
49074
d8af889dcbe3 renamed three BNF/(co)datatype-related commands
blanchet
parents: 49053
diff changeset
    22
structure BNF_Wrap_Tactics : BNF_WRAP_TACTICS =
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
    23
struct
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
    24
49050
9f4a7ed344b4 optimized "mk_case_disc_tac"
blanchet
parents: 49049
diff changeset
    25
open BNF_Util
49029
f0ecfa9575a9 generate "disc_exhaust" property
blanchet
parents: 49028
diff changeset
    26
open BNF_Tactics
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
    27
49051
58d3c939f91a optimized "mk_case_disc_tac" further
blanchet
parents: 49050
diff changeset
    28
fun triangle _ [] = []
58d3c939f91a optimized "mk_case_disc_tac" further
blanchet
parents: 49050
diff changeset
    29
  | triangle k (xs :: xss) = take k xs :: triangle (k + 1) xss
58d3c939f91a optimized "mk_case_disc_tac" further
blanchet
parents: 49050
diff changeset
    30
58d3c939f91a optimized "mk_case_disc_tac" further
blanchet
parents: 49050
diff changeset
    31
fun mk_if_P_or_not_P thm =
58d3c939f91a optimized "mk_case_disc_tac" further
blanchet
parents: 49050
diff changeset
    32
  thm RS @{thm if_not_P} handle THM _ => thm RS @{thm if_P}
49031
632ee0da3c5b generate "case_disc" property
blanchet
parents: 49030
diff changeset
    33
49047
f57c4bb10575 optimized "case_cong" proof
blanchet
parents: 49045
diff changeset
    34
fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms
49032
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
    35
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
    36
fun mk_nchotomy_tac n exhaust =
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
    37
  (rtac allI THEN' rtac exhaust THEN'
49022
005ce926a932 define selectors and discriminators
blanchet
parents: 49020
diff changeset
    38
   EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1;
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
    39
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
    40
fun mk_not_other_disc_def_tac ctxt other_disc_def distinct exhaust' =
3d520eec2746 allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
blanchet
parents: 49075
diff changeset
    41
  EVERY' [subst_tac ctxt [other_disc_def], rtac @{thm iffI_np}, hyp_subst_tac,
3d520eec2746 allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
blanchet
parents: 49075
diff changeset
    42
    SELECT_GOAL (Local_Defs.unfold_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI, rtac distinct,
3d520eec2746 allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
blanchet
parents: 49075
diff changeset
    43
    rtac exhaust', etac notE, atac, REPEAT_DETERM o rtac exI, atac] 1;
3d520eec2746 allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
blanchet
parents: 49075
diff changeset
    44
49053
a6df36ecc2a8 renamed "disc_disjoint" property "disj_exclus"
blanchet
parents: 49052
diff changeset
    45
fun mk_half_disc_exclus_tac m discD disc'_thm =
49030
d0f4f113e43d generate "ctr_sels" theorems
blanchet
parents: 49029
diff changeset
    46
  (dtac discD THEN'
49028
487427a02bee generate "disc_distinct" theorems
blanchet
parents: 49022
diff changeset
    47
   REPEAT_DETERM_N m o etac exE THEN'
487427a02bee generate "disc_distinct" theorems
blanchet
parents: 49022
diff changeset
    48
   hyp_subst_tac THEN'
487427a02bee generate "disc_distinct" theorems
blanchet
parents: 49022
diff changeset
    49
   rtac disc'_thm) 1;
487427a02bee generate "disc_distinct" theorems
blanchet
parents: 49022
diff changeset
    50
49053
a6df36ecc2a8 renamed "disc_disjoint" property "disj_exclus"
blanchet
parents: 49052
diff changeset
    51
fun mk_other_half_disc_exclus_tac half_thm =
49028
487427a02bee generate "disc_distinct" theorems
blanchet
parents: 49022
diff changeset
    52
  (etac @{thm contrapos_pn} THEN' etac half_thm) 1;
487427a02bee generate "disc_distinct" theorems
blanchet
parents: 49022
diff changeset
    53
49029
f0ecfa9575a9 generate "disc_exhaust" property
blanchet
parents: 49028
diff changeset
    54
fun mk_disc_exhaust_tac n exhaust discIs =
f0ecfa9575a9 generate "disc_exhaust" property
blanchet
parents: 49028
diff changeset
    55
  (rtac exhaust THEN'
f0ecfa9575a9 generate "disc_exhaust" property
blanchet
parents: 49028
diff changeset
    56
   EVERY' (map2 (fn k => fn discI =>
f0ecfa9575a9 generate "disc_exhaust" property
blanchet
parents: 49028
diff changeset
    57
     dtac discI THEN' select_prem_tac n (etac @{thm meta_mp}) k THEN' atac) (1 upto n) discIs)) 1;
f0ecfa9575a9 generate "disc_exhaust" property
blanchet
parents: 49028
diff changeset
    58
49118
b815fa776b91 renamed theorem
blanchet
parents: 49116
diff changeset
    59
fun mk_collapse_tac ctxt m discD sel_thms =
49030
d0f4f113e43d generate "ctr_sels" theorems
blanchet
parents: 49029
diff changeset
    60
  (dtac discD THEN'
d0f4f113e43d generate "ctr_sels" theorems
blanchet
parents: 49029
diff changeset
    61
   (if m = 0 then
d0f4f113e43d generate "ctr_sels" theorems
blanchet
parents: 49029
diff changeset
    62
      atac
d0f4f113e43d generate "ctr_sels" theorems
blanchet
parents: 49029
diff changeset
    63
    else
d0f4f113e43d generate "ctr_sels" theorems
blanchet
parents: 49029
diff changeset
    64
      REPEAT_DETERM_N m o etac exE THEN'
d0f4f113e43d generate "ctr_sels" theorems
blanchet
parents: 49029
diff changeset
    65
      hyp_subst_tac THEN'
49031
632ee0da3c5b generate "case_disc" property
blanchet
parents: 49030
diff changeset
    66
      SELECT_GOAL (Local_Defs.unfold_tac ctxt sel_thms) THEN'
49030
d0f4f113e43d generate "ctr_sels" theorems
blanchet
parents: 49029
diff changeset
    67
      rtac refl)) 1;
d0f4f113e43d generate "ctr_sels" theorems
blanchet
parents: 49029
diff changeset
    68
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
fun mk_case_eq_tac ctxt exhaust' case_thms disc_thmss' sel_thmss =
49050
9f4a7ed344b4 optimized "mk_case_disc_tac"
blanchet
parents: 49049
diff changeset
    70
  (rtac exhaust' THEN'
49051
58d3c939f91a optimized "mk_case_disc_tac" further
blanchet
parents: 49050
diff changeset
    71
   EVERY' (map3 (fn case_thm => fn if_disc_thms => fn sel_thms => EVERY' [
49050
9f4a7ed344b4 optimized "mk_case_disc_tac"
blanchet
parents: 49049
diff changeset
    72
     hyp_subst_tac THEN'
49051
58d3c939f91a optimized "mk_case_disc_tac" further
blanchet
parents: 49050
diff changeset
    73
     SELECT_GOAL (Local_Defs.unfold_tac ctxt (if_disc_thms @ sel_thms)) THEN'
58d3c939f91a optimized "mk_case_disc_tac" further
blanchet
parents: 49050
diff changeset
    74
     rtac case_thm]) case_thms
58d3c939f91a optimized "mk_case_disc_tac" further
blanchet
parents: 49050
diff changeset
    75
  (map (map mk_if_P_or_not_P) (triangle 1 (map (fst o split_last) disc_thmss'))) sel_thmss)) 1;
49031
632ee0da3c5b generate "case_disc" property
blanchet
parents: 49030
diff changeset
    76
49049
blanchet
parents: 49048
diff changeset
    77
fun mk_case_cong_tac exhaust' case_thms =
49047
f57c4bb10575 optimized "case_cong" proof
blanchet
parents: 49045
diff changeset
    78
  (rtac exhaust' THEN'
f57c4bb10575 optimized "case_cong" proof
blanchet
parents: 49045
diff changeset
    79
   EVERY' (maps (fn case_thm => [dtac sym, asm_simp_tac (ss_only [case_thm])]) case_thms)) 1;
49043
bd3e33ee762d generate "split" property
blanchet
parents: 49032
diff changeset
    80
bd3e33ee762d generate "split" property
blanchet
parents: 49032
diff changeset
    81
val naked_ctxt = Proof_Context.init_global @{theory HOL};
bd3e33ee762d generate "split" property
blanchet
parents: 49032
diff changeset
    82
49052
3510b943dd5b optimized "mk_split_tac" + use "notes"
blanchet
parents: 49051
diff changeset
    83
fun mk_split_tac exhaust' case_thms injectss distinctsss =
49043
bd3e33ee762d generate "split" property
blanchet
parents: 49032
diff changeset
    84
  rtac exhaust' 1 THEN
49052
3510b943dd5b optimized "mk_split_tac" + use "notes"
blanchet
parents: 49051
diff changeset
    85
  ALLGOALS (fn k =>
3510b943dd5b optimized "mk_split_tac" + use "notes"
blanchet
parents: 49051
diff changeset
    86
    (hyp_subst_tac THEN'
3510b943dd5b optimized "mk_split_tac" + use "notes"
blanchet
parents: 49051
diff changeset
    87
     simp_tac (ss_only (@{thms simp_thms} @ case_thms @ nth injectss (k - 1) @
3510b943dd5b optimized "mk_split_tac" + use "notes"
blanchet
parents: 49051
diff changeset
    88
       flat (nth distinctsss (k - 1))))) k) THEN
49045
7d9631754bba minor fixes (for compatibility with existing datatype package)
blanchet
parents: 49044
diff changeset
    89
  ALLGOALS (blast_tac naked_ctxt);
49032
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
    90
49044
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
    91
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
    92
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
    93
fun mk_split_asm_tac ctxt split =
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
    94
  rtac (split RS trans) 1 THEN
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
    95
  Local_Defs.unfold_tac ctxt split_asm_thms THEN
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
    96
  rtac refl 1;
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
    97
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff changeset
    98
end;