src/HOL/Tools/BNF/bnf_def.ML
author haftmann
Tue Oct 13 09:21:15 2015 +0200 (2015-10-13)
changeset 61424 c3658c18b7bc
parent 61334 8d40ddaa427f
child 61760 1647bb489522
permissions -rw-r--r--
prod_case as canonical name for product type eliminator
blanchet@55061
     1
(*  Title:      HOL/Tools/BNF/bnf_def.ML
blanchet@48975
     2
    Author:     Dmitriy Traytel, TU Muenchen
blanchet@48975
     3
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@57668
     4
    Author:     Martin Desharnais, TU Muenchen
blanchet@57668
     5
    Copyright   2012, 2013, 2014
blanchet@48975
     6
blanchet@48975
     7
Definition of bounded natural functors.
blanchet@48975
     8
*)
blanchet@48975
     9
blanchet@48975
    10
signature BNF_DEF =
blanchet@48975
    11
sig
blanchet@51837
    12
  type bnf
blanchet@48975
    13
  type nonemptiness_witness = {I: int list, wit: term, prop: thm list}
blanchet@48975
    14
blanchet@51837
    15
  val morph_bnf: morphism -> bnf -> bnf
traytel@56016
    16
  val morph_bnf_defs: morphism -> bnf -> bnf
blanchet@58175
    17
  val transfer_bnf: theory -> bnf -> bnf
blanchet@51837
    18
  val bnf_of: Proof.context -> string -> bnf option
blanchet@58116
    19
  val bnf_of_global: theory -> string -> bnf option
wenzelm@58659
    20
  val bnf_interpretation: string -> (bnf -> local_theory -> local_theory) -> theory -> theory
blanchet@58188
    21
  val interpret_bnf: (string -> bool) -> bnf -> local_theory -> local_theory
blanchet@58177
    22
  val register_bnf_raw: string -> bnf -> local_theory -> local_theory
blanchet@58188
    23
  val register_bnf: (string -> bool) -> string -> bnf -> local_theory -> local_theory
traytel@49434
    24
blanchet@51837
    25
  val name_of_bnf: bnf -> binding
blanchet@51837
    26
  val T_of_bnf: bnf -> typ
blanchet@51837
    27
  val live_of_bnf: bnf -> int
blanchet@51837
    28
  val lives_of_bnf: bnf -> typ list
blanchet@51837
    29
  val dead_of_bnf: bnf -> int
blanchet@51837
    30
  val deads_of_bnf: bnf -> typ list
blanchet@56346
    31
  val bd_of_bnf: bnf -> term
blanchet@51837
    32
  val nwits_of_bnf: bnf -> int
blanchet@48975
    33
blanchet@48975
    34
  val mapN: string
blanchet@49507
    35
  val relN: string
blanchet@48975
    36
  val setN: string
blanchet@48975
    37
  val mk_setN: int -> string
traytel@55025
    38
  val mk_witN: int -> string
blanchet@48975
    39
blanchet@51837
    40
  val map_of_bnf: bnf -> term
blanchet@51837
    41
  val sets_of_bnf: bnf -> term list
blanchet@51837
    42
  val rel_of_bnf: bnf -> term
blanchet@49214
    43
blanchet@51837
    44
  val mk_T_of_bnf: typ list -> typ list -> bnf -> typ
blanchet@51837
    45
  val mk_bd_of_bnf: typ list -> typ list -> bnf -> term
blanchet@51837
    46
  val mk_map_of_bnf: typ list -> typ list -> typ list -> bnf -> term
blanchet@51837
    47
  val mk_rel_of_bnf: typ list -> typ list -> typ list -> bnf -> term
blanchet@51837
    48
  val mk_sets_of_bnf: typ list list -> typ list list -> bnf -> term list
blanchet@51837
    49
  val mk_wits_of_bnf: typ list list -> typ list list -> bnf -> (int list * term) list
blanchet@48975
    50
blanchet@51837
    51
  val bd_Card_order_of_bnf: bnf -> thm
blanchet@51837
    52
  val bd_Cinfinite_of_bnf: bnf -> thm
blanchet@51837
    53
  val bd_Cnotzero_of_bnf: bnf -> thm
blanchet@51837
    54
  val bd_card_order_of_bnf: bnf -> thm
blanchet@51837
    55
  val bd_cinfinite_of_bnf: bnf -> thm
blanchet@51837
    56
  val collect_set_map_of_bnf: bnf -> thm
blanchet@51837
    57
  val in_bd_of_bnf: bnf -> thm
blanchet@51837
    58
  val in_cong_of_bnf: bnf -> thm
blanchet@51837
    59
  val in_mono_of_bnf: bnf -> thm
traytel@51893
    60
  val in_rel_of_bnf: bnf -> thm
blanchet@56635
    61
  val inj_map_of_bnf: bnf -> thm
desharna@57970
    62
  val inj_map_strong_of_bnf: bnf -> thm
blanchet@53287
    63
  val map_comp0_of_bnf: bnf -> thm
blanchet@53288
    64
  val map_comp_of_bnf: bnf -> thm
blanchet@51837
    65
  val map_cong0_of_bnf: bnf -> thm
blanchet@51837
    66
  val map_cong_of_bnf: bnf -> thm
desharna@57981
    67
  val map_cong_simp_of_bnf: bnf -> thm
blanchet@51837
    68
  val map_def_of_bnf: bnf -> thm
blanchet@53270
    69
  val map_id0_of_bnf: bnf -> thm
blanchet@53285
    70
  val map_id_of_bnf: bnf -> thm
blanchet@57399
    71
  val map_ident0_of_bnf: bnf -> thm
desharna@56903
    72
  val map_ident_of_bnf: bnf -> thm
traytel@52719
    73
  val map_transfer_of_bnf: bnf -> thm
traytel@54841
    74
  val le_rel_OO_of_bnf: bnf -> thm
blanchet@51837
    75
  val rel_def_of_bnf: bnf -> thm
traytel@51893
    76
  val rel_Grp_of_bnf: bnf -> thm
traytel@51893
    77
  val rel_OO_of_bnf: bnf -> thm
traytel@51893
    78
  val rel_OO_Grp_of_bnf: bnf -> thm
traytel@61242
    79
  val rel_cong0_of_bnf: bnf -> thm
traytel@51893
    80
  val rel_cong_of_bnf: bnf -> thm
traytel@61242
    81
  val rel_cong_simp_of_bnf: bnf -> thm
traytel@51893
    82
  val rel_conversep_of_bnf: bnf -> thm
traytel@51893
    83
  val rel_mono_of_bnf: bnf -> thm
desharna@57967
    84
  val rel_mono_strong0_of_bnf: bnf -> thm
desharna@57968
    85
  val rel_mono_strong_of_bnf: bnf -> thm
traytel@59726
    86
  val rel_refl_of_bnf: bnf -> thm
traytel@61240
    87
  val rel_refl_strong_of_bnf: bnf -> thm
traytel@61240
    88
  val rel_reflp_of_bnf: bnf -> thm
traytel@61240
    89
  val rel_symp_of_bnf: bnf -> thm
traytel@61240
    90
  val rel_transp_of_bnf: bnf -> thm
traytel@60742
    91
  val rel_map_of_bnf: bnf -> thm list
desharna@58106
    92
  val rel_transfer_of_bnf: bnf -> thm
blanchet@51837
    93
  val rel_eq_of_bnf: bnf -> thm
blanchet@51837
    94
  val rel_flip_of_bnf: bnf -> thm
blanchet@51837
    95
  val set_bd_of_bnf: bnf -> thm list
blanchet@51837
    96
  val set_defs_of_bnf: bnf -> thm list
blanchet@53289
    97
  val set_map0_of_bnf: bnf -> thm list
blanchet@53290
    98
  val set_map_of_bnf: bnf -> thm list
desharna@58106
    99
  val set_transfer_of_bnf: bnf -> thm list
blanchet@51837
   100
  val wit_thms_of_bnf: bnf -> thm list
blanchet@51837
   101
  val wit_thmss_of_bnf: bnf -> thm list list
blanchet@48975
   102
blanchet@54236
   103
  val mk_map: int -> typ list -> typ list -> term -> term
blanchet@54236
   104
  val mk_rel: int -> typ list -> typ list -> term -> term
desharna@57303
   105
  val build_map: Proof.context -> typ list -> (typ * typ -> term) -> typ * typ -> term
desharna@58104
   106
  val build_rel: (string * (int * term)) list -> Proof.context -> typ list -> (typ * typ -> term) ->
desharna@58104
   107
    typ * typ -> term
blanchet@54246
   108
  val flatten_type_args_of_bnf: bnf -> 'a -> 'a list -> 'a list
blanchet@54246
   109
  val map_flattened_map_args: Proof.context -> string -> (term list -> 'a list) -> term list ->
blanchet@54246
   110
    'a list
blanchet@54236
   111
blanchet@48975
   112
  val mk_witness: int list * term -> thm list -> nonemptiness_witness
traytel@60918
   113
  val mk_wit_goals: term list -> term list -> term list -> int list * term -> term list
traytel@49103
   114
  val minimize_wits: (''a list * 'b) list -> (''a list * 'b) list
blanchet@51837
   115
  val wits_of_bnf: bnf -> nonemptiness_witness list
blanchet@48975
   116
traytel@52635
   117
  val zip_axioms: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list
blanchet@49456
   118
blanchet@55854
   119
  datatype inline_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline
blanchet@49538
   120
  datatype fact_policy = Dont_Note | Note_Some | Note_All
blanchet@49538
   121
blanchet@48975
   122
  val bnf_note_all: bool Config.T
traytel@53143
   123
  val bnf_timing: bool Config.T
traytel@49435
   124
  val user_policy: fact_policy -> Proof.context -> fact_policy
traytel@52720
   125
  val note_bnf_thms: fact_policy -> (binding -> binding) -> binding -> bnf -> Proof.context ->
blanchet@57631
   126
    bnf * Proof.context
blanchet@48975
   127
blanchet@48975
   128
  val print_bnfs: Proof.context -> unit
traytel@56016
   129
  val prepare_def: inline_policy -> (Proof.context -> fact_policy) -> bool ->
traytel@56016
   130
    (binding -> binding) -> (Proof.context -> 'a -> typ) -> (Proof.context -> 'b -> term) ->
traytel@56016
   131
    typ list option -> binding -> binding -> binding list ->
traytel@54601
   132
    (((((binding * 'a) * 'b) * 'b list) * 'b) * 'b list) * 'b option -> Proof.context ->
blanchet@58189
   133
    string * term list * ((Proof.context -> thm list -> tactic) option * term list list) *
traytel@54601
   134
    ((thm list -> thm list list) -> thm list list -> Proof.context -> bnf * local_theory) *
traytel@54601
   135
    local_theory * thm list
traytel@56016
   136
  val define_bnf_consts: inline_policy -> fact_policy -> bool -> typ list option ->
traytel@54841
   137
    binding -> binding -> binding list ->
traytel@54841
   138
    (((((binding * typ) * term) * term list) * term) * term list) * term option -> local_theory ->
traytel@54841
   139
      ((typ list * typ list * typ list * typ) *
traytel@54841
   140
       (term * term list * term * (int list * term) list * term) *
traytel@54841
   141
       (thm * thm list * thm * thm list * thm) *
traytel@54841
   142
       ((typ list -> typ list -> typ list -> term) *
traytel@54841
   143
        (typ list -> typ list -> term -> term) *
traytel@54841
   144
        (typ list -> typ list -> typ -> typ) *
traytel@54841
   145
        (typ list -> typ list -> typ list -> term) *
traytel@54841
   146
        (typ list -> typ list -> typ list -> term))) * local_theory
traytel@54841
   147
traytel@56016
   148
  val bnf_def: inline_policy -> (Proof.context -> fact_policy) -> bool -> (binding -> binding) ->
blanchet@58189
   149
    (Proof.context -> tactic) list -> (Proof.context -> tactic) -> typ list option -> binding ->
blanchet@51767
   150
    binding -> binding list ->
blanchet@58189
   151
    (((((binding * typ) * term) * term list) * term) * term list) * term option -> local_theory ->
blanchet@58189
   152
    bnf * local_theory
blanchet@61301
   153
  val bnf_cmd: ((((((binding * string) * string) * string list) * string) * string list)
blanchet@61301
   154
      * string option) * (Proof.context -> Plugin_Name.filter) ->
blanchet@61301
   155
    Proof.context -> Proof.state
blanchet@48975
   156
end;
blanchet@48975
   157
blanchet@48975
   158
structure BNF_Def : BNF_DEF =
blanchet@48975
   159
struct
blanchet@48975
   160
blanchet@48975
   161
open BNF_Util
blanchet@49463
   162
open BNF_Tactics
blanchet@49284
   163
open BNF_Def_Tactics
blanchet@48975
   164
blanchet@54624
   165
val fundefcong_attrs = @{attributes [fundef_cong]};
blanchet@58344
   166
val mono_attrs = @{attributes [mono]};
blanchet@51765
   167
blanchet@48975
   168
type axioms = {
blanchet@53270
   169
  map_id0: thm,
blanchet@53287
   170
  map_comp0: thm,
blanchet@51761
   171
  map_cong0: thm,
blanchet@53289
   172
  set_map0: thm list,
blanchet@48975
   173
  bd_card_order: thm,
blanchet@48975
   174
  bd_cinfinite: thm,
blanchet@48975
   175
  set_bd: thm list,
traytel@54841
   176
  le_rel_OO: thm,
traytel@51893
   177
  rel_OO_Grp: thm
blanchet@48975
   178
};
blanchet@48975
   179
traytel@54841
   180
fun mk_axioms' ((((((((id, comp), cong), map), c_o), cinf), set_bd), le_rel_OO), rel) =
blanchet@53289
   181
  {map_id0 = id, map_comp0 = comp, map_cong0 = cong, set_map0 = map, bd_card_order = c_o,
traytel@54841
   182
   bd_cinfinite = cinf, set_bd = set_bd, le_rel_OO = le_rel_OO, rel_OO_Grp = rel};
blanchet@48975
   183
wenzelm@51930
   184
fun dest_cons [] = raise List.Empty
blanchet@48975
   185
  | dest_cons (x :: xs) = (x, xs);
blanchet@48975
   186
blanchet@48975
   187
fun mk_axioms n thms = thms
blanchet@48975
   188
  |> map the_single
blanchet@48975
   189
  |> dest_cons
blanchet@48975
   190
  ||>> dest_cons
blanchet@48975
   191
  ||>> dest_cons
blanchet@48975
   192
  ||>> chop n
blanchet@48975
   193
  ||>> dest_cons
blanchet@48975
   194
  ||>> dest_cons
blanchet@48975
   195
  ||>> chop n
blanchet@48975
   196
  ||>> dest_cons
blanchet@48975
   197
  ||> the_single
blanchet@48975
   198
  |> mk_axioms';
blanchet@48975
   199
traytel@54841
   200
fun zip_axioms mid mcomp mcong smap bdco bdinf sbd le_rel_OO rel =
traytel@54841
   201
  [mid, mcomp, mcong] @ smap @ [bdco, bdinf] @ sbd @ [le_rel_OO, rel];
blanchet@49460
   202
blanchet@53289
   203
fun dest_axioms {map_id0, map_comp0, map_cong0, set_map0, bd_card_order, bd_cinfinite, set_bd,
traytel@54841
   204
  le_rel_OO, rel_OO_Grp} =
traytel@54841
   205
  zip_axioms map_id0 map_comp0 map_cong0 set_map0 bd_card_order bd_cinfinite set_bd le_rel_OO
traytel@51893
   206
    rel_OO_Grp;
blanchet@48975
   207
blanchet@53289
   208
fun map_axioms f {map_id0, map_comp0, map_cong0, set_map0, bd_card_order, bd_cinfinite, set_bd,
traytel@54841
   209
  le_rel_OO, rel_OO_Grp} =
blanchet@53270
   210
  {map_id0 = f map_id0,
blanchet@53287
   211
    map_comp0 = f map_comp0,
blanchet@51761
   212
    map_cong0 = f map_cong0,
blanchet@53289
   213
    set_map0 = map f set_map0,
blanchet@49463
   214
    bd_card_order = f bd_card_order,
blanchet@49463
   215
    bd_cinfinite = f bd_cinfinite,
blanchet@49463
   216
    set_bd = map f set_bd,
traytel@54841
   217
    le_rel_OO = f le_rel_OO,
traytel@51893
   218
    rel_OO_Grp = f rel_OO_Grp};
blanchet@48975
   219
blanchet@48975
   220
val morph_axioms = map_axioms o Morphism.thm;
blanchet@48975
   221
blanchet@48975
   222
type defs = {
blanchet@48975
   223
  map_def: thm,
blanchet@48975
   224
  set_defs: thm list,
traytel@51893
   225
  rel_def: thm
blanchet@48975
   226
}
blanchet@48975
   227
traytel@51893
   228
fun mk_defs map sets rel = {map_def = map, set_defs = sets, rel_def = rel};
blanchet@48975
   229
traytel@51893
   230
fun map_defs f {map_def, set_defs, rel_def} =
traytel@51893
   231
  {map_def = f map_def, set_defs = map f set_defs, rel_def = f rel_def};
blanchet@48975
   232
blanchet@48975
   233
val morph_defs = map_defs o Morphism.thm;
blanchet@48975
   234
blanchet@48975
   235
type facts = {
blanchet@48975
   236
  bd_Card_order: thm,
blanchet@48975
   237
  bd_Cinfinite: thm,
blanchet@48975
   238
  bd_Cnotzero: thm,
blanchet@51766
   239
  collect_set_map: thm lazy,
traytel@52635
   240
  in_bd: thm lazy,
blanchet@48975
   241
  in_cong: thm lazy,
blanchet@48975
   242
  in_mono: thm lazy,
traytel@51893
   243
  in_rel: thm lazy,
blanchet@56635
   244
  inj_map: thm lazy,
desharna@57970
   245
  inj_map_strong: thm lazy,
blanchet@53288
   246
  map_comp: thm lazy,
blanchet@51762
   247
  map_cong: thm lazy,
desharna@57981
   248
  map_cong_simp: thm lazy,
blanchet@53285
   249
  map_id: thm lazy,
blanchet@57399
   250
  map_ident0: thm lazy,
desharna@56903
   251
  map_ident: thm lazy,
traytel@52719
   252
  map_transfer: thm lazy,
blanchet@49591
   253
  rel_eq: thm lazy,
blanchet@49537
   254
  rel_flip: thm lazy,
blanchet@53290
   255
  set_map: thm lazy list,
traytel@61242
   256
  rel_cong0: thm lazy,
traytel@51893
   257
  rel_cong: thm lazy,
traytel@61242
   258
  rel_cong_simp: thm lazy,
desharna@57932
   259
  rel_map: thm list lazy,
traytel@51893
   260
  rel_mono: thm lazy,
desharna@57967
   261
  rel_mono_strong0: thm lazy,
desharna@57968
   262
  rel_mono_strong: thm lazy,
desharna@58106
   263
  set_transfer: thm list lazy,
traytel@51893
   264
  rel_Grp: thm lazy,
traytel@51893
   265
  rel_conversep: thm lazy,
desharna@58106
   266
  rel_OO: thm lazy,
traytel@59726
   267
  rel_refl: thm lazy,
traytel@61240
   268
  rel_refl_strong: thm lazy,
traytel@61240
   269
  rel_reflp: thm lazy,
traytel@61240
   270
  rel_symp: thm lazy,
traytel@61240
   271
  rel_transp: thm lazy,
desharna@58106
   272
  rel_transfer: thm lazy
blanchet@48975
   273
};
blanchet@48975
   274
traytel@52635
   275
fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
traytel@61240
   276
    inj_map inj_map_strong map_comp map_cong map_cong_simp map_id map_ident0 map_ident map_transfer
traytel@61242
   277
    rel_eq rel_flip set_map rel_cong0 rel_cong rel_cong_simp rel_map rel_mono rel_mono_strong0
traytel@61242
   278
    rel_mono_strong set_transfer rel_Grp rel_conversep rel_OO rel_refl rel_refl_strong rel_reflp
traytel@61242
   279
    rel_symp rel_transp rel_transfer = {
blanchet@48975
   280
  bd_Card_order = bd_Card_order,
blanchet@48975
   281
  bd_Cinfinite = bd_Cinfinite,
blanchet@48975
   282
  bd_Cnotzero = bd_Cnotzero,
blanchet@51766
   283
  collect_set_map = collect_set_map,
traytel@52635
   284
  in_bd = in_bd,
blanchet@48975
   285
  in_cong = in_cong,
blanchet@48975
   286
  in_mono = in_mono,
traytel@51893
   287
  in_rel = in_rel,
blanchet@56635
   288
  inj_map = inj_map,
desharna@57970
   289
  inj_map_strong = inj_map_strong,
blanchet@53288
   290
  map_comp = map_comp,
blanchet@51762
   291
  map_cong = map_cong,
desharna@57981
   292
  map_cong_simp = map_cong_simp,
blanchet@53285
   293
  map_id = map_id,
blanchet@57399
   294
  map_ident0 = map_ident0,
desharna@56903
   295
  map_ident = map_ident,
traytel@52719
   296
  map_transfer = map_transfer,
blanchet@49591
   297
  rel_eq = rel_eq,
blanchet@49537
   298
  rel_flip = rel_flip,
blanchet@53290
   299
  set_map = set_map,
traytel@61242
   300
  rel_cong0 = rel_cong0,
traytel@51893
   301
  rel_cong = rel_cong,
traytel@61242
   302
  rel_cong_simp = rel_cong_simp,
desharna@57932
   303
  rel_map = rel_map,
traytel@51893
   304
  rel_mono = rel_mono,
desharna@57967
   305
  rel_mono_strong0 = rel_mono_strong0,
desharna@57968
   306
  rel_mono_strong = rel_mono_strong,
desharna@58104
   307
  rel_transfer = rel_transfer,
traytel@51893
   308
  rel_Grp = rel_Grp,
traytel@51893
   309
  rel_conversep = rel_conversep,
desharna@58106
   310
  rel_OO = rel_OO,
traytel@59726
   311
  rel_refl = rel_refl,
traytel@61240
   312
  rel_refl_strong = rel_refl_strong,
traytel@61240
   313
  rel_reflp = rel_reflp,
traytel@61240
   314
  rel_symp = rel_symp,
traytel@61240
   315
  rel_transp = rel_transp,
desharna@58106
   316
  set_transfer = set_transfer};
blanchet@48975
   317
blanchet@48975
   318
fun map_facts f {
blanchet@48975
   319
  bd_Card_order,
blanchet@48975
   320
  bd_Cinfinite,
blanchet@48975
   321
  bd_Cnotzero,
blanchet@51766
   322
  collect_set_map,
traytel@52635
   323
  in_bd,
blanchet@48975
   324
  in_cong,
blanchet@48975
   325
  in_mono,
traytel@51893
   326
  in_rel,
blanchet@56635
   327
  inj_map,
desharna@57970
   328
  inj_map_strong,
blanchet@53288
   329
  map_comp,
blanchet@51762
   330
  map_cong,
desharna@57981
   331
  map_cong_simp,
blanchet@53285
   332
  map_id,
blanchet@57399
   333
  map_ident0,
desharna@56903
   334
  map_ident,
traytel@52719
   335
  map_transfer,
blanchet@49591
   336
  rel_eq,
blanchet@49537
   337
  rel_flip,
blanchet@53290
   338
  set_map,
traytel@61242
   339
  rel_cong0,
traytel@51893
   340
  rel_cong,
traytel@61242
   341
  rel_cong_simp,
desharna@57932
   342
  rel_map,
traytel@51893
   343
  rel_mono,
desharna@57967
   344
  rel_mono_strong0,
desharna@57968
   345
  rel_mono_strong,
desharna@58104
   346
  rel_transfer,
traytel@51893
   347
  rel_Grp,
traytel@51893
   348
  rel_conversep,
desharna@58106
   349
  rel_OO,
traytel@59726
   350
  rel_refl,
traytel@61240
   351
  rel_refl_strong,
traytel@61240
   352
  rel_reflp,
traytel@61240
   353
  rel_symp,
traytel@61240
   354
  rel_transp,
desharna@58106
   355
  set_transfer} =
blanchet@48975
   356
  {bd_Card_order = f bd_Card_order,
blanchet@48975
   357
    bd_Cinfinite = f bd_Cinfinite,
blanchet@48975
   358
    bd_Cnotzero = f bd_Cnotzero,
blanchet@51766
   359
    collect_set_map = Lazy.map f collect_set_map,
traytel@52635
   360
    in_bd = Lazy.map f in_bd,
blanchet@48975
   361
    in_cong = Lazy.map f in_cong,
blanchet@48975
   362
    in_mono = Lazy.map f in_mono,
traytel@51893
   363
    in_rel = Lazy.map f in_rel,
blanchet@56635
   364
    inj_map = Lazy.map f inj_map,
desharna@57970
   365
    inj_map_strong = Lazy.map f inj_map_strong,
blanchet@53288
   366
    map_comp = Lazy.map f map_comp,
blanchet@51762
   367
    map_cong = Lazy.map f map_cong,
desharna@57981
   368
    map_cong_simp = Lazy.map f map_cong_simp,
blanchet@53285
   369
    map_id = Lazy.map f map_id,
blanchet@57399
   370
    map_ident0 = Lazy.map f map_ident0,
desharna@56903
   371
    map_ident = Lazy.map f map_ident,
traytel@52719
   372
    map_transfer = Lazy.map f map_transfer,
blanchet@49591
   373
    rel_eq = Lazy.map f rel_eq,
blanchet@49537
   374
    rel_flip = Lazy.map f rel_flip,
blanchet@53290
   375
    set_map = map (Lazy.map f) set_map,
traytel@61242
   376
    rel_cong0 = Lazy.map f rel_cong0,
traytel@51893
   377
    rel_cong = Lazy.map f rel_cong,
traytel@61242
   378
    rel_cong_simp = Lazy.map f rel_cong_simp,
desharna@57932
   379
    rel_map = Lazy.map (map f) rel_map,
traytel@51893
   380
    rel_mono = Lazy.map f rel_mono,
desharna@57967
   381
    rel_mono_strong0 = Lazy.map f rel_mono_strong0,
desharna@57968
   382
    rel_mono_strong = Lazy.map f rel_mono_strong,
desharna@58104
   383
    rel_transfer = Lazy.map f rel_transfer,
traytel@51893
   384
    rel_Grp = Lazy.map f rel_Grp,
traytel@51893
   385
    rel_conversep = Lazy.map f rel_conversep,
desharna@58106
   386
    rel_OO = Lazy.map f rel_OO,
traytel@59726
   387
    rel_refl = Lazy.map f rel_refl,
traytel@61240
   388
    rel_refl_strong = Lazy.map f rel_refl_strong,
traytel@61240
   389
    rel_reflp = Lazy.map f rel_reflp,
traytel@61240
   390
    rel_symp = Lazy.map f rel_symp,
traytel@61240
   391
    rel_transp = Lazy.map f rel_transp,
desharna@58106
   392
    set_transfer = Lazy.map (map f) set_transfer};
blanchet@48975
   393
blanchet@48975
   394
val morph_facts = map_facts o Morphism.thm;
blanchet@48975
   395
blanchet@48975
   396
type nonemptiness_witness = {
blanchet@48975
   397
  I: int list,
blanchet@48975
   398
  wit: term,
blanchet@48975
   399
  prop: thm list
blanchet@48975
   400
};
blanchet@48975
   401
blanchet@48975
   402
fun mk_witness (I, wit) prop = {I = I, wit = wit, prop = prop};
blanchet@48975
   403
fun map_witness f g {I, wit, prop} = {I = I, wit = f wit, prop = map g prop};
blanchet@48975
   404
fun morph_witness phi = map_witness (Morphism.term phi) (Morphism.thm phi);
blanchet@48975
   405
blanchet@51837
   406
datatype bnf = BNF of {
blanchet@48975
   407
  name: binding,
blanchet@48975
   408
  T: typ,
blanchet@48975
   409
  live: int,
panny@53261
   410
  lives: typ list, (*source type variables of map*)
panny@53261
   411
  lives': typ list, (*target type variables of map*)
blanchet@48975
   412
  dead: int,
panny@53261
   413
  deads: typ list,
blanchet@48975
   414
  map: term,
blanchet@48975
   415
  sets: term list,
blanchet@48975
   416
  bd: term,
blanchet@48975
   417
  axioms: axioms,
blanchet@48975
   418
  defs: defs,
blanchet@48975
   419
  facts: facts,
blanchet@48975
   420
  nwits: int,
blanchet@48975
   421
  wits: nonemptiness_witness list,
traytel@51893
   422
  rel: term
blanchet@48975
   423
};
blanchet@48975
   424
blanchet@48975
   425
(* getters *)
blanchet@48975
   426
blanchet@48975
   427
fun rep_bnf (BNF bnf) = bnf;
blanchet@48975
   428
val name_of_bnf = #name o rep_bnf;
blanchet@48975
   429
val T_of_bnf = #T o rep_bnf;
blanchet@48975
   430
fun mk_T_of_bnf Ds Ts bnf =
blanchet@48975
   431
  let val bnf_rep = rep_bnf bnf
blanchet@48975
   432
  in Term.typ_subst_atomic ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts)) (#T bnf_rep) end;
blanchet@48975
   433
val live_of_bnf = #live o rep_bnf;
blanchet@48975
   434
val lives_of_bnf = #lives o rep_bnf;
blanchet@48975
   435
val dead_of_bnf = #dead o rep_bnf;
blanchet@48975
   436
val deads_of_bnf = #deads o rep_bnf;
blanchet@48975
   437
val axioms_of_bnf = #axioms o rep_bnf;
blanchet@48975
   438
val facts_of_bnf = #facts o rep_bnf;
blanchet@48975
   439
val nwits_of_bnf = #nwits o rep_bnf;
blanchet@48975
   440
val wits_of_bnf = #wits o rep_bnf;
blanchet@48975
   441
blanchet@53031
   442
fun flatten_type_args_of_bnf bnf dead_x xs =
blanchet@53031
   443
  let
blanchet@53031
   444
    val Type (_, Ts) = T_of_bnf bnf;
blanchet@53031
   445
    val lives = lives_of_bnf bnf;
blanchet@53031
   446
    val deads = deads_of_bnf bnf;
blanchet@53031
   447
  in
blanchet@55480
   448
    permute_like_unique (op =) (deads @ lives) Ts (replicate (length deads) dead_x @ xs)
blanchet@53031
   449
  end;
blanchet@53031
   450
blanchet@48975
   451
(*terms*)
blanchet@48975
   452
val map_of_bnf = #map o rep_bnf;
blanchet@48975
   453
val sets_of_bnf = #sets o rep_bnf;
blanchet@48975
   454
fun mk_map_of_bnf Ds Ts Us bnf =
blanchet@48975
   455
  let val bnf_rep = rep_bnf bnf;
blanchet@48975
   456
  in
blanchet@48975
   457
    Term.subst_atomic_types
blanchet@48975
   458
      ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts) @ (#lives' bnf_rep ~~ Us)) (#map bnf_rep)
blanchet@48975
   459
  end;
blanchet@48975
   460
fun mk_sets_of_bnf Dss Tss bnf =
blanchet@48975
   461
  let val bnf_rep = rep_bnf bnf;
blanchet@48975
   462
  in
blanchet@48975
   463
    map2 (fn (Ds, Ts) => Term.subst_atomic_types
blanchet@48975
   464
      ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts))) (Dss ~~ Tss) (#sets bnf_rep)
blanchet@48975
   465
  end;
blanchet@48975
   466
val bd_of_bnf = #bd o rep_bnf;
blanchet@48975
   467
fun mk_bd_of_bnf Ds Ts bnf =
blanchet@48975
   468
  let val bnf_rep = rep_bnf bnf;
blanchet@48975
   469
  in Term.subst_atomic_types ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts)) (#bd bnf_rep) end;
blanchet@48975
   470
fun mk_wits_of_bnf Dss Tss bnf =
blanchet@48975
   471
  let
blanchet@48975
   472
    val bnf_rep = rep_bnf bnf;
blanchet@48975
   473
    val wits = map (fn x => (#I x, #wit x)) (#wits bnf_rep);
blanchet@48975
   474
  in
blanchet@48975
   475
    map2 (fn (Ds, Ts) => apsnd (Term.subst_atomic_types
blanchet@48975
   476
      ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts)))) (Dss ~~ Tss) wits
blanchet@48975
   477
  end;
blanchet@49507
   478
val rel_of_bnf = #rel o rep_bnf;
blanchet@49507
   479
fun mk_rel_of_bnf Ds Ts Us bnf =
blanchet@49462
   480
  let val bnf_rep = rep_bnf bnf;
blanchet@49462
   481
  in
blanchet@49462
   482
    Term.subst_atomic_types
blanchet@49507
   483
      ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts) @ (#lives' bnf_rep ~~ Us)) (#rel bnf_rep)
blanchet@49462
   484
  end;
blanchet@48975
   485
blanchet@48975
   486
(*thms*)
blanchet@48975
   487
val bd_card_order_of_bnf = #bd_card_order o #axioms o rep_bnf;
blanchet@48975
   488
val bd_cinfinite_of_bnf = #bd_cinfinite o #axioms o rep_bnf;
blanchet@48975
   489
val bd_Card_order_of_bnf = #bd_Card_order o #facts o rep_bnf;
blanchet@48975
   490
val bd_Cinfinite_of_bnf = #bd_Cinfinite o #facts o rep_bnf;
blanchet@48975
   491
val bd_Cnotzero_of_bnf = #bd_Cnotzero o #facts o rep_bnf;
blanchet@51766
   492
val collect_set_map_of_bnf = Lazy.force o #collect_set_map o #facts o rep_bnf;
traytel@52635
   493
val in_bd_of_bnf = Lazy.force o #in_bd o #facts o rep_bnf;
blanchet@48975
   494
val in_cong_of_bnf = Lazy.force o #in_cong o #facts o rep_bnf;
blanchet@48975
   495
val in_mono_of_bnf = Lazy.force o #in_mono o #facts o rep_bnf;
traytel@51893
   496
val in_rel_of_bnf = Lazy.force o #in_rel o #facts o rep_bnf;
blanchet@56635
   497
val inj_map_of_bnf = Lazy.force o #inj_map o #facts o rep_bnf;
desharna@57970
   498
val inj_map_strong_of_bnf = Lazy.force o #inj_map_strong o #facts o rep_bnf;
blanchet@48975
   499
val map_def_of_bnf = #map_def o #defs o rep_bnf;
blanchet@53270
   500
val map_id0_of_bnf = #map_id0 o #axioms o rep_bnf;
blanchet@53285
   501
val map_id_of_bnf = Lazy.force o #map_id o #facts o rep_bnf;
blanchet@57399
   502
val map_ident0_of_bnf = Lazy.force o #map_ident0 o #facts o rep_bnf;
desharna@56903
   503
val map_ident_of_bnf = Lazy.force o #map_ident o #facts o rep_bnf;
blanchet@53287
   504
val map_comp0_of_bnf = #map_comp0 o #axioms o rep_bnf;
blanchet@53288
   505
val map_comp_of_bnf = Lazy.force o #map_comp o #facts o rep_bnf;
blanchet@51761
   506
val map_cong0_of_bnf = #map_cong0 o #axioms o rep_bnf;
blanchet@51762
   507
val map_cong_of_bnf = Lazy.force o #map_cong o #facts o rep_bnf;
desharna@57981
   508
val map_cong_simp_of_bnf = Lazy.force o #map_cong_simp o #facts o rep_bnf;
traytel@52731
   509
val map_transfer_of_bnf = Lazy.force o #map_transfer o #facts o rep_bnf;
traytel@54841
   510
val le_rel_OO_of_bnf = #le_rel_OO o #axioms o rep_bnf;
blanchet@49507
   511
val rel_def_of_bnf = #rel_def o #defs o rep_bnf;
blanchet@49591
   512
val rel_eq_of_bnf = Lazy.force o #rel_eq o #facts o rep_bnf;
blanchet@49537
   513
val rel_flip_of_bnf = Lazy.force o #rel_flip o #facts o rep_bnf;
blanchet@48975
   514
val set_bd_of_bnf = #set_bd o #axioms o rep_bnf;
blanchet@48975
   515
val set_defs_of_bnf = #set_defs o #defs o rep_bnf;
blanchet@53289
   516
val set_map0_of_bnf = #set_map0 o #axioms o rep_bnf;
blanchet@53290
   517
val set_map_of_bnf = map Lazy.force o #set_map o #facts o rep_bnf;
desharna@58106
   518
val set_transfer_of_bnf = Lazy.force o #set_transfer o #facts o rep_bnf;
traytel@61242
   519
val rel_cong0_of_bnf = Lazy.force o #rel_cong0 o #facts o rep_bnf;
traytel@51893
   520
val rel_cong_of_bnf = Lazy.force o #rel_cong o #facts o rep_bnf;
traytel@61242
   521
val rel_cong_simp_of_bnf = Lazy.force o #rel_cong_simp o #facts o rep_bnf;
traytel@51893
   522
val rel_mono_of_bnf = Lazy.force o #rel_mono o #facts o rep_bnf;
desharna@57967
   523
val rel_mono_strong0_of_bnf = Lazy.force o #rel_mono_strong0 o #facts o rep_bnf;
desharna@57968
   524
val rel_mono_strong_of_bnf = Lazy.force o #rel_mono_strong o #facts o rep_bnf;
traytel@59726
   525
val rel_refl_of_bnf = Lazy.force o #rel_refl o #facts o rep_bnf;
traytel@61240
   526
val rel_refl_strong_of_bnf = Lazy.force o #rel_refl_strong o #facts o rep_bnf;
traytel@61240
   527
val rel_reflp_of_bnf = Lazy.force o #rel_reflp o #facts o rep_bnf;
traytel@61240
   528
val rel_symp_of_bnf = Lazy.force o #rel_symp o #facts o rep_bnf;
traytel@61240
   529
val rel_transp_of_bnf = Lazy.force o #rel_transp o #facts o rep_bnf;
traytel@60742
   530
val rel_map_of_bnf = Lazy.force o #rel_map o #facts o rep_bnf;
desharna@58104
   531
val rel_transfer_of_bnf = Lazy.force o #rel_transfer o #facts o rep_bnf;
traytel@51893
   532
val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf;
traytel@51893
   533
val rel_conversep_of_bnf = Lazy.force o #rel_conversep o #facts o rep_bnf;
traytel@51893
   534
val rel_OO_of_bnf = Lazy.force o #rel_OO o #facts o rep_bnf;
traytel@51893
   535
val rel_OO_Grp_of_bnf = #rel_OO_Grp o #axioms o rep_bnf;
blanchet@48975
   536
val wit_thms_of_bnf = maps #prop o wits_of_bnf;
blanchet@48975
   537
val wit_thmss_of_bnf = map #prop o wits_of_bnf;
blanchet@48975
   538
traytel@51893
   539
fun mk_bnf name T live lives lives' dead deads map sets bd axioms defs facts wits rel =
blanchet@48975
   540
  BNF {name = name, T = T,
blanchet@48975
   541
       live = live, lives = lives, lives' = lives', dead = dead, deads = deads,
blanchet@48975
   542
       map = map, sets = sets, bd = bd,
blanchet@48975
   543
       axioms = axioms, defs = defs, facts = facts,
traytel@51893
   544
       nwits = length wits, wits = wits, rel = rel};
blanchet@48975
   545
traytel@56016
   546
fun map_bnf f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16
traytel@56016
   547
  (BNF {name = name, T = T, live = live, lives = lives, lives' = lives',
blanchet@48975
   548
  dead = dead, deads = deads, map = map, sets = sets, bd = bd,
blanchet@48975
   549
  axioms = axioms, defs = defs, facts = facts,
traytel@51893
   550
  nwits = nwits, wits = wits, rel = rel}) =
traytel@56016
   551
  BNF {name = f1 name, T = f2 T,
traytel@56016
   552
       live = f3 live, lives = f4 lives, lives' = f5 lives', dead = f6 dead, deads = f7 deads,
traytel@56016
   553
       map = f8 map, sets = f9 sets, bd = f10 bd,
traytel@56016
   554
       axioms = f11 axioms, defs = f12 defs, facts = f13 facts,
traytel@56016
   555
       nwits = f14 nwits, wits = f15 wits, rel = f16 rel};
traytel@56016
   556
traytel@56016
   557
fun morph_bnf phi =
traytel@56016
   558
  let
traytel@56016
   559
    val Tphi = Morphism.typ phi;
traytel@56016
   560
    val tphi = Morphism.term phi;
traytel@56016
   561
  in
traytel@56016
   562
    map_bnf (Morphism.binding phi) Tphi I (map Tphi) (map Tphi) I (map Tphi) tphi (map tphi) tphi
traytel@56016
   563
      (morph_axioms phi) (morph_defs phi) (morph_facts phi) I (map (morph_witness phi)) tphi
traytel@56016
   564
  end;
traytel@56016
   565
traytel@56016
   566
fun morph_bnf_defs phi = map_bnf I I I I I I I I I I I (morph_defs phi) I I I I;
blanchet@48975
   567
blanchet@58175
   568
val transfer_bnf = morph_bnf o Morphism.transfer_morphism;
blanchet@58175
   569
blanchet@48975
   570
structure Data = Generic_Data
blanchet@48975
   571
(
blanchet@51837
   572
  type T = bnf Symtab.table;
blanchet@48975
   573
  val empty = Symtab.empty;
blanchet@48975
   574
  val extend = I;
blanchet@55394
   575
  fun merge data : T = Symtab.merge (K true) data;
blanchet@48975
   576
);
blanchet@48975
   577
blanchet@58116
   578
fun bnf_of_generic context =
blanchet@58175
   579
  Option.map (transfer_bnf (Context.theory_of context)) o Symtab.lookup (Data.get context);
blanchet@58116
   580
blanchet@58116
   581
val bnf_of = bnf_of_generic o Context.Proof;
blanchet@58116
   582
val bnf_of_global = bnf_of_generic o Context.Theory;
blanchet@48975
   583
blanchet@48975
   584
blanchet@48975
   585
(* Utilities *)
blanchet@48975
   586
blanchet@48975
   587
fun normalize_set insts instA set =
blanchet@48975
   588
  let
blanchet@48975
   589
    val (T, T') = dest_funT (fastype_of set);
blanchet@48975
   590
    val A = fst (Term.dest_TVar (HOLogic.dest_setT T'));
blanchet@48975
   591
    val params = Term.add_tvar_namesT T [];
blanchet@48975
   592
  in Term.subst_TVars ((A :: params) ~~ (instA :: insts)) set end;
blanchet@48975
   593
blanchet@49507
   594
fun normalize_rel ctxt instTs instA instB rel =
blanchet@49462
   595
  let
blanchet@49462
   596
    val thy = Proof_Context.theory_of ctxt;
blanchet@49462
   597
    val tyenv =
blanchet@49507
   598
      Sign.typ_match thy (fastype_of rel, Library.foldr (op -->) (instTs, mk_pred2T instA instB))
blanchet@49463
   599
        Vartab.empty;
blanchet@49507
   600
  in Envir.subst_term (tyenv, Vartab.empty) rel end
blanchet@49453
   601
  handle Type.TYPE_MATCH => error "Bad relator";
blanchet@48975
   602
blanchet@48975
   603
fun normalize_wit insts CA As wit =
blanchet@48975
   604
  let
blanchet@48975
   605
    fun strip_param (Ts, T as Type (@{type_name fun}, [T1, T2])) =
blanchet@48975
   606
        if Type.raw_instance (CA, T) then (Ts, T) else strip_param (T1 :: Ts, T2)
blanchet@48975
   607
      | strip_param x = x;
blanchet@48975
   608
    val (Ts, T) = strip_param ([], fastype_of wit);
blanchet@48975
   609
    val subst = Term.add_tvar_namesT T [] ~~ insts;
blanchet@48975
   610
    fun find y = find_index (fn x => x = y) As;
blanchet@48975
   611
  in
blanchet@48975
   612
    (map (find o Term.typ_subst_TVars subst) (rev Ts), Term.subst_TVars subst wit)
blanchet@48975
   613
  end;
blanchet@48975
   614
blanchet@48975
   615
fun minimize_wits wits =
blanchet@48975
   616
 let
blanchet@48975
   617
   fun minimize done [] = done
traytel@49103
   618
     | minimize done ((I, wit) :: todo) =
blanchet@48975
   619
       if exists (fn (J, _) => subset (op =) (J, I)) (done @ todo)
blanchet@48975
   620
       then minimize done todo
blanchet@48975
   621
       else minimize ((I, wit) :: done) todo;
blanchet@48975
   622
 in minimize [] wits end;
blanchet@48975
   623
blanchet@54236
   624
fun mk_map live Ts Us t =
blanchet@54236
   625
  let val (Type (_, Ts0), Type (_, Us0)) = strip_typeN (live + 1) (fastype_of t) |>> List.last in
blanchet@54236
   626
    Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
blanchet@54236
   627
  end;
blanchet@54236
   628
blanchet@54236
   629
fun mk_rel live Ts Us t =
blanchet@54236
   630
  let val [Type (_, Ts0), Type (_, Us0)] = binder_types (snd (strip_typeN live (fastype_of t))) in
blanchet@54236
   631
    Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
blanchet@54236
   632
  end;
blanchet@54236
   633
blanchet@58352
   634
fun build_map_or_rel mk const of_bnf dest pre_cst_table ctxt simple_Ts build_simple =
blanchet@54236
   635
  let
blanchet@54236
   636
    fun build (TU as (T, U)) =
blanchet@58352
   637
      if exists (curry (op =) T) simple_Ts then
desharna@57301
   638
        build_simple TU
blanchet@58352
   639
      else if T = U andalso not (exists_subtype_in simple_Ts T) then
blanchet@54236
   640
        const T
blanchet@54236
   641
      else
blanchet@54236
   642
        (case TU of
blanchet@54236
   643
          (Type (s, Ts), Type (s', Us)) =>
blanchet@54236
   644
          if s = s' then
blanchet@54236
   645
            let
desharna@58093
   646
              val (live, cst0) =
desharna@58104
   647
                (case AList.lookup (op =) pre_cst_table s of
desharna@58104
   648
                  NONE => let val bnf = the (bnf_of ctxt s) in (live_of_bnf bnf, of_bnf bnf) end
desharna@58104
   649
                | SOME p => p);
desharna@58093
   650
              val cst = mk live Ts Us cst0;
desharna@58093
   651
              val TUs' = map dest (fst (strip_typeN live (fastype_of cst)));
desharna@58093
   652
            in Term.list_comb (cst, map build TUs') end
blanchet@58352
   653
          else
blanchet@58352
   654
            build_simple TU
blanchet@54236
   655
        | _ => build_simple TU);
blanchet@54236
   656
  in build end;
blanchet@54236
   657
desharna@58104
   658
val build_map = build_map_or_rel mk_map HOLogic.id_const map_of_bnf dest_funT [];
desharna@58104
   659
val build_rel = build_map_or_rel mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T o append
desharna@58104
   660
  [(@{type_name set}, (1, @{term rel_set})), (@{type_name fun}, (2, @{term rel_fun}))];
blanchet@48975
   661
blanchet@54246
   662
fun map_flattened_map_args ctxt s map_args fs =
blanchet@54246
   663
  let
blanchet@54246
   664
    val flat_fs = flatten_type_args_of_bnf (the (bnf_of ctxt s)) Term.dummy fs;
blanchet@54246
   665
    val flat_fs' = map_args flat_fs;
blanchet@54246
   666
  in
blanchet@55480
   667
    permute_like_unique (op aconv) flat_fs fs flat_fs'
blanchet@54246
   668
  end;
blanchet@54246
   669
blanchet@48975
   670
blanchet@48975
   671
(* Names *)
blanchet@48975
   672
blanchet@48975
   673
val mapN = "map";
blanchet@48975
   674
val setN = "set";
blanchet@48975
   675
fun mk_setN i = setN ^ nonzero_string_of_int i;
blanchet@48975
   676
val bdN = "bd";
blanchet@48975
   677
val witN = "wit";
blanchet@48975
   678
fun mk_witN i = witN ^ nonzero_string_of_int i;
blanchet@49507
   679
val relN = "rel";
blanchet@48975
   680
blanchet@48975
   681
val bd_card_orderN = "bd_card_order";
blanchet@48975
   682
val bd_cinfiniteN = "bd_cinfinite";
blanchet@48975
   683
val bd_Card_orderN = "bd_Card_order";
blanchet@48975
   684
val bd_CinfiniteN = "bd_Cinfinite";
blanchet@48975
   685
val bd_CnotzeroN = "bd_Cnotzero";
blanchet@51766
   686
val collect_set_mapN = "collect_set_map";
blanchet@48975
   687
val in_bdN = "in_bd";
blanchet@48975
   688
val in_monoN = "in_mono";
traytel@51893
   689
val in_relN = "in_rel";
blanchet@56635
   690
val inj_mapN = "inj_map";
desharna@57970
   691
val inj_map_strongN = "inj_map_strong";
blanchet@53270
   692
val map_id0N = "map_id0";
blanchet@53285
   693
val map_idN = "map_id";
desharna@56903
   694
val map_identN = "map_ident";
blanchet@53287
   695
val map_comp0N = "map_comp0";
blanchet@53288
   696
val map_compN = "map_comp";
blanchet@51761
   697
val map_cong0N = "map_cong0";
blanchet@51762
   698
val map_congN = "map_cong";
desharna@57981
   699
val map_cong_simpN = "map_cong_simp";
traytel@52719
   700
val map_transferN = "map_transfer";
blanchet@49591
   701
val rel_eqN = "rel_eq";
blanchet@49537
   702
val rel_flipN = "rel_flip";
blanchet@53289
   703
val set_map0N = "set_map0";
blanchet@53290
   704
val set_mapN = "set_map";
blanchet@49537
   705
val set_bdN = "set_bd";
traytel@59726
   706
val set_transferN = "set_transfer";
traytel@51893
   707
val rel_GrpN = "rel_Grp";
traytel@51893
   708
val rel_conversepN = "rel_conversep";
traytel@59726
   709
val rel_mapN = "rel_map";
traytel@59726
   710
val rel_monoN = "rel_mono";
traytel@59726
   711
val rel_mono_strong0N = "rel_mono_strong0";
traytel@59726
   712
val rel_mono_strongN = "rel_mono_strong";
traytel@61242
   713
val rel_congN = "rel_cong";
traytel@61242
   714
val rel_cong_simpN = "rel_cong_simp";
traytel@59726
   715
val rel_reflN = "rel_refl";
traytel@61240
   716
val rel_refl_strongN = "rel_refl_strong";
traytel@61240
   717
val rel_reflpN = "rel_reflp";
traytel@61240
   718
val rel_sympN = "rel_symp";
traytel@61240
   719
val rel_transpN = "rel_transp";
traytel@59726
   720
val rel_transferN = "rel_transfer";
blanchet@54620
   721
val rel_comppN = "rel_compp";
blanchet@54620
   722
val rel_compp_GrpN = "rel_compp_Grp";
blanchet@48975
   723
blanchet@55854
   724
datatype inline_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline;
blanchet@48975
   725
blanchet@49538
   726
datatype fact_policy = Dont_Note | Note_Some | Note_All;
blanchet@48975
   727
blanchet@48975
   728
val bnf_note_all = Attrib.setup_config_bool @{binding bnf_note_all} (K false);
traytel@53143
   729
val bnf_timing = Attrib.setup_config_bool @{binding bnf_timing} (K false);
blanchet@48975
   730
blanchet@49538
   731
fun user_policy policy ctxt = if Config.get ctxt bnf_note_all then Note_All else policy;
blanchet@48975
   732
blanchet@55854
   733
val smart_max_inline_term_size = 25; (*FUDGE*)
blanchet@48975
   734
blanchet@57631
   735
fun note_bnf_thms fact_policy qualify0 bnf_b bnf lthy =
traytel@52720
   736
  let
traytel@52720
   737
    val axioms = axioms_of_bnf bnf;
traytel@52720
   738
    val facts = facts_of_bnf bnf;
traytel@52720
   739
    val wits = wits_of_bnf bnf;
traytel@54045
   740
    val qualify =
wenzelm@59858
   741
      let val qs = Binding.path_of bnf_b;
blanchet@56766
   742
      in fold_rev (fn (s, mand) => Binding.qualify mand s) qs #> qualify0 end;
blanchet@57631
   743
blanchet@57631
   744
    fun note_if_note_all (noted0, lthy0) =
traytel@52720
   745
      let
traytel@52720
   746
        val witNs = if length wits = 1 then [witN] else map mk_witN (1 upto length wits);
traytel@52720
   747
        val notes =
traytel@52720
   748
          [(bd_card_orderN, [#bd_card_order axioms]),
blanchet@57631
   749
           (bd_cinfiniteN, [#bd_cinfinite axioms]),
blanchet@57631
   750
           (bd_Card_orderN, [#bd_Card_order facts]),
blanchet@57631
   751
           (bd_CinfiniteN, [#bd_Cinfinite facts]),
blanchet@57631
   752
           (bd_CnotzeroN, [#bd_Cnotzero facts]),
blanchet@57631
   753
           (collect_set_mapN, [Lazy.force (#collect_set_map facts)]),
blanchet@57631
   754
           (in_bdN, [Lazy.force (#in_bd facts)]),
blanchet@57631
   755
           (in_monoN, [Lazy.force (#in_mono facts)]),
blanchet@57631
   756
           (map_comp0N, [#map_comp0 axioms]),
desharna@57967
   757
           (rel_mono_strong0N, [Lazy.force (#rel_mono_strong0 facts)]),
blanchet@57631
   758
           (set_map0N, #set_map0 axioms),
blanchet@57631
   759
           (set_bdN, #set_bd axioms)] @
blanchet@57631
   760
          (witNs ~~ wit_thmss_of_bnf bnf)
blanchet@57631
   761
          |> map (fn (thmN, thms) =>
blanchet@57631
   762
            ((qualify (Binding.qualify true (Binding.name_of bnf_b) (Binding.name thmN)), []),
blanchet@57631
   763
             [(thms, [])]));
blanchet@57631
   764
      in
blanchet@57631
   765
        Local_Theory.notes notes lthy0 |>> append noted0
desharna@58104
   766
      end;
blanchet@57631
   767
blanchet@57631
   768
    fun note_unless_dont_note (noted0, lthy0) =
blanchet@57631
   769
      let
blanchet@57631
   770
        val notes =
traytel@59133
   771
          [(in_relN, [Lazy.force (#in_rel facts)], []),
traytel@59133
   772
           (inj_mapN, [Lazy.force (#inj_map facts)], []),
desharna@57970
   773
           (inj_map_strongN, [Lazy.force (#inj_map_strong facts)], []),
desharna@57969
   774
           (map_compN, [Lazy.force (#map_comp facts)], []),
blanchet@57631
   775
           (map_cong0N, [#map_cong0 axioms], []),
blanchet@57631
   776
           (map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs),
desharna@57981
   777
           (map_cong_simpN, [Lazy.force (#map_cong_simp facts)], []),
blanchet@57631
   778
           (map_idN, [Lazy.force (#map_id facts)], []),
blanchet@57631
   779
           (map_id0N, [#map_id0 axioms], []),
desharna@58102
   780
           (map_transferN, [Lazy.force (#map_transfer facts)], []),
blanchet@57631
   781
           (map_identN, [Lazy.force (#map_ident facts)], []),
blanchet@57631
   782
           (rel_comppN, [Lazy.force (#rel_OO facts)], []),
blanchet@57631
   783
           (rel_compp_GrpN, no_refl [#rel_OO_Grp axioms], []),
blanchet@57631
   784
           (rel_conversepN, [Lazy.force (#rel_conversep facts)], []),
blanchet@57631
   785
           (rel_eqN, [Lazy.force (#rel_eq facts)], []),
blanchet@57631
   786
           (rel_flipN, [Lazy.force (#rel_flip facts)], []),
blanchet@57631
   787
           (rel_GrpN, [Lazy.force (#rel_Grp facts)], []),
desharna@57932
   788
           (rel_mapN, Lazy.force (#rel_map facts), []),
blanchet@58344
   789
           (rel_monoN, [Lazy.force (#rel_mono facts)], mono_attrs),
traytel@59133
   790
           (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)], []),
traytel@61242
   791
           (rel_congN, [Lazy.force (#rel_cong facts)], fundefcong_attrs),
traytel@61242
   792
           (rel_cong_simpN, [Lazy.force (#rel_cong_simp facts)], []),
traytel@59726
   793
           (rel_reflN, [Lazy.force (#rel_refl facts)], []),
traytel@61240
   794
           (rel_refl_strongN, [Lazy.force (#rel_refl_strong facts)], []),
traytel@61240
   795
           (rel_reflpN, [Lazy.force (#rel_reflp facts)], []),
traytel@61240
   796
           (rel_sympN, [Lazy.force (#rel_symp facts)], []),
traytel@61240
   797
           (rel_transpN, [Lazy.force (#rel_transp facts)], []),
desharna@58104
   798
           (rel_transferN, [Lazy.force (#rel_transfer facts)], []),
desharna@58106
   799
           (set_mapN, map Lazy.force (#set_map facts), []),
desharna@58106
   800
           (set_transferN, Lazy.force (#set_transfer facts), [])]
blanchet@57631
   801
          |> filter_out (null o #2)
blanchet@57631
   802
          |> map (fn (thmN, thms, attrs) =>
blanchet@57631
   803
            ((qualify (Binding.qualify true (Binding.name_of bnf_b) (Binding.name thmN)), attrs),
blanchet@57631
   804
             [(thms, [])]));
blanchet@57631
   805
      in
blanchet@57631
   806
        Local_Theory.notes notes lthy0 |>> append noted0
desharna@58104
   807
      end;
blanchet@57631
   808
  in
blanchet@57631
   809
    ([], lthy)
blanchet@57631
   810
    |> fact_policy = Note_All ? note_if_note_all
blanchet@57631
   811
    |> fact_policy <> Dont_Note ? note_unless_dont_note
blanchet@57631
   812
    |>> (fn [] => bnf | noted => morph_bnf (substitute_noted_thm noted) bnf)
traytel@52720
   813
  end;
traytel@52720
   814
traytel@60918
   815
fun mk_wit_goals zs bs sets (I, wit) =
traytel@60918
   816
  let
traytel@60918
   817
    val xs = map (nth bs) I;
traytel@60918
   818
    fun wit_goal i =
traytel@60918
   819
      let
traytel@60918
   820
        val z = nth zs i;
traytel@60918
   821
        val set_wit = nth sets i $ Term.list_comb (wit, xs);
traytel@60918
   822
        val concl = HOLogic.mk_Trueprop
traytel@60918
   823
          (if member (op =) I i then HOLogic.mk_eq (z, nth bs i) else @{term False});
traytel@60918
   824
      in
traytel@60918
   825
        fold_rev Logic.all (z :: xs) (Logic.mk_implies (mk_Trueprop_mem (z, set_wit), concl))
traytel@60918
   826
      end;
traytel@60918
   827
  in
traytel@60918
   828
    map wit_goal (0 upto length sets - 1)
traytel@60918
   829
  end;
traytel@60918
   830
blanchet@48975
   831
blanchet@48975
   832
(* Define new BNFs *)
blanchet@48975
   833
traytel@56016
   834
fun define_bnf_consts const_policy fact_policy internal Ds_opt map_b rel_b set_bs
traytel@54841
   835
  ((((((bnf_b, T_rhs), map_rhs), set_rhss), bd_rhs), wit_rhss), rel_rhs_opt) no_defs_lthy =
blanchet@48975
   836
  let
traytel@54841
   837
    val live = length set_rhss;
blanchet@53265
   838
traytel@61241
   839
    val def_qualify = Binding.qualify false (Binding.name_of bnf_b);
blanchet@53265
   840
blanchet@54490
   841
    fun mk_prefix_binding pre = Binding.prefix_name (pre ^ "_") bnf_b;
traytel@49434
   842
blanchet@49463
   843
    fun maybe_define user_specified (b, rhs) lthy =
blanchet@48975
   844
      let
blanchet@48975
   845
        val inline =
blanchet@49538
   846
          (user_specified orelse fact_policy = Dont_Note) andalso
blanchet@48975
   847
          (case const_policy of
blanchet@48975
   848
            Dont_Inline => false
blanchet@48975
   849
          | Hardly_Inline => Term.is_Free rhs orelse Term.is_Const rhs
blanchet@55854
   850
          | Smart_Inline => Term.size_of_term rhs <= smart_max_inline_term_size
blanchet@60154
   851
          | Do_Inline => true);
blanchet@48975
   852
      in
blanchet@48975
   853
        if inline then
blanchet@49460
   854
          ((rhs, Drule.reflexive_thm), lthy)
blanchet@48975
   855
        else
blanchet@48975
   856
          let val b = b () in
traytel@56016
   857
            apfst (apsnd snd)
traytel@56016
   858
              ((if internal then Local_Theory.define_internal else Local_Theory.define)
traytel@61241
   859
                ((b, NoSyn), ((Binding.concealed (Thm.def_binding b), []), rhs)) lthy)
blanchet@48975
   860
          end
blanchet@48975
   861
      end;
blanchet@49459
   862
blanchet@51758
   863
    val map_bind_def =
blanchet@54490
   864
      (fn () => def_qualify (if Binding.is_empty map_b then mk_prefix_binding mapN else map_b),
blanchet@53265
   865
         map_rhs);
blanchet@49459
   866
    val set_binds_defs =
blanchet@49459
   867
      let
blanchet@51757
   868
        fun set_name i get_b =
blanchet@51757
   869
          (case try (nth set_bs) (i - 1) of
blanchet@51757
   870
            SOME b => if Binding.is_empty b then get_b else K b
blanchet@53265
   871
          | NONE => get_b) #> def_qualify;
blanchet@54490
   872
        val bs = if live = 1 then [set_name 1 (fn () => mk_prefix_binding setN)]
blanchet@54490
   873
          else map (fn i => set_name i (fn () => mk_prefix_binding (mk_setN i))) (1 upto live);
blanchet@51757
   874
      in bs ~~ set_rhss end;
blanchet@54490
   875
    val bd_bind_def = (fn () => def_qualify (mk_prefix_binding bdN), bd_rhs);
blanchet@49459
   876
traytel@54189
   877
    val ((((bnf_map_term, raw_map_def),
blanchet@48975
   878
      (bnf_set_terms, raw_set_defs)),
traytel@54189
   879
      (bnf_bd_term, raw_bd_def)), (lthy, lthy_old)) =
blanchet@48975
   880
        no_defs_lthy
traytel@61101
   881
        |> Local_Theory.open_target |> snd
blanchet@49463
   882
        |> maybe_define true map_bind_def
blanchet@49463
   883
        ||>> apfst split_list o fold_map (maybe_define true) set_binds_defs
blanchet@49463
   884
        ||>> maybe_define true bd_bind_def
traytel@61101
   885
        ||> `Local_Theory.close_target;
blanchet@48975
   886
blanchet@49459
   887
    val phi = Proof_Context.export_morphism lthy_old lthy;
blanchet@48975
   888
blanchet@48975
   889
    val bnf_map_def = Morphism.thm phi raw_map_def;
blanchet@48975
   890
    val bnf_set_defs = map (Morphism.thm phi) raw_set_defs;
blanchet@48975
   891
    val bnf_bd_def = Morphism.thm phi raw_bd_def;
blanchet@48975
   892
blanchet@48975
   893
    val bnf_map = Morphism.term phi bnf_map_term;
blanchet@48975
   894
blanchet@48975
   895
    (*TODO: handle errors*)
blanchet@48975
   896
    (*simple shape analysis of a map function*)
traytel@54841
   897
    val ((alphas, betas), (Calpha, _)) =
traytel@49395
   898
      fastype_of bnf_map
traytel@49395
   899
      |> strip_typeN live
traytel@49395
   900
      |>> map_split dest_funT
traytel@49395
   901
      ||> dest_funT
traytel@49395
   902
      handle TYPE _ => error "Bad map function";
blanchet@48975
   903
traytel@54841
   904
    val Calpha_params = map TVar (Term.add_tvarsT Calpha []);
blanchet@48975
   905
traytel@54426
   906
    val bnf_T = Morphism.typ phi T_rhs;
traytel@54426
   907
    val bad_args = Term.add_tfreesT bnf_T [];
blanchet@59281
   908
    val _ = null bad_args orelse error ("Locally fixed type arguments " ^
traytel@54426
   909
      commas_quote (map (Syntax.string_of_typ no_defs_lthy o TFree) bad_args));
traytel@54426
   910
traytel@54841
   911
    val bnf_sets =
traytel@54841
   912
      map2 (normalize_set Calpha_params) alphas (map (Morphism.term phi) bnf_set_terms);
blanchet@48975
   913
    val bnf_bd =
traytel@54841
   914
      Term.subst_TVars (Term.add_tvar_namesT bnf_T [] ~~ Calpha_params)
traytel@54841
   915
        (Morphism.term phi bnf_bd_term);
blanchet@48975
   916
blanchet@48975
   917
    (*TODO: assert Ds = (TVars of bnf_map) \ (alphas @ betas) as sets*)
blanchet@48975
   918
    val deads = (case Ds_opt of
blanchet@48975
   919
      NONE => subtract (op =) (alphas @ betas) (map TVar (Term.add_tvars bnf_map []))
blanchet@48975
   920
    | SOME Ds => map (Morphism.typ phi) Ds);
blanchet@48975
   921
blanchet@48975
   922
    (*TODO: further checks of type of bnf_map*)
blanchet@48975
   923
    (*TODO: check types of bnf_sets*)
blanchet@48975
   924
    (*TODO: check type of bnf_bd*)
blanchet@49507
   925
    (*TODO: check type of bnf_rel*)
blanchet@48975
   926
traytel@54841
   927
    fun mk_bnf_map Ds As' Bs' =
traytel@54841
   928
      Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As') @ (betas ~~ Bs')) bnf_map;
traytel@54841
   929
    fun mk_bnf_t Ds As' = Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As'));
traytel@54841
   930
    fun mk_bnf_T Ds As' = Term.typ_subst_atomic ((deads ~~ Ds) @ (alphas ~~ As'));
traytel@54841
   931
blanchet@60154
   932
    val (((As, Bs), unsorted_Ds), names_lthy) = lthy
traytel@54841
   933
      |> mk_TFrees live
traytel@54841
   934
      ||>> mk_TFrees live
traytel@54841
   935
      ||>> mk_TFrees (length deads);
blanchet@60154
   936
blanchet@60154
   937
    val Ds = map2 (resort_tfree_or_tvar o Type.sort_of_atyp) deads unsorted_Ds;
blanchet@60154
   938
traytel@54841
   939
    val RTs = map2 (curry HOLogic.mk_prodT) As Bs;
traytel@54841
   940
    val pred2RTs = map2 mk_pred2T As Bs;
blanchet@60154
   941
    val (Rs, Rs') = names_lthy |> mk_Frees' "R" pred2RTs |> fst;
traytel@54841
   942
    val CA = mk_bnf_T Ds As Calpha;
traytel@54841
   943
    val CR = mk_bnf_T Ds RTs Calpha;
traytel@54841
   944
    val setRs =
wenzelm@58634
   945
      @{map 3} (fn R => fn T => fn U =>
haftmann@61424
   946
          HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_case_prod R) Rs As Bs;
traytel@54841
   947
traytel@54841
   948
    (*Grp (in (Collect (split R1) .. Collect (split Rn))) (map fst .. fst)^--1 OO
traytel@54841
   949
      Grp (in (Collect (split R1) .. Collect (split Rn))) (map snd .. snd)*)
traytel@54841
   950
    val OO_Grp =
traytel@54841
   951
      let
traytel@54841
   952
        val map1 = Term.list_comb (mk_bnf_map Ds RTs As, map fst_const RTs);
traytel@54841
   953
        val map2 = Term.list_comb (mk_bnf_map Ds RTs Bs, map snd_const RTs);
traytel@54841
   954
        val bnf_in = mk_in setRs (map (mk_bnf_t Ds RTs) bnf_sets) CR;
traytel@54841
   955
      in
traytel@54841
   956
        mk_rel_compp (mk_conversep (mk_Grp bnf_in map1), mk_Grp bnf_in map2)
traytel@54841
   957
        |> fold_rev Term.absfree Rs'
traytel@54841
   958
      end;
traytel@54841
   959
traytel@54841
   960
    val rel_rhs = the_default OO_Grp rel_rhs_opt;
traytel@54841
   961
traytel@54841
   962
    val rel_bind_def =
traytel@54841
   963
      (fn () => def_qualify (if Binding.is_empty rel_b then mk_prefix_binding relN else rel_b),
traytel@54841
   964
         rel_rhs);
traytel@54841
   965
traytel@54841
   966
    val wit_rhss =
traytel@54841
   967
      if null wit_rhss then
traytel@54841
   968
        [fold_rev Term.absdummy As (Term.list_comb (mk_bnf_map Ds As As,
traytel@54841
   969
          map2 (fn T => fn i => Term.absdummy T (Bound i)) As (live downto 1)) $
traytel@54841
   970
          Const (@{const_name undefined}, CA))]
traytel@54841
   971
      else wit_rhss;
traytel@54841
   972
    val nwits = length wit_rhss;
traytel@54841
   973
    val wit_binds_defs =
traytel@54841
   974
      let
traytel@54841
   975
        val bs = if nwits = 1 then [fn () => def_qualify (mk_prefix_binding witN)]
traytel@54841
   976
          else map (fn i => fn () => def_qualify (mk_prefix_binding (mk_witN i))) (1 upto nwits);
traytel@54841
   977
      in bs ~~ wit_rhss end;
traytel@54841
   978
traytel@54841
   979
    val (((bnf_rel_term, raw_rel_def), (bnf_wit_terms, raw_wit_defs)), (lthy, lthy_old)) =
traytel@54841
   980
      lthy
traytel@61101
   981
      |> Local_Theory.open_target |> snd
traytel@54841
   982
      |> maybe_define (is_some rel_rhs_opt) rel_bind_def
traytel@54841
   983
      ||>> apfst split_list o fold_map (maybe_define (not (null wit_rhss))) wit_binds_defs
traytel@61101
   984
      ||> `Local_Theory.close_target;
traytel@54841
   985
traytel@54841
   986
    val phi = Proof_Context.export_morphism lthy_old lthy;
traytel@54841
   987
    val bnf_rel_def = Morphism.thm phi raw_rel_def;
traytel@54841
   988
    val bnf_rel = Morphism.term phi bnf_rel_term;
traytel@54841
   989
    fun mk_bnf_rel Ds As' Bs' =
traytel@54841
   990
      normalize_rel lthy (map2 mk_pred2T As' Bs') (mk_bnf_T Ds As' Calpha) (mk_bnf_T Ds Bs' Calpha)
traytel@54841
   991
        bnf_rel;
traytel@54841
   992
traytel@54841
   993
    val bnf_wit_defs = map (Morphism.thm phi) raw_wit_defs;
traytel@54841
   994
    val bnf_wits =
traytel@54841
   995
      map (normalize_wit Calpha_params Calpha alphas o Morphism.term phi) bnf_wit_terms;
traytel@54841
   996
traytel@54841
   997
    fun mk_OO_Grp Ds' As' Bs' =
traytel@54841
   998
      Term.subst_atomic_types ((Ds ~~ Ds') @ (As ~~ As') @ (Bs ~~ Bs')) OO_Grp;
traytel@54841
   999
  in
traytel@54841
  1000
    (((alphas, betas, deads, Calpha),
traytel@54841
  1001
     (bnf_map, bnf_sets, bnf_bd, bnf_wits, bnf_rel),
traytel@54841
  1002
     (bnf_map_def, bnf_set_defs, bnf_bd_def, bnf_wit_defs, bnf_rel_def),
traytel@54841
  1003
     (mk_bnf_map, mk_bnf_t, mk_bnf_T, mk_bnf_rel, mk_OO_Grp)), lthy)
traytel@54841
  1004
  end;
traytel@54841
  1005
traytel@56016
  1006
fun prepare_def const_policy mk_fact_policy internal qualify prep_typ prep_term Ds_opt map_b rel_b
traytel@56016
  1007
  set_bs ((((((raw_bnf_b, raw_bnf_T), raw_map), raw_sets), raw_bd), raw_wits), raw_rel_opt)
traytel@54841
  1008
  no_defs_lthy =
traytel@54841
  1009
  let
traytel@54841
  1010
    val fact_policy = mk_fact_policy no_defs_lthy;
traytel@54841
  1011
    val bnf_b = qualify raw_bnf_b;
traytel@54841
  1012
    val live = length raw_sets;
traytel@54841
  1013
traytel@54841
  1014
    val T_rhs = prep_typ no_defs_lthy raw_bnf_T;
traytel@54841
  1015
    val map_rhs = prep_term no_defs_lthy raw_map;
traytel@54841
  1016
    val set_rhss = map (prep_term no_defs_lthy) raw_sets;
traytel@54841
  1017
    val bd_rhs = prep_term no_defs_lthy raw_bd;
traytel@54841
  1018
    val wit_rhss = map (prep_term no_defs_lthy) raw_wits;
traytel@54841
  1019
    val rel_rhs_opt = Option.map (prep_term no_defs_lthy) raw_rel_opt;
traytel@54841
  1020
traytel@54841
  1021
    fun err T =
traytel@54841
  1022
      error ("Trying to register the type " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^
traytel@54841
  1023
        " as unnamed BNF");
traytel@54841
  1024
traytel@54841
  1025
    val (bnf_b, key) =
traytel@54841
  1026
      if Binding.eq_name (bnf_b, Binding.empty) then
traytel@54841
  1027
        (case T_rhs of
traytel@54841
  1028
          Type (C, Ts) => if forall (can dest_TFree) Ts
traytel@54841
  1029
            then (Binding.qualified_name C, C) else err T_rhs
traytel@54841
  1030
        | T => err T)
traytel@54841
  1031
      else (bnf_b, Local_Theory.full_name no_defs_lthy bnf_b);
traytel@54841
  1032
traytel@54841
  1033
    val (((alphas, betas, deads, Calpha),
traytel@54841
  1034
     (bnf_map, bnf_sets, bnf_bd, bnf_wits, bnf_rel),
traytel@54841
  1035
     (bnf_map_def, bnf_set_defs, bnf_bd_def, bnf_wit_defs, bnf_rel_def),
traytel@54841
  1036
     (mk_bnf_map_Ds, mk_bnf_t_Ds, mk_bnf_T_Ds, _, mk_OO_Grp)), lthy) =
traytel@56016
  1037
       define_bnf_consts const_policy fact_policy internal Ds_opt map_b rel_b set_bs
traytel@54841
  1038
         ((((((bnf_b, T_rhs), map_rhs), set_rhss), bd_rhs), wit_rhss), rel_rhs_opt) no_defs_lthy;
traytel@54841
  1039
traytel@54841
  1040
    val dead = length deads;
traytel@54841
  1041
blanchet@60154
  1042
    val (((((((As', Bs'), Cs), unsorted_Ds), Es), B1Ts), B2Ts), (Ts, T)) = lthy
blanchet@48975
  1043
      |> mk_TFrees live
blanchet@48975
  1044
      ||>> mk_TFrees live
blanchet@48975
  1045
      ||>> mk_TFrees live
blanchet@48975
  1046
      ||>> mk_TFrees dead
blanchet@48975
  1047
      ||>> mk_TFrees live
blanchet@48975
  1048
      ||>> mk_TFrees live
desharna@58104
  1049
      ||>> mk_TFrees live
blanchet@48975
  1050
      ||> fst o mk_TFrees 1
blanchet@48975
  1051
      ||> the_single
blanchet@48975
  1052
      ||> `(replicate live);
blanchet@48975
  1053
blanchet@60154
  1054
    val Ds = map2 (resort_tfree_or_tvar o Type.sort_of_atyp) deads unsorted_Ds;
blanchet@60154
  1055
traytel@54841
  1056
    val mk_bnf_map = mk_bnf_map_Ds Ds;
traytel@54841
  1057
    val mk_bnf_t = mk_bnf_t_Ds Ds;
traytel@54841
  1058
    val mk_bnf_T = mk_bnf_T_Ds Ds;
blanchet@49453
  1059
traytel@51893
  1060
    val pred2RTs = map2 mk_pred2T As' Bs';
traytel@51893
  1061
    val pred2RTsAsCs = map2 mk_pred2T As' Cs;
traytel@51893
  1062
    val pred2RTsBsCs = map2 mk_pred2T Bs' Cs;
desharna@58104
  1063
    val pred2RTsBsEs = map2 mk_pred2T Bs' Es;
desharna@57932
  1064
    val pred2RTsCsBs = map2 mk_pred2T Cs Bs';
desharna@58104
  1065
    val pred2RTsCsEs = map2 mk_pred2T Cs Es;
traytel@51893
  1066
    val pred2RT's = map2 mk_pred2T Bs' As';
traytel@51893
  1067
    val self_pred2RTs = map2 mk_pred2T As' As';
traytel@52719
  1068
    val transfer_domRTs = map2 mk_pred2T As' B1Ts;
traytel@52719
  1069
    val transfer_ranRTs = map2 mk_pred2T Bs' B2Ts;
blanchet@48975
  1070
traytel@54841
  1071
    val CA' = mk_bnf_T As' Calpha;
traytel@54841
  1072
    val CB' = mk_bnf_T Bs' Calpha;
traytel@54841
  1073
    val CC' = mk_bnf_T Cs Calpha;
desharna@58104
  1074
    val CE' = mk_bnf_T Es Calpha;
traytel@54841
  1075
    val CB1 = mk_bnf_T B1Ts Calpha;
traytel@54841
  1076
    val CB2 = mk_bnf_T B2Ts Calpha;
blanchet@49453
  1077
blanchet@48975
  1078
    val bnf_map_AsAs = mk_bnf_map As' As';
blanchet@48975
  1079
    val bnf_map_AsBs = mk_bnf_map As' Bs';
blanchet@48975
  1080
    val bnf_map_AsCs = mk_bnf_map As' Cs;
blanchet@48975
  1081
    val bnf_map_BsCs = mk_bnf_map Bs' Cs;
blanchet@48975
  1082
    val bnf_sets_As = map (mk_bnf_t As') bnf_sets;
blanchet@48975
  1083
    val bnf_sets_Bs = map (mk_bnf_t Bs') bnf_sets;
blanchet@48975
  1084
    val bnf_bd_As = mk_bnf_t As' bnf_bd;
traytel@54841
  1085
    fun mk_bnf_rel RTs CA CB = normalize_rel lthy RTs CA CB bnf_rel;
blanchet@48975
  1086
blanchet@49595
  1087
    val pre_names_lthy = lthy;
traytel@61242
  1088
    val (((((((((((((((((((((((fs, fs'), gs), hs), is), x), x'), y), y'), zs), zs'), ys), As),
desharna@58104
  1089
      As_copy), bs), Rs), Rs_copy), Ss), S_AsCs), S_CsBs), S_BsEs),
traytel@52719
  1090
      transfer_domRs), transfer_ranRs), names_lthy) = pre_names_lthy
traytel@52923
  1091
      |> mk_Frees "f" (map2 (curry op -->) As' Bs')
desharna@57970
  1092
      ||>> mk_Frees "f" (map2 (curry op -->) As' Bs')
traytel@52923
  1093
      ||>> mk_Frees "g" (map2 (curry op -->) Bs' Cs)
traytel@52923
  1094
      ||>> mk_Frees "h" (map2 (curry op -->) As' Ts)
desharna@57932
  1095
      ||>> mk_Frees "i" (map2 (curry op -->) As' Cs)
traytel@51894
  1096
      ||>> yield_singleton (mk_Frees "x") CA'
desharna@57970
  1097
      ||>> yield_singleton (mk_Frees "x") CA'
traytel@51894
  1098
      ||>> yield_singleton (mk_Frees "y") CB'
traytel@61242
  1099
      ||>> yield_singleton (mk_Frees "y") CB'
blanchet@48975
  1100
      ||>> mk_Frees "z" As'
desharna@57970
  1101
      ||>> mk_Frees "z" As'
traytel@51916
  1102
      ||>> mk_Frees "y" Bs'
blanchet@48975
  1103
      ||>> mk_Frees "A" (map HOLogic.mk_setT As')
blanchet@48975
  1104
      ||>> mk_Frees "A" (map HOLogic.mk_setT As')
blanchet@48975
  1105
      ||>> mk_Frees "b" As'
traytel@54841
  1106
      ||>> mk_Frees "R" pred2RTs
traytel@51893
  1107
      ||>> mk_Frees "R" pred2RTs
traytel@52719
  1108
      ||>> mk_Frees "S" pred2RTsBsCs
desharna@57932
  1109
      ||>> mk_Frees "S" pred2RTsAsCs
desharna@57932
  1110
      ||>> mk_Frees "S" pred2RTsCsBs
desharna@58104
  1111
      ||>> mk_Frees "S" pred2RTsBsEs
traytel@52719
  1112
      ||>> mk_Frees "R" transfer_domRTs
traytel@52719
  1113
      ||>> mk_Frees "S" transfer_ranRTs;
blanchet@48975
  1114
blanchet@56651
  1115
    val fs_copy = map2 (retype_const_or_free o fastype_of) fs gs;
traytel@61242
  1116
    val x_copy = retype_const_or_free CA' y';
traytel@61242
  1117
    val y_copy = retype_const_or_free CB' x';
blanchet@51762
  1118
traytel@51893
  1119
    val rel = mk_bnf_rel pred2RTs CA' CB';
desharna@58104
  1120
    val relCsEs = mk_bnf_rel pred2RTsCsEs CC' CE';
traytel@52719
  1121
    val relAsAs = mk_bnf_rel self_pred2RTs CA' CA';
traytel@54189
  1122
    val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits;
traytel@54189
  1123
blanchet@53270
  1124
    val map_id0_goal =
blanchet@51762
  1125
      let val bnf_map_app_id = Term.list_comb (bnf_map_AsAs, map HOLogic.id_const As') in
blanchet@51762
  1126
        mk_Trueprop_eq (bnf_map_app_id, HOLogic.id_const CA')
blanchet@48975
  1127
      end;
blanchet@48975
  1128
blanchet@53287
  1129
    val map_comp0_goal =
blanchet@48975
  1130
      let
blanchet@49018
  1131
        val bnf_map_app_comp = Term.list_comb (bnf_map_AsCs, map2 (curry HOLogic.mk_comp) gs fs);
blanchet@48975
  1132
        val comp_bnf_map_app = HOLogic.mk_comp
blanchet@51762
  1133
          (Term.list_comb (bnf_map_BsCs, gs), Term.list_comb (bnf_map_AsBs, fs));
blanchet@48975
  1134
      in
blanchet@49123
  1135
        fold_rev Logic.all (fs @ gs) (mk_Trueprop_eq (bnf_map_app_comp, comp_bnf_map_app))
blanchet@48975
  1136
      end;
blanchet@48975
  1137
desharna@57981
  1138
    fun mk_map_cong_prem mk_implies x z set f f_copy =
blanchet@58108
  1139
      Logic.all z (mk_implies (mk_Trueprop_mem (z, set $ x), mk_Trueprop_eq (f $ z, f_copy $ z)));
blanchet@51762
  1140
blanchet@51761
  1141
    val map_cong0_goal =
blanchet@48975
  1142
      let
wenzelm@58634
  1143
        val prems = @{map 4} (mk_map_cong_prem Logic.mk_implies x) zs bnf_sets_As fs fs_copy;
blanchet@51762
  1144
        val eq = mk_Trueprop_eq (Term.list_comb (bnf_map_AsBs, fs) $ x,
blanchet@48975
  1145
          Term.list_comb (bnf_map_AsBs, fs_copy) $ x);
blanchet@48975
  1146
      in
blanchet@51762
  1147
        fold_rev Logic.all (x :: fs @ fs_copy) (Logic.list_implies (prems, eq))
blanchet@48975
  1148
      end;
blanchet@48975
  1149
blanchet@53289
  1150
    val set_map0s_goal =
blanchet@48975
  1151
      let
blanchet@48975
  1152
        fun mk_goal setA setB f =
blanchet@48975
  1153
          let
blanchet@58108
  1154
            val set_comp_map = HOLogic.mk_comp (setB, Term.list_comb (bnf_map_AsBs, fs));
blanchet@48975
  1155
            val image_comp_set = HOLogic.mk_comp (mk_image f, setA);
blanchet@48975
  1156
          in
blanchet@49123
  1157
            fold_rev Logic.all fs (mk_Trueprop_eq (set_comp_map, image_comp_set))
blanchet@48975
  1158
          end;
blanchet@48975
  1159
      in
wenzelm@58634
  1160
        @{map 3} mk_goal bnf_sets_As bnf_sets_Bs fs
blanchet@48975
  1161
      end;
blanchet@48975
  1162
blanchet@49458
  1163
    val card_order_bd_goal = HOLogic.mk_Trueprop (mk_card_order bnf_bd_As);
blanchet@48975
  1164
blanchet@49458
  1165
    val cinfinite_bd_goal = HOLogic.mk_Trueprop (mk_cinfinite bnf_bd_As);
blanchet@48975
  1166
blanchet@49458
  1167
    val set_bds_goal =
blanchet@48975
  1168
      let
blanchet@48975
  1169
        fun mk_goal set =
blanchet@48975
  1170
          Logic.all x (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of (set $ x)) bnf_bd_As));
blanchet@48975
  1171
      in
blanchet@48975
  1172
        map mk_goal bnf_sets_As
blanchet@48975
  1173
      end;
blanchet@48975
  1174
traytel@54841
  1175
    val relAsCs = mk_bnf_rel pred2RTsAsCs CA' CC';
traytel@54841
  1176
    val relBsCs = mk_bnf_rel pred2RTsBsCs CB' CC';
desharna@57932
  1177
    val relCsBs = mk_bnf_rel pred2RTsCsBs CC' CB';
traytel@54841
  1178
    val rel_OO_lhs = Term.list_comb (relAsCs, map2 (curry mk_rel_compp) Rs Ss);
traytel@54841
  1179
    val rel_OO_rhs = mk_rel_compp (Term.list_comb (rel, Rs), Term.list_comb (relBsCs, Ss));
traytel@54841
  1180
    val le_rel_OO_goal =
traytel@54841
  1181
      fold_rev Logic.all (Rs @ Ss) (HOLogic.mk_Trueprop (mk_leq rel_OO_rhs rel_OO_lhs));
blanchet@48975
  1182
traytel@54841
  1183
    val rel_OO_Grp_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (rel, Rs),
traytel@54841
  1184
      Term.list_comb (mk_OO_Grp Ds As' Bs', Rs)));
blanchet@49453
  1185
blanchet@53289
  1186
    val goals = zip_axioms map_id0_goal map_comp0_goal map_cong0_goal set_map0s_goal
traytel@54841
  1187
      card_order_bd_goal cinfinite_bd_goal set_bds_goal le_rel_OO_goal rel_OO_Grp_goal;
blanchet@48975
  1188
traytel@60918
  1189
    val mk_wit_goals = mk_wit_goals bs zs bnf_sets_As;
traytel@55197
  1190
    fun triv_wit_tac ctxt = mk_trivial_wit_tac ctxt bnf_wit_defs;
blanchet@48975
  1191
traytel@54189
  1192
    val wit_goalss =
blanchet@54921
  1193
      (if null raw_wits then SOME triv_wit_tac else NONE, map mk_wit_goals bnf_wit_As);
traytel@54189
  1194
traytel@54189
  1195
    fun after_qed mk_wit_thms thms lthy =
blanchet@48975
  1196
      let
traytel@54189
  1197
        val (axioms, nontriv_wit_thms) = apfst (mk_axioms live) (chop (length goals) thms);
blanchet@48975
  1198
traytel@49109
  1199
        val bd_Card_order = #bd_card_order axioms RS @{thm conjunct2[OF card_order_on_Card_order]};
blanchet@48975
  1200
        val bd_Cinfinite = @{thm conjI} OF [#bd_cinfinite axioms, bd_Card_order];
blanchet@48975
  1201
        val bd_Cnotzero = bd_Cinfinite RS @{thm Cinfinite_Cnotzero};
blanchet@48975
  1202
blanchet@51766
  1203
        fun mk_collect_set_map () =
blanchet@48975
  1204
          let
traytel@54841
  1205
            val defT = mk_bnf_T Ts Calpha --> HOLogic.mk_setT T;
blanchet@58108
  1206
            val collect_map = HOLogic.mk_comp (mk_collect (map (mk_bnf_t Ts) bnf_sets) defT,
blanchet@48975
  1207
              Term.list_comb (mk_bnf_map As' Ts, hs));
blanchet@48975
  1208
            val image_collect = mk_collect
blanchet@58108
  1209
              (map2 (fn h => fn set => HOLogic.mk_comp (mk_image h, set)) hs bnf_sets_As) defT;
blanchet@48975
  1210
            (*collect {set1 ... setm} o map f1 ... fm = collect {f1` o set1 ... fm` o setm}*)
blanchet@49123
  1211
            val goal = fold_rev Logic.all hs (mk_Trueprop_eq (collect_map, image_collect));
blanchet@48975
  1212
          in
traytel@60728
  1213
            Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => 
traytel@60728
  1214
              mk_collect_set_map_tac ctxt (#set_map0 axioms))
traytel@49109
  1215
            |> Thm.close_derivation
blanchet@48975
  1216
          end;
blanchet@48975
  1217
blanchet@51766
  1218
        val collect_set_map = Lazy.lazy mk_collect_set_map;
blanchet@48975
  1219
blanchet@48975
  1220
        fun mk_in_mono () =
blanchet@48975
  1221
          let
traytel@51893
  1222
            val prems_mono = map2 (HOLogic.mk_Trueprop oo mk_leq) As As_copy;
blanchet@49458
  1223
            val in_mono_goal =
blanchet@48975
  1224
              fold_rev Logic.all (As @ As_copy)
blanchet@48975
  1225
                (Logic.list_implies (prems_mono, HOLogic.mk_Trueprop
traytel@51893
  1226
                  (mk_leq (mk_in As bnf_sets_As CA') (mk_in As_copy bnf_sets_As CA'))));
blanchet@48975
  1227
          in
traytel@60728
  1228
            Goal.prove_sorry lthy [] [] in_mono_goal (fn {context = ctxt, prems = _} =>
traytel@60728
  1229
              mk_in_mono_tac ctxt live)
traytel@49109
  1230
            |> Thm.close_derivation
blanchet@48975
  1231
          end;
blanchet@48975
  1232
blanchet@49538
  1233
        val in_mono = Lazy.lazy mk_in_mono;
blanchet@48975
  1234
blanchet@48975
  1235
        fun mk_in_cong () =
blanchet@48975
  1236
          let
blanchet@51762
  1237
            val prems_cong = map2 (curry mk_Trueprop_eq) As As_copy;
blanchet@49458
  1238
            val in_cong_goal =
blanchet@48975
  1239
              fold_rev Logic.all (As @ As_copy)
blanchet@51762
  1240
                (Logic.list_implies (prems_cong,
blanchet@51762
  1241
                  mk_Trueprop_eq (mk_in As bnf_sets_As CA', mk_in As_copy bnf_sets_As CA')));
blanchet@48975
  1242
          in
wenzelm@51798
  1243
            Goal.prove_sorry lthy [] [] in_cong_goal
traytel@60728
  1244
              (fn {context = ctxt, prems = _} => (TRY o hyp_subst_tac ctxt THEN' rtac ctxt refl) 1)
traytel@49109
  1245
            |> Thm.close_derivation
blanchet@48975
  1246
          end;
blanchet@48975
  1247
blanchet@49538
  1248
        val in_cong = Lazy.lazy mk_in_cong;
blanchet@48975
  1249
blanchet@53285
  1250
        val map_id = Lazy.lazy (fn () => mk_map_id (#map_id0 axioms));
blanchet@57399
  1251
        val map_ident0 = Lazy.lazy (fn () => mk_map_ident lthy (#map_id0 axioms));
desharna@56903
  1252
        val map_ident = Lazy.lazy (fn () => mk_map_ident lthy (Lazy.force map_id));
blanchet@53288
  1253
        val map_comp = Lazy.lazy (fn () => mk_map_comp (#map_comp0 axioms));
blanchet@51762
  1254
desharna@57981
  1255
        fun mk_map_cong mk_implies () =
blanchet@51762
  1256
          let
blanchet@51762
  1257
            val prem0 = mk_Trueprop_eq (x, x_copy);
wenzelm@58634
  1258
            val prems = @{map 4} (mk_map_cong_prem mk_implies x_copy) zs bnf_sets_As fs fs_copy;
blanchet@51762
  1259
            val eq = mk_Trueprop_eq (Term.list_comb (bnf_map_AsBs, fs) $ x,
blanchet@51762
  1260
              Term.list_comb (bnf_map_AsBs, fs_copy) $ x_copy);
blanchet@51762
  1261
            val goal = fold_rev Logic.all (x :: x_copy :: fs @ fs_copy)
blanchet@51762
  1262
              (Logic.list_implies (prem0 :: prems, eq));
blanchet@51762
  1263
          in
traytel@61271
  1264
            Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
traytel@61271
  1265
              unfold_thms_tac ctxt @{thms simp_implies_def} THEN
traytel@61271
  1266
              mk_map_cong_tac ctxt (#map_cong0 axioms))
blanchet@51762
  1267
            |> Thm.close_derivation
blanchet@51762
  1268
          end;
blanchet@51762
  1269
desharna@57981
  1270
        val map_cong = Lazy.lazy (mk_map_cong Logic.mk_implies);
desharna@57981
  1271
        val map_cong_simp = Lazy.lazy (mk_map_cong (fn (a, b) => @{term simp_implies} $ a $ b));
blanchet@48975
  1272
blanchet@56635
  1273
        fun mk_inj_map () =
blanchet@56635
  1274
          let
blanchet@56635
  1275
            val prems = map (HOLogic.mk_Trueprop o mk_inj) fs;
blanchet@56635
  1276
            val concl = HOLogic.mk_Trueprop (mk_inj (Term.list_comb (bnf_map_AsBs, fs)));
blanchet@56635
  1277
            val goal = fold_rev Logic.all fs (Logic.list_implies (prems, concl));
blanchet@56635
  1278
          in
traytel@60728
  1279
            Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
traytel@60728
  1280
              mk_inj_map_tac ctxt live (Lazy.force map_id) (Lazy.force map_comp) (#map_cong0 axioms)
traytel@60728
  1281
                (Lazy.force map_cong))
blanchet@56635
  1282
            |> Thm.close_derivation
blanchet@56635
  1283
          end;
blanchet@56635
  1284
blanchet@56635
  1285
        val inj_map = Lazy.lazy mk_inj_map;
blanchet@56635
  1286
blanchet@53290
  1287
        val set_map = map (fn thm => Lazy.lazy (fn () => mk_set_map thm)) (#set_map0 axioms);
blanchet@48975
  1288
traytel@54189
  1289
        val wit_thms =
traytel@54189
  1290
          if null nontriv_wit_thms then mk_wit_thms (map Lazy.force set_map) else nontriv_wit_thms;
traytel@54189
  1291
traytel@52635
  1292
        fun mk_in_bd () =
traytel@52635
  1293
          let
traytel@52813
  1294
            val bdT = fst (dest_relT (fastype_of bnf_bd_As));
traytel@52813
  1295
            val bdTs = replicate live bdT;
traytel@54841
  1296
            val bd_bnfT = mk_bnf_T bdTs Calpha;
traytel@52813
  1297
            val surj_imp_ordLeq_inst = (if live = 0 then TrueI else
traytel@52813
  1298
              let
traytel@52813
  1299
                val ranTs = map (fn AT => mk_sumT (AT, HOLogic.unitT)) As';
traytel@52813
  1300
                val funTs = map (fn T => bdT --> T) ranTs;
traytel@54841
  1301
                val ran_bnfT = mk_bnf_T ranTs Calpha;
traytel@52813
  1302
                val (revTs, Ts) = `rev (bd_bnfT :: funTs);
wenzelm@59621
  1303
                val cTs = map (SOME o Thm.ctyp_of lthy) [ran_bnfT, Library.foldr1 HOLogic.mk_prodT Ts];
haftmann@61424
  1304
                val tinst = fold (fn T => fn t => HOLogic.mk_case_prod (Term.absdummy T t)) (tl revTs)
traytel@52813
  1305
                  (Term.absdummy (hd revTs) (Term.list_comb (mk_bnf_map bdTs ranTs,
traytel@52813
  1306
                    map Bound (live - 1 downto 0)) $ Bound live));
wenzelm@59621
  1307
                val cts = [NONE, SOME (Thm.cterm_of lthy tinst)];
traytel@52813
  1308
              in
wenzelm@60801
  1309
                Thm.instantiate' cTs cts @{thm surj_imp_ordLeq}
traytel@52813
  1310
              end);
traytel@52635
  1311
            val bd = mk_cexp
traytel@52635
  1312
              (if live = 0 then ctwo
traytel@52635
  1313
                else mk_csum (Library.foldr1 (uncurry mk_csum) (map mk_card_of As)) ctwo)
traytel@52813
  1314
              (mk_csum bnf_bd_As (mk_card_of (HOLogic.mk_UNIV bd_bnfT)));
traytel@52635
  1315
            val in_bd_goal =
traytel@52635
  1316
              fold_rev Logic.all As
traytel@52635
  1317
                (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of (mk_in As bnf_sets_As CA')) bd));
traytel@52635
  1318
          in
traytel@52635
  1319
            Goal.prove_sorry lthy [] [] in_bd_goal
traytel@55197
  1320
              (fn {context = ctxt, prems = _} => mk_in_bd_tac ctxt live surj_imp_ordLeq_inst
blanchet@53288
  1321
                (Lazy.force map_comp) (Lazy.force map_id) (#map_cong0 axioms)
blanchet@53290
  1322
                (map Lazy.force set_map) (#set_bd axioms) (#bd_card_order axioms)
traytel@52635
  1323
                bd_Card_order bd_Cinfinite bd_Cnotzero)
traytel@52635
  1324
            |> Thm.close_derivation
traytel@52635
  1325
          end;
traytel@52635
  1326
traytel@52635
  1327
        val in_bd = Lazy.lazy mk_in_bd;
traytel@52635
  1328
traytel@53561
  1329
        val rel_OO_Grp = #rel_OO_Grp axioms;
traytel@53561
  1330
        val rel_OO_Grps = no_refl [rel_OO_Grp];
blanchet@48975
  1331
traytel@51893
  1332
        fun mk_rel_Grp () =
blanchet@48975
  1333
          let
traytel@51893
  1334
            val lhs = Term.list_comb (rel, map2 mk_Grp As fs);
traytel@51893
  1335
            val rhs = mk_Grp (mk_in As bnf_sets_As CA') (Term.list_comb (bnf_map_AsBs, fs));
blanchet@49123
  1336
            val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs));
blanchet@48975
  1337
          in
wenzelm@51551
  1338
            Goal.prove_sorry lthy [] [] goal
traytel@55197
  1339
              (fn {context = ctxt, prems = _} => mk_rel_Grp_tac ctxt rel_OO_Grps (#map_id0 axioms)
traytel@55197
  1340
                (#map_cong0 axioms) (Lazy.force map_id) (Lazy.force map_comp)
traytel@55197
  1341
                (map Lazy.force set_map))
traytel@49109
  1342
            |> Thm.close_derivation
blanchet@48975
  1343
          end;
blanchet@48975
  1344
traytel@51893
  1345
        val rel_Grp = Lazy.lazy mk_rel_Grp;
blanchet@48975
  1346
traytel@61242
  1347
        fun mk_rel_prems f = map2 (HOLogic.mk_Trueprop oo f) Rs Rs_copy;
traytel@51893
  1348
        fun mk_rel_concl f = HOLogic.mk_Trueprop
traytel@51893
  1349
          (f (Term.list_comb (rel, Rs), Term.list_comb (rel, Rs_copy)));
blanchet@48975
  1350
traytel@51893
  1351
        fun mk_rel_mono () =
blanchet@48975
  1352
          let
traytel@51893
  1353
            val mono_prems = mk_rel_prems mk_leq;
traytel@51893
  1354
            val mono_concl = mk_rel_concl (uncurry mk_leq);
blanchet@48975
  1355
          in
wenzelm@51551
  1356
            Goal.prove_sorry lthy [] []
blanchet@48975
  1357
              (fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (mono_prems, mono_concl)))
traytel@60728
  1358
              (fn {context = ctxt, prems = _} =>
traytel@60728
  1359
                mk_rel_mono_tac ctxt rel_OO_Grps (Lazy.force in_mono))
traytel@49109
  1360
            |> Thm.close_derivation
blanchet@48975
  1361
          end;
blanchet@48975
  1362
traytel@61242
  1363
        fun mk_rel_cong0 () =
blanchet@48975
  1364
          let
traytel@51893
  1365
            val cong_prems = mk_rel_prems (curry HOLogic.mk_eq);
traytel@51893
  1366
            val cong_concl = mk_rel_concl HOLogic.mk_eq;
blanchet@48975
  1367
          in
wenzelm@51551
  1368
            Goal.prove_sorry lthy [] []
blanchet@48975
  1369
              (fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (cong_prems, cong_concl)))
traytel@60728
  1370
              (fn {context = ctxt, prems = _} => (TRY o hyp_subst_tac ctxt THEN' rtac ctxt refl) 1)
traytel@49109
  1371
            |> Thm.close_derivation
blanchet@48975
  1372
          end;
blanchet@48975
  1373
traytel@51893
  1374
        val rel_mono = Lazy.lazy mk_rel_mono;
traytel@61242
  1375
        val rel_cong0 = Lazy.lazy mk_rel_cong0;
blanchet@48975
  1376
traytel@51893
  1377
        fun mk_rel_eq () =
traytel@52719
  1378
          Goal.prove_sorry lthy [] []
traytel@52719
  1379
            (mk_Trueprop_eq (Term.list_comb (relAsAs, map HOLogic.eq_const As'),
traytel@52719
  1380
              HOLogic.eq_const CA'))
traytel@60728
  1381
            (fn {context = ctxt, prems = _} =>
traytel@61242
  1382
              mk_rel_eq_tac ctxt live (Lazy.force rel_Grp) (Lazy.force rel_cong0) (#map_id0 axioms))
traytel@52719
  1383
          |> Thm.close_derivation;
blanchet@48975
  1384
traytel@51893
  1385
        val rel_eq = Lazy.lazy mk_rel_eq;
blanchet@48975
  1386
traytel@51893
  1387
        fun mk_rel_conversep () =
blanchet@48975
  1388
          let
traytel@51893
  1389
            val relBsAs = mk_bnf_rel pred2RT's CB' CA';
traytel@51893
  1390
            val lhs = Term.list_comb (relBsAs, map mk_conversep Rs);
traytel@51893
  1391
            val rhs = mk_conversep (Term.list_comb (rel, Rs));
traytel@51893
  1392
            val le_goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (mk_leq lhs rhs));
wenzelm@51551
  1393
            val le_thm = Goal.prove_sorry lthy [] [] le_goal
traytel@55197
  1394
              (fn {context = ctxt, prems = _} => mk_rel_conversep_le_tac ctxt rel_OO_Grps
traytel@55197
  1395
                (Lazy.force rel_eq) (#map_cong0 axioms) (Lazy.force map_comp)
traytel@55197
  1396
                (map Lazy.force set_map))
traytel@49109
  1397
              |> Thm.close_derivation
blanchet@49123
  1398
            val goal = fold_rev Logic.all Rs (mk_Trueprop_eq (lhs, rhs));
blanchet@48975
  1399
          in
traytel@51893
  1400
            Goal.prove_sorry lthy [] [] goal
traytel@60728
  1401
              (fn {context = ctxt, prems = _} =>
traytel@60728
  1402
                mk_rel_conversep_tac ctxt le_thm (Lazy.force rel_mono))
traytel@49109
  1403
            |> Thm.close_derivation
blanchet@48975
  1404
          end;
blanchet@48975
  1405
traytel@51893
  1406
        val rel_conversep = Lazy.lazy mk_rel_conversep;
blanchet@48975
  1407
traytel@51893
  1408
        fun mk_rel_OO () =
traytel@54841
  1409
          Goal.prove_sorry lthy [] []
traytel@54841
  1410
            (fold_rev Logic.all (Rs @ Ss) (HOLogic.mk_Trueprop (mk_leq rel_OO_lhs rel_OO_rhs)))
traytel@55197
  1411
            (fn {context = ctxt, prems = _} => mk_rel_OO_le_tac ctxt rel_OO_Grps (Lazy.force rel_eq)
traytel@55197
  1412
              (#map_cong0 axioms) (Lazy.force map_comp) (map Lazy.force set_map))
traytel@54841
  1413
          |> Thm.close_derivation
traytel@54841
  1414
          |> (fn thm => @{thm antisym} OF [thm, #le_rel_OO axioms]);
blanchet@48975
  1415
traytel@51893
  1416
        val rel_OO = Lazy.lazy mk_rel_OO;
blanchet@48975
  1417
traytel@53561
  1418
        fun mk_in_rel () = trans OF [rel_OO_Grp, @{thm OO_Grp_alt}] RS @{thm predicate2_eqD};
blanchet@48975
  1419
traytel@51893
  1420
        val in_rel = Lazy.lazy mk_in_rel;
blanchet@49537
  1421
blanchet@49537
  1422
        fun mk_rel_flip () =
traytel@61334
  1423
          unfold_thms lthy @{thms conversep_iff} (Lazy.force rel_conversep RS @{thm predicate2_eqD});
blanchet@49537
  1424
blanchet@49538
  1425
        val rel_flip = Lazy.lazy mk_rel_flip;
blanchet@49537
  1426
desharna@57967
  1427
        fun mk_rel_mono_strong0 () =
traytel@51916
  1428
          let
traytel@51916
  1429
            fun mk_prem setA setB R S a b =
traytel@51916
  1430
              HOLogic.mk_Trueprop
traytel@51916
  1431
                (mk_Ball (setA $ x) (Term.absfree (dest_Free a)
traytel@51916
  1432
                  (mk_Ball (setB $ y) (Term.absfree (dest_Free b)
traytel@51916
  1433
                    (HOLogic.mk_imp (R $ a $ b, S $ a $ b))))));
desharna@57301
  1434
            val prems = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs) $ x $ y) ::
wenzelm@58634
  1435
              @{map 6} mk_prem bnf_sets_As bnf_sets_Bs Rs Rs_copy zs ys;
traytel@51916
  1436
            val concl = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs_copy) $ x $ y);
traytel@51916
  1437
          in
traytel@51916
  1438
            Goal.prove_sorry lthy [] []
traytel@51916
  1439
              (fold_rev Logic.all (x :: y :: Rs @ Rs_copy) (Logic.list_implies (prems, concl)))
desharna@57967
  1440
              (fn {context = ctxt, prems = _} => mk_rel_mono_strong0_tac ctxt (Lazy.force in_rel)
traytel@55197
  1441
                (map Lazy.force set_map))
traytel@51916
  1442
            |> Thm.close_derivation
traytel@51916
  1443
          end;
traytel@51916
  1444
desharna@57967
  1445
        val rel_mono_strong0 = Lazy.lazy mk_rel_mono_strong0;
traytel@51916
  1446
desharna@57968
  1447
        fun mk_rel_mono_strong () = Object_Logic.rulify lthy (Lazy.force rel_mono_strong0)
desharna@57968
  1448
desharna@57968
  1449
        val rel_mono_strong = Lazy.lazy mk_rel_mono_strong;
desharna@57968
  1450
traytel@61242
  1451
        fun mk_rel_cong_prem mk_implies x x' z z' set set' R R_copy =
traytel@61242
  1452
          Logic.all z (Logic.all z'
traytel@61242
  1453
            (mk_implies (mk_Trueprop_mem (z, set $ x), mk_implies (mk_Trueprop_mem (z', set' $ x'),
traytel@61242
  1454
              mk_Trueprop_eq (R $ z $ z', R_copy $ z $ z')))));
traytel@61242
  1455
traytel@61242
  1456
        fun mk_rel_cong mk_implies () =
traytel@61242
  1457
          let
traytel@61242
  1458
            val prem0 = mk_Trueprop_eq (x, x_copy);
traytel@61242
  1459
            val prem1 = mk_Trueprop_eq (y, y_copy);
traytel@61242
  1460
            val prems = @{map 6} (mk_rel_cong_prem mk_implies x_copy y_copy)
traytel@61242
  1461
              zs ys bnf_sets_As bnf_sets_Bs Rs Rs_copy;
traytel@61242
  1462
            val eq = mk_Trueprop_eq (Term.list_comb (rel, Rs) $ x $ y,
traytel@61242
  1463
              Term.list_comb (rel, Rs_copy) $ x_copy $ y_copy);
traytel@61242
  1464
          in
traytel@61334
  1465
            fold (Variable.add_free_names lthy) (eq :: prem0 :: prem1 :: prems) []
traytel@61334
  1466
            |> (fn vars => Goal.prove_sorry lthy vars (prem0 :: prem1 :: prems) eq
traytel@61242
  1467
              (fn {context = ctxt, prems} =>
traytel@61334
  1468
                mk_rel_cong_tac ctxt (chop 2 prems) (Lazy.force rel_mono_strong)))
traytel@61242
  1469
            |> Thm.close_derivation
traytel@61242
  1470
          end;
traytel@61242
  1471
traytel@61242
  1472
        val rel_cong = Lazy.lazy (mk_rel_cong Logic.mk_implies);
traytel@61242
  1473
        val rel_cong_simp = Lazy.lazy (mk_rel_cong (fn (a, b) => @{term simp_implies} $ a $ b));
traytel@61242
  1474
desharna@57932
  1475
        fun mk_rel_map () =
desharna@57932
  1476
          let
desharna@57932
  1477
            fun mk_goal lhs rhs =
desharna@57932
  1478
              fold_rev Logic.all ([x, y] @ S_CsBs @ S_AsCs @ is @ gs) (mk_Trueprop_eq (lhs, rhs));
desharna@57932
  1479
desharna@57932
  1480
            val lhss =
desharna@57932
  1481
              [Term.list_comb (relCsBs, S_CsBs) $ (Term.list_comb (bnf_map_AsCs, is) $ x) $ y,
desharna@57932
  1482
               Term.list_comb (relAsCs, S_AsCs) $ x $ (Term.list_comb (bnf_map_BsCs, gs) $ y)];
desharna@57932
  1483
            val rhss =
wenzelm@58634
  1484
              [Term.list_comb (rel, @{map 3} (fn f => fn P => fn T =>
desharna@57932
  1485
                 mk_vimage2p f (HOLogic.id_const T) $ P) is S_CsBs Bs') $ x $ y,
wenzelm@58634
  1486
               Term.list_comb (rel, @{map 3} (fn f => fn P => fn T =>
desharna@57932
  1487
                 mk_vimage2p (HOLogic.id_const T) f $ P) gs S_AsCs As') $ x $ y];
desharna@57932
  1488
            val goals = map2 mk_goal lhss rhss;
desharna@57932
  1489
          in
desharna@57970
  1490
            goals
desharna@57970
  1491
            |> map (fn goal => Goal.prove_sorry lthy [] [] goal
desharna@57932
  1492
              (fn {context = ctxt, prems = _} =>
desharna@57932
  1493
                 mk_rel_map0_tac ctxt live (Lazy.force rel_OO) (Lazy.force rel_conversep)
desharna@57970
  1494
                  (Lazy.force rel_Grp) (Lazy.force map_id)))
desharna@57970
  1495
            |> map (unfold_thms lthy @{thms vimage2p_def[of id, unfolded id_apply]
desharna@57970
  1496
                 vimage2p_def[of _ id, unfolded id_apply]})
desharna@57932
  1497
            |> map Thm.close_derivation
desharna@57932
  1498
          end;
desharna@57932
  1499
desharna@57932
  1500
        val rel_map = Lazy.lazy mk_rel_map;
desharna@57932
  1501
traytel@59726
  1502
        fun mk_rel_refl () = @{thm ge_eq_refl[OF ord_eq_le_trans]} OF
traytel@59726
  1503
          [Lazy.force rel_eq RS sym, Lazy.force rel_mono OF (replicate live @{thm refl_ge_eq})];
traytel@59726
  1504
traytel@59726
  1505
        val rel_refl = Lazy.lazy mk_rel_refl;
traytel@59726
  1506
traytel@61240
  1507
        fun mk_rel_refl_strong () =
traytel@61240
  1508
          (rule_by_tactic lthy (ALLGOALS (Object_Logic.full_atomize_tac lthy))
traytel@61240
  1509
            ((Lazy.force rel_eq RS @{thm predicate2_eqD}) RS @{thm iffD2[OF _ refl]} RS
traytel@61240
  1510
              Lazy.force rel_mono_strong)) OF
traytel@61240
  1511
            (replicate live @{thm diag_imp_eq_le})
traytel@61240
  1512
traytel@61240
  1513
        val rel_refl_strong = Lazy.lazy mk_rel_refl_strong;
traytel@61240
  1514
traytel@61240
  1515
        fun mk_rel_preserves mk_prop prop_conv_thm thm () =
traytel@61240
  1516
          let
traytel@61240
  1517
            val Rs = map2 retype_const_or_free self_pred2RTs Rs;
traytel@61240
  1518
            val prems = map (HOLogic.mk_Trueprop o mk_prop) Rs;
traytel@61240
  1519
            val goal = HOLogic.mk_Trueprop (mk_prop (Term.list_comb (relAsAs, Rs)));
traytel@61334
  1520
        val vars = fold (Variable.add_free_names lthy) (goal :: prems) [];
traytel@61240
  1521
          in
traytel@61334
  1522
            Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, goal))
traytel@61240
  1523
              (fn {context = ctxt, prems = _} =>
traytel@61240
  1524
                unfold_thms_tac ctxt [prop_conv_thm] THEN
traytel@61240
  1525
                HEADGOAL (rtac ctxt (Lazy.force thm RS sym RS @{thm ord_eq_le_trans}) 
traytel@61240
  1526
                  THEN' rtac ctxt (Lazy.force rel_mono) THEN_ALL_NEW assume_tac ctxt))
traytel@61240
  1527
            |> Thm.close_derivation
traytel@61240
  1528
          end;
traytel@61240
  1529
traytel@61240
  1530
        val rel_reflp = Lazy.lazy (mk_rel_preserves mk_reflp @{thm reflp_eq} rel_eq);
traytel@61240
  1531
        val rel_symp = Lazy.lazy (mk_rel_preserves mk_symp @{thm symp_conversep} rel_conversep);
traytel@61240
  1532
        val rel_transp = Lazy.lazy (mk_rel_preserves mk_transp @{thm transp_relcompp} rel_OO);
traytel@61240
  1533
traytel@52719
  1534
        fun mk_map_transfer () =
traytel@52719
  1535
          let
blanchet@55945
  1536
            val rels = map2 mk_rel_fun transfer_domRs transfer_ranRs;
blanchet@55945
  1537
            val rel = mk_rel_fun
traytel@52725
  1538
              (Term.list_comb (mk_bnf_rel transfer_domRTs CA' CB1, transfer_domRs))
traytel@52725
  1539
              (Term.list_comb (mk_bnf_rel transfer_ranRTs CB' CB2, transfer_ranRs));
traytel@52725
  1540
            val concl = HOLogic.mk_Trueprop
blanchet@55945
  1541
              (fold_rev mk_rel_fun rels rel $ bnf_map_AsBs $ mk_bnf_map B1Ts B2Ts);
traytel@52719
  1542
          in
traytel@52719
  1543
            Goal.prove_sorry lthy [] []
traytel@52725
  1544
              (fold_rev Logic.all (transfer_domRs @ transfer_ranRs) concl)
traytel@55197
  1545
              (fn {context = ctxt, prems = _} => mk_map_transfer_tac ctxt (Lazy.force rel_mono)
traytel@55197
  1546
                (Lazy.force in_rel) (map Lazy.force set_map) (#map_cong0 axioms)
traytel@55197
  1547
                (Lazy.force map_comp))
traytel@52719
  1548
            |> Thm.close_derivation
traytel@52719
  1549
          end;
traytel@52719
  1550
traytel@52719
  1551
        val map_transfer = Lazy.lazy mk_map_transfer;
traytel@52719
  1552
desharna@58104
  1553
        fun mk_rel_transfer () =
desharna@58104
  1554
          let
desharna@58104
  1555
            val iff = HOLogic.eq_const HOLogic.boolT;
desharna@58104
  1556
            val prem_rels =
desharna@58104
  1557
              map2 (fn T1 => fn T2 => mk_rel_fun T1 (mk_rel_fun T2 iff)) S_AsCs S_BsEs;
desharna@58104
  1558
            val prem_elems =
desharna@58104
  1559
              mk_rel_fun (Term.list_comb (mk_bnf_rel pred2RTsAsCs CA' CC', S_AsCs))
desharna@58104
  1560
                (mk_rel_fun (Term.list_comb (mk_bnf_rel pred2RTsBsEs CB' CE', S_BsEs)) iff);
desharna@58104
  1561
            val goal =
desharna@58104
  1562
              HOLogic.mk_Trueprop (fold_rev mk_rel_fun prem_rels prem_elems $ rel $ relCsEs);
traytel@61334
  1563
            val vars = Variable.add_free_names lthy goal [];
desharna@58104
  1564
          in
traytel@61334
  1565
            Goal.prove_sorry lthy vars [] goal
desharna@58104
  1566
              (fn {context = ctxt, prems = _} =>
desharna@58104
  1567
                mk_rel_transfer_tac ctxt (Lazy.force in_rel) (Lazy.force rel_map)
desharna@58104
  1568
                  (Lazy.force rel_mono_strong))
desharna@58104
  1569
            |> Thm.close_derivation
desharna@58104
  1570
          end;
desharna@58104
  1571
desharna@58104
  1572
        val rel_transfer = Lazy.lazy mk_rel_transfer;
desharna@58104
  1573
desharna@58106
  1574
        fun mk_set_transfer () =
desharna@58106
  1575
          let
desharna@58106
  1576
            val rel_sets = map2 (fn A => fn B => mk_rel 1 [A] [B] @{term rel_set}) As' Bs';
desharna@58106
  1577
            val rel_Rs = Term.list_comb (rel, Rs);
wenzelm@58634
  1578
            val goals = @{map 4} (fn R => fn rel_set => fn setA => fn setB => HOLogic.mk_Trueprop
desharna@58106
  1579
              (mk_rel_fun rel_Rs (rel_set $ R) $ setA $ setB)) Rs rel_sets bnf_sets_As bnf_sets_Bs;
desharna@58106
  1580
          in
desharna@58106
  1581
            if null goals then []
desharna@58106
  1582
            else
traytel@61334
  1583
              let
traytel@61334
  1584
                val goal = Logic.mk_conjunction_balanced goals;
traytel@61334
  1585
                val vars = Variable.add_free_names lthy goal [];
traytel@61334
  1586
              in
traytel@61334
  1587
                Goal.prove_sorry lthy vars [] goal
traytel@61334
  1588
                  (fn {context = ctxt, prems = _} =>
traytel@61334
  1589
                     mk_set_transfer_tac ctxt (Lazy.force in_rel) (map Lazy.force set_map))
traytel@61334
  1590
                |> Thm.close_derivation
traytel@61334
  1591
                |> Conjunction.elim_balanced (length goals)
traytel@61334
  1592
              end
desharna@58106
  1593
          end;
desharna@58106
  1594
desharna@58106
  1595
        val set_transfer = Lazy.lazy mk_set_transfer;
desharna@58106
  1596
desharna@57970
  1597
        fun mk_inj_map_strong () =
desharna@57970
  1598
          let
wenzelm@58634
  1599
            val assms = @{map 5} (fn setA => fn z => fn f => fn z' => fn f' =>
desharna@57970
  1600
              fold_rev Logic.all [z, z']
desharna@57970
  1601
                (Logic.mk_implies (mk_Trueprop_mem (z, setA $ x),
desharna@57970
  1602
                   Logic.mk_implies (mk_Trueprop_mem (z', setA $ x'),
desharna@57970
  1603
                     Logic.mk_implies (mk_Trueprop_eq (f $ z, f' $ z'),
desharna@57970
  1604
                       mk_Trueprop_eq (z, z')))))) bnf_sets_As zs fs zs' fs';
desharna@57970
  1605
            val concl = Logic.mk_implies
desharna@57970
  1606
              (mk_Trueprop_eq
desharna@57970
  1607
                 (Term.list_comb (bnf_map_AsBs, fs) $ x,
desharna@57970
  1608
                  Term.list_comb (bnf_map_AsBs, fs') $ x'),
desharna@57970
  1609
               mk_Trueprop_eq (x, x'));
desharna@57970
  1610
            val goal = fold_rev Logic.all (x :: x' :: fs @ fs')
desharna@57970
  1611
              (fold_rev (curry Logic.mk_implies) assms concl);
desharna@57970
  1612
          in
desharna@57970
  1613
            Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
desharna@57970
  1614
              mk_inj_map_strong_tac ctxt (Lazy.force rel_eq) (Lazy.force rel_map)
desharna@57970
  1615
                (Lazy.force rel_mono_strong))
desharna@57970
  1616
            |> Thm.close_derivation
desharna@57970
  1617
          end;
desharna@57970
  1618
desharna@57970
  1619
        val inj_map_strong = Lazy.lazy mk_inj_map_strong;
desharna@57970
  1620
traytel@51893
  1621
        val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def;
blanchet@48975
  1622
traytel@52635
  1623
        val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
desharna@57981
  1624
          in_mono in_rel inj_map inj_map_strong map_comp map_cong map_cong_simp map_id map_ident0
traytel@61242
  1625
          map_ident map_transfer rel_eq rel_flip set_map rel_cong0 rel_cong rel_cong_simp rel_map
traytel@61242
  1626
          rel_mono rel_mono_strong0 rel_mono_strong set_transfer rel_Grp rel_conversep rel_OO
traytel@61242
  1627
          rel_refl rel_refl_strong rel_reflp rel_symp rel_transp rel_transfer;
blanchet@48975
  1628
blanchet@48975
  1629
        val wits = map2 mk_witness bnf_wits wit_thms;
blanchet@48975
  1630
blanchet@49507
  1631
        val bnf_rel =
blanchet@49507
  1632
          Term.subst_atomic_types ((Ds ~~ deads) @ (As' ~~ alphas) @ (Bs' ~~ betas)) rel;
blanchet@48975
  1633
traytel@54841
  1634
        val bnf = mk_bnf bnf_b Calpha live alphas betas dead deads bnf_map bnf_sets bnf_bd axioms
traytel@54841
  1635
          defs facts wits bnf_rel;
blanchet@48975
  1636
      in
blanchet@57631
  1637
        note_bnf_thms fact_policy qualify bnf_b bnf lthy
blanchet@48975
  1638
      end;
blanchet@49459
  1639
blanchet@49459
  1640
    val one_step_defs =
traytel@51893
  1641
      no_reflexive (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs @ [bnf_rel_def]);
blanchet@48975
  1642
  in
blanchet@49459
  1643
    (key, goals, wit_goalss, after_qed, lthy, one_step_defs)
blanchet@48975
  1644
  end;
blanchet@48975
  1645
wenzelm@58659
  1646
structure BNF_Plugin = Plugin(type T = bnf);
blanchet@56346
  1647
wenzelm@58659
  1648
fun bnf_interpretation name f =
wenzelm@58659
  1649
  BNF_Plugin.interpretation name
wenzelm@58659
  1650
    (fn bnf => fn lthy => f (transfer_bnf (Proof_Context.theory_of lthy) bnf) lthy);
blanchet@56376
  1651
wenzelm@58659
  1652
val interpret_bnf = BNF_Plugin.data;
blanchet@56346
  1653
blanchet@58177
  1654
fun register_bnf_raw key bnf =
blanchet@56346
  1655
  Local_Theory.declaration {syntax = false, pervasive = true}
blanchet@58177
  1656
    (fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf)));
blanchet@58177
  1657
blanchet@58189
  1658
fun register_bnf plugins key bnf =
blanchet@58189
  1659
  register_bnf_raw key bnf #> interpret_bnf plugins bnf;
traytel@49434
  1660
blanchet@58189
  1661
fun bnf_def const_policy fact_policy internal qualify tacs wit_tac Ds map_b rel_b set_bs raw_csts =
traytel@54189
  1662
  (fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) =>
blanchet@48975
  1663
  let
traytel@55197
  1664
    fun mk_wits_tac ctxt set_maps =
traytel@55197
  1665
      TRYALL Goal.conjunction_tac THEN
traytel@54189
  1666
      (case triv_tac_opt of
traytel@55197
  1667
        SOME tac => tac ctxt set_maps
traytel@55197
  1668
      | NONE => unfold_thms_tac ctxt one_step_defs THEN wit_tac ctxt);
traytel@54189
  1669
    val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
traytel@54189
  1670
    fun mk_wit_thms set_maps =
traytel@55197
  1671
      Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
traytel@55197
  1672
        (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps)
wenzelm@61116
  1673
        |> Thm.close_derivation
traytel@54189
  1674
        |> Conjunction.elim_balanced (length wit_goals)
traytel@54189
  1675
        |> map2 (Conjunction.elim_balanced o length) wit_goalss
wenzelm@61116
  1676
        |> (map o map) (Thm.forall_elim_vars 0);
blanchet@48975
  1677
  in
wenzelm@51551
  1678
    map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])
traytel@55197
  1679
      goals (map (fn tac => fn {context = ctxt, prems = _} =>
traytel@55197
  1680
        unfold_thms_tac ctxt one_step_defs THEN tac ctxt) tacs)
traytel@54189
  1681
    |> (fn thms => after_qed mk_wit_thms (map single thms) lthy)
blanchet@58189
  1682
  end) o prepare_def const_policy fact_policy internal qualify (K I) (K I) Ds map_b rel_b set_bs
blanchet@58189
  1683
    raw_csts;
blanchet@48975
  1684
wenzelm@58659
  1685
fun bnf_cmd (raw_csts, raw_plugins) =
blanchet@58189
  1686
  (fn (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, defs) =>
traytel@54189
  1687
  let
wenzelm@58659
  1688
    val plugins = raw_plugins lthy;
traytel@54189
  1689
    val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
traytel@54189
  1690
    fun mk_triv_wit_thms tac set_maps =
traytel@54189
  1691
      Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
traytel@55197
  1692
        (fn {context = ctxt, prems = _} => TRYALL Goal.conjunction_tac THEN tac ctxt set_maps)
wenzelm@61116
  1693
        |> Thm.close_derivation
traytel@54189
  1694
        |> Conjunction.elim_balanced (length wit_goals)
traytel@54189
  1695
        |> map2 (Conjunction.elim_balanced o length) wit_goalss
wenzelm@61116
  1696
        |> (map o map) (Thm.forall_elim_vars 0);
desharna@57301
  1697
    val (mk_wit_thms, nontriv_wit_goals) =
traytel@54189
  1698
      (case triv_tac_opt of
traytel@54189
  1699
        NONE => (fn _ => [], map (map (rpair [])) wit_goalss)
traytel@54189
  1700
      | SOME tac => (mk_triv_wit_thms tac, []));
traytel@54189
  1701
  in
traytel@54189
  1702
    Proof.unfolding ([[(defs, [])]])
blanchet@59663
  1703
      (lthy
blanchet@59663
  1704
       |> Proof.theorem NONE (uncurry (register_bnf plugins key) oo after_qed mk_wit_thms)
blanchet@59663
  1705
         (map (single o rpair []) goals @ nontriv_wit_goals)
blanchet@59663
  1706
       |> Proof.refine (Method.primitive_text (K I))
blanchet@59663
  1707
       |> Seq.hd)
blanchet@58189
  1708
  end) o prepare_def Do_Inline (user_policy Note_Some) false I Syntax.read_typ Syntax.read_term
blanchet@58189
  1709
    NONE Binding.empty Binding.empty [] raw_csts;
blanchet@48975
  1710
blanchet@48975
  1711
fun print_bnfs ctxt =
blanchet@48975
  1712
  let
blanchet@48975
  1713
    fun pretty_set sets i = Pretty.block
blanchet@48975
  1714
      [Pretty.str (mk_setN (i + 1) ^ ":"), Pretty.brk 1,
blanchet@59663
  1715
        Pretty.quote (Syntax.pretty_term ctxt (nth sets i))];
blanchet@48975
  1716
desharna@56903
  1717
    fun pretty_bnf (key, BNF {T, map, sets, bd, live, lives, dead, deads, ...}) =
blanchet@48975
  1718
      Pretty.big_list
blanchet@48975
  1719
        (Pretty.string_of (Pretty.block [Pretty.str key, Pretty.str ":", Pretty.brk 1,
blanchet@48975
  1720
          Pretty.quote (Syntax.pretty_typ ctxt T)]))
blanchet@48975
  1721
        ([Pretty.block [Pretty.str "live:", Pretty.brk 1, Pretty.str (string_of_int live),
blanchet@48975
  1722
            Pretty.brk 3, Pretty.list "[" "]" (List.map (Syntax.pretty_typ ctxt) lives)],
blanchet@48975
  1723
          Pretty.block [Pretty.str "dead:", Pretty.brk 1, Pretty.str (string_of_int dead),
blanchet@48975
  1724
            Pretty.brk 3, Pretty.list "[" "]" (List.map (Syntax.pretty_typ ctxt) deads)],
blanchet@48975
  1725
          Pretty.block [Pretty.str (mapN ^ ":"), Pretty.brk 1,
blanchet@48975
  1726
            Pretty.quote (Syntax.pretty_term ctxt map)]] @
blanchet@48975
  1727
          List.map (pretty_set sets) (0 upto length sets - 1) @
blanchet@48975
  1728
          [Pretty.block [Pretty.str (bdN ^ ":"), Pretty.brk 1,
blanchet@48975
  1729
            Pretty.quote (Syntax.pretty_term ctxt bd)]]);
blanchet@48975
  1730
  in
blanchet@59822
  1731
    Pretty.big_list "Registered bounded natural functors:"
wenzelm@60924
  1732
      (map pretty_bnf (sort_by fst (Symtab.dest (Data.get (Context.Proof ctxt)))))
blanchet@48975
  1733
    |> Pretty.writeln
blanchet@48975
  1734
  end;
blanchet@48975
  1735
blanchet@48975
  1736
val _ =
wenzelm@59936
  1737
  Outer_Syntax.command @{command_keyword print_bnfs}
blanchet@53289
  1738
    "print all bounded natural functors"
blanchet@48975
  1739
    (Scan.succeed (Toplevel.keep (print_bnfs o Toplevel.context_of)));
blanchet@48975
  1740
blanchet@48975
  1741
val _ =
wenzelm@59936
  1742
  Outer_Syntax.local_theory_to_proof @{command_keyword bnf}
blanchet@53289
  1743
    "register a type as a bounded natural functor"
traytel@54421
  1744
    (parse_opt_binding_colon -- Parse.typ --|
traytel@54421
  1745
       (Parse.reserved "map" -- @{keyword ":"}) -- Parse.term --
blanchet@58189
  1746
       Scan.optional ((Parse.reserved "sets" -- @{keyword ":"}) |--
blanchet@58189
  1747
         Scan.repeat1 (Scan.unless (Parse.reserved "bd") Parse.term)) [] --|
traytel@54421
  1748
       (Parse.reserved "bd" -- @{keyword ":"}) -- Parse.term --
blanchet@58189
  1749
       Scan.optional ((Parse.reserved "wits" -- @{keyword ":"}) |--
blanchet@58432
  1750
         Scan.repeat1 (Scan.unless (Parse.reserved "rel" ||
blanchet@58432
  1751
           Parse.reserved "plugins") Parse.term)) [] --
blanchet@58189
  1752
       Scan.option ((Parse.reserved "rel" -- @{keyword ":"}) |-- Parse.term) --
wenzelm@58660
  1753
       Scan.optional Plugin_Name.parse_filter (K Plugin_Name.default_filter)
blanchet@51836
  1754
       >> bnf_cmd);
blanchet@48975
  1755
blanchet@48975
  1756
end;