src/HOL/Codatatype/Tools/bnf_comp.ML
author blanchet
Fri Sep 21 15:53:29 2012 +0200 (2012-09-21)
changeset 49503 dbbde075a42e
parent 49502 92a7c1842c78
child 49504 df9b897fb254
permissions -rw-r--r--
simplified code
blanchet@48975
     1
(*  Title:      HOL/Codatatype/Tools/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@49502
    11
  type unfold_set
blanchet@49502
    12
  val empty_unfolds: unfold_set
blanchet@49502
    13
  val map_unfolds_of: unfold_set -> thm list
blanchet@49502
    14
  val set_unfoldss_of: unfold_set -> thm list list
blanchet@49502
    15
  val pred_unfolds_of: unfold_set -> thm list
blanchet@49502
    16
  val rel_unfolds_of: unfold_set -> thm list
blanchet@48975
    17
traytel@49425
    18
  val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
blanchet@49502
    19
    ((string * sort) list list -> (string * sort) list) -> typ -> unfold_set * Proof.context ->
blanchet@49502
    20
    (BNF_Def.BNF * (typ list * typ list)) * (unfold_set * Proof.context)
blanchet@49014
    21
  val default_comp_sort: (string * sort) list list -> (string * sort) list
blanchet@48975
    22
  val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list ->
blanchet@49502
    23
    (''a list list -> ''a list) -> BNF_Def.BNF list -> unfold_set -> Proof.context ->
blanchet@49502
    24
    (int list list * ''a list) * (BNF_Def.BNF list * (unfold_set * Proof.context))
blanchet@49502
    25
  val seal_bnf: unfold_set -> binding -> typ list -> BNF_Def.BNF -> Proof.context ->
traytel@49185
    26
    (BNF_Def.BNF * typ list) * local_theory
blanchet@48975
    27
end;
blanchet@48975
    28
blanchet@48975
    29
structure BNF_Comp : BNF_COMP =
blanchet@48975
    30
struct
blanchet@48975
    31
blanchet@48975
    32
open BNF_Def
blanchet@48975
    33
open BNF_Util
blanchet@48975
    34
open BNF_Tactics
blanchet@48975
    35
open BNF_Comp_Tactics
blanchet@48975
    36
blanchet@49502
    37
type unfold_set = {
blanchet@48975
    38
  map_unfolds: thm list,
blanchet@48975
    39
  set_unfoldss: thm list list,
blanchet@49463
    40
  pred_unfolds: thm list,
blanchet@49456
    41
  rel_unfolds: thm list
blanchet@48975
    42
};
blanchet@48975
    43
blanchet@49502
    44
val empty_unfolds = {map_unfolds = [], set_unfoldss = [], pred_unfolds = [], rel_unfolds = []};
blanchet@48975
    45
blanchet@49503
    46
fun add_to_thms thms new = thms |> not (Thm.is_reflexive new) ? insert Thm.eq_thm new;
blanchet@49503
    47
fun adds_to_thms thms news = insert (eq_set Thm.eq_thm) (no_reflexive news) thms;
blanchet@49503
    48
blanchet@49503
    49
fun add_to_unfolds map sets pred rel
blanchet@49463
    50
  {map_unfolds, set_unfoldss, pred_unfolds, rel_unfolds} =
blanchet@49503
    51
  {map_unfolds = add_to_thms map_unfolds map,
blanchet@49503
    52
    set_unfoldss = adds_to_thms set_unfoldss sets,
blanchet@49503
    53
    pred_unfolds = add_to_thms pred_unfolds pred,
blanchet@49503
    54
    rel_unfolds = add_to_thms rel_unfolds rel};
blanchet@48975
    55
blanchet@49503
    56
fun add_bnf_to_unfolds bnf =
blanchet@49503
    57
  add_to_unfolds (map_def_of_bnf bnf) (set_defs_of_bnf bnf) (pred_def_of_bnf bnf)
blanchet@49503
    58
    (rel_def_of_bnf bnf);
blanchet@48975
    59
blanchet@48975
    60
val map_unfolds_of = #map_unfolds;
blanchet@48975
    61
val set_unfoldss_of = #set_unfoldss;
blanchet@49463
    62
val pred_unfolds_of = #pred_unfolds;
blanchet@48975
    63
val rel_unfolds_of = #rel_unfolds;
blanchet@48975
    64
blanchet@48975
    65
val bdTN = "bdT";
blanchet@48975
    66
traytel@49425
    67
fun mk_killN n = "_kill" ^ string_of_int n;
traytel@49425
    68
fun mk_liftN n = "_lift" ^ string_of_int n;
blanchet@48975
    69
fun mk_permuteN src dest =
traytel@49425
    70
  "_permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest);
blanchet@48975
    71
blanchet@48975
    72
(*copied from Envir.expand_term_free*)
blanchet@48975
    73
fun expand_term_const defs =
blanchet@48975
    74
  let
blanchet@48975
    75
    val eqs = map ((fn ((x, U), u) => (x, (U, u))) o apfst dest_Const) defs;
blanchet@48975
    76
    val get = fn Const (x, _) => AList.lookup (op =) eqs x | _ => NONE;
blanchet@48975
    77
  in Envir.expand_term get end;
blanchet@48975
    78
blanchet@49502
    79
fun clean_compose_bnf const_policy qualify b outer inners (unfold_set, lthy) =
blanchet@48975
    80
  let
blanchet@48975
    81
    val olive = live_of_bnf outer;
blanchet@48975
    82
    val onwits = nwits_of_bnf outer;
blanchet@48975
    83
    val odead = dead_of_bnf outer;
blanchet@48975
    84
    val inner = hd inners;
blanchet@48975
    85
    val ilive = live_of_bnf inner;
blanchet@48975
    86
    val ideads = map dead_of_bnf inners;
blanchet@48975
    87
    val inwitss = map nwits_of_bnf inners;
blanchet@48975
    88
blanchet@48975
    89
    (* TODO: check olive = length inners > 0,
blanchet@48975
    90
                   forall inner from inners. ilive = live,
blanchet@48975
    91
                   forall inner from inners. idead = dead  *)
blanchet@48975
    92
blanchet@48975
    93
    val (oDs, lthy1) = apfst (map TFree)
blanchet@48975
    94
      (Variable.invent_types (replicate odead HOLogic.typeS) lthy);
blanchet@48975
    95
    val (Dss, lthy2) = apfst (map (map TFree))
blanchet@48975
    96
        (fold_map Variable.invent_types (map (fn n => replicate n HOLogic.typeS) ideads) lthy1);
blanchet@48975
    97
    val (Ass, lthy3) = apfst (replicate ilive o map TFree)
blanchet@48975
    98
      (Variable.invent_types (replicate ilive HOLogic.typeS) lthy2);
blanchet@48975
    99
    val As = if ilive > 0 then hd Ass else [];
blanchet@48975
   100
    val Ass_repl = replicate olive As;
blanchet@48975
   101
    val (Bs, _(*lthy4*)) = apfst (map TFree)
blanchet@48975
   102
      (Variable.invent_types (replicate ilive HOLogic.typeS) lthy3);
blanchet@48975
   103
    val Bss_repl = replicate olive Bs;
blanchet@48975
   104
blanchet@49463
   105
    val ((((fs', Qs'), Asets), xs), _(*names_lthy*)) = lthy
blanchet@48975
   106
      |> apfst snd o mk_Frees' "f" (map2 (curry (op -->)) As Bs)
blanchet@49463
   107
      ||>> apfst snd o mk_Frees' "Q" (map2 mk_pred2T As Bs)
blanchet@49456
   108
      ||>> mk_Frees "A" (map HOLogic.mk_setT As)
blanchet@48975
   109
      ||>> mk_Frees "x" As;
blanchet@48975
   110
blanchet@48975
   111
    val CAs = map3 mk_T_of_bnf Dss Ass_repl inners;
blanchet@48975
   112
    val CCA = mk_T_of_bnf oDs CAs outer;
blanchet@48975
   113
    val CBs = map3 mk_T_of_bnf Dss Bss_repl inners;
blanchet@48975
   114
    val outer_sets = mk_sets_of_bnf (replicate olive oDs) (replicate olive CAs) outer;
blanchet@48975
   115
    val inner_setss = map3 mk_sets_of_bnf (map (replicate ilive) Dss) (replicate olive Ass) inners;
blanchet@48975
   116
    val inner_bds = map3 mk_bd_of_bnf Dss Ass_repl inners;
blanchet@48975
   117
    val outer_bd = mk_bd_of_bnf oDs CAs outer;
blanchet@48975
   118
blanchet@48975
   119
    (*%f1 ... fn. outer.map (inner_1.map f1 ... fn) ... (inner_m.map f1 ... fn)*)
blanchet@49303
   120
    val mapx = fold_rev Term.abs fs'
blanchet@48975
   121
      (Term.list_comb (mk_map_of_bnf oDs CAs CBs outer,
blanchet@49463
   122
        map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o
blanchet@48975
   123
          mk_map_of_bnf Ds As Bs) Dss inners));
blanchet@49463
   124
    (*%Q1 ... Qn. outer.pred (inner_1.pred Q1 ... Qn) ... (inner_m.pred Q1 ... Qn)*)
blanchet@49463
   125
    val pred = fold_rev Term.abs Qs'
blanchet@49463
   126
      (Term.list_comb (mk_pred_of_bnf oDs CAs CBs outer,
blanchet@49463
   127
        map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o
blanchet@49463
   128
          mk_pred_of_bnf Ds As Bs) Dss inners));
blanchet@48975
   129
blanchet@48975
   130
    (*Union o collect {outer.set_1 ... outer.set_m} o outer.map inner_1.set_i ... inner_m.set_i*)
blanchet@48975
   131
    (*Union o collect {image inner_1.set_i o outer.set_1 ... image inner_m.set_i o outer.set_m}*)
blanchet@49303
   132
    fun mk_set i =
blanchet@48975
   133
      let
blanchet@48975
   134
        val (setTs, T) = `(replicate olive o HOLogic.mk_setT) (nth As i);
blanchet@48975
   135
        val outer_set = mk_collect
blanchet@48975
   136
          (mk_sets_of_bnf (replicate olive oDs) (replicate olive setTs) outer)
blanchet@48975
   137
          (mk_T_of_bnf oDs setTs outer --> HOLogic.mk_setT T);
blanchet@48975
   138
        val inner_sets = map (fn sets => nth sets i) inner_setss;
blanchet@48975
   139
        val outer_map = mk_map_of_bnf oDs CAs setTs outer;
blanchet@48975
   140
        val map_inner_sets = Term.list_comb (outer_map, inner_sets);
blanchet@48975
   141
        val collect_image = mk_collect
blanchet@48975
   142
          (map2 (fn f => fn set => HOLogic.mk_comp (mk_image f, set)) inner_sets outer_sets)
blanchet@48975
   143
          (CCA --> HOLogic.mk_setT T);
blanchet@48975
   144
      in
blanchet@48975
   145
        (Library.foldl1 HOLogic.mk_comp [mk_Union T, outer_set, map_inner_sets],
blanchet@48975
   146
        HOLogic.mk_comp (mk_Union T, collect_image))
blanchet@48975
   147
      end;
blanchet@48975
   148
blanchet@49303
   149
    val (sets, sets_alt) = map_split mk_set (0 upto ilive - 1);
blanchet@48975
   150
blanchet@48975
   151
    (*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*)
blanchet@49303
   152
    val bd = Term.absdummy CCA (mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd);
blanchet@48975
   153
blanchet@49303
   154
    fun map_id_tac {context = ctxt, ...} =
blanchet@48975
   155
      let
blanchet@48975
   156
        (*order the theorems by reverse size to prevent bad interaction with nonconfluent rewrite
blanchet@48975
   157
          rules*)
blanchet@48975
   158
        val thms = (map map_id_of_bnf inners
blanchet@48975
   159
          |> map (`(Term.size_of_term o Thm.prop_of))
blanchet@48975
   160
          |> sort (rev_order o int_ord o pairself fst)
blanchet@48975
   161
          |> map snd) @ [map_id_of_bnf outer];
blanchet@48975
   162
      in
blanchet@48975
   163
        (EVERY' (map (fn thm => subst_tac ctxt [thm]) thms) THEN' rtac refl) 1
blanchet@48975
   164
      end;
blanchet@48975
   165
blanchet@49303
   166
    fun map_comp_tac _ =
blanchet@48975
   167
      mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong_of_bnf outer)
blanchet@48975
   168
        (map map_comp_of_bnf inners);
blanchet@48975
   169
blanchet@49303
   170
    fun mk_single_set_natural_tac i _ =
blanchet@48975
   171
      mk_comp_set_natural_tac (map_comp_of_bnf outer) (map_cong_of_bnf outer)
blanchet@48975
   172
        (collect_set_natural_of_bnf outer)
blanchet@48975
   173
        (map ((fn thms => nth thms i) o set_natural_of_bnf) inners);
blanchet@48975
   174
blanchet@49303
   175
    val set_natural_tacs = map mk_single_set_natural_tac (0 upto ilive - 1);
blanchet@48975
   176
blanchet@49303
   177
    fun bd_card_order_tac _ =
blanchet@48975
   178
      mk_comp_bd_card_order_tac (map bd_card_order_of_bnf inners) (bd_card_order_of_bnf outer);
blanchet@48975
   179
blanchet@49303
   180
    fun bd_cinfinite_tac _ =
blanchet@48975
   181
      mk_comp_bd_cinfinite_tac (bd_cinfinite_of_bnf inner) (bd_cinfinite_of_bnf outer);
blanchet@48975
   182
blanchet@49303
   183
    val set_alt_thms =
blanchet@48975
   184
      if ! quick_and_dirty then
blanchet@49456
   185
        []
blanchet@48975
   186
      else
traytel@49109
   187
        map (fn goal =>
traytel@49109
   188
          Skip_Proof.prove lthy [] [] goal
traytel@49109
   189
            (fn {context, ...} => (mk_comp_set_alt_tac context (collect_set_natural_of_bnf outer)))
traytel@49109
   190
          |> Thm.close_derivation)
blanchet@49303
   191
        (map2 (curry (HOLogic.mk_Trueprop o HOLogic.mk_eq)) sets sets_alt);
blanchet@48975
   192
blanchet@49303
   193
    fun map_cong_tac _ =
blanchet@49303
   194
      mk_comp_map_cong_tac set_alt_thms (map_cong_of_bnf outer) (map map_cong_of_bnf inners);
blanchet@48975
   195
blanchet@49303
   196
    val set_bd_tacs =
blanchet@48975
   197
      if ! quick_and_dirty then
blanchet@49303
   198
        replicate (length set_alt_thms) (K all_tac)
blanchet@48975
   199
      else
blanchet@48975
   200
        let
blanchet@48975
   201
          val outer_set_bds = set_bd_of_bnf outer;
blanchet@48975
   202
          val inner_set_bdss = map set_bd_of_bnf inners;
blanchet@48975
   203
          val inner_bd_Card_orders = map bd_Card_order_of_bnf inners;
blanchet@49303
   204
          fun single_set_bd_thm i j =
blanchet@48975
   205
            @{thm comp_single_set_bd} OF [nth inner_bd_Card_orders j, nth (nth inner_set_bdss j) i,
blanchet@48975
   206
              nth outer_set_bds j]
blanchet@48975
   207
          val single_set_bd_thmss =
blanchet@49303
   208
            map ((fn f => map f (0 upto olive - 1)) o single_set_bd_thm) (0 upto ilive - 1);
blanchet@48975
   209
        in
blanchet@49303
   210
          map2 (fn set_alt => fn single_set_bds => fn {context, ...} =>
blanchet@49303
   211
            mk_comp_set_bd_tac context set_alt single_set_bds)
blanchet@49303
   212
          set_alt_thms single_set_bd_thmss
blanchet@48975
   213
        end;
blanchet@48975
   214
blanchet@49303
   215
    val in_alt_thm =
traytel@49155
   216
      let
blanchet@49303
   217
        val inx = mk_in Asets sets CCA;
blanchet@49303
   218
        val in_alt = mk_in (map2 (mk_in Asets) inner_setss CAs) outer_sets CCA;
blanchet@49303
   219
        val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
traytel@49155
   220
      in
traytel@49155
   221
        Skip_Proof.prove lthy [] [] goal
blanchet@49303
   222
          (fn {context, ...} => mk_comp_in_alt_tac context set_alt_thms)
traytel@49155
   223
        |> Thm.close_derivation
traytel@49155
   224
      end;
blanchet@48975
   225
blanchet@49303
   226
    fun in_bd_tac _ =
blanchet@49303
   227
      mk_comp_in_bd_tac in_alt_thm (map in_bd_of_bnf inners) (in_bd_of_bnf outer)
blanchet@48975
   228
        (map bd_Cinfinite_of_bnf inners) (bd_Card_order_of_bnf outer);
blanchet@48975
   229
blanchet@49303
   230
    fun map_wpull_tac _ =
blanchet@49303
   231
      mk_map_wpull_tac in_alt_thm (map map_wpull_of_bnf inners) (map_wpull_of_bnf outer);
blanchet@48975
   232
blanchet@49456
   233
    fun rel_O_Gr_tac _ =
blanchet@49456
   234
      let
blanchet@49463
   235
        val basic_thms = @{thms mem_Collect_eq fst_conv snd_conv}; (*TODO: tune*)
blanchet@49456
   236
        val outer_rel_Gr = rel_Gr_of_bnf outer RS sym;
blanchet@49456
   237
        val outer_rel_cong = rel_cong_of_bnf outer;
blanchet@49463
   238
        val thm =
blanchet@49463
   239
          (trans OF [in_alt_thm RS @{thm subst_rel_def},
blanchet@49463
   240
             trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
blanchet@49463
   241
               [trans OF [outer_rel_Gr RS @{thm arg_cong[of _ _ converse]},
blanchet@49463
   242
                 rel_converse_of_bnf outer RS sym], outer_rel_Gr],
blanchet@49463
   243
               trans OF [rel_O_of_bnf outer RS sym, outer_rel_cong OF
blanchet@49463
   244
                 (map (fn bnf => rel_O_Gr_of_bnf bnf RS sym) inners)]]] RS sym)
blanchet@49463
   245
          |> unfold_defs lthy (basic_thms @ rel_def_of_bnf outer :: map rel_def_of_bnf inners);
blanchet@49456
   246
      in
blanchet@49463
   247
        unfold_defs_tac lthy basic_thms THEN rtac thm 1
blanchet@49463
   248
      end;
blanchet@49456
   249
blanchet@49460
   250
    val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
blanchet@49456
   251
      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac;
blanchet@48975
   252
blanchet@48975
   253
    val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
blanchet@48975
   254
blanchet@48975
   255
    val inner_witss = map (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)))
blanchet@48975
   256
      (map3 (fn Ds => fn n => mk_wits_of_bnf (replicate n Ds) (replicate n As))
blanchet@48975
   257
        Dss inwitss inners);
blanchet@48975
   258
blanchet@48975
   259
    val inner_witsss = map (map (nth inner_witss) o fst) outer_wits;
blanchet@48975
   260
blanchet@49303
   261
    val wits = (inner_witsss, (map (single o snd) outer_wits))
blanchet@48975
   262
      |-> map2 (fold (map_product (fn iwit => fn owit => owit $ iwit)))
blanchet@48975
   263
      |> flat
blanchet@48975
   264
      |> map (`(fn t => Term.add_frees t []))
blanchet@48975
   265
      |> minimize_wits
blanchet@48975
   266
      |> map (fn (frees, t) => fold absfree frees t);
blanchet@48975
   267
blanchet@48975
   268
    fun wit_tac {context = ctxt, ...} =
blanchet@48975
   269
      mk_comp_wit_tac ctxt (wit_thms_of_bnf outer) (collect_set_natural_of_bnf outer)
blanchet@48975
   270
        (maps wit_thms_of_bnf inners);
blanchet@48975
   271
blanchet@48975
   272
    val (bnf', lthy') =
blanchet@49461
   273
      bnf_def const_policy (K Derive_Few_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss))
blanchet@49463
   274
        (((((b, mapx), sets), bd), wits), SOME pred) lthy;
blanchet@48975
   275
  in
blanchet@49503
   276
    (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
blanchet@48975
   277
  end;
blanchet@48975
   278
blanchet@48975
   279
(* Killing live variables *)
blanchet@48975
   280
blanchet@49502
   281
fun kill_bnf qualify n bnf (unfold_set, lthy) = if n = 0 then (bnf, (unfold_set, lthy)) else
blanchet@48975
   282
  let
traytel@49425
   283
    val b = Binding.suffix_name (mk_killN n) (name_of_bnf bnf);
blanchet@48975
   284
    val live = live_of_bnf bnf;
blanchet@48975
   285
    val dead = dead_of_bnf bnf;
blanchet@48975
   286
    val nwits = nwits_of_bnf bnf;
blanchet@48975
   287
blanchet@48975
   288
    (* TODO: check 0 < n <= live *)
blanchet@48975
   289
blanchet@48975
   290
    val (Ds, lthy1) = apfst (map TFree)
blanchet@48975
   291
      (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
blanchet@48975
   292
    val ((killedAs, As), lthy2) = apfst (`(take n) o map TFree)
blanchet@48975
   293
      (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
blanchet@48975
   294
    val (Bs, _(*lthy3*)) = apfst (append killedAs o map TFree)
blanchet@48975
   295
      (Variable.invent_types (replicate (live - n) HOLogic.typeS) lthy2);
blanchet@48975
   296
blanchet@48975
   297
    val ((Asets, lives), _(*names_lthy*)) = lthy
blanchet@49456
   298
      |> mk_Frees "A" (map HOLogic.mk_setT (drop n As))
blanchet@48975
   299
      ||>> mk_Frees "x" (drop n As);
blanchet@48975
   300
    val xs = map (fn T => HOLogic.choice_const T $ absdummy T @{term True}) killedAs @ lives;
blanchet@48975
   301
blanchet@48975
   302
    val T = mk_T_of_bnf Ds As bnf;
blanchet@48975
   303
blanchet@48975
   304
    (*bnf.map id ... id*)
blanchet@49303
   305
    val mapx = Term.list_comb (mk_map_of_bnf Ds As Bs bnf, map HOLogic.id_const killedAs);
blanchet@49463
   306
    (*bnf.pred (op =) ... (op =)*)
blanchet@49463
   307
    val pred = Term.list_comb (mk_pred_of_bnf Ds As Bs bnf, map HOLogic.eq_const killedAs);
blanchet@48975
   308
blanchet@48975
   309
    val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
blanchet@49303
   310
    val sets = drop n bnf_sets;
blanchet@48975
   311
blanchet@48975
   312
    (*(|UNIV :: A1 set| +c ... +c |UNIV :: An set|) *c bnf.bd*)
blanchet@48975
   313
    val bnf_bd = mk_bd_of_bnf Ds As bnf;
blanchet@49303
   314
    val bd = mk_cprod
blanchet@48975
   315
      (Library.foldr1 (uncurry mk_csum) (map (mk_card_of o HOLogic.mk_UNIV) killedAs)) bnf_bd;
blanchet@48975
   316
blanchet@49303
   317
    fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
blanchet@49303
   318
    fun map_comp_tac {context, ...} =
blanchet@49463
   319
      unfold_defs_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
blanchet@48975
   320
      rtac refl 1;
blanchet@49303
   321
    fun map_cong_tac {context, ...} =
blanchet@49304
   322
      mk_kill_map_cong_tac context n (live - n) (map_cong_of_bnf bnf);
blanchet@49303
   323
    val set_natural_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_natural_of_bnf bnf));
blanchet@49304
   324
    fun bd_card_order_tac _ = mk_kill_bd_card_order_tac n (bd_card_order_of_bnf bnf);
blanchet@49304
   325
    fun bd_cinfinite_tac _ = mk_kill_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf);
blanchet@49303
   326
    val set_bd_tacs =
blanchet@49304
   327
      map (fn thm => fn _ => mk_kill_set_bd_tac (bd_Card_order_of_bnf bnf) thm)
blanchet@48975
   328
        (drop n (set_bd_of_bnf bnf));
blanchet@48975
   329
blanchet@49303
   330
    val in_alt_thm =
traytel@49155
   331
      let
blanchet@49303
   332
        val inx = mk_in Asets sets T;
blanchet@49303
   333
        val in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T;
blanchet@49303
   334
        val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
traytel@49155
   335
      in
blanchet@49304
   336
        Skip_Proof.prove lthy [] [] goal (K kill_in_alt_tac) |> Thm.close_derivation
traytel@49155
   337
      end;
blanchet@48975
   338
blanchet@49303
   339
    fun in_bd_tac _ =
blanchet@49304
   340
      mk_kill_in_bd_tac n (live > n) in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf)
blanchet@49303
   341
        (bd_Cinfinite_of_bnf bnf) (bd_Cnotzero_of_bnf bnf);
blanchet@49303
   342
    fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
blanchet@48975
   343
blanchet@49456
   344
    fun rel_O_Gr_tac _ =
blanchet@49456
   345
      let
blanchet@49456
   346
        val rel_Gr = rel_Gr_of_bnf bnf RS sym
blanchet@49463
   347
        val thm =
blanchet@49463
   348
          (trans OF [in_alt_thm RS @{thm subst_rel_def},
blanchet@49463
   349
            trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
blanchet@49463
   350
              [trans OF [rel_Gr RS @{thm arg_cong[of _ _ converse]},
blanchet@49463
   351
                rel_converse_of_bnf bnf RS sym], rel_Gr],
blanchet@49463
   352
              trans OF [rel_O_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF
blanchet@49463
   353
                (replicate n @{thm trans[OF Gr_UNIV_id[OF refl] Id_alt[symmetric]]} @
blanchet@49463
   354
                 replicate (live - n) @{thm Gr_fst_snd})]]] RS sym)
blanchet@49463
   355
          |> unfold_defs lthy (rel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv});
blanchet@49456
   356
      in
blanchet@49463
   357
        rtac thm 1
blanchet@49456
   358
      end;
blanchet@49456
   359
blanchet@49460
   360
    val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
blanchet@49456
   361
      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac;
blanchet@48975
   362
blanchet@49303
   363
    val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
blanchet@48975
   364
blanchet@49303
   365
    val wits = map (fn t => fold absfree (Term.add_frees t []) t)
blanchet@49303
   366
      (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)) bnf_wits);
blanchet@48975
   367
blanchet@48975
   368
    fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
blanchet@48975
   369
blanchet@48975
   370
    val (bnf', lthy') =
blanchet@49461
   371
      bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds))
blanchet@49463
   372
        (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy;
blanchet@48975
   373
  in
blanchet@49503
   374
    (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
blanchet@48975
   375
  end;
blanchet@48975
   376
blanchet@48975
   377
(* Adding dummy live variables *)
blanchet@48975
   378
blanchet@49502
   379
fun lift_bnf qualify n bnf (unfold_set, lthy) = if n = 0 then (bnf, (unfold_set, lthy)) else
blanchet@48975
   380
  let
traytel@49425
   381
    val b = Binding.suffix_name (mk_liftN n) (name_of_bnf bnf);
blanchet@48975
   382
    val live = live_of_bnf bnf;
blanchet@48975
   383
    val dead = dead_of_bnf bnf;
blanchet@48975
   384
    val nwits = nwits_of_bnf bnf;
blanchet@48975
   385
blanchet@48975
   386
    (* TODO: check 0 < n *)
blanchet@48975
   387
blanchet@48975
   388
    val (Ds, lthy1) = apfst (map TFree)
blanchet@48975
   389
      (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
blanchet@48975
   390
    val ((newAs, As), lthy2) = apfst (chop n o map TFree)
blanchet@48975
   391
      (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy1);
blanchet@48975
   392
    val ((newBs, Bs), _(*lthy3*)) = apfst (chop n o map TFree)
blanchet@48975
   393
      (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy2);
blanchet@48975
   394
blanchet@48975
   395
    val (Asets, _(*names_lthy*)) = lthy
blanchet@49456
   396
      |> mk_Frees "A" (map HOLogic.mk_setT (newAs @ As));
blanchet@48975
   397
blanchet@48975
   398
    val T = mk_T_of_bnf Ds As bnf;
blanchet@48975
   399
blanchet@48975
   400
    (*%f1 ... fn. bnf.map*)
blanchet@49303
   401
    val mapx =
blanchet@48975
   402
      fold_rev Term.absdummy (map2 (curry (op -->)) newAs newBs) (mk_map_of_bnf Ds As Bs bnf);
blanchet@49463
   403
    (*%Q1 ... Qn. bnf.pred*)
blanchet@49463
   404
    val pred = fold_rev Term.absdummy (map2 mk_pred2T newAs newBs) (mk_pred_of_bnf Ds As Bs bnf);
blanchet@48975
   405
blanchet@48975
   406
    val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
blanchet@49303
   407
    val sets = map (fn A => absdummy T (HOLogic.mk_set A [])) newAs @ bnf_sets;
blanchet@48975
   408
blanchet@49303
   409
    val bd = mk_bd_of_bnf Ds As bnf;
blanchet@48975
   410
blanchet@49303
   411
    fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
blanchet@49303
   412
    fun map_comp_tac {context, ...} =
blanchet@49463
   413
      unfold_defs_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
blanchet@48975
   414
      rtac refl 1;
blanchet@49303
   415
    fun map_cong_tac {context, ...} =
blanchet@48975
   416
      rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac context 1);
blanchet@49303
   417
    val set_natural_tacs =
blanchet@48975
   418
      if ! quick_and_dirty then
blanchet@48975
   419
        replicate (n + live) (K all_tac)
blanchet@48975
   420
      else
blanchet@48975
   421
        replicate n (K empty_natural_tac) @
blanchet@48975
   422
        map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf);
blanchet@49303
   423
    fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
blanchet@49303
   424
    fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
blanchet@49303
   425
    val set_bd_tacs =
blanchet@48975
   426
      if ! quick_and_dirty then
blanchet@48975
   427
        replicate (n + live) (K all_tac)
blanchet@48975
   428
      else
blanchet@49304
   429
        replicate n (K (mk_lift_set_bd_tac (bd_Card_order_of_bnf bnf))) @
blanchet@48975
   430
        (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf));
blanchet@48975
   431
blanchet@49303
   432
    val in_alt_thm =
traytel@49155
   433
      let
blanchet@49303
   434
        val inx = mk_in Asets sets T;
blanchet@49303
   435
        val in_alt = mk_in (drop n Asets) bnf_sets T;
blanchet@49303
   436
        val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
traytel@49155
   437
      in
blanchet@49304
   438
        Skip_Proof.prove lthy [] [] goal (K lift_in_alt_tac) |> Thm.close_derivation
traytel@49155
   439
      end;
blanchet@48975
   440
blanchet@49304
   441
    fun in_bd_tac _ = mk_lift_in_bd_tac n in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
blanchet@49303
   442
    fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
blanchet@48975
   443
blanchet@49456
   444
    fun rel_O_Gr_tac _ =
blanchet@49463
   445
      mk_simple_rel_O_Gr_tac lthy (rel_def_of_bnf bnf) (rel_O_Gr_of_bnf bnf) in_alt_thm;
blanchet@49456
   446
blanchet@49460
   447
    val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
blanchet@49456
   448
      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac;
blanchet@48975
   449
blanchet@49303
   450
    val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
blanchet@48975
   451
blanchet@48975
   452
    fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
blanchet@48975
   453
blanchet@48975
   454
    val (bnf', lthy') =
blanchet@49461
   455
      bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds)
blanchet@49463
   456
        (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy;
blanchet@48975
   457
blanchet@48975
   458
  in
blanchet@49503
   459
    (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
blanchet@48975
   460
  end;
blanchet@48975
   461
blanchet@48975
   462
(* Changing the order of live variables *)
blanchet@48975
   463
blanchet@49502
   464
fun permute_bnf qualify src dest bnf (unfold_set, lthy) =
blanchet@49502
   465
  if src = dest then (bnf, (unfold_set, lthy)) else
blanchet@48975
   466
  let
traytel@49425
   467
    val b = Binding.suffix_name (mk_permuteN src dest) (name_of_bnf bnf);
blanchet@48975
   468
    val live = live_of_bnf bnf;
blanchet@48975
   469
    val dead = dead_of_bnf bnf;
blanchet@48975
   470
    val nwits = nwits_of_bnf bnf;
blanchet@48975
   471
    fun permute xs = mk_permute src dest xs;
blanchet@48975
   472
    fun permute_rev xs = mk_permute dest src xs;
blanchet@48975
   473
blanchet@48975
   474
    val (Ds, lthy1) = apfst (map TFree)
blanchet@48975
   475
      (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
blanchet@48975
   476
    val (As, lthy2) = apfst (map TFree)
blanchet@48975
   477
      (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
blanchet@48975
   478
    val (Bs, _(*lthy3*)) = apfst (map TFree)
blanchet@48975
   479
      (Variable.invent_types (replicate live HOLogic.typeS) lthy2);
blanchet@48975
   480
blanchet@48975
   481
    val (Asets, _(*names_lthy*)) = lthy
blanchet@49456
   482
      |> mk_Frees "A" (map HOLogic.mk_setT (permute As));
blanchet@48975
   483
blanchet@48975
   484
    val T = mk_T_of_bnf Ds As bnf;
blanchet@48975
   485
blanchet@48975
   486
    (*%f(1) ... f(n). bnf.map f\<sigma>(1) ... f\<sigma>(n)*)
blanchet@49303
   487
    val mapx = fold_rev Term.absdummy (permute (map2 (curry op -->) As Bs))
blanchet@49463
   488
      (Term.list_comb (mk_map_of_bnf Ds As Bs bnf, permute_rev (map Bound (live - 1 downto 0))));
blanchet@49463
   489
    (*%Q(1) ... Q(n). bnf.pred Q\<sigma>(1) ... Q\<sigma>(n)*)
blanchet@49463
   490
    val pred = fold_rev Term.absdummy (permute (map2 mk_pred2T As Bs))
blanchet@49463
   491
      (Term.list_comb (mk_pred_of_bnf Ds As Bs bnf, permute_rev (map Bound (live - 1 downto 0))));
blanchet@48975
   492
blanchet@48975
   493
    val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
blanchet@49303
   494
    val sets = permute bnf_sets;
blanchet@48975
   495
blanchet@49303
   496
    val bd = mk_bd_of_bnf Ds As bnf;
blanchet@48975
   497
blanchet@49303
   498
    fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
blanchet@49303
   499
    fun map_comp_tac _ = rtac (map_comp_of_bnf bnf) 1;
blanchet@49303
   500
    fun map_cong_tac {context, ...} =
blanchet@48975
   501
      rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac context 1);
blanchet@49303
   502
    val set_natural_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf));
blanchet@49303
   503
    fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
blanchet@49303
   504
    fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
blanchet@49303
   505
    val set_bd_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf));
blanchet@48975
   506
blanchet@49303
   507
    val in_alt_thm =
traytel@49155
   508
      let
blanchet@49303
   509
        val inx = mk_in Asets sets T;
blanchet@49303
   510
        val in_alt = mk_in (permute_rev Asets) bnf_sets T;
blanchet@49303
   511
        val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
traytel@49155
   512
      in
traytel@49155
   513
        Skip_Proof.prove lthy [] [] goal (K (mk_permute_in_alt_tac src dest))
traytel@49155
   514
        |> Thm.close_derivation
traytel@49155
   515
      end;
blanchet@48975
   516
blanchet@49303
   517
    fun in_bd_tac _ =
blanchet@49303
   518
      mk_permute_in_bd_tac src dest in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
blanchet@49303
   519
    fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
blanchet@48975
   520
blanchet@49456
   521
    fun rel_O_Gr_tac _ =
blanchet@49463
   522
      mk_simple_rel_O_Gr_tac lthy (rel_def_of_bnf bnf) (rel_O_Gr_of_bnf bnf) in_alt_thm;
blanchet@49456
   523
blanchet@49460
   524
    val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
blanchet@49456
   525
      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac;
blanchet@48975
   526
blanchet@49303
   527
    val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
blanchet@48975
   528
blanchet@48975
   529
    fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
blanchet@48975
   530
blanchet@48975
   531
    val (bnf', lthy') =
blanchet@49461
   532
      bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds)
blanchet@49463
   533
        (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy;
blanchet@48975
   534
  in
blanchet@49503
   535
    (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
blanchet@48975
   536
  end;
blanchet@48975
   537
blanchet@49014
   538
(* Composition pipeline *)
blanchet@49014
   539
blanchet@49014
   540
fun permute_and_kill qualify n src dest bnf =
blanchet@49014
   541
  bnf
blanchet@49014
   542
  |> permute_bnf qualify src dest
blanchet@49304
   543
  #> uncurry (kill_bnf qualify n);
blanchet@49014
   544
blanchet@49014
   545
fun lift_and_permute qualify n src dest bnf =
blanchet@49014
   546
  bnf
blanchet@49304
   547
  |> lift_bnf qualify n
blanchet@49014
   548
  #> uncurry (permute_bnf qualify src dest);
blanchet@49014
   549
blanchet@49502
   550
fun normalize_bnfs qualify Ass Ds sort bnfs unfold_set lthy =
blanchet@49014
   551
  let
blanchet@49014
   552
    val before_kill_src = map (fn As => 0 upto (length As - 1)) Ass;
blanchet@49014
   553
    val kill_poss = map (find_indices Ds) Ass;
blanchet@49014
   554
    val live_poss = map2 (subtract (op =)) kill_poss before_kill_src;
blanchet@49014
   555
    val before_kill_dest = map2 append kill_poss live_poss;
blanchet@49014
   556
    val kill_ns = map length kill_poss;
blanchet@49502
   557
    val (inners', (unfold_set', lthy')) =
blanchet@49014
   558
      fold_map5 (fn i => permute_and_kill (qualify i))
blanchet@49014
   559
        (if length bnfs = 1 then [0] else (1 upto length bnfs))
blanchet@49502
   560
        kill_ns before_kill_src before_kill_dest bnfs (unfold_set, lthy);
blanchet@49014
   561
blanchet@49014
   562
    val Ass' = map2 (map o nth) Ass live_poss;
blanchet@49014
   563
    val As = sort Ass';
blanchet@49014
   564
    val after_lift_dest = replicate (length Ass') (0 upto (length As - 1));
blanchet@49014
   565
    val old_poss = map (map (fn x => find_index (fn y => x = y) As)) Ass';
blanchet@49014
   566
    val new_poss = map2 (subtract (op =)) old_poss after_lift_dest;
blanchet@49014
   567
    val after_lift_src = map2 append new_poss old_poss;
blanchet@49014
   568
    val lift_ns = map (fn xs => length As - length xs) Ass';
blanchet@49014
   569
  in
blanchet@49014
   570
    ((kill_poss, As), fold_map5 (fn i => lift_and_permute (qualify i))
blanchet@49014
   571
      (if length bnfs = 1 then [0] else (1 upto length bnfs))
blanchet@49502
   572
      lift_ns after_lift_src after_lift_dest inners' (unfold_set', lthy'))
blanchet@49014
   573
  end;
blanchet@49014
   574
blanchet@49014
   575
fun default_comp_sort Ass =
blanchet@49014
   576
  Library.sort (Term_Ord.typ_ord o pairself TFree) (fold (fold (insert (op =))) Ass []);
blanchet@49014
   577
blanchet@49502
   578
fun compose_bnf const_policy qualify sort outer inners oDs Dss tfreess (unfold_set, lthy) =
blanchet@49014
   579
  let
traytel@49425
   580
    val b = name_of_bnf outer;
blanchet@49014
   581
blanchet@49121
   582
    val Ass = map (map Term.dest_TFree) tfreess;
blanchet@49014
   583
    val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) [];
blanchet@49014
   584
blanchet@49502
   585
    val ((kill_poss, As), (inners', (unfold_set', lthy'))) =
blanchet@49502
   586
      normalize_bnfs qualify Ass Ds sort inners unfold_set lthy;
blanchet@49014
   587
blanchet@49014
   588
    val Ds = oDs @ flat (map3 (append oo map o nth) tfreess kill_poss Dss);
blanchet@49014
   589
    val As = map TFree As;
blanchet@49014
   590
  in
traytel@49425
   591
    apfst (rpair (Ds, As))
blanchet@49502
   592
      (clean_compose_bnf const_policy (qualify 0) b outer inners' (unfold_set', lthy'))
blanchet@49014
   593
  end;
blanchet@49014
   594
blanchet@48975
   595
(* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *)
blanchet@48975
   596
blanchet@49502
   597
fun seal_bnf unfold_set b Ds bnf lthy =
blanchet@48975
   598
  let
blanchet@48975
   599
    val live = live_of_bnf bnf;
blanchet@48975
   600
    val nwits = nwits_of_bnf bnf;
blanchet@48975
   601
blanchet@48975
   602
    val (As, lthy1) = apfst (map TFree)
blanchet@48975
   603
      (Variable.invent_types (replicate live HOLogic.typeS) (fold Variable.declare_typ Ds lthy));
blanchet@48975
   604
    val (Bs, _) = apfst (map TFree)
blanchet@48975
   605
      (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
blanchet@48975
   606
blanchet@49502
   607
    val map_unfolds = map_unfolds_of unfold_set;
blanchet@49502
   608
    val set_unfoldss = set_unfoldss_of unfold_set;
blanchet@49502
   609
    val pred_unfolds = pred_unfolds_of unfold_set;
blanchet@49502
   610
    val rel_unfolds = rel_unfolds_of unfold_set;
blanchet@48975
   611
blanchet@48975
   612
    val expand_maps = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of)
blanchet@48975
   613
      map_unfolds);
blanchet@48975
   614
    val expand_sets = fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of))
blanchet@48975
   615
      set_unfoldss);
blanchet@49463
   616
    val expand_preds = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of)
blanchet@49463
   617
      pred_unfolds);
blanchet@49463
   618
    val unfold_maps = fold (unfold_defs lthy o single) map_unfolds;
blanchet@49463
   619
    val unfold_sets = fold (unfold_defs lthy) set_unfoldss;
blanchet@49463
   620
    val unfold_preds = unfold_defs lthy pred_unfolds;
blanchet@49463
   621
    val unfold_rels = unfold_defs lthy rel_unfolds;
blanchet@49463
   622
    val unfold_all = unfold_sets o unfold_maps o unfold_preds o unfold_rels;
blanchet@48975
   623
    val bnf_map = expand_maps (mk_map_of_bnf Ds As Bs bnf);
blanchet@48975
   624
    val bnf_sets = map (expand_maps o expand_sets)
blanchet@48975
   625
      (mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf);
blanchet@48975
   626
    val bnf_bd = mk_bd_of_bnf Ds As bnf;
blanchet@49463
   627
    val bnf_pred = expand_preds (mk_pred_of_bnf Ds As Bs bnf);
blanchet@48975
   628
    val T = mk_T_of_bnf Ds As bnf;
blanchet@48975
   629
blanchet@48975
   630
    (*bd should only depend on dead type variables!*)
blanchet@48975
   631
    val bd_repT = fst (dest_relT (fastype_of bnf_bd));
blanchet@48975
   632
    val bdT_bind = Binding.suffix_name ("_" ^ bdTN) b;
blanchet@48975
   633
    val params = fold Term.add_tfreesT Ds [];
traytel@49185
   634
    val deads = map TFree params;
blanchet@48975
   635
traytel@49228
   636
    val ((bdT_name, (bdT_glob_info, bdT_loc_info)), lthy) =
traytel@49228
   637
      typedef false NONE (bdT_bind, params, NoSyn)
traytel@49228
   638
        (HOLogic.mk_UNIV bd_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
blanchet@48975
   639
blanchet@48975
   640
    val bnf_bd' = mk_dir_image bnf_bd
traytel@49185
   641
      (Const (#Abs_name bdT_glob_info, bd_repT --> Type (bdT_name, deads)))
blanchet@48975
   642
traytel@49228
   643
    val Abs_bdT_inj = mk_Abs_inj_thm (#Abs_inject bdT_loc_info);
traytel@49228
   644
    val Abs_bdT_bij = mk_Abs_bij_thm lthy Abs_bdT_inj (#Abs_cases bdT_loc_info);
blanchet@48975
   645
blanchet@48975
   646
    val bd_ordIso = @{thm dir_image} OF [Abs_bdT_inj, bd_Card_order_of_bnf bnf];
blanchet@48975
   647
    val bd_card_order =
blanchet@48975
   648
      @{thm card_order_dir_image} OF [Abs_bdT_bij, bd_card_order_of_bnf bnf];
blanchet@48975
   649
    val bd_cinfinite =
blanchet@48975
   650
      (@{thm Cinfinite_cong} OF [bd_ordIso, bd_Cinfinite_of_bnf bnf]) RS conjunct1;
blanchet@48975
   651
blanchet@48975
   652
    val set_bds =
blanchet@48975
   653
      map (fn thm => @{thm ordLeq_ordIso_trans} OF [thm, bd_ordIso]) (set_bd_of_bnf bnf);
blanchet@48975
   654
    val in_bd =
blanchet@48975
   655
      @{thm ordLeq_ordIso_trans} OF [in_bd_of_bnf bnf,
blanchet@48975
   656
        @{thm cexp_cong2_Cnotzero} OF [bd_ordIso, if live = 0 then
blanchet@48975
   657
          @{thm ctwo_Cnotzero} else @{thm ctwo_Cnotzero} RS @{thm csum_Cnotzero2},
blanchet@48975
   658
            bd_Card_order_of_bnf bnf]];
blanchet@48975
   659
blanchet@49463
   660
    fun mk_tac thm {context = ctxt, prems = _} =
blanchet@49463
   661
      (rtac (unfold_all thm) THEN'
blanchet@48975
   662
      SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
blanchet@49456
   663
blanchet@49460
   664
    val tacs = zip_axioms (mk_tac (map_id_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf))
blanchet@49456
   665
      (mk_tac (map_cong_of_bnf bnf)) (map mk_tac (set_natural_of_bnf bnf))
blanchet@49456
   666
      (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac in_bd)
blanchet@49463
   667
      (mk_tac (map_wpull_of_bnf bnf))
blanchet@49463
   668
      (mk_tac (unfold_defs lthy [rel_def_of_bnf bnf] (rel_O_Gr_of_bnf bnf)));
blanchet@48975
   669
blanchet@48975
   670
    val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
blanchet@48975
   671
blanchet@49463
   672
    fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf));
blanchet@48975
   673
traytel@49435
   674
    val policy = user_policy Derive_All_Facts;
traytel@49435
   675
traytel@49435
   676
    val (bnf', lthy') = bnf_def Hardly_Inline policy I tacs wit_tac (SOME deads)
blanchet@49463
   677
      (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_pred) lthy;
blanchet@48975
   678
  in
blanchet@49456
   679
    ((bnf', deads), lthy')
blanchet@48975
   680
  end;
blanchet@48975
   681
blanchet@49450
   682
val ID_bnf = the (bnf_of @{context} "Basic_BNFs.ID");
blanchet@49450
   683
val DEADID_bnf = the (bnf_of @{context} "Basic_BNFs.DEADID");
blanchet@49450
   684
blanchet@49456
   685
fun bnf_of_typ _ _ _ (T as TFree _) accum = ((ID_bnf, ([], [T])), accum)
traytel@49425
   686
  | bnf_of_typ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
blanchet@49502
   687
  | bnf_of_typ const_policy qualify' sort (T as Type (C, Ts)) (unfold_set, lthy) =
traytel@49186
   688
    let
traytel@49186
   689
      val tfrees = Term.add_tfreesT T [];
traytel@49236
   690
      val bnf_opt = if null tfrees then NONE else bnf_of lthy C;
blanchet@48975
   691
    in
traytel@49186
   692
      (case bnf_opt of
blanchet@49502
   693
        NONE => ((DEADID_bnf, ([T], [])), (unfold_set, lthy))
traytel@49186
   694
      | SOME bnf =>
traytel@49186
   695
        if forall (can Term.dest_TFree) Ts andalso length Ts = length tfrees then
traytel@49186
   696
          let
traytel@49186
   697
            val T' = T_of_bnf bnf;
traytel@49186
   698
            val deads = deads_of_bnf bnf;
traytel@49186
   699
            val lives = lives_of_bnf bnf;
traytel@49186
   700
            val tvars' = Term.add_tvarsT T' [];
traytel@49186
   701
            val deads_lives =
traytel@49186
   702
              pairself (map (Term.typ_subst_TVars (map fst tvars' ~~ map TFree tfrees)))
traytel@49186
   703
                (deads, lives);
blanchet@49502
   704
          in ((bnf, deads_lives), (unfold_set, lthy)) end
traytel@49186
   705
        else
traytel@49186
   706
          let
traytel@49425
   707
            val name = Long_Name.base_name C;
traytel@49425
   708
            fun qualify i =
traytel@49425
   709
              let val namei = name ^ nonzero_string_of_int i;
traytel@49425
   710
              in qualify' o Binding.qualify true namei end;
traytel@49186
   711
            val odead = dead_of_bnf bnf;
traytel@49186
   712
            val olive = live_of_bnf bnf;
traytel@49186
   713
            val oDs_pos = find_indices [TFree ("dead", [])] (snd (Term.dest_Type
traytel@49186
   714
              (mk_T_of_bnf (replicate odead (TFree ("dead", []))) (replicate olive dummyT) bnf)));
traytel@49186
   715
            val oDs = map (nth Ts) oDs_pos;
traytel@49186
   716
            val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1));
blanchet@49502
   717
            val ((inners, (Dss, Ass)), (unfold_set', lthy')) =
traytel@49186
   718
              apfst (apsnd split_list o split_list)
traytel@49425
   719
                (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) sort)
blanchet@49502
   720
                (if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' (unfold_set, lthy));
traytel@49186
   721
          in
blanchet@49502
   722
            compose_bnf const_policy qualify sort bnf inners oDs Dss Ass (unfold_set', lthy')
traytel@49186
   723
          end)
blanchet@48975
   724
    end;
blanchet@48975
   725
blanchet@48975
   726
end;