Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bnf_gfp_grec.ML   Sprache: SML

Original von: Isabelle©

(*  Title:      HOL/Tools/BNF/bnf_gfp_grec.ML
    Author:     Jasmin Blanchette, Inria, LORIA, MPII
    Author:     Aymeric Bouzy, Ecole polytechnique
    Author:     Dmitriy Traytel, ETH Zürich
    Copyright   2015, 2016

Generalized corecursor construction.
*)


signature BNF_GFP_GREC =
sig
  val Tsubst: typ -> typ -> typ -> typ
  val substT: typ -> typ -> term -> term
  val freeze_types: Proof.context -> (indexname * sort) list -> typ list -> typ list
  val dummify_atomic_types: term -> term
  val define_const: bool -> binding -> int -> string -> term -> local_theory ->
    (term * thm) * local_theory

  type buffer =
    {Oper: term,
     VLeaf: term,
     CLeaf: term,
     ctr_wrapper: term,
     friends: (typ * term) Symtab.table}

  val map_buffer: (term -> term) -> buffer -> buffer
  val specialize_buffer_types: buffer -> buffer

  type dtor_coinduct_info =
    {dtor_coinduct: thm,
     cong_def: thm,
     cong_locale: thm,
     cong_base: thm,
     cong_refl: thm,
     cong_sym: thm,
     cong_trans: thm,
     cong_alg_intros: thm list}

  type corec_info =
    {fp_b: binding,
     version: int,
     fpT: typ,
     Y: typ,
     Z: typ,
     friend_names: string list,
     sig_fp_sugars: BNF_FP_Def_Sugar.fp_sugar list,
     ssig_fp_sugar: BNF_FP_Def_Sugar.fp_sugar,
     Lam: term,
     proto_sctr: term,
     flat: term,
     eval_core: term,
     eval: term,
     algLam: term,
     corecUU: term,
     dtor_transfer: thm,
     Lam_transfer: thm,
     Lam_pointful_natural: thm,
     proto_sctr_transfer: thm,
     flat_simps: thm list,
     eval_core_simps: thm list,
     eval_thm: thm,
     eval_simps: thm list,
     all_algLam_algs: thm list,
     algLam_thm: thm,
     dtor_algLam: thm,
     corecUU_thm: thm,
     corecUU_unique: thm,
     corecUU_transfer: thm,
     buffer: buffer,
     all_dead_k_bnfs: BNF_Def.bnf list,
     Retr: term,
     equivp_Retr: thm,
     Retr_coinduct: thm,
     dtor_coinduct_info: dtor_coinduct_info}

  type friend_info =
    {algrho: term,
     dtor_algrho: thm,
     algLam_algrho: thm}

  val not_codatatype: Proof.context -> typ -> 'a
  val mk_fp_binding: binding -> string -> binding
  val bnf_kill_all_but: int -> BNF_Def.bnf -> local_theory -> BNF_Def.bnf * local_theory

  val print_corec_infos: Proof.context -> unit
  val has_no_corec_info: Proof.context -> string -> bool
  val corec_info_of: typ -> local_theory -> corec_info * local_theory
  val maybe_corec_info_of: Proof.context -> typ -> corec_info option
  val corec_infos_of: Proof.context -> string -> corec_info list
  val corec_infos_of_generic: Context.generic -> Symtab.key -> corec_info list
  val prepare_friend_corec: string -> typ -> local_theory ->
    (corec_info * binding * int * typ * typ * typ * typ * typ * BNF_Def.bnf * BNF_Def.bnf
     * BNF_FP_Def_Sugar.fp_sugar * BNF_FP_Def_Sugar.fp_sugar * buffer) * local_theory
  val register_friend_corec: string -> binding -> int -> typ -> typ -> typ -> BNF_Def.bnf ->
    BNF_FP_Def_Sugar.fp_sugar -> BNF_FP_Def_Sugar.fp_sugar -> term -> term -> thm -> corec_info ->
    local_theory -> friend_info * local_theory
end;

structure BNF_GFP_Grec : BNF_GFP_GREC =
struct

open Ctr_Sugar
open BNF_Util
open BNF_Def
open BNF_Comp
open BNF_FP_Util
open BNF_LFP
open BNF_FP_Def_Sugar
open BNF_LFP_Rec_Sugar
open BNF_GFP_Grec_Tactics

val algLamN = "algLam";
val algLam_algLamN = "algLam_algLam";
val algLam_algrhoN = "algLam_algrho";
val algrhoN = "algrho";
val CLeafN = "CLeaf";
val congN = "congclp";
val cong_alg_introsN = "cong_alg_intros";
val cong_localeN = "cong_locale";
val corecUUN = "corecUU";
val corecUU_transferN = "corecUU_transfer";
val corecUU_uniqueN = "corecUU_unique";
val cutSsigN = "cutSsig";
val dtor_algLamN = "dtor_algLam";
val dtor_algrhoN = "dtor_algrho";
val dtor_coinductN = "dtor_coinduct";
val dtor_transferN = "dtor_transfer";
val embLN = "embL";
val embLLN = "embLL";
val embLRN = "embLR";
val embL_pointful_naturalN = "embL_pointful_natural";
val embL_transferN = "embL_transfer";
val equivp_RetrN = "equivp_Retr";
val evalN = "eval";
val eval_coreN = "eval_core";
val eval_core_pointful_naturalN = "eval_core_pointful_natural";
val eval_core_transferN = "eval_core_transfer";
val eval_flatN = "eval_flat";
val eval_simpsN = "eval_simps";
val flatN = "flat";
val flat_pointful_naturalN = "flat_pointful_natural";
val flat_transferN = "flat_transfer";
val k_as_ssig_naturalN = "k_as_ssig_natural";
val k_as_ssig_transferN = "k_as_ssig_transfer";
val LamN = "Lam";
val Lam_transferN = "Lam_transfer";
val Lam_pointful_naturalN = "Lam_pointful_natural";
val OperN = "Oper";
val proto_sctrN = "proto_sctr";
val proto_sctr_pointful_naturalN = "proto_sctr_pointful_natural";
val proto_sctr_transferN = "proto_sctr_transfer";
val rho_transferN = "rho_transfer";
val Retr_coinductN = "Retr_coinduct";
val sctrN = "sctr";
val sctr_transferN = "sctr_transfer";
val sctr_pointful_naturalN = "sctr_pointful_natural";
val sigN = "sig";
val SigN = "Sig";
val Sig_pointful_naturalN = "Sig_pointful_natural";
val corecUN = "corecU";
val corecU_ctorN = "corecU_ctor";
val corecU_uniqueN = "corecU_unique";
val unsigN = "unsig";
val VLeafN = "VLeaf";

val s_prefix = "s"(* transforms "sig" into "ssig" *)

fun not_codatatype ctxt T =
  error ("Not a codatatype: " ^ Syntax.string_of_typ ctxt T);
fun mutual_codatatype () =
  error ("Mutually corecursive codatatypes are not supported (try " ^
    quote (#1 \<^command_keyword>\<open>primcorec\<close>) ^ " instead of " ^
    quote (#1 \<^command_keyword>\<open>corec\<close>) ^ ")");
fun noncorecursive_codatatype () =
  error ("Noncorecursive codatatypes are not supported (try " ^
    quote (#1 \<^command_keyword>\<open>definition\<close>) ^ " instead of " ^
    quote (#1 \<^command_keyword>\<open>corec\<close>) ^ ")");
fun singleton_codatatype ctxt =
  error ("Singleton corecursive codatatypes are not supported (use " ^
    quote (Syntax.string_of_typ ctxt \<^typ>\<open>unit\<close>) ^ " instead)");

fun merge_lists eq old1 old2 = (old1 |> subtract eq old2) @ old2;

fun add_type_namesT (Type (s, Ts)) = insert (op =) s #> fold add_type_namesT Ts
  | add_type_namesT _ = I;

fun Tsubst Y T = Term.typ_subst_atomic [(Y, T)];
fun substT Y T = Term.subst_atomic_types [(Y, T)];

fun freeze_types ctxt except_tvars Ts =
  let
    val As = fold Term.add_tvarsT Ts [] |> subtract (op =) except_tvars;
    val (Bs, _) = ctxt |> mk_TFrees' (map snd As);
  in
    map (Term.typ_subst_TVars (map fst As ~~ Bs)) Ts
  end;

fun typ_unify_disjointly thy (T, T') =
  if T = T' then
    T
  else
    let
      val tvars = Term.add_tvar_namesT T [];
      val tvars' = Term.add_tvar_namesT T' [];
      val maxidx' = maxidx_of_typ T';
      val T = T |> exists (member (op =) tvars') tvars ? Logic.incr_tvar (maxidx' + 1);
      val maxidx = Integer.max (maxidx_of_typ T) maxidx';
      val (tyenv, _) = Sign.typ_unify thy (T, T') (Vartab.empty, maxidx);
    in
      Envir.subst_type tyenv T
    end;

val dummify_atomic_types = Term.map_types (Term.map_atyps (K Term.dummyT));

fun mk_internal internal ctxt f =
  if internal andalso not (Config.get ctxt bnf_internals) then f else I
fun mk_fp_binding fp_b pre = Binding.map_name (K pre) fp_b
  |> Binding.qualify true (Binding.name_of fp_b);
fun mk_version_binding version = Binding.qualify false ("v" ^ string_of_int version);
fun mk_version_fp_binding internal ctxt =
  mk_internal internal ctxt Binding.concealed ooo (mk_fp_binding oo mk_version_binding);
(*FIXME: get rid of ugly names when typedef and primrec respect qualification*)
fun mk_version_binding_ugly version = Binding.suffix_name ("_v" ^ string_of_int version);
fun mk_version_fp_binding_ugly internal ctxt version fp_b pre =
  Binding.prefix_name (pre ^ "_") fp_b
  |> mk_version_binding_ugly version
  |> mk_internal internal ctxt Binding.concealed;

fun mk_mapN ctxt live_AsBs TA bnf =
  let val TB = Term.typ_subst_atomic live_AsBs TA in
    enforce_type ctxt (snd o strip_typeN (length live_AsBs)) (TA --> TB) (map_of_bnf bnf)
  end;

fun mk_relN ctxt live_AsBs TA bnf =
  let val TB = Term.typ_subst_atomic live_AsBs TA in
    enforce_type ctxt (snd o strip_typeN (length live_AsBs)) (mk_pred2T TA TB) (rel_of_bnf bnf)
  end;

fun mk_map1 ctxt Y Z = mk_mapN ctxt [(Y, Z)];
fun mk_rel1 ctxt Y Z = mk_relN ctxt [(Y, Z)];

fun define_const internal fp_b version name rhs lthy =
  let
    val b = mk_version_fp_binding internal lthy version fp_b name;

    val ((free, (_, def_free)), (lthy, lthy_old)) = lthy
      |> (snd o Local_Theory.begin_nested)
      |> Local_Theory.define ((b, NoSyn), ((Thm.def_binding b |> Binding.concealed, []), rhs))
      ||> `Local_Theory.end_nested;

    val phi = Proof_Context.export_morphism lthy_old lthy;

    val const = Morphism.term phi free;
    val const' = enforce_type lthy I (fastype_of free) const;
  in
    ((const', Morphism.thm phi def_free), lthy)
  end;

fun define_single_primrec b eqs lthy =
  let
    val (([free], [def_free], [simps_free]), (lthy, lthy_old)) = lthy
      |> (snd o Local_Theory.begin_nested)
      |> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed) (*TODO check*)
      |> primrec false [] [(b, NONE, NoSyn)] (map (fn eq => ((Binding.empty_atts, eq), [], [])) eqs)
      ||> `Local_Theory.end_nested;

    val phi = Proof_Context.export_morphism lthy_old lthy;

    val const = Morphism.term phi free;
    val const' = enforce_type lthy I (fastype_of free) const;
  in
    ((const', Morphism.thm phi def_free, map (Morphism.thm phi) simps_free), lthy)
  end;

type buffer =
  {Oper: term,
   VLeaf: term,
   CLeaf: term,
   ctr_wrapper: term,
   friends: (typ * term) Symtab.table};

fun map_buffer f {Oper, VLeaf, CLeaf, ctr_wrapper, friends} =
  {Oper = f Oper, VLeaf = f VLeaf, CLeaf = f CLeaf, ctr_wrapper = f ctr_wrapper,
   friends = Symtab.map (K (apsnd f)) friends};

fun morph_buffer phi = map_buffer (Morphism.term phi);

fun specialize_buffer_types {Oper, VLeaf, CLeaf, ctr_wrapper, friends} =
  let
    val ssig_T as Type (_, Ts) = body_type (fastype_of VLeaf);
    val Y = List.last Ts;
    val ssigifyT = substT Y ssig_T;
  in
    {Oper = Oper, VLeaf = VLeaf, CLeaf = CLeaf, ctr_wrapper = ssigifyT ctr_wrapper,
     friends = Symtab.map (K (apsnd ssigifyT)) friends}
  end;

type dtor_coinduct_info =
  {dtor_coinduct: thm,
   cong_def: thm,
   cong_locale: thm,
   cong_base: thm,
   cong_refl: thm,
   cong_sym: thm,
   cong_trans: thm,
   cong_alg_intros: thm list};

fun map_dtor_coinduct_info f {dtor_coinduct, cong_def, cong_locale, cong_base, cong_refl, cong_sym,
    cong_trans, cong_alg_intros} =
  {dtor_coinduct = f dtor_coinduct, cong_def = f cong_def, cong_locale = f cong_locale,
   cong_base = f cong_base, cong_refl = f cong_refl, cong_sym = f cong_sym,
   cong_trans = f cong_trans, cong_alg_intros = map f cong_alg_intros};

fun morph_dtor_coinduct_info phi = map_dtor_coinduct_info (Morphism.thm phi);

type corec_ad =
  {fpT: typ,
   friend_names: string list};

fun morph_corec_ad phi {fpT, friend_names} =
  {fpT = Morphism.typ phi fpT, friend_names = friend_names};

type corec_info =
  {fp_b: binding,
   version: int,
   fpT: typ,
   Y: typ,
   Z: typ,
   friend_names: string list,
   sig_fp_sugars: fp_sugar list,
   ssig_fp_sugar: fp_sugar,
   Lam: term,
   proto_sctr: term,
   flat: term,
   eval_core: term,
   eval: term,
   algLam: term,
   corecUU: term,
   dtor_transfer: thm,
   Lam_transfer: thm,
   Lam_pointful_natural: thm,
   proto_sctr_transfer: thm,
   flat_simps: thm list,
   eval_core_simps: thm list,
   eval_thm: thm,
   eval_simps: thm list,
   all_algLam_algs: thm list,
   algLam_thm: thm,
   dtor_algLam: thm,
   corecUU_thm: thm,
   corecUU_unique: thm,
   corecUU_transfer: thm,
   buffer: buffer,
   all_dead_k_bnfs: bnf list,
   Retr: term,
   equivp_Retr: thm,
   Retr_coinduct: thm,
   dtor_coinduct_info: dtor_coinduct_info};

fun morph_corec_info phi
    ({fp_b, version, fpT, Y, Z, friend_names, sig_fp_sugars, ssig_fp_sugar, Lam, proto_sctr, flat,
      eval_core, eval, algLam, corecUU, dtor_transfer, Lam_transfer, Lam_pointful_natural,
      proto_sctr_transfer, flat_simps, eval_core_simps, eval_thm, eval_simps, all_algLam_algs,
      algLam_thm, dtor_algLam, corecUU_thm, corecUU_unique, corecUU_transfer, buffer,
      all_dead_k_bnfs, Retr, equivp_Retr, Retr_coinduct, dtor_coinduct_info} : corec_info) =
  {fp_b = fp_b, version = version, fpT = Morphism.typ phi fpT, Y = Morphism.typ phi Y,
   Z = Morphism.typ phi Z, friend_names = friend_names, sig_fp_sugars = sig_fp_sugars (*no morph*),
   ssig_fp_sugar = ssig_fp_sugar (*no morph*), Lam = Morphism.term phi Lam,
   proto_sctr = Morphism.term phi proto_sctr, flat = Morphism.term phi flat,
   eval_core = Morphism.term phi eval_core, eval = Morphism.term phi eval,
   algLam = Morphism.term phi algLam, corecUU = Morphism.term phi corecUU,
   dtor_transfer = dtor_transfer, Lam_transfer = Morphism.thm phi Lam_transfer,
   Lam_pointful_natural = Morphism.thm phi Lam_pointful_natural,
   proto_sctr_transfer = Morphism.thm phi proto_sctr_transfer,
   flat_simps = map (Morphism.thm phi) flat_simps,
   eval_core_simps = map (Morphism.thm phi) eval_core_simps, eval_thm = Morphism.thm phi eval_thm,
   eval_simps = map (Morphism.thm phi) eval_simps,
   all_algLam_algs = map (Morphism.thm phi) all_algLam_algs,
   algLam_thm = Morphism.thm phi algLam_thm, dtor_algLam = Morphism.thm phi dtor_algLam,
   corecUU_thm = Morphism.thm phi corecUU_thm, corecUU_unique = Morphism.thm phi corecUU_unique,
   corecUU_transfer = Morphism.thm phi corecUU_transfer, buffer = morph_buffer phi buffer,
   all_dead_k_bnfs = map (morph_bnf phi) all_dead_k_bnfs, Retr = Morphism.term phi Retr,
   equivp_Retr = Morphism.thm phi equivp_Retr, Retr_coinduct = Morphism.thm phi Retr_coinduct,
   dtor_coinduct_info = morph_dtor_coinduct_info phi dtor_coinduct_info};

datatype ('a, 'b) expr =
  Ad of 'a * (local_theory -> 'b * local_theory) |
  Info of 'b;

fun is_Ad (Ad _) = true
  | is_Ad _ = false;

fun is_Info (Info _) = true
  | is_Info _ = false;

type corec_info_expr = (corec_ad, corec_info) expr;

fun morph_corec_info_expr phi (Ad (ad, f)) = Ad (morph_corec_ad phi ad, f)
  | morph_corec_info_expr phi (Info info) = Info (morph_corec_info phi info);

val transfer_corec_info_expr = morph_corec_info_expr o Morphism.transfer_morphism;

type corec_data = int Symtab.table * corec_info_expr list Symtab.table list;

structure Data = Generic_Data
(
  type T = corec_data;
  val empty = (Symtab.empty, [Symtab.empty]);
  val extend = I;
  fun merge ((version_tab1, info_tabs1), (version_tab2, info_tabs2)) : T =
    (Symtab.join (K Int.max) (version_tab1, version_tab2), info_tabs1 @ info_tabs2);
);

fun corec_ad_of_expr (Ad (ad, _)) = ad
  | corec_ad_of_expr (Info {fpT, friend_names, ...}) = {fpT = fpT, friend_names = friend_names};

fun corec_info_exprs_of_generic context fpT_name =
  let
    val thy = Context.theory_of context;
    val info_tabs = snd (Data.get context);
  in
    maps (fn info_tab => these (Symtab.lookup info_tab fpT_name)) info_tabs
    |> map (transfer_corec_info_expr thy)
  end;

val corec_info_exprs_of = corec_info_exprs_of_generic o Context.Proof;

val keep_corec_infos = map_filter (fn Ad _ => NONE | Info info => SOME info);

val corec_infos_of_generic = keep_corec_infos oo corec_info_exprs_of_generic;
val corec_infos_of = keep_corec_infos oo corec_info_exprs_of;

fun str_of_corec_ad ctxt {fpT, friend_names} =
  "[" ^ Syntax.string_of_typ ctxt fpT ^ "; " ^ commas friend_names ^ "]";

fun str_of_corec_info ctxt {fpT, version, friend_names, ...} =
  "{" ^ Syntax.string_of_typ ctxt fpT ^ "; " ^ commas friend_names ^ "; v" ^ string_of_int version ^
  "}";

fun str_of_corec_info_expr ctxt (Ad (ad, _)) = str_of_corec_ad ctxt ad
  | str_of_corec_info_expr ctxt (Info info) = str_of_corec_info ctxt info;

fun print_corec_infos ctxt =
  Symtab.fold (fn (fpT_name, exprs) => fn () =>
      writeln (fpT_name ^ ":\n" ^
        cat_lines (map (prefix " " o str_of_corec_info_expr ctxt) exprs)))
    (the_single (snd (Data.get (Context.Proof ctxt)))) ();

val has_no_corec_info = null oo corec_info_exprs_of;

fun get_name_next_version_of fpT_name ctxt =
  let
    val (version_tab, info_tabs) = Data.get (Context.Theory (Proof_Context.theory_of ctxt));
    val fp_base = Long_Name.base_name fpT_name;
    val fp_b = Binding.name fp_base;
    val version_tab' = Symtab.map_default (fp_base, ~1) (Integer.add 1) version_tab;
    val SOME version = Symtab.lookup version_tab' fp_base;
    val ctxt' = ctxt
      |> Local_Theory.background_theory (Context.theory_map (Data.put (version_tab', info_tabs)));
  in
    ((fp_b, version), ctxt')
  end;

type friend_info =
  {algrho: term,
   dtor_algrho: thm,
   algLam_algrho: thm};

fun morph_friend_info phi ({algrho, dtor_algrho, algLam_algrho} : friend_info) =
  {algrho = Morphism.term phi algrho, dtor_algrho = Morphism.thm phi dtor_algrho,
   algLam_algrho = Morphism.thm phi algLam_algrho};

fun checked_fp_sugar_of ctxt fpT_name =
  let
    val fp_sugar as {X, fp_res = {Ts = fpTs, ...}, fp_ctr_sugar = {ctrXs_Tss, ...}, ...} =
      (case fp_sugar_of ctxt fpT_name of
        SOME (fp_sugar as {fp = Greatest_FP, ...}) => fp_sugar
      | _ => not_codatatype ctxt (Type (fpT_name, [] (*yuck*))));

    val _ =
      if length fpTs > 1 then
        mutual_codatatype ()
      else if not (exists (exists (Term.exists_subtype (curry (op =) X))) ctrXs_Tss) then
        noncorecursive_codatatype ()
      else if ctrXs_Tss = [[X]] then
        singleton_codatatype ctxt
      else
        ();
  in
    fp_sugar
  end;

fun bnf_kill_all_but nn bnf lthy =
  ((empty_comp_cache, empty_unfolds), lthy)
  |> kill_bnf I (live_of_bnf bnf - nn) bnf
  ||> snd;

fun bnf_with_deads_and_lives dead_Es live_As Y fpT T lthy =
   let
     val qsoty = quote o Syntax.string_of_typ lthy;

     val unfreeze_fp = Tsubst Y fpT;

    fun flatten_tyargs Ass =
      map dest_TFree live_As
      |> filter (fn T => exists (fn Ts => member (op =) Ts T) Ass);

    val ((bnf, _), (_, lthy)) =
      bnf_of_typ false Do_Inline I flatten_tyargs [Term.dest_TFree Y] (map Term.dest_TFree dead_Es)
        T ((empty_comp_cache, empty_unfolds), lthy)
      handle BAD_DEAD (Y, Y_backdrop) =>
        (case Y_backdrop of
          Type (bad_tc, _) =>
          let
            val T = qsoty (unfreeze_fp Y);
            val T_backdrop = qsoty (unfreeze_fp Y_backdrop);
            fun register_hint () =
              "\nUse the " ^ quote (#1 \<^command_keyword>\<open>bnf\<close>) ^ " command to register " ^
              quote bad_tc ^ " as a bounded natural functor to allow nested (co)recursion through \
              \it";
          in
            if is_some (bnf_of lthy bad_tc) orelse is_some (fp_sugar_of lthy bad_tc) then
              error ("Inadmissible occurrence of type " ^ T ^ " in type expression " ^
                T_backdrop)
            else
              error ("Unsupported occurrence of type " ^ T ^ " via type constructor " ^
                quote bad_tc ^ " in type expression " ^ T_backdrop ^ register_hint ())
          end);

    val phi =
      Morphism.term_morphism "BNF" (Raw_Simplifier.rewrite_term (Proof_Context.theory_of lthy)
        @{thms BNF_Composition.id_bnf_def} [])
      $> Morphism.thm_morphism "BNF" (unfold_thms lthy @{thms BNF_Composition.id_bnf_def});
  in
    (morph_bnf phi bnf, lthy)
  end;

fun define_sig_type fp_b version fp_alives Es Y rhsT lthy =
  let
    val T_b = mk_version_fp_binding_ugly true lthy version fp_b sigN;
    val ctr_b = mk_version_fp_binding false lthy version fp_b SigN;
    val sel_b = mk_version_fp_binding true lthy version fp_b unsigN;

    val lthy = (snd o Local_Theory.begin_nested) lthy;

    val T_name = Local_Theory.full_name lthy T_b;

    val tyargs = map2 (fn alive => fn T =>
        (if alive then SOME Binding.empty else NONE, (T, Type.sort_of_atyp T)))
      (fp_alives @ [true]) (Es @ [Y]);
    val ctr_specs = [(((Binding.empty, ctr_b), [(sel_b, rhsT)]), NoSyn)];
    val spec = (((((tyargs, T_b), NoSyn), ctr_specs),
      (Binding.empty, Binding.empty, Binding.empty)), []);

    val plugins = Plugin_Name.make_filter lthy (K (curry (op =) transfer_plugin));
    val discs_sels = true;

    val lthy = lthy
      |> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed) (*TODO check*)
      |> with_typedef_threshold ~1
        (co_datatypes Least_FP construct_lfp ((plugins, discs_sels), [spec]))
      |> Local_Theory.end_nested;

    val SOME fp_sugar = fp_sugar_of lthy T_name;
  in
    (fp_sugar, lthy)
  end;

fun define_ssig_type fp_b version fp_alives Es Y fpT lthy =
  let
    val sig_T_b = mk_version_fp_binding_ugly true lthy version fp_b sigN;
    val T_b = Binding.prefix_name s_prefix sig_T_b;
    val Oper_b = mk_version_fp_binding false lthy version fp_b OperN;
    val VLeaf_b = mk_version_fp_binding false lthy version fp_b VLeafN;
    val CLeaf_b = mk_version_fp_binding false lthy version fp_b CLeafN;

    val lthy = (snd o Local_Theory.begin_nested) lthy;

    val sig_T_name = Local_Theory.full_name lthy sig_T_b;
    val T_name = Long_Name.map_base_name (prefix s_prefix) sig_T_name;

    val As = Es @ [Y];
    val ssig_sig_T = Type (sig_T_name, Es @ [Type (T_name, As)]);

    val tyargs = map2 (fn alive => fn T =>
        (if alive then SOME Binding.empty else NONE, (T, Type.sort_of_atyp T)))
      (fp_alives @ [true]) (Es @ [Y]);
    val ctr_specs =
      [(((Binding.empty, Oper_b), [(Binding.empty, ssig_sig_T)]), NoSyn),
       (((Binding.empty, VLeaf_b), [(Binding.empty, Y)]), NoSyn),
       (((Binding.empty, CLeaf_b), [(Binding.empty, fpT)]), NoSyn)];
    val spec = (((((tyargs, T_b), NoSyn), ctr_specs),
      (Binding.empty, Binding.empty, Binding.empty)), []);

    val plugins = Plugin_Name.make_filter lthy (K (curry (op =) transfer_plugin));
    val discs_sels = false;

    val lthy = lthy
      |> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed) (*TODO check*)
      |> with_typedef_threshold ~1
        (co_datatypes Least_FP construct_lfp ((plugins, discs_sels), [spec]))
      |> Local_Theory.end_nested;

    val SOME fp_sugar = fp_sugar_of lthy T_name;
  in
    (fp_sugar, lthy)
  end;

fun embed_Sig ctxt Sig inl_or_r t =
  Library.foldl1 HOLogic.mk_comp [Sig, inl_or_r, dummify_atomic_types t]
  |> Syntax.check_term ctxt;

fun mk_ctr_wrapper_friends ctxt friend_name friend_T old_sig_T k_T Sig old_buffer =
  let
    val embed_Sig_inl = embed_Sig ctxt Sig (Inl_const old_sig_T k_T);

    val ctr_wrapper = embed_Sig_inl (#ctr_wrapper old_buffer);
    val friends = Symtab.map (K (apsnd embed_Sig_inl)) (#friends old_buffer)
      |> Symtab.update_new (friend_name, (friend_T,
        HOLogic.mk_comp (Sig, Inr_const old_sig_T k_T)));
  in
    (ctr_wrapper, friends)
  end;

fun pre_type_of_ctor Y ctor =
  let
    val (fp_preT, fpT) = dest_funT (fastype_of ctor);
  in
    typ_subst_nonatomic [(fpT, Y)] fp_preT
  end;

fun mk_k_as_ssig Z old_sig_T k_T ssig_T Sig dead_sig_map Oper VLeaf =
  let
    val inr' = Inr_const old_sig_T k_T;
    val dead_sig_map' = substT Z ssig_T dead_sig_map;
  in
    Library.foldl1 HOLogic.mk_comp [Oper, dead_sig_map' $ VLeaf, Sig, inr']
  end;

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
    dead_old_sig_map Sig old_Oper old_VLeaf old_CLeaf Oper VLeaf CLeaf lthy =
  let
    val embL_b = mk_version_fp_binding true lthy version fp_b name;
    val old_ssig_old_sig_T = Tsubst Y old_ssig_T old_sig_T;
    val ssig_old_sig_T = Tsubst Y ssig_T old_sig_T;
    val ssig_other_summand_T = Tsubst Y ssig_T other_summand_T;

    val sigx = Var (("s", 0), old_ssig_old_sig_T);
    val x = Var (("x", 0), Y);
    val j = Var (("j", 0), fpT);
    val embL = Free (Binding.name_of embL_b, old_ssig_T --> ssig_T);
    val dead_old_sig_map' = Term.subst_atomic_types [(Y, old_ssig_T), (Z, ssig_T)] dead_old_sig_map;
    val Sig' = substT Y ssig_T Sig;
    val inl' = Inl_or_r_const ssig_old_sig_T ssig_other_summand_T;

    val Oper_eq = mk_Trueprop_eq (embL $ (old_Oper $ sigx),
        Oper $ (Sig' $ (inl' $ (dead_old_sig_map' $ embL $ sigx))))
      |> Logic.all sigx;
    val VLeaf_eq = mk_Trueprop_eq (embL $ (old_VLeaf $ x), VLeaf $ x)
      |> Logic.all x;
    val CLeaf_eq = mk_Trueprop_eq (embL $ (old_CLeaf $ j), CLeaf $ j)
      |> Logic.all j;
  in
    define_single_primrec embL_b [Oper_eq, VLeaf_eq, CLeaf_eq] lthy
  end;

fun define_Lam_base fp_b version Y Z preT ssig_T dead_pre_map Sig unsig dead_sig_map Oper VLeaf
    lthy =
  let
    val YpreT = HOLogic.mk_prodT (Y, preT);

    val snd' = snd_const YpreT;
    val dead_pre_map' = substT Z ssig_T dead_pre_map;
    val Sig' = substT Y ssig_T Sig;
    val unsig' = substT Y ssig_T unsig;
    val dead_sig_map' = Term.subst_atomic_types [(Y, YpreT), (Z, ssig_T)] dead_sig_map;

    val rhs = HOLogic.mk_comp (unsig', dead_sig_map'
      $ Library.foldl1 HOLogic.mk_comp [Oper, Sig', dead_pre_map' $ VLeaf, snd']);
  in
    define_const true fp_b version LamN rhs lthy
  end;

fun define_Lam_step_or_merge fp_b version Y preT unsig left_case right_case lthy =
  let
    val YpreT = HOLogic.mk_prodT (Y, preT);

    val unsig' = substT Y YpreT unsig;

    val rhs = HOLogic.mk_comp (mk_case_sum (left_case, right_case), unsig');
  in
    define_const true fp_b version LamN rhs lthy
  end;

fun define_Lam_step fp_b version Y Z preT old_ssig_T ssig_T dead_pre_map unsig rho embL old_Lam
    lthy =
  let
    val dead_pre_map' = Term.subst_atomic_types [(Y, old_ssig_T), (Z, ssig_T)] dead_pre_map;
    val left_case = HOLogic.mk_comp (dead_pre_map' $ embL, old_Lam);
  in
    define_Lam_step_or_merge fp_b version Y preT unsig left_case rho lthy
  end;

fun define_Lam_merge fp_b version Y Z preT old1_ssig_T old2_ssig_T ssig_T dead_pre_map unsig embLL
    embLR old1_Lam old2_Lam lthy =
  let
    val dead_pre_map' = Term.subst_atomic_types [(Y, old1_ssig_T), (Z, ssig_T)] dead_pre_map;
    val dead_pre_map'' = Term.subst_atomic_types [(Y, old2_ssig_T), (Z, ssig_T)] dead_pre_map;
    val left_case = HOLogic.mk_comp (dead_pre_map' $ embLL, old1_Lam);
    val right_case = HOLogic.mk_comp (dead_pre_map'' $ embLR, old2_Lam);
  in
    define_Lam_step_or_merge fp_b version Y preT unsig left_case right_case lthy
  end;

fun define_proto_sctr_step_or_merge fp_b version old_sig_T right_T Sig old_proto_sctr =
  let
    val rhs = Library.foldl1 HOLogic.mk_comp [Sig, Inl_const old_sig_T right_T, old_proto_sctr];
  in
    define_const true fp_b version proto_sctrN rhs
  end;

fun define_flat fp_b version Y Z fpT sig_T ssig_T Oper VLeaf CLeaf dead_sig_map lthy =
  let
    val flat_b = mk_version_fp_binding true lthy version fp_b flatN;
    val ssig_sig_T = Tsubst Y ssig_T sig_T;
    val ssig_ssig_sig_T = Tsubst Y ssig_T ssig_sig_T;
    val ssig_ssig_T = Tsubst Y ssig_T ssig_T;

    val sigx = Var (("s", 0), ssig_ssig_sig_T);
    val x = Var (("x", 0), ssig_T);
    val j = Var (("j", 0), fpT);
    val flat = Free (Binding.name_of flat_b, ssig_ssig_T --> ssig_T);
    val Oper' = substT Y ssig_T Oper;
    val VLeaf' = substT Y ssig_T VLeaf;
    val CLeaf' = substT Y ssig_T CLeaf;
    val dead_sig_map' = Term.subst_atomic_types [(Y, ssig_ssig_T), (Z, ssig_T)] dead_sig_map;

    val Oper_eq = mk_Trueprop_eq (flat $ (Oper' $ sigx), Oper $ (dead_sig_map' $ flat $ sigx))
      |> Logic.all sigx;
    val VLeaf_eq = mk_Trueprop_eq (flat $ (VLeaf' $ x), x)
      |> Logic.all x;
    val CLeaf_eq = mk_Trueprop_eq (flat $ (CLeaf' $ j), CLeaf $ j)
      |> Logic.all j;
  in
    define_single_primrec flat_b [Oper_eq, VLeaf_eq, CLeaf_eq] lthy
  end;

fun define_eval_core fp_b version Y Z preT fpT sig_T ssig_T dtor Oper VLeaf CLeaf dead_pre_map
    dead_sig_map dead_ssig_map flat Lam lthy =
  let
    val eval_core_b = mk_version_fp_binding true lthy version fp_b eval_coreN;
    val YpreT = HOLogic.mk_prodT (Y, preT);
    val Ypre_ssig_T = Tsubst Y YpreT ssig_T;
    val Ypre_ssig_sig_T = Tsubst Y Ypre_ssig_T sig_T;
    val ssig_preT = Tsubst Y ssig_T preT;
    val ssig_YpreT = Tsubst Y ssig_T YpreT;
    val ssig_ssig_T = Tsubst Y ssig_T ssig_T;

    val sigx = Var (("s", 0), Ypre_ssig_sig_T);
    val x = Var (("x", 0), YpreT);
    val j = Var (("j", 0), fpT);
    val eval_core = Free (Binding.name_of eval_core_b, Ypre_ssig_T --> ssig_preT);
    val Oper' = substT Y YpreT Oper;
    val VLeaf' = substT Y YpreT VLeaf;
    val CLeaf' = substT Y YpreT CLeaf;
    val dead_pre_map' = Term.subst_atomic_types [(Y, ssig_ssig_T), (Z, ssig_T)] dead_pre_map;
    val dead_pre_map'' = substT Z ssig_T dead_pre_map;
    val dead_pre_map''' = Term.subst_atomic_types [(Y, fpT), (Z, ssig_T)] dead_pre_map;
    val dead_sig_map' = Term.subst_atomic_types [(Y, Ypre_ssig_T), (Z, ssig_YpreT)] dead_sig_map;
    val dead_ssig_map' = Term.subst_atomic_types [(Y, YpreT), (Z, Y)] dead_ssig_map;
    val Lam' = substT Y ssig_T Lam;
    val fst' = fst_const YpreT;
    val snd' = snd_const YpreT;

    val Oper_eq = mk_Trueprop_eq (eval_core $ (Oper' $ sigx),
        dead_pre_map' $ flat $ (Lam' $ (dead_sig_map' $ (Abs (Name.uu, Ypre_ssig_T,
          HOLogic.mk_prod (dead_ssig_map' $ fst' $ Bound 0, eval_core $ Bound 0))) $ sigx)))
      |> Logic.all sigx;
    val VLeaf_eq = mk_Trueprop_eq (eval_core $ (VLeaf' $ x), dead_pre_map'' $ VLeaf $ (snd' $ x))
      |> Logic.all x;
    val CLeaf_eq = mk_Trueprop_eq (eval_core $ (CLeaf' $ j), dead_pre_map''' $ CLeaf $ (dtor $ j))
      |> Logic.all j;
  in
    define_single_primrec eval_core_b [Oper_eq, VLeaf_eq, CLeaf_eq] lthy
  end;

fun define_eval fp_b version Y Z preT fpT ssig_T dtor dtor_unfold dead_ssig_map eval_core lthy =
  let
    val fp_preT = Tsubst Y fpT preT;
    val fppreT = HOLogic.mk_prodT (fpT, fp_preT);
    val fp_ssig_T = Tsubst Y fpT ssig_T;

    val dtor_unfold' = substT Z fp_ssig_T dtor_unfold;
    val dead_ssig_map' = Term.subst_atomic_types [(Y, fpT), (Z, fppreT)] dead_ssig_map;
    val eval_core' = substT Y fpT eval_core;
    val id' = HOLogic.id_const fpT;

    val rhs = dtor_unfold' $ HOLogic.mk_comp (eval_core', dead_ssig_map' $ mk_convol (id', dtor));
  in
    define_const true fp_b version evalN rhs lthy
  end;

fun define_cutSsig fp_b version Y Z preT ssig_T dead_pre_map VLeaf dead_ssig_map flat eval_core
    lthy =
  let
    val ssig_preT = Tsubst Y ssig_T preT;
    val ssig_ssig_T = Tsubst Y ssig_T ssig_T;
    val ssig_ssig_preT = HOLogic.mk_prodT (ssig_T, ssig_preT);

    val h = Var (("h", 0), Y --> ssig_preT);
    val dead_pre_map' = Term.subst_atomic_types [(Y, ssig_ssig_T), (Z, ssig_T)] dead_pre_map;
    val dead_ssig_map' = substT Z ssig_ssig_preT dead_ssig_map;
    val eval_core' = substT Y ssig_T eval_core;

    val rhs = Library.foldl1 HOLogic.mk_comp [dead_pre_map' $ flat, eval_core',
        dead_ssig_map' $ mk_convol (VLeaf, h)]
      |> Term.lambda h;
  in
    define_const true fp_b version cutSsigN rhs lthy
  end;

fun define_algLam fp_b version Y Z fpT ssig_T Oper VLeaf dead_sig_map eval lthy =
  let
    val fp_ssig_T = Tsubst Y fpT ssig_T;

    val Oper' = substT Y fpT Oper;
    val VLeaf' = substT Y fpT VLeaf;
    val dead_sig_map' = Term.subst_atomic_types [(Y, fpT), (Z, fp_ssig_T)] dead_sig_map;

    val rhs = Library.foldl1 HOLogic.mk_comp [eval, Oper', dead_sig_map' $ VLeaf'];
  in
    define_const true fp_b version algLamN rhs lthy
  end;

fun define_corecU fp_b version Y Z preT ssig_T dtor_unfold VLeaf cutSsig lthy =
  let
    val ssig_preT = Tsubst Y ssig_T preT;

    val h = Var (("h", 0), Y --> ssig_preT);
    val dtor_unfold' = substT Z ssig_T dtor_unfold;

    val rhs = HOLogic.mk_comp (dtor_unfold' $ (cutSsig $ h), VLeaf)
      |> Term.lambda h;
  in
    define_const true fp_b version corecUN rhs lthy
  end;

fun define_corecUU fp_b version Y Z preT ssig_T dead_pre_map dead_ssig_map flat eval_core sctr
    corecU lthy =
  let
    val ssig_preT = Tsubst Y ssig_T preT;
    val ssig_ssig_T = Tsubst Y ssig_T ssig_T
    val ssig_ssig_preT = HOLogic.mk_prodT (ssig_T, ssig_preT);

    val ssig_pre_ssig_T = Tsubst Y ssig_preT ssig_T;

    val h = Var (("h", 0), Y --> ssig_pre_ssig_T);
    val dead_pre_map' = Term.subst_atomic_types [(Y, ssig_ssig_T), (Z, ssig_T)] dead_pre_map;
    val eval_core' = substT Y ssig_T eval_core;
    val dead_ssig_map' =
      Term.subst_atomic_types [(Y, ssig_preT), (Z, ssig_ssig_preT)] dead_ssig_map;
    val id' = HOLogic.id_const ssig_preT;

    val rhs = corecU $ Library.foldl1 HOLogic.mk_comp
        [dead_pre_map' $ flat, eval_core', dead_ssig_map' $ mk_convol (sctr, id'), h]
      |> Term.lambda h;
  in
    define_const true fp_b version corecUUN rhs lthy
  end;

fun derive_sig_transfer maybe_swap ctxt live_AsBs pre_rel sig_rel Rs R const pre_rel_def
    preT_rel_eqs transfer_thm =
  let
    val RRpre_rel = list_comb (pre_rel, Rs) $ R;
    val RRsig_rel = list_comb (sig_rel, Rs) $ R;
    val constB = Term.subst_atomic_types live_AsBs const;

    val goal = uncurry mk_rel_fun (maybe_swap (RRpre_rel, RRsig_rel)) $ const $ constB
      |> HOLogic.mk_Trueprop;
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_sig_transfer_tac ctxt pre_rel_def preT_rel_eqs transfer_thm))
    |> Thm.close_derivation \<^here>
  end;

fun derive_transfer_by_transfer_prover ctxt live_AsBs Rs R const const_defs rel_eqs transfers =
  let
    val constB = Term.subst_atomic_types live_AsBs const;
    val goal = mk_parametricity_goal ctxt (Rs @ [R]) const constB;
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_transfer_by_transfer_prover_tac ctxt (const_defs @ map (fn thm => thm RS sym) rel_eqs)
        rel_eqs transfers))
    |> Thm.close_derivation \<^here>
  end;

fun derive_dtor_transfer ctxt live_EsFs Y Z pre_rel fp_rel Rs dtor dtor_rel_thm =
  let
    val Type (\<^type_name>\<open>fun\<close>, [fpT, Type (\<^type_name>\<open>fun\<close>, [fpTB, \<^typ>\<open>bool\<close>])]) =
      snd (strip_typeN (length live_EsFs) (fastype_of fp_rel));

    val pre_rel' = Term.subst_atomic_types [(Y, fpT), (Z, fpTB)] pre_rel;
    val Rpre_rel = list_comb (pre_rel', Rs);
    val Rfp_rel = list_comb (fp_rel, Rs);
    val dtorB = Term.subst_atomic_types live_EsFs dtor;

    val goal = HOLogic.mk_Trueprop (mk_rel_fun Rfp_rel (Rpre_rel $ Rfp_rel) $ dtor $ dtorB);
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_dtor_transfer_tac ctxt dtor_rel_thm))
    |> Thm.close_derivation \<^here>
  end;

fun derive_Lam_or_eval_core_transfer ctxt live_AsBs Y Z preT ssig_T Rs R pre_rel sig_or_ssig_rel
    ssig_rel const const_def rel_eqs transfers =
  let
    val YpreT = HOLogic.mk_prodT (Y, preT);
    val ZpreTB = typ_subst_atomic live_AsBs YpreT;
    val ssig_TB = typ_subst_atomic live_AsBs ssig_T;

    val pre_rel' = Term.subst_atomic_types [(Y, ssig_T), (Z, ssig_TB)] pre_rel;
    val sig_or_ssig_rel' = Term.subst_atomic_types [(Y, YpreT), (Z, ZpreTB)] sig_or_ssig_rel;
    val Rsig_or_ssig_rel' = list_comb (sig_or_ssig_rel', Rs);
    val RRpre_rel = list_comb (pre_rel, Rs) $ R;
    val RRssig_rel = list_comb (ssig_rel, Rs) $ R;
    val Rpre_rel' = list_comb (pre_rel', Rs);
    val constB = subst_atomic_types live_AsBs const;

    val goal = mk_rel_fun (Rsig_or_ssig_rel' $ mk_rel_prod R RRpre_rel) (Rpre_rel' $ RRssig_rel)
        $ const $ constB
      |> HOLogic.mk_Trueprop;
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_transfer_by_transfer_prover_tac ctxt [const_def] rel_eqs transfers))
    |> Thm.close_derivation \<^here>
  end;

fun derive_proto_sctr_transfer_step_or_merge ctxt Y Z R dead_pre_rel dead_sig_rel proto_sctr
    proto_sctr_def fp_k_T_rel_eqs transfers =
  let
    val proto_sctrZ = substT Y Z proto_sctr;
    val goal = mk_rel_fun (dead_pre_rel $ R) (dead_sig_rel $ R) $ proto_sctr $ proto_sctrZ
      |> HOLogic.mk_Trueprop;
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_transfer_by_transfer_prover_tac ctxt [proto_sctr_def] fp_k_T_rel_eqs transfers))
    |> Thm.close_derivation \<^here>
  end;

fun derive_sctr_transfer ctxt live_AsBs Y Z ssig_T Rs R pre_rel ssig_rel sctr sctr_def
    fp_k_T_rel_eqs transfers =
  let
    val ssig_TB = typ_subst_atomic live_AsBs ssig_T;

    val pre_rel' = Term.subst_atomic_types [(Y, ssig_T), (Z, ssig_TB)] pre_rel;
    val Rpre_rel' = list_comb (pre_rel', Rs);
    val RRssig_rel = list_comb (ssig_rel, Rs) $ R;
    val sctrB = subst_atomic_types live_AsBs sctr;

    val goal = HOLogic.mk_Trueprop (mk_rel_fun (Rpre_rel' $ RRssig_rel) RRssig_rel $ sctr $ sctrB);
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_transfer_by_transfer_prover_tac ctxt [sctr_def] fp_k_T_rel_eqs transfers))
    |> Thm.close_derivation \<^here>
  end;

fun derive_corecUU_transfer ctxt live_AsBs Y Z Rs R preT ssig_T pre_rel fp_rel ssig_rel corecUU
    cutSsig_def corecU_def corecUU_def fp_k_T_rel_eqs transfers =
  let
    val ssig_preT = Tsubst Y ssig_T preT;
    val ssig_TB = typ_subst_atomic live_AsBs ssig_T;
    val ssig_preTB = typ_subst_atomic live_AsBs ssig_preT;

    val pre_rel' = Term.subst_atomic_types [(Y, ssig_T), (Z, ssig_TB)] pre_rel;
    val ssig_rel' = Term.subst_atomic_types [(Y, ssig_preT), (Z, ssig_preTB)] ssig_rel;
    val Rpre_rel' = list_comb (pre_rel', Rs);
    val Rfp_rel = list_comb (fp_rel, Rs);
    val RRssig_rel = list_comb (ssig_rel, Rs) $ R;
    val Rssig_rel' = list_comb (ssig_rel', Rs);
    val corecUUB = subst_atomic_types live_AsBs corecUU;

    val goal = mk_rel_fun (mk_rel_fun R (Rssig_rel' $ (Rpre_rel' $ RRssig_rel)))
        (mk_rel_fun R Rfp_rel) $ corecUU $ corecUUB
      |> HOLogic.mk_Trueprop;
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_transfer_by_transfer_prover_tac ctxt [cutSsig_def, corecU_def, corecUU_def] fp_k_T_rel_eqs
        transfers))
    |> Thm.close_derivation \<^here>
  end;

fun mk_natural_goal ctxt simple_T_mapfs fs t u =
  let
    fun build_simple (T, _) =
      (case AList.lookup (op =) simple_T_mapfs T of
        SOME mapf => mapf
      | NONE => the (find_first (fn f => domain_type (fastype_of f) = T) fs));

    val simple_Ts = map fst simple_T_mapfs;

    val t_map = build_map ctxt simple_Ts [] build_simple (apply2 (range_type o fastype_of) (t, u));
    val u_map = build_map ctxt simple_Ts [] build_simple (apply2 (domain_type o fastype_of) (t, u));
  in
    mk_Trueprop_eq (HOLogic.mk_comp (u, u_map), HOLogic.mk_comp (t_map, t))
  end;

fun derive_natural_by_unfolding ctxt live_AsBs preT pre_map fs f const map_thms =
  let
    val ffpre_map = list_comb (pre_map, fs) $ f;
    val constB = subst_atomic_types live_AsBs const;

    val goal = mk_natural_goal ctxt [(preT, ffpre_map)] (fs @ [f]) const constB;
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_natural_by_unfolding_tac ctxt map_thms))
    |> Thm.close_derivation \<^here>
  end;

fun derive_natural_from_transfer ctxt live_AsBs simple_T_mapfs fs f const transfer bnfs subst_bnfs =
  let
    val m = length live_AsBs;

    val constB = Term.subst_atomic_types live_AsBs const;
    val goal = mk_natural_goal ctxt simple_T_mapfs (fs @ [f]) const constB;
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_natural_from_transfer_tac ctxt m (replicate m true) transfer [] (map rel_Grp_of_bnf bnfs)
        (map rel_Grp_of_bnf subst_bnfs)))
    |> Thm.close_derivation \<^here>
  end;

fun derive_natural_from_transfer_with_pre_type ctxt live_AsBs Y Z preT ssig_T pre_map ssig_map fs
    f =
  let
    val ssig_TB = typ_subst_atomic live_AsBs ssig_T;
    val preT' = Term.typ_subst_atomic [(Y, ssig_T), (Z, ssig_TB)] preT;

    val ffpre_map = list_comb (pre_map, fs) $ f;
    val pre_map' = Term.subst_atomic_types [(Y, ssig_T), (Z, ssig_TB)] pre_map;
    val fpre_map' = list_comb (pre_map', fs);
    val ffssig_map = list_comb (ssig_map, fs) $ f;

    val preT_mapfs = [(preT, ffpre_map), (preT', fpre_map' $ ffssig_map)];
  in
    derive_natural_from_transfer ctxt live_AsBs preT_mapfs fs f
  end;

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
    Lam rho unsig_thm Lam_def =
  let
    val YpreT = HOLogic.mk_prodT (Y, preT);
    val Ypre_old_sig_T = Tsubst Y YpreT old_sig_T;
    val Ypre_k_T = Tsubst Y YpreT k_T;

    val inl' = Inl_const Ypre_old_sig_T Ypre_k_T;
    val inr' = Inr_const Ypre_old_sig_T Ypre_k_T;
    val dead_pre_map' = Term.subst_atomic_types [(Y, old_ssig_T), (Z, ssig_T)] dead_pre_map;
    val Sig' = substT Y YpreT Sig;
    val Lam_o_Sig = HOLogic.mk_comp (Lam, Sig');

    val inl_goal = mk_Trueprop_eq (HOLogic.mk_comp (Lam_o_Sig, inl'),
      HOLogic.mk_comp (dead_pre_map' $ embL, old_Lam));
    val inr_goal = mk_Trueprop_eq (HOLogic.mk_comp (Lam_o_Sig, inr'), rho);
    val goals = [inl_goal, inr_goal];
    val goal = Logic.mk_conjunction_balanced goals;
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove_sorry ctxt vars [] goal
      (fn {context = ctxt, prems = _} => mk_Lam_Inl_Inr_tac ctxt unsig_thm Lam_def))
    |> Conjunction.elim_balanced (length goals)
    |> map (Thm.close_derivation \<^here>)
  end;

fun derive_flat_VLeaf ctxt Y Z ssig_T x VLeaf dead_ssig_map flat ssig_induct fp_map_id sig_map_cong
    sig_map_ident sig_map_comp ssig_map_thms flat_simps =
  let
    val x' = substT Y ssig_T x;
    val dead_ssig_map' = substT Z ssig_T dead_ssig_map;

    val goal = mk_Trueprop_eq (flat $ (dead_ssig_map' $ VLeaf $ x'), x');

    val ssig_induct' = infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt x')] ssig_induct;
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_flat_VLeaf_or_flat_tac ctxt ssig_induct' sig_map_cong
        (fp_map_id :: sig_map_ident :: sig_map_comp :: ssig_map_thms @ flat_simps @
         @{thms o_apply id_apply id_def[symmetric]})))
    |> Thm.close_derivation \<^here>
  end;

fun derive_flat_flat ctxt Y Z ssig_T x dead_ssig_map flat ssig_induct fp_map_id sig_map_cong
    sig_map_comp ssig_map_thms flat_simps =
  let
    val ssig_ssig_T = Tsubst Y ssig_T ssig_T;
    val ssig_ssig_ssig_T = Tsubst Y ssig_T ssig_ssig_T;

    val x' = substT Y ssig_ssig_ssig_T x;
    val dead_ssig_map' = Term.subst_atomic_types [(Y, ssig_ssig_T), (Z, ssig_T)] dead_ssig_map;
    val flat' = substT Y ssig_T flat;

    val goal = mk_Trueprop_eq (flat $ (dead_ssig_map' $ flat $ x'), flat $ (flat' $ x'));

    val ssig_induct' = infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt x')] ssig_induct;
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_flat_VLeaf_or_flat_tac ctxt ssig_induct' sig_map_cong
        (o_apply :: fp_map_id :: sig_map_comp :: ssig_map_thms @ flat_simps)))
    |> Thm.close_derivation \<^here>
  end;

fun derive_eval_core_flat ctxt Y Z preT ssig_T dead_pre_map dead_ssig_map flat eval_core x
    ssig_induct dead_pre_map_id dead_pre_map_comp0 dead_pre_map_comp fp_map_id sig_map_comp
    sig_map_cong ssig_map_thms ssig_map_comp flat_simps flat_pointful_natural flat_flat
    Lam_pointful_natural eval_core_simps =
  let
    val YpreT = HOLogic.mk_prodT (Y, preT);
    val ssig_ssig_T = Tsubst Y ssig_T ssig_T;
    val Ypre_ssig_T = Tsubst Y YpreT ssig_T;
    val Ypre_ssig_ssig_T = Tsubst Y YpreT ssig_ssig_T;
    val ssig_YpreT = Tsubst Y ssig_T YpreT;

    val dead_pre_map' = Term.subst_atomic_types [(Y, ssig_ssig_T), (Z, ssig_T)] dead_pre_map;
    val dead_ssig_map' = Term.subst_atomic_types [(Y, Ypre_ssig_T), (Z, ssig_YpreT)] dead_ssig_map;
    val dead_ssig_map'' = Term.subst_atomic_types [(Y, YpreT), (Z, Y)] dead_ssig_map;
    val flat' = substT Y YpreT flat;
    val eval_core' = substT Y ssig_T eval_core;
    val x' = substT Y Ypre_ssig_ssig_T x;
    val fst' = fst_const YpreT;

    val goal = mk_Trueprop_eq (eval_core $ (flat' $ x'), dead_pre_map' $ flat
      $ (eval_core' $ (dead_ssig_map' $ mk_convol (dead_ssig_map'' $ fst', eval_core) $ x')));

    val ssig_induct' = infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt x')] ssig_induct;
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_eval_core_flat_tac ctxt ssig_induct' dead_pre_map_id dead_pre_map_comp0 dead_pre_map_comp
        fp_map_id sig_map_comp sig_map_cong ssig_map_thms ssig_map_comp flat_simps
        flat_pointful_natural flat_flat Lam_pointful_natural eval_core_simps))
    |> Thm.close_derivation \<^here>
  end;

fun derive_eval_thm ctxt dtor_inject dtor_unfold_thm eval_def =
  (trans OF [iffD2 OF [dtor_inject, HOLogic.mk_obj_eq eval_def RS fun_cong], dtor_unfold_thm])
  |> unfold_thms ctxt [o_apply, eval_def RS symmetric_thm];

fun derive_eval_flat ctxt Y Z fpT ssig_T dead_ssig_map flat eval x dead_pre_map_comp0
    dtor_unfold_unique ssig_map_id ssig_map_comp flat_pointful_natural eval_core_pointful_natural
    eval_core_flat eval_thm =
  let
    val fp_ssig_T = Tsubst Y fpT ssig_T;
    val fp_ssig_ssig_T = Tsubst Y fp_ssig_T ssig_T;

    val dead_ssig_map' = Term.subst_atomic_types [(Y, fp_ssig_T), (Z, fpT)] dead_ssig_map;
    val flat' = substT Y fpT flat;
    val x' = substT Y fp_ssig_ssig_T x;

    val goal = mk_Trueprop_eq (eval $ (flat' $ x'), eval $ (dead_ssig_map' $ eval $ x'));

    val cond_eval_o_flat =
      infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt (HOLogic.mk_comp (eval, flat')))]
        (trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym] RS fun_cong)
      OF [ext, ext];
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_eval_flat_tac ctxt dead_pre_map_comp0 ssig_map_id ssig_map_comp flat_pointful_natural
        eval_core_pointful_natural eval_core_flat eval_thm cond_eval_o_flat))
    |> Thm.close_derivation \<^here>
  end;

fun derive_eval_Oper ctxt live Y Z fpT sig_T ssig_T dead_sig_map Oper eval algLam x sig_map_ident
    sig_map_comp0 sig_map_comp Oper_natural_pointful VLeaf_natural flat_simps eval_flat algLam_def =
  let
    val fp_ssig_T = Tsubst Y fpT ssig_T;
    val fp_ssig_sig_T = Tsubst Y fp_ssig_T sig_T;

    val dead_sig_map' = Term.subst_atomic_types [(Y, fp_ssig_T), (Z, fpT)] dead_sig_map;
    val Oper' = substT Y fpT Oper;
    val x' = substT Y fp_ssig_sig_T x;

    val goal = mk_Trueprop_eq (eval $ (Oper' $ x'), algLam $ (dead_sig_map' $ eval $ x'));
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_eval_Oper_tac ctxt live sig_map_ident sig_map_comp0 sig_map_comp Oper_natural_pointful
        VLeaf_natural flat_simps eval_flat algLam_def))
    |> Thm.close_derivation \<^here>
  end;

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
    dtor_unfold_unique V_or_CLeaf_map_thm eval_core_simps eval_thm =
  let
    val V_or_CLeaf' = substT Y fpT V_or_CLeaf;
    val x' = substT Y fpT x;

    val goal = mk_Trueprop_eq (eval $ (V_or_CLeaf' $ x'), x');
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_eval_V_or_CLeaf_tac ctxt dead_pre_map_id dead_pre_map_comp fp_map_id dtor_unfold_unique
        V_or_CLeaf_map_thm eval_core_simps eval_thm))
    |> Thm.close_derivation \<^here>
  end;

fun derive_extdd_mor ctxt Y Z preT fpT ssig_T dead_pre_map dtor extdd cutSsig f g dead_pre_map_comp0
    dead_pre_map_comp VLeaf_map_thm ssig_map_comp flat_pointful_natural eval_core_pointful_natural
    eval_thm eval_flat eval_VLeaf cutSsig_def =
  let
    val ssig_preT = Tsubst Y ssig_T preT;

    val dead_pre_map' = Term.subst_atomic_types [(Y, ssig_T), (Z, fpT)] dead_pre_map;
    val f' = substT Z fpT f;
    val g' = substT Z ssig_preT g;
    val extdd_f = extdd $ f';

    val prem = mk_Trueprop_eq (HOLogic.mk_comp (dead_pre_map' $ extdd_f, g'),
      HOLogic.mk_comp (dtor, f'));
    val goal = mk_Trueprop_eq (HOLogic.mk_comp (dead_pre_map' $ extdd_f, cutSsig $ g'),
      HOLogic.mk_comp (dtor, extdd_f));
  in
    fold (Variable.add_free_names ctxt) [prem, goal] []
    |> (fn vars => Goal.prove_sorry ctxt vars [prem] goal (fn {context = ctxt, prems = [prem]} =>
      mk_extdd_mor_tac ctxt dead_pre_map_comp0 dead_pre_map_comp VLeaf_map_thm ssig_map_comp
        flat_pointful_natural eval_core_pointful_natural eval_thm eval_flat eval_VLeaf cutSsig_def
        prem))
    |> Thm.close_derivation \<^here>
  end;

fun derive_mor_cutSsig_flat ctxt Y Z preT fpT ssig_T dead_pre_map dead_ssig_map dtor flat eval_core
    eval cutSsig f g dead_pre_map_comp0 dead_pre_map_comp dead_pre_map_cong dtor_unfold_unique
    dead_ssig_map_comp0 ssig_map_comp flat_simps flat_pointful_natural eval_core_pointful_natural
    flat_flat flat_VLeaf eval_core_flat cutSsig_def cutSsig_def_pointful_natural eval_thm =
  let
    val ssig_preT = Tsubst Y ssig_T preT;

    val substYZ = Term.subst_atomic_types [(Y, ssig_T), (Z, fpT)];

    val dead_pre_map' = substYZ dead_pre_map;
    val dead_ssig_map' = substYZ dead_ssig_map;
    val f' = substYZ f;
    val g' = substT Z ssig_preT g;
    val cutSsig_g = cutSsig $ g';

    val id' = HOLogic.id_const ssig_T;
    val convol' = mk_convol (id', cutSsig_g);
    val dead_ssig_map'' =
      Term.subst_atomic_types [(Y, ssig_T), (Z, range_type (fastype_of convol'))] dead_ssig_map;
    val eval_core' = substT Y ssig_T eval_core;
    val eval_core_o_map = HOLogic.mk_comp (eval_core', dead_ssig_map'' $ convol');

    val prem = mk_Trueprop_eq (HOLogic.mk_comp (dead_pre_map' $ f', cutSsig_g),
      HOLogic.mk_comp (dtor, f'));
    val goal = mk_Trueprop_eq (HOLogic.mk_comp (eval, dead_ssig_map' $ f'),
      HOLogic.mk_comp (f', flat));
  in
    fold (Variable.add_free_names ctxt) [prem, goal] []
    |> (fn vars => Goal.prove_sorry ctxt vars [prem] goal (fn {context = ctxt, prems = [prem]} =>
      mk_mor_cutSsig_flat_tac ctxt eval_core_o_map dead_pre_map_comp0 dead_pre_map_comp
        dead_pre_map_cong dtor_unfold_unique dead_ssig_map_comp0 ssig_map_comp flat_simps
        flat_pointful_natural eval_core_pointful_natural flat_flat flat_VLeaf eval_core_flat
        cutSsig_def cutSsig_def_pointful_natural eval_thm prem))
    |> Thm.close_derivation \<^here>
  end;

fun derive_extdd_o_VLeaf ctxt Y Z preT fpT ssig_T dead_pre_map dtor VLeaf extdd f g
    dead_pre_map_comp0 dead_pre_map_comp dtor_inject ssig_map_thms eval_core_simps eval_thm
    eval_VLeaf =
  let
    val ssig_preT = Tsubst Y ssig_T preT;

    val substYZ = Term.subst_atomic_types [(Y, ssig_T), (Z, fpT)];

    val dead_pre_map' = substYZ dead_pre_map;
    val f' = substT Z fpT f;
    val g' = substT Z ssig_preT g;
    val extdd_f = extdd $ f';

    val prem = mk_Trueprop_eq (HOLogic.mk_comp (dead_pre_map' $ extdd_f, g'),
      HOLogic.mk_comp (dtor, f'));
    val goal = mk_Trueprop_eq (HOLogic.mk_comp (extdd_f, VLeaf), f');
  in
    fold (Variable.add_free_names ctxt) [prem, goal] []
    |> (fn vars => Goal.prove_sorry ctxt vars [prem] goal (fn {context = ctxt, prems = [prem]} =>
      mk_extdd_o_VLeaf_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_inject ssig_map_thms
        eval_core_simps eval_thm eval_VLeaf prem))
    |> Thm.close_derivation \<^here>
  end;

fun derive_corecU_pointfree ctxt Y Z preT fpT ssig_T dead_pre_map dtor extdd corecU g
    dead_pre_map_comp dtor_unfold_thm ssig_map_thms dead_ssig_map_comp0 flat_simps flat_VLeaf
    eval_core_simps cutSsig_def mor_cutSsig_flat corecU_def =
  let
    val ssig_preT = Tsubst Y ssig_T preT;

    val substYZ = Term.subst_atomic_types [(Y, ssig_T), (Z, fpT)];

    val dead_pre_map' = substYZ dead_pre_map;
    val g' = substT Z ssig_preT g;
    val corecU_g = corecU $ g';

    val goal = mk_Trueprop_eq (HOLogic.mk_comp (dead_pre_map' $ (extdd $ corecU_g), g'),
      HOLogic.mk_comp (dtor, corecU_g));
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_corecU_pointfree_tac ctxt dead_pre_map_comp dtor_unfold_thm ssig_map_thms
      dead_ssig_map_comp0 flat_simps flat_VLeaf eval_core_simps cutSsig_def mor_cutSsig_flat
      corecU_def))
    |> Thm.close_derivation \<^here>
  end;

fun derive_corecU_ctor_unique ctxt Y Z preT fpT ssig_T dead_pre_map ctor dtor VLeaf extdd corecU f g
    dead_pre_map_comp ctor_dtor dtor_unfold_thm dtor_unfold_unique ssig_map_thms dead_ssig_map_comp0
    flat_simps flat_VLeaf eval_core_simps extdd_mor extdd_o_VLeaf cutSsig_def mor_cutSsig_flat
    corecU_def =
  let
    val corecU_pointfree = derive_corecU_pointfree ctxt Y Z preT fpT ssig_T dead_pre_map dtor extdd
      corecU g dead_pre_map_comp dtor_unfold_thm ssig_map_thms dead_ssig_map_comp0 flat_simps
      flat_VLeaf eval_core_simps cutSsig_def mor_cutSsig_flat corecU_def;

    val corecU_thm = corecU_pointfree RS @{thm comp_eq_dest};

    val corecU_ctor =
      let
        val arg_cong' =
          infer_instantiate' ctxt [NONE, NONE, SOME (Thm.cterm_of ctxt ctor)] arg_cong;
      in
        unfold_thms ctxt [ctor_dtor] (corecU_thm RS arg_cong')
      end;

    val corecU_unique =
      let
        val substYZ = Term.subst_atomic_types [(Y, ssig_T), (Z, fpT)];

        val f' = substYZ f;
        val abs_f_o_VLeaf = Term.lambda f' (HOLogic.mk_comp (f', VLeaf));

        val inject_refine' = infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt abs_f_o_VLeaf),
          SOME (Thm.cterm_of ctxt extdd)] @{thm inject_refine};
      in
        unfold_thms ctxt @{thms atomize_imp}
          (((inject_refine' OF [extdd_o_VLeaf, extdd_o_VLeaf] RS iffD1)
            OF [asm_rl, corecU_pointfree])
           OF [asm_rl, trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym]
             OF [extdd_mor, corecU_pointfree RS extdd_mor]])
        RS @{thm obj_distinct_prems}
      end;
  in
    (corecU_ctor, corecU_unique)
  end;

fun derive_dtor_algLam ctxt Y Z preT fpT sig_T ssig_T dead_pre_map dtor dead_sig_map Lam eval algLam
    x pre_map_comp dead_pre_map_id dead_pre_map_comp0 dead_pre_map_comp sig_map_comp
    Oper_pointful_natural ssig_map_thms dead_ssig_map_comp0 Lam_pointful_natural eval_core_simps
    eval_thm eval_flat eval_VLeaf algLam_def =
  let
    val fp_preT = Tsubst Y fpT preT;
    val fppreT = HOLogic.mk_prodT (fpT, fp_preT);
    val fp_sig_T = Tsubst Y fpT sig_T;
    val fp_ssig_T = Tsubst Y fpT ssig_T;

    val id' = HOLogic.id_const fpT;
    val convol' = mk_convol (id', dtor);
    val dead_pre_map' = Term.subst_atomic_types [(Y, fp_ssig_T), (Z, fpT)] dead_pre_map;
    val dead_sig_map' = Term.subst_atomic_types [(Y, fpT), (Z, fppreT)] dead_sig_map;
    val Lam' = substT Y fpT Lam;
    val x' = substT Y fp_sig_T x;

    val goal = mk_Trueprop_eq (dtor $ (algLam $ x'),
      dead_pre_map' $ eval $ (Lam' $ (dead_sig_map' $ convol' $ x')));
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_dtor_algLam_tac ctxt pre_map_comp dead_pre_map_id dead_pre_map_comp0 dead_pre_map_comp
        sig_map_comp Oper_pointful_natural ssig_map_thms dead_ssig_map_comp0 Lam_pointful_natural
        eval_core_simps eval_thm eval_flat eval_VLeaf algLam_def))
    |> Thm.close_derivation \<^here>
  end;

fun derive_algLam_base ctxt Y Z preT fpT dead_pre_map ctor dtor algLam proto_sctr dead_pre_map_id
    dead_pre_map_comp ctor_dtor dtor_ctor dtor_unfold_unique unsig_thm Sig_pointful_natural
    ssig_map_thms Lam_def flat_simps eval_core_simps eval_thm algLam_def =
  let
    val fp_preT = Tsubst Y fpT preT;

    val proto_sctr' = substT Y fpT proto_sctr;

    val dead_pre_map' = Term.subst_atomic_types [(Y, fpT), (Z, fp_preT)] dead_pre_map;
    val dead_pre_map_dtor = dead_pre_map' $ dtor;

    val goal = mk_Trueprop_eq (HOLogic.mk_comp (algLam, proto_sctr'), ctor);
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_algLam_base_tac ctxt dead_pre_map_dtor dead_pre_map_id dead_pre_map_comp ctor_dtor
        dtor_ctor dtor_unfold_unique unsig_thm Sig_pointful_natural ssig_map_thms Lam_def flat_simps
        eval_core_simps eval_thm algLam_def))
    |> Thm.close_derivation \<^here>
  end;

fun derive_flat_embL ctxt Y Z old_ssig_T ssig_T dead_old_ssig_map embL old_flat flat x
    old_ssig_induct fp_map_id Sig_pointful_natural old_sig_map_comp old_sig_map_cong
    old_ssig_map_thms old_flat_simps flat_simps embL_simps =
  let
    val old_ssig_old_ssig_T = Tsubst Y old_ssig_T old_ssig_T;

    val dead_old_ssig_map' =
      Term.subst_atomic_types [(Y, old_ssig_T), (Z, ssig_T)] dead_old_ssig_map;
    val embL' = substT Y ssig_T embL;
    val x' = substT Y old_ssig_old_ssig_T x;

    val goal = mk_Trueprop_eq (flat $ (embL' $ (dead_old_ssig_map' $ embL $ x')),
      embL $ (old_flat $ x'));

    val old_ssig_induct' =
      infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt x')] old_ssig_induct;
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_flat_embL_tac ctxt old_ssig_induct' fp_map_id Sig_pointful_natural old_sig_map_comp
        old_sig_map_cong old_ssig_map_thms old_flat_simps flat_simps embL_simps))
    |> Thm.close_derivation \<^here>
  end;

fun derive_eval_core_embL ctxt Y Z preT old_ssig_T ssig_T dead_pre_map embL old_eval_core eval_core
    x old_ssig_induct dead_pre_map_comp0 dead_pre_map_comp Sig_pointful_natural unsig_thm
    old_sig_map_comp old_sig_map_cong old_Lam_pointful_natural Lam_def flat_embL embL_simps
    embL_pointful_natural old_eval_core_simps eval_core_simps =
  let
    val YpreT = HOLogic.mk_prodT (Y, preT);
    val Ypre_old_ssig_T = Tsubst Y YpreT old_ssig_T;

    val dead_pre_map' = Term.subst_atomic_types [(Y, old_ssig_T), (Z, ssig_T)] dead_pre_map;
    val embL' = substT Y YpreT embL;
    val x' = substT Y Ypre_old_ssig_T x;

    val goal =
      mk_Trueprop_eq (eval_core $ (embL' $ x'), dead_pre_map' $ embL $ (old_eval_core $ x'));

    val old_ssig_induct' =
      infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt x')] old_ssig_induct;
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_eval_core_embL_tac ctxt old_ssig_induct' dead_pre_map_comp0 dead_pre_map_comp
        Sig_pointful_natural unsig_thm old_sig_map_comp old_sig_map_cong old_Lam_pointful_natural
        Lam_def flat_embL old_eval_core_simps eval_core_simps embL_simps embL_pointful_natural))
    |> Thm.close_derivation \<^here>
  end;

fun derive_eval_embL ctxt Y fpT embL old_eval eval dead_pre_map_comp0 dtor_unfold_unique
    embL_pointful_natural eval_core_embL old_eval_thm eval_thm =
  let
    val embL' = substT Y fpT embL;
    val goal = mk_Trueprop_eq (HOLogic.mk_comp (eval, embL'), old_eval);
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_eval_embL_tac ctxt dead_pre_map_comp0 dtor_unfold_unique embL_pointful_natural
        eval_core_embL old_eval_thm eval_thm))
    |> Thm.close_derivation \<^here>
  end;

fun derive_algLam_algLam ctxt Inx_const Y fpT Sig old_algLam algLam dead_pre_map_comp dtor_inject
    unsig_thm sig_map_thm Lam_def eval_embL old_dtor_algLam dtor_algLam =
  let
    val Sig' = substT Y fpT Sig;
    val (left_T, right_T) = dest_sumT (domain_type (fastype_of Sig'));
    val inx' = Inx_const left_T right_T;

    val goal = mk_Trueprop_eq (Library.foldl1 HOLogic.mk_comp [algLam, Sig', inx'], old_algLam);
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_algLam_algLam_tac ctxt dead_pre_map_comp dtor_inject unsig_thm sig_map_thm Lam_def
        eval_embL old_dtor_algLam dtor_algLam))
    |> Thm.close_derivation \<^here>
  end;

fun derive_eval_core_k_as_ssig ctxt Y preT k_T rho eval_core k_as_ssig x pre_map_comp
    dead_pre_map_id sig_map_comp ssig_map_thms Lam_natural_pointful Lam_Inr flat_VLeaf
    eval_core_simps =
  let
    val YpreT = HOLogic.mk_prodT (Y, preT);
    val Ypre_k_T = Tsubst Y YpreT k_T;

    val k_as_ssig' = substT Y YpreT k_as_ssig;
    val x' = substT Y Ypre_k_T x;

    val goal = mk_Trueprop_eq (eval_core $ (k_as_ssig' $ x'), rho $ x');
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_eval_core_k_as_ssig_tac ctxt pre_map_comp dead_pre_map_id sig_map_comp ssig_map_thms
        Lam_natural_pointful Lam_Inr flat_VLeaf eval_core_simps))
    |> Thm.close_derivation \<^here>
  end;

fun derive_algLam_algrho ctxt Y fpT Sig algLam algrho algLam_def algrho_def =
  let
    val Sig' = substT Y fpT Sig;
    val (left_T, right_T) = dest_sumT (domain_type (fastype_of Sig'));
    val inr' = Inr_const left_T right_T;

    val goal = mk_Trueprop_eq (Library.foldl1 HOLogic.mk_comp [algLam, Sig', inr'], algrho);
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_algLam_algrho_tac ctxt algLam_def algrho_def))
    |> Thm.close_derivation \<^here>
  end;

fun derive_dtor_algrho ctxt Y Z preT fpT k_T ssig_T dead_pre_map dead_k_map dtor rho eval algrho x
    eval_thm k_as_ssig_natural_pointful eval_core_k_as_ssig algrho_def =
  let
    val YpreT = HOLogic.mk_prodT (Y, preT);
    val fppreT = Tsubst Y fpT YpreT;
    val fp_k_T = Tsubst Y fpT k_T;
    val fp_ssig_T = Tsubst Y fpT ssig_T;

    val id' = HOLogic.id_const fpT;
    val convol' = mk_convol (id', dtor);
    val dead_pre_map' = Term.subst_atomic_types [(Y, fp_ssig_T), (Z, fpT)] dead_pre_map;
    val dead_k_map' = Term.subst_atomic_types [(Y, fpT), (Z, fppreT)] dead_k_map;
    val rho' = substT Y fpT rho;
    val x' = substT Y fp_k_T x;

    val goal = mk_Trueprop_eq (dtor $ (algrho $ x'),
      dead_pre_map' $ eval $ (rho' $ (dead_k_map' $ convol' $ x')));
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_dtor_algrho_tac ctxt eval_thm k_as_ssig_natural_pointful eval_core_k_as_ssig algrho_def))
    |> Thm.close_derivation \<^here>
  end;

fun derive_algLam_step_or_merge ctxt Y fpT ctor proto_sctr algLam proto_sctr_def old_algLam_pointful
    algLam_algLam =
  let
    val proto_sctr' = substT Y fpT proto_sctr;
    val goal = mk_Trueprop_eq (HOLogic.mk_comp (algLam, proto_sctr'), ctor);

    val algLam_algLam_pointful = mk_pointful ctxt algLam_algLam;
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_algLam_step_tac ctxt proto_sctr_def old_algLam_pointful algLam_algLam_pointful))
    |> Thm.close_derivation \<^here>
  end;

fun derive_eval_sctr ctxt Y Z fpT ssig_T dead_pre_map ctor eval sctr proto_sctr_pointful_natural
    eval_Oper algLam_thm sctr_def =
  let
    val fp_ssig_T = Tsubst Y fpT ssig_T;

    val dead_pre_map' = Term.subst_atomic_types [(Y, fp_ssig_T), (Z, fpT)] dead_pre_map;
    val sctr' = substT Y fpT sctr;

    val goal = mk_Trueprop_eq (HOLogic.mk_comp (eval, sctr'),
      HOLogic.mk_comp (ctor, dead_pre_map' $ eval));
  in
    Variable.add_free_names ctxt goal []
    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      mk_eval_sctr_tac ctxt proto_sctr_pointful_natural eval_Oper algLam_thm sctr_def))
    |> Thm.close_derivation \<^here>
  end;

fun derive_corecUU_pointfree_unique ctxt Y Z preT fpT ssig_T dead_pre_map ctor dead_ssig_map eval
    corecUU f g dead_pre_map_comp0 dead_pre_map_comp dtor_ctor dtor_inject ssig_map_comp
    flat_pointful_natural eval_core_pointful_natural eval_thm eval_flat corecU_ctor corecU_unique
    sctr_pointful_natural eval_sctr_pointful corecUU_def =
  let
    val ssig_preT = Tsubst Y ssig_T preT;
    val ssig_pre_ssig_T = Tsubst Y ssig_preT ssig_T;
    val fp_ssig_T = Tsubst Y fpT ssig_T;

    val dead_pre_map' = Term.subst_atomic_types [(Y, fp_ssig_T), (Z, fpT)] dead_pre_map;
    val dead_pre_map'' = Term.subst_atomic_types [(Y, ssig_T), (Z, fp_ssig_T)] dead_pre_map;
    val dead_ssig_map' = Term.subst_atomic_types [(Y, ssig_preT), (Z, fpT)] dead_ssig_map;
    val dead_ssig_map'' = substT Z fpT dead_ssig_map;
    val f' = substT Z ssig_pre_ssig_T f;
    val g' = substT Z fpT g;
    val corecUU_f = corecUU $ f';

    fun mk_eq fpf =
      mk_Trueprop_eq (fpf, Library.foldl1 HOLogic.mk_comp [eval, dead_ssig_map' $
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.31 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik