src/HOL/Tools/BNF/Tools/bnf_gfp.ML
changeset 55058 4e700eb471d4
parent 54899 7a01387c47d5
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/BNF/Tools/bnf_gfp.ML	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -0,0 +1,2827 @@
     1.4 +(*  Title:      HOL/BNF/Tools/bnf_gfp.ML
     1.5 +    Author:     Dmitriy Traytel, TU Muenchen
     1.6 +    Author:     Andrei Popescu, TU Muenchen
     1.7 +    Author:     Jasmin Blanchette, TU Muenchen
     1.8 +    Copyright   2012
     1.9 +
    1.10 +Codatatype construction.
    1.11 +*)
    1.12 +
    1.13 +signature BNF_GFP =
    1.14 +sig
    1.15 +  val construct_gfp: mixfix list -> binding list -> binding list -> binding list list ->
    1.16 +    binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
    1.17 +    local_theory -> BNF_FP_Util.fp_result * local_theory
    1.18 +end;
    1.19 +
    1.20 +structure BNF_GFP : BNF_GFP =
    1.21 +struct
    1.22 +
    1.23 +open BNF_Def
    1.24 +open BNF_Util
    1.25 +open BNF_Tactics
    1.26 +open BNF_Comp
    1.27 +open BNF_FP_Util
    1.28 +open BNF_FP_Def_Sugar
    1.29 +open BNF_GFP_Rec_Sugar
    1.30 +open BNF_GFP_Util
    1.31 +open BNF_GFP_Tactics
    1.32 +
    1.33 +datatype wit_tree = Wit_Leaf of int | Wit_Node of (int * int * int list) * wit_tree list;
    1.34 +
    1.35 +fun mk_tree_args (I, T) (I', Ts) = (sort_distinct int_ord (I @ I'), T :: Ts);
    1.36 +
    1.37 +fun finish Iss m seen i (nwit, I) =
    1.38 +  let
    1.39 +    val treess = map (fn j =>
    1.40 +        if j < m orelse member (op =) seen j then [([j], Wit_Leaf j)]
    1.41 +        else
    1.42 +          map_index (finish Iss m (insert (op =) j seen) j) (nth Iss (j - m))
    1.43 +          |> flat
    1.44 +          |> minimize_wits)
    1.45 +      I;
    1.46 +  in
    1.47 +    map (fn (I, t) => (I, Wit_Node ((i - m, nwit, filter (fn i => i < m) I), t)))
    1.48 +      (fold_rev (map_product mk_tree_args) treess [([], [])])
    1.49 +    |> minimize_wits
    1.50 +  end;
    1.51 +
    1.52 +fun tree_to_ctor_wit vars _ _ (Wit_Leaf j) = ([j], nth vars j)
    1.53 +  | tree_to_ctor_wit vars ctors witss (Wit_Node ((i, nwit, I), subtrees)) =
    1.54 +     (I, nth ctors i $ (Term.list_comb (snd (nth (nth witss i) nwit),
    1.55 +       map (snd o tree_to_ctor_wit vars ctors witss) subtrees)));
    1.56 +
    1.57 +fun tree_to_coind_wits _ (Wit_Leaf _) = []
    1.58 +  | tree_to_coind_wits lwitss (Wit_Node ((i, nwit, I), subtrees)) =
    1.59 +     ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees;
    1.60 +
    1.61 +(*all BNFs have the same lives*)
    1.62 +fun construct_gfp mixfixes map_bs rel_bs set_bss0 bs resBs (resDs, Dss) bnfs lthy =
    1.63 +  let
    1.64 +    val time = time lthy;
    1.65 +    val timer = time (Timer.startRealTimer ());
    1.66 +
    1.67 +    val live = live_of_bnf (hd bnfs);
    1.68 +    val n = length bnfs; (*active*)
    1.69 +    val ks = 1 upto n;
    1.70 +    val m = live - n; (*passive, if 0 don't generate a new BNF*)
    1.71 +    val ls = 1 upto m;
    1.72 +
    1.73 +    val note_all = Config.get lthy bnf_note_all;
    1.74 +    val b_names = map Binding.name_of bs;
    1.75 +    val b_name = mk_common_name b_names;
    1.76 +    val b = Binding.name b_name;
    1.77 +    val mk_internal_b = Binding.name #> Binding.prefix true b_name #> Binding.conceal;
    1.78 +    fun mk_internal_bs name =
    1.79 +      map (fn b =>
    1.80 +        Binding.prefix true b_name (Binding.prefix_name (name ^ "_") b) |> Binding.conceal) bs;
    1.81 +    val external_bs = map2 (Binding.prefix false) b_names bs
    1.82 +      |> note_all = false ? map Binding.conceal;
    1.83 +
    1.84 +    (* TODO: check if m, n, etc., are sane *)
    1.85 +
    1.86 +    val deads = fold (union (op =)) Dss resDs;
    1.87 +    val names_lthy = fold Variable.declare_typ deads lthy;
    1.88 +    val passives = map fst (subtract (op = o apsnd TFree) deads resBs);
    1.89 +
    1.90 +    (* tvars *)
    1.91 +    val ((((((passiveAs, activeAs), passiveBs), activeBs), passiveCs), activeCs), idxT) = names_lthy
    1.92 +      |> variant_tfrees passives
    1.93 +      ||>> mk_TFrees n
    1.94 +      ||>> variant_tfrees passives
    1.95 +      ||>> mk_TFrees n
    1.96 +      ||>> mk_TFrees m
    1.97 +      ||>> mk_TFrees n
    1.98 +      ||> fst o mk_TFrees 1
    1.99 +      ||> the_single;
   1.100 +
   1.101 +    val allAs = passiveAs @ activeAs;
   1.102 +    val allBs' = passiveBs @ activeBs;
   1.103 +    val Ass = replicate n allAs;
   1.104 +    val allBs = passiveAs @ activeBs;
   1.105 +    val Bss = replicate n allBs;
   1.106 +    val allCs = passiveAs @ activeCs;
   1.107 +    val allCs' = passiveBs @ activeCs;
   1.108 +    val Css' = replicate n allCs';
   1.109 +
   1.110 +    (* types *)
   1.111 +    val dead_poss =
   1.112 +      map (fn x => if member (op =) deads (TFree x) then SOME (TFree x) else NONE) resBs;
   1.113 +    fun mk_param NONE passive = (hd passive, tl passive)
   1.114 +      | mk_param (SOME a) passive = (a, passive);
   1.115 +    val mk_params = fold_map mk_param dead_poss #> fst;
   1.116 +
   1.117 +    fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs;
   1.118 +    val (params, params') = `(map Term.dest_TFree) (mk_params passiveAs);
   1.119 +    val (dead_params, dead_params') = `(map Term.dest_TFree) (subtract (op =) passiveAs params');
   1.120 +    val FTsAs = mk_FTs allAs;
   1.121 +    val FTsBs = mk_FTs allBs;
   1.122 +    val FTsCs = mk_FTs allCs;
   1.123 +    val ATs = map HOLogic.mk_setT passiveAs;
   1.124 +    val BTs = map HOLogic.mk_setT activeAs;
   1.125 +    val B'Ts = map HOLogic.mk_setT activeBs;
   1.126 +    val B''Ts = map HOLogic.mk_setT activeCs;
   1.127 +    val sTs = map2 (fn T => fn U => T --> U) activeAs FTsAs;
   1.128 +    val s'Ts = map2 (fn T => fn U => T --> U) activeBs FTsBs;
   1.129 +    val s''Ts = map2 (fn T => fn U => T --> U) activeCs FTsCs;
   1.130 +    val fTs = map2 (fn T => fn U => T --> U) activeAs activeBs;
   1.131 +    val self_fTs = map (fn T => T --> T) activeAs;
   1.132 +    val gTs = map2 (fn T => fn U => T --> U) activeBs activeCs;
   1.133 +    val all_gTs = map2 (fn T => fn U => T --> U) allBs allCs';
   1.134 +    val RTs = map2 (fn T => fn U => HOLogic.mk_prodT (T, U)) activeAs activeBs;
   1.135 +    val sRTs = map2 (fn T => fn U => HOLogic.mk_prodT (T, U)) activeAs activeAs;
   1.136 +    val R'Ts = map2 (fn T => fn U => HOLogic.mk_prodT (T, U)) activeBs activeCs;
   1.137 +    val setsRTs = map HOLogic.mk_setT sRTs;
   1.138 +    val setRTs = map HOLogic.mk_setT RTs;
   1.139 +    val all_sbisT = HOLogic.mk_tupleT setsRTs;
   1.140 +    val setR'Ts = map HOLogic.mk_setT R'Ts;
   1.141 +    val FRTs = mk_FTs (passiveAs @ RTs);
   1.142 +    val sumBsAs = map2 (curry mk_sumT) activeBs activeAs;
   1.143 +    val sumFTs = mk_FTs (passiveAs @ sumBsAs);
   1.144 +    val sum_sTs = map2 (fn T => fn U => T --> U) activeAs sumFTs;
   1.145 +
   1.146 +    (* terms *)
   1.147 +    val mapsAsAs = map4 mk_map_of_bnf Dss Ass Ass bnfs;
   1.148 +    val mapsAsBs = map4 mk_map_of_bnf Dss Ass Bss bnfs;
   1.149 +    val mapsBsCs' = map4 mk_map_of_bnf Dss Bss Css' bnfs;
   1.150 +    val mapsAsCs' = map4 mk_map_of_bnf Dss Ass Css' bnfs;
   1.151 +    val map_Inls = map4 mk_map_of_bnf Dss Bss (replicate n (passiveAs @ sumBsAs)) bnfs;
   1.152 +    val map_Inls_rev = map4 mk_map_of_bnf Dss (replicate n (passiveAs @ sumBsAs)) Bss bnfs;
   1.153 +    val map_fsts = map4 mk_map_of_bnf Dss (replicate n (passiveAs @ RTs)) Ass bnfs;
   1.154 +    val map_snds = map4 mk_map_of_bnf Dss (replicate n (passiveAs @ RTs)) Bss bnfs;
   1.155 +    fun mk_setss Ts = map3 mk_sets_of_bnf (map (replicate live) Dss)
   1.156 +      (map (replicate live) (replicate n Ts)) bnfs;
   1.157 +    val setssAs = mk_setss allAs;
   1.158 +    val setssAs' = transpose setssAs;
   1.159 +    val bis_setss = mk_setss (passiveAs @ RTs);
   1.160 +    val relsAsBs = map4 mk_rel_of_bnf Dss Ass Bss bnfs;
   1.161 +    val bds = map3 mk_bd_of_bnf Dss Ass bnfs;
   1.162 +    val sum_bd = Library.foldr1 (uncurry mk_csum) bds;
   1.163 +    val sum_bdT = fst (dest_relT (fastype_of sum_bd));
   1.164 +
   1.165 +    val emptys = map (fn T => HOLogic.mk_set T []) passiveAs;
   1.166 +    val Zeros = map (fn empty =>
   1.167 +     HOLogic.mk_tuple (map (fn U => absdummy U empty) activeAs)) emptys;
   1.168 +    val hrecTs = map fastype_of Zeros;
   1.169 +    val hsetTs = map (fn hrecT => Library.foldr (op -->) (sTs, HOLogic.natT --> hrecT)) hrecTs;
   1.170 +
   1.171 +    val (((((((((((((((((((((((((((((((((((zs, zs'), zs_copy), zs_copy2), z's), (ys, ys')),
   1.172 +      As), Bs), Bs_copy), B's), B''s), ss), sum_ss), s's), s''s), fs), fs_copy),
   1.173 +      self_fs), gs), all_gs), xFs), yFs), yFs_copy), RFs), (Rtuple, Rtuple')), (hrecs, hrecs')),
   1.174 +      (nat, nat')), Rs), Rs_copy), R's), sRs), (idx, idx')), Idx), Ris), Kss), names_lthy) = lthy
   1.175 +      |> mk_Frees' "b" activeAs
   1.176 +      ||>> mk_Frees "b" activeAs
   1.177 +      ||>> mk_Frees "b" activeAs
   1.178 +      ||>> mk_Frees "b" activeBs
   1.179 +      ||>> mk_Frees' "y" passiveAs
   1.180 +      ||>> mk_Frees "A" ATs
   1.181 +      ||>> mk_Frees "B" BTs
   1.182 +      ||>> mk_Frees "B" BTs
   1.183 +      ||>> mk_Frees "B'" B'Ts
   1.184 +      ||>> mk_Frees "B''" B''Ts
   1.185 +      ||>> mk_Frees "s" sTs
   1.186 +      ||>> mk_Frees "sums" sum_sTs
   1.187 +      ||>> mk_Frees "s'" s'Ts
   1.188 +      ||>> mk_Frees "s''" s''Ts
   1.189 +      ||>> mk_Frees "f" fTs
   1.190 +      ||>> mk_Frees "f" fTs
   1.191 +      ||>> mk_Frees "f" self_fTs
   1.192 +      ||>> mk_Frees "g" gTs
   1.193 +      ||>> mk_Frees "g" all_gTs
   1.194 +      ||>> mk_Frees "x" FTsAs
   1.195 +      ||>> mk_Frees "y" FTsBs
   1.196 +      ||>> mk_Frees "y" FTsBs
   1.197 +      ||>> mk_Frees "x" FRTs
   1.198 +      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "Rtuple") all_sbisT
   1.199 +      ||>> mk_Frees' "rec" hrecTs
   1.200 +      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "n") HOLogic.natT
   1.201 +      ||>> mk_Frees "R" setRTs
   1.202 +      ||>> mk_Frees "R" setRTs
   1.203 +      ||>> mk_Frees "R'" setR'Ts
   1.204 +      ||>> mk_Frees "R" setsRTs
   1.205 +      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") idxT
   1.206 +      ||>> yield_singleton (mk_Frees "I") (HOLogic.mk_setT idxT)
   1.207 +      ||>> mk_Frees "Ri" (map (fn T => idxT --> T) setRTs)
   1.208 +      ||>> mk_Freess "K" (map (fn AT => map (fn T => T --> AT) activeAs) ATs);
   1.209 +
   1.210 +    val passive_UNIVs = map HOLogic.mk_UNIV passiveAs;
   1.211 +    val passive_Id_ons = map mk_Id_on As;
   1.212 +    val active_UNIVs = map HOLogic.mk_UNIV activeAs;
   1.213 +    val sum_UNIVs = map HOLogic.mk_UNIV sumBsAs;
   1.214 +    val passive_ids = map HOLogic.id_const passiveAs;
   1.215 +    val active_ids = map HOLogic.id_const activeAs;
   1.216 +    val Inls = map2 Inl_const activeBs activeAs;
   1.217 +    val fsts = map fst_const RTs;
   1.218 +    val snds = map snd_const RTs;
   1.219 +
   1.220 +    (* thms *)
   1.221 +    val bd_card_orders = map bd_card_order_of_bnf bnfs;
   1.222 +    val bd_card_order = hd bd_card_orders
   1.223 +    val bd_Card_orders = map bd_Card_order_of_bnf bnfs;
   1.224 +    val bd_Card_order = hd bd_Card_orders;
   1.225 +    val bd_Cinfinites = map bd_Cinfinite_of_bnf bnfs;
   1.226 +    val bd_Cinfinite = hd bd_Cinfinites;
   1.227 +    val in_monos = map in_mono_of_bnf bnfs;
   1.228 +    val map_comp0s = map map_comp0_of_bnf bnfs;
   1.229 +    val sym_map_comps = map mk_sym map_comp0s;
   1.230 +    val map_comps = map map_comp_of_bnf bnfs;
   1.231 +    val map_cong0s = map map_cong0_of_bnf bnfs;
   1.232 +    val map_id0s = map map_id0_of_bnf bnfs;
   1.233 +    val map_ids = map map_id_of_bnf bnfs;
   1.234 +    val set_bdss = map set_bd_of_bnf bnfs;
   1.235 +    val set_mapss = map set_map_of_bnf bnfs;
   1.236 +    val rel_congs = map rel_cong_of_bnf bnfs;
   1.237 +    val rel_converseps = map rel_conversep_of_bnf bnfs;
   1.238 +    val rel_Grps = map rel_Grp_of_bnf bnfs;
   1.239 +    val rel_OOs = map rel_OO_of_bnf bnfs;
   1.240 +    val rel_OO_Grps = map rel_OO_Grp_of_bnf bnfs;
   1.241 +
   1.242 +    val timer = time (timer "Extracted terms & thms");
   1.243 +
   1.244 +    (* derived thms *)
   1.245 +
   1.246 +    (*map g1 ... gm g(m+1) ... g(m+n) (map id ... id f(m+1) ... f(m+n) x) =
   1.247 +      map g1 ... gm (g(m+1) o f(m+1)) ... (g(m+n) o f(m+n)) x*)
   1.248 +    fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp0 =
   1.249 +      let
   1.250 +        val lhs = Term.list_comb (mapBsCs, all_gs) $
   1.251 +          (Term.list_comb (mapAsBs, passive_ids @ fs) $ x);
   1.252 +        val rhs =
   1.253 +          Term.list_comb (mapAsCs, take m all_gs @ map HOLogic.mk_comp (drop m all_gs ~~ fs)) $ x;
   1.254 +      in
   1.255 +        Goal.prove_sorry lthy [] []
   1.256 +          (fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs)))
   1.257 +          (K (mk_map_comp_id_tac map_comp0))
   1.258 +        |> Thm.close_derivation
   1.259 +      end;
   1.260 +
   1.261 +    val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;
   1.262 +
   1.263 +    (*forall a : set(m+1) x. f(m+1) a = a; ...; forall a : set(m+n) x. f(m+n) a = a ==>
   1.264 +      map id ... id f(m+1) ... f(m+n) x = x*)
   1.265 +    fun mk_map_cong0L x mapAsAs sets map_cong0 map_id =
   1.266 +      let
   1.267 +        fun mk_prem set f z z' =
   1.268 +          HOLogic.mk_Trueprop
   1.269 +            (mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z))));
   1.270 +        val prems = map4 mk_prem (drop m sets) self_fs zs zs';
   1.271 +        val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x);
   1.272 +      in
   1.273 +        Goal.prove_sorry lthy [] []
   1.274 +          (fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
   1.275 +          (K (mk_map_cong0L_tac m map_cong0 map_id))
   1.276 +        |> Thm.close_derivation
   1.277 +      end;
   1.278 +
   1.279 +    val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
   1.280 +    val in_mono'_thms = map (fn thm =>
   1.281 +      (thm OF (replicate m subset_refl)) RS @{thm set_mp}) in_monos;
   1.282 +
   1.283 +    val map_arg_cong_thms =
   1.284 +      let
   1.285 +        val prems = map2 (curry mk_Trueprop_eq) yFs yFs_copy;
   1.286 +        val maps = map (fn mapx => Term.list_comb (mapx, all_gs)) mapsBsCs';
   1.287 +        val concls =
   1.288 +          map3 (fn x => fn y => fn mapx => mk_Trueprop_eq (mapx $ x, mapx $ y)) yFs yFs_copy maps;
   1.289 +        val goals =
   1.290 +          map4 (fn prem => fn concl => fn x => fn y =>
   1.291 +            fold_rev Logic.all (x :: y :: all_gs) (Logic.mk_implies (prem, concl)))
   1.292 +          prems concls yFs yFs_copy;
   1.293 +      in
   1.294 +        map (fn goal => Goal.prove_sorry lthy [] [] goal
   1.295 +          (K ((hyp_subst_tac lthy THEN' rtac refl) 1)) |> Thm.close_derivation) goals
   1.296 +      end;
   1.297 +
   1.298 +    val timer = time (timer "Derived simple theorems");
   1.299 +
   1.300 +    (* coalgebra *)
   1.301 +
   1.302 +    val coalg_bind = mk_internal_b (coN ^ algN) ;
   1.303 +    val coalg_name = Binding.name_of coalg_bind;
   1.304 +    val coalg_def_bind = (Thm.def_binding coalg_bind, []);
   1.305 +
   1.306 +    (*forall i = 1 ... n: (\<forall>x \<in> Bi. si \<in> Fi_in A1 .. Am B1 ... Bn)*)
   1.307 +    val coalg_spec =
   1.308 +      let
   1.309 +        val coalgT = Library.foldr (op -->) (ATs @ BTs @ sTs, HOLogic.boolT);
   1.310 +
   1.311 +        val ins = map3 mk_in (replicate n (As @ Bs)) setssAs FTsAs;
   1.312 +        fun mk_coalg_conjunct B s X z z' =
   1.313 +          mk_Ball B (Term.absfree z' (HOLogic.mk_mem (s $ z, X)));
   1.314 +
   1.315 +        val lhs = Term.list_comb (Free (coalg_name, coalgT), As @ Bs @ ss);
   1.316 +        val rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_coalg_conjunct Bs ss ins zs zs')
   1.317 +      in
   1.318 +        mk_Trueprop_eq (lhs, rhs)
   1.319 +      end;
   1.320 +
   1.321 +    val ((coalg_free, (_, coalg_def_free)), (lthy, lthy_old)) =
   1.322 +      lthy
   1.323 +      |> Specification.definition (SOME (coalg_bind, NONE, NoSyn), (coalg_def_bind, coalg_spec))
   1.324 +      ||> `Local_Theory.restore;
   1.325 +
   1.326 +    val phi = Proof_Context.export_morphism lthy_old lthy;
   1.327 +    val coalg = fst (Term.dest_Const (Morphism.term phi coalg_free));
   1.328 +    val coalg_def = Morphism.thm phi coalg_def_free;
   1.329 +
   1.330 +    fun mk_coalg As Bs ss =
   1.331 +      let
   1.332 +        val args = As @ Bs @ ss;
   1.333 +        val Ts = map fastype_of args;
   1.334 +        val coalgT = Library.foldr (op -->) (Ts, HOLogic.boolT);
   1.335 +      in
   1.336 +        Term.list_comb (Const (coalg, coalgT), args)
   1.337 +      end;
   1.338 +
   1.339 +    val coalg_prem = HOLogic.mk_Trueprop (mk_coalg As Bs ss);
   1.340 +
   1.341 +    val coalg_in_thms = map (fn i =>
   1.342 +      coalg_def RS iffD1 RS mk_conjunctN n i RS bspec) ks
   1.343 +
   1.344 +    val coalg_set_thmss =
   1.345 +      let
   1.346 +        val coalg_prem = HOLogic.mk_Trueprop (mk_coalg As Bs ss);
   1.347 +        fun mk_prem x B = HOLogic.mk_Trueprop (HOLogic.mk_mem (x, B));
   1.348 +        fun mk_concl s x B set = HOLogic.mk_Trueprop (mk_leq (set $ (s $ x)) B);
   1.349 +        val prems = map2 mk_prem zs Bs;
   1.350 +        val conclss = map3 (fn s => fn x => fn sets => map2 (mk_concl s x) (As @ Bs) sets)
   1.351 +          ss zs setssAs;
   1.352 +        val goalss = map3 (fn x => fn prem => fn concls => map (fn concl =>
   1.353 +          fold_rev Logic.all (x :: As @ Bs @ ss)
   1.354 +            (Logic.list_implies (coalg_prem :: [prem], concl))) concls) zs prems conclss;
   1.355 +      in
   1.356 +        map (fn goals => map (fn goal => Goal.prove_sorry lthy [] [] goal
   1.357 +          (K (mk_coalg_set_tac coalg_def)) |> Thm.close_derivation) goals) goalss
   1.358 +      end;
   1.359 +
   1.360 +    fun mk_tcoalg ATs BTs = mk_coalg (map HOLogic.mk_UNIV ATs) (map HOLogic.mk_UNIV BTs);
   1.361 +
   1.362 +    val tcoalg_thm =
   1.363 +      let
   1.364 +        val goal = fold_rev Logic.all ss
   1.365 +          (HOLogic.mk_Trueprop (mk_tcoalg passiveAs activeAs ss))
   1.366 +      in
   1.367 +        Goal.prove_sorry lthy [] [] goal
   1.368 +          (K (stac coalg_def 1 THEN CONJ_WRAP
   1.369 +            (K (EVERY' [rtac ballI, rtac CollectI,
   1.370 +              CONJ_WRAP' (K (EVERY' [rtac @{thm subset_UNIV}])) allAs] 1)) ss))
   1.371 +        |> Thm.close_derivation
   1.372 +      end;
   1.373 +
   1.374 +    val timer = time (timer "Coalgebra definition & thms");
   1.375 +
   1.376 +    (* morphism *)
   1.377 +
   1.378 +    val mor_bind = mk_internal_b morN;
   1.379 +    val mor_name = Binding.name_of mor_bind;
   1.380 +    val mor_def_bind = (Thm.def_binding mor_bind, []);
   1.381 +
   1.382 +    (*fbetw) forall i = 1 ... n: (\<forall>x \<in> Bi. fi x \<in> B'i)*)
   1.383 +    (*mor) forall i = 1 ... n: (\<forall>x \<in> Bi.
   1.384 +       Fi_map id ... id f1 ... fn (si x) = si' (fi x)*)
   1.385 +    val mor_spec =
   1.386 +      let
   1.387 +        val morT = Library.foldr (op -->) (BTs @ sTs @ B'Ts @ s'Ts @ fTs, HOLogic.boolT);
   1.388 +
   1.389 +        fun mk_fbetw f B1 B2 z z' =
   1.390 +          mk_Ball B1 (Term.absfree z' (HOLogic.mk_mem (f $ z, B2)));
   1.391 +        fun mk_mor B mapAsBs f s s' z z' =
   1.392 +          mk_Ball B (Term.absfree z' (HOLogic.mk_eq
   1.393 +            (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ z]), s' $ (f $ z))));
   1.394 +        val lhs = Term.list_comb (Free (mor_name, morT), Bs @ ss @ B's @ s's @ fs);
   1.395 +        val rhs = HOLogic.mk_conj
   1.396 +          (Library.foldr1 HOLogic.mk_conj (map5 mk_fbetw fs Bs B's zs zs'),
   1.397 +           Library.foldr1 HOLogic.mk_conj (map7 mk_mor Bs mapsAsBs fs ss s's zs zs'))
   1.398 +      in
   1.399 +        mk_Trueprop_eq (lhs, rhs)
   1.400 +      end;
   1.401 +
   1.402 +    val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) =
   1.403 +      lthy
   1.404 +      |> Specification.definition (SOME (mor_bind, NONE, NoSyn), (mor_def_bind, mor_spec))
   1.405 +      ||> `Local_Theory.restore;
   1.406 +
   1.407 +    val phi = Proof_Context.export_morphism lthy_old lthy;
   1.408 +    val mor = fst (Term.dest_Const (Morphism.term phi mor_free));
   1.409 +    val mor_def = Morphism.thm phi mor_def_free;
   1.410 +
   1.411 +    fun mk_mor Bs1 ss1 Bs2 ss2 fs =
   1.412 +      let
   1.413 +        val args = Bs1 @ ss1 @ Bs2 @ ss2 @ fs;
   1.414 +        val Ts = map fastype_of (Bs1 @ ss1 @ Bs2 @ ss2 @ fs);
   1.415 +        val morT = Library.foldr (op -->) (Ts, HOLogic.boolT);
   1.416 +      in
   1.417 +        Term.list_comb (Const (mor, morT), args)
   1.418 +      end;
   1.419 +
   1.420 +    val mor_prem = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs);
   1.421 +
   1.422 +    val (mor_image_thms, morE_thms) =
   1.423 +      let
   1.424 +        val prem = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs);
   1.425 +        fun mk_image_goal f B1 B2 = fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs)
   1.426 +          (Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_leq (mk_image f $ B1) B2)));
   1.427 +        val image_goals = map3 mk_image_goal fs Bs B's;
   1.428 +        fun mk_elim_goal B mapAsBs f s s' x =
   1.429 +          fold_rev Logic.all (x :: Bs @ ss @ B's @ s's @ fs)
   1.430 +            (Logic.list_implies ([prem, HOLogic.mk_Trueprop (HOLogic.mk_mem (x, B))],
   1.431 +              mk_Trueprop_eq (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ x]), s' $ (f $ x))));
   1.432 +        val elim_goals = map6 mk_elim_goal Bs mapsAsBs fs ss s's zs;
   1.433 +        fun prove goal =
   1.434 +          Goal.prove_sorry lthy [] [] goal (K (mk_mor_elim_tac mor_def))
   1.435 +          |> Thm.close_derivation;
   1.436 +      in
   1.437 +        (map prove image_goals, map prove elim_goals)
   1.438 +      end;
   1.439 +
   1.440 +    val mor_image'_thms = map (fn thm => @{thm set_mp} OF [thm, imageI]) mor_image_thms;
   1.441 +
   1.442 +    val mor_incl_thm =
   1.443 +      let
   1.444 +        val prems = map2 (HOLogic.mk_Trueprop oo mk_leq) Bs Bs_copy;
   1.445 +        val concl = HOLogic.mk_Trueprop (mk_mor Bs ss Bs_copy ss active_ids);
   1.446 +      in
   1.447 +        Goal.prove_sorry lthy [] []
   1.448 +          (fold_rev Logic.all (Bs @ ss @ Bs_copy) (Logic.list_implies (prems, concl)))
   1.449 +          (K (mk_mor_incl_tac mor_def map_ids))
   1.450 +        |> Thm.close_derivation
   1.451 +      end;
   1.452 +
   1.453 +    val mor_id_thm = mor_incl_thm OF (replicate n subset_refl);
   1.454 +
   1.455 +    val mor_comp_thm =
   1.456 +      let
   1.457 +        val prems =
   1.458 +          [HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs),
   1.459 +           HOLogic.mk_Trueprop (mk_mor B's s's B''s s''s gs)];
   1.460 +        val concl =
   1.461 +          HOLogic.mk_Trueprop (mk_mor Bs ss B''s s''s (map2 (curry HOLogic.mk_comp) gs fs));
   1.462 +      in
   1.463 +        Goal.prove_sorry lthy [] []
   1.464 +          (fold_rev Logic.all (Bs @ ss @ B's @ s's @ B''s @ s''s @ fs @ gs)
   1.465 +            (Logic.list_implies (prems, concl)))
   1.466 +          (K (mk_mor_comp_tac mor_def mor_image'_thms morE_thms map_comp_id_thms))
   1.467 +        |> Thm.close_derivation
   1.468 +      end;
   1.469 +
   1.470 +    val mor_cong_thm =
   1.471 +      let
   1.472 +        val prems = map HOLogic.mk_Trueprop
   1.473 +         (map2 (curry HOLogic.mk_eq) fs_copy fs @ [mk_mor Bs ss B's s's fs])
   1.474 +        val concl = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs_copy);
   1.475 +      in
   1.476 +        Goal.prove_sorry lthy [] []
   1.477 +          (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ fs_copy)
   1.478 +            (Logic.list_implies (prems, concl)))
   1.479 +          (K ((hyp_subst_tac lthy THEN' atac) 1))
   1.480 +        |> Thm.close_derivation
   1.481 +      end;
   1.482 +
   1.483 +    val mor_UNIV_thm =
   1.484 +      let
   1.485 +        fun mk_conjunct mapAsBs f s s' = HOLogic.mk_eq
   1.486 +            (HOLogic.mk_comp (Term.list_comb (mapAsBs, passive_ids @ fs), s),
   1.487 +            HOLogic.mk_comp (s', f));
   1.488 +        val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs;
   1.489 +        val rhs = Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct mapsAsBs fs ss s's);
   1.490 +      in
   1.491 +        Goal.prove_sorry lthy [] [] (fold_rev Logic.all (ss @ s's @ fs) (mk_Trueprop_eq (lhs, rhs)))
   1.492 +          (K (mk_mor_UNIV_tac morE_thms mor_def))
   1.493 +        |> Thm.close_derivation
   1.494 +      end;
   1.495 +
   1.496 +    val mor_str_thm =
   1.497 +      let
   1.498 +        val maps = map2 (fn Ds => fn bnf => Term.list_comb
   1.499 +          (mk_map_of_bnf Ds allAs (passiveAs @ FTsAs) bnf, passive_ids @ ss)) Dss bnfs;
   1.500 +      in
   1.501 +        Goal.prove_sorry lthy [] []
   1.502 +          (fold_rev Logic.all ss (HOLogic.mk_Trueprop
   1.503 +            (mk_mor active_UNIVs ss (map HOLogic.mk_UNIV FTsAs) maps ss)))
   1.504 +          (K (mk_mor_str_tac ks mor_UNIV_thm))
   1.505 +        |> Thm.close_derivation
   1.506 +      end;
   1.507 +
   1.508 +    val mor_sum_case_thm =
   1.509 +      let
   1.510 +        val maps = map3 (fn s => fn sum_s => fn mapx =>
   1.511 +          mk_sum_case (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ Inls), s), sum_s))
   1.512 +          s's sum_ss map_Inls;
   1.513 +      in
   1.514 +        Goal.prove_sorry lthy [] []
   1.515 +          (fold_rev Logic.all (s's @ sum_ss) (HOLogic.mk_Trueprop
   1.516 +            (mk_mor (map HOLogic.mk_UNIV activeBs) s's sum_UNIVs maps Inls)))
   1.517 +          (K (mk_mor_sum_case_tac ks mor_UNIV_thm))
   1.518 +        |> Thm.close_derivation
   1.519 +      end;
   1.520 +
   1.521 +    val timer = time (timer "Morphism definition & thms");
   1.522 +
   1.523 +    fun hset_rec_bind j = mk_internal_b (hset_recN ^ (if m = 1 then "" else string_of_int j));
   1.524 +    val hset_rec_name = Binding.name_of o hset_rec_bind;
   1.525 +    val hset_rec_def_bind = rpair [] o Thm.def_binding o hset_rec_bind;
   1.526 +
   1.527 +    fun hset_rec_spec j Zero hsetT hrec hrec' =
   1.528 +      let
   1.529 +        fun mk_Suc s setsAs z z' =
   1.530 +          let
   1.531 +            val (set, sets) = apfst (fn xs => nth xs (j - 1)) (chop m setsAs);
   1.532 +            fun mk_UN set k = mk_UNION (set $ (s $ z)) (mk_nthN n hrec k);
   1.533 +          in
   1.534 +            Term.absfree z'
   1.535 +              (mk_union (set $ (s $ z), Library.foldl1 mk_union (map2 mk_UN sets ks)))
   1.536 +          end;
   1.537 +
   1.538 +        val Suc = Term.absdummy HOLogic.natT (Term.absfree hrec'
   1.539 +          (HOLogic.mk_tuple (map4 mk_Suc ss setssAs zs zs')));
   1.540 +
   1.541 +        val lhs = Term.list_comb (Free (hset_rec_name j, hsetT), ss);
   1.542 +        val rhs = mk_nat_rec Zero Suc;
   1.543 +      in
   1.544 +        mk_Trueprop_eq (lhs, rhs)
   1.545 +      end;
   1.546 +
   1.547 +    val ((hset_rec_frees, (_, hset_rec_def_frees)), (lthy, lthy_old)) =
   1.548 +      lthy
   1.549 +      |> fold_map5 (fn j => fn Zero => fn hsetT => fn hrec => fn hrec' => Specification.definition
   1.550 +        (SOME (hset_rec_bind j, NONE, NoSyn),
   1.551 +          (hset_rec_def_bind j, hset_rec_spec j Zero hsetT hrec hrec')))
   1.552 +        ls Zeros hsetTs hrecs hrecs'
   1.553 +      |>> apsnd split_list o split_list
   1.554 +      ||> `Local_Theory.restore;
   1.555 +
   1.556 +    val phi = Proof_Context.export_morphism lthy_old lthy;
   1.557 +
   1.558 +    val hset_rec_defs = map (Morphism.thm phi) hset_rec_def_frees;
   1.559 +    val hset_recs = map (fst o Term.dest_Const o Morphism.term phi) hset_rec_frees;
   1.560 +
   1.561 +    fun mk_hset_rec ss nat i j T =
   1.562 +      let
   1.563 +        val args = ss @ [nat];
   1.564 +        val Ts = map fastype_of ss;
   1.565 +        val bTs = map domain_type Ts;
   1.566 +        val hrecT = HOLogic.mk_tupleT (map (fn U => U --> HOLogic.mk_setT T) bTs)
   1.567 +        val hset_recT = Library.foldr (op -->) (Ts, HOLogic.natT --> hrecT);
   1.568 +      in
   1.569 +        mk_nthN n (Term.list_comb (Const (nth hset_recs (j - 1), hset_recT), args)) i
   1.570 +      end;
   1.571 +
   1.572 +    val hset_rec_0ss = mk_rec_simps n @{thm nat_rec_0} hset_rec_defs;
   1.573 +    val hset_rec_Sucss = mk_rec_simps n @{thm nat_rec_Suc} hset_rec_defs;
   1.574 +    val hset_rec_0ss' = transpose hset_rec_0ss;
   1.575 +    val hset_rec_Sucss' = transpose hset_rec_Sucss;
   1.576 +
   1.577 +    fun hset_binds j = mk_internal_bs (hsetN ^ (if m = 1 then "" else string_of_int j))
   1.578 +    fun hset_bind i j = nth (hset_binds j) (i - 1);
   1.579 +    val hset_name = Binding.name_of oo hset_bind;
   1.580 +    val hset_def_bind = rpair [] o Thm.def_binding oo hset_bind;
   1.581 +
   1.582 +    fun hset_spec i j =
   1.583 +      let
   1.584 +        val U = nth activeAs (i - 1);
   1.585 +        val z = nth zs (i - 1);
   1.586 +        val T = nth passiveAs (j - 1);
   1.587 +        val setT = HOLogic.mk_setT T;
   1.588 +        val hsetT = Library.foldr (op -->) (sTs, U --> setT);
   1.589 +
   1.590 +        val lhs = Term.list_comb (Free (hset_name i j, hsetT), ss @ [z]);
   1.591 +        val rhs = mk_UNION (HOLogic.mk_UNIV HOLogic.natT)
   1.592 +          (Term.absfree nat' (mk_hset_rec ss nat i j T $ z));
   1.593 +      in
   1.594 +        mk_Trueprop_eq (lhs, rhs)
   1.595 +      end;
   1.596 +
   1.597 +    val ((hset_frees, (_, hset_def_frees)), (lthy, lthy_old)) =
   1.598 +      lthy
   1.599 +      |> fold_map (fn i => fold_map (fn j => Specification.definition
   1.600 +        (SOME (hset_bind i j, NONE, NoSyn), (hset_def_bind i j, hset_spec i j))) ls) ks
   1.601 +      |>> map (apsnd split_list o split_list)
   1.602 +      |>> apsnd split_list o split_list
   1.603 +      ||> `Local_Theory.restore;
   1.604 +
   1.605 +    val phi = Proof_Context.export_morphism lthy_old lthy;
   1.606 +
   1.607 +    val hset_defss = map (map (Morphism.thm phi)) hset_def_frees;
   1.608 +    val hset_defss' = transpose hset_defss;
   1.609 +    val hset_namess = map (map (fst o Term.dest_Const o Morphism.term phi)) hset_frees;
   1.610 +
   1.611 +    fun mk_hset ss i j T =
   1.612 +      let
   1.613 +        val Ts = map fastype_of ss;
   1.614 +        val bTs = map domain_type Ts;
   1.615 +        val hsetT = Library.foldr (op -->) (Ts, nth bTs (i - 1) --> HOLogic.mk_setT T);
   1.616 +      in
   1.617 +        Term.list_comb (Const (nth (nth hset_namess (i - 1)) (j - 1), hsetT), ss)
   1.618 +      end;
   1.619 +
   1.620 +    val hsetssAs = map (fn i => map2 (mk_hset ss i) ls passiveAs) ks;
   1.621 +
   1.622 +    val (set_incl_hset_thmss, set_hset_incl_hset_thmsss) =
   1.623 +      let
   1.624 +        fun mk_set_incl_hset s x set hset = fold_rev Logic.all (x :: ss)
   1.625 +          (HOLogic.mk_Trueprop (mk_leq (set $ (s $ x)) (hset $ x)));
   1.626 +
   1.627 +        fun mk_set_hset_incl_hset s x y set hset1 hset2 =
   1.628 +          fold_rev Logic.all (x :: y :: ss)
   1.629 +            (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x, set $ (s $ y))),
   1.630 +            HOLogic.mk_Trueprop (mk_leq (hset1 $ x) (hset2 $ y))));
   1.631 +
   1.632 +        val set_incl_hset_goalss =
   1.633 +          map4 (fn s => fn x => fn sets => fn hsets =>
   1.634 +            map2 (mk_set_incl_hset s x) (take m sets) hsets)
   1.635 +          ss zs setssAs hsetssAs;
   1.636 +
   1.637 +        (*xk : F(i)set(m+k) (si yi) ==> F(k)_hset(j) s1 ... sn xk <= F(i)_hset(j) s1 ... sn yi*)
   1.638 +        val set_hset_incl_hset_goalsss =
   1.639 +          map4 (fn si => fn yi => fn sets => fn hsetsi =>
   1.640 +            map3 (fn xk => fn set => fn hsetsk =>
   1.641 +              map2 (mk_set_hset_incl_hset si xk yi set) hsetsk hsetsi)
   1.642 +            zs_copy (drop m sets) hsetssAs)
   1.643 +          ss zs setssAs hsetssAs;
   1.644 +      in
   1.645 +        (map3 (fn goals => fn defs => fn rec_Sucs =>
   1.646 +          map3 (fn goal => fn def => fn rec_Suc =>
   1.647 +            Goal.prove_sorry lthy [] [] goal (K (mk_set_incl_hset_tac def rec_Suc))
   1.648 +            |> Thm.close_derivation)
   1.649 +          goals defs rec_Sucs)
   1.650 +        set_incl_hset_goalss hset_defss hset_rec_Sucss,
   1.651 +        map3 (fn goalss => fn defsi => fn rec_Sucs =>
   1.652 +          map3 (fn k => fn goals => fn defsk =>
   1.653 +            map4 (fn goal => fn defk => fn defi => fn rec_Suc =>
   1.654 +              Goal.prove_sorry lthy [] [] goal
   1.655 +                (K (mk_set_hset_incl_hset_tac n [defk, defi] rec_Suc k))
   1.656 +              |> Thm.close_derivation)
   1.657 +            goals defsk defsi rec_Sucs)
   1.658 +          ks goalss hset_defss)
   1.659 +        set_hset_incl_hset_goalsss hset_defss hset_rec_Sucss)
   1.660 +      end;
   1.661 +
   1.662 +    val set_incl_hset_thmss' = transpose set_incl_hset_thmss;
   1.663 +    val set_hset_incl_hset_thmsss' = transpose (map transpose set_hset_incl_hset_thmsss);
   1.664 +    val set_hset_thmss = map (map (fn thm => thm RS @{thm set_mp})) set_incl_hset_thmss;
   1.665 +    val set_hset_hset_thmsss = map (map (map (fn thm => thm RS @{thm set_mp})))
   1.666 +      set_hset_incl_hset_thmsss;
   1.667 +    val set_hset_thmss' = transpose set_hset_thmss;
   1.668 +    val set_hset_hset_thmsss' = transpose (map transpose set_hset_hset_thmsss);
   1.669 +
   1.670 +    val hset_minimal_thms =
   1.671 +      let
   1.672 +        fun mk_passive_prem set s x K =
   1.673 +          Logic.all x (HOLogic.mk_Trueprop (mk_leq (set $ (s $ x)) (K $ x)));
   1.674 +
   1.675 +        fun mk_active_prem s x1 K1 set x2 K2 =
   1.676 +          fold_rev Logic.all [x1, x2]
   1.677 +            (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x2, set $ (s $ x1))),
   1.678 +              HOLogic.mk_Trueprop (mk_leq (K2 $ x2) (K1 $ x1))));
   1.679 +
   1.680 +        val premss = map2 (fn j => fn Ks =>
   1.681 +          map4 mk_passive_prem (map (fn xs => nth xs (j - 1)) setssAs) ss zs Ks @
   1.682 +            flat (map4 (fn sets => fn s => fn x1 => fn K1 =>
   1.683 +              map3 (mk_active_prem s x1 K1) (drop m sets) zs_copy Ks) setssAs ss zs Ks))
   1.684 +          ls Kss;
   1.685 +
   1.686 +        val hset_rec_minimal_thms =
   1.687 +          let
   1.688 +            fun mk_conjunct j T i K x = mk_leq (mk_hset_rec ss nat i j T $ x) (K $ x);
   1.689 +            fun mk_concl j T Ks = list_all_free zs
   1.690 +              (Library.foldr1 HOLogic.mk_conj (map3 (mk_conjunct j T) ks Ks zs));
   1.691 +            val concls = map3 mk_concl ls passiveAs Kss;
   1.692 +
   1.693 +            val goals = map2 (fn prems => fn concl =>
   1.694 +              Logic.list_implies (prems, HOLogic.mk_Trueprop concl)) premss concls
   1.695 +
   1.696 +            val ctss =
   1.697 +              map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) concls;
   1.698 +          in
   1.699 +            map4 (fn goal => fn cts => fn hset_rec_0s => fn hset_rec_Sucs =>
   1.700 +              singleton (Proof_Context.export names_lthy lthy)
   1.701 +                (Goal.prove_sorry lthy [] [] goal
   1.702 +                  (mk_hset_rec_minimal_tac m cts hset_rec_0s hset_rec_Sucs))
   1.703 +              |> Thm.close_derivation)
   1.704 +            goals ctss hset_rec_0ss' hset_rec_Sucss'
   1.705 +          end;
   1.706 +
   1.707 +        fun mk_conjunct j T i K x = mk_leq (mk_hset ss i j T $ x) (K $ x);
   1.708 +        fun mk_concl j T Ks = Library.foldr1 HOLogic.mk_conj (map3 (mk_conjunct j T) ks Ks zs);
   1.709 +        val concls = map3 mk_concl ls passiveAs Kss;
   1.710 +
   1.711 +        val goals = map3 (fn Ks => fn prems => fn concl =>
   1.712 +          fold_rev Logic.all (Ks @ ss @ zs)
   1.713 +            (Logic.list_implies (prems, HOLogic.mk_Trueprop concl))) Kss premss concls;
   1.714 +      in
   1.715 +        map3 (fn goal => fn hset_defs => fn hset_rec_minimal =>
   1.716 +          Goal.prove_sorry lthy [] [] goal
   1.717 +            (mk_hset_minimal_tac n hset_defs hset_rec_minimal)
   1.718 +          |> Thm.close_derivation)
   1.719 +        goals hset_defss' hset_rec_minimal_thms
   1.720 +      end;
   1.721 +
   1.722 +    val timer = time (timer "Hereditary sets");
   1.723 +
   1.724 +    (* bisimulation *)
   1.725 +
   1.726 +    val bis_bind = mk_internal_b bisN;
   1.727 +    val bis_name = Binding.name_of bis_bind;
   1.728 +    val bis_def_bind = (Thm.def_binding bis_bind, []);
   1.729 +
   1.730 +    fun mk_bis_le_conjunct R B1 B2 = mk_leq R (mk_Times (B1, B2));
   1.731 +    val bis_le = Library.foldr1 HOLogic.mk_conj (map3 mk_bis_le_conjunct Rs Bs B's)
   1.732 +
   1.733 +    val bis_spec =
   1.734 +      let
   1.735 +        val bisT = Library.foldr (op -->) (ATs @ BTs @ sTs @ B'Ts @ s'Ts @ setRTs, HOLogic.boolT);
   1.736 +
   1.737 +        val fst_args = passive_ids @ fsts;
   1.738 +        val snd_args = passive_ids @ snds;
   1.739 +        fun mk_bis R s s' b1 b2 RF map1 map2 sets =
   1.740 +          list_all_free [b1, b2] (HOLogic.mk_imp
   1.741 +            (HOLogic.mk_mem (HOLogic.mk_prod (b1, b2), R),
   1.742 +            mk_Bex (mk_in (As @ Rs) sets (snd (dest_Free RF))) (Term.absfree (dest_Free RF)
   1.743 +              (HOLogic.mk_conj
   1.744 +                (HOLogic.mk_eq (Term.list_comb (map1, fst_args) $ RF, s $ b1),
   1.745 +                HOLogic.mk_eq (Term.list_comb (map2, snd_args) $ RF, s' $ b2))))));
   1.746 +
   1.747 +        val lhs = Term.list_comb (Free (bis_name, bisT), As @ Bs @ ss @ B's @ s's @ Rs);
   1.748 +        val rhs = HOLogic.mk_conj
   1.749 +          (bis_le, Library.foldr1 HOLogic.mk_conj
   1.750 +            (map9 mk_bis Rs ss s's zs z's RFs map_fsts map_snds bis_setss))
   1.751 +      in
   1.752 +        mk_Trueprop_eq (lhs, rhs)
   1.753 +      end;
   1.754 +
   1.755 +    val ((bis_free, (_, bis_def_free)), (lthy, lthy_old)) =
   1.756 +      lthy
   1.757 +      |> Specification.definition (SOME (bis_bind, NONE, NoSyn), (bis_def_bind, bis_spec))
   1.758 +      ||> `Local_Theory.restore;
   1.759 +
   1.760 +    val phi = Proof_Context.export_morphism lthy_old lthy;
   1.761 +    val bis = fst (Term.dest_Const (Morphism.term phi bis_free));
   1.762 +    val bis_def = Morphism.thm phi bis_def_free;
   1.763 +
   1.764 +    fun mk_bis As Bs1 ss1 Bs2 ss2 Rs =
   1.765 +      let
   1.766 +        val args = As @ Bs1 @ ss1 @ Bs2 @ ss2 @ Rs;
   1.767 +        val Ts = map fastype_of args;
   1.768 +        val bisT = Library.foldr (op -->) (Ts, HOLogic.boolT);
   1.769 +      in
   1.770 +        Term.list_comb (Const (bis, bisT), args)
   1.771 +      end;
   1.772 +
   1.773 +    val bis_cong_thm =
   1.774 +      let
   1.775 +        val prems = map HOLogic.mk_Trueprop
   1.776 +         (mk_bis As Bs ss B's s's Rs :: map2 (curry HOLogic.mk_eq) Rs_copy Rs)
   1.777 +        val concl = HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's Rs_copy);
   1.778 +      in
   1.779 +        Goal.prove_sorry lthy [] []
   1.780 +          (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs @ Rs_copy)
   1.781 +            (Logic.list_implies (prems, concl)))
   1.782 +          (K ((hyp_subst_tac lthy THEN' atac) 1))
   1.783 +        |> Thm.close_derivation
   1.784 +      end;
   1.785 +
   1.786 +    val bis_rel_thm =
   1.787 +      let
   1.788 +        fun mk_conjunct R s s' b1 b2 rel =
   1.789 +          list_all_free [b1, b2] (HOLogic.mk_imp
   1.790 +            (HOLogic.mk_mem (HOLogic.mk_prod (b1, b2), R),
   1.791 +            Term.list_comb (rel, map mk_in_rel (passive_Id_ons @ Rs)) $ (s $ b1) $ (s' $ b2)));
   1.792 +
   1.793 +        val rhs = HOLogic.mk_conj
   1.794 +          (bis_le, Library.foldr1 HOLogic.mk_conj
   1.795 +            (map6 mk_conjunct Rs ss s's zs z's relsAsBs))
   1.796 +      in
   1.797 +        Goal.prove_sorry lthy [] []
   1.798 +          (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
   1.799 +            (mk_Trueprop_eq (mk_bis As Bs ss B's s's Rs, rhs)))
   1.800 +          (K (mk_bis_rel_tac lthy m bis_def rel_OO_Grps map_comps map_cong0s set_mapss))
   1.801 +        |> Thm.close_derivation
   1.802 +      end;
   1.803 +
   1.804 +    val bis_converse_thm =
   1.805 +      Goal.prove_sorry lthy [] []
   1.806 +        (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
   1.807 +          (Logic.mk_implies
   1.808 +            (HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's Rs),
   1.809 +            HOLogic.mk_Trueprop (mk_bis As B's s's Bs ss (map mk_converse Rs)))))
   1.810 +        (K (mk_bis_converse_tac m bis_rel_thm rel_congs rel_converseps))
   1.811 +      |> Thm.close_derivation;
   1.812 +
   1.813 +    val bis_O_thm =
   1.814 +      let
   1.815 +        val prems =
   1.816 +          [HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's Rs),
   1.817 +           HOLogic.mk_Trueprop (mk_bis As B's s's B''s s''s R's)];
   1.818 +        val concl =
   1.819 +          HOLogic.mk_Trueprop (mk_bis As Bs ss B''s s''s (map2 (curry mk_rel_comp) Rs R's));
   1.820 +      in
   1.821 +        Goal.prove_sorry lthy [] []
   1.822 +          (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ B''s @ s''s @ Rs @ R's)
   1.823 +            (Logic.list_implies (prems, concl)))
   1.824 +          (K (mk_bis_O_tac lthy m bis_rel_thm rel_congs rel_OOs))
   1.825 +        |> Thm.close_derivation
   1.826 +      end;
   1.827 +
   1.828 +    val bis_Gr_thm =
   1.829 +      let
   1.830 +        val concl =
   1.831 +          HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's (map2 mk_Gr Bs fs));
   1.832 +      in
   1.833 +        Goal.prove_sorry lthy [] []
   1.834 +          (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ fs)
   1.835 +            (Logic.list_implies ([coalg_prem, mor_prem], concl)))
   1.836 +          (mk_bis_Gr_tac bis_rel_thm rel_Grps mor_image_thms morE_thms coalg_in_thms)
   1.837 +        |> Thm.close_derivation
   1.838 +      end;
   1.839 +
   1.840 +    val bis_image2_thm = bis_cong_thm OF
   1.841 +      ((bis_O_thm OF [bis_Gr_thm RS bis_converse_thm, bis_Gr_thm]) ::
   1.842 +      replicate n @{thm image2_Gr});
   1.843 +
   1.844 +    val bis_Id_on_thm = bis_cong_thm OF ((mor_id_thm RSN (2, bis_Gr_thm)) ::
   1.845 +      replicate n @{thm Id_on_Gr});
   1.846 +
   1.847 +    val bis_Union_thm =
   1.848 +      let
   1.849 +        val prem =
   1.850 +          HOLogic.mk_Trueprop (mk_Ball Idx
   1.851 +            (Term.absfree idx' (mk_bis As Bs ss B's s's (map (fn R => R $ idx) Ris))));
   1.852 +        val concl =
   1.853 +          HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's (map (mk_UNION Idx) Ris));
   1.854 +      in
   1.855 +        Goal.prove_sorry lthy [] []
   1.856 +          (fold_rev Logic.all (Idx :: As @ Bs @ ss @ B's @ s's @ Ris)
   1.857 +            (Logic.mk_implies (prem, concl)))
   1.858 +          (mk_bis_Union_tac bis_def in_mono'_thms)
   1.859 +        |> Thm.close_derivation
   1.860 +      end;
   1.861 +
   1.862 +    (* self-bisimulation *)
   1.863 +
   1.864 +    fun mk_sbis As Bs ss Rs = mk_bis As Bs ss Bs ss Rs;
   1.865 +
   1.866 +    val sbis_prem = HOLogic.mk_Trueprop (mk_sbis As Bs ss sRs);
   1.867 +
   1.868 +    (* largest self-bisimulation *)
   1.869 +
   1.870 +    val lsbis_binds = mk_internal_bs lsbisN;
   1.871 +    fun lsbis_bind i = nth lsbis_binds (i - 1);
   1.872 +    val lsbis_name = Binding.name_of o lsbis_bind;
   1.873 +    val lsbis_def_bind = rpair [] o Thm.def_binding o lsbis_bind;
   1.874 +
   1.875 +    val all_sbis = HOLogic.mk_Collect (fst Rtuple', snd Rtuple', list_exists_free sRs
   1.876 +      (HOLogic.mk_conj (HOLogic.mk_eq (Rtuple, HOLogic.mk_tuple sRs), mk_sbis As Bs ss sRs)));
   1.877 +
   1.878 +    fun lsbis_spec i RT =
   1.879 +      let
   1.880 +        fun mk_lsbisT RT =
   1.881 +          Library.foldr (op -->) (map fastype_of (As @ Bs @ ss), RT);
   1.882 +        val lhs = Term.list_comb (Free (lsbis_name i, mk_lsbisT RT), As @ Bs @ ss);
   1.883 +        val rhs = mk_UNION all_sbis (Term.absfree Rtuple' (mk_nthN n Rtuple i));
   1.884 +      in
   1.885 +        mk_Trueprop_eq (lhs, rhs)
   1.886 +      end;
   1.887 +
   1.888 +    val ((lsbis_frees, (_, lsbis_def_frees)), (lthy, lthy_old)) =
   1.889 +      lthy
   1.890 +      |> fold_map2 (fn i => fn RT => Specification.definition
   1.891 +        (SOME (lsbis_bind i, NONE, NoSyn), (lsbis_def_bind i, lsbis_spec i RT))) ks setsRTs
   1.892 +      |>> apsnd split_list o split_list
   1.893 +      ||> `Local_Theory.restore;
   1.894 +
   1.895 +    val phi = Proof_Context.export_morphism lthy_old lthy;
   1.896 +
   1.897 +    val lsbis_defs = map (Morphism.thm phi) lsbis_def_frees;
   1.898 +    val lsbiss = map (fst o Term.dest_Const o Morphism.term phi) lsbis_frees;
   1.899 +
   1.900 +    fun mk_lsbis As Bs ss i =
   1.901 +      let
   1.902 +        val args = As @ Bs @ ss;
   1.903 +        val Ts = map fastype_of args;
   1.904 +        val RT = mk_relT (`I (HOLogic.dest_setT (fastype_of (nth Bs (i - 1)))));
   1.905 +        val lsbisT = Library.foldr (op -->) (Ts, RT);
   1.906 +      in
   1.907 +        Term.list_comb (Const (nth lsbiss (i - 1), lsbisT), args)
   1.908 +      end;
   1.909 +
   1.910 +    val sbis_lsbis_thm =
   1.911 +      Goal.prove_sorry lthy [] []
   1.912 +        (fold_rev Logic.all (As @ Bs @ ss)
   1.913 +          (HOLogic.mk_Trueprop (mk_sbis As Bs ss (map (mk_lsbis As Bs ss) ks))))
   1.914 +        (K (mk_sbis_lsbis_tac lthy lsbis_defs bis_Union_thm bis_cong_thm))
   1.915 +      |> Thm.close_derivation;
   1.916 +
   1.917 +    val lsbis_incl_thms = map (fn i => sbis_lsbis_thm RS
   1.918 +      (bis_def RS iffD1 RS conjunct1 RS mk_conjunctN n i)) ks;
   1.919 +    val lsbisE_thms = map (fn i => (mk_specN 2 (sbis_lsbis_thm RS
   1.920 +      (bis_def RS iffD1 RS conjunct2 RS mk_conjunctN n i))) RS mp) ks;
   1.921 +
   1.922 +    val incl_lsbis_thms =
   1.923 +      let
   1.924 +        fun mk_concl i R = HOLogic.mk_Trueprop (mk_leq R (mk_lsbis As Bs ss i));
   1.925 +        val goals = map2 (fn i => fn R => fold_rev Logic.all (As @ Bs @ ss @ sRs)
   1.926 +          (Logic.mk_implies (sbis_prem, mk_concl i R))) ks sRs;
   1.927 +      in
   1.928 +        map3 (fn goal => fn i => fn def => Goal.prove_sorry lthy [] [] goal
   1.929 +          (K (mk_incl_lsbis_tac n i def)) |> Thm.close_derivation) goals ks lsbis_defs
   1.930 +      end;
   1.931 +
   1.932 +    val equiv_lsbis_thms =
   1.933 +      let
   1.934 +        fun mk_concl i B = HOLogic.mk_Trueprop (mk_equiv B (mk_lsbis As Bs ss i));
   1.935 +        val goals = map2 (fn i => fn B => fold_rev Logic.all (As @ Bs @ ss)
   1.936 +          (Logic.mk_implies (coalg_prem, mk_concl i B))) ks Bs;
   1.937 +      in
   1.938 +        map3 (fn goal => fn l_incl => fn incl_l =>
   1.939 +          Goal.prove_sorry lthy [] [] goal
   1.940 +            (K (mk_equiv_lsbis_tac sbis_lsbis_thm l_incl incl_l
   1.941 +              bis_Id_on_thm bis_converse_thm bis_O_thm))
   1.942 +          |> Thm.close_derivation)
   1.943 +        goals lsbis_incl_thms incl_lsbis_thms
   1.944 +      end;
   1.945 +
   1.946 +    val timer = time (timer "Bisimulations");
   1.947 +
   1.948 +    (* bounds *)
   1.949 +
   1.950 +    val (lthy, sbd, sbdT,
   1.951 +      sbd_card_order, sbd_Cinfinite, sbd_Card_order, set_sbdss) =
   1.952 +      if n = 1
   1.953 +      then (lthy, sum_bd, sum_bdT, bd_card_order, bd_Cinfinite, bd_Card_order, set_bdss)
   1.954 +      else
   1.955 +        let
   1.956 +          val sbdT_bind = mk_internal_b sum_bdTN;
   1.957 +
   1.958 +          val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) =
   1.959 +            typedef (sbdT_bind, dead_params, NoSyn)
   1.960 +              (HOLogic.mk_UNIV sum_bdT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
   1.961 +
   1.962 +          val sbdT = Type (sbdT_name, dead_params');
   1.963 +          val Abs_sbdT = Const (#Abs_name sbdT_glob_info, sum_bdT --> sbdT);
   1.964 +
   1.965 +          val sbd_bind = mk_internal_b sum_bdN;
   1.966 +          val sbd_name = Binding.name_of sbd_bind;
   1.967 +          val sbd_def_bind = (Thm.def_binding sbd_bind, []);
   1.968 +
   1.969 +          val sbd_spec = HOLogic.mk_Trueprop
   1.970 +            (HOLogic.mk_eq (Free (sbd_name, mk_relT (`I sbdT)), mk_dir_image sum_bd Abs_sbdT));
   1.971 +
   1.972 +          val ((sbd_free, (_, sbd_def_free)), (lthy, lthy_old)) =
   1.973 +            lthy
   1.974 +            |> Specification.definition (SOME (sbd_bind, NONE, NoSyn), (sbd_def_bind, sbd_spec))
   1.975 +            ||> `Local_Theory.restore;
   1.976 +
   1.977 +          val phi = Proof_Context.export_morphism lthy_old lthy;
   1.978 +
   1.979 +          val sbd_def = Morphism.thm phi sbd_def_free;
   1.980 +          val sbd = Const (fst (Term.dest_Const (Morphism.term phi sbd_free)), mk_relT (`I sbdT));
   1.981 +
   1.982 +          val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info);
   1.983 +          val Abs_sbdT_bij = mk_Abs_bij_thm lthy Abs_sbdT_inj (#Abs_cases sbdT_loc_info);
   1.984 +
   1.985 +          fun mk_sum_Cinfinite [thm] = thm
   1.986 +            | mk_sum_Cinfinite (thm :: thms) =
   1.987 +              @{thm Cinfinite_csum_strong} OF [thm, mk_sum_Cinfinite thms];
   1.988 +
   1.989 +          val sum_Cinfinite = mk_sum_Cinfinite bd_Cinfinites;
   1.990 +          val sum_Card_order = sum_Cinfinite RS conjunct2;
   1.991 +
   1.992 +          fun mk_sum_card_order [thm] = thm
   1.993 +            | mk_sum_card_order (thm :: thms) =
   1.994 +              @{thm card_order_csum} OF [thm, mk_sum_card_order thms];
   1.995 +
   1.996 +          val sum_card_order = mk_sum_card_order bd_card_orders;
   1.997 +
   1.998 +          val sbd_ordIso = fold_thms lthy [sbd_def]
   1.999 +            (@{thm dir_image} OF [Abs_sbdT_inj, sum_Card_order]);
  1.1000 +          val sbd_card_order =  fold_thms lthy [sbd_def]
  1.1001 +            (@{thm card_order_dir_image} OF [Abs_sbdT_bij, sum_card_order]);
  1.1002 +          val sbd_Cinfinite = @{thm Cinfinite_cong} OF [sbd_ordIso, sum_Cinfinite];
  1.1003 +          val sbd_Card_order = sbd_Cinfinite RS conjunct2;
  1.1004 +
  1.1005 +          fun mk_set_sbd i bd_Card_order bds =
  1.1006 +            map (fn thm => @{thm ordLeq_ordIso_trans} OF
  1.1007 +              [bd_Card_order RS mk_ordLeq_csum n i thm, sbd_ordIso]) bds;
  1.1008 +          val set_sbdss = map3 mk_set_sbd ks bd_Card_orders set_bdss;
  1.1009 +       in
  1.1010 +         (lthy, sbd, sbdT, sbd_card_order, sbd_Cinfinite, sbd_Card_order, set_sbdss)
  1.1011 +       end;
  1.1012 +
  1.1013 +    val sbdTs = replicate n sbdT;
  1.1014 +    val sum_sbd = Library.foldr1 (uncurry mk_csum) (replicate n sbd);
  1.1015 +    val sum_sbdT = mk_sumTN sbdTs;
  1.1016 +    val sum_sbd_listT = HOLogic.listT sum_sbdT;
  1.1017 +    val sum_sbd_list_setT = HOLogic.mk_setT sum_sbd_listT;
  1.1018 +    val bdTs = passiveAs @ replicate n sbdT;
  1.1019 +    val to_sbd_maps = map4 mk_map_of_bnf Dss Ass (replicate n bdTs) bnfs;
  1.1020 +    val bdFTs = mk_FTs bdTs;
  1.1021 +    val sbdFT = mk_sumTN bdFTs;
  1.1022 +    val treeT = HOLogic.mk_prodT (sum_sbd_list_setT, sum_sbd_listT --> sbdFT);
  1.1023 +    val treeQT = HOLogic.mk_setT treeT;
  1.1024 +    val treeTs = passiveAs @ replicate n treeT;
  1.1025 +    val treeQTs = passiveAs @ replicate n treeQT;
  1.1026 +    val treeFTs = mk_FTs treeTs;
  1.1027 +    val tree_maps = map4 mk_map_of_bnf Dss (replicate n bdTs) (replicate n treeTs) bnfs;
  1.1028 +    val final_maps = map4 mk_map_of_bnf Dss (replicate n treeTs) (replicate n treeQTs) bnfs;
  1.1029 +    val isNode_setss = mk_setss (passiveAs @ replicate n sbdT);
  1.1030 +
  1.1031 +    val root = HOLogic.mk_set sum_sbd_listT [HOLogic.mk_list sum_sbdT []];
  1.1032 +    val Zero = HOLogic.mk_tuple (map (fn U => absdummy U root) activeAs);
  1.1033 +    val Lev_recT = fastype_of Zero;
  1.1034 +    val LevT = Library.foldr (op -->) (sTs, HOLogic.natT --> Lev_recT);
  1.1035 +
  1.1036 +    val Nil = HOLogic.mk_tuple (map3 (fn i => fn z => fn z'=>
  1.1037 +      Term.absfree z' (mk_InN activeAs z i)) ks zs zs');
  1.1038 +    val rv_recT = fastype_of Nil;
  1.1039 +    val rvT = Library.foldr (op -->) (sTs, sum_sbd_listT --> rv_recT);
  1.1040 +
  1.1041 +    val (((((((((((sumx, sumx'), (kks, kks')), (kl, kl')), (kl_copy, kl'_copy)), (Kl, Kl')),
  1.1042 +      (lab, lab')), (Kl_lab, Kl_lab')), xs), (Lev_rec, Lev_rec')), (rv_rec, rv_rec')),
  1.1043 +      names_lthy) = names_lthy
  1.1044 +      |> yield_singleton (apfst (op ~~) oo mk_Frees' "sumx") sum_sbdT
  1.1045 +      ||>> mk_Frees' "k" sbdTs
  1.1046 +      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "kl") sum_sbd_listT
  1.1047 +      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "kl") sum_sbd_listT
  1.1048 +      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "Kl") sum_sbd_list_setT
  1.1049 +      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "lab") (sum_sbd_listT --> sbdFT)
  1.1050 +      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "Kl_lab") treeT
  1.1051 +      ||>> mk_Frees "x" bdFTs
  1.1052 +      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "rec") Lev_recT
  1.1053 +      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "rec") rv_recT;
  1.1054 +
  1.1055 +    val (k, k') = (hd kks, hd kks')
  1.1056 +
  1.1057 +    val timer = time (timer "Bounds");
  1.1058 +
  1.1059 +    (* tree coalgebra *)
  1.1060 +
  1.1061 +    val isNode_binds = mk_internal_bs isNodeN;
  1.1062 +    fun isNode_bind i = nth isNode_binds (i - 1);
  1.1063 +    val isNode_name = Binding.name_of o isNode_bind;
  1.1064 +    val isNode_def_bind = rpair [] o Thm.def_binding o isNode_bind;
  1.1065 +
  1.1066 +    val isNodeT =
  1.1067 +      Library.foldr (op -->) (map fastype_of (As @ [Kl, lab, kl]), HOLogic.boolT);
  1.1068 +
  1.1069 +    val Succs = map3 (fn i => fn k => fn k' =>
  1.1070 +      HOLogic.mk_Collect (fst k', snd k', HOLogic.mk_mem (mk_InN sbdTs k i, mk_Succ Kl kl)))
  1.1071 +      ks kks kks';
  1.1072 +
  1.1073 +    fun isNode_spec sets x i =
  1.1074 +      let
  1.1075 +        val (passive_sets, active_sets) = chop m (map (fn set => set $ x) sets);
  1.1076 +        val lhs = Term.list_comb (Free (isNode_name i, isNodeT), As @ [Kl, lab, kl]);
  1.1077 +        val rhs = list_exists_free [x]
  1.1078 +          (Library.foldr1 HOLogic.mk_conj (HOLogic.mk_eq (lab $ kl, mk_InN bdFTs x i) ::
  1.1079 +          map2 mk_leq passive_sets As @ map2 (curry HOLogic.mk_eq) active_sets Succs));
  1.1080 +      in
  1.1081 +        mk_Trueprop_eq (lhs, rhs)
  1.1082 +      end;
  1.1083 +
  1.1084 +    val ((isNode_frees, (_, isNode_def_frees)), (lthy, lthy_old)) =
  1.1085 +      lthy
  1.1086 +      |> fold_map3 (fn i => fn x => fn sets => Specification.definition
  1.1087 +        (SOME (isNode_bind i, NONE, NoSyn), (isNode_def_bind i, isNode_spec sets x i)))
  1.1088 +        ks xs isNode_setss
  1.1089 +      |>> apsnd split_list o split_list
  1.1090 +      ||> `Local_Theory.restore;
  1.1091 +
  1.1092 +    val phi = Proof_Context.export_morphism lthy_old lthy;
  1.1093 +
  1.1094 +    val isNode_defs = map (Morphism.thm phi) isNode_def_frees;
  1.1095 +    val isNodes = map (fst o Term.dest_Const o Morphism.term phi) isNode_frees;
  1.1096 +
  1.1097 +    fun mk_isNode As kl i =
  1.1098 +      Term.list_comb (Const (nth isNodes (i - 1), isNodeT), As @ [Kl, lab, kl]);
  1.1099 +
  1.1100 +    val isTree =
  1.1101 +      let
  1.1102 +        val empty = HOLogic.mk_mem (HOLogic.mk_list sum_sbdT [], Kl);
  1.1103 +        val Field = mk_leq Kl (mk_Field (mk_clists sum_sbd));
  1.1104 +        val prefCl = mk_prefCl Kl;
  1.1105 +
  1.1106 +        val tree = mk_Ball Kl (Term.absfree kl'
  1.1107 +          (HOLogic.mk_conj
  1.1108 +            (Library.foldr1 HOLogic.mk_disj (map (mk_isNode As kl) ks),
  1.1109 +            Library.foldr1 HOLogic.mk_conj (map4 (fn Succ => fn i => fn k => fn k' =>
  1.1110 +              mk_Ball Succ (Term.absfree k' (mk_isNode As
  1.1111 +                (mk_append (kl, HOLogic.mk_list sum_sbdT [mk_InN sbdTs k i])) i)))
  1.1112 +            Succs ks kks kks'))));
  1.1113 +
  1.1114 +        val undef = list_all_free [kl] (HOLogic.mk_imp
  1.1115 +          (HOLogic.mk_not (HOLogic.mk_mem (kl, Kl)),
  1.1116 +          HOLogic.mk_eq (lab $ kl, mk_undefined sbdFT)));
  1.1117 +      in
  1.1118 +        Library.foldr1 HOLogic.mk_conj [empty, Field, prefCl, tree, undef]
  1.1119 +      end;
  1.1120 +
  1.1121 +    val carT_binds = mk_internal_bs carTN;
  1.1122 +    fun carT_bind i = nth carT_binds (i - 1);
  1.1123 +    val carT_name = Binding.name_of o carT_bind;
  1.1124 +    val carT_def_bind = rpair [] o Thm.def_binding o carT_bind;
  1.1125 +
  1.1126 +    fun carT_spec i =
  1.1127 +      let
  1.1128 +        val carTT = Library.foldr (op -->) (ATs, HOLogic.mk_setT treeT);
  1.1129 +
  1.1130 +        val lhs = Term.list_comb (Free (carT_name i, carTT), As);
  1.1131 +        val rhs = HOLogic.mk_Collect (fst Kl_lab', snd Kl_lab', list_exists_free [Kl, lab]
  1.1132 +          (HOLogic.mk_conj (HOLogic.mk_eq (Kl_lab, HOLogic.mk_prod (Kl, lab)),
  1.1133 +            HOLogic.mk_conj (isTree, mk_isNode As (HOLogic.mk_list sum_sbdT []) i))));
  1.1134 +      in
  1.1135 +        mk_Trueprop_eq (lhs, rhs)
  1.1136 +      end;
  1.1137 +
  1.1138 +    val ((carT_frees, (_, carT_def_frees)), (lthy, lthy_old)) =
  1.1139 +      lthy
  1.1140 +      |> fold_map (fn i => Specification.definition
  1.1141 +        (SOME (carT_bind i, NONE, NoSyn), (carT_def_bind i, carT_spec i))) ks
  1.1142 +      |>> apsnd split_list o split_list
  1.1143 +      ||> `Local_Theory.restore;
  1.1144 +
  1.1145 +    val phi = Proof_Context.export_morphism lthy_old lthy;
  1.1146 +
  1.1147 +    val carT_defs = map (Morphism.thm phi) carT_def_frees;
  1.1148 +    val carTs = map (fst o Term.dest_Const o Morphism.term phi) carT_frees;
  1.1149 +
  1.1150 +    fun mk_carT As i = Term.list_comb
  1.1151 +      (Const (nth carTs (i - 1),
  1.1152 +         Library.foldr (op -->) (map fastype_of As, HOLogic.mk_setT treeT)), As);
  1.1153 +
  1.1154 +    val strT_binds = mk_internal_bs strTN;
  1.1155 +    fun strT_bind i = nth strT_binds (i - 1);
  1.1156 +    val strT_name = Binding.name_of o strT_bind;
  1.1157 +    val strT_def_bind = rpair [] o Thm.def_binding o strT_bind;
  1.1158 +
  1.1159 +    fun strT_spec mapFT FT i =
  1.1160 +      let
  1.1161 +        val strTT = treeT --> FT;
  1.1162 +
  1.1163 +        fun mk_f i k k' =
  1.1164 +          let val in_k = mk_InN sbdTs k i;
  1.1165 +          in Term.absfree k' (HOLogic.mk_prod (mk_Shift Kl in_k, mk_shift lab in_k)) end;
  1.1166 +
  1.1167 +        val f = Term.list_comb (mapFT, passive_ids @ map3 mk_f ks kks kks');
  1.1168 +        val (fTs1, fTs2) = apsnd tl (chop (i - 1) (map (fn T => T --> FT) bdFTs));
  1.1169 +        val fs = map mk_undefined fTs1 @ (f :: map mk_undefined fTs2);
  1.1170 +        val lhs = Free (strT_name i, strTT);
  1.1171 +        val rhs = HOLogic.mk_split (Term.absfree Kl' (Term.absfree lab'
  1.1172 +          (mk_sum_caseN fs $ (lab $ HOLogic.mk_list sum_sbdT []))));
  1.1173 +      in
  1.1174 +        mk_Trueprop_eq (lhs, rhs)
  1.1175 +      end;
  1.1176 +
  1.1177 +    val ((strT_frees, (_, strT_def_frees)), (lthy, lthy_old)) =
  1.1178 +      lthy
  1.1179 +      |> fold_map3 (fn i => fn mapFT => fn FT => Specification.definition
  1.1180 +        (SOME (strT_bind i, NONE, NoSyn), (strT_def_bind i, strT_spec mapFT FT i)))
  1.1181 +        ks tree_maps treeFTs
  1.1182 +      |>> apsnd split_list o split_list
  1.1183 +      ||> `Local_Theory.restore;
  1.1184 +
  1.1185 +    val phi = Proof_Context.export_morphism lthy_old lthy;
  1.1186 +
  1.1187 +    val strT_defs = map ((fn def => trans OF [def RS fun_cong, @{thm prod.cases}]) o
  1.1188 +      Morphism.thm phi) strT_def_frees;
  1.1189 +    val strTs = map (fst o Term.dest_Const o Morphism.term phi) strT_frees;
  1.1190 +
  1.1191 +    fun mk_strT FT i = Const (nth strTs (i - 1), treeT --> FT);
  1.1192 +
  1.1193 +    val carTAs = map (mk_carT As) ks;
  1.1194 +    val strTAs = map2 mk_strT treeFTs ks;
  1.1195 +
  1.1196 +    val coalgT_thm =
  1.1197 +      Goal.prove_sorry lthy [] []
  1.1198 +        (fold_rev Logic.all As (HOLogic.mk_Trueprop (mk_coalg As carTAs strTAs)))
  1.1199 +        (mk_coalgT_tac m (coalg_def :: isNode_defs @ carT_defs) strT_defs set_mapss)
  1.1200 +      |> Thm.close_derivation;
  1.1201 +
  1.1202 +    val timer = time (timer "Tree coalgebra");
  1.1203 +
  1.1204 +    fun mk_to_sbd s x i i' =
  1.1205 +      mk_toCard (nth (nth setssAs (i - 1)) (m + i' - 1) $ (s $ x)) sbd;
  1.1206 +    fun mk_from_sbd s x i i' =
  1.1207 +      mk_fromCard (nth (nth setssAs (i - 1)) (m + i' - 1) $ (s $ x)) sbd;
  1.1208 +
  1.1209 +    fun mk_to_sbd_thmss thm = map (map (fn set_sbd =>
  1.1210 +      thm OF [set_sbd, sbd_Card_order]) o drop m) set_sbdss;
  1.1211 +
  1.1212 +    val to_sbd_inj_thmss = mk_to_sbd_thmss @{thm toCard_inj};
  1.1213 +    val to_sbd_thmss = mk_to_sbd_thmss @{thm toCard};
  1.1214 +    val from_to_sbd_thmss = mk_to_sbd_thmss @{thm fromCard_toCard};
  1.1215 +
  1.1216 +    val Lev_bind = mk_internal_b LevN;
  1.1217 +    val Lev_name = Binding.name_of Lev_bind;
  1.1218 +    val Lev_def_bind = rpair [] (Thm.def_binding Lev_bind);
  1.1219 +
  1.1220 +    val Lev_spec =
  1.1221 +      let
  1.1222 +        fun mk_Suc i s setsAs a a' =
  1.1223 +          let
  1.1224 +            val sets = drop m setsAs;
  1.1225 +            fun mk_set i' set b =
  1.1226 +              let
  1.1227 +                val Cons = HOLogic.mk_eq (kl_copy,
  1.1228 +                  mk_Cons (mk_InN sbdTs (mk_to_sbd s a i i' $ b) i') kl)
  1.1229 +                val b_set = HOLogic.mk_mem (b, set $ (s $ a));
  1.1230 +                val kl_rec = HOLogic.mk_mem (kl, mk_nthN n Lev_rec i' $ b);
  1.1231 +              in
  1.1232 +                HOLogic.mk_Collect (fst kl'_copy, snd kl'_copy, list_exists_free [b, kl]
  1.1233 +                  (HOLogic.mk_conj (Cons, HOLogic.mk_conj (b_set, kl_rec))))
  1.1234 +              end;
  1.1235 +          in
  1.1236 +            Term.absfree a' (Library.foldl1 mk_union (map3 mk_set ks sets zs_copy))
  1.1237 +          end;
  1.1238 +
  1.1239 +        val Suc = Term.absdummy HOLogic.natT (Term.absfree Lev_rec'
  1.1240 +          (HOLogic.mk_tuple (map5 mk_Suc ks ss setssAs zs zs')));
  1.1241 +
  1.1242 +        val lhs = Term.list_comb (Free (Lev_name, LevT), ss);
  1.1243 +        val rhs = mk_nat_rec Zero Suc;
  1.1244 +      in
  1.1245 +        mk_Trueprop_eq (lhs, rhs)
  1.1246 +      end;
  1.1247 +
  1.1248 +    val ((Lev_free, (_, Lev_def_free)), (lthy, lthy_old)) =
  1.1249 +      lthy
  1.1250 +      |> Specification.definition (SOME (Lev_bind, NONE, NoSyn), (Lev_def_bind, Lev_spec))
  1.1251 +      ||> `Local_Theory.restore;
  1.1252 +
  1.1253 +    val phi = Proof_Context.export_morphism lthy_old lthy;
  1.1254 +
  1.1255 +    val Lev_def = Morphism.thm phi Lev_def_free;
  1.1256 +    val Lev = fst (Term.dest_Const (Morphism.term phi Lev_free));
  1.1257 +
  1.1258 +    fun mk_Lev ss nat i =
  1.1259 +      let
  1.1260 +        val Ts = map fastype_of ss;
  1.1261 +        val LevT = Library.foldr (op -->) (Ts, HOLogic.natT -->
  1.1262 +          HOLogic.mk_tupleT (map (fn U => domain_type U --> sum_sbd_list_setT) Ts));
  1.1263 +      in
  1.1264 +        mk_nthN n (Term.list_comb (Const (Lev, LevT), ss) $ nat) i
  1.1265 +      end;
  1.1266 +
  1.1267 +    val Lev_0s = flat (mk_rec_simps n @{thm nat_rec_0} [Lev_def]);
  1.1268 +    val Lev_Sucs = flat (mk_rec_simps n @{thm nat_rec_Suc} [Lev_def]);
  1.1269 +
  1.1270 +    val rv_bind = mk_internal_b rvN;
  1.1271 +    val rv_name = Binding.name_of rv_bind;
  1.1272 +    val rv_def_bind = rpair [] (Thm.def_binding rv_bind);
  1.1273 +
  1.1274 +    val rv_spec =
  1.1275 +      let
  1.1276 +        fun mk_Cons i s b b' =
  1.1277 +          let
  1.1278 +            fun mk_case i' =
  1.1279 +              Term.absfree k' (mk_nthN n rv_rec i' $ (mk_from_sbd s b i i' $ k));
  1.1280 +          in
  1.1281 +            Term.absfree b' (mk_sum_caseN (map mk_case ks) $ sumx)
  1.1282 +          end;
  1.1283 +
  1.1284 +        val Cons = Term.absfree sumx' (Term.absdummy sum_sbd_listT (Term.absfree rv_rec'
  1.1285 +          (HOLogic.mk_tuple (map4 mk_Cons ks ss zs zs'))));
  1.1286 +
  1.1287 +        val lhs = Term.list_comb (Free (rv_name, rvT), ss);
  1.1288 +        val rhs = mk_list_rec Nil Cons;
  1.1289 +      in
  1.1290 +        mk_Trueprop_eq (lhs, rhs)
  1.1291 +      end;
  1.1292 +
  1.1293 +    val ((rv_free, (_, rv_def_free)), (lthy, lthy_old)) =
  1.1294 +      lthy
  1.1295 +      |> Specification.definition (SOME (rv_bind, NONE, NoSyn), (rv_def_bind, rv_spec))
  1.1296 +      ||> `Local_Theory.restore;
  1.1297 +
  1.1298 +    val phi = Proof_Context.export_morphism lthy_old lthy;
  1.1299 +
  1.1300 +    val rv_def = Morphism.thm phi rv_def_free;
  1.1301 +    val rv = fst (Term.dest_Const (Morphism.term phi rv_free));
  1.1302 +
  1.1303 +    fun mk_rv ss kl i =
  1.1304 +      let
  1.1305 +        val Ts = map fastype_of ss;
  1.1306 +        val As = map domain_type Ts;
  1.1307 +        val rvT = Library.foldr (op -->) (Ts, fastype_of kl -->
  1.1308 +          HOLogic.mk_tupleT (map (fn U => U --> mk_sumTN As) As));
  1.1309 +      in
  1.1310 +        mk_nthN n (Term.list_comb (Const (rv, rvT), ss) $ kl) i
  1.1311 +      end;
  1.1312 +
  1.1313 +    val rv_Nils = flat (mk_rec_simps n @{thm list_rec_Nil} [rv_def]);
  1.1314 +    val rv_Conss = flat (mk_rec_simps n @{thm list_rec_Cons} [rv_def]);
  1.1315 +
  1.1316 +    val beh_binds = mk_internal_bs behN;
  1.1317 +    fun beh_bind i = nth beh_binds (i - 1);
  1.1318 +    val beh_name = Binding.name_of o beh_bind;
  1.1319 +    val beh_def_bind = rpair [] o Thm.def_binding o beh_bind;
  1.1320 +
  1.1321 +    fun beh_spec i z =
  1.1322 +      let
  1.1323 +        val mk_behT = Library.foldr (op -->) (map fastype_of (ss @ [z]), treeT);
  1.1324 +
  1.1325 +        fun mk_case i to_sbd_map s k k' =
  1.1326 +          Term.absfree k' (mk_InN bdFTs
  1.1327 +            (Term.list_comb (to_sbd_map, passive_ids @ map (mk_to_sbd s k i) ks) $ (s $ k)) i);
  1.1328 +
  1.1329 +        val Lab = Term.absfree kl' (mk_If
  1.1330 +          (HOLogic.mk_mem (kl, mk_Lev ss (mk_size kl) i $ z))
  1.1331 +          (mk_sum_caseN (map5 mk_case ks to_sbd_maps ss zs zs') $ (mk_rv ss kl i $ z))
  1.1332 +          (mk_undefined sbdFT));
  1.1333 +
  1.1334 +        val lhs = Term.list_comb (Free (beh_name i, mk_behT), ss) $ z;
  1.1335 +        val rhs = HOLogic.mk_prod (mk_UNION (HOLogic.mk_UNIV HOLogic.natT)
  1.1336 +          (Term.absfree nat' (mk_Lev ss nat i $ z)), Lab);
  1.1337 +      in
  1.1338 +        mk_Trueprop_eq (lhs, rhs)
  1.1339 +      end;
  1.1340 +
  1.1341 +    val ((beh_frees, (_, beh_def_frees)), (lthy, lthy_old)) =
  1.1342 +      lthy
  1.1343 +      |> fold_map2 (fn i => fn z => Specification.definition
  1.1344 +        (SOME (beh_bind i, NONE, NoSyn), (beh_def_bind i, beh_spec i z))) ks zs
  1.1345 +      |>> apsnd split_list o split_list
  1.1346 +      ||> `Local_Theory.restore;
  1.1347 +
  1.1348 +    val phi = Proof_Context.export_morphism lthy_old lthy;
  1.1349 +
  1.1350 +    val beh_defs = map (Morphism.thm phi) beh_def_frees;
  1.1351 +    val behs = map (fst o Term.dest_Const o Morphism.term phi) beh_frees;
  1.1352 +
  1.1353 +    fun mk_beh ss i =
  1.1354 +      let
  1.1355 +        val Ts = map fastype_of ss;
  1.1356 +        val behT = Library.foldr (op -->) (Ts, nth activeAs (i - 1) --> treeT);
  1.1357 +      in
  1.1358 +        Term.list_comb (Const (nth behs (i - 1), behT), ss)
  1.1359 +      end;
  1.1360 +
  1.1361 +    val Lev_sbd_thms =
  1.1362 +      let
  1.1363 +        fun mk_conjunct i z = mk_leq (mk_Lev ss nat i $ z) (mk_Field (mk_clists sum_sbd));
  1.1364 +        val goal = list_all_free zs
  1.1365 +          (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs));
  1.1366 +
  1.1367 +        val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
  1.1368 +
  1.1369 +        val Lev_sbd = singleton (Proof_Context.export names_lthy lthy)
  1.1370 +          (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
  1.1371 +            (K (mk_Lev_sbd_tac lthy cts Lev_0s Lev_Sucs to_sbd_thmss))
  1.1372 +          |> Thm.close_derivation);
  1.1373 +
  1.1374 +        val Lev_sbd' = mk_specN n Lev_sbd;
  1.1375 +      in
  1.1376 +        map (fn i => Lev_sbd' RS mk_conjunctN n i) ks
  1.1377 +      end;
  1.1378 +
  1.1379 +    val (length_Lev_thms, length_Lev'_thms) =
  1.1380 +      let
  1.1381 +        fun mk_conjunct i z = HOLogic.mk_imp (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z),
  1.1382 +          HOLogic.mk_eq (mk_size kl, nat));
  1.1383 +        val goal = list_all_free (kl :: zs)
  1.1384 +          (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs));
  1.1385 +
  1.1386 +        val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
  1.1387 +
  1.1388 +        val length_Lev = singleton (Proof_Context.export names_lthy lthy)
  1.1389 +          (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
  1.1390 +            (K (mk_length_Lev_tac lthy cts Lev_0s Lev_Sucs))
  1.1391 +          |> Thm.close_derivation);
  1.1392 +
  1.1393 +        val length_Lev' = mk_specN (n + 1) length_Lev;
  1.1394 +        val length_Levs = map (fn i => length_Lev' RS mk_conjunctN n i RS mp) ks;
  1.1395 +
  1.1396 +        fun mk_goal i z = fold_rev Logic.all (z :: kl :: nat :: ss) (Logic.mk_implies
  1.1397 +            (HOLogic.mk_Trueprop (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z)),
  1.1398 +            HOLogic.mk_Trueprop (HOLogic.mk_mem (kl, mk_Lev ss (mk_size kl) i $ z))));
  1.1399 +        val goals = map2 mk_goal ks zs;
  1.1400 +
  1.1401 +        val length_Levs' = map2 (fn goal => fn length_Lev =>
  1.1402 +          Goal.prove_sorry lthy [] [] goal (K (mk_length_Lev'_tac length_Lev))
  1.1403 +          |> Thm.close_derivation) goals length_Levs;
  1.1404 +      in
  1.1405 +        (length_Levs, length_Levs')
  1.1406 +      end;
  1.1407 +
  1.1408 +    val prefCl_Lev_thms =
  1.1409 +      let
  1.1410 +        fun mk_conjunct i z = HOLogic.mk_imp
  1.1411 +          (HOLogic.mk_conj (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z), mk_prefixeq kl_copy kl),
  1.1412 +          HOLogic.mk_mem (kl_copy, mk_Lev ss (mk_size kl_copy) i $ z));
  1.1413 +        val goal = list_all_free (kl :: kl_copy :: zs)
  1.1414 +          (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs));
  1.1415 +
  1.1416 +        val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
  1.1417 +
  1.1418 +        val prefCl_Lev = singleton (Proof_Context.export names_lthy lthy)
  1.1419 +          (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
  1.1420 +            (K (mk_prefCl_Lev_tac lthy cts Lev_0s Lev_Sucs)))
  1.1421 +          |> Thm.close_derivation;
  1.1422 +
  1.1423 +        val prefCl_Lev' = mk_specN (n + 2) prefCl_Lev;
  1.1424 +      in
  1.1425 +        map (fn i => prefCl_Lev' RS mk_conjunctN n i RS mp) ks
  1.1426 +      end;
  1.1427 +
  1.1428 +    val rv_last_thmss =
  1.1429 +      let
  1.1430 +        fun mk_conjunct i z i' z_copy = list_exists_free [z_copy]
  1.1431 +          (HOLogic.mk_eq
  1.1432 +            (mk_rv ss (mk_append (kl, HOLogic.mk_list sum_sbdT [mk_InN sbdTs k i'])) i $ z,
  1.1433 +            mk_InN activeAs z_copy i'));
  1.1434 +        val goal = list_all_free (k :: zs)
  1.1435 +          (Library.foldr1 HOLogic.mk_conj (map2 (fn i => fn z =>
  1.1436 +            Library.foldr1 HOLogic.mk_conj
  1.1437 +              (map2 (mk_conjunct i z) ks zs_copy)) ks zs));
  1.1438 +
  1.1439 +        val cTs = [SOME (certifyT lthy sum_sbdT)];
  1.1440 +        val cts = map (SOME o certify lthy) [Term.absfree kl' goal, kl];
  1.1441 +
  1.1442 +        val rv_last = singleton (Proof_Context.export names_lthy lthy)
  1.1443 +          (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
  1.1444 +            (K (mk_rv_last_tac cTs cts rv_Nils rv_Conss)))
  1.1445 +          |> Thm.close_derivation;
  1.1446 +
  1.1447 +        val rv_last' = mk_specN (n + 1) rv_last;
  1.1448 +      in
  1.1449 +        map (fn i => map (fn i' => rv_last' RS mk_conjunctN n i RS mk_conjunctN n i') ks) ks
  1.1450 +      end;
  1.1451 +
  1.1452 +    val set_rv_Lev_thmsss = if m = 0 then replicate n (replicate n []) else
  1.1453 +      let
  1.1454 +        fun mk_case s sets z z_free = Term.absfree z_free (Library.foldr1 HOLogic.mk_conj
  1.1455 +          (map2 (fn set => fn A => mk_leq (set $ (s $ z)) A) (take m sets) As));
  1.1456 +
  1.1457 +        fun mk_conjunct i z B = HOLogic.mk_imp
  1.1458 +          (HOLogic.mk_conj (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z), HOLogic.mk_mem (z, B)),
  1.1459 +          mk_sum_caseN (map4 mk_case ss setssAs zs zs') $ (mk_rv ss kl i $ z));
  1.1460 +
  1.1461 +        val goal = list_all_free (kl :: zs)
  1.1462 +          (Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct ks zs Bs));
  1.1463 +
  1.1464 +        val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
  1.1465 +
  1.1466 +        val set_rv_Lev = singleton (Proof_Context.export names_lthy lthy)
  1.1467 +          (Goal.prove_sorry lthy [] []
  1.1468 +            (Logic.mk_implies (coalg_prem, HOLogic.mk_Trueprop goal))
  1.1469 +            (K (mk_set_rv_Lev_tac lthy m cts Lev_0s Lev_Sucs rv_Nils rv_Conss
  1.1470 +              coalg_set_thmss from_to_sbd_thmss)))
  1.1471 +          |> Thm.close_derivation;
  1.1472 +
  1.1473 +        val set_rv_Lev' = mk_specN (n + 1) set_rv_Lev;
  1.1474 +      in
  1.1475 +        map (fn i => map (fn i' =>
  1.1476 +          split_conj_thm (if n = 1 then set_rv_Lev' RS mk_conjunctN n i RS mp
  1.1477 +            else set_rv_Lev' RS mk_conjunctN n i RS mp RSN
  1.1478 +              (2, @{thm sum_case_weak_cong} RS iffD1) RS
  1.1479 +              (mk_sum_casesN n i' RS iffD1))) ks) ks
  1.1480 +      end;
  1.1481 +
  1.1482 +    val set_Lev_thmsss =
  1.1483 +      let
  1.1484 +        fun mk_conjunct i z =
  1.1485 +          let
  1.1486 +            fun mk_conjunct' i' sets s z' =
  1.1487 +              let
  1.1488 +                fun mk_conjunct'' i'' set z'' = HOLogic.mk_imp
  1.1489 +                  (HOLogic.mk_mem (z'', set $ (s $ z')),
  1.1490 +                    HOLogic.mk_mem (mk_append (kl,
  1.1491 +                      HOLogic.mk_list sum_sbdT [mk_InN sbdTs (mk_to_sbd s z' i' i'' $ z'') i'']),
  1.1492 +                      mk_Lev ss (HOLogic.mk_Suc nat) i $ z));
  1.1493 +              in
  1.1494 +                HOLogic.mk_imp (HOLogic.mk_eq (mk_rv ss kl i $ z, mk_InN activeAs z' i'),
  1.1495 +                  (Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct'' ks (drop m sets) zs_copy2)))
  1.1496 +              end;
  1.1497 +          in
  1.1498 +            HOLogic.mk_imp (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z),
  1.1499 +              Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct' ks setssAs ss zs_copy))
  1.1500 +          end;
  1.1501 +
  1.1502 +        val goal = list_all_free (kl :: zs @ zs_copy @ zs_copy2)
  1.1503 +          (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs));
  1.1504 +
  1.1505 +        val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
  1.1506 +
  1.1507 +        val set_Lev = singleton (Proof_Context.export names_lthy lthy)
  1.1508 +          (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
  1.1509 +            (K (mk_set_Lev_tac lthy cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss)))
  1.1510 +          |> Thm.close_derivation;
  1.1511 +
  1.1512 +        val set_Lev' = mk_specN (3 * n + 1) set_Lev;
  1.1513 +      in
  1.1514 +        map (fn i => map (fn i' => map (fn i'' => set_Lev' RS
  1.1515 +          mk_conjunctN n i RS mp RS
  1.1516 +          mk_conjunctN n i' RS mp RS
  1.1517 +          mk_conjunctN n i'' RS mp) ks) ks) ks
  1.1518 +      end;
  1.1519 +
  1.1520 +    val set_image_Lev_thmsss =
  1.1521 +      let
  1.1522 +        fun mk_conjunct i z =
  1.1523 +          let
  1.1524 +            fun mk_conjunct' i' sets =
  1.1525 +              let
  1.1526 +                fun mk_conjunct'' i'' set s z'' = HOLogic.mk_imp
  1.1527 +                  (HOLogic.mk_eq (mk_rv ss kl i $ z, mk_InN activeAs z'' i''),
  1.1528 +                  HOLogic.mk_mem (k, mk_image (mk_to_sbd s z'' i'' i') $ (set $ (s $ z''))));
  1.1529 +              in
  1.1530 +                HOLogic.mk_imp (HOLogic.mk_mem
  1.1531 +                  (mk_append (kl, HOLogic.mk_list sum_sbdT [mk_InN sbdTs k i']),
  1.1532 +                    mk_Lev ss (HOLogic.mk_Suc nat) i $ z),
  1.1533 +                  (Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct'' ks sets ss zs_copy)))
  1.1534 +              end;
  1.1535 +          in
  1.1536 +            HOLogic.mk_imp (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z),
  1.1537 +              Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct' ks (drop m setssAs')))
  1.1538 +          end;
  1.1539 +
  1.1540 +        val goal = list_all_free (kl :: k :: zs @ zs_copy)
  1.1541 +          (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs));
  1.1542 +
  1.1543 +        val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
  1.1544 +
  1.1545 +        val set_image_Lev = singleton (Proof_Context.export names_lthy lthy)
  1.1546 +          (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
  1.1547 +            (K (mk_set_image_Lev_tac lthy cts Lev_0s Lev_Sucs rv_Nils rv_Conss
  1.1548 +              from_to_sbd_thmss to_sbd_inj_thmss)))
  1.1549 +          |> Thm.close_derivation;
  1.1550 +
  1.1551 +        val set_image_Lev' = mk_specN (2 * n + 2) set_image_Lev;
  1.1552 +      in
  1.1553 +        map (fn i => map (fn i' => map (fn i'' => set_image_Lev' RS
  1.1554 +          mk_conjunctN n i RS mp RS
  1.1555 +          mk_conjunctN n i'' RS mp RS
  1.1556 +          mk_conjunctN n i' RS mp) ks) ks) ks
  1.1557 +      end;
  1.1558 +
  1.1559 +    val mor_beh_thm =
  1.1560 +      Goal.prove_sorry lthy [] []
  1.1561 +        (fold_rev Logic.all (As @ Bs @ ss) (Logic.mk_implies (coalg_prem,
  1.1562 +          HOLogic.mk_Trueprop (mk_mor Bs ss carTAs strTAs (map (mk_beh ss) ks)))))
  1.1563 +        (mk_mor_beh_tac m mor_def mor_cong_thm
  1.1564 +          beh_defs carT_defs strT_defs isNode_defs
  1.1565 +          to_sbd_inj_thmss from_to_sbd_thmss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbd_thms
  1.1566 +          length_Lev_thms length_Lev'_thms prefCl_Lev_thms rv_last_thmss
  1.1567 +          set_rv_Lev_thmsss set_Lev_thmsss set_image_Lev_thmsss
  1.1568 +          set_mapss coalg_set_thmss map_comp_id_thms map_cong0s map_arg_cong_thms)
  1.1569 +      |> Thm.close_derivation;
  1.1570 +
  1.1571 +    val timer = time (timer "Behavioral morphism");
  1.1572 +
  1.1573 +    fun mk_LSBIS As i = mk_lsbis As (map (mk_carT As) ks) strTAs i;
  1.1574 +    fun mk_car_final As i =
  1.1575 +      mk_quotient (mk_carT As i) (mk_LSBIS As i);
  1.1576 +    fun mk_str_final As i =
  1.1577 +      mk_univ (HOLogic.mk_comp (Term.list_comb (nth final_maps (i - 1),
  1.1578 +        passive_ids @ map (mk_proj o mk_LSBIS As) ks), nth strTAs (i - 1)));
  1.1579 +
  1.1580 +    val car_finalAs = map (mk_car_final As) ks;
  1.1581 +    val str_finalAs = map (mk_str_final As) ks;
  1.1582 +    val car_finals = map (mk_car_final passive_UNIVs) ks;
  1.1583 +    val str_finals = map (mk_str_final passive_UNIVs) ks;
  1.1584 +
  1.1585 +    val coalgT_set_thmss = map (map (fn thm => coalgT_thm RS thm)) coalg_set_thmss;
  1.1586 +    val equiv_LSBIS_thms = map (fn thm => coalgT_thm RS thm) equiv_lsbis_thms;
  1.1587 +
  1.1588 +    val congruent_str_final_thms =
  1.1589 +      let
  1.1590 +        fun mk_goal R final_map strT =
  1.1591 +          fold_rev Logic.all As (HOLogic.mk_Trueprop
  1.1592 +            (mk_congruent R (HOLogic.mk_comp
  1.1593 +              (Term.list_comb (final_map, passive_ids @ map (mk_proj o mk_LSBIS As) ks), strT))));
  1.1594 +
  1.1595 +        val goals = map3 mk_goal (map (mk_LSBIS As) ks) final_maps strTAs;
  1.1596 +      in
  1.1597 +        map4 (fn goal => fn lsbisE => fn map_comp_id => fn map_cong0 =>
  1.1598 +          Goal.prove_sorry lthy [] [] goal
  1.1599 +            (K (mk_congruent_str_final_tac m lsbisE map_comp_id map_cong0 equiv_LSBIS_thms))
  1.1600 +          |> Thm.close_derivation)
  1.1601 +        goals lsbisE_thms map_comp_id_thms map_cong0s
  1.1602 +      end;
  1.1603 +
  1.1604 +    val coalg_final_thm = Goal.prove_sorry lthy [] [] (fold_rev Logic.all As
  1.1605 +      (HOLogic.mk_Trueprop (mk_coalg As car_finalAs str_finalAs)))
  1.1606 +      (K (mk_coalg_final_tac m coalg_def congruent_str_final_thms equiv_LSBIS_thms
  1.1607 +        set_mapss coalgT_set_thmss))
  1.1608 +      |> Thm.close_derivation;
  1.1609 +
  1.1610 +    val mor_T_final_thm = Goal.prove_sorry lthy [] [] (fold_rev Logic.all As
  1.1611 +      (HOLogic.mk_Trueprop (mk_mor carTAs strTAs car_finalAs str_finalAs
  1.1612 +        (map (mk_proj o mk_LSBIS As) ks))))
  1.1613 +      (K (mk_mor_T_final_tac mor_def congruent_str_final_thms equiv_LSBIS_thms))
  1.1614 +      |> Thm.close_derivation;
  1.1615 +
  1.1616 +    val mor_final_thm = mor_comp_thm OF [mor_beh_thm, mor_T_final_thm];
  1.1617 +    val in_car_final_thms = map (fn mor_image' => mor_image' OF
  1.1618 +      [tcoalg_thm RS mor_final_thm, UNIV_I]) mor_image'_thms;
  1.1619 +
  1.1620 +    val timer = time (timer "Final coalgebra");
  1.1621 +
  1.1622 +    val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
  1.1623 +      lthy
  1.1624 +      |> fold_map4 (fn b => fn mx => fn car_final => fn in_car_final =>
  1.1625 +        typedef (Binding.conceal b, params, mx) car_final NONE
  1.1626 +          (EVERY' [rtac exI, rtac in_car_final] 1)) bs mixfixes car_finals in_car_final_thms
  1.1627 +      |>> apsnd split_list o split_list;
  1.1628 +
  1.1629 +    val Ts = map (fn name => Type (name, params')) T_names;
  1.1630 +    fun mk_Ts passive = map (Term.typ_subst_atomic (passiveAs ~~ passive)) Ts;
  1.1631 +    val Ts' = mk_Ts passiveBs;
  1.1632 +    val Rep_Ts = map2 (fn info => fn T => Const (#Rep_name info, T --> treeQT)) T_glob_infos Ts;
  1.1633 +    val Abs_Ts = map2 (fn info => fn T => Const (#Abs_name info, treeQT --> T)) T_glob_infos Ts;
  1.1634 +
  1.1635 +    val Reps = map #Rep T_loc_infos;
  1.1636 +    val Rep_injects = map #Rep_inject T_loc_infos;
  1.1637 +    val Abs_inverses = map #Abs_inverse T_loc_infos;
  1.1638 +
  1.1639 +    val timer = time (timer "THE TYPEDEFs & Rep/Abs thms");
  1.1640 +
  1.1641 +    val UNIVs = map HOLogic.mk_UNIV Ts;
  1.1642 +    val FTs = mk_FTs (passiveAs @ Ts);
  1.1643 +    val FTs' = mk_FTs (passiveBs @ Ts);
  1.1644 +    val prodTs = map (HOLogic.mk_prodT o `I) Ts;
  1.1645 +    val prodFTs = mk_FTs (passiveAs @ prodTs);
  1.1646 +    val FTs_setss = mk_setss (passiveAs @ Ts);
  1.1647 +    val prodFT_setss = mk_setss (passiveAs @ prodTs);
  1.1648 +    val map_FTs = map2 (fn Ds => mk_map_of_bnf Ds treeQTs (passiveAs @ Ts)) Dss bnfs;
  1.1649 +    val map_FT_nths = map2 (fn Ds =>
  1.1650 +      mk_map_of_bnf Ds (passiveAs @ prodTs) (passiveAs @ Ts)) Dss bnfs;
  1.1651 +    val fstsTs = map fst_const prodTs;
  1.1652 +    val sndsTs = map snd_const prodTs;
  1.1653 +    val dtorTs = map2 (curry op -->) Ts FTs;
  1.1654 +    val ctorTs = map2 (curry op -->) FTs Ts;
  1.1655 +    val unfold_fTs = map2 (curry op -->) activeAs Ts;
  1.1656 +    val corec_sTs = map (Term.typ_subst_atomic (activeBs ~~ Ts)) sum_sTs;
  1.1657 +    val corec_maps = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_Inls;
  1.1658 +    val corec_maps_rev = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_Inls_rev;
  1.1659 +    val corec_Inls = map (Term.subst_atomic_types (activeBs ~~ Ts)) Inls;
  1.1660 +    val corec_UNIVs = map2 (HOLogic.mk_UNIV oo curry mk_sumT) Ts activeAs;
  1.1661 +
  1.1662 +    val (((((((((((((Jzs, Jzs'), Jz's), Jzs_copy), Jz's_copy), Jzs1), Jzs2),
  1.1663 +      FJzs), TRs), unfold_fs), corec_ss), phis), dtor_set_induct_phiss),
  1.1664 +      names_lthy) = names_lthy
  1.1665 +      |> mk_Frees' "z" Ts
  1.1666 +      ||>> mk_Frees "y" Ts'
  1.1667 +      ||>> mk_Frees "z'" Ts
  1.1668 +      ||>> mk_Frees "y'" Ts'
  1.1669 +      ||>> mk_Frees "z1" Ts
  1.1670 +      ||>> mk_Frees "z2" Ts
  1.1671 +      ||>> mk_Frees "x" prodFTs
  1.1672 +      ||>> mk_Frees "r" (map (mk_relT o `I) Ts)
  1.1673 +      ||>> mk_Frees "f" unfold_fTs
  1.1674 +      ||>> mk_Frees "s" corec_sTs
  1.1675 +      ||>> mk_Frees "P" (map2 mk_pred2T Ts Ts)
  1.1676 +      ||>> mk_Freess "P" (map (fn A => map (mk_pred2T A) Ts) passiveAs);
  1.1677 +
  1.1678 +    fun dtor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtorN ^ "_");
  1.1679 +    val dtor_name = Binding.name_of o dtor_bind;
  1.1680 +    val dtor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o dtor_bind;
  1.1681 +
  1.1682 +    fun dtor_spec i rep str map_FT dtorT Jz Jz' =
  1.1683 +      let
  1.1684 +        val lhs = Free (dtor_name i, dtorT);
  1.1685 +        val rhs = Term.absfree Jz'
  1.1686 +          (Term.list_comb (map_FT, map HOLogic.id_const passiveAs @ Abs_Ts) $
  1.1687 +            (str $ (rep $ Jz)));
  1.1688 +      in
  1.1689 +        mk_Trueprop_eq (lhs, rhs)
  1.1690 +      end;
  1.1691 +
  1.1692 +    val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) =
  1.1693 +      lthy
  1.1694 +      |> fold_map7 (fn i => fn rep => fn str => fn mapx => fn dtorT => fn Jz => fn Jz' =>
  1.1695 +        Specification.definition (SOME (dtor_bind i, NONE, NoSyn),
  1.1696 +          (dtor_def_bind i, dtor_spec i rep str mapx dtorT Jz Jz')))
  1.1697 +        ks Rep_Ts str_finals map_FTs dtorTs Jzs Jzs'
  1.1698 +      |>> apsnd split_list o split_list
  1.1699 +      ||> `Local_Theory.restore;
  1.1700 +
  1.1701 +    val phi = Proof_Context.export_morphism lthy_old lthy;
  1.1702 +    fun mk_dtors passive =
  1.1703 +      map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (mk_params passive)) o
  1.1704 +        Morphism.term phi) dtor_frees;
  1.1705 +    val dtors = mk_dtors passiveAs;
  1.1706 +    val dtor's = mk_dtors passiveBs;
  1.1707 +    val dtor_defs = map ((fn thm => thm RS fun_cong) o Morphism.thm phi) dtor_def_frees;
  1.1708 +
  1.1709 +    val coalg_final_set_thmss = map (map (fn thm => coalg_final_thm RS thm)) coalg_set_thmss;
  1.1710 +    val (mor_Rep_thm, mor_Abs_thm) =
  1.1711 +      let
  1.1712 +        val mor_Rep =
  1.1713 +          Goal.prove_sorry lthy [] []
  1.1714 +            (HOLogic.mk_Trueprop (mk_mor UNIVs dtors car_finals str_finals Rep_Ts))
  1.1715 +            (mk_mor_Rep_tac m (mor_def :: dtor_defs) Reps Abs_inverses coalg_final_set_thmss
  1.1716 +              map_comp_id_thms map_cong0L_thms)
  1.1717 +          |> Thm.close_derivation;
  1.1718 +
  1.1719 +        val mor_Abs =
  1.1720 +          Goal.prove_sorry lthy [] []
  1.1721 +            (HOLogic.mk_Trueprop (mk_mor car_finals str_finals UNIVs dtors Abs_Ts))
  1.1722 +            (mk_mor_Abs_tac (mor_def :: dtor_defs) Abs_inverses)
  1.1723 +          |> Thm.close_derivation;
  1.1724 +      in
  1.1725 +        (mor_Rep, mor_Abs)
  1.1726 +      end;
  1.1727 +
  1.1728 +    val timer = time (timer "dtor definitions & thms");
  1.1729 +
  1.1730 +    fun unfold_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtor_unfoldN ^ "_");
  1.1731 +    val unfold_name = Binding.name_of o unfold_bind;
  1.1732 +    val unfold_def_bind = rpair [] o Binding.conceal o Thm.def_binding o unfold_bind;
  1.1733 +
  1.1734 +    fun unfold_spec i T AT abs f z z' =
  1.1735 +      let
  1.1736 +        val unfoldT = Library.foldr (op -->) (sTs, AT --> T);
  1.1737 +
  1.1738 +        val lhs = Term.list_comb (Free (unfold_name i, unfoldT), ss);
  1.1739 +        val rhs = Term.absfree z' (abs $ (f $ z));
  1.1740 +      in
  1.1741 +        mk_Trueprop_eq (lhs, rhs)
  1.1742 +      end;
  1.1743 +
  1.1744 +    val ((unfold_frees, (_, unfold_def_frees)), (lthy, lthy_old)) =
  1.1745 +      lthy
  1.1746 +      |> fold_map7 (fn i => fn T => fn AT => fn abs => fn f => fn z => fn z' =>
  1.1747 +        Specification.definition
  1.1748 +          (SOME (unfold_bind i, NONE, NoSyn), (unfold_def_bind i, unfold_spec i T AT abs f z z')))
  1.1749 +          ks Ts activeAs Abs_Ts (map (fn i => HOLogic.mk_comp
  1.1750 +            (mk_proj (mk_LSBIS passive_UNIVs i), mk_beh ss i)) ks) zs zs'
  1.1751 +      |>> apsnd split_list o split_list
  1.1752 +      ||> `Local_Theory.restore;
  1.1753 +
  1.1754 +    val phi = Proof_Context.export_morphism lthy_old lthy;
  1.1755 +    val unfolds = map (Morphism.term phi) unfold_frees;
  1.1756 +    val unfold_names = map (fst o dest_Const) unfolds;
  1.1757 +    fun mk_unfolds passives actives =
  1.1758 +      map3 (fn name => fn T => fn active =>
  1.1759 +        Const (name, Library.foldr (op -->)
  1.1760 +          (map2 (curry op -->) actives (mk_FTs (passives @ actives)), active --> T)))
  1.1761 +      unfold_names (mk_Ts passives) actives;
  1.1762 +    fun mk_unfold Ts ss i = Term.list_comb (Const (nth unfold_names (i - 1), Library.foldr (op -->)
  1.1763 +      (map fastype_of ss, domain_type (fastype_of (nth ss (i - 1))) --> nth Ts (i - 1))), ss);
  1.1764 +    val unfold_defs = map ((fn thm => thm RS fun_cong) o Morphism.thm phi) unfold_def_frees;
  1.1765 +
  1.1766 +    val mor_unfold_thm =
  1.1767 +      let
  1.1768 +        val Abs_inverses' = map2 (curry op RS) in_car_final_thms Abs_inverses;
  1.1769 +        val morEs' = map (fn thm =>
  1.1770 +          (thm OF [tcoalg_thm RS mor_final_thm, UNIV_I]) RS sym) morE_thms;
  1.1771 +      in
  1.1772 +        Goal.prove_sorry lthy [] []
  1.1773 +          (fold_rev Logic.all ss
  1.1774 +            (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors (map (mk_unfold Ts ss) ks))))
  1.1775 +          (K (mk_mor_unfold_tac m mor_UNIV_thm dtor_defs unfold_defs Abs_inverses' morEs'
  1.1776 +            map_comp_id_thms map_cong0s))
  1.1777 +        |> Thm.close_derivation
  1.1778 +      end;
  1.1779 +    val dtor_unfold_thms = map (fn thm => (thm OF [mor_unfold_thm, UNIV_I]) RS sym) morE_thms;
  1.1780 +
  1.1781 +    val (raw_coind_thms, raw_coind_thm) =
  1.1782 +      let
  1.1783 +        val prem = HOLogic.mk_Trueprop (mk_sbis passive_UNIVs UNIVs dtors TRs);
  1.1784 +        val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  1.1785 +          (map2 (fn R => fn T => mk_leq R (Id_const T)) TRs Ts));
  1.1786 +        val goal = fold_rev Logic.all TRs (Logic.mk_implies (prem, concl));
  1.1787 +      in
  1.1788 +        `split_conj_thm (Goal.prove_sorry lthy [] [] goal
  1.1789 +          (K (mk_raw_coind_tac bis_def bis_cong_thm bis_O_thm bis_converse_thm bis_Gr_thm
  1.1790 +            tcoalg_thm coalgT_thm mor_T_final_thm sbis_lsbis_thm
  1.1791 +            lsbis_incl_thms incl_lsbis_thms equiv_LSBIS_thms mor_Rep_thm Rep_injects))
  1.1792 +          |> Thm.close_derivation)
  1.1793 +      end;
  1.1794 +
  1.1795 +    val (unfold_unique_mor_thms, unfold_unique_mor_thm) =
  1.1796 +      let
  1.1797 +        val prem = HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors unfold_fs);
  1.1798 +        fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_unfold Ts ss i);
  1.1799 +        val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  1.1800 +          (map2 mk_fun_eq unfold_fs ks));
  1.1801 +
  1.1802 +        val bis_thm = tcoalg_thm RSN (2, tcoalg_thm RS bis_image2_thm);
  1.1803 +        val mor_thm = mor_comp_thm OF [tcoalg_thm RS mor_final_thm, mor_Abs_thm];
  1.1804 +
  1.1805 +        val unique_mor = Goal.prove_sorry lthy [] []
  1.1806 +          (fold_rev Logic.all (ss @ unfold_fs) (Logic.mk_implies (prem, unique)))
  1.1807 +          (K (mk_unfold_unique_mor_tac raw_coind_thms bis_thm mor_thm unfold_defs))
  1.1808 +          |> Thm.close_derivation;
  1.1809 +      in
  1.1810 +        `split_conj_thm unique_mor
  1.1811 +      end;
  1.1812 +
  1.1813 +    val (dtor_unfold_unique_thms, dtor_unfold_unique_thm) = `split_conj_thm (split_conj_prems n
  1.1814 +      (mor_UNIV_thm RS iffD2 RS unfold_unique_mor_thm));
  1.1815 +
  1.1816 +    val unfold_dtor_thms = map (fn thm => mor_id_thm RS thm RS sym) unfold_unique_mor_thms;
  1.1817 +
  1.1818 +    val unfold_o_dtor_thms =
  1.1819 +      let
  1.1820 +        val mor = mor_comp_thm OF [mor_str_thm, mor_unfold_thm];
  1.1821 +      in
  1.1822 +        map2 (fn unique => fn unfold_ctor =>
  1.1823 +          trans OF [mor RS unique, unfold_ctor]) unfold_unique_mor_thms unfold_dtor_thms
  1.1824 +      end;
  1.1825 +
  1.1826 +    val timer = time (timer "unfold definitions & thms");
  1.1827 +
  1.1828 +    val map_dtors = map2 (fn Ds => fn bnf =>
  1.1829 +      Term.list_comb (mk_map_of_bnf Ds (passiveAs @ Ts) (passiveAs @ FTs) bnf,
  1.1830 +        map HOLogic.id_const passiveAs @ dtors)) Dss bnfs;
  1.1831 +
  1.1832 +    fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_");
  1.1833 +    val ctor_name = Binding.name_of o ctor_bind;
  1.1834 +    val ctor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o ctor_bind;
  1.1835 +
  1.1836 +    fun ctor_spec i ctorT =
  1.1837 +      let
  1.1838 +        val lhs = Free (ctor_name i, ctorT);
  1.1839 +        val rhs = mk_unfold Ts map_dtors i;
  1.1840 +      in
  1.1841 +        mk_Trueprop_eq (lhs, rhs)
  1.1842 +      end;
  1.1843 +
  1.1844 +    val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) =
  1.1845 +      lthy
  1.1846 +      |> fold_map2 (fn i => fn ctorT =>
  1.1847 +        Specification.definition
  1.1848 +          (SOME (ctor_bind i, NONE, NoSyn), (ctor_def_bind i, ctor_spec i ctorT))) ks ctorTs
  1.1849 +      |>> apsnd split_list o split_list
  1.1850 +      ||> `Local_Theory.restore;
  1.1851 +
  1.1852 +    val phi = Proof_Context.export_morphism lthy_old lthy;
  1.1853 +    fun mk_ctors params =
  1.1854 +      map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ params) o Morphism.term phi)
  1.1855 +        ctor_frees;
  1.1856 +    val ctors = mk_ctors params';
  1.1857 +    val ctor_defs = map (Morphism.thm phi) ctor_def_frees;
  1.1858 +
  1.1859 +    val ctor_o_dtor_thms = map2 (fold_thms lthy o single) ctor_defs unfold_o_dtor_thms;
  1.1860 +
  1.1861 +    val dtor_o_ctor_thms =
  1.1862 +      let
  1.1863 +        fun mk_goal dtor ctor FT =
  1.1864 +         mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT);
  1.1865 +        val goals = map3 mk_goal dtors ctors FTs;
  1.1866 +      in
  1.1867 +        map5 (fn goal => fn ctor_def => fn unfold => fn map_comp_id => fn map_cong0L =>
  1.1868 +          Goal.prove_sorry lthy [] [] goal
  1.1869 +            (mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_cong0L unfold_o_dtor_thms)
  1.1870 +          |> Thm.close_derivation)
  1.1871 +          goals ctor_defs dtor_unfold_thms map_comp_id_thms map_cong0L_thms
  1.1872 +      end;
  1.1873 +
  1.1874 +    val dtor_ctor_thms = map (fn thm => thm RS @{thm pointfree_idE}) dtor_o_ctor_thms;
  1.1875 +    val ctor_dtor_thms = map (fn thm => thm RS @{thm pointfree_idE}) ctor_o_dtor_thms;
  1.1876 +
  1.1877 +    val bij_dtor_thms =
  1.1878 +      map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) ctor_o_dtor_thms dtor_o_ctor_thms;
  1.1879 +    val inj_dtor_thms = map (fn thm => thm RS @{thm bij_is_inj}) bij_dtor_thms;
  1.1880 +    val surj_dtor_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_dtor_thms;
  1.1881 +    val dtor_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_dtor_thms;
  1.1882 +    val dtor_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_dtor_thms;
  1.1883 +    val dtor_exhaust_thms = map (fn thm => thm RS exE) dtor_nchotomy_thms;
  1.1884 +
  1.1885 +    val bij_ctor_thms =
  1.1886 +      map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) dtor_o_ctor_thms ctor_o_dtor_thms;
  1.1887 +    val inj_ctor_thms = map (fn thm => thm RS @{thm bij_is_inj}) bij_ctor_thms;
  1.1888 +    val surj_ctor_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_ctor_thms;
  1.1889 +    val ctor_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_ctor_thms;
  1.1890 +    val ctor_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_ctor_thms;
  1.1891 +    val ctor_exhaust_thms = map (fn thm => thm RS exE) ctor_nchotomy_thms;
  1.1892 +
  1.1893 +    val timer = time (timer "ctor definitions & thms");
  1.1894 +
  1.1895 +    val corec_Inl_sum_thms =
  1.1896 +      let
  1.1897 +        val mor = mor_comp_thm OF [mor_sum_case_thm, mor_unfold_thm];
  1.1898 +      in
  1.1899 +        map2 (fn unique => fn unfold_dtor =>
  1.1900 +          trans OF [mor RS unique, unfold_dtor]) unfold_unique_mor_thms unfold_dtor_thms
  1.1901 +      end;
  1.1902 +
  1.1903 +    fun corec_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtor_corecN ^ "_");
  1.1904 +    val corec_name = Binding.name_of o corec_bind;
  1.1905 +    val corec_def_bind = rpair [] o Binding.conceal o Thm.def_binding o corec_bind;
  1.1906 +
  1.1907 +    val corec_strs =
  1.1908 +      map3 (fn dtor => fn sum_s => fn mapx =>
  1.1909 +        mk_sum_case
  1.1910 +          (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ corec_Inls), dtor), sum_s))
  1.1911 +      dtors corec_ss corec_maps;
  1.1912 +
  1.1913 +    fun corec_spec i T AT =
  1.1914 +      let
  1.1915 +        val corecT = Library.foldr (op -->) (corec_sTs, AT --> T);
  1.1916 +
  1.1917 +        val lhs = Term.list_comb (Free (corec_name i, corecT), corec_ss);
  1.1918 +        val rhs = HOLogic.mk_comp (mk_unfold Ts corec_strs i, Inr_const T AT);
  1.1919 +      in
  1.1920 +        mk_Trueprop_eq (lhs, rhs)
  1.1921 +      end;
  1.1922 +
  1.1923 +    val ((corec_frees, (_, corec_def_frees)), (lthy, lthy_old)) =
  1.1924 +      lthy
  1.1925 +      |> fold_map3 (fn i => fn T => fn AT =>
  1.1926 +        Specification.definition
  1.1927 +          (SOME (corec_bind i, NONE, NoSyn), (corec_def_bind i, corec_spec i T AT)))
  1.1928 +          ks Ts activeAs
  1.1929 +      |>> apsnd split_list o split_list
  1.1930 +      ||> `Local_Theory.restore;
  1.1931 +
  1.1932 +    val phi = Proof_Context.export_morphism lthy_old lthy;
  1.1933 +    val corecs = map (Morphism.term phi) corec_frees;
  1.1934 +    val corec_names = map (fst o dest_Const) corecs;
  1.1935 +    fun mk_corec ss i = Term.list_comb (Const (nth corec_names (i - 1), Library.foldr (op -->)
  1.1936 +      (map fastype_of ss, domain_type (fastype_of (nth ss (i - 1))) --> nth Ts (i - 1))), ss);
  1.1937 +    val corec_defs = map (Morphism.thm phi) corec_def_frees;
  1.1938 +
  1.1939 +    val sum_cases =
  1.1940 +      map2 (fn T => fn i => mk_sum_case (HOLogic.id_const T, mk_corec corec_ss i)) Ts ks;
  1.1941 +    val dtor_corec_thms =
  1.1942 +      let
  1.1943 +        fun mk_goal i corec_s corec_map dtor z =
  1.1944 +          let
  1.1945 +            val lhs = dtor $ (mk_corec corec_ss i $ z);
  1.1946 +            val rhs = Term.list_comb (corec_map, passive_ids @ sum_cases) $ (corec_s $ z);
  1.1947 +          in
  1.1948 +            fold_rev Logic.all (z :: corec_ss) (mk_Trueprop_eq (lhs, rhs))
  1.1949 +          end;
  1.1950 +        val goals = map5 mk_goal ks corec_ss corec_maps_rev dtors zs;
  1.1951 +      in
  1.1952 +        map3 (fn goal => fn unfold => fn map_cong0 =>
  1.1953 +          Goal.prove_sorry lthy [] [] goal
  1.1954 +            (mk_corec_tac m corec_defs unfold map_cong0 corec_Inl_sum_thms)
  1.1955 +          |> Thm.close_derivation)
  1.1956 +        goals dtor_unfold_thms map_cong0s
  1.1957 +      end;
  1.1958 +
  1.1959 +    val corec_unique_mor_thm =
  1.1960 +      let
  1.1961 +        val id_fs = map2 (fn T => fn f => mk_sum_case (HOLogic.id_const T, f)) Ts unfold_fs;
  1.1962 +        val prem = HOLogic.mk_Trueprop (mk_mor corec_UNIVs corec_strs UNIVs dtors id_fs);
  1.1963 +        fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_corec corec_ss i);
  1.1964 +        val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  1.1965 +          (map2 mk_fun_eq unfold_fs ks));
  1.1966 +      in
  1.1967 +        Goal.prove_sorry lthy [] []
  1.1968 +          (fold_rev Logic.all (corec_ss @ unfold_fs) (Logic.mk_implies (prem, unique)))
  1.1969 +          (mk_corec_unique_mor_tac corec_defs corec_Inl_sum_thms unfold_unique_mor_thm)
  1.1970 +          |> Thm.close_derivation
  1.1971 +      end;
  1.1972 +
  1.1973 +    val map_id0s_o_id =
  1.1974 +      map (fn thm =>
  1.1975 +        mk_trans (thm RS @{thm arg_cong2[of _ _ _ _ "op o", OF _ refl]}) @{thm id_o})
  1.1976 +      map_id0s;
  1.1977 +
  1.1978 +    val (dtor_corec_unique_thms, dtor_corec_unique_thm) =
  1.1979 +      `split_conj_thm (split_conj_prems n
  1.1980 +        (mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm)
  1.1981 +        |> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o o_assoc sum_case_o_inj(1)} @
  1.1982 +           map_id0s_o_id @ sym_map_comps)
  1.1983 +        OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]});
  1.1984 +
  1.1985 +    val timer = time (timer "corec definitions & thms");
  1.1986 +
  1.1987 +    val (dtor_map_coinduct_thm, coinduct_params, dtor_coinduct_thm) =
  1.1988 +      let
  1.1989 +        val zs = Jzs1 @ Jzs2;
  1.1990 +        val frees = phis @ zs;
  1.1991 +
  1.1992 +        val rels = map (Term.subst_atomic_types ((activeAs ~~ Ts) @ (activeBs ~~ Ts))) relsAsBs;
  1.1993 +
  1.1994 +        fun mk_concl phi z1 z2 = HOLogic.mk_imp (phi $ z1 $ z2, HOLogic.mk_eq (z1, z2));
  1.1995 +        val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  1.1996 +          (map3 mk_concl phis Jzs1 Jzs2));
  1.1997 +
  1.1998 +        fun mk_rel_prem phi dtor rel Jz Jz_copy =
  1.1999 +          let
  1.2000 +            val concl = Term.list_comb (rel, map HOLogic.eq_const passiveAs @ phis) $
  1.2001 +              (dtor $ Jz) $ (dtor $ Jz_copy);
  1.2002 +          in
  1.2003 +            HOLogic.mk_Trueprop
  1.2004 +              (list_all_free [Jz, Jz_copy] (HOLogic.mk_imp (phi $ Jz $ Jz_copy, concl)))
  1.2005 +          end;
  1.2006 +
  1.2007 +        val rel_prems = map5 mk_rel_prem phis dtors rels Jzs Jzs_copy;
  1.2008 +        val dtor_coinduct_goal =
  1.2009 +          fold_rev Logic.all frees (Logic.list_implies (rel_prems, concl));
  1.2010 +
  1.2011 +        val dtor_coinduct =
  1.2012 +          Goal.prove_sorry lthy [] [] dtor_coinduct_goal
  1.2013 +            (K (mk_dtor_coinduct_tac m raw_coind_thm bis_rel_thm rel_congs))
  1.2014 +          |> Thm.close_derivation;
  1.2015 +
  1.2016 +        fun mk_prem phi dtor map_nth sets Jz Jz_copy FJz =
  1.2017 +          let
  1.2018 +            val xs = [Jz, Jz_copy];
  1.2019 +
  1.2020 +            fun mk_map_conjunct nths x =
  1.2021 +              HOLogic.mk_eq (Term.list_comb (map_nth, passive_ids @ nths) $ FJz, dtor $ x);
  1.2022 +
  1.2023 +            fun mk_set_conjunct set phi z1 z2 =
  1.2024 +              list_all_free [z1, z2]
  1.2025 +                (HOLogic.mk_imp (HOLogic.mk_mem (HOLogic.mk_prod (z1, z2), set $ FJz),
  1.2026 +                  phi $ z1 $ z2));
  1.2027 +
  1.2028 +            val concl = list_exists_free [FJz] (HOLogic.mk_conj
  1.2029 +              (Library.foldr1 HOLogic.mk_conj (map2 mk_map_conjunct [fstsTs, sndsTs] xs),
  1.2030 +              Library.foldr1 HOLogic.mk_conj
  1.2031 +                (map4 mk_set_conjunct (drop m sets) phis Jzs1 Jzs2)));
  1.2032 +          in
  1.2033 +            fold_rev Logic.all xs (Logic.mk_implies
  1.2034 +              (HOLogic.mk_Trueprop (Term.list_comb (phi, xs)), HOLogic.mk_Trueprop concl))
  1.2035 +          end;
  1.2036 +
  1.2037 +        val prems = map7 mk_prem phis dtors map_FT_nths prodFT_setss Jzs Jzs_copy FJzs;
  1.2038 +
  1.2039 +        val dtor_map_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (prems, concl));
  1.2040 +        val dtor_map_coinduct =
  1.2041 +          Goal.prove_sorry lthy [] [] dtor_map_coinduct_goal
  1.2042 +            (K (mk_dtor_map_coinduct_tac m ks raw_coind_thm bis_def))
  1.2043 +          |> Thm.close_derivation;
  1.2044 +      in
  1.2045 +        (dtor_map_coinduct, rev (Term.add_tfrees dtor_map_coinduct_goal []), dtor_coinduct)
  1.2046 +      end;
  1.2047 +
  1.2048 +    val timer = time (timer "coinduction");
  1.2049 +
  1.2050 +    val setss_by_bnf = map (fn i => map2 (mk_hset dtors i) ls passiveAs) ks;
  1.2051 +    val setss_by_range = transpose setss_by_bnf;
  1.2052 +
  1.2053 +    val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, dtor_hset_induct_thms) =
  1.2054 +      let
  1.2055 +        fun tinst_of dtor =
  1.2056 +          map (SOME o certify lthy) (dtor :: remove (op =) dtor dtors);
  1.2057 +        fun tinst_of' dtor = case tinst_of dtor of t :: ts => t :: NONE :: ts;
  1.2058 +        val Tinst = map (pairself (certifyT lthy))
  1.2059 +          (map Logic.varifyT_global (deads @ allAs) ~~ (deads @ passiveAs @ Ts));
  1.2060 +        val set_incl_thmss =
  1.2061 +          map2 (fn dtor => map (singleton (Proof_Context.export names_lthy lthy) o
  1.2062 +            Drule.instantiate' [] (tinst_of' dtor) o
  1.2063 +            Thm.instantiate (Tinst, []) o Drule.zero_var_indexes))
  1.2064 +          dtors set_incl_hset_thmss;
  1.2065 +
  1.2066 +        val tinst = splice (map (SOME o certify lthy) dtors) (replicate n NONE)
  1.2067 +        val set_minimal_thms =
  1.2068 +          map (Drule.instantiate' [] tinst o Thm.instantiate (Tinst, []) o
  1.2069 +            Drule.zero_var_indexes)
  1.2070 +          hset_minimal_thms;
  1.2071 +
  1.2072 +        val set_set_incl_thmsss =
  1.2073 +          map2 (fn dtor => map (map (singleton (Proof_Context.export names_lthy lthy) o
  1.2074 +            Drule.instantiate' [] (NONE :: tinst_of' dtor) o
  1.2075 +            Thm.instantiate (Tinst, []) o Drule.zero_var_indexes)))
  1.2076 +          dtors set_hset_incl_hset_thmsss;
  1.2077 +
  1.2078 +        val set_set_incl_thmsss' = transpose (map transpose set_set_incl_thmsss);
  1.2079 +
  1.2080 +        val incls =
  1.2081 +          maps (map (fn thm => thm RS @{thm subset_Collect_iff})) set_incl_thmss @
  1.2082 +            @{thms subset_Collect_iff[OF subset_refl]};
  1.2083 +
  1.2084 +        fun mk_induct_tinst phis jsets y y' =
  1.2085 +          map4 (fn phi => fn jset => fn Jz => fn Jz' =>
  1.2086 +            SOME (certify lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y',
  1.2087 +              HOLogic.mk_conj (HOLogic.mk_mem (y, jset $ Jz), phi $ y $ Jz))))))
  1.2088 +          phis jsets Jzs Jzs';
  1.2089 +        val dtor_set_induct_thms =
  1.2090 +          map6 (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis =>
  1.2091 +            ((set_minimal
  1.2092 +              |> Drule.instantiate' [] (mk_induct_tinst phis jsets y y')
  1.2093 +              |> unfold_thms lthy incls) OF
  1.2094 +              (replicate n ballI @
  1.2095 +                maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss))
  1.2096 +            |> singleton (Proof_Context.export names_lthy lthy)
  1.2097 +            |> rule_by_tactic lthy (ALLGOALS (TRY o etac asm_rl)))
  1.2098 +          set_minimal_thms set_set_incl_thmsss' setss_by_range ys ys' dtor_set_induct_phiss
  1.2099 +      in
  1.2100 +        (set_incl_thmss, set_set_incl_thmsss, dtor_set_induct_thms)
  1.2101 +      end;
  1.2102 +
  1.2103 +    fun mk_dtor_map_DEADID_thm dtor_inject map_id0 =
  1.2104 +      trans OF [iffD2 OF [dtor_inject, id_apply], map_id0 RS sym];
  1.2105 +
  1.2106 +    fun mk_dtor_Jrel_DEADID_thm dtor_inject bnf =
  1.2107 +      trans OF [rel_eq_of_bnf bnf RS @{thm predicate2_eqD}, dtor_inject] RS sym;
  1.2108 +
  1.2109 +    val JphiTs = map2 mk_pred2T passiveAs passiveBs;
  1.2110 +    val Jpsi1Ts = map2 mk_pred2T passiveAs passiveCs;
  1.2111 +    val Jpsi2Ts = map2 mk_pred2T passiveCs passiveBs;
  1.2112 +    val prodTsTs' = map2 (curry HOLogic.mk_prodT) Ts Ts';
  1.2113 +    val fstsTsTs' = map fst_const prodTsTs';
  1.2114 +    val sndsTsTs' = map snd_const prodTsTs';
  1.2115 +    val activephiTs = map2 mk_pred2T activeAs activeBs;
  1.2116 +    val activeJphiTs = map2 mk_pred2T Ts Ts';
  1.2117 +    val (((((Jphis, Jpsi1s), Jpsi2s), activephis), activeJphis), names_lthy) = names_lthy
  1.2118 +      |> mk_Frees "R" JphiTs
  1.2119 +      ||>> mk_Frees "R" Jpsi1Ts
  1.2120 +      ||>> mk_Frees "Q" Jpsi2Ts
  1.2121 +      ||>> mk_Frees "S" activephiTs
  1.2122 +      ||>> mk_Frees "JR" activeJphiTs;
  1.2123 +    val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
  1.2124 +    val in_rels = map in_rel_of_bnf bnfs;
  1.2125 +
  1.2126 +    fun mk_Jrel_DEADID_coinduct_thm () = 
  1.2127 +      mk_rel_xtor_co_induct_thm Greatest_FP rels activeJphis (map HOLogic.eq_const Ts) Jphis
  1.2128 +        Jzs Jz's dtors dtor's (fn {context = ctxt, prems} =>
  1.2129 +          (unfold_thms_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN
  1.2130 +          REPEAT_DETERM (rtac allI 1) THEN rtac (dtor_coinduct_thm OF prems) 1)) lthy;
  1.2131 +
  1.2132 +    (*register new codatatypes as BNFs*)
  1.2133 +    val (timer, Jbnfs, (dtor_Jmap_o_thms, dtor_Jmap_thms), dtor_Jset_thmss',
  1.2134 +      dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_notes, lthy) =
  1.2135 +      if m = 0 then
  1.2136 +        (timer, replicate n DEADID_bnf,
  1.2137 +        map_split (`(mk_pointfree lthy)) (map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_ids),
  1.2138 +        replicate n [], map2 mk_dtor_Jrel_DEADID_thm dtor_inject_thms bnfs,
  1.2139 +        mk_Jrel_DEADID_coinduct_thm (), [], lthy)
  1.2140 +      else let
  1.2141 +        val fTs = map2 (curry op -->) passiveAs passiveBs;
  1.2142 +        val gTs = map2 (curry op -->) passiveBs passiveCs;
  1.2143 +        val uTs = map2 (curry op -->) Ts Ts';
  1.2144 +
  1.2145 +        val ((((((((fs, fs'), fs_copy), gs), us), (Jys, Jys')), (Jys_copy, Jys'_copy)),
  1.2146 +          (ys_copy, ys'_copy)), names_lthy) = names_lthy
  1.2147 +          |> mk_Frees' "f" fTs
  1.2148 +          ||>> mk_Frees "f" fTs
  1.2149 +          ||>> mk_Frees "g" gTs
  1.2150 +          ||>> mk_Frees "u" uTs
  1.2151 +          ||>> mk_Frees' "b" Ts'
  1.2152 +          ||>> mk_Frees' "b" Ts'
  1.2153 +          ||>> mk_Frees' "y" passiveAs;
  1.2154 +
  1.2155 +        val map_FTFT's = map2 (fn Ds =>
  1.2156 +          mk_map_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
  1.2157 +
  1.2158 +        fun mk_maps ATs BTs Ts mk_T =
  1.2159 +          map2 (fn Ds => mk_map_of_bnf Ds (ATs @ Ts) (BTs @ map mk_T Ts)) Dss bnfs;
  1.2160 +        fun mk_Fmap mk_const fs Ts Fmap = Term.list_comb (Fmap, fs @ map mk_const Ts);
  1.2161 +        fun mk_map mk_const mk_T Ts fs Ts' dtors mk_maps =
  1.2162 +          mk_unfold Ts' (map2 (fn dtor => fn Fmap =>
  1.2163 +            HOLogic.mk_comp (mk_Fmap mk_const fs Ts Fmap, dtor)) dtors (mk_maps Ts mk_T));
  1.2164 +        val mk_map_id = mk_map HOLogic.id_const I;
  1.2165 +        val mk_mapsAB = mk_maps passiveAs passiveBs;
  1.2166 +        val fs_maps = map (mk_map_id Ts fs Ts' dtors mk_mapsAB) ks;
  1.2167 +
  1.2168 +        val set_bss =
  1.2169 +          map (flat o map2 (fn B => fn b =>
  1.2170 +            if member (op =) resDs (TFree B) then [] else [b]) resBs) set_bss0;
  1.2171 +
  1.2172 +        fun close_wit I wit = (I, fold_rev Term.absfree (map (nth ys') I) wit);
  1.2173 +
  1.2174 +        val all_unitTs = replicate live HOLogic.unitT;
  1.2175 +        val unitTs = replicate n HOLogic.unitT;
  1.2176 +        val unit_funs = replicate n (Term.absdummy HOLogic.unitT HOLogic.unit);
  1.2177 +        fun mk_map_args I =
  1.2178 +          map (fn i =>
  1.2179 +            if member (op =) I i then Term.absdummy HOLogic.unitT (nth ys i)
  1.2180 +            else mk_undefined (HOLogic.unitT --> nth passiveAs i))
  1.2181 +          (0 upto (m - 1));
  1.2182 +
  1.2183 +        fun mk_nat_wit Ds bnf (I, wit) () =
  1.2184 +          let
  1.2185 +            val passiveI = filter (fn i => i < m) I;
  1.2186 +            val map_args = mk_map_args passiveI;
  1.2187 +          in
  1.2188 +            Term.absdummy HOLogic.unitT (Term.list_comb
  1.2189 +              (mk_map_of_bnf Ds all_unitTs (passiveAs @ unitTs) bnf, map_args @ unit_funs) $ wit)
  1.2190 +          end;
  1.2191 +
  1.2192 +        fun mk_dummy_wit Ds bnf I =
  1.2193 +          let
  1.2194 +            val map_args = mk_map_args I;
  1.2195 +          in
  1.2196 +            Term.absdummy HOLogic.unitT (Term.list_comb
  1.2197 +              (mk_map_of_bnf Ds all_unitTs (passiveAs @ unitTs) bnf, map_args @ unit_funs) $
  1.2198 +              mk_undefined (mk_T_of_bnf Ds all_unitTs bnf))
  1.2199 +          end;
  1.2200 +
  1.2201 +        val nat_witss =
  1.2202 +          map2 (fn Ds => fn bnf => mk_wits_of_bnf (replicate (nwits_of_bnf bnf) Ds)
  1.2203 +            (replicate (nwits_of_bnf bnf) (replicate live HOLogic.unitT)) bnf
  1.2204 +            |> map (fn (I, wit) =>
  1.2205 +              (I, Lazy.lazy (mk_nat_wit Ds bnf (I, Term.list_comb (wit, map (K HOLogic.unit) I))))))
  1.2206 +          Dss bnfs;
  1.2207 +
  1.2208 +        val nat_wit_thmss = map2 (curry op ~~) nat_witss (map wit_thmss_of_bnf bnfs)
  1.2209 +
  1.2210 +        val Iss = map (map fst) nat_witss;
  1.2211 +
  1.2212 +        fun filter_wits (I, wit) =
  1.2213 +          let val J = filter (fn i => i < m) I;
  1.2214 +          in (J, (length J < length I, wit)) end;
  1.2215 +
  1.2216 +        val wit_treess = map_index (fn (i, Is) =>
  1.2217 +          map_index (finish Iss m [i+m] (i+m)) Is) Iss
  1.2218 +          |> map (minimize_wits o map filter_wits o minimize_wits o flat);
  1.2219 +
  1.2220 +        val coind_wit_argsss =
  1.2221 +          map (map (tree_to_coind_wits nat_wit_thmss o snd o snd) o filter (fst o snd)) wit_treess;
  1.2222 +
  1.2223 +        val nonredundant_coind_wit_argsss =
  1.2224 +          fold (fn i => fn argsss =>
  1.2225 +            nth_map (i - 1) (filter_out (fn xs =>
  1.2226 +              exists (fn ys =>
  1.2227 +                let
  1.2228 +                  val xs' = (map (fst o fst) xs, snd (fst (hd xs)));
  1.2229 +                  val ys' = (map (fst o fst) ys, snd (fst (hd ys)));
  1.2230 +                in
  1.2231 +                  eq_pair (subset (op =)) (eq_set (op =)) (xs', ys') andalso not (fst xs' = fst ys')
  1.2232 +                end)
  1.2233 +              (flat argsss)))
  1.2234 +            argsss)
  1.2235 +          ks coind_wit_argsss;
  1.2236 +
  1.2237 +        fun prepare_args args =
  1.2238 +          let
  1.2239 +            val I = snd (fst (hd args));
  1.2240 +            val (dummys, args') =
  1.2241 +              map_split (fn i =>
  1.2242 +                (case find_first (fn arg => fst (fst arg) = i - 1) args of
  1.2243 +                  SOME (_, ((_, wit), thms)) => (NONE, (Lazy.force wit, thms))
  1.2244 +                | NONE =>
  1.2245 +                  (SOME (i - 1), (mk_dummy_wit (nth Dss (i - 1)) (nth bnfs (i - 1)) I, []))))
  1.2246 +              ks;
  1.2247 +          in
  1.2248 +            ((I, dummys), apsnd flat (split_list args'))
  1.2249 +          end;
  1.2250 +
  1.2251 +        fun mk_coind_wits ((I, dummys), (args, thms)) =
  1.2252 +          ((I, dummys), (map (fn i => mk_unfold Ts args i $ HOLogic.unit) ks, thms));
  1.2253 +
  1.2254 +        val coind_witss =
  1.2255 +          maps (map (mk_coind_wits o prepare_args)) nonredundant_coind_wit_argsss;
  1.2256 +
  1.2257 +        val witss = map2 (fn Ds => fn bnf => mk_wits_of_bnf
  1.2258 +          (replicate (nwits_of_bnf bnf) Ds)
  1.2259 +          (replicate (nwits_of_bnf bnf) (passiveAs @ Ts)) bnf) Dss bnfs;
  1.2260 +
  1.2261 +        val ctor_witss =
  1.2262 +          map (map (uncurry close_wit o tree_to_ctor_wit ys ctors witss o snd o snd) o
  1.2263 +            filter_out (fst o snd)) wit_treess;
  1.2264 +
  1.2265 +        fun mk_coind_wit_thms ((I, dummys), (wits, wit_thms)) =
  1.2266 +          let
  1.2267 +            fun mk_goal sets y y_copy y'_copy j =
  1.2268 +              let
  1.2269 +                fun mk_conjunct set z dummy wit =
  1.2270 +                  mk_Ball (set $ z) (Term.absfree y'_copy
  1.2271 +                    (if dummy = NONE orelse member (op =) I (j - 1) then
  1.2272 +                      HOLogic.mk_imp (HOLogic.mk_eq (z, wit),
  1.2273 +                        if member (op =) I (j - 1) then HOLogic.mk_eq (y_copy, y)
  1.2274 +                        else @{term False})
  1.2275 +                    else @{term True}));
  1.2276 +              in
  1.2277 +                fold_rev Logic.all (map (nth ys) I @ Jzs) (HOLogic.mk_Trueprop
  1.2278 +                  (Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct sets Jzs dummys wits)))
  1.2279 +              end;
  1.2280 +            val goals = map5 mk_goal setss_by_range ys ys_copy ys'_copy ls;
  1.2281 +          in
  1.2282 +            map2 (fn goal => fn induct =>
  1.2283 +              Goal.prove_sorry lthy [] [] goal
  1.2284 +                (mk_coind_wit_tac induct dtor_unfold_thms (flat set_mapss) wit_thms)
  1.2285 +              |> Thm.close_derivation)
  1.2286 +            goals dtor_hset_induct_thms
  1.2287 +            |> map split_conj_thm
  1.2288 +            |> transpose
  1.2289 +            |> map (map_filter (try (fn thm => thm RS bspec RS mp)))
  1.2290 +            |> curry op ~~ (map_index Library.I (map (close_wit I) wits))
  1.2291 +            |> filter (fn (_, thms) => length thms = m)
  1.2292 +          end;
  1.2293 +
  1.2294 +        val coind_wit_thms = maps mk_coind_wit_thms coind_witss;
  1.2295 +
  1.2296 +        val (wit_thmss, all_witss) =
  1.2297 +          fold (fn ((i, wit), thms) => fn witss =>
  1.2298 +            nth_map i (fn (thms', wits) => (thms @ thms', wit :: wits)) witss)
  1.2299 +          coind_wit_thms (map (pair []) ctor_witss)
  1.2300 +          |> map (apsnd (map snd o minimize_wits))
  1.2301 +          |> split_list;
  1.2302 +
  1.2303 +        val (Jbnf_consts, lthy) =
  1.2304 +          fold_map8 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn wits =>
  1.2305 +              fn T => fn lthy =>
  1.2306 +            define_bnf_consts Dont_Inline (user_policy Note_Some lthy) (SOME deads)
  1.2307 +              map_b rel_b set_bs
  1.2308 +              ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), wits), NONE) lthy)
  1.2309 +          bs map_bs rel_bs set_bss fs_maps setss_by_bnf all_witss Ts lthy;
  1.2310 +
  1.2311 +        val (_, Jconsts, Jconst_defs, mk_Jconsts) = split_list4 Jbnf_consts;
  1.2312 +        val (_, Jsetss, Jbds_Ds, Jwitss_Ds, _) = split_list5 Jconsts;
  1.2313 +        val (Jmap_defs, Jset_defss, Jbd_defs, Jwit_defss, Jrel_defs) = split_list5 Jconst_defs;
  1.2314 +        val (mk_Jmaps_Ds, mk_Jt_Ds, _, mk_Jrels_Ds, _) = split_list5 mk_Jconsts;
  1.2315 +
  1.2316 +        val Jrel_unabs_defs = map (fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) Jrel_defs;
  1.2317 +        val Jset_defs = flat Jset_defss;
  1.2318 +        val Jset_unabs_defs = map (fn def => def RS meta_eq_to_obj_eq RS fun_cong) Jset_defs;
  1.2319 +
  1.2320 +        fun mk_Jmaps As Bs = map (fn mk => mk deads As Bs) mk_Jmaps_Ds;
  1.2321 +        fun mk_Jsetss As = map2 (fn mk => fn Jsets => map (mk deads As) Jsets) mk_Jt_Ds Jsetss;
  1.2322 +        val Jbds = map2 (fn mk => mk deads passiveAs) mk_Jt_Ds Jbds_Ds;
  1.2323 +        val Jwitss =
  1.2324 +          map2 (fn mk => fn Jwits => map (mk deads passiveAs o snd) Jwits) mk_Jt_Ds Jwitss_Ds;
  1.2325 +        fun mk_Jrels As Bs = map (fn mk => mk deads As Bs) mk_Jrels_Ds;
  1.2326 +
  1.2327 +        val Jmaps = mk_Jmaps passiveAs passiveBs;
  1.2328 +        val fs_Jmaps = map (fn m => Term.list_comb (m, fs)) Jmaps;
  1.2329 +        val fs_copy_Jmaps = map (fn m => Term.list_comb (m, fs_copy)) Jmaps;
  1.2330 +        val gs_Jmaps = map (fn m => Term.list_comb (m, gs)) (mk_Jmaps passiveBs passiveCs);
  1.2331 +        val fgs_Jmaps = map (fn m => Term.list_comb (m, map2 (curry HOLogic.mk_comp) gs fs))
  1.2332 +          (mk_Jmaps passiveAs passiveCs);
  1.2333 +        val (Jsetss_by_range, Jsetss_by_bnf) = `transpose (mk_Jsetss passiveAs);
  1.2334 +
  1.2335 +        val timer = time (timer "bnf constants for the new datatypes");
  1.2336 +
  1.2337 +        val (dtor_Jmap_thms, Jmap_thms) =
  1.2338 +          let
  1.2339 +            fun mk_goal fs_Jmap map dtor dtor' = fold_rev Logic.all fs
  1.2340 +              (mk_Trueprop_eq (HOLogic.mk_comp (dtor', fs_Jmap),
  1.2341 +                HOLogic.mk_comp (Term.list_comb (map, fs @ fs_Jmaps), dtor)));
  1.2342 +            val goals = map4 mk_goal fs_Jmaps map_FTFT's dtors dtor's;
  1.2343 +            val cTs = map (SOME o certifyT lthy) FTs';
  1.2344 +            val maps =
  1.2345 +              map5 (fn goal => fn cT => fn unfold => fn map_comp => fn map_cong0 =>
  1.2346 +                Goal.prove_sorry lthy [] [] goal
  1.2347 +                  (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN
  1.2348 +                     mk_map_tac m n cT unfold map_comp map_cong0)
  1.2349 +                |> Thm.close_derivation)
  1.2350 +              goals cTs dtor_unfold_thms map_comps map_cong0s;
  1.2351 +          in
  1.2352 +            map_split (fn thm => (thm RS @{thm comp_eq_dest}, thm)) maps
  1.2353 +          end;
  1.2354 +
  1.2355 +        val dtor_Jmap_unique_thm =
  1.2356 +          let
  1.2357 +            fun mk_prem u map dtor dtor' =
  1.2358 +              mk_Trueprop_eq (HOLogic.mk_comp (dtor', u),
  1.2359 +                HOLogic.mk_comp (Term.list_comb (map, fs @ us), dtor));
  1.2360 +            val prems = map4 mk_prem us map_FTFT's dtors dtor's;
  1.2361 +            val goal =
  1.2362 +              HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  1.2363 +                (map2 (curry HOLogic.mk_eq) us fs_Jmaps));
  1.2364 +          in
  1.2365 +            Goal.prove_sorry lthy [] []
  1.2366 +              (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
  1.2367 +                (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN
  1.2368 +                  mk_dtor_map_unique_tac dtor_unfold_unique_thm sym_map_comps ctxt)
  1.2369 +              |> Thm.close_derivation
  1.2370 +          end;
  1.2371 +
  1.2372 +        val Jmap_comp0_thms =
  1.2373 +          let
  1.2374 +            val goal = fold_rev Logic.all (fs @ gs)
  1.2375 +              (HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  1.2376 +                (map3 (fn fmap => fn gmap => fn fgmap =>
  1.2377 +                   HOLogic.mk_eq (HOLogic.mk_comp (gmap, fmap), fgmap))
  1.2378 +                fs_Jmaps gs_Jmaps fgs_Jmaps)))
  1.2379 +          in
  1.2380 +            split_conj_thm (Goal.prove_sorry lthy [] [] goal
  1.2381 +              (K (mk_map_comp0_tac Jmap_thms map_comp0s dtor_Jmap_unique_thm))
  1.2382 +              |> Thm.close_derivation)
  1.2383 +          end;
  1.2384 +
  1.2385 +        val timer = time (timer "map functions for the new codatatypes");
  1.2386 +
  1.2387 +        val (dtor_Jset_thmss', dtor_Jset_thmss) =
  1.2388 +          let
  1.2389 +            fun mk_simp_goal relate pas_set act_sets sets dtor z set =
  1.2390 +              relate (set $ z, mk_union (pas_set $ (dtor $ z),
  1.2391 +                 Library.foldl1 mk_union
  1.2392 +                   (map2 (fn X => mk_UNION (X $ (dtor $ z))) act_sets sets)));
  1.2393 +            fun mk_goals eq =
  1.2394 +              map2 (fn i => fn sets =>
  1.2395 +                map4 (fn Fsets =>
  1.2396 +                  mk_simp_goal eq (nth Fsets (i - 1)) (drop m Fsets) sets)
  1.2397 +                FTs_setss dtors Jzs sets)
  1.2398 +              ls Jsetss_by_range;
  1.2399 +
  1.2400 +            val le_goals = map
  1.2401 +              (fold_rev Logic.all Jzs o HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj)
  1.2402 +              (mk_goals (uncurry mk_leq));
  1.2403 +            val set_le_thmss = map split_conj_thm
  1.2404 +              (map4 (fn goal => fn hset_minimal => fn set_hsets => fn set_hset_hsetss =>
  1.2405 +                Goal.prove_sorry lthy [] [] goal
  1.2406 +                  (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
  1.2407 +                    mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss)
  1.2408 +                |> Thm.close_derivation)
  1.2409 +              le_goals hset_minimal_thms set_hset_thmss' set_hset_hset_thmsss');
  1.2410 +
  1.2411 +            val ge_goalss = map (map2 (fn z => fn goal =>
  1.2412 +                Logic.all z (HOLogic.mk_Trueprop goal)) Jzs)
  1.2413 +              (mk_goals (uncurry mk_leq o swap));
  1.2414 +            val set_ge_thmss = 
  1.2415 +              map3 (map3 (fn goal => fn set_incl_hset => fn set_hset_incl_hsets =>
  1.2416 +                Goal.prove_sorry lthy [] [] goal
  1.2417 +                  (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
  1.2418 +                    mk_set_ge_tac n set_incl_hset set_hset_incl_hsets)
  1.2419 +                |> Thm.close_derivation))
  1.2420 +              ge_goalss set_incl_hset_thmss' set_hset_incl_hset_thmsss'
  1.2421 +          in
  1.2422 +            map2 (map2 (fn le => fn ge => equalityI OF [le, ge])) set_le_thmss set_ge_thmss
  1.2423 +            |> `transpose
  1.2424 +          end;
  1.2425 +
  1.2426 +        val timer = time (timer "set functions for the new codatatypes");
  1.2427 +
  1.2428 +        val colss = map2 (fn j => fn T =>
  1.2429 +          map (fn i => mk_hset_rec dtors nat i j T) ks) ls passiveAs;
  1.2430 +        val colss' = map2 (fn j => fn T =>
  1.2431 +          map (fn i => mk_hset_rec dtor's nat i j T) ks) ls passiveBs;
  1.2432 +
  1.2433 +        val col_natural_thmss =
  1.2434 +          let
  1.2435 +            fun mk_col_natural f map z col col' =
  1.2436 +              HOLogic.mk_eq (mk_image f $ (col $ z), col' $ (map $ z));
  1.2437 +
  1.2438 +            fun mk_goal f cols cols' = list_all_free Jzs (Library.foldr1 HOLogic.mk_conj
  1.2439 +              (map4 (mk_col_natural f) fs_Jmaps Jzs cols cols'));
  1.2440 +
  1.2441 +            val goals = map3 mk_goal fs colss colss';
  1.2442 +
  1.2443 +            val ctss =
  1.2444 +              map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) goals;
  1.2445 +
  1.2446 +            val thms =
  1.2447 +              map4 (fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
  1.2448 +                singleton (Proof_Context.export names_lthy lthy)
  1.2449 +                  (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
  1.2450 +                    (mk_col_natural_tac cts rec_0s rec_Sucs dtor_Jmap_thms set_mapss))
  1.2451 +                |> Thm.close_derivation)
  1.2452 +              goals ctss hset_rec_0ss' hset_rec_Sucss';
  1.2453 +          in
  1.2454 +            map (split_conj_thm o mk_specN n) thms
  1.2455 +          end;
  1.2456 +
  1.2457 +        val col_bd_thmss =
  1.2458 +          let
  1.2459 +            fun mk_col_bd z col bd = mk_ordLeq (mk_card_of (col $ z)) bd;
  1.2460 +
  1.2461 +            fun mk_goal bds cols = list_all_free Jzs (Library.foldr1 HOLogic.mk_conj
  1.2462 +              (map3 mk_col_bd Jzs cols bds));
  1.2463 +
  1.2464 +            val goals = map (mk_goal Jbds) colss;
  1.2465 +
  1.2466 +            val ctss = map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat])
  1.2467 +              (map (mk_goal (replicate n sbd)) colss);
  1.2468 +
  1.2469 +            val thms =
  1.2470 +              map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
  1.2471 +                singleton (Proof_Context.export names_lthy lthy)
  1.2472 +                  (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
  1.2473 +                    (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jbd_defs THEN
  1.2474 +                      mk_col_bd_tac m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss))
  1.2475 +                |> Thm.close_derivation)
  1.2476 +              ls goals ctss hset_rec_0ss' hset_rec_Sucss';
  1.2477 +          in
  1.2478 +            map (split_conj_thm o mk_specN n) thms
  1.2479 +          end;
  1.2480 +
  1.2481 +        val map_cong0_thms =
  1.2482 +          let
  1.2483 +            val cTs = map (SOME o certifyT lthy o
  1.2484 +              Term.typ_subst_atomic (passiveAs ~~ passiveBs) o TFree) coinduct_params;
  1.2485 +
  1.2486 +            fun mk_prem z set f g y y' =
  1.2487 +              mk_Ball (set $ z) (Term.absfree y' (HOLogic.mk_eq (f $ y, g $ y)));
  1.2488 +
  1.2489 +            fun mk_prems sets z =
  1.2490 +              Library.foldr1 HOLogic.mk_conj (map5 (mk_prem z) sets fs fs_copy ys ys')
  1.2491 +
  1.2492 +            fun mk_map_cong0 sets z fmap gmap =
  1.2493 +              HOLogic.mk_imp (mk_prems sets z, HOLogic.mk_eq (fmap $ z, gmap $ z));
  1.2494 +
  1.2495 +            fun mk_coind_body sets (x, T) z fmap gmap y y_copy =
  1.2496 +              HOLogic.mk_conj
  1.2497 +                (HOLogic.mk_mem (z, HOLogic.mk_Collect (x, T, mk_prems sets z)),
  1.2498 +                  HOLogic.mk_conj (HOLogic.mk_eq (y, fmap $ z),
  1.2499 +                    HOLogic.mk_eq (y_copy, gmap $ z)))
  1.2500 +
  1.2501 +            fun mk_cphi sets (z' as (x, T)) z fmap gmap y' y y'_copy y_copy =
  1.2502 +              HOLogic.mk_exists (x, T, mk_coind_body sets z' z fmap gmap y y_copy)
  1.2503 +              |> Term.absfree y'_copy
  1.2504 +              |> Term.absfree y'
  1.2505 +              |> certify lthy;
  1.2506 +
  1.2507 +            val cphis = map9 mk_cphi
  1.2508 +              Jsetss_by_bnf Jzs' Jzs fs_Jmaps fs_copy_Jmaps Jys' Jys Jys'_copy Jys_copy;
  1.2509 +
  1.2510 +            val coinduct = unfold_thms lthy Jset_defs
  1.2511 +              (Drule.instantiate' cTs (map SOME cphis) dtor_map_coinduct_thm);
  1.2512 +
  1.2513 +            val goal =
  1.2514 +              HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  1.2515 +                (map4 mk_map_cong0 Jsetss_by_bnf Jzs fs_Jmaps fs_copy_Jmaps));
  1.2516 +
  1.2517 +            val thm = singleton (Proof_Context.export names_lthy lthy)
  1.2518 +              (Goal.prove_sorry lthy [] [] goal
  1.2519 +                (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
  1.2520 +                  mk_mcong_tac lthy m (rtac coinduct) map_comps dtor_Jmap_thms map_cong0s
  1.2521 +                    set_mapss set_hset_thmss set_hset_hset_thmsss))
  1.2522 +              |> Thm.close_derivation
  1.2523 +          in
  1.2524 +            split_conj_thm thm
  1.2525 +          end;
  1.2526 +
  1.2527 +        val in_Jrels = map (fn def => trans OF [def, @{thm OO_Grp_alt}] RS @{thm predicate2_eqD})
  1.2528 +            Jrel_unabs_defs;
  1.2529 +
  1.2530 +        val fold_Jsets = fold_thms lthy Jset_unabs_defs;
  1.2531 +        val dtor_Jset_incl_thmss = map (map fold_Jsets) hset_dtor_incl_thmss;
  1.2532 +        val dtor_set_Jset_incl_thmsss = map (map (map fold_Jsets)) hset_hset_dtor_incl_thmsss;
  1.2533 +        val dtor_Jset_induct_thms = map fold_Jsets dtor_hset_induct_thms;
  1.2534 +        val Jwit_thmss = map (map fold_Jsets) wit_thmss;
  1.2535 +
  1.2536 +        val Jrels = mk_Jrels passiveAs passiveBs;
  1.2537 +        val Jrelphis = map (fn rel => Term.list_comb (rel, Jphis)) Jrels;
  1.2538 +        val relphis = map (fn rel => Term.list_comb (rel, Jphis @ Jrelphis)) rels;
  1.2539 +        val Jrelpsi1s = map (fn rel => Term.list_comb (rel, Jpsi1s)) (mk_Jrels passiveAs passiveCs);
  1.2540 +        val Jrelpsi2s = map (fn rel => Term.list_comb (rel, Jpsi2s)) (mk_Jrels passiveCs passiveBs);
  1.2541 +        val Jrelpsi12s = map (fn rel =>
  1.2542 +            Term.list_comb (rel, map2 (curry mk_rel_compp) Jpsi1s Jpsi2s)) Jrels;
  1.2543 +
  1.2544 +        val dtor_Jrel_thms =
  1.2545 +          let
  1.2546 +            fun mk_goal Jz Jz' dtor dtor' Jrelphi relphi = fold_rev Logic.all (Jz :: Jz' :: Jphis)
  1.2547 +              (mk_Trueprop_eq (Jrelphi $ Jz $ Jz', relphi $ (dtor $ Jz) $ (dtor' $ Jz')));
  1.2548 +            val goals = map6 mk_goal Jzs Jz's dtors dtor's Jrelphis relphis;
  1.2549 +          in
  1.2550 +            map12 (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 =>
  1.2551 +              fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor =>
  1.2552 +              fn set_map0s => fn dtor_set_incls => fn dtor_set_set_inclss =>
  1.2553 +              Goal.prove_sorry lthy [] [] goal
  1.2554 +                (K (mk_dtor_rel_tac lthy in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets
  1.2555 +                  dtor_inject dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss))
  1.2556 +              |> Thm.close_derivation)
  1.2557 +            ks goals in_rels map_comps map_cong0s dtor_Jmap_thms dtor_Jset_thmss'
  1.2558 +              dtor_inject_thms dtor_ctor_thms set_mapss dtor_Jset_incl_thmss
  1.2559 +              dtor_set_Jset_incl_thmsss
  1.2560 +          end;
  1.2561 +
  1.2562 +      val passiveABs = map2 (curry HOLogic.mk_prodT) passiveAs passiveBs;
  1.2563 +      val zip_ranTs = passiveABs @ prodTsTs';
  1.2564 +      val allJphis = Jphis @ activeJphis;
  1.2565 +      val zipFTs = mk_FTs zip_ranTs;
  1.2566 +      val zipTs = map3 (fn T => fn T' => fn FT => T --> T' --> FT) Ts Ts' zipFTs;
  1.2567 +      val zip_zTs = mk_Ts passiveABs;
  1.2568 +      val (((zips, (abs, abs')), zip_zs), names_lthy) = names_lthy
  1.2569 +        |> mk_Frees "zip" zipTs
  1.2570 +        ||>> mk_Frees' "ab" passiveABs
  1.2571 +        ||>> mk_Frees "z" zip_zTs;
  1.2572 +
  1.2573 +      val Iphi_sets =
  1.2574 +        map2 (fn phi => fn T => HOLogic.Collect_const T $ HOLogic.mk_split phi) allJphis zip_ranTs;
  1.2575 +      val in_phis = map2 (mk_in Iphi_sets) (mk_setss zip_ranTs) zipFTs;
  1.2576 +      val fstABs = map fst_const passiveABs;
  1.2577 +      val all_fsts = fstABs @ fstsTsTs';
  1.2578 +      val map_all_fsts = map2 (fn Ds => fn bnf =>
  1.2579 +        Term.list_comb (mk_map_of_bnf Ds zip_ranTs (passiveAs @ Ts) bnf, all_fsts)) Dss bnfs;
  1.2580 +      val Jmap_fsts = map2 (fn map => fn T => if m = 0 then HOLogic.id_const T
  1.2581 +        else Term.list_comb (map, fstABs)) (mk_Jmaps passiveABs passiveAs) Ts;
  1.2582 +
  1.2583 +      val sndABs = map snd_const passiveABs;
  1.2584 +      val all_snds = sndABs @ sndsTsTs';
  1.2585 +      val map_all_snds = map2 (fn Ds => fn bnf =>
  1.2586 +        Term.list_comb (mk_map_of_bnf Ds zip_ranTs (passiveBs @ Ts') bnf, all_snds)) Dss bnfs;
  1.2587 +      val Jmap_snds = map2 (fn map => fn T => if m = 0 then HOLogic.id_const T
  1.2588 +        else Term.list_comb (map, sndABs)) (mk_Jmaps passiveABs passiveBs) Ts;
  1.2589 +      val zip_unfolds = map (mk_unfold zip_zTs (map HOLogic.mk_split zips)) ks;
  1.2590 +      val zip_setss = mk_Jsetss passiveABs |> transpose;
  1.2591 +
  1.2592 +      val Jrel_coinduct_tac =
  1.2593 +        let
  1.2594 +          fun mk_helper_prem phi in_phi zip x y map map' dtor dtor' =
  1.2595 +            let
  1.2596 +              val zipxy = zip $ x $ y;
  1.2597 +            in
  1.2598 +              HOLogic.mk_Trueprop (list_all_free [x, y]
  1.2599 +                (HOLogic.mk_imp (phi $ x $ y, HOLogic.mk_conj (HOLogic.mk_mem (zipxy, in_phi),
  1.2600 +                  HOLogic.mk_conj (HOLogic.mk_eq (map $ zipxy, dtor $ x),
  1.2601 +                    HOLogic.mk_eq (map' $ zipxy, dtor' $ y))))))
  1.2602 +            end;
  1.2603 +          val helper_prems = map9 mk_helper_prem
  1.2604 +            activeJphis in_phis zips Jzs Jz's map_all_fsts map_all_snds dtors dtor's;
  1.2605 +          fun mk_helper_coind_concl fst phi x alt y map zip_unfold =
  1.2606 +            HOLogic.mk_imp (list_exists_free [if fst then y else x] (HOLogic.mk_conj (phi $ x $ y,
  1.2607 +              HOLogic.mk_eq (alt, map $ (zip_unfold $ HOLogic.mk_prod (x, y))))),
  1.2608 +            HOLogic.mk_eq (alt, if fst then x else y));
  1.2609 +          val helper_coind1_concl =
  1.2610 +            HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  1.2611 +              (map6 (mk_helper_coind_concl true)
  1.2612 +              activeJphis Jzs Jzs_copy Jz's Jmap_fsts zip_unfolds));
  1.2613 +          val helper_coind2_concl =
  1.2614 +            HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  1.2615 +              (map6 (mk_helper_coind_concl false)
  1.2616 +              activeJphis Jzs Jz's_copy Jz's Jmap_snds zip_unfolds));
  1.2617 +          val helper_coind_tac = mk_rel_coinduct_coind_tac m dtor_map_coinduct_thm ks map_comps
  1.2618 +            map_cong0s map_arg_cong_thms set_mapss dtor_unfold_thms dtor_Jmap_thms;
  1.2619 +          fun mk_helper_coind_thms vars concl =
  1.2620 +            Goal.prove_sorry lthy [] []
  1.2621 +              (fold_rev Logic.all (Jphis @ activeJphis @ vars @ zips)
  1.2622 +                (Logic.list_implies (helper_prems, concl)))
  1.2623 +              helper_coind_tac
  1.2624 +            |> Thm.close_derivation
  1.2625 +            |> split_conj_thm;
  1.2626 +          val helper_coind1_thms = mk_helper_coind_thms (Jzs @ Jzs_copy) helper_coind1_concl;
  1.2627 +          val helper_coind2_thms = mk_helper_coind_thms (Jz's @ Jz's_copy) helper_coind2_concl;
  1.2628 +  
  1.2629 +          fun mk_helper_ind_concl phi ab' ab fst snd z active_phi x y zip_unfold set =
  1.2630 +            mk_Ball (set $ z) (Term.absfree ab' (list_all_free [x, y] (HOLogic.mk_imp
  1.2631 +              (HOLogic.mk_conj (active_phi $ x $ y,
  1.2632 +                 HOLogic.mk_eq (z, zip_unfold $ HOLogic.mk_prod (x, y))),
  1.2633 +              phi $ (fst $ ab) $ (snd $ ab)))));
  1.2634 +  
  1.2635 +          val mk_helper_ind_concls =
  1.2636 +            map6 (fn Jphi => fn ab' => fn ab => fn fst => fn snd => fn zip_sets =>
  1.2637 +              map6 (mk_helper_ind_concl Jphi ab' ab fst snd)
  1.2638 +              zip_zs activeJphis Jzs Jz's zip_unfolds zip_sets)
  1.2639 +            Jphis abs' abs fstABs sndABs zip_setss
  1.2640 +            |> map (HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj);
  1.2641 +  
  1.2642 +          val helper_ind_thmss = if m = 0 then replicate n [] else
  1.2643 +            map3 (fn concl => fn j => fn set_induct =>
  1.2644 +              Goal.prove_sorry lthy [] []
  1.2645 +                (fold_rev Logic.all (Jphis @ activeJphis @ zip_zs @ zips)
  1.2646 +                  (Logic.list_implies (helper_prems, concl)))
  1.2647 +                (mk_rel_coinduct_ind_tac m ks dtor_unfold_thms set_mapss j set_induct)
  1.2648 +              |> Thm.close_derivation
  1.2649 +              |> split_conj_thm)
  1.2650 +            mk_helper_ind_concls ls dtor_Jset_induct_thms
  1.2651 +            |> transpose;
  1.2652 +        in
  1.2653 +          mk_rel_coinduct_tac in_rels in_Jrels
  1.2654 +            helper_ind_thmss helper_coind1_thms helper_coind2_thms
  1.2655 +        end;
  1.2656 +
  1.2657 +      val Jrel_coinduct_thm =
  1.2658 +        mk_rel_xtor_co_induct_thm Greatest_FP rels activeJphis Jrels Jphis Jzs Jz's dtors dtor's
  1.2659 +          Jrel_coinduct_tac lthy;
  1.2660 +
  1.2661 +        val le_Jrel_OO_thm =
  1.2662 +          let
  1.2663 +            fun mk_le_Jrel_OO Jrelpsi1 Jrelpsi2 Jrelpsi12 =
  1.2664 +              mk_leq (mk_rel_compp (Jrelpsi1, Jrelpsi2)) Jrelpsi12;
  1.2665 +            val goals = map3 mk_le_Jrel_OO Jrelpsi1s Jrelpsi2s Jrelpsi12s;
  1.2666 +
  1.2667 +            val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals);
  1.2668 +          in
  1.2669 +            singleton (Proof_Context.export names_lthy lthy)
  1.2670 +              (Goal.prove_sorry lthy [] [] goal
  1.2671 +                (K (mk_le_rel_OO_tac Jrel_coinduct_thm dtor_Jrel_thms rel_OOs)))
  1.2672 +              |> Thm.close_derivation
  1.2673 +          end;
  1.2674 +
  1.2675 +        val timer = time (timer "helpers for BNF properties");
  1.2676 +
  1.2677 +        val map_id0_tacs =
  1.2678 +          map2 (K oo mk_map_id0_tac Jmap_thms) dtor_unfold_unique_thms unfold_dtor_thms;
  1.2679 +        val map_comp0_tacs = map (fn thm => K (rtac (thm RS sym) 1)) Jmap_comp0_thms;
  1.2680 +        val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
  1.2681 +        val set_nat_tacss =
  1.2682 +          map2 (map2 (fn def => fn col => fn {context = ctxt, prems = _} =>
  1.2683 +              unfold_thms_tac ctxt Jset_defs THEN mk_set_map0_tac def col))
  1.2684 +            hset_defss (transpose col_natural_thmss);
  1.2685 +
  1.2686 +        val Jbd_card_orders = map (fn def => fold_thms lthy [def] sbd_card_order) Jbd_defs;
  1.2687 +        val Jbd_Cinfinites = map (fn def => fold_thms lthy [def] sbd_Cinfinite) Jbd_defs;
  1.2688 +
  1.2689 +        val bd_co_tacs = map (fn thm => K (rtac thm 1)) Jbd_card_orders;
  1.2690 +        val bd_cinf_tacs = map (fn thm => K (rtac (thm RS conjunct1) 1)) Jbd_Cinfinites;
  1.2691 +
  1.2692 +        val set_bd_tacss =
  1.2693 +          map3 (fn Cinf => map2 (fn def => fn col => fn {context = ctxt, prems = _} =>
  1.2694 +            unfold_thms_tac ctxt Jset_defs THEN mk_set_bd_tac Cinf def col))
  1.2695 +          Jbd_Cinfinites hset_defss (transpose col_bd_thmss);
  1.2696 +
  1.2697 +        val le_rel_OO_tacs = map (fn i => K (rtac (le_Jrel_OO_thm RS mk_conjunctN n i) 1)) ks;
  1.2698 +
  1.2699 +        val rel_OO_Grp_tacs = map (fn def => K (rtac def 1)) Jrel_unabs_defs;
  1.2700 +
  1.2701 +        val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_nat_tacss
  1.2702 +          bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs;
  1.2703 +
  1.2704 +        fun wit_tac thms {context = ctxt, prems = _} = unfold_thms_tac ctxt (flat Jwit_defss) THEN
  1.2705 +          mk_wit_tac n dtor_ctor_thms (flat dtor_Jset_thmss) (maps wit_thms_of_bnf bnfs) thms ctxt;
  1.2706 +
  1.2707 +        val (Jbnfs, lthy) =
  1.2708 +          fold_map6 (fn tacs => fn map_b => fn rel_b => fn set_bs => fn Jwit_thms => fn consts =>
  1.2709 +              fn lthy =>
  1.2710 +            bnf_def Do_Inline (user_policy Note_Some) I tacs (wit_tac Jwit_thms) (SOME deads)
  1.2711 +              map_b rel_b set_bs consts lthy
  1.2712 +            |> register_bnf (Local_Theory.full_name lthy b))
  1.2713 +          tacss map_bs rel_bs set_bss Jwit_thmss
  1.2714 +          ((((((bs ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~ Jwitss) ~~ map SOME Jrels)
  1.2715 +          lthy;
  1.2716 +
  1.2717 +        val timer = time (timer "registered new codatatypes as BNFs");
  1.2718 +
  1.2719 +        val ls' = if m = 1 then [0] else ls;
  1.2720 +
  1.2721 +        val Jbnf_common_notes =
  1.2722 +          [(dtor_map_uniqueN, [dtor_Jmap_unique_thm])] @
  1.2723 +          map2 (fn i => fn thm => (mk_dtor_set_inductN i, [thm])) ls' dtor_Jset_induct_thms
  1.2724 +          |> map (fn (thmN, thms) =>
  1.2725 +            ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
  1.2726 +
  1.2727 +        val Jbnf_notes =
  1.2728 +          [(dtor_mapN, map single dtor_Jmap_thms),
  1.2729 +          (dtor_relN, map single dtor_Jrel_thms),
  1.2730 +          (dtor_set_inclN, dtor_Jset_incl_thmss),
  1.2731 +          (dtor_set_set_inclN, map flat dtor_set_Jset_incl_thmsss)] @
  1.2732 +          map2 (fn i => fn thms => (mk_dtor_setN i, map single thms)) ls' dtor_Jset_thmss
  1.2733 +          |> maps (fn (thmN, thmss) =>
  1.2734 +            map2 (fn b => fn thms =>
  1.2735 +              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
  1.2736 +            bs thmss)
  1.2737 +      in
  1.2738 +        (timer, Jbnfs, (Jmap_thms, dtor_Jmap_thms), dtor_Jset_thmss',
  1.2739 +          dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_common_notes @ Jbnf_notes, lthy)
  1.2740 +      end;
  1.2741 +
  1.2742 +      val dtor_unfold_o_Jmap_thms = mk_xtor_un_fold_o_map_thms Greatest_FP false m
  1.2743 +        dtor_unfold_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_unfold_thms)
  1.2744 +        sym_map_comps map_cong0s;
  1.2745 +      val dtor_corec_o_Jmap_thms = mk_xtor_un_fold_o_map_thms Greatest_FP true m
  1.2746 +        dtor_corec_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_corec_thms)
  1.2747 +        sym_map_comps map_cong0s;
  1.2748 +
  1.2749 +      val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
  1.2750 +
  1.2751 +      val dtor_unfold_transfer_thms =
  1.2752 +        mk_un_fold_transfer_thms Greatest_FP rels activephis
  1.2753 +          (if m = 0 then map HOLogic.eq_const Ts
  1.2754 +            else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs) Jphis
  1.2755 +          (mk_unfolds passiveAs activeAs) (mk_unfolds passiveBs activeBs)
  1.2756 +          (mk_unfold_transfer_tac m Jrel_coinduct_thm (map map_transfer_of_bnf bnfs)
  1.2757 +            dtor_unfold_thms)
  1.2758 +          lthy;
  1.2759 +
  1.2760 +      val timer = time (timer "relator coinduction");
  1.2761 +
  1.2762 +      val common_notes =
  1.2763 +        [(dtor_coinductN, [dtor_coinduct_thm]),
  1.2764 +        (dtor_map_coinductN, [dtor_map_coinduct_thm]),
  1.2765 +        (rel_coinductN, [Jrel_coinduct_thm]),
  1.2766 +        (dtor_unfold_transferN, dtor_unfold_transfer_thms)]
  1.2767 +        |> map (fn (thmN, thms) =>
  1.2768 +          ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
  1.2769 +
  1.2770 +      val notes =
  1.2771 +        [(ctor_dtorN, ctor_dtor_thms),
  1.2772 +        (ctor_exhaustN, ctor_exhaust_thms),
  1.2773 +        (ctor_injectN, ctor_inject_thms),
  1.2774 +        (dtor_corecN, dtor_corec_thms),
  1.2775 +        (dtor_ctorN, dtor_ctor_thms),
  1.2776 +        (dtor_exhaustN, dtor_exhaust_thms),
  1.2777 +        (dtor_injectN, dtor_inject_thms),
  1.2778 +        (dtor_unfoldN, dtor_unfold_thms),
  1.2779 +        (dtor_unfold_uniqueN, dtor_unfold_unique_thms),
  1.2780 +        (dtor_corec_uniqueN, dtor_corec_unique_thms),
  1.2781 +        (dtor_unfold_o_mapN, dtor_unfold_o_Jmap_thms),
  1.2782 +        (dtor_corec_o_mapN, dtor_corec_o_Jmap_thms)]
  1.2783 +        |> map (apsnd (map single))
  1.2784 +        |> maps (fn (thmN, thmss) =>
  1.2785 +          map2 (fn b => fn thms =>
  1.2786 +            ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
  1.2787 +          bs thmss);
  1.2788 +
  1.2789 +    (*FIXME: once the package exports all the necessary high-level characteristic theorems,
  1.2790 +       those should not only be concealed but rather not noted at all*)
  1.2791 +    val maybe_conceal_notes = note_all = false ? map (apfst (apfst Binding.conceal));
  1.2792 +  in
  1.2793 +    timer;
  1.2794 +    ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors,
  1.2795 +      xtor_co_iterss = transpose [unfolds, corecs],
  1.2796 +      xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms,
  1.2797 +      ctor_dtors = ctor_dtor_thms,
  1.2798 +      ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
  1.2799 +      xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss',
  1.2800 +      xtor_rel_thms = dtor_Jrel_thms,
  1.2801 +      xtor_co_iter_thmss = transpose [dtor_unfold_thms, dtor_corec_thms],
  1.2802 +      xtor_co_iter_o_map_thmss = transpose [dtor_unfold_o_Jmap_thms, dtor_corec_o_Jmap_thms],
  1.2803 +      rel_xtor_co_induct_thm = Jrel_coinduct_thm},
  1.2804 +     lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Jbnf_notes)) |> snd)
  1.2805 +  end;
  1.2806 +
  1.2807 +val _ =
  1.2808 +  Outer_Syntax.local_theory @{command_spec "codatatype"} "define coinductive datatypes"
  1.2809 +    (parse_co_datatype_cmd Greatest_FP construct_gfp);
  1.2810 +
  1.2811 +val option_parser = Parse.group (fn () => "option")
  1.2812 +  ((Parse.reserved "sequential" >> K Sequential_Option)
  1.2813 +  || (Parse.reserved "exhaustive" >> K Exhaustive_Option))
  1.2814 +
  1.2815 +val where_alt_specs_of_parser = Parse.where_ |-- Parse.!!! (Parse.enum1 "|"
  1.2816 +  (Parse_Spec.spec -- Scan.option (Parse.reserved "of" |-- Parse.const)));
  1.2817 +
  1.2818 +val _ = Outer_Syntax.local_theory_to_proof @{command_spec "primcorecursive"}
  1.2819 +  "define primitive corecursive functions"
  1.2820 +  ((Scan.optional (@{keyword "("} |--
  1.2821 +      Parse.!!! (Parse.list1 option_parser) --| @{keyword ")"}) []) --
  1.2822 +    (Parse.fixes -- where_alt_specs_of_parser) >> uncurry add_primcorecursive_cmd);
  1.2823 +
  1.2824 +val _ = Outer_Syntax.local_theory @{command_spec "primcorec"}
  1.2825 +  "define primitive corecursive functions"
  1.2826 +  ((Scan.optional (@{keyword "("} |--
  1.2827 +      Parse.!!! (Parse.list1 option_parser) --| @{keyword ")"}) []) --
  1.2828 +    (Parse.fixes -- where_alt_specs_of_parser) >> uncurry add_primcorec_cmd);
  1.2829 +
  1.2830 +end;