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