more intuitive syntax for equality-style discriminators of nullary constructors
authorblanchet
Fri Apr 26 12:09:51 2013 +0200 (2013-04-26)
changeset 5179022517d04d20b
parent 51789 75b92ff1d853
child 51791 c4db685eaed0
child 51793 22f22172a361
more intuitive syntax for equality-style discriminators of nullary constructors
src/HOL/BNF/Tools/bnf_def.ML
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
src/HOL/BNF/Tools/bnf_util.ML
src/HOL/BNF/Tools/bnf_wrap.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_def.ML	Fri Apr 26 11:04:47 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_def.ML	Fri Apr 26 12:09:51 2013 +0200
     1.3 @@ -1320,7 +1320,7 @@
     1.4  
     1.5  val _ =
     1.6    Outer_Syntax.local_theory_to_proof @{command_spec "bnf_def"} "define a BNF for an existing type"
     1.7 -    ((parse_opt_binding_colon Binding.empty -- Parse.term --
     1.8 +    ((parse_opt_binding_colon -- Parse.term --
     1.9         (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term --
    1.10         (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Scan.option Parse.term)
    1.11         >> bnf_def_cmd);
     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Apr 26 11:04:47 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Apr 26 12:09:51 2013 +0200
     2.3 @@ -1222,17 +1222,16 @@
     2.4    @{keyword "("} |-- @{keyword "defaults"} |-- Scan.repeat parse_bound_term --| @{keyword ")"};
     2.5  
     2.6  val parse_type_arg_constrained =
     2.7 -  Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort)
     2.8 +  Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort);
     2.9  
    2.10 -val parse_type_arg_named_constrained =
    2.11 -  parse_opt_binding_colon Binding.empty -- parse_type_arg_constrained
    2.12 +val parse_type_arg_named_constrained = parse_opt_binding_colon -- parse_type_arg_constrained;
    2.13  
    2.14  val parse_type_args_named_constrained =
    2.15    parse_type_arg_constrained >> (single o pair Binding.empty) ||
    2.16    @{keyword "("} |-- Parse.!!! (Parse.list1 parse_type_arg_named_constrained --| @{keyword ")"}) ||
    2.17    Scan.succeed [];
    2.18  
    2.19 -val parse_map_rel_binding = Parse.short_ident --| @{keyword ":"} -- Parse.binding;
    2.20 +val parse_map_rel_binding = Parse.short_ident --| @{keyword ":"} -- parse_binding;
    2.21  
    2.22  val no_map_rel = (Binding.empty, Binding.empty);
    2.23  
    2.24 @@ -1249,11 +1248,11 @@
    2.25    Scan.succeed no_map_rel;
    2.26  
    2.27  val parse_ctr_spec =
    2.28 -  parse_opt_binding_colon smart_binding -- Parse.binding -- Scan.repeat parse_ctr_arg --
    2.29 +  parse_opt_binding_colon -- parse_binding -- Scan.repeat parse_ctr_arg --
    2.30    Scan.optional parse_defaults [] -- Parse.opt_mixfix;
    2.31  
    2.32  val parse_spec =
    2.33 -  parse_type_args_named_constrained -- Parse.binding -- parse_map_rel_bindings --
    2.34 +  parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings --
    2.35    Parse.opt_mixfix -- (@{keyword "="} |-- Parse.enum1 "|" parse_ctr_spec);
    2.36  
    2.37  val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_spec;
     3.1 --- a/src/HOL/BNF/Tools/bnf_util.ML	Fri Apr 26 11:04:47 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_util.ML	Fri Apr 26 12:09:51 2013 +0200
     3.3 @@ -160,10 +160,10 @@
     3.4    val certify: Proof.context -> term -> cterm
     3.5  
     3.6    val standard_binding: binding
     3.7 -  val smart_binding: binding
     3.8 -  val binding_eq: binding * binding -> bool
     3.9 +  val equal_binding: binding
    3.10 +  val parse_binding: Token.T list -> binding * Token.T list
    3.11    val parse_binding_colon: Token.T list -> binding * Token.T list
    3.12 -  val parse_opt_binding_colon: binding -> Token.T list -> binding * Token.T list
    3.13 +  val parse_opt_binding_colon: Token.T list -> binding * Token.T list
    3.14  
    3.15    val typedef: binding * (string * sort) list * mixfix -> term ->
    3.16      (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory
    3.17 @@ -305,16 +305,15 @@
    3.18  fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
    3.19  fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);
    3.20  
    3.21 -val binding_eq = (op =) o pairself Binding.dest
    3.22 -
    3.23  (* The standard binding stands for a name generated following the canonical convention (e.g.
    3.24     "is_Nil" from "Nil"). The smart binding is either the standard binding or no binding at all,
    3.25     depending on the context. *)
    3.26  val standard_binding = @{binding _};
    3.27 -val smart_binding = Binding.conceal standard_binding;
    3.28 +val equal_binding = @{binding "="};
    3.29  
    3.30 -val parse_binding_colon = Parse.binding --| @{keyword ":"};
    3.31 -val parse_opt_binding_colon = Scan.optional parse_binding_colon;
    3.32 +val parse_binding = Parse.binding || @{keyword "="} >> K equal_binding;
    3.33 +val parse_binding_colon = parse_binding --| @{keyword ":"};
    3.34 +val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty;
    3.35  
    3.36  (*TODO: is this really different from Typedef.add_typedef_global?*)
    3.37  fun typedef typ set opt_morphs tac lthy =
     4.1 --- a/src/HOL/BNF/Tools/bnf_wrap.ML	Fri Apr 26 11:04:47 2013 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Fri Apr 26 12:09:51 2013 +0200
     4.3 @@ -157,38 +157,33 @@
     4.4  
     4.5      val ms = map length ctr_Tss;
     4.6  
     4.7 -    val raw_disc_bindings' = pad_list smart_binding n raw_disc_bindings;
     4.8 -
     4.9 -    fun can_really_rely_on_disc k =
    4.10 -      not (Binding.is_empty (nth raw_disc_bindings' (k - 1))) orelse nth ms (k - 1) = 0;
    4.11 -    fun can_rely_on_disc k =
    4.12 -      can_really_rely_on_disc k orelse (k = 1 andalso not (can_really_rely_on_disc 2));
    4.13 -    fun can_omit_disc_binding k m =
    4.14 -      m = 0 orelse n = 1 orelse (n = 2 andalso can_rely_on_disc (3 - k));
    4.15 +    val raw_disc_bindings' = pad_list Binding.empty n raw_disc_bindings;
    4.16  
    4.17 -    fun should_really_rely_on_disc k =
    4.18 -      let val b = nth raw_disc_bindings' (k - 1) in
    4.19 -        not (Binding.is_empty b orelse binding_eq (b, smart_binding))
    4.20 -      end;
    4.21 -    fun should_rely_on_disc k =
    4.22 -      should_really_rely_on_disc k orelse (k = 1 andalso not (should_really_rely_on_disc 2));
    4.23 +    fun can_definitely_rely_on_disc k =
    4.24 +      not (Binding.is_empty (nth raw_disc_bindings' (k - 1)));
    4.25 +    fun can_rely_on_disc k =
    4.26 +      can_definitely_rely_on_disc k orelse (k = 1 andalso not (can_definitely_rely_on_disc 2));
    4.27      fun should_omit_disc_binding k =
    4.28 -      n = 1 orelse (n = 2 andalso should_rely_on_disc (3 - k));
    4.29 +      n = 1 orelse (n = 2 andalso can_rely_on_disc (3 - k));
    4.30 +
    4.31 +    fun is_disc_binding_valid b =
    4.32 +      not (Binding.is_empty b orelse Binding.eq_name (b, equal_binding));
    4.33  
    4.34      val standard_disc_binding = qualify false o Binding.name o prefix isN o base_name_of_ctr;
    4.35  
    4.36      val disc_bindings =
    4.37        raw_disc_bindings'
    4.38        |> map4 (fn k => fn m => fn ctr => fn disc =>
    4.39 -        Option.map (qualify false)
    4.40 +        qualify false
    4.41            (if Binding.is_empty disc then
    4.42 -             if can_omit_disc_binding k m then NONE else error "Cannot omit discriminator name"
    4.43 -           else if binding_eq (disc, smart_binding) then
    4.44 -             if should_omit_disc_binding k then NONE else SOME (standard_disc_binding ctr)
    4.45 -           else if binding_eq (disc, standard_binding) then
    4.46 -             SOME (standard_disc_binding ctr)
    4.47 +             if should_omit_disc_binding k then disc else standard_disc_binding ctr
    4.48 +           else if Binding.eq_name (disc, equal_binding) then
    4.49 +             if m = 0 then disc
    4.50 +             else error "Cannot use \"=\" syntax for discriminating nonnullary constructor"
    4.51 +           else if Binding.eq_name (disc, standard_binding) then
    4.52 +             standard_disc_binding ctr
    4.53             else
    4.54 -             SOME disc)) ks ms ctrs0;
    4.55 +             disc)) ks ms ctrs0;
    4.56  
    4.57      fun standard_sel_binding m l = Binding.name o mk_unN m l o base_name_of_ctr;
    4.58  
    4.59 @@ -196,7 +191,7 @@
    4.60        pad_list [] n raw_sel_bindingss
    4.61        |> map3 (fn ctr => fn m => map2 (fn l => fn sel =>
    4.62          qualify false
    4.63 -          (if Binding.is_empty sel orelse binding_eq (sel, standard_binding) then
    4.64 +          (if Binding.is_empty sel orelse Binding.eq_name (sel, standard_binding) then
    4.65              standard_sel_binding m l ctr
    4.66            else
    4.67              sel)) (1 upto m) o pad_list Binding.empty m) ctrs0 ms;
    4.68 @@ -250,9 +245,9 @@
    4.69  
    4.70      fun alternate_disc_lhs get_udisc k =
    4.71        HOLogic.mk_not
    4.72 -        (case nth disc_bindings (k - 1) of
    4.73 -          NONE => nth exist_xs_u_eq_ctrs (k - 1)
    4.74 -        | SOME b => get_udisc b (k - 1));
    4.75 +        (let val b = nth disc_bindings (k - 1) in
    4.76 +           if is_disc_binding_valid b then get_udisc b (k - 1) else nth exist_xs_u_eq_ctrs (k - 1)
    4.77 +         end);
    4.78  
    4.79      val (all_sels_distinct, discs, selss, udiscs, uselss, vdiscs, vselss, disc_defs, sel_defs,
    4.80           sel_defss, lthy') =
    4.81 @@ -314,18 +309,15 @@
    4.82  
    4.83            val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) =
    4.84              no_defs_lthy
    4.85 -            |> apfst split_list o fold_map4 (fn k => fn m => fn exist_xs_u_eq_ctr =>
    4.86 -              fn NONE =>
    4.87 -                 if n = 1 then
    4.88 -                   pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def)
    4.89 -                 else if n = 2 andalso should_omit_disc_binding k then
    4.90 -                   pair (alternate_disc k, alternate_disc_no_def)
    4.91 -                 else if m = 0 then
    4.92 -                   pair (Term.lambda u exist_xs_u_eq_ctr, refl)
    4.93 -                 else
    4.94 -                   raise Fail "missing discriminator"
    4.95 -               | SOME b => Specification.definition (SOME (b, NONE, NoSyn),
    4.96 -                   ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr)) #>> apsnd snd)
    4.97 +            |> apfst split_list o fold_map4 (fn k => fn m => fn exist_xs_u_eq_ctr => fn b =>
    4.98 +                if Binding.is_empty b then
    4.99 +                  if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def)
   4.100 +                  else pair (alternate_disc k, alternate_disc_no_def)
   4.101 +                else if Binding.eq_name (b, equal_binding) then
   4.102 +                  pair (Term.lambda u exist_xs_u_eq_ctr, refl)
   4.103 +                else
   4.104 +                  Specification.definition (SOME (b, NONE, NoSyn),
   4.105 +                    ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr)) #>> apsnd snd)
   4.106                ks ms exist_xs_u_eq_ctrs disc_bindings
   4.107              ||>> apfst split_list o fold_map (fn (b, proto_sels) =>
   4.108                Specification.definition (SOME (b, NONE, NoSyn),
   4.109 @@ -493,7 +485,8 @@
   4.110                    map3 mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose
   4.111                  end;
   4.112  
   4.113 -              val disc_thms = flat (map2 (fn NONE => K [] | SOME _ => I) disc_bindings disc_thmss);
   4.114 +              val disc_thms = flat (map2 (fn b => if is_disc_binding_valid b then I else K [])
   4.115 +                disc_bindings disc_thmss);
   4.116  
   4.117                val (disc_exclude_thms, (disc_exclude_thmsss', disc_exclude_thmsss)) =
   4.118                  let
   4.119 @@ -694,10 +687,10 @@
   4.120  
   4.121  fun parse_bracket_list parser = @{keyword "["} |-- Parse.list parser --|  @{keyword "]"};
   4.122  
   4.123 -val parse_bindings = parse_bracket_list Parse.binding;
   4.124 +val parse_bindings = parse_bracket_list parse_binding;
   4.125  val parse_bindingss = parse_bracket_list parse_bindings;
   4.126  
   4.127 -val parse_bound_term = (Parse.binding --| @{keyword ":"}) -- Parse.term;
   4.128 +val parse_bound_term = (parse_binding --| @{keyword ":"}) -- Parse.term;
   4.129  val parse_bound_terms = parse_bracket_list parse_bound_term;
   4.130  val parse_bound_termss = parse_bracket_list parse_bound_terms;
   4.131