Quelle bnf_gfp.ML Sprache: SML

(*  Title:      HOL/Tools/BNF/bnf_gfp.ML
    Author:     Dmitriy Traytel, TU Muenchen
    Author:     Andrei Popescu, TU Muenchen
    Author:     Jasmin Blanchette, TU Muenchen
    Author:     Jan van Brügge, TU Muenchen
    Copyright   2012, 2022

Codatatype construction.
*)

signature BNF_GFP =
sig
  val construct_gfp: mixfix list -> binding list -> binding list -> binding list ->
    binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
    BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
    BNF_FP_Util.fp_result * local_theory
end;

structure BNF_GFP : BNF_GFP =
struct

open BNF_Def
open BNF_Util
open BNF_Tactics
open BNF_Comp
open BNF_FP_Util
open BNF_FP_Def_Sugar
open BNF_GFP_Util
open BNF_GFP_Tactics

datatype wit_tree = Wit_Leaf of int | Wit_Node of (int * int * int list) * wit_tree list;

fun mk_tree_args (I, T) (I', Ts) = (sort_distinct int_ord (I @ I'), T :: Ts);

fun finish Iss m seen i (nwit, I) =
  let
    val treess = map (fn j =>
        if j < m orelse member (op =) seen j then [([j], Wit_Leaf j)]
        else
          map_index (finish Iss m (insert (op =) j seen) j) (nth Iss (j - m))
          |> flat
          |> minimize_wits)
      I;
  in
    map (fn (I, t) => (I, Wit_Node ((i - m, nwit, filter (fn i => i < m) I), t)))
      (fold_rev (map_product mk_tree_args) treess [([], [])])
    |> minimize_wits
  end;

fun tree_to_ctor_wit vars _ _ (Wit_Leaf j) = ([j], nth vars j)
  | tree_to_ctor_wit vars ctors witss (Wit_Node ((i, nwit, I), subtrees)) =
     (I, nth ctors i $ (Term.list_comb (snd (nth (nth witss i) nwit),
       map (snd o tree_to_ctor_wit vars ctors witss) subtrees)));

fun tree_to_coind_wits _ (Wit_Leaf _) = []
  | tree_to_coind_wits lwitss (Wit_Node ((i, nwit, I), subtrees)) =
     ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees;

(*all BNFs have the same lives*)
fun construct_gfp mixfixes map_bs rel_bs pred_bs set_bss0 bs resBs (resDs, Dss) bnfs absT_infos
    lthy =
  let
    val time = time lthy;
    val timer = time (Timer.startRealTimer ());

    val live = live_of_bnf (hd bnfs);
    val n = length bnfs; (*active*)
    val ks = 1 upto n;
    val m = live - n; (*passive, if 0 don't generate a new BNF*)
    val ls = 1 upto m;

    val internals = Config.get lthy bnf_internals;
    val b_names = map Binding.name_of bs;
    val b_name = mk_common_name b_names;
    val b = Binding.name b_name;

    fun mk_internal_of_b name =
      Binding.prefix_name (name ^ "_") #> Binding.prefix true b_name #> Binding.concealed;
    fun mk_internal_b name = mk_internal_of_b name b;
    fun mk_internal_bs name = map (mk_internal_of_b name) bs;
    val external_bs = map2 (Binding.prefix false) b_names bs
      |> not internals ? map Binding.concealed;

    val deads = fold (union (op =)) Dss resDs;
    val names_lthy = fold Variable.declare_typ deads lthy;
    val passives = map fst (subtract (op = o apsnd TFree) deads resBs);

    (* tvars *)
    val ((((((passiveAs, activeAs), passiveBs), activeBs), passiveCs), activeCs), idxT) = names_lthy
      |> variant_tfrees passives
      ||>> mk_TFrees n
      ||>> variant_tfrees passives
      ||>> mk_TFrees n
      ||>> mk_TFrees m
      ||>> mk_TFrees n
      ||> fst o mk_TFrees 1
      ||> the_single;

    val allAs = passiveAs @ activeAs;
    val allBs' = passiveBs @ activeBs;
    val Ass = replicate n allAs;
    val allBs = passiveAs @ activeBs;
    val Bss = replicate n allBs;
    val allCs = passiveAs @ activeCs;
    val allCs' = passiveBs @ activeCs;
    val Css' = replicate n allCs';

    (* types *)
    val dead_poss =
      map (fn x => if member (op =) deads (TFree x) then SOME (TFree x) else NONE) resBs;
    fun mk_param NONE passive = (hd passive, tl passive)
      | mk_param (SOME a) passive = (a, passive);
    val mk_params = fold_map mk_param dead_poss #> fst;

    fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs;
    val (params, params') = `(map Term.dest_TFree) (mk_params passiveAs);
    val FTsAs = mk_FTs allAs;
    val FTsBs = mk_FTs allBs;
    val FTsCs = mk_FTs allCs;
    val ATs = map HOLogic.mk_setT passiveAs;
    val BTs = map HOLogic.mk_setT activeAs;
    val B'Ts = map HOLogic.mk_setT activeBs;
    val B''Ts = map HOLogic.mk_setT activeCs;
    val sTs = map2 (fn T => fn U => T --> U) activeAs FTsAs;
    val s'Ts = map2 (fn T => fn U => T --> U) activeBs FTsBs;
    val s''Ts = map2 (fn T => fn U => T --> U) activeCs FTsCs;
    val fTs = map2 (fn T => fn U => T --> U) activeAs activeBs;
    val self_fTs = map (fn T => T --> T) activeAs;
    val gTs = map2 (fn T => fn U => T --> U) activeBs activeCs;
    val all_gTs = map2 (fn T => fn U => T --> U) allBs allCs';
    val RTs = map2 (fn T => fn U => HOLogic.mk_prodT (T, U)) activeAs activeBs;
    val sRTs = map2 (fn T => fn U => HOLogic.mk_prodT (T, U)) activeAs activeAs;
    val R'Ts = map2 (fn T => fn U => HOLogic.mk_prodT (T, U)) activeBs activeCs;
    val setsRTs = map HOLogic.mk_setT sRTs;
    val setRTs = map HOLogic.mk_setT RTs;
    val all_sbisT = HOLogic.mk_tupleT setsRTs;
    val setR'Ts = map HOLogic.mk_setT R'Ts;
    val FRTs = mk_FTs (passiveAs @ RTs);

    (* terms *)
    val mapsAsAs = @{map 4} mk_map_of_bnf Dss Ass Ass bnfs;
    val mapsAsBs = @{map 4} mk_map_of_bnf Dss Ass Bss bnfs;
    val mapsBsCs' = @{map 4} mk_map_of_bnf Dss Bss Css' bnfs;
    val mapsAsCs' = @{map 4} mk_map_of_bnf Dss Ass Css' bnfs;
    val map_fsts = @{map 4} mk_map_of_bnf Dss (replicate n (passiveAs @ RTs)) Ass bnfs;
    val map_snds = @{map 4} mk_map_of_bnf Dss (replicate n (passiveAs @ RTs)) Bss bnfs;
    fun mk_setss Ts = @{map 3} mk_sets_of_bnf (map (replicate live) Dss)
      (map (replicate live) (replicate n Ts)) bnfs;
    val setssAs = mk_setss allAs;
    val setssAs' = transpose setssAs;
    val bis_setss = mk_setss (passiveAs @ RTs);
    val relsAsBs = @{map 4} mk_rel_of_bnf Dss Ass Bss bnfs;
    val bds = @{map 3} mk_bd_of_bnf Dss Ass bnfs;
    val sum_bd = Library.foldr1 (uncurry mk_csum) bds;
    val sum_bdT = fst (dest_relT (fastype_of sum_bd));
    val (sum_bdT_params, sum_bdT_params') = `(map TFree) (Term.add_tfreesT sum_bdT []);

    val ((((((((((zs, zs'), Bs), ss), fs), self_fs), all_gs), xFs), yFs), yFs_copy), _) =
      lthy
      |> mk_Frees' "b" activeAs
      ||>> mk_Frees "B" BTs
      ||>> mk_Frees "s" sTs
      ||>> mk_Frees "f" fTs
      ||>> mk_Frees "f" self_fTs
      ||>> mk_Frees "g" all_gTs
      ||>> mk_Frees "x" FTsAs
      ||>> mk_Frees "y" FTsBs
      ||>> mk_Frees "y" FTsBs;

    val passive_UNIVs = map HOLogic.mk_UNIV passiveAs;
    val passive_eqs = map HOLogic.eq_const passiveAs;
    val active_UNIVs = map HOLogic.mk_UNIV activeAs;
    val passive_ids = map HOLogic.id_const passiveAs;
    val active_ids = map HOLogic.id_const activeAs;
    val fsts = map fst_const RTs;
    val snds = map snd_const RTs;

    (* thms *)
    val bd_card_orders = map bd_card_order_of_bnf bnfs;
    val bd_card_order = hd bd_card_orders
    val bd_Card_orders = map bd_Card_order_of_bnf bnfs;
    val bd_Card_order = hd bd_Card_orders;
    val bd_Cinfinites = map bd_Cinfinite_of_bnf bnfs;
    val bd_Cinfinite = hd bd_Cinfinites;
    val bd_regularCards = map bd_regularCard_of_bnf bnfs;
    val in_monos = map in_mono_of_bnf bnfs;
    val map_comp0s = map map_comp0_of_bnf bnfs;
    val sym_map_comps = map mk_sym map_comp0s;
    val map_comps = map map_comp_of_bnf bnfs;
    val map_cong0s = map map_cong0_of_bnf bnfs;
    val map_id0s = map map_id0_of_bnf bnfs;
    val map_ids = map map_id_of_bnf bnfs;
    val set_bdss = map set_bd_of_bnf bnfs;
    val set_mapss = map set_map_of_bnf bnfs;
    val rel_congs = map rel_cong0_of_bnf bnfs;
    val rel_converseps = map rel_conversep_of_bnf bnfs;
    val rel_Grps = map rel_Grp_of_bnf bnfs;
    val le_rel_OOs = map le_rel_OO_of_bnf bnfs;
    val in_rels = map in_rel_of_bnf bnfs;

    val timer = time (timer "Extracted terms & thms");

    (* derived thms *)

    (*map g1 ... gm g(m+1) ... g(m+n) (map id ... id f(m+1) ... f(m+n) x) =
      map g1 ... gm (g(m+1) o f(m+1)) ... (g(m+n) o f(m+n)) x*)
    fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp0 =
      let
        val lhs = Term.list_comb (mapBsCs, all_gs) $
          (Term.list_comb (mapAsBs, passive_ids @ fs) $ x);
        val rhs =
          Term.list_comb (mapAsCs, take m all_gs @ map HOLogic.mk_comp (drop m all_gs ~~ fs)) $ x;
        val goal = mk_Trueprop_eq (lhs, rhs);
        val vars = Variable.add_free_names lthy goal [];
      in
        Goal.prove_sorry lthy vars [] goal
          (fn {context = ctxt, prems = _} => mk_map_comp_id_tac ctxt map_comp0)
        |> Thm.close_derivation \<^here>
      end;

    val map_comp_id_thms = @{map 5} mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;

    (*forall a : set(m+1) x. f(m+1) a = a; ...; forall a : set(m+n) x. f(m+n) a = a ==>
      map id ... id f(m+1) ... f(m+n) x = x*)
    fun mk_map_cong0L x mapAsAs sets map_cong0 map_id =
      let
        fun mk_prem set f z z' =
          HOLogic.mk_Trueprop
            (mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z))));
        val prems = @{map 4} mk_prem (drop m sets) self_fs zs zs';
        val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x);
        val vars = Variable.add_free_names lthy goal [];
      in
        Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, goal))
          (fn {context = ctxt, prems = _} => mk_map_cong0L_tac ctxt m map_cong0 map_id)
        |> Thm.close_derivation \<^here>
      end;

    val map_cong0L_thms = @{map 5} mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
    val in_mono'_thms = map (fn thm =>
      (thm OF (replicate m @{thm subset_refl})) RS @{thm set_mp}) in_monos;

    val map_arg_cong_thms =
      let
        val prems = map2 (curry mk_Trueprop_eq) yFs yFs_copy;
        val maps = map (fn mapx => Term.list_comb (mapx, all_gs)) mapsBsCs';
        val concls =
          @{map 3} (fn x => fn y => fn mapx => mk_Trueprop_eq (mapx $ x, mapx $ y))
            yFs yFs_copy maps;
        val goals = map2 (fn prem => fn concl => Logic.mk_implies (prem, concl)) prems concls;
      in
        map (fn goal =>
          Variable.add_free_names lthy goal []
          |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
            (hyp_subst_tac ctxt THEN' rtac ctxt refl) 1))
          |> Thm.close_derivation \<^here>)
        goals
      end;

    val timer = time (timer "Derived simple theorems");

    (* coalgebra *)

    val coalg_bind = mk_internal_b (coN ^ algN) ;
    val coalg_def_bind = (Thm.def_binding coalg_bind, []);

    (*forall i = 1 ... n: (\<forall>x \<in> Bi. si \<in> Fi_in UNIV .. UNIV B1 ... Bn)*)
    val coalg_spec =
      let
        val ins = @{map 3} mk_in (replicate n (passive_UNIVs @ Bs)) setssAs FTsAs;
        fun mk_coalg_conjunct B s X z z' =
          mk_Ball B (Term.absfree z' (HOLogic.mk_mem (s $ z, X)));

        val rhs = Library.foldr1 HOLogic.mk_conj (@{map 5} mk_coalg_conjunct Bs ss ins zs zs')
      in
        fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss) rhs
      end;

    val ((coalg_free, (_, coalg_def_free)), (lthy, lthy_old)) =
      lthy
      |> (snd o Local_Theory.begin_nested)
      |> Local_Theory.define ((coalg_bind, NoSyn), (coalg_def_bind, coalg_spec))
      ||> `Local_Theory.end_nested;

    val phi = Proof_Context.export_morphism lthy_old lthy;
    val coalg = dest_Const_name (Morphism.term phi coalg_free);
    val coalg_def = mk_unabs_def (2 * n) (HOLogic.mk_obj_eq (Morphism.thm phi coalg_def_free));

    fun mk_coalg Bs ss =
      let
        val args = Bs @ ss;
        val Ts = map fastype_of args;
        val coalgT = Library.foldr (op -->) (Ts, HOLogic.boolT);
      in
        Term.list_comb (Const (coalg, coalgT), args)
      end;

    val((((((zs, zs'), Bs), B's), ss), s's), _) =
      lthy
      |> mk_Frees' "b" activeAs
      ||>> mk_Frees "B" BTs
      ||>> mk_Frees "B'" B'Ts
      ||>> mk_Frees "s" sTs
      ||>> mk_Frees "s'" s'Ts;

    val coalg_prem = HOLogic.mk_Trueprop (mk_coalg Bs ss);

    val coalg_in_thms = map (fn i =>
      coalg_def RS iffD1 RS mk_conjunctN n i RS @{thm bspec}) ks

    val coalg_set_thmss =
      let
        val coalg_prem = HOLogic.mk_Trueprop (mk_coalg Bs ss);
        fun mk_prem x B = mk_Trueprop_mem (x, B);
        fun mk_concl s x B set = HOLogic.mk_Trueprop (mk_leq (set $ (s $ x)) B);
        val prems = map2 mk_prem zs Bs;
        val conclss = @{map 3} (fn s => fn x => fn sets => map2 (mk_concl s x) Bs (drop m sets))
          ss zs setssAs;
        val goalss = map2 (fn prem => fn concls => map (fn concl =>
          Logic.list_implies (coalg_prem :: [prem], concl)) concls) prems conclss;
      in
        map (fn goals => map (fn goal =>
          Variable.add_free_names lthy goal []
          |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
            mk_coalg_set_tac ctxt coalg_def))
          |> Thm.close_derivation \<^here>)
        goals) goalss
      end;

    fun mk_tcoalg BTs = mk_coalg (map HOLogic.mk_UNIV BTs);

    val tcoalg_thm =
      let
        val goal = HOLogic.mk_Trueprop (mk_tcoalg activeAs ss);
        val vars = Variable.add_free_names lthy goal [];
      in
        Goal.prove_sorry lthy vars [] goal
          (fn {context = ctxt, prems = _} => (rtac ctxt (coalg_def RS iffD2) 1 THEN CONJ_WRAP
            (K (EVERY' [rtac ctxt @{thm ballI}, rtac ctxt @{thm CollectI},
              CONJ_WRAP' (K (EVERY' [rtac ctxt @{thm subset_UNIV}])) allAs] 1)) ss))
        |> Thm.close_derivation \<^here>
      end;

    val timer = time (timer "Coalgebra definition & thms");

    (* morphism *)

    val mor_bind = mk_internal_b morN;
    val mor_def_bind = (Thm.def_binding mor_bind, []);

    (*fbetw) forall i = 1 ... n: (\<forall>x \<in> Bi. fi x \<in> B'i)*)
    (*mor) forall i = 1 ... n: (\<forall>x \<in> Bi.
       Fi_map id ... id f1 ... fn (si x) = si' (fi x)*)
    val mor_spec =
      let
        fun mk_fbetw f B1 B2 z z' =
          mk_Ball B1 (Term.absfree z' (HOLogic.mk_mem (f $ z, B2)));
        fun mk_mor B mapAsBs f s s' z z' =
          mk_Ball B (Term.absfree z' (HOLogic.mk_eq
            (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ z]), s' $ (f $ z))));
        val rhs = HOLogic.mk_conj
          (Library.foldr1 HOLogic.mk_conj (@{map 5} mk_fbetw fs Bs B's zs zs'),
           Library.foldr1 HOLogic.mk_conj (@{map 7} mk_mor Bs mapsAsBs fs ss s's zs zs'))
      in
        fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss @ B's @ s's @ fs) rhs
      end;

    val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) =
      lthy
      |> (snd o Local_Theory.begin_nested)
      |> Local_Theory.define ((mor_bind, NoSyn), (mor_def_bind, mor_spec))
      ||> `Local_Theory.end_nested;

    val phi = Proof_Context.export_morphism lthy_old lthy;
    val mor = dest_Const_name (Morphism.term phi mor_free);
    val mor_def = mk_unabs_def (5 * n) (HOLogic.mk_obj_eq (Morphism.thm phi mor_def_free));

    fun mk_mor Bs1 ss1 Bs2 ss2 fs =
      let
        val args = Bs1 @ ss1 @ Bs2 @ ss2 @ fs;
        val Ts = map fastype_of (Bs1 @ ss1 @ Bs2 @ ss2 @ fs);
        val morT = Library.foldr (op -->) (Ts, HOLogic.boolT);
      in
        Term.list_comb (Const (mor, morT), args)
      end;

    val ((((((((((((((zs, z's), Bs), Bs_copy), B's), B''s), ss), s's), s''s), fs), fs_copy), gs),
        RFs), Rs), _) =
      lthy
      |> mk_Frees "b" activeAs
      ||>> mk_Frees "b" activeBs
      ||>> mk_Frees "B" BTs
      ||>> mk_Frees "B" BTs
      ||>> mk_Frees "B'" B'Ts
      ||>> mk_Frees "B''" B''Ts
      ||>> mk_Frees "s" sTs
      ||>> mk_Frees "s'" s'Ts
      ||>> mk_Frees "s''" s''Ts
      ||>> mk_Frees "f" fTs
      ||>> mk_Frees "f" fTs
      ||>> mk_Frees "g" gTs
      ||>> mk_Frees "x" FRTs
      ||>> mk_Frees "R" setRTs;

    val mor_prem = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs);

    val (mor_image_thms, morE_thms) =
      let
        val prem = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs);
        fun mk_image_goal f B1 B2 =
          Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_leq (mk_image f $ B1) B2));
        val image_goals = @{map 3} mk_image_goal fs Bs B's;
        fun mk_elim_goal B mapAsBs f s s' x =
          Logic.list_implies ([prem, mk_Trueprop_mem (x, B)],
            mk_Trueprop_eq (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ x]), s' $ (f $ x)));
        val elim_goals = @{map 6} mk_elim_goal Bs mapsAsBs fs ss s's zs;
        fun prove goal =
          Variable.add_free_names lthy goal []
          |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
            mk_mor_elim_tac ctxt mor_def))
          |> Thm.close_derivation \<^here>;
      in
        (map prove image_goals, map prove elim_goals)
      end;

    val mor_image'_thms = map (fn thm => @{thm set_mp} OF [thm, @{thm imageI}]) mor_image_thms;

    val mor_incl_thm =
      let
        val prems = map2 (HOLogic.mk_Trueprop oo mk_leq) Bs Bs_copy;
        val concl = HOLogic.mk_Trueprop (mk_mor Bs ss Bs_copy ss active_ids);
        val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
      in
        Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
          (fn {context = ctxt, prems = _} => mk_mor_incl_tac ctxt mor_def map_ids)
        |> Thm.close_derivation \<^here>
      end;

    val mor_id_thm = mor_incl_thm OF (replicate n @{thm subset_refl});

    val mor_comp_thm =
      let
        val prems =
          [HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs),
           HOLogic.mk_Trueprop (mk_mor B's s's B''s s''s gs)];
        val concl =
          HOLogic.mk_Trueprop (mk_mor Bs ss B''s s''s (map2 (curry HOLogic.mk_comp) gs fs));
        val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
      in
        Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
          (fn {context = ctxt, prems = _} =>
            mk_mor_comp_tac ctxt mor_def mor_image'_thms morE_thms map_comp_id_thms)
        |> Thm.close_derivation \<^here>
      end;

    val mor_cong_thm =
      let
        val prems = map HOLogic.mk_Trueprop
         (map2 (curry HOLogic.mk_eq) fs_copy fs @ [mk_mor Bs ss B's s's fs])
        val concl = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs_copy);
        val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
      in
        Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
          (fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' assume_tac ctxt) 1)
        |> Thm.close_derivation \<^here>
      end;

    val mor_UNIV_thm =
      let
        fun mk_conjunct mapAsBs f s s' = HOLogic.mk_eq
            (HOLogic.mk_comp (Term.list_comb (mapAsBs, passive_ids @ fs), s),
            HOLogic.mk_comp (s', f));
        val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs;
        val rhs = Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct mapsAsBs fs ss s's);
        val vars = fold (Variable.add_free_names lthy) [lhs, rhs] [];
      in
        Goal.prove_sorry lthy vars [] (mk_Trueprop_eq (lhs, rhs))
          (fn {context = ctxt, prems = _} => mk_mor_UNIV_tac ctxt morE_thms mor_def)
        |> Thm.close_derivation \<^here>
      end;

    val mor_str_thm =
      let
        val maps = map2 (fn Ds => fn bnf => Term.list_comb
          (mk_map_of_bnf Ds allAs (passiveAs @ FTsAs) bnf, passive_ids @ ss)) Dss bnfs;
        val goal = HOLogic.mk_Trueprop (mk_mor active_UNIVs ss (map HOLogic.mk_UNIV FTsAs) maps ss);
        val vars = Variable.add_free_names lthy goal [];
      in
        Goal.prove_sorry lthy vars [] goal
          (fn {context = ctxt, prems = _} => mk_mor_str_tac ctxt ks mor_UNIV_thm)
        |> Thm.close_derivation \<^here>
      end;

    val timer = time (timer "Morphism definition & thms");

    (* bisimulation *)

    val bis_bind = mk_internal_b bisN;
    val bis_def_bind = (Thm.def_binding bis_bind, []);

    fun mk_bis_le_conjunct R B1 B2 = mk_leq R (mk_Times (B1, B2));
    val bis_le = Library.foldr1 HOLogic.mk_conj (@{map 3} mk_bis_le_conjunct Rs Bs B's)

    val bis_spec =
      let
        val fst_args = passive_ids @ fsts;
        val snd_args = passive_ids @ snds;
        fun mk_bis R s s' b1 b2 RF map1 map2 sets =
          list_all_free [b1, b2] (HOLogic.mk_imp
            (HOLogic.mk_mem (HOLogic.mk_prod (b1, b2), R),
            mk_Bex (mk_in (passive_UNIVs @ Rs) sets (snd (dest_Free RF)))
              (Term.absfree (dest_Free RF) (HOLogic.mk_conj
                (HOLogic.mk_eq (Term.list_comb (map1, fst_args) $ RF, s $ b1),
                HOLogic.mk_eq (Term.list_comb (map2, snd_args) $ RF, s' $ b2))))));

        val rhs = HOLogic.mk_conj
          (bis_le, Library.foldr1 HOLogic.mk_conj
            (@{map 9} mk_bis Rs ss s's zs z's RFs map_fsts map_snds bis_setss))
      in
        fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss @ B's @ s's @ Rs) rhs
      end;

    val ((bis_free, (_, bis_def_free)), (lthy, lthy_old)) =
      lthy
      |> (snd o Local_Theory.begin_nested)
      |> Local_Theory.define ((bis_bind, NoSyn), (bis_def_bind, bis_spec))
      ||> `Local_Theory.end_nested;

    val phi = Proof_Context.export_morphism lthy_old lthy;
    val bis = dest_Const_name (Morphism.term phi bis_free);
    val bis_def = mk_unabs_def (5 * n) (HOLogic.mk_obj_eq (Morphism.thm phi bis_def_free));

    fun mk_bis Bs1 ss1 Bs2 ss2 Rs =
      let
        val args = Bs1 @ ss1 @ Bs2 @ ss2 @ Rs;
        val Ts = map fastype_of args;
        val bisT = Library.foldr (op -->) (Ts, HOLogic.boolT);
      in
        Term.list_comb (Const (bis, bisT), args)
      end;

    val (((((((((((((((((zs, z's), Bs), B's), B''s), ss), s's), s''s), fs), (Rtuple, Rtuple')), Rs),
        Rs_copy), R's), sRs), (idx, idx')), Idx), Ris), _) =
      lthy
      |> mk_Frees "b" activeAs
      ||>> mk_Frees "b" activeBs
      ||>> mk_Frees "B" BTs
      ||>> mk_Frees "B'" B'Ts
      ||>> mk_Frees "B''" B''Ts
      ||>> mk_Frees "s" sTs
      ||>> mk_Frees "s'" s'Ts
      ||>> mk_Frees "s''" s''Ts
      ||>> mk_Frees "f" fTs
      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "Rtuple") all_sbisT
      ||>> mk_Frees "R" setRTs
      ||>> mk_Frees "R" setRTs
      ||>> mk_Frees "R'" setR'Ts
      ||>> mk_Frees "R" setsRTs
      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") idxT
      ||>> yield_singleton (mk_Frees "I") (HOLogic.mk_setT idxT)
      ||>> mk_Frees "Ri" (map (fn T => idxT --> T) setRTs);

    val bis_cong_thm =
      let
        val prems = map HOLogic.mk_Trueprop
         (mk_bis Bs ss B's s's Rs :: map2 (curry HOLogic.mk_eq) Rs_copy Rs)
        val concl = HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs_copy);
        val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
      in
        Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
          (fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' assume_tac ctxt) 1)
        |> Thm.close_derivation \<^here>
      end;

    val bis_rel_thm =
      let
        fun mk_conjunct R s s' b1 b2 rel =
          list_all_free [b1, b2] (HOLogic.mk_imp
            (HOLogic.mk_mem (HOLogic.mk_prod (b1, b2), R),
            Term.list_comb (rel, passive_eqs @ map mk_in_rel Rs) $ (s $ b1) $ (s' $ b2)));

        val rhs = HOLogic.mk_conj
          (bis_le, Library.foldr1 HOLogic.mk_conj
            (@{map 6} mk_conjunct Rs ss s's zs z's relsAsBs))
        val goal = mk_Trueprop_eq (mk_bis Bs ss B's s's Rs, rhs);
        val vars = Variable.add_free_names lthy goal [];
      in
        Goal.prove_sorry lthy vars [] goal
          (fn {context = ctxt, prems = _} => mk_bis_rel_tac ctxt m bis_def in_rels map_comps
            map_cong0s set_mapss)
        |> Thm.close_derivation \<^here>
      end;

    val bis_converse_thm =
      let
        val goal = Logic.mk_implies (HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs),
          HOLogic.mk_Trueprop (mk_bis B's s's Bs ss (map mk_converse Rs)));
        val vars = Variable.add_free_names lthy goal [];
      in
        Goal.prove_sorry lthy vars [] goal
          (fn {context = ctxt, prems = _} => mk_bis_converse_tac ctxt m bis_rel_thm rel_congs
            rel_converseps)
        |> Thm.close_derivation \<^here>
      end;

    val bis_O_thm =
      let
        val prems =
          [HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs),
           HOLogic.mk_Trueprop (mk_bis B's s's B''s s''s R's)];
        val concl =
          HOLogic.mk_Trueprop (mk_bis Bs ss B''s s''s (map2 (curry mk_rel_comp) Rs R's));
        val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
      in
        Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
          (fn {context = ctxt, prems = _} => mk_bis_O_tac ctxt m bis_rel_thm rel_congs le_rel_OOs)
        |> Thm.close_derivation \<^here>
      end;

    val bis_Gr_thm =
      let
        val concl = HOLogic.mk_Trueprop (mk_bis Bs ss B's s's (map2 mk_Gr Bs fs));
        val vars = fold (Variable.add_free_names lthy) ([coalg_prem, mor_prem, concl]) [];
      in
        Goal.prove_sorry lthy vars [] (Logic.list_implies ([coalg_prem, mor_prem], concl))
          (fn {context = ctxt, prems = _} => mk_bis_Gr_tac ctxt bis_rel_thm rel_Grps mor_image_thms
            morE_thms coalg_in_thms)
        |> Thm.close_derivation \<^here>
      end;

    val bis_image2_thm = bis_cong_thm OF
      ((bis_O_thm OF [bis_Gr_thm RS bis_converse_thm, bis_Gr_thm]) ::
      replicate n @{thm image2_Gr});

    val bis_Id_on_thm = bis_cong_thm OF ((mor_id_thm RSN (2, bis_Gr_thm)) ::
      replicate n @{thm Id_on_Gr});

    val bis_Union_thm =
      let
        val prem =
          HOLogic.mk_Trueprop (mk_Ball Idx
            (Term.absfree idx' (mk_bis Bs ss B's s's (map (fn R => R $ idx) Ris))));
        val concl =
          HOLogic.mk_Trueprop (mk_bis Bs ss B's s's (map (mk_UNION Idx) Ris));
        val vars = fold (Variable.add_free_names lthy) [prem, concl] [];
      in
        Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, concl))
          (fn {context = ctxt, prems = _} => mk_bis_Union_tac ctxt bis_def in_mono'_thms)
        |> Thm.close_derivation \<^here>
      end;

    (* self-bisimulation *)

    fun mk_sbis Bs ss Rs = mk_bis Bs ss Bs ss Rs;

    (* largest self-bisimulation *)

    val lsbis_binds = mk_internal_bs lsbisN;
    fun lsbis_bind i = nth lsbis_binds (i - 1);
    val lsbis_def_bind = rpair [] o Thm.def_binding o lsbis_bind;

    val all_sbis = HOLogic.mk_Collect (fst Rtuple', snd Rtuple', list_exists_free sRs
      (HOLogic.mk_conj (HOLogic.mk_eq (Rtuple, HOLogic.mk_tuple sRs), mk_sbis Bs ss sRs)));

    fun lsbis_spec i =
      fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss)
        (mk_UNION all_sbis (Term.absfree Rtuple' (mk_nthN n Rtuple i)));

    val ((lsbis_frees, (_, lsbis_def_frees)), (lthy, lthy_old)) =
      lthy
      |> (snd o Local_Theory.begin_nested)
      |> fold_map (fn i => Local_Theory.define
        ((lsbis_bind i, NoSyn), (lsbis_def_bind i, lsbis_spec i))) ks
      |>> apsnd split_list o split_list
      ||> `Local_Theory.end_nested;

    val phi = Proof_Context.export_morphism lthy_old lthy;

    val lsbis_defs = map (fn def =>
      mk_unabs_def (2 * n) (HOLogic.mk_obj_eq (Morphism.thm phi def))) lsbis_def_frees;
    val lsbiss = map (dest_Const_name o Morphism.term phi) lsbis_frees;

    fun mk_lsbis Bs ss i =
      let
        val args = Bs @ ss;
        val Ts = map fastype_of args;
        val RT = mk_relT (`I (HOLogic.dest_setT (fastype_of (nth Bs (i - 1)))));
        val lsbisT = Library.foldr (op -->) (Ts, RT);
      in
        Term.list_comb (Const (nth lsbiss (i - 1), lsbisT), args)
      end;

    val (((((zs, zs'), Bs), ss), sRs), _) =
      lthy
      |> mk_Frees' "b" activeAs
      ||>> mk_Frees "B" BTs
      ||>> mk_Frees "s" sTs
      ||>> mk_Frees "R" setsRTs;

    val sbis_prem = HOLogic.mk_Trueprop (mk_sbis Bs ss sRs);
    val coalg_prem = HOLogic.mk_Trueprop (mk_coalg Bs ss);

    val sbis_lsbis_thm =
      let
        val goal = HOLogic.mk_Trueprop (mk_sbis Bs ss (map (mk_lsbis Bs ss) ks));
        val vars = Variable.add_free_names lthy goal [];
      in
        Goal.prove_sorry lthy vars [] goal
          (fn {context = ctxt, prems = _} =>
            mk_sbis_lsbis_tac ctxt lsbis_defs bis_Union_thm bis_cong_thm)
        |> Thm.close_derivation \<^here>
      end;

    val lsbis_incl_thms = map (fn i => sbis_lsbis_thm RS
      (bis_def RS iffD1 RS conjunct1 RS mk_conjunctN n i)) ks;
    val lsbisE_thms = map (fn i => (mk_specN 2 (sbis_lsbis_thm RS
      (bis_def RS iffD1 RS conjunct2 RS mk_conjunctN n i))) RS mp) ks;

    val incl_lsbis_thms =
      let
        fun mk_concl i R = HOLogic.mk_Trueprop (mk_leq R (mk_lsbis Bs ss i));
        val goals = map2 (fn i => fn R => Logic.mk_implies (sbis_prem, mk_concl i R)) ks sRs;
      in
        @{map 3} (fn goal => fn i => fn def =>
          Variable.add_free_names lthy goal []
          |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
            mk_incl_lsbis_tac ctxt n i def))
          |> Thm.close_derivation \<^here>)
        goals ks lsbis_defs
      end;

    val equiv_lsbis_thms =
      let
        fun mk_concl i B = HOLogic.mk_Trueprop (mk_equiv B (mk_lsbis Bs ss i));
        val goals = map2 (fn i => fn B => Logic.mk_implies (coalg_prem, mk_concl i B)) ks Bs;
      in
        @{map 3} (fn goal => fn l_incl => fn incl_l =>
          Variable.add_free_names lthy goal []
          |> (fn vars => Goal.prove_sorry lthy vars [] goal
            (fn {context = ctxt, prems = _} => mk_equiv_lsbis_tac ctxt sbis_lsbis_thm l_incl incl_l
              bis_Id_on_thm bis_converse_thm bis_O_thm)
          |> Thm.close_derivation \<^here>))
        goals lsbis_incl_thms incl_lsbis_thms
      end;

    val timer = time (timer "Bisimulations");

    (* bounds *)

    val (lthy, sbd', sbdT', sbd_card_order', sbd_Cinfinite', sbd_Card_order', set_sbdss') =
      if n = 1
      then (lthy, sum_bd, sum_bdT, bd_card_order, bd_Cinfinite, bd_Card_order, set_bdss)
      else
        let
          val sbdT_bind = mk_internal_b sum_bdTN;

          val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) =
            typedef (sbdT_bind, sum_bdT_params', NoSyn)
              (HOLogic.mk_UNIV sum_bdT) NONE (fn ctxt =>
                EVERY' [rtac ctxt exI, rtac ctxt @{thm UNIV_I}] 1) lthy;

          val sbdT = Type (sbdT_name, sum_bdT_params);
          val Abs_sbdT = Const (#Abs_name sbdT_glob_info, sum_bdT --> sbdT);

          val sbd_bind = mk_internal_b sum_bdN;
          val sbd_def_bind = (Thm.def_binding sbd_bind, []);

          val sbd_spec = mk_dir_image sum_bd Abs_sbdT;

          val ((sbd_free, (_, sbd_def_free)), (lthy, lthy_old)) =
            lthy
            |> (snd o Local_Theory.begin_nested)
            |> Local_Theory.define ((sbd_bind, NoSyn), (sbd_def_bind, sbd_spec))
            ||> `Local_Theory.end_nested;

          val phi = Proof_Context.export_morphism lthy_old lthy;

          val sbd_def = HOLogic.mk_obj_eq (Morphism.thm phi sbd_def_free);
          val sbd = Const (dest_Const_name (Morphism.term phi sbd_free), mk_relT (`I sbdT));

          val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info);
          val Abs_sbdT_bij = mk_Abs_bij_thm lthy Abs_sbdT_inj (#Abs_cases sbdT_loc_info);

          val sum_Cinfinite = mk_sum_Cinfinite bd_Cinfinites;
          val sum_Card_order = sum_Cinfinite RS conjunct2;
          val sum_card_order = mk_sum_card_order bd_card_orders;

          val sbd_ordIso = @{thm ssubst_Pair_rhs} OF
            [@{thm dir_image} OF [Abs_sbdT_inj, sum_Card_order],
            sbd_def
          ];
          val sbd_card_order = @{thm iffD2[OF arg_cong[of _ _ card_order]]} OF
            [sbd_def, @{thm card_order_dir_image} OF [Abs_sbdT_bij, sum_card_order]];
          val sbd_Cinfinite = @{thm Cinfinite_cong} OF [sbd_ordIso, sum_Cinfinite];
          val sbd_Card_order = conjunct2 OF [sbd_Cinfinite];

          fun mk_set_sbd i bd_Card_order bds =
            map (fn thm => @{thm ordLess_ordIso_trans} OF
              [mk_ordLess_csum n i thm OF [bd_Card_order], sbd_ordIso]) bds;
          val set_sbdss = @{map 3} mk_set_sbd ks bd_Card_orders set_bdss;
       in
         (lthy, sbd, sbdT, sbd_card_order, sbd_Cinfinite, sbd_Card_order, set_sbdss)
       end;
    val sbd = mk_card_suc sbd';
    val sbdT = fst (dest_relT (fastype_of sbd));
    val sbd_card_order = @{thm card_order_card_suc} OF [sbd_card_order'];
    val sbd_Cinfinite = @{thm Cinfinite_card_suc} OF [sbd_Cinfinite', sbd_card_order'];
    val sbd_Card_order = @{thm Card_order_card_suc} OF [sbd_card_order'];
    val sbd_regularCard = @{thm regularCard_card_suc} OF [sbd_card_order', sbd_Cinfinite'];
    val set_sbdss = map (map (fn thm => @{thm ordLess_transitive} OF [
      thm, @{thm card_suc_greater} OF [sbd_card_order']
    ])) set_sbdss';

    val sbdTs = replicate n sbdT;
    val sum_sbdT = mk_sumTN sbdTs;
    val sum_sbd_listT = HOLogic.listT sum_sbdT;
    val sum_sbd_list_setT = HOLogic.mk_setT sum_sbd_listT;
    val bdTs = passiveAs @ replicate n sbdT;
    val to_sbd_maps = @{map 4} mk_map_of_bnf Dss Ass (replicate n bdTs) bnfs;
    val bdFTs = mk_FTs bdTs;
    val sbdFT = mk_sumTN bdFTs;
    val treeT = HOLogic.mk_prodT (sum_sbd_list_setT, sum_sbd_listT --> sbdFT);
    val treeQT = HOLogic.mk_setT treeT;
    val treeTs = passiveAs @ replicate n treeT;
    val treeQTs = passiveAs @ replicate n treeQT;
    val treeFTs = mk_FTs treeTs;
    val tree_maps = @{map 4} mk_map_of_bnf Dss (replicate n bdTs) (replicate n treeTs) bnfs;
    val final_maps = @{map 4} mk_map_of_bnf Dss (replicate n treeTs) (replicate n treeQTs) bnfs;
    val isNode_setss = mk_setss (passiveAs @ replicate n sbdT);

    val root = HOLogic.mk_set sum_sbd_listT [HOLogic.mk_list sum_sbdT []];
    val Zero = HOLogic.mk_tuple (map (fn U => absdummy U root) activeAs);
    val Lev_recT = fastype_of Zero;

    val Nil = HOLogic.mk_tuple (@{map 3} (fn i => fn z => fn z'=>
      Term.absfree z' (mk_InN activeAs z i)) ks zs zs');
    val rv_recT = fastype_of Nil;

    val (((((((((((((((zs, zs'), zs_copy), ss), (nat, nat')),
        (sumx, sumx')), (kks, kks')), (kl, kl')), (kl_copy, kl'_copy)), (Kl, Kl')), (lab, lab')),
        (Kl_lab, Kl_lab')), xs), (Lev_rec, Lev_rec')), (rv_rec, rv_rec')), _) =
      lthy
      |> mk_Frees' "b" activeAs
      ||>> mk_Frees "b" activeAs
      ||>> mk_Frees "s" sTs
      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "n") HOLogic.natT
      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "sumx") sum_sbdT
      ||>> mk_Frees' "k" sbdTs
      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "kl") sum_sbd_listT
      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "kl") sum_sbd_listT
      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "Kl") sum_sbd_list_setT
      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "lab") (sum_sbd_listT --> sbdFT)
      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "Kl_lab") treeT
      ||>> mk_Frees "x" bdFTs
      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "rec") Lev_recT
      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "rec") rv_recT;

    val (k, k') = (hd kks, hd kks')

    val timer = time (timer "Bounds");

    (* tree coalgebra *)

    val isNode_binds = mk_internal_bs isNodeN;
    fun isNode_bind i = nth isNode_binds (i - 1);
    val isNode_def_bind = rpair [] o Thm.def_binding o isNode_bind;

    val isNodeT =
      Library.foldr (op -->) (map fastype_of [Kl, lab, kl], HOLogic.boolT);

    val Succs = @{map 3} (fn i => fn k => fn k' =>
      HOLogic.mk_Collect (fst k', snd k', HOLogic.mk_mem (mk_InN sbdTs k i, mk_Succ Kl kl)))
      ks kks kks';

    fun isNode_spec sets x i =
      let
        val active_sets = drop m (map (fn set => set $ x) sets);
        val rhs = list_exists_free [x]
          (Library.foldr1 HOLogic.mk_conj (HOLogic.mk_eq (lab $ kl, mk_InN bdFTs x i) ::
          map2 (curry HOLogic.mk_eq) active_sets Succs));
      in
        fold_rev (Term.absfree o Term.dest_Free) [Kl, lab, kl] rhs
      end;

    val ((isNode_frees, (_, isNode_def_frees)), (lthy, lthy_old)) =
      lthy
      |> (snd o Local_Theory.begin_nested)
      |> @{fold_map 3} (fn i => fn x => fn sets => Local_Theory.define
        ((isNode_bind i, NoSyn), (isNode_def_bind i, isNode_spec sets x i)))
        ks xs isNode_setss
      |>> apsnd split_list o split_list
      ||> `Local_Theory.end_nested;

    val phi = Proof_Context.export_morphism lthy_old lthy;

    val isNode_defs = map (fn def =>
      mk_unabs_def 3 (HOLogic.mk_obj_eq (Morphism.thm phi def))) isNode_def_frees;
    val isNodes = map (dest_Const_name o Morphism.term phi) isNode_frees;

    fun mk_isNode kl i =
      Term.list_comb (Const (nth isNodes (i - 1), isNodeT), [Kl, lab, kl]);

    val isTree =
      let
        val empty = HOLogic.mk_mem (HOLogic.mk_list sum_sbdT [], Kl);

        val tree = mk_Ball Kl (Term.absfree kl'
          (Library.foldr1 HOLogic.mk_conj (@{map 4} (fn Succ => fn i => fn k => fn k' =>
            mk_Ball Succ (Term.absfree k' (mk_isNode
              (mk_append (kl, HOLogic.mk_list sum_sbdT [mk_InN sbdTs k i])) i)))
          Succs ks kks kks')));
      in
        HOLogic.mk_conj (empty, tree)
      end;

    val carT_binds = mk_internal_bs carTN;
    fun carT_bind i = nth carT_binds (i - 1);
    val carT_def_bind = rpair [] o Thm.def_binding o carT_bind;

    fun carT_spec i =
      HOLogic.mk_Collect (fst Kl_lab', snd Kl_lab', list_exists_free [Kl, lab]
        (HOLogic.mk_conj (HOLogic.mk_eq (Kl_lab, HOLogic.mk_prod (Kl, lab)),
          HOLogic.mk_conj (isTree, mk_isNode (HOLogic.mk_list sum_sbdT []) i))));

    val ((carT_frees, (_, carT_def_frees)), (lthy, lthy_old)) =
      lthy
      |> (snd o Local_Theory.begin_nested)
      |> fold_map (fn i =>
        Local_Theory.define ((carT_bind i, NoSyn), (carT_def_bind i, carT_spec i))) ks
      |>> apsnd split_list o split_list
      ||> `Local_Theory.end_nested;

    val phi = Proof_Context.export_morphism lthy_old lthy;

    val carT_defs = map (fn def => HOLogic.mk_obj_eq (Morphism.thm phi def)) carT_def_frees;
    val carTs = map (dest_Const_name o Morphism.term phi) carT_frees;

    fun mk_carT i = Const (nth carTs (i - 1), HOLogic.mk_setT treeT);

    val strT_binds = mk_internal_bs strTN;
    fun strT_bind i = nth strT_binds (i - 1);
    val strT_def_bind = rpair [] o Thm.def_binding o strT_bind;

    fun strT_spec mapFT FT i =
      let
        fun mk_f i k k' =
          let val in_k = mk_InN sbdTs k i;
          in Term.absfree k' (HOLogic.mk_prod (mk_Shift Kl in_k, mk_shift lab in_k)) end;

        val f = Term.list_comb (mapFT, passive_ids @ @{map 3} mk_f ks kks kks');
        val (fTs1, fTs2) = apsnd tl (chop (i - 1) (map (fn T => T --> FT) bdFTs));
        val fs = map mk_undefined fTs1 @ (f :: map mk_undefined fTs2);
      in
        HOLogic.mk_case_prod (Term.absfree Kl' (Term.absfree lab'
          (mk_case_sumN fs $ (lab $ HOLogic.mk_list sum_sbdT []))))
      end;

    val ((strT_frees, (_, strT_def_frees)), (lthy, lthy_old)) =
      lthy
      |> (snd o Local_Theory.begin_nested)
      |> @{fold_map 3} (fn i => fn mapFT => fn FT => Local_Theory.define
        ((strT_bind i, NoSyn), (strT_def_bind i, strT_spec mapFT FT i)))
        ks tree_maps treeFTs
      |>> apsnd split_list o split_list
      ||> `Local_Theory.end_nested;

    val phi = Proof_Context.export_morphism lthy_old lthy;

    val strT_defs = map (fn def =>
        trans OF [HOLogic.mk_obj_eq (Morphism.thm phi def) RS fun_cong, @{thm prod.case}])
      strT_def_frees;
    val strTs = map (dest_Const_name o Morphism.term phi) strT_frees;

    fun mk_strT FT i = Const (nth strTs (i - 1), treeT --> FT);

    val carTAs = map mk_carT ks;
    val strTAs = map2 mk_strT treeFTs ks;

    val coalgT_thm =
      Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (mk_coalg carTAs strTAs))
        (fn {context = ctxt, prems = _} => mk_coalgT_tac ctxt m
          (coalg_def :: isNode_defs @ carT_defs) strT_defs set_mapss)
      |> Thm.close_derivation \<^here>;

    val timer = time (timer "Tree coalgebra");

    fun mk_to_sbd s x i i' =
      mk_toCard (nth (nth setssAs (i - 1)) (m + i' - 1) $ (s $ x)) sbd;
    fun mk_from_sbd s x i i' =
      mk_fromCard (nth (nth setssAs (i - 1)) (m + i' - 1) $ (s $ x)) sbd;

    fun mk_to_sbd_thmss thm = map (map (fn set_sbd =>
      thm OF [@{thm ordLess_imp_ordLeq} OF [set_sbd], sbd_Card_order]) o drop m) set_sbdss;

    val to_sbd_inj_thmss = mk_to_sbd_thmss @{thm toCard_inj};
    val from_to_sbd_thmss = mk_to_sbd_thmss @{thm fromCard_toCard};

    val Lev_bind = mk_internal_b LevN;
    val Lev_def_bind = rpair [] (Thm.def_binding Lev_bind);

    val Lev_spec =
      let
        fun mk_Suc i s setsAs a a' =
          let
            val sets = drop m setsAs;
            fun mk_set i' set b =
              let
                val Cons = HOLogic.mk_eq (kl_copy,
                  mk_Cons (mk_InN sbdTs (mk_to_sbd s a i i' $ b) i') kl)
                val b_set = HOLogic.mk_mem (b, set $ (s $ a));
                val kl_rec = HOLogic.mk_mem (kl, mk_nthN n Lev_rec i' $ b);
              in
                HOLogic.mk_Collect (fst kl'_copy, snd kl'_copy, list_exists_free [b, kl]
                  (HOLogic.mk_conj (Cons, HOLogic.mk_conj (b_set, kl_rec))))
              end;
          in
            Term.absfree a' (Library.foldl1 mk_union (@{map 3} mk_set ks sets zs_copy))
          end;

        val Suc = Term.absdummy HOLogic.natT (Term.absfree Lev_rec'
          (HOLogic.mk_tuple (@{map 5} mk_Suc ks ss setssAs zs zs')));

        val rhs = mk_rec_nat Zero Suc;
      in
        fold_rev (Term.absfree o Term.dest_Free) ss rhs
      end;

    val ((Lev_free, (_, Lev_def_free)), (lthy, lthy_old)) =
      lthy
      |> (snd o Local_Theory.begin_nested)
      |> Local_Theory.define ((Lev_bind, NoSyn), (Lev_def_bind, Lev_spec))
      ||> `Local_Theory.end_nested;

    val phi = Proof_Context.export_morphism lthy_old lthy;

    val Lev_def = mk_unabs_def n (HOLogic.mk_obj_eq (Morphism.thm phi Lev_def_free));
    val Lev = dest_Const_name (Morphism.term phi Lev_free);

    fun mk_Lev ss nat i =
      let
        val Ts = map fastype_of ss;
        val LevT = Library.foldr (op -->) (Ts, HOLogic.natT -->
          HOLogic.mk_tupleT (map (fn U => domain_type U --> sum_sbd_list_setT) Ts));
      in
        mk_nthN n (Term.list_comb (Const (Lev, LevT), ss) $ nat) i
      end;

    val Lev_0s = flat (mk_rec_simps n @{thm rec_nat_0_imp} [Lev_def]);
    val Lev_Sucs = flat (mk_rec_simps n @{thm rec_nat_Suc_imp} [Lev_def]);

    val rv_bind = mk_internal_b rvN;
    val rv_def_bind = rpair [] (Thm.def_binding rv_bind);

    val rv_spec =
      let
        fun mk_Cons i s b b' =
          let
            fun mk_case i' =
              Term.absfree k' (mk_nthN n rv_rec i' $ (mk_from_sbd s b i i' $ k));
          in
            Term.absfree b' (mk_case_sumN (map mk_case ks) $ sumx)
          end;

        val Cons = Term.absfree sumx' (Term.absdummy sum_sbd_listT (Term.absfree rv_rec'
          (HOLogic.mk_tuple (@{map 4} mk_Cons ks ss zs zs'))));

        val rhs = mk_rec_list Nil Cons;
      in
        fold_rev (Term.absfree o Term.dest_Free) ss rhs
      end;

    val ((rv_free, (_, rv_def_free)), (lthy, lthy_old)) =
      lthy
      |> (snd o Local_Theory.begin_nested)
      |> Local_Theory.define ((rv_bind, NoSyn), (rv_def_bind, rv_spec))
      ||> `Local_Theory.end_nested;

    val phi = Proof_Context.export_morphism lthy_old lthy;

    val rv_def = mk_unabs_def n (HOLogic.mk_obj_eq (Morphism.thm phi rv_def_free));
    val rv = dest_Const_name (Morphism.term phi rv_free);

    fun mk_rv ss kl i =
      let
        val Ts = map fastype_of ss;
        val As = map domain_type Ts;
        val rvT = Library.foldr (op -->) (Ts, fastype_of kl -->
          HOLogic.mk_tupleT (map (fn U => U --> mk_sumTN As) As));
      in
        mk_nthN n (Term.list_comb (Const (rv, rvT), ss) $ kl) i
      end;

    val rv_Nils = flat (mk_rec_simps n @{thm rec_list_Nil_imp} [rv_def]);
    val rv_Conss = flat (mk_rec_simps n @{thm rec_list_Cons_imp} [rv_def]);

    val beh_binds = mk_internal_bs behN;
    fun beh_bind i = nth beh_binds (i - 1);
    val beh_def_bind = rpair [] o Thm.def_binding o beh_bind;

    fun beh_spec i z =
      let
        fun mk_case i to_sbd_map s k k' =
          Term.absfree k' (mk_InN bdFTs
            (Term.list_comb (to_sbd_map, passive_ids @ map (mk_to_sbd s k i) ks) $ (s $ k)) i);

        val Lab = Term.absfree kl'
          (mk_case_sumN (@{map 5} mk_case ks to_sbd_maps ss zs zs') $ (mk_rv ss kl i $ z));

        val rhs = HOLogic.mk_prod (mk_UNION (HOLogic.mk_UNIV HOLogic.natT)
          (Term.absfree nat' (mk_Lev ss nat i $ z)), Lab);
      in
        fold_rev (Term.absfree o Term.dest_Free) (ss @ [z]) rhs
      end;

    val ((beh_frees, (_, beh_def_frees)), (lthy, lthy_old)) =
      lthy
      |> (snd o Local_Theory.begin_nested)
      |> @{fold_map 2} (fn i => fn z =>
        Local_Theory.define ((beh_bind i, NoSyn), (beh_def_bind i, beh_spec i z))) ks zs
      |>> apsnd split_list o split_list
      ||> `Local_Theory.end_nested;

    val phi = Proof_Context.export_morphism lthy_old lthy;

    val beh_defs = map (fn def =>
      mk_unabs_def (n + 1) (HOLogic.mk_obj_eq (Morphism.thm phi def))) beh_def_frees;
    val behs = map (dest_Const_name o Morphism.term phi) beh_frees;

    fun mk_beh ss i =
      let
        val Ts = map fastype_of ss;
        val behT = Library.foldr (op -->) (Ts, nth activeAs (i - 1) --> treeT);
      in
        Term.list_comb (Const (nth behs (i - 1), behT), ss)
      end;

    val ((((((zs, zs_copy), zs_copy2), ss), (nat, nat')), (kl, kl')), _) =
      lthy
      |> mk_Frees "b" activeAs
      ||>> mk_Frees "b" activeAs
      ||>> mk_Frees "b" activeAs
      ||>> mk_Frees "s" sTs
      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "n") HOLogic.natT
      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "kl") sum_sbd_listT;

    val (length_Lev_thms, length_Lev'_thms) =
      let
        fun mk_conjunct i z = HOLogic.mk_imp (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z),
          HOLogic.mk_eq (mk_size kl, nat));
        val goal = list_all_free (kl :: zs)
          (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs));
        val vars = Variable.add_free_names lthy goal [];

        val cts = map (SOME o Thm.cterm_of lthy) [Term.absfree nat' goal, nat];

        val length_Lev =
          Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal)
            (fn {context = ctxt, prems = _} => mk_length_Lev_tac ctxt cts Lev_0s Lev_Sucs)
          |> Thm.close_derivation \<^here>;

        val length_Lev' = mk_specN (n + 1) length_Lev;
        val length_Levs = map (fn i => length_Lev' RS mk_conjunctN n i RS mp) ks;

        fun mk_goal i z = Logic.mk_implies
            (mk_Trueprop_mem (kl, mk_Lev ss nat i $ z),
            mk_Trueprop_mem (kl, mk_Lev ss (mk_size kl) i $ z));
        val goals = map2 mk_goal ks zs;

        val length_Levs' =
          map2 (fn goal => fn length_Lev =>
            Variable.add_free_names lthy goal []
            |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
              mk_length_Lev'_tac ctxt length_Lev))
            |> Thm.close_derivation \<^here>)
          goals length_Levs;
      in
        (length_Levs, length_Levs')
      end;

    val rv_last_thmss =
      let
        fun mk_conjunct i z i' z_copy = list_exists_free [z_copy]
          (HOLogic.mk_eq
            (mk_rv ss (mk_append (kl, HOLogic.mk_list sum_sbdT [mk_InN sbdTs k i'])) i $ z,
            mk_InN activeAs z_copy i'));
        val goal = list_all_free (k :: zs)
          (Library.foldr1 HOLogic.mk_conj (map2 (fn i => fn z =>
            Library.foldr1 HOLogic.mk_conj
              (map2 (mk_conjunct i z) ks zs_copy)) ks zs));
        val vars = Variable.add_free_names lthy goal [];

        val cTs = [SOME (Thm.ctyp_of lthy sum_sbdT)];
        val cts = map (SOME o Thm.cterm_of lthy) [Term.absfree kl' goal, kl];

        val rv_last =
          Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal)
            (fn {context = ctxt, prems = _} => mk_rv_last_tac ctxt cTs cts rv_Nils rv_Conss)
          |> Thm.close_derivation \<^here>;

        val rv_last' = mk_specN (n + 1) rv_last;
      in
        map (fn i => map (fn i' => rv_last' RS mk_conjunctN n i RS mk_conjunctN n i') ks) ks
      end;

    val set_Lev_thmsss =
      let
        fun mk_conjunct i z =
          let
            fun mk_conjunct' i' sets s z' =
              let
                fun mk_conjunct'' i'' set z'' = HOLogic.mk_imp
                  (HOLogic.mk_mem (z'', set $ (s $ z')),
                    HOLogic.mk_mem (mk_append (kl,
                      HOLogic.mk_list sum_sbdT [mk_InN sbdTs (mk_to_sbd s z' i' i'' $ z'') i'']),
                      mk_Lev ss (HOLogic.mk_Suc nat) i $ z));
              in
                HOLogic.mk_imp (HOLogic.mk_eq (mk_rv ss kl i $ z, mk_InN activeAs z' i'),
                  (Library.foldr1 HOLogic.mk_conj
                    (@{map 3} mk_conjunct'' ks (drop m sets) zs_copy2)))
              end;
          in
            HOLogic.mk_imp (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z),
              Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct' ks setssAs ss zs_copy))
          end;

        val goal = list_all_free (kl :: zs @ zs_copy @ zs_copy2)
          (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs));
        val vars = Variable.add_free_names lthy goal [];

        val cts = map (SOME o Thm.cterm_of lthy) [Term.absfree nat' goal, nat];

        val set_Lev =
          Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal)
            (fn {context = ctxt, prems = _} =>
              mk_set_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss)
          |> Thm.close_derivation \<^here>;

        val set_Lev' = mk_specN (3 * n + 1) set_Lev;
      in
        map (fn i => map (fn i' => map (fn i'' => set_Lev' RS
          mk_conjunctN n i RS mp RS
          mk_conjunctN n i' RS mp RS
          mk_conjunctN n i'' RS mp) ks) ks) ks
      end;

    val set_image_Lev_thmsss =
      let
        fun mk_conjunct i z =
          let
            fun mk_conjunct' i' sets =
              let
                fun mk_conjunct'' i'' set s z'' = HOLogic.mk_imp
                  (HOLogic.mk_eq (mk_rv ss kl i $ z, mk_InN activeAs z'' i''),
                  HOLogic.mk_mem (k, mk_image (mk_to_sbd s z'' i'' i') $ (set $ (s $ z''))));
              in
                HOLogic.mk_imp (HOLogic.mk_mem
                  (mk_append (kl, HOLogic.mk_list sum_sbdT [mk_InN sbdTs k i']),
                    mk_Lev ss (HOLogic.mk_Suc nat) i $ z),
                  (Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct'' ks sets ss zs_copy)))
              end;
          in
            HOLogic.mk_imp (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z),
              Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct' ks (drop m setssAs')))
          end;

        val goal = list_all_free (kl :: k :: zs @ zs_copy)
          (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs));
        val vars = Variable.add_free_names lthy goal [];

        val cts = map (SOME o Thm.cterm_of lthy) [Term.absfree nat' goal, nat];

        val set_image_Lev =
          Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal)
            (fn {context = ctxt, prems = _} =>
              mk_set_image_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss
                from_to_sbd_thmss to_sbd_inj_thmss)
          |> Thm.close_derivation \<^here>;

        val set_image_Lev' = mk_specN (2 * n + 2) set_image_Lev;
      in
        map (fn i => map (fn i' => map (fn i'' => set_image_Lev' RS
          mk_conjunctN n i RS mp RS
          mk_conjunctN n i'' RS mp RS
          mk_conjunctN n i' RS mp) ks) ks) ks
      end;

    val mor_beh_thm =
      let
        val goal = HOLogic.mk_Trueprop (mk_mor active_UNIVs ss carTAs strTAs (map (mk_beh ss) ks));
        val vars = Variable.add_free_names lthy goal [];
      in
        Goal.prove_sorry lthy vars [] goal
          (fn {context = ctxt, prems = _} => mk_mor_beh_tac ctxt m mor_def mor_cong_thm
            beh_defs carT_defs strT_defs isNode_defs
            to_sbd_inj_thmss from_to_sbd_thmss Lev_0s Lev_Sucs rv_Nils rv_Conss
            length_Lev_thms length_Lev'_thms rv_last_thmss set_Lev_thmsss
            set_image_Lev_thmsss set_mapss map_comp_id_thms map_cong0s)
        |> Thm.close_derivation \<^here>
      end;

    val timer = time (timer "Behavioral morphism");

    val lsbisAs = map (mk_lsbis carTAs strTAs) ks;

    fun mk_str_final i =
      mk_univ (HOLogic.mk_comp (Term.list_comb (nth final_maps (i - 1),
        passive_ids @ map mk_proj lsbisAs), nth strTAs (i - 1)));

    val car_finals = map2 mk_quotient carTAs lsbisAs;
    val str_finals = map mk_str_final ks;

    val coalgT_set_thmss = map (map (fn thm => coalgT_thm RS thm)) coalg_set_thmss;
    val equiv_LSBIS_thms = map (fn thm => coalgT_thm RS thm) equiv_lsbis_thms;

    val congruent_str_final_thms =
      let
        fun mk_goal R final_map strT =
          HOLogic.mk_Trueprop (mk_congruent R (HOLogic.mk_comp
            (Term.list_comb (final_map, passive_ids @ map mk_proj lsbisAs), strT)));

        val goals = @{map 3} mk_goal lsbisAs final_maps strTAs;
      in
        @{map 4} (fn goal => fn lsbisE => fn map_comp_id => fn map_cong0 =>
          Goal.prove_sorry lthy [] [] goal
            (fn {context = ctxt, prems = _} => mk_congruent_str_final_tac ctxt m lsbisE map_comp_id
              map_cong0 equiv_LSBIS_thms)
          |> Thm.close_derivation \<^here>)
        goals lsbisE_thms map_comp_id_thms map_cong0s
      end;

    val coalg_final_thm = Goal.prove_sorry lthy [] []
      (HOLogic.mk_Trueprop (mk_coalg car_finals str_finals))
      (fn {context = ctxt, prems = _} => mk_coalg_final_tac ctxt m coalg_def
        congruent_str_final_thms equiv_LSBIS_thms set_mapss coalgT_set_thmss)
      |> Thm.close_derivation \<^here>;

    val mor_T_final_thm = Goal.prove_sorry lthy [] []
      (HOLogic.mk_Trueprop (mk_mor carTAs strTAs car_finals str_finals (map mk_proj lsbisAs)))
      (fn {context = ctxt, prems = _} => mk_mor_T_final_tac ctxt mor_def congruent_str_final_thms
        equiv_LSBIS_thms)
      |> Thm.close_derivation \<^here>;

    val mor_final_thm = mor_comp_thm OF [mor_beh_thm, mor_T_final_thm];
    val in_car_final_thms = map (fn thm => thm OF [mor_final_thm, @{thm UNIV_I}]) mor_image'_thms;

    val timer = time (timer "Final coalgebra");

    val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
      lthy
      |> @{fold_map 4} (fn b => fn mx => fn car_final => fn in_car_final =>
          typedef (b, params, mx) car_final NONE
            (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt in_car_final] 1))
        bs mixfixes car_finals in_car_final_thms
      |>> apsnd split_list o split_list;

    val Ts = map (fn name => Type (name, params')) T_names;
    fun mk_Ts passive = map (Term.typ_subst_atomic (passiveAs ~~ passive)) Ts;
    val Ts' = mk_Ts passiveBs;
    val Rep_Ts = map2 (fn info => fn T => Const (#Rep_name info, T --> treeQT)) T_glob_infos Ts;
    val Abs_Ts = map2 (fn info => fn T => Const (#Abs_name info, treeQT --> T)) T_glob_infos Ts;

    val Reps = map #Rep T_loc_infos;
    val Rep_injects = map #Rep_inject T_loc_infos;
    val Abs_inverses = map #Abs_inverse T_loc_infos;

    val timer = time (timer "THE TYPEDEFs & Rep/Abs thms");

    val UNIVs = map HOLogic.mk_UNIV Ts;
    val FTs = mk_FTs (passiveAs @ Ts);
    val FTs_setss = mk_setss (passiveAs @ Ts);
    val map_FTs = map2 (fn Ds => mk_map_of_bnf Ds treeQTs (passiveAs @ Ts)) Dss bnfs;
    val unfold_fTs = map2 (curry op -->) activeAs Ts;

    val emptys = map (fn T => HOLogic.mk_set T []) passiveAs;
    val Zeros = map (fn empty =>
     HOLogic.mk_tuple (map (fn U => absdummy U empty) Ts)) emptys;
    val hrecTs = map fastype_of Zeros;

    val (((zs, ss), (Jzs, Jzs')), _) =
      lthy
      |> mk_Frees "b" activeAs
      ||>> mk_Frees "s" sTs
      ||>> mk_Frees' "z" Ts;

    fun dtor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtorN ^ "_");
    val dtor_def_bind = rpair [] o Binding.concealed o Thm.def_binding o dtor_bind;

    fun dtor_spec rep str map_FT Jz Jz' =
      Term.absfree Jz'
        (Term.list_comb (map_FT, map HOLogic.id_const passiveAs @ Abs_Ts) $ (str $ (rep $ Jz)));

    val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) =
      lthy
      |> (snd o Local_Theory.begin_nested)
      |> @{fold_map 6} (fn i => fn rep => fn str => fn mapx => fn Jz => fn Jz' =>
        Local_Theory.define ((dtor_bind i, NoSyn),
          (dtor_def_bind i, dtor_spec rep str mapx Jz Jz')))
        ks Rep_Ts str_finals map_FTs Jzs Jzs'
      |>> apsnd split_list o split_list
      ||> `Local_Theory.end_nested;

    val phi = Proof_Context.export_morphism lthy_old lthy;
    fun mk_dtors passive =
      map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (mk_params passive)) o
        Morphism.term phi) dtor_frees;
    val dtors = mk_dtors passiveAs;
    val dtor's = mk_dtors passiveBs;
    val dtor_defs =
      map (fn def => HOLogic.mk_obj_eq (Morphism.thm phi def) RS fun_cong) dtor_def_frees;

    val coalg_final_set_thmss = map (map (fn thm => coalg_final_thm RS thm)) coalg_set_thmss;
    val (mor_Rep_thm, mor_Abs_thm) =
      let
        val mor_Rep =
          Goal.prove_sorry lthy [] []
            (HOLogic.mk_Trueprop (mk_mor UNIVs dtors car_finals str_finals Rep_Ts))
            (fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt (mor_def :: dtor_defs) Reps
              Abs_inverses coalg_final_set_thmss map_comp_id_thms map_cong0L_thms)
          |> Thm.close_derivation \<^here>;

        val mor_Abs =
          Goal.prove_sorry lthy [] []
            (HOLogic.mk_Trueprop (mk_mor car_finals str_finals UNIVs dtors Abs_Ts))
            (fn {context = ctxt, prems = _} => mk_mor_Abs_tac ctxt (mor_def :: dtor_defs)
              Abs_inverses)
          |> Thm.close_derivation \<^here>;
      in
        (mor_Rep, mor_Abs)
      end;

    val timer = time (timer "dtor definitions & thms");

    fun unfold_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtor_unfoldN ^ "_");
    val unfold_def_bind = rpair [] o Binding.concealed o Thm.def_binding o unfold_bind;

    fun unfold_spec abs f z = fold_rev (Term.absfree o Term.dest_Free) (ss @ [z]) (abs $ (f $ z));

    val ((unfold_frees, (_, unfold_def_frees)), (lthy, lthy_old)) =
      lthy
      |> (snd o Local_Theory.begin_nested)
      |> @{fold_map 4} (fn i => fn abs => fn f => fn z =>
        Local_Theory.define ((unfold_bind i, NoSyn), (unfold_def_bind i, unfold_spec abs f z)))
          ks Abs_Ts (map (fn i => HOLogic.mk_comp
            (mk_proj (nth lsbisAs (i - 1)), mk_beh ss i)) ks) zs
      |>> apsnd split_list o split_list
      ||> `Local_Theory.end_nested;

    val phi = Proof_Context.export_morphism lthy_old lthy;
    val unfolds = map (Morphism.term phi) unfold_frees;
    val unfold_names = map dest_Const_name unfolds;
    fun mk_unfolds passives actives =
      @{map 3} (fn name => fn T => fn active =>
        Const (name, Library.foldr (op -->)
          (map2 (curry op -->) actives (mk_FTs (passives @ actives)), active --> T)))
      unfold_names (mk_Ts passives) actives;
    fun mk_unfold Ts ss i = Term.list_comb (Const (nth unfold_names (i - 1), Library.foldr (op -->)
      (map fastype_of ss, domain_type (fastype_of (nth ss (i - 1))) --> nth Ts (i - 1))), ss);
    val unfold_defs = map (fn def =>
      mk_unabs_def (n + 1) (HOLogic.mk_obj_eq (Morphism.thm phi def))) unfold_def_frees;

    val (((ss, TRs), unfold_fs), _) =
      lthy
      |> mk_Frees "s" sTs
      ||>> mk_Frees "r" (map (mk_relT o `I) Ts)
      ||>> mk_Frees "f" unfold_fTs;

    val mor_unfold_thm =
      let
        val Abs_inverses' = map2 (curry op RS) in_car_final_thms Abs_inverses;
        val morEs' = map (fn thm => (thm OF [mor_final_thm, @{thm UNIV_I}]) RS sym) morE_thms;
        val goal = HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors (map (mk_unfold Ts ss) ks));
        val vars = Variable.add_free_names lthy goal [];
      in
        Goal.prove_sorry lthy vars [] goal
          (fn {context = ctxt, prems = _} => mk_mor_unfold_tac ctxt m mor_UNIV_thm dtor_defs
            unfold_defs Abs_inverses' morEs' map_comp_id_thms map_cong0s)
        |> Thm.close_derivation \<^here>
      end;
    val dtor_unfold_thms = map (fn thm => (thm OF [mor_unfold_thm, @{thm UNIV_I}]) RS sym) morE_thms;

    val (raw_coind_thms, raw_coind_thm) =
      let
        val prem = HOLogic.mk_Trueprop (mk_sbis UNIVs dtors TRs);
        val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
          (map2 (fn R => fn T => mk_leq R (Id_const T)) TRs Ts));
        val vars = fold (Variable.add_free_names lthy) [prem, concl] [];
      in
        `split_conj_thm (Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, concl))
          (fn {context = ctxt, prems = _} => mk_raw_coind_tac ctxt bis_def bis_cong_thm bis_O_thm
            bis_converse_thm bis_Gr_thm tcoalg_thm coalgT_thm mor_T_final_thm sbis_lsbis_thm
            lsbis_incl_thms incl_lsbis_thms equiv_LSBIS_thms mor_Rep_thm Rep_injects)
          |> Thm.close_derivation \<^here>)
      end;

    val (unfold_unique_mor_thms, unfold_unique_mor_thm) =
      let
        val prem = HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors unfold_fs);
        fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_unfold Ts ss i);
        val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
          (map2 mk_fun_eq unfold_fs ks));
        val vars = fold (Variable.add_free_names lthy) [prem, unique] [];

        val bis_thm = tcoalg_thm RSN (2, tcoalg_thm RS bis_image2_thm);
        val mor_thm = mor_comp_thm OF [mor_final_thm, mor_Abs_thm];

        val unique_mor = Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, unique))
          (fn {context = ctxt, prems = _} => mk_unfold_unique_mor_tac ctxt raw_coind_thms
            bis_thm mor_thm unfold_defs)
          |> Thm.close_derivation \<^here>;
      in
        `split_conj_thm unique_mor
      end;

    val (dtor_unfold_unique_thms, dtor_unfold_unique_thm) = `split_conj_thm (split_conj_prems n
      (mor_UNIV_thm RS iffD2 RS unfold_unique_mor_thm));

    val unfold_dtor_thms = map (fn thm => mor_id_thm RS thm RS sym) unfold_unique_mor_thms;

    val unfold_o_dtor_thms =
      let
        val mor = mor_comp_thm OF [mor_str_thm, mor_unfold_thm];
      in
        map2 (fn unique => fn unfold_ctor =>
          trans OF [mor RS unique, unfold_ctor]) unfold_unique_mor_thms unfold_dtor_thms
      end;

    val timer = time (timer "unfold definitions & thms");

    val map_dtors = map2 (fn Ds => fn bnf =>
      Term.list_comb (mk_map_of_bnf Ds (passiveAs @ Ts) (passiveAs @ FTs) bnf,
        map HOLogic.id_const passiveAs @ dtors)) Dss bnfs;

    fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_");
    val ctor_def_bind = rpair [] o Binding.concealed o Thm.def_binding o ctor_bind;

    fun ctor_spec i = mk_unfold Ts map_dtors i;

    val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) =
      lthy
      |> (snd o Local_Theory.begin_nested)
      |> fold_map (fn i =>
        Local_Theory.define ((ctor_bind i, NoSyn), (ctor_def_bind i, ctor_spec i))) ks
      |>> apsnd split_list o split_list
      ||> `Local_Theory.end_nested;

    val phi = Proof_Context.export_morphism lthy_old lthy;
    fun mk_ctors params =
      map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ params) o Morphism.term phi)
        ctor_frees;
    val ctors = mk_ctors params';
    val ctor_defs = map (fn def => HOLogic.mk_obj_eq (Morphism.thm phi def)) ctor_def_frees;

    val ctor_o_dtor_thms = map2 (Local_Defs.fold lthy o single) ctor_defs unfold_o_dtor_thms;

    val dtor_o_ctor_thms =
      let
        fun mk_goal dtor ctor FT =
         mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT);
        val goals = @{map 3} mk_goal dtors ctors FTs;
      in
        @{map 5} (fn goal => fn ctor_def => fn unfold => fn map_comp_id => fn map_cong0L =>
          Goal.prove_sorry lthy [] [] goal
            (fn {context = ctxt, prems = _} => mk_dtor_o_ctor_tac ctxt ctor_def unfold map_comp_id
              map_cong0L unfold_o_dtor_thms)
          |> Thm.close_derivation \<^here>)
          goals ctor_defs dtor_unfold_thms map_comp_id_thms map_cong0L_thms
      end;

    val dtor_ctor_thms = map (fn thm => thm RS @{thm pointfree_idE}) dtor_o_ctor_thms;
    val ctor_dtor_thms = map (fn thm => thm RS @{thm pointfree_idE}) ctor_o_dtor_thms;

    val bij_dtor_thms =
      map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) ctor_o_dtor_thms dtor_o_ctor_thms;
    val inj_dtor_thms = map (fn thm => thm RS @{thm bij_is_inj}) bij_dtor_thms;
    val surj_dtor_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_dtor_thms;
    val dtor_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_dtor_thms;
    val dtor_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_dtor_thms;
--> --------------------

--> maximum size reached

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

quality100%

¤ Dauer der Verarbeitung: 0.34 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.