--- 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 \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
case_elem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"
case_abs :: "('c \<Rightarrow> 'b) \<Rightarrow> 'b"
+
declare [[coercion_args case_guard - + -]]
declare [[coercion_args case_cons - -]]
declare [[coercion_args case_abs -]]
--- 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 =
--- 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
--- 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 _ =
--- 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 _ =
--- 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;
--- 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,
--- 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.,