src/HOL/Tools/BNF/bnf_gfp_grec.ML
author blanchet
Wed Mar 23 16:37:13 2016 +0100 (2016-03-23)
changeset 62699 add334b71e16
parent 62692 0701f25fac39
child 62721 f3248e77c960
permissions -rw-r--r--
sorted out type issue with sort constraints
     1 (*  Title:      HOL/Tools/BNF/bnf_gfp_grec.ML
     2     Author:     Jasmin Blanchette, Inria, LORIA, MPII
     3     Author:     Aymeric Bouzy, Ecole polytechnique
     4     Author:     Dmitriy Traytel, ETH Z├╝rich
     5     Copyright   2015, 2016
     6 
     7 Generalized corecursor construction.
     8 *)
     9 
    10 signature BNF_GFP_GREC =
    11 sig
    12   val Tsubst: typ -> typ -> typ -> typ
    13   val substT: typ -> typ -> term -> term
    14   val freeze_types: Proof.context -> (indexname * sort) list -> typ list -> typ list
    15   val dummify_atomic_types: term -> term
    16   val enforce_type: Proof.context -> (typ -> typ) -> typ -> term -> term
    17   val define_const: bool -> binding -> int -> string -> term -> local_theory ->
    18     (term * thm) * local_theory
    19 
    20   type buffer =
    21     {Oper: term,
    22      VLeaf: term,
    23      CLeaf: term,
    24      ctr_wrapper: term,
    25      friends: (typ * term) Symtab.table}
    26 
    27   val map_buffer: (term -> term) -> buffer -> buffer
    28   val specialize_buffer_types: buffer -> buffer
    29 
    30   type dtor_coinduct_info =
    31     {dtor_coinduct: thm,
    32      cong_def: thm,
    33      cong_locale: thm,
    34      cong_base: thm,
    35      cong_refl: thm,
    36      cong_sym: thm,
    37      cong_trans: thm,
    38      cong_alg_intros: thm list}
    39 
    40   type corec_info =
    41     {fp_b: binding,
    42      version: int,
    43      fpT: typ,
    44      Y: typ,
    45      Z: typ,
    46      friend_names: string list,
    47      sig_fp_sugars: BNF_FP_Def_Sugar.fp_sugar list,
    48      ssig_fp_sugar: BNF_FP_Def_Sugar.fp_sugar,
    49      Lam: term,
    50      proto_sctr: term,
    51      flat: term,
    52      eval_core: term,
    53      eval: term,
    54      algLam: term,
    55      corecUU: term,
    56      dtor_transfer: thm,
    57      Lam_transfer: thm,
    58      Lam_pointful_natural: thm,
    59      proto_sctr_transfer: thm,
    60      flat_simps: thm list,
    61      eval_core_simps: thm list,
    62      eval_thm: thm,
    63      eval_simps: thm list,
    64      all_algLam_algs: thm list,
    65      algLam_thm: thm,
    66      dtor_algLam: thm,
    67      corecUU_thm: thm,
    68      corecUU_unique: thm,
    69      corecUU_transfer: thm,
    70      buffer: buffer,
    71      all_dead_k_bnfs: BNF_Def.bnf list,
    72      Retr: term,
    73      equivp_Retr: thm,
    74      Retr_coinduct: thm,
    75      dtor_coinduct_info: dtor_coinduct_info}
    76 
    77   type friend_info =
    78     {algrho: term,
    79      dtor_algrho: thm,
    80      algLam_algrho: thm}
    81 
    82   val not_codatatype: Proof.context -> typ -> 'a
    83   val mk_fp_binding: binding -> string -> binding
    84   val bnf_kill_all_but: int -> BNF_Def.bnf -> local_theory -> BNF_Def.bnf * local_theory
    85 
    86   val print_corec_infos: Proof.context -> unit
    87   val has_no_corec_info: Proof.context -> string -> bool
    88   val corec_info_of: typ -> local_theory -> corec_info * local_theory
    89   val maybe_corec_info_of: Proof.context -> typ -> corec_info option
    90   val corec_infos_of: Proof.context -> string -> corec_info list
    91   val corec_infos_of_generic: Context.generic -> Symtab.key -> corec_info list
    92   val prepare_friend_corec: string -> typ -> local_theory ->
    93     (corec_info * binding * int * typ * typ * typ * typ * typ * BNF_Def.bnf * BNF_Def.bnf
    94      * BNF_FP_Def_Sugar.fp_sugar * BNF_FP_Def_Sugar.fp_sugar * buffer) * local_theory
    95   val register_friend_corec: string -> binding -> int -> typ -> typ -> typ -> BNF_Def.bnf ->
    96     BNF_FP_Def_Sugar.fp_sugar -> BNF_FP_Def_Sugar.fp_sugar -> term -> term -> thm -> corec_info ->
    97     local_theory -> friend_info * local_theory
    98 end;
    99 
   100 structure BNF_GFP_Grec : BNF_GFP_GREC =
   101 struct
   102 
   103 open Ctr_Sugar
   104 open BNF_Util
   105 open BNF_Def
   106 open BNF_Comp
   107 open BNF_FP_Util
   108 open BNF_LFP
   109 open BNF_FP_Def_Sugar
   110 open BNF_LFP_Rec_Sugar
   111 open BNF_GFP_Grec_Tactics
   112 
   113 val algLamN = "algLam";
   114 val algLam_algLamN = "algLam_algLam";
   115 val algLam_algrhoN = "algLam_algrho";
   116 val algrhoN = "algrho";
   117 val CLeafN = "CLeaf";
   118 val congN = "congclp";
   119 val cong_alg_introsN = "cong_alg_intros";
   120 val cong_localeN = "cong_locale";
   121 val corecUUN = "corecUU";
   122 val corecUU_transferN = "corecUU_transfer";
   123 val corecUU_uniqueN = "corecUU_unique";
   124 val cutSsigN = "cutSsig";
   125 val dtor_algLamN = "dtor_algLam";
   126 val dtor_algrhoN = "dtor_algrho";
   127 val dtor_coinductN = "dtor_coinduct";
   128 val dtor_transferN = "dtor_transfer";
   129 val embLN = "embL";
   130 val embLLN = "embLL";
   131 val embLRN = "embLR";
   132 val embL_pointful_naturalN = "embL_pointful_natural";
   133 val embL_transferN = "embL_transfer";
   134 val equivp_RetrN = "equivp_Retr";
   135 val evalN = "eval";
   136 val eval_coreN = "eval_core";
   137 val eval_core_pointful_naturalN = "eval_core_pointful_natural";
   138 val eval_core_transferN = "eval_core_transfer";
   139 val eval_flatN = "eval_flat";
   140 val eval_simpsN = "eval_simps";
   141 val flatN = "flat";
   142 val flat_pointful_naturalN = "flat_pointful_natural";
   143 val flat_transferN = "flat_transfer";
   144 val k_as_ssig_naturalN = "k_as_ssig_natural";
   145 val k_as_ssig_transferN = "k_as_ssig_transfer";
   146 val LamN = "Lam";
   147 val Lam_transferN = "Lam_transfer";
   148 val Lam_pointful_naturalN = "Lam_pointful_natural";
   149 val OperN = "Oper";
   150 val proto_sctrN = "proto_sctr";
   151 val proto_sctr_pointful_naturalN = "proto_sctr_pointful_natural";
   152 val proto_sctr_transferN = "proto_sctr_transfer";
   153 val rho_transferN = "rho_transfer";
   154 val Retr_coinductN = "Retr_coinduct";
   155 val sctrN = "sctr";
   156 val sctr_transferN = "sctr_transfer";
   157 val sctr_pointful_naturalN = "sctr_pointful_natural";
   158 val sigN = "sig";
   159 val SigN = "Sig";
   160 val Sig_pointful_naturalN = "Sig_pointful_natural";
   161 val corecUN = "corecU";
   162 val corecU_ctorN = "corecU_ctor";
   163 val corecU_uniqueN = "corecU_unique";
   164 val unsigN = "unsig";
   165 val VLeafN = "VLeaf";
   166 
   167 val s_prefix = "s"; (* transforms "sig" into "ssig" *)
   168 
   169 fun not_codatatype ctxt T =
   170   error ("Not a codatatype: " ^ Syntax.string_of_typ ctxt T);
   171 fun mutual_codatatype () =
   172   error ("Mutually corecursive codatatypes are not supported (try " ^
   173     quote (#1 @{command_keyword primcorec}) ^ " instead of " ^
   174     quote (#1 @{command_keyword corec}) ^ ")");
   175 fun noncorecursive_codatatype () =
   176   error ("Noncorecursive codatatypes are not supported (try " ^
   177     quote (#1 @{command_keyword definition}) ^ " instead of " ^
   178     quote (#1 @{command_keyword corec}) ^ ")");
   179 fun singleton_codatatype ctxt =
   180   error ("Singleton corecursive codatatypes are not supported (use " ^
   181     quote (Syntax.string_of_typ ctxt @{typ unit}) ^ " instead)");
   182 
   183 fun merge_lists eq old1 old2 = (old1 |> subtract eq old2) @ old2;
   184 
   185 fun add_type_namesT (Type (s, Ts)) = insert (op =) s #> fold add_type_namesT Ts
   186   | add_type_namesT _ = I;
   187 
   188 fun Tsubst Y T = Term.typ_subst_atomic [(Y, T)];
   189 fun substT Y T = Term.subst_atomic_types [(Y, T)];
   190 
   191 fun freeze_types ctxt except_tvars Ts =
   192   let
   193     val As = fold Term.add_tvarsT Ts [] |> subtract (op =) except_tvars;
   194     val (Bs, _) = ctxt |> mk_TFrees' (map snd As);
   195   in
   196     map (Term.typ_subst_TVars (map fst As ~~ Bs)) Ts
   197   end;
   198 
   199 fun typ_unify_disjointly thy (T, T') =
   200   if T = T' then
   201     T
   202   else
   203     let
   204       val tvars = Term.add_tvar_namesT T [];
   205       val tvars' = Term.add_tvar_namesT T' [];
   206       val maxidx' = maxidx_of_typ T';
   207       val T = T |> exists (member (op =) tvars') tvars ? Logic.incr_tvar (maxidx' + 1);
   208       val maxidx = Integer.max (maxidx_of_typ T) maxidx';
   209       val (tyenv, _) = Sign.typ_unify thy (T, T') (Vartab.empty, maxidx);
   210     in
   211       Envir.subst_type tyenv T
   212     end;
   213 
   214 val dummify_atomic_types = Term.map_types (Term.map_atyps (K Term.dummyT));
   215 
   216 fun enforce_type ctxt get_T T t =
   217   Term.subst_TVars (tvar_subst (Proof_Context.theory_of ctxt) [get_T (fastype_of t)] [T]) t;
   218 
   219 fun mk_internal internal ctxt f =
   220   if internal andalso not (Config.get ctxt bnf_internals) then f else I
   221 fun mk_fp_binding fp_b pre = Binding.map_name (K pre) fp_b
   222   |> Binding.qualify true (Binding.name_of fp_b);
   223 fun mk_version_binding version = Binding.qualify false ("v" ^ string_of_int version);
   224 fun mk_version_fp_binding internal ctxt =
   225   mk_internal internal ctxt Binding.concealed ooo (mk_fp_binding oo mk_version_binding);
   226 (*FIXME: get rid of ugly names when typedef and primrec respect qualification*)
   227 fun mk_version_binding_ugly version = Binding.suffix_name ("_v" ^ string_of_int version);
   228 fun mk_version_fp_binding_ugly internal ctxt version fp_b pre =
   229   Binding.prefix_name (pre ^ "_") fp_b
   230   |> mk_version_binding_ugly version
   231   |> mk_internal internal ctxt Binding.concealed;
   232 
   233 fun mk_mapN ctxt live_AsBs TA bnf =
   234   let val TB = Term.typ_subst_atomic live_AsBs TA in
   235     enforce_type ctxt (snd o strip_typeN (length live_AsBs)) (TA --> TB) (map_of_bnf bnf)
   236   end;
   237 
   238 fun mk_relN ctxt live_AsBs TA bnf =
   239   let val TB = Term.typ_subst_atomic live_AsBs TA in
   240     enforce_type ctxt (snd o strip_typeN (length live_AsBs)) (mk_pred2T TA TB) (rel_of_bnf bnf)
   241   end;
   242 
   243 fun mk_map1 ctxt Y Z = mk_mapN ctxt [(Y, Z)];
   244 fun mk_rel1 ctxt Y Z = mk_relN ctxt [(Y, Z)];
   245 
   246 fun define_const internal fp_b version name rhs lthy =
   247   let
   248     val b = mk_version_fp_binding internal lthy version fp_b name;
   249 
   250     val ((free, (_, def_free)), (lthy, lthy_old)) = lthy
   251       |> Local_Theory.open_target |> snd
   252       |> Local_Theory.define ((b, NoSyn), ((Thm.def_binding b |> Binding.concealed, []), rhs))
   253       ||> `Local_Theory.close_target;
   254 
   255     val phi = Proof_Context.export_morphism lthy_old lthy;
   256 
   257     val const = Morphism.term phi free;
   258     val const' = enforce_type lthy I (fastype_of free) const;
   259   in
   260     ((const', Morphism.thm phi def_free), lthy)
   261   end;
   262 
   263 fun define_single_primrec b eqs lthy =
   264   let
   265     val (([free], [def_free], [simps_free]), (lthy, lthy_old)) = lthy
   266       |> Local_Theory.open_target |> snd
   267       |> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed) (*TODO check*)
   268       |> primrec [(b, NONE, NoSyn)] (map (pair Attrib.empty_binding) eqs)
   269       ||> `Local_Theory.close_target;
   270 
   271     val phi = Proof_Context.export_morphism lthy_old lthy;
   272 
   273     val const = Morphism.term phi free;
   274     val const' = enforce_type lthy I (fastype_of free) const;
   275   in
   276     ((const', Morphism.thm phi def_free, map (Morphism.thm phi) simps_free), lthy)
   277   end;
   278 
   279 type buffer =
   280   {Oper: term,
   281    VLeaf: term,
   282    CLeaf: term,
   283    ctr_wrapper: term,
   284    friends: (typ * term) Symtab.table};
   285 
   286 fun map_buffer f {Oper, VLeaf, CLeaf, ctr_wrapper, friends} =
   287   {Oper = f Oper, VLeaf = f VLeaf, CLeaf = f CLeaf, ctr_wrapper = f ctr_wrapper,
   288    friends = Symtab.map (K (apsnd f)) friends};
   289 
   290 fun morph_buffer phi = map_buffer (Morphism.term phi);
   291 
   292 fun specialize_buffer_types {Oper, VLeaf, CLeaf, ctr_wrapper, friends} =
   293   let
   294     val ssig_T as Type (_, Ts) = body_type (fastype_of VLeaf);
   295     val Y = List.last Ts;
   296     val ssigifyT = substT Y ssig_T;
   297   in
   298     {Oper = Oper, VLeaf = VLeaf, CLeaf = CLeaf, ctr_wrapper = ssigifyT ctr_wrapper,
   299      friends = Symtab.map (K (apsnd ssigifyT)) friends}
   300   end;
   301 
   302 type dtor_coinduct_info =
   303   {dtor_coinduct: thm,
   304    cong_def: thm,
   305    cong_locale: thm,
   306    cong_base: thm,
   307    cong_refl: thm,
   308    cong_sym: thm,
   309    cong_trans: thm,
   310    cong_alg_intros: thm list};
   311 
   312 fun map_dtor_coinduct_info f {dtor_coinduct, cong_def, cong_locale, cong_base, cong_refl, cong_sym,
   313     cong_trans, cong_alg_intros} =
   314   {dtor_coinduct = f dtor_coinduct, cong_def = f cong_def, cong_locale = f cong_locale,
   315    cong_base = f cong_base, cong_refl = f cong_refl, cong_sym = f cong_sym,
   316    cong_trans = f cong_trans, cong_alg_intros = map f cong_alg_intros};
   317 
   318 fun morph_dtor_coinduct_info phi = map_dtor_coinduct_info (Morphism.thm phi);
   319 
   320 type corec_ad =
   321   {fpT: typ,
   322    friend_names: string list};
   323 
   324 fun morph_corec_ad phi {fpT, friend_names} =
   325   {fpT = Morphism.typ phi fpT, friend_names = friend_names};
   326 
   327 type corec_info =
   328   {fp_b: binding,
   329    version: int,
   330    fpT: typ,
   331    Y: typ,
   332    Z: typ,
   333    friend_names: string list,
   334    sig_fp_sugars: fp_sugar list,
   335    ssig_fp_sugar: fp_sugar,
   336    Lam: term,
   337    proto_sctr: term,
   338    flat: term,
   339    eval_core: term,
   340    eval: term,
   341    algLam: term,
   342    corecUU: term,
   343    dtor_transfer: thm,
   344    Lam_transfer: thm,
   345    Lam_pointful_natural: thm,
   346    proto_sctr_transfer: thm,
   347    flat_simps: thm list,
   348    eval_core_simps: thm list,
   349    eval_thm: thm,
   350    eval_simps: thm list,
   351    all_algLam_algs: thm list,
   352    algLam_thm: thm,
   353    dtor_algLam: thm,
   354    corecUU_thm: thm,
   355    corecUU_unique: thm,
   356    corecUU_transfer: thm,
   357    buffer: buffer,
   358    all_dead_k_bnfs: BNF_Def.bnf list,
   359    Retr: term,
   360    equivp_Retr: thm,
   361    Retr_coinduct: thm,
   362    dtor_coinduct_info: dtor_coinduct_info};
   363 
   364 fun morph_corec_info phi
   365     ({fp_b, version, fpT, Y, Z, friend_names, sig_fp_sugars, ssig_fp_sugar, Lam, proto_sctr, flat,
   366       eval_core, eval, algLam, corecUU, dtor_transfer, Lam_transfer, Lam_pointful_natural,
   367       proto_sctr_transfer, flat_simps, eval_core_simps, eval_thm, eval_simps, all_algLam_algs,
   368       algLam_thm, dtor_algLam, corecUU_thm, corecUU_unique, corecUU_transfer, buffer,
   369       all_dead_k_bnfs, Retr, equivp_Retr, Retr_coinduct, dtor_coinduct_info} : corec_info) =
   370   {fp_b = fp_b, version = version, fpT = Morphism.typ phi fpT, Y = Morphism.typ phi Y,
   371    Z = Morphism.typ phi Z, friend_names = friend_names, sig_fp_sugars = sig_fp_sugars (*no morph*),
   372    ssig_fp_sugar = ssig_fp_sugar (*no morph*), Lam = Morphism.term phi Lam,
   373    proto_sctr = Morphism.term phi proto_sctr, flat = Morphism.term phi flat,
   374    eval_core = Morphism.term phi eval_core, eval = Morphism.term phi eval,
   375    algLam = Morphism.term phi algLam, corecUU = Morphism.term phi corecUU,
   376    dtor_transfer = dtor_transfer, Lam_transfer = Morphism.thm phi Lam_transfer,
   377    Lam_pointful_natural = Morphism.thm phi Lam_pointful_natural,
   378    proto_sctr_transfer = Morphism.thm phi proto_sctr_transfer,
   379    flat_simps = map (Morphism.thm phi) flat_simps,
   380    eval_core_simps = map (Morphism.thm phi) eval_core_simps, eval_thm = Morphism.thm phi eval_thm,
   381    eval_simps = map (Morphism.thm phi) eval_simps,
   382    all_algLam_algs = map (Morphism.thm phi) all_algLam_algs,
   383    algLam_thm = Morphism.thm phi algLam_thm, dtor_algLam = Morphism.thm phi dtor_algLam,
   384    corecUU_thm = Morphism.thm phi corecUU_thm, corecUU_unique = Morphism.thm phi corecUU_unique,
   385    corecUU_transfer = Morphism.thm phi corecUU_transfer, buffer = morph_buffer phi buffer,
   386    all_dead_k_bnfs = map (morph_bnf phi) all_dead_k_bnfs, Retr = Morphism.term phi Retr,
   387    equivp_Retr = Morphism.thm phi equivp_Retr, Retr_coinduct = Morphism.thm phi Retr_coinduct,
   388    dtor_coinduct_info = morph_dtor_coinduct_info phi dtor_coinduct_info};
   389 
   390 datatype ('a, 'b) expr =
   391   Ad of 'a * (local_theory -> 'b * local_theory) |
   392   Info of 'b;
   393 
   394 fun is_Ad (Ad _) = true
   395   | is_Ad _ = false;
   396 
   397 fun is_Info (Info _) = true
   398   | is_Info _ = false;
   399 
   400 type corec_info_expr = (corec_ad, corec_info) expr;
   401 
   402 fun morph_corec_info_expr phi (Ad (ad, f)) = Ad (morph_corec_ad phi ad, f)
   403   | morph_corec_info_expr phi (Info info) = Info (morph_corec_info phi info);
   404 
   405 val transfer_corec_info_expr = morph_corec_info_expr o Morphism.transfer_morphism;
   406 
   407 type corec_data = int Symtab.table * corec_info_expr list Symtab.table list;
   408 
   409 structure Data = Generic_Data
   410 (
   411   type T = corec_data;
   412   val empty = (Symtab.empty, [Symtab.empty]);
   413   val extend = I;
   414   fun merge ((version_tab1, info_tabs1), (version_tab2, info_tabs2)) : T =
   415     (Symtab.join (K Int.max) (version_tab1, version_tab2), info_tabs1 @ info_tabs2);
   416 );
   417 
   418 fun corec_ad_of_expr (Ad (ad, _)) = ad
   419   | corec_ad_of_expr (Info {fpT, friend_names, ...}) = {fpT = fpT, friend_names = friend_names};
   420 
   421 fun corec_info_exprs_of_generic context fpT_name =
   422   let
   423     val thy = Context.theory_of context;
   424     val info_tabs = snd (Data.get context);
   425   in
   426     maps (fn info_tab => these (Symtab.lookup info_tab fpT_name)) info_tabs
   427     |> map (transfer_corec_info_expr thy)
   428   end;
   429 
   430 val corec_info_exprs_of = corec_info_exprs_of_generic o Context.Proof;
   431 
   432 val keep_corec_infos = map_filter (fn Ad _ => NONE | Info info => SOME info);
   433 
   434 val corec_infos_of_generic = keep_corec_infos oo corec_info_exprs_of_generic;
   435 val corec_infos_of = keep_corec_infos oo corec_info_exprs_of;
   436 
   437 fun str_of_corec_ad ctxt {fpT, friend_names} =
   438   "[" ^ Syntax.string_of_typ ctxt fpT ^ "; " ^ commas friend_names ^ "]";
   439 
   440 fun str_of_corec_info ctxt {fpT, version, friend_names, ...} =
   441   "{" ^ Syntax.string_of_typ ctxt fpT ^ "; " ^ commas friend_names ^ "; v" ^ string_of_int version ^
   442   "}";
   443 
   444 fun str_of_corec_info_expr ctxt (Ad (ad, _)) = str_of_corec_ad ctxt ad
   445   | str_of_corec_info_expr ctxt (Info info) = str_of_corec_info ctxt info;
   446 
   447 fun print_corec_infos ctxt =
   448   Symtab.fold (fn (fpT_name, exprs) => fn () =>
   449       writeln (fpT_name ^ ":\n" ^
   450         cat_lines (map (prefix "  " o str_of_corec_info_expr ctxt) exprs)))
   451     (the_single (snd (Data.get (Context.Proof ctxt)))) ();
   452 
   453 val has_no_corec_info = null oo corec_info_exprs_of;
   454 
   455 fun get_name_next_version_of fpT_name ctxt =
   456   let
   457     val (version_tab, info_tabs) = Data.get (Context.Theory (Proof_Context.theory_of ctxt));
   458     val fp_base = Long_Name.base_name fpT_name;
   459     val fp_b = Binding.name fp_base;
   460     val version_tab' = Symtab.map_default (fp_base, ~1) (Integer.add 1) version_tab;
   461     val SOME version = Symtab.lookup version_tab' fp_base;
   462     val ctxt' = ctxt
   463       |> Local_Theory.background_theory (Context.theory_map (Data.put (version_tab', info_tabs)));
   464   in
   465     ((fp_b, version), ctxt')
   466   end;
   467 
   468 type friend_info =
   469   {algrho: term,
   470    dtor_algrho: thm,
   471    algLam_algrho: thm};
   472 
   473 fun morph_friend_info phi ({algrho, dtor_algrho, algLam_algrho} : friend_info) =
   474   {algrho = Morphism.term phi algrho, dtor_algrho = Morphism.thm phi dtor_algrho,
   475    algLam_algrho = Morphism.thm phi algLam_algrho};
   476 
   477 fun checked_fp_sugar_of ctxt fpT_name =
   478   let
   479     val fp_sugar as {X, fp_res = {Ts = fpTs, ...}, fp_ctr_sugar = {ctrXs_Tss, ...}, ...} =
   480       (case fp_sugar_of ctxt fpT_name of
   481         SOME (fp_sugar as {fp = Greatest_FP, ...}) => fp_sugar
   482       | _ => not_codatatype ctxt (Type (fpT_name, [] (*yuck*))));
   483 
   484     val _ =
   485       if length fpTs > 1 then
   486         mutual_codatatype ()
   487       else if not (exists (exists (Term.exists_subtype (curry (op =) X))) ctrXs_Tss) then
   488         noncorecursive_codatatype ()
   489       else if ctrXs_Tss = [[X]] then
   490         singleton_codatatype ctxt
   491       else
   492         ();
   493   in
   494     fp_sugar
   495   end;
   496 
   497 fun inline_pre_bnfs f lthy =
   498   lthy
   499   |> Config.put typedef_threshold ~1
   500   |> f
   501   |> Config.put typedef_threshold (Config.get lthy typedef_threshold);
   502 
   503 fun bnf_kill_all_but nn bnf lthy =
   504   ((empty_comp_cache, empty_unfolds), lthy)
   505   |> kill_bnf I (live_of_bnf bnf - nn) bnf
   506   ||> snd;
   507 
   508 fun bnf_with_deads_and_lives dead_Es live_As Y fpT T lthy =
   509    let
   510      val qsoty = quote o Syntax.string_of_typ lthy;
   511 
   512      val unfreeze_fp = Tsubst Y fpT;
   513 
   514     fun flatten_tyargs Ass =
   515       map dest_TFree live_As
   516       |> filter (fn T => exists (fn Ts => member (op =) Ts T) Ass);
   517 
   518      val ((bnf, _), (_, lthy)) =
   519       bnf_of_typ false Do_Inline I flatten_tyargs [Term.dest_TFree Y]
   520         (map Term.dest_TFree dead_Es) T ((empty_comp_cache, empty_unfolds), lthy)
   521       handle BAD_DEAD (Y, Y_backdrop) =>
   522         (case Y_backdrop of
   523           Type (bad_tc, _) =>
   524           let
   525             val T = qsoty (unfreeze_fp Y);
   526             val T_backdrop = qsoty (unfreeze_fp Y_backdrop);
   527             fun register_hint () =
   528               "\nUse the " ^ quote (#1 @{command_keyword "bnf"}) ^ " command to register " ^
   529               quote bad_tc ^ " as a bounded natural functor to allow nested (co)recursion through \
   530               \it";
   531           in
   532             if is_some (bnf_of lthy bad_tc) orelse is_some (fp_sugar_of lthy bad_tc) then
   533               error ("Inadmissible occurrence of type " ^ T ^ " in type expression " ^
   534                 T_backdrop)
   535             else
   536               error ("Unsupported occurrence of type " ^ T ^ " via type constructor " ^
   537                 quote bad_tc ^ " in type expression " ^ T_backdrop ^ register_hint ())
   538           end);
   539 
   540     val phi =
   541       Morphism.term_morphism "BNF" (Raw_Simplifier.rewrite_term (Proof_Context.theory_of lthy)
   542         @{thms BNF_Composition.id_bnf_def} [])
   543       $> Morphism.thm_morphism "BNF" (unfold_thms lthy @{thms BNF_Composition.id_bnf_def});
   544   in
   545     (morph_bnf phi bnf, lthy)
   546   end;
   547 
   548 fun define_sig_type fp_b version fp_alives Es Y rhsT lthy =
   549   let
   550     val T_b = mk_version_fp_binding_ugly true lthy version fp_b sigN;
   551     val ctr_b = mk_version_fp_binding false lthy version fp_b SigN;
   552     val sel_b = mk_version_fp_binding true lthy version fp_b unsigN;
   553 
   554     val lthy = Local_Theory.open_target lthy |> snd;
   555 
   556     val T_name = Local_Theory.full_name lthy T_b;
   557 
   558     val tyargs = map2 (fn alive => fn T =>
   559         (if alive then SOME Binding.empty else NONE, (T, Type.sort_of_atyp T)))
   560       (fp_alives @ [true]) (Es @ [Y]);
   561     val ctr_specs = [(((Binding.empty, ctr_b), [(sel_b, rhsT)]), NoSyn)];
   562     val spec = (((((tyargs, T_b), NoSyn), ctr_specs),
   563       (Binding.empty, Binding.empty, Binding.empty)), []);
   564 
   565     val plugins = Plugin_Name.make_filter lthy (K (curry (op =) transfer_plugin));
   566     val discs_sels = true;
   567 
   568     val lthy = lthy
   569       |> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed) (*TODO check*)
   570       |> inline_pre_bnfs (co_datatypes Least_FP construct_lfp ((plugins, discs_sels), [spec]))
   571       |> Local_Theory.close_target;
   572 
   573     val SOME fp_sugar = fp_sugar_of lthy T_name;
   574   in
   575     (fp_sugar, lthy)
   576   end;
   577 
   578 fun define_ssig_type fp_b version fp_alives Es Y fpT lthy =
   579   let
   580     val sig_T_b = mk_version_fp_binding_ugly true lthy version fp_b sigN;
   581     val T_b = Binding.prefix_name s_prefix sig_T_b;
   582     val Oper_b = mk_version_fp_binding false lthy version fp_b OperN;
   583     val VLeaf_b = mk_version_fp_binding false lthy version fp_b VLeafN;
   584     val CLeaf_b = mk_version_fp_binding false lthy version fp_b CLeafN;
   585 
   586     val lthy = Local_Theory.open_target lthy |> snd;
   587 
   588     val sig_T_name = Local_Theory.full_name lthy sig_T_b;
   589     val T_name = Long_Name.map_base_name (prefix s_prefix) sig_T_name;
   590 
   591     val As = Es @ [Y];
   592     val ssig_sig_T = Type (sig_T_name, Es @ [Type (T_name, As)]);
   593 
   594     val tyargs = map2 (fn alive => fn T =>
   595         (if alive then SOME Binding.empty else NONE, (T, Type.sort_of_atyp T)))
   596       (fp_alives @ [true]) (Es @ [Y]);
   597     val ctr_specs =
   598       [(((Binding.empty, Oper_b), [(Binding.empty, ssig_sig_T)]), NoSyn),
   599        (((Binding.empty, VLeaf_b), [(Binding.empty, Y)]), NoSyn),
   600        (((Binding.empty, CLeaf_b), [(Binding.empty, fpT)]), NoSyn)];
   601     val spec = (((((tyargs, T_b), NoSyn), ctr_specs),
   602       (Binding.empty, Binding.empty, Binding.empty)), []);
   603 
   604     val plugins = Plugin_Name.make_filter lthy (K (curry (op =) transfer_plugin));
   605     val discs_sels = false;
   606 
   607     val lthy = lthy
   608       |> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed) (*TODO check*)
   609       |> inline_pre_bnfs (co_datatypes Least_FP construct_lfp ((plugins, discs_sels), [spec]))
   610       |> Local_Theory.close_target;
   611 
   612     val SOME fp_sugar = fp_sugar_of lthy T_name;
   613   in
   614     (fp_sugar, lthy)
   615   end;
   616 
   617 fun embed_Sig ctxt Sig inl_or_r t =
   618   Library.foldl1 HOLogic.mk_comp [Sig, inl_or_r, dummify_atomic_types t]
   619   |> Syntax.check_term ctxt;
   620 
   621 fun mk_ctr_wrapper_friends ctxt friend_name friend_T old_sig_T k_T Sig old_buffer =
   622   let
   623     val embed_Sig_inl = embed_Sig ctxt Sig (Inl_const old_sig_T k_T);
   624 
   625     val ctr_wrapper = embed_Sig_inl (#ctr_wrapper old_buffer);
   626     val friends = Symtab.map (K (apsnd embed_Sig_inl)) (#friends old_buffer)
   627       |> Symtab.update_new (friend_name, (friend_T,
   628         HOLogic.mk_comp (Sig, Inr_const old_sig_T k_T)));
   629   in
   630     (ctr_wrapper, friends)
   631   end;
   632 
   633 fun pre_type_of_ctor Y ctor =
   634   let
   635     val (fp_preT, fpT) = dest_funT (fastype_of ctor);
   636   in
   637     typ_subst_nonatomic [(fpT, Y)] fp_preT
   638   end;
   639 
   640 fun mk_k_as_ssig Z old_sig_T k_T ssig_T Sig dead_sig_map Oper VLeaf =
   641   let
   642     val inr' = Inr_const old_sig_T k_T;
   643     val dead_sig_map' = substT Z ssig_T dead_sig_map;
   644   in
   645     Library.foldl1 HOLogic.mk_comp [Oper, dead_sig_map' $ VLeaf, Sig, inr']
   646   end;
   647 
   648 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
   649     dead_old_sig_map Sig old_Oper old_VLeaf old_CLeaf Oper VLeaf CLeaf lthy =
   650   let
   651     val embL_b = mk_version_fp_binding true lthy version fp_b name;
   652     val old_ssig_old_sig_T = Tsubst Y old_ssig_T old_sig_T;
   653     val ssig_old_sig_T = Tsubst Y ssig_T old_sig_T;
   654     val ssig_other_summand_T = Tsubst Y ssig_T other_summand_T;
   655 
   656     val sigx = Var (("s", 0), old_ssig_old_sig_T);
   657     val x = Var (("x", 0), Y);
   658     val j = Var (("j", 0), fpT);
   659     val embL = Free (Binding.name_of embL_b, old_ssig_T --> ssig_T);
   660     val dead_old_sig_map' = Term.subst_atomic_types [(Y, old_ssig_T), (Z, ssig_T)] dead_old_sig_map;
   661     val Sig' = substT Y ssig_T Sig;
   662     val inl' = Inl_or_r_const ssig_old_sig_T ssig_other_summand_T;
   663 
   664     val Oper_eq = mk_Trueprop_eq (embL $ (old_Oper $ sigx),
   665         Oper $ (Sig' $ (inl' $ (dead_old_sig_map' $ embL $ sigx))))
   666       |> Logic.all sigx;
   667     val VLeaf_eq = mk_Trueprop_eq (embL $ (old_VLeaf $ x), VLeaf $ x)
   668       |> Logic.all x;
   669     val CLeaf_eq = mk_Trueprop_eq (embL $ (old_CLeaf $ j), CLeaf $ j)
   670       |> Logic.all j;
   671   in
   672     define_single_primrec embL_b [Oper_eq, VLeaf_eq, CLeaf_eq] lthy
   673   end;
   674 
   675 fun define_Lam_base fp_b version Y Z preT ssig_T dead_pre_map Sig unsig dead_sig_map Oper VLeaf
   676     lthy =
   677   let
   678     val YpreT = HOLogic.mk_prodT (Y, preT);
   679 
   680     val snd' = snd_const YpreT;
   681     val dead_pre_map' = substT Z ssig_T dead_pre_map;
   682     val Sig' = substT Y ssig_T Sig;
   683     val unsig' = substT Y ssig_T unsig;
   684     val dead_sig_map' = Term.subst_atomic_types [(Y, YpreT), (Z, ssig_T)] dead_sig_map;
   685 
   686     val rhs = HOLogic.mk_comp (unsig', dead_sig_map'
   687       $ Library.foldl1 HOLogic.mk_comp [Oper, Sig', dead_pre_map' $ VLeaf, snd']);
   688   in
   689     define_const true fp_b version LamN rhs lthy
   690   end;
   691 
   692 fun define_Lam_step_or_merge fp_b version Y preT unsig left_case right_case lthy =
   693   let
   694     val YpreT = HOLogic.mk_prodT (Y, preT);
   695 
   696     val unsig' = substT Y YpreT unsig;
   697 
   698     val rhs = HOLogic.mk_comp (mk_case_sum (left_case, right_case), unsig');
   699   in
   700     define_const true fp_b version LamN rhs lthy
   701   end;
   702 
   703 fun define_Lam_step fp_b version Y Z preT old_ssig_T ssig_T dead_pre_map unsig rho embL old_Lam
   704     lthy =
   705   let
   706     val dead_pre_map' = Term.subst_atomic_types [(Y, old_ssig_T), (Z, ssig_T)] dead_pre_map;
   707     val left_case = HOLogic.mk_comp (dead_pre_map' $ embL, old_Lam);
   708   in
   709     define_Lam_step_or_merge fp_b version Y preT unsig left_case rho lthy
   710   end;
   711 
   712 fun define_Lam_merge fp_b version Y Z preT old1_ssig_T old2_ssig_T ssig_T dead_pre_map unsig embLL
   713     embLR old1_Lam old2_Lam lthy =
   714   let
   715     val dead_pre_map' = Term.subst_atomic_types [(Y, old1_ssig_T), (Z, ssig_T)] dead_pre_map;
   716     val dead_pre_map'' = Term.subst_atomic_types [(Y, old2_ssig_T), (Z, ssig_T)] dead_pre_map;
   717     val left_case = HOLogic.mk_comp (dead_pre_map' $ embLL, old1_Lam);
   718     val right_case = HOLogic.mk_comp (dead_pre_map'' $ embLR, old2_Lam);
   719   in
   720     define_Lam_step_or_merge fp_b version Y preT unsig left_case right_case lthy
   721   end;
   722 
   723 fun define_proto_sctr_step_or_merge fp_b version old_sig_T right_T Sig old_proto_sctr =
   724   let
   725     val rhs = Library.foldl1 HOLogic.mk_comp [Sig, Inl_const old_sig_T right_T, old_proto_sctr];
   726   in
   727     define_const true fp_b version proto_sctrN rhs
   728   end;
   729 
   730 fun define_flat fp_b version Y Z fpT sig_T ssig_T Oper VLeaf CLeaf dead_sig_map lthy =
   731   let
   732     val flat_b = mk_version_fp_binding true lthy version fp_b flatN;
   733     val ssig_sig_T = Tsubst Y ssig_T sig_T;
   734     val ssig_ssig_sig_T = Tsubst Y ssig_T ssig_sig_T;
   735     val ssig_ssig_T = Tsubst Y ssig_T ssig_T;
   736 
   737     val sigx = Var (("s", 0), ssig_ssig_sig_T);
   738     val x = Var (("x", 0), ssig_T);
   739     val j = Var (("j", 0), fpT);
   740     val flat = Free (Binding.name_of flat_b, ssig_ssig_T --> ssig_T);
   741     val Oper' = substT Y ssig_T Oper;
   742     val VLeaf' = substT Y ssig_T VLeaf;
   743     val CLeaf' = substT Y ssig_T CLeaf;
   744     val dead_sig_map' = Term.subst_atomic_types [(Y, ssig_ssig_T), (Z, ssig_T)] dead_sig_map;
   745 
   746     val Oper_eq = mk_Trueprop_eq (flat $ (Oper' $ sigx), Oper $ (dead_sig_map' $ flat $ sigx))
   747       |> Logic.all sigx;
   748     val VLeaf_eq = mk_Trueprop_eq (flat $ (VLeaf' $ x), x)
   749       |> Logic.all x;
   750     val CLeaf_eq = mk_Trueprop_eq (flat $ (CLeaf' $ j), CLeaf $ j)
   751       |> Logic.all j;
   752   in
   753     define_single_primrec flat_b [Oper_eq, VLeaf_eq, CLeaf_eq] lthy
   754   end;
   755 
   756 fun define_eval_core fp_b version Y Z preT fpT sig_T ssig_T dtor Oper VLeaf CLeaf dead_pre_map
   757     dead_sig_map dead_ssig_map flat Lam lthy =
   758   let
   759     val eval_core_b = mk_version_fp_binding true lthy version fp_b eval_coreN;
   760     val YpreT = HOLogic.mk_prodT (Y, preT);
   761     val Ypre_ssig_T = Tsubst Y YpreT ssig_T;
   762     val Ypre_ssig_sig_T = Tsubst Y Ypre_ssig_T sig_T;
   763     val ssig_preT = Tsubst Y ssig_T preT;
   764     val ssig_YpreT = Tsubst Y ssig_T YpreT;
   765     val ssig_ssig_T = Tsubst Y ssig_T ssig_T;
   766 
   767     val sigx = Var (("s", 0), Ypre_ssig_sig_T);
   768     val x = Var (("x", 0), YpreT);
   769     val j = Var (("j", 0), fpT);
   770     val eval_core = Free (Binding.name_of eval_core_b, Ypre_ssig_T --> ssig_preT);
   771     val Oper' = substT Y YpreT Oper;
   772     val VLeaf' = substT Y YpreT VLeaf;
   773     val CLeaf' = substT Y YpreT CLeaf;
   774     val dead_pre_map' = Term.subst_atomic_types [(Y, ssig_ssig_T), (Z, ssig_T)] dead_pre_map;
   775     val dead_pre_map'' = substT Z ssig_T dead_pre_map;
   776     val dead_pre_map''' = Term.subst_atomic_types [(Y, fpT), (Z, ssig_T)] dead_pre_map;
   777     val dead_sig_map' = Term.subst_atomic_types [(Y, Ypre_ssig_T), (Z, ssig_YpreT)] dead_sig_map;
   778     val dead_ssig_map' = Term.subst_atomic_types [(Y, YpreT), (Z, Y)] dead_ssig_map;
   779     val Lam' = substT Y ssig_T Lam;
   780     val fst' = fst_const YpreT;
   781     val snd' = snd_const YpreT;
   782 
   783     val Oper_eq = mk_Trueprop_eq (eval_core $ (Oper' $ sigx),
   784         dead_pre_map' $ flat $ (Lam' $ (dead_sig_map' $ (Abs (Name.uu, Ypre_ssig_T,
   785           HOLogic.mk_prod (dead_ssig_map' $ fst' $ Bound 0, eval_core $ Bound 0))) $ sigx)))
   786       |> Logic.all sigx;
   787     val VLeaf_eq = mk_Trueprop_eq (eval_core $ (VLeaf' $ x), dead_pre_map'' $ VLeaf $ (snd' $ x))
   788       |> Logic.all x;
   789     val CLeaf_eq = mk_Trueprop_eq (eval_core $ (CLeaf' $ j), dead_pre_map''' $ CLeaf $ (dtor $ j))
   790       |> Logic.all j;
   791   in
   792     define_single_primrec eval_core_b [Oper_eq, VLeaf_eq, CLeaf_eq] lthy
   793   end;
   794 
   795 fun define_eval fp_b version Y Z preT fpT ssig_T dtor dtor_unfold dead_ssig_map eval_core lthy =
   796   let
   797     val fp_preT = Tsubst Y fpT preT;
   798     val fppreT = HOLogic.mk_prodT (fpT, fp_preT);
   799     val fp_ssig_T = Tsubst Y fpT ssig_T;
   800 
   801     val dtor_unfold' = substT Z fp_ssig_T dtor_unfold;
   802     val dead_ssig_map' = Term.subst_atomic_types [(Y, fpT), (Z, fppreT)] dead_ssig_map;
   803     val eval_core' = substT Y fpT eval_core;
   804     val id' = HOLogic.id_const fpT;
   805 
   806     val rhs = dtor_unfold' $ HOLogic.mk_comp (eval_core', dead_ssig_map' $ mk_convol (id', dtor));
   807   in
   808     define_const true fp_b version evalN rhs lthy
   809   end;
   810 
   811 fun define_cutSsig fp_b version Y Z preT ssig_T dead_pre_map VLeaf dead_ssig_map flat eval_core
   812     lthy =
   813   let
   814     val ssig_preT = Tsubst Y ssig_T preT;
   815     val ssig_ssig_T = Tsubst Y ssig_T ssig_T;
   816     val ssig_ssig_preT = HOLogic.mk_prodT (ssig_T, ssig_preT);
   817 
   818     val h = Var (("h", 0), Y --> ssig_preT);
   819     val dead_pre_map' = Term.subst_atomic_types [(Y, ssig_ssig_T), (Z, ssig_T)] dead_pre_map;
   820     val dead_ssig_map' = substT Z ssig_ssig_preT dead_ssig_map;
   821     val eval_core' = substT Y ssig_T eval_core;
   822 
   823     val rhs = Library.foldl1 HOLogic.mk_comp [dead_pre_map' $ flat, eval_core',
   824         dead_ssig_map' $ mk_convol (VLeaf, h)]
   825       |> Term.lambda h;
   826   in
   827     define_const true fp_b version cutSsigN rhs lthy
   828   end;
   829 
   830 fun define_algLam fp_b version Y Z fpT ssig_T Oper VLeaf dead_sig_map eval lthy =
   831   let
   832     val fp_ssig_T = Tsubst Y fpT ssig_T;
   833 
   834     val Oper' = substT Y fpT Oper;
   835     val VLeaf' = substT Y fpT VLeaf;
   836     val dead_sig_map' = Term.subst_atomic_types [(Y, fpT), (Z, fp_ssig_T)] dead_sig_map;
   837 
   838     val rhs = Library.foldl1 HOLogic.mk_comp [eval, Oper', dead_sig_map' $ VLeaf'];
   839   in
   840     define_const true fp_b version algLamN rhs lthy
   841   end;
   842 
   843 fun define_corecU fp_b version Y Z preT ssig_T dtor_unfold VLeaf cutSsig lthy =
   844   let
   845     val ssig_preT = Tsubst Y ssig_T preT;
   846 
   847     val h = Var (("h", 0), Y --> ssig_preT);
   848     val dtor_unfold' = substT Z ssig_T dtor_unfold;
   849 
   850     val rhs = HOLogic.mk_comp (dtor_unfold' $ (cutSsig $ h), VLeaf)
   851       |> Term.lambda h;
   852   in
   853     define_const true fp_b version corecUN rhs lthy
   854   end;
   855 
   856 fun define_corecUU fp_b version Y Z preT ssig_T dead_pre_map dead_ssig_map flat eval_core sctr
   857     corecU lthy =
   858   let
   859     val ssig_preT = Tsubst Y ssig_T preT;
   860     val ssig_ssig_T = Tsubst Y ssig_T ssig_T
   861     val ssig_ssig_preT = HOLogic.mk_prodT (ssig_T, ssig_preT);
   862 
   863     val ssig_pre_ssig_T = Tsubst Y ssig_preT ssig_T;
   864 
   865     val h = Var (("h", 0), Y --> ssig_pre_ssig_T);
   866     val dead_pre_map' = Term.subst_atomic_types [(Y, ssig_ssig_T), (Z, ssig_T)] dead_pre_map;
   867     val eval_core' = substT Y ssig_T eval_core;
   868     val dead_ssig_map' =
   869       Term.subst_atomic_types [(Y, ssig_preT), (Z, ssig_ssig_preT)] dead_ssig_map;
   870     val id' = HOLogic.id_const ssig_preT;
   871 
   872     val rhs = corecU $ Library.foldl1 HOLogic.mk_comp
   873         [dead_pre_map' $ flat, eval_core', dead_ssig_map' $ mk_convol (sctr, id'), h]
   874       |> Term.lambda h;
   875   in
   876     define_const true fp_b version corecUUN rhs lthy
   877   end;
   878 
   879 fun derive_sig_transfer maybe_swap ctxt live_AsBs pre_rel sig_rel Rs R const pre_rel_def
   880     preT_rel_eqs transfer_thm =
   881   let
   882     val RRpre_rel = list_comb (pre_rel, Rs) $ R;
   883     val RRsig_rel = list_comb (sig_rel, Rs) $ R;
   884     val constB = Term.subst_atomic_types live_AsBs const;
   885 
   886     val goal = uncurry mk_rel_fun (maybe_swap (RRpre_rel, RRsig_rel)) $ const $ constB
   887       |> HOLogic.mk_Trueprop;
   888   in
   889     Variable.add_free_names ctxt goal []
   890     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
   891       mk_sig_transfer_tac ctxt pre_rel_def preT_rel_eqs transfer_thm))
   892     |> Thm.close_derivation
   893   end;
   894 
   895 fun derive_transfer_by_transfer_prover ctxt live_AsBs Rs R const const_defs rel_eqs transfers =
   896   let
   897     val constB = Term.subst_atomic_types live_AsBs const;
   898     val goal = mk_parametricity_goal ctxt (Rs @ [R]) const constB;
   899   in
   900     Variable.add_free_names ctxt goal []
   901     |> (fn vars => Goal.prove_sorry (*FIXME*) (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
   902       mk_transfer_by_transfer_prover_tac ctxt (const_defs @ map (fn thm => thm RS sym) rel_eqs)
   903         rel_eqs transfers))
   904     |> Thm.close_derivation
   905   end;
   906 
   907 fun derive_dtor_transfer ctxt live_EsFs Y Z pre_rel fp_rel Rs dtor dtor_rel_thm =
   908   let
   909     val Type (@{type_name fun}, [fpT, Type (@{type_name fun}, [fpTB, @{typ bool}])]) =
   910       snd (strip_typeN (length live_EsFs) (fastype_of fp_rel));
   911 
   912     val pre_rel' = Term.subst_atomic_types [(Y, fpT), (Z, fpTB)] pre_rel;
   913     val Rpre_rel = list_comb (pre_rel', Rs);
   914     val Rfp_rel = list_comb (fp_rel, Rs);
   915     val dtorB = Term.subst_atomic_types live_EsFs dtor;
   916 
   917     val goal = HOLogic.mk_Trueprop (mk_rel_fun Rfp_rel (Rpre_rel $ Rfp_rel) $ dtor $ dtorB);
   918   in
   919     Variable.add_free_names ctxt goal []
   920     |> (fn vars => Goal.prove_sorry (*FIXME*) (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
   921       mk_dtor_transfer_tac ctxt dtor_rel_thm))
   922     |> Thm.close_derivation
   923   end;
   924 
   925 fun derive_Lam_or_eval_core_transfer ctxt live_AsBs Y Z preT ssig_T Rs R pre_rel sig_or_ssig_rel
   926     ssig_rel const const_def rel_eqs transfers =
   927   let
   928     val YpreT = HOLogic.mk_prodT (Y, preT);
   929     val ZpreTB = typ_subst_atomic live_AsBs YpreT;
   930     val ssig_TB = typ_subst_atomic live_AsBs ssig_T;
   931 
   932     val pre_rel' = Term.subst_atomic_types [(Y, ssig_T), (Z, ssig_TB)] pre_rel;
   933     val sig_or_ssig_rel' = Term.subst_atomic_types [(Y, YpreT), (Z, ZpreTB)] sig_or_ssig_rel;
   934     val Rsig_or_ssig_rel' = list_comb (sig_or_ssig_rel', Rs);
   935     val RRpre_rel = list_comb (pre_rel, Rs) $ R;
   936     val RRssig_rel = list_comb (ssig_rel, Rs) $ R;
   937     val Rpre_rel' = list_comb (pre_rel', Rs);
   938     val constB = subst_atomic_types live_AsBs const;
   939 
   940     val goal = mk_rel_fun (Rsig_or_ssig_rel' $ mk_rel_prod R RRpre_rel) (Rpre_rel' $ RRssig_rel)
   941         $ const $ constB
   942       |> HOLogic.mk_Trueprop;
   943   in
   944     Variable.add_free_names ctxt goal []
   945     |> (fn vars => Goal.prove_sorry (*FIXME*) (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
   946       mk_transfer_by_transfer_prover_tac ctxt [const_def] rel_eqs transfers))
   947     |> Thm.close_derivation
   948   end;
   949 
   950 fun derive_proto_sctr_transfer_step_or_merge ctxt Y Z R dead_pre_rel dead_sig_rel proto_sctr
   951     proto_sctr_def fp_k_T_rel_eqs transfers =
   952   let
   953     val proto_sctrZ = substT Y Z proto_sctr;
   954     val goal = mk_rel_fun (dead_pre_rel $ R) (dead_sig_rel $ R) $ proto_sctr $ proto_sctrZ
   955       |> HOLogic.mk_Trueprop;
   956   in
   957     Variable.add_free_names ctxt goal []
   958     |> (fn vars => Goal.prove_sorry (*FIXME*) (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
   959       mk_transfer_by_transfer_prover_tac ctxt [proto_sctr_def] fp_k_T_rel_eqs transfers))
   960     |> Thm.close_derivation
   961   end;
   962 
   963 fun derive_sctr_transfer ctxt live_AsBs Y Z ssig_T Rs R pre_rel ssig_rel sctr sctr_def
   964     fp_k_T_rel_eqs transfers =
   965   let
   966     val ssig_TB = typ_subst_atomic live_AsBs ssig_T;
   967 
   968     val pre_rel' = Term.subst_atomic_types [(Y, ssig_T), (Z, ssig_TB)] pre_rel;
   969     val Rpre_rel' = list_comb (pre_rel', Rs);
   970     val RRssig_rel = list_comb (ssig_rel, Rs) $ R;
   971     val sctrB = subst_atomic_types live_AsBs sctr;
   972 
   973     val goal = HOLogic.mk_Trueprop (mk_rel_fun (Rpre_rel' $ RRssig_rel) RRssig_rel $ sctr $ sctrB);
   974   in
   975     Variable.add_free_names ctxt goal []
   976     |> (fn vars => Goal.prove_sorry (*FIXME*) (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
   977       mk_transfer_by_transfer_prover_tac ctxt [sctr_def] fp_k_T_rel_eqs transfers))
   978     |> Thm.close_derivation
   979   end;
   980 
   981 fun derive_corecUU_transfer ctxt live_AsBs Y Z Rs R preT ssig_T pre_rel fp_rel ssig_rel corecUU
   982     cutSsig_def corecU_def corecUU_def fp_k_T_rel_eqs transfers =
   983   let
   984     val ssig_preT = Tsubst Y ssig_T preT;
   985     val ssig_TB = typ_subst_atomic live_AsBs ssig_T;
   986     val ssig_preTB = typ_subst_atomic live_AsBs ssig_preT;
   987 
   988     val pre_rel' = Term.subst_atomic_types [(Y, ssig_T), (Z, ssig_TB)] pre_rel;
   989     val ssig_rel' = Term.subst_atomic_types [(Y, ssig_preT), (Z, ssig_preTB)] ssig_rel;
   990     val Rpre_rel' = list_comb (pre_rel', Rs);
   991     val Rfp_rel = list_comb (fp_rel, Rs);
   992     val RRssig_rel = list_comb (ssig_rel, Rs) $ R;
   993     val Rssig_rel' = list_comb (ssig_rel', Rs);
   994     val corecUUB = subst_atomic_types live_AsBs corecUU;
   995 
   996     val goal = mk_rel_fun (mk_rel_fun R (Rssig_rel' $ (Rpre_rel' $ RRssig_rel)))
   997         (mk_rel_fun R Rfp_rel) $ corecUU $ corecUUB
   998       |> HOLogic.mk_Trueprop;
   999   in
  1000     Variable.add_free_names ctxt goal []
  1001     |> (fn vars => Goal.prove_sorry (*FIXME*) (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1002       mk_transfer_by_transfer_prover_tac ctxt [cutSsig_def, corecU_def, corecUU_def] fp_k_T_rel_eqs
  1003         transfers))
  1004     |> Thm.close_derivation
  1005   end;
  1006 
  1007 fun mk_natural_goal ctxt simple_T_mapfs fs t u =
  1008   let
  1009     fun build_simple (T, _) =
  1010       (case AList.lookup (op =) simple_T_mapfs T of
  1011         SOME mapf => mapf
  1012       | NONE => the (find_first (fn f => domain_type (fastype_of f) = T) fs));
  1013 
  1014     val simple_Ts = map fst simple_T_mapfs;
  1015 
  1016     val t_map = build_map ctxt simple_Ts build_simple (apply2 (range_type o fastype_of) (t, u));
  1017     val u_map = build_map ctxt simple_Ts build_simple (apply2 (domain_type o fastype_of) (t, u));
  1018   in
  1019     mk_Trueprop_eq (HOLogic.mk_comp (u, u_map), HOLogic.mk_comp (t_map, t))
  1020   end;
  1021 
  1022 fun derive_natural_by_unfolding ctxt live_AsBs preT pre_map fs f const map_thms =
  1023   let
  1024     val ffpre_map = list_comb (pre_map, fs) $ f;
  1025     val constB = subst_atomic_types live_AsBs const;
  1026 
  1027     val goal = mk_natural_goal ctxt [(preT, ffpre_map)] (fs @ [f]) const constB;
  1028   in
  1029     Variable.add_free_names ctxt goal []
  1030     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1031       mk_natural_by_unfolding_tac ctxt map_thms))
  1032     |> Thm.close_derivation
  1033   end;
  1034 
  1035 fun derive_natural_from_transfer ctxt live_AsBs simple_T_mapfs fs f const transfer bnfs subst_bnfs =
  1036   let
  1037     val m = length live_AsBs;
  1038 
  1039     val constB = Term.subst_atomic_types live_AsBs const;
  1040     val goal = mk_natural_goal ctxt simple_T_mapfs (fs @ [f]) const constB;
  1041   in
  1042     Variable.add_free_names ctxt goal []
  1043     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1044       mk_natural_from_transfer_tac ctxt m (replicate m true) transfer [] (map rel_Grp_of_bnf bnfs)
  1045         (map rel_Grp_of_bnf subst_bnfs)))
  1046     |> Thm.close_derivation
  1047   end;
  1048 
  1049 fun derive_natural_from_transfer_with_pre_type ctxt live_AsBs Y Z preT ssig_T pre_map ssig_map fs
  1050     f =
  1051   let
  1052     val ssig_TB = typ_subst_atomic live_AsBs ssig_T;
  1053     val preT' = Term.typ_subst_atomic [(Y, ssig_T), (Z, ssig_TB)] preT;
  1054 
  1055     val ffpre_map = list_comb (pre_map, fs) $ f;
  1056     val pre_map' = Term.subst_atomic_types [(Y, ssig_T), (Z, ssig_TB)] pre_map;
  1057     val fpre_map' = list_comb (pre_map', fs);
  1058     val ffssig_map = list_comb (ssig_map, fs) $ f;
  1059 
  1060     val preT_mapfs = [(preT, ffpre_map), (preT', fpre_map' $ ffssig_map)];
  1061   in
  1062     derive_natural_from_transfer ctxt live_AsBs preT_mapfs fs f
  1063   end;
  1064 
  1065 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
  1066     Lam rho unsig_thm Lam_def =
  1067   let
  1068     val YpreT = HOLogic.mk_prodT (Y, preT);
  1069     val Ypre_old_sig_T = Tsubst Y YpreT old_sig_T;
  1070     val Ypre_k_T = Tsubst Y YpreT k_T;
  1071 
  1072     val inl' = Inl_const Ypre_old_sig_T Ypre_k_T;
  1073     val inr' = Inr_const Ypre_old_sig_T Ypre_k_T;
  1074     val dead_pre_map' = Term.subst_atomic_types [(Y, old_ssig_T), (Z, ssig_T)] dead_pre_map;
  1075     val Sig' = substT Y YpreT Sig;
  1076     val Lam_o_Sig = HOLogic.mk_comp (Lam, Sig');
  1077 
  1078     val inl_goal = mk_Trueprop_eq (HOLogic.mk_comp (Lam_o_Sig, inl'),
  1079       HOLogic.mk_comp (dead_pre_map' $ embL, old_Lam));
  1080     val inr_goal = mk_Trueprop_eq (HOLogic.mk_comp (Lam_o_Sig, inr'), rho);
  1081     val goals = [inl_goal, inr_goal];
  1082     val goal = Logic.mk_conjunction_balanced goals;
  1083   in
  1084     Variable.add_free_names ctxt goal []
  1085     |> (fn vars => Goal.prove_sorry ctxt vars [] goal
  1086       (fn {context = ctxt, prems = _} => mk_Lam_Inl_Inr_tac ctxt unsig_thm Lam_def))
  1087     |> Conjunction.elim_balanced (length goals)
  1088     |> map Thm.close_derivation
  1089   end;
  1090 
  1091 fun derive_flat_VLeaf ctxt Y Z ssig_T x VLeaf dead_ssig_map flat ssig_induct fp_map_id sig_map_cong
  1092     sig_map_ident sig_map_comp ssig_map_thms flat_simps =
  1093   let
  1094     val x' = substT Y ssig_T x;
  1095     val dead_ssig_map' = substT Z ssig_T dead_ssig_map;
  1096 
  1097     val goal = mk_Trueprop_eq (flat $ (dead_ssig_map' $ VLeaf $ x'), x');
  1098 
  1099     val ssig_induct' = infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt x')] ssig_induct;
  1100   in
  1101     Variable.add_free_names ctxt goal []
  1102     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1103       mk_flat_VLeaf_or_flat_tac ctxt ssig_induct' sig_map_cong
  1104         (fp_map_id :: sig_map_ident :: sig_map_comp :: ssig_map_thms @ flat_simps @
  1105          @{thms o_apply id_apply id_def[symmetric]})))
  1106     |> Thm.close_derivation
  1107   end;
  1108 
  1109 fun derive_flat_flat ctxt Y Z ssig_T x dead_ssig_map flat ssig_induct fp_map_id sig_map_cong
  1110     sig_map_comp ssig_map_thms flat_simps =
  1111   let
  1112     val ssig_ssig_T = Tsubst Y ssig_T ssig_T;
  1113     val ssig_ssig_ssig_T = Tsubst Y ssig_T ssig_ssig_T;
  1114 
  1115     val x' = substT Y ssig_ssig_ssig_T x;
  1116     val dead_ssig_map' = Term.subst_atomic_types [(Y, ssig_ssig_T), (Z, ssig_T)] dead_ssig_map;
  1117     val flat' = substT Y ssig_T flat;
  1118 
  1119     val goal = mk_Trueprop_eq (flat $ (dead_ssig_map' $ flat $ x'), flat $ (flat' $ x'));
  1120 
  1121     val ssig_induct' = infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt x')] ssig_induct;
  1122   in
  1123     Variable.add_free_names ctxt goal []
  1124     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1125       mk_flat_VLeaf_or_flat_tac ctxt ssig_induct' sig_map_cong
  1126         (o_apply :: fp_map_id :: sig_map_comp :: ssig_map_thms @ flat_simps)))
  1127     |> Thm.close_derivation
  1128   end;
  1129 
  1130 fun derive_eval_core_flat ctxt Y Z preT ssig_T dead_pre_map dead_ssig_map flat eval_core x
  1131     ssig_induct dead_pre_map_id dead_pre_map_comp0 dead_pre_map_comp fp_map_id sig_map_comp
  1132     sig_map_cong ssig_map_thms ssig_map_comp flat_simps flat_pointful_natural flat_flat
  1133     Lam_pointful_natural eval_core_simps =
  1134   let
  1135     val YpreT = HOLogic.mk_prodT (Y, preT);
  1136     val ssig_ssig_T = Tsubst Y ssig_T ssig_T;
  1137     val Ypre_ssig_T = Tsubst Y YpreT ssig_T;
  1138     val Ypre_ssig_ssig_T = Tsubst Y YpreT ssig_ssig_T;
  1139     val ssig_YpreT = Tsubst Y ssig_T YpreT;
  1140 
  1141     val dead_pre_map' = Term.subst_atomic_types [(Y, ssig_ssig_T), (Z, ssig_T)] dead_pre_map;
  1142     val dead_ssig_map' = Term.subst_atomic_types [(Y, Ypre_ssig_T), (Z, ssig_YpreT)] dead_ssig_map;
  1143     val dead_ssig_map'' = Term.subst_atomic_types [(Y, YpreT), (Z, Y)] dead_ssig_map;
  1144     val flat' = substT Y YpreT flat;
  1145     val eval_core' = substT Y ssig_T eval_core;
  1146     val x' = substT Y Ypre_ssig_ssig_T x;
  1147     val fst' = fst_const YpreT;
  1148 
  1149     val goal = mk_Trueprop_eq (eval_core $ (flat' $ x'), dead_pre_map' $ flat
  1150       $ (eval_core' $ (dead_ssig_map' $ mk_convol (dead_ssig_map'' $ fst', eval_core) $ x')));
  1151 
  1152     val ssig_induct' = infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt x')] ssig_induct;
  1153   in
  1154     Variable.add_free_names ctxt goal []
  1155     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1156       mk_eval_core_flat_tac ctxt ssig_induct' dead_pre_map_id dead_pre_map_comp0 dead_pre_map_comp
  1157         fp_map_id sig_map_comp sig_map_cong ssig_map_thms ssig_map_comp flat_simps
  1158         flat_pointful_natural flat_flat Lam_pointful_natural eval_core_simps))
  1159     |> Thm.close_derivation
  1160   end;
  1161 
  1162 fun derive_eval_thm ctxt dtor_inject dtor_unfold_thm eval_def =
  1163   (trans OF [iffD2 OF [dtor_inject, eval_def RS meta_eq_to_obj_eq RS fun_cong], dtor_unfold_thm])
  1164   |> unfold_thms ctxt [o_apply, eval_def RS Drule.symmetric_thm];
  1165 
  1166 fun derive_eval_flat ctxt Y Z fpT ssig_T dead_ssig_map flat eval x dead_pre_map_comp0
  1167     dtor_unfold_unique ssig_map_id ssig_map_comp flat_pointful_natural eval_core_pointful_natural
  1168     eval_core_flat eval_thm =
  1169   let
  1170     val fp_ssig_T = Tsubst Y fpT ssig_T;
  1171     val fp_ssig_ssig_T = Tsubst Y fp_ssig_T ssig_T;
  1172 
  1173     val dead_ssig_map' = Term.subst_atomic_types [(Y, fp_ssig_T), (Z, fpT)] dead_ssig_map;
  1174     val flat' = substT Y fpT flat;
  1175     val x' = substT Y fp_ssig_ssig_T x;
  1176 
  1177     val goal = mk_Trueprop_eq (eval $ (flat' $ x'), eval $ (dead_ssig_map' $ eval $ x'));
  1178 
  1179     val cond_eval_o_flat =
  1180       infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt (HOLogic.mk_comp (eval, flat')))]
  1181         (trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym] RS fun_cong)
  1182       OF [ext, ext];
  1183   in
  1184     Variable.add_free_names ctxt goal []
  1185     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1186       mk_eval_flat_tac ctxt dead_pre_map_comp0 ssig_map_id ssig_map_comp flat_pointful_natural
  1187         eval_core_pointful_natural eval_core_flat eval_thm cond_eval_o_flat))
  1188     |> Thm.close_derivation
  1189   end;
  1190 
  1191 fun derive_eval_Oper ctxt live Y Z fpT sig_T ssig_T dead_sig_map Oper eval algLam x sig_map_ident
  1192     sig_map_comp0 sig_map_comp Oper_natural_pointful VLeaf_natural flat_simps eval_flat algLam_def =
  1193   let
  1194     val fp_ssig_T = Tsubst Y fpT ssig_T;
  1195     val fp_ssig_sig_T = Tsubst Y fp_ssig_T sig_T;
  1196 
  1197     val dead_sig_map' = Term.subst_atomic_types [(Y, fp_ssig_T), (Z, fpT)] dead_sig_map;
  1198     val Oper' = substT Y fpT Oper;
  1199     val x' = substT Y fp_ssig_sig_T x;
  1200 
  1201     val goal = mk_Trueprop_eq (eval $ (Oper' $ x'), algLam $ (dead_sig_map' $ eval $ x'));
  1202   in
  1203     Variable.add_free_names ctxt goal []
  1204     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1205       mk_eval_Oper_tac ctxt live sig_map_ident sig_map_comp0 sig_map_comp Oper_natural_pointful
  1206         VLeaf_natural flat_simps eval_flat algLam_def))
  1207     |> Thm.close_derivation
  1208   end;
  1209 
  1210 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
  1211     dtor_unfold_unique V_or_CLeaf_map_thm eval_core_simps eval_thm =
  1212   let
  1213     val V_or_CLeaf' = substT Y fpT V_or_CLeaf;
  1214     val x' = substT Y fpT x;
  1215 
  1216     val goal = mk_Trueprop_eq (eval $ (V_or_CLeaf' $ x'), x');
  1217   in
  1218     Variable.add_free_names ctxt goal []
  1219     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1220       mk_eval_V_or_CLeaf_tac ctxt dead_pre_map_id dead_pre_map_comp fp_map_id dtor_unfold_unique
  1221         V_or_CLeaf_map_thm eval_core_simps eval_thm))
  1222     |> Thm.close_derivation
  1223   end;
  1224 
  1225 fun derive_extdd_mor ctxt Y Z preT fpT ssig_T dead_pre_map dtor extdd cutSsig f g dead_pre_map_comp0
  1226     dead_pre_map_comp VLeaf_map_thm ssig_map_comp flat_pointful_natural eval_core_pointful_natural
  1227     eval_thm eval_flat eval_VLeaf cutSsig_def =
  1228   let
  1229     val ssig_preT = Tsubst Y ssig_T preT;
  1230 
  1231     val dead_pre_map' = Term.subst_atomic_types [(Y, ssig_T), (Z, fpT)] dead_pre_map;
  1232     val f' = substT Z fpT f;
  1233     val g' = substT Z ssig_preT g;
  1234     val extdd_f = extdd $ f';
  1235 
  1236     val prem = mk_Trueprop_eq (HOLogic.mk_comp (dead_pre_map' $ extdd_f, g'),
  1237       HOLogic.mk_comp (dtor, f'));
  1238     val goal = mk_Trueprop_eq (HOLogic.mk_comp (dead_pre_map' $ extdd_f, cutSsig $ g'),
  1239       HOLogic.mk_comp (dtor, extdd_f));
  1240   in
  1241     fold (Variable.add_free_names ctxt) [prem, goal] []
  1242     |> (fn vars => Goal.prove_sorry ctxt vars [prem] goal (fn {context = ctxt, prems = [prem]} =>
  1243       mk_extdd_mor_tac ctxt dead_pre_map_comp0 dead_pre_map_comp VLeaf_map_thm ssig_map_comp
  1244         flat_pointful_natural eval_core_pointful_natural eval_thm eval_flat eval_VLeaf cutSsig_def
  1245         prem))
  1246     |> Thm.close_derivation
  1247   end;
  1248 
  1249 fun derive_mor_cutSsig_flat ctxt Y Z preT fpT ssig_T dead_pre_map dead_ssig_map dtor flat eval_core
  1250     eval cutSsig f g dead_pre_map_comp0 dead_pre_map_comp dead_pre_map_cong dtor_unfold_unique
  1251     dead_ssig_map_comp0 ssig_map_comp flat_simps flat_pointful_natural eval_core_pointful_natural
  1252     flat_flat flat_VLeaf eval_core_flat cutSsig_def cutSsig_def_pointful_natural eval_thm =
  1253   let
  1254     val ssig_preT = Tsubst Y ssig_T preT;
  1255 
  1256     val substYZ = Term.subst_atomic_types [(Y, ssig_T), (Z, fpT)];
  1257 
  1258     val dead_pre_map' = substYZ dead_pre_map;
  1259     val dead_ssig_map' = substYZ dead_ssig_map;
  1260     val f' = substYZ f;
  1261     val g' = substT Z ssig_preT g;
  1262     val cutSsig_g = cutSsig $ g';
  1263 
  1264     val id' = HOLogic.id_const ssig_T;
  1265     val convol' = mk_convol (id', cutSsig_g);
  1266     val dead_ssig_map'' =
  1267       Term.subst_atomic_types [(Y, ssig_T), (Z, range_type (fastype_of convol'))] dead_ssig_map;
  1268     val eval_core' = substT Y ssig_T eval_core;
  1269     val eval_core_o_map = HOLogic.mk_comp (eval_core', dead_ssig_map'' $ convol');
  1270 
  1271     val prem = mk_Trueprop_eq (HOLogic.mk_comp (dead_pre_map' $ f', cutSsig_g),
  1272       HOLogic.mk_comp (dtor, f'));
  1273     val goal = mk_Trueprop_eq (HOLogic.mk_comp (eval, dead_ssig_map' $ f'),
  1274       HOLogic.mk_comp (f', flat));
  1275   in
  1276     fold (Variable.add_free_names ctxt) [prem, goal] []
  1277     |> (fn vars => Goal.prove_sorry ctxt vars [prem] goal (fn {context = ctxt, prems = [prem]} =>
  1278       mk_mor_cutSsig_flat_tac ctxt eval_core_o_map dead_pre_map_comp0 dead_pre_map_comp
  1279         dead_pre_map_cong dtor_unfold_unique dead_ssig_map_comp0 ssig_map_comp flat_simps
  1280         flat_pointful_natural eval_core_pointful_natural flat_flat flat_VLeaf eval_core_flat
  1281         cutSsig_def cutSsig_def_pointful_natural eval_thm prem))
  1282     |> Thm.close_derivation
  1283   end;
  1284 
  1285 fun derive_extdd_o_VLeaf ctxt Y Z preT fpT ssig_T dead_pre_map dtor VLeaf extdd f g
  1286     dead_pre_map_comp0 dead_pre_map_comp dtor_inject ssig_map_thms eval_core_simps eval_thm
  1287     eval_VLeaf =
  1288   let
  1289     val ssig_preT = Tsubst Y ssig_T preT;
  1290 
  1291     val substYZ = Term.subst_atomic_types [(Y, ssig_T), (Z, fpT)];
  1292 
  1293     val dead_pre_map' = substYZ dead_pre_map;
  1294     val f' = substT Z fpT f;
  1295     val g' = substT Z ssig_preT g;
  1296     val extdd_f = extdd $ f';
  1297 
  1298     val prem = mk_Trueprop_eq (HOLogic.mk_comp (dead_pre_map' $ extdd_f, g'),
  1299       HOLogic.mk_comp (dtor, f'));
  1300     val goal = mk_Trueprop_eq (HOLogic.mk_comp (extdd_f, VLeaf), f');
  1301   in
  1302     fold (Variable.add_free_names ctxt) [prem, goal] []
  1303     |> (fn vars => Goal.prove_sorry ctxt vars [prem] goal (fn {context = ctxt, prems = [prem]} =>
  1304       mk_extdd_o_VLeaf_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_inject ssig_map_thms
  1305         eval_core_simps eval_thm eval_VLeaf prem))
  1306     |> Thm.close_derivation
  1307   end;
  1308 
  1309 fun derive_corecU_pointfree ctxt Y Z preT fpT ssig_T dead_pre_map dtor extdd corecU g
  1310     dead_pre_map_comp dtor_unfold_thm ssig_map_thms dead_ssig_map_comp0 flat_simps flat_VLeaf
  1311     eval_core_simps cutSsig_def mor_cutSsig_flat corecU_def =
  1312   let
  1313     val ssig_preT = Tsubst Y ssig_T preT;
  1314 
  1315     val substYZ = Term.subst_atomic_types [(Y, ssig_T), (Z, fpT)];
  1316 
  1317     val dead_pre_map' = substYZ dead_pre_map;
  1318     val g' = substT Z ssig_preT g;
  1319     val corecU_g = corecU $ g';
  1320 
  1321     val goal = mk_Trueprop_eq (HOLogic.mk_comp (dead_pre_map' $ (extdd $ corecU_g), g'),
  1322       HOLogic.mk_comp (dtor, corecU_g));
  1323   in
  1324     Variable.add_free_names ctxt goal []
  1325     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1326       mk_corecU_pointfree_tac ctxt dead_pre_map_comp dtor_unfold_thm ssig_map_thms
  1327       dead_ssig_map_comp0 flat_simps flat_VLeaf eval_core_simps cutSsig_def mor_cutSsig_flat
  1328       corecU_def))
  1329     |> Thm.close_derivation
  1330   end;
  1331 
  1332 fun derive_corecU_ctor_unique ctxt Y Z preT fpT ssig_T dead_pre_map ctor dtor VLeaf extdd corecU f g
  1333     dead_pre_map_comp ctor_dtor dtor_unfold_thm dtor_unfold_unique ssig_map_thms dead_ssig_map_comp0
  1334     flat_simps flat_VLeaf eval_core_simps extdd_mor extdd_o_VLeaf cutSsig_def mor_cutSsig_flat
  1335     corecU_def =
  1336   let
  1337     val corecU_pointfree = derive_corecU_pointfree ctxt Y Z preT fpT ssig_T dead_pre_map dtor extdd
  1338       corecU g dead_pre_map_comp dtor_unfold_thm ssig_map_thms dead_ssig_map_comp0 flat_simps
  1339       flat_VLeaf eval_core_simps cutSsig_def mor_cutSsig_flat corecU_def;
  1340 
  1341     val corecU_thm = corecU_pointfree RS @{thm comp_eq_dest};
  1342 
  1343     val corecU_ctor =
  1344       let
  1345         val arg_cong' =
  1346           infer_instantiate' ctxt [NONE, NONE, SOME (Thm.cterm_of ctxt ctor)] arg_cong;
  1347       in
  1348         unfold_thms ctxt [ctor_dtor] (corecU_thm RS arg_cong')
  1349       end;
  1350 
  1351     val corecU_unique =
  1352       let
  1353         val substYZ = Term.subst_atomic_types [(Y, ssig_T), (Z, fpT)];
  1354 
  1355         val f' = substYZ f;
  1356         val abs_f_o_VLeaf = Term.lambda f' (HOLogic.mk_comp (f', VLeaf));
  1357 
  1358         val inject_refine' = infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt abs_f_o_VLeaf),
  1359           SOME (Thm.cterm_of ctxt extdd)] @{thm inject_refine};
  1360       in
  1361         unfold_thms ctxt @{thms atomize_imp}
  1362           (((inject_refine' OF [extdd_o_VLeaf, extdd_o_VLeaf] RS iffD1)
  1363             OF [Drule.asm_rl, corecU_pointfree])
  1364            OF [Drule.asm_rl, trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym]
  1365              OF [extdd_mor, corecU_pointfree RS extdd_mor]])
  1366         RS @{thm obj_distinct_prems}
  1367       end;
  1368   in
  1369     (corecU_ctor, corecU_unique)
  1370   end;
  1371 
  1372 fun derive_dtor_algLam ctxt Y Z preT fpT sig_T ssig_T dead_pre_map dtor dead_sig_map Lam eval algLam
  1373     x pre_map_comp dead_pre_map_id dead_pre_map_comp0 dead_pre_map_comp sig_map_comp
  1374     Oper_pointful_natural ssig_map_thms dead_ssig_map_comp0 Lam_pointful_natural eval_core_simps
  1375     eval_thm eval_flat eval_VLeaf algLam_def =
  1376   let
  1377     val fp_preT = Tsubst Y fpT preT;
  1378     val fppreT = HOLogic.mk_prodT (fpT, fp_preT);
  1379     val fp_sig_T = Tsubst Y fpT sig_T;
  1380     val fp_ssig_T = Tsubst Y fpT ssig_T;
  1381 
  1382     val id' = HOLogic.id_const fpT;
  1383     val convol' = mk_convol (id', dtor);
  1384     val dead_pre_map' = Term.subst_atomic_types [(Y, fp_ssig_T), (Z, fpT)] dead_pre_map;
  1385     val dead_sig_map' = Term.subst_atomic_types [(Y, fpT), (Z, fppreT)] dead_sig_map;
  1386     val Lam' = substT Y fpT Lam;
  1387     val x' = substT Y fp_sig_T x;
  1388 
  1389     val goal = mk_Trueprop_eq (dtor $ (algLam $ x'),
  1390       dead_pre_map' $ eval $ (Lam' $ (dead_sig_map' $ convol' $ x')));
  1391   in
  1392     Variable.add_free_names ctxt goal []
  1393     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1394       mk_dtor_algLam_tac ctxt pre_map_comp dead_pre_map_id dead_pre_map_comp0 dead_pre_map_comp
  1395         sig_map_comp Oper_pointful_natural ssig_map_thms dead_ssig_map_comp0 Lam_pointful_natural
  1396         eval_core_simps eval_thm eval_flat eval_VLeaf algLam_def))
  1397     |> Thm.close_derivation
  1398   end;
  1399 
  1400 fun derive_algLam_base ctxt Y Z preT fpT dead_pre_map ctor dtor algLam proto_sctr dead_pre_map_id
  1401     dead_pre_map_comp ctor_dtor dtor_ctor dtor_unfold_unique unsig_thm Sig_pointful_natural
  1402     ssig_map_thms Lam_def flat_simps eval_core_simps eval_thm algLam_def =
  1403   let
  1404     val fp_preT = Tsubst Y fpT preT;
  1405 
  1406     val proto_sctr' = substT Y fpT proto_sctr;
  1407 
  1408     val dead_pre_map' = Term.subst_atomic_types [(Y, fpT), (Z, fp_preT)] dead_pre_map;
  1409     val dead_pre_map_dtor = dead_pre_map' $ dtor;
  1410 
  1411     val goal = mk_Trueprop_eq (HOLogic.mk_comp (algLam, proto_sctr'), ctor);
  1412   in
  1413     Variable.add_free_names ctxt goal []
  1414     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1415       mk_algLam_base_tac ctxt dead_pre_map_dtor dead_pre_map_id dead_pre_map_comp ctor_dtor
  1416         dtor_ctor dtor_unfold_unique unsig_thm Sig_pointful_natural ssig_map_thms Lam_def flat_simps
  1417         eval_core_simps eval_thm algLam_def))
  1418     |> Thm.close_derivation
  1419   end;
  1420 
  1421 fun derive_flat_embL ctxt Y Z old_ssig_T ssig_T dead_old_ssig_map embL old_flat flat x
  1422     old_ssig_induct fp_map_id Sig_pointful_natural old_sig_map_comp old_sig_map_cong
  1423     old_ssig_map_thms old_flat_simps flat_simps embL_simps =
  1424   let
  1425     val old_ssig_old_ssig_T = Tsubst Y old_ssig_T old_ssig_T;
  1426 
  1427     val dead_old_ssig_map' =
  1428       Term.subst_atomic_types [(Y, old_ssig_T), (Z, ssig_T)] dead_old_ssig_map;
  1429     val embL' = substT Y ssig_T embL;
  1430     val x' = substT Y old_ssig_old_ssig_T x;
  1431 
  1432     val goal = mk_Trueprop_eq (flat $ (embL' $ (dead_old_ssig_map' $ embL $ x')),
  1433       embL $ (old_flat $ x'));
  1434 
  1435     val old_ssig_induct' =
  1436       infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt x')] old_ssig_induct;
  1437   in
  1438     Variable.add_free_names ctxt goal []
  1439     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1440       mk_flat_embL_tac ctxt old_ssig_induct' fp_map_id Sig_pointful_natural old_sig_map_comp
  1441         old_sig_map_cong old_ssig_map_thms old_flat_simps flat_simps embL_simps))
  1442     |> Thm.close_derivation
  1443   end;
  1444 
  1445 fun derive_eval_core_embL ctxt Y Z preT old_ssig_T ssig_T dead_pre_map embL old_eval_core eval_core
  1446     x old_ssig_induct dead_pre_map_comp0 dead_pre_map_comp Sig_pointful_natural unsig_thm
  1447     old_sig_map_comp old_sig_map_cong old_Lam_pointful_natural Lam_def flat_embL embL_simps
  1448     embL_pointful_natural old_eval_core_simps eval_core_simps =
  1449   let
  1450     val YpreT = HOLogic.mk_prodT (Y, preT);
  1451     val Ypre_old_ssig_T = Tsubst Y YpreT old_ssig_T;
  1452 
  1453     val dead_pre_map' = Term.subst_atomic_types [(Y, old_ssig_T), (Z, ssig_T)] dead_pre_map;
  1454     val embL' = substT Y YpreT embL;
  1455     val x' = substT Y Ypre_old_ssig_T x;
  1456 
  1457     val goal =
  1458       mk_Trueprop_eq (eval_core $ (embL' $ x'), dead_pre_map' $ embL $ (old_eval_core $ x'));
  1459 
  1460     val old_ssig_induct' =
  1461       infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt x')] old_ssig_induct;
  1462   in
  1463     Variable.add_free_names ctxt goal []
  1464     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1465       mk_eval_core_embL_tac ctxt old_ssig_induct' dead_pre_map_comp0 dead_pre_map_comp
  1466         Sig_pointful_natural unsig_thm old_sig_map_comp old_sig_map_cong old_Lam_pointful_natural
  1467         Lam_def flat_embL old_eval_core_simps eval_core_simps embL_simps embL_pointful_natural))
  1468     |> Thm.close_derivation
  1469   end;
  1470 
  1471 fun derive_eval_embL ctxt Y fpT embL old_eval eval dead_pre_map_comp0 dtor_unfold_unique
  1472     embL_pointful_natural eval_core_embL old_eval_thm eval_thm =
  1473   let
  1474     val embL' = substT Y fpT embL;
  1475     val goal = mk_Trueprop_eq (HOLogic.mk_comp (eval, embL'), old_eval);
  1476   in
  1477     Variable.add_free_names ctxt goal []
  1478     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1479       mk_eval_embL_tac ctxt dead_pre_map_comp0 dtor_unfold_unique embL_pointful_natural
  1480         eval_core_embL old_eval_thm eval_thm))
  1481     |> Thm.close_derivation
  1482   end;
  1483 
  1484 fun derive_algLam_algLam ctxt Inx_const Y fpT Sig old_algLam algLam dead_pre_map_comp dtor_inject
  1485     unsig_thm sig_map_thm Lam_def eval_embL old_dtor_algLam dtor_algLam =
  1486   let
  1487     val Sig' = substT Y fpT Sig;
  1488     val (left_T, right_T) = dest_sumT (domain_type (fastype_of Sig'));
  1489     val inx' = Inx_const left_T right_T;
  1490 
  1491     val goal = mk_Trueprop_eq (Library.foldl1 HOLogic.mk_comp [algLam, Sig', inx'], old_algLam);
  1492   in
  1493     Variable.add_free_names ctxt goal []
  1494     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1495       mk_algLam_algLam_tac ctxt dead_pre_map_comp dtor_inject unsig_thm sig_map_thm Lam_def
  1496         eval_embL old_dtor_algLam dtor_algLam))
  1497     |> Thm.close_derivation
  1498   end;
  1499 
  1500 fun derive_eval_core_k_as_ssig ctxt Y preT k_T rho eval_core k_as_ssig x pre_map_comp
  1501     dead_pre_map_id sig_map_comp ssig_map_thms Lam_natural_pointful Lam_Inr flat_VLeaf
  1502     eval_core_simps =
  1503   let
  1504     val YpreT = HOLogic.mk_prodT (Y, preT);
  1505     val Ypre_k_T = Tsubst Y YpreT k_T;
  1506 
  1507     val k_as_ssig' = substT Y YpreT k_as_ssig;
  1508     val x' = substT Y Ypre_k_T x;
  1509 
  1510     val goal = mk_Trueprop_eq (eval_core $ (k_as_ssig' $ x'), rho $ x');
  1511   in
  1512     Variable.add_free_names ctxt goal []
  1513     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1514       mk_eval_core_k_as_ssig_tac ctxt pre_map_comp dead_pre_map_id sig_map_comp ssig_map_thms
  1515         Lam_natural_pointful Lam_Inr flat_VLeaf eval_core_simps))
  1516     |> Thm.close_derivation
  1517   end;
  1518 
  1519 fun derive_algLam_algrho ctxt Y fpT Sig algLam algrho algLam_def algrho_def =
  1520   let
  1521     val Sig' = substT Y fpT Sig;
  1522     val (left_T, right_T) = dest_sumT (domain_type (fastype_of Sig'));
  1523     val inr' = Inr_const left_T right_T;
  1524 
  1525     val goal = mk_Trueprop_eq (Library.foldl1 HOLogic.mk_comp [algLam, Sig', inr'], algrho);
  1526   in
  1527     Variable.add_free_names ctxt goal []
  1528     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1529       mk_algLam_algrho_tac ctxt algLam_def algrho_def))
  1530     |> Thm.close_derivation
  1531   end;
  1532 
  1533 fun derive_dtor_algrho ctxt Y Z preT fpT k_T ssig_T dead_pre_map dead_k_map dtor rho eval algrho x
  1534     eval_thm k_as_ssig_natural_pointful eval_core_k_as_ssig algrho_def =
  1535   let
  1536     val YpreT = HOLogic.mk_prodT (Y, preT);
  1537     val fppreT = Tsubst Y fpT YpreT;
  1538     val fp_k_T = Tsubst Y fpT k_T;
  1539     val fp_ssig_T = Tsubst Y fpT ssig_T;
  1540 
  1541     val id' = HOLogic.id_const fpT;
  1542     val convol' = mk_convol (id', dtor);
  1543     val dead_pre_map' = Term.subst_atomic_types [(Y, fp_ssig_T), (Z, fpT)] dead_pre_map;
  1544     val dead_k_map' = Term.subst_atomic_types [(Y, fpT), (Z, fppreT)] dead_k_map;
  1545     val rho' = substT Y fpT rho;
  1546     val x' = substT Y fp_k_T x;
  1547 
  1548     val goal = mk_Trueprop_eq (dtor $ (algrho $ x'),
  1549       dead_pre_map' $ eval $ (rho' $ (dead_k_map' $ convol' $ x')));
  1550   in
  1551     Variable.add_free_names ctxt goal []
  1552     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1553       mk_dtor_algrho_tac ctxt eval_thm k_as_ssig_natural_pointful eval_core_k_as_ssig algrho_def))
  1554     |> Thm.close_derivation
  1555   end;
  1556 
  1557 fun derive_algLam_step_or_merge ctxt Y fpT ctor proto_sctr algLam proto_sctr_def old_algLam_pointful
  1558     algLam_algLam =
  1559   let
  1560     val proto_sctr' = substT Y fpT proto_sctr;
  1561     val goal = mk_Trueprop_eq (HOLogic.mk_comp (algLam, proto_sctr'), ctor);
  1562 
  1563     val algLam_algLam_pointful = mk_pointful ctxt algLam_algLam;
  1564   in
  1565     Variable.add_free_names ctxt goal []
  1566     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1567       mk_algLam_step_tac ctxt proto_sctr_def old_algLam_pointful algLam_algLam_pointful))
  1568     |> Thm.close_derivation
  1569   end;
  1570 
  1571 fun derive_eval_sctr ctxt Y Z fpT ssig_T dead_pre_map ctor eval sctr proto_sctr_pointful_natural
  1572     eval_Oper algLam_thm sctr_def =
  1573   let
  1574     val fp_ssig_T = Tsubst Y fpT ssig_T;
  1575 
  1576     val dead_pre_map' = Term.subst_atomic_types [(Y, fp_ssig_T), (Z, fpT)] dead_pre_map;
  1577     val sctr' = substT Y fpT sctr;
  1578 
  1579     val goal = mk_Trueprop_eq (HOLogic.mk_comp (eval, sctr'),
  1580       HOLogic.mk_comp (ctor, dead_pre_map' $ eval));
  1581   in
  1582     Variable.add_free_names ctxt goal []
  1583     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1584       mk_eval_sctr_tac ctxt proto_sctr_pointful_natural eval_Oper algLam_thm sctr_def))
  1585     |> Thm.close_derivation
  1586   end;
  1587 
  1588 fun derive_corecUU_pointfree_unique ctxt Y Z preT fpT ssig_T dead_pre_map ctor dead_ssig_map eval
  1589     corecUU f g dead_pre_map_comp0 dead_pre_map_comp dtor_ctor dtor_inject ssig_map_comp
  1590     flat_pointful_natural eval_core_pointful_natural eval_thm eval_flat corecU_ctor corecU_unique
  1591     sctr_pointful_natural eval_sctr_pointful corecUU_def =
  1592   let
  1593     val ssig_preT = Tsubst Y ssig_T preT;
  1594     val ssig_pre_ssig_T = Tsubst Y ssig_preT ssig_T;
  1595     val fp_ssig_T = Tsubst Y fpT ssig_T;
  1596 
  1597     val dead_pre_map' = Term.subst_atomic_types [(Y, fp_ssig_T), (Z, fpT)] dead_pre_map;
  1598     val dead_pre_map'' = Term.subst_atomic_types [(Y, ssig_T), (Z, fp_ssig_T)] dead_pre_map;
  1599     val dead_ssig_map' = Term.subst_atomic_types [(Y, ssig_preT), (Z, fpT)] dead_ssig_map;
  1600     val dead_ssig_map'' = substT Z fpT dead_ssig_map;
  1601     val f' = substT Z ssig_pre_ssig_T f;
  1602     val g' = substT Z fpT g;
  1603     val corecUU_f = corecUU $ f';
  1604 
  1605     fun mk_eq fpf =
  1606       mk_Trueprop_eq (fpf, Library.foldl1 HOLogic.mk_comp [eval, dead_ssig_map' $
  1607           Library.foldl1 HOLogic.mk_comp [ctor, dead_pre_map' $ eval, dead_pre_map''
  1608             $ (dead_ssig_map'' $ fpf)],
  1609         f']);
  1610 
  1611     val corecUU_pointfree =
  1612       let
  1613         val goal = mk_eq corecUU_f;
  1614       in
  1615         Variable.add_free_names ctxt goal []
  1616         |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1617           mk_corecUU_pointfree_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor dtor_inject
  1618             ssig_map_comp flat_pointful_natural eval_core_pointful_natural eval_thm eval_flat
  1619             corecU_ctor sctr_pointful_natural eval_sctr_pointful corecUU_def))
  1620         |> Thm.close_derivation
  1621       end;
  1622 
  1623     val corecUU_unique =
  1624       let
  1625         val prem = mk_eq g';
  1626         val goal = mk_Trueprop_eq (g', corecUU_f);
  1627       in
  1628         fold (Variable.add_free_names ctxt) [prem, goal] []
  1629         |> (fn vars => Goal.prove_sorry ctxt vars [prem] goal
  1630               (fn {context = ctxt, prems = [prem]} =>
  1631                 mk_corecUU_unique_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor
  1632                   ssig_map_comp flat_pointful_natural eval_core_pointful_natural eval_thm eval_flat
  1633                   corecU_unique sctr_pointful_natural eval_sctr_pointful corecUU_def prem))
  1634         |> Thm.close_derivation
  1635       end;
  1636   in
  1637     (corecUU_pointfree, corecUU_unique)
  1638   end;
  1639 
  1640 fun define_flat_etc fp_b version live_AsBs Y Z preT fpT sig_T ssig_T Oper VLeaf CLeaf pre_rel
  1641     dead_pre_map dtor dtor_unfold dead_sig_map ssig_rel dead_ssig_map Lam Rs R pre_map_transfer
  1642     fp_k_T_rel_eqs sig_map_transfer ssig_map_transfer Lam_transfer dtor_transfer lthy =
  1643   let
  1644     val (flat_data as (flat, flat_def, _), lthy) = lthy
  1645       |> define_flat fp_b version Y Z fpT sig_T ssig_T Oper VLeaf CLeaf dead_sig_map;
  1646 
  1647     val (eval_core_data as (eval_core, eval_core_def, _), lthy) = lthy
  1648       |> define_eval_core fp_b version Y Z preT fpT sig_T ssig_T dtor Oper VLeaf CLeaf dead_pre_map
  1649         dead_sig_map dead_ssig_map flat Lam;
  1650 
  1651     val ((eval_data as (eval, _), cutSsig_data as (cutSsig, _)), lthy) = lthy
  1652       |> define_eval fp_b version Y Z preT fpT ssig_T dtor dtor_unfold dead_ssig_map eval_core
  1653       ||>> define_cutSsig fp_b version Y Z preT ssig_T dead_pre_map VLeaf dead_ssig_map flat
  1654         eval_core;
  1655 
  1656     val ((algLam_data, unfold_data), lthy) = lthy
  1657       |> define_algLam fp_b version Y Z fpT ssig_T Oper VLeaf dead_sig_map eval
  1658       ||>> define_corecU fp_b version Y Z preT ssig_T dtor_unfold VLeaf cutSsig;
  1659 
  1660     val flat_transfer = derive_transfer_by_transfer_prover lthy live_AsBs Rs R flat [flat_def] []
  1661       [sig_map_transfer];
  1662     val eval_core_transfer = derive_Lam_or_eval_core_transfer lthy live_AsBs Y Z preT ssig_T Rs R
  1663       pre_rel ssig_rel ssig_rel eval_core eval_core_def fp_k_T_rel_eqs
  1664       [pre_map_transfer, sig_map_transfer, ssig_map_transfer, flat_transfer, Lam_transfer,
  1665        dtor_transfer];
  1666   in
  1667     (((((((flat_data, flat_transfer), (eval_core_data, eval_core_transfer)), eval_data),
  1668       cutSsig_data), algLam_data), unfold_data), lthy)
  1669   end;
  1670 
  1671 fun derive_Sig_natural_etc ctxt live live_AsBs Y Z preT fpT k_or_fpT sig_T ssig_T pre_map
  1672     dead_pre_map ctor dtor Sig dead_sig_map Oper VLeaf CLeaf ssig_map dead_ssig_map Lam flat
  1673     eval_core eval cutSsig algLam corecU x fs f g ctor_dtor dtor_inject dtor_unfold_thm
  1674     dtor_unfold_unique sig_map_thm ssig_induct ssig_map_thms Oper_map_thm VLeaf_map_thm
  1675     CLeaf_map_thm Lam_transfer flat_simps flat_transfer eval_core_simps eval_core_transfer eval_def
  1676     cutSsig_def algLam_def corecU_def live_pre_bnf pre_bnf dead_pre_bnf fp_bnf sig_bnf ssig_bnf
  1677     dead_ssig_bnf =
  1678   let
  1679     val SOME prod_fp_sugar = fp_sugar_of ctxt @{type_name prod};
  1680     val prod_bnf = #fp_bnf prod_fp_sugar;
  1681 
  1682     val f' = substT Z fpT f;
  1683     val dead_ssig_map' = substT Z fpT dead_ssig_map;
  1684     val extdd = Term.lambda f' (HOLogic.mk_comp (eval, dead_ssig_map' $ f'));
  1685 
  1686     val live_pre_map_def = map_def_of_bnf live_pre_bnf;
  1687     val pre_map_comp = map_comp_of_bnf pre_bnf;
  1688     val dead_pre_map_id = map_id_of_bnf dead_pre_bnf;
  1689     val dead_pre_map_comp0 = map_comp0_of_bnf dead_pre_bnf;
  1690     val dead_pre_map_comp = map_comp_of_bnf dead_pre_bnf;
  1691     val dead_pre_map_cong = map_cong_of_bnf dead_pre_bnf;
  1692     val fp_map_id = map_id_of_bnf fp_bnf;
  1693     val sig_map_ident = map_ident_of_bnf sig_bnf;
  1694     val sig_map_comp0 = map_comp0_of_bnf sig_bnf;
  1695     val sig_map_comp = map_comp_of_bnf sig_bnf;
  1696     val sig_map_cong = map_cong_of_bnf sig_bnf;
  1697     val ssig_map_id = map_id_of_bnf ssig_bnf;
  1698     val ssig_map_comp = map_comp_of_bnf ssig_bnf;
  1699     val dead_ssig_map_comp0 = map_comp0_of_bnf dead_ssig_bnf;
  1700 
  1701     val k_preT_map_id0s =
  1702       map map_id0_of_bnf (map_filter (bnf_of ctxt) (fold add_type_namesT [preT, k_or_fpT] []));
  1703 
  1704     val Sig_natural = derive_natural_by_unfolding ctxt live_AsBs preT pre_map fs f Sig
  1705       ([sig_map_thm, live_pre_map_def, @{thm BNF_Composition.id_bnf_def}] @ k_preT_map_id0s);
  1706     val Oper_natural =
  1707       derive_natural_by_unfolding ctxt live_AsBs preT pre_map fs f Oper [Oper_map_thm];
  1708     val VLeaf_natural =
  1709       derive_natural_by_unfolding ctxt live_AsBs preT pre_map fs f VLeaf [VLeaf_map_thm];
  1710     val Lam_natural = derive_natural_from_transfer_with_pre_type ctxt live_AsBs Y Z preT ssig_T
  1711       pre_map ssig_map fs f Lam Lam_transfer [prod_bnf, pre_bnf, sig_bnf, ssig_bnf] [];
  1712     val flat_natural = derive_natural_from_transfer ctxt live_AsBs [] fs f flat flat_transfer
  1713       [ssig_bnf] [];
  1714     val eval_core_natural = derive_natural_from_transfer_with_pre_type ctxt live_AsBs Y Z preT
  1715       ssig_T pre_map ssig_map fs f eval_core eval_core_transfer [prod_bnf, pre_bnf, ssig_bnf] [];
  1716 
  1717     val Sig_pointful_natural = mk_pointful ctxt Sig_natural RS sym;
  1718     val Oper_natural_pointful = mk_pointful ctxt Oper_natural;
  1719     val Oper_pointful_natural = Oper_natural_pointful RS sym;
  1720     val flat_pointful_natural = mk_pointful ctxt flat_natural RS sym;
  1721     val Lam_natural_pointful = mk_pointful ctxt Lam_natural;
  1722     val Lam_pointful_natural = Lam_natural_pointful RS sym;
  1723     val eval_core_pointful_natural = mk_pointful ctxt eval_core_natural RS sym;
  1724     val cutSsig_def_pointful_natural = mk_pointful ctxt (cutSsig_def RS meta_eq_to_obj_eq) RS sym;
  1725 
  1726     val flat_VLeaf = derive_flat_VLeaf ctxt Y Z ssig_T x VLeaf dead_ssig_map flat ssig_induct
  1727       fp_map_id sig_map_cong sig_map_ident sig_map_comp ssig_map_thms flat_simps;
  1728     val flat_flat = derive_flat_flat ctxt Y Z ssig_T x dead_ssig_map flat ssig_induct fp_map_id
  1729       sig_map_cong sig_map_comp ssig_map_thms flat_simps;
  1730 
  1731     val eval_core_flat = derive_eval_core_flat ctxt Y Z preT ssig_T dead_pre_map dead_ssig_map flat
  1732       eval_core x ssig_induct dead_pre_map_id dead_pre_map_comp0 dead_pre_map_comp fp_map_id
  1733       sig_map_comp sig_map_cong ssig_map_thms ssig_map_comp flat_simps flat_pointful_natural
  1734       flat_flat Lam_pointful_natural eval_core_simps;
  1735 
  1736     val eval_thm = derive_eval_thm ctxt dtor_inject dtor_unfold_thm eval_def;
  1737     val eval_flat = derive_eval_flat ctxt Y Z fpT ssig_T dead_ssig_map flat eval x
  1738       dead_pre_map_comp0 dtor_unfold_unique ssig_map_id ssig_map_comp flat_pointful_natural
  1739       eval_core_pointful_natural eval_core_flat eval_thm;
  1740     val eval_Oper = derive_eval_Oper ctxt live Y Z fpT sig_T ssig_T dead_sig_map Oper eval algLam x
  1741       sig_map_ident sig_map_comp0 sig_map_comp Oper_natural_pointful VLeaf_natural flat_simps
  1742       eval_flat algLam_def;
  1743     val eval_VLeaf = derive_eval_V_or_CLeaf ctxt Y fpT VLeaf eval x dead_pre_map_id
  1744       dead_pre_map_comp fp_map_id dtor_unfold_unique VLeaf_map_thm eval_core_simps eval_thm;
  1745     val eval_CLeaf = derive_eval_V_or_CLeaf ctxt Y fpT CLeaf eval x dead_pre_map_id
  1746       dead_pre_map_comp fp_map_id dtor_unfold_unique CLeaf_map_thm eval_core_simps eval_thm;
  1747 
  1748     val extdd_mor = derive_extdd_mor ctxt Y Z preT fpT ssig_T dead_pre_map dtor extdd cutSsig f g
  1749       dead_pre_map_comp0 dead_pre_map_comp VLeaf_map_thm ssig_map_comp flat_pointful_natural
  1750       eval_core_pointful_natural eval_thm eval_flat eval_VLeaf cutSsig_def;
  1751     val mor_cutSsig_flat = derive_mor_cutSsig_flat ctxt Y Z preT fpT ssig_T dead_pre_map
  1752       dead_ssig_map dtor flat eval_core eval cutSsig f g dead_pre_map_comp0 dead_pre_map_comp
  1753       dead_pre_map_cong dtor_unfold_unique dead_ssig_map_comp0 ssig_map_comp flat_simps
  1754       flat_pointful_natural eval_core_pointful_natural flat_flat flat_VLeaf eval_core_flat
  1755       cutSsig_def cutSsig_def_pointful_natural eval_thm;
  1756     val extdd_o_VLeaf = derive_extdd_o_VLeaf ctxt Y Z preT fpT ssig_T dead_pre_map dtor VLeaf extdd
  1757       f g dead_pre_map_comp0 dead_pre_map_comp dtor_inject ssig_map_thms eval_core_simps eval_thm
  1758       eval_VLeaf;
  1759 
  1760     val (corecU_ctor, corecU_unique) = derive_corecU_ctor_unique ctxt Y Z preT fpT ssig_T
  1761       dead_pre_map ctor dtor VLeaf extdd corecU f g dead_pre_map_comp ctor_dtor dtor_unfold_thm
  1762       dtor_unfold_unique ssig_map_thms dead_ssig_map_comp0 flat_simps flat_VLeaf eval_core_simps
  1763       extdd_mor extdd_o_VLeaf cutSsig_def mor_cutSsig_flat corecU_def;
  1764 
  1765     val dtor_algLam = derive_dtor_algLam ctxt Y Z preT fpT sig_T ssig_T dead_pre_map dtor
  1766       dead_sig_map Lam eval algLam x pre_map_comp dead_pre_map_id dead_pre_map_comp0
  1767       dead_pre_map_comp sig_map_comp Oper_pointful_natural ssig_map_thms dead_ssig_map_comp0
  1768       Lam_pointful_natural eval_core_simps eval_thm eval_flat eval_VLeaf algLam_def;
  1769   in
  1770     (Sig_pointful_natural, flat_pointful_natural, Lam_natural_pointful, Lam_pointful_natural,
  1771      flat_VLeaf, eval_core_pointful_natural, eval_thm, eval_flat,
  1772      [eval_Oper, eval_VLeaf, eval_CLeaf], corecU_ctor, corecU_unique, dtor_algLam)
  1773   end;
  1774 
  1775 fun derive_embL_natural_etc ctxt Inx_const old_ssig_bnf ssig_bnf Y Z preT fpT old_ssig_T ssig_T
  1776     dead_pre_map Sig dead_old_ssig_map embL old_algLam algLam old_flat flat old_eval_core eval_core
  1777     old_eval eval x f old_ssig_induct dead_pre_map_comp0 dead_pre_map_comp fp_map_id dtor_inject
  1778     dtor_unfold_unique Sig_pointful_natural unsig_thm sig_map_thm old_sig_map_comp old_sig_map_cong
  1779     old_ssig_map_thms old_Lam_pointful_natural Lam_def old_flat_simps flat_simps embL_simps
  1780     embL_transfer old_eval_core_simps eval_core_simps old_eval_thm eval_thm old_dtor_algLam
  1781     dtor_algLam old_algLam_thm =
  1782   let
  1783     val embL_natural = derive_natural_from_transfer ctxt [(Y, Z)] [] [] f embL embL_transfer
  1784       [old_ssig_bnf, ssig_bnf] [];
  1785 
  1786     val embL_pointful_natural = mk_pointful ctxt embL_natural RS sym;
  1787     val old_algLam_pointful = mk_pointful ctxt old_algLam_thm;
  1788 
  1789     val flat_embL = derive_flat_embL ctxt Y Z old_ssig_T ssig_T dead_old_ssig_map embL old_flat flat
  1790       x old_ssig_induct fp_map_id Sig_pointful_natural old_sig_map_comp old_sig_map_cong
  1791       old_ssig_map_thms old_flat_simps flat_simps embL_simps;
  1792     val eval_core_embL = derive_eval_core_embL ctxt Y Z preT old_ssig_T ssig_T dead_pre_map embL
  1793       old_eval_core eval_core x old_ssig_induct dead_pre_map_comp0 dead_pre_map_comp
  1794       Sig_pointful_natural unsig_thm old_sig_map_comp old_sig_map_cong old_Lam_pointful_natural
  1795       Lam_def flat_embL embL_simps embL_pointful_natural old_eval_core_simps eval_core_simps;
  1796     val eval_embL = derive_eval_embL ctxt Y fpT embL old_eval eval dead_pre_map_comp0
  1797       dtor_unfold_unique embL_pointful_natural eval_core_embL old_eval_thm eval_thm;
  1798 
  1799     val algLam_algLam = derive_algLam_algLam ctxt Inx_const Y fpT Sig old_algLam algLam
  1800       dead_pre_map_comp dtor_inject unsig_thm sig_map_thm Lam_def eval_embL old_dtor_algLam
  1801       dtor_algLam;
  1802   in
  1803     (embL_pointful_natural, old_algLam_pointful, eval_embL, algLam_algLam)
  1804   end;
  1805 
  1806 fun define_corecUU_etc fp_b version live_AsBs Y Z preT fpT ssig_T pre_map dead_pre_map pre_rel
  1807     fp_rel ctor Oper ssig_map dead_ssig_map ssig_rel proto_sctr flat eval_core eval corecU fs f g Rs
  1808     R pre_map_transfer fp_k_T_rel_eqs dtor_unfold_transfer dtor_transfer ssig_map_transfer
  1809     proto_sctr_transfer proto_sctr_pointful_natural flat_transfer flat_pointful_natural
  1810     eval_core_transfer eval_core_pointful_natural eval_thm eval_flat eval_Oper algLam_thm
  1811     cutSsig_def corecU_def corecU_ctor corecU_unique pre_bnf dead_pre_bnf fp_res ssig_fp_sugar
  1812     lthy =
  1813   let
  1814     val ssig_bnf = #fp_bnf ssig_fp_sugar;
  1815 
  1816     val dead_pre_map_comp0 = map_comp0_of_bnf dead_pre_bnf;
  1817     val dead_pre_map_comp = map_comp_of_bnf dead_pre_bnf;
  1818     val [dtor_ctor] = #dtor_ctors fp_res;
  1819     val [dtor_inject] = #dtor_injects fp_res;
  1820     val ssig_map_comp = map_comp_of_bnf ssig_bnf;
  1821 
  1822     val sctr_rhs = HOLogic.mk_comp (Oper, substT Y ssig_T proto_sctr);
  1823     val ((sctr, sctr_def), lthy) = lthy
  1824       |> define_const true fp_b version sctrN sctr_rhs;
  1825 
  1826     val (corecUU_data as (corecUU, corecUU_def), lthy) = lthy
  1827       |> define_corecUU fp_b version Y Z preT ssig_T dead_pre_map dead_ssig_map flat eval_core sctr
  1828         corecU;
  1829 
  1830     val eval_sctr = derive_eval_sctr lthy Y Z fpT ssig_T dead_pre_map ctor eval sctr
  1831       proto_sctr_pointful_natural eval_Oper algLam_thm sctr_def;
  1832 
  1833     val sctr_transfer = derive_sctr_transfer lthy live_AsBs Y Z ssig_T Rs R pre_rel ssig_rel sctr
  1834       sctr_def fp_k_T_rel_eqs [proto_sctr_transfer];
  1835 
  1836     val sctr_natural = derive_natural_from_transfer_with_pre_type lthy live_AsBs Y Z preT ssig_T
  1837       pre_map ssig_map fs f sctr sctr_transfer [pre_bnf, ssig_bnf] [];
  1838 
  1839     val sctr_pointful_natural = mk_pointful lthy sctr_natural RS sym;
  1840     val eval_sctr_pointful = mk_pointful lthy eval_sctr RS sym;
  1841 
  1842     val (corecUU_pointfree, corecUU_unique) = derive_corecUU_pointfree_unique lthy Y Z preT fpT
  1843       ssig_T dead_pre_map ctor dead_ssig_map eval corecUU f g dead_pre_map_comp0 dead_pre_map_comp
  1844       dtor_ctor dtor_inject ssig_map_comp flat_pointful_natural eval_core_pointful_natural eval_thm
  1845       eval_flat corecU_ctor corecU_unique sctr_pointful_natural eval_sctr_pointful corecUU_def;
  1846 
  1847     val corecUU_thm = mk_pointful lthy corecUU_pointfree;
  1848 
  1849     val corecUU_transfer = derive_corecUU_transfer lthy live_AsBs Y Z Rs R preT ssig_T pre_rel
  1850       fp_rel ssig_rel corecUU cutSsig_def corecU_def corecUU_def fp_k_T_rel_eqs
  1851       [pre_map_transfer, dtor_unfold_transfer, dtor_transfer, ssig_map_transfer, flat_transfer,
  1852        eval_core_transfer, sctr_transfer, @{thm convol_transfer} (*FIXME: needed?*)];
  1853   in
  1854     ((corecUU_data, corecUU_thm, corecUU_unique, corecUU_transfer, eval_sctr, sctr_transfer,
  1855       sctr_pointful_natural), lthy)
  1856   end;
  1857 
  1858 fun mk_equivp T = Const (@{const_name equivp}, mk_predT [mk_pred2T T T]);
  1859 
  1860 fun derive_equivp_Retr ctxt fpT Retr R dead_pre_rel_refl_thm dead_pre_rel_flip_thm
  1861     dead_pre_rel_mono_thm dead_pre_rel_compp_thm =
  1862   let
  1863     val prem = HOLogic.mk_Trueprop (mk_equivp fpT $ R);
  1864     val goal = Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_equivp fpT $ (betapply (Retr, R))));
  1865   in
  1866     Variable.add_free_names ctxt goal []
  1867     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
  1868       mk_equivp_Retr_tac ctxt dead_pre_rel_refl_thm dead_pre_rel_flip_thm dead_pre_rel_mono_thm
  1869         dead_pre_rel_compp_thm))
  1870     |> Thm.close_derivation
  1871   end;
  1872 
  1873 fun derive_Retr_coinduct ctxt fpT Retr R dtor_rel_coinduct_thm rel_eq_thm =
  1874   let
  1875     val goal = HOLogic.mk_Trueprop (list_all_free [R]
  1876       (HOLogic.mk_imp (mk_leq R (Retr $ R), mk_leq R (HOLogic.eq_const fpT))));
  1877   in
  1878     Goal.prove_sorry ctxt [] [] goal (fn {context = ctxt, prems = _} =>
  1879       mk_Retr_coinduct_tac ctxt dtor_rel_coinduct_thm rel_eq_thm)
  1880     |> Thm.close_derivation
  1881   end;
  1882 
  1883 fun derive_Retr fp_sugar fpT dead_pre_bnf ctor dtor names_lthy lthy =
  1884   let
  1885     val (R, _) = names_lthy
  1886       |> yield_singleton (mk_Frees "R") (mk_pred2T fpT fpT);
  1887     val pre_fpT = pre_type_of_ctor fpT ctor;
  1888     val fp_pre_rel = mk_rel1 lthy fpT fpT pre_fpT dead_pre_bnf;
  1889     val Retr = Abs ("R", fastype_of R, Abs ("a", fpT,
  1890       Abs ("b", fpT, list_comb (fp_pre_rel, [Bound 2, dtor $ Bound 1, dtor $ Bound 0]))));
  1891     val equivp_Retr = derive_equivp_Retr lthy fpT Retr R (rel_refl_of_bnf dead_pre_bnf)
  1892       (rel_flip_of_bnf dead_pre_bnf) (rel_mono_of_bnf dead_pre_bnf) (rel_OO_of_bnf dead_pre_bnf);
  1893 
  1894     val Retr_coinduct = derive_Retr_coinduct lthy fpT Retr R
  1895       (fp_sugar |> #fp_res |> #xtor_rel_co_induct) (fp_sugar |> #fp_bnf |> rel_eq_of_bnf);
  1896   in
  1897     (Retr, equivp_Retr, Retr_coinduct)
  1898   end;
  1899 
  1900 fun mk_gen_cong fpT eval_domT =
  1901   let val fp_relT = mk_pred2T fpT fpT in
  1902     Const (@{const_name "cong.gen_cong"},
  1903       [mk_predT [fp_relT, eval_domT, eval_domT], eval_domT --> fpT, fp_relT] ---> fp_relT)
  1904   end;
  1905 
  1906 fun mk_cong_locale rel eval Retr =
  1907   Const (@{const_name cong}, mk_predT (map fastype_of [rel, eval, Retr]));
  1908 
  1909 fun derive_cong_locale ctxt rel eval Retr0 tac =
  1910   let
  1911     val Retr = enforce_type ctxt domain_type (domain_type (fastype_of rel)) Retr0;
  1912     val goal = HOLogic.mk_Trueprop (list_comb (mk_cong_locale rel eval Retr, [rel, eval, Retr]));
  1913   in
  1914     Variable.add_free_names ctxt goal []
  1915     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} => tac ctxt))
  1916     |> Thm.close_derivation
  1917   end;
  1918 
  1919 fun derive_cong_general fp_b version fpT dead_ssig_bnf dead_pre_bnf eval Retr equivp_Retr
  1920     Retr_coinduct eval_thm eval_core_transfer lthy =
  1921   let
  1922     val eval_domT = domain_type (fastype_of eval);
  1923 
  1924     fun cong_locale_tac ctxt =
  1925       mk_cong_locale_tac ctxt (rel_mono_of_bnf dead_pre_bnf) (rel_map_of_bnf dead_pre_bnf)
  1926         equivp_Retr (rel_mono_of_bnf dead_ssig_bnf) (rel_map_of_bnf dead_ssig_bnf) eval_thm
  1927         eval_core_transfer;
  1928 
  1929     val rel = mk_rel1 lthy fpT fpT eval_domT dead_ssig_bnf;
  1930     val cong_rhs = list_comb (mk_gen_cong fpT eval_domT, [rel, eval]);
  1931     val ((_, cong_def), lthy) = lthy
  1932       |> define_const false fp_b version congN cong_rhs;
  1933 
  1934     val cong_locale = derive_cong_locale lthy rel eval Retr cong_locale_tac;
  1935 
  1936     val fold_cong_def = fold_thms lthy [cong_def];
  1937 
  1938     fun instance_of_gen thm = fold_cong_def (thm OF [cong_locale]);
  1939 
  1940     val cong_base = instance_of_gen @{thm cong.imp_gen_cong};
  1941     val cong_refl = instance_of_gen @{thm cong.gen_cong_reflp};
  1942     val cong_sym = instance_of_gen @{thm cong.gen_cong_symp};
  1943     val cong_trans = instance_of_gen @{thm cong.gen_cong_transp};
  1944 
  1945     fun mk_cong_rho thm = thm RS instance_of_gen @{thm cong.gen_cong_rho};
  1946 
  1947     val dtor_coinduct = @{thm predicate2I_obj} RS
  1948       (Retr_coinduct RS instance_of_gen @{thm cong.coinduction} RS @{thm predicate2D_obj});
  1949   in
  1950     (cong_def, cong_locale, cong_base, cong_refl, cong_sym, cong_trans, dtor_coinduct, mk_cong_rho,
  1951      lthy)
  1952   end;
  1953 
  1954 fun derive_cong_base fp_b version fpT dead_ssig_bnf ssig_fp_bnf_sugar dead_pre_bnf eval eval_thm
  1955     eval_core_transfer eval_VLeaf eval_sctr sctr_transfer Retr equivp_Retr Retr_coinduct lthy =
  1956   let
  1957     val (cong_def, cong_locale, cong_base, cong_refl, cong_sym, cong_trans, dtor_coinduct,
  1958          mk_cong_rho, lthy) =
  1959       derive_cong_general fp_b version fpT dead_ssig_bnf dead_pre_bnf eval Retr equivp_Retr
  1960         Retr_coinduct eval_thm eval_core_transfer lthy;
  1961 
  1962     val dead_pre_map_id0 = map_id0_of_bnf dead_pre_bnf;
  1963     val dead_pre_map_comp0 = map_comp0_of_bnf dead_pre_bnf;
  1964     val dead_pre_map_cong0 = map_cong0_of_bnf dead_pre_bnf;
  1965     val dead_pre_map_cong0' =
  1966       @{thm box_equals[OF _ o_apply[symmetric] id_apply[symmetric]]} RS dead_pre_map_cong0 RS ext;
  1967     val dead_pre_rel_map = rel_map_of_bnf dead_pre_bnf;
  1968 
  1969     val ctor_alt_thm = eval_VLeaf RS (@{thm eq_comp_compI} OF [eval_sctr,
  1970       trans OF [dead_pre_map_comp0 RS sym, trans OF [dead_pre_map_cong0', dead_pre_map_id0]]]);
  1971 
  1972     val cong_ctor_intro = mk_cong_rho ctor_alt_thm
  1973       |> unfold_thms lthy [o_apply]
  1974       |> (fn thm => sctr_transfer RS rel_funD RS thm)
  1975       |> unfold_thms lthy (id_apply :: dead_pre_rel_map @ #rel_injects ssig_fp_bnf_sugar);
  1976   in
  1977     ({cong_def = cong_def, cong_locale = cong_locale, cong_base = cong_base, cong_refl = cong_refl,
  1978       cong_sym = cong_sym, cong_trans = cong_trans, dtor_coinduct = dtor_coinduct,
  1979       cong_alg_intros = [cong_ctor_intro]}, lthy)
  1980   end;
  1981 
  1982 fun update_cong_alg_intros ctxt cong_def cong_locale old_cong_def old_cong_locale emb =
  1983   let
  1984     fun instance_of_gen thm = fold_thms ctxt [cong_def] (thm OF [cong_locale]);
  1985     fun instance_of_old_gen thm = fold_thms ctxt [old_cong_def] (thm OF [old_cong_locale]);
  1986 
  1987     val emb_idem = @{thm ord_le_eq_trans} OF [emb, instance_of_gen @{thm cong.gen_cong_idem}];
  1988     fun mk_rel_mono bnf = instance_of_old_gen @{thm cong.leq_gen_cong} RS rel_mono_of_bnf bnf RS
  1989       @{thm predicate2D};
  1990     fun mk_intro bnf thm = mk_rel_mono bnf RS (@{thm predicate2D} OF [emb_idem, thm]);
  1991   in
  1992     map2 mk_intro
  1993   end
  1994 
  1995 fun derive_cong_step fp_b version fpT dead_ssig_bnf dead_pre_bnf eval eval_thm eval_core_transfer
  1996     old_dtor_coinduct_info algrho_def k_as_ssig_transfer Retr equivp_Retr Retr_coinduct
  1997     eval_embL embL_transfer old_all_dead_k_bnfs lthy =
  1998   let
  1999     val old_cong_def = #cong_def old_dtor_coinduct_info;
  2000     val old_cong_locale = #cong_locale old_dtor_coinduct_info;
  2001     val old_cong_alg_intros = #cong_alg_intros old_dtor_coinduct_info;
  2002 
  2003     val (cong_def, cong_locale, cong_base, cong_refl, cong_sym, cong_trans, dtor_coinduct,
  2004          mk_cong_rho, lthy) =
  2005       derive_cong_general fp_b version fpT dead_ssig_bnf dead_pre_bnf eval Retr equivp_Retr
  2006         Retr_coinduct eval_thm eval_core_transfer lthy;
  2007 
  2008     val cong_alg_intro =
  2009       k_as_ssig_transfer RS rel_funD RS mk_cong_rho (algrho_def RS meta_eq_to_obj_eq);
  2010 
  2011     val gen_cong_emb =
  2012       (@{thm gen_cong_emb} OF [old_cong_locale, cong_locale, eval_embL, embL_transfer])
  2013       |> fold_thms lthy [old_cong_def, cong_def];
  2014 
  2015     val cong_alg_intros = update_cong_alg_intros lthy cong_def cong_locale old_cong_def
  2016       old_cong_locale gen_cong_emb old_all_dead_k_bnfs old_cong_alg_intros;
  2017   in
  2018     ({cong_def = cong_def, cong_locale = cong_locale, cong_base = cong_base, cong_refl = cong_refl,
  2019       cong_sym = cong_sym, cong_trans = cong_trans, dtor_coinduct = dtor_coinduct,
  2020       cong_alg_intros = cong_alg_intro :: cong_alg_intros}, lthy)
  2021   end;
  2022 
  2023 fun derive_cong_merge fp_b version fpT old1_friend_names old2_friend_names dead_ssig_bnf
  2024     dead_pre_bnf eval eval_thm eval_core_transfer old1_dtor_coinduct_info old2_dtor_coinduct_info
  2025     Retr equivp_Retr Retr_coinduct eval_embLL embLL_transfer eval_embLR embLR_transfer
  2026     old1_all_dead_k_bnfs old2_all_dead_k_bnfs lthy =
  2027   let
  2028     val old1_cong_def = #cong_def old1_dtor_coinduct_info;
  2029     val old1_cong_locale = #cong_locale old1_dtor_coinduct_info;
  2030     val old1_cong_alg_intros = #cong_alg_intros old1_dtor_coinduct_info;
  2031     val old2_cong_def = #cong_def old2_dtor_coinduct_info;
  2032     val old2_cong_locale = #cong_locale old2_dtor_coinduct_info;
  2033     val old2_cong_alg_intros = #cong_alg_intros old2_dtor_coinduct_info;
  2034 
  2035     val (cong_def, cong_locale, cong_base, cong_refl, cong_sym, cong_trans, dtor_coinduct, _,
  2036          lthy) =
  2037       derive_cong_general fp_b version fpT dead_ssig_bnf dead_pre_bnf eval Retr equivp_Retr
  2038         Retr_coinduct eval_thm eval_core_transfer lthy;
  2039 
  2040     val emb1 = (@{thm gen_cong_emb} OF [old1_cong_locale, cong_locale, eval_embLL, embLL_transfer])
  2041       |> fold_thms lthy [old1_cong_def, cong_def];
  2042     val emb2 = (@{thm gen_cong_emb} OF [old2_cong_locale, cong_locale, eval_embLR, embLR_transfer])
  2043       |> fold_thms lthy [old2_cong_def, cong_def];
  2044 
  2045     val cong_alg_intros1 = update_cong_alg_intros lthy cong_def cong_locale old1_cong_def
  2046       old1_cong_locale emb1 old1_all_dead_k_bnfs old1_cong_alg_intros;
  2047     val cong_alg_intros2 = update_cong_alg_intros lthy cong_def cong_locale old2_cong_def
  2048       old2_cong_locale emb2 old2_all_dead_k_bnfs old2_cong_alg_intros;
  2049 
  2050     val (cong_algrho_intros1, cong_ctor_intro1) = split_last cong_alg_intros1;
  2051     val (cong_algrho_intros2, _) = split_last cong_alg_intros2;
  2052     val (old1_all_rho_k_bnfs, old1_Sig_bnf) = split_last old1_all_dead_k_bnfs;
  2053     val (old2_all_rho_k_bnfs, _) = split_last old2_all_dead_k_bnfs;
  2054 
  2055     val (friend_names, (cong_algrho_intros, all_rho_k_bnfs)) =
  2056       merge_lists (op = o apply2 fst)
  2057         (old1_friend_names ~~ (cong_algrho_intros1 ~~ old1_all_rho_k_bnfs))
  2058         (old2_friend_names ~~ (cong_algrho_intros2 ~~ old2_all_rho_k_bnfs))
  2059       |> split_list ||> split_list;
  2060   in
  2061     (({cong_def = cong_def, cong_locale = cong_locale, cong_base = cong_base, cong_refl = cong_refl,
  2062        cong_sym = cong_sym, cong_trans = cong_trans, dtor_coinduct = dtor_coinduct,
  2063        cong_alg_intros = cong_algrho_intros @ [cong_ctor_intro1]}, all_rho_k_bnfs @ [old1_Sig_bnf],
  2064        friend_names), lthy)
  2065   end;
  2066 
  2067 fun derive_corecUU_base fpT_name lthy =
  2068   let
  2069     val fp_sugar as {T = Type (_, fpT_args0), pre_bnf, fp_bnf, fp_res, ...} =
  2070       checked_fp_sugar_of lthy fpT_name;
  2071     val fpT_Ss = map Type.sort_of_atyp fpT_args0;
  2072     val fp_alives = liveness_of_fp_bnf (length fpT_args0) fp_bnf;
  2073 
  2074     val (((Es, Fs0), [Y, Z]), names_lthy) = lthy
  2075       |> mk_TFrees' fpT_Ss
  2076       ||>> mk_TFrees' fpT_Ss
  2077       ||>> mk_TFrees 2;
  2078     val Fs = @{map 3} (fn alive => fn E => fn F => if alive then F else E) fp_alives Es Fs0;
  2079 
  2080     val As = Es @ [Y];
  2081     val Bs = Es @ [Z];
  2082 
  2083     val live_EsFs = filter (op <>) (Es ~~ Fs);
  2084     val live_AsBs = live_EsFs @ [(Y, Z)];
  2085     val fTs = map (op -->) live_EsFs;
  2086     val RTs = map (uncurry mk_pred2T) live_EsFs;
  2087     val live = length live_EsFs;
  2088 
  2089     val ((((((x, fs), f), g), Rs), R), names_lthy) = names_lthy
  2090       |> yield_singleton (mk_Frees "x") Y
  2091       ||>> mk_Frees "f" fTs
  2092       ||>> yield_singleton (mk_Frees "f") (Y --> Z)
  2093       ||>> yield_singleton (mk_Frees "g") (Y --> Z)
  2094       ||>> mk_Frees "R" RTs
  2095       ||>> yield_singleton (mk_Frees "R") (mk_pred2T Y Z);
  2096 
  2097     val ctor = mk_ctor Es (the_single (#ctors fp_res));
  2098     val dtor = mk_dtor Es (the_single (#dtors fp_res));
  2099 
  2100     val fpT = Type (fpT_name, Es);
  2101     val preT = pre_type_of_ctor Y ctor;
  2102 
  2103     val ((fp_b, version), lthy) = lthy |> get_name_next_version_of fpT_name;
  2104 
  2105     val ((sig_fp_sugar, ssig_fp_sugar), lthy) = lthy
  2106       |> define_sig_type fp_b version fp_alives Es Y preT
  2107       ||>> define_ssig_type fp_b version fp_alives Es Y fpT;
  2108 
  2109     val sig_bnf = #fp_bnf sig_fp_sugar;
  2110     val ssig_bnf = #fp_bnf ssig_fp_sugar;
  2111 
  2112     val (((dead_pre_bnf, dead_sig_bnf), dead_ssig_bnf), lthy) = lthy
  2113       |> bnf_kill_all_but 1 pre_bnf
  2114       ||>> bnf_kill_all_but 1 sig_bnf
  2115       ||>> bnf_kill_all_but 1 ssig_bnf;
  2116 
  2117     val sig_fp_ctr_sugar = #fp_ctr_sugar sig_fp_sugar;
  2118     val ssig_fp_ctr_sugar = #fp_ctr_sugar ssig_fp_sugar;
  2119 
  2120     val sig_fp_bnf_sugar = #fp_bnf_sugar sig_fp_sugar;
  2121     val ssig_fp_bnf_sugar = #fp_bnf_sugar ssig_fp_sugar;
  2122     val ssig_fp_induct_sugar = #fp_co_induct_sugar ssig_fp_sugar;
  2123 
  2124     val sig_ctr_sugar = #ctr_sugar sig_fp_ctr_sugar;
  2125     val ssig_ctr_sugar = #ctr_sugar ssig_fp_ctr_sugar;
  2126 
  2127     val sig_T_name = fst (dest_Type (#T sig_fp_sugar));
  2128     val ssig_T_name = fst (dest_Type (#T ssig_fp_sugar));
  2129 
  2130     val sig_T = Type (sig_T_name, As);
  2131     val ssig_T = Type (ssig_T_name, As);
  2132 
  2133     val pre_map = mk_mapN lthy live_AsBs preT pre_bnf;
  2134     val pre_rel = mk_relN lthy live_AsBs preT pre_bnf;
  2135     val dead_pre_map = mk_map1 lthy Y Z preT dead_pre_bnf;
  2136     val fp_rel = mk_relN lthy live_EsFs fpT fp_bnf;
  2137     val dtor_unfold = mk_co_rec (Proof_Context.theory_of lthy) Greatest_FP [Z] fpT
  2138       (the_single (#xtor_un_folds fp_res));
  2139     val Sig = mk_ctr As (the_single (#ctrs sig_ctr_sugar));
  2140     val unsig = mk_disc_or_sel As (the_single (the_single (#selss sig_ctr_sugar)));
  2141     val sig_rel = mk_relN lthy live_AsBs sig_T sig_bnf;
  2142     val dead_sig_map = mk_map 1 As Bs (map_of_bnf dead_sig_bnf);
  2143     val [Oper, VLeaf, CLeaf] = map (mk_ctr As) (#ctrs ssig_ctr_sugar);
  2144     val ssig_map = mk_mapN lthy live_AsBs ssig_T ssig_bnf;
  2145     val ssig_rel = mk_relN lthy live_AsBs ssig_T ssig_bnf;
  2146     val dead_ssig_map = mk_map 1 As Bs (map_of_bnf dead_ssig_bnf);
  2147     val dead_ssig_rel = mk_rel 1 As Bs (rel_of_bnf dead_ssig_bnf);
  2148 
  2149     val ((Lam, Lam_def), lthy) = lthy
  2150       |> define_Lam_base fp_b version Y Z preT ssig_T dead_pre_map Sig unsig dead_sig_map Oper
  2151         VLeaf;
  2152 
  2153     val proto_sctr = Sig;
  2154 
  2155     val pre_map_transfer = map_transfer_of_bnf pre_bnf;
  2156     val pre_rel_def = rel_def_of_bnf pre_bnf;
  2157     val dead_pre_map_id = map_id_of_bnf dead_pre_bnf;
  2158     val dead_pre_map_comp = map_comp_of_bnf dead_pre_bnf;
  2159     val fp_rel_eq = rel_eq_of_bnf fp_bnf;
  2160     val [ctor_dtor] = #ctor_dtors fp_res;
  2161     val [dtor_ctor] = #dtor_ctors fp_res;
  2162     val [dtor_inject] = #dtor_injects fp_res;
  2163     val [dtor_unfold_thm] = #xtor_un_fold_thms fp_res;
  2164     val [dtor_unfold_unique] = #xtor_un_fold_uniques fp_res;
  2165     val [dtor_unfold_transfer] = #xtor_un_fold_transfers fp_res;
  2166     val [dtor_rel_thm] = #xtor_rels fp_res;
  2167     val unsig_thm = the_single (the_single (#sel_thmss sig_ctr_sugar));
  2168     val [sig_map_thm] = #map_thms sig_fp_bnf_sugar;
  2169     val [Oper_map_thm, VLeaf_map_thm, CLeaf_map_thm] = #map_thms ssig_fp_bnf_sugar;
  2170     val sig_map_transfer = map_transfer_of_bnf sig_bnf;
  2171     val ssig_map_thms = #map_thms ssig_fp_bnf_sugar;
  2172     val ssig_map_transfer = map_transfer_of_bnf ssig_bnf;
  2173     val ssig_induct = the_single (#co_inducts ssig_fp_induct_sugar);
  2174 
  2175     val dtor_transfer = derive_dtor_transfer lthy live_EsFs Y Z pre_rel fp_rel Rs dtor dtor_rel_thm;
  2176     val preT_rel_eqs = map rel_eq_of_bnf (map_filter (bnf_of lthy) (add_type_namesT preT []));
  2177 
  2178     val Sig_transfer = derive_sig_transfer I lthy live_AsBs pre_rel sig_rel Rs R Sig pre_rel_def
  2179       preT_rel_eqs (the_single (#ctr_transfers sig_fp_ctr_sugar));
  2180     val proto_sctr_transfer = Sig_transfer;
  2181     val unsig_transfer = derive_sig_transfer swap lthy live_AsBs pre_rel sig_rel Rs R unsig
  2182       pre_rel_def preT_rel_eqs (the_single (#sel_transfers sig_fp_ctr_sugar));
  2183     val Lam_transfer = derive_Lam_or_eval_core_transfer lthy live_AsBs Y Z preT ssig_T Rs R pre_rel
  2184       sig_rel ssig_rel Lam Lam_def []
  2185       [pre_map_transfer, sig_map_transfer, Sig_transfer, unsig_transfer];
  2186 
  2187     val ((((((((flat, _, flat_simps), flat_transfer),
  2188             ((eval_core, _, eval_core_simps), eval_core_transfer)), (eval, eval_def)),
  2189           (cutSsig, cutSsig_def)), (algLam, algLam_def)), (corecU, corecU_def)), lthy) = lthy
  2190       |> define_flat_etc fp_b version live_AsBs Y Z preT fpT sig_T ssig_T Oper VLeaf CLeaf pre_rel
  2191         dead_pre_map dtor dtor_unfold dead_sig_map ssig_rel dead_ssig_map Lam Rs R pre_map_transfer
  2192         [fp_rel_eq] sig_map_transfer ssig_map_transfer Lam_transfer dtor_transfer;
  2193 
  2194     val (Sig_pointful_natural, flat_pointful_natural, _, Lam_pointful_natural, _,
  2195          eval_core_pointful_natural, eval_thm, eval_flat, eval_simps as [eval_Oper, eval_VLeaf, _],
  2196          corecU_ctor, corecU_unique, dtor_algLam) =
  2197       derive_Sig_natural_etc lthy live live_AsBs Y Z preT fpT fpT sig_T ssig_T pre_map dead_pre_map
  2198         ctor dtor Sig dead_sig_map Oper VLeaf CLeaf ssig_map dead_ssig_map Lam flat eval_core eval
  2199         cutSsig algLam corecU x fs f g ctor_dtor dtor_inject dtor_unfold_thm dtor_unfold_unique
  2200         sig_map_thm ssig_induct ssig_map_thms Oper_map_thm VLeaf_map_thm CLeaf_map_thm Lam_transfer
  2201         flat_simps flat_transfer eval_core_simps eval_core_transfer eval_def cutSsig_def algLam_def
  2202         corecU_def pre_bnf pre_bnf dead_pre_bnf fp_bnf sig_bnf ssig_bnf dead_ssig_bnf;
  2203 
  2204     val proto_sctr_pointful_natural = Sig_pointful_natural;
  2205 
  2206     val algLam_thm = derive_algLam_base lthy Y Z preT fpT dead_pre_map ctor dtor algLam proto_sctr
  2207       dead_pre_map_id dead_pre_map_comp ctor_dtor dtor_ctor dtor_unfold_unique unsig_thm
  2208       Sig_pointful_natural ssig_map_thms Lam_def flat_simps eval_core_simps eval_thm algLam_def;
  2209 
  2210     val (((corecUU, _), corecUU_thm, corecUU_unique, corecUU_transfer, eval_sctr, sctr_transfer,
  2211           sctr_pointful_natural), lthy) = lthy
  2212       |> define_corecUU_etc fp_b version live_AsBs Y Z preT fpT ssig_T pre_map dead_pre_map pre_rel
  2213         fp_rel ctor Oper ssig_map dead_ssig_map ssig_rel proto_sctr flat eval_core eval corecU fs f
  2214         g Rs R pre_map_transfer [] dtor_unfold_transfer dtor_transfer ssig_map_transfer
  2215         proto_sctr_transfer proto_sctr_pointful_natural flat_transfer flat_pointful_natural
  2216         eval_core_transfer eval_core_pointful_natural eval_thm eval_flat eval_Oper algLam_thm
  2217         cutSsig_def corecU_def corecU_ctor corecU_unique pre_bnf dead_pre_bnf fp_res ssig_fp_sugar;
  2218 
  2219     val (Retr, equivp_Retr, Retr_coinduct) = lthy
  2220       |> derive_Retr fp_sugar fpT dead_pre_bnf ctor dtor names_lthy;
  2221 
  2222     val (dtor_coinduct_info, lthy) = lthy
  2223       |> derive_cong_base fp_b version fpT dead_ssig_bnf ssig_fp_bnf_sugar dead_pre_bnf eval
  2224       eval_thm eval_core_transfer eval_VLeaf eval_sctr sctr_transfer Retr equivp_Retr Retr_coinduct;
  2225 
  2226     val buffer =
  2227       {Oper = Oper, VLeaf = VLeaf, CLeaf = CLeaf, ctr_wrapper = Sig, friends = Symtab.empty};
  2228 
  2229     val notes =
  2230       [(corecUU_transferN, [corecUU_transfer])] @
  2231       (if Config.get lthy bnf_internals then
  2232          [(algLamN, [algLam_thm]),
  2233           (cong_alg_introsN, #cong_alg_intros dtor_coinduct_info),
  2234           (cong_localeN, [#cong_locale dtor_coinduct_info]),
  2235           (corecU_ctorN, [corecU_ctor]),
  2236           (corecU_uniqueN, [corecU_unique]),
  2237           (corecUUN, [corecUU_thm]),
  2238           (corecUU_uniqueN, [corecUU_unique]),
  2239           (dtor_algLamN, [dtor_algLam]),
  2240           (dtor_coinductN, [#dtor_coinduct dtor_coinduct_info]),
  2241           (dtor_transferN, [dtor_transfer]),
  2242           (equivp_RetrN, [equivp_Retr]),
  2243           (evalN, [eval_thm]),
  2244           (eval_core_pointful_naturalN, [eval_core_pointful_natural]),
  2245           (eval_core_transferN, [eval_core_transfer]),
  2246           (eval_flatN, [eval_flat]),
  2247           (eval_simpsN, eval_simps),
  2248           (flat_pointful_naturalN, [flat_pointful_natural]),
  2249           (flat_transferN, [flat_transfer]),
  2250           (Lam_pointful_naturalN, [Lam_pointful_natural]),
  2251           (Lam_transferN, [Lam_transfer]),
  2252           (proto_sctr_pointful_naturalN, [proto_sctr_pointful_natural]),
  2253           (proto_sctr_transferN, [proto_sctr_transfer]),
  2254           (Retr_coinductN, [Retr_coinduct]),
  2255           (sctr_pointful_naturalN, [sctr_pointful_natural]),
  2256           (sctr_transferN, [sctr_transfer]),
  2257           (Sig_pointful_naturalN, [Sig_pointful_natural])]
  2258         else
  2259           [])
  2260       |> map (fn (thmN, thms) =>
  2261         ((mk_version_fp_binding true lthy version fp_b thmN, []), [(thms, [])]));
  2262   in
  2263     ({fp_b = fp_b, version = version, fpT = fpT, Y = Y, Z = Z, friend_names = [],
  2264       sig_fp_sugars = [sig_fp_sugar], ssig_fp_sugar = ssig_fp_sugar, Lam = Lam,
  2265       proto_sctr = proto_sctr, flat = flat, eval_core = eval_core, eval = eval, algLam = algLam,
  2266       corecUU = corecUU, dtor_transfer = dtor_transfer, Lam_transfer = Lam_transfer,
  2267       Lam_pointful_natural = Lam_pointful_natural, proto_sctr_transfer = proto_sctr_transfer,
  2268       flat_simps = flat_simps, eval_core_simps = eval_core_simps, eval_thm = eval_thm,
  2269       eval_simps = eval_simps, all_algLam_algs = [algLam_thm], algLam_thm = algLam_thm,
  2270       dtor_algLam = dtor_algLam, corecUU_thm = corecUU_thm, corecUU_unique = corecUU_unique,
  2271       corecUU_transfer = corecUU_transfer, buffer = buffer, all_dead_k_bnfs = [dead_pre_bnf],
  2272       Retr = Retr, equivp_Retr = equivp_Retr, Retr_coinduct = Retr_coinduct,
  2273       dtor_coinduct_info = dtor_coinduct_info}
  2274      |> morph_corec_info (Local_Theory.target_morphism lthy),
  2275      lthy |> Local_Theory.notes notes |> snd)
  2276   end;
  2277 
  2278 fun derive_corecUU_step (fpT as Type (fpT_name, res_Ds))
  2279     ({friend_names = old_friend_names, sig_fp_sugars = old_sig_fp_sugars as old_sig_fp_sugar :: _,
  2280       ssig_fp_sugar = old_ssig_fp_sugar, Lam = old_Lam0, proto_sctr = old_proto_sctr0,
  2281       flat = old_flat0, eval_core = old_eval_core0, eval = old_eval0, algLam = old_algLam0,
  2282       dtor_transfer, Lam_transfer = old_Lam_transfer,
  2283       Lam_pointful_natural = old_Lam_pointful_natural,
  2284       proto_sctr_transfer = old_proto_sctr_transfer, flat_simps = old_flat_simps,
  2285       eval_core_simps = old_eval_core_simps, eval_thm = old_eval_thm,
  2286       all_algLam_algs = old_all_algLam_algs, algLam_thm = old_algLam_thm,
  2287       dtor_algLam = old_dtor_algLam, buffer = old_buffer, all_dead_k_bnfs = old_all_dead_k_bnfs,
  2288       Retr = old_Retr0, equivp_Retr, Retr_coinduct, dtor_coinduct_info = old_dtor_coinduct_info,
  2289       ...} : corec_info)
  2290     friend_name friend_T fp_b version Y Z k_T dead_k_bnf sig_fp_sugar ssig_fp_sugar rho rho_transfer
  2291     lthy =
  2292   let
  2293     val {pre_bnf = live_pre_bnf, fp_bnf = live_fp_bnf, fp_res, ...} =
  2294       checked_fp_sugar_of lthy fpT_name;
  2295 
  2296     val names_lthy = lthy
  2297       |> fold Variable.declare_typ [Y, Z];
  2298 
  2299     (* FIXME *)
  2300     val live_EsFs = [];
  2301     val live_AsBs = live_EsFs @ [(Y, Z)];
  2302     val live = length live_EsFs;
  2303 
  2304     val ((((x, f), g), R), _) = names_lthy
  2305       |> yield_singleton (mk_Frees "x") Y
  2306       ||>> yield_singleton (mk_Frees "f") (Y --> Z)
  2307       ||>> yield_singleton (mk_Frees "g") (Y --> Z)
  2308       ||>> yield_singleton (mk_Frees "R") (mk_pred2T Y Z);
  2309 
  2310     (* FIXME *)
  2311     val fs = [];
  2312     val Rs = [];
  2313 
  2314     val ctor = mk_ctor res_Ds (the_single (#ctors fp_res));
  2315     val dtor = mk_dtor res_Ds (the_single (#dtors fp_res));
  2316 
  2317     val friend_names = friend_name :: old_friend_names;
  2318 
  2319     val old_sig_bnf = #fp_bnf old_sig_fp_sugar;
  2320     val old_ssig_bnf = #fp_bnf old_ssig_fp_sugar;
  2321     val sig_bnf = #fp_bnf sig_fp_sugar;
  2322     val ssig_bnf = #fp_bnf ssig_fp_sugar;
  2323 
  2324     val ((((((dead_pre_bnf, dead_fp_bnf), dead_old_sig_bnf), dead_old_ssig_bnf), dead_sig_bnf),
  2325           dead_ssig_bnf), lthy) = lthy
  2326       |> bnf_kill_all_but 1 live_pre_bnf
  2327       ||>> bnf_kill_all_but 0 live_fp_bnf
  2328       ||>> bnf_kill_all_but 1 old_sig_bnf
  2329       ||>> bnf_kill_all_but 1 old_ssig_bnf
  2330       ||>> bnf_kill_all_but 1 sig_bnf
  2331       ||>> bnf_kill_all_but 1 ssig_bnf;
  2332 
  2333     (* FIXME *)
  2334     val pre_bnf = dead_pre_bnf;
  2335     val fp_bnf = dead_fp_bnf;
  2336 
  2337     val old_ssig_fp_ctr_sugar = #fp_ctr_sugar old_ssig_fp_sugar;
  2338     val sig_fp_ctr_sugar = #fp_ctr_sugar sig_fp_sugar;
  2339     val ssig_fp_ctr_sugar = #fp_ctr_sugar ssig_fp_sugar;
  2340 
  2341     val sig_fp_bnf_sugar = #fp_bnf_sugar sig_fp_sugar;
  2342     val old_ssig_fp_bnf_sugar = #fp_bnf_sugar old_ssig_fp_sugar;
  2343     val ssig_fp_bnf_sugar = #fp_bnf_sugar ssig_fp_sugar;
  2344     val old_ssig_fp_induct_sugar = #fp_co_induct_sugar old_ssig_fp_sugar;
  2345     val ssig_fp_induct_sugar = #fp_co_induct_sugar ssig_fp_sugar;
  2346 
  2347     val old_ssig_ctr_sugar = #ctr_sugar old_ssig_fp_ctr_sugar;
  2348     val sig_ctr_sugar = #ctr_sugar sig_fp_ctr_sugar;
  2349     val ssig_ctr_sugar = #ctr_sugar ssig_fp_ctr_sugar;
  2350 
  2351     val old_sig_T_name = fst (dest_Type (#T old_sig_fp_sugar));
  2352     val old_ssig_T_name = fst (dest_Type (#T old_ssig_fp_sugar));
  2353     val sig_T_name = fst (dest_Type (#T sig_fp_sugar));
  2354     val ssig_T_name = fst (dest_Type (#T ssig_fp_sugar));
  2355 
  2356     val res_As = res_Ds @ [Y];
  2357     val res_Bs = res_Ds @ [Z];
  2358     val preT = pre_type_of_ctor Y ctor;
  2359     val YpreT = HOLogic.mk_prodT (Y, preT);
  2360     val old_sig_T = Type (old_sig_T_name, res_As);
  2361     val old_ssig_T = Type (old_ssig_T_name, res_As);
  2362     val sig_T = Type (sig_T_name, res_As);
  2363     val ssig_T = Type (ssig_T_name, res_As);
  2364     val old_Lam_domT = Tsubst Y YpreT old_sig_T;
  2365     val old_eval_core_domT = Tsubst Y YpreT old_ssig_T;
  2366 
  2367     val pre_map = mk_mapN lthy live_AsBs preT pre_bnf;
  2368     val pre_rel = mk_relN lthy live_AsBs preT pre_bnf;
  2369     val dead_pre_map = mk_map1 lthy Y Z preT dead_pre_bnf;
  2370     val dead_pre_rel = mk_rel1 lthy Y Z preT dead_pre_bnf;
  2371     val fp_rel = mk_relN lthy live_EsFs fpT fp_bnf;
  2372     val dtor_unfold = mk_co_rec (Proof_Context.theory_of lthy) Greatest_FP [Z] fpT
  2373       (the_single (#xtor_un_folds fp_res));
  2374     val dead_k_map = mk_map1 lthy Y Z k_T dead_k_bnf;
  2375     val Sig = mk_ctr res_As (the_single (#ctrs sig_ctr_sugar));
  2376     val unsig = mk_disc_or_sel res_As (the_single (the_single (#selss sig_ctr_sugar)));
  2377     val sig_rel = mk_relN lthy live_AsBs sig_T sig_bnf;
  2378     val dead_old_sig_map = mk_map 1 res_As res_Bs (map_of_bnf dead_old_sig_bnf);
  2379     val dead_sig_map = mk_map 1 res_As res_Bs (map_of_bnf dead_sig_bnf);
  2380     val dead_sig_rel = mk_rel 1 res_As res_Bs (rel_of_bnf dead_sig_bnf);
  2381     val [old_Oper, old_VLeaf, old_CLeaf] = map (mk_ctr res_As) (#ctrs old_ssig_ctr_sugar);
  2382     val [Oper, VLeaf, CLeaf] = map (mk_ctr res_As) (#ctrs ssig_ctr_sugar);
  2383     val dead_old_ssig_map = mk_map 1 res_As res_Bs (map_of_bnf dead_old_ssig_bnf);
  2384     val ssig_map = mk_mapN lthy live_AsBs ssig_T ssig_bnf;
  2385     val ssig_rel = mk_relN lthy live_AsBs ssig_T ssig_bnf;
  2386     val dead_ssig_map = mk_map 1 res_As res_Bs (map_of_bnf dead_ssig_bnf);
  2387     val dead_ssig_rel = mk_rel 1 res_As res_Bs (rel_of_bnf dead_ssig_bnf);
  2388     val old_Lam = enforce_type lthy domain_type old_Lam_domT old_Lam0;
  2389     val old_proto_sctr = enforce_type lthy domain_type preT old_proto_sctr0;
  2390     val old_flat = enforce_type lthy range_type old_ssig_T old_flat0;
  2391     val old_eval_core = enforce_type lthy domain_type old_eval_core_domT old_eval_core0;
  2392     val old_eval = enforce_type lthy range_type fpT old_eval0;
  2393     val old_algLam = enforce_type lthy range_type fpT old_algLam0;
  2394 
  2395     val ((embL, embL_def, embL_simps), lthy) = lthy
  2396       |> define_embL embLN fp_b version Y Z fpT old_sig_T old_ssig_T k_T ssig_T Inl_const
  2397         dead_old_sig_map Sig old_Oper old_VLeaf old_CLeaf Oper VLeaf CLeaf;
  2398 
  2399     val ((Lam, Lam_def), lthy) = lthy
  2400       |> define_Lam_step fp_b version Y Z preT old_ssig_T ssig_T dead_pre_map unsig rho embL
  2401         old_Lam;
  2402 
  2403     val ((proto_sctr, proto_sctr_def), lthy) = lthy
  2404       |> define_proto_sctr_step_or_merge fp_b version old_sig_T k_T Sig old_proto_sctr;
  2405 
  2406     val pre_map_comp = map_comp_of_bnf pre_bnf;
  2407     val pre_map_transfer = map_transfer_of_bnf pre_bnf;
  2408     val dead_pre_map_id = map_id_of_bnf dead_pre_bnf;
  2409     val dead_pre_map_comp0 = map_comp0_of_bnf dead_pre_bnf;
  2410     val dead_pre_map_comp = map_comp_of_bnf dead_pre_bnf;
  2411     val fp_map_id = map_id_of_bnf fp_bnf;
  2412     val fp_rel_eq = rel_eq_of_bnf fp_bnf;
  2413     val [ctor_dtor] = #ctor_dtors fp_res;
  2414     val [dtor_inject] = #dtor_injects fp_res;
  2415     val [dtor_unfold_thm] = #xtor_un_fold_thms fp_res;
  2416     val [dtor_unfold_unique] = #xtor_un_fold_uniques fp_res;
  2417     val [dtor_unfold_transfer] = #xtor_un_fold_transfers fp_res;
  2418     val fp_k_T_rel_eqs =
  2419       map rel_eq_of_bnf (map_filter (bnf_of lthy) (fold add_type_namesT [fpT, k_T] []));
  2420     val unsig_thm = the_single (the_single (#sel_thmss sig_ctr_sugar));
  2421     val [sig_map_thm] = #map_thms sig_fp_bnf_sugar;
  2422     val old_sig_map_comp = map_comp_of_bnf old_sig_bnf;
  2423     val old_sig_map_cong = map_cong_of_bnf old_sig_bnf;
  2424     val old_ssig_map_thms = #map_thms old_ssig_fp_bnf_sugar;
  2425     val [Oper_map_thm, VLeaf_map_thm, CLeaf_map_thm] = #map_thms ssig_fp_bnf_sugar;
  2426     val old_sig_map_transfer = map_transfer_of_bnf old_sig_bnf;
  2427     val sig_map_comp = map_comp_of_bnf sig_bnf;
  2428     val sig_map_transfer = map_transfer_of_bnf sig_bnf;
  2429     val ssig_map_thms = #map_thms ssig_fp_bnf_sugar;
  2430     val ssig_map_transfer = map_transfer_of_bnf ssig_bnf;
  2431     val old_ssig_induct = the_single (#co_inducts old_ssig_fp_induct_sugar);
  2432     val ssig_induct = the_single (#co_inducts ssig_fp_induct_sugar);
  2433 
  2434     val proto_sctr_transfer = derive_proto_sctr_transfer_step_or_merge lthy Y Z R dead_pre_rel
  2435       dead_sig_rel proto_sctr proto_sctr_def fp_k_T_rel_eqs [old_proto_sctr_transfer];
  2436     val embL_transfer = derive_transfer_by_transfer_prover lthy live_AsBs Rs R embL [embL_def]
  2437       fp_k_T_rel_eqs [old_sig_map_transfer];
  2438     val Lam_transfer = derive_Lam_or_eval_core_transfer lthy live_AsBs Y Z preT ssig_T Rs R pre_rel
  2439       sig_rel ssig_rel Lam Lam_def fp_k_T_rel_eqs
  2440       [pre_map_transfer, old_Lam_transfer, embL_transfer, rho_transfer];
  2441 
  2442     val ((((((((flat, _, flat_simps), flat_transfer),
  2443             ((eval_core, _, eval_core_simps), eval_core_transfer)), (eval, eval_def)),
  2444           (cutSsig, cutSsig_def)), (algLam, algLam_def)), (corecU, corecU_def)), lthy) = lthy
  2445       |> define_flat_etc fp_b version live_AsBs Y Z preT fpT sig_T ssig_T Oper VLeaf CLeaf pre_rel
  2446         dead_pre_map dtor dtor_unfold dead_sig_map ssig_rel dead_ssig_map Lam Rs R pre_map_transfer
  2447         fp_k_T_rel_eqs sig_map_transfer ssig_map_transfer Lam_transfer dtor_transfer;
  2448 
  2449     val (Sig_pointful_natural, flat_pointful_natural, Lam_natural_pointful, Lam_pointful_natural,
  2450          flat_VLeaf, eval_core_pointful_natural, eval_thm, eval_flat,
  2451          eval_simps as [eval_Oper, _, _], corecU_ctor, corecU_unique, dtor_algLam) =
  2452       derive_Sig_natural_etc lthy live live_AsBs Y Z preT fpT k_T sig_T ssig_T pre_map dead_pre_map
  2453         ctor dtor Sig dead_sig_map Oper VLeaf CLeaf ssig_map dead_ssig_map Lam flat eval_core eval
  2454         cutSsig algLam corecU x fs f g ctor_dtor dtor_inject dtor_unfold_thm dtor_unfold_unique
  2455         sig_map_thm ssig_induct ssig_map_thms Oper_map_thm VLeaf_map_thm CLeaf_map_thm Lam_transfer
  2456         flat_simps flat_transfer eval_core_simps eval_core_transfer eval_def cutSsig_def algLam_def
  2457         corecU_def live_pre_bnf pre_bnf dead_pre_bnf fp_bnf sig_bnf ssig_bnf dead_ssig_bnf;
  2458 
  2459     val proto_sctr_natural = derive_natural_from_transfer_with_pre_type lthy live_AsBs Y Z preT
  2460       ssig_T pre_map ssig_map fs f proto_sctr proto_sctr_transfer [pre_bnf, sig_bnf] [];
  2461     val proto_sctr_pointful_natural = mk_pointful lthy proto_sctr_natural RS sym;
  2462 
  2463     val (embL_pointful_natural, old_algLam_pointful, eval_embL, algLam_algLam) =
  2464       derive_embL_natural_etc lthy Inl_const old_ssig_bnf ssig_bnf Y Z preT fpT old_ssig_T ssig_T
  2465         dead_pre_map Sig dead_old_ssig_map embL old_algLam algLam old_flat flat old_eval_core
  2466         eval_core old_eval eval x f old_ssig_induct dead_pre_map_comp0 dead_pre_map_comp fp_map_id
  2467         dtor_inject dtor_unfold_unique Sig_pointful_natural unsig_thm sig_map_thm old_sig_map_comp
  2468         old_sig_map_cong old_ssig_map_thms old_Lam_pointful_natural Lam_def old_flat_simps
  2469         flat_simps embL_simps embL_transfer old_eval_core_simps eval_core_simps old_eval_thm
  2470         eval_thm old_dtor_algLam dtor_algLam old_algLam_thm;
  2471 
  2472     val algLam_thm = derive_algLam_step_or_merge lthy Y fpT ctor proto_sctr algLam proto_sctr_def
  2473       old_algLam_pointful algLam_algLam;
  2474 
  2475     val k_as_ssig = mk_k_as_ssig Z old_sig_T k_T ssig_T Sig dead_sig_map Oper VLeaf;
  2476     val k_as_ssig' = substT Y fpT k_as_ssig;
  2477 
  2478     val algrho_rhs = HOLogic.mk_comp (eval, k_as_ssig');
  2479     val ((algrho, algrho_def), lthy) = lthy
  2480       |> define_const true fp_b version algrhoN algrho_rhs;
  2481 
  2482     val k_as_ssig_transfer = derive_transfer_by_transfer_prover lthy live_AsBs Rs R k_as_ssig []
  2483       fp_k_T_rel_eqs [sig_map_transfer];
  2484 
  2485     val k_as_ssig_natural = derive_natural_from_transfer lthy [(Y, Z)] [] [] f k_as_ssig
  2486       k_as_ssig_transfer [ssig_bnf] [dead_k_bnf];
  2487 
  2488     val k_as_ssig_natural_pointful = mk_pointful lthy k_as_ssig_natural;
  2489 
  2490     val [_, Lam_Inr] = derive_Lam_Inl_Inr lthy Y Z preT old_sig_T old_ssig_T k_T ssig_T
  2491       dead_pre_map Sig embL old_Lam Lam rho unsig_thm Lam_def;
  2492 
  2493     val eval_core_k_as_ssig = derive_eval_core_k_as_ssig lthy Y preT k_T rho eval_core k_as_ssig x
  2494       pre_map_comp dead_pre_map_id sig_map_comp ssig_map_thms Lam_natural_pointful Lam_Inr
  2495       flat_VLeaf eval_core_simps;
  2496 
  2497     val algLam_algrho = derive_algLam_algrho lthy Y fpT Sig algLam algrho algLam_def algrho_def;
  2498     val dtor_algrho = derive_dtor_algrho lthy Y Z preT fpT k_T ssig_T dead_pre_map dead_k_map dtor
  2499       rho eval algrho x eval_thm k_as_ssig_natural_pointful eval_core_k_as_ssig algrho_def;
  2500     val all_algLam_algs = algLam_algLam :: algLam_algrho :: old_all_algLam_algs;
  2501 
  2502     val (((corecUU, _), corecUU_thm, corecUU_unique, corecUU_transfer, _, sctr_transfer,
  2503           sctr_pointful_natural), lthy) = lthy
  2504       |> define_corecUU_etc fp_b version live_AsBs Y Z preT fpT ssig_T pre_map dead_pre_map pre_rel
  2505         fp_rel ctor Oper ssig_map dead_ssig_map ssig_rel proto_sctr flat eval_core eval corecU fs f
  2506         g Rs R pre_map_transfer fp_k_T_rel_eqs dtor_unfold_transfer dtor_transfer ssig_map_transfer
  2507         proto_sctr_transfer proto_sctr_pointful_natural flat_transfer flat_pointful_natural
  2508         eval_core_transfer eval_core_pointful_natural eval_thm eval_flat eval_Oper algLam_thm
  2509         cutSsig_def corecU_def corecU_ctor corecU_unique pre_bnf dead_pre_bnf fp_res ssig_fp_sugar;
  2510 
  2511     val (ctr_wrapper, friends) =
  2512       mk_ctr_wrapper_friends lthy friend_name friend_T old_sig_T k_T Sig old_buffer;
  2513 
  2514     val Retr = enforce_type lthy (domain_type o domain_type) fpT old_Retr0;
  2515 
  2516     val (dtor_coinduct_info, lthy) = lthy
  2517       |> derive_cong_step fp_b version fpT dead_ssig_bnf dead_pre_bnf eval eval_thm
  2518         eval_core_transfer old_dtor_coinduct_info algrho_def k_as_ssig_transfer Retr equivp_Retr
  2519         Retr_coinduct eval_embL embL_transfer old_all_dead_k_bnfs;
  2520 
  2521     val buffer =
  2522       {Oper = Oper, VLeaf = VLeaf, CLeaf = CLeaf, ctr_wrapper = ctr_wrapper, friends = friends};
  2523 
  2524     val notes =
  2525       [(corecUU_transferN, [corecUU_transfer])] @
  2526       (if Config.get lthy bnf_internals then
  2527          [(algLamN, [algLam_thm]),
  2528           (algLam_algLamN, [algLam_algLam]),
  2529           (algLam_algrhoN, [algLam_algrho]),
  2530           (cong_alg_introsN, #cong_alg_intros dtor_coinduct_info),
  2531           (cong_localeN, [#cong_locale dtor_coinduct_info]),
  2532           (corecU_ctorN, [corecU_ctor]),
  2533           (corecU_uniqueN, [corecU_unique]),
  2534           (corecUUN, [corecUU_thm]),
  2535           (corecUU_uniqueN, [corecUU_unique]),
  2536           (dtor_algLamN, [dtor_algLam]),
  2537           (dtor_algrhoN, [dtor_algrho]),
  2538           (dtor_coinductN, [#dtor_coinduct dtor_coinduct_info]),
  2539           (embL_pointful_naturalN, [embL_pointful_natural]),
  2540           (embL_transferN, [embL_transfer]),
  2541           (evalN, [eval_thm]),
  2542           (eval_core_pointful_naturalN, [eval_core_pointful_natural]),
  2543           (eval_core_transferN, [eval_core_transfer]),
  2544           (eval_flatN, [eval_flat]),
  2545           (eval_simpsN, eval_simps),
  2546           (flat_pointful_naturalN, [flat_pointful_natural]),
  2547           (flat_transferN, [flat_transfer]),
  2548           (k_as_ssig_naturalN, [k_as_ssig_natural]),
  2549           (k_as_ssig_transferN, [k_as_ssig_transfer]),
  2550           (Lam_pointful_naturalN, [Lam_pointful_natural]),
  2551           (Lam_transferN, [Lam_transfer]),
  2552           (proto_sctr_pointful_naturalN, [proto_sctr_pointful_natural]),
  2553           (proto_sctr_transferN, [proto_sctr_transfer]),
  2554           (rho_transferN, [rho_transfer]),
  2555           (sctr_pointful_naturalN, [sctr_pointful_natural]),
  2556           (sctr_transferN, [sctr_transfer]),
  2557           (Sig_pointful_naturalN, [Sig_pointful_natural])]
  2558        else
  2559          [])
  2560       |> map (fn (thmN, thms) =>
  2561         ((mk_version_fp_binding true lthy version fp_b thmN, []), [(thms, [])]));
  2562 
  2563     val phi = Local_Theory.target_morphism lthy;
  2564   in
  2565     (({fp_b = fp_b, version = version, fpT = fpT, Y = Y, Z = Z, friend_names = friend_names,
  2566        sig_fp_sugars = sig_fp_sugar :: old_sig_fp_sugars, ssig_fp_sugar = ssig_fp_sugar, Lam = Lam,
  2567        proto_sctr = proto_sctr, flat = flat, eval_core = eval_core, eval = eval, algLam = algLam,
  2568        corecUU = corecUU, dtor_transfer = dtor_transfer, Lam_transfer = Lam_transfer,
  2569        Lam_pointful_natural = Lam_pointful_natural, proto_sctr_transfer = proto_sctr_transfer,
  2570        flat_simps = flat_simps, eval_core_simps = eval_core_simps, eval_thm = eval_thm,
  2571        eval_simps = eval_simps, all_algLam_algs = all_algLam_algs, algLam_thm = algLam_thm,
  2572        dtor_algLam = dtor_algLam, corecUU_thm = corecUU_thm, corecUU_unique = corecUU_unique,
  2573        corecUU_transfer = corecUU_transfer, buffer = buffer,
  2574        all_dead_k_bnfs = dead_k_bnf :: old_all_dead_k_bnfs, Retr = Retr, equivp_Retr = equivp_Retr,
  2575        Retr_coinduct = Retr_coinduct, dtor_coinduct_info = dtor_coinduct_info}
  2576       |> morph_corec_info phi,
  2577       ({algrho = algrho, dtor_algrho = dtor_algrho, algLam_algrho = algLam_algrho}
  2578        |> morph_friend_info phi)),
  2579      lthy |> Local_Theory.notes notes |> snd)
  2580   end;
  2581 
  2582 fun derive_corecUU_merge (fpT as Type (fpT_name, res_Ds))
  2583     ({friend_names = old1_friend_names,
  2584       sig_fp_sugars = old1_sig_fp_sugars as old1_sig_fp_sugar :: _,
  2585       ssig_fp_sugar = old1_ssig_fp_sugar, Lam = old1_Lam0, proto_sctr = old1_proto_sctr0,
  2586       flat = old1_flat0, eval_core = old1_eval_core0, eval = old1_eval0, algLam = old1_algLam0,
  2587       dtor_transfer, Lam_transfer = old1_Lam_transfer,
  2588       Lam_pointful_natural = old1_Lam_pointful_natural,
  2589       proto_sctr_transfer = old1_proto_sctr_transfer, flat_simps = old1_flat_simps,
  2590       eval_core_simps = old1_eval_core_simps, eval_thm = old1_eval_thm,
  2591       all_algLam_algs = old1_all_algLam_algs, algLam_thm = old1_algLam_thm,
  2592       dtor_algLam = old1_dtor_algLam, buffer = old1_buffer, all_dead_k_bnfs = old1_all_dead_k_bnfs,
  2593       Retr = old1_Retr0, equivp_Retr, Retr_coinduct, dtor_coinduct_info = old1_dtor_coinduct_info,
  2594       ...} : corec_info)
  2595     ({friend_names = old2_friend_names,
  2596       sig_fp_sugars = old2_sig_fp_sugars as old2_sig_fp_sugar :: _,
  2597       ssig_fp_sugar = old2_ssig_fp_sugar, Lam = old2_Lam0, flat = old2_flat0,
  2598       eval_core = old2_eval_core0, eval = old2_eval0, algLam = old2_algLam0,
  2599       Lam_transfer = old2_Lam_transfer, Lam_pointful_natural = old2_Lam_pointful_natural,
  2600       flat_simps = old2_flat_simps, eval_core_simps = old2_eval_core_simps,
  2601       eval_thm = old2_eval_thm, all_algLam_algs = old2_all_algLam_algs,
  2602       algLam_thm = old2_algLam_thm, dtor_algLam = old2_dtor_algLam, buffer = old2_buffer,
  2603       all_dead_k_bnfs = old2_all_dead_k_bnfs, dtor_coinduct_info = old2_dtor_coinduct_info, ...}
  2604      : corec_info)
  2605     lthy =
  2606   let
  2607     val {T = Type (_, fpT_args0), pre_bnf = live_pre_bnf, fp_bnf = live_fp_bnf, fp_res, ...} =
  2608       checked_fp_sugar_of lthy fpT_name;
  2609     val fpT_Ss = map Type.sort_of_atyp fpT_args0;
  2610     val live_fp_alives = liveness_of_fp_bnf (length fpT_args0) live_fp_bnf;
  2611 
  2612     val ((Ds, [Y, Z]), names_lthy) = lthy
  2613       |> mk_TFrees' fpT_Ss
  2614       ||>> mk_TFrees 2;
  2615 
  2616     (* FIXME *)
  2617     val live_EsFs = [];
  2618     val live_AsBs = live_EsFs @ [(Y, Z)];
  2619     val live = length live_EsFs;
  2620 
  2621     val ((((x, f), g), R), _) = names_lthy
  2622       |> yield_singleton (mk_Frees "x") Y
  2623       ||>> yield_singleton (mk_Frees "f") (Y --> Z)
  2624       ||>> yield_singleton (mk_Frees "g") (Y --> Z)
  2625       ||>> yield_singleton (mk_Frees "R") (mk_pred2T Y Z);
  2626 
  2627     (* FIXME *)
  2628     val fs = [];
  2629     val Rs = [];
  2630 
  2631     val ctor = mk_ctor res_Ds (the_single (#ctors fp_res));
  2632     val dtor = mk_dtor res_Ds (the_single (#dtors fp_res));
  2633 
  2634     val old1_sig_T_name = fst (dest_Type (#T old1_sig_fp_sugar));
  2635     val old2_sig_T_name = fst (dest_Type (#T old2_sig_fp_sugar));
  2636     val old1_ssig_T_name = fst (dest_Type (#T old1_ssig_fp_sugar));
  2637     val old2_ssig_T_name = fst (dest_Type (#T old2_ssig_fp_sugar));
  2638 
  2639     val fp_alives = map (K false) live_fp_alives;
  2640 
  2641     val As = Ds @ [Y];
  2642     val res_As = res_Ds @ [Y];
  2643     val res_Bs = res_Ds @ [Z];
  2644     val preT = pre_type_of_ctor Y ctor;
  2645     val YpreT = HOLogic.mk_prodT (Y, preT);
  2646     val fpT0 = Type (fpT_name, Ds);
  2647     val old1_sig_T0 = Type (old1_sig_T_name, As);
  2648     val old2_sig_T0 = Type (old2_sig_T_name, As);
  2649     val old1_sig_T = Type (old1_sig_T_name, res_As);
  2650     val old2_sig_T = Type (old2_sig_T_name, res_As);
  2651     val old1_ssig_T = Type (old1_ssig_T_name, res_As);
  2652     val old2_ssig_T = Type (old2_ssig_T_name, res_As);
  2653     val old1_Lam_domT = Tsubst Y YpreT old1_sig_T;
  2654     val old2_Lam_domT = Tsubst Y YpreT old2_sig_T;
  2655     val old1_eval_core_domT = Tsubst Y YpreT old1_ssig_T;
  2656     val old2_eval_core_domT = Tsubst Y YpreT old2_ssig_T;
  2657 
  2658     val ((fp_b, version), lthy) = lthy |> get_name_next_version_of fpT_name;
  2659 
  2660     val ((sig_fp_sugar, ssig_fp_sugar), lthy) = lthy
  2661       |> define_sig_type fp_b version fp_alives Ds Y (mk_sumT (old1_sig_T0, old2_sig_T0))
  2662       ||>> define_ssig_type fp_b version fp_alives Ds Y fpT0;
  2663 
  2664     val sig_T_name = fst (dest_Type (#T sig_fp_sugar));
  2665     val ssig_T_name = fst (dest_Type (#T ssig_fp_sugar));
  2666 
  2667     val old1_sig_bnf = #fp_bnf old1_sig_fp_sugar;
  2668     val old2_sig_bnf = #fp_bnf old2_sig_fp_sugar;
  2669     val old1_ssig_bnf = #fp_bnf old1_ssig_fp_sugar;
  2670     val old2_ssig_bnf = #fp_bnf old2_ssig_fp_sugar;
  2671     val sig_bnf = #fp_bnf sig_fp_sugar;
  2672     val ssig_bnf = #fp_bnf ssig_fp_sugar;
  2673 
  2674     val ((((((((dead_pre_bnf, dead_fp_bnf), dead_old1_sig_bnf), dead_old2_sig_bnf),
  2675         dead_old1_ssig_bnf), dead_old2_ssig_bnf), dead_sig_bnf), dead_ssig_bnf), lthy) = lthy
  2676       |> bnf_kill_all_but 1 live_pre_bnf
  2677       ||>> bnf_kill_all_but 0 live_fp_bnf
  2678       ||>> bnf_kill_all_but 1 old1_sig_bnf
  2679       ||>> bnf_kill_all_but 1 old2_sig_bnf
  2680       ||>> bnf_kill_all_but 1 old1_ssig_bnf
  2681       ||>> bnf_kill_all_but 1 old2_ssig_bnf
  2682       ||>> bnf_kill_all_but 1 sig_bnf
  2683       ||>> bnf_kill_all_but 1 ssig_bnf;
  2684 
  2685     (* FIXME *)
  2686     val pre_bnf = dead_pre_bnf;
  2687     val fp_bnf = dead_fp_bnf;
  2688 
  2689     val old1_ssig_fp_ctr_sugar = #fp_ctr_sugar old1_ssig_fp_sugar;
  2690     val old2_ssig_fp_ctr_sugar = #fp_ctr_sugar old2_ssig_fp_sugar;
  2691     val sig_fp_ctr_sugar = #fp_ctr_sugar sig_fp_sugar;
  2692     val ssig_fp_ctr_sugar = #fp_ctr_sugar ssig_fp_sugar;
  2693 
  2694     val sig_fp_bnf_sugar = #fp_bnf_sugar sig_fp_sugar;
  2695     val old1_ssig_fp_bnf_sugar = #fp_bnf_sugar old1_ssig_fp_sugar;
  2696     val old2_ssig_fp_bnf_sugar = #fp_bnf_sugar old2_ssig_fp_sugar;
  2697     val ssig_fp_bnf_sugar = #fp_bnf_sugar ssig_fp_sugar;
  2698     val old1_ssig_fp_induct_sugar = #fp_co_induct_sugar old1_ssig_fp_sugar;
  2699     val old2_ssig_fp_induct_sugar = #fp_co_induct_sugar old2_ssig_fp_sugar;
  2700     val ssig_fp_induct_sugar = #fp_co_induct_sugar ssig_fp_sugar;
  2701 
  2702     val old1_ssig_ctr_sugar = #ctr_sugar old1_ssig_fp_ctr_sugar;
  2703     val old2_ssig_ctr_sugar = #ctr_sugar old2_ssig_fp_ctr_sugar;
  2704     val sig_ctr_sugar = #ctr_sugar sig_fp_ctr_sugar;
  2705     val ssig_ctr_sugar = #ctr_sugar ssig_fp_ctr_sugar;
  2706 
  2707     val sig_T = Type (sig_T_name, res_As);
  2708     val ssig_T = Type (ssig_T_name, res_As);
  2709 
  2710     val pre_map = mk_mapN lthy live_AsBs preT pre_bnf;
  2711     val pre_rel = mk_relN lthy live_AsBs preT pre_bnf;
  2712     val dead_pre_map = mk_map1 lthy Y Z preT dead_pre_bnf;
  2713     val dead_pre_rel = mk_rel1 lthy Y Z preT dead_pre_bnf;
  2714     val fp_rel = mk_relN lthy live_EsFs fpT fp_bnf;
  2715     val dtor_unfold = mk_co_rec (Proof_Context.theory_of lthy) Greatest_FP [Z] fpT
  2716       (the_single (#xtor_un_folds fp_res));
  2717     val Sig = mk_ctr res_As (the_single (#ctrs sig_ctr_sugar));
  2718     val unsig = mk_disc_or_sel res_As (the_single (the_single (#selss sig_ctr_sugar)));
  2719     val sig_rel = mk_relN lthy live_AsBs sig_T sig_bnf;
  2720     val dead_old1_sig_map = mk_map 1 res_As res_Bs (map_of_bnf dead_old1_sig_bnf);
  2721     val dead_old2_sig_map = mk_map 1 res_As res_Bs (map_of_bnf dead_old2_sig_bnf);
  2722     val dead_sig_map = mk_map 1 res_As res_Bs (map_of_bnf dead_sig_bnf);
  2723     val dead_sig_rel = mk_rel 1 res_As res_Bs (rel_of_bnf dead_sig_bnf);
  2724     val [old1_Oper, old1_VLeaf, old1_CLeaf] = map (mk_ctr res_As) (#ctrs old1_ssig_ctr_sugar);
  2725     val [old2_Oper, old2_VLeaf, old2_CLeaf] = map (mk_ctr res_As) (#ctrs old2_ssig_ctr_sugar);
  2726     val [Oper, VLeaf, CLeaf] = map (mk_ctr res_As) (#ctrs ssig_ctr_sugar);
  2727     val old1_ssig_map = mk_map 1 res_As res_Bs (map_of_bnf dead_old1_ssig_bnf);
  2728     val old2_ssig_map = mk_map 1 res_As res_Bs (map_of_bnf dead_old2_ssig_bnf);
  2729     val ssig_map = mk_mapN lthy live_AsBs ssig_T ssig_bnf;
  2730     val ssig_rel = mk_relN lthy live_AsBs ssig_T ssig_bnf;
  2731     val dead_ssig_map = mk_map 1 res_As res_Bs (map_of_bnf dead_ssig_bnf);
  2732     val old1_Lam = enforce_type lthy domain_type old1_Lam_domT old1_Lam0;
  2733     val old2_Lam = enforce_type lthy domain_type old2_Lam_domT old2_Lam0;
  2734     val old1_proto_sctr = enforce_type lthy domain_type preT old1_proto_sctr0;
  2735     val old1_flat = enforce_type lthy range_type old1_ssig_T old1_flat0;
  2736     val old2_flat = enforce_type lthy range_type old2_ssig_T old2_flat0;
  2737     val old1_eval_core = enforce_type lthy domain_type old1_eval_core_domT old1_eval_core0;
  2738     val old2_eval_core = enforce_type lthy domain_type old2_eval_core_domT old2_eval_core0;
  2739     val old1_eval = enforce_type lthy range_type fpT old1_eval0;
  2740     val old2_eval = enforce_type lthy range_type fpT old2_eval0;
  2741     val old1_algLam = enforce_type lthy range_type fpT old1_algLam0;
  2742     val old2_algLam = enforce_type lthy range_type fpT old2_algLam0;
  2743 
  2744     val ((embLL, embLL_def, embLL_simps), lthy) = lthy
  2745       |> define_embL embLLN fp_b version Y Z fpT old1_sig_T old1_ssig_T old2_sig_T ssig_T Inl_const
  2746         dead_old1_sig_map Sig old1_Oper old1_VLeaf old1_CLeaf Oper VLeaf CLeaf;
  2747 
  2748     val ((embLR, embLR_def, embLR_simps), lthy) = lthy
  2749       |> define_embL embLRN fp_b version Y Z fpT old2_sig_T old2_ssig_T old1_sig_T ssig_T
  2750         (fn T => fn U => Inr_const U T) dead_old2_sig_map Sig old2_Oper old2_VLeaf old2_CLeaf Oper
  2751         VLeaf CLeaf;
  2752 
  2753     val ((Lam, Lam_def), lthy) = lthy
  2754       |> define_Lam_merge fp_b version Y Z preT old1_ssig_T old2_ssig_T ssig_T dead_pre_map unsig
  2755         embLL embLR old1_Lam old2_Lam;
  2756 
  2757     val ((proto_sctr, proto_sctr_def), lthy) = lthy
  2758       |> define_proto_sctr_step_or_merge fp_b version old1_sig_T old2_sig_T Sig old1_proto_sctr;
  2759 
  2760     val pre_map_transfer = map_transfer_of_bnf pre_bnf;
  2761     val dead_pre_map_comp0 = map_comp0_of_bnf dead_pre_bnf;
  2762     val dead_pre_map_comp = map_comp_of_bnf dead_pre_bnf;
  2763     val fp_map_id = map_id_of_bnf fp_bnf;
  2764     val fp_rel_eq = rel_eq_of_bnf fp_bnf;
  2765     val [ctor_dtor] = #ctor_dtors fp_res;
  2766     val [dtor_inject] = #dtor_injects fp_res;
  2767     val [dtor_unfold_thm] = #xtor_un_fold_thms fp_res;
  2768     val [dtor_unfold_unique] = #xtor_un_fold_uniques fp_res;
  2769     val [dtor_unfold_transfer] = #xtor_un_fold_transfers fp_res;
  2770     val unsig_thm = the_single (the_single (#sel_thmss sig_ctr_sugar));
  2771     val [sig_map_thm] = #map_thms sig_fp_bnf_sugar;
  2772     val old1_sig_map_comp = map_comp_of_bnf old1_sig_bnf;
  2773     val old2_sig_map_comp = map_comp_of_bnf old2_sig_bnf;
  2774     val old1_sig_map_cong = map_cong_of_bnf old1_sig_bnf;
  2775     val old2_sig_map_cong = map_cong_of_bnf old2_sig_bnf;
  2776     val old1_ssig_map_thms = #map_thms old1_ssig_fp_bnf_sugar;
  2777     val old2_ssig_map_thms = #map_thms old2_ssig_fp_bnf_sugar;
  2778     val [Oper_map_thm, VLeaf_map_thm, CLeaf_map_thm] = #map_thms ssig_fp_bnf_sugar;
  2779     val old1_sig_map_transfer = map_transfer_of_bnf old1_sig_bnf;
  2780     val old2_sig_map_transfer = map_transfer_of_bnf old2_sig_bnf;
  2781     val sig_map_transfer = map_transfer_of_bnf sig_bnf;
  2782     val ssig_map_thms = #map_thms ssig_fp_bnf_sugar;
  2783     val ssig_map_transfer = map_transfer_of_bnf ssig_bnf;
  2784     val old1_ssig_induct = the_single (#co_inducts old1_ssig_fp_induct_sugar);
  2785     val old2_ssig_induct = the_single (#co_inducts old2_ssig_fp_induct_sugar);
  2786     val ssig_induct = the_single (#co_inducts ssig_fp_induct_sugar);
  2787 
  2788     val proto_sctr_transfer = derive_proto_sctr_transfer_step_or_merge lthy Y Z R dead_pre_rel
  2789       dead_sig_rel proto_sctr proto_sctr_def [] [old1_proto_sctr_transfer];
  2790     val embLL_transfer = derive_transfer_by_transfer_prover lthy live_AsBs Rs R embLL [embLL_def] []
  2791       [old1_sig_map_transfer];
  2792     val embLR_transfer = derive_transfer_by_transfer_prover lthy live_AsBs Rs R embLR [embLR_def] []
  2793       [old2_sig_map_transfer];
  2794     val Lam_transfer = derive_Lam_or_eval_core_transfer lthy live_AsBs Y Z preT ssig_T Rs R
  2795       pre_rel sig_rel ssig_rel Lam Lam_def []
  2796       [pre_map_transfer, old1_Lam_transfer, old2_Lam_transfer, embLL_transfer, embLR_transfer];
  2797 
  2798     val ((((((((flat, _, flat_simps), flat_transfer),
  2799             ((eval_core, _, eval_core_simps), eval_core_transfer)), (eval, eval_def)),
  2800           (cutSsig, cutSsig_def)), (algLam, algLam_def)), (corecU, corecU_def)), lthy) = lthy
  2801       |> define_flat_etc fp_b version live_AsBs Y Z preT fpT sig_T ssig_T Oper VLeaf CLeaf pre_rel
  2802         dead_pre_map dtor dtor_unfold dead_sig_map ssig_rel dead_ssig_map Lam Rs R pre_map_transfer
  2803         [fp_rel_eq] sig_map_transfer ssig_map_transfer Lam_transfer dtor_transfer;
  2804 
  2805     val (Sig_pointful_natural, flat_pointful_natural, _, Lam_pointful_natural, _,
  2806          eval_core_pointful_natural, eval_thm, eval_flat, eval_simps as [eval_Oper, _, _],
  2807          corecU_ctor, corecU_unique, dtor_algLam) =
  2808       derive_Sig_natural_etc lthy live live_AsBs Y Z preT fpT fpT sig_T ssig_T pre_map dead_pre_map
  2809         ctor dtor Sig dead_sig_map Oper VLeaf CLeaf ssig_map dead_ssig_map Lam flat eval_core eval
  2810         cutSsig algLam corecU x fs f g ctor_dtor dtor_inject dtor_unfold_thm dtor_unfold_unique
  2811         sig_map_thm ssig_induct ssig_map_thms Oper_map_thm VLeaf_map_thm CLeaf_map_thm Lam_transfer
  2812         flat_simps flat_transfer eval_core_simps eval_core_transfer eval_def cutSsig_def algLam_def
  2813         corecU_def live_pre_bnf pre_bnf dead_pre_bnf fp_bnf sig_bnf ssig_bnf dead_ssig_bnf;
  2814 
  2815     val proto_sctr_natural = derive_natural_from_transfer_with_pre_type lthy live_AsBs Y Z preT
  2816       ssig_T pre_map ssig_map fs f proto_sctr proto_sctr_transfer [pre_bnf, sig_bnf] [];
  2817     val proto_sctr_pointful_natural = mk_pointful lthy proto_sctr_natural RS sym;
  2818 
  2819     val (embLL_pointful_natural, old1_algLam_pointful, eval_embLL, algLam_algLamL) =
  2820       derive_embL_natural_etc lthy Inl_const old1_ssig_bnf ssig_bnf Y Z preT fpT old1_ssig_T ssig_T
  2821         dead_pre_map Sig old1_ssig_map embLL old1_algLam algLam old1_flat flat old1_eval_core
  2822         eval_core old1_eval eval x f old1_ssig_induct dead_pre_map_comp0 dead_pre_map_comp fp_map_id
  2823         dtor_inject dtor_unfold_unique Sig_pointful_natural unsig_thm sig_map_thm old1_sig_map_comp
  2824         old1_sig_map_cong old1_ssig_map_thms old1_Lam_pointful_natural Lam_def old1_flat_simps
  2825         flat_simps embLL_simps embLL_transfer old1_eval_core_simps eval_core_simps old1_eval_thm
  2826         eval_thm old1_dtor_algLam dtor_algLam old1_algLam_thm;
  2827 
  2828     val (embLR_pointful_natural, _, eval_embLR, algLam_algLamR) =
  2829       derive_embL_natural_etc lthy Inr_const old2_ssig_bnf ssig_bnf Y Z preT fpT old2_ssig_T ssig_T
  2830         dead_pre_map Sig old2_ssig_map embLR old2_algLam algLam old2_flat flat old2_eval_core
  2831         eval_core old2_eval eval x f old2_ssig_induct dead_pre_map_comp0 dead_pre_map_comp fp_map_id
  2832         dtor_inject dtor_unfold_unique Sig_pointful_natural unsig_thm sig_map_thm old2_sig_map_comp
  2833         old2_sig_map_cong old2_ssig_map_thms old2_Lam_pointful_natural Lam_def old2_flat_simps
  2834         flat_simps embLR_simps embLR_transfer old2_eval_core_simps eval_core_simps old2_eval_thm
  2835         eval_thm old2_dtor_algLam dtor_algLam old2_algLam_thm;
  2836 
  2837     val algLam_thm = derive_algLam_step_or_merge lthy Y fpT ctor proto_sctr algLam proto_sctr_def
  2838       old1_algLam_pointful algLam_algLamL;
  2839 
  2840     val all_algLam_algs = algLam_algLamL :: algLam_algLamR ::
  2841       merge_lists (Thm.eq_thm_prop o apply2 zero_var_indexes) old1_all_algLam_algs
  2842         old2_all_algLam_algs;
  2843 
  2844     val (((corecUU, _), corecUU_thm, corecUU_unique, corecUU_transfer, _, sctr_transfer,
  2845           sctr_pointful_natural), lthy) = lthy
  2846       |> define_corecUU_etc fp_b version live_AsBs Y Z preT fpT ssig_T pre_map dead_pre_map pre_rel
  2847         fp_rel ctor Oper ssig_map dead_ssig_map ssig_rel proto_sctr flat eval_core eval corecU fs f
  2848         g Rs R pre_map_transfer [] dtor_unfold_transfer dtor_transfer ssig_map_transfer
  2849         proto_sctr_transfer proto_sctr_pointful_natural flat_transfer flat_pointful_natural
  2850         eval_core_transfer eval_core_pointful_natural eval_thm eval_flat eval_Oper algLam_thm
  2851         cutSsig_def corecU_def corecU_ctor corecU_unique pre_bnf dead_pre_bnf fp_res ssig_fp_sugar;
  2852 
  2853     val Retr = enforce_type lthy (domain_type o domain_type) fpT old1_Retr0;
  2854 
  2855     val embed_Sig_inl = embed_Sig lthy Sig (Inl_const old1_sig_T old2_sig_T);
  2856     val embed_Sig_inr = embed_Sig lthy Sig (Inr_const old1_sig_T old2_sig_T);
  2857 
  2858     val ctr_wrapper = embed_Sig_inl (#ctr_wrapper old1_buffer);
  2859     val friends = Symtab.merge (K true)
  2860       (Symtab.map (K (apsnd embed_Sig_inl)) (#friends old1_buffer),
  2861        Symtab.map (K (apsnd embed_Sig_inr)) (#friends old2_buffer));
  2862 
  2863     val old_fp_sugars =
  2864       merge_lists (op = o apply2 (fst o dest_Type o #T)) old1_sig_fp_sugars old2_sig_fp_sugars;
  2865 
  2866     val ((dtor_coinduct_info, all_dead_k_bnfs, friend_names), lthy) = lthy
  2867       |> derive_cong_merge fp_b version fpT old1_friend_names old2_friend_names dead_ssig_bnf
  2868         dead_pre_bnf eval eval_thm eval_core_transfer old1_dtor_coinduct_info
  2869         old2_dtor_coinduct_info Retr equivp_Retr Retr_coinduct eval_embLL embLL_transfer eval_embLR
  2870         embLR_transfer old1_all_dead_k_bnfs old2_all_dead_k_bnfs;
  2871 
  2872     val buffer =
  2873       {Oper = Oper, VLeaf = VLeaf, CLeaf = CLeaf, ctr_wrapper = ctr_wrapper, friends = friends};
  2874 
  2875     val notes =
  2876       [(corecUU_transferN, [corecUU_transfer])] @
  2877       (if Config.get lthy bnf_internals then
  2878          [(algLamN, [algLam_thm]),
  2879           (algLam_algLamN, [algLam_algLamL, algLam_algLamR]),
  2880           (cong_alg_introsN, #cong_alg_intros dtor_coinduct_info),
  2881           (cong_localeN, [#cong_locale dtor_coinduct_info]),
  2882           (corecU_ctorN, [corecU_ctor]),
  2883           (corecU_uniqueN, [corecU_unique]),
  2884           (corecUUN, [corecUU_thm]),
  2885           (corecUU_uniqueN, [corecUU_unique]),
  2886           (dtor_algLamN, [dtor_algLam]),
  2887           (dtor_coinductN, [#dtor_coinduct dtor_coinduct_info]),
  2888           (eval_core_pointful_naturalN, [eval_core_pointful_natural]),
  2889           (eval_core_transferN, [eval_core_transfer]),
  2890           (embL_pointful_naturalN, [embLL_pointful_natural, embLR_pointful_natural]),
  2891           (embL_transferN, [embLL_transfer, embLR_transfer]),
  2892           (evalN, [eval_thm]),
  2893           (eval_flatN, [eval_flat]),
  2894           (eval_simpsN, eval_simps),
  2895           (flat_pointful_naturalN, [flat_pointful_natural]),
  2896           (flat_transferN, [flat_transfer]),
  2897           (Lam_pointful_naturalN, [Lam_pointful_natural]),
  2898           (Lam_transferN, [Lam_transfer]),
  2899           (proto_sctr_pointful_naturalN, [proto_sctr_pointful_natural]),
  2900           (proto_sctr_transferN, [proto_sctr_transfer]),
  2901           (sctr_pointful_naturalN, [sctr_pointful_natural]),
  2902           (sctr_transferN, [sctr_transfer]),
  2903           (Sig_pointful_naturalN, [Sig_pointful_natural])]
  2904        else
  2905          [])
  2906       |> map (fn (thmN, thms) =>
  2907         ((mk_version_fp_binding true lthy version fp_b thmN, []), [(thms, [])]));
  2908   in
  2909     ({fp_b = fp_b, version = version, fpT = fpT, Y = Y, Z = Z, friend_names = friend_names,
  2910       sig_fp_sugars = sig_fp_sugar :: old_fp_sugars, ssig_fp_sugar = ssig_fp_sugar, Lam = Lam,
  2911       proto_sctr = proto_sctr, flat = flat, eval_core = eval_core, eval = eval, algLam = algLam,
  2912       corecUU = corecUU, dtor_transfer = dtor_transfer, Lam_transfer = Lam_transfer,
  2913       Lam_pointful_natural = Lam_pointful_natural, proto_sctr_transfer = proto_sctr_transfer,
  2914       flat_simps = flat_simps, eval_core_simps = eval_core_simps, eval_thm = eval_thm,
  2915       eval_simps = eval_simps, all_algLam_algs = all_algLam_algs, algLam_thm = algLam_thm,
  2916       dtor_algLam = dtor_algLam, corecUU_thm = corecUU_thm, corecUU_unique = corecUU_unique,
  2917       corecUU_transfer = corecUU_transfer, buffer = buffer, all_dead_k_bnfs = all_dead_k_bnfs,
  2918       Retr = Retr, equivp_Retr = equivp_Retr, Retr_coinduct = Retr_coinduct,
  2919       dtor_coinduct_info = dtor_coinduct_info}
  2920      |> morph_corec_info (Local_Theory.target_morphism lthy),
  2921      lthy |> Local_Theory.notes notes |> snd)
  2922   end;
  2923 
  2924 fun set_corec_info_exprs fpT_name f =
  2925   Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
  2926     let val exprs = f phi in
  2927       Data.map (apsnd (fn [info_tab] => [Symtab.map_default (fpT_name, exprs) (K exprs) info_tab]))
  2928     end);
  2929 
  2930 fun subsume_corec_info_ad ctxt {fpT = fpT1, friend_names = friend_names1}
  2931     {fpT = fpT2, friend_names = friend_names2} =
  2932   Sign.typ_instance (Proof_Context.theory_of ctxt) (fpT1, fpT2) andalso
  2933   subset (op =) (friend_names1, friend_names2);
  2934 
  2935 fun subsume_corec_info_expr ctxt expr1 expr2 =
  2936   subsume_corec_info_ad ctxt (corec_ad_of_expr expr1) (corec_ad_of_expr expr2);
  2937 
  2938 fun instantiate_corec_info thy res_T (info as {fpT, ...}) =
  2939   let
  2940     val As_rho = tvar_subst thy [fpT] [res_T];
  2941     val substAT = Term.typ_subst_TVars As_rho;
  2942     val substA = Term.subst_TVars As_rho;
  2943     val phi = Morphism.typ_morphism "BNF" substAT $> Morphism.term_morphism "BNF" substA;
  2944   in
  2945     morph_corec_info phi info
  2946   end;
  2947 
  2948 fun instantiate_corec_info_expr thy res_T (Ad ({friend_names, ...}, f)) =
  2949     Ad ({fpT = res_T, friend_names = friend_names}, f #>> instantiate_corec_info thy res_T)
  2950   | instantiate_corec_info_expr thy res_T (Info info) =
  2951     Info (instantiate_corec_info thy res_T info);
  2952 
  2953 fun ensure_Info expr = corec_info_of_expr expr #>> Info
  2954 and ensure_Info_if_Info old_expr (expr, lthy) =
  2955   if is_Info old_expr then ensure_Info expr lthy else (expr, lthy)
  2956 and merge_corec_info_exprs old_exprs expr1 expr2 lthy =
  2957   if subsume_corec_info_expr lthy expr2 expr1 then
  2958     if subsume_corec_info_expr lthy expr1 expr2 andalso is_Ad expr1 then
  2959       (expr2, lthy)
  2960     else
  2961       ensure_Info_if_Info expr2 (expr1, lthy)
  2962   else if subsume_corec_info_expr lthy expr1 expr2 then
  2963     ensure_Info_if_Info expr1 (expr2, lthy)
  2964   else
  2965     let
  2966       val thy = Proof_Context.theory_of lthy;
  2967 
  2968       val {fpT = fpT1, friend_names = friend_names1} = corec_ad_of_expr expr1;
  2969       val {fpT = fpT2, friend_names = friend_names2} = corec_ad_of_expr expr2;
  2970       val fpT0 = typ_unify_disjointly thy (fpT1, fpT2);
  2971 
  2972       val fpT = singleton (freeze_types lthy []) fpT0;
  2973       val friend_names = merge_lists (op =) friend_names1 friend_names2;
  2974 
  2975       val expr =
  2976         Ad ({fpT = fpT, friend_names = friend_names},
  2977           corec_info_of_expr expr1
  2978           ##>> corec_info_of_expr expr2
  2979           #-> uncurry (derive_corecUU_merge fpT));
  2980 
  2981       val old_same_type_exprs =
  2982         if old_exprs then
  2983           []
  2984           |> Sign.typ_instance thy (fpT1, fpT0) ? cons expr1
  2985           |> Sign.typ_instance thy (fpT2, fpT0) ? cons expr2
  2986         else
  2987           [];
  2988     in
  2989       (expr, lthy) |> fold ensure_Info_if_Info old_same_type_exprs
  2990     end
  2991 and insert_corec_info_expr expr exprs lthy =
  2992   let
  2993     val thy = Proof_Context.theory_of lthy;
  2994 
  2995     val {fpT = new_fpT, ...} = corec_ad_of_expr expr;
  2996 
  2997     val is_Tinst = curry (Sign.typ_instance thy);
  2998     fun is_Tequiv T U = is_Tinst T U andalso is_Tinst U T;
  2999 
  3000     val (((equiv_exprs, sub_exprs), sup_exprs), incomp_exprs) = exprs
  3001       |> List.partition ((fn {fpT, ...} => is_Tequiv fpT new_fpT) o corec_ad_of_expr)
  3002       ||>> List.partition ((fn {fpT, ...} => is_Tinst fpT new_fpT) o corec_ad_of_expr)
  3003       ||>> List.partition ((fn {fpT, ...} => is_Tinst new_fpT fpT) o corec_ad_of_expr);
  3004 
  3005     fun add_instantiated_incomp_expr expr exprs =
  3006       let val {fpT, ...} = corec_ad_of_expr expr in
  3007         (case try (typ_unify_disjointly thy) (fpT, new_fpT) of
  3008           SOME new_T =>
  3009           let val subsumes = (fn {fpT, ...} => is_Tinst new_T fpT) o corec_ad_of_expr in
  3010             if exists (exists subsumes) [exprs, sub_exprs] then exprs
  3011             else instantiate_corec_info_expr thy new_T expr :: exprs
  3012           end
  3013         | NONE => exprs)
  3014       end;
  3015 
  3016     val unincomp_exprs = fold add_instantiated_incomp_expr incomp_exprs [];
  3017     val ((merged_sub_exprs, merged_unincomp_exprs), lthy) = lthy
  3018       |> fold_map (merge_corec_info_exprs true expr) sub_exprs
  3019       ||>> fold_map (merge_corec_info_exprs false expr) unincomp_exprs;
  3020     val (merged_equiv_expr, lthy) = (expr, lthy)
  3021       |> fold (uncurry o merge_corec_info_exprs true) equiv_exprs;
  3022   in
  3023     (merged_unincomp_exprs @ merged_sub_exprs @ merged_equiv_expr :: sup_exprs @ incomp_exprs
  3024      |> sort (rev_order o int_ord o apply2 (length o #friend_names o corec_ad_of_expr)),
  3025      lthy)
  3026   end
  3027 and register_corec_info (info as {fpT = Type (fpT_name, _), ...}) lthy =
  3028   let
  3029     val (exprs, lthy) = insert_corec_info_expr (Info info) (corec_info_exprs_of lthy fpT_name) lthy;
  3030   in
  3031     lthy |> set_corec_info_exprs fpT_name (fn phi => map (morph_corec_info_expr phi) exprs)
  3032   end
  3033 and corec_info_of_expr (Ad (_, f)) lthy = f lthy
  3034   | corec_info_of_expr (Info info) lthy = (info, lthy);
  3035 
  3036 fun nonempty_corec_info_exprs_of fpT_name lthy =
  3037   (case corec_info_exprs_of lthy fpT_name of
  3038     [] =>
  3039     derive_corecUU_base fpT_name lthy
  3040     |> (fn (info, lthy) =>
  3041       ([Info info], lthy
  3042          |> set_corec_info_exprs fpT_name (fn phi => [Info (morph_corec_info phi info)])))
  3043   | exprs => (exprs, lthy));
  3044 
  3045 fun corec_info_of res_T lthy =
  3046   (case res_T of
  3047     Type (fpT_name, _) =>
  3048     let
  3049       val (exprs, lthy) = nonempty_corec_info_exprs_of fpT_name lthy;
  3050       val thy = Proof_Context.theory_of lthy;
  3051       val SOME expr =
  3052         find_first ((fn {fpT, ...} => Sign.typ_instance thy (res_T, fpT)) o corec_ad_of_expr) exprs;
  3053       val (info, lthy) = corec_info_of_expr expr lthy;
  3054     in
  3055       (instantiate_corec_info thy res_T info, lthy |> is_Ad expr ? register_corec_info info)
  3056     end
  3057   | _ => not_codatatype lthy res_T);
  3058 
  3059 fun maybe_corec_info_of ctxt res_T =
  3060   (case res_T of
  3061     Type (fpT_name, _) =>
  3062     let
  3063       val thy = Proof_Context.theory_of ctxt;
  3064       val infos = corec_infos_of ctxt fpT_name;
  3065     in
  3066       find_first (fn {fpT, ...} => Sign.typ_instance thy (res_T, fpT)) infos
  3067       |> Option.map (instantiate_corec_info thy res_T)
  3068     end
  3069   | _ => not_codatatype ctxt res_T);
  3070 
  3071 fun prepare_friend_corec friend_name friend_T lthy =
  3072   let
  3073     val (arg_Ts, res_T) = strip_type friend_T;
  3074     val Type (fpT_name, res_Ds) =
  3075       (case res_T of
  3076         T as Type _ => T
  3077       | T => error (not_codatatype lthy T));
  3078 
  3079     val _ = not (null arg_Ts) orelse
  3080       error "Function with no argument cannot be registered as friend";
  3081 
  3082     val {T = Type (fpT_name, fpT_args0), pre_bnf, fp_bnf = live_fp_bnf, fp_res, ...} =
  3083       checked_fp_sugar_of lthy fpT_name;
  3084     val num_fp_tyargs = length fpT_args0;
  3085     val fpT_Ss = map Type.sort_of_atyp fpT_args0;
  3086     val live_fp_alives = liveness_of_fp_bnf num_fp_tyargs live_fp_bnf;
  3087 
  3088     val (old_info as {friend_names = old_friend_names, sig_fp_sugars = old_sig_fp_sugar :: _,
  3089            buffer = old_buffer, ...}, lthy) =
  3090       corec_info_of res_T lthy;
  3091     val old_sig_T_name = fst (dest_Type (#T old_sig_fp_sugar));
  3092     val old_sig_alives = liveness_of_fp_bnf (num_fp_tyargs + 1) (#fp_bnf old_sig_fp_sugar);
  3093 
  3094     (* FIXME: later *)
  3095     val fp_alives = fst (split_last old_sig_alives);
  3096     val fp_alives = map (K false) live_fp_alives;
  3097 
  3098     val _ = not (member (op =) old_friend_names friend_name) orelse
  3099       error ("Function " ^ quote (Syntax.string_of_term lthy (Const (friend_name, friend_T))) ^
  3100         " already registered as friend");
  3101 
  3102     val lthy = lthy |> Variable.declare_typ friend_T;
  3103     val ((Ds, [Y, Z]), _) = lthy
  3104       |> mk_TFrees' fpT_Ss
  3105       ||>> mk_TFrees 2;
  3106 
  3107     (* FIXME *)
  3108     val dead_Ds = Ds;
  3109     val live_As = [Y];
  3110 
  3111     val ctor = mk_ctor res_Ds (the_single (#ctors fp_res));
  3112 
  3113     val fpT0 = Type (fpT_name, Ds);
  3114     val k_Ts0 = map (typ_subst_nonatomic (res_Ds ~~ Ds) o typ_subst_nonatomic [(res_T, Y)]) arg_Ts;
  3115     val k_T0 = mk_tupleT_balanced k_Ts0;
  3116 
  3117     val As = Ds @ [Y];
  3118     val res_As = res_Ds @ [Y];
  3119 
  3120     val k_As = fold Term.add_tfreesT k_Ts0 [];
  3121     val _ = (case filter_out (member (op =) As o TFree) k_As of [] => ()
  3122       | k_A :: _ => error ("Cannot have type variable " ^
  3123           quote (Syntax.string_of_typ lthy (TFree k_A)) ^ " used like that in friend"));
  3124 
  3125     val substDT = Term.typ_subst_atomic (Ds ~~ res_Ds);
  3126 
  3127     val old_sig_T0 = Type (old_sig_T_name, As);
  3128 
  3129     val ((fp_b, version), lthy) = lthy |> get_name_next_version_of fpT_name;
  3130 
  3131     val (((dead_k_bnf, sig_fp_sugar), ssig_fp_sugar), lthy) = lthy
  3132       |> bnf_with_deads_and_lives dead_Ds live_As Y fpT0 k_T0
  3133       ||>> define_sig_type fp_b version fp_alives Ds Y (mk_sumT (old_sig_T0, k_T0))
  3134       ||>> define_ssig_type fp_b version fp_alives Ds Y fpT0;
  3135 
  3136     val _ = live_of_bnf dead_k_bnf = 1 orelse
  3137       error "Impossible type for friend (the result codatatype must occur live in the arguments)";
  3138 
  3139     val (dead_pre_bnf, lthy) = lthy
  3140       |> bnf_kill_all_but 1 pre_bnf;
  3141 
  3142     val sig_fp_ctr_sugar = #fp_ctr_sugar sig_fp_sugar;
  3143     val ssig_fp_ctr_sugar = #fp_ctr_sugar ssig_fp_sugar;
  3144 
  3145     val sig_ctr_sugar = #ctr_sugar sig_fp_ctr_sugar;
  3146     val ssig_ctr_sugar = #ctr_sugar ssig_fp_ctr_sugar;
  3147 
  3148     val ssig_T_name = fst (dest_Type (#T ssig_fp_sugar));
  3149 
  3150     val preT = pre_type_of_ctor Y ctor;
  3151     val old_sig_T = substDT old_sig_T0;
  3152     val k_T = substDT k_T0;
  3153     val ssig_T = Type (ssig_T_name, res_As);
  3154 
  3155     val Sig = mk_ctr res_As (the_single (#ctrs sig_ctr_sugar));
  3156 
  3157     val [Oper, VLeaf, CLeaf] = map (mk_ctr res_As) (#ctrs ssig_ctr_sugar);
  3158     val (ctr_wrapper, friends) =
  3159       mk_ctr_wrapper_friends lthy friend_name friend_T old_sig_T k_T Sig old_buffer;
  3160 
  3161     val buffer =
  3162       {Oper = Oper, VLeaf = VLeaf, CLeaf = CLeaf, ctr_wrapper = ctr_wrapper, friends = friends};
  3163   in
  3164     ((old_info, fp_b, version, Y, Z, preT, k_T, ssig_T, dead_pre_bnf, dead_k_bnf, sig_fp_sugar,
  3165       ssig_fp_sugar, buffer), lthy)
  3166   end;
  3167 
  3168 fun register_friend_corec key fp_b version Y Z k_T dead_k_bnf sig_fp_sugar ssig_fp_sugar
  3169     friend_const rho rho_transfer old_info lthy =
  3170   let
  3171     val friend_T = fastype_of friend_const;
  3172     val res_T = body_type friend_T;
  3173   in
  3174     derive_corecUU_step res_T old_info key friend_T fp_b version Y Z k_T dead_k_bnf sig_fp_sugar
  3175       ssig_fp_sugar rho rho_transfer lthy
  3176     |> (fn ((info, friend_info), lthy) => (friend_info, register_corec_info info lthy))
  3177   end;
  3178 
  3179 fun merge_corec_info_exprss exprs1 exprs2 lthy =
  3180   let
  3181     fun all_friend_names_of exprs =
  3182       fold (union (op =)) (map (#friend_names o corec_ad_of_expr) exprs) [];
  3183 
  3184     val friend_names1 = all_friend_names_of exprs1;
  3185     val friend_names2 = all_friend_names_of exprs2;
  3186   in
  3187     if subset (op =) (friend_names2, friend_names1) then
  3188       if subset (op =) (friend_names1, friend_names2) andalso
  3189          length (filter is_Info exprs2) > length (filter is_Info exprs1) then
  3190         (exprs2, lthy)
  3191       else
  3192         (exprs1, lthy)
  3193     else if subset (op =) (friend_names1, friend_names2) then
  3194       (exprs2, lthy)
  3195     else
  3196       fold_rev (uncurry o insert_corec_info_expr) exprs2 (exprs1, lthy)
  3197   end;
  3198 
  3199 fun merge_corec_info_tabs info_tab1 info_tab2 lthy =
  3200   let
  3201     val fpT_names = union (op =) (Symtab.keys info_tab1) (Symtab.keys info_tab2);
  3202 
  3203     fun add_infos_of fpT_name (info_tab, lthy) =
  3204       (case Symtab.lookup info_tab1 fpT_name of
  3205         NONE =>
  3206         (Symtab.update_new (fpT_name, the (Symtab.lookup info_tab2 fpT_name)) info_tab, lthy)
  3207       | SOME exprs1 =>
  3208         (case Symtab.lookup info_tab2 fpT_name of
  3209           NONE => (Symtab.update_new (fpT_name, exprs1) info_tab, lthy)
  3210         | SOME exprs2 =>
  3211           let val (exprs, lthy) = merge_corec_info_exprss exprs1 exprs2 lthy in
  3212             (Symtab.update_new (fpT_name, exprs) info_tab, lthy)
  3213           end));
  3214   in
  3215     fold add_infos_of fpT_names (Symtab.empty, lthy)
  3216   end;
  3217 
  3218 fun consolidate lthy =
  3219   (case snd (Data.get (Context.Proof lthy)) of
  3220     [_] => raise Same.SAME
  3221   | info_tab :: info_tabs =>
  3222     let
  3223       val (info_tab', lthy) = fold_rev (uncurry o merge_corec_info_tabs) info_tabs (info_tab, lthy);
  3224     in
  3225       Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
  3226           Data.map (apsnd (fn _ => [Symtab.map (K (map (morph_corec_info_expr phi))) info_tab'])))
  3227         lthy
  3228     end);
  3229 
  3230 fun consolidate_global thy =
  3231   SOME (Named_Target.theory_map consolidate thy)
  3232   handle Same.SAME => NONE;
  3233 
  3234 val _ = Theory.setup (Theory.at_begin consolidate_global);
  3235 
  3236 end;