src/HOL/Codatatype/Tools/bnf_wrap.ML
author blanchet
Wed, 12 Sep 2012 00:20:37 +0200
changeset 49300 c707df2e2083
parent 49298 36e551d3af3b
child 49302 f5bd87aac224
permissions -rw-r--r--
added attributes to theorems
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
49074
d8af889dcbe3 renamed three BNF/(co)datatype-related commands
blanchet
parents: 49057
diff changeset
     1
(*  Title:      HOL/Codatatype/Tools/bnf_wrap.ML
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
     3
    Copyright   2012
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
     4
49074
d8af889dcbe3 renamed three BNF/(co)datatype-related commands
blanchet
parents: 49057
diff changeset
     5
Wrapping existing datatypes.
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
     6
*)
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
     7
49074
d8af889dcbe3 renamed three BNF/(co)datatype-related commands
blanchet
parents: 49057
diff changeset
     8
signature BNF_WRAP =
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
     9
sig
49129
b5413cb7d860 define "case" constant
blanchet
parents: 49125
diff changeset
    10
  val no_binder: binding
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
    11
  val mk_half_pairss: 'a list -> ('a * 'a) list list
49203
262ab1ac38b9 repaired constant types
blanchet
parents: 49201
diff changeset
    12
  val mk_ctr: typ list -> term -> term
49199
7c9a3c67c55d added high-level recursor, not yet curried
blanchet
parents: 49174
diff changeset
    13
  val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list ->
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
    14
    ((bool * term list) * term) *
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
    15
      (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
49266
70ffce5b65a4 generate "sel_coiters" and friends
blanchet
parents: 49265
diff changeset
    16
    (term list list * thm list * thm list list) * local_theory
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
    17
  val parse_wrap_options: bool parser
49286
dde4967c9233 added "defaults" option
blanchet
parents: 49285
diff changeset
    18
  val parse_bound_term: (binding * string) parser
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
    19
end;
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
    20
49074
d8af889dcbe3 renamed three BNF/(co)datatype-related commands
blanchet
parents: 49057
diff changeset
    21
structure BNF_Wrap : BNF_WRAP =
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
    22
struct
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
    23
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
    24
open BNF_Util
49074
d8af889dcbe3 renamed three BNF/(co)datatype-related commands
blanchet
parents: 49057
diff changeset
    25
open BNF_Wrap_Tactics
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
    26
49223
blanchet
parents: 49210
diff changeset
    27
val isN = "is_";
blanchet
parents: 49210
diff changeset
    28
val unN = "un_";
blanchet
parents: 49210
diff changeset
    29
fun mk_unN 1 1 suf = unN ^ suf
blanchet
parents: 49210
diff changeset
    30
  | mk_unN _ l suf = unN ^ suf ^ string_of_int l;
49046
3c5eba97d93a allow default names for selectors via wildcard (_) + fix wrong index (k)
blanchet
parents: 49045
diff changeset
    31
49054
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
    32
val case_congN = "case_cong";
49116
3d520eec2746 allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
blanchet
parents: 49114
diff changeset
    33
val case_eqN = "case_eq";
49054
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
    34
val casesN = "cases";
49118
b815fa776b91 renamed theorem
blanchet
parents: 49117
diff changeset
    35
val collapseN = "collapse";
49122
83515378d4d7 renamed "disc_exclus" theorem to "disc_exclude"
blanchet
parents: 49121
diff changeset
    36
val disc_excludeN = "disc_exclude";
49054
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
    37
val disc_exhaustN = "disc_exhaust";
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
    38
val discsN = "discs";
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
    39
val distinctN = "distinct";
49075
ed769978dc8d rearrange dependencies
blanchet
parents: 49074
diff changeset
    40
val exhaustN = "exhaust";
ed769978dc8d rearrange dependencies
blanchet
parents: 49074
diff changeset
    41
val injectN = "inject";
ed769978dc8d rearrange dependencies
blanchet
parents: 49074
diff changeset
    42
val nchotomyN = "nchotomy";
49054
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
    43
val selsN = "sels";
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
    44
val splitN = "split";
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
    45
val split_asmN = "split_asm";
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
    46
val weak_case_cong_thmsN = "weak_case_cong";
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
    47
49139
e36ce78add78 use empty binding rather than "*" for default
blanchet
parents: 49137
diff changeset
    48
val no_binder = @{binding ""};
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
    49
val std_binder = @{binding _};
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
    50
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
    51
val induct_simp_attrs = @{attributes [induct_simp]};
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
    52
val cong_attrs = @{attributes [cong]};
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
    53
val iff_attrs = @{attributes [iff]};
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
    54
val safe_elim_attrs = @{attributes [elim!]};
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
    55
val simp_attrs = @{attributes [simp]};
49046
3c5eba97d93a allow default names for selectors via wildcard (_) + fix wrong index (k)
blanchet
parents: 49045
diff changeset
    56
49056
blanchet
parents: 49055
diff changeset
    57
fun pad_list x n xs = xs @ replicate (n - length xs) x;
blanchet
parents: 49055
diff changeset
    58
49259
b21c03c7a097 minor optimization
blanchet
parents: 49258
diff changeset
    59
fun unflat_lookup eq ys zs = map (map (fn x => nth zs (find_index (curry eq x) ys)));
49258
84f13469d7f0 allow same selector name for several constructors
blanchet
parents: 49257
diff changeset
    60
49048
4e0f0f98be02 rationalized data structure for distinctness theorems
blanchet
parents: 49046
diff changeset
    61
fun mk_half_pairss' _ [] = []
49056
blanchet
parents: 49055
diff changeset
    62
  | mk_half_pairss' indent (y :: ys) =
blanchet
parents: 49055
diff changeset
    63
    indent @ fold_rev (cons o single o pair y) ys (mk_half_pairss' ([] :: indent) ys);
49027
fc3b9b49c92d added discriminator theorems
blanchet
parents: 49025
diff changeset
    64
49048
4e0f0f98be02 rationalized data structure for distinctness theorems
blanchet
parents: 49046
diff changeset
    65
fun mk_half_pairss ys = mk_half_pairss' [[]] ys;
49027
fc3b9b49c92d added discriminator theorems
blanchet
parents: 49025
diff changeset
    66
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
    67
fun mk_undefined T = Const (@{const_name undefined}, T);
49055
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
    68
49203
262ab1ac38b9 repaired constant types
blanchet
parents: 49201
diff changeset
    69
fun mk_ctr Ts ctr =
262ab1ac38b9 repaired constant types
blanchet
parents: 49201
diff changeset
    70
  let val Type (_, Ts0) = body_type (fastype_of ctr) in
262ab1ac38b9 repaired constant types
blanchet
parents: 49201
diff changeset
    71
    Term.subst_atomic_types (Ts0 ~~ Ts) ctr
262ab1ac38b9 repaired constant types
blanchet
parents: 49201
diff changeset
    72
  end;
262ab1ac38b9 repaired constant types
blanchet
parents: 49201
diff changeset
    73
49130
3c26e17b2849 implemented "mk_case_tac" -- and got rid of "cheat_tac"
blanchet
parents: 49129
diff changeset
    74
fun eta_expand_case_arg xs f_xs = fold_rev Term.lambda xs f_xs;
49032
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
    75
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
    76
fun base_name_of_ctr c =
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
    77
  Long_Name.base_name (case head_of c of
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
    78
      Const (s, _) => s
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
    79
    | Free (s, _) => s
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
    80
    | _ => error "Cannot extract name of constructor");
49046
3c5eba97d93a allow default names for selectors via wildcard (_) + fix wrong index (k)
blanchet
parents: 49045
diff changeset
    81
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
    82
fun prepare_wrap_datatype prep_term (((no_dests, raw_ctrs), raw_case),
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
    83
    (raw_disc_binders, (raw_sel_binderss, raw_sel_defaultss))) no_defs_lthy =
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
    84
  let
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
    85
    (* TODO: sanity checks on arguments *)
49113
ef3eea7ae251 tuned TODOs
blanchet
parents: 49111
diff changeset
    86
    (* TODO: attributes (simp, case_names, etc.) *)
ef3eea7ae251 tuned TODOs
blanchet
parents: 49111
diff changeset
    87
    (* TODO: case syntax *)
ef3eea7ae251 tuned TODOs
blanchet
parents: 49111
diff changeset
    88
    (* TODO: integration with function package ("size") *)
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
    89
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
    90
    val n = length raw_ctrs;
49054
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
    91
    val ks = 1 upto n;
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
    92
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
    93
    val _ = if n > 0 then () else error "No constructors specified";
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
    94
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
    95
    val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs;
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
    96
    val case0 = prep_term no_defs_lthy raw_case;
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
    97
    val sel_defaultss =
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
    98
      pad_list [] n (map (map (apsnd (prep_term no_defs_lthy))) raw_sel_defaultss);
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
    99
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   100
    val Type (dataT_name, As0) = body_type (fastype_of (hd ctrs0));
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   101
    val b = Binding.qualified_name dataT_name;
49055
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   102
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   103
    val (As, B) =
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   104
      no_defs_lthy
49298
36e551d3af3b support for sort constraints in new (co)data commands
blanchet
parents: 49297
diff changeset
   105
      |> mk_TFrees' (map Type.sort_of_atyp As0)
49055
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   106
      ||> the_single o fst o mk_TFrees 1;
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   107
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   108
    val dataT = Type (dataT_name, As);
49055
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   109
    val ctrs = map (mk_ctr As) ctrs0;
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   110
    val ctr_Tss = map (binder_types o fastype_of) ctrs;
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   111
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   112
    val ms = map length ctr_Tss;
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   113
49129
b5413cb7d860 define "case" constant
blanchet
parents: 49125
diff changeset
   114
    val raw_disc_binders' = pad_list no_binder n raw_disc_binders;
49120
7f8e69fc6ac9 smarter "*" syntax -- fallback on "_" if "*" is impossible
blanchet
parents: 49119
diff changeset
   115
49174
41790d616f63 by default, only generate one discriminator for a two-value datatype
blanchet
parents: 49157
diff changeset
   116
    fun can_really_rely_on_disc k =
49152
feb984727eec tuning (systematic 1-based indices)
blanchet
parents: 49150
diff changeset
   117
      not (Binding.eq_name (nth raw_disc_binders' (k - 1), no_binder)) orelse nth ms (k - 1) = 0;
49174
41790d616f63 by default, only generate one discriminator for a two-value datatype
blanchet
parents: 49157
diff changeset
   118
    fun can_rely_on_disc k =
41790d616f63 by default, only generate one discriminator for a two-value datatype
blanchet
parents: 49157
diff changeset
   119
      can_really_rely_on_disc k orelse (k = 1 andalso not (can_really_rely_on_disc 2));
49129
b5413cb7d860 define "case" constant
blanchet
parents: 49125
diff changeset
   120
    fun can_omit_disc_binder k m =
49174
41790d616f63 by default, only generate one discriminator for a two-value datatype
blanchet
parents: 49157
diff changeset
   121
      n = 1 orelse m = 0 orelse (n = 2 andalso can_rely_on_disc (3 - k));
49120
7f8e69fc6ac9 smarter "*" syntax -- fallback on "_" if "*" is impossible
blanchet
parents: 49119
diff changeset
   122
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   123
    val std_disc_binder = Binding.name o prefix isN o base_name_of_ctr;
49120
7f8e69fc6ac9 smarter "*" syntax -- fallback on "_" if "*" is impossible
blanchet
parents: 49119
diff changeset
   124
49129
b5413cb7d860 define "case" constant
blanchet
parents: 49125
diff changeset
   125
    val disc_binders =
b5413cb7d860 define "case" constant
blanchet
parents: 49125
diff changeset
   126
      raw_disc_binders'
49120
7f8e69fc6ac9 smarter "*" syntax -- fallback on "_" if "*" is impossible
blanchet
parents: 49119
diff changeset
   127
      |> map4 (fn k => fn m => fn ctr => fn disc =>
49129
b5413cb7d860 define "case" constant
blanchet
parents: 49125
diff changeset
   128
        if Binding.eq_name (disc, no_binder) then
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   129
          if can_omit_disc_binder k m then NONE else SOME (std_disc_binder ctr)
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   130
        else if Binding.eq_name (disc, std_binder) then
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   131
          SOME (std_disc_binder ctr)
49046
3c5eba97d93a allow default names for selectors via wildcard (_) + fix wrong index (k)
blanchet
parents: 49045
diff changeset
   132
        else
49120
7f8e69fc6ac9 smarter "*" syntax -- fallback on "_" if "*" is impossible
blanchet
parents: 49119
diff changeset
   133
          SOME disc) ks ms ctrs0;
49056
blanchet
parents: 49055
diff changeset
   134
49129
b5413cb7d860 define "case" constant
blanchet
parents: 49125
diff changeset
   135
    val no_discs = map is_none disc_binders;
49137
5c8fefe0f103 fixed bugs in one-constructor case
blanchet
parents: 49136
diff changeset
   136
    val no_discs_at_all = forall I no_discs;
49116
3d520eec2746 allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
blanchet
parents: 49114
diff changeset
   137
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   138
    fun std_sel_binder m l = Binding.name o mk_unN m l o base_name_of_ctr;
49120
7f8e69fc6ac9 smarter "*" syntax -- fallback on "_" if "*" is impossible
blanchet
parents: 49119
diff changeset
   139
49129
b5413cb7d860 define "case" constant
blanchet
parents: 49125
diff changeset
   140
    val sel_binderss =
b5413cb7d860 define "case" constant
blanchet
parents: 49125
diff changeset
   141
      pad_list [] n raw_sel_binderss
49056
blanchet
parents: 49055
diff changeset
   142
      |> map3 (fn ctr => fn m => map2 (fn l => fn sel =>
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   143
        if Binding.eq_name (sel, no_binder) orelse Binding.eq_name (sel, std_binder) then
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   144
          std_sel_binder m l ctr
49056
blanchet
parents: 49055
diff changeset
   145
        else
49129
b5413cb7d860 define "case" constant
blanchet
parents: 49125
diff changeset
   146
          sel) (1 upto m) o pad_list no_binder m) ctrs0 ms;
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   147
49130
3c26e17b2849 implemented "mk_case_tac" -- and got rid of "cheat_tac"
blanchet
parents: 49129
diff changeset
   148
    fun mk_case Ts T =
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   149
      let
49130
3c26e17b2849 implemented "mk_case_tac" -- and got rid of "cheat_tac"
blanchet
parents: 49129
diff changeset
   150
        val (binders, body) = strip_type (fastype_of case0)
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   151
        val Type (_, Ts0) = List.last binders
49130
3c26e17b2849 implemented "mk_case_tac" -- and got rid of "cheat_tac"
blanchet
parents: 49129
diff changeset
   152
      in Term.subst_atomic_types ((body, T) :: (Ts0 ~~ Ts)) case0 end;
49022
005ce926a932 define selectors and discriminators
blanchet
parents: 49020
diff changeset
   153
49201
blanchet
parents: 49199
diff changeset
   154
    val casex = mk_case As B;
blanchet
parents: 49199
diff changeset
   155
    val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
49043
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   156
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   157
    val (((((((xss, yss), fs), gs), (v, v')), w), (p, p')), names_lthy) = no_defs_lthy |>
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   158
      mk_Freess "x" ctr_Tss
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   159
      ||>> mk_Freess "y" ctr_Tss
49201
blanchet
parents: 49199
diff changeset
   160
      ||>> mk_Frees "f" case_Ts
blanchet
parents: 49199
diff changeset
   161
      ||>> mk_Frees "g" case_Ts
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   162
      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "v") dataT
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   163
      ||>> yield_singleton (mk_Frees "w") dataT
49043
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   164
      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT;
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   165
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   166
    val q = Free (fst p', B --> HOLogic.boolT);
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   167
49210
656fb50d33f0 define coiterators
blanchet
parents: 49203
diff changeset
   168
    fun ap_v t = t $ v;
49137
5c8fefe0f103 fixed bugs in one-constructor case
blanchet
parents: 49136
diff changeset
   169
    fun mk_v_eq_v () = HOLogic.mk_eq (v, v);
5c8fefe0f103 fixed bugs in one-constructor case
blanchet
parents: 49136
diff changeset
   170
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   171
    val xctrs = map2 (curry Term.list_comb) ctrs xss;
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   172
    val yctrs = map2 (curry Term.list_comb) ctrs yss;
49032
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   173
49043
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   174
    val xfs = map2 (curry Term.list_comb) fs xss;
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   175
    val xgs = map2 (curry Term.list_comb) gs xss;
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   176
49130
3c26e17b2849 implemented "mk_case_tac" -- and got rid of "cheat_tac"
blanchet
parents: 49129
diff changeset
   177
    val eta_fs = map2 eta_expand_case_arg xss xfs;
3c26e17b2849 implemented "mk_case_tac" -- and got rid of "cheat_tac"
blanchet
parents: 49129
diff changeset
   178
    val eta_gs = map2 eta_expand_case_arg xss xgs;
49043
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   179
49201
blanchet
parents: 49199
diff changeset
   180
    val fcase = Term.list_comb (casex, eta_fs);
blanchet
parents: 49199
diff changeset
   181
    val gcase = Term.list_comb (casex, eta_gs);
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   182
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   183
    val exist_xs_v_eq_ctrs =
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   184
      map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (v, xctr))) xctrs xss;
49022
005ce926a932 define selectors and discriminators
blanchet
parents: 49020
diff changeset
   185
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   186
    val unique_disc_no_def = TrueI; (*arbitrary marker*)
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   187
    val alternate_disc_no_def = FalseE; (*arbitrary marker*)
49116
3d520eec2746 allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
blanchet
parents: 49114
diff changeset
   188
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   189
    fun alternate_disc_lhs get_disc k =
49116
3d520eec2746 allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
blanchet
parents: 49114
diff changeset
   190
      HOLogic.mk_not
49152
feb984727eec tuning (systematic 1-based indices)
blanchet
parents: 49150
diff changeset
   191
        (case nth disc_binders (k - 1) of
feb984727eec tuning (systematic 1-based indices)
blanchet
parents: 49150
diff changeset
   192
          NONE => nth exist_xs_v_eq_ctrs (k - 1)
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   193
        | SOME b => get_disc b (k - 1) $ v);
49116
3d520eec2746 allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
blanchet
parents: 49114
diff changeset
   194
49285
036b833b99aa removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents: 49281
diff changeset
   195
    val (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') =
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   196
      if no_dests then
49285
036b833b99aa removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents: 49281
diff changeset
   197
        (true, [], [], [], [], [], no_defs_lthy)
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   198
      else
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   199
        let
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   200
          fun disc_free b = Free (Binding.name_of b, dataT --> HOLogic.boolT);
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   201
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   202
          fun disc_spec b exist_xs_v_eq_ctr = mk_Trueprop_eq (disc_free b $ v, exist_xs_v_eq_ctr);
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   203
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   204
          fun alternate_disc k = Term.lambda v (alternate_disc_lhs (K o disc_free) (3 - k));
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   205
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   206
          fun mk_sel_case_args b proto_sels T =
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   207
            map2 (fn Ts => fn k =>
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   208
              (case AList.lookup (op =) proto_sels k of
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   209
                NONE =>
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   210
                let val def_T = Ts ---> T in
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   211
                  (case AList.lookup Binding.eq_name (rev (nth sel_defaultss (k - 1))) b of
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   212
                    NONE => mk_undefined def_T
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   213
                  | SOME t => fold_rev (fn T => Term.lambda (Free (Name.uu, T))) Ts
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   214
                      (Term.subst_atomic_types [(fastype_of t, T)] t))
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   215
                end
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   216
              | SOME (xs, x) => fold_rev Term.lambda xs x)) ctr_Tss ks;
49258
84f13469d7f0 allow same selector name for several constructors
blanchet
parents: 49257
diff changeset
   217
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   218
          fun sel_spec b proto_sels =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   219
            let
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   220
              val _ =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   221
                (case duplicates (op =) (map fst proto_sels) of
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   222
                   k :: _ => error ("Duplicate selector name " ^ quote (Binding.name_of b) ^
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   223
                     " for constructor " ^
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   224
                     quote (Syntax.string_of_term no_defs_lthy (nth ctrs (k - 1))))
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   225
                 | [] => ())
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   226
              val T =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   227
                (case distinct (op =) (map (fastype_of o snd o snd) proto_sels) of
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   228
                  [T] => T
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   229
                | T :: T' :: _ => error ("Inconsistent range type for selector " ^
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   230
                    quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   231
                    " vs. " ^ quote (Syntax.string_of_typ no_defs_lthy T')));
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   232
            in
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   233
              mk_Trueprop_eq (Free (Binding.name_of b, dataT --> T) $ v,
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   234
                Term.list_comb (mk_case As T, mk_sel_case_args b proto_sels T) $ v)
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   235
            end;
49116
3d520eec2746 allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
blanchet
parents: 49114
diff changeset
   236
49285
036b833b99aa removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents: 49281
diff changeset
   237
          val sel_binders = flat sel_binderss;
036b833b99aa removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents: 49281
diff changeset
   238
          val uniq_sel_binders = distinct Binding.eq_name sel_binders;
036b833b99aa removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents: 49281
diff changeset
   239
          val all_sels_distinct = (length uniq_sel_binders = length sel_binders);
036b833b99aa removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents: 49281
diff changeset
   240
036b833b99aa removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents: 49281
diff changeset
   241
          val sel_binder_index =
036b833b99aa removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents: 49281
diff changeset
   242
            if all_sels_distinct then 1 upto length sel_binders
036b833b99aa removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents: 49281
diff changeset
   243
            else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_binders) sel_binders;
036b833b99aa removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents: 49281
diff changeset
   244
036b833b99aa removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents: 49281
diff changeset
   245
          val proto_sels = flat (map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss);
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   246
          val sel_infos =
49285
036b833b99aa removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents: 49281
diff changeset
   247
            AList.group (op =) (sel_binder_index ~~ proto_sels)
036b833b99aa removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents: 49281
diff changeset
   248
            |> sort (int_ord o pairself fst)
036b833b99aa removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents: 49281
diff changeset
   249
            |> map snd |> curry (op ~~) uniq_sel_binders;
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   250
          val sel_binders = map fst sel_infos;
49258
84f13469d7f0 allow same selector name for several constructors
blanchet
parents: 49257
diff changeset
   251
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   252
          fun unflat_selss xs = unflat_lookup Binding.eq_name sel_binders xs sel_binderss;
49258
84f13469d7f0 allow same selector name for several constructors
blanchet
parents: 49257
diff changeset
   253
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   254
          val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   255
            no_defs_lthy
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   256
            |> apfst split_list o fold_map4 (fn k => fn m => fn exist_xs_v_eq_ctr =>
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   257
              fn NONE =>
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   258
                 if n = 1 then pair (Term.lambda v (mk_v_eq_v ()), unique_disc_no_def)
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   259
                 else if m = 0 then pair (Term.lambda v exist_xs_v_eq_ctr, refl)
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   260
                 else pair (alternate_disc k, alternate_disc_no_def)
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   261
               | SOME b => Specification.definition (SOME (b, NONE, NoSyn),
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   262
                   ((Thm.def_binding b, []), disc_spec b exist_xs_v_eq_ctr)) #>> apsnd snd)
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   263
              ks ms exist_xs_v_eq_ctrs disc_binders
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   264
            ||>> apfst split_list o fold_map (fn (b, proto_sels) =>
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   265
              Specification.definition (SOME (b, NONE, NoSyn),
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   266
                ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   267
            ||> `Local_Theory.restore;
49022
005ce926a932 define selectors and discriminators
blanchet
parents: 49020
diff changeset
   268
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   269
          (*transforms defined frees into consts (and more)*)
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   270
          val phi = Proof_Context.export_morphism lthy lthy';
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   271
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   272
          val disc_defs = map (Morphism.thm phi) raw_disc_defs;
49281
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   273
          val sel_defs = map (Morphism.thm phi) raw_sel_defs;
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   274
          val sel_defss = unflat_selss sel_defs;
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   275
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   276
          val discs0 = map (Morphism.term phi) raw_discs;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   277
          val selss0 = unflat_selss (map (Morphism.term phi) raw_sels);
49028
487427a02bee generate "disc_distinct" theorems
blanchet
parents: 49027
diff changeset
   278
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   279
          fun mk_disc_or_sel Ts c =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   280
            Term.subst_atomic_types (snd (Term.dest_Type (domain_type (fastype_of c))) ~~ Ts) c;
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   281
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   282
          val discs = map (mk_disc_or_sel As) discs0;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   283
          val selss = map (map (mk_disc_or_sel As)) selss0;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   284
        in
49285
036b833b99aa removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents: 49281
diff changeset
   285
          (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy')
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   286
        end;
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   287
49032
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   288
    fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p);
49029
f0ecfa9575a9 generate "disc_exhaust" property
blanchet
parents: 49028
diff changeset
   289
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   290
    val goal_exhaust =
49032
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   291
      let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (v, xctr)]) in
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   292
        fold_rev Logic.all [p, v] (mk_imp_p (map2 mk_prem xctrs xss))
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   293
      end;
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   294
49034
b77e1910af8a make parallel list indexing possible for inject theorems
blanchet
parents: 49033
diff changeset
   295
    val goal_injectss =
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   296
      let
49034
b77e1910af8a make parallel list indexing possible for inject theorems
blanchet
parents: 49033
diff changeset
   297
        fun mk_goal _ _ [] [] = []
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   298
          | mk_goal xctr yctr xs ys =
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   299
            [fold_rev Logic.all (xs @ ys) (mk_Trueprop_eq (HOLogic.mk_eq (xctr, yctr),
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   300
              Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys)))];
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   301
      in
49034
b77e1910af8a make parallel list indexing possible for inject theorems
blanchet
parents: 49033
diff changeset
   302
        map4 mk_goal xctrs yctrs xss yss
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   303
      end;
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   304
49048
4e0f0f98be02 rationalized data structure for distinctness theorems
blanchet
parents: 49046
diff changeset
   305
    val goal_half_distinctss =
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   306
      let
49203
262ab1ac38b9 repaired constant types
blanchet
parents: 49201
diff changeset
   307
        fun mk_goal ((xs, xc), (xs', xc')) =
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   308
          fold_rev Logic.all (xs @ xs')
49203
262ab1ac38b9 repaired constant types
blanchet
parents: 49201
diff changeset
   309
            (HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (xc, xc'))));
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   310
      in
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   311
        map (map mk_goal) (mk_half_pairss (xss ~~ xctrs))
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   312
      end;
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   313
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   314
    val goal_cases =
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   315
      map3 (fn xs => fn xctr => fn xf =>
49201
blanchet
parents: 49199
diff changeset
   316
        fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (fcase $ xctr, xf))) xss xctrs xfs;
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   317
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   318
    val goalss = [goal_exhaust] :: goal_injectss @ goal_half_distinctss @ [goal_cases];
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   319
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   320
    fun after_qed thmss lthy =
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   321
      let
49048
4e0f0f98be02 rationalized data structure for distinctness theorems
blanchet
parents: 49046
diff changeset
   322
        val ([exhaust_thm], (inject_thmss, (half_distinct_thmss, [case_thms]))) =
4e0f0f98be02 rationalized data structure for distinctness theorems
blanchet
parents: 49046
diff changeset
   323
          (hd thmss, apsnd (chop (n * n)) (chop n (tl thmss)));
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   324
49032
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   325
        val exhaust_thm' =
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   326
          let val Tinst = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As) in
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   327
            Drule.instantiate' [] [SOME (certify lthy v)]
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   328
              (Thm.instantiate (Tinst, []) (Drule.zero_var_indexes exhaust_thm))
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   329
          end;
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   330
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   331
        val exhaust_cases = map base_name_of_ctr ctrs;
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   332
49048
4e0f0f98be02 rationalized data structure for distinctness theorems
blanchet
parents: 49046
diff changeset
   333
        val other_half_distinct_thmss = map (map (fn thm => thm RS not_sym)) half_distinct_thmss;
4e0f0f98be02 rationalized data structure for distinctness theorems
blanchet
parents: 49046
diff changeset
   334
49052
3510b943dd5b optimized "mk_split_tac" + use "notes"
blanchet
parents: 49050
diff changeset
   335
        val (distinct_thmsss', distinct_thmsss) =
49048
4e0f0f98be02 rationalized data structure for distinctness theorems
blanchet
parents: 49046
diff changeset
   336
          map2 (map2 append) (Library.chop_groups n half_distinct_thmss)
49052
3510b943dd5b optimized "mk_split_tac" + use "notes"
blanchet
parents: 49050
diff changeset
   337
            (transpose (Library.chop_groups n other_half_distinct_thmss))
3510b943dd5b optimized "mk_split_tac" + use "notes"
blanchet
parents: 49050
diff changeset
   338
          |> `transpose;
49048
4e0f0f98be02 rationalized data structure for distinctness theorems
blanchet
parents: 49046
diff changeset
   339
        val distinct_thms = interleave (flat half_distinct_thmss) (flat other_half_distinct_thmss);
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   340
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   341
        val nchotomy_thm =
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   342
          let
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   343
            val goal =
49022
005ce926a932 define selectors and discriminators
blanchet
parents: 49020
diff changeset
   344
              HOLogic.mk_Trueprop (HOLogic.mk_all (fst v', snd v',
49029
f0ecfa9575a9 generate "disc_exhaust" property
blanchet
parents: 49028
diff changeset
   345
                Library.foldr1 HOLogic.mk_disj exist_xs_v_eq_ctrs));
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   346
          in
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   347
            Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm)
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   348
          end;
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   349
49281
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   350
        val (all_sel_thms, sel_thmss, disc_thms, discI_thms, disc_exclude_thms, disc_exhaust_thms,
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   351
             collapse_thms, case_eq_thms) =
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   352
          if no_dests then
49281
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   353
            ([], [], [], [], [], [], [], [])
49116
3d520eec2746 allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
blanchet
parents: 49114
diff changeset
   354
          else
3d520eec2746 allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
blanchet
parents: 49114
diff changeset
   355
            let
49281
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   356
              fun make_sel_thm case_thm sel_def = case_thm RS (sel_def RS trans);
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   357
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   358
              fun has_undefined_rhs thm =
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   359
                (case snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))) of
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   360
                  Const (@{const_name undefined}, _) => true
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   361
                | _ => false);
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   362
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   363
              val sel_thmss = map2 (map o make_sel_thm) case_thms sel_defss;
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   364
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   365
              val all_sel_thms =
49285
036b833b99aa removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents: 49281
diff changeset
   366
                (if all_sels_distinct andalso forall null sel_defaultss then
036b833b99aa removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents: 49281
diff changeset
   367
                   flat sel_thmss
036b833b99aa removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents: 49281
diff changeset
   368
                 else
036b833b99aa removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents: 49281
diff changeset
   369
                   map_product (fn s => fn c => make_sel_thm c s) sel_defs case_thms)
036b833b99aa removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents: 49281
diff changeset
   370
                |> filter_out has_undefined_rhs;
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   371
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   372
              fun mk_unique_disc_def () =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   373
                let
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   374
                  val m = the_single ms;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   375
                  val goal = mk_Trueprop_eq (mk_v_eq_v (), the_single exist_xs_v_eq_ctrs);
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   376
                in
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   377
                  Skip_Proof.prove lthy [] [] goal (fn _ => mk_unique_disc_def_tac m exhaust_thm')
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   378
                  |> singleton (Proof_Context.export names_lthy lthy)
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   379
                  |> Thm.close_derivation
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   380
                end;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   381
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   382
              fun mk_alternate_disc_def k =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   383
                let
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   384
                  val goal =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   385
                    mk_Trueprop_eq (alternate_disc_lhs (K (nth discs)) (3 - k),
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   386
                      nth exist_xs_v_eq_ctrs (k - 1));
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   387
                in
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   388
                  Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   389
                    mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k))
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   390
                      (nth distinct_thms (2 - k)) exhaust_thm')
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   391
                  |> singleton (Proof_Context.export names_lthy lthy)
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   392
                  |> Thm.close_derivation
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   393
                end;
49028
487427a02bee generate "disc_distinct" theorems
blanchet
parents: 49027
diff changeset
   394
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   395
              val has_alternate_disc_def =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   396
                exists (fn def => Thm.eq_thm_prop (def, alternate_disc_no_def)) disc_defs;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   397
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   398
              val disc_defs' =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   399
                map2 (fn k => fn def =>
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   400
                  if Thm.eq_thm_prop (def, unique_disc_no_def) then mk_unique_disc_def ()
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   401
                  else if Thm.eq_thm_prop (def, alternate_disc_no_def) then mk_alternate_disc_def k
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   402
                  else def) ks disc_defs;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   403
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   404
              val discD_thms = map (fn def => def RS iffD1) disc_defs';
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   405
              val discI_thms =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   406
                map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   407
                  disc_defs';
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   408
              val not_discI_thms =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   409
                map2 (fn m => fn def => funpow m (fn thm => allI RS thm)
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   410
                    (Local_Defs.unfold lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]})))
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   411
                  ms disc_defs';
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   412
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   413
              val (disc_thmss', disc_thmss) =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   414
                let
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   415
                  fun mk_thm discI _ [] = refl RS discI
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   416
                    | mk_thm _ not_discI [distinct] = distinct RS not_discI;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   417
                  fun mk_thms discI not_discI distinctss = map (mk_thm discI not_discI) distinctss;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   418
                in
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   419
                  map3 mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   420
                end;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   421
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   422
              val disc_thms = flat (map2 (fn true => K [] | false => I) no_discs disc_thmss);
49028
487427a02bee generate "disc_distinct" theorems
blanchet
parents: 49027
diff changeset
   423
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   424
              val disc_exclude_thms =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   425
                if has_alternate_disc_def then
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   426
                  []
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   427
                else
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   428
                  let
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   429
                    fun mk_goal [] = []
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   430
                      | mk_goal [((_, true), (_, true))] = []
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   431
                      | mk_goal [(((_, disc), _), ((_, disc'), _))] =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   432
                        [Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (betapply (disc, v)),
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   433
                           HOLogic.mk_Trueprop (HOLogic.mk_not (betapply (disc', v)))))];
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   434
                    fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac);
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   435
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   436
                    val infos = ms ~~ discD_thms ~~ discs ~~ no_discs;
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   437
                    val half_pairss = mk_half_pairss infos;
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   438
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   439
                    val goal_halvess = map mk_goal half_pairss;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   440
                    val half_thmss =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   441
                      map3 (fn [] => K (K []) | [goal] => fn [((((m, discD), _), _), _)] =>
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   442
                          fn disc_thm => [prove (mk_half_disc_exclude_tac m discD disc_thm) goal])
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   443
                        goal_halvess half_pairss (flat disc_thmss');
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   444
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   445
                    val goal_other_halvess = map (mk_goal o map swap) half_pairss;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   446
                    val other_half_thmss =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   447
                      map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   448
                        goal_other_halvess;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   449
                  in
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   450
                    interleave (flat half_thmss) (flat other_half_thmss)
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   451
                  end;
49028
487427a02bee generate "disc_distinct" theorems
blanchet
parents: 49027
diff changeset
   452
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   453
              val disc_exhaust_thms =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   454
                if has_alternate_disc_def orelse no_discs_at_all then
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   455
                  []
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   456
                else
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   457
                  let
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   458
                    fun mk_prem disc = mk_imp_p [HOLogic.mk_Trueprop (betapply (disc, v))];
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   459
                    val goal = fold_rev Logic.all [p, v] (mk_imp_p (map mk_prem discs));
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   460
                  in
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   461
                    [Skip_Proof.prove lthy [] [] goal (fn _ =>
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   462
                       mk_disc_exhaust_tac n exhaust_thm discI_thms)]
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   463
                  end;
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   464
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   465
              val collapse_thms =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   466
                if no_dests then
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   467
                  []
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   468
                else
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   469
                  let
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   470
                    fun mk_goal ctr disc sels =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   471
                      let
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   472
                        val prem = HOLogic.mk_Trueprop (betapply (disc, v));
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   473
                        val concl =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   474
                          mk_Trueprop_eq ((null sels ? swap)
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   475
                            (Term.list_comb (ctr, map ap_v sels), v));
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   476
                      in
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   477
                        if prem aconv concl then NONE
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   478
                        else SOME (Logic.all v (Logic.mk_implies (prem, concl)))
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   479
                      end;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   480
                    val goals = map3 mk_goal ctrs discs selss;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   481
                  in
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   482
                    map4 (fn m => fn discD => fn sel_thms => Option.map (fn goal =>
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   483
                      Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   484
                        mk_collapse_tac ctxt m discD sel_thms)
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   485
                      |> perhaps (try (fn thm => refl RS thm)))) ms discD_thms sel_thmss goals
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   486
                    |> map_filter I
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   487
                  end;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   488
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   489
              val case_eq_thms =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   490
                if no_dests then
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   491
                  []
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   492
                else
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   493
                  let
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   494
                    fun mk_body f sels = Term.list_comb (f, map ap_v sels);
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   495
                    val goal =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   496
                      mk_Trueprop_eq (fcase $ v, mk_IfN B (map ap_v discs) (map2 mk_body fs selss));
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   497
                  in
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   498
                    [Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   499
                      mk_case_eq_tac ctxt n exhaust_thm' case_thms disc_thmss' sel_thmss)]
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   500
                    |> Proof_Context.export names_lthy lthy
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   501
                  end;
49116
3d520eec2746 allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
blanchet
parents: 49114
diff changeset
   502
            in
49281
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   503
              (all_sel_thms, sel_thmss, disc_thms, discI_thms, disc_exclude_thms, disc_exhaust_thms,
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   504
               collapse_thms, case_eq_thms)
49116
3d520eec2746 allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
blanchet
parents: 49114
diff changeset
   505
            end;
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   506
49033
23ef2d429931 generate "weak_case_cong" property
blanchet
parents: 49032
diff changeset
   507
        val (case_cong_thm, weak_case_cong_thm) =
49032
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   508
          let
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   509
            fun mk_prem xctr xs f g =
49045
7d9631754bba minor fixes (for compatibility with existing datatype package)
blanchet
parents: 49044
diff changeset
   510
              fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (w, xctr),
49032
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   511
                mk_Trueprop_eq (f, g)));
49033
23ef2d429931 generate "weak_case_cong" property
blanchet
parents: 49032
diff changeset
   512
23ef2d429931 generate "weak_case_cong" property
blanchet
parents: 49032
diff changeset
   513
            val v_eq_w = mk_Trueprop_eq (v, w);
49032
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   514
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   515
            val goal =
49033
23ef2d429931 generate "weak_case_cong" property
blanchet
parents: 49032
diff changeset
   516
              Logic.list_implies (v_eq_w :: map4 mk_prem xctrs xss fs gs,
49201
blanchet
parents: 49199
diff changeset
   517
                 mk_Trueprop_eq (fcase $ v, gcase $ w));
blanchet
parents: 49199
diff changeset
   518
            val goal_weak = Logic.mk_implies (v_eq_w, mk_Trueprop_eq (fcase $ v, fcase $ w));
49032
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   519
          in
49049
blanchet
parents: 49048
diff changeset
   520
            (Skip_Proof.prove lthy [] [] goal (fn _ => mk_case_cong_tac exhaust_thm' case_thms),
49033
23ef2d429931 generate "weak_case_cong" property
blanchet
parents: 49032
diff changeset
   521
             Skip_Proof.prove lthy [] [] goal_weak (K (etac arg_cong 1)))
23ef2d429931 generate "weak_case_cong" property
blanchet
parents: 49032
diff changeset
   522
            |> pairself (singleton (Proof_Context.export names_lthy lthy))
49032
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   523
          end;
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   524
49044
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   525
        val (split_thm, split_asm_thm) =
49043
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   526
          let
49044
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   527
            fun mk_conjunct xctr xs f_xs =
49043
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   528
              list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (v, xctr), q $ f_xs));
49044
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   529
            fun mk_disjunct xctr xs f_xs =
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   530
              list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (v, xctr),
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   531
                HOLogic.mk_not (q $ f_xs)));
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   532
49201
blanchet
parents: 49199
diff changeset
   533
            val lhs = q $ (fcase $ v);
49044
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   534
49043
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   535
            val goal =
49044
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   536
              mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs));
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   537
            val goal_asm =
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   538
              mk_Trueprop_eq (lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   539
                (map3 mk_disjunct xctrs xss xfs)));
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   540
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   541
            val split_thm =
49049
blanchet
parents: 49048
diff changeset
   542
              Skip_Proof.prove lthy [] [] goal
49052
3510b943dd5b optimized "mk_split_tac" + use "notes"
blanchet
parents: 49050
diff changeset
   543
                (fn _ => mk_split_tac exhaust_thm' case_thms inject_thmss distinct_thmsss)
49044
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   544
              |> singleton (Proof_Context.export names_lthy lthy)
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   545
            val split_asm_thm =
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   546
              Skip_Proof.prove lthy [] [] goal_asm (fn {context = ctxt, ...} =>
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   547
                mk_split_asm_tac ctxt split_thm)
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   548
              |> singleton (Proof_Context.export names_lthy lthy)
49043
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   549
          in
49044
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   550
            (split_thm, split_asm_thm)
49043
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   551
          end;
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   552
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   553
        val cases_type_attr = Attrib.internal (K (Induct.cases_type dataT_name));
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   554
        val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   555
49052
3510b943dd5b optimized "mk_split_tac" + use "notes"
blanchet
parents: 49050
diff changeset
   556
        val notes =
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   557
          [(case_congN, [case_cong_thm], []),
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   558
           (case_eqN, case_eq_thms, []),
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   559
           (casesN, case_thms, simp_attrs),
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   560
           (collapseN, collapse_thms, simp_attrs),
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   561
           (discsN, disc_thms, simp_attrs),
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   562
           (disc_excludeN, disc_exclude_thms, []),
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   563
           (disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]),
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   564
           (distinctN, distinct_thms, simp_attrs @ induct_simp_attrs),
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   565
           (exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]),
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   566
           (injectN, flat inject_thmss, iff_attrs @ induct_simp_attrs),
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   567
           (nchotomyN, [nchotomy_thm], []),
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   568
           (selsN, all_sel_thms, simp_attrs),
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   569
           (splitN, [split_thm], []),
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   570
           (split_asmN, [split_asm_thm], []),
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   571
           (weak_case_cong_thmsN, [weak_case_cong_thm], cong_attrs)]
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   572
          |> filter_out (null o #2)
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   573
          |> map (fn (thmN, thms, attrs) =>
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   574
            ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs), [(thms, [])]));
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   575
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   576
        val notes' =
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   577
          [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)]
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   578
          |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   579
      in
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   580
        ((selss, discI_thms, sel_thmss), lthy |> Local_Theory.notes (notes' @ notes) |> snd)
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   581
      end;
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   582
  in
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   583
    (goalss, after_qed, lthy')
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   584
  end;
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   585
49199
7c9a3c67c55d added high-level recursor, not yet curried
blanchet
parents: 49174
diff changeset
   586
fun wrap_datatype tacss = (fn (goalss, after_qed, lthy) =>
49111
9d511132394e export "wrap" function
blanchet
parents: 49075
diff changeset
   587
  map2 (map2 (Skip_Proof.prove lthy [] [])) goalss tacss
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   588
  |> (fn thms => after_qed thms lthy)) oo prepare_wrap_datatype (K I);
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   589
49297
47fbf2e3e89c provide a programmatic interface for FP sugar
blanchet
parents: 49286
diff changeset
   590
val wrap_datatype_cmd = (fn (goalss, after_qed, lthy) =>
47fbf2e3e89c provide a programmatic interface for FP sugar
blanchet
parents: 49286
diff changeset
   591
  Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
47fbf2e3e89c provide a programmatic interface for FP sugar
blanchet
parents: 49286
diff changeset
   592
  prepare_wrap_datatype Syntax.read_term;
47fbf2e3e89c provide a programmatic interface for FP sugar
blanchet
parents: 49286
diff changeset
   593
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   594
fun parse_bracket_list parser = @{keyword "["} |-- Parse.list parser --|  @{keyword "]"};
49111
9d511132394e export "wrap" function
blanchet
parents: 49075
diff changeset
   595
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   596
val parse_bindings = parse_bracket_list Parse.binding;
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   597
val parse_bindingss = parse_bracket_list parse_bindings;
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   598
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   599
val parse_bound_term = (Parse.binding --| @{keyword ":"}) -- Parse.term;
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   600
val parse_bound_terms = parse_bracket_list parse_bound_term;
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   601
val parse_bound_termss = parse_bracket_list parse_bound_terms;
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   602
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   603
val parse_wrap_options =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   604
  Scan.optional (@{keyword "("} |-- (@{keyword "no_dests"} >> K true) --| @{keyword ")"}) false;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   605
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   606
val _ =
49074
d8af889dcbe3 renamed three BNF/(co)datatype-related commands
blanchet
parents: 49057
diff changeset
   607
  Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wraps an existing datatype"
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   608
    ((parse_wrap_options -- (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) --
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   609
      Parse.term -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss --
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   610
        Scan.optional parse_bound_termss []) ([], [])) ([], ([], [])))
49199
7c9a3c67c55d added high-level recursor, not yet curried
blanchet
parents: 49174
diff changeset
   611
     >> wrap_datatype_cmd);
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   612
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   613
end;