--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Aug 01 14:46:50 2019 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Aug 02 11:23:09 2019 +0200
@@ -844,7 +844,7 @@
fun split_conjs i nprems th =
if i > nprems then th
else
- (case try Drule.RSN (@{thm conjI}, (i, th)) of
+ (case try (op RSN) (@{thm conjI}, (i, th)) of
SOME th' => split_conjs i (nprems + 1) th'
| NONE => split_conjs (i + 1) nprems th)
in
--- a/src/Pure/axclass.ML Thu Aug 01 14:46:50 2019 +0200
+++ b/src/Pure/axclass.ML Fri Aug 02 11:23:09 2019 +0200
@@ -11,7 +11,6 @@
val get_info: theory -> class -> info
val class_of_param: theory -> string -> class option
val instance_name: string * class -> string
- val thynames_of_arity: theory -> string * class -> string list
val param_of_inst: theory -> string * string -> string
val inst_of_param: theory -> string -> (string * string) option
val unoverload: Proof.context -> thm -> thm
@@ -69,30 +68,23 @@
datatype data = Data of
{axclasses: info Symtab.table,
params: param list,
- proven_classrels: thm Symreltab.table,
- proven_arities: ((class * sort list) * (thm * string)) list Symtab.table,
(*arity theorems with theory name*)
inst_params:
(string * thm) Symtab.table Symtab.table *
(*constant name ~> type constructor ~> (constant name, equation)*)
(string * string) Symtab.table (*constant name ~> (constant name, type constructor)*)};
-fun make_data
- (axclasses, params, proven_classrels, proven_arities, inst_params) =
- Data {axclasses = axclasses, params = params, proven_classrels = proven_classrels,
- proven_arities = proven_arities, inst_params = inst_params};
+fun make_data (axclasses, params, inst_params) =
+ Data {axclasses = axclasses, params = params, inst_params = inst_params};
structure Data = Theory_Data'
(
type T = data;
- val empty =
- make_data (Symtab.empty, [], Symreltab.empty, Symtab.empty, (Symtab.empty, Symtab.empty));
+ val empty = make_data (Symtab.empty, [], (Symtab.empty, Symtab.empty));
val extend = I;
fun merge old_thys
- (Data {axclasses = axclasses1, params = params1, proven_classrels = proven_classrels1,
- proven_arities = proven_arities1, inst_params = inst_params1},
- Data {axclasses = axclasses2, params = params2, proven_classrels = proven_classrels2,
- proven_arities = proven_arities2, inst_params = inst_params2}) =
+ (Data {axclasses = axclasses1, params = params1, inst_params = inst_params1},
+ Data {axclasses = axclasses2, params = params2, inst_params = inst_params2}) =
let
val old_ctxt = Syntax.init_pretty_global (fst old_thys);
@@ -103,48 +95,32 @@
fold_rev (fn p => if member (op =) params1 p then I else add_param old_ctxt p)
params2 params1;
- (*see Theory.at_begin hook for transitive closure of classrels and arity completion*)
- val proven_classrels' = Symreltab.merge (K true) (proven_classrels1, proven_classrels2);
- val proven_arities' = Symtab.merge_list (eq_fst op =) (proven_arities1, proven_arities2);
-
val inst_params' =
(Symtab.join (K (Symtab.merge (K true))) (#1 inst_params1, #1 inst_params2),
Symtab.merge (K true) (#2 inst_params1, #2 inst_params2));
- in
- make_data (axclasses', params', proven_classrels', proven_arities', inst_params')
- end;
+ in make_data (axclasses', params', inst_params') end;
);
fun map_data f =
- Data.map (fn Data {axclasses, params, proven_classrels, proven_arities, inst_params} =>
- make_data (f (axclasses, params, proven_classrels, proven_arities, inst_params)));
+ Data.map (fn Data {axclasses, params, inst_params} =>
+ make_data (f (axclasses, params, inst_params)));
fun map_axclasses f =
- map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params) =>
- (f axclasses, params, proven_classrels, proven_arities, inst_params));
+ map_data (fn (axclasses, params, inst_params) =>
+ (f axclasses, params, inst_params));
fun map_params f =
- map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params) =>
- (axclasses, f params, proven_classrels, proven_arities, inst_params));
-
-fun map_proven_classrels f =
- map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params) =>
- (axclasses, params, f proven_classrels, proven_arities, inst_params));
-
-fun map_proven_arities f =
- map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params) =>
- (axclasses, params, proven_classrels, f proven_arities, inst_params));
+ map_data (fn (axclasses, params, inst_params) =>
+ (axclasses, f params, inst_params));
fun map_inst_params f =
- map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params) =>
- (axclasses, params, proven_classrels, proven_arities, f inst_params));
+ map_data (fn (axclasses, params, inst_params) =>
+ (axclasses, params, f inst_params));
val rep_data = Data.get #> (fn Data args => args);
val axclasses_of = #axclasses o rep_data;
val params_of = #params o rep_data;
-val proven_classrels_of = #proven_classrels o rep_data;
-val proven_arities_of = #proven_arities o rep_data;
val inst_params_of = #inst_params o rep_data;
@@ -166,120 +142,6 @@
fun class_of_param thy = AList.lookup (op =) (params_of thy);
-(* maintain instances *)
-
-val classrel_prefix = "classrel_";
-val arity_prefix = "arity_";
-
-fun instance_name (a, c) = Long_Name.base_name c ^ "_" ^ Long_Name.base_name a;
-
-fun standard_tvars thm =
- let
- val thy = Thm.theory_of_thm thm;
- val tvars = rev (Term.add_tvars (Thm.prop_of thm) []);
- val names = Name.invent Name.context Name.aT (length tvars);
- val tinst =
- map2 (fn (ai, S) => fn b => ((ai, S), Thm.global_ctyp_of thy (TVar ((b, 0), S)))) tvars names;
- in Thm.instantiate (tinst, []) thm end
-
-
-val is_classrel = Symreltab.defined o proven_classrels_of;
-
-fun the_classrel thy (c1, c2) =
- (case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of
- SOME thm => Thm.transfer thy thm
- | NONE => error ("Unproven class relation " ^
- Syntax.string_of_classrel (Proof_Context.init_global thy) [c1, c2]));
-
-fun complete_classrels thy =
- let
- fun complete (c, (_, (all_preds, all_succs))) (finished1, thy1) =
- let
- fun compl c1 c2 (finished2, thy2) =
- if is_classrel thy2 (c1, c2) then (finished2, thy2)
- else
- (false,
- thy2
- |> (map_proven_classrels o Symreltab.update) ((c1, c2),
- (the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2))
- |> standard_tvars
- |> Thm.close_derivation
- |> Thm.trim_context));
-
- val proven = is_classrel thy1;
- val preds = Graph.Keys.fold (fn c1 => proven (c1, c) ? cons c1) all_preds [];
- val succs = Graph.Keys.fold (fn c2 => proven (c, c2) ? cons c2) all_succs [];
- in
- fold_product compl preds succs (finished1, thy1)
- end;
- in
- (case Graph.fold complete (Sorts.classes_of (Sign.classes_of thy)) (true, thy) of
- (true, _) => NONE
- | (_, thy') => SOME thy')
- end;
-
-
-fun the_arity thy (a, Ss, c) =
- (case AList.lookup (op =) (Symtab.lookup_list (proven_arities_of thy) a) (c, Ss) of
- SOME (thm, _) => Thm.transfer thy thm
- | NONE => error ("Unproven type arity " ^
- Syntax.string_of_arity (Proof_Context.init_global thy) (a, Ss, [c])));
-
-fun thynames_of_arity thy (a, c) =
- Symtab.lookup_list (proven_arities_of thy) a
- |> map_filter (fn ((c', _), (_, name)) => if c = c' then SOME name else NONE)
- |> rev;
-
-fun insert_arity_completions thy t ((c, Ss), ((th, thy_name))) (finished, arities) =
- let
- val algebra = Sign.classes_of thy;
- val ars = Symtab.lookup_list arities t;
- val super_class_completions =
- Sign.super_classes thy c
- |> filter_out (fn c1 => exists (fn ((c2, Ss2), _) =>
- c1 = c2 andalso Sorts.sorts_le algebra (Ss2, Ss)) ars);
-
- val completions = super_class_completions |> map (fn c1 =>
- let
- val th1 =
- (th RS the_classrel thy (c, c1))
- |> standard_tvars
- |> Thm.close_derivation
- |> Thm.trim_context;
- in ((th1, thy_name), c1) end);
-
- val finished' = finished andalso null completions;
- val arities' = fold (fn (th, c1) => Symtab.cons_list (t, ((c1, Ss), th))) completions arities;
- in (finished', arities') end;
-
-fun put_arity_completion ((t, Ss, c), th) thy =
- let val ar = ((c, Ss), (th, Context.theory_name thy)) in
- thy
- |> map_proven_arities
- (Symtab.insert_list (eq_fst op =) (t, ar) #>
- curry (insert_arity_completions thy t ar) true #> #2)
- end;
-
-fun complete_arities thy =
- let
- val arities = proven_arities_of thy;
- val (finished, arities') =
- Symtab.fold (fn (t, ars) => fold (insert_arity_completions thy t) ars)
- arities (true, arities);
- in
- if finished then NONE
- else SOME (map_proven_arities (K arities') thy)
- end;
-
-val _ =
- Theory.setup
- (Theory.at_begin complete_classrels #>
- Theory.at_begin complete_arities #>
- Proofterm.install_axclass_proofs
- {classrel_proof = Thm.proof_of oo the_classrel,
- arity_proof = Thm.proof_of oo the_arity});
-
-
(* maintain instance parameters *)
fun get_inst_param thy (c, tyco) =
@@ -323,6 +185,12 @@
(** instances **)
+val classrel_prefix = "classrel_";
+val arity_prefix = "arity_";
+
+fun instance_name (a, c) = Long_Name.base_name c ^ "_" ^ Long_Name.base_name a;
+
+
(* class relations *)
fun cert_classrel thy raw_rel =
@@ -400,17 +268,7 @@
val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
val binding =
Binding.concealed (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))));
- val (th', thy') = Global_Theory.store_thm (binding, th) thy;
- val th'' = th'
- |> Thm.unconstrainT
- |> Thm.trim_context;
- in
- thy'
- |> Sign.primitive_classrel (c1, c2)
- |> map_proven_classrels (Symreltab.update ((c1, c2), th''))
- |> perhaps complete_classrels
- |> perhaps complete_arities
- end;
+ in thy |> Global_Theory.store_thm (binding, th) |-> Thm.add_classrel end;
fun add_arity raw_th thy =
let
@@ -421,24 +279,18 @@
val binding =
Binding.concealed (Binding.name (prefix arity_prefix (Logic.name_arity arity)));
- val (th', thy') = Global_Theory.store_thm (binding, th) thy;
val args = Name.invent_names Name.context Name.aT Ss;
- val T = Type (t, map TFree args);
-
- val missing_params = Sign.complete_sort thy' [c]
- |> maps (these o Option.map #params o try (get_info thy'))
- |> filter_out (fn (const, _) => can (get_inst_param thy') (const, t))
- |> (map o apsnd o map_atyps) (K T);
-
- val th'' = th'
- |> Thm.unconstrainT
- |> Thm.trim_context;
+ val missing_params =
+ Sign.complete_sort thy [c]
+ |> maps (these o Option.map #params o try (get_info thy))
+ |> filter_out (fn (const, _) => can (get_inst_param thy) (const, t))
+ |> (map o apsnd o map_atyps) (K (Type (t, map TFree args)));
in
- thy'
+ thy
+ |> Global_Theory.store_thm (binding, th)
+ |-> Thm.add_arity
|> fold (#2 oo declare_overloaded) missing_params
- |> Sign.primitive_arity (t, Ss, [c])
- |> put_arity_completion ((t, Ss, c), th'')
end;
@@ -569,12 +421,10 @@
val axclass =
make_axclass
(Thm.trim_context def, Thm.trim_context intro, map Thm.trim_context axioms, params);
+
val result_thy =
facts_thy
- |> map_proven_classrels
- (fold2 (fn c => fn th => Symreltab.update ((class, c), Thm.trim_context th))
- super classrel)
- |> perhaps complete_classrels
+ |> fold (fn th => Thm.add_classrel (class_triv RS th)) classrel
|> Sign.qualified_path false bconst
|> Global_Theory.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms))
|> #2
--- a/src/Pure/drule.ML Thu Aug 01 14:46:50 2019 +0200
+++ b/src/Pure/drule.ML Fri Aug 02 11:23:09 2019 +0200
@@ -4,7 +4,7 @@
Derived rules and other operations on theorems.
*)
-infix 0 RS RSN RL RLN MRS OF COMP INCR_COMP COMP_INCR;
+infix 0 RL RLN MRS OF COMP INCR_COMP COMP_INCR;
signature BASIC_DRULE =
sig
@@ -30,8 +30,6 @@
val implies_intr_hyps: thm -> thm
val rotate_prems: int -> thm -> thm
val rearrange_prems: int list -> thm -> thm
- val RSN: thm * (int * thm) -> thm
- val RS: thm * thm -> thm
val RLN: thm list * (int * thm list) -> thm list
val RL: thm list * thm list -> thm list
val MRS: thm list * thm -> thm
@@ -294,16 +292,6 @@
Seq.maps (multi_resolve opt_ctxt facts) (Seq.of_list rules);
end;
-(*Resolution: exactly one resolvent must be produced*)
-fun tha RSN (i, thb) =
- (case Seq.chop 2 (Thm.biresolution NONE false [(false, tha)] i thb) of
- ([th], _) => th
- | ([], _) => raise THM ("RSN: no unifiers", i, [tha, thb])
- | _ => raise THM ("RSN: multiple unifiers", i, [tha, thb]));
-
-(*Resolution: P \<Longrightarrow> Q, Q \<Longrightarrow> R gives P \<Longrightarrow> R*)
-fun tha RS thb = tha RSN (1,thb);
-
(*For joining lists of rules*)
fun thas RLN (i, thbs) =
let
--- a/src/Pure/more_thm.ML Thu Aug 01 14:46:50 2019 +0200
+++ b/src/Pure/more_thm.ML Fri Aug 02 11:23:09 2019 +0200
@@ -53,7 +53,6 @@
val class_triv: theory -> class -> thm
val of_sort: ctyp * sort -> thm list
val is_dummy: thm -> bool
- val plain_prop_of: thm -> term
val add_thm: thm -> thm list -> thm list
val del_thm: thm -> thm list -> thm list
val merge_thms: thm list * thm list -> thm list
@@ -268,20 +267,6 @@
NONE => false
| SOME t => Term.is_dummy_pattern (Term.head_of t));
-fun plain_prop_of raw_thm =
- let
- val thm = Thm.strip_shyps raw_thm;
- fun err msg = raise THM ("plain_prop_of: " ^ msg, 0, [thm]);
- in
- if not (null (Thm.hyps_of thm)) then
- err "theorem may not contain hypotheses"
- else if not (null (Thm.extra_shyps thm)) then
- err "theorem may not contain sort hypotheses"
- else if not (null (Thm.tpairs_of thm)) then
- err "theorem may not contain flex-flex pairs"
- else Thm.prop_of thm
- end;
-
(* collections of theorems in canonical order *)
--- a/src/Pure/thm.ML Thu Aug 01 14:46:50 2019 +0200
+++ b/src/Pure/thm.ML Fri Aug 02 11:23:09 2019 +0200
@@ -7,6 +7,8 @@
resolution), oracles.
*)
+infix 0 RS RSN;
+
signature BASIC_THM =
sig
type ctyp
@@ -15,6 +17,8 @@
type thm
type conv = cterm -> thm
exception THM of string * int * thm list
+ val RSN: thm * (int * thm) -> thm
+ val RS: thm * thm -> thm
end;
signature THM =
@@ -145,6 +149,7 @@
val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
val varifyT_global: thm -> thm
val legacy_freezeT: thm -> thm
+ val plain_prop_of: thm -> term
val dest_state: thm * int -> (term * term) list * term list * term * term
val lift_rule: cterm -> thm -> thm
val incr_indexes: int -> thm -> thm
@@ -155,6 +160,12 @@
val bicompose: Proof.context option -> {flatten: bool, match: bool, incremented: bool} ->
bool * thm * int -> int -> thm -> thm Seq.seq
val biresolution: Proof.context option -> bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
+ val is_classrel: theory -> class * class -> bool
+ val the_classrel: theory -> class * class -> thm
+ val the_arity: theory -> string * sort list * class -> thm
+ val thynames_of_arity: theory -> string * class -> string list
+ val add_classrel: thm -> theory -> theory
+ val add_arity: thm -> theory -> theory
end;
structure Thm: THM =
@@ -394,6 +405,7 @@
fun full_prop_of (Thm (_, {tpairs, prop, ...})) = attach_tpairs tpairs prop;
+
val union_hyps = Ord_List.union Term_Ord.fast_term_ord;
val insert_hyps = Ord_List.insert Term_Ord.fast_term_ord;
val remove_hyps = Ord_List.remove Term_Ord.fast_term_ord;
@@ -817,17 +829,41 @@
(*** Theory data ***)
+datatype sorts = Sorts of
+ {classrels: thm Symreltab.table,
+ arities: ((class * sort list) * (thm * string)) list Symtab.table};
+
+fun make_sorts (classrels, arities) = Sorts {classrels = classrels, arities = arities};
+
+val empty_sorts = make_sorts (Symreltab.empty, Symtab.empty);
+
+fun merge_sorts
+ (Sorts {classrels = classrels1, arities = arities1},
+ Sorts {classrels = classrels2, arities = arities2}) =
+ let
+ (*see Theory.at_begin hook for transitive closure of classrels and arity completion*)
+ val classrels' = Symreltab.merge (K true) (classrels1, classrels2);
+ val arities' = Symtab.merge_list (eq_fst op =) (arities1, arities2);
+ in make_sorts (classrels', arities') end;
+
+
structure Data = Theory_Data
(
type T =
- unit Name_Space.table; (*oracles: authentic derivation names*)
- val empty : T = Name_Space.empty_table "oracle";
+ unit Name_Space.table * (*oracles: authentic derivation names*)
+ sorts; (*sort algebra within the logic*)
+
+ val empty : T = (Name_Space.empty_table "oracle", empty_sorts);
val extend = I;
- fun merge data : T = Name_Space.merge_tables data;
+ fun merge ((oracles1, sorts1), (oracles2, sorts2)) : T =
+ (Name_Space.merge_tables (oracles1, oracles2), merge_sorts (sorts1, sorts2));
);
-val get_oracles = Data.get;
-val map_oracles = Data.map;
+val get_oracles = #1 o Data.get;
+val map_oracles = Data.map o apfst;
+
+val get_sorts = (fn (_, Sorts args) => args) o Data.get;
+val map_sorts = Data.map o apsnd;
@@ -1511,6 +1547,20 @@
prop = prop3})
end;
+fun plain_prop_of raw_thm =
+ let
+ val thm = strip_shyps raw_thm;
+ fun err msg = raise THM ("plain_prop_of: " ^ msg, 0, [thm]);
+ in
+ if not (null (hyps_of thm)) then
+ err "theorem may not contain hypotheses"
+ else if not (null (extra_shyps thm)) then
+ err "theorem may not contain sort hypotheses"
+ else if not (null (tpairs_of thm)) then
+ err "theorem may not contain flex-flex pairs"
+ else prop_of thm
+ end;
+
(*** Inference rules for tactics ***)
@@ -1910,6 +1960,163 @@
else res brules
in Seq.flat (res brules) end;
+(*Resolution: exactly one resolvent must be produced*)
+fun tha RSN (i, thb) =
+ (case Seq.chop 2 (biresolution NONE false [(false, tha)] i thb) of
+ ([th], _) => th
+ | ([], _) => raise THM ("RSN: no unifiers", i, [tha, thb])
+ | _ => raise THM ("RSN: multiple unifiers", i, [tha, thb]));
+
+(*Resolution: P \<Longrightarrow> Q, Q \<Longrightarrow> R gives P \<Longrightarrow> R*)
+fun tha RS thb = tha RSN (1,thb);
+
+
+
+(*** sort algebra within the logic ***)
+
+fun standard_tvars thm =
+ let
+ val thy = theory_of_thm thm;
+ val tvars = rev (Term.add_tvars (prop_of thm) []);
+ val names = Name.invent Name.context Name.aT (length tvars);
+ val tinst =
+ map2 (fn (ai, S) => fn b => ((ai, S), global_ctyp_of thy (TVar ((b, 0), S)))) tvars names;
+ in instantiate (tinst, []) thm end
+
+
+(* class relations *)
+
+val get_classrels = #classrels o get_sorts;
+fun map_classrels f = map_sorts (fn Sorts {classrels, arities} => make_sorts (f classrels, arities));
+
+val is_classrel = Symreltab.defined o get_classrels;
+
+fun the_classrel thy (c1, c2) =
+ (case Symreltab.lookup (get_classrels thy) (c1, c2) of
+ SOME thm => transfer thy thm
+ | NONE => error ("Unproven class relation " ^
+ Syntax.string_of_classrel (Proof_Context.init_global thy) [c1, c2]));
+
+fun complete_classrels thy =
+ let
+ fun complete (c, (_, (all_preds, all_succs))) (finished1, thy1) =
+ let
+ fun compl c1 c2 (finished2, thy2) =
+ if is_classrel thy2 (c1, c2) then (finished2, thy2)
+ else
+ (false,
+ thy2
+ |> (map_classrels o Symreltab.update) ((c1, c2),
+ (the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2))
+ |> standard_tvars
+ |> close_derivation
+ |> trim_context));
+
+ val proven = is_classrel thy1;
+ val preds = Graph.Keys.fold (fn c1 => proven (c1, c) ? cons c1) all_preds [];
+ val succs = Graph.Keys.fold (fn c2 => proven (c, c2) ? cons c2) all_succs [];
+ in
+ fold_product compl preds succs (finished1, thy1)
+ end;
+ in
+ (case Graph.fold complete (Sorts.classes_of (Sign.classes_of thy)) (true, thy) of
+ (true, _) => NONE
+ | (_, thy') => SOME thy')
+ end;
+
+
+(* type arities *)
+
+val get_arities = #arities o get_sorts;
+fun map_arities f = map_sorts (fn Sorts {classrels, arities} => make_sorts (classrels, f arities));
+
+fun the_arity thy (a, Ss, c) =
+ (case AList.lookup (op =) (Symtab.lookup_list (get_arities thy) a) (c, Ss) of
+ SOME (thm, _) => transfer thy thm
+ | NONE => error ("Unproven type arity " ^
+ Syntax.string_of_arity (Proof_Context.init_global thy) (a, Ss, [c])));
+
+fun thynames_of_arity thy (a, c) =
+ Symtab.lookup_list (get_arities thy) a
+ |> map_filter (fn ((c', _), (_, name)) => if c = c' then SOME name else NONE)
+ |> rev;
+
+fun insert_arity_completions thy t ((c, Ss), ((th, thy_name))) (finished, arities) =
+ let
+ val algebra = Sign.classes_of thy;
+ val ars = Symtab.lookup_list arities t;
+ val super_class_completions =
+ Sign.super_classes thy c
+ |> filter_out (fn c1 => exists (fn ((c2, Ss2), _) =>
+ c1 = c2 andalso Sorts.sorts_le algebra (Ss2, Ss)) ars);
+
+ val completions = super_class_completions |> map (fn c1 =>
+ let
+ val th1 =
+ (th RS the_classrel thy (c, c1))
+ |> standard_tvars
+ |> close_derivation
+ |> trim_context;
+ in ((th1, thy_name), c1) end);
+
+ val finished' = finished andalso null completions;
+ val arities' = fold (fn (th, c1) => Symtab.cons_list (t, ((c1, Ss), th))) completions arities;
+ in (finished', arities') end;
+
+fun put_arity_completion ((t, Ss, c), th) thy =
+ let val ar = ((c, Ss), (th, Context.theory_name thy)) in
+ thy
+ |> map_arities
+ (Symtab.insert_list (eq_fst op =) (t, ar) #>
+ curry (insert_arity_completions thy t ar) true #> #2)
+ end;
+
+fun complete_arities thy =
+ let
+ val arities = get_arities thy;
+ val (finished, arities') =
+ Symtab.fold (fn (t, ars) => fold (insert_arity_completions thy t) ars)
+ arities (true, arities);
+ in
+ if finished then NONE
+ else SOME (map_arities (K arities') thy)
+ end;
+
+val _ =
+ Theory.setup
+ (Theory.at_begin complete_classrels #>
+ Theory.at_begin complete_arities #>
+ Proofterm.install_axclass_proofs
+ {classrel_proof = proof_of oo the_classrel,
+ arity_proof = proof_of oo the_arity});
+
+
+(* primitive rules *)
+
+fun add_classrel raw_th thy =
+ let
+ val th = strip_shyps (transfer thy raw_th);
+ val prop = plain_prop_of th;
+ val (c1, c2) = Logic.dest_classrel prop;
+ in
+ thy
+ |> Sign.primitive_classrel (c1, c2)
+ |> map_classrels (Symreltab.update ((c1, c2), th |> unconstrainT |> trim_context))
+ |> perhaps complete_classrels
+ |> perhaps complete_arities
+ end;
+
+fun add_arity raw_th thy =
+ let
+ val th = strip_shyps (transfer thy raw_th);
+ val prop = plain_prop_of th;
+ val (t, Ss, c) = Logic.dest_arity prop;
+ in
+ thy
+ |> Sign.primitive_arity (t, Ss, [c])
+ |> put_arity_completion ((t, Ss, c), th |> unconstrainT |> trim_context)
+ end;
+
end;
structure Basic_Thm: BASIC_THM = Thm;
--- a/src/Tools/Code/code_symbol.ML Thu Aug 01 14:46:50 2019 +0200
+++ b/src/Tools/Code/code_symbol.ML Fri Aug 02 11:23:09 2019 +0200
@@ -99,7 +99,7 @@
local
fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy);
- fun thyname_of_instance thy inst = case Axclass.thynames_of_arity thy inst
+ fun thyname_of_instance thy inst = case Thm.thynames_of_arity thy inst
of [] => error ("No such instance: " ^ quote (fst inst ^ " :: " ^ snd inst))
| thyname :: _ => thyname;
fun thyname_of_const thy c = case Axclass.class_of_param thy c