src/HOL/BNF/Tools/bnf_wrap.ML
author traytel
Sun, 30 Sep 2012 12:08:16 +0200
changeset 49667 44d85dc8ca08
parent 49633 5b5450bc544c
child 49668 0209087a14d0
permissions -rw-r--r--
use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
49509
163914705f8d renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents: 49504
diff changeset
     1
(*  Title:      HOL/BNF/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
49633
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
    10
  val rep_compat_prefix: string
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
    11
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49536
diff changeset
    12
  val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49536
diff changeset
    13
  val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49536
diff changeset
    14
49203
262ab1ac38b9 repaired constant types
blanchet
parents: 49201
diff changeset
    15
  val mk_ctr: typ list -> term -> term
49484
0194a18f80cf finished "disc_coiter_iff" etc. generation
blanchet
parents: 49478
diff changeset
    16
  val mk_disc_or_sel: typ list -> term -> term
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49536
diff changeset
    17
49622
a93f976c3307 use a nicer scheme to indexify names
blanchet
parents: 49619
diff changeset
    18
  val name_of_ctr: term -> string
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49536
diff changeset
    19
49199
7c9a3c67c55d added high-level recursor, not yet curried
blanchet
parents: 49174
diff changeset
    20
  val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list ->
49633
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
    21
    (((bool * bool) * term list) * term) *
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
    22
      (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
49591
91b228e26348 generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents: 49586
diff changeset
    23
    (term list * term list list * thm * thm list * thm list * thm list * thm list list * thm list *
49484
0194a18f80cf finished "disc_coiter_iff" etc. generation
blanchet
parents: 49478
diff changeset
    24
     thm list list) * local_theory
49633
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
    25
  val parse_wrap_options: (bool * bool) parser
49286
dde4967c9233 added "defaults" option
blanchet
parents: 49285
diff changeset
    26
  val parse_bound_term: (binding * string) parser
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
    27
end;
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
    28
49074
d8af889dcbe3 renamed three BNF/(co)datatype-related commands
blanchet
parents: 49057
diff changeset
    29
structure BNF_Wrap : BNF_WRAP =
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
    30
struct
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
    31
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
    32
open BNF_Util
49074
d8af889dcbe3 renamed three BNF/(co)datatype-related commands
blanchet
parents: 49057
diff changeset
    33
open BNF_Wrap_Tactics
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
    34
49633
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
    35
val rep_compat_prefix = "new";
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
    36
49223
blanchet
parents: 49210
diff changeset
    37
val isN = "is_";
blanchet
parents: 49210
diff changeset
    38
val unN = "un_";
blanchet
parents: 49210
diff changeset
    39
fun mk_unN 1 1 suf = unN ^ suf
blanchet
parents: 49210
diff changeset
    40
  | 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
    41
49594
55e798614c45 tweaked theorem names (in particular, dropped s's)
blanchet
parents: 49591
diff changeset
    42
val caseN = "case";
49054
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
    43
val case_congN = "case_cong";
49594
55e798614c45 tweaked theorem names (in particular, dropped s's)
blanchet
parents: 49591
diff changeset
    44
val case_convN = "case_conv";
49118
b815fa776b91 renamed theorem
blanchet
parents: 49117
diff changeset
    45
val collapseN = "collapse";
49122
83515378d4d7 renamed "disc_exclus" theorem to "disc_exclude"
blanchet
parents: 49121
diff changeset
    46
val disc_excludeN = "disc_exclude";
49054
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
    47
val disc_exhaustN = "disc_exhaust";
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
    48
val discsN = "discs";
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
    49
val distinctN = "distinct";
49075
ed769978dc8d rearrange dependencies
blanchet
parents: 49074
diff changeset
    50
val exhaustN = "exhaust";
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
    51
val expandN = "expand";
49075
ed769978dc8d rearrange dependencies
blanchet
parents: 49074
diff changeset
    52
val injectN = "inject";
ed769978dc8d rearrange dependencies
blanchet
parents: 49074
diff changeset
    53
val nchotomyN = "nchotomy";
49054
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
    54
val selsN = "sels";
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
    55
val splitN = "split";
49633
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
    56
val splitsN = "splits";
49054
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
    57
val split_asmN = "split_asm";
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
    58
val weak_case_cong_thmsN = "weak_case_cong";
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
    59
49336
blanchet
parents: 49311
diff changeset
    60
val std_binding = @{binding _};
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
    61
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
    62
val induct_simp_attrs = @{attributes [induct_simp]};
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
    63
val cong_attrs = @{attributes [cong]};
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
    64
val iff_attrs = @{attributes [iff]};
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
    65
val safe_elim_attrs = @{attributes [elim!]};
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
    66
val simp_attrs = @{attributes [simp]};
49046
3c5eba97d93a allow default names for selectors via wildcard (_) + fix wrong index (k)
blanchet
parents: 49045
diff changeset
    67
49056
blanchet
parents: 49055
diff changeset
    68
fun pad_list x n xs = xs @ replicate (n - length xs) x;
blanchet
parents: 49055
diff changeset
    69
49259
b21c03c7a097 minor optimization
blanchet
parents: 49258
diff changeset
    70
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
    71
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49536
diff changeset
    72
fun mk_half_pairss' _ ([], []) = []
49591
91b228e26348 generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents: 49586
diff changeset
    73
  | mk_half_pairss' indent (x :: xs, _ :: ys) =
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49536
diff changeset
    74
    indent @ fold_rev (cons o single o pair x) ys (mk_half_pairss' ([] :: indent) (xs, ys));
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
    75
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49536
diff changeset
    76
fun mk_half_pairss p = mk_half_pairss' [[]] p;
49027
fc3b9b49c92d added discriminator theorems
blanchet
parents: 49025
diff changeset
    77
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
    78
fun join_halves n half_xss other_half_xss =
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
    79
  let
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
    80
    val xsss =
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
    81
      map2 (map2 append) (Library.chop_groups n half_xss)
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
    82
        (transpose (Library.chop_groups n other_half_xss))
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
    83
    val xs = interleave (flat half_xss) (flat other_half_xss);
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49536
diff changeset
    84
  in (xs, xsss) end;
49027
fc3b9b49c92d added discriminator theorems
blanchet
parents: 49025
diff changeset
    85
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
    86
fun mk_undefined T = Const (@{const_name undefined}, T);
49055
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
    87
49500
blanchet
parents: 49498
diff changeset
    88
fun mk_ctr Ts t =
blanchet
parents: 49498
diff changeset
    89
  let val Type (_, Ts0) = body_type (fastype_of t) in
blanchet
parents: 49498
diff changeset
    90
    Term.subst_atomic_types (Ts0 ~~ Ts) t
49203
262ab1ac38b9 repaired constant types
blanchet
parents: 49201
diff changeset
    91
  end;
262ab1ac38b9 repaired constant types
blanchet
parents: 49201
diff changeset
    92
49484
0194a18f80cf finished "disc_coiter_iff" etc. generation
blanchet
parents: 49478
diff changeset
    93
fun mk_disc_or_sel Ts t =
0194a18f80cf finished "disc_coiter_iff" etc. generation
blanchet
parents: 49478
diff changeset
    94
  Term.subst_atomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
0194a18f80cf finished "disc_coiter_iff" etc. generation
blanchet
parents: 49478
diff changeset
    95
49536
898aea2e7a94 started work on generation of "rel" theorems
blanchet
parents: 49510
diff changeset
    96
fun mk_case Ts T t =
898aea2e7a94 started work on generation of "rel" theorems
blanchet
parents: 49510
diff changeset
    97
  let val (Type (_, Ts0), body) = strip_type (fastype_of t) |>> List.last in
898aea2e7a94 started work on generation of "rel" theorems
blanchet
parents: 49510
diff changeset
    98
    Term.subst_atomic_types ((body, T) :: (Ts0 ~~ Ts)) t
898aea2e7a94 started work on generation of "rel" theorems
blanchet
parents: 49510
diff changeset
    99
  end;
898aea2e7a94 started work on generation of "rel" theorems
blanchet
parents: 49510
diff changeset
   100
49622
a93f976c3307 use a nicer scheme to indexify names
blanchet
parents: 49619
diff changeset
   101
fun name_of_ctr c =
a93f976c3307 use a nicer scheme to indexify names
blanchet
parents: 49619
diff changeset
   102
  (case head_of c of
a93f976c3307 use a nicer scheme to indexify names
blanchet
parents: 49619
diff changeset
   103
    Const (s, _) => s
a93f976c3307 use a nicer scheme to indexify names
blanchet
parents: 49619
diff changeset
   104
  | Free (s, _) => s
a93f976c3307 use a nicer scheme to indexify names
blanchet
parents: 49619
diff changeset
   105
  | _ => error "Cannot extract name of constructor");
a93f976c3307 use a nicer scheme to indexify names
blanchet
parents: 49619
diff changeset
   106
a93f976c3307 use a nicer scheme to indexify names
blanchet
parents: 49619
diff changeset
   107
val base_name_of_ctr = Long_Name.base_name o name_of_ctr;
49046
3c5eba97d93a allow default names for selectors via wildcard (_) + fix wrong index (k)
blanchet
parents: 49045
diff changeset
   108
49437
c139da00fb4a register induct attributes
blanchet
parents: 49434
diff changeset
   109
fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
c139da00fb4a register induct attributes
blanchet
parents: 49434
diff changeset
   110
49633
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
   111
fun prepare_wrap_datatype prep_term ((((no_dests, rep_compat), raw_ctrs), raw_case),
49336
blanchet
parents: 49311
diff changeset
   112
    (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   113
  let
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   114
    (* TODO: sanity checks on arguments *)
49113
ef3eea7ae251 tuned TODOs
blanchet
parents: 49111
diff changeset
   115
    (* TODO: case syntax *)
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   116
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   117
    val n = length raw_ctrs;
49054
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
   118
    val ks = 1 upto n;
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
   119
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   120
    val _ = if n > 0 then () else error "No constructors specified";
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   121
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   122
    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
   123
    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
   124
    val sel_defaultss =
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   125
      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
   126
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   127
    val Type (dataT_name, As0) = body_type (fastype_of (hd ctrs0));
49302
f5bd87aac224 added optional qualifiers for constructors and destructors, similarly to the old package
blanchet
parents: 49300
diff changeset
   128
    val data_b = Binding.qualified_name dataT_name;
49498
acc583e14167 tuned variable names
blanchet
parents: 49486
diff changeset
   129
    val data_b_name = Binding.name_of data_b;
49055
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   130
49633
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
   131
    fun qualify mandatory =
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
   132
      Binding.qualify mandatory data_b_name o
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
   133
      (rep_compat ? Binding.qualify false rep_compat_prefix);
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
   134
49055
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   135
    val (As, B) =
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   136
      no_defs_lthy
49298
36e551d3af3b support for sort constraints in new (co)data commands
blanchet
parents: 49297
diff changeset
   137
      |> mk_TFrees' (map Type.sort_of_atyp As0)
49055
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   138
      ||> the_single o fst o mk_TFrees 1;
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   139
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   140
    val dataT = Type (dataT_name, As);
49055
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   141
    val ctrs = map (mk_ctr As) ctrs0;
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   142
    val ctr_Tss = map (binder_types o fastype_of) ctrs;
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   143
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   144
    val ms = map length ctr_Tss;
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   145
49434
433dc7e028c8 separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)
traytel
parents: 49364
diff changeset
   146
    val raw_disc_bindings' = pad_list Binding.empty n raw_disc_bindings;
49120
7f8e69fc6ac9 smarter "*" syntax -- fallback on "_" if "*" is impossible
blanchet
parents: 49119
diff changeset
   147
49174
41790d616f63 by default, only generate one discriminator for a two-value datatype
blanchet
parents: 49157
diff changeset
   148
    fun can_really_rely_on_disc k =
49434
433dc7e028c8 separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)
traytel
parents: 49364
diff changeset
   149
      not (Binding.eq_name (nth raw_disc_bindings' (k - 1), Binding.empty)) orelse
433dc7e028c8 separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)
traytel
parents: 49364
diff changeset
   150
      nth ms (k - 1) = 0;
49174
41790d616f63 by default, only generate one discriminator for a two-value datatype
blanchet
parents: 49157
diff changeset
   151
    fun can_rely_on_disc k =
41790d616f63 by default, only generate one discriminator for a two-value datatype
blanchet
parents: 49157
diff changeset
   152
      can_really_rely_on_disc k orelse (k = 1 andalso not (can_really_rely_on_disc 2));
49336
blanchet
parents: 49311
diff changeset
   153
    fun can_omit_disc_binding k m =
49174
41790d616f63 by default, only generate one discriminator for a two-value datatype
blanchet
parents: 49157
diff changeset
   154
      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
   155
49633
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
   156
    val std_disc_binding = qualify false o Binding.name o prefix isN o base_name_of_ctr;
49120
7f8e69fc6ac9 smarter "*" syntax -- fallback on "_" if "*" is impossible
blanchet
parents: 49119
diff changeset
   157
49336
blanchet
parents: 49311
diff changeset
   158
    val disc_bindings =
blanchet
parents: 49311
diff changeset
   159
      raw_disc_bindings'
49120
7f8e69fc6ac9 smarter "*" syntax -- fallback on "_" if "*" is impossible
blanchet
parents: 49119
diff changeset
   160
      |> map4 (fn k => fn m => fn ctr => fn disc =>
49633
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
   161
        Option.map (qualify false)
49434
433dc7e028c8 separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)
traytel
parents: 49364
diff changeset
   162
          (if Binding.eq_name (disc, Binding.empty) then
49336
blanchet
parents: 49311
diff changeset
   163
             if can_omit_disc_binding k m then NONE else SOME (std_disc_binding ctr)
blanchet
parents: 49311
diff changeset
   164
           else if Binding.eq_name (disc, std_binding) then
blanchet
parents: 49311
diff changeset
   165
             SOME (std_disc_binding ctr)
49302
f5bd87aac224 added optional qualifiers for constructors and destructors, similarly to the old package
blanchet
parents: 49300
diff changeset
   166
           else
f5bd87aac224 added optional qualifiers for constructors and destructors, similarly to the old package
blanchet
parents: 49300
diff changeset
   167
             SOME disc)) ks ms ctrs0;
49056
blanchet
parents: 49055
diff changeset
   168
49336
blanchet
parents: 49311
diff changeset
   169
    val no_discs = map is_none disc_bindings;
49137
5c8fefe0f103 fixed bugs in one-constructor case
blanchet
parents: 49136
diff changeset
   170
    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
   171
49336
blanchet
parents: 49311
diff changeset
   172
    fun std_sel_binding 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
   173
49336
blanchet
parents: 49311
diff changeset
   174
    val sel_bindingss =
blanchet
parents: 49311
diff changeset
   175
      pad_list [] n raw_sel_bindingss
49056
blanchet
parents: 49055
diff changeset
   176
      |> map3 (fn ctr => fn m => map2 (fn l => fn sel =>
49633
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
   177
        qualify false
49434
433dc7e028c8 separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)
traytel
parents: 49364
diff changeset
   178
          (if Binding.eq_name (sel, Binding.empty) orelse Binding.eq_name (sel, std_binding) then
49336
blanchet
parents: 49311
diff changeset
   179
            std_sel_binding m l ctr
49302
f5bd87aac224 added optional qualifiers for constructors and destructors, similarly to the old package
blanchet
parents: 49300
diff changeset
   180
          else
49434
433dc7e028c8 separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)
traytel
parents: 49364
diff changeset
   181
            sel)) (1 upto m) o pad_list Binding.empty m) ctrs0 ms;
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   182
49536
898aea2e7a94 started work on generation of "rel" theorems
blanchet
parents: 49510
diff changeset
   183
    val casex = mk_case As B case0;
49201
blanchet
parents: 49199
diff changeset
   184
    val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
49043
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   185
49498
acc583e14167 tuned variable names
blanchet
parents: 49486
diff changeset
   186
    val (((((((xss, xss'), yss), fs), gs), [u', v']), (p, p')), names_lthy) = no_defs_lthy |>
49364
838b5e8ede73 allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents: 49336
diff changeset
   187
      mk_Freess' "x" ctr_Tss
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   188
      ||>> mk_Freess "y" ctr_Tss
49201
blanchet
parents: 49199
diff changeset
   189
      ||>> mk_Frees "f" case_Ts
blanchet
parents: 49199
diff changeset
   190
      ||>> mk_Frees "g" case_Ts
49498
acc583e14167 tuned variable names
blanchet
parents: 49486
diff changeset
   191
      ||>> (apfst (map (rpair dataT)) oo Variable.variant_fixes) [data_b_name, data_b_name ^ "'"]
49043
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   192
      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT;
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   193
49498
acc583e14167 tuned variable names
blanchet
parents: 49486
diff changeset
   194
    val u = Free u';
acc583e14167 tuned variable names
blanchet
parents: 49486
diff changeset
   195
    val v = Free v';
49463
83ac281bcdc2 provide predicator, define relator
blanchet
parents: 49458
diff changeset
   196
    val q = Free (fst p', mk_pred1T B);
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   197
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   198
    val xctrs = map2 (curry Term.list_comb) ctrs xss;
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   199
    val yctrs = map2 (curry Term.list_comb) ctrs yss;
49032
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   200
49043
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   201
    val xfs = map2 (curry Term.list_comb) fs xss;
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   202
    val xgs = map2 (curry Term.list_comb) gs xss;
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   203
49437
c139da00fb4a register induct attributes
blanchet
parents: 49434
diff changeset
   204
    val eta_fs = map2 eta_expand_arg xss xfs;
c139da00fb4a register induct attributes
blanchet
parents: 49434
diff changeset
   205
    val eta_gs = map2 eta_expand_arg xss xgs;
49043
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   206
49201
blanchet
parents: 49199
diff changeset
   207
    val fcase = Term.list_comb (casex, eta_fs);
blanchet
parents: 49199
diff changeset
   208
    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
   209
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   210
    val ufcase = fcase $ u;
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   211
    val vfcase = fcase $ v;
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   212
    val vgcase = gcase $ v;
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   213
49591
91b228e26348 generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents: 49586
diff changeset
   214
    fun mk_uu_eq () = HOLogic.mk_eq (u, u);
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   215
49591
91b228e26348 generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents: 49586
diff changeset
   216
    val uv_eq = mk_Trueprop_eq (u, v);
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   217
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   218
    val exist_xs_u_eq_ctrs =
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   219
      map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (u, xctr))) xctrs xss;
49022
005ce926a932 define selectors and discriminators
blanchet
parents: 49020
diff changeset
   220
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   221
    val unique_disc_no_def = TrueI; (*arbitrary marker*)
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   222
    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
   223
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   224
    fun alternate_disc_lhs get_udisc 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
   225
      HOLogic.mk_not
49336
blanchet
parents: 49311
diff changeset
   226
        (case nth disc_bindings (k - 1) of
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   227
          NONE => nth exist_xs_u_eq_ctrs (k - 1)
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   228
        | SOME b => get_udisc b (k - 1));
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
   229
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   230
    val (all_sels_distinct, discs, selss, udiscs, uselss, vdiscs, vselss, disc_defs, sel_defs,
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   231
         sel_defss, lthy') =
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   232
      if no_dests then
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   233
        (true, [], [], [], [], [], [], [], [], [], no_defs_lthy)
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   234
      else
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   235
        let
49463
83ac281bcdc2 provide predicator, define relator
blanchet
parents: 49458
diff changeset
   236
          fun disc_free b = Free (Binding.name_of b, mk_pred1T dataT);
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   237
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   238
          fun disc_spec b exist_xs_u_eq_ctr = mk_Trueprop_eq (disc_free b $ u, exist_xs_u_eq_ctr);
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   239
49500
blanchet
parents: 49498
diff changeset
   240
          fun alternate_disc k =
blanchet
parents: 49498
diff changeset
   241
            Term.lambda u (alternate_disc_lhs (K o rapp u o disc_free) (3 - k));
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   242
49364
838b5e8ede73 allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents: 49336
diff changeset
   243
          fun mk_default T t =
838b5e8ede73 allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents: 49336
diff changeset
   244
            let
838b5e8ede73 allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents: 49336
diff changeset
   245
              val Ts0 = map TFree (Term.add_tfreesT (fastype_of t) []);
838b5e8ede73 allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents: 49336
diff changeset
   246
              val Ts = map TFree (Term.add_tfreesT T []);
838b5e8ede73 allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents: 49336
diff changeset
   247
            in Term.subst_atomic_types (Ts0 ~~ Ts) t end;
838b5e8ede73 allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents: 49336
diff changeset
   248
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   249
          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
   250
            map2 (fn Ts => fn k =>
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   251
              (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
   252
                NONE =>
49364
838b5e8ede73 allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents: 49336
diff changeset
   253
                (case AList.lookup Binding.eq_name (rev (nth sel_defaultss (k - 1))) b of
838b5e8ede73 allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents: 49336
diff changeset
   254
                  NONE => fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T)
838b5e8ede73 allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents: 49336
diff changeset
   255
                | SOME t => mk_default (Ts ---> T) t)
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   256
              | 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
   257
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   258
          fun sel_spec b proto_sels =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   259
            let
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   260
              val _ =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   261
                (case duplicates (op =) (map fst proto_sels) of
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   262
                   k :: _ => error ("Duplicate selector name " ^ quote (Binding.name_of b) ^
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   263
                     " for constructor " ^
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   264
                     quote (Syntax.string_of_term no_defs_lthy (nth ctrs (k - 1))))
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   265
                 | [] => ())
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   266
              val T =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   267
                (case distinct (op =) (map (fastype_of o snd o snd) proto_sels) of
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   268
                  [T] => T
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   269
                | T :: T' :: _ => error ("Inconsistent range type for selector " ^
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   270
                    quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   271
                    " vs. " ^ quote (Syntax.string_of_typ no_defs_lthy T')));
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   272
            in
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   273
              mk_Trueprop_eq (Free (Binding.name_of b, dataT --> T) $ u,
49536
898aea2e7a94 started work on generation of "rel" theorems
blanchet
parents: 49510
diff changeset
   274
                Term.list_comb (mk_case As T case0, mk_sel_case_args b proto_sels T) $ u)
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   275
            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
   276
49336
blanchet
parents: 49311
diff changeset
   277
          val sel_bindings = flat sel_bindingss;
blanchet
parents: 49311
diff changeset
   278
          val uniq_sel_bindings = distinct Binding.eq_name sel_bindings;
blanchet
parents: 49311
diff changeset
   279
          val all_sels_distinct = (length uniq_sel_bindings = length sel_bindings);
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
   280
49336
blanchet
parents: 49311
diff changeset
   281
          val sel_binding_index =
blanchet
parents: 49311
diff changeset
   282
            if all_sels_distinct then 1 upto length sel_bindings
blanchet
parents: 49311
diff changeset
   283
            else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) sel_bindings;
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
   284
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
          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
   286
          val sel_infos =
49336
blanchet
parents: 49311
diff changeset
   287
            AList.group (op =) (sel_binding_index ~~ proto_sels)
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
   288
            |> sort (int_ord o pairself fst)
49336
blanchet
parents: 49311
diff changeset
   289
            |> map snd |> curry (op ~~) uniq_sel_bindings;
blanchet
parents: 49311
diff changeset
   290
          val sel_bindings = map fst sel_infos;
49258
84f13469d7f0 allow same selector name for several constructors
blanchet
parents: 49257
diff changeset
   291
49336
blanchet
parents: 49311
diff changeset
   292
          fun unflat_selss xs = unflat_lookup Binding.eq_name sel_bindings xs sel_bindingss;
49258
84f13469d7f0 allow same selector name for several constructors
blanchet
parents: 49257
diff changeset
   293
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   294
          val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   295
            no_defs_lthy
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   296
            |> apfst split_list o fold_map4 (fn k => fn m => fn exist_xs_u_eq_ctr =>
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   297
              fn NONE =>
49591
91b228e26348 generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents: 49586
diff changeset
   298
                 if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def)
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   299
                 else if m = 0 then pair (Term.lambda u exist_xs_u_eq_ctr, refl)
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   300
                 else pair (alternate_disc k, alternate_disc_no_def)
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   301
               | SOME b => Specification.definition (SOME (b, NONE, NoSyn),
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   302
                   ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr)) #>> apsnd snd)
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   303
              ks ms exist_xs_u_eq_ctrs disc_bindings
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   304
            ||>> apfst split_list o fold_map (fn (b, proto_sels) =>
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   305
              Specification.definition (SOME (b, NONE, NoSyn),
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   306
                ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   307
            ||> `Local_Theory.restore;
49022
005ce926a932 define selectors and discriminators
blanchet
parents: 49020
diff changeset
   308
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   309
          val phi = Proof_Context.export_morphism lthy lthy';
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   310
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   311
          val disc_defs = map (Morphism.thm phi) raw_disc_defs;
49281
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   312
          val sel_defs = map (Morphism.thm phi) raw_sel_defs;
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   313
          val sel_defss = unflat_selss sel_defs;
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   314
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   315
          val discs0 = map (Morphism.term phi) raw_discs;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   316
          val selss0 = unflat_selss (map (Morphism.term phi) raw_sels);
49028
487427a02bee generate "disc_distinct" theorems
blanchet
parents: 49027
diff changeset
   317
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   318
          val discs = map (mk_disc_or_sel As) discs0;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   319
          val selss = map (map (mk_disc_or_sel As)) selss0;
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   320
49500
blanchet
parents: 49498
diff changeset
   321
          val udiscs = map (rapp u) discs;
blanchet
parents: 49498
diff changeset
   322
          val uselss = map (map (rapp u)) selss;
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   323
49500
blanchet
parents: 49498
diff changeset
   324
          val vdiscs = map (rapp v) discs;
blanchet
parents: 49498
diff changeset
   325
          val vselss = map (map (rapp v)) selss;
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   326
        in
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   327
          (all_sels_distinct, discs, selss, udiscs, uselss, vdiscs, vselss, disc_defs, sel_defs,
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   328
           sel_defss, lthy')
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   329
        end;
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   330
49032
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   331
    fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p);
49029
f0ecfa9575a9 generate "disc_exhaust" property
blanchet
parents: 49028
diff changeset
   332
49458
blanchet
parents: 49438
diff changeset
   333
    val exhaust_goal =
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   334
      let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (u, xctr)]) in
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   335
        fold_rev Logic.all [p, u] (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
   336
      end;
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   337
49484
0194a18f80cf finished "disc_coiter_iff" etc. generation
blanchet
parents: 49478
diff changeset
   338
    val inject_goalss =
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   339
      let
49034
b77e1910af8a make parallel list indexing possible for inject theorems
blanchet
parents: 49033
diff changeset
   340
        fun mk_goal _ _ [] [] = []
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   341
          | mk_goal xctr yctr xs ys =
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   342
            [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
   343
              Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys)))];
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   344
      in
49034
b77e1910af8a make parallel list indexing possible for inject theorems
blanchet
parents: 49033
diff changeset
   345
        map4 mk_goal xctrs yctrs xss yss
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   346
      end;
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   347
49484
0194a18f80cf finished "disc_coiter_iff" etc. generation
blanchet
parents: 49478
diff changeset
   348
    val half_distinct_goalss =
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   349
      let
49203
262ab1ac38b9 repaired constant types
blanchet
parents: 49201
diff changeset
   350
        fun mk_goal ((xs, xc), (xs', xc')) =
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   351
          fold_rev Logic.all (xs @ xs')
49203
262ab1ac38b9 repaired constant types
blanchet
parents: 49201
diff changeset
   352
            (HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (xc, xc'))));
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   353
      in
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49536
diff changeset
   354
        map (map mk_goal) (mk_half_pairss (`I (xss ~~ xctrs)))
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   355
      end;
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   356
49458
blanchet
parents: 49438
diff changeset
   357
    val cases_goal =
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   358
      map3 (fn xs => fn xctr => fn xf =>
49201
blanchet
parents: 49199
diff changeset
   359
        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
   360
49484
0194a18f80cf finished "disc_coiter_iff" etc. generation
blanchet
parents: 49478
diff changeset
   361
    val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss @ [cases_goal];
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   362
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   363
    fun after_qed thmss lthy =
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   364
      let
49048
4e0f0f98be02 rationalized data structure for distinctness theorems
blanchet
parents: 49046
diff changeset
   365
        val ([exhaust_thm], (inject_thmss, (half_distinct_thmss, [case_thms]))) =
4e0f0f98be02 rationalized data structure for distinctness theorems
blanchet
parents: 49046
diff changeset
   366
          (hd thmss, apsnd (chop (n * n)) (chop n (tl thmss)));
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   367
49438
5bc80d96241e group "simps" together
blanchet
parents: 49437
diff changeset
   368
        val inject_thms = flat inject_thmss;
5bc80d96241e group "simps" together
blanchet
parents: 49437
diff changeset
   369
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   370
        val Tinst = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As);
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   371
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   372
        fun inst_thm t thm =
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   373
          Drule.instantiate' [] [SOME (certify lthy t)]
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   374
            (Thm.instantiate (Tinst, []) (Drule.zero_var_indexes thm));
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   375
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   376
        val uexhaust_thm = inst_thm u exhaust_thm;
49032
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   377
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   378
        val exhaust_cases = map base_name_of_ctr ctrs;
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   379
49048
4e0f0f98be02 rationalized data structure for distinctness theorems
blanchet
parents: 49046
diff changeset
   380
        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
   381
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   382
        val (distinct_thms, (distinct_thmsss', distinct_thmsss)) =
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49536
diff changeset
   383
          join_halves n half_distinct_thmss other_half_distinct_thmss ||> `transpose;
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   384
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   385
        val nchotomy_thm =
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   386
          let
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   387
            val goal =
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   388
              HOLogic.mk_Trueprop (HOLogic.mk_all (fst u', snd u',
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   389
                Library.foldr1 HOLogic.mk_disj exist_xs_u_eq_ctrs));
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   390
          in
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   391
            Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm)
49667
44d85dc8ca08 use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents: 49633
diff changeset
   392
            |> Thm.close_derivation
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   393
          end;
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   394
49484
0194a18f80cf finished "disc_coiter_iff" etc. generation
blanchet
parents: 49478
diff changeset
   395
        val (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms,
49594
55e798614c45 tweaked theorem names (in particular, dropped s's)
blanchet
parents: 49591
diff changeset
   396
             disc_exhaust_thms, collapse_thms, expand_thms, case_conv_thms) =
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   397
          if no_dests then
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   398
            ([], [], [], [], [], [], [], [], [], [])
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
   399
          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
   400
            let
49364
838b5e8ede73 allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents: 49336
diff changeset
   401
              fun make_sel_thm xs' case_thm sel_def =
838b5e8ede73 allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents: 49336
diff changeset
   402
                zero_var_indexes (Drule.gen_all (Drule.rename_bvars' (map (SOME o fst) xs')
838b5e8ede73 allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents: 49336
diff changeset
   403
                    (Drule.forall_intr_vars (case_thm RS (sel_def RS trans)))));
49281
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   404
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   405
              fun has_undefined_rhs thm =
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   406
                (case snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))) of
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   407
                  Const (@{const_name undefined}, _) => true
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   408
                | _ => false);
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   409
49364
838b5e8ede73 allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents: 49336
diff changeset
   410
              val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss;
49281
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   411
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   412
              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
   413
                (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
   414
                   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
   415
                 else
49364
838b5e8ede73 allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents: 49336
diff changeset
   416
                   map_product (fn s => fn (xs', c) => make_sel_thm xs' c s) sel_defs
838b5e8ede73 allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents: 49336
diff changeset
   417
                     (xss' ~~ case_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
   418
                |> filter_out has_undefined_rhs;
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   419
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   420
              fun mk_unique_disc_def () =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   421
                let
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   422
                  val m = the_single ms;
49591
91b228e26348 generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents: 49586
diff changeset
   423
                  val goal = mk_Trueprop_eq (mk_uu_eq (), the_single exist_xs_u_eq_ctrs);
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   424
                in
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   425
                  Skip_Proof.prove lthy [] [] goal (fn _ => mk_unique_disc_def_tac m uexhaust_thm)
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   426
                  |> singleton (Proof_Context.export names_lthy lthy)
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   427
                  |> Thm.close_derivation
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   428
                end;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   429
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   430
              fun mk_alternate_disc_def k =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   431
                let
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   432
                  val goal =
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   433
                    mk_Trueprop_eq (alternate_disc_lhs (K (nth udiscs)) (3 - k),
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   434
                      nth exist_xs_u_eq_ctrs (k - 1));
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   435
                in
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   436
                  Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   437
                    mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k))
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   438
                      (nth distinct_thms (2 - k)) uexhaust_thm)
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   439
                  |> singleton (Proof_Context.export names_lthy lthy)
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   440
                  |> Thm.close_derivation
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   441
                end;
49028
487427a02bee generate "disc_distinct" theorems
blanchet
parents: 49027
diff changeset
   442
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   443
              val has_alternate_disc_def =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   444
                exists (fn def => Thm.eq_thm_prop (def, alternate_disc_no_def)) disc_defs;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   445
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   446
              val disc_defs' =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   447
                map2 (fn k => fn def =>
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   448
                  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
   449
                  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
   450
                  else def) ks disc_defs;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   451
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   452
              val discD_thms = map (fn def => def RS iffD1) disc_defs';
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   453
              val discI_thms =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   454
                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
   455
                  disc_defs';
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   456
              val not_discI_thms =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   457
                map2 (fn m => fn def => funpow m (fn thm => allI RS thm)
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49500
diff changeset
   458
                    (unfold_thms lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]})))
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   459
                  ms disc_defs';
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   460
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   461
              val (disc_thmss', disc_thmss) =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   462
                let
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   463
                  fun mk_thm discI _ [] = refl RS discI
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   464
                    | mk_thm _ not_discI [distinct] = distinct RS not_discI;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   465
                  fun mk_thms discI not_discI distinctss = map (mk_thm discI not_discI) distinctss;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   466
                in
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   467
                  map3 mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   468
                end;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   469
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   470
              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
   471
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   472
              val (disc_exclude_thms, (disc_exclude_thmsss', disc_exclude_thmsss)) =
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   473
                let
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   474
                  fun mk_goal [] = []
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   475
                    | mk_goal [((_, udisc), (_, udisc'))] =
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   476
                      [Logic.all u (Logic.mk_implies (HOLogic.mk_Trueprop udisc,
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   477
                         HOLogic.mk_Trueprop (HOLogic.mk_not udisc')))];
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   478
49667
44d85dc8ca08 use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents: 49633
diff changeset
   479
                  fun prove tac goal =
44d85dc8ca08 use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents: 49633
diff changeset
   480
                    Skip_Proof.prove lthy [] [] goal (K tac)
44d85dc8ca08 use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents: 49633
diff changeset
   481
                    |> Thm.close_derivation;
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   482
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49536
diff changeset
   483
                  val half_pairss = mk_half_pairss (`I (ms ~~ discD_thms ~~ udiscs));
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   484
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   485
                  val half_goalss = map mk_goal half_pairss;
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   486
                  val half_thmss =
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   487
                    map3 (fn [] => K (K []) | [goal] => fn [(((m, discD), _), _)] =>
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   488
                        fn disc_thm => [prove (mk_half_disc_exclude_tac m discD disc_thm) goal])
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   489
                      half_goalss half_pairss (flat disc_thmss');
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   490
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   491
                  val other_half_goalss = map (mk_goal o map swap) half_pairss;
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   492
                  val other_half_thmss =
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   493
                    map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   494
                      other_half_goalss;
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   495
                in
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49536
diff changeset
   496
                  join_halves n half_thmss other_half_thmss ||> `transpose
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   497
                  |>> has_alternate_disc_def ? K []
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   498
                end;
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   499
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   500
              val disc_exhaust_thm =
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   501
                let
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   502
                  fun mk_prem udisc = mk_imp_p [HOLogic.mk_Trueprop udisc];
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   503
                  val goal = fold_rev Logic.all [p, u] (mk_imp_p (map mk_prem udiscs));
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   504
                in
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   505
                  Skip_Proof.prove lthy [] [] goal (fn _ =>
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   506
                    mk_disc_exhaust_tac n exhaust_thm discI_thms)
49667
44d85dc8ca08 use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents: 49633
diff changeset
   507
                  |> Thm.close_derivation
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   508
                end;
49028
487427a02bee generate "disc_distinct" theorems
blanchet
parents: 49027
diff changeset
   509
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   510
              val (collapse_thms, collapse_thm_opts) =
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   511
                let
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   512
                  fun mk_goal ctr udisc usels =
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   513
                    let
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   514
                      val prem = HOLogic.mk_Trueprop udisc;
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   515
                      val concl =
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   516
                        mk_Trueprop_eq ((null usels ? swap) (Term.list_comb (ctr, usels), u));
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   517
                    in
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   518
                      if prem aconv concl then NONE
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   519
                      else SOME (Logic.all u (Logic.mk_implies (prem, concl)))
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   520
                    end;
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   521
                  val goals = map3 mk_goal ctrs udiscs uselss;
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   522
                in
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   523
                  map4 (fn m => fn discD => fn sel_thms => Option.map (fn goal =>
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   524
                    Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   525
                      mk_collapse_tac ctxt m discD sel_thms)
49667
44d85dc8ca08 use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents: 49633
diff changeset
   526
                    |> Thm.close_derivation
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   527
                    |> perhaps (try (fn thm => refl RS thm)))) ms discD_thms sel_thmss goals
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   528
                  |> `(map_filter I)
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   529
                end;
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   530
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   531
              val expand_thms =
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   532
                let
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   533
                  fun mk_prems k udisc usels vdisc vsels =
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   534
                    (if k = n then [] else [mk_Trueprop_eq (udisc, vdisc)]) @
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   535
                    (if null usels then
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   536
                       []
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   537
                     else
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   538
                       [Logic.list_implies
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   539
                          (if n = 1 then [] else map HOLogic.mk_Trueprop [udisc, vdisc],
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   540
                             HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   541
                               (map2 (curry HOLogic.mk_eq) usels vsels)))]);
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   542
49591
91b228e26348 generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents: 49586
diff changeset
   543
                  val goal =
91b228e26348 generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents: 49586
diff changeset
   544
                    Library.foldr Logic.list_implies
91b228e26348 generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents: 49586
diff changeset
   545
                      (map5 mk_prems ks udiscs uselss vdiscs vselss, uv_eq);
91b228e26348 generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents: 49586
diff changeset
   546
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   547
                  val uncollapse_thms =
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   548
                    map (fn NONE => Drule.dummy_thm | SOME thm => thm RS sym) collapse_thm_opts;
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   549
                in
49667
44d85dc8ca08 use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents: 49633
diff changeset
   550
                  [Skip_Proof.prove lthy [] [] goal (fn _ =>
44d85dc8ca08 use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents: 49633
diff changeset
   551
                     mk_expand_tac n ms (inst_thm u disc_exhaust_thm)
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   552
                       (inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   553
                       disc_exclude_thmsss')]
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   554
                  |> Proof_Context.export names_lthy lthy
49667
44d85dc8ca08 use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents: 49633
diff changeset
   555
                  |> map Thm.close_derivation
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   556
                end;
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   557
49594
55e798614c45 tweaked theorem names (in particular, dropped s's)
blanchet
parents: 49591
diff changeset
   558
              val case_conv_thms =
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   559
                let
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   560
                  fun mk_body f usels = Term.list_comb (f, usels);
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   561
                  val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs (map2 mk_body fs uselss));
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   562
                in
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   563
                  [Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
49594
55e798614c45 tweaked theorem names (in particular, dropped s's)
blanchet
parents: 49591
diff changeset
   564
                     mk_case_conv_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)]
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   565
                  |> Proof_Context.export names_lthy lthy
49667
44d85dc8ca08 use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents: 49633
diff changeset
   566
                  |> map Thm.close_derivation
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   567
                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
   568
            in
49484
0194a18f80cf finished "disc_coiter_iff" etc. generation
blanchet
parents: 49478
diff changeset
   569
              (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms,
49594
55e798614c45 tweaked theorem names (in particular, dropped s's)
blanchet
parents: 49591
diff changeset
   570
               [disc_exhaust_thm], collapse_thms, expand_thms, case_conv_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
   571
            end;
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   572
49033
23ef2d429931 generate "weak_case_cong" property
blanchet
parents: 49032
diff changeset
   573
        val (case_cong_thm, weak_case_cong_thm) =
49032
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   574
          let
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   575
            fun mk_prem xctr xs f g =
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   576
              fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (v, xctr),
49032
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   577
                mk_Trueprop_eq (f, g)));
49033
23ef2d429931 generate "weak_case_cong" property
blanchet
parents: 49032
diff changeset
   578
49032
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   579
            val goal =
49591
91b228e26348 generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents: 49586
diff changeset
   580
              Logic.list_implies (uv_eq :: map4 mk_prem xctrs xss fs gs,
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   581
                 mk_Trueprop_eq (ufcase, vgcase));
49591
91b228e26348 generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents: 49586
diff changeset
   582
            val weak_goal = Logic.mk_implies (uv_eq, mk_Trueprop_eq (ufcase, vfcase));
49032
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   583
          in
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   584
            (Skip_Proof.prove lthy [] [] goal (fn _ => mk_case_cong_tac uexhaust_thm case_thms),
49458
blanchet
parents: 49438
diff changeset
   585
             Skip_Proof.prove lthy [] [] weak_goal (K (etac arg_cong 1)))
49667
44d85dc8ca08 use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents: 49633
diff changeset
   586
            |> pairself (singleton (Proof_Context.export names_lthy lthy) #> Thm.close_derivation)
49032
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   587
          end;
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   588
49044
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   589
        val (split_thm, split_asm_thm) =
49043
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   590
          let
49044
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   591
            fun mk_conjunct xctr xs f_xs =
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   592
              list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (u, xctr), q $ f_xs));
49044
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   593
            fun mk_disjunct xctr xs f_xs =
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   594
              list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr),
49044
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   595
                HOLogic.mk_not (q $ f_xs)));
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   596
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   597
            val lhs = q $ ufcase;
49044
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   598
49043
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   599
            val goal =
49044
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   600
              mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs));
49458
blanchet
parents: 49438
diff changeset
   601
            val asm_goal =
49044
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   602
              mk_Trueprop_eq (lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   603
                (map3 mk_disjunct xctrs xss xfs)));
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   604
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   605
            val split_thm =
49049
blanchet
parents: 49048
diff changeset
   606
              Skip_Proof.prove lthy [] [] goal
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   607
                (fn _ => mk_split_tac uexhaust_thm case_thms inject_thmss distinct_thmsss)
49044
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   608
              |> singleton (Proof_Context.export names_lthy lthy)
49667
44d85dc8ca08 use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents: 49633
diff changeset
   609
              |> Thm.close_derivation;
49044
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   610
            val split_asm_thm =
49458
blanchet
parents: 49438
diff changeset
   611
              Skip_Proof.prove lthy [] [] asm_goal (fn {context = ctxt, ...} =>
49044
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   612
                mk_split_asm_tac ctxt split_thm)
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   613
              |> singleton (Proof_Context.export names_lthy lthy)
49667
44d85dc8ca08 use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents: 49633
diff changeset
   614
              |> Thm.close_derivation;
49043
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   615
          in
49044
c4a34ae5504d generate "split_asm" property
blanchet
parents: 49043
diff changeset
   616
            (split_thm, split_asm_thm)
49043
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   617
          end;
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   618
49437
c139da00fb4a register induct attributes
blanchet
parents: 49434
diff changeset
   619
        val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   620
        val cases_type_attr = Attrib.internal (K (Induct.cases_type dataT_name));
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   621
49052
3510b943dd5b optimized "mk_split_tac" + use "notes"
blanchet
parents: 49050
diff changeset
   622
        val notes =
49594
55e798614c45 tweaked theorem names (in particular, dropped s's)
blanchet
parents: 49591
diff changeset
   623
          [(caseN, case_thms, simp_attrs),
55e798614c45 tweaked theorem names (in particular, dropped s's)
blanchet
parents: 49591
diff changeset
   624
           (case_congN, [case_cong_thm], []),
55e798614c45 tweaked theorem names (in particular, dropped s's)
blanchet
parents: 49591
diff changeset
   625
           (case_convN, case_conv_thms, []),
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   626
           (collapseN, collapse_thms, simp_attrs),
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   627
           (discsN, disc_thms, simp_attrs),
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   628
           (disc_excludeN, disc_exclude_thms, []),
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   629
           (disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]),
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   630
           (distinctN, distinct_thms, simp_attrs @ induct_simp_attrs),
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   631
           (exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]),
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   632
           (expandN, expand_thms, []),
49438
5bc80d96241e group "simps" together
blanchet
parents: 49437
diff changeset
   633
           (injectN, inject_thms, iff_attrs @ induct_simp_attrs),
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   634
           (nchotomyN, [nchotomy_thm], []),
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   635
           (selsN, all_sel_thms, simp_attrs),
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   636
           (splitN, [split_thm], []),
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   637
           (split_asmN, [split_asm_thm], []),
49633
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
   638
           (splitsN, [split_thm, split_asm_thm], []),
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   639
           (weak_case_cong_thmsN, [weak_case_cong_thm], cong_attrs)]
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   640
          |> filter_out (null o #2)
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   641
          |> map (fn (thmN, thms, attrs) =>
49633
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
   642
            ((qualify true (Binding.name thmN), attrs), [(thms, [])]));
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   643
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   644
        val notes' =
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   645
          [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)]
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   646
          |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   647
      in
49591
91b228e26348 generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents: 49586
diff changeset
   648
        ((discs, selss, exhaust_thm, inject_thms, distinct_thms, case_thms, disc_thmss, discI_thms,
91b228e26348 generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents: 49586
diff changeset
   649
          sel_thmss), lthy |> Local_Theory.notes (notes' @ notes) |> snd)
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   650
      end;
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   651
  in
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   652
    (goalss, after_qed, lthy')
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   653
  end;
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   654
49199
7c9a3c67c55d added high-level recursor, not yet curried
blanchet
parents: 49174
diff changeset
   655
fun wrap_datatype tacss = (fn (goalss, after_qed, lthy) =>
49667
44d85dc8ca08 use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents: 49633
diff changeset
   656
  map2 (map2 (Thm.close_derivation oo Skip_Proof.prove lthy [] [])) goalss tacss
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   657
  |> (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
   658
49297
47fbf2e3e89c provide a programmatic interface for FP sugar
blanchet
parents: 49286
diff changeset
   659
val wrap_datatype_cmd = (fn (goalss, after_qed, lthy) =>
47fbf2e3e89c provide a programmatic interface for FP sugar
blanchet
parents: 49286
diff changeset
   660
  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
   661
  prepare_wrap_datatype Syntax.read_term;
47fbf2e3e89c provide a programmatic interface for FP sugar
blanchet
parents: 49286
diff changeset
   662
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   663
fun parse_bracket_list parser = @{keyword "["} |-- Parse.list parser --|  @{keyword "]"};
49111
9d511132394e export "wrap" function
blanchet
parents: 49075
diff changeset
   664
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   665
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
   666
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
   667
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   668
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
   669
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
   670
val parse_bound_termss = parse_bracket_list parse_bound_terms;
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   671
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   672
val parse_wrap_options =
49633
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
   673
  Scan.optional (@{keyword "("} |-- Parse.list1 ((@{keyword "no_dests"} >> K (true, false)) ||
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
   674
      (@{keyword "rep_compat"} >> K (false, true))) --| @{keyword ")"}
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
   675
    >> (pairself (exists I) o split_list)) (false, false);
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   676
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   677
val _ =
49074
d8af889dcbe3 renamed three BNF/(co)datatype-related commands
blanchet
parents: 49057
diff changeset
   678
  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
   679
    ((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
   680
      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
   681
        Scan.optional parse_bound_termss []) ([], [])) ([], ([], [])))
49199
7c9a3c67c55d added high-level recursor, not yet curried
blanchet
parents: 49174
diff changeset
   682
     >> wrap_datatype_cmd);
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   683
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   684
end;