# HG changeset patch
# User blanchet
# Date 1396342289 -7200
# Node ID 42533f8f4729e4f3c58017fa140cccddffe630b1
# Parent  228e30cb111d86bb53a1ddfaef307de0484f9d67
added BNF interpretation hook

diff -r 228e30cb111d -r 42533f8f4729 src/HOL/BNF_LFP.thy
--- 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"
diff -r 228e30cb111d -r 42533f8f4729 src/HOL/Tools/BNF/bnf_def.ML
--- 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 [];
diff -r 228e30cb111d -r 42533f8f4729 src/HOL/Tools/BNF/bnf_gfp.ML
--- 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;
diff -r 228e30cb111d -r 42533f8f4729 src/HOL/Tools/BNF/bnf_lfp.ML
--- 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;