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