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