--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Jun 16 17:52:33 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Jun 16 19:18:10 2014 +0200
@@ -26,7 +26,7 @@
val transfer_lfp_sugar_thms: Proof.context -> lfp_sugar_thms -> lfp_sugar_thms
type gfp_sugar_thms =
- ((thm list * thm) list * Args.src list)
+ ((thm list * thm) list * (Args.src list * Args.src list))
* (thm list list * Args.src list)
* (thm list list * Args.src list)
* (thm list list * Args.src list)
@@ -280,17 +280,17 @@
morph_lfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
type gfp_sugar_thms =
- ((thm list * thm) list * Args.src list)
+ ((thm list * thm) list * (Args.src list * Args.src list))
* (thm list list * Args.src list)
* (thm list list * Args.src list)
* (thm list list * Args.src list)
* (thm list list list * Args.src list);
-fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs),
+fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs_pair),
(corecss, corec_attrs), (disc_corecss, disc_corec_attrs),
(disc_corec_iffss, disc_corec_iff_attrs), (sel_corecsss, sel_corec_attrs)) =
((map (apfst (map (Morphism.thm phi)) o apsnd (Morphism.thm phi)) coinducts_pairs,
- coinduct_attrs),
+ coinduct_attrs_pair),
(map (map (Morphism.thm phi)) corecss, corec_attrs),
(map (map (Morphism.thm phi)) disc_corecss, disc_corec_attrs),
(map (map (Morphism.thm phi)) disc_corec_iffss, disc_corec_iff_attrs),
@@ -688,18 +688,20 @@
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation;
- fun postproc nn thm =
- Thm.permute_prems 0 nn
- (if nn = 1 then thm RS mp else funpow nn (fn thm => reassoc_conjs (thm RS mp_conj)) thm)
- |> Drule.zero_var_indexes
- |> `(conj_dests nn);
+ val postproc =
+ Drule.zero_var_indexes
+ #> `(conj_dests nn)
+ #>> map (fn thm => Thm.permute_prems 0 nn (thm RS mp))
+ ##> (fn thm => Thm.permute_prems 0 nn
+ (if nn = 1 then thm RS mp
+ else funpow nn (fn thm => reassoc_conjs (thm RS mp_conj)) thm));
val rel_eqs = map rel_eq_of_bnf pre_bnfs;
val rel_monos = map rel_mono_of_bnf pre_bnfs;
val dtor_coinducts =
[dtor_coinduct, mk_strong_coinduct_thm dtor_coinduct rel_eqs rel_monos mk_vimage2p lthy]
in
- map2 (postproc nn oo prove) dtor_coinducts goals
+ map2 (postproc oo prove) dtor_coinducts goals
end;
fun mk_coinduct_concls ms discs ctrs =
@@ -809,16 +811,21 @@
val sel_corec_thmsss = mk_sel_corec_thms corec_thmss;
- val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
+ val common_coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
+ val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
+
val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases));
val coinduct_case_concl_attrs =
map2 (fn casex => fn concls =>
Attrib.internal (K (Rule_Cases.case_conclusion (casex, concls))))
coinduct_cases coinduct_conclss;
- val coinduct_case_attrs =
+
+ val common_coinduct_attrs =
+ common_coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
+ val coinduct_attrs =
coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
in
- ((coinduct_thms_pairs, coinduct_case_attrs),
+ ((coinduct_thms_pairs, (coinduct_attrs, common_coinduct_attrs)),
(corec_thmss, code_nitpicksimp_attrs),
(disc_corec_thmss, []),
(disc_corec_iff_thmss, simp_attrs),
@@ -1176,7 +1183,7 @@
||>> mk_TFrees (live_of_bnf fp_bnf)
||>> mk_TFrees (live_of_bnf fp_bnf);
val TA as Type (_, ADs) = mk_T_of_bnf Ds As fp_bnf;
- val TB as Type (_, BDs) = mk_T_of_bnf Ds Bs fp_bnf;
+ val Type (_, BDs) = mk_T_of_bnf Ds Bs fp_bnf;
val fTs = map2 (curry op -->) As Bs;
val ((fs, ta), names_lthy) = names_lthy
|> mk_Frees "f" fTs
@@ -1466,7 +1473,7 @@
(corecs, corec_defs)), lthy) =
let
val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)],
- coinduct_attrs),
+ (coinduct_attrs, common_coinduct_attrs)),
(corec_thmss, corec_attrs), (disc_corec_thmss, disc_corec_attrs),
(disc_corec_iff_thmss, disc_corec_iff_attrs), (sel_corec_thmsss, sel_corec_attrs)) =
derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct
@@ -1487,8 +1494,8 @@
val common_notes =
(if nn > 1 then
- [(coinductN, [coinduct_thm], coinduct_attrs),
- (strong_coinductN, [strong_coinduct_thm], coinduct_attrs)]
+ [(coinductN, [coinduct_thm], common_coinduct_attrs),
+ (strong_coinductN, [strong_coinduct_thm], common_coinduct_attrs)]
else
[])
|> massage_simple_notes fp_common_name;
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Jun 16 17:52:33 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Jun 16 19:18:10 2014 +0200
@@ -262,17 +262,16 @@
val name_of_ctr = name_of_const "constructor";
val notN = "not_";
-val eqN = "eq_";
-val neqN = "neq_";
+val isN = "is_";
fun name_of_disc t =
(case head_of t of
Abs (_, _, @{const Not} $ (t' $ Bound 0)) =>
Long_Name.map_base_name (prefix notN) (name_of_disc t')
| Abs (_, _, Const (@{const_name HOL.eq}, _) $ Bound 0 $ t') =>
- Long_Name.map_base_name (prefix eqN) (name_of_disc t')
+ Long_Name.map_base_name (prefix isN) (name_of_disc t')
| Abs (_, _, @{const Not} $ (Const (@{const_name HOL.eq}, _) $ Bound 0 $ t')) =>
- Long_Name.map_base_name (prefix neqN) (name_of_disc t')
+ Long_Name.map_base_name (prefix (notN ^ isN)) (name_of_disc t')
| t' => name_of_const "destructor" t');
val base_name_of_ctr = Long_Name.base_name o name_of_ctr;