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