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