1.1 --- a/src/HOL/Codatatype/Basic_BNFs.thy	Tue Sep 18 03:33:53 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Basic_BNFs.thy	Tue Sep 18 09:15:53 2012 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4  lemma natLeq_cinfinite: "cinfinite natLeq"
     1.5  unfolding cinfinite_def Field_natLeq by (rule nat_infinite)
     1.6  
     1.7 -bnf_def ID = "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"]
     1.8 +bnf_def ID: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"]
     1.9  apply auto
    1.10  apply (rule natLeq_card_order)
    1.11  apply (rule natLeq_cinfinite)
    1.12 @@ -52,7 +52,7 @@
    1.13  lemma ID_pred[simp]: "ID_pred \<phi> = \<phi>"
    1.14  unfolding ID_pred_def ID_rel_def Gr_def fun_eq_iff by auto
    1.15  
    1.16 -bnf_def DEADID = "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"]
    1.17 +bnf_def DEADID: "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"]
    1.18  apply (auto simp add: wpull_id)
    1.19  apply (rule card_order_csum)
    1.20  apply (rule natLeq_card_order)
    1.21 @@ -86,8 +86,8 @@
    1.22  structure Basic_BNFs : BASIC_BNFS =
    1.23  struct
    1.24  
    1.25 -val ID_bnf = the (BNF_Def.bnf_of @{context} "ID");
    1.26 -val DEADID_bnf = the (BNF_Def.bnf_of @{context} "DEADID");
    1.27 +val ID_bnf = the (BNF_Def.bnf_of @{context} "Basic_BNFs.ID");
    1.28 +val DEADID_bnf = the (BNF_Def.bnf_of @{context} "Basic_BNFs.DEADID");
    1.29  
    1.30  val rel_def = BNF_Def.rel_def_of_bnf ID_bnf;
    1.31  val ID_rel_def = rel_def RS sym;
    1.32 @@ -104,7 +104,7 @@
    1.33  
    1.34  lemmas sum_set_defs = sum_setl_def[abs_def] sum_setr_def[abs_def]
    1.35  
    1.36 -bnf_def sum = sum_map [sum_setl, sum_setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr]
    1.37 +bnf_def sum_map [sum_setl, sum_setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr]
    1.38  proof -
    1.39    show "sum_map id id = id" by (rule sum_map.id)
    1.40  next
    1.41 @@ -240,7 +240,7 @@
    1.42  
    1.43  lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
    1.44  
    1.45 -bnf_def prod = map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair]
    1.46 +bnf_def map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair]
    1.47  proof (unfold prod_set_defs)
    1.48    show "map_pair id id = id" by (rule map_pair.id)
    1.49  next
    1.50 @@ -358,7 +358,7 @@
    1.51    ultimately show ?thesis using card_of_ordLeq by fast
    1.52  qed
    1.53  
    1.54 -bnf_def "fun" = "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|"
    1.55 +bnf_def "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|"
    1.56    ["%c x::'b::type. c::'a::type"]
    1.57  proof
    1.58    fix f show "id \<circ> f = id f" by simp

     2.1 --- a/src/HOL/Codatatype/More_BNFs.thy	Tue Sep 18 03:33:53 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/More_BNFs.thy	Tue Sep 18 09:15:53 2012 +0200
     2.3 @@ -22,7 +22,7 @@
     2.4  lemma option_rec_conv_option_case: "option_rec = option_case"
     2.5  by (simp add: fun_eq_iff split: option.split)
     2.6  
     2.7 -bnf_def option = Option.map [Option.set] "\<lambda>_::'a option. natLeq" ["None"]
     2.8 +bnf_def Option.map [Option.set] "\<lambda>_::'a option. natLeq" ["None"]
     2.9  proof -
    2.10    show "Option.map id = id" by (simp add: fun_eq_iff Option.map_def split: option.split)
    2.11  next
    2.12 @@ -190,7 +190,7 @@
    2.13    qed
    2.14  qed
    2.15  
    2.16 -bnf_def list = map [set] "\<lambda>_::'a list. natLeq" ["[]"]
    2.17 +bnf_def map [set] "\<lambda>_::'a list. natLeq" ["[]"]
    2.18  proof -
    2.19    show "map id = id" by (rule List.map.id)
    2.20  next
    2.21 @@ -355,7 +355,7 @@
    2.22  lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A"
    2.23  by (rule f_the_inv_into_f) (auto simp: inj_on_def fset_cong dest!: finite_ex_fset)
    2.24  
    2.25 -bnf_def fset = map_fset [fset] "\<lambda>_::'a fset. natLeq" ["{||}"]
    2.26 +bnf_def map_fset [fset] "\<lambda>_::'a fset. natLeq" ["{||}"]
    2.27  proof -
    2.28    show "map_fset id = id"
    2.29    unfolding map_fset_def2 map_id o_id afset_rfset_id ..
    2.30 @@ -511,7 +511,7 @@
    2.31    finally show ?thesis .
    2.32  qed
    2.33  
    2.34 -bnf_def cset = cIm [rcset] "\<lambda>_::'a cset. natLeq" ["cEmp"]
    2.35 +bnf_def cIm [rcset] "\<lambda>_::'a cset. natLeq" ["cEmp"]
    2.36  proof -
    2.37    show "cIm id = id" unfolding cIm_def[abs_def] id_def by auto
    2.38  next
    2.39 @@ -1134,7 +1134,7 @@
    2.40  definition mset_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
    2.41  "mset_map h = Abs_multiset \<circ> mmap h \<circ> count"
    2.42  
    2.43 -bnf_def mset = mset_map [set_of] "\<lambda>_::'a multiset. natLeq" ["{#}"]
    2.44 +bnf_def mset_map [set_of] "\<lambda>_::'a multiset. natLeq" ["{#}"]
    2.45  unfolding mset_map_def
    2.46  proof -
    2.47    show "Abs_multiset \<circ> mmap id \<circ> count = id" unfolding mmap_id by (auto simp: count_inverse)

     3.1 --- a/src/HOL/Codatatype/Tools/bnf_def.ML	Tue Sep 18 03:33:53 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Tue Sep 18 09:15:53 2012 +0200
     3.3 @@ -12,6 +12,8 @@
     3.4    type nonemptiness_witness = {I: int list, wit: term, prop: thm list}
     3.5  
     3.6    val bnf_of: Proof.context -> string -> BNF option
     3.7 +  val register_bnf: string -> (BNF * local_theory) -> (BNF * local_theory)
     3.8 +
     3.9    val name_of_bnf: BNF -> binding
    3.10    val T_of_bnf: BNF -> typ
    3.11    val live_of_bnf: BNF -> int
    3.12 @@ -540,6 +542,18 @@
    3.13      | _ => error "Bad bound constant");
    3.14      val wit_rhss = map (prep_term no_defs_lthy) raw_wits;
    3.15  
    3.16 +    fun err T =
    3.17 +      error ("Trying to register the type " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^
    3.18 +        " as unnamed BNF");
    3.19 +
    3.20 +    val (b, key) =
    3.21 +      if Binding.eq_name (b, Binding.empty) then
    3.22 +        (case bd_rhsT of
    3.23 +          Type (C, Ts) => if forall (is_some o try dest_TFree) Ts
    3.24 +            then (Binding.qualified_name C, C) else err bd_rhsT
    3.25 +        | T => err T)
    3.26 +      else (b, Local_Theory.full_name no_defs_lthy b);
    3.27 +
    3.28      val map_bind_def = (fn () => Binding.suffix_name ("_" ^ mapN) b, map_rhs);
    3.29      val set_binds_defs =
    3.30        let
    3.31 @@ -624,12 +638,6 @@
    3.32      | SOME Ds => map (Morphism.typ phi) Ds);
    3.33      val dead = length deads;
    3.34  
    3.35 -    (*FIXME: check DUP here, not in after_qed*)
    3.36 -    val key =
    3.37 -      (case (CA, Binding.eq_name (qualify b, b)) of
    3.38 -        (Type (C, _), true) => C
    3.39 -      | _ => Name_Space.full_name Name_Space.default_naming b);
    3.40 -
    3.41      (*TODO: further checks of type of bnf_map*)
    3.42      (*TODO: check types of bnf_sets*)
    3.43      (*TODO: check type of bnf_bd*)
    3.44 @@ -1152,18 +1160,20 @@
    3.45                        [(thms, [])]));
    3.46                  in
    3.47                    Local_Theory.notes notes #> snd
    3.48 -                  #> Local_Theory.declaration {syntax = false, pervasive = true}
    3.49 -                    (fn phi => Data.map (Symtab.update_new (key, morph_bnf phi bnf)))
    3.50                  end
    3.51                else
    3.52                  I))
    3.53        end;
    3.54    in
    3.55 -    (goals, wit_goalss, after_qed, lthy', one_step_defs)
    3.56 +    (key, goals, wit_goalss, after_qed, lthy', one_step_defs)
    3.57    end;
    3.58  
    3.59 +fun register_bnf key (bnf, lthy) =
    3.60 +  (bnf, Local_Theory.declaration {syntax = false, pervasive = true}
    3.61 +    (fn phi => Data.map (Symtab.update_new (key, morph_bnf phi bnf))) lthy);
    3.62 +
    3.63  fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds =
    3.64 -  (fn (goals, wit_goalss, after_qed, lthy, defs) =>
    3.65 +  (fn (_, goals, wit_goalss, after_qed, lthy, defs) =>
    3.66    let
    3.67      val wits_tac = K (TRYALL Goal.conjunction_tac) THEN' unfold_defs_tac lthy defs wit_tac;
    3.68      val wit_goals = wit_goalss |> map Logic.mk_conjunction_balanced;
    3.69 @@ -1179,9 +1189,9 @@
    3.70      |> (fn thms => after_qed (map single thms @ wit_thms) lthy)
    3.71    end) oo prepare_def const_policy fact_policy qualify (K I) Ds;
    3.72  
    3.73 -val bnf_def_cmd = (fn (goals, wit_goals, after_qed, lthy, defs) =>
    3.74 +val bnf_def_cmd = (fn (key, goals, wit_goals, after_qed, lthy, defs) =>
    3.75    Proof.unfolding ([[(defs, [])]])
    3.76 -    (Proof.theorem NONE (snd oo after_qed)
    3.77 +    (Proof.theorem NONE (snd o register_bnf key oo after_qed)
    3.78        (map (single o rpair []) goals @ map (map (rpair [])) wit_goals) lthy)) oo
    3.79    prepare_def Do_Inline user_policy I Syntax.read_term NONE;
    3.80  
    3.81 @@ -1216,7 +1226,7 @@
    3.82  
    3.83  val _ =
    3.84    Outer_Syntax.local_theory_to_proof @{command_spec "bnf_def"} "define a BNF for an existing type"
    3.85 -    (((Parse.binding --| @{keyword "="}) -- Parse.term --
    3.86 +    ((parse_opt_binding_colon -- Parse.term --
    3.87         (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term --
    3.88         (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"})) >> bnf_def_cmd);
    3.89  

     4.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 18 03:33:53 2012 +0200
     4.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 18 09:15:53 2012 +0200
     4.3 @@ -805,12 +805,9 @@
     4.4  
     4.5  val datatype_cmd = define_datatype Typedecl.read_constraint Syntax.parse_typ Syntax.read_term;
     4.6  
     4.7 -val parse_binding_colon = Parse.binding --| @{keyword ":"};
     4.8 -val parse_opt_binding_colon = Scan.optional parse_binding_colon no_binding;
     4.9 -
    4.10  val parse_ctr_arg =
    4.11    @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} ||
    4.12 -  (Parse.typ >> pair no_binding);
    4.13 +  (Parse.typ >> pair Binding.empty);
    4.14  
    4.15  val parse_defaults =
    4.16    @{keyword "("} |-- @{keyword "defaults"} |-- Scan.repeat parse_bound_term --| @{keyword ")"};

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

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

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

     8.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 18 03:33:53 2012 +0200
     8.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 18 09:15:53 2012 +0200
     8.3 @@ -7,7 +7,6 @@
     8.4  
     8.5  signature BNF_WRAP =
     8.6  sig
     8.7 -  val no_binding: binding
     8.8    val mk_half_pairss: 'a list -> ('a * 'a) list list
     8.9    val mk_ctr: typ list -> term -> term
    8.10    val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list ->
    8.11 @@ -45,7 +44,6 @@
    8.12  val split_asmN = "split_asm";
    8.13  val weak_case_cong_thmsN = "weak_case_cong";
    8.14  
    8.15 -val no_binding = @{binding ""};
    8.16  val std_binding = @{binding _};
    8.17  
    8.18  val induct_simp_attrs = @{attributes [induct_simp]};
    8.19 @@ -111,10 +109,11 @@
    8.20  
    8.21      val ms = map length ctr_Tss;
    8.22  
    8.23 -    val raw_disc_bindings' = pad_list no_binding n raw_disc_bindings;
    8.24 +    val raw_disc_bindings' = pad_list Binding.empty n raw_disc_bindings;
    8.25  
    8.26      fun can_really_rely_on_disc k =
    8.27 -      not (Binding.eq_name (nth raw_disc_bindings' (k - 1), no_binding)) orelse nth ms (k - 1) = 0;
    8.28 +      not (Binding.eq_name (nth raw_disc_bindings' (k - 1), Binding.empty)) orelse
    8.29 +      nth ms (k - 1) = 0;
    8.30      fun can_rely_on_disc k =
    8.31        can_really_rely_on_disc k orelse (k = 1 andalso not (can_really_rely_on_disc 2));
    8.32      fun can_omit_disc_binding k m =
    8.33 @@ -127,7 +126,7 @@
    8.34        raw_disc_bindings'
    8.35        |> map4 (fn k => fn m => fn ctr => fn disc =>
    8.36          Option.map (Binding.qualify false (Binding.name_of data_b))
    8.37 -          (if Binding.eq_name (disc, no_binding) then
    8.38 +          (if Binding.eq_name (disc, Binding.empty) then
    8.39               if can_omit_disc_binding k m then NONE else SOME (std_disc_binding ctr)
    8.40             else if Binding.eq_name (disc, std_binding) then
    8.41               SOME (std_disc_binding ctr)
    8.42 @@ -143,10 +142,10 @@
    8.43        pad_list [] n raw_sel_bindingss
    8.44        |> map3 (fn ctr => fn m => map2 (fn l => fn sel =>
    8.45          Binding.qualify false (Binding.name_of data_b)
    8.46 -          (if Binding.eq_name (sel, no_binding) orelse Binding.eq_name (sel, std_binding) then
    8.47 +          (if Binding.eq_name (sel, Binding.empty) orelse Binding.eq_name (sel, std_binding) then
    8.48              std_sel_binding m l ctr
    8.49            else
    8.50 -            sel)) (1 upto m) o pad_list no_binding m) ctrs0 ms;
    8.51 +            sel)) (1 upto m) o pad_list Binding.empty m) ctrs0 ms;
    8.52  
    8.53      fun mk_case Ts T =
    8.54        let