1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sun Sep 09 13:04:57 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sun Sep 09 17:14:39 2012 +0200
     1.3 @@ -447,6 +447,24 @@
     1.4          Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
     1.5        end;
     1.6  
     1.7 +    fun build_iter_like_call vs basic_Ts fiter_likes maybe_tick =
     1.8 +      let
     1.9 +        fun build (T, U) =
    1.10 +          if T = U then
    1.11 +            Const (@{const_name id}, T --> T)
    1.12 +          else
    1.13 +            (case (find_index (curry (op =) T) basic_Ts, (T, U)) of
    1.14 +              (~1, (Type (s, Ts), Type (_, Us))) =>
    1.15 +              let
    1.16 +                val map0 = map_of_bnf (the (bnf_of lthy (Long_Name.base_name s)));
    1.17 +                val mapx = mk_map Ts Us map0;
    1.18 +                val TUs =
    1.19 +                  map dest_funT (fst (split_last (fst (strip_map_type (fastype_of mapx)))));
    1.20 +                val args = map build TUs;
    1.21 +              in Term.list_comb (mapx, args) end
    1.22 +            | (j, _) => maybe_tick (nth vs j) (nth fiter_likes j))
    1.23 +      in build end;
    1.24 +
    1.25      fun pour_more_sugar_on_lfps ((ctrss, iters, recs, vs, xsss, ctr_defss, iter_defs, rec_defs),
    1.26          lthy) =
    1.27        let
    1.28 @@ -460,32 +478,14 @@
    1.29                fold_rev (fold_rev Logic.all) (xs :: fss)
    1.30                  (mk_Trueprop_eq (fiter_like $ xctr, Term.list_comb (f, fxs)));
    1.31  
    1.32 -            fun build_call fiter_likes maybe_tick =
    1.33 -              let
    1.34 -                fun build (T, U) =
    1.35 -                  if T = U then
    1.36 -                    Const (@{const_name id}, T --> T)
    1.37 -                  else
    1.38 -                    (case (find_index (curry (op =) T) fpTs, (T, U)) of
    1.39 -                      (~1, (Type (s, Ts), Type (_, Us))) =>
    1.40 -                      let
    1.41 -                        val map0 = map_of_bnf (the (bnf_of lthy (Long_Name.base_name s)));
    1.42 -                        val mapx = mk_map Ts Us map0;
    1.43 -                        val TUs =
    1.44 -                          map dest_funT (fst (split_last (fst (strip_map_type (fastype_of mapx)))));
    1.45 -                        val args = map build TUs;
    1.46 -                      in Term.list_comb (mapx, args) end
    1.47 -                    | (j, _) => maybe_tick (nth vs j) (nth fiter_likes j))
    1.48 -              in build end;
    1.49 -
    1.50              fun mk_U maybe_prodT =
    1.51                typ_subst (map2 (fn fpT => fn C => (fpT, maybe_prodT fpT C)) fpTs Cs);
    1.52  
    1.53              fun repair_calls fiter_likes maybe_cons maybe_tick maybe_prodT (x as Free (_, T)) =
    1.54                if member (op =) fpTs T then
    1.55 -                maybe_cons x [build_call fiter_likes (K I) (T, mk_U (K I) T) $ x]
    1.56 +                maybe_cons x [build_iter_like_call vs fpTs fiter_likes (K I) (T, mk_U (K I) T) $ x]
    1.57                else if exists_subtype (member (op =) fpTs) T then
    1.58 -                [build_call fiter_likes maybe_tick (T, mk_U maybe_prodT T) $ x]
    1.59 +                [build_iter_like_call vs fpTs fiter_likes maybe_tick (T, mk_U maybe_prodT T) $ x]
    1.60                else
    1.61                  [x];
    1.62  
    1.63 @@ -526,17 +526,24 @@
    1.64  
    1.65          val (coiter_thmss, corec_thmss) =
    1.66            let
    1.67 -            fun mk_cond pos = HOLogic.mk_Trueprop o (not pos ? HOLogic.mk_not);
    1.68 +            fun mk_goal_cond pos = HOLogic.mk_Trueprop o (not pos ? HOLogic.mk_not);
    1.69  
    1.70              fun mk_goal_coiter_like pfss c cps fcoiter_like n k ctr cfs' =
    1.71                fold_rev (fold_rev Logic.all) ([c] :: pfss)
    1.72 -                (Logic.list_implies (seq_conds mk_cond n k cps,
    1.73 +                (Logic.list_implies (seq_conds mk_goal_cond n k cps,
    1.74                     mk_Trueprop_eq (fcoiter_like $ c, Term.list_comb (ctr, cfs'))));
    1.75  
    1.76 -            fun repair_call fcoiter_likes (cf as Free (_, Type (_, [_, T])) $ _) =
    1.77 -              (case find_index (curry (op =) T) Cs of ~1 => cf | j => nth fcoiter_likes j $ cf);
    1.78 +            fun mk_U maybe_sumT =
    1.79 +              typ_subst (map2 (fn C => fn fpT => (C, maybe_sumT C fpT)) Cs fpTs);
    1.80  
    1.81 -            val cgsss = map (map (map (repair_call gcoiters))) cgsss;
    1.82 +            fun repair_calls fiter_likes maybe_sumT maybe_tack
    1.83 +                (cf as Free (_, Type (_, [_, T])) $ _) =
    1.84 +              if exists_subtype (member (op =) Cs) T then
    1.85 +                build_iter_like_call vs Cs fiter_likes maybe_tack (T, mk_U maybe_sumT T) $ cf
    1.86 +              else
    1.87 +                cf;
    1.88 +
    1.89 +            val cgsss = map (map (map (repair_calls gcoiters (K I) (K I)))) cgsss;
    1.90  
    1.91              val goal_coiterss =
    1.92                map7 (map3 oooo mk_goal_coiter_like pgss) cs cpss gcoiters ns kss ctrss cgsss;

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sun Sep 09 13:04:57 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sun Sep 09 17:14:39 2012 +0200
     2.3 @@ -51,19 +51,19 @@
     2.4    Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
     2.5  
     2.6  val iter_like_thms =
     2.7 -  @{thms case_unit comp_def convol_def id_apply map_pair_def sum.simps(5,6) sum_map.simps
     2.8 -      split_conv};
     2.9 +  @{thms case_unit comp_def convol_def map_pair_def sum.simps(5,6) sum_map.simps split_conv};
    2.10  
    2.11  fun mk_iter_like_tac pre_map_defs map_ids iter_like_defs fld_iter_like ctr_def ctxt =
    2.12    Local_Defs.unfold_tac ctxt (ctr_def :: fld_iter_like :: iter_like_defs @ pre_map_defs @ map_ids @
    2.13 -    iter_like_thms) THEN rtac refl 1;
    2.14 +    iter_like_thms) THEN Local_Defs.unfold_tac ctxt @{thms id_def} THEN rtac refl 1;
    2.15  
    2.16  val coiter_like_ss = ss_only @{thms if_True if_False};
    2.17 -val coiter_like_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases};
    2.18 +val coiter_like_thms = @{thms map_pair_def sum_map.simps prod.cases};
    2.19  
    2.20  fun mk_coiter_like_tac coiter_like_defs map_ids fld_unf_coiter_like pre_map_def ctr_def ctxt =
    2.21    Local_Defs.unfold_tac ctxt (ctr_def :: coiter_like_defs) THEN
    2.22    subst_tac ctxt [fld_unf_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN
    2.23 -  Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN rtac refl 1;
    2.24 +  Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN
    2.25 +  Local_Defs.unfold_tac ctxt @{thms id_def} THEN rtac refl 1;
    2.26  
    2.27  end;