1.1 --- a/src/HOL/Codatatype/BNF_Def.thy	Tue Sep 11 18:12:23 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/BNF_Def.thy	Tue Sep 11 18:39:47 2012 +0200
     1.3 @@ -10,8 +10,7 @@
     1.4  theory BNF_Def
     1.5  imports BNF_Util
     1.6  keywords
     1.7 -  "print_bnfs" :: diag
     1.8 -and
     1.9 +  "print_bnfs" :: diag and
    1.10    "bnf_def" :: thy_goal
    1.11  uses
    1.12    "Tools/bnf_def_tactics.ML"

     2.1 --- a/src/HOL/Codatatype/BNF_Wrap.thy	Tue Sep 11 18:12:23 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/BNF_Wrap.thy	Tue Sep 11 18:39:47 2012 +0200
     2.3 @@ -10,8 +10,7 @@
     2.4  theory BNF_Wrap
     2.5  imports BNF_Util
     2.6  keywords
     2.7 -  "wrap_data" :: thy_goal
     2.8 -and
     2.9 +  "wrap_data" :: thy_goal and
    2.10    "no_dests"
    2.11  uses
    2.12    "Tools/bnf_wrap_tactics.ML"

     3.1 --- a/src/HOL/Codatatype/Codatatype.thy	Tue Sep 11 18:12:23 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Codatatype.thy	Tue Sep 11 18:39:47 2012 +0200
     3.3 @@ -12,9 +12,9 @@
     3.4  theory Codatatype
     3.5  imports BNF_LFP BNF_GFP BNF_Wrap
     3.6  keywords
     3.7 -  "data" :: thy_decl
     3.8 -and
     3.9 -  "codata" :: thy_decl
    3.10 +  "data" :: thy_decl and
    3.11 +  "codata" :: thy_decl and
    3.12 +  "defaults"
    3.13  uses
    3.14    "Tools/bnf_fp_sugar_tactics.ML"
    3.15    "Tools/bnf_fp_sugar.ML"

     4.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 11 18:12:23 2012 +0200
     4.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 11 18:39:47 2012 +0200
     4.3 @@ -90,14 +90,15 @@
     4.4  fun mixfix_of ((_, mx), _) = mx;
     4.5  fun ctr_specs_of (_, ctr_specs) = ctr_specs;
     4.6  
     4.7 -fun disc_of (((disc, _), _), _) = disc;
     4.8 -fun ctr_of (((_, ctr), _), _) = ctr;
     4.9 -fun args_of ((_, args), _) = args;
    4.10 +fun disc_of ((((disc, _), _), _), _) = disc;
    4.11 +fun ctr_of ((((_, ctr), _), _), _) = ctr;
    4.12 +fun args_of (((_, args), _), _) = args;
    4.13 +fun defaults_of ((_, ds), _) = ds;
    4.14  fun ctr_mixfix_of (_, mx) = mx;
    4.15  
    4.16 -fun prepare_datatype prepare_typ lfp (no_dests, specs) fake_lthy no_defs_lthy =
    4.17 +fun prepare_datatype prepare_typ prepare_term lfp (no_dests, specs) fake_lthy no_defs_lthy =
    4.18    let
    4.19 -    val _ = if not lfp andalso no_dests then error "Cannot use \"no_dests\" option for codatatypes"
    4.20 +    val _ = if not lfp andalso no_dests then error "Cannot define destructor-less codatatypes"
    4.21        else ();
    4.22  
    4.23      val constrained_As =
    4.24 @@ -136,6 +137,8 @@
    4.25      val sel_bindersss = map (map (map fst)) ctr_argsss;
    4.26      val fake_ctr_Tsss = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss;
    4.27  
    4.28 +    val raw_sel_defaultsss = map (map defaults_of) ctr_specss;
    4.29 +
    4.30      val rhs_As' = fold (fold (fold Term.add_tfreesT)) fake_ctr_Tsss [];
    4.31      val _ = (case subtract (op =) As' rhs_As' of
    4.32          [] => ()
    4.33 @@ -316,9 +319,9 @@
    4.34              (mk_terms sssss hssss, (h_sum_prod_Ts, ph_Tss))))
    4.35          end;
    4.36  
    4.37 -    fun pour_some_sugar_on_type (((((((((((((((((b, fpT), C), fld), unf), fp_iter), fp_rec),
    4.38 +    fun pour_some_sugar_on_type ((((((((((((((((((b, fpT), C), fld), unf), fp_iter), fp_rec),
    4.39            fld_unf), unf_fld), fld_inject), n), ks), ms), ctr_binders), ctr_mixfixes), ctr_Tss),
    4.40 -        disc_binders), sel_binderss) no_defs_lthy =
    4.41 +        disc_binders), sel_binderss), raw_sel_defaultss) no_defs_lthy =
    4.42        let
    4.43          val unfT = domain_type (fastype_of fld);
    4.44          val ctr_prod_Ts = map HOLogic.mk_tupleT ctr_Tss;
    4.45 @@ -479,8 +482,11 @@
    4.46              ((ctrs, selss0, coiter, corec, v, xss, ctr_defs, discIs, sel_thmss, coiter_def,
    4.47                corec_def), lthy)
    4.48            end;
    4.49 +
    4.50 +        val sel_defaultss = map (map (apsnd (prepare_term lthy'))) raw_sel_defaultss;
    4.51        in
    4.52 -        wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_binders, (sel_binderss, []))) lthy'
    4.53 +        wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_binders, (sel_binderss,
    4.54 +          sel_defaultss))) lthy'
    4.55          |> (if lfp then some_lfp_sugar else some_gfp_sugar)
    4.56        end;
    4.57  
    4.58 @@ -662,7 +668,7 @@
    4.59      val lthy' = lthy
    4.60        |> fold_map pour_some_sugar_on_type (bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~
    4.61          fp_recs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ns ~~ kss ~~ mss ~~ ctr_binderss ~~
    4.62 -        ctr_mixfixess ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss)
    4.63 +        ctr_mixfixess ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss ~~ raw_sel_defaultsss)
    4.64        |>> split_list11
    4.65        |> (if lfp then pour_more_sugar_on_lfps else pour_more_sugar_on_gfps);
    4.66  
    4.67 @@ -682,7 +688,7 @@
    4.68          (type_binder_of spec, length (type_args_constrained_of spec), mixfix_of spec)))) specs;
    4.69      val fake_lthy = Proof_Context.background_theory fake_thy lthy;
    4.70    in
    4.71 -    prepare_datatype Syntax.read_typ lfp bundle fake_lthy lthy
    4.72 +    prepare_datatype Syntax.read_typ Syntax.read_term lfp bundle fake_lthy lthy
    4.73    end;
    4.74  
    4.75  val parse_opt_binding_colon = Scan.optional (Parse.binding --| @{keyword ":"}) no_binder
    4.76 @@ -691,10 +697,13 @@
    4.77    @{keyword "("} |-- parse_opt_binding_colon -- Parse.typ --| @{keyword ")"} ||
    4.78    (Parse.typ >> pair no_binder);
    4.79  
    4.80 +val parse_defaults =
    4.81 +  @{keyword "("} |-- @{keyword "defaults"} |-- Scan.repeat parse_bound_term --| @{keyword ")"};
    4.82 +
    4.83  val parse_single_spec =
    4.84    Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
    4.85    (@{keyword "="} |-- Parse.enum1 "|" (parse_opt_binding_colon -- Parse.binding --
    4.86 -    Scan.repeat parse_ctr_arg -- Parse.opt_mixfix));
    4.87 +    Scan.repeat parse_ctr_arg -- Scan.optional parse_defaults [] -- Parse.opt_mixfix));
    4.88  
    4.89  val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_single_spec;
    4.90  

     5.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 11 18:12:23 2012 +0200
     5.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 11 18:39:47 2012 +0200
     5.3 @@ -15,6 +15,7 @@
     5.4        (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
     5.5      (term list list * thm list * thm list list) * local_theory
     5.6    val parse_wrap_options: bool parser
     5.7 +  val parse_bound_term: (binding * string) parser
     5.8  end;
     5.9  
    5.10  structure BNF_Wrap : BNF_WRAP =