1.1 --- a/src/HOL/Codatatype/Tools/bnf_def.ML	Sat Sep 08 21:04:26 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Sat Sep 08 21:04:26 2012 +0200
     1.3 @@ -28,6 +28,8 @@
     1.4    val rel_unfoldN: string
     1.5    val pred_unfoldN: string
     1.6  
     1.7 +  val map_of_bnf: BNF -> term
     1.8 +
     1.9    val mk_T_of_bnf: typ list -> typ list -> BNF -> typ
    1.10    val mk_bd_of_bnf: typ list -> typ list -> BNF -> term
    1.11    val mk_map_of_bnf: typ list -> typ list -> typ list -> BNF -> term

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:26 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:26 2012 +0200
     2.3 @@ -15,6 +15,7 @@
     2.4  
     2.5  open BNF_Util
     2.6  open BNF_Wrap
     2.7 +open BNF_Def
     2.8  open BNF_FP_Util
     2.9  open BNF_LFP
    2.10  open BNF_GFP
    2.11 @@ -26,7 +27,14 @@
    2.12  val itersN = "iters";
    2.13  val recsN = "recs";
    2.14  
    2.15 -fun split_list7 xs = (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs);
    2.16 +fun split_list8 xs =
    2.17 +  (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs, map #8 xs);
    2.18 +
    2.19 +fun typ_subst inst (T as Type (s, Ts)) =
    2.20 +    (case AList.lookup (op =) inst T of
    2.21 +      NONE => Type (s, map (typ_subst inst) Ts)
    2.22 +    | SOME T' => T')
    2.23 +  | typ_subst inst T = the_default T (AList.lookup (op =) inst T);
    2.24  
    2.25  fun retype_free (Free (s, _)) T = Free (s, T);
    2.26  
    2.27 @@ -37,6 +45,8 @@
    2.28  fun mk_uncurried2_fun f xss =
    2.29    mk_tupled_fun (HOLogic.mk_tuple (map HOLogic.mk_tuple xss)) f (flat xss);
    2.30  
    2.31 +fun tick v f = Term.lambda v (HOLogic.mk_prod (v, f $ v))
    2.32 +
    2.33  fun popescu_zip [] [fs] = fs
    2.34    | popescu_zip (p :: ps) (fs :: fss) = p :: fs @ popescu_zip ps fss;
    2.35  
    2.36 @@ -160,14 +170,14 @@
    2.37      val mss = map (map length) ctr_Tsss;
    2.38      val Css = map2 replicate ns Cs;
    2.39  
    2.40 -    fun mk_iter_like Ts Us c =
    2.41 +    fun mk_iter_like Ts Us t =
    2.42        let
    2.43 -        val (binders, body) = strip_type (fastype_of c);
    2.44 +        val (binders, body) = strip_type (fastype_of t);
    2.45          val (f_Us, prebody) = split_last binders;
    2.46          val Type (_, Ts0) = if lfp then prebody else body;
    2.47          val Us0 = distinct (op =) (map (if lfp then body_type else domain_type) f_Us);
    2.48        in
    2.49 -        Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) c
    2.50 +        Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
    2.51        end;
    2.52  
    2.53      val fp_iters as fp_iter1 :: _ = map (mk_iter_like As Cs) fp_iters0;
    2.54 @@ -359,7 +369,7 @@
    2.55              val iter = mk_iter_like As Cs iter0;
    2.56              val recx = mk_iter_like As Cs rec0;
    2.57            in
    2.58 -            ((ctrs, iter, recx, xss, ctr_defs, iter_def, rec_def), lthy)
    2.59 +            ((ctrs, iter, recx, v, xss, ctr_defs, iter_def, rec_def), lthy)
    2.60            end;
    2.61  
    2.62          fun some_gfp_sugar no_defs_lthy =
    2.63 @@ -402,14 +412,19 @@
    2.64  
    2.65              val [coiter, corec] = map (mk_iter_like As Cs o Morphism.term phi) csts;
    2.66            in
    2.67 -            ((ctrs, coiter, corec, xss, ctr_defs, coiter_def, corec_def), lthy)
    2.68 +            ((ctrs, coiter, corec, v, xss, ctr_defs, coiter_def, corec_def), lthy)
    2.69            end;
    2.70        in
    2.71          wrap_datatype tacss ((ctrs0, casex0), (disc_binders, sel_binderss)) lthy'
    2.72          |> (if lfp then some_lfp_sugar else some_gfp_sugar)
    2.73        end;
    2.74  
    2.75 -    fun pour_more_sugar_on_lfps ((ctrss, iters, recs, xsss, ctr_defss, iter_defs, rec_defs),
    2.76 +    fun mk_map Ts Us t =
    2.77 +      let val (Type (_, Ts0), Type (_, Us0)) = strip_type (fastype_of t) |>> List.last in
    2.78 +        Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
    2.79 +      end;
    2.80 +
    2.81 +    fun pour_more_sugar_on_lfps ((ctrss, iters, recs, vs, xsss, ctr_defss, iter_defs, rec_defs),
    2.82          lthy) =
    2.83        let
    2.84          val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;
    2.85 @@ -422,13 +437,40 @@
    2.86                fold_rev (fold_rev Logic.all) (xs :: fss)
    2.87                  (mk_Trueprop_eq (fiter_like $ xctr, Term.list_comb (f, fxs)));
    2.88  
    2.89 -            fun repair_iter_call (x as Free (_, T)) =
    2.90 -              (case find_index (curry (op =) T) fpTs of ~1 => x | j => nth giters j $ x);
    2.91 +            fun build_iter_like fiter_likes maybe_tick =
    2.92 +              let
    2.93 +                fun build (T, U) =
    2.94 +                  if T = U then
    2.95 +                    Const (@{const_name id}, T --> T)
    2.96 +                  else
    2.97 +                    (case (find_index (curry (op =) T) fpTs, (T, U)) of
    2.98 +                      (~1, (Type (s, Ts), Type (_, Us))) =>
    2.99 +                      let
   2.100 +                        val map0 = map_of_bnf (the (bnf_of lthy (Long_Name.base_name s)));
   2.101 +                        val mapx = mk_map Ts Us map0;
   2.102 +                        val TUs = map dest_funT (fst (split_last (binder_types (fastype_of mapx))));
   2.103 +                        val args = map build TUs;
   2.104 +                      in Term.list_comb (mapx, args) end
   2.105 +                    | (j, _) => maybe_tick (nth vs j) (nth fiter_likes j))
   2.106 +              in build end;
   2.107 +
   2.108 +            fun mk_U maybe_prodT =
   2.109 +              typ_subst (map2 (fn fpT => fn C => (fpT, maybe_prodT fpT C)) fpTs Cs);
   2.110 +
   2.111 +            fun repair_calls fiter_likes maybe_cons maybe_tick maybe_prodT (x as Free (_, T)) =
   2.112 +              if member (op =) fpTs T then
   2.113 +                maybe_cons x [build_iter_like fiter_likes (K I) (T, mk_U (K I) T) $ x]
   2.114 +              else if exists_subtype (member (op =) fpTs) T then
   2.115 +                [build_iter_like fiter_likes maybe_tick (T, mk_U maybe_prodT T) $ x]
   2.116 +              else
   2.117 +                [x];
   2.118 +
   2.119              fun repair_rec_call (x as Free (_, T)) =
   2.120                (case find_index (curry (op =) T) fpTs of ~1 => [x] | j => [x, nth hrecs j $ x]);
   2.121  
   2.122 -            val gxsss = map (map (map repair_iter_call)) xsss;
   2.123 -            val hxsss = map (map (maps repair_rec_call)) xsss;
   2.124 +            val gxsss = map (map (maps (repair_calls giters (K I) (K I) (K I)))) xsss;
   2.125 +            val hxsss =
   2.126 +              map (map (maps (repair_calls hrecs cons tick (curry HOLogic.mk_prodT)))) xsss;
   2.127  
   2.128              val goal_iterss = map5 (map4 o mk_goal_iter_like gss) giters xctrss gss xsss gxsss;
   2.129              val goal_recss = map5 (map4 o mk_goal_iter_like hss) hrecs xctrss hss xsss hxsss;
   2.130 @@ -455,8 +497,8 @@
   2.131          lthy |> Local_Theory.notes notes |> snd
   2.132        end;
   2.133  
   2.134 -    fun pour_more_sugar_on_gfps ((ctrss, coiters, corecs, xsss, ctr_defss, coiter_defs, corec_defs),
   2.135 -        lthy) =
   2.136 +    fun pour_more_sugar_on_gfps ((ctrss, coiters, corecs, vs, xsss, ctr_defss, coiter_defs,
   2.137 +        corec_defs), lthy) =
   2.138        let
   2.139          val gcoiters = map (lists_bmoc pgss) coiters;
   2.140          val hcorecs = map (lists_bmoc phss) corecs;
   2.141 @@ -505,7 +547,7 @@
   2.142        |> fold_map pour_some_sugar_on_type (bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~
   2.143          fp_recs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ns ~~ kss ~~ mss ~~ ctr_binderss ~~
   2.144          ctr_mixfixess ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss)
   2.145 -      |>> split_list7
   2.146 +      |>> split_list8
   2.147        |> (if lfp then pour_more_sugar_on_lfps else pour_more_sugar_on_gfps);
   2.148  
   2.149      val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^