# HG changeset patch # User wenzelm # Date 1575295478 -3600 # Node ID 5727bcc3c47c826296a077f748d995f843fcb5bb # Parent 39ccdbbed539312edf16025db987a163986ebcbf proper spec_rule name via naming/binding/Morphism.binding; diff -r 39ccdbbed539 -r 5727bcc3c47c src/HOL/Library/old_recdef.ML --- a/src/HOL/Library/old_recdef.ML Mon Dec 02 13:34:02 2019 +0100 +++ b/src/HOL/Library/old_recdef.ML Mon Dec 02 15:04:38 2019 +0100 @@ -2842,7 +2842,7 @@ |> Global_Theory.add_thmss (((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts)) ||>> Global_Theory.add_thms [((Binding.name "induct", induct), [])] - ||> Spec_Rules.add_global name Spec_Rules.equational_recdef [lhs] (flat rules) + ||> Spec_Rules.add_global (Binding.name bname) Spec_Rules.equational_recdef [lhs] (flat rules) ||> null tcs ? Code.declare_default_eqns_global (map (rpair true) (flat rules)); val result = {lhs = lhs, simps = simps', rules = rules', induct = induct', tcs = tcs}; val thy3 = diff -r 39ccdbbed539 -r 5727bcc3c47c src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Dec 02 13:34:02 2019 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Dec 02 15:04:38 2019 +0100 @@ -1414,10 +1414,13 @@ |> massage_simple_notes fp_b_name; val (noted, lthy') = lthy - |> uncurry (Spec_Rules.add "" Spec_Rules.equational) (`(single o lhs_head_of o hd) map_thms) + |> uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational) + (`(single o lhs_head_of o hd) map_thms) |> fp = Least_FP ? - uncurry (Spec_Rules.add "" Spec_Rules.equational) (`(single o lhs_head_of o hd) rel_code_thms) - |> uncurry (Spec_Rules.add "" Spec_Rules.equational) (`(single o lhs_head_of o hd) set0_thms) + uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational) + (`(single o lhs_head_of o hd) rel_code_thms) + |> uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational) + (`(single o lhs_head_of o hd) set0_thms) |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (rel_code_thms @ map_thms @ set_thms)) |> Local_Theory.notes (anonymous_notes @ notes); @@ -2689,7 +2692,7 @@ |> massage_multi_notes fp_b_names fpTs; in lthy - |> Spec_Rules.add "" Spec_Rules.equational recs (flat rec_thmss) + |> Spec_Rules.add Binding.empty Spec_Rules.equational recs (flat rec_thmss) |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (flat rec_thmss)) |> Local_Theory.notes (common_notes @ notes) (* for "datatype_realizer.ML": *) @@ -2869,7 +2872,7 @@ |> massage_multi_notes fp_b_names fpTs; in lthy - |> fold (Spec_Rules.add "" Spec_Rules.equational corecs) + |> fold (Spec_Rules.add Binding.empty Spec_Rules.equational corecs) [flat corec_sel_thmss, flat corec_thmss] |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) corec_code_thms) |> Local_Theory.notes (common_notes @ notes) diff -r 39ccdbbed539 -r 5727bcc3c47c src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Mon Dec 02 13:34:02 2019 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Mon Dec 02 15:04:38 2019 +0100 @@ -2157,7 +2157,7 @@ |> Spec_Rules.add Spec_Rules.equational ([fun_lhs], flat sel_thmss) |> Spec_Rules.add Spec_Rules.equational ([fun_lhs], flat ctr_thmss) *) - |> Spec_Rules.add "" Spec_Rules.equational [fun_lhs] [code_thm] + |> Spec_Rules.add Binding.empty Spec_Rules.equational [fun_lhs] [code_thm] |> plugins code_plugin ? Code.declare_default_eqns [(code_thm, true)] |> Local_Theory.notes (anonymous_notes @ notes) |> snd diff -r 39ccdbbed539 -r 5727bcc3c47c src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Dec 02 13:34:02 2019 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Dec 02 15:04:38 2019 +0100 @@ -1533,9 +1533,10 @@ val fun_ts0 = map fst def_infos; in lthy - |> Spec_Rules.add "" (Spec_Rules.equational_primcorec primcorec_types) fun_ts0 (flat sel_thmss) - |> Spec_Rules.add "" Spec_Rules.equational fun_ts0 (flat ctr_thmss) - |> Spec_Rules.add "" Spec_Rules.equational fun_ts0 (flat code_thmss) + |> Spec_Rules.add Binding.empty (Spec_Rules.equational_primcorec primcorec_types) + fun_ts0 (flat sel_thmss) + |> Spec_Rules.add Binding.empty Spec_Rules.equational fun_ts0 (flat ctr_thmss) + |> Spec_Rules.add Binding.empty Spec_Rules.equational fun_ts0 (flat code_thmss) |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (flat code_thmss)) |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd diff -r 39ccdbbed539 -r 5727bcc3c47c src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Dec 02 13:34:02 2019 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Dec 02 15:04:38 2019 +0100 @@ -637,7 +637,7 @@ val transfer = exists (can (fn Transfer_Option => ())) opts; val (fixes, specs) = fst (prep_spec raw_fixes raw_specs lthy); - val spec_name = Local_Theory.full_name lthy (Binding.conglomerate (map (#1 o #1) fixes)); + val spec_name = Binding.conglomerate (map (#1 o #1) fixes); val mk_notes = flat oooo @{map 4} (fn js => fn prefix => fn qualify => fn thms => diff -r 39ccdbbed539 -r 5727bcc3c47c src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Dec 02 13:34:02 2019 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Dec 02 15:04:38 2019 +0100 @@ -373,8 +373,9 @@ val (noted, lthy3) = lthy2 - |> Spec_Rules.add "" Spec_Rules.equational size_consts size_simps - |> Spec_Rules.add "" Spec_Rules.equational overloaded_size_consts overloaded_size_simps + |> Spec_Rules.add Binding.empty Spec_Rules.equational size_consts size_simps + |> Spec_Rules.add Binding.empty Spec_Rules.equational + overloaded_size_consts overloaded_size_simps |> Code.declare_default_eqns (map (rpair true) (flat size_thmss)) (*Ideally, this would be issued only if the "code" plugin is enabled.*) |> Local_Theory.notes notes; diff -r 39ccdbbed539 -r 5727bcc3c47c src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Dec 02 13:34:02 2019 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Dec 02 15:04:38 2019 +0100 @@ -1111,10 +1111,10 @@ ((qualify true (Binding.name thmN), attrs), [(thms, [])])); val (noted, lthy') = lthy - |> Spec_Rules.add "" Spec_Rules.equational [casex] case_thms - |> fold (uncurry (Spec_Rules.add "" Spec_Rules.equational)) + |> Spec_Rules.add Binding.empty Spec_Rules.equational [casex] case_thms + |> fold (uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational)) (AList.group (eq_list (op aconv)) (map (`(single o lhs_head_of)) all_sel_thms)) - |> fold (uncurry (Spec_Rules.add "" Spec_Rules.equational)) + |> fold (uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational)) (filter_out (null o snd) (map single discs ~~ nontriv_disc_eq_thmss)) |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Case_Translation.register diff -r 39ccdbbed539 -r 5727bcc3c47c src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Mon Dec 02 13:34:02 2019 +0100 +++ b/src/HOL/Tools/Function/function.ML Mon Dec 02 15:04:38 2019 +0100 @@ -211,7 +211,7 @@ lthy2 |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => add_function_data (transform_function_data phi info')) - |> Spec_Rules.add "" Spec_Rules.equational_recdef fs tsimps) + |> Spec_Rules.add Binding.empty Spec_Rules.equational_recdef fs tsimps) end) end in diff -r 39ccdbbed539 -r 5727bcc3c47c src/HOL/Tools/Function/partial_function.ML --- a/src/HOL/Tools/Function/partial_function.ML Mon Dec 02 13:34:02 2019 +0100 +++ b/src/HOL/Tools/Function/partial_function.ML Mon Dec 02 15:04:38 2019 +0100 @@ -302,7 +302,7 @@ val ((_, [rec_rule']), lthy'') = lthy' |> Local_Theory.note (eq_abinding, [rec_rule]) in lthy'' - |> Spec_Rules.add "" Spec_Rules.equational_recdef [f] [rec_rule'] + |> Spec_Rules.add Binding.empty Spec_Rules.equational_recdef [f] [rec_rule'] |> note_qualified ("simps", [rec_rule']) |> note_qualified ("mono", [mono_thm]) |> (case raw_induct of NONE => I | SOME thm => note_qualified ("raw_induct", [thm])) diff -r 39ccdbbed539 -r 5727bcc3c47c src/HOL/Tools/Old_Datatype/old_primrec.ML --- a/src/HOL/Tools/Old_Datatype/old_primrec.ML Mon Dec 02 13:34:02 2019 +0100 +++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML Mon Dec 02 15:04:38 2019 +0100 @@ -278,7 +278,7 @@ fun gen_primrec prep_spec int raw_fixes raw_spec lthy = let val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy); - val spec_name = Local_Theory.full_name lthy (Binding.conglomerate (map (#1 o #1) fixes)); + val spec_name = Binding.conglomerate (map (#1 o #1) fixes); fun attr_bindings prefix = map (fn ((b, attrs), _) => (Binding.qualify false prefix b, attrs)) spec; fun simp_attr_binding prefix = diff -r 39ccdbbed539 -r 5727bcc3c47c src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Mon Dec 02 13:34:02 2019 +0100 +++ b/src/HOL/Tools/inductive.ML Mon Dec 02 15:04:38 2019 +0100 @@ -71,7 +71,7 @@ term list -> (Attrib.binding * term) list -> thm list -> term list -> (binding * mixfix) list -> local_theory -> result * local_theory - val declare_rules: binding -> bool -> bool -> string -> string list -> term list -> + val declare_rules: binding -> bool -> bool -> binding -> string list -> term list -> thm list -> binding list -> Token.src list list -> (thm * string list * int) list -> thm list -> thm -> local_theory -> thm list * thm list * thm list * thm * thm list * local_theory val add_ind_def: add_ind_def @@ -1099,7 +1099,7 @@ val _ = message (quiet_mode andalso not verbose) ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names); - val spec_name = Local_Theory.full_name lthy (Binding.conglomerate (map #1 cnames_syn)); + val spec_name = Binding.conglomerate (map #1 cnames_syn); val cnames = map (Local_Theory.full_name lthy o #1) cnames_syn; (* FIXME *) val ((intr_names, intr_atts), intr_ts) = apfst split_list (split_list (map (check_rule lthy cs params) intros)); diff -r 39ccdbbed539 -r 5727bcc3c47c src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Mon Dec 02 13:34:02 2019 +0100 +++ b/src/HOL/Tools/inductive_set.ML Mon Dec 02 15:04:38 2019 +0100 @@ -503,7 +503,7 @@ val rec_name = if Binding.is_empty alt_name then Binding.conglomerate (map #1 cnames_syn) else alt_name; val cnames = map (Local_Theory.full_name lthy3 o #1) cnames_syn; (* FIXME *) - val spec_name = Local_Theory.full_name lthy3 (Binding.conglomerate (map #1 cnames_syn)); + val spec_name = Binding.conglomerate (map #1 cnames_syn); val (intr_names, intr_atts) = split_list (map fst intros); val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct; val (intrs', elims', eqs', induct, inducts, lthy4) = diff -r 39ccdbbed539 -r 5727bcc3c47c src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Mon Dec 02 13:34:02 2019 +0100 +++ b/src/HOL/Tools/record.ML Mon Dec 02 15:04:38 2019 +0100 @@ -1814,7 +1814,7 @@ fun add_spec_rule rule = let val head = head_of (lhs_of_equation (Thm.prop_of rule)) - in Spec_Rules.add_global "" Spec_Rules.equational [head] [rule] end; + in Spec_Rules.add_global Binding.empty Spec_Rules.equational [head] [rule] end; (* definition *) diff -r 39ccdbbed539 -r 5727bcc3c47c src/Pure/Isar/spec_rules.ML --- a/src/Pure/Isar/spec_rules.ML Mon Dec 02 13:34:02 2019 +0100 +++ b/src/Pure/Isar/spec_rules.ML Mon Dec 02 15:04:38 2019 +0100 @@ -38,8 +38,8 @@ val dest_theory: theory -> spec_rule list val retrieve: Proof.context -> term -> spec_rule list val retrieve_global: theory -> term -> spec_rule list - val add: string -> rough_classification -> term list -> thm list -> local_theory -> local_theory - val add_global: string -> rough_classification -> term list -> thm list -> theory -> theory + val add: binding -> rough_classification -> term list -> thm list -> local_theory -> local_theory + val add_global: binding -> rough_classification -> term list -> thm list -> theory -> theory end; structure Spec_Rules: SPEC_RULES = @@ -158,7 +158,7 @@ (* add *) -fun add name rough_classification terms rules lthy = +fun add b rough_classification terms rules lthy = let val pos = Position.thread_data (); val thms0 = map Thm.trim_context (map (Drule.mk_term o Thm.cterm_of lthy) terms @ rules); @@ -166,6 +166,7 @@ lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context => let + val name = Name_Space.full_name (Name_Space.naming_of context) (Morphism.binding phi b); val (terms', rules') = map (Thm.transfer (Context.theory_of context)) thms0 |> Morphism.fact phi @@ -179,9 +180,12 @@ end) end; -fun add_global name rough_classification terms rules = - (Context.theory_map o Rules.map o Item_Net.update) - {pos = Position.thread_data (), name = name, rough_classification = rough_classification, - terms = terms, rules = map Thm.trim_context rules}; +fun add_global b rough_classification terms rules thy = + thy |> (Context.theory_map o Rules.map o Item_Net.update) + {pos = Position.thread_data (), + name = Sign.full_name thy b, + rough_classification = rough_classification, + terms = terms, + rules = map Thm.trim_context rules}; end; diff -r 39ccdbbed539 -r 5727bcc3c47c src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Mon Dec 02 13:34:02 2019 +0100 +++ b/src/Pure/Isar/specification.ML Mon Dec 02 15:04:38 2019 +0100 @@ -217,8 +217,7 @@ map ((apsnd o map) (prep_att vars_ctxt) o fst) raw_concls ~~ map close concls; val spec_name = - Sign.full_name thy - (Binding.conglomerate (if null decls then map (#1 o #1) specs else map (#1 o #1) decls)); + Binding.conglomerate (if null decls then map (#1 o #1) specs else map (#1 o #1) decls); (*consts*) @@ -270,7 +269,7 @@ |> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs)); val th = prove lthy2 raw_th; - val lthy3 = lthy2 |> Spec_Rules.add const_name Spec_Rules.equational [lhs] [th]; + val lthy3 = lthy2 |> Spec_Rules.add b Spec_Rules.equational [lhs] [th]; val ([(def_name, [th'])], lthy4) = lthy3 |> Local_Theory.notes [((name, atts), [([th], [])])]; diff -r 39ccdbbed539 -r 5727bcc3c47c src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Mon Dec 02 13:34:02 2019 +0100 +++ b/src/Pure/Proof/extraction.ML Mon Dec 02 15:04:38 2019 +0100 @@ -816,7 +816,6 @@ val fu = Type.legacy_freeze u; val head = head_of (strip_abs_body fu); val b = Binding.qualified_name (extr_name s vs); - val const_name = Sign.full_name thy b; in thy |> Sign.add_consts [(b, fastype_of ft, NoSyn)] @@ -824,7 +823,7 @@ [((Binding.qualified_name (Thm.def_name (extr_name s vs)), Logic.mk_equals (head, ft)), [])] |-> (fn [def_thm] => - Spec_Rules.add_global const_name Spec_Rules.equational + Spec_Rules.add_global b Spec_Rules.equational [Thm.term_of (Thm.lhs_of def_thm)] [def_thm] #> Code.declare_default_eqns_global [(def_thm, true)]) end;