1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 11 18:12:23 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 11 18:39:47 2012 +0200
     1.3 @@ -90,14 +90,15 @@
     1.4  fun mixfix_of ((_, mx), _) = mx;
     1.5  fun ctr_specs_of (_, ctr_specs) = ctr_specs;
     1.6  
     1.7 -fun disc_of (((disc, _), _), _) = disc;
     1.8 -fun ctr_of (((_, ctr), _), _) = ctr;
     1.9 -fun args_of ((_, args), _) = args;
    1.10 +fun disc_of ((((disc, _), _), _), _) = disc;
    1.11 +fun ctr_of ((((_, ctr), _), _), _) = ctr;
    1.12 +fun args_of (((_, args), _), _) = args;
    1.13 +fun defaults_of ((_, ds), _) = ds;
    1.14  fun ctr_mixfix_of (_, mx) = mx;
    1.15  
    1.16 -fun prepare_datatype prepare_typ lfp (no_dests, specs) fake_lthy no_defs_lthy =
    1.17 +fun prepare_datatype prepare_typ prepare_term lfp (no_dests, specs) fake_lthy no_defs_lthy =
    1.18    let
    1.19 -    val _ = if not lfp andalso no_dests then error "Cannot use \"no_dests\" option for codatatypes"
    1.20 +    val _ = if not lfp andalso no_dests then error "Cannot define destructor-less codatatypes"
    1.21        else ();
    1.22  
    1.23      val constrained_As =
    1.24 @@ -136,6 +137,8 @@
    1.25      val sel_bindersss = map (map (map fst)) ctr_argsss;
    1.26      val fake_ctr_Tsss = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss;
    1.27  
    1.28 +    val raw_sel_defaultsss = map (map defaults_of) ctr_specss;
    1.29 +
    1.30      val rhs_As' = fold (fold (fold Term.add_tfreesT)) fake_ctr_Tsss [];
    1.31      val _ = (case subtract (op =) As' rhs_As' of
    1.32          [] => ()
    1.33 @@ -316,9 +319,9 @@
    1.34              (mk_terms sssss hssss, (h_sum_prod_Ts, ph_Tss))))
    1.35          end;
    1.36  
    1.37 -    fun pour_some_sugar_on_type (((((((((((((((((b, fpT), C), fld), unf), fp_iter), fp_rec),
    1.38 +    fun pour_some_sugar_on_type ((((((((((((((((((b, fpT), C), fld), unf), fp_iter), fp_rec),
    1.39            fld_unf), unf_fld), fld_inject), n), ks), ms), ctr_binders), ctr_mixfixes), ctr_Tss),
    1.40 -        disc_binders), sel_binderss) no_defs_lthy =
    1.41 +        disc_binders), sel_binderss), raw_sel_defaultss) no_defs_lthy =
    1.42        let
    1.43          val unfT = domain_type (fastype_of fld);
    1.44          val ctr_prod_Ts = map HOLogic.mk_tupleT ctr_Tss;
    1.45 @@ -479,8 +482,11 @@
    1.46              ((ctrs, selss0, coiter, corec, v, xss, ctr_defs, discIs, sel_thmss, coiter_def,
    1.47                corec_def), lthy)
    1.48            end;
    1.49 +
    1.50 +        val sel_defaultss = map (map (apsnd (prepare_term lthy'))) raw_sel_defaultss;
    1.51        in
    1.52 -        wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_binders, (sel_binderss, []))) lthy'
    1.53 +        wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_binders, (sel_binderss,
    1.54 +          sel_defaultss))) lthy'
    1.55          |> (if lfp then some_lfp_sugar else some_gfp_sugar)
    1.56        end;
    1.57  
    1.58 @@ -662,7 +668,7 @@
    1.59      val lthy' = lthy
    1.60        |> fold_map pour_some_sugar_on_type (bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~
    1.61          fp_recs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ns ~~ kss ~~ mss ~~ ctr_binderss ~~
    1.62 -        ctr_mixfixess ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss)
    1.63 +        ctr_mixfixess ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss ~~ raw_sel_defaultsss)
    1.64        |>> split_list11
    1.65        |> (if lfp then pour_more_sugar_on_lfps else pour_more_sugar_on_gfps);
    1.66  
    1.67 @@ -682,7 +688,7 @@
    1.68          (type_binder_of spec, length (type_args_constrained_of spec), mixfix_of spec)))) specs;
    1.69      val fake_lthy = Proof_Context.background_theory fake_thy lthy;
    1.70    in
    1.71 -    prepare_datatype Syntax.read_typ lfp bundle fake_lthy lthy
    1.72 +    prepare_datatype Syntax.read_typ Syntax.read_term lfp bundle fake_lthy lthy
    1.73    end;
    1.74  
    1.75  val parse_opt_binding_colon = Scan.optional (Parse.binding --| @{keyword ":"}) no_binder
    1.76 @@ -691,10 +697,13 @@
    1.77    @{keyword "("} |-- parse_opt_binding_colon -- Parse.typ --| @{keyword ")"} ||
    1.78    (Parse.typ >> pair no_binder);
    1.79  
    1.80 +val parse_defaults =
    1.81 +  @{keyword "("} |-- @{keyword "defaults"} |-- Scan.repeat parse_bound_term --| @{keyword ")"};
    1.82 +
    1.83  val parse_single_spec =
    1.84    Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
    1.85    (@{keyword "="} |-- Parse.enum1 "|" (parse_opt_binding_colon -- Parse.binding --
    1.86 -    Scan.repeat parse_ctr_arg -- Parse.opt_mixfix));
    1.87 +    Scan.repeat parse_ctr_arg -- Scan.optional parse_defaults [] -- Parse.opt_mixfix));
    1.88  
    1.89  val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_single_spec;
    1.90