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