more intuitive syntax for equality-style discriminators of nullary constructors

--- a/src/HOL/BNF/Tools/bnf_def.ML	Fri Apr 26 11:04:47 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Fri Apr 26 12:09:51 2013 +0200
@@ -1320,7 +1320,7 @@
 
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "bnf_def"} "define a BNF for an existing type"
-    ((parse_opt_binding_colon Binding.empty -- Parse.term --
+    ((parse_opt_binding_colon -- Parse.term --
        (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term --
        (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Scan.option Parse.term)
        >> bnf_def_cmd);

--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Apr 26 11:04:47 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Apr 26 12:09:51 2013 +0200
@@ -1222,17 +1222,16 @@
   @{keyword "("} |-- @{keyword "defaults"} |-- Scan.repeat parse_bound_term --| @{keyword ")"};
 
 val parse_type_arg_constrained =
-  Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort)
+  Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort);
 
-val parse_type_arg_named_constrained =
-  parse_opt_binding_colon Binding.empty -- parse_type_arg_constrained
+val parse_type_arg_named_constrained = parse_opt_binding_colon -- parse_type_arg_constrained;
 
 val parse_type_args_named_constrained =
   parse_type_arg_constrained >> (single o pair Binding.empty) ||
   @{keyword "("} |-- Parse.!!! (Parse.list1 parse_type_arg_named_constrained --| @{keyword ")"}) ||
   Scan.succeed [];
 
-val parse_map_rel_binding = Parse.short_ident --| @{keyword ":"} -- Parse.binding;
+val parse_map_rel_binding = Parse.short_ident --| @{keyword ":"} -- parse_binding;
 
 val no_map_rel = (Binding.empty, Binding.empty);
 
@@ -1249,11 +1248,11 @@
   Scan.succeed no_map_rel;
 
 val parse_ctr_spec =
-  parse_opt_binding_colon smart_binding -- Parse.binding -- Scan.repeat parse_ctr_arg --
+  parse_opt_binding_colon -- parse_binding -- Scan.repeat parse_ctr_arg --
   Scan.optional parse_defaults [] -- Parse.opt_mixfix;
 
 val parse_spec =
-  parse_type_args_named_constrained -- Parse.binding -- parse_map_rel_bindings --
+  parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings --
   Parse.opt_mixfix -- (@{keyword "="} |-- Parse.enum1 "|" parse_ctr_spec);
 
 val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_spec;

--- a/src/HOL/BNF/Tools/bnf_util.ML	Fri Apr 26 11:04:47 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Fri Apr 26 12:09:51 2013 +0200
@@ -160,10 +160,10 @@
   val certify: Proof.context -> term -> cterm
 
   val standard_binding: binding
-  val smart_binding: binding
-  val binding_eq: binding * binding -> bool
+  val equal_binding: binding
+  val parse_binding: Token.T list -> binding * Token.T list
   val parse_binding_colon: Token.T list -> binding * Token.T list
-  val parse_opt_binding_colon: binding -> Token.T list -> binding * Token.T list
+  val parse_opt_binding_colon: Token.T list -> binding * Token.T list
 
   val typedef: binding * (string * sort) list * mixfix -> term ->
     (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory
@@ -305,16 +305,15 @@
 fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
 fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);
 
-val binding_eq = (op =) o pairself Binding.dest
-
 (* The standard binding stands for a name generated following the canonical convention (e.g.
    "is_Nil" from "Nil"). The smart binding is either the standard binding or no binding at all,
    depending on the context. *)
 val standard_binding = @{binding _};
-val smart_binding = Binding.conceal standard_binding;
+val equal_binding = @{binding "="};
 
-val parse_binding_colon = Parse.binding --| @{keyword ":"};
-val parse_opt_binding_colon = Scan.optional parse_binding_colon;
+val parse_binding = Parse.binding || @{keyword "="} >> K equal_binding;
+val parse_binding_colon = parse_binding --| @{keyword ":"};
+val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty;
 
 (*TODO: is this really different from Typedef.add_typedef_global?*)
 fun typedef typ set opt_morphs tac lthy =

--- a/src/HOL/BNF/Tools/bnf_wrap.ML	Fri Apr 26 11:04:47 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Fri Apr 26 12:09:51 2013 +0200
@@ -157,38 +157,33 @@
 
     val ms = map length ctr_Tss;
 
-    val raw_disc_bindings' = pad_list smart_binding n raw_disc_bindings;
-
-    fun can_really_rely_on_disc k =
-      not (Binding.is_empty (nth raw_disc_bindings' (k - 1))) orelse nth ms (k - 1) = 0;
-    fun can_rely_on_disc k =
-      can_really_rely_on_disc k orelse (k = 1 andalso not (can_really_rely_on_disc 2));
-    fun can_omit_disc_binding k m =
-      m = 0 orelse n = 1 orelse (n = 2 andalso can_rely_on_disc (3 - k));
+    val raw_disc_bindings' = pad_list Binding.empty n raw_disc_bindings;
 
-    fun should_really_rely_on_disc k =
-      let val b = nth raw_disc_bindings' (k - 1) in
-        not (Binding.is_empty b orelse binding_eq (b, smart_binding))
-      end;
-    fun should_rely_on_disc k =
-      should_really_rely_on_disc k orelse (k = 1 andalso not (should_really_rely_on_disc 2));
+    fun can_definitely_rely_on_disc k =
+      not (Binding.is_empty (nth raw_disc_bindings' (k - 1)));
+    fun can_rely_on_disc k =
+      can_definitely_rely_on_disc k orelse (k = 1 andalso not (can_definitely_rely_on_disc 2));
     fun should_omit_disc_binding k =
-      n = 1 orelse (n = 2 andalso should_rely_on_disc (3 - k));
+      n = 1 orelse (n = 2 andalso can_rely_on_disc (3 - k));
+
+    fun is_disc_binding_valid b =
+      not (Binding.is_empty b orelse Binding.eq_name (b, equal_binding));
 
     val standard_disc_binding = qualify false o Binding.name o prefix isN o base_name_of_ctr;
 
     val disc_bindings =
       raw_disc_bindings'
       |> map4 (fn k => fn m => fn ctr => fn disc =>
-        Option.map (qualify false)
+        qualify false
           (if Binding.is_empty disc then
-             if can_omit_disc_binding k m then NONE else error "Cannot omit discriminator name"
-           else if binding_eq (disc, smart_binding) then
-             if should_omit_disc_binding k then NONE else SOME (standard_disc_binding ctr)
-           else if binding_eq (disc, standard_binding) then
-             SOME (standard_disc_binding ctr)
+             if should_omit_disc_binding k then disc else standard_disc_binding ctr
+           else if Binding.eq_name (disc, equal_binding) then
+             if m = 0 then disc
+             else error "Cannot use \"=\" syntax for discriminating nonnullary constructor"
+           else if Binding.eq_name (disc, standard_binding) then
+             standard_disc_binding ctr
            else
-             SOME disc)) ks ms ctrs0;
+             disc)) ks ms ctrs0;
 
     fun standard_sel_binding m l = Binding.name o mk_unN m l o base_name_of_ctr;
 
@@ -196,7 +191,7 @@
       pad_list [] n raw_sel_bindingss
       |> map3 (fn ctr => fn m => map2 (fn l => fn sel =>
         qualify false
-          (if Binding.is_empty sel orelse binding_eq (sel, standard_binding) then
+          (if Binding.is_empty sel orelse Binding.eq_name (sel, standard_binding) then
             standard_sel_binding m l ctr
           else
             sel)) (1 upto m) o pad_list Binding.empty m) ctrs0 ms;
@@ -250,9 +245,9 @@
 
     fun alternate_disc_lhs get_udisc k =
       HOLogic.mk_not
-        (case nth disc_bindings (k - 1) of
-          NONE => nth exist_xs_u_eq_ctrs (k - 1)
-        | SOME b => get_udisc b (k - 1));
+        (let val b = nth disc_bindings (k - 1) in
+           if is_disc_binding_valid b then get_udisc b (k - 1) else nth exist_xs_u_eq_ctrs (k - 1)
+         end);
 
     val (all_sels_distinct, discs, selss, udiscs, uselss, vdiscs, vselss, disc_defs, sel_defs,
          sel_defss, lthy') =
@@ -314,18 +309,15 @@
 
           val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) =
             no_defs_lthy
-            |> apfst split_list o fold_map4 (fn k => fn m => fn exist_xs_u_eq_ctr =>
-              fn NONE =>
-                 if n = 1 then
-                   pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def)
-                 else if n = 2 andalso should_omit_disc_binding k then
-                   pair (alternate_disc k, alternate_disc_no_def)
-                 else if m = 0 then
-                   pair (Term.lambda u exist_xs_u_eq_ctr, refl)
-                 else
-                   raise Fail "missing discriminator"
-               | SOME b => Specification.definition (SOME (b, NONE, NoSyn),
-                   ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr)) #>> apsnd snd)
+            |> apfst split_list o fold_map4 (fn k => fn m => fn exist_xs_u_eq_ctr => fn b =>
+                if Binding.is_empty b then
+                  if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def)
+                  else pair (alternate_disc k, alternate_disc_no_def)
+                else if Binding.eq_name (b, equal_binding) then
+                  pair (Term.lambda u exist_xs_u_eq_ctr, refl)
+                else
+                  Specification.definition (SOME (b, NONE, NoSyn),
+                    ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr)) #>> apsnd snd)
               ks ms exist_xs_u_eq_ctrs disc_bindings
             ||>> apfst split_list o fold_map (fn (b, proto_sels) =>
               Specification.definition (SOME (b, NONE, NoSyn),
@@ -493,7 +485,8 @@
                   map3 mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose
                 end;
 
-              val disc_thms = flat (map2 (fn NONE => K [] | SOME _ => I) disc_bindings disc_thmss);
+              val disc_thms = flat (map2 (fn b => if is_disc_binding_valid b then I else K [])
+                disc_bindings disc_thmss);
 
               val (disc_exclude_thms, (disc_exclude_thmsss', disc_exclude_thmsss)) =
                 let
@@ -694,10 +687,10 @@
 
 fun parse_bracket_list parser = @{keyword "["} |-- Parse.list parser --|  @{keyword "]"};
 
-val parse_bindings = parse_bracket_list Parse.binding;
+val parse_bindings = parse_bracket_list parse_binding;
 val parse_bindingss = parse_bracket_list parse_bindings;
 
-val parse_bound_term = (Parse.binding --| @{keyword ":"}) -- Parse.term;
+val parse_bound_term = (parse_binding --| @{keyword ":"}) -- Parse.term;
 val parse_bound_terms = parse_bracket_list parse_bound_term;
 val parse_bound_termss = parse_bracket_list parse_bound_terms;