separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)

--- a/src/HOL/Codatatype/Basic_BNFs.thy	Tue Sep 18 03:33:53 2012 +0200
+++ b/src/HOL/Codatatype/Basic_BNFs.thy	Tue Sep 18 09:15:53 2012 +0200
@@ -24,7 +24,7 @@
 lemma natLeq_cinfinite: "cinfinite natLeq"
 unfolding cinfinite_def Field_natLeq by (rule nat_infinite)
 
-bnf_def ID = "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"]
+bnf_def ID: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"]
 apply auto
 apply (rule natLeq_card_order)
 apply (rule natLeq_cinfinite)
@@ -52,7 +52,7 @@
 lemma ID_pred[simp]: "ID_pred \<phi> = \<phi>"
 unfolding ID_pred_def ID_rel_def Gr_def fun_eq_iff by auto
 
-bnf_def DEADID = "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"]
+bnf_def DEADID: "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"]
 apply (auto simp add: wpull_id)
 apply (rule card_order_csum)
 apply (rule natLeq_card_order)
@@ -86,8 +86,8 @@
 structure Basic_BNFs : BASIC_BNFS =
 struct
 
-val ID_bnf = the (BNF_Def.bnf_of @{context} "ID");
-val DEADID_bnf = the (BNF_Def.bnf_of @{context} "DEADID");
+val ID_bnf = the (BNF_Def.bnf_of @{context} "Basic_BNFs.ID");
+val DEADID_bnf = the (BNF_Def.bnf_of @{context} "Basic_BNFs.DEADID");
 
 val rel_def = BNF_Def.rel_def_of_bnf ID_bnf;
 val ID_rel_def = rel_def RS sym;
@@ -104,7 +104,7 @@
 
 lemmas sum_set_defs = sum_setl_def[abs_def] sum_setr_def[abs_def]
 
-bnf_def sum = sum_map [sum_setl, sum_setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr]
+bnf_def sum_map [sum_setl, sum_setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr]
 proof -
   show "sum_map id id = id" by (rule sum_map.id)
 next
@@ -240,7 +240,7 @@
 
 lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
 
-bnf_def prod = map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair]
+bnf_def map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair]
 proof (unfold prod_set_defs)
   show "map_pair id id = id" by (rule map_pair.id)
 next
@@ -358,7 +358,7 @@
   ultimately show ?thesis using card_of_ordLeq by fast
 qed
 
-bnf_def "fun" = "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|"
+bnf_def "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|"
   ["%c x::'b::type. c::'a::type"]
 proof
   fix f show "id \<circ> f = id f" by simp

--- a/src/HOL/Codatatype/More_BNFs.thy	Tue Sep 18 03:33:53 2012 +0200
+++ b/src/HOL/Codatatype/More_BNFs.thy	Tue Sep 18 09:15:53 2012 +0200
@@ -22,7 +22,7 @@
 lemma option_rec_conv_option_case: "option_rec = option_case"
 by (simp add: fun_eq_iff split: option.split)
 
-bnf_def option = Option.map [Option.set] "\<lambda>_::'a option. natLeq" ["None"]
+bnf_def Option.map [Option.set] "\<lambda>_::'a option. natLeq" ["None"]
 proof -
   show "Option.map id = id" by (simp add: fun_eq_iff Option.map_def split: option.split)
 next
@@ -190,7 +190,7 @@
   qed
 qed
 
-bnf_def list = map [set] "\<lambda>_::'a list. natLeq" ["[]"]
+bnf_def map [set] "\<lambda>_::'a list. natLeq" ["[]"]
 proof -
   show "map id = id" by (rule List.map.id)
 next
@@ -355,7 +355,7 @@
 lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A"
 by (rule f_the_inv_into_f) (auto simp: inj_on_def fset_cong dest!: finite_ex_fset)
 
-bnf_def fset = map_fset [fset] "\<lambda>_::'a fset. natLeq" ["{||}"]
+bnf_def map_fset [fset] "\<lambda>_::'a fset. natLeq" ["{||}"]
 proof -
   show "map_fset id = id"
   unfolding map_fset_def2 map_id o_id afset_rfset_id ..
@@ -511,7 +511,7 @@
   finally show ?thesis .
 qed
 
-bnf_def cset = cIm [rcset] "\<lambda>_::'a cset. natLeq" ["cEmp"]
+bnf_def cIm [rcset] "\<lambda>_::'a cset. natLeq" ["cEmp"]
 proof -
   show "cIm id = id" unfolding cIm_def[abs_def] id_def by auto
 next
@@ -1134,7 +1134,7 @@
 definition mset_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
 "mset_map h = Abs_multiset \<circ> mmap h \<circ> count"
 
-bnf_def mset = mset_map [set_of] "\<lambda>_::'a multiset. natLeq" ["{#}"]
+bnf_def mset_map [set_of] "\<lambda>_::'a multiset. natLeq" ["{#}"]
 unfolding mset_map_def
 proof -
   show "Abs_multiset \<circ> mmap id \<circ> count = id" unfolding mmap_id by (auto simp: count_inverse)

--- a/src/HOL/Codatatype/Tools/bnf_def.ML	Tue Sep 18 03:33:53 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Tue Sep 18 09:15:53 2012 +0200
@@ -12,6 +12,8 @@
   type nonemptiness_witness = {I: int list, wit: term, prop: thm list}
 
   val bnf_of: Proof.context -> string -> BNF option
+  val register_bnf: string -> (BNF * local_theory) -> (BNF * local_theory)
+
   val name_of_bnf: BNF -> binding
   val T_of_bnf: BNF -> typ
   val live_of_bnf: BNF -> int
@@ -540,6 +542,18 @@
     | _ => error "Bad bound constant");
     val wit_rhss = map (prep_term no_defs_lthy) raw_wits;
 
+    fun err T =
+      error ("Trying to register the type " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^
+        " as unnamed BNF");
+
+    val (b, key) =
+      if Binding.eq_name (b, Binding.empty) then
+        (case bd_rhsT of
+          Type (C, Ts) => if forall (is_some o try dest_TFree) Ts
+            then (Binding.qualified_name C, C) else err bd_rhsT
+        | T => err T)
+      else (b, Local_Theory.full_name no_defs_lthy b);
+
     val map_bind_def = (fn () => Binding.suffix_name ("_" ^ mapN) b, map_rhs);
     val set_binds_defs =
       let
@@ -624,12 +638,6 @@
     | SOME Ds => map (Morphism.typ phi) Ds);
     val dead = length deads;
 
-    (*FIXME: check DUP here, not in after_qed*)
-    val key =
-      (case (CA, Binding.eq_name (qualify b, b)) of
-        (Type (C, _), true) => C
-      | _ => Name_Space.full_name Name_Space.default_naming b);
-
     (*TODO: further checks of type of bnf_map*)
     (*TODO: check types of bnf_sets*)
     (*TODO: check type of bnf_bd*)
@@ -1152,18 +1160,20 @@
                       [(thms, [])]));
                 in
                   Local_Theory.notes notes #> snd
-                  #> Local_Theory.declaration {syntax = false, pervasive = true}
-                    (fn phi => Data.map (Symtab.update_new (key, morph_bnf phi bnf)))
                 end
               else
                 I))
       end;
   in
-    (goals, wit_goalss, after_qed, lthy', one_step_defs)
+    (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_new (key, morph_bnf phi bnf))) lthy);
+
 fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds =
-  (fn (goals, wit_goalss, after_qed, lthy, defs) =>
+  (fn (_, goals, wit_goalss, after_qed, lthy, defs) =>
   let
     val wits_tac = K (TRYALL Goal.conjunction_tac) THEN' unfold_defs_tac lthy defs wit_tac;
     val wit_goals = wit_goalss |> map Logic.mk_conjunction_balanced;
@@ -1179,9 +1189,9 @@
     |> (fn thms => after_qed (map single thms @ wit_thms) lthy)
   end) oo prepare_def const_policy fact_policy qualify (K I) Ds;
 
-val bnf_def_cmd = (fn (goals, wit_goals, after_qed, lthy, defs) =>
+val bnf_def_cmd = (fn (key, goals, wit_goals, after_qed, lthy, defs) =>
   Proof.unfolding ([[(defs, [])]])
-    (Proof.theorem NONE (snd oo after_qed)
+    (Proof.theorem NONE (snd o register_bnf key oo after_qed)
       (map (single o rpair []) goals @ map (map (rpair [])) wit_goals) lthy)) oo
   prepare_def Do_Inline user_policy I Syntax.read_term NONE;
 
@@ -1216,7 +1226,7 @@
 
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "bnf_def"} "define a BNF for an existing type"
-    (((Parse.binding --| @{keyword "="}) -- Parse.term --
+    ((parse_opt_binding_colon -- Parse.term --
        (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term --
        (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"})) >> bnf_def_cmd);
 

--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 18 03:33:53 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 18 09:15:53 2012 +0200
@@ -805,12 +805,9 @@
 
 val datatype_cmd = define_datatype Typedecl.read_constraint Syntax.parse_typ Syntax.read_term;
 
-val parse_binding_colon = Parse.binding --| @{keyword ":"};
-val parse_opt_binding_colon = Scan.optional parse_binding_colon no_binding;
-
 val parse_ctr_arg =
   @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} ||
-  (Parse.typ >> pair no_binding);
+  (Parse.typ >> pair Binding.empty);
 
 val parse_defaults =
   @{keyword "("} |-- @{keyword "defaults"} |-- Scan.repeat parse_bound_term --| @{keyword ")"};

--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 18 03:33:53 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 18 09:15:53 2012 +0200
@@ -2855,9 +2855,10 @@
         val wit_tac = mk_wit_tac n unf_fld_thms (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs);
 
         val (Jbnfs, lthy) =
-          fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn (thms, wits) =>
+          fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn (thms, wits) => fn lthy =>
             bnf_def Dont_Inline user_policy I tacs (wit_tac thms) (SOME deads)
-              ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits))
+              ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits) lthy
+            |> register_bnf (Local_Theory.full_name lthy b))
           tacss bs fs_maps setss_by_bnf Ts all_witss lthy;
 
         val fold_maps = Local_Defs.fold lthy (map (fn bnf =>

--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Tue Sep 18 03:33:53 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Tue Sep 18 09:15:53 2012 +0200
@@ -1701,9 +1701,10 @@
         fun wit_tac _ = mk_wit_tac n (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs);
 
         val (Ibnfs, lthy) =
-          fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn wits =>
+          fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn wits => fn lthy =>
             bnf_def Dont_Inline user_policy I tacs wit_tac (SOME deads)
-              ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits))
+              ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits) lthy
+            |> register_bnf (Local_Theory.full_name lthy b))
           tacss bs fs_maps setss_by_bnf Ts fld_witss lthy;
 
         val fold_maps = Local_Defs.fold lthy (map (fn bnf =>

--- a/src/HOL/Codatatype/Tools/bnf_util.ML	Tue Sep 18 03:33:53 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Tue Sep 18 09:15:53 2012 +0200
@@ -128,6 +128,9 @@
   val certifyT: Proof.context -> typ -> ctyp
   val certify: Proof.context -> term -> cterm
 
+  val parse_binding_colon: Token.T list -> binding * Token.T list
+  val parse_opt_binding_colon: Token.T list -> binding * Token.T list
+
   val typedef: bool -> binding option -> binding * (string * sort) list * mixfix -> term ->
     (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory
 
@@ -250,6 +253,9 @@
 fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
 fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);
 
+val parse_binding_colon = Parse.binding --| @{keyword ":"};
+val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty;
+
 (*TODO: is this really different from Typedef.add_typedef_global?*)
 fun typedef def opt_name typ set opt_morphs tac lthy =
   let

--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 18 03:33:53 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 18 09:15:53 2012 +0200
@@ -7,7 +7,6 @@
 
 signature BNF_WRAP =
 sig
-  val no_binding: binding
   val mk_half_pairss: 'a list -> ('a * 'a) list list
   val mk_ctr: typ list -> term -> term
   val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list ->
@@ -45,7 +44,6 @@
 val split_asmN = "split_asm";
 val weak_case_cong_thmsN = "weak_case_cong";
 
-val no_binding = @{binding ""};
 val std_binding = @{binding _};
 
 val induct_simp_attrs = @{attributes [induct_simp]};
@@ -111,10 +109,11 @@
 
     val ms = map length ctr_Tss;
 
-    val raw_disc_bindings' = pad_list no_binding n raw_disc_bindings;
+    val raw_disc_bindings' = pad_list Binding.empty n raw_disc_bindings;
 
     fun can_really_rely_on_disc k =
-      not (Binding.eq_name (nth raw_disc_bindings' (k - 1), no_binding)) orelse nth ms (k - 1) = 0;
+      not (Binding.eq_name (nth raw_disc_bindings' (k - 1), Binding.empty)) orelse
+      nth ms (k - 1) = 0;
     fun can_rely_on_disc k =
       can_really_rely_on_disc k orelse (k = 1 andalso not (can_really_rely_on_disc 2));
     fun can_omit_disc_binding k m =
@@ -127,7 +126,7 @@
       raw_disc_bindings'
       |> map4 (fn k => fn m => fn ctr => fn disc =>
         Option.map (Binding.qualify false (Binding.name_of data_b))
-          (if Binding.eq_name (disc, no_binding) then
+          (if Binding.eq_name (disc, Binding.empty) then
              if can_omit_disc_binding k m then NONE else SOME (std_disc_binding ctr)
            else if Binding.eq_name (disc, std_binding) then
              SOME (std_disc_binding ctr)
@@ -143,10 +142,10 @@
       pad_list [] n raw_sel_bindingss
       |> map3 (fn ctr => fn m => map2 (fn l => fn sel =>
         Binding.qualify false (Binding.name_of data_b)
-          (if Binding.eq_name (sel, no_binding) orelse Binding.eq_name (sel, std_binding) then
+          (if Binding.eq_name (sel, Binding.empty) orelse Binding.eq_name (sel, std_binding) then
             std_sel_binding m l ctr
           else
-            sel)) (1 upto m) o pad_list no_binding m) ctrs0 ms;
+            sel)) (1 upto m) o pad_list Binding.empty m) ctrs0 ms;
 
     fun mk_case Ts T =
       let