src/Pure/Isar/spec_rules.ML
author wenzelm
Mon Nov 14 16:52:19 2011 +0100 (2011-11-14 ago)
changeset 45488 6d71d9e52369
parent 45291 57cd50f98fdc
child 59573 d09cc83cdce9
permissions -rw-r--r--
pass positions for named targets, for formal links in the document model;
     1 (*  Title:      Pure/Isar/spec_rules.ML
     2     Author:     Makarius
     3 
     4 Rules that characterize specifications, with rough classification.
     5 NB: In the face of arbitrary morphisms, the original shape of
     6 specifications may get lost.
     7 *)
     8 
     9 signature SPEC_RULES =
    10 sig
    11   datatype rough_classification = Unknown | Equational | Inductive | Co_Inductive
    12   type spec = rough_classification * (term list * thm list)
    13   val get: Proof.context -> spec list
    14   val get_global: theory -> spec list
    15   val retrieve: Proof.context -> term -> spec list
    16   val retrieve_global: theory -> term -> spec list
    17   val add: rough_classification -> term list * thm list -> local_theory -> local_theory
    18   val add_global: rough_classification -> term list * thm list -> theory -> theory
    19 end;
    20 
    21 structure Spec_Rules: SPEC_RULES =
    22 struct
    23 
    24 (* maintain rules *)
    25 
    26 datatype rough_classification = Unknown | Equational | Inductive | Co_Inductive;
    27 type spec = rough_classification * (term list * thm list);
    28 
    29 structure Rules = Generic_Data
    30 (
    31   type T = spec Item_Net.T;
    32   val empty : T =
    33     Item_Net.init
    34       (fn ((class1, (ts1, ths1)), (class2, (ts2, ths2))) =>
    35         class1 = class2 andalso
    36         eq_list (op aconv) (ts1, ts2) andalso
    37         eq_list Thm.eq_thm_prop (ths1, ths2))
    38       (#1 o #2);
    39   val extend = I;
    40   val merge = Item_Net.merge;
    41 );
    42 
    43 val get = Item_Net.content o Rules.get o Context.Proof;
    44 val get_global = Item_Net.content o Rules.get o Context.Theory;
    45 
    46 val retrieve = Item_Net.retrieve o Rules.get o Context.Proof;
    47 val retrieve_global = Item_Net.retrieve o Rules.get o Context.Theory;
    48 
    49 fun add class (ts, ths) lthy =
    50   let
    51     val cts = map (Thm.cterm_of (Proof_Context.theory_of lthy)) ts;
    52   in
    53     lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
    54       (fn phi =>
    55         let
    56           val (ts', ths') =
    57             Morphism.fact phi (map Drule.mk_term cts @ ths)
    58             |> chop (length cts)
    59             |>> map (Thm.term_of o Drule.dest_term);
    60         in Rules.map (Item_Net.update (class, (ts', ths'))) end)
    61   end;
    62 
    63 fun add_global class spec =
    64   Context.theory_map (Rules.map (Item_Net.update (class, spec)));
    65 
    66 end;