src/HOL/Tools/BNF/bnf_lfp.ML
author traytel
Thu Apr 07 17:56:22 2016 +0200 (2016-04-07)
changeset 62905 52c5a25e0c96
parent 62863 e0b894bba6ff
child 62907 9ad0bac25a84
permissions -rw-r--r--
derive (co)rec uniformly from (un)fold
     1 (*  Title:      HOL/Tools/BNF/bnf_lfp.ML
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Author:     Andrei Popescu, TU Muenchen
     4     Copyright   2012
     5 
     6 Datatype construction.
     7 *)
     8 
     9 signature BNF_LFP =
    10 sig
    11   val construct_lfp: mixfix list -> binding list -> binding list -> binding list ->
    12     binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
    13     BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
    14     BNF_FP_Util.fp_result * local_theory
    15 end;
    16 
    17 structure BNF_LFP : BNF_LFP =
    18 struct
    19 
    20 open BNF_Def
    21 open BNF_Util
    22 open BNF_Tactics
    23 open BNF_Comp
    24 open BNF_FP_Util
    25 open BNF_FP_Def_Sugar
    26 open BNF_LFP_Util
    27 open BNF_LFP_Tactics
    28 
    29 (*all BNFs have the same lives*)
    30 fun construct_lfp mixfixes map_bs rel_bs pred_bs set_bss0 bs resBs (resDs, Dss) bnfs absT_infos
    31     lthy =
    32   let
    33     val time = time lthy;
    34     val timer = time (Timer.startRealTimer ());
    35 
    36     val live = live_of_bnf (hd bnfs);
    37     val n = length bnfs; (*active*)
    38     val ks = 1 upto n;
    39     val m = live - n; (*passive, if 0 don't generate a new BNF*)
    40 
    41     val internals = Config.get lthy bnf_internals;
    42     val b_names = map Binding.name_of bs;
    43     val b_name = mk_common_name b_names;
    44     val b = Binding.name b_name;
    45 
    46     fun mk_internal_of_b name =
    47       Binding.prefix_name (name ^ "_") #> Binding.prefix true b_name #> Binding.concealed;
    48     fun mk_internal_b name = mk_internal_of_b name b;
    49     fun mk_internal_bs name = map (mk_internal_of_b name) bs;
    50     val external_bs = map2 (Binding.prefix false) b_names bs
    51       |> not internals ? map Binding.concealed;
    52 
    53     val deads = fold (union (op =)) Dss resDs;
    54     val names_lthy = fold Variable.declare_typ deads lthy;
    55     val passives = map fst (subtract (op = o apsnd TFree) deads resBs);
    56 
    57     (* tvars *)
    58     val (((((passiveAs, activeAs), passiveBs), activeBs), passiveCs), activeCs) =
    59       names_lthy
    60       |> variant_tfrees passives
    61       ||>> mk_TFrees n
    62       ||>> variant_tfrees passives
    63       ||>> mk_TFrees n
    64       ||>> variant_tfrees passives
    65       ||>> mk_TFrees n
    66       |> fst;
    67 
    68     val allAs = passiveAs @ activeAs;
    69     val allBs' = passiveBs @ activeBs;
    70     val Ass = replicate n allAs;
    71     val allBs = passiveAs @ activeBs;
    72     val Bss = replicate n allBs;
    73     val allCs = passiveAs @ activeCs;
    74     val allCs' = passiveBs @ activeCs;
    75     val Css' = replicate n allCs';
    76 
    77     (* types *)
    78     val dead_poss =
    79       map (fn x => if member (op =) deads (TFree x) then SOME (TFree x) else NONE) resBs;
    80     fun mk_param NONE passive = (hd passive, tl passive)
    81       | mk_param (SOME a) passive = (a, passive);
    82     val mk_params = fold_map mk_param dead_poss #> fst;
    83 
    84     fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs;
    85     val (params, params') = `(map Term.dest_TFree) (mk_params passiveAs);
    86     val FTsAs = mk_FTs allAs;
    87     val FTsBs = mk_FTs allBs;
    88     val FTsCs = mk_FTs allCs;
    89     val BTs = map HOLogic.mk_setT activeAs;
    90     val B'Ts = map HOLogic.mk_setT activeBs;
    91     val B''Ts = map HOLogic.mk_setT activeCs;
    92     val sTs = map2 (curry op -->) FTsAs activeAs;
    93     val s'Ts = map2 (curry op -->) FTsBs activeBs;
    94     val s''Ts = map2 (curry op -->) FTsCs activeCs;
    95     val fTs = map2 (curry op -->) activeAs activeBs;
    96     val inv_fTs = map2 (curry op -->) activeBs activeAs;
    97     val self_fTs = map2 (curry op -->) activeAs activeAs;
    98     val gTs = map2 (curry op -->) activeBs activeCs;
    99     val all_gTs = map2 (curry op -->) allBs allCs';
   100     val prodBsAs = map2 (curry HOLogic.mk_prodT) activeBs activeAs;
   101     val prodFTs = mk_FTs (passiveAs @ prodBsAs);
   102     val prod_sTs = map2 (curry op -->) prodFTs activeAs;
   103 
   104     (* terms *)
   105     val mapsAsAs = @{map 4} mk_map_of_bnf Dss Ass Ass bnfs;
   106     val mapsAsBs = @{map 4} mk_map_of_bnf Dss Ass Bss bnfs;
   107     val mapsBsCs' = @{map 4} mk_map_of_bnf Dss Bss Css' bnfs;
   108     val mapsAsCs' = @{map 4} mk_map_of_bnf Dss Ass Css' bnfs;
   109     val map_fsts = @{map 4} mk_map_of_bnf Dss (replicate n (passiveAs @ prodBsAs)) Bss bnfs;
   110     val map_fsts_rev = @{map 4} mk_map_of_bnf Dss Bss (replicate n (passiveAs @ prodBsAs)) bnfs;
   111     fun mk_setss Ts = @{map 3} mk_sets_of_bnf (map (replicate live) Dss)
   112       (map (replicate live) (replicate n Ts)) bnfs;
   113     val setssAs = mk_setss allAs;
   114     val bd0s = @{map 3} mk_bd_of_bnf Dss Ass bnfs;
   115     val bds =
   116       @{map 3} (fn bd0 => fn Ds => fn bnf => mk_csum bd0
   117         (mk_card_of (HOLogic.mk_UNIV
   118           (mk_T_of_bnf Ds (replicate live (fst (dest_relT (fastype_of bd0)))) bnf))))
   119       bd0s Dss bnfs;
   120     val witss = map wits_of_bnf bnfs;
   121 
   122     val ((((((((zs, zs'), Bs), ss), fs), self_fs), all_gs), (xFs, xFs')), _) =
   123       lthy
   124       |> mk_Frees' "z" activeAs
   125       ||>> mk_Frees "B" BTs
   126       ||>> mk_Frees "s" sTs
   127       ||>> mk_Frees "f" fTs
   128       ||>> mk_Frees "f" self_fTs
   129       ||>> mk_Frees "g" all_gTs
   130       ||>> mk_Frees' "x" FTsAs;
   131 
   132     val passive_UNIVs = map HOLogic.mk_UNIV passiveAs;
   133     val active_UNIVs = map HOLogic.mk_UNIV activeAs;
   134     val prod_UNIVs = map HOLogic.mk_UNIV prodBsAs;
   135     val passive_ids = map HOLogic.id_const passiveAs;
   136     val active_ids = map HOLogic.id_const activeAs;
   137     val fsts = map fst_const prodBsAs;
   138 
   139     (* thms *)
   140     val bd0_card_orders = map bd_card_order_of_bnf bnfs;
   141     val bd0_Card_orders = map bd_Card_order_of_bnf bnfs;
   142     val bd0_Cinfinites = map bd_Cinfinite_of_bnf bnfs;
   143     val set_bd0ss = map set_bd_of_bnf bnfs;
   144 
   145     val bd_Card_order = @{thm Card_order_csum};
   146     val bd_Card_orders = replicate n bd_Card_order;
   147     val bd_Cinfinites = map (fn thm => thm RS @{thm Cinfinite_csum1}) bd0_Cinfinites;
   148     val bd_Cnotzeros = map (fn thm => thm RS @{thm Cinfinite_Cnotzero}) bd_Cinfinites;
   149     val bd_Cinfinite = hd bd_Cinfinites;
   150     val set_bdss =
   151       map2 (fn set_bd0s => fn bd0_Card_order =>
   152         map (fn thm => ctrans OF [thm, bd0_Card_order RS @{thm ordLeq_csum1}]) set_bd0s)
   153       set_bd0ss bd0_Card_orders;
   154     val in_bds = map in_bd_of_bnf bnfs;
   155     val sym_map_comps = map (fn bnf => map_comp0_of_bnf bnf RS sym) bnfs;
   156     val map_comps = map map_comp_of_bnf bnfs;
   157     val map_cong0s = map map_cong0_of_bnf bnfs;
   158     val map_id0s = map map_id0_of_bnf bnfs;
   159     val map_ids = map map_id_of_bnf bnfs;
   160     val set_mapss = map set_map_of_bnf bnfs;
   161     val rel_mono_strong0s = map rel_mono_strong0_of_bnf bnfs;
   162     val le_rel_OOs = map le_rel_OO_of_bnf bnfs;
   163 
   164     val timer = time (timer "Extracted terms & thms");
   165 
   166     (* nonemptiness check *)
   167     fun new_wit X (wit: nonemptiness_witness) = subset (op =) (#I wit, (0 upto m - 1) @ map snd X);
   168 
   169     val all = m upto m + n - 1;
   170 
   171     fun enrich X = map_filter (fn i =>
   172       (case find_first (fn (_, i') => i = i') X of
   173         NONE =>
   174           (case find_index (new_wit X) (nth witss (i - m)) of
   175             ~1 => NONE
   176           | j => SOME (j, i))
   177       | SOME ji => SOME ji)) all;
   178     val reachable = fixpoint (op =) enrich [];
   179     val _ = (case subtract (op =) (map snd reachable) all of
   180         [] => ()
   181       | i :: _ => error ("Cannot define empty datatype " ^ quote (Binding.name_of (nth bs (i - m)))));
   182 
   183     val wit_thms = flat (map2 (fn bnf => fn (j, _) => nth (wit_thmss_of_bnf bnf) j) bnfs reachable);
   184 
   185     val timer = time (timer "Checked nonemptiness");
   186 
   187     (* derived thms *)
   188 
   189     (*map g1 ... gm g(m+1) ... g(m+n) (map id ... id f(m+1) ... f(m+n) x) =
   190       map g1 ... gm (g(m+1) o f(m+1)) ... (g(m+n) o f(m+n)) x*)
   191     fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp0 =
   192       let
   193         val lhs = Term.list_comb (mapBsCs, all_gs) $
   194           (Term.list_comb (mapAsBs, passive_ids @ fs) $ x);
   195         val rhs = Term.list_comb (mapAsCs,
   196           take m all_gs @ map HOLogic.mk_comp (drop m all_gs ~~ fs)) $ x;
   197         val vars = fold (Variable.add_free_names lthy) [lhs, rhs] [];
   198       in
   199         Goal.prove_sorry lthy vars [] (mk_Trueprop_eq (lhs, rhs))
   200           (fn {context = ctxt, prems = _} => mk_map_comp_id_tac ctxt map_comp0)
   201         |> Thm.close_derivation
   202       end;
   203 
   204     val map_comp_id_thms = @{map 5} mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;
   205 
   206     (*forall a : set(m+1) x. f(m+1) a = a; ...; forall a : set(m+n) x. f(m+n) a = a ==>
   207       map id ... id f(m+1) ... f(m+n) x = x*)
   208     fun mk_map_cong0L x mapAsAs sets map_cong0 map_id =
   209       let
   210         fun mk_prem set f z z' = HOLogic.mk_Trueprop
   211           (mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z))));
   212         val prems = @{map 4} mk_prem (drop m sets) self_fs zs zs';
   213         val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x);
   214         val vars = fold (Variable.add_free_names lthy) (goal :: prems) [];
   215       in
   216         Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, goal))
   217           (fn {context = ctxt, prems = _} => mk_map_cong0L_tac ctxt m map_cong0 map_id)
   218         |> Thm.close_derivation
   219       end;
   220 
   221     val map_cong0L_thms = @{map 5} mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
   222     val in_mono'_thms = map (fn bnf => in_mono_of_bnf bnf OF (replicate m subset_refl)) bnfs;
   223     val in_cong'_thms = map (fn bnf => in_cong_of_bnf bnf OF (replicate m refl)) bnfs;
   224 
   225     val timer = time (timer "Derived simple theorems");
   226 
   227     (* algebra *)
   228 
   229     val alg_bind = mk_internal_b algN;
   230     val alg_def_bind = (Thm.def_binding alg_bind, []);
   231 
   232     (*forall i = 1 ... n: (\<forall>x \<in> Fi_in UNIV .. UNIV B1 ... Bn. si x \<in> Bi)*)
   233     val alg_spec =
   234       let
   235         val ins = @{map 3} mk_in (replicate n (passive_UNIVs @ Bs)) setssAs FTsAs;
   236         fun mk_alg_conjunct B s X x x' =
   237           mk_Ball X (Term.absfree x' (HOLogic.mk_mem (s $ x, B)));
   238 
   239         val rhs = Library.foldr1 HOLogic.mk_conj (@{map 5} mk_alg_conjunct Bs ss ins xFs xFs')
   240       in
   241         fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss) rhs
   242       end;
   243 
   244     val ((alg_free, (_, alg_def_free)), (lthy, lthy_old)) =
   245       lthy
   246       |> Local_Theory.open_target |> snd
   247       |> Local_Theory.define ((alg_bind, NoSyn), (alg_def_bind, alg_spec))
   248       ||> `Local_Theory.close_target;
   249 
   250     val phi = Proof_Context.export_morphism lthy_old lthy;
   251     val alg = fst (Term.dest_Const (Morphism.term phi alg_free));
   252     val alg_def = mk_unabs_def (2 * n) (Morphism.thm phi alg_def_free RS meta_eq_to_obj_eq);
   253 
   254     fun mk_alg Bs ss =
   255       let
   256         val args = Bs @ ss;
   257         val Ts = map fastype_of args;
   258         val algT = Library.foldr (op -->) (Ts, HOLogic.boolT);
   259       in
   260         Term.list_comb (Const (alg, algT), args)
   261       end;
   262 
   263     val ((((((((zs, zs'), Bs), B's), ss), s's), fs), (xFs, xFs')), _) =
   264       lthy
   265       |> mk_Frees' "z" activeAs
   266       ||>> mk_Frees "B" BTs
   267       ||>> mk_Frees "B'" B'Ts
   268       ||>> mk_Frees "s" sTs
   269       ||>> mk_Frees "s'" s'Ts
   270       ||>> mk_Frees "f" fTs
   271       ||>> mk_Frees' "x" FTsAs;
   272 
   273     val alg_set_thms =
   274       let
   275         val alg_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
   276         fun mk_prem x set B = HOLogic.mk_Trueprop (mk_leq (set $ x) B);
   277         fun mk_concl s x B = mk_Trueprop_mem (s $ x, B);
   278         val premss = map2 ((fn x => fn sets => map2 (mk_prem x) (drop m sets) Bs)) xFs setssAs;
   279         val concls = @{map 3} mk_concl ss xFs Bs;
   280         val goals = map2 (fn prems => fn concl =>
   281           Logic.list_implies (alg_prem :: prems, concl)) premss concls;
   282       in
   283         map (fn goal =>
   284           Variable.add_free_names lthy goal []
   285           |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
   286             mk_alg_set_tac ctxt alg_def))
   287           |> Thm.close_derivation)
   288         goals
   289       end;
   290 
   291     val timer = time (timer "Algebra definition & thms");
   292 
   293     val alg_not_empty_thms =
   294       let
   295         val alg_prem =
   296           HOLogic.mk_Trueprop (mk_alg Bs ss);
   297         val concls = map (HOLogic.mk_Trueprop o mk_not_empty) Bs;
   298         val goals =
   299           map (fn concl => Logic.mk_implies (alg_prem, concl)) concls;
   300       in
   301         map2 (fn goal => fn alg_set =>
   302           Variable.add_free_names lthy goal []
   303           |> (fn vars => Goal.prove_sorry lthy vars [] goal
   304             (fn {context = ctxt, prems = _} =>
   305               mk_alg_not_empty_tac ctxt alg_set alg_set_thms wit_thms))
   306           |> Thm.close_derivation)
   307         goals alg_set_thms
   308       end;
   309 
   310     val timer = time (timer "Proved nonemptiness");
   311 
   312     (* morphism *)
   313 
   314     val mor_bind = mk_internal_b morN;
   315     val mor_def_bind = (Thm.def_binding mor_bind, []);
   316 
   317     (*fbetw) forall i = 1 ... n: (\<forall>x \<in> Bi. f x \<in> B'i)*)
   318     (*mor) forall i = 1 ... n: (\<forall>x \<in> Fi_in UNIV ... UNIV B1 ... Bn.
   319        f (s1 x) = s1' (Fi_map id ... id f1 ... fn x))*)
   320     val mor_spec =
   321       let
   322         fun mk_fbetw f B1 B2 z z' =
   323           mk_Ball B1 (Term.absfree z' (HOLogic.mk_mem (f $ z, B2)));
   324         fun mk_mor sets mapAsBs f s s' T x x' =
   325           mk_Ball (mk_in (passive_UNIVs @ Bs) sets T)
   326             (Term.absfree x' (HOLogic.mk_eq (f $ (s $ x), s' $
   327               (Term.list_comb (mapAsBs, passive_ids @ fs) $ x))));
   328         val rhs = HOLogic.mk_conj
   329           (Library.foldr1 HOLogic.mk_conj (@{map 5} mk_fbetw fs Bs B's zs zs'),
   330           Library.foldr1 HOLogic.mk_conj
   331             (@{map 8} mk_mor setssAs mapsAsBs fs ss s's FTsAs xFs xFs'))
   332       in
   333         fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss @ B's @ s's @ fs) rhs
   334       end;
   335 
   336     val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) =
   337       lthy
   338       |> Local_Theory.open_target |> snd
   339       |> Local_Theory.define ((mor_bind, NoSyn), (mor_def_bind, mor_spec))
   340       ||> `Local_Theory.close_target;
   341 
   342     val phi = Proof_Context.export_morphism lthy_old lthy;
   343     val mor = fst (Term.dest_Const (Morphism.term phi mor_free));
   344     val mor_def = mk_unabs_def (5 * n) (Morphism.thm phi mor_def_free RS meta_eq_to_obj_eq);
   345 
   346     fun mk_mor Bs1 ss1 Bs2 ss2 fs =
   347       let
   348         val args = Bs1 @ ss1 @ Bs2 @ ss2 @ fs;
   349         val Ts = map fastype_of (Bs1 @ ss1 @ Bs2 @ ss2 @ fs);
   350         val morT = Library.foldr (op -->) (Ts, HOLogic.boolT);
   351       in
   352         Term.list_comb (Const (mor, morT), args)
   353       end;
   354 
   355     val ((((((((((((Bs, Bs_copy), B's), B''s), ss), prod_ss), s's), s''s), fs), fs_copy), gs), xFs),
   356         _) =
   357       lthy
   358       |> mk_Frees "B" BTs
   359       ||>> mk_Frees "B" BTs
   360       ||>> mk_Frees "B'" B'Ts
   361       ||>> mk_Frees "B''" B''Ts
   362       ||>> mk_Frees "s" sTs
   363       ||>> mk_Frees "prods" prod_sTs
   364       ||>> mk_Frees "s'" s'Ts
   365       ||>> mk_Frees "s''" s''Ts
   366       ||>> mk_Frees "f" fTs
   367       ||>> mk_Frees "f" fTs
   368       ||>> mk_Frees "g" gTs
   369       ||>> mk_Frees "x" FTsAs;
   370 
   371     val morE_thms =
   372       let
   373         val prem = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs);
   374         fun mk_elim_prem sets x T = HOLogic.mk_Trueprop
   375           (HOLogic.mk_mem (x, mk_in (passive_UNIVs @ Bs) sets T));
   376         fun mk_elim_goal sets mapAsBs f s s' x T =
   377           Logic.list_implies ([prem, mk_elim_prem sets x T],
   378             mk_Trueprop_eq (f $ (s $ x), s' $ Term.list_comb (mapAsBs, passive_ids @ fs @ [x])));
   379         val elim_goals = @{map 7} mk_elim_goal setssAs mapsAsBs fs ss s's xFs FTsAs;
   380         fun prove goal =
   381           Variable.add_free_names lthy goal []
   382           |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
   383             mk_mor_elim_tac ctxt mor_def))
   384           |> Thm.close_derivation;
   385       in
   386         map prove elim_goals
   387       end;
   388 
   389     val mor_incl_thm =
   390       let
   391         val prems = map2 (HOLogic.mk_Trueprop oo mk_leq) Bs Bs_copy;
   392         val concl = HOLogic.mk_Trueprop (mk_mor Bs ss Bs_copy ss active_ids);
   393         val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
   394       in
   395         Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
   396           (fn {context = ctxt, prems = _} => mk_mor_incl_tac ctxt mor_def map_ids)
   397         |> Thm.close_derivation
   398       end;
   399 
   400     val mor_comp_thm =
   401       let
   402         val prems =
   403           [HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs),
   404            HOLogic.mk_Trueprop (mk_mor B's s's B''s s''s gs)];
   405         val concl =
   406           HOLogic.mk_Trueprop (mk_mor Bs ss B''s s''s (map2 (curry HOLogic.mk_comp) gs fs));
   407         val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
   408       in
   409         Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
   410           (fn {context = ctxt, prems = _} => mk_mor_comp_tac ctxt mor_def set_mapss map_comp_id_thms)
   411         |> Thm.close_derivation
   412       end;
   413 
   414     val mor_cong_thm =
   415       let
   416         val prems = map HOLogic.mk_Trueprop
   417          (map2 (curry HOLogic.mk_eq) fs_copy fs @ [mk_mor Bs ss B's s's fs])
   418         val concl = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs_copy);
   419         val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
   420       in
   421         Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
   422           (fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' assume_tac ctxt) 1)
   423         |> Thm.close_derivation
   424       end;
   425 
   426     val mor_str_thm =
   427       let
   428         val maps = map2 (fn Ds => fn bnf => Term.list_comb
   429           (mk_map_of_bnf Ds (passiveAs @ FTsAs) allAs bnf, passive_ids @ ss)) Dss bnfs;
   430         val goal = HOLogic.mk_Trueprop
   431           (mk_mor (map HOLogic.mk_UNIV FTsAs) maps active_UNIVs ss ss);
   432         val vars = Variable.add_free_names lthy goal [];
   433       in
   434         Goal.prove_sorry lthy vars [] goal
   435           (fn {context = ctxt, prems = _} => mk_mor_str_tac ctxt ks mor_def)
   436         |> Thm.close_derivation
   437       end;
   438 
   439     val mor_convol_thm =
   440       let
   441         val maps = @{map 3} (fn s => fn prod_s => fn mapx =>
   442           mk_convol (HOLogic.mk_comp (s, Term.list_comb (mapx, passive_ids @ fsts)), prod_s))
   443           s's prod_ss map_fsts;
   444         val goal = HOLogic.mk_Trueprop
   445           (mk_mor prod_UNIVs maps (map HOLogic.mk_UNIV activeBs) s's fsts)
   446         val vars = Variable.add_free_names lthy goal [];
   447       in
   448         Goal.prove_sorry lthy vars [] goal
   449           (fn {context = ctxt, prems = _} => mk_mor_convol_tac ctxt ks mor_def)
   450         |> Thm.close_derivation
   451       end;
   452 
   453     val mor_UNIV_thm =
   454       let
   455         fun mk_conjunct mapAsBs f s s' = HOLogic.mk_eq
   456             (HOLogic.mk_comp (f, s),
   457             HOLogic.mk_comp (s', Term.list_comb (mapAsBs, passive_ids @ fs)));
   458         val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs;
   459         val rhs = Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct mapsAsBs fs ss s's);
   460         val vars = fold (Variable.add_free_names lthy) [lhs, rhs] [];
   461       in
   462         Goal.prove_sorry lthy vars [] (mk_Trueprop_eq (lhs, rhs))
   463           (fn {context = ctxt, prems = _} => mk_mor_UNIV_tac ctxt m morE_thms mor_def)
   464         |> Thm.close_derivation
   465       end;
   466 
   467     val timer = time (timer "Morphism definition & thms");
   468 
   469     (* bounds *)
   470 
   471     val sum_bd = Library.foldr1 (uncurry mk_csum) bds;
   472     val sum_bdT = fst (dest_relT (fastype_of sum_bd));
   473     val (sum_bdT_params, sum_bdT_params') = `(map TFree) (Term.add_tfreesT sum_bdT []);
   474 
   475     val (lthy, sbd, sbd_Cinfinite, sbd_Card_order, set_sbdss, in_sbds) =
   476       if n = 1
   477       then (lthy, sum_bd, bd_Cinfinite, bd_Card_order, set_bdss, in_bds)
   478       else
   479         let
   480           val sbdT_bind = mk_internal_b sum_bdTN;
   481 
   482           val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) =
   483             typedef (sbdT_bind, sum_bdT_params', NoSyn)
   484               (HOLogic.mk_UNIV sum_bdT) NONE (fn ctxt =>
   485                 EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy;
   486 
   487           val sbdT = Type (sbdT_name, sum_bdT_params);
   488           val Abs_sbdT = Const (#Abs_name sbdT_glob_info, sum_bdT --> sbdT);
   489 
   490           val sbd_bind = mk_internal_b sum_bdN;
   491           val sbd_def_bind = (Thm.def_binding sbd_bind, []);
   492 
   493           val sbd_spec = mk_dir_image sum_bd Abs_sbdT;
   494 
   495           val ((sbd_free, (_, sbd_def_free)), (lthy, lthy_old)) =
   496             lthy
   497             |> Local_Theory.open_target |> snd
   498             |> Local_Theory.define ((sbd_bind, NoSyn), (sbd_def_bind, sbd_spec))
   499             ||> `Local_Theory.close_target;
   500 
   501           val phi = Proof_Context.export_morphism lthy_old lthy;
   502 
   503           val sbd_def = Morphism.thm phi sbd_def_free RS meta_eq_to_obj_eq;
   504           val sbd = Const (fst (Term.dest_Const (Morphism.term phi sbd_free)), mk_relT (`I sbdT));
   505 
   506           val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info);
   507 
   508           val sum_Cinfinite = mk_sum_Cinfinite bd_Cinfinites;
   509           val sum_Card_order = sum_Cinfinite RS conjunct2;
   510 
   511           val sbd_ordIso = @{thm ssubst_Pair_rhs} OF
   512             [@{thm dir_image} OF [Abs_sbdT_inj, sum_Card_order], sbd_def];
   513           val sbd_Cinfinite = @{thm Cinfinite_cong} OF [sbd_ordIso, sum_Cinfinite];
   514           val sbd_Card_order = sbd_Cinfinite RS conjunct2;
   515 
   516           fun mk_set_sbd i bd_Card_order bds =
   517             map (fn thm => @{thm ordLeq_ordIso_trans} OF
   518               [bd_Card_order RS mk_ordLeq_csum n i thm, sbd_ordIso]) bds;
   519           val set_sbdss = @{map 3} mk_set_sbd ks bd_Card_orders set_bdss;
   520 
   521           fun mk_in_bd_sum i Co Cnz bd =
   522             Cnz RS ((@{thm ordLeq_ordIso_trans} OF
   523               [Co RS mk_ordLeq_csum n i (Co RS @{thm ordLeq_refl}), sbd_ordIso]) RS
   524               (bd RS @{thm ordLeq_transitive[OF _ cexp_mono2_Cnotzero[OF _ Card_order_csum]]}));
   525           val in_sbds = @{map 4} mk_in_bd_sum ks bd_Card_orders bd_Cnotzeros in_bds;
   526        in
   527          (lthy, sbd, sbd_Cinfinite, sbd_Card_order, set_sbdss, in_sbds)
   528        end;
   529 
   530     val sbd_Cnotzero = sbd_Cinfinite RS @{thm Cinfinite_Cnotzero};
   531     val suc_bd = mk_cardSuc sbd;
   532 
   533     val field_suc_bd = mk_Field suc_bd;
   534     val suc_bdT = fst (dest_relT (fastype_of suc_bd));
   535     fun mk_Asuc_bd [] = mk_cexp ctwo suc_bd
   536       | mk_Asuc_bd As =
   537         mk_cexp (mk_csum (Library.foldr1 (uncurry mk_csum) (map mk_card_of As)) ctwo) suc_bd;
   538 
   539     val suc_bd_Card_order =  sbd_Card_order RS @{thm cardSuc_Card_order};
   540     val suc_bd_Cinfinite = sbd_Cinfinite RS @{thm Cinfinite_cardSuc};
   541     val suc_bd_Cnotzero = suc_bd_Cinfinite RS @{thm Cinfinite_Cnotzero};
   542     val suc_bd_worel = suc_bd_Card_order RS @{thm Card_order_wo_rel}
   543     val basis_Asuc = if m = 0 then @{thm ordLeq_refl[OF Card_order_ctwo]}
   544         else @{thm ordLeq_csum2[OF Card_order_ctwo]};
   545     val Asuc_bd_Cinfinite = suc_bd_Cinfinite RS (basis_Asuc RS @{thm Cinfinite_cexp});
   546 
   547     val suc_bd_Asuc_bd = @{thm ordLess_ordLeq_trans[OF ordLess_ctwo_cexp cexp_mono1]} OF
   548       [suc_bd_Card_order, basis_Asuc, suc_bd_Card_order];
   549 
   550 
   551     val Asuc_bd = mk_Asuc_bd passive_UNIVs;
   552     val Asuc_bdT = fst (dest_relT (fastype_of Asuc_bd));
   553     val II_BTs = replicate n (HOLogic.mk_setT Asuc_bdT);
   554     val II_sTs = map2 (fn Ds => fn bnf =>
   555       mk_T_of_bnf Ds (passiveAs @ replicate n Asuc_bdT) bnf --> Asuc_bdT) Dss bnfs;
   556 
   557     val ((((((Bs, ss), idxs), Asi_name), (idx, idx')), (jdx, jdx')), _) =
   558       lthy
   559       |> mk_Frees "B" BTs
   560       ||>> mk_Frees "s" sTs
   561       ||>> mk_Frees "i" (replicate n suc_bdT)
   562       ||>> (fn ctxt => apfst the_single (mk_fresh_names ctxt 1 "Asi"))
   563       ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") suc_bdT
   564       ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "j") suc_bdT;
   565 
   566     val suc_bd_limit_thm =
   567       let
   568         val prem = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   569           (map (fn idx => HOLogic.mk_mem (idx, field_suc_bd)) idxs));
   570         fun mk_conjunct idx = HOLogic.mk_conj (mk_not_eq idx jdx,
   571           HOLogic.mk_mem (HOLogic.mk_prod (idx, jdx), suc_bd));
   572         val concl = HOLogic.mk_Trueprop (mk_Bex field_suc_bd
   573           (Term.absfree jdx' (Library.foldr1 HOLogic.mk_conj (map mk_conjunct idxs))));
   574         val vars = fold (Variable.add_free_names lthy) [prem, concl] [];
   575       in
   576         Goal.prove_sorry lthy vars [] (Logic.list_implies ([prem], concl))
   577           (fn {context = ctxt, prems = _} => mk_bd_limit_tac ctxt n suc_bd_Cinfinite)
   578         |> Thm.close_derivation
   579       end;
   580 
   581     val timer = time (timer "Bounds");
   582 
   583     (* minimal algebra *)
   584 
   585     fun mk_minG Asi i k = mk_UNION (mk_underS suc_bd $ i)
   586       (Term.absfree jdx' (mk_nthN n (Asi $ jdx) k));
   587 
   588     fun mk_minH_component Asi i sets Ts s k =
   589       HOLogic.mk_binop @{const_name "sup"}
   590       (mk_minG Asi i k, mk_image s $ mk_in (passive_UNIVs @ map (mk_minG Asi i) ks) sets Ts);
   591 
   592     fun mk_min_algs ss =
   593       let
   594         val BTs = map (range_type o fastype_of) ss;
   595         val Ts = passiveAs @ BTs;
   596         val (Asi, Asi') = `Free (Asi_name, suc_bdT -->
   597           Library.foldr1 HOLogic.mk_prodT (map HOLogic.mk_setT BTs));
   598       in
   599          mk_worec suc_bd (Term.absfree Asi' (Term.absfree idx' (HOLogic.mk_tuple
   600            (@{map 4} (mk_minH_component Asi idx) (mk_setss Ts) (mk_FTs Ts) ss ks))))
   601       end;
   602 
   603     val (min_algs_thms, min_algs_mono_thms, card_of_min_algs_thm, least_min_algs_thm) =
   604       let
   605         val i_field = HOLogic.mk_mem (idx, field_suc_bd);
   606         val min_algs = mk_min_algs ss;
   607 
   608         val min_algss = map (fn k => mk_nthN n (min_algs $ idx) k) ks;
   609 
   610         val concl = HOLogic.mk_Trueprop
   611           (HOLogic.mk_eq (min_algs $ idx, HOLogic.mk_tuple
   612             (@{map 4} (mk_minH_component min_algs idx) setssAs FTsAs ss ks)));
   613         val goal = Logic.mk_implies (HOLogic.mk_Trueprop i_field, concl);
   614         val vars = Variable.add_free_names lthy goal [];
   615 
   616         val min_algs_thm = Goal.prove_sorry lthy vars [] goal
   617           (fn {context = ctxt, prems = _} => mk_min_algs_tac ctxt suc_bd_worel in_cong'_thms)
   618           |> Thm.close_derivation;
   619 
   620         val min_algs_thms = map (fn k => min_algs_thm RS mk_nthI n k) ks;
   621 
   622         fun mk_mono_goal min_alg =
   623           HOLogic.mk_Trueprop (mk_relChain suc_bd (Term.absfree idx' min_alg));
   624 
   625         val monos =
   626           map2 (fn goal => fn min_algs =>
   627             Variable.add_free_names lthy goal []
   628             |> (fn vars => Goal.prove_sorry lthy vars [] goal
   629               (fn {context = ctxt, prems = _} => mk_min_algs_mono_tac ctxt min_algs))
   630             |> Thm.close_derivation)
   631           (map mk_mono_goal min_algss) min_algs_thms;
   632 
   633         fun mk_card_conjunct min_alg = mk_ordLeq (mk_card_of min_alg) Asuc_bd;
   634         val card_conjunction = Library.foldr1 HOLogic.mk_conj (map mk_card_conjunct min_algss);
   635         val card_cT = Thm.ctyp_of lthy suc_bdT;
   636         val card_ct = Thm.cterm_of lthy (Term.absfree idx' card_conjunction);
   637 
   638         val card_of =
   639           let
   640             val goal = HOLogic.mk_Trueprop (HOLogic.mk_imp (i_field, card_conjunction));
   641             val vars = Variable.add_free_names lthy goal [];
   642           in
   643             Goal.prove_sorry lthy vars [] goal
   644               (fn {context = ctxt, prems = _} => mk_min_algs_card_of_tac ctxt card_cT card_ct
   645                 m suc_bd_worel min_algs_thms in_sbds
   646                 sbd_Card_order sbd_Cnotzero suc_bd_Card_order suc_bd_Cinfinite suc_bd_Cnotzero
   647                 suc_bd_Asuc_bd Asuc_bd_Cinfinite)
   648             |> Thm.close_derivation
   649           end;
   650 
   651         val least_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
   652         val least_conjunction = Library.foldr1 HOLogic.mk_conj (map2 mk_leq min_algss Bs);
   653         val least_cT = Thm.ctyp_of lthy suc_bdT;
   654         val least_ct = Thm.cterm_of lthy (Term.absfree idx' least_conjunction);
   655 
   656         val least =
   657           let
   658             val goal = Logic.mk_implies (least_prem,
   659               HOLogic.mk_Trueprop (HOLogic.mk_imp (i_field, least_conjunction)));
   660             val vars = Variable.add_free_names lthy goal [];
   661           in
   662             Goal.prove_sorry lthy vars [] goal
   663               (fn {context = ctxt, prems = _} => mk_min_algs_least_tac ctxt least_cT least_ct
   664                 suc_bd_worel min_algs_thms alg_set_thms)
   665             |> Thm.close_derivation
   666           end;
   667       in
   668         (min_algs_thms, monos, card_of, least)
   669       end;
   670 
   671     val timer = time (timer "min_algs definition & thms");
   672 
   673     val min_alg_binds = mk_internal_bs min_algN;
   674     fun min_alg_bind i = nth min_alg_binds (i - 1);
   675     val min_alg_def_bind = rpair [] o Thm.def_binding o min_alg_bind;
   676 
   677     fun min_alg_spec i =
   678       let
   679         val rhs = mk_UNION (field_suc_bd)
   680           (Term.absfree idx' (mk_nthN n (mk_min_algs ss $ idx) i));
   681       in
   682         fold_rev (Term.absfree o Term.dest_Free) ss rhs
   683       end;
   684 
   685     val ((min_alg_frees, (_, min_alg_def_frees)), (lthy, lthy_old)) =
   686       lthy
   687       |> Local_Theory.open_target |> snd
   688       |> fold_map (fn i => Local_Theory.define
   689         ((min_alg_bind i, NoSyn), (min_alg_def_bind i, min_alg_spec i))) ks
   690       |>> apsnd split_list o split_list
   691       ||> `Local_Theory.close_target;
   692 
   693     val phi = Proof_Context.export_morphism lthy_old lthy;
   694     val min_algs = map (fst o Term.dest_Const o Morphism.term phi) min_alg_frees;
   695     val min_alg_defs = map (fn def =>
   696       mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) min_alg_def_frees;
   697 
   698     fun mk_min_alg ss i =
   699       let
   700         val T = HOLogic.mk_setT (range_type (fastype_of (nth ss (i - 1))))
   701         val Ts = map fastype_of ss;
   702         val min_algT = Library.foldr (op -->) (Ts, T);
   703       in
   704         Term.list_comb (Const (nth min_algs (i - 1), min_algT), ss)
   705       end;
   706 
   707     val min_algs = map (mk_min_alg ss) ks;
   708 
   709     val ((Bs, ss), _) =
   710       lthy
   711       |> mk_Frees "B" BTs
   712       ||>> mk_Frees "s" sTs;
   713 
   714     val (alg_min_alg_thm, card_of_min_alg_thms, least_min_alg_thms, mor_incl_min_alg_thm) =
   715       let
   716         val alg_min_alg =
   717           let
   718             val goal = HOLogic.mk_Trueprop (mk_alg min_algs ss);
   719             val vars = Variable.add_free_names lthy goal [];
   720           in
   721             Goal.prove_sorry lthy vars [] goal
   722               (fn {context = ctxt, prems = _} => mk_alg_min_alg_tac ctxt m alg_def min_alg_defs
   723                 suc_bd_limit_thm sbd_Cinfinite set_sbdss min_algs_thms min_algs_mono_thms)
   724             |> Thm.close_derivation
   725           end;
   726 
   727         fun mk_card_of_thm min_alg def =
   728           let
   729             val goal = HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of min_alg) Asuc_bd);
   730             val vars = Variable.add_free_names lthy goal [];
   731           in
   732             Goal.prove_sorry lthy vars [] goal
   733               (fn {context = ctxt, prems = _} => mk_card_of_min_alg_tac ctxt def card_of_min_algs_thm
   734                 suc_bd_Card_order suc_bd_Asuc_bd Asuc_bd_Cinfinite)
   735             |> Thm.close_derivation
   736           end;
   737 
   738         fun mk_least_thm min_alg B def =
   739           let
   740             val prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
   741             val goal = Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_leq min_alg B));
   742             val vars = Variable.add_free_names lthy goal [];
   743           in
   744             Goal.prove_sorry lthy vars [] goal
   745               (fn {context = ctxt, prems = _} => mk_least_min_alg_tac ctxt def least_min_algs_thm)
   746             |> Thm.close_derivation
   747           end;
   748 
   749         val leasts = @{map 3} mk_least_thm min_algs Bs min_alg_defs;
   750 
   751         val incl =
   752           let
   753             val prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
   754             val goal = Logic.mk_implies (prem,
   755               HOLogic.mk_Trueprop (mk_mor min_algs ss Bs ss active_ids));
   756             val vars = Variable.add_free_names lthy goal [];
   757           in
   758             Goal.prove_sorry lthy vars [] goal
   759               (fn {context = ctxt, prems = _} =>
   760                 EVERY' (rtac ctxt mor_incl_thm :: map (etac ctxt) leasts) 1)
   761             |> Thm.close_derivation
   762           end;
   763       in
   764         (alg_min_alg, map2 mk_card_of_thm min_algs min_alg_defs, leasts, incl)
   765       end;
   766 
   767     val timer = time (timer "Minimal algebra definition & thms");
   768 
   769     val II_repT = HOLogic.mk_prodT (HOLogic.mk_tupleT II_BTs, HOLogic.mk_tupleT II_sTs);
   770     val IIT_bind = mk_internal_b IITN;
   771 
   772     val ((IIT_name, (IIT_glob_info, IIT_loc_info)), lthy) =
   773       typedef (IIT_bind, params, NoSyn)
   774         (HOLogic.mk_UNIV II_repT) NONE (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy;
   775 
   776     val IIT = Type (IIT_name, params');
   777     val Abs_IIT = Const (#Abs_name IIT_glob_info, II_repT --> IIT);
   778     val Rep_IIT = Const (#Rep_name IIT_glob_info, IIT --> II_repT);
   779     val Abs_IIT_inverse_thm = UNIV_I RS #Abs_inverse IIT_loc_info;
   780 
   781     val initT = IIT --> Asuc_bdT;
   782     val active_initTs = replicate n initT;
   783     val init_FTs = map2 (fn Ds => mk_T_of_bnf Ds (passiveAs @ active_initTs)) Dss bnfs;
   784     val init_fTs = map (fn T => initT --> T) activeAs;
   785 
   786     val ((((II_Bs, II_ss), (iidx, iidx')), init_xFs), _) =
   787       lthy
   788       |> mk_Frees "IIB" II_BTs
   789       ||>> mk_Frees "IIs" II_sTs
   790       ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") IIT
   791       ||>> mk_Frees "x" init_FTs;
   792 
   793     val II = HOLogic.mk_Collect (fst iidx', IIT, list_exists_free (II_Bs @ II_ss)
   794       (HOLogic.mk_conj (HOLogic.mk_eq (iidx,
   795         Abs_IIT $ (HOLogic.mk_prod (HOLogic.mk_tuple II_Bs, HOLogic.mk_tuple II_ss))),
   796         mk_alg II_Bs II_ss)));
   797 
   798     val select_Bs = map (mk_nthN n (HOLogic.mk_fst (Rep_IIT $ iidx))) ks;
   799     val select_ss = map (mk_nthN n (HOLogic.mk_snd (Rep_IIT $ iidx))) ks;
   800 
   801     val str_init_binds = mk_internal_bs str_initN;
   802     fun str_init_bind i = nth str_init_binds (i - 1);
   803     val str_init_def_bind = rpair [] o Thm.def_binding o str_init_bind;
   804 
   805     fun str_init_spec i =
   806       let
   807         val init_xF = nth init_xFs (i - 1)
   808         val select_s = nth select_ss (i - 1);
   809         val map = mk_map_of_bnf (nth Dss (i - 1))
   810           (passiveAs @ active_initTs) (passiveAs @ replicate n Asuc_bdT)
   811           (nth bnfs (i - 1));
   812         val map_args = passive_ids @ replicate n (mk_rapp iidx Asuc_bdT);
   813         val rhs = select_s $ (Term.list_comb (map, map_args) $ init_xF);
   814       in
   815         fold_rev (Term.absfree o Term.dest_Free) [init_xF, iidx] rhs
   816       end;
   817 
   818     val ((str_init_frees, (_, str_init_def_frees)), (lthy, lthy_old)) =
   819       lthy
   820       |> Local_Theory.open_target |> snd
   821       |> fold_map (fn i => Local_Theory.define
   822         ((str_init_bind i, NoSyn), (str_init_def_bind i, str_init_spec i))) ks
   823       |>> apsnd split_list o split_list
   824       ||> `Local_Theory.close_target;
   825 
   826     val phi = Proof_Context.export_morphism lthy_old lthy;
   827     val str_inits =
   828       map (Term.subst_atomic_types (map (`(Morphism.typ phi)) params') o Morphism.term phi)
   829         str_init_frees;
   830 
   831     val str_init_defs = map (fn def =>
   832       mk_unabs_def 2 (Morphism.thm phi def RS meta_eq_to_obj_eq)) str_init_def_frees;
   833 
   834     val car_inits = map (mk_min_alg str_inits) ks;
   835 
   836     val (((((((((Bs, ss), Asuc_fs), (iidx, iidx')), init_xs), (init_xFs, init_xFs')), init_fs),
   837         init_fs_copy), init_phis), _) =
   838       lthy
   839       |> mk_Frees "B" BTs
   840       ||>> mk_Frees "s" sTs
   841       ||>> mk_Frees "f" (map (fn T => Asuc_bdT --> T) activeAs)
   842       ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") IIT
   843       ||>> mk_Frees "ix" active_initTs
   844       ||>> mk_Frees' "x" init_FTs
   845       ||>> mk_Frees "f" init_fTs
   846       ||>> mk_Frees "f" init_fTs
   847       ||>> mk_Frees "P" (replicate n (mk_pred1T initT));
   848 
   849     val alg_init_thm =
   850       infer_instantiate' lthy (map (SOME o Thm.cterm_of lthy) str_inits) alg_min_alg_thm;
   851 
   852     val alg_select_thm = Goal.prove_sorry lthy [] []
   853       (HOLogic.mk_Trueprop (mk_Ball II
   854         (Term.absfree iidx' (mk_alg select_Bs select_ss))))
   855       (fn {context = ctxt, prems = _} => mk_alg_select_tac ctxt Abs_IIT_inverse_thm)
   856       |> Thm.close_derivation;
   857 
   858     val mor_select_thm =
   859       let
   860         val i_prem = mk_Trueprop_mem (iidx, II);
   861         val mor_prem = HOLogic.mk_Trueprop (mk_mor select_Bs select_ss active_UNIVs ss Asuc_fs);
   862         val prems = [i_prem, mor_prem];
   863         val concl = HOLogic.mk_Trueprop
   864           (mk_mor car_inits str_inits active_UNIVs ss
   865             (map (fn f => HOLogic.mk_comp (f, mk_rapp iidx Asuc_bdT)) Asuc_fs));
   866         val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
   867       in
   868         Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
   869           (fn {context = ctxt, prems = _} => mk_mor_select_tac ctxt mor_def mor_cong_thm
   870             mor_comp_thm mor_incl_min_alg_thm alg_def alg_select_thm alg_set_thms set_mapss
   871             str_init_defs)
   872         |> Thm.close_derivation
   873       end;
   874 
   875     val init_unique_mor_thms =
   876       let
   877         val prems = map2 (HOLogic.mk_Trueprop oo curry HOLogic.mk_mem) init_xs car_inits
   878         val mor_prems = map HOLogic.mk_Trueprop
   879           [mk_mor car_inits str_inits Bs ss init_fs,
   880           mk_mor car_inits str_inits Bs ss init_fs_copy];
   881         fun mk_fun_eq f g x = HOLogic.mk_eq (f $ x, g $ x);
   882         val unique = HOLogic.mk_Trueprop
   883           (Library.foldr1 HOLogic.mk_conj (@{map 3} mk_fun_eq init_fs init_fs_copy init_xs));
   884         val cts = map (Thm.cterm_of lthy) ss;
   885         val all_prems = prems @ mor_prems;
   886         val vars = fold (Variable.add_free_names lthy) (unique :: all_prems) [];
   887         val unique_mor =
   888           Goal.prove_sorry lthy vars [] (Logic.list_implies (all_prems, unique))
   889             (fn {context = ctxt, prems = _} => mk_init_unique_mor_tac ctxt cts m alg_def
   890               alg_init_thm least_min_alg_thms in_mono'_thms alg_set_thms morE_thms map_cong0s)
   891           |> Thm.close_derivation;
   892       in
   893         split_conj_thm unique_mor
   894       end;
   895 
   896     val init_setss = mk_setss (passiveAs @ active_initTs);
   897     val active_init_setss = map (drop m) init_setss;
   898     val init_ins = map2 (fn sets => mk_in (passive_UNIVs @ car_inits) sets) init_setss init_FTs;
   899 
   900     fun mk_closed phis =
   901       let
   902         fun mk_conjunct phi str_init init_sets init_in x x' =
   903           let
   904             val prem = Library.foldr1 HOLogic.mk_conj
   905               (map2 (fn set => mk_Ball (set $ x)) init_sets phis);
   906             val concl = phi $ (str_init $ x);
   907           in
   908             mk_Ball init_in (Term.absfree x' (HOLogic.mk_imp (prem, concl)))
   909           end;
   910       in
   911         Library.foldr1 HOLogic.mk_conj
   912           (@{map 6} mk_conjunct phis str_inits active_init_setss init_ins init_xFs init_xFs')
   913       end;
   914 
   915     val init_induct_thm =
   916       let
   917         val prem = HOLogic.mk_Trueprop (mk_closed init_phis);
   918         val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   919           (map2 mk_Ball car_inits init_phis));
   920         val vars = fold (Variable.add_free_names lthy) [concl, prem] [];
   921       in
   922         Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, concl))
   923           (fn {context = ctxt, prems = _} => mk_init_induct_tac ctxt m alg_def alg_init_thm
   924             least_min_alg_thms alg_set_thms)
   925         |> Thm.close_derivation
   926       end;
   927 
   928     val timer = time (timer "Initiality definition & thms");
   929 
   930     val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
   931       lthy
   932       |> @{fold_map 3} (fn b => fn mx => fn car_init =>
   933         typedef (b, params, mx) car_init NONE
   934           (fn ctxt =>
   935             EVERY' [rtac ctxt iffD2, rtac ctxt @{thm ex_in_conv}, resolve_tac ctxt alg_not_empty_thms,
   936             rtac ctxt alg_init_thm] 1)) bs mixfixes car_inits
   937       |>> apsnd split_list o split_list;
   938 
   939     val Ts = map (fn name => Type (name, params')) T_names;
   940     fun mk_Ts passive = map (Term.typ_subst_atomic (passiveAs ~~ passive)) Ts;
   941     val Ts' = mk_Ts passiveBs;
   942     val Rep_Ts = map2 (fn info => fn T => Const (#Rep_name info, T --> initT)) T_glob_infos Ts;
   943     val Abs_Ts = map2 (fn info => fn T => Const (#Abs_name info, initT --> T)) T_glob_infos Ts;
   944 
   945     val type_defs = map #type_definition T_loc_infos;
   946     val Reps = map #Rep T_loc_infos;
   947     val Rep_inverses = map #Rep_inverse T_loc_infos;
   948     val Abs_inverses = map #Abs_inverse T_loc_infos;
   949 
   950     val timer = time (timer "THE TYPEDEFs & Rep/Abs thms");
   951 
   952     val UNIVs = map HOLogic.mk_UNIV Ts;
   953     val FTs = mk_FTs (passiveAs @ Ts);
   954     val FTs' = mk_FTs (passiveBs @ Ts');
   955     fun mk_set_Ts T = passiveAs @ replicate n (HOLogic.mk_setT T);
   956     val setFTss = map (mk_FTs o mk_set_Ts) passiveAs;
   957     val FTs_setss = mk_setss (passiveAs @ Ts);
   958     val FTs'_setss = mk_setss (passiveBs @ Ts');
   959     val map_FT_inits = map2 (fn Ds =>
   960       mk_map_of_bnf Ds (passiveAs @ Ts) (passiveAs @ active_initTs)) Dss bnfs;
   961     val fTs = map2 (curry op -->) Ts activeAs;
   962     val foldT = Library.foldr1 HOLogic.mk_prodT (map2 (curry op -->) Ts activeAs);
   963     val rec_sTs = map (Term.typ_subst_atomic (activeBs ~~ Ts)) prod_sTs;
   964     val rec_maps = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_fsts;
   965     val rec_maps_rev = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_fsts_rev;
   966     val rec_fsts = map (Term.subst_atomic_types (activeBs ~~ Ts)) fsts;
   967     val rec_UNIVs = map2 (HOLogic.mk_UNIV oo curry HOLogic.mk_prodT) Ts activeAs;
   968 
   969     val ((ss, (fold_f, fold_f')), _) =
   970       lthy
   971       |> mk_Frees "s" sTs
   972       ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "f") foldT;
   973 
   974     fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_");
   975     val ctor_def_bind = rpair [] o Binding.concealed o Thm.def_binding o ctor_bind;
   976 
   977     fun ctor_spec abs str map_FT_init =
   978       Library.foldl1 HOLogic.mk_comp [abs, str,
   979         Term.list_comb (map_FT_init, map HOLogic.id_const passiveAs @ Rep_Ts)];
   980 
   981     val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) =
   982       lthy
   983       |> Local_Theory.open_target |> snd
   984       |> @{fold_map 4} (fn i => fn abs => fn str => fn mapx =>
   985         Local_Theory.define
   986           ((ctor_bind i, NoSyn), (ctor_def_bind i, ctor_spec abs str mapx)))
   987           ks Abs_Ts str_inits map_FT_inits
   988       |>> apsnd split_list o split_list
   989       ||> `Local_Theory.close_target;
   990 
   991     val phi = Proof_Context.export_morphism lthy_old lthy;
   992     fun mk_ctors passive =
   993       map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (mk_params passive)) o
   994         Morphism.term phi) ctor_frees;
   995     val ctors = mk_ctors passiveAs;
   996     val ctor's = mk_ctors passiveBs;
   997     val ctor_defs = map (fn def => Morphism.thm phi def RS meta_eq_to_obj_eq) ctor_def_frees;
   998 
   999     val (mor_Rep_thm, mor_Abs_thm) =
  1000       let
  1001         val defs = mor_def :: ctor_defs;
  1002 
  1003         val mor_Rep =
  1004           Goal.prove_sorry lthy [] []
  1005             (HOLogic.mk_Trueprop (mk_mor UNIVs ctors car_inits str_inits Rep_Ts))
  1006             (fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt m defs Reps Abs_inverses
  1007               alg_min_alg_thm alg_set_thms set_mapss)
  1008           |> Thm.close_derivation;
  1009 
  1010         fun mk_ct initFT str abs = Term.absdummy initFT (abs $ (str $ Bound 0))
  1011         val cts = @{map 3} (Thm.cterm_of lthy ooo mk_ct) init_FTs str_inits Abs_Ts;
  1012 
  1013         val mor_Abs =
  1014           Goal.prove_sorry lthy [] []
  1015             (HOLogic.mk_Trueprop (mk_mor car_inits str_inits UNIVs ctors Abs_Ts))
  1016             (fn {context = ctxt, prems = _} => mk_mor_Abs_tac ctxt cts defs Abs_inverses
  1017               map_comp_id_thms map_cong0L_thms)
  1018           |> Thm.close_derivation;
  1019       in
  1020         (mor_Rep, mor_Abs)
  1021       end;
  1022 
  1023     val timer = time (timer "ctor definitions & thms");
  1024 
  1025     val fold_fun = Term.absfree fold_f'
  1026       (mk_mor UNIVs ctors active_UNIVs ss (map (mk_nthN n fold_f) ks));
  1027     val foldx = HOLogic.choice_const foldT $ fold_fun;
  1028 
  1029     fun fold_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctor_foldN ^ "_");
  1030     val fold_def_bind = rpair [] o Binding.concealed o Thm.def_binding o fold_bind;
  1031 
  1032     fun fold_spec i = fold_rev (Term.absfree o Term.dest_Free) ss (mk_nthN n foldx i);
  1033 
  1034     val ((fold_frees, (_, fold_def_frees)), (lthy, lthy_old)) =
  1035       lthy
  1036       |> Local_Theory.open_target |> snd
  1037       |> fold_map (fn i =>
  1038         Local_Theory.define ((fold_bind i, NoSyn), (fold_def_bind i, fold_spec i))) ks
  1039       |>> apsnd split_list o split_list
  1040       ||> `Local_Theory.close_target;
  1041 
  1042     val phi = Proof_Context.export_morphism lthy_old lthy;
  1043     val folds = map (Morphism.term phi) fold_frees;
  1044     val fold_names = map (fst o dest_Const) folds;
  1045     fun mk_folds passives actives =
  1046       @{map 3} (fn name => fn T => fn active =>
  1047         Const (name, Library.foldr (op -->)
  1048           (map2 (curry op -->) (mk_FTs (passives @ actives)) actives, T --> active)))
  1049       fold_names (mk_Ts passives) actives;
  1050     fun mk_fold Ts ss i = Term.list_comb (Const (nth fold_names (i - 1), Library.foldr (op -->)
  1051       (map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss);
  1052     val fold_defs = map (fn def =>
  1053       mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) fold_def_frees;
  1054 
  1055     (* algebra copies *)
  1056 
  1057     val (((((((Bs, B's), ss), s's), inv_fs), fs), rec_ss), _) =
  1058       lthy
  1059       |> mk_Frees "B" BTs
  1060       ||>> mk_Frees "B'" B'Ts
  1061       ||>> mk_Frees "s" sTs
  1062       ||>> mk_Frees "s'" s'Ts
  1063       ||>> mk_Frees "f" inv_fTs
  1064       ||>> mk_Frees "f" fTs
  1065       ||>> mk_Frees "s" rec_sTs;
  1066 
  1067     val copy_thm =
  1068       let
  1069         val prems = HOLogic.mk_Trueprop (mk_alg Bs ss) ::
  1070           @{map 3} (HOLogic.mk_Trueprop ooo mk_bij_betw) inv_fs B's Bs;
  1071         val concl = HOLogic.mk_Trueprop (list_exists_free s's
  1072           (HOLogic.mk_conj (mk_alg B's s's, mk_mor B's s's Bs ss inv_fs)));
  1073         val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
  1074       in
  1075         Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
  1076           (fn {context = ctxt, prems = _} => mk_copy_tac ctxt m alg_def mor_def alg_set_thms
  1077             set_mapss)
  1078         |> Thm.close_derivation
  1079       end;
  1080 
  1081     val init_ex_mor_thm =
  1082       let
  1083         val goal = HOLogic.mk_Trueprop
  1084           (list_exists_free fs (mk_mor UNIVs ctors active_UNIVs ss fs));
  1085         val vars = Variable.add_free_names lthy goal [];
  1086       in
  1087         Goal.prove_sorry lthy vars [] goal
  1088           (fn {context = ctxt, prems = _} =>
  1089             mk_init_ex_mor_tac ctxt Abs_IIT_inverse_thm (alg_min_alg_thm RS copy_thm)
  1090               card_of_min_alg_thms mor_Rep_thm mor_comp_thm mor_select_thm mor_incl_thm)
  1091         |> Thm.close_derivation
  1092       end;
  1093 
  1094     val mor_fold_thm =
  1095       let
  1096         val mor_cong = mor_cong_thm OF (map (mk_nth_conv n) ks);
  1097         val cT = Thm.ctyp_of lthy foldT;
  1098         val ct = Thm.cterm_of lthy fold_fun
  1099         val goal = HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss (map (mk_fold Ts ss) ks));
  1100         val vars = Variable.add_free_names lthy goal [];
  1101       in
  1102         Goal.prove_sorry lthy vars [] goal
  1103           (fn {context = ctxt, ...} =>
  1104             mk_mor_fold_tac ctxt cT ct fold_defs init_ex_mor_thm mor_cong)
  1105         |> Thm.close_derivation
  1106       end;
  1107 
  1108     val ctor_fold_thms = map (fn morE => rule_by_tactic lthy
  1109       ((rtac lthy CollectI THEN' CONJ_WRAP' (K (rtac lthy @{thm subset_UNIV})) (1 upto m + n)) 1)
  1110       (mor_fold_thm RS morE)) morE_thms;
  1111 
  1112     val (fold_unique_mor_thms, fold_unique_mor_thm) =
  1113       let
  1114         val prem = HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss fs);
  1115         fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_fold Ts ss i);
  1116         val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_fun_eq fs ks));
  1117         val vars = fold (Variable.add_free_names lthy) [prem, unique] [];
  1118         val unique_mor = Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, unique))
  1119           (fn {context = ctxt, prems = _} => mk_fold_unique_mor_tac ctxt type_defs
  1120             init_unique_mor_thms Reps mor_comp_thm mor_Abs_thm mor_fold_thm)
  1121           |> Thm.close_derivation;
  1122       in
  1123         `split_conj_thm unique_mor
  1124       end;
  1125 
  1126     val (ctor_fold_unique_thms, ctor_fold_unique_thm) =
  1127       `split_conj_thm (mk_conjIN n RS
  1128         (mor_UNIV_thm RS iffD2 RS fold_unique_mor_thm))
  1129 
  1130     val fold_ctor_thms =
  1131       map (fn thm => (mor_incl_thm OF replicate n @{thm subset_UNIV}) RS thm RS sym)
  1132         fold_unique_mor_thms;
  1133 
  1134     val ctor_o_fold_thms =
  1135       let
  1136         val mor = mor_comp_thm OF [mor_fold_thm, mor_str_thm];
  1137       in
  1138         map2 (fn unique => fn fold_ctor =>
  1139           trans OF [mor RS unique, fold_ctor]) fold_unique_mor_thms fold_ctor_thms
  1140       end;
  1141 
  1142     val timer = time (timer "fold definitions & thms");
  1143 
  1144     val map_ctors = map2 (fn Ds => fn bnf =>
  1145       Term.list_comb (mk_map_of_bnf Ds (passiveAs @ FTs) (passiveAs @ Ts) bnf,
  1146         map HOLogic.id_const passiveAs @ ctors)) Dss bnfs;
  1147 
  1148     fun dtor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtorN ^ "_");
  1149     val dtor_def_bind = rpair [] o Binding.concealed o Thm.def_binding o dtor_bind;
  1150 
  1151     fun dtor_spec i = mk_fold Ts map_ctors i;
  1152 
  1153     val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) =
  1154       lthy
  1155       |> Local_Theory.open_target |> snd
  1156       |> fold_map (fn i =>
  1157         Local_Theory.define ((dtor_bind i, NoSyn), (dtor_def_bind i, dtor_spec i))) ks
  1158       |>> apsnd split_list o split_list
  1159       ||> `Local_Theory.close_target;
  1160 
  1161     val phi = Proof_Context.export_morphism lthy_old lthy;
  1162     fun mk_dtors params =
  1163       map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ params) o Morphism.term phi)
  1164         dtor_frees;
  1165     val dtors = mk_dtors params';
  1166     val dtor_defs = map (fn def => Morphism.thm phi def RS meta_eq_to_obj_eq) dtor_def_frees;
  1167 
  1168     val ctor_o_dtor_thms = map2 (fold_thms lthy o single) dtor_defs ctor_o_fold_thms;
  1169 
  1170     val dtor_o_ctor_thms =
  1171       let
  1172         fun mk_goal dtor ctor FT =
  1173           mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT);
  1174         val goals = @{map 3} mk_goal dtors ctors FTs;
  1175       in
  1176         @{map 5} (fn goal => fn dtor_def => fn foldx => fn map_comp_id => fn map_cong0L =>
  1177           Goal.prove_sorry lthy [] [] goal
  1178             (fn {context = ctxt, prems = _} => mk_dtor_o_ctor_tac ctxt dtor_def foldx map_comp_id
  1179               map_cong0L ctor_o_fold_thms)
  1180           |> Thm.close_derivation)
  1181         goals dtor_defs ctor_fold_thms map_comp_id_thms map_cong0L_thms
  1182       end;
  1183 
  1184     val dtor_ctor_thms = map (fn thm => thm RS @{thm pointfree_idE}) dtor_o_ctor_thms;
  1185     val ctor_dtor_thms = map (fn thm => thm RS @{thm pointfree_idE}) ctor_o_dtor_thms;
  1186 
  1187     val bij_dtor_thms =
  1188       map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) ctor_o_dtor_thms dtor_o_ctor_thms;
  1189     val inj_dtor_thms = map (fn thm => thm RS @{thm bij_is_inj}) bij_dtor_thms;
  1190     val surj_dtor_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_dtor_thms;
  1191     val dtor_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_dtor_thms;
  1192     val dtor_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_dtor_thms;
  1193     val dtor_exhaust_thms = map (fn thm => thm RS exE) dtor_nchotomy_thms;
  1194 
  1195     val bij_ctor_thms =
  1196       map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) dtor_o_ctor_thms ctor_o_dtor_thms;
  1197     val inj_ctor_thms = map (fn thm => thm RS @{thm bij_is_inj}) bij_ctor_thms;
  1198     val surj_ctor_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_ctor_thms;
  1199     val ctor_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_ctor_thms;
  1200     val ctor_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_ctor_thms;
  1201     val ctor_exhaust_thms = map (fn thm => thm RS exE) ctor_nchotomy_thms;
  1202 
  1203     val timer = time (timer "dtor definitions & thms");
  1204 
  1205     val (((((((((Izs, (Izs1, Izs1'))), (Izs2, Izs2')), xFs), yFs), fs), rec_ss), init_phis), _) =
  1206       lthy
  1207       |> mk_Frees "z" Ts
  1208       ||>> mk_Frees' "z1" Ts
  1209       ||>> mk_Frees' "z2" Ts'
  1210       ||>> mk_Frees "x" FTs
  1211       ||>> mk_Frees "y" FTs'
  1212       ||>> mk_Frees "f" fTs
  1213       ||>> mk_Frees "s" rec_sTs
  1214       ||>> mk_Frees "P" (replicate n (mk_pred1T initT));
  1215 
  1216     val phis = map2 retype_const_or_free (map mk_pred1T Ts) init_phis;
  1217     val phi2s = map2 retype_const_or_free (map2 mk_pred2T Ts Ts') init_phis;
  1218 
  1219     val (ctor_induct_thm, induct_params) =
  1220       let
  1221         fun mk_prem phi ctor sets x =
  1222           let
  1223             fun mk_IH phi set z =
  1224               let
  1225                 val prem = mk_Trueprop_mem (z, set $ x);
  1226                 val concl = HOLogic.mk_Trueprop (phi $ z);
  1227               in
  1228                 Logic.all z (Logic.mk_implies (prem, concl))
  1229               end;
  1230 
  1231             val IHs = @{map 3} mk_IH phis (drop m sets) Izs;
  1232             val concl = HOLogic.mk_Trueprop (phi $ (ctor $ x));
  1233           in
  1234             Logic.all x (Logic.list_implies (IHs, concl))
  1235           end;
  1236 
  1237         val prems = @{map 4} mk_prem phis ctors FTs_setss xFs;
  1238 
  1239         fun mk_concl phi z = phi $ z;
  1240         val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_concl phis Izs));
  1241 
  1242         val goal = Logic.list_implies (prems, concl);
  1243         val vars = Variable.add_free_names lthy goal [];
  1244       in
  1245         (Goal.prove_sorry lthy vars [] goal
  1246           (fn {context = ctxt, prems = _} =>
  1247             mk_ctor_induct_tac ctxt m set_mapss init_induct_thm morE_thms mor_Abs_thm
  1248             Rep_inverses Abs_inverses Reps)
  1249         |> Thm.close_derivation,
  1250         rev (Term.add_tfrees goal []))
  1251       end;
  1252 
  1253     val cTs = map (SOME o Thm.ctyp_of lthy o TFree) induct_params;
  1254 
  1255     val weak_ctor_induct_thms =
  1256       let fun insts i = (replicate (i - 1) TrueI) @ (asm_rl :: replicate (n - i) TrueI);
  1257       in map (fn i => (ctor_induct_thm OF insts i) RS mk_conjunctN n i) ks end;
  1258 
  1259     val (ctor_induct2_thm, induct2_params) =
  1260       let
  1261         fun mk_prem phi ctor ctor' sets sets' x y =
  1262           let
  1263             fun mk_IH phi set set' z1 z2 =
  1264               let
  1265                 val prem1 = mk_Trueprop_mem (z1, (set $ x));
  1266                 val prem2 = mk_Trueprop_mem (z2, (set' $ y));
  1267                 val concl = HOLogic.mk_Trueprop (phi $ z1 $ z2);
  1268               in
  1269                 fold_rev Logic.all [z1, z2] (Logic.list_implies ([prem1, prem2], concl))
  1270               end;
  1271 
  1272             val IHs = @{map 5} mk_IH phi2s (drop m sets) (drop m sets') Izs1 Izs2;
  1273             val concl = HOLogic.mk_Trueprop (phi $ (ctor $ x) $ (ctor' $ y));
  1274           in
  1275             fold_rev Logic.all [x, y] (Logic.list_implies (IHs, concl))
  1276           end;
  1277 
  1278         val prems = @{map 7} mk_prem phi2s ctors ctor's FTs_setss FTs'_setss xFs yFs;
  1279 
  1280         fun mk_concl phi z1 z2 = phi $ z1 $ z2;
  1281         val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  1282           (@{map 3} mk_concl phi2s Izs1 Izs2));
  1283         fun mk_t phi (z1, z1') (z2, z2') =
  1284           Term.absfree z1' (HOLogic.mk_all (fst z2', snd z2', phi $ z1 $ z2));
  1285         val cts = @{map 3} (SOME o Thm.cterm_of lthy ooo mk_t) phi2s (Izs1 ~~ Izs1') (Izs2 ~~ Izs2');
  1286         val goal = Logic.list_implies (prems, concl);
  1287         val vars = Variable.add_free_names lthy goal [];
  1288       in
  1289         (Goal.prove_sorry lthy vars [] goal
  1290           (fn {context = ctxt, prems = _} => mk_ctor_induct2_tac ctxt cTs cts ctor_induct_thm
  1291             weak_ctor_induct_thms)
  1292         |> Thm.close_derivation,
  1293         rev (Term.add_tfrees goal []))
  1294       end;
  1295 
  1296     val timer = time (timer "induction");
  1297 
  1298     fun mk_ctor_map_DEADID_thm ctor_inject map_id0 =
  1299       trans OF [id_apply, iffD2 OF [ctor_inject, map_id0 RS sym]];
  1300 
  1301     fun mk_ctor_map_unique_DEADID_thm () =
  1302       let
  1303         val (funs, algs) =
  1304           HOLogic.conjuncts (HOLogic.dest_Trueprop (Thm.concl_of ctor_fold_unique_thm))
  1305           |> map_split HOLogic.dest_eq
  1306           ||>  snd o strip_comb o hd
  1307           |> @{apply 2} (map (fst o dest_Var));
  1308         fun mk_fun_insts T ix = Thm.cterm_of lthy (Var (ix, T --> T));
  1309         val theta =
  1310           (funs ~~ @{map 2} mk_fun_insts Ts funs) @ (algs ~~ map (Thm.cterm_of lthy) ctors);
  1311         val ctor_fold_ctors = (ctor_fold_unique_thm OF
  1312           map (fn thm => mk_trans @{thm id_o} (mk_sym (thm RS
  1313             @{thm trans[OF arg_cong2[of _ _ _ _ "op o", OF refl] o_id]}))) map_id0s)
  1314           |> split_conj_thm |> map mk_sym;
  1315       in
  1316         infer_instantiate lthy theta ctor_fold_unique_thm
  1317         |> unfold_thms lthy ctor_fold_ctors
  1318         |> Morphism.thm (Local_Theory.target_morphism lthy)
  1319       end;
  1320 
  1321     fun mk_ctor_Irel_DEADID_thm ctor_inject bnf =
  1322       trans OF [ctor_inject, rel_eq_of_bnf bnf RS @{thm predicate2_eqD} RS sym];
  1323 
  1324     val IphiTs = map2 mk_pred2T passiveAs passiveBs;
  1325     val Ipsi1Ts = map2 mk_pred2T passiveAs passiveCs;
  1326     val Ipsi2Ts = map2 mk_pred2T passiveCs passiveBs;
  1327     val activephiTs = map2 mk_pred2T activeAs activeBs;
  1328     val activeIphiTs = map2 mk_pred2T Ts Ts';
  1329 
  1330     val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
  1331 
  1332     (*register new datatypes as BNFs*)
  1333     val (timer, Ibnfs, (ctor_Imap_o_thms, ctor_Imap_thms), ctor_Imap_unique_thm, ctor_Iset_thmss',
  1334         ctor_Irel_thms, Ibnf_notes, lthy) =
  1335       if m = 0 then
  1336         (timer, replicate n DEADID_bnf,
  1337         map_split (`(mk_pointfree lthy)) (map2 mk_ctor_map_DEADID_thm ctor_inject_thms map_ids),
  1338         mk_ctor_map_unique_DEADID_thm (),
  1339         replicate n [], map2 mk_ctor_Irel_DEADID_thm ctor_inject_thms bnfs, [], lthy)
  1340       else let
  1341         val fTs = map2 (curry op -->) passiveAs passiveBs;
  1342         val uTs = map2 (curry op -->) Ts Ts';
  1343 
  1344         val ((((fs, fs'), (AFss, AFss')), (ys, ys')), _) =
  1345           lthy
  1346           |> mk_Frees' "f" fTs
  1347           ||>> mk_Freess' "z" setFTss
  1348           ||>> mk_Frees' "y" passiveAs;
  1349 
  1350         val map_FTFT's = map2 (fn Ds =>
  1351           mk_map_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
  1352         fun mk_passive_maps ATs BTs Ts =
  1353           map2 (fn Ds => mk_map_of_bnf Ds (ATs @ Ts) (BTs @ Ts)) Dss bnfs;
  1354         fun mk_map_fold_arg fs Ts ctor fmap =
  1355           HOLogic.mk_comp (ctor, Term.list_comb (fmap, fs @ map HOLogic.id_const Ts));
  1356         fun mk_map Ts fs Ts' ctors mk_maps =
  1357           mk_fold Ts (map2 (mk_map_fold_arg fs Ts') ctors (mk_maps Ts'));
  1358         val pmapsABT' = mk_passive_maps passiveAs passiveBs;
  1359         val fs_maps = map (mk_map Ts fs Ts' ctor's pmapsABT') ks;
  1360 
  1361         val ls = 1 upto m;
  1362         val setsss = map (mk_setss o mk_set_Ts) passiveAs;
  1363 
  1364         fun mk_col l T z z' sets =
  1365           let
  1366             fun mk_UN set = mk_Union T $ (set $ z);
  1367           in
  1368             Term.absfree z'
  1369               (mk_union (nth sets (l - 1) $ z,
  1370                 Library.foldl1 mk_union (map mk_UN (drop m sets))))
  1371           end;
  1372 
  1373         val colss = @{map 5} (fn l => fn T => @{map 3} (mk_col l T)) ls passiveAs AFss AFss' setsss;
  1374         val setss_by_range = map (fn cols => map (mk_fold Ts cols) ks) colss;
  1375         val setss_by_bnf = transpose setss_by_range;
  1376 
  1377         val set_bss =
  1378           map (flat o map2 (fn B => fn b =>
  1379             if member (op =) deads (TFree B) then [] else [b]) resBs) set_bss0;
  1380 
  1381         val ctor_witss =
  1382           let
  1383             val witss = map2 (fn Ds => fn bnf => mk_wits_of_bnf
  1384               (replicate (nwits_of_bnf bnf) Ds)
  1385               (replicate (nwits_of_bnf bnf) (passiveAs @ Ts)) bnf) Dss bnfs;
  1386             fun close_wit (I, wit) = fold_rev Term.absfree (map (nth ys') I) wit;
  1387             fun wit_apply (arg_I, arg_wit) (fun_I, fun_wit) =
  1388               (union (op =) arg_I fun_I, fun_wit $ arg_wit);
  1389 
  1390             fun gen_arg support i =
  1391               if i < m then [([i], nth ys i)]
  1392               else maps (mk_wit support (nth ctors (i - m)) (i - m)) (nth support (i - m))
  1393             and mk_wit support ctor i (I, wit) =
  1394               let val args = map (gen_arg (nth_map i (remove (op =) (I, wit)) support)) I;
  1395               in
  1396                 (args, [([], wit)])
  1397                 |-> fold (map_product wit_apply)
  1398                 |> map (apsnd (fn t => ctor $ t))
  1399                 |> minimize_wits
  1400               end;
  1401           in
  1402             @{map 3} (fn ctor => fn i => map close_wit o minimize_wits o maps (mk_wit witss ctor i))
  1403               ctors (0 upto n - 1) witss
  1404           end;
  1405 
  1406         val (lthy, sbd0, sbd0_card_order, sbd0_Cinfinite, set_sbd0ss) =
  1407           if n = 1
  1408           then (lthy, hd bd0s, hd bd0_card_orders, hd bd0_Cinfinites, set_bd0ss)
  1409           else
  1410             let
  1411               val sum_bd0 = Library.foldr1 (uncurry mk_csum) bd0s;
  1412               val sum_bd0T = fst (dest_relT (fastype_of sum_bd0));
  1413               val (sum_bd0T_params, sum_bd0T_params') = `(map TFree) (Term.add_tfreesT sum_bd0T []);
  1414 
  1415               val sbd0T_bind = mk_internal_b (sum_bdTN ^ "0");
  1416 
  1417               val ((sbd0T_name, (sbd0T_glob_info, sbd0T_loc_info)), lthy) =
  1418                 typedef (sbd0T_bind, sum_bd0T_params', NoSyn)
  1419                   (HOLogic.mk_UNIV sum_bd0T) NONE (fn ctxt =>
  1420                     EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy;
  1421 
  1422               val sbd0T = Type (sbd0T_name, sum_bd0T_params);
  1423               val Abs_sbd0T = Const (#Abs_name sbd0T_glob_info, sum_bd0T --> sbd0T);
  1424 
  1425               val sbd0_bind = mk_internal_b (sum_bdN ^ "0");
  1426               val sbd0_def_bind = (Thm.def_binding sbd0_bind, []);
  1427 
  1428               val sbd0_spec = mk_dir_image sum_bd0 Abs_sbd0T;
  1429 
  1430               val ((sbd0_free, (_, sbd0_def_free)), (lthy, lthy_old)) =
  1431                 lthy
  1432                 |> Local_Theory.open_target |> snd
  1433                 |> Local_Theory.define ((sbd0_bind, NoSyn), (sbd0_def_bind, sbd0_spec))
  1434                 ||> `Local_Theory.close_target;
  1435 
  1436               val phi = Proof_Context.export_morphism lthy_old lthy;
  1437 
  1438               val sbd0_def = Morphism.thm phi sbd0_def_free RS meta_eq_to_obj_eq;
  1439               val sbd0 = Const (fst (Term.dest_Const (Morphism.term phi sbd0_free)),
  1440                 mk_relT (`I sbd0T));
  1441 
  1442               val Abs_sbd0T_inj = mk_Abs_inj_thm (#Abs_inject sbd0T_loc_info);
  1443               val Abs_sbd0T_bij = mk_Abs_bij_thm lthy Abs_sbd0T_inj (#Abs_cases sbd0T_loc_info);
  1444 
  1445               val sum_Cinfinite = mk_sum_Cinfinite bd0_Cinfinites;
  1446               val sum_Card_order = sum_Cinfinite RS conjunct2;
  1447               val sum_card_order = mk_sum_card_order bd0_card_orders;
  1448 
  1449               val sbd0_ordIso = @{thm ssubst_Pair_rhs} OF
  1450                 [@{thm dir_image} OF [Abs_sbd0T_inj, sum_Card_order], sbd0_def];
  1451               val sbd0_Cinfinite = @{thm Cinfinite_cong} OF [sbd0_ordIso, sum_Cinfinite];
  1452 
  1453               val sbd0_card_order = @{thm iffD2[OF arg_cong[of _ _ card_order]]} OF
  1454                 [sbd0_def, @{thm card_order_dir_image} OF [Abs_sbd0T_bij, sum_card_order]];
  1455 
  1456               fun mk_set_sbd0 i bd0_Card_order bd0s =
  1457                 map (fn thm => @{thm ordLeq_ordIso_trans} OF
  1458                   [bd0_Card_order RS mk_ordLeq_csum n i thm, sbd0_ordIso]) bd0s;
  1459               val set_sbd0ss = @{map 3} mk_set_sbd0 ks bd0_Card_orders set_bd0ss;
  1460             in
  1461               (lthy, sbd0, sbd0_card_order, sbd0_Cinfinite, set_sbd0ss)
  1462             end;
  1463 
  1464         val (Ibnf_consts, lthy) =
  1465           @{fold_map 9} (fn b => fn map_b => fn rel_b => fn pred_b => fn set_bs => fn mapx =>
  1466               fn sets => fn wits => fn T => fn lthy =>
  1467             define_bnf_consts Hardly_Inline (user_policy Note_Some lthy) false (SOME deads)
  1468               map_b rel_b pred_b set_bs
  1469               (((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd0), wits), NONE), NONE) lthy)
  1470           bs map_bs rel_bs pred_bs set_bss fs_maps setss_by_bnf ctor_witss Ts lthy;
  1471 
  1472         val ((((((((((((((Izs, (Izs1, Izs1')), (Izs2, Izs2')), xFs), yFs))), Iphis), Ipsi1s),
  1473             Ipsi2s), fs), fs_copy), us), (ys, ys')), _) =
  1474           lthy
  1475           |> mk_Frees "z" Ts
  1476           ||>> mk_Frees' "z1" Ts
  1477           ||>> mk_Frees' "z2" Ts'
  1478           ||>> mk_Frees "x" FTs
  1479           ||>> mk_Frees "y" FTs'
  1480           ||>> mk_Frees "R" IphiTs
  1481           ||>> mk_Frees "R" Ipsi1Ts
  1482           ||>> mk_Frees "Q" Ipsi2Ts
  1483           ||>> mk_Frees "f" fTs
  1484           ||>> mk_Frees "f" fTs
  1485           ||>> mk_Frees "u" uTs
  1486           ||>> mk_Frees' "y" passiveAs;
  1487 
  1488         val (_, Iconsts, Iconst_defs, mk_Iconsts) = @{split_list 4} Ibnf_consts;
  1489         val (_, Isetss, Ibds_Ds, Iwitss_Ds, _, _) = @{split_list 6} Iconsts;
  1490         val (Imap_defs, Iset_defss, Ibd_defs, Iwit_defss, Irel_defs, Ipred_defs) =
  1491           @{split_list 6} Iconst_defs;
  1492         val (mk_Imaps_Ds, mk_It_Ds, _, mk_Irels_Ds, mk_Ipreds_Ds, _, _) =
  1493           @{split_list 7} mk_Iconsts;
  1494 
  1495         val Irel_unabs_defs = map (fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) Irel_defs;
  1496         val Ipred_unabs_defs = map (fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) Ipred_defs;
  1497         val Iset_defs = flat Iset_defss;
  1498 
  1499         fun mk_Imaps As Bs = map (fn mk => mk deads As Bs) mk_Imaps_Ds;
  1500         fun mk_Isetss As = map2 (fn mk => fn Isets => map (mk deads As) Isets) mk_It_Ds Isetss;
  1501         val Ibds = map2 (fn mk => mk deads passiveAs) mk_It_Ds Ibds_Ds;
  1502         val Iwitss =
  1503           map2 (fn mk => fn Iwits => map (mk deads passiveAs o snd) Iwits) mk_It_Ds Iwitss_Ds;
  1504         fun mk_Irels As Bs = map (fn mk => mk deads As Bs) mk_Irels_Ds;
  1505         fun mk_Ipreds As = map (fn mk => mk deads As) mk_Ipreds_Ds;
  1506 
  1507         val Imaps = mk_Imaps passiveAs passiveBs;
  1508         val fs_Imaps = map (fn m => Term.list_comb (m, fs)) Imaps;
  1509         val fs_copy_Imaps = map (fn m => Term.list_comb (m, fs_copy)) Imaps;
  1510         val (Isetss_by_range, Isetss_by_bnf) = `transpose (mk_Isetss passiveAs);
  1511 
  1512         val map_setss = map (fn T => map2 (fn Ds =>
  1513           mk_map_of_bnf Ds (passiveAs @ Ts) (mk_set_Ts T)) Dss bnfs) passiveAs;
  1514 
  1515         val timer = time (timer "bnf constants for the new datatypes");
  1516 
  1517         val (ctor_Imap_thms, ctor_Imap_o_thms) =
  1518           let
  1519             fun mk_goal fs_map map ctor ctor' =
  1520               mk_Trueprop_eq (HOLogic.mk_comp (fs_map, ctor),
  1521                 HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ fs_Imaps)));
  1522             val goals = @{map 4} mk_goal fs_Imaps map_FTFT's ctors ctor's;
  1523             val maps =
  1524               @{map 4} (fn goal => fn foldx => fn map_comp_id => fn map_cong0 =>
  1525                 Variable.add_free_names lthy goal []
  1526                 |> (fn vars => Goal.prove_sorry lthy vars [] goal
  1527                   (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Imap_defs THEN
  1528                     mk_map_tac ctxt m n foldx map_comp_id map_cong0))
  1529                 |> Thm.close_derivation)
  1530               goals ctor_fold_thms map_comp_id_thms map_cong0s;
  1531           in
  1532             `(map (fn thm => thm RS @{thm comp_eq_dest})) maps
  1533           end;
  1534 
  1535         val (ctor_Imap_unique_thms, ctor_Imap_unique_thm) =
  1536           let
  1537             fun mk_prem u map ctor ctor' =
  1538               mk_Trueprop_eq (HOLogic.mk_comp (u, ctor),
  1539                 HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ us)));
  1540             val prems = @{map 4} mk_prem us map_FTFT's ctors ctor's;
  1541             val goal =
  1542               HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  1543                 (map2 (curry HOLogic.mk_eq) us fs_Imaps));
  1544             val vars = fold (Variable.add_free_names lthy) (goal :: prems) [];
  1545             val unique = Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, goal))
  1546               (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Imap_defs THEN
  1547                 mk_ctor_map_unique_tac ctxt ctor_fold_unique_thm sym_map_comps)
  1548               |> Thm.close_derivation;
  1549           in
  1550             `split_conj_thm unique
  1551           end;
  1552 
  1553         val timer = time (timer "map functions for the new datatypes");
  1554 
  1555         val ctor_Iset_thmss =
  1556           let
  1557             fun mk_goal sets ctor set col map =
  1558               mk_Trueprop_eq (HOLogic.mk_comp (set, ctor),
  1559                 HOLogic.mk_comp (col, Term.list_comb (map, passive_ids @ sets)));
  1560             val goalss =
  1561               @{map 3} (fn sets => @{map 4} (mk_goal sets) ctors sets)
  1562                 Isetss_by_range colss map_setss;
  1563             val setss = map (map2 (fn foldx => fn goal =>
  1564                 Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
  1565                   unfold_thms_tac ctxt Iset_defs THEN mk_set_tac ctxt foldx)
  1566                 |> Thm.close_derivation)
  1567               ctor_fold_thms) goalss;
  1568 
  1569             fun mk_simp_goal pas_set act_sets sets ctor z set =
  1570               mk_Trueprop_eq (set $ (ctor $ z),
  1571                 mk_union (pas_set $ z,
  1572                   Library.foldl1 mk_union (map2 (fn X => mk_UNION (X $ z)) act_sets sets)));
  1573             val simp_goalss =
  1574               map2 (fn i => fn sets =>
  1575                 @{map 4} (fn Fsets => mk_simp_goal (nth Fsets (i - 1)) (drop m Fsets) sets)
  1576                   FTs_setss ctors xFs sets)
  1577                 ls Isetss_by_range;
  1578 
  1579             val ctor_setss = @{map 3} (fn i => @{map 3} (fn set_nats => fn goal => fn set =>
  1580               Variable.add_free_names lthy goal []
  1581               |> (fn vars => Goal.prove_sorry lthy vars [] goal
  1582                   (fn {context = ctxt, prems = _} =>
  1583                     mk_ctor_set_tac ctxt set (nth set_nats (i - 1)) (drop m set_nats)))
  1584                 |> Thm.close_derivation)
  1585               set_mapss) ls simp_goalss setss;
  1586           in
  1587             ctor_setss
  1588           end;
  1589 
  1590         fun mk_set_thms ctor_set = (@{thm xt1(3)} OF [ctor_set, @{thm Un_upper1}]) ::
  1591           map (fn i => (@{thm xt1(3)} OF [ctor_set, @{thm Un_upper2}]) RS
  1592             (mk_Un_upper n i RS subset_trans) RSN
  1593             (2, @{thm UN_upper} RS subset_trans))
  1594             (1 upto n);
  1595         val set_Iset_thmsss = transpose (map (map mk_set_thms) ctor_Iset_thmss);
  1596 
  1597         val timer = time (timer "set functions for the new datatypes");
  1598 
  1599         val cxs = map (SOME o Thm.cterm_of lthy) Izs;
  1600         val Isetss_by_range' =
  1601           map (map (Term.subst_atomic_types (passiveAs ~~ passiveBs))) Isetss_by_range;
  1602 
  1603         val Iset_Imap0_thmss =
  1604           let
  1605             fun mk_set_map0 f map z set set' =
  1606               HOLogic.mk_eq (mk_image f $ (set $ z), set' $ (map $ z));
  1607 
  1608             fun mk_cphi f map z set set' = Thm.cterm_of lthy
  1609               (Term.absfree (dest_Free z) (mk_set_map0 f map z set set'));
  1610 
  1611             val csetss = map (map (Thm.cterm_of lthy)) Isetss_by_range';
  1612 
  1613             val cphiss = @{map 3} (fn f => fn sets => fn sets' =>
  1614               (@{map 4} (mk_cphi f) fs_Imaps Izs sets sets')) fs Isetss_by_range Isetss_by_range';
  1615 
  1616             val inducts = map (fn cphis =>
  1617               Thm.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss;
  1618 
  1619             val goals =
  1620               @{map 3} (fn f => fn sets => fn sets' =>
  1621                 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  1622                   (@{map 4} (mk_set_map0 f) fs_Imaps Izs sets sets')))
  1623                   fs Isetss_by_range Isetss_by_range';
  1624 
  1625             fun mk_tac ctxt induct = mk_set_nat_tac ctxt m (rtac ctxt induct) set_mapss ctor_Imap_thms;
  1626             val thms =
  1627               @{map 5} (fn goal => fn csets => fn ctor_sets => fn induct => fn i =>
  1628                 Variable.add_free_names lthy goal []
  1629                 |> (fn vars => Goal.prove_sorry lthy vars [] goal
  1630                   (fn {context = ctxt, prems = _} => mk_tac ctxt induct csets ctor_sets i))
  1631                 |> Thm.close_derivation)
  1632               goals csetss ctor_Iset_thmss inducts ls;
  1633           in
  1634             map split_conj_thm thms
  1635           end;
  1636 
  1637         val Iset_bd_thmss =
  1638           let
  1639             fun mk_set_bd z bd set = mk_ordLeq (mk_card_of (set $ z)) bd;
  1640 
  1641             fun mk_cphi z set = Thm.cterm_of lthy (Term.absfree (dest_Free z) (mk_set_bd z sbd0 set));
  1642 
  1643             val cphiss = map (map2 mk_cphi Izs) Isetss_by_range;
  1644 
  1645             val inducts = map (fn cphis =>
  1646               Thm.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss;
  1647 
  1648             val goals =
  1649               map (fn sets =>
  1650                 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  1651                   (@{map 3} mk_set_bd Izs Ibds sets))) Isetss_by_range;
  1652 
  1653             fun mk_tac ctxt induct = mk_set_bd_tac ctxt m (rtac ctxt induct) sbd0_Cinfinite set_sbd0ss;
  1654             val thms =
  1655               @{map 4} (fn goal => fn ctor_sets => fn induct => fn i =>
  1656                 Variable.add_free_names lthy goal []
  1657                 |> (fn vars => Goal.prove_sorry lthy vars [] goal
  1658                     (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Ibd_defs THEN
  1659                       mk_tac ctxt induct ctor_sets i))
  1660                 |> Thm.close_derivation)
  1661               goals ctor_Iset_thmss inducts ls;
  1662           in
  1663             map split_conj_thm thms
  1664           end;
  1665 
  1666         val Imap_cong0_thms =
  1667           let
  1668             fun mk_prem z set f g y y' =
  1669               mk_Ball (set $ z) (Term.absfree y' (HOLogic.mk_eq (f $ y, g $ y)));
  1670 
  1671             fun mk_map_cong0 sets z fmap gmap =
  1672               HOLogic.mk_imp
  1673                 (Library.foldr1 HOLogic.mk_conj (@{map 5} (mk_prem z) sets fs fs_copy ys ys'),
  1674                 HOLogic.mk_eq (fmap $ z, gmap $ z));
  1675 
  1676             fun mk_cphi sets z fmap gmap =
  1677               Thm.cterm_of lthy (Term.absfree (dest_Free z) (mk_map_cong0 sets z fmap gmap));
  1678 
  1679             val cphis = @{map 4} mk_cphi Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps;
  1680 
  1681             val induct = Thm.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm;
  1682 
  1683             val goal =
  1684               HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  1685                 (@{map 4} mk_map_cong0 Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps));
  1686             val vars = Variable.add_free_names lthy goal [];
  1687 
  1688             val thm = Goal.prove_sorry lthy vars [] goal
  1689                 (fn {context = ctxt, prems = _} => mk_mcong_tac ctxt (rtac ctxt induct) set_Iset_thmsss
  1690                   map_cong0s ctor_Imap_thms)
  1691               |> Thm.close_derivation;
  1692           in
  1693             split_conj_thm thm
  1694           end;
  1695 
  1696         val in_rels = map in_rel_of_bnf bnfs;
  1697         val in_Irels = map (fn def => trans OF [def, @{thm OO_Grp_alt}] RS @{thm predicate2_eqD})
  1698             Irel_unabs_defs;
  1699 
  1700         val ctor_Iset_incl_thmss = map (map hd) set_Iset_thmsss;
  1701         val ctor_set_Iset_incl_thmsss = map (transpose o map tl) set_Iset_thmsss;
  1702         val ctor_Iset_thmss' = transpose ctor_Iset_thmss;
  1703 
  1704         val Irels = mk_Irels passiveAs passiveBs;
  1705         val Ipreds = mk_Ipreds passiveAs;
  1706         val Irelphis = map (fn rel => Term.list_comb (rel, Iphis)) Irels;
  1707         val relphis = map (fn rel => Term.list_comb (rel, Iphis @ Irelphis)) rels;
  1708         val Irelpsi1s = map (fn rel => Term.list_comb (rel, Ipsi1s)) (mk_Irels passiveAs passiveCs);
  1709         val Irelpsi2s = map (fn rel => Term.list_comb (rel, Ipsi2s)) (mk_Irels passiveCs passiveBs);
  1710         val Irelpsi12s = map (fn rel =>
  1711             Term.list_comb (rel, map2 (curry mk_rel_compp) Ipsi1s Ipsi2s)) Irels;
  1712 
  1713         val ctor_Irel_thms =
  1714           let
  1715             fun mk_goal xF yF ctor ctor' Irelphi relphi =
  1716               mk_Trueprop_eq (Irelphi $ (ctor $ xF) $ (ctor' $ yF), relphi $ xF $ yF);
  1717             val goals = @{map 6} mk_goal xFs yFs ctors ctor's Irelphis relphis;
  1718           in
  1719             @{map 12} (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 =>
  1720               fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor =>
  1721               fn set_map0s => fn ctor_set_incls => fn ctor_set_set_inclss =>
  1722               Variable.add_free_names lthy goal []
  1723               |> (fn vars => Goal.prove_sorry lthy vars [] goal
  1724                (fn {context = ctxt, prems = _} =>
  1725                  mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets
  1726                    ctor_inject ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss))
  1727               |> Thm.close_derivation)
  1728             ks goals in_rels map_comps map_cong0s ctor_Imap_thms ctor_Iset_thmss'
  1729               ctor_inject_thms ctor_dtor_thms set_mapss ctor_Iset_incl_thmss
  1730               ctor_set_Iset_incl_thmsss
  1731           end;
  1732 
  1733         val le_Irel_OO_thm =
  1734           let
  1735             fun mk_le_Irel_OO Irelpsi1 Irelpsi2 Irelpsi12 Iz1 Iz2 =
  1736               HOLogic.mk_imp (mk_rel_compp (Irelpsi1, Irelpsi2) $ Iz1 $ Iz2,
  1737                 Irelpsi12 $ Iz1 $ Iz2);
  1738             val goals = @{map 5} mk_le_Irel_OO Irelpsi1s Irelpsi2s Irelpsi12s Izs1 Izs2;
  1739 
  1740             val cTs = map (SOME o Thm.ctyp_of lthy o TFree) induct2_params;
  1741             val cxs = map (SOME o Thm.cterm_of lthy) (splice Izs1 Izs2);
  1742             fun mk_cphi z1 z2 goal = SOME (Thm.cterm_of lthy (Term.absfree z1 (Term.absfree z2 goal)));
  1743             val cphis = @{map 3} mk_cphi Izs1' Izs2' goals;
  1744             val induct = Thm.instantiate' cTs (cphis @ cxs) ctor_induct2_thm;
  1745 
  1746             val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals);
  1747             val vars = Variable.add_free_names lthy goal [];
  1748           in
  1749             Goal.prove_sorry lthy vars [] goal
  1750               (fn {context = ctxt, prems = _} => mk_le_rel_OO_tac ctxt m induct ctor_nchotomy_thms
  1751                 ctor_Irel_thms rel_mono_strong0s le_rel_OOs)
  1752             |> Thm.close_derivation
  1753           end;
  1754 
  1755         val timer = time (timer "helpers for BNF properties");
  1756 
  1757         val map_id0_tacs = map (fn thm => fn ctxt => mk_map_id0_tac ctxt map_id0s thm)
  1758           ctor_Imap_unique_thms;
  1759         val map_comp0_tacs =
  1760           map2 (fn thm => fn i => fn ctxt =>
  1761             mk_map_comp0_tac ctxt map_comps ctor_Imap_thms thm i)
  1762           ctor_Imap_unique_thms ks;
  1763         val map_cong0_tacs = map (fn thm => fn ctxt => mk_map_cong0_tac ctxt m thm) Imap_cong0_thms;
  1764         val set_map0_tacss = map (map (fn thm => fn ctxt => mk_set_map0_tac ctxt thm))
  1765           (transpose Iset_Imap0_thmss);
  1766         val bd_co_tacs = replicate n (fn ctxt =>
  1767           unfold_thms_tac ctxt Ibd_defs THEN rtac ctxt sbd0_card_order 1);
  1768         val bd_cinf_tacs = replicate n (fn ctxt =>
  1769           unfold_thms_tac ctxt Ibd_defs THEN rtac ctxt (sbd0_Cinfinite RS conjunct1) 1);
  1770         val set_bd_tacss = map (map (fn thm => fn ctxt => rtac ctxt thm 1)) (transpose Iset_bd_thmss);
  1771         val le_rel_OO_tacs = map (fn i => fn ctxt =>
  1772           (rtac ctxt @{thm predicate2I} THEN' etac ctxt (le_Irel_OO_thm RS mk_conjunctN n i RS mp)) 1) ks;
  1773 
  1774         val rel_OO_Grp_tacs = map (fn def => fn ctxt => rtac ctxt def 1) Irel_unabs_defs;
  1775 
  1776         val pred_set_tacs = map (fn def => fn ctxt => rtac ctxt def 1) Ipred_unabs_defs;
  1777 
  1778         val tacss = @{map 10} zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss
  1779           bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs pred_set_tacs;
  1780 
  1781         fun wit_tac ctxt = unfold_thms_tac ctxt (flat Iwit_defss) THEN
  1782           mk_wit_tac ctxt n (flat ctor_Iset_thmss) (maps wit_thms_of_bnf bnfs);
  1783 
  1784         val (Ibnfs, lthy) =
  1785           @{fold_map 6} (fn tacs => fn map_b => fn rel_b => fn pred_b => fn set_bs => fn consts =>
  1786             bnf_def Do_Inline (user_policy Note_Some) false I tacs wit_tac (SOME deads)
  1787               map_b rel_b pred_b set_bs consts)
  1788           tacss map_bs rel_bs pred_bs set_bss
  1789             (((((((replicate n Binding.empty ~~ Ts) ~~ Imaps) ~~ Isetss_by_bnf) ~~ Ibds) ~~
  1790               Iwitss) ~~ map SOME Irels) ~~ map SOME Ipreds) lthy;
  1791 
  1792         val timer = time (timer "registered new datatypes as BNFs");
  1793 
  1794         val ls' = if m = 1 then [0] else ls
  1795 
  1796         val Ibnf_common_notes =
  1797           [(ctor_map_uniqueN, [ctor_Imap_unique_thm])]
  1798           |> map (fn (thmN, thms) =>
  1799             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
  1800 
  1801         val Ibnf_notes =
  1802           [(ctor_mapN, map single ctor_Imap_thms),
  1803           (ctor_relN, map single ctor_Irel_thms),
  1804           (ctor_set_inclN, ctor_Iset_incl_thmss),
  1805           (ctor_set_set_inclN, map flat ctor_set_Iset_incl_thmsss)] @
  1806           map2 (fn i => fn thms => (mk_ctor_setN i, map single thms)) ls' ctor_Iset_thmss
  1807           |> maps (fn (thmN, thmss) =>
  1808             map2 (fn b => fn thms =>
  1809               ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
  1810             bs thmss)
  1811       in
  1812         (timer, Ibnfs, (ctor_Imap_o_thms, ctor_Imap_thms), ctor_Imap_unique_thm, ctor_Iset_thmss',
  1813           ctor_Irel_thms, Ibnf_common_notes @ Ibnf_notes, lthy)
  1814       end;
  1815 
  1816     val ((((((xFs, yFs)), Iphis), activephis), activeIphis), _) =
  1817       lthy
  1818       |> mk_Frees "x" FTs
  1819       ||>> mk_Frees "y" FTs'
  1820       ||>> mk_Frees "R" IphiTs
  1821       ||>> mk_Frees "S" activephiTs
  1822       ||>> mk_Frees "IR" activeIphiTs;
  1823 
  1824     val ctor_fold_o_Imap_thms = mk_xtor_co_iter_o_map_thms Least_FP false m ctor_fold_unique_thm
  1825       ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_fold_thms) sym_map_comps map_cong0s;
  1826 
  1827     val Irels = if m = 0 then map HOLogic.eq_const Ts
  1828       else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;
  1829     val Irel_induct_thm =
  1830       mk_xtor_rel_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's
  1831         (fn {context = ctxt, prems = IHs} => mk_rel_induct_tac ctxt IHs m ctor_induct2_thm ks
  1832            ctor_Irel_thms rel_mono_strong0s) lthy;
  1833 
  1834     val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
  1835     val ctor_fold_transfer_thms =
  1836       mk_xtor_co_iter_transfer_thms Least_FP rels activephis activephis Irels Iphis
  1837         (mk_folds passiveAs activeAs) (mk_folds passiveBs activeBs)
  1838         (fn {context = ctxt, prems = _} => mk_fold_transfer_tac ctxt m Irel_induct_thm
  1839           (map map_transfer_of_bnf bnfs) ctor_fold_thms)
  1840         lthy;
  1841 
  1842     val timer = time (timer "relator induction");
  1843 
  1844     fun mk_Ts As = map (typ_subst_atomic (passiveAs ~~ As)) Ts;
  1845     val export = map (Morphism.term (Local_Theory.target_morphism lthy))
  1846     val ((recs, (ctor_rec_thms, ctor_rec_unique_thm, ctor_rec_o_Imap_thms, ctor_rec_transfer_thms)),
  1847         lthy) = lthy
  1848       |> derive_xtor_co_recs Least_FP external_bs mk_Ts (Dss, resDs) bnfs
  1849         (export ctors) (export folds)
  1850         ctor_fold_unique_thm ctor_fold_thms ctor_fold_transfer_thms ctor_Imap_thms ctor_Irel_thms;
  1851 
  1852     val timer = time (timer "recursor");
  1853 
  1854     val common_notes =
  1855       [(ctor_inductN, [ctor_induct_thm]),
  1856       (ctor_induct2N, [ctor_induct2_thm]),
  1857       (ctor_rel_inductN, [Irel_induct_thm])]
  1858       |> map (fn (thmN, thms) =>
  1859         ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
  1860 
  1861     val notes =
  1862       [(ctor_dtorN, ctor_dtor_thms),
  1863       (ctor_exhaustN, ctor_exhaust_thms),
  1864       (ctor_foldN, ctor_fold_thms),
  1865       (ctor_fold_o_mapN, ctor_fold_o_Imap_thms),
  1866       (ctor_fold_transferN, ctor_fold_transfer_thms),
  1867       (ctor_fold_uniqueN, ctor_fold_unique_thms),
  1868       (ctor_injectN, ctor_inject_thms),
  1869       (dtor_ctorN, dtor_ctor_thms),
  1870       (dtor_exhaustN, dtor_exhaust_thms),
  1871       (dtor_injectN, dtor_inject_thms)]
  1872       |> map (apsnd (map single))
  1873       |> maps (fn (thmN, thmss) =>
  1874         map2 (fn b => fn thms =>
  1875           ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
  1876         bs thmss);
  1877 
  1878     val lthy' = lthy |> internals ? snd o Local_Theory.notes (common_notes @ notes @ Ibnf_notes);
  1879 
  1880     val fp_res =
  1881       {Ts = Ts, bnfs = Ibnfs, pre_bnfs = bnfs, absT_infos = absT_infos,
  1882        ctors = ctors, dtors = dtors, xtor_un_folds_legacy = folds, xtor_co_recs = export recs,
  1883        xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
  1884        ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms,
  1885        dtor_injects = dtor_inject_thms, xtor_maps = ctor_Imap_thms,
  1886        xtor_map_unique = ctor_Imap_unique_thm, xtor_setss = ctor_Iset_thmss',
  1887        xtor_rels = ctor_Irel_thms, xtor_un_fold_thms_legacy = ctor_fold_thms,
  1888        xtor_co_rec_thms = ctor_rec_thms, xtor_un_fold_unique_legacy = ctor_fold_unique_thm,
  1889        xtor_co_rec_unique = ctor_rec_unique_thm,
  1890        xtor_un_fold_o_maps_legacy = ctor_fold_o_Imap_thms,
  1891        xtor_co_rec_o_maps = ctor_rec_o_Imap_thms,
  1892        xtor_un_fold_transfers_legacy = ctor_fold_transfer_thms,
  1893        xtor_co_rec_transfers = ctor_rec_transfer_thms, xtor_rel_co_induct = Irel_induct_thm,
  1894        dtor_set_inducts = []};
  1895   in
  1896     timer; (fp_res, lthy')
  1897   end;
  1898 
  1899 val _ =
  1900   Outer_Syntax.local_theory @{command_keyword datatype} "define inductive datatypes"
  1901     (parse_co_datatype_cmd Least_FP construct_lfp);
  1902 
  1903 val _ = Theory.setup (fp_antiquote_setup @{binding datatype});
  1904 
  1905 end;