--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Thu Sep 20 17:25:07 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Thu Sep 20 17:35:49 2012 +0200
@@ -227,8 +227,9 @@
val fp_iter_fun_Ts = fst (split_last (binder_types (fastype_of fp_iter1)));
val fp_rec_fun_Ts = fst (split_last (binder_types (fastype_of fp_rec1)));
- val ((iter_only as (gss, _, _), rec_only as (hss, _, _)),
- (zs, cs, cpss, coiter_only as ((pgss, crgsss), _), corec_only as ((phss, cshsss), _))) =
+ val (((iter_only as (gss, _, _), rec_only as (hss, _, _)),
+ (zs, cs, cpss, coiter_only as ((pgss, crgsss), _), corec_only as ((phss, cshsss), _))),
+ names_lthy) =
if lfp then
let
val y_Tsss =
@@ -236,7 +237,7 @@
ns mss fp_iter_fun_Ts;
val g_Tss = map2 (map2 (curry (op --->))) y_Tsss Css;
- val ((gss, ysss), _) =
+ val ((gss, ysss), lthy) =
lthy
|> mk_Freess "f" g_Tss
||>> mk_Freesss "x" y_Tsss;
@@ -253,13 +254,13 @@
val hss = map2 (map2 retype_free) h_Tss gss;
val zssss_hd = map2 (map2 (map2 (retype_free o hd))) z_Tssss ysss;
- val (zssss_tl, _) =
+ val (zssss_tl, lthy) =
lthy
|> mk_Freessss "y" (map (map (map tl)) z_Tssss);
val zssss = map2 (map2 (map2 cons)) zssss_hd zssss_tl;
in
- (((gss, g_Tss, yssss), (hss, h_Tss, zssss)),
- ([], [], [], (([], []), ([], [])), (([], []), ([], []))))
+ ((((gss, g_Tss, yssss), (hss, h_Tss, zssss)),
+ ([], [], [], (([], []), ([], [])), (([], []), ([], [])))), lthy)
end
else
let
@@ -288,7 +289,7 @@
val (r_Tssss, g_sum_prod_Ts, g_Tssss, pg_Tss) = mk_types single fp_iter_fun_Ts;
- val ((((Free (z, _), cs), pss), gssss), _) =
+ val ((((Free (z, _), cs), pss), gssss), lthy) =
lthy
|> yield_singleton (mk_Frees "z") dummyT
||>> mk_Frees "a" Cs
@@ -303,7 +304,7 @@
val (s_Tssss, h_sum_prod_Ts, h_Tssss, ph_Tss) = mk_types dest_corec_sumT fp_rec_fun_Ts;
val hssss_hd = map2 (map2 (map2 (fn T :: _ => fn [g] => retype_free T g))) h_Tssss gssss;
- val ((sssss, hssss_tl), _) =
+ val ((sssss, hssss_tl), lthy) =
lthy
|> mk_Freessss "q" s_Tssss
||>> mk_Freessss "h" (map (map (map tl)) h_Tssss);
@@ -323,9 +324,9 @@
val cqfsss = map2 (map2 (map2 mk_preds_getters_join)) cqssss cfssss;
in (pfss, cqfsss) end;
in
- ((([], [], []), ([], [], [])),
- ([z], cs, cpss, (mk_terms rssss gssss, (g_sum_prod_Ts, pg_Tss)),
- (mk_terms sssss hssss, (h_sum_prod_Ts, ph_Tss))))
+ (((([], [], []), ([], [], [])),
+ ([z], cs, cpss, (mk_terms rssss gssss, (g_sum_prod_Ts, pg_Tss)),
+ (mk_terms sssss hssss, (h_sum_prod_Ts, ph_Tss)))), lthy)
end;
fun define_ctrs_case_for_type ((((((((((((((((((fp_b, fpT), C), fld), unf), fp_iter), fp_rec),
@@ -518,7 +519,7 @@
in Term.list_comb (mapx, args) end;
val mk_simp_thmss =
- map3 (fn (_, injects, distincts, cases, _, _) => fn rec_likes => fn iter_likes =>
+ map3 (fn (_, _, injects, distincts, cases, _, _, _) => fn rec_likes => fn iter_likes =>
injects @ distincts @ cases @ rec_likes @ iter_likes);
fun derive_induct_iter_rec_thms_for_types ((wrap_ress, ctrss, iters, recs, xsss, ctr_defss,
@@ -594,8 +595,7 @@
val goal =
Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss,
- HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
- (map2 (curry (op $)) phis vs)));
+ HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry (op $)) phis vs)));
val kksss = map (map (map (fst o snd) o #2)) raw_premss;
@@ -619,7 +619,7 @@
val giters = map (lists_bmoc gss) iters;
val hrecs = map (lists_bmoc hss) recs;
- fun mk_iter_like_goal fss fiter_like xctr f xs fxs =
+ fun mk_goal fss fiter_like xctr f xs fxs =
fold_rev (fold_rev Logic.all) (xs :: fss)
(mk_Trueprop_eq (fiter_like $ xctr, Term.list_comb (f, fxs)));
@@ -645,8 +645,8 @@
val gxsss = map (map (maps (intr_calls giters (K I) (K I) (K I)))) xsss;
val hxsss = map (map (maps (intr_calls hrecs cons tick (curry HOLogic.mk_prodT)))) xsss;
- val iterss_goal = map5 (map4 o mk_iter_like_goal gss) giters xctrss gss xsss gxsss;
- val recss_goal = map5 (map4 o mk_iter_like_goal hss) hrecs xctrss hss xsss hxsss;
+ val iter_goalss = map5 (map4 o mk_goal gss) giters xctrss gss xsss gxsss;
+ val rec_goalss = map5 (map4 o mk_goal hss) hrecs xctrss hss xsss hxsss;
val iter_tacss =
map2 (map o mk_iter_like_tac pre_map_defs nesting_map_ids iter_defs) fp_iter_thms
@@ -654,11 +654,11 @@
val rec_tacss =
map2 (map o mk_iter_like_tac pre_map_defs nesting_map_ids rec_defs) fp_rec_thms
ctr_defss;
+
+ fun prove goal tac = Skip_Proof.prove lthy [] [] goal (tac o #context);
in
- (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
- iterss_goal iter_tacss,
- map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
- recss_goal rec_tacss)
+ (map2 (map2 prove) iter_goalss iter_tacss,
+ map2 (map2 prove) rec_goalss rec_tacss)
end;
val simp_thmss = mk_simp_thmss wrap_ress rec_thmss iter_thmss;
@@ -690,9 +690,11 @@
fun derive_coinduct_coiter_corec_thms_for_types ((wrap_ress, ctrss, coiters, corecs, _,
ctr_defss, coiter_defs, corec_defs), lthy) =
let
- val selsss = map #1 wrap_ress;
- val discIss = map #5 wrap_ress;
- val sel_thmsss = map #6 wrap_ress;
+ val discss = map (map (mk_disc_or_sel As) o #1) wrap_ress;
+ val selsss = map #2 wrap_ress;
+ val disc_thmsss = map #6 wrap_ress;
+ val discIss = map #7 wrap_ress;
+ val sel_thmsss = map #8 wrap_ress;
val (vs', _) =
lthy
@@ -707,17 +709,17 @@
`(conj_dests nn) coinduct_thm
end;
+ fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
+
+ val z = the_single zs;
+ val gcoiters = map (lists_bmoc pgss) coiters;
+ val hcorecs = map (lists_bmoc phss) corecs;
+
val (coiter_thmss, corec_thmss, safe_coiter_thmss, safe_corec_thmss) =
let
- val z = the_single zs;
- val gcoiters = map (lists_bmoc pgss) coiters;
- val hcorecs = map (lists_bmoc phss) corecs;
-
- fun mk_cond_goal pos = HOLogic.mk_Trueprop o (not pos ? HOLogic.mk_not);
-
- fun mk_coiter_like_goal pfss c cps fcoiter_like n k ctr m cfs' =
+ fun mk_goal pfss c cps fcoiter_like n k ctr m cfs' =
fold_rev (fold_rev Logic.all) ([c] :: pfss)
- (Logic.list_implies (seq_conds mk_cond_goal n k cps,
+ (Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps,
mk_Trueprop_eq (fcoiter_like $ c, Term.list_comb (ctr, take m cfs'))));
fun build_call fiter_likes maybe_tack (T, U) =
@@ -742,10 +744,10 @@
val crgsss' = map (map (map (intr_calls gcoiters (K I) (K I)))) crgsss;
val cshsss' = map (map (map (intr_calls hcorecs (curry mk_sumT) (tack z)))) cshsss;
- val coiterss_goal =
- map8 (map4 oooo mk_coiter_like_goal pgss) cs cpss gcoiters ns kss ctrss mss crgsss';
- val corecss_goal =
- map8 (map4 oooo mk_coiter_like_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss';
+ val coiter_goalss =
+ map8 (map4 oooo mk_goal pgss) cs cpss gcoiters ns kss ctrss mss crgsss';
+ val corec_goalss =
+ map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss';
val coiter_tacss =
map3 (map oo mk_coiter_like_tac coiter_defs nesting_map_ids) fp_iter_thms pre_map_defs
@@ -754,15 +756,13 @@
map3 (map oo mk_coiter_like_tac corec_defs nesting_map_ids) fp_rec_thms pre_map_defs
ctr_defss;
- val coiter_thmss =
- map2 (map2 (fn goal => fn tac =>
- Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation))
- coiterss_goal coiter_tacss;
+ fun prove goal tac =
+ Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation;
+
+ val coiter_thmss = map2 (map2 prove) coiter_goalss coiter_tacss;
val corec_thmss =
- map2 (map2 (fn goal => fn tac =>
- Skip_Proof.prove lthy [] [] goal (tac o #context)
- |> unfold_defs lthy @{thms sum_case_if} |> Thm.close_derivation))
- corecss_goal corec_tacss;
+ map2 (map2 prove) corec_goalss corec_tacss
+ |> map (map (unfold_defs lthy @{thms sum_case_if}));
val coiter_safesss = map2 (map2 (map2 (curry (op =)))) crgsss' crgsss;
val corec_safesss = map2 (map2 (map2 (curry (op =)))) cshsss' cshsss;
@@ -777,14 +777,36 @@
(coiter_thmss, corec_thmss, safe_coiter_thmss, safe_corec_thmss)
end;
- val (coiter_iff_thmss, corec_iff_thmss) =
+ val (disc_coiter_iff_thmss, disc_corec_iff_thmss) =
let
- (* TODO: smoothly handle the n = 1 case *)
+ fun mk_goal c cps fcoiter_like n k disc =
+ mk_Trueprop_eq (disc $ (fcoiter_like $ c),
+ if n = 1 then @{const True}
+ else Library.foldr1 HOLogic.mk_conj (seq_conds mk_maybe_not n k cps));
+
+ val coiter_goalss = map6 (map2 oooo mk_goal) cs cpss gcoiters ns kss discss;
+ val corec_goalss = map6 (map2 oooo mk_goal) cs cpss hcorecs ns kss discss;
+
+ fun mk_case_split' cp =
+ Drule.instantiate' [] [SOME (certify lthy cp)] @{thm case_split};
+
+ val case_splitss' = map (map mk_case_split') cpss;
- val coiter_iff_thmss = [];
- val corec_iff_thmss = [];
+ val coiter_tacss =
+ map3 (map oo mk_disc_coiter_like_iff_tac) case_splitss' coiter_thmss disc_thmsss;
+ val corec_tacss =
+ map3 (map oo mk_disc_coiter_like_iff_tac) case_splitss' corec_thmss disc_thmsss;
+
+ fun prove goal tac =
+ Skip_Proof.prove lthy [] [] goal (tac o #context)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy no_defs_lthy);
+
+ fun proves [_] [_] = []
+ | proves goals tacs = map2 prove goals tacs;
in
- (coiter_iff_thmss, corec_iff_thmss)
+ (map2 proves coiter_goalss coiter_tacss,
+ map2 proves corec_goalss corec_tacss)
end;
fun mk_disc_coiter_like_thms coiter_likes discIs =
@@ -831,10 +853,10 @@
val notes =
[(coinductN, map single coinduct_thms, []), (* FIXME: attribs *)
(coitersN, coiter_thmss, []),
- (coiter_iffN, coiter_iff_thmss, simp_attrs),
(corecsN, corec_thmss, []),
- (corec_iffN, corec_iff_thmss, simp_attrs),
+ (disc_coiter_iffN, disc_coiter_iff_thmss, simp_attrs),
(disc_coitersN, disc_coiter_thmss, simp_attrs),
+ (disc_corec_iffN, disc_corec_iff_thmss, simp_attrs),
(disc_corecsN, disc_corec_thmss, simp_attrs),
(sel_coitersN, sel_coiter_thmss, simp_attrs),
(sel_corecsN, sel_corec_thmss, simp_attrs),
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Thu Sep 20 17:25:07 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Thu Sep 20 17:35:49 2012 +0200
@@ -9,11 +9,13 @@
sig
val mk_half_pairss: 'a list -> ('a * 'a) list list
val mk_ctr: typ list -> term -> term
+ val mk_disc_or_sel: typ list -> term -> term
val base_name_of_ctr: term -> string
val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list ->
((bool * term list) * term) *
(binding list * (binding list list * (binding * term) list list)) -> local_theory ->
- (term list list * thm list * thm list * thm list * thm list * thm list list) * local_theory
+ (term list * term list list * thm list * thm list * thm list * thm list list * thm list *
+ thm list list) * local_theory
val parse_wrap_options: bool parser
val parse_bound_term: (binding * string) parser
end;
@@ -70,6 +72,9 @@
Term.subst_atomic_types (Ts0 ~~ Ts) ctr
end;
+fun mk_disc_or_sel Ts t =
+ Term.subst_atomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
+
fun base_name_of_ctr c =
Long_Name.base_name (case head_of c of
Const (s, _) => s
@@ -279,9 +284,6 @@
val discs0 = map (Morphism.term phi) raw_discs;
val selss0 = unflat_selss (map (Morphism.term phi) raw_sels);
- fun mk_disc_or_sel Ts c =
- Term.subst_atomic_types (snd (Term.dest_Type (domain_type (fastype_of c))) ~~ Ts) c;
-
val discs = map (mk_disc_or_sel As) discs0;
val selss = map (map (mk_disc_or_sel As)) selss0;
in
@@ -295,7 +297,7 @@
fold_rev Logic.all [p, v] (mk_imp_p (map2 mk_prem xctrs xss))
end;
- val injectss_goal =
+ val inject_goalss =
let
fun mk_goal _ _ [] [] = []
| mk_goal xctr yctr xs ys =
@@ -305,7 +307,7 @@
map4 mk_goal xctrs yctrs xss yss
end;
- val half_distinctss_goal =
+ val half_distinct_goalss =
let
fun mk_goal ((xs, xc), (xs', xc')) =
fold_rev Logic.all (xs @ xs')
@@ -318,7 +320,7 @@
map3 (fn xs => fn xctr => fn xf =>
fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (fcase $ xctr, xf))) xss xctrs xfs;
- val goalss = [exhaust_goal] :: injectss_goal @ half_distinctss_goal @ [cases_goal];
+ val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss @ [cases_goal];
fun after_qed thmss lthy =
let
@@ -352,10 +354,10 @@
Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm)
end;
- val (all_sel_thms, sel_thmss, disc_thms, discI_thms, disc_exclude_thms, disc_exhaust_thms,
- collapse_thms, case_eq_thms) =
+ val (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms,
+ disc_exhaust_thms, collapse_thms, case_eq_thms) =
if no_dests then
- ([], [], [], [], [], [], [], [])
+ ([], [], [], [], [], [], [], [], [])
else
let
fun make_sel_thm xs' case_thm sel_def =
@@ -444,16 +446,16 @@
val infos = ms ~~ discD_thms ~~ discs ~~ no_discs;
val half_pairss = mk_half_pairss infos;
- val halvess_goal = map mk_goal half_pairss;
+ val half_goalss = map mk_goal half_pairss;
val half_thmss =
map3 (fn [] => K (K []) | [goal] => fn [((((m, discD), _), _), _)] =>
fn disc_thm => [prove (mk_half_disc_exclude_tac m discD disc_thm) goal])
- halvess_goal half_pairss (flat disc_thmss');
+ half_goalss half_pairss (flat disc_thmss');
- val other_halvess_goal = map (mk_goal o map swap) half_pairss;
+ val other_half_goalss = map (mk_goal o map swap) half_pairss;
val other_half_thmss =
map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss
- other_halvess_goal;
+ other_half_goalss;
in
interleave (flat half_thmss) (flat other_half_thmss)
end;
@@ -508,8 +510,8 @@
|> Proof_Context.export names_lthy lthy
end;
in
- (all_sel_thms, sel_thmss, disc_thms, discI_thms, disc_exclude_thms, disc_exhaust_thms,
- collapse_thms, case_eq_thms)
+ (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms,
+ disc_exhaust_thms, collapse_thms, case_eq_thms)
end;
val (case_cong_thm, weak_case_cong_thm) =
@@ -586,7 +588,7 @@
[(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)]
|> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
in
- ((selss, inject_thms, distinct_thms, case_thms, discI_thms, sel_thmss),
+ ((discs, selss, inject_thms, distinct_thms, case_thms, disc_thmss, discI_thms, sel_thmss),
lthy |> Local_Theory.notes (notes' @ notes) |> snd)
end;
in