--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 18 11:42:11 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 18 11:42:22 2012 +0200
@@ -34,9 +34,8 @@
val simp_attrs = @{attributes [simp]};
-fun split_list10 xs =
- (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs, map #8 xs,
- map #9 xs, map #10 xs);
+fun split_list8 xs =
+ (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs, map #8 xs);
fun resort_tfree S (TFree (s, _)) = TFree (s, S);
@@ -406,7 +405,7 @@
val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs];
- fun define_iter_rec ((selss0, discIs, sel_thmss), no_defs_lthy) =
+ fun define_iter_rec (wrap_res, no_defs_lthy) =
let
val fpT_to_C = fpT --> C;
@@ -438,10 +437,10 @@
val [iter, recx] = map (mk_iter_like As Cs o Morphism.term phi) csts;
in
- ((ctrs, selss0, iter, recx, xss, ctr_defs, discIs, sel_thmss, iter_def, rec_def), lthy)
+ ((wrap_res, ctrs, iter, recx, xss, ctr_defs, iter_def, rec_def), lthy)
end;
- fun define_coiter_corec ((selss0, discIs, sel_thmss), no_defs_lthy) =
+ fun define_coiter_corec (wrap_res, no_defs_lthy) =
let
val B_to_fpT = C --> fpT;
@@ -478,8 +477,7 @@
val [coiter, corec] = map (mk_iter_like As Cs o Morphism.term phi) csts;
in
- ((ctrs, selss0, coiter, corec, xss, ctr_defs, discIs, sel_thmss, coiter_def, corec_def),
- lthy)
+ ((wrap_res, ctrs, coiter, corec, xss, ctr_defs, coiter_def, corec_def), lthy)
end;
fun wrap lthy =
@@ -514,9 +512,13 @@
val args = map build_arg TUs;
in Term.list_comb (mapx, args) end;
- fun derive_induct_iter_rec_thms_for_types ((ctrss, _, iters, recs, xsss, ctr_defss, _, _,
+ fun derive_induct_iter_rec_thms_for_types ((wrap_ress, ctrss, iters, recs, xsss, ctr_defss,
iter_defs, rec_defs), lthy) =
let
+ val inject_thmss = map #2 wrap_ress;
+ val distinct_thmss = map #3 wrap_ress;
+ val case_thmss = map #4 wrap_ress;
+
val (((phis, phis'), vs'), names_lthy) =
lthy
|> mk_Frees' "P" (map mk_predT fpTs)
@@ -603,6 +605,7 @@
`(conj_dests nn) induct_thm
end;
+ (* TODO: Generate nicer names in case of clashes *)
val induct_cases = Datatype_Prop.indexify_names (maps (map base_name_of_ctr) ctrss);
val (iter_thmss, rec_thmss) =
@@ -653,6 +656,10 @@
goal_recss rec_tacss)
end;
+ val simp_thmss =
+ map4 (fn injects => fn distincts => fn cases => fn recs =>
+ injects @ distincts @ cases @ recs) inject_thmss distinct_thmss case_thmss rec_thmss;
+
val induct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names induct_cases));
fun induct_type_attr T_name = Attrib.internal (K (Induct.induct_type T_name));
@@ -665,7 +672,8 @@
[(inductN, map single induct_thms,
fn T_name => [induct_case_names_attr, induct_type_attr T_name]),
(itersN, iter_thmss, K simp_attrs),
- (recsN, rec_thmss, K (Code.add_default_eqn_attrib :: simp_attrs))]
+ (recsN, rec_thmss, K (Code.add_default_eqn_attrib :: simp_attrs)),
+ (simpsN, simp_thmss, K [])]
|> maps (fn (thmN, thmss, attrs) =>
map3 (fn b => fn Type (T_name, _) => fn thms =>
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs T_name),
@@ -674,9 +682,13 @@
lthy |> Local_Theory.notes (common_notes @ notes) |> snd
end;
- fun derive_coinduct_coiter_corec_thms_for_types ((ctrss, selsss, coiters, corecs, _, ctr_defss,
- discIss, sel_thmsss, coiter_defs, corec_defs), lthy) =
+ fun derive_coinduct_coiter_corec_thms_for_types ((wrap_ress, ctrss, coiters, corecs, _,
+ ctr_defss, coiter_defs, corec_defs), lthy) =
let
+ val selsss0 = map #1 wrap_ress;
+ val discIss = map #5 wrap_ress;
+ val sel_thmsss = map #6 wrap_ress;
+
val (vs', _) =
lthy
|> Variable.variant_fixes (map Binding.name_of fp_bs);
@@ -765,9 +777,9 @@
end;
val sel_coiter_thmsss =
- map3 (map3 (map2 o mk_sel_coiter_like_thm)) coiter_thmss selsss sel_thmsss;
+ map3 (map3 (map2 o mk_sel_coiter_like_thm)) coiter_thmss selsss0 sel_thmsss;
val sel_corec_thmsss =
- map3 (map3 (map2 o mk_sel_coiter_like_thm)) corec_thmss selsss sel_thmsss;
+ map3 (map3 (map2 o mk_sel_coiter_like_thm)) corec_thmss selsss0 sel_thmsss;
val common_notes =
(if nn > 1 then [(coinductN, [coinduct_thm], [])] (* FIXME: attribs *) else [])
@@ -791,7 +803,7 @@
end;
fun wrap_types_and_define_iter_likes ((wraps, define_iter_likess), lthy) =
- fold_map2 (curry (op o)) define_iter_likess wraps lthy |>> split_list10
+ fold_map2 (curry (op o)) define_iter_likess wraps lthy |>> split_list8
val lthy' = lthy
|> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Tue Sep 18 11:42:11 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Tue Sep 18 11:42:22 2012 +0200
@@ -13,7 +13,7 @@
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 list) * local_theory
+ (term list list * thm list * thm list * thm list * thm list * thm list list) * local_theory
val parse_wrap_options: bool parser
val parse_bound_term: (binding * string) parser
end;
@@ -327,6 +327,8 @@
val ([exhaust_thm], (inject_thmss, (half_distinct_thmss, [case_thms]))) =
(hd thmss, apsnd (chop (n * n)) (chop n (tl thmss)));
+ val inject_thms = flat inject_thmss;
+
val exhaust_thm' =
let val Tinst = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As) in
Drule.instantiate' [] [SOME (certify lthy v)]
@@ -571,7 +573,7 @@
(disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]),
(distinctN, distinct_thms, simp_attrs @ induct_simp_attrs),
(exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]),
- (injectN, flat inject_thmss, iff_attrs @ induct_simp_attrs),
+ (injectN, inject_thms, iff_attrs @ induct_simp_attrs),
(nchotomyN, [nchotomy_thm], []),
(selsN, all_sel_thms, simp_attrs),
(splitN, [split_thm], []),
@@ -586,7 +588,8 @@
[(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)]
|> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
in
- ((selss, discI_thms, sel_thmss), lthy |> Local_Theory.notes (notes' @ notes) |> snd)
+ ((selss, inject_thms, distinct_thms, case_thms, discI_thms, sel_thmss),
+ lthy |> Local_Theory.notes (notes' @ notes) |> snd)
end;
in
(goalss, after_qed, lthy')