src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
changeset 55575 a5e33e18fb5c
parent 55573 6a1cbddebf86
child 55699 1f9cc432ecd4
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 19 08:34:32 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 19 08:34:33 2014 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  sig
     1.5    type fp_sugar =
     1.6      {T: typ,
     1.7 -     fp: BNF_FP_Util.fp_kind,
     1.8 +     fp: BNF_Util.fp_kind,
     1.9       fp_res_index: int,
    1.10       fp_res: BNF_FP_Util.fp_result,
    1.11       pre_bnf: BNF_Def.bnf,
    1.12 @@ -53,7 +53,7 @@
    1.13    val morph_gfp_sugar_thms: morphism -> gfp_sugar_thms -> gfp_sugar_thms
    1.14    val transfer_gfp_sugar_thms: Proof.context -> gfp_sugar_thms -> gfp_sugar_thms
    1.15  
    1.16 -  val mk_co_iters_prelims: BNF_FP_Util.fp_kind -> typ list list list -> typ list -> typ list ->
    1.17 +  val mk_co_iters_prelims: BNF_Util.fp_kind -> typ list list list -> typ list -> typ list ->
    1.18      int list -> int list list -> term list list -> Proof.context ->
    1.19      (term list list
    1.20       * (typ list list * typ list list list list * term list list
    1.21 @@ -89,12 +89,12 @@
    1.22      ((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix)
    1.23      * ((binding, binding * typ, term) Ctr_Sugar.ctr_spec * mixfix) list
    1.24  
    1.25 -  val co_datatypes: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
    1.26 +  val co_datatypes: BNF_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
    1.27        binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
    1.28        BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) ->
    1.29      (bool * bool) * co_datatype_spec list ->
    1.30      local_theory -> local_theory
    1.31 -  val parse_co_datatype_cmd: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
    1.32 +  val parse_co_datatype_cmd: BNF_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
    1.33        binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
    1.34        BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) ->
    1.35      (local_theory -> local_theory) parser
    1.36 @@ -259,6 +259,11 @@
    1.37      map (Term.subst_TVars rho) ts0
    1.38    end;
    1.39  
    1.40 +
    1.41 +fun unzip_recT (Type (@{type_name prod}, _)) T = [T]
    1.42 +  | unzip_recT _ (Type (@{type_name prod}, Ts)) = Ts
    1.43 +  | unzip_recT _ T = [T];
    1.44 +
    1.45  fun unzip_corecT (Type (@{type_name sum}, _)) T = [T]
    1.46    | unzip_corecT _ (Type (@{type_name sum}, Ts)) = Ts
    1.47    | unzip_corecT _ T = [T];
    1.48 @@ -339,6 +344,8 @@
    1.49  val transfer_gfp_sugar_thms =
    1.50    morph_gfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
    1.51  
    1.52 +fun mk_iter_fun_arg_types n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type;
    1.53 +
    1.54  fun mk_iters_args_types ctr_Tsss Cs ns mss ctor_iter_fun_Tss lthy =
    1.55    let
    1.56      val Css = map2 replicate ns Cs;