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