src/HOL/Codatatype/Tools/bnf_lfp.ML
author blanchet
Tue Sep 11 18:39:47 2012 +0200 (2012-09-11)
changeset 49286 dde4967c9233
parent 49277 aee77001243f
child 49308 6190b701e4f4
permissions -rw-r--r--
added "defaults" option
     1 (*  Title:      HOL/Codatatype/Tools/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 bnf_lfp: mixfix list -> (string * sort) list option -> binding list ->
    12     typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
    13     (term list * term list * term list * term list * thm list * thm list * thm list * thm list *
    14       thm list) * 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_FP_Util
    24 open BNF_LFP_Util
    25 open BNF_LFP_Tactics
    26 
    27 (*all bnfs have the same lives*)
    28 fun bnf_lfp mixfixes resBs bs (resDs, Dss) bnfs lthy =
    29   let
    30     val timer = time (Timer.startRealTimer ());
    31     val live = live_of_bnf (hd bnfs);
    32     val n = length bnfs; (*active*)
    33     val ks = 1 upto n;
    34     val m = live - n; (*passive, if 0 don't generate a new bnf*)
    35     val b = Binding.name (fold_rev (fn b => fn s => Binding.name_of b ^ s) bs "");
    36 
    37     (* TODO: check if m, n etc are sane *)
    38 
    39     val deads = fold (union (op =)) Dss resDs;
    40     val names_lthy = fold Variable.declare_typ deads lthy;
    41 
    42     (* tvars *)
    43     val (((((((passiveAs, activeAs), allAs)), (passiveBs, activeBs)),
    44       activeCs), passiveXs), passiveYs) = names_lthy
    45       |> mk_TFrees live
    46       |> apfst (`(chop m))
    47       ||> mk_TFrees live
    48       ||>> apfst (chop m)
    49       ||>> mk_TFrees n
    50       ||>> mk_TFrees m
    51       ||> fst o mk_TFrees m;
    52 
    53     val Ass = replicate n allAs;
    54     val allBs = passiveAs @ activeBs;
    55     val Bss = replicate n allBs;
    56     val allCs = passiveAs @ activeCs;
    57     val allCs' = passiveBs @ activeCs;
    58     val Css' = replicate n allCs';
    59 
    60     (* typs *)
    61     val dead_poss =
    62       (case resBs of
    63         NONE => map SOME deads @ replicate m NONE
    64       | SOME Ts => map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) Ts);
    65     fun mk_param NONE passive = (hd passive, tl passive)
    66       | mk_param (SOME a) passive = (a, passive);
    67     val mk_params = fold_map mk_param dead_poss #> fst;
    68 
    69     fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs;
    70     val (params, params') = `(map Term.dest_TFree) (mk_params passiveAs);
    71     val FTsAs = mk_FTs allAs;
    72     val FTsBs = mk_FTs allBs;
    73     val FTsCs = mk_FTs allCs;
    74     val ATs = map HOLogic.mk_setT passiveAs;
    75     val BTs = map HOLogic.mk_setT activeAs;
    76     val B'Ts = map HOLogic.mk_setT activeBs;
    77     val B''Ts = map HOLogic.mk_setT activeCs;
    78     val sTs = map2 (curry (op -->)) FTsAs activeAs;
    79     val s'Ts = map2 (curry (op -->)) FTsBs activeBs;
    80     val s''Ts = map2 (curry (op -->)) FTsCs activeCs;
    81     val fTs = map2 (curry (op -->)) activeAs activeBs;
    82     val inv_fTs = map2 (curry (op -->)) activeBs activeAs;
    83     val self_fTs = map2 (curry (op -->)) activeAs activeAs;
    84     val gTs = map2 (curry (op -->)) activeBs activeCs;
    85     val all_gTs = map2 (curry (op -->)) allBs allCs';
    86     val prodBsAs = map2 (curry HOLogic.mk_prodT) activeBs activeAs;
    87     val prodFTs = mk_FTs (passiveAs @ prodBsAs);
    88     val prod_sTs = map2 (curry (op -->)) prodFTs activeAs;
    89 
    90     (* terms *)
    91     val mapsAsAs = map4 mk_map_of_bnf Dss Ass Ass bnfs;
    92     val mapsAsBs = map4 mk_map_of_bnf Dss Ass Bss bnfs;
    93     val mapsBsAs = map4 mk_map_of_bnf Dss Bss Ass bnfs;
    94     val mapsBsCs' = map4 mk_map_of_bnf Dss Bss Css' bnfs;
    95     val mapsAsCs' = map4 mk_map_of_bnf Dss Ass Css' bnfs;
    96     val map_fsts = map4 mk_map_of_bnf Dss (replicate n (passiveAs @ prodBsAs)) Bss bnfs;
    97     val map_fsts_rev = map4 mk_map_of_bnf Dss Bss (replicate n (passiveAs @ prodBsAs)) bnfs;
    98     fun mk_setss Ts = map3 mk_sets_of_bnf (map (replicate live) Dss)
    99       (map (replicate live) (replicate n Ts)) bnfs;
   100     val setssAs = mk_setss allAs;
   101     val bds = map3 mk_bd_of_bnf Dss Ass bnfs;
   102     val witss = map wits_of_bnf bnfs;
   103 
   104     val (((((((((((((((((((zs, zs'), As), Bs), Bs_copy), B's), B''s), ss), prod_ss), s's), s''s),
   105       fs), fs_copy), inv_fs), self_fs), gs), all_gs), (xFs, xFs')), (yFs, yFs')),
   106       names_lthy) = lthy
   107       |> mk_Frees' "z" activeAs
   108       ||>> mk_Frees "A" ATs
   109       ||>> mk_Frees "B" BTs
   110       ||>> mk_Frees "B" BTs
   111       ||>> mk_Frees "B'" B'Ts
   112       ||>> mk_Frees "B''" B''Ts
   113       ||>> mk_Frees "s" sTs
   114       ||>> mk_Frees "prods" prod_sTs
   115       ||>> mk_Frees "s'" s'Ts
   116       ||>> mk_Frees "s''" s''Ts
   117       ||>> mk_Frees "f" fTs
   118       ||>> mk_Frees "f" fTs
   119       ||>> mk_Frees "f" inv_fTs
   120       ||>> mk_Frees "f" self_fTs
   121       ||>> mk_Frees "g" gTs
   122       ||>> mk_Frees "g" all_gTs
   123       ||>> mk_Frees' "x" FTsAs
   124       ||>> mk_Frees' "y" FTsBs;
   125 
   126     val passive_UNIVs = map HOLogic.mk_UNIV passiveAs;
   127     val active_UNIVs = map HOLogic.mk_UNIV activeAs;
   128     val prod_UNIVs = map HOLogic.mk_UNIV prodBsAs;
   129     val passive_ids = map HOLogic.id_const passiveAs;
   130     val active_ids = map HOLogic.id_const activeAs;
   131     val fsts = map fst_const prodBsAs;
   132 
   133     (* thms *)
   134     val bd_card_orders = map bd_card_order_of_bnf bnfs;
   135     val bd_Card_orders = map bd_Card_order_of_bnf bnfs;
   136     val bd_Card_order = hd bd_Card_orders;
   137     val bd_Cinfinite = bd_Cinfinite_of_bnf (hd bnfs);
   138     val bd_Cnotzeros = map bd_Cnotzero_of_bnf bnfs;
   139     val bd_Cnotzero = hd bd_Cnotzeros;
   140     val in_bds = map in_bd_of_bnf bnfs;
   141     val map_comp's = map map_comp'_of_bnf bnfs;
   142     val map_congs = map map_cong_of_bnf bnfs;
   143     val map_ids = map map_id_of_bnf bnfs;
   144     val map_id's = map map_id'_of_bnf bnfs;
   145     val map_wpulls = map map_wpull_of_bnf bnfs;
   146     val set_bdss = map set_bd_of_bnf bnfs;
   147     val set_natural'ss = map set_natural'_of_bnf bnfs;
   148 
   149     val timer = time (timer "Extracted terms & thms");
   150 
   151     (* nonemptiness check *)
   152     fun new_wit X wit = subset (op =) (#I wit, (0 upto m - 1) @ map snd X);
   153 
   154     fun enrich X = map_filter (fn i =>
   155       (case find_first (fn (_, i') => i = i') X of
   156         NONE =>
   157           (case find_index (new_wit X) (nth witss (i - m)) of
   158             ~1 => NONE
   159           | j => SOME (j, i))
   160       | SOME ji => SOME ji)) (m upto m + n - 1);
   161     val reachable = fixpoint (op =) enrich [];
   162     val _ = if map snd reachable = (m upto m + n - 1) then ()
   163       else error "The datatype could not be generated because nonemptiness could not be proved";
   164 
   165     val wit_thms =
   166       flat (map2 (fn bnf => fn (j, _) => nth (wit_thmss_of_bnf bnf) j) bnfs reachable);
   167 
   168     val timer = time (timer "Checked nonemptiness");
   169 
   170     (* derived thms *)
   171 
   172     (*map g1 ... gm g(m+1) ... g(m+n) (map id ... id f(m+1) ... f(m+n) x)=
   173       map g1 ... gm (g(m+1) o f(m+1)) ... (g(m+n) o f(m+n)) x*)
   174     fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp =
   175       let
   176         val lhs = Term.list_comb (mapBsCs, all_gs) $
   177           (Term.list_comb (mapAsBs, passive_ids @ fs) $ x);
   178         val rhs = Term.list_comb (mapAsCs,
   179           take m all_gs @ map HOLogic.mk_comp (drop m all_gs ~~ fs)) $ x;
   180       in
   181         Skip_Proof.prove lthy [] []
   182           (fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs)))
   183           (K (mk_map_comp_id_tac map_comp))
   184         |> Thm.close_derivation
   185       end;
   186 
   187     val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comp's;
   188 
   189     (*forall a : set(m+1) x. f(m+1) a = a; ...; forall a : set(m+n) x. f(m+n) a = a ==>
   190       map id ... id f(m+1) ... f(m+n) x = x*)
   191     fun mk_map_congL x mapAsAs sets map_cong map_id' =
   192       let
   193         fun mk_prem set f z z' = HOLogic.mk_Trueprop
   194           (mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z))));
   195         val prems = map4 mk_prem (drop m sets) self_fs zs zs';
   196         val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x);
   197       in
   198         Skip_Proof.prove lthy [] []
   199           (fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
   200           (K (mk_map_congL_tac m map_cong map_id'))
   201         |> Thm.close_derivation
   202       end;
   203 
   204     val map_congL_thms = map5 mk_map_congL xFs mapsAsAs setssAs map_congs map_id's;
   205     val in_mono'_thms = map (fn bnf => in_mono_of_bnf bnf OF (replicate m subset_refl)) bnfs
   206     val in_cong'_thms = map (fn bnf => in_cong_of_bnf bnf OF (replicate m refl)) bnfs
   207 
   208     val timer = time (timer "Derived simple theorems");
   209 
   210     (* algebra *)
   211 
   212     val alg_bind = Binding.suffix_name ("_" ^ algN) b;
   213     val alg_name = Binding.name_of alg_bind;
   214     val alg_def_bind = (Thm.def_binding alg_bind, []);
   215 
   216     (*forall i = 1 ... n: (\<forall>x \<in> Fi_in A1 .. Am B1 ... Bn. si x \<in> Bi)*)
   217     val alg_spec =
   218       let
   219         val algT = Library.foldr (op -->) (ATs @ BTs @ sTs, HOLogic.boolT);
   220 
   221         val ins = map3 mk_in (replicate n (As @ Bs)) setssAs FTsAs;
   222         fun mk_alg_conjunct B s X x x' =
   223           mk_Ball X (Term.absfree x' (HOLogic.mk_mem (s $ x, B)));
   224 
   225         val lhs = Term.list_comb (Free (alg_name, algT), As @ Bs @ ss);
   226         val rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_alg_conjunct Bs ss ins xFs xFs')
   227       in
   228         mk_Trueprop_eq (lhs, rhs)
   229       end;
   230 
   231     val ((alg_free, (_, alg_def_free)), (lthy, lthy_old)) =
   232         lthy
   233         |> Specification.definition (SOME (alg_bind, NONE, NoSyn), (alg_def_bind, alg_spec))
   234         ||> `Local_Theory.restore;
   235 
   236     (*transforms defined frees into consts*)
   237     val phi = Proof_Context.export_morphism lthy_old lthy;
   238     val alg = fst (Term.dest_Const (Morphism.term phi alg_free));
   239     val alg_def = Morphism.thm phi alg_def_free;
   240 
   241     fun mk_alg As Bs ss =
   242       let
   243         val args = As @ Bs @ ss;
   244         val Ts = map fastype_of args;
   245         val algT = Library.foldr (op -->) (Ts, HOLogic.boolT);
   246       in
   247         Term.list_comb (Const (alg, algT), args)
   248       end;
   249 
   250     val alg_set_thms =
   251       let
   252         val alg_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
   253         fun mk_prem x set B = HOLogic.mk_Trueprop (mk_subset (set $ x) B);
   254         fun mk_concl s x B = HOLogic.mk_Trueprop (HOLogic.mk_mem (s $ x, B));
   255         val premss = map2 ((fn x => fn sets =>  map2 (mk_prem x) sets (As @ Bs))) xFs setssAs;
   256         val concls = map3 mk_concl ss xFs Bs;
   257         val goals = map3 (fn x => fn prems => fn concl =>
   258           fold_rev Logic.all (x :: As @ Bs @ ss)
   259             (Logic.list_implies (alg_prem :: prems, concl))) xFs premss concls;
   260       in
   261         map (fn goal =>
   262           Skip_Proof.prove lthy [] [] goal (K (mk_alg_set_tac alg_def)) |> Thm.close_derivation)
   263         goals
   264       end;
   265 
   266     fun mk_talg ATs BTs = mk_alg (map HOLogic.mk_UNIV ATs) (map HOLogic.mk_UNIV BTs);
   267 
   268     val talg_thm =
   269       let
   270         val goal = fold_rev Logic.all ss
   271           (HOLogic.mk_Trueprop (mk_talg passiveAs activeAs ss))
   272       in
   273         Skip_Proof.prove lthy [] [] goal
   274           (K (stac alg_def 1 THEN CONJ_WRAP (K (EVERY' [rtac ballI, rtac UNIV_I] 1)) ss))
   275         |> Thm.close_derivation
   276       end;
   277 
   278     val timer = time (timer "Algebra definition & thms");
   279 
   280     val alg_not_empty_thms =
   281       let
   282         val alg_prem =
   283           HOLogic.mk_Trueprop (mk_alg passive_UNIVs Bs ss);
   284         val concls = map (HOLogic.mk_Trueprop o mk_not_empty) Bs;
   285         val goals =
   286           map (fn concl =>
   287             fold_rev Logic.all (Bs @ ss) (Logic.mk_implies (alg_prem, concl))) concls;
   288       in
   289         map2 (fn goal => fn alg_set =>
   290           Skip_Proof.prove lthy [] []
   291             goal (K (mk_alg_not_empty_tac alg_set alg_set_thms wit_thms))
   292           |> Thm.close_derivation)
   293         goals alg_set_thms
   294       end;
   295 
   296     val timer = time (timer "Proved nonemptiness");
   297 
   298     (* morphism *)
   299 
   300     val mor_bind = Binding.suffix_name ("_" ^ morN) b;
   301     val mor_name = Binding.name_of mor_bind;
   302     val mor_def_bind = (Thm.def_binding mor_bind, []);
   303 
   304     (*fbetw) forall i = 1 ... n: (\<forall>x \<in> Bi. f x \<in> B'i)*)
   305     (*mor) forall i = 1 ... n: (\<forall>x \<in> Fi_in UNIV ... UNIV B1 ... Bn.
   306        f (s1 x) = s1' (Fi_map id ... id f1 ... fn x))*)
   307     val mor_spec =
   308       let
   309         val morT = Library.foldr (op -->) (BTs @ sTs @ B'Ts @ s'Ts @ fTs, HOLogic.boolT);
   310 
   311         fun mk_fbetw f B1 B2 z z' =
   312           mk_Ball B1 (Term.absfree z' (HOLogic.mk_mem (f $ z, B2)));
   313         fun mk_mor sets mapAsBs f s s' T x x' =
   314           mk_Ball (mk_in (passive_UNIVs @ Bs) sets T)
   315             (Term.absfree x' (HOLogic.mk_eq (f $ (s $ x), s' $
   316               (Term.list_comb (mapAsBs, passive_ids @ fs) $ x))));
   317         val lhs = Term.list_comb (Free (mor_name, morT), Bs @ ss @ B's @ s's @ fs);
   318         val rhs = HOLogic.mk_conj
   319           (Library.foldr1 HOLogic.mk_conj (map5 mk_fbetw fs Bs B's zs zs'),
   320           Library.foldr1 HOLogic.mk_conj
   321             (map8 mk_mor setssAs mapsAsBs fs ss s's FTsAs xFs xFs'))
   322       in
   323         mk_Trueprop_eq (lhs, rhs)
   324       end;
   325 
   326     val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) =
   327         lthy
   328         |> Specification.definition (SOME (mor_bind, NONE, NoSyn), (mor_def_bind, mor_spec))
   329         ||> `Local_Theory.restore;
   330 
   331     (*transforms defined frees into consts*)
   332     val phi = Proof_Context.export_morphism lthy_old lthy;
   333     val mor = fst (Term.dest_Const (Morphism.term phi mor_free));
   334     val mor_def = Morphism.thm phi mor_def_free;
   335 
   336     fun mk_mor Bs1 ss1 Bs2 ss2 fs =
   337       let
   338         val args = Bs1 @ ss1 @ Bs2 @ ss2 @ fs;
   339         val Ts = map fastype_of (Bs1 @ ss1 @ Bs2 @ ss2 @ fs);
   340         val morT = Library.foldr (op -->) (Ts, HOLogic.boolT);
   341       in
   342         Term.list_comb (Const (mor, morT), args)
   343       end;
   344 
   345     val (mor_image_thms, morE_thms) =
   346       let
   347         val prem = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs);
   348         fun mk_image_goal f B1 B2 = fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs)
   349           (Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_subset (mk_image f $ B1) B2)));
   350         val image_goals = map3 mk_image_goal fs Bs B's;
   351         fun mk_elim_prem sets x T = HOLogic.mk_Trueprop
   352           (HOLogic.mk_mem (x, mk_in (passive_UNIVs @ Bs) sets T));
   353         fun mk_elim_goal sets mapAsBs f s s' x T =
   354           fold_rev Logic.all (x :: Bs @ ss @ B's @ s's @ fs)
   355             (Logic.list_implies ([prem, mk_elim_prem sets x T],
   356               mk_Trueprop_eq (f $ (s $ x), s' $ Term.list_comb (mapAsBs, passive_ids @ fs @ [x]))));
   357         val elim_goals = map7 mk_elim_goal setssAs mapsAsBs fs ss s's xFs FTsAs;
   358         fun prove goal =
   359           Skip_Proof.prove lthy [] [] goal (K (mk_mor_elim_tac mor_def)) |> Thm.close_derivation;
   360       in
   361         (map prove image_goals, map prove elim_goals)
   362       end;
   363 
   364     val mor_incl_thm =
   365       let
   366         val prems = map2 (HOLogic.mk_Trueprop oo mk_subset) Bs Bs_copy;
   367         val concl = HOLogic.mk_Trueprop (mk_mor Bs ss Bs_copy ss active_ids);
   368       in
   369         Skip_Proof.prove lthy [] []
   370           (fold_rev Logic.all (Bs @ ss @ Bs_copy) (Logic.list_implies (prems, concl)))
   371           (K (mk_mor_incl_tac mor_def map_id's))
   372         |> Thm.close_derivation
   373       end;
   374 
   375     val mor_comp_thm =
   376       let
   377         val prems =
   378           [HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs),
   379            HOLogic.mk_Trueprop (mk_mor B's s's B''s s''s gs)];
   380         val concl =
   381           HOLogic.mk_Trueprop (mk_mor Bs ss B''s s''s (map2 (curry HOLogic.mk_comp) gs fs));
   382       in
   383         Skip_Proof.prove lthy [] []
   384           (fold_rev Logic.all (Bs @ ss @ B's @ s's @ B''s @ s''s @ fs @ gs)
   385              (Logic.list_implies (prems, concl)))
   386           (K (mk_mor_comp_tac mor_def set_natural'ss map_comp_id_thms))
   387         |> Thm.close_derivation
   388       end;
   389 
   390     val mor_inv_thm =
   391       let
   392         fun mk_inv_prem f inv_f B B' = HOLogic.mk_conj (mk_subset (mk_image inv_f $ B') B,
   393           HOLogic.mk_conj (mk_inver inv_f f B, mk_inver f inv_f B'));
   394         val prems = map HOLogic.mk_Trueprop
   395           ([mk_mor Bs ss B's s's fs,
   396           mk_alg passive_UNIVs Bs ss,
   397           mk_alg passive_UNIVs B's s's] @
   398           map4 mk_inv_prem fs inv_fs Bs B's);
   399         val concl = HOLogic.mk_Trueprop (mk_mor B's s's Bs ss inv_fs);
   400       in
   401         Skip_Proof.prove lthy [] []
   402           (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ inv_fs)
   403             (Logic.list_implies (prems, concl)))
   404           (K (mk_mor_inv_tac alg_def mor_def
   405             set_natural'ss morE_thms map_comp_id_thms map_congL_thms))
   406         |> Thm.close_derivation
   407       end;
   408 
   409     val mor_cong_thm =
   410       let
   411         val prems = map HOLogic.mk_Trueprop
   412          (map2 (curry HOLogic.mk_eq) fs_copy fs @ [mk_mor Bs ss B's s's fs])
   413         val concl = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs_copy);
   414       in
   415         Skip_Proof.prove lthy [] []
   416           (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ fs_copy)
   417              (Logic.list_implies (prems, concl)))
   418           (K ((hyp_subst_tac THEN' atac) 1))
   419         |> Thm.close_derivation
   420       end;
   421 
   422     val mor_str_thm =
   423       let
   424         val maps = map2 (fn Ds => fn bnf => Term.list_comb
   425           (mk_map_of_bnf Ds (passiveAs @ FTsAs) allAs bnf, passive_ids @ ss)) Dss bnfs;
   426       in
   427         Skip_Proof.prove lthy [] []
   428           (fold_rev Logic.all ss (HOLogic.mk_Trueprop
   429             (mk_mor (map HOLogic.mk_UNIV FTsAs) maps active_UNIVs ss ss)))
   430           (K (mk_mor_str_tac ks mor_def))
   431         |> Thm.close_derivation
   432       end;
   433 
   434     val mor_convol_thm =
   435       let
   436         val maps = map3 (fn s => fn prod_s => fn map =>
   437           mk_convol (HOLogic.mk_comp (s, Term.list_comb (map, passive_ids @ fsts)), prod_s))
   438           s's prod_ss map_fsts;
   439       in
   440         Skip_Proof.prove lthy [] []
   441           (fold_rev Logic.all (s's @ prod_ss) (HOLogic.mk_Trueprop
   442             (mk_mor prod_UNIVs maps (map HOLogic.mk_UNIV activeBs) s's fsts)))
   443           (K (mk_mor_convol_tac ks mor_def))
   444         |> Thm.close_derivation
   445       end;
   446 
   447     val mor_UNIV_thm =
   448       let
   449         fun mk_conjunct mapAsBs f s s' = HOLogic.mk_eq
   450             (HOLogic.mk_comp (f, s),
   451             HOLogic.mk_comp (s', Term.list_comb (mapAsBs, passive_ids @ fs)));
   452         val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs;
   453         val rhs = Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct mapsAsBs fs ss s's);
   454       in
   455         Skip_Proof.prove lthy [] [] (fold_rev Logic.all (ss @ s's @ fs) (mk_Trueprop_eq (lhs, rhs)))
   456           (K (mk_mor_UNIV_tac m morE_thms mor_def))
   457         |> Thm.close_derivation
   458       end;
   459 
   460     val timer = time (timer "Morphism definition & thms");
   461 
   462     (* isomorphism *)
   463 
   464     (*mor Bs1 ss1 Bs2 ss2 fs \<and> (\<exists>gs. mor Bs2 ss2 Bs1 ss1 fs \<and>
   465        forall i = 1 ... n. (inver gs[i] fs[i] Bs1[i] \<and> inver fs[i] gs[i] Bs2[i]))*)
   466     fun mk_iso Bs1 ss1 Bs2 ss2 fs gs =
   467       let
   468         val ex_inv_mor = list_exists_free gs
   469           (HOLogic.mk_conj (mk_mor Bs2 ss2 Bs1 ss1 gs,
   470             Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_conj)
   471               (map3 mk_inver gs fs Bs1) (map3 mk_inver fs gs Bs2))));
   472       in
   473         HOLogic.mk_conj (mk_mor Bs1 ss1 Bs2 ss2 fs, ex_inv_mor)
   474       end;
   475 
   476     val iso_alt_thm =
   477       let
   478         val prems = map HOLogic.mk_Trueprop
   479          [mk_alg passive_UNIVs Bs ss,
   480          mk_alg passive_UNIVs B's s's]
   481         val concl = mk_Trueprop_eq (mk_iso Bs ss B's s's fs inv_fs,
   482           HOLogic.mk_conj (mk_mor Bs ss B's s's fs,
   483             Library.foldr1 HOLogic.mk_conj (map3 mk_bij_betw fs Bs B's)));
   484       in
   485         Skip_Proof.prove lthy [] []
   486           (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs) (Logic.list_implies (prems, concl)))
   487           (K (mk_iso_alt_tac mor_image_thms mor_inv_thm))
   488         |> Thm.close_derivation
   489       end;
   490 
   491     val timer = time (timer "Isomorphism definition & thms");
   492 
   493     (* algebra copies *)
   494 
   495     val (copy_alg_thm, ex_copy_alg_thm) =
   496       let
   497         val prems = map HOLogic.mk_Trueprop
   498          (mk_alg passive_UNIVs Bs ss :: map3 mk_bij_betw inv_fs B's Bs);
   499         val inver_prems = map HOLogic.mk_Trueprop
   500           (map3 mk_inver inv_fs fs Bs @ map3 mk_inver fs inv_fs B's);
   501         val all_prems = prems @ inver_prems;
   502         fun mk_s f s mapT y y' = Term.absfree y' (f $ (s $
   503           (Term.list_comb (mapT, passive_ids @ inv_fs) $ y)));
   504 
   505         val alg = HOLogic.mk_Trueprop
   506           (mk_alg passive_UNIVs B's (map5 mk_s fs ss mapsBsAs yFs yFs'));
   507         val copy_str_thm = Skip_Proof.prove lthy [] []
   508           (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs)
   509             (Logic.list_implies (all_prems, alg)))
   510           (K (mk_copy_str_tac set_natural'ss alg_def alg_set_thms))
   511           |> Thm.close_derivation;
   512 
   513         val iso = HOLogic.mk_Trueprop
   514           (mk_iso B's (map5 mk_s fs ss mapsBsAs yFs yFs') Bs ss inv_fs fs_copy);
   515         val copy_alg_thm = Skip_Proof.prove lthy [] []
   516           (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs)
   517             (Logic.list_implies (all_prems, iso)))
   518           (K (mk_copy_alg_tac set_natural'ss alg_set_thms mor_def iso_alt_thm copy_str_thm))
   519           |> Thm.close_derivation;
   520 
   521         val ex = HOLogic.mk_Trueprop
   522           (list_exists_free s's
   523             (HOLogic.mk_conj (mk_alg passive_UNIVs B's s's,
   524               mk_iso B's s's Bs ss inv_fs fs_copy)));
   525         val ex_copy_alg_thm = Skip_Proof.prove lthy [] []
   526           (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs)
   527              (Logic.list_implies (prems, ex)))
   528           (K (mk_ex_copy_alg_tac n copy_str_thm copy_alg_thm))
   529           |> Thm.close_derivation;
   530       in
   531         (copy_alg_thm, ex_copy_alg_thm)
   532       end;
   533 
   534     val timer = time (timer "Copy thms");
   535 
   536 
   537     (* bounds *)
   538 
   539     val sum_Card_order = if n = 1 then bd_Card_order else @{thm Card_order_csum};
   540     val sum_Cnotzero = if n = 1 then bd_Cnotzero else bd_Cnotzero RS @{thm csum_Cnotzero1};
   541     val sum_Cinfinite = if n = 1 then bd_Cinfinite else bd_Cinfinite RS @{thm Cinfinite_csum1};
   542     fun mk_set_bd_sums i bd_Card_order bds =
   543       if n = 1 then bds
   544       else map (fn thm => bd_Card_order RS mk_ordLeq_csum n i thm) bds;
   545     val set_bd_sumss = map3 mk_set_bd_sums ks bd_Card_orders set_bdss;
   546 
   547     fun mk_in_bd_sum i Co Cnz bd =
   548       if n = 1 then bd
   549       else Cnz RS ((Co RS mk_ordLeq_csum n i (Co RS @{thm ordLeq_refl})) RS
   550         (bd RS @{thm ordLeq_transitive[OF _
   551           cexp_mono2_Cnotzero[OF _ csum_Cnotzero2[OF ctwo_Cnotzero]]]}));
   552     val in_bd_sums = map4 mk_in_bd_sum ks bd_Card_orders bd_Cnotzeros in_bds;
   553 
   554     val sum_bd = Library.foldr1 (uncurry mk_csum) bds;
   555     val suc_bd = mk_cardSuc sum_bd;
   556     val field_suc_bd = mk_Field suc_bd;
   557     val suc_bdT = fst (dest_relT (fastype_of suc_bd));
   558     fun mk_Asuc_bd [] = mk_cexp ctwo suc_bd
   559       | mk_Asuc_bd As =
   560         mk_cexp (mk_csum (Library.foldr1 (uncurry mk_csum) (map mk_card_of As)) ctwo) suc_bd;
   561 
   562     val suc_bd_Card_order = if n = 1 then bd_Card_order RS @{thm cardSuc_Card_order}
   563       else @{thm cardSuc_Card_order[OF Card_order_csum]};
   564     val suc_bd_Cinfinite = if n = 1 then bd_Cinfinite RS @{thm Cinfinite_cardSuc}
   565       else bd_Cinfinite RS @{thm Cinfinite_cardSuc[OF Cinfinite_csum1]};
   566     val suc_bd_Cnotzero = suc_bd_Cinfinite RS @{thm Cinfinite_Cnotzero};
   567     val suc_bd_worel = suc_bd_Card_order RS @{thm Card_order_wo_rel}
   568     val basis_Asuc = if m = 0 then @{thm ordLeq_refl[OF Card_order_ctwo]}
   569         else @{thm ordLeq_csum2[OF Card_order_ctwo]};
   570     val Asuc_bd_Cinfinite = suc_bd_Cinfinite RS (basis_Asuc RS @{thm Cinfinite_cexp});
   571     val Asuc_bd_Cnotzero = Asuc_bd_Cinfinite RS @{thm Cinfinite_Cnotzero};
   572 
   573     val suc_bd_Asuc_bd = @{thm ordLess_ordLeq_trans[OF
   574       ordLess_ctwo_cexp
   575       cexp_mono1_Cnotzero[OF _ ctwo_Cnotzero]]} OF
   576       [suc_bd_Card_order, basis_Asuc, suc_bd_Card_order];
   577 
   578     val Asuc_bdT = fst (dest_relT (fastype_of (mk_Asuc_bd As)));
   579     val II_BTs = replicate n (HOLogic.mk_setT Asuc_bdT);
   580     val II_sTs = map2 (fn Ds => fn bnf =>
   581       mk_T_of_bnf Ds (passiveAs @ replicate n Asuc_bdT) bnf --> Asuc_bdT) Dss bnfs;
   582 
   583     val (((((((idxs, Asi_name), (idx, idx')), (jdx, jdx')), II_Bs), II_ss), Asuc_fs),
   584       names_lthy) = names_lthy
   585       |> mk_Frees "i" (replicate n suc_bdT)
   586       ||>> (fn ctxt => apfst the_single (mk_fresh_names ctxt 1 "Asi"))
   587       ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") suc_bdT
   588       ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "j") suc_bdT
   589       ||>> mk_Frees "IIB" II_BTs
   590       ||>> mk_Frees "IIs" II_sTs
   591       ||>> mk_Frees "f" (map (fn T => Asuc_bdT --> T) activeAs);
   592 
   593     val suc_bd_limit_thm =
   594       let
   595         val prem = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   596           (map (fn idx => HOLogic.mk_mem (idx, field_suc_bd)) idxs));
   597         fun mk_conjunct idx = HOLogic.mk_conj (mk_not_eq idx jdx,
   598           HOLogic.mk_mem (HOLogic.mk_prod (idx, jdx), suc_bd));
   599         val concl = HOLogic.mk_Trueprop (mk_Bex field_suc_bd
   600           (Term.absfree jdx' (Library.foldr1 HOLogic.mk_conj (map mk_conjunct idxs))));
   601       in
   602         Skip_Proof.prove lthy [] []
   603           (fold_rev Logic.all idxs (Logic.list_implies ([prem], concl)))
   604           (K (mk_bd_limit_tac n suc_bd_Cinfinite))
   605         |> Thm.close_derivation
   606       end;
   607 
   608     val timer = time (timer "Bounds");
   609 
   610 
   611     (* minimal algebra *)
   612 
   613     fun mk_minG Asi i k = mk_UNION (mk_underS suc_bd $ i)
   614       (Term.absfree jdx' (mk_nthN n (Asi $ jdx) k));
   615 
   616     fun mk_minH_component As Asi i sets Ts s k =
   617       HOLogic.mk_binop @{const_name "sup"}
   618       (mk_minG Asi i k, mk_image s $ mk_in (As @ map (mk_minG Asi i) ks) sets Ts);
   619 
   620     fun mk_min_algs As ss =
   621       let
   622         val BTs = map (range_type o fastype_of) ss;
   623         val Ts = map (HOLogic.dest_setT o fastype_of) As @ BTs;
   624         val (Asi, Asi') = `Free (Asi_name, suc_bdT -->
   625           Library.foldr1 HOLogic.mk_prodT (map HOLogic.mk_setT BTs));
   626       in
   627          mk_worec suc_bd (Term.absfree Asi' (Term.absfree idx' (HOLogic.mk_tuple
   628            (map4 (mk_minH_component As Asi idx) (mk_setss Ts) (mk_FTs Ts) ss ks))))
   629       end;
   630 
   631     val (min_algs_thms, min_algs_mono_thms, card_of_min_algs_thm, least_min_algs_thm) =
   632       let
   633         val i_field = HOLogic.mk_mem (idx, field_suc_bd);
   634         val min_algs = mk_min_algs As ss;
   635         val min_algss = map (fn k => mk_nthN n (min_algs $ idx) k) ks;
   636 
   637         val concl = HOLogic.mk_Trueprop
   638           (HOLogic.mk_eq (min_algs $ idx, HOLogic.mk_tuple
   639             (map4 (mk_minH_component As min_algs idx) setssAs FTsAs ss ks)));
   640         val goal = fold_rev Logic.all (idx :: As @ ss)
   641           (Logic.mk_implies (HOLogic.mk_Trueprop i_field, concl));
   642 
   643         val min_algs_thm = Skip_Proof.prove lthy [] [] goal
   644           (K (mk_min_algs_tac suc_bd_worel in_cong'_thms))
   645           |> Thm.close_derivation;
   646 
   647         val min_algs_thms = map (fn k => min_algs_thm RS mk_nthI n k) ks;
   648 
   649         fun mk_mono_goal min_alg =
   650           fold_rev Logic.all (As @ ss) (HOLogic.mk_Trueprop (mk_relChain suc_bd
   651             (Term.absfree idx' min_alg)));
   652 
   653         val monos =
   654           map2 (fn goal => fn min_algs =>
   655             Skip_Proof.prove lthy [] [] goal (K (mk_min_algs_mono_tac min_algs))
   656             |> Thm.close_derivation)
   657           (map mk_mono_goal min_algss) min_algs_thms;
   658 
   659         val Asuc_bd = mk_Asuc_bd As;
   660 
   661         fun mk_card_conjunct min_alg = mk_ordLeq (mk_card_of min_alg) Asuc_bd;
   662         val card_conjunction = Library.foldr1 HOLogic.mk_conj (map mk_card_conjunct min_algss);
   663         val card_cT = certifyT lthy suc_bdT;
   664         val card_ct = certify lthy (Term.absfree idx' card_conjunction);
   665 
   666         val card_of = singleton (Proof_Context.export names_lthy lthy)
   667           (Skip_Proof.prove lthy [] []
   668             (HOLogic.mk_Trueprop (HOLogic.mk_imp (i_field, card_conjunction)))
   669             (K (mk_min_algs_card_of_tac card_cT card_ct
   670               m suc_bd_worel min_algs_thms in_bd_sums
   671               sum_Card_order sum_Cnotzero suc_bd_Card_order suc_bd_Cinfinite suc_bd_Cnotzero
   672               suc_bd_Asuc_bd Asuc_bd_Cinfinite Asuc_bd_Cnotzero)))
   673           |> Thm.close_derivation;
   674 
   675         val least_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
   676         val least_conjunction = Library.foldr1 HOLogic.mk_conj (map2 mk_subset min_algss Bs);
   677         val least_cT = certifyT lthy suc_bdT;
   678         val least_ct = certify lthy (Term.absfree idx' least_conjunction);
   679 
   680         val least = singleton (Proof_Context.export names_lthy lthy)
   681           (Skip_Proof.prove lthy [] []
   682             (Logic.mk_implies (least_prem,
   683               HOLogic.mk_Trueprop (HOLogic.mk_imp (i_field, least_conjunction))))
   684             (K (mk_min_algs_least_tac least_cT least_ct
   685               suc_bd_worel min_algs_thms alg_set_thms)))
   686           |> Thm.close_derivation;
   687       in
   688         (min_algs_thms, monos, card_of, least)
   689       end;
   690 
   691     val timer = time (timer "min_algs definition & thms");
   692 
   693     fun min_alg_bind i = Binding.suffix_name
   694       ("_" ^ min_algN ^ (if n = 1 then "" else string_of_int i)) b;
   695     val min_alg_name = Binding.name_of o min_alg_bind;
   696     val min_alg_def_bind = rpair [] o Thm.def_binding o min_alg_bind;
   697 
   698     fun min_alg_spec i =
   699       let
   700         val min_algT =
   701           Library.foldr (op -->) (ATs @ sTs, HOLogic.mk_setT (nth activeAs (i - 1)));
   702 
   703         val lhs = Term.list_comb (Free (min_alg_name i, min_algT), As @ ss);
   704         val rhs = mk_UNION (field_suc_bd)
   705           (Term.absfree idx' (mk_nthN n (mk_min_algs As ss $ idx) i));
   706       in
   707         mk_Trueprop_eq (lhs, rhs)
   708       end;
   709 
   710     val ((min_alg_frees, (_, min_alg_def_frees)), (lthy, lthy_old)) =
   711         lthy
   712         |> fold_map (fn i => Specification.definition
   713           (SOME (min_alg_bind i, NONE, NoSyn), (min_alg_def_bind i, min_alg_spec i))) ks
   714         |>> apsnd split_list o split_list
   715         ||> `Local_Theory.restore;
   716 
   717     (*transforms defined frees into consts*)
   718     val phi = Proof_Context.export_morphism lthy_old lthy;
   719     val min_algs = map (fst o Term.dest_Const o Morphism.term phi) min_alg_frees;
   720     val min_alg_defs = map (Morphism.thm phi) min_alg_def_frees;
   721 
   722     fun mk_min_alg As ss i =
   723       let
   724         val T = HOLogic.mk_setT (range_type (fastype_of (nth ss (i - 1))))
   725         val args = As @ ss;
   726         val Ts = map fastype_of args;
   727         val min_algT = Library.foldr (op -->) (Ts, T);
   728       in
   729         Term.list_comb (Const (nth min_algs (i - 1), min_algT), args)
   730       end;
   731 
   732     val (alg_min_alg_thm, card_of_min_alg_thms, least_min_alg_thms, mor_incl_min_alg_thm) =
   733       let
   734         val min_algs = map (mk_min_alg As ss) ks;
   735 
   736         val goal = fold_rev Logic.all (As @ ss) (HOLogic.mk_Trueprop (mk_alg As min_algs ss));
   737         val alg_min_alg = Skip_Proof.prove lthy [] [] goal
   738           (K (mk_alg_min_alg_tac m alg_def min_alg_defs suc_bd_limit_thm sum_Cinfinite
   739             set_bd_sumss min_algs_thms min_algs_mono_thms))
   740           |> Thm.close_derivation;
   741 
   742         val Asuc_bd = mk_Asuc_bd As;
   743         fun mk_card_of_thm min_alg def = Skip_Proof.prove lthy [] []
   744           (fold_rev Logic.all (As @ ss)
   745             (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of min_alg) Asuc_bd)))
   746           (K (mk_card_of_min_alg_tac def card_of_min_algs_thm
   747             suc_bd_Card_order suc_bd_Asuc_bd Asuc_bd_Cinfinite))
   748           |> Thm.close_derivation;
   749 
   750         val least_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
   751         fun mk_least_thm min_alg B def = Skip_Proof.prove lthy [] []
   752           (fold_rev Logic.all (As @ Bs @ ss)
   753             (Logic.mk_implies (least_prem, HOLogic.mk_Trueprop (mk_subset min_alg B))))
   754           (K (mk_least_min_alg_tac def least_min_algs_thm))
   755           |> Thm.close_derivation;
   756 
   757         val leasts = map3 mk_least_thm min_algs Bs min_alg_defs;
   758 
   759         val incl_prem = HOLogic.mk_Trueprop (mk_alg passive_UNIVs Bs ss);
   760         val incl_min_algs = map (mk_min_alg passive_UNIVs ss) ks;
   761         val incl = Skip_Proof.prove lthy [] []
   762           (fold_rev Logic.all (Bs @ ss)
   763             (Logic.mk_implies (incl_prem,
   764               HOLogic.mk_Trueprop (mk_mor incl_min_algs ss Bs ss active_ids))))
   765           (K (EVERY' (rtac mor_incl_thm :: map etac leasts) 1))
   766           |> Thm.close_derivation;
   767       in
   768         (alg_min_alg, map2 mk_card_of_thm min_algs min_alg_defs, leasts, incl)
   769       end;
   770 
   771     val timer = time (timer "Minimal algebra definition & thms");
   772 
   773     val II_repT = HOLogic.mk_prodT (HOLogic.mk_tupleT II_BTs, HOLogic.mk_tupleT II_sTs);
   774     val IIT_bind = Binding.suffix_name ("_" ^ IITN) b;
   775 
   776     val ((IIT_name, (IIT_glob_info, IIT_loc_info)), lthy) =
   777       typedef false NONE (IIT_bind, params, NoSyn)
   778         (HOLogic.mk_UNIV II_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
   779 
   780     val IIT = Type (IIT_name, params');
   781     val Abs_IIT = Const (#Abs_name IIT_glob_info, II_repT --> IIT);
   782     val Rep_IIT = Const (#Rep_name IIT_glob_info, IIT --> II_repT);
   783     val Abs_IIT_inverse_thm = UNIV_I RS #Abs_inverse IIT_loc_info;
   784 
   785     val initT = IIT --> Asuc_bdT;
   786     val active_initTs = replicate n initT;
   787     val init_FTs = map2 (fn Ds => mk_T_of_bnf Ds (passiveAs @ active_initTs)) Dss bnfs;
   788     val init_fTs = map (fn T => initT --> T) activeAs;
   789 
   790     val (((((((iidx, iidx'), init_xs), (init_xFs, init_xFs')),
   791       init_fs), init_fs_copy), init_phis), names_lthy) = names_lthy
   792       |> yield_singleton (apfst (op ~~) oo mk_Frees' "i") IIT
   793       ||>> mk_Frees "ix" active_initTs
   794       ||>> mk_Frees' "x" init_FTs
   795       ||>> mk_Frees "f" init_fTs
   796       ||>> mk_Frees "f" init_fTs
   797       ||>> mk_Frees "phi" (replicate n (initT --> HOLogic.boolT));
   798 
   799     val II = HOLogic.mk_Collect (fst iidx', IIT, list_exists_free (II_Bs @ II_ss)
   800       (HOLogic.mk_conj (HOLogic.mk_eq (iidx,
   801         Abs_IIT $ (HOLogic.mk_prod (HOLogic.mk_tuple II_Bs, HOLogic.mk_tuple II_ss))),
   802         mk_alg passive_UNIVs II_Bs II_ss)));
   803 
   804     val select_Bs = map (mk_nthN n (HOLogic.mk_fst (Rep_IIT $ iidx))) ks;
   805     val select_ss = map (mk_nthN n (HOLogic.mk_snd (Rep_IIT $ iidx))) ks;
   806 
   807     fun str_init_bind i = Binding.suffix_name ("_" ^ str_initN ^ (if n = 1 then "" else
   808       string_of_int i)) b;
   809     val str_init_name = Binding.name_of o str_init_bind;
   810     val str_init_def_bind = rpair [] o Thm.def_binding o str_init_bind;
   811 
   812     fun str_init_spec i =
   813       let
   814         val T = nth init_FTs (i - 1);
   815         val init_xF = nth init_xFs (i - 1)
   816         val select_s = nth select_ss (i - 1);
   817         val map = mk_map_of_bnf (nth Dss (i - 1))
   818           (passiveAs @ active_initTs) (passiveAs @ replicate n Asuc_bdT)
   819           (nth bnfs (i - 1));
   820         val map_args = passive_ids @ replicate n (mk_rapp iidx Asuc_bdT);
   821         val str_initT = T --> IIT --> Asuc_bdT;
   822 
   823         val lhs = Term.list_comb (Free (str_init_name i, str_initT), [init_xF, iidx]);
   824         val rhs = select_s $ (Term.list_comb (map, map_args) $ init_xF);
   825       in
   826         mk_Trueprop_eq (lhs, rhs)
   827       end;
   828 
   829     val ((str_init_frees, (_, str_init_def_frees)), (lthy, lthy_old)) =
   830       lthy
   831       |> fold_map (fn i => Specification.definition
   832         (SOME (str_init_bind i, NONE, NoSyn), (str_init_def_bind i, str_init_spec i))) ks
   833       |>> apsnd split_list o split_list
   834       ||> `Local_Theory.restore;
   835 
   836     (*transforms defined frees into consts*)
   837     val phi = Proof_Context.export_morphism lthy_old lthy;
   838     val str_inits =
   839       map (Term.subst_atomic_types (map (`(Morphism.typ phi)) params') o Morphism.term phi)
   840         str_init_frees;
   841 
   842     val str_init_defs = map (Morphism.thm phi) str_init_def_frees;
   843 
   844     val car_inits = map (mk_min_alg passive_UNIVs str_inits) ks;
   845 
   846     (*TODO: replace with instantiate? (problem: figure out right type instantiation)*)
   847     val alg_init_thm = Skip_Proof.prove lthy [] []
   848       (HOLogic.mk_Trueprop (mk_alg passive_UNIVs car_inits str_inits))
   849       (K (rtac alg_min_alg_thm 1))
   850       |> Thm.close_derivation;
   851 
   852     val alg_select_thm = Skip_Proof.prove lthy [] []
   853       (HOLogic.mk_Trueprop (mk_Ball II
   854         (Term.absfree iidx' (mk_alg passive_UNIVs select_Bs select_ss))))
   855       (mk_alg_select_tac Abs_IIT_inverse_thm)
   856       |> Thm.close_derivation;
   857 
   858     val mor_select_thm =
   859       let
   860         val alg_prem = HOLogic.mk_Trueprop (mk_alg passive_UNIVs Bs ss);
   861         val i_prem = HOLogic.mk_Trueprop (HOLogic.mk_mem (iidx, II));
   862         val mor_prem = HOLogic.mk_Trueprop (mk_mor select_Bs select_ss Bs ss Asuc_fs);
   863         val prems = [alg_prem, i_prem, mor_prem];
   864         val concl = HOLogic.mk_Trueprop
   865           (mk_mor car_inits str_inits Bs ss
   866             (map (fn f => HOLogic.mk_comp (f, mk_rapp iidx Asuc_bdT)) Asuc_fs));
   867       in
   868         Skip_Proof.prove lthy [] []
   869           (fold_rev Logic.all (iidx :: Bs @ ss @ Asuc_fs) (Logic.list_implies (prems, concl)))
   870           (K (mk_mor_select_tac mor_def mor_cong_thm mor_comp_thm mor_incl_min_alg_thm alg_def
   871             alg_select_thm alg_set_thms set_natural'ss str_init_defs))
   872         |> Thm.close_derivation
   873       end;
   874 
   875     val (init_ex_mor_thm, init_unique_mor_thms) =
   876       let
   877         val prem = HOLogic.mk_Trueprop (mk_alg passive_UNIVs Bs ss);
   878         val concl = HOLogic.mk_Trueprop
   879           (list_exists_free init_fs (mk_mor car_inits str_inits Bs ss init_fs));
   880         val ex_mor = Skip_Proof.prove lthy [] []
   881           (fold_rev Logic.all (Bs @ ss) (Logic.mk_implies (prem, concl)))
   882           (mk_init_ex_mor_tac Abs_IIT_inverse_thm ex_copy_alg_thm alg_min_alg_thm
   883             card_of_min_alg_thms mor_comp_thm mor_select_thm mor_incl_min_alg_thm)
   884           |> Thm.close_derivation;
   885 
   886         val prems = map2 (HOLogic.mk_Trueprop oo curry HOLogic.mk_mem) init_xs car_inits
   887         val mor_prems = map HOLogic.mk_Trueprop
   888           [mk_mor car_inits str_inits Bs ss init_fs,
   889           mk_mor car_inits str_inits Bs ss init_fs_copy];
   890         fun mk_fun_eq f g x = HOLogic.mk_eq (f $ x, g $ x);
   891         val unique = HOLogic.mk_Trueprop
   892           (Library.foldr1 HOLogic.mk_conj (map3 mk_fun_eq init_fs init_fs_copy init_xs));
   893         val unique_mor = Skip_Proof.prove lthy [] []
   894           (fold_rev Logic.all (init_xs @ Bs @ ss @ init_fs @ init_fs_copy)
   895             (Logic.list_implies (prems @ mor_prems, unique)))
   896           (K (mk_init_unique_mor_tac m alg_def alg_init_thm least_min_alg_thms
   897             in_mono'_thms alg_set_thms morE_thms map_congs))
   898           |> Thm.close_derivation;
   899       in
   900         (ex_mor, split_conj_thm unique_mor)
   901       end;
   902 
   903     val init_setss = mk_setss (passiveAs @ active_initTs);
   904     val active_init_setss = map (drop m) init_setss;
   905     val init_ins = map2 (fn sets => mk_in (passive_UNIVs @ car_inits) sets) init_setss init_FTs;
   906 
   907     fun mk_closed phis =
   908       let
   909         fun mk_conjunct phi str_init init_sets init_in x x' =
   910           let
   911             val prem = Library.foldr1 HOLogic.mk_conj
   912               (map2 (fn set => mk_Ball (set $ x)) init_sets phis);
   913             val concl = phi $ (str_init $ x);
   914           in
   915             mk_Ball init_in (Term.absfree x' (HOLogic.mk_imp (prem, concl)))
   916           end;
   917       in
   918         Library.foldr1 HOLogic.mk_conj
   919           (map6 mk_conjunct phis str_inits active_init_setss init_ins init_xFs init_xFs')
   920       end;
   921 
   922     val init_induct_thm =
   923       let
   924         val prem = HOLogic.mk_Trueprop (mk_closed init_phis);
   925         val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   926           (map2 mk_Ball car_inits init_phis));
   927       in
   928         Skip_Proof.prove lthy [] []
   929           (fold_rev Logic.all init_phis (Logic.mk_implies (prem, concl)))
   930           (K (mk_init_induct_tac m alg_def alg_init_thm least_min_alg_thms alg_set_thms))
   931         |> Thm.close_derivation
   932       end;
   933 
   934     val timer = time (timer "Initiality definition & thms");
   935 
   936     val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
   937       lthy
   938       |> fold_map3 (fn b => fn mx => fn car_init => typedef false NONE (b, params, mx) car_init NONE
   939           (EVERY' [rtac ssubst, rtac @{thm ex_in_conv}, resolve_tac alg_not_empty_thms,
   940             rtac alg_init_thm] 1)) bs mixfixes car_inits
   941       |>> apsnd split_list o split_list;
   942 
   943     val Ts = map (fn name => Type (name, params')) T_names;
   944     fun mk_Ts passive = map (Term.typ_subst_atomic (passiveAs ~~ passive)) Ts;
   945     val Ts' = mk_Ts passiveBs;
   946     val Rep_Ts = map2 (fn info => fn T => Const (#Rep_name info, T --> initT)) T_glob_infos Ts;
   947     val Abs_Ts = map2 (fn info => fn T => Const (#Abs_name info, initT --> T)) T_glob_infos Ts;
   948 
   949     val type_defs = map #type_definition T_loc_infos;
   950     val Reps = map #Rep T_loc_infos;
   951     val Rep_casess = map #Rep_cases T_loc_infos;
   952     val Rep_injects = map #Rep_inject T_loc_infos;
   953     val Rep_inverses = map #Rep_inverse T_loc_infos;
   954     val Abs_inverses = map #Abs_inverse T_loc_infos;
   955 
   956     fun mk_inver_thm mk_tac rep abs X thm =
   957       Skip_Proof.prove lthy [] []
   958         (HOLogic.mk_Trueprop (mk_inver rep abs X))
   959         (K (EVERY' [rtac ssubst, rtac @{thm inver_def}, rtac ballI, mk_tac thm] 1))
   960       |> Thm.close_derivation;
   961 
   962     val inver_Reps = map4 (mk_inver_thm rtac) Abs_Ts Rep_Ts (map HOLogic.mk_UNIV Ts) Rep_inverses;
   963     val inver_Abss = map4 (mk_inver_thm etac) Rep_Ts Abs_Ts car_inits Abs_inverses;
   964 
   965     val timer = time (timer "THE TYPEDEFs & Rep/Abs thms");
   966 
   967     val UNIVs = map HOLogic.mk_UNIV Ts;
   968     val FTs = mk_FTs (passiveAs @ Ts);
   969     val FTs' = mk_FTs (passiveBs @ Ts');
   970     fun mk_set_Ts T = passiveAs @ replicate n (HOLogic.mk_setT T);
   971     val setFTss = map (mk_FTs o mk_set_Ts) passiveAs;
   972     val FTs_setss = mk_setss (passiveAs @ Ts);
   973     val FTs'_setss = mk_setss (passiveBs @ Ts');
   974     val map_FT_inits = map2 (fn Ds =>
   975       mk_map_of_bnf Ds (passiveAs @ Ts) (passiveAs @ active_initTs)) Dss bnfs;
   976     val fTs = map2 (curry op -->) Ts activeAs;
   977     val iterT = Library.foldr1 HOLogic.mk_prodT (map2 (curry op -->) Ts activeAs);
   978     val rec_sTs = map (Term.typ_subst_atomic (activeBs ~~ Ts)) prod_sTs;
   979     val rec_maps = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_fsts;
   980     val rec_maps_rev = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_fsts_rev;
   981     val rec_fsts = map (Term.subst_atomic_types (activeBs ~~ Ts)) fsts;
   982 
   983     val (((((((((((Izs, (Izs1, Izs1')), (Izs2, Izs2')), (xFs, xFs')), yFs), (AFss, AFss')),
   984       (iter_f, iter_f')), fs), phis), phi2s), rec_ss), names_lthy) = names_lthy
   985       |> mk_Frees "z" Ts
   986       ||>> mk_Frees' "z1" Ts
   987       ||>> mk_Frees' "z2" Ts'
   988       ||>> mk_Frees' "x" FTs
   989       ||>> mk_Frees "y" FTs'
   990       ||>> mk_Freess' "z" setFTss
   991       ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "f") iterT
   992       ||>> mk_Frees "f" fTs
   993       ||>> mk_Frees "phi" (map (fn T => T --> HOLogic.boolT) Ts)
   994       ||>> mk_Frees "phi" (map2 (fn T => fn U => T --> U --> HOLogic.boolT) Ts Ts')
   995       ||>> mk_Frees "s" rec_sTs;
   996 
   997     fun fld_bind i = Binding.suffix_name ("_" ^ fldN) (nth bs (i - 1));
   998     val fld_name = Binding.name_of o fld_bind;
   999     val fld_def_bind = rpair [] o Thm.def_binding o fld_bind;
  1000 
  1001     fun fld_spec i abs str map_FT_init x x' =
  1002       let
  1003         val fldT = nth FTs (i - 1) --> nth Ts (i - 1);
  1004 
  1005         val lhs = Free (fld_name i, fldT);
  1006         val rhs = Term.absfree x' (abs $ (str $
  1007           (Term.list_comb (map_FT_init, map HOLogic.id_const passiveAs @ Rep_Ts) $ x)));
  1008       in
  1009         mk_Trueprop_eq (lhs, rhs)
  1010       end;
  1011 
  1012     val ((fld_frees, (_, fld_def_frees)), (lthy, lthy_old)) =
  1013         lthy
  1014         |> fold_map6 (fn i => fn abs => fn str => fn map => fn x => fn x' =>
  1015           Specification.definition
  1016             (SOME (fld_bind i, NONE, NoSyn), (fld_def_bind i, fld_spec i abs str map x x')))
  1017             ks Abs_Ts str_inits map_FT_inits xFs xFs'
  1018         |>> apsnd split_list o split_list
  1019         ||> `Local_Theory.restore;
  1020 
  1021     (*transforms defined frees into consts*)
  1022     val phi = Proof_Context.export_morphism lthy_old lthy;
  1023     fun mk_flds passive =
  1024       map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (mk_params passive)) o
  1025         Morphism.term phi) fld_frees;
  1026     val flds = mk_flds passiveAs;
  1027     val fld's = mk_flds passiveBs;
  1028     val fld_defs = map (Morphism.thm phi) fld_def_frees;
  1029 
  1030     val (mor_Rep_thm, mor_Abs_thm) =
  1031       let
  1032         val copy = alg_init_thm RS copy_alg_thm;
  1033         fun mk_bij inj Rep cases = @{thm bij_betwI'} OF [inj, Rep, cases];
  1034         val bijs = map3 mk_bij Rep_injects Reps Rep_casess;
  1035         val mor_Rep =
  1036           Skip_Proof.prove lthy [] []
  1037             (HOLogic.mk_Trueprop (mk_mor UNIVs flds car_inits str_inits Rep_Ts))
  1038             (mk_mor_Rep_tac fld_defs copy bijs inver_Abss inver_Reps)
  1039           |> Thm.close_derivation;
  1040 
  1041         val inv = mor_inv_thm OF [mor_Rep, talg_thm, alg_init_thm];
  1042         val mor_Abs =
  1043           Skip_Proof.prove lthy [] []
  1044             (HOLogic.mk_Trueprop (mk_mor car_inits str_inits UNIVs flds Abs_Ts))
  1045             (K (mk_mor_Abs_tac inv inver_Abss inver_Reps))
  1046           |> Thm.close_derivation;
  1047       in
  1048         (mor_Rep, mor_Abs)
  1049       end;
  1050 
  1051     val timer = time (timer "fld definitions & thms");
  1052 
  1053     val iter_fun = Term.absfree iter_f'
  1054       (mk_mor UNIVs flds active_UNIVs ss (map (mk_nthN n iter_f) ks));
  1055     val iter = HOLogic.choice_const iterT $ iter_fun;
  1056 
  1057     fun iter_bind i = Binding.suffix_name ("_" ^ fld_iterN) (nth bs (i - 1));
  1058     val iter_name = Binding.name_of o iter_bind;
  1059     val iter_def_bind = rpair [] o Thm.def_binding o iter_bind;
  1060 
  1061     fun iter_spec i T AT =
  1062       let
  1063         val iterT = Library.foldr (op -->) (sTs, T --> AT);
  1064 
  1065         val lhs = Term.list_comb (Free (iter_name i, iterT), ss);
  1066         val rhs = mk_nthN n iter i;
  1067       in
  1068         mk_Trueprop_eq (lhs, rhs)
  1069       end;
  1070 
  1071     val ((iter_frees, (_, iter_def_frees)), (lthy, lthy_old)) =
  1072         lthy
  1073         |> fold_map3 (fn i => fn T => fn AT =>
  1074           Specification.definition
  1075             (SOME (iter_bind i, NONE, NoSyn), (iter_def_bind i, iter_spec i T AT)))
  1076             ks Ts activeAs
  1077         |>> apsnd split_list o split_list
  1078         ||> `Local_Theory.restore;
  1079 
  1080     (*transforms defined frees into consts*)
  1081     val phi = Proof_Context.export_morphism lthy_old lthy;
  1082     val iters = map (Morphism.term phi) iter_frees;
  1083     val iter_names = map (fst o dest_Const) iters;
  1084     fun mk_iter Ts ss i = Term.list_comb (Const (nth iter_names (i - 1), Library.foldr (op -->)
  1085       (map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss);
  1086     val iter_defs = map (Morphism.thm phi) iter_def_frees;
  1087 
  1088     val mor_iter_thm =
  1089       let
  1090         val ex_mor = talg_thm RS init_ex_mor_thm;
  1091         val mor_cong = mor_cong_thm OF (map (mk_nth_conv n) ks);
  1092         val mor_comp = mor_Rep_thm RS mor_comp_thm;
  1093         val cT = certifyT lthy iterT;
  1094         val ct = certify lthy iter_fun
  1095       in
  1096         singleton (Proof_Context.export names_lthy lthy)
  1097           (Skip_Proof.prove lthy [] []
  1098             (HOLogic.mk_Trueprop (mk_mor UNIVs flds active_UNIVs ss (map (mk_iter Ts ss) ks)))
  1099             (K (mk_mor_iter_tac cT ct iter_defs ex_mor (mor_comp RS mor_cong))))
  1100         |> Thm.close_derivation
  1101       end;
  1102 
  1103     val iter_thms = map (fn morE => rule_by_tactic lthy
  1104       ((rtac CollectI THEN' CONJ_WRAP' (K (rtac @{thm subset_UNIV})) (1 upto m + n)) 1)
  1105       (mor_iter_thm RS morE)) morE_thms;
  1106 
  1107     val (iter_unique_mor_thms, iter_unique_mor_thm) =
  1108       let
  1109         val prem = HOLogic.mk_Trueprop (mk_mor UNIVs flds active_UNIVs ss fs);
  1110         fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_iter Ts ss i);
  1111         val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_fun_eq fs ks));
  1112         val unique_mor = Skip_Proof.prove lthy [] []
  1113           (fold_rev Logic.all (ss @ fs) (Logic.mk_implies (prem, unique)))
  1114           (K (mk_iter_unique_mor_tac type_defs init_unique_mor_thms Reps
  1115             mor_comp_thm mor_Abs_thm mor_iter_thm))
  1116           |> Thm.close_derivation;
  1117       in
  1118         `split_conj_thm unique_mor
  1119       end;
  1120 
  1121     val (iter_unique_thms, iter_unique_thm) =
  1122       `split_conj_thm (mk_conjIN n RS
  1123         (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS iter_unique_mor_thm))
  1124 
  1125     val iter_fld_thms =
  1126       map (fn thm => (mor_incl_thm OF replicate n @{thm subset_UNIV}) RS thm RS sym)
  1127         iter_unique_mor_thms;
  1128 
  1129     val fld_o_iter_thms =
  1130       let
  1131         val mor = mor_comp_thm OF [mor_iter_thm, mor_str_thm];
  1132       in
  1133         map2 (fn unique => fn iter_fld =>
  1134           trans OF [mor RS unique, iter_fld]) iter_unique_mor_thms iter_fld_thms
  1135       end;
  1136 
  1137     val timer = time (timer "iter definitions & thms");
  1138 
  1139     val map_flds = map2 (fn Ds => fn bnf =>
  1140       Term.list_comb (mk_map_of_bnf Ds (passiveAs @ FTs) (passiveAs @ Ts) bnf,
  1141         map HOLogic.id_const passiveAs @ flds)) Dss bnfs;
  1142 
  1143     fun unf_bind i = Binding.suffix_name ("_" ^ unfN) (nth bs (i - 1));
  1144     val unf_name = Binding.name_of o unf_bind;
  1145     val unf_def_bind = rpair [] o Thm.def_binding o unf_bind;
  1146 
  1147     fun unf_spec i FT T =
  1148       let
  1149         val unfT = T --> FT;
  1150 
  1151         val lhs = Free (unf_name i, unfT);
  1152         val rhs = mk_iter Ts map_flds i;
  1153       in
  1154         mk_Trueprop_eq (lhs, rhs)
  1155       end;
  1156 
  1157     val ((unf_frees, (_, unf_def_frees)), (lthy, lthy_old)) =
  1158         lthy
  1159         |> fold_map3 (fn i => fn FT => fn T =>
  1160           Specification.definition
  1161             (SOME (unf_bind i, NONE, NoSyn), (unf_def_bind i, unf_spec i FT T))) ks FTs Ts
  1162         |>> apsnd split_list o split_list
  1163         ||> `Local_Theory.restore;
  1164 
  1165     (*transforms defined frees into consts*)
  1166     val phi = Proof_Context.export_morphism lthy_old lthy;
  1167     fun mk_unfs params =
  1168       map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ params) o Morphism.term phi)
  1169         unf_frees;
  1170     val unfs = mk_unfs params';
  1171     val unf_defs = map (Morphism.thm phi) unf_def_frees;
  1172 
  1173     val fld_o_unf_thms = map2 (Local_Defs.fold lthy o single) unf_defs fld_o_iter_thms;
  1174 
  1175     val unf_o_fld_thms =
  1176       let
  1177         fun mk_goal unf fld FT = mk_Trueprop_eq (HOLogic.mk_comp (unf, fld), HOLogic.id_const FT);
  1178         val goals = map3 mk_goal unfs flds FTs;
  1179       in
  1180         map5 (fn goal => fn unf_def => fn iter => fn map_comp_id => fn map_congL =>
  1181           Skip_Proof.prove lthy [] [] goal
  1182             (K (mk_unf_o_fld_tac unf_def iter map_comp_id map_congL fld_o_iter_thms))
  1183           |> Thm.close_derivation)
  1184         goals unf_defs iter_thms map_comp_id_thms map_congL_thms
  1185       end;
  1186 
  1187     val unf_fld_thms = map (fn thm => thm RS @{thm pointfree_idE}) unf_o_fld_thms;
  1188     val fld_unf_thms = map (fn thm => thm RS @{thm pointfree_idE}) fld_o_unf_thms;
  1189 
  1190     val bij_unf_thms =
  1191       map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) fld_o_unf_thms unf_o_fld_thms;
  1192     val inj_unf_thms = map (fn thm => thm RS @{thm bij_is_inj}) bij_unf_thms;
  1193     val surj_unf_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_unf_thms;
  1194     val unf_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_unf_thms;
  1195     val unf_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_unf_thms;
  1196     val unf_exhaust_thms = map (fn thm => thm RS exE) unf_nchotomy_thms;
  1197 
  1198     val bij_fld_thms =
  1199       map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) unf_o_fld_thms fld_o_unf_thms;
  1200     val inj_fld_thms = map (fn thm => thm RS @{thm bij_is_inj}) bij_fld_thms;
  1201     val surj_fld_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_fld_thms;
  1202     val fld_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_fld_thms;
  1203     val fld_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_fld_thms;
  1204     val fld_exhaust_thms = map (fn thm => thm RS exE) fld_nchotomy_thms;
  1205 
  1206     val timer = time (timer "unf definitions & thms");
  1207 
  1208     val fst_rec_pair_thms =
  1209       let
  1210         val mor = mor_comp_thm OF [mor_iter_thm, mor_convol_thm];
  1211       in
  1212         map2 (fn unique => fn iter_fld =>
  1213           trans OF [mor RS unique, iter_fld]) iter_unique_mor_thms iter_fld_thms
  1214       end;
  1215 
  1216     fun rec_bind i = Binding.suffix_name ("_" ^ fld_recN) (nth bs (i - 1));
  1217     val rec_name = Binding.name_of o rec_bind;
  1218     val rec_def_bind = rpair [] o Thm.def_binding o rec_bind;
  1219 
  1220     fun rec_spec i T AT =
  1221       let
  1222         val recT = Library.foldr (op -->) (rec_sTs, T --> AT);
  1223         val maps = map3 (fn fld => fn prod_s => fn map =>
  1224           mk_convol (HOLogic.mk_comp (fld, Term.list_comb (map, passive_ids @ rec_fsts)), prod_s))
  1225           flds rec_ss rec_maps;
  1226 
  1227         val lhs = Term.list_comb (Free (rec_name i, recT), rec_ss);
  1228         val rhs = HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_iter Ts maps i);
  1229       in
  1230         mk_Trueprop_eq (lhs, rhs)
  1231       end;
  1232 
  1233     val ((rec_frees, (_, rec_def_frees)), (lthy, lthy_old)) =
  1234         lthy
  1235         |> fold_map3 (fn i => fn T => fn AT =>
  1236           Specification.definition
  1237             (SOME (rec_bind i, NONE, NoSyn), (rec_def_bind i, rec_spec i T AT)))
  1238             ks Ts activeAs
  1239         |>> apsnd split_list o split_list
  1240         ||> `Local_Theory.restore;
  1241 
  1242     (*transforms defined frees into consts*)
  1243     val phi = Proof_Context.export_morphism lthy_old lthy;
  1244     val recs = map (Morphism.term phi) rec_frees;
  1245     val rec_names = map (fst o dest_Const) recs;
  1246     fun mk_rec ss i = Term.list_comb (Const (nth rec_names (i - 1), Library.foldr (op -->)
  1247       (map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss);
  1248     val rec_defs = map (Morphism.thm phi) rec_def_frees;
  1249 
  1250     val convols = map2 (fn T => fn i => mk_convol (HOLogic.id_const T, mk_rec rec_ss i)) Ts ks;
  1251     val rec_thms =
  1252       let
  1253         fun mk_goal i rec_s rec_map fld x =
  1254           let
  1255             val lhs = mk_rec rec_ss i $ (fld $ x);
  1256             val rhs = rec_s $ (Term.list_comb (rec_map, passive_ids @ convols) $ x);
  1257           in
  1258             fold_rev Logic.all (x :: rec_ss) (mk_Trueprop_eq (lhs, rhs))
  1259           end;
  1260         val goals = map5 mk_goal ks rec_ss rec_maps_rev flds xFs;
  1261       in
  1262         map2 (fn goal => fn iter =>
  1263           Skip_Proof.prove lthy [] [] goal (mk_rec_tac rec_defs iter fst_rec_pair_thms)
  1264           |> Thm.close_derivation)
  1265         goals iter_thms
  1266       end;
  1267 
  1268     val timer = time (timer "rec definitions & thms");
  1269 
  1270     val (fld_induct_thm, induct_params) =
  1271       let
  1272         fun mk_prem phi fld sets x =
  1273           let
  1274             fun mk_IH phi set z =
  1275               let
  1276                 val prem = HOLogic.mk_Trueprop (HOLogic.mk_mem (z, set $ x));
  1277                 val concl = HOLogic.mk_Trueprop (phi $ z);
  1278               in
  1279                 Logic.all z (Logic.mk_implies (prem, concl))
  1280               end;
  1281 
  1282             val IHs = map3 mk_IH phis (drop m sets) Izs;
  1283             val concl = HOLogic.mk_Trueprop (phi $ (fld $ x));
  1284           in
  1285             Logic.all x (Logic.list_implies (IHs, concl))
  1286           end;
  1287 
  1288         val prems = map4 mk_prem phis flds FTs_setss xFs;
  1289 
  1290         fun mk_concl phi z = phi $ z;
  1291         val concl =
  1292           HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_concl phis Izs));
  1293 
  1294         val goal = Logic.list_implies (prems, concl);
  1295       in
  1296         (Skip_Proof.prove lthy [] []
  1297           (fold_rev Logic.all (phis @ Izs) goal)
  1298           (K (mk_fld_induct_tac m set_natural'ss init_induct_thm morE_thms mor_Abs_thm
  1299             Rep_inverses Abs_inverses Reps))
  1300         |> Thm.close_derivation,
  1301         rev (Term.add_tfrees goal []))
  1302       end;
  1303 
  1304     val cTs = map (SOME o certifyT lthy o TFree) induct_params;
  1305 
  1306     val weak_fld_induct_thms =
  1307       let fun insts i = (replicate (i - 1) TrueI) @ (@{thm asm_rl} :: replicate (n - i) TrueI);
  1308       in map (fn i => (fld_induct_thm OF insts i) RS mk_conjunctN n i) ks end;
  1309 
  1310     val (fld_induct2_thm, induct2_params) =
  1311       let
  1312         fun mk_prem phi fld fld' sets sets' x y =
  1313           let
  1314             fun mk_IH phi set set' z1 z2 =
  1315               let
  1316                 val prem1 = HOLogic.mk_Trueprop (HOLogic.mk_mem (z1, (set $ x)));
  1317                 val prem2 = HOLogic.mk_Trueprop (HOLogic.mk_mem (z2, (set' $ y)));
  1318                 val concl = HOLogic.mk_Trueprop (phi $ z1 $ z2);
  1319               in
  1320                 fold_rev Logic.all [z1, z2] (Logic.list_implies ([prem1, prem2], concl))
  1321               end;
  1322 
  1323             val IHs = map5 mk_IH phi2s (drop m sets) (drop m sets') Izs1 Izs2;
  1324             val concl = HOLogic.mk_Trueprop (phi $ (fld $ x) $ (fld' $ y));
  1325           in
  1326             fold_rev Logic.all [x, y] (Logic.list_implies (IHs, concl))
  1327           end;
  1328 
  1329         val prems = map7 mk_prem phi2s flds fld's FTs_setss FTs'_setss xFs yFs;
  1330 
  1331         fun mk_concl phi z1 z2 = phi $ z1 $ z2;
  1332         val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  1333           (map3 mk_concl phi2s Izs1 Izs2));
  1334         fun mk_t phi (z1, z1') (z2, z2') =
  1335           Term.absfree z1' (HOLogic.mk_all (fst z2', snd z2', phi $ z1 $ z2));
  1336         val cts = map3 (SOME o certify lthy ooo mk_t) phi2s (Izs1 ~~ Izs1') (Izs2 ~~ Izs2');
  1337         val goal = Logic.list_implies (prems, concl);
  1338       in
  1339         (singleton (Proof_Context.export names_lthy lthy)
  1340           (Skip_Proof.prove lthy [] [] goal
  1341             (mk_fld_induct2_tac cTs cts fld_induct_thm weak_fld_induct_thms))
  1342           |> Thm.close_derivation,
  1343         rev (Term.add_tfrees goal []))
  1344       end;
  1345 
  1346     val timer = time (timer "induction");
  1347 
  1348     (*register new datatypes as BNFs*)
  1349     val lthy = if m = 0 then lthy else
  1350       let
  1351         val fTs = map2 (curry op -->) passiveAs passiveBs;
  1352         val f1Ts = map2 (curry op -->) passiveAs passiveYs;
  1353         val f2Ts = map2 (curry op -->) passiveBs passiveYs;
  1354         val p1Ts = map2 (curry op -->) passiveXs passiveAs;
  1355         val p2Ts = map2 (curry op -->) passiveXs passiveBs;
  1356         val uTs = map2 (curry op -->) Ts Ts';
  1357         val B1Ts = map HOLogic.mk_setT passiveAs;
  1358         val B2Ts = map HOLogic.mk_setT passiveBs;
  1359         val AXTs = map HOLogic.mk_setT passiveXs;
  1360         val XTs = mk_Ts passiveXs;
  1361         val YTs = mk_Ts passiveYs;
  1362         val IRTs = map2 (curry mk_relT) passiveAs passiveBs;
  1363         val IphiTs = map2 (fn T => fn U => T --> U --> HOLogic.boolT) passiveAs passiveBs;
  1364 
  1365         val (((((((((((((((fs, fs'), fs_copy), us),
  1366           B1s), B2s), AXs), (xs, xs')), f1s), f2s), p1s), p2s), (ys, ys')), IRs), Iphis),
  1367           names_lthy) = names_lthy
  1368           |> mk_Frees' "f" fTs
  1369           ||>> mk_Frees "f" fTs
  1370           ||>> mk_Frees "u" uTs
  1371           ||>> mk_Frees "B1" B1Ts
  1372           ||>> mk_Frees "B2" B2Ts
  1373           ||>> mk_Frees "A" AXTs
  1374           ||>> mk_Frees' "x" XTs
  1375           ||>> mk_Frees "f1" f1Ts
  1376           ||>> mk_Frees "f2" f2Ts
  1377           ||>> mk_Frees "p1" p1Ts
  1378           ||>> mk_Frees "p2" p2Ts
  1379           ||>> mk_Frees' "y" passiveAs
  1380           ||>> mk_Frees "R" IRTs
  1381           ||>> mk_Frees "phi" IphiTs;
  1382 
  1383         val map_FTFT's = map2 (fn Ds =>
  1384           mk_map_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
  1385         fun mk_passive_maps ATs BTs Ts =
  1386           map2 (fn Ds => mk_map_of_bnf Ds (ATs @ Ts) (BTs @ Ts)) Dss bnfs;
  1387         fun mk_map_iter_arg fs Ts fld fmap =
  1388           HOLogic.mk_comp (fld, Term.list_comb (fmap, fs @ map HOLogic.id_const Ts));
  1389         fun mk_map Ts fs Ts' flds mk_maps =
  1390           mk_iter Ts (map2 (mk_map_iter_arg fs Ts') flds (mk_maps Ts'));
  1391         val pmapsABT' = mk_passive_maps passiveAs passiveBs;
  1392         val fs_maps = map (mk_map Ts fs Ts' fld's pmapsABT') ks;
  1393         val fs_copy_maps = map (mk_map Ts fs_copy Ts' fld's pmapsABT') ks;
  1394         val Yflds = mk_flds passiveYs;
  1395         val f1s_maps = map (mk_map Ts f1s YTs Yflds (mk_passive_maps passiveAs passiveYs)) ks;
  1396         val f2s_maps = map (mk_map Ts' f2s YTs Yflds (mk_passive_maps passiveBs passiveYs)) ks;
  1397         val p1s_maps = map (mk_map XTs p1s Ts flds (mk_passive_maps passiveXs passiveAs)) ks;
  1398         val p2s_maps = map (mk_map XTs p2s Ts' fld's (mk_passive_maps passiveXs passiveBs)) ks;
  1399 
  1400         val (map_simp_thms, map_thms) =
  1401           let
  1402             fun mk_goal fs_map map fld fld' = fold_rev Logic.all fs
  1403               (mk_Trueprop_eq (HOLogic.mk_comp (fs_map, fld),
  1404                 HOLogic.mk_comp (fld', Term.list_comb (map, fs @ fs_maps))));
  1405             val goals = map4 mk_goal fs_maps map_FTFT's flds fld's;
  1406             val maps =
  1407               map4 (fn goal => fn iter => fn map_comp_id => fn map_cong =>
  1408                 Skip_Proof.prove lthy [] [] goal (K (mk_map_tac m n iter map_comp_id map_cong))
  1409                 |> Thm.close_derivation)
  1410               goals iter_thms map_comp_id_thms map_congs;
  1411           in
  1412             map_split (fn thm => (thm RS @{thm pointfreeE}, thm)) maps
  1413           end;
  1414 
  1415         val (map_unique_thms, map_unique_thm) =
  1416           let
  1417             fun mk_prem u map fld fld' =
  1418               mk_Trueprop_eq (HOLogic.mk_comp (u, fld),
  1419                 HOLogic.mk_comp (fld', Term.list_comb (map, fs @ us)));
  1420             val prems = map4 mk_prem us map_FTFT's flds fld's;
  1421             val goal =
  1422               HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  1423                 (map2 (curry HOLogic.mk_eq) us fs_maps));
  1424             val unique = Skip_Proof.prove lthy [] []
  1425               (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
  1426               (K (mk_map_unique_tac m mor_def iter_unique_mor_thm map_comp_id_thms map_congs))
  1427               |> Thm.close_derivation;
  1428           in
  1429             `split_conj_thm unique
  1430           end;
  1431 
  1432         val timer = time (timer "map functions for the new datatypes");
  1433 
  1434         val bd = mk_cpow sum_bd;
  1435         val bd_Cinfinite = sum_Cinfinite RS @{thm Cinfinite_cpow};
  1436         fun mk_cpow_bd thm = @{thm ordLeq_transitive} OF
  1437           [thm, sum_Card_order RS @{thm cpow_greater_eq}];
  1438         val set_bd_cpowss = map (map mk_cpow_bd) set_bd_sumss;
  1439 
  1440         val timer = time (timer "bounds for the new datatypes");
  1441 
  1442         val ls = 1 upto m;
  1443         val setsss = map (mk_setss o mk_set_Ts) passiveAs;
  1444         val map_setss = map (fn T => map2 (fn Ds =>
  1445           mk_map_of_bnf Ds (passiveAs @ Ts) (mk_set_Ts T)) Dss bnfs) passiveAs;
  1446 
  1447         fun mk_col l T z z' sets =
  1448           let
  1449             fun mk_UN set = mk_Union T $ (set $ z);
  1450           in
  1451             Term.absfree z'
  1452               (mk_union (nth sets (l - 1) $ z,
  1453                 Library.foldl1 mk_union (map mk_UN (drop m sets))))
  1454           end;
  1455 
  1456         val colss = map5 (fn l => fn T => map3 (mk_col l T)) ls passiveAs AFss AFss' setsss;
  1457         val setss_by_range = map (fn cols => map (mk_iter Ts cols) ks) colss;
  1458         val setss_by_bnf = transpose setss_by_range;
  1459 
  1460         val (set_simp_thmss, set_thmss) =
  1461           let
  1462             fun mk_goal sets fld set col map =
  1463               mk_Trueprop_eq (HOLogic.mk_comp (set, fld),
  1464                 HOLogic.mk_comp (col, Term.list_comb (map, passive_ids @ sets)));
  1465             val goalss =
  1466               map3 (fn sets => map4 (mk_goal sets) flds sets) setss_by_range colss map_setss;
  1467             val setss = map (map2 (fn iter => fn goal =>
  1468               Skip_Proof.prove lthy [] [] goal (K (mk_set_tac iter)) |> Thm.close_derivation)
  1469               iter_thms) goalss;
  1470 
  1471             fun mk_simp_goal pas_set act_sets sets fld z set =
  1472               Logic.all z (mk_Trueprop_eq (set $ (fld $ z),
  1473                 mk_union (pas_set $ z,
  1474                   Library.foldl1 mk_union (map2 (fn X => mk_UNION (X $ z)) act_sets sets))));
  1475             val simp_goalss =
  1476               map2 (fn i => fn sets =>
  1477                 map4 (fn Fsets => mk_simp_goal (nth Fsets (i - 1)) (drop m Fsets) sets)
  1478                   FTs_setss flds xFs sets)
  1479                 ls setss_by_range;
  1480 
  1481             val set_simpss = map3 (fn i => map3 (fn set_nats => fn goal => fn set =>
  1482                 Skip_Proof.prove lthy [] [] goal
  1483                   (K (mk_set_simp_tac set (nth set_nats (i - 1)) (drop m set_nats)))
  1484                 |> Thm.close_derivation)
  1485               set_natural'ss) ls simp_goalss setss;
  1486           in
  1487             (set_simpss, setss)
  1488           end;
  1489 
  1490         fun mk_set_thms set_simp = (@{thm xt1(3)} OF [set_simp, @{thm Un_upper1}]) ::
  1491           map (fn i => (@{thm xt1(3)} OF [set_simp, @{thm Un_upper2}]) RS
  1492             (mk_Un_upper n i RS subset_trans) RSN
  1493             (2, @{thm UN_upper} RS subset_trans))
  1494             (1 upto n);
  1495         val Fset_set_thmsss = transpose (map (map mk_set_thms) set_simp_thmss);
  1496 
  1497         val timer = time (timer "set functions for the new datatypes");
  1498 
  1499         val cxs = map (SOME o certify lthy) Izs;
  1500         val setss_by_bnf' =
  1501           map (map (Term.subst_atomic_types (passiveAs ~~ passiveBs))) setss_by_bnf;
  1502         val setss_by_range' = transpose setss_by_bnf';
  1503 
  1504         val set_natural_thmss =
  1505           let
  1506             fun mk_set_natural f map z set set' =
  1507               HOLogic.mk_eq (mk_image f $ (set $ z), set' $ (map $ z));
  1508 
  1509             fun mk_cphi f map z set set' = certify lthy
  1510               (Term.absfree (dest_Free z) (mk_set_natural f map z set set'));
  1511 
  1512             val csetss = map (map (certify lthy)) setss_by_range';
  1513 
  1514             val cphiss = map3 (fn f => fn sets => fn sets' =>
  1515               (map4 (mk_cphi f) fs_maps Izs sets sets')) fs setss_by_range setss_by_range';
  1516 
  1517             val inducts = map (fn cphis =>
  1518               Drule.instantiate' cTs (map SOME cphis @ cxs) fld_induct_thm) cphiss;
  1519 
  1520             val goals =
  1521               map3 (fn f => fn sets => fn sets' =>
  1522                 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  1523                   (map4 (mk_set_natural f) fs_maps Izs sets sets')))
  1524                   fs setss_by_range setss_by_range';
  1525 
  1526             fun mk_tac induct = mk_set_nat_tac m (rtac induct) set_natural'ss map_simp_thms;
  1527             val thms =
  1528               map5 (fn goal => fn csets => fn set_simps => fn induct => fn i =>
  1529                 singleton (Proof_Context.export names_lthy lthy)
  1530                   (Skip_Proof.prove lthy [] [] goal (mk_tac induct csets set_simps i))
  1531                 |> Thm.close_derivation)
  1532               goals csetss set_simp_thmss inducts ls;
  1533           in
  1534             map split_conj_thm thms
  1535           end;
  1536 
  1537         val set_bd_thmss =
  1538           let
  1539             fun mk_set_bd z set = mk_ordLeq (mk_card_of (set $ z)) bd;
  1540 
  1541             fun mk_cphi z set = certify lthy (Term.absfree (dest_Free z) (mk_set_bd z set));
  1542 
  1543             val cphiss = map (map2 mk_cphi Izs) setss_by_range;
  1544 
  1545             val inducts = map (fn cphis =>
  1546               Drule.instantiate' cTs (map SOME cphis @ cxs) fld_induct_thm) cphiss;
  1547 
  1548             val goals =
  1549               map (fn sets =>
  1550                 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  1551                   (map2 mk_set_bd Izs sets))) setss_by_range;
  1552 
  1553             fun mk_tac induct = mk_set_bd_tac m (rtac induct) bd_Cinfinite set_bd_cpowss;
  1554             val thms =
  1555               map4 (fn goal => fn set_simps => fn induct => fn i =>
  1556                 singleton (Proof_Context.export names_lthy lthy)
  1557                   (Skip_Proof.prove lthy [] [] goal (mk_tac induct set_simps i))
  1558                 |> Thm.close_derivation)
  1559               goals set_simp_thmss inducts ls;
  1560           in
  1561             map split_conj_thm thms
  1562           end;
  1563 
  1564         val map_cong_thms =
  1565           let
  1566             fun mk_prem z set f g y y' =
  1567               mk_Ball (set $ z) (Term.absfree y' (HOLogic.mk_eq (f $ y, g $ y)));
  1568 
  1569             fun mk_map_cong sets z fmap gmap =
  1570               HOLogic.mk_imp
  1571                 (Library.foldr1 HOLogic.mk_conj (map5 (mk_prem z) sets fs fs_copy ys ys'),
  1572                 HOLogic.mk_eq (fmap $ z, gmap $ z));
  1573 
  1574             fun mk_cphi sets z fmap gmap =
  1575               certify lthy (Term.absfree (dest_Free z) (mk_map_cong sets z fmap gmap));
  1576 
  1577             val cphis = map4 mk_cphi setss_by_bnf Izs fs_maps fs_copy_maps;
  1578 
  1579             val induct = Drule.instantiate' cTs (map SOME cphis @ cxs) fld_induct_thm;
  1580 
  1581             val goal =
  1582               HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  1583                 (map4 mk_map_cong setss_by_bnf Izs fs_maps fs_copy_maps));
  1584 
  1585             val thm = singleton (Proof_Context.export names_lthy lthy)
  1586               (Skip_Proof.prove lthy [] [] goal
  1587               (mk_mcong_tac (rtac induct) Fset_set_thmsss map_congs map_simp_thms))
  1588               |> Thm.close_derivation;
  1589           in
  1590             split_conj_thm thm
  1591           end;
  1592 
  1593         val in_incl_min_alg_thms =
  1594           let
  1595             fun mk_prem z sets =
  1596               HOLogic.mk_mem (z, mk_in As sets (fastype_of z));
  1597 
  1598             fun mk_incl z sets i =
  1599               HOLogic.mk_imp (mk_prem z sets, HOLogic.mk_mem (z, mk_min_alg As flds i));
  1600 
  1601             fun mk_cphi z sets i =
  1602               certify lthy (Term.absfree (dest_Free z) (mk_incl z sets i));
  1603 
  1604             val cphis = map3 mk_cphi Izs setss_by_bnf ks;
  1605 
  1606             val induct = Drule.instantiate' cTs (map SOME cphis @ cxs) fld_induct_thm;
  1607 
  1608             val goal =
  1609               HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  1610                 (map3 mk_incl Izs setss_by_bnf ks));
  1611 
  1612             val thm = singleton (Proof_Context.export names_lthy lthy)
  1613               (Skip_Proof.prove lthy [] [] goal
  1614               (mk_incl_min_alg_tac (rtac induct) Fset_set_thmsss alg_set_thms alg_min_alg_thm))
  1615               |> Thm.close_derivation;
  1616           in
  1617             split_conj_thm thm
  1618           end;
  1619 
  1620         val Xsetss = map (map (Term.subst_atomic_types (passiveAs ~~ passiveXs))) setss_by_bnf;
  1621 
  1622         val map_wpull_thms =
  1623           let
  1624             val cTs = map (SOME o certifyT lthy o TFree) induct2_params;
  1625             val cxs = map (SOME o certify lthy) (interleave Izs1 Izs2);
  1626 
  1627             fun mk_prem z1 z2 sets1 sets2 map1 map2 =
  1628               HOLogic.mk_conj
  1629                 (HOLogic.mk_mem (z1, mk_in B1s sets1 (fastype_of z1)),
  1630                 HOLogic.mk_conj
  1631                   (HOLogic.mk_mem (z2, mk_in B2s sets2 (fastype_of z2)),
  1632                   HOLogic.mk_eq (map1 $ z1, map2 $ z2)));
  1633 
  1634             val prems = map6 mk_prem Izs1 Izs2 setss_by_bnf setss_by_bnf' f1s_maps f2s_maps;
  1635 
  1636             fun mk_concl z1 z2 sets map1 map2 T x x' =
  1637               mk_Bex (mk_in AXs sets T) (Term.absfree x'
  1638                 (HOLogic.mk_conj (HOLogic.mk_eq (map1 $ x, z1), HOLogic.mk_eq (map2 $ x, z2))));
  1639 
  1640             val concls = map8 mk_concl Izs1 Izs2 Xsetss p1s_maps p2s_maps XTs xs xs';
  1641 
  1642             val goals = map2 (curry HOLogic.mk_imp) prems concls;
  1643 
  1644             fun mk_cphi z1 z2 goal = certify lthy (Term.absfree z1 (Term.absfree z2 goal));
  1645 
  1646             val cphis = map3 mk_cphi Izs1' Izs2' goals;
  1647 
  1648             val induct = Drule.instantiate' cTs (map SOME cphis @ cxs) fld_induct2_thm;
  1649 
  1650             val goal = Logic.list_implies (map HOLogic.mk_Trueprop
  1651                 (map8 mk_wpull AXs B1s B2s f1s f2s (replicate m NONE) p1s p2s),
  1652               HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals));
  1653 
  1654             val thm = singleton (Proof_Context.export names_lthy lthy)
  1655               (Skip_Proof.prove lthy [] [] goal
  1656               (K (mk_lfp_map_wpull_tac m (rtac induct) map_wpulls map_simp_thms
  1657                 (transpose set_simp_thmss) Fset_set_thmsss fld_inject_thms)))
  1658               |> Thm.close_derivation;
  1659           in
  1660             split_conj_thm thm
  1661           end;
  1662 
  1663         val timer = time (timer "helpers for BNF properties");
  1664 
  1665         val map_id_tacs = map (K o mk_map_id_tac map_ids) map_unique_thms;
  1666         val map_comp_tacs =
  1667           map2 (K oo mk_map_comp_tac map_comp's map_simp_thms) map_unique_thms ks;
  1668         val map_cong_tacs = map (mk_map_cong_tac m) map_cong_thms;
  1669         val set_nat_tacss = map (map (K o mk_set_natural_tac)) (transpose set_natural_thmss);
  1670         val bd_co_tacs = replicate n (K (mk_bd_card_order_tac bd_card_orders));
  1671         val bd_cinf_tacs = replicate n (K (rtac (bd_Cinfinite RS conjunct1) 1));
  1672         val set_bd_tacss = map (map (fn thm => K (rtac thm 1))) (transpose set_bd_thmss);
  1673         val in_bd_tacs = map2 (K oo mk_in_bd_tac sum_Card_order suc_bd_Cnotzero)
  1674           in_incl_min_alg_thms card_of_min_alg_thms;
  1675         val map_wpull_tacs = map (K o mk_wpull_tac) map_wpull_thms;
  1676 
  1677         val tacss = map9 mk_tactics map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss bd_co_tacs
  1678           bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs;
  1679 
  1680         val fld_witss =
  1681           let
  1682             val witss = map2 (fn Ds => fn bnf => mk_wits_of_bnf
  1683               (replicate (nwits_of_bnf bnf) Ds)
  1684               (replicate (nwits_of_bnf bnf) (passiveAs @ Ts)) bnf) Dss bnfs;
  1685             fun close_wit (I, wit) = fold_rev Term.absfree (map (nth ys') I) wit;
  1686             fun wit_apply (arg_I, arg_wit) (fun_I, fun_wit) =
  1687               (union (op =) arg_I fun_I, fun_wit $ arg_wit);
  1688 
  1689             fun gen_arg support i =
  1690               if i < m then [([i], nth ys i)]
  1691               else maps (mk_wit support (nth flds (i - m)) (i - m)) (nth support (i - m))
  1692             and mk_wit support fld i (I, wit) =
  1693               let val args = map (gen_arg (nth_map i (remove (op =) (I, wit)) support)) I;
  1694               in
  1695                 (args, [([], wit)])
  1696                 |-> fold (map_product wit_apply)
  1697                 |> map (apsnd (fn t => fld $ t))
  1698                 |> minimize_wits
  1699               end;
  1700           in
  1701             map3 (fn fld => fn i => map close_wit o minimize_wits o maps (mk_wit witss fld i))
  1702               flds (0 upto n - 1) witss
  1703           end;
  1704 
  1705         fun wit_tac _ = mk_wit_tac n (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs);
  1706 
  1707         val (Ibnfs, lthy) =
  1708           fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn wits =>
  1709             bnf_def Dont_Inline user_policy I tacs wit_tac (SOME deads)
  1710               ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits))
  1711           tacss bs fs_maps setss_by_bnf Ts fld_witss lthy;
  1712 
  1713         val fold_maps = Local_Defs.fold lthy (map (fn bnf =>
  1714           mk_unabs_def m (map_def_of_bnf bnf RS @{thm meta_eq_to_obj_eq})) Ibnfs);
  1715 
  1716         val fold_sets = Local_Defs.fold lthy (maps (fn bnf =>
  1717          map (fn thm => thm RS @{thm meta_eq_to_obj_eq}) (set_defs_of_bnf bnf)) Ibnfs);
  1718 
  1719         val timer = time (timer "registered new datatypes as BNFs");
  1720 
  1721         val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
  1722         val Irels = map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;
  1723         val preds = map2 (fn Ds => mk_pred_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
  1724         val Ipreds = map (mk_pred_of_bnf deads passiveAs passiveBs) Ibnfs;
  1725 
  1726         val IrelRs = map (fn Irel => Term.list_comb (Irel, IRs)) Irels;
  1727         val relRs = map (fn rel => Term.list_comb (rel, IRs @ IrelRs)) rels;
  1728         val Ipredphis = map (fn Irel => Term.list_comb (Irel, Iphis)) Ipreds;
  1729         val predphis = map (fn rel => Term.list_comb (rel, Iphis @ Ipredphis)) preds;
  1730 
  1731         val in_rels = map in_rel_of_bnf bnfs;
  1732         val in_Irels = map in_rel_of_bnf Ibnfs;
  1733         val pred_defs = map pred_def_of_bnf bnfs;
  1734         val Ipred_defs =
  1735           map (Drule.abs_def o (fn thm => thm RS @{thm eq_reflection}) o pred_def_of_bnf) Ibnfs;
  1736 
  1737         val set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss;
  1738         val set_set_incl_thmsss = map (transpose o map (map fold_sets o tl)) Fset_set_thmsss;
  1739         val folded_map_simp_thms = map fold_maps map_simp_thms;
  1740         val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss;
  1741         val folded_set_simp_thmss' = transpose folded_set_simp_thmss;
  1742 
  1743         val Irel_unfold_thms =
  1744           let
  1745             fun mk_goal xF yF fld fld' IrelR relR = fold_rev Logic.all (xF :: yF :: IRs)
  1746               (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (fld $ xF, fld' $ yF), IrelR),
  1747                   HOLogic.mk_mem (HOLogic.mk_prod (xF, yF), relR)));
  1748             val goals = map6 mk_goal xFs yFs flds fld's IrelRs relRs;
  1749           in
  1750             map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong =>
  1751               fn map_simp => fn set_simps => fn fld_inject => fn fld_unf =>
  1752               fn set_naturals => fn set_incls => fn set_set_inclss =>
  1753               Skip_Proof.prove lthy [] [] goal
  1754                (K (mk_rel_unfold_tac in_Irels i in_rel map_comp map_cong map_simp set_simps
  1755                  fld_inject fld_unf set_naturals set_incls set_set_inclss))
  1756               |> Thm.close_derivation)
  1757             ks goals in_rels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss'
  1758               fld_inject_thms fld_unf_thms set_natural'ss set_incl_thmss set_set_incl_thmsss
  1759           end;
  1760 
  1761         val Ipred_unfold_thms =
  1762           let
  1763             fun mk_goal xF yF fld fld' Ipredphi predphi = fold_rev Logic.all (xF :: yF :: Iphis)
  1764               (mk_Trueprop_eq (Ipredphi $ (fld $ xF) $ (fld' $ yF), predphi $ xF $ yF));
  1765             val goals = map6 mk_goal xFs yFs flds fld's Ipredphis predphis;
  1766           in
  1767             map3 (fn goal => fn pred_def => fn Irel_unfold =>
  1768               Skip_Proof.prove lthy [] [] goal (mk_pred_unfold_tac pred_def Ipred_defs Irel_unfold)
  1769               |> Thm.close_derivation)
  1770             goals pred_defs Irel_unfold_thms
  1771           end;
  1772 
  1773         val timer = time (timer "additional properties");
  1774 
  1775         val ls' = if m = 1 then [0] else ls
  1776 
  1777         val Ibnf_common_notes =
  1778           [(map_uniqueN, [fold_maps map_unique_thm])]
  1779           |> map (fn (thmN, thms) =>
  1780             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
  1781 
  1782         val Ibnf_notes =
  1783           [(map_simpsN, map single folded_map_simp_thms),
  1784           (set_inclN, set_incl_thmss),
  1785           (set_set_inclN, map flat set_set_incl_thmsss),
  1786           (rel_unfoldN, map single Irel_unfold_thms),
  1787           (pred_unfoldN, map single Ipred_unfold_thms)] @
  1788           map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss
  1789           |> maps (fn (thmN, thmss) =>
  1790             map2 (fn b => fn thms =>
  1791               ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
  1792             bs thmss)
  1793       in
  1794         lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd
  1795       end;
  1796 
  1797       val common_notes =
  1798         [(fld_inductN, [fld_induct_thm]),
  1799         (fld_induct2N, [fld_induct2_thm])]
  1800         |> map (fn (thmN, thms) =>
  1801           ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
  1802 
  1803       val notes =
  1804         [(fld_itersN, iter_thms),
  1805         (fld_iter_uniqueN, iter_unique_thms),
  1806         (fld_recsN, rec_thms),
  1807         (unf_fldN, unf_fld_thms),
  1808         (fld_unfN, fld_unf_thms),
  1809         (unf_injectN, unf_inject_thms),
  1810         (unf_exhaustN, unf_exhaust_thms),
  1811         (fld_injectN, fld_inject_thms),
  1812         (fld_exhaustN, fld_exhaust_thms)]
  1813         |> map (apsnd (map single))
  1814         |> maps (fn (thmN, thmss) =>
  1815           map2 (fn b => fn thms =>
  1816             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
  1817           bs thmss)
  1818   in
  1819     ((unfs, flds, iters, recs, unf_fld_thms, fld_unf_thms, fld_inject_thms, iter_thms, rec_thms),
  1820      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
  1821   end;
  1822 
  1823 val _ =
  1824   Outer_Syntax.local_theory @{command_spec "data_raw"} "least fixed points of BNF equations"
  1825     (Parse.and_list1
  1826       ((Parse.binding --| @{keyword ":"}) -- (Parse.typ --| @{keyword "="} -- Parse.typ)) >>
  1827       (snd oo fp_bnf_cmd bnf_lfp o apsnd split_list o split_list));
  1828 
  1829 end;