src/HOL/Tools/ctr_sugar.ML
author blanchet
Thu, 05 Dec 2013 14:35:58 +0100
changeset 54635 30666a281ae3
parent 54634 366297517091
child 54691 506312c293f5
permissions -rw-r--r--
proper code generation for discriminators/selectors
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
54397
f4b4fa25ce56 tuned headers
blanchet
parents: 54396
diff changeset
     1
(*  Title:      HOL/Tools/ctr_sugar.ML
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
54397
f4b4fa25ce56 tuned headers
blanchet
parents: 54396
diff changeset
     3
    Copyright   2012, 2013
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
     4
51797
182454c06a80 tuned ML and thy file names
blanchet
parents: 51790
diff changeset
     5
Wrapping existing freely generated type's constructors.
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
     6
*)
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
     7
54006
9fe1bd54d437 renamed theory file
blanchet
parents: 53925
diff changeset
     8
signature CTR_SUGAR =
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
     9
sig
51840
b304fb6c5ef5 renamed records
blanchet
parents: 51839
diff changeset
    10
  type ctr_sugar =
51839
5c552de1d8d1 added constructors to data structure
blanchet
parents: 51823
diff changeset
    11
    {ctrs: term list,
52375
bae65fd74633 store more theorems in data structure
blanchet
parents: 52322
diff changeset
    12
     casex: term,
51839
5c552de1d8d1 added constructors to data structure
blanchet
parents: 51823
diff changeset
    13
     discs: term list,
51819
9df935196be9 use record instead of big tuple
blanchet
parents: 51809
diff changeset
    14
     selss: term list list,
9df935196be9 use record instead of big tuple
blanchet
parents: 51809
diff changeset
    15
     exhaust: thm,
52375
bae65fd74633 store more theorems in data structure
blanchet
parents: 52322
diff changeset
    16
     nchotomy: thm,
51819
9df935196be9 use record instead of big tuple
blanchet
parents: 51809
diff changeset
    17
     injects: thm list,
9df935196be9 use record instead of big tuple
blanchet
parents: 51809
diff changeset
    18
     distincts: thm list,
9df935196be9 use record instead of big tuple
blanchet
parents: 51809
diff changeset
    19
     case_thms: thm list,
52375
bae65fd74633 store more theorems in data structure
blanchet
parents: 52322
diff changeset
    20
     case_cong: thm,
bae65fd74633 store more theorems in data structure
blanchet
parents: 52322
diff changeset
    21
     weak_case_cong: thm,
bae65fd74633 store more theorems in data structure
blanchet
parents: 52322
diff changeset
    22
     split: thm,
bae65fd74633 store more theorems in data structure
blanchet
parents: 52322
diff changeset
    23
     split_asm: thm,
51819
9df935196be9 use record instead of big tuple
blanchet
parents: 51809
diff changeset
    24
     disc_thmss: thm list list,
9df935196be9 use record instead of big tuple
blanchet
parents: 51809
diff changeset
    25
     discIs: thm list,
53475
185ad6cf6576 enriched data structure with necessary theorems
blanchet
parents: 53268
diff changeset
    26
     sel_thmss: thm list list,
185ad6cf6576 enriched data structure with necessary theorems
blanchet
parents: 53268
diff changeset
    27
     disc_exhausts: thm list,
53916
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53908
diff changeset
    28
     sel_exhausts: thm list,
53475
185ad6cf6576 enriched data structure with necessary theorems
blanchet
parents: 53268
diff changeset
    29
     collapses: thm list,
185ad6cf6576 enriched data structure with necessary theorems
blanchet
parents: 53268
diff changeset
    30
     expands: thm list,
53917
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
    31
     sel_splits: thm list,
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
    32
     sel_split_asms: thm list,
54491
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54435
diff changeset
    33
     case_eq_ifs: thm list};
51809
d4c1abbb4095 code tuning
blanchet
parents: 51798
diff changeset
    34
51840
b304fb6c5ef5 renamed records
blanchet
parents: 51839
diff changeset
    35
  val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar
54256
4843082be7ef added some N2M caching
blanchet
parents: 54155
diff changeset
    36
  val transfer_ctr_sugar: Proof.context -> ctr_sugar -> ctr_sugar
53867
8ad44ecc0d15 keep a database of free constructor type information
blanchet
parents: 53864
diff changeset
    37
  val ctr_sugar_of: Proof.context -> string -> ctr_sugar option
53906
17fc7811feb7 added data query function
blanchet
parents: 53888
diff changeset
    38
  val ctr_sugars_of: Proof.context -> ctr_sugar list
54403
40382f65bc80 added convenience function
blanchet
parents: 54400
diff changeset
    39
  val ctr_sugar_of_case: Proof.context -> string -> ctr_sugar option
54399
60cd3ebf2d94 export useful ML function
blanchet
parents: 54397
diff changeset
    40
  val register_ctr_sugar: string -> ctr_sugar -> local_theory -> local_theory
54400
418a183fbe21 register old-style datatypes as 'Ctr_Sugar'
blanchet
parents: 54399
diff changeset
    41
  val register_ctr_sugar_global: string -> ctr_sugar -> theory -> theory
51823
38996458bc5c create data structure for storing (co)datatype information
blanchet
parents: 51819
diff changeset
    42
49633
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
    43
  val rep_compat_prefix: string
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
    44
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49536
diff changeset
    45
  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
    46
  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
    47
49203
262ab1ac38b9 repaired constant types
blanchet
parents: 49201
diff changeset
    48
  val mk_ctr: typ list -> term -> term
53864
a48d4bd3faaa use case rather than sequence of ifs in expansion
blanchet
parents: 53857
diff changeset
    49
  val mk_case: typ list -> typ -> term -> term
49484
0194a18f80cf finished "disc_coiter_iff" etc. generation
blanchet
parents: 49478
diff changeset
    50
  val mk_disc_or_sel: typ list -> term -> term
49622
a93f976c3307 use a nicer scheme to indexify names
blanchet
parents: 49619
diff changeset
    51
  val name_of_ctr: term -> string
51777
48a0ae342ea0 generate proper attributes for coinduction rules
blanchet
parents: 51771
diff changeset
    52
  val name_of_disc: term -> string
53888
7031775668e8 improved massaging of case expressions
blanchet
parents: 53870
diff changeset
    53
  val dest_ctr: Proof.context -> string -> term -> term * term list
53870
5d45882b4f36 properly fold over branches
blanchet
parents: 53867
diff changeset
    54
  val dest_case: Proof.context -> string -> typ list -> term -> (term list * term list) option
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49536
diff changeset
    55
51781
0504e286d66d renamed "wrap_data" to "wrap_free_constructors"
blanchet
parents: 51777
diff changeset
    56
  val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
54626
8a5e82425e55 added 'no_code' option
blanchet
parents: 54622
diff changeset
    57
    (((bool * (bool * bool)) * term list) * binding) *
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
    58
      (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
51840
b304fb6c5ef5 renamed records
blanchet
parents: 51839
diff changeset
    59
    ctr_sugar * local_theory
54626
8a5e82425e55 added 'no_code' option
blanchet
parents: 54622
diff changeset
    60
  val parse_wrap_free_constructors_options: (bool * (bool * bool)) parser
49286
dde4967c9233 added "defaults" option
blanchet
parents: 49285
diff changeset
    61
  val parse_bound_term: (binding * string) parser
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
    62
end;
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
    63
54006
9fe1bd54d437 renamed theory file
blanchet
parents: 53925
diff changeset
    64
structure Ctr_Sugar : CTR_SUGAR =
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
    65
struct
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
    66
54008
b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents: 54007
diff changeset
    67
open Ctr_Sugar_Util
54006
9fe1bd54d437 renamed theory file
blanchet
parents: 53925
diff changeset
    68
open Ctr_Sugar_Tactics
54615
62fb5af93fe2 generalized datatype code generation code so that it works with old-style and new-style (co)datatypes (as long as they are not local)
blanchet
parents: 54493
diff changeset
    69
open Ctr_Sugar_Code
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
    70
51840
b304fb6c5ef5 renamed records
blanchet
parents: 51839
diff changeset
    71
type ctr_sugar =
51839
5c552de1d8d1 added constructors to data structure
blanchet
parents: 51823
diff changeset
    72
  {ctrs: term list,
52375
bae65fd74633 store more theorems in data structure
blanchet
parents: 52322
diff changeset
    73
   casex: term,
51839
5c552de1d8d1 added constructors to data structure
blanchet
parents: 51823
diff changeset
    74
   discs: term list,
51819
9df935196be9 use record instead of big tuple
blanchet
parents: 51809
diff changeset
    75
   selss: term list list,
9df935196be9 use record instead of big tuple
blanchet
parents: 51809
diff changeset
    76
   exhaust: thm,
52375
bae65fd74633 store more theorems in data structure
blanchet
parents: 52322
diff changeset
    77
   nchotomy: thm,
51819
9df935196be9 use record instead of big tuple
blanchet
parents: 51809
diff changeset
    78
   injects: thm list,
9df935196be9 use record instead of big tuple
blanchet
parents: 51809
diff changeset
    79
   distincts: thm list,
9df935196be9 use record instead of big tuple
blanchet
parents: 51809
diff changeset
    80
   case_thms: thm list,
52375
bae65fd74633 store more theorems in data structure
blanchet
parents: 52322
diff changeset
    81
   case_cong: thm,
bae65fd74633 store more theorems in data structure
blanchet
parents: 52322
diff changeset
    82
   weak_case_cong: thm,
bae65fd74633 store more theorems in data structure
blanchet
parents: 52322
diff changeset
    83
   split: thm,
bae65fd74633 store more theorems in data structure
blanchet
parents: 52322
diff changeset
    84
   split_asm: thm,
51819
9df935196be9 use record instead of big tuple
blanchet
parents: 51809
diff changeset
    85
   disc_thmss: thm list list,
9df935196be9 use record instead of big tuple
blanchet
parents: 51809
diff changeset
    86
   discIs: thm list,
53475
185ad6cf6576 enriched data structure with necessary theorems
blanchet
parents: 53268
diff changeset
    87
   sel_thmss: thm list list,
185ad6cf6576 enriched data structure with necessary theorems
blanchet
parents: 53268
diff changeset
    88
   disc_exhausts: thm list,
53916
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53908
diff changeset
    89
   sel_exhausts: thm list,
53475
185ad6cf6576 enriched data structure with necessary theorems
blanchet
parents: 53268
diff changeset
    90
   collapses: thm list,
185ad6cf6576 enriched data structure with necessary theorems
blanchet
parents: 53268
diff changeset
    91
   expands: thm list,
53917
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
    92
   sel_splits: thm list,
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
    93
   sel_split_asms: thm list,
54491
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54435
diff changeset
    94
   case_eq_ifs: thm list};
51809
d4c1abbb4095 code tuning
blanchet
parents: 51798
diff changeset
    95
53906
17fc7811feb7 added data query function
blanchet
parents: 53888
diff changeset
    96
fun eq_ctr_sugar ({ctrs = ctrs1, casex = case1, discs = discs1, selss = selss1, ...} : ctr_sugar,
17fc7811feb7 added data query function
blanchet
parents: 53888
diff changeset
    97
    {ctrs = ctrs2, casex = case2, discs = discs2, selss = selss2, ...} : ctr_sugar) =
17fc7811feb7 added data query function
blanchet
parents: 53888
diff changeset
    98
  ctrs1 = ctrs2 andalso case1 = case2 andalso discs1 = discs2 andalso selss1 = selss2;
17fc7811feb7 added data query function
blanchet
parents: 53888
diff changeset
    99
52375
bae65fd74633 store more theorems in data structure
blanchet
parents: 52322
diff changeset
   100
fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
53475
185ad6cf6576 enriched data structure with necessary theorems
blanchet
parents: 53268
diff changeset
   101
    case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss,
54491
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54435
diff changeset
   102
    disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms, case_eq_ifs} =
51839
5c552de1d8d1 added constructors to data structure
blanchet
parents: 51823
diff changeset
   103
  {ctrs = map (Morphism.term phi) ctrs,
52375
bae65fd74633 store more theorems in data structure
blanchet
parents: 52322
diff changeset
   104
   casex = Morphism.term phi casex,
51839
5c552de1d8d1 added constructors to data structure
blanchet
parents: 51823
diff changeset
   105
   discs = map (Morphism.term phi) discs,
51823
38996458bc5c create data structure for storing (co)datatype information
blanchet
parents: 51819
diff changeset
   106
   selss = map (map (Morphism.term phi)) selss,
38996458bc5c create data structure for storing (co)datatype information
blanchet
parents: 51819
diff changeset
   107
   exhaust = Morphism.thm phi exhaust,
52375
bae65fd74633 store more theorems in data structure
blanchet
parents: 52322
diff changeset
   108
   nchotomy = Morphism.thm phi nchotomy,
51823
38996458bc5c create data structure for storing (co)datatype information
blanchet
parents: 51819
diff changeset
   109
   injects = map (Morphism.thm phi) injects,
38996458bc5c create data structure for storing (co)datatype information
blanchet
parents: 51819
diff changeset
   110
   distincts = map (Morphism.thm phi) distincts,
38996458bc5c create data structure for storing (co)datatype information
blanchet
parents: 51819
diff changeset
   111
   case_thms = map (Morphism.thm phi) case_thms,
52375
bae65fd74633 store more theorems in data structure
blanchet
parents: 52322
diff changeset
   112
   case_cong = Morphism.thm phi case_cong,
bae65fd74633 store more theorems in data structure
blanchet
parents: 52322
diff changeset
   113
   weak_case_cong = Morphism.thm phi weak_case_cong,
bae65fd74633 store more theorems in data structure
blanchet
parents: 52322
diff changeset
   114
   split = Morphism.thm phi split,
bae65fd74633 store more theorems in data structure
blanchet
parents: 52322
diff changeset
   115
   split_asm = Morphism.thm phi split_asm,
51823
38996458bc5c create data structure for storing (co)datatype information
blanchet
parents: 51819
diff changeset
   116
   disc_thmss = map (map (Morphism.thm phi)) disc_thmss,
38996458bc5c create data structure for storing (co)datatype information
blanchet
parents: 51819
diff changeset
   117
   discIs = map (Morphism.thm phi) discIs,
53475
185ad6cf6576 enriched data structure with necessary theorems
blanchet
parents: 53268
diff changeset
   118
   sel_thmss = map (map (Morphism.thm phi)) sel_thmss,
185ad6cf6576 enriched data structure with necessary theorems
blanchet
parents: 53268
diff changeset
   119
   disc_exhausts = map (Morphism.thm phi) disc_exhausts,
53916
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53908
diff changeset
   120
   sel_exhausts = map (Morphism.thm phi) sel_exhausts,
53475
185ad6cf6576 enriched data structure with necessary theorems
blanchet
parents: 53268
diff changeset
   121
   collapses = map (Morphism.thm phi) collapses,
185ad6cf6576 enriched data structure with necessary theorems
blanchet
parents: 53268
diff changeset
   122
   expands = map (Morphism.thm phi) expands,
53917
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   123
   sel_splits = map (Morphism.thm phi) sel_splits,
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   124
   sel_split_asms = map (Morphism.thm phi) sel_split_asms,
54491
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54435
diff changeset
   125
   case_eq_ifs = map (Morphism.thm phi) case_eq_ifs};
51823
38996458bc5c create data structure for storing (co)datatype information
blanchet
parents: 51819
diff changeset
   126
53906
17fc7811feb7 added data query function
blanchet
parents: 53888
diff changeset
   127
val transfer_ctr_sugar =
17fc7811feb7 added data query function
blanchet
parents: 53888
diff changeset
   128
  morph_ctr_sugar o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
53867
8ad44ecc0d15 keep a database of free constructor type information
blanchet
parents: 53864
diff changeset
   129
8ad44ecc0d15 keep a database of free constructor type information
blanchet
parents: 53864
diff changeset
   130
structure Data = Generic_Data
8ad44ecc0d15 keep a database of free constructor type information
blanchet
parents: 53864
diff changeset
   131
(
8ad44ecc0d15 keep a database of free constructor type information
blanchet
parents: 53864
diff changeset
   132
  type T = ctr_sugar Symtab.table;
8ad44ecc0d15 keep a database of free constructor type information
blanchet
parents: 53864
diff changeset
   133
  val empty = Symtab.empty;
8ad44ecc0d15 keep a database of free constructor type information
blanchet
parents: 53864
diff changeset
   134
  val extend = I;
8ad44ecc0d15 keep a database of free constructor type information
blanchet
parents: 53864
diff changeset
   135
  val merge = Symtab.merge eq_ctr_sugar;
8ad44ecc0d15 keep a database of free constructor type information
blanchet
parents: 53864
diff changeset
   136
);
8ad44ecc0d15 keep a database of free constructor type information
blanchet
parents: 53864
diff changeset
   137
8ad44ecc0d15 keep a database of free constructor type information
blanchet
parents: 53864
diff changeset
   138
fun ctr_sugar_of ctxt =
8ad44ecc0d15 keep a database of free constructor type information
blanchet
parents: 53864
diff changeset
   139
  Symtab.lookup (Data.get (Context.Proof ctxt))
53906
17fc7811feb7 added data query function
blanchet
parents: 53888
diff changeset
   140
  #> Option.map (transfer_ctr_sugar ctxt);
17fc7811feb7 added data query function
blanchet
parents: 53888
diff changeset
   141
17fc7811feb7 added data query function
blanchet
parents: 53888
diff changeset
   142
fun ctr_sugars_of ctxt =
17fc7811feb7 added data query function
blanchet
parents: 53888
diff changeset
   143
  Symtab.fold (cons o transfer_ctr_sugar ctxt o snd) (Data.get (Context.Proof ctxt)) [];
53867
8ad44ecc0d15 keep a database of free constructor type information
blanchet
parents: 53864
diff changeset
   144
54403
40382f65bc80 added convenience function
blanchet
parents: 54400
diff changeset
   145
fun ctr_sugar_of_case ctxt s =
40382f65bc80 added convenience function
blanchet
parents: 54400
diff changeset
   146
  find_first (fn {casex = Const (s', _), ...} => s' = s | _ => false) (ctr_sugars_of ctxt);
40382f65bc80 added convenience function
blanchet
parents: 54400
diff changeset
   147
53867
8ad44ecc0d15 keep a database of free constructor type information
blanchet
parents: 53864
diff changeset
   148
fun register_ctr_sugar key ctr_sugar =
54285
578371ba74cc reverted 3e1d230f1c00 -- pervasiveness is useful, cf. Coinductive_Nat in the AFP
blanchet
parents: 54265
diff changeset
   149
  Local_Theory.declaration {syntax = false, pervasive = true}
53867
8ad44ecc0d15 keep a database of free constructor type information
blanchet
parents: 53864
diff changeset
   150
    (fn phi => Data.map (Symtab.default (key, morph_ctr_sugar phi ctr_sugar)));
8ad44ecc0d15 keep a database of free constructor type information
blanchet
parents: 53864
diff changeset
   151
54400
418a183fbe21 register old-style datatypes as 'Ctr_Sugar'
blanchet
parents: 54399
diff changeset
   152
fun register_ctr_sugar_global key ctr_sugar =
418a183fbe21 register old-style datatypes as 'Ctr_Sugar'
blanchet
parents: 54399
diff changeset
   153
  Context.theory_map (Data.map (Symtab.default (key, ctr_sugar)));
418a183fbe21 register old-style datatypes as 'Ctr_Sugar'
blanchet
parents: 54399
diff changeset
   154
49633
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
   155
val rep_compat_prefix = "new";
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
   156
49223
blanchet
parents: 49210
diff changeset
   157
val isN = "is_";
blanchet
parents: 49210
diff changeset
   158
val unN = "un_";
blanchet
parents: 49210
diff changeset
   159
fun mk_unN 1 1 suf = unN ^ suf
blanchet
parents: 49210
diff changeset
   160
  | 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
   161
49594
55e798614c45 tweaked theorem names (in particular, dropped s's)
blanchet
parents: 49591
diff changeset
   162
val caseN = "case";
49054
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
   163
val case_congN = "case_cong";
54491
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54435
diff changeset
   164
val case_eq_ifN = "case_eq_if";
49118
b815fa776b91 renamed theorem
blanchet
parents: 49117
diff changeset
   165
val collapseN = "collapse";
49122
83515378d4d7 renamed "disc_exclus" theorem to "disc_exclude"
blanchet
parents: 49121
diff changeset
   166
val disc_excludeN = "disc_exclude";
49054
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
   167
val disc_exhaustN = "disc_exhaust";
53694
7b453b619b5f use singular to avoid confusion
blanchet
parents: 53475
diff changeset
   168
val discN = "disc";
53700
e6a44d775be3 note "discI"
blanchet
parents: 53694
diff changeset
   169
val discIN = "discI";
49054
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
   170
val distinctN = "distinct";
49075
ed769978dc8d rearrange dependencies
blanchet
parents: 49074
diff changeset
   171
val exhaustN = "exhaust";
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   172
val expandN = "expand";
49075
ed769978dc8d rearrange dependencies
blanchet
parents: 49074
diff changeset
   173
val injectN = "inject";
ed769978dc8d rearrange dependencies
blanchet
parents: 49074
diff changeset
   174
val nchotomyN = "nchotomy";
53694
7b453b619b5f use singular to avoid confusion
blanchet
parents: 53475
diff changeset
   175
val selN = "sel";
53916
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53908
diff changeset
   176
val sel_exhaustN = "sel_exhaust";
53917
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   177
val sel_splitN = "sel_split";
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   178
val sel_split_asmN = "sel_split_asm";
49054
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
   179
val splitN = "split";
49633
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
   180
val splitsN = "splits";
49054
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
   181
val split_asmN = "split_asm";
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
   182
val weak_case_cong_thmsN = "weak_case_cong";
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   183
53700
e6a44d775be3 note "discI"
blanchet
parents: 53694
diff changeset
   184
val cong_attrs = @{attributes [cong]};
53836
a1632a5f5fb3 added [dest] to "disc_exclude"
blanchet
parents: 53810
diff changeset
   185
val dest_attrs = @{attributes [dest]};
53700
e6a44d775be3 note "discI"
blanchet
parents: 53694
diff changeset
   186
val safe_elim_attrs = @{attributes [elim!]};
e6a44d775be3 note "discI"
blanchet
parents: 53694
diff changeset
   187
val iff_attrs = @{attributes [iff]};
54145
297d1c603999 make sure that registered code equations are actually equations
blanchet
parents: 54008
diff changeset
   188
val inductsimp_attrs = @{attributes [induct_simp]};
297d1c603999 make sure that registered code equations are actually equations
blanchet
parents: 54008
diff changeset
   189
val nitpicksimp_attrs = @{attributes [nitpick_simp]};
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   190
val simp_attrs = @{attributes [simp]};
54151
71dc4e6c001c set code attribute on discriminator equations
blanchet
parents: 54145
diff changeset
   191
val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs;
71dc4e6c001c set code attribute on discriminator equations
blanchet
parents: 54145
diff changeset
   192
val code_nitpicksimp_simp_attrs = code_nitpicksimp_attrs @ simp_attrs;
49046
3c5eba97d93a allow default names for selectors via wildcard (_) + fix wrong index (k)
blanchet
parents: 49045
diff changeset
   193
53040
e6edd7abc4ce renamed function
blanchet
parents: 53039
diff changeset
   194
fun unflat_lookup eq xs ys = map (fn xs' => permute_like eq xs xs' ys);
49258
84f13469d7f0 allow same selector name for several constructors
blanchet
parents: 49257
diff changeset
   195
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49536
diff changeset
   196
fun mk_half_pairss' _ ([], []) = []
49591
91b228e26348 generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents: 49586
diff changeset
   197
  | mk_half_pairss' indent (x :: xs, _ :: ys) =
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49536
diff changeset
   198
    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
   199
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49536
diff changeset
   200
fun mk_half_pairss p = mk_half_pairss' [[]] p;
49027
fc3b9b49c92d added discriminator theorems
blanchet
parents: 49025
diff changeset
   201
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   202
fun join_halves n half_xss other_half_xss =
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   203
  let
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   204
    val xsss =
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   205
      map2 (map2 append) (Library.chop_groups n half_xss)
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   206
        (transpose (Library.chop_groups n other_half_xss))
49668
blanchet
parents: 49667
diff changeset
   207
    val xs = splice (flat half_xss) (flat other_half_xss);
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49536
diff changeset
   208
  in (xs, xsss) end;
49027
fc3b9b49c92d added discriminator theorems
blanchet
parents: 49025
diff changeset
   209
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   210
fun mk_undefined T = Const (@{const_name undefined}, T);
49055
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   211
49500
blanchet
parents: 49498
diff changeset
   212
fun mk_ctr Ts t =
blanchet
parents: 49498
diff changeset
   213
  let val Type (_, Ts0) = body_type (fastype_of t) in
54435
4a655e62ad34 fixed type variable confusion in 'datatype_new_compat'
blanchet
parents: 54422
diff changeset
   214
    subst_nonatomic_types (Ts0 ~~ Ts) t
49203
262ab1ac38b9 repaired constant types
blanchet
parents: 49201
diff changeset
   215
  end;
262ab1ac38b9 repaired constant types
blanchet
parents: 49201
diff changeset
   216
49536
898aea2e7a94 started work on generation of "rel" theorems
blanchet
parents: 49510
diff changeset
   217
fun mk_case Ts T t =
898aea2e7a94 started work on generation of "rel" theorems
blanchet
parents: 49510
diff changeset
   218
  let val (Type (_, Ts0), body) = strip_type (fastype_of t) |>> List.last in
54435
4a655e62ad34 fixed type variable confusion in 'datatype_new_compat'
blanchet
parents: 54422
diff changeset
   219
    subst_nonatomic_types ((body, T) :: (Ts0 ~~ Ts)) t
49536
898aea2e7a94 started work on generation of "rel" theorems
blanchet
parents: 49510
diff changeset
   220
  end;
898aea2e7a94 started work on generation of "rel" theorems
blanchet
parents: 49510
diff changeset
   221
53864
a48d4bd3faaa use case rather than sequence of ifs in expansion
blanchet
parents: 53857
diff changeset
   222
fun mk_disc_or_sel Ts t =
54435
4a655e62ad34 fixed type variable confusion in 'datatype_new_compat'
blanchet
parents: 54422
diff changeset
   223
  subst_nonatomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
53864
a48d4bd3faaa use case rather than sequence of ifs in expansion
blanchet
parents: 53857
diff changeset
   224
51777
48a0ae342ea0 generate proper attributes for coinduction rules
blanchet
parents: 51771
diff changeset
   225
fun name_of_const what t =
48a0ae342ea0 generate proper attributes for coinduction rules
blanchet
parents: 51771
diff changeset
   226
  (case head_of t of
49622
a93f976c3307 use a nicer scheme to indexify names
blanchet
parents: 49619
diff changeset
   227
    Const (s, _) => s
a93f976c3307 use a nicer scheme to indexify names
blanchet
parents: 49619
diff changeset
   228
  | Free (s, _) => s
51777
48a0ae342ea0 generate proper attributes for coinduction rules
blanchet
parents: 51771
diff changeset
   229
  | _ => error ("Cannot extract name of " ^ what));
48a0ae342ea0 generate proper attributes for coinduction rules
blanchet
parents: 51771
diff changeset
   230
48a0ae342ea0 generate proper attributes for coinduction rules
blanchet
parents: 51771
diff changeset
   231
val name_of_ctr = name_of_const "constructor";
48a0ae342ea0 generate proper attributes for coinduction rules
blanchet
parents: 51771
diff changeset
   232
48a0ae342ea0 generate proper attributes for coinduction rules
blanchet
parents: 51771
diff changeset
   233
val notN = "not_";
48a0ae342ea0 generate proper attributes for coinduction rules
blanchet
parents: 51771
diff changeset
   234
val eqN = "eq_";
48a0ae342ea0 generate proper attributes for coinduction rules
blanchet
parents: 51771
diff changeset
   235
val neqN = "neq_";
48a0ae342ea0 generate proper attributes for coinduction rules
blanchet
parents: 51771
diff changeset
   236
48a0ae342ea0 generate proper attributes for coinduction rules
blanchet
parents: 51771
diff changeset
   237
fun name_of_disc t =
48a0ae342ea0 generate proper attributes for coinduction rules
blanchet
parents: 51771
diff changeset
   238
  (case head_of t of
48a0ae342ea0 generate proper attributes for coinduction rules
blanchet
parents: 51771
diff changeset
   239
    Abs (_, _, @{const Not} $ (t' $ Bound 0)) =>
48a0ae342ea0 generate proper attributes for coinduction rules
blanchet
parents: 51771
diff changeset
   240
    Long_Name.map_base_name (prefix notN) (name_of_disc t')
48a0ae342ea0 generate proper attributes for coinduction rules
blanchet
parents: 51771
diff changeset
   241
  | Abs (_, _, Const (@{const_name HOL.eq}, _) $ Bound 0 $ t') =>
48a0ae342ea0 generate proper attributes for coinduction rules
blanchet
parents: 51771
diff changeset
   242
    Long_Name.map_base_name (prefix eqN) (name_of_disc t')
48a0ae342ea0 generate proper attributes for coinduction rules
blanchet
parents: 51771
diff changeset
   243
  | Abs (_, _, @{const Not} $ (Const (@{const_name HOL.eq}, _) $ Bound 0 $ t')) =>
48a0ae342ea0 generate proper attributes for coinduction rules
blanchet
parents: 51771
diff changeset
   244
    Long_Name.map_base_name (prefix neqN) (name_of_disc t')
48a0ae342ea0 generate proper attributes for coinduction rules
blanchet
parents: 51771
diff changeset
   245
  | t' => name_of_const "destructor" t');
49622
a93f976c3307 use a nicer scheme to indexify names
blanchet
parents: 49619
diff changeset
   246
a93f976c3307 use a nicer scheme to indexify names
blanchet
parents: 49619
diff changeset
   247
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
   248
53888
7031775668e8 improved massaging of case expressions
blanchet
parents: 53870
diff changeset
   249
fun dest_ctr ctxt s t =
7031775668e8 improved massaging of case expressions
blanchet
parents: 53870
diff changeset
   250
  let
7031775668e8 improved massaging of case expressions
blanchet
parents: 53870
diff changeset
   251
    val (f, args) = Term.strip_comb t;
7031775668e8 improved massaging of case expressions
blanchet
parents: 53870
diff changeset
   252
  in
7031775668e8 improved massaging of case expressions
blanchet
parents: 53870
diff changeset
   253
    (case ctr_sugar_of ctxt s of
7031775668e8 improved massaging of case expressions
blanchet
parents: 53870
diff changeset
   254
      SOME {ctrs, ...} =>
7031775668e8 improved massaging of case expressions
blanchet
parents: 53870
diff changeset
   255
      (case find_first (can (fo_match ctxt f)) ctrs of
7031775668e8 improved massaging of case expressions
blanchet
parents: 53870
diff changeset
   256
        SOME f' => (f', args)
7031775668e8 improved massaging of case expressions
blanchet
parents: 53870
diff changeset
   257
      | NONE => raise Fail "dest_ctr")
7031775668e8 improved massaging of case expressions
blanchet
parents: 53870
diff changeset
   258
    | NONE => raise Fail "dest_ctr")
7031775668e8 improved massaging of case expressions
blanchet
parents: 53870
diff changeset
   259
  end;
7031775668e8 improved massaging of case expressions
blanchet
parents: 53870
diff changeset
   260
53870
5d45882b4f36 properly fold over branches
blanchet
parents: 53867
diff changeset
   261
fun dest_case ctxt s Ts t =
5d45882b4f36 properly fold over branches
blanchet
parents: 53867
diff changeset
   262
  (case Term.strip_comb t of
5d45882b4f36 properly fold over branches
blanchet
parents: 53867
diff changeset
   263
    (Const (c, _), args as _ :: _) =>
5d45882b4f36 properly fold over branches
blanchet
parents: 53867
diff changeset
   264
    (case ctr_sugar_of ctxt s of
5d45882b4f36 properly fold over branches
blanchet
parents: 53867
diff changeset
   265
      SOME {casex = Const (case_name, _), discs = discs0, selss = selss0, ...} =>
5d45882b4f36 properly fold over branches
blanchet
parents: 53867
diff changeset
   266
      if case_name = c then
53924
b19d300db73b avoid calls to nth with ~1
blanchet
parents: 53919
diff changeset
   267
        let val n = length discs0 in
b19d300db73b avoid calls to nth with ~1
blanchet
parents: 53919
diff changeset
   268
          if n < length args then
b19d300db73b avoid calls to nth with ~1
blanchet
parents: 53919
diff changeset
   269
            let
b19d300db73b avoid calls to nth with ~1
blanchet
parents: 53919
diff changeset
   270
              val (branches, obj :: leftovers) = chop n args;
b19d300db73b avoid calls to nth with ~1
blanchet
parents: 53919
diff changeset
   271
              val discs = map (mk_disc_or_sel Ts) discs0;
b19d300db73b avoid calls to nth with ~1
blanchet
parents: 53919
diff changeset
   272
              val selss = map (map (mk_disc_or_sel Ts)) selss0;
b19d300db73b avoid calls to nth with ~1
blanchet
parents: 53919
diff changeset
   273
              val conds = map (rapp obj) discs;
b19d300db73b avoid calls to nth with ~1
blanchet
parents: 53919
diff changeset
   274
              val branch_argss = map (fn sels => map (rapp obj) sels @ leftovers) selss;
b19d300db73b avoid calls to nth with ~1
blanchet
parents: 53919
diff changeset
   275
              val branches' = map2 (curry Term.betapplys) branches branch_argss;
b19d300db73b avoid calls to nth with ~1
blanchet
parents: 53919
diff changeset
   276
            in
b19d300db73b avoid calls to nth with ~1
blanchet
parents: 53919
diff changeset
   277
              SOME (conds, branches')
b19d300db73b avoid calls to nth with ~1
blanchet
parents: 53919
diff changeset
   278
            end
b19d300db73b avoid calls to nth with ~1
blanchet
parents: 53919
diff changeset
   279
          else
b19d300db73b avoid calls to nth with ~1
blanchet
parents: 53919
diff changeset
   280
            NONE
53870
5d45882b4f36 properly fold over branches
blanchet
parents: 53867
diff changeset
   281
        end
5d45882b4f36 properly fold over branches
blanchet
parents: 53867
diff changeset
   282
      else
5d45882b4f36 properly fold over branches
blanchet
parents: 53867
diff changeset
   283
        NONE
5d45882b4f36 properly fold over branches
blanchet
parents: 53867
diff changeset
   284
    | _ => NONE)
5d45882b4f36 properly fold over branches
blanchet
parents: 53867
diff changeset
   285
  | _ => NONE);
5d45882b4f36 properly fold over branches
blanchet
parents: 53867
diff changeset
   286
49437
c139da00fb4a register induct attributes
blanchet
parents: 49434
diff changeset
   287
fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
c139da00fb4a register induct attributes
blanchet
parents: 49434
diff changeset
   288
54626
8a5e82425e55 added 'no_code' option
blanchet
parents: 54622
diff changeset
   289
fun prepare_wrap_free_constructors prep_term ((((no_discs_sels, (no_code, rep_compat)), raw_ctrs),
52968
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   290
    raw_case_binding), (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   291
  let
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   292
    (* TODO: sanity checks on arguments *)
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   293
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   294
    val n = length raw_ctrs;
49054
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
   295
    val ks = 1 upto n;
ee0a1d449f89 generate default names for selectors
blanchet
parents: 49053
diff changeset
   296
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   297
    val _ = if n > 0 then () else error "No constructors specified";
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   298
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   299
    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
   300
    val sel_defaultss =
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   301
      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
   302
53908
blanchet
parents: 53906
diff changeset
   303
    val Type (fcT_name, As0) = body_type (fastype_of (hd ctrs0));
blanchet
parents: 53906
diff changeset
   304
    val fc_b_name = Long_Name.base_name fcT_name;
blanchet
parents: 53906
diff changeset
   305
    val fc_b = Binding.name fc_b_name;
49055
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   306
49633
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
   307
    fun qualify mandatory =
53908
blanchet
parents: 53906
diff changeset
   308
      Binding.qualify mandatory fc_b_name o (rep_compat ? Binding.qualify false rep_compat_prefix);
49633
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
   309
54386
3514fdfdf59b minor doc fix
blanchet
parents: 54285
diff changeset
   310
    fun dest_TFree_or_TVar (TFree sS) = sS
53268
de1dc709f9d4 handle type class annotations on (co)datatype parameters gracefully
blanchet
parents: 53210
diff changeset
   311
      | dest_TFree_or_TVar (TVar ((s, _), S)) = (s, S)
de1dc709f9d4 handle type class annotations on (co)datatype parameters gracefully
blanchet
parents: 53210
diff changeset
   312
      | dest_TFree_or_TVar _ = error "Invalid type argument";
52965
0cd62cb233e0 handle both TVars and TFrees -- necessary for 'wrap_free_constructors'
blanchet
parents: 52963
diff changeset
   313
53268
de1dc709f9d4 handle type class annotations on (co)datatype parameters gracefully
blanchet
parents: 53210
diff changeset
   314
    val (unsorted_As, B) =
49055
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   315
      no_defs_lthy
53268
de1dc709f9d4 handle type class annotations on (co)datatype parameters gracefully
blanchet
parents: 53210
diff changeset
   316
      |> variant_tfrees (map (fst o dest_TFree_or_TVar) As0)
49055
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   317
      ||> the_single o fst o mk_TFrees 1;
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   318
53268
de1dc709f9d4 handle type class annotations on (co)datatype parameters gracefully
blanchet
parents: 53210
diff changeset
   319
    val As = map2 (resort_tfree o snd o dest_TFree_or_TVar) As0 unsorted_As;
de1dc709f9d4 handle type class annotations on (co)datatype parameters gracefully
blanchet
parents: 53210
diff changeset
   320
53908
blanchet
parents: 53906
diff changeset
   321
    val fcT = Type (fcT_name, As);
49055
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   322
    val ctrs = map (mk_ctr As) ctrs0;
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   323
    val ctr_Tss = map (binder_types o fastype_of) ctrs;
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   324
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   325
    val ms = map length ctr_Tss;
631512830082 pad the selectors' list with default names
blanchet
parents: 49054
diff changeset
   326
51790
22517d04d20b more intuitive syntax for equality-style discriminators of nullary constructors
blanchet
parents: 51787
diff changeset
   327
    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
   328
53925
blanchet
parents: 53924
diff changeset
   329
    fun can_definitely_rely_on_disc k = not (Binding.is_empty (nth raw_disc_bindings' (k - 1)));
51790
22517d04d20b more intuitive syntax for equality-style discriminators of nullary constructors
blanchet
parents: 51787
diff changeset
   330
    fun can_rely_on_disc k =
22517d04d20b more intuitive syntax for equality-style discriminators of nullary constructors
blanchet
parents: 51787
diff changeset
   331
      can_definitely_rely_on_disc k orelse (k = 1 andalso not (can_definitely_rely_on_disc 2));
53925
blanchet
parents: 53924
diff changeset
   332
    fun should_omit_disc_binding k = n = 1 orelse (n = 2 andalso can_rely_on_disc (3 - k));
51790
22517d04d20b more intuitive syntax for equality-style discriminators of nullary constructors
blanchet
parents: 51787
diff changeset
   333
22517d04d20b more intuitive syntax for equality-style discriminators of nullary constructors
blanchet
parents: 51787
diff changeset
   334
    fun is_disc_binding_valid b =
22517d04d20b more intuitive syntax for equality-style discriminators of nullary constructors
blanchet
parents: 51787
diff changeset
   335
      not (Binding.is_empty b orelse Binding.eq_name (b, equal_binding));
51787
1267c28c7bdd changed discriminator default: avoid mixing ctor and dtor views
blanchet
parents: 51781
diff changeset
   336
52322
74315fe137ba too much qualification is like too little
blanchet
parents: 52280
diff changeset
   337
    val standard_disc_binding = Binding.name o prefix isN o base_name_of_ctr;
49120
7f8e69fc6ac9 smarter "*" syntax -- fallback on "_" if "*" is impossible
blanchet
parents: 49119
diff changeset
   338
49336
blanchet
parents: 49311
diff changeset
   339
    val disc_bindings =
blanchet
parents: 49311
diff changeset
   340
      raw_disc_bindings'
49120
7f8e69fc6ac9 smarter "*" syntax -- fallback on "_" if "*" is impossible
blanchet
parents: 49119
diff changeset
   341
      |> map4 (fn k => fn m => fn ctr => fn disc =>
51790
22517d04d20b more intuitive syntax for equality-style discriminators of nullary constructors
blanchet
parents: 51787
diff changeset
   342
        qualify false
51787
1267c28c7bdd changed discriminator default: avoid mixing ctor and dtor views
blanchet
parents: 51781
diff changeset
   343
          (if Binding.is_empty disc then
51790
22517d04d20b more intuitive syntax for equality-style discriminators of nullary constructors
blanchet
parents: 51787
diff changeset
   344
             if should_omit_disc_binding k then disc else standard_disc_binding ctr
22517d04d20b more intuitive syntax for equality-style discriminators of nullary constructors
blanchet
parents: 51787
diff changeset
   345
           else if Binding.eq_name (disc, equal_binding) then
22517d04d20b more intuitive syntax for equality-style discriminators of nullary constructors
blanchet
parents: 51787
diff changeset
   346
             if m = 0 then disc
22517d04d20b more intuitive syntax for equality-style discriminators of nullary constructors
blanchet
parents: 51787
diff changeset
   347
             else error "Cannot use \"=\" syntax for discriminating nonnullary constructor"
22517d04d20b more intuitive syntax for equality-style discriminators of nullary constructors
blanchet
parents: 51787
diff changeset
   348
           else if Binding.eq_name (disc, standard_binding) then
22517d04d20b more intuitive syntax for equality-style discriminators of nullary constructors
blanchet
parents: 51787
diff changeset
   349
             standard_disc_binding ctr
49302
f5bd87aac224 added optional qualifiers for constructors and destructors, similarly to the old package
blanchet
parents: 49300
diff changeset
   350
           else
51790
22517d04d20b more intuitive syntax for equality-style discriminators of nullary constructors
blanchet
parents: 51787
diff changeset
   351
             disc)) ks ms ctrs0;
49056
blanchet
parents: 49055
diff changeset
   352
51787
1267c28c7bdd changed discriminator default: avoid mixing ctor and dtor views
blanchet
parents: 51781
diff changeset
   353
    fun standard_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
   354
49336
blanchet
parents: 49311
diff changeset
   355
    val sel_bindingss =
blanchet
parents: 49311
diff changeset
   356
      pad_list [] n raw_sel_bindingss
49056
blanchet
parents: 49055
diff changeset
   357
      |> map3 (fn ctr => fn m => map2 (fn l => fn sel =>
49633
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
   358
        qualify false
51790
22517d04d20b more intuitive syntax for equality-style discriminators of nullary constructors
blanchet
parents: 51787
diff changeset
   359
          (if Binding.is_empty sel orelse Binding.eq_name (sel, standard_binding) then
51787
1267c28c7bdd changed discriminator default: avoid mixing ctor and dtor views
blanchet
parents: 51781
diff changeset
   360
            standard_sel_binding m l ctr
49302
f5bd87aac224 added optional qualifiers for constructors and destructors, similarly to the old package
blanchet
parents: 49300
diff changeset
   361
          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
   362
            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
   363
49201
blanchet
parents: 49199
diff changeset
   364
    val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
49043
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   365
52968
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   366
    val ((((((((xss, xss'), yss), fs), gs), [u', v']), [w]), (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
   367
      mk_Freess' "x" ctr_Tss
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   368
      ||>> mk_Freess "y" ctr_Tss
49201
blanchet
parents: 49199
diff changeset
   369
      ||>> mk_Frees "f" case_Ts
blanchet
parents: 49199
diff changeset
   370
      ||>> mk_Frees "g" case_Ts
53908
blanchet
parents: 53906
diff changeset
   371
      ||>> (apfst (map (rpair fcT)) oo Variable.variant_fixes) [fc_b_name, fc_b_name ^ "'"]
52968
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   372
      ||>> mk_Frees "z" [B]
49043
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   373
      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT;
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   374
49498
acc583e14167 tuned variable names
blanchet
parents: 49486
diff changeset
   375
    val u = Free u';
acc583e14167 tuned variable names
blanchet
parents: 49486
diff changeset
   376
    val v = Free v';
49463
83ac281bcdc2 provide predicator, define relator
blanchet
parents: 49458
diff changeset
   377
    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
   378
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   379
    val xctrs = map2 (curry Term.list_comb) ctrs xss;
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   380
    val yctrs = map2 (curry Term.list_comb) ctrs yss;
49032
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   381
49043
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   382
    val xfs = map2 (curry Term.list_comb) fs xss;
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   383
    val xgs = map2 (curry Term.list_comb) gs xss;
bd3e33ee762d generate "split" property
blanchet
parents: 49034
diff changeset
   384
52968
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   385
    (* TODO: Eta-expension is for compatibility with the old datatype package (but it also provides
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   386
       nicer names). Consider removing. *)
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   387
    val eta_fs = map2 eta_expand_arg xss xfs;
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   388
    val eta_gs = map2 eta_expand_arg xss xgs;
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   389
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   390
    val case_binding =
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   391
      qualify false
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   392
        (if Binding.is_empty raw_case_binding orelse
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   393
            Binding.eq_name (raw_case_binding, standard_binding) then
54493
5b34a5b93ec2 use type suffixes instead of prefixes for 'case', '(un)fold', '(co)rec'
blanchet
parents: 54491
diff changeset
   394
           Binding.prefix_name (caseN ^ "_") fc_b
52968
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   395
         else
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   396
           raw_case_binding);
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   397
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   398
    fun mk_case_disj xctr xf xs =
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   399
      list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr), HOLogic.mk_eq (w, xf)));
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   400
53925
blanchet
parents: 53924
diff changeset
   401
    val case_rhs = fold_rev (fold_rev Term.lambda) [fs, [u]]
blanchet
parents: 53924
diff changeset
   402
      (Const (@{const_name The}, (B --> HOLogic.boolT) --> B) $
blanchet
parents: 53924
diff changeset
   403
         Term.lambda w (Library.foldr1 HOLogic.mk_disj (map3 mk_case_disj xctrs xfs xss)));
52968
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   404
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   405
    val ((raw_case, (_, raw_case_def)), (lthy', lthy)) = no_defs_lthy
54155
b964fad0cbbd conceal more ugly constructions
blanchet
parents: 54151
diff changeset
   406
      |> Local_Theory.define ((case_binding, NoSyn),
b964fad0cbbd conceal more ugly constructions
blanchet
parents: 54151
diff changeset
   407
        ((Binding.conceal (Thm.def_binding case_binding), []), case_rhs))
52968
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   408
      ||> `Local_Theory.restore;
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   409
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   410
    val phi = Proof_Context.export_morphism lthy lthy';
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   411
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   412
    val case_def = Morphism.thm phi raw_case_def;
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   413
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   414
    val case0 = Morphism.term phi raw_case;
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   415
    val casex = mk_case As B case0;
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   416
51759
587bba425430 eta-contracted weak congruence rules (like in the old package)
blanchet
parents: 51757
diff changeset
   417
    val fcase = Term.list_comb (casex, fs);
587bba425430 eta-contracted weak congruence rules (like in the old package)
blanchet
parents: 51757
diff changeset
   418
587bba425430 eta-contracted weak congruence rules (like in the old package)
blanchet
parents: 51757
diff changeset
   419
    val ufcase = fcase $ u;
587bba425430 eta-contracted weak congruence rules (like in the old package)
blanchet
parents: 51757
diff changeset
   420
    val vfcase = fcase $ v;
587bba425430 eta-contracted weak congruence rules (like in the old package)
blanchet
parents: 51757
diff changeset
   421
587bba425430 eta-contracted weak congruence rules (like in the old package)
blanchet
parents: 51757
diff changeset
   422
    val eta_fcase = Term.list_comb (casex, eta_fs);
587bba425430 eta-contracted weak congruence rules (like in the old package)
blanchet
parents: 51757
diff changeset
   423
    val eta_gcase = Term.list_comb (casex, eta_gs);
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   424
51759
587bba425430 eta-contracted weak congruence rules (like in the old package)
blanchet
parents: 51757
diff changeset
   425
    val eta_ufcase = eta_fcase $ u;
587bba425430 eta-contracted weak congruence rules (like in the old package)
blanchet
parents: 51757
diff changeset
   426
    val eta_vgcase = eta_gcase $ v;
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   427
49591
91b228e26348 generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents: 49586
diff changeset
   428
    fun mk_uu_eq () = HOLogic.mk_eq (u, u);
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   429
49591
91b228e26348 generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents: 49586
diff changeset
   430
    val uv_eq = mk_Trueprop_eq (u, v);
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   431
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   432
    val exist_xs_u_eq_ctrs =
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   433
      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
   434
51743
blanchet
parents: 51742
diff changeset
   435
    val unique_disc_no_def = TrueI; (*arbitrary marker*)
blanchet
parents: 51742
diff changeset
   436
    val alternate_disc_no_def = FalseE; (*arbitrary marker*)
blanchet
parents: 51742
diff changeset
   437
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   438
    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
   439
      HOLogic.mk_not
51790
22517d04d20b more intuitive syntax for equality-style discriminators of nullary constructors
blanchet
parents: 51787
diff changeset
   440
        (let val b = nth disc_bindings (k - 1) in
22517d04d20b more intuitive syntax for equality-style discriminators of nullary constructors
blanchet
parents: 51787
diff changeset
   441
           if is_disc_binding_valid b then get_udisc b (k - 1) else nth exist_xs_u_eq_ctrs (k - 1)
22517d04d20b more intuitive syntax for equality-style discriminators of nullary constructors
blanchet
parents: 51787
diff changeset
   442
         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
   443
53917
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   444
    val (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') =
52969
f2df0730f8ac clarified option name (since case/fold/rec are also destructors)
blanchet
parents: 52968
diff changeset
   445
      if no_discs_sels then
53917
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   446
        (true, [], [], [], [], [], lthy)
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   447
      else
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   448
        let
53908
blanchet
parents: 53906
diff changeset
   449
          fun disc_free b = Free (Binding.name_of b, mk_pred1T fcT);
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   450
54634
366297517091 reverted 141cb34744de and e78e7df36690 -- better provide nicer "eta-expanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents: 54626
diff changeset
   451
          fun disc_spec b exist_xs_u_eq_ctr = mk_Trueprop_eq (disc_free b $ u, exist_xs_u_eq_ctr);
366297517091 reverted 141cb34744de and e78e7df36690 -- better provide nicer "eta-expanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents: 54626
diff changeset
   452
49500
blanchet
parents: 49498
diff changeset
   453
          fun alternate_disc k =
blanchet
parents: 49498
diff changeset
   454
            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
   455
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   456
          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
   457
            map2 (fn Ts => fn k =>
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   458
              (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
   459
                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
   460
                (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
   461
                  NONE => fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T)
52968
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   462
                | SOME t => t |> Type.constraint (Ts ---> T) |> Syntax.check_term lthy)
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   463
              | 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
   464
54634
366297517091 reverted 141cb34744de and e78e7df36690 -- better provide nicer "eta-expanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents: 54626
diff changeset
   465
          fun sel_spec b proto_sels =
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   466
            let
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   467
              val _ =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   468
                (case duplicates (op =) (map fst proto_sels) of
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   469
                   k :: _ => error ("Duplicate selector name " ^ quote (Binding.name_of b) ^
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   470
                     " for constructor " ^
52968
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   471
                     quote (Syntax.string_of_term lthy (nth ctrs (k - 1))))
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   472
                 | [] => ())
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   473
              val T =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   474
                (case distinct (op =) (map (fastype_of o snd o snd) proto_sels) of
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   475
                  [T] => T
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   476
                | T :: T' :: _ => error ("Inconsistent range type for selector " ^
52968
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   477
                    quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ lthy T) ^ " vs. "
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   478
                    ^ quote (Syntax.string_of_typ lthy T')));
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   479
            in
54634
366297517091 reverted 141cb34744de and e78e7df36690 -- better provide nicer "eta-expanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents: 54626
diff changeset
   480
              mk_Trueprop_eq (Free (Binding.name_of b, fcT --> T) $ u,
366297517091 reverted 141cb34744de and e78e7df36690 -- better provide nicer "eta-expanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents: 54626
diff changeset
   481
                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
   482
            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
   483
49336
blanchet
parents: 49311
diff changeset
   484
          val sel_bindings = flat sel_bindingss;
blanchet
parents: 49311
diff changeset
   485
          val uniq_sel_bindings = distinct Binding.eq_name sel_bindings;
blanchet
parents: 49311
diff changeset
   486
          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
   487
49336
blanchet
parents: 49311
diff changeset
   488
          val sel_binding_index =
blanchet
parents: 49311
diff changeset
   489
            if all_sels_distinct then 1 upto length sel_bindings
blanchet
parents: 49311
diff changeset
   490
            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
   491
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
   492
          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
   493
          val sel_infos =
49336
blanchet
parents: 49311
diff changeset
   494
            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
   495
            |> sort (int_ord o pairself fst)
49336
blanchet
parents: 49311
diff changeset
   496
            |> map snd |> curry (op ~~) uniq_sel_bindings;
blanchet
parents: 49311
diff changeset
   497
          val sel_bindings = map fst sel_infos;
49258
84f13469d7f0 allow same selector name for several constructors
blanchet
parents: 49257
diff changeset
   498
49336
blanchet
parents: 49311
diff changeset
   499
          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
   500
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   501
          val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) =
52968
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   502
            lthy
51809
d4c1abbb4095 code tuning
blanchet
parents: 51798
diff changeset
   503
            |> apfst split_list o fold_map3 (fn k => fn exist_xs_u_eq_ctr => fn b =>
54634
366297517091 reverted 141cb34744de and e78e7df36690 -- better provide nicer "eta-expanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents: 54626
diff changeset
   504
                if Binding.is_empty b then
366297517091 reverted 141cb34744de and e78e7df36690 -- better provide nicer "eta-expanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents: 54626
diff changeset
   505
                  if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def)
366297517091 reverted 141cb34744de and e78e7df36690 -- better provide nicer "eta-expanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents: 54626
diff changeset
   506
                  else pair (alternate_disc k, alternate_disc_no_def)
366297517091 reverted 141cb34744de and e78e7df36690 -- better provide nicer "eta-expanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents: 54626
diff changeset
   507
                else if Binding.eq_name (b, equal_binding) then
366297517091 reverted 141cb34744de and e78e7df36690 -- better provide nicer "eta-expanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents: 54626
diff changeset
   508
                  pair (Term.lambda u exist_xs_u_eq_ctr, refl)
366297517091 reverted 141cb34744de and e78e7df36690 -- better provide nicer "eta-expanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents: 54626
diff changeset
   509
                else
366297517091 reverted 141cb34744de and e78e7df36690 -- better provide nicer "eta-expanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents: 54626
diff changeset
   510
                  Specification.definition (SOME (b, NONE, NoSyn),
366297517091 reverted 141cb34744de and e78e7df36690 -- better provide nicer "eta-expanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents: 54626
diff changeset
   511
                    ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr)) #>> apsnd snd)
366297517091 reverted 141cb34744de and e78e7df36690 -- better provide nicer "eta-expanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents: 54626
diff changeset
   512
              ks exist_xs_u_eq_ctrs disc_bindings
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   513
            ||>> apfst split_list o fold_map (fn (b, proto_sels) =>
54634
366297517091 reverted 141cb34744de and e78e7df36690 -- better provide nicer "eta-expanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents: 54626
diff changeset
   514
              Specification.definition (SOME (b, NONE, NoSyn),
366297517091 reverted 141cb34744de and e78e7df36690 -- better provide nicer "eta-expanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents: 54626
diff changeset
   515
                ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   516
            ||> `Local_Theory.restore;
49022
005ce926a932 define selectors and discriminators
blanchet
parents: 49020
diff changeset
   517
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   518
          val phi = Proof_Context.export_morphism lthy lthy';
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   519
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   520
          val disc_defs = map (Morphism.thm phi) raw_disc_defs;
49281
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   521
          val sel_defs = map (Morphism.thm phi) raw_sel_defs;
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   522
          val sel_defss = unflat_selss sel_defs;
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   523
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   524
          val discs0 = map (Morphism.term phi) raw_discs;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   525
          val selss0 = unflat_selss (map (Morphism.term phi) raw_sels);
49028
487427a02bee generate "disc_distinct" theorems
blanchet
parents: 49027
diff changeset
   526
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   527
          val discs = map (mk_disc_or_sel As) discs0;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   528
          val selss = map (map (mk_disc_or_sel As)) selss0;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   529
        in
53917
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   530
          (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy')
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   531
        end;
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   532
49032
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   533
    fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p);
49029
f0ecfa9575a9 generate "disc_exhaust" property
blanchet
parents: 49028
diff changeset
   534
49458
blanchet
parents: 49438
diff changeset
   535
    val exhaust_goal =
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   536
      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
   537
        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
   538
      end;
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   539
49484
0194a18f80cf finished "disc_coiter_iff" etc. generation
blanchet
parents: 49478
diff changeset
   540
    val inject_goalss =
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   541
      let
49034
b77e1910af8a make parallel list indexing possible for inject theorems
blanchet
parents: 49033
diff changeset
   542
        fun mk_goal _ _ [] [] = []
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   543
          | mk_goal xctr yctr xs ys =
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   544
            [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
   545
              Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys)))];
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   546
      in
49034
b77e1910af8a make parallel list indexing possible for inject theorems
blanchet
parents: 49033
diff changeset
   547
        map4 mk_goal xctrs yctrs xss yss
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   548
      end;
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   549
49484
0194a18f80cf finished "disc_coiter_iff" etc. generation
blanchet
parents: 49478
diff changeset
   550
    val half_distinct_goalss =
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   551
      let
49203
262ab1ac38b9 repaired constant types
blanchet
parents: 49201
diff changeset
   552
        fun mk_goal ((xs, xc), (xs', xc')) =
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   553
          fold_rev Logic.all (xs @ xs')
49203
262ab1ac38b9 repaired constant types
blanchet
parents: 49201
diff changeset
   554
            (HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (xc, xc'))));
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   555
      in
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49536
diff changeset
   556
        map (map mk_goal) (mk_half_pairss (`I (xss ~~ xctrs)))
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   557
      end;
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   558
52968
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   559
    val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss;
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   560
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   561
    fun after_qed thmss lthy =
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   562
      let
52968
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   563
        val ([exhaust_thm], (inject_thmss, half_distinct_thmss)) = (hd thmss, chop n (tl thmss));
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   564
49438
5bc80d96241e group "simps" together
blanchet
parents: 49437
diff changeset
   565
        val inject_thms = flat inject_thmss;
5bc80d96241e group "simps" together
blanchet
parents: 49437
diff changeset
   566
53210
7219c61796c0 simplify code (now that ctr_sugar uses the same type variables as fp_sugar)
blanchet
parents: 53040
diff changeset
   567
        val rho_As = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As);
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   568
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   569
        fun inst_thm t thm =
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   570
          Drule.instantiate' [] [SOME (certify lthy t)]
53210
7219c61796c0 simplify code (now that ctr_sugar uses the same type variables as fp_sugar)
blanchet
parents: 53040
diff changeset
   571
            (Thm.instantiate (rho_As, []) (Drule.zero_var_indexes thm));
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   572
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   573
        val uexhaust_thm = inst_thm u exhaust_thm;
49032
c2a7bedd57d8 generate "case_cong" property
blanchet
parents: 49031
diff changeset
   574
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   575
        val exhaust_cases = map base_name_of_ctr ctrs;
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   576
49048
4e0f0f98be02 rationalized data structure for distinctness theorems
blanchet
parents: 49046
diff changeset
   577
        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
   578
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   579
        val (distinct_thms, (distinct_thmsss', distinct_thmsss)) =
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49536
diff changeset
   580
          join_halves n half_distinct_thmss other_half_distinct_thmss ||> `transpose;
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   581
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   582
        val nchotomy_thm =
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   583
          let
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   584
            val goal =
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   585
              HOLogic.mk_Trueprop (HOLogic.mk_all (fst u', snd u',
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   586
                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
   587
          in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51380
diff changeset
   588
            Goal.prove_sorry 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
   589
            |> Thm.close_derivation
49020
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   590
          end;
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents: 49019
diff changeset
   591
52968
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   592
        val case_thms =
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   593
          let
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   594
            val goals =
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   595
              map3 (fn xctr => fn xf => fn xs =>
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   596
                fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (fcase $ xctr, xf))) xctrs xfs xss;
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   597
          in
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   598
            map4 (fn k => fn goal => fn injects => fn distinctss =>
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   599
                Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   600
                  mk_case_tac ctxt n k case_def injects distinctss)
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   601
                |> Thm.close_derivation)
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   602
              ks goals inject_thmss distinct_thmsss
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   603
          end;
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   604
53917
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   605
        val (case_cong_thm, weak_case_cong_thm) =
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   606
          let
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   607
            fun mk_prem xctr xs xf xg =
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   608
              fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (v, xctr),
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   609
                mk_Trueprop_eq (xf, xg)));
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   610
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   611
            val goal =
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   612
              Logic.list_implies (uv_eq :: map4 mk_prem xctrs xss xfs xgs,
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   613
                 mk_Trueprop_eq (eta_ufcase, eta_vgcase));
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   614
            val weak_goal = Logic.mk_implies (uv_eq, mk_Trueprop_eq (ufcase, vfcase));
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   615
          in
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   616
            (Goal.prove_sorry lthy [] [] goal (fn _ => mk_case_cong_tac lthy uexhaust_thm case_thms),
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   617
             Goal.prove_sorry lthy [] [] weak_goal (K (etac arg_cong 1)))
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   618
            |> pairself (Thm.close_derivation #> singleton (Proof_Context.export names_lthy lthy))
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   619
          end;
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   620
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   621
        val split_lhs = q $ ufcase;
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   622
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   623
        fun mk_split_conjunct xctr xs f_xs =
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   624
          list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (u, xctr), q $ f_xs));
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   625
        fun mk_split_disjunct xctr xs f_xs =
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   626
          list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr),
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   627
            HOLogic.mk_not (q $ f_xs)));
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   628
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   629
        fun mk_split_goal xctrs xss xfs =
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   630
          mk_Trueprop_eq (split_lhs, Library.foldr1 HOLogic.mk_conj
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   631
            (map3 mk_split_conjunct xctrs xss xfs));
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   632
        fun mk_split_asm_goal xctrs xss xfs =
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   633
          mk_Trueprop_eq (split_lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   634
            (map3 mk_split_disjunct xctrs xss xfs)));
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   635
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   636
        fun prove_split selss goal =
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   637
          Goal.prove_sorry lthy [] [] goal (fn _ =>
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   638
            mk_split_tac lthy uexhaust_thm case_thms selss inject_thmss distinct_thmsss)
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   639
          |> Thm.close_derivation
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   640
          |> singleton (Proof_Context.export names_lthy lthy);
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   641
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   642
        fun prove_split_asm asm_goal split_thm =
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   643
          Goal.prove_sorry lthy [] [] asm_goal (fn {context = ctxt, ...} =>
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   644
            mk_split_asm_tac ctxt split_thm)
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   645
          |> Thm.close_derivation
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   646
          |> singleton (Proof_Context.export names_lthy lthy);
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   647
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   648
        val (split_thm, split_asm_thm) =
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   649
          let
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   650
            val goal = mk_split_goal xctrs xss xfs;
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   651
            val asm_goal = mk_split_asm_goal xctrs xss xfs;
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   652
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   653
            val thm = prove_split (replicate n []) goal;
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   654
            val asm_thm = prove_split_asm asm_goal thm;
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   655
          in
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   656
            (thm, asm_thm)
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   657
          end;
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   658
53704
657c89169d1a include more "discI" rules
blanchet
parents: 53700
diff changeset
   659
        val (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms, nontriv_discI_thms,
53916
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53908
diff changeset
   660
             disc_exclude_thms, disc_exhaust_thms, sel_exhaust_thms, all_collapse_thms,
54491
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54435
diff changeset
   661
             safe_collapse_thms, expand_thms, sel_split_thms, sel_split_asm_thms, case_eq_if_thms) =
52969
f2df0730f8ac clarified option name (since case/fold/rec are also destructors)
blanchet
parents: 52968
diff changeset
   662
          if no_discs_sels then
53917
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   663
            ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
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
   664
          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
   665
            let
53917
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   666
              val udiscs = map (rapp u) discs;
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   667
              val uselss = map (map (rapp u)) selss;
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   668
              val usel_ctrs = map2 (curry Term.list_comb) ctrs uselss;
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   669
              val usel_fs = map2 (curry Term.list_comb) fs uselss;
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   670
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   671
              val vdiscs = map (rapp v) discs;
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   672
              val vselss = map (map (rapp v)) selss;
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   673
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
   674
              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
   675
                zero_var_indexes (Drule.gen_all (Drule.rename_bvars' (map (SOME o fst) xs')
54634
366297517091 reverted 141cb34744de and e78e7df36690 -- better provide nicer "eta-expanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents: 54626
diff changeset
   676
                    (Drule.forall_intr_vars (case_thm RS (sel_def RS trans)))));
49281
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   677
53704
657c89169d1a include more "discI" rules
blanchet
parents: 53700
diff changeset
   678
              val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss;
657c89169d1a include more "discI" rules
blanchet
parents: 53700
diff changeset
   679
49281
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   680
              fun has_undefined_rhs thm =
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   681
                (case snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))) of
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   682
                  Const (@{const_name undefined}, _) => true
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   683
                | _ => false);
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   684
3d87f4fd0d50 generate all sel theorems
blanchet
parents: 49280
diff changeset
   685
              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
   686
                (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
   687
                   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
   688
                 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
   689
                   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
   690
                     (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
   691
                |> filter_out has_undefined_rhs;
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   692
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   693
              fun mk_unique_disc_def () =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   694
                let
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   695
                  val m = the_single ms;
49591
91b228e26348 generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents: 49586
diff changeset
   696
                  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
   697
                in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51380
diff changeset
   698
                  Goal.prove_sorry lthy [] [] goal (fn _ => mk_unique_disc_def_tac m uexhaust_thm)
49692
a8a3b82b37f8 made code more conform to rest of BNF package
blanchet
parents: 49668
diff changeset
   699
                  |> Thm.close_derivation
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   700
                  |> singleton (Proof_Context.export names_lthy lthy)
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   701
                end;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   702
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   703
              fun mk_alternate_disc_def k =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   704
                let
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   705
                  val goal =
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   706
                    mk_Trueprop_eq (alternate_disc_lhs (K (nth udiscs)) (3 - k),
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   707
                      nth exist_xs_u_eq_ctrs (k - 1));
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   708
                in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51380
diff changeset
   709
                  Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
54634
366297517091 reverted 141cb34744de and e78e7df36690 -- better provide nicer "eta-expanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents: 54626
diff changeset
   710
                    mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k))
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   711
                      (nth distinct_thms (2 - k)) uexhaust_thm)
49692
a8a3b82b37f8 made code more conform to rest of BNF package
blanchet
parents: 49668
diff changeset
   712
                  |> Thm.close_derivation
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   713
                  |> singleton (Proof_Context.export names_lthy lthy)
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   714
                end;
49028
487427a02bee generate "disc_distinct" theorems
blanchet
parents: 49027
diff changeset
   715
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   716
              val has_alternate_disc_def =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   717
                exists (fn def => Thm.eq_thm_prop (def, alternate_disc_no_def)) disc_defs;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   718
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   719
              val disc_defs' =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   720
                map2 (fn k => fn def =>
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   721
                  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
   722
                  else if Thm.eq_thm_prop (def, alternate_disc_no_def) then mk_alternate_disc_def k
54634
366297517091 reverted 141cb34744de and e78e7df36690 -- better provide nicer "eta-expanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents: 54626
diff changeset
   723
                  else def) ks disc_defs;
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   724
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   725
              val discD_thms = map (fn def => def RS iffD1) disc_defs';
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   726
              val discI_thms =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   727
                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
   728
                  disc_defs';
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   729
              val not_discI_thms =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   730
                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
   731
                    (unfold_thms lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]})))
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   732
                  ms disc_defs';
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   733
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   734
              val (disc_thmss', disc_thmss) =
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   735
                let
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   736
                  fun mk_thm discI _ [] = refl RS discI
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   737
                    | mk_thm _ not_discI [distinct] = distinct RS not_discI;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   738
                  fun mk_thms discI not_discI distinctss = map (mk_thm discI not_discI) distinctss;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   739
                in
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   740
                  map3 mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   741
                end;
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   742
53704
657c89169d1a include more "discI" rules
blanchet
parents: 53700
diff changeset
   743
              val nontriv_disc_thms =
657c89169d1a include more "discI" rules
blanchet
parents: 53700
diff changeset
   744
                flat (map2 (fn b => if is_disc_binding_valid b then I else K [])
657c89169d1a include more "discI" rules
blanchet
parents: 53700
diff changeset
   745
                  disc_bindings disc_thmss);
657c89169d1a include more "discI" rules
blanchet
parents: 53700
diff changeset
   746
657c89169d1a include more "discI" rules
blanchet
parents: 53700
diff changeset
   747
              fun is_discI_boring b =
657c89169d1a include more "discI" rules
blanchet
parents: 53700
diff changeset
   748
                (n = 1 andalso Binding.is_empty b) orelse Binding.eq_name (b, equal_binding);
657c89169d1a include more "discI" rules
blanchet
parents: 53700
diff changeset
   749
657c89169d1a include more "discI" rules
blanchet
parents: 53700
diff changeset
   750
              val nontriv_discI_thms =
657c89169d1a include more "discI" rules
blanchet
parents: 53700
diff changeset
   751
                flat (map2 (fn b => if is_discI_boring b then K [] else single) disc_bindings
657c89169d1a include more "discI" rules
blanchet
parents: 53700
diff changeset
   752
                  discI_thms);
49028
487427a02bee generate "disc_distinct" theorems
blanchet
parents: 49027
diff changeset
   753
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   754
              val (disc_exclude_thms, (disc_exclude_thmsss', disc_exclude_thmsss)) =
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   755
                let
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   756
                  fun mk_goal [] = []
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   757
                    | mk_goal [((_, udisc), (_, udisc'))] =
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   758
                      [Logic.all u (Logic.mk_implies (HOLogic.mk_Trueprop udisc,
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   759
                         HOLogic.mk_Trueprop (HOLogic.mk_not udisc')))];
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   760
49667
44d85dc8ca08 use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents: 49633
diff changeset
   761
                  fun prove tac goal =
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51380
diff changeset
   762
                    Goal.prove_sorry lthy [] [] goal (K tac)
49667
44d85dc8ca08 use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents: 49633
diff changeset
   763
                    |> Thm.close_derivation;
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   764
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49536
diff changeset
   765
                  val half_pairss = mk_half_pairss (`I (ms ~~ discD_thms ~~ udiscs));
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   766
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   767
                  val half_goalss = map mk_goal half_pairss;
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   768
                  val half_thmss =
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   769
                    map3 (fn [] => K (K []) | [goal] => fn [(((m, discD), _), _)] =>
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51797
diff changeset
   770
                        fn disc_thm => [prove (mk_half_disc_exclude_tac lthy m discD disc_thm) goal])
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   771
                      half_goalss half_pairss (flat disc_thmss');
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   772
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   773
                  val other_half_goalss = map (mk_goal o map swap) half_pairss;
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   774
                  val other_half_thmss =
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   775
                    map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   776
                      other_half_goalss;
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   777
                in
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49536
diff changeset
   778
                  join_halves n half_thmss other_half_thmss ||> `transpose
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   779
                  |>> has_alternate_disc_def ? K []
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   780
                end;
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   781
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   782
              val disc_exhaust_thm =
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   783
                let
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   784
                  fun mk_prem udisc = mk_imp_p [HOLogic.mk_Trueprop udisc];
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   785
                  val goal = fold_rev Logic.all [p, u] (mk_imp_p (map mk_prem udiscs));
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   786
                in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51380
diff changeset
   787
                  Goal.prove_sorry lthy [] [] goal (fn _ =>
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   788
                    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
   789
                  |> Thm.close_derivation
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   790
                end;
49028
487427a02bee generate "disc_distinct" theorems
blanchet
parents: 49027
diff changeset
   791
53740
c1911450b84a cleaner handling of collapse theorems
blanchet
parents: 53704
diff changeset
   792
              val (safe_collapse_thms, all_collapse_thms) =
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   793
                let
54008
b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents: 54007
diff changeset
   794
                  fun mk_goal m udisc usel_ctr =
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   795
                    let
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   796
                      val prem = HOLogic.mk_Trueprop udisc;
53916
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53908
diff changeset
   797
                      val concl = mk_Trueprop_eq ((usel_ctr, u) |> m = 0 ? swap);
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   798
                    in
53740
c1911450b84a cleaner handling of collapse theorems
blanchet
parents: 53704
diff changeset
   799
                      (prem aconv concl, Logic.all u (Logic.mk_implies (prem, concl)))
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   800
                    end;
54008
b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents: 54007
diff changeset
   801
                  val (trivs, goals) = map3 mk_goal ms udiscs usel_ctrs |> split_list;
53740
c1911450b84a cleaner handling of collapse theorems
blanchet
parents: 53704
diff changeset
   802
                  val thms =
c1911450b84a cleaner handling of collapse theorems
blanchet
parents: 53704
diff changeset
   803
                    map5 (fn m => fn discD => fn sel_thms => fn triv => fn goal =>
c1911450b84a cleaner handling of collapse theorems
blanchet
parents: 53704
diff changeset
   804
                        Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
c1911450b84a cleaner handling of collapse theorems
blanchet
parents: 53704
diff changeset
   805
                          mk_collapse_tac ctxt m discD sel_thms ORELSE HEADGOAL atac)
c1911450b84a cleaner handling of collapse theorems
blanchet
parents: 53704
diff changeset
   806
                        |> Thm.close_derivation
c1911450b84a cleaner handling of collapse theorems
blanchet
parents: 53704
diff changeset
   807
                        |> not triv ? perhaps (try (fn thm => refl RS thm)))
c1911450b84a cleaner handling of collapse theorems
blanchet
parents: 53704
diff changeset
   808
                      ms discD_thms sel_thmss trivs goals;
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   809
                in
53740
c1911450b84a cleaner handling of collapse theorems
blanchet
parents: 53704
diff changeset
   810
                  (map_filter (fn (true, _) => NONE | (false, thm) => SOME thm) (trivs ~~ thms),
c1911450b84a cleaner handling of collapse theorems
blanchet
parents: 53704
diff changeset
   811
                   thms)
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   812
                end;
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   813
53916
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53908
diff changeset
   814
              val swapped_all_collapse_thms =
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53908
diff changeset
   815
                map2 (fn m => fn thm => if m = 0 then thm else thm RS sym) ms all_collapse_thms;
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53908
diff changeset
   816
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53908
diff changeset
   817
              val sel_exhaust_thm =
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53908
diff changeset
   818
                let
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53908
diff changeset
   819
                  fun mk_prem usel_ctr = mk_imp_p [mk_Trueprop_eq (u, usel_ctr)];
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53908
diff changeset
   820
                  val goal = fold_rev Logic.all [p, u] (mk_imp_p (map mk_prem usel_ctrs));
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53908
diff changeset
   821
                in
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53908
diff changeset
   822
                  Goal.prove_sorry lthy [] [] goal (fn _ =>
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53908
diff changeset
   823
                    mk_sel_exhaust_tac n disc_exhaust_thm swapped_all_collapse_thms)
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53908
diff changeset
   824
                  |> Thm.close_derivation
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53908
diff changeset
   825
                end;
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53908
diff changeset
   826
53919
blanchet
parents: 53917
diff changeset
   827
              val expand_thm =
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   828
                let
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   829
                  fun mk_prems k udisc usels vdisc vsels =
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   830
                    (if k = n then [] else [mk_Trueprop_eq (udisc, vdisc)]) @
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   831
                    (if null usels then
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   832
                       []
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   833
                     else
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   834
                       [Logic.list_implies
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   835
                          (if n = 1 then [] else map HOLogic.mk_Trueprop [udisc, vdisc],
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   836
                             HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   837
                               (map2 (curry HOLogic.mk_eq) usels vsels)))]);
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   838
49591
91b228e26348 generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents: 49586
diff changeset
   839
                  val goal =
91b228e26348 generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents: 49586
diff changeset
   840
                    Library.foldr Logic.list_implies
91b228e26348 generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents: 49586
diff changeset
   841
                      (map5 mk_prems ks udiscs uselss vdiscs vselss, uv_eq);
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   842
                  val uncollapse_thms =
53740
c1911450b84a cleaner handling of collapse theorems
blanchet
parents: 53704
diff changeset
   843
                    map2 (fn thm => fn [] => thm | _ => thm RS sym) all_collapse_thms uselss;
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   844
                in
53919
blanchet
parents: 53917
diff changeset
   845
                  Goal.prove_sorry lthy [] [] goal (fn _ =>
blanchet
parents: 53917
diff changeset
   846
                    mk_expand_tac lthy n ms (inst_thm u disc_exhaust_thm)
blanchet
parents: 53917
diff changeset
   847
                      (inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss
blanchet
parents: 53917
diff changeset
   848
                      disc_exclude_thmsss')
blanchet
parents: 53917
diff changeset
   849
                  |> Thm.close_derivation
blanchet
parents: 53917
diff changeset
   850
                  |> singleton (Proof_Context.export names_lthy lthy)
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   851
                end;
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   852
53917
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   853
              val (sel_split_thm, sel_split_asm_thm) =
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   854
                let
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   855
                  val zss = map (K []) xss;
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   856
                  val goal = mk_split_goal usel_ctrs zss usel_fs;
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   857
                  val asm_goal = mk_split_asm_goal usel_ctrs zss usel_fs;
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   858
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   859
                  val thm = prove_split sel_thmss goal;
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   860
                  val asm_thm = prove_split_asm asm_goal thm;
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   861
                in
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   862
                  (thm, asm_thm)
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   863
                end;
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   864
54491
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54435
diff changeset
   865
              val case_eq_if_thm =
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   866
                let
53917
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   867
                  val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs usel_fs);
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   868
                in
53919
blanchet
parents: 53917
diff changeset
   869
                  Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
54491
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54435
diff changeset
   870
                    mk_case_eq_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)
53919
blanchet
parents: 53917
diff changeset
   871
                  |> Thm.close_derivation
blanchet
parents: 53917
diff changeset
   872
                  |> singleton (Proof_Context.export names_lthy lthy)
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   873
                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
   874
            in
53704
657c89169d1a include more "discI" rules
blanchet
parents: 53700
diff changeset
   875
              (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms,
53916
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53908
diff changeset
   876
               nontriv_discI_thms, disc_exclude_thms, [disc_exhaust_thm], [sel_exhaust_thm],
53919
blanchet
parents: 53917
diff changeset
   877
               all_collapse_thms, safe_collapse_thms, [expand_thm], [sel_split_thm],
54491
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54435
diff changeset
   878
               [sel_split_asm_thm], [case_eq_if_thm])
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
   879
            end;
49025
7e89b0520e83 more work on sugar
blanchet
parents: 49023
diff changeset
   880
49437
c139da00fb4a register induct attributes
blanchet
parents: 49434
diff changeset
   881
        val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
53908
blanchet
parents: 53906
diff changeset
   882
        val cases_type_attr = Attrib.internal (K (Induct.cases_type fcT_name));
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   883
54151
71dc4e6c001c set code attribute on discriminator equations
blanchet
parents: 54145
diff changeset
   884
        val anonymous_notes =
71dc4e6c001c set code attribute on discriminator equations
blanchet
parents: 54145
diff changeset
   885
          [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs),
71dc4e6c001c set code attribute on discriminator equations
blanchet
parents: 54145
diff changeset
   886
           (map (fn th => th RS @{thm eq_False[THEN iffD2]}
71dc4e6c001c set code attribute on discriminator equations
blanchet
parents: 54145
diff changeset
   887
              handle THM _ => th RS @{thm eq_True[THEN iffD2]}) nontriv_disc_thms,
71dc4e6c001c set code attribute on discriminator equations
blanchet
parents: 54145
diff changeset
   888
            code_nitpicksimp_attrs)]
71dc4e6c001c set code attribute on discriminator equations
blanchet
parents: 54145
diff changeset
   889
          |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
71dc4e6c001c set code attribute on discriminator equations
blanchet
parents: 54145
diff changeset
   890
49052
3510b943dd5b optimized "mk_split_tac" + use "notes"
blanchet
parents: 49050
diff changeset
   891
        val notes =
54145
297d1c603999 make sure that registered code equations are actually equations
blanchet
parents: 54008
diff changeset
   892
          [(caseN, case_thms, code_nitpicksimp_simp_attrs),
49594
55e798614c45 tweaked theorem names (in particular, dropped s's)
blanchet
parents: 49591
diff changeset
   893
           (case_congN, [case_cong_thm], []),
54491
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54435
diff changeset
   894
           (case_eq_ifN, case_eq_if_thms, []),
53740
c1911450b84a cleaner handling of collapse theorems
blanchet
parents: 53704
diff changeset
   895
           (collapseN, safe_collapse_thms, simp_attrs),
53704
657c89169d1a include more "discI" rules
blanchet
parents: 53700
diff changeset
   896
           (discN, nontriv_disc_thms, simp_attrs),
53700
e6a44d775be3 note "discI"
blanchet
parents: 53694
diff changeset
   897
           (discIN, nontriv_discI_thms, []),
53836
a1632a5f5fb3 added [dest] to "disc_exclude"
blanchet
parents: 53810
diff changeset
   898
           (disc_excludeN, disc_exclude_thms, dest_attrs),
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   899
           (disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]),
54145
297d1c603999 make sure that registered code equations are actually equations
blanchet
parents: 54008
diff changeset
   900
           (distinctN, distinct_thms, simp_attrs @ inductsimp_attrs),
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   901
           (exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]),
49486
64cc57c0d0fe generate "expand" property
blanchet
parents: 49484
diff changeset
   902
           (expandN, expand_thms, []),
54145
297d1c603999 make sure that registered code equations are actually equations
blanchet
parents: 54008
diff changeset
   903
           (injectN, inject_thms, iff_attrs @ inductsimp_attrs),
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   904
           (nchotomyN, [nchotomy_thm], []),
54145
297d1c603999 make sure that registered code equations are actually equations
blanchet
parents: 54008
diff changeset
   905
           (selN, all_sel_thms, code_nitpicksimp_simp_attrs),
53916
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53908
diff changeset
   906
           (sel_exhaustN, sel_exhaust_thms, [exhaust_case_names_attr]),
53917
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   907
           (sel_splitN, sel_split_thms, []),
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   908
           (sel_split_asmN, sel_split_asm_thms, []),
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   909
           (splitN, [split_thm], []),
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   910
           (split_asmN, [split_asm_thm], []),
49633
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
   911
           (splitsN, [split_thm, split_asm_thm], []),
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   912
           (weak_case_cong_thmsN, [weak_case_cong_thm], cong_attrs)]
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   913
          |> filter_out (null o #2)
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   914
          |> map (fn (thmN, thms, attrs) =>
49633
5b5450bc544c compatibility option to use "rep_datatype"
blanchet
parents: 49622
diff changeset
   915
            ((qualify true (Binding.name thmN), attrs), [(thms, [])]));
49300
c707df2e2083 added attributes to theorems
blanchet
parents: 49298
diff changeset
   916
53867
8ad44ecc0d15 keep a database of free constructor type information
blanchet
parents: 53864
diff changeset
   917
        val ctr_sugar =
8ad44ecc0d15 keep a database of free constructor type information
blanchet
parents: 53864
diff changeset
   918
          {ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
8ad44ecc0d15 keep a database of free constructor type information
blanchet
parents: 53864
diff changeset
   919
           nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
8ad44ecc0d15 keep a database of free constructor type information
blanchet
parents: 53864
diff changeset
   920
           case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm,
8ad44ecc0d15 keep a database of free constructor type information
blanchet
parents: 53864
diff changeset
   921
           split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss,
8ad44ecc0d15 keep a database of free constructor type information
blanchet
parents: 53864
diff changeset
   922
           discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms,
53916
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53908
diff changeset
   923
           sel_exhausts = sel_exhaust_thms, collapses = all_collapse_thms, expands = expand_thms,
53917
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   924
           sel_splits = sel_split_thms, sel_split_asms = sel_split_asm_thms,
54491
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54435
diff changeset
   925
           case_eq_ifs = case_eq_if_thms};
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   926
      in
53867
8ad44ecc0d15 keep a database of free constructor type information
blanchet
parents: 53864
diff changeset
   927
        (ctr_sugar,
51819
9df935196be9 use record instead of big tuple
blanchet
parents: 51809
diff changeset
   928
         lthy
9df935196be9 use record instead of big tuple
blanchet
parents: 51809
diff changeset
   929
         |> not rep_compat ?
54615
62fb5af93fe2 generalized datatype code generation code so that it works with old-style and new-style (co)datatypes (as long as they are not local)
blanchet
parents: 54493
diff changeset
   930
            Local_Theory.declaration {syntax = false, pervasive = true}
62fb5af93fe2 generalized datatype code generation code so that it works with old-style and new-style (co)datatypes (as long as they are not local)
blanchet
parents: 54493
diff changeset
   931
              (fn phi => Case_Translation.register
62fb5af93fe2 generalized datatype code generation code so that it works with old-style and new-style (co)datatypes (as long as they are not local)
blanchet
parents: 54493
diff changeset
   932
                 (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
54626
8a5e82425e55 added 'no_code' option
blanchet
parents: 54622
diff changeset
   933
         |> (not no_code andalso null (Thm.hyps_of (hd case_thms)))
54617
1183bd511980 don't try to register code equations in a locale with assumptions
blanchet
parents: 54615
diff changeset
   934
           ? Local_Theory.background_theory
54635
30666a281ae3 proper code generation for discriminators/selectors
blanchet
parents: 54634
diff changeset
   935
               (fold (fold Code.del_eqn) [disc_defs, sel_defs]
30666a281ae3 proper code generation for discriminators/selectors
blanchet
parents: 54634
diff changeset
   936
                #> add_ctr_code fcT_name As (map dest_Const ctrs) inject_thms distinct_thms
30666a281ae3 proper code generation for discriminators/selectors
blanchet
parents: 54634
diff changeset
   937
                  case_thms)
30666a281ae3 proper code generation for discriminators/selectors
blanchet
parents: 54634
diff changeset
   938
         |> Local_Theory.notes (anonymous_notes @ notes) |> snd
30666a281ae3 proper code generation for discriminators/selectors
blanchet
parents: 54634
diff changeset
   939
         |> register_ctr_sugar fcT_name ctr_sugar)
49019
fc4decdba5ce more work on BNF sugar
blanchet
parents: 49017
diff changeset
   940
      end;
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   941
  in
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49120
diff changeset
   942
    (goalss, after_qed, lthy')
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   943
  end;
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   944
51781
0504e286d66d renamed "wrap_data" to "wrap_free_constructors"
blanchet
parents: 51777
diff changeset
   945
fun wrap_free_constructors tacss = (fn (goalss, after_qed, lthy) =>
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51380
diff changeset
   946
  map2 (map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])) goalss tacss
51781
0504e286d66d renamed "wrap_data" to "wrap_free_constructors"
blanchet
parents: 51777
diff changeset
   947
  |> (fn thms => after_qed thms lthy)) oo prepare_wrap_free_constructors (K I);
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   948
51781
0504e286d66d renamed "wrap_data" to "wrap_free_constructors"
blanchet
parents: 51777
diff changeset
   949
val wrap_free_constructors_cmd = (fn (goalss, after_qed, lthy) =>
49297
47fbf2e3e89c provide a programmatic interface for FP sugar
blanchet
parents: 49286
diff changeset
   950
  Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
51781
0504e286d66d renamed "wrap_data" to "wrap_free_constructors"
blanchet
parents: 51777
diff changeset
   951
  prepare_wrap_free_constructors Syntax.read_term;
49297
47fbf2e3e89c provide a programmatic interface for FP sugar
blanchet
parents: 49286
diff changeset
   952
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   953
fun parse_bracket_list parser = @{keyword "["} |-- Parse.list parser --|  @{keyword "]"};
49111
9d511132394e export "wrap" function
blanchet
parents: 49075
diff changeset
   954
51790
22517d04d20b more intuitive syntax for equality-style discriminators of nullary constructors
blanchet
parents: 51787
diff changeset
   955
val parse_bindings = parse_bracket_list parse_binding;
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   956
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
   957
51790
22517d04d20b more intuitive syntax for equality-style discriminators of nullary constructors
blanchet
parents: 51787
diff changeset
   958
val parse_bound_term = (parse_binding --| @{keyword ":"}) -- Parse.term;
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   959
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
   960
val parse_bound_termss = parse_bracket_list parse_bound_terms;
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   961
52823
blanchet
parents: 52375
diff changeset
   962
val parse_wrap_free_constructors_options =
54626
8a5e82425e55 added 'no_code' option
blanchet
parents: 54622
diff changeset
   963
  Scan.optional (@{keyword "("} |-- Parse.list1
8a5e82425e55 added 'no_code' option
blanchet
parents: 54622
diff changeset
   964
        (Parse.reserved "no_discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1 ||
8a5e82425e55 added 'no_code' option
blanchet
parents: 54622
diff changeset
   965
         Parse.reserved "rep_compat" >> K 2) --| @{keyword ")"}
8a5e82425e55 added 'no_code' option
blanchet
parents: 54622
diff changeset
   966
      >> (fn js => (member (op =) js 0, (member (op =) js 1, member (op =) js 2))))
8a5e82425e55 added 'no_code' option
blanchet
parents: 54622
diff changeset
   967
    (false, (false, false));
49278
718e4ad1517e added no_dests option
blanchet
parents: 49277
diff changeset
   968
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   969
val _ =
51781
0504e286d66d renamed "wrap_data" to "wrap_free_constructors"
blanchet
parents: 51777
diff changeset
   970
  Outer_Syntax.local_theory_to_proof @{command_spec "wrap_free_constructors"}
51797
182454c06a80 tuned ML and thy file names
blanchet
parents: 51790
diff changeset
   971
    "wrap an existing freely generated type's constructors"
52823
blanchet
parents: 52375
diff changeset
   972
    ((parse_wrap_free_constructors_options -- (@{keyword "["} |-- Parse.list Parse.term --|
blanchet
parents: 52375
diff changeset
   973
        @{keyword "]"}) --
52968
2b430bbb5a1a define case constant from other 'free constructor' axioms
blanchet
parents: 52965
diff changeset
   974
      parse_binding -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss --
49280
52413dc96326 allow default values for selectors in low-level "wrap_data" command
blanchet
parents: 49278
diff changeset
   975
        Scan.optional parse_bound_termss []) ([], [])) ([], ([], [])))
51781
0504e286d66d renamed "wrap_data" to "wrap_free_constructors"
blanchet
parents: 51777
diff changeset
   976
     >> wrap_free_constructors_cmd);
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   977
66fc7fc2d49b started work on datatype sugar
blanchet
parents:
diff changeset
   978
end;