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