src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 52872 fd14b0ead643
parent 52871 94ab1f8151e2
child 52898 2af1caada147
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Aug 06 15:50:23 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Aug 06 15:50:23 2013 +0200
     1.3 @@ -42,8 +42,10 @@
     1.4          * ((term list list * term list list list) * (typ list * typ list list)) list) option)
     1.5      * Proof.context
     1.6  
     1.7 -  val mk_iter_fun_arg_typessss: typ list -> int list -> int list list -> term ->
     1.8 +  val mk_iter_fun_arg_types: typ list -> int list -> int list list -> term ->
     1.9      typ list list list list
    1.10 +  val mk_coiter_fun_arg_types: typ list -> int list -> int list list -> term ->
    1.11 +    typ list list list list * typ list list list * typ list list list list * typ list
    1.12    val define_iters: string list ->
    1.13      (typ list list * typ list list list list * term list list * term list list list list) list ->
    1.14      (string -> binding) -> typ list -> typ list -> term list -> Proof.context ->
    1.15 @@ -327,17 +329,17 @@
    1.16  
    1.17  fun indexify proj xs f p = f (find_index (curry (op =) (proj p)) xs) p;
    1.18  
    1.19 -fun mk_fun_arg_typess n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type;
    1.20 +fun mk_iter_fun_arg_types0 n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type;
    1.21  
    1.22 -fun mk_iter_fun_arg_typessss Cs ns mss =
    1.23 +fun mk_iter_fun_arg_types Cs ns mss =
    1.24    mk_fp_iter_fun_types
    1.25 -  #> map3 mk_fun_arg_typess ns mss
    1.26 +  #> map3 mk_iter_fun_arg_types0 ns mss
    1.27    #> map (map (map (unzip_recT Cs)));
    1.28  
    1.29  fun mk_iters_args_types Cs ns mss ctor_iter_fun_Tss lthy =
    1.30    let
    1.31      val Css = map2 replicate ns Cs;
    1.32 -    val y_Tsss = map3 mk_fun_arg_typess ns mss (map un_fold_of ctor_iter_fun_Tss);
    1.33 +    val y_Tsss = map3 mk_iter_fun_arg_types0 ns mss (map un_fold_of ctor_iter_fun_Tss);
    1.34      val g_Tss = map2 (fn C => map (fn y_Ts => y_Ts ---> C)) Cs y_Tsss;
    1.35  
    1.36      val ((gss, ysss), lthy) =
    1.37 @@ -365,7 +367,7 @@
    1.38      ([(g_Tss, y_Tssss, gss, yssss), (h_Tss, z_Tssss, hss, zssss)], lthy)
    1.39    end;
    1.40  
    1.41 -fun mk_coiter_fun_arg_typessss_typesss_typessss Cs ns mss fun_Ts =
    1.42 +fun mk_coiter_fun_arg_types0 Cs ns mss fun_Ts =
    1.43    let
    1.44      (*avoid "'a itself" arguments in coiterators and corecursors*)
    1.45      fun repair_arity [0] = [1]
    1.46 @@ -380,6 +382,10 @@
    1.47      (q_Tssss, f_Tsss, f_Tssss, f_sum_prod_Ts)
    1.48    end;
    1.49  
    1.50 +fun mk_coiter_fun_arg_types Cs ns mss =
    1.51 +  mk_fp_iter_fun_types
    1.52 +  #> mk_coiter_fun_arg_types0 Cs ns mss;
    1.53 +
    1.54  fun mk_coiters_args_types Cs ns mss dtor_coiter_fun_Tss lthy =
    1.55    let
    1.56      val p_Tss = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_pred1T) ns Cs;
    1.57 @@ -387,8 +393,7 @@
    1.58      fun mk_types get_Ts =
    1.59        let
    1.60          val fun_Ts = map get_Ts dtor_coiter_fun_Tss;
    1.61 -        val (q_Tssss, f_Tsss, f_Tssss, f_sum_prod_Ts) =
    1.62 -          mk_coiter_fun_arg_typessss_typesss_typessss Cs ns mss fun_Ts;
    1.63 +        val (q_Tssss, f_Tsss, f_Tssss, f_sum_prod_Ts) = mk_coiter_fun_arg_types0 Cs ns mss fun_Ts;
    1.64          val pf_Tss = map3 flat_corec_preds_predsss_gettersss p_Tss q_Tssss f_Tssss;
    1.65        in
    1.66          (q_Tssss, f_Tsss, f_Tssss, (f_sum_prod_Ts, pf_Tss))