# HG changeset patch # User blanchet # Date 1347203679 -7200 # Node ID 9ea11f0c53e41d1cf8ec6327114374cb713a8fbf # Parent 43d2df3135595c5991938799cfc96d2ef08ed247 fixed and enabled generation of "coiters" theorems, including the recursive case diff -r 43d2df313559 -r 9ea11f0c53e4 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Sun Sep 09 13:04:57 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Sun Sep 09 17:14:39 2012 +0200 @@ -447,6 +447,24 @@ Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t end; + fun build_iter_like_call vs basic_Ts fiter_likes maybe_tick = + let + fun build (T, U) = + if T = U then + Const (@{const_name id}, T --> T) + else + (case (find_index (curry (op =) T) basic_Ts, (T, U)) of + (~1, (Type (s, Ts), Type (_, Us))) => + let + val map0 = map_of_bnf (the (bnf_of lthy (Long_Name.base_name s))); + val mapx = mk_map Ts Us map0; + val TUs = + map dest_funT (fst (split_last (fst (strip_map_type (fastype_of mapx))))); + val args = map build TUs; + in Term.list_comb (mapx, args) end + | (j, _) => maybe_tick (nth vs j) (nth fiter_likes j)) + in build end; + fun pour_more_sugar_on_lfps ((ctrss, iters, recs, vs, xsss, ctr_defss, iter_defs, rec_defs), lthy) = let @@ -460,32 +478,14 @@ fold_rev (fold_rev Logic.all) (xs :: fss) (mk_Trueprop_eq (fiter_like $ xctr, Term.list_comb (f, fxs))); - fun build_call fiter_likes maybe_tick = - let - fun build (T, U) = - if T = U then - Const (@{const_name id}, T --> T) - else - (case (find_index (curry (op =) T) fpTs, (T, U)) of - (~1, (Type (s, Ts), Type (_, Us))) => - let - val map0 = map_of_bnf (the (bnf_of lthy (Long_Name.base_name s))); - val mapx = mk_map Ts Us map0; - val TUs = - map dest_funT (fst (split_last (fst (strip_map_type (fastype_of mapx))))); - val args = map build TUs; - in Term.list_comb (mapx, args) end - | (j, _) => maybe_tick (nth vs j) (nth fiter_likes j)) - in build end; - fun mk_U maybe_prodT = typ_subst (map2 (fn fpT => fn C => (fpT, maybe_prodT fpT C)) fpTs Cs); fun repair_calls fiter_likes maybe_cons maybe_tick maybe_prodT (x as Free (_, T)) = if member (op =) fpTs T then - maybe_cons x [build_call fiter_likes (K I) (T, mk_U (K I) T) $ x] + maybe_cons x [build_iter_like_call vs fpTs fiter_likes (K I) (T, mk_U (K I) T) $ x] else if exists_subtype (member (op =) fpTs) T then - [build_call fiter_likes maybe_tick (T, mk_U maybe_prodT T) $ x] + [build_iter_like_call vs fpTs fiter_likes maybe_tick (T, mk_U maybe_prodT T) $ x] else [x]; @@ -526,17 +526,24 @@ val (coiter_thmss, corec_thmss) = let - fun mk_cond pos = HOLogic.mk_Trueprop o (not pos ? HOLogic.mk_not); + fun mk_goal_cond pos = HOLogic.mk_Trueprop o (not pos ? HOLogic.mk_not); fun mk_goal_coiter_like pfss c cps fcoiter_like n k ctr cfs' = fold_rev (fold_rev Logic.all) ([c] :: pfss) - (Logic.list_implies (seq_conds mk_cond n k cps, + (Logic.list_implies (seq_conds mk_goal_cond n k cps, mk_Trueprop_eq (fcoiter_like $ c, Term.list_comb (ctr, cfs')))); - fun repair_call fcoiter_likes (cf as Free (_, Type (_, [_, T])) $ _) = - (case find_index (curry (op =) T) Cs of ~1 => cf | j => nth fcoiter_likes j $ cf); + fun mk_U maybe_sumT = + typ_subst (map2 (fn C => fn fpT => (C, maybe_sumT C fpT)) Cs fpTs); - val cgsss = map (map (map (repair_call gcoiters))) cgsss; + fun repair_calls fiter_likes maybe_sumT maybe_tack + (cf as Free (_, Type (_, [_, T])) $ _) = + if exists_subtype (member (op =) Cs) T then + build_iter_like_call vs Cs fiter_likes maybe_tack (T, mk_U maybe_sumT T) $ cf + else + cf; + + val cgsss = map (map (map (repair_calls gcoiters (K I) (K I)))) cgsss; val goal_coiterss = map7 (map3 oooo mk_goal_coiter_like pgss) cs cpss gcoiters ns kss ctrss cgsss; diff -r 43d2df313559 -r 9ea11f0c53e4 src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Sun Sep 09 13:04:57 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Sun Sep 09 17:14:39 2012 +0200 @@ -51,19 +51,19 @@ Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1; val iter_like_thms = - @{thms case_unit comp_def convol_def id_apply map_pair_def sum.simps(5,6) sum_map.simps - split_conv}; + @{thms case_unit comp_def convol_def map_pair_def sum.simps(5,6) sum_map.simps split_conv}; fun mk_iter_like_tac pre_map_defs map_ids iter_like_defs fld_iter_like ctr_def ctxt = Local_Defs.unfold_tac ctxt (ctr_def :: fld_iter_like :: iter_like_defs @ pre_map_defs @ map_ids @ - iter_like_thms) THEN rtac refl 1; + iter_like_thms) THEN Local_Defs.unfold_tac ctxt @{thms id_def} THEN rtac refl 1; val coiter_like_ss = ss_only @{thms if_True if_False}; -val coiter_like_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases}; +val coiter_like_thms = @{thms map_pair_def sum_map.simps prod.cases}; fun mk_coiter_like_tac coiter_like_defs map_ids fld_unf_coiter_like pre_map_def ctr_def ctxt = Local_Defs.unfold_tac ctxt (ctr_def :: coiter_like_defs) THEN subst_tac ctxt [fld_unf_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN - Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN rtac refl 1; + Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN + Local_Defs.unfold_tac ctxt @{thms id_def} THEN rtac refl 1; end;