renamed "bnf_fp_util.ML" to "bnf_fp.ML"
authorblanchet
Thu Sep 20 02:42:48 2012 +0200 (2012-09-20)
changeset 494571d2825673cec
parent 49456 fa8302c8dea1
child 49458 9321a9465021
renamed "bnf_fp_util.ML" to "bnf_fp.ML"
src/HOL/Codatatype/BNF_FP.thy
src/HOL/Codatatype/Tools/bnf_fp.ML
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
src/HOL/Codatatype/Tools/bnf_fp_util.ML
src/HOL/Codatatype/Tools/bnf_gfp.ML
src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML
src/HOL/Codatatype/Tools/bnf_lfp.ML
     1.1 --- a/src/HOL/Codatatype/BNF_FP.thy	Thu Sep 20 02:42:48 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/BNF_FP.thy	Thu Sep 20 02:42:48 2012 +0200
     1.3 @@ -119,7 +119,7 @@
     1.4  "setr (Inr x) = {x}"
     1.5  unfolding sum_set_defs by simp+
     1.6  
     1.7 -ML_file "Tools/bnf_fp_util.ML"
     1.8 +ML_file "Tools/bnf_fp.ML"
     1.9  ML_file "Tools/bnf_fp_sugar_tactics.ML"
    1.10  ML_file "Tools/bnf_fp_sugar.ML"
    1.11  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp.ML	Thu Sep 20 02:42:48 2012 +0200
     2.3 @@ -0,0 +1,439 @@
     2.4 +(*  Title:      HOL/Codatatype/Tools/bnf_fp.ML
     2.5 +    Author:     Dmitriy Traytel, TU Muenchen
     2.6 +    Copyright   2012
     2.7 +
     2.8 +Shared library for the datatype and codatatype constructions.
     2.9 +*)
    2.10 +
    2.11 +signature BNF_FP =
    2.12 +sig
    2.13 +  val time: Timer.real_timer -> string -> Timer.real_timer
    2.14 +
    2.15 +  val IITN: string
    2.16 +  val LevN: string
    2.17 +  val algN: string
    2.18 +  val behN: string
    2.19 +  val bisN: string
    2.20 +  val carTN: string
    2.21 +  val caseN: string
    2.22 +  val coN: string
    2.23 +  val coinductN: string
    2.24 +  val coiterN: string
    2.25 +  val coitersN: string
    2.26 +  val corecN: string
    2.27 +  val corecsN: string
    2.28 +  val disc_coitersN: string
    2.29 +  val disc_corecsN: string
    2.30 +  val exhaustN: string
    2.31 +  val fldN: string
    2.32 +  val fld_exhaustN: string
    2.33 +  val fld_induct2N: string
    2.34 +  val fld_inductN: string
    2.35 +  val fld_injectN: string
    2.36 +  val fld_iterN: string
    2.37 +  val fld_iter_uniqueN: string
    2.38 +  val fld_itersN: string
    2.39 +  val fld_recN: string
    2.40 +  val fld_recsN: string
    2.41 +  val fld_unfN: string
    2.42 +  val fld_unf_coitersN: string
    2.43 +  val fld_unf_corecsN: string
    2.44 +  val hsetN: string
    2.45 +  val hset_recN: string
    2.46 +  val inductN: string
    2.47 +  val injectN: string
    2.48 +  val isNodeN: string
    2.49 +  val iterN: string
    2.50 +  val itersN: string
    2.51 +  val lsbisN: string
    2.52 +  val map_simpsN: string
    2.53 +  val map_uniqueN: string
    2.54 +  val min_algN: string
    2.55 +  val morN: string
    2.56 +  val nchotomyN: string
    2.57 +  val pred_coinductN: string
    2.58 +  val pred_coinduct_uptoN: string
    2.59 +  val pred_simpN: string
    2.60 +  val recN: string
    2.61 +  val recsN: string
    2.62 +  val rel_coinductN: string
    2.63 +  val rel_coinduct_uptoN: string
    2.64 +  val rel_simpN: string
    2.65 +  val rvN: string
    2.66 +  val sel_coitersN: string
    2.67 +  val sel_corecsN: string
    2.68 +  val set_inclN: string
    2.69 +  val set_set_inclN: string
    2.70 +  val simpsN: string
    2.71 +  val strTN: string
    2.72 +  val str_initN: string
    2.73 +  val sum_bdN: string
    2.74 +  val sum_bdTN: string
    2.75 +  val unfN: string
    2.76 +  val unf_coinductN: string
    2.77 +  val unf_coinduct_uptoN: string
    2.78 +  val unf_coiterN: string
    2.79 +  val unf_coiter_uniqueN: string
    2.80 +  val unf_coitersN: string
    2.81 +  val unf_corecN: string
    2.82 +  val unf_corecsN: string
    2.83 +  val unf_exhaustN: string
    2.84 +  val unf_fldN: string
    2.85 +  val unf_injectN: string
    2.86 +  val uniqueN: string
    2.87 +  val uptoN: string
    2.88 +
    2.89 +  val mk_exhaustN: string -> string
    2.90 +  val mk_injectN: string -> string
    2.91 +  val mk_nchotomyN: string -> string
    2.92 +  val mk_set_simpsN: int -> string
    2.93 +  val mk_set_minimalN: int -> string
    2.94 +  val mk_set_inductN: int -> string
    2.95 +
    2.96 +  val mk_common_name: binding list -> string
    2.97 +
    2.98 +  val split_conj_thm: thm -> thm list
    2.99 +  val split_conj_prems: int -> thm -> thm
   2.100 +
   2.101 +  val retype_free: typ -> term -> term
   2.102 +
   2.103 +  val mk_predT: typ -> typ;
   2.104 +
   2.105 +  val mk_sumTN: typ list -> typ
   2.106 +  val mk_sumTN_balanced: typ list -> typ
   2.107 +
   2.108 +  val id_const: typ -> term
   2.109 +  val id_abs: typ -> term
   2.110 +
   2.111 +  val Inl_const: typ -> typ -> term
   2.112 +  val Inr_const: typ -> typ -> term
   2.113 +
   2.114 +  val mk_Inl: typ -> term -> term
   2.115 +  val mk_Inr: typ -> term -> term
   2.116 +  val mk_InN: typ list -> term -> int -> term
   2.117 +  val mk_InN_balanced: typ -> int -> term -> int -> term
   2.118 +  val mk_sum_case: term * term -> term
   2.119 +  val mk_sum_caseN: term list -> term
   2.120 +  val mk_sum_caseN_balanced: term list -> term
   2.121 +
   2.122 +  val dest_sumT: typ -> typ * typ
   2.123 +  val dest_sumTN: int -> typ -> typ list
   2.124 +  val dest_sumTN_balanced: int -> typ -> typ list
   2.125 +  val dest_tupleT: int -> typ -> typ list
   2.126 +
   2.127 +  val mk_Field: term -> term
   2.128 +  val mk_If: term -> term -> term -> term
   2.129 +  val mk_union: term * term -> term
   2.130 +
   2.131 +  val mk_sumEN: int -> thm
   2.132 +  val mk_sumEN_balanced: int -> thm
   2.133 +  val mk_sumEN_tupled_balanced: int list -> thm
   2.134 +  val mk_sum_casesN: int -> int -> thm
   2.135 +  val mk_sum_casesN_balanced: int -> int -> thm
   2.136 +
   2.137 +  val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
   2.138 +
   2.139 +  val fp_bnf: (mixfix list -> (string * sort) list option -> binding list ->
   2.140 +    typ list * typ list list -> BNF_Def.BNF list -> local_theory -> 'a) ->
   2.141 +    binding list -> mixfix list -> (string * sort) list -> ((string * sort) * typ) list ->
   2.142 +    local_theory -> BNF_Def.BNF list * 'a
   2.143 +  val fp_bnf_cmd: (mixfix list -> (string * sort) list option -> binding list ->
   2.144 +    typ list * typ list list -> BNF_Def.BNF list -> local_theory -> 'a) ->
   2.145 +    binding list * (string list * string list) -> local_theory -> 'a
   2.146 +end;
   2.147 +
   2.148 +structure BNF_FP : BNF_FP =
   2.149 +struct
   2.150 +
   2.151 +open BNF_Comp
   2.152 +open BNF_Def
   2.153 +open BNF_Util
   2.154 +
   2.155 +val timing = true;
   2.156 +fun time timer msg = (if timing
   2.157 +  then warning (msg ^ ": " ^ ATP_Util.string_from_time (Timer.checkRealTimer timer))
   2.158 +  else (); Timer.startRealTimer ());
   2.159 +
   2.160 +val preN = "pre_"
   2.161 +val rawN = "raw_"
   2.162 +
   2.163 +val coN = "co"
   2.164 +val algN = "alg"
   2.165 +val IITN = "IITN"
   2.166 +val iterN = "iter"
   2.167 +val itersN = iterN ^ "s"
   2.168 +val coiterN = coN ^ iterN
   2.169 +val coitersN = coiterN ^ "s"
   2.170 +val uniqueN = "_unique"
   2.171 +val simpsN = "simps"
   2.172 +val fldN = "fld"
   2.173 +val unfN = "unf"
   2.174 +val fld_iterN = fldN ^ "_" ^ iterN
   2.175 +val fld_itersN = fld_iterN ^ "s"
   2.176 +val unf_coiterN = unfN ^ "_" ^ coiterN
   2.177 +val unf_coitersN = unf_coiterN ^ "s"
   2.178 +val fld_iter_uniqueN = fld_iterN ^ uniqueN
   2.179 +val unf_coiter_uniqueN = unf_coiterN ^ uniqueN
   2.180 +val fld_unf_coitersN = fldN ^ "_" ^ unf_coiterN ^ "s"
   2.181 +val map_simpsN = mapN ^ "_" ^ simpsN
   2.182 +val map_uniqueN = mapN ^ uniqueN
   2.183 +val min_algN = "min_alg"
   2.184 +val morN = "mor"
   2.185 +val bisN = "bis"
   2.186 +val lsbisN = "lsbis"
   2.187 +val sum_bdTN = "sbdT"
   2.188 +val sum_bdN = "sbd"
   2.189 +val carTN = "carT"
   2.190 +val strTN = "strT"
   2.191 +val isNodeN = "isNode"
   2.192 +val LevN = "Lev"
   2.193 +val rvN = "recover"
   2.194 +val behN = "beh"
   2.195 +fun mk_set_simpsN i = mk_setN i ^ "_" ^ simpsN
   2.196 +fun mk_set_minimalN i = mk_setN i ^ "_minimal"
   2.197 +fun mk_set_inductN i = mk_setN i ^ "_induct"
   2.198 +
   2.199 +val str_initN = "str_init"
   2.200 +val recN = "rec"
   2.201 +val recsN = recN ^ "s"
   2.202 +val corecN = coN ^ recN
   2.203 +val corecsN = corecN ^ "s"
   2.204 +val fld_recN = fldN ^ "_" ^ recN
   2.205 +val fld_recsN = fld_recN ^ "s"
   2.206 +val unf_corecN = unfN ^ "_" ^ corecN
   2.207 +val unf_corecsN = unf_corecN ^ "s"
   2.208 +val fld_unf_corecsN = fldN ^ "_" ^ unf_corecN ^ "s"
   2.209 +
   2.210 +val fld_unfN = fldN ^ "_" ^ unfN
   2.211 +val unf_fldN = unfN ^ "_" ^ fldN
   2.212 +val nchotomyN = "nchotomy"
   2.213 +fun mk_nchotomyN s = s ^ "_" ^ nchotomyN
   2.214 +val injectN = "inject"
   2.215 +fun mk_injectN s = s ^ "_" ^ injectN
   2.216 +val exhaustN = "exhaust"
   2.217 +fun mk_exhaustN s = s ^ "_" ^ exhaustN
   2.218 +val fld_injectN = mk_injectN fldN
   2.219 +val fld_exhaustN = mk_exhaustN fldN
   2.220 +val unf_injectN = mk_injectN unfN
   2.221 +val unf_exhaustN = mk_exhaustN unfN
   2.222 +val inductN = "induct"
   2.223 +val coinductN = coN ^ inductN
   2.224 +val fld_inductN = fldN ^ "_" ^ inductN
   2.225 +val fld_induct2N = fld_inductN ^ "2"
   2.226 +val unf_coinductN = unfN ^ "_" ^ coinductN
   2.227 +val rel_coinductN = relN ^ "_" ^ coinductN
   2.228 +val pred_coinductN = predN ^ "_" ^ coinductN
   2.229 +val simpN = "_simp";
   2.230 +val rel_simpN = relN ^ simpN;
   2.231 +val pred_simpN = predN ^ simpN;
   2.232 +val uptoN = "upto"
   2.233 +val unf_coinduct_uptoN = unf_coinductN ^ "_" ^ uptoN
   2.234 +val rel_coinduct_uptoN = rel_coinductN ^ "_" ^ uptoN
   2.235 +val pred_coinduct_uptoN = pred_coinductN ^ "_" ^ uptoN
   2.236 +val hsetN = "Hset"
   2.237 +val hset_recN = hsetN ^ "_rec"
   2.238 +val set_inclN = "set_incl"
   2.239 +val set_set_inclN = "set_set_incl"
   2.240 +
   2.241 +val caseN = "case"
   2.242 +val discN = "disc"
   2.243 +val disc_coitersN = discN ^ "_" ^ coitersN
   2.244 +val disc_corecsN = discN ^ "_" ^ corecsN
   2.245 +val selN = "sel"
   2.246 +val sel_coitersN = selN ^ "_" ^ coitersN
   2.247 +val sel_corecsN = selN ^ "_" ^ corecsN
   2.248 +
   2.249 +val mk_common_name = space_implode "_" o map Binding.name_of;
   2.250 +
   2.251 +fun mk_predT T = T --> HOLogic.boolT;
   2.252 +
   2.253 +fun retype_free T (Free (s, _)) = Free (s, T);
   2.254 +
   2.255 +fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T');
   2.256 +
   2.257 +fun dest_sumTN 1 T = [T]
   2.258 +  | dest_sumTN n (Type (@{type_name sum}, [T, T'])) = T :: dest_sumTN (n - 1) T';
   2.259 +
   2.260 +val dest_sumTN_balanced = Balanced_Tree.dest dest_sumT;
   2.261 +
   2.262 +(* TODO: move something like this to "HOLogic"? *)
   2.263 +fun dest_tupleT 0 @{typ unit} = []
   2.264 +  | dest_tupleT 1 T = [T]
   2.265 +  | dest_tupleT n (Type (@{type_name prod}, [T, T'])) = T :: dest_tupleT (n - 1) T';
   2.266 +
   2.267 +val mk_sumTN = Library.foldr1 mk_sumT;
   2.268 +val mk_sumTN_balanced = Balanced_Tree.make mk_sumT;
   2.269 +
   2.270 +fun id_const T = Const (@{const_name id}, T --> T);
   2.271 +fun id_abs T = Abs (Name.uu, T, Bound 0);
   2.272 +
   2.273 +fun Inl_const LT RT = Const (@{const_name Inl}, LT --> mk_sumT (LT, RT));
   2.274 +fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t;
   2.275 +
   2.276 +fun Inr_const LT RT = Const (@{const_name Inr}, RT --> mk_sumT (LT, RT));
   2.277 +fun mk_Inr LT t = Inr_const LT (fastype_of t) $ t;
   2.278 +
   2.279 +fun mk_InN [_] t 1 = t
   2.280 +  | mk_InN (_ :: Ts) t 1 = mk_Inl (mk_sumTN Ts) t
   2.281 +  | mk_InN (LT :: Ts) t m = mk_Inr LT (mk_InN Ts t (m - 1))
   2.282 +  | mk_InN Ts t _ = raise (TYPE ("mk_InN", Ts, [t]));
   2.283 +
   2.284 +fun mk_InN_balanced sum_T n t k =
   2.285 +  let
   2.286 +    fun repair_types T (Const (s as @{const_name Inl}, _) $ t) = repair_inj_types T s fst t
   2.287 +      | repair_types T (Const (s as @{const_name Inr}, _) $ t) = repair_inj_types T s snd t
   2.288 +      | repair_types _ t = t
   2.289 +    and repair_inj_types T s get t =
   2.290 +      let val T' = get (dest_sumT T) in
   2.291 +        Const (s, T' --> T) $ repair_types T' t
   2.292 +      end;
   2.293 +  in
   2.294 +    Balanced_Tree.access {left = mk_Inl dummyT, right = mk_Inr dummyT, init = t} n k
   2.295 +    |> repair_types sum_T
   2.296 +  end;
   2.297 +
   2.298 +fun mk_sum_case (f, g) =
   2.299 +  let
   2.300 +    val fT = fastype_of f;
   2.301 +    val gT = fastype_of g;
   2.302 +  in
   2.303 +    Const (@{const_name sum_case},
   2.304 +      fT --> gT --> mk_sumT (domain_type fT, domain_type gT) --> range_type fT) $ f $ g
   2.305 +  end;
   2.306 +
   2.307 +val mk_sum_caseN = Library.foldr1 mk_sum_case;
   2.308 +val mk_sum_caseN_balanced = Balanced_Tree.make mk_sum_case;
   2.309 +
   2.310 +fun mk_If p t f =
   2.311 +  let val T = fastype_of t;
   2.312 +  in Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ p $ t $ f end;
   2.313 +
   2.314 +fun mk_Field r =
   2.315 +  let val T = fst (dest_relT (fastype_of r));
   2.316 +  in Const (@{const_name Field}, mk_relT (T, T) --> HOLogic.mk_setT T) $ r end;
   2.317 +
   2.318 +val mk_union = HOLogic.mk_binop @{const_name sup};
   2.319 +
   2.320 +(*dangerous; use with monotonic, converging functions only!*)
   2.321 +fun fixpoint eq f X = if subset eq (f X, X) then X else fixpoint eq f (f X);
   2.322 +
   2.323 +(* stolen from "~~/src/HOL/Tools/Datatype/datatype_aux.ML" *)
   2.324 +fun split_conj_thm th =
   2.325 +  ((th RS conjunct1) :: split_conj_thm (th RS conjunct2)) handle THM _ => [th];
   2.326 +
   2.327 +fun split_conj_prems limit th =
   2.328 +  let
   2.329 +    fun split n i th =
   2.330 +      if i = n then th else split n (i + 1) (conjI RSN (i, th)) handle THM _ => th;
   2.331 +  in split limit 1 th end;
   2.332 +
   2.333 +fun mk_sumEN 1 = @{thm one_pointE}
   2.334 +  | mk_sumEN 2 = @{thm sumE}
   2.335 +  | mk_sumEN n =
   2.336 +    (fold (fn i => fn thm => @{thm obj_sum_step} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF
   2.337 +      replicate n (impI RS allI);
   2.338 +
   2.339 +fun mk_obj_sumEN_balanced n =
   2.340 +  Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f})))
   2.341 +    (replicate n asm_rl);
   2.342 +
   2.343 +fun mk_sumEN_balanced' n all_impIs = mk_obj_sumEN_balanced n OF all_impIs RS @{thm obj_one_pointE};
   2.344 +
   2.345 +fun mk_sumEN_balanced 1 = @{thm one_pointE} (*optimization*)
   2.346 +  | mk_sumEN_balanced 2 = @{thm sumE} (*optimization*)
   2.347 +  | mk_sumEN_balanced n = mk_sumEN_balanced' n (replicate n (impI RS allI));
   2.348 +
   2.349 +fun mk_tupled_allIN 0 = @{thm unit_all_impI}
   2.350 +  | mk_tupled_allIN 1 = @{thm impI[THEN allI]}
   2.351 +  | mk_tupled_allIN 2 = @{thm prod_all_impI} (*optimization*)
   2.352 +  | mk_tupled_allIN n = mk_tupled_allIN (n - 1) RS @{thm prod_all_impI_step};
   2.353 +
   2.354 +fun mk_sumEN_tupled_balanced ms =
   2.355 +  let val n = length ms in
   2.356 +    if forall (curry (op =) 1) ms then mk_sumEN_balanced n
   2.357 +    else mk_sumEN_balanced' n (map mk_tupled_allIN ms)
   2.358 +  end;
   2.359 +
   2.360 +fun mk_sum_casesN 1 1 = refl
   2.361 +  | mk_sum_casesN _ 1 = @{thm sum.cases(1)}
   2.362 +  | mk_sum_casesN 2 2 = @{thm sum.cases(2)}
   2.363 +  | mk_sum_casesN n k = trans OF [@{thm sum_case_step(2)}, mk_sum_casesN (n - 1) (k - 1)];
   2.364 +
   2.365 +fun mk_sum_step base step thm =
   2.366 +  if Thm.eq_thm_prop (thm, refl) then base else trans OF [step, thm];
   2.367 +
   2.368 +fun mk_sum_casesN_balanced 1 1 = refl
   2.369 +  | mk_sum_casesN_balanced n k =
   2.370 +    Balanced_Tree.access {left = mk_sum_step @{thm sum.cases(1)} @{thm sum_case_step(1)},
   2.371 +      right = mk_sum_step @{thm sum.cases(2)} @{thm sum_case_step(2)}, init = refl} n k;
   2.372 +
   2.373 +(* FIXME: because of "@ lhss", the output could contain type variables that are not in the input;
   2.374 +   also, "fp_sort" should put the "resBs" first and in the order in which they appear *)
   2.375 +fun fp_sort lhss NONE Ass = Library.sort (Term_Ord.typ_ord o pairself TFree)
   2.376 +    (subtract (op =) lhss (fold (fold (insert (op =))) Ass [])) @ lhss
   2.377 +  | fp_sort lhss (SOME resBs) Ass =
   2.378 +    (subtract (op =) lhss (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs)) @ lhss;
   2.379 +
   2.380 +fun mk_fp_bnf timer construct resBs bs sort lhss bnfs deadss livess unfold lthy =
   2.381 +  let
   2.382 +    val name = mk_common_name bs;
   2.383 +    fun qualify i =
   2.384 +      let val namei = name ^ nonzero_string_of_int i;
   2.385 +      in Binding.qualify true namei end;
   2.386 +
   2.387 +    val Ass = map (map dest_TFree) livess;
   2.388 +    val resDs = (case resBs of NONE => [] | SOME Ts => fold (subtract (op =)) Ass Ts);
   2.389 +    val Ds = fold (fold Term.add_tfreesT) deadss [];
   2.390 +
   2.391 +    val _ = (case Library.inter (op =) Ds lhss of [] => ()
   2.392 +      | A :: _ => error ("Nonadmissible type recursion (cannot take fixed point of dead type \
   2.393 +        \variable " ^ quote (Syntax.string_of_typ lthy (TFree A)) ^ ")"));
   2.394 +
   2.395 +    val timer = time (timer "Construction of BNFs");
   2.396 +
   2.397 +    val ((kill_poss, _), (bnfs', (unfold', lthy'))) =
   2.398 +      normalize_bnfs qualify Ass Ds sort bnfs unfold lthy;
   2.399 +
   2.400 +    val Dss = map3 (append oo map o nth) livess kill_poss deadss;
   2.401 +
   2.402 +    val ((bnfs'', deadss), lthy'') =
   2.403 +      fold_map3 (seal_bnf unfold') (map (Binding.prefix_name preN) bs) Dss bnfs' lthy'
   2.404 +      |>> split_list;
   2.405 +
   2.406 +    val timer = time (timer "Normalization & sealing of BNFs");
   2.407 +
   2.408 +    val res = construct resBs bs (map TFree resDs, deadss) bnfs'' lthy'';
   2.409 +
   2.410 +    val timer = time (timer "FP construction in total");
   2.411 +  in
   2.412 +    timer; (bnfs'', res)
   2.413 +  end;
   2.414 +
   2.415 +fun fp_bnf construct bs mixfixes resBs eqs lthy =
   2.416 +  let
   2.417 +    val timer = time (Timer.startRealTimer ());
   2.418 +    val (lhss, rhss) = split_list eqs;
   2.419 +    val sort = fp_sort lhss (SOME resBs);
   2.420 +    fun qualify b = Binding.qualify true (Binding.name_of (Binding.prefix_name rawN b));
   2.421 +    val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list)
   2.422 +      (fold_map2 (fn b => bnf_of_typ Smart_Inline (qualify b) sort) bs rhss
   2.423 +        (empty_unfold, lthy));
   2.424 +  in
   2.425 +    mk_fp_bnf timer (construct mixfixes) (SOME resBs) bs sort lhss bnfs Dss Ass unfold lthy'
   2.426 +  end;
   2.427 +
   2.428 +fun fp_bnf_cmd construct (bs, (raw_lhss, raw_bnfs)) lthy =
   2.429 +  let
   2.430 +    val timer = time (Timer.startRealTimer ());
   2.431 +    val lhss = map (dest_TFree o Syntax.read_typ lthy) raw_lhss;
   2.432 +    val sort = fp_sort lhss NONE;
   2.433 +    fun qualify b = Binding.qualify true (Binding.name_of (Binding.prefix_name rawN b));
   2.434 +    val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list)
   2.435 +      (fold_map2 (fn b => fn rawT =>
   2.436 +        (bnf_of_typ Smart_Inline (qualify b) sort (Syntax.read_typ lthy rawT)))
   2.437 +      bs raw_bnfs (empty_unfold, lthy));
   2.438 +  in
   2.439 +    snd (mk_fp_bnf timer (construct (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold lthy')
   2.440 +  end;
   2.441 +
   2.442 +end;
     3.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Thu Sep 20 02:42:48 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Thu Sep 20 02:42:48 2012 +0200
     3.3 @@ -29,7 +29,7 @@
     3.4  open BNF_Util
     3.5  open BNF_Wrap
     3.6  open BNF_Def
     3.7 -open BNF_FP_Util
     3.8 +open BNF_FP
     3.9  open BNF_FP_Sugar_Tactics
    3.10  
    3.11  val simp_attrs = @{attributes [simp]};
     4.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Thu Sep 20 02:42:48 2012 +0200
     4.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Thu Sep 20 02:42:48 2012 +0200
     4.3 @@ -24,7 +24,7 @@
     4.4  
     4.5  open BNF_Tactics
     4.6  open BNF_Util
     4.7 -open BNF_FP_Util
     4.8 +open BNF_FP
     4.9  
    4.10  val meta_mp = @{thm meta_mp};
    4.11  val meta_spec = @{thm meta_spec};
     5.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Thu Sep 20 02:42:48 2012 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,439 +0,0 @@
     5.4 -(*  Title:      HOL/Codatatype/Tools/bnf_fp_util.ML
     5.5 -    Author:     Dmitriy Traytel, TU Muenchen
     5.6 -    Copyright   2012
     5.7 -
     5.8 -Shared library for the datatype and codatatype constructions.
     5.9 -*)
    5.10 -
    5.11 -signature BNF_FP_UTIL =
    5.12 -sig
    5.13 -  val time: Timer.real_timer -> string -> Timer.real_timer
    5.14 -
    5.15 -  val IITN: string
    5.16 -  val LevN: string
    5.17 -  val algN: string
    5.18 -  val behN: string
    5.19 -  val bisN: string
    5.20 -  val carTN: string
    5.21 -  val caseN: string
    5.22 -  val coN: string
    5.23 -  val coinductN: string
    5.24 -  val coiterN: string
    5.25 -  val coitersN: string
    5.26 -  val corecN: string
    5.27 -  val corecsN: string
    5.28 -  val disc_coitersN: string
    5.29 -  val disc_corecsN: string
    5.30 -  val exhaustN: string
    5.31 -  val fldN: string
    5.32 -  val fld_exhaustN: string
    5.33 -  val fld_induct2N: string
    5.34 -  val fld_inductN: string
    5.35 -  val fld_injectN: string
    5.36 -  val fld_iterN: string
    5.37 -  val fld_iter_uniqueN: string
    5.38 -  val fld_itersN: string
    5.39 -  val fld_recN: string
    5.40 -  val fld_recsN: string
    5.41 -  val fld_unfN: string
    5.42 -  val fld_unf_coitersN: string
    5.43 -  val fld_unf_corecsN: string
    5.44 -  val hsetN: string
    5.45 -  val hset_recN: string
    5.46 -  val inductN: string
    5.47 -  val injectN: string
    5.48 -  val isNodeN: string
    5.49 -  val iterN: string
    5.50 -  val itersN: string
    5.51 -  val lsbisN: string
    5.52 -  val map_simpsN: string
    5.53 -  val map_uniqueN: string
    5.54 -  val min_algN: string
    5.55 -  val morN: string
    5.56 -  val nchotomyN: string
    5.57 -  val pred_coinductN: string
    5.58 -  val pred_coinduct_uptoN: string
    5.59 -  val pred_simpN: string
    5.60 -  val recN: string
    5.61 -  val recsN: string
    5.62 -  val rel_coinductN: string
    5.63 -  val rel_coinduct_uptoN: string
    5.64 -  val rel_simpN: string
    5.65 -  val rvN: string
    5.66 -  val sel_coitersN: string
    5.67 -  val sel_corecsN: string
    5.68 -  val set_inclN: string
    5.69 -  val set_set_inclN: string
    5.70 -  val simpsN: string
    5.71 -  val strTN: string
    5.72 -  val str_initN: string
    5.73 -  val sum_bdN: string
    5.74 -  val sum_bdTN: string
    5.75 -  val unfN: string
    5.76 -  val unf_coinductN: string
    5.77 -  val unf_coinduct_uptoN: string
    5.78 -  val unf_coiterN: string
    5.79 -  val unf_coiter_uniqueN: string
    5.80 -  val unf_coitersN: string
    5.81 -  val unf_corecN: string
    5.82 -  val unf_corecsN: string
    5.83 -  val unf_exhaustN: string
    5.84 -  val unf_fldN: string
    5.85 -  val unf_injectN: string
    5.86 -  val uniqueN: string
    5.87 -  val uptoN: string
    5.88 -
    5.89 -  val mk_exhaustN: string -> string
    5.90 -  val mk_injectN: string -> string
    5.91 -  val mk_nchotomyN: string -> string
    5.92 -  val mk_set_simpsN: int -> string
    5.93 -  val mk_set_minimalN: int -> string
    5.94 -  val mk_set_inductN: int -> string
    5.95 -
    5.96 -  val mk_common_name: binding list -> string
    5.97 -
    5.98 -  val split_conj_thm: thm -> thm list
    5.99 -  val split_conj_prems: int -> thm -> thm
   5.100 -
   5.101 -  val retype_free: typ -> term -> term
   5.102 -
   5.103 -  val mk_predT: typ -> typ;
   5.104 -
   5.105 -  val mk_sumTN: typ list -> typ
   5.106 -  val mk_sumTN_balanced: typ list -> typ
   5.107 -
   5.108 -  val id_const: typ -> term
   5.109 -  val id_abs: typ -> term
   5.110 -
   5.111 -  val Inl_const: typ -> typ -> term
   5.112 -  val Inr_const: typ -> typ -> term
   5.113 -
   5.114 -  val mk_Inl: typ -> term -> term
   5.115 -  val mk_Inr: typ -> term -> term
   5.116 -  val mk_InN: typ list -> term -> int -> term
   5.117 -  val mk_InN_balanced: typ -> int -> term -> int -> term
   5.118 -  val mk_sum_case: term * term -> term
   5.119 -  val mk_sum_caseN: term list -> term
   5.120 -  val mk_sum_caseN_balanced: term list -> term
   5.121 -
   5.122 -  val dest_sumT: typ -> typ * typ
   5.123 -  val dest_sumTN: int -> typ -> typ list
   5.124 -  val dest_sumTN_balanced: int -> typ -> typ list
   5.125 -  val dest_tupleT: int -> typ -> typ list
   5.126 -
   5.127 -  val mk_Field: term -> term
   5.128 -  val mk_If: term -> term -> term -> term
   5.129 -  val mk_union: term * term -> term
   5.130 -
   5.131 -  val mk_sumEN: int -> thm
   5.132 -  val mk_sumEN_balanced: int -> thm
   5.133 -  val mk_sumEN_tupled_balanced: int list -> thm
   5.134 -  val mk_sum_casesN: int -> int -> thm
   5.135 -  val mk_sum_casesN_balanced: int -> int -> thm
   5.136 -
   5.137 -  val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
   5.138 -
   5.139 -  val fp_bnf: (mixfix list -> (string * sort) list option -> binding list ->
   5.140 -    typ list * typ list list -> BNF_Def.BNF list -> local_theory -> 'a) ->
   5.141 -    binding list -> mixfix list -> (string * sort) list -> ((string * sort) * typ) list ->
   5.142 -    local_theory -> BNF_Def.BNF list * 'a
   5.143 -  val fp_bnf_cmd: (mixfix list -> (string * sort) list option -> binding list ->
   5.144 -    typ list * typ list list -> BNF_Def.BNF list -> local_theory -> 'a) ->
   5.145 -    binding list * (string list * string list) -> local_theory -> 'a
   5.146 -end;
   5.147 -
   5.148 -structure BNF_FP_Util : BNF_FP_UTIL =
   5.149 -struct
   5.150 -
   5.151 -open BNF_Comp
   5.152 -open BNF_Def
   5.153 -open BNF_Util
   5.154 -
   5.155 -val timing = true;
   5.156 -fun time timer msg = (if timing
   5.157 -  then warning (msg ^ ": " ^ ATP_Util.string_from_time (Timer.checkRealTimer timer))
   5.158 -  else (); Timer.startRealTimer ());
   5.159 -
   5.160 -val preN = "pre_"
   5.161 -val rawN = "raw_"
   5.162 -
   5.163 -val coN = "co"
   5.164 -val algN = "alg"
   5.165 -val IITN = "IITN"
   5.166 -val iterN = "iter"
   5.167 -val itersN = iterN ^ "s"
   5.168 -val coiterN = coN ^ iterN
   5.169 -val coitersN = coiterN ^ "s"
   5.170 -val uniqueN = "_unique"
   5.171 -val simpsN = "simps"
   5.172 -val fldN = "fld"
   5.173 -val unfN = "unf"
   5.174 -val fld_iterN = fldN ^ "_" ^ iterN
   5.175 -val fld_itersN = fld_iterN ^ "s"
   5.176 -val unf_coiterN = unfN ^ "_" ^ coiterN
   5.177 -val unf_coitersN = unf_coiterN ^ "s"
   5.178 -val fld_iter_uniqueN = fld_iterN ^ uniqueN
   5.179 -val unf_coiter_uniqueN = unf_coiterN ^ uniqueN
   5.180 -val fld_unf_coitersN = fldN ^ "_" ^ unf_coiterN ^ "s"
   5.181 -val map_simpsN = mapN ^ "_" ^ simpsN
   5.182 -val map_uniqueN = mapN ^ uniqueN
   5.183 -val min_algN = "min_alg"
   5.184 -val morN = "mor"
   5.185 -val bisN = "bis"
   5.186 -val lsbisN = "lsbis"
   5.187 -val sum_bdTN = "sbdT"
   5.188 -val sum_bdN = "sbd"
   5.189 -val carTN = "carT"
   5.190 -val strTN = "strT"
   5.191 -val isNodeN = "isNode"
   5.192 -val LevN = "Lev"
   5.193 -val rvN = "recover"
   5.194 -val behN = "beh"
   5.195 -fun mk_set_simpsN i = mk_setN i ^ "_" ^ simpsN
   5.196 -fun mk_set_minimalN i = mk_setN i ^ "_minimal"
   5.197 -fun mk_set_inductN i = mk_setN i ^ "_induct"
   5.198 -
   5.199 -val str_initN = "str_init"
   5.200 -val recN = "rec"
   5.201 -val recsN = recN ^ "s"
   5.202 -val corecN = coN ^ recN
   5.203 -val corecsN = corecN ^ "s"
   5.204 -val fld_recN = fldN ^ "_" ^ recN
   5.205 -val fld_recsN = fld_recN ^ "s"
   5.206 -val unf_corecN = unfN ^ "_" ^ corecN
   5.207 -val unf_corecsN = unf_corecN ^ "s"
   5.208 -val fld_unf_corecsN = fldN ^ "_" ^ unf_corecN ^ "s"
   5.209 -
   5.210 -val fld_unfN = fldN ^ "_" ^ unfN
   5.211 -val unf_fldN = unfN ^ "_" ^ fldN
   5.212 -val nchotomyN = "nchotomy"
   5.213 -fun mk_nchotomyN s = s ^ "_" ^ nchotomyN
   5.214 -val injectN = "inject"
   5.215 -fun mk_injectN s = s ^ "_" ^ injectN
   5.216 -val exhaustN = "exhaust"
   5.217 -fun mk_exhaustN s = s ^ "_" ^ exhaustN
   5.218 -val fld_injectN = mk_injectN fldN
   5.219 -val fld_exhaustN = mk_exhaustN fldN
   5.220 -val unf_injectN = mk_injectN unfN
   5.221 -val unf_exhaustN = mk_exhaustN unfN
   5.222 -val inductN = "induct"
   5.223 -val coinductN = coN ^ inductN
   5.224 -val fld_inductN = fldN ^ "_" ^ inductN
   5.225 -val fld_induct2N = fld_inductN ^ "2"
   5.226 -val unf_coinductN = unfN ^ "_" ^ coinductN
   5.227 -val rel_coinductN = relN ^ "_" ^ coinductN
   5.228 -val pred_coinductN = predN ^ "_" ^ coinductN
   5.229 -val simpN = "_simp";
   5.230 -val rel_simpN = relN ^ simpN;
   5.231 -val pred_simpN = predN ^ simpN;
   5.232 -val uptoN = "upto"
   5.233 -val unf_coinduct_uptoN = unf_coinductN ^ "_" ^ uptoN
   5.234 -val rel_coinduct_uptoN = rel_coinductN ^ "_" ^ uptoN
   5.235 -val pred_coinduct_uptoN = pred_coinductN ^ "_" ^ uptoN
   5.236 -val hsetN = "Hset"
   5.237 -val hset_recN = hsetN ^ "_rec"
   5.238 -val set_inclN = "set_incl"
   5.239 -val set_set_inclN = "set_set_incl"
   5.240 -
   5.241 -val caseN = "case"
   5.242 -val discN = "disc"
   5.243 -val disc_coitersN = discN ^ "_" ^ coitersN
   5.244 -val disc_corecsN = discN ^ "_" ^ corecsN
   5.245 -val selN = "sel"
   5.246 -val sel_coitersN = selN ^ "_" ^ coitersN
   5.247 -val sel_corecsN = selN ^ "_" ^ corecsN
   5.248 -
   5.249 -val mk_common_name = space_implode "_" o map Binding.name_of;
   5.250 -
   5.251 -fun mk_predT T = T --> HOLogic.boolT;
   5.252 -
   5.253 -fun retype_free T (Free (s, _)) = Free (s, T);
   5.254 -
   5.255 -fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T');
   5.256 -
   5.257 -fun dest_sumTN 1 T = [T]
   5.258 -  | dest_sumTN n (Type (@{type_name sum}, [T, T'])) = T :: dest_sumTN (n - 1) T';
   5.259 -
   5.260 -val dest_sumTN_balanced = Balanced_Tree.dest dest_sumT;
   5.261 -
   5.262 -(* TODO: move something like this to "HOLogic"? *)
   5.263 -fun dest_tupleT 0 @{typ unit} = []
   5.264 -  | dest_tupleT 1 T = [T]
   5.265 -  | dest_tupleT n (Type (@{type_name prod}, [T, T'])) = T :: dest_tupleT (n - 1) T';
   5.266 -
   5.267 -val mk_sumTN = Library.foldr1 mk_sumT;
   5.268 -val mk_sumTN_balanced = Balanced_Tree.make mk_sumT;
   5.269 -
   5.270 -fun id_const T = Const (@{const_name id}, T --> T);
   5.271 -fun id_abs T = Abs (Name.uu, T, Bound 0);
   5.272 -
   5.273 -fun Inl_const LT RT = Const (@{const_name Inl}, LT --> mk_sumT (LT, RT));
   5.274 -fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t;
   5.275 -
   5.276 -fun Inr_const LT RT = Const (@{const_name Inr}, RT --> mk_sumT (LT, RT));
   5.277 -fun mk_Inr LT t = Inr_const LT (fastype_of t) $ t;
   5.278 -
   5.279 -fun mk_InN [_] t 1 = t
   5.280 -  | mk_InN (_ :: Ts) t 1 = mk_Inl (mk_sumTN Ts) t
   5.281 -  | mk_InN (LT :: Ts) t m = mk_Inr LT (mk_InN Ts t (m - 1))
   5.282 -  | mk_InN Ts t _ = raise (TYPE ("mk_InN", Ts, [t]));
   5.283 -
   5.284 -fun mk_InN_balanced sum_T n t k =
   5.285 -  let
   5.286 -    fun repair_types T (Const (s as @{const_name Inl}, _) $ t) = repair_inj_types T s fst t
   5.287 -      | repair_types T (Const (s as @{const_name Inr}, _) $ t) = repair_inj_types T s snd t
   5.288 -      | repair_types _ t = t
   5.289 -    and repair_inj_types T s get t =
   5.290 -      let val T' = get (dest_sumT T) in
   5.291 -        Const (s, T' --> T) $ repair_types T' t
   5.292 -      end;
   5.293 -  in
   5.294 -    Balanced_Tree.access {left = mk_Inl dummyT, right = mk_Inr dummyT, init = t} n k
   5.295 -    |> repair_types sum_T
   5.296 -  end;
   5.297 -
   5.298 -fun mk_sum_case (f, g) =
   5.299 -  let
   5.300 -    val fT = fastype_of f;
   5.301 -    val gT = fastype_of g;
   5.302 -  in
   5.303 -    Const (@{const_name sum_case},
   5.304 -      fT --> gT --> mk_sumT (domain_type fT, domain_type gT) --> range_type fT) $ f $ g
   5.305 -  end;
   5.306 -
   5.307 -val mk_sum_caseN = Library.foldr1 mk_sum_case;
   5.308 -val mk_sum_caseN_balanced = Balanced_Tree.make mk_sum_case;
   5.309 -
   5.310 -fun mk_If p t f =
   5.311 -  let val T = fastype_of t;
   5.312 -  in Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ p $ t $ f end;
   5.313 -
   5.314 -fun mk_Field r =
   5.315 -  let val T = fst (dest_relT (fastype_of r));
   5.316 -  in Const (@{const_name Field}, mk_relT (T, T) --> HOLogic.mk_setT T) $ r end;
   5.317 -
   5.318 -val mk_union = HOLogic.mk_binop @{const_name sup};
   5.319 -
   5.320 -(*dangerous; use with monotonic, converging functions only!*)
   5.321 -fun fixpoint eq f X = if subset eq (f X, X) then X else fixpoint eq f (f X);
   5.322 -
   5.323 -(* stolen from "~~/src/HOL/Tools/Datatype/datatype_aux.ML" *)
   5.324 -fun split_conj_thm th =
   5.325 -  ((th RS conjunct1) :: split_conj_thm (th RS conjunct2)) handle THM _ => [th];
   5.326 -
   5.327 -fun split_conj_prems limit th =
   5.328 -  let
   5.329 -    fun split n i th =
   5.330 -      if i = n then th else split n (i + 1) (conjI RSN (i, th)) handle THM _ => th;
   5.331 -  in split limit 1 th end;
   5.332 -
   5.333 -fun mk_sumEN 1 = @{thm one_pointE}
   5.334 -  | mk_sumEN 2 = @{thm sumE}
   5.335 -  | mk_sumEN n =
   5.336 -    (fold (fn i => fn thm => @{thm obj_sum_step} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF
   5.337 -      replicate n (impI RS allI);
   5.338 -
   5.339 -fun mk_obj_sumEN_balanced n =
   5.340 -  Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f})))
   5.341 -    (replicate n asm_rl);
   5.342 -
   5.343 -fun mk_sumEN_balanced' n all_impIs = mk_obj_sumEN_balanced n OF all_impIs RS @{thm obj_one_pointE};
   5.344 -
   5.345 -fun mk_sumEN_balanced 1 = @{thm one_pointE} (*optimization*)
   5.346 -  | mk_sumEN_balanced 2 = @{thm sumE} (*optimization*)
   5.347 -  | mk_sumEN_balanced n = mk_sumEN_balanced' n (replicate n (impI RS allI));
   5.348 -
   5.349 -fun mk_tupled_allIN 0 = @{thm unit_all_impI}
   5.350 -  | mk_tupled_allIN 1 = @{thm impI[THEN allI]}
   5.351 -  | mk_tupled_allIN 2 = @{thm prod_all_impI} (*optimization*)
   5.352 -  | mk_tupled_allIN n = mk_tupled_allIN (n - 1) RS @{thm prod_all_impI_step};
   5.353 -
   5.354 -fun mk_sumEN_tupled_balanced ms =
   5.355 -  let val n = length ms in
   5.356 -    if forall (curry (op =) 1) ms then mk_sumEN_balanced n
   5.357 -    else mk_sumEN_balanced' n (map mk_tupled_allIN ms)
   5.358 -  end;
   5.359 -
   5.360 -fun mk_sum_casesN 1 1 = refl
   5.361 -  | mk_sum_casesN _ 1 = @{thm sum.cases(1)}
   5.362 -  | mk_sum_casesN 2 2 = @{thm sum.cases(2)}
   5.363 -  | mk_sum_casesN n k = trans OF [@{thm sum_case_step(2)}, mk_sum_casesN (n - 1) (k - 1)];
   5.364 -
   5.365 -fun mk_sum_step base step thm =
   5.366 -  if Thm.eq_thm_prop (thm, refl) then base else trans OF [step, thm];
   5.367 -
   5.368 -fun mk_sum_casesN_balanced 1 1 = refl
   5.369 -  | mk_sum_casesN_balanced n k =
   5.370 -    Balanced_Tree.access {left = mk_sum_step @{thm sum.cases(1)} @{thm sum_case_step(1)},
   5.371 -      right = mk_sum_step @{thm sum.cases(2)} @{thm sum_case_step(2)}, init = refl} n k;
   5.372 -
   5.373 -(* FIXME: because of "@ lhss", the output could contain type variables that are not in the input;
   5.374 -   also, "fp_sort" should put the "resBs" first and in the order in which they appear *)
   5.375 -fun fp_sort lhss NONE Ass = Library.sort (Term_Ord.typ_ord o pairself TFree)
   5.376 -    (subtract (op =) lhss (fold (fold (insert (op =))) Ass [])) @ lhss
   5.377 -  | fp_sort lhss (SOME resBs) Ass =
   5.378 -    (subtract (op =) lhss (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs)) @ lhss;
   5.379 -
   5.380 -fun mk_fp_bnf timer construct resBs bs sort lhss bnfs deadss livess unfold lthy =
   5.381 -  let
   5.382 -    val name = mk_common_name bs;
   5.383 -    fun qualify i =
   5.384 -      let val namei = name ^ nonzero_string_of_int i;
   5.385 -      in Binding.qualify true namei end;
   5.386 -
   5.387 -    val Ass = map (map dest_TFree) livess;
   5.388 -    val resDs = (case resBs of NONE => [] | SOME Ts => fold (subtract (op =)) Ass Ts);
   5.389 -    val Ds = fold (fold Term.add_tfreesT) deadss [];
   5.390 -
   5.391 -    val _ = (case Library.inter (op =) Ds lhss of [] => ()
   5.392 -      | A :: _ => error ("Nonadmissible type recursion (cannot take fixed point of dead type \
   5.393 -        \variable " ^ quote (Syntax.string_of_typ lthy (TFree A)) ^ ")"));
   5.394 -
   5.395 -    val timer = time (timer "Construction of BNFs");
   5.396 -
   5.397 -    val ((kill_poss, _), (bnfs', (unfold', lthy'))) =
   5.398 -      normalize_bnfs qualify Ass Ds sort bnfs unfold lthy;
   5.399 -
   5.400 -    val Dss = map3 (append oo map o nth) livess kill_poss deadss;
   5.401 -
   5.402 -    val ((bnfs'', deadss), lthy'') =
   5.403 -      fold_map3 (seal_bnf unfold') (map (Binding.prefix_name preN) bs) Dss bnfs' lthy'
   5.404 -      |>> split_list;
   5.405 -
   5.406 -    val timer = time (timer "Normalization & sealing of BNFs");
   5.407 -
   5.408 -    val res = construct resBs bs (map TFree resDs, deadss) bnfs'' lthy'';
   5.409 -
   5.410 -    val timer = time (timer "FP construction in total");
   5.411 -  in
   5.412 -    timer; (bnfs'', res)
   5.413 -  end;
   5.414 -
   5.415 -fun fp_bnf construct bs mixfixes resBs eqs lthy =
   5.416 -  let
   5.417 -    val timer = time (Timer.startRealTimer ());
   5.418 -    val (lhss, rhss) = split_list eqs;
   5.419 -    val sort = fp_sort lhss (SOME resBs);
   5.420 -    fun qualify b = Binding.qualify true (Binding.name_of (Binding.prefix_name rawN b));
   5.421 -    val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list)
   5.422 -      (fold_map2 (fn b => bnf_of_typ Smart_Inline (qualify b) sort) bs rhss
   5.423 -        (empty_unfold, lthy));
   5.424 -  in
   5.425 -    mk_fp_bnf timer (construct mixfixes) (SOME resBs) bs sort lhss bnfs Dss Ass unfold lthy'
   5.426 -  end;
   5.427 -
   5.428 -fun fp_bnf_cmd construct (bs, (raw_lhss, raw_bnfs)) lthy =
   5.429 -  let
   5.430 -    val timer = time (Timer.startRealTimer ());
   5.431 -    val lhss = map (dest_TFree o Syntax.read_typ lthy) raw_lhss;
   5.432 -    val sort = fp_sort lhss NONE;
   5.433 -    fun qualify b = Binding.qualify true (Binding.name_of (Binding.prefix_name rawN b));
   5.434 -    val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list)
   5.435 -      (fold_map2 (fn b => fn rawT =>
   5.436 -        (bnf_of_typ Smart_Inline (qualify b) sort (Syntax.read_typ lthy rawT)))
   5.437 -      bs raw_bnfs (empty_unfold, lthy));
   5.438 -  in
   5.439 -    snd (mk_fp_bnf timer (construct (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold lthy')
   5.440 -  end;
   5.441 -
   5.442 -end;
     6.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Thu Sep 20 02:42:48 2012 +0200
     6.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Thu Sep 20 02:42:48 2012 +0200
     6.3 @@ -21,7 +21,7 @@
     6.4  open BNF_Def
     6.5  open BNF_Util
     6.6  open BNF_Tactics
     6.7 -open BNF_FP_Util
     6.8 +open BNF_FP
     6.9  open BNF_FP_Sugar
    6.10  open BNF_GFP_Util
    6.11  open BNF_GFP_Tactics
     7.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Thu Sep 20 02:42:48 2012 +0200
     7.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Thu Sep 20 02:42:48 2012 +0200
     7.3 @@ -126,7 +126,7 @@
     7.4  
     7.5  open BNF_Tactics
     7.6  open BNF_Util
     7.7 -open BNF_FP_Util
     7.8 +open BNF_FP
     7.9  open BNF_GFP_Util
    7.10  
    7.11  val Pair_eq_subst_id = @{thm Pair_eq[THEN subst, of "%x. x"]};
     8.1 --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Thu Sep 20 02:42:48 2012 +0200
     8.2 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Thu Sep 20 02:42:48 2012 +0200
     8.3 @@ -20,7 +20,7 @@
     8.4  open BNF_Def
     8.5  open BNF_Util
     8.6  open BNF_Tactics
     8.7 -open BNF_FP_Util
     8.8 +open BNF_FP
     8.9  open BNF_FP_Sugar
    8.10  open BNF_LFP_Util
    8.11  open BNF_LFP_Tactics