# 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 \ nat", Suc] case_nat [=] [[], [pred]] [[pred: "0 \ nat"]] +free_constructors case_nat for + =: "0 \ nat" (defaults pred: "0 \ 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: "(\a b. P (Pair a b)) \ 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 \ 'b" show "(\x1 x2. p = Pair x1 x2 \ P) \ 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;