src/HOL/Tools/BNF/bnf_comp.ML
author wenzelm
Sun Nov 26 21:08:32 2017 +0100 (17 months ago)
changeset 67091 1393c2340eec
parent 65436 1fd2dca8eb60
child 68960 b85d509e7cbf
permissions -rw-r--r--
more symbols;
blanchet@55061
     1
(*  Title:      HOL/Tools/BNF/bnf_comp.ML
blanchet@48975
     2
    Author:     Dmitriy Traytel, TU Muenchen
blanchet@48975
     3
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@48975
     4
    Copyright   2012
blanchet@48975
     5
blanchet@48975
     6
Composition of bounded natural functors.
blanchet@48975
     7
*)
blanchet@48975
     8
blanchet@48975
     9
signature BNF_COMP =
blanchet@48975
    10
sig
blanchet@59994
    11
  val typedef_threshold: int Config.T
blanchet@63800
    12
  val with_typedef_threshold: int -> (Proof.context -> Proof.context) -> Proof.context ->
blanchet@63800
    13
    Proof.context
blanchet@63800
    14
  val with_typedef_threshold_yield: int -> (Proof.context -> 'a * Proof.context) -> Proof.context ->
blanchet@63800
    15
    'a * Proof.context
blanchet@59710
    16
blanchet@51837
    17
  val ID_bnf: BNF_Def.bnf
blanchet@51837
    18
  val DEADID_bnf: BNF_Def.bnf
blanchet@49585
    19
blanchet@55706
    20
  type comp_cache
traytel@65436
    21
  type unfold_set =
traytel@65436
    22
    {map_unfolds: thm list,
traytel@65436
    23
     set_unfoldss: thm list list,
traytel@65436
    24
     rel_unfolds: thm list}
blanchet@55706
    25
blanchet@55706
    26
  val empty_comp_cache: comp_cache
blanchet@49502
    27
  val empty_unfolds: unfold_set
blanchet@48975
    28
blanchet@53222
    29
  exception BAD_DEAD of typ * typ
blanchet@53222
    30
blanchet@62621
    31
  val bnf_of_typ: bool -> BNF_Def.inline_policy -> (binding -> binding) ->
blanchet@55703
    32
    ((string * sort) list list -> (string * sort) list) -> (string * sort) list ->
blanchet@55904
    33
    (string * sort) list -> typ -> (comp_cache * unfold_set) * local_theory ->
blanchet@55904
    34
    (BNF_Def.bnf * (typ list * typ list)) * ((comp_cache * unfold_set) * local_theory)
blanchet@49014
    35
  val default_comp_sort: (string * sort) list list -> (string * sort) list
blanchet@59725
    36
  val clean_compose_bnf: BNF_Def.inline_policy -> (binding -> binding) -> binding -> BNF_Def.bnf ->
blanchet@59725
    37
    BNF_Def.bnf list -> unfold_set * local_theory -> BNF_Def.bnf * (unfold_set * local_theory)
blanchet@59725
    38
  val kill_bnf: (binding -> binding) -> int -> BNF_Def.bnf ->
blanchet@59725
    39
    (comp_cache * unfold_set) * local_theory ->
blanchet@59725
    40
    BNF_Def.bnf * ((comp_cache * unfold_set) * local_theory)
blanchet@59725
    41
  val lift_bnf: (binding -> binding) -> int -> BNF_Def.bnf ->
blanchet@59725
    42
    (comp_cache * unfold_set) * local_theory ->
blanchet@59725
    43
    BNF_Def.bnf * ((comp_cache * unfold_set) * local_theory)
blanchet@59725
    44
  val permute_bnf: (binding -> binding) -> int list -> int list -> BNF_Def.bnf ->
blanchet@59725
    45
    (comp_cache * unfold_set) * local_theory ->
blanchet@59725
    46
    BNF_Def.bnf * ((comp_cache * unfold_set) * local_theory)
blanchet@59725
    47
  val permute_and_kill_bnf: (binding -> binding) -> int -> int list -> int list -> BNF_Def.bnf ->
blanchet@59725
    48
    (comp_cache * unfold_set) * local_theory ->
blanchet@59725
    49
    BNF_Def.bnf * ((comp_cache * unfold_set) * local_theory)
blanchet@59725
    50
  val lift_and_permute_bnf: (binding -> binding) -> int -> int list -> int list -> BNF_Def.bnf ->
blanchet@59725
    51
    (comp_cache * unfold_set) * local_theory ->
blanchet@59725
    52
    BNF_Def.bnf * ((comp_cache * unfold_set) * local_theory)
blanchet@48975
    53
  val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list ->
blanchet@55904
    54
    (''a list list -> ''a list) -> BNF_Def.bnf list -> (comp_cache * unfold_set) * local_theory ->
blanchet@55904
    55
    (int list list * ''a list) * (BNF_Def.bnf list * ((comp_cache * unfold_set) * local_theory))
blanchet@59725
    56
  val compose_bnf: BNF_Def.inline_policy -> (int -> binding -> binding) ->
blanchet@59725
    57
    ((string * sort) list list -> (string * sort) list) -> BNF_Def.bnf -> BNF_Def.bnf list ->
blanchet@59725
    58
    typ list -> typ list list -> typ list list -> (comp_cache * unfold_set) * local_theory ->
blanchet@59725
    59
    (BNF_Def.bnf * (typ list * typ list)) * ((comp_cache * unfold_set) * local_theory)
traytel@55803
    60
  type absT_info =
traytel@55803
    61
    {absT: typ,
traytel@55803
    62
     repT: typ,
traytel@55803
    63
     abs: term,
traytel@55803
    64
     rep: term,
traytel@55803
    65
     abs_inject: thm,
traytel@55803
    66
     abs_inverse: thm,
traytel@55803
    67
     type_definition: thm}
traytel@55803
    68
traytel@55803
    69
  val morph_absT_info: morphism -> absT_info -> absT_info
traytel@55803
    70
  val mk_absT: theory -> typ -> typ -> typ -> typ
traytel@55803
    71
  val mk_repT: typ -> typ -> typ -> typ
traytel@55803
    72
  val mk_abs: typ -> term -> term
traytel@55803
    73
  val mk_rep: typ -> term -> term
blanchet@63837
    74
  val seal_bnf: (binding -> binding) -> unfold_set -> binding -> bool -> typ list -> typ list ->
blanchet@63837
    75
    BNF_Def.bnf -> local_theory -> (BNF_Def.bnf * (typ list * absT_info)) * local_theory
blanchet@48975
    76
end;
blanchet@48975
    77
blanchet@48975
    78
structure BNF_Comp : BNF_COMP =
blanchet@48975
    79
struct
blanchet@48975
    80
blanchet@48975
    81
open BNF_Def
blanchet@48975
    82
open BNF_Util
blanchet@48975
    83
open BNF_Tactics
blanchet@48975
    84
open BNF_Comp_Tactics
blanchet@48975
    85
blanchet@59994
    86
val typedef_threshold = Attrib.setup_config_int @{binding bnf_typedef_threshold} (K 6);
blanchet@59710
    87
blanchet@63800
    88
fun with_typedef_threshold threshold f lthy =
blanchet@63800
    89
  lthy
blanchet@63800
    90
  |> Config.put typedef_threshold threshold
blanchet@63800
    91
  |> f
blanchet@63800
    92
  |> Config.put typedef_threshold (Config.get lthy typedef_threshold);
blanchet@63800
    93
blanchet@63800
    94
fun with_typedef_threshold_yield threshold f lthy =
blanchet@63800
    95
  lthy
blanchet@63800
    96
  |> Config.put typedef_threshold threshold
blanchet@63800
    97
  |> f
blanchet@63800
    98
  ||> Config.put typedef_threshold (Config.get lthy typedef_threshold);
blanchet@63800
    99
blanchet@58128
   100
val ID_bnf = the (bnf_of @{context} "BNF_Composition.ID");
blanchet@58128
   101
val DEADID_bnf = the (bnf_of @{context} "BNF_Composition.DEADID");
blanchet@49585
   102
blanchet@55706
   103
type comp_cache = (bnf * (typ list * typ list)) Typtab.table;
blanchet@55706
   104
blanchet@55904
   105
fun key_of_types s Ts = Type (s, Ts);
blanchet@55904
   106
fun key_of_typess s = key_of_types s o map (key_of_types "");
blanchet@55904
   107
fun typ_of_int n = Type (string_of_int n, []);
blanchet@55904
   108
fun typ_of_bnf bnf =
blanchet@55904
   109
  key_of_typess "" [[T_of_bnf bnf], lives_of_bnf bnf, sort Term_Ord.typ_ord (deads_of_bnf bnf)];
blanchet@55904
   110
blanchet@55904
   111
fun key_of_kill n bnf = key_of_types "k" [typ_of_int n, typ_of_bnf bnf];
blanchet@55904
   112
fun key_of_lift n bnf = key_of_types "l" [typ_of_int n, typ_of_bnf bnf];
blanchet@55904
   113
fun key_of_permute src dest bnf =
blanchet@55904
   114
  key_of_types "p" (map typ_of_int src @ map typ_of_int dest @ [typ_of_bnf bnf]);
blanchet@55904
   115
fun key_of_compose oDs Dss Ass outer inners =
blanchet@55904
   116
  key_of_types "c" (map (key_of_typess "") [[oDs], Dss, Ass, [map typ_of_bnf (outer :: inners)]]);
blanchet@55904
   117
blanchet@55904
   118
fun cache_comp_simple key cache (bnf, (unfold_set, lthy)) =
blanchet@55904
   119
  (bnf, ((Typtab.update (key, (bnf, ([], []))) cache, unfold_set), lthy));
blanchet@55904
   120
blanchet@55904
   121
fun cache_comp key (bnf_Ds_As, ((cache, unfold_set), lthy)) =
blanchet@55904
   122
  (bnf_Ds_As, ((Typtab.update (key, bnf_Ds_As) cache, unfold_set), lthy));
blanchet@55904
   123
blanchet@49502
   124
type unfold_set = {
blanchet@48975
   125
  map_unfolds: thm list,
blanchet@48975
   126
  set_unfoldss: thm list list,
traytel@51893
   127
  rel_unfolds: thm list
blanchet@48975
   128
};
blanchet@48975
   129
blanchet@55706
   130
val empty_comp_cache = Typtab.empty;
traytel@51893
   131
val empty_unfolds = {map_unfolds = [], set_unfoldss = [], rel_unfolds = []};
blanchet@48975
   132
blanchet@49503
   133
fun add_to_thms thms new = thms |> not (Thm.is_reflexive new) ? insert Thm.eq_thm new;
blanchet@49503
   134
fun adds_to_thms thms news = insert (eq_set Thm.eq_thm) (no_reflexive news) thms;
blanchet@49503
   135
traytel@51893
   136
fun add_to_unfolds map sets rel
traytel@51893
   137
  {map_unfolds, set_unfoldss, rel_unfolds} =
blanchet@49503
   138
  {map_unfolds = add_to_thms map_unfolds map,
blanchet@49503
   139
    set_unfoldss = adds_to_thms set_unfoldss sets,
traytel@51893
   140
    rel_unfolds = add_to_thms rel_unfolds rel};
blanchet@48975
   141
blanchet@49503
   142
fun add_bnf_to_unfolds bnf =
traytel@51893
   143
  add_to_unfolds (map_def_of_bnf bnf) (set_defs_of_bnf bnf) (rel_def_of_bnf bnf);
blanchet@48975
   144
blanchet@48975
   145
val bdTN = "bdT";
blanchet@48975
   146
traytel@49425
   147
fun mk_killN n = "_kill" ^ string_of_int n;
traytel@49425
   148
fun mk_liftN n = "_lift" ^ string_of_int n;
blanchet@48975
   149
fun mk_permuteN src dest =
traytel@49425
   150
  "_permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest);
blanchet@48975
   151
traytel@55935
   152
blanchet@48975
   153
(*copied from Envir.expand_term_free*)
blanchet@48975
   154
fun expand_term_const defs =
blanchet@48975
   155
  let
blanchet@48975
   156
    val eqs = map ((fn ((x, U), u) => (x, (U, u))) o apfst dest_Const) defs;
blanchet@48975
   157
    val get = fn Const (x, _) => AList.lookup (op =) eqs x | _ => NONE;
blanchet@48975
   158
  in Envir.expand_term get end;
blanchet@48975
   159
blanchet@58181
   160
val id_bnf_def = @{thm id_bnf_def};
blanchet@58181
   161
val expand_id_bnf_def = expand_term_const [Thm.prop_of id_bnf_def |> Logic.dest_equals];
traytel@55937
   162
blanchet@55851
   163
fun is_sum_prod_natLeq (Const (@{const_name csum}, _) $ t $ u) = forall is_sum_prod_natLeq [t, u]
blanchet@55851
   164
  | is_sum_prod_natLeq (Const (@{const_name cprod}, _) $ t $ u) = forall is_sum_prod_natLeq [t, u]
blanchet@55853
   165
  | is_sum_prod_natLeq t = t aconv @{term natLeq};
blanchet@55851
   166
blanchet@49502
   167
fun clean_compose_bnf const_policy qualify b outer inners (unfold_set, lthy) =
blanchet@48975
   168
  let
blanchet@48975
   169
    val olive = live_of_bnf outer;
blanchet@48975
   170
    val onwits = nwits_of_bnf outer;
blanchet@60207
   171
    val odeads = deads_of_bnf outer;
blanchet@48975
   172
    val inner = hd inners;
blanchet@48975
   173
    val ilive = live_of_bnf inner;
blanchet@60207
   174
    val ideadss = map deads_of_bnf inners;
blanchet@48975
   175
    val inwitss = map nwits_of_bnf inners;
blanchet@48975
   176
blanchet@48975
   177
    (* TODO: check olive = length inners > 0,
blanchet@48975
   178
                   forall inner from inners. ilive = live,
blanchet@48975
   179
                   forall inner from inners. idead = dead  *)
blanchet@48975
   180
blanchet@48975
   181
    val (oDs, lthy1) = apfst (map TFree)
blanchet@60207
   182
      (Variable.invent_types (map Type.sort_of_atyp odeads) lthy);
blanchet@48975
   183
    val (Dss, lthy2) = apfst (map (map TFree))
blanchet@60207
   184
      (fold_map Variable.invent_types (map (map Type.sort_of_atyp) ideadss) lthy1);
blanchet@48975
   185
    val (Ass, lthy3) = apfst (replicate ilive o map TFree)
wenzelm@56254
   186
      (Variable.invent_types (replicate ilive @{sort type}) lthy2);
blanchet@48975
   187
    val As = if ilive > 0 then hd Ass else [];
blanchet@48975
   188
    val Ass_repl = replicate olive As;
blanchet@55906
   189
    val (Bs, names_lthy) = apfst (map TFree)
wenzelm@56254
   190
      (Variable.invent_types (replicate ilive @{sort type}) lthy3);
blanchet@48975
   191
    val Bss_repl = replicate olive Bs;
blanchet@48975
   192
traytel@62324
   193
    val (((((fs', Qs'), Ps'), Asets), xs), _) = names_lthy
traytel@52923
   194
      |> apfst snd o mk_Frees' "f" (map2 (curry op -->) As Bs)
blanchet@49463
   195
      ||>> apfst snd o mk_Frees' "Q" (map2 mk_pred2T As Bs)
traytel@62324
   196
      ||>> apfst snd o mk_Frees' "P" (map mk_pred1T As)
blanchet@49456
   197
      ||>> mk_Frees "A" (map HOLogic.mk_setT As)
blanchet@48975
   198
      ||>> mk_Frees "x" As;
blanchet@48975
   199
wenzelm@58634
   200
    val CAs = @{map 3} mk_T_of_bnf Dss Ass_repl inners;
blanchet@48975
   201
    val CCA = mk_T_of_bnf oDs CAs outer;
wenzelm@58634
   202
    val CBs = @{map 3} mk_T_of_bnf Dss Bss_repl inners;
blanchet@48975
   203
    val outer_sets = mk_sets_of_bnf (replicate olive oDs) (replicate olive CAs) outer;
blanchet@61760
   204
    val inner_setss =
blanchet@61760
   205
      @{map 3} mk_sets_of_bnf (map (replicate ilive) Dss) (replicate olive Ass) inners;
wenzelm@58634
   206
    val inner_bds = @{map 3} mk_bd_of_bnf Dss Ass_repl inners;
blanchet@48975
   207
    val outer_bd = mk_bd_of_bnf oDs CAs outer;
blanchet@48975
   208
blanchet@48975
   209
    (*%f1 ... fn. outer.map (inner_1.map f1 ... fn) ... (inner_m.map f1 ... fn)*)
blanchet@49303
   210
    val mapx = fold_rev Term.abs fs'
blanchet@48975
   211
      (Term.list_comb (mk_map_of_bnf oDs CAs CBs outer,
blanchet@49463
   212
        map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o
blanchet@48975
   213
          mk_map_of_bnf Ds As Bs) Dss inners));
blanchet@49507
   214
    (*%Q1 ... Qn. outer.rel (inner_1.rel Q1 ... Qn) ... (inner_m.rel Q1 ... Qn)*)
blanchet@49507
   215
    val rel = fold_rev Term.abs Qs'
blanchet@49507
   216
      (Term.list_comb (mk_rel_of_bnf oDs CAs CBs outer,
blanchet@49463
   217
        map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o
blanchet@49507
   218
          mk_rel_of_bnf Ds As Bs) Dss inners));
traytel@62324
   219
    (*%P1 ... Pn. outer.pred (inner_1.pred P1 ... Pn) ... (inner_m.pred P1 ... Pn)*)
traytel@62324
   220
    val pred = fold_rev Term.abs Ps'
traytel@62324
   221
      (Term.list_comb (mk_pred_of_bnf oDs CAs outer,
traytel@62324
   222
        map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o
traytel@62324
   223
          mk_pred_of_bnf Ds As) Dss inners));
blanchet@48975
   224
blanchet@48975
   225
    (*Union o collect {outer.set_1 ... outer.set_m} o outer.map inner_1.set_i ... inner_m.set_i*)
blanchet@48975
   226
    (*Union o collect {image inner_1.set_i o outer.set_1 ... image inner_m.set_i o outer.set_m}*)
blanchet@49303
   227
    fun mk_set i =
blanchet@48975
   228
      let
blanchet@48975
   229
        val (setTs, T) = `(replicate olive o HOLogic.mk_setT) (nth As i);
blanchet@48975
   230
        val outer_set = mk_collect
blanchet@48975
   231
          (mk_sets_of_bnf (replicate olive oDs) (replicate olive setTs) outer)
blanchet@48975
   232
          (mk_T_of_bnf oDs setTs outer --> HOLogic.mk_setT T);
blanchet@48975
   233
        val inner_sets = map (fn sets => nth sets i) inner_setss;
blanchet@48975
   234
        val outer_map = mk_map_of_bnf oDs CAs setTs outer;
blanchet@48975
   235
        val map_inner_sets = Term.list_comb (outer_map, inner_sets);
blanchet@48975
   236
        val collect_image = mk_collect
blanchet@48975
   237
          (map2 (fn f => fn set => HOLogic.mk_comp (mk_image f, set)) inner_sets outer_sets)
blanchet@48975
   238
          (CCA --> HOLogic.mk_setT T);
blanchet@48975
   239
      in
blanchet@48975
   240
        (Library.foldl1 HOLogic.mk_comp [mk_Union T, outer_set, map_inner_sets],
blanchet@48975
   241
        HOLogic.mk_comp (mk_Union T, collect_image))
blanchet@48975
   242
      end;
blanchet@48975
   243
blanchet@49303
   244
    val (sets, sets_alt) = map_split mk_set (0 upto ilive - 1);
blanchet@48975
   245
blanchet@55906
   246
    fun mk_simplified_set set =
blanchet@55906
   247
      let
blanchet@55906
   248
        val setT = fastype_of set;
blanchet@58181
   249
        val var_set' = Const (@{const_name id_bnf}, setT --> setT) $ Var ((Name.uu, 0), setT);
blanchet@55908
   250
        val goal = mk_Trueprop_eq (var_set', set);
traytel@55930
   251
        fun tac {context = ctxt, prems = _} =
traytel@55930
   252
          mk_simplified_set_tac ctxt (collect_set_map_of_bnf outer);
blanchet@55906
   253
        val set'_eq_set =
traytel@57890
   254
          Goal.prove (*no sorry*) names_lthy [] [] goal tac
blanchet@55906
   255
          |> Thm.close_derivation;
blanchet@55906
   256
        val set' = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of set'_eq_set)));
blanchet@55906
   257
      in
blanchet@55906
   258
        (set', set'_eq_set)
blanchet@55906
   259
      end;
blanchet@55906
   260
blanchet@55906
   261
    val (sets', set'_eq_sets) =
blanchet@55906
   262
      map_split mk_simplified_set sets
blanchet@55906
   263
      ||> Proof_Context.export names_lthy lthy;
blanchet@55906
   264
blanchet@48975
   265
    (*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*)
traytel@54421
   266
    val bd = mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd;
blanchet@48975
   267
blanchet@55851
   268
    val (bd', bd_ordIso_natLeq_thm_opt) =
blanchet@55851
   269
      if is_sum_prod_natLeq bd then
blanchet@55851
   270
        let
blanchet@55851
   271
          val bd' = @{term natLeq};
blanchet@55851
   272
          val bd_bd' = HOLogic.mk_prod (bd, bd');
blanchet@55851
   273
          val ordIso = Const (@{const_name ordIso}, HOLogic.mk_setT (fastype_of bd_bd'));
desharna@57567
   274
          val goal = mk_Trueprop_mem (bd_bd', ordIso);
blanchet@55851
   275
        in
wenzelm@60757
   276
          (bd', SOME (Goal.prove_sorry lthy [] [] goal (bd_ordIso_natLeq_tac o #context)
blanchet@55851
   277
            |> Thm.close_derivation))
blanchet@55851
   278
        end
blanchet@55851
   279
      else
blanchet@55851
   280
        (bd, NONE);
blanchet@55851
   281
traytel@60728
   282
    fun map_id0_tac ctxt =
traytel@60728
   283
      mk_comp_map_id0_tac ctxt (map_id0_of_bnf outer) (map_cong0_of_bnf outer)
blanchet@53270
   284
        (map map_id0_of_bnf inners);
blanchet@48975
   285
traytel@60728
   286
    fun map_comp0_tac ctxt =
traytel@60728
   287
      mk_comp_map_comp0_tac ctxt (map_comp0_of_bnf outer) (map_cong0_of_bnf outer)
blanchet@53287
   288
        (map map_comp0_of_bnf inners);
blanchet@48975
   289
blanchet@55906
   290
    fun mk_single_set_map0_tac i ctxt =
blanchet@55906
   291
      mk_comp_set_map0_tac ctxt (nth set'_eq_sets i) (map_comp0_of_bnf outer)
blanchet@55906
   292
        (map_cong0_of_bnf outer) (collect_set_map_of_bnf outer)
blanchet@53289
   293
        (map ((fn thms => nth thms i) o set_map0_of_bnf) inners);
blanchet@48975
   294
blanchet@53289
   295
    val set_map0_tacs = map mk_single_set_map0_tac (0 upto ilive - 1);
blanchet@48975
   296
traytel@60728
   297
    fun bd_card_order_tac ctxt =
traytel@60728
   298
      mk_comp_bd_card_order_tac ctxt (map bd_card_order_of_bnf inners) (bd_card_order_of_bnf outer);
blanchet@48975
   299
traytel@60728
   300
    fun bd_cinfinite_tac ctxt =
traytel@60728
   301
      mk_comp_bd_cinfinite_tac ctxt (bd_cinfinite_of_bnf inner) (bd_cinfinite_of_bnf outer);
blanchet@48975
   302
blanchet@49303
   303
    val set_alt_thms =
wenzelm@52059
   304
      if Config.get lthy quick_and_dirty then
blanchet@49456
   305
        []
blanchet@48975
   306
      else
traytel@49109
   307
        map (fn goal =>
wenzelm@51551
   308
          Goal.prove_sorry lthy [] [] goal
traytel@49714
   309
            (fn {context = ctxt, prems = _} =>
blanchet@51766
   310
              mk_comp_set_alt_tac ctxt (collect_set_map_of_bnf outer))
traytel@49109
   311
          |> Thm.close_derivation)
blanchet@63824
   312
        (map2 (curry mk_Trueprop_eq) sets sets_alt);
blanchet@48975
   313
blanchet@55906
   314
    fun map_cong0_tac ctxt =
blanchet@55906
   315
      mk_comp_map_cong0_tac ctxt set'_eq_sets set_alt_thms (map_cong0_of_bnf outer)
blanchet@55906
   316
        (map map_cong0_of_bnf inners);
blanchet@48975
   317
blanchet@49303
   318
    val set_bd_tacs =
wenzelm@52059
   319
      if Config.get lthy quick_and_dirty then
blanchet@49669
   320
        replicate ilive (K all_tac)
blanchet@48975
   321
      else
blanchet@48975
   322
        let
blanchet@48975
   323
          val outer_set_bds = set_bd_of_bnf outer;
blanchet@48975
   324
          val inner_set_bdss = map set_bd_of_bnf inners;
blanchet@48975
   325
          val inner_bd_Card_orders = map bd_Card_order_of_bnf inners;
blanchet@49303
   326
          fun single_set_bd_thm i j =
blanchet@48975
   327
            @{thm comp_single_set_bd} OF [nth inner_bd_Card_orders j, nth (nth inner_set_bdss j) i,
blanchet@48975
   328
              nth outer_set_bds j]
blanchet@48975
   329
          val single_set_bd_thmss =
blanchet@49303
   330
            map ((fn f => map f (0 upto olive - 1)) o single_set_bd_thm) (0 upto ilive - 1);
blanchet@48975
   331
        in
wenzelm@58634
   332
          @{map 3} (fn set'_eq_set => fn set_alt => fn single_set_bds => fn ctxt =>
blanchet@55906
   333
            mk_comp_set_bd_tac ctxt set'_eq_set bd_ordIso_natLeq_thm_opt set_alt single_set_bds)
blanchet@55906
   334
          set'_eq_sets set_alt_thms single_set_bd_thmss
blanchet@48975
   335
        end;
blanchet@48975
   336
blanchet@49303
   337
    val in_alt_thm =
traytel@49155
   338
      let
blanchet@49303
   339
        val inx = mk_in Asets sets CCA;
blanchet@49303
   340
        val in_alt = mk_in (map2 (mk_in Asets) inner_setss CAs) outer_sets CCA;
blanchet@49303
   341
        val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
traytel@49155
   342
      in
wenzelm@51551
   343
        Goal.prove_sorry lthy [] [] goal
traytel@49714
   344
          (fn {context = ctxt, prems = _} => mk_comp_in_alt_tac ctxt set_alt_thms)
traytel@49155
   345
        |> Thm.close_derivation
traytel@49155
   346
      end;
blanchet@48975
   347
traytel@60728
   348
    fun le_rel_OO_tac ctxt = mk_le_rel_OO_tac ctxt (le_rel_OO_of_bnf outer) (rel_mono_of_bnf outer)
traytel@54841
   349
      (map le_rel_OO_of_bnf inners);
blanchet@48975
   350
blanchet@55906
   351
    fun rel_OO_Grp_tac ctxt =
blanchet@49456
   352
      let
traytel@51893
   353
        val outer_rel_Grp = rel_Grp_of_bnf outer RS sym;
blanchet@49463
   354
        val thm =
traytel@62324
   355
          trans OF [in_alt_thm RS @{thm OO_Grp_cong},
traytel@51893
   356
             trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF
traytel@51893
   357
               [trans OF [outer_rel_Grp RS @{thm arg_cong[of _ _ conversep]},
traytel@51893
   358
                 rel_conversep_of_bnf outer RS sym], outer_rel_Grp],
traytel@61242
   359
               trans OF [rel_OO_of_bnf outer RS sym, rel_cong0_of_bnf outer OF
traytel@62324
   360
                 (map (fn bnf => rel_OO_Grp_of_bnf bnf RS sym) inners)]]] RS sym;
blanchet@49456
   361
      in
traytel@60728
   362
        unfold_thms_tac ctxt set'_eq_sets THEN rtac ctxt thm 1
blanchet@49463
   363
      end;
blanchet@49456
   364
traytel@62324
   365
    fun pred_set_tac ctxt =
traytel@62324
   366
      let
traytel@62324
   367
        val pred_alt = unfold_thms ctxt @{thms Ball_Collect}
traytel@62324
   368
          (trans OF [pred_cong0_of_bnf outer OF map pred_set_of_bnf inners, pred_set_of_bnf outer]);
traytel@62324
   369
        val in_alt = in_alt_thm RS @{thm Collect_inj} RS sym;
traytel@62324
   370
      in
traytel@62324
   371
        unfold_thms_tac ctxt (@{thm Ball_Collect} :: set'_eq_sets) THEN
traytel@62324
   372
        HEADGOAL (rtac ctxt (trans OF [pred_alt, in_alt]))
traytel@62324
   373
      end
traytel@62324
   374
blanchet@53289
   375
    val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac
traytel@62324
   376
      bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac pred_set_tac;
blanchet@48975
   377
blanchet@48975
   378
    val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
blanchet@48975
   379
blanchet@48975
   380
    val inner_witss = map (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)))
wenzelm@58634
   381
      (@{map 3} (fn Ds => fn n => mk_wits_of_bnf (replicate n Ds) (replicate n As))
blanchet@48975
   382
        Dss inwitss inners);
blanchet@48975
   383
blanchet@48975
   384
    val inner_witsss = map (map (nth inner_witss) o fst) outer_wits;
blanchet@48975
   385
blanchet@49303
   386
    val wits = (inner_witsss, (map (single o snd) outer_wits))
blanchet@48975
   387
      |-> map2 (fold (map_product (fn iwit => fn owit => owit $ iwit)))
blanchet@48975
   388
      |> flat
blanchet@48975
   389
      |> map (`(fn t => Term.add_frees t []))
blanchet@48975
   390
      |> minimize_wits
blanchet@48975
   391
      |> map (fn (frees, t) => fold absfree frees t);
blanchet@48975
   392
traytel@55197
   393
    fun wit_tac ctxt =
blanchet@55906
   394
      mk_comp_wit_tac ctxt set'_eq_sets (wit_thms_of_bnf outer) (collect_set_map_of_bnf outer)
blanchet@48975
   395
        (maps wit_thms_of_bnf inners);
blanchet@48975
   396
blanchet@48975
   397
    val (bnf', lthy') =
traytel@56016
   398
      bnf_def const_policy (K Dont_Note) true qualify tacs wit_tac (SOME (oDs @ flat Dss))
traytel@62324
   399
        Binding.empty Binding.empty Binding.empty []
traytel@62324
   400
        (((((((b, CCA), mapx), sets'), bd'), wits), SOME rel), SOME pred) lthy;
blanchet@55906
   401
blanchet@55906
   402
    val phi =
blanchet@58181
   403
      Morphism.thm_morphism "BNF" (unfold_thms lthy' [id_bnf_def])
blanchet@58181
   404
      $> Morphism.term_morphism "BNF" expand_id_bnf_def;
blanchet@55906
   405
blanchet@55906
   406
    val bnf'' = morph_bnf phi bnf';
blanchet@48975
   407
  in
blanchet@55906
   408
    (bnf'', (add_bnf_to_unfolds bnf'' unfold_set, lthy'))
blanchet@48975
   409
  end;
blanchet@48975
   410
blanchet@48975
   411
(* Killing live variables *)
blanchet@48975
   412
blanchet@55904
   413
fun raw_kill_bnf qualify n bnf (accum as (unfold_set, lthy)) =
blanchet@55904
   414
  if n = 0 then (bnf, accum) else
blanchet@48975
   415
  let
traytel@49425
   416
    val b = Binding.suffix_name (mk_killN n) (name_of_bnf bnf);
blanchet@48975
   417
    val live = live_of_bnf bnf;
blanchet@60207
   418
    val deads = deads_of_bnf bnf;
blanchet@48975
   419
    val nwits = nwits_of_bnf bnf;
blanchet@48975
   420
blanchet@48975
   421
    (* TODO: check 0 < n <= live *)
blanchet@48975
   422
blanchet@48975
   423
    val (Ds, lthy1) = apfst (map TFree)
blanchet@60207
   424
      (Variable.invent_types (map Type.sort_of_atyp deads) lthy);
blanchet@48975
   425
    val ((killedAs, As), lthy2) = apfst (`(take n) o map TFree)
wenzelm@56254
   426
      (Variable.invent_types (replicate live @{sort type}) lthy1);
blanchet@48975
   427
    val (Bs, _(*lthy3*)) = apfst (append killedAs o map TFree)
wenzelm@56254
   428
      (Variable.invent_types (replicate (live - n) @{sort type}) lthy2);
blanchet@48975
   429
blanchet@48975
   430
    val ((Asets, lives), _(*names_lthy*)) = lthy
blanchet@49456
   431
      |> mk_Frees "A" (map HOLogic.mk_setT (drop n As))
blanchet@48975
   432
      ||>> mk_Frees "x" (drop n As);
blanchet@62316
   433
    val xs = map (fn T => Const (@{const_name undefined}, T)) killedAs @ lives;
blanchet@48975
   434
blanchet@48975
   435
    val T = mk_T_of_bnf Ds As bnf;
blanchet@48975
   436
blanchet@48975
   437
    (*bnf.map id ... id*)
blanchet@49303
   438
    val mapx = Term.list_comb (mk_map_of_bnf Ds As Bs bnf, map HOLogic.id_const killedAs);
blanchet@49507
   439
    (*bnf.rel (op =) ... (op =)*)
blanchet@49507
   440
    val rel = Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, map HOLogic.eq_const killedAs);
traytel@62324
   441
    (*bnf.pred (%_. True) ... (%_ True)*)
traytel@62324
   442
    val pred = Term.list_comb (mk_pred_of_bnf Ds As bnf,
traytel@62324
   443
      map (fn T => Term.absdummy T @{term True}) killedAs);
blanchet@48975
   444
blanchet@48975
   445
    val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
blanchet@49303
   446
    val sets = drop n bnf_sets;
blanchet@48975
   447
traytel@55707
   448
    val bd = mk_bd_of_bnf Ds As bnf;
blanchet@48975
   449
traytel@60728
   450
    fun map_id0_tac ctxt = rtac ctxt (map_id0_of_bnf bnf) 1;
traytel@55197
   451
    fun map_comp0_tac ctxt =
blanchet@55067
   452
      unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) ::
traytel@60728
   453
        @{thms comp_assoc id_comp comp_id}) THEN rtac ctxt refl 1;
traytel@55197
   454
    fun map_cong0_tac ctxt =
blanchet@51761
   455
      mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf);
traytel@60728
   456
    val set_map0_tacs = map (fn thm => fn ctxt => rtac ctxt thm 1) (drop n (set_map0_of_bnf bnf));
traytel@60728
   457
    fun bd_card_order_tac ctxt = rtac ctxt (bd_card_order_of_bnf bnf) 1;
traytel@60728
   458
    fun bd_cinfinite_tac ctxt = rtac ctxt (bd_cinfinite_of_bnf bnf) 1;
traytel@60728
   459
    val set_bd_tacs = map (fn thm => fn ctxt => rtac ctxt thm 1) (drop n (set_bd_of_bnf bnf));
blanchet@48975
   460
blanchet@49303
   461
    val in_alt_thm =
traytel@49155
   462
      let
blanchet@49303
   463
        val inx = mk_in Asets sets T;
blanchet@49303
   464
        val in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T;
blanchet@49303
   465
        val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
traytel@49155
   466
      in
traytel@60728
   467
        Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
traytel@60728
   468
          kill_in_alt_tac ctxt) |> Thm.close_derivation
traytel@49155
   469
      end;
blanchet@48975
   470
traytel@55197
   471
    fun le_rel_OO_tac ctxt =
traytel@60728
   472
      EVERY' [rtac ctxt @{thm ord_le_eq_trans}, rtac ctxt (le_rel_OO_of_bnf bnf)] 1 THEN
traytel@60728
   473
      unfold_thms_tac ctxt @{thms eq_OO} THEN rtac ctxt refl 1;
blanchet@48975
   474
traytel@60728
   475
    fun rel_OO_Grp_tac ctxt =
blanchet@49456
   476
      let
traytel@51893
   477
        val rel_Grp = rel_Grp_of_bnf bnf RS sym
blanchet@49463
   478
        val thm =
traytel@51893
   479
          (trans OF [in_alt_thm RS @{thm OO_Grp_cong},
traytel@51893
   480
            trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF
traytel@51893
   481
              [trans OF [rel_Grp RS @{thm arg_cong[of _ _ conversep]},
traytel@51893
   482
                rel_conversep_of_bnf bnf RS sym], rel_Grp],
traytel@61242
   483
              trans OF [rel_OO_of_bnf bnf RS sym, rel_cong0_of_bnf bnf OF
traytel@51893
   484
                (replicate n @{thm trans[OF Grp_UNIV_id[OF refl] eq_alt[symmetric]]} @
traytel@52660
   485
                 replicate (live - n) @{thm Grp_fst_snd})]]] RS sym);
blanchet@49456
   486
      in
traytel@60728
   487
        rtac ctxt thm 1
blanchet@49456
   488
      end;
blanchet@49456
   489
traytel@62324
   490
    fun pred_set_tac ctxt = mk_simple_pred_set_tac ctxt (pred_set_of_bnf bnf) in_alt_thm;
traytel@62324
   491
blanchet@53289
   492
    val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac
traytel@62324
   493
      bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac pred_set_tac;
blanchet@48975
   494
blanchet@49303
   495
    val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
blanchet@48975
   496
blanchet@49303
   497
    val wits = map (fn t => fold absfree (Term.add_frees t []) t)
blanchet@49303
   498
      (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)) bnf_wits);
blanchet@48975
   499
wenzelm@60752
   500
    fun wit_tac ctxt = mk_simple_wit_tac ctxt (wit_thms_of_bnf bnf);
blanchet@48975
   501
blanchet@48975
   502
    val (bnf', lthy') =
traytel@58297
   503
      bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME (Ds @ killedAs))
traytel@62324
   504
        Binding.empty Binding.empty Binding.empty []
traytel@62324
   505
        (((((((b, T), mapx), sets), bd), wits), SOME rel), SOME pred) lthy;
blanchet@48975
   506
  in
blanchet@49503
   507
    (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
blanchet@48975
   508
  end;
blanchet@48975
   509
blanchet@55904
   510
fun kill_bnf qualify n bnf (accum as ((cache, unfold_set), lthy)) =
blanchet@55904
   511
  let val key = key_of_kill n bnf in
blanchet@55904
   512
    (case Typtab.lookup cache key of
blanchet@55904
   513
      SOME (bnf, _) => (bnf, accum)
blanchet@55904
   514
    | NONE => cache_comp_simple key cache (raw_kill_bnf qualify n bnf (unfold_set, lthy)))
blanchet@55904
   515
  end;
blanchet@55904
   516
blanchet@48975
   517
(* Adding dummy live variables *)
blanchet@48975
   518
blanchet@55904
   519
fun raw_lift_bnf qualify n bnf (accum as (unfold_set, lthy)) =
blanchet@55904
   520
  if n = 0 then (bnf, accum) else
blanchet@48975
   521
  let
traytel@49425
   522
    val b = Binding.suffix_name (mk_liftN n) (name_of_bnf bnf);
blanchet@48975
   523
    val live = live_of_bnf bnf;
blanchet@60207
   524
    val deads = deads_of_bnf bnf;
blanchet@48975
   525
    val nwits = nwits_of_bnf bnf;
blanchet@48975
   526
blanchet@48975
   527
    (* TODO: check 0 < n *)
blanchet@48975
   528
blanchet@48975
   529
    val (Ds, lthy1) = apfst (map TFree)
blanchet@60207
   530
      (Variable.invent_types (map Type.sort_of_atyp deads) lthy);
blanchet@48975
   531
    val ((newAs, As), lthy2) = apfst (chop n o map TFree)
wenzelm@56254
   532
      (Variable.invent_types (replicate (n + live) @{sort type}) lthy1);
blanchet@48975
   533
    val ((newBs, Bs), _(*lthy3*)) = apfst (chop n o map TFree)
wenzelm@56254
   534
      (Variable.invent_types (replicate (n + live) @{sort type}) lthy2);
blanchet@48975
   535
blanchet@48975
   536
    val (Asets, _(*names_lthy*)) = lthy
blanchet@49456
   537
      |> mk_Frees "A" (map HOLogic.mk_setT (newAs @ As));
blanchet@48975
   538
blanchet@48975
   539
    val T = mk_T_of_bnf Ds As bnf;
blanchet@48975
   540
blanchet@48975
   541
    (*%f1 ... fn. bnf.map*)
blanchet@49303
   542
    val mapx =
traytel@52923
   543
      fold_rev Term.absdummy (map2 (curry op -->) newAs newBs) (mk_map_of_bnf Ds As Bs bnf);
blanchet@49507
   544
    (*%Q1 ... Qn. bnf.rel*)
blanchet@49507
   545
    val rel = fold_rev Term.absdummy (map2 mk_pred2T newAs newBs) (mk_rel_of_bnf Ds As Bs bnf);
traytel@62324
   546
    (*%P1 ... Pn. bnf.pred*)
traytel@62324
   547
    val pred = fold_rev Term.absdummy (map mk_pred1T newAs) (mk_pred_of_bnf Ds As bnf);
blanchet@48975
   548
blanchet@48975
   549
    val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
blanchet@49303
   550
    val sets = map (fn A => absdummy T (HOLogic.mk_set A [])) newAs @ bnf_sets;
blanchet@48975
   551
blanchet@49303
   552
    val bd = mk_bd_of_bnf Ds As bnf;
blanchet@48975
   553
traytel@60728
   554
    fun map_id0_tac ctxt = rtac ctxt (map_id0_of_bnf bnf) 1;
traytel@55197
   555
    fun map_comp0_tac ctxt =
blanchet@55067
   556
      unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) ::
traytel@60728
   557
        @{thms comp_assoc id_comp comp_id}) THEN rtac ctxt refl 1;
traytel@55197
   558
    fun map_cong0_tac ctxt =
traytel@60728
   559
      rtac ctxt (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
blanchet@53289
   560
    val set_map0_tacs =
wenzelm@52059
   561
      if Config.get lthy quick_and_dirty then
blanchet@48975
   562
        replicate (n + live) (K all_tac)
blanchet@48975
   563
      else
traytel@60728
   564
        replicate n empty_natural_tac @
traytel@60728
   565
        map (fn thm => fn ctxt => rtac ctxt thm 1) (set_map0_of_bnf bnf);
traytel@60728
   566
    fun bd_card_order_tac ctxt = rtac ctxt (bd_card_order_of_bnf bnf) 1;
traytel@60728
   567
    fun bd_cinfinite_tac ctxt = rtac ctxt (bd_cinfinite_of_bnf bnf) 1;
blanchet@49303
   568
    val set_bd_tacs =
wenzelm@52059
   569
      if Config.get lthy quick_and_dirty then
blanchet@48975
   570
        replicate (n + live) (K all_tac)
blanchet@48975
   571
      else
traytel@60728
   572
        replicate n (fn ctxt => mk_lift_set_bd_tac ctxt (bd_Card_order_of_bnf bnf)) @
traytel@60728
   573
        (map (fn thm => fn ctxt => rtac ctxt thm 1) (set_bd_of_bnf bnf));
blanchet@48975
   574
blanchet@49303
   575
    val in_alt_thm =
traytel@49155
   576
      let
blanchet@49303
   577
        val inx = mk_in Asets sets T;
blanchet@49303
   578
        val in_alt = mk_in (drop n Asets) bnf_sets T;
blanchet@49303
   579
        val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
traytel@49155
   580
      in
traytel@60728
   581
        Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => lift_in_alt_tac ctxt)
traytel@60728
   582
        |> Thm.close_derivation
traytel@49155
   583
      end;
blanchet@48975
   584
traytel@60728
   585
    fun le_rel_OO_tac ctxt = rtac ctxt (le_rel_OO_of_bnf bnf) 1;
blanchet@48975
   586
traytel@60728
   587
    fun rel_OO_Grp_tac ctxt = mk_simple_rel_OO_Grp_tac ctxt (rel_OO_Grp_of_bnf bnf) in_alt_thm;
blanchet@49456
   588
traytel@62324
   589
    fun pred_set_tac ctxt = mk_simple_pred_set_tac ctxt (pred_set_of_bnf bnf) in_alt_thm;
traytel@62324
   590
blanchet@53289
   591
    val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac
traytel@62324
   592
      bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac pred_set_tac;
blanchet@48975
   593
blanchet@49303
   594
    val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
blanchet@48975
   595
wenzelm@60752
   596
    fun wit_tac ctxt = mk_simple_wit_tac ctxt (wit_thms_of_bnf bnf);
blanchet@48975
   597
blanchet@48975
   598
    val (bnf', lthy') =
traytel@56016
   599
      bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME Ds) Binding.empty
traytel@62324
   600
        Binding.empty Binding.empty []
traytel@62324
   601
        (((((((b, T), mapx), sets), bd), wits), SOME rel), SOME pred) lthy;
blanchet@48975
   602
  in
blanchet@49503
   603
    (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
blanchet@48975
   604
  end;
blanchet@48975
   605
blanchet@55904
   606
fun lift_bnf qualify n bnf (accum as ((cache, unfold_set), lthy)) =
blanchet@55904
   607
  let val key = key_of_lift n bnf in
blanchet@55904
   608
    (case Typtab.lookup cache key of
blanchet@55904
   609
      SOME (bnf, _) => (bnf, accum)
blanchet@55904
   610
    | NONE => cache_comp_simple key cache (raw_lift_bnf qualify n bnf (unfold_set, lthy)))
blanchet@55904
   611
  end;
blanchet@55904
   612
blanchet@48975
   613
(* Changing the order of live variables *)
blanchet@48975
   614
blanchet@55904
   615
fun raw_permute_bnf qualify src dest bnf (accum as (unfold_set, lthy)) =
blanchet@55904
   616
  if src = dest then (bnf, accum) else
blanchet@48975
   617
  let
traytel@49425
   618
    val b = Binding.suffix_name (mk_permuteN src dest) (name_of_bnf bnf);
blanchet@48975
   619
    val live = live_of_bnf bnf;
blanchet@60207
   620
    val deads = deads_of_bnf bnf;
blanchet@48975
   621
    val nwits = nwits_of_bnf bnf;
blanchet@55480
   622
blanchet@55480
   623
    fun permute xs = permute_like_unique (op =) src dest xs;
blanchet@55480
   624
    fun unpermute xs = permute_like_unique (op =) dest src xs;
blanchet@48975
   625
blanchet@48975
   626
    val (Ds, lthy1) = apfst (map TFree)
blanchet@60207
   627
      (Variable.invent_types (map Type.sort_of_atyp deads) lthy);
blanchet@48975
   628
    val (As, lthy2) = apfst (map TFree)
wenzelm@56254
   629
      (Variable.invent_types (replicate live @{sort type}) lthy1);
blanchet@48975
   630
    val (Bs, _(*lthy3*)) = apfst (map TFree)
wenzelm@56254
   631
      (Variable.invent_types (replicate live @{sort type}) lthy2);
blanchet@48975
   632
blanchet@48975
   633
    val (Asets, _(*names_lthy*)) = lthy
blanchet@49456
   634
      |> mk_Frees "A" (map HOLogic.mk_setT (permute As));
blanchet@48975
   635
blanchet@48975
   636
    val T = mk_T_of_bnf Ds As bnf;
blanchet@48975
   637
blanchet@48975
   638
    (*%f(1) ... f(n). bnf.map f\<sigma>(1) ... f\<sigma>(n)*)
blanchet@49303
   639
    val mapx = fold_rev Term.absdummy (permute (map2 (curry op -->) As Bs))
blanchet@53038
   640
      (Term.list_comb (mk_map_of_bnf Ds As Bs bnf, unpermute (map Bound (live - 1 downto 0))));
blanchet@49507
   641
    (*%Q(1) ... Q(n). bnf.rel Q\<sigma>(1) ... Q\<sigma>(n)*)
blanchet@49507
   642
    val rel = fold_rev Term.absdummy (permute (map2 mk_pred2T As Bs))
blanchet@53038
   643
      (Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, unpermute (map Bound (live - 1 downto 0))));
traytel@62324
   644
    (*%P(1) ... P(n). bnf.pred P\<sigma>(1) ... P\<sigma>(n)*)
traytel@62324
   645
    val pred = fold_rev Term.absdummy (permute (map mk_pred1T As))
traytel@62324
   646
      (Term.list_comb (mk_pred_of_bnf Ds As bnf, unpermute (map Bound (live - 1 downto 0))));
blanchet@48975
   647
blanchet@48975
   648
    val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
blanchet@49303
   649
    val sets = permute bnf_sets;
blanchet@48975
   650
blanchet@49303
   651
    val bd = mk_bd_of_bnf Ds As bnf;
blanchet@48975
   652
traytel@60728
   653
    fun map_id0_tac ctxt = rtac ctxt (map_id0_of_bnf bnf) 1;
traytel@60728
   654
    fun map_comp0_tac ctxt = rtac ctxt (map_comp0_of_bnf bnf) 1;
traytel@55197
   655
    fun map_cong0_tac ctxt =
traytel@60728
   656
      rtac ctxt (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
traytel@60728
   657
    val set_map0_tacs = permute (map (fn thm => fn ctxt => rtac ctxt thm 1) (set_map0_of_bnf bnf));
traytel@60728
   658
    fun bd_card_order_tac ctxt = rtac ctxt (bd_card_order_of_bnf bnf) 1;
traytel@60728
   659
    fun bd_cinfinite_tac ctxt = rtac ctxt (bd_cinfinite_of_bnf bnf) 1;
traytel@60728
   660
    val set_bd_tacs = permute (map (fn thm => fn ctxt => rtac ctxt thm 1) (set_bd_of_bnf bnf));
blanchet@48975
   661
blanchet@49303
   662
    val in_alt_thm =
traytel@49155
   663
      let
blanchet@49303
   664
        val inx = mk_in Asets sets T;
blanchet@53038
   665
        val in_alt = mk_in (unpermute Asets) bnf_sets T;
blanchet@49303
   666
        val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
traytel@49155
   667
      in
traytel@60728
   668
        Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
traytel@60728
   669
          mk_permute_in_alt_tac ctxt src dest)
traytel@49155
   670
        |> Thm.close_derivation
traytel@49155
   671
      end;
blanchet@48975
   672
traytel@60728
   673
    fun le_rel_OO_tac ctxt = rtac ctxt (le_rel_OO_of_bnf bnf) 1;
blanchet@48975
   674
traytel@60728
   675
    fun rel_OO_Grp_tac ctxt = mk_simple_rel_OO_Grp_tac ctxt (rel_OO_Grp_of_bnf bnf) in_alt_thm;
blanchet@49456
   676
traytel@62324
   677
    fun pred_set_tac ctxt = mk_simple_pred_set_tac ctxt (pred_set_of_bnf bnf) in_alt_thm;
traytel@62324
   678
blanchet@53289
   679
    val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac
traytel@62324
   680
      bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac pred_set_tac;
blanchet@48975
   681
blanchet@49303
   682
    val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
blanchet@48975
   683
wenzelm@60752
   684
    fun wit_tac ctxt = mk_simple_wit_tac ctxt (wit_thms_of_bnf bnf);
blanchet@48975
   685
blanchet@48975
   686
    val (bnf', lthy') =
traytel@56016
   687
      bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME Ds) Binding.empty
traytel@62324
   688
        Binding.empty Binding.empty []
traytel@62324
   689
        (((((((b, T), mapx), sets), bd), wits), SOME rel), SOME pred) lthy;
blanchet@48975
   690
  in
blanchet@49503
   691
    (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
blanchet@48975
   692
  end;
blanchet@48975
   693
blanchet@55904
   694
fun permute_bnf qualify src dest bnf (accum as ((cache, unfold_set), lthy)) =
blanchet@55904
   695
  let val key = key_of_permute src dest bnf in
blanchet@55904
   696
    (case Typtab.lookup cache key of
blanchet@55904
   697
      SOME (bnf, _) => (bnf, accum)
blanchet@55904
   698
    | NONE => cache_comp_simple key cache (raw_permute_bnf qualify src dest bnf (unfold_set, lthy)))
blanchet@55904
   699
  end;
blanchet@55904
   700
blanchet@49014
   701
(* Composition pipeline *)
blanchet@49014
   702
blanchet@59725
   703
fun permute_and_kill_bnf qualify n src dest bnf =
blanchet@55703
   704
  permute_bnf qualify src dest bnf
blanchet@49304
   705
  #> uncurry (kill_bnf qualify n);
blanchet@49014
   706
blanchet@59725
   707
fun lift_and_permute_bnf qualify n src dest bnf =
blanchet@55703
   708
  lift_bnf qualify n bnf
blanchet@49014
   709
  #> uncurry (permute_bnf qualify src dest);
blanchet@49014
   710
blanchet@58332
   711
fun normalize_bnfs qualify Ass Ds flatten_tyargs bnfs accum =
blanchet@49014
   712
  let
blanchet@49014
   713
    val before_kill_src = map (fn As => 0 upto (length As - 1)) Ass;
traytel@52985
   714
    val kill_poss = map (find_indices op = Ds) Ass;
traytel@52985
   715
    val live_poss = map2 (subtract op =) kill_poss before_kill_src;
blanchet@49014
   716
    val before_kill_dest = map2 append kill_poss live_poss;
blanchet@49014
   717
    val kill_ns = map length kill_poss;
blanchet@55904
   718
    val (inners', accum') =
blanchet@59725
   719
      @{fold_map 5} (permute_and_kill_bnf o qualify)
blanchet@59725
   720
        (if length bnfs = 1 then [0] else 1 upto length bnfs)
blanchet@55904
   721
        kill_ns before_kill_src before_kill_dest bnfs accum;
blanchet@49014
   722
blanchet@49014
   723
    val Ass' = map2 (map o nth) Ass live_poss;
blanchet@58332
   724
    val As = flatten_tyargs Ass';
blanchet@49014
   725
    val after_lift_dest = replicate (length Ass') (0 upto (length As - 1));
blanchet@49014
   726
    val old_poss = map (map (fn x => find_index (fn y => x = y) As)) Ass';
traytel@52985
   727
    val new_poss = map2 (subtract op =) old_poss after_lift_dest;
blanchet@49014
   728
    val after_lift_src = map2 append new_poss old_poss;
blanchet@49014
   729
    val lift_ns = map (fn xs => length As - length xs) Ass';
blanchet@49014
   730
  in
blanchet@59725
   731
    ((kill_poss, As), @{fold_map 5} (lift_and_permute_bnf o qualify)
blanchet@55703
   732
      (if length bnfs = 1 then [0] else 1 upto length bnfs)
blanchet@55904
   733
      lift_ns after_lift_src after_lift_dest inners' accum')
blanchet@49014
   734
  end;
blanchet@49014
   735
blanchet@49014
   736
fun default_comp_sort Ass =
wenzelm@59058
   737
  Library.sort (Term_Ord.typ_ord o apply2 TFree) (fold (fold (insert (op =))) Ass []);
blanchet@49014
   738
blanchet@58332
   739
fun raw_compose_bnf const_policy qualify flatten_tyargs outer inners oDs Dss tfreess accum =
blanchet@49014
   740
  let
traytel@49425
   741
    val b = name_of_bnf outer;
blanchet@49014
   742
blanchet@49121
   743
    val Ass = map (map Term.dest_TFree) tfreess;
blanchet@49014
   744
    val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) [];
blanchet@49014
   745
blanchet@55904
   746
    val ((kill_poss, As), (inners', ((cache', unfold_set'), lthy'))) =
blanchet@58332
   747
      normalize_bnfs qualify Ass Ds flatten_tyargs inners accum;
blanchet@49014
   748
blanchet@61760
   749
    val Ds =
blanchet@61760
   750
      oDs @ flat (@{map 3} (uncurry append oo curry swap oo map o nth) tfreess kill_poss Dss);
blanchet@49014
   751
    val As = map TFree As;
blanchet@49014
   752
  in
traytel@49425
   753
    apfst (rpair (Ds, As))
blanchet@55904
   754
      (apsnd (apfst (pair cache'))
blanchet@55904
   755
        (clean_compose_bnf const_policy (qualify 0) b outer inners' (unfold_set', lthy')))
blanchet@55904
   756
  end;
blanchet@55904
   757
blanchet@58332
   758
fun compose_bnf const_policy qualify flatten_tyargs outer inners oDs Dss tfreess
blanchet@58332
   759
    (accum as ((cache, _), _)) =
blanchet@55904
   760
  let val key = key_of_compose oDs Dss tfreess outer inners in
blanchet@55904
   761
    (case Typtab.lookup cache key of
blanchet@55904
   762
      SOME bnf_Ds_As => (bnf_Ds_As, accum)
blanchet@55904
   763
    | NONE =>
blanchet@58332
   764
      cache_comp key
blanchet@58332
   765
        (raw_compose_bnf const_policy qualify flatten_tyargs outer inners oDs Dss tfreess accum))
blanchet@49014
   766
  end;
blanchet@49014
   767
blanchet@48975
   768
(* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *)
blanchet@48975
   769
traytel@55803
   770
type absT_info =
traytel@55803
   771
  {absT: typ,
traytel@55803
   772
   repT: typ,
traytel@55803
   773
   abs: term,
traytel@55803
   774
   rep: term,
traytel@55803
   775
   abs_inject: thm,
traytel@55803
   776
   abs_inverse: thm,
traytel@55803
   777
   type_definition: thm};
traytel@55803
   778
traytel@55803
   779
fun morph_absT_info phi
traytel@55803
   780
  {absT, repT, abs, rep, abs_inject, abs_inverse, type_definition} =
traytel@55803
   781
  {absT = Morphism.typ phi absT,
traytel@55803
   782
   repT = Morphism.typ phi repT,
traytel@55803
   783
   abs = Morphism.term phi abs,
traytel@55803
   784
   rep = Morphism.term phi rep,
traytel@55803
   785
   abs_inject = Morphism.thm phi abs_inject,
traytel@55803
   786
   abs_inverse = Morphism.thm phi abs_inverse,
traytel@55803
   787
   type_definition = Morphism.thm phi type_definition};
traytel@55803
   788
traytel@55803
   789
fun mk_absT thy repT absT repU =
traytel@55900
   790
  let
blanchet@56634
   791
    val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (repT, repU) Vartab.empty) [];
traytel@55900
   792
  in Term.typ_subst_TVars rho absT end
traytel@55900
   793
  handle Type.TYPE_MATCH => raise Term.TYPE ("mk_absT", [repT, absT, repU], []);
traytel@55803
   794
blanchet@55854
   795
fun mk_repT absT repT absU =
blanchet@55854
   796
  if absT = repT then absU
blanchet@55854
   797
  else
blanchet@55854
   798
    (case (absT, absU) of
blanchet@55854
   799
      (Type (C, Ts), Type (C', Us)) =>
blanchet@55854
   800
        if C = C' then Term.typ_subst_atomic (Ts ~~ Us) repT
traytel@62684
   801
        else raise Term.TYPE ("mk_repT", [absT, repT, absU], [])
traytel@62684
   802
    | _ => raise Term.TYPE ("mk_repT", [absT, repT, absU], []));
traytel@55803
   803
blanchet@58181
   804
fun mk_abs_or_rep _ absU (Const (@{const_name id_bnf}, _)) =
blanchet@58181
   805
    Const (@{const_name id_bnf}, absU --> absU)
blanchet@55854
   806
  | mk_abs_or_rep getT (Type (_, Us)) abs =
blanchet@55854
   807
    let val Ts = snd (dest_Type (getT (fastype_of abs)))
blanchet@55854
   808
    in Term.subst_atomic_types (Ts ~~ Us) abs end;
traytel@55803
   809
traytel@55803
   810
val mk_abs = mk_abs_or_rep range_type;
traytel@55803
   811
val mk_rep = mk_abs_or_rep domain_type;
traytel@55803
   812
blanchet@63802
   813
fun maybe_typedef force_out_of_line (b, As, mx) set opt_morphs tac lthy =
blanchet@55854
   814
  let
blanchet@63802
   815
    val threshold = Config.get lthy typedef_threshold;
blanchet@55854
   816
    val repT = HOLogic.dest_setT (fastype_of set);
blanchet@59710
   817
    val out_of_line = force_out_of_line orelse
blanchet@59994
   818
      (threshold >= 0 andalso Term.size_of_typ repT >= threshold);
blanchet@55854
   819
  in
blanchet@58332
   820
    if out_of_line then
blanchet@63802
   821
      typedef (b, As, mx) set opt_morphs tac lthy
blanchet@63802
   822
      |>> (fn (T_name, ({Rep_name, Abs_name, ...},
blanchet@58332
   823
          {type_definition, Abs_inverse, Abs_inject, Abs_cases, ...}) : Typedef.info) =>
blanchet@58332
   824
        (Type (T_name, map TFree As),
blanchet@58332
   825
          (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, Abs_cases)))
blanchet@58332
   826
    else
blanchet@63802
   827
      ((repT,
blanchet@58181
   828
        (@{const_name id_bnf}, @{const_name id_bnf},
blanchet@58181
   829
         @{thm type_definition_id_bnf_UNIV},
blanchet@58181
   830
         @{thm type_definition.Abs_inverse[OF type_definition_id_bnf_UNIV]},
blanchet@58181
   831
         @{thm type_definition.Abs_inject[OF type_definition_id_bnf_UNIV]},
blanchet@63802
   832
         @{thm type_definition.Abs_cases[OF type_definition_id_bnf_UNIV]})), lthy)
blanchet@55854
   833
  end;
blanchet@55854
   834
blanchet@63837
   835
fun seal_bnf qualify (unfold_set : unfold_set) b force_out_of_line Ds all_Ds bnf lthy =
blanchet@48975
   836
  let
blanchet@48975
   837
    val live = live_of_bnf bnf;
blanchet@48975
   838
    val nwits = nwits_of_bnf bnf;
blanchet@48975
   839
blanchet@58332
   840
    val ((As, As'), lthy1) = apfst (`(map TFree))
blanchet@63837
   841
      (Variable.invent_types (replicate live @{sort type}) (fold Variable.declare_typ all_Ds lthy));
blanchet@58332
   842
    val (Bs, _) = apfst (map TFree) (Variable.invent_types (replicate live @{sort type}) lthy1);
blanchet@48975
   843
traytel@62324
   844
    val ((((fs, fs'), (Rs, Rs')), (Ps, Ps')), _(*names_lthy*)) = lthy
traytel@55803
   845
      |> mk_Frees' "f" (map2 (curry op -->) As Bs)
traytel@62324
   846
      ||>> mk_Frees' "R" (map2 mk_pred2T As Bs)
traytel@62324
   847
      ||>> mk_Frees' "P" (map mk_pred1T As);
traytel@55803
   848
traytel@55803
   849
    val repTA = mk_T_of_bnf Ds As bnf;
traytel@55803
   850
    val T_bind = qualify b;
blanchet@63836
   851
    val repTA_tfrees = Term.add_tfreesT repTA [];
blanchet@63837
   852
    val all_TA_params_in_order = fold_rev Term.add_tfreesT all_Ds As';
blanchet@59821
   853
    val TA_params =
blanchet@63802
   854
      (if force_out_of_line then all_TA_params_in_order
blanchet@63836
   855
       else inter (op =) repTA_tfrees all_TA_params_in_order);
traytel@56012
   856
    val ((TA, (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, _)), lthy) =
blanchet@63802
   857
      maybe_typedef force_out_of_line (T_bind, TA_params, NoSyn) (HOLogic.mk_UNIV repTA) NONE
traytel@60728
   858
        (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy;
blanchet@55854
   859
blanchet@55854
   860
    val repTB = mk_T_of_bnf Ds Bs bnf;
blanchet@55854
   861
    val TB = Term.typ_subst_atomic (As ~~ Bs) TA;
blanchet@55854
   862
    val RepA = Const (Rep_name, TA --> repTA);
blanchet@55854
   863
    val RepB = Const (Rep_name, TB --> repTB);
blanchet@55854
   864
    val AbsA = Const (Abs_name, repTA --> TA);
blanchet@55854
   865
    val AbsB = Const (Abs_name, repTB --> TB);
blanchet@55854
   866
    val Abs_inject' = Abs_inject OF @{thms UNIV_I UNIV_I};
blanchet@55854
   867
    val Abs_inverse' = Abs_inverse OF @{thms UNIV_I};
traytel@55803
   868
traytel@55803
   869
    val absT_info = {absT = TA, repT = repTA, abs = AbsA, rep = RepA, abs_inject = Abs_inject',
blanchet@55854
   870
      abs_inverse = Abs_inverse', type_definition = type_definition};
traytel@55803
   871
traytel@55803
   872
    val bnf_map = fold_rev Term.absfree fs' (HOLogic.mk_comp (HOLogic.mk_comp (AbsB,
traytel@56016
   873
      Term.list_comb (mk_map_of_bnf Ds As Bs bnf, fs)), RepA));
traytel@56016
   874
    val bnf_sets = map ((fn t => HOLogic.mk_comp (t, RepA)))
blanchet@48975
   875
      (mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf);
blanchet@48975
   876
    val bnf_bd = mk_bd_of_bnf Ds As bnf;
traytel@55803
   877
    val bnf_rel = fold_rev Term.absfree Rs' (mk_vimage2p RepA RepB $
traytel@56016
   878
      (Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, Rs)));
traytel@62324
   879
    val bnf_pred = fold_rev Term.absfree Ps' (HOLogic.mk_comp
traytel@62324
   880
      (Term.list_comb (mk_pred_of_bnf Ds As bnf, Ps), RepA));
blanchet@48975
   881
blanchet@55704
   882
    (*bd may depend only on dead type variables*)
blanchet@48975
   883
    val bd_repT = fst (dest_relT (fastype_of bnf_bd));
blanchet@53264
   884
    val bdT_bind = qualify (Binding.suffix_name ("_" ^ bdTN) b);
traytel@55707
   885
    val params = Term.add_tfreesT bd_repT [];
blanchet@63837
   886
    val all_deads = map TFree (fold_rev Term.add_tfreesT all_Ds []);
blanchet@48975
   887
traytel@56012
   888
    val ((bdT, (_, Abs_bd_name, _, _, Abs_bdT_inject, Abs_bdT_cases)), lthy) =
blanchet@63802
   889
      maybe_typedef false (bdT_bind, params, NoSyn) (HOLogic.mk_UNIV bd_repT) NONE
blanchet@63802
   890
        (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy;
blanchet@48975
   891
traytel@56012
   892
    val (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite) =
traytel@56012
   893
      if bdT = bd_repT then (bnf_bd, bd_Card_order_of_bnf bnf RS @{thm ordIso_refl},
traytel@56012
   894
        bd_card_order_of_bnf bnf, bd_cinfinite_of_bnf bnf)
traytel@56012
   895
      else
traytel@56012
   896
        let
traytel@56012
   897
          val bnf_bd' = mk_dir_image bnf_bd (Const (Abs_bd_name, bd_repT --> bdT));
blanchet@48975
   898
traytel@56012
   899
          val Abs_bdT_inj = mk_Abs_inj_thm Abs_bdT_inject;
traytel@56012
   900
          val Abs_bdT_bij = mk_Abs_bij_thm lthy Abs_bdT_inj Abs_bdT_cases;
desharna@57567
   901
traytel@56012
   902
          val bd_ordIso = @{thm dir_image} OF [Abs_bdT_inj, bd_Card_order_of_bnf bnf];
traytel@56012
   903
          val bd_card_order =
traytel@56012
   904
            @{thm card_order_dir_image} OF [Abs_bdT_bij, bd_card_order_of_bnf bnf];
traytel@56012
   905
          val bd_cinfinite =
traytel@56012
   906
            (@{thm Cinfinite_cong} OF [bd_ordIso, bd_Cinfinite_of_bnf bnf]) RS conjunct1;
traytel@56012
   907
        in
traytel@56012
   908
          (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite)
traytel@56012
   909
        end;
blanchet@48975
   910
traytel@60728
   911
    fun map_id0_tac ctxt =
traytel@60728
   912
      rtac ctxt (@{thm type_copy_map_id0} OF [type_definition, map_id0_of_bnf bnf]) 1;
traytel@60728
   913
    fun map_comp0_tac ctxt =
traytel@60728
   914
      rtac ctxt (@{thm type_copy_map_comp0} OF [type_definition, map_comp0_of_bnf bnf]) 1;
traytel@60728
   915
    fun map_cong0_tac ctxt =
traytel@60728
   916
      EVERY' (rtac ctxt @{thm type_copy_map_cong0} :: rtac ctxt (map_cong0_of_bnf bnf) ::
traytel@60728
   917
        map (fn i => EVERY' [select_prem_tac ctxt live (dtac ctxt meta_spec) i, etac ctxt meta_mp,
traytel@60728
   918
          etac ctxt (o_apply RS equalityD2 RS set_mp)]) (1 upto live)) 1;
traytel@60728
   919
    fun set_map0_tac thm ctxt =
traytel@60728
   920
      rtac ctxt (@{thm type_copy_set_map0} OF [type_definition, thm]) 1;
traytel@60728
   921
    val set_bd_tacs = map (fn thm => fn ctxt => rtac ctxt (@{thm ordLeq_ordIso_trans} OF
traytel@56016
   922
        [thm, bd_ordIso] RS @{thm type_copy_set_bd}) 1) (set_bd_of_bnf bnf);
traytel@60728
   923
    fun le_rel_OO_tac ctxt =
traytel@60728
   924
      rtac ctxt (le_rel_OO_of_bnf bnf RS @{thm vimage2p_relcompp_mono}) 1;
traytel@55803
   925
    fun rel_OO_Grp_tac ctxt =
traytel@60728
   926
      (rtac ctxt (rel_OO_Grp_of_bnf bnf RS @{thm vimage2p_cong} RS trans) THEN'
blanchet@63802
   927
       (if force_out_of_line then subst_tac ctxt NONE else SELECT_GOAL o unfold_thms_tac ctxt)
blanchet@58359
   928
         [type_definition RS @{thm vimage2p_relcompp_converse}] THEN'
blanchet@58332
   929
       SELECT_GOAL (unfold_thms_tac ctxt [o_apply,
blanchet@58332
   930
         type_definition RS @{thm type_copy_vimage2p_Grp_Rep},
blanchet@58332
   931
         type_definition RS @{thm vimage2p_relcompp_converse}]) THEN'
traytel@60728
   932
       rtac ctxt refl) 1;
traytel@62324
   933
    fun pred_set_tac ctxt =
traytel@62324
   934
      HEADGOAL (EVERY'
wenzelm@67091
   935
        [rtac ctxt (pred_set_of_bnf bnf RS @{thm arg_cong[of _ _ "\<lambda>f. f \<circ> _"]} RS trans),
traytel@62324
   936
        SELECT_GOAL (unfold_thms_tac ctxt (@{thms Ball_comp_iff conj_comp_iff})), rtac ctxt refl]);
blanchet@49456
   937
traytel@55803
   938
    val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac
traytel@60728
   939
      (map set_map0_tac (set_map0_of_bnf bnf))
traytel@60728
   940
      (fn ctxt => rtac ctxt bd_card_order 1) (fn ctxt => rtac ctxt bd_cinfinite 1)
traytel@62324
   941
      set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac pred_set_tac;
blanchet@48975
   942
traytel@55803
   943
    val bnf_wits = map (fn (I, t) =>
traytel@55803
   944
        fold Term.absdummy (map (nth As) I)
traytel@56016
   945
          (AbsA $ Term.list_comb (t, map Bound (0 upto length I - 1))))
traytel@55803
   946
      (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
blanchet@48975
   947
wenzelm@60752
   948
    fun wit_tac ctxt =
wenzelm@60752
   949
      ALLGOALS (dtac ctxt (type_definition RS @{thm type_copy_wit})) THEN
wenzelm@60752
   950
      mk_simple_wit_tac ctxt (wit_thms_of_bnf bnf);
blanchet@48975
   951
blanchet@53264
   952
    val (bnf', lthy') =
traytel@56016
   953
      bnf_def Hardly_Inline (user_policy Dont_Note) true qualify tacs wit_tac (SOME all_deads)
traytel@62324
   954
        Binding.empty Binding.empty Binding.empty []
traytel@62324
   955
        (((((((b, TA), bnf_map), bnf_sets), bnf_bd'), bnf_wits), SOME bnf_rel), SOME bnf_pred) lthy;
traytel@56016
   956
blanchet@58181
   957
    val unfolds = @{thm id_bnf_apply} ::
traytel@56016
   958
      (#map_unfolds unfold_set @ flat (#set_unfoldss unfold_set) @ #rel_unfolds unfold_set);
traytel@56016
   959
traytel@56016
   960
    val bnf'' = bnf' |> morph_bnf_defs (Morphism.thm_morphism "BNF" (unfold_thms lthy' unfolds));
desharna@57567
   961
traytel@56016
   962
    val map_def = map_def_of_bnf bnf'';
traytel@56016
   963
    val set_defs = set_defs_of_bnf bnf'';
traytel@56018
   964
    val rel_def = rel_def_of_bnf bnf'';
traytel@56016
   965
traytel@56016
   966
    val bnf_b = qualify b;
traytel@56016
   967
    val def_qualify =
wenzelm@59859
   968
      Thm.def_binding o Binding.concealed o Binding.qualify false (Binding.name_of bnf_b);
traytel@56016
   969
    fun mk_prefix_binding pre = Binding.prefix_name (pre ^ "_") bnf_b;
traytel@56016
   970
    val map_b = def_qualify (mk_prefix_binding mapN);
traytel@56016
   971
    val rel_b = def_qualify (mk_prefix_binding relN);
traytel@56016
   972
    val set_bs = if live = 1 then [def_qualify (mk_prefix_binding setN)]
blanchet@59725
   973
      else map (def_qualify o mk_prefix_binding o mk_setN) (1 upto live);
traytel@56016
   974
traytel@56016
   975
    val notes = (map_b, map_def) :: (rel_b, rel_def) :: (set_bs ~~ set_defs)
traytel@56016
   976
      |> map (fn (b, def) => ((b, []), [([def], [])]))
blanchet@57632
   977
blanchet@59820
   978
    val (noted, lthy'') = lthy'
blanchet@59820
   979
      |> Local_Theory.notes notes
blanchet@59820
   980
      ||> (if repTA = TA then I else register_bnf_raw (fst (dest_Type TA)) bnf'')
blanchet@48975
   981
  in
blanchet@57632
   982
    ((morph_bnf (substitute_noted_thm noted) bnf'', (all_deads, absT_info)), lthy'')
blanchet@48975
   983
  end;
blanchet@48975
   984
blanchet@53222
   985
exception BAD_DEAD of typ * typ;
blanchet@53222
   986
blanchet@62621
   987
fun bnf_of_typ _ _ _ _ _ Ds0 (T as TFree T') accum =
blanchet@55704
   988
    (if member (op =) Ds0 T' then (DEADID_bnf, ([T], [])) else (ID_bnf, ([], [T])), accum)
blanchet@62621
   989
  | bnf_of_typ _ _ _ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
blanchet@62621
   990
  | bnf_of_typ optim const_policy qualify' flatten_tyargs Xs Ds0 (T as Type (C, Ts))
blanchet@58332
   991
      (accum as (_, lthy)) =
traytel@49186
   992
    let
blanchet@53222
   993
      fun check_bad_dead ((_, (deads, _)), _) =
blanchet@53222
   994
        let val Ds = fold Term.add_tfreesT deads [] in
blanchet@53222
   995
          (case Library.inter (op =) Ds Xs of [] => ()
blanchet@55705
   996
          | X :: _ => raise BAD_DEAD (TFree X, T))
blanchet@53222
   997
        end;
blanchet@53222
   998
blanchet@55704
   999
      val tfrees = subtract (op =) Ds0 (Term.add_tfreesT T []);
blanchet@55704
  1000
      val bnf_opt = if null tfrees then NONE else bnf_of lthy C;
blanchet@48975
  1001
    in
traytel@49186
  1002
      (case bnf_opt of
blanchet@55704
  1003
        NONE => ((DEADID_bnf, ([T], [])), accum)
traytel@49186
  1004
      | SOME bnf =>
blanchet@62621
  1005
        if optim andalso forall (can Term.dest_TFree) Ts andalso length Ts = length tfrees then
traytel@49186
  1006
          let
traytel@49186
  1007
            val T' = T_of_bnf bnf;
traytel@49186
  1008
            val deads = deads_of_bnf bnf;
traytel@49186
  1009
            val lives = lives_of_bnf bnf;
traytel@49186
  1010
            val tvars' = Term.add_tvarsT T' [];
blanchet@55904
  1011
            val Ds_As =
wenzelm@59058
  1012
              apply2 (map (Term.typ_subst_TVars (map fst tvars' ~~ map TFree tfrees)))
traytel@49186
  1013
                (deads, lives);
blanchet@55904
  1014
          in ((bnf, Ds_As), accum) end
traytel@49186
  1015
        else
traytel@49186
  1016
          let
traytel@49425
  1017
            val name = Long_Name.base_name C;
traytel@49425
  1018
            fun qualify i =
traytel@49425
  1019
              let val namei = name ^ nonzero_string_of_int i;
traytel@49425
  1020
              in qualify' o Binding.qualify true namei end;
traytel@49186
  1021
            val odead = dead_of_bnf bnf;
traytel@49186
  1022
            val olive = live_of_bnf bnf;
traytel@59131
  1023
            val Ds = map (fn i => TFree (string_of_int i, [])) (1 upto odead);
traytel@59131
  1024
            val Us = snd (Term.dest_Type (mk_T_of_bnf Ds (replicate olive dummyT) bnf));
traytel@59131
  1025
            val oDs_pos = map (fn x => find_index (fn y => x = y) Us) Ds
traytel@59131
  1026
              |> filter (fn x => x >= 0);
traytel@49186
  1027
            val oDs = map (nth Ts) oDs_pos;
traytel@49186
  1028
            val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1));
blanchet@55904
  1029
            val ((inners, (Dss, Ass)), (accum', lthy')) =
blanchet@62621
  1030
              apfst (apsnd split_list o split_list) (@{fold_map 2}
blanchet@62621
  1031
                (fn i => bnf_of_typ optim Smart_Inline (qualify i) flatten_tyargs Xs Ds0)
blanchet@59725
  1032
                (if length Ts' = 1 then [0] else 1 upto length Ts') Ts' accum);
traytel@49186
  1033
          in
blanchet@58332
  1034
            compose_bnf const_policy qualify flatten_tyargs bnf inners oDs Dss Ass (accum', lthy')
traytel@49186
  1035
          end)
blanchet@53222
  1036
      |> tap check_bad_dead
blanchet@48975
  1037
    end;
blanchet@48975
  1038
blanchet@48975
  1039
end;