# HG changeset patch # User blanchet # Date 1406154240 -7200 # Node ID 959caab43a3d2c23df6da2d5106ac3c84e4f5ca1 # Parent 04ab38720b50a9cd048c6ad0297a33ea69b41d6a use the noted theorem whenever possible, also in 'BNF_Def' diff -r 04ab38720b50 -r 959caab43a3d src/HOL/Ctr_Sugar.thy --- a/src/HOL/Ctr_Sugar.thy Thu Jul 24 00:24:00 2014 +0200 +++ b/src/HOL/Ctr_Sugar.thy Thu Jul 24 00:24:00 2014 +0200 @@ -21,6 +21,7 @@ case_cons :: "('a \ 'b) \ ('a \ 'b) \ 'a \ 'b" case_elem :: "'a \ 'b \ 'a \ 'b" case_abs :: "('c \ 'b) \ 'b" + declare [[coercion_args case_guard - + -]] declare [[coercion_args case_cons - -]] declare [[coercion_args case_abs -]] diff -r 04ab38720b50 -r 959caab43a3d src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Thu Jul 24 00:24:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Thu Jul 24 00:24:00 2014 +0200 @@ -103,7 +103,7 @@ val bnf_timing: bool Config.T val user_policy: fact_policy -> Proof.context -> fact_policy val note_bnf_thms: fact_policy -> (binding -> binding) -> binding -> bnf -> Proof.context -> - Proof.context + bnf * Proof.context val print_bnfs: Proof.context -> unit val prepare_def: inline_policy -> (Proof.context -> fact_policy) -> bool -> @@ -624,7 +624,7 @@ val smart_max_inline_term_size = 25; (*FUDGE*) -fun note_bnf_thms fact_policy qualify0 bnf_b bnf = +fun note_bnf_thms fact_policy qualify0 bnf_b bnf lthy = let val axioms = axioms_of_bnf bnf; val facts = facts_of_bnf bnf; @@ -632,61 +632,63 @@ val qualify = let val (_, qs, _) = Binding.dest bnf_b; in fold_rev (fn (s, mand) => Binding.qualify mand s) qs #> qualify0 end; - in - (if fact_policy = Note_All then + + fun note_if_note_all (noted0, lthy0) = let val witNs = if length wits = 1 then [witN] else map mk_witN (1 upto length wits); val notes = [(bd_card_orderN, [#bd_card_order axioms]), - (bd_cinfiniteN, [#bd_cinfinite axioms]), - (bd_Card_orderN, [#bd_Card_order facts]), - (bd_CinfiniteN, [#bd_Cinfinite facts]), - (bd_CnotzeroN, [#bd_Cnotzero facts]), - (collect_set_mapN, [Lazy.force (#collect_set_map facts)]), - (in_bdN, [Lazy.force (#in_bd facts)]), - (in_monoN, [Lazy.force (#in_mono facts)]), - (in_relN, [Lazy.force (#in_rel facts)]), - (inj_mapN, [Lazy.force (#inj_map facts)]), - (map_comp0N, [#map_comp0 axioms]), - (map_transferN, [Lazy.force (#map_transfer facts)]), - (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]), - (set_map0N, #set_map0 axioms), - (set_bdN, #set_bd axioms)] @ - (witNs ~~ wit_thmss_of_bnf bnf) - |> map (fn (thmN, thms) => - ((qualify (Binding.qualify true (Binding.name_of bnf_b) (Binding.name thmN)), []), - [(thms, [])])); - in - Local_Theory.notes notes #> snd - end - else - I) - #> (if fact_policy <> Dont_Note then - let - val notes = - [(map_compN, [Lazy.force (#map_comp facts)], []), - (map_cong0N, [#map_cong0 axioms], []), - (map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs), - (map_idN, [Lazy.force (#map_id facts)], []), - (map_id0N, [#map_id0 axioms], []), - (map_identN, [Lazy.force (#map_ident facts)], []), - (rel_comppN, [Lazy.force (#rel_OO facts)], []), - (rel_compp_GrpN, no_refl [#rel_OO_Grp axioms], []), - (rel_conversepN, [Lazy.force (#rel_conversep facts)], []), - (rel_eqN, [Lazy.force (#rel_eq facts)], []), - (rel_flipN, [Lazy.force (#rel_flip facts)], []), - (rel_GrpN, [Lazy.force (#rel_Grp facts)], []), - (rel_monoN, [Lazy.force (#rel_mono facts)], []), - (set_mapN, map Lazy.force (#set_map facts), [])] - |> filter_out (null o #2) - |> map (fn (thmN, thms, attrs) => - ((qualify (Binding.qualify true (Binding.name_of bnf_b) (Binding.name thmN)), - attrs), [(thms, [])])); - in - Local_Theory.notes notes #> snd - end - else - I) + (bd_cinfiniteN, [#bd_cinfinite axioms]), + (bd_Card_orderN, [#bd_Card_order facts]), + (bd_CinfiniteN, [#bd_Cinfinite facts]), + (bd_CnotzeroN, [#bd_Cnotzero facts]), + (collect_set_mapN, [Lazy.force (#collect_set_map facts)]), + (in_bdN, [Lazy.force (#in_bd facts)]), + (in_monoN, [Lazy.force (#in_mono facts)]), + (in_relN, [Lazy.force (#in_rel facts)]), + (inj_mapN, [Lazy.force (#inj_map facts)]), + (map_comp0N, [#map_comp0 axioms]), + (map_transferN, [Lazy.force (#map_transfer facts)]), + (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]), + (set_map0N, #set_map0 axioms), + (set_bdN, #set_bd axioms)] @ + (witNs ~~ wit_thmss_of_bnf bnf) + |> map (fn (thmN, thms) => + ((qualify (Binding.qualify true (Binding.name_of bnf_b) (Binding.name thmN)), []), + [(thms, [])])); + in + Local_Theory.notes notes lthy0 |>> append noted0 + end + + fun note_unless_dont_note (noted0, lthy0) = + let + val notes = + [(map_compN, [Lazy.force (#map_comp facts)], []), + (map_cong0N, [#map_cong0 axioms], []), + (map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs), + (map_idN, [Lazy.force (#map_id facts)], []), + (map_id0N, [#map_id0 axioms], []), + (map_identN, [Lazy.force (#map_ident facts)], []), + (rel_comppN, [Lazy.force (#rel_OO facts)], []), + (rel_compp_GrpN, no_refl [#rel_OO_Grp axioms], []), + (rel_conversepN, [Lazy.force (#rel_conversep facts)], []), + (rel_eqN, [Lazy.force (#rel_eq facts)], []), + (rel_flipN, [Lazy.force (#rel_flip facts)], []), + (rel_GrpN, [Lazy.force (#rel_Grp facts)], []), + (rel_monoN, [Lazy.force (#rel_mono facts)], []), + (set_mapN, map Lazy.force (#set_map facts), [])] + |> filter_out (null o #2) + |> map (fn (thmN, thms, attrs) => + ((qualify (Binding.qualify true (Binding.name_of bnf_b) (Binding.name thmN)), attrs), + [(thms, [])])); + in + Local_Theory.notes notes lthy0 |>> append noted0 + end + in + ([], lthy) + |> fact_policy = Note_All ? note_if_note_all + |> fact_policy <> Dont_Note ? note_unless_dont_note + |>> (fn [] => bnf | noted => morph_bnf (substitute_noted_thm noted) bnf) end; @@ -1339,7 +1341,7 @@ val bnf = mk_bnf bnf_b Calpha live alphas betas dead deads bnf_map bnf_sets bnf_bd axioms defs facts wits bnf_rel; in - (bnf, lthy |> note_bnf_thms fact_policy qualify bnf_b bnf) + note_bnf_thms fact_policy qualify bnf_b bnf lthy end; val one_step_defs = diff -r 04ab38720b50 -r 959caab43a3d src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Jul 24 00:24:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Jul 24 00:24:00 2014 +0200 @@ -150,7 +150,7 @@ fun register_as_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs mapss common_co_inducts co_inductss - co_rec_thmss disc_co_recss sel_co_recsss rel_injectss rel_distinctss = + co_rec_thmss disc_co_recss sel_co_recsss rel_injectss rel_distinctss noted = let val fp_sugars = map_index (fn (kk, T) => @@ -162,7 +162,8 @@ common_co_inducts = common_co_inducts, co_inducts = nth co_inductss kk, co_rec_thms = nth co_rec_thmss kk, disc_co_recs = nth disc_co_recss kk, sel_co_recss = nth sel_co_recsss kk, rel_injects = nth rel_injectss kk, - rel_distincts = nth rel_distinctss kk}) Ts + rel_distincts = nth rel_distinctss kk} + |> morph_fp_sugar (substitute_noted_thm noted)) Ts in register_fp_sugars fp_sugars end; @@ -1251,7 +1252,7 @@ end; fun derive_maps_sets_rels (ctr_sugar as {case_cong, discs, selss, ctrs, exhaust, disc_thmss, - sel_thmss, injects, distincts, ...} : ctr_sugar, lthy) = + sel_thmss, injects, distincts, ...} : ctr_sugar, lthy) = if live = 0 then ((([], [], [], []), ctr_sugar), lthy) else @@ -1630,15 +1631,19 @@ (sel_setN, sel_set_thms, []), (set_emptyN, set_empty_thms, [])] |> massage_simple_notes fp_b_name; + + val (noted, lthy') = + lthy + |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) map_thms) + |> fp = Least_FP + ? Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) rel_eq_thms) + |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) set_thms) + |> Local_Theory.notes (anonymous_notes @ notes); + + val subst = Morphism.thm (substitute_noted_thm noted); in - (((map_thms, rel_inject_thms, rel_distinct_thms, set_thmss), ctr_sugar), - lthy - |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) map_thms) - |> fp = Least_FP - ? Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) rel_eq_thms) - |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) set_thms) - |> Local_Theory.notes (anonymous_notes @ notes) - |> snd) + (((map subst map_thms, map subst rel_inject_thms, map subst rel_distinct_thms, + map (map subst) set_thmss), ctr_sugar), lthy') end; fun mk_binding pre = Binding.qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b); @@ -1709,8 +1714,8 @@ in lthy |> Spec_Rules.add Spec_Rules.Equational (recs, flat rec_thmss) - |> Local_Theory.notes (common_notes @ notes) |> snd - |> register_as_fp_sugars fpTs fpBTs Xs Least_FP pre_bnfs absT_infos fp_nesting_bnfs + |> Local_Theory.notes (common_notes @ notes) + |-> register_as_fp_sugars fpTs fpBTs Xs Least_FP pre_bnfs absT_infos fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs mapss [induct_thm] (map single induct_thms) rec_thmss (replicate nn []) (replicate nn []) rel_injectss rel_distinctss @@ -1791,11 +1796,10 @@ |> massage_multi_notes; in lthy - (* TODO: code theorems *) |> fold (curry (Spec_Rules.add Spec_Rules.Equational) corecs) [flat sel_corec_thmss, flat corec_thmss] - |> Local_Theory.notes (common_notes @ notes) |> snd - |> register_as_fp_sugars fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos fp_nesting_bnfs + |> Local_Theory.notes (common_notes @ notes) + |-> register_as_fp_sugars fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs mapss [coinduct_thm, strong_coinduct_thm] (transpose [coinduct_thms, strong_coinduct_thms]) corec_thmss disc_corec_thmss sel_corec_thmsss rel_injectss rel_distinctss diff -r 04ab38720b50 -r 959caab43a3d src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Thu Jul 24 00:24:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Thu Jul 24 00:24:00 2014 +0200 @@ -2467,64 +2467,69 @@ dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_common_notes @ Jbnf_notes, lthy) end; - val dtor_unfold_o_Jmap_thms = mk_xtor_un_fold_o_map_thms Greatest_FP false m - dtor_unfold_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_unfold_thms) - sym_map_comps map_cong0s; - val dtor_corec_o_Jmap_thms = mk_xtor_un_fold_o_map_thms Greatest_FP true m - dtor_corec_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_corec_thms) - sym_map_comps map_cong0s; + val dtor_unfold_o_Jmap_thms = mk_xtor_un_fold_o_map_thms Greatest_FP false m + dtor_unfold_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_unfold_thms) + sym_map_comps map_cong0s; + val dtor_corec_o_Jmap_thms = mk_xtor_un_fold_o_map_thms Greatest_FP true m + dtor_corec_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_corec_thms) + sym_map_comps map_cong0s; - val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs; + val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs; - val dtor_unfold_transfer_thms = - mk_un_fold_transfer_thms Greatest_FP rels activephis - (if m = 0 then map HOLogic.eq_const Ts - else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs) Jphis - (mk_unfolds passiveAs activeAs) (mk_unfolds passiveBs activeBs) - (fn {context = ctxt, prems = _} => mk_unfold_transfer_tac ctxt m Jrel_coinduct_thm - (map map_transfer_of_bnf bnfs) dtor_unfold_thms) - lthy; + val dtor_unfold_transfer_thms = + mk_un_fold_transfer_thms Greatest_FP rels activephis + (if m = 0 then map HOLogic.eq_const Ts + else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs) Jphis + (mk_unfolds passiveAs activeAs) (mk_unfolds passiveBs activeBs) + (fn {context = ctxt, prems = _} => mk_unfold_transfer_tac ctxt m Jrel_coinduct_thm + (map map_transfer_of_bnf bnfs) dtor_unfold_thms) + lthy; - val timer = time (timer "relator coinduction"); + val timer = time (timer "relator coinduction"); - val common_notes = - [(dtor_coinductN, [dtor_coinduct_thm]), - (dtor_rel_coinductN, [Jrel_coinduct_thm]), - (dtor_unfold_transferN, dtor_unfold_transfer_thms)] - |> map (fn (thmN, thms) => - ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); + val common_notes = + [(dtor_coinductN, [dtor_coinduct_thm]), + (dtor_rel_coinductN, [Jrel_coinduct_thm]), + (dtor_unfold_transferN, dtor_unfold_transfer_thms)] + |> map (fn (thmN, thms) => + ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); - val notes = - [(ctor_dtorN, ctor_dtor_thms), - (ctor_exhaustN, ctor_exhaust_thms), - (ctor_injectN, ctor_inject_thms), - (dtor_corecN, dtor_corec_thms), - (dtor_ctorN, dtor_ctor_thms), - (dtor_exhaustN, dtor_exhaust_thms), - (dtor_injectN, dtor_inject_thms), - (dtor_unfoldN, dtor_unfold_thms), - (dtor_unfold_uniqueN, dtor_unfold_unique_thms), - (dtor_corec_uniqueN, dtor_corec_unique_thms), - (dtor_unfold_o_mapN, dtor_unfold_o_Jmap_thms), - (dtor_corec_o_mapN, dtor_corec_o_Jmap_thms)] - |> map (apsnd (map single)) - |> maps (fn (thmN, thmss) => - map2 (fn b => fn thms => - ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) - bs thmss); + val notes = + [(ctor_dtorN, ctor_dtor_thms), + (ctor_exhaustN, ctor_exhaust_thms), + (ctor_injectN, ctor_inject_thms), + (dtor_corecN, dtor_corec_thms), + (dtor_ctorN, dtor_ctor_thms), + (dtor_exhaustN, dtor_exhaust_thms), + (dtor_injectN, dtor_inject_thms), + (dtor_unfoldN, dtor_unfold_thms), + (dtor_unfold_uniqueN, dtor_unfold_unique_thms), + (dtor_corec_uniqueN, dtor_corec_unique_thms), + (dtor_unfold_o_mapN, dtor_unfold_o_Jmap_thms), + (dtor_corec_o_mapN, dtor_corec_o_Jmap_thms)] + |> map (apsnd (map single)) + |> maps (fn (thmN, thmss) => + map2 (fn b => fn thms => + ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) + bs thmss); (*FIXME: once the package exports all the necessary high-level characteristic theorems, those should not only be concealed but rather not noted at all*) val maybe_conceal_notes = note_all = false ? map (apfst (apfst Binding.conceal)); + + val (noted, lthy') = + lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Jbnf_notes)); + + val fp_res = + {Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_co_recs = corecs, + xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, + ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, + xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss', + xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms, + xtor_co_rec_o_map_thms = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm} + |> morph_fp_result (substitute_noted_thm noted); in - timer; - ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_co_recs = corecs, - xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms, - ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, - xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss', - xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms, - xtor_co_rec_o_map_thms = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm}, - lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Jbnf_notes)) |> snd) + timer; (fp_res, lthy') end; val _ = diff -r 04ab38720b50 -r 959caab43a3d src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Thu Jul 24 00:24:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Thu Jul 24 00:24:00 2014 +0200 @@ -1752,67 +1752,72 @@ ctor_Irel_thms, Ibnf_common_notes @ Ibnf_notes, lthy) end; - val ctor_fold_o_Imap_thms = mk_xtor_un_fold_o_map_thms Least_FP false m ctor_fold_unique_thm - ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_fold_thms) sym_map_comps map_cong0s; - val ctor_rec_o_Imap_thms = mk_xtor_un_fold_o_map_thms Least_FP true m ctor_rec_unique_thm - ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_rec_thms) sym_map_comps map_cong0s; + val ctor_fold_o_Imap_thms = mk_xtor_un_fold_o_map_thms Least_FP false m ctor_fold_unique_thm + ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_fold_thms) sym_map_comps map_cong0s; + val ctor_rec_o_Imap_thms = mk_xtor_un_fold_o_map_thms Least_FP true m ctor_rec_unique_thm + ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_rec_thms) sym_map_comps map_cong0s; - val Irels = if m = 0 then map HOLogic.eq_const Ts - else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs; - val Irel_induct_thm = - mk_rel_xtor_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's - (fn {context = ctxt, prems = IHs} => mk_rel_induct_tac ctxt IHs m ctor_induct2_thm ks - ctor_Irel_thms rel_mono_strongs) lthy; + val Irels = if m = 0 then map HOLogic.eq_const Ts + else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs; + val Irel_induct_thm = + mk_rel_xtor_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's + (fn {context = ctxt, prems = IHs} => mk_rel_induct_tac ctxt IHs m ctor_induct2_thm ks + ctor_Irel_thms rel_mono_strongs) lthy; - val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs; - val ctor_fold_transfer_thms = - mk_un_fold_transfer_thms Least_FP rels activephis Irels Iphis - (mk_folds passiveAs activeAs) (mk_folds passiveBs activeBs) - (fn {context = ctxt, prems = _} => mk_fold_transfer_tac ctxt m Irel_induct_thm - (map map_transfer_of_bnf bnfs) ctor_fold_thms) - lthy; + val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs; + val ctor_fold_transfer_thms = + mk_un_fold_transfer_thms Least_FP rels activephis Irels Iphis + (mk_folds passiveAs activeAs) (mk_folds passiveBs activeBs) + (fn {context = ctxt, prems = _} => mk_fold_transfer_tac ctxt m Irel_induct_thm + (map map_transfer_of_bnf bnfs) ctor_fold_thms) + lthy; - val timer = time (timer "relator induction"); + val timer = time (timer "relator induction"); - val common_notes = - [(ctor_inductN, [ctor_induct_thm]), - (ctor_induct2N, [ctor_induct2_thm]), - (ctor_fold_transferN, ctor_fold_transfer_thms), - (ctor_rel_inductN, [Irel_induct_thm])] - |> map (fn (thmN, thms) => - ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); + val common_notes = + [(ctor_inductN, [ctor_induct_thm]), + (ctor_induct2N, [ctor_induct2_thm]), + (ctor_fold_transferN, ctor_fold_transfer_thms), + (ctor_rel_inductN, [Irel_induct_thm])] + |> map (fn (thmN, thms) => + ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); - val notes = - [(ctor_dtorN, ctor_dtor_thms), - (ctor_exhaustN, ctor_exhaust_thms), - (ctor_foldN, ctor_fold_thms), - (ctor_fold_uniqueN, ctor_fold_unique_thms), - (ctor_rec_uniqueN, ctor_rec_unique_thms), - (ctor_fold_o_mapN, ctor_fold_o_Imap_thms), - (ctor_rec_o_mapN, ctor_rec_o_Imap_thms), - (ctor_injectN, ctor_inject_thms), - (ctor_recN, ctor_rec_thms), - (dtor_ctorN, dtor_ctor_thms), - (dtor_exhaustN, dtor_exhaust_thms), - (dtor_injectN, dtor_inject_thms)] - |> map (apsnd (map single)) - |> maps (fn (thmN, thmss) => - map2 (fn b => fn thms => - ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) - bs thmss); + val notes = + [(ctor_dtorN, ctor_dtor_thms), + (ctor_exhaustN, ctor_exhaust_thms), + (ctor_foldN, ctor_fold_thms), + (ctor_fold_uniqueN, ctor_fold_unique_thms), + (ctor_rec_uniqueN, ctor_rec_unique_thms), + (ctor_fold_o_mapN, ctor_fold_o_Imap_thms), + (ctor_rec_o_mapN, ctor_rec_o_Imap_thms), + (ctor_injectN, ctor_inject_thms), + (ctor_recN, ctor_rec_thms), + (dtor_ctorN, dtor_ctor_thms), + (dtor_exhaustN, dtor_exhaust_thms), + (dtor_injectN, dtor_inject_thms)] + |> map (apsnd (map single)) + |> maps (fn (thmN, thmss) => + map2 (fn b => fn thms => + ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) + bs thmss); (*FIXME: once the package exports all the necessary high-level characteristic theorems, those should not only be concealed but rather not noted at all*) val maybe_conceal_notes = note_all = false ? map (apfst (apfst Binding.conceal)); + + val (noted, lthy') = + lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Ibnf_notes)); + + val fp_res = + {Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_recs = recs, + xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, + ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, + xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss', + xtor_rel_thms = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms, + xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm} + |> morph_fp_result (substitute_noted_thm noted); in - timer; - ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_recs = recs, - xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, - ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, - xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss', - xtor_rel_thms = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms, - xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm}, - lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Ibnf_notes)) |> snd) + timer; (fp_res, lthy') end; val _ = diff -r 04ab38720b50 -r 959caab43a3d src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Thu Jul 24 00:24:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Thu Jul 24 00:24:00 2014 +0200 @@ -354,14 +354,19 @@ (sizeN, size_thmss, code_nitpicksimp_simp_attrs), (size_o_mapN, size_o_map_thmss, [])] |> massage_multi_notes; + + val (noted, lthy3) = + lthy2 + |> Spec_Rules.add Spec_Rules.Equational (size_consts, size_simps) + |> Local_Theory.notes notes; + + val phi0 = substitute_noted_thm noted; in - lthy2 - |> Local_Theory.notes notes |> snd - |> Spec_Rules.add Spec_Rules.Equational (size_consts, size_simps) + lthy3 |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Data.map (fold2 (fn T_name => fn Const (size_name, _) => Symtab.update (T_name, (size_name, - pairself (map (Morphism.thm phi)) (size_simps, flat size_o_map_thmss)))) + pairself (map (Morphism.thm (phi0 $> phi))) (size_simps, flat size_o_map_thmss)))) T_names size_consts)) end; diff -r 04ab38720b50 -r 959caab43a3d src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Thu Jul 24 00:24:00 2014 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Thu Jul 24 00:24:00 2014 +0200 @@ -1011,7 +1011,7 @@ (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms) (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms)) I) - |> Local_Theory.notes (anonymous_notes @ notes) + |> Local_Theory.notes (anonymous_notes @ notes); val ctr_sugar = {ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm, diff -r 04ab38720b50 -r 959caab43a3d src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Thu Jul 24 00:24:00 2014 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Thu Jul 24 00:24:00 2014 +0200 @@ -239,7 +239,7 @@ fun substitute_noted_thm noted = let val tab = fold (fold (Termtab.default o `Thm.full_prop_of) o snd) noted Termtab.empty in Morphism.thm_morphism "Ctr_Sugar_Util.substitute_noted_thm" - (perhaps (Termtab.lookup tab o Thm.full_prop_of)) + (perhaps (Termtab.lookup tab o Thm.full_prop_of) o Drule.zero_var_indexes) end (* The standard binding stands for a name generated following the canonical convention (e.g.,