src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 52871 94ab1f8151e2
parent 52870 47b1c2f3ff24
child 52872 fd14b0ead643
     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 @@ -250,6 +250,10 @@
     1.4      if member (op =) Cs U then Ts else [T]
     1.5    | unzip_recT _ T = [T];
     1.6  
     1.7 +fun unzip_corecT Cs (T as Type (@{type_name sum}, Ts as [_, U])) =
     1.8 +    if member (op =) Cs U then Ts else [T]
     1.9 +  | unzip_corecT _ T = [T];
    1.10 +
    1.11  fun mk_map live Ts Us t =
    1.12    let val (Type (_, Ts0), Type (_, Us0)) = strip_typeN (live + 1) (fastype_of t) |>> List.last in
    1.13      Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
    1.14 @@ -361,11 +365,7 @@
    1.15      ([(g_Tss, y_Tssss, gss, yssss), (h_Tss, z_Tssss, hss, zssss)], lthy)
    1.16    end;
    1.17  
    1.18 -fun unzip_corecT Cs (T as Type (@{type_name sum}, Ts as [_, U])) =
    1.19 -    if member (op =) Cs U then Ts else [T]
    1.20 -  | unzip_corecT _ T = [T];
    1.21 -
    1.22 -fun mk_coiter_fun_arg_typessss_typesss_typessss Cs ns mss maybe_unzipT fun_Ts =
    1.23 +fun mk_coiter_fun_arg_typessss_typesss_typessss Cs ns mss fun_Ts =
    1.24    let
    1.25      (*avoid "'a itself" arguments in coiterators and corecursors*)
    1.26      fun repair_arity [0] = [1]
    1.27 @@ -374,9 +374,8 @@
    1.28      val f_sum_prod_Ts = map range_type fun_Ts;
    1.29      val f_prod_Tss = map2 dest_sumTN_balanced ns f_sum_prod_Ts;
    1.30      val f_Tsss = map2 (map2 dest_tupleT o repair_arity) mss f_prod_Tss;
    1.31 -    val f_Tssss = map2 (fn C => map (map (map (curry (op -->) C) o maybe_unzipT))) Cs f_Tsss;
    1.32 -    val q_Tssss =
    1.33 -      map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) f_Tssss;
    1.34 +    val f_Tssss = map2 (fn C => map (map (map (curry (op -->) C) o unzip_corecT Cs))) Cs f_Tsss;
    1.35 +    val q_Tssss = map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) f_Tssss;
    1.36    in
    1.37      (q_Tssss, f_Tsss, f_Tssss, f_sum_prod_Ts)
    1.38    end;
    1.39 @@ -385,18 +384,18 @@
    1.40    let
    1.41      val p_Tss = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_pred1T) ns Cs;
    1.42  
    1.43 -    fun mk_types maybe_unzipT get_Ts =
    1.44 +    fun mk_types get_Ts =
    1.45        let
    1.46          val fun_Ts = map get_Ts dtor_coiter_fun_Tss;
    1.47          val (q_Tssss, f_Tsss, f_Tssss, f_sum_prod_Ts) =
    1.48 -          mk_coiter_fun_arg_typessss_typesss_typessss Cs ns mss maybe_unzipT fun_Ts;
    1.49 +          mk_coiter_fun_arg_typessss_typesss_typessss Cs ns mss fun_Ts;
    1.50          val pf_Tss = map3 flat_corec_preds_predsss_gettersss p_Tss q_Tssss f_Tssss;
    1.51        in
    1.52          (q_Tssss, f_Tsss, f_Tssss, (f_sum_prod_Ts, pf_Tss))
    1.53        end;
    1.54  
    1.55 -    val (r_Tssss, g_Tsss, g_Tssss, unfold_types) = mk_types single un_fold_of;
    1.56 -    val (s_Tssss, h_Tsss, h_Tssss, corec_types) = mk_types (unzip_corecT Cs) co_rec_of;
    1.57 +    val (r_Tssss, g_Tsss, g_Tssss, unfold_types) = mk_types un_fold_of;
    1.58 +    val (s_Tssss, h_Tsss, h_Tssss, corec_types) = mk_types co_rec_of;
    1.59  
    1.60      val ((((Free (z, _), cs), pss), gssss), lthy) =
    1.61        lthy