# HG changeset patch # User blanchet # Date 1401114775 -7200 # Node ID 1fa9c19ba2c9269dff764efadc523e057dac897a # Parent 0224caba67caa4f7b9c507729431bb852c753860 got rid of '=:' squiggly diff -r 0224caba67ca -r 1fa9c19ba2c9 NEWS --- 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 diff -r 0224caba67ca -r 1fa9c19ba2c9 src/Doc/Datatypes/Datatypes.thy --- 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 "\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 "\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 \ - @{syntax_def dt_ctor}: ((name | '=') ':')? name (@{syntax dt_ctor_arg} * ) \ + @{syntax_def dt_ctor}: (name ':')? name (@{syntax dt_ctor_arg} * ) \ @{syntax dt_sel_defaults}? mixfix? \} @@ -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 "\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 "\x. x = C\<^sub>j"} for nullary constructors and +@{text t.is_C\<^sub>j} otherwise. @{rail \ @{syntax_def dt_ctor_arg}: type | '(' name ':' type ')' @@ -2238,7 +2237,7 @@ primcorec random_process :: "'a stream \ (int \ int) \ int \ 'a process" where - "n mod 4 = 0 \ is_Fail (random_process s f n)" | + "n mod 4 = 0 \ random_process s f n = Fail" | "n mod 4 = 1 \ is_Skip (random_process s f n)" | "n mod 4 = 2 \ is_Action (random_process s f n)" | "n mod 4 = 3 \ is_Choice (random_process s f n)" | @@ -2260,7 +2259,7 @@ even_infty :: even_enat and odd_infty :: odd_enat where - "\ is_Even_EZero even_infty" | + "even_infty \ Even_EZero" | "un_Even_ESuc even_infty = odd_infty" | "un_Odd_ESuc odd_infty = even_infty" diff -r 0224caba67ca -r 1fa9c19ba2c9 src/HOL/Library/bnf_axiomatization.ML --- 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 _ = diff -r 0224caba67ca -r 1fa9c19ba2c9 src/HOL/List.thy --- 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 diff -r 0224caba67ca -r 1fa9c19ba2c9 src/HOL/Nat.thy --- 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 \ nat" (defaults pred: "0 \ nat") + "0 \ nat" (defaults pred: "0 \ nat") | Suc pred apply atomize_elim apply (rename_tac n, induct_tac n rule: nat_induct0, auto) diff -r 0224caba67ca -r 1fa9c19ba2c9 src/HOL/Option.thy --- 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 diff -r 0224caba67ca -r 1fa9c19ba2c9 src/HOL/Product_Type.thy --- 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}. *} diff -r 0224caba67ca -r 1fa9c19ba2c9 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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; diff -r 0224caba67ca -r 1fa9c19ba2c9 src/HOL/Tools/BNF/bnf_util.ML --- 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); diff -r 0224caba67ca -r 1fa9c19ba2c9 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- 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); diff -r 0224caba67ca -r 1fa9c19ba2c9 src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML --- 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;