# HG changeset patch
# User traytel
# Date 1374577827 -7200
# Node ID fdc04f9bf906bd67fea35caff21115bd419705ec
# Parent  480a3479fa470deb3e1c99e7c84c7dea8728ade4
separate ML interface to note facts of a bnf

diff -r 480a3479fa47 -r fdc04f9bf906 src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Mon Jul 22 21:12:15 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Tue Jul 23 13:10:27 2013 +0200
@@ -88,6 +88,8 @@
 
   val bnf_note_all: 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
 
   val print_bnfs: Proof.context -> unit
   val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
@@ -522,6 +524,67 @@
 
 val smart_max_inline_size = 25; (*FUDGE*)
 
+fun note_bnf_thms fact_policy qualify b bnf =
+  let
+    val axioms = axioms_of_bnf bnf;
+    val facts = facts_of_bnf bnf;
+    val wits = wits_of_bnf bnf;
+  in
+    (if fact_policy = Note_All then
+      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)]),
+            (map_compN, [#map_comp axioms]),
+            (map_idN, [#map_id axioms]),
+            (map_transferN, [Lazy.force (#map_transfer facts)]),
+            (map_wpullN, [#map_wpull axioms]),
+            (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]),
+            (set_mapN, #set_map axioms),
+            (set_bdN, #set_bd axioms)] @
+            (witNs ~~ wit_thmss_of_bnf bnf)
+            |> map (fn (thmN, thms) =>
+              ((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)), []),
+              [(thms, [])]));
+        in
+          Local_Theory.notes notes #> snd
+        end
+      else
+        I)
+    #> (if fact_policy <> Dont_Note then
+        let
+          val notes =
+            [(map_comp'N, [Lazy.force (#map_comp' facts)], []),
+            (map_cong0N, [#map_cong0 axioms], []),
+            (map_congN, [Lazy.force (#map_cong facts)], fundef_cong_attrs),
+            (map_id'N, [Lazy.force (#map_id' facts)], []),
+            (rel_eqN, [Lazy.force (#rel_eq facts)], []),
+            (rel_flipN, [Lazy.force (#rel_flip facts)], []),
+            (set_map'N, map Lazy.force (#set_map' facts), []),
+            (rel_OO_GrpN, no_refl [#rel_OO_Grp axioms], []),
+            (rel_GrpN, [Lazy.force (#rel_Grp facts)], []),
+            (rel_conversepN, [Lazy.force (#rel_conversep facts)], []),
+            (rel_monoN, [Lazy.force (#rel_mono facts)], []),
+            (rel_OON, [Lazy.force (#rel_OO facts)], [])]
+            |> filter_out (null o #2)
+            |> map (fn (thmN, thms, attrs) =>
+              ((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)),
+                attrs), [(thms, [])]));
+        in
+          Local_Theory.notes notes #> snd
+        end
+      else
+        I)
+  end;
+
 
 (* Define new BNFs *)
 
@@ -1173,60 +1236,7 @@
         val bnf = mk_bnf b CA live alphas betas dead deads bnf_map bnf_sets bnf_bd axioms defs facts
           wits bnf_rel;
       in
-        (bnf, lthy
-          |> (if fact_policy = Note_All then
-                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)]),
-                    (map_compN, [#map_comp axioms]),
-                    (map_idN, [#map_id axioms]),
-                    (map_transferN, [Lazy.force (#map_transfer facts)]),
-                    (map_wpullN, [#map_wpull axioms]),
-                    (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]),
-                    (set_mapN, #set_map axioms),
-                    (set_bdN, #set_bd axioms)] @
-                    (witNs ~~ wit_thms)
-                    |> map (fn (thmN, thms) =>
-                      ((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)), []),
-                      [(thms, [])]));
-                in
-                  Local_Theory.notes notes #> snd
-                end
-              else
-                I)
-          |> (if fact_policy <> Dont_Note then
-                let
-                  val notes =
-                    [(map_comp'N, [Lazy.force (#map_comp' facts)], []),
-                    (map_cong0N, [#map_cong0 axioms], []),
-                    (map_congN, [Lazy.force (#map_cong facts)], fundef_cong_attrs),
-                    (map_id'N, [Lazy.force (#map_id' facts)], []),
-                    (rel_eqN, [Lazy.force (#rel_eq facts)], []),
-                    (rel_flipN, [Lazy.force (#rel_flip facts)], []),
-                    (set_map'N, map Lazy.force (#set_map' facts), []),
-                    (rel_OO_GrpN, rel_OO_Grps, []),
-                    (rel_GrpN, [Lazy.force (#rel_Grp facts)], []),
-                    (rel_conversepN, [Lazy.force (#rel_conversep facts)], []),
-                    (rel_monoN, [Lazy.force (#rel_mono facts)], []),
-                    (rel_OON, [Lazy.force (#rel_OO facts)], [])]
-                    |> filter_out (null o #2)
-                    |> map (fn (thmN, thms, attrs) =>
-                      ((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)),
-                        attrs), [(thms, [])]));
-                in
-                  Local_Theory.notes notes #> snd
-                end
-              else
-                I))
+        (bnf, lthy |> note_bnf_thms fact_policy qualify b bnf)
       end;
 
     val one_step_defs =