src/Pure/Isar/spec_rules.ML

adapted LocalTheory.declaration;

(*  Title:      Pure/Isar/spec_rules.ML
    Author:     Makarius

Rules that characterize specifications, with rough classification.
NB: In the face of arbitrary morphisms, the original shape of
specifications may get lost.
*)

signature SPEC_RULES =
sig
  datatype rough_classification = Unknown | Equational | Inductive | Co_Inductive
  type spec = rough_classification * (term list * thm list)
  val get: Proof.context -> spec list
  val get_global: theory -> 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
end;

structure Spec_Rules: SPEC_RULES =
struct

(* maintain rules *)

datatype rough_classification = Unknown | Equational | Inductive | Co_Inductive;
type spec = rough_classification * (term list * thm list);

structure Rules = GenericDataFun
(
  type T = spec Item_Net.T;
  val empty : T =
    Item_Net.init
      (fn ((class1, (ts1, ths1)), (class2, (ts2, ths2))) =>
        class1 = class2 andalso
        eq_list (op aconv) (ts1, ts2) andalso
        eq_list Thm.eq_thm_prop (ths1, ths2))
      (#1 o #2);
  val extend = I;
  fun merge _ = Item_Net.merge;
);

val get = Item_Net.content o Rules.get o Context.Proof;
val get_global = Item_Net.content o Rules.get o Context.Theory;

fun add class (ts, ths) = LocalTheory.declaration true
  (fn phi =>
    let
      val ts' = map (Morphism.term phi) ts;
      val ths' = map (Morphism.thm phi) ths;
    in Rules.map (Item_Net.update (class, (ts', ths'))) end);

fun add_global class spec =
  Context.theory_map (Rules.map (Item_Net.update (class, spec)));

end;