src/HOL/Codatatype/Tools/bnf_comp.ML
author blanchet
Thu Aug 30 09:47:46 2012 +0200 (2012-08-30)
changeset 49014 332e5e661675
parent 48975 7f79f94a432c
child 49015 6b7cdb1f37d5
permissions -rw-r--r--
have "bnf_of_typ" command seal the BNF
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@48975
    11
  type unfold_thms
blanchet@48975
    12
  val empty_unfold: unfold_thms
blanchet@48975
    13
  val map_unfolds_of: unfold_thms -> thm list
blanchet@48975
    14
  val set_unfoldss_of: unfold_thms -> thm list list
blanchet@48975
    15
  val rel_unfolds_of: unfold_thms -> thm list
blanchet@48975
    16
  val pred_unfolds_of: unfold_thms -> thm list
blanchet@48975
    17
blanchet@48975
    18
  val bnf_of_typ: BNF_Def.const_policy -> binding -> (binding -> binding) ->
blanchet@48975
    19
    ((string * sort) list list -> (string * sort) list) -> typ -> unfold_thms * Proof.context ->
blanchet@48975
    20
    (BNF_Def.BNF * (typ list * typ list)) * (unfold_thms * Proof.context)
blanchet@48975
    21
  val bnf_of_typ_cmd: binding * string -> Proof.context -> Proof.context
blanchet@49014
    22
  val default_comp_sort: (string * sort) list list -> (string * sort) list
blanchet@48975
    23
  val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list ->
blanchet@48975
    24
    (''a list list -> ''a list) -> BNF_Def.BNF list -> unfold_thms -> Proof.context ->
blanchet@48975
    25
    (int list list * ''a list) * (BNF_Def.BNF list * (unfold_thms * Proof.context))
blanchet@49014
    26
  val seal_bnf: unfold_thms -> binding -> typ list -> BNF_Def.BNF -> Proof.context ->
blanchet@49014
    27
    BNF_Def.BNF * local_theory
blanchet@48975
    28
end;
blanchet@48975
    29
blanchet@48975
    30
structure BNF_Comp : BNF_COMP =
blanchet@48975
    31
struct
blanchet@48975
    32
blanchet@48975
    33
open BNF_Def
blanchet@48975
    34
open BNF_Util
blanchet@48975
    35
open BNF_Tactics
blanchet@48975
    36
open BNF_Comp_Tactics
blanchet@48975
    37
blanchet@48975
    38
type unfold_thms = {
blanchet@48975
    39
  map_unfolds: thm list,
blanchet@48975
    40
  set_unfoldss: thm list list,
blanchet@48975
    41
  rel_unfolds: thm list,
blanchet@48975
    42
  pred_unfolds: thm list
blanchet@48975
    43
};
blanchet@48975
    44
blanchet@48975
    45
fun add_to_thms thms NONE = thms
blanchet@48975
    46
  | add_to_thms thms (SOME new) = if Thm.is_reflexive new then thms else insert Thm.eq_thm new thms;
blanchet@48975
    47
fun adds_to_thms thms NONE = thms
blanchet@48975
    48
  | adds_to_thms thms (SOME news) = insert (eq_set Thm.eq_thm) (filter_refl news) thms;
blanchet@48975
    49
blanchet@48975
    50
fun mk_unfold_thms maps setss rels preds =
blanchet@48975
    51
  {map_unfolds = maps, set_unfoldss = setss, rel_unfolds = rels, pred_unfolds = preds};
blanchet@48975
    52
blanchet@48975
    53
val empty_unfold = mk_unfold_thms [] [] [] [];
blanchet@48975
    54
blanchet@48975
    55
fun add_to_unfold_opt map_opt sets_opt rel_opt pred_opt
blanchet@48975
    56
  {map_unfolds = maps, set_unfoldss = setss, rel_unfolds = rels, pred_unfolds = preds} = {
blanchet@48975
    57
    map_unfolds = add_to_thms maps map_opt,
blanchet@48975
    58
    set_unfoldss = adds_to_thms setss sets_opt,
blanchet@48975
    59
    rel_unfolds = add_to_thms rels rel_opt,
blanchet@48975
    60
    pred_unfolds = add_to_thms preds pred_opt};
blanchet@48975
    61
blanchet@48975
    62
fun add_to_unfold map sets rel pred =
blanchet@48975
    63
  add_to_unfold_opt (SOME map) (SOME sets) (SOME rel) (SOME pred);
blanchet@48975
    64
blanchet@48975
    65
val map_unfolds_of = #map_unfolds;
blanchet@48975
    66
val set_unfoldss_of = #set_unfoldss;
blanchet@48975
    67
val rel_unfolds_of = #rel_unfolds;
blanchet@48975
    68
val pred_unfolds_of = #pred_unfolds;
blanchet@48975
    69
blanchet@48975
    70
val bdTN = "bdT";
blanchet@48975
    71
blanchet@48975
    72
val compN = "comp_"
blanchet@48975
    73
fun mk_killN n = "kill" ^ string_of_int n ^ "_";
blanchet@48975
    74
fun mk_liftN n = "lift" ^ string_of_int n ^ "_";
blanchet@48975
    75
fun mk_permuteN src dest =
blanchet@48975
    76
  "permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest) ^ "_";
blanchet@48975
    77
blanchet@48975
    78
val no_thm = refl;
blanchet@48975
    79
val Collect_split_box_equals = box_equals RS @{thm Collect_split_cong};
blanchet@48975
    80
val abs_pred_sym = sym RS @{thm abs_pred_def};
blanchet@48975
    81
val abs_pred_sym_pred_abs = abs_pred_sym RS @{thm pred_def_abs};
blanchet@48975
    82
blanchet@48975
    83
(*copied from Envir.expand_term_free*)
blanchet@48975
    84
fun expand_term_const defs =
blanchet@48975
    85
  let
blanchet@48975
    86
    val eqs = map ((fn ((x, U), u) => (x, (U, u))) o apfst dest_Const) defs;
blanchet@48975
    87
    val get = fn Const (x, _) => AList.lookup (op =) eqs x | _ => NONE;
blanchet@48975
    88
  in Envir.expand_term get end;
blanchet@48975
    89
blanchet@48975
    90
fun clean_compose_bnf const_policy qualify b outer inners (unfold, lthy) =
blanchet@48975
    91
  let
blanchet@48975
    92
    val olive = live_of_bnf outer;
blanchet@48975
    93
    val onwits = nwits_of_bnf outer;
blanchet@48975
    94
    val odead = dead_of_bnf outer;
blanchet@48975
    95
    val inner = hd inners;
blanchet@48975
    96
    val ilive = live_of_bnf inner;
blanchet@48975
    97
    val ideads = map dead_of_bnf inners;
blanchet@48975
    98
    val inwitss = map nwits_of_bnf inners;
blanchet@48975
    99
blanchet@48975
   100
    (* TODO: check olive = length inners > 0,
blanchet@48975
   101
                   forall inner from inners. ilive = live,
blanchet@48975
   102
                   forall inner from inners. idead = dead  *)
blanchet@48975
   103
blanchet@48975
   104
    val (oDs, lthy1) = apfst (map TFree)
blanchet@48975
   105
      (Variable.invent_types (replicate odead HOLogic.typeS) lthy);
blanchet@48975
   106
    val (Dss, lthy2) = apfst (map (map TFree))
blanchet@48975
   107
        (fold_map Variable.invent_types (map (fn n => replicate n HOLogic.typeS) ideads) lthy1);
blanchet@48975
   108
    val (Ass, lthy3) = apfst (replicate ilive o map TFree)
blanchet@48975
   109
      (Variable.invent_types (replicate ilive HOLogic.typeS) lthy2);
blanchet@48975
   110
    val As = if ilive > 0 then hd Ass else [];
blanchet@48975
   111
    val Ass_repl = replicate olive As;
blanchet@48975
   112
    val (Bs, _(*lthy4*)) = apfst (map TFree)
blanchet@48975
   113
      (Variable.invent_types (replicate ilive HOLogic.typeS) lthy3);
blanchet@48975
   114
    val Bss_repl = replicate olive Bs;
blanchet@48975
   115
blanchet@48975
   116
    val (((fs', Asets), xs), _(*names_lthy*)) = lthy
blanchet@48975
   117
      |> apfst snd o mk_Frees' "f" (map2 (curry (op -->)) As Bs)
blanchet@48975
   118
      ||>> mk_Frees "A" (map (HOLogic.mk_setT) As)
blanchet@48975
   119
      ||>> mk_Frees "x" As;
blanchet@48975
   120
blanchet@48975
   121
    val CAs = map3 mk_T_of_bnf Dss Ass_repl inners;
blanchet@48975
   122
    val CCA = mk_T_of_bnf oDs CAs outer;
blanchet@48975
   123
    val CBs = map3 mk_T_of_bnf Dss Bss_repl inners;
blanchet@48975
   124
    val outer_sets = mk_sets_of_bnf (replicate olive oDs) (replicate olive CAs) outer;
blanchet@48975
   125
    val inner_setss = map3 mk_sets_of_bnf (map (replicate ilive) Dss) (replicate olive Ass) inners;
blanchet@48975
   126
    val inner_bds = map3 mk_bd_of_bnf Dss Ass_repl inners;
blanchet@48975
   127
    val outer_bd = mk_bd_of_bnf oDs CAs outer;
blanchet@48975
   128
blanchet@48975
   129
    (*%f1 ... fn. outer.map (inner_1.map f1 ... fn) ... (inner_m.map f1 ... fn)*)
blanchet@48975
   130
    val comp_map = fold_rev Term.abs fs'
blanchet@48975
   131
      (Term.list_comb (mk_map_of_bnf oDs CAs CBs outer,
blanchet@48975
   132
        map2 (fn Ds => (fn f => Term.list_comb (f, map Bound ((ilive - 1) downto 0))) o
blanchet@48975
   133
          mk_map_of_bnf Ds As Bs) Dss inners));
blanchet@48975
   134
blanchet@48975
   135
    (*Union o collect {outer.set_1 ... outer.set_m} o outer.map inner_1.set_i ... inner_m.set_i*)
blanchet@48975
   136
    (*Union o collect {image inner_1.set_i o outer.set_1 ... image inner_m.set_i o outer.set_m}*)
blanchet@48975
   137
    fun mk_comp_set i =
blanchet@48975
   138
      let
blanchet@48975
   139
        val (setTs, T) = `(replicate olive o HOLogic.mk_setT) (nth As i);
blanchet@48975
   140
        val outer_set = mk_collect
blanchet@48975
   141
          (mk_sets_of_bnf (replicate olive oDs) (replicate olive setTs) outer)
blanchet@48975
   142
          (mk_T_of_bnf oDs setTs outer --> HOLogic.mk_setT T);
blanchet@48975
   143
        val inner_sets = map (fn sets => nth sets i) inner_setss;
blanchet@48975
   144
        val outer_map = mk_map_of_bnf oDs CAs setTs outer;
blanchet@48975
   145
        val map_inner_sets = Term.list_comb (outer_map, inner_sets);
blanchet@48975
   146
        val collect_image = mk_collect
blanchet@48975
   147
          (map2 (fn f => fn set => HOLogic.mk_comp (mk_image f, set)) inner_sets outer_sets)
blanchet@48975
   148
          (CCA --> HOLogic.mk_setT T);
blanchet@48975
   149
      in
blanchet@48975
   150
        (Library.foldl1 HOLogic.mk_comp [mk_Union T, outer_set, map_inner_sets],
blanchet@48975
   151
        HOLogic.mk_comp (mk_Union T, collect_image))
blanchet@48975
   152
      end;
blanchet@48975
   153
blanchet@48975
   154
    val (comp_sets, comp_sets_alt) = map_split mk_comp_set (0 upto ilive - 1);
blanchet@48975
   155
blanchet@48975
   156
    (*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*)
blanchet@48975
   157
    val comp_bd = Term.absdummy CCA (mk_cprod
blanchet@48975
   158
      (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd);
blanchet@48975
   159
blanchet@48975
   160
    fun comp_map_id_tac {context = ctxt, ...} =
blanchet@48975
   161
      let
blanchet@48975
   162
        (*order the theorems by reverse size to prevent bad interaction with nonconfluent rewrite
blanchet@48975
   163
          rules*)
blanchet@48975
   164
        val thms = (map map_id_of_bnf inners
blanchet@48975
   165
          |> map (`(Term.size_of_term o Thm.prop_of))
blanchet@48975
   166
          |> sort (rev_order o int_ord o pairself fst)
blanchet@48975
   167
          |> map snd) @ [map_id_of_bnf outer];
blanchet@48975
   168
      in
blanchet@48975
   169
        (EVERY' (map (fn thm => subst_tac ctxt [thm]) thms) THEN' rtac refl) 1
blanchet@48975
   170
      end;
blanchet@48975
   171
blanchet@48975
   172
    fun comp_map_comp_tac _ =
blanchet@48975
   173
      mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong_of_bnf outer)
blanchet@48975
   174
        (map map_comp_of_bnf inners);
blanchet@48975
   175
blanchet@48975
   176
    fun mk_single_comp_set_natural_tac i _ =
blanchet@48975
   177
      mk_comp_set_natural_tac (map_comp_of_bnf outer) (map_cong_of_bnf outer)
blanchet@48975
   178
        (collect_set_natural_of_bnf outer)
blanchet@48975
   179
        (map ((fn thms => nth thms i) o set_natural_of_bnf) inners);
blanchet@48975
   180
blanchet@48975
   181
    val comp_set_natural_tacs = map mk_single_comp_set_natural_tac (0 upto ilive - 1);
blanchet@48975
   182
blanchet@48975
   183
    fun comp_bd_card_order_tac _ =
blanchet@48975
   184
      mk_comp_bd_card_order_tac (map bd_card_order_of_bnf inners) (bd_card_order_of_bnf outer);
blanchet@48975
   185
blanchet@48975
   186
    fun comp_bd_cinfinite_tac _ =
blanchet@48975
   187
      mk_comp_bd_cinfinite_tac (bd_cinfinite_of_bnf inner) (bd_cinfinite_of_bnf outer);
blanchet@48975
   188
blanchet@48975
   189
    val comp_set_alt_thms =
blanchet@48975
   190
      if ! quick_and_dirty then
blanchet@48975
   191
        replicate ilive no_thm
blanchet@48975
   192
      else
blanchet@48975
   193
        map (fn goal => Skip_Proof.prove lthy [] [] goal
blanchet@48975
   194
        (fn {context, ...} => (mk_comp_set_alt_tac context (collect_set_natural_of_bnf outer))))
blanchet@48975
   195
        (map2 (curry (HOLogic.mk_Trueprop o HOLogic.mk_eq)) comp_sets comp_sets_alt);
blanchet@48975
   196
blanchet@48975
   197
    fun comp_map_cong_tac _ =
blanchet@48975
   198
      mk_comp_map_cong_tac comp_set_alt_thms (map_cong_of_bnf outer) (map map_cong_of_bnf inners);
blanchet@48975
   199
blanchet@48975
   200
    val comp_set_bd_tacs =
blanchet@48975
   201
      if ! quick_and_dirty then
blanchet@48975
   202
        replicate (length comp_set_alt_thms) (K all_tac)
blanchet@48975
   203
      else
blanchet@48975
   204
        let
blanchet@48975
   205
          val outer_set_bds = set_bd_of_bnf outer;
blanchet@48975
   206
          val inner_set_bdss = map set_bd_of_bnf inners;
blanchet@48975
   207
          val inner_bd_Card_orders = map bd_Card_order_of_bnf inners;
blanchet@48975
   208
          fun comp_single_set_bd_thm i j =
blanchet@48975
   209
            @{thm comp_single_set_bd} OF [nth inner_bd_Card_orders j, nth (nth inner_set_bdss j) i,
blanchet@48975
   210
              nth outer_set_bds j]
blanchet@48975
   211
          val single_set_bd_thmss =
blanchet@48975
   212
            map ((fn f => map f (0 upto olive - 1)) o comp_single_set_bd_thm) (0 upto ilive - 1);
blanchet@48975
   213
        in
blanchet@48975
   214
          map2 (fn comp_set_alt => fn single_set_bds => fn {context, ...} =>
blanchet@48975
   215
            mk_comp_set_bd_tac context comp_set_alt single_set_bds)
blanchet@48975
   216
          comp_set_alt_thms single_set_bd_thmss
blanchet@48975
   217
        end;
blanchet@48975
   218
blanchet@48975
   219
    val comp_in_alt_thm =
blanchet@48975
   220
      if ! quick_and_dirty then
blanchet@48975
   221
        no_thm
blanchet@48975
   222
      else
blanchet@48975
   223
        let
blanchet@48975
   224
          val comp_in = mk_in Asets comp_sets CCA;
blanchet@48975
   225
          val comp_in_alt = mk_in (map2 (mk_in Asets) inner_setss CAs) outer_sets CCA;
blanchet@48975
   226
          val goal =
blanchet@48975
   227
            fold_rev Logic.all Asets
blanchet@48975
   228
              (HOLogic.mk_Trueprop (HOLogic.mk_eq (comp_in, comp_in_alt)));
blanchet@48975
   229
        in
blanchet@48975
   230
          Skip_Proof.prove lthy [] [] goal
blanchet@48975
   231
            (fn {context, ...} => mk_comp_in_alt_tac context comp_set_alt_thms)
blanchet@48975
   232
        end;
blanchet@48975
   233
blanchet@48975
   234
    fun comp_in_bd_tac _ =
blanchet@48975
   235
      mk_comp_in_bd_tac comp_in_alt_thm (map in_bd_of_bnf inners) (in_bd_of_bnf outer)
blanchet@48975
   236
        (map bd_Cinfinite_of_bnf inners) (bd_Card_order_of_bnf outer);
blanchet@48975
   237
blanchet@48975
   238
    fun comp_map_wpull_tac _ =
blanchet@48975
   239
      mk_map_wpull_tac comp_in_alt_thm (map map_wpull_of_bnf inners) (map_wpull_of_bnf outer);
blanchet@48975
   240
blanchet@48975
   241
    val tacs = [comp_map_id_tac, comp_map_comp_tac, comp_map_cong_tac] @ comp_set_natural_tacs @
blanchet@48975
   242
      [comp_bd_card_order_tac, comp_bd_cinfinite_tac] @ comp_set_bd_tacs @
blanchet@48975
   243
      [comp_in_bd_tac, comp_map_wpull_tac];
blanchet@48975
   244
blanchet@48975
   245
    val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
blanchet@48975
   246
blanchet@48975
   247
    val inner_witss = map (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)))
blanchet@48975
   248
      (map3 (fn Ds => fn n => mk_wits_of_bnf (replicate n Ds) (replicate n As))
blanchet@48975
   249
        Dss inwitss inners);
blanchet@48975
   250
blanchet@48975
   251
    val inner_witsss = map (map (nth inner_witss) o fst) outer_wits;
blanchet@48975
   252
blanchet@48975
   253
    val comp_wits = (inner_witsss, (map (single o snd) outer_wits))
blanchet@48975
   254
      |-> map2 (fold (map_product (fn iwit => fn owit => owit $ iwit)))
blanchet@48975
   255
      |> flat
blanchet@48975
   256
      |> map (`(fn t => Term.add_frees t []))
blanchet@48975
   257
      |> minimize_wits
blanchet@48975
   258
      |> map (fn (frees, t) => fold absfree frees t);
blanchet@48975
   259
blanchet@48975
   260
    fun wit_tac {context = ctxt, ...} =
blanchet@48975
   261
      mk_comp_wit_tac ctxt (wit_thms_of_bnf outer) (collect_set_natural_of_bnf outer)
blanchet@48975
   262
        (maps wit_thms_of_bnf inners);
blanchet@48975
   263
blanchet@48975
   264
    val (bnf', lthy') =
blanchet@48975
   265
      add_bnf const_policy (K Derive_Some_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss))
blanchet@48975
   266
        ((((b, comp_map), comp_sets), comp_bd), comp_wits) lthy;
blanchet@48975
   267
blanchet@48975
   268
    val outer_rel_Gr = rel_Gr_of_bnf outer RS sym;
blanchet@48975
   269
    val outer_rel_cong = rel_cong_of_bnf outer;
blanchet@48975
   270
blanchet@48975
   271
    val comp_rel_unfold_thm =
blanchet@48975
   272
      trans OF [rel_def_of_bnf bnf',
blanchet@48975
   273
        trans OF [comp_in_alt_thm RS @{thm subst_rel_def},
blanchet@48975
   274
          trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
blanchet@48975
   275
            [trans OF [outer_rel_Gr RS @{thm arg_cong[of _ _ converse]},
blanchet@48975
   276
              rel_converse_of_bnf outer RS sym], outer_rel_Gr],
blanchet@48975
   277
            trans OF [rel_O_of_bnf outer RS sym, outer_rel_cong OF
blanchet@48975
   278
              (map (fn bnf => rel_def_of_bnf bnf RS sym) inners)]]]];
blanchet@48975
   279
blanchet@48975
   280
    val comp_pred_unfold_thm = Collect_split_box_equals OF [comp_rel_unfold_thm,
blanchet@48975
   281
      pred_def_of_bnf bnf' RS abs_pred_sym,
blanchet@48975
   282
        trans OF [outer_rel_cong OF (map (fn bnf => pred_def_of_bnf bnf RS abs_pred_sym) inners),
blanchet@48975
   283
          pred_def_of_bnf outer RS abs_pred_sym]];
blanchet@48975
   284
blanchet@48975
   285
    val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf')
blanchet@48975
   286
      comp_rel_unfold_thm comp_pred_unfold_thm unfold;
blanchet@48975
   287
  in
blanchet@48975
   288
    (bnf', (unfold', lthy'))
blanchet@48975
   289
  end;
blanchet@48975
   290
blanchet@48975
   291
fun clean_compose_bnf_cmd (outer, inners) lthy =
blanchet@48975
   292
  let
blanchet@48975
   293
    val outer = the (bnf_of lthy outer)
blanchet@48975
   294
    val inners = map (the o bnf_of lthy) inners
blanchet@48975
   295
    val b = name_of_bnf outer
blanchet@48975
   296
      |> Binding.prefix_name compN
blanchet@48975
   297
      |> Binding.suffix_name ("_" ^ implode (map (Binding.name_of o name_of_bnf) inners));
blanchet@48975
   298
  in
blanchet@48975
   299
    (snd o snd) (clean_compose_bnf Dont_Inline I b outer inners
blanchet@48975
   300
      (empty_unfold, lthy))
blanchet@48975
   301
  end;
blanchet@48975
   302
blanchet@48975
   303
(* Killing live variables *)
blanchet@48975
   304
blanchet@48975
   305
fun killN_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else
blanchet@48975
   306
  let
blanchet@48975
   307
    val b = Binding.prefix_name (mk_killN n) (name_of_bnf bnf);
blanchet@48975
   308
    val live = live_of_bnf bnf;
blanchet@48975
   309
    val dead = dead_of_bnf bnf;
blanchet@48975
   310
    val nwits = nwits_of_bnf bnf;
blanchet@48975
   311
blanchet@48975
   312
    (* TODO: check 0 < n <= live *)
blanchet@48975
   313
blanchet@48975
   314
    val (Ds, lthy1) = apfst (map TFree)
blanchet@48975
   315
      (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
blanchet@48975
   316
    val ((killedAs, As), lthy2) = apfst (`(take n) o map TFree)
blanchet@48975
   317
      (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
blanchet@48975
   318
    val (Bs, _(*lthy3*)) = apfst (append killedAs o map TFree)
blanchet@48975
   319
      (Variable.invent_types (replicate (live - n) HOLogic.typeS) lthy2);
blanchet@48975
   320
blanchet@48975
   321
    val ((Asets, lives), _(*names_lthy*)) = lthy
blanchet@48975
   322
      |> mk_Frees "A" (map (HOLogic.mk_setT) (drop n As))
blanchet@48975
   323
      ||>> mk_Frees "x" (drop n As);
blanchet@48975
   324
    val xs = map (fn T => HOLogic.choice_const T $ absdummy T @{term True}) killedAs @ lives;
blanchet@48975
   325
blanchet@48975
   326
    val T = mk_T_of_bnf Ds As bnf;
blanchet@48975
   327
blanchet@48975
   328
    (*bnf.map id ... id*)
blanchet@48975
   329
    val killN_map = Term.list_comb (mk_map_of_bnf Ds As Bs bnf, map HOLogic.id_const killedAs);
blanchet@48975
   330
blanchet@48975
   331
    val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
blanchet@48975
   332
    val killN_sets = drop n bnf_sets;
blanchet@48975
   333
blanchet@48975
   334
    (*(|UNIV :: A1 set| +c ... +c |UNIV :: An set|) *c bnf.bd*)
blanchet@48975
   335
    val bnf_bd = mk_bd_of_bnf Ds As bnf;
blanchet@48975
   336
    val killN_bd = mk_cprod
blanchet@48975
   337
      (Library.foldr1 (uncurry mk_csum) (map (mk_card_of o HOLogic.mk_UNIV) killedAs)) bnf_bd;
blanchet@48975
   338
blanchet@48975
   339
    fun killN_map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
blanchet@48975
   340
    fun killN_map_comp_tac {context, ...} =
blanchet@48975
   341
      Local_Defs.unfold_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
blanchet@48975
   342
      rtac refl 1;
blanchet@48975
   343
    fun killN_map_cong_tac {context, ...} =
blanchet@48975
   344
      mk_killN_map_cong_tac context n (live - n) (map_cong_of_bnf bnf);
blanchet@48975
   345
    val killN_set_natural_tacs =
blanchet@48975
   346
      map (fn thm => fn _ => rtac thm 1) (drop n (set_natural_of_bnf bnf));
blanchet@48975
   347
    fun killN_bd_card_order_tac _ = mk_killN_bd_card_order_tac n (bd_card_order_of_bnf bnf);
blanchet@48975
   348
    fun killN_bd_cinfinite_tac _ = mk_killN_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf);
blanchet@48975
   349
    val killN_set_bd_tacs =
blanchet@48975
   350
      map (fn thm => fn _ => mk_killN_set_bd_tac (bd_Card_order_of_bnf bnf) thm)
blanchet@48975
   351
        (drop n (set_bd_of_bnf bnf));
blanchet@48975
   352
blanchet@48975
   353
    val killN_in_alt_thm =
blanchet@48975
   354
      if ! quick_and_dirty then
blanchet@48975
   355
        no_thm
blanchet@48975
   356
      else
blanchet@48975
   357
        let
blanchet@48975
   358
          val killN_in = mk_in Asets killN_sets T;
blanchet@48975
   359
          val killN_in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T;
blanchet@48975
   360
          val goal =
blanchet@48975
   361
            fold_rev Logic.all Asets (HOLogic.mk_Trueprop (HOLogic.mk_eq (killN_in, killN_in_alt)));
blanchet@48975
   362
        in
blanchet@48975
   363
          Skip_Proof.prove lthy [] [] goal (K killN_in_alt_tac)
blanchet@48975
   364
        end;
blanchet@48975
   365
blanchet@48975
   366
    fun killN_in_bd_tac _ =
blanchet@48975
   367
      mk_killN_in_bd_tac n (live > n) killN_in_alt_thm (in_bd_of_bnf bnf)
blanchet@48975
   368
         (bd_Card_order_of_bnf bnf) (bd_Cinfinite_of_bnf bnf) (bd_Cnotzero_of_bnf bnf);
blanchet@48975
   369
    fun killN_map_wpull_tac _ =
blanchet@48975
   370
      mk_map_wpull_tac killN_in_alt_thm [] (map_wpull_of_bnf bnf);
blanchet@48975
   371
blanchet@48975
   372
    val tacs = [killN_map_id_tac, killN_map_comp_tac, killN_map_cong_tac] @ killN_set_natural_tacs @
blanchet@48975
   373
      [killN_bd_card_order_tac, killN_bd_cinfinite_tac] @ killN_set_bd_tacs @
blanchet@48975
   374
      [killN_in_bd_tac, killN_map_wpull_tac];
blanchet@48975
   375
blanchet@48975
   376
    val wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
blanchet@48975
   377
blanchet@48975
   378
    val killN_wits = map (fn t => fold absfree (Term.add_frees t []) t)
blanchet@48975
   379
      (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)) wits);
blanchet@48975
   380
blanchet@48975
   381
    fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
blanchet@48975
   382
blanchet@48975
   383
    val (bnf', lthy') =
blanchet@48975
   384
      add_bnf Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds))
blanchet@48975
   385
        ((((b, killN_map), killN_sets), Term.absdummy T killN_bd), killN_wits) lthy;
blanchet@48975
   386
blanchet@48975
   387
    val rel_Gr = rel_Gr_of_bnf bnf RS sym;
blanchet@48975
   388
blanchet@48975
   389
    val killN_rel_unfold_thm =
blanchet@48975
   390
      trans OF [rel_def_of_bnf bnf',
blanchet@48975
   391
        trans OF [killN_in_alt_thm RS @{thm subst_rel_def},
blanchet@48975
   392
          trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
blanchet@48975
   393
            [trans OF [rel_Gr RS @{thm arg_cong[of _ _ converse]}, rel_converse_of_bnf bnf RS sym],
blanchet@48975
   394
              rel_Gr],
blanchet@48975
   395
            trans OF [rel_O_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF
blanchet@48975
   396
              (replicate n @{thm trans[OF Gr_UNIV_id[OF refl] Id_alt[symmetric]]} @
blanchet@48975
   397
               replicate (live - n) @{thm Gr_fst_snd})]]]];
blanchet@48975
   398
blanchet@48975
   399
    val killN_pred_unfold_thm = Collect_split_box_equals OF
blanchet@48975
   400
      [Local_Defs.unfold lthy' @{thms Id_def'} killN_rel_unfold_thm,
blanchet@48975
   401
        pred_def_of_bnf bnf' RS abs_pred_sym, pred_def_of_bnf bnf RS abs_pred_sym];
blanchet@48975
   402
blanchet@48975
   403
    val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf')
blanchet@48975
   404
      killN_rel_unfold_thm killN_pred_unfold_thm unfold;
blanchet@48975
   405
  in
blanchet@48975
   406
    (bnf', (unfold', lthy'))
blanchet@48975
   407
  end;
blanchet@48975
   408
blanchet@48975
   409
fun killN_bnf_cmd (n, raw_bnf) lthy =
blanchet@48975
   410
  (snd o snd) (killN_bnf I n (the (bnf_of lthy raw_bnf)) (empty_unfold, lthy));
blanchet@48975
   411
blanchet@48975
   412
(* Adding dummy live variables *)
blanchet@48975
   413
blanchet@48975
   414
fun liftN_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else
blanchet@48975
   415
  let
blanchet@48975
   416
    val b = Binding.prefix_name (mk_liftN n) (name_of_bnf bnf);
blanchet@48975
   417
    val live = live_of_bnf bnf;
blanchet@48975
   418
    val dead = dead_of_bnf bnf;
blanchet@48975
   419
    val nwits = nwits_of_bnf bnf;
blanchet@48975
   420
blanchet@48975
   421
    (* TODO: check 0 < n *)
blanchet@48975
   422
blanchet@48975
   423
    val (Ds, lthy1) = apfst (map TFree)
blanchet@48975
   424
      (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
blanchet@48975
   425
    val ((newAs, As), lthy2) = apfst (chop n o map TFree)
blanchet@48975
   426
      (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy1);
blanchet@48975
   427
    val ((newBs, Bs), _(*lthy3*)) = apfst (chop n o map TFree)
blanchet@48975
   428
      (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy2);
blanchet@48975
   429
blanchet@48975
   430
    val (Asets, _(*names_lthy*)) = lthy
blanchet@48975
   431
      |> mk_Frees "A" (map (HOLogic.mk_setT) (newAs @ As));
blanchet@48975
   432
blanchet@48975
   433
    val T = mk_T_of_bnf Ds As bnf;
blanchet@48975
   434
blanchet@48975
   435
    (*%f1 ... fn. bnf.map*)
blanchet@48975
   436
    val liftN_map =
blanchet@48975
   437
      fold_rev Term.absdummy (map2 (curry (op -->)) newAs newBs) (mk_map_of_bnf Ds As Bs bnf);
blanchet@48975
   438
blanchet@48975
   439
    val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
blanchet@48975
   440
    val liftN_sets = map (fn A => absdummy T (HOLogic.mk_set A [])) newAs @ bnf_sets;
blanchet@48975
   441
blanchet@48975
   442
    val liftN_bd = mk_bd_of_bnf Ds As bnf;
blanchet@48975
   443
blanchet@48975
   444
    fun liftN_map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
blanchet@48975
   445
    fun liftN_map_comp_tac {context, ...} =
blanchet@48975
   446
      Local_Defs.unfold_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
blanchet@48975
   447
      rtac refl 1;
blanchet@48975
   448
    fun liftN_map_cong_tac {context, ...} =
blanchet@48975
   449
      rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac context 1);
blanchet@48975
   450
    val liftN_set_natural_tacs =
blanchet@48975
   451
      if ! quick_and_dirty then
blanchet@48975
   452
        replicate (n + live) (K all_tac)
blanchet@48975
   453
      else
blanchet@48975
   454
        replicate n (K empty_natural_tac) @
blanchet@48975
   455
        map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf);
blanchet@48975
   456
    fun liftN_bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
blanchet@48975
   457
    fun liftN_bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
blanchet@48975
   458
    val liftN_set_bd_tacs =
blanchet@48975
   459
      if ! quick_and_dirty then
blanchet@48975
   460
        replicate (n + live) (K all_tac)
blanchet@48975
   461
      else
blanchet@48975
   462
        replicate n (K (mk_liftN_set_bd_tac (bd_Card_order_of_bnf bnf))) @
blanchet@48975
   463
        (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf));
blanchet@48975
   464
blanchet@48975
   465
    val liftN_in_alt_thm =
blanchet@48975
   466
      if ! quick_and_dirty then
blanchet@48975
   467
        no_thm
blanchet@48975
   468
      else
blanchet@48975
   469
        let
blanchet@48975
   470
          val liftN_in = mk_in Asets liftN_sets T;
blanchet@48975
   471
          val liftN_in_alt = mk_in (drop n Asets) bnf_sets T;
blanchet@48975
   472
          val goal =
blanchet@48975
   473
            fold_rev Logic.all Asets (HOLogic.mk_Trueprop (HOLogic.mk_eq (liftN_in, liftN_in_alt)))
blanchet@48975
   474
        in
blanchet@48975
   475
          Skip_Proof.prove lthy [] [] goal (K liftN_in_alt_tac)
blanchet@48975
   476
        end;
blanchet@48975
   477
blanchet@48975
   478
    fun liftN_in_bd_tac _ =
blanchet@48975
   479
      mk_liftN_in_bd_tac n liftN_in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
blanchet@48975
   480
    fun liftN_map_wpull_tac _ =
blanchet@48975
   481
      mk_map_wpull_tac liftN_in_alt_thm [] (map_wpull_of_bnf bnf);
blanchet@48975
   482
blanchet@48975
   483
    val tacs = [liftN_map_id_tac, liftN_map_comp_tac, liftN_map_cong_tac] @ liftN_set_natural_tacs @
blanchet@48975
   484
      [liftN_bd_card_order_tac, liftN_bd_cinfinite_tac] @ liftN_set_bd_tacs @
blanchet@48975
   485
      [liftN_in_bd_tac, liftN_map_wpull_tac];
blanchet@48975
   486
blanchet@48975
   487
    val liftN_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
blanchet@48975
   488
blanchet@48975
   489
    fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
blanchet@48975
   490
blanchet@48975
   491
    val (bnf', lthy') =
blanchet@48975
   492
      add_bnf Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds)
blanchet@48975
   493
        ((((b, liftN_map), liftN_sets), Term.absdummy T liftN_bd), liftN_wits) lthy;
blanchet@48975
   494
blanchet@48975
   495
    val liftN_rel_unfold_thm =
blanchet@48975
   496
      trans OF [rel_def_of_bnf bnf',
blanchet@48975
   497
        trans OF [liftN_in_alt_thm RS @{thm subst_rel_def}, rel_def_of_bnf bnf RS sym]];
blanchet@48975
   498
blanchet@48975
   499
    val liftN_pred_unfold_thm = Collect_split_box_equals OF [liftN_rel_unfold_thm,
blanchet@48975
   500
      pred_def_of_bnf bnf' RS abs_pred_sym, pred_def_of_bnf bnf RS abs_pred_sym];
blanchet@48975
   501
blanchet@48975
   502
    val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf')
blanchet@48975
   503
      liftN_rel_unfold_thm liftN_pred_unfold_thm unfold;
blanchet@48975
   504
  in
blanchet@48975
   505
    (bnf', (unfold', lthy'))
blanchet@48975
   506
  end;
blanchet@48975
   507
blanchet@48975
   508
fun liftN_bnf_cmd (n, raw_bnf) lthy =
blanchet@48975
   509
  (snd o snd) (liftN_bnf I n (the (bnf_of lthy raw_bnf)) (empty_unfold, lthy));
blanchet@48975
   510
blanchet@48975
   511
(* Changing the order of live variables *)
blanchet@48975
   512
blanchet@48975
   513
fun permute_bnf qualify src dest bnf (unfold, lthy) = if src = dest then (bnf, (unfold, lthy)) else
blanchet@48975
   514
  let
blanchet@48975
   515
    val b = Binding.prefix_name (mk_permuteN src dest) (name_of_bnf bnf);
blanchet@48975
   516
    val live = live_of_bnf bnf;
blanchet@48975
   517
    val dead = dead_of_bnf bnf;
blanchet@48975
   518
    val nwits = nwits_of_bnf bnf;
blanchet@48975
   519
    fun permute xs = mk_permute src dest xs;
blanchet@48975
   520
    fun permute_rev xs = mk_permute dest src xs;
blanchet@48975
   521
blanchet@48975
   522
    val (Ds, lthy1) = apfst (map TFree)
blanchet@48975
   523
      (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
blanchet@48975
   524
    val (As, lthy2) = apfst (map TFree)
blanchet@48975
   525
      (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
blanchet@48975
   526
    val (Bs, _(*lthy3*)) = apfst (map TFree)
blanchet@48975
   527
      (Variable.invent_types (replicate live HOLogic.typeS) lthy2);
blanchet@48975
   528
blanchet@48975
   529
    val (Asets, _(*names_lthy*)) = lthy
blanchet@48975
   530
      |> mk_Frees "A" (map (HOLogic.mk_setT) (permute As));
blanchet@48975
   531
blanchet@48975
   532
    val T = mk_T_of_bnf Ds As bnf;
blanchet@48975
   533
blanchet@48975
   534
    (*%f(1) ... f(n). bnf.map f\<sigma>(1) ... f\<sigma>(n)*)
blanchet@48975
   535
    val permute_map = fold_rev Term.absdummy (permute (map2 (curry op -->) As Bs))
blanchet@48975
   536
      (Term.list_comb (mk_map_of_bnf Ds As Bs bnf,
blanchet@48975
   537
        permute_rev (map Bound ((live - 1) downto 0))));
blanchet@48975
   538
blanchet@48975
   539
    val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
blanchet@48975
   540
    val permute_sets = permute bnf_sets;
blanchet@48975
   541
blanchet@48975
   542
    val permute_bd = mk_bd_of_bnf Ds As bnf;
blanchet@48975
   543
blanchet@48975
   544
    fun permute_map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
blanchet@48975
   545
    fun permute_map_comp_tac _ = rtac (map_comp_of_bnf bnf) 1;
blanchet@48975
   546
    fun permute_map_cong_tac {context, ...} =
blanchet@48975
   547
      rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac context 1);
blanchet@48975
   548
    val permute_set_natural_tacs =
blanchet@48975
   549
      permute (map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf));
blanchet@48975
   550
    fun permute_bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
blanchet@48975
   551
    fun permute_bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
blanchet@48975
   552
    val permute_set_bd_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf));
blanchet@48975
   553
blanchet@48975
   554
    val permute_in_alt_thm =
blanchet@48975
   555
      if ! quick_and_dirty then
blanchet@48975
   556
        no_thm
blanchet@48975
   557
      else
blanchet@48975
   558
        let
blanchet@48975
   559
          val permute_in = mk_in Asets permute_sets T;
blanchet@48975
   560
          val permute_in_alt = mk_in (permute_rev Asets) bnf_sets T;
blanchet@48975
   561
          val goal =
blanchet@48975
   562
            fold_rev Logic.all Asets
blanchet@48975
   563
              (HOLogic.mk_Trueprop (HOLogic.mk_eq (permute_in, permute_in_alt)));
blanchet@48975
   564
        in
blanchet@48975
   565
          Skip_Proof.prove lthy [] [] goal (K (mk_permute_in_alt_tac src dest))
blanchet@48975
   566
        end;
blanchet@48975
   567
blanchet@48975
   568
    fun permute_in_bd_tac _ =
blanchet@48975
   569
      mk_permute_in_bd_tac src dest permute_in_alt_thm (in_bd_of_bnf bnf)
blanchet@48975
   570
        (bd_Card_order_of_bnf bnf);
blanchet@48975
   571
    fun permute_map_wpull_tac _ =
blanchet@48975
   572
      mk_map_wpull_tac permute_in_alt_thm [] (map_wpull_of_bnf bnf);
blanchet@48975
   573
blanchet@48975
   574
    val tacs = [permute_map_id_tac, permute_map_comp_tac, permute_map_cong_tac] @
blanchet@48975
   575
      permute_set_natural_tacs @ [permute_bd_card_order_tac, permute_bd_cinfinite_tac] @
blanchet@48975
   576
      permute_set_bd_tacs @ [permute_in_bd_tac, permute_map_wpull_tac];
blanchet@48975
   577
blanchet@48975
   578
    val permute_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
blanchet@48975
   579
blanchet@48975
   580
    fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
blanchet@48975
   581
blanchet@48975
   582
    val (bnf', lthy') =
blanchet@48975
   583
      add_bnf Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds)
blanchet@48975
   584
        ((((b, permute_map), permute_sets), Term.absdummy T permute_bd), permute_wits) lthy;
blanchet@48975
   585
blanchet@48975
   586
    val permute_rel_unfold_thm =
blanchet@48975
   587
      trans OF [rel_def_of_bnf bnf',
blanchet@48975
   588
        trans OF [permute_in_alt_thm RS @{thm subst_rel_def}, rel_def_of_bnf bnf RS sym]];
blanchet@48975
   589
blanchet@48975
   590
    val permute_pred_unfold_thm = Collect_split_box_equals OF [permute_rel_unfold_thm,
blanchet@48975
   591
      pred_def_of_bnf bnf' RS abs_pred_sym, pred_def_of_bnf bnf RS abs_pred_sym];
blanchet@48975
   592
blanchet@48975
   593
    val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf')
blanchet@48975
   594
      permute_rel_unfold_thm permute_pred_unfold_thm unfold;
blanchet@48975
   595
  in
blanchet@48975
   596
    (bnf', (unfold', lthy'))
blanchet@48975
   597
  end;
blanchet@48975
   598
blanchet@48975
   599
fun permute_bnf_cmd ((src, dest), raw_bnf) lthy =
blanchet@48975
   600
  (snd o snd) (permute_bnf I src dest (the (bnf_of lthy raw_bnf))
blanchet@48975
   601
    (empty_unfold, lthy));
blanchet@48975
   602
blanchet@49014
   603
(* Composition pipeline *)
blanchet@49014
   604
blanchet@49014
   605
fun permute_and_kill qualify n src dest bnf =
blanchet@49014
   606
  bnf
blanchet@49014
   607
  |> permute_bnf qualify src dest
blanchet@49014
   608
  #> uncurry (killN_bnf qualify n);
blanchet@49014
   609
blanchet@49014
   610
fun lift_and_permute qualify n src dest bnf =
blanchet@49014
   611
  bnf
blanchet@49014
   612
  |> liftN_bnf qualify n
blanchet@49014
   613
  #> uncurry (permute_bnf qualify src dest);
blanchet@49014
   614
blanchet@49014
   615
fun normalize_bnfs qualify Ass Ds sort bnfs unfold lthy =
blanchet@49014
   616
  let
blanchet@49014
   617
    val before_kill_src = map (fn As => 0 upto (length As - 1)) Ass;
blanchet@49014
   618
    val kill_poss = map (find_indices Ds) Ass;
blanchet@49014
   619
    val live_poss = map2 (subtract (op =)) kill_poss before_kill_src;
blanchet@49014
   620
    val before_kill_dest = map2 append kill_poss live_poss;
blanchet@49014
   621
    val kill_ns = map length kill_poss;
blanchet@49014
   622
    val (inners', (unfold', lthy')) =
blanchet@49014
   623
      fold_map5 (fn i => permute_and_kill (qualify i))
blanchet@49014
   624
        (if length bnfs = 1 then [0] else (1 upto length bnfs))
blanchet@49014
   625
        kill_ns before_kill_src before_kill_dest bnfs (unfold, lthy);
blanchet@49014
   626
blanchet@49014
   627
    val Ass' = map2 (map o nth) Ass live_poss;
blanchet@49014
   628
    val As = sort Ass';
blanchet@49014
   629
    val after_lift_dest = replicate (length Ass') (0 upto (length As - 1));
blanchet@49014
   630
    val old_poss = map (map (fn x => find_index (fn y => x = y) As)) Ass';
blanchet@49014
   631
    val new_poss = map2 (subtract (op =)) old_poss after_lift_dest;
blanchet@49014
   632
    val after_lift_src = map2 append new_poss old_poss;
blanchet@49014
   633
    val lift_ns = map (fn xs => length As - length xs) Ass';
blanchet@49014
   634
  in
blanchet@49014
   635
    ((kill_poss, As), fold_map5 (fn i => lift_and_permute (qualify i))
blanchet@49014
   636
      (if length bnfs = 1 then [0] else (1 upto length bnfs))
blanchet@49014
   637
      lift_ns after_lift_src after_lift_dest inners' (unfold', lthy'))
blanchet@49014
   638
  end;
blanchet@49014
   639
blanchet@49014
   640
fun default_comp_sort Ass =
blanchet@49014
   641
  Library.sort (Term_Ord.typ_ord o pairself TFree) (fold (fold (insert (op =))) Ass []);
blanchet@49014
   642
blanchet@49014
   643
fun compose_bnf const_policy qualify' b sort outer inners oDs Dss tfreess (unfold, lthy) =
blanchet@49014
   644
  let
blanchet@49014
   645
    val name = Binding.name_of b;
blanchet@49014
   646
    fun qualify i bind =
blanchet@49014
   647
      let val namei = if i > 0 then name ^ string_of_int i else name;
blanchet@49014
   648
      in
blanchet@49014
   649
        if member (op =) (#2 (Binding.dest bind)) (namei, true) then qualify' bind
blanchet@49014
   650
        else qualify' (Binding.prefix_name namei bind)
blanchet@49014
   651
      end;
blanchet@49014
   652
blanchet@49014
   653
    val Ass = map (map dest_TFree) tfreess;
blanchet@49014
   654
    val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) [];
blanchet@49014
   655
blanchet@49014
   656
    val ((kill_poss, As), (inners', (unfold', lthy'))) =
blanchet@49014
   657
      normalize_bnfs qualify Ass Ds sort inners unfold lthy;
blanchet@49014
   658
blanchet@49014
   659
    val Ds = oDs @ flat (map3 (append oo map o nth) tfreess kill_poss Dss);
blanchet@49014
   660
    val As = map TFree As;
blanchet@49014
   661
  in
blanchet@49014
   662
    apfst (rpair (Ds, As)) (clean_compose_bnf const_policy I b outer inners' (unfold', lthy'))
blanchet@49014
   663
  end;
blanchet@49014
   664
blanchet@49014
   665
fun compose_bnf_cmd (((((b, outer), inners), oDs), Dss), Ass) lthy = (snd o snd)
blanchet@49014
   666
  (compose_bnf Dont_Inline I b default_comp_sort (the (bnf_of lthy outer))
blanchet@49014
   667
    (map (the o bnf_of lthy) inners)
blanchet@49014
   668
    (map (Syntax.read_typ lthy) oDs) (map (map (Syntax.read_typ lthy)) Dss)
blanchet@49014
   669
    (map (map (Syntax.read_typ lthy)) Ass) (empty_unfold, lthy));
blanchet@49014
   670
blanchet@48975
   671
(* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *)
blanchet@48975
   672
blanchet@48975
   673
fun seal_bnf unfold b Ds bnf lthy =
blanchet@48975
   674
  let
blanchet@48975
   675
    val live = live_of_bnf bnf;
blanchet@48975
   676
    val nwits = nwits_of_bnf bnf;
blanchet@48975
   677
blanchet@48975
   678
    val (As, lthy1) = apfst (map TFree)
blanchet@48975
   679
      (Variable.invent_types (replicate live HOLogic.typeS) (fold Variable.declare_typ Ds lthy));
blanchet@48975
   680
    val (Bs, _) = apfst (map TFree)
blanchet@48975
   681
      (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
blanchet@48975
   682
blanchet@48975
   683
    val map_unfolds = filter_refl (map_unfolds_of unfold);
blanchet@48975
   684
    val set_unfoldss = map filter_refl (set_unfoldss_of unfold);
blanchet@48975
   685
blanchet@48975
   686
    val expand_maps = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of)
blanchet@48975
   687
      map_unfolds);
blanchet@48975
   688
    val expand_sets = fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of))
blanchet@48975
   689
      set_unfoldss);
blanchet@48975
   690
    val unfold_maps = fold (Local_Defs.unfold lthy o single) map_unfolds;
blanchet@48975
   691
    val unfold_sets = fold (Local_Defs.unfold lthy) set_unfoldss;
blanchet@48975
   692
    val unfold_defs = unfold_sets o unfold_maps;
blanchet@48975
   693
    val bnf_map = expand_maps (mk_map_of_bnf Ds As Bs bnf);
blanchet@48975
   694
    val bnf_sets = map (expand_maps o expand_sets)
blanchet@48975
   695
      (mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf);
blanchet@48975
   696
    val bnf_bd = mk_bd_of_bnf Ds As bnf;
blanchet@48975
   697
    val T = mk_T_of_bnf Ds As bnf;
blanchet@48975
   698
blanchet@48975
   699
    (*bd should only depend on dead type variables!*)
blanchet@48975
   700
    val bd_repT = fst (dest_relT (fastype_of bnf_bd));
blanchet@48975
   701
    val bdT_bind = Binding.suffix_name ("_" ^ bdTN) b;
blanchet@48975
   702
    val params = fold Term.add_tfreesT Ds [];
blanchet@48975
   703
blanchet@48975
   704
    val ((bdT_name, (bdT_glob_info, bdT_loc_info)), (lthy', lthy)) =
blanchet@48975
   705
      lthy
blanchet@48975
   706
      |> Typedef.add_typedef true NONE (bdT_bind, params, NoSyn)
blanchet@48975
   707
        (HOLogic.mk_UNIV bd_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1)
blanchet@48975
   708
      ||> `Local_Theory.restore;
blanchet@48975
   709
blanchet@48975
   710
    val phi = Proof_Context.export_morphism lthy lthy';
blanchet@48975
   711
blanchet@48975
   712
    val bnf_bd' = mk_dir_image bnf_bd
blanchet@48975
   713
      (Const (#Abs_name bdT_glob_info, bd_repT --> Type (bdT_name, map TFree params)))
blanchet@48975
   714
blanchet@48975
   715
    val set_def = Morphism.thm phi (the (#set_def bdT_loc_info));
blanchet@48975
   716
    val Abs_inject = Morphism.thm phi (#Abs_inject bdT_loc_info);
blanchet@48975
   717
    val Abs_cases = Morphism.thm phi (#Abs_cases bdT_loc_info);
blanchet@48975
   718
blanchet@48975
   719
    val Abs_bdT_inj = mk_Abs_inj_thm set_def Abs_inject;
blanchet@48975
   720
    val Abs_bdT_bij = mk_Abs_bij_thm lthy' set_def Abs_inject Abs_cases;
blanchet@48975
   721
blanchet@48975
   722
    val bd_ordIso = @{thm dir_image} OF [Abs_bdT_inj, bd_Card_order_of_bnf bnf];
blanchet@48975
   723
    val bd_card_order =
blanchet@48975
   724
      @{thm card_order_dir_image} OF [Abs_bdT_bij, bd_card_order_of_bnf bnf];
blanchet@48975
   725
    val bd_cinfinite =
blanchet@48975
   726
      (@{thm Cinfinite_cong} OF [bd_ordIso, bd_Cinfinite_of_bnf bnf]) RS conjunct1;
blanchet@48975
   727
blanchet@48975
   728
    val set_bds =
blanchet@48975
   729
      map (fn thm => @{thm ordLeq_ordIso_trans} OF [thm, bd_ordIso]) (set_bd_of_bnf bnf);
blanchet@48975
   730
    val in_bd =
blanchet@48975
   731
      @{thm ordLeq_ordIso_trans} OF [in_bd_of_bnf bnf,
blanchet@48975
   732
        @{thm cexp_cong2_Cnotzero} OF [bd_ordIso, if live = 0 then
blanchet@48975
   733
          @{thm ctwo_Cnotzero} else @{thm ctwo_Cnotzero} RS @{thm csum_Cnotzero2},
blanchet@48975
   734
            bd_Card_order_of_bnf bnf]];
blanchet@48975
   735
blanchet@48975
   736
    fun mk_tac thm {context = ctxt, prems = _} = (rtac (unfold_defs thm) THEN'
blanchet@48975
   737
      SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
blanchet@48975
   738
    val tacs =
blanchet@48975
   739
      map mk_tac ([map_id_of_bnf bnf, map_comp_of_bnf bnf, map_cong_of_bnf bnf] @
blanchet@48975
   740
        set_natural_of_bnf bnf) @
blanchet@48975
   741
      map K [rtac bd_card_order 1, rtac bd_cinfinite 1] @
blanchet@48975
   742
      map mk_tac (set_bds @ [in_bd, map_wpull_of_bnf bnf]);
blanchet@48975
   743
blanchet@48975
   744
    val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
blanchet@48975
   745
blanchet@48975
   746
    fun wit_tac _ = mk_simple_wit_tac (map unfold_defs (wit_thms_of_bnf bnf));
blanchet@48975
   747
blanchet@48975
   748
    val (bnf', lthy') = add_bnf Hardly_Inline (K Derive_All_Facts) I tacs wit_tac NONE
blanchet@48975
   749
        ((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits) lthy;
blanchet@48975
   750
blanchet@48975
   751
    val defs' = filter_refl (map_def_of_bnf bnf' :: set_defs_of_bnf bnf');
blanchet@48975
   752
    val unfold_defs' = unfold_defs o Local_Defs.unfold lthy' defs';
blanchet@48975
   753
blanchet@48975
   754
    val rel_def = unfold_defs' (rel_def_of_bnf bnf');
blanchet@48975
   755
    val rel_unfold = Local_Defs.unfold lthy'
blanchet@48975
   756
      (map unfold_defs (filter_refl (rel_unfolds_of unfold))) rel_def;
blanchet@48975
   757
blanchet@48975
   758
    val unfold_defs'' =
blanchet@48975
   759
      unfold_defs' o (Local_Defs.unfold lthy' (filter_refl [rel_def_of_bnf bnf']));
blanchet@48975
   760
blanchet@48975
   761
    val pred_def = unfold_defs'' (pred_def_of_bnf bnf' RS abs_pred_sym_pred_abs);
blanchet@48975
   762
    val pred_unfold = Local_Defs.unfold lthy'
blanchet@48975
   763
      (map unfold_defs (filter_refl (pred_unfolds_of unfold))) pred_def;
blanchet@48975
   764
blanchet@48975
   765
    fun note thmN thms =
blanchet@48975
   766
      snd o Local_Theory.note
blanchet@48975
   767
        ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), thms);
blanchet@48975
   768
  in
blanchet@48975
   769
    (bnf', lthy'
blanchet@48975
   770
      |> note rel_unfoldN [rel_unfold]
blanchet@48975
   771
      |> note pred_unfoldN [pred_unfold])
blanchet@48975
   772
  end;
blanchet@48975
   773
blanchet@48975
   774
fun bnf_of_typ _ _ _ _ (T as TFree _) (unfold, lthy) =
blanchet@48975
   775
    ((Basic_BNFs.ID_bnf, ([], [T])), (add_to_unfold_opt NONE NONE
blanchet@48975
   776
      (SOME Basic_BNFs.ID_rel_def) (SOME Basic_BNFs.ID_pred_def) unfold, lthy))
blanchet@48975
   777
  | bnf_of_typ _ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
blanchet@48975
   778
  | bnf_of_typ const_policy b qualify' sort (T as Type (C, Ts)) (unfold, lthy) =
blanchet@48975
   779
    let val tfrees = Term.add_tfreesT T [];
blanchet@48975
   780
    in
blanchet@48975
   781
      if null tfrees then
blanchet@48975
   782
        ((Basic_BNFs.DEADID_bnf, ([T], [])), (unfold, lthy))
blanchet@48975
   783
      else if forall (can Term.dest_TFree) Ts andalso length Ts = length tfrees then let
blanchet@48975
   784
        val bnf = the (bnf_of lthy (Long_Name.base_name C));
blanchet@48975
   785
        val T' = T_of_bnf bnf;
blanchet@48975
   786
        val deads = deads_of_bnf bnf;
blanchet@48975
   787
        val lives = lives_of_bnf bnf;
blanchet@48975
   788
        val tvars' = Term.add_tvarsT T' [];
blanchet@48975
   789
        val deads_lives =
blanchet@48975
   790
          pairself (map (Term.typ_subst_TVars (map fst tvars' ~~ map TFree tfrees)))
blanchet@48975
   791
          (deads, lives);
blanchet@48975
   792
      val rel_def = rel_def_of_bnf bnf;
blanchet@48975
   793
      val unfold' = add_to_unfold_opt NONE NONE (SOME (rel_def RS sym))
blanchet@48975
   794
        (SOME (Local_Defs.unfold lthy [rel_def] (pred_def_of_bnf bnf) RS sym)) unfold;
blanchet@48975
   795
      in ((bnf, deads_lives), (unfold', lthy)) end
blanchet@48975
   796
      else
blanchet@48975
   797
        let
blanchet@48975
   798
          (* FIXME: we should allow several BNFs with the same base name *)
blanchet@48975
   799
          val Tname = Long_Name.base_name C;
blanchet@48975
   800
          val name = Binding.name_of b ^ "_" ^ Tname;
blanchet@48975
   801
          fun qualify i bind =
blanchet@48975
   802
            let val namei = if i > 0 then name ^ string_of_int i else name;
blanchet@48975
   803
            in
blanchet@48975
   804
              if member (op =) (#2 (Binding.dest bind)) (namei, true) then qualify' bind
blanchet@48975
   805
              else qualify' (Binding.prefix_name namei bind)
blanchet@48975
   806
            end;
blanchet@48975
   807
          val outer = the (bnf_of lthy Tname);
blanchet@48975
   808
          val odead = dead_of_bnf outer;
blanchet@48975
   809
          val olive = live_of_bnf outer;
blanchet@48975
   810
          val oDs_pos = find_indices [TFree ("dead", [])]
blanchet@48975
   811
            (snd (dest_Type
blanchet@48975
   812
              (mk_T_of_bnf (replicate odead (TFree ("dead", []))) (replicate olive dummyT) outer)));
blanchet@48975
   813
          val oDs = map (nth Ts) oDs_pos;
blanchet@48975
   814
          val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1));
blanchet@48975
   815
          val ((inners, (Dss, Ass)), (unfold', lthy')) =
blanchet@48975
   816
            apfst (apsnd split_list o split_list)
blanchet@48975
   817
              (fold_map2 (fn i =>
blanchet@48975
   818
                  bnf_of_typ Smart_Inline (Binding.name (name ^ string_of_int i)) (qualify i) sort)
blanchet@48975
   819
                (if length Ts' = 1 then [0] else (1 upto length Ts'))
blanchet@48975
   820
                Ts' (unfold, lthy));
blanchet@48975
   821
        in
blanchet@48975
   822
          compose_bnf const_policy (qualify 0) b sort outer inners oDs Dss Ass (unfold', lthy')
blanchet@48975
   823
        end
blanchet@48975
   824
    end;
blanchet@48975
   825
blanchet@49014
   826
fun bnf_of_typ_cmd (b, rawT) lthy =
blanchet@49014
   827
  let
blanchet@49014
   828
    val ((bnf, (Ds, As)), (unfold, lthy')) =
blanchet@49014
   829
      bnf_of_typ Smart_Inline b I default_comp_sort (Syntax.read_typ lthy rawT)
blanchet@49014
   830
        (empty_unfold, lthy);
blanchet@49014
   831
  in
blanchet@49014
   832
    snd (seal_bnf unfold b Ds bnf lthy')
blanchet@49014
   833
  end;
blanchet@48975
   834
blanchet@48975
   835
val _ =
blanchet@48975
   836
  Outer_Syntax.local_theory @{command_spec "bnf_of_typ"} "parse a type as composition of BNFs"
blanchet@48975
   837
    (((Parse.binding --| Parse.$$$ "=") -- Parse.typ) >> bnf_of_typ_cmd);
blanchet@48975
   838
blanchet@48975
   839
end;