# HG changeset patch
# User traytel
# Date 1499801802 -7200
# Node ID c6714a9562aef0a7f7c7c4533f03d43094aa8f05
# Parent  d157195a468a0cf55cc095c5b09d5804652ad7fa
store the unfolded definitions of the lifted bnf constants under "_def" name

diff -r d157195a468a -r c6714a9562ae src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Tue Jul 11 20:47:19 2017 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Tue Jul 11 21:36:42 2017 +0200
@@ -143,8 +143,9 @@
   val bnf_internals: bool Config.T
   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 ->
-    bnf * Proof.context
+  val note_bnf_thms: fact_policy -> (binding -> binding) -> binding -> bnf -> local_theory ->
+    bnf * local_theory
+  val note_bnf_defs: bnf -> local_theory -> bnf * local_theory
 
   val print_bnfs: Proof.context -> unit
   val prepare_def: inline_policy -> (Proof.context -> fact_policy) -> bool ->
@@ -983,6 +984,22 @@
     |>> (fn [] => bnf | noted => morph_bnf (substitute_noted_thm noted) bnf)
   end;
 
+fun note_bnf_defs bnf lthy =
+  let
+    fun mk_def_binding cst_of =
+      Thm.def_binding (Binding.qualified_name (dest_Const (cst_of bnf) |> fst));
+    val notes =
+      [(mk_def_binding map_of_bnf, map_def_of_bnf bnf),
+       (mk_def_binding rel_of_bnf, rel_def_of_bnf bnf),
+       (mk_def_binding pred_of_bnf, pred_def_of_bnf bnf)] @
+      @{map 2} (pair o mk_def_binding o K) (sets_of_bnf bnf) (set_defs_of_bnf bnf)
+      |> map (fn (b, thm) => ((b, []), [([thm], [])]));
+  in
+    lthy
+    |> Local_Theory.notes notes
+    |>> (fn noted => morph_bnf (substitute_noted_thm noted) bnf)
+  end;
+
 fun mk_wit_goals zs bs sets (I, wit) =
   let
     val xs = map (nth bs) I;
diff -r d157195a468a -r c6714a9562ae src/HOL/Tools/BNF/bnf_lift.ML
--- a/src/HOL/Tools/BNF/bnf_lift.ML	Tue Jul 11 20:47:19 2017 +0200
+++ b/src/HOL/Tools/BNF/bnf_lift.ML	Tue Jul 11 21:36:42 2017 +0200
@@ -326,12 +326,14 @@
               [card_order_bd_tac, cinfinite_bd_tac] @ set_bds_tac @
               [le_rel_OO_tac, rel_OO_Grp_tac, pred_set_tac];
 
-            val (bnf, lthy) = bnf_def Dont_Inline (user_policy Note_Some) false I
+            val (bnf, lthy) = bnf_def Dont_Inline (user_policy Note_Some) true I
               tactics wit_tac NONE map_b rel_b pred_b set_bs
               (((((((Binding.empty, AbsT), map_G), sets_G), bd_G), wits_G), SOME rel_G), SOME pred_G)
               lthy;
 
-            val bnf = morph_bnf_defs (Morphism.thm_morphism "BNF" (unfold_thms lthy defs)) bnf;
+            val (bnf, lthy) =
+              morph_bnf_defs (Morphism.thm_morphism "BNF" (unfold_thms lthy defs)) bnf
+              |> (fn bnf => note_bnf_defs bnf lthy);
           in
             lthy |> BNF_Def.register_bnf plugins AbsT_name bnf
           end