# HG changeset patch
# User blanchet
# Date 1392360826 -3600
# Node ID b19dd108f0c228cf7ef14db2ecf26c4a61acf738
# Parent  98b25c51e9e58131640ab2d4ec266fef214ec864
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax

diff -r 98b25c51e9e5 -r b19dd108f0c2 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Nat.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -82,7 +82,9 @@
 apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
 done
 
-free_constructors ["0 \<Colon> nat", Suc] case_nat [=] [[], [pred]] [[pred: "0 \<Colon> nat"]]
+free_constructors case_nat for
+    =: "0 \<Colon> nat" (defaults pred: "0 \<Colon> nat")
+  | Suc pred
   apply atomize_elim
   apply (rename_tac n, induct_tac n rule: nat_induct0, auto)
  apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI
diff -r 98b25c51e9e5 -r b19dd108f0c2 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Product_Type.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -12,7 +12,7 @@
 
 subsection {* @{typ bool} is a datatype *}
 
-free_constructors [True, False] case_bool [=]
+free_constructors case_bool for =: True | False
 by auto
 
 text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
@@ -82,7 +82,7 @@
     else SOME (mk_meta_eq @{thm unit_eq})
 *}
 
-free_constructors ["()"] case_unit
+free_constructors case_unit for "()"
 by auto
 
 text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
@@ -184,7 +184,7 @@
 lemma prod_cases: "(\<And>a b. P (Pair a b)) \<Longrightarrow> P p"
   by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
 
-free_constructors [Pair] case_prod [] [[fst, snd]]
+free_constructors case_prod for Pair fst snd
 proof -
   fix P :: bool and p :: "'a \<times> 'b"
   show "(\<And>x1 x2. p = Pair x1 x2 \<Longrightarrow> P) \<Longrightarrow> P"
diff -r 98b25c51e9e5 -r b19dd108f0c2 src/HOL/Sum_Type.thy
--- a/src/HOL/Sum_Type.thy	Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Sum_Type.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -85,7 +85,9 @@
   with assms show P by (auto simp add: sum_def Inl_def Inr_def)
 qed
 
-free_constructors [Inl, Inr] case_sum [isl] [[projl], [projr]]
+free_constructors case_sum for
+    isl: Inl projl
+  | Inr projr
 by (erule sumE, assumption) (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
 
 text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
diff -r 98b25c51e9e5 -r b19dd108f0c2 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
@@ -92,12 +92,15 @@
     typ list -> typ list list list -> int list list -> int list list -> int list -> thm list list ->
     Ctr_Sugar.ctr_sugar list -> term list list -> thm list list -> (thm list -> thm list) ->
     local_theory -> gfp_sugar_thms
+
+  type co_datatype_spec =
+    ((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix)
+    * ((binding, binding * typ, term) Ctr_Sugar.ctr_spec * mixfix) list
+
   val co_datatypes: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
       binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
       BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) ->
-    (bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding))
-      * mixfix) * ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
-        mixfix) list) list ->
+    (bool * bool) * co_datatype_spec list ->
     local_theory -> local_theory
   val parse_co_datatype_cmd: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
       binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
@@ -310,18 +313,16 @@
   reassoc_conjs (thm RS @{thm conj_assoc[THEN iffD1]})
   handle THM _ => thm;
 
-fun type_args_named_constrained_of ((((ncAs, _), _), _), _) = ncAs;
-fun type_binding_of ((((_, b), _), _), _) = b;
-fun map_binding_of (((_, (b, _)), _), _) = b;
-fun rel_binding_of (((_, (_, b)), _), _) = b;
-fun mixfix_of ((_, mx), _) = mx;
-fun ctr_specs_of (_, ctr_specs) = ctr_specs;
+type co_datatype_spec =
+  ((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix)
+  * ((binding, binding * typ, term) ctr_spec * mixfix) list;
 
-fun disc_of ((((disc, _), _), _), _) = disc;
-fun ctr_of ((((_, ctr), _), _), _) = ctr;
-fun args_of (((_, args), _), _) = args;
-fun defaults_of ((_, ds), _) = ds;
-fun ctr_mixfix_of (_, mx) = mx;
+fun type_args_named_constrained_of_spec ((((ncAs, _), _), _), _) = ncAs;
+fun type_binding_of_spec ((((_, b), _), _), _) = b;
+fun map_binding_of_spec (((_, (b, _)), _), _) = b;
+fun rel_binding_of_spec (((_, (_, b)), _), _) = b;
+fun mixfix_of_spec ((_, mx), _) = mx;
+fun mixfixed_ctr_specs_of_spec (_, mx_ctr_specs) = mx_ctr_specs;
 
 fun add_nesty_bnf_names Us =
   let
@@ -991,22 +992,22 @@
         ();
 
     val nn = length specs;
-    val fp_bs = map type_binding_of specs;
+    val fp_bs = map type_binding_of_spec specs;
     val fp_b_names = map Binding.name_of fp_bs;
     val fp_common_name = mk_common_name fp_b_names;
-    val map_bs = map map_binding_of specs;
-    val rel_bs = map rel_binding_of specs;
+    val map_bs = map map_binding_of_spec specs;
+    val rel_bs = map rel_binding_of_spec specs;
 
     fun prepare_type_arg (_, (ty, c)) =
       let val TFree (s, _) = prepare_typ no_defs_lthy0 ty in
         TFree (s, prepare_constraint no_defs_lthy0 c)
       end;
 
-    val Ass0 = map (map prepare_type_arg o type_args_named_constrained_of) specs;
+    val Ass0 = map (map prepare_type_arg o type_args_named_constrained_of_spec) specs;
     val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0;
     val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0;
     val num_As = length unsorted_As;
-    val set_bss = map (map fst o type_args_named_constrained_of) specs;
+    val set_bss = map (map fst o type_args_named_constrained_of_spec) specs;
 
     val (((Bs0, Cs), Xs), no_defs_lthy) =
       no_defs_lthy0
@@ -1015,7 +1016,8 @@
       ||>> mk_TFrees nn
       ||>> variant_tfrees fp_b_names;
 
-    fun add_fake_type spec = Typedecl.basic_typedecl (type_binding_of spec, num_As, mixfix_of spec);
+    fun add_fake_type spec =
+      Typedecl.basic_typedecl (type_binding_of_spec spec, num_As, mixfix_of_spec spec);
 
     val (fake_T_names, fake_lthy) = fold_map add_fake_type specs no_defs_lthy0;
 
@@ -1032,22 +1034,24 @@
       error ("Locally fixed type argument " ^ qsoty (hd bad_args) ^ " in " ^ co_prefix fp ^
         "datatype specification");
 
-    val mixfixes = map mixfix_of specs;
+    val mixfixes = map mixfix_of_spec specs;
 
     val _ = (case Library.duplicates Binding.eq_name fp_bs of [] => ()
       | b :: _ => error ("Duplicate type name declaration " ^ quote (Binding.name_of b)));
 
-    val ctr_specss = map ctr_specs_of specs;
+    val mx_ctr_specss = map mixfixed_ctr_specs_of_spec specs;
+    val ctr_specss = map (map fst) mx_ctr_specss;
+    val ctr_mixfixess = map (map snd) mx_ctr_specss;
 
-    val disc_bindingss = map (map disc_of) ctr_specss;
+    val disc_bindingss = map (map disc_of_ctr_spec) ctr_specss;
     val ctr_bindingss =
-      map2 (fn fp_b_name => map (Binding.qualify false fp_b_name o ctr_of)) fp_b_names ctr_specss;
-    val ctr_argsss = map (map args_of) ctr_specss;
-    val ctr_mixfixess = map (map ctr_mixfix_of) ctr_specss;
+      map2 (fn fp_b_name => map (Binding.qualify false fp_b_name o ctr_of_ctr_spec)) fp_b_names
+        ctr_specss;
+    val ctr_argsss = map (map args_of_ctr_spec) ctr_specss;
 
     val sel_bindingsss = map (map (map fst)) ctr_argsss;
     val fake_ctr_Tsss0 = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss;
-    val raw_sel_defaultsss = map (map defaults_of) ctr_specss;
+    val raw_sel_defaultsss = map (map sel_defaults_of_ctr_spec) ctr_specss;
 
     val (As :: _) :: fake_ctr_Tsss =
       burrow (burrow (Syntax.check_typs fake_lthy)) (Ass0 :: fake_ctr_Tsss0);
@@ -1249,9 +1253,11 @@
             val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss;
 
             val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss
+
+            fun ctr_spec_of disc_b ctr0 sel_bs sel_defs = (((disc_b, ctr0), sel_bs), sel_defs);
+            val ctr_specs = map4 ctr_spec_of disc_bindings ctrs0 sel_bindingss sel_defaultss;
           in
-            free_constructors tacss (((wrap_opts, ctrs0), standard_binding), (disc_bindings,
-              (sel_bindingss, sel_defaultss))) lthy
+            free_constructors tacss ((wrap_opts, standard_binding), ctr_specs) lthy
           end;
 
         fun derive_maps_sets_rels (ctr_sugar as {case_cong, ...} : ctr_sugar, lthy) =
@@ -1500,13 +1506,6 @@
 fun co_datatype_cmd x =
   define_co_datatypes Typedecl.read_constraint Syntax.parse_typ Syntax.parse_term x;
 
-val parse_ctr_arg =
-  @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} ||
-  (Parse.typ >> pair Binding.empty);
-
-val parse_defaults =
-  @{keyword "("} |-- Parse.reserved "defaults" |-- Scan.repeat parse_bound_term --| @{keyword ")"};
-
 val parse_type_arg_constrained =
   Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort);
 
@@ -1519,15 +1518,18 @@
   @{keyword "("} |-- Parse.!!! (Parse.list1 parse_type_arg_named_constrained --| @{keyword ")"}) ||
   Scan.succeed [];
 
-val parse_ctr_spec =
-  parse_opt_binding_colon -- parse_binding -- Scan.repeat parse_ctr_arg --
-  Scan.optional parse_defaults [] -- Parse.opt_mixfix;
+val parse_ctr_arg =
+  @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} ||
+  (Parse.typ >> pair Binding.empty);
+
+val parse_ctr_specs =
+  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.opt_mixfix -- (@{keyword "="} |-- Parse.enum1 "|" parse_ctr_spec);
+  Parse.opt_mixfix -- (@{keyword "="} |-- parse_ctr_specs);
 
-val parse_co_datatype = parse_free_constructors_options -- Parse.and_list1 parse_spec;
+val parse_co_datatype = parse_ctr_options -- Parse.and_list1 parse_spec;
 
 fun parse_co_datatype_cmd fp construct_fp = parse_co_datatype >> co_datatype_cmd fp construct_fp;
 
diff -r 98b25c51e9e5 -r b19dd108f0c2 src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Fri Feb 14 07:53:46 2014 +0100
@@ -137,8 +137,6 @@
 
   val fold_thms: Proof.context -> thm list -> thm -> thm
 
-  val parse_binding_colon: binding parser
-  val parse_opt_binding_colon: binding parser
   val parse_type_args_named_constrained: (binding option * (string * string option)) list parser
   val parse_map_rel_bindings: (binding * binding) parser
 
@@ -267,9 +265,6 @@
     let val (xs1, xs2, xs3, xs4, xs5) = split_list5 xs;
     in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5) end;
 
-val parse_binding_colon = parse_binding --| @{keyword ":"};
-val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty;
-
 val parse_type_arg_constrained =
   Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort);
 
diff -r 98b25c51e9e5 -r b19dd108f0c2 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
@@ -53,12 +53,19 @@
   val dest_case: Proof.context -> string -> typ list -> term ->
     (ctr_sugar * term list * term list) option
 
+  type ('c, 'a, 'v) ctr_spec = ((binding * 'c) * 'a list) * (binding * 'v) list
+
+  val disc_of_ctr_spec: ('c, 'a, 'v) ctr_spec -> binding
+  val ctr_of_ctr_spec: ('c, 'a, 'v) ctr_spec -> 'c
+  val args_of_ctr_spec: ('c, 'a, 'v) ctr_spec -> 'a list
+  val sel_defaults_of_ctr_spec: ('c, 'a, 'v) ctr_spec -> (binding * 'v) list
+
   val free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
-    (((bool * bool) * term list) * binding) *
-      (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
+    ((bool * bool) * binding) * (term, binding, term) ctr_spec list -> local_theory ->
     ctr_sugar * local_theory
-  val parse_free_constructors_options: (bool * bool) parser
   val parse_bound_term: (binding * string) parser
+  val parse_ctr_options: (bool * bool) parser
+  val parse_ctr_spec: 'c parser -> 'a parser -> ('c, 'a, string) ctr_spec parser
 end;
 
 structure Ctr_Sugar : CTR_SUGAR =
@@ -278,11 +285,23 @@
 
 fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
 
-fun prepare_free_constructors prep_term ((((no_discs_sels, no_code), raw_ctrs), raw_case_binding),
-    (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
+type ('c, 'a, 'v) ctr_spec = ((binding * 'c) * 'a list) * (binding * 'v) list;
+
+fun disc_of_ctr_spec (((disc, _), _), _) = disc;
+fun ctr_of_ctr_spec (((_, ctr), _), _) = ctr;
+fun args_of_ctr_spec ((_, args), _) = args;
+fun sel_defaults_of_ctr_spec (_, ds) = ds;
+
+fun prepare_free_constructors prep_term (((no_discs_sels, no_code), raw_case_binding), ctr_specs)
+    no_defs_lthy =
   let
     (* TODO: sanity checks on arguments *)
 
+    val raw_ctrs = map ctr_of_ctr_spec ctr_specs;
+    val raw_disc_bindings = map disc_of_ctr_spec ctr_specs;
+    val raw_sel_bindingss = map args_of_ctr_spec ctr_specs;
+    val raw_sel_defaultss = map sel_defaults_of_ctr_spec ctr_specs;
+
     val n = length raw_ctrs;
     val ks = 1 upto n;
 
@@ -954,29 +973,28 @@
   Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
   prepare_free_constructors Syntax.read_term;
 
-fun parse_bracket_list parser = @{keyword "["} |-- Parse.list parser --|  @{keyword "]"};
-
-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;
-
-val parse_free_constructors_options =
+val parse_ctr_options =
   Scan.optional (@{keyword "("} |-- Parse.list1
         (Parse.reserved "no_discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1) --|
       @{keyword ")"}
       >> (fn js => (member (op =) js 0, member (op =) js 1)))
     (false, false);
 
+val parse_defaults =
+  @{keyword "("} |-- Parse.reserved "defaults" |-- Scan.repeat parse_bound_term --| @{keyword ")"};
+
+fun parse_ctr_spec parse_ctr parse_arg =
+  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 _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "free_constructors"}
     "register an existing freely generated type's constructors"
-    ((parse_free_constructors_options -- (@{keyword "["} |-- Parse.list Parse.term --|
-        @{keyword "]"}) --
-      parse_binding -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss --
-        Scan.optional parse_bound_termss []) ([], [])) ([], ([], [])))
+    (parse_ctr_options -- parse_binding --| @{keyword "for"} -- parse_ctr_specs
      >> free_constructors_cmd);
 
 end;
diff -r 98b25c51e9e5 -r b19dd108f0c2 src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Feb 14 07:53:46 2014 +0100
@@ -65,6 +65,8 @@
   val standard_binding: binding
   val equal_binding: binding
   val parse_binding: binding parser
+  val parse_binding_colon: binding parser
+  val parse_opt_binding_colon: binding parser
 
   val ss_only: thm list -> Proof.context -> Proof.context
 
@@ -219,6 +221,8 @@
 val equal_binding = @{binding "="};
 
 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;
 
 fun ss_only thms ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps thms;