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;