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