--- a/src/HOL/Library/old_recdef.ML Fri Nov 29 21:29:18 2019 +0100
+++ b/src/HOL/Library/old_recdef.ML Fri Nov 29 21:53:02 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 Spec_Rules.equational_recdef ([lhs], flat rules)
+ ||> Spec_Rules.add_global name 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 =
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Nov 29 21:29:18 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Nov 29 21:53:02 2019 +0100
@@ -1414,10 +1414,10 @@
|> massage_simple_notes fp_b_name;
val (noted, lthy') = lthy
- |> Spec_Rules.add Spec_Rules.equational (`(single o lhs_head_of o hd) map_thms)
- |> fp = Least_FP
- ? Spec_Rules.add Spec_Rules.equational (`(single o lhs_head_of o hd) rel_code_thms)
- |> Spec_Rules.add Spec_Rules.equational (`(single o lhs_head_of o hd) set0_thms)
+ |> uncurry (Spec_Rules.add "" 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)
|> 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 +2689,7 @@
|> massage_multi_notes fp_b_names fpTs;
in
lthy
- |> Spec_Rules.add Spec_Rules.equational (recs, flat rec_thmss)
+ |> Spec_Rules.add "" 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 +2869,7 @@
|> massage_multi_notes fp_b_names fpTs;
in
lthy
- |> fold (curry (Spec_Rules.add Spec_Rules.equational) corecs)
+ |> fold (Spec_Rules.add "" 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)
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Fri Nov 29 21:29:18 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Fri Nov 29 21:53:02 2019 +0100
@@ -2157,7 +2157,7 @@
|> Spec_Rules.add Spec_Rules.equational ([fun_t0], flat sel_thmss)
|> Spec_Rules.add Spec_Rules.equational ([fun_t0], flat ctr_thmss)
*)
- |> Spec_Rules.add Spec_Rules.equational ([fun_t0], [code_thm])
+ |> Spec_Rules.add "" Spec_Rules.equational [fun_t0] [code_thm]
|> plugins code_plugin ? Code.declare_default_eqns [(code_thm, true)]
|> Local_Theory.notes (anonymous_notes @ notes)
|> snd
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Nov 29 21:29:18 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Nov 29 21:53:02 2019 +0100
@@ -1533,9 +1533,9 @@
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 "" (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)
|> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (flat code_thmss))
|> Local_Theory.notes (anonymous_notes @ common_notes @ notes)
|> snd
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Fri Nov 29 21:29:18 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Fri Nov 29 21:53:02 2019 +0100
@@ -637,6 +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 mk_notes =
flat oooo @{map 4} (fn js => fn prefix => fn qualify => fn thms =>
@@ -654,7 +655,7 @@
lthy
|> primrec_simple0 int plugins nonexhaustive transfer fixes (map snd specs)
|-> (fn {prefix = (names, qualifys), types, result = (ts, defs, (jss, simpss))} =>
- Spec_Rules.add (Spec_Rules.equational_primrec types) (ts, flat simpss)
+ Spec_Rules.add spec_name (Spec_Rules.equational_primrec types) ts (flat simpss)
#> Local_Theory.notes (mk_notes jss names qualifys simpss)
#-> (fn notes =>
plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (maps snd notes))
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Nov 29 21:29:18 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Nov 29 21:53:02 2019 +0100
@@ -373,8 +373,8 @@
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 "" Spec_Rules.equational size_consts size_simps
+ |> Spec_Rules.add "" 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;
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Nov 29 21:29:18 2019 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Nov 29 21:53:02 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 (Spec_Rules.add Spec_Rules.equational)
+ |> Spec_Rules.add "" Spec_Rules.equational [casex] case_thms
+ |> fold (uncurry (Spec_Rules.add "" Spec_Rules.equational))
(AList.group (eq_list (op aconv)) (map (`(single o lhs_head_of)) all_sel_thms))
- |> fold (Spec_Rules.add Spec_Rules.equational)
+ |> fold (uncurry (Spec_Rules.add "" 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
--- a/src/HOL/Tools/Function/function.ML Fri Nov 29 21:29:18 2019 +0100
+++ b/src/HOL/Tools/Function/function.ML Fri Nov 29 21:53:02 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 "" Spec_Rules.equational_recdef fs tsimps)
end)
end
in
--- a/src/HOL/Tools/Function/function_common.ML Fri Nov 29 21:29:18 2019 +0100
+++ b/src/HOL/Tools/Function/function_common.ML Fri Nov 29 21:53:02 2019 +0100
@@ -314,6 +314,7 @@
SOME (transform_function_data (inst_morph u) data) handle Pattern.MATCH => NONE
in
get_first match (retrieve_function_data ctxt t)
+ |> Option.map (transform_function_data (Morphism.transfer_morphism' ctxt))
end
fun import_last_function ctxt =
--- a/src/HOL/Tools/Function/partial_function.ML Fri Nov 29 21:29:18 2019 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML Fri Nov 29 21:53:02 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 "" 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]))
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Nov 29 21:29:18 2019 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Nov 29 21:53:02 2019 +0100
@@ -1353,8 +1353,8 @@
fun all_nondefs_of ctxt subst =
ctxt |> Spec_Rules.get
- |> filter (Spec_Rules.is_unknown o fst)
- |> maps (snd o snd)
+ |> filter (Spec_Rules.is_unknown o #rough_classification)
+ |> maps #rules
|> filter_out (is_built_in_theory o Thm.theory_id)
|> map (subst_atomic subst o Thm.prop_of)
@@ -1945,10 +1945,9 @@
fun inductive_intro_table ctxt subst def_tables =
let val thy = Proof_Context.theory_of ctxt in
def_table_for
- (maps (map (unfold_mutually_inductive_preds thy def_tables o Thm.prop_of)
- o snd o snd)
- (filter ((Spec_Rules.is_inductive orf Spec_Rules.is_co_inductive) o #1)
- (Spec_Rules.get ctxt))) subst
+ (maps (map (unfold_mutually_inductive_preds thy def_tables o Thm.prop_of) o #rules)
+ (filter (Spec_Rules.is_relational o #rough_classification)
+ (Spec_Rules.get ctxt))) subst
end
fun ground_theorem_table thy =
--- a/src/HOL/Tools/Nunchaku/nunchaku_collect.ML Fri Nov 29 21:29:18 2019 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_collect.ML Fri Nov 29 21:53:02 2019 +0100
@@ -479,7 +479,7 @@
try (Sign.typ_match thy (fastype_of t0, T)) Vartab.empty;
fun process_spec _ (res as SOME _) = res
- | process_spec (classif, (ts0, ths as _ :: _)) NONE =
+ | process_spec {rough_classification = classif, terms = ts0, rules = ths as _ :: _, ...} NONE =
(case get_first subst_of ts0 of
SOME subst =>
(let
@@ -496,18 +496,21 @@
fun spec_rules () =
Spec_Rules.retrieve ctxt (Const x)
- |> sort (Spec_Rules.rough_classification_ord o apply2 fst);
+ |> sort (Spec_Rules.rough_classification_ord o apply2 #rough_classification);
val specs =
if s = \<^const_name>\<open>The\<close> then
- [(Spec_Rules.Unknown, ([Logic.varify_global \<^term>\<open>The\<close>], [@{thm theI_unique}]))]
+ [{name = "", rough_classification = Spec_Rules.Unknown,
+ terms = [Logic.varify_global \<^term>\<open>The\<close>],
+ rules = [@{thm theI_unique}]}]
else if s = \<^const_name>\<open>finite\<close> then
let val card = card_of_type ctxt T in
if card = Inf orelse card = Fin_or_Inf then
spec_rules ()
else
- [(Spec_Rules.equational, ([Logic.varify_global \<^term>\<open>finite\<close>],
- [Skip_Proof.make_thm thy (Logic.varify_global \<^prop>\<open>finite A = True\<close>)]))]
+ [{name = "", rough_classification = Spec_Rules.equational,
+ terms = [Logic.varify_global \<^term>\<open>finite\<close>],
+ rules = [Skip_Proof.make_thm thy (Logic.varify_global \<^prop>\<open>finite A = True\<close>)]}]
end
else
spec_rules ();
@@ -537,10 +540,9 @@
val orphan_axioms_of =
Spec_Rules.get
- #> filter (Spec_Rules.is_unknown o fst)
- #> map snd
- #> filter (null o fst)
- #> maps snd
+ #> filter (Spec_Rules.is_unknown o #rough_classification)
+ #> filter (null o #terms)
+ #> maps #rules
#> filter_out (is_builtin_theory o Thm.theory_id)
#> map Thm.prop_of;
@@ -961,7 +963,7 @@
pat_complete = is_apparently_pat_complete ctxt props})
consts propss)])
| NONE => def_or_spec ())
- else if (Spec_Rules.is_inductive orf Spec_Rules.is_co_inductive) classif
+ else if Spec_Rules.is_relational classif
then
if is_inductive_set_intro (hd props) then
def_or_spec ()
--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML Fri Nov 29 21:29:18 2019 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML Fri Nov 29 21:53:02 2019 +0100
@@ -278,6 +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));
fun attr_bindings prefix = map (fn ((b, attrs), _) =>
(Binding.qualify false prefix b, attrs)) spec;
fun simp_attr_binding prefix =
@@ -286,7 +287,7 @@
lthy
|> primrec_simple int fixes (map snd spec)
|-> (fn {prefix, types, result = (ts, simps)} =>
- Spec_Rules.add (Spec_Rules.equational_primrec types) (ts, simps)
+ Spec_Rules.add spec_name (Spec_Rules.equational_primrec types) ts simps
#> fold_map Local_Theory.note (attr_bindings prefix ~~ map single simps)
#-> (fn simps' => Local_Theory.note (simp_attr_binding prefix, maps snd simps')
#-> (fn (_, simps'') =>
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Nov 29 21:29:18 2019 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Nov 29 21:53:02 2019 +0100
@@ -212,7 +212,7 @@
[] =>
(case Spec_Rules.retrieve ctxt t of
[] => error ("No specification for " ^ Syntax.string_of_term_global thy t)
- | ((_, (_, ths)) :: _) => filter_defs ths)
+ | ({rules = ths, ...} :: _) => filter_defs ths)
| ths => ths)
val _ =
if show_intermediate_results options then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Nov 29 21:29:18 2019 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Nov 29 21:53:02 2019 +0100
@@ -317,12 +317,12 @@
*)
val specs = Spec_Rules.get ctxt
val (rec_defs, nonrec_defs) = specs
- |> filter (Spec_Rules.is_equational o fst)
- |> maps (snd o snd)
+ |> filter (Spec_Rules.is_equational o #rough_classification)
+ |> maps #rules
|> List.partition (is_rec_def o Thm.prop_of)
val spec_intros = specs
- |> filter ((Spec_Rules.is_inductive orf Spec_Rules.is_co_inductive) o fst)
- |> maps (snd o snd)
+ |> filter (Spec_Rules.is_relational o #rough_classification)
+ |> maps #rules
in
Termtab.empty
|> fold (add Simp o snd) simps
--- a/src/HOL/Tools/inductive.ML Fri Nov 29 21:29:18 2019 +0100
+++ b/src/HOL/Tools/inductive.ML Fri Nov 29 21:53:02 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 list -> term list ->
+ val declare_rules: binding -> bool -> bool -> string -> 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
@@ -1017,7 +1017,7 @@
list_comb (rec_const, params), preds, argTs, bs, xs)
end;
-fun declare_rules rec_binding coind no_ind cnames
+fun declare_rules rec_binding coind no_ind spec_name cnames
preds intrs intr_bindings intr_atts elims eqs raw_induct lthy =
let
val rec_name = Binding.name_of rec_binding;
@@ -1041,8 +1041,8 @@
val (intrs', lthy1) =
lthy |>
- Spec_Rules.add
- (if coind then Spec_Rules.Co_Inductive else Spec_Rules.Inductive) (preds, intrs) |>
+ Spec_Rules.add spec_name
+ (if coind then Spec_Rules.Co_Inductive else Spec_Rules.Inductive) preds intrs |>
Local_Theory.notes
(map (rec_qualified false) intr_bindings ~~ intr_atts ~~
map (fn th => [([th], @{attributes [Pure.intro?]})]) intrs) |>>
@@ -1099,6 +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 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));
@@ -1131,7 +1132,7 @@
val (intrs'', elims'', eqs', induct, inducts, lthy3) =
declare_rules rec_binding coind no_ind
- cnames preds intrs' intr_names intr_atts elims' eqs raw_induct lthy1;
+ spec_name cnames preds intrs' intr_names intr_atts elims' eqs raw_induct lthy1;
val result =
{preds = preds,
--- a/src/HOL/Tools/inductive_set.ML Fri Nov 29 21:29:18 2019 +0100
+++ b/src/HOL/Tools/inductive_set.ML Fri Nov 29 21:53:02 2019 +0100
@@ -503,10 +503,11 @@
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 (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) =
- Inductive.declare_rules rec_name coind no_ind cnames (map fst defs)
+ Inductive.declare_rules rec_name coind no_ind spec_name cnames (map fst defs)
(map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
(map (fn th => (to_set [] (Context.Proof lthy3) th,
map (fst o fst) (fst (Rule_Cases.get th)),
--- a/src/HOL/Tools/record.ML Fri Nov 29 21:29:18 2019 +0100
+++ b/src/HOL/Tools/record.ML Fri Nov 29 21:53:02 2019 +0100
@@ -1813,9 +1813,8 @@
| lhs_of_equation (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ _)) = t;
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;
+ let val head = head_of (lhs_of_equation (Thm.prop_of rule))
+ in Spec_Rules.add_global "" Spec_Rules.equational [head] [rule] end;
(* definition *)
--- a/src/Pure/Isar/generic_target.ML Fri Nov 29 21:29:18 2019 +0100
+++ b/src/Pure/Isar/generic_target.ML Fri Nov 29 21:53:02 2019 +0100
@@ -180,9 +180,9 @@
fun background_declaration decl lthy =
let
- val theory_decl =
+ fun theory_decl context =
Local_Theory.standard_form lthy
- (Proof_Context.init_global (Proof_Context.theory_of lthy)) decl;
+ (Proof_Context.init_global (Context.theory_of context)) decl context;
in Local_Theory.background_theory (Context.theory_map theory_decl) lthy end;
fun background_abbrev (b, global_rhs) params =
--- a/src/Pure/Isar/spec_rules.ML Fri Nov 29 21:29:18 2019 +0100
+++ b/src/Pure/Isar/spec_rules.ML Fri Nov 29 21:53:02 2019 +0100
@@ -21,14 +21,16 @@
val is_equational: rough_classification -> bool
val is_inductive: rough_classification -> bool
val is_co_inductive: rough_classification -> bool
+ val is_relational: rough_classification -> bool
val is_unknown: rough_classification -> bool
- type spec = rough_classification * (term list * thm list)
+ type spec =
+ {name: string, rough_classification: rough_classification, terms: term list, rules: thm list}
val get: Proof.context -> spec list
val get_global: theory -> spec list
val retrieve: Proof.context -> term -> spec list
val retrieve_global: theory -> term -> spec list
- val add: rough_classification -> term list * thm list -> local_theory -> local_theory
- val add_global: rough_classification -> term list * thm list -> theory -> theory
+ 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
end;
structure Spec_Rules: SPEC_RULES =
@@ -64,23 +66,28 @@
val is_equational = fn Equational _ => true | _ => false;
val is_inductive = fn Inductive => true | _ => false;
val is_co_inductive = fn Co_Inductive => true | _ => false;
+val is_relational = is_inductive orf is_co_inductive;
val is_unknown = fn Unknown => true | _ => false;
(* rules *)
-type spec = rough_classification * (term list * thm list);
+type spec =
+ {name: string, rough_classification: rough_classification, terms: term list, rules: thm list};
+
+fun eq_spec (specs: spec * spec) =
+ (op =) (apply2 #name specs) andalso
+ is_equal (rough_classification_ord (apply2 #rough_classification specs)) andalso
+ eq_list (op aconv) (apply2 #terms specs) andalso
+ eq_list Thm.eq_thm_prop (apply2 #rules specs);
+
+fun map_spec_rules f ({name, rough_classification, terms, rules}: spec) : spec =
+ {name = name, rough_classification = rough_classification, terms = terms, rules = map f rules};
structure Rules = Generic_Data
(
type T = spec Item_Net.T;
- val empty : T =
- Item_Net.init
- (fn ((c1, (ts1, ths1)), (c2, (ts2, ths2))) =>
- is_equal (rough_classification_ord (c1, c2)) andalso
- eq_list (op aconv) (ts1, ts2) andalso
- eq_list Thm.eq_thm_prop (ths1, ths2))
- (#1 o #2);
+ val empty : T = Item_Net.init eq_spec #terms;
val extend = I;
val merge = Item_Net.merge;
);
@@ -92,7 +99,10 @@
let
val thy = Context.theory_of context;
val transfer = Global_Theory.transfer_theories thy;
- in Item_Net.content (Rules.get context) |> (map o apsnd o apsnd o map) transfer end;
+ in
+ Item_Net.content (Rules.get context)
+ |> (map o map_spec_rules) transfer
+ end;
val get = get_generic o Context.Proof;
val get_global = get_generic o Context.Theory;
@@ -102,7 +112,7 @@
fun retrieve_generic context =
Item_Net.retrieve (Rules.get context)
- #> (map o apsnd o apsnd o map) (Thm.transfer'' context);
+ #> (map o map_spec_rules) (Thm.transfer'' context);
val retrieve = retrieve_generic o Context.Proof;
val retrieve_global = retrieve_generic o Context.Theory;
@@ -110,22 +120,27 @@
(* add *)
-fun add class (ts, ths) lthy =
- let
- val cts = map (Thm.cterm_of lthy) ts;
- in
+fun add name rough_classification terms rules lthy =
+ let val thms0 = map Thm.trim_context (map (Drule.mk_term o Thm.cterm_of lthy) terms @ rules) in
lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi =>
+ (fn phi => fn context =>
let
- val (ts', ths') =
- Morphism.fact phi (map Drule.mk_term cts @ ths)
- |> chop (length cts)
+ val (terms', rules') =
+ map (Thm.transfer (Context.theory_of context)) thms0
+ |> Morphism.fact phi
+ |> chop (length terms)
|>> map (Thm.term_of o Drule.dest_term)
||> map Thm.trim_context;
- in Rules.map (Item_Net.update (class, (ts', ths'))) end)
+ in
+ context |> (Rules.map o Item_Net.update)
+ {name = name, rough_classification = rough_classification,
+ terms = terms', rules = rules'}
+ end)
end;
-fun add_global class spec =
- Context.theory_map (Rules.map (Item_Net.update (class, (apsnd o map) Thm.trim_context spec)));
+fun add_global name rough_classification terms rules =
+ (Context.theory_map o Rules.map o Item_Net.update)
+ {name = name, rough_classification = rough_classification,
+ terms = terms, rules = map Thm.trim_context rules};
end;
--- a/src/Pure/Isar/specification.ML Fri Nov 29 21:29:18 2019 +0100
+++ b/src/Pure/Isar/specification.ML Fri Nov 29 21:53:02 2019 +0100
@@ -229,7 +229,7 @@
(*facts*)
val (facts, facts_lthy) = axioms_thy
|> Named_Target.theory_init
- |> Spec_Rules.add Spec_Rules.Unknown (consts, maps (maps #1 o #2) axioms)
+ |> Spec_Rules.add "" Spec_Rules.Unknown consts (maps (maps #1 o #2) axioms)
|> Local_Theory.notes axioms;
in ((consts, map (the_single o #2) facts), Local_Theory.exit_global facts_lthy) end;
@@ -258,12 +258,14 @@
else
error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
Position.here (Binding.pos_of b)));
+ val const_name = Local_Theory.full_name lthy b;
+
val name = Thm.def_binding_optional b a;
val ((lhs, (_, raw_th)), lthy2) = lthy
|> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs));
val th = prove lthy2 raw_th;
- val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.equational ([lhs], [th]);
+ val lthy3 = lthy2 |> Spec_Rules.add const_name Spec_Rules.equational [lhs] [th];
val ([(def_name, [th'])], lthy4) = lthy3
|> Local_Theory.notes [((name, atts), [([th], [])])];
--- a/src/Pure/Proof/extraction.ML Fri Nov 29 21:29:18 2019 +0100
+++ b/src/Pure/Proof/extraction.ML Fri Nov 29 21:53:02 2019 +0100
@@ -815,14 +815,16 @@
val ft = Type.legacy_freeze t;
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 [(Binding.qualified_name (extr_name s vs), fastype_of ft, NoSyn)]
+ |> Sign.add_consts [(b, fastype_of ft, NoSyn)]
|> Global_Theory.add_defs false
[((Binding.qualified_name (Thm.def_name (extr_name s vs)),
Logic.mk_equals (head, ft)), [])]
|-> (fn [def_thm] =>
- Spec_Rules.add_global Spec_Rules.equational ([head], [def_thm])
+ Spec_Rules.add_global const_name Spec_Rules.equational [head] [def_thm]
#> Code.declare_default_eqns_global [(def_thm, true)])
end;
--- a/src/Pure/Thy/export_theory.ML Fri Nov 29 21:29:18 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML Fri Nov 29 21:53:02 2019 +0100
@@ -60,9 +60,10 @@
fun primrec_types ctxt const =
Spec_Rules.retrieve ctxt (Const const)
|> get_first
- (fn (Spec_Rules.Equational (Spec_Rules.Primrec types), _) => SOME (types, false)
- | (Spec_Rules.Equational (Spec_Rules.Primcorec types), _) => SOME (types, true)
- | _ => NONE)
+ (#rough_classification #>
+ (fn Spec_Rules.Equational (Spec_Rules.Primrec types) => SOME (types, false)
+ | Spec_Rules.Equational (Spec_Rules.Primcorec types) => SOME (types, true)
+ | _ => NONE))
|> the_default ([], false);
--- a/src/Pure/assumption.ML Fri Nov 29 21:29:18 2019 +0100
+++ b/src/Pure/assumption.ML Fri Nov 29 21:53:02 2019 +0100
@@ -128,14 +128,10 @@
(* export *)
-fun normalize ctxt0 th0 =
- let val (ctxt, th) = Thm.join_transfer_context (ctxt0, th0)
- in Raw_Simplifier.norm_hhf_protect ctxt th end;
-
fun export is_goal inner outer =
- normalize inner #>
+ Raw_Simplifier.norm_hhf_protect inner #>
fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #>
- normalize outer;
+ Raw_Simplifier.norm_hhf_protect outer;
fun export_term inner outer =
fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer);
--- a/src/Pure/raw_simplifier.ML Fri Nov 29 21:29:18 2019 +0100
+++ b/src/Pure/raw_simplifier.ML Fri Nov 29 21:53:02 2019 +0100
@@ -1426,15 +1426,14 @@
local
-fun gen_norm_hhf ss ctxt =
- Thm.transfer' ctxt #>
- (fn th =>
- if Drule.is_norm_hhf (Thm.prop_of th) then th
- else
- Conv.fconv_rule
- (rewrite_cterm (true, false, false) (K (K NONE)) (put_simpset ss ctxt)) th) #>
- Thm.adjust_maxidx_thm ~1 #>
- Variable.gen_all ctxt;
+fun gen_norm_hhf ss ctxt0 th0 =
+ let
+ val (ctxt, th) = Thm.join_transfer_context (ctxt0, th0);
+ val th' =
+ if Drule.is_norm_hhf (Thm.prop_of th) then th
+ else
+ Conv.fconv_rule (rewrite_cterm (true, false, false) (K (K NONE)) (put_simpset ss ctxt)) th;
+ in th' |> Thm.adjust_maxidx_thm ~1 |> Variable.gen_all ctxt end;
val hhf_ss =
Context.the_local_context ()
--- a/src/Pure/thm.ML Fri Nov 29 21:29:18 2019 +0100
+++ b/src/Pure/thm.ML Fri Nov 29 21:53:02 2019 +0100
@@ -610,9 +610,9 @@
else transfer thy th;
fun join_transfer_context (ctxt, th) =
- if Context.subthy_id (Context.theory_id (Proof_Context.theory_of ctxt), theory_id th) then
- (Context.raw_transfer (theory_of_thm th) ctxt, th)
- else (ctxt, transfer' ctxt th);
+ if Context.subthy_id (theory_id th, Context.theory_id (Proof_Context.theory_of ctxt))
+ then (ctxt, transfer' ctxt th)
+ else (Context.raw_transfer (theory_of_thm th) ctxt, th);
(* matching *)