--- a/src/HOL/BNF_LFP.thy Tue Apr 01 10:51:29 2014 +0200
+++ b/src/HOL/BNF_LFP.thy Tue Apr 01 10:51:29 2014 +0200
@@ -19,8 +19,7 @@
lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
by blast
-lemma image_Collect_subsetI:
- "(\<And>x. P x \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` {x. P x} \<subseteq> B"
+lemma image_Collect_subsetI: "(\<And>x. P x \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` {x. P x} \<subseteq> B"
by blast
lemma Collect_restrict: "{x. x \<in> X \<and> P x} \<subseteq> X"
--- a/src/HOL/Tools/BNF/bnf_def.ML Tue Apr 01 10:51:29 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Tue Apr 01 10:51:29 2014 +0200
@@ -14,7 +14,8 @@
val morph_bnf: morphism -> bnf -> bnf
val morph_bnf_defs: morphism -> bnf -> bnf
val bnf_of: Proof.context -> string -> bnf option
- val register_bnf: string -> (bnf * local_theory) -> (bnf * local_theory)
+ val bnf_interpretation: (bnf -> theory -> theory) -> theory -> theory
+ val register_bnf: string -> bnf -> local_theory -> local_theory
val name_of_bnf: bnf -> binding
val T_of_bnf: bnf -> typ
@@ -22,6 +23,7 @@
val lives_of_bnf: bnf -> typ list
val dead_of_bnf: bnf -> int
val deads_of_bnf: bnf -> typ list
+ val bd_of_bnf: bnf -> term
val nwits_of_bnf: bnf -> int
val mapN: string
@@ -1307,9 +1309,18 @@
(key, goals, wit_goalss, after_qed, lthy, one_step_defs)
end;
-fun register_bnf key (bnf, lthy) =
- (bnf, Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf))) lthy);
+structure BNF_Interpretation = Interpretation
+(
+ type T = bnf;
+ val eq: T * T -> bool = op = o pairself T_of_bnf;
+);
+
+val bnf_interpretation = BNF_Interpretation.interpretation;
+
+fun register_bnf key bnf =
+ Local_Theory.declaration {syntax = false, pervasive = true}
+ (fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf)))
+ #> Local_Theory.background_theory (BNF_Interpretation.data bnf);
fun bnf_def const_policy fact_policy internal qualify tacs wit_tac Ds map_b rel_b set_bs =
(fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) =>
@@ -1348,7 +1359,7 @@
| SOME tac => (mk_triv_wit_thms tac, []));
in
Proof.unfolding ([[(defs, [])]])
- (Proof.theorem NONE (snd o register_bnf key oo after_qed mk_wit_thms)
+ (Proof.theorem NONE (uncurry (register_bnf key) oo after_qed mk_wit_thms)
(map (single o rpair []) goals @ nontriv_wit_goals) lthy)
end) oo prepare_def Do_Inline (user_policy Note_Some) false I Syntax.read_typ Syntax.read_term
NONE Binding.empty Binding.empty [];
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Tue Apr 01 10:51:29 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Tue Apr 01 10:51:29 2014 +0200
@@ -2436,7 +2436,7 @@
fn consts => fn lthy =>
bnf_def Hardly_Inline (user_policy Note_Some) false I tacs (wit_tac wit_thms)
(SOME deads) map_b rel_b set_bs consts lthy
- |> register_bnf (Local_Theory.full_name lthy b))
+ |> (fn (bnf, lthy) => (bnf, register_bnf (Local_Theory.full_name lthy b) bnf lthy)))
bs tacss map_bs rel_bs set_bss wit_thmss
((((((bs ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~ all_witss) ~~ map SOME Jrels)
lthy;
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Tue Apr 01 10:51:29 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Tue Apr 01 10:51:29 2014 +0200
@@ -1675,7 +1675,7 @@
fold_map6 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn consts => fn lthy =>
bnf_def Do_Inline (user_policy Note_Some) false I tacs wit_tac (SOME deads)
map_b rel_b set_bs consts lthy
- |> register_bnf (Local_Theory.full_name lthy b))
+ |> (fn (bnf, lthy) => (bnf, register_bnf (Local_Theory.full_name lthy b) bnf lthy)))
bs tacss map_bs rel_bs set_bss
((((((bs ~~ Ts) ~~ Imaps) ~~ Isetss_by_bnf) ~~ Ibds) ~~ Iwitss) ~~ map SOME Irels)
lthy;