1.1 --- a/src/HOL/Codatatype/Tools/bnf_def.ML	Tue Sep 18 03:33:53 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Tue Sep 18 09:15:53 2012 +0200
     1.3 @@ -12,6 +12,8 @@
     1.4    type nonemptiness_witness = {I: int list, wit: term, prop: thm list}
     1.5  
     1.6    val bnf_of: Proof.context -> string -> BNF option
     1.7 +  val register_bnf: string -> (BNF * local_theory) -> (BNF * local_theory)
     1.8 +
     1.9    val name_of_bnf: BNF -> binding
    1.10    val T_of_bnf: BNF -> typ
    1.11    val live_of_bnf: BNF -> int
    1.12 @@ -540,6 +542,18 @@
    1.13      | _ => error "Bad bound constant");
    1.14      val wit_rhss = map (prep_term no_defs_lthy) raw_wits;
    1.15  
    1.16 +    fun err T =
    1.17 +      error ("Trying to register the type " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^
    1.18 +        " as unnamed BNF");
    1.19 +
    1.20 +    val (b, key) =
    1.21 +      if Binding.eq_name (b, Binding.empty) then
    1.22 +        (case bd_rhsT of
    1.23 +          Type (C, Ts) => if forall (is_some o try dest_TFree) Ts
    1.24 +            then (Binding.qualified_name C, C) else err bd_rhsT
    1.25 +        | T => err T)
    1.26 +      else (b, Local_Theory.full_name no_defs_lthy b);
    1.27 +
    1.28      val map_bind_def = (fn () => Binding.suffix_name ("_" ^ mapN) b, map_rhs);
    1.29      val set_binds_defs =
    1.30        let
    1.31 @@ -624,12 +638,6 @@
    1.32      | SOME Ds => map (Morphism.typ phi) Ds);
    1.33      val dead = length deads;
    1.34  
    1.35 -    (*FIXME: check DUP here, not in after_qed*)
    1.36 -    val key =
    1.37 -      (case (CA, Binding.eq_name (qualify b, b)) of
    1.38 -        (Type (C, _), true) => C
    1.39 -      | _ => Name_Space.full_name Name_Space.default_naming b);
    1.40 -
    1.41      (*TODO: further checks of type of bnf_map*)
    1.42      (*TODO: check types of bnf_sets*)
    1.43      (*TODO: check type of bnf_bd*)
    1.44 @@ -1152,18 +1160,20 @@
    1.45                        [(thms, [])]));
    1.46                  in
    1.47                    Local_Theory.notes notes #> snd
    1.48 -                  #> Local_Theory.declaration {syntax = false, pervasive = true}
    1.49 -                    (fn phi => Data.map (Symtab.update_new (key, morph_bnf phi bnf)))
    1.50                  end
    1.51                else
    1.52                  I))
    1.53        end;
    1.54    in
    1.55 -    (goals, wit_goalss, after_qed, lthy', one_step_defs)
    1.56 +    (key, goals, wit_goalss, after_qed, lthy', one_step_defs)
    1.57    end;
    1.58  
    1.59 +fun register_bnf key (bnf, lthy) =
    1.60 +  (bnf, Local_Theory.declaration {syntax = false, pervasive = true}
    1.61 +    (fn phi => Data.map (Symtab.update_new (key, morph_bnf phi bnf))) lthy);
    1.62 +
    1.63  fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds =
    1.64 -  (fn (goals, wit_goalss, after_qed, lthy, defs) =>
    1.65 +  (fn (_, goals, wit_goalss, after_qed, lthy, defs) =>
    1.66    let
    1.67      val wits_tac = K (TRYALL Goal.conjunction_tac) THEN' unfold_defs_tac lthy defs wit_tac;
    1.68      val wit_goals = wit_goalss |> map Logic.mk_conjunction_balanced;
    1.69 @@ -1179,9 +1189,9 @@
    1.70      |> (fn thms => after_qed (map single thms @ wit_thms) lthy)
    1.71    end) oo prepare_def const_policy fact_policy qualify (K I) Ds;
    1.72  
    1.73 -val bnf_def_cmd = (fn (goals, wit_goals, after_qed, lthy, defs) =>
    1.74 +val bnf_def_cmd = (fn (key, goals, wit_goals, after_qed, lthy, defs) =>
    1.75    Proof.unfolding ([[(defs, [])]])
    1.76 -    (Proof.theorem NONE (snd oo after_qed)
    1.77 +    (Proof.theorem NONE (snd o register_bnf key oo after_qed)
    1.78        (map (single o rpair []) goals @ map (map (rpair [])) wit_goals) lthy)) oo
    1.79    prepare_def Do_Inline user_policy I Syntax.read_term NONE;
    1.80  
    1.81 @@ -1216,7 +1226,7 @@
    1.82  
    1.83  val _ =
    1.84    Outer_Syntax.local_theory_to_proof @{command_spec "bnf_def"} "define a BNF for an existing type"
    1.85 -    (((Parse.binding --| @{keyword "="}) -- Parse.term --
    1.86 +    ((parse_opt_binding_colon -- Parse.term --
    1.87         (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term --
    1.88         (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"})) >> bnf_def_cmd);
    1.89