aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
--- 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
--- 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"
--- 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}. *}
--- 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;
--- 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);
--- 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;
--- 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;