# HG changeset patch # User blanchet # Date 1409870461 -7200 # Node ID 9d714be4f02827e8462b89d3d873b10cf3d56212 # Parent cc71d2be4f0acce777751469fdd4406bf3c0e6f6 added 'plugins' option to control which hooks are enabled diff -r cc71d2be4f0a -r 9d714be4f028 src/HOL/Library/bnf_axiomatization.ML --- a/src/HOL/Library/bnf_axiomatization.ML Fri Sep 05 00:41:01 2014 +0200 +++ b/src/HOL/Library/bnf_axiomatization.ML Fri Sep 05 00:41:01 2014 +0200 @@ -7,8 +7,8 @@ signature BNF_AXIOMATIZATION = sig - val bnf_axiomatization: (binding option * (typ * sort)) list -> binding -> mixfix -> binding -> - binding -> typ list -> local_theory -> BNF_Def.bnf * local_theory + val bnf_axiomatization: (string -> bool) -> (binding option * (typ * sort)) list -> binding -> + mixfix -> binding -> binding -> typ list -> local_theory -> BNF_Def.bnf * local_theory end structure BNF_Axiomatization : BNF_AXIOMATIZATION = @@ -17,7 +17,8 @@ open BNF_Util open BNF_Def -fun prepare_decl prepare_constraint prepare_typ raw_vars b mx user_mapb user_relb user_witTs lthy = +fun prepare_decl prepare_constraint prepare_typ plugins raw_vars b mx user_mapb user_relb user_witTs + lthy = let fun prepare_type_arg (set_opt, (ty, c)) = let val s = fst (dest_TFree (prepare_typ lthy ty)) in @@ -46,14 +47,14 @@ val mapT = map2 (curry op -->) lives lives' ---> T --> T'; val setTs = map (fn U => T --> HOLogic.mk_setT U) lives; val bdT = BNF_Util.mk_relT (bd_type_T, bd_type_T); - val mapb = mk_b BNF_Def.mapN user_mapb; + val mapb = mk_b mapN user_mapb; val bdb = mk_b "bd" Binding.empty; - val setbs = map2 (fn b => fn i => mk_b (BNF_Def.mk_setN i) b) user_setbs + val setbs = map2 (fn b => fn i => mk_b (mk_setN i) b) user_setbs (if live = 1 then [0] else 1 upto live); val witTs = map (prepare_typ lthy) user_witTs; val nwits = length witTs; - val witbs = map (fn i => mk_b (BNF_Def.mk_witN i) Binding.empty) + val witbs = map (fn i => mk_b (mk_witN i) Binding.empty) (if nwits = 1 then [0] else 1 upto nwits); val lthy = Local_Theory.background_theory @@ -91,7 +92,7 @@ val (bnf, lthy') = after_qed mk_wit_thms thms lthy in - (bnf, BNF_Def.register_bnf (K true) key bnf lthy') + (bnf, register_bnf plugins key bnf lthy') end; val bnf_axiomatization = prepare_decl (K I) (K I); @@ -107,14 +108,17 @@ | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --| @{keyword "]"} || Scan.succeed []; +val parse_bnf_axiomatization_options = + Scan.optional (@{keyword "("} |-- parse_plugins --| @{keyword ")"}) (K true); + val parse_bnf_axiomatization = - parse_type_args_named_constrained -- Parse.binding -- parse_witTs -- Parse.opt_mixfix -- - parse_map_rel_bindings; + parse_bnf_axiomatization_options -- parse_type_args_named_constrained -- Parse.binding -- + parse_witTs -- Parse.opt_mixfix -- parse_map_rel_bindings; val _ = Outer_Syntax.local_theory @{command_spec "bnf_axiomatization"} "bnf declaration" (parse_bnf_axiomatization >> - (fn ((((bsTs, b), witTs), mx), (mapb, relb)) => - bnf_axiomatization_cmd bsTs b mx mapb relb witTs #> snd)); + (fn (((((plugins, bsTs), b), witTs), mx), (mapb, relb)) => + bnf_axiomatization_cmd plugins bsTs b mx mapb relb witTs #> snd)); end; diff -r cc71d2be4f0a -r 9d714be4f028 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Fri Sep 05 00:41:01 2014 +0200 +++ b/src/HOL/Nat.thy Fri Sep 05 00:41:01 2014 +0200 @@ -89,12 +89,12 @@ | Suc pred where "pred (0 \ nat) = (0 \ nat)" - 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 - Suc_Rep_inject' Rep_Nat_inject) -apply (simp only: Suc_not_Zero) -done + 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 Suc_Rep_inject' + Rep_Nat_inject) + apply (simp only: Suc_not_Zero) + done -- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *} setup {* Sign.mandatory_path "old" *} diff -r cc71d2be4f0a -r 9d714be4f028 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Fri Sep 05 00:41:01 2014 +0200 +++ b/src/HOL/Product_Type.thy Fri Sep 05 00:41:01 2014 +0200 @@ -13,7 +13,7 @@ subsection {* @{typ bool} is a datatype *} free_constructors case_bool for True | False -by auto + by auto text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *} @@ -82,7 +82,7 @@ *} free_constructors case_unit for "()" -by auto + by auto text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *} diff -r cc71d2be4f0a -r 9d714be4f028 src/HOL/Sum_Type.thy --- a/src/HOL/Sum_Type.thy Fri Sep 05 00:41:01 2014 +0200 +++ b/src/HOL/Sum_Type.thy Fri Sep 05 00:41:01 2014 +0200 @@ -88,7 +88,7 @@ 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) + 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 cc71d2be4f0a -r 9d714be4f028 src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Fri Sep 05 00:41:01 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Fri Sep 05 00:41:01 2014 +0200 @@ -122,11 +122,9 @@ (binding -> binding) -> (Proof.context -> 'a -> typ) -> (Proof.context -> 'b -> term) -> typ list option -> binding -> binding -> binding list -> (((((binding * 'a) * 'b) * 'b list) * 'b) * 'b list) * 'b option -> Proof.context -> - string * term list * - ((Proof.context -> thm list -> tactic) option * term list list) * + string * term list * ((Proof.context -> thm list -> tactic) option * term list list) * ((thm list -> thm list list) -> thm list list -> Proof.context -> bnf * local_theory) * local_theory * thm list - val define_bnf_consts: inline_policy -> fact_policy -> bool -> typ list option -> binding -> binding -> binding list -> (((((binding * typ) * term) * term list) * term) * term list) * term option -> local_theory -> @@ -140,11 +138,10 @@ (typ list -> typ list -> typ list -> term))) * local_theory val bnf_def: inline_policy -> (Proof.context -> fact_policy) -> bool -> (binding -> binding) -> - (Proof.context -> tactic) list -> - (Proof.context -> tactic) -> typ list option -> binding -> + (Proof.context -> tactic) list -> (Proof.context -> tactic) -> typ list option -> binding -> binding -> binding list -> - (((((binding * typ) * term) * term list) * term) * term list) * term option -> - local_theory -> bnf * local_theory + (((((binding * typ) * term) * term list) * term) * term list) * term option -> local_theory -> + bnf * local_theory end; structure BNF_Def : BNF_DEF = @@ -1532,10 +1529,10 @@ Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf))); -fun register_bnf keep key bnf = - register_bnf_raw key bnf #> interpret_bnf keep bnf; +fun register_bnf plugins key bnf = + register_bnf_raw key bnf #> interpret_bnf plugins bnf; -fun bnf_def const_policy fact_policy internal qualify tacs wit_tac Ds map_b rel_b set_bs = +fun bnf_def const_policy fact_policy internal qualify tacs wit_tac Ds map_b rel_b set_bs raw_csts = (fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) => let fun mk_wits_tac ctxt set_maps = @@ -1555,9 +1552,11 @@ goals (map (fn tac => fn {context = ctxt, prems = _} => unfold_thms_tac ctxt one_step_defs THEN tac ctxt) tacs) |> (fn thms => after_qed mk_wit_thms (map single thms) lthy) - end) oo prepare_def const_policy fact_policy internal qualify (K I) (K I) Ds map_b rel_b set_bs; + end) o prepare_def const_policy fact_policy internal qualify (K I) (K I) Ds map_b rel_b set_bs + raw_csts; -val bnf_cmd = (fn (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, defs) => +fun bnf_cmd (raw_csts, plugins) = + (fn (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, defs) => let val wit_goals = map Logic.mk_conjunction_balanced wit_goalss; fun mk_triv_wit_thms tac set_maps = @@ -1572,10 +1571,10 @@ | SOME tac => (mk_triv_wit_thms tac, [])); in Proof.unfolding ([[(defs, [])]]) - (Proof.theorem NONE (uncurry (register_bnf (K true) key) oo after_qed mk_wit_thms) + (Proof.theorem NONE (uncurry (register_bnf plugins key) oo after_qed mk_wit_thms) (map (single o rpair []) goals @ nontriv_wit_goals) lthy) - end) oo prepare_def Do_Inline (user_policy Note_Some) false I Syntax.read_typ Syntax.read_term - NONE Binding.empty Binding.empty []; + end) o prepare_def Do_Inline (user_policy Note_Some) false I Syntax.read_typ Syntax.read_term + NONE Binding.empty Binding.empty [] raw_csts; fun print_bnfs ctxt = let @@ -1611,12 +1610,13 @@ "register a type as a bounded natural functor" (parse_opt_binding_colon -- Parse.typ --| (Parse.reserved "map" -- @{keyword ":"}) -- Parse.term -- - (Scan.option ((Parse.reserved "sets" -- @{keyword ":"}) |-- - Scan.repeat1 (Scan.unless (Parse.reserved "bd") Parse.term)) >> the_default []) --| + Scan.optional ((Parse.reserved "sets" -- @{keyword ":"}) |-- + Scan.repeat1 (Scan.unless (Parse.reserved "bd") Parse.term)) [] --| (Parse.reserved "bd" -- @{keyword ":"}) -- Parse.term -- - (Scan.option ((Parse.reserved "wits" -- @{keyword ":"}) |-- - Scan.repeat1 (Scan.unless (Parse.reserved "rel") Parse.term)) >> the_default []) -- - Scan.option ((Parse.reserved "rel" -- @{keyword ":"}) |-- Parse.term) + Scan.optional ((Parse.reserved "wits" -- @{keyword ":"}) |-- + Scan.repeat1 (Scan.unless (Parse.reserved "rel") Parse.term)) [] -- + Scan.option ((Parse.reserved "rel" -- @{keyword ":"}) |-- Parse.term) -- + Scan.optional parse_plugins (K true) >> bnf_cmd); val _ = Context.>> (Context.map_theory BNF_Interpretation.init); diff -r cc71d2be4f0a -r 9d714be4f028 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 05 00:41:01 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 05 00:41:01 2014 +0200 @@ -104,7 +104,7 @@ binding list list -> binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory -> BNF_FP_Util.fp_result * local_theory) -> - (bool * bool) + Ctr_Sugar.ctr_options * ((((((binding option * (typ * sort)) list * binding) * mixfix) * ((binding, binding * typ) Ctr_Sugar.ctr_spec * mixfix) list) * (binding * binding)) * term list) list -> @@ -236,10 +236,10 @@ (fn phi => Data.map (Symtab.update (s, morph_fp_sugar phi fp_sugar)))) fp_sugars; -fun register_fp_sugars keep fp_sugars = - register_fp_sugars_raw fp_sugars #> interpret_fp_sugars keep fp_sugars; +fun register_fp_sugars plugins fp_sugars = + register_fp_sugars_raw fp_sugars #> interpret_fp_sugars plugins fp_sugars; -fun interpret_bnfs_register_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs +fun interpret_bnfs_register_fp_sugars plugins Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs mapss common_co_inducts co_inductss co_rec_thmss co_rec_discss co_rec_selsss rel_injectss rel_distinctss noted = @@ -258,8 +258,8 @@ |> morph_fp_sugar (substitute_noted_thm noted)) Ts; in register_fp_sugars_raw fp_sugars - #> fold (interpret_bnf (K true)) (#bnfs fp_res) - #> interpret_fp_sugars (K true) fp_sugars + #> fold (interpret_bnf plugins) (#bnfs fp_res) + #> interpret_fp_sugars plugins fp_sugars end; (* This function could produce (fairly harmless) clashes in contrived examples (e.g., "x.A", @@ -1166,7 +1166,7 @@ end; fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp - ((discs_sels0, no_code), specs) no_defs_lthy0 = + ((plugins, (discs_sels0, no_code)), specs) no_defs_lthy0 = let (* TODO: sanity checks on arguments *) @@ -1458,8 +1458,8 @@ fun ctr_spec_of disc_b ctr0 sel_bs = ((disc_b, ctr0), sel_bs); val ctr_specs = map3 ctr_spec_of disc_bindings ctrs0 sel_bindingss; in - free_constructors tacss ((((discs_sels, no_code), standard_binding), ctr_specs), - sel_default_eqs) lthy + free_constructors tacss ((((plugins, (discs_sels, no_code)), standard_binding), + ctr_specs), sel_default_eqs) lthy end; fun derive_maps_sets_rels (ctr_sugar as {casex, case_cong, case_thms, discs, selss, ctrs, @@ -2054,7 +2054,7 @@ (* for "datatype_realizer.ML": *) |>> name_noted_thms (fst (dest_Type (hd fpTs)) ^ (implode (map (prefix "_") (tl fp_b_names)))) inductN - |-> interpret_bnfs_register_fp_sugars fpTs fpBTs Xs Least_FP pre_bnfs absT_infos + |-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Least_FP pre_bnfs absT_infos fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs mapss [induct_thm] (map single induct_thms) rec_thmss (replicate nn []) (replicate nn []) rel_injectss rel_distinctss @@ -2146,7 +2146,7 @@ |> fold (curry (Spec_Rules.add Spec_Rules.Equational) corecs) [flat corec_sel_thmss, flat corec_thmss] |> Local_Theory.notes (common_notes @ notes) - |-> interpret_bnfs_register_fp_sugars fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos + |-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs mapss [coinduct_thm, coinduct_strong_thm] (transpose [coinduct_thms, coinduct_strong_thms]) corec_thmss corec_disc_thmss diff -r cc71d2be4f0a -r 9d714be4f028 src/HOL/Tools/BNF/bnf_lfp_compat.ML --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Fri Sep 05 00:41:01 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Fri Sep 05 00:41:01 2014 +0200 @@ -357,7 +357,7 @@ in (fpT_names, thy - |> map_local_theory (co_datatypes Least_FP construct_lfp ((false, false), new_specs)) + |> map_local_theory (co_datatypes Least_FP construct_lfp (default_ctr_options, new_specs)) |> nesting_pref = Unfold_Nesting ? perhaps (try (datatype_compat_global fpT_names))) end; diff -r cc71d2be4f0a -r 9d714be4f028 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Sep 05 00:41:01 2014 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Sep 05 00:41:01 2014 +0200 @@ -69,12 +69,15 @@ val ctr_of_ctr_spec: ('c, 'a) ctr_spec -> 'c val args_of_ctr_spec: ('c, 'a) ctr_spec -> 'a list + type ctr_options = (string -> bool) * (bool * bool) + val fake_local_theory_for_sel_defaults: (binding * typ) list -> Proof.context -> Proof.context val free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list -> - (((bool * bool) * binding) * (term, binding) ctr_spec list) * term list -> local_theory -> + ((ctr_options * binding) * (term, binding) ctr_spec list) * term list -> local_theory -> ctr_sugar * local_theory + val default_ctr_options: ctr_options val parse_bound_term: (binding * string) parser - val parse_ctr_options: (bool * bool) parser + val parse_ctr_options: ctr_options parser val parse_ctr_spec: 'c parser -> 'a parser -> ('c, 'a) ctr_spec parser val parse_sel_default_eqs: string list parser end; @@ -193,17 +196,17 @@ Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Data.map (Symtab.update (s, morph_ctr_sugar phi ctr_sugar))); -fun register_ctr_sugar keep ctr_sugar = - register_ctr_sugar_raw ctr_sugar #> interpret_ctr_sugar keep ctr_sugar; +fun register_ctr_sugar plugins ctr_sugar = + register_ctr_sugar_raw ctr_sugar #> interpret_ctr_sugar plugins ctr_sugar; -fun default_register_ctr_sugar_global keep (ctr_sugar as {T = Type (s, _), ...}) thy = +fun default_register_ctr_sugar_global plugins (ctr_sugar as {T = Type (s, _), ...}) thy = let val tab = Data.get (Context.Theory thy) in if Symtab.defined tab s then thy else thy |> Context.theory_map (Data.put (Symtab.update_new (s, ctr_sugar) tab)) - |> Ctr_Sugar_Interpretation.data_global keep ctr_sugar + |> Ctr_Sugar_Interpretation.data_global plugins ctr_sugar end; val isN = "is_"; @@ -359,8 +362,8 @@ fun ctr_of_ctr_spec ((_, ctr), _) = ctr; fun args_of_ctr_spec (_, args) = args; -fun prepare_free_constructors prep_term - ((((discs_sels, no_code), raw_case_binding), ctr_specs), sel_default_eqs) no_defs_lthy = +fun prepare_free_constructors prep_term ((((plugins, (discs_sels, no_code)), raw_case_binding), + ctr_specs), sel_default_eqs) no_defs_lthy = let (* TODO: sanity checks on arguments *) @@ -1045,7 +1048,7 @@ case_eq_ifs = case_eq_if_thms} |> morph_ctr_sugar (substitute_noted_thm noted); in - (ctr_sugar, lthy' |> register_ctr_sugar (K true) ctr_sugar) + (ctr_sugar, lthy' |> register_ctr_sugar plugins ctr_sugar) end; in (goalss, after_qed, lthy') @@ -1061,12 +1064,18 @@ val parse_bound_term = Parse.binding --| @{keyword ":"} -- Parse.term; +type ctr_options = (string -> bool) * (bool * bool) + +val default_ctr_options = (K true, (false, false)); + val parse_ctr_options = Scan.optional (@{keyword "("} |-- Parse.list1 - (Parse.reserved "discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1) --| + (parse_plugins >> (apfst o K) + || Parse.reserved "discs_sels" >> (apsnd o apfst o K o K true) + || Parse.reserved "no_code" >> (apsnd o apsnd o K o K true)) --| @{keyword ")"} - >> (fn js => (member (op =) js 0, member (op =) js 1))) - (false, false); + >> (fn fs => fold I fs default_ctr_options)) + default_ctr_options; fun parse_ctr_spec parse_ctr parse_arg = parse_opt_binding_colon -- parse_ctr -- Scan.repeat parse_arg; diff -r cc71d2be4f0a -r 9d714be4f028 src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Fri Sep 05 00:41:01 2014 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Fri Sep 05 00:41:01 2014 +0200 @@ -76,6 +76,7 @@ val standard_binding: binding val parse_binding_colon: binding parser val parse_opt_binding_colon: binding parser + val parse_plugins: (string -> bool) parser val ss_only: thm list -> Proof.context -> Proof.context @@ -268,6 +269,11 @@ val parse_binding_colon = Parse.binding --| @{keyword ":"}; val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty; +val parse_plugins = + Parse.reserved "plugins" |-- + ((Parse.reserved "only" >> K I || Parse.reserved "del" >> K not) --| @{keyword ":"} + -- Scan.repeat Parse.short_ident) >> (fn (modif, ss) => modif o member (op =) ss); + fun ss_only thms ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps thms; (*Tactical WRAP surrounds a static given tactic (core) with two deterministic chains of tactics*)