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