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