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