src/HOL/Tools/BNF/bnf_gfp_grec.ML
changeset 62692 0701f25fac39
child 62699 add334b71e16
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Tue Mar 22 12:39:37 2016 +0100
     1.3 @@ -0,0 +1,3234 @@
     1.4 +(*  Title:      HOL/Tools/BNF/bnf_gfp_grec.ML
     1.5 +    Author:     Jasmin Blanchette, Inria, LORIA, MPII
     1.6 +    Author:     Aymeric Bouzy, Ecole polytechnique
     1.7 +    Author:     Dmitriy Traytel, ETH Z├╝rich
     1.8 +    Copyright   2015, 2016
     1.9 +
    1.10 +Generalized corecursor construction.
    1.11 +*)
    1.12 +
    1.13 +signature BNF_GFP_GREC =
    1.14 +sig
    1.15 +  val Tsubst: typ -> typ -> typ -> typ
    1.16 +  val substT: typ -> typ -> term -> term
    1.17 +  val freeze_types: Proof.context -> (indexname * sort) list -> typ list -> typ list
    1.18 +  val dummify_atomic_types: term -> term
    1.19 +  val enforce_type: Proof.context -> (typ -> typ) -> typ -> term -> term
    1.20 +  val define_const: bool -> binding -> int -> string -> term -> local_theory ->
    1.21 +    (term * thm) * local_theory
    1.22 +
    1.23 +  type buffer =
    1.24 +    {Oper: term,
    1.25 +     VLeaf: term,
    1.26 +     CLeaf: term,
    1.27 +     ctr_wrapper: term,
    1.28 +     friends: (typ * term) Symtab.table}
    1.29 +
    1.30 +  val map_buffer: (term -> term) -> buffer -> buffer
    1.31 +  val specialize_buffer_types: buffer -> buffer
    1.32 +
    1.33 +  type dtor_coinduct_info =
    1.34 +    {dtor_coinduct: thm,
    1.35 +     cong_def: thm,
    1.36 +     cong_locale: thm,
    1.37 +     cong_base: thm,
    1.38 +     cong_refl: thm,
    1.39 +     cong_sym: thm,
    1.40 +     cong_trans: thm,
    1.41 +     cong_alg_intros: thm list}
    1.42 +
    1.43 +  type corec_info =
    1.44 +    {fp_b: binding,
    1.45 +     version: int,
    1.46 +     fpT: typ,
    1.47 +     Y: typ,
    1.48 +     Z: typ,
    1.49 +     friend_names: string list,
    1.50 +     sig_fp_sugars: BNF_FP_Def_Sugar.fp_sugar list,
    1.51 +     ssig_fp_sugar: BNF_FP_Def_Sugar.fp_sugar,
    1.52 +     Lam: term,
    1.53 +     proto_sctr: term,
    1.54 +     flat: term,
    1.55 +     eval_core: term,
    1.56 +     eval: term,
    1.57 +     algLam: term,
    1.58 +     corecUU: term,
    1.59 +     dtor_transfer: thm,
    1.60 +     Lam_transfer: thm,
    1.61 +     Lam_pointful_natural: thm,
    1.62 +     proto_sctr_transfer: thm,
    1.63 +     flat_simps: thm list,
    1.64 +     eval_core_simps: thm list,
    1.65 +     eval_thm: thm,
    1.66 +     eval_simps: thm list,
    1.67 +     all_algLam_algs: thm list,
    1.68 +     algLam_thm: thm,
    1.69 +     dtor_algLam: thm,
    1.70 +     corecUU_thm: thm,
    1.71 +     corecUU_unique: thm,
    1.72 +     corecUU_transfer: thm,
    1.73 +     buffer: buffer,
    1.74 +     all_dead_k_bnfs: BNF_Def.bnf list,
    1.75 +     Retr: term,
    1.76 +     equivp_Retr: thm,
    1.77 +     Retr_coinduct: thm,
    1.78 +     dtor_coinduct_info: dtor_coinduct_info}
    1.79 +
    1.80 +  type friend_info =
    1.81 +    {algrho: term,
    1.82 +     dtor_algrho: thm,
    1.83 +     algLam_algrho: thm}
    1.84 +
    1.85 +  val not_codatatype: Proof.context -> typ -> 'a
    1.86 +  val mk_fp_binding: binding -> string -> binding
    1.87 +  val bnf_kill_all_but: int -> BNF_Def.bnf -> local_theory -> BNF_Def.bnf * local_theory
    1.88 +
    1.89 +  val print_corec_infos: Proof.context -> unit
    1.90 +  val has_no_corec_info: Proof.context -> string -> bool
    1.91 +  val corec_info_of: typ -> local_theory -> corec_info * local_theory
    1.92 +  val maybe_corec_info_of: Proof.context -> typ -> corec_info option
    1.93 +  val corec_infos_of: Proof.context -> string -> corec_info list
    1.94 +  val corec_infos_of_generic: Context.generic -> Symtab.key -> corec_info list
    1.95 +  val prepare_friend_corec: string -> typ -> local_theory ->
    1.96 +    (corec_info * binding * int * typ * typ * typ * typ * typ * BNF_Def.bnf * BNF_Def.bnf
    1.97 +     * BNF_FP_Def_Sugar.fp_sugar * BNF_FP_Def_Sugar.fp_sugar * buffer) * local_theory
    1.98 +  val register_friend_corec: string -> binding -> int -> typ -> typ -> typ -> BNF_Def.bnf ->
    1.99 +    BNF_FP_Def_Sugar.fp_sugar -> BNF_FP_Def_Sugar.fp_sugar -> term -> term -> thm -> corec_info ->
   1.100 +    local_theory -> friend_info * local_theory
   1.101 +end;
   1.102 +
   1.103 +structure BNF_GFP_Grec : BNF_GFP_GREC =
   1.104 +struct
   1.105 +
   1.106 +open Ctr_Sugar
   1.107 +open BNF_Util
   1.108 +open BNF_Def
   1.109 +open BNF_Comp
   1.110 +open BNF_FP_Util
   1.111 +open BNF_LFP
   1.112 +open BNF_FP_Def_Sugar
   1.113 +open BNF_LFP_Rec_Sugar
   1.114 +open BNF_GFP_Grec_Tactics
   1.115 +
   1.116 +val algLamN = "algLam";
   1.117 +val algLam_algLamN = "algLam_algLam";
   1.118 +val algLam_algrhoN = "algLam_algrho";
   1.119 +val algrhoN = "algrho";
   1.120 +val CLeafN = "CLeaf";
   1.121 +val congN = "congclp";
   1.122 +val cong_alg_introsN = "cong_alg_intros";
   1.123 +val cong_localeN = "cong_locale";
   1.124 +val corecUUN = "corecUU";
   1.125 +val corecUU_transferN = "corecUU_transfer";
   1.126 +val corecUU_uniqueN = "corecUU_unique";
   1.127 +val cutSsigN = "cutSsig";
   1.128 +val dtor_algLamN = "dtor_algLam";
   1.129 +val dtor_algrhoN = "dtor_algrho";
   1.130 +val dtor_coinductN = "dtor_coinduct";
   1.131 +val dtor_transferN = "dtor_transfer";
   1.132 +val embLN = "embL";
   1.133 +val embLLN = "embLL";
   1.134 +val embLRN = "embLR";
   1.135 +val embL_pointful_naturalN = "embL_pointful_natural";
   1.136 +val embL_transferN = "embL_transfer";
   1.137 +val equivp_RetrN = "equivp_Retr";
   1.138 +val evalN = "eval";
   1.139 +val eval_coreN = "eval_core";
   1.140 +val eval_core_pointful_naturalN = "eval_core_pointful_natural";
   1.141 +val eval_core_transferN = "eval_core_transfer";
   1.142 +val eval_flatN = "eval_flat";
   1.143 +val eval_simpsN = "eval_simps";
   1.144 +val flatN = "flat";
   1.145 +val flat_pointful_naturalN = "flat_pointful_natural";
   1.146 +val flat_transferN = "flat_transfer";
   1.147 +val k_as_ssig_naturalN = "k_as_ssig_natural";
   1.148 +val k_as_ssig_transferN = "k_as_ssig_transfer";
   1.149 +val LamN = "Lam";
   1.150 +val Lam_transferN = "Lam_transfer";
   1.151 +val Lam_pointful_naturalN = "Lam_pointful_natural";
   1.152 +val OperN = "Oper";
   1.153 +val proto_sctrN = "proto_sctr";
   1.154 +val proto_sctr_pointful_naturalN = "proto_sctr_pointful_natural";
   1.155 +val proto_sctr_transferN = "proto_sctr_transfer";
   1.156 +val rho_transferN = "rho_transfer";
   1.157 +val Retr_coinductN = "Retr_coinduct";
   1.158 +val sctrN = "sctr";
   1.159 +val sctr_transferN = "sctr_transfer";
   1.160 +val sctr_pointful_naturalN = "sctr_pointful_natural";
   1.161 +val sigN = "sig";
   1.162 +val SigN = "Sig";
   1.163 +val Sig_pointful_naturalN = "Sig_pointful_natural";
   1.164 +val corecUN = "corecU";
   1.165 +val corecU_ctorN = "corecU_ctor";
   1.166 +val corecU_uniqueN = "corecU_unique";
   1.167 +val unsigN = "unsig";
   1.168 +val VLeafN = "VLeaf";
   1.169 +
   1.170 +val s_prefix = "s"; (* transforms "sig" into "ssig" *)
   1.171 +
   1.172 +fun not_codatatype ctxt T =
   1.173 +  error ("Not a codatatype: " ^ Syntax.string_of_typ ctxt T);
   1.174 +fun mutual_codatatype () =
   1.175 +  error ("Mutually corecursive codatatypes are not supported (try " ^
   1.176 +    quote (#1 @{command_keyword primcorec}) ^ " instead of " ^
   1.177 +    quote (#1 @{command_keyword corec}) ^ ")");
   1.178 +fun noncorecursive_codatatype () =
   1.179 +  error ("Noncorecursive codatatypes are not supported (try " ^
   1.180 +    quote (#1 @{command_keyword definition}) ^ " instead of " ^
   1.181 +    quote (#1 @{command_keyword corec}) ^ ")");
   1.182 +fun singleton_codatatype ctxt =
   1.183 +  error ("Singleton corecursive codatatypes are not supported (use " ^
   1.184 +    quote (Syntax.string_of_typ ctxt @{typ unit}) ^ " instead)");
   1.185 +
   1.186 +fun merge_lists eq old1 old2 = (old1 |> subtract eq old2) @ old2;
   1.187 +
   1.188 +fun add_type_namesT (Type (s, Ts)) = insert (op =) s #> fold add_type_namesT Ts
   1.189 +  | add_type_namesT _ = I;
   1.190 +
   1.191 +fun Tsubst Y T = Term.typ_subst_atomic [(Y, T)];
   1.192 +fun substT Y T = Term.subst_atomic_types [(Y, T)];
   1.193 +
   1.194 +fun freeze_types ctxt except_tvars Ts =
   1.195 +  let
   1.196 +    val As = fold Term.add_tvarsT Ts [] |> subtract (op =) except_tvars;
   1.197 +    val (Bs, _) = ctxt |> mk_TFrees' (map snd As);
   1.198 +  in
   1.199 +    map (Term.typ_subst_TVars (map fst As ~~ Bs)) Ts
   1.200 +  end;
   1.201 +
   1.202 +fun typ_unify_disjointly thy (T, T') =
   1.203 +  if T = T' then
   1.204 +    T
   1.205 +  else
   1.206 +    let
   1.207 +      val tvars = Term.add_tvar_namesT T [];
   1.208 +      val tvars' = Term.add_tvar_namesT T' [];
   1.209 +      val maxidx' = maxidx_of_typ T';
   1.210 +      val T = T |> exists (member (op =) tvars') tvars ? Logic.incr_tvar (maxidx' + 1);
   1.211 +      val maxidx = Integer.max (maxidx_of_typ T) maxidx';
   1.212 +      val (tyenv, _) = Sign.typ_unify thy (T, T') (Vartab.empty, maxidx);
   1.213 +    in
   1.214 +      Envir.subst_type tyenv T
   1.215 +    end;
   1.216 +
   1.217 +val dummify_atomic_types = Term.map_types (Term.map_atyps (K Term.dummyT));
   1.218 +
   1.219 +fun enforce_type ctxt get_T T t =
   1.220 +  Term.subst_TVars (tvar_subst (Proof_Context.theory_of ctxt) [get_T (fastype_of t)] [T]) t;
   1.221 +
   1.222 +fun mk_internal internal ctxt f =
   1.223 +  if internal andalso not (Config.get ctxt bnf_internals) then f else I
   1.224 +fun mk_fp_binding fp_b pre = Binding.map_name (K pre) fp_b
   1.225 +  |> Binding.qualify true (Binding.name_of fp_b);
   1.226 +fun mk_version_binding version = Binding.qualify false ("v" ^ string_of_int version);
   1.227 +fun mk_version_fp_binding internal ctxt =
   1.228 +  mk_internal internal ctxt Binding.concealed ooo (mk_fp_binding oo mk_version_binding);
   1.229 +(*FIXME: get rid of ugly names when typedef and primrec respect qualification*)
   1.230 +fun mk_version_binding_ugly version = Binding.suffix_name ("_v" ^ string_of_int version);
   1.231 +fun mk_version_fp_binding_ugly internal ctxt version fp_b pre =
   1.232 +  Binding.prefix_name (pre ^ "_") fp_b
   1.233 +  |> mk_version_binding_ugly version
   1.234 +  |> mk_internal internal ctxt Binding.concealed;
   1.235 +
   1.236 +fun mk_mapN ctxt live_AsBs TA bnf =
   1.237 +  let val TB = Term.typ_subst_atomic live_AsBs TA in
   1.238 +    enforce_type ctxt (snd o strip_typeN (length live_AsBs)) (TA --> TB) (map_of_bnf bnf)
   1.239 +  end;
   1.240 +
   1.241 +fun mk_relN ctxt live_AsBs TA bnf =
   1.242 +  let val TB = Term.typ_subst_atomic live_AsBs TA in
   1.243 +    enforce_type ctxt (snd o strip_typeN (length live_AsBs)) (mk_pred2T TA TB) (rel_of_bnf bnf)
   1.244 +  end;
   1.245 +
   1.246 +fun mk_map1 ctxt Y Z = mk_mapN ctxt [(Y, Z)];
   1.247 +fun mk_rel1 ctxt Y Z = mk_relN ctxt [(Y, Z)];
   1.248 +
   1.249 +fun define_const internal fp_b version name rhs lthy =
   1.250 +  let
   1.251 +    val b = mk_version_fp_binding internal lthy version fp_b name;
   1.252 +
   1.253 +    val ((free, (_, def_free)), (lthy, lthy_old)) = lthy
   1.254 +      |> Local_Theory.open_target |> snd
   1.255 +      |> Local_Theory.define ((b, NoSyn), ((Thm.def_binding b |> Binding.concealed, []), rhs))
   1.256 +      ||> `Local_Theory.close_target;
   1.257 +
   1.258 +    val phi = Proof_Context.export_morphism lthy_old lthy;
   1.259 +
   1.260 +    val const = Morphism.term phi free;
   1.261 +    val const' = enforce_type lthy I (fastype_of free) const;
   1.262 +  in
   1.263 +    ((const', Morphism.thm phi def_free), lthy)
   1.264 +  end;
   1.265 +
   1.266 +fun define_single_primrec b eqs lthy =
   1.267 +  let
   1.268 +    val (([free], [def_free], [simps_free]), (lthy, lthy_old)) = lthy
   1.269 +      |> Local_Theory.open_target |> snd
   1.270 +      |> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed) (*TODO check*)
   1.271 +      |> primrec [(b, NONE, NoSyn)] (map (pair Attrib.empty_binding) eqs)
   1.272 +      ||> `Local_Theory.close_target;
   1.273 +
   1.274 +    val phi = Proof_Context.export_morphism lthy_old lthy;
   1.275 +
   1.276 +    val const = Morphism.term phi free;
   1.277 +    val const' = enforce_type lthy I (fastype_of free) const;
   1.278 +  in
   1.279 +    ((const', Morphism.thm phi def_free, map (Morphism.thm phi) simps_free), lthy)
   1.280 +  end;
   1.281 +
   1.282 +type buffer =
   1.283 +  {Oper: term,
   1.284 +   VLeaf: term,
   1.285 +   CLeaf: term,
   1.286 +   ctr_wrapper: term,
   1.287 +   friends: (typ * term) Symtab.table};
   1.288 +
   1.289 +fun map_buffer f {Oper, VLeaf, CLeaf, ctr_wrapper, friends} =
   1.290 +  {Oper = f Oper, VLeaf = f VLeaf, CLeaf = f CLeaf, ctr_wrapper = f ctr_wrapper,
   1.291 +   friends = Symtab.map (K (apsnd f)) friends};
   1.292 +
   1.293 +fun morph_buffer phi = map_buffer (Morphism.term phi);
   1.294 +
   1.295 +fun specialize_buffer_types {Oper, VLeaf, CLeaf, ctr_wrapper, friends} =
   1.296 +  let
   1.297 +    val ssig_T as Type (_, Ts) = body_type (fastype_of VLeaf);
   1.298 +    val Y = List.last Ts;
   1.299 +    val ssigifyT = substT Y ssig_T;
   1.300 +  in
   1.301 +    {Oper = Oper, VLeaf = VLeaf, CLeaf = CLeaf, ctr_wrapper = ssigifyT ctr_wrapper,
   1.302 +     friends = Symtab.map (K (apsnd ssigifyT)) friends}
   1.303 +  end;
   1.304 +
   1.305 +type dtor_coinduct_info =
   1.306 +  {dtor_coinduct: thm,
   1.307 +   cong_def: thm,
   1.308 +   cong_locale: thm,
   1.309 +   cong_base: thm,
   1.310 +   cong_refl: thm,
   1.311 +   cong_sym: thm,
   1.312 +   cong_trans: thm,
   1.313 +   cong_alg_intros: thm list};
   1.314 +
   1.315 +fun map_dtor_coinduct_info f {dtor_coinduct, cong_def, cong_locale, cong_base, cong_refl, cong_sym,
   1.316 +    cong_trans, cong_alg_intros} =
   1.317 +  {dtor_coinduct = f dtor_coinduct, cong_def = f cong_def, cong_locale = f cong_locale,
   1.318 +   cong_base = f cong_base, cong_refl = f cong_refl, cong_sym = f cong_sym,
   1.319 +   cong_trans = f cong_trans, cong_alg_intros = map f cong_alg_intros};
   1.320 +
   1.321 +fun morph_dtor_coinduct_info phi = map_dtor_coinduct_info (Morphism.thm phi);
   1.322 +
   1.323 +type corec_ad =
   1.324 +  {fpT: typ,
   1.325 +   friend_names: string list};
   1.326 +
   1.327 +fun morph_corec_ad phi {fpT, friend_names} =
   1.328 +  {fpT = Morphism.typ phi fpT, friend_names = friend_names};
   1.329 +
   1.330 +type corec_info =
   1.331 +  {fp_b: binding,
   1.332 +   version: int,
   1.333 +   fpT: typ,
   1.334 +   Y: typ,
   1.335 +   Z: typ,
   1.336 +   friend_names: string list,
   1.337 +   sig_fp_sugars: fp_sugar list,
   1.338 +   ssig_fp_sugar: fp_sugar,
   1.339 +   Lam: term,
   1.340 +   proto_sctr: term,
   1.341 +   flat: term,
   1.342 +   eval_core: term,
   1.343 +   eval: term,
   1.344 +   algLam: term,
   1.345 +   corecUU: term,
   1.346 +   dtor_transfer: thm,
   1.347 +   Lam_transfer: thm,
   1.348 +   Lam_pointful_natural: thm,
   1.349 +   proto_sctr_transfer: thm,
   1.350 +   flat_simps: thm list,
   1.351 +   eval_core_simps: thm list,
   1.352 +   eval_thm: thm,
   1.353 +   eval_simps: thm list,
   1.354 +   all_algLam_algs: thm list,
   1.355 +   algLam_thm: thm,
   1.356 +   dtor_algLam: thm,
   1.357 +   corecUU_thm: thm,
   1.358 +   corecUU_unique: thm,
   1.359 +   corecUU_transfer: thm,
   1.360 +   buffer: buffer,
   1.361 +   all_dead_k_bnfs: BNF_Def.bnf list,
   1.362 +   Retr: term,
   1.363 +   equivp_Retr: thm,
   1.364 +   Retr_coinduct: thm,
   1.365 +   dtor_coinduct_info: dtor_coinduct_info};
   1.366 +
   1.367 +fun morph_corec_info phi
   1.368 +    ({fp_b, version, fpT, Y, Z, friend_names, sig_fp_sugars, ssig_fp_sugar, Lam, proto_sctr, flat,
   1.369 +      eval_core, eval, algLam, corecUU, dtor_transfer, Lam_transfer, Lam_pointful_natural,
   1.370 +      proto_sctr_transfer, flat_simps, eval_core_simps, eval_thm, eval_simps, all_algLam_algs,
   1.371 +      algLam_thm, dtor_algLam, corecUU_thm, corecUU_unique, corecUU_transfer, buffer,
   1.372 +      all_dead_k_bnfs, Retr, equivp_Retr, Retr_coinduct, dtor_coinduct_info} : corec_info) =
   1.373 +  {fp_b = fp_b, version = version, fpT = Morphism.typ phi fpT, Y = Morphism.typ phi Y,
   1.374 +   Z = Morphism.typ phi Z, friend_names = friend_names, sig_fp_sugars = sig_fp_sugars (*no morph*),
   1.375 +   ssig_fp_sugar = ssig_fp_sugar (*no morph*), Lam = Morphism.term phi Lam,
   1.376 +   proto_sctr = Morphism.term phi proto_sctr, flat = Morphism.term phi flat,
   1.377 +   eval_core = Morphism.term phi eval_core, eval = Morphism.term phi eval,
   1.378 +   algLam = Morphism.term phi algLam, corecUU = Morphism.term phi corecUU,
   1.379 +   dtor_transfer = dtor_transfer, Lam_transfer = Morphism.thm phi Lam_transfer,
   1.380 +   Lam_pointful_natural = Morphism.thm phi Lam_pointful_natural,
   1.381 +   proto_sctr_transfer = Morphism.thm phi proto_sctr_transfer,
   1.382 +   flat_simps = map (Morphism.thm phi) flat_simps,
   1.383 +   eval_core_simps = map (Morphism.thm phi) eval_core_simps, eval_thm = Morphism.thm phi eval_thm,
   1.384 +   eval_simps = map (Morphism.thm phi) eval_simps,
   1.385 +   all_algLam_algs = map (Morphism.thm phi) all_algLam_algs,
   1.386 +   algLam_thm = Morphism.thm phi algLam_thm, dtor_algLam = Morphism.thm phi dtor_algLam,
   1.387 +   corecUU_thm = Morphism.thm phi corecUU_thm, corecUU_unique = Morphism.thm phi corecUU_unique,
   1.388 +   corecUU_transfer = Morphism.thm phi corecUU_transfer, buffer = morph_buffer phi buffer,
   1.389 +   all_dead_k_bnfs = map (morph_bnf phi) all_dead_k_bnfs, Retr = Morphism.term phi Retr,
   1.390 +   equivp_Retr = Morphism.thm phi equivp_Retr, Retr_coinduct = Morphism.thm phi Retr_coinduct,
   1.391 +   dtor_coinduct_info = morph_dtor_coinduct_info phi dtor_coinduct_info};
   1.392 +
   1.393 +datatype ('a, 'b) expr =
   1.394 +  Ad of 'a * (local_theory -> 'b * local_theory) |
   1.395 +  Info of 'b;
   1.396 +
   1.397 +fun is_Ad (Ad _) = true
   1.398 +  | is_Ad _ = false;
   1.399 +
   1.400 +fun is_Info (Info _) = true
   1.401 +  | is_Info _ = false;
   1.402 +
   1.403 +type corec_info_expr = (corec_ad, corec_info) expr;
   1.404 +
   1.405 +fun morph_corec_info_expr phi (Ad (ad, f)) = Ad (morph_corec_ad phi ad, f)
   1.406 +  | morph_corec_info_expr phi (Info info) = Info (morph_corec_info phi info);
   1.407 +
   1.408 +val transfer_corec_info_expr = morph_corec_info_expr o Morphism.transfer_morphism;
   1.409 +
   1.410 +type corec_data = int Symtab.table * corec_info_expr list Symtab.table list;
   1.411 +
   1.412 +structure Data = Generic_Data
   1.413 +(
   1.414 +  type T = corec_data;
   1.415 +  val empty = (Symtab.empty, [Symtab.empty]);
   1.416 +  val extend = I;
   1.417 +  fun merge ((version_tab1, info_tabs1), (version_tab2, info_tabs2)) : T =
   1.418 +    (Symtab.join (K Int.max) (version_tab1, version_tab2), info_tabs1 @ info_tabs2);
   1.419 +);
   1.420 +
   1.421 +fun corec_ad_of_expr (Ad (ad, _)) = ad
   1.422 +  | corec_ad_of_expr (Info {fpT, friend_names, ...}) = {fpT = fpT, friend_names = friend_names};
   1.423 +
   1.424 +fun corec_info_exprs_of_generic context fpT_name =
   1.425 +  let
   1.426 +    val thy = Context.theory_of context;
   1.427 +    val info_tabs = snd (Data.get context);
   1.428 +  in
   1.429 +    maps (fn info_tab => these (Symtab.lookup info_tab fpT_name)) info_tabs
   1.430 +    |> map (transfer_corec_info_expr thy)
   1.431 +  end;
   1.432 +
   1.433 +val corec_info_exprs_of = corec_info_exprs_of_generic o Context.Proof;
   1.434 +
   1.435 +val keep_corec_infos = map_filter (fn Ad _ => NONE | Info info => SOME info);
   1.436 +
   1.437 +val corec_infos_of_generic = keep_corec_infos oo corec_info_exprs_of_generic;
   1.438 +val corec_infos_of = keep_corec_infos oo corec_info_exprs_of;
   1.439 +
   1.440 +fun str_of_corec_ad ctxt {fpT, friend_names} =
   1.441 +  "[" ^ Syntax.string_of_typ ctxt fpT ^ "; " ^ commas friend_names ^ "]";
   1.442 +
   1.443 +fun str_of_corec_info ctxt {fpT, version, friend_names, ...} =
   1.444 +  "{" ^ Syntax.string_of_typ ctxt fpT ^ "; " ^ commas friend_names ^ "; v" ^ string_of_int version ^
   1.445 +  "}";
   1.446 +
   1.447 +fun str_of_corec_info_expr ctxt (Ad (ad, _)) = str_of_corec_ad ctxt ad
   1.448 +  | str_of_corec_info_expr ctxt (Info info) = str_of_corec_info ctxt info;
   1.449 +
   1.450 +fun print_corec_infos ctxt =
   1.451 +  Symtab.fold (fn (fpT_name, exprs) => fn () =>
   1.452 +      writeln (fpT_name ^ ":\n" ^
   1.453 +        cat_lines (map (prefix "  " o str_of_corec_info_expr ctxt) exprs)))
   1.454 +    (the_single (snd (Data.get (Context.Proof ctxt)))) ();
   1.455 +
   1.456 +val has_no_corec_info = null oo corec_info_exprs_of;
   1.457 +
   1.458 +fun get_name_next_version_of fpT_name ctxt =
   1.459 +  let
   1.460 +    val (version_tab, info_tabs) = Data.get (Context.Theory (Proof_Context.theory_of ctxt));
   1.461 +    val fp_base = Long_Name.base_name fpT_name;
   1.462 +    val fp_b = Binding.name fp_base;
   1.463 +    val version_tab' = Symtab.map_default (fp_base, ~1) (Integer.add 1) version_tab;
   1.464 +    val SOME version = Symtab.lookup version_tab' fp_base;
   1.465 +    val ctxt' = ctxt
   1.466 +      |> Local_Theory.background_theory (Context.theory_map (Data.put (version_tab', info_tabs)));
   1.467 +  in
   1.468 +    ((fp_b, version), ctxt')
   1.469 +  end;
   1.470 +
   1.471 +type friend_info =
   1.472 +  {algrho: term,
   1.473 +   dtor_algrho: thm,
   1.474 +   algLam_algrho: thm};
   1.475 +
   1.476 +fun morph_friend_info phi ({algrho, dtor_algrho, algLam_algrho} : friend_info) =
   1.477 +  {algrho = Morphism.term phi algrho, dtor_algrho = Morphism.thm phi dtor_algrho,
   1.478 +   algLam_algrho = Morphism.thm phi algLam_algrho};
   1.479 +
   1.480 +fun checked_fp_sugar_of ctxt fpT_name =
   1.481 +  let
   1.482 +    val fp_sugar as {X, fp_res = {Ts = fpTs, ...}, fp_ctr_sugar = {ctrXs_Tss, ...}, ...} =
   1.483 +      (case fp_sugar_of ctxt fpT_name of
   1.484 +        SOME (fp_sugar as {fp = Greatest_FP, ...}) => fp_sugar
   1.485 +      | _ => not_codatatype ctxt (Type (fpT_name, [] (*yuck*))));
   1.486 +
   1.487 +    val _ =
   1.488 +      if length fpTs > 1 then
   1.489 +        mutual_codatatype ()
   1.490 +      else if not (exists (exists (Term.exists_subtype (curry (op =) X))) ctrXs_Tss) then
   1.491 +        noncorecursive_codatatype ()
   1.492 +      else if ctrXs_Tss = [[X]] then
   1.493 +        singleton_codatatype ctxt
   1.494 +      else
   1.495 +        ();
   1.496 +  in
   1.497 +    fp_sugar
   1.498 +  end;
   1.499 +
   1.500 +fun inline_pre_bnfs f lthy =
   1.501 +  lthy
   1.502 +  |> Config.put typedef_threshold ~1
   1.503 +  |> f
   1.504 +  |> Config.put typedef_threshold (Config.get lthy typedef_threshold);
   1.505 +
   1.506 +fun bnf_kill_all_but nn bnf lthy =
   1.507 +  ((empty_comp_cache, empty_unfolds), lthy)
   1.508 +  |> kill_bnf I (live_of_bnf bnf - nn) bnf
   1.509 +  ||> snd;
   1.510 +
   1.511 +fun bnf_with_deads_and_lives dead_Es live_As Y fpT T lthy =
   1.512 +   let
   1.513 +     val qsoty = quote o Syntax.string_of_typ lthy;
   1.514 +
   1.515 +     val unfreeze_fp = Tsubst Y fpT;
   1.516 +
   1.517 +    fun flatten_tyargs Ass =
   1.518 +      map dest_TFree live_As
   1.519 +      |> filter (fn T => exists (fn Ts => member (op =) Ts T) Ass);
   1.520 +
   1.521 +     val ((bnf, _), (_, lthy)) =
   1.522 +      bnf_of_typ false Do_Inline I flatten_tyargs [Term.dest_TFree Y]
   1.523 +        (map Term.dest_TFree dead_Es) T ((empty_comp_cache, empty_unfolds), lthy)
   1.524 +      handle BAD_DEAD (Y, Y_backdrop) =>
   1.525 +        (case Y_backdrop of
   1.526 +          Type (bad_tc, _) =>
   1.527 +          let
   1.528 +            val T = qsoty (unfreeze_fp Y);
   1.529 +            val T_backdrop = qsoty (unfreeze_fp Y_backdrop);
   1.530 +            fun register_hint () =
   1.531 +              "\nUse the " ^ quote (#1 @{command_keyword "bnf"}) ^ " command to register " ^
   1.532 +              quote bad_tc ^ " as a bounded natural functor to allow nested (co)recursion through \
   1.533 +              \it";
   1.534 +          in
   1.535 +            if is_some (bnf_of lthy bad_tc) orelse is_some (fp_sugar_of lthy bad_tc) then
   1.536 +              error ("Inadmissible occurrence of type " ^ T ^ " in type expression " ^
   1.537 +                T_backdrop)
   1.538 +            else
   1.539 +              error ("Unsupported occurrence of type " ^ T ^ " via type constructor " ^
   1.540 +                quote bad_tc ^ " in type expression " ^ T_backdrop ^ register_hint ())
   1.541 +          end);
   1.542 +
   1.543 +    val phi =
   1.544 +      Morphism.term_morphism "BNF" (Raw_Simplifier.rewrite_term (Proof_Context.theory_of lthy)
   1.545 +        @{thms BNF_Composition.id_bnf_def} [])
   1.546 +      $> Morphism.thm_morphism "BNF" (unfold_thms lthy @{thms BNF_Composition.id_bnf_def});
   1.547 +  in
   1.548 +    (morph_bnf phi bnf, lthy)
   1.549 +  end;
   1.550 +
   1.551 +fun define_sig_type fp_b version fp_alives Es Y rhsT lthy =
   1.552 +  let
   1.553 +    val T_b = mk_version_fp_binding_ugly true lthy version fp_b sigN;
   1.554 +    val ctr_b = mk_version_fp_binding false lthy version fp_b SigN;
   1.555 +    val sel_b = mk_version_fp_binding true lthy version fp_b unsigN;
   1.556 +
   1.557 +    val lthy = Local_Theory.open_target lthy |> snd;
   1.558 +
   1.559 +    val T_name = Local_Theory.full_name lthy T_b;
   1.560 +
   1.561 +    val tyargs = map2 (fn alive => pair (if alive then SOME Binding.empty else NONE)
   1.562 +      o rpair @{sort type}) (fp_alives @ [true]) (Es @ [Y]);
   1.563 +    val ctr_specs = [(((Binding.empty, ctr_b), [(sel_b, rhsT)]), NoSyn)];
   1.564 +    val spec = (((((tyargs, T_b), NoSyn), ctr_specs),
   1.565 +      (Binding.empty, Binding.empty, Binding.empty)), []);
   1.566 +
   1.567 +    val plugins = Plugin_Name.make_filter lthy (K (curry (op =) transfer_plugin));
   1.568 +    val discs_sels = true;
   1.569 +
   1.570 +    val lthy = lthy
   1.571 +      |> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed) (*TODO check*)
   1.572 +      |> inline_pre_bnfs (co_datatypes Least_FP construct_lfp ((plugins, discs_sels), [spec]))
   1.573 +      |> Local_Theory.close_target;
   1.574 +
   1.575 +    val SOME fp_sugar = fp_sugar_of lthy T_name;
   1.576 +  in
   1.577 +    (fp_sugar, lthy)
   1.578 +  end;
   1.579 +
   1.580 +fun define_ssig_type fp_b version fp_alives Es Y fpT lthy =
   1.581 +  let
   1.582 +    val sig_T_b = mk_version_fp_binding_ugly true lthy version fp_b sigN;
   1.583 +    val T_b = Binding.prefix_name s_prefix sig_T_b;
   1.584 +    val Oper_b = mk_version_fp_binding false lthy version fp_b OperN;
   1.585 +    val VLeaf_b = mk_version_fp_binding false lthy version fp_b VLeafN;
   1.586 +    val CLeaf_b = mk_version_fp_binding false lthy version fp_b CLeafN;
   1.587 +
   1.588 +    val lthy = Local_Theory.open_target lthy |> snd;
   1.589 +
   1.590 +    val sig_T_name = Local_Theory.full_name lthy sig_T_b;
   1.591 +    val T_name = Long_Name.map_base_name (prefix s_prefix) sig_T_name;
   1.592 +
   1.593 +    val As = Es @ [Y];
   1.594 +    val ssig_sig_T = Type (sig_T_name, Es @ [Type (T_name, As)]);
   1.595 +
   1.596 +    val tyargs = map2 (fn alive => pair (if alive then SOME Binding.empty else NONE)
   1.597 +      o rpair @{sort type}) (fp_alives @ [true]) As;
   1.598 +    val ctr_specs =
   1.599 +      [(((Binding.empty, Oper_b), [(Binding.empty, ssig_sig_T)]), NoSyn),
   1.600 +       (((Binding.empty, VLeaf_b), [(Binding.empty, Y)]), NoSyn),
   1.601 +       (((Binding.empty, CLeaf_b), [(Binding.empty, fpT)]), NoSyn)];
   1.602 +    val spec = (((((tyargs, T_b), NoSyn), ctr_specs),
   1.603 +      (Binding.empty, Binding.empty, Binding.empty)), []);
   1.604 +
   1.605 +    val plugins = Plugin_Name.make_filter lthy (K (curry (op =) transfer_plugin));
   1.606 +    val discs_sels = false;
   1.607 +
   1.608 +    val lthy = lthy
   1.609 +      |> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed) (*TODO check*)
   1.610 +      |> inline_pre_bnfs (co_datatypes Least_FP construct_lfp ((plugins, discs_sels), [spec]))
   1.611 +      |> Local_Theory.close_target;
   1.612 +
   1.613 +    val SOME fp_sugar = fp_sugar_of lthy T_name;
   1.614 +  in
   1.615 +    (fp_sugar, lthy)
   1.616 +  end;
   1.617 +
   1.618 +fun embed_Sig ctxt Sig inl_or_r t =
   1.619 +  Library.foldl1 HOLogic.mk_comp [Sig, inl_or_r, dummify_atomic_types t]
   1.620 +  |> Syntax.check_term ctxt;
   1.621 +
   1.622 +fun mk_ctr_wrapper_friends ctxt friend_name friend_T old_sig_T k_T Sig old_buffer =
   1.623 +  let
   1.624 +    val embed_Sig_inl = embed_Sig ctxt Sig (Inl_const old_sig_T k_T);
   1.625 +
   1.626 +    val ctr_wrapper = embed_Sig_inl (#ctr_wrapper old_buffer);
   1.627 +    val friends = Symtab.map (K (apsnd embed_Sig_inl)) (#friends old_buffer)
   1.628 +      |> Symtab.update_new (friend_name, (friend_T,
   1.629 +        HOLogic.mk_comp (Sig, Inr_const old_sig_T k_T)));
   1.630 +  in
   1.631 +    (ctr_wrapper, friends)
   1.632 +  end;
   1.633 +
   1.634 +fun pre_type_of_ctor Y ctor =
   1.635 +  let
   1.636 +    val (fp_preT, fpT) = dest_funT (fastype_of ctor);
   1.637 +  in
   1.638 +    typ_subst_nonatomic [(fpT, Y)] fp_preT
   1.639 +  end;
   1.640 +
   1.641 +fun mk_k_as_ssig Z old_sig_T k_T ssig_T Sig dead_sig_map Oper VLeaf =
   1.642 +  let
   1.643 +    val inr' = Inr_const old_sig_T k_T;
   1.644 +    val dead_sig_map' = substT Z ssig_T dead_sig_map;
   1.645 +  in
   1.646 +    Library.foldl1 HOLogic.mk_comp [Oper, dead_sig_map' $ VLeaf, Sig, inr']
   1.647 +  end;
   1.648 +
   1.649 +fun define_embL name fp_b version Y Z fpT old_sig_T old_ssig_T other_summand_T ssig_T Inl_or_r_const
   1.650 +    dead_old_sig_map Sig old_Oper old_VLeaf old_CLeaf Oper VLeaf CLeaf lthy =
   1.651 +  let
   1.652 +    val embL_b = mk_version_fp_binding true lthy version fp_b name;
   1.653 +    val old_ssig_old_sig_T = Tsubst Y old_ssig_T old_sig_T;
   1.654 +    val ssig_old_sig_T = Tsubst Y ssig_T old_sig_T;
   1.655 +    val ssig_other_summand_T = Tsubst Y ssig_T other_summand_T;
   1.656 +
   1.657 +    val sigx = Var (("s", 0), old_ssig_old_sig_T);
   1.658 +    val x = Var (("x", 0), Y);
   1.659 +    val j = Var (("j", 0), fpT);
   1.660 +    val embL = Free (Binding.name_of embL_b, old_ssig_T --> ssig_T);
   1.661 +    val dead_old_sig_map' = Term.subst_atomic_types [(Y, old_ssig_T), (Z, ssig_T)] dead_old_sig_map;
   1.662 +    val Sig' = substT Y ssig_T Sig;
   1.663 +    val inl' = Inl_or_r_const ssig_old_sig_T ssig_other_summand_T;
   1.664 +
   1.665 +    val Oper_eq = mk_Trueprop_eq (embL $ (old_Oper $ sigx),
   1.666 +        Oper $ (Sig' $ (inl' $ (dead_old_sig_map' $ embL $ sigx))))
   1.667 +      |> Logic.all sigx;
   1.668 +    val VLeaf_eq = mk_Trueprop_eq (embL $ (old_VLeaf $ x), VLeaf $ x)
   1.669 +      |> Logic.all x;
   1.670 +    val CLeaf_eq = mk_Trueprop_eq (embL $ (old_CLeaf $ j), CLeaf $ j)
   1.671 +      |> Logic.all j;
   1.672 +  in
   1.673 +    define_single_primrec embL_b [Oper_eq, VLeaf_eq, CLeaf_eq] lthy
   1.674 +  end;
   1.675 +
   1.676 +fun define_Lam_base fp_b version Y Z preT ssig_T dead_pre_map Sig unsig dead_sig_map Oper VLeaf
   1.677 +    lthy =
   1.678 +  let
   1.679 +    val YpreT = HOLogic.mk_prodT (Y, preT);
   1.680 +
   1.681 +    val snd' = snd_const YpreT;
   1.682 +    val dead_pre_map' = substT Z ssig_T dead_pre_map;
   1.683 +    val Sig' = substT Y ssig_T Sig;
   1.684 +    val unsig' = substT Y ssig_T unsig;
   1.685 +    val dead_sig_map' = Term.subst_atomic_types [(Y, YpreT), (Z, ssig_T)] dead_sig_map;
   1.686 +
   1.687 +    val rhs = HOLogic.mk_comp (unsig', dead_sig_map'
   1.688 +      $ Library.foldl1 HOLogic.mk_comp [Oper, Sig', dead_pre_map' $ VLeaf, snd']);
   1.689 +  in
   1.690 +    define_const true fp_b version LamN rhs lthy
   1.691 +  end;
   1.692 +
   1.693 +fun define_Lam_step_or_merge fp_b version Y preT unsig left_case right_case lthy =
   1.694 +  let
   1.695 +    val YpreT = HOLogic.mk_prodT (Y, preT);
   1.696 +
   1.697 +    val unsig' = substT Y YpreT unsig;
   1.698 +
   1.699 +    val rhs = HOLogic.mk_comp (mk_case_sum (left_case, right_case), unsig');
   1.700 +  in
   1.701 +    define_const true fp_b version LamN rhs lthy
   1.702 +  end;
   1.703 +
   1.704 +fun define_Lam_step fp_b version Y Z preT old_ssig_T ssig_T dead_pre_map unsig rho embL old_Lam
   1.705 +    lthy =
   1.706 +  let
   1.707 +    val dead_pre_map' = Term.subst_atomic_types [(Y, old_ssig_T), (Z, ssig_T)] dead_pre_map;
   1.708 +    val left_case = HOLogic.mk_comp (dead_pre_map' $ embL, old_Lam);
   1.709 +  in
   1.710 +    define_Lam_step_or_merge fp_b version Y preT unsig left_case rho lthy
   1.711 +  end;
   1.712 +
   1.713 +fun define_Lam_merge fp_b version Y Z preT old1_ssig_T old2_ssig_T ssig_T dead_pre_map unsig embLL
   1.714 +    embLR old1_Lam old2_Lam lthy =
   1.715 +  let
   1.716 +    val dead_pre_map' = Term.subst_atomic_types [(Y, old1_ssig_T), (Z, ssig_T)] dead_pre_map;
   1.717 +    val dead_pre_map'' = Term.subst_atomic_types [(Y, old2_ssig_T), (Z, ssig_T)] dead_pre_map;
   1.718 +    val left_case = HOLogic.mk_comp (dead_pre_map' $ embLL, old1_Lam);
   1.719 +    val right_case = HOLogic.mk_comp (dead_pre_map'' $ embLR, old2_Lam);
   1.720 +  in
   1.721 +    define_Lam_step_or_merge fp_b version Y preT unsig left_case right_case lthy
   1.722 +  end;
   1.723 +
   1.724 +fun define_proto_sctr_step_or_merge fp_b version old_sig_T right_T Sig old_proto_sctr =
   1.725 +  let
   1.726 +    val rhs = Library.foldl1 HOLogic.mk_comp [Sig, Inl_const old_sig_T right_T, old_proto_sctr];
   1.727 +  in
   1.728 +    define_const true fp_b version proto_sctrN rhs
   1.729 +  end;
   1.730 +
   1.731 +fun define_flat fp_b version Y Z fpT sig_T ssig_T Oper VLeaf CLeaf dead_sig_map lthy =
   1.732 +  let
   1.733 +    val flat_b = mk_version_fp_binding true lthy version fp_b flatN;
   1.734 +    val ssig_sig_T = Tsubst Y ssig_T sig_T;
   1.735 +    val ssig_ssig_sig_T = Tsubst Y ssig_T ssig_sig_T;
   1.736 +    val ssig_ssig_T = Tsubst Y ssig_T ssig_T;
   1.737 +
   1.738 +    val sigx = Var (("s", 0), ssig_ssig_sig_T);
   1.739 +    val x = Var (("x", 0), ssig_T);
   1.740 +    val j = Var (("j", 0), fpT);
   1.741 +    val flat = Free (Binding.name_of flat_b, ssig_ssig_T --> ssig_T);
   1.742 +    val Oper' = substT Y ssig_T Oper;
   1.743 +    val VLeaf' = substT Y ssig_T VLeaf;
   1.744 +    val CLeaf' = substT Y ssig_T CLeaf;
   1.745 +    val dead_sig_map' = Term.subst_atomic_types [(Y, ssig_ssig_T), (Z, ssig_T)] dead_sig_map;
   1.746 +
   1.747 +    val Oper_eq = mk_Trueprop_eq (flat $ (Oper' $ sigx), Oper $ (dead_sig_map' $ flat $ sigx))
   1.748 +      |> Logic.all sigx;
   1.749 +    val VLeaf_eq = mk_Trueprop_eq (flat $ (VLeaf' $ x), x)
   1.750 +      |> Logic.all x;
   1.751 +    val CLeaf_eq = mk_Trueprop_eq (flat $ (CLeaf' $ j), CLeaf $ j)
   1.752 +      |> Logic.all j;
   1.753 +  in
   1.754 +    define_single_primrec flat_b [Oper_eq, VLeaf_eq, CLeaf_eq] lthy
   1.755 +  end;
   1.756 +
   1.757 +fun define_eval_core fp_b version Y Z preT fpT sig_T ssig_T dtor Oper VLeaf CLeaf dead_pre_map
   1.758 +    dead_sig_map dead_ssig_map flat Lam lthy =
   1.759 +  let
   1.760 +    val eval_core_b = mk_version_fp_binding true lthy version fp_b eval_coreN;
   1.761 +    val YpreT = HOLogic.mk_prodT (Y, preT);
   1.762 +    val Ypre_ssig_T = Tsubst Y YpreT ssig_T;
   1.763 +    val Ypre_ssig_sig_T = Tsubst Y Ypre_ssig_T sig_T;
   1.764 +    val ssig_preT = Tsubst Y ssig_T preT;
   1.765 +    val ssig_YpreT = Tsubst Y ssig_T YpreT;
   1.766 +    val ssig_ssig_T = Tsubst Y ssig_T ssig_T;
   1.767 +
   1.768 +    val sigx = Var (("s", 0), Ypre_ssig_sig_T);
   1.769 +    val x = Var (("x", 0), YpreT);
   1.770 +    val j = Var (("j", 0), fpT);
   1.771 +    val eval_core = Free (Binding.name_of eval_core_b, Ypre_ssig_T --> ssig_preT);
   1.772 +    val Oper' = substT Y YpreT Oper;
   1.773 +    val VLeaf' = substT Y YpreT VLeaf;
   1.774 +    val CLeaf' = substT Y YpreT CLeaf;
   1.775 +    val dead_pre_map' = Term.subst_atomic_types [(Y, ssig_ssig_T), (Z, ssig_T)] dead_pre_map;
   1.776 +    val dead_pre_map'' = substT Z ssig_T dead_pre_map;
   1.777 +    val dead_pre_map''' = Term.subst_atomic_types [(Y, fpT), (Z, ssig_T)] dead_pre_map;
   1.778 +    val dead_sig_map' = Term.subst_atomic_types [(Y, Ypre_ssig_T), (Z, ssig_YpreT)] dead_sig_map;
   1.779 +    val dead_ssig_map' = Term.subst_atomic_types [(Y, YpreT), (Z, Y)] dead_ssig_map;
   1.780 +    val Lam' = substT Y ssig_T Lam;
   1.781 +    val fst' = fst_const YpreT;
   1.782 +    val snd' = snd_const YpreT;
   1.783 +
   1.784 +    val Oper_eq = mk_Trueprop_eq (eval_core $ (Oper' $ sigx),
   1.785 +        dead_pre_map' $ flat $ (Lam' $ (dead_sig_map' $ (Abs (Name.uu, Ypre_ssig_T,
   1.786 +          HOLogic.mk_prod (dead_ssig_map' $ fst' $ Bound 0, eval_core $ Bound 0))) $ sigx)))
   1.787 +      |> Logic.all sigx;
   1.788 +    val VLeaf_eq = mk_Trueprop_eq (eval_core $ (VLeaf' $ x), dead_pre_map'' $ VLeaf $ (snd' $ x))
   1.789 +      |> Logic.all x;
   1.790 +    val CLeaf_eq = mk_Trueprop_eq (eval_core $ (CLeaf' $ j), dead_pre_map''' $ CLeaf $ (dtor $ j))
   1.791 +      |> Logic.all j;
   1.792 +  in
   1.793 +    define_single_primrec eval_core_b [Oper_eq, VLeaf_eq, CLeaf_eq] lthy
   1.794 +  end;
   1.795 +
   1.796 +fun define_eval fp_b version Y Z preT fpT ssig_T dtor dtor_unfold dead_ssig_map eval_core lthy =
   1.797 +  let
   1.798 +    val fp_preT = Tsubst Y fpT preT;
   1.799 +    val fppreT = HOLogic.mk_prodT (fpT, fp_preT);
   1.800 +    val fp_ssig_T = Tsubst Y fpT ssig_T;
   1.801 +
   1.802 +    val dtor_unfold' = substT Z fp_ssig_T dtor_unfold;
   1.803 +    val dead_ssig_map' = Term.subst_atomic_types [(Y, fpT), (Z, fppreT)] dead_ssig_map;
   1.804 +    val eval_core' = substT Y fpT eval_core;
   1.805 +    val id' = HOLogic.id_const fpT;
   1.806 +
   1.807 +    val rhs = dtor_unfold' $ HOLogic.mk_comp (eval_core', dead_ssig_map' $ mk_convol (id', dtor));
   1.808 +  in
   1.809 +    define_const true fp_b version evalN rhs lthy
   1.810 +  end;
   1.811 +
   1.812 +fun define_cutSsig fp_b version Y Z preT ssig_T dead_pre_map VLeaf dead_ssig_map flat eval_core
   1.813 +    lthy =
   1.814 +  let
   1.815 +    val ssig_preT = Tsubst Y ssig_T preT;
   1.816 +    val ssig_ssig_T = Tsubst Y ssig_T ssig_T;
   1.817 +    val ssig_ssig_preT = HOLogic.mk_prodT (ssig_T, ssig_preT);
   1.818 +
   1.819 +    val h = Var (("h", 0), Y --> ssig_preT);
   1.820 +    val dead_pre_map' = Term.subst_atomic_types [(Y, ssig_ssig_T), (Z, ssig_T)] dead_pre_map;
   1.821 +    val dead_ssig_map' = substT Z ssig_ssig_preT dead_ssig_map;
   1.822 +    val eval_core' = substT Y ssig_T eval_core;
   1.823 +
   1.824 +    val rhs = Library.foldl1 HOLogic.mk_comp [dead_pre_map' $ flat, eval_core',
   1.825 +        dead_ssig_map' $ mk_convol (VLeaf, h)]
   1.826 +      |> Term.lambda h;
   1.827 +  in
   1.828 +    define_const true fp_b version cutSsigN rhs lthy
   1.829 +  end;
   1.830 +
   1.831 +fun define_algLam fp_b version Y Z fpT ssig_T Oper VLeaf dead_sig_map eval lthy =
   1.832 +  let
   1.833 +    val fp_ssig_T = Tsubst Y fpT ssig_T;
   1.834 +
   1.835 +    val Oper' = substT Y fpT Oper;
   1.836 +    val VLeaf' = substT Y fpT VLeaf;
   1.837 +    val dead_sig_map' = Term.subst_atomic_types [(Y, fpT), (Z, fp_ssig_T)] dead_sig_map;
   1.838 +
   1.839 +    val rhs = Library.foldl1 HOLogic.mk_comp [eval, Oper', dead_sig_map' $ VLeaf'];
   1.840 +  in
   1.841 +    define_const true fp_b version algLamN rhs lthy
   1.842 +  end;
   1.843 +
   1.844 +fun define_corecU fp_b version Y Z preT ssig_T dtor_unfold VLeaf cutSsig lthy =
   1.845 +  let
   1.846 +    val ssig_preT = Tsubst Y ssig_T preT;
   1.847 +
   1.848 +    val h = Var (("h", 0), Y --> ssig_preT);
   1.849 +    val dtor_unfold' = substT Z ssig_T dtor_unfold;
   1.850 +
   1.851 +    val rhs = HOLogic.mk_comp (dtor_unfold' $ (cutSsig $ h), VLeaf)
   1.852 +      |> Term.lambda h;
   1.853 +  in
   1.854 +    define_const true fp_b version corecUN rhs lthy
   1.855 +  end;
   1.856 +
   1.857 +fun define_corecUU fp_b version Y Z preT ssig_T dead_pre_map dead_ssig_map flat eval_core sctr
   1.858 +    corecU lthy =
   1.859 +  let
   1.860 +    val ssig_preT = Tsubst Y ssig_T preT;
   1.861 +    val ssig_ssig_T = Tsubst Y ssig_T ssig_T
   1.862 +    val ssig_ssig_preT = HOLogic.mk_prodT (ssig_T, ssig_preT);
   1.863 +
   1.864 +    val ssig_pre_ssig_T = Tsubst Y ssig_preT ssig_T;
   1.865 +
   1.866 +    val h = Var (("h", 0), Y --> ssig_pre_ssig_T);
   1.867 +    val dead_pre_map' = Term.subst_atomic_types [(Y, ssig_ssig_T), (Z, ssig_T)] dead_pre_map;
   1.868 +    val eval_core' = substT Y ssig_T eval_core;
   1.869 +    val dead_ssig_map' =
   1.870 +      Term.subst_atomic_types [(Y, ssig_preT), (Z, ssig_ssig_preT)] dead_ssig_map;
   1.871 +    val id' = HOLogic.id_const ssig_preT;
   1.872 +
   1.873 +    val rhs = corecU $ Library.foldl1 HOLogic.mk_comp
   1.874 +        [dead_pre_map' $ flat, eval_core', dead_ssig_map' $ mk_convol (sctr, id'), h]
   1.875 +      |> Term.lambda h;
   1.876 +  in
   1.877 +    define_const true fp_b version corecUUN rhs lthy
   1.878 +  end;
   1.879 +
   1.880 +fun derive_sig_transfer maybe_swap ctxt live_AsBs pre_rel sig_rel Rs R const pre_rel_def
   1.881 +    preT_rel_eqs transfer_thm =
   1.882 +  let
   1.883 +    val RRpre_rel = list_comb (pre_rel, Rs) $ R;
   1.884 +    val RRsig_rel = list_comb (sig_rel, Rs) $ R;
   1.885 +    val constB = Term.subst_atomic_types live_AsBs const;
   1.886 +
   1.887 +    val goal = uncurry mk_rel_fun (maybe_swap (RRpre_rel, RRsig_rel)) $ const $ constB
   1.888 +      |> HOLogic.mk_Trueprop;
   1.889 +  in
   1.890 +    Variable.add_free_names ctxt goal []
   1.891 +    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
   1.892 +      mk_sig_transfer_tac ctxt pre_rel_def preT_rel_eqs transfer_thm))
   1.893 +    |> Thm.close_derivation
   1.894 +  end;
   1.895 +
   1.896 +fun derive_transfer_by_transfer_prover ctxt live_AsBs Rs R const const_defs rel_eqs transfers =
   1.897 +  let
   1.898 +    val constB = Term.subst_atomic_types live_AsBs const;
   1.899 +    val goal = mk_parametricity_goal ctxt (Rs @ [R]) const constB;
   1.900 +  in
   1.901 +    Variable.add_free_names ctxt goal []
   1.902 +    |> (fn vars => Goal.prove_sorry (*FIXME*) (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
   1.903 +      mk_transfer_by_transfer_prover_tac ctxt (const_defs @ map (fn thm => thm RS sym) rel_eqs)
   1.904 +        rel_eqs transfers))
   1.905 +    |> Thm.close_derivation
   1.906 +  end;
   1.907 +
   1.908 +fun derive_dtor_transfer ctxt live_EsFs Y Z pre_rel fp_rel Rs dtor dtor_rel_thm =
   1.909 +  let
   1.910 +    val Type (@{type_name fun}, [fpT, Type (@{type_name fun}, [fpTB, @{typ bool}])]) =
   1.911 +      snd (strip_typeN (length live_EsFs) (fastype_of fp_rel));
   1.912 +
   1.913 +    val pre_rel' = Term.subst_atomic_types [(Y, fpT), (Z, fpTB)] pre_rel;
   1.914 +    val Rpre_rel = list_comb (pre_rel', Rs);
   1.915 +    val Rfp_rel = list_comb (fp_rel, Rs);
   1.916 +    val dtorB = Term.subst_atomic_types live_EsFs dtor;
   1.917 +
   1.918 +    val goal = HOLogic.mk_Trueprop (mk_rel_fun Rfp_rel (Rpre_rel $ Rfp_rel) $ dtor $ dtorB);
   1.919 +  in
   1.920 +    Variable.add_free_names ctxt goal []
   1.921 +    |> (fn vars => Goal.prove_sorry (*FIXME*) (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
   1.922 +      mk_dtor_transfer_tac ctxt dtor_rel_thm))
   1.923 +    |> Thm.close_derivation
   1.924 +  end;
   1.925 +
   1.926 +fun derive_Lam_or_eval_core_transfer ctxt live_AsBs Y Z preT ssig_T Rs R pre_rel sig_or_ssig_rel
   1.927 +    ssig_rel const const_def rel_eqs transfers =
   1.928 +  let
   1.929 +    val YpreT = HOLogic.mk_prodT (Y, preT);
   1.930 +    val ZpreTB = typ_subst_atomic live_AsBs YpreT;
   1.931 +    val ssig_TB = typ_subst_atomic live_AsBs ssig_T;
   1.932 +
   1.933 +    val pre_rel' = Term.subst_atomic_types [(Y, ssig_T), (Z, ssig_TB)] pre_rel;
   1.934 +    val sig_or_ssig_rel' = Term.subst_atomic_types [(Y, YpreT), (Z, ZpreTB)] sig_or_ssig_rel;
   1.935 +    val Rsig_or_ssig_rel' = list_comb (sig_or_ssig_rel', Rs);
   1.936 +    val RRpre_rel = list_comb (pre_rel, Rs) $ R;
   1.937 +    val RRssig_rel = list_comb (ssig_rel, Rs) $ R;
   1.938 +    val Rpre_rel' = list_comb (pre_rel', Rs);
   1.939 +    val constB = subst_atomic_types live_AsBs const;
   1.940 +
   1.941 +    val goal = mk_rel_fun (Rsig_or_ssig_rel' $ mk_rel_prod R RRpre_rel) (Rpre_rel' $ RRssig_rel)
   1.942 +        $ const $ constB
   1.943 +      |> HOLogic.mk_Trueprop;
   1.944 +  in
   1.945 +    Variable.add_free_names ctxt goal []
   1.946 +    |> (fn vars => Goal.prove_sorry (*FIXME*) (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
   1.947 +      mk_transfer_by_transfer_prover_tac ctxt [const_def] rel_eqs transfers))
   1.948 +    |> Thm.close_derivation
   1.949 +  end;
   1.950 +
   1.951 +fun derive_proto_sctr_transfer_step_or_merge ctxt Y Z R dead_pre_rel dead_sig_rel proto_sctr
   1.952 +    proto_sctr_def fp_k_T_rel_eqs transfers =
   1.953 +  let
   1.954 +    val proto_sctrZ = substT Y Z proto_sctr;
   1.955 +    val goal = mk_rel_fun (dead_pre_rel $ R) (dead_sig_rel $ R) $ proto_sctr $ proto_sctrZ
   1.956 +      |> HOLogic.mk_Trueprop;
   1.957 +  in
   1.958 +    Variable.add_free_names ctxt goal []
   1.959 +    |> (fn vars => Goal.prove_sorry (*FIXME*) (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
   1.960 +      mk_transfer_by_transfer_prover_tac ctxt [proto_sctr_def] fp_k_T_rel_eqs transfers))
   1.961 +    |> Thm.close_derivation
   1.962 +  end;
   1.963 +
   1.964 +fun derive_sctr_transfer ctxt live_AsBs Y Z ssig_T Rs R pre_rel ssig_rel sctr sctr_def
   1.965 +    fp_k_T_rel_eqs transfers =
   1.966 +  let
   1.967 +    val ssig_TB = typ_subst_atomic live_AsBs ssig_T;
   1.968 +
   1.969 +    val pre_rel' = Term.subst_atomic_types [(Y, ssig_T), (Z, ssig_TB)] pre_rel;
   1.970 +    val Rpre_rel' = list_comb (pre_rel', Rs);
   1.971 +    val RRssig_rel = list_comb (ssig_rel, Rs) $ R;
   1.972 +    val sctrB = subst_atomic_types live_AsBs sctr;
   1.973 +
   1.974 +    val goal = HOLogic.mk_Trueprop (mk_rel_fun (Rpre_rel' $ RRssig_rel) RRssig_rel $ sctr $ sctrB);
   1.975 +  in
   1.976 +    Variable.add_free_names ctxt goal []
   1.977 +    |> (fn vars => Goal.prove_sorry (*FIXME*) (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
   1.978 +      mk_transfer_by_transfer_prover_tac ctxt [sctr_def] fp_k_T_rel_eqs transfers))
   1.979 +    |> Thm.close_derivation
   1.980 +  end;
   1.981 +
   1.982 +fun derive_corecUU_transfer ctxt live_AsBs Y Z Rs R preT ssig_T pre_rel fp_rel ssig_rel corecUU
   1.983 +    cutSsig_def corecU_def corecUU_def fp_k_T_rel_eqs transfers =
   1.984 +  let
   1.985 +    val ssig_preT = Tsubst Y ssig_T preT;
   1.986 +    val ssig_TB = typ_subst_atomic live_AsBs ssig_T;
   1.987 +    val ssig_preTB = typ_subst_atomic live_AsBs ssig_preT;
   1.988 +
   1.989 +    val pre_rel' = Term.subst_atomic_types [(Y, ssig_T), (Z, ssig_TB)] pre_rel;
   1.990 +    val ssig_rel' = Term.subst_atomic_types [(Y, ssig_preT), (Z, ssig_preTB)] ssig_rel;
   1.991 +    val Rpre_rel' = list_comb (pre_rel', Rs);
   1.992 +    val Rfp_rel = list_comb (fp_rel, Rs);
   1.993 +    val RRssig_rel = list_comb (ssig_rel, Rs) $ R;
   1.994 +    val Rssig_rel' = list_comb (ssig_rel', Rs);
   1.995 +    val corecUUB = subst_atomic_types live_AsBs corecUU;
   1.996 +
   1.997 +    val goal = mk_rel_fun (mk_rel_fun R (Rssig_rel' $ (Rpre_rel' $ RRssig_rel)))
   1.998 +        (mk_rel_fun R Rfp_rel) $ corecUU $ corecUUB
   1.999 +      |> HOLogic.mk_Trueprop;
  1.1000 +  in
  1.1001 +    Variable.add_free_names ctxt goal []
  1.1002 +    |> (fn vars => Goal.prove_sorry (*FIXME*) (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1.1003 +      mk_transfer_by_transfer_prover_tac ctxt [cutSsig_def, corecU_def, corecUU_def] fp_k_T_rel_eqs
  1.1004 +        transfers))
  1.1005 +    |> Thm.close_derivation
  1.1006 +  end;
  1.1007 +
  1.1008 +fun mk_natural_goal ctxt simple_T_mapfs fs t u =
  1.1009 +  let
  1.1010 +    fun build_simple (T, _) =
  1.1011 +      (case AList.lookup (op =) simple_T_mapfs T of
  1.1012 +        SOME mapf => mapf
  1.1013 +      | NONE => the (find_first (fn f => domain_type (fastype_of f) = T) fs));
  1.1014 +
  1.1015 +    val simple_Ts = map fst simple_T_mapfs;
  1.1016 +
  1.1017 +    val t_map = build_map ctxt simple_Ts build_simple (apply2 (range_type o fastype_of) (t, u));
  1.1018 +    val u_map = build_map ctxt simple_Ts build_simple (apply2 (domain_type o fastype_of) (t, u));
  1.1019 +  in
  1.1020 +    mk_Trueprop_eq (HOLogic.mk_comp (u, u_map), HOLogic.mk_comp (t_map, t))
  1.1021 +  end;
  1.1022 +
  1.1023 +fun derive_natural_by_unfolding ctxt live_AsBs preT pre_map fs f const map_thms =
  1.1024 +  let
  1.1025 +    val ffpre_map = list_comb (pre_map, fs) $ f;
  1.1026 +    val constB = subst_atomic_types live_AsBs const;
  1.1027 +
  1.1028 +    val goal = mk_natural_goal ctxt [(preT, ffpre_map)] (fs @ [f]) const constB;
  1.1029 +  in
  1.1030 +    Variable.add_free_names ctxt goal []
  1.1031 +    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1.1032 +      mk_natural_by_unfolding_tac ctxt map_thms))
  1.1033 +    |> Thm.close_derivation
  1.1034 +  end;
  1.1035 +
  1.1036 +fun derive_natural_from_transfer ctxt live_AsBs simple_T_mapfs fs f const transfer bnfs subst_bnfs =
  1.1037 +  let
  1.1038 +    val m = length live_AsBs;
  1.1039 +
  1.1040 +    val constB = Term.subst_atomic_types live_AsBs const;
  1.1041 +    val goal = mk_natural_goal ctxt simple_T_mapfs (fs @ [f]) const constB;
  1.1042 +  in
  1.1043 +    Variable.add_free_names ctxt goal []
  1.1044 +    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1.1045 +      mk_natural_from_transfer_tac ctxt m (replicate m true) transfer [] (map rel_Grp_of_bnf bnfs)
  1.1046 +        (map rel_Grp_of_bnf subst_bnfs)))
  1.1047 +    |> Thm.close_derivation
  1.1048 +  end;
  1.1049 +
  1.1050 +fun derive_natural_from_transfer_with_pre_type ctxt live_AsBs Y Z preT ssig_T pre_map ssig_map fs
  1.1051 +    f =
  1.1052 +  let
  1.1053 +    val ssig_TB = typ_subst_atomic live_AsBs ssig_T;
  1.1054 +    val preT' = Term.typ_subst_atomic [(Y, ssig_T), (Z, ssig_TB)] preT;
  1.1055 +
  1.1056 +    val ffpre_map = list_comb (pre_map, fs) $ f;
  1.1057 +    val pre_map' = Term.subst_atomic_types [(Y, ssig_T), (Z, ssig_TB)] pre_map;
  1.1058 +    val fpre_map' = list_comb (pre_map', fs);
  1.1059 +    val ffssig_map = list_comb (ssig_map, fs) $ f;
  1.1060 +
  1.1061 +    val preT_mapfs = [(preT, ffpre_map), (preT', fpre_map' $ ffssig_map)];
  1.1062 +  in
  1.1063 +    derive_natural_from_transfer ctxt live_AsBs preT_mapfs fs f
  1.1064 +  end;
  1.1065 +
  1.1066 +fun derive_Lam_Inl_Inr ctxt Y Z preT old_sig_T old_ssig_T k_T ssig_T dead_pre_map Sig embL old_Lam
  1.1067 +    Lam rho unsig_thm Lam_def =
  1.1068 +  let
  1.1069 +    val YpreT = HOLogic.mk_prodT (Y, preT);
  1.1070 +    val Ypre_old_sig_T = Tsubst Y YpreT old_sig_T;
  1.1071 +    val Ypre_k_T = Tsubst Y YpreT k_T;
  1.1072 +
  1.1073 +    val inl' = Inl_const Ypre_old_sig_T Ypre_k_T;
  1.1074 +    val inr' = Inr_const Ypre_old_sig_T Ypre_k_T;
  1.1075 +    val dead_pre_map' = Term.subst_atomic_types [(Y, old_ssig_T), (Z, ssig_T)] dead_pre_map;
  1.1076 +    val Sig' = substT Y YpreT Sig;
  1.1077 +    val Lam_o_Sig = HOLogic.mk_comp (Lam, Sig');
  1.1078 +
  1.1079 +    val inl_goal = mk_Trueprop_eq (HOLogic.mk_comp (Lam_o_Sig, inl'),
  1.1080 +      HOLogic.mk_comp (dead_pre_map' $ embL, old_Lam));
  1.1081 +    val inr_goal = mk_Trueprop_eq (HOLogic.mk_comp (Lam_o_Sig, inr'), rho);
  1.1082 +    val goals = [inl_goal, inr_goal];
  1.1083 +    val goal = Logic.mk_conjunction_balanced goals;
  1.1084 +  in
  1.1085 +    Variable.add_free_names ctxt goal []
  1.1086 +    |> (fn vars => Goal.prove_sorry ctxt vars [] goal
  1.1087 +      (fn {context = ctxt, prems = _} => mk_Lam_Inl_Inr_tac ctxt unsig_thm Lam_def))
  1.1088 +    |> Conjunction.elim_balanced (length goals)
  1.1089 +    |> map Thm.close_derivation
  1.1090 +  end;
  1.1091 +
  1.1092 +fun derive_flat_VLeaf ctxt Y Z ssig_T x VLeaf dead_ssig_map flat ssig_induct fp_map_id sig_map_cong
  1.1093 +    sig_map_ident sig_map_comp ssig_map_thms flat_simps =
  1.1094 +  let
  1.1095 +    val x' = substT Y ssig_T x;
  1.1096 +    val dead_ssig_map' = substT Z ssig_T dead_ssig_map;
  1.1097 +
  1.1098 +    val goal = mk_Trueprop_eq (flat $ (dead_ssig_map' $ VLeaf $ x'), x');
  1.1099 +
  1.1100 +    val ssig_induct' = infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt x')] ssig_induct;
  1.1101 +  in
  1.1102 +    Variable.add_free_names ctxt goal []
  1.1103 +    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1.1104 +      mk_flat_VLeaf_or_flat_tac ctxt ssig_induct' sig_map_cong
  1.1105 +        (fp_map_id :: sig_map_ident :: sig_map_comp :: ssig_map_thms @ flat_simps @
  1.1106 +         @{thms o_apply id_apply id_def[symmetric]})))
  1.1107 +    |> Thm.close_derivation
  1.1108 +  end;
  1.1109 +
  1.1110 +fun derive_flat_flat ctxt Y Z ssig_T x dead_ssig_map flat ssig_induct fp_map_id sig_map_cong
  1.1111 +    sig_map_comp ssig_map_thms flat_simps =
  1.1112 +  let
  1.1113 +    val ssig_ssig_T = Tsubst Y ssig_T ssig_T;
  1.1114 +    val ssig_ssig_ssig_T = Tsubst Y ssig_T ssig_ssig_T;
  1.1115 +
  1.1116 +    val x' = substT Y ssig_ssig_ssig_T x;
  1.1117 +    val dead_ssig_map' = Term.subst_atomic_types [(Y, ssig_ssig_T), (Z, ssig_T)] dead_ssig_map;
  1.1118 +    val flat' = substT Y ssig_T flat;
  1.1119 +
  1.1120 +    val goal = mk_Trueprop_eq (flat $ (dead_ssig_map' $ flat $ x'), flat $ (flat' $ x'));
  1.1121 +
  1.1122 +    val ssig_induct' = infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt x')] ssig_induct;
  1.1123 +  in
  1.1124 +    Variable.add_free_names ctxt goal []
  1.1125 +    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1.1126 +      mk_flat_VLeaf_or_flat_tac ctxt ssig_induct' sig_map_cong
  1.1127 +        (o_apply :: fp_map_id :: sig_map_comp :: ssig_map_thms @ flat_simps)))
  1.1128 +    |> Thm.close_derivation
  1.1129 +  end;
  1.1130 +
  1.1131 +fun derive_eval_core_flat ctxt Y Z preT ssig_T dead_pre_map dead_ssig_map flat eval_core x
  1.1132 +    ssig_induct dead_pre_map_id dead_pre_map_comp0 dead_pre_map_comp fp_map_id sig_map_comp
  1.1133 +    sig_map_cong ssig_map_thms ssig_map_comp flat_simps flat_pointful_natural flat_flat
  1.1134 +    Lam_pointful_natural eval_core_simps =
  1.1135 +  let
  1.1136 +    val YpreT = HOLogic.mk_prodT (Y, preT);
  1.1137 +    val ssig_ssig_T = Tsubst Y ssig_T ssig_T;
  1.1138 +    val Ypre_ssig_T = Tsubst Y YpreT ssig_T;
  1.1139 +    val Ypre_ssig_ssig_T = Tsubst Y YpreT ssig_ssig_T;
  1.1140 +    val ssig_YpreT = Tsubst Y ssig_T YpreT;
  1.1141 +
  1.1142 +    val dead_pre_map' = Term.subst_atomic_types [(Y, ssig_ssig_T), (Z, ssig_T)] dead_pre_map;
  1.1143 +    val dead_ssig_map' = Term.subst_atomic_types [(Y, Ypre_ssig_T), (Z, ssig_YpreT)] dead_ssig_map;
  1.1144 +    val dead_ssig_map'' = Term.subst_atomic_types [(Y, YpreT), (Z, Y)] dead_ssig_map;
  1.1145 +    val flat' = substT Y YpreT flat;
  1.1146 +    val eval_core' = substT Y ssig_T eval_core;
  1.1147 +    val x' = substT Y Ypre_ssig_ssig_T x;
  1.1148 +    val fst' = fst_const YpreT;
  1.1149 +
  1.1150 +    val goal = mk_Trueprop_eq (eval_core $ (flat' $ x'), dead_pre_map' $ flat
  1.1151 +      $ (eval_core' $ (dead_ssig_map' $ mk_convol (dead_ssig_map'' $ fst', eval_core) $ x')));
  1.1152 +
  1.1153 +    val ssig_induct' = infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt x')] ssig_induct;
  1.1154 +  in
  1.1155 +    Variable.add_free_names ctxt goal []
  1.1156 +    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1.1157 +      mk_eval_core_flat_tac ctxt ssig_induct' dead_pre_map_id dead_pre_map_comp0 dead_pre_map_comp
  1.1158 +        fp_map_id sig_map_comp sig_map_cong ssig_map_thms ssig_map_comp flat_simps
  1.1159 +        flat_pointful_natural flat_flat Lam_pointful_natural eval_core_simps))
  1.1160 +    |> Thm.close_derivation
  1.1161 +  end;
  1.1162 +
  1.1163 +fun derive_eval_thm ctxt dtor_inject dtor_unfold_thm eval_def =
  1.1164 +  (trans OF [iffD2 OF [dtor_inject, eval_def RS meta_eq_to_obj_eq RS fun_cong], dtor_unfold_thm])
  1.1165 +  |> unfold_thms ctxt [o_apply, eval_def RS Drule.symmetric_thm];
  1.1166 +
  1.1167 +fun derive_eval_flat ctxt Y Z fpT ssig_T dead_ssig_map flat eval x dead_pre_map_comp0
  1.1168 +    dtor_unfold_unique ssig_map_id ssig_map_comp flat_pointful_natural eval_core_pointful_natural
  1.1169 +    eval_core_flat eval_thm =
  1.1170 +  let
  1.1171 +    val fp_ssig_T = Tsubst Y fpT ssig_T;
  1.1172 +    val fp_ssig_ssig_T = Tsubst Y fp_ssig_T ssig_T;
  1.1173 +
  1.1174 +    val dead_ssig_map' = Term.subst_atomic_types [(Y, fp_ssig_T), (Z, fpT)] dead_ssig_map;
  1.1175 +    val flat' = substT Y fpT flat;
  1.1176 +    val x' = substT Y fp_ssig_ssig_T x;
  1.1177 +
  1.1178 +    val goal = mk_Trueprop_eq (eval $ (flat' $ x'), eval $ (dead_ssig_map' $ eval $ x'));
  1.1179 +
  1.1180 +    val cond_eval_o_flat =
  1.1181 +      infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt (HOLogic.mk_comp (eval, flat')))]
  1.1182 +        (trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym] RS fun_cong)
  1.1183 +      OF [ext, ext];
  1.1184 +  in
  1.1185 +    Variable.add_free_names ctxt goal []
  1.1186 +    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1.1187 +      mk_eval_flat_tac ctxt dead_pre_map_comp0 ssig_map_id ssig_map_comp flat_pointful_natural
  1.1188 +        eval_core_pointful_natural eval_core_flat eval_thm cond_eval_o_flat))
  1.1189 +    |> Thm.close_derivation
  1.1190 +  end;
  1.1191 +
  1.1192 +fun derive_eval_Oper ctxt live Y Z fpT sig_T ssig_T dead_sig_map Oper eval algLam x sig_map_ident
  1.1193 +    sig_map_comp0 sig_map_comp Oper_natural_pointful VLeaf_natural flat_simps eval_flat algLam_def =
  1.1194 +  let
  1.1195 +    val fp_ssig_T = Tsubst Y fpT ssig_T;
  1.1196 +    val fp_ssig_sig_T = Tsubst Y fp_ssig_T sig_T;
  1.1197 +
  1.1198 +    val dead_sig_map' = Term.subst_atomic_types [(Y, fp_ssig_T), (Z, fpT)] dead_sig_map;
  1.1199 +    val Oper' = substT Y fpT Oper;
  1.1200 +    val x' = substT Y fp_ssig_sig_T x;
  1.1201 +
  1.1202 +    val goal = mk_Trueprop_eq (eval $ (Oper' $ x'), algLam $ (dead_sig_map' $ eval $ x'));
  1.1203 +  in
  1.1204 +    Variable.add_free_names ctxt goal []
  1.1205 +    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1.1206 +      mk_eval_Oper_tac ctxt live sig_map_ident sig_map_comp0 sig_map_comp Oper_natural_pointful
  1.1207 +        VLeaf_natural flat_simps eval_flat algLam_def))
  1.1208 +    |> Thm.close_derivation
  1.1209 +  end;
  1.1210 +
  1.1211 +fun derive_eval_V_or_CLeaf ctxt Y fpT V_or_CLeaf eval x dead_pre_map_id dead_pre_map_comp fp_map_id
  1.1212 +    dtor_unfold_unique V_or_CLeaf_map_thm eval_core_simps eval_thm =
  1.1213 +  let
  1.1214 +    val V_or_CLeaf' = substT Y fpT V_or_CLeaf;
  1.1215 +    val x' = substT Y fpT x;
  1.1216 +
  1.1217 +    val goal = mk_Trueprop_eq (eval $ (V_or_CLeaf' $ x'), x');
  1.1218 +  in
  1.1219 +    Variable.add_free_names ctxt goal []
  1.1220 +    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1.1221 +      mk_eval_V_or_CLeaf_tac ctxt dead_pre_map_id dead_pre_map_comp fp_map_id dtor_unfold_unique
  1.1222 +        V_or_CLeaf_map_thm eval_core_simps eval_thm))
  1.1223 +    |> Thm.close_derivation
  1.1224 +  end;
  1.1225 +
  1.1226 +fun derive_extdd_mor ctxt Y Z preT fpT ssig_T dead_pre_map dtor extdd cutSsig f g dead_pre_map_comp0
  1.1227 +    dead_pre_map_comp VLeaf_map_thm ssig_map_comp flat_pointful_natural eval_core_pointful_natural
  1.1228 +    eval_thm eval_flat eval_VLeaf cutSsig_def =
  1.1229 +  let
  1.1230 +    val ssig_preT = Tsubst Y ssig_T preT;
  1.1231 +
  1.1232 +    val dead_pre_map' = Term.subst_atomic_types [(Y, ssig_T), (Z, fpT)] dead_pre_map;
  1.1233 +    val f' = substT Z fpT f;
  1.1234 +    val g' = substT Z ssig_preT g;
  1.1235 +    val extdd_f = extdd $ f';
  1.1236 +
  1.1237 +    val prem = mk_Trueprop_eq (HOLogic.mk_comp (dead_pre_map' $ extdd_f, g'),
  1.1238 +      HOLogic.mk_comp (dtor, f'));
  1.1239 +    val goal = mk_Trueprop_eq (HOLogic.mk_comp (dead_pre_map' $ extdd_f, cutSsig $ g'),
  1.1240 +      HOLogic.mk_comp (dtor, extdd_f));
  1.1241 +  in
  1.1242 +    fold (Variable.add_free_names ctxt) [prem, goal] []
  1.1243 +    |> (fn vars => Goal.prove_sorry ctxt vars [prem] goal (fn {context = ctxt, prems = [prem]} =>
  1.1244 +      mk_extdd_mor_tac ctxt dead_pre_map_comp0 dead_pre_map_comp VLeaf_map_thm ssig_map_comp
  1.1245 +        flat_pointful_natural eval_core_pointful_natural eval_thm eval_flat eval_VLeaf cutSsig_def
  1.1246 +        prem))
  1.1247 +    |> Thm.close_derivation
  1.1248 +  end;
  1.1249 +
  1.1250 +fun derive_mor_cutSsig_flat ctxt Y Z preT fpT ssig_T dead_pre_map dead_ssig_map dtor flat eval_core
  1.1251 +    eval cutSsig f g dead_pre_map_comp0 dead_pre_map_comp dead_pre_map_cong dtor_unfold_unique
  1.1252 +    dead_ssig_map_comp0 ssig_map_comp flat_simps flat_pointful_natural eval_core_pointful_natural
  1.1253 +    flat_flat flat_VLeaf eval_core_flat cutSsig_def cutSsig_def_pointful_natural eval_thm =
  1.1254 +  let
  1.1255 +    val ssig_preT = Tsubst Y ssig_T preT;
  1.1256 +
  1.1257 +    val substYZ = Term.subst_atomic_types [(Y, ssig_T), (Z, fpT)];
  1.1258 +
  1.1259 +    val dead_pre_map' = substYZ dead_pre_map;
  1.1260 +    val dead_ssig_map' = substYZ dead_ssig_map;
  1.1261 +    val f' = substYZ f;
  1.1262 +    val g' = substT Z ssig_preT g;
  1.1263 +    val cutSsig_g = cutSsig $ g';
  1.1264 +
  1.1265 +    val id' = HOLogic.id_const ssig_T;
  1.1266 +    val convol' = mk_convol (id', cutSsig_g);
  1.1267 +    val dead_ssig_map'' =
  1.1268 +      Term.subst_atomic_types [(Y, ssig_T), (Z, range_type (fastype_of convol'))] dead_ssig_map;
  1.1269 +    val eval_core' = substT Y ssig_T eval_core;
  1.1270 +    val eval_core_o_map = HOLogic.mk_comp (eval_core', dead_ssig_map'' $ convol');
  1.1271 +
  1.1272 +    val prem = mk_Trueprop_eq (HOLogic.mk_comp (dead_pre_map' $ f', cutSsig_g),
  1.1273 +      HOLogic.mk_comp (dtor, f'));
  1.1274 +    val goal = mk_Trueprop_eq (HOLogic.mk_comp (eval, dead_ssig_map' $ f'),
  1.1275 +      HOLogic.mk_comp (f', flat));
  1.1276 +  in
  1.1277 +    fold (Variable.add_free_names ctxt) [prem, goal] []
  1.1278 +    |> (fn vars => Goal.prove_sorry ctxt vars [prem] goal (fn {context = ctxt, prems = [prem]} =>
  1.1279 +      mk_mor_cutSsig_flat_tac ctxt eval_core_o_map dead_pre_map_comp0 dead_pre_map_comp
  1.1280 +        dead_pre_map_cong dtor_unfold_unique dead_ssig_map_comp0 ssig_map_comp flat_simps
  1.1281 +        flat_pointful_natural eval_core_pointful_natural flat_flat flat_VLeaf eval_core_flat
  1.1282 +        cutSsig_def cutSsig_def_pointful_natural eval_thm prem))
  1.1283 +    |> Thm.close_derivation
  1.1284 +  end;
  1.1285 +
  1.1286 +fun derive_extdd_o_VLeaf ctxt Y Z preT fpT ssig_T dead_pre_map dtor VLeaf extdd f g
  1.1287 +    dead_pre_map_comp0 dead_pre_map_comp dtor_inject ssig_map_thms eval_core_simps eval_thm
  1.1288 +    eval_VLeaf =
  1.1289 +  let
  1.1290 +    val ssig_preT = Tsubst Y ssig_T preT;
  1.1291 +
  1.1292 +    val substYZ = Term.subst_atomic_types [(Y, ssig_T), (Z, fpT)];
  1.1293 +
  1.1294 +    val dead_pre_map' = substYZ dead_pre_map;
  1.1295 +    val f' = substT Z fpT f;
  1.1296 +    val g' = substT Z ssig_preT g;
  1.1297 +    val extdd_f = extdd $ f';
  1.1298 +
  1.1299 +    val prem = mk_Trueprop_eq (HOLogic.mk_comp (dead_pre_map' $ extdd_f, g'),
  1.1300 +      HOLogic.mk_comp (dtor, f'));
  1.1301 +    val goal = mk_Trueprop_eq (HOLogic.mk_comp (extdd_f, VLeaf), f');
  1.1302 +  in
  1.1303 +    fold (Variable.add_free_names ctxt) [prem, goal] []
  1.1304 +    |> (fn vars => Goal.prove_sorry ctxt vars [prem] goal (fn {context = ctxt, prems = [prem]} =>
  1.1305 +      mk_extdd_o_VLeaf_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_inject ssig_map_thms
  1.1306 +        eval_core_simps eval_thm eval_VLeaf prem))
  1.1307 +    |> Thm.close_derivation
  1.1308 +  end;
  1.1309 +
  1.1310 +fun derive_corecU_pointfree ctxt Y Z preT fpT ssig_T dead_pre_map dtor extdd corecU g
  1.1311 +    dead_pre_map_comp dtor_unfold_thm ssig_map_thms dead_ssig_map_comp0 flat_simps flat_VLeaf
  1.1312 +    eval_core_simps cutSsig_def mor_cutSsig_flat corecU_def =
  1.1313 +  let
  1.1314 +    val ssig_preT = Tsubst Y ssig_T preT;
  1.1315 +
  1.1316 +    val substYZ = Term.subst_atomic_types [(Y, ssig_T), (Z, fpT)];
  1.1317 +
  1.1318 +    val dead_pre_map' = substYZ dead_pre_map;
  1.1319 +    val g' = substT Z ssig_preT g;
  1.1320 +    val corecU_g = corecU $ g';
  1.1321 +
  1.1322 +    val goal = mk_Trueprop_eq (HOLogic.mk_comp (dead_pre_map' $ (extdd $ corecU_g), g'),
  1.1323 +      HOLogic.mk_comp (dtor, corecU_g));
  1.1324 +  in
  1.1325 +    Variable.add_free_names ctxt goal []
  1.1326 +    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1.1327 +      mk_corecU_pointfree_tac ctxt dead_pre_map_comp dtor_unfold_thm ssig_map_thms
  1.1328 +      dead_ssig_map_comp0 flat_simps flat_VLeaf eval_core_simps cutSsig_def mor_cutSsig_flat
  1.1329 +      corecU_def))
  1.1330 +    |> Thm.close_derivation
  1.1331 +  end;
  1.1332 +
  1.1333 +fun derive_corecU_ctor_unique ctxt Y Z preT fpT ssig_T dead_pre_map ctor dtor VLeaf extdd corecU f g
  1.1334 +    dead_pre_map_comp ctor_dtor dtor_unfold_thm dtor_unfold_unique ssig_map_thms dead_ssig_map_comp0
  1.1335 +    flat_simps flat_VLeaf eval_core_simps extdd_mor extdd_o_VLeaf cutSsig_def mor_cutSsig_flat
  1.1336 +    corecU_def =
  1.1337 +  let
  1.1338 +    val corecU_pointfree = derive_corecU_pointfree ctxt Y Z preT fpT ssig_T dead_pre_map dtor extdd
  1.1339 +      corecU g dead_pre_map_comp dtor_unfold_thm ssig_map_thms dead_ssig_map_comp0 flat_simps
  1.1340 +      flat_VLeaf eval_core_simps cutSsig_def mor_cutSsig_flat corecU_def;
  1.1341 +
  1.1342 +    val corecU_thm = corecU_pointfree RS @{thm comp_eq_dest};
  1.1343 +
  1.1344 +    val corecU_ctor =
  1.1345 +      let
  1.1346 +        val arg_cong' =
  1.1347 +          infer_instantiate' ctxt [NONE, NONE, SOME (Thm.cterm_of ctxt ctor)] arg_cong;
  1.1348 +      in
  1.1349 +        unfold_thms ctxt [ctor_dtor] (corecU_thm RS arg_cong')
  1.1350 +      end;
  1.1351 +
  1.1352 +    val corecU_unique =
  1.1353 +      let
  1.1354 +        val substYZ = Term.subst_atomic_types [(Y, ssig_T), (Z, fpT)];
  1.1355 +
  1.1356 +        val f' = substYZ f;
  1.1357 +        val abs_f_o_VLeaf = Term.lambda f' (HOLogic.mk_comp (f', VLeaf));
  1.1358 +
  1.1359 +        val inject_refine' = infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt abs_f_o_VLeaf),
  1.1360 +          SOME (Thm.cterm_of ctxt extdd)] @{thm inject_refine};
  1.1361 +      in
  1.1362 +        unfold_thms ctxt @{thms atomize_imp}
  1.1363 +          (((inject_refine' OF [extdd_o_VLeaf, extdd_o_VLeaf] RS iffD1)
  1.1364 +            OF [Drule.asm_rl, corecU_pointfree])
  1.1365 +           OF [Drule.asm_rl, trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym]
  1.1366 +             OF [extdd_mor, corecU_pointfree RS extdd_mor]])
  1.1367 +        RS @{thm obj_distinct_prems}
  1.1368 +      end;
  1.1369 +  in
  1.1370 +    (corecU_ctor, corecU_unique)
  1.1371 +  end;
  1.1372 +
  1.1373 +fun derive_dtor_algLam ctxt Y Z preT fpT sig_T ssig_T dead_pre_map dtor dead_sig_map Lam eval algLam
  1.1374 +    x pre_map_comp dead_pre_map_id dead_pre_map_comp0 dead_pre_map_comp sig_map_comp
  1.1375 +    Oper_pointful_natural ssig_map_thms dead_ssig_map_comp0 Lam_pointful_natural eval_core_simps
  1.1376 +    eval_thm eval_flat eval_VLeaf algLam_def =
  1.1377 +  let
  1.1378 +    val fp_preT = Tsubst Y fpT preT;
  1.1379 +    val fppreT = HOLogic.mk_prodT (fpT, fp_preT);
  1.1380 +    val fp_sig_T = Tsubst Y fpT sig_T;
  1.1381 +    val fp_ssig_T = Tsubst Y fpT ssig_T;
  1.1382 +
  1.1383 +    val id' = HOLogic.id_const fpT;
  1.1384 +    val convol' = mk_convol (id', dtor);
  1.1385 +    val dead_pre_map' = Term.subst_atomic_types [(Y, fp_ssig_T), (Z, fpT)] dead_pre_map;
  1.1386 +    val dead_sig_map' = Term.subst_atomic_types [(Y, fpT), (Z, fppreT)] dead_sig_map;
  1.1387 +    val Lam' = substT Y fpT Lam;
  1.1388 +    val x' = substT Y fp_sig_T x;
  1.1389 +
  1.1390 +    val goal = mk_Trueprop_eq (dtor $ (algLam $ x'),
  1.1391 +      dead_pre_map' $ eval $ (Lam' $ (dead_sig_map' $ convol' $ x')));
  1.1392 +  in
  1.1393 +    Variable.add_free_names ctxt goal []
  1.1394 +    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1.1395 +      mk_dtor_algLam_tac ctxt pre_map_comp dead_pre_map_id dead_pre_map_comp0 dead_pre_map_comp
  1.1396 +        sig_map_comp Oper_pointful_natural ssig_map_thms dead_ssig_map_comp0 Lam_pointful_natural
  1.1397 +        eval_core_simps eval_thm eval_flat eval_VLeaf algLam_def))
  1.1398 +    |> Thm.close_derivation
  1.1399 +  end;
  1.1400 +
  1.1401 +fun derive_algLam_base ctxt Y Z preT fpT dead_pre_map ctor dtor algLam proto_sctr dead_pre_map_id
  1.1402 +    dead_pre_map_comp ctor_dtor dtor_ctor dtor_unfold_unique unsig_thm Sig_pointful_natural
  1.1403 +    ssig_map_thms Lam_def flat_simps eval_core_simps eval_thm algLam_def =
  1.1404 +  let
  1.1405 +    val fp_preT = Tsubst Y fpT preT;
  1.1406 +
  1.1407 +    val proto_sctr' = substT Y fpT proto_sctr;
  1.1408 +
  1.1409 +    val dead_pre_map' = Term.subst_atomic_types [(Y, fpT), (Z, fp_preT)] dead_pre_map;
  1.1410 +    val dead_pre_map_dtor = dead_pre_map' $ dtor;
  1.1411 +
  1.1412 +    val goal = mk_Trueprop_eq (HOLogic.mk_comp (algLam, proto_sctr'), ctor);
  1.1413 +  in
  1.1414 +    Variable.add_free_names ctxt goal []
  1.1415 +    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1.1416 +      mk_algLam_base_tac ctxt dead_pre_map_dtor dead_pre_map_id dead_pre_map_comp ctor_dtor
  1.1417 +        dtor_ctor dtor_unfold_unique unsig_thm Sig_pointful_natural ssig_map_thms Lam_def flat_simps
  1.1418 +        eval_core_simps eval_thm algLam_def))
  1.1419 +    |> Thm.close_derivation
  1.1420 +  end;
  1.1421 +
  1.1422 +fun derive_flat_embL ctxt Y Z old_ssig_T ssig_T dead_old_ssig_map embL old_flat flat x
  1.1423 +    old_ssig_induct fp_map_id Sig_pointful_natural old_sig_map_comp old_sig_map_cong
  1.1424 +    old_ssig_map_thms old_flat_simps flat_simps embL_simps =
  1.1425 +  let
  1.1426 +    val old_ssig_old_ssig_T = Tsubst Y old_ssig_T old_ssig_T;
  1.1427 +
  1.1428 +    val dead_old_ssig_map' =
  1.1429 +      Term.subst_atomic_types [(Y, old_ssig_T), (Z, ssig_T)] dead_old_ssig_map;
  1.1430 +    val embL' = substT Y ssig_T embL;
  1.1431 +    val x' = substT Y old_ssig_old_ssig_T x;
  1.1432 +
  1.1433 +    val goal = mk_Trueprop_eq (flat $ (embL' $ (dead_old_ssig_map' $ embL $ x')),
  1.1434 +      embL $ (old_flat $ x'));
  1.1435 +
  1.1436 +    val old_ssig_induct' =
  1.1437 +      infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt x')] old_ssig_induct;
  1.1438 +  in
  1.1439 +    Variable.add_free_names ctxt goal []
  1.1440 +    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1.1441 +      mk_flat_embL_tac ctxt old_ssig_induct' fp_map_id Sig_pointful_natural old_sig_map_comp
  1.1442 +        old_sig_map_cong old_ssig_map_thms old_flat_simps flat_simps embL_simps))
  1.1443 +    |> Thm.close_derivation
  1.1444 +  end;
  1.1445 +
  1.1446 +fun derive_eval_core_embL ctxt Y Z preT old_ssig_T ssig_T dead_pre_map embL old_eval_core eval_core
  1.1447 +    x old_ssig_induct dead_pre_map_comp0 dead_pre_map_comp Sig_pointful_natural unsig_thm
  1.1448 +    old_sig_map_comp old_sig_map_cong old_Lam_pointful_natural Lam_def flat_embL embL_simps
  1.1449 +    embL_pointful_natural old_eval_core_simps eval_core_simps =
  1.1450 +  let
  1.1451 +    val YpreT = HOLogic.mk_prodT (Y, preT);
  1.1452 +    val Ypre_old_ssig_T = Tsubst Y YpreT old_ssig_T;
  1.1453 +
  1.1454 +    val dead_pre_map' = Term.subst_atomic_types [(Y, old_ssig_T), (Z, ssig_T)] dead_pre_map;
  1.1455 +    val embL' = substT Y YpreT embL;
  1.1456 +    val x' = substT Y Ypre_old_ssig_T x;
  1.1457 +
  1.1458 +    val goal =
  1.1459 +      mk_Trueprop_eq (eval_core $ (embL' $ x'), dead_pre_map' $ embL $ (old_eval_core $ x'));
  1.1460 +
  1.1461 +    val old_ssig_induct' =
  1.1462 +      infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt x')] old_ssig_induct;
  1.1463 +  in
  1.1464 +    Variable.add_free_names ctxt goal []
  1.1465 +    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1.1466 +      mk_eval_core_embL_tac ctxt old_ssig_induct' dead_pre_map_comp0 dead_pre_map_comp
  1.1467 +        Sig_pointful_natural unsig_thm old_sig_map_comp old_sig_map_cong old_Lam_pointful_natural
  1.1468 +        Lam_def flat_embL old_eval_core_simps eval_core_simps embL_simps embL_pointful_natural))
  1.1469 +    |> Thm.close_derivation
  1.1470 +  end;
  1.1471 +
  1.1472 +fun derive_eval_embL ctxt Y fpT embL old_eval eval dead_pre_map_comp0 dtor_unfold_unique
  1.1473 +    embL_pointful_natural eval_core_embL old_eval_thm eval_thm =
  1.1474 +  let
  1.1475 +    val embL' = substT Y fpT embL;
  1.1476 +    val goal = mk_Trueprop_eq (HOLogic.mk_comp (eval, embL'), old_eval);
  1.1477 +  in
  1.1478 +    Variable.add_free_names ctxt goal []
  1.1479 +    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1.1480 +      mk_eval_embL_tac ctxt dead_pre_map_comp0 dtor_unfold_unique embL_pointful_natural
  1.1481 +        eval_core_embL old_eval_thm eval_thm))
  1.1482 +    |> Thm.close_derivation
  1.1483 +  end;
  1.1484 +
  1.1485 +fun derive_algLam_algLam ctxt Inx_const Y fpT Sig old_algLam algLam dead_pre_map_comp dtor_inject
  1.1486 +    unsig_thm sig_map_thm Lam_def eval_embL old_dtor_algLam dtor_algLam =
  1.1487 +  let
  1.1488 +    val Sig' = substT Y fpT Sig;
  1.1489 +    val (left_T, right_T) = dest_sumT (domain_type (fastype_of Sig'));
  1.1490 +    val inx' = Inx_const left_T right_T;
  1.1491 +
  1.1492 +    val goal = mk_Trueprop_eq (Library.foldl1 HOLogic.mk_comp [algLam, Sig', inx'], old_algLam);
  1.1493 +  in
  1.1494 +    Variable.add_free_names ctxt goal []
  1.1495 +    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1.1496 +      mk_algLam_algLam_tac ctxt dead_pre_map_comp dtor_inject unsig_thm sig_map_thm Lam_def
  1.1497 +        eval_embL old_dtor_algLam dtor_algLam))
  1.1498 +    |> Thm.close_derivation
  1.1499 +  end;
  1.1500 +
  1.1501 +fun derive_eval_core_k_as_ssig ctxt Y preT k_T rho eval_core k_as_ssig x pre_map_comp
  1.1502 +    dead_pre_map_id sig_map_comp ssig_map_thms Lam_natural_pointful Lam_Inr flat_VLeaf
  1.1503 +    eval_core_simps =
  1.1504 +  let
  1.1505 +    val YpreT = HOLogic.mk_prodT (Y, preT);
  1.1506 +    val Ypre_k_T = Tsubst Y YpreT k_T;
  1.1507 +
  1.1508 +    val k_as_ssig' = substT Y YpreT k_as_ssig;
  1.1509 +    val x' = substT Y Ypre_k_T x;
  1.1510 +
  1.1511 +    val goal = mk_Trueprop_eq (eval_core $ (k_as_ssig' $ x'), rho $ x');
  1.1512 +  in
  1.1513 +    Variable.add_free_names ctxt goal []
  1.1514 +    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1.1515 +      mk_eval_core_k_as_ssig_tac ctxt pre_map_comp dead_pre_map_id sig_map_comp ssig_map_thms
  1.1516 +        Lam_natural_pointful Lam_Inr flat_VLeaf eval_core_simps))
  1.1517 +    |> Thm.close_derivation
  1.1518 +  end;
  1.1519 +
  1.1520 +fun derive_algLam_algrho ctxt Y fpT Sig algLam algrho algLam_def algrho_def =
  1.1521 +  let
  1.1522 +    val Sig' = substT Y fpT Sig;
  1.1523 +    val (left_T, right_T) = dest_sumT (domain_type (fastype_of Sig'));
  1.1524 +    val inr' = Inr_const left_T right_T;
  1.1525 +
  1.1526 +    val goal = mk_Trueprop_eq (Library.foldl1 HOLogic.mk_comp [algLam, Sig', inr'], algrho);
  1.1527 +  in
  1.1528 +    Variable.add_free_names ctxt goal []
  1.1529 +    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1.1530 +      mk_algLam_algrho_tac ctxt algLam_def algrho_def))
  1.1531 +    |> Thm.close_derivation
  1.1532 +  end;
  1.1533 +
  1.1534 +fun derive_dtor_algrho ctxt Y Z preT fpT k_T ssig_T dead_pre_map dead_k_map dtor rho eval algrho x
  1.1535 +    eval_thm k_as_ssig_natural_pointful eval_core_k_as_ssig algrho_def =
  1.1536 +  let
  1.1537 +    val YpreT = HOLogic.mk_prodT (Y, preT);
  1.1538 +    val fppreT = Tsubst Y fpT YpreT;
  1.1539 +    val fp_k_T = Tsubst Y fpT k_T;
  1.1540 +    val fp_ssig_T = Tsubst Y fpT ssig_T;
  1.1541 +
  1.1542 +    val id' = HOLogic.id_const fpT;
  1.1543 +    val convol' = mk_convol (id', dtor);
  1.1544 +    val dead_pre_map' = Term.subst_atomic_types [(Y, fp_ssig_T), (Z, fpT)] dead_pre_map;
  1.1545 +    val dead_k_map' = Term.subst_atomic_types [(Y, fpT), (Z, fppreT)] dead_k_map;
  1.1546 +    val rho' = substT Y fpT rho;
  1.1547 +    val x' = substT Y fp_k_T x;
  1.1548 +
  1.1549 +    val goal = mk_Trueprop_eq (dtor $ (algrho $ x'),
  1.1550 +      dead_pre_map' $ eval $ (rho' $ (dead_k_map' $ convol' $ x')));
  1.1551 +  in
  1.1552 +    Variable.add_free_names ctxt goal []
  1.1553 +    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1.1554 +      mk_dtor_algrho_tac ctxt eval_thm k_as_ssig_natural_pointful eval_core_k_as_ssig algrho_def))
  1.1555 +    |> Thm.close_derivation
  1.1556 +  end;
  1.1557 +
  1.1558 +fun derive_algLam_step_or_merge ctxt Y fpT ctor proto_sctr algLam proto_sctr_def old_algLam_pointful
  1.1559 +    algLam_algLam =
  1.1560 +  let
  1.1561 +    val proto_sctr' = substT Y fpT proto_sctr;
  1.1562 +    val goal = mk_Trueprop_eq (HOLogic.mk_comp (algLam, proto_sctr'), ctor);
  1.1563 +
  1.1564 +    val algLam_algLam_pointful = mk_pointful ctxt algLam_algLam;
  1.1565 +  in
  1.1566 +    Variable.add_free_names ctxt goal []
  1.1567 +    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1.1568 +      mk_algLam_step_tac ctxt proto_sctr_def old_algLam_pointful algLam_algLam_pointful))
  1.1569 +    |> Thm.close_derivation
  1.1570 +  end;
  1.1571 +
  1.1572 +fun derive_eval_sctr ctxt Y Z fpT ssig_T dead_pre_map ctor eval sctr proto_sctr_pointful_natural
  1.1573 +    eval_Oper algLam_thm sctr_def =
  1.1574 +  let
  1.1575 +    val fp_ssig_T = Tsubst Y fpT ssig_T;
  1.1576 +
  1.1577 +    val dead_pre_map' = Term.subst_atomic_types [(Y, fp_ssig_T), (Z, fpT)] dead_pre_map;
  1.1578 +    val sctr' = substT Y fpT sctr;
  1.1579 +
  1.1580 +    val goal = mk_Trueprop_eq (HOLogic.mk_comp (eval, sctr'),
  1.1581 +      HOLogic.mk_comp (ctor, dead_pre_map' $ eval));
  1.1582 +  in
  1.1583 +    Variable.add_free_names ctxt goal []
  1.1584 +    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1.1585 +      mk_eval_sctr_tac ctxt proto_sctr_pointful_natural eval_Oper algLam_thm sctr_def))
  1.1586 +    |> Thm.close_derivation
  1.1587 +  end;
  1.1588 +
  1.1589 +fun derive_corecUU_pointfree_unique ctxt Y Z preT fpT ssig_T dead_pre_map ctor dead_ssig_map eval
  1.1590 +    corecUU f g dead_pre_map_comp0 dead_pre_map_comp dtor_ctor dtor_inject ssig_map_comp
  1.1591 +    flat_pointful_natural eval_core_pointful_natural eval_thm eval_flat corecU_ctor corecU_unique
  1.1592 +    sctr_pointful_natural eval_sctr_pointful corecUU_def =
  1.1593 +  let
  1.1594 +    val ssig_preT = Tsubst Y ssig_T preT;
  1.1595 +    val ssig_pre_ssig_T = Tsubst Y ssig_preT ssig_T;
  1.1596 +    val fp_ssig_T = Tsubst Y fpT ssig_T;
  1.1597 +
  1.1598 +    val dead_pre_map' = Term.subst_atomic_types [(Y, fp_ssig_T), (Z, fpT)] dead_pre_map;
  1.1599 +    val dead_pre_map'' = Term.subst_atomic_types [(Y, ssig_T), (Z, fp_ssig_T)] dead_pre_map;
  1.1600 +    val dead_ssig_map' = Term.subst_atomic_types [(Y, ssig_preT), (Z, fpT)] dead_ssig_map;
  1.1601 +    val dead_ssig_map'' = substT Z fpT dead_ssig_map;
  1.1602 +    val f' = substT Z ssig_pre_ssig_T f;
  1.1603 +    val g' = substT Z fpT g;
  1.1604 +    val corecUU_f = corecUU $ f';
  1.1605 +
  1.1606 +    fun mk_eq fpf =
  1.1607 +      mk_Trueprop_eq (fpf, Library.foldl1 HOLogic.mk_comp [eval, dead_ssig_map' $
  1.1608 +          Library.foldl1 HOLogic.mk_comp [ctor, dead_pre_map' $ eval, dead_pre_map''
  1.1609 +            $ (dead_ssig_map'' $ fpf)],
  1.1610 +        f']);
  1.1611 +
  1.1612 +    val corecUU_pointfree =
  1.1613 +      let
  1.1614 +        val goal = mk_eq corecUU_f;
  1.1615 +      in
  1.1616 +        Variable.add_free_names ctxt goal []
  1.1617 +        |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1.1618 +          mk_corecUU_pointfree_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor dtor_inject
  1.1619 +            ssig_map_comp flat_pointful_natural eval_core_pointful_natural eval_thm eval_flat
  1.1620 +            corecU_ctor sctr_pointful_natural eval_sctr_pointful corecUU_def))
  1.1621 +        |> Thm.close_derivation
  1.1622 +      end;
  1.1623 +
  1.1624 +    val corecUU_unique =
  1.1625 +      let
  1.1626 +        val prem = mk_eq g';
  1.1627 +        val goal = mk_Trueprop_eq (g', corecUU_f);
  1.1628 +      in
  1.1629 +        fold (Variable.add_free_names ctxt) [prem, goal] []
  1.1630 +        |> (fn vars => Goal.prove_sorry ctxt vars [prem] goal
  1.1631 +              (fn {context = ctxt, prems = [prem]} =>
  1.1632 +                mk_corecUU_unique_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor
  1.1633 +                  ssig_map_comp flat_pointful_natural eval_core_pointful_natural eval_thm eval_flat
  1.1634 +                  corecU_unique sctr_pointful_natural eval_sctr_pointful corecUU_def prem))
  1.1635 +        |> Thm.close_derivation
  1.1636 +      end;
  1.1637 +  in
  1.1638 +    (corecUU_pointfree, corecUU_unique)
  1.1639 +  end;
  1.1640 +
  1.1641 +fun define_flat_etc fp_b version live_AsBs Y Z preT fpT sig_T ssig_T Oper VLeaf CLeaf pre_rel
  1.1642 +    dead_pre_map dtor dtor_unfold dead_sig_map ssig_rel dead_ssig_map Lam Rs R pre_map_transfer
  1.1643 +    fp_k_T_rel_eqs sig_map_transfer ssig_map_transfer Lam_transfer dtor_transfer lthy =
  1.1644 +  let
  1.1645 +    val (flat_data as (flat, flat_def, _), lthy) = lthy
  1.1646 +      |> define_flat fp_b version Y Z fpT sig_T ssig_T Oper VLeaf CLeaf dead_sig_map;
  1.1647 +
  1.1648 +    val (eval_core_data as (eval_core, eval_core_def, _), lthy) = lthy
  1.1649 +      |> define_eval_core fp_b version Y Z preT fpT sig_T ssig_T dtor Oper VLeaf CLeaf dead_pre_map
  1.1650 +        dead_sig_map dead_ssig_map flat Lam;
  1.1651 +
  1.1652 +    val ((eval_data as (eval, _), cutSsig_data as (cutSsig, _)), lthy) = lthy
  1.1653 +      |> define_eval fp_b version Y Z preT fpT ssig_T dtor dtor_unfold dead_ssig_map eval_core
  1.1654 +      ||>> define_cutSsig fp_b version Y Z preT ssig_T dead_pre_map VLeaf dead_ssig_map flat
  1.1655 +        eval_core;
  1.1656 +
  1.1657 +    val ((algLam_data, unfold_data), lthy) = lthy
  1.1658 +      |> define_algLam fp_b version Y Z fpT ssig_T Oper VLeaf dead_sig_map eval
  1.1659 +      ||>> define_corecU fp_b version Y Z preT ssig_T dtor_unfold VLeaf cutSsig;
  1.1660 +
  1.1661 +    val flat_transfer = derive_transfer_by_transfer_prover lthy live_AsBs Rs R flat [flat_def] []
  1.1662 +      [sig_map_transfer];
  1.1663 +    val eval_core_transfer = derive_Lam_or_eval_core_transfer lthy live_AsBs Y Z preT ssig_T Rs R
  1.1664 +      pre_rel ssig_rel ssig_rel eval_core eval_core_def fp_k_T_rel_eqs
  1.1665 +      [pre_map_transfer, sig_map_transfer, ssig_map_transfer, flat_transfer, Lam_transfer,
  1.1666 +       dtor_transfer];
  1.1667 +  in
  1.1668 +    (((((((flat_data, flat_transfer), (eval_core_data, eval_core_transfer)), eval_data),
  1.1669 +      cutSsig_data), algLam_data), unfold_data), lthy)
  1.1670 +  end;
  1.1671 +
  1.1672 +fun derive_Sig_natural_etc ctxt live live_AsBs Y Z preT fpT k_or_fpT sig_T ssig_T pre_map
  1.1673 +    dead_pre_map ctor dtor Sig dead_sig_map Oper VLeaf CLeaf ssig_map dead_ssig_map Lam flat
  1.1674 +    eval_core eval cutSsig algLam corecU x fs f g ctor_dtor dtor_inject dtor_unfold_thm
  1.1675 +    dtor_unfold_unique sig_map_thm ssig_induct ssig_map_thms Oper_map_thm VLeaf_map_thm
  1.1676 +    CLeaf_map_thm Lam_transfer flat_simps flat_transfer eval_core_simps eval_core_transfer eval_def
  1.1677 +    cutSsig_def algLam_def corecU_def live_pre_bnf pre_bnf dead_pre_bnf fp_bnf sig_bnf ssig_bnf
  1.1678 +    dead_ssig_bnf =
  1.1679 +  let
  1.1680 +    val SOME prod_fp_sugar = fp_sugar_of ctxt @{type_name prod};
  1.1681 +    val prod_bnf = #fp_bnf prod_fp_sugar;
  1.1682 +
  1.1683 +    val f' = substT Z fpT f;
  1.1684 +    val dead_ssig_map' = substT Z fpT dead_ssig_map;
  1.1685 +    val extdd = Term.lambda f' (HOLogic.mk_comp (eval, dead_ssig_map' $ f'));
  1.1686 +
  1.1687 +    val live_pre_map_def = map_def_of_bnf live_pre_bnf;
  1.1688 +    val pre_map_comp = map_comp_of_bnf pre_bnf;
  1.1689 +    val dead_pre_map_id = map_id_of_bnf dead_pre_bnf;
  1.1690 +    val dead_pre_map_comp0 = map_comp0_of_bnf dead_pre_bnf;
  1.1691 +    val dead_pre_map_comp = map_comp_of_bnf dead_pre_bnf;
  1.1692 +    val dead_pre_map_cong = map_cong_of_bnf dead_pre_bnf;
  1.1693 +    val fp_map_id = map_id_of_bnf fp_bnf;
  1.1694 +    val sig_map_ident = map_ident_of_bnf sig_bnf;
  1.1695 +    val sig_map_comp0 = map_comp0_of_bnf sig_bnf;
  1.1696 +    val sig_map_comp = map_comp_of_bnf sig_bnf;
  1.1697 +    val sig_map_cong = map_cong_of_bnf sig_bnf;
  1.1698 +    val ssig_map_id = map_id_of_bnf ssig_bnf;
  1.1699 +    val ssig_map_comp = map_comp_of_bnf ssig_bnf;
  1.1700 +    val dead_ssig_map_comp0 = map_comp0_of_bnf dead_ssig_bnf;
  1.1701 +
  1.1702 +    val k_preT_map_id0s =
  1.1703 +      map map_id0_of_bnf (map_filter (bnf_of ctxt) (fold add_type_namesT [preT, k_or_fpT] []));
  1.1704 +
  1.1705 +    val Sig_natural = derive_natural_by_unfolding ctxt live_AsBs preT pre_map fs f Sig
  1.1706 +      ([sig_map_thm, live_pre_map_def, @{thm BNF_Composition.id_bnf_def}] @ k_preT_map_id0s);
  1.1707 +    val Oper_natural =
  1.1708 +      derive_natural_by_unfolding ctxt live_AsBs preT pre_map fs f Oper [Oper_map_thm];
  1.1709 +    val VLeaf_natural =
  1.1710 +      derive_natural_by_unfolding ctxt live_AsBs preT pre_map fs f VLeaf [VLeaf_map_thm];
  1.1711 +    val Lam_natural = derive_natural_from_transfer_with_pre_type ctxt live_AsBs Y Z preT ssig_T
  1.1712 +      pre_map ssig_map fs f Lam Lam_transfer [prod_bnf, pre_bnf, sig_bnf, ssig_bnf] [];
  1.1713 +    val flat_natural = derive_natural_from_transfer ctxt live_AsBs [] fs f flat flat_transfer
  1.1714 +      [ssig_bnf] [];
  1.1715 +    val eval_core_natural = derive_natural_from_transfer_with_pre_type ctxt live_AsBs Y Z preT
  1.1716 +      ssig_T pre_map ssig_map fs f eval_core eval_core_transfer [prod_bnf, pre_bnf, ssig_bnf] [];
  1.1717 +
  1.1718 +    val Sig_pointful_natural = mk_pointful ctxt Sig_natural RS sym;
  1.1719 +    val Oper_natural_pointful = mk_pointful ctxt Oper_natural;
  1.1720 +    val Oper_pointful_natural = Oper_natural_pointful RS sym;
  1.1721 +    val flat_pointful_natural = mk_pointful ctxt flat_natural RS sym;
  1.1722 +    val Lam_natural_pointful = mk_pointful ctxt Lam_natural;
  1.1723 +    val Lam_pointful_natural = Lam_natural_pointful RS sym;
  1.1724 +    val eval_core_pointful_natural = mk_pointful ctxt eval_core_natural RS sym;
  1.1725 +    val cutSsig_def_pointful_natural = mk_pointful ctxt (cutSsig_def RS meta_eq_to_obj_eq) RS sym;
  1.1726 +
  1.1727 +    val flat_VLeaf = derive_flat_VLeaf ctxt Y Z ssig_T x VLeaf dead_ssig_map flat ssig_induct
  1.1728 +      fp_map_id sig_map_cong sig_map_ident sig_map_comp ssig_map_thms flat_simps;
  1.1729 +    val flat_flat = derive_flat_flat ctxt Y Z ssig_T x dead_ssig_map flat ssig_induct fp_map_id
  1.1730 +      sig_map_cong sig_map_comp ssig_map_thms flat_simps;
  1.1731 +
  1.1732 +    val eval_core_flat = derive_eval_core_flat ctxt Y Z preT ssig_T dead_pre_map dead_ssig_map flat
  1.1733 +      eval_core x ssig_induct dead_pre_map_id dead_pre_map_comp0 dead_pre_map_comp fp_map_id
  1.1734 +      sig_map_comp sig_map_cong ssig_map_thms ssig_map_comp flat_simps flat_pointful_natural
  1.1735 +      flat_flat Lam_pointful_natural eval_core_simps;
  1.1736 +
  1.1737 +    val eval_thm = derive_eval_thm ctxt dtor_inject dtor_unfold_thm eval_def;
  1.1738 +    val eval_flat = derive_eval_flat ctxt Y Z fpT ssig_T dead_ssig_map flat eval x
  1.1739 +      dead_pre_map_comp0 dtor_unfold_unique ssig_map_id ssig_map_comp flat_pointful_natural
  1.1740 +      eval_core_pointful_natural eval_core_flat eval_thm;
  1.1741 +    val eval_Oper = derive_eval_Oper ctxt live Y Z fpT sig_T ssig_T dead_sig_map Oper eval algLam x
  1.1742 +      sig_map_ident sig_map_comp0 sig_map_comp Oper_natural_pointful VLeaf_natural flat_simps
  1.1743 +      eval_flat algLam_def;
  1.1744 +    val eval_VLeaf = derive_eval_V_or_CLeaf ctxt Y fpT VLeaf eval x dead_pre_map_id
  1.1745 +      dead_pre_map_comp fp_map_id dtor_unfold_unique VLeaf_map_thm eval_core_simps eval_thm;
  1.1746 +    val eval_CLeaf = derive_eval_V_or_CLeaf ctxt Y fpT CLeaf eval x dead_pre_map_id
  1.1747 +      dead_pre_map_comp fp_map_id dtor_unfold_unique CLeaf_map_thm eval_core_simps eval_thm;
  1.1748 +
  1.1749 +    val extdd_mor = derive_extdd_mor ctxt Y Z preT fpT ssig_T dead_pre_map dtor extdd cutSsig f g
  1.1750 +      dead_pre_map_comp0 dead_pre_map_comp VLeaf_map_thm ssig_map_comp flat_pointful_natural
  1.1751 +      eval_core_pointful_natural eval_thm eval_flat eval_VLeaf cutSsig_def;
  1.1752 +    val mor_cutSsig_flat = derive_mor_cutSsig_flat ctxt Y Z preT fpT ssig_T dead_pre_map
  1.1753 +      dead_ssig_map dtor flat eval_core eval cutSsig f g dead_pre_map_comp0 dead_pre_map_comp
  1.1754 +      dead_pre_map_cong dtor_unfold_unique dead_ssig_map_comp0 ssig_map_comp flat_simps
  1.1755 +      flat_pointful_natural eval_core_pointful_natural flat_flat flat_VLeaf eval_core_flat
  1.1756 +      cutSsig_def cutSsig_def_pointful_natural eval_thm;
  1.1757 +    val extdd_o_VLeaf = derive_extdd_o_VLeaf ctxt Y Z preT fpT ssig_T dead_pre_map dtor VLeaf extdd
  1.1758 +      f g dead_pre_map_comp0 dead_pre_map_comp dtor_inject ssig_map_thms eval_core_simps eval_thm
  1.1759 +      eval_VLeaf;
  1.1760 +
  1.1761 +    val (corecU_ctor, corecU_unique) = derive_corecU_ctor_unique ctxt Y Z preT fpT ssig_T
  1.1762 +      dead_pre_map ctor dtor VLeaf extdd corecU f g dead_pre_map_comp ctor_dtor dtor_unfold_thm
  1.1763 +      dtor_unfold_unique ssig_map_thms dead_ssig_map_comp0 flat_simps flat_VLeaf eval_core_simps
  1.1764 +      extdd_mor extdd_o_VLeaf cutSsig_def mor_cutSsig_flat corecU_def;
  1.1765 +
  1.1766 +    val dtor_algLam = derive_dtor_algLam ctxt Y Z preT fpT sig_T ssig_T dead_pre_map dtor
  1.1767 +      dead_sig_map Lam eval algLam x pre_map_comp dead_pre_map_id dead_pre_map_comp0
  1.1768 +      dead_pre_map_comp sig_map_comp Oper_pointful_natural ssig_map_thms dead_ssig_map_comp0
  1.1769 +      Lam_pointful_natural eval_core_simps eval_thm eval_flat eval_VLeaf algLam_def;
  1.1770 +  in
  1.1771 +    (Sig_pointful_natural, flat_pointful_natural, Lam_natural_pointful, Lam_pointful_natural,
  1.1772 +     flat_VLeaf, eval_core_pointful_natural, eval_thm, eval_flat,
  1.1773 +     [eval_Oper, eval_VLeaf, eval_CLeaf], corecU_ctor, corecU_unique, dtor_algLam)
  1.1774 +  end;
  1.1775 +
  1.1776 +fun derive_embL_natural_etc ctxt Inx_const old_ssig_bnf ssig_bnf Y Z preT fpT old_ssig_T ssig_T
  1.1777 +    dead_pre_map Sig dead_old_ssig_map embL old_algLam algLam old_flat flat old_eval_core eval_core
  1.1778 +    old_eval eval x f old_ssig_induct dead_pre_map_comp0 dead_pre_map_comp fp_map_id dtor_inject
  1.1779 +    dtor_unfold_unique Sig_pointful_natural unsig_thm sig_map_thm old_sig_map_comp old_sig_map_cong
  1.1780 +    old_ssig_map_thms old_Lam_pointful_natural Lam_def old_flat_simps flat_simps embL_simps
  1.1781 +    embL_transfer old_eval_core_simps eval_core_simps old_eval_thm eval_thm old_dtor_algLam
  1.1782 +    dtor_algLam old_algLam_thm =
  1.1783 +  let
  1.1784 +    val embL_natural = derive_natural_from_transfer ctxt [(Y, Z)] [] [] f embL embL_transfer
  1.1785 +      [old_ssig_bnf, ssig_bnf] [];
  1.1786 +
  1.1787 +    val embL_pointful_natural = mk_pointful ctxt embL_natural RS sym;
  1.1788 +    val old_algLam_pointful = mk_pointful ctxt old_algLam_thm;
  1.1789 +
  1.1790 +    val flat_embL = derive_flat_embL ctxt Y Z old_ssig_T ssig_T dead_old_ssig_map embL old_flat flat
  1.1791 +      x old_ssig_induct fp_map_id Sig_pointful_natural old_sig_map_comp old_sig_map_cong
  1.1792 +      old_ssig_map_thms old_flat_simps flat_simps embL_simps;
  1.1793 +    val eval_core_embL = derive_eval_core_embL ctxt Y Z preT old_ssig_T ssig_T dead_pre_map embL
  1.1794 +      old_eval_core eval_core x old_ssig_induct dead_pre_map_comp0 dead_pre_map_comp
  1.1795 +      Sig_pointful_natural unsig_thm old_sig_map_comp old_sig_map_cong old_Lam_pointful_natural
  1.1796 +      Lam_def flat_embL embL_simps embL_pointful_natural old_eval_core_simps eval_core_simps;
  1.1797 +    val eval_embL = derive_eval_embL ctxt Y fpT embL old_eval eval dead_pre_map_comp0
  1.1798 +      dtor_unfold_unique embL_pointful_natural eval_core_embL old_eval_thm eval_thm;
  1.1799 +
  1.1800 +    val algLam_algLam = derive_algLam_algLam ctxt Inx_const Y fpT Sig old_algLam algLam
  1.1801 +      dead_pre_map_comp dtor_inject unsig_thm sig_map_thm Lam_def eval_embL old_dtor_algLam
  1.1802 +      dtor_algLam;
  1.1803 +  in
  1.1804 +    (embL_pointful_natural, old_algLam_pointful, eval_embL, algLam_algLam)
  1.1805 +  end;
  1.1806 +
  1.1807 +fun define_corecUU_etc fp_b version live_AsBs Y Z preT fpT ssig_T pre_map dead_pre_map pre_rel
  1.1808 +    fp_rel ctor Oper ssig_map dead_ssig_map ssig_rel proto_sctr flat eval_core eval corecU fs f g Rs
  1.1809 +    R pre_map_transfer fp_k_T_rel_eqs dtor_unfold_transfer dtor_transfer ssig_map_transfer
  1.1810 +    proto_sctr_transfer proto_sctr_pointful_natural flat_transfer flat_pointful_natural
  1.1811 +    eval_core_transfer eval_core_pointful_natural eval_thm eval_flat eval_Oper algLam_thm
  1.1812 +    cutSsig_def corecU_def corecU_ctor corecU_unique pre_bnf dead_pre_bnf fp_res ssig_fp_sugar
  1.1813 +    lthy =
  1.1814 +  let
  1.1815 +    val ssig_bnf = #fp_bnf ssig_fp_sugar;
  1.1816 +
  1.1817 +    val dead_pre_map_comp0 = map_comp0_of_bnf dead_pre_bnf;
  1.1818 +    val dead_pre_map_comp = map_comp_of_bnf dead_pre_bnf;
  1.1819 +    val [dtor_ctor] = #dtor_ctors fp_res;
  1.1820 +    val [dtor_inject] = #dtor_injects fp_res;
  1.1821 +    val ssig_map_comp = map_comp_of_bnf ssig_bnf;
  1.1822 +
  1.1823 +    val sctr_rhs = HOLogic.mk_comp (Oper, substT Y ssig_T proto_sctr);
  1.1824 +    val ((sctr, sctr_def), lthy) = lthy
  1.1825 +      |> define_const true fp_b version sctrN sctr_rhs;
  1.1826 +
  1.1827 +    val (corecUU_data as (corecUU, corecUU_def), lthy) = lthy
  1.1828 +      |> define_corecUU fp_b version Y Z preT ssig_T dead_pre_map dead_ssig_map flat eval_core sctr
  1.1829 +        corecU;
  1.1830 +
  1.1831 +    val eval_sctr = derive_eval_sctr lthy Y Z fpT ssig_T dead_pre_map ctor eval sctr
  1.1832 +      proto_sctr_pointful_natural eval_Oper algLam_thm sctr_def;
  1.1833 +
  1.1834 +    val sctr_transfer = derive_sctr_transfer lthy live_AsBs Y Z ssig_T Rs R pre_rel ssig_rel sctr
  1.1835 +      sctr_def fp_k_T_rel_eqs [proto_sctr_transfer];
  1.1836 +
  1.1837 +    val sctr_natural = derive_natural_from_transfer_with_pre_type lthy live_AsBs Y Z preT ssig_T
  1.1838 +      pre_map ssig_map fs f sctr sctr_transfer [pre_bnf, ssig_bnf] [];
  1.1839 +
  1.1840 +    val sctr_pointful_natural = mk_pointful lthy sctr_natural RS sym;
  1.1841 +    val eval_sctr_pointful = mk_pointful lthy eval_sctr RS sym;
  1.1842 +
  1.1843 +    val (corecUU_pointfree, corecUU_unique) = derive_corecUU_pointfree_unique lthy Y Z preT fpT
  1.1844 +      ssig_T dead_pre_map ctor dead_ssig_map eval corecUU f g dead_pre_map_comp0 dead_pre_map_comp
  1.1845 +      dtor_ctor dtor_inject ssig_map_comp flat_pointful_natural eval_core_pointful_natural eval_thm
  1.1846 +      eval_flat corecU_ctor corecU_unique sctr_pointful_natural eval_sctr_pointful corecUU_def;
  1.1847 +
  1.1848 +    val corecUU_thm = mk_pointful lthy corecUU_pointfree;
  1.1849 +
  1.1850 +    val corecUU_transfer = derive_corecUU_transfer lthy live_AsBs Y Z Rs R preT ssig_T pre_rel
  1.1851 +      fp_rel ssig_rel corecUU cutSsig_def corecU_def corecUU_def fp_k_T_rel_eqs
  1.1852 +      [pre_map_transfer, dtor_unfold_transfer, dtor_transfer, ssig_map_transfer, flat_transfer,
  1.1853 +       eval_core_transfer, sctr_transfer, @{thm convol_transfer} (*FIXME: needed?*)];
  1.1854 +  in
  1.1855 +    ((corecUU_data, corecUU_thm, corecUU_unique, corecUU_transfer, eval_sctr, sctr_transfer,
  1.1856 +      sctr_pointful_natural), lthy)
  1.1857 +  end;
  1.1858 +
  1.1859 +fun mk_equivp T = Const (@{const_name equivp}, mk_predT [mk_pred2T T T]);
  1.1860 +
  1.1861 +fun derive_equivp_Retr ctxt fpT Retr R dead_pre_rel_refl_thm dead_pre_rel_flip_thm
  1.1862 +    dead_pre_rel_mono_thm dead_pre_rel_compp_thm =
  1.1863 +  let
  1.1864 +    val prem = HOLogic.mk_Trueprop (mk_equivp fpT $ R);
  1.1865 +    val goal = Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_equivp fpT $ (betapply (Retr, R))));
  1.1866 +  in
  1.1867 +    Variable.add_free_names ctxt goal []
  1.1868 +    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1.1869 +      mk_equivp_Retr_tac ctxt dead_pre_rel_refl_thm dead_pre_rel_flip_thm dead_pre_rel_mono_thm
  1.1870 +        dead_pre_rel_compp_thm))
  1.1871 +    |> Thm.close_derivation
  1.1872 +  end;
  1.1873 +
  1.1874 +fun derive_Retr_coinduct ctxt fpT Retr R dtor_rel_coinduct_thm rel_eq_thm =
  1.1875 +  let
  1.1876 +    val goal = HOLogic.mk_Trueprop (list_all_free [R]
  1.1877 +      (HOLogic.mk_imp (mk_leq R (Retr $ R), mk_leq R (HOLogic.eq_const fpT))));
  1.1878 +  in
  1.1879 +    Goal.prove_sorry ctxt [] [] goal (fn {context = ctxt, prems = _} =>
  1.1880 +      mk_Retr_coinduct_tac ctxt dtor_rel_coinduct_thm rel_eq_thm)
  1.1881 +    |> Thm.close_derivation
  1.1882 +  end;
  1.1883 +
  1.1884 +fun derive_Retr fp_sugar fpT dead_pre_bnf ctor dtor names_lthy lthy =
  1.1885 +  let
  1.1886 +    val (R, _) = names_lthy
  1.1887 +      |> yield_singleton (mk_Frees "R") (mk_pred2T fpT fpT);
  1.1888 +    val pre_fpT = pre_type_of_ctor fpT ctor;
  1.1889 +    val fp_pre_rel = mk_rel1 lthy fpT fpT pre_fpT dead_pre_bnf;
  1.1890 +    val Retr = Abs ("R", fastype_of R, Abs ("a", fpT,
  1.1891 +      Abs ("b", fpT, list_comb (fp_pre_rel, [Bound 2, dtor $ Bound 1, dtor $ Bound 0]))));
  1.1892 +    val equivp_Retr = derive_equivp_Retr lthy fpT Retr R (rel_refl_of_bnf dead_pre_bnf)
  1.1893 +      (rel_flip_of_bnf dead_pre_bnf) (rel_mono_of_bnf dead_pre_bnf) (rel_OO_of_bnf dead_pre_bnf);
  1.1894 +
  1.1895 +    val Retr_coinduct = derive_Retr_coinduct lthy fpT Retr R
  1.1896 +      (fp_sugar |> #fp_res |> #xtor_rel_co_induct) (fp_sugar |> #fp_bnf |> rel_eq_of_bnf);
  1.1897 +  in
  1.1898 +    (Retr, equivp_Retr, Retr_coinduct)
  1.1899 +  end;
  1.1900 +
  1.1901 +fun mk_gen_cong fpT eval_domT =
  1.1902 +  let val fp_relT = mk_pred2T fpT fpT in
  1.1903 +    Const (@{const_name "cong.gen_cong"},
  1.1904 +      [mk_predT [fp_relT, eval_domT, eval_domT], eval_domT --> fpT, fp_relT] ---> fp_relT)
  1.1905 +  end;
  1.1906 +
  1.1907 +fun mk_cong_locale rel eval Retr =
  1.1908 +  Const (@{const_name cong}, mk_predT (map fastype_of [rel, eval, Retr]));
  1.1909 +
  1.1910 +fun derive_cong_locale ctxt rel eval Retr0 tac =
  1.1911 +  let
  1.1912 +    val Retr = enforce_type ctxt domain_type (domain_type (fastype_of rel)) Retr0;
  1.1913 +    val goal = HOLogic.mk_Trueprop (list_comb (mk_cong_locale rel eval Retr, [rel, eval, Retr]));
  1.1914 +  in
  1.1915 +    Variable.add_free_names ctxt goal []
  1.1916 +    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} => tac ctxt))
  1.1917 +    |> Thm.close_derivation
  1.1918 +  end;
  1.1919 +
  1.1920 +fun derive_cong_general fp_b version fpT dead_ssig_bnf dead_pre_bnf eval Retr equivp_Retr
  1.1921 +    Retr_coinduct eval_thm eval_core_transfer lthy =
  1.1922 +  let
  1.1923 +    val eval_domT = domain_type (fastype_of eval);
  1.1924 +
  1.1925 +    fun cong_locale_tac ctxt =
  1.1926 +      mk_cong_locale_tac ctxt (rel_mono_of_bnf dead_pre_bnf) (rel_map_of_bnf dead_pre_bnf)
  1.1927 +        equivp_Retr (rel_mono_of_bnf dead_ssig_bnf) (rel_map_of_bnf dead_ssig_bnf) eval_thm
  1.1928 +        eval_core_transfer;
  1.1929 +
  1.1930 +    val rel = mk_rel1 lthy fpT fpT eval_domT dead_ssig_bnf;
  1.1931 +    val cong_rhs = list_comb (mk_gen_cong fpT eval_domT, [rel, eval]);
  1.1932 +    val ((_, cong_def), lthy) = lthy
  1.1933 +      |> define_const false fp_b version congN cong_rhs;
  1.1934 +
  1.1935 +    val cong_locale = derive_cong_locale lthy rel eval Retr cong_locale_tac;
  1.1936 +
  1.1937 +    val fold_cong_def = fold_thms lthy [cong_def];
  1.1938 +
  1.1939 +    fun instance_of_gen thm = fold_cong_def (thm OF [cong_locale]);
  1.1940 +
  1.1941 +    val cong_base = instance_of_gen @{thm cong.imp_gen_cong};
  1.1942 +    val cong_refl = instance_of_gen @{thm cong.gen_cong_reflp};
  1.1943 +    val cong_sym = instance_of_gen @{thm cong.gen_cong_symp};
  1.1944 +    val cong_trans = instance_of_gen @{thm cong.gen_cong_transp};
  1.1945 +
  1.1946 +    fun mk_cong_rho thm = thm RS instance_of_gen @{thm cong.gen_cong_rho};
  1.1947 +
  1.1948 +    val dtor_coinduct = @{thm predicate2I_obj} RS
  1.1949 +      (Retr_coinduct RS instance_of_gen @{thm cong.coinduction} RS @{thm predicate2D_obj});
  1.1950 +  in
  1.1951 +    (cong_def, cong_locale, cong_base, cong_refl, cong_sym, cong_trans, dtor_coinduct, mk_cong_rho,
  1.1952 +     lthy)
  1.1953 +  end;
  1.1954 +
  1.1955 +fun derive_cong_base fp_b version fpT dead_ssig_bnf ssig_fp_bnf_sugar dead_pre_bnf eval eval_thm
  1.1956 +    eval_core_transfer eval_VLeaf eval_sctr sctr_transfer Retr equivp_Retr Retr_coinduct lthy =
  1.1957 +  let
  1.1958 +    val (cong_def, cong_locale, cong_base, cong_refl, cong_sym, cong_trans, dtor_coinduct,
  1.1959 +         mk_cong_rho, lthy) =
  1.1960 +      derive_cong_general fp_b version fpT dead_ssig_bnf dead_pre_bnf eval Retr equivp_Retr
  1.1961 +        Retr_coinduct eval_thm eval_core_transfer lthy;
  1.1962 +
  1.1963 +    val dead_pre_map_id0 = map_id0_of_bnf dead_pre_bnf;
  1.1964 +    val dead_pre_map_comp0 = map_comp0_of_bnf dead_pre_bnf;
  1.1965 +    val dead_pre_map_cong0 = map_cong0_of_bnf dead_pre_bnf;
  1.1966 +    val dead_pre_map_cong0' =
  1.1967 +      @{thm box_equals[OF _ o_apply[symmetric] id_apply[symmetric]]} RS dead_pre_map_cong0 RS ext;
  1.1968 +    val dead_pre_rel_map = rel_map_of_bnf dead_pre_bnf;
  1.1969 +
  1.1970 +    val ctor_alt_thm = eval_VLeaf RS (@{thm eq_comp_compI} OF [eval_sctr,
  1.1971 +      trans OF [dead_pre_map_comp0 RS sym, trans OF [dead_pre_map_cong0', dead_pre_map_id0]]]);
  1.1972 +
  1.1973 +    val cong_ctor_intro = mk_cong_rho ctor_alt_thm
  1.1974 +      |> unfold_thms lthy [o_apply]
  1.1975 +      |> (fn thm => sctr_transfer RS rel_funD RS thm)
  1.1976 +      |> unfold_thms lthy (id_apply :: dead_pre_rel_map @ #rel_injects ssig_fp_bnf_sugar);
  1.1977 +  in
  1.1978 +    ({cong_def = cong_def, cong_locale = cong_locale, cong_base = cong_base, cong_refl = cong_refl,
  1.1979 +      cong_sym = cong_sym, cong_trans = cong_trans, dtor_coinduct = dtor_coinduct,
  1.1980 +      cong_alg_intros = [cong_ctor_intro]}, lthy)
  1.1981 +  end;
  1.1982 +
  1.1983 +fun update_cong_alg_intros ctxt cong_def cong_locale old_cong_def old_cong_locale emb =
  1.1984 +  let
  1.1985 +    fun instance_of_gen thm = fold_thms ctxt [cong_def] (thm OF [cong_locale]);
  1.1986 +    fun instance_of_old_gen thm = fold_thms ctxt [old_cong_def] (thm OF [old_cong_locale]);
  1.1987 +
  1.1988 +    val emb_idem = @{thm ord_le_eq_trans} OF [emb, instance_of_gen @{thm cong.gen_cong_idem}];
  1.1989 +    fun mk_rel_mono bnf = instance_of_old_gen @{thm cong.leq_gen_cong} RS rel_mono_of_bnf bnf RS
  1.1990 +      @{thm predicate2D};
  1.1991 +    fun mk_intro bnf thm = mk_rel_mono bnf RS (@{thm predicate2D} OF [emb_idem, thm]);
  1.1992 +  in
  1.1993 +    map2 mk_intro
  1.1994 +  end
  1.1995 +
  1.1996 +fun derive_cong_step fp_b version fpT dead_ssig_bnf dead_pre_bnf eval eval_thm eval_core_transfer
  1.1997 +    old_dtor_coinduct_info algrho_def k_as_ssig_transfer Retr equivp_Retr Retr_coinduct
  1.1998 +    eval_embL embL_transfer old_all_dead_k_bnfs lthy =
  1.1999 +  let
  1.2000 +    val old_cong_def = #cong_def old_dtor_coinduct_info;
  1.2001 +    val old_cong_locale = #cong_locale old_dtor_coinduct_info;
  1.2002 +    val old_cong_alg_intros = #cong_alg_intros old_dtor_coinduct_info;
  1.2003 +
  1.2004 +    val (cong_def, cong_locale, cong_base, cong_refl, cong_sym, cong_trans, dtor_coinduct,
  1.2005 +         mk_cong_rho, lthy) =
  1.2006 +      derive_cong_general fp_b version fpT dead_ssig_bnf dead_pre_bnf eval Retr equivp_Retr
  1.2007 +        Retr_coinduct eval_thm eval_core_transfer lthy;
  1.2008 +
  1.2009 +    val cong_alg_intro =
  1.2010 +      k_as_ssig_transfer RS rel_funD RS mk_cong_rho (algrho_def RS meta_eq_to_obj_eq);
  1.2011 +
  1.2012 +    val gen_cong_emb =
  1.2013 +      (@{thm gen_cong_emb} OF [old_cong_locale, cong_locale, eval_embL, embL_transfer])
  1.2014 +      |> fold_thms lthy [old_cong_def, cong_def];
  1.2015 +
  1.2016 +    val cong_alg_intros = update_cong_alg_intros lthy cong_def cong_locale old_cong_def
  1.2017 +      old_cong_locale gen_cong_emb old_all_dead_k_bnfs old_cong_alg_intros;
  1.2018 +  in
  1.2019 +    ({cong_def = cong_def, cong_locale = cong_locale, cong_base = cong_base, cong_refl = cong_refl,
  1.2020 +      cong_sym = cong_sym, cong_trans = cong_trans, dtor_coinduct = dtor_coinduct,
  1.2021 +      cong_alg_intros = cong_alg_intro :: cong_alg_intros}, lthy)
  1.2022 +  end;
  1.2023 +
  1.2024 +fun derive_cong_merge fp_b version fpT old1_friend_names old2_friend_names dead_ssig_bnf
  1.2025 +    dead_pre_bnf eval eval_thm eval_core_transfer old1_dtor_coinduct_info old2_dtor_coinduct_info
  1.2026 +    Retr equivp_Retr Retr_coinduct eval_embLL embLL_transfer eval_embLR embLR_transfer
  1.2027 +    old1_all_dead_k_bnfs old2_all_dead_k_bnfs lthy =
  1.2028 +  let
  1.2029 +    val old1_cong_def = #cong_def old1_dtor_coinduct_info;
  1.2030 +    val old1_cong_locale = #cong_locale old1_dtor_coinduct_info;
  1.2031 +    val old1_cong_alg_intros = #cong_alg_intros old1_dtor_coinduct_info;
  1.2032 +    val old2_cong_def = #cong_def old2_dtor_coinduct_info;
  1.2033 +    val old2_cong_locale = #cong_locale old2_dtor_coinduct_info;
  1.2034 +    val old2_cong_alg_intros = #cong_alg_intros old2_dtor_coinduct_info;
  1.2035 +
  1.2036 +    val (cong_def, cong_locale, cong_base, cong_refl, cong_sym, cong_trans, dtor_coinduct, _,
  1.2037 +         lthy) =
  1.2038 +      derive_cong_general fp_b version fpT dead_ssig_bnf dead_pre_bnf eval Retr equivp_Retr
  1.2039 +        Retr_coinduct eval_thm eval_core_transfer lthy;
  1.2040 +
  1.2041 +    val emb1 = (@{thm gen_cong_emb} OF [old1_cong_locale, cong_locale, eval_embLL, embLL_transfer])
  1.2042 +      |> fold_thms lthy [old1_cong_def, cong_def];
  1.2043 +    val emb2 = (@{thm gen_cong_emb} OF [old2_cong_locale, cong_locale, eval_embLR, embLR_transfer])
  1.2044 +      |> fold_thms lthy [old2_cong_def, cong_def];
  1.2045 +
  1.2046 +    val cong_alg_intros1 = update_cong_alg_intros lthy cong_def cong_locale old1_cong_def
  1.2047 +      old1_cong_locale emb1 old1_all_dead_k_bnfs old1_cong_alg_intros;
  1.2048 +    val cong_alg_intros2 = update_cong_alg_intros lthy cong_def cong_locale old2_cong_def
  1.2049 +      old2_cong_locale emb2 old2_all_dead_k_bnfs old2_cong_alg_intros;
  1.2050 +
  1.2051 +    val (cong_algrho_intros1, cong_ctor_intro1) = split_last cong_alg_intros1;
  1.2052 +    val (cong_algrho_intros2, _) = split_last cong_alg_intros2;
  1.2053 +    val (old1_all_rho_k_bnfs, old1_Sig_bnf) = split_last old1_all_dead_k_bnfs;
  1.2054 +    val (old2_all_rho_k_bnfs, _) = split_last old2_all_dead_k_bnfs;
  1.2055 +
  1.2056 +    val (friend_names, (cong_algrho_intros, all_rho_k_bnfs)) =
  1.2057 +      merge_lists (op = o apply2 fst)
  1.2058 +        (old1_friend_names ~~ (cong_algrho_intros1 ~~ old1_all_rho_k_bnfs))
  1.2059 +        (old2_friend_names ~~ (cong_algrho_intros2 ~~ old2_all_rho_k_bnfs))
  1.2060 +      |> split_list ||> split_list;
  1.2061 +  in
  1.2062 +    (({cong_def = cong_def, cong_locale = cong_locale, cong_base = cong_base, cong_refl = cong_refl,
  1.2063 +       cong_sym = cong_sym, cong_trans = cong_trans, dtor_coinduct = dtor_coinduct,
  1.2064 +       cong_alg_intros = cong_algrho_intros @ [cong_ctor_intro1]}, all_rho_k_bnfs @ [old1_Sig_bnf],
  1.2065 +       friend_names), lthy)
  1.2066 +  end;
  1.2067 +
  1.2068 +fun derive_corecUU_base fpT_name lthy =
  1.2069 +  let
  1.2070 +    val fp_sugar as {T = Type (_, fpT_args0), pre_bnf, fp_bnf, fp_res, ...} =
  1.2071 +      checked_fp_sugar_of lthy fpT_name;
  1.2072 +    val num_fp_tyargs = length fpT_args0;
  1.2073 +    val fp_alives = liveness_of_fp_bnf num_fp_tyargs fp_bnf;
  1.2074 +
  1.2075 +    val (((Es, Fs0), [Y, Z]), names_lthy) = lthy
  1.2076 +      |> mk_TFrees num_fp_tyargs
  1.2077 +      ||>> mk_TFrees num_fp_tyargs
  1.2078 +      ||>> mk_TFrees 2;
  1.2079 +    val Fs = @{map 3} (fn alive => fn E => fn F => if alive then F else E) fp_alives Es Fs0;
  1.2080 +
  1.2081 +    val As = Es @ [Y];
  1.2082 +    val Bs = Es @ [Z];
  1.2083 +
  1.2084 +    val live_EsFs = filter (op <>) (Es ~~ Fs);
  1.2085 +    val live_AsBs = live_EsFs @ [(Y, Z)];
  1.2086 +    val fTs = map (op -->) live_EsFs;
  1.2087 +    val RTs = map (uncurry mk_pred2T) live_EsFs;
  1.2088 +    val live = length live_EsFs;
  1.2089 +
  1.2090 +    val ((((((x, fs), f), g), Rs), R), names_lthy) = names_lthy
  1.2091 +      |> yield_singleton (mk_Frees "x") Y
  1.2092 +      ||>> mk_Frees "f" fTs
  1.2093 +      ||>> yield_singleton (mk_Frees "f") (Y --> Z)
  1.2094 +      ||>> yield_singleton (mk_Frees "g") (Y --> Z)
  1.2095 +      ||>> mk_Frees "R" RTs
  1.2096 +      ||>> yield_singleton (mk_Frees "R") (mk_pred2T Y Z);
  1.2097 +
  1.2098 +    val ctor = mk_ctor Es (the_single (#ctors fp_res));
  1.2099 +    val dtor = mk_dtor Es (the_single (#dtors fp_res));
  1.2100 +
  1.2101 +    val fpT = Type (fpT_name, Es);
  1.2102 +    val preT = pre_type_of_ctor Y ctor;
  1.2103 +
  1.2104 +    val ((fp_b, version), lthy) = lthy |> get_name_next_version_of fpT_name;
  1.2105 +
  1.2106 +    val ((sig_fp_sugar, ssig_fp_sugar), lthy) = lthy
  1.2107 +      |> define_sig_type fp_b version fp_alives Es Y preT
  1.2108 +      ||>> define_ssig_type fp_b version fp_alives Es Y fpT;
  1.2109 +
  1.2110 +    val sig_bnf = #fp_bnf sig_fp_sugar;
  1.2111 +    val ssig_bnf = #fp_bnf ssig_fp_sugar;
  1.2112 +
  1.2113 +    val (((dead_pre_bnf, dead_sig_bnf), dead_ssig_bnf), lthy) = lthy
  1.2114 +      |> bnf_kill_all_but 1 pre_bnf
  1.2115 +      ||>> bnf_kill_all_but 1 sig_bnf
  1.2116 +      ||>> bnf_kill_all_but 1 ssig_bnf;
  1.2117 +
  1.2118 +    val sig_fp_ctr_sugar = #fp_ctr_sugar sig_fp_sugar;
  1.2119 +    val ssig_fp_ctr_sugar = #fp_ctr_sugar ssig_fp_sugar;
  1.2120 +
  1.2121 +    val sig_fp_bnf_sugar = #fp_bnf_sugar sig_fp_sugar;
  1.2122 +    val ssig_fp_bnf_sugar = #fp_bnf_sugar ssig_fp_sugar;
  1.2123 +    val ssig_fp_induct_sugar = #fp_co_induct_sugar ssig_fp_sugar;
  1.2124 +
  1.2125 +    val sig_ctr_sugar = #ctr_sugar sig_fp_ctr_sugar;
  1.2126 +    val ssig_ctr_sugar = #ctr_sugar ssig_fp_ctr_sugar;
  1.2127 +
  1.2128 +    val sig_T_name = fst (dest_Type (#T sig_fp_sugar));
  1.2129 +    val ssig_T_name = fst (dest_Type (#T ssig_fp_sugar));
  1.2130 +
  1.2131 +    val sig_T = Type (sig_T_name, As);
  1.2132 +    val ssig_T = Type (ssig_T_name, As);
  1.2133 +
  1.2134 +    val pre_map = mk_mapN lthy live_AsBs preT pre_bnf;
  1.2135 +    val pre_rel = mk_relN lthy live_AsBs preT pre_bnf;
  1.2136 +    val dead_pre_map = mk_map1 lthy Y Z preT dead_pre_bnf;
  1.2137 +    val fp_rel = mk_relN lthy live_EsFs fpT fp_bnf;
  1.2138 +    val dtor_unfold = mk_co_rec (Proof_Context.theory_of lthy) Greatest_FP [Z] fpT
  1.2139 +      (the_single (#xtor_un_folds fp_res));
  1.2140 +    val Sig = mk_ctr As (the_single (#ctrs sig_ctr_sugar));
  1.2141 +    val unsig = mk_disc_or_sel As (the_single (the_single (#selss sig_ctr_sugar)));
  1.2142 +    val sig_rel = mk_relN lthy live_AsBs sig_T sig_bnf;
  1.2143 +    val dead_sig_map = mk_map 1 As Bs (map_of_bnf dead_sig_bnf);
  1.2144 +    val [Oper, VLeaf, CLeaf] = map (mk_ctr As) (#ctrs ssig_ctr_sugar);
  1.2145 +    val ssig_map = mk_mapN lthy live_AsBs ssig_T ssig_bnf;
  1.2146 +    val ssig_rel = mk_relN lthy live_AsBs ssig_T ssig_bnf;
  1.2147 +    val dead_ssig_map = mk_map 1 As Bs (map_of_bnf dead_ssig_bnf);
  1.2148 +    val dead_ssig_rel = mk_rel 1 As Bs (rel_of_bnf dead_ssig_bnf);
  1.2149 +
  1.2150 +    val ((Lam, Lam_def), lthy) = lthy
  1.2151 +      |> define_Lam_base fp_b version Y Z preT ssig_T dead_pre_map Sig unsig dead_sig_map Oper
  1.2152 +        VLeaf;
  1.2153 +
  1.2154 +    val proto_sctr = Sig;
  1.2155 +
  1.2156 +    val pre_map_transfer = map_transfer_of_bnf pre_bnf;
  1.2157 +    val pre_rel_def = rel_def_of_bnf pre_bnf;
  1.2158 +    val dead_pre_map_id = map_id_of_bnf dead_pre_bnf;
  1.2159 +    val dead_pre_map_comp = map_comp_of_bnf dead_pre_bnf;
  1.2160 +    val fp_rel_eq = rel_eq_of_bnf fp_bnf;
  1.2161 +    val [ctor_dtor] = #ctor_dtors fp_res;
  1.2162 +    val [dtor_ctor] = #dtor_ctors fp_res;
  1.2163 +    val [dtor_inject] = #dtor_injects fp_res;
  1.2164 +    val [dtor_unfold_thm] = #xtor_un_fold_thms fp_res;
  1.2165 +    val [dtor_unfold_unique] = #xtor_un_fold_uniques fp_res;
  1.2166 +    val [dtor_unfold_transfer] = #xtor_un_fold_transfers fp_res;
  1.2167 +    val [dtor_rel_thm] = #xtor_rels fp_res;
  1.2168 +    val unsig_thm = the_single (the_single (#sel_thmss sig_ctr_sugar));
  1.2169 +    val [sig_map_thm] = #map_thms sig_fp_bnf_sugar;
  1.2170 +    val [Oper_map_thm, VLeaf_map_thm, CLeaf_map_thm] = #map_thms ssig_fp_bnf_sugar;
  1.2171 +    val sig_map_transfer = map_transfer_of_bnf sig_bnf;
  1.2172 +    val ssig_map_thms = #map_thms ssig_fp_bnf_sugar;
  1.2173 +    val ssig_map_transfer = map_transfer_of_bnf ssig_bnf;
  1.2174 +    val ssig_induct = the_single (#co_inducts ssig_fp_induct_sugar);
  1.2175 +
  1.2176 +    val dtor_transfer = derive_dtor_transfer lthy live_EsFs Y Z pre_rel fp_rel Rs dtor dtor_rel_thm;
  1.2177 +    val preT_rel_eqs = map rel_eq_of_bnf (map_filter (bnf_of lthy) (add_type_namesT preT []));
  1.2178 +
  1.2179 +    val Sig_transfer = derive_sig_transfer I lthy live_AsBs pre_rel sig_rel Rs R Sig pre_rel_def
  1.2180 +      preT_rel_eqs (the_single (#ctr_transfers sig_fp_ctr_sugar));
  1.2181 +    val proto_sctr_transfer = Sig_transfer;
  1.2182 +    val unsig_transfer = derive_sig_transfer swap lthy live_AsBs pre_rel sig_rel Rs R unsig
  1.2183 +      pre_rel_def preT_rel_eqs (the_single (#sel_transfers sig_fp_ctr_sugar));
  1.2184 +    val Lam_transfer = derive_Lam_or_eval_core_transfer lthy live_AsBs Y Z preT ssig_T Rs R pre_rel
  1.2185 +      sig_rel ssig_rel Lam Lam_def []
  1.2186 +      [pre_map_transfer, sig_map_transfer, Sig_transfer, unsig_transfer];
  1.2187 +
  1.2188 +    val ((((((((flat, _, flat_simps), flat_transfer),
  1.2189 +            ((eval_core, _, eval_core_simps), eval_core_transfer)), (eval, eval_def)),
  1.2190 +          (cutSsig, cutSsig_def)), (algLam, algLam_def)), (corecU, corecU_def)), lthy) = lthy
  1.2191 +      |> define_flat_etc fp_b version live_AsBs Y Z preT fpT sig_T ssig_T Oper VLeaf CLeaf pre_rel
  1.2192 +        dead_pre_map dtor dtor_unfold dead_sig_map ssig_rel dead_ssig_map Lam Rs R pre_map_transfer
  1.2193 +        [fp_rel_eq] sig_map_transfer ssig_map_transfer Lam_transfer dtor_transfer;
  1.2194 +
  1.2195 +    val (Sig_pointful_natural, flat_pointful_natural, _, Lam_pointful_natural, _,
  1.2196 +         eval_core_pointful_natural, eval_thm, eval_flat, eval_simps as [eval_Oper, eval_VLeaf, _],
  1.2197 +         corecU_ctor, corecU_unique, dtor_algLam) =
  1.2198 +      derive_Sig_natural_etc lthy live live_AsBs Y Z preT fpT fpT sig_T ssig_T pre_map dead_pre_map
  1.2199 +        ctor dtor Sig dead_sig_map Oper VLeaf CLeaf ssig_map dead_ssig_map Lam flat eval_core eval
  1.2200 +        cutSsig algLam corecU x fs f g ctor_dtor dtor_inject dtor_unfold_thm dtor_unfold_unique
  1.2201 +        sig_map_thm ssig_induct ssig_map_thms Oper_map_thm VLeaf_map_thm CLeaf_map_thm Lam_transfer
  1.2202 +        flat_simps flat_transfer eval_core_simps eval_core_transfer eval_def cutSsig_def algLam_def
  1.2203 +        corecU_def pre_bnf pre_bnf dead_pre_bnf fp_bnf sig_bnf ssig_bnf dead_ssig_bnf;
  1.2204 +
  1.2205 +    val proto_sctr_pointful_natural = Sig_pointful_natural;
  1.2206 +
  1.2207 +    val algLam_thm = derive_algLam_base lthy Y Z preT fpT dead_pre_map ctor dtor algLam proto_sctr
  1.2208 +      dead_pre_map_id dead_pre_map_comp ctor_dtor dtor_ctor dtor_unfold_unique unsig_thm
  1.2209 +      Sig_pointful_natural ssig_map_thms Lam_def flat_simps eval_core_simps eval_thm algLam_def;
  1.2210 +
  1.2211 +    val (((corecUU, _), corecUU_thm, corecUU_unique, corecUU_transfer, eval_sctr, sctr_transfer,
  1.2212 +          sctr_pointful_natural), lthy) = lthy
  1.2213 +      |> define_corecUU_etc fp_b version live_AsBs Y Z preT fpT ssig_T pre_map dead_pre_map pre_rel
  1.2214 +        fp_rel ctor Oper ssig_map dead_ssig_map ssig_rel proto_sctr flat eval_core eval corecU fs f
  1.2215 +        g Rs R pre_map_transfer [] dtor_unfold_transfer dtor_transfer ssig_map_transfer
  1.2216 +        proto_sctr_transfer proto_sctr_pointful_natural flat_transfer flat_pointful_natural
  1.2217 +        eval_core_transfer eval_core_pointful_natural eval_thm eval_flat eval_Oper algLam_thm
  1.2218 +        cutSsig_def corecU_def corecU_ctor corecU_unique pre_bnf dead_pre_bnf fp_res ssig_fp_sugar;
  1.2219 +
  1.2220 +    val (Retr, equivp_Retr, Retr_coinduct) = lthy
  1.2221 +      |> derive_Retr fp_sugar fpT dead_pre_bnf ctor dtor names_lthy;
  1.2222 +
  1.2223 +    val (dtor_coinduct_info, lthy) = lthy
  1.2224 +      |> derive_cong_base fp_b version fpT dead_ssig_bnf ssig_fp_bnf_sugar dead_pre_bnf eval
  1.2225 +      eval_thm eval_core_transfer eval_VLeaf eval_sctr sctr_transfer Retr equivp_Retr Retr_coinduct;
  1.2226 +
  1.2227 +    val buffer =
  1.2228 +      {Oper = Oper, VLeaf = VLeaf, CLeaf = CLeaf, ctr_wrapper = Sig, friends = Symtab.empty};
  1.2229 +
  1.2230 +    val notes =
  1.2231 +      [(corecUU_transferN, [corecUU_transfer])] @
  1.2232 +      (if Config.get lthy bnf_internals then
  1.2233 +         [(algLamN, [algLam_thm]),
  1.2234 +          (cong_alg_introsN, #cong_alg_intros dtor_coinduct_info),
  1.2235 +          (cong_localeN, [#cong_locale dtor_coinduct_info]),
  1.2236 +          (corecU_ctorN, [corecU_ctor]),
  1.2237 +          (corecU_uniqueN, [corecU_unique]),
  1.2238 +          (corecUUN, [corecUU_thm]),
  1.2239 +          (corecUU_uniqueN, [corecUU_unique]),
  1.2240 +          (dtor_algLamN, [dtor_algLam]),
  1.2241 +          (dtor_coinductN, [#dtor_coinduct dtor_coinduct_info]),
  1.2242 +          (dtor_transferN, [dtor_transfer]),
  1.2243 +          (equivp_RetrN, [equivp_Retr]),
  1.2244 +          (evalN, [eval_thm]),
  1.2245 +          (eval_core_pointful_naturalN, [eval_core_pointful_natural]),
  1.2246 +          (eval_core_transferN, [eval_core_transfer]),
  1.2247 +          (eval_flatN, [eval_flat]),
  1.2248 +          (eval_simpsN, eval_simps),
  1.2249 +          (flat_pointful_naturalN, [flat_pointful_natural]),
  1.2250 +          (flat_transferN, [flat_transfer]),
  1.2251 +          (Lam_pointful_naturalN, [Lam_pointful_natural]),
  1.2252 +          (Lam_transferN, [Lam_transfer]),
  1.2253 +          (proto_sctr_pointful_naturalN, [proto_sctr_pointful_natural]),
  1.2254 +          (proto_sctr_transferN, [proto_sctr_transfer]),
  1.2255 +          (Retr_coinductN, [Retr_coinduct]),
  1.2256 +          (sctr_pointful_naturalN, [sctr_pointful_natural]),
  1.2257 +          (sctr_transferN, [sctr_transfer]),
  1.2258 +          (Sig_pointful_naturalN, [Sig_pointful_natural])]
  1.2259 +        else
  1.2260 +          [])
  1.2261 +      |> map (fn (thmN, thms) =>
  1.2262 +        ((mk_version_fp_binding true lthy version fp_b thmN, []), [(thms, [])]));
  1.2263 +  in
  1.2264 +    ({fp_b = fp_b, version = version, fpT = fpT, Y = Y, Z = Z, friend_names = [],
  1.2265 +      sig_fp_sugars = [sig_fp_sugar], ssig_fp_sugar = ssig_fp_sugar, Lam = Lam,
  1.2266 +      proto_sctr = proto_sctr, flat = flat, eval_core = eval_core, eval = eval, algLam = algLam,
  1.2267 +      corecUU = corecUU, dtor_transfer = dtor_transfer, Lam_transfer = Lam_transfer,
  1.2268 +      Lam_pointful_natural = Lam_pointful_natural, proto_sctr_transfer = proto_sctr_transfer,
  1.2269 +      flat_simps = flat_simps, eval_core_simps = eval_core_simps, eval_thm = eval_thm,
  1.2270 +      eval_simps = eval_simps, all_algLam_algs = [algLam_thm], algLam_thm = algLam_thm,
  1.2271 +      dtor_algLam = dtor_algLam, corecUU_thm = corecUU_thm, corecUU_unique = corecUU_unique,
  1.2272 +      corecUU_transfer = corecUU_transfer, buffer = buffer, all_dead_k_bnfs = [dead_pre_bnf],
  1.2273 +      Retr = Retr, equivp_Retr = equivp_Retr, Retr_coinduct = Retr_coinduct,
  1.2274 +      dtor_coinduct_info = dtor_coinduct_info}
  1.2275 +     |> morph_corec_info (Local_Theory.target_morphism lthy),
  1.2276 +     lthy |> Local_Theory.notes notes |> snd)
  1.2277 +  end;
  1.2278 +
  1.2279 +fun derive_corecUU_step (fpT as Type (fpT_name, res_Ds))
  1.2280 +    ({friend_names = old_friend_names, sig_fp_sugars = old_sig_fp_sugars as old_sig_fp_sugar :: _,
  1.2281 +      ssig_fp_sugar = old_ssig_fp_sugar, Lam = old_Lam0, proto_sctr = old_proto_sctr0,
  1.2282 +      flat = old_flat0, eval_core = old_eval_core0, eval = old_eval0, algLam = old_algLam0,
  1.2283 +      dtor_transfer, Lam_transfer = old_Lam_transfer,
  1.2284 +      Lam_pointful_natural = old_Lam_pointful_natural,
  1.2285 +      proto_sctr_transfer = old_proto_sctr_transfer, flat_simps = old_flat_simps,
  1.2286 +      eval_core_simps = old_eval_core_simps, eval_thm = old_eval_thm,
  1.2287 +      all_algLam_algs = old_all_algLam_algs, algLam_thm = old_algLam_thm,
  1.2288 +      dtor_algLam = old_dtor_algLam, buffer = old_buffer, all_dead_k_bnfs = old_all_dead_k_bnfs,
  1.2289 +      Retr = old_Retr0, equivp_Retr, Retr_coinduct, dtor_coinduct_info = old_dtor_coinduct_info,
  1.2290 +      ...} : corec_info)
  1.2291 +    friend_name friend_T fp_b version Y Z k_T dead_k_bnf sig_fp_sugar ssig_fp_sugar rho rho_transfer
  1.2292 +    lthy =
  1.2293 +  let
  1.2294 +    val {pre_bnf = live_pre_bnf, fp_bnf = live_fp_bnf, fp_res, ...} =
  1.2295 +      checked_fp_sugar_of lthy fpT_name;
  1.2296 +
  1.2297 +    val names_lthy = lthy
  1.2298 +      |> fold Variable.declare_typ [Y, Z];
  1.2299 +
  1.2300 +    (* FIXME *)
  1.2301 +    val live_EsFs = [];
  1.2302 +    val live_AsBs = live_EsFs @ [(Y, Z)];
  1.2303 +    val live = length live_EsFs;
  1.2304 +
  1.2305 +    val ((((x, f), g), R), _) = names_lthy
  1.2306 +      |> yield_singleton (mk_Frees "x") Y
  1.2307 +      ||>> yield_singleton (mk_Frees "f") (Y --> Z)
  1.2308 +      ||>> yield_singleton (mk_Frees "g") (Y --> Z)
  1.2309 +      ||>> yield_singleton (mk_Frees "R") (mk_pred2T Y Z);
  1.2310 +
  1.2311 +    (* FIXME *)
  1.2312 +    val fs = [];
  1.2313 +    val Rs = [];
  1.2314 +
  1.2315 +    val ctor = mk_ctor res_Ds (the_single (#ctors fp_res));
  1.2316 +    val dtor = mk_dtor res_Ds (the_single (#dtors fp_res));
  1.2317 +
  1.2318 +    val friend_names = friend_name :: old_friend_names;
  1.2319 +
  1.2320 +    val old_sig_bnf = #fp_bnf old_sig_fp_sugar;
  1.2321 +    val old_ssig_bnf = #fp_bnf old_ssig_fp_sugar;
  1.2322 +    val sig_bnf = #fp_bnf sig_fp_sugar;
  1.2323 +    val ssig_bnf = #fp_bnf ssig_fp_sugar;
  1.2324 +
  1.2325 +    val ((((((dead_pre_bnf, dead_fp_bnf), dead_old_sig_bnf), dead_old_ssig_bnf), dead_sig_bnf),
  1.2326 +          dead_ssig_bnf), lthy) = lthy
  1.2327 +      |> bnf_kill_all_but 1 live_pre_bnf
  1.2328 +      ||>> bnf_kill_all_but 0 live_fp_bnf
  1.2329 +      ||>> bnf_kill_all_but 1 old_sig_bnf
  1.2330 +      ||>> bnf_kill_all_but 1 old_ssig_bnf
  1.2331 +      ||>> bnf_kill_all_but 1 sig_bnf
  1.2332 +      ||>> bnf_kill_all_but 1 ssig_bnf;
  1.2333 +
  1.2334 +    (* FIXME *)
  1.2335 +    val pre_bnf = dead_pre_bnf;
  1.2336 +    val fp_bnf = dead_fp_bnf;
  1.2337 +
  1.2338 +    val old_ssig_fp_ctr_sugar = #fp_ctr_sugar old_ssig_fp_sugar;
  1.2339 +    val sig_fp_ctr_sugar = #fp_ctr_sugar sig_fp_sugar;
  1.2340 +    val ssig_fp_ctr_sugar = #fp_ctr_sugar ssig_fp_sugar;
  1.2341 +
  1.2342 +    val sig_fp_bnf_sugar = #fp_bnf_sugar sig_fp_sugar;
  1.2343 +    val old_ssig_fp_bnf_sugar = #fp_bnf_sugar old_ssig_fp_sugar;
  1.2344 +    val ssig_fp_bnf_sugar = #fp_bnf_sugar ssig_fp_sugar;
  1.2345 +    val old_ssig_fp_induct_sugar = #fp_co_induct_sugar old_ssig_fp_sugar;
  1.2346 +    val ssig_fp_induct_sugar = #fp_co_induct_sugar ssig_fp_sugar;
  1.2347 +
  1.2348 +    val old_ssig_ctr_sugar = #ctr_sugar old_ssig_fp_ctr_sugar;
  1.2349 +    val sig_ctr_sugar = #ctr_sugar sig_fp_ctr_sugar;
  1.2350 +    val ssig_ctr_sugar = #ctr_sugar ssig_fp_ctr_sugar;
  1.2351 +
  1.2352 +    val old_sig_T_name = fst (dest_Type (#T old_sig_fp_sugar));
  1.2353 +    val old_ssig_T_name = fst (dest_Type (#T old_ssig_fp_sugar));
  1.2354 +    val sig_T_name = fst (dest_Type (#T sig_fp_sugar));
  1.2355 +    val ssig_T_name = fst (dest_Type (#T ssig_fp_sugar));
  1.2356 +
  1.2357 +    val res_As = res_Ds @ [Y];
  1.2358 +    val res_Bs = res_Ds @ [Z];
  1.2359 +    val preT = pre_type_of_ctor Y ctor;
  1.2360 +    val YpreT = HOLogic.mk_prodT (Y, preT);
  1.2361 +    val old_sig_T = Type (old_sig_T_name, res_As);
  1.2362 +    val old_ssig_T = Type (old_ssig_T_name, res_As);
  1.2363 +    val sig_T = Type (sig_T_name, res_As);
  1.2364 +    val ssig_T = Type (ssig_T_name, res_As);
  1.2365 +    val old_Lam_domT = Tsubst Y YpreT old_sig_T;
  1.2366 +    val old_eval_core_domT = Tsubst Y YpreT old_ssig_T;
  1.2367 +
  1.2368 +    val pre_map = mk_mapN lthy live_AsBs preT pre_bnf;
  1.2369 +    val pre_rel = mk_relN lthy live_AsBs preT pre_bnf;
  1.2370 +    val dead_pre_map = mk_map1 lthy Y Z preT dead_pre_bnf;
  1.2371 +    val dead_pre_rel = mk_rel1 lthy Y Z preT dead_pre_bnf;
  1.2372 +    val fp_rel = mk_relN lthy live_EsFs fpT fp_bnf;
  1.2373 +    val dtor_unfold = mk_co_rec (Proof_Context.theory_of lthy) Greatest_FP [Z] fpT
  1.2374 +      (the_single (#xtor_un_folds fp_res));
  1.2375 +    val dead_k_map = mk_map1 lthy Y Z k_T dead_k_bnf;
  1.2376 +    val Sig = mk_ctr res_As (the_single (#ctrs sig_ctr_sugar));
  1.2377 +    val unsig = mk_disc_or_sel res_As (the_single (the_single (#selss sig_ctr_sugar)));
  1.2378 +    val sig_rel = mk_relN lthy live_AsBs sig_T sig_bnf;
  1.2379 +    val dead_old_sig_map = mk_map 1 res_As res_Bs (map_of_bnf dead_old_sig_bnf);
  1.2380 +    val dead_sig_map = mk_map 1 res_As res_Bs (map_of_bnf dead_sig_bnf);
  1.2381 +    val dead_sig_rel = mk_rel 1 res_As res_Bs (rel_of_bnf dead_sig_bnf);
  1.2382 +    val [old_Oper, old_VLeaf, old_CLeaf] = map (mk_ctr res_As) (#ctrs old_ssig_ctr_sugar);
  1.2383 +    val [Oper, VLeaf, CLeaf] = map (mk_ctr res_As) (#ctrs ssig_ctr_sugar);
  1.2384 +    val dead_old_ssig_map = mk_map 1 res_As res_Bs (map_of_bnf dead_old_ssig_bnf);
  1.2385 +    val ssig_map = mk_mapN lthy live_AsBs ssig_T ssig_bnf;
  1.2386 +    val ssig_rel = mk_relN lthy live_AsBs ssig_T ssig_bnf;
  1.2387 +    val dead_ssig_map = mk_map 1 res_As res_Bs (map_of_bnf dead_ssig_bnf);
  1.2388 +    val dead_ssig_rel = mk_rel 1 res_As res_Bs (rel_of_bnf dead_ssig_bnf);
  1.2389 +    val old_Lam = enforce_type lthy domain_type old_Lam_domT old_Lam0;
  1.2390 +    val old_proto_sctr = enforce_type lthy domain_type preT old_proto_sctr0;
  1.2391 +    val old_flat = enforce_type lthy range_type old_ssig_T old_flat0;
  1.2392 +    val old_eval_core = enforce_type lthy domain_type old_eval_core_domT old_eval_core0;
  1.2393 +    val old_eval = enforce_type lthy range_type fpT old_eval0;
  1.2394 +    val old_algLam = enforce_type lthy range_type fpT old_algLam0;
  1.2395 +
  1.2396 +    val ((embL, embL_def, embL_simps), lthy) = lthy
  1.2397 +      |> define_embL embLN fp_b version Y Z fpT old_sig_T old_ssig_T k_T ssig_T Inl_const
  1.2398 +        dead_old_sig_map Sig old_Oper old_VLeaf old_CLeaf Oper VLeaf CLeaf;
  1.2399 +
  1.2400 +    val ((Lam, Lam_def), lthy) = lthy
  1.2401 +      |> define_Lam_step fp_b version Y Z preT old_ssig_T ssig_T dead_pre_map unsig rho embL
  1.2402 +        old_Lam;
  1.2403 +
  1.2404 +    val ((proto_sctr, proto_sctr_def), lthy) = lthy
  1.2405 +      |> define_proto_sctr_step_or_merge fp_b version old_sig_T k_T Sig old_proto_sctr;
  1.2406 +
  1.2407 +    val pre_map_comp = map_comp_of_bnf pre_bnf;
  1.2408 +    val pre_map_transfer = map_transfer_of_bnf pre_bnf;
  1.2409 +    val dead_pre_map_id = map_id_of_bnf dead_pre_bnf;
  1.2410 +    val dead_pre_map_comp0 = map_comp0_of_bnf dead_pre_bnf;
  1.2411 +    val dead_pre_map_comp = map_comp_of_bnf dead_pre_bnf;
  1.2412 +    val fp_map_id = map_id_of_bnf fp_bnf;
  1.2413 +    val fp_rel_eq = rel_eq_of_bnf fp_bnf;
  1.2414 +    val [ctor_dtor] = #ctor_dtors fp_res;
  1.2415 +    val [dtor_inject] = #dtor_injects fp_res;
  1.2416 +    val [dtor_unfold_thm] = #xtor_un_fold_thms fp_res;
  1.2417 +    val [dtor_unfold_unique] = #xtor_un_fold_uniques fp_res;
  1.2418 +    val [dtor_unfold_transfer] = #xtor_un_fold_transfers fp_res;
  1.2419 +    val fp_k_T_rel_eqs =
  1.2420 +      map rel_eq_of_bnf (map_filter (bnf_of lthy) (fold add_type_namesT [fpT, k_T] []));
  1.2421 +    val unsig_thm = the_single (the_single (#sel_thmss sig_ctr_sugar));
  1.2422 +    val [sig_map_thm] = #map_thms sig_fp_bnf_sugar;
  1.2423 +    val old_sig_map_comp = map_comp_of_bnf old_sig_bnf;
  1.2424 +    val old_sig_map_cong = map_cong_of_bnf old_sig_bnf;
  1.2425 +    val old_ssig_map_thms = #map_thms old_ssig_fp_bnf_sugar;
  1.2426 +    val [Oper_map_thm, VLeaf_map_thm, CLeaf_map_thm] = #map_thms ssig_fp_bnf_sugar;
  1.2427 +    val old_sig_map_transfer = map_transfer_of_bnf old_sig_bnf;
  1.2428 +    val sig_map_comp = map_comp_of_bnf sig_bnf;
  1.2429 +    val sig_map_transfer = map_transfer_of_bnf sig_bnf;
  1.2430 +    val ssig_map_thms = #map_thms ssig_fp_bnf_sugar;
  1.2431 +    val ssig_map_transfer = map_transfer_of_bnf ssig_bnf;
  1.2432 +    val old_ssig_induct = the_single (#co_inducts old_ssig_fp_induct_sugar);
  1.2433 +    val ssig_induct = the_single (#co_inducts ssig_fp_induct_sugar);
  1.2434 +
  1.2435 +    val proto_sctr_transfer = derive_proto_sctr_transfer_step_or_merge lthy Y Z R dead_pre_rel
  1.2436 +      dead_sig_rel proto_sctr proto_sctr_def fp_k_T_rel_eqs [old_proto_sctr_transfer];
  1.2437 +    val embL_transfer = derive_transfer_by_transfer_prover lthy live_AsBs Rs R embL [embL_def]
  1.2438 +      fp_k_T_rel_eqs [old_sig_map_transfer];
  1.2439 +    val Lam_transfer = derive_Lam_or_eval_core_transfer lthy live_AsBs Y Z preT ssig_T Rs R pre_rel
  1.2440 +      sig_rel ssig_rel Lam Lam_def fp_k_T_rel_eqs
  1.2441 +      [pre_map_transfer, old_Lam_transfer, embL_transfer, rho_transfer];
  1.2442 +
  1.2443 +    val ((((((((flat, _, flat_simps), flat_transfer),
  1.2444 +            ((eval_core, _, eval_core_simps), eval_core_transfer)), (eval, eval_def)),
  1.2445 +          (cutSsig, cutSsig_def)), (algLam, algLam_def)), (corecU, corecU_def)), lthy) = lthy
  1.2446 +      |> define_flat_etc fp_b version live_AsBs Y Z preT fpT sig_T ssig_T Oper VLeaf CLeaf pre_rel
  1.2447 +        dead_pre_map dtor dtor_unfold dead_sig_map ssig_rel dead_ssig_map Lam Rs R pre_map_transfer
  1.2448 +        fp_k_T_rel_eqs sig_map_transfer ssig_map_transfer Lam_transfer dtor_transfer;
  1.2449 +
  1.2450 +    val (Sig_pointful_natural, flat_pointful_natural, Lam_natural_pointful, Lam_pointful_natural,
  1.2451 +         flat_VLeaf, eval_core_pointful_natural, eval_thm, eval_flat,
  1.2452 +         eval_simps as [eval_Oper, _, _], corecU_ctor, corecU_unique, dtor_algLam) =
  1.2453 +      derive_Sig_natural_etc lthy live live_AsBs Y Z preT fpT k_T sig_T ssig_T pre_map dead_pre_map
  1.2454 +        ctor dtor Sig dead_sig_map Oper VLeaf CLeaf ssig_map dead_ssig_map Lam flat eval_core eval
  1.2455 +        cutSsig algLam corecU x fs f g ctor_dtor dtor_inject dtor_unfold_thm dtor_unfold_unique
  1.2456 +        sig_map_thm ssig_induct ssig_map_thms Oper_map_thm VLeaf_map_thm CLeaf_map_thm Lam_transfer
  1.2457 +        flat_simps flat_transfer eval_core_simps eval_core_transfer eval_def cutSsig_def algLam_def
  1.2458 +        corecU_def live_pre_bnf pre_bnf dead_pre_bnf fp_bnf sig_bnf ssig_bnf dead_ssig_bnf;
  1.2459 +
  1.2460 +    val proto_sctr_natural = derive_natural_from_transfer_with_pre_type lthy live_AsBs Y Z preT
  1.2461 +      ssig_T pre_map ssig_map fs f proto_sctr proto_sctr_transfer [pre_bnf, sig_bnf] [];
  1.2462 +    val proto_sctr_pointful_natural = mk_pointful lthy proto_sctr_natural RS sym;
  1.2463 +
  1.2464 +    val (embL_pointful_natural, old_algLam_pointful, eval_embL, algLam_algLam) =
  1.2465 +      derive_embL_natural_etc lthy Inl_const old_ssig_bnf ssig_bnf Y Z preT fpT old_ssig_T ssig_T
  1.2466 +        dead_pre_map Sig dead_old_ssig_map embL old_algLam algLam old_flat flat old_eval_core
  1.2467 +        eval_core old_eval eval x f old_ssig_induct dead_pre_map_comp0 dead_pre_map_comp fp_map_id
  1.2468 +        dtor_inject dtor_unfold_unique Sig_pointful_natural unsig_thm sig_map_thm old_sig_map_comp
  1.2469 +        old_sig_map_cong old_ssig_map_thms old_Lam_pointful_natural Lam_def old_flat_simps
  1.2470 +        flat_simps embL_simps embL_transfer old_eval_core_simps eval_core_simps old_eval_thm
  1.2471 +        eval_thm old_dtor_algLam dtor_algLam old_algLam_thm;
  1.2472 +
  1.2473 +    val algLam_thm = derive_algLam_step_or_merge lthy Y fpT ctor proto_sctr algLam proto_sctr_def
  1.2474 +      old_algLam_pointful algLam_algLam;
  1.2475 +
  1.2476 +    val k_as_ssig = mk_k_as_ssig Z old_sig_T k_T ssig_T Sig dead_sig_map Oper VLeaf;
  1.2477 +    val k_as_ssig' = substT Y fpT k_as_ssig;
  1.2478 +
  1.2479 +    val algrho_rhs = HOLogic.mk_comp (eval, k_as_ssig');
  1.2480 +    val ((algrho, algrho_def), lthy) = lthy
  1.2481 +      |> define_const true fp_b version algrhoN algrho_rhs;
  1.2482 +
  1.2483 +    val k_as_ssig_transfer = derive_transfer_by_transfer_prover lthy live_AsBs Rs R k_as_ssig []
  1.2484 +      fp_k_T_rel_eqs [sig_map_transfer];
  1.2485 +
  1.2486 +    val k_as_ssig_natural = derive_natural_from_transfer lthy [(Y, Z)] [] [] f k_as_ssig
  1.2487 +      k_as_ssig_transfer [ssig_bnf] [dead_k_bnf];
  1.2488 +
  1.2489 +    val k_as_ssig_natural_pointful = mk_pointful lthy k_as_ssig_natural;
  1.2490 +
  1.2491 +    val [_, Lam_Inr] = derive_Lam_Inl_Inr lthy Y Z preT old_sig_T old_ssig_T k_T ssig_T
  1.2492 +      dead_pre_map Sig embL old_Lam Lam rho unsig_thm Lam_def;
  1.2493 +
  1.2494 +    val eval_core_k_as_ssig = derive_eval_core_k_as_ssig lthy Y preT k_T rho eval_core k_as_ssig x
  1.2495 +      pre_map_comp dead_pre_map_id sig_map_comp ssig_map_thms Lam_natural_pointful Lam_Inr
  1.2496 +      flat_VLeaf eval_core_simps;
  1.2497 +
  1.2498 +    val algLam_algrho = derive_algLam_algrho lthy Y fpT Sig algLam algrho algLam_def algrho_def;
  1.2499 +    val dtor_algrho = derive_dtor_algrho lthy Y Z preT fpT k_T ssig_T dead_pre_map dead_k_map dtor
  1.2500 +      rho eval algrho x eval_thm k_as_ssig_natural_pointful eval_core_k_as_ssig algrho_def;
  1.2501 +    val all_algLam_algs = algLam_algLam :: algLam_algrho :: old_all_algLam_algs;
  1.2502 +
  1.2503 +    val (((corecUU, _), corecUU_thm, corecUU_unique, corecUU_transfer, _, sctr_transfer,
  1.2504 +          sctr_pointful_natural), lthy) = lthy
  1.2505 +      |> define_corecUU_etc fp_b version live_AsBs Y Z preT fpT ssig_T pre_map dead_pre_map pre_rel
  1.2506 +        fp_rel ctor Oper ssig_map dead_ssig_map ssig_rel proto_sctr flat eval_core eval corecU fs f
  1.2507 +        g Rs R pre_map_transfer fp_k_T_rel_eqs dtor_unfold_transfer dtor_transfer ssig_map_transfer
  1.2508 +        proto_sctr_transfer proto_sctr_pointful_natural flat_transfer flat_pointful_natural
  1.2509 +        eval_core_transfer eval_core_pointful_natural eval_thm eval_flat eval_Oper algLam_thm
  1.2510 +        cutSsig_def corecU_def corecU_ctor corecU_unique pre_bnf dead_pre_bnf fp_res ssig_fp_sugar;
  1.2511 +
  1.2512 +    val (ctr_wrapper, friends) =
  1.2513 +      mk_ctr_wrapper_friends lthy friend_name friend_T old_sig_T k_T Sig old_buffer;
  1.2514 +
  1.2515 +    val Retr = enforce_type lthy (domain_type o domain_type) fpT old_Retr0;
  1.2516 +
  1.2517 +    val (dtor_coinduct_info, lthy) = lthy
  1.2518 +      |> derive_cong_step fp_b version fpT dead_ssig_bnf dead_pre_bnf eval eval_thm
  1.2519 +        eval_core_transfer old_dtor_coinduct_info algrho_def k_as_ssig_transfer Retr equivp_Retr
  1.2520 +        Retr_coinduct eval_embL embL_transfer old_all_dead_k_bnfs;
  1.2521 +
  1.2522 +    val buffer =
  1.2523 +      {Oper = Oper, VLeaf = VLeaf, CLeaf = CLeaf, ctr_wrapper = ctr_wrapper, friends = friends};
  1.2524 +
  1.2525 +    val notes =
  1.2526 +      [(corecUU_transferN, [corecUU_transfer])] @
  1.2527 +      (if Config.get lthy bnf_internals then
  1.2528 +         [(algLamN, [algLam_thm]),
  1.2529 +          (algLam_algLamN, [algLam_algLam]),
  1.2530 +          (algLam_algrhoN, [algLam_algrho]),
  1.2531 +          (cong_alg_introsN, #cong_alg_intros dtor_coinduct_info),
  1.2532 +          (cong_localeN, [#cong_locale dtor_coinduct_info]),
  1.2533 +          (corecU_ctorN, [corecU_ctor]),
  1.2534 +          (corecU_uniqueN, [corecU_unique]),
  1.2535 +          (corecUUN, [corecUU_thm]),
  1.2536 +          (corecUU_uniqueN, [corecUU_unique]),
  1.2537 +          (dtor_algLamN, [dtor_algLam]),
  1.2538 +          (dtor_algrhoN, [dtor_algrho]),
  1.2539 +          (dtor_coinductN, [#dtor_coinduct dtor_coinduct_info]),
  1.2540 +          (embL_pointful_naturalN, [embL_pointful_natural]),
  1.2541 +          (embL_transferN, [embL_transfer]),
  1.2542 +          (evalN, [eval_thm]),
  1.2543 +          (eval_core_pointful_naturalN, [eval_core_pointful_natural]),
  1.2544 +          (eval_core_transferN, [eval_core_transfer]),
  1.2545 +          (eval_flatN, [eval_flat]),
  1.2546 +          (eval_simpsN, eval_simps),
  1.2547 +          (flat_pointful_naturalN, [flat_pointful_natural]),
  1.2548 +          (flat_transferN, [flat_transfer]),
  1.2549 +          (k_as_ssig_naturalN, [k_as_ssig_natural]),
  1.2550 +          (k_as_ssig_transferN, [k_as_ssig_transfer]),
  1.2551 +          (Lam_pointful_naturalN, [Lam_pointful_natural]),
  1.2552 +          (Lam_transferN, [Lam_transfer]),
  1.2553 +          (proto_sctr_pointful_naturalN, [proto_sctr_pointful_natural]),
  1.2554 +          (proto_sctr_transferN, [proto_sctr_transfer]),
  1.2555 +          (rho_transferN, [rho_transfer]),
  1.2556 +          (sctr_pointful_naturalN, [sctr_pointful_natural]),
  1.2557 +          (sctr_transferN, [sctr_transfer]),
  1.2558 +          (Sig_pointful_naturalN, [Sig_pointful_natural])]
  1.2559 +       else
  1.2560 +         [])
  1.2561 +      |> map (fn (thmN, thms) =>
  1.2562 +        ((mk_version_fp_binding true lthy version fp_b thmN, []), [(thms, [])]));
  1.2563 +
  1.2564 +    val phi = Local_Theory.target_morphism lthy;
  1.2565 +  in
  1.2566 +    (({fp_b = fp_b, version = version, fpT = fpT, Y = Y, Z = Z, friend_names = friend_names,
  1.2567 +       sig_fp_sugars = sig_fp_sugar :: old_sig_fp_sugars, ssig_fp_sugar = ssig_fp_sugar, Lam = Lam,
  1.2568 +       proto_sctr = proto_sctr, flat = flat, eval_core = eval_core, eval = eval, algLam = algLam,
  1.2569 +       corecUU = corecUU, dtor_transfer = dtor_transfer, Lam_transfer = Lam_transfer,
  1.2570 +       Lam_pointful_natural = Lam_pointful_natural, proto_sctr_transfer = proto_sctr_transfer,
  1.2571 +       flat_simps = flat_simps, eval_core_simps = eval_core_simps, eval_thm = eval_thm,
  1.2572 +       eval_simps = eval_simps, all_algLam_algs = all_algLam_algs, algLam_thm = algLam_thm,
  1.2573 +       dtor_algLam = dtor_algLam, corecUU_thm = corecUU_thm, corecUU_unique = corecUU_unique,
  1.2574 +       corecUU_transfer = corecUU_transfer, buffer = buffer,
  1.2575 +       all_dead_k_bnfs = dead_k_bnf :: old_all_dead_k_bnfs, Retr = Retr, equivp_Retr = equivp_Retr,
  1.2576 +       Retr_coinduct = Retr_coinduct, dtor_coinduct_info = dtor_coinduct_info}
  1.2577 +      |> morph_corec_info phi,
  1.2578 +      ({algrho = algrho, dtor_algrho = dtor_algrho, algLam_algrho = algLam_algrho}
  1.2579 +       |> morph_friend_info phi)),
  1.2580 +     lthy |> Local_Theory.notes notes |> snd)
  1.2581 +  end;
  1.2582 +
  1.2583 +fun derive_corecUU_merge (fpT as Type (fpT_name, res_Ds))
  1.2584 +    ({friend_names = old1_friend_names,
  1.2585 +      sig_fp_sugars = old1_sig_fp_sugars as old1_sig_fp_sugar :: _,
  1.2586 +      ssig_fp_sugar = old1_ssig_fp_sugar, Lam = old1_Lam0, proto_sctr = old1_proto_sctr0,
  1.2587 +      flat = old1_flat0, eval_core = old1_eval_core0, eval = old1_eval0, algLam = old1_algLam0,
  1.2588 +      dtor_transfer, Lam_transfer = old1_Lam_transfer,
  1.2589 +      Lam_pointful_natural = old1_Lam_pointful_natural,
  1.2590 +      proto_sctr_transfer = old1_proto_sctr_transfer, flat_simps = old1_flat_simps,
  1.2591 +      eval_core_simps = old1_eval_core_simps, eval_thm = old1_eval_thm,
  1.2592 +      all_algLam_algs = old1_all_algLam_algs, algLam_thm = old1_algLam_thm,
  1.2593 +      dtor_algLam = old1_dtor_algLam, buffer = old1_buffer, all_dead_k_bnfs = old1_all_dead_k_bnfs,
  1.2594 +      Retr = old1_Retr0, equivp_Retr, Retr_coinduct, dtor_coinduct_info = old1_dtor_coinduct_info,
  1.2595 +      ...} : corec_info)
  1.2596 +    ({friend_names = old2_friend_names,
  1.2597 +      sig_fp_sugars = old2_sig_fp_sugars as old2_sig_fp_sugar :: _,
  1.2598 +      ssig_fp_sugar = old2_ssig_fp_sugar, Lam = old2_Lam0, flat = old2_flat0,
  1.2599 +      eval_core = old2_eval_core0, eval = old2_eval0, algLam = old2_algLam0,
  1.2600 +      Lam_transfer = old2_Lam_transfer, Lam_pointful_natural = old2_Lam_pointful_natural,
  1.2601 +      flat_simps = old2_flat_simps, eval_core_simps = old2_eval_core_simps,
  1.2602 +      eval_thm = old2_eval_thm, all_algLam_algs = old2_all_algLam_algs,
  1.2603 +      algLam_thm = old2_algLam_thm, dtor_algLam = old2_dtor_algLam, buffer = old2_buffer,
  1.2604 +      all_dead_k_bnfs = old2_all_dead_k_bnfs, dtor_coinduct_info = old2_dtor_coinduct_info, ...}
  1.2605 +     : corec_info)
  1.2606 +    lthy =
  1.2607 +  let
  1.2608 +    val {pre_bnf = live_pre_bnf, fp_bnf = live_fp_bnf, fp_res, ...} =
  1.2609 +      checked_fp_sugar_of lthy fpT_name;
  1.2610 +    val num_fp_tyargs = length res_Ds;
  1.2611 +    val live_fp_alives = liveness_of_fp_bnf num_fp_tyargs live_fp_bnf;
  1.2612 +
  1.2613 +    val ((Ds, [Y, Z]), names_lthy) = lthy
  1.2614 +      |> mk_TFrees num_fp_tyargs
  1.2615 +      ||>> mk_TFrees 2;
  1.2616 +
  1.2617 +    (* FIXME *)
  1.2618 +    val live_EsFs = [];
  1.2619 +    val live_AsBs = live_EsFs @ [(Y, Z)];
  1.2620 +    val live = length live_EsFs;
  1.2621 +
  1.2622 +    val ((((x, f), g), R), _) = names_lthy
  1.2623 +      |> yield_singleton (mk_Frees "x") Y
  1.2624 +      ||>> yield_singleton (mk_Frees "f") (Y --> Z)
  1.2625 +      ||>> yield_singleton (mk_Frees "g") (Y --> Z)
  1.2626 +      ||>> yield_singleton (mk_Frees "R") (mk_pred2T Y Z);
  1.2627 +
  1.2628 +    (* FIXME *)
  1.2629 +    val fs = [];
  1.2630 +    val Rs = [];
  1.2631 +
  1.2632 +    val ctor = mk_ctor res_Ds (the_single (#ctors fp_res));
  1.2633 +    val dtor = mk_dtor res_Ds (the_single (#dtors fp_res));
  1.2634 +
  1.2635 +    val old1_sig_T_name = fst (dest_Type (#T old1_sig_fp_sugar));
  1.2636 +    val old2_sig_T_name = fst (dest_Type (#T old2_sig_fp_sugar));
  1.2637 +    val old1_ssig_T_name = fst (dest_Type (#T old1_ssig_fp_sugar));
  1.2638 +    val old2_ssig_T_name = fst (dest_Type (#T old2_ssig_fp_sugar));
  1.2639 +
  1.2640 +    val fp_alives = map (K false) live_fp_alives;
  1.2641 +
  1.2642 +    val As = Ds @ [Y];
  1.2643 +    val res_As = res_Ds @ [Y];
  1.2644 +    val res_Bs = res_Ds @ [Z];
  1.2645 +    val preT = pre_type_of_ctor Y ctor;
  1.2646 +    val YpreT = HOLogic.mk_prodT (Y, preT);
  1.2647 +    val fpT0 = Type (fpT_name, Ds);
  1.2648 +    val old1_sig_T0 = Type (old1_sig_T_name, As);
  1.2649 +    val old2_sig_T0 = Type (old2_sig_T_name, As);
  1.2650 +    val old1_sig_T = Type (old1_sig_T_name, res_As);
  1.2651 +    val old2_sig_T = Type (old2_sig_T_name, res_As);
  1.2652 +    val old1_ssig_T = Type (old1_ssig_T_name, res_As);
  1.2653 +    val old2_ssig_T = Type (old2_ssig_T_name, res_As);
  1.2654 +    val old1_Lam_domT = Tsubst Y YpreT old1_sig_T;
  1.2655 +    val old2_Lam_domT = Tsubst Y YpreT old2_sig_T;
  1.2656 +    val old1_eval_core_domT = Tsubst Y YpreT old1_ssig_T;
  1.2657 +    val old2_eval_core_domT = Tsubst Y YpreT old2_ssig_T;
  1.2658 +
  1.2659 +    val ((fp_b, version), lthy) = lthy |> get_name_next_version_of fpT_name;
  1.2660 +
  1.2661 +    val ((sig_fp_sugar, ssig_fp_sugar), lthy) = lthy
  1.2662 +      |> define_sig_type fp_b version fp_alives Ds Y (mk_sumT (old1_sig_T0, old2_sig_T0))
  1.2663 +      ||>> define_ssig_type fp_b version fp_alives Ds Y fpT0;
  1.2664 +
  1.2665 +    val sig_T_name = fst (dest_Type (#T sig_fp_sugar));
  1.2666 +    val ssig_T_name = fst (dest_Type (#T ssig_fp_sugar));
  1.2667 +
  1.2668 +    val old1_sig_bnf = #fp_bnf old1_sig_fp_sugar;
  1.2669 +    val old2_sig_bnf = #fp_bnf old2_sig_fp_sugar;
  1.2670 +    val old1_ssig_bnf = #fp_bnf old1_ssig_fp_sugar;
  1.2671 +    val old2_ssig_bnf = #fp_bnf old2_ssig_fp_sugar;
  1.2672 +    val sig_bnf = #fp_bnf sig_fp_sugar;
  1.2673 +    val ssig_bnf = #fp_bnf ssig_fp_sugar;
  1.2674 +
  1.2675 +    val ((((((((dead_pre_bnf, dead_fp_bnf), dead_old1_sig_bnf), dead_old2_sig_bnf),
  1.2676 +        dead_old1_ssig_bnf), dead_old2_ssig_bnf), dead_sig_bnf), dead_ssig_bnf), lthy) = lthy
  1.2677 +      |> bnf_kill_all_but 1 live_pre_bnf
  1.2678 +      ||>> bnf_kill_all_but 0 live_fp_bnf
  1.2679 +      ||>> bnf_kill_all_but 1 old1_sig_bnf
  1.2680 +      ||>> bnf_kill_all_but 1 old2_sig_bnf
  1.2681 +      ||>> bnf_kill_all_but 1 old1_ssig_bnf
  1.2682 +      ||>> bnf_kill_all_but 1 old2_ssig_bnf
  1.2683 +      ||>> bnf_kill_all_but 1 sig_bnf
  1.2684 +      ||>> bnf_kill_all_but 1 ssig_bnf;
  1.2685 +
  1.2686 +    (* FIXME *)
  1.2687 +    val pre_bnf = dead_pre_bnf;
  1.2688 +    val fp_bnf = dead_fp_bnf;
  1.2689 +
  1.2690 +    val old1_ssig_fp_ctr_sugar = #fp_ctr_sugar old1_ssig_fp_sugar;
  1.2691 +    val old2_ssig_fp_ctr_sugar = #fp_ctr_sugar old2_ssig_fp_sugar;
  1.2692 +    val sig_fp_ctr_sugar = #fp_ctr_sugar sig_fp_sugar;
  1.2693 +    val ssig_fp_ctr_sugar = #fp_ctr_sugar ssig_fp_sugar;
  1.2694 +
  1.2695 +    val sig_fp_bnf_sugar = #fp_bnf_sugar sig_fp_sugar;
  1.2696 +    val old1_ssig_fp_bnf_sugar = #fp_bnf_sugar old1_ssig_fp_sugar;
  1.2697 +    val old2_ssig_fp_bnf_sugar = #fp_bnf_sugar old2_ssig_fp_sugar;
  1.2698 +    val ssig_fp_bnf_sugar = #fp_bnf_sugar ssig_fp_sugar;
  1.2699 +    val old1_ssig_fp_induct_sugar = #fp_co_induct_sugar old1_ssig_fp_sugar;
  1.2700 +    val old2_ssig_fp_induct_sugar = #fp_co_induct_sugar old2_ssig_fp_sugar;
  1.2701 +    val ssig_fp_induct_sugar = #fp_co_induct_sugar ssig_fp_sugar;
  1.2702 +
  1.2703 +    val old1_ssig_ctr_sugar = #ctr_sugar old1_ssig_fp_ctr_sugar;
  1.2704 +    val old2_ssig_ctr_sugar = #ctr_sugar old2_ssig_fp_ctr_sugar;
  1.2705 +    val sig_ctr_sugar = #ctr_sugar sig_fp_ctr_sugar;
  1.2706 +    val ssig_ctr_sugar = #ctr_sugar ssig_fp_ctr_sugar;
  1.2707 +
  1.2708 +    val sig_T = Type (sig_T_name, res_As);
  1.2709 +    val ssig_T = Type (ssig_T_name, res_As);
  1.2710 +
  1.2711 +    val pre_map = mk_mapN lthy live_AsBs preT pre_bnf;
  1.2712 +    val pre_rel = mk_relN lthy live_AsBs preT pre_bnf;
  1.2713 +    val dead_pre_map = mk_map1 lthy Y Z preT dead_pre_bnf;
  1.2714 +    val dead_pre_rel = mk_rel1 lthy Y Z preT dead_pre_bnf;
  1.2715 +    val fp_rel = mk_relN lthy live_EsFs fpT fp_bnf;
  1.2716 +    val dtor_unfold = mk_co_rec (Proof_Context.theory_of lthy) Greatest_FP [Z] fpT
  1.2717 +      (the_single (#xtor_un_folds fp_res));
  1.2718 +    val Sig = mk_ctr res_As (the_single (#ctrs sig_ctr_sugar));
  1.2719 +    val unsig = mk_disc_or_sel res_As (the_single (the_single (#selss sig_ctr_sugar)));
  1.2720 +    val sig_rel = mk_relN lthy live_AsBs sig_T sig_bnf;
  1.2721 +    val dead_old1_sig_map = mk_map 1 res_As res_Bs (map_of_bnf dead_old1_sig_bnf);
  1.2722 +    val dead_old2_sig_map = mk_map 1 res_As res_Bs (map_of_bnf dead_old2_sig_bnf);
  1.2723 +    val dead_sig_map = mk_map 1 res_As res_Bs (map_of_bnf dead_sig_bnf);
  1.2724 +    val dead_sig_rel = mk_rel 1 res_As res_Bs (rel_of_bnf dead_sig_bnf);
  1.2725 +    val [old1_Oper, old1_VLeaf, old1_CLeaf] = map (mk_ctr res_As) (#ctrs old1_ssig_ctr_sugar);
  1.2726 +    val [old2_Oper, old2_VLeaf, old2_CLeaf] = map (mk_ctr res_As) (#ctrs old2_ssig_ctr_sugar);
  1.2727 +    val [Oper, VLeaf, CLeaf] = map (mk_ctr res_As) (#ctrs ssig_ctr_sugar);
  1.2728 +    val old1_ssig_map = mk_map 1 res_As res_Bs (map_of_bnf dead_old1_ssig_bnf);
  1.2729 +    val old2_ssig_map = mk_map 1 res_As res_Bs (map_of_bnf dead_old2_ssig_bnf);
  1.2730 +    val ssig_map = mk_mapN lthy live_AsBs ssig_T ssig_bnf;
  1.2731 +    val ssig_rel = mk_relN lthy live_AsBs ssig_T ssig_bnf;
  1.2732 +    val dead_ssig_map = mk_map 1 res_As res_Bs (map_of_bnf dead_ssig_bnf);
  1.2733 +    val old1_Lam = enforce_type lthy domain_type old1_Lam_domT old1_Lam0;
  1.2734 +    val old2_Lam = enforce_type lthy domain_type old2_Lam_domT old2_Lam0;
  1.2735 +    val old1_proto_sctr = enforce_type lthy domain_type preT old1_proto_sctr0;
  1.2736 +    val old1_flat = enforce_type lthy range_type old1_ssig_T old1_flat0;
  1.2737 +    val old2_flat = enforce_type lthy range_type old2_ssig_T old2_flat0;
  1.2738 +    val old1_eval_core = enforce_type lthy domain_type old1_eval_core_domT old1_eval_core0;
  1.2739 +    val old2_eval_core = enforce_type lthy domain_type old2_eval_core_domT old2_eval_core0;
  1.2740 +    val old1_eval = enforce_type lthy range_type fpT old1_eval0;
  1.2741 +    val old2_eval = enforce_type lthy range_type fpT old2_eval0;
  1.2742 +    val old1_algLam = enforce_type lthy range_type fpT old1_algLam0;
  1.2743 +    val old2_algLam = enforce_type lthy range_type fpT old2_algLam0;
  1.2744 +
  1.2745 +    val ((embLL, embLL_def, embLL_simps), lthy) = lthy
  1.2746 +      |> define_embL embLLN fp_b version Y Z fpT old1_sig_T old1_ssig_T old2_sig_T ssig_T Inl_const
  1.2747 +        dead_old1_sig_map Sig old1_Oper old1_VLeaf old1_CLeaf Oper VLeaf CLeaf;
  1.2748 +
  1.2749 +    val ((embLR, embLR_def, embLR_simps), lthy) = lthy
  1.2750 +      |> define_embL embLRN fp_b version Y Z fpT old2_sig_T old2_ssig_T old1_sig_T ssig_T
  1.2751 +        (fn T => fn U => Inr_const U T) dead_old2_sig_map Sig old2_Oper old2_VLeaf old2_CLeaf Oper
  1.2752 +        VLeaf CLeaf;
  1.2753 +
  1.2754 +    val ((Lam, Lam_def), lthy) = lthy
  1.2755 +      |> define_Lam_merge fp_b version Y Z preT old1_ssig_T old2_ssig_T ssig_T dead_pre_map unsig
  1.2756 +        embLL embLR old1_Lam old2_Lam;
  1.2757 +
  1.2758 +    val ((proto_sctr, proto_sctr_def), lthy) = lthy
  1.2759 +      |> define_proto_sctr_step_or_merge fp_b version old1_sig_T old2_sig_T Sig old1_proto_sctr;
  1.2760 +
  1.2761 +    val pre_map_transfer = map_transfer_of_bnf pre_bnf;
  1.2762 +    val dead_pre_map_comp0 = map_comp0_of_bnf dead_pre_bnf;
  1.2763 +    val dead_pre_map_comp = map_comp_of_bnf dead_pre_bnf;
  1.2764 +    val fp_map_id = map_id_of_bnf fp_bnf;
  1.2765 +    val fp_rel_eq = rel_eq_of_bnf fp_bnf;
  1.2766 +    val [ctor_dtor] = #ctor_dtors fp_res;
  1.2767 +    val [dtor_inject] = #dtor_injects fp_res;
  1.2768 +    val [dtor_unfold_thm] = #xtor_un_fold_thms fp_res;
  1.2769 +    val [dtor_unfold_unique] = #xtor_un_fold_uniques fp_res;
  1.2770 +    val [dtor_unfold_transfer] = #xtor_un_fold_transfers fp_res;
  1.2771 +    val unsig_thm = the_single (the_single (#sel_thmss sig_ctr_sugar));
  1.2772 +    val [sig_map_thm] = #map_thms sig_fp_bnf_sugar;
  1.2773 +    val old1_sig_map_comp = map_comp_of_bnf old1_sig_bnf;
  1.2774 +    val old2_sig_map_comp = map_comp_of_bnf old2_sig_bnf;
  1.2775 +    val old1_sig_map_cong = map_cong_of_bnf old1_sig_bnf;
  1.2776 +    val old2_sig_map_cong = map_cong_of_bnf old2_sig_bnf;
  1.2777 +    val old1_ssig_map_thms = #map_thms old1_ssig_fp_bnf_sugar;
  1.2778 +    val old2_ssig_map_thms = #map_thms old2_ssig_fp_bnf_sugar;
  1.2779 +    val [Oper_map_thm, VLeaf_map_thm, CLeaf_map_thm] = #map_thms ssig_fp_bnf_sugar;
  1.2780 +    val old1_sig_map_transfer = map_transfer_of_bnf old1_sig_bnf;
  1.2781 +    val old2_sig_map_transfer = map_transfer_of_bnf old2_sig_bnf;
  1.2782 +    val sig_map_transfer = map_transfer_of_bnf sig_bnf;
  1.2783 +    val ssig_map_thms = #map_thms ssig_fp_bnf_sugar;
  1.2784 +    val ssig_map_transfer = map_transfer_of_bnf ssig_bnf;
  1.2785 +    val old1_ssig_induct = the_single (#co_inducts old1_ssig_fp_induct_sugar);
  1.2786 +    val old2_ssig_induct = the_single (#co_inducts old2_ssig_fp_induct_sugar);
  1.2787 +    val ssig_induct = the_single (#co_inducts ssig_fp_induct_sugar);
  1.2788 +
  1.2789 +    val proto_sctr_transfer = derive_proto_sctr_transfer_step_or_merge lthy Y Z R dead_pre_rel
  1.2790 +      dead_sig_rel proto_sctr proto_sctr_def [] [old1_proto_sctr_transfer];
  1.2791 +    val embLL_transfer = derive_transfer_by_transfer_prover lthy live_AsBs Rs R embLL [embLL_def] []
  1.2792 +      [old1_sig_map_transfer];
  1.2793 +    val embLR_transfer = derive_transfer_by_transfer_prover lthy live_AsBs Rs R embLR [embLR_def] []
  1.2794 +      [old2_sig_map_transfer];
  1.2795 +    val Lam_transfer = derive_Lam_or_eval_core_transfer lthy live_AsBs Y Z preT ssig_T Rs R
  1.2796 +      pre_rel sig_rel ssig_rel Lam Lam_def []
  1.2797 +      [pre_map_transfer, old1_Lam_transfer, old2_Lam_transfer, embLL_transfer, embLR_transfer];
  1.2798 +
  1.2799 +    val ((((((((flat, _, flat_simps), flat_transfer),
  1.2800 +            ((eval_core, _, eval_core_simps), eval_core_transfer)), (eval, eval_def)),
  1.2801 +          (cutSsig, cutSsig_def)), (algLam, algLam_def)), (corecU, corecU_def)), lthy) = lthy
  1.2802 +      |> define_flat_etc fp_b version live_AsBs Y Z preT fpT sig_T ssig_T Oper VLeaf CLeaf pre_rel
  1.2803 +        dead_pre_map dtor dtor_unfold dead_sig_map ssig_rel dead_ssig_map Lam Rs R pre_map_transfer
  1.2804 +        [fp_rel_eq] sig_map_transfer ssig_map_transfer Lam_transfer dtor_transfer;
  1.2805 +
  1.2806 +    val (Sig_pointful_natural, flat_pointful_natural, _, Lam_pointful_natural, _,
  1.2807 +         eval_core_pointful_natural, eval_thm, eval_flat, eval_simps as [eval_Oper, _, _],
  1.2808 +         corecU_ctor, corecU_unique, dtor_algLam) =
  1.2809 +      derive_Sig_natural_etc lthy live live_AsBs Y Z preT fpT fpT sig_T ssig_T pre_map dead_pre_map
  1.2810 +        ctor dtor Sig dead_sig_map Oper VLeaf CLeaf ssig_map dead_ssig_map Lam flat eval_core eval
  1.2811 +        cutSsig algLam corecU x fs f g ctor_dtor dtor_inject dtor_unfold_thm dtor_unfold_unique
  1.2812 +        sig_map_thm ssig_induct ssig_map_thms Oper_map_thm VLeaf_map_thm CLeaf_map_thm Lam_transfer
  1.2813 +        flat_simps flat_transfer eval_core_simps eval_core_transfer eval_def cutSsig_def algLam_def
  1.2814 +        corecU_def live_pre_bnf pre_bnf dead_pre_bnf fp_bnf sig_bnf ssig_bnf dead_ssig_bnf;
  1.2815 +
  1.2816 +    val proto_sctr_natural = derive_natural_from_transfer_with_pre_type lthy live_AsBs Y Z preT
  1.2817 +      ssig_T pre_map ssig_map fs f proto_sctr proto_sctr_transfer [pre_bnf, sig_bnf] [];
  1.2818 +    val proto_sctr_pointful_natural = mk_pointful lthy proto_sctr_natural RS sym;
  1.2819 +
  1.2820 +    val (embLL_pointful_natural, old1_algLam_pointful, eval_embLL, algLam_algLamL) =
  1.2821 +      derive_embL_natural_etc lthy Inl_const old1_ssig_bnf ssig_bnf Y Z preT fpT old1_ssig_T ssig_T
  1.2822 +        dead_pre_map Sig old1_ssig_map embLL old1_algLam algLam old1_flat flat old1_eval_core
  1.2823 +        eval_core old1_eval eval x f old1_ssig_induct dead_pre_map_comp0 dead_pre_map_comp fp_map_id
  1.2824 +        dtor_inject dtor_unfold_unique Sig_pointful_natural unsig_thm sig_map_thm old1_sig_map_comp
  1.2825 +        old1_sig_map_cong old1_ssig_map_thms old1_Lam_pointful_natural Lam_def old1_flat_simps
  1.2826 +        flat_simps embLL_simps embLL_transfer old1_eval_core_simps eval_core_simps old1_eval_thm
  1.2827 +        eval_thm old1_dtor_algLam dtor_algLam old1_algLam_thm;
  1.2828 +
  1.2829 +    val (embLR_pointful_natural, _, eval_embLR, algLam_algLamR) =
  1.2830 +      derive_embL_natural_etc lthy Inr_const old2_ssig_bnf ssig_bnf Y Z preT fpT old2_ssig_T ssig_T
  1.2831 +        dead_pre_map Sig old2_ssig_map embLR old2_algLam algLam old2_flat flat old2_eval_core
  1.2832 +        eval_core old2_eval eval x f old2_ssig_induct dead_pre_map_comp0 dead_pre_map_comp fp_map_id
  1.2833 +        dtor_inject dtor_unfold_unique Sig_pointful_natural unsig_thm sig_map_thm old2_sig_map_comp
  1.2834 +        old2_sig_map_cong old2_ssig_map_thms old2_Lam_pointful_natural Lam_def old2_flat_simps
  1.2835 +        flat_simps embLR_simps embLR_transfer old2_eval_core_simps eval_core_simps old2_eval_thm
  1.2836 +        eval_thm old2_dtor_algLam dtor_algLam old2_algLam_thm;
  1.2837 +
  1.2838 +    val algLam_thm = derive_algLam_step_or_merge lthy Y fpT ctor proto_sctr algLam proto_sctr_def
  1.2839 +      old1_algLam_pointful algLam_algLamL;
  1.2840 +
  1.2841 +    val all_algLam_algs = algLam_algLamL :: algLam_algLamR ::
  1.2842 +      merge_lists (Thm.eq_thm_prop o apply2 zero_var_indexes) old1_all_algLam_algs
  1.2843 +        old2_all_algLam_algs;
  1.2844 +
  1.2845 +    val (((corecUU, _), corecUU_thm, corecUU_unique, corecUU_transfer, _, sctr_transfer,
  1.2846 +          sctr_pointful_natural), lthy) = lthy
  1.2847 +      |> define_corecUU_etc fp_b version live_AsBs Y Z preT fpT ssig_T pre_map dead_pre_map pre_rel
  1.2848 +        fp_rel ctor Oper ssig_map dead_ssig_map ssig_rel proto_sctr flat eval_core eval corecU fs f
  1.2849 +        g Rs R pre_map_transfer [] dtor_unfold_transfer dtor_transfer ssig_map_transfer
  1.2850 +        proto_sctr_transfer proto_sctr_pointful_natural flat_transfer flat_pointful_natural
  1.2851 +        eval_core_transfer eval_core_pointful_natural eval_thm eval_flat eval_Oper algLam_thm
  1.2852 +        cutSsig_def corecU_def corecU_ctor corecU_unique pre_bnf dead_pre_bnf fp_res ssig_fp_sugar;
  1.2853 +
  1.2854 +    val Retr = enforce_type lthy (domain_type o domain_type) fpT old1_Retr0;
  1.2855 +
  1.2856 +    val embed_Sig_inl = embed_Sig lthy Sig (Inl_const old1_sig_T old2_sig_T);
  1.2857 +    val embed_Sig_inr = embed_Sig lthy Sig (Inr_const old1_sig_T old2_sig_T);
  1.2858 +
  1.2859 +    val ctr_wrapper = embed_Sig_inl (#ctr_wrapper old1_buffer);
  1.2860 +    val friends = Symtab.merge (K true)
  1.2861 +      (Symtab.map (K (apsnd embed_Sig_inl)) (#friends old1_buffer),
  1.2862 +       Symtab.map (K (apsnd embed_Sig_inr)) (#friends old2_buffer));
  1.2863 +
  1.2864 +    val old_fp_sugars =
  1.2865 +      merge_lists (op = o apply2 (fst o dest_Type o #T)) old1_sig_fp_sugars old2_sig_fp_sugars;
  1.2866 +
  1.2867 +    val ((dtor_coinduct_info, all_dead_k_bnfs, friend_names), lthy) = lthy
  1.2868 +      |> derive_cong_merge fp_b version fpT old1_friend_names old2_friend_names dead_ssig_bnf
  1.2869 +        dead_pre_bnf eval eval_thm eval_core_transfer old1_dtor_coinduct_info
  1.2870 +        old2_dtor_coinduct_info Retr equivp_Retr Retr_coinduct eval_embLL embLL_transfer eval_embLR
  1.2871 +        embLR_transfer old1_all_dead_k_bnfs old2_all_dead_k_bnfs;
  1.2872 +
  1.2873 +    val buffer =
  1.2874 +      {Oper = Oper, VLeaf = VLeaf, CLeaf = CLeaf, ctr_wrapper = ctr_wrapper, friends = friends};
  1.2875 +
  1.2876 +    val notes =
  1.2877 +      [(corecUU_transferN, [corecUU_transfer])] @
  1.2878 +      (if Config.get lthy bnf_internals then
  1.2879 +         [(algLamN, [algLam_thm]),
  1.2880 +          (algLam_algLamN, [algLam_algLamL, algLam_algLamR]),
  1.2881 +          (cong_alg_introsN, #cong_alg_intros dtor_coinduct_info),
  1.2882 +          (cong_localeN, [#cong_locale dtor_coinduct_info]),
  1.2883 +          (corecU_ctorN, [corecU_ctor]),
  1.2884 +          (corecU_uniqueN, [corecU_unique]),
  1.2885 +          (corecUUN, [corecUU_thm]),
  1.2886 +          (corecUU_uniqueN, [corecUU_unique]),
  1.2887 +          (dtor_algLamN, [dtor_algLam]),
  1.2888 +          (dtor_coinductN, [#dtor_coinduct dtor_coinduct_info]),
  1.2889 +          (eval_core_pointful_naturalN, [eval_core_pointful_natural]),
  1.2890 +          (eval_core_transferN, [eval_core_transfer]),
  1.2891 +          (embL_pointful_naturalN, [embLL_pointful_natural, embLR_pointful_natural]),
  1.2892 +          (embL_transferN, [embLL_transfer, embLR_transfer]),
  1.2893 +          (evalN, [eval_thm]),
  1.2894 +          (eval_flatN, [eval_flat]),
  1.2895 +          (eval_simpsN, eval_simps),
  1.2896 +          (flat_pointful_naturalN, [flat_pointful_natural]),
  1.2897 +          (flat_transferN, [flat_transfer]),
  1.2898 +          (Lam_pointful_naturalN, [Lam_pointful_natural]),
  1.2899 +          (Lam_transferN, [Lam_transfer]),
  1.2900 +          (proto_sctr_pointful_naturalN, [proto_sctr_pointful_natural]),
  1.2901 +          (proto_sctr_transferN, [proto_sctr_transfer]),
  1.2902 +          (sctr_pointful_naturalN, [sctr_pointful_natural]),
  1.2903 +          (sctr_transferN, [sctr_transfer]),
  1.2904 +          (Sig_pointful_naturalN, [Sig_pointful_natural])]
  1.2905 +       else
  1.2906 +         [])
  1.2907 +      |> map (fn (thmN, thms) =>
  1.2908 +        ((mk_version_fp_binding true lthy version fp_b thmN, []), [(thms, [])]));
  1.2909 +  in
  1.2910 +    ({fp_b = fp_b, version = version, fpT = fpT, Y = Y, Z = Z, friend_names = friend_names,
  1.2911 +      sig_fp_sugars = sig_fp_sugar :: old_fp_sugars, ssig_fp_sugar = ssig_fp_sugar, Lam = Lam,
  1.2912 +      proto_sctr = proto_sctr, flat = flat, eval_core = eval_core, eval = eval, algLam = algLam,
  1.2913 +      corecUU = corecUU, dtor_transfer = dtor_transfer, Lam_transfer = Lam_transfer,
  1.2914 +      Lam_pointful_natural = Lam_pointful_natural, proto_sctr_transfer = proto_sctr_transfer,
  1.2915 +      flat_simps = flat_simps, eval_core_simps = eval_core_simps, eval_thm = eval_thm,
  1.2916 +      eval_simps = eval_simps, all_algLam_algs = all_algLam_algs, algLam_thm = algLam_thm,
  1.2917 +      dtor_algLam = dtor_algLam, corecUU_thm = corecUU_thm, corecUU_unique = corecUU_unique,
  1.2918 +      corecUU_transfer = corecUU_transfer, buffer = buffer, all_dead_k_bnfs = all_dead_k_bnfs,
  1.2919 +      Retr = Retr, equivp_Retr = equivp_Retr, Retr_coinduct = Retr_coinduct,
  1.2920 +      dtor_coinduct_info = dtor_coinduct_info}
  1.2921 +     |> morph_corec_info (Local_Theory.target_morphism lthy),
  1.2922 +     lthy |> Local_Theory.notes notes |> snd)
  1.2923 +  end;
  1.2924 +
  1.2925 +fun set_corec_info_exprs fpT_name f =
  1.2926 +  Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
  1.2927 +    let val exprs = f phi in
  1.2928 +      Data.map (apsnd (fn [info_tab] => [Symtab.map_default (fpT_name, exprs) (K exprs) info_tab]))
  1.2929 +    end);
  1.2930 +
  1.2931 +fun subsume_corec_info_ad ctxt {fpT = fpT1, friend_names = friend_names1}
  1.2932 +    {fpT = fpT2, friend_names = friend_names2} =
  1.2933 +  Sign.typ_instance (Proof_Context.theory_of ctxt) (fpT1, fpT2) andalso
  1.2934 +  subset (op =) (friend_names1, friend_names2);
  1.2935 +
  1.2936 +fun subsume_corec_info_expr ctxt expr1 expr2 =
  1.2937 +  subsume_corec_info_ad ctxt (corec_ad_of_expr expr1) (corec_ad_of_expr expr2);
  1.2938 +
  1.2939 +fun instantiate_corec_info thy res_T (info as {fpT, ...}) =
  1.2940 +  let
  1.2941 +    val As_rho = tvar_subst thy [fpT] [res_T];
  1.2942 +    val substAT = Term.typ_subst_TVars As_rho;
  1.2943 +    val substA = Term.subst_TVars As_rho;
  1.2944 +    val phi = Morphism.typ_morphism "BNF" substAT $> Morphism.term_morphism "BNF" substA;
  1.2945 +  in
  1.2946 +    morph_corec_info phi info
  1.2947 +  end;
  1.2948 +
  1.2949 +fun instantiate_corec_info_expr thy res_T (Ad ({friend_names, ...}, f)) =
  1.2950 +    Ad ({fpT = res_T, friend_names = friend_names}, f #>> instantiate_corec_info thy res_T)
  1.2951 +  | instantiate_corec_info_expr thy res_T (Info info) =
  1.2952 +    Info (instantiate_corec_info thy res_T info);
  1.2953 +
  1.2954 +fun ensure_Info expr = corec_info_of_expr expr #>> Info
  1.2955 +and ensure_Info_if_Info old_expr (expr, lthy) =
  1.2956 +  if is_Info old_expr then ensure_Info expr lthy else (expr, lthy)
  1.2957 +and merge_corec_info_exprs old_exprs expr1 expr2 lthy =
  1.2958 +  if subsume_corec_info_expr lthy expr2 expr1 then
  1.2959 +    if subsume_corec_info_expr lthy expr1 expr2 andalso is_Ad expr1 then
  1.2960 +      (expr2, lthy)
  1.2961 +    else
  1.2962 +      ensure_Info_if_Info expr2 (expr1, lthy)
  1.2963 +  else if subsume_corec_info_expr lthy expr1 expr2 then
  1.2964 +    ensure_Info_if_Info expr1 (expr2, lthy)
  1.2965 +  else
  1.2966 +    let
  1.2967 +      val thy = Proof_Context.theory_of lthy;
  1.2968 +
  1.2969 +      val {fpT = fpT1, friend_names = friend_names1} = corec_ad_of_expr expr1;
  1.2970 +      val {fpT = fpT2, friend_names = friend_names2} = corec_ad_of_expr expr2;
  1.2971 +      val fpT0 = typ_unify_disjointly thy (fpT1, fpT2);
  1.2972 +
  1.2973 +      val fpT = singleton (freeze_types lthy []) fpT0;
  1.2974 +      val friend_names = merge_lists (op =) friend_names1 friend_names2;
  1.2975 +
  1.2976 +      val expr =
  1.2977 +        Ad ({fpT = fpT, friend_names = friend_names},
  1.2978 +          corec_info_of_expr expr1
  1.2979 +          ##>> corec_info_of_expr expr2
  1.2980 +          #-> uncurry (derive_corecUU_merge fpT));
  1.2981 +
  1.2982 +      val old_same_type_exprs =
  1.2983 +        if old_exprs then
  1.2984 +          []
  1.2985 +          |> Sign.typ_instance thy (fpT1, fpT0) ? cons expr1
  1.2986 +          |> Sign.typ_instance thy (fpT2, fpT0) ? cons expr2
  1.2987 +        else
  1.2988 +          [];
  1.2989 +    in
  1.2990 +      (expr, lthy) |> fold ensure_Info_if_Info old_same_type_exprs
  1.2991 +    end
  1.2992 +and insert_corec_info_expr expr exprs lthy =
  1.2993 +  let
  1.2994 +    val thy = Proof_Context.theory_of lthy;
  1.2995 +
  1.2996 +    val {fpT = new_fpT, ...} = corec_ad_of_expr expr;
  1.2997 +
  1.2998 +    val is_Tinst = curry (Sign.typ_instance thy);
  1.2999 +    fun is_Tequiv T U = is_Tinst T U andalso is_Tinst U T;
  1.3000 +
  1.3001 +    val (((equiv_exprs, sub_exprs), sup_exprs), incomp_exprs) = exprs
  1.3002 +      |> List.partition ((fn {fpT, ...} => is_Tequiv fpT new_fpT) o corec_ad_of_expr)
  1.3003 +      ||>> List.partition ((fn {fpT, ...} => is_Tinst fpT new_fpT) o corec_ad_of_expr)
  1.3004 +      ||>> List.partition ((fn {fpT, ...} => is_Tinst new_fpT fpT) o corec_ad_of_expr);
  1.3005 +
  1.3006 +    fun add_instantiated_incomp_expr expr exprs =
  1.3007 +      let val {fpT, ...} = corec_ad_of_expr expr in
  1.3008 +        (case try (typ_unify_disjointly thy) (fpT, new_fpT) of
  1.3009 +          SOME new_T =>
  1.3010 +          let val subsumes = (fn {fpT, ...} => is_Tinst new_T fpT) o corec_ad_of_expr in
  1.3011 +            if exists (exists subsumes) [exprs, sub_exprs] then exprs
  1.3012 +            else instantiate_corec_info_expr thy new_T expr :: exprs
  1.3013 +          end
  1.3014 +        | NONE => exprs)
  1.3015 +      end;
  1.3016 +
  1.3017 +    val unincomp_exprs = fold add_instantiated_incomp_expr incomp_exprs [];
  1.3018 +    val ((merged_sub_exprs, merged_unincomp_exprs), lthy) = lthy
  1.3019 +      |> fold_map (merge_corec_info_exprs true expr) sub_exprs
  1.3020 +      ||>> fold_map (merge_corec_info_exprs false expr) unincomp_exprs;
  1.3021 +    val (merged_equiv_expr, lthy) = (expr, lthy)
  1.3022 +      |> fold (uncurry o merge_corec_info_exprs true) equiv_exprs;
  1.3023 +  in
  1.3024 +    (merged_unincomp_exprs @ merged_sub_exprs @ merged_equiv_expr :: sup_exprs @ incomp_exprs
  1.3025 +     |> sort (rev_order o int_ord o apply2 (length o #friend_names o corec_ad_of_expr)),
  1.3026 +     lthy)
  1.3027 +  end
  1.3028 +and register_corec_info (info as {fpT = Type (fpT_name, _), ...}) lthy =
  1.3029 +  let
  1.3030 +    val (exprs, lthy) = insert_corec_info_expr (Info info) (corec_info_exprs_of lthy fpT_name) lthy;
  1.3031 +  in
  1.3032 +    lthy |> set_corec_info_exprs fpT_name (fn phi => map (morph_corec_info_expr phi) exprs)
  1.3033 +  end
  1.3034 +and corec_info_of_expr (Ad (_, f)) lthy = f lthy
  1.3035 +  | corec_info_of_expr (Info info) lthy = (info, lthy);
  1.3036 +
  1.3037 +fun nonempty_corec_info_exprs_of fpT_name lthy =
  1.3038 +  (case corec_info_exprs_of lthy fpT_name of
  1.3039 +    [] =>
  1.3040 +    derive_corecUU_base fpT_name lthy
  1.3041 +    |> (fn (info, lthy) =>
  1.3042 +      ([Info info], lthy
  1.3043 +         |> set_corec_info_exprs fpT_name (fn phi => [Info (morph_corec_info phi info)])))
  1.3044 +  | exprs => (exprs, lthy));
  1.3045 +
  1.3046 +fun corec_info_of res_T lthy =
  1.3047 +  (case res_T of
  1.3048 +    Type (fpT_name, _) =>
  1.3049 +    let
  1.3050 +      val (exprs, lthy) = nonempty_corec_info_exprs_of fpT_name lthy;
  1.3051 +      val thy = Proof_Context.theory_of lthy;
  1.3052 +      val SOME expr =
  1.3053 +        find_first ((fn {fpT, ...} => Sign.typ_instance thy (res_T, fpT)) o corec_ad_of_expr) exprs;
  1.3054 +      val (info, lthy) = corec_info_of_expr expr lthy;
  1.3055 +    in
  1.3056 +      (instantiate_corec_info thy res_T info, lthy |> is_Ad expr ? register_corec_info info)
  1.3057 +    end
  1.3058 +  | _ => not_codatatype lthy res_T);
  1.3059 +
  1.3060 +fun maybe_corec_info_of ctxt res_T =
  1.3061 +  (case res_T of
  1.3062 +    Type (fpT_name, _) =>
  1.3063 +    let
  1.3064 +      val thy = Proof_Context.theory_of ctxt;
  1.3065 +      val infos = corec_infos_of ctxt fpT_name;
  1.3066 +    in
  1.3067 +      find_first (fn {fpT, ...} => Sign.typ_instance thy (res_T, fpT)) infos
  1.3068 +      |> Option.map (instantiate_corec_info thy res_T)
  1.3069 +    end
  1.3070 +  | _ => not_codatatype ctxt res_T);
  1.3071 +
  1.3072 +fun prepare_friend_corec friend_name friend_T lthy =
  1.3073 +  let
  1.3074 +    val (arg_Ts, res_T) = strip_type friend_T;
  1.3075 +    val Type (fpT_name, res_Ds) =
  1.3076 +      (case res_T of
  1.3077 +        T as Type _ => T
  1.3078 +      | T => error (not_codatatype lthy T));
  1.3079 +
  1.3080 +    val _ = not (null arg_Ts) orelse
  1.3081 +      error "Function with no argument cannot be registered as friend";
  1.3082 +
  1.3083 +    val {pre_bnf, fp_bnf = live_fp_bnf, fp_res, ...} = checked_fp_sugar_of lthy fpT_name;
  1.3084 +    val num_fp_tyargs = length res_Ds;
  1.3085 +    val live_fp_alives = liveness_of_fp_bnf num_fp_tyargs live_fp_bnf;
  1.3086 +
  1.3087 +    val fpT_name = fst (dest_Type res_T);
  1.3088 +
  1.3089 +    val (old_info as {friend_names = old_friend_names, sig_fp_sugars = old_sig_fp_sugar :: _,
  1.3090 +           buffer = old_buffer, ...}, lthy) =
  1.3091 +      corec_info_of res_T lthy;
  1.3092 +    val old_sig_T_name = fst (dest_Type (#T old_sig_fp_sugar));
  1.3093 +    val old_sig_alives = liveness_of_fp_bnf (num_fp_tyargs + 1) (#fp_bnf old_sig_fp_sugar);
  1.3094 +
  1.3095 +    (* FIXME: later *)
  1.3096 +    val fp_alives = fst (split_last old_sig_alives);
  1.3097 +    val fp_alives = map (K false) live_fp_alives;
  1.3098 +
  1.3099 +    val _ = not (member (op =) old_friend_names friend_name) orelse
  1.3100 +      error ("Function " ^ quote (Syntax.string_of_term lthy (Const (friend_name, friend_T))) ^
  1.3101 +        " already registered as friend");
  1.3102 +
  1.3103 +    val lthy = lthy |> Variable.declare_typ friend_T;
  1.3104 +    val ((Ds, [Y, Z]), _) = lthy
  1.3105 +      |> mk_TFrees num_fp_tyargs
  1.3106 +      ||>> mk_TFrees 2;
  1.3107 +
  1.3108 +    (* FIXME *)
  1.3109 +    val dead_Ds = Ds;
  1.3110 +    val live_As = [Y];
  1.3111 +
  1.3112 +    val ctor = mk_ctor res_Ds (the_single (#ctors fp_res));
  1.3113 +
  1.3114 +    val fpT0 = Type (fpT_name, Ds);
  1.3115 +    val k_Ts0 = map (typ_subst_nonatomic (res_Ds ~~ Ds) o typ_subst_nonatomic [(res_T, Y)]) arg_Ts;
  1.3116 +    val k_T0 = mk_tupleT_balanced k_Ts0;
  1.3117 +
  1.3118 +    val As = Ds @ [Y];
  1.3119 +    val res_As = res_Ds @ [Y];
  1.3120 +
  1.3121 +    val k_As = fold Term.add_tfreesT k_Ts0 [];
  1.3122 +    val _ = (case filter_out (member (op =) As o TFree) k_As of [] => ()
  1.3123 +      | k_A :: _ => error ("Cannot have type variable " ^
  1.3124 +          quote (Syntax.string_of_typ lthy (TFree k_A)) ^ " used like that in friend"));
  1.3125 +
  1.3126 +    val substDT = Term.typ_subst_atomic (Ds ~~ res_Ds);
  1.3127 +
  1.3128 +    val old_sig_T0 = Type (old_sig_T_name, As);
  1.3129 +
  1.3130 +    val ((fp_b, version), lthy) = lthy |> get_name_next_version_of fpT_name;
  1.3131 +
  1.3132 +    val (((dead_k_bnf, sig_fp_sugar), ssig_fp_sugar), lthy) = lthy
  1.3133 +      |> bnf_with_deads_and_lives dead_Ds live_As Y fpT0 k_T0
  1.3134 +      ||>> define_sig_type fp_b version fp_alives Ds Y (mk_sumT (old_sig_T0, k_T0))
  1.3135 +      ||>> define_ssig_type fp_b version fp_alives Ds Y fpT0;
  1.3136 +
  1.3137 +    val _ = live_of_bnf dead_k_bnf = 1 orelse
  1.3138 +      error "Impossible type for friend (the result codatatype must occur live in the arguments)";
  1.3139 +
  1.3140 +    val (dead_pre_bnf, lthy) = lthy
  1.3141 +      |> bnf_kill_all_but 1 pre_bnf;
  1.3142 +
  1.3143 +    val sig_fp_ctr_sugar = #fp_ctr_sugar sig_fp_sugar;
  1.3144 +    val ssig_fp_ctr_sugar = #fp_ctr_sugar ssig_fp_sugar;
  1.3145 +
  1.3146 +    val sig_ctr_sugar = #ctr_sugar sig_fp_ctr_sugar;
  1.3147 +    val ssig_ctr_sugar = #ctr_sugar ssig_fp_ctr_sugar;
  1.3148 +
  1.3149 +    val ssig_T_name = fst (dest_Type (#T ssig_fp_sugar));
  1.3150 +
  1.3151 +    val preT = pre_type_of_ctor Y ctor;
  1.3152 +    val old_sig_T = substDT old_sig_T0;
  1.3153 +    val k_T = substDT k_T0;
  1.3154 +    val ssig_T = Type (ssig_T_name, res_As);
  1.3155 +
  1.3156 +    val Sig = mk_ctr res_As (the_single (#ctrs sig_ctr_sugar));
  1.3157 +
  1.3158 +    val [Oper, VLeaf, CLeaf] = map (mk_ctr res_As) (#ctrs ssig_ctr_sugar);
  1.3159 +    val (ctr_wrapper, friends) =
  1.3160 +      mk_ctr_wrapper_friends lthy friend_name friend_T old_sig_T k_T Sig old_buffer;
  1.3161 +
  1.3162 +    val buffer =
  1.3163 +      {Oper = Oper, VLeaf = VLeaf, CLeaf = CLeaf, ctr_wrapper = ctr_wrapper, friends = friends};
  1.3164 +  in
  1.3165 +    ((old_info, fp_b, version, Y, Z, preT, k_T, ssig_T, dead_pre_bnf, dead_k_bnf, sig_fp_sugar,
  1.3166 +      ssig_fp_sugar, buffer), lthy)
  1.3167 +  end;
  1.3168 +
  1.3169 +fun register_friend_corec key fp_b version Y Z k_T dead_k_bnf sig_fp_sugar ssig_fp_sugar
  1.3170 +    friend_const rho rho_transfer old_info lthy =
  1.3171 +  let
  1.3172 +    val friend_T = fastype_of friend_const;
  1.3173 +    val res_T = body_type friend_T;
  1.3174 +  in
  1.3175 +    derive_corecUU_step res_T old_info key friend_T fp_b version Y Z k_T dead_k_bnf sig_fp_sugar
  1.3176 +      ssig_fp_sugar rho rho_transfer lthy
  1.3177 +    |> (fn ((info, friend_info), lthy) => (friend_info, register_corec_info info lthy))
  1.3178 +  end;
  1.3179 +
  1.3180 +fun merge_corec_info_exprss exprs1 exprs2 lthy =
  1.3181 +  let
  1.3182 +    fun all_friend_names_of exprs =
  1.3183 +      fold (union (op =)) (map (#friend_names o corec_ad_of_expr) exprs) [];
  1.3184 +
  1.3185 +    val friend_names1 = all_friend_names_of exprs1;
  1.3186 +    val friend_names2 = all_friend_names_of exprs2;
  1.3187 +  in
  1.3188 +    if subset (op =) (friend_names2, friend_names1) then
  1.3189 +      if subset (op =) (friend_names1, friend_names2) andalso
  1.3190 +         length (filter is_Info exprs2) > length (filter is_Info exprs1) then
  1.3191 +        (exprs2, lthy)
  1.3192 +      else
  1.3193 +        (exprs1, lthy)
  1.3194 +    else if subset (op =) (friend_names1, friend_names2) then
  1.3195 +      (exprs2, lthy)
  1.3196 +    else
  1.3197 +      fold_rev (uncurry o insert_corec_info_expr) exprs2 (exprs1, lthy)
  1.3198 +  end;
  1.3199 +
  1.3200 +fun merge_corec_info_tabs info_tab1 info_tab2 lthy =
  1.3201 +  let
  1.3202 +    val fpT_names = union (op =) (Symtab.keys info_tab1) (Symtab.keys info_tab2);
  1.3203 +
  1.3204 +    fun add_infos_of fpT_name (info_tab, lthy) =
  1.3205 +      (case Symtab.lookup info_tab1 fpT_name of
  1.3206 +        NONE =>
  1.3207 +        (Symtab.update_new (fpT_name, the (Symtab.lookup info_tab2 fpT_name)) info_tab, lthy)
  1.3208 +      | SOME exprs1 =>
  1.3209 +        (case Symtab.lookup info_tab2 fpT_name of
  1.3210 +          NONE => (Symtab.update_new (fpT_name, exprs1) info_tab, lthy)
  1.3211 +        | SOME exprs2 =>
  1.3212 +          let val (exprs, lthy) = merge_corec_info_exprss exprs1 exprs2 lthy in
  1.3213 +            (Symtab.update_new (fpT_name, exprs) info_tab, lthy)
  1.3214 +          end));
  1.3215 +  in
  1.3216 +    fold add_infos_of fpT_names (Symtab.empty, lthy)
  1.3217 +  end;
  1.3218 +
  1.3219 +fun consolidate lthy =
  1.3220 +  (case snd (Data.get (Context.Proof lthy)) of
  1.3221 +    [_] => raise Same.SAME
  1.3222 +  | info_tab :: info_tabs =>
  1.3223 +    let
  1.3224 +      val (info_tab', lthy) = fold_rev (uncurry o merge_corec_info_tabs) info_tabs (info_tab, lthy);
  1.3225 +    in
  1.3226 +      Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
  1.3227 +          Data.map (apsnd (fn _ => [Symtab.map (K (map (morph_corec_info_expr phi))) info_tab'])))
  1.3228 +        lthy
  1.3229 +    end);
  1.3230 +
  1.3231 +fun consolidate_global thy =
  1.3232 +  SOME (Named_Target.theory_map consolidate thy)
  1.3233 +  handle Same.SAME => NONE;
  1.3234 +
  1.3235 +val _ = Theory.setup (Theory.at_begin consolidate_global);
  1.3236 +
  1.3237 +end;