use 'where' clause for selector default value syntax
authorblanchet
Tue Jun 10 12:16:22 2014 +0200 (2014-06-10)
changeset 57200aab87ffa60cc
parent 57199 472360558b22
child 57201 697e0fad9337
use 'where' clause for selector default value syntax
src/Doc/Datatypes/Datatypes.thy
src/HOL/BNF_Examples/ListF.thy
src/HOL/List.thy
src/HOL/Nat.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Tue Jun 10 11:38:53 2014 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Tue Jun 10 12:16:22 2014 +0200
     1.3 @@ -375,8 +375,10 @@
     1.4      context early begin
     1.5  (*>*)
     1.6      datatype_new (set: 'a) list (map: map rel: list_all2) =
     1.7 -      null: Nil (defaults tl: Nil)
     1.8 +      null: Nil
     1.9      | Cons (hd: 'a) (tl: "'a list")
    1.10 +    where
    1.11 +      "tl Nil = Nil"
    1.12  
    1.13  text {*
    1.14  \noindent
    1.15 @@ -415,10 +417,10 @@
    1.16  The discriminator associated with @{const Cons} is simply
    1.17  @{term "\<lambda>xs. \<not> null xs"}.
    1.18  
    1.19 -The @{text defaults} clause following the @{const Nil} constructor specifies a
    1.20 -default value for selectors associated with other constructors. Here, it is used
    1.21 -to ensure that the tail of the empty list is itself (instead of being left
    1.22 -unspecified).
    1.23 +The \keyw{where} clause at the end of the command specifies a default value for
    1.24 +selectors applied to constructors on which they are not a priori specified.
    1.25 +Here, it is used to ensure that the tail of the empty list is itself (instead of
    1.26 +being left unspecified).
    1.27  
    1.28  Because @{const Nil} is nullary, it is also possible to use
    1.29  @{term "\<lambda>xs. xs = Nil"} as a discriminator. This is the default behavior
    1.30 @@ -470,7 +472,8 @@
    1.31  
    1.32  @{rail \<open>
    1.33    @@{command datatype_new} target? @{syntax dt_options}? \<newline>
    1.34 -    (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') + @'and')
    1.35 +    (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') + @'and') \<newline>
    1.36 +    (@'where' (@{syntax prop} + '|'))?
    1.37    ;
    1.38    @{syntax_def dt_options}: '(' (('discs_sels' | 'no_code') + ',') ')'
    1.39  \<close>}
    1.40 @@ -482,7 +485,8 @@
    1.41  datatypes specified by their constructors.
    1.42  
    1.43  The syntactic entity \synt{target} can be used to specify a local
    1.44 -context---e.g., @{text "(in linorder)"} \cite{isabelle-isar-ref}.
    1.45 +context (e.g., @{text "(in linorder)"} \cite{isabelle-isar-ref}),
    1.46 +and \synt{prop} denotes a HOL proposition.
    1.47  
    1.48  The optional target is optionally followed by one or both of the following
    1.49  options:
    1.50 @@ -500,6 +504,11 @@
    1.51  registered for code generation.
    1.52  \end{itemize}
    1.53  
    1.54 +The optional \keyw{where} clause specifies default values for selectors.
    1.55 +Each proposition must be an equation of the form
    1.56 +@{text "un_D (C \<dots>) = \<dots>"}, where @{text C} is a constructor and
    1.57 +@{text un_D} is a selector.
    1.58 +
    1.59  The left-hand sides of the datatype equations specify the name of the type to
    1.60  define, its type parameters, and additional information:
    1.61  
    1.62 @@ -531,8 +540,7 @@
    1.63  mention exactly the same type variables in the same order.
    1.64  
    1.65  @{rail \<open>
    1.66 -  @{syntax_def dt_ctor}: (name ':')? name (@{syntax dt_ctor_arg} * ) \<newline>
    1.67 -    @{syntax dt_sel_defaults}? mixfix?
    1.68 +  @{syntax_def dt_ctor}: (name ':')? name (@{syntax dt_ctor_arg} * ) mixfix?
    1.69  \<close>}
    1.70  
    1.71  \medskip
    1.72 @@ -557,21 +565,6 @@
    1.73  name for the corresponding selector to override the default name
    1.74  (@{text un_C\<^sub>ji}). The same selector names can be reused for several
    1.75  constructors as long as they share the same type.
    1.76 -
    1.77 -@{rail \<open>
    1.78 -  @{syntax_def dt_sel_defaults}: '(' 'defaults' (name ':' term +) ')'
    1.79 -\<close>}
    1.80 -
    1.81 -\medskip
    1.82 -
    1.83 -\noindent
    1.84 -Given a constructor
    1.85 -@{text "C \<Colon> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<sigma>\<^sub>p \<Rightarrow> \<sigma>"},
    1.86 -default values can be specified for any selector
    1.87 -@{text "un_D \<Colon> \<sigma> \<Rightarrow> \<tau>"}
    1.88 -associated with other constructors. The specified default value must be of type
    1.89 -@{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<sigma>\<^sub>p \<Rightarrow> \<tau>"}
    1.90 -(i.e., it may depend on @{text C}'s arguments).
    1.91  *}
    1.92  
    1.93  
    1.94 @@ -1485,13 +1478,19 @@
    1.95  The following example illustrates this procedure:
    1.96  *}
    1.97  
    1.98 +(*<*)
    1.99 +    hide_const termi
   1.100 +(*>*)
   1.101      consts termi\<^sub>0 :: 'a
   1.102  
   1.103  text {* \blankline *}
   1.104  
   1.105      datatype_new ('a, 'b) tlist =
   1.106 -      TNil (termi: 'b) (defaults ttl: TNil)
   1.107 -    | TCons (thd: 'a) (ttl : "('a, 'b) tlist") (defaults termi: "\<lambda>_ xs. termi\<^sub>0 xs")
   1.108 +      TNil (termi: 'b)
   1.109 +    | TCons (thd: 'a) (ttl: "('a, 'b) tlist")
   1.110 +    where
   1.111 +      "ttl (TNil y) = TNil y"
   1.112 +    | "termi (TCons _ xs) = termi\<^sub>0 xs"
   1.113  
   1.114  text {* \blankline *}
   1.115  
   1.116 @@ -1557,8 +1556,10 @@
   1.117  *}
   1.118  
   1.119      codatatype (lset: 'a) llist (map: lmap rel: llist_all2) =
   1.120 -      lnull: LNil (defaults ltl: LNil)
   1.121 +      lnull: LNil
   1.122      | LCons (lhd: 'a) (ltl: "'a llist")
   1.123 +    where
   1.124 +      "ltl LNil = LNil"
   1.125  
   1.126  text {*
   1.127  \noindent
   1.128 @@ -2646,10 +2647,10 @@
   1.129  
   1.130  @{rail \<open>
   1.131    @@{command free_constructors} target? @{syntax dt_options} \<newline>
   1.132 -    name 'for' (@{syntax fc_ctor} + '|')
   1.133 +    name 'for' (@{syntax fc_ctor} + '|') \<newline>
   1.134 +  (@'where' (@{syntax prop} + '|'))?
   1.135    ;
   1.136 -  @{syntax_def fc_ctor}: (name ':')? term (name * ) \<newline>
   1.137 -    @{syntax dt_sel_defaults}?
   1.138 +  @{syntax_def fc_ctor}: (name ':')? term (name * )
   1.139  \<close>}
   1.140  
   1.141  \medskip
   1.142 @@ -2661,8 +2662,8 @@
   1.143  that is queried by various tools (e.g., \keyw{function}).
   1.144  
   1.145  The syntactic entity \synt{target} can be used to specify a local context,
   1.146 -\synt{name} denotes an identifier, and \synt{term} denotes a HOL term
   1.147 -\cite{isabelle-isar-ref}.
   1.148 +\synt{name} denotes an identifier, \synt{prop} denotes a HOL proposition, and
   1.149 +\synt{term} denotes a HOL term \cite{isabelle-isar-ref}.
   1.150  
   1.151  The syntax resembles that of @{command datatype_new} and @{command codatatype}
   1.152  definitions (Sections
     2.1 --- a/src/HOL/BNF_Examples/ListF.thy	Tue Jun 10 11:38:53 2014 +0200
     2.2 +++ b/src/HOL/BNF_Examples/ListF.thy	Tue Jun 10 12:16:22 2014 +0200
     2.3 @@ -13,7 +13,10 @@
     2.4  begin
     2.5  
     2.6  datatype_new 'a listF (map: mapF rel: relF) =
     2.7 -  NilF (defaults tlF: NilF) | Conss (hdF: 'a) (tlF: "'a listF")
     2.8 +    NilF
     2.9 +  | Conss (hdF: 'a) (tlF: "'a listF")
    2.10 +where
    2.11 +  "tlF NilF = NilF"
    2.12  
    2.13  datatype_compat listF
    2.14  
     3.1 --- a/src/HOL/List.thy	Tue Jun 10 11:38:53 2014 +0200
     3.2 +++ b/src/HOL/List.thy	Tue Jun 10 12:16:22 2014 +0200
     3.3 @@ -9,8 +9,10 @@
     3.4  begin
     3.5  
     3.6  datatype_new (set: 'a) list  (map: map rel: list_all2) =
     3.7 -    Nil (defaults tl: "[]")  ("[]")
     3.8 +    Nil  ("[]")
     3.9    | Cons (hd: 'a) (tl: "'a list")  (infixr "#" 65)
    3.10 +where
    3.11 +  "tl [] = []"
    3.12  
    3.13  datatype_compat list
    3.14  
     4.1 --- a/src/HOL/Nat.thy	Tue Jun 10 11:38:53 2014 +0200
     4.2 +++ b/src/HOL/Nat.thy	Tue Jun 10 12:16:22 2014 +0200
     4.3 @@ -83,8 +83,10 @@
     4.4  done
     4.5  
     4.6  free_constructors case_nat for
     4.7 -    "0 \<Colon> nat" (defaults pred: "0 \<Colon> nat")
     4.8 +    "0 \<Colon> nat"
     4.9    | Suc pred
    4.10 +where
    4.11 +  "pred (0 \<Colon> nat) = (0 \<Colon> nat)"
    4.12    apply atomize_elim
    4.13    apply (rename_tac n, induct_tac n rule: nat_induct0, auto)
    4.14   apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI
     5.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jun 10 11:38:53 2014 +0200
     5.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jun 10 12:16:22 2014 +0200
     5.3 @@ -67,15 +67,13 @@
     5.4      thm list -> (thm -> thm) -> thm list list -> Ctr_Sugar.ctr_sugar list -> term list ->
     5.5      thm list -> (thm list -> thm list) -> Proof.context -> gfp_sugar_thms
     5.6  
     5.7 -  type co_datatype_spec =
     5.8 -    ((((binding option * (typ * sort)) list * binding) * (binding * binding)) * mixfix)
     5.9 -    * ((binding, binding * typ, term) Ctr_Sugar.ctr_spec * mixfix) list
    5.10 -
    5.11    val co_datatypes: BNF_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
    5.12        binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
    5.13        BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
    5.14        BNF_FP_Util.fp_result * local_theory) ->
    5.15 -    (bool * bool) * co_datatype_spec list ->
    5.16 +    (bool * bool)
    5.17 +    * ((((((binding option * (typ * sort)) list * binding) * (binding * binding)) * mixfix)
    5.18 +       * ((binding, binding * typ) Ctr_Sugar.ctr_spec * mixfix) list) * term list) list ->
    5.19      local_theory -> local_theory
    5.20    val parse_co_datatype_cmd: BNF_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
    5.21        binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
    5.22 @@ -250,15 +248,16 @@
    5.23    handle THM _ => thm;
    5.24  
    5.25  type co_datatype_spec =
    5.26 -  ((((binding option * (typ * sort)) list * binding) * (binding * binding)) * mixfix)
    5.27 -  * ((binding, binding * typ, term) ctr_spec * mixfix) list;
    5.28 +  (((((binding option * (typ * sort)) list * binding) * (binding * binding)) * mixfix)
    5.29 +   * ((binding, binding * typ) ctr_spec * mixfix) list) * term list;
    5.30  
    5.31 -fun type_args_named_constrained_of_spec ((((ncAs, _), _), _), _) = ncAs;
    5.32 -fun type_binding_of_spec ((((_, b), _), _), _) = b;
    5.33 -fun map_binding_of_spec (((_, (b, _)), _), _) = b;
    5.34 -fun rel_binding_of_spec (((_, (_, b)), _), _) = b;
    5.35 -fun mixfix_of_spec ((_, mx), _) = mx;
    5.36 -fun mixfixed_ctr_specs_of_spec (_, mx_ctr_specs) = mx_ctr_specs;
    5.37 +fun type_args_named_constrained_of_spec (((((ncAs, _), _), _), _), _) = ncAs;
    5.38 +fun type_binding_of_spec (((((_, b), _), _), _), _) = b;
    5.39 +fun map_binding_of_spec ((((_, (b, _)), _), _), _) = b;
    5.40 +fun rel_binding_of_spec ((((_, (_, b)), _), _), _) = b;
    5.41 +fun mixfix_of_spec (((_, mx), _), _) = mx;
    5.42 +fun mixfixed_ctr_specs_of_spec ((_, mx_ctr_specs), _) = mx_ctr_specs;
    5.43 +fun sel_default_eqs_of_spec (_, ts) = ts;
    5.44  
    5.45  fun add_nesty_bnf_names Us =
    5.46    let
    5.47 @@ -900,7 +899,7 @@
    5.48  
    5.49      val sel_bindingsss = map (map (map fst)) ctr_argsss;
    5.50      val fake_ctr_Tsss0 = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss;
    5.51 -    val raw_sel_defaultsss = map (map sel_defaults_of_ctr_spec) ctr_specss;
    5.52 +    val raw_sel_default_eqss = map sel_default_eqs_of_spec specs;
    5.53  
    5.54      val (As :: _) :: fake_ctr_Tsss =
    5.55        burrow (burrow (Syntax.check_typs fake_lthy)) (Ass0 :: fake_ctr_Tsss0);
    5.56 @@ -1038,7 +1037,7 @@
    5.57                xtor_co_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),
    5.58              pre_rel_def), fp_map_thm), fp_set_thms), fp_rel_thm), n), ks), ms), abs),
    5.59            abs_inject), abs_inverse), type_definition), ctr_bindings), ctr_mixfixes), ctr_Tss),
    5.60 -        disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy =
    5.61 +        disc_bindings), sel_bindingss), raw_sel_default_eqs) no_defs_lthy =
    5.62        let
    5.63          val fp_b_name = Binding.name_of fp_b;
    5.64  
    5.65 @@ -1110,12 +1109,13 @@
    5.66  
    5.67              val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss;
    5.68  
    5.69 -            val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss
    5.70 +            val sel_default_eqs = map (prepare_term lthy) raw_sel_default_eqs;
    5.71  
    5.72 -            fun ctr_spec_of disc_b ctr0 sel_bs sel_defs = (((disc_b, ctr0), sel_bs), sel_defs);
    5.73 -            val ctr_specs = map4 ctr_spec_of disc_bindings ctrs0 sel_bindingss sel_defaultss;
    5.74 +            fun ctr_spec_of disc_b ctr0 sel_bs = ((disc_b, ctr0), sel_bs);
    5.75 +            val ctr_specs = map3 ctr_spec_of disc_bindings ctrs0 sel_bindingss;
    5.76            in
    5.77 -            free_constructors tacss (((discs_sels, no_code), standard_binding), ctr_specs) lthy
    5.78 +            free_constructors tacss ((((discs_sels, no_code), standard_binding), ctr_specs),
    5.79 +              sel_default_eqs) lthy
    5.80            end;
    5.81  
    5.82          fun derive_maps_sets_rels (ctr_sugar as {case_cong, discs, selss, ctrs, exhaust, disc_thmss,
    5.83 @@ -1525,7 +1525,7 @@
    5.84          xtor_co_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~ pre_set_defss ~~
    5.85          pre_rel_defs ~~ xtor_map_thms ~~ xtor_set_thmss ~~ xtor_rel_thms ~~ ns ~~ kss ~~ mss ~~
    5.86          abss ~~ abs_injects ~~ abs_inverses ~~ type_definitions ~~ ctr_bindingss ~~ ctr_mixfixess ~~
    5.87 -        ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss)
    5.88 +        ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_default_eqss)
    5.89        |> wrap_types_etc
    5.90        |> case_fp fp derive_note_induct_recs_thms_for_types
    5.91             derive_note_coinduct_corecs_thms_for_types;
    5.92 @@ -1550,7 +1550,7 @@
    5.93  
    5.94  val parse_spec =
    5.95    parse_type_args_named_constrained -- Parse.binding -- parse_map_rel_bindings --
    5.96 -  Parse.opt_mixfix -- (@{keyword "="} |-- parse_ctr_specs);
    5.97 +  Parse.opt_mixfix -- (@{keyword "="} |-- parse_ctr_specs) -- parse_sel_default_eqs;
    5.98  
    5.99  val parse_co_datatype = parse_ctr_options -- Parse.and_list1 parse_spec;
   5.100  
     6.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Jun 10 11:38:53 2014 +0200
     6.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Jun 10 12:16:22 2014 +0200
     6.3 @@ -56,19 +56,19 @@
     6.4    val dest_case: Proof.context -> string -> typ list -> term ->
     6.5      (ctr_sugar * term list * term list) option
     6.6  
     6.7 -  type ('c, 'a, 'v) ctr_spec = ((binding * 'c) * 'a list) * (binding * 'v) list
     6.8 +  type ('c, 'a) ctr_spec = (binding * 'c) * 'a list
     6.9  
    6.10 -  val disc_of_ctr_spec: ('c, 'a, 'v) ctr_spec -> binding
    6.11 -  val ctr_of_ctr_spec: ('c, 'a, 'v) ctr_spec -> 'c
    6.12 -  val args_of_ctr_spec: ('c, 'a, 'v) ctr_spec -> 'a list
    6.13 -  val sel_defaults_of_ctr_spec: ('c, 'a, 'v) ctr_spec -> (binding * 'v) list
    6.14 +  val disc_of_ctr_spec: ('c, 'a) ctr_spec -> binding
    6.15 +  val ctr_of_ctr_spec: ('c, 'a) ctr_spec -> 'c
    6.16 +  val args_of_ctr_spec: ('c, 'a) ctr_spec -> 'a list
    6.17  
    6.18    val free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
    6.19 -    ((bool * bool) * binding) * (term, binding, term) ctr_spec list -> local_theory ->
    6.20 +    (((bool * bool) * binding) * (term, binding) ctr_spec list) * term list -> local_theory ->
    6.21      ctr_sugar * local_theory
    6.22    val parse_bound_term: (binding * string) parser
    6.23    val parse_ctr_options: (bool * bool) parser
    6.24 -  val parse_ctr_spec: 'c parser -> 'a parser -> ('c, 'a, string) ctr_spec parser
    6.25 +  val parse_ctr_spec: 'c parser -> 'a parser -> ('c, 'a) ctr_spec parser
    6.26 +  val parse_sel_default_eqs: string list parser
    6.27  end;
    6.28  
    6.29  structure Ctr_Sugar : CTR_SUGAR =
    6.30 @@ -313,24 +313,43 @@
    6.31      | _ => NONE)
    6.32    | _ => NONE);
    6.33  
    6.34 -fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
    6.35 +fun const_or_free_name (Const (s, _)) = Long_Name.base_name s
    6.36 +  | const_or_free_name (Free (s, _)) = s
    6.37 +  | const_or_free_name t = raise TERM ("const_or_free_name", [t])
    6.38  
    6.39 -type ('c, 'a, 'v) ctr_spec = ((binding * 'c) * 'a list) * (binding * 'v) list;
    6.40 +fun extract_sel_default ctxt t =
    6.41 +  let
    6.42 +    fun malformed () =
    6.43 +      error ("Malformed selector default value equation: " ^ Syntax.string_of_term ctxt t);
    6.44  
    6.45 -fun disc_of_ctr_spec (((disc, _), _), _) = disc;
    6.46 -fun ctr_of_ctr_spec (((_, ctr), _), _) = ctr;
    6.47 -fun args_of_ctr_spec ((_, args), _) = args;
    6.48 -fun sel_defaults_of_ctr_spec (_, ds) = ds;
    6.49 +    val ((sel, (ctr, vars)), rhs) =
    6.50 +      fst (Term.replace_dummy_patterns (Syntax.check_term ctxt t) 0)
    6.51 +      |> HOLogic.dest_eq
    6.52 +      |>> (Term.dest_comb
    6.53 +        #>> const_or_free_name
    6.54 +        ##> (Term.strip_comb #>> (Term.dest_Const #> fst)))
    6.55 +      handle TERM _ => malformed ();
    6.56 +  in
    6.57 +    if forall (is_Free orf is_Var) vars andalso not (has_duplicates (op aconv) vars) then
    6.58 +      ((ctr, sel), fold_rev Term.lambda vars rhs)
    6.59 +    else
    6.60 +      malformed ()
    6.61 +  end;
    6.62  
    6.63 -fun prepare_free_constructors prep_term (((discs_sels, no_code), raw_case_binding), ctr_specs)
    6.64 -    no_defs_lthy =
    6.65 +type ('c, 'a) ctr_spec = (binding * 'c) * 'a list;
    6.66 +
    6.67 +fun disc_of_ctr_spec ((disc, _), _) = disc;
    6.68 +fun ctr_of_ctr_spec ((_, ctr), _) = ctr;
    6.69 +fun args_of_ctr_spec (_, args) = args;
    6.70 +
    6.71 +fun prepare_free_constructors prep_term
    6.72 +    ((((discs_sels, no_code), raw_case_binding), ctr_specs), sel_default_eqs) no_defs_lthy =
    6.73    let
    6.74      (* TODO: sanity checks on arguments *)
    6.75  
    6.76      val raw_ctrs = map ctr_of_ctr_spec ctr_specs;
    6.77      val raw_disc_bindings = map disc_of_ctr_spec ctr_specs;
    6.78      val raw_sel_bindingss = map args_of_ctr_spec ctr_specs;
    6.79 -    val raw_sel_defaultss = map sel_defaults_of_ctr_spec ctr_specs;
    6.80  
    6.81      val n = length raw_ctrs;
    6.82      val ks = 1 upto n;
    6.83 @@ -338,7 +357,6 @@
    6.84      val _ = if n > 0 then () else error "No constructors specified";
    6.85  
    6.86      val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs;
    6.87 -    val sel_defaultss = map (map (apsnd (prep_term no_defs_lthy))) raw_sel_defaultss;
    6.88  
    6.89      val Type (fcT_name, As0) = body_type (fastype_of (hd ctrs0));
    6.90      val fc_b_name = Long_Name.base_name fcT_name;
    6.91 @@ -424,8 +442,8 @@
    6.92  
    6.93      (* TODO: Eta-expension is for compatibility with the old datatype package (but it also provides
    6.94         nicer names). Consider removing. *)
    6.95 -    val eta_fs = map2 eta_expand_arg xss xfs;
    6.96 -    val eta_gs = map2 eta_expand_arg xss xgs;
    6.97 +    val eta_fs = map2 (fold_rev Term.lambda) xss xfs;
    6.98 +    val eta_gs = map2 (fold_rev Term.lambda) xss xgs;
    6.99  
   6.100      val case_binding =
   6.101        qualify false
   6.102 @@ -484,13 +502,38 @@
   6.103      val no_discs_sels =
   6.104        not discs_sels andalso
   6.105        forall (forall Binding.is_empty) (raw_disc_bindings :: raw_sel_bindingss) andalso
   6.106 -      forall null raw_sel_defaultss;
   6.107 +      null sel_default_eqs;
   6.108  
   6.109      val (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') =
   6.110        if no_discs_sels then
   6.111          (true, [], [], [], [], [], lthy')
   6.112        else
   6.113          let
   6.114 +          val sel_bindings = flat sel_bindingss;
   6.115 +          val uniq_sel_bindings = distinct Binding.eq_name sel_bindings;
   6.116 +          val all_sels_distinct = (length uniq_sel_bindings = length sel_bindings);
   6.117 +
   6.118 +          val sel_binding_index =
   6.119 +            if all_sels_distinct then 1 upto length sel_bindings
   6.120 +            else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) sel_bindings;
   6.121 +
   6.122 +          val all_proto_sels = flat (map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss);
   6.123 +          val sel_infos =
   6.124 +            AList.group (op =) (sel_binding_index ~~ all_proto_sels)
   6.125 +            |> sort (int_ord o pairself fst)
   6.126 +            |> map snd |> curry (op ~~) uniq_sel_bindings;
   6.127 +          val sel_bindings = map fst sel_infos;
   6.128 +          val sel_Ts = map (curry (op -->) fcT o fastype_of o snd o snd o hd o snd) sel_infos;
   6.129 +
   6.130 +          val sel_default_lthy = no_defs_lthy
   6.131 +            |> Proof_Context.allow_dummies
   6.132 +            |> Proof_Context.add_fixes
   6.133 +              (map2 (fn b => fn T => (b, SOME T, NoSyn)) sel_bindings sel_Ts)
   6.134 +            |> snd;
   6.135 +
   6.136 +          val sel_defaults =
   6.137 +            map (extract_sel_default sel_default_lthy o prep_term sel_default_lthy) sel_default_eqs;
   6.138 +
   6.139            fun disc_free b = Free (Binding.name_of b, mk_pred1T fcT);
   6.140  
   6.141            fun disc_spec b exist_xs_u_eq_ctr = mk_Trueprop_eq (disc_free b $ u, exist_xs_u_eq_ctr);
   6.142 @@ -499,48 +542,33 @@
   6.143              Term.lambda u (alternate_disc_lhs (K o rapp u o disc_free) (3 - k));
   6.144  
   6.145            fun mk_sel_case_args b proto_sels T =
   6.146 -            map2 (fn Ts => fn k =>
   6.147 +            map3 (fn Const (c, _) => fn Ts => fn k =>
   6.148                (case AList.lookup (op =) proto_sels k of
   6.149                  NONE =>
   6.150 -                (case AList.lookup Binding.eq_name (rev (nth sel_defaultss (k - 1))) b of
   6.151 -                  NONE => fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T)
   6.152 -                | SOME t => t |> Type.constraint (Ts ---> T) |> Syntax.check_term lthy)
   6.153 -              | SOME (xs, x) => fold_rev Term.lambda xs x)) ctr_Tss ks;
   6.154 +                (case filter (curry (op =) (c, Binding.name_of b) o fst) sel_defaults of
   6.155 +                  [] => fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T)
   6.156 +                | [(_, t)] => t
   6.157 +                | _ => error "Multiple default values for selector/constructor pair")
   6.158 +              | SOME (xs, x) => fold_rev Term.lambda xs x)) ctrs ctr_Tss ks;
   6.159  
   6.160            fun sel_spec b proto_sels =
   6.161              let
   6.162                val _ =
   6.163                  (case duplicates (op =) (map fst proto_sels) of
   6.164                     k :: _ => error ("Duplicate selector name " ^ quote (Binding.name_of b) ^
   6.165 -                     " for constructor " ^
   6.166 -                     quote (Syntax.string_of_term lthy (nth ctrs (k - 1))))
   6.167 +                     " for constructor " ^ quote (Syntax.string_of_term lthy (nth ctrs (k - 1))))
   6.168                   | [] => ())
   6.169                val T =
   6.170                  (case distinct (op =) (map (fastype_of o snd o snd) proto_sels) of
   6.171                    [T] => T
   6.172                  | T :: T' :: _ => error ("Inconsistent range type for selector " ^
   6.173 -                    quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ lthy T) ^ " vs. "
   6.174 -                    ^ quote (Syntax.string_of_typ lthy T')));
   6.175 +                    quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ lthy T) ^
   6.176 +                    " vs. " ^ quote (Syntax.string_of_typ lthy T')));
   6.177              in
   6.178                mk_Trueprop_eq (Free (Binding.name_of b, fcT --> T) $ u,
   6.179                  Term.list_comb (mk_case As T case0, mk_sel_case_args b proto_sels T) $ u)
   6.180              end;
   6.181  
   6.182 -          val sel_bindings = flat sel_bindingss;
   6.183 -          val uniq_sel_bindings = distinct Binding.eq_name sel_bindings;
   6.184 -          val all_sels_distinct = (length uniq_sel_bindings = length sel_bindings);
   6.185 -
   6.186 -          val sel_binding_index =
   6.187 -            if all_sels_distinct then 1 upto length sel_bindings
   6.188 -            else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) sel_bindings;
   6.189 -
   6.190 -          val proto_sels = flat (map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss);
   6.191 -          val sel_infos =
   6.192 -            AList.group (op =) (sel_binding_index ~~ proto_sels)
   6.193 -            |> sort (int_ord o pairself fst)
   6.194 -            |> map snd |> curry (op ~~) uniq_sel_bindings;
   6.195 -          val sel_bindings = map fst sel_infos;
   6.196 -
   6.197            fun unflat_selss xs = unflat_lookup Binding.eq_name sel_bindings xs sel_bindingss;
   6.198  
   6.199            val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) =
   6.200 @@ -733,7 +761,7 @@
   6.201                  | _ => false);
   6.202  
   6.203                val all_sel_thms =
   6.204 -                (if all_sels_distinct andalso forall null sel_defaultss then
   6.205 +                (if all_sels_distinct andalso null sel_default_eqs then
   6.206                     flat sel_thmss
   6.207                   else
   6.208                     map_product (fn s => fn (xs', c) => make_sel_thm xs' c s) sel_defs
   6.209 @@ -1020,19 +1048,17 @@
   6.210        >> (fn js => (member (op =) js 0, member (op =) js 1)))
   6.211      (false, false);
   6.212  
   6.213 -val parse_defaults =
   6.214 -  @{keyword "("} |-- Parse.reserved "defaults" |-- Scan.repeat parse_bound_term --| @{keyword ")"};
   6.215 -
   6.216  fun parse_ctr_spec parse_ctr parse_arg =
   6.217 -  parse_opt_binding_colon -- parse_ctr -- Scan.repeat parse_arg --
   6.218 -  Scan.optional parse_defaults [];
   6.219 +  parse_opt_binding_colon -- parse_ctr -- Scan.repeat parse_arg;
   6.220  
   6.221  val parse_ctr_specs = Parse.enum1 "|" (parse_ctr_spec Parse.term Parse.binding);
   6.222 +val parse_sel_default_eqs = Scan.optional (@{keyword "where"} |-- Parse.enum1 "|" Parse.prop) [];
   6.223  
   6.224  val _ =
   6.225    Outer_Syntax.local_theory_to_proof @{command_spec "free_constructors"}
   6.226      "register an existing freely generated type's constructors"
   6.227      (parse_ctr_options -- Parse.binding --| @{keyword "for"} -- parse_ctr_specs
   6.228 +       -- parse_sel_default_eqs
   6.229       >> free_constructors_cmd);
   6.230  
   6.231  val _ = Context.>> (Context.map_theory Ctr_Sugar_Interpretation.init);