src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
author blanchet
Mon Apr 29 13:47:46 2013 +0200 (2013-04-29)
changeset 51814 8b89afea27e7
parent 51813 ca201253e7bb
child 51815 efacb9b99865
permissions -rw-r--r--
tuning
     1 (*  Title:      HOL/BNF/Tools/bnf_fp_def_sugar.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2012
     4 
     5 Sugared datatype and codatatype constructions.
     6 *)
     7 
     8 signature BNF_FP_DEF_SUGAR =
     9 sig
    10   val derive_induct_fold_rec_thms_for_types: int -> BNF_Def.BNF list -> thm -> thm list ->
    11     thm list -> BNF_Def.BNF list -> BNF_Def.BNF list -> typ list -> typ list ->
    12     typ list list list -> int list list -> int list -> term list list -> term list list ->
    13     term list list -> term list list list -> thm list list -> term list -> term list -> thm list ->
    14     thm list -> Proof.context ->
    15     (thm * thm list * Args.src list) * (thm list list * Args.src list)
    16       * (thm list list * Args.src list)
    17   val derive_coinduct_unfold_corec_thms_for_types: Proof.context -> Proof.context -> int ->
    18     BNF_Def.BNF list -> thm -> thm -> thm list -> thm list -> thm list -> BNF_Def.BNF list ->
    19     BNF_Def.BNF list -> typ list -> typ list -> typ list -> int list list -> int list list ->
    20     int list -> term list -> term list list -> term list list -> term list list list list ->
    21     term list list list list -> term list list -> term list list list list ->
    22     term list list list list -> term list list -> thm list list ->
    23     BNF_Ctr_Sugar.ctr_wrap_result list -> term list -> term list -> thm list -> thm list ->
    24     Proof.context ->
    25     (thm * thm list * thm * thm list * Args.src list) * (thm list list * thm list list * 'e list)
    26     * (thm list list * thm list list) * (thm list list * thm list list * Args.src list)
    27     * (thm list list * thm list list * Args.src list) *
    28     (thm list list * thm list list * Args.src list)
    29   val datatypes: bool ->
    30     (mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list ->
    31       binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
    32       BNF_FP.fp_result * local_theory) ->
    33     (bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix) *
    34       ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
    35         mixfix) list) list ->
    36     local_theory -> local_theory
    37   val parse_datatype_cmd: bool ->
    38     (mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list ->
    39       binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
    40       BNF_FP.fp_result * local_theory) ->
    41     (local_theory -> local_theory) parser
    42 end;
    43 
    44 structure BNF_FP_Def_Sugar : BNF_FP_DEF_SUGAR =
    45 struct
    46 
    47 open BNF_Util
    48 open BNF_Ctr_Sugar
    49 open BNF_Def
    50 open BNF_FP
    51 open BNF_FP_Def_Sugar_Tactics
    52 
    53 val EqN = "Eq_";
    54 
    55 (* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *)
    56 fun quasi_unambiguous_case_names names =
    57   let
    58     val ps = map (`Long_Name.base_name) names;
    59     val dups = Library.duplicates (op =) (map fst ps);
    60     fun underscore s =
    61       let val ss = space_explode Long_Name.separator s in
    62         space_implode "_" (drop (length ss - 2) ss)
    63       end;
    64   in
    65     map (fn (base, full) => if member (op =) dups base then underscore full else base) ps
    66   end;
    67 
    68 val mp_conj = @{thm mp_conj};
    69 
    70 val simp_attrs = @{attributes [simp]};
    71 val code_simp_attrs = Code.add_default_eqn_attrib :: simp_attrs;
    72 
    73 fun split_list4 [] = ([], [], [], [])
    74   | split_list4 ((x1, x2, x3, x4) :: xs) =
    75     let val (xs1, xs2, xs3, xs4) = split_list4 xs;
    76     in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4) end;
    77 
    78 fun add_components_of_typ (Type (s, Ts)) =
    79     fold add_components_of_typ Ts
    80     #> cons s
    81   | add_components_of_typ _ = I;
    82 
    83 fun name_of_typ T = space_implode "_" (add_components_of_typ T []);
    84 
    85 fun exists_subtype_in Ts = exists_subtype (member (op =) Ts);
    86 
    87 fun resort_tfree S (TFree (s, _)) = TFree (s, S);
    88 
    89 fun typ_subst inst (T as Type (s, Ts)) =
    90     (case AList.lookup (op =) inst T of
    91       NONE => Type (s, map (typ_subst inst) Ts)
    92     | SOME T' => T')
    93   | typ_subst inst T = the_default T (AList.lookup (op =) inst T);
    94 
    95 fun variant_types ss Ss ctxt =
    96   let
    97     val (tfrees, _) =
    98       fold_map2 (fn s => fn S => Name.variant s #> apfst (rpair S)) ss Ss (Variable.names_of ctxt);
    99     val ctxt' = fold (Variable.declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
   100   in (tfrees, ctxt') end;
   101 
   102 val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs));
   103 
   104 fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs));
   105 fun mk_uncurried_fun f xs = mk_tupled_fun (HOLogic.mk_tuple xs) f xs;
   106 
   107 fun flat_rec unzipf xs =
   108   let val ps = map unzipf xs in
   109     (* The first line below gives the preferred order. The second line is for compatibility with the
   110        old datatype package: *)
   111 (*
   112     maps (op @) ps
   113 *)
   114     maps fst ps @ maps snd ps
   115   end;
   116 
   117 fun mk_flip (x, Type (_, [T1, Type (_, [T2, T3])])) =
   118   Abs ("x", T1, Abs ("y", T2, Var (x, T2 --> T1 --> T3) $ Bound 0 $ Bound 1));
   119 
   120 fun flip_rels lthy n thm =
   121   let
   122     val Rs = Term.add_vars (prop_of thm) [];
   123     val Rs' = rev (drop (length Rs - n) Rs);
   124     val cRs = map (fn f => (certify lthy (Var f), certify lthy (mk_flip f))) Rs';
   125   in
   126     Drule.cterm_instantiate cRs thm
   127   end;
   128 
   129 fun mk_ctor_or_dtor get_T Ts t =
   130   let val Type (_, Ts0) = get_T (fastype_of t) in
   131     Term.subst_atomic_types (Ts0 ~~ Ts) t
   132   end;
   133 
   134 val mk_ctor = mk_ctor_or_dtor range_type;
   135 val mk_dtor = mk_ctor_or_dtor domain_type;
   136 
   137 fun mk_rec_like lfp Ts Us t =
   138   let
   139     val (bindings, body) = strip_type (fastype_of t);
   140     val (f_Us, prebody) = split_last bindings;
   141     val Type (_, Ts0) = if lfp then prebody else body;
   142     val Us0 = distinct (op =) (map (if lfp then body_type else domain_type) f_Us);
   143   in
   144     Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
   145   end;
   146 
   147 fun mk_map live Ts Us t =
   148   let val (Type (_, Ts0), Type (_, Us0)) = strip_typeN (live + 1) (fastype_of t) |>> List.last in
   149     Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
   150   end;
   151 
   152 fun mk_rel live Ts Us t =
   153   let val [Type (_, Ts0), Type (_, Us0)] = binder_types (snd (strip_typeN live (fastype_of t))) in
   154     Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
   155   end;
   156 
   157 fun liveness_of_fp_bnf n bnf =
   158   (case T_of_bnf bnf of
   159     Type (_, Ts) => map (not o member (op =) (deads_of_bnf bnf)) Ts
   160   | _ => replicate n false);
   161 
   162 fun cannot_merge_types () = error "Mutually recursive types must have the same type parameters";
   163 
   164 fun merge_type_arg T T' = if T = T' then T else cannot_merge_types ();
   165 
   166 fun merge_type_args (As, As') =
   167   if length As = length As' then map2 merge_type_arg As As' else cannot_merge_types ();
   168 
   169 fun reassoc_conjs thm =
   170   reassoc_conjs (thm RS @{thm conj_assoc[THEN iffD1]})
   171   handle THM _ => thm;
   172 
   173 fun type_args_named_constrained_of ((((ncAs, _), _), _), _) = ncAs;
   174 fun type_binding_of ((((_, b), _), _), _) = b;
   175 fun map_binding_of (((_, (b, _)), _), _) = b;
   176 fun rel_binding_of (((_, (_, b)), _), _) = b;
   177 fun mixfix_of ((_, mx), _) = mx;
   178 fun ctr_specs_of (_, ctr_specs) = ctr_specs;
   179 
   180 fun disc_of ((((disc, _), _), _), _) = disc;
   181 fun ctr_of ((((_, ctr), _), _), _) = ctr;
   182 fun args_of (((_, args), _), _) = args;
   183 fun defaults_of ((_, ds), _) = ds;
   184 fun ctr_mixfix_of (_, mx) = mx;
   185 
   186 fun build_map lthy build_arg (Type (s, Ts)) (Type (_, Us)) =
   187   let
   188     val bnf = the (bnf_of lthy s);
   189     val live = live_of_bnf bnf;
   190     val mapx = mk_map live Ts Us (map_of_bnf bnf);
   191     val TUs' = map dest_funT (fst (strip_typeN live (fastype_of mapx)));
   192   in Term.list_comb (mapx, map build_arg TUs') end;
   193 
   194 fun build_rel_step lthy build_arg (Type (s, Ts)) =
   195   let
   196     val bnf = the (bnf_of lthy s);
   197     val live = live_of_bnf bnf;
   198     val rel = mk_rel live Ts Ts (rel_of_bnf bnf);
   199     val Ts' = map domain_type (fst (strip_typeN live (fastype_of rel)));
   200   in Term.list_comb (rel, map build_arg Ts') end;
   201 
   202 fun derive_induct_fold_rec_thms_for_types nn pre_bnfs ctor_induct ctor_fold_thms ctor_rec_thms
   203     nesting_bnfs nested_bnfs fpTs Cs ctr_Tsss mss ns gss hss ctrss xsss ctr_defss folds recs
   204     fold_defs rec_defs lthy =
   205   let
   206     val pre_map_defs = map map_def_of_bnf pre_bnfs;
   207     val pre_set_defss = map set_defs_of_bnf pre_bnfs;
   208     val nested_map_comp's = map map_comp'_of_bnf nested_bnfs;
   209     val nested_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nested_bnfs;
   210     val nested_set_map's = maps set_map'_of_bnf nested_bnfs;
   211     val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs;
   212 
   213     val fp_T_names = map name_of_typ fpTs;
   214 
   215     val (((ps, ps'), us'), names_lthy) =
   216       lthy
   217       |> mk_Frees' "P" (map mk_pred1T fpTs)
   218       ||>> Variable.variant_fixes fp_T_names;
   219 
   220     val us = map2 (curry Free) us' fpTs;
   221 
   222     fun mk_sets_nested bnf =
   223       let
   224         val Type (T_name, Us) = T_of_bnf bnf;
   225         val lives = lives_of_bnf bnf;
   226         val sets = sets_of_bnf bnf;
   227         fun mk_set U =
   228           (case find_index (curry (op =) U) lives of
   229             ~1 => Term.dummy
   230           | i => nth sets i);
   231       in
   232         (T_name, map mk_set Us)
   233       end;
   234 
   235     val setss_nested = map mk_sets_nested nested_bnfs;
   236 
   237     val (induct_thms, induct_thm) =
   238       let
   239         fun mk_set Ts t =
   240           let val Type (_, Ts0) = domain_type (fastype_of t) in
   241             Term.subst_atomic_types (Ts0 ~~ Ts) t
   242           end;
   243 
   244         fun mk_raw_prem_prems names_lthy (x as Free (s, T as Type (T_name, Ts0))) =
   245             (case find_index (curry (op =) T) fpTs of
   246               ~1 =>
   247               (case AList.lookup (op =) setss_nested T_name of
   248                 NONE => []
   249               | SOME raw_sets0 =>
   250                 let
   251                   val (Ts, raw_sets) =
   252                     split_list (filter (exists_subtype_in fpTs o fst) (Ts0 ~~ raw_sets0));
   253                   val sets = map (mk_set Ts0) raw_sets;
   254                   val (ys, names_lthy') = names_lthy |> mk_Frees s Ts;
   255                   val xysets = map (pair x) (ys ~~ sets);
   256                   val ppremss = map (mk_raw_prem_prems names_lthy') ys;
   257                 in
   258                   flat (map2 (map o apfst o cons) xysets ppremss)
   259                 end)
   260             | kk => [([], (kk + 1, x))])
   261           | mk_raw_prem_prems _ _ = [];
   262 
   263         fun close_prem_prem xs t =
   264           fold_rev Logic.all (map Free (drop (nn + length xs)
   265             (rev (Term.add_frees t (map dest_Free xs @ ps'))))) t;
   266 
   267         fun mk_prem_prem xs (xysets, (j, x)) =
   268           close_prem_prem xs (Logic.list_implies (map (fn (x', (y, set)) =>
   269               HOLogic.mk_Trueprop (HOLogic.mk_mem (y, set $ x'))) xysets,
   270             HOLogic.mk_Trueprop (nth ps (j - 1) $ x)));
   271 
   272         fun mk_raw_prem phi ctr ctr_Ts =
   273           let
   274             val (xs, names_lthy') = names_lthy |> mk_Frees "x" ctr_Ts;
   275             val pprems = maps (mk_raw_prem_prems names_lthy') xs;
   276           in (xs, pprems, HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs))) end;
   277 
   278         fun mk_prem (xs, raw_pprems, concl) =
   279           fold_rev Logic.all xs (Logic.list_implies (map (mk_prem_prem xs) raw_pprems, concl));
   280 
   281         val raw_premss = map3 (map2 o mk_raw_prem) ps ctrss ctr_Tsss;
   282 
   283         val goal =
   284           Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss,
   285             HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry (op $)) ps us)));
   286 
   287         val kksss = map (map (map (fst o snd) o #2)) raw_premss;
   288 
   289         val ctor_induct' = ctor_induct OF (map mk_sumEN_tupled_balanced mss);
   290 
   291         val thm =
   292           Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
   293             mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' nested_set_map's
   294               pre_set_defss)
   295           |> singleton (Proof_Context.export names_lthy lthy)
   296           |> Thm.close_derivation;
   297       in
   298         `(conj_dests nn) thm
   299       end;
   300 
   301     val induct_cases = quasi_unambiguous_case_names (maps (map name_of_ctr) ctrss);
   302 
   303     val (fold_thmss, rec_thmss) =
   304       let
   305         val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;
   306         val gfolds = map (lists_bmoc gss) folds;
   307         val hrecs = map (lists_bmoc hss) recs;
   308 
   309         fun mk_goal fss frec_like xctr f xs fxs =
   310           fold_rev (fold_rev Logic.all) (xs :: fss)
   311             (mk_Trueprop_eq (frec_like $ xctr, Term.list_comb (f, fxs)));
   312 
   313         fun build_rec_like frec_likes (T, U) =
   314           if T = U then
   315             id_const T
   316           else
   317             (case find_index (curry (op =) T) fpTs of
   318               ~1 => build_map lthy (build_rec_like frec_likes) T U
   319             | kk => nth frec_likes kk);
   320 
   321         val mk_U = typ_subst (map2 pair fpTs Cs);
   322 
   323         fun unzip_rec_likes frec_likes combine (x as Free (_, T)) =
   324           if exists_subtype_in fpTs T then
   325             combine (x, build_rec_like frec_likes (T, mk_U T) $ x)
   326           else
   327             ([x], []);
   328 
   329         val gxsss = map (map (flat_rec (unzip_rec_likes gfolds (fn (_, t) => ([t], []))))) xsss;
   330         val hxsss = map (map (flat_rec (unzip_rec_likes hrecs (pairself single)))) xsss;
   331 
   332         val fold_goalss = map5 (map4 o mk_goal gss) gfolds xctrss gss xsss gxsss;
   333         val rec_goalss = map5 (map4 o mk_goal hss) hrecs xctrss hss xsss hxsss;
   334 
   335         val fold_tacss =
   336           map2 (map o mk_rec_like_tac pre_map_defs [] nesting_map_ids'' fold_defs) ctor_fold_thms
   337             ctr_defss;
   338         val rec_tacss =
   339           map2 (map o mk_rec_like_tac pre_map_defs nested_map_comp's
   340             (nested_map_ids'' @ nesting_map_ids'') rec_defs) ctor_rec_thms ctr_defss;
   341 
   342         fun prove goal tac =
   343           Goal.prove_sorry lthy [] [] goal (tac o #context)
   344           |> Thm.close_derivation;
   345       in
   346         (map2 (map2 prove) fold_goalss fold_tacss, map2 (map2 prove) rec_goalss rec_tacss)
   347       end;
   348 
   349     val induct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names induct_cases));
   350   in
   351     ((induct_thm, induct_thms, [induct_case_names_attr]),
   352      (fold_thmss, code_simp_attrs), (rec_thmss, code_simp_attrs))
   353   end;
   354 
   355 fun derive_coinduct_unfold_corec_thms_for_types names_lthy0 no_defs_lthy nn pre_bnfs dtor_coinduct
   356     dtor_strong_induct dtor_ctors dtor_unfold_thms dtor_corec_thms nesting_bnfs nested_bnfs fpTs Cs
   357     As kss mss ns cs cpss pgss crssss cgssss phss csssss chssss ctrss ctr_defss ctr_wrap_ress
   358     unfolds corecs unfold_defs corec_defs lthy =
   359   let
   360     val pre_map_defs = map map_def_of_bnf pre_bnfs;
   361     val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
   362     val nested_map_comp's = map map_comp'_of_bnf nested_bnfs;
   363     val nested_map_comps'' = map ((fn thm => thm RS sym) o map_comp_of_bnf) nested_bnfs;
   364     val nested_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nested_bnfs;
   365     val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs;
   366     val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs;
   367 
   368     val fp_T_names = map name_of_typ fpTs;
   369 
   370     val discss = map (map (mk_disc_or_sel As) o #1) ctr_wrap_ress;
   371     val selsss = map (map (map (mk_disc_or_sel As)) o #2) ctr_wrap_ress;
   372     val exhaust_thms = map #3 ctr_wrap_ress;
   373     val disc_thmsss = map #7 ctr_wrap_ress;
   374     val discIss = map #8 ctr_wrap_ress;
   375     val sel_thmsss = map #9 ctr_wrap_ress;
   376 
   377     val (((rs, us'), vs'), names_lthy) =
   378       lthy
   379       |> mk_Frees "R" (map (fn T => mk_pred2T T T) fpTs)
   380       ||>> Variable.variant_fixes fp_T_names
   381       ||>> Variable.variant_fixes (map (suffix "'") fp_T_names);
   382 
   383     val us = map2 (curry Free) us' fpTs;
   384     val udiscss = map2 (map o rapp) us discss;
   385     val uselsss = map2 (map o map o rapp) us selsss;
   386 
   387     val vs = map2 (curry Free) vs' fpTs;
   388     val vdiscss = map2 (map o rapp) vs discss;
   389     val vselsss = map2 (map o map o rapp) vs selsss;
   390 
   391     val ((coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)) =
   392       let
   393         val uvrs = map3 (fn r => fn u => fn v => r $ u $ v) rs us vs;
   394         val uv_eqs = map2 (curry HOLogic.mk_eq) us vs;
   395         val strong_rs =
   396           map4 (fn u => fn v => fn uvr => fn uv_eq =>
   397             fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs;
   398 
   399         fun build_rel rs' T =
   400           (case find_index (curry (op =) T) fpTs of
   401             ~1 =>
   402             if exists_subtype_in fpTs T then build_rel_step lthy (build_rel rs') T
   403             else HOLogic.eq_const T
   404           | kk => nth rs' kk);
   405 
   406         fun build_rel_app rs' usel vsel =
   407           fold rapp [usel, vsel] (build_rel rs' (fastype_of usel));
   408 
   409         fun mk_prem_ctr_concls rs' n k udisc usels vdisc vsels =
   410           (if k = n then [] else [HOLogic.mk_eq (udisc, vdisc)]) @
   411           (if null usels then
   412              []
   413            else
   414              [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc],
   415                 Library.foldr1 HOLogic.mk_conj (map2 (build_rel_app rs') usels vsels))]);
   416 
   417         fun mk_prem_concl rs' n udiscs uselss vdiscs vselss =
   418           Library.foldr1 HOLogic.mk_conj
   419             (flat (map5 (mk_prem_ctr_concls rs' n) (1 upto n) udiscs uselss vdiscs vselss))
   420           handle List.Empty => @{term True};
   421 
   422         fun mk_prem rs' uvr u v n udiscs uselss vdiscs vselss =
   423           fold_rev Logic.all [u, v] (Logic.mk_implies (HOLogic.mk_Trueprop uvr,
   424             HOLogic.mk_Trueprop (mk_prem_concl rs' n udiscs uselss vdiscs vselss)));
   425 
   426         val concl =
   427           HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   428             (map3 (fn uvr => fn u => fn v => HOLogic.mk_imp (uvr, HOLogic.mk_eq (u, v)))
   429                uvrs us vs));
   430 
   431         fun mk_goal rs' =
   432           Logic.list_implies (map8 (mk_prem rs') uvrs us vs ns udiscss uselsss vdiscss vselsss,
   433             concl);
   434 
   435         val goal = mk_goal rs;
   436         val strong_goal = mk_goal strong_rs;
   437 
   438         fun prove dtor_coinduct' goal =
   439           Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
   440             mk_coinduct_tac ctxt nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs dtor_ctors
   441               exhaust_thms ctr_defss disc_thmsss sel_thmsss)
   442           |> singleton (Proof_Context.export names_lthy lthy)
   443           |> Thm.close_derivation;
   444 
   445         fun postproc nn thm =
   446           Thm.permute_prems 0 nn
   447             (if nn = 1 then thm RS mp
   448              else funpow nn (fn thm => reassoc_conjs (thm RS mp_conj)) thm)
   449           |> Drule.zero_var_indexes
   450           |> `(conj_dests nn);
   451       in
   452         (postproc nn (prove dtor_coinduct goal), postproc nn (prove dtor_strong_induct strong_goal))
   453       end;
   454 
   455     fun mk_coinduct_concls ms discs ctrs =
   456       let
   457         fun mk_disc_concl disc = [name_of_disc disc];
   458         fun mk_ctr_concl 0 _ = []
   459           | mk_ctr_concl _ ctor = [name_of_ctr ctor];
   460         val disc_concls = map mk_disc_concl (fst (split_last discs)) @ [[]];
   461         val ctr_concls = map2 mk_ctr_concl ms ctrs;
   462       in
   463         flat (map2 append disc_concls ctr_concls)
   464       end;
   465 
   466     val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_T_names);
   467     val coinduct_conclss =
   468       map3 (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss;
   469 
   470     fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
   471 
   472     val gunfolds = map (lists_bmoc pgss) unfolds;
   473     val hcorecs = map (lists_bmoc phss) corecs;
   474 
   475     val (unfold_thmss, corec_thmss, safe_unfold_thmss, safe_corec_thmss) =
   476       let
   477         fun mk_goal pfss c cps fcorec_like n k ctr m cfs' =
   478           fold_rev (fold_rev Logic.all) ([c] :: pfss)
   479             (Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps,
   480                mk_Trueprop_eq (fcorec_like $ c, Term.list_comb (ctr, take m cfs'))));
   481 
   482         fun build_corec_like fcorec_likes (T, U) =
   483           if T = U then
   484             id_const T
   485           else
   486             (case find_index (curry (op =) U) fpTs of
   487               ~1 => build_map lthy (build_corec_like fcorec_likes) T U
   488             | kk => nth fcorec_likes kk);
   489 
   490         val mk_U = typ_subst (map2 pair Cs fpTs);
   491 
   492         fun intr_corec_likes fcorec_likes [] [cf] =
   493             let val T = fastype_of cf in
   494               if exists_subtype_in Cs T then build_corec_like fcorec_likes (T, mk_U T) $ cf
   495               else cf
   496             end
   497           | intr_corec_likes fcorec_likes [cq] [cf, cf'] =
   498             mk_If cq (intr_corec_likes fcorec_likes [] [cf])
   499               (intr_corec_likes fcorec_likes [] [cf']);
   500 
   501         val crgsss = map2 (map2 (map2 (intr_corec_likes gunfolds))) crssss cgssss;
   502         val cshsss = map2 (map2 (map2 (intr_corec_likes hcorecs))) csssss chssss;
   503 
   504         val unfold_goalss =
   505           map8 (map4 oooo mk_goal pgss) cs cpss gunfolds ns kss ctrss mss crgsss;
   506         val corec_goalss =
   507           map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss;
   508 
   509         fun mk_map_if_distrib bnf =
   510           let
   511             val mapx = map_of_bnf bnf;
   512             val live = live_of_bnf bnf;
   513             val ((Ts, T), U) = strip_typeN (live + 1) (fastype_of mapx) |>> split_last;
   514             val fs = Variable.variant_frees lthy [mapx] (map (pair "f") Ts);
   515             val t = Term.list_comb (mapx, map (Var o apfst (rpair 0)) fs);
   516           in
   517             Drule.instantiate' (map (SOME o certifyT lthy) [U, T]) [SOME (certify lthy t)]
   518               @{thm if_distrib}
   519           end;
   520 
   521         val nested_map_if_distribs = map mk_map_if_distrib nested_bnfs;
   522 
   523         val unfold_tacss =
   524           map3 (map oo mk_corec_like_tac unfold_defs [] [] nesting_map_ids'' [])
   525             dtor_unfold_thms pre_map_defs ctr_defss;
   526         val corec_tacss =
   527           map3 (map oo mk_corec_like_tac corec_defs nested_map_comps'' nested_map_comp's
   528               (nested_map_ids'' @ nesting_map_ids'') nested_map_if_distribs)
   529             dtor_corec_thms pre_map_defs ctr_defss;
   530 
   531         fun prove goal tac =
   532           Goal.prove_sorry lthy [] [] goal (tac o #context) |> Thm.close_derivation;
   533 
   534         val unfold_thmss = map2 (map2 prove) unfold_goalss unfold_tacss;
   535         val corec_thmss = map2 (map2 prove) corec_goalss corec_tacss;
   536 
   537         val filter_safesss =
   538           map2 (map_filter (fn (safes, thm) => if forall I safes then SOME thm else NONE) oo
   539             curry (op ~~)) (map2 (map2 (map2 (member (op =)))) cgssss crgsss);
   540 
   541         val safe_unfold_thmss = filter_safesss unfold_thmss;
   542         val safe_corec_thmss = filter_safesss corec_thmss;
   543       in
   544         (unfold_thmss, corec_thmss, safe_unfold_thmss, safe_corec_thmss)
   545       end;
   546 
   547     val (disc_unfold_iff_thmss, disc_corec_iff_thmss) =
   548       let
   549         fun mk_goal c cps fcorec_like n k disc =
   550           mk_Trueprop_eq (disc $ (fcorec_like $ c),
   551             if n = 1 then @{const True}
   552             else Library.foldr1 HOLogic.mk_conj (seq_conds mk_maybe_not n k cps));
   553 
   554         val unfold_goalss = map6 (map2 oooo mk_goal) cs cpss gunfolds ns kss discss;
   555         val corec_goalss = map6 (map2 oooo mk_goal) cs cpss hcorecs ns kss discss;
   556 
   557         fun mk_case_split' cp =
   558           Drule.instantiate' [] [SOME (certify lthy cp)] @{thm case_split};
   559 
   560         val case_splitss' = map (map mk_case_split') cpss;
   561 
   562         val unfold_tacss =
   563           map3 (map oo mk_disc_corec_like_iff_tac) case_splitss' unfold_thmss disc_thmsss;
   564         val corec_tacss =
   565           map3 (map oo mk_disc_corec_like_iff_tac) case_splitss' corec_thmss disc_thmsss;
   566 
   567         fun prove goal tac =
   568           Goal.prove_sorry lthy [] [] goal (tac o #context)
   569           |> singleton (Proof_Context.export names_lthy0 no_defs_lthy)
   570           |> Thm.close_derivation;
   571 
   572         fun proves [_] [_] = []
   573           | proves goals tacs = map2 prove goals tacs;
   574       in
   575         (map2 proves unfold_goalss unfold_tacss,
   576          map2 proves corec_goalss corec_tacss)
   577       end;
   578 
   579     val is_triv_discI = is_triv_implies orf is_concl_refl;
   580 
   581     fun mk_disc_corec_like_thms corec_likes discIs =
   582       map (op RS) (filter_out (is_triv_discI o snd) (corec_likes ~~ discIs));
   583 
   584     val disc_unfold_thmss = map2 mk_disc_corec_like_thms unfold_thmss discIss;
   585     val disc_corec_thmss = map2 mk_disc_corec_like_thms corec_thmss discIss;
   586 
   587     fun mk_sel_corec_like_thm corec_like_thm sel sel_thm =
   588       let
   589         val (domT, ranT) = dest_funT (fastype_of sel);
   590         val arg_cong' =
   591           Drule.instantiate' (map (SOME o certifyT lthy) [domT, ranT])
   592             [NONE, NONE, SOME (certify lthy sel)] arg_cong
   593           |> Thm.varifyT_global;
   594         val sel_thm' = sel_thm RSN (2, trans);
   595       in
   596         corec_like_thm RS arg_cong' RS sel_thm'
   597       end;
   598 
   599     fun mk_sel_corec_like_thms corec_likess =
   600       map3 (map3 (map2 o mk_sel_corec_like_thm)) corec_likess selsss sel_thmsss |> map flat;
   601 
   602     val sel_unfold_thmss = mk_sel_corec_like_thms unfold_thmss;
   603     val sel_corec_thmss = mk_sel_corec_like_thms corec_thmss;
   604 
   605     val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
   606     val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases));
   607     val coinduct_case_concl_attrs =
   608       map2 (fn casex => fn concls =>
   609           Attrib.internal (K (Rule_Cases.case_conclusion (casex, concls))))
   610         coinduct_cases coinduct_conclss;
   611     val coinduct_case_attrs =
   612       coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
   613   in
   614     ((coinduct_thm, coinduct_thms, strong_coinduct_thm, strong_coinduct_thms, coinduct_case_attrs),
   615      (unfold_thmss, corec_thmss, []),
   616      (safe_unfold_thmss, safe_corec_thmss),
   617      (disc_unfold_thmss, disc_corec_thmss, simp_attrs),
   618      (disc_unfold_iff_thmss, disc_corec_iff_thmss, simp_attrs),
   619      (sel_unfold_thmss, sel_corec_thmss, simp_attrs))
   620   end;
   621 
   622 fun define_datatypes prepare_constraint prepare_typ prepare_term lfp construct_fp
   623     (wrap_opts as (no_dests, rep_compat), specs) no_defs_lthy0 =
   624   let
   625     (* TODO: sanity checks on arguments *)
   626 
   627     val _ = if not lfp andalso no_dests then error "Cannot define destructor-less codatatypes"
   628       else ();
   629 
   630     fun qualify mandatory fp_b_name =
   631       Binding.qualify mandatory fp_b_name o (rep_compat ? Binding.qualify false rep_compat_prefix);
   632 
   633     val nn = length specs;
   634     val fp_bs = map type_binding_of specs;
   635     val fp_b_names = map Binding.name_of fp_bs;
   636     val fp_common_name = mk_common_name fp_b_names;
   637     val map_bs = map map_binding_of specs;
   638     val rel_bs = map rel_binding_of specs;
   639 
   640     fun prepare_type_arg (_, (ty, c)) =
   641       let val TFree (s, _) = prepare_typ no_defs_lthy0 ty in
   642         TFree (s, prepare_constraint no_defs_lthy0 c)
   643       end;
   644 
   645     val Ass0 = map (map prepare_type_arg o type_args_named_constrained_of) specs;
   646     val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0;
   647     val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0;
   648     val set_bss = map (map fst o type_args_named_constrained_of) specs;
   649 
   650     val (((Bs0, Cs), Xs), no_defs_lthy) =
   651       no_defs_lthy0
   652       |> fold (Variable.declare_typ o resort_tfree dummyS) unsorted_As
   653       |> mk_TFrees (length unsorted_As)
   654       ||>> mk_TFrees nn
   655       ||>> apfst (map TFree) o
   656         variant_types (map (prefix "'") fp_b_names) (replicate nn HOLogic.typeS);
   657 
   658     (* TODO: cleaner handling of fake contexts, without "background_theory" *)
   659     (*the "perhaps o try" below helps gracefully handles the case where the new type is defined in a
   660       locale and shadows an existing global type*)
   661 
   662     fun add_fake_type spec =
   663       Sign.add_type no_defs_lthy (type_binding_of spec,
   664         length (type_args_named_constrained_of spec), mixfix_of spec);
   665 
   666     val fake_thy = Theory.copy #> fold add_fake_type specs;
   667     val fake_lthy = Proof_Context.background_theory fake_thy no_defs_lthy;
   668 
   669     fun mk_fake_T b =
   670       Type (fst (Term.dest_Type (Proof_Context.read_type_name fake_lthy true (Binding.name_of b))),
   671         unsorted_As);
   672 
   673     val fake_Ts = map mk_fake_T fp_bs;
   674 
   675     val mixfixes = map mixfix_of specs;
   676 
   677     val _ = (case duplicates Binding.eq_name fp_bs of [] => ()
   678       | b :: _ => error ("Duplicate type name declaration " ^ quote (Binding.name_of b)));
   679 
   680     val ctr_specss = map ctr_specs_of specs;
   681 
   682     val disc_bindingss = map (map disc_of) ctr_specss;
   683     val ctr_bindingss =
   684       map2 (fn fp_b_name => map (qualify false fp_b_name o ctr_of)) fp_b_names ctr_specss;
   685     val ctr_argsss = map (map args_of) ctr_specss;
   686     val ctr_mixfixess = map (map ctr_mixfix_of) ctr_specss;
   687 
   688     val sel_bindingsss = map (map (map fst)) ctr_argsss;
   689     val fake_ctr_Tsss0 = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss;
   690     val raw_sel_defaultsss = map (map defaults_of) ctr_specss;
   691 
   692     val (As :: _) :: fake_ctr_Tsss =
   693       burrow (burrow (Syntax.check_typs fake_lthy)) (Ass0 :: fake_ctr_Tsss0);
   694 
   695     val _ = (case duplicates (op =) unsorted_As of [] => ()
   696       | A :: _ => error ("Duplicate type parameter " ^
   697           quote (Syntax.string_of_typ no_defs_lthy A)));
   698 
   699     val rhs_As' = fold (fold (fold Term.add_tfreesT)) fake_ctr_Tsss [];
   700     val _ = (case subtract (op =) (map dest_TFree As) rhs_As' of
   701         [] => ()
   702       | A' :: _ => error ("Extra type variable on right-hand side: " ^
   703           quote (Syntax.string_of_typ no_defs_lthy (TFree A'))));
   704 
   705     fun eq_fpT_check (T as Type (s, Us)) (Type (s', Us')) =
   706         s = s' andalso (Us = Us' orelse error ("Illegal occurrence of recursive type " ^
   707           quote (Syntax.string_of_typ fake_lthy T)))
   708       | eq_fpT_check _ _ = false;
   709 
   710     fun freeze_fp (T as Type (s, Us)) =
   711         (case find_index (eq_fpT_check T) fake_Ts of
   712           ~1 => Type (s, map freeze_fp Us)
   713         | kk => nth Xs kk)
   714       | freeze_fp T = T;
   715 
   716     val ctr_TsssXs = map (map (map freeze_fp)) fake_ctr_Tsss;
   717     val ctr_sum_prod_TsXs = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctr_TsssXs;
   718 
   719     val fp_eqs =
   720       map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctr_sum_prod_TsXs;
   721 
   722     val (pre_bnfs, ({bnfs = fp_bnfs as any_fp_bnf :: _, dtors = dtors0, ctors = ctors0,
   723            folds = fp_folds0, recs = fp_recs0, induct = fp_induct, strong_induct = fp_strong_induct,
   724            dtor_ctors, ctor_dtors, ctor_injects, map_thms = fp_map_thms, set_thmss = fp_set_thmss,
   725            rel_thms = fp_rel_thms, fold_thms = fp_fold_thms, rec_thms = fp_rec_thms}, lthy)) =
   726       fp_bnf construct_fp fp_bs mixfixes map_bs rel_bs set_bss (map dest_TFree unsorted_As) fp_eqs
   727         no_defs_lthy0;
   728 
   729     val timer = time (Timer.startRealTimer ());
   730 
   731     fun add_nesty_bnf_names Us =
   732       let
   733         fun add (Type (s, Ts)) ss =
   734             let val (needs, ss') = fold_map add Ts ss in
   735               if exists I needs then (true, insert (op =) s ss') else (false, ss')
   736             end
   737           | add T ss = (member (op =) Us T, ss);
   738       in snd oo add end;
   739 
   740     fun nesty_bnfs Us =
   741       map_filter (bnf_of lthy) (fold (fold (fold (add_nesty_bnf_names Us))) ctr_TsssXs []);
   742 
   743     val nesting_bnfs = nesty_bnfs As;
   744     val nested_bnfs = nesty_bnfs Xs;
   745 
   746     val pre_map_defs = map map_def_of_bnf pre_bnfs;
   747     val pre_set_defss = map set_defs_of_bnf pre_bnfs;
   748     val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
   749     val nested_set_map's = maps set_map'_of_bnf nested_bnfs;
   750     val nesting_set_map's = maps set_map'_of_bnf nesting_bnfs;
   751 
   752     val live = live_of_bnf any_fp_bnf;
   753 
   754     val Bs =
   755       map3 (fn alive => fn A as TFree (_, S) => fn B => if alive then resort_tfree S B else A)
   756         (liveness_of_fp_bnf (length As) any_fp_bnf) As Bs0;
   757 
   758     val B_ify = Term.typ_subst_atomic (As ~~ Bs);
   759 
   760     val ctors = map (mk_ctor As) ctors0;
   761     val dtors = map (mk_dtor As) dtors0;
   762 
   763     val fpTs = map (domain_type o fastype_of) dtors;
   764 
   765     fun massage_simple_notes base =
   766       filter_out (null o #2)
   767       #> map (fn (thmN, thms, attrs) =>
   768         ((qualify true base (Binding.name thmN), attrs), [(thms, [])]));
   769 
   770     val massage_multi_notes =
   771       maps (fn (thmN, thmss, attrs) =>
   772         if forall null thmss then
   773           []
   774         else
   775           map3 (fn fp_b_name => fn Type (T_name, _) => fn thms =>
   776             ((qualify true fp_b_name (Binding.name thmN), attrs T_name),
   777              [(thms, [])])) fp_b_names fpTs thmss);
   778 
   779     val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Xs ~~ fpTs)))) ctr_TsssXs;
   780     val ns = map length ctr_Tsss;
   781     val kss = map (fn n => 1 upto n) ns;
   782     val mss = map (map length) ctr_Tsss;
   783     val Css = map2 replicate ns Cs;
   784 
   785     val fp_folds as any_fp_fold :: _ = map (mk_rec_like lfp As Cs) fp_folds0;
   786     val fp_recs as any_fp_rec :: _ = map (mk_rec_like lfp As Cs) fp_recs0;
   787 
   788     val fp_fold_fun_Ts = fst (split_last (binder_types (fastype_of any_fp_fold)));
   789     val fp_rec_fun_Ts = fst (split_last (binder_types (fastype_of any_fp_rec)));
   790 
   791     val (((fold_only as (gss, _, _), rec_only as (hss, _, _)),
   792           (cs, cpss, unfold_only as ((pgss, crssss, cgssss), (_, g_Tsss, _)),
   793            corec_only as ((phss, csssss, chssss), (_, h_Tsss, _)))), names_lthy0) =
   794       if lfp then
   795         let
   796           val y_Tsss =
   797             map3 (fn n => fn ms => map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type)
   798               ns mss fp_fold_fun_Ts;
   799           val g_Tss = map2 (map2 (curry (op --->))) y_Tsss Css;
   800 
   801           val ((gss, ysss), lthy) =
   802             lthy
   803             |> mk_Freess "f" g_Tss
   804             ||>> mk_Freesss "x" y_Tsss;
   805 
   806           fun proj_recT proj (Type (s as @{type_name prod}, Ts as [T, U])) =
   807               if member (op =) fpTs T then proj (T, U) else Type (s, map (proj_recT proj) Ts)
   808             | proj_recT proj (Type (s, Ts)) = Type (s, map (proj_recT proj) Ts)
   809             | proj_recT _ T = T;
   810 
   811           fun unzip_recT T =
   812             if exists_subtype_in fpTs T then ([proj_recT fst T], [proj_recT snd T]) else ([T], []);
   813 
   814           val z_Tsss =
   815             map3 (fn n => fn ms => map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type)
   816               ns mss fp_rec_fun_Ts;
   817           val z_Tsss' = map (map (flat_rec unzip_recT)) z_Tsss;
   818           val h_Tss = map2 (map2 (curry (op --->))) z_Tsss' Css;
   819 
   820           val hss = map2 (map2 retype_free) h_Tss gss;
   821           val zsss = map2 (map2 (map2 retype_free)) z_Tsss ysss;
   822         in
   823           ((((gss, g_Tss, ysss), (hss, h_Tss, zsss)),
   824             ([], [], (([], [], []), ([], [], [])), (([], [], []), ([], [], [])))), lthy)
   825         end
   826       else
   827         let
   828           (*avoid "'a itself" arguments in coiterators and corecursors*)
   829           val mss' =  map (fn [0] => [1] | ms => ms) mss;
   830 
   831           val p_Tss = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_pred1T) ns Cs;
   832 
   833           fun flat_predss_getterss qss fss = maps (op @) (qss ~~ fss);
   834 
   835           fun flat_preds_predsss_gettersss [] [qss] [fss] = flat_predss_getterss qss fss
   836             | flat_preds_predsss_gettersss (p :: ps) (qss :: qsss) (fss :: fsss) =
   837               p :: flat_predss_getterss qss fss @ flat_preds_predsss_gettersss ps qsss fsss;
   838 
   839           fun mk_types maybe_unzipT fun_Ts =
   840             let
   841               val f_sum_prod_Ts = map range_type fun_Ts;
   842               val f_prod_Tss = map2 dest_sumTN_balanced ns f_sum_prod_Ts;
   843               val f_Tsss = map2 (map2 dest_tupleT) mss' f_prod_Tss;
   844               val f_Tssss =
   845                 map2 (fn C => map (map (map (curry (op -->) C) o maybe_unzipT))) Cs f_Tsss;
   846               val q_Tssss =
   847                 map (map (map (fn [_] => [] | [_, C] => [mk_pred1T (domain_type C)]))) f_Tssss;
   848               val pf_Tss = map3 flat_preds_predsss_gettersss p_Tss q_Tssss f_Tssss;
   849             in (q_Tssss, f_sum_prod_Ts, f_Tsss, f_Tssss, pf_Tss) end;
   850 
   851           val (r_Tssss, g_sum_prod_Ts, g_Tsss, g_Tssss, pg_Tss) = mk_types single fp_fold_fun_Ts;
   852 
   853           val (((cs, pss), gssss), lthy) =
   854             lthy
   855             |> mk_Frees "a" Cs
   856             ||>> mk_Freess "p" p_Tss
   857             ||>> mk_Freessss "g" g_Tssss;
   858           val rssss = map (map (map (fn [] => []))) r_Tssss;
   859 
   860           fun proj_corecT proj (Type (s as @{type_name sum}, Ts as [T, U])) =
   861               if member (op =) fpTs T then proj (T, U) else Type (s, map (proj_corecT proj) Ts)
   862             | proj_corecT proj (Type (s, Ts)) = Type (s, map (proj_corecT proj) Ts)
   863             | proj_corecT _ T = T;
   864 
   865           fun unzip_corecT T =
   866             if exists_subtype_in fpTs T then [proj_corecT fst T, proj_corecT snd T] else [T];
   867 
   868           val (s_Tssss, h_sum_prod_Ts, h_Tsss, h_Tssss, ph_Tss) =
   869             mk_types unzip_corecT fp_rec_fun_Ts;
   870 
   871           val hssss_hd = map2 (map2 (map2 (fn T :: _ => fn [g] => retype_free T g))) h_Tssss gssss;
   872           val ((sssss, hssss_tl), lthy) =
   873             lthy
   874             |> mk_Freessss "q" s_Tssss
   875             ||>> mk_Freessss "h" (map (map (map tl)) h_Tssss);
   876           val hssss = map2 (map2 (map2 cons)) hssss_hd hssss_tl;
   877 
   878           val cpss = map2 (map o rapp) cs pss;
   879 
   880           fun mk_terms qssss fssss =
   881             let
   882               val pfss = map3 flat_preds_predsss_gettersss pss qssss fssss;
   883               val cqssss = map2 (map o map o map o rapp) cs qssss;
   884               val cfssss = map2 (map o map o map o rapp) cs fssss;
   885             in (pfss, cqssss, cfssss) end;
   886         in
   887           (((([], [], []), ([], [], [])),
   888             (cs, cpss, (mk_terms rssss gssss, (g_sum_prod_Ts, g_Tsss, pg_Tss)),
   889              (mk_terms sssss hssss, (h_sum_prod_Ts, h_Tsss, ph_Tss)))), lthy)
   890         end;
   891 
   892     fun define_ctrs_case_for_type (((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), ctor), dtor),
   893             fp_fold), fp_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),
   894           pre_rel_def), fp_map_thm), fp_set_thms), fp_rel_thm), n), ks), ms), ctr_bindings),
   895         ctr_mixfixes), ctr_Tss), disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy =
   896       let
   897         val fp_b_name = Binding.name_of fp_b;
   898 
   899         val dtorT = domain_type (fastype_of ctor);
   900         val ctr_prod_Ts = map HOLogic.mk_tupleT ctr_Tss;
   901         val ctr_sum_prod_T = mk_sumTN_balanced ctr_prod_Ts;
   902         val case_Ts = map (fn Ts => Ts ---> C) ctr_Tss;
   903 
   904         val (((((w, fs), xss), yss), u'), names_lthy) =
   905           no_defs_lthy
   906           |> yield_singleton (mk_Frees "w") dtorT
   907           ||>> mk_Frees "f" case_Ts
   908           ||>> mk_Freess "x" ctr_Tss
   909           ||>> mk_Freess "y" (map (map B_ify) ctr_Tss)
   910           ||>> yield_singleton Variable.variant_fixes fp_b_name;
   911 
   912         val u = Free (u', fpT);
   913 
   914         val tuple_xs = map HOLogic.mk_tuple xss;
   915         val tuple_ys = map HOLogic.mk_tuple yss;
   916 
   917         val ctr_rhss =
   918           map3 (fn k => fn xs => fn tuple_x => fold_rev Term.lambda xs (ctor $
   919             mk_InN_balanced ctr_sum_prod_T n tuple_x k)) ks xss tuple_xs;
   920 
   921         val case_binding = qualify false fp_b_name (Binding.suffix_name ("_" ^ caseN) fp_b);
   922 
   923         val case_rhs =
   924           fold_rev Term.lambda (fs @ [u])
   925             (mk_sum_caseN_balanced (map2 mk_uncurried_fun fs xss) $ (dtor $ u));
   926 
   927         val ((raw_case :: raw_ctrs, raw_case_def :: raw_ctr_defs), (lthy', lthy)) = no_defs_lthy
   928           |> apfst split_list o fold_map3 (fn b => fn mx => fn rhs =>
   929               Local_Theory.define ((b, mx), ((Thm.def_binding b, []), rhs)) #>> apsnd snd)
   930             (case_binding :: ctr_bindings) (NoSyn :: ctr_mixfixes) (case_rhs :: ctr_rhss)
   931           ||> `Local_Theory.restore;
   932 
   933         val phi = Proof_Context.export_morphism lthy lthy';
   934 
   935         val ctr_defs = map (Morphism.thm phi) raw_ctr_defs;
   936         val ctr_defs' =
   937           map2 (fn m => fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) ms ctr_defs;
   938         val case_def = Morphism.thm phi raw_case_def;
   939 
   940         val ctrs0 = map (Morphism.term phi) raw_ctrs;
   941         val casex0 = Morphism.term phi raw_case;
   942 
   943         val ctrs = map (mk_ctr As) ctrs0;
   944 
   945         fun wrap lthy =
   946           let
   947             fun exhaust_tac {context = ctxt, prems = _} =
   948               let
   949                 val ctor_iff_dtor_thm =
   950                   let
   951                     val goal =
   952                       fold_rev Logic.all [w, u]
   953                         (mk_Trueprop_eq (HOLogic.mk_eq (u, ctor $ w), HOLogic.mk_eq (dtor $ u, w)));
   954                   in
   955                     Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
   956                       mk_ctor_iff_dtor_tac ctxt (map (SOME o certifyT lthy) [dtorT, fpT])
   957                         (certify lthy ctor) (certify lthy dtor) ctor_dtor dtor_ctor)
   958                     |> Thm.close_derivation
   959                     |> Morphism.thm phi
   960                   end;
   961 
   962                 val sumEN_thm' =
   963                   unfold_thms lthy @{thms all_unit_eq}
   964                     (Drule.instantiate' (map (SOME o certifyT lthy) ctr_prod_Ts) []
   965                        (mk_sumEN_balanced n))
   966                   |> Morphism.thm phi;
   967               in
   968                 mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor_thm sumEN_thm'
   969               end;
   970 
   971             val inject_tacss =
   972               map2 (fn 0 => K [] | _ => fn ctr_def => [fn {context = ctxt, ...} =>
   973                   mk_inject_tac ctxt ctr_def ctor_inject]) ms ctr_defs;
   974 
   975             val half_distinct_tacss =
   976               map (map (fn (def, def') => fn {context = ctxt, ...} =>
   977                 mk_half_distinct_tac ctxt ctor_inject [def, def'])) (mk_half_pairss (`I ctr_defs));
   978 
   979             val case_tacs =
   980               map3 (fn k => fn m => fn ctr_def => fn {context = ctxt, ...} =>
   981                 mk_case_tac ctxt n k m case_def ctr_def dtor_ctor) ks ms ctr_defs;
   982 
   983             val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs];
   984 
   985             val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss
   986           in
   987             wrap_free_constructors tacss (((wrap_opts, ctrs0), casex0), (disc_bindings,
   988               (sel_bindingss, sel_defaultss))) lthy
   989           end;
   990 
   991         fun derive_maps_sets_rels (ctr_wrap_res, lthy) =
   992           let
   993             val rel_flip = rel_flip_of_bnf fp_bnf;
   994             val nones = replicate live NONE;
   995 
   996             val ctor_cong =
   997               if lfp then
   998                 Drule.dummy_thm
   999               else
  1000                 let val ctor' = mk_ctor Bs ctor in
  1001                   cterm_instantiate_pos [NONE, NONE, SOME (certify lthy ctor')] arg_cong
  1002                 end;
  1003 
  1004             fun mk_cIn ify =
  1005               certify lthy o (not lfp ? curry (op $) (map_types ify ctor)) oo
  1006               mk_InN_balanced (ify ctr_sum_prod_T) n;
  1007 
  1008             val cxIns = map2 (mk_cIn I) tuple_xs ks;
  1009             val cyIns = map2 (mk_cIn B_ify) tuple_ys ks;
  1010 
  1011             fun mk_map_thm ctr_def' cxIn =
  1012               fold_thms lthy [ctr_def']
  1013                 (unfold_thms lthy (pre_map_def ::
  1014                      (if lfp then [] else [ctor_dtor, dtor_ctor]) @ sum_prod_thms_map)
  1015                    (cterm_instantiate_pos (nones @ [SOME cxIn])
  1016                       (if lfp then fp_map_thm else fp_map_thm RS ctor_cong)))
  1017               |> singleton (Proof_Context.export names_lthy no_defs_lthy);
  1018 
  1019             fun mk_set_thm fp_set_thm ctr_def' cxIn =
  1020               fold_thms lthy [ctr_def']
  1021                 (unfold_thms lthy (pre_set_defs @ nested_set_map's @ nesting_set_map's @
  1022                      (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_set)
  1023                    (cterm_instantiate_pos [SOME cxIn] fp_set_thm))
  1024               |> singleton (Proof_Context.export names_lthy no_defs_lthy);
  1025 
  1026             fun mk_set_thms fp_set_thm = map2 (mk_set_thm fp_set_thm) ctr_defs' cxIns;
  1027 
  1028             val map_thms = map2 mk_map_thm ctr_defs' cxIns;
  1029             val set_thmss = map mk_set_thms fp_set_thms;
  1030 
  1031             val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns);
  1032 
  1033             fun mk_rel_thm postproc ctr_defs' cxIn cyIn =
  1034               fold_thms lthy ctr_defs'
  1035                  (unfold_thms lthy (@{thm Inl_Inr_False} :: pre_rel_def ::
  1036                       (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_rel)
  1037                     (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
  1038               |> postproc
  1039               |> singleton (Proof_Context.export names_lthy no_defs_lthy);
  1040 
  1041             fun mk_rel_inject_thm ((ctr_def', cxIn), (_, cyIn)) =
  1042               mk_rel_thm (unfold_thms lthy @{thms eq_sym_Unity_conv}) [ctr_def'] cxIn cyIn;
  1043 
  1044             val rel_inject_thms = map mk_rel_inject_thm (op ~~ rel_infos);
  1045 
  1046             fun mk_half_rel_distinct_thm ((xctr_def', cxIn), (yctr_def', cyIn)) =
  1047               mk_rel_thm (fn thm => thm RS @{thm eq_False[THEN iffD1]}) [xctr_def', yctr_def']
  1048                 cxIn cyIn;
  1049 
  1050             fun mk_other_half_rel_distinct_thm thm =
  1051               flip_rels lthy live thm RS (rel_flip RS sym RS @{thm arg_cong[of _ _ Not]} RS iffD2);
  1052 
  1053             val half_rel_distinct_thmss =
  1054               map (map mk_half_rel_distinct_thm) (mk_half_pairss rel_infos);
  1055             val other_half_rel_distinct_thmss =
  1056               map (map mk_other_half_rel_distinct_thm) half_rel_distinct_thmss;
  1057             val (rel_distinct_thms, _) =
  1058               join_halves n half_rel_distinct_thmss other_half_rel_distinct_thmss;
  1059 
  1060             val notes =
  1061               [(mapN, map_thms, code_simp_attrs),
  1062                (rel_distinctN, rel_distinct_thms, code_simp_attrs),
  1063                (rel_injectN, rel_inject_thms, code_simp_attrs),
  1064                (setsN, flat set_thmss, code_simp_attrs)]
  1065               |> massage_simple_notes fp_b_name;
  1066           in
  1067             (ctr_wrap_res, lthy |> Local_Theory.notes notes |> snd)
  1068           end;
  1069 
  1070         fun define_fold_rec no_defs_lthy =
  1071           let
  1072             val fpT_to_C = fpT --> C;
  1073 
  1074             fun build_prod_proj mk_proj (T, U) =
  1075               if T = U then
  1076                 id_const T
  1077               else
  1078                 (case (T, U) of
  1079                   (Type (s, _), Type (s', _)) =>
  1080                   if s = s' then build_map lthy (build_prod_proj mk_proj) T U else mk_proj T
  1081                 | _ => mk_proj T);
  1082 
  1083             (* TODO: Avoid these complications; cf. corec case *)
  1084             fun mk_U proj (Type (s as @{type_name prod}, Ts as [T', U])) =
  1085                 if member (op =) fpTs T' then proj (T', U) else Type (s, map (mk_U proj) Ts)
  1086               | mk_U proj (Type (s, Ts)) = Type (s, map (mk_U proj) Ts)
  1087               | mk_U _ T = T;
  1088 
  1089             fun unzip_rec (x as Free (_, T)) =
  1090               if exists_subtype_in fpTs T then
  1091                 ([build_prod_proj fst_const (T, mk_U fst T) $ x],
  1092                  [build_prod_proj snd_const (T, mk_U snd T) $ x])
  1093               else
  1094                 ([x], []);
  1095 
  1096             fun mk_rec_like_arg f xs =
  1097               mk_tupled_fun (HOLogic.mk_tuple xs) f (flat_rec unzip_rec xs);
  1098 
  1099             fun generate_rec_like (suf, fp_rec_like, (fss, f_Tss, xsss)) =
  1100               let
  1101                 val res_T = fold_rev (curry (op --->)) f_Tss fpT_to_C;
  1102                 val binding = qualify false fp_b_name (Binding.suffix_name ("_" ^ suf) fp_b);
  1103                 val spec =
  1104                   mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binding, res_T)),
  1105                     Term.list_comb (fp_rec_like,
  1106                       map2 (mk_sum_caseN_balanced oo map2 mk_rec_like_arg) fss xsss));
  1107               in (binding, spec) end;
  1108 
  1109             val rec_like_infos =
  1110               [(foldN, fp_fold, fold_only),
  1111                (recN, fp_rec, rec_only)];
  1112 
  1113             val (bindings, specs) = map generate_rec_like rec_like_infos |> split_list;
  1114 
  1115             val ((csts, defs), (lthy', lthy)) = no_defs_lthy
  1116               |> apfst split_list o fold_map2 (fn b => fn spec =>
  1117                 Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec))
  1118                 #>> apsnd snd) bindings specs
  1119               ||> `Local_Theory.restore;
  1120 
  1121             val phi = Proof_Context.export_morphism lthy lthy';
  1122 
  1123             val [fold_def, rec_def] = map (Morphism.thm phi) defs;
  1124 
  1125             val [foldx, recx] = map (mk_rec_like lfp As Cs o Morphism.term phi) csts;
  1126           in
  1127             ((foldx, recx, fold_def, rec_def), lthy')
  1128           end;
  1129 
  1130         fun define_unfold_corec no_defs_lthy =
  1131           let
  1132             val B_to_fpT = C --> fpT;
  1133 
  1134             fun build_sum_inj mk_inj (T, U) =
  1135               if T = U then
  1136                 id_const T
  1137               else
  1138                 (case (T, U) of
  1139                   (Type (s, _), Type (s', _)) =>
  1140                   if s = s' then build_map lthy (build_sum_inj mk_inj) T U
  1141                   else uncurry mk_inj (dest_sumT U)
  1142                 | _ => uncurry mk_inj (dest_sumT U));
  1143 
  1144             fun build_dtor_corec_like_arg _ [] [cf] = cf
  1145               | build_dtor_corec_like_arg T [cq] [cf, cf'] =
  1146                 mk_If cq (build_sum_inj Inl_const (fastype_of cf, T) $ cf)
  1147                   (build_sum_inj Inr_const (fastype_of cf', T) $ cf')
  1148 
  1149             val crgsss = map3 (map3 (map3 build_dtor_corec_like_arg)) g_Tsss crssss cgssss;
  1150             val cshsss = map3 (map3 (map3 build_dtor_corec_like_arg)) h_Tsss csssss chssss;
  1151 
  1152             fun mk_preds_getterss_join c n cps sum_prod_T cqfss =
  1153               Term.lambda c (mk_IfN sum_prod_T cps
  1154                 (map2 (mk_InN_balanced sum_prod_T n) (map HOLogic.mk_tuple cqfss) (1 upto n)));
  1155 
  1156             fun generate_corec_like (suf, fp_rec_like, (cqfsss, ((pfss, _, _), (f_sum_prod_Ts, _,
  1157                 pf_Tss)))) =
  1158               let
  1159                 val res_T = fold_rev (curry (op --->)) pf_Tss B_to_fpT;
  1160                 val binding = qualify false fp_b_name (Binding.suffix_name ("_" ^ suf) fp_b);
  1161                 val spec =
  1162                   mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binding, res_T)),
  1163                     Term.list_comb (fp_rec_like,
  1164                       map5 mk_preds_getterss_join cs ns cpss f_sum_prod_Ts cqfsss));
  1165               in (binding, spec) end;
  1166 
  1167             val corec_like_infos =
  1168               [(unfoldN, fp_fold, (crgsss, unfold_only)),
  1169                (corecN, fp_rec, (cshsss, corec_only))];
  1170 
  1171             val (bindings, specs) = map generate_corec_like corec_like_infos |> split_list;
  1172 
  1173             val ((csts, defs), (lthy', lthy)) = no_defs_lthy
  1174               |> apfst split_list o fold_map2 (fn b => fn spec =>
  1175                 Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec))
  1176                 #>> apsnd snd) bindings specs
  1177               ||> `Local_Theory.restore;
  1178 
  1179             val phi = Proof_Context.export_morphism lthy lthy';
  1180 
  1181             val [unfold_def, corec_def] = map (Morphism.thm phi) defs;
  1182 
  1183             val [unfold, corec] = map (mk_rec_like lfp As Cs o Morphism.term phi) csts;
  1184           in
  1185             ((unfold, corec, unfold_def, corec_def), lthy')
  1186           end;
  1187 
  1188         val define_rec_likes = if lfp then define_fold_rec else define_unfold_corec;
  1189 
  1190         fun massage_res ((ctr_wrap_res, rec_like_res), lthy) =
  1191           (((ctrs, xss, ctr_defs, ctr_wrap_res), rec_like_res), lthy);
  1192       in
  1193         (wrap #> (live > 0 ? derive_maps_sets_rels) ##>> define_rec_likes #> massage_res, lthy')
  1194       end;
  1195 
  1196     fun wrap_types_and_more (wrap_types_and_mores, lthy) =
  1197       fold_map I wrap_types_and_mores lthy
  1198       |>> apsnd split_list4 o apfst split_list4 o split_list;
  1199 
  1200     (* TODO: Add map, sets, rel simps *)
  1201     val mk_simp_thmss =
  1202       map3 (fn (_, _, _, injects, distincts, cases, _, _, _) => fn rec_likes => fn fold_likes =>
  1203         injects @ distincts @ cases @ rec_likes @ fold_likes);
  1204 
  1205     fun derive_and_note_induct_fold_rec_thms_for_types
  1206         (((ctrss, xsss, ctr_defss, ctr_wrap_ress), (folds, recs, fold_defs, rec_defs)), lthy) =
  1207       let
  1208         val ((induct_thm, induct_thms, induct_attrs),
  1209              (fold_thmss, fold_attrs),
  1210              (rec_thmss, rec_attrs)) =
  1211           derive_induct_fold_rec_thms_for_types nn pre_bnfs fp_induct fp_fold_thms fp_rec_thms
  1212             nesting_bnfs nested_bnfs fpTs Cs ctr_Tsss mss ns gss hss ctrss xsss ctr_defss folds recs
  1213             fold_defs rec_defs lthy;
  1214 
  1215         fun induct_type_attr T_name = Attrib.internal (K (Induct.induct_type T_name));
  1216 
  1217         val simp_thmss = mk_simp_thmss ctr_wrap_ress rec_thmss fold_thmss;
  1218 
  1219         val common_notes =
  1220           (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])
  1221           |> massage_simple_notes fp_common_name;
  1222 
  1223         val notes =
  1224           [(foldN, fold_thmss, K fold_attrs),
  1225            (inductN, map single induct_thms, fn T_name => induct_attrs @ [induct_type_attr T_name]),
  1226            (recN, rec_thmss, K rec_attrs),
  1227            (simpsN, simp_thmss, K [])]
  1228           |> massage_multi_notes;
  1229       in
  1230         lthy |> Local_Theory.notes (common_notes @ notes) |> snd
  1231       end;
  1232 
  1233     fun derive_and_note_coinduct_unfold_corec_thms_for_types
  1234         (((ctrss, _, ctr_defss, ctr_wrap_ress), (unfolds, corecs, unfold_defs, corec_defs)), lthy) =
  1235       let
  1236         val ((coinduct_thm, coinduct_thms, strong_coinduct_thm, strong_coinduct_thms,
  1237               coinduct_attrs),
  1238              (unfold_thmss, corec_thmss, corec_like_attrs),
  1239              (safe_unfold_thmss, safe_corec_thmss),
  1240              (disc_unfold_thmss, disc_corec_thmss, disc_corec_like_attrs),
  1241              (disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_corec_like_iff_attrs),
  1242              (sel_unfold_thmss, sel_corec_thmss, sel_corec_like_attrs)) =
  1243           derive_coinduct_unfold_corec_thms_for_types names_lthy0 no_defs_lthy nn pre_bnfs fp_induct
  1244             fp_strong_induct dtor_ctors fp_fold_thms fp_rec_thms nesting_bnfs nested_bnfs fpTs Cs As
  1245             kss mss ns cs cpss pgss crssss cgssss phss csssss chssss ctrss ctr_defss ctr_wrap_ress
  1246             unfolds corecs unfold_defs corec_defs lthy;
  1247 
  1248         fun coinduct_type_attr T_name = Attrib.internal (K (Induct.coinduct_type T_name));
  1249 
  1250         fun flat_corec_like_thms corec_likes disc_corec_likes sel_corec_likes =
  1251           corec_likes @ disc_corec_likes @ sel_corec_likes;
  1252 
  1253         val simp_thmss =
  1254           mk_simp_thmss ctr_wrap_ress
  1255             (map3 flat_corec_like_thms safe_corec_thmss disc_corec_thmss sel_corec_thmss)
  1256             (map3 flat_corec_like_thms safe_unfold_thmss disc_unfold_thmss sel_unfold_thmss);
  1257 
  1258         val anonymous_notes =
  1259           [(flat safe_unfold_thmss @ flat safe_corec_thmss, simp_attrs)]
  1260           |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
  1261 
  1262         val common_notes =
  1263           (if nn > 1 then
  1264              [(coinductN, [coinduct_thm], coinduct_attrs),
  1265               (strong_coinductN, [strong_coinduct_thm], coinduct_attrs)]
  1266            else
  1267              [])
  1268           |> massage_simple_notes fp_common_name;
  1269 
  1270         val notes =
  1271           [(coinductN, map single coinduct_thms,
  1272             fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]),
  1273            (corecN, corec_thmss, K corec_like_attrs),
  1274            (disc_corecN, disc_corec_thmss, K disc_corec_like_attrs),
  1275            (disc_corec_iffN, disc_corec_iff_thmss, K disc_corec_like_iff_attrs),
  1276            (disc_unfoldN, disc_unfold_thmss, K disc_corec_like_attrs),
  1277            (disc_unfold_iffN, disc_unfold_iff_thmss, K disc_corec_like_iff_attrs),
  1278            (sel_corecN, sel_corec_thmss, K sel_corec_like_attrs),
  1279            (sel_unfoldN, sel_unfold_thmss, K sel_corec_like_attrs),
  1280            (simpsN, simp_thmss, K []),
  1281            (strong_coinductN, map single strong_coinduct_thms, K coinduct_attrs),
  1282            (unfoldN, unfold_thmss, K corec_like_attrs)]
  1283           |> massage_multi_notes;
  1284       in
  1285         lthy |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
  1286       end;
  1287 
  1288     val lthy' = lthy
  1289       |> fold_map define_ctrs_case_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~
  1290         fp_folds ~~ fp_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~
  1291         pre_set_defss ~~ pre_rel_defs ~~ fp_map_thms ~~ fp_set_thmss ~~ fp_rel_thms ~~ ns ~~ kss ~~
  1292         mss ~~ ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~
  1293         raw_sel_defaultsss)
  1294       |> wrap_types_and_more
  1295       |> (if lfp then derive_and_note_induct_fold_rec_thms_for_types
  1296           else derive_and_note_coinduct_unfold_corec_thms_for_types);
  1297 
  1298     val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
  1299       (if lfp then "" else "co") ^ "datatype"));
  1300   in
  1301     timer; lthy'
  1302   end;
  1303 
  1304 val datatypes = define_datatypes (K I) (K I) (K I);
  1305 
  1306 val datatype_cmd = define_datatypes Typedecl.read_constraint Syntax.parse_typ Syntax.parse_term;
  1307 
  1308 val parse_ctr_arg =
  1309   @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} ||
  1310   (Parse.typ >> pair Binding.empty);
  1311 
  1312 val parse_defaults =
  1313   @{keyword "("} |-- @{keyword "defaults"} |-- Scan.repeat parse_bound_term --| @{keyword ")"};
  1314 
  1315 val parse_type_arg_constrained =
  1316   Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort);
  1317 
  1318 val parse_type_arg_named_constrained = parse_opt_binding_colon -- parse_type_arg_constrained;
  1319 
  1320 val parse_type_args_named_constrained =
  1321   parse_type_arg_constrained >> (single o pair Binding.empty) ||
  1322   @{keyword "("} |-- Parse.!!! (Parse.list1 parse_type_arg_named_constrained --| @{keyword ")"}) ||
  1323   Scan.succeed [];
  1324 
  1325 val parse_map_rel_binding = Parse.short_ident --| @{keyword ":"} -- parse_binding;
  1326 
  1327 val no_map_rel = (Binding.empty, Binding.empty);
  1328 
  1329 (* "map" and "rel" are purposedly not registered as keywords, because they are short and nice names
  1330    that we don't want them to be highlighted everywhere because of some obscure feature of the BNF
  1331    package. *)
  1332 fun extract_map_rel ("map", b) = apfst (K b)
  1333   | extract_map_rel ("rel", b) = apsnd (K b)
  1334   | extract_map_rel (s, _) = error ("Expected \"map\" or \"rel\" instead of " ^ quote s);
  1335 
  1336 val parse_map_rel_bindings =
  1337   @{keyword "("} |-- Scan.repeat parse_map_rel_binding --| @{keyword ")"}
  1338     >> (fn ps => fold extract_map_rel ps no_map_rel) ||
  1339   Scan.succeed no_map_rel;
  1340 
  1341 val parse_ctr_spec =
  1342   parse_opt_binding_colon -- parse_binding -- Scan.repeat parse_ctr_arg --
  1343   Scan.optional parse_defaults [] -- Parse.opt_mixfix;
  1344 
  1345 val parse_spec =
  1346   parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings --
  1347   Parse.opt_mixfix -- (@{keyword "="} |-- Parse.enum1 "|" parse_ctr_spec);
  1348 
  1349 val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_spec;
  1350 
  1351 fun parse_datatype_cmd lfp construct_fp = parse_datatype >> datatype_cmd lfp construct_fp;
  1352 
  1353 end;