merged

--- a/src/HOL/BNF/Examples/Misc_Codatatype.thy	Thu Sep 12 18:09:17 2013 -0700
+++ b/src/HOL/BNF/Examples/Misc_Codatatype.thy	Thu Sep 12 18:09:56 2013 -0700
@@ -43,6 +43,8 @@
   ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2
 *)
 
+codatatype 'a p = P "'a + 'a p"
+
 codatatype 'a J1 = J11 'a "'a J1" | J12 'a "'a J2"
 and 'a J2 = J21 | J22 "'a J1" "'a J2"
 

--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Sep 12 18:09:17 2013 -0700
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Sep 12 18:09:56 2013 -0700
@@ -44,8 +44,8 @@
   val build_rel: local_theory -> (typ * typ -> term) -> typ * typ -> term
   val dest_map: Proof.context -> string -> term -> term * term list
   val dest_ctr: Proof.context -> string -> term -> term * term list
-  val mk_co_iters_prelims: BNF_FP_Util.fp_kind -> typ list -> typ list -> int list ->
-    int list list -> term list list -> Proof.context ->
+  val mk_co_iters_prelims: BNF_FP_Util.fp_kind -> typ list list list -> typ list -> typ list ->
+    int list -> int list list -> term list list -> Proof.context ->
     (term list list
      * (typ list list * typ list list list list * term list list
         * term list list list list) list option
@@ -53,9 +53,9 @@
         * ((term list list * term list list list) * (typ list * typ list list)) list) option)
     * Proof.context
 
-  val mk_iter_fun_arg_types: typ list -> int list -> int list list -> term ->
+  val mk_iter_fun_arg_types: typ list list list -> int list -> int list list -> term ->
     typ list list list list
-  val mk_coiter_fun_arg_types: typ list -> int list -> int list list -> term ->
+  val mk_coiter_fun_arg_types: typ list list list -> typ list -> int list -> term ->
     typ list list
     * (typ list list list list * typ list list list * typ list list list list * typ list)
   val define_iters: string list ->
@@ -268,12 +268,12 @@
 
 val mk_fp_iter_fun_types = binder_fun_types o fastype_of;
 
-fun unzip_recT Cs (T as Type (@{type_name prod}, Ts as [_, U])) =
-    if member (op =) Cs U then Ts else [T]
+fun unzip_recT (Type (@{type_name prod}, _)) T = [T]
+  | unzip_recT _ (T as Type (@{type_name prod}, Ts)) = Ts
   | unzip_recT _ T = [T];
 
-fun unzip_corecT Cs (T as Type (@{type_name sum}, Ts as [_, U])) =
-    if member (op =) Cs U then Ts else [T]
+fun unzip_corecT (Type (@{type_name sum}, _)) T = [T]
+  | unzip_corecT _ (T as Type (@{type_name sum}, Ts)) = Ts
   | unzip_corecT _ T = [T];
 
 fun mk_map live Ts Us t =
@@ -398,12 +398,12 @@
 
 fun mk_iter_fun_arg_types0 n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type;
 
-fun mk_iter_fun_arg_types Cs ns mss =
+fun mk_iter_fun_arg_types ctr_Tsss ns mss =
   mk_fp_iter_fun_types
   #> map3 mk_iter_fun_arg_types0 ns mss
-  #> map (map (map (unzip_recT Cs)));
+  #> map2 (map2 (map2 unzip_recT)) ctr_Tsss;
 
-fun mk_iters_args_types Cs ns mss ctor_iter_fun_Tss lthy =
+fun mk_iters_args_types ctr_Tsss Cs ns mss ctor_iter_fun_Tss lthy =
   let
     val Css = map2 replicate ns Cs;
     val y_Tsss = map3 mk_iter_fun_arg_types0 ns mss (map un_fold_of ctor_iter_fun_Tss);
@@ -418,8 +418,11 @@
     val yssss = map (map (map single)) ysss;
 
     val z_Tssss =
-      map3 (fn n => fn ms => map2 (map (unzip_recT Cs) oo dest_tupleT) ms o
-        dest_sumTN_balanced n o domain_type o co_rec_of) ns mss ctor_iter_fun_Tss;
+      map4 (fn n => fn ms => fn ctr_Tss => fn ctor_iter_fun_Ts =>
+          map3 (fn m => fn ctr_Ts => fn ctor_iter_fun_T =>
+              map2 unzip_recT ctr_Ts (dest_tupleT m ctor_iter_fun_T))
+            ms ctr_Tss (dest_sumTN_balanced n (domain_type (co_rec_of ctor_iter_fun_Ts))))
+        ns mss ctr_Tsss ctor_iter_fun_Tss;
 
     val z_Tsss' = map (map flat_rec_arg_args) z_Tssss;
     val h_Tss = map2 (map2 (curry op --->)) z_Tsss' Css;
@@ -434,16 +437,18 @@
     ([(g_Tss, y_Tssss, gss, yssss), (h_Tss, z_Tssss, hss, zssss)], lthy)
   end;
 
-fun mk_coiter_fun_arg_types0 Cs ns mss fun_Ts =
+fun mk_coiter_fun_arg_types0 ctr_Tsss Cs ns fun_Ts =
   let
-    (*avoid "'a itself" arguments in coiterators and corecursors*)
-    fun repair_arity [0] = [1]
-      | repair_arity ms = ms;
+    (*avoid "'a itself" arguments in coiterators*)
+    fun repair_arity [[]] = [[@{typ unit}]]
+      | repair_arity Tss = Tss;
 
+    val ctr_Tsss' = map repair_arity ctr_Tsss;
     val f_sum_prod_Ts = map range_type fun_Ts;
     val f_prod_Tss = map2 dest_sumTN_balanced ns f_sum_prod_Ts;
-    val f_Tsss = map2 (map2 dest_tupleT o repair_arity) mss f_prod_Tss;
-    val f_Tssss = map2 (fn C => map (map (map (curry op --> C) o unzip_corecT Cs))) Cs f_Tsss;
+    val f_Tsss = map2 (map2 (dest_tupleT o length)) ctr_Tsss' f_prod_Tss;
+    val f_Tssss = map3 (fn C => map2 (map2 (map (curry op --> C) oo unzip_corecT)))
+      Cs ctr_Tsss' f_Tsss;
     val q_Tssss = map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) f_Tssss;
   in
     (q_Tssss, f_Tsss, f_Tssss, f_sum_prod_Ts)
@@ -451,18 +456,18 @@
 
 fun mk_coiter_p_pred_types Cs ns = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_pred1T) ns Cs;
 
-fun mk_coiter_fun_arg_types Cs ns mss dtor_coiter =
+fun mk_coiter_fun_arg_types ctr_Tsss Cs ns dtor_coiter =
   (mk_coiter_p_pred_types Cs ns,
-   mk_fp_iter_fun_types dtor_coiter |> mk_coiter_fun_arg_types0 Cs ns mss);
+   mk_fp_iter_fun_types dtor_coiter |> mk_coiter_fun_arg_types0 ctr_Tsss Cs ns);
 
-fun mk_coiters_args_types Cs ns mss dtor_coiter_fun_Tss lthy =
+fun mk_coiters_args_types ctr_Tsss Cs ns mss dtor_coiter_fun_Tss lthy =
   let
     val p_Tss = mk_coiter_p_pred_types Cs ns;
 
     fun mk_types get_Ts =
       let
         val fun_Ts = map get_Ts dtor_coiter_fun_Tss;
-        val (q_Tssss, f_Tsss, f_Tssss, f_sum_prod_Ts) = mk_coiter_fun_arg_types0 Cs ns mss fun_Ts;
+        val (q_Tssss, f_Tsss, f_Tssss, f_sum_prod_Ts) = mk_coiter_fun_arg_types0 ctr_Tsss Cs ns fun_Ts;
         val pf_Tss = map3 flat_corec_preds_predsss_gettersss p_Tss q_Tssss f_Tssss;
       in
         (q_Tssss, f_Tsss, f_Tssss, (f_sum_prod_Ts, pf_Tss))
@@ -509,7 +514,7 @@
     ((z, cs, cpss, [(unfold_args, unfold_types), (corec_args, corec_types)]), lthy)
   end;
 
-fun mk_co_iters_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy =
+fun mk_co_iters_prelims fp ctr_Tsss fpTs Cs ns mss xtor_co_iterss0 lthy =
   let
     val thy = Proof_Context.theory_of lthy;
 
@@ -519,9 +524,9 @@
 
     val ((iters_args_types, coiters_args_types), lthy') =
       if fp = Least_FP then
-        mk_iters_args_types Cs ns mss xtor_co_iter_fun_Tss lthy |>> (rpair NONE o SOME)
+        mk_iters_args_types ctr_Tsss Cs ns mss xtor_co_iter_fun_Tss lthy |>> (rpair NONE o SOME)
       else
-        mk_coiters_args_types Cs ns mss xtor_co_iter_fun_Tss lthy |>> (pair NONE o SOME)
+        mk_coiters_args_types ctr_Tsss Cs ns mss xtor_co_iter_fun_Tss lthy |>> (pair NONE o SOME)
   in
     ((xtor_co_iterss, iters_args_types, coiters_args_types), lthy')
   end;
@@ -1224,7 +1229,7 @@
     val mss = map (map length) ctr_Tsss;
 
     val ((xtor_co_iterss, iters_args_types, coiters_args_types), lthy') =
-      mk_co_iters_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy;
+      mk_co_iters_prelims fp ctr_Tsss fpTs Cs ns mss xtor_co_iterss0 lthy;
 
     fun define_ctrs_dtrs_for_type (((((((((((((((((((((((fp_bnf, fp_b), fpT), ctor), dtor),
             xtor_co_iters), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),

--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Thu Sep 12 18:09:17 2013 -0700
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Thu Sep 12 18:09:56 2013 -0700
@@ -127,7 +127,7 @@
       val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs;
 
       val ((xtor_co_iterss, iters_args_types, coiters_args_types), _) =
-        mk_co_iters_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy;
+        mk_co_iters_prelims fp ctr_Tsss fpTs Cs ns mss xtor_co_iterss0 lthy;
 
       fun mk_binding b suf = Binding.suffix_name ("_" ^ suf) b;
 

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 12 18:09:17 2013 -0700
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 12 18:09:56 2013 -0700
@@ -312,7 +312,8 @@
 
     val perm_Cs = map (body_type o fastype_of o co_rec_of o of_fp_sugar (#xtor_co_iterss o #fp_res))
       perm_fp_sugars;
-    val perm_fun_arg_Tssss = mk_iter_fun_arg_types perm_Cs perm_ns perm_mss (co_rec_of ctor_iters1);
+    val perm_fun_arg_Tssss =
+      mk_iter_fun_arg_types perm_ctr_Tsss perm_ns perm_mss (co_rec_of ctor_iters1);
 
     fun unpermute0 perm0_xs = permute_like (op =) perm0_kks kks perm0_xs;
     fun unpermute perm_xs = permute_like (op =) perm_indices indices perm_xs;
@@ -389,12 +390,11 @@
     val nn = length perm_fpTs;
     val kks = 0 upto nn - 1;
     val perm_ns = map length perm_ctr_Tsss;
-    val perm_mss = map (map length) perm_ctr_Tsss;
 
     val perm_Cs = map (domain_type o body_fun_type o fastype_of o co_rec_of o
       of_fp_sugar (#xtor_co_iterss o #fp_res)) perm_fp_sugars;
     val (perm_p_Tss, (perm_q_Tssss, _, perm_f_Tssss, _)) =
-      mk_coiter_fun_arg_types perm_Cs perm_ns perm_mss (co_rec_of dtor_coiters1);
+      mk_coiter_fun_arg_types perm_ctr_Tsss perm_Cs perm_ns (co_rec_of dtor_coiters1);
 
     val (perm_p_hss, h) = indexedd perm_p_Tss 0;
     val (perm_q_hssss, h') = indexedddd perm_q_Tssss h;