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