src/HOL/BNF/Tools/bnf_fp_util.ML
author blanchet
Thu Jun 06 11:33:41 2013 +0200 (2013-06-06)
changeset 52312 f461dca57c66
parent 52207 21026c312cc3
child 52314 9606cf677021
permissions -rw-r--r--
tuned record field names to avoid confusion between low-level and high-level constants/theorems
     1 (*  Title:      HOL/BNF/Tools/bnf_fp_util.ML
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4     Copyright   2012, 2013
     5 
     6 Shared library for the datatype and codatatype constructions.
     7 *)
     8 
     9 signature BNF_FP_UTIL =
    10 sig
    11   datatype fp_kind = Least_FP | Greatest_FP
    12 
    13   type fp_result =
    14     {Ts: typ list,
    15      bnfs: BNF_Def.bnf list,
    16      ctors: term list,
    17      dtors: term list,
    18      xtor_un_folds: term list,
    19      xtor_co_recs: term list,
    20      xtor_co_induct: thm,
    21      xtor_strong_co_induct: thm,
    22      dtor_ctors: thm list,
    23      ctor_dtors: thm list,
    24      ctor_injects: thm list,
    25      map_thms: thm list,
    26      set_thmss: thm list list,
    27      rel_thms: thm list,
    28      xtor_un_fold_thms: thm list,
    29      xtor_co_rec_thms: thm list}
    30 
    31   val morph_fp_result: morphism -> fp_result -> fp_result
    32   val eq_fp_result: fp_result * fp_result -> bool
    33 
    34   val time: Timer.real_timer -> string -> Timer.real_timer
    35 
    36   val IITN: string
    37   val LevN: string
    38   val algN: string
    39   val behN: string
    40   val bisN: string
    41   val carTN: string
    42   val caseN: string
    43   val coN: string
    44   val coinductN: string
    45   val corecN: string
    46   val ctorN: string
    47   val ctor_dtorN: string
    48   val ctor_dtor_corecN: string
    49   val ctor_dtor_unfoldN: string
    50   val ctor_exhaustN: string
    51   val ctor_induct2N: string
    52   val ctor_inductN: string
    53   val ctor_injectN: string
    54   val ctor_foldN: string
    55   val ctor_fold_uniqueN: string
    56   val ctor_mapN: string
    57   val ctor_map_uniqueN: string
    58   val ctor_recN: string
    59   val ctor_rec_uniqueN: string
    60   val ctor_relN: string
    61   val ctor_set_inclN: string
    62   val ctor_set_set_inclN: string
    63   val disc_unfoldN: string
    64   val disc_unfold_iffN: string
    65   val disc_corecN: string
    66   val disc_corec_iffN: string
    67   val dtorN: string
    68   val dtor_coinductN: string
    69   val dtor_corecN: string
    70   val dtor_corec_uniqueN: string
    71   val dtor_ctorN: string
    72   val dtor_exhaustN: string
    73   val dtor_injectN: string
    74   val dtor_mapN: string
    75   val dtor_map_coinductN: string
    76   val dtor_map_strong_coinductN: string
    77   val dtor_map_uniqueN: string
    78   val dtor_relN: string
    79   val dtor_set_inclN: string
    80   val dtor_set_set_inclN: string
    81   val dtor_strong_coinductN: string
    82   val dtor_unfoldN: string
    83   val dtor_unfold_uniqueN: string
    84   val exhaustN: string
    85   val foldN: string
    86   val hsetN: string
    87   val hset_recN: string
    88   val inductN: string
    89   val injectN: string
    90   val isNodeN: string
    91   val lsbisN: string
    92   val mapN: string
    93   val map_uniqueN: string
    94   val min_algN: string
    95   val morN: string
    96   val nchotomyN: string
    97   val recN: string
    98   val rel_coinductN: string
    99   val rel_inductN: string
   100   val rel_injectN: string
   101   val rel_distinctN: string
   102   val rvN: string
   103   val sel_corecN: string
   104   val set_inclN: string
   105   val set_set_inclN: string
   106   val sel_unfoldN: string
   107   val setsN: string
   108   val simpsN: string
   109   val strTN: string
   110   val str_initN: string
   111   val strong_coinductN: string
   112   val sum_bdN: string
   113   val sum_bdTN: string
   114   val unfoldN: string
   115   val uniqueN: string
   116 
   117   (* TODO: Don't index set facts. Isabelle packages traditionally generate uniform names. *)
   118   val mk_ctor_setN: int -> string
   119   val mk_dtor_setN: int -> string
   120   val mk_dtor_set_inductN: int -> string
   121   val mk_set_inductN: int -> string
   122 
   123   val datatype_word: fp_kind -> string
   124 
   125   val base_name_of_typ: typ -> string
   126   val mk_common_name: string list -> string
   127 
   128   val variant_types: string list -> sort list -> Proof.context ->
   129     (string * sort) list * Proof.context
   130   val variant_tfrees: string list -> Proof.context -> typ list * Proof.context
   131 
   132   val split_conj_thm: thm -> thm list
   133   val split_conj_prems: int -> thm -> thm
   134 
   135   val mk_sumTN: typ list -> typ
   136   val mk_sumTN_balanced: typ list -> typ
   137 
   138   val id_const: typ -> term
   139 
   140   val Inl_const: typ -> typ -> term
   141   val Inr_const: typ -> typ -> term
   142 
   143   val mk_Inl: typ -> term -> term
   144   val mk_Inr: typ -> term -> term
   145   val mk_InN: typ list -> term -> int -> term
   146   val mk_InN_balanced: typ -> int -> term -> int -> term
   147   val mk_sum_case: term * term -> term
   148   val mk_sum_caseN: term list -> term
   149   val mk_sum_caseN_balanced: term list -> term
   150 
   151   val dest_sumT: typ -> typ * typ
   152   val dest_sumTN: int -> typ -> typ list
   153   val dest_sumTN_balanced: int -> typ -> typ list
   154   val dest_tupleT: int -> typ -> typ list
   155 
   156   val mk_Field: term -> term
   157   val mk_If: term -> term -> term -> term
   158   val mk_union: term * term -> term
   159 
   160   val mk_sumEN: int -> thm
   161   val mk_sumEN_balanced: int -> thm
   162   val mk_sumEN_tupled_balanced: int list -> thm
   163   val mk_sum_casesN: int -> int -> thm
   164   val mk_sum_casesN_balanced: int -> int -> thm
   165 
   166   val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
   167 
   168   val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list ->
   169       BNF_Def.bnf list -> local_theory -> 'a) ->
   170     binding list -> (string * sort) list -> ((string * sort) * typ) list -> local_theory ->
   171     BNF_Def.bnf list * 'a
   172 end;
   173 
   174 structure BNF_FP_Util : BNF_FP_UTIL =
   175 struct
   176 
   177 open BNF_Comp
   178 open BNF_Def
   179 open BNF_Util
   180 
   181 datatype fp_kind = Least_FP | Greatest_FP;
   182 
   183 type fp_result =
   184   {Ts: typ list,
   185    bnfs: BNF_Def.bnf list,
   186    ctors: term list,
   187    dtors: term list,
   188    xtor_un_folds: term list,
   189    xtor_co_recs: term list,
   190    xtor_co_induct: thm,
   191    xtor_strong_co_induct: thm,
   192    dtor_ctors: thm list,
   193    ctor_dtors: thm list,
   194    ctor_injects: thm list,
   195    map_thms: thm list,
   196    set_thmss: thm list list,
   197    rel_thms: thm list,
   198    xtor_un_fold_thms: thm list,
   199    xtor_co_rec_thms: thm list};
   200 
   201 fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_un_folds, xtor_co_recs, xtor_co_induct,
   202     xtor_strong_co_induct, dtor_ctors, ctor_dtors, ctor_injects, map_thms, set_thmss, rel_thms,
   203     xtor_un_fold_thms, xtor_co_rec_thms} =
   204   {Ts = map (Morphism.typ phi) Ts,
   205    bnfs = map (morph_bnf phi) bnfs,
   206    ctors = map (Morphism.term phi) ctors,
   207    dtors = map (Morphism.term phi) dtors,
   208    xtor_un_folds = map (Morphism.term phi) xtor_un_folds,
   209    xtor_co_recs = map (Morphism.term phi) xtor_co_recs,
   210    xtor_co_induct = Morphism.thm phi xtor_co_induct,
   211    xtor_strong_co_induct = Morphism.thm phi xtor_strong_co_induct,
   212    dtor_ctors = map (Morphism.thm phi) dtor_ctors,
   213    ctor_dtors = map (Morphism.thm phi) ctor_dtors,
   214    ctor_injects = map (Morphism.thm phi) ctor_injects,
   215    map_thms = map (Morphism.thm phi) map_thms,
   216    set_thmss = map (map (Morphism.thm phi)) set_thmss,
   217    rel_thms = map (Morphism.thm phi) rel_thms,
   218    xtor_un_fold_thms = map (Morphism.thm phi) xtor_un_fold_thms,
   219    xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms};
   220 
   221 fun eq_fp_result ({bnfs = bnfs1, ...} : fp_result, {bnfs = bnfs2, ...} : fp_result) =
   222   eq_list eq_bnf (bnfs1, bnfs2);
   223 
   224 val timing = true;
   225 fun time timer msg = (if timing
   226   then warning (msg ^ ": " ^ ATP_Util.string_of_time (Timer.checkRealTimer timer))
   227   else (); Timer.startRealTimer ());
   228 
   229 val preN = "pre_"
   230 val rawN = "raw_"
   231 
   232 val coN = "co"
   233 val unN = "un"
   234 val algN = "alg"
   235 val IITN = "IITN"
   236 val foldN = "fold"
   237 val unfoldN = unN ^ foldN
   238 val uniqueN = "_unique"
   239 val simpsN = "simps"
   240 val ctorN = "ctor"
   241 val dtorN = "dtor"
   242 val ctor_foldN = ctorN ^ "_" ^ foldN
   243 val dtor_unfoldN = dtorN ^ "_" ^ unfoldN
   244 val ctor_fold_uniqueN = ctor_foldN ^ uniqueN
   245 val dtor_unfold_uniqueN = dtor_unfoldN ^ uniqueN
   246 val ctor_dtor_unfoldN = ctorN ^ "_" ^ dtor_unfoldN
   247 val ctor_mapN = ctorN ^ "_" ^ mapN
   248 val dtor_mapN = dtorN ^ "_" ^ mapN
   249 val map_uniqueN = mapN ^ uniqueN
   250 val ctor_map_uniqueN = ctorN ^ "_" ^ map_uniqueN
   251 val dtor_map_uniqueN = dtorN ^ "_" ^ map_uniqueN
   252 val min_algN = "min_alg"
   253 val morN = "mor"
   254 val bisN = "bis"
   255 val lsbisN = "lsbis"
   256 val sum_bdTN = "sbdT"
   257 val sum_bdN = "sbd"
   258 val carTN = "carT"
   259 val strTN = "strT"
   260 val isNodeN = "isNode"
   261 val LevN = "Lev"
   262 val rvN = "recover"
   263 val behN = "beh"
   264 val setsN = "sets"
   265 val mk_ctor_setN = prefix (ctorN ^ "_") o mk_setN
   266 val mk_dtor_setN = prefix (dtorN ^ "_") o mk_setN
   267 fun mk_set_inductN i = mk_setN i ^ "_induct"
   268 val mk_dtor_set_inductN = prefix (dtorN ^ "_") o mk_set_inductN
   269 
   270 val str_initN = "str_init"
   271 val recN = "rec"
   272 val corecN = coN ^ recN
   273 val ctor_recN = ctorN ^ "_" ^ recN
   274 val ctor_rec_uniqueN = ctor_recN ^ uniqueN
   275 val dtor_corecN = dtorN ^ "_" ^ corecN
   276 val dtor_corec_uniqueN = dtor_corecN ^ uniqueN
   277 val ctor_dtor_corecN = ctorN ^ "_" ^ dtor_corecN
   278 
   279 val ctor_dtorN = ctorN ^ "_" ^ dtorN
   280 val dtor_ctorN = dtorN ^ "_" ^ ctorN
   281 val nchotomyN = "nchotomy"
   282 val injectN = "inject"
   283 val exhaustN = "exhaust"
   284 val ctor_injectN = ctorN ^ "_" ^ injectN
   285 val ctor_exhaustN = ctorN ^ "_" ^ exhaustN
   286 val dtor_injectN = dtorN ^ "_" ^ injectN
   287 val dtor_exhaustN = dtorN ^ "_" ^ exhaustN
   288 val ctor_relN = ctorN ^ "_" ^ relN
   289 val dtor_relN = dtorN ^ "_" ^ relN
   290 val inductN = "induct"
   291 val coinductN = coN ^ inductN
   292 val ctor_inductN = ctorN ^ "_" ^ inductN
   293 val ctor_induct2N = ctor_inductN ^ "2"
   294 val dtor_map_coinductN = dtor_mapN ^ "_" ^ coinductN
   295 val dtor_coinductN = dtorN ^ "_" ^ coinductN
   296 val strong_coinductN = "strong_" ^ coinductN
   297 val dtor_map_strong_coinductN = dtor_mapN ^ "_" ^ strong_coinductN
   298 val dtor_strong_coinductN = dtorN ^ "_" ^ strong_coinductN
   299 val hsetN = "Hset"
   300 val hset_recN = hsetN ^ "_rec"
   301 val set_inclN = "set_incl"
   302 val ctor_set_inclN = ctorN ^ "_" ^ set_inclN
   303 val dtor_set_inclN = dtorN ^ "_" ^ set_inclN
   304 val set_set_inclN = "set_set_incl"
   305 val ctor_set_set_inclN = ctorN ^ "_" ^ set_set_inclN
   306 val dtor_set_set_inclN = dtorN ^ "_" ^ set_set_inclN
   307 
   308 val caseN = "case"
   309 val discN = "disc"
   310 val disc_unfoldN = discN ^ "_" ^ unfoldN
   311 val disc_corecN = discN ^ "_" ^ corecN
   312 val iffN = "_iff"
   313 val disc_unfold_iffN = discN ^ "_" ^ unfoldN ^ iffN
   314 val disc_corec_iffN = discN ^ "_" ^ corecN ^ iffN
   315 val distinctN = "distinct"
   316 val rel_distinctN = relN ^ "_" ^ distinctN
   317 val injectN = "inject"
   318 val rel_injectN = relN ^ "_" ^ injectN
   319 val rel_coinductN = relN ^ "_" ^ coinductN
   320 val rel_inductN = relN ^ "_" ^ inductN
   321 val selN = "sel"
   322 val sel_unfoldN = selN ^ "_" ^ unfoldN
   323 val sel_corecN = selN ^ "_" ^ corecN
   324 
   325 fun datatype_word fp = (if fp = Greatest_FP then "co" else "") ^ "datatype";
   326 
   327 fun add_components_of_typ (Type (s, Ts)) =
   328     fold add_components_of_typ Ts #> cons (Long_Name.base_name s)
   329   | add_components_of_typ _ = I;
   330 
   331 fun base_name_of_typ T = space_implode "_" (add_components_of_typ T []);
   332 
   333 val mk_common_name = space_implode "_";
   334 
   335 fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T');
   336 
   337 fun dest_sumTN 1 T = [T]
   338   | dest_sumTN n (Type (@{type_name sum}, [T, T'])) = T :: dest_sumTN (n - 1) T';
   339 
   340 val dest_sumTN_balanced = Balanced_Tree.dest dest_sumT;
   341 
   342 (* TODO: move something like this to "HOLogic"? *)
   343 fun dest_tupleT 0 @{typ unit} = []
   344   | dest_tupleT 1 T = [T]
   345   | dest_tupleT n (Type (@{type_name prod}, [T, T'])) = T :: dest_tupleT (n - 1) T';
   346 
   347 val mk_sumTN = Library.foldr1 mk_sumT;
   348 val mk_sumTN_balanced = Balanced_Tree.make mk_sumT;
   349 
   350 fun id_const T = Const (@{const_name id}, T --> T);
   351 
   352 fun Inl_const LT RT = Const (@{const_name Inl}, LT --> mk_sumT (LT, RT));
   353 fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t;
   354 
   355 fun Inr_const LT RT = Const (@{const_name Inr}, RT --> mk_sumT (LT, RT));
   356 fun mk_Inr LT t = Inr_const LT (fastype_of t) $ t;
   357 
   358 fun mk_InN [_] t 1 = t
   359   | mk_InN (_ :: Ts) t 1 = mk_Inl (mk_sumTN Ts) t
   360   | mk_InN (LT :: Ts) t m = mk_Inr LT (mk_InN Ts t (m - 1))
   361   | mk_InN Ts t _ = raise (TYPE ("mk_InN", Ts, [t]));
   362 
   363 fun mk_InN_balanced sum_T n t k =
   364   let
   365     fun repair_types T (Const (s as @{const_name Inl}, _) $ t) = repair_inj_types T s fst t
   366       | repair_types T (Const (s as @{const_name Inr}, _) $ t) = repair_inj_types T s snd t
   367       | repair_types _ t = t
   368     and repair_inj_types T s get t =
   369       let val T' = get (dest_sumT T) in
   370         Const (s, T' --> T) $ repair_types T' t
   371       end;
   372   in
   373     Balanced_Tree.access {left = mk_Inl dummyT, right = mk_Inr dummyT, init = t} n k
   374     |> repair_types sum_T
   375   end;
   376 
   377 fun mk_sum_case (f, g) =
   378   let
   379     val fT = fastype_of f;
   380     val gT = fastype_of g;
   381   in
   382     Const (@{const_name sum_case},
   383       fT --> gT --> mk_sumT (domain_type fT, domain_type gT) --> range_type fT) $ f $ g
   384   end;
   385 
   386 val mk_sum_caseN = Library.foldr1 mk_sum_case;
   387 val mk_sum_caseN_balanced = Balanced_Tree.make mk_sum_case;
   388 
   389 fun mk_If p t f =
   390   let val T = fastype_of t;
   391   in Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ p $ t $ f end;
   392 
   393 fun mk_Field r =
   394   let val T = fst (dest_relT (fastype_of r));
   395   in Const (@{const_name Field}, mk_relT (T, T) --> HOLogic.mk_setT T) $ r end;
   396 
   397 val mk_union = HOLogic.mk_binop @{const_name sup};
   398 
   399 (*dangerous; use with monotonic, converging functions only!*)
   400 fun fixpoint eq f X = if subset eq (f X, X) then X else fixpoint eq f (f X);
   401 
   402 fun variant_types ss Ss ctxt =
   403   let
   404     val (tfrees, _) =
   405       fold_map2 (fn s => fn S => Name.variant s #> apfst (rpair S)) ss Ss (Variable.names_of ctxt);
   406     val ctxt' = fold (Variable.declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
   407   in (tfrees, ctxt') end;
   408 
   409 fun variant_tfrees ss =
   410   apfst (map TFree) o variant_types (map (prefix "'") ss) (replicate (length ss) HOLogic.typeS);
   411 
   412 (* stolen from "~~/src/HOL/Tools/Datatype/datatype_aux.ML" *)
   413 fun split_conj_thm th =
   414   ((th RS conjunct1) :: split_conj_thm (th RS conjunct2)) handle THM _ => [th];
   415 
   416 fun split_conj_prems limit th =
   417   let
   418     fun split n i th =
   419       if i = n then th else split n (i + 1) (conjI RSN (i, th)) handle THM _ => th;
   420   in split limit 1 th end;
   421 
   422 fun mk_sumEN 1 = @{thm one_pointE}
   423   | mk_sumEN 2 = @{thm sumE}
   424   | mk_sumEN n =
   425     (fold (fn i => fn thm => @{thm obj_sum_step} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF
   426       replicate n (impI RS allI);
   427 
   428 fun mk_obj_sumEN_balanced n =
   429   Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f})))
   430     (replicate n asm_rl);
   431 
   432 fun mk_sumEN_balanced' n all_impIs = mk_obj_sumEN_balanced n OF all_impIs RS @{thm obj_one_pointE};
   433 
   434 fun mk_sumEN_balanced 1 = @{thm one_pointE} (*optimization*)
   435   | mk_sumEN_balanced 2 = @{thm sumE} (*optimization*)
   436   | mk_sumEN_balanced n = mk_sumEN_balanced' n (replicate n (impI RS allI));
   437 
   438 fun mk_tupled_allIN 0 = @{thm unit_all_impI}
   439   | mk_tupled_allIN 1 = @{thm impI[THEN allI]}
   440   | mk_tupled_allIN 2 = @{thm prod_all_impI} (*optimization*)
   441   | mk_tupled_allIN n = mk_tupled_allIN (n - 1) RS @{thm prod_all_impI_step};
   442 
   443 fun mk_sumEN_tupled_balanced ms =
   444   let val n = length ms in
   445     if forall (curry (op =) 1) ms then mk_sumEN_balanced n
   446     else mk_sumEN_balanced' n (map mk_tupled_allIN ms)
   447   end;
   448 
   449 fun mk_sum_casesN 1 1 = refl
   450   | mk_sum_casesN _ 1 = @{thm sum.cases(1)}
   451   | mk_sum_casesN 2 2 = @{thm sum.cases(2)}
   452   | mk_sum_casesN n k = trans OF [@{thm sum_case_step(2)}, mk_sum_casesN (n - 1) (k - 1)];
   453 
   454 fun mk_sum_step base step thm =
   455   if Thm.eq_thm_prop (thm, refl) then base else trans OF [step, thm];
   456 
   457 fun mk_sum_casesN_balanced 1 1 = refl
   458   | mk_sum_casesN_balanced n k =
   459     Balanced_Tree.access {left = mk_sum_step @{thm sum.cases(1)} @{thm sum_case_step(1)},
   460       right = mk_sum_step @{thm sum.cases(2)} @{thm sum_case_step(2)}, init = refl} n k;
   461 
   462 fun fp_bnf construct_fp bs resBs eqs lthy =
   463   let
   464     val timer = time (Timer.startRealTimer ());
   465     val (lhss, rhss) = split_list eqs;
   466 
   467     (* FIXME: because of "@ lhss", the output could contain type variables that are not in the
   468        input; also, "fp_sort" should put the "resBs" first and in the order in which they appear *)
   469     fun fp_sort Ass =
   470       subtract (op =) lhss (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs) @ lhss;
   471 
   472     fun raw_qualify b = Binding.qualify true (Binding.name_of (Binding.prefix_name rawN b));
   473 
   474     val ((bnfs, (deadss, livess)), (unfold_set, lthy)) = apfst (apsnd split_list o split_list)
   475       (fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) fp_sort) bs rhss
   476         (empty_unfolds, lthy));
   477 
   478     val name = mk_common_name (map Binding.name_of bs);
   479     fun qualify i =
   480       let val namei = name ^ nonzero_string_of_int i;
   481       in Binding.qualify true namei end;
   482 
   483     val Ass = map (map dest_TFree) livess;
   484     val resDs = fold (subtract (op =)) Ass resBs;
   485     val Ds = fold (fold Term.add_tfreesT) deadss [];
   486 
   487     val _ = (case Library.inter (op =) Ds lhss of [] => ()
   488       | A :: _ => error ("Inadmissible type recursion (cannot take fixed point of dead type \
   489         \variable " ^ quote (Syntax.string_of_typ lthy (TFree A)) ^ ")"));
   490 
   491     val timer = time (timer "Construction of BNFs");
   492 
   493     val ((kill_poss, _), (bnfs', (unfold_set', lthy'))) =
   494       normalize_bnfs qualify Ass Ds fp_sort bnfs unfold_set lthy;
   495 
   496     val Dss = map3 (append oo map o nth) livess kill_poss deadss;
   497 
   498     val ((pre_bnfs, deadss), lthy'') =
   499       fold_map3 (seal_bnf unfold_set') (map (Binding.prefix_name preN) bs) Dss bnfs' lthy'
   500       |>> split_list;
   501 
   502     val timer = time (timer "Normalization & sealing of BNFs");
   503 
   504     val res = construct_fp bs resBs (map TFree resDs, deadss) pre_bnfs lthy'';
   505 
   506     val timer = time (timer "FP construction in total");
   507   in
   508     timer; (pre_bnfs, res)
   509   end;
   510 
   511 end;