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