1.1 --- a/src/HOL/Codatatype/BNF_Library.thy	Tue Sep 11 13:06:13 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/BNF_Library.thy	Tue Sep 11 13:06:13 2012 +0200
     1.3 @@ -843,6 +843,14 @@
     1.4    "\<lbrakk>\<forall>x. s = f (Inr (Inl x)) \<longrightarrow> P; \<forall>x. s = f (Inr (Inr x)) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f (Inr x) \<longrightarrow> P"
     1.5  by (metis obj_sumE)
     1.6  
     1.7 +lemma sum_map_if:
     1.8 +"sum_map f g (if p then Inl x else Inr y) = (if p then Inl (f x) else Inr (g y))"
     1.9 +by simp
    1.10 +
    1.11 +lemma sum_case_if:
    1.12 +"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
    1.13 +by simp
    1.14 +
    1.15  lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
    1.16  by simp
    1.17  

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 11 13:06:13 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 11 13:06:13 2012 +0200
     2.3 @@ -210,12 +210,8 @@
     2.4      val fp_iter_fun_Ts = fst (split_last (binder_types (fastype_of fp_iter1)));
     2.5      val fp_rec_fun_Ts = fst (split_last (binder_types (fastype_of fp_rec1)));
     2.6  
     2.7 -    fun dest_rec_pair (T as Type (@{type_name prod}, Us as [_, U])) =
     2.8 -        if member (op =) Cs U then Us else [T]
     2.9 -      | dest_rec_pair T = [T];
    2.10 -
    2.11      val ((iter_only as (gss, _, _), rec_only as (hss, _, _)),
    2.12 -         (zs, cs, cpss, coiter_only as ((pgss, cgsss), _), corec_only as ((phss, chsss), _))) =
    2.13 +         (zs, cs, cpss, coiter_only as ((pgss, cgssss), _), corec_only as ((phss, chssss), _))) =
    2.14        if lfp then
    2.15          let
    2.16            val y_Tsss =
    2.17 @@ -227,18 +223,25 @@
    2.18              lthy
    2.19              |> mk_Freess "f" g_Tss
    2.20              ||>> mk_Freesss "x" y_Tsss;
    2.21 +          val yssss = map (map (map single)) ysss;
    2.22 +
    2.23 +          fun dest_rec_prodT (T as Type (@{type_name prod}, Us as [_, U])) =
    2.24 +              if member (op =) Cs U then Us else [T]
    2.25 +            | dest_rec_prodT T = [T];
    2.26  
    2.27            val z_Tssss =
    2.28 -            map3 (fn n => fn ms => map2 (map dest_rec_pair oo dest_tupleT) ms o
    2.29 +            map3 (fn n => fn ms => map2 (map dest_rec_prodT oo dest_tupleT) ms o
    2.30                dest_sumTN_balanced n o domain_type) ns mss fp_rec_fun_Ts;
    2.31            val h_Tss = map2 (map2 (fold_rev (curry (op --->)))) z_Tssss Css;
    2.32  
    2.33            val hss = map2 (map2 retype_free) gss h_Tss;
    2.34 -          val (zssss, _) =
    2.35 +          val zssss_hd = map2 (map2 (map2 (fn y => fn T :: _ => retype_free y T))) ysss z_Tssss;
    2.36 +          val (zssss_tl, _) =
    2.37              lthy
    2.38 -            |> mk_Freessss "x" z_Tssss;
    2.39 +            |> mk_Freessss "y" (map (map (map tl)) z_Tssss);
    2.40 +          val zssss = map2 (map2 (map2 cons)) zssss_hd zssss_tl;
    2.41          in
    2.42 -          (((gss, g_Tss, map (map (map single)) ysss), (hss, h_Tss, zssss)),
    2.43 +          (((gss, g_Tss, yssss), (hss, h_Tss, zssss)),
    2.44             ([], [], [], (([], []), ([], [])), (([], []), ([], []))))
    2.45          end
    2.46        else
    2.47 @@ -249,20 +252,23 @@
    2.48            val p_Tss =
    2.49              map2 (fn C => fn n => replicate (Int.max (0, n - 1)) (C --> HOLogic.boolT)) Cs ns;
    2.50  
    2.51 -          fun zip_preds_getters [] [fs] = fs
    2.52 -            | zip_preds_getters (p :: ps) (fs :: fss) = p :: fs @ zip_preds_getters ps fss;
    2.53 +          fun zip_getters fss = flat fss;
    2.54  
    2.55 -          fun mk_types fun_Ts =
    2.56 +          fun zip_preds_getters [] [fss] = zip_getters fss
    2.57 +            | zip_preds_getters (p :: ps) (fss :: fsss) =
    2.58 +              p :: zip_getters fss @ zip_preds_getters ps fsss;
    2.59 +
    2.60 +          fun mk_types maybe_dest_sumT fun_Ts =
    2.61              let
    2.62                val f_sum_prod_Ts = map range_type fun_Ts;
    2.63                val f_prod_Tss = map2 dest_sumTN_balanced ns f_sum_prod_Ts;
    2.64                val f_Tsss =
    2.65                  map3 (fn C => map2 (map (curry (op -->) C) oo dest_tupleT)) Cs mss' f_prod_Tss;
    2.66 -              val pf_Tss = map2 zip_preds_getters p_Tss f_Tsss
    2.67 +              val f_Tssss = map (map (map maybe_dest_sumT)) f_Tsss;
    2.68 +              val pf_Tss = map2 zip_preds_getters p_Tss f_Tssss;
    2.69              in (f_sum_prod_Ts, f_Tsss, pf_Tss) end;
    2.70  
    2.71 -          val (g_sum_prod_Ts, g_Tsss, pg_Tss) = mk_types fp_iter_fun_Ts;
    2.72 -          val (h_sum_prod_Ts, h_Tsss, ph_Tss) = mk_types fp_rec_fun_Ts;
    2.73 +          val (g_sum_prod_Ts, g_Tsss, pg_Tss) = mk_types single fp_iter_fun_Ts;
    2.74  
    2.75            val ((((Free (z, _), cs), pss), gsss), _) =
    2.76              lthy
    2.77 @@ -270,20 +276,28 @@
    2.78              ||>> mk_Frees "a" Cs
    2.79              ||>> mk_Freess "p" p_Tss
    2.80              ||>> mk_Freesss "g" g_Tsss;
    2.81 +          val gssss = map (map (map single)) gsss;
    2.82 +
    2.83 +          fun dest_corec_sumT (T as Type (@{type_name sum}, Us as [_, U])) =
    2.84 +              if member (op =) Cs U then Us else [T]
    2.85 +            | dest_corec_sumT T = [T];
    2.86 +
    2.87 +          val (h_sum_prod_Ts, h_Tsss, ph_Tss) = mk_types dest_corec_sumT fp_rec_fun_Ts;
    2.88  
    2.89            val hsss = map2 (map2 (map2 retype_free)) gsss h_Tsss;
    2.90 +          val hssss = map (map (map single)) hsss; (*###*)
    2.91  
    2.92            val cpss = map2 (fn c => map (fn p => p $ c)) cs pss;
    2.93  
    2.94 -          fun mk_terms fsss =
    2.95 +          fun mk_terms fssss =
    2.96              let
    2.97 -              val pfss = map2 zip_preds_getters pss fsss;
    2.98 -              val cfsss = map2 (fn c => map (map (fn f => f $ c))) cs fsss
    2.99 -            in (pfss, cfsss) end;
   2.100 +              val pfss = map2 zip_preds_getters pss fssss;
   2.101 +              val cfssss = map2 (fn c => map (map (map (fn f => f $ c)))) cs fssss;
   2.102 +            in (pfss, cfssss) end;
   2.103          in
   2.104            ((([], [], []), ([], [], [])),
   2.105 -           ([z], cs, cpss, (mk_terms gsss, (g_sum_prod_Ts, pg_Tss)),
   2.106 -            (mk_terms hsss, (h_sum_prod_Ts, ph_Tss))))
   2.107 +           ([z], cs, cpss, (mk_terms gssss, (g_sum_prod_Ts, pg_Tss)),
   2.108 +            (mk_terms hssss, (h_sum_prod_Ts, ph_Tss))))
   2.109          end;
   2.110  
   2.111      fun pour_some_sugar_on_type (((((((((((((((((b, fpT), C), fld), unf), fp_iter), fp_rec),
   2.112 @@ -383,11 +397,11 @@
   2.113                        map2 (mk_sum_caseN_balanced oo map2 mk_uncurried2_fun) fss xssss));
   2.114                in (binder, spec) end;
   2.115  
   2.116 -            val iter_likes =
   2.117 +            val iter_like_bundles =
   2.118                [(iterN, fp_iter, iter_only),
   2.119                 (recN, fp_rec, rec_only)];
   2.120  
   2.121 -            val (binders, specs) = map generate_iter_like iter_likes |> split_list;
   2.122 +            val (binders, specs) = map generate_iter_like iter_like_bundles |> split_list;
   2.123  
   2.124              val ((csts, defs), (lthy', lthy)) = no_defs_lthy
   2.125                |> apfst split_list o fold_map2 (fn b => fn spec =>
   2.126 @@ -410,27 +424,29 @@
   2.127            let
   2.128              val B_to_fpT = C --> fpT;
   2.129  
   2.130 -            fun generate_coiter_like (suf, fp_iter_like, ((pfss, cfsss), (f_sum_prod_Ts, pf_Tss))) =
   2.131 +            fun mk_preds_getters_join c n cps sum_prod_T cfsss =
   2.132 +              Term.lambda c (mk_IfN sum_prod_T cps
   2.133 +                (map2 (mk_InN_balanced sum_prod_T n) (map (HOLogic.mk_tuple o flat) cfsss) (*###*)
   2.134 +                   (1 upto n)));
   2.135 +
   2.136 +            fun generate_coiter_like (suf, fp_iter_like, ((pfss, cfssss), (f_sum_prod_Ts,
   2.137 +                pf_Tss))) =
   2.138                let
   2.139                  val res_T = fold_rev (curry (op --->)) pf_Tss B_to_fpT;
   2.140  
   2.141                  val binder = Binding.suffix_name ("_" ^ suf) b;
   2.142  
   2.143 -                fun mk_preds_getters_join c n cps sum_prod_T cfss =
   2.144 -                  Term.lambda c (mk_IfN sum_prod_T cps
   2.145 -                    (map2 (mk_InN_balanced sum_prod_T n) (map HOLogic.mk_tuple cfss) (1 upto n)));
   2.146 -
   2.147                  val spec =
   2.148                    mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binder, res_T)),
   2.149                      Term.list_comb (fp_iter_like,
   2.150 -                      map5 mk_preds_getters_join cs ns cpss f_sum_prod_Ts cfsss));
   2.151 +                      map5 mk_preds_getters_join cs ns cpss f_sum_prod_Ts cfssss));
   2.152                in (binder, spec) end;
   2.153  
   2.154 -            val coiter_likes =
   2.155 +            val coiter_like_bundles =
   2.156                [(coiterN, fp_iter, coiter_only),
   2.157                 (corecN, fp_rec, corec_only)];
   2.158  
   2.159 -            val (binders, specs) = map generate_coiter_like coiter_likes |> split_list;
   2.160 +            val (binders, specs) = map generate_coiter_like coiter_like_bundles |> split_list;
   2.161  
   2.162              val ((csts, defs), (lthy', lthy)) = no_defs_lthy
   2.163                |> apfst split_list o fold_map2 (fn b => fn spec =>
   2.164 @@ -490,14 +506,14 @@
   2.165                    ~1 => build_map (build_call fiter_likes maybe_tick) T U
   2.166                  | j => maybe_tick (nth vs j) (nth fiter_likes j));
   2.167  
   2.168 -            fun mk_U maybe_prodT =
   2.169 -              typ_subst (map2 (fn fpT => fn C => (fpT, maybe_prodT fpT C)) fpTs Cs);
   2.170 +            fun mk_U maybe_mk_prodT =
   2.171 +              typ_subst (map2 (fn fpT => fn C => (fpT, maybe_mk_prodT fpT C)) fpTs Cs);
   2.172  
   2.173 -            fun repair_calls fiter_likes maybe_cons maybe_tick maybe_prodT (x as Free (_, T)) =
   2.174 +            fun repair_calls fiter_likes maybe_cons maybe_tick maybe_mk_prodT (x as Free (_, T)) =
   2.175                if member (op =) fpTs T then
   2.176                  maybe_cons x [build_call fiter_likes (K I) (T, mk_U (K I) T) $ x]
   2.177                else if exists_subtype (member (op =) fpTs) T then
   2.178 -                [build_call fiter_likes maybe_tick (T, mk_U maybe_prodT T) $ x]
   2.179 +                [build_call fiter_likes maybe_tick (T, mk_U maybe_mk_prodT T) $ x]
   2.180                else
   2.181                  [x];
   2.182  
   2.183 @@ -544,10 +560,10 @@
   2.184            let
   2.185              fun mk_goal_cond pos = HOLogic.mk_Trueprop o (not pos ? HOLogic.mk_not);
   2.186  
   2.187 -            fun mk_goal_coiter_like pfss c cps fcoiter_like n k ctr m cfs' =
   2.188 +            fun mk_goal_coiter_like pfss c cps fcoiter_like n k ctr m cfss' =
   2.189                fold_rev (fold_rev Logic.all) ([c] :: pfss)
   2.190                  (Logic.list_implies (seq_conds mk_goal_cond n k cps,
   2.191 -                   mk_Trueprop_eq (fcoiter_like $ c, Term.list_comb (ctr, take m cfs'))));
   2.192 +                   mk_Trueprop_eq (fcoiter_like $ c, lists_bmoc (take m cfss') ctr)));
   2.193  
   2.194              fun build_call fiter_likes maybe_tack (T, U) =
   2.195                if T = U then
   2.196 @@ -557,23 +573,25 @@
   2.197                    ~1 => build_map (build_call fiter_likes maybe_tack) T U
   2.198                  | j => maybe_tack (nth cs j, nth vs j) (nth fiter_likes j));
   2.199  
   2.200 -            fun mk_U maybe_sumT =
   2.201 -              typ_subst (map2 (fn C => fn fpT => (maybe_sumT fpT C, fpT)) Cs fpTs);
   2.202 +            fun mk_U maybe_mk_sumT =
   2.203 +              typ_subst (map2 (fn C => fn fpT => (maybe_mk_sumT fpT C, fpT)) Cs fpTs);
   2.204  
   2.205 -            fun repair_calls fiter_likes maybe_sumT maybe_tack
   2.206 +            fun repair_calls fiter_likes maybe_mk_sumT maybe_tack
   2.207                  (cf as Free (_, Type (_, [_, T])) $ _) =
   2.208                if exists_subtype (member (op =) Cs) T then
   2.209 -                build_call fiter_likes maybe_tack (T, mk_U maybe_sumT T) $ cf
   2.210 +                build_call fiter_likes maybe_tack (T, mk_U maybe_mk_sumT T) $ cf
   2.211                else
   2.212                  cf;
   2.213  
   2.214 -            val cgsss' = map (map (map (repair_calls gcoiters (K I) (K I)))) cgsss;
   2.215 -            val chsss' = map (map (map (repair_calls hcorecs (curry mk_sumT) (tack z)))) chsss;
   2.216 +            val cgssss' =
   2.217 +              map (map (map (map (repair_calls gcoiters (K I) (K I))))) cgssss;
   2.218 +            val chssss' =
   2.219 +              map (map (map (map (repair_calls hcorecs (curry mk_sumT) (tack z))))) chssss;
   2.220  
   2.221              val goal_coiterss =
   2.222 -              map8 (map4 oooo mk_goal_coiter_like pgss) cs cpss gcoiters ns kss ctrss mss cgsss';
   2.223 +              map8 (map4 oooo mk_goal_coiter_like pgss) cs cpss gcoiters ns kss ctrss mss cgssss';
   2.224              val goal_corecss =
   2.225 -              map8 (map4 oooo mk_goal_coiter_like phss) cs cpss hcorecs ns kss ctrss mss chsss';
   2.226 +              map8 (map4 oooo mk_goal_coiter_like phss) cs cpss hcorecs ns kss ctrss mss chssss';
   2.227  
   2.228              val coiter_tacss =
   2.229                map3 (map oo mk_coiter_like_tac coiter_defs map_ids) fp_iter_thms pre_map_defs

     3.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Tue Sep 11 13:06:13 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Tue Sep 11 13:06:13 2012 +0200
     3.3 @@ -60,7 +60,8 @@
     3.4      iter_like_thms) THEN Local_Defs.unfold_tac ctxt @{thms id_def} THEN rtac refl 1;
     3.5  
     3.6  val coiter_like_ss = ss_only @{thms if_True if_False};
     3.7 -val coiter_like_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases};
     3.8 +val coiter_like_thms =
     3.9 +  @{thms id_apply map_pair_def sum_case_if sum_map.simps sum_map_if prod.cases};
    3.10  
    3.11  fun mk_coiter_like_tac coiter_like_defs map_ids fld_unf_coiter_like pre_map_def ctr_def ctxt =
    3.12    Local_Defs.unfold_tac ctxt (ctr_def :: coiter_like_defs) THEN