--- a/NEWS Mon May 26 16:32:51 2014 +0200
+++ b/NEWS Mon May 26 16:32:55 2014 +0200
@@ -316,6 +316,9 @@
* The constant "xxx_(un)fold" and related theorems are no longer generated.
Use "xxx_(co)rec" or define "xxx_(un)fold" manually using "prim(co)rec".
INCOMPATIBILITY.
+ * No discriminators are generated for nullary constructors by default,
+ eliminating the need for the odd "=:" syntax.
+ INCOMPATIBILITY.
* Old datatype package:
* The generated theorems "xxx.cases" and "xxx.recs" have been renamed
--- a/src/Doc/Datatypes/Datatypes.thy Mon May 26 16:32:51 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Mon May 26 16:32:55 2014 +0200
@@ -421,11 +421,11 @@
unspecified).
Because @{const Nil} is nullary, it is also possible to use
-@{term "\<lambda>xs. xs = Nil"} as a discriminator. This is specified by
-entering ``@{text "="}'' (equality) instead of the identifier @{const null}.
-Although this may look appealing, the mixture of constructors and selectors
-in the characteristic theorems can lead Isabelle's automation to switch between
-the constructor and the destructor view in surprising ways.
+@{term "\<lambda>xs. xs = Nil"} as a discriminator. This is the default behavior
+if we omit the identifier @{const null} and the associated colon. Some users
+argue against this, because the mixture of constructors and selectors in the
+characteristic theorems can lead Isabelle's automation to switch between the
+constructor and the destructor view in surprising ways.
The usual mixfix syntax annotations are available for both types and
constructors. For example:
@@ -530,7 +530,7 @@
mention exactly the same type variables in the same order.
@{rail \<open>
- @{syntax_def dt_ctor}: ((name | '=') ':')? name (@{syntax dt_ctor_arg} * ) \<newline>
+ @{syntax_def dt_ctor}: (name ':')? name (@{syntax dt_ctor_arg} * ) \<newline>
@{syntax dt_sel_defaults}? mixfix?
\<close>}
@@ -539,10 +539,9 @@
\noindent
The main constituents of a constructor specification are the name of the
constructor and the list of its argument types. An optional discriminator name
-can be supplied at the front to override the default name
-(@{text t.is_C\<^sub>j}). For nullary constructors @{text C\<^sub>j}, the term
-@{text "\<lambda>x. x = C\<^sub>j"} can be used as a discriminator by entering
-``@{text "="}'' (equality) instead of a name.
+can be supplied at the front to override the default, which is
+@{text "\<lambda>x. x = C\<^sub>j"} for nullary constructors and
+@{text t.is_C\<^sub>j} otherwise.
@{rail \<open>
@{syntax_def dt_ctor_arg}: type | '(' name ':' type ')'
@@ -2238,7 +2237,7 @@
primcorec
random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process"
where
- "n mod 4 = 0 \<Longrightarrow> is_Fail (random_process s f n)" |
+ "n mod 4 = 0 \<Longrightarrow> random_process s f n = Fail" |
"n mod 4 = 1 \<Longrightarrow> is_Skip (random_process s f n)" |
"n mod 4 = 2 \<Longrightarrow> is_Action (random_process s f n)" |
"n mod 4 = 3 \<Longrightarrow> is_Choice (random_process s f n)" |
@@ -2260,7 +2259,7 @@
even_infty :: even_enat and
odd_infty :: odd_enat
where
- "\<not> is_Even_EZero even_infty" |
+ "even_infty \<noteq> Even_EZero" |
"un_Even_ESuc even_infty = odd_infty" |
"un_Odd_ESuc odd_infty = even_infty"
--- a/src/HOL/Library/bnf_axiomatization.ML Mon May 26 16:32:51 2014 +0200
+++ b/src/HOL/Library/bnf_axiomatization.ML Mon May 26 16:32:55 2014 +0200
@@ -108,7 +108,7 @@
@{keyword "]"} || Scan.succeed [];
val parse_bnf_axiomatization =
- parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings --
+ parse_type_args_named_constrained -- Parse.binding -- parse_map_rel_bindings --
parse_witTs -- Parse.opt_mixfix;
val _ =
--- a/src/HOL/List.thy Mon May 26 16:32:51 2014 +0200
+++ b/src/HOL/List.thy Mon May 26 16:32:55 2014 +0200
@@ -9,7 +9,7 @@
begin
datatype_new (set: 'a) list (map: map rel: list_all2) =
- =: Nil (defaults tl: "[]") ("[]")
+ Nil (defaults tl: "[]") ("[]")
| Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
datatype_compat list
--- a/src/HOL/Nat.thy Mon May 26 16:32:51 2014 +0200
+++ b/src/HOL/Nat.thy Mon May 26 16:32:55 2014 +0200
@@ -83,7 +83,7 @@
done
free_constructors case_nat for
- =: "0 \<Colon> nat" (defaults pred: "0 \<Colon> nat")
+ "0 \<Colon> nat" (defaults pred: "0 \<Colon> nat")
| Suc pred
apply atomize_elim
apply (rename_tac n, induct_tac n rule: nat_induct0, auto)
--- a/src/HOL/Option.thy Mon May 26 16:32:51 2014 +0200
+++ b/src/HOL/Option.thy Mon May 26 16:32:55 2014 +0200
@@ -9,7 +9,7 @@
begin
datatype_new 'a option =
- =: None
+ None
| Some (the: 'a)
datatype_compat option
--- a/src/HOL/Product_Type.thy Mon May 26 16:32:51 2014 +0200
+++ b/src/HOL/Product_Type.thy Mon May 26 16:32:55 2014 +0200
@@ -12,7 +12,7 @@
subsection {* @{typ bool} is a datatype *}
-free_constructors case_bool for =: True | False
+free_constructors case_bool for True | False
by auto
text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon May 26 16:32:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon May 26 16:32:55 2014 +0200
@@ -1474,10 +1474,10 @@
(Parse.typ >> pair Binding.empty);
val parse_ctr_specs =
- Parse.enum1 "|" (parse_ctr_spec parse_binding parse_ctr_arg -- Parse.opt_mixfix);
+ Parse.enum1 "|" (parse_ctr_spec Parse.binding parse_ctr_arg -- 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_ctr_specs);
val parse_co_datatype = parse_ctr_options -- Parse.and_list1 parse_spec;
--- a/src/HOL/Tools/BNF/bnf_util.ML Mon May 26 16:32:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Mon May 26 16:32:55 2014 +0200
@@ -298,7 +298,7 @@
@{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);
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon May 26 16:32:51 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon May 26 16:32:55 2014 +0200
@@ -363,7 +363,8 @@
val ms = map length ctr_Tss;
- fun can_definitely_rely_on_disc k = not (Binding.is_empty (nth raw_disc_bindings (k - 1)));
+ fun can_definitely_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_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 can_rely_on_disc (3 - k));
@@ -380,8 +381,8 @@
|> map4 (fn k => fn m => fn ctr => fn disc =>
qualify false
(if Binding.is_empty disc then
- if should_omit_disc_binding k then disc
- else if m = 0 then equal_binding
+ if m = 0 then equal_binding
+ else if should_omit_disc_binding k then disc
else standard_disc_binding ctr
else if Binding.eq_name (disc, standard_binding) then
standard_disc_binding ctr
@@ -1005,7 +1006,7 @@
Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
prepare_free_constructors Syntax.read_term;
-val parse_bound_term = parse_binding --| @{keyword ":"} -- Parse.term;
+val parse_bound_term = Parse.binding --| @{keyword ":"} -- Parse.term;
val parse_ctr_options =
Scan.optional (@{keyword "("} |-- Parse.list1
@@ -1021,12 +1022,12 @@
parse_opt_binding_colon -- parse_ctr -- Scan.repeat parse_arg --
Scan.optional parse_defaults [];
-val parse_ctr_specs = Parse.enum1 "|" (parse_ctr_spec Parse.term parse_binding);
+val parse_ctr_specs = Parse.enum1 "|" (parse_ctr_spec Parse.term Parse.binding);
val _ =
Outer_Syntax.local_theory_to_proof @{command_spec "free_constructors"}
"register an existing freely generated type's constructors"
- (parse_ctr_options -- parse_binding --| @{keyword "for"} -- parse_ctr_specs
+ (parse_ctr_options -- Parse.binding --| @{keyword "for"} -- parse_ctr_specs
>> free_constructors_cmd);
val _ = Context.>> (Context.map_theory Ctr_Sugar_Interpretation.init);
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Mon May 26 16:32:51 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Mon May 26 16:32:55 2014 +0200
@@ -66,7 +66,6 @@
val certify: Proof.context -> term -> cterm
val standard_binding: binding
- val parse_binding: binding parser
val parse_binding_colon: binding parser
val parse_opt_binding_colon: binding parser
@@ -234,8 +233,7 @@
binding at all, depending on the context. *)
val standard_binding = @{binding _};
-val parse_binding = Parse.binding || @{keyword "="} >> K equal_binding;
-val parse_binding_colon = parse_binding --| @{keyword ":"};
+val parse_binding_colon = Parse.binding --| @{keyword ":"};
val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty;
fun ss_only thms ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps thms;