# HG changeset patch
# User wenzelm
# Date 1564737789 -7200
# Node ID c742527a25fe34e8ba30d448ebc8cf35de1b1311
# Parent  f0d9f873f470cc26caccc1f907910ddd3eca2ece
clarified modules: inference kernel maintains sort algebra within the logic;

diff -r f0d9f873f470 -r c742527a25fe src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- 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
diff -r f0d9f873f470 -r c742527a25fe src/Pure/axclass.ML
--- 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
diff -r f0d9f873f470 -r c742527a25fe src/Pure/drule.ML
--- 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
diff -r f0d9f873f470 -r c742527a25fe src/Pure/more_thm.ML
--- 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 *)
 
diff -r f0d9f873f470 -r c742527a25fe src/Pure/thm.ML
--- 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;
diff -r f0d9f873f470 -r c742527a25fe src/Tools/Code/code_symbol.ML
--- 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