src/Pure/Isar/spec_rules.ML
author wenzelm
Mon May 03 14:25:56 2010 +0200 (2010-05-03)
changeset 36610 bafd82950e24
parent 34948 2d5f2a9f7601
child 41472 f6ab14e61604
permissions -rw-r--r--
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm@33374
     1
(*  Title:      Pure/Isar/spec_rules.ML
wenzelm@33374
     2
    Author:     Makarius
wenzelm@33374
     3
wenzelm@33454
     4
Rules that characterize specifications, with rough classification.
wenzelm@33454
     5
NB: In the face of arbitrary morphisms, the original shape of
wenzelm@33454
     6
specifications may get lost.
wenzelm@33374
     7
*)
wenzelm@33374
     8
wenzelm@33374
     9
signature SPEC_RULES =
wenzelm@33374
    10
sig
wenzelm@33454
    11
  datatype rough_classification = Unknown | Equational | Inductive | Co_Inductive
wenzelm@33454
    12
  type spec = rough_classification * (term list * thm list)
wenzelm@33454
    13
  val get: Proof.context -> spec list
wenzelm@33454
    14
  val get_global: theory -> spec list
bulwahn@34948
    15
  val retrieve: Proof.context -> term -> spec list
bulwahn@34948
    16
  val retrieve_global: theory -> term -> spec list
wenzelm@33454
    17
  val add: rough_classification -> term list * thm list -> local_theory -> local_theory
wenzelm@33454
    18
  val add_global: rough_classification -> term list * thm list -> theory -> theory
wenzelm@33374
    19
end;
wenzelm@33374
    20
wenzelm@33374
    21
structure Spec_Rules: SPEC_RULES =
wenzelm@33374
    22
struct
wenzelm@33374
    23
wenzelm@33374
    24
(* maintain rules *)
wenzelm@33374
    25
wenzelm@33454
    26
datatype rough_classification = Unknown | Equational | Inductive | Co_Inductive;
wenzelm@33454
    27
type spec = rough_classification * (term list * thm list);
wenzelm@33374
    28
wenzelm@33519
    29
structure Rules = Generic_Data
wenzelm@33374
    30
(
wenzelm@33454
    31
  type T = spec Item_Net.T;
wenzelm@33374
    32
  val empty : T =
wenzelm@33374
    33
    Item_Net.init
wenzelm@33454
    34
      (fn ((class1, (ts1, ths1)), (class2, (ts2, ths2))) =>
wenzelm@33454
    35
        class1 = class2 andalso
wenzelm@33454
    36
        eq_list (op aconv) (ts1, ts2) andalso
wenzelm@33454
    37
        eq_list Thm.eq_thm_prop (ths1, ths2))
wenzelm@33454
    38
      (#1 o #2);
wenzelm@33374
    39
  val extend = I;
wenzelm@33519
    40
  fun merge data = Item_Net.merge data;
wenzelm@33374
    41
);
wenzelm@33374
    42
wenzelm@33454
    43
val get = Item_Net.content o Rules.get o Context.Proof;
wenzelm@33454
    44
val get_global = Item_Net.content o Rules.get o Context.Theory;
wenzelm@33374
    45
bulwahn@34948
    46
val retrieve = Item_Net.retrieve o Rules.get o Context.Proof;
bulwahn@34948
    47
val retrieve_global = Item_Net.retrieve o Rules.get o Context.Theory;
bulwahn@34948
    48
wenzelm@33702
    49
fun add class (ts, ths) lthy =
wenzelm@33702
    50
  let
wenzelm@33702
    51
    val cts = map (Thm.cterm_of (ProofContext.theory_of lthy)) ts;
wenzelm@33702
    52
  in
wenzelm@33702
    53
    lthy |> Local_Theory.declaration true
wenzelm@33702
    54
      (fn phi =>
wenzelm@33702
    55
        let
wenzelm@33702
    56
          val (ts', ths') =
wenzelm@33702
    57
            Morphism.fact phi (map Drule.mk_term cts @ ths)
wenzelm@33702
    58
            |> chop (length cts)
wenzelm@33702
    59
            |>> map (Thm.term_of o Drule.dest_term);
wenzelm@33702
    60
        in Rules.map (Item_Net.update (class, (ts', ths'))) end)
wenzelm@33702
    61
  end;
wenzelm@33374
    62
wenzelm@33454
    63
fun add_global class spec =
wenzelm@33454
    64
  Context.theory_map (Rules.map (Item_Net.update (class, spec)));
wenzelm@33374
    65
wenzelm@33374
    66
end;